The mouse eats the squirrel. The mouse eats the tiger. The mouse is big. The mouse needs the tiger. The mouse visits the squirrel. The squirrel eats the mouse. The squirrel eats the tiger. The squirrel is green. The squirrel needs the tiger. The tiger is rough. The tiger needs the mouse. The tiger visits the squirrel. If something needs the tiger and the tiger needs the squirrel then the squirrel is nice. If something visits the tiger and it needs the squirrel then the tiger needs the squirrel. If something is rough and it eats the mouse then it eats the squirrel. If the squirrel eats the mouse then the mouse needs the squirrel. If something is nice and it eats the tiger then the tiger eats the mouse. If something eats the squirrel then the squirrel is nice.
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something needs the tiger and the tiger needs the squirrel then the squirrel is nice.
((("something" "needs" "tiger" "+") ("tiger" "needs" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
If something visits the tiger and it needs the squirrel then the tiger needs the squirrel.
((("something" "visits" "tiger" "+") ("something" "needs" "squirrel" "+")) -> ("tiger" "needs" "squirrel" "+"))
If something is rough and it eats the mouse then it eats the squirrel.
((("something" "is" "rough" "+") ("something" "eats" "mouse" "+")) -> ("something" "eats" "squirrel" "+"))
If the squirrel eats the mouse then the mouse needs the squirrel.
((("squirrel" "eats" "mouse" "+")) -> ("mouse" "needs" "squirrel" "+"))
If something is nice and it eats the tiger then the tiger eats the mouse.
((("something" "is" "nice" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "eats" "mouse" "+"))
If something eats the squirrel then the squirrel is nice.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "nice" "+"))
The tiger needs the mouse.
True
1
proof
[(triple11)]
("tiger" "needs" "mouse" "+")
triple11
The tiger does not need the mouse.
False
1
inv-proof
[(triple11)]
("tiger" "needs" "mouse" "-")
triple11
The mouse needs the squirrel.
True
2
proof
[(((triple6) -> rule4))]
("mouse" "needs" "squirrel" "+")
((triple6) -> (rule4 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel is not nice.
False
2
inv-proof
[(((triple1) -> rule6))]
("squirrel" "is" "nice" "-")
((triple1) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The tiger eats the mouse.
True
4
proof
[(((((triple1) -> rule6) triple7) -> rule5))]
("tiger" "eats" "mouse" "+")
((((triple1) -> (rule6 % int2)) triple7) -> (rule5 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The tiger does not eat the mouse.
False
4
inv-proof
[(((((triple1) -> rule6) triple7) -> rule5))]
("tiger" "eats" "mouse" "-")
((((triple1) -> (rule6 % int2)) triple7) -> (rule5 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The tiger eats the squirrel.
True
6
proof
[(((triple10 ((((triple1) -> rule6) triple7) -> rule5)) -> rule3))]
("tiger" "eats" "squirrel" "+")
((triple10 ((((triple1) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The tiger does not eat the squirrel.
False
6
inv-proof
[(((triple10 ((((triple1) -> rule6) triple7) -> rule5)) -> rule3))]
("tiger" "eats" "squirrel" "-")
((triple10 ((((triple1) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The tiger does not need the squirrel.
Unknown
inv-rconc
[@1: The tiger needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "needs" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "eats" "squirrel" "+")
The tiger does not visit the mouse.
Unknown
inv-random
[@0: The tiger visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "mouse" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
The squirrel does not visit the tiger.
Unknown
inv-random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The mouse eats the squirrel.[(triple1)] The mouse eats the tiger.[(triple2)] The mouse is big.[(triple3)] The mouse needs the tiger.[(triple4)] The mouse visits the squirrel.[(triple5)] The squirrel eats the mouse.[(triple6)] The squirrel eats the tiger.[(triple7)] The squirrel is green.[(triple8)] The squirrel needs the tiger.[(triple9)] The tiger is rough.[(triple10)] The tiger needs the mouse.[(triple11)] The tiger visits the squirrel.[(triple12)] @1: The mouse needs the squirrel.[(((triple6) -> rule4))] The squirrel is nice.[(((triple1) -> rule6))] @2: The tiger eats the mouse.[(((((triple1) -> rule6) triple7) -> rule5))] @3: The tiger eats the squirrel.[(((triple10 ((((triple1) -> rule6) triple7) -> rule5)) -> rule3))]
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The mouse is big.
("mouse" "is" "big" "+")
triple3
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple4
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple5
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple6
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple7
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple9
The tiger is rough.
("tiger" "is" "rough" "+")
triple10
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple11
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple12
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
((triple6) -> (rule4 % int1))
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple1) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((((triple1) -> (rule6 % int2)) triple7) -> (rule5 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
((triple10 ((((triple1) -> (rule6 % int3)) triple7) -> (rule5 % int2))) -> (rule3 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3