Dave is kind. Dave is quiet. Erin is blue. Erin is cold. Erin is green. Erin is kind. Erin is quiet. If someone is kind then they are blue. If Dave is blue then Dave is red. If someone is quiet then they are white. If Erin is green and Erin is quiet then Erin is red. If Dave is red and Dave is kind then Dave is quiet. All blue people are quiet. If Erin is white then Erin is quiet. If Dave is white and Dave is red then Dave is green.
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If someone is kind then they are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If Dave is blue then Dave is red.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "red" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If Erin is green and Erin is quiet then Erin is red.
((("Erin" "is" "green" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "red" "+"))
If Dave is red and Dave is kind then Dave is quiet.
((("Dave" "is" "red" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "quiet" "+"))
All blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is white then Erin is quiet.
((("Erin" "is" "white" "+")) -> ("Erin" "is" "quiet" "+"))
If Dave is white and Dave is red then Dave is green.
((("Dave" "is" "white" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "green" "+"))
Erin is quiet.
True
1
proof
[(triple7 OR ((triple3) -> rule6) OR ((((triple6) -> rule1)) -> rule6))]
("Erin" "is" "quiet" "+")
triple7
((triple3) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not blue.
False
1
inv-proof
[(triple3 OR ((triple6) -> rule1))]
("Erin" "is" "blue" "-")
triple3
((triple6) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
@0: Dave is kind.[(triple1)] Dave is quiet.[(triple2 OR ((((triple1) -> rule1)) -> rule6) OR ((((((triple1) -> rule1)) -> rule2) triple1) -> rule5))] Erin is blue.[(triple3 OR ((triple6) -> rule1))] Erin is cold.[(triple4)] Erin is green.[(triple5)] Erin is kind.[(triple6)] Erin is quiet.[(triple7 OR ((triple3) -> rule6) OR ((((triple6) -> rule1)) -> rule6))] @1: Dave is blue.[(((triple1) -> rule1))] Dave is white.[(((triple2) -> rule3) OR ((((((triple1) -> rule1)) -> rule6)) -> rule3) OR ((((((((triple1) -> rule1)) -> rule2) triple1) -> rule5)) -> rule3))] Erin is red.[(((triple5 triple7) -> rule4) OR ((triple5 ((triple3) -> rule6)) -> rule4) OR ((triple5 ((((triple6) -> rule1)) -> rule6)) -> rule4))] Erin is white.[(((triple7) -> rule3) OR ((((triple3) -> rule6)) -> rule3) OR ((((((triple6) -> rule1)) -> rule6)) -> rule3))] @2: Dave is red.[(((((triple1) -> rule1)) -> rule2))] @3: Dave is green.[(((((triple2) -> rule3) ((((triple1) -> rule1)) -> rule2)) -> rule8) OR ((((((((triple1) -> rule1)) -> rule6)) -> rule3) ((((triple1) -> rule1)) -> rule2)) -> rule8) OR ((((((((((triple1) -> rule1)) -> rule2) triple1) -> rule5)) -> rule3) ((((triple1) -> rule1)) -> rule2)) -> rule8))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
triple3
((triple6) -> (rule1 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple4
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
((triple3) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((((triple1) -> (rule1 % int4))) -> (rule2 % int3)) triple1) -> (rule5 % int2))) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
((triple5 triple7) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple5 ((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple5 ((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((triple7) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((((triple6) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
((((triple2) -> (rule3 % int4)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((((((triple1) -> (rule1 % int5))) -> (rule6 % int4))) -> (rule3 % int3)) ((((triple1) -> (rule1 % int5))) -> (rule2 % int2))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is quiet.
("Dave" "is" "quiet" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
((((((((((triple1) -> (rule1 % int5))) -> (rule2 % int4)) triple1) -> (rule5 % int3))) -> (rule3 % int2)) ((((triple1) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5