%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : LAT319+1 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sun Jul 17 06:57:12 EDT 2022 % Result : Theorem 2.73s 2.93s % Output : Proof 2.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : LAT319+1 : TPTP v8.1.0. Released v3.4.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n003.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Thu Jun 30 02:00:06 EDT 2022 % 0.12/0.33 % CPUTime : % 2.73/2.93 % SZS status Theorem % 2.73/2.93 (* PROOF-FOUND *) % 2.73/2.93 (* BEGIN-PROOF *) % 2.73/2.93 % SZS output start Proof % 2.73/2.93 1. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.73/2.93 2. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.73/2.93 3. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.73/2.93 4. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.73/2.93 5. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.73/2.93 6. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.73/2.93 7. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.73/2.93 8. (-. (v3_struct_0 (k1_lattice2 T_0))) (v3_struct_0 (k1_lattice2 T_0)) ### Axiom % 2.73/2.93 9. (v10_lattices (k1_lattice2 T_0)) (-. (v10_lattices (k1_lattice2 T_0))) ### Axiom % 2.73/2.93 10. (l3_lattices (k1_lattice2 T_0)) (-. (l3_lattices (k1_lattice2 T_0))) ### Axiom % 2.73/2.93 11. (-. (v3_struct_0 (k1_lattice2 T_0))) (v3_struct_0 (k1_lattice2 T_0)) ### Axiom % 2.73/2.93 12. (v17_lattices (k1_lattice2 T_0)) (-. (v17_lattices (k1_lattice2 T_0))) ### Axiom % 2.73/2.93 13. (-. (v15_lattices (k1_lattice2 T_0))) (v15_lattices (k1_lattice2 T_0)) ### Axiom % 2.73/2.93 14. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v11_lattices (k1_lattice2 T_0)) /\ ((v13_lattices (k1_lattice2 T_0)) /\ ((v14_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ (v16_lattices (k1_lattice2 T_0))))))) (-. (v15_lattices (k1_lattice2 T_0))) ### ConjTree 13 % 2.73/2.93 15. ((l3_lattices (k1_lattice2 T_0)) => (((-. (v3_struct_0 (k1_lattice2 T_0))) /\ (v17_lattices (k1_lattice2 T_0))) => ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v11_lattices (k1_lattice2 T_0)) /\ ((v13_lattices (k1_lattice2 T_0)) /\ ((v14_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ (v16_lattices (k1_lattice2 T_0))))))))) (-. (v15_lattices (k1_lattice2 T_0))) (v17_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (l3_lattices (k1_lattice2 T_0)) ### DisjTree 10 11 12 14 % 2.73/2.93 16. (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (l3_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (v17_lattices (k1_lattice2 T_0)) (-. (v15_lattices (k1_lattice2 T_0))) ### All 15 % 2.73/2.93 17. (l3_lattices (k1_lattice2 T_0)) (-. (l3_lattices (k1_lattice2 T_0))) ### Axiom % 2.73/2.93 18. (-. (v3_struct_0 (k1_lattice2 T_0))) (v3_struct_0 (k1_lattice2 T_0)) ### Axiom % 2.73/2.93 19. (v17_lattices (k1_lattice2 T_0)) (-. (v17_lattices (k1_lattice2 T_0))) ### Axiom % 2.73/2.93 20. (-. (v16_lattices (k1_lattice2 T_0))) (v16_lattices (k1_lattice2 T_0)) ### Axiom % 2.73/2.93 21. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v11_lattices (k1_lattice2 T_0)) /\ ((v13_lattices (k1_lattice2 T_0)) /\ ((v14_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ (v16_lattices (k1_lattice2 T_0))))))) (-. (v16_lattices (k1_lattice2 T_0))) ### ConjTree 20 % 2.73/2.93 22. ((l3_lattices (k1_lattice2 T_0)) => (((-. (v3_struct_0 (k1_lattice2 T_0))) /\ (v17_lattices (k1_lattice2 T_0))) => ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v11_lattices (k1_lattice2 T_0)) /\ ((v13_lattices (k1_lattice2 T_0)) /\ ((v14_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ (v16_lattices (k1_lattice2 T_0))))))))) (-. (v16_lattices (k1_lattice2 T_0))) (v17_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (l3_lattices (k1_lattice2 T_0)) ### DisjTree 17 18 19 21 % 2.73/2.93 23. (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (l3_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (v17_lattices (k1_lattice2 T_0)) (-. (v16_lattices (k1_lattice2 T_0))) ### All 22 % 2.73/2.93 24. (l3_lattices (k1_lattice2 T_0)) (-. (l3_lattices (k1_lattice2 T_0))) ### Axiom % 2.73/2.93 25. (-. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))))) (v17_lattices (k1_lattice2 T_0)) (l3_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (v10_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) ### DisjTree 8 9 16 23 24 % 2.73/2.93 26. (-. (v15_lattices T_0)) (v15_lattices T_0) ### Axiom % 2.73/2.93 27. ((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) (-. (v15_lattices T_0)) ### ConjTree 26 % 2.73/2.93 28. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))))) (-. (v15_lattices T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (v10_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (l3_lattices (k1_lattice2 T_0)) (v17_lattices (k1_lattice2 T_0)) ### Equiv 25 27 % 2.73/2.93 29. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))))) (v17_lattices (k1_lattice2 T_0)) (l3_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (v10_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (-. (v15_lattices T_0)) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 5 6 7 28 % 2.73/2.93 30. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (-. (v15_lattices T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (v10_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (l3_lattices (k1_lattice2 T_0)) (v17_lattices (k1_lattice2 T_0)) ### All 29 % 2.73/2.93 31. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.73/2.93 32. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.73/2.93 33. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.73/2.93 34. (-. (v16_lattices T_0)) (v16_lattices T_0) ### Axiom % 2.73/2.93 35. ((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) (-. (v16_lattices T_0)) ### ConjTree 34 % 2.73/2.93 36. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))))) (-. (v16_lattices T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (v10_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (l3_lattices (k1_lattice2 T_0)) (v17_lattices (k1_lattice2 T_0)) ### Equiv 25 35 % 2.73/2.93 37. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))))) (v17_lattices (k1_lattice2 T_0)) (l3_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (v10_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (-. (v16_lattices T_0)) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 31 32 33 36 % 2.73/2.95 38. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (-. (v16_lattices T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (v10_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (l3_lattices (k1_lattice2 T_0)) (v17_lattices (k1_lattice2 T_0)) ### All 37 % 2.73/2.95 39. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.73/2.95 40. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.73/2.95 41. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.73/2.95 42. (-. (v3_struct_0 (k1_lattice2 T_0))) (v3_struct_0 (k1_lattice2 T_0)) ### Axiom % 2.73/2.95 43. (v10_lattices (k1_lattice2 T_0)) (-. (v10_lattices (k1_lattice2 T_0))) ### Axiom % 2.73/2.95 44. (l3_lattices (k1_lattice2 T_0)) (-. (l3_lattices (k1_lattice2 T_0))) ### Axiom % 2.73/2.95 45. (-. (v3_struct_0 (k1_lattice2 T_0))) (v3_struct_0 (k1_lattice2 T_0)) ### Axiom % 2.73/2.95 46. (v17_lattices (k1_lattice2 T_0)) (-. (v17_lattices (k1_lattice2 T_0))) ### Axiom % 2.73/2.95 47. (-. (v11_lattices (k1_lattice2 T_0))) (v11_lattices (k1_lattice2 T_0)) ### Axiom % 2.73/2.95 48. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v11_lattices (k1_lattice2 T_0)) /\ ((v13_lattices (k1_lattice2 T_0)) /\ ((v14_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ (v16_lattices (k1_lattice2 T_0))))))) (-. (v11_lattices (k1_lattice2 T_0))) ### ConjTree 47 % 2.73/2.95 49. ((l3_lattices (k1_lattice2 T_0)) => (((-. (v3_struct_0 (k1_lattice2 T_0))) /\ (v17_lattices (k1_lattice2 T_0))) => ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v11_lattices (k1_lattice2 T_0)) /\ ((v13_lattices (k1_lattice2 T_0)) /\ ((v14_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ (v16_lattices (k1_lattice2 T_0))))))))) (-. (v11_lattices (k1_lattice2 T_0))) (v17_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (l3_lattices (k1_lattice2 T_0)) ### DisjTree 44 45 46 48 % 2.73/2.95 50. (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (l3_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (v17_lattices (k1_lattice2 T_0)) (-. (v11_lattices (k1_lattice2 T_0))) ### All 49 % 2.73/2.95 51. (l3_lattices (k1_lattice2 T_0)) (-. (l3_lattices (k1_lattice2 T_0))) ### Axiom % 2.73/2.95 52. (-. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v11_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))) (v17_lattices (k1_lattice2 T_0)) (l3_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (v10_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) ### DisjTree 42 43 50 51 % 2.73/2.95 53. (-. (v11_lattices T_0)) (v11_lattices T_0) ### Axiom % 2.73/2.95 54. ((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v11_lattices T_0) /\ (l3_lattices T_0)))) (-. (v11_lattices T_0)) ### ConjTree 53 % 2.73/2.95 55. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v11_lattices T_0) /\ (l3_lattices T_0)))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v11_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))) (-. (v11_lattices T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (v10_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (l3_lattices (k1_lattice2 T_0)) (v17_lattices (k1_lattice2 T_0)) ### Equiv 52 54 % 2.73/2.95 56. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v11_lattices T_0) /\ (l3_lattices T_0)))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v11_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))))) (v17_lattices (k1_lattice2 T_0)) (l3_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (v10_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (-. (v11_lattices T_0)) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 39 40 41 55 % 2.73/2.95 57. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (-. (v11_lattices T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (v10_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (l3_lattices (k1_lattice2 T_0)) (v17_lattices (k1_lattice2 T_0)) ### All 56 % 2.73/2.95 58. (-. ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0)))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (v17_lattices (k1_lattice2 T_0)) (l3_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (v10_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) ### DisjTree 30 38 57 % 2.73/2.95 59. (-. (v17_lattices T_0)) (v17_lattices T_0) ### Axiom % 2.73/2.95 60. ((v17_lattices T_0) <=> ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0)))) (-. (v17_lattices T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (-. (v3_struct_0 (k1_lattice2 T_0))) (v10_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (l3_lattices (k1_lattice2 T_0)) (v17_lattices (k1_lattice2 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) ### Equiv 58 59 % 2.79/2.97 61. (((-. (v3_struct_0 T_0)) /\ (l3_lattices T_0)) => ((v17_lattices T_0) <=> ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (v17_lattices (k1_lattice2 T_0)) (l3_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (v10_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (-. (v17_lattices T_0)) (l3_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 3 4 60 % 2.79/2.97 62. (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (-. (v3_struct_0 T_0)) (l3_lattices T_0) (-. (v17_lattices T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (v10_lattices T_0) (-. (v3_struct_0 (k1_lattice2 T_0))) (v10_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (l3_lattices (k1_lattice2 T_0)) (v17_lattices (k1_lattice2 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) ### All 61 % 2.79/2.97 63. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.79/2.97 64. (-. ((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v17_lattices T_0) /\ (l3_lattices T_0))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (v17_lattices (k1_lattice2 T_0)) (l3_lattices (k1_lattice2 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (v10_lattices (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 1 2 62 63 % 2.79/2.97 65. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v17_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (-. ((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v17_lattices T_0) /\ (l3_lattices T_0))))) ### ConjTree 64 % 2.79/2.97 66. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.79/2.97 67. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.79/2.97 68. (v3_struct_0 (k1_lattice2 T_0)) (-. (v3_struct_0 (k1_lattice2 T_0))) ### Axiom % 2.79/2.97 69. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ (v3_lattices (k1_lattice2 T_0))) (v3_struct_0 (k1_lattice2 T_0)) ### And 68 % 2.79/2.97 70. (((-. (v3_struct_0 T_0)) /\ (l3_lattices T_0)) => ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ (v3_lattices (k1_lattice2 T_0)))) (v3_struct_0 (k1_lattice2 T_0)) (l3_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 66 67 69 % 2.79/2.97 71. (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((-. (v3_struct_0 (k1_lattice2 A))) /\ (v3_lattices (k1_lattice2 A))))) (-. (v3_struct_0 T_0)) (l3_lattices T_0) (v3_struct_0 (k1_lattice2 T_0)) ### All 70 % 2.79/2.97 72. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.79/2.97 73. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.79/2.97 74. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.79/2.97 75. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.79/2.97 76. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.79/2.97 77. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.79/2.97 78. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.79/2.97 79. (v17_lattices T_0) (-. (v17_lattices T_0)) ### Axiom % 2.79/2.97 80. (-. (v11_lattices T_0)) (v11_lattices T_0) ### Axiom % 2.79/2.97 81. ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0))) (-. (v11_lattices T_0)) ### ConjTree 80 % 2.79/2.97 82. ((v17_lattices T_0) <=> ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0)))) (-. (v11_lattices T_0)) (v17_lattices T_0) ### Equiv 79 81 % 2.79/2.97 83. (((-. (v3_struct_0 T_0)) /\ (l3_lattices T_0)) => ((v17_lattices T_0) <=> ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0))))) (v17_lattices T_0) (-. (v11_lattices T_0)) (l3_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 77 78 82 % 2.79/2.97 84. (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (-. (v3_struct_0 T_0)) (l3_lattices T_0) (-. (v11_lattices T_0)) (v17_lattices T_0) ### All 83 % 2.79/2.97 85. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.79/2.97 86. (-. ((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v11_lattices T_0) /\ (l3_lattices T_0))))) (v17_lattices T_0) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 75 76 84 85 % 2.79/3.04 87. (-. (v10_lattices (k1_lattice2 T_0))) (v10_lattices (k1_lattice2 T_0)) ### Axiom % 2.79/3.04 88. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v11_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))) (-. (v10_lattices (k1_lattice2 T_0))) ### ConjTree 87 % 2.79/3.04 89. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v11_lattices T_0) /\ (l3_lattices T_0)))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v11_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))) (-. (v10_lattices (k1_lattice2 T_0))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (l3_lattices T_0) (v17_lattices T_0) ### Equiv 86 88 % 2.79/3.04 90. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v11_lattices T_0) /\ (l3_lattices T_0)))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v11_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))))) (v17_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (-. (v10_lattices (k1_lattice2 T_0))) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 72 73 74 89 % 2.79/3.04 91. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (-. (v10_lattices (k1_lattice2 T_0))) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v17_lattices T_0) ### All 90 % 2.79/3.04 92. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.79/3.04 93. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.79/3.04 94. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.79/3.04 95. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.79/3.04 96. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.79/3.04 97. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.79/3.04 98. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.79/3.04 99. (v17_lattices T_0) (-. (v17_lattices T_0)) ### Axiom % 2.79/3.04 100. (-. (v15_lattices T_0)) (v15_lattices T_0) ### Axiom % 2.79/3.04 101. ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0))) (-. (v15_lattices T_0)) ### ConjTree 100 % 2.79/3.04 102. ((v17_lattices T_0) <=> ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0)))) (-. (v15_lattices T_0)) (v17_lattices T_0) ### Equiv 99 101 % 2.79/3.04 103. (((-. (v3_struct_0 T_0)) /\ (l3_lattices T_0)) => ((v17_lattices T_0) <=> ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0))))) (v17_lattices T_0) (-. (v15_lattices T_0)) (l3_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 97 98 102 % 2.79/3.04 104. (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (-. (v3_struct_0 T_0)) (l3_lattices T_0) (-. (v15_lattices T_0)) (v17_lattices T_0) ### All 103 % 2.79/3.04 105. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.79/3.04 106. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.79/3.04 107. (v17_lattices T_0) (-. (v17_lattices T_0)) ### Axiom % 2.79/3.04 108. (-. (v16_lattices T_0)) (v16_lattices T_0) ### Axiom % 2.79/3.04 109. ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0))) (-. (v16_lattices T_0)) ### ConjTree 108 % 2.79/3.04 110. ((v17_lattices T_0) <=> ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0)))) (-. (v16_lattices T_0)) (v17_lattices T_0) ### Equiv 107 109 % 2.79/3.04 111. (((-. (v3_struct_0 T_0)) /\ (l3_lattices T_0)) => ((v17_lattices T_0) <=> ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (v11_lattices T_0))))) (v17_lattices T_0) (-. (v16_lattices T_0)) (l3_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 105 106 110 % 2.79/3.04 112. (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (-. (v3_struct_0 T_0)) (l3_lattices T_0) (-. (v16_lattices T_0)) (v17_lattices T_0) ### All 111 % 2.79/3.04 113. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.79/3.04 114. (-. ((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0)))))) (v17_lattices T_0) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 95 96 104 112 113 % 2.79/3.04 115. (-. (l3_lattices (k1_lattice2 T_0))) (l3_lattices (k1_lattice2 T_0)) ### Axiom % 2.79/3.04 116. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))) (-. (l3_lattices (k1_lattice2 T_0))) ### ConjTree 115 % 2.79/3.04 117. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))))) (-. (l3_lattices (k1_lattice2 T_0))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (l3_lattices T_0) (v17_lattices T_0) ### Equiv 114 116 % 2.79/3.04 118. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))))) (v17_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (-. (l3_lattices (k1_lattice2 T_0))) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 92 93 94 117 % 2.79/3.04 119. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (-. (l3_lattices (k1_lattice2 T_0))) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v17_lattices T_0) ### All 118 % 2.79/3.04 120. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.79/3.04 121. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.79/3.04 122. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.79/3.04 123. (-. (v15_lattices (k1_lattice2 T_0))) (v15_lattices (k1_lattice2 T_0)) ### Axiom % 2.79/3.04 124. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))) (-. (v15_lattices (k1_lattice2 T_0))) ### ConjTree 123 % 2.79/3.04 125. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))))) (-. (v15_lattices (k1_lattice2 T_0))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (l3_lattices T_0) (v17_lattices T_0) ### Equiv 114 124 % 2.88/3.06 126. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))))) (v17_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (-. (v15_lattices (k1_lattice2 T_0))) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 120 121 122 125 % 2.88/3.06 127. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (-. (v15_lattices (k1_lattice2 T_0))) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v17_lattices T_0) ### All 126 % 2.88/3.06 128. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.88/3.06 129. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.88/3.06 130. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.88/3.06 131. (-. (v16_lattices (k1_lattice2 T_0))) (v16_lattices (k1_lattice2 T_0)) ### Axiom % 2.88/3.06 132. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))) (-. (v16_lattices (k1_lattice2 T_0))) ### ConjTree 131 % 2.88/3.06 133. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))))) (-. (v16_lattices (k1_lattice2 T_0))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (l3_lattices T_0) (v17_lattices T_0) ### Equiv 114 132 % 2.88/3.06 134. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v15_lattices T_0) /\ ((v16_lattices T_0) /\ (l3_lattices T_0))))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))))) (v17_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (-. (v16_lattices (k1_lattice2 T_0))) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 128 129 130 133 % 2.88/3.06 135. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (-. (v16_lattices (k1_lattice2 T_0))) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v17_lattices T_0) ### All 134 % 2.88/3.06 136. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.88/3.06 137. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.88/3.06 138. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.88/3.06 139. (-. (v11_lattices (k1_lattice2 T_0))) (v11_lattices (k1_lattice2 T_0)) ### Axiom % 2.88/3.06 140. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v11_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))) (-. (v11_lattices (k1_lattice2 T_0))) ### ConjTree 139 % 2.88/3.06 141. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v11_lattices T_0) /\ (l3_lattices T_0)))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v11_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))) (-. (v11_lattices (k1_lattice2 T_0))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (l3_lattices T_0) (v17_lattices T_0) ### Equiv 86 140 % 2.88/3.06 142. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v11_lattices T_0) /\ (l3_lattices T_0)))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v11_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))))) (v17_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (-. (v11_lattices (k1_lattice2 T_0))) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 136 137 138 141 % 2.88/3.06 143. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (-. (v11_lattices (k1_lattice2 T_0))) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v17_lattices T_0) ### All 142 % 2.88/3.06 144. (-. ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (v11_lattices (k1_lattice2 T_0))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (v17_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) ### DisjTree 127 135 143 % 2.88/3.06 145. (-. (v17_lattices (k1_lattice2 T_0))) (v17_lattices (k1_lattice2 T_0)) ### Axiom % 2.88/3.06 146. ((v17_lattices (k1_lattice2 T_0)) <=> ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (v11_lattices (k1_lattice2 T_0))))) (-. (v17_lattices (k1_lattice2 T_0))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v17_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) ### Equiv 144 145 % 2.88/3.07 147. (((-. (v3_struct_0 (k1_lattice2 T_0))) /\ (l3_lattices (k1_lattice2 T_0))) => ((v17_lattices (k1_lattice2 T_0)) <=> ((v15_lattices (k1_lattice2 T_0)) /\ ((v16_lattices (k1_lattice2 T_0)) /\ (v11_lattices (k1_lattice2 T_0)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (-. (v17_lattices (k1_lattice2 T_0))) (v17_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (l3_lattices T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((-. (v3_struct_0 (k1_lattice2 A))) /\ (v3_lattices (k1_lattice2 A))))) ### DisjTree 71 119 146 % 2.88/3.07 148. (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((-. (v3_struct_0 (k1_lattice2 A))) /\ (v3_lattices (k1_lattice2 A))))) (-. (v3_struct_0 T_0)) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v17_lattices T_0) (-. (v17_lattices (k1_lattice2 T_0))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) ### All 147 % 2.88/3.07 149. (-. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v17_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (v17_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (l3_lattices T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((-. (v3_struct_0 (k1_lattice2 A))) /\ (v3_lattices (k1_lattice2 A))))) ### DisjTree 71 91 148 119 % 2.88/3.07 150. ((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v17_lattices T_0) /\ (l3_lattices T_0)))) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((-. (v3_struct_0 (k1_lattice2 A))) /\ (v3_lattices (k1_lattice2 A))))) (-. (v3_struct_0 T_0)) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (-. ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v17_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))) ### ConjTree 149 % 2.88/3.07 151. (-. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v17_lattices T_0) /\ (l3_lattices T_0)))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v17_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0))))))) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((-. (v3_struct_0 (k1_lattice2 A))) /\ (v3_lattices (k1_lattice2 A))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### NotEquiv 65 150 % 2.88/3.07 152. (-. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ ((v17_lattices T_0) /\ (l3_lattices T_0)))) <=> ((-. (v3_struct_0 (k1_lattice2 T_0))) /\ ((v10_lattices (k1_lattice2 T_0)) /\ ((v17_lattices (k1_lattice2 T_0)) /\ (l3_lattices (k1_lattice2 T_0)))))))) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((-. (v3_struct_0 (k1_lattice2 A))) /\ (v3_lattices (k1_lattice2 A))))) ### ConjTree 151 % 2.88/3.07 153. (-. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v17_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v17_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((-. (v3_struct_0 (k1_lattice2 A))) /\ (v3_lattices (k1_lattice2 A))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v11_lattices A) /\ (l3_lattices A)))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v11_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A)))))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v17_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v11_lattices A) /\ ((v13_lattices A) /\ ((v14_lattices A) /\ ((v15_lattices A) /\ (v16_lattices A))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ ((v15_lattices A) /\ ((v16_lattices A) /\ (l3_lattices A))))) <=> ((-. (v3_struct_0 (k1_lattice2 A))) /\ ((v10_lattices (k1_lattice2 A)) /\ ((v15_lattices (k1_lattice2 A)) /\ ((v16_lattices (k1_lattice2 A)) /\ (l3_lattices (k1_lattice2 A))))))))) (All A, (((-. (v3_struct_0 A)) /\ (l3_lattices A)) => ((v17_lattices A) <=> ((v15_lattices A) /\ ((v16_lattices A) /\ (v11_lattices A)))))) ### NotAllEx 152 % 2.88/3.08 % SZS output end Proof % 2.88/3.08 (* END-PROOF *) %------------------------------------------------------------------------------