The bear eats the lion. The lion likes the mouse. The mouse needs the lion. If someone likes the lion and they like the bear then the bear eats the lion. If someone is green and they eat the lion then they need the mouse. If someone needs the lion and the lion likes the mouse then the mouse eats the lion. If someone needs the bear and they eat the mouse then the mouse likes the bear. If someone likes the lion then the lion eats the bear. If someone needs the lion and the lion is big then the lion needs the mouse. If someone eats the lion then the lion is green. If someone is green then they eat the lion.
The bear eats the lion.
("bear" "eats" "lion" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
If someone likes the lion and they like the bear then the bear eats the lion.
((("someone" "likes" "lion" "+") ("someone" "likes" "bear" "+")) -> ("bear" "eats" "lion" "+"))
If someone is green and they eat the lion then they need the mouse.
((("someone" "is" "green" "+") ("someone" "eats" "lion" "+")) -> ("someone" "needs" "mouse" "+"))
If someone needs the lion and the lion likes the mouse then the mouse eats the lion.
((("someone" "needs" "lion" "+") ("lion" "likes" "mouse" "+")) -> ("mouse" "eats" "lion" "+"))
If someone needs the bear and they eat the mouse then the mouse likes the bear.
((("someone" "needs" "bear" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "likes" "bear" "+"))
If someone likes the lion then the lion eats the bear.
((("someone" "likes" "lion" "+")) -> ("lion" "eats" "bear" "+"))
If someone needs the lion and the lion is big then the lion needs the mouse.
((("someone" "needs" "lion" "+") ("lion" "is" "big" "+")) -> ("lion" "needs" "mouse" "+"))
If someone eats the lion then the lion is green.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "green" "+"))
If someone is green then they eat the lion.
((("someone" "is" "green" "+")) -> ("someone" "eats" "lion" "+"))
The mouse needs the lion.
True
1
proof
[(triple3)]
("mouse" "needs" "lion" "+")
triple3
The lion does not like the mouse.
False
1
inv-proof
[(triple2)]
("lion" "likes" "mouse" "-")
triple2
The mouse eats the lion.
True
3
proof
[(((triple3 triple2) -> rule3))]
("mouse" "eats" "lion" "+")
((triple3 triple2) -> (rule3 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The lion is not green.
False
2
inv-proof
[(((triple1) -> rule7) OR ((((triple3 triple2) -> rule3)) -> rule7))]
("lion" "is" "green" "-")
((triple1) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((((triple3 triple2) -> (rule3 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The lion eats the lion.
True
3
proof
[(((((triple1) -> rule7)) -> rule8) OR ((((((triple3 triple2) -> rule3)) -> rule7)) -> rule8))]
("lion" "eats" "lion" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
((((((triple3 triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion does not eat the lion.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule8) OR ((((((triple3 triple2) -> rule3)) -> rule7)) -> rule8))]
("lion" "eats" "lion" "-")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
((((((triple3 triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion needs the mouse.
True
6
proof
[(((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule8)) -> rule2) OR ((((((triple3 triple2) -> rule3)) -> rule7) ((((triple1) -> rule7)) -> rule8)) -> rule2) OR ((((triple1) -> rule7) ((((((triple3 triple2) -> rule3)) -> rule7)) -> rule8)) -> rule2) OR ((((((triple3 triple2) -> rule3)) -> rule7) ((((((triple3 triple2) -> rule3)) -> rule7)) -> rule8)) -> rule2))]
("lion" "needs" "mouse" "+")
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
((((((triple3 triple2) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int4
((((triple1) -> (rule7 % int4)) ((((((triple3 triple2) -> (rule3 % int3))) -> (rule7 % int4))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion is green.
("lion" "is" "green" "+")
int4
((((((triple3 triple2) -> (rule3 % int4))) -> (rule7 % int3)) ((((((triple3 triple2) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int4
The lion does not need the mouse.
False
6
inv-proof
[(((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule8)) -> rule2) OR ((((((triple3 triple2) -> rule3)) -> rule7) ((((triple1) -> rule7)) -> rule8)) -> rule2) OR ((((triple1) -> rule7) ((((((triple3 triple2) -> rule3)) -> rule7)) -> rule8)) -> rule2) OR ((((((triple3 triple2) -> rule3)) -> rule7) ((((((triple3 triple2) -> rule3)) -> rule7)) -> rule8)) -> rule2))]
("lion" "needs" "mouse" "-")
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
((((((triple3 triple2) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int4
((((triple1) -> (rule7 % int4)) ((((((triple3 triple2) -> (rule3 % int3))) -> (rule7 % int4))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion is green.
("lion" "is" "green" "+")
int4
((((((triple3 triple2) -> (rule3 % int4))) -> (rule7 % int3)) ((((((triple3 triple2) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int4
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The lion eats the bear.
Unknown
rconc
[@1: The lion eats the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "eats" "bear" "+")
The mouse does not like the bear.
Unknown
inv-rconc
[@1: The mouse likes the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "likes" "bear" "-")
The bear needs the mouse.
Unknown
rconc
[@1: The bear needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "needs" "mouse" "+")
The bear does not eat the mouse.
Unknown
inv-random
[@0: The bear eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "mouse" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The bear is not green.
Unknown
inv-random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The bear eats the lion.[(triple1)] The lion likes the mouse.[(triple2)] The mouse needs the lion.[(triple3)] @1: The lion is green.[(((triple1) -> rule7) OR ((((triple3 triple2) -> rule3)) -> rule7))] The mouse eats the lion.[(((triple3 triple2) -> rule3))] @2: The lion eats the lion.[(((((triple1) -> rule7)) -> rule8) OR ((((((triple3 triple2) -> rule3)) -> rule7)) -> rule8))] @3: The lion needs the mouse.[(((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule8)) -> rule2) OR ((((((triple3 triple2) -> rule3)) -> rule7) ((((triple1) -> rule7)) -> rule8)) -> rule2) OR ((((triple1) -> rule7) ((((((triple3 triple2) -> rule3)) -> rule7)) -> rule8)) -> rule2) OR ((((((triple3 triple2) -> rule3)) -> rule7) ((((((triple3 triple2) -> rule3)) -> rule7)) -> rule8)) -> rule2))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple2
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
((triple1) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((((triple3 triple2) -> (rule3 % int2))) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
((triple3 triple2) -> (rule3 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
((((triple1) -> (rule7 % int2))) -> (rule8 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
((((((triple3 triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
((((((triple3 triple2) -> (rule3 % int4))) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int4
((((triple1) -> (rule7 % int4)) ((((((triple3 triple2) -> (rule3 % int3))) -> (rule7 % int4))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The lion is green.
("lion" "is" "green" "+")
int4
((((((triple3 triple2) -> (rule3 % int4))) -> (rule7 % int3)) ((((((triple3 triple2) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int4