%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU261+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 : n014.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:49:44 EDT 2022 % Result : Theorem 0.18s 0.41s % Output : Proof 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SEU261+1 : TPTP v8.1.0. Released v3.3.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n014.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 : Sun Jun 19 16:13:03 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.41 % SZS status Theorem % 0.18/0.41 (* PROOF-FOUND *) % 0.18/0.41 (* BEGIN-PROOF *) % 0.18/0.41 % SZS output start Proof % 0.18/0.41 1. (relation T_0) (-. (relation T_0)) ### Axiom % 0.18/0.41 2. (relation T_1) (-. (relation T_1)) ### Axiom % 0.18/0.41 3. (well_ordering T_1) (-. (well_ordering T_1)) ### Axiom % 0.18/0.41 4. (relation T_1) (-. (relation T_1)) ### Axiom % 0.18/0.41 5. (relation T_0) (-. (relation T_0)) ### Axiom % 0.18/0.41 6. (relation T_2) (-. (relation T_2)) ### Axiom % 0.18/0.41 7. (function T_2) (-. (function T_2)) ### Axiom % 0.18/0.41 8. (relation_isomorphism T_1 T_0 T_2) (-. (relation_isomorphism T_1 T_0 T_2)) ### Axiom % 0.18/0.41 9. (reflexive T_1) (-. (reflexive T_1)) ### Axiom % 0.18/0.41 10. (-. (reflexive T_0)) (reflexive T_0) ### Axiom % 0.18/0.41 11. ((reflexive T_1) => (reflexive T_0)) (-. (reflexive T_0)) (reflexive T_1) ### Imply 9 10 % 0.18/0.41 12. (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))) (reflexive T_1) (-. (reflexive T_0)) ### ConjTree 11 % 0.18/0.41 13. (((relation T_2) /\ (function T_2)) => ((relation_isomorphism T_1 T_0 T_2) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))))) (-. (reflexive T_0)) (reflexive T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) ### DisjTree 6 7 8 12 % 0.18/0.41 14. (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 T_0 C) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0))))))))) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (reflexive T_1) (-. (reflexive T_0)) ### All 13 % 0.18/0.41 15. ((relation T_0) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 T_0 C) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))))))) (-. (reflexive T_0)) (reflexive T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) ### Imply 5 14 % 0.18/0.41 16. (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 B C) => (((reflexive T_1) => (reflexive B)) /\ (((transitive T_1) => (transitive B)) /\ (((connected T_1) => (connected B)) /\ (((antisymmetric T_1) => (antisymmetric B)) /\ ((well_founded_relation T_1) => (well_founded_relation B))))))))))) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (reflexive T_1) (-. (reflexive T_0)) ### All 15 % 0.18/0.41 17. ((relation T_1) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 B C) => (((reflexive T_1) => (reflexive B)) /\ (((transitive T_1) => (transitive B)) /\ (((connected T_1) => (connected B)) /\ (((antisymmetric T_1) => (antisymmetric B)) /\ ((well_founded_relation T_1) => (well_founded_relation B)))))))))))) (-. (reflexive T_0)) (reflexive T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (relation T_1) ### Imply 4 16 % 0.18/0.41 18. (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (reflexive T_1) (-. (reflexive T_0)) ### All 17 % 0.18/0.41 19. ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1))))) (-. (reflexive T_0)) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) ### ConjTree 18 % 0.18/0.41 20. ((well_ordering T_1) <=> ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1)))))) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (-. (reflexive T_0)) (well_ordering T_1) ### Equiv 3 19 % 0.18/0.41 21. ((relation T_1) => ((well_ordering T_1) <=> ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1))))))) (well_ordering T_1) (-. (reflexive T_0)) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) ### Imply 2 20 % 0.18/0.41 22. (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (-. (reflexive T_0)) (well_ordering T_1) ### All 21 % 0.18/0.41 23. (relation T_1) (-. (relation T_1)) ### Axiom % 0.18/0.41 24. (well_ordering T_1) (-. (well_ordering T_1)) ### Axiom % 0.18/0.41 25. (relation T_1) (-. (relation T_1)) ### Axiom % 0.18/0.41 26. (relation T_0) (-. (relation T_0)) ### Axiom % 0.18/0.41 27. (relation T_2) (-. (relation T_2)) ### Axiom % 0.18/0.41 28. (function T_2) (-. (function T_2)) ### Axiom % 0.18/0.41 29. (relation_isomorphism T_1 T_0 T_2) (-. (relation_isomorphism T_1 T_0 T_2)) ### Axiom % 0.18/0.41 30. (transitive T_1) (-. (transitive T_1)) ### Axiom % 0.18/0.41 31. (-. (transitive T_0)) (transitive T_0) ### Axiom % 0.18/0.41 32. ((transitive T_1) => (transitive T_0)) (-. (transitive T_0)) (transitive T_1) ### Imply 30 31 % 0.18/0.41 33. (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))) (transitive T_1) (-. (transitive T_0)) ### ConjTree 32 % 0.18/0.41 34. (((relation T_2) /\ (function T_2)) => ((relation_isomorphism T_1 T_0 T_2) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))))) (-. (transitive T_0)) (transitive T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) ### DisjTree 27 28 29 33 % 0.18/0.41 35. (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 T_0 C) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0))))))))) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (transitive T_1) (-. (transitive T_0)) ### All 34 % 0.18/0.42 36. ((relation T_0) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 T_0 C) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))))))) (-. (transitive T_0)) (transitive T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) ### Imply 26 35 % 0.18/0.42 37. (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 B C) => (((reflexive T_1) => (reflexive B)) /\ (((transitive T_1) => (transitive B)) /\ (((connected T_1) => (connected B)) /\ (((antisymmetric T_1) => (antisymmetric B)) /\ ((well_founded_relation T_1) => (well_founded_relation B))))))))))) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (transitive T_1) (-. (transitive T_0)) ### All 36 % 0.18/0.42 38. ((relation T_1) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 B C) => (((reflexive T_1) => (reflexive B)) /\ (((transitive T_1) => (transitive B)) /\ (((connected T_1) => (connected B)) /\ (((antisymmetric T_1) => (antisymmetric B)) /\ ((well_founded_relation T_1) => (well_founded_relation B)))))))))))) (-. (transitive T_0)) (transitive T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (relation T_1) ### Imply 25 37 % 0.18/0.42 39. (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (transitive T_1) (-. (transitive T_0)) ### All 38 % 0.18/0.42 40. ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1))))) (-. (transitive T_0)) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) ### ConjTree 39 % 0.18/0.42 41. ((well_ordering T_1) <=> ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1)))))) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (-. (transitive T_0)) (well_ordering T_1) ### Equiv 24 40 % 0.18/0.42 42. ((relation T_1) => ((well_ordering T_1) <=> ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1))))))) (well_ordering T_1) (-. (transitive T_0)) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) ### Imply 23 41 % 0.18/0.42 43. (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (-. (transitive T_0)) (well_ordering T_1) ### All 42 % 0.18/0.42 44. (relation T_1) (-. (relation T_1)) ### Axiom % 0.18/0.42 45. (well_ordering T_1) (-. (well_ordering T_1)) ### Axiom % 0.18/0.42 46. (relation T_1) (-. (relation T_1)) ### Axiom % 0.18/0.42 47. (relation T_0) (-. (relation T_0)) ### Axiom % 0.18/0.42 48. (relation T_2) (-. (relation T_2)) ### Axiom % 0.18/0.42 49. (function T_2) (-. (function T_2)) ### Axiom % 0.18/0.42 50. (relation_isomorphism T_1 T_0 T_2) (-. (relation_isomorphism T_1 T_0 T_2)) ### Axiom % 0.18/0.42 51. (antisymmetric T_1) (-. (antisymmetric T_1)) ### Axiom % 0.18/0.42 52. (-. (antisymmetric T_0)) (antisymmetric T_0) ### Axiom % 0.18/0.42 53. ((antisymmetric T_1) => (antisymmetric T_0)) (-. (antisymmetric T_0)) (antisymmetric T_1) ### Imply 51 52 % 0.18/0.42 54. (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))) (antisymmetric T_1) (-. (antisymmetric T_0)) ### ConjTree 53 % 0.18/0.42 55. (((relation T_2) /\ (function T_2)) => ((relation_isomorphism T_1 T_0 T_2) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))))) (-. (antisymmetric T_0)) (antisymmetric T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) ### DisjTree 48 49 50 54 % 0.18/0.42 56. (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 T_0 C) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0))))))))) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (antisymmetric T_1) (-. (antisymmetric T_0)) ### All 55 % 0.18/0.42 57. ((relation T_0) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 T_0 C) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))))))) (-. (antisymmetric T_0)) (antisymmetric T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) ### Imply 47 56 % 0.18/0.42 58. (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 B C) => (((reflexive T_1) => (reflexive B)) /\ (((transitive T_1) => (transitive B)) /\ (((connected T_1) => (connected B)) /\ (((antisymmetric T_1) => (antisymmetric B)) /\ ((well_founded_relation T_1) => (well_founded_relation B))))))))))) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (antisymmetric T_1) (-. (antisymmetric T_0)) ### All 57 % 0.18/0.42 59. ((relation T_1) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 B C) => (((reflexive T_1) => (reflexive B)) /\ (((transitive T_1) => (transitive B)) /\ (((connected T_1) => (connected B)) /\ (((antisymmetric T_1) => (antisymmetric B)) /\ ((well_founded_relation T_1) => (well_founded_relation B)))))))))))) (-. (antisymmetric T_0)) (antisymmetric T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (relation T_1) ### Imply 46 58 % 0.18/0.42 60. (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (antisymmetric T_1) (-. (antisymmetric T_0)) ### All 59 % 0.18/0.43 61. ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1))))) (-. (antisymmetric T_0)) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) ### ConjTree 60 % 0.18/0.43 62. ((well_ordering T_1) <=> ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1)))))) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (-. (antisymmetric T_0)) (well_ordering T_1) ### Equiv 45 61 % 0.18/0.43 63. ((relation T_1) => ((well_ordering T_1) <=> ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1))))))) (well_ordering T_1) (-. (antisymmetric T_0)) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) ### Imply 44 62 % 0.18/0.43 64. (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (-. (antisymmetric T_0)) (well_ordering T_1) ### All 63 % 0.18/0.43 65. (relation T_1) (-. (relation T_1)) ### Axiom % 0.18/0.43 66. (well_ordering T_1) (-. (well_ordering T_1)) ### Axiom % 0.18/0.43 67. (relation T_1) (-. (relation T_1)) ### Axiom % 0.18/0.43 68. (relation T_0) (-. (relation T_0)) ### Axiom % 0.18/0.43 69. (relation T_2) (-. (relation T_2)) ### Axiom % 0.18/0.43 70. (function T_2) (-. (function T_2)) ### Axiom % 0.18/0.43 71. (relation_isomorphism T_1 T_0 T_2) (-. (relation_isomorphism T_1 T_0 T_2)) ### Axiom % 0.18/0.43 72. (connected T_1) (-. (connected T_1)) ### Axiom % 0.18/0.43 73. (-. (connected T_0)) (connected T_0) ### Axiom % 0.18/0.43 74. ((connected T_1) => (connected T_0)) (-. (connected T_0)) (connected T_1) ### Imply 72 73 % 0.18/0.43 75. (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))) (connected T_1) (-. (connected T_0)) ### ConjTree 74 % 0.18/0.43 76. (((relation T_2) /\ (function T_2)) => ((relation_isomorphism T_1 T_0 T_2) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))))) (-. (connected T_0)) (connected T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) ### DisjTree 69 70 71 75 % 0.18/0.43 77. (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 T_0 C) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0))))))))) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (connected T_1) (-. (connected T_0)) ### All 76 % 0.18/0.43 78. ((relation T_0) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 T_0 C) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))))))) (-. (connected T_0)) (connected T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) ### Imply 68 77 % 0.18/0.43 79. (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 B C) => (((reflexive T_1) => (reflexive B)) /\ (((transitive T_1) => (transitive B)) /\ (((connected T_1) => (connected B)) /\ (((antisymmetric T_1) => (antisymmetric B)) /\ ((well_founded_relation T_1) => (well_founded_relation B))))))))))) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (connected T_1) (-. (connected T_0)) ### All 78 % 0.18/0.43 80. ((relation T_1) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 B C) => (((reflexive T_1) => (reflexive B)) /\ (((transitive T_1) => (transitive B)) /\ (((connected T_1) => (connected B)) /\ (((antisymmetric T_1) => (antisymmetric B)) /\ ((well_founded_relation T_1) => (well_founded_relation B)))))))))))) (-. (connected T_0)) (connected T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (relation T_1) ### Imply 67 79 % 0.18/0.43 81. (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (connected T_1) (-. (connected T_0)) ### All 80 % 0.18/0.43 82. ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1))))) (-. (connected T_0)) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) ### ConjTree 81 % 0.18/0.43 83. ((well_ordering T_1) <=> ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1)))))) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (-. (connected T_0)) (well_ordering T_1) ### Equiv 66 82 % 0.18/0.43 84. ((relation T_1) => ((well_ordering T_1) <=> ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1))))))) (well_ordering T_1) (-. (connected T_0)) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) ### Imply 65 83 % 0.18/0.44 85. (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (-. (connected T_0)) (well_ordering T_1) ### All 84 % 0.18/0.44 86. (relation T_1) (-. (relation T_1)) ### Axiom % 0.18/0.44 87. (well_ordering T_1) (-. (well_ordering T_1)) ### Axiom % 0.18/0.44 88. (relation T_1) (-. (relation T_1)) ### Axiom % 0.18/0.44 89. (relation T_0) (-. (relation T_0)) ### Axiom % 0.18/0.44 90. (relation T_2) (-. (relation T_2)) ### Axiom % 0.18/0.44 91. (function T_2) (-. (function T_2)) ### Axiom % 0.18/0.44 92. (relation_isomorphism T_1 T_0 T_2) (-. (relation_isomorphism T_1 T_0 T_2)) ### Axiom % 0.18/0.44 93. (well_founded_relation T_1) (-. (well_founded_relation T_1)) ### Axiom % 0.18/0.44 94. (-. (well_founded_relation T_0)) (well_founded_relation T_0) ### Axiom % 0.18/0.44 95. ((well_founded_relation T_1) => (well_founded_relation T_0)) (-. (well_founded_relation T_0)) (well_founded_relation T_1) ### Imply 93 94 % 0.18/0.44 96. (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))) (well_founded_relation T_1) (-. (well_founded_relation T_0)) ### ConjTree 95 % 0.18/0.44 97. (((relation T_2) /\ (function T_2)) => ((relation_isomorphism T_1 T_0 T_2) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))))) (-. (well_founded_relation T_0)) (well_founded_relation T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) ### DisjTree 90 91 92 96 % 0.18/0.44 98. (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 T_0 C) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0))))))))) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (well_founded_relation T_1) (-. (well_founded_relation T_0)) ### All 97 % 0.18/0.44 99. ((relation T_0) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 T_0 C) => (((reflexive T_1) => (reflexive T_0)) /\ (((transitive T_1) => (transitive T_0)) /\ (((connected T_1) => (connected T_0)) /\ (((antisymmetric T_1) => (antisymmetric T_0)) /\ ((well_founded_relation T_1) => (well_founded_relation T_0)))))))))) (-. (well_founded_relation T_0)) (well_founded_relation T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) ### Imply 89 98 % 0.18/0.44 100. (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 B C) => (((reflexive T_1) => (reflexive B)) /\ (((transitive T_1) => (transitive B)) /\ (((connected T_1) => (connected B)) /\ (((antisymmetric T_1) => (antisymmetric B)) /\ ((well_founded_relation T_1) => (well_founded_relation B))))))))))) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (well_founded_relation T_1) (-. (well_founded_relation T_0)) ### All 99 % 0.18/0.44 101. ((relation T_1) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism T_1 B C) => (((reflexive T_1) => (reflexive B)) /\ (((transitive T_1) => (transitive B)) /\ (((connected T_1) => (connected B)) /\ (((antisymmetric T_1) => (antisymmetric B)) /\ ((well_founded_relation T_1) => (well_founded_relation B)))))))))))) (-. (well_founded_relation T_0)) (well_founded_relation T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (relation T_1) ### Imply 88 100 % 0.18/0.44 102. (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (well_founded_relation T_1) (-. (well_founded_relation T_0)) ### All 101 % 0.18/0.44 103. ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1))))) (-. (well_founded_relation T_0)) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) ### ConjTree 102 % 0.18/0.44 104. ((well_ordering T_1) <=> ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1)))))) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (-. (well_founded_relation T_0)) (well_ordering T_1) ### Equiv 87 103 % 0.18/0.44 105. ((relation T_1) => ((well_ordering T_1) <=> ((reflexive T_1) /\ ((transitive T_1) /\ ((antisymmetric T_1) /\ ((connected T_1) /\ (well_founded_relation T_1))))))) (well_ordering T_1) (-. (well_founded_relation T_0)) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) ### Imply 86 104 % 0.18/0.44 106. (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (-. (well_founded_relation T_0)) (well_ordering T_1) ### All 105 % 0.18/0.44 107. (-. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0)))))) (well_ordering T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (relation T_0) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) ### DisjTree 22 43 64 85 106 % 0.18/0.44 108. (-. (well_ordering T_0)) (well_ordering T_0) ### Axiom % 0.18/0.44 109. ((well_ordering T_0) <=> ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0)))))) (-. (well_ordering T_0)) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_0) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (well_ordering T_1) ### Equiv 107 108 % 0.18/0.44 110. ((relation T_0) => ((well_ordering T_0) <=> ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0))))))) (well_ordering T_1) (relation_isomorphism T_1 T_0 T_2) (function T_2) (relation T_2) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (-. (well_ordering T_0)) (relation T_0) ### Imply 1 109 % 0.18/0.44 111. (relation T_0) (-. (well_ordering T_0)) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_2) (function T_2) (relation_isomorphism T_1 T_0 T_2) (well_ordering T_1) ### All 110 % 0.18/0.44 112. (-. (((relation T_2) /\ (function T_2)) => (((well_ordering T_1) /\ (relation_isomorphism T_1 T_0 T_2)) => (well_ordering T_0)))) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_0) ### ConjTree 111 % 0.18/0.44 113. (-. (All C, (((relation C) /\ (function C)) => (((well_ordering T_1) /\ (relation_isomorphism T_1 T_0 C)) => (well_ordering T_0))))) (relation T_0) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) ### NotAllEx 112 % 0.18/0.44 114. (-. ((relation T_0) => (All C, (((relation C) /\ (function C)) => (((well_ordering T_1) /\ (relation_isomorphism T_1 T_0 C)) => (well_ordering T_0)))))) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (relation T_1) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) ### NotImply 113 % 0.18/0.44 115. (-. (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => (((well_ordering T_1) /\ (relation_isomorphism T_1 B C)) => (well_ordering B))))))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_1) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) ### NotAllEx 114 % 0.18/0.44 116. (-. ((relation T_1) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => (((well_ordering T_1) /\ (relation_isomorphism T_1 B C)) => (well_ordering B)))))))) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) ### NotImply 115 % 0.18/0.44 117. (-. (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => (((well_ordering A) /\ (relation_isomorphism A B C)) => (well_ordering B))))))))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (All A, ((relation A) => (All B, ((relation B) => (All C, (((relation C) /\ (function C)) => ((relation_isomorphism A B C) => (((reflexive A) => (reflexive B)) /\ (((transitive A) => (transitive B)) /\ (((connected A) => (connected B)) /\ (((antisymmetric A) => (antisymmetric B)) /\ ((well_founded_relation A) => (well_founded_relation B))))))))))))) ### NotAllEx 116 % 0.18/0.44 % SZS output end Proof % 0.18/0.44 (* END-PROOF *) %------------------------------------------------------------------------------