Bob is big. Bob is blue. Bob is furry. Bob is quiet. Bob is red. Bob is smart. Bob is white. Charlie is big. Charlie is furry. Charlie is red. Charlie is smart. Charlie is white. If Charlie is big then Charlie is red. If Charlie is quiet and Charlie is big then Charlie is smart. Furry, smart people are red. If Charlie is furry then Charlie is big. If someone is blue and furry then they are quiet. If someone is red then they are blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If Charlie is big then Charlie is red.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "red" "+"))
If Charlie is quiet and Charlie is big then Charlie is smart.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "smart" "+"))
Furry, smart people are red.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If Charlie is furry then Charlie is big.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "big" "+"))
If someone is blue and furry then they are quiet.
((("someone" "is" "blue" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is red then they are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Charlie is not red.
False
1
inv-proof
[(triple10 OR ((triple8) -> rule1) OR ((triple9 triple11) -> rule3) OR ((((triple9) -> rule4)) -> rule1))]
("Charlie" "is" "red" "-")
triple10
((triple8) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple9 triple11) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is blue.
True
2
proof
[(((triple10) -> rule6) OR ((((triple8) -> rule1)) -> rule6) OR ((((triple9 triple11) -> rule3)) -> rule6) OR ((((((triple9) -> rule4)) -> rule1)) -> rule6))]
("Charlie" "is" "blue" "+")
((triple10) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple9 triple11) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((((triple9) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not blue.
False
2
inv-proof
[(((triple10) -> rule6) OR ((((triple8) -> rule1)) -> rule6) OR ((((triple9 triple11) -> rule3)) -> rule6) OR ((((((triple9) -> rule4)) -> rule1)) -> rule6))]
("Charlie" "is" "blue" "-")
((triple10) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple9 triple11) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((((triple9) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is quiet.
True
4
proof
[(((((triple10) -> rule6) triple9) -> rule5) OR ((((((triple8) -> rule1)) -> rule6) triple9) -> rule5) OR ((((((triple9 triple11) -> rule3)) -> rule6) triple9) -> rule5) OR ((((((((triple9) -> rule4)) -> rule1)) -> rule6) triple9) -> rule5))]
("Charlie" "is" "quiet" "+")
((((triple10) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((triple9 triple11) -> (rule3 % int3))) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((((triple9) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
Charlie is not quiet.
False
4
inv-proof
[(((((triple10) -> rule6) triple9) -> rule5) OR ((((((triple8) -> rule1)) -> rule6) triple9) -> rule5) OR ((((((triple9 triple11) -> rule3)) -> rule6) triple9) -> rule5) OR ((((((((triple9) -> rule4)) -> rule1)) -> rule6) triple9) -> rule5))]
("Charlie" "is" "quiet" "-")
((((triple10) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((triple9 triple11) -> (rule3 % int3))) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((((triple9) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4
@0: Bob is big.[(triple1)] Bob is blue.[(triple2 OR ((triple5) -> rule6) OR ((((triple3 triple6) -> rule3)) -> rule6))] Bob is furry.[(triple3)] Bob is quiet.[(triple4 OR ((triple2 triple3) -> rule5) OR ((((triple5) -> rule6) triple3) -> rule5) OR ((((((triple3 triple6) -> rule3)) -> rule6) triple3) -> rule5))] Bob is red.[(triple5 OR ((triple3 triple6) -> rule3))] Bob is smart.[(triple6)] Bob is white.[(triple7)] Charlie is big.[(triple8 OR ((triple9) -> rule4))] Charlie is furry.[(triple9)] Charlie is red.[(triple10 OR ((triple8) -> rule1) OR ((triple9 triple11) -> rule3) OR ((((triple9) -> rule4)) -> rule1))] Charlie is smart.[(triple11 OR ((((((triple10) -> rule6) triple9) -> rule5) triple8) -> rule2) OR ((((((triple10) -> rule6) triple9) -> rule5) ((triple9) -> rule4)) -> rule2) OR ((((((((triple8) -> rule1)) -> rule6) triple9) -> rule5) triple8) -> rule2) OR ((((((((triple8) -> rule1)) -> rule6) triple9) -> rule5) ((triple9) -> rule4)) -> rule2) OR ((((((((((triple9) -> rule4)) -> rule1)) -> rule6) triple9) -> rule5) triple8) -> rule2) OR ((((((((((triple9) -> rule4)) -> rule1)) -> rule6) triple9) -> rule5) ((triple9) -> rule4)) -> rule2))] Charlie is white.[(triple12)] @1: Charlie is blue.[(((triple10) -> rule6) OR ((((triple8) -> rule1)) -> rule6) OR ((((triple9 triple11) -> rule3)) -> rule6) OR ((((((triple9) -> rule4)) -> rule1)) -> rule6))] @2: Charlie is quiet.[(((((triple10) -> rule6) triple9) -> rule5) OR ((((((triple8) -> rule1)) -> rule6) triple9) -> rule5) OR ((((((triple9 triple11) -> rule3)) -> rule6) triple9) -> rule5) OR ((((((((triple9) -> rule4)) -> rule1)) -> rule6) triple9) -> rule5))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple5) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple3 triple6) -> (rule3 % int2))) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
((triple2 triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((((triple5) -> (rule6 % int2)) triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((((triple3 triple6) -> (rule3 % int3))) -> (rule6 % int2)) triple3) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is red.
("Bob" "is" "red" "+")
triple5
((triple3 triple6) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Bob is white.
("Bob" "is" "white" "+")
triple7
Charlie is big.
("Charlie" "is" "big" "+")
triple8
((triple9) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple9
Charlie is red.
("Charlie" "is" "red" "+")
triple10
((triple8) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple9 triple11) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((((triple9) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
((((((triple10) -> (rule6 % int3)) triple9) -> (rule5 % int2)) triple8) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
((((((triple10) -> (rule6 % int4)) triple9) -> (rule5 % int3)) ((triple9) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
((((((((triple8) -> (rule1 % int4))) -> (rule6 % int3)) triple9) -> (rule5 % int2)) triple8) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
((((((((triple8) -> (rule1 % int5))) -> (rule6 % int4)) triple9) -> (rule5 % int3)) ((triple9) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
int5
((((((((((triple9) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule6 % int3)) triple9) -> (rule5 % int2)) triple8) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
int5
((((((((((triple9) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule6 % int3)) triple9) -> (rule5 % int2)) ((triple9) -> (rule4 % int5))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is big.
("Charlie" "is" "big" "+")
int5
Charlie is white.
("Charlie" "is" "white" "+")
triple12
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple10) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple8) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((triple9 triple11) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
((((((triple9) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple10) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple8) -> (rule1 % int3))) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((triple9 triple11) -> (rule3 % int3))) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
((((((((triple9) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule6 % int2)) triple9) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4