The bear does not chase the lion. The lion eats the bear. If someone eats the bear then they chase the lion. If someone chases the lion then the lion needs the bear. If someone needs the lion and the lion is big then the lion is rough. If someone is big then they eat the bear. If someone is nice and big then they chase the bear. If someone eats the bear and they chase the bear then the bear does not need the lion. If someone needs the bear then they do not eat the lion. If the lion is rough then the lion is big.
The bear does not chase the lion.
("bear" "chases" "lion" "-")
The lion eats the bear.
("lion" "eats" "bear" "+")
If someone eats the bear then they chase the lion.
((("someone" "eats" "bear" "+")) -> ("someone" "chases" "lion" "+"))
If someone chases the lion then the lion needs the bear.
((("someone" "chases" "lion" "+")) -> ("lion" "needs" "bear" "+"))
If someone needs the lion and the lion is big then the lion is rough.
((("someone" "needs" "lion" "+") ("lion" "is" "big" "+")) -> ("lion" "is" "rough" "+"))
If someone is big then they eat the bear.
((("someone" "is" "big" "+")) -> ("someone" "eats" "bear" "+"))
If someone is nice and big then they chase the bear.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "chases" "bear" "+"))
If someone eats the bear and they chase the bear then the bear does not need the lion.
((("someone" "eats" "bear" "+") ("someone" "chases" "bear" "+")) -> ("bear" "needs" "lion" "-"))
If someone needs the bear then they do not eat the lion.
((("someone" "needs" "bear" "+")) -> ("someone" "eats" "lion" "-"))
If the lion is rough then the lion is big.
((("lion" "is" "rough" "+")) -> ("lion" "is" "big" "+"))
The lion eats the bear.
True
1
proof
[(triple2)]
("lion" "eats" "bear" "+")
triple2
The bear chases the lion.
False
1
inv-proof
[(triple1)]
("bear" "chases" "lion" "+")
triple1
The lion chases the lion.
True
2
proof
[(((triple2) -> rule1))]
("lion" "chases" "lion" "+")
((triple2) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion does not chase the lion.
False
2
inv-proof
[(((triple2) -> rule1))]
("lion" "chases" "lion" "-")
((triple2) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion needs the bear.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("lion" "needs" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion does not need the bear.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("lion" "needs" "bear" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "chases" "bear" "-")
The lion is rough.
Unknown
rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "rough" "+")
The lion is not big.
Unknown
inv-rconc
[@2: The lion is big.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("lion" "is" "big" "-")
The bear eats the lion.
Unknown
random
[@0: The bear eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "lion" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear does not chase the lion.[(triple1)] The lion eats the bear.[(triple2)] @1: The lion chases the lion.[(((triple2) -> rule1))] @2: The lion needs the bear.[(((((triple2) -> rule1)) -> rule2))] @3: The lion does not eat the lion.[(((((((triple2) -> rule1)) -> rule2)) -> rule7))]
The bear does not chase the lion.
("bear" "chases" "lion" "-")
triple1
The lion eats the bear.
("lion" "eats" "bear" "+")
triple2
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple2) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion does not eat the lion.
("lion" "eats" "lion" "-")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The lion does not eat the lion.
("lion" "eats" "lion" "-")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
int3