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