Inverting First-Order Resolution

θ can be uniquely factored into θ1 and θ2 where θ1 contains all the substitutions involving variables from C1, and θ2 for C2.
So now,
C = (C1 - {L1})θ1 ∪ (C2 - {L2})θ2
which can be re-written as
C - (C1 - {L1})θ1 = (C2 - {L2})θ2
then by definition we have that L2 = ¬L1 θ1 θ2^-1 so
C2 = (C - (C1 - {L1}θ1)θ2^-1 ∪ {¬L1 θ1 θ2^-1}
In applying this we will find multiple choices for L1, θ1, and θ2.