Gary is blue. Gary is furry. Gary is green. Gary is quiet. Gary is red. Gary is rough. Gary is white. Harry is blue. Harry is furry. Harry is green. Harry is quiet. Harry is red. Harry is rough. Harry is white. If Harry is green and Harry is red then Harry is blue. Rough, green things are quiet.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is green and Harry is red then Harry is blue.
((("Harry" "is" "green" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "blue" "+"))
Rough, green things are quiet.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
Harry is white.
True
1
proof
[(triple14)]
("Harry" "is" "white" "+")
triple14
Harry is not red.
False
1
inv-proof
[(triple12)]
("Harry" "is" "red" "-")
triple12
@0: Gary is blue.[(triple1)] Gary is furry.[(triple2)] Gary is green.[(triple3)] Gary is quiet.[(triple4 OR ((triple6 triple3) -> rule2))] Gary is red.[(triple5)] Gary is rough.[(triple6)] Gary is white.[(triple7)] Harry is blue.[(triple8 OR ((triple10 triple12) -> rule1))] Harry is furry.[(triple9)] Harry is green.[(triple10)] Harry is quiet.[(triple11 OR ((triple13 triple10) -> rule2))] Harry is red.[(triple12)] Harry is rough.[(triple13)] Harry is white.[(triple14)]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple4
((triple6 triple3) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
((triple10 triple12) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
((triple13 triple10) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is rough.
("Harry" "is" "rough" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14