Anne is rough. Anne is not smart. Gary is smart. If Gary is cold then Gary is not nice. If someone is smart then they are not young. If someone is blue and not rough then they are young. If Anne is not rough then Anne is not blue. If someone is round and not smart then they are cold. If someone is young and rough then they are blue.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Gary is smart.
("Gary" "is" "smart" "+")
If Gary is cold then Gary is not nice.
((("Gary" "is" "cold" "+")) -> ("Gary" "is" "nice" "-"))
If someone is smart then they are not young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "-"))
If someone is blue and not rough then they are young.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "young" "+"))
If Anne is not rough then Anne is not blue.
((("Anne" "is" "rough" "~")) -> ("Anne" "is" "blue" "-"))
If someone is round and not smart then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "cold" "+"))
If someone is young and rough then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Anne is not smart.[(triple2)] Anne is rough.[(triple1)] Gary is smart.[(triple3)] @1: Gary is not young.[(((triple3) -> rule2))]
Anne is not smart.
("Anne" "is" "smart" "-")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Gary is not young.
("Gary" "is" "young" "-")
((triple3) -> (rule2 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1