X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Ftests%2FTPTP%2FVeloci%2FGRP458-1.p.ma;h=44091f50eed3ca30e865be7d43f24db7a8a1a99b;hb=50371578cbaffb42e686a2c4389ba2bb52a2c503;hp=e297b3b08085b2e8e7929164a4e4d93129fb662c;hpb=fa2319814d744d3e374490fe4e4746d9a5c84f1f;p=helm.git diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP458-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP458-1.p.ma index e297b3b08..44091f50e 100644 --- a/helm/software/matita/tests/TPTP/Veloci/GRP458-1.p.ma +++ b/helm/software/matita/tests/TPTP/Veloci/GRP458-1.p.ma @@ -34,7 +34,7 @@ theorem prove_these_axioms_2: \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide (divide A A) (divide A (divide B (divide (divide identity A) C)))) C) B.eq Univ (multiply identity a2) a2 . intros. -autobatch paramodulation timeout=100. +autobatch paramodulation timeout=100; try assumption. print proofterm. qed.