The bear sees the mouse. The bear sees the squirrel. The cow is cold. The cow is red. The cow likes the squirrel. The cow needs the mouse. The cow needs the squirrel. The mouse likes the cow. The mouse needs the cow. The mouse sees the bear. The squirrel likes the cow. The squirrel needs the mouse. If the squirrel is red and the squirrel sees the cow then the cow is not round. If someone sees the bear and they need the bear then they like the squirrel. If someone needs the bear then the bear needs the squirrel. If someone sees the squirrel and the squirrel needs the cow then the squirrel needs the bear. If someone likes the cow then they like the mouse. If someone sees the bear then they need the bear.
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is red.
("cow" "is" "red" "+")
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If the squirrel is red and the squirrel sees the cow then the cow is not round.
((("squirrel" "is" "red" "+") ("squirrel" "sees" "cow" "+")) -> ("cow" "is" "round" "-"))
If someone sees the bear and they need the bear then they like the squirrel.
((("someone" "sees" "bear" "+") ("someone" "needs" "bear" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone needs the bear then the bear needs the squirrel.
((("someone" "needs" "bear" "+")) -> ("bear" "needs" "squirrel" "+"))
If someone sees the squirrel and the squirrel needs the cow then the squirrel needs the bear.
((("someone" "sees" "squirrel" "+") ("squirrel" "needs" "cow" "+")) -> ("squirrel" "needs" "bear" "+"))
If someone likes the cow then they like the mouse.
((("someone" "likes" "cow" "+")) -> ("someone" "likes" "mouse" "+"))
If someone sees the bear then they need the bear.
((("someone" "sees" "bear" "+")) -> ("someone" "needs" "bear" "+"))
The mouse needs the cow.
True
1
proof
[(triple9)]
("mouse" "needs" "cow" "+")
triple9
The cow is not cold.
False
1
inv-proof
[(triple3)]
("cow" "is" "cold" "-")
triple3
The mouse needs the bear.
True
2
proof
[(((triple10) -> rule6))]
("mouse" "needs" "bear" "+")
((triple10) -> (rule6 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse does not need the bear.
False
2
inv-proof
[(((triple10) -> rule6))]
("mouse" "needs" "bear" "-")
((triple10) -> (rule6 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The bear needs the squirrel.
True
3
proof
[(((((triple10) -> rule6)) -> rule3))]
("bear" "needs" "squirrel" "+")
((((triple10) -> (rule6 % int2))) -> (rule3 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse does not like the squirrel.
False
4
inv-proof
[(((triple10 ((triple10) -> rule6)) -> rule2))]
("mouse" "likes" "squirrel" "-")
((triple10 ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The squirrel does not need the bear.
Unknown
inv-rconc
[@1: The squirrel needs the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "bear" "-")
The bear likes the squirrel.
Unknown
rconc
[@1: The bear likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "squirrel" "+")
The cow does not like the mouse.
Unknown
inv-rconc
[@1: The cow likes the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "likes" "mouse" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The mouse does not see the cow.
Unknown
inv-random
[@0: The mouse sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cow" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
@0: The bear sees the mouse.[(triple1)] The bear sees the squirrel.[(triple2)] The cow is cold.[(triple3)] The cow is red.[(triple4)] The cow likes the squirrel.[(triple5)] The cow needs the mouse.[(triple6)] The cow needs the squirrel.[(triple7)] The mouse likes the cow.[(triple8)] The mouse needs the cow.[(triple9)] The mouse sees the bear.[(triple10)] The squirrel likes the cow.[(triple11)] The squirrel needs the mouse.[(triple12)] @1: The mouse likes the mouse.[(((triple8) -> rule5))] The mouse needs the bear.[(((triple10) -> rule6))] The squirrel likes the mouse.[(((triple11) -> rule5))] @2: The bear needs the squirrel.[(((((triple10) -> rule6)) -> rule3))] The mouse likes the squirrel.[(((triple10 ((triple10) -> rule6)) -> rule2))]
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple1
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple2
The cow is cold.
("cow" "is" "cold" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple5
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple6
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple7
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple8
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple9
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple10
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple11
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple12
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple8) -> (rule5 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((triple10) -> (rule6 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
((triple11) -> (rule5 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((((triple10) -> (rule6 % int2))) -> (rule3 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
((triple10 ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2