%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : LAT300+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 : n011.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:56:53 EDT 2022 % Result : Theorem 52.04s 52.27s % Output : Proof 52.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : LAT300+1 : TPTP v8.1.0. Released v3.4.0. % 0.10/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n011.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 14:21:02 EDT 2022 % 0.12/0.33 % CPUTime : % 52.04/52.27 % SZS status Theorem % 52.04/52.27 (* PROOF-FOUND *) % 52.04/52.27 (* BEGIN-PROOF *) % 52.04/52.27 % SZS output start Proof % 52.04/52.27 1. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 52.04/52.27 2. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 52.04/52.27 3. (-. (l1_lattices T_0)) (l1_lattices T_0) ### Axiom % 52.04/52.27 4. ((l1_lattices T_0) /\ (l2_lattices T_0)) (-. (l1_lattices T_0)) ### And 3 % 52.04/52.27 5. ((l3_lattices T_0) => ((l1_lattices T_0) /\ (l2_lattices T_0))) (-. (l1_lattices T_0)) (l3_lattices T_0) ### Imply 2 4 % 52.04/52.27 6. (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (l3_lattices T_0) (-. (l1_lattices T_0)) ### All 5 % 52.04/52.27 7. (-. (l1_struct_0 T_0)) (l1_struct_0 T_0) ### Axiom % 52.04/52.27 8. ((l1_lattices T_0) => (l1_struct_0 T_0)) (-. (l1_struct_0 T_0)) (l3_lattices T_0) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) ### Imply 6 7 % 52.04/52.27 9. (All A, ((l1_lattices A) => (l1_struct_0 A))) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (l3_lattices T_0) (-. (l1_struct_0 T_0)) ### All 8 % 52.04/52.27 10. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 52.04/52.27 11. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 52.04/52.27 12. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 52.04/52.27 13. (m2_filter_2 T_1 T_0) (-. (m2_filter_2 T_1 T_0)) ### Axiom % 52.04/52.27 14. (v1_xboole_0 T_1) (-. (v1_xboole_0 T_1)) ### Axiom % 52.04/52.27 15. ((-. (v1_xboole_0 T_1)) /\ (m2_lattice4 T_1 T_0)) (v1_xboole_0 T_1) ### And 14 % 52.04/52.27 16. ((m2_filter_2 T_1 T_0) => ((-. (v1_xboole_0 T_1)) /\ (m2_lattice4 T_1 T_0))) (v1_xboole_0 T_1) (m2_filter_2 T_1 T_0) ### Imply 13 15 % 52.04/52.27 17. (All B, ((m2_filter_2 B T_0) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B T_0)))) (m2_filter_2 T_1 T_0) (v1_xboole_0 T_1) ### All 16 % 52.04/52.27 18. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (All B, ((m2_filter_2 B T_0) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B T_0))))) (v1_xboole_0 T_1) (m2_filter_2 T_1 T_0) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 10 11 12 17 % 52.04/52.27 19. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (m2_filter_2 T_1 T_0) (v1_xboole_0 T_1) ### All 18 % 52.04/52.27 20. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 52.04/52.27 21. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 52.04/52.27 22. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 52.04/52.27 23. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 52.04/52.27 24. (v10_lattices T_0) (-. (v10_lattices T_0)) ### Axiom % 52.04/52.27 25. (l3_lattices T_0) (-. (l3_lattices T_0)) ### Axiom % 52.04/52.27 26. (m2_filter_2 T_1 T_0) (-. (m2_filter_2 T_1 T_0)) ### Axiom % 52.04/52.27 27. (-. (m2_lattice4 T_1 T_0)) (m2_lattice4 T_1 T_0) ### Axiom % 52.04/52.27 28. ((-. (v1_xboole_0 T_1)) /\ (m2_lattice4 T_1 T_0)) (-. (m2_lattice4 T_1 T_0)) ### And 27 % 52.04/52.27 29. ((m2_filter_2 T_1 T_0) => ((-. (v1_xboole_0 T_1)) /\ (m2_lattice4 T_1 T_0))) (-. (m2_lattice4 T_1 T_0)) (m2_filter_2 T_1 T_0) ### Imply 26 28 % 52.04/52.27 30. (All B, ((m2_filter_2 B T_0) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B T_0)))) (m2_filter_2 T_1 T_0) (-. (m2_lattice4 T_1 T_0)) ### All 29 % 52.04/52.27 31. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (All B, ((m2_filter_2 B T_0) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B T_0))))) (-. (m2_lattice4 T_1 T_0)) (m2_filter_2 T_1 T_0) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 23 24 25 30 % 52.04/52.27 32. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (m2_filter_2 T_1 T_0) (-. (m2_lattice4 T_1 T_0)) ### All 31 % 52.04/52.27 33. (-. (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0)))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ### Axiom % 52.04/52.27 34. ((m2_lattice4 T_1 T_0) => (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0)))) (-. (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0)))) (m2_filter_2 T_1 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, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) ### Imply 32 33 % 52.04/52.27 35. (All B, ((m2_lattice4 B T_0) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (m2_filter_2 T_1 T_0) (-. (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0)))) ### All 34 % 52.04/52.27 36. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (All B, ((m2_lattice4 B T_0) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0)))))) (-. (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0)))) (m2_filter_2 T_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (l3_lattices T_0) (v10_lattices T_0) (-. (v3_struct_0 T_0)) ### DisjTree 20 21 22 35 % 52.04/52.27 37. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (m2_filter_2 T_1 T_0) (-. (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0)))) ### All 36 % 52.04/52.27 38. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 52.04/52.27 39. (m1_subset_1 T_2 T_1) (-. (m1_subset_1 T_2 T_1)) ### Axiom % 52.04/52.27 40. (-. (m1_struct_0 T_2 T_0 T_1)) (m1_struct_0 T_2 T_0 T_1) ### Axiom % 52.04/52.27 41. ((m1_struct_0 T_2 T_0 T_1) <=> (m1_subset_1 T_2 T_1)) (-. (m1_struct_0 T_2 T_0 T_1)) (m1_subset_1 T_2 T_1) ### Equiv 39 40 % 52.04/52.27 42. (All C, ((m1_struct_0 C T_0 T_1) <=> (m1_subset_1 C T_1))) (m1_subset_1 T_2 T_1) (-. (m1_struct_0 T_2 T_0 T_1)) ### All 41 % 52.04/52.27 43. (((-. (v3_struct_0 T_0)) /\ ((l1_struct_0 T_0) /\ ((-. (v1_xboole_0 T_1)) /\ (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0)))))) => (All C, ((m1_struct_0 C T_0 T_1) <=> (m1_subset_1 C T_1)))) (-. (m1_struct_0 T_2 T_0 T_1)) (m1_subset_1 T_2 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (m2_filter_2 T_1 T_0) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (l3_lattices T_0) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (All A, ((l1_lattices A) => (l1_struct_0 A))) (-. (v3_struct_0 T_0)) ### DisjTree 38 9 19 37 42 % 52.04/52.27 44. (All B, (((-. (v3_struct_0 T_0)) /\ ((l1_struct_0 T_0) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0)))))) => (All C, ((m1_struct_0 C T_0 B) <=> (m1_subset_1 C B))))) (-. (v3_struct_0 T_0)) (All A, ((l1_lattices A) => (l1_struct_0 A))) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (v10_lattices T_0) (m2_filter_2 T_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (m1_subset_1 T_2 T_1) (-. (m1_struct_0 T_2 T_0 T_1)) ### All 43 % 52.04/52.27 45. (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (-. (m1_struct_0 T_2 T_0 T_1)) (m1_subset_1 T_2 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (m2_filter_2 T_1 T_0) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (l3_lattices T_0) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (All A, ((l1_lattices A) => (l1_struct_0 A))) (-. (v3_struct_0 T_0)) ### All 44 % 52.14/52.31 46. (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) (m1_subset_1 T_2 (u1_struct_0 T_0)) ### Axiom % 52.14/52.31 47. ((m1_struct_0 T_2 T_0 T_1) => (m1_subset_1 T_2 (u1_struct_0 T_0))) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) (-. (v3_struct_0 T_0)) (All A, ((l1_lattices A) => (l1_struct_0 A))) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (v10_lattices T_0) (m2_filter_2 T_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (m1_subset_1 T_2 T_1) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) ### Imply 45 46 % 52.14/52.31 48. (All C, ((m1_struct_0 C T_0 T_1) => (m1_subset_1 C (u1_struct_0 T_0)))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (m1_subset_1 T_2 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (m2_filter_2 T_1 T_0) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (l3_lattices T_0) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (All A, ((l1_lattices A) => (l1_struct_0 A))) (-. (v3_struct_0 T_0)) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) ### All 47 % 52.14/52.31 49. (((-. (v3_struct_0 T_0)) /\ ((l1_struct_0 T_0) /\ ((-. (v1_xboole_0 T_1)) /\ (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0)))))) => (All C, ((m1_struct_0 C T_0 T_1) => (m1_subset_1 C (u1_struct_0 T_0))))) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) (m1_subset_1 T_2 T_1) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (m2_filter_2 T_1 T_0) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (l3_lattices T_0) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (All A, ((l1_lattices A) => (l1_struct_0 A))) (-. (v3_struct_0 T_0)) ### DisjTree 1 9 19 37 48 % 52.14/52.31 50. (All B, (((-. (v3_struct_0 T_0)) /\ ((l1_struct_0 T_0) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0)))))) => (All C, ((m1_struct_0 C T_0 B) => (m1_subset_1 C (u1_struct_0 T_0)))))) (-. (v3_struct_0 T_0)) (All A, ((l1_lattices A) => (l1_struct_0 A))) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (v10_lattices T_0) (m2_filter_2 T_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (m1_subset_1 T_2 T_1) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) ### All 49 % 52.14/52.31 51. (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) => (m1_subset_1 C (u1_struct_0 A))))))) (-. (m1_subset_1 T_2 (u1_struct_0 T_0))) (m1_subset_1 T_2 T_1) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (m2_filter_2 T_1 T_0) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (l3_lattices T_0) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (All A, ((l1_lattices A) => (l1_struct_0 A))) (-. (v3_struct_0 T_0)) ### All 50 % 52.14/52.31 52. (m1_subset_1 T_2 T_1) (-. (m1_subset_1 T_2 T_1)) ### Axiom % 52.14/52.31 53. (-. (r2_hidden T_2 T_1)) (r2_hidden T_2 T_1) ### Axiom % 52.14/52.31 54. ((m1_subset_1 T_2 T_1) => ((v1_xboole_0 T_1) \/ (r2_hidden T_2 T_1))) (-. (r2_hidden T_2 T_1)) (m2_filter_2 T_1 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, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (m1_subset_1 T_2 T_1) ### DisjTree 52 19 53 % 52.14/52.31 55. (All B, ((m1_subset_1 T_2 B) => ((v1_xboole_0 B) \/ (r2_hidden T_2 B)))) (m1_subset_1 T_2 T_1) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (-. (v3_struct_0 T_0)) (v10_lattices T_0) (l3_lattices T_0) (m2_filter_2 T_1 T_0) (-. (r2_hidden T_2 T_1)) ### All 54 % 52.14/52.31 56. (All A, (All B, ((m1_subset_1 A B) => ((v1_xboole_0 B) \/ (r2_hidden A B))))) (-. (r2_hidden T_2 T_1)) (m2_filter_2 T_1 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, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (m1_subset_1 T_2 T_1) ### All 55 % 52.14/52.31 57. (-. ((m1_subset_1 T_2 (u1_struct_0 T_0)) /\ (r2_hidden T_2 T_1))) (All A, (All B, ((m1_subset_1 A B) => ((v1_xboole_0 B) \/ (r2_hidden A B))))) (-. (v3_struct_0 T_0)) (All A, ((l1_lattices A) => (l1_struct_0 A))) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (v10_lattices T_0) (m2_filter_2 T_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (m1_subset_1 T_2 T_1) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) => (m1_subset_1 C (u1_struct_0 A))))))) ### NotAnd 51 56 % 52.14/52.31 58. (-. (Ex C, ((m1_subset_1 C (u1_struct_0 T_0)) /\ (r2_hidden C T_1)))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) => (m1_subset_1 C (u1_struct_0 A))))))) (m1_subset_1 T_2 T_1) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (m2_filter_2 T_1 T_0) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (l3_lattices T_0) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (All A, ((l1_lattices A) => (l1_struct_0 A))) (-. (v3_struct_0 T_0)) (All A, (All B, ((m1_subset_1 A B) => ((v1_xboole_0 B) \/ (r2_hidden A B))))) ### NotExists 57 % 52.14/52.32 59. (Ex B, (m1_subset_1 B T_1)) (All A, (All B, ((m1_subset_1 A B) => ((v1_xboole_0 B) \/ (r2_hidden A B))))) (-. (v3_struct_0 T_0)) (All A, ((l1_lattices A) => (l1_struct_0 A))) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (v10_lattices T_0) (m2_filter_2 T_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) => (m1_subset_1 C (u1_struct_0 A))))))) (-. (Ex C, ((m1_subset_1 C (u1_struct_0 T_0)) /\ (r2_hidden C T_1)))) ### Exists 58 % 52.14/52.32 60. (All A, (Ex B, (m1_subset_1 B A))) (-. (Ex C, ((m1_subset_1 C (u1_struct_0 T_0)) /\ (r2_hidden C T_1)))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) => (m1_subset_1 C (u1_struct_0 A))))))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (m2_filter_2 T_1 T_0) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (l3_lattices T_0) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (All A, ((l1_lattices A) => (l1_struct_0 A))) (-. (v3_struct_0 T_0)) (All A, (All B, ((m1_subset_1 A B) => ((v1_xboole_0 B) \/ (r2_hidden A B))))) ### All 59 % 52.14/52.32 61. (-. ((m2_filter_2 T_1 T_0) => (Ex C, ((m1_subset_1 C (u1_struct_0 T_0)) /\ (r2_hidden C T_1))))) (All A, (All B, ((m1_subset_1 A B) => ((v1_xboole_0 B) \/ (r2_hidden A B))))) (-. (v3_struct_0 T_0)) (All A, ((l1_lattices A) => (l1_struct_0 A))) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (l3_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) => (m1_subset_1 C (u1_struct_0 A))))))) (All A, (Ex B, (m1_subset_1 B A))) ### NotImply 60 % 52.14/52.32 62. (-. (All B, ((m2_filter_2 B T_0) => (Ex C, ((m1_subset_1 C (u1_struct_0 T_0)) /\ (r2_hidden C B)))))) (All A, (Ex B, (m1_subset_1 B A))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) => (m1_subset_1 C (u1_struct_0 A))))))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (v10_lattices T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (l3_lattices T_0) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (All A, ((l1_lattices A) => (l1_struct_0 A))) (-. (v3_struct_0 T_0)) (All A, (All B, ((m1_subset_1 A B) => ((v1_xboole_0 B) \/ (r2_hidden A B))))) ### NotAllEx 61 % 52.14/52.32 63. (-. (((-. (v3_struct_0 T_0)) /\ ((v10_lattices T_0) /\ (l3_lattices T_0))) => (All B, ((m2_filter_2 B T_0) => (Ex C, ((m1_subset_1 C (u1_struct_0 T_0)) /\ (r2_hidden C B))))))) (All A, (All B, ((m1_subset_1 A B) => ((v1_xboole_0 B) \/ (r2_hidden A B))))) (All A, ((l1_lattices A) => (l1_struct_0 A))) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) => (m1_subset_1 C (u1_struct_0 A))))))) (All A, (Ex B, (m1_subset_1 B A))) ### ConjTree 62 % 52.14/52.32 64. (-. (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => (Ex C, ((m1_subset_1 C (u1_struct_0 A)) /\ (r2_hidden C B)))))))) (All A, (Ex B, (m1_subset_1 B A))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) => (m1_subset_1 C (u1_struct_0 A))))))) (All A, (All B, (((-. (v3_struct_0 A)) /\ ((l1_struct_0 A) /\ ((-. (v1_xboole_0 B)) /\ (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A)))))) => (All C, ((m1_struct_0 C A B) <=> (m1_subset_1 C B)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_lattice4 B A) => (m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v10_lattices A) /\ (l3_lattices A))) => (All B, ((m2_filter_2 B A) => ((-. (v1_xboole_0 B)) /\ (m2_lattice4 B A)))))) (All A, ((l3_lattices A) => ((l1_lattices A) /\ (l2_lattices A)))) (All A, ((l1_lattices A) => (l1_struct_0 A))) (All A, (All B, ((m1_subset_1 A B) => ((v1_xboole_0 B) \/ (r2_hidden A B))))) ### NotAllEx 63 % 52.14/52.32 % SZS output end Proof % 52.14/52.32 (* END-PROOF *) %------------------------------------------------------------------------------