X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FTPTP%2FHEQ%2FLCL149-1.ma;h=2df109131323f9a555e26a7c67d6f26f1266caa8;hb=e91eb82d2b5e032907758bff0b474d62d57463dc;hp=d0181b85eff9684c92f729ca77e7db4e4f0889b1;hpb=36326bac6e833046698176f50fdbb4517f6705a5;p=helm.git

diff --git a/helm/software/matita/contribs/TPTP/HEQ/LCL149-1.ma b/helm/software/matita/contribs/TPTP/HEQ/LCL149-1.ma
index d0181b85e..2df109131 100644
--- a/helm/software/matita/contribs/TPTP/HEQ/LCL149-1.ma
+++ b/helm/software/matita/contribs/TPTP/HEQ/LCL149-1.ma
@@ -148,7 +148,7 @@ theorem prove_wajsberg_theorem:
  ∀Univ:Set.∀X:Univ.∀Y:Univ.∀Z:Univ.∀big_V:∀_:Univ.∀_:Univ.Univ.∀big_hat:∀_:Univ.∀_:Univ.Univ.∀implies:∀_:Univ.∀_:Univ.Univ.∀not:∀_:Univ.Univ.∀ordered:∀_:Univ.∀_:Univ.Prop.∀truth:Univ.∀x:Univ.∀y:Univ.∀z:Univ.∀H0:∀X:Univ.∀Y:Univ.∀_:eq Univ (implies X Y) truth.ordered X Y.∀H1:∀X:Univ.∀Y:Univ.∀_:ordered X Y.eq Univ (implies X Y) truth.∀H2:∀X:Univ.∀Y:Univ.eq Univ (big_hat X Y) (not (big_V (not X) (not Y))).∀H3:∀X:Univ.∀Y:Univ.eq Univ (big_V X Y) (implies (implies X Y) Y).∀H4:∀X:Univ.∀Y:Univ.eq Univ (implies (implies (not X) (not Y)) (implies Y X)) truth.∀H5:∀X:Univ.∀Y:Univ.eq Univ (implies (implies X Y) Y) (implies (implies Y X) X).∀H6:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (implies (implies X Y) (implies (implies Y Z) (implies X Z))) truth.∀H7:∀X:Univ.eq Univ (implies truth X) X.eq Univ (implies x (big_V y z)) (big_V (implies x y) (implies x z))
 .
 intros.
-autobatch paramodulation timeout=600;
+autobatch depth=5 width=5 size=20 timeout=10;
 try assumption.
 print proofterm.
 qed.