, whose conjunction is equivalent to . In two cases we prove that the related satisfiability problem is [NP]{}-complete, whereas in the remaining cases we obtain [NP]{}-completeness under the additional assumption that the number of choice terms is constant.  