Anne is quiet. Dave is rough. Gary is furry. If Anne is rough then Anne is white. If Gary is rough and Gary is not round then Gary is not quiet. Furry things are not blue. If Gary is not furry then Gary is white. All round things are rough. All white things are rough. If something is blue then it is quiet. If something is green and not white then it is quiet.
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is furry.
("Gary" "is" "furry" "+")
If Anne is rough then Anne is white.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "white" "+"))
If Gary is rough and Gary is not round then Gary is not quiet.
((("Gary" "is" "rough" "+") ("Gary" "is" "round" "~")) -> ("Gary" "is" "quiet" "-"))
Furry things are not blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "-"))
If Gary is not furry then Gary is white.
((("Gary" "is" "furry" "~")) -> ("Gary" "is" "white" "+"))
All round things are rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
All white things are rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is green and not white then it is quiet.
((("something" "is" "green" "+") ("something" "is" "white" "~")) -> ("something" "is" "quiet" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is not white.
Unknown
inv-rconc
[@2: Anne is white.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is quiet.[(triple1)] Dave is rough.[(triple2)] Gary is furry.[(triple3)] @1: Gary is not blue.[(((triple3) -> rule3))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Gary is not blue.
("Gary" "is" "blue" "-")
((triple3) -> (rule3 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1