%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : LAT327+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 : n012.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sun Jul 17 06:57:20 EDT 2022 % Result : Theorem 2.93s 3.16s % Output : Proof 3.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : LAT327+1 : TPTP v8.1.0. Released v3.4.0. % 0.06/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n012.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 : Wed Jun 29 09:16:33 EDT 2022 % 0.12/0.33 % CPUTime : % 2.93/3.16 % SZS status Theorem % 2.93/3.16 (* PROOF-FOUND *) % 2.93/3.16 (* BEGIN-PROOF *) % 2.93/3.16 % SZS output start Proof % 2.93/3.16 1. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.93/3.16 2. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.93/3.16 3. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.93/3.16 4. (m1_subset_1 T_1 (u1_struct_0 T_0)) (-. (m1_subset_1 T_1 (u1_struct_0 T_0))) ### Axiom % 2.93/3.16 5. (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) ### Axiom % 2.93/3.16 6. (m1_subset_1 T_1 (u1_struct_0 T_0)) (-. (m1_subset_1 T_1 (u1_struct_0 T_0))) ### Axiom % 2.93/3.16 7. (r3_lattices T_0 T_1 T_2) (-. (r3_lattices T_0 T_1 T_2)) ### Axiom % 2.93/3.16 8. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.93/3.16 9. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.93/3.16 10. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.93/3.16 11. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.93/3.16 12. (-. (v6_lattices T_0)) (v6_lattices T_0) ### Axiom % 2.93/3.16 13. ((-. (v3_struct_0 T_0)) /\ ((v4_lattices T_0) /\ ((v5_lattices T_0) /\ ((v6_lattices T_0) /\ ((v7_lattices T_0) /\ ((v8_lattices T_0) /\ (v9_lattices T_0))))))) (-. (v6_lattices T_0)) ### ConjTree 12 % 2.93/3.16 14. ((l3_lattices T_0) => (((-. (v3_struct_0 T_0)) /\ (v10_lattices T_0)) => ((-. (v3_struct_0 T_0)) /\ ((v4_lattices T_0) /\ ((v5_lattices T_0) /\ ((v6_lattices T_0) /\ ((v7_lattices T_0) /\ ((v8_lattices T_0) /\ (v9_lattices T_0))))))))) (-. (v6_lattices T_0)) (v10_lattices T_0) (-. (v3_struct_0 T_0)) (l3_lattices T_0) ### DisjTree 9 10 11 13 % 2.93/3.16 15. (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (-. (v6_lattices T_0)) ### All 14 % 2.93/3.16 16. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.93/3.16 17. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.93/3.16 18. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.93/3.16 19. (-. (v8_lattices T_0)) (v8_lattices T_0) ### Axiom % 2.93/3.16 20. ((-. (v3_struct_0 T_0)) /\ ((v4_lattices T_0) /\ ((v5_lattices T_0) /\ ((v6_lattices T_0) /\ ((v7_lattices T_0) /\ ((v8_lattices T_0) /\ (v9_lattices T_0))))))) (-. (v8_lattices T_0)) ### ConjTree 19 % 2.93/3.16 21. ((l3_lattices T_0) => (((-. (v3_struct_0 T_0)) /\ (v10_lattices T_0)) => ((-. (v3_struct_0 T_0)) /\ ((v4_lattices T_0) /\ ((v5_lattices T_0) /\ ((v6_lattices T_0) /\ ((v7_lattices T_0) /\ ((v8_lattices T_0) /\ (v9_lattices T_0))))))))) (-. (v8_lattices T_0)) (v10_lattices T_0) (-. (v3_struct_0 T_0)) (l3_lattices T_0) ### DisjTree 16 17 18 20 % 2.93/3.16 22. (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (-. (v8_lattices T_0)) ### All 21 % 2.93/3.16 23. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.93/3.16 24. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.93/3.16 25. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.93/3.16 26. (-. (v9_lattices T_0)) (v9_lattices T_0) ### Axiom % 2.93/3.16 27. ((-. (v3_struct_0 T_0)) /\ ((v4_lattices T_0) /\ ((v5_lattices T_0) /\ ((v6_lattices T_0) /\ ((v7_lattices T_0) /\ ((v8_lattices T_0) /\ (v9_lattices T_0))))))) (-. (v9_lattices T_0)) ### ConjTree 26 % 2.93/3.16 28. ((l3_lattices T_0) => (((-. (v3_struct_0 T_0)) /\ (v10_lattices T_0)) => ((-. (v3_struct_0 T_0)) /\ ((v4_lattices T_0) /\ ((v5_lattices T_0) /\ ((v6_lattices T_0) /\ ((v7_lattices T_0) /\ ((v8_lattices T_0) /\ (v9_lattices T_0))))))))) (-. (v9_lattices T_0)) (v10_lattices T_0) (-. (v3_struct_0 T_0)) (l3_lattices T_0) ### DisjTree 23 24 25 27 % 2.93/3.16 29. (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (-. (v9_lattices T_0)) ### All 28 % 2.93/3.16 30. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.93/3.16 31. (m1_subset_1 T_1 (u1_struct_0 T_0)) (-. (m1_subset_1 T_1 (u1_struct_0 T_0))) ### Axiom % 2.93/3.16 32. (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) ### Axiom % 2.93/3.16 33. (-. (r3_lattices T_0 T_1 T_1)) (r3_lattices T_0 T_1 T_1) ### Axiom % 2.93/3.16 34. (((-. (v3_struct_0 T_0)) /\ ((v6_lattices T_0) /\ ((v8_lattices T_0) /\ ((v9_lattices T_0) /\ ((l3_lattices T_0) /\ ((m1_subset_1 T_1 (u1_struct_0 T_0)) /\ (m1_subset_1 T_2 (u1_struct_0 T_0)))))))) => (r3_lattices T_0 T_1 T_1)) (-. (r3_lattices T_0 T_1 T_1)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_1 (u1_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) ### DisjTree 8 15 22 29 30 31 32 33 % 2.93/3.16 35. (All C, (((-. (v3_struct_0 T_0)) /\ ((v6_lattices T_0) /\ ((v8_lattices T_0) /\ ((v9_lattices T_0) /\ ((l3_lattices T_0) /\ ((m1_subset_1 T_1 (u1_struct_0 T_0)) /\ (m1_subset_1 C (u1_struct_0 T_0)))))))) => (r3_lattices T_0 T_1 T_1))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) (m1_subset_1 T_1 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (r3_lattices T_0 T_1 T_1)) ### All 34 % 2.93/3.16 36. (All B, (All C, (((-. (v3_struct_0 T_0)) /\ ((v6_lattices T_0) /\ ((v8_lattices T_0) /\ ((v9_lattices T_0) /\ ((l3_lattices T_0) /\ ((m1_subset_1 B (u1_struct_0 T_0)) /\ (m1_subset_1 C (u1_struct_0 T_0)))))))) => (r3_lattices T_0 B B)))) (-. (r3_lattices T_0 T_1 T_1)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_1 (u1_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) ### All 35 % 2.93/3.16 37. (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) (m1_subset_1 T_1 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (r3_lattices T_0 T_1 T_1)) ### All 36 % 2.93/3.16 38. (r3_lattices T_0 T_1 T_2) (-. (r3_lattices T_0 T_1 T_2)) ### Axiom % 2.93/3.16 39. (-. ((r3_lattices T_0 T_1 T_1) /\ (r3_lattices T_0 T_1 T_2))) (r3_lattices T_0 T_1 T_2) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_1 (u1_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) ### NotAnd 37 38 % 2.93/3.16 40. (-. (r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2))) (r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2)) ### Axiom % 2.93/3.16 41. ((r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2)) <=> ((r3_lattices T_0 T_1 T_1) /\ (r3_lattices T_0 T_1 T_2))) (-. (r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) (m1_subset_1 T_1 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (r3_lattices T_0 T_1 T_2) ### Equiv 39 40 % 2.93/3.19 42. ((m1_subset_1 T_1 (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 T_2) => ((r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2)) <=> ((r3_lattices T_0 T_1 T_1) /\ (r3_lattices T_0 T_1 T_2))))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2))) (r3_lattices T_0 T_1 T_2) (m1_subset_1 T_1 (u1_struct_0 T_0)) ### DisjTree 6 7 41 % 2.93/3.19 43. (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 T_2) => ((r2_hidden D (k22_filter_2 T_0 T_1 T_2)) <=> ((r3_lattices T_0 T_1 D) /\ (r3_lattices T_0 D T_2)))))) (m1_subset_1 T_1 (u1_struct_0 T_0)) (r3_lattices T_0 T_1 T_2) (-. (r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) (m1_subset_1 T_2 (u1_struct_0 T_0)) ### All 42 % 2.93/3.19 44. ((m1_subset_1 T_2 (u1_struct_0 T_0)) => (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 T_2) => ((r2_hidden D (k22_filter_2 T_0 T_1 T_2)) <=> ((r3_lattices T_0 T_1 D) /\ (r3_lattices T_0 D T_2))))))) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2))) (r3_lattices T_0 T_1 T_2) (m1_subset_1 T_1 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) ### Imply 5 43 % 2.93/3.19 45. (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 C) => ((r2_hidden D (k22_filter_2 T_0 T_1 C)) <=> ((r3_lattices T_0 T_1 D) /\ (r3_lattices T_0 D C)))))))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_1 (u1_struct_0 T_0)) (r3_lattices T_0 T_1 T_2) (-. (r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) ### All 44 % 2.93/3.19 46. ((m1_subset_1 T_1 (u1_struct_0 T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 C) => ((r2_hidden D (k22_filter_2 T_0 T_1 C)) <=> ((r3_lattices T_0 T_1 D) /\ (r3_lattices T_0 D C))))))))) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2))) (r3_lattices T_0 T_1 T_2) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_1 (u1_struct_0 T_0)) ### Imply 4 45 % 2.93/3.19 47. (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_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 B C) => ((r2_hidden D (k22_filter_2 T_0 B C)) <=> ((r3_lattices T_0 B D) /\ (r3_lattices T_0 D C)))))))))) (m1_subset_1 T_1 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (r3_lattices T_0 T_1 T_2) (-. (r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) ### All 46 % 2.93/3.19 48. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices 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_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 B C) => ((r2_hidden D (k22_filter_2 T_0 B C)) <=> ((r3_lattices T_0 B D) /\ (r3_lattices T_0 D C))))))))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2))) (r3_lattices T_0 T_1 T_2) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_1 (u1_struct_0 T_0)) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 1 2 3 47 % 2.93/3.19 49. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_subset_1 D (u1_struct_0 A)) => ((r3_lattices A B C) => ((r2_hidden D (k22_filter_2 A B C)) <=> ((r3_lattices A B D) /\ (r3_lattices A D C)))))))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (m1_subset_1 T_1 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (r3_lattices T_0 T_1 T_2) (-. (r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) ### All 48 % 2.93/3.19 50. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 2.93/3.19 51. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 2.93/3.19 52. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 2.93/3.19 53. (m1_subset_1 T_1 (u1_struct_0 T_0)) (-. (m1_subset_1 T_1 (u1_struct_0 T_0))) ### Axiom % 2.93/3.19 54. (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) ### Axiom % 2.93/3.19 55. (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) ### Axiom % 3.03/3.27 56. (r3_lattices T_0 T_1 T_2) (-. (r3_lattices T_0 T_1 T_2)) ### Axiom % 3.03/3.27 57. (r3_lattices T_0 T_1 T_2) (-. (r3_lattices T_0 T_1 T_2)) ### Axiom % 3.03/3.27 58. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 3.03/3.27 59. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 3.03/3.27 60. (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) ### Axiom % 3.03/3.27 61. (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) ### Axiom % 3.03/3.27 62. (-. (r3_lattices T_0 T_2 T_2)) (r3_lattices T_0 T_2 T_2) ### Axiom % 3.03/3.27 63. (((-. (v3_struct_0 T_0)) /\ ((v6_lattices T_0) /\ ((v8_lattices T_0) /\ ((v9_lattices T_0) /\ ((l3_lattices T_0) /\ ((m1_subset_1 T_2 (u1_struct_0 T_0)) /\ (m1_subset_1 T_2 (u1_struct_0 T_0)))))))) => (r3_lattices T_0 T_2 T_2)) (-. (r3_lattices T_0 T_2 T_2)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) ### DisjTree 58 15 22 29 59 60 61 62 % 3.03/3.27 64. (All C, (((-. (v3_struct_0 T_0)) /\ ((v6_lattices T_0) /\ ((v8_lattices T_0) /\ ((v9_lattices T_0) /\ ((l3_lattices T_0) /\ ((m1_subset_1 T_2 (u1_struct_0 T_0)) /\ (m1_subset_1 C (u1_struct_0 T_0)))))))) => (r3_lattices T_0 T_2 T_2))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (r3_lattices T_0 T_2 T_2)) ### All 63 % 3.03/3.27 65. (All B, (All C, (((-. (v3_struct_0 T_0)) /\ ((v6_lattices T_0) /\ ((v8_lattices T_0) /\ ((v9_lattices T_0) /\ ((l3_lattices T_0) /\ ((m1_subset_1 B (u1_struct_0 T_0)) /\ (m1_subset_1 C (u1_struct_0 T_0)))))))) => (r3_lattices T_0 B B)))) (-. (r3_lattices T_0 T_2 T_2)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) ### All 64 % 3.03/3.27 66. (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) (m1_subset_1 T_2 (u1_struct_0 T_0)) (-. (r3_lattices T_0 T_2 T_2)) ### All 65 % 3.03/3.27 67. (-. ((r3_lattices T_0 T_1 T_2) /\ (r3_lattices T_0 T_2 T_2))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (r3_lattices T_0 T_1 T_2) ### NotAnd 57 66 % 3.03/3.27 68. (-. (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2))) (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2)) ### Axiom % 3.03/3.27 69. ((r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2)) <=> ((r3_lattices T_0 T_1 T_2) /\ (r3_lattices T_0 T_2 T_2))) (-. (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2))) (r3_lattices T_0 T_1 T_2) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) (m1_subset_1 T_2 (u1_struct_0 T_0)) ### Equiv 67 68 % 3.03/3.27 70. ((m1_subset_1 T_2 (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 T_2) => ((r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2)) <=> ((r3_lattices T_0 T_1 T_2) /\ (r3_lattices T_0 T_2 T_2))))) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2))) (r3_lattices T_0 T_1 T_2) (m1_subset_1 T_2 (u1_struct_0 T_0)) ### DisjTree 55 56 69 % 3.03/3.27 71. (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 T_2) => ((r2_hidden D (k22_filter_2 T_0 T_1 T_2)) <=> ((r3_lattices T_0 T_1 D) /\ (r3_lattices T_0 D T_2)))))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (r3_lattices T_0 T_1 T_2) (-. (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) ### All 70 % 3.03/3.27 72. ((m1_subset_1 T_2 (u1_struct_0 T_0)) => (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 T_2) => ((r2_hidden D (k22_filter_2 T_0 T_1 T_2)) <=> ((r3_lattices T_0 T_1 D) /\ (r3_lattices T_0 D T_2))))))) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2))) (r3_lattices T_0 T_1 T_2) (m1_subset_1 T_2 (u1_struct_0 T_0)) ### Imply 54 71 % 3.03/3.27 73. (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 C) => ((r2_hidden D (k22_filter_2 T_0 T_1 C)) <=> ((r3_lattices T_0 T_1 D) /\ (r3_lattices T_0 D C)))))))) (m1_subset_1 T_2 (u1_struct_0 T_0)) (r3_lattices T_0 T_1 T_2) (-. (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) ### All 72 % 3.03/3.27 74. ((m1_subset_1 T_1 (u1_struct_0 T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => (All D, ((m1_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 C) => ((r2_hidden D (k22_filter_2 T_0 T_1 C)) <=> ((r3_lattices T_0 T_1 D) /\ (r3_lattices T_0 D C))))))))) (v10_lattices T_0) (l3_lattices T_0) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (-. (v3_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2))) (r3_lattices T_0 T_1 T_2) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_1 (u1_struct_0 T_0)) ### Imply 53 73 % 3.13/3.29 75. (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_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 B C) => ((r2_hidden D (k22_filter_2 T_0 B C)) <=> ((r3_lattices T_0 B D) /\ (r3_lattices T_0 D C)))))))))) (m1_subset_1 T_1 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (r3_lattices T_0 T_1 T_2) (-. (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (v3_struct_0 T_0)) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (l3_lattices T_0) (v10_lattices T_0) ### All 74 % 3.13/3.29 76. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices 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_subset_1 D (u1_struct_0 T_0)) => ((r3_lattices T_0 B C) => ((r2_hidden D (k22_filter_2 T_0 B C)) <=> ((r3_lattices T_0 B D) /\ (r3_lattices T_0 D C))))))))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (-. (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2))) (r3_lattices T_0 T_1 T_2) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_1 (u1_struct_0 T_0)) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 50 51 52 75 % 3.13/3.29 77. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_subset_1 D (u1_struct_0 A)) => ((r3_lattices A B C) => ((r2_hidden D (k22_filter_2 A B C)) <=> ((r3_lattices A B D) /\ (r3_lattices A D C)))))))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (m1_subset_1 T_1 (u1_struct_0 T_0)) (m1_subset_1 T_2 (u1_struct_0 T_0)) (r3_lattices T_0 T_1 T_2) (-. (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) ### All 76 % 3.13/3.29 78. (-. ((r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2)) /\ (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2)))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (r3_lattices T_0 T_1 T_2) (m1_subset_1 T_2 (u1_struct_0 T_0)) (m1_subset_1 T_1 (u1_struct_0 T_0)) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_subset_1 D (u1_struct_0 A)) => ((r3_lattices A B C) => ((r2_hidden D (k22_filter_2 A B C)) <=> ((r3_lattices A B D) /\ (r3_lattices A D C)))))))))))) ### NotAnd 49 77 % 3.13/3.29 79. (-. ((m1_subset_1 T_2 (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 T_2) => ((r2_hidden T_1 (k22_filter_2 T_0 T_1 T_2)) /\ (r2_hidden T_2 (k22_filter_2 T_0 T_1 T_2)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_subset_1 D (u1_struct_0 A)) => ((r3_lattices A B C) => ((r2_hidden D (k22_filter_2 A B C)) <=> ((r3_lattices A B D) /\ (r3_lattices A D C)))))))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (m1_subset_1 T_1 (u1_struct_0 T_0)) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) ### ConjTree 78 % 3.13/3.29 80. (-. (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 C) => ((r2_hidden T_1 (k22_filter_2 T_0 T_1 C)) /\ (r2_hidden C (k22_filter_2 T_0 T_1 C))))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (m1_subset_1 T_1 (u1_struct_0 T_0)) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_subset_1 D (u1_struct_0 A)) => ((r3_lattices A B C) => ((r2_hidden D (k22_filter_2 A B C)) <=> ((r3_lattices A B D) /\ (r3_lattices A D C)))))))))))) ### NotAllEx 79 % 3.13/3.29 81. (-. ((m1_subset_1 T_1 (u1_struct_0 T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r3_lattices T_0 T_1 C) => ((r2_hidden T_1 (k22_filter_2 T_0 T_1 C)) /\ (r2_hidden C (k22_filter_2 T_0 T_1 C)))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_subset_1 D (u1_struct_0 A)) => ((r3_lattices A B C) => ((r2_hidden D (k22_filter_2 A B C)) <=> ((r3_lattices A B D) /\ (r3_lattices A D C)))))))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) ### NotImply 80 % 3.13/3.29 82. (-. (All B, ((m1_subset_1 B (u1_struct_0 T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r3_lattices T_0 B C) => ((r2_hidden B (k22_filter_2 T_0 B C)) /\ (r2_hidden C (k22_filter_2 T_0 B C))))))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_subset_1 D (u1_struct_0 A)) => ((r3_lattices A B C) => ((r2_hidden D (k22_filter_2 A B C)) <=> ((r3_lattices A B D) /\ (r3_lattices A D C)))))))))))) ### NotAllEx 81 % 3.13/3.30 83. (-. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (All B, ((m1_subset_1 B (u1_struct_0 T_0)) => (All C, ((m1_subset_1 C (u1_struct_0 T_0)) => ((r3_lattices T_0 B C) => ((r2_hidden B (k22_filter_2 T_0 B C)) /\ (r2_hidden C (k22_filter_2 T_0 B C)))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_subset_1 D (u1_struct_0 A)) => ((r3_lattices A B C) => ((r2_hidden D (k22_filter_2 A B C)) <=> ((r3_lattices A B D) /\ (r3_lattices A D C)))))))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) ### ConjTree 82 % 3.13/3.30 84. (-. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => ((r3_lattices A B C) => ((r2_hidden B (k22_filter_2 A B C)) /\ (r2_hidden C (k22_filter_2 A B C))))))))))) (All A, ((l3_lattices A) => (((-. (v3_struct_0 A)) /\ (v10_lattices A)) => ((-. (v3_struct_0 A)) /\ ((v4_lattices A) /\ ((v5_lattices A) /\ ((v6_lattices A) /\ ((v7_lattices A) /\ ((v8_lattices A) /\ (v9_lattices A)))))))))) (All A, (All B, (All C, (((-. (v3_struct_0 A)) /\ ((v6_lattices A) /\ ((v8_lattices A) /\ ((v9_lattices A) /\ ((l3_lattices A) /\ ((m1_subset_1 B (u1_struct_0 A)) /\ (m1_subset_1 C (u1_struct_0 A)))))))) => (r3_lattices A B B))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m1_subset_1 B (u1_struct_0 A)) => (All C, ((m1_subset_1 C (u1_struct_0 A)) => (All D, ((m1_subset_1 D (u1_struct_0 A)) => ((r3_lattices A B C) => ((r2_hidden D (k22_filter_2 A B C)) <=> ((r3_lattices A B D) /\ (r3_lattices A D C)))))))))))) ### NotAllEx 83 % 3.13/3.30 % SZS output end Proof % 3.13/3.30 (* END-PROOF *) %------------------------------------------------------------------------------