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