Anne is kind. Anne is not quiet. Anne is not rough. Anne is smart. Anne is young. Dave is cold. Dave is kind. Dave is smart. Dave is white. Dave is young. All white people are rough. All young, rough people are not quiet. If someone is white then they are cold.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
All white people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
All young, rough people are not quiet.
((("someone" "is" "young" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "-"))
If someone is white then they are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Dave is smart.
True
1
proof
[(triple8)]
("Dave" "is" "smart" "+")
triple8
Anne is rough.
False
1
inv-proof
[(triple3)]
("Anne" "is" "rough" "+")
triple3
Dave is rough.
True
2
proof
[(((triple9) -> rule1))]
("Dave" "is" "rough" "+")
((triple9) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple9) -> rule1))]
("Dave" "is" "rough" "-")
((triple9) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not quiet.
True
4
proof
[(((triple10 ((triple9) -> rule1)) -> rule2))]
("Dave" "is" "quiet" "-")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is quiet.
False
4
inv-proof
[(((triple10 ((triple9) -> rule1)) -> rule2))]
("Dave" "is" "quiet" "+")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is kind.[(triple1)] Anne is not quiet.[(triple2)] Anne is not rough.[(triple3)] Anne is smart.[(triple4)] Anne is young.[(triple5)] Dave is cold.[(triple6 OR ((triple9) -> rule3))] Dave is kind.[(triple7)] Dave is smart.[(triple8)] Dave is white.[(triple9)] Dave is young.[(triple10)] @1: Dave is rough.[(((triple9) -> rule1))] @2: Dave is not quiet.[(((triple10 ((triple9) -> rule1)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple2
Anne is not rough.
("Anne" "is" "rough" "-")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
((triple9) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is smart.
("Dave" "is" "smart" "+")
triple8
Dave is white.
("Dave" "is" "white" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Dave is rough.
("Dave" "is" "rough" "+")
((triple9) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is not quiet.
("Dave" "is" "quiet" "-")
((triple10 ((triple9) -> (rule1 % int2))) -> (rule2 % int1))
Dave is not quiet.
("Dave" "is" "quiet" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2