%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU356+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n020.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 : Tue Jul 19 14:50:31 EDT 2022 % Result : Theorem 0.84s 1.02s % Output : Proof 0.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SEU356+1 : TPTP v8.1.0. Released v3.3.0. % 0.08/0.15 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.15/0.37 % Computer : n020.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 600 % 0.15/0.37 % DateTime : Sun Jun 19 00:35:03 EDT 2022 % 0.15/0.37 % CPUTime : % 0.84/1.02 % SZS status Theorem % 0.84/1.02 (* PROOF-FOUND *) % 0.84/1.02 (* BEGIN-PROOF *) % 0.84/1.02 % SZS output start Proof % 0.84/1.02 1. (rel_str T_0) (-. (rel_str T_0)) ### Axiom % 0.84/1.02 2. (antisymmetric_relstr T_0) (-. (antisymmetric_relstr T_0)) ### Axiom % 0.84/1.02 3. (rel_str T_0) (-. (rel_str T_0)) ### Axiom % 0.84/1.02 4. (element T_1 (the_carrier T_0)) (-. (element T_1 (the_carrier T_0))) ### Axiom % 0.84/1.02 5. (element T_1 (the_carrier T_0)) (-. (element T_1 (the_carrier T_0))) ### Axiom % 0.84/1.02 6. (relstr_set_smaller T_0 T_2 T_1) (-. (relstr_set_smaller T_0 T_2 T_1)) ### Axiom % 0.84/1.02 7. (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (-. (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D))))) ### Axiom % 0.84/1.02 8. (element T_1 (the_carrier T_0)) (-. (element T_1 (the_carrier T_0))) ### Axiom % 0.84/1.02 9. (relstr_set_smaller T_0 T_2 T_1) (-. (relstr_set_smaller T_0 T_2 T_1)) ### Axiom % 0.84/1.02 10. (element T_3 (the_carrier T_0)) (-. (element T_3 (the_carrier T_0))) ### Axiom % 0.84/1.02 11. (element T_3 (the_carrier T_0)) (-. (element T_3 (the_carrier T_0))) ### Axiom % 0.84/1.02 12. (relstr_set_smaller T_0 T_2 T_3) (-. (relstr_set_smaller T_0 T_2 T_3)) ### Axiom % 0.84/1.02 13. (-. (related T_0 T_1 T_3)) (related T_0 T_1 T_3) ### Axiom % 0.84/1.02 14. ((element T_3 (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 T_3) => (related T_0 T_1 T_3))) (-. (related T_0 T_1 T_3)) (relstr_set_smaller T_0 T_2 T_3) (element T_3 (the_carrier T_0)) ### DisjTree 11 12 13 % 0.84/1.02 15. (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (element T_3 (the_carrier T_0)) (relstr_set_smaller T_0 T_2 T_3) (-. (related T_0 T_1 T_3)) ### All 14 % 0.84/1.02 16. (related T_0 T_3 T_1) (-. (related T_0 T_3 T_1)) ### Axiom % 0.84/1.02 17. (T_3 != T_1) (T_1 = T_3) ### Sym(=) % 0.84/1.02 18. ((element T_3 (the_carrier T_0)) => (((related T_0 T_1 T_3) /\ (related T_0 T_3 T_1)) => (T_1 = T_3))) (T_3 != T_1) (related T_0 T_3 T_1) (relstr_set_smaller T_0 T_2 T_3) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (element T_3 (the_carrier T_0)) ### DisjTree 10 15 16 17 % 0.84/1.02 19. (All C, ((element C (the_carrier T_0)) => (((related T_0 T_1 C) /\ (related T_0 C T_1)) => (T_1 = C)))) (element T_3 (the_carrier T_0)) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (relstr_set_smaller T_0 T_2 T_3) (related T_0 T_3 T_1) (T_3 != T_1) ### All 18 % 0.84/1.02 20. ((element T_1 (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 T_1) => (related T_0 T_3 T_1))) (T_3 != T_1) (relstr_set_smaller T_0 T_2 T_3) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (element T_3 (the_carrier T_0)) (All C, ((element C (the_carrier T_0)) => (((related T_0 T_1 C) /\ (related T_0 C T_1)) => (T_1 = C)))) (relstr_set_smaller T_0 T_2 T_1) (element T_1 (the_carrier T_0)) ### DisjTree 8 9 19 % 0.84/1.02 21. (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 T_3 E)))) (element T_1 (the_carrier T_0)) (relstr_set_smaller T_0 T_2 T_1) (All C, ((element C (the_carrier T_0)) => (((related T_0 T_1 C) /\ (related T_0 C T_1)) => (T_1 = C)))) (element T_3 (the_carrier T_0)) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (relstr_set_smaller T_0 T_2 T_3) (T_3 != T_1) ### All 20 % 0.84/1.02 22. (-. ((element T_3 (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 T_3) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 T_3 E))))) => (T_3 = T_1)))) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (All C, ((element C (the_carrier T_0)) => (((related T_0 T_1 C) /\ (related T_0 C T_1)) => (T_1 = C)))) (relstr_set_smaller T_0 T_2 T_1) (element T_1 (the_carrier T_0)) ### ConjTree 21 % 0.84/1.02 23. (-. (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 D E))))) => (D = T_1))))) (element T_1 (the_carrier T_0)) (relstr_set_smaller T_0 T_2 T_1) (All C, ((element C (the_carrier T_0)) => (((related T_0 T_1 C) /\ (related T_0 C T_1)) => (T_1 = C)))) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) ### NotAllEx 22 % 0.84/1.02 24. (-. ((element T_1 (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 T_1) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 D E))))) => (D = T_1)))))))) (All C, ((element C (the_carrier T_0)) => (((related T_0 T_1 C) /\ (related T_0 C T_1)) => (T_1 = C)))) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (relstr_set_smaller T_0 T_2 T_1) (element T_1 (the_carrier T_0)) ### DisjTree 5 6 7 23 % 0.84/1.02 25. (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 D E))))) => (D = C))))))))) (element T_1 (the_carrier T_0)) (relstr_set_smaller T_0 T_2 T_1) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (All C, ((element C (the_carrier T_0)) => (((related T_0 T_1 C) /\ (related T_0 C T_1)) => (T_1 = C)))) ### NotExists 24 % 0.84/1.02 26. ((element T_1 (the_carrier T_0)) => (All C, ((element C (the_carrier T_0)) => (((related T_0 T_1 C) /\ (related T_0 C T_1)) => (T_1 = C))))) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (relstr_set_smaller T_0 T_2 T_1) (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 D E))))) => (D = C))))))))) (element T_1 (the_carrier T_0)) ### Imply 4 25 % 0.84/1.02 27. (All B, ((element B (the_carrier T_0)) => (All C, ((element C (the_carrier T_0)) => (((related T_0 B C) /\ (related T_0 C B)) => (B = C)))))) (element T_1 (the_carrier T_0)) (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 D E))))) => (D = C))))))))) (relstr_set_smaller T_0 T_2 T_1) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) ### All 26 % 0.84/1.02 28. (((antisymmetric_relstr T_0) /\ (rel_str T_0)) => (All B, ((element B (the_carrier T_0)) => (All C, ((element C (the_carrier T_0)) => (((related T_0 B C) /\ (related T_0 C B)) => (B = C))))))) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (relstr_set_smaller T_0 T_2 T_1) (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 D E))))) => (D = C))))))))) (element T_1 (the_carrier T_0)) (rel_str T_0) (antisymmetric_relstr T_0) ### DisjTree 2 3 27 % 0.84/1.02 29. (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((element B (the_carrier A)) => (All C, ((element C (the_carrier A)) => (((related A B C) /\ (related A C B)) => (B = C)))))))) (antisymmetric_relstr T_0) (rel_str T_0) (element T_1 (the_carrier T_0)) (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 D E))))) => (D = C))))))))) (relstr_set_smaller T_0 T_2 T_1) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) ### All 28 % 0.84/1.03 30. (-. (ex_sup_of_relstr_set T_0 T_2)) (ex_sup_of_relstr_set T_0 T_2) ### Axiom % 0.84/1.03 31. ((ex_sup_of_relstr_set T_0 T_2) <=> (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 D E))))) => (D = C))))))))) (-. (ex_sup_of_relstr_set T_0 T_2)) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (relstr_set_smaller T_0 T_2 T_1) (element T_1 (the_carrier T_0)) (rel_str T_0) (antisymmetric_relstr T_0) (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((element B (the_carrier A)) => (All C, ((element C (the_carrier A)) => (((related A B C) /\ (related A C B)) => (B = C)))))))) ### Equiv 29 30 % 0.84/1.03 32. (All B, ((ex_sup_of_relstr_set T_0 B) <=> (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 B C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 B D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 B D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 B E) => (related T_0 D E))))) => (D = C)))))))))) (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((element B (the_carrier A)) => (All C, ((element C (the_carrier A)) => (((related A B C) /\ (related A C B)) => (B = C)))))))) (antisymmetric_relstr T_0) (rel_str T_0) (element T_1 (the_carrier T_0)) (relstr_set_smaller T_0 T_2 T_1) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (-. (ex_sup_of_relstr_set T_0 T_2)) ### All 31 % 0.84/1.03 33. ((rel_str T_0) => (All B, ((ex_sup_of_relstr_set T_0 B) <=> (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 B C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 B D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 B D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 B E) => (related T_0 D E))))) => (D = C))))))))))) (-. (ex_sup_of_relstr_set T_0 T_2)) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (relstr_set_smaller T_0 T_2 T_1) (element T_1 (the_carrier T_0)) (antisymmetric_relstr T_0) (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((element B (the_carrier A)) => (All C, ((element C (the_carrier A)) => (((related A B C) /\ (related A C B)) => (B = C)))))))) (rel_str T_0) ### Imply 1 32 % 0.84/1.03 34. (All A, ((rel_str A) => (All B, ((ex_sup_of_relstr_set A B) <=> (Ex C, ((element C (the_carrier A)) /\ ((relstr_set_smaller A B C) /\ ((All D, ((element D (the_carrier A)) => ((relstr_set_smaller A B D) => (related A C D)))) /\ (All D, ((element D (the_carrier A)) => (((relstr_set_smaller A B D) /\ (All E, ((element E (the_carrier A)) => ((relstr_set_smaller A B E) => (related A D E))))) => (D = C)))))))))))) (rel_str T_0) (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((element B (the_carrier A)) => (All C, ((element C (the_carrier A)) => (((related A B C) /\ (related A C B)) => (B = C)))))))) (antisymmetric_relstr T_0) (element T_1 (the_carrier T_0)) (relstr_set_smaller T_0 T_2 T_1) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))) (-. (ex_sup_of_relstr_set T_0 T_2)) ### All 33 % 0.84/1.03 35. ((element T_1 (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 T_1) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_1 D)))))) (-. (ex_sup_of_relstr_set T_0 T_2)) (antisymmetric_relstr T_0) (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((element B (the_carrier A)) => (All C, ((element C (the_carrier A)) => (((related A B C) /\ (related A C B)) => (B = C)))))))) (rel_str T_0) (All A, ((rel_str A) => (All B, ((ex_sup_of_relstr_set A B) <=> (Ex C, ((element C (the_carrier A)) /\ ((relstr_set_smaller A B C) /\ ((All D, ((element D (the_carrier A)) => ((relstr_set_smaller A B D) => (related A C D)))) /\ (All D, ((element D (the_carrier A)) => (((relstr_set_smaller A B D) /\ (All E, ((element E (the_carrier A)) => ((relstr_set_smaller A B E) => (related A D E))))) => (D = C)))))))))))) ### ConjTree 34 % 0.84/1.03 36. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D))))))) (All A, ((rel_str A) => (All B, ((ex_sup_of_relstr_set A B) <=> (Ex C, ((element C (the_carrier A)) /\ ((relstr_set_smaller A B C) /\ ((All D, ((element D (the_carrier A)) => ((relstr_set_smaller A B D) => (related A C D)))) /\ (All D, ((element D (the_carrier A)) => (((relstr_set_smaller A B D) /\ (All E, ((element E (the_carrier A)) => ((relstr_set_smaller A B E) => (related A D E))))) => (D = C)))))))))))) (rel_str T_0) (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((element B (the_carrier A)) => (All C, ((element C (the_carrier A)) => (((related A B C) /\ (related A C B)) => (B = C)))))))) (antisymmetric_relstr T_0) (-. (ex_sup_of_relstr_set T_0 T_2)) ### Exists 35 % 0.84/1.03 37. (rel_str T_0) (-. (rel_str T_0)) ### Axiom % 0.84/1.03 38. (ex_sup_of_relstr_set T_0 T_2) (-. (ex_sup_of_relstr_set T_0 T_2)) ### Axiom % 0.84/1.03 39. (element T_4 (the_carrier T_0)) (-. (element T_4 (the_carrier T_0))) ### Axiom % 0.84/1.03 40. (relstr_set_smaller T_0 T_2 T_4) (-. (relstr_set_smaller T_0 T_2 T_4)) ### Axiom % 0.84/1.03 41. (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_4 D)))) (-. (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_4 D))))) ### Axiom % 0.84/1.03 42. (-. ((element T_4 (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 T_4) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_4 D))))))) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_4 D)))) (relstr_set_smaller T_0 T_2 T_4) (element T_4 (the_carrier T_0)) ### DisjTree 39 40 41 % 0.84/1.03 43. (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))))))) (element T_4 (the_carrier T_0)) (relstr_set_smaller T_0 T_2 T_4) (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_4 D)))) ### NotExists 42 % 0.84/1.03 44. ((element T_4 (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 T_4) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 T_4 D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 D E))))) => (D = T_4))))))) (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))))))) ### ConjTree 43 % 0.84/1.03 45. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 D E))))) => (D = C)))))))) (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))))))) ### Exists 44 % 0.84/1.03 46. ((ex_sup_of_relstr_set T_0 T_2) <=> (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 T_2 D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 E) => (related T_0 D E))))) => (D = C))))))))) (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))))))) (ex_sup_of_relstr_set T_0 T_2) ### Equiv 38 45 % 0.84/1.03 47. (All B, ((ex_sup_of_relstr_set T_0 B) <=> (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 B C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 B D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 B D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 B E) => (related T_0 D E))))) => (D = C)))))))))) (ex_sup_of_relstr_set T_0 T_2) (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))))))) ### All 46 % 0.84/1.03 48. ((rel_str T_0) => (All B, ((ex_sup_of_relstr_set T_0 B) <=> (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 B C) /\ ((All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 B D) => (related T_0 C D)))) /\ (All D, ((element D (the_carrier T_0)) => (((relstr_set_smaller T_0 B D) /\ (All E, ((element E (the_carrier T_0)) => ((relstr_set_smaller T_0 B E) => (related T_0 D E))))) => (D = C))))))))))) (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))))))) (ex_sup_of_relstr_set T_0 T_2) (rel_str T_0) ### Imply 37 47 % 0.84/1.03 49. (All A, ((rel_str A) => (All B, ((ex_sup_of_relstr_set A B) <=> (Ex C, ((element C (the_carrier A)) /\ ((relstr_set_smaller A B C) /\ ((All D, ((element D (the_carrier A)) => ((relstr_set_smaller A B D) => (related A C D)))) /\ (All D, ((element D (the_carrier A)) => (((relstr_set_smaller A B D) /\ (All E, ((element E (the_carrier A)) => ((relstr_set_smaller A B E) => (related A D E))))) => (D = C)))))))))))) (rel_str T_0) (ex_sup_of_relstr_set T_0 T_2) (-. (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D)))))))) ### All 48 % 0.84/1.03 50. (-. ((ex_sup_of_relstr_set T_0 T_2) <=> (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 T_2 C) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 T_2 D) => (related T_0 C D))))))))) (antisymmetric_relstr T_0) (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((element B (the_carrier A)) => (All C, ((element C (the_carrier A)) => (((related A B C) /\ (related A C B)) => (B = C)))))))) (rel_str T_0) (All A, ((rel_str A) => (All B, ((ex_sup_of_relstr_set A B) <=> (Ex C, ((element C (the_carrier A)) /\ ((relstr_set_smaller A B C) /\ ((All D, ((element D (the_carrier A)) => ((relstr_set_smaller A B D) => (related A C D)))) /\ (All D, ((element D (the_carrier A)) => (((relstr_set_smaller A B D) /\ (All E, ((element E (the_carrier A)) => ((relstr_set_smaller A B E) => (related A D E))))) => (D = C)))))))))))) ### NotEquiv 36 49 % 0.84/1.03 51. (-. (All B, ((ex_sup_of_relstr_set T_0 B) <=> (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 B C) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 B D) => (related T_0 C D)))))))))) (All A, ((rel_str A) => (All B, ((ex_sup_of_relstr_set A B) <=> (Ex C, ((element C (the_carrier A)) /\ ((relstr_set_smaller A B C) /\ ((All D, ((element D (the_carrier A)) => ((relstr_set_smaller A B D) => (related A C D)))) /\ (All D, ((element D (the_carrier A)) => (((relstr_set_smaller A B D) /\ (All E, ((element E (the_carrier A)) => ((relstr_set_smaller A B E) => (related A D E))))) => (D = C)))))))))))) (rel_str T_0) (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((element B (the_carrier A)) => (All C, ((element C (the_carrier A)) => (((related A B C) /\ (related A C B)) => (B = C)))))))) (antisymmetric_relstr T_0) ### NotAllEx 50 % 0.84/1.03 52. (-. (((antisymmetric_relstr T_0) /\ (rel_str T_0)) => (All B, ((ex_sup_of_relstr_set T_0 B) <=> (Ex C, ((element C (the_carrier T_0)) /\ ((relstr_set_smaller T_0 B C) /\ (All D, ((element D (the_carrier T_0)) => ((relstr_set_smaller T_0 B D) => (related T_0 C D))))))))))) (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((element B (the_carrier A)) => (All C, ((element C (the_carrier A)) => (((related A B C) /\ (related A C B)) => (B = C)))))))) (All A, ((rel_str A) => (All B, ((ex_sup_of_relstr_set A B) <=> (Ex C, ((element C (the_carrier A)) /\ ((relstr_set_smaller A B C) /\ ((All D, ((element D (the_carrier A)) => ((relstr_set_smaller A B D) => (related A C D)))) /\ (All D, ((element D (the_carrier A)) => (((relstr_set_smaller A B D) /\ (All E, ((element E (the_carrier A)) => ((relstr_set_smaller A B E) => (related A D E))))) => (D = C)))))))))))) ### ConjTree 51 % 0.84/1.03 53. (-. (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((ex_sup_of_relstr_set A B) <=> (Ex C, ((element C (the_carrier A)) /\ ((relstr_set_smaller A B C) /\ (All D, ((element D (the_carrier A)) => ((relstr_set_smaller A B D) => (related A C D)))))))))))) (All A, ((rel_str A) => (All B, ((ex_sup_of_relstr_set A B) <=> (Ex C, ((element C (the_carrier A)) /\ ((relstr_set_smaller A B C) /\ ((All D, ((element D (the_carrier A)) => ((relstr_set_smaller A B D) => (related A C D)))) /\ (All D, ((element D (the_carrier A)) => (((relstr_set_smaller A B D) /\ (All E, ((element E (the_carrier A)) => ((relstr_set_smaller A B E) => (related A D E))))) => (D = C)))))))))))) (All A, (((antisymmetric_relstr A) /\ (rel_str A)) => (All B, ((element B (the_carrier A)) => (All C, ((element C (the_carrier A)) => (((related A B C) /\ (related A C B)) => (B = C)))))))) ### NotAllEx 52 % 0.84/1.03 % SZS output end Proof % 0.84/1.03 (* END-PROOF *) %------------------------------------------------------------------------------