The cow needs the squirrel. The mouse likes the cow. The squirrel needs the cow. If someone is rough then they do not see the mouse. If someone needs the mouse then the mouse needs the cow. If the squirrel is rough and the squirrel does not see the cow then the cow is round. If someone needs the cow then the cow likes the squirrel. If the cow likes the squirrel then the squirrel needs the mouse. If someone needs the squirrel and they do not need the mouse then the mouse sees the cow.
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If someone is rough then they do not see the mouse.
((("someone" "is" "rough" "+")) -> ("someone" "sees" "mouse" "-"))
If someone needs the mouse then the mouse needs the cow.
((("someone" "needs" "mouse" "+")) -> ("mouse" "needs" "cow" "+"))
If the squirrel is rough and the squirrel does not see the cow then the cow is round.
((("squirrel" "is" "rough" "+") ("squirrel" "sees" "cow" "~")) -> ("cow" "is" "round" "+"))
If someone needs the cow then the cow likes the squirrel.
((("someone" "needs" "cow" "+")) -> ("cow" "likes" "squirrel" "+"))
If the cow likes the squirrel then the squirrel needs the mouse.
((("cow" "likes" "squirrel" "+")) -> ("squirrel" "needs" "mouse" "+"))
If someone needs the squirrel and they do not need the mouse then the mouse sees the cow.
((("someone" "needs" "squirrel" "+") ("someone" "needs" "mouse" "~")) -> ("mouse" "sees" "cow" "+"))
The mouse likes the cow.
True
1
proof
[(triple2)]
("mouse" "likes" "cow" "+")
triple2
The cow does not need the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "needs" "squirrel" "-")
triple1
The cow likes the squirrel.
True
2
proof
[(((triple3) -> rule4))]
("cow" "likes" "squirrel" "+")
((triple3) -> (rule4 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The cow does not like the squirrel.
False
2
inv-proof
[(((triple3) -> rule4))]
("cow" "likes" "squirrel" "-")
((triple3) -> (rule4 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The squirrel needs the mouse.
True
3
proof
[(((((triple3) -> rule4)) -> rule5))]
("squirrel" "needs" "mouse" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int2
The squirrel does not need the mouse.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule5))]
("squirrel" "needs" "mouse" "-")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int2
The mouse needs the cow.
True
4
proof
[(((((((triple3) -> rule4)) -> rule5)) -> rule2))]
("mouse" "needs" "cow" "+")
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int3
The mouse does not need the cow.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule5)) -> rule2))]
("mouse" "needs" "cow" "-")
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int3
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "round" "-")
The mouse sees the cow.
Unknown
rconc
[@1: The mouse sees the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "sees" "cow" "+")
The squirrel does not like the cow.
Unknown
inv-random
[@0: The squirrel likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "cow" "-")
The mouse needs the mouse.
Unknown
random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The cow needs the squirrel.[(triple1)] The mouse likes the cow.[(triple2)] The squirrel needs the cow.[(triple3)] @1: The cow likes the squirrel.[(((triple3) -> rule4))] @2: The squirrel needs the mouse.[(((((triple3) -> rule4)) -> rule5))] @3: The mouse needs the cow.[(((((((triple3) -> rule4)) -> rule5)) -> rule2))]
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple3
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
((triple3) -> (rule4 % int1))
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
((((triple3) -> (rule4 % int2))) -> (rule5 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int2
The mouse needs the cow.
("mouse" "needs" "cow" "+")
((((((triple3) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The mouse needs the cow.
("mouse" "needs" "cow" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
int3