The bear does not chase the cat. The bear is not big. The bear is cold. The bear is green. The bear visits the lion. The cat chases the lion. The cat is cold. The cat is young. The cat likes the bear. The cat does not visit the bear. The lion chases the bear. The lion is green. The lion is round. The lion likes the bear. The lion likes the cat. If someone is young and they like the cat then the cat likes the bear. If someone likes the lion and they visit the lion then the lion does not visit the bear. If someone visits the lion then the lion chases the bear. If someone chases the bear then they do not chase the cat. If someone is cold then they visit the cat. If someone likes the cat and the cat does not like the bear then the bear is big.
The bear does not chase the cat.
("bear" "chases" "cat" "-")
The bear is not big.
("bear" "is" "big" "-")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat does not visit the bear.
("cat" "visits" "bear" "-")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
If someone is young and they like the cat then the cat likes the bear.
((("someone" "is" "young" "+") ("someone" "likes" "cat" "+")) -> ("cat" "likes" "bear" "+"))
If someone likes the lion and they visit the lion then the lion does not visit the bear.
((("someone" "likes" "lion" "+") ("someone" "visits" "lion" "+")) -> ("lion" "visits" "bear" "-"))
If someone visits the lion then the lion chases the bear.
((("someone" "visits" "lion" "+")) -> ("lion" "chases" "bear" "+"))
If someone chases the bear then they do not chase the cat.
((("someone" "chases" "bear" "+")) -> ("someone" "chases" "cat" "-"))
If someone is cold then they visit the cat.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "cat" "+"))
If someone likes the cat and the cat does not like the bear then the bear is big.
((("someone" "likes" "cat" "+") ("cat" "likes" "bear" "~")) -> ("bear" "is" "big" "+"))
The cat is young.
True
1
proof
[(triple8)]
("cat" "is" "young" "+")
triple8
The bear chases the cat.
False
1
inv-proof
[(triple1)]
("bear" "chases" "cat" "+")
triple1
The lion does not visit the cat.
Unknown
inv-rconc
[@1: The lion visits the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "cat" "-")
The bear is round.
Unknown
random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "+")
@0: The bear does not chase the cat.[(triple1)] The bear is cold.[(triple3)] The bear is green.[(triple4)] The bear is not big.[(triple2)] The bear visits the lion.[(triple5)] The cat chases the lion.[(triple6)] The cat does not visit the bear.[(triple10)] The cat is cold.[(triple7)] The cat is young.[(triple8)] The cat likes the bear.[(triple9)] The lion chases the bear.[(triple11 OR ((triple5) -> rule3))] The lion is green.[(triple12)] The lion is round.[(triple13)] The lion likes the bear.[(triple14)] The lion likes the cat.[(triple15)] @1: The bear visits the cat.[(((triple3) -> rule5))] The cat visits the cat.[(((triple7) -> rule5))] The lion does not chase the cat.[(((triple11) -> rule4) OR ((((triple5) -> rule3)) -> rule4))]
The bear does not chase the cat.
("bear" "chases" "cat" "-")
triple1
The bear is cold.
("bear" "is" "cold" "+")
triple3
The bear is green.
("bear" "is" "green" "+")
triple4
The bear is not big.
("bear" "is" "big" "-")
triple2
The bear visits the lion.
("bear" "visits" "lion" "+")
triple5
The cat chases the lion.
("cat" "chases" "lion" "+")
triple6
The cat does not visit the bear.
("cat" "visits" "bear" "-")
triple10
The cat is cold.
("cat" "is" "cold" "+")
triple7
The cat is young.
("cat" "is" "young" "+")
triple8
The cat likes the bear.
("cat" "likes" "bear" "+")
triple9
The lion chases the bear.
("lion" "chases" "bear" "+")
triple11
((triple5) -> (rule3 % int1))
The lion chases the bear.
("lion" "chases" "bear" "+")
int1
The lion is green.
("lion" "is" "green" "+")
triple12
The lion is round.
("lion" "is" "round" "+")
triple13
The lion likes the bear.
("lion" "likes" "bear" "+")
triple14
The lion likes the cat.
("lion" "likes" "cat" "+")
triple15
The bear visits the cat.
("bear" "visits" "cat" "+")
((triple3) -> (rule5 % int1))
The bear visits the cat.
("bear" "visits" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple7) -> (rule5 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion does not chase the cat.
("lion" "chases" "cat" "-")
((triple11) -> (rule4 % int1))
The lion does not chase the cat.
("lion" "chases" "cat" "-")
int1
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
The lion does not chase the cat.
("lion" "chases" "cat" "-")
int1
The lion chases the bear.
("lion" "chases" "bear" "+")
int2