The bald eagle chases the mouse. The bald eagle is green. The bald eagle is kind. The lion chases the mouse. The lion is kind. The lion needs the mouse. The lion sees the bald eagle. The lion sees the mouse. The mouse is not green. The mouse is rough. The mouse needs the bald eagle. The mouse sees the squirrel. The squirrel is cold. The squirrel needs the mouse. The squirrel sees the lion. If something sees the bald eagle then it is green. If something needs the lion then the lion chases the bald eagle. If something is green then it needs the squirrel.
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
The bald eagle is green.
("bald eagle" "is" "green" "+")
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If something sees the bald eagle then it is green.
((("something" "sees" "bald eagle" "+")) -> ("something" "is" "green" "+"))
If something needs the lion then the lion chases the bald eagle.
((("something" "needs" "lion" "+")) -> ("lion" "chases" "bald eagle" "+"))
If something is green then it needs the squirrel.
((("something" "is" "green" "+")) -> ("something" "needs" "squirrel" "+"))
The mouse is rough.
True
1
proof
[(triple10)]
("mouse" "is" "rough" "+")
triple10
The lion does not see the mouse.
False
1
inv-proof
[(triple8)]
("lion" "sees" "mouse" "-")
triple8
The bald eagle needs the squirrel.
True
2
proof
[(((triple2) -> rule3))]
("bald eagle" "needs" "squirrel" "+")
((triple2) -> (rule3 % int1))
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
int1
The lion is not green.
False
2
inv-proof
[(((triple7) -> rule1))]
("lion" "is" "green" "-")
((triple7) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the squirrel.
True
3
proof
[(((((triple7) -> rule1)) -> rule3))]
("lion" "needs" "squirrel" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion does not need the squirrel.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule3))]
("lion" "needs" "squirrel" "-")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The mouse does not need the squirrel.
Unknown
inv-rconc
[@1: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "needs" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
rconc
[@2: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel is not green.
Unknown
inv-rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "green" "-")
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 squirrel does not chase the mouse.
Unknown
inv-random
[@0: The squirrel chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "mouse" "-")
The bald eagle is rough.
Unknown
random
[@0: The bald eagle is rough.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "rough" "+")
@0: The bald eagle chases the mouse.[(triple1)] The bald eagle is green.[(triple2)] The bald eagle is kind.[(triple3)] The lion chases the mouse.[(triple4)] The lion is kind.[(triple5)] The lion needs the mouse.[(triple6)] The lion sees the bald eagle.[(triple7)] The lion sees the mouse.[(triple8)] The mouse is not green.[(triple9)] The mouse is rough.[(triple10)] The mouse needs the bald eagle.[(triple11)] The mouse sees the squirrel.[(triple12)] The squirrel is cold.[(triple13)] The squirrel needs the mouse.[(triple14)] The squirrel sees the lion.[(triple15)] @1: The bald eagle needs the squirrel.[(((triple2) -> rule3))] The lion is green.[(((triple7) -> rule1))] @2: The lion needs the squirrel.[(((((triple7) -> rule1)) -> rule3))]
The bald eagle chases the mouse.
("bald eagle" "chases" "mouse" "+")
triple1
The bald eagle is green.
("bald eagle" "is" "green" "+")
triple2
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple3
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple4
The lion is kind.
("lion" "is" "kind" "+")
triple5
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple6
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
triple7
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple8
The mouse is not green.
("mouse" "is" "green" "-")
triple9
The mouse is rough.
("mouse" "is" "rough" "+")
triple10
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple11
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple12
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple13
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple14
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple15
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
((triple2) -> (rule3 % int1))
The bald eagle needs the squirrel.
("bald eagle" "needs" "squirrel" "+")
int1
The lion is green.
("lion" "is" "green" "+")
((triple7) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
((((triple7) -> (rule1 % int2))) -> (rule3 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2