Erin is big. Erin is blue. Erin is cold. Erin is nice. Erin is quiet. Erin is white. Erin is young. All cold, quiet people are nice. If Erin is nice then Erin is big. If someone is quiet and nice then they are blue. If Erin is big and Erin is quiet then Erin is white. If someone is young and quiet then they are blue. Big people are cold. Cold people are nice. All quiet, white people are cold.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
All cold, quiet people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
If Erin is nice then Erin is big.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "big" "+"))
If someone is quiet and nice then they are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If Erin is big and Erin is quiet then Erin is white.
((("Erin" "is" "big" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "white" "+"))
If someone is young and quiet then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
Cold people are nice.
((("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
All quiet, white people are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Erin is white.
True
1
proof
[(triple6 OR ((triple1 triple5) -> rule4) OR ((((triple4) -> rule2) triple5) -> rule4) OR ((((((triple3) -> rule7)) -> rule2) triple5) -> rule4) OR ((((((triple3 triple5) -> rule1)) -> rule2) triple5) -> rule4))]
("Erin" "is" "white" "+")
triple6
((triple1 triple5) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple4) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
((((((triple3 triple5) -> (rule1 % int3))) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is not young.
False
1
inv-proof
[(triple7)]
("Erin" "is" "young" "-")
triple7
@0: Erin is big.[(triple1 OR ((triple4) -> rule2) OR ((((triple3) -> rule7)) -> rule2) OR ((((triple3 triple5) -> rule1)) -> rule2) OR ((((((triple5 triple6) -> rule8)) -> rule7)) -> rule2) OR ((((((triple5 triple6) -> rule8) triple5) -> rule1)) -> rule2))] Erin is blue.[(triple2 OR ((triple5 triple4) -> rule3) OR ((triple7 triple5) -> rule5) OR ((triple5 ((triple3) -> rule7)) -> rule3) OR ((triple5 ((triple3 triple5) -> rule1)) -> rule3) OR ((triple5 ((((triple1) -> rule6)) -> rule7)) -> rule3) OR ((triple5 ((((triple5 triple6) -> rule8)) -> rule7)) -> rule3) OR ((triple5 ((((triple1) -> rule6) triple5) -> rule1)) -> rule3) OR ((triple5 ((((triple5 triple6) -> rule8) triple5) -> rule1)) -> rule3) OR ((triple5 ((((triple5 ((triple1 triple5) -> rule4)) -> rule8)) -> rule7)) -> rule3) OR ((triple5 ((((triple5 ((triple1 triple5) -> rule4)) -> rule8) triple5) -> rule1)) -> rule3))] Erin is cold.[(triple3 OR ((triple1) -> rule6) OR ((triple5 triple6) -> rule8) OR ((((triple4) -> rule2)) -> rule6) OR ((triple5 ((triple1 triple5) -> rule4)) -> rule8) OR ((triple5 ((((triple4) -> rule2) triple5) -> rule4)) -> rule8))] Erin is nice.[(triple4 OR ((triple3) -> rule7) OR ((triple3 triple5) -> rule1) OR ((((triple1) -> rule6)) -> rule7) OR ((((triple5 triple6) -> rule8)) -> rule7) OR ((((triple1) -> rule6) triple5) -> rule1) OR ((((triple5 triple6) -> rule8) triple5) -> rule1) OR ((((triple5 ((triple1 triple5) -> rule4)) -> rule8)) -> rule7) OR ((((triple5 ((triple1 triple5) -> rule4)) -> rule8) triple5) -> rule1))] Erin is quiet.[(triple5)] Erin is white.[(triple6 OR ((triple1 triple5) -> rule4) OR ((((triple4) -> rule2) triple5) -> rule4) OR ((((((triple3) -> rule7)) -> rule2) triple5) -> rule4) OR ((((((triple3 triple5) -> rule1)) -> rule2) triple5) -> rule4))] Erin is young.[(triple7)]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple4) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((triple3 triple5) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((((triple5 triple6) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple5 triple6) -> (rule8 % int3)) triple5) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
triple2
((triple5 triple4) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple7 triple5) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple5 ((triple3) -> (rule7 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple5 ((triple3 triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((triple5 ((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((triple5 ((((triple5 triple6) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((triple5 ((((triple1) -> (rule6 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((triple5 ((((triple5 triple6) -> (rule8 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((triple5 ((((triple5 ((triple1 triple5) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
((triple5 ((((triple5 ((triple1 triple5) -> (rule4 % int4))) -> (rule8 % int3)) triple5) -> (rule1 % int2))) -> (rule3 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
triple3
((triple1) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((triple5 triple6) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((triple5 ((triple1 triple5) -> (rule4 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((triple5 ((((triple4) -> (rule2 % int3)) triple5) -> (rule4 % int2))) -> (rule8 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
((triple3) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((triple3 triple5) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple5 triple6) -> (rule8 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple1) -> (rule6 % int2)) triple5) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple5 triple6) -> (rule8 % int2)) triple5) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple5 ((triple1 triple5) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((triple5 ((triple1 triple5) -> (rule4 % int3))) -> (rule8 % int2)) triple5) -> (rule1 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
((triple1 triple5) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple4) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
((((((triple3 triple5) -> (rule1 % int3))) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple7