NuITP (alpha 30) ProofProved


Goal

True = paired($1:Card, $2:Card) → shuffle($3:List, $2:Card $4:List, $5:List) = shuffle($1:Card $3:List, $2:Card $4:List, $1:Card $5:List)

Script

set goal (paired(C1:Card,C2:Card) = True) → shuffle(C1:Card L1:List, C2:Card L2:List, C1:Card L3:List) = shuffle(L1:List, C2:Card L2:List, L3:List) .
apply ufree* to 0 .
apply ni! to 0.5.1 on shuffle(black $6:NeList, red, black $7:NeList) .
apply ni! to 0.5.2 on shuffle(red $6:NeList, black, red $7:NeList) .
apply ni! to 0.7.1 on shuffle(black, red $6:NeList, black $7:NeList) .
apply ni! to 0.7.2 on shuffle(red, black $6:NeList, red $7:NeList) .
apply ni! to 0.8.1 on shuffle(black $6:NeList, red $7:NeList, black $8:NeList) .
apply ni! to 0.8.2 on shuffle(red $6:NeList, black $7:NeList, red $8:NeList) .

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:
True = paired($1:Card, $2:Card) → shuffle($3:List, $2:Card $4:List, $5:List) = shuffle($1:Card $3:List, $2:Card $4:List, $1:Card $5:List)
Goal Id:  0.1
Generated By:  UFREE
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired($1:Card, $2:Card) → shuffle(nil, $2:Card, nil) = shuffle($1:Card, $2:Card, $1:Card)
Goal Id:  0.2
Generated By:  UFREE
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired($1:Card, $2:Card) → shuffle($6:NeList, $2:Card, nil) = shuffle($1:Card $6:NeList, $2:Card, $1:Card)
Goal Id:  0.3
Generated By:  UFREE
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired($1:Card, $2:Card) → shuffle(nil, $2:Card, $6:NeList) = shuffle($1:Card, $2:Card, $1:Card $6:NeList)
Goal Id:  0.4
Generated By:  UFREE
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired($1:Card, $2:Card) → shuffle(nil, $2:Card $6:NeList, nil) = shuffle($1:Card, $2:Card $6:NeList, $1:Card)
Goal Id:  0.5
Generated By:  UFREE
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired($1:Card, $2:Card) → shuffle($6:NeList, $2:Card, $7:NeList) = shuffle($1:Card $6:NeList, $2:Card, $1:Card $7:NeList)
Goal Id:  0.6
Generated By:  UFREE
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired($1:Card, $2:Card) → shuffle($6:NeList, $2:Card $7:NeList, nil) = shuffle($1:Card $6:NeList, $2:Card $7:NeList, $1:Card)
Goal Id:  0.7
Generated By:  UFREE
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired($1:Card, $2:Card) → shuffle(nil, $2:Card $6:NeList, $7:NeList) = shuffle($1:Card, $2:Card $6:NeList, $1:Card $7:NeList)
Goal Id:  0.8
Generated By:  UFREE
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
True = paired($1:Card, $2:Card) → shuffle($6:NeList, $2:Card $7:NeList, $8:NeList) = shuffle($1:Card $6:NeList, $2:Card $7:NeList, $1:Card $8:NeList)
Goal Id:  0.1.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.3.1
Generated By:  CVUL
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(black, red, black $6:NeList) = shuffle(nil, red, $6:NeList)
Goal Id:  0.3.2
Generated By:  CVUL
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(nil, black, $6:NeList) = shuffle(red, black, red $6:NeList)
Goal Id:  0.4.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1
Generated By:  CVUL
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle($6:NeList, red, $7:NeList) = shuffle(black $6:NeList, red, black $7:NeList)
Goal Id:  0.5.2
Generated By:  CVUL
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle($6:NeList, black, $7:NeList) = shuffle(red $6:NeList, black, red $7:NeList)
Goal Id:  0.6.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1
Generated By:  CVUL
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(black, red $6:NeList, black $7:NeList) = shuffle(nil, red $6:NeList, $7:NeList)
Goal Id:  0.7.2
Generated By:  CVUL
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(nil, black $6:NeList, $7:NeList) = shuffle(red, black $6:NeList, red $7:NeList)
Goal Id:  0.8.1
Generated By:  CVUL
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle($6:NeList, red $7:NeList, $8:NeList) = shuffle(black $6:NeList, red $7:NeList, black $8:NeList)
Goal Id:  0.8.2
Generated By:  CVUL
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle($6:NeList, black $7:NeList, $8:NeList) = shuffle(red $6:NeList, black $7:NeList, red $8:NeList)
Goal Id:  0.3.1.1
Generated By:  CAS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(black, red, black black) = shuffle(nil, red, black)
Goal Id:  0.3.1.2
Generated By:  CAS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(black, red, black red) = shuffle(nil, red, red)
Goal Id:  0.3.1.3
Generated By:  CAS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(black, red, black black $7:NeList) = shuffle(nil, red, black $7:NeList)
Goal Id:  0.3.1.4
Generated By:  CAS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(black, red, black red $7:NeList) = shuffle(nil, red, red $7:NeList)
Goal Id:  0.3.2.1
Generated By:  CAS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(nil, black, black) = shuffle(red, black, red black)
Goal Id:  0.3.2.2
Generated By:  CAS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(nil, black, red) = shuffle(red, black, red red)
Goal Id:  0.3.2.3
Generated By:  CAS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(nil, black, black $7:NeList) = shuffle(red, black, red black $7:NeList)
Goal Id:  0.3.2.4
Generated By:  CAS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
shuffle(nil, black, red $7:NeList) = shuffle(red, black, red red $7:NeList)
Goal Id:  0.5.1.1
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.10
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.11
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.12
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired(red, black)) /\ True = shuffle(black $8:NeList, nil, $9:NeList) → True = shuffle($8:NeList, red, $9:NeList)
Goal Id:  0.5.1.2
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(black $8:NeList, nil, $9:NeList)) /\ True = paired(black, black) → False = shuffle($8:NeList, red, $9:NeList)
Goal Id:  0.5.1.3
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired(black, black)) /\ True = paired(red, black) → False = shuffle($8:NeList, red, $9:NeList)
Goal Id:  0.5.1.4
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.5
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.6
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired(red, black)) /\ True = shuffle(black $8:NeList, nil, $9:NeList) → True = shuffle($8:NeList, red, $9:NeList)
Goal Id:  0.5.1.7
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.8
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(black $8:NeList, nil, $9:NeList)) /\ True = paired(black, black) → False = shuffle($8:NeList, red, $9:NeList)
Goal Id:  0.5.1.9
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired(black, black)) /\ True = paired(red, black) → False = shuffle($8:NeList, red, $9:NeList)
Goal Id:  0.5.2.1
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.10
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.11
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.12
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired(black, red)) /\ True = shuffle(red $8:NeList, nil, $9:NeList) → True = shuffle($8:NeList, black, $9:NeList)
Goal Id:  0.5.2.2
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(red $8:NeList, nil, $9:NeList)) /\ True = paired(red, red) → False = shuffle($8:NeList, black, $9:NeList)
Goal Id:  0.5.2.3
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired(black, red)) /\ True = paired(red, red) → False = shuffle($8:NeList, black, $9:NeList)
Goal Id:  0.5.2.4
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.5
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.6
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired(black, red)) /\ True = shuffle(red $8:NeList, nil, $9:NeList) → True = shuffle($8:NeList, black, $9:NeList)
Goal Id:  0.5.2.7
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.8
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(red $8:NeList, nil, $9:NeList)) /\ True = paired(red, red) → False = shuffle($8:NeList, black, $9:NeList)
Goal Id:  0.5.2.9
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired(black, red)) /\ True = paired(red, red) → False = shuffle($8:NeList, black, $9:NeList)
Goal Id:  0.7.1.1
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.10
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.11
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.12
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired(red, black)) /\ True = shuffle(black, $8:NeList, $9:NeList) → True = shuffle(nil, red $8:NeList, $9:NeList)
Goal Id:  0.7.1.2
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(black, $8:NeList, $9:NeList)) /\ True = paired(black, black) → False = shuffle(nil, red $8:NeList, $9:NeList)
Goal Id:  0.7.1.3
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired(black, black)) /\ True = paired(red, black) → False = shuffle(nil, red $8:NeList, $9:NeList)
Goal Id:  0.7.1.4
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.5
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.6
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired(red, black)) /\ True = shuffle(black, $8:NeList, $9:NeList) → True = shuffle(nil, red $8:NeList, $9:NeList)
Goal Id:  0.7.1.7
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.8
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(black, $8:NeList, $9:NeList)) /\ True = paired(black, black) → False = shuffle(nil, red $8:NeList, $9:NeList)
Goal Id:  0.7.1.9
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired(black, black)) /\ True = paired(red, black) → False = shuffle(nil, red $8:NeList, $9:NeList)
Goal Id:  0.7.2.1
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.10
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.11
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.12
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired(black, red)) /\ True = shuffle(red, $8:NeList, $9:NeList) → True = shuffle(nil, black $8:NeList, $9:NeList)
Goal Id:  0.7.2.2
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(red, $8:NeList, $9:NeList)) /\ True = paired(red, red) → False = shuffle(nil, black $8:NeList, $9:NeList)
Goal Id:  0.7.2.3
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired(black, red)) /\ True = paired(red, red) → False = shuffle(nil, black $8:NeList, $9:NeList)
Goal Id:  0.7.2.4
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.5
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.6
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired(black, red)) /\ True = shuffle(red, $8:NeList, $9:NeList) → True = shuffle(nil, black $8:NeList, $9:NeList)
Goal Id:  0.7.2.7
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.8
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(red, $8:NeList, $9:NeList)) /\ True = paired(red, red) → False = shuffle(nil, black $8:NeList, $9:NeList)
Goal Id:  0.7.2.9
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired(black, red)) /\ True = paired(red, red) → False = shuffle(nil, black $8:NeList, $9:NeList)
Goal Id:  0.8.1.1
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.1.2
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(black $9:NeList, $10:NeList, $11:NeList)) /\ True = paired(black, black) → False = shuffle($9:NeList, red $10:NeList, $11:NeList)
Goal Id:  0.8.1.3
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired(black, black)) /\ True = paired(red, black) → False = shuffle($9:NeList, red $10:NeList, $11:NeList)
Goal Id:  0.8.1.4
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.1.5
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.1.6
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired(red, black)) /\ True = shuffle(black $9:NeList, $10:NeList, $11:NeList) → True = shuffle($9:NeList, red $10:NeList, $11:NeList)
Goal Id:  0.8.2.1
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.2.2
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = shuffle(red $9:NeList, $10:NeList, $11:NeList)) /\ True = paired(red, red) → False = shuffle($9:NeList, black $10:NeList, $11:NeList)
Goal Id:  0.8.2.3
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = paired(black, red)) /\ True = paired(red, red) → False = shuffle($9:NeList, black $10:NeList, $11:NeList)
Goal Id:  0.8.2.4
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.2.5
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.2.6
Generated By:  NI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(False = paired(black, red)) /\ True = shuffle(red $9:NeList, $10:NeList, $11:NeList) → True = shuffle($9:NeList, black $10:NeList, $11:NeList)
Goal Id:  0.3.1.1.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.1.4.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.2.1.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.2.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.2.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.3.2.4.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.12.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.6.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.8.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.1.9.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.12.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.6.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.8.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.5.2.9.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.12.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.6.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.8.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.1.9.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.12.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.6.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.8.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.7.2.9.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.1.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.1.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.1.6.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.2.2.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.2.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.8.2.6.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true

Proof Tree