Anne is white. Charlie is green. Gary is blue. Harry is big. If Charlie is round and Charlie is white then Charlie is green. If Charlie is kind then Charlie is white. If Anne is green and Anne is blue then Anne is rough.
Anne is white.
("Anne" "is" "white" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Harry is big.
("Harry" "is" "big" "+")
If Charlie is round and Charlie is white then Charlie is green.
((("Charlie" "is" "round" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "green" "+"))
If Charlie is kind then Charlie is white.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "white" "+"))
If Anne is green and Anne is blue then Anne is rough.
((("Anne" "is" "green" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "rough" "+"))
Gary is blue.
True
1
proof
[(triple3)]
("Gary" "is" "blue" "+")
triple3
Harry is not big.
False
1
inv-proof
[(triple4)]
("Harry" "is" "big" "-")
triple4
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is white.[(triple1)] Charlie is green.[(triple2)] Gary is blue.[(triple3)] Harry is big.[(triple4)]
Anne is white.
("Anne" "is" "white" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4