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