X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2FTPTP%2FVeloci%2FGRP145-1.p.ma;h=032cdfd55a72b4cab42112b2ad330e1a3a1f197d;hb=4441b81ba3179696c42ebc8ab720d1ba0f67078a;hp=63b6c5087e7a8c0eca1abc9e03ad9a9ffd7c140c;hpb=d765468f2df1976b995a2047fe76a6032c84840b;p=helm.git

diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP145-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP145-1.p.ma
index 63b6c5087..032cdfd55 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP145-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP145-1.p.ma
@@ -110,7 +110,7 @@ theorem prove_ax_glb3b:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (greatest_lower_bound a b) b) (greatest_lower_bound a b)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.