Higher order proof reconstruction from paramodulation-based refutations: the unit equality case.