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