Trivial observation on resolution

Hello,

I wonder whether anybody ever looked into the following system. I'm 
sure somebody noticed it already, because it's a total triviality, 
but I didn't see it mentioned anywhere, especially in conjunction to 
the equally trivial considerations I'm going to make.

If I'm not embarrassingly wrong, under the usual conventions for 
system KS, the system

        S{S'{S"{t}}}           S{f}         S[R,R]
    ur----------------- ,   w_------ ,   c_--------
       S[S'{a},S"{-a}]         S{R}          S{R}

is sound and complete for propositional classical logic, as one can 
immediately check by looking at

         S{t}   = S{S'{S"{t}}}
    ai_-------------------------- ,   where S'{ } = { } ,
        S[a,-a] = S[S'{a},S"{a}]            S"{ } = { } ;

      S([R,U],T) = S{S'{S"{t}}}
    s----------------------------- ,   where S'{ } = ([R,{ }],T) ,
      S[(R,T),U] = S[S'{f},S"{t}]            S"{ } = (U,{ }) .

In this system, weakening and contraction are non-atomic, and switch 
and interaction are merged into the rule ur (ultra-resolution, sorry 
for the name but it's late, actually, it's almost time to bring the 
kids to school).

Together with contraction, the rule ur is more general than 
resolution, in fact one can do

           (R,T)      = S{S'{S"{t}}}               S{ } = { } ,
    ur--------------------------------- ,   where S'{ } = (R,{ }) ,
       [(R,a),(-a,T)] = S[S'{a},S"{a}]            S"{ } = ({ },T) .

which is nothing else than resolution in its positive form. Notice 
that for resolution we ask for the context S{ } to be empty, and for 
the formula to be proved to be in disjunctive normal form.

Now, contrary to resolution, the rule ur does not require any normal 
form and can be applied deeply. The bookkeeping associated to it, and 
which is embodied by weakening and contraction, is the same as for 
resolution.

So, the question is: it looks like, not requiring a normal form to 
start with, the system above provides for an exponential speed-up 
over resolution proofs. Anybody knows anything about this already? Is 
what I'm saying reasonable, correct, etc.? If so, I think it's 
material that could go in the paper Paola and I are writing about 
proof complexity.

Ciao,

-Alessio