Anne is big. Charlie is red. Dave is rough. Gary is rough. If Dave is quiet then Dave is nice. If something is red and not blue then it is round. Blue, round things are quiet. If something is red then it is quiet. If Gary is blue then Gary is round. If Anne is not red and Anne is not blue then Anne is not quiet. If something is nice and not round then it is rough. If something is blue then it is rough.
Anne is big.
("Anne" "is" "big" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Dave is quiet then Dave is nice.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "nice" "+"))
If something is red and not blue then it is round.
((("something" "is" "red" "+") ("something" "is" "blue" "~")) -> ("something" "is" "round" "+"))
Blue, round things are quiet.
((("something" "is" "blue" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
If something is red then it is quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
If Gary is blue then Gary is round.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "round" "+"))
If Anne is not red and Anne is not blue then Anne is not quiet.
((("Anne" "is" "red" "~") ("Anne" "is" "blue" "~")) -> ("Anne" "is" "quiet" "-"))
If something is nice and not round then it is rough.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "is" "rough" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Dave is rough.
True
1
proof
[(triple3)]
("Dave" "is" "rough" "+")
triple3
Dave is not rough.
False
1
inv-proof
[(triple3)]
("Dave" "is" "rough" "-")
triple3
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "quiet" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is big.[(triple1)] Charlie is red.[(triple2)] Dave is rough.[(triple3)] Gary is rough.[(triple4)] @1: Charlie is quiet.[(((triple2) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Gary is rough.
("Gary" "is" "rough" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1