The bear chases the cat. The bear chases the lion. The bear likes the lion. The bear needs the cat. The bear needs the lion. The cat likes the bear. The cat needs the lion. The lion chases the tiger. The lion is blue. The lion is cold. The lion is rough. The lion needs the cat. The lion needs the tiger. The tiger is rough. The tiger needs the cat. If something needs the tiger then it is cold. If the lion chases the tiger then the lion is cold. If something likes the cat and it needs the tiger then the tiger needs the lion.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If something needs the tiger then it is cold.
((("something" "needs" "tiger" "+")) -> ("something" "is" "cold" "+"))
If the lion chases the tiger then the lion is cold.
((("lion" "chases" "tiger" "+")) -> ("lion" "is" "cold" "+"))
If something likes the cat and it needs the tiger then the tiger needs the lion.
((("something" "likes" "cat" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
The bear chases the cat.
True
1
proof
[(triple1)]
("bear" "chases" "cat" "+")
triple1
The cat does not like the bear.
False
1
inv-proof
[(triple6)]
("cat" "likes" "bear" "-")
triple6
The bear is not cold.
Unknown
inv-rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "cold" "-")
The cat chases the lion.
Unknown
random
[@0: The cat chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "lion" "+")
@0: The bear chases the cat.[(triple1)] The bear chases the lion.[(triple2)] The bear likes the lion.[(triple3)] The bear needs the cat.[(triple4)] The bear needs the lion.[(triple5)] The cat likes the bear.[(triple6)] The cat needs the lion.[(triple7)] The lion chases the tiger.[(triple8)] The lion is blue.[(triple9)] The lion is cold.[(triple10 OR ((triple13) -> rule1) OR ((triple8) -> rule2))] The lion is rough.[(triple11)] The lion needs the cat.[(triple12)] The lion needs the tiger.[(triple13)] The tiger is rough.[(triple14)] The tiger needs the cat.[(triple15)]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear chases the lion.
("bear" "chases" "lion" "+")
triple2
The bear likes the lion.
("bear" "likes" "lion" "+")
triple3
The bear needs the cat.
("bear" "needs" "cat" "+")
triple4
The bear needs the lion.
("bear" "needs" "lion" "+")
triple5
The cat likes the bear.
("cat" "likes" "bear" "+")
triple6
The cat needs the lion.
("cat" "needs" "lion" "+")
triple7
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple8
The lion is blue.
("lion" "is" "blue" "+")
triple9
The lion is cold.
("lion" "is" "cold" "+")
triple10
((triple13) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((triple8) -> (rule2 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
triple11
The lion needs the cat.
("lion" "needs" "cat" "+")
triple12
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple13
The tiger is rough.
("tiger" "is" "rough" "+")
triple14
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple15