The bald eagle does not need the mouse. The bald eagle does not see the cow. The cow chases the bald eagle. The cow chases the rabbit. The cow is cold. The cow is green. The cow does not need the mouse. The mouse chases the bald eagle. The mouse is green. The mouse is red. The mouse sees the cow. The mouse sees the rabbit. The rabbit needs the cow. The rabbit needs the mouse. The rabbit sees the bald eagle. If the cow is red and the cow is big then the cow is green. If something needs the rabbit then it does not see the mouse. If the bald eagle chases the cow and the bald eagle is not green then the cow does not see the bald eagle. If something needs the mouse then it is young. If something needs the cow then it sees the bald eagle. If something chases the bald eagle and the bald eagle does not see the cow then the cow needs the rabbit.
The bald eagle does not need the mouse.
("bald eagle" "needs" "mouse" "-")
The bald eagle does not see the cow.
("bald eagle" "sees" "cow" "-")
The cow chases the bald eagle.
("cow" "chases" "bald eagle" "+")
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
If the cow is red and the cow is big then the cow is green.
((("cow" "is" "red" "+") ("cow" "is" "big" "+")) -> ("cow" "is" "green" "+"))
If something needs the rabbit then it does not see the mouse.
((("something" "needs" "rabbit" "+")) -> ("something" "sees" "mouse" "-"))
If the bald eagle chases the cow and the bald eagle is not green then the cow does not see the bald eagle.
((("bald eagle" "chases" "cow" "+") ("bald eagle" "is" "green" "~")) -> ("cow" "sees" "bald eagle" "-"))
If something needs the mouse then it is young.
((("something" "needs" "mouse" "+")) -> ("something" "is" "young" "+"))
If something needs the cow then it sees the bald eagle.
((("something" "needs" "cow" "+")) -> ("something" "sees" "bald eagle" "+"))
If something chases the bald eagle and the bald eagle does not see the cow then the cow needs the rabbit.
((("something" "chases" "bald eagle" "+") ("bald eagle" "sees" "cow" "~")) -> ("cow" "needs" "rabbit" "+"))
The mouse sees the rabbit.
True
1
proof
[(triple12)]
("mouse" "sees" "rabbit" "+")
triple12
The cow does not chase the rabbit.
False
1
inv-proof
[(triple4)]
("cow" "chases" "rabbit" "-")
triple4
The cow needs the rabbit.
True
3
proof
[(((triple3 triple2) -> rule6) OR ((triple8 triple2) -> rule6))]
("cow" "needs" "rabbit" "+")
((triple3 triple2) -> (rule6 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
((triple8 triple2) -> (rule6 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow does not need the rabbit.
False
3
inv-proof
[(((triple3 triple2) -> rule6) OR ((triple8 triple2) -> rule6))]
("cow" "needs" "rabbit" "-")
((triple3 triple2) -> (rule6 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
((triple8 triple2) -> (rule6 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow does not see the mouse.
True
4
proof
[(((((triple3 triple2) -> rule6)) -> rule2) OR ((((triple8 triple2) -> rule6)) -> rule2))]
("cow" "sees" "mouse" "-")
((((triple3 triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
((((triple8 triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The cow sees the mouse.
False
4
inv-proof
[(((((triple3 triple2) -> rule6)) -> rule2) OR ((((triple8 triple2) -> rule6)) -> rule2))]
("cow" "sees" "mouse" "+")
((((triple3 triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
((((triple8 triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "young" "-")
The mouse sees the bald eagle.
Unknown
rconc
[@1: The mouse sees the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "sees" "bald eagle" "+")
The bald eagle does not see the bald eagle.
Unknown
inv-rconc
[@1: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "sees" "bald eagle" "-")
The bald eagle is cold.
Unknown
random
[@0: The bald eagle is cold.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "cold" "+")
The bald eagle does not chase the mouse.
Unknown
inv-random
[@0: The bald eagle chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "mouse" "-")
The mouse needs the rabbit.
Unknown
random
[@0: The mouse needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "rabbit" "+")
@0: The bald eagle does not need the mouse.[(triple1)] The bald eagle does not see the cow.[(triple2)] The cow chases the bald eagle.[(triple3)] The cow chases the rabbit.[(triple4)] The cow does not need the mouse.[(triple7)] The cow is cold.[(triple5)] The cow is green.[(triple6)] The mouse chases the bald eagle.[(triple8)] The mouse is green.[(triple9)] The mouse is red.[(triple10)] The mouse sees the cow.[(triple11)] The mouse sees the rabbit.[(triple12)] The rabbit needs the cow.[(triple13)] The rabbit needs the mouse.[(triple14)] The rabbit sees the bald eagle.[(triple15 OR ((triple13) -> rule5))] @1: The cow needs the rabbit.[(((triple3 triple2) -> rule6) OR ((triple8 triple2) -> rule6))] The rabbit is young.[(((triple14) -> rule4))] @2: The cow does not see the mouse.[(((((triple3 triple2) -> rule6)) -> rule2) OR ((((triple8 triple2) -> rule6)) -> rule2))]
The bald eagle does not need the mouse.
("bald eagle" "needs" "mouse" "-")
triple1
The bald eagle does not see the cow.
("bald eagle" "sees" "cow" "-")
triple2
The cow chases the bald eagle.
("cow" "chases" "bald eagle" "+")
triple3
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple4
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
triple7
The cow is cold.
("cow" "is" "cold" "+")
triple5
The cow is green.
("cow" "is" "green" "+")
triple6
The mouse chases the bald eagle.
("mouse" "chases" "bald eagle" "+")
triple8
The mouse is green.
("mouse" "is" "green" "+")
triple9
The mouse is red.
("mouse" "is" "red" "+")
triple10
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple11
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple12
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple13
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple14
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
triple15
((triple13) -> (rule5 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
((triple3 triple2) -> (rule6 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
((triple8 triple2) -> (rule6 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((triple14) -> (rule4 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
((((triple3 triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
((((triple8 triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow does not see the mouse.
("cow" "sees" "mouse" "-")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2