Harry is blue. Harry is green. Harry is smart. Green, smart things are cold. All smart, quiet things are furry. If Harry is cold then Harry is furry. If something is young then it is quiet. Blue things are smart. All furry, blue things are young. If something is quiet and furry then it is green. If something is green and smart then it is furry.
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Green, smart things are cold.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All smart, quiet things are furry.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If Harry is cold then Harry is furry.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "furry" "+"))
If something is young then it is quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
All furry, blue things are young.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is quiet and furry then it is green.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is green and smart then it is furry.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Harry is blue.
True
1
proof
[(triple1)]
("Harry" "is" "blue" "+")
triple1
Harry is not green.
False
1
inv-proof
[(triple2)]
("Harry" "is" "green" "-")
triple2
Harry is furry.
True
3
proof
[(((triple2 triple3) -> rule8) OR ((((triple2 triple3) -> rule1)) -> rule3) OR ((triple2 ((triple1) -> rule5)) -> rule8) OR ((((triple2 ((triple1) -> rule5)) -> rule1)) -> rule3))]
("Harry" "is" "furry" "+")
((triple2 triple3) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple2 ((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not furry.
False
3
inv-proof
[(((triple2 triple3) -> rule8) OR ((((triple2 triple3) -> rule1)) -> rule3) OR ((triple2 ((triple1) -> rule5)) -> rule8) OR ((((triple2 ((triple1) -> rule5)) -> rule1)) -> rule3))]
("Harry" "is" "furry" "-")
((triple2 triple3) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple2 ((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is young.
True
5
proof
[(((((triple2 triple3) -> rule8) triple1) -> rule6) OR ((((((triple2 triple3) -> rule1)) -> rule3) triple1) -> rule6) OR ((((triple2 ((triple1) -> rule5)) -> rule8) triple1) -> rule6) OR ((((((triple2 ((triple1) -> rule5)) -> rule1)) -> rule3) triple1) -> rule6))]
("Harry" "is" "young" "+")
((((triple2 triple3) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple2 triple3) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple2 ((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is not young.
False
5
inv-proof
[(((((triple2 triple3) -> rule8) triple1) -> rule6) OR ((((((triple2 triple3) -> rule1)) -> rule3) triple1) -> rule6) OR ((((triple2 ((triple1) -> rule5)) -> rule8) triple1) -> rule6) OR ((((((triple2 ((triple1) -> rule5)) -> rule1)) -> rule3) triple1) -> rule6))]
("Harry" "is" "young" "-")
((((triple2 triple3) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple2 triple3) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple2 ((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is quiet.
True
6
proof
[(((((((triple2 triple3) -> rule8) triple1) -> rule6)) -> rule4) OR ((((((((triple2 triple3) -> rule1)) -> rule3) triple1) -> rule6)) -> rule4) OR ((((((triple2 ((triple1) -> rule5)) -> rule8) triple1) -> rule6)) -> rule4) OR ((((((((triple2 ((triple1) -> rule5)) -> rule1)) -> rule3) triple1) -> rule6)) -> rule4))]
("Harry" "is" "quiet" "+")
((((((triple2 triple3) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((((triple2 triple3) -> (rule1 % int4))) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
((((((triple2 ((triple1) -> (rule5 % int4))) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((((((triple2 ((triple1) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
int5
Harry is not quiet.
False
6
inv-proof
[(((((((triple2 triple3) -> rule8) triple1) -> rule6)) -> rule4) OR ((((((((triple2 triple3) -> rule1)) -> rule3) triple1) -> rule6)) -> rule4) OR ((((((triple2 ((triple1) -> rule5)) -> rule8) triple1) -> rule6)) -> rule4) OR ((((((((triple2 ((triple1) -> rule5)) -> rule1)) -> rule3) triple1) -> rule6)) -> rule4))]
("Harry" "is" "quiet" "-")
((((((triple2 triple3) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((((triple2 triple3) -> (rule1 % int4))) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
((((((triple2 ((triple1) -> (rule5 % int4))) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((((((triple2 ((triple1) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
int5
@0: Harry is blue.[(triple1)] Harry is green.[(triple2)] Harry is smart.[(triple3 OR ((triple1) -> rule5))] @1: Harry is cold.[(((triple2 triple3) -> rule1) OR ((triple2 ((triple1) -> rule5)) -> rule1))] Harry is furry.[(((triple2 triple3) -> rule8) OR ((((triple2 triple3) -> rule1)) -> rule3) OR ((triple2 ((triple1) -> rule5)) -> rule8) OR ((((triple2 ((triple1) -> rule5)) -> rule1)) -> rule3))] @2: Harry is young.[(((((triple2 triple3) -> rule8) triple1) -> rule6) OR ((((((triple2 triple3) -> rule1)) -> rule3) triple1) -> rule6) OR ((((triple2 ((triple1) -> rule5)) -> rule8) triple1) -> rule6) OR ((((((triple2 ((triple1) -> rule5)) -> rule1)) -> rule3) triple1) -> rule6))] @3: Harry is quiet.[(((((((triple2 triple3) -> rule8) triple1) -> rule6)) -> rule4) OR ((((((((triple2 triple3) -> rule1)) -> rule3) triple1) -> rule6)) -> rule4) OR ((((((triple2 ((triple1) -> rule5)) -> rule8) triple1) -> rule6)) -> rule4) OR ((((((((triple2 ((triple1) -> rule5)) -> rule1)) -> rule3) triple1) -> rule6)) -> rule4))]
Harry is blue.
("Harry" "is" "blue" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
((triple1) -> (rule5 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple2 triple3) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple2 ((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple2 triple3) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple2 triple3) -> (rule1 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
((triple2 ((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((((triple2 triple3) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple2 triple3) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
((((triple2 ((triple1) -> (rule5 % int3))) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((((triple2 ((triple1) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((triple2 triple3) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
((((((((triple2 triple3) -> (rule1 % int4))) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
((((((triple2 ((triple1) -> (rule5 % int4))) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((((((triple2 ((triple1) -> (rule5 % int5))) -> (rule1 % int4))) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
int5