Gary is big. Gary is cold. Gary is green. Gary is kind. Gary is quiet. Gary is red. Gary is rough. Red, quiet things are kind. All big things are green.
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Red, quiet things are kind.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
Gary is red.
True
1
proof
[(triple6)]
("Gary" "is" "red" "+")
triple6
Gary is not red.
False
1
inv-proof
[(triple6)]
("Gary" "is" "red" "-")
triple6
@0: Gary is big.[(triple1)] Gary is cold.[(triple2)] Gary is green.[(triple3 OR ((triple1) -> rule2))] Gary is kind.[(triple4 OR ((triple6 triple5) -> rule1))] Gary is quiet.[(triple5)] Gary is red.[(triple6)] Gary is rough.[(triple7)]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is green.
("Gary" "is" "green" "+")
triple3
((triple1) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple4
((triple6 triple5) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7