The bald eagle is rough. The cow chases the mouse. The lion likes the mouse. The mouse likes the bald eagle. If something eats the lion then the lion does not like the bald eagle. If something likes the mouse and it likes the bald eagle then the mouse likes the lion. If something chases the mouse then it eats the lion. If the bald eagle likes the cow and the bald eagle eats the cow then the cow likes the mouse. If something chases the lion and the lion eats the cow then the cow eats the bald eagle. If something is red then it eats the cow. If the lion is red then the lion eats the cow. If the cow eats the lion and the cow chases the mouse then the mouse is red.
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The cow chases the mouse.
("cow" "chases" "mouse" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
If something eats the lion then the lion does not like the bald eagle.
((("something" "eats" "lion" "+")) -> ("lion" "likes" "bald eagle" "-"))
If something likes the mouse and it likes the bald eagle then the mouse likes the lion.
((("something" "likes" "mouse" "+") ("something" "likes" "bald eagle" "+")) -> ("mouse" "likes" "lion" "+"))
If something chases the mouse then it eats the lion.
((("something" "chases" "mouse" "+")) -> ("something" "eats" "lion" "+"))
If the bald eagle likes the cow and the bald eagle eats the cow then the cow likes the mouse.
((("bald eagle" "likes" "cow" "+") ("bald eagle" "eats" "cow" "+")) -> ("cow" "likes" "mouse" "+"))
If something chases the lion and the lion eats the cow then the cow eats the bald eagle.
((("something" "chases" "lion" "+") ("lion" "eats" "cow" "+")) -> ("cow" "eats" "bald eagle" "+"))
If something is red then it eats the cow.
((("something" "is" "red" "+")) -> ("something" "eats" "cow" "+"))
If the lion is red then the lion eats the cow.
((("lion" "is" "red" "+")) -> ("lion" "eats" "cow" "+"))
If the cow eats the lion and the cow chases the mouse then the mouse is red.
((("cow" "eats" "lion" "+") ("cow" "chases" "mouse" "+")) -> ("mouse" "is" "red" "+"))
The lion likes the mouse.
True
1
proof
[(triple3)]
("lion" "likes" "mouse" "+")
triple3
The cow does not chase the mouse.
False
1
inv-proof
[(triple2)]
("cow" "chases" "mouse" "-")
triple2
The cow eats the lion.
True
2
proof
[(((triple2) -> rule3))]
("cow" "eats" "lion" "+")
((triple2) -> (rule3 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow does not eat the lion.
False
2
inv-proof
[(((triple2) -> rule3))]
("cow" "eats" "lion" "-")
((triple2) -> (rule3 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The lion does not like the bald eagle.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("lion" "likes" "bald eagle" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The lion does not like the bald eagle.
("lion" "likes" "bald eagle" "-")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The mouse is not red.
False
4
inv-proof
[(((((triple2) -> rule3) triple2) -> rule8))]
("mouse" "is" "red" "-")
((((triple2) -> (rule3 % int2)) triple2) -> (rule8 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The mouse eats the cow.
True
5
proof
[(((((((triple2) -> rule3) triple2) -> rule8)) -> rule6))]
("mouse" "eats" "cow" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule6 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3
The mouse does not eat the cow.
False
5
inv-proof
[(((((((triple2) -> rule3) triple2) -> rule8)) -> rule6))]
("mouse" "eats" "cow" "-")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule6 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3
The cow does not like the mouse.
Unknown
inv-rconc
[@1: The cow likes the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "likes" "mouse" "-")
The mouse likes the lion.
Unknown
rconc
[@1: The mouse likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "lion" "+")
The mouse does not eat the lion.
Unknown
inv-rconc
[@1: The mouse eats the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "eats" "lion" "-")
The cow eats the cow.
Unknown
rconc
[@1: The cow eats the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "eats" "cow" "+")
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 bald eagle is cold.
Unknown
random
[@0: The bald eagle is cold.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "cold" "+")
The lion does not eat the mouse.
Unknown
inv-random
[@0: The lion eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "mouse" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
@0: The bald eagle is rough.[(triple1)] The cow chases the mouse.[(triple2)] The lion likes the mouse.[(triple3)] The mouse likes the bald eagle.[(triple4)] @1: The cow eats the lion.[(((triple2) -> rule3))] @2: The lion does not like the bald eagle.[(((((triple2) -> rule3)) -> rule1))] The mouse is red.[(((((triple2) -> rule3) triple2) -> rule8))] @3: The mouse eats the cow.[(((((((triple2) -> rule3) triple2) -> rule8)) -> rule6))]
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
triple2
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple3
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
triple4
The cow eats the lion.
("cow" "eats" "lion" "+")
((triple2) -> (rule3 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The lion does not like the bald eagle.
("lion" "likes" "bald eagle" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The lion does not like the bald eagle.
("lion" "likes" "bald eagle" "-")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The mouse is red.
("mouse" "is" "red" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule8 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The mouse eats the cow.
("mouse" "eats" "cow" "+")
((((((triple2) -> (rule3 % int3)) triple2) -> (rule8 % int2))) -> (rule6 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3