The bear does not need the mouse. The dog does not need the bear. The mouse is red. The squirrel eats the mouse. If something is nice and it needs the bear then the bear eats the mouse. If something eats the squirrel then the squirrel is big. If something eats the bear then the bear chases the dog. If something is red then it eats the squirrel. If the mouse needs the squirrel then the squirrel eats the bear. If something chases the squirrel then it eats the dog.
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
The dog does not need the bear.
("dog" "needs" "bear" "-")
The mouse is red.
("mouse" "is" "red" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
If something is nice and it needs the bear then the bear eats the mouse.
((("something" "is" "nice" "+") ("something" "needs" "bear" "+")) -> ("bear" "eats" "mouse" "+"))
If something eats the squirrel then the squirrel is big.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "big" "+"))
If something eats the bear then the bear chases the dog.
((("something" "eats" "bear" "+")) -> ("bear" "chases" "dog" "+"))
If something is red then it eats the squirrel.
((("something" "is" "red" "+")) -> ("something" "eats" "squirrel" "+"))
If the mouse needs the squirrel then the squirrel eats the bear.
((("mouse" "needs" "squirrel" "+")) -> ("squirrel" "eats" "bear" "+"))
If something chases the squirrel then it eats the dog.
((("something" "chases" "squirrel" "+")) -> ("something" "eats" "dog" "+"))
The squirrel eats the mouse.
True
1
proof
[(triple4)]
("squirrel" "eats" "mouse" "+")
triple4
The squirrel does not eat the mouse.
False
1
inv-proof
[(triple4)]
("squirrel" "eats" "mouse" "-")
triple4
The mouse eats the squirrel.
True
2
proof
[(((triple3) -> rule4))]
("mouse" "eats" "squirrel" "+")
((triple3) -> (rule4 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse does not eat the squirrel.
False
2
inv-proof
[(((triple3) -> rule4))]
("mouse" "eats" "squirrel" "-")
((triple3) -> (rule4 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The squirrel is big.
True
3
proof
[(((((triple3) -> rule4)) -> rule2))]
("squirrel" "is" "big" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel is not big.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule2))]
("squirrel" "is" "big" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel eats the dog.
Unknown
rconc
[@1: The squirrel eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "eats" "dog" "+")
The bear does not eat the mouse.
Unknown
inv-rconc
[@1: The bear eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "eats" "mouse" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
The mouse does not need the squirrel.
Unknown
inv-random
[@0: The mouse needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "squirrel" "-")
The bear chases the squirrel.
Unknown
random
[@0: The bear chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "squirrel" "+")
@0: The bear does not need the mouse.[(triple1)] The dog does not need the bear.[(triple2)] The mouse is red.[(triple3)] The squirrel eats the mouse.[(triple4)] @1: The mouse eats the squirrel.[(((triple3) -> rule4))] @2: The squirrel is big.[(((((triple3) -> rule4)) -> rule2))]
The bear does not need the mouse.
("bear" "needs" "mouse" "-")
triple1
The dog does not need the bear.
("dog" "needs" "bear" "-")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple3
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple4
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
((triple3) -> (rule4 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2