The bald eagle needs the lion. The bald eagle needs the mouse. The bald eagle needs the squirrel. The bald eagle sees the squirrel. The lion needs the bald eagle. The lion sees the squirrel. The mouse needs the squirrel. The squirrel is cold. The squirrel needs the lion. The squirrel sees the lion. If someone needs the bald eagle then they like the mouse. If someone is kind and rough then they see the mouse. If someone likes the mouse then the mouse is cold. If someone is cold then they need the squirrel. If someone likes the mouse then the mouse sees the squirrel. If the bald eagle needs the lion then the lion likes the mouse.
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If someone needs the bald eagle then they like the mouse.
((("someone" "needs" "bald eagle" "+")) -> ("someone" "likes" "mouse" "+"))
If someone is kind and rough then they see the mouse.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "sees" "mouse" "+"))
If someone likes the mouse then the mouse is cold.
((("someone" "likes" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If someone is cold then they need the squirrel.
((("someone" "is" "cold" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone likes the mouse then the mouse sees the squirrel.
((("someone" "likes" "mouse" "+")) -> ("mouse" "sees" "squirrel" "+"))
If the bald eagle needs the lion then the lion likes the mouse.
((("bald eagle" "needs" "lion" "+")) -> ("lion" "likes" "mouse" "+"))
The squirrel needs the lion.
True
1
proof
[(triple9)]
("squirrel" "needs" "lion" "+")
triple9
The lion does not need the bald eagle.
False
1
inv-proof
[(triple5)]
("lion" "needs" "bald eagle" "-")
triple5
The mouse does not like the mouse.
Unknown
inv-rconc
[@1: The mouse likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "mouse" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
@0: The bald eagle needs the lion.[(triple1)] The bald eagle needs the mouse.[(triple2)] The bald eagle needs the squirrel.[(triple3)] The bald eagle sees the squirrel.[(triple4)] The lion needs the bald eagle.[(triple5)] The lion sees the squirrel.[(triple6)] The mouse needs the squirrel.[(triple7 OR ((((((triple1) -> rule6)) -> rule3)) -> rule4) OR ((((((triple5) -> rule1)) -> rule3)) -> rule4))] The squirrel is cold.[(triple8)] The squirrel needs the lion.[(triple9)] The squirrel sees the lion.[(triple10)] @1: The lion likes the mouse.[(((triple1) -> rule6) OR ((triple5) -> rule1))] The squirrel needs the squirrel.[(((triple8) -> rule4))] @2: The mouse is cold.[(((((triple1) -> rule6)) -> rule3) OR ((((triple5) -> rule1)) -> rule3))] The mouse sees the squirrel.[(((((triple1) -> rule6)) -> rule5) OR ((((triple5) -> rule1)) -> rule5))]
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
triple1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
triple2
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
triple3
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
triple4
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
triple5
The lion sees the squirrel.
("lion" "sees" "squirrel" "+")
triple6
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple7
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
((((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple8
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple9
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple10
The lion likes the mouse.
("lion" "likes" "mouse" "+")
((triple1) -> (rule6 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
((triple5) -> (rule1 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple8) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int2