The bear eats the lion. The lion likes the tiger. The tiger eats the lion. If the lion needs the tiger then the tiger likes the lion. If something is round then it eats the bear. If something eats the lion then the lion is round.
The bear eats the lion.
("bear" "eats" "lion" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
If the lion needs the tiger then the tiger likes the lion.
((("lion" "needs" "tiger" "+")) -> ("tiger" "likes" "lion" "+"))
If something is round then it eats the bear.
((("something" "is" "round" "+")) -> ("something" "eats" "bear" "+"))
If something eats the lion then the lion is round.
((("something" "eats" "lion" "+")) -> ("lion" "is" "round" "+"))
The bear eats the lion.
True
1
proof
[(triple1)]
("bear" "eats" "lion" "+")
triple1
The bear does not eat the lion.
False
1
inv-proof
[(triple1)]
("bear" "eats" "lion" "-")
triple1
The lion is round.
True
2
proof
[(((triple1) -> rule3) OR ((triple3) -> rule3))]
("lion" "is" "round" "+")
((triple1) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((triple3) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is not round.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple3) -> rule3))]
("lion" "is" "round" "-")
((triple1) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((triple3) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion eats the bear.
True
3
proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple3) -> rule3)) -> rule2))]
("lion" "eats" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion does not eat the bear.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple3) -> rule3)) -> rule2))]
("lion" "eats" "bear" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "bear" "-")
The tiger likes the lion.
Unknown
rconc
[@1: The tiger likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "lion" "+")
The tiger does not eat the bear.
Unknown
inv-rconc
[@1: The tiger eats the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "eats" "bear" "-")
The bear needs the tiger.
Unknown
random
[@0: The bear needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "tiger" "+")
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 lion eats the tiger.
Unknown
random
[@0: The lion eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "tiger" "+")
@0: The bear eats the lion.[(triple1)] The lion likes the tiger.[(triple2)] The tiger eats the lion.[(triple3)] @1: The lion is round.[(((triple1) -> rule3) OR ((triple3) -> rule3))] @2: The lion eats the bear.[(((((triple1) -> rule3)) -> rule2) OR ((((triple3) -> rule3)) -> rule2))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple2
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
((triple1) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((triple3) -> (rule3 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2