The bear is big. The bear is green. The bear is kind. The bear is nice. The bear is rough. The bear needs the squirrel. The bear sees the squirrel. The bear visits the squirrel. The squirrel is big. The squirrel is green. The squirrel is kind. The squirrel is nice. The squirrel is rough. The squirrel needs the bear. The squirrel sees the bear. The squirrel visits the bear. If the bear needs the squirrel then the squirrel needs the bear. All rough things are big. If something visits the squirrel then it is kind. If something visits the squirrel and the squirrel needs the bear then the bear sees the squirrel. If something needs the squirrel then the squirrel visits the bear. If something needs the squirrel and it is big then it sees the bear.
The bear is big.
("bear" "is" "big" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
If the bear needs the squirrel then the squirrel needs the bear.
((("bear" "needs" "squirrel" "+")) -> ("squirrel" "needs" "bear" "+"))
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something visits the squirrel then it is kind.
((("something" "visits" "squirrel" "+")) -> ("something" "is" "kind" "+"))
If something visits the squirrel and the squirrel needs the bear then the bear sees the squirrel.
((("something" "visits" "squirrel" "+") ("squirrel" "needs" "bear" "+")) -> ("bear" "sees" "squirrel" "+"))
If something needs the squirrel then the squirrel visits the bear.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "visits" "bear" "+"))
If something needs the squirrel and it is big then it sees the bear.
((("something" "needs" "squirrel" "+") ("something" "is" "big" "+")) -> ("something" "sees" "bear" "+"))
The bear is green.
True
1
proof
[(triple2)]
("bear" "is" "green" "+")
triple2
The bear is not rough.
False
1
inv-proof
[(triple5)]
("bear" "is" "rough" "-")
triple5
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "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 big.[(triple1 OR ((triple5) -> rule2))] The bear is green.[(triple2)] The bear is kind.[(triple3 OR ((triple8) -> rule3))] The bear is nice.[(triple4)] The bear is rough.[(triple5)] The bear needs the squirrel.[(triple6)] The bear sees the squirrel.[(triple7 OR ((triple8 triple14) -> rule4) OR ((triple8 ((triple6) -> rule1)) -> rule4))] The bear visits the squirrel.[(triple8)] The squirrel is big.[(triple9 OR ((triple13) -> rule2))] The squirrel is green.[(triple10)] The squirrel is kind.[(triple11)] The squirrel is nice.[(triple12)] The squirrel is rough.[(triple13)] The squirrel needs the bear.[(triple14 OR ((triple6) -> rule1))] The squirrel sees the bear.[(triple15)] The squirrel visits the bear.[(triple16 OR ((triple6) -> rule5))] @1: The bear sees the bear.[(((triple6 triple1) -> rule6) OR ((triple6 ((triple5) -> rule2)) -> rule6))]
The bear is big.
("bear" "is" "big" "+")
triple1
((triple5) -> (rule2 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear is kind.
("bear" "is" "kind" "+")
triple3
((triple8) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
triple4
The bear is rough.
("bear" "is" "rough" "+")
triple5
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple6
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple7
((triple8 triple14) -> (rule4 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
((triple8 ((triple6) -> (rule1 % int2))) -> (rule4 % int1))
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
int1
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple8
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
((triple13) -> (rule2 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
triple10
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple11
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple12
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple13
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple14
((triple6) -> (rule1 % int1))
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
int1
The squirrel sees the bear.
("squirrel" "sees" "bear" "+")
triple15
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple16
((triple6) -> (rule5 % int1))
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple6 triple1) -> (rule6 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
((triple6 ((triple5) -> (rule2 % int2))) -> (rule6 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The bear is big.
("bear" "is" "big" "+")
int2