John Kalman's book on OTTER on page 217 has the following problem:

"In [this newsletter], Morgan essentially proposed the following problem.

Problem 8.6 Use an automatic theorem-prover to find a proof that the propositional formula CpNNp is derivable by the of condensed detachment from the propositional formulas CpCqp, CCpCqrCCpqCpr, and CCpqCNqNp."

This problem isn't solvable.  Let 0 be the designated element.  Suppose we have only two values "0" and "1", and C(0,x)=x, C(1,x)=0, and N(x)=1.  Then, CpCqp, CCpCqrCCpqCpr, and CCpqCNqNp are satisfied, but CpNNp is not.