The bald eagle is cold. The bald eagle is not green. The bear is not round. The mouse chases the bald eagle. The mouse chases the squirrel. The mouse is green. The mouse is young. The mouse sees the bear. The squirrel chases the mouse. The squirrel needs the mouse. If something is young then it does not see the bald eagle. If something needs the squirrel then the squirrel chases the bear. If something chases the bald eagle then the bald eagle is not young. If the bald eagle chases the bear and the bald eagle is not young then the bear does not see the bald eagle. If something needs the mouse then it sees the squirrel. If something needs the mouse then the mouse does not see the squirrel. If something is green and it does not see the bald eagle then the bald eagle needs the mouse. If something needs the mouse and it is not cold then the mouse is green.
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
The bald eagle is not green.
("bald eagle" "is" "green" "-")
The bear is not round.
("bear" "is" "round" "-")
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the bear.
("mouse" "sees" "bear" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If something is young then it does not see the bald eagle.
((("something" "is" "young" "+")) -> ("something" "sees" "bald eagle" "-"))
If something needs the squirrel then the squirrel chases the bear.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "chases" "bear" "+"))
If something chases the bald eagle then the bald eagle is not young.
((("something" "chases" "bald eagle" "+")) -> ("bald eagle" "is" "young" "-"))
If the bald eagle chases the bear and the bald eagle is not young then the bear does not see the bald eagle.
((("bald eagle" "chases" "bear" "+") ("bald eagle" "is" "young" "~")) -> ("bear" "sees" "bald eagle" "-"))
If something needs the mouse then it sees the squirrel.
((("something" "needs" "mouse" "+")) -> ("something" "sees" "squirrel" "+"))
If something needs the mouse then the mouse does not see the squirrel.
((("something" "needs" "mouse" "+")) -> ("mouse" "sees" "squirrel" "-"))
If something is green and it does not see the bald eagle then the bald eagle needs the mouse.
((("something" "is" "green" "+") ("something" "sees" "bald eagle" "~")) -> ("bald eagle" "needs" "mouse" "+"))
If something needs the mouse and it is not cold then the mouse is green.
((("something" "needs" "mouse" "+") ("something" "is" "cold" "~")) -> ("mouse" "is" "green" "+"))
The bald eagle is not green.
True
1
proof
[(triple2)]
("bald eagle" "is" "green" "-")
triple2
The mouse does not see the bear.
False
1
inv-proof
[(triple8)]
("mouse" "sees" "bear" "-")
triple8
The mouse does not see the squirrel.
True
2
proof
[(((triple10) -> rule6) OR ((((triple6 ((triple7) -> rule1)) -> rule7)) -> rule6))]
("mouse" "sees" "squirrel" "-")
((triple10) -> (rule6 % int1))
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
int1
((((triple6 ((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int2
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
int3
The mouse sees the bald eagle.
False
2
inv-proof
[(((triple7) -> rule1))]
("mouse" "sees" "bald eagle" "+")
((triple7) -> (rule1 % int1))
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
int1
The bald eagle needs the mouse.
True
4
proof
[(((triple6 ((triple7) -> rule1)) -> rule7))]
("bald eagle" "needs" "mouse" "+")
((triple6 ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
int2
The bald eagle does not need the mouse.
False
4
inv-proof
[(((triple6 ((triple7) -> rule1)) -> rule7))]
("bald eagle" "needs" "mouse" "-")
((triple6 ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
int2
The bald eagle sees the squirrel.
True
5
proof
[(((((triple6 ((triple7) -> rule1)) -> rule7)) -> rule5))]
("bald eagle" "sees" "squirrel" "+")
((((triple6 ((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int2
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
int3
The bald eagle does not see the squirrel.
False
5
inv-proof
[(((((triple6 ((triple7) -> rule1)) -> rule7)) -> rule5))]
("bald eagle" "sees" "squirrel" "-")
((((triple6 ((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int2
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
int3
The squirrel does not chase the bear.
Unknown
inv-rconc
[@1: The squirrel chases the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "bear" "-")
The bear sees the squirrel.
Unknown
rconc
[@1: The bear sees the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "sees" "squirrel" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The mouse needs the bear.
Unknown
random
[@0: The mouse needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "bear" "+")
The mouse is not round.
Unknown
inv-random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "-")
The bald eagle sees the bear.
Unknown
random
[@0: The bald eagle sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bear" "+")
The bear does not see the mouse.
Unknown
inv-random
[@0: The bear sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "mouse" "-")
The squirrel needs the bear.
Unknown
random
[@0: The squirrel needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "bear" "+")
@0: The bald eagle is cold.[(triple1)] The bald eagle is not green.[(triple2)] The bear is not round.[(triple3)] The mouse chases the bald eagle.[(triple4)] The mouse chases the squirrel.[(triple5)] The mouse is green.[(triple6)] The mouse is young.[(triple7)] The mouse sees the bear.[(triple8)] The squirrel chases the mouse.[(triple9)] The squirrel needs the mouse.[(triple10)] @1: The bald eagle is not young.[(((triple4) -> rule3))] The mouse does not see the bald eagle.[(((triple7) -> rule1))] The mouse does not see the squirrel.[(((triple10) -> rule6) OR ((((triple6 ((triple7) -> rule1)) -> rule7)) -> rule6))] The squirrel sees the squirrel.[(((triple10) -> rule5))] @2: The bald eagle needs the mouse.[(((triple6 ((triple7) -> rule1)) -> rule7))] @3: The bald eagle sees the squirrel.[(((((triple6 ((triple7) -> rule1)) -> rule7)) -> rule5))]
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
triple1
The bald eagle is not green.
("bald eagle" "is" "green" "-")
triple2
The bear is not round.
("bear" "is" "round" "-")
triple3
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
triple4
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple6
The mouse is young.
("mouse" "is" "young" "+")
triple7
The mouse sees the bear.
("mouse" "sees" "bear" "+")
triple8
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple9
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple10
The bald eagle is not young.
("bald eagle" "is" "young" "-")
((triple4) -> (rule3 % int1))
The bald eagle is not young.
("bald eagle" "is" "young" "-")
int1
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
((triple7) -> (rule1 % int1))
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
int1
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
((triple10) -> (rule6 % int1))
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
int1
((((triple6 ((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int2
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
int3
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple10) -> (rule5 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
((triple6 ((triple7) -> (rule1 % int2))) -> (rule7 % int1))
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int1
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
int2
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
((((triple6 ((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bald eagle sees the squirrel.
("bald eagle" "sees" "squirrel" "+")
int1
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
int2
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
int3