The bald eagle is cold. The bald eagle is rough. The bald eagle sees the lion. The lion chases the mouse. The lion is rough. The lion needs the bald eagle. The lion sees the mouse. The mouse needs the bald eagle. The mouse sees the bald eagle. The mouse sees the lion. If something sees the mouse and the mouse chases the bald eagle then the mouse needs the bald eagle. If something sees the mouse then it is rough. If something is young and it needs the mouse then the mouse chases the bald eagle.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
If something sees the mouse and the mouse chases the bald eagle then the mouse needs the bald eagle.
((("something" "sees" "mouse" "+") ("mouse" "chases" "bald eagle" "+")) -> ("mouse" "needs" "bald eagle" "+"))
If something sees the mouse then it is rough.
((("something" "sees" "mouse" "+")) -> ("something" "is" "rough" "+"))
If something is young and it needs the mouse then the mouse chases the bald eagle.
((("something" "is" "young" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "chases" "bald eagle" "+"))
The mouse needs the bald eagle.
True
1
proof
[(triple8)]
("mouse" "needs" "bald eagle" "+")
triple8
The bald eagle does not see the lion.
False
1
inv-proof
[(triple3)]
("bald eagle" "sees" "lion" "-")
triple3
The mouse does not chase the bald eagle.
Unknown
inv-rconc
[@1: The mouse chases the bald eagle.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "bald eagle" "-")
The mouse chases the lion.
Unknown
random
[@0: The mouse chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "lion" "+")
@0: The bald eagle is cold.[(triple1)] The bald eagle is rough.[(triple2)] The bald eagle sees the lion.[(triple3)] The lion chases the mouse.[(triple4)] The lion is rough.[(triple5 OR ((triple7) -> rule2))] The lion needs the bald eagle.[(triple6)] The lion sees the mouse.[(triple7)] The mouse needs the bald eagle.[(triple8)] The mouse sees the bald eagle.[(triple9)] The mouse sees the lion.[(triple10)]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple2
The bald eagle sees the lion.
("bald eagle" "sees" "lion" "+")
triple3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
((triple7) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
triple6
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple7
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple8
The mouse sees the bald eagle.
("mouse" "sees" "bald eagle" "+")
triple9
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple10