The cat is big. The cat is not green. The cat is not kind. The cat is red. The cat is not young. All green people are young. If someone is kind and not green then they are red. If someone is green then they are kind.
The cat is big.
("cat" "is" "big" "+")
The cat is not green.
("cat" "is" "green" "-")
The cat is not kind.
("cat" "is" "kind" "-")
The cat is red.
("cat" "is" "red" "+")
The cat is not young.
("cat" "is" "young" "-")
All green people are young.
((("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and not green then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "red" "+"))
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
The cat is not green.
True
1
proof
[(triple2)]
("cat" "is" "green" "-")
triple2
The cat is kind.
False
1
inv-proof
[(triple3)]
("cat" "is" "kind" "+")
triple3
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
@0: The cat is big.[(triple1)] The cat is not green.[(triple2)] The cat is not kind.[(triple3)] The cat is not young.[(triple5)] The cat is red.[(triple4)]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is not green.
("cat" "is" "green" "-")
triple2
The cat is not kind.
("cat" "is" "kind" "-")
triple3
The cat is not young.
("cat" "is" "young" "-")
triple5
The cat is red.
("cat" "is" "red" "+")
triple4