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