Charlie is cold. Charlie is green. Charlie is round. Charlie is smart. Charlie is white. Erin is blue. Erin is cold. Erin is green. Erin is quiet. Erin is round. Erin is smart. Erin is white. All quiet, smart people are blue. If someone is white and round then they are quiet. If someone is smart and white then they are quiet. If someone is white then they are smart. If someone is cold then they are quiet. If someone is cold and quiet then they are green.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
All quiet, smart people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is white and round then they are quiet.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If someone is smart and white then they are quiet.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white then they are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold and quiet then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Erin is smart.
True
1
proof
[(triple11 OR ((triple12) -> rule4))]
("Erin" "is" "smart" "+")
triple11
((triple12) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Charlie is not white.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "white" "-")
triple5
@0: Charlie is cold.[(triple1)] Charlie is green.[(triple2 OR ((triple1 ((triple1) -> rule5)) -> rule6) OR ((triple1 ((triple4 triple5) -> rule3)) -> rule6) OR ((triple1 ((triple5 triple3) -> rule2)) -> rule6) OR ((triple1 ((((triple5) -> rule4) triple5) -> rule3)) -> rule6))] Charlie is round.[(triple3)] Charlie is smart.[(triple4 OR ((triple5) -> rule4))] Charlie is white.[(triple5)] Erin is blue.[(triple6 OR ((triple9 triple11) -> rule1) OR ((triple9 ((triple12) -> rule4)) -> rule1) OR ((((triple7) -> rule5) triple11) -> rule1) OR ((((triple11 triple12) -> rule3) triple11) -> rule1) OR ((((triple12 triple10) -> rule2) triple11) -> rule1) OR ((((triple7) -> rule5) ((triple12) -> rule4)) -> rule1) OR ((((triple11 triple12) -> rule3) ((triple12) -> rule4)) -> rule1) OR ((((triple12 triple10) -> rule2) ((triple12) -> rule4)) -> rule1) OR ((((((triple12) -> rule4) triple12) -> rule3) triple11) -> rule1) OR ((((((triple12) -> rule4) triple12) -> rule3) ((triple12) -> rule4)) -> rule1))] Erin is cold.[(triple7)] Erin is green.[(triple8 OR ((triple7 triple9) -> rule6) OR ((triple7 ((triple7) -> rule5)) -> rule6) OR ((triple7 ((triple11 triple12) -> rule3)) -> rule6) OR ((triple7 ((triple12 triple10) -> rule2)) -> rule6) OR ((triple7 ((((triple12) -> rule4) triple12) -> rule3)) -> rule6))] Erin is quiet.[(triple9 OR ((triple7) -> rule5) OR ((triple11 triple12) -> rule3) OR ((triple12 triple10) -> rule2) OR ((((triple12) -> rule4) triple12) -> rule3))] Erin is round.[(triple10)] Erin is smart.[(triple11 OR ((triple12) -> rule4))] Erin is white.[(triple12)] @1: Charlie is quiet.[(((triple1) -> rule5) OR ((triple4 triple5) -> rule3) OR ((triple5 triple3) -> rule2) OR ((((triple5) -> rule4) triple5) -> rule3))] @2: Charlie is blue.[(((((triple1) -> rule5) triple4) -> rule1) OR ((((triple4 triple5) -> rule3) triple4) -> rule1) OR ((((triple5 triple3) -> rule2) triple4) -> rule1) OR ((((triple1) -> rule5) ((triple5) -> rule4)) -> rule1) OR ((((triple4 triple5) -> rule3) ((triple5) -> rule4)) -> rule1) OR ((((triple5 triple3) -> rule2) ((triple5) -> rule4)) -> rule1) OR ((((((triple5) -> rule4) triple5) -> rule3) triple4) -> rule1) OR ((((((triple5) -> rule4) triple5) -> rule3) ((triple5) -> rule4)) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((triple1 ((triple4 triple5) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((triple1 ((triple5 triple3) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((triple1 ((((triple5) -> (rule4 % int3)) triple5) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
((triple5) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
((triple9 triple11) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple9 ((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple7) -> (rule5 % int2)) triple11) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple11 triple12) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple12 triple10) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple7) -> (rule5 % int3)) ((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple11 triple12) -> (rule3 % int3)) ((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((triple12 triple10) -> (rule2 % int3)) ((triple12) -> (rule4 % int2))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
((((((triple12) -> (rule4 % int3)) triple12) -> (rule3 % int2)) triple11) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((((triple12) -> (rule4 % int3)) triple12) -> (rule3 % int2)) ((triple12) -> (rule4 % int3))) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
((triple7 triple9) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple7 ((triple7) -> (rule5 % int2))) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple7 ((triple11 triple12) -> (rule3 % int2))) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple7 ((triple12 triple10) -> (rule2 % int2))) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple7 ((((triple12) -> (rule4 % int3)) triple12) -> (rule3 % int2))) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((triple7) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple11 triple12) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple12 triple10) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple12) -> (rule4 % int2)) triple12) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
((triple12) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple12
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple4 triple5) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple5 triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple5) -> (rule4 % int2)) triple5) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1) -> (rule5 % int2)) triple4) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple4 triple5) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple5 triple3) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple1) -> (rule5 % int3)) ((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple4 triple5) -> (rule3 % int3)) ((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((triple5 triple3) -> (rule2 % int3)) ((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple5) -> (rule4 % int3)) triple5) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple5) -> (rule4 % int3)) triple5) -> (rule3 % int2)) ((triple5) -> (rule4 % int3))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3