The bald eagle eats the mouse. The bald eagle is big. The bald eagle is red. The bald eagle needs the cow. The bald eagle does not see the cow. The bald eagle does not see the mouse. The cow does not need the mouse. The cow sees the bald eagle. The mouse needs the bald eagle. The mouse needs the cow. The mouse does not see the bald eagle. The mouse sees the cow. If something sees the mouse and the mouse eats the bald eagle then the bald eagle eats the cow. If the cow is big then the cow does not need the mouse. If something needs the bald eagle then the bald eagle is cold. If the cow eats the mouse and the cow eats the bald eagle then the mouse does not eat the cow. If something eats the bald eagle then it eats the mouse. If something sees the bald eagle then it eats the bald eagle. If something eats the cow and the cow is blue then the cow sees the mouse. If something eats the bald eagle and it does not eat the cow then the bald eagle eats the mouse.
The bald eagle eats the mouse.
("bald eagle" "eats" "mouse" "+")
The bald eagle is big.
("bald eagle" "is" "big" "+")
The bald eagle is red.
("bald eagle" "is" "red" "+")
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
The bald eagle does not see the cow.
("bald eagle" "sees" "cow" "-")
The bald eagle does not see the mouse.
("bald eagle" "sees" "mouse" "-")
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
If something sees the mouse and the mouse eats the bald eagle then the bald eagle eats the cow.
((("something" "sees" "mouse" "+") ("mouse" "eats" "bald eagle" "+")) -> ("bald eagle" "eats" "cow" "+"))
If the cow is big then the cow does not need the mouse.
((("cow" "is" "big" "+")) -> ("cow" "needs" "mouse" "-"))
If something needs the bald eagle then the bald eagle is cold.
((("something" "needs" "bald eagle" "+")) -> ("bald eagle" "is" "cold" "+"))
If the cow eats the mouse and the cow eats the bald eagle then the mouse does not eat the cow.
((("cow" "eats" "mouse" "+") ("cow" "eats" "bald eagle" "+")) -> ("mouse" "eats" "cow" "-"))
If something eats the bald eagle then it eats the mouse.
((("something" "eats" "bald eagle" "+")) -> ("something" "eats" "mouse" "+"))
If something sees the bald eagle then it eats the bald eagle.
((("something" "sees" "bald eagle" "+")) -> ("something" "eats" "bald eagle" "+"))
If something eats the cow and the cow is blue then the cow sees the mouse.
((("something" "eats" "cow" "+") ("cow" "is" "blue" "+")) -> ("cow" "sees" "mouse" "+"))
If something eats the bald eagle and it does not eat the cow then the bald eagle eats the mouse.
((("something" "eats" "bald eagle" "+") ("something" "eats" "cow" "~")) -> ("bald eagle" "eats" "mouse" "+"))
The bald eagle is big.
True
1
proof
[(triple2)]
("bald eagle" "is" "big" "+")
triple2
The cow does not see the bald eagle.
False
1
inv-proof
[(triple8)]
("cow" "sees" "bald eagle" "-")
triple8
The bald eagle is cold.
True
2
proof
[(((triple9) -> rule3))]
("bald eagle" "is" "cold" "+")
((triple9) -> (rule3 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle is not cold.
False
2
inv-proof
[(((triple9) -> rule3))]
("bald eagle" "is" "cold" "-")
((triple9) -> (rule3 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The cow eats the mouse.
True
3
proof
[(((((triple8) -> rule6)) -> rule5))]
("cow" "eats" "mouse" "+")
((((triple8) -> (rule6 % int2))) -> (rule5 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
int2
The cow does not eat the mouse.
False
3
inv-proof
[(((((triple8) -> rule6)) -> rule5))]
("cow" "eats" "mouse" "-")
((((triple8) -> (rule6 % int2))) -> (rule5 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
int2
The mouse does not eat the cow.
True
6
proof
[(((((((triple8) -> rule6)) -> rule5) ((triple8) -> rule6)) -> rule4))]
("mouse" "eats" "cow" "-")
((((((triple8) -> (rule6 % int3))) -> (rule5 % int2)) ((triple8) -> (rule6 % int3))) -> (rule4 % int1))
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
int3
The mouse eats the cow.
False
6
inv-proof
[(((((((triple8) -> rule6)) -> rule5) ((triple8) -> rule6)) -> rule4))]
("mouse" "eats" "cow" "+")
((((((triple8) -> (rule6 % int3))) -> (rule5 % int2)) ((triple8) -> (rule6 % int3))) -> (rule4 % int1))
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
int3
The mouse does not eat the bald eagle.
Unknown
inv-rconc
[@1: The mouse eats the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "bald eagle" "-")
The cow sees the mouse.
Unknown
rconc
[@1: The cow sees the mouse.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "sees" "mouse" "+")
The bald eagle does not eat the cow.
Unknown
inv-rconc
[@2: The bald eagle eats the cow.[CWA. Example of deepest failure = (rule1 <- rule7 <- FAIL)]]
("bald eagle" "eats" "cow" "-")
The bald eagle eats the bald eagle.
Unknown
rconc
[@1: The bald eagle eats the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "eats" "bald eagle" "+")
The mouse is not cold.
Unknown
inv-random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The bald eagle does not see the cow.[(triple5)] The bald eagle does not see the mouse.[(triple6)] The bald eagle eats the mouse.[(triple1)] The bald eagle is big.[(triple2)] The bald eagle is red.[(triple3)] The bald eagle needs the cow.[(triple4)] The cow does not need the mouse.[(triple7)] The cow sees the bald eagle.[(triple8)] The mouse does not see the bald eagle.[(triple11)] The mouse needs the bald eagle.[(triple9)] The mouse needs the cow.[(triple10)] The mouse sees the cow.[(triple12)] @1: The bald eagle is cold.[(((triple9) -> rule3))] The cow eats the bald eagle.[(((triple8) -> rule6))] @2: The cow eats the mouse.[(((((triple8) -> rule6)) -> rule5))] @3: The mouse does not eat the cow.[(((((((triple8) -> rule6)) -> rule5) ((triple8) -> rule6)) -> rule4))]
The bald eagle does not see the cow.
("bald eagle" "sees" "cow" "-")
triple5
The bald eagle does not see the mouse.
("bald eagle" "sees" "mouse" "-")
triple6
The bald eagle eats the mouse.
("bald eagle" "eats" "mouse" "+")
triple1
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple2
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple3
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
triple4
The cow does not need the mouse.
("cow" "needs" "mouse" "-")
triple7
The cow sees the bald eagle.
("cow" "sees" "bald eagle" "+")
triple8
The mouse does not see the bald eagle.
("mouse" "sees" "bald eagle" "-")
triple11
The mouse needs the bald eagle.
("mouse" "needs" "bald eagle" "+")
triple9
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple10
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple12
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
((triple9) -> (rule3 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
((triple8) -> (rule6 % int1))
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
((((triple8) -> (rule6 % int2))) -> (rule5 % int1))
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int1
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
int2
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
((((((triple8) -> (rule6 % int3))) -> (rule5 % int2)) ((triple8) -> (rule6 % int3))) -> (rule4 % int1))
The mouse does not eat the cow.
("mouse" "eats" "cow" "-")
int1
The cow eats the mouse.
("cow" "eats" "mouse" "+")
int2
The cow eats the bald eagle.
("cow" "eats" "bald eagle" "+")
int3