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