Anne is furry. Charlie is green. Gary is rough. Furry, red things are blue. If Gary is red and Gary is blue then Gary is not green. All green things are not nice. If Gary is blue and Gary is not green then Gary is rough. If something is nice and not green then it is rough. If something is blue and not red then it is rough.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Furry, red things are blue.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If Gary is red and Gary is blue then Gary is not green.
((("Gary" "is" "red" "+") ("Gary" "is" "blue" "+")) -> ("Gary" "is" "green" "-"))
All green things are not nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "-"))
If Gary is blue and Gary is not green then Gary is rough.
((("Gary" "is" "blue" "+") ("Gary" "is" "green" "~")) -> ("Gary" "is" "rough" "+"))
If something is nice and not green then it is rough.
((("something" "is" "nice" "+") ("something" "is" "green" "~")) -> ("something" "is" "rough" "+"))
If something is blue and not red then it is rough.
((("something" "is" "blue" "+") ("something" "is" "red" "~")) -> ("something" "is" "rough" "+"))
Gary is rough.
True
1
proof
[(triple3)]
("Gary" "is" "rough" "+")
triple3
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Charlie is not nice.
True
2
proof
[(((triple2) -> rule3))]
("Charlie" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("Charlie" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "rough" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is furry.[(triple1)] Charlie is green.[(triple2)] Gary is rough.[(triple3)] @1: Charlie is not nice.[(((triple2) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Charlie is not nice.
("Charlie" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Charlie is not nice.
("Charlie" "is" "nice" "-")
int1