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