]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/tests/TPTP/Veloci/LAT039-1.p.ma
reduced timeout to 100s
[helm.git] / helm / software / matita / tests / TPTP / Veloci / LAT039-1.p.ma
index d9727fe9002f0c248d790491e1c4680c66498369..570d2372434417a723d37f31646cbc0159160bc0 100644 (file)
@@ -70,7 +70,7 @@ theorem rhs:
 \forall H10:\forall X:Univ.eq Univ (meet X X) X.eq Univ (join xx (meet yy zz)) (meet yy (join xx zz))
 .
 intros.
-auto paramodulation timeout=600.
+auto paramodulation timeout=100.
 try assumption.
 print proofterm.
 qed.