[mizar] Error No 9

[Boris Schminke <schminkeba@gmail.com>]

Dear All,
I have suddenly met such an error message:

environ
  vocabularies ZFMISC_1, PRE_TOPC, EUCLID;
  constructors ZFMISC_1, PRE_TOPC, EUCLID;
  notations ZFMISC_1, PRE_TOPC, EUCLID;
  theorems ZFMISC_1;
  registrations MEMBERED;
  requirements SUBSET, NUMERALS;
begin
  reserve A, B, C for Point of (TOP-REAL 2), x, y, z for set;

  A, B, C are_mutually_different implies C, B, A are_mutually_different
  by ZFMISC_1:def 5;
::>,9,9
  A, B, C are_mutually_different implies C, B, A are_mutually_different
  proof
    assume A, B, C are_mutually_different;
    then A <> B & A <> C & B <> C by ZFMISC_1:def 5;
    hence C, B, A are_mutually_different by ZFMISC_1:def 5;
  end;
  x, y, z are_mutually_different implies z, y, x are_mutually_different
  by ZFMISC_1:def 5;
::>,4
::> 4: This inference is not accepted
::> 9: Too many instantiations

>From the last line of this article it's obvious that even without
error No9 the first statement won't be accepted by checker. But I'm
curious about the nature of this error. How instantiations are counted
and what is their maximal number?

--
Yours,
Boris.