Harry is blue. Harry is cold. Harry is furry. Harry is nice. Harry is red. Harry is rough. Harry is young. All young things are furry. If Harry is rough and Harry is furry then Harry is young. Furry things are rough. Blue, nice things are red. Red things are furry. If something is young and furry then it is red. If Harry is red then Harry is young. All red things are blue.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
All young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If Harry is rough and Harry is furry then Harry is young.
((("Harry" "is" "rough" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "young" "+"))
Furry things are rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Blue, nice things are red.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is young and furry then it is red.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If Harry is red then Harry is young.
((("Harry" "is" "red" "+")) -> ("Harry" "is" "young" "+"))
All red things are blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
Harry is cold.
True
1
proof
[(triple2)]
("Harry" "is" "cold" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple2)]
("Harry" "is" "cold" "-")
triple2
@0: Harry is blue.[(triple1 OR ((triple5) -> rule8) OR ((((triple7 triple3) -> rule6)) -> rule8) OR ((((triple7 ((triple7) -> rule1)) -> rule6)) -> rule8) OR ((((((triple6 triple3) -> rule2) triple3) -> rule6)) -> rule8) OR ((((((triple6 triple3) -> rule2) ((triple7) -> rule1)) -> rule6)) -> rule8) OR ((((((((triple3) -> rule3) triple3) -> rule2) triple3) -> rule6)) -> rule8) OR ((((((((triple3) -> rule3) triple3) -> rule2) ((triple7) -> rule1)) -> rule6)) -> rule8))] Harry is cold.[(triple2)] Harry is furry.[(triple3 OR ((triple5) -> rule5) OR ((triple7) -> rule1) OR ((((triple5) -> rule7)) -> rule1) OR ((((triple1 triple4) -> rule4)) -> rule5) OR ((((((triple1 triple4) -> rule4)) -> rule7)) -> rule1))] Harry is nice.[(triple4)] Harry is red.[(triple5 OR ((triple1 triple4) -> rule4) OR ((triple7 triple3) -> rule6) OR ((triple7 ((triple7) -> rule1)) -> rule6) OR ((((triple6 triple3) -> rule2) triple3) -> rule6) OR ((((triple6 triple3) -> rule2) ((triple7) -> rule1)) -> rule6) OR ((((((triple3) -> rule3) triple3) -> rule2) triple3) -> rule6) OR ((((((triple3) -> rule3) triple3) -> rule2) ((triple7) -> rule1)) -> rule6))] Harry is rough.[(triple6 OR ((triple3) -> rule3) OR ((((triple5) -> rule5)) -> rule3) OR ((((triple7) -> rule1)) -> rule3) OR ((((((triple5) -> rule7)) -> rule1)) -> rule3) OR ((((((triple1 triple4) -> rule4)) -> rule5)) -> rule3) OR ((((((((triple1 triple4) -> rule4)) -> rule7)) -> rule1)) -> rule3))] Harry is young.[(triple7 OR ((triple5) -> rule7) OR ((triple6 triple3) -> rule2) OR ((((triple1 triple4) -> rule4)) -> rule7) OR ((triple6 ((triple5) -> rule5)) -> rule2) OR ((((triple3) -> rule3) triple3) -> rule2) OR ((((triple3) -> rule3) ((triple5) -> rule5)) -> rule2) OR ((triple6 ((((triple1 triple4) -> rule4)) -> rule5)) -> rule2) OR ((((((triple5) -> rule5)) -> rule3) triple3) -> rule2) OR ((((triple3) -> rule3) ((((triple1 triple4) -> rule4)) -> rule5)) -> rule2) OR ((((((triple5) -> rule5)) -> rule3) ((triple5) -> rule5)) -> rule2) OR ((((((triple5) -> rule5)) -> rule3) ((((triple1 triple4) -> rule4)) -> rule5)) -> rule2) OR ((((((((triple1 triple4) -> rule4)) -> rule5)) -> rule3) triple3) -> rule2) OR ((((((((triple1 triple4) -> rule4)) -> rule5)) -> rule3) ((triple5) -> rule5)) -> rule2) OR ((((((((triple1 triple4) -> rule4)) -> rule5)) -> rule3) ((((triple1 triple4) -> rule4)) -> rule5)) -> rule2))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
((triple5) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple7 triple3) -> (rule6 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple7 ((triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple6 triple3) -> (rule2 % int3)) triple3) -> (rule6 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple6 triple3) -> (rule2 % int4)) ((triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
((((((((triple3) -> (rule3 % int4)) triple3) -> (rule2 % int3)) triple3) -> (rule6 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
((((((((triple3) -> (rule3 % int5)) triple3) -> (rule2 % int4)) ((triple7) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
int5
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
((triple5) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple7) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple5) -> (rule7 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple1 triple4) -> (rule4 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((((triple1 triple4) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Harry is red.
("Harry" "is" "red" "+")
triple5
((triple1 triple4) -> (rule4 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple7 triple3) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple7 ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple6 triple3) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple6 triple3) -> (rule2 % int3)) ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple3) -> (rule3 % int3)) triple3) -> (rule2 % int2)) triple3) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((((((triple3) -> (rule3 % int4)) triple3) -> (rule2 % int3)) ((triple7) -> (rule1 % int2))) -> (rule6 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is rough.
("Harry" "is" "rough" "+")
triple6
((triple3) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple5) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
((((((triple1 triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((((((triple1 triple4) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is young.
("Harry" "is" "young" "+")
triple7
((triple5) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple6 triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple1 triple4) -> (rule4 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((triple6 ((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((triple3) -> (rule3 % int3)) ((triple5) -> (rule5 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
((triple6 ((((triple1 triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((triple3) -> (rule3 % int4)) ((((triple1 triple4) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
((((((triple5) -> (rule5 % int3))) -> (rule3 % int2)) ((triple5) -> (rule5 % int3))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((triple5) -> (rule5 % int4))) -> (rule3 % int3)) ((((triple1 triple4) -> (rule4 % int2))) -> (rule5 % int4))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
((((((((triple1 triple4) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
((((((((triple1 triple4) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((triple5) -> (rule5 % int3))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
((((((((triple1 triple4) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule3 % int2)) ((((triple1 triple4) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4