Anne is furry. Bob is not quiet. Charlie is nice. Nice things are not rough. If something is quiet and not cold then it is rough. Big, round things are not nice.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Nice things are not rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "-"))
If something is quiet and not cold then it is rough.
((("something" "is" "quiet" "+") ("something" "is" "cold" "~")) -> ("something" "is" "rough" "+"))
Big, round things are not nice.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "-"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Bob is quiet.
False
1
inv-proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Anne is furry.[(triple1)] Bob is not quiet.[(triple2)] Charlie is nice.[(triple3)] @1: Charlie is not rough.[(((triple3) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is not rough.
("Charlie" "is" "rough" "-")
((triple3) -> (rule1 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1