{ unsatisfiable }

conj (<> (c & p), <>(c & p1), [] (-p v -p1))