The mouse is red. The squirrel eats the mouse. The tiger eats the mouse. The tiger likes the mouse. The tiger likes the squirrel. The tiger needs the mouse. The tiger needs the squirrel. If something likes the squirrel and the squirrel is red then it needs the squirrel. If something needs the mouse then the mouse likes the squirrel. If the squirrel likes the mouse and the squirrel is big then the squirrel is red. If something likes the tiger then it needs the squirrel. If the squirrel eats the mouse and the mouse likes the squirrel then the mouse eats the tiger. If something likes the mouse then it eats the tiger.
The mouse is red.
("mouse" "is" "red" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
If something likes the squirrel and the squirrel is red then it needs the squirrel.
((("something" "likes" "squirrel" "+") ("squirrel" "is" "red" "+")) -> ("something" "needs" "squirrel" "+"))
If something needs the mouse then the mouse likes the squirrel.
((("something" "needs" "mouse" "+")) -> ("mouse" "likes" "squirrel" "+"))
If the squirrel likes the mouse and the squirrel is big then the squirrel is red.
((("squirrel" "likes" "mouse" "+") ("squirrel" "is" "big" "+")) -> ("squirrel" "is" "red" "+"))
If something likes the tiger then it needs the squirrel.
((("something" "likes" "tiger" "+")) -> ("something" "needs" "squirrel" "+"))
If the squirrel eats the mouse and the mouse likes the squirrel then the mouse eats the tiger.
((("squirrel" "eats" "mouse" "+") ("mouse" "likes" "squirrel" "+")) -> ("mouse" "eats" "tiger" "+"))
If something likes the mouse then it eats the tiger.
((("something" "likes" "mouse" "+")) -> ("something" "eats" "tiger" "+"))
The squirrel eats the mouse.
True
1
proof
[(triple2)]
("squirrel" "eats" "mouse" "+")
triple2
The tiger does not need the squirrel.
False
1
inv-proof
[(triple7)]
("tiger" "needs" "squirrel" "-")
triple7
The tiger eats the tiger.
True
2
proof
[(((triple4) -> rule6))]
("tiger" "eats" "tiger" "+")
((triple4) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger does not eat the tiger.
False
2
inv-proof
[(((triple4) -> rule6))]
("tiger" "eats" "tiger" "-")
((triple4) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The mouse eats the tiger.
True
4
proof
[(((triple2 ((triple6) -> rule2)) -> rule5))]
("mouse" "eats" "tiger" "+")
((triple2 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse does not eat the tiger.
False
4
inv-proof
[(((triple2 ((triple6) -> rule2)) -> rule5))]
("mouse" "eats" "tiger" "-")
((triple2 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2
The mouse does not need the squirrel.
Unknown
inv-rconc
[@2: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("mouse" "needs" "squirrel" "-")
The squirrel is red.
Unknown
rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "red" "+")
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The tiger does not eat the squirrel.
Unknown
inv-random
[@0: The tiger eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "squirrel" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
@0: The mouse is red.[(triple1)] The squirrel eats the mouse.[(triple2)] The tiger eats the mouse.[(triple3)] The tiger likes the mouse.[(triple4)] The tiger likes the squirrel.[(triple5)] The tiger needs the mouse.[(triple6)] The tiger needs the squirrel.[(triple7)] @1: The mouse likes the squirrel.[(((triple6) -> rule2))] The tiger eats the tiger.[(((triple4) -> rule6))] @2: The mouse eats the tiger.[(((triple2 ((triple6) -> rule2)) -> rule5))]
The mouse is red.
("mouse" "is" "red" "+")
triple1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple3
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple4
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple5
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple6
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple7
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
((triple6) -> (rule2 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple4) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((triple2 ((triple6) -> (rule2 % int2))) -> (rule5 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int2