Anne is blue. Erin is green. Gary is quiet. If someone is nice then they are blue. Blue, nice people are rough. If someone is green then they are rough. If someone is round then they are nice. If someone is smart and nice then they are blue. If Anne is smart then Anne is quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Erin is green.
("Erin" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
If someone is nice then they are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Blue, nice people are rough.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is round then they are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart and nice then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If Anne is smart then Anne is quiet.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "quiet" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Gary is not quiet.
False
1
inv-proof
[(triple3)]
("Gary" "is" "quiet" "-")
triple3
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "nice" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is blue.[(triple1)] Erin is green.[(triple2)] Gary is quiet.[(triple3)] @1: Erin is rough.[(((triple2) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
((triple2) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1