Gary is blue. Gary is green. Gary is quiet. Gary is red. Gary is rough. Gary is round. Gary is white. If Gary is quiet and Gary is white then Gary is blue.
Gary is blue.
("Gary" "is" "blue" "+")
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 round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If Gary is quiet and Gary is white then Gary is blue.
((("Gary" "is" "quiet" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "blue" "+"))
Gary is blue.
True
1
proof
[(triple1 OR ((triple3 triple7) -> rule1))]
("Gary" "is" "blue" "+")
triple1
((triple3 triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not white.
False
1
inv-proof
[(triple7)]
("Gary" "is" "white" "-")
triple7
@0: Gary is blue.[(triple1 OR ((triple3 triple7) -> rule1))] Gary is green.[(triple2)] Gary is quiet.[(triple3)] Gary is red.[(triple4)] Gary is rough.[(triple5)] Gary is round.[(triple6)] Gary is white.[(triple7)]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
((triple3 triple7) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7