The cat needs the lion. The lion needs the rabbit. The rabbit sees the tiger. The tiger needs the cat. If someone sees the tiger then the tiger eats the rabbit. If someone needs the cat then they see the cat. If someone needs the rabbit then the rabbit needs the cat.
The cat needs the lion.
("cat" "needs" "lion" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If someone sees the tiger then the tiger eats the rabbit.
((("someone" "sees" "tiger" "+")) -> ("tiger" "eats" "rabbit" "+"))
If someone needs the cat then they see the cat.
((("someone" "needs" "cat" "+")) -> ("someone" "sees" "cat" "+"))
If someone needs the rabbit then the rabbit needs the cat.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "needs" "cat" "+"))
The rabbit sees the tiger.
True
1
proof
[(triple3)]
("rabbit" "sees" "tiger" "+")
triple3
The tiger does not need the cat.
False
1
inv-proof
[(triple4)]
("tiger" "needs" "cat" "-")
triple4
The tiger sees the cat.
True
2
proof
[(((triple4) -> rule2))]
("tiger" "sees" "cat" "+")
((triple4) -> (rule2 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The tiger does not see the cat.
False
2
inv-proof
[(((triple4) -> rule2))]
("tiger" "sees" "cat" "-")
((triple4) -> (rule2 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The rabbit sees the cat.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("rabbit" "sees" "cat" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The rabbit does not see the cat.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("rabbit" "sees" "cat" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The lion does not see the cat.
Unknown
inv-rconc
[@1: The lion sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "cat" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "cat" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
@0: The cat needs the lion.[(triple1)] The lion needs the rabbit.[(triple2)] The rabbit sees the tiger.[(triple3)] The tiger needs the cat.[(triple4)] @1: The rabbit needs the cat.[(((triple2) -> rule3))] The tiger eats the rabbit.[(((triple3) -> rule1))] The tiger sees the cat.[(((triple4) -> rule2))] @2: The rabbit sees the cat.[(((((triple2) -> rule3)) -> rule2))]
The cat needs the lion.
("cat" "needs" "lion" "+")
triple1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple4
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
((triple2) -> (rule3 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
((triple3) -> (rule1 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
((triple4) -> (rule2 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2