The cat is big. The cat is green. The cat is nice. The cat is rough. The cat is not young. If something is big and not rough then it is young. If the cat is big and the cat is not rough then the cat is green. If something is big and not rough then it is nice.
The cat is big.
("cat" "is" "big" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is not young.
("cat" "is" "young" "-")
If something is big and not rough then it is young.
((("something" "is" "big" "+") ("something" "is" "rough" "~")) -> ("something" "is" "young" "+"))
If the cat is big and the cat is not rough then the cat is green.
((("cat" "is" "big" "+") ("cat" "is" "rough" "~")) -> ("cat" "is" "green" "+"))
If something is big and not rough then it is nice.
((("something" "is" "big" "+") ("something" "is" "rough" "~")) -> ("something" "is" "nice" "+"))
The cat is big.
True
1
proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The cat is not rough.
False
1
inv-proof
[(triple4)]
("cat" "is" "rough" "-")
triple4
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat is big.[(triple1)] The cat is green.[(triple2)] The cat is nice.[(triple3)] The cat is not young.[(triple5)] The cat is rough.[(triple4)]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is not young.
("cat" "is" "young" "-")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple4