The lion eats the squirrel. The mouse sees the lion. The squirrel sees the tiger. The tiger is nice. If someone is rough and they need the squirrel then they eat the lion. If someone eats the mouse then the mouse eats the squirrel. If someone sees the lion then they need the squirrel. If someone needs the mouse and they see the squirrel then they need the tiger. If someone sees the lion then they are rough. If someone is rough and they eat the lion then the lion eats the mouse.
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If someone is rough and they need the squirrel then they eat the lion.
((("someone" "is" "rough" "+") ("someone" "needs" "squirrel" "+")) -> ("someone" "eats" "lion" "+"))
If someone eats the mouse then the mouse eats the squirrel.
((("someone" "eats" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
If someone sees the lion then they need the squirrel.
((("someone" "sees" "lion" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone needs the mouse and they see the squirrel then they need the tiger.
((("someone" "needs" "mouse" "+") ("someone" "sees" "squirrel" "+")) -> ("someone" "needs" "tiger" "+"))
If someone sees the lion then they are rough.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and they eat the lion then the lion eats the mouse.
((("someone" "is" "rough" "+") ("someone" "eats" "lion" "+")) -> ("lion" "eats" "mouse" "+"))
The mouse sees the lion.
True
1
proof
[(triple2)]
("mouse" "sees" "lion" "+")
triple2
The lion does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("lion" "eats" "squirrel" "-")
triple1
The mouse needs the squirrel.
True
2
proof
[(((triple2) -> rule3))]
("mouse" "needs" "squirrel" "+")
((triple2) -> (rule3 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse does not need the squirrel.
False
2
inv-proof
[(((triple2) -> rule3))]
("mouse" "needs" "squirrel" "-")
((triple2) -> (rule3 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse eats the lion.
True
5
proof
[(((((triple2) -> rule5) ((triple2) -> rule3)) -> rule1))]
("mouse" "eats" "lion" "+")
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The mouse does not eat the lion.
False
5
inv-proof
[(((((triple2) -> rule5) ((triple2) -> rule3)) -> rule1))]
("mouse" "eats" "lion" "-")
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The lion eats the mouse.
True
8
proof
[(((((triple2) -> rule5) ((((triple2) -> rule5) ((triple2) -> rule3)) -> rule1)) -> rule6))]
("lion" "eats" "mouse" "+")
((((triple2) -> (rule5 % int4)) ((((triple2) -> (rule5 % int4)) ((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The lion does not eat the mouse.
False
8
inv-proof
[(((((triple2) -> rule5) ((((triple2) -> rule5) ((triple2) -> rule3)) -> rule1)) -> rule6))]
("lion" "eats" "mouse" "-")
((((triple2) -> (rule5 % int4)) ((((triple2) -> (rule5 % int4)) ((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "rough" "-")
The tiger eats the lion.
Unknown
rconc
[@2: The tiger eats the lion.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("tiger" "eats" "lion" "+")
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The squirrel eats the lion.
Unknown
rconc
[@2: The squirrel eats the lion.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("squirrel" "eats" "lion" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The tiger sees the mouse.
Unknown
random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "mouse" "+")
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 tiger is red.
Unknown
random
[@0: The tiger is red.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "red" "+")
@0: The lion eats the squirrel.[(triple1)] The mouse sees the lion.[(triple2)] The squirrel sees the tiger.[(triple3)] The tiger is nice.[(triple4)] @1: The mouse is rough.[(((triple2) -> rule5))] The mouse needs the squirrel.[(((triple2) -> rule3))] @2: The mouse eats the lion.[(((((triple2) -> rule5) ((triple2) -> rule3)) -> rule1))] @3: The lion eats the mouse.[(((((triple2) -> rule5) ((((triple2) -> rule5) ((triple2) -> rule3)) -> rule1)) -> rule6))] @4: The mouse eats the squirrel.[(((((((triple2) -> rule5) ((((triple2) -> rule5) ((triple2) -> rule3)) -> rule1)) -> rule6)) -> rule2))]
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple2
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
((triple2) -> (rule5 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
((triple2) -> (rule3 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
((((triple2) -> (rule5 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int2
The mouse is rough.
("mouse" "is" "rough" "+")
int3
The lion eats the mouse.
("lion" "eats" "mouse" "+")
((((triple2) -> (rule5 % int4)) ((((triple2) -> (rule5 % int4)) ((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int3
The mouse is rough.
("mouse" "is" "rough" "+")
int4
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
((((((triple2) -> (rule5 % int5)) ((((triple2) -> (rule5 % int5)) ((triple2) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int3
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int4
The mouse is rough.
("mouse" "is" "rough" "+")
int5