Anne is big. Anne is blue. Anne is furry. Anne is nice. Anne is quiet. Anne is young. Dave is furry. Dave is nice. Erin is big. Erin is furry. Erin is nice. Erin is young. If something is furry and big then it is quiet. If something is nice then it is big. If something is furry and quiet then it is young.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is furry and big then it is quiet.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is furry and quiet then it is young.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Anne is blue.
True
1
proof
[(triple2)]
("Anne" "is" "blue" "+")
triple2
Dave is not furry.
False
1
inv-proof
[(triple7)]
("Dave" "is" "furry" "-")
triple7
Dave is big.
True
2
proof
[(((triple8) -> rule2))]
("Dave" "is" "big" "+")
((triple8) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Erin is not quiet.
False
3
inv-proof
[(((triple10 triple9) -> rule1) OR ((triple10 ((triple11) -> rule2)) -> rule1))]
("Erin" "is" "quiet" "-")
((triple10 triple9) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple10 ((triple11) -> (rule2 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Dave is quiet.
True
4
proof
[(((triple7 ((triple8) -> rule2)) -> rule1))]
("Dave" "is" "quiet" "+")
((triple7 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not quiet.
False
4
inv-proof
[(((triple7 ((triple8) -> rule2)) -> rule1))]
("Dave" "is" "quiet" "-")
((triple7 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is big.[(triple1 OR ((triple4) -> rule2))] Anne is blue.[(triple2)] Anne is furry.[(triple3)] Anne is nice.[(triple4)] Anne is quiet.[(triple5 OR ((triple3 triple1) -> rule1) OR ((triple3 ((triple4) -> rule2)) -> rule1))] Anne is young.[(triple6 OR ((triple3 triple5) -> rule3) OR ((triple3 ((triple3 triple1) -> rule1)) -> rule3) OR ((triple3 ((triple3 ((triple4) -> rule2)) -> rule1)) -> rule3))] Dave is furry.[(triple7)] Dave is nice.[(triple8)] Erin is big.[(triple9 OR ((triple11) -> rule2))] Erin is furry.[(triple10)] Erin is nice.[(triple11)] Erin is young.[(triple12 OR ((triple10 ((triple10 triple9) -> rule1)) -> rule3) OR ((triple10 ((triple10 ((triple11) -> rule2)) -> rule1)) -> rule3))] @1: Dave is big.[(((triple8) -> rule2))] Erin is quiet.[(((triple10 triple9) -> rule1) OR ((triple10 ((triple11) -> rule2)) -> rule1))] @2: Dave is quiet.[(((triple7 ((triple8) -> rule2)) -> rule1))] @3: Dave is young.[(((triple7 ((triple7 ((triple8) -> rule2)) -> rule1)) -> rule3))]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple4) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
((triple3 triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple3 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple6
((triple3 triple5) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple3 ((triple3 triple1) -> (rule1 % int2))) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
((triple3 ((triple3 ((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
triple8
Erin is big.
("Erin" "is" "big" "+")
triple9
((triple11) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple10
Erin is nice.
("Erin" "is" "nice" "+")
triple11
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple10 ((triple10 triple9) -> (rule1 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((triple10 ((triple10 ((triple11) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Dave is big.
("Dave" "is" "big" "+")
((triple8) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple10 triple9) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple10 ((triple11) -> (rule2 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple7 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((triple7 ((triple7 ((triple8) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3