NuITP (alpha 30) ProofProved


Goal

(True = alter($2:List $1:Card $3:List $1:Card $4:List)) /\ True = even($3:List) → false

Script

set goal ((alter(L1:List C:Card L2:List C:Card L3:List) = True) /\ (even(L2:List) = True)) → false .
apply gnd! to 0 .
apply gsi! to 0.1 on $2 with GLISTL .
apply cas! to 0.1.4 on $5 .
apply cas! to 0.1.5 on $5 .
apply gsi! to 0.2 on $2 with GLISTL .
apply cas! to 0.2.4 on $5 .
apply cas! to 0.2.5 on $5 .
apply gsi! to 0.2.2 on $4 with GLISTL .

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 = alter($2:List $1:Card $3:List $1:Card $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1
Generated By:  GND
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter($2:List black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2
Generated By:  GND
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter($2:List red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.1
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(black black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.2
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.3
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(red black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.4
Generated By:  GSI
Skolem Ops:
$5.NeList
Executable Hypotheses:
None
Non-Executable Hypotheses:
(True = alter($5 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black $5 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.5
Generated By:  GSI
Skolem Ops:
$5.NeList
Executable Hypotheses:
None
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
(True = alter($5 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red $5 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.1
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(black red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.2
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.3
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(red red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.4
Generated By:  GSI
Skolem Ops:
$5.NeList
Executable Hypotheses:
None
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
(True = alter($5 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black $5 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.5
Generated By:  GSI
Skolem Ops:
$5.NeList
Executable Hypotheses:
None
Non-Executable Hypotheses:
(True = alter($5 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red $5 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.1.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.2.1
Generated By:  CS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.4.1
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
None
Goal:
(True = alter(black black black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.4.2
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black red black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.4.3
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
Non-Executable Hypotheses:
(True = alter(black $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black black $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.4.4
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
Non-Executable Hypotheses:
(True = alter(red $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black red $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.5.1
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red black black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.5.2
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red red black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.5.3
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
(True = alter(black $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red black $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.5.4
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
(True = alter(red $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red red $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.1.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.2.1
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(red $3:List red black)) /\ True = even($3:List) → false
Goal Id:  0.2.2.2
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(red $3:List red)) /\ True = even($3:List) → false
Goal Id:  0.2.2.3
Generated By:  GSI
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(red $3:List red red)) /\ True = even($3:List) → false
Goal Id:  0.2.2.4
Generated By:  GSI
Skolem Ops:
$5.NeList
Executable Hypotheses:
None
Non-Executable Hypotheses:
(True = alter(red $3:List red)) /\ True = even($3:List) → false
(True = alter(red $3:List red $5)) /\ True = even($3:List) → false
Goal:
(True = alter(red $3:List red black $5)) /\ True = even($3:List) → false
Goal Id:  0.2.2.5
Generated By:  GSI
Skolem Ops:
$5.NeList
Executable Hypotheses:
None
Non-Executable Hypotheses:
(True = alter(red $3:List red $5)) /\ True = even($3:List) → false
Goal:
(True = alter(red $3:List red red $5)) /\ True = even($3:List) → false
Goal Id:  0.2.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.4.1
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black black red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.4.2
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black red red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.4.3
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
(True = alter(black $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black black $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.4.4
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
(True = alter(red $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black red $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.5.1
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red black red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.5.2
Generated By:  CAS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
None
Goal:
(True = alter(red red red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.5.3
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
Non-Executable Hypotheses:
(True = alter(black $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red black $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.5.4
Generated By:  CAS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
Non-Executable Hypotheses:
(True = alter(red $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red red $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.3.1.1
Generated By:  CS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.4.1.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.1.4.2.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.4.3.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
Non-Executable Hypotheses:
(True = alter(black $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.1.4.4.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
Non-Executable Hypotheses:
(True = alter(red $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.5.1.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.1.5.2.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.1.5.3.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
(True = alter(black $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal Id:  0.1.5.4.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
(True = alter(red $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.2.1.1.1
Generated By:  CS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.2.1.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
(True = alter(red $3:List red)) /\ True = even($3:List) → false
Goal Id:  0.2.2.2.1
Generated By:  CS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.2.3.1
Generated By:  EPS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.2.4.1
Generated By:  CS
Skolem Ops:
$5.NeList
Executable Hypotheses:
None
Non-Executable Hypotheses:
(True = alter(red $3:List red)) /\ True = even($3:List) → false
(True = alter(red $3:List red $5)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.2.2.5.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
None
Non-Executable Hypotheses:
(True = alter(red $3:List red $5)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.2.4.1.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.2.4.2.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.2.4.3.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
(True = alter(black $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.2.4.4.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
(True = alter(red $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.5.1.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.5.2.1
Generated By:  EPS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.5.3.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
Non-Executable Hypotheses:
(True = alter(black $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
(True = alter(black $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal Id:  0.2.5.4.1
Generated By:  EPS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
Non-Executable Hypotheses:
(True = alter(red $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.1.4.2.1.1
Generated By:  CS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ red
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.1.4.4.1.1
Generated By:  CS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
Non-Executable Hypotheses:
(True = alter(red $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.1.5.3.1.1
Generated By:  CS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
Non-Executable Hypotheses:
(True = alter(black $3:List black $4:List)) /\ True = even($3:List) → false
(True = alter(black $6 black $3:List black $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.2.2.1.1.1
Generated By:  CS
Skolem Ops:
None
Executable Hypotheses:
None
Non-Executable Hypotheses:
None
Goal:
true
Goal Id:  0.2.4.4.1.1
Generated By:  CS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ red $6
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
(True = alter(red $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.2.5.1.1.1
Generated By:  CS
Skolem Ops:
$5.NeList
Executable Hypotheses:
$5 ⇒ black
Non-Executable Hypotheses:
(True = alter(red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
true
Goal Id:  0.2.5.3.1.1
Generated By:  CS
Skolem Ops:
$5.NeList
$6.NeList
Executable Hypotheses:
$5 ⇒ black $6
Non-Executable Hypotheses:
(True = alter(black $6 red $3:List red $4:List)) /\ True = even($3:List) → false
Goal:
true

Proof Tree