  In this paper we study an extension of the Polynomial Calculus proof system
where we can introduce new variables and take a square root. We prove that an
instance of the subset-sum principle, the binary value principle, requires
refutations of exponential bit size over rationals in this system.
  Part and Tzameret proved an exponential lower bound on the size of Res-Lin
(Resolution over linear equations) refutations of the binary value principle.
We show that our system p-simulates Res-Lin and thus we get an alternative
exponential lower bound for the size of Res-Lin refutations of the binary value
principle.
