Anne is green. Anne is kind. Anne is red. Dave is green. Dave is nice. Dave is quiet. Dave is red. All quiet, green things are nice. All red, kind things are young. If Dave is green and Dave is rough then Dave is quiet. Quiet, kind things are green. Red, green things are nice. All red things are nice. Young things are rough. All kind, young things are rough.
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
All quiet, green things are nice.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All red, kind things are young.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If Dave is green and Dave is rough then Dave is quiet.
((("Dave" "is" "green" "+") ("Dave" "is" "rough" "+")) -> ("Dave" "is" "quiet" "+"))
Quiet, kind things are green.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Red, green things are nice.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Young things are rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
All kind, young things are rough.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Dave is quiet.
True
1
proof
[(triple6)]
("Dave" "is" "quiet" "+")
triple6
Dave is not quiet.
False
1
inv-proof
[(triple6)]
("Dave" "is" "quiet" "-")
triple6
Anne is young.
True
3
proof
[(((triple3 triple2) -> rule2))]
("Anne" "is" "young" "+")
((triple3 triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple3) -> rule6) OR ((triple3 triple1) -> rule5))]
("Anne" "is" "nice" "-")
((triple3) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple3 triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
True
4
proof
[(((((triple3 triple2) -> rule2)) -> rule7) OR ((triple2 ((triple3 triple2) -> rule2)) -> rule8))]
("Anne" "is" "rough" "+")
((((triple3 triple2) -> (rule2 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple2 ((triple3 triple2) -> (rule2 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not rough.
False
4
inv-proof
[(((((triple3 triple2) -> rule2)) -> rule7) OR ((triple2 ((triple3 triple2) -> rule2)) -> rule8))]
("Anne" "is" "rough" "-")
((((triple3 triple2) -> (rule2 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple2 ((triple3 triple2) -> (rule2 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Dave is not rough.
Unknown
inv-rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is young.
Unknown
rconc
[@1: Dave is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "young" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Anne is green.[(triple1)] Anne is kind.[(triple2)] Anne is red.[(triple3)] Dave is green.[(triple4)] Dave is nice.[(triple5 OR ((triple7) -> rule6) OR ((triple6 triple4) -> rule1) OR ((triple7 triple4) -> rule5))] Dave is quiet.[(triple6)] Dave is red.[(triple7)] @1: Anne is nice.[(((triple3) -> rule6) OR ((triple3 triple1) -> rule5))] Anne is young.[(((triple3 triple2) -> rule2))] @2: Anne is rough.[(((((triple3 triple2) -> rule2)) -> rule7) OR ((triple2 ((triple3 triple2) -> rule2)) -> rule8))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple4
Dave is nice.
("Dave" "is" "nice" "+")
triple5
((triple7) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple6 triple4) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple7 triple4) -> (rule5 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Dave is red.
("Dave" "is" "red" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple3 triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple3 triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple3 triple2) -> (rule2 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((triple2 ((triple3 triple2) -> (rule2 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2