The bald eagle chases the lion. The bald eagle chases the mouse. The bald eagle visits the lion. The lion is red. The lion visits the mouse. The mouse chases the bald eagle. The mouse chases the lion. The mouse chases the squirrel. The mouse eats the bald eagle. The mouse is red. The mouse visits the bald eagle. The mouse visits the lion. The mouse visits the squirrel. The squirrel chases the mouse. The squirrel eats the lion. The squirrel visits the lion. If something visits the squirrel then it eats the bald eagle. If something visits the mouse then it visits the squirrel. If something is red and it eats the squirrel then it chases the squirrel.
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
The lion is red.
("lion" "is" "red" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something visits the squirrel then it eats the bald eagle.
((("something" "visits" "squirrel" "+")) -> ("something" "eats" "bald eagle" "+"))
If something visits the mouse then it visits the squirrel.
((("something" "visits" "mouse" "+")) -> ("something" "visits" "squirrel" "+"))
If something is red and it eats the squirrel then it chases the squirrel.
((("something" "is" "red" "+") ("something" "eats" "squirrel" "+")) -> ("something" "chases" "squirrel" "+"))
The lion is red.
True
1
proof
[(triple4)]
("lion" "is" "red" "+")
triple4
The lion does not visit the mouse.
False
1
inv-proof
[(triple5)]
("lion" "visits" "mouse" "-")
triple5
The lion visits the squirrel.
True
2
proof
[(((triple5) -> rule2))]
("lion" "visits" "squirrel" "+")
((triple5) -> (rule2 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion does not visit the squirrel.
False
2
inv-proof
[(((triple5) -> rule2))]
("lion" "visits" "squirrel" "-")
((triple5) -> (rule2 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion eats the bald eagle.
True
3
proof
[(((((triple5) -> rule2)) -> rule1))]
("lion" "eats" "bald eagle" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The lion does not eat the bald eagle.
False
3
inv-proof
[(((((triple5) -> rule2)) -> rule1))]
("lion" "eats" "bald eagle" "-")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2
The bald eagle does not chase the squirrel.
Unknown
inv-rconc
[@1: The bald eagle chases the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "chases" "squirrel" "-")
The bald eagle eats the bald eagle.
Unknown
rconc
[@2: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
The lion does not chase the squirrel.
Unknown
inv-rconc
[@1: The lion chases the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "chases" "squirrel" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The bald eagle chases the lion.[(triple1)] The bald eagle chases the mouse.[(triple2)] The bald eagle visits the lion.[(triple3)] The lion is red.[(triple4)] The lion visits the mouse.[(triple5)] The mouse chases the bald eagle.[(triple6)] The mouse chases the lion.[(triple7)] The mouse chases the squirrel.[(triple8)] The mouse eats the bald eagle.[(triple9 OR ((triple13) -> rule1))] The mouse is red.[(triple10)] The mouse visits the bald eagle.[(triple11)] The mouse visits the lion.[(triple12)] The mouse visits the squirrel.[(triple13)] The squirrel chases the mouse.[(triple14)] The squirrel eats the lion.[(triple15)] The squirrel visits the lion.[(triple16)] @1: The lion visits the squirrel.[(((triple5) -> rule2))] @2: The lion eats the bald eagle.[(((((triple5) -> rule2)) -> rule1))]
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
triple1
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
triple2
The bald eagle visits the lion.
("bald eagle" "visits" "lion" "+")
triple3
The lion is red.
("lion" "is" "red" "+")
triple4
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple5
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
triple6
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple7
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple8
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
triple9
((triple13) -> (rule1 % int1))
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
triple10
The mouse visits the bald eagle.
("mouse" "visits" "bald eagle" "+")
triple11
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple12
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple13
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple14
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple15
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple16
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
((triple5) -> (rule2 % int1))
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int1
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
((((triple5) -> (rule2 % int2))) -> (rule1 % int1))
The lion eats the bald eagle.
("lion" "eats" "bald eagle" "+")
int1
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
int2