Anne is big. Bob is not big. Bob is quiet. Charlie is quiet. Dave is green. Dave is nice. Dave is quiet. Big people are rough. All rough people are not quiet.
Anne is big.
("Anne" "is" "big" "+")
Bob is not big.
("Bob" "is" "big" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
All rough people are not quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "-"))
Bob is quiet.
True
1
proof
[(triple3)]
("Bob" "is" "quiet" "+")
triple3
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is rough.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "rough" "-")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not quiet.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is quiet.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "rough" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "rough" "+")
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is big.[(triple1)] Bob is not big.[(triple2)] Bob is quiet.[(triple3)] Charlie is quiet.[(triple4)] Dave is green.[(triple5)] Dave is nice.[(triple6)] Dave is quiet.[(triple7)] @1: Anne is rough.[(((triple1) -> rule1))] @2: Anne is not quiet.[(((((triple1) -> rule1)) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Bob is not big.
("Bob" "is" "big" "-")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is nice.
("Dave" "is" "nice" "+")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2