Anne is not nice. Anne is quiet. Anne is red. Charlie is not kind. Charlie is nice. Charlie is young. Dave is kind. Dave is red. Dave is young. Erin is blue. Erin is kind. Erin is young. Kind things are young. All kind things are quiet. All red things are not blue. If something is quiet then it is kind. Red, rough things are kind. If something is quiet then it is not rough.
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is young.
("Erin" "is" "young" "+")
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
All red things are not blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "-"))
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Red, rough things are kind.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is quiet then it is not rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "-"))
Anne is quiet.
True
1
proof
[(triple2)]
("Anne" "is" "quiet" "+")
triple2
Charlie is kind.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "kind" "+")
triple4
Anne is not blue.
True
2
proof
[(((triple3) -> rule3))]
("Anne" "is" "blue" "-")
((triple3) -> (rule3 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is not kind.
False
2
inv-proof
[(((triple2) -> rule4))]
("Anne" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Anne is not nice.[(triple1)] Anne is quiet.[(triple2)] Anne is red.[(triple3)] Charlie is nice.[(triple5)] Charlie is not kind.[(triple4)] Charlie is young.[(triple6)] Dave is kind.[(triple7)] Dave is red.[(triple8)] Dave is young.[(triple9 OR ((triple7) -> rule1))] Erin is blue.[(triple10)] Erin is kind.[(triple11)] Erin is young.[(triple12 OR ((triple11) -> rule1))] @1: Anne is kind.[(((triple2) -> rule4))] Anne is not blue.[(((triple3) -> rule3))] Anne is not rough.[(((triple2) -> rule6))] Dave is not blue.[(((triple8) -> rule3))] Dave is quiet.[(((triple7) -> rule2))] Erin is quiet.[(((triple11) -> rule2))] @2: Anne is young.[(((((triple2) -> rule4)) -> rule1))] Dave is not rough.[(((((triple7) -> rule2)) -> rule6))] Erin is not rough.[(((((triple11) -> rule2)) -> rule6))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is young.
("Dave" "is" "young" "+")
triple9
((triple7) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple10
Erin is kind.
("Erin" "is" "kind" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple11) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not blue.
("Anne" "is" "blue" "-")
((triple3) -> (rule3 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is not rough.
("Anne" "is" "rough" "-")
((triple2) -> (rule6 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Dave is not blue.
("Dave" "is" "blue" "-")
((triple8) -> (rule3 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple7) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple11) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Dave is not rough.
("Dave" "is" "rough" "-")
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Dave is not rough.
("Dave" "is" "rough" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Erin is not rough.
("Erin" "is" "rough" "-")
((((triple11) -> (rule2 % int2))) -> (rule6 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2