Dave is big. Dave is furry. Dave is red. Dave is rough. Dave is smart. Erin is big. Erin is blue. Erin is furry. Erin is red. Erin is rough. Erin is smart. Erin is young. If someone is red then they are furry. Red people are blue. All blue people are young. Blue, red people are big. Big, young people are furry. If Dave is young then Dave is blue.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
If someone is red then they are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
Blue, red people are big.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Big, young people are furry.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If Dave is young then Dave is blue.
((("Dave" "is" "young" "+")) -> ("Dave" "is" "blue" "+"))
Erin is furry.
True
1
proof
[(triple8 OR ((triple9) -> rule1) OR ((triple6 triple12) -> rule5) OR ((triple6 ((triple7) -> rule3)) -> rule5) OR ((((triple7 triple9) -> rule4) triple12) -> rule5) OR ((((triple7 triple9) -> rule4) ((triple7) -> rule3)) -> rule5) OR ((triple6 ((((triple9) -> rule2)) -> rule3)) -> rule5) OR ((((((triple9) -> rule2) triple9) -> rule4) triple12) -> rule5) OR ((((triple7 triple9) -> rule4) ((((triple9) -> rule2)) -> rule3)) -> rule5) OR ((((((triple9) -> rule2) triple9) -> rule4) ((triple7) -> rule3)) -> rule5) OR ((((((triple9) -> rule2) triple9) -> rule4) ((((triple9) -> rule2)) -> rule3)) -> rule5))]
("Erin" "is" "furry" "+")
triple8
((triple9) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple6 triple12) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple6 ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple7 triple9) -> (rule4 % int2)) triple12) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple7 triple9) -> (rule4 % int3)) ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((triple6 ((((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple9) -> (rule2 % int3)) triple9) -> (rule4 % int2)) triple12) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((triple7 triple9) -> (rule4 % int4)) ((((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
((((((triple9) -> (rule2 % int4)) triple9) -> (rule4 % int3)) ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
((((((triple9) -> (rule2 % int4)) triple9) -> (rule4 % int3)) ((((triple9) -> (rule2 % int4))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is not red.
False
1
inv-proof
[(triple9)]
("Erin" "is" "red" "-")
triple9
Dave is blue.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Dave" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not young.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Dave" "is" "young" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
@0: Dave is big.[(triple1 OR ((((triple3) -> rule2) triple3) -> rule4))] Dave is furry.[(triple2 OR ((triple3) -> rule1) OR ((triple1 ((((triple3) -> rule2)) -> rule3)) -> rule5) OR ((((((triple3) -> rule2) triple3) -> rule4) ((((triple3) -> rule2)) -> rule3)) -> rule5))] Dave is red.[(triple3)] Dave is rough.[(triple4)] Dave is smart.[(triple5)] Erin is big.[(triple6 OR ((triple7 triple9) -> rule4) OR ((((triple9) -> rule2) triple9) -> rule4))] Erin is blue.[(triple7 OR ((triple9) -> rule2))] Erin is furry.[(triple8 OR ((triple9) -> rule1) OR ((triple6 triple12) -> rule5) OR ((triple6 ((triple7) -> rule3)) -> rule5) OR ((((triple7 triple9) -> rule4) triple12) -> rule5) OR ((((triple7 triple9) -> rule4) ((triple7) -> rule3)) -> rule5) OR ((triple6 ((((triple9) -> rule2)) -> rule3)) -> rule5) OR ((((((triple9) -> rule2) triple9) -> rule4) triple12) -> rule5) OR ((((triple7 triple9) -> rule4) ((((triple9) -> rule2)) -> rule3)) -> rule5) OR ((((((triple9) -> rule2) triple9) -> rule4) ((triple7) -> rule3)) -> rule5) OR ((((((triple9) -> rule2) triple9) -> rule4) ((((triple9) -> rule2)) -> rule3)) -> rule5))] Erin is red.[(triple9)] Erin is rough.[(triple10)] Erin is smart.[(triple11)] Erin is young.[(triple12 OR ((triple7) -> rule3) OR ((((triple9) -> rule2)) -> rule3))] @1: Dave is blue.[(((triple3) -> rule2))] @2: Dave is young.[(((((triple3) -> rule2)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
((((triple3) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple3) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple1 ((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
((((((triple3) -> (rule2 % int4)) triple3) -> (rule4 % int3)) ((((triple3) -> (rule2 % int4))) -> (rule3 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Erin is big.
("Erin" "is" "big" "+")
triple6
((triple7 triple9) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple9) -> (rule2 % int2)) triple9) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
triple7
((triple9) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple8
((triple9) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple6 triple12) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple6 ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple7 triple9) -> (rule4 % int2)) triple12) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple7 triple9) -> (rule4 % int3)) ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
((triple6 ((((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((((triple9) -> (rule2 % int3)) triple9) -> (rule4 % int2)) triple12) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
((((triple7 triple9) -> (rule4 % int4)) ((((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
int4
((((((triple9) -> (rule2 % int4)) triple9) -> (rule4 % int3)) ((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
((((((triple9) -> (rule2 % int4)) triple9) -> (rule4 % int3)) ((((triple9) -> (rule2 % int4))) -> (rule3 % int2))) -> (rule5 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
int4
Erin is red.
("Erin" "is" "red" "+")
triple9
Erin is rough.
("Erin" "is" "rough" "+")
triple10
Erin is smart.
("Erin" "is" "smart" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple7) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2