The bear is cold. The bear is green. The bear is red. The bear is rough. The bear is young. The bear likes the cat. The bear needs the cat. The bear visits the cat. The cat is green. The cat is rough. The cat likes the bear. The cat visits the bear. If someone is red then they need the cat. If someone needs the cat then they visit the cat. If someone is red and they need the cat then they visit the cat. If someone visits the bear then the bear visits the cat. If someone needs the cat and they like the cat then the cat is red. If someone needs the bear and the bear needs the cat then they visit the cat.
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
If someone is red then they need the cat.
((("someone" "is" "red" "+")) -> ("someone" "needs" "cat" "+"))
If someone needs the cat then they visit the cat.
((("someone" "needs" "cat" "+")) -> ("someone" "visits" "cat" "+"))
If someone is red and they need the cat then they visit the cat.
((("someone" "is" "red" "+") ("someone" "needs" "cat" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the bear then the bear visits the cat.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "cat" "+"))
If someone needs the cat and they like the cat then the cat is red.
((("someone" "needs" "cat" "+") ("someone" "likes" "cat" "+")) -> ("cat" "is" "red" "+"))
If someone needs the bear and the bear needs the cat then they visit the cat.
((("someone" "needs" "bear" "+") ("bear" "needs" "cat" "+")) -> ("someone" "visits" "cat" "+"))
The bear likes the cat.
True
1
proof
[(triple6)]
("bear" "likes" "cat" "+")
triple6
The bear is not rough.
False
1
inv-proof
[(triple4)]
("bear" "is" "rough" "-")
triple4
The cat is red.
True
3
proof
[(((triple7 triple6) -> rule5) OR ((((triple3) -> rule1) triple6) -> rule5))]
("cat" "is" "red" "+")
((triple7 triple6) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple3) -> (rule1 % int2)) triple6) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The bear needs the cat.
("bear" "needs" "cat" "+")
int2
The cat is not red.
False
3
inv-proof
[(((triple7 triple6) -> rule5) OR ((((triple3) -> rule1) triple6) -> rule5))]
("cat" "is" "red" "-")
((triple7 triple6) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple3) -> (rule1 % int2)) triple6) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The bear needs the cat.
("bear" "needs" "cat" "+")
int2
The cat needs the cat.
True
4
proof
[(((((triple7 triple6) -> rule5)) -> rule1) OR ((((((triple3) -> rule1) triple6) -> rule5)) -> rule1))]
("cat" "needs" "cat" "+")
((((triple7 triple6) -> (rule5 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((((triple3) -> (rule1 % int3)) triple6) -> (rule5 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The bear needs the cat.
("bear" "needs" "cat" "+")
int3
The cat does not need the cat.
False
4
inv-proof
[(((((triple7 triple6) -> rule5)) -> rule1) OR ((((((triple3) -> rule1) triple6) -> rule5)) -> rule1))]
("cat" "needs" "cat" "-")
((((triple7 triple6) -> (rule5 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((((triple3) -> (rule1 % int3)) triple6) -> (rule5 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The bear needs the cat.
("bear" "needs" "cat" "+")
int3
The cat does not need the bear.
Unknown
inv-random
[@0: The cat needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "bear" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The bear does not need the bear.
Unknown
inv-random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is cold.[(triple1)] The bear is green.[(triple2)] The bear is red.[(triple3)] The bear is rough.[(triple4)] The bear is young.[(triple5)] The bear likes the cat.[(triple6)] The bear needs the cat.[(triple7 OR ((triple3) -> rule1))] The bear visits the cat.[(triple8 OR ((triple12) -> rule4) OR ((triple7) -> rule2) OR ((triple3 triple7) -> rule3) OR ((((triple3) -> rule1)) -> rule2) OR ((triple3 ((triple3) -> rule1)) -> rule3))] The cat is green.[(triple9)] The cat is rough.[(triple10)] The cat likes the bear.[(triple11)] The cat visits the bear.[(triple12)] @1: The cat is red.[(((triple7 triple6) -> rule5) OR ((((triple3) -> rule1) triple6) -> rule5))] @2: The cat needs the cat.[(((((triple7 triple6) -> rule5)) -> rule1) OR ((((((triple3) -> rule1) triple6) -> rule5)) -> rule1))] @3: The cat visits the cat.[(((((((triple7 triple6) -> rule5)) -> rule1)) -> rule2) OR ((((triple7 triple6) -> rule5) ((((triple7 triple6) -> rule5)) -> rule1)) -> rule3) OR ((((((triple3) -> rule1) triple6) -> rule5) ((((triple7 triple6) -> rule5)) -> rule1)) -> rule3) OR ((((((((triple3) -> rule1) triple6) -> rule5)) -> rule1)) -> rule2) OR ((((triple7 triple6) -> rule5) ((((((triple3) -> rule1) triple6) -> rule5)) -> rule1)) -> rule3) OR ((((((triple3) -> rule1) triple6) -> rule5) ((((((triple3) -> rule1) triple6) -> rule5)) -> rule1)) -> rule3))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
The bear is rough.
("bear" "is" "rough" "+")
triple4
The bear is young.
("bear" "is" "young" "+")
triple5
The bear likes the cat.
("bear" "likes" "cat" "+")
triple6
The bear needs the cat.
("bear" "needs" "cat" "+")
triple7
((triple3) -> (rule1 % int1))
The bear needs the cat.
("bear" "needs" "cat" "+")
int1
The bear visits the cat.
("bear" "visits" "cat" "+")
triple8
((triple12) -> (rule4 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
((triple7) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
((triple3 triple7) -> (rule3 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear needs the cat.
("bear" "needs" "cat" "+")
int2
((triple3 ((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The bear needs the cat.
("bear" "needs" "cat" "+")
int2
The cat is green.
("cat" "is" "green" "+")
triple9
The cat is rough.
("cat" "is" "rough" "+")
triple10
The cat likes the bear.
("cat" "likes" "bear" "+")
triple11
The cat visits the bear.
("cat" "visits" "bear" "+")
triple12
The cat is red.
("cat" "is" "red" "+")
((triple7 triple6) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
((((triple3) -> (rule1 % int2)) triple6) -> (rule5 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The bear needs the cat.
("bear" "needs" "cat" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
((((triple7 triple6) -> (rule5 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((((triple3) -> (rule1 % int3)) triple6) -> (rule5 % int2))) -> (rule1 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The bear needs the cat.
("bear" "needs" "cat" "+")
int3
The cat visits the cat.
("cat" "visits" "cat" "+")
((((((triple7 triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
((((triple7 triple6) -> (rule5 % int3)) ((((triple7 triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
((((((triple3) -> (rule1 % int4)) triple6) -> (rule5 % int3)) ((((triple7 triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The bear needs the cat.
("bear" "needs" "cat" "+")
int4
((((((((triple3) -> (rule1 % int4)) triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The bear needs the cat.
("bear" "needs" "cat" "+")
int4
((((triple7 triple6) -> (rule5 % int4)) ((((((triple3) -> (rule1 % int3)) triple6) -> (rule5 % int4))) -> (rule1 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The bear needs the cat.
("bear" "needs" "cat" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
((((((triple3) -> (rule1 % int4)) triple6) -> (rule5 % int3)) ((((((triple3) -> (rule1 % int4)) triple6) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The bear needs the cat.
("bear" "needs" "cat" "+")
int4