The bear chases the lion. The bear is big. The bear is kind. The lion chases the bear. The lion eats the bear. The lion is young. The lion needs the bear. If someone needs the bear then the bear eats the lion.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is kind.
("bear" "is" "kind" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
If someone needs the bear then the bear eats the lion.
((("someone" "needs" "bear" "+")) -> ("bear" "eats" "lion" "+"))
The lion is young.
True
1
proof
[(triple6)]
("lion" "is" "young" "+")
triple6
The bear is not kind.
False
1
inv-proof
[(triple3)]
("bear" "is" "kind" "-")
triple3
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The bear chases the lion.[(triple1)] The bear is big.[(triple2)] The bear is kind.[(triple3)] The lion chases the bear.[(triple4)] The lion eats the bear.[(triple5)] The lion is young.[(triple6)] The lion needs the bear.[(triple7)] @1: The bear eats the lion.[(((triple7) -> rule1))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is kind.
("bear" "is" "kind" "+")
triple3
The lion chases the bear.
("lion" "chases" "bear" "+")
triple4
The lion eats the bear.
("lion" "eats" "bear" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion needs the bear.
("lion" "needs" "bear" "+")
triple7
The bear eats the lion.
("bear" "eats" "lion" "+")
((triple7) -> (rule1 % int1))
The bear eats the lion.
("bear" "eats" "lion" "+")
int1