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