Gary is big. Gary is not cold. Gary is furry. Gary is green. Gary is red. Gary is round. Gary is white. If someone is red and not furry then they are cold. All white, round people are green. If Gary is not green and Gary is not round then Gary is big.
Gary is big.
("Gary" "is" "big" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is red and not furry then they are cold.
((("someone" "is" "red" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "cold" "+"))
All white, round people are green.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If Gary is not green and Gary is not round then Gary is big.
((("Gary" "is" "green" "~") ("Gary" "is" "round" "~")) -> ("Gary" "is" "big" "+"))
Gary is green.
True
1
proof
[(triple4 OR ((triple7 triple6) -> rule2))]
("Gary" "is" "green" "+")
triple4
((triple7 triple6) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not red.
False
1
inv-proof
[(triple5)]
("Gary" "is" "red" "-")
triple5
@0: Gary is big.[(triple1)] Gary is furry.[(triple3)] Gary is green.[(triple4 OR ((triple7 triple6) -> rule2))] Gary is not cold.[(triple2)] Gary is red.[(triple5)] Gary is round.[(triple6)] Gary is white.[(triple7)]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Gary is green.
("Gary" "is" "green" "+")
triple4
((triple7 triple6) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not cold.
("Gary" "is" "cold" "-")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is round.
("Gary" "is" "round" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7