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