Anne is furry. Gary is smart. If something is smart then it is not quiet. If Gary is not smart then Gary is not kind. If something is kind then it is rough.
Anne is furry.
("Anne" "is" "furry" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is smart then it is not quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "-"))
If Gary is not smart then Gary is not kind.
((("Gary" "is" "smart" "~")) -> ("Gary" "is" "kind" "-"))
If something is kind then it is rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Gary is smart.
True
1
proof
[(triple2)]
("Gary" "is" "smart" "+")
triple2
Gary is not smart.
False
1
inv-proof
[(triple2)]
("Gary" "is" "smart" "-")
triple2
Gary is not quiet.
True
2
proof
[(((triple2) -> rule1))]
("Gary" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is quiet.
False
2
inv-proof
[(((triple2) -> rule1))]
("Gary" "is" "quiet" "+")
((triple2) -> (rule1 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is not rough.
Unknown
inv-rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "rough" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "rough" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is furry.[(triple1)] Gary is smart.[(triple2)] @1: Gary is not quiet.[(((triple2) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Gary is smart.
("Gary" "is" "smart" "+")
triple2
Gary is not quiet.
("Gary" "is" "quiet" "-")
((triple2) -> (rule1 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1