Harry is cold. Harry is furry. Harry is kind. Harry is quiet. Harry is red. Harry is round. Harry is white. Red things are furry. If something is furry and not quiet then it is white.
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
If something is furry and not quiet then it is white.
((("something" "is" "furry" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "white" "+"))
Harry is furry.
True
1
proof
[(triple2 OR ((triple5) -> rule1))]
("Harry" "is" "furry" "+")
triple2
((triple5) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not red.
False
1
inv-proof
[(triple5)]
("Harry" "is" "red" "-")
triple5
@0: Harry is cold.[(triple1)] Harry is furry.[(triple2 OR ((triple5) -> rule1))] Harry is kind.[(triple3)] Harry is quiet.[(triple4)] Harry is red.[(triple5)] Harry is round.[(triple6)] Harry is white.[(triple7)]
Harry is cold.
("Harry" "is" "cold" "+")
triple1
Harry is furry.
("Harry" "is" "furry" "+")
triple2
((triple5) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Harry is red.
("Harry" "is" "red" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7