The lion eats the tiger. The lion is blue. The lion is cold. The lion is young. The lion does not need the tiger. The tiger does not eat the lion. The tiger is big. The tiger is cold. The tiger is kind. The tiger needs the lion. If the tiger is kind then the tiger does not see the lion.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is young.
("lion" "is" "young" "+")
The lion does not need the tiger.
("lion" "needs" "tiger" "-")
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If the tiger is kind then the tiger does not see the lion.
((("tiger" "is" "kind" "+")) -> ("tiger" "sees" "lion" "-"))
The tiger is big.
True
1
proof
[(triple7)]
("tiger" "is" "big" "+")
triple7
The lion is not blue.
False
1
inv-proof
[(triple2)]
("lion" "is" "blue" "-")
triple2
The tiger does not see the lion.
True
2
proof
[(((triple9) -> rule1))]
("tiger" "sees" "lion" "-")
((triple9) -> (rule1 % int1))
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
int1
The tiger sees the lion.
False
2
inv-proof
[(((triple9) -> rule1))]
("tiger" "sees" "lion" "+")
((triple9) -> (rule1 % int1))
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
int1
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The lion does not need the tiger.[(triple5)] The lion eats the tiger.[(triple1)] The lion is blue.[(triple2)] The lion is cold.[(triple3)] The lion is young.[(triple4)] The tiger does not eat the lion.[(triple6)] The tiger is big.[(triple7)] The tiger is cold.[(triple8)] The tiger is kind.[(triple9)] The tiger needs the lion.[(triple10)] @1: The tiger does not see the lion.[(((triple9) -> rule1))]
The lion does not need the tiger.
("lion" "needs" "tiger" "-")
triple5
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion is young.
("lion" "is" "young" "+")
triple4
The tiger does not eat the lion.
("tiger" "eats" "lion" "-")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The tiger is cold.
("tiger" "is" "cold" "+")
triple8
The tiger is kind.
("tiger" "is" "kind" "+")
triple9
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple10
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
((triple9) -> (rule1 % int1))
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
int1