Krishnamurthy (here is the abstract of his paper) showed that resolution augmented with the principle of symmetry forms a proof system (referred to as SR) in which certain formulas (which do not admit short proof in resolution proof system) can exhibit short proofs.
This also holds for the resolution proof augmented with the rule of extension (referred to as ER). He however left open the question if these proof systems SR and ER p-simulate each other.
Is there any recent work on this question?
Does SR polynomially simulate ER?