The bald eagle needs the rabbit. The lion chases the bald eagle. The mouse chases the lion. The mouse does not chase the rabbit. The mouse eats the bald eagle. The mouse eats the rabbit. The rabbit is not young. If someone eats the bald eagle then the bald eagle needs the rabbit. If someone eats the rabbit then they need the lion. If someone eats the mouse and the mouse eats the lion then they chase the lion. If someone is red then they do not chase the bald eagle. If someone needs the rabbit and they need the lion then they do not eat the bald eagle. If someone needs the lion then the lion eats the rabbit. If someone eats the mouse and they are not green then the mouse is not blue. If someone is green and not red then they are rough.
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The rabbit is not young.
("rabbit" "is" "young" "-")
If someone eats the bald eagle then the bald eagle needs the rabbit.
((("someone" "eats" "bald eagle" "+")) -> ("bald eagle" "needs" "rabbit" "+"))
If someone eats the rabbit then they need the lion.
((("someone" "eats" "rabbit" "+")) -> ("someone" "needs" "lion" "+"))
If someone eats the mouse and the mouse eats the lion then they chase the lion.
((("someone" "eats" "mouse" "+") ("mouse" "eats" "lion" "+")) -> ("someone" "chases" "lion" "+"))
If someone is red then they do not chase the bald eagle.
((("someone" "is" "red" "+")) -> ("someone" "chases" "bald eagle" "-"))
If someone needs the rabbit and they need the lion then they do not eat the bald eagle.
((("someone" "needs" "rabbit" "+") ("someone" "needs" "lion" "+")) -> ("someone" "eats" "bald eagle" "-"))
If someone needs the lion then the lion eats the rabbit.
((("someone" "needs" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If someone eats the mouse and they are not green then the mouse is not blue.
((("someone" "eats" "mouse" "+") ("someone" "is" "green" "~")) -> ("mouse" "is" "blue" "-"))
If someone is green and not red then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "rough" "+"))
The mouse eats the bald eagle.
True
1
proof
[(triple5)]
("mouse" "eats" "bald eagle" "+")
triple5
The rabbit is young.
False
1
inv-proof
[(triple7)]
("rabbit" "is" "young" "+")
triple7
The mouse needs the lion.
True
2
proof
[(((triple6) -> rule2))]
("mouse" "needs" "lion" "+")
((triple6) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The mouse does not need the lion.
False
2
inv-proof
[(((triple6) -> rule2))]
("mouse" "needs" "lion" "-")
((triple6) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion eats the rabbit.
True
3
proof
[(((((triple6) -> rule2)) -> rule6))]
("lion" "eats" "rabbit" "+")
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The lion does not eat the rabbit.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule6))]
("lion" "eats" "rabbit" "-")
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The lion needs the lion.
True
4
proof
[(((((((triple6) -> rule2)) -> rule6)) -> rule2))]
("lion" "needs" "lion" "+")
((((((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3
The lion does not need the lion.
False
4
inv-proof
[(((((((triple6) -> rule2)) -> rule6)) -> rule2))]
("lion" "needs" "lion" "-")
((((((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3
The bald eagle does not need the lion.
Unknown
inv-rconc
[@1: The bald eagle needs the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "needs" "lion" "-")
The bald eagle is rough.
Unknown
rconc
[@1: The bald eagle is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bald eagle" "is" "rough" "+")
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit needs the lion.
Unknown
rconc
[@1: The rabbit needs the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "needs" "lion" "+")
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 mouse eats the lion.
Unknown
random
[@0: The mouse eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "lion" "+")
The bald eagle does not eat the mouse.
Unknown
inv-random
[@0: The bald eagle eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "mouse" "-")
The bald eagle chases the rabbit.
Unknown
random
[@0: The bald eagle chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "rabbit" "+")
@0: The bald eagle needs the rabbit.[(triple1 OR ((triple5) -> rule1))] The lion chases the bald eagle.[(triple2)] The mouse chases the lion.[(triple3)] The mouse does not chase the rabbit.[(triple4)] The mouse eats the bald eagle.[(triple5)] The mouse eats the rabbit.[(triple6)] The rabbit is not young.[(triple7)] @1: The mouse needs the lion.[(((triple6) -> rule2))] @2: The lion eats the rabbit.[(((((triple6) -> rule2)) -> rule6))] @3: The lion needs the lion.[(((((((triple6) -> rule2)) -> rule6)) -> rule2))]
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
triple1
((triple5) -> (rule1 % int1))
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
int1
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
triple2
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple3
The mouse does not chase the rabbit.
("mouse" "chases" "rabbit" "-")
triple4
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
triple5
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple6
The rabbit is not young.
("rabbit" "is" "young" "-")
triple7
The mouse needs the lion.
("mouse" "needs" "lion" "+")
((triple6) -> (rule2 % int1))
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
((((triple6) -> (rule2 % int2))) -> (rule6 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
((((((triple6) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
int3