%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : TOP034+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 : n021.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:24 EDT 2022 % Result : Theorem 3.26s 3.52s % Output : Proof 3.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : TOP034+1 : TPTP v8.1.0. Released v3.4.0. % 0.12/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.35 % Computer : n021.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Sun May 29 05:23:12 EDT 2022 % 0.14/0.35 % CPUTime : % 3.26/3.52 % SZS status Theorem % 3.26/3.52 (* PROOF-FOUND *) % 3.26/3.52 (* BEGIN-PROOF *) % 3.26/3.52 % SZS output start Proof % 3.26/3.52 1. (l1_pre_topc T_0) (-. (l1_pre_topc T_0)) ### Axiom % 3.26/3.52 2. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 3.26/3.52 3. (v2_pre_topc T_0) (-. (v2_pre_topc T_0)) ### Axiom % 3.26/3.52 4. (l1_pre_topc T_0) (-. (l1_pre_topc T_0)) ### Axiom % 3.26/3.52 5. (-. (v3_struct_0 T_1)) (v3_struct_0 T_1) ### Axiom % 3.26/3.52 6. (m2_tsp_1 T_1 T_0) (-. (m2_tsp_1 T_1 T_0)) ### Axiom % 3.26/3.52 7. (-. (m1_pre_topc T_1 T_0)) (m1_pre_topc T_1 T_0) ### Axiom % 3.26/3.52 8. ((m2_tsp_1 T_1 T_0) <=> (m1_pre_topc T_1 T_0)) (-. (m1_pre_topc T_1 T_0)) (m2_tsp_1 T_1 T_0) ### Equiv 6 7 % 3.26/3.52 9. (All B, ((m2_tsp_1 B T_0) <=> (m1_pre_topc B T_0))) (m2_tsp_1 T_1 T_0) (-. (m1_pre_topc T_1 T_0)) ### All 8 % 3.26/3.52 10. (-. (v3_struct_0 T_0)) (v3_struct_0 T_0) ### Axiom % 3.26/3.52 11. (v2_pre_topc T_0) (-. (v2_pre_topc T_0)) ### Axiom % 3.26/3.52 12. (l1_pre_topc T_0) (-. (l1_pre_topc T_0)) ### Axiom % 3.26/3.52 13. (-. (v3_struct_0 T_1)) (v3_struct_0 T_1) ### Axiom % 3.26/3.52 14. (v2_tsp_2 T_1 T_0) (-. (v2_tsp_2 T_1 T_0)) ### Axiom % 3.26/3.52 15. (m2_tsp_1 T_1 T_0) (-. (m2_tsp_1 T_1 T_0)) ### Axiom % 3.26/3.52 16. (-. (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v5_pre_topc C T_0 T_1) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (v3_borsuk_1 C T_0 T_1))))))) (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v5_pre_topc C T_0 T_1) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (v3_borsuk_1 C T_0 T_1)))))) ### Axiom % 3.26/3.52 17. (((-. (v3_struct_0 T_1)) /\ ((v2_tsp_2 T_1 T_0) /\ (m2_tsp_1 T_1 T_0))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v5_pre_topc C T_0 T_1) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (v3_borsuk_1 C T_0 T_1))))))) (-. (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v5_pre_topc C T_0 T_1) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (v3_borsuk_1 C T_0 T_1))))))) (m2_tsp_1 T_1 T_0) (v2_tsp_2 T_1 T_0) (-. (v3_struct_0 T_1)) ### DisjTree 13 14 15 16 % 3.26/3.52 18. (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B T_0) /\ (m2_tsp_1 B T_0))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ ((v5_pre_topc C T_0 B) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ (v3_borsuk_1 C T_0 B)))))))) (-. (v3_struct_0 T_1)) (v2_tsp_2 T_1 T_0) (m2_tsp_1 T_1 T_0) (-. (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v5_pre_topc C T_0 T_1) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (v3_borsuk_1 C T_0 T_1))))))) ### All 17 % 3.26/3.52 19. (((-. (v3_struct_0 T_0)) /\ ((v2_pre_topc T_0) /\ (l1_pre_topc T_0))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B T_0) /\ (m2_tsp_1 B T_0))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ ((v5_pre_topc C T_0 B) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ (v3_borsuk_1 C T_0 B))))))))) (-. (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v5_pre_topc C T_0 T_1) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (v3_borsuk_1 C T_0 T_1))))))) (m2_tsp_1 T_1 T_0) (v2_tsp_2 T_1 T_0) (-. (v3_struct_0 T_1)) (l1_pre_topc T_0) (v2_pre_topc T_0) (-. (v3_struct_0 T_0)) ### DisjTree 10 11 12 18 % 3.26/3.52 20. (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) (-. (v3_struct_0 T_0)) (v2_pre_topc T_0) (l1_pre_topc T_0) (-. (v3_struct_0 T_1)) (v2_tsp_2 T_1 T_0) (m2_tsp_1 T_1 T_0) (-. (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v5_pre_topc C T_0 T_1) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (v3_borsuk_1 C T_0 T_1))))))) ### All 19 % 3.26/3.52 21. (-. (r1_borsuk_1 T_0 T_1)) (r1_borsuk_1 T_0 T_1) ### Axiom % 3.26/3.52 22. ((r1_borsuk_1 T_0 T_1) <=> (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v5_pre_topc C T_0 T_1) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (v3_borsuk_1 C T_0 T_1))))))) (-. (r1_borsuk_1 T_0 T_1)) (m2_tsp_1 T_1 T_0) (v2_tsp_2 T_1 T_0) (-. (v3_struct_0 T_1)) (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, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) ### Equiv 20 21 % 3.26/3.52 23. (((-. (v3_struct_0 T_1)) /\ (m1_pre_topc T_1 T_0)) => ((r1_borsuk_1 T_0 T_1) <=> (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ ((v5_pre_topc C T_0 T_1) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 T_1)) /\ (v3_borsuk_1 C T_0 T_1)))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) (-. (v3_struct_0 T_0)) (v2_pre_topc T_0) (l1_pre_topc T_0) (v2_tsp_2 T_1 T_0) (-. (r1_borsuk_1 T_0 T_1)) (m2_tsp_1 T_1 T_0) (All B, ((m2_tsp_1 B T_0) <=> (m1_pre_topc B T_0))) (-. (v3_struct_0 T_1)) ### DisjTree 5 9 22 % 3.26/3.52 24. (All B, (((-. (v3_struct_0 B)) /\ (m1_pre_topc B T_0)) => ((r1_borsuk_1 T_0 B) <=> (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ ((v5_pre_topc C T_0 B) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ (v3_borsuk_1 C T_0 B))))))))) (-. (v3_struct_0 T_1)) (All B, ((m2_tsp_1 B T_0) <=> (m1_pre_topc B T_0))) (m2_tsp_1 T_1 T_0) (-. (r1_borsuk_1 T_0 T_1)) (v2_tsp_2 T_1 T_0) (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, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) ### All 23 % 3.26/3.52 25. (((-. (v3_struct_0 T_0)) /\ ((v2_pre_topc T_0) /\ (l1_pre_topc T_0))) => (All B, (((-. (v3_struct_0 B)) /\ (m1_pre_topc B T_0)) => ((r1_borsuk_1 T_0 B) <=> (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ ((v5_pre_topc C T_0 B) /\ ((m2_relset_1 C (u1_struct_0 T_0) (u1_struct_0 B)) /\ (v3_borsuk_1 C T_0 B)))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) (v2_tsp_2 T_1 T_0) (-. (r1_borsuk_1 T_0 T_1)) (m2_tsp_1 T_1 T_0) (All B, ((m2_tsp_1 B T_0) <=> (m1_pre_topc B T_0))) (-. (v3_struct_0 T_1)) (l1_pre_topc T_0) (v2_pre_topc T_0) (-. (v3_struct_0 T_0)) ### DisjTree 2 3 4 24 % 3.26/3.52 26. (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ (m1_pre_topc B A)) => ((r1_borsuk_1 A B) <=> (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B))))))))))) (-. (v3_struct_0 T_0)) (v2_pre_topc T_0) (l1_pre_topc T_0) (-. (v3_struct_0 T_1)) (All B, ((m2_tsp_1 B T_0) <=> (m1_pre_topc B T_0))) (m2_tsp_1 T_1 T_0) (-. (r1_borsuk_1 T_0 T_1)) (v2_tsp_2 T_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) ### All 25 % 3.26/3.52 27. ((l1_pre_topc T_0) => (All B, ((m2_tsp_1 B T_0) <=> (m1_pre_topc B T_0)))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) (v2_tsp_2 T_1 T_0) (-. (r1_borsuk_1 T_0 T_1)) (m2_tsp_1 T_1 T_0) (-. (v3_struct_0 T_1)) (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, (((-. (v3_struct_0 B)) /\ (m1_pre_topc B A)) => ((r1_borsuk_1 A B) <=> (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B))))))))))) (l1_pre_topc T_0) ### Imply 1 26 % 3.26/3.53 28. (All A, ((l1_pre_topc A) => (All B, ((m2_tsp_1 B A) <=> (m1_pre_topc B A))))) (l1_pre_topc T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ (m1_pre_topc B A)) => ((r1_borsuk_1 A B) <=> (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B))))))))))) (-. (v3_struct_0 T_0)) (v2_pre_topc T_0) (-. (v3_struct_0 T_1)) (m2_tsp_1 T_1 T_0) (-. (r1_borsuk_1 T_0 T_1)) (v2_tsp_2 T_1 T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) ### All 27 % 3.26/3.53 29. (-. (((-. (v3_struct_0 T_1)) /\ ((v2_tsp_2 T_1 T_0) /\ (m2_tsp_1 T_1 T_0))) => (r1_borsuk_1 T_0 T_1))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) (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, (((-. (v3_struct_0 B)) /\ (m1_pre_topc B A)) => ((r1_borsuk_1 A B) <=> (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B))))))))))) (l1_pre_topc T_0) (All A, ((l1_pre_topc A) => (All B, ((m2_tsp_1 B A) <=> (m1_pre_topc B A))))) ### ConjTree 28 % 3.26/3.53 30. (-. (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B T_0) /\ (m2_tsp_1 B T_0))) => (r1_borsuk_1 T_0 B)))) (All A, ((l1_pre_topc A) => (All B, ((m2_tsp_1 B A) <=> (m1_pre_topc B A))))) (l1_pre_topc T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ (m1_pre_topc B A)) => ((r1_borsuk_1 A B) <=> (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B))))))))))) (-. (v3_struct_0 T_0)) (v2_pre_topc T_0) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) ### NotAllEx 29 % 3.26/3.53 31. (-. (((-. (v3_struct_0 T_0)) /\ ((v2_pre_topc T_0) /\ (l1_pre_topc T_0))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B T_0) /\ (m2_tsp_1 B T_0))) => (r1_borsuk_1 T_0 B))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ (m1_pre_topc B A)) => ((r1_borsuk_1 A B) <=> (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B))))))))))) (All A, ((l1_pre_topc A) => (All B, ((m2_tsp_1 B A) <=> (m1_pre_topc B A))))) ### ConjTree 30 % 3.26/3.53 32. (-. (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (r1_borsuk_1 A B)))))) (All A, ((l1_pre_topc A) => (All B, ((m2_tsp_1 B A) <=> (m1_pre_topc B A))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ (m1_pre_topc B A)) => ((r1_borsuk_1 A B) <=> (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B))))))))))) (All A, (((-. (v3_struct_0 A)) /\ ((v2_pre_topc A) /\ (l1_pre_topc A))) => (All B, (((-. (v3_struct_0 B)) /\ ((v2_tsp_2 B A) /\ (m2_tsp_1 B A))) => (Ex C, ((v1_funct_1 C) /\ ((v1_funct_2 C (u1_struct_0 A) (u1_struct_0 B)) /\ ((v5_pre_topc C A B) /\ ((m2_relset_1 C (u1_struct_0 A) (u1_struct_0 B)) /\ (v3_borsuk_1 C A B)))))))))) ### NotAllEx 31 % 3.26/3.53 % SZS output end Proof % 3.26/3.53 (* END-PROOF *) %------------------------------------------------------------------------------