Gary is big. Gary is blue. Gary is cold. Gary is furry. Gary is nice. Gary is red. Gary is white. Furry people are blue. If Gary is cold then Gary is white.
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Furry people are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If Gary is cold then Gary is white.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "white" "+"))
Gary is blue.
True
1
proof
[(triple2 OR ((triple4) -> rule1))]
("Gary" "is" "blue" "+")
triple2
((triple4) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not furry.
False
1
inv-proof
[(triple4)]
("Gary" "is" "furry" "-")
triple4
@0: Gary is big.[(triple1)] Gary is blue.[(triple2 OR ((triple4) -> rule1))] Gary is cold.[(triple3)] Gary is furry.[(triple4)] Gary is nice.[(triple5)] Gary is red.[(triple6)] Gary is white.[(triple7 OR ((triple3) -> rule2))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is blue.
("Gary" "is" "blue" "+")
triple2
((triple4) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Gary is furry.
("Gary" "is" "furry" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is red.
("Gary" "is" "red" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
((triple3) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1