Harry is big. Harry is cold. Harry is furry. Harry is nice. Harry is quiet. Harry is red. Harry is smart. If someone is furry and big then they are cold. All quiet people are big.
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is furry and big then they are cold.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Harry is nice.
True
1
proof
[(triple4)]
("Harry" "is" "nice" "+")
triple4
Harry is not smart.
False
1
inv-proof
[(triple7)]
("Harry" "is" "smart" "-")
triple7
@0: Harry is big.[(triple1 OR ((triple5) -> rule2))] Harry is cold.[(triple2 OR ((triple3 triple1) -> rule1) OR ((triple3 ((triple5) -> rule2)) -> rule1))] Harry is furry.[(triple3)] Harry is nice.[(triple4)] Harry is quiet.[(triple5)] Harry is red.[(triple6)] Harry is smart.[(triple7)]
Harry is big.
("Harry" "is" "big" "+")
triple1
((triple5) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
((triple3 triple1) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple3 ((triple5) -> (rule2 % int2))) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7