Charlie is blue. Charlie is cold. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is rough. Harry is cold. Harry is nice. Harry is rough. Quiet, rough people are blue. If someone is cold then they are quiet. If Harry is furry and Harry is kind then Harry is blue. If Charlie is furry and Charlie is quiet then Charlie is blue. If someone is cold then they are quiet. If someone is quiet then they are nice. Kind, rough people are furry. All blue people are furry.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Quiet, rough people are blue.
((("someone" "is" "quiet" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If Harry is furry and Harry is kind then Harry is blue.
((("Harry" "is" "furry" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "blue" "+"))
If Charlie is furry and Charlie is quiet then Charlie is blue.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "blue" "+"))
If someone is cold then they are quiet.
((("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
If someone is quiet then they are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Kind, rough people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
All blue people are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Harry is rough.
True
1
proof
[(triple10)]
("Harry" "is" "rough" "+")
triple10
Charlie is not quiet.
False
1
inv-proof
[(triple6 OR ((triple2) -> rule2) OR ((triple2) -> rule5))]
("Charlie" "is" "quiet" "-")
triple6
((triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple2) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Harry is quiet.
True
2
proof
[(((triple8) -> rule2) OR ((triple8) -> rule5))]
("Harry" "is" "quiet" "+")
((triple8) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple8) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple8) -> rule2) OR ((triple8) -> rule5))]
("Harry" "is" "quiet" "-")
((triple8) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple8) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
True
4
proof
[(((((triple8) -> rule2) triple10) -> rule1) OR ((((triple8) -> rule5) triple10) -> rule1))]
("Harry" "is" "blue" "+")
((((triple8) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple8) -> (rule5 % int2)) triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((((triple8) -> rule2) triple10) -> rule1) OR ((((triple8) -> rule5) triple10) -> rule1))]
("Harry" "is" "blue" "-")
((((triple8) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple8) -> (rule5 % int2)) triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
True
5
proof
[(((((((triple8) -> rule2) triple10) -> rule1)) -> rule8) OR ((((((triple8) -> rule5) triple10) -> rule1)) -> rule8))]
("Harry" "is" "furry" "+")
((((((triple8) -> (rule2 % int3)) triple10) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple8) -> (rule5 % int3)) triple10) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not furry.
False
5
inv-proof
[(((((((triple8) -> rule2) triple10) -> rule1)) -> rule8) OR ((((((triple8) -> rule5) triple10) -> rule1)) -> rule8))]
("Harry" "is" "furry" "-")
((((((triple8) -> (rule2 % int3)) triple10) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple8) -> (rule5 % int3)) triple10) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
@0: Charlie is blue.[(triple1 OR ((triple3 triple6) -> rule4) OR ((triple6 triple7) -> rule1) OR ((triple3 ((triple2) -> rule2)) -> rule4) OR ((triple3 ((triple2) -> rule5)) -> rule4) OR ((((triple2) -> rule2) triple7) -> rule1) OR ((((triple2) -> rule5) triple7) -> rule1) OR ((((triple4 triple7) -> rule7) triple6) -> rule4) OR ((((triple4 triple7) -> rule7) ((triple2) -> rule2)) -> rule4) OR ((((triple4 triple7) -> rule7) ((triple2) -> rule5)) -> rule4))] Charlie is cold.[(triple2)] Charlie is furry.[(triple3 OR ((triple1) -> rule8) OR ((triple4 triple7) -> rule7) OR ((((triple6 triple7) -> rule1)) -> rule8) OR ((((((triple2) -> rule2) triple7) -> rule1)) -> rule8) OR ((((((triple2) -> rule5) triple7) -> rule1)) -> rule8))] Charlie is kind.[(triple4)] Charlie is nice.[(triple5 OR ((triple6) -> rule6) OR ((((triple2) -> rule2)) -> rule6) OR ((((triple2) -> rule5)) -> rule6))] Charlie is quiet.[(triple6 OR ((triple2) -> rule2) OR ((triple2) -> rule5))] Charlie is rough.[(triple7)] Harry is cold.[(triple8)] Harry is nice.[(triple9 OR ((((triple8) -> rule2)) -> rule6) OR ((((triple8) -> rule5)) -> rule6))] Harry is rough.[(triple10)] @1: Harry is quiet.[(((triple8) -> rule2) OR ((triple8) -> rule5))] @2: Harry is blue.[(((((triple8) -> rule2) triple10) -> rule1) OR ((((triple8) -> rule5) triple10) -> rule1))] @3: Harry is furry.[(((((((triple8) -> rule2) triple10) -> rule1)) -> rule8) OR ((((((triple8) -> rule5) triple10) -> rule1)) -> rule8))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple3 triple6) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple6 triple7) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple3 ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((triple3 ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple2) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple2) -> (rule5 % int2)) triple7) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple4 triple7) -> (rule7 % int2)) triple6) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple4 triple7) -> (rule7 % int3)) ((triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((triple4 triple7) -> (rule7 % int3)) ((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((triple1) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple4 triple7) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple6 triple7) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((((triple2) -> (rule2 % int3)) triple7) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple2) -> (rule5 % int3)) triple7) -> (rule1 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
((triple6) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
((triple2) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((triple2) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Harry is cold.
("Harry" "is" "cold" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
((((triple8) -> (rule2 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple8) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple8) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple8) -> (rule2 % int2)) triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple8) -> (rule5 % int2)) triple10) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple8) -> (rule2 % int3)) triple10) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple8) -> (rule5 % int3)) triple10) -> (rule1 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3