The lion eats the rabbit. The lion is cold. The lion needs the rabbit. The lion sees the rabbit. The lion sees the tiger. The rabbit is cold. The tiger needs the lion. If someone sees the tiger then the tiger eats the lion. If the lion sees the rabbit and the rabbit sees the lion then the rabbit eats the lion.
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If someone sees the tiger then the tiger eats the lion.
((("someone" "sees" "tiger" "+")) -> ("tiger" "eats" "lion" "+"))
If the lion sees the rabbit and the rabbit sees the lion then the rabbit eats the lion.
((("lion" "sees" "rabbit" "+") ("rabbit" "sees" "lion" "+")) -> ("rabbit" "eats" "lion" "+"))
The rabbit is cold.
True
1
proof
[(triple6)]
("rabbit" "is" "cold" "+")
triple6
The rabbit is not cold.
False
1
inv-proof
[(triple6)]
("rabbit" "is" "cold" "-")
triple6
The tiger eats the lion.
True
2
proof
[(((triple5) -> rule1))]
("tiger" "eats" "lion" "+")
((triple5) -> (rule1 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The tiger does not eat the lion.
False
2
inv-proof
[(((triple5) -> rule1))]
("tiger" "eats" "lion" "-")
((triple5) -> (rule1 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The rabbit does not eat the lion.
Unknown
inv-rconc
[@1: The rabbit eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "eats" "lion" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The lion does not eat the tiger.
Unknown
inv-random
[@0: The lion eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "tiger" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
@0: The lion eats the rabbit.[(triple1)] The lion is cold.[(triple2)] The lion needs the rabbit.[(triple3)] The lion sees the rabbit.[(triple4)] The lion sees the tiger.[(triple5)] The rabbit is cold.[(triple6)] The tiger needs the lion.[(triple7)] @1: The tiger eats the lion.[(((triple5) -> rule1))]
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple3
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple4
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple5
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple6
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple7
The tiger eats the lion.
("tiger" "eats" "lion" "+")
((triple5) -> (rule1 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1