The bear sees the squirrel. The mouse does not see the squirrel. The squirrel needs the bear. If someone is young then they do not like the bear. If someone needs the bear then the bear likes the squirrel. If someone is blue then they like the squirrel. If someone likes the squirrel then they need the bear. If someone is blue then they do not need the bear. If someone sees the mouse then the mouse is not young. If the squirrel is not round then the squirrel does not like the bear. If the mouse likes the squirrel and the squirrel does not need the mouse then the squirrel sees the bear.
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
If someone is young then they do not like the bear.
((("someone" "is" "young" "+")) -> ("someone" "likes" "bear" "-"))
If someone needs the bear then the bear likes the squirrel.
((("someone" "needs" "bear" "+")) -> ("bear" "likes" "squirrel" "+"))
If someone is blue then they like the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "squirrel" "+"))
If someone likes the squirrel then they need the bear.
((("someone" "likes" "squirrel" "+")) -> ("someone" "needs" "bear" "+"))
If someone is blue then they do not need the bear.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "bear" "-"))
If someone sees the mouse then the mouse is not young.
((("someone" "sees" "mouse" "+")) -> ("mouse" "is" "young" "-"))
If the squirrel is not round then the squirrel does not like the bear.
((("squirrel" "is" "round" "~")) -> ("squirrel" "likes" "bear" "-"))
If the mouse likes the squirrel and the squirrel does not need the mouse then the squirrel sees the bear.
((("mouse" "likes" "squirrel" "+") ("squirrel" "needs" "mouse" "~")) -> ("squirrel" "sees" "bear" "+"))
The mouse does not see the squirrel.
True
1
proof
[(triple2)]
("mouse" "sees" "squirrel" "-")
triple2
The mouse sees the squirrel.
False
1
inv-proof
[(triple2)]
("mouse" "sees" "squirrel" "+")
triple2
The bear likes the squirrel.
True
2
proof
[(((triple3) -> rule2))]
("bear" "likes" "squirrel" "+")
((triple3) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear does not like the squirrel.
False
2
inv-proof
[(((triple3) -> rule2))]
("bear" "likes" "squirrel" "-")
((triple3) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear needs the bear.
True
3
proof
[(((((triple3) -> rule2)) -> rule4))]
("bear" "needs" "bear" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear does not need the bear.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule4))]
("bear" "needs" "bear" "-")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The mouse does not need the bear.
Unknown
inv-rconc
[@2: The mouse needs the bear.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("mouse" "needs" "bear" "-")
The squirrel sees the bear.
Unknown
rconc
[@1: The squirrel sees the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "sees" "bear" "+")
The mouse does not like the squirrel.
Unknown
inv-rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "likes" "squirrel" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
@0: The bear sees the squirrel.[(triple1)] The mouse does not see the squirrel.[(triple2)] The squirrel needs the bear.[(triple3)] @1: The bear likes the squirrel.[(((triple3) -> rule2))] @2: The bear needs the bear.[(((((triple3) -> rule2)) -> rule4))]
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple1
The mouse does not see the squirrel.
("mouse" "sees" "squirrel" "-")
triple2
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple3
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
((triple3) -> (rule2 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear needs the bear.
("bear" "needs" "bear" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2