Harry is furry. Harry is green. Harry is kind. Harry is nice. Harry is red. Harry is round. Harry is white. If Harry is nice and Harry is white then Harry is round.
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is nice and Harry is white then Harry is round.
((("Harry" "is" "nice" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "round" "+"))
Harry is kind.
True
1
proof
[(triple3)]
("Harry" "is" "kind" "+")
triple3
Harry is not furry.
False
1
inv-proof
[(triple1)]
("Harry" "is" "furry" "-")
triple1
@0: Harry is furry.[(triple1)] Harry is green.[(triple2)] Harry is kind.[(triple3)] Harry is nice.[(triple4)] Harry is red.[(triple5)] Harry is round.[(triple6 OR ((triple4 triple7) -> rule1))] Harry is white.[(triple7)]
Harry is furry.
("Harry" "is" "furry" "+")
triple1
Harry is green.
("Harry" "is" "green" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Harry is red.
("Harry" "is" "red" "+")
triple5
Harry is round.
("Harry" "is" "round" "+")
triple6
((triple4 triple7) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple7