The lion is big. The lion is not kind. The lion is red. The lion is rough. The lion is young. If something is young and kind then it is big. If something is big and not young then it is rough.
The lion is big.
("lion" "is" "big" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
If something is young and kind then it is big.
((("something" "is" "young" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If something is big and not young then it is rough.
((("something" "is" "big" "+") ("something" "is" "young" "~")) -> ("something" "is" "rough" "+"))
The lion is not kind.
True
1
proof
[(triple2)]
("lion" "is" "kind" "-")
triple2
The lion is not rough.
False
1
inv-proof
[(triple4)]
("lion" "is" "rough" "-")
triple4
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 lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The lion is big.[(triple1)] The lion is not kind.[(triple2)] The lion is red.[(triple3)] The lion is rough.[(triple4)] The lion is young.[(triple5)]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is not kind.
("lion" "is" "kind" "-")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5