Resolution is a scheme to prove unsatisfiability of CNFs. A proof in resolution is a logical deduction of the empty clause for the initial clauses in of the CNF. In particular any initial clause can be inferred, and from two clauses $A \lor x$ and $B \lor \neg{x}$ the clause $A \lor B$ can be deduced as well. A refutation is a sequence of deductions which ends with an empty clause.
If such refutation is implemented, we can consider a procedure that keeps some clauses in memory. In case a non-initial clause must be used again and it is not in memory anymore, the algorithm should must it again from scratch or from the ones in memory.
Let $Sp(F)$ the smallest number of clauses to be kept in memory to reach the empty clauses. This is called the clause space complexity of $F$. We say say that $Sp(F)=\infty$ is $F$ is satisfiable.
The problem I'm suggesting is this: consider two CNFs $A=\bigwedge_{i=1}^m A_i$ and $B=\bigwedge_{j=1}^n B_j$, and let the CNF
$$A \lor B = \bigwedge_{i=1}^m \bigwedge_{j=1}^n A_i \lor B_j$$
What is the relation of $Sp(A \lor B)$ with $Sp(A)$ and $Sp(B)$?
The obvious upper bound is $Sp(A \lor B) \leq Sp(A) + Sp(B) -1$. Is this tight?