Intractability of read-once resolution

Read-once resolution (ROR) is a resolution proof system in which the rule (A+x)(B+x¯)→(A+B) is applied in such a way that two clauses (A+x) and (B+x¯) are replaced by (A+B), i.e., (A+x) and (B+x¯) disappear, and any clause can never be copied. Therefore ROR runs in (nondeterministic) polynomial time and is no longer complete. It is shown that, in spite of its simplicity and weak power ROR is still intractable: (1) the problem whether a CNF formula can be proved by ROR is NP-complete. (2) Let R(k) be a set of formulas f such that f can be proved by ROR but using up to k copy operations. Then R(k)-R(k-1) is D ^P-complete. Thus if we can use one more copy operation then the set of provable formulas enlarges essentially