Anne is big. Anne is cold. Anne is furry. Anne is green. Anne is nice. Anne is quiet. Anne is smart. Harry is furry. Harry is nice. Harry is smart. If something is green and smart then it is cold. All nice, cold things are quiet. If something is nice then it is green. Green, cold things are furry. If Harry is big and Harry is smart then Harry is cold. If something is big and nice then it is furry.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is green and smart then it is cold.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All nice, cold things are quiet.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Green, cold things are furry.
((("something" "is" "green" "+") ("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
If Harry is big and Harry is smart then Harry is cold.
((("Harry" "is" "big" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "cold" "+"))
If something is big and nice then it is furry.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Anne is furry.
True
1
proof
[(triple3 OR ((triple1 triple5) -> rule6) OR ((triple4 triple2) -> rule4) OR ((triple4 ((triple4 triple7) -> rule1)) -> rule4) OR ((((triple5) -> rule3) triple2) -> rule4) OR ((((triple5) -> rule3) ((triple4 triple7) -> rule1)) -> rule4) OR ((triple4 ((((triple5) -> rule3) triple7) -> rule1)) -> rule4) OR ((((triple5) -> rule3) ((((triple5) -> rule3) triple7) -> rule1)) -> rule4))]
("Anne" "is" "furry" "+")
triple3
((triple1 triple5) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple4 triple2) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple4 ((triple4 triple7) -> (rule1 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple5) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple5) -> (rule3 % int3)) ((triple4 triple7) -> (rule1 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((triple4 ((((triple5) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((triple5) -> (rule3 % int3)) ((((triple5) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Harry is not nice.
False
1
inv-proof
[(triple9)]
("Harry" "is" "nice" "-")
triple9
Harry is green.
True
2
proof
[(((triple9) -> rule3))]
("Harry" "is" "green" "+")
((triple9) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple9) -> rule3))]
("Harry" "is" "green" "-")
((triple9) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
True
4
proof
[(((((triple9) -> rule3) triple10) -> rule1))]
("Harry" "is" "cold" "+")
((((triple9) -> (rule3 % int2)) triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not cold.
False
4
inv-proof
[(((((triple9) -> rule3) triple10) -> rule1))]
("Harry" "is" "cold" "-")
((((triple9) -> (rule3 % int2)) triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
True
6
proof
[(((triple9 ((((triple9) -> rule3) triple10) -> rule1)) -> rule2))]
("Harry" "is" "quiet" "+")
((triple9 ((((triple9) -> (rule3 % int3)) triple10) -> (rule1 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is not quiet.
False
6
inv-proof
[(((triple9 ((((triple9) -> rule3) triple10) -> rule1)) -> rule2))]
("Harry" "is" "quiet" "-")
((triple9 ((((triple9) -> (rule3 % int3)) triple10) -> (rule1 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
@0: Anne is big.[(triple1)] Anne is cold.[(triple2 OR ((triple4 triple7) -> rule1) OR ((((triple5) -> rule3) triple7) -> rule1))] Anne is furry.[(triple3 OR ((triple1 triple5) -> rule6) OR ((triple4 triple2) -> rule4) OR ((triple4 ((triple4 triple7) -> rule1)) -> rule4) OR ((((triple5) -> rule3) triple2) -> rule4) OR ((((triple5) -> rule3) ((triple4 triple7) -> rule1)) -> rule4) OR ((triple4 ((((triple5) -> rule3) triple7) -> rule1)) -> rule4) OR ((((triple5) -> rule3) ((((triple5) -> rule3) triple7) -> rule1)) -> rule4))] Anne is green.[(triple4 OR ((triple5) -> rule3))] Anne is nice.[(triple5)] Anne is quiet.[(triple6 OR ((triple5 triple2) -> rule2) OR ((triple5 ((triple4 triple7) -> rule1)) -> rule2) OR ((triple5 ((((triple5) -> rule3) triple7) -> rule1)) -> rule2))] Anne is smart.[(triple7)] Harry is furry.[(triple8 OR ((((triple9) -> rule3) ((((triple9) -> rule3) triple10) -> rule1)) -> rule4))] Harry is nice.[(triple9)] Harry is smart.[(triple10)] @1: Harry is green.[(((triple9) -> rule3))] @2: Harry is cold.[(((((triple9) -> rule3) triple10) -> rule1))] @3: Harry is quiet.[(((triple9 ((((triple9) -> rule3) triple10) -> rule1)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((triple4 triple7) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple5) -> (rule3 % int2)) triple7) -> (rule1 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple1 triple5) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple4 triple2) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple4 ((triple4 triple7) -> (rule1 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple5) -> (rule3 % int2)) triple2) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((triple5) -> (rule3 % int3)) ((triple4 triple7) -> (rule1 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((triple4 ((((triple5) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
((((triple5) -> (rule3 % int3)) ((((triple5) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is green.
("Anne" "is" "green" "+")
triple4
((triple5) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple5
Anne is quiet.
("Anne" "is" "quiet" "+")
triple6
((triple5 triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple5 ((triple4 triple7) -> (rule1 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple5 ((((triple5) -> (rule3 % int3)) triple7) -> (rule1 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
triple8
((((triple9) -> (rule3 % int3)) ((((triple9) -> (rule3 % int3)) triple10) -> (rule1 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Harry is green.
("Harry" "is" "green" "+")
((triple9) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple9) -> (rule3 % int2)) triple10) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple9 ((((triple9) -> (rule3 % int3)) triple10) -> (rule1 % int2))) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3