Gary is smart. If someone is furry and not cold then they are round. If someone is smart then they are rough. If someone is quiet and not cold then they are big. Quiet people are smart. If someone is cold and round then they are not quiet. If Gary is big and Gary is not cold then Gary is not furry.
Gary is smart.
("Gary" "is" "smart" "+")
If someone is furry and not cold then they are round.
((("someone" "is" "furry" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "round" "+"))
If someone is smart then they are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
If someone is quiet and not cold then they are big.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "big" "+"))
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold and round then they are not quiet.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "-"))
If Gary is big and Gary is not cold then Gary is not furry.
((("Gary" "is" "big" "+") ("Gary" "is" "cold" "~")) -> ("Gary" "is" "furry" "-"))
Gary is smart.
True
1
proof
[(triple1)]
("Gary" "is" "smart" "+")
triple1
Gary is not smart.
False
1
inv-proof
[(triple1)]
("Gary" "is" "smart" "-")
triple1
Gary is rough.
True
2
proof
[(((triple1) -> rule2))]
("Gary" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("Gary" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Gary is smart.[(triple1)] @1: Gary is rough.[(((triple1) -> rule2))]
Gary is smart.
("Gary" "is" "smart" "+")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1