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