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