Gary is blue. Gary is cold. Gary is nice. Gary is red. Gary is rough. Gary is not smart. Gary is young. If something is rough and not red then it is not cold. If Gary is young then Gary is nice.
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is not smart.
("Gary" "is" "smart" "-")
Gary is young.
("Gary" "is" "young" "+")
If something is rough and not red then it is not cold.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "cold" "-"))
If Gary is young then Gary is nice.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "nice" "+"))
Gary is not smart.
True
1
proof
[(triple6)]
("Gary" "is" "smart" "-")
triple6
Gary is not cold.
False
1
inv-proof
[(triple2)]
("Gary" "is" "cold" "-")
triple2
@0: Gary is blue.[(triple1)] Gary is cold.[(triple2)] Gary is nice.[(triple3 OR ((triple7) -> rule2))] Gary is not smart.[(triple6)] Gary is red.[(triple4)] Gary is rough.[(triple5)] Gary is young.[(triple7)]
Gary is blue.
("Gary" "is" "blue" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
((triple7) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not smart.
("Gary" "is" "smart" "-")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Gary is young.
("Gary" "is" "young" "+")
triple7