The bald eagle likes the mouse. The lion likes the bald eagle. The mouse needs the bald eagle. If the bald eagle visits the lion then the lion likes the mouse. If something likes the bald eagle then the bald eagle visits the lion.
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
The lion likes the bald eagle.
("lion" "likes" "bald eagle" "+")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
If the bald eagle visits the lion then the lion likes the mouse.
((("bald eagle" "visits" "lion" "+")) -> ("lion" "likes" "mouse" "+"))
If something likes the bald eagle then the bald eagle visits the lion.
((("something" "likes" "bald eagle" "+")) -> ("bald eagle" "visits" "lion" "+"))
The mouse needs the bald eagle.
True
1
proof
[(triple3)]
("mouse" "needs" "bald eagle" "+")
triple3
The mouse does not need the bald eagle.
False
1
inv-proof
[(triple3)]
("mouse" "needs" "bald eagle" "-")
triple3
The bald eagle visits the lion.
True
2
proof
[(((triple2) -> rule2))]
("bald eagle" "visits" "lion" "+")
((triple2) -> (rule2 % int1))
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int1
The bald eagle does not visit the lion.
False
2
inv-proof
[(((triple2) -> rule2))]
("bald eagle" "visits" "lion" "-")
((triple2) -> (rule2 % int1))
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int1
The lion likes the mouse.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("lion" "likes" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int2
The lion does not like the mouse.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("lion" "likes" "mouse" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int2
The bald eagle does not need the mouse.
Unknown
inv-random
[@0: The bald eagle needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "mouse" "-")
The lion needs the bald eagle.
Unknown
random
[@0: The lion needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bald eagle" "+")
The mouse does not like the mouse.
Unknown
inv-random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "-")
The mouse likes the bald eagle.
Unknown
random
[@0: The mouse likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "bald eagle" "+")
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 lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The bald eagle likes the mouse.[(triple1)] The lion likes the bald eagle.[(triple2)] The mouse needs the bald eagle.[(triple3)] @1: The bald eagle visits the lion.[(((triple2) -> rule2))] @2: The lion likes the mouse.[(((((triple2) -> rule2)) -> rule1))]
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
triple1
The lion likes the bald eagle.
("lion" "likes" "bald eagle" "+")
triple2
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple3
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
((triple2) -> (rule2 % int1))
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The lion likes the mouse.
("lion" "likes" "mouse" "+")
int1
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
int2