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