The lion needs the mouse. The mouse is green. The squirrel does not eat the tiger. The squirrel is big. The squirrel is blue. The squirrel is young. The squirrel needs the lion. The squirrel does not need the mouse. The squirrel needs the tiger. The squirrel sees the lion. The squirrel sees the mouse. The tiger is big. If something eats the squirrel then the squirrel does not need the lion. If something is big and it needs the squirrel then the squirrel does not see the tiger. All red things are green. If the squirrel eats the lion and the lion is red then the squirrel does not eat the tiger. If something needs the tiger then the tiger is red. If something sees the tiger then the tiger eats the mouse.
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The squirrel does not eat the tiger.
("squirrel" "eats" "tiger" "-")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
If something eats the squirrel then the squirrel does not need the lion.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "needs" "lion" "-"))
If something is big and it needs the squirrel then the squirrel does not see the tiger.
((("something" "is" "big" "+") ("something" "needs" "squirrel" "+")) -> ("squirrel" "sees" "tiger" "-"))
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If the squirrel eats the lion and the lion is red then the squirrel does not eat the tiger.
((("squirrel" "eats" "lion" "+") ("lion" "is" "red" "+")) -> ("squirrel" "eats" "tiger" "-"))
If something needs the tiger then the tiger is red.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If something sees the tiger then the tiger eats the mouse.
((("something" "sees" "tiger" "+")) -> ("tiger" "eats" "mouse" "+"))
The squirrel is young.
True
1
proof
[(triple6)]
("squirrel" "is" "young" "+")
triple6
The squirrel eats the tiger.
False
1
inv-proof
[(triple3)]
("squirrel" "eats" "tiger" "+")
triple3
The tiger is red.
True
2
proof
[(((triple9) -> rule5))]
("tiger" "is" "red" "+")
((triple9) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is not red.
False
2
inv-proof
[(((triple9) -> rule5))]
("tiger" "is" "red" "-")
((triple9) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is green.
True
3
proof
[(((((triple9) -> rule5)) -> rule3))]
("tiger" "is" "green" "+")
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is not green.
False
3
inv-proof
[(((((triple9) -> rule5)) -> rule3))]
("tiger" "is" "green" "-")
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger does not eat the mouse.
Unknown
inv-rconc
[@1: The tiger eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "eats" "mouse" "-")
The lion is green.
Unknown
rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "green" "+")
The squirrel is not green.
Unknown
inv-rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "green" "-")
The squirrel is red.
Unknown
random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The mouse needs the squirrel.
Unknown
random
[@0: The mouse needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "squirrel" "+")
@0: The lion needs the mouse.[(triple1)] The mouse is green.[(triple2)] The squirrel does not eat the tiger.[(triple3)] The squirrel does not need the mouse.[(triple8)] The squirrel is big.[(triple4)] The squirrel is blue.[(triple5)] The squirrel is young.[(triple6)] The squirrel needs the lion.[(triple7)] The squirrel needs the tiger.[(triple9)] The squirrel sees the lion.[(triple10)] The squirrel sees the mouse.[(triple11)] The tiger is big.[(triple12)] @1: The tiger is red.[(((triple9) -> rule5))] @2: The tiger is green.[(((((triple9) -> rule5)) -> rule3))]
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple1
The mouse is green.
("mouse" "is" "green" "+")
triple2
The squirrel does not eat the tiger.
("squirrel" "eats" "tiger" "-")
triple3
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
triple8
The squirrel is big.
("squirrel" "is" "big" "+")
triple4
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple5
The squirrel is young.
("squirrel" "is" "young" "+")
triple6
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple7
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple9
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple10
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple11
The tiger is big.
("tiger" "is" "big" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
((triple9) -> (rule5 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
((((triple9) -> (rule5 % int2))) -> (rule3 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2