The bear likes the tiger. The bear needs the lion. The bear needs the squirrel. The lion is blue. The lion likes the tiger. The lion needs the bear. The squirrel likes the tiger. The squirrel needs the lion. The squirrel needs the tiger. The squirrel visits the bear. The squirrel visits the lion. The tiger is big. The tiger is green. The tiger likes the lion. The tiger visits the squirrel. If someone likes the lion then they are green. If the tiger likes the squirrel then the tiger is blue. If someone likes the bear then the bear is blue. If someone likes the squirrel then they visit the lion. If someone is round and they visit the tiger then they visit the squirrel. If someone visits the lion then they like the lion. If someone needs the tiger and they are round then they are blue. If someone is green then they visit the lion.
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone likes the lion then they are green.
((("someone" "likes" "lion" "+")) -> ("someone" "is" "green" "+"))
If the tiger likes the squirrel then the tiger is blue.
((("tiger" "likes" "squirrel" "+")) -> ("tiger" "is" "blue" "+"))
If someone likes the bear then the bear is blue.
((("someone" "likes" "bear" "+")) -> ("bear" "is" "blue" "+"))
If someone likes the squirrel then they visit the lion.
((("someone" "likes" "squirrel" "+")) -> ("someone" "visits" "lion" "+"))
If someone is round and they visit the tiger then they visit the squirrel.
((("someone" "is" "round" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "visits" "squirrel" "+"))
If someone visits the lion then they like the lion.
((("someone" "visits" "lion" "+")) -> ("someone" "likes" "lion" "+"))
If someone needs the tiger and they are round then they are blue.
((("someone" "needs" "tiger" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "blue" "+"))
If someone is green then they visit the lion.
((("someone" "is" "green" "+")) -> ("someone" "visits" "lion" "+"))
The tiger likes the lion.
True
1
proof
[(triple14 OR ((((triple13) -> rule8)) -> rule6))]
("tiger" "likes" "lion" "+")
triple14
((((triple13) -> (rule8 % int2))) -> (rule6 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The bear does not need the squirrel.
False
1
inv-proof
[(triple3)]
("bear" "needs" "squirrel" "-")
triple3
The squirrel likes the lion.
True
2
proof
[(((triple11) -> rule6))]
("squirrel" "likes" "lion" "+")
((triple11) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The tiger does not visit the lion.
False
2
inv-proof
[(((triple13) -> rule8) OR ((((triple14) -> rule1)) -> rule8))]
("tiger" "visits" "lion" "-")
((triple13) -> (rule8 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule8 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The squirrel is green.
True
3
proof
[(((((triple11) -> rule6)) -> rule1))]
("squirrel" "is" "green" "+")
((((triple11) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The squirrel is not green.
False
3
inv-proof
[(((((triple11) -> rule6)) -> rule1))]
("squirrel" "is" "green" "-")
((((triple11) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2
The lion does not like the lion.
Unknown
inv-rconc
[@3: The lion likes the lion.[CWA. Example of deepest failure = (rule6 <- rule8 <- rule1 <- FAIL)]]
("lion" "likes" "lion" "-")
The lion visits the squirrel.
Unknown
rconc
[@1: The lion visits the squirrel.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "squirrel" "+")
The bear does not visit the lion.
Unknown
inv-rconc
[@4: The bear visits the lion.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule6 <- rule4 <- FAIL)]]
("bear" "visits" "lion" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The lion needs the tiger.
Unknown
random
[@0: The lion needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "tiger" "+")
@0: The bear likes the tiger.[(triple1)] The bear needs the lion.[(triple2)] The bear needs the squirrel.[(triple3)] The lion is blue.[(triple4)] The lion likes the tiger.[(triple5)] The lion needs the bear.[(triple6)] The squirrel likes the tiger.[(triple7)] The squirrel needs the lion.[(triple8)] The squirrel needs the tiger.[(triple9)] The squirrel visits the bear.[(triple10)] The squirrel visits the lion.[(triple11)] The tiger is big.[(triple12)] The tiger is green.[(triple13 OR ((triple14) -> rule1))] The tiger likes the lion.[(triple14 OR ((((triple13) -> rule8)) -> rule6))] The tiger visits the squirrel.[(triple15)] @1: The squirrel likes the lion.[(((triple11) -> rule6))] The tiger visits the lion.[(((triple13) -> rule8) OR ((((triple14) -> rule1)) -> rule8))] @2: The squirrel is green.[(((((triple11) -> rule6)) -> rule1))]
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple1
The bear needs the lion.
("bear" "needs" "lion" "+")
triple2
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple3
The lion is blue.
("lion" "is" "blue" "+")
triple4
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple5
The lion needs the bear.
("lion" "needs" "bear" "+")
triple6
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple7
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple8
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple9
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple10
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple11
The tiger is big.
("tiger" "is" "big" "+")
triple12
The tiger is green.
("tiger" "is" "green" "+")
triple13
((triple14) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple14
((((triple13) -> (rule8 % int2))) -> (rule6 % int1))
The tiger likes the lion.
("tiger" "likes" "lion" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple15
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
((triple11) -> (rule6 % int1))
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
((triple13) -> (rule8 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
((((triple14) -> (rule1 % int2))) -> (rule8 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
((((triple11) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
int2