%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : TOP025+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 : n028.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 : Thu Jul 21 21:35:22 EDT 2022 % Result : Theorem 10.63s 10.82s % Output : Proof 10.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : TOP025+1 : TPTP v8.1.0. Released v3.4.0. % 0.11/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n028.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun May 29 04:12:18 EDT 2022 % 0.12/0.34 % CPUTime : % 10.63/10.82 % SZS status Theorem % 10.63/10.82 (* PROOF-FOUND *) % 10.63/10.82 (* BEGIN-PROOF *) % 10.63/10.82 % SZS output start Proof % 10.63/10.82 1. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 10.63/10.82 2. (v2_pre_topc T_0) (-. (v2_pre_topc T_0)) ### Axiom % 10.63/10.82 3. (l1_pre_topc T_0) (-. (l1_pre_topc T_0)) ### Axiom % 10.63/10.82 4. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 10.63/10.82 5. (v2_pre_topc T_0) (-. (v2_pre_topc T_0)) ### Axiom % 10.63/10.82 6. (l1_pre_topc T_0) (-. (l1_pre_topc T_0)) ### Axiom % 10.63/10.82 7. (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 % 10.63/10.82 8. (v3_pre_topc T_1 T_0) (-. (v3_pre_topc T_1 T_0)) ### Axiom % 10.63/10.82 9. (-. (r1_tarski T_1 T_1)) ### Refl(r1_tarski) % 10.63/10.82 10. (-. (m1_subset_1 T_1 (k1_zfmisc_1 T_1))) (m1_subset_1 T_1 (k1_zfmisc_1 T_1)) ### Axiom % 10.63/10.82 11. ((m1_subset_1 T_1 (k1_zfmisc_1 T_1)) <=> (r1_tarski T_1 T_1)) (-. (m1_subset_1 T_1 (k1_zfmisc_1 T_1))) ### Equiv 9 10 % 10.63/10.82 12. (All B, ((m1_subset_1 T_1 (k1_zfmisc_1 B)) <=> (r1_tarski T_1 B))) (-. (m1_subset_1 T_1 (k1_zfmisc_1 T_1))) ### All 11 % 10.63/10.82 13. (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (-. (m1_subset_1 T_1 (k1_zfmisc_1 T_1))) ### All 12 % 10.63/10.82 14. (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 % 10.63/10.82 15. (v1_tsp_2 T_1 T_0) (-. (v1_tsp_2 T_1 T_0)) ### Axiom % 10.63/10.82 16. (-. (T_1 != T_1)) (T_1 != T_1) ### Axiom % 10.63/10.82 17. ((k3_tex_4 T_0 T_1) = (u1_struct_0 T_0)) ((u1_struct_0 T_0) != (k3_tex_4 T_0 T_1)) ### Sym(=) % 10.63/10.82 18. ((k1_zfmisc_1 (u1_struct_0 T_0)) != (k1_zfmisc_1 (k3_tex_4 T_0 T_1))) ((k3_tex_4 T_0 T_1) = (u1_struct_0 T_0)) ### NotEqual 17 % 10.63/10.82 19. (-. (m1_subset_1 T_1 (k1_zfmisc_1 (k3_tex_4 T_0 T_1)))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ((k3_tex_4 T_0 T_1) = (u1_struct_0 T_0)) (-. (T_1 != T_1)) ### P-NotP 16 18 % 10.63/10.82 20. (-. (T_1 != T_1)) (T_1 != T_1) ### Axiom % 10.63/10.82 21. (-. (v1_tex_2 T_1 (k1_zfmisc_1 (k3_tex_4 T_0 T_1)))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ((k3_tex_4 T_0 T_1) = (u1_struct_0 T_0)) (-. (T_1 != T_1)) ### P-NotP 20 18 % 10.63/10.82 22. ((k3_tex_4 T_0 T_1) = T_1) (T_1 != (k3_tex_4 T_0 T_1)) ### Sym(=) % 10.63/10.82 23. ((v1_tex_2 T_1 (k1_zfmisc_1 (k3_tex_4 T_0 T_1))) <=> (T_1 != (k3_tex_4 T_0 T_1))) ((k3_tex_4 T_0 T_1) = T_1) (-. (T_1 != T_1)) ((k3_tex_4 T_0 T_1) = (u1_struct_0 T_0)) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ### Equiv 21 22 % 10.63/10.82 24. ((m1_subset_1 T_1 (k1_zfmisc_1 (k3_tex_4 T_0 T_1))) => ((v1_tex_2 T_1 (k1_zfmisc_1 (k3_tex_4 T_0 T_1))) <=> (T_1 != (k3_tex_4 T_0 T_1)))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ((k3_tex_4 T_0 T_1) = T_1) (-. (T_1 != T_1)) ((k3_tex_4 T_0 T_1) = (u1_struct_0 T_0)) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ### Imply 19 23 % 10.63/10.82 25. (All B, ((m1_subset_1 B (k1_zfmisc_1 (k3_tex_4 T_0 T_1))) => ((v1_tex_2 B (k1_zfmisc_1 (k3_tex_4 T_0 T_1))) <=> (B != (k3_tex_4 T_0 T_1))))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ((k3_tex_4 T_0 T_1) = (u1_struct_0 T_0)) (-. (T_1 != T_1)) ((k3_tex_4 T_0 T_1) = T_1) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ### All 24 % 10.63/10.82 26. (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ((k3_tex_4 T_0 T_1) = T_1) (-. (T_1 != T_1)) ((k3_tex_4 T_0 T_1) = (u1_struct_0 T_0)) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ### All 25 % 10.63/10.82 27. ((v1_tsp_1 T_1 T_0) /\ ((k3_tex_4 T_0 T_1) = (u1_struct_0 T_0))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (-. (T_1 != T_1)) ((k3_tex_4 T_0 T_1) = T_1) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) ### And 26 % 10.63/10.82 28. ((v1_tsp_2 T_1 T_0) <=> ((v1_tsp_1 T_1 T_0) /\ ((k3_tex_4 T_0 T_1) = (u1_struct_0 T_0)))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ((k3_tex_4 T_0 T_1) = T_1) (-. (T_1 != T_1)) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v1_tsp_2 T_1 T_0) ### Equiv 15 27 % 10.63/10.82 29. ((m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 T_1 T_0) <=> ((v1_tsp_1 T_1 T_0) /\ ((k3_tex_4 T_0 T_1) = (u1_struct_0 T_0))))) (v1_tsp_2 T_1 T_0) (-. (T_1 != T_1)) ((k3_tex_4 T_0 T_1) = T_1) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ### Imply 14 28 % 10.63/10.82 30. (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ((k3_tex_4 T_0 T_1) = T_1) (-. (T_1 != T_1)) (v1_tsp_2 T_1 T_0) ### All 29 % 10.63/10.82 31. (T_1 != T_1) ### Refl(=) % 10.63/10.82 32. ((v1_tex_2 T_1 (k1_zfmisc_1 T_1)) <=> (T_1 != T_1)) (v1_tsp_2 T_1 T_0) ((k3_tex_4 T_0 T_1) = T_1) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) ### Equiv 30 31 % 10.63/10.82 33. ((m1_subset_1 T_1 (k1_zfmisc_1 T_1)) => ((v1_tex_2 T_1 (k1_zfmisc_1 T_1)) <=> (T_1 != T_1))) (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ((k3_tex_4 T_0 T_1) = T_1) (v1_tsp_2 T_1 T_0) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) ### Imply 13 32 % 10.63/10.82 34. (All B, ((m1_subset_1 B (k1_zfmisc_1 T_1)) => ((v1_tex_2 B (k1_zfmisc_1 T_1)) <=> (B != T_1)))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (v1_tsp_2 T_1 T_0) ((k3_tex_4 T_0 T_1) = T_1) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) ### All 33 % 10.63/10.82 35. (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ((k3_tex_4 T_0 T_1) = T_1) (v1_tsp_2 T_1 T_0) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) ### All 34 % 10.63/10.82 36. ((m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v3_pre_topc T_1 T_0) => ((k3_tex_4 T_0 T_1) = T_1))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (v1_tsp_2 T_1 T_0) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) (v3_pre_topc T_1 T_0) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ### DisjTree 7 8 35 % 10.63/10.82 37. (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v3_pre_topc B T_0) => ((k3_tex_4 T_0 B) = B)))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v3_pre_topc T_1 T_0) (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v1_tsp_2 T_1 T_0) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) ### All 36 % 10.63/10.82 38. (((-. (v3_struct_0 T_0)) /\ ((v2_pre_topc T_0) /\ (l1_pre_topc T_0))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v3_pre_topc B T_0) => ((k3_tex_4 T_0 B) = B))))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (v1_tsp_2 T_1 T_0) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) (v3_pre_topc T_1 T_0) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (l1_pre_topc T_0) (v2_pre_topc T_0) (-. (v3_struct_0 T_0)) ### DisjTree 4 5 6 37 % 10.63/10.85 39. (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v3_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (-. (v3_struct_0 T_0)) (v2_pre_topc T_0) (l1_pre_topc T_0) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v3_pre_topc T_1 T_0) (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v1_tsp_2 T_1 T_0) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) ### All 38 % 10.63/10.85 40. (((-. (v3_struct_0 T_0)) /\ ((v2_pre_topc T_0) /\ (l1_pre_topc T_0))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0))))))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (v1_tsp_2 T_1 T_0) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v3_pre_topc T_1 T_0) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v3_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (l1_pre_topc T_0) (v2_pre_topc T_0) (-. (v3_struct_0 T_0)) ### DisjTree 1 2 3 39 % 10.63/10.85 41. (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v1_tsp_2 B A) <=> ((v1_tsp_1 B A) /\ ((k3_tex_4 A B) = (u1_struct_0 A)))))))) (-. (v3_struct_0 T_0)) (v2_pre_topc T_0) (l1_pre_topc T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v3_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v3_pre_topc T_1 T_0) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v1_tsp_2 T_1 T_0) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) ### All 40 % 10.63/10.85 42. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 10.63/10.85 43. (v2_pre_topc T_0) (-. (v2_pre_topc T_0)) ### Axiom % 10.63/10.85 44. (l1_pre_topc T_0) (-. (l1_pre_topc T_0)) ### Axiom % 10.63/10.85 45. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 10.63/10.85 46. (v2_pre_topc T_0) (-. (v2_pre_topc T_0)) ### Axiom % 10.63/10.85 47. (l1_pre_topc T_0) (-. (l1_pre_topc T_0)) ### Axiom % 10.63/10.85 48. (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 % 10.63/10.85 49. (v4_pre_topc T_1 T_0) (-. (v4_pre_topc T_1 T_0)) ### Axiom % 10.63/10.85 50. ((m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v4_pre_topc T_1 T_0) => ((k3_tex_4 T_0 T_1) = T_1))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (v1_tsp_2 T_1 T_0) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) (v4_pre_topc T_1 T_0) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) ### DisjTree 48 49 35 % 10.63/10.85 51. (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v4_pre_topc B T_0) => ((k3_tex_4 T_0 B) = B)))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v4_pre_topc T_1 T_0) (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v1_tsp_2 T_1 T_0) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) ### All 50 % 10.63/10.85 52. (((-. (v3_struct_0 T_0)) /\ ((v2_pre_topc T_0) /\ (l1_pre_topc T_0))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v4_pre_topc B T_0) => ((k3_tex_4 T_0 B) = B))))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (v1_tsp_2 T_1 T_0) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) (v4_pre_topc T_1 T_0) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (l1_pre_topc T_0) (v2_pre_topc T_0) (-. (v3_struct_0 T_0)) ### DisjTree 45 46 47 51 % 10.63/10.85 53. (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v4_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (-. (v3_struct_0 T_0)) (v2_pre_topc T_0) (l1_pre_topc T_0) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v4_pre_topc T_1 T_0) (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0)))))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v1_tsp_2 T_1 T_0) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) ### All 52 % 10.63/10.85 54. (((-. (v3_struct_0 T_0)) /\ ((v2_pre_topc T_0) /\ (l1_pre_topc T_0))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => ((v1_tsp_2 B T_0) <=> ((v1_tsp_1 B T_0) /\ ((k3_tex_4 T_0 B) = (u1_struct_0 T_0))))))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (v1_tsp_2 T_1 T_0) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v4_pre_topc T_1 T_0) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v4_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (l1_pre_topc T_0) (v2_pre_topc T_0) (-. (v3_struct_0 T_0)) ### DisjTree 42 43 44 53 % 10.63/10.85 55. (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v1_tsp_2 B A) <=> ((v1_tsp_1 B A) /\ ((k3_tex_4 A B) = (u1_struct_0 A)))))))) (-. (v3_struct_0 T_0)) (v2_pre_topc T_0) (l1_pre_topc T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v4_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v4_pre_topc T_1 T_0) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (v1_tsp_2 T_1 T_0) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) ### All 54 % 10.63/10.85 56. ((v3_pre_topc T_1 T_0) \/ (v4_pre_topc T_1 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v4_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (v1_tsp_2 T_1 T_0) (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v3_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (l1_pre_topc T_0) (v2_pre_topc T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v1_tsp_2 B A) <=> ((v1_tsp_1 B A) /\ ((k3_tex_4 A B) = (u1_struct_0 A)))))))) ### Or 41 55 % 10.86/11.06 57. (-. ((m1_subset_1 T_1 (k1_zfmisc_1 (u1_struct_0 T_0))) => (-. (((v3_pre_topc T_1 T_0) \/ (v4_pre_topc T_1 T_0)) /\ ((v1_tsp_2 T_1 T_0) /\ (v1_tex_2 T_1 (k1_zfmisc_1 (u1_struct_0 T_0)))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v1_tsp_2 B A) <=> ((v1_tsp_1 B A) /\ ((k3_tex_4 A B) = (u1_struct_0 A)))))))) (-. (v3_struct_0 T_0)) (v2_pre_topc T_0) (l1_pre_topc T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v3_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v4_pre_topc B A) => ((k3_tex_4 A B) = B)))))) ### ConjTree 56 % 10.86/11.06 58. (-. (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => (-. (((v3_pre_topc B T_0) \/ (v4_pre_topc B T_0)) /\ ((v1_tsp_2 B T_0) /\ (v1_tex_2 B (k1_zfmisc_1 (u1_struct_0 T_0))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v4_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v3_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (l1_pre_topc T_0) (v2_pre_topc T_0) (-. (v3_struct_0 T_0)) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v1_tsp_2 B A) <=> ((v1_tsp_1 B A) /\ ((k3_tex_4 A B) = (u1_struct_0 A)))))))) ### NotAllEx 57 % 10.86/11.06 59. (-. (((-. (v3_struct_0 T_0)) /\ ((v2_pre_topc T_0) /\ (l1_pre_topc T_0))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 T_0))) => (-. (((v3_pre_topc B T_0) \/ (v4_pre_topc B T_0)) /\ ((v1_tsp_2 B T_0) /\ (v1_tex_2 B (k1_zfmisc_1 (u1_struct_0 T_0)))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v1_tsp_2 B A) <=> ((v1_tsp_1 B A) /\ ((k3_tex_4 A B) = (u1_struct_0 A)))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v3_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v4_pre_topc B A) => ((k3_tex_4 A B) = B)))))) ### ConjTree 58 % 10.86/11.06 60. (-. (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => (-. (((v3_pre_topc B A) \/ (v4_pre_topc B A)) /\ ((v1_tsp_2 B A) /\ (v1_tex_2 B (k1_zfmisc_1 (u1_struct_0 A))))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v4_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (All A, (All B, ((m1_subset_1 A (k1_zfmisc_1 B)) <=> (r1_tarski A B)))) (All A, (All B, ((m1_subset_1 B (k1_zfmisc_1 A)) => ((v1_tex_2 B (k1_zfmisc_1 A)) <=> (B != A))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v3_pre_topc B A) => ((k3_tex_4 A B) = B)))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, ((m1_subset_1 B (k1_zfmisc_1 (u1_struct_0 A))) => ((v1_tsp_2 B A) <=> ((v1_tsp_1 B A) /\ ((k3_tex_4 A B) = (u1_struct_0 A)))))))) ### NotAllEx 59 % 10.86/11.06 % SZS output end Proof % 10.86/11.06 (* END-PROOF *) %------------------------------------------------------------------------------