Anne is red. Anne is young. Bob is young. Dave is not green. Dave is quiet. Dave is not rough. Dave is not white. Gary is green. Gary is smart. Gary is young. Smart, quiet people are not green. White people are not green. All red, green people are not white. Quiet, green people are white. All white, red people are rough. If someone is white and young then they are not red. If Gary is rough and Gary is smart then Gary is green. If someone is red then they are smart.
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is not green.
("Dave" "is" "green" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is not white.
("Dave" "is" "white" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Smart, quiet people are not green.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "-"))
White people are not green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "-"))
All red, green people are not white.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "-"))
Quiet, green people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
All white, red people are rough.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If someone is white and young then they are not red.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "red" "-"))
If Gary is rough and Gary is smart then Gary is green.
((("Gary" "is" "rough" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "green" "+"))
If someone is red then they are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
Dave is quiet.
True
1
proof
[(triple5)]
("Dave" "is" "quiet" "+")
triple5
Dave is white.
False
1
inv-proof
[(triple7)]
("Dave" "is" "white" "+")
triple7
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "white" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is red.[(triple1)] Anne is young.[(triple2)] Bob is young.[(triple3)] Dave is not green.[(triple4)] Dave is not rough.[(triple6)] Dave is not white.[(triple7)] Dave is quiet.[(triple5)] Gary is green.[(triple8)] Gary is smart.[(triple9)] Gary is young.[(triple10)] @1: Anne is smart.[(((triple1) -> rule8))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
Dave is not green.
("Dave" "is" "green" "-")
triple4
Dave is not rough.
("Dave" "is" "rough" "-")
triple6
Dave is not white.
("Dave" "is" "white" "-")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1