The bear likes the cat. The bear does not like the squirrel. The bear sees the cow. The cat likes the squirrel. The cat does not see the bear. The cow likes the bear. The cow likes the squirrel. The cow does not need the squirrel. The cow sees the squirrel. The squirrel is not big. The squirrel is young. The squirrel needs the cow. If something needs the cat then the cat likes the squirrel. All rough things are not young. If the bear sees the cow then the cow is rough.
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear does not like the squirrel.
("bear" "likes" "squirrel" "-")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cat does not see the bear.
("cat" "sees" "bear" "-")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The cow does not need the squirrel.
("cow" "needs" "squirrel" "-")
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
The squirrel is not big.
("squirrel" "is" "big" "-")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If something needs the cat then the cat likes the squirrel.
((("something" "needs" "cat" "+")) -> ("cat" "likes" "squirrel" "+"))
All rough things are not young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "-"))
If the bear sees the cow then the cow is rough.
((("bear" "sees" "cow" "+")) -> ("cow" "is" "rough" "+"))
The cat does not see the bear.
True
1
proof
[(triple5)]
("cat" "sees" "bear" "-")
triple5
The cat does not like the squirrel.
False
1
inv-proof
[(triple4)]
("cat" "likes" "squirrel" "-")
triple4
The cow is rough.
True
2
proof
[(((triple3) -> rule3))]
("cow" "is" "rough" "+")
((triple3) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is not rough.
False
2
inv-proof
[(((triple3) -> rule3))]
("cow" "is" "rough" "-")
((triple3) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is not young.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("cow" "is" "young" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The cow is young.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("cow" "is" "young" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The bear does not need the cat.
Unknown
inv-random
[@0: The bear needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cat" "-")
The squirrel needs the bear.
Unknown
random
[@0: The squirrel needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "bear" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The bear needs the cow.
Unknown
random
[@0: The bear needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "cow" "+")
@0: The bear does not like the squirrel.[(triple2)] The bear likes the cat.[(triple1)] The bear sees the cow.[(triple3)] The cat does not see the bear.[(triple5)] The cat likes the squirrel.[(triple4)] The cow does not need the squirrel.[(triple8)] The cow likes the bear.[(triple6)] The cow likes the squirrel.[(triple7)] The cow sees the squirrel.[(triple9)] The squirrel is not big.[(triple10)] The squirrel is young.[(triple11)] The squirrel needs the cow.[(triple12)] @1: The cow is rough.[(((triple3) -> rule3))] @2: The cow is not young.[(((((triple3) -> rule3)) -> rule2))]
The bear does not like the squirrel.
("bear" "likes" "squirrel" "-")
triple2
The bear likes the cat.
("bear" "likes" "cat" "+")
triple1
The bear sees the cow.
("bear" "sees" "cow" "+")
triple3
The cat does not see the bear.
("cat" "sees" "bear" "-")
triple5
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple4
The cow does not need the squirrel.
("cow" "needs" "squirrel" "-")
triple8
The cow likes the bear.
("cow" "likes" "bear" "+")
triple6
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple7
The cow sees the squirrel.
("cow" "sees" "squirrel" "+")
triple9
The squirrel is not big.
("squirrel" "is" "big" "-")
triple10
The squirrel is young.
("squirrel" "is" "young" "+")
triple11
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple12
The cow is rough.
("cow" "is" "rough" "+")
((triple3) -> (rule3 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The cow is not young.
("cow" "is" "young" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The cow is not young.
("cow" "is" "young" "-")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2