Harry is big. Harry is blue. Harry is cold. Harry is furry. Harry is quiet. Harry is red. Harry is smart. If something is big then it is red. All quiet, red things are big. Big things are blue.
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All quiet, red things are big.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Harry is blue.
True
1
proof
[(triple2 OR ((triple1) -> rule3) OR ((((triple5 triple6) -> rule2)) -> rule3))]
("Harry" "is" "blue" "+")
triple2
((triple1) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple5 triple6) -> (rule2 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not cold.
False
1
inv-proof
[(triple3)]
("Harry" "is" "cold" "-")
triple3
@0: Harry is big.[(triple1 OR ((triple5 triple6) -> rule2))] Harry is blue.[(triple2 OR ((triple1) -> rule3) OR ((((triple5 triple6) -> rule2)) -> rule3))] Harry is cold.[(triple3)] Harry is furry.[(triple4)] Harry is quiet.[(triple5)] Harry is red.[(triple6 OR ((triple1) -> rule1))] Harry is smart.[(triple7)]
Harry is big.
("Harry" "is" "big" "+")
triple1
((triple5 triple6) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
((triple1) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple5 triple6) -> (rule2 % int2))) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
((triple1) -> (rule1 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
triple7