The bear chases the lion. The lion needs the tiger. The tiger needs the lion. If someone chases the lion then they are rough. If someone likes the lion and they like the bear then they chase the bear. If someone chases the lion then the lion is green. If someone is green then they like the bear. If someone is green then they need the bear. If the bear chases the tiger and the bear is not rough then the bear needs the lion. If someone is rough and they do not need the lion then the lion does not need the bear. If someone chases the lion and the lion is not green then the lion needs the bear.
The bear chases the lion.
("bear" "chases" "lion" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If someone chases the lion then they are rough.
((("someone" "chases" "lion" "+")) -> ("someone" "is" "rough" "+"))
If someone likes the lion and they like the bear then they chase the bear.
((("someone" "likes" "lion" "+") ("someone" "likes" "bear" "+")) -> ("someone" "chases" "bear" "+"))
If someone chases the lion then the lion is green.
((("someone" "chases" "lion" "+")) -> ("lion" "is" "green" "+"))
If someone is green then they like the bear.
((("someone" "is" "green" "+")) -> ("someone" "likes" "bear" "+"))
If someone is green then they need the bear.
((("someone" "is" "green" "+")) -> ("someone" "needs" "bear" "+"))
If the bear chases the tiger and the bear is not rough then the bear needs the lion.
((("bear" "chases" "tiger" "+") ("bear" "is" "rough" "~")) -> ("bear" "needs" "lion" "+"))
If someone is rough and they do not need the lion then the lion does not need the bear.
((("someone" "is" "rough" "+") ("someone" "needs" "lion" "~")) -> ("lion" "needs" "bear" "-"))
If someone chases the lion and the lion is not green then the lion needs the bear.
((("someone" "chases" "lion" "+") ("lion" "is" "green" "~")) -> ("lion" "needs" "bear" "+"))
The tiger needs the lion.
True
1
proof
[(triple3)]
("tiger" "needs" "lion" "+")
triple3
The lion does not need the tiger.
False
1
inv-proof
[(triple2)]
("lion" "needs" "tiger" "-")
triple2
The lion is green.
True
2
proof
[(((triple1) -> rule3))]
("lion" "is" "green" "+")
((triple1) -> (rule3 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The bear is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "is" "rough" "-")
((triple1) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The lion likes the bear.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("lion" "likes" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion does not need the bear.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("lion" "needs" "bear" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The tiger does not need the bear.
Unknown
inv-rconc
[@1: The tiger needs the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "needs" "bear" "-")
The bear needs the lion.
Unknown
rconc
[@1: The bear needs the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "needs" "lion" "+")
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "likes" "bear" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The bear likes the lion.
Unknown
random
[@0: The bear likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "lion" "+")
@0: The bear chases the lion.[(triple1)] The lion needs the tiger.[(triple2)] The tiger needs the lion.[(triple3)] @1: The bear is rough.[(((triple1) -> rule1))] The lion is green.[(((triple1) -> rule3))] @2: The lion likes the bear.[(((((triple1) -> rule3)) -> rule4))] The lion needs the bear.[(((((triple1) -> rule3)) -> rule5))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple3
The bear is rough.
("bear" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The lion is green.
("lion" "is" "green" "+")
((triple1) -> (rule3 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion needs the bear.
("lion" "needs" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2