Error Number: 9

Mizar Message:

Description

Typical examples

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);
  (A = B implies B = A) & C, B, A are_mutually_different implies A, B, C are_mutually_different by ZFMISC_1:def 5;
::>                                                                                              *9
::> 9: Too many instantiations

Could be eliminated by braking complex sentence into smaller ones:

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);

  A: (A = B implies B = A);
  A, B, C are_mutually_different implies A, B, C are_mutually_different by ZFMISC_1:def 5;
  then (A = B implies B = A) & A, B, C are_mutually_different implies A, B, C are_mutually_different by A;

Weird examples

Please contribute