Harry is big. Harry is cold. Harry is furry. Harry is quiet. Harry is rough. Harry is round. Harry is smart. Cold, round people are furry.
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Cold, round people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
Harry is furry.
True
1
proof
[(triple3 OR ((triple2 triple6) -> rule1))]
("Harry" "is" "furry" "+")
triple3
((triple2 triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not smart.
False
1
inv-proof
[(triple7)]
("Harry" "is" "smart" "-")
triple7
@0: Harry is big.[(triple1)] Harry is cold.[(triple2)] Harry is furry.[(triple3 OR ((triple2 triple6) -> rule1))] Harry is quiet.[(triple4)] Harry is rough.[(triple5)] Harry is round.[(triple6)] Harry is smart.[(triple7)]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
((triple2 triple6) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Harry is rough.
("Harry" "is" "rough" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7