NuITP (alpha 30) ProofProved


Goal

False = shuffle($2:NeList, $3:NeList, $1:Card)

Script

set goal shuffle(L1:NeList, L2:NeList, C:Card) = False .
apply ns* to 0 .

Rewriting Theory

fmod GILBREATH-ACU is
sorts Boolean Card List NeList .
subsort Card < NeList .
subsort NeList < List .
op False : -> Boolean [ ctor metadata "1" ] .
op True : -> Boolean [ ctor metadata "0" ] .
op __ : List List -> List [ assoc id: nil metadata "5" ] .
op __ : NeList NeList -> NeList [ assoc ctor id: nil metadata "5" ] .
op alter : List -> Boolean [ metadata "8" ] .
op black : -> Card [ ctor metadata "3" ] .
op even : List -> Boolean [ metadata "11" ] .
op neg : Card -> Card [ metadata "12" ] .
op nil : -> List [ ctor metadata "2" ] .
op opposite : List List -> Boolean [ metadata "7" ] .
op paired : Card Card -> Boolean [ metadata "6" ] .
op pairedList : List -> Boolean [ metadata "9" ] .
op red : -> Card [ ctor metadata "4" ] .
op rotate : List -> List [ metadata "13" ] .
op shuffle : List List List -> Boolean [ metadata "10" ] .
eq alter(C:Card) = True .
eq alter(nil) = True .
eq even(C:Card) = False .
eq even(nil) = True .
eq even(L1:List C1:Card L2:List C2:Card L3:List) = even(L1:List L2:List L3:List) .
eq neg(black) = red [ variant ] .
eq neg(red) = black [ variant ] .
eq opposite(L:List, nil) = False [ variant ] .
eq opposite(nil, L:List) = False [ variant ] .
eq opposite(C1:Card L1:List, C2:Card L2:List) = paired(C1:Card, C2:Card) [ variant ] .
eq paired(C:Card, C:Card) = False [ variant ] .
eq paired(black, red) = True [ variant ] .
eq paired(red, black) = True [ variant ] .
eq pairedList(C:Card) = False .
eq pairedList(nil) = True .
eq pairedList(C:Card C:Card L:List) = False .
eq rotate(nil) = nil [ variant ] .
eq rotate(C:Card L:List) = L:List C:Card [ variant ] .
eq shuffle(L1:List, C2:Card L2:List, nil) = False .
eq shuffle(nil, nil, nil) = True .
eq shuffle(nil, nil, C3:Card L3:List) = False .
eq shuffle(C1:Card L1:List, L2:List, nil) = False .
ceq alter(C1:Card C2:Card L:List) = False if paired(C1:Card, C2:Card) = False .
ceq alter(C1:Card C2:Card L:List) = alter(C2:Card L:List) if paired(C1:Card, C2:Card) = True .
ceq pairedList(C1:Card C2:Card L:List) = pairedList(L:List) if paired(C1:Card, C2:Card) = True .
ceq shuffle(nil, C2:Card L2:List, C3:Card L3:List) = False if paired(C2:Card, C3:Card) = True .
ceq shuffle(nil, C2:Card L2:List, C3:Card L3:List) = shuffle(nil, L2:List, L3:List) if paired(C2:Card, C3:Card) = False .
ceq shuffle(C1:Card L1:List, nil, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True .
ceq shuffle(C1:Card L1:List, nil, C3:Card L3:List) = shuffle(L1:List, nil, L3:List) if paired(C1:Card, C3:Card) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True /\ paired(C2:Card, C3:Card) = True .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C1:Card, C3:Card) = True /\ shuffle(C1:Card L1:List, L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if paired(C2:Card, C3:Card) = True /\ shuffle(L1:List, C2:Card L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = False if shuffle(L1:List, C2:Card L2:List, L3:List) = False /\ shuffle(C1:Card L1:List, L2:List, L3:List) = False .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = True if paired(C1:Card, C3:Card) = False /\ shuffle(L1:List, C2:Card L2:List, L3:List) = True .
ceq shuffle(C1:Card L1:List, C2:Card L2:List, C3:Card L3:List) = True if paired(C2:Card, C3:Card) = False /\ shuffle(C1:Card L1:List, L2:List, L3:List) = True .
endfm

Goals

Goal Id:  0
Generated By:  init
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
False = shuffle($2:NeList, $3:NeList, $1:Card)
Goal Id:  0.1
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ False = shuffle($4:Card, nil, nil) → False = False
Goal Id:  0.10
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.100
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.101
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $8:Card)) /\ True = shuffle($5:NeList, $6:Card $7:NeList, nil) → False = True
Goal Id:  0.102
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $7:Card)) /\ True = shuffle($5:NeList, $6:Card, nil) → False = True
Goal Id:  0.103
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $7:Card)) /\ True = shuffle(nil, $5:Card $6:NeList, nil) → False = True
Goal Id:  0.104
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $6:Card)) /\ True = shuffle(nil, $5:Card, nil) → False = True
Goal Id:  0.105
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($6:Card, $8:Card)) /\ True = shuffle($4:Card $5:NeList, $7:NeList, nil) → False = True
Goal Id:  0.106
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($6:Card, $7:Card)) /\ True = shuffle($4:Card $5:NeList, nil, nil) → False = True
Goal Id:  0.107
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $7:Card)) /\ True = shuffle($4:Card, $6:NeList, nil) → False = True
Goal Id:  0.108
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $6:Card)) /\ True = shuffle($4:Card, nil, nil) → False = True
Goal Id:  0.11
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $6:Card)) /\ True = shuffle(nil, $5:Card, nil) → False = True
Goal Id:  0.12
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $6:Card)) /\ True = shuffle($4:Card, nil, nil) → False = True
Goal Id:  0.13
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card $6:NeList, nil)) /\ False = shuffle($4:Card, $6:NeList, nil) → False = False
Goal Id:  0.14
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ False = shuffle($4:Card, nil, nil) → False = False
Goal Id:  0.15
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, $6:NeList, nil)) /\ True = paired($4:Card, $7:Card) → False = False
Goal Id:  0.16
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, nil, nil)) /\ True = paired($4:Card, $6:Card) → False = False
Goal Id:  0.17
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $7:Card)) /\ True = paired($5:Card, $7:Card) → False = False
Goal Id:  0.18
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $6:Card)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.19
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card $6:NeList, nil)) /\ True = paired($5:Card, $7:Card) → False = False
Goal Id:  0.2
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, nil, nil)) /\ True = paired($4:Card, $6:Card) → False = False
Goal Id:  0.20
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.21
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $7:Card)) /\ True = shuffle(nil, $5:Card $6:NeList, nil) → False = True
Goal Id:  0.22
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $6:Card)) /\ True = shuffle(nil, $5:Card, nil) → False = True
Goal Id:  0.23
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $7:Card)) /\ True = shuffle($4:Card, $6:NeList, nil) → False = True
Goal Id:  0.24
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $6:Card)) /\ True = shuffle($4:Card, nil, nil) → False = True
Goal Id:  0.25
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card $6:NeList, nil)) /\ False = shuffle($4:Card, $6:NeList, nil) → False = False
Goal Id:  0.26
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ False = shuffle($4:Card, nil, nil) → False = False
Goal Id:  0.27
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, $6:NeList, nil)) /\ True = paired($4:Card, $7:Card) → False = False
Goal Id:  0.28
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, nil, nil)) /\ True = paired($4:Card, $6:Card) → False = False
Goal Id:  0.29
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $7:Card)) /\ True = paired($5:Card, $7:Card) → False = False
Goal Id:  0.3
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $6:Card)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.30
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $6:Card)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.31
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card $6:NeList, nil)) /\ True = paired($5:Card, $7:Card) → False = False
Goal Id:  0.32
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.33
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $7:Card)) /\ True = shuffle(nil, $5:Card $6:NeList, nil) → False = True
Goal Id:  0.34
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $6:Card)) /\ True = shuffle(nil, $5:Card, nil) → False = True
Goal Id:  0.35
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $7:Card)) /\ True = shuffle($4:Card, $6:NeList, nil) → False = True
Goal Id:  0.36
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $6:Card)) /\ True = shuffle($4:Card, nil, nil) → False = True
Goal Id:  0.37
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card, nil)) /\ False = shuffle($4:Card $5:NeList, nil, nil) → False = False
Goal Id:  0.38
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ False = shuffle($4:Card, nil, nil) → False = False
Goal Id:  0.39
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card $5:NeList, nil, nil)) /\ True = paired($4:Card, $7:Card) → False = False
Goal Id:  0.4
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.40
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, nil, nil)) /\ True = paired($4:Card, $6:Card) → False = False
Goal Id:  0.41
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $7:Card)) /\ True = paired($6:Card, $7:Card) → False = False
Goal Id:  0.42
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $6:Card)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.43
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card, nil)) /\ True = paired($6:Card, $7:Card) → False = False
Goal Id:  0.44
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.45
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $7:Card)) /\ True = shuffle($5:NeList, $6:Card, nil) → False = True
Goal Id:  0.46
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $6:Card)) /\ True = shuffle(nil, $5:Card, nil) → False = True
Goal Id:  0.47
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($6:Card, $7:Card)) /\ True = shuffle($4:Card $5:NeList, nil, nil) → False = True
Goal Id:  0.48
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $6:Card)) /\ True = shuffle($4:Card, nil, nil) → False = True
Goal Id:  0.49
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card, nil)) /\ False = shuffle($4:Card $5:NeList, nil, nil) → False = False
Goal Id:  0.5
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $6:Card)) /\ True = shuffle(nil, $5:Card, nil) → False = True
Goal Id:  0.50
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ False = shuffle($4:Card, nil, nil) → False = False
Goal Id:  0.51
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card $5:NeList, nil, nil)) /\ True = paired($4:Card, $7:Card) → False = False
Goal Id:  0.52
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, nil, nil)) /\ True = paired($4:Card, $6:Card) → False = False
Goal Id:  0.53
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $7:Card)) /\ True = paired($6:Card, $7:Card) → False = False
Goal Id:  0.54
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $6:Card)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.55
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card, nil)) /\ True = paired($6:Card, $7:Card) → False = False
Goal Id:  0.56
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.57
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $7:Card)) /\ True = shuffle($5:NeList, $6:Card, nil) → False = True
Goal Id:  0.58
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $6:Card)) /\ True = shuffle(nil, $5:Card, nil) → False = True
Goal Id:  0.59
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($6:Card, $7:Card)) /\ True = shuffle($4:Card $5:NeList, nil, nil) → False = True
Goal Id:  0.6
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $6:Card)) /\ True = shuffle($4:Card, nil, nil) → False = True
Goal Id:  0.60
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $6:Card)) /\ True = shuffle($4:Card, nil, nil) → False = True
Goal Id:  0.61
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card $7:NeList, nil)) /\ False = shuffle($4:Card $5:NeList, $7:NeList, nil) → False = False
Goal Id:  0.62
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card, nil)) /\ False = shuffle($4:Card $5:NeList, nil, nil) → False = False
Goal Id:  0.63
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card $6:NeList, nil)) /\ False = shuffle($4:Card, $6:NeList, nil) → False = False
Goal Id:  0.64
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ False = shuffle($4:Card, nil, nil) → False = False
Goal Id:  0.65
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card $5:NeList, $7:NeList, nil)) /\ True = paired($4:Card, $8:Card) → False = False
Goal Id:  0.66
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card $5:NeList, nil, nil)) /\ True = paired($4:Card, $7:Card) → False = False
Goal Id:  0.67
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, $6:NeList, nil)) /\ True = paired($4:Card, $7:Card) → False = False
Goal Id:  0.68
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, nil, nil)) /\ True = paired($4:Card, $6:Card) → False = False
Goal Id:  0.69
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $8:Card)) /\ True = paired($6:Card, $8:Card) → False = False
Goal Id:  0.7
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ False = shuffle($4:Card, nil, nil) → False = False
Goal Id:  0.70
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $7:Card)) /\ True = paired($6:Card, $7:Card) → False = False
Goal Id:  0.71
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $7:Card)) /\ True = paired($5:Card, $7:Card) → False = False
Goal Id:  0.72
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $6:Card)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.73
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card $7:NeList, nil)) /\ True = paired($6:Card, $8:Card) → False = False
Goal Id:  0.74
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card, nil)) /\ True = paired($6:Card, $7:Card) → False = False
Goal Id:  0.75
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card $6:NeList, nil)) /\ True = paired($5:Card, $7:Card) → False = False
Goal Id:  0.76
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.77
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $8:Card)) /\ True = shuffle($5:NeList, $6:Card $7:NeList, nil) → False = True
Goal Id:  0.78
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $7:Card)) /\ True = shuffle($5:NeList, $6:Card, nil) → False = True
Goal Id:  0.79
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $7:Card)) /\ True = shuffle(nil, $5:Card $6:NeList, nil) → False = True
Goal Id:  0.8
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, nil, nil)) /\ True = paired($4:Card, $6:Card) → False = False
Goal Id:  0.80
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($4:Card, $6:Card)) /\ True = shuffle(nil, $5:Card, nil) → False = True
Goal Id:  0.81
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($6:Card, $8:Card)) /\ True = shuffle($4:Card $5:NeList, $7:NeList, nil) → False = True
Goal Id:  0.82
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($6:Card, $7:Card)) /\ True = shuffle($4:Card $5:NeList, nil, nil) → False = True
Goal Id:  0.83
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $7:Card)) /\ True = shuffle($4:Card, $6:NeList, nil) → False = True
Goal Id:  0.84
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired($5:Card, $6:Card)) /\ True = shuffle($4:Card, nil, nil) → False = True
Goal Id:  0.85
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card $7:NeList, nil)) /\ False = shuffle($4:Card $5:NeList, $7:NeList, nil) → False = False
Goal Id:  0.86
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card, nil)) /\ False = shuffle($4:Card $5:NeList, nil, nil) → False = False
Goal Id:  0.87
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card $6:NeList, nil)) /\ False = shuffle($4:Card, $6:NeList, nil) → False = False
Goal Id:  0.88
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card, nil)) /\ False = shuffle($4:Card, nil, nil) → False = False
Goal Id:  0.89
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card $5:NeList, $7:NeList, nil)) /\ True = paired($4:Card, $8:Card) → False = False
Goal Id:  0.9
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $6:Card)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.90
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card $5:NeList, nil, nil)) /\ True = paired($4:Card, $7:Card) → False = False
Goal Id:  0.91
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, $6:NeList, nil)) /\ True = paired($4:Card, $7:Card) → False = False
Goal Id:  0.92
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($4:Card, nil, nil)) /\ True = paired($4:Card, $6:Card) → False = False
Goal Id:  0.93
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $8:Card)) /\ True = paired($6:Card, $8:Card) → False = False
Goal Id:  0.94
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $7:Card)) /\ True = paired($6:Card, $7:Card) → False = False
Goal Id:  0.95
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $7:Card)) /\ True = paired($5:Card, $7:Card) → False = False
Goal Id:  0.96
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired($4:Card, $6:Card)) /\ True = paired($5:Card, $6:Card) → False = False
Goal Id:  0.97
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card $7:NeList, nil)) /\ True = paired($6:Card, $8:Card) → False = False
Goal Id:  0.98
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle($5:NeList, $6:Card, nil)) /\ True = paired($6:Card, $7:Card) → False = False
Goal Id:  0.99
Generated By:  NS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(nil, $5:Card $6:NeList, nil)) /\ True = paired($5:Card, $7:Card) → False = False
Goal Id:  0.1.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.10.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.100.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.101.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.102.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.103.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.104.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.105.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.106.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.107.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.108.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.11.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.12.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.13.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.14.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.15.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.16.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.17.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.18.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.19.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.20.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.21.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.22.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.23.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.24.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.25.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.26.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.27.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.28.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.29.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.30.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.31.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.32.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.33.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.34.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.35.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.36.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.37.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.38.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.39.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.4.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.40.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.41.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.42.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.43.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.44.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.45.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.46.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.47.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.48.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.49.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.50.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.51.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.52.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.53.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.54.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.55.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.56.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.57.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.58.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.59.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.6.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.60.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.61.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.62.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.63.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.64.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.65.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.66.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.67.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.68.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.69.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.70.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.71.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.72.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.73.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.74.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.75.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.76.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.77.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.78.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.79.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.80.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.81.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.82.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.83.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.84.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.85.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.86.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.87.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.88.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.89.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.9.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.90.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.91.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.92.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.93.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.94.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.95.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.96.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.97.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.98.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.99.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true

Proof Tree