Erin is blue. Erin is cold. Erin is green. Erin is quiet. Erin is red. Erin is rough. Erin is white. Harry is blue. Harry is cold. Harry is green. Harry is quiet. Harry is red. Harry is rough. Harry is white. Green, white things are red. If something is cold and white then it is blue. If Erin is rough then Erin is white. All cold, rough things are blue. Blue things are white. Green things are cold.
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 red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Green, white things are red.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is cold and white then it is blue.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
If Erin is rough then Erin is white.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "white" "+"))
All cold, rough things are blue.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Erin is white.
True
1
proof
[(triple7 OR ((triple1) -> rule5) OR ((triple6) -> rule3) OR ((((triple2 triple6) -> rule4)) -> rule5) OR ((((((triple3) -> rule6) triple6) -> rule4)) -> rule5))]
("Erin" "is" "white" "+")
triple7
((triple1) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple6) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple2 triple6) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((((triple3) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is not red.
False
1
inv-proof
[(triple5 OR ((triple3 triple7) -> rule1) OR ((triple3 ((triple1) -> rule5)) -> rule1) OR ((triple3 ((triple6) -> rule3)) -> rule1) OR ((triple3 ((((triple2 triple6) -> rule4)) -> rule5)) -> rule1) OR ((triple3 ((((((triple3) -> rule6) triple6) -> rule4)) -> rule5)) -> rule1))]
("Erin" "is" "red" "-")
triple5
((triple3 triple7) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple3 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple3 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple3 ((((triple2 triple6) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((triple3 ((((((triple3) -> (rule6 % int4)) triple6) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
@0: Erin is blue.[(triple1 OR ((triple2 triple6) -> rule4) OR ((triple2 triple7) -> rule2) OR ((triple2 ((triple6) -> rule3)) -> rule2) OR ((((triple3) -> rule6) triple6) -> rule4) OR ((((triple3) -> rule6) triple7) -> rule2) OR ((((triple3) -> rule6) ((triple6) -> rule3)) -> rule2))] Erin is cold.[(triple2 OR ((triple3) -> rule6))] Erin is green.[(triple3)] Erin is quiet.[(triple4)] Erin is red.[(triple5 OR ((triple3 triple7) -> rule1) OR ((triple3 ((triple1) -> rule5)) -> rule1) OR ((triple3 ((triple6) -> rule3)) -> rule1) OR ((triple3 ((((triple2 triple6) -> rule4)) -> rule5)) -> rule1) OR ((triple3 ((((((triple3) -> rule6) triple6) -> rule4)) -> rule5)) -> rule1))] Erin is rough.[(triple6)] Erin is white.[(triple7 OR ((triple1) -> rule5) OR ((triple6) -> rule3) OR ((((triple2 triple6) -> rule4)) -> rule5) OR ((((((triple3) -> rule6) triple6) -> rule4)) -> rule5))] Harry is blue.[(triple8 OR ((triple9 triple13) -> rule4) OR ((triple9 triple14) -> rule2) OR ((((triple10) -> rule6) triple13) -> rule4) OR ((((triple10) -> rule6) triple14) -> rule2))] Harry is cold.[(triple9 OR ((triple10) -> rule6))] Harry is green.[(triple10)] Harry is quiet.[(triple11)] Harry is red.[(triple12 OR ((triple10 triple14) -> rule1) OR ((triple10 ((triple8) -> rule5)) -> rule1) OR ((triple10 ((((triple9 triple13) -> rule4)) -> rule5)) -> rule1) OR ((triple10 ((((((triple10) -> rule6) triple13) -> rule4)) -> rule5)) -> rule1))] Harry is rough.[(triple13)] Harry is white.[(triple14 OR ((triple8) -> rule5) OR ((((triple9 triple13) -> rule4)) -> rule5) OR ((((((triple10) -> rule6) triple13) -> rule4)) -> rule5))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple2 triple6) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple2 triple7) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple2 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple3) -> (rule6 % int2)) triple6) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple3) -> (rule6 % int2)) triple7) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple3) -> (rule6 % int3)) ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple3) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
((triple3 triple7) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple3 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple3 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple3 ((((triple2 triple6) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((triple3 ((((((triple3) -> (rule6 % int4)) triple6) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
((triple1) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple6) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple2 triple6) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
((((((triple3) -> (rule6 % int3)) triple6) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
triple8
((triple9 triple13) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple9 triple14) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple10) -> (rule6 % int2)) triple13) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((((triple10) -> (rule6 % int2)) triple14) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple9
((triple10) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
((triple10 triple14) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple10 ((triple8) -> (rule5 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple10 ((((triple9 triple13) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
((triple10 ((((((triple10) -> (rule6 % int4)) triple13) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14
((triple8) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple9 triple13) -> (rule4 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((((triple10) -> (rule6 % int3)) triple13) -> (rule4 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3