Anne is big. Anne is kind. Dave is furry. Dave is quiet. Dave is white. Erin is big. Erin is furry. Erin is green. Erin is white. Erin is young. All white things are green. All furry things are white. If Erin is kind then Erin is quiet. Quiet things are kind. Furry, green things are kind. All kind things are furry. All quiet things are furry. Quiet things are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
All white things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
All furry things are white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If Erin is kind then Erin is quiet.
((("Erin" "is" "kind" "+")) -> ("Erin" "is" "quiet" "+"))
Quiet things are kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Furry, green things are kind.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
All quiet things are furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Erin is young.
True
1
proof
[(triple10)]
("Erin" "is" "young" "+")
triple10
Dave is not white.
False
1
inv-proof
[(triple5 OR ((triple3) -> rule2) OR ((((triple4) -> rule7)) -> rule2) OR ((((((triple4) -> rule4)) -> rule6)) -> rule2))]
("Dave" "is" "white" "-")
triple5
((triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Erin is kind.
True
3
proof
[(((triple7 triple8) -> rule5) OR ((triple7 ((triple9) -> rule1)) -> rule5) OR ((triple7 ((((triple7) -> rule2)) -> rule1)) -> rule5))]
("Erin" "is" "kind" "+")
((triple7 triple8) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple7 ((triple9) -> (rule1 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((triple7 ((((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Dave is not green.
False
2
inv-proof
[(((triple4) -> rule8) OR ((triple5) -> rule1) OR ((((triple3) -> rule2)) -> rule1) OR ((((((triple4) -> rule7)) -> rule2)) -> rule1) OR ((((((((triple4) -> rule4)) -> rule6)) -> rule2)) -> rule1))]
("Dave" "is" "green" "-")
((triple4) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Erin is quiet.
True
4
proof
[(((((triple7 triple8) -> rule5)) -> rule3) OR ((((triple7 ((triple9) -> rule1)) -> rule5)) -> rule3) OR ((((triple7 ((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule3))]
("Erin" "is" "quiet" "+")
((((triple7 triple8) -> (rule5 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple7 ((triple9) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((triple7 ((((triple7) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Anne is not white.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("Anne" "is" "white" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
True
4
proof
[(((((((triple2) -> rule6)) -> rule2)) -> rule1))]
("Anne" "is" "green" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not green.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule2)) -> rule1))]
("Anne" "is" "green" "-")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is kind.[(triple2)] Dave is furry.[(triple3 OR ((triple4) -> rule7) OR ((((triple4) -> rule4)) -> rule6))] Dave is quiet.[(triple4)] Dave is white.[(triple5 OR ((triple3) -> rule2) OR ((((triple4) -> rule7)) -> rule2) OR ((((((triple4) -> rule4)) -> rule6)) -> rule2))] Erin is big.[(triple6)] Erin is furry.[(triple7)] Erin is green.[(triple8 OR ((triple9) -> rule1) OR ((((triple7) -> rule2)) -> rule1))] Erin is white.[(triple9 OR ((triple7) -> rule2))] Erin is young.[(triple10)] @1: Anne is furry.[(((triple2) -> rule6))] Dave is green.[(((triple4) -> rule8) OR ((triple5) -> rule1) OR ((((triple3) -> rule2)) -> rule1) OR ((((((triple4) -> rule7)) -> rule2)) -> rule1) OR ((((((((triple4) -> rule4)) -> rule6)) -> rule2)) -> rule1))] Dave is kind.[(((triple4) -> rule4) OR ((triple3 ((triple4) -> rule8)) -> rule5) OR ((triple3 ((triple5) -> rule1)) -> rule5) OR ((((triple4) -> rule7) ((triple4) -> rule8)) -> rule5) OR ((((triple4) -> rule7) ((triple5) -> rule1)) -> rule5) OR ((triple3 ((((triple3) -> rule2)) -> rule1)) -> rule5) OR ((((triple4) -> rule7) ((((triple3) -> rule2)) -> rule1)) -> rule5) OR ((triple3 ((((((triple4) -> rule7)) -> rule2)) -> rule1)) -> rule5) OR ((((triple4) -> rule7) ((((((triple4) -> rule7)) -> rule2)) -> rule1)) -> rule5))] Erin is kind.[(((triple7 triple8) -> rule5) OR ((triple7 ((triple9) -> rule1)) -> rule5) OR ((triple7 ((((triple7) -> rule2)) -> rule1)) -> rule5))] @2: Anne is white.[(((((triple2) -> rule6)) -> rule2))] Erin is quiet.[(((((triple7 triple8) -> rule5)) -> rule3) OR ((((triple7 ((triple9) -> rule1)) -> rule5)) -> rule3) OR ((((triple7 ((((triple7) -> rule2)) -> rule1)) -> rule5)) -> rule3))] @3: Anne is green.[(((((((triple2) -> rule6)) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple4) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
((triple3) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((((triple4) -> (rule7 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
((triple9) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple9
((triple7) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple10
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule6 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple5) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((((triple4) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((((((triple4) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
((triple4) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple3 ((triple4) -> (rule8 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((triple3 ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
((((triple4) -> (rule7 % int3)) ((triple4) -> (rule8 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((((triple4) -> (rule7 % int3)) ((triple5) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((((triple4) -> (rule7 % int4)) ((((triple3) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
((triple3 ((((((triple4) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
((((triple4) -> (rule7 % int4)) ((((((triple4) -> (rule7 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
((triple7 triple8) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple7 ((triple9) -> (rule1 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
((triple7 ((((triple7) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple7 triple8) -> (rule5 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((((triple7 ((triple9) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
((((triple7 ((((triple7) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Anne is green.
("Anne" "is" "green" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3