Gary is big. Gary is blue. Gary is cold. Gary is nice. Gary is red. Gary is rough. Gary is white. Cold, rough things are big. If something is nice and blue then it is rough. If something is big and cold then it is rough.
Gary is big.
("Gary" "is" "big" "+")
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 white.
("Gary" "is" "white" "+")
Cold, rough things are big.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something is nice and blue then it is rough.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is big and cold then it is rough.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Gary is rough.
True
1
proof
[(triple6 OR ((triple1 triple3) -> rule3) OR ((triple4 triple2) -> rule2))]
("Gary" "is" "rough" "+")
triple6
((triple1 triple3) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple4 triple2) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not white.
False
1
inv-proof
[(triple7)]
("Gary" "is" "white" "-")
triple7
@0: Gary is big.[(triple1 OR ((triple3 triple6) -> rule1) OR ((triple3 ((triple4 triple2) -> rule2)) -> rule1))] Gary is blue.[(triple2)] Gary is cold.[(triple3)] Gary is nice.[(triple4)] Gary is red.[(triple5)] Gary is rough.[(triple6 OR ((triple1 triple3) -> rule3) OR ((triple4 triple2) -> rule2))] Gary is white.[(triple7)]
Gary is big.
("Gary" "is" "big" "+")
triple1
((triple3 triple6) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((triple3 ((triple4 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
((triple1 triple3) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
((triple4 triple2) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple7