Anne is big. Furry, red things are rough. If something is big then it is rough. Rough things are blue. If Anne is blue then Anne is not quiet. If Anne is red then Anne is furry. Blue things are white.
Anne is big.
("Anne" "is" "big" "+")
Furry, red things are rough.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is big then it is rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
Rough things are blue.
((("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If Anne is blue then Anne is not quiet.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "quiet" "-"))
If Anne is red then Anne is furry.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "furry" "+"))
Blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is rough.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is white.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule6))]
("Anne" "is" "white" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is quiet.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule4))]
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not furry.
Unknown
inv-rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "furry" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is big.[(triple1)] @1: Anne is rough.[(((triple1) -> rule2))] @2: Anne is blue.[(((((triple1) -> rule2)) -> rule3))] @3: Anne is not quiet.[(((((((triple1) -> rule2)) -> rule3)) -> rule4))] Anne is white.[(((((((triple1) -> rule2)) -> rule3)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not quiet.
("Anne" "is" "quiet" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3