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