You can’t influence the length of a proof by placing it at a different position in some list of proofs. Parameter ‘maxsteps’ specifies the maximum length (or Gödel number) of the proofs that get checked, not the maximum number of steps performed by the proof checker algorithm.
You can’t influence the length of a proof by placing it at a different position in some list of proofs. Parameter ‘maxsteps’ specifies the maximum length (or Gödel number) of the proofs that get checked, not the maximum number of steps performed by the proof checker algorithm.
Ouch. maxsteps means maxprooflenght. My inattention, sorry.