The bear is not red. The cat is green. The mouse needs the squirrel. The squirrel sees the cat. If the bear is not kind then the bear sees the squirrel. If the bear likes the squirrel and the bear sees the mouse then the squirrel is big. If something sees the cat then it is big. If the bear does not like the squirrel then the squirrel needs the bear. If something sees the cat then it needs the mouse. If something needs the mouse then the mouse likes the bear.
The bear is not red.
("bear" "is" "red" "-")
The cat is green.
("cat" "is" "green" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If the bear is not kind then the bear sees the squirrel.
((("bear" "is" "kind" "~")) -> ("bear" "sees" "squirrel" "+"))
If the bear likes the squirrel and the bear sees the mouse then the squirrel is big.
((("bear" "likes" "squirrel" "+") ("bear" "sees" "mouse" "+")) -> ("squirrel" "is" "big" "+"))
If something sees the cat then it is big.
((("something" "sees" "cat" "+")) -> ("something" "is" "big" "+"))
If the bear does not like the squirrel then the squirrel needs the bear.
((("bear" "likes" "squirrel" "~")) -> ("squirrel" "needs" "bear" "+"))
If something sees the cat then it needs the mouse.
((("something" "sees" "cat" "+")) -> ("something" "needs" "mouse" "+"))
If something needs the mouse then the mouse likes the bear.
((("something" "needs" "mouse" "+")) -> ("mouse" "likes" "bear" "+"))
The mouse needs the squirrel.
True
1
proof
[(triple3)]
("mouse" "needs" "squirrel" "+")
triple3
The mouse does not need the squirrel.
False
1
inv-proof
[(triple3)]
("mouse" "needs" "squirrel" "-")
triple3
The squirrel needs the mouse.
True
2
proof
[(((triple4) -> rule5))]
("squirrel" "needs" "mouse" "+")
((triple4) -> (rule5 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The squirrel does not need the mouse.
False
2
inv-proof
[(((triple4) -> rule5))]
("squirrel" "needs" "mouse" "-")
((triple4) -> (rule5 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The mouse likes the bear.
True
3
proof
[(((((triple4) -> rule5)) -> rule6))]
("mouse" "likes" "bear" "+")
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The mouse does not like the bear.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule6))]
("mouse" "likes" "bear" "-")
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "big" "-")
The bear is big.
Unknown
rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "big" "+")
The cat is not big.
Unknown
inv-rconc
[@1: The cat is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "is" "big" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The mouse likes the cat.
Unknown
random
[@0: The mouse likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "cat" "+")
@0: The bear is not red.[(triple1)] The cat is green.[(triple2)] The mouse needs the squirrel.[(triple3)] The squirrel sees the cat.[(triple4)] @1: The squirrel is big.[(((triple4) -> rule3))] The squirrel needs the mouse.[(((triple4) -> rule5))] @2: The mouse likes the bear.[(((((triple4) -> rule5)) -> rule6))]
The bear is not red.
("bear" "is" "red" "-")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple3
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple4
The squirrel is big.
("squirrel" "is" "big" "+")
((triple4) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
((triple4) -> (rule5 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The mouse likes the bear.
("mouse" "likes" "bear" "+")
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
The mouse likes the bear.
("mouse" "likes" "bear" "+")
int1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int2