The bear is young. The bear likes the lion. The bear likes the squirrel. The bear likes the tiger. The bear does not see the lion. The bear sees the squirrel. The lion likes the tiger. The lion sees the bear. The squirrel is cold. The squirrel is kind. The squirrel is rough. The squirrel is young. The tiger is young. The tiger likes the bear. The tiger sees the bear. If someone is kind and they need the bear then the bear is not young. If someone sees the squirrel then they do not see the tiger.
The bear is young.
("bear" "is" "young" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear does not see the lion.
("bear" "sees" "lion" "-")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If someone is kind and they need the bear then the bear is not young.
((("someone" "is" "kind" "+") ("someone" "needs" "bear" "+")) -> ("bear" "is" "young" "-"))
If someone sees the squirrel then they do not see the tiger.
((("someone" "sees" "squirrel" "+")) -> ("someone" "sees" "tiger" "-"))
The tiger is young.
True
1
proof
[(triple13)]
("tiger" "is" "young" "+")
triple13
The bear does not like the squirrel.
False
1
inv-proof
[(triple3)]
("bear" "likes" "squirrel" "-")
triple3
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The bear does not see the lion.[(triple5)] The bear is young.[(triple1)] The bear likes the lion.[(triple2)] The bear likes the squirrel.[(triple3)] The bear likes the tiger.[(triple4)] The bear sees the squirrel.[(triple6)] The lion likes the tiger.[(triple7)] The lion sees the bear.[(triple8)] The squirrel is cold.[(triple9)] The squirrel is kind.[(triple10)] The squirrel is rough.[(triple11)] The squirrel is young.[(triple12)] The tiger is young.[(triple13)] The tiger likes the bear.[(triple14)] The tiger sees the bear.[(triple15)] @1: The bear does not see the tiger.[(((triple6) -> rule2))]
The bear does not see the lion.
("bear" "sees" "lion" "-")
triple5
The bear is young.
("bear" "is" "young" "+")
triple1
The bear likes the lion.
("bear" "likes" "lion" "+")
triple2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple3
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple4
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple6
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple7
The lion sees the bear.
("lion" "sees" "bear" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple11
The squirrel is young.
("squirrel" "is" "young" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple14
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple15
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
((triple6) -> (rule2 % int1))
The bear does not see the tiger.
("bear" "sees" "tiger" "-")
int1