The bald eagle chases the mouse. The bald eagle is kind. The bald eagle visits the squirrel. The mouse needs the bald eagle. The squirrel chases the bald eagle. The squirrel needs the bald eagle. The squirrel needs the mouse. If someone needs the bald eagle then the bald eagle needs the mouse.
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
The squirrel chases the bald eagle.
("squirrel" "chases" "bald eagle" "+")
The squirrel needs the bald eagle.
("squirrel" "needs" "bald eagle" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If someone needs the bald eagle then the bald eagle needs the mouse.
((("someone" "needs" "bald eagle" "+")) -> ("bald eagle" "needs" "mouse" "+"))
The mouse needs the bald eagle.
True
1
proof
[(triple4)]
("mouse" "needs" "bald eagle" "+")
triple4
The mouse does not need the bald eagle.
False
1
inv-proof
[(triple4)]
("mouse" "needs" "bald eagle" "-")
triple4
The bald eagle needs the mouse.
True
2
proof
[(((triple4) -> rule1) OR ((triple6) -> rule1))]
("bald eagle" "needs" "mouse" "+")
((triple4) -> (rule1 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
((triple6) -> (rule1 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The bald eagle does not need the mouse.
False
2
inv-proof
[(((triple4) -> rule1) OR ((triple6) -> rule1))]
("bald eagle" "needs" "mouse" "-")
((triple4) -> (rule1 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
((triple6) -> (rule1 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The mouse chases the squirrel.
Unknown
random
[@0: The mouse chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "squirrel" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The bald eagle chases the bald eagle.
Unknown
random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "+")
@0: The bald eagle chases the mouse.[(triple1)] The bald eagle is kind.[(triple2)] The bald eagle visits the squirrel.[(triple3)] The mouse needs the bald eagle.[(triple4)] The squirrel chases the bald eagle.[(triple5)] The squirrel needs the bald eagle.[(triple6)] The squirrel needs the mouse.[(triple7)] @1: The bald eagle needs the mouse.[(((triple4) -> rule1) OR ((triple6) -> rule1))]
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
triple1
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple2
The bald eagle visits the squirrel.
("bald eagle" "visits" "squirrel" "+")
triple3
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple4
The squirrel chases the bald eagle.
("squirrel" "chases" "bald eagle" "+")
triple5
The squirrel needs the bald eagle.
("squirrel" "needs" "bald eagle" "+")
triple6
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple7
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
((triple4) -> (rule1 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
((triple6) -> (rule1 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1