The lion is green. The lion is red. The lion is young. If the lion is red and the lion is big then the lion is green. All red, green things are big.
The lion is green.
("lion" "is" "green" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
If the lion is red and the lion is big then the lion is green.
((("lion" "is" "red" "+") ("lion" "is" "big" "+")) -> ("lion" "is" "green" "+"))
All red, green things are big.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
The lion is young.
True
1
proof
[(triple3)]
("lion" "is" "young" "+")
triple3
The lion is not green.
False
1
inv-proof
[(triple1)]
("lion" "is" "green" "-")
triple1
The lion is big.
True
3
proof
[(((triple2 triple1) -> rule2))]
("lion" "is" "big" "+")
((triple2 triple1) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("lion" "is" "big" "-")
((triple2 triple1) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
The lion is not blue.
Unknown
inv-random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The lion is green.[(triple1)] The lion is red.[(triple2)] The lion is young.[(triple3)] @1: The lion is big.[(((triple2 triple1) -> rule2))]
The lion is green.
("lion" "is" "green" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The lion is young.
("lion" "is" "young" "+")
triple3
The lion is big.
("lion" "is" "big" "+")
((triple2 triple1) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1