\e[0;32mInfo: \e[0mexecution of auto.ma started:
\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/tests/auto/"''
\e[0;32mInfo: \e[0mexecution of auto.ma started:
\e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/tests/auto/"''
\e[0;34mDebug: \e[0mExecuting: ``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
\e[0;34mDebug: \e[0mExecuting: ``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