The bear eats the lion. The bear is nice. The bear does not need the lion. The bear visits the lion. The lion eats the bear. The lion is big. The lion is cold. The lion is nice. The lion is not red. The lion is rough. The lion does not need the bear. The lion does not visit the bear. If the bear is cold and the bear needs the lion then the lion does not visit the bear. If someone eats the bear and the bear does not need the lion then the bear is not rough. If someone visits the bear and the bear eats the lion then the lion needs the bear.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear does not need the lion.
("bear" "needs" "lion" "-")
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is not red.
("lion" "is" "red" "-")
The lion is rough.
("lion" "is" "rough" "+")
The lion does not need the bear.
("lion" "needs" "bear" "-")
The lion does not visit the bear.
("lion" "visits" "bear" "-")
If the bear is cold and the bear needs the lion then the lion does not visit the bear.
((("bear" "is" "cold" "+") ("bear" "needs" "lion" "+")) -> ("lion" "visits" "bear" "-"))
If someone eats the bear and the bear does not need the lion then the bear is not rough.
((("someone" "eats" "bear" "+") ("bear" "needs" "lion" "~")) -> ("bear" "is" "rough" "-"))
If someone visits the bear and the bear eats the lion then the lion needs the bear.
((("someone" "visits" "bear" "+") ("bear" "eats" "lion" "+")) -> ("lion" "needs" "bear" "+"))
The lion is rough.
True
1
proof
[(triple10)]
("lion" "is" "rough" "+")
triple10
The lion is not big.
False
1
inv-proof
[(triple6)]
("lion" "is" "big" "-")
triple6
The bear is not rough.
True
3
proof
[(((triple5 triple3) -> rule2))]
("bear" "is" "rough" "-")
((triple5 triple3) -> (rule2 % int1))
The bear is not rough.
("bear" "is" "rough" "-")
int1
The bear is rough.
False
3
inv-proof
[(((triple5 triple3) -> rule2))]
("bear" "is" "rough" "+")
((triple5 triple3) -> (rule2 % int1))
The bear is not rough.
("bear" "is" "rough" "-")
int1
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 bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
@0: The bear does not need the lion.[(triple3)] The bear eats the lion.[(triple1)] The bear is nice.[(triple2)] The bear visits the lion.[(triple4)] The lion does not need the bear.[(triple11)] The lion does not visit the bear.[(triple12)] The lion eats the bear.[(triple5)] The lion is big.[(triple6)] The lion is cold.[(triple7)] The lion is nice.[(triple8)] The lion is not red.[(triple9)] The lion is rough.[(triple10)] @1: The bear is not rough.[(((triple5 triple3) -> rule2))]
The bear does not need the lion.
("bear" "needs" "lion" "-")
triple3
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear visits the lion.
("bear" "visits" "lion" "+")
triple4
The lion does not need the bear.
("lion" "needs" "bear" "-")
triple11
The lion does not visit the bear.
("lion" "visits" "bear" "-")
triple12
The lion eats the bear.
("lion" "eats" "bear" "+")
triple5
The lion is big.
("lion" "is" "big" "+")
triple6
The lion is cold.
("lion" "is" "cold" "+")
triple7
The lion is nice.
("lion" "is" "nice" "+")
triple8
The lion is not red.
("lion" "is" "red" "-")
triple9
The lion is rough.
("lion" "is" "rough" "+")
triple10
The bear is not rough.
("bear" "is" "rough" "-")
((triple5 triple3) -> (rule2 % int1))
The bear is not rough.
("bear" "is" "rough" "-")
int1