The lion eats the tiger. The lion is big. The lion is blue. The lion is cold. The lion is green. The lion is kind. The lion needs the tiger. The lion sees the tiger. The tiger eats the lion. The tiger is big. The tiger is blue. The tiger is cold. The tiger is green. The tiger is kind. The tiger needs the lion. The tiger sees the lion. If the tiger is cold and the tiger eats the lion then the tiger sees the lion. If something is green then it needs the tiger.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If the tiger is cold and the tiger eats the lion then the tiger sees the lion.
((("tiger" "is" "cold" "+") ("tiger" "eats" "lion" "+")) -> ("tiger" "sees" "lion" "+"))
If something is green then it needs the tiger.
((("something" "is" "green" "+")) -> ("something" "needs" "tiger" "+"))
The lion eats the tiger.
True
1
proof
[(triple1)]
("lion" "eats" "tiger" "+")
triple1
The tiger does not see the lion.
False
1
inv-proof
[(triple16 OR ((triple12 triple9) -> rule1))]
("tiger" "sees" "lion" "-")
triple16
((triple12 triple9) -> (rule1 % int1))
The tiger sees 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 sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The lion eats the tiger.[(triple1)] The lion is big.[(triple2)] The lion is blue.[(triple3)] The lion is cold.[(triple4)] The lion is green.[(triple5)] The lion is kind.[(triple6)] The lion needs the tiger.[(triple7 OR ((triple5) -> rule2))] The lion sees the tiger.[(triple8)] The tiger eats the lion.[(triple9)] The tiger is big.[(triple10)] The tiger is blue.[(triple11)] The tiger is cold.[(triple12)] The tiger is green.[(triple13)] The tiger is kind.[(triple14)] The tiger needs the lion.[(triple15)] The tiger sees the lion.[(triple16 OR ((triple12 triple9) -> rule1))] @1: The tiger needs the tiger.[(((triple13) -> rule2))]
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion is green.
("lion" "is" "green" "+")
triple5
The lion is kind.
("lion" "is" "kind" "+")
triple6
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple7
((triple5) -> (rule2 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple8
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
The tiger is cold.
("tiger" "is" "cold" "+")
triple12
The tiger is green.
("tiger" "is" "green" "+")
triple13
The tiger is kind.
("tiger" "is" "kind" "+")
triple14
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple15
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple16
((triple12 triple9) -> (rule1 % int1))
The tiger sees the lion.
("tiger" "sees" "lion" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple13) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1