The lion needs the tiger. The rabbit eats the lion. The tiger eats the rabbit. If someone eats the lion then they are round. If someone needs the rabbit and they eat the rabbit then they need the tiger. If someone eats the tiger then they eat the lion. If the rabbit needs the tiger and the rabbit likes the lion then the tiger eats the lion. If someone likes the tiger and they like the lion then they are blue. If someone likes the rabbit then the rabbit is rough.
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
If someone eats the lion then they are round.
((("someone" "eats" "lion" "+")) -> ("someone" "is" "round" "+"))
If someone needs the rabbit and they eat the rabbit then they need the tiger.
((("someone" "needs" "rabbit" "+") ("someone" "eats" "rabbit" "+")) -> ("someone" "needs" "tiger" "+"))
If someone eats the tiger then they eat the lion.
((("someone" "eats" "tiger" "+")) -> ("someone" "eats" "lion" "+"))
If the rabbit needs the tiger and the rabbit likes the lion then the tiger eats the lion.
((("rabbit" "needs" "tiger" "+") ("rabbit" "likes" "lion" "+")) -> ("tiger" "eats" "lion" "+"))
If someone likes the tiger and they like the lion then they are blue.
((("someone" "likes" "tiger" "+") ("someone" "likes" "lion" "+")) -> ("someone" "is" "blue" "+"))
If someone likes the rabbit then the rabbit is rough.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
The tiger eats the rabbit.
True
1
proof
[(triple3)]
("tiger" "eats" "rabbit" "+")
triple3
The rabbit does not eat the lion.
False
1
inv-proof
[(triple2)]
("rabbit" "eats" "lion" "-")
triple2
The rabbit is round.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "is" "round" "+")
((triple2) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "is" "round" "-")
((triple2) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The tiger does not eat the lion.
Unknown
inv-rconc
[@1: The tiger eats the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "eats" "lion" "-")
The tiger is blue.
Unknown
rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "blue" "+")
The tiger does not need the lion.
Unknown
inv-random
[@0: The tiger needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "lion" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The lion needs the tiger.[(triple1)] The rabbit eats the lion.[(triple2)] The tiger eats the rabbit.[(triple3)] @1: The rabbit is round.[(((triple2) -> rule1))]
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple1
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
((triple2) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1