The lion is green. The lion does not need the squirrel. The squirrel eats the tiger. The squirrel needs the lion. The tiger is big. The tiger is young. The tiger needs the lion. If something needs the tiger and the tiger needs the squirrel then the squirrel needs the lion. If something visits the squirrel and it eats the squirrel then the squirrel is not cold. If something needs the lion then the lion is big.
The lion is green.
("lion" "is" "green" "+")
The lion does not need the squirrel.
("lion" "needs" "squirrel" "-")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
If something needs the tiger and the tiger needs the squirrel then the squirrel needs the lion.
((("something" "needs" "tiger" "+") ("tiger" "needs" "squirrel" "+")) -> ("squirrel" "needs" "lion" "+"))
If something visits the squirrel and it eats the squirrel then the squirrel is not cold.
((("something" "visits" "squirrel" "+") ("something" "eats" "squirrel" "+")) -> ("squirrel" "is" "cold" "-"))
If something needs the lion then the lion is big.
((("something" "needs" "lion" "+")) -> ("lion" "is" "big" "+"))
The tiger needs the lion.
True
1
proof
[(triple7)]
("tiger" "needs" "lion" "+")
triple7
The tiger is not big.
False
1
inv-proof
[(triple5)]
("tiger" "is" "big" "-")
triple5
The lion is big.
True
2
proof
[(((triple4) -> rule3) OR ((triple7) -> rule3))]
("lion" "is" "big" "+")
((triple4) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple7) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
2
inv-proof
[(((triple4) -> rule3) OR ((triple7) -> rule3))]
("lion" "is" "big" "-")
((triple4) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple7) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The tiger does not need the squirrel.
Unknown
inv-random
[@0: The tiger needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "squirrel" "-")
The lion is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
The squirrel does not visit the tiger.
Unknown
inv-random
[@0: The squirrel visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "tiger" "-")
The squirrel eats the lion.
Unknown
random
[@0: The squirrel eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "lion" "+")
@0: The lion does not need the squirrel.[(triple2)] The lion is green.[(triple1)] The squirrel eats the tiger.[(triple3)] The squirrel needs the lion.[(triple4)] The tiger is big.[(triple5)] The tiger is young.[(triple6)] The tiger needs the lion.[(triple7)] @1: The lion is big.[(((triple4) -> rule3) OR ((triple7) -> rule3))]
The lion does not need the squirrel.
("lion" "needs" "squirrel" "-")
triple2
The lion is green.
("lion" "is" "green" "+")
triple1
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple3
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple4
The tiger is big.
("tiger" "is" "big" "+")
triple5
The tiger is young.
("tiger" "is" "young" "+")
triple6
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple7
The lion is big.
("lion" "is" "big" "+")
((triple4) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple7) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1