Anne is white. If someone is furry and red then they are rough. If Anne is blue and Anne is white then Anne is green. If someone is red and furry then they are green. All white, quiet people are rough. If Anne is white then Anne is quiet. All white, red people are rough.
Anne is white.
("Anne" "is" "white" "+")
If someone is furry and red then they are rough.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If Anne is blue and Anne is white then Anne is green.
((("Anne" "is" "blue" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "green" "+"))
If someone is red and furry then they are green.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All white, quiet people are rough.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If Anne is white then Anne is quiet.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "quiet" "+"))
All white, red people are rough.
((("someone" "is" "white" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Anne is quiet.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule4))]
("Anne" "is" "rough" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule4))]
("Anne" "is" "rough" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is white.[(triple1)] @1: Anne is quiet.[(((triple1) -> rule5))] @2: Anne is rough.[(((triple1 ((triple1) -> rule5)) -> rule4))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2