Anne is blue. Anne is furry. Anne is quiet. Anne is round. Anne is smart. Anne is white. Anne is young. Dave is quiet. Dave is smart. Dave is young. Harry is blue. Harry is quiet. Harry is round. Harry is smart. Harry is white. Harry is young. If someone is young then they are white. If someone is blue then they are furry. Smart, quiet people are young. All white, smart people are blue. If Anne is young then Anne is white. If someone is round then they are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is young then they are white.
((("someone" "is" "young" "+")) -> ("someone" "is" "white" "+"))
If someone is blue then they are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Smart, quiet people are young.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
All white, smart people are blue.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If Anne is young then Anne is white.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "white" "+"))
If someone is round then they are blue.
((("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
Dave is quiet.
True
1
proof
[(triple8)]
("Dave" "is" "quiet" "+")
triple8
Anne is not round.
False
1
inv-proof
[(triple4)]
("Anne" "is" "round" "-")
triple4
Harry is furry.
True
2
proof
[(((triple11) -> rule2) OR ((((triple13) -> rule6)) -> rule2) OR ((((triple15 triple14) -> rule4)) -> rule2) OR ((((((triple16) -> rule1) triple14) -> rule4)) -> rule2) OR ((((((((triple14 triple12) -> rule3)) -> rule1) triple14) -> rule4)) -> rule2))]
("Harry" "is" "furry" "+")
((triple11) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple15 triple14) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((((triple16) -> (rule1 % int3)) triple14) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((((triple14 triple12) -> (rule3 % int4))) -> (rule1 % int3)) triple14) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Dave is not white.
False
2
inv-proof
[(((triple10) -> rule1) OR ((((triple9 triple8) -> rule3)) -> rule1))]
("Dave" "is" "white" "-")
((triple10) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple9 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is blue.
True
4
proof
[(((((triple10) -> rule1) triple9) -> rule4) OR ((((((triple9 triple8) -> rule3)) -> rule1) triple9) -> rule4))]
("Dave" "is" "blue" "+")
((((triple10) -> (rule1 % int2)) triple9) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple9 triple8) -> (rule3 % int3))) -> (rule1 % int2)) triple9) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is not blue.
False
4
inv-proof
[(((((triple10) -> rule1) triple9) -> rule4) OR ((((((triple9 triple8) -> rule3)) -> rule1) triple9) -> rule4))]
("Dave" "is" "blue" "-")
((((triple10) -> (rule1 % int2)) triple9) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple9 triple8) -> (rule3 % int3))) -> (rule1 % int2)) triple9) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is furry.
True
5
proof
[(((((((triple10) -> rule1) triple9) -> rule4)) -> rule2) OR ((((((((triple9 triple8) -> rule3)) -> rule1) triple9) -> rule4)) -> rule2))]
("Dave" "is" "furry" "+")
((((((triple10) -> (rule1 % int3)) triple9) -> (rule4 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((((triple9 triple8) -> (rule3 % int4))) -> (rule1 % int3)) triple9) -> (rule4 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
Dave is not furry.
False
5
inv-proof
[(((((((triple10) -> rule1) triple9) -> rule4)) -> rule2) OR ((((((((triple9 triple8) -> rule3)) -> rule1) triple9) -> rule4)) -> rule2))]
("Dave" "is" "furry" "-")
((((((triple10) -> (rule1 % int3)) triple9) -> (rule4 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((((triple9 triple8) -> (rule3 % int4))) -> (rule1 % int3)) triple9) -> (rule4 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4
@0: Anne is blue.[(triple1 OR ((triple4) -> rule6) OR ((triple6 triple5) -> rule4) OR ((((triple7) -> rule1) triple5) -> rule4) OR ((((triple7) -> rule5) triple5) -> rule4) OR ((((((triple5 triple3) -> rule3)) -> rule1) triple5) -> rule4) OR ((((((triple5 triple3) -> rule3)) -> rule5) triple5) -> rule4))] Anne is furry.[(triple2 OR ((triple1) -> rule2) OR ((((triple4) -> rule6)) -> rule2) OR ((((triple6 triple5) -> rule4)) -> rule2) OR ((((((triple7) -> rule1) triple5) -> rule4)) -> rule2) OR ((((((triple7) -> rule5) triple5) -> rule4)) -> rule2) OR ((((((((triple5 triple3) -> rule3)) -> rule1) triple5) -> rule4)) -> rule2) OR ((((((((triple5 triple3) -> rule3)) -> rule5) triple5) -> rule4)) -> rule2))] Anne is quiet.[(triple3)] Anne is round.[(triple4)] Anne is smart.[(triple5)] Anne is white.[(triple6 OR ((triple7) -> rule1) OR ((triple7) -> rule5) OR ((((triple5 triple3) -> rule3)) -> rule1) OR ((((triple5 triple3) -> rule3)) -> rule5))] Anne is young.[(triple7 OR ((triple5 triple3) -> rule3))] Dave is quiet.[(triple8)] Dave is smart.[(triple9)] Dave is young.[(triple10 OR ((triple9 triple8) -> rule3))] Harry is blue.[(triple11 OR ((triple13) -> rule6) OR ((triple15 triple14) -> rule4) OR ((((triple16) -> rule1) triple14) -> rule4) OR ((((((triple14 triple12) -> rule3)) -> rule1) triple14) -> rule4))] Harry is quiet.[(triple12)] Harry is round.[(triple13)] Harry is smart.[(triple14)] Harry is white.[(triple15 OR ((triple16) -> rule1) OR ((((triple14 triple12) -> rule3)) -> rule1))] Harry is young.[(triple16 OR ((triple14 triple12) -> rule3))] @1: Dave is white.[(((triple10) -> rule1) OR ((((triple9 triple8) -> rule3)) -> rule1))] Harry is furry.[(((triple11) -> rule2) OR ((((triple13) -> rule6)) -> rule2) OR ((((triple15 triple14) -> rule4)) -> rule2) OR ((((((triple16) -> rule1) triple14) -> rule4)) -> rule2) OR ((((((((triple14 triple12) -> rule3)) -> rule1) triple14) -> rule4)) -> rule2))] @2: Dave is blue.[(((((triple10) -> rule1) triple9) -> rule4) OR ((((((triple9 triple8) -> rule3)) -> rule1) triple9) -> rule4))] @3: Dave is furry.[(((((((triple10) -> rule1) triple9) -> rule4)) -> rule2) OR ((((((((triple9 triple8) -> rule3)) -> rule1) triple9) -> rule4)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple4) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple6 triple5) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple7) -> (rule1 % int2)) triple5) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((triple7) -> (rule5 % int2)) triple5) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
((((((triple5 triple3) -> (rule3 % int3))) -> (rule1 % int2)) triple5) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((((triple5 triple3) -> (rule3 % int3))) -> (rule5 % int2)) triple5) -> (rule4 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple6 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple7) -> (rule1 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((triple7) -> (rule5 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
((((((((triple5 triple3) -> (rule3 % int4))) -> (rule1 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
((((((((triple5 triple3) -> (rule3 % int4))) -> (rule5 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple7) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple7) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((triple5 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple5 triple3) -> (rule3 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple5 triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
((triple9 triple8) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple11
((triple13) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple15 triple14) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple16) -> (rule1 % int2)) triple14) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((((triple14 triple12) -> (rule3 % int3))) -> (rule1 % int2)) triple14) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple16) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple14 triple12) -> (rule3 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple14 triple12) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple10) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple9 triple8) -> (rule3 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple11) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple13) -> (rule6 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple15 triple14) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((((triple16) -> (rule1 % int3)) triple14) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((((((triple14 triple12) -> (rule3 % int4))) -> (rule1 % int3)) triple14) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
((((triple10) -> (rule1 % int2)) triple9) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple9 triple8) -> (rule3 % int3))) -> (rule1 % int2)) triple9) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((((((triple10) -> (rule1 % int3)) triple9) -> (rule4 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((((((triple9 triple8) -> (rule3 % int4))) -> (rule1 % int3)) triple9) -> (rule4 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
int4