Gary is big. Gary is cold. Gary is furry. Gary is nice. Gary is not quiet. Gary is not red. Gary is not rough. If Gary is quiet and Gary is furry then Gary is rough. If Gary is quiet and Gary is furry then Gary is rough. If something is nice then it is furry. Quiet things are red. If Gary is cold and Gary is furry then Gary is not quiet. If Gary is red and Gary is furry then Gary is quiet. If Gary is nice and Gary is red then Gary is big. If something is quiet and not red then it is big.
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is not red.
("Gary" "is" "red" "-")
Gary is not rough.
("Gary" "is" "rough" "-")
If Gary is quiet and Gary is furry then Gary is rough.
((("Gary" "is" "quiet" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "rough" "+"))
If Gary is quiet and Gary is furry then Gary is rough.
((("Gary" "is" "quiet" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "rough" "+"))
If something is nice then it is furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Quiet things are red.
((("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If Gary is cold and Gary is furry then Gary is not quiet.
((("Gary" "is" "cold" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "quiet" "-"))
If Gary is red and Gary is furry then Gary is quiet.
((("Gary" "is" "red" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "quiet" "+"))
If Gary is nice and Gary is red then Gary is big.
((("Gary" "is" "nice" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "big" "+"))
If something is quiet and not red then it is big.
((("something" "is" "quiet" "+") ("something" "is" "red" "~")) -> ("something" "is" "big" "+"))
Gary is furry.
True
1
proof
[(triple3 OR ((triple4) -> rule3))]
("Gary" "is" "furry" "+")
triple3
((triple4) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
1
inv-proof
[(triple3 OR ((triple4) -> rule3))]
("Gary" "is" "furry" "-")
triple3
((triple4) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
@0: Gary is big.[(triple1)] Gary is cold.[(triple2)] Gary is furry.[(triple3 OR ((triple4) -> rule3))] Gary is nice.[(triple4)] Gary is not quiet.[(triple5 OR ((triple2 triple3) -> rule5) OR ((triple2 ((triple4) -> rule3)) -> rule5))] Gary is not red.[(triple6)] Gary is not rough.[(triple7)]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
((triple4) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple5
((triple2 triple3) -> (rule5 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
((triple2 ((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not red.
("Gary" "is" "red" "-")
triple6
Gary is not rough.
("Gary" "is" "rough" "-")
triple7