%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : GRP643+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 : n022.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:24 EDT 2022 % Result : Theorem 2.83s 3.07s % Output : Proof 2.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : GRP643+1 : TPTP v8.1.0. Released v3.4.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n022.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 : Mon Jun 13 17:41:33 EDT 2022 % 0.12/0.33 % CPUTime : % 2.83/3.07 % SZS status Theorem % 2.83/3.07 (* PROOF-FOUND *) % 2.83/3.07 (* BEGIN-PROOF *) % 2.83/3.07 % SZS output start Proof % 2.83/3.07 1. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.83/3.07 2. (v3_group_1 T_0) (-. (v3_group_1 T_0)) ### Axiom % 2.83/3.07 3. (v4_group_1 T_0) (-. (v4_group_1 T_0)) ### Axiom % 2.83/3.07 4. (l1_group_1 T_0) (-. (l1_group_1 T_0)) ### Axiom % 2.83/3.07 5. (v1_group_1 T_1) (-. (v1_group_1 T_1)) ### Axiom % 2.83/3.07 6. (m1_group_2 T_1 T_0) (-. (m1_group_2 T_1 T_0)) ### Axiom % 2.83/3.07 7. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.83/3.07 8. (l1_group_1 T_0) (-. (l1_group_1 T_0)) ### Axiom % 2.83/3.07 9. (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) ### Axiom % 2.83/3.07 10. (m1_subset_1 T_3 (u1_struct_0 T_0)) (-. (m1_subset_1 T_3 (u1_struct_0 T_0))) ### Axiom % 2.83/3.07 11. (-. (m1_subset_1 (k1_group_1 T_0 T_2 T_3) (u1_struct_0 T_0))) (m1_subset_1 (k1_group_1 T_0 T_2 T_3) (u1_struct_0 T_0)) ### Axiom % 2.83/3.07 12. (((-. (v3_struct_0 T_0)) /\ ((l1_group_1 T_0) /\ ((m1_subset_1 T_2 (u1_struct_0 T_0)) /\ (m1_subset_1 T_3 (u1_struct_0 T_0))))) => (m1_subset_1 (k1_group_1 T_0 T_2 T_3) (u1_struct_0 T_0))) (-. (m1_subset_1 (k1_group_1 T_0 T_2 T_3) (u1_struct_0 T_0))) (m1_subset_1 T_3 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (l1_group_1 T_0) (-. (v3_struct_0 T_0)) ### DisjTree 7 8 9 10 11 % 2.83/3.07 13. (All C, (((-. (v3_struct_0 T_0)) /\ ((l1_group_1 T_0) /\ ((m1_subset_1 T_2 (u1_struct_0 T_0)) /\ (m1_subset_1 C (u1_struct_0 T_0))))) => (m1_subset_1 (k1_group_1 T_0 T_2 C) (u1_struct_0 T_0)))) (-. (v3_struct_0 T_0)) (l1_group_1 T_0) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_3 (u1_struct_0 T_0)) (-. (m1_subset_1 (k1_group_1 T_0 T_2 T_3) (u1_struct_0 T_0))) ### All 12 % 2.83/3.07 14. (All B, (All C, (((-. (v3_struct_0 T_0)) /\ ((l1_group_1 T_0) /\ ((m1_subset_1 B (u1_struct_0 T_0)) /\ (m1_subset_1 C (u1_struct_0 T_0))))) => (m1_subset_1 (k1_group_1 T_0 B C) (u1_struct_0 T_0))))) (-. (m1_subset_1 (k1_group_1 T_0 T_2 T_3) (u1_struct_0 T_0))) (m1_subset_1 T_3 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (l1_group_1 T_0) (-. (v3_struct_0 T_0)) ### All 13 % 2.83/3.07 15. (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (-. (v3_struct_0 T_0)) (l1_group_1 T_0) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_3 (u1_struct_0 T_0)) (-. (m1_subset_1 (k1_group_1 T_0 T_2 T_3) (u1_struct_0 T_0))) ### All 14 % 2.83/3.07 16. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.83/3.07 17. (v3_group_1 T_0) (-. (v3_group_1 T_0)) ### Axiom % 2.83/3.07 18. (v4_group_1 T_0) (-. (v4_group_1 T_0)) ### Axiom % 2.83/3.07 19. (l1_group_1 T_0) (-. (l1_group_1 T_0)) ### Axiom % 2.83/3.07 20. (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) ### Axiom % 2.83/3.07 21. (m1_subset_1 T_3 (u1_struct_0 T_0)) (-. (m1_subset_1 T_3 (u1_struct_0 T_0))) ### Axiom % 2.83/3.07 22. (m1_group_2 T_1 T_0) (-. (m1_group_2 T_1 T_0)) ### Axiom % 2.83/3.07 23. (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) ### Axiom % 2.83/3.07 24. (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (-. (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1))) ### Axiom % 2.83/3.07 25. (-. (r1_rlvect_1 T_1 T_2)) (r1_rlvect_1 T_1 T_2) ### Axiom % 2.83/3.07 26. ((r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 T_2)) (-. (r1_rlvect_1 T_1 T_2)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) ### Equiv 24 25 % 2.83/3.07 27. ((m1_subset_1 T_2 (u1_struct_0 T_0)) => ((r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 T_2))) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (-. (r1_rlvect_1 T_1 T_2)) (m1_subset_1 T_2 (u1_struct_0 T_0)) ### Imply 23 26 % 2.83/3.07 28. (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (r1_rlvect_1 T_1 T_2)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) ### All 27 % 2.83/3.07 29. (m1_subset_1 T_3 (u1_struct_0 T_0)) (-. (m1_subset_1 T_3 (u1_struct_0 T_0))) ### Axiom % 2.83/3.07 30. (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (-. (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1))) ### Axiom % 2.83/3.07 31. (-. (r1_rlvect_1 T_1 T_3)) (r1_rlvect_1 T_1 T_3) ### Axiom % 2.83/3.07 32. ((r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 T_3)) (-. (r1_rlvect_1 T_1 T_3)) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) ### Equiv 30 31 % 2.83/3.07 33. ((m1_subset_1 T_3 (u1_struct_0 T_0)) => ((r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 T_3))) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (-. (r1_rlvect_1 T_1 T_3)) (m1_subset_1 T_3 (u1_struct_0 T_0)) ### Imply 29 32 % 2.83/3.07 34. (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (m1_subset_1 T_3 (u1_struct_0 T_0)) (-. (r1_rlvect_1 T_1 T_3)) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) ### All 33 % 2.83/3.07 35. (-. (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3))) (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3)) ### Axiom % 2.83/3.07 36. ((m1_group_2 T_1 T_0) => (((r1_rlvect_1 T_1 T_2) /\ (r1_rlvect_1 T_1 T_3)) => (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3)))) (-. (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3))) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (m1_subset_1 T_3 (u1_struct_0 T_0)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (m1_group_2 T_1 T_0) ### DisjTree 22 28 34 35 % 2.83/3.07 37. (All D, ((m1_group_2 D T_0) => (((r1_rlvect_1 D T_2) /\ (r1_rlvect_1 D T_3)) => (r1_rlvect_1 D (k1_group_1 T_0 T_2 T_3))))) (m1_group_2 T_1 T_0) (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (m1_subset_1 T_3 (u1_struct_0 T_0)) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (-. (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3))) ### All 36 % 2.83/3.07 38. ((m1_subset_1 T_3 (u1_struct_0 T_0)) => (All D, ((m1_group_2 D T_0) => (((r1_rlvect_1 D T_2) /\ (r1_rlvect_1 D T_3)) => (r1_rlvect_1 D (k1_group_1 T_0 T_2 T_3)))))) (-. (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3))) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (m1_group_2 T_1 T_0) (m1_subset_1 T_3 (u1_struct_0 T_0)) ### Imply 21 37 % 2.83/3.07 39. (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_group_2 D T_0) => (((r1_rlvect_1 D T_2) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 T_0 T_2 C))))))) (m1_subset_1 T_3 (u1_struct_0 T_0)) (m1_group_2 T_1 T_0) (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (-. (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3))) ### All 38 % 2.83/3.07 40. ((m1_subset_1 T_2 (u1_struct_0 T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_group_2 D T_0) => (((r1_rlvect_1 D T_2) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 T_0 T_2 C)))))))) (-. (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3))) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (m1_group_2 T_1 T_0) (m1_subset_1 T_3 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) ### Imply 20 39 % 2.83/3.07 41. (All B, ((m1_subset_1 B (u1_struct_0 T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_group_2 D T_0) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 T_0 B C))))))))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_3 (u1_struct_0 T_0)) (m1_group_2 T_1 T_0) (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (-. (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3))) ### All 40 % 2.93/3.17 42. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ (l1_group_1 T_0)))) => (All B, ((m1_subset_1 B (u1_struct_0 T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_group_2 D T_0) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 T_0 B C)))))))))) (-. (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3))) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (m1_group_2 T_1 T_0) (m1_subset_1 T_3 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (l1_group_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (-. (v3_struct_0 T_0)) ### DisjTree 16 17 18 19 41 % 2.93/3.17 43. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_3 (u1_struct_0 T_0)) (m1_group_2 T_1 T_0) (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (-. (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3))) ### All 42 % 2.93/3.17 44. (-. (r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1))) (r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1)) ### Axiom % 2.93/3.17 45. ((r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3))) (-. (r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1))) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (m1_group_2 T_1 T_0) (m1_subset_1 T_3 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (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, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) ### Equiv 43 44 % 2.93/3.17 46. ((m1_subset_1 (k1_group_1 T_0 T_2 T_3) (u1_struct_0 T_0)) => ((r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 (k1_group_1 T_0 T_2 T_3)))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) (v3_group_1 T_0) (v4_group_1 T_0) (m1_group_2 T_1 T_0) (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (-. (r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1))) (m1_subset_1 T_3 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (l1_group_1 T_0) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) ### Imply 15 45 % 2.93/3.17 47. (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (-. (v3_struct_0 T_0)) (l1_group_1 T_0) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_3 (u1_struct_0 T_0)) (-. (r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1))) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C)))) (m1_group_2 T_1 T_0) (v4_group_1 T_0) (v3_group_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) ### All 46 % 2.93/3.17 48. (((v1_group_1 T_1) /\ (m1_group_2 T_1 T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) <=> (r1_rlvect_1 T_1 C))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) (v3_group_1 T_0) (v4_group_1 T_0) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (-. (r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1))) (m1_subset_1 T_3 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (l1_group_1 T_0) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (m1_group_2 T_1 T_0) (v1_group_1 T_1) ### DisjTree 5 6 47 % 2.93/3.17 49. (All B, (((v1_group_1 B) /\ (m1_group_2 B T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) B)) <=> (r1_rlvect_1 B C)))))) (v1_group_1 T_1) (m1_group_2 T_1 T_0) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (-. (v3_struct_0 T_0)) (l1_group_1 T_0) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_3 (u1_struct_0 T_0)) (-. (r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1))) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (v4_group_1 T_0) (v3_group_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) ### All 48 % 2.93/3.17 50. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ (l1_group_1 T_0)))) => (All B, (((v1_group_1 B) /\ (m1_group_2 B T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) B)) <=> (r1_rlvect_1 B C))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (-. (r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1))) (m1_subset_1 T_3 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (m1_group_2 T_1 T_0) (v1_group_1 T_1) (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 49 % 2.93/3.17 51. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((v1_group_1 B) /\ (m1_group_2 B A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr A) B)) <=> (r1_rlvect_1 B C)))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (v1_group_1 T_1) (m1_group_2 T_1 T_0) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_3 (u1_struct_0 T_0)) (-. (r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1))) (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1)) (r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) ### All 50 % 2.93/3.19 52. (-. ((m1_subset_1 T_3 (u1_struct_0 T_0)) => (((r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) /\ (r2_hidden T_3 (k1_funct_1 (k1_latsubgr T_0) T_1))) => (r2_hidden (k1_group_1 T_0 T_2 T_3) (k1_funct_1 (k1_latsubgr T_0) T_1))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (m1_group_2 T_1 T_0) (v1_group_1 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, (((v1_group_1 B) /\ (m1_group_2 B A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr A) B)) <=> (r1_rlvect_1 B C)))))))) ### ConjTree 51 % 2.93/3.19 53. (-. (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => (((r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) /\ (r2_hidden D (k1_funct_1 (k1_latsubgr T_0) T_1))) => (r2_hidden (k1_group_1 T_0 T_2 D) (k1_funct_1 (k1_latsubgr T_0) T_1)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((v1_group_1 B) /\ (m1_group_2 B A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr A) B)) <=> (r1_rlvect_1 B C)))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (v1_group_1 T_1) (m1_group_2 T_1 T_0) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) ### NotAllEx 52 % 2.93/3.19 54. (-. ((m1_subset_1 T_2 (u1_struct_0 T_0)) => (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => (((r2_hidden T_2 (k1_funct_1 (k1_latsubgr T_0) T_1)) /\ (r2_hidden D (k1_funct_1 (k1_latsubgr T_0) T_1))) => (r2_hidden (k1_group_1 T_0 T_2 D) (k1_funct_1 (k1_latsubgr T_0) T_1))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (m1_group_2 T_1 T_0) (v1_group_1 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, (((v1_group_1 B) /\ (m1_group_2 B A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr A) B)) <=> (r1_rlvect_1 B C)))))))) ### NotImply 53 % 2.93/3.19 55. (-. (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => (((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) /\ (r2_hidden D (k1_funct_1 (k1_latsubgr T_0) T_1))) => (r2_hidden (k1_group_1 T_0 C D) (k1_funct_1 (k1_latsubgr T_0) T_1)))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((v1_group_1 B) /\ (m1_group_2 B A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr A) B)) <=> (r1_rlvect_1 B C)))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (v1_group_1 T_1) (m1_group_2 T_1 T_0) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) ### NotAllEx 54 % 2.93/3.19 56. (-. (((v1_group_1 T_1) /\ (m1_group_2 T_1 T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => (((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) T_1)) /\ (r2_hidden D (k1_funct_1 (k1_latsubgr T_0) T_1))) => (r2_hidden (k1_group_1 T_0 C D) (k1_funct_1 (k1_latsubgr T_0) T_1))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 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)))) => (All B, (((v1_group_1 B) /\ (m1_group_2 B A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr A) B)) <=> (r1_rlvect_1 B C)))))))) ### ConjTree 55 % 2.93/3.19 57. (-. (All B, (((v1_group_1 B) /\ (m1_group_2 B T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => (((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) B)) /\ (r2_hidden D (k1_funct_1 (k1_latsubgr T_0) B))) => (r2_hidden (k1_group_1 T_0 C D) (k1_funct_1 (k1_latsubgr T_0) B)))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((v1_group_1 B) /\ (m1_group_2 B A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr A) B)) <=> (r1_rlvect_1 B C)))))))) (-. (v3_struct_0 T_0)) (v3_group_1 T_0) (v4_group_1 T_0) (l1_group_1 T_0) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) ### NotAllEx 56 % 2.93/3.19 58. (-. (((-. (v3_struct_0 T_0)) /\ ((v3_group_1 T_0) /\ ((v4_group_1 T_0) /\ (l1_group_1 T_0)))) => (All B, (((v1_group_1 B) /\ (m1_group_2 B T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => (((r2_hidden C (k1_funct_1 (k1_latsubgr T_0) B)) /\ (r2_hidden D (k1_funct_1 (k1_latsubgr T_0) B))) => (r2_hidden (k1_group_1 T_0 C D) (k1_funct_1 (k1_latsubgr T_0) B))))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((v1_group_1 B) /\ (m1_group_2 B A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr A) B)) <=> (r1_rlvect_1 B C)))))))) ### ConjTree 57 % 2.93/3.19 59. (-. (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((v1_group_1 B) /\ (m1_group_2 B A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_subset_1 D (u1_struct_0 A)) => (((r2_hidden C (k1_funct_1 (k1_latsubgr A) B)) /\ (r2_hidden D (k1_funct_1 (k1_latsubgr A) B))) => (r2_hidden (k1_group_1 A C D) (k1_funct_1 (k1_latsubgr A) B)))))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, (((v1_group_1 B) /\ (m1_group_2 B A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => ((r2_hidden C (k1_funct_1 (k1_latsubgr A) B)) <=> (r1_rlvect_1 B C)))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((l1_group_1 A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A))))) => (m1_subset_1 (k1_group_1 A B C) (u1_struct_0 A)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v3_group_1 A) /\ ((v4_group_1 A) /\ (l1_group_1 A)))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_group_2 D A) => (((r1_rlvect_1 D B) /\ (r1_rlvect_1 D C)) => (r1_rlvect_1 D (k1_group_1 A B C))))))))))) ### NotAllEx 58 % 2.93/3.19 % SZS output end Proof % 2.93/3.19 (* END-PROOF *) %------------------------------------------------------------------------------