The bear does not chase the lion. The bear is big. The bear is not blue. The bear is not cold. The bear is nice. The bear does not need the lion. The bear visits the lion. The lion chases the bear. The lion is big. The lion is blue. The lion is cold. The lion is not kind. The lion is nice. The lion needs the bear. The lion visits the bear. If someone is cold and they do not visit the bear then they are nice. If the bear is nice and the bear does not chase the lion then the lion needs the bear. If someone is nice and they do not need the lion then they do not need the bear. If someone needs the lion then they do not chase the bear. If someone visits the bear and the bear does not visit the lion then they chase the bear. If someone is big and they do not need the bear then they chase the bear.
The bear does not chase the lion.
("bear" "chases" "lion" "-")
The bear is big.
("bear" "is" "big" "+")
The bear is not blue.
("bear" "is" "blue" "-")
The bear is not cold.
("bear" "is" "cold" "-")
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 chases the bear.
("lion" "chases" "bear" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion is nice.
("lion" "is" "nice" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If someone is cold and they do not visit the bear then they are nice.
((("someone" "is" "cold" "+") ("someone" "visits" "bear" "~")) -> ("someone" "is" "nice" "+"))
If the bear is nice and the bear does not chase the lion then the lion needs the bear.
((("bear" "is" "nice" "+") ("bear" "chases" "lion" "~")) -> ("lion" "needs" "bear" "+"))
If someone is nice and they do not need the lion then they do not need the bear.
((("someone" "is" "nice" "+") ("someone" "needs" "lion" "~")) -> ("someone" "needs" "bear" "-"))
If someone needs the lion then they do not chase the bear.
((("someone" "needs" "lion" "+")) -> ("someone" "chases" "bear" "-"))
If someone visits the bear and the bear does not visit the lion then they chase the bear.
((("someone" "visits" "bear" "+") ("bear" "visits" "lion" "~")) -> ("someone" "chases" "bear" "+"))
If someone is big and they do not need the bear then they chase the bear.
((("someone" "is" "big" "+") ("someone" "needs" "bear" "~")) -> ("someone" "chases" "bear" "+"))
The bear does not chase the lion.
True
1
proof
[(triple1)]
("bear" "chases" "lion" "-")
triple1
The lion is kind.
False
1
inv-proof
[(triple12)]
("lion" "is" "kind" "+")
triple12
The bear does not need the bear.
True
3
proof
[(((triple5 triple6) -> rule3))]
("bear" "needs" "bear" "-")
((triple5 triple6) -> (rule3 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1
The bear needs the bear.
False
3
inv-proof
[(((triple5 triple6) -> rule3))]
("bear" "needs" "bear" "+")
((triple5 triple6) -> (rule3 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1
The bear chases the bear.
True
5
proof
[(((triple2 ((triple5 triple6) -> rule3)) -> rule6))]
("bear" "chases" "bear" "+")
((triple2 ((triple5 triple6) -> (rule3 % int2))) -> (rule6 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear does not need the bear.
("bear" "needs" "bear" "-")
int2
The bear does not chase the bear.
False
5
inv-proof
[(((triple2 ((triple5 triple6) -> rule3)) -> rule6))]
("bear" "chases" "bear" "-")
((triple2 ((triple5 triple6) -> (rule3 % int2))) -> (rule6 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear does not need the bear.
("bear" "needs" "bear" "-")
int2
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The bear does not chase the lion.[(triple1)] The bear does not need the lion.[(triple6)] The bear is big.[(triple2)] The bear is nice.[(triple5)] The bear is not blue.[(triple3)] The bear is not cold.[(triple4)] The bear visits the lion.[(triple7)] The lion chases the bear.[(triple8)] The lion is big.[(triple9)] The lion is blue.[(triple10)] The lion is cold.[(triple11)] The lion is nice.[(triple13)] The lion is not kind.[(triple12)] The lion needs the bear.[(triple14 OR ((triple5 triple1) -> rule2))] The lion visits the bear.[(triple15)] @1: The bear does not need the bear.[(((triple5 triple6) -> rule3))] @2: The bear chases the bear.[(((triple2 ((triple5 triple6) -> rule3)) -> rule6))]
The bear does not chase the lion.
("bear" "chases" "lion" "-")
triple1
The bear does not need the lion.
("bear" "needs" "lion" "-")
triple6
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple5
The bear is not blue.
("bear" "is" "blue" "-")
triple3
The bear is not cold.
("bear" "is" "cold" "-")
triple4
The bear visits the lion.
("bear" "visits" "lion" "+")
triple7
The lion chases the bear.
("lion" "chases" "bear" "+")
triple8
The lion is big.
("lion" "is" "big" "+")
triple9
The lion is blue.
("lion" "is" "blue" "+")
triple10
The lion is cold.
("lion" "is" "cold" "+")
triple11
The lion is nice.
("lion" "is" "nice" "+")
triple13
The lion is not kind.
("lion" "is" "kind" "-")
triple12
The lion needs the bear.
("lion" "needs" "bear" "+")
triple14
((triple5 triple1) -> (rule2 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
triple15
The bear does not need the bear.
("bear" "needs" "bear" "-")
((triple5 triple6) -> (rule3 % int1))
The bear does not need the bear.
("bear" "needs" "bear" "-")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple2 ((triple5 triple6) -> (rule3 % int2))) -> (rule6 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear does not need the bear.
("bear" "needs" "bear" "-")
int2