Info:  execution of auto.ma started:
Debug: Executing: ``set "baseuri" "cic:/matita/tests/auto/"''
Debug: Executing: ``include cic:/matita/legacy/coq''
Debug: Executing: ``Theorem a: @[\forall ((x): (@[nat])).(\forall ((y) ...''
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Datatypes/nat.ind
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/eq.ind
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/minus.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult.con
Error: Bad name: a
Debug: Executing: ``intro.''
Debug: Executing: ``auto.''
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/trans_eq.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/z.var
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal3.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal2.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/B.var
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/f.var
WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/add_sub_square_identity.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult_n_Sm.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/TreeAutomata/semantics/conservation_0_0.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/technical_lemma.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/ARITH/Chinese/Nat_complements/technical_lemma.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/plus_minus.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_plus_simpl_l_reverse.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_plus.con
WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/minus_minus.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_plus_distr_r.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_plus_distr_l.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_plus_distr_r.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_plus_distr2.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_n_n.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_n_O.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/minus_minus_lem1.con
WE HAVE NO UNIVERSE FILE FOR cic:/Cachan/SMC/mu/Splus_nm.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_n_Sm.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_Sn_m.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_Snm_nSm.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/TreeAutomata/bases/S_plus_l.con
WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/Qpositive/mult_reg_l.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_reg_l.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_permute_2_in_4.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_permute.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_comm.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_assoc_reverse.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_assoc.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_plus_reg_r.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_plus_reg_l.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/plus_eq.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_permute2.con
WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/minus_eq_decompose.con
WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/Qpositive/minus_decompose.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/minus_eq.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/eq_add_S.con
WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/expand_mult2.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_n_2.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/ring/ArithRing/S_to_plus_one.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/ZArith/BinInt/ZL0.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/S_plus.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_n_SO.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_n_O.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_0_r.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_0_l.con
WE HAVE NO UNIVERSE FILE FOR cic:/Marseille/GC/lib_arith/lib_plus/plus_O_O.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/plus_eqO.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_O_O.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Bertrand/Misc/plus_eqO.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/g0.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/McCarthy/g.var
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/mult_SO.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Bertrand/Misc/mult_SO.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack1.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/Ackermann/Ack.var
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_1_r.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_1_l.con
WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/mult2_recompose.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_n_1.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult_n_O.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_0_r.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_0_l.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_comm.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_assoc_reverse.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_assoc.con
WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/square_recompose.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_sym.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_permut.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_assoc_l.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_mult_reg_r.con
WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_mult_reg_l.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/mult_eq.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_sym.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_permute.con
WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Float/Faux/minus_inv_lt_aux.con
WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_minus_distr_r.con
WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/mult_minus_distr_l.con
Error: Tactic error: No Applicable theorem