Anne is green. Bob is red. Dave is quiet. If someone is big then they are white. If Anne is green then Anne is big. If someone is rough and white then they are green.
Anne is green.
("Anne" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If Anne is green then Anne is big.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "big" "+"))
If someone is rough and white then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Anne is green.
True
1
proof
[(triple1)]
("Anne" "is" "green" "+")
triple1
Dave is not quiet.
False
1
inv-proof
[(triple3)]
("Dave" "is" "quiet" "-")
triple3
Anne is big.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "big" "-")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "white" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "white" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "+")
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Anne is green.[(triple1)] Bob is red.[(triple2)] Dave is quiet.[(triple3)] @1: Anne is big.[(((triple1) -> rule2))] @2: Anne is white.[(((((triple1) -> rule2)) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2