Anne is rough. Charlie is big. Gary is young. Harry is quiet. If something is rough and blue then it is nice. All young, nice things are not blue. If Harry is nice and Harry is blue then Harry is rough. If Harry is nice then Harry is quiet. If something is green then it is rough. If something is quiet and nice then it is rough.
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If something is rough and blue then it is nice.
((("something" "is" "rough" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
All young, nice things are not blue.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "-"))
If Harry is nice and Harry is blue then Harry is rough.
((("Harry" "is" "nice" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "rough" "+"))
If Harry is nice then Harry is quiet.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "quiet" "+"))
If something is green then it is rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something is quiet and nice then it is rough.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Charlie is big.
True
1
proof
[(triple2)]
("Charlie" "is" "big" "+")
triple2
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is rough.[(triple1)] Charlie is big.[(triple2)] Gary is young.[(triple3)] Harry is quiet.[(triple4)]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4