The bear likes the lion. The lion eats the bear. The rabbit likes the tiger. The tiger is cold. If something is nice then it likes the tiger. If something eats the lion then the lion needs the bear. If something needs the lion then the lion needs the tiger. If something eats the bear then it eats the lion. If the rabbit is red and the rabbit likes the lion then the lion is nice. If the rabbit eats the tiger then the rabbit likes the lion.
The bear likes the lion.
("bear" "likes" "lion" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
If something is nice then it likes the tiger.
((("something" "is" "nice" "+")) -> ("something" "likes" "tiger" "+"))
If something eats the lion then the lion needs the bear.
((("something" "eats" "lion" "+")) -> ("lion" "needs" "bear" "+"))
If something needs the lion then the lion needs the tiger.
((("something" "needs" "lion" "+")) -> ("lion" "needs" "tiger" "+"))
If something eats the bear then it eats the lion.
((("something" "eats" "bear" "+")) -> ("something" "eats" "lion" "+"))
If the rabbit is red and the rabbit likes the lion then the lion is nice.
((("rabbit" "is" "red" "+") ("rabbit" "likes" "lion" "+")) -> ("lion" "is" "nice" "+"))
If the rabbit eats the tiger then the rabbit likes the lion.
((("rabbit" "eats" "tiger" "+")) -> ("rabbit" "likes" "lion" "+"))
The bear likes the lion.
True
1
proof
[(triple1)]
("bear" "likes" "lion" "+")
triple1
The rabbit does not like the tiger.
False
1
inv-proof
[(triple3)]
("rabbit" "likes" "tiger" "-")
triple3
The lion eats the lion.
True
2
proof
[(((triple2) -> rule4))]
("lion" "eats" "lion" "+")
((triple2) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion does not eat the lion.
False
2
inv-proof
[(((triple2) -> rule4))]
("lion" "eats" "lion" "-")
((triple2) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the bear.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("lion" "needs" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion does not need the bear.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("lion" "needs" "bear" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The bear likes the tiger.
Unknown
rconc
[@1: The bear likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "tiger" "+")
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "nice" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
@0: The bear likes the lion.[(triple1)] The lion eats the bear.[(triple2)] The rabbit likes the tiger.[(triple3)] The tiger is cold.[(triple4)] @1: The lion eats the lion.[(((triple2) -> rule4))] @2: The lion needs the bear.[(((((triple2) -> rule4)) -> rule2))]
The bear likes the lion.
("bear" "likes" "lion" "+")
triple1
The lion eats the bear.
("lion" "eats" "bear" "+")
triple2
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple3
The tiger is cold.
("tiger" "is" "cold" "+")
triple4
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple2) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2