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