The lion is big. The lion is not blue. The lion is green. The lion is rough. The lion is young. If the lion is green and the lion is not big then the lion is rough. If the lion is green and the lion is rough then the lion is young.
The lion is big.
("lion" "is" "big" "+")
The lion is not blue.
("lion" "is" "blue" "-")
The lion is green.
("lion" "is" "green" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
If the lion is green and the lion is not big then the lion is rough.
((("lion" "is" "green" "+") ("lion" "is" "big" "~")) -> ("lion" "is" "rough" "+"))
If the lion is green and the lion is rough then the lion is young.
((("lion" "is" "green" "+") ("lion" "is" "rough" "+")) -> ("lion" "is" "young" "+"))
The lion is young.
True
1
proof
[(triple5 OR ((triple3 triple4) -> rule2))]
("lion" "is" "young" "+")
triple5
((triple3 triple4) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is blue.
False
1
inv-proof
[(triple2)]
("lion" "is" "blue" "+")
triple2
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The lion is big.[(triple1)] The lion is green.[(triple3)] The lion is not blue.[(triple2)] The lion is rough.[(triple4)] The lion is young.[(triple5 OR ((triple3 triple4) -> rule2))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is not blue.
("lion" "is" "blue" "-")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
((triple3 triple4) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1