%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : GRP653+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 : n024.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 : Sat Jul 16 11:55:30 EDT 2022 % Result : Theorem 2.83s 3.03s % Output : Proof 3.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : GRP653+1 : TPTP v8.1.0. Released v3.4.0. % 0.12/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jun 14 12:08:18 EDT 2022 % 0.13/0.34 % CPUTime : % 2.83/3.03 % SZS status Theorem % 2.83/3.03 (* PROOF-FOUND *) % 2.83/3.03 (* BEGIN-PROOF *) % 2.83/3.03 % SZS output start Proof % 2.83/3.03 1. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.83/3.03 2. (v3_group_1 T_0) (-. (v3_group_1 T_0)) ### Axiom % 2.83/3.03 3. (v4_group_1 T_0) (-. (v4_group_1 T_0)) ### Axiom % 2.83/3.03 4. (l1_group_1 T_0) (-. (l1_group_1 T_0)) ### Axiom % 2.83/3.03 5. (v3_struct_0 (k11_group_4 T_0)) (-. (v3_struct_0 (k11_group_4 T_0))) ### Axiom % 2.83/3.03 6. ((-. (v3_struct_0 (k11_group_4 T_0))) /\ ((v3_lattices (k11_group_4 T_0)) /\ ((v4_lattices (k11_group_4 T_0)) /\ ((v5_lattices (k11_group_4 T_0)) /\ ((v6_lattices (k11_group_4 T_0)) /\ ((v7_lattices (k11_group_4 T_0)) /\ ((v8_lattices (k11_group_4 T_0)) /\ ((v9_lattices (k11_group_4 T_0)) /\ ((v10_lattices (k11_group_4 T_0)) /\ ((v13_lattices (k11_group_4 T_0)) /\ ((v14_lattices (k11_group_4 T_0)) /\ (v15_lattices (k11_group_4 T_0))))))))))))) (v3_struct_0 (k11_group_4 T_0)) ### ConjTree 5 % 2.83/3.03 7. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ (l1_group_1 T_0)))) => ((-. (v3_struct_0 (k11_group_4 T_0))) /\ ((v3_lattices (k11_group_4 T_0)) /\ ((v4_lattices (k11_group_4 T_0)) /\ ((v5_lattices (k11_group_4 T_0)) /\ ((v6_lattices (k11_group_4 T_0)) /\ ((v7_lattices (k11_group_4 T_0)) /\ ((v8_lattices (k11_group_4 T_0)) /\ ((v9_lattices (k11_group_4 T_0)) /\ ((v10_lattices (k11_group_4 T_0)) /\ ((v13_lattices (k11_group_4 T_0)) /\ ((v14_lattices (k11_group_4 T_0)) /\ (v15_lattices (k11_group_4 T_0)))))))))))))) (v3_struct_0 (k11_group_4 T_0)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### DisjTree 1 2 3 4 6 % 2.83/3.03 8. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (v3_struct_0 (k11_group_4 T_0)) ### All 7 % 2.83/3.03 9. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.83/3.03 10. (v3_group_1 T_0) (-. (v3_group_1 T_0)) ### Axiom % 2.83/3.03 11. (v4_group_1 T_0) (-. (v4_group_1 T_0)) ### Axiom % 2.83/3.03 12. (l1_group_1 T_0) (-. (l1_group_1 T_0)) ### Axiom % 2.83/3.03 13. (-. (v10_lattices (k11_group_4 T_0))) (v10_lattices (k11_group_4 T_0)) ### Axiom % 2.83/3.03 14. ((-. (v3_struct_0 (k11_group_4 T_0))) /\ ((v3_lattices (k11_group_4 T_0)) /\ ((v4_lattices (k11_group_4 T_0)) /\ ((v5_lattices (k11_group_4 T_0)) /\ ((v6_lattices (k11_group_4 T_0)) /\ ((v7_lattices (k11_group_4 T_0)) /\ ((v8_lattices (k11_group_4 T_0)) /\ ((v9_lattices (k11_group_4 T_0)) /\ ((v10_lattices (k11_group_4 T_0)) /\ ((v13_lattices (k11_group_4 T_0)) /\ ((v14_lattices (k11_group_4 T_0)) /\ (v15_lattices (k11_group_4 T_0))))))))))))) (-. (v10_lattices (k11_group_4 T_0))) ### ConjTree 13 % 2.83/3.03 15. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ (l1_group_1 T_0)))) => ((-. (v3_struct_0 (k11_group_4 T_0))) /\ ((v3_lattices (k11_group_4 T_0)) /\ ((v4_lattices (k11_group_4 T_0)) /\ ((v5_lattices (k11_group_4 T_0)) /\ ((v6_lattices (k11_group_4 T_0)) /\ ((v7_lattices (k11_group_4 T_0)) /\ ((v8_lattices (k11_group_4 T_0)) /\ ((v9_lattices (k11_group_4 T_0)) /\ ((v10_lattices (k11_group_4 T_0)) /\ ((v13_lattices (k11_group_4 T_0)) /\ ((v14_lattices (k11_group_4 T_0)) /\ (v15_lattices (k11_group_4 T_0)))))))))))))) (-. (v10_lattices (k11_group_4 T_0))) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### DisjTree 9 10 11 12 14 % 2.83/3.03 16. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (v10_lattices (k11_group_4 T_0))) ### All 15 % 2.83/3.03 17. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.83/3.03 18. (v3_group_1 T_0) (-. (v3_group_1 T_0)) ### Axiom % 2.83/3.03 19. (v4_group_1 T_0) (-. (v4_group_1 T_0)) ### Axiom % 2.83/3.03 20. (l1_group_1 T_0) (-. (l1_group_1 T_0)) ### Axiom % 2.83/3.03 21. (-. (l3_lattices (k11_group_4 T_0))) (l3_lattices (k11_group_4 T_0)) ### Axiom % 2.83/3.03 22. ((-. (v3_struct_0 (k11_group_4 T_0))) /\ ((v3_lattices (k11_group_4 T_0)) /\ ((v10_lattices (k11_group_4 T_0)) /\ (l3_lattices (k11_group_4 T_0))))) (-. (l3_lattices (k11_group_4 T_0))) ### ConjTree 21 % 2.83/3.03 23. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ (l1_group_1 T_0)))) => ((-. (v3_struct_0 (k11_group_4 T_0))) /\ ((v3_lattices (k11_group_4 T_0)) /\ ((v10_lattices (k11_group_4 T_0)) /\ (l3_lattices (k11_group_4 T_0)))))) (-. (l3_lattices (k11_group_4 T_0))) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### DisjTree 17 18 19 20 22 % 2.83/3.03 24. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (l3_lattices (k11_group_4 T_0))) ### All 23 % 2.83/3.03 25. (-. (v3_struct_0 T_1)) (v3_struct_0 T_1) ### Axiom % 2.83/3.03 26. (v3_group_1 T_1) (-. (v3_group_1 T_1)) ### Axiom % 2.83/3.03 27. (v4_group_1 T_1) (-. (v4_group_1 T_1)) ### Axiom % 2.83/3.03 28. (l1_group_1 T_1) (-. (l1_group_1 T_1)) ### Axiom % 2.83/3.03 29. (v3_struct_0 (k11_group_4 T_1)) (-. (v3_struct_0 (k11_group_4 T_1))) ### Axiom % 2.83/3.03 30. ((-. (v3_struct_0 (k11_group_4 T_1))) /\ ((v3_lattices (k11_group_4 T_1)) /\ ((v4_lattices (k11_group_4 T_1)) /\ ((v5_lattices (k11_group_4 T_1)) /\ ((v6_lattices (k11_group_4 T_1)) /\ ((v7_lattices (k11_group_4 T_1)) /\ ((v8_lattices (k11_group_4 T_1)) /\ ((v9_lattices (k11_group_4 T_1)) /\ ((v10_lattices (k11_group_4 T_1)) /\ ((v13_lattices (k11_group_4 T_1)) /\ ((v14_lattices (k11_group_4 T_1)) /\ (v15_lattices (k11_group_4 T_1))))))))))))) (v3_struct_0 (k11_group_4 T_1)) ### ConjTree 29 % 2.83/3.03 31. (((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ (l1_group_1 T_1)))) => ((-. (v3_struct_0 (k11_group_4 T_1))) /\ ((v3_lattices (k11_group_4 T_1)) /\ ((v4_lattices (k11_group_4 T_1)) /\ ((v5_lattices (k11_group_4 T_1)) /\ ((v6_lattices (k11_group_4 T_1)) /\ ((v7_lattices (k11_group_4 T_1)) /\ ((v8_lattices (k11_group_4 T_1)) /\ ((v9_lattices (k11_group_4 T_1)) /\ ((v10_lattices (k11_group_4 T_1)) /\ ((v13_lattices (k11_group_4 T_1)) /\ ((v14_lattices (k11_group_4 T_1)) /\ (v15_lattices (k11_group_4 T_1)))))))))))))) (v3_struct_0 (k11_group_4 T_1)) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) ### DisjTree 25 26 27 28 30 % 2.83/3.03 32. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v3_struct_0 (k11_group_4 T_1)) ### All 31 % 2.83/3.03 33. (-. (v3_struct_0 T_1)) (v3_struct_0 T_1) ### Axiom % 2.83/3.03 34. (v3_group_1 T_1) (-. (v3_group_1 T_1)) ### Axiom % 2.83/3.03 35. (v4_group_1 T_1) (-. (v4_group_1 T_1)) ### Axiom % 2.83/3.03 36. (l1_group_1 T_1) (-. (l1_group_1 T_1)) ### Axiom % 2.83/3.03 37. (-. (v10_lattices (k11_group_4 T_1))) (v10_lattices (k11_group_4 T_1)) ### Axiom % 2.83/3.03 38. ((-. (v3_struct_0 (k11_group_4 T_1))) /\ ((v3_lattices (k11_group_4 T_1)) /\ ((v4_lattices (k11_group_4 T_1)) /\ ((v5_lattices (k11_group_4 T_1)) /\ ((v6_lattices (k11_group_4 T_1)) /\ ((v7_lattices (k11_group_4 T_1)) /\ ((v8_lattices (k11_group_4 T_1)) /\ ((v9_lattices (k11_group_4 T_1)) /\ ((v10_lattices (k11_group_4 T_1)) /\ ((v13_lattices (k11_group_4 T_1)) /\ ((v14_lattices (k11_group_4 T_1)) /\ (v15_lattices (k11_group_4 T_1))))))))))))) (-. (v10_lattices (k11_group_4 T_1))) ### ConjTree 37 % 2.83/3.07 39. (((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ (l1_group_1 T_1)))) => ((-. (v3_struct_0 (k11_group_4 T_1))) /\ ((v3_lattices (k11_group_4 T_1)) /\ ((v4_lattices (k11_group_4 T_1)) /\ ((v5_lattices (k11_group_4 T_1)) /\ ((v6_lattices (k11_group_4 T_1)) /\ ((v7_lattices (k11_group_4 T_1)) /\ ((v8_lattices (k11_group_4 T_1)) /\ ((v9_lattices (k11_group_4 T_1)) /\ ((v10_lattices (k11_group_4 T_1)) /\ ((v13_lattices (k11_group_4 T_1)) /\ ((v14_lattices (k11_group_4 T_1)) /\ (v15_lattices (k11_group_4 T_1)))))))))))))) (-. (v10_lattices (k11_group_4 T_1))) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) ### DisjTree 33 34 35 36 38 % 2.83/3.07 40. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (-. (v10_lattices (k11_group_4 T_1))) ### All 39 % 2.83/3.07 41. (-. (v3_struct_0 T_1)) (v3_struct_0 T_1) ### Axiom % 2.83/3.07 42. (v3_group_1 T_1) (-. (v3_group_1 T_1)) ### Axiom % 2.83/3.07 43. (v4_group_1 T_1) (-. (v4_group_1 T_1)) ### Axiom % 2.83/3.07 44. (l1_group_1 T_1) (-. (l1_group_1 T_1)) ### Axiom % 2.83/3.07 45. (-. (l3_lattices (k11_group_4 T_1))) (l3_lattices (k11_group_4 T_1)) ### Axiom % 2.83/3.07 46. ((-. (v3_struct_0 (k11_group_4 T_1))) /\ ((v3_lattices (k11_group_4 T_1)) /\ ((v10_lattices (k11_group_4 T_1)) /\ (l3_lattices (k11_group_4 T_1))))) (-. (l3_lattices (k11_group_4 T_1))) ### ConjTree 45 % 2.83/3.07 47. (((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ (l1_group_1 T_1)))) => ((-. (v3_struct_0 (k11_group_4 T_1))) /\ ((v3_lattices (k11_group_4 T_1)) /\ ((v10_lattices (k11_group_4 T_1)) /\ (l3_lattices (k11_group_4 T_1)))))) (-. (l3_lattices (k11_group_4 T_1))) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) ### DisjTree 41 42 43 44 46 % 2.83/3.07 48. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (-. (l3_lattices (k11_group_4 T_1))) ### All 47 % 2.83/3.07 49. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.83/3.07 50. (v3_group_1 T_0) (-. (v3_group_1 T_0)) ### Axiom % 2.83/3.07 51. (v4_group_1 T_0) (-. (v4_group_1 T_0)) ### Axiom % 2.83/3.07 52. (l1_group_1 T_0) (-. (l1_group_1 T_0)) ### Axiom % 2.83/3.07 53. (-. (v3_struct_0 T_1)) (v3_struct_0 T_1) ### Axiom % 2.83/3.07 54. (v3_group_1 T_1) (-. (v3_group_1 T_1)) ### Axiom % 2.83/3.07 55. (v4_group_1 T_1) (-. (v4_group_1 T_1)) ### Axiom % 2.83/3.07 56. (l1_group_1 T_1) (-. (l1_group_1 T_1)) ### Axiom % 2.83/3.07 57. (v1_funct_1 T_2) (-. (v1_funct_1 T_2)) ### Axiom % 2.83/3.07 58. (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))) ### Axiom % 2.83/3.07 59. (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))) ### Axiom % 2.83/3.07 60. (-. (v1_funct_1 (k3_latsubgr T_0 T_1 T_2))) (v1_funct_1 (k3_latsubgr T_0 T_1 T_2)) ### Axiom % 2.83/3.07 61. ((v1_funct_1 (k3_latsubgr T_0 T_1 T_2)) /\ ((v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))))) (-. (v1_funct_1 (k3_latsubgr T_0 T_1 T_2))) ### ConjTree 60 % 2.83/3.07 62. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ ((l1_group_1 T_0) /\ ((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ ((l1_group_1 T_1) /\ ((v1_funct_1 T_2) /\ ((v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)))))))))))) => ((v1_funct_1 (k3_latsubgr T_0 T_1 T_2)) /\ ((v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))))) (-. (v1_funct_1 (k3_latsubgr T_0 T_1 T_2))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### DisjTree 49 50 51 52 53 54 55 56 57 58 59 61 % 2.83/3.07 63. (All C, (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ ((l1_group_1 T_0) /\ ((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ ((l1_group_1 T_1) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (m1_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)))))))))))) => ((v1_funct_1 (k3_latsubgr T_0 T_1 C)) /\ ((v1_funct_2 (k3_latsubgr T_0 T_1 C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 (k3_latsubgr T_0 T_1 C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (v1_funct_1 (k3_latsubgr T_0 T_1 T_2))) ### All 62 % 2.83/3.07 64. (All B, (All C, (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ ((l1_group_1 T_0) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr T_0 B C)) /\ ((v1_funct_2 (k3_latsubgr T_0 B C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr T_0 B C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 B)))))))) (-. (v1_funct_1 (k3_latsubgr T_0 T_1 T_2))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### All 63 % 2.83/3.07 65. (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (v1_funct_1 (k3_latsubgr T_0 T_1 T_2))) ### All 64 % 2.83/3.07 66. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.83/3.07 67. (v3_group_1 T_0) (-. (v3_group_1 T_0)) ### Axiom % 2.83/3.07 68. (v4_group_1 T_0) (-. (v4_group_1 T_0)) ### Axiom % 2.83/3.07 69. (l1_group_1 T_0) (-. (l1_group_1 T_0)) ### Axiom % 2.83/3.07 70. (-. (v3_struct_0 T_1)) (v3_struct_0 T_1) ### Axiom % 2.83/3.07 71. (v3_group_1 T_1) (-. (v3_group_1 T_1)) ### Axiom % 2.83/3.07 72. (v4_group_1 T_1) (-. (v4_group_1 T_1)) ### Axiom % 2.96/3.18 73. (l1_group_1 T_1) (-. (l1_group_1 T_1)) ### Axiom % 2.96/3.18 74. (v1_funct_1 T_2) (-. (v1_funct_1 T_2)) ### Axiom % 2.96/3.18 75. (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))) ### Axiom % 2.96/3.18 76. (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))) ### Axiom % 2.96/3.18 77. (-. (v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) (v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) ### Axiom % 2.96/3.18 78. ((v1_funct_1 (k3_latsubgr T_0 T_1 T_2)) /\ ((v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))))) (-. (v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) ### ConjTree 77 % 2.96/3.18 79. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ ((l1_group_1 T_0) /\ ((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ ((l1_group_1 T_1) /\ ((v1_funct_1 T_2) /\ ((v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)))))))))))) => ((v1_funct_1 (k3_latsubgr T_0 T_1 T_2)) /\ ((v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))))) (-. (v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### DisjTree 66 67 68 69 70 71 72 73 74 75 76 78 % 2.96/3.18 80. (All C, (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ ((l1_group_1 T_0) /\ ((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ ((l1_group_1 T_1) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (m1_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)))))))))))) => ((v1_funct_1 (k3_latsubgr T_0 T_1 C)) /\ ((v1_funct_2 (k3_latsubgr T_0 T_1 C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 (k3_latsubgr T_0 T_1 C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) ### All 79 % 2.96/3.18 81. (All B, (All C, (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ ((l1_group_1 T_0) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr T_0 B C)) /\ ((v1_funct_2 (k3_latsubgr T_0 B C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr T_0 B C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 B)))))))) (-. (v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### All 80 % 2.96/3.18 82. (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) ### All 81 % 2.96/3.18 83. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.96/3.18 84. (v3_group_1 T_0) (-. (v3_group_1 T_0)) ### Axiom % 2.96/3.18 85. (v4_group_1 T_0) (-. (v4_group_1 T_0)) ### Axiom % 2.96/3.18 86. (l1_group_1 T_0) (-. (l1_group_1 T_0)) ### Axiom % 2.96/3.18 87. (-. (v3_struct_0 T_1)) (v3_struct_0 T_1) ### Axiom % 2.96/3.18 88. (v3_group_1 T_1) (-. (v3_group_1 T_1)) ### Axiom % 2.96/3.18 89. (v4_group_1 T_1) (-. (v4_group_1 T_1)) ### Axiom % 2.96/3.18 90. (l1_group_1 T_1) (-. (l1_group_1 T_1)) ### Axiom % 2.96/3.18 91. (v1_funct_1 T_2) (-. (v1_funct_1 T_2)) ### Axiom % 2.96/3.18 92. (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))) ### Axiom % 2.96/3.18 93. (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))) ### Axiom % 2.96/3.18 94. (-. (m1_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) (m1_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) ### Axiom % 2.96/3.18 95. (m2_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) (-. (m1_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) ### Definition-Pseudo(m2_relset_1) 94 % 2.96/3.18 96. ((v1_funct_1 (k3_latsubgr T_0 T_1 T_2)) /\ ((v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))))) (-. (m1_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) ### ConjTree 95 % 2.96/3.18 97. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ ((l1_group_1 T_0) /\ ((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ ((l1_group_1 T_1) /\ ((v1_funct_1 T_2) /\ ((v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)))))))))))) => ((v1_funct_1 (k3_latsubgr T_0 T_1 T_2)) /\ ((v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))))) (-. (m1_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### DisjTree 83 84 85 86 87 88 89 90 91 92 93 96 % 2.96/3.18 98. (All C, (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ ((l1_group_1 T_0) /\ ((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ ((l1_group_1 T_1) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (m1_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)))))))))))) => ((v1_funct_1 (k3_latsubgr T_0 T_1 C)) /\ ((v1_funct_2 (k3_latsubgr T_0 T_1 C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 (k3_latsubgr T_0 T_1 C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m1_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) ### All 97 % 3.36/3.52 99. (All B, (All C, (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ ((l1_group_1 T_0) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr T_0 B C)) /\ ((v1_funct_2 (k3_latsubgr T_0 B C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr T_0 B C) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 B)))))))) (-. (m1_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### All 98 % 3.36/3.52 100. (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m1_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) ### All 99 % 3.36/3.52 101. (-. (m2_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1)))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) ### Definition-Pseudo(m2_relset_1) 100 % 3.36/3.52 102. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 3.36/3.52 103. (v3_group_1 T_0) (-. (v3_group_1 T_0)) ### Axiom % 3.36/3.52 104. (v4_group_1 T_0) (-. (v4_group_1 T_0)) ### Axiom % 3.36/3.52 105. (l1_group_1 T_0) (-. (l1_group_1 T_0)) ### Axiom % 3.36/3.52 106. (-. (v3_struct_0 T_1)) (v3_struct_0 T_1) ### Axiom % 3.36/3.52 107. (v3_group_1 T_1) (-. (v3_group_1 T_1)) ### Axiom % 3.36/3.52 108. (v4_group_1 T_1) (-. (v4_group_1 T_1)) ### Axiom % 3.36/3.52 109. (l1_group_1 T_1) (-. (l1_group_1 T_1)) ### Axiom % 3.36/3.52 110. (v1_funct_1 T_2) (-. (v1_funct_1 T_2)) ### Axiom % 3.36/3.52 111. (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))) ### Axiom % 3.36/3.52 112. (v1_group_6 T_2 T_0 T_1) (-. (v1_group_6 T_2 T_0 T_1)) ### Axiom % 3.36/3.52 113. (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))) ### Axiom % 3.36/3.52 114. (-. (m2_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) ### Definition-Pseudo(m2_relset_1) 113 % 3.36/3.52 115. (-. (m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1)) ### Axiom % 3.36/3.52 116. (((v1_funct_1 T_2) /\ ((v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v1_group_6 T_2 T_0 T_1) /\ (m2_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))))) => (m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (-. (m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) ### DisjTree 110 111 112 114 115 % 3.36/3.52 117. (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v1_group_6 C T_0 T_1) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1))))) => (m4_vectsp_8 (k3_latsubgr T_0 T_1 C) (k11_group_4 T_0) (k11_group_4 T_1)))) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) ### All 116 % 3.36/3.52 118. (((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ (l1_group_1 T_1)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v1_group_6 C T_0 T_1) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1))))) => (m4_vectsp_8 (k3_latsubgr T_0 T_1 C) (k11_group_4 T_0) (k11_group_4 T_1))))) (-. (m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) ### DisjTree 106 107 108 109 117 % 3.36/3.52 119. (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ ((v1_group_6 C T_0 B) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr T_0 B C) (k11_group_4 T_0) (k11_group_4 B)))))) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) ### All 118 % 3.36/3.52 120. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ (l1_group_1 T_0)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ ((v1_group_6 C T_0 B) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr T_0 B C) (k11_group_4 T_0) (k11_group_4 B))))))) (-. (m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### DisjTree 102 103 104 105 119 % 3.36/3.52 121. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) ### All 120 % 3.36/3.53 122. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 3.36/3.53 123. (v3_group_1 T_0) (-. (v3_group_1 T_0)) ### Axiom % 3.36/3.53 124. (v4_group_1 T_0) (-. (v4_group_1 T_0)) ### Axiom % 3.36/3.53 125. (l1_group_1 T_0) (-. (l1_group_1 T_0)) ### Axiom % 3.36/3.53 126. (-. (v3_struct_0 T_1)) (v3_struct_0 T_1) ### Axiom % 3.36/3.53 127. (v3_group_1 T_1) (-. (v3_group_1 T_1)) ### Axiom % 3.36/3.53 128. (v4_group_1 T_1) (-. (v4_group_1 T_1)) ### Axiom % 3.36/3.53 129. (l1_group_1 T_1) (-. (l1_group_1 T_1)) ### Axiom % 3.36/3.53 130. (v1_funct_1 T_2) (-. (v1_funct_1 T_2)) ### Axiom % 3.36/3.53 131. (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))) ### Axiom % 3.36/3.53 132. (v1_group_6 T_2 T_0 T_1) (-. (v1_group_6 T_2 T_0 T_1)) ### Axiom % 3.36/3.53 133. (v2_funct_1 T_2) (-. (v2_funct_1 T_2)) ### Axiom % 3.36/3.53 134. (-. (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1)) ### Axiom % 3.36/3.53 135. (((v1_funct_1 T_2) /\ ((v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v1_group_6 T_2 T_0 T_1) /\ (m2_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))))) => ((v2_funct_1 T_2) => (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1)))) (-. (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (v2_funct_1 T_2) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) ### DisjTree 130 131 132 114 133 134 % 3.36/3.53 136. (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v1_group_6 C T_0 T_1) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr T_0 T_1 C) (k11_group_4 T_0) (k11_group_4 T_1))))) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v2_funct_1 T_2) (-. (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) ### All 135 % 3.36/3.53 137. (((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ (l1_group_1 T_1)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v1_group_6 C T_0 T_1) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr T_0 T_1 C) (k11_group_4 T_0) (k11_group_4 T_1)))))) (-. (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (v2_funct_1 T_2) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) ### DisjTree 126 127 128 129 136 % 3.36/3.53 138. (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ ((v1_group_6 C T_0 B) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr T_0 B C) (k11_group_4 T_0) (k11_group_4 B))))))) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v2_funct_1 T_2) (-. (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) ### All 137 % 3.36/3.53 139. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ (l1_group_1 T_0)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ ((v1_group_6 C T_0 B) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr T_0 B C) (k11_group_4 T_0) (k11_group_4 B)))))))) (-. (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (v2_funct_1 T_2) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### DisjTree 122 123 124 125 138 % 3.36/3.53 140. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v2_funct_1 T_2) (-. (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) ### All 139 % 3.36/3.53 141. (-. ((m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1)) /\ (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1)))) (v2_funct_1 T_2) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) ### NotAnd 121 140 % 3.36/3.53 142. (-. (m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1)) ### Axiom % 3.36/3.53 143. ((m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1)) <=> ((m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1)) /\ (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1)))) (-. (m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_group_6 T_2 T_0 T_1) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (v2_funct_1 T_2) ### Equiv 141 142 % 3.41/3.57 144. (((v1_funct_1 (k3_latsubgr T_0 T_1 T_2)) /\ ((v1_funct_2 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 (k3_latsubgr T_0 T_1 T_2) (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))))) => ((m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1)) <=> ((m4_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1)) /\ (m3_vectsp_8 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))))) (v2_funct_1 T_2) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (v1_group_6 T_2 T_0 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (-. (m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) ### DisjTree 65 82 101 143 % 3.41/3.57 145. (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 C (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))))) => ((m1_lattice4 C (k11_group_4 T_0) (k11_group_4 T_1)) <=> ((m4_vectsp_8 C (k11_group_4 T_0) (k11_group_4 T_1)) /\ (m3_vectsp_8 C (k11_group_4 T_0) (k11_group_4 T_1)))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (v1_group_6 T_2 T_0 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (v2_funct_1 T_2) ### All 144 % 3.41/3.57 146. (((-. (v3_struct_0 (k11_group_4 T_1))) /\ ((v10_lattices (k11_group_4 T_1)) /\ (l3_lattices (k11_group_4 T_1)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))) /\ (m2_relset_1 C (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 (k11_group_4 T_1))))) => ((m1_lattice4 C (k11_group_4 T_0) (k11_group_4 T_1)) <=> ((m4_vectsp_8 C (k11_group_4 T_0) (k11_group_4 T_1)) /\ (m3_vectsp_8 C (k11_group_4 T_0) (k11_group_4 T_1))))))) (v2_funct_1 T_2) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (v1_group_6 T_2 T_0 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (-. (m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) ### DisjTree 32 40 48 145 % 3.41/3.57 147. (All B, (((-. (v3_struct_0 B)) /\ ((v10_lattices B) /\ (l3_lattices B))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 B)) /\ (m2_relset_1 C (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 B)))) => ((m1_lattice4 C (k11_group_4 T_0) B) <=> ((m4_vectsp_8 C (k11_group_4 T_0) B) /\ (m3_vectsp_8 C (k11_group_4 T_0) B))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (v1_group_6 T_2 T_0 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (v2_funct_1 T_2) ### All 146 % 3.41/3.58 148. (((-. (v3_struct_0 (k11_group_4 T_0))) /\ ((v10_lattices (k11_group_4 T_0)) /\ (l3_lattices (k11_group_4 T_0)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v10_lattices B) /\ (l3_lattices B))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 B)) /\ (m2_relset_1 C (u1_struct_0 (k11_group_4 T_0)) (u1_struct_0 B)))) => ((m1_lattice4 C (k11_group_4 T_0) B) <=> ((m4_vectsp_8 C (k11_group_4 T_0) B) /\ (m3_vectsp_8 C (k11_group_4 T_0) B)))))))) (v2_funct_1 T_2) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (v1_group_6 T_2 T_0 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (-. (m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) ### DisjTree 8 16 24 147 % 3.41/3.58 149. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v10_lattices B) /\ (l3_lattices B))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))) => ((m1_lattice4 C A B) <=> ((m4_vectsp_8 C A B) /\ (m3_vectsp_8 C A B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (v1_funct_1 T_2) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (m1_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (-. (m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (v1_group_6 T_2 T_0 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (v2_funct_1 T_2) ### All 148 % 3.41/3.58 150. (m2_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v2_funct_1 T_2) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (v1_group_6 T_2 T_0 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (-. (m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))) (v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) (v1_funct_1 T_2) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v10_lattices B) /\ (l3_lattices B))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))) => ((m1_lattice4 C A B) <=> ((m4_vectsp_8 C A B) /\ (m3_vectsp_8 C A B))))))))) ### Definition-Pseudo(m2_relset_1) 149 % 3.41/3.58 151. (-. (((v1_funct_1 T_2) /\ ((v1_funct_2 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v1_group_6 T_2 T_0 T_1) /\ (m2_relset_1 T_2 (u1_struct_0 T_0) (u1_struct_0 T_1))))) => ((v2_funct_1 T_2) => (m1_lattice4 (k3_latsubgr T_0 T_1 T_2) (k11_group_4 T_0) (k11_group_4 T_1))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v10_lattices B) /\ (l3_lattices B))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))) => ((m1_lattice4 C A B) <=> ((m4_vectsp_8 C A B) /\ (m3_vectsp_8 C A B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (-. (v3_struct_0 T_1)) (v3_group_1 T_1) (v4_group_1 T_1) (l1_group_1 T_1) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) ### ConjTree 150 % 3.41/3.58 152. (-. (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v1_group_6 C T_0 T_1) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1))))) => ((v2_funct_1 C) => (m1_lattice4 (k3_latsubgr T_0 T_1 C) (k11_group_4 T_0) (k11_group_4 T_1)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (l1_group_1 T_1) (v4_group_1 T_1) (v3_group_1 T_1) (-. (v3_struct_0 T_1)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v10_lattices B) /\ (l3_lattices B))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))) => ((m1_lattice4 C A B) <=> ((m4_vectsp_8 C A B) /\ (m3_vectsp_8 C A B))))))))) ### NotAllEx 151 % 3.41/3.58 153. (-. (((-. (v3_struct_0 T_1)) /\ ((v3_group_1 T_1) /\ ((v4_group_1 T_1) /\ (l1_group_1 T_1)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v1_group_6 C T_0 T_1) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1))))) => ((v2_funct_1 C) => (m1_lattice4 (k3_latsubgr T_0 T_1 C) (k11_group_4 T_0) (k11_group_4 T_1))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v10_lattices B) /\ (l3_lattices B))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))) => ((m1_lattice4 C A B) <=> ((m4_vectsp_8 C A B) /\ (m3_vectsp_8 C A B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) ### ConjTree 152 % 3.41/3.58 154. (-. (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ ((v1_group_6 C T_0 B) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m1_lattice4 (k3_latsubgr T_0 B C) (k11_group_4 T_0) (k11_group_4 B)))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v10_lattices B) /\ (l3_lattices B))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))) => ((m1_lattice4 C A B) <=> ((m4_vectsp_8 C A B) /\ (m3_vectsp_8 C A B))))))))) ### NotAllEx 153 % 3.41/3.58 155. (-. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ (l1_group_1 T_0)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ ((v1_group_6 C T_0 B) /\ (m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m1_lattice4 (k3_latsubgr T_0 B C) (k11_group_4 T_0) (k11_group_4 B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v10_lattices B) /\ (l3_lattices B))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))) => ((m1_lattice4 C A B) <=> ((m4_vectsp_8 C A B) /\ (m3_vectsp_8 C A B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) ### ConjTree 154 % 3.41/3.59 156. (-. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m1_lattice4 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => ((v2_funct_1 C) => (m3_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ (l1_group_1 B)))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v1_group_6 C A B) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B))))) => (m4_vectsp_8 (k3_latsubgr A B C) (k11_group_4 A) (k11_group_4 B)))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ ((l1_group_1 A) /\ ((-. (v3_struct_0 B)) /\ ((v3_group_1 B) /\ ((v4_group_1 B) /\ ((l1_group_1 B) /\ ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m1_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))))))))))) => ((v1_funct_1 (k3_latsubgr A B C)) /\ ((v1_funct_2 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))) /\ (m2_relset_1 (k3_latsubgr A B C) (u1_struct_0 (k11_group_4 A)) (u1_struct_0 (k11_group_4 B))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ (l3_lattices (k11_group_4 A))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => ((-. (v3_struct_0 (k11_group_4 A))) /\ ((v3_lattices (k11_group_4 A)) /\ ((v4_lattices (k11_group_4 A)) /\ ((v5_lattices (k11_group_4 A)) /\ ((v6_lattices (k11_group_4 A)) /\ ((v7_lattices (k11_group_4 A)) /\ ((v8_lattices (k11_group_4 A)) /\ ((v9_lattices (k11_group_4 A)) /\ ((v10_lattices (k11_group_4 A)) /\ ((v13_lattices (k11_group_4 A)) /\ ((v14_lattices (k11_group_4 A)) /\ (v15_lattices (k11_group_4 A))))))))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v10_lattices B) /\ (l3_lattices B))) => (All C, (((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ (m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)))) => ((m1_lattice4 C A B) <=> ((m4_vectsp_8 C A B) /\ (m3_vectsp_8 C A B))))))))) ### NotAllEx 155 % 3.41/3.59 % SZS output end Proof % 3.41/3.59 (* END-PROOF *) %------------------------------------------------------------------------------