The bear is cold. The bear is kind. The bear is red. The bear is young. The bear likes the squirrel. The bear needs the squirrel. The bear sees the squirrel. The squirrel is blue. The squirrel is cold. The squirrel is kind. The squirrel is red. The squirrel is young. The squirrel likes the bear. The squirrel needs the bear. The squirrel sees the bear. Cold people are red. If someone likes the bear then they see the squirrel.
The bear is cold.
("bear" "is" "cold" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is red.
("bear" "is" "red" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone likes the bear then they see the squirrel.
((("someone" "likes" "bear" "+")) -> ("someone" "sees" "squirrel" "+"))
The bear is red.
True
1
proof
[(triple3 OR ((triple1) -> rule1))]
("bear" "is" "red" "+")
triple3
((triple1) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear does not need the squirrel.
False
1
inv-proof
[(triple6)]
("bear" "needs" "squirrel" "-")
triple6
The squirrel sees the squirrel.
True
2
proof
[(((triple13) -> rule2))]
("squirrel" "sees" "squirrel" "+")
((triple13) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not see the squirrel.
False
2
inv-proof
[(((triple13) -> rule2))]
("squirrel" "sees" "squirrel" "-")
((triple13) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
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 bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
@0: The bear is cold.[(triple1)] The bear is kind.[(triple2)] The bear is red.[(triple3 OR ((triple1) -> rule1))] The bear is young.[(triple4)] The bear likes the squirrel.[(triple5)] The bear needs the squirrel.[(triple6)] The bear sees the squirrel.[(triple7)] The squirrel is blue.[(triple8)] The squirrel is cold.[(triple9)] The squirrel is kind.[(triple10)] The squirrel is red.[(triple11 OR ((triple9) -> rule1))] The squirrel is young.[(triple12)] The squirrel likes the bear.[(triple13)] The squirrel needs the bear.[(triple14)] The squirrel sees the bear.[(triple15)] @1: The squirrel sees the squirrel.[(((triple13) -> rule2))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear is red.
("bear" "is" "red" "+")
triple3
((triple1) -> (rule1 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear is young.
("bear" "is" "young" "+")
triple4
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple5
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple6
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple7
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple8
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple9
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple10
The squirrel is red.
("squirrel" "is" "red" "+")
triple11
((triple9) -> (rule1 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
triple12
The squirrel likes the bear.
("squirrel" "likes" "bear" "+")
triple13
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple14
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple15
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple13) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1