The bear eats the lion. The bear is big. The bear is blue. The bear is not cold. The bear is green. The bear is red. The bear needs the lion. The bear sees the lion. The lion eats the bear. The lion is big. The lion is blue. The lion is not cold. The lion is green. The lion is red. The lion does not need the bear. The lion sees the bear. If something sees the bear then it is red. If something sees the bear and it is cold then the bear needs the lion. If something eats the bear and it is not red then the bear is cold.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is not cold.
("bear" "is" "cold" "-")
The bear is green.
("bear" "is" "green" "+")
The bear is red.
("bear" "is" "red" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is not cold.
("lion" "is" "cold" "-")
The lion is green.
("lion" "is" "green" "+")
The lion is red.
("lion" "is" "red" "+")
The lion does not need the bear.
("lion" "needs" "bear" "-")
The lion sees the bear.
("lion" "sees" "bear" "+")
If something sees the bear then it is red.
((("something" "sees" "bear" "+")) -> ("something" "is" "red" "+"))
If something sees the bear and it is cold then the bear needs the lion.
((("something" "sees" "bear" "+") ("something" "is" "cold" "+")) -> ("bear" "needs" "lion" "+"))
If something eats the bear and it is not red then the bear is cold.
((("something" "eats" "bear" "+") ("something" "is" "red" "~")) -> ("bear" "is" "cold" "+"))
The bear is big.
True
1
proof
[(triple2)]
("bear" "is" "big" "+")
triple2
The bear is not blue.
False
1
inv-proof
[(triple3)]
("bear" "is" "blue" "-")
triple3
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 lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The bear eats the lion.[(triple1)] The bear is big.[(triple2)] The bear is blue.[(triple3)] The bear is green.[(triple5)] The bear is not cold.[(triple4)] The bear is red.[(triple6)] The bear needs the lion.[(triple7)] The bear sees the lion.[(triple8)] The lion does not need the bear.[(triple15)] The lion eats the bear.[(triple9)] The lion is big.[(triple10)] The lion is blue.[(triple11)] The lion is green.[(triple13)] The lion is not cold.[(triple12)] The lion is red.[(triple14 OR ((triple16) -> rule1))] The lion sees the bear.[(triple16)]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is blue.
("bear" "is" "blue" "+")
triple3
The bear is green.
("bear" "is" "green" "+")
triple5
The bear is not cold.
("bear" "is" "cold" "-")
triple4
The bear is red.
("bear" "is" "red" "+")
triple6
The bear needs the lion.
("bear" "needs" "lion" "+")
triple7
The bear sees the lion.
("bear" "sees" "lion" "+")
triple8
The lion does not need the bear.
("lion" "needs" "bear" "-")
triple15
The lion eats the bear.
("lion" "eats" "bear" "+")
triple9
The lion is big.
("lion" "is" "big" "+")
triple10
The lion is blue.
("lion" "is" "blue" "+")
triple11
The lion is green.
("lion" "is" "green" "+")
triple13
The lion is not cold.
("lion" "is" "cold" "-")
triple12
The lion is red.
("lion" "is" "red" "+")
triple14
((triple16) -> (rule1 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion sees the bear.
("lion" "sees" "bear" "+")
triple16