The lion sees the tiger. The tiger eats the lion. If someone sees the lion then they are kind. If someone is green then they see the lion. If someone sees the tiger then the tiger sees the lion. If someone is big then they need the lion. If someone needs the lion then the lion eats the tiger. If someone is green and they need the tiger then the tiger is big.
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
If someone sees the lion then they are kind.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "kind" "+"))
If someone is green then they see the lion.
((("someone" "is" "green" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the tiger then the tiger sees the lion.
((("someone" "sees" "tiger" "+")) -> ("tiger" "sees" "lion" "+"))
If someone is big then they need the lion.
((("someone" "is" "big" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the lion then the lion eats the tiger.
((("someone" "needs" "lion" "+")) -> ("lion" "eats" "tiger" "+"))
If someone is green and they need the tiger then the tiger is big.
((("someone" "is" "green" "+") ("someone" "needs" "tiger" "+")) -> ("tiger" "is" "big" "+"))
The lion sees the tiger.
True
1
proof
[(triple1)]
("lion" "sees" "tiger" "+")
triple1
The lion does not see the tiger.
False
1
inv-proof
[(triple1)]
("lion" "sees" "tiger" "-")
triple1
The tiger sees the lion.
True
2
proof
[(((triple1) -> rule3))]
("tiger" "sees" "lion" "+")
((triple1) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger does not see the lion.
False
2
inv-proof
[(((triple1) -> rule3))]
("tiger" "sees" "lion" "-")
((triple1) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "lion" "-")
The lion eats the tiger.
Unknown
rconc
[@3: The lion eats the tiger.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule6 <- FAIL)]]
("lion" "eats" "tiger" "+")
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 green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
@0: The lion sees the tiger.[(triple1)] The tiger eats the lion.[(triple2)] @1: The tiger sees the lion.[(((triple1) -> rule3))] @2: The tiger is kind.[(((((triple1) -> rule3)) -> rule1))]
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
((triple1) -> (rule3 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int2