An example of backtracking over ∃x.∀y.f(x)≤f(y) acceptable in no logic.

Classical Logic with Constructive Implication and Cut rule: using Stolzenberg Principle, prove that every f:N→N has three 0's or  three non-0's. A Cut between: Stolzenberg Principle and
Stolzenberg
⇒
( ∃x.∃y.∃z.((x<y∧y<z)∧(f(x)=0∧(f(y)=0∧f(z)=0)))
  ∨
  ∃x.∃y.∃z.((x<y∧y<z)∧(f(x)>0∧(f(y)>0∧f(z)>0))))