The bald eagle likes the mouse. The mouse visits the bald eagle. The tiger likes the bald eagle. If the bald eagle likes the tiger then the tiger visits the bald eagle. If something likes the tiger and the tiger is not cold then the tiger likes the bald eagle. If something is round then it sees the mouse.
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
If the bald eagle likes the tiger then the tiger visits the bald eagle.
((("bald eagle" "likes" "tiger" "+")) -> ("tiger" "visits" "bald eagle" "+"))
If something likes the tiger and the tiger is not cold then the tiger likes the bald eagle.
((("something" "likes" "tiger" "+") ("tiger" "is" "cold" "~")) -> ("tiger" "likes" "bald eagle" "+"))
If something is round then it sees the mouse.
((("something" "is" "round" "+")) -> ("something" "sees" "mouse" "+"))
The tiger likes the bald eagle.
True
1
proof
[(triple3)]
("tiger" "likes" "bald eagle" "+")
triple3
The bald eagle does not like the mouse.
False
1
inv-proof
[(triple1)]
("bald eagle" "likes" "mouse" "-")
triple1
The tiger does not see the mouse.
Unknown
inv-rconc
[@1: The tiger sees the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "sees" "mouse" "-")
The tiger visits the mouse.
Unknown
random
[@0: The tiger visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "mouse" "+")
@0: The bald eagle likes the mouse.[(triple1)] The mouse visits the bald eagle.[(triple2)] The tiger likes the bald eagle.[(triple3)]
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
triple1
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
triple2
The tiger likes the bald eagle.
("tiger" "likes" "bald eagle" "+")
triple3