The lion eats the tiger. The lion is cold. The lion is green. The lion is rough. The lion is young. The lion needs the tiger. The lion visits the tiger. The tiger eats the lion. The tiger is big. The tiger is cold. The tiger is green. The tiger is rough. The tiger is young. The tiger needs the lion. The tiger visits the lion. If someone eats the lion then the lion is green. If someone is young then they need the tiger. If the tiger is rough and the tiger visits the lion then the tiger needs the lion.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone eats the lion then the lion is green.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "green" "+"))
If someone is young then they need the tiger.
((("someone" "is" "young" "+")) -> ("someone" "needs" "tiger" "+"))
If the tiger is rough and the tiger visits the lion then the tiger needs the lion.
((("tiger" "is" "rough" "+") ("tiger" "visits" "lion" "+")) -> ("tiger" "needs" "lion" "+"))
The lion needs the tiger.
True
1
proof
[(triple6 OR ((triple5) -> rule2))]
("lion" "needs" "tiger" "+")
triple6
((triple5) -> (rule2 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion does not need the tiger.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule2))]
("lion" "needs" "tiger" "-")
triple6
((triple5) -> (rule2 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The lion eats the tiger.[(triple1)] The lion is cold.[(triple2)] The lion is green.[(triple3 OR ((triple8) -> rule1))] The lion is rough.[(triple4)] The lion is young.[(triple5)] The lion needs the tiger.[(triple6 OR ((triple5) -> rule2))] The lion visits the tiger.[(triple7)] The tiger eats the lion.[(triple8)] The tiger is big.[(triple9)] The tiger is cold.[(triple10)] The tiger is green.[(triple11)] The tiger is rough.[(triple12)] The tiger is young.[(triple13)] The tiger needs the lion.[(triple14 OR ((triple12 triple15) -> rule3))] The tiger visits the lion.[(triple15)] @1: The tiger needs the tiger.[(((triple13) -> rule2))]
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is green.
("lion" "is" "green" "+")
triple3
((triple8) -> (rule1 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple6
((triple5) -> (rule2 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple7
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is green.
("tiger" "is" "green" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple14
((triple12 triple15) -> (rule3 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple13) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1