%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU244+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 : n006.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:36 EDT 2022 % Result : Theorem 0.11s 0.39s % Output : Proof 0.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : SEU244+1 : TPTP v8.1.0. Released v3.3.0. % 0.10/0.11 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.11/0.32 % Computer : n006.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Mon Jun 20 10:11:25 EDT 2022 % 0.11/0.32 % CPUTime : % 0.11/0.39 % SZS status Theorem % 0.11/0.39 (* PROOF-FOUND *) % 0.11/0.39 (* BEGIN-PROOF *) % 0.11/0.39 % SZS output start Proof % 0.11/0.39 1. (relation T_0) (-. (relation T_0)) ### Axiom % 0.11/0.39 2. (well_ordering T_0) (-. (well_ordering T_0)) ### Axiom % 0.11/0.39 3. (-. (well_founded_relation T_0)) (well_founded_relation T_0) ### Axiom % 0.11/0.39 4. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0))))) (-. (well_founded_relation T_0)) ### ConjTree 3 % 0.11/0.39 5. ((well_ordering T_0) <=> ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0)))))) (-. (well_founded_relation T_0)) (well_ordering T_0) ### Equiv 2 4 % 0.11/0.39 6. ((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_0) (-. (well_founded_relation T_0)) (relation T_0) ### Imply 1 5 % 0.11/0.39 7. (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_0) (-. (well_founded_relation T_0)) (well_ordering T_0) ### All 6 % 0.11/0.39 8. (relation T_0) (-. (relation T_0)) ### Axiom % 0.11/0.39 9. (well_orders T_0 (relation_field T_0)) (-. (well_orders T_0 (relation_field T_0))) ### Axiom % 0.11/0.39 10. (-. (is_well_founded_in T_0 (relation_field T_0))) (is_well_founded_in T_0 (relation_field T_0)) ### Axiom % 0.11/0.39 11. ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0)))))) (-. (is_well_founded_in T_0 (relation_field T_0))) ### ConjTree 10 % 0.11/0.39 12. ((well_orders T_0 (relation_field T_0)) <=> ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0))))))) (-. (is_well_founded_in T_0 (relation_field T_0))) (well_orders T_0 (relation_field T_0)) ### Equiv 9 11 % 0.11/0.39 13. (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B))))))) (well_orders T_0 (relation_field T_0)) (-. (is_well_founded_in T_0 (relation_field T_0))) ### All 12 % 0.11/0.39 14. ((relation T_0) => (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B)))))))) (-. (is_well_founded_in T_0 (relation_field T_0))) (well_orders T_0 (relation_field T_0)) (relation T_0) ### Imply 8 13 % 0.11/0.39 15. (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (relation T_0) (well_orders T_0 (relation_field T_0)) (-. (is_well_founded_in T_0 (relation_field T_0))) ### All 14 % 0.11/0.39 16. (-. ((well_orders T_0 (relation_field T_0)) <=> (well_ordering T_0))) (-. (is_well_founded_in T_0 (relation_field T_0))) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (-. (well_founded_relation T_0)) (relation T_0) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) ### NotEquiv 7 15 % 0.11/0.39 17. (relation T_0) (-. (relation T_0)) ### Axiom % 0.11/0.39 18. (relation T_0) (-. (relation T_0)) ### Axiom % 0.11/0.39 19. (relation T_0) (-. (relation T_0)) ### Axiom % 0.11/0.39 20. (well_ordering T_0) (-. (well_ordering T_0)) ### Axiom % 0.11/0.39 21. (-. (reflexive T_0)) (reflexive T_0) ### Axiom % 0.11/0.39 22. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0))))) (-. (reflexive T_0)) ### ConjTree 21 % 0.11/0.39 23. ((well_ordering T_0) <=> ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0)))))) (-. (reflexive T_0)) (well_ordering T_0) ### Equiv 20 22 % 0.11/0.40 24. ((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_0) (-. (reflexive T_0)) (relation T_0) ### Imply 19 23 % 0.11/0.40 25. (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_0) (-. (reflexive T_0)) (well_ordering T_0) ### All 24 % 0.11/0.40 26. (-. (is_reflexive_in T_0 (relation_field T_0))) (is_reflexive_in T_0 (relation_field T_0)) ### Axiom % 0.11/0.40 27. ((reflexive T_0) <=> (is_reflexive_in T_0 (relation_field T_0))) (-. (is_reflexive_in T_0 (relation_field T_0))) (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)))))))) ### Equiv 25 26 % 0.11/0.40 28. ((relation T_0) => ((reflexive T_0) <=> (is_reflexive_in T_0 (relation_field T_0)))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (well_ordering T_0) (-. (is_reflexive_in T_0 (relation_field T_0))) (relation T_0) ### Imply 18 27 % 0.11/0.40 29. (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (relation T_0) (-. (is_reflexive_in T_0 (relation_field 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)))))))) ### All 28 % 0.11/0.40 30. (relation T_0) (-. (relation T_0)) ### Axiom % 0.11/0.40 31. (relation T_0) (-. (relation T_0)) ### Axiom % 0.11/0.40 32. (well_ordering T_0) (-. (well_ordering T_0)) ### Axiom % 0.11/0.40 33. (-. (transitive T_0)) (transitive T_0) ### Axiom % 0.11/0.40 34. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0))))) (-. (transitive T_0)) ### ConjTree 33 % 0.11/0.40 35. ((well_ordering T_0) <=> ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0)))))) (-. (transitive T_0)) (well_ordering T_0) ### Equiv 32 34 % 0.11/0.40 36. ((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_0) (-. (transitive T_0)) (relation T_0) ### Imply 31 35 % 0.11/0.40 37. (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_0) (-. (transitive T_0)) (well_ordering T_0) ### All 36 % 0.11/0.40 38. (-. (is_transitive_in T_0 (relation_field T_0))) (is_transitive_in T_0 (relation_field T_0)) ### Axiom % 0.11/0.40 39. ((transitive T_0) <=> (is_transitive_in T_0 (relation_field T_0))) (-. (is_transitive_in T_0 (relation_field T_0))) (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)))))))) ### Equiv 37 38 % 0.11/0.40 40. ((relation T_0) => ((transitive T_0) <=> (is_transitive_in T_0 (relation_field T_0)))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (well_ordering T_0) (-. (is_transitive_in T_0 (relation_field T_0))) (relation T_0) ### Imply 30 39 % 0.11/0.40 41. (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (relation T_0) (-. (is_transitive_in T_0 (relation_field 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)))))))) ### All 40 % 0.11/0.40 42. (relation T_0) (-. (relation T_0)) ### Axiom % 0.11/0.40 43. (relation T_0) (-. (relation T_0)) ### Axiom % 0.11/0.40 44. (well_ordering T_0) (-. (well_ordering T_0)) ### Axiom % 0.11/0.40 45. (-. (antisymmetric T_0)) (antisymmetric T_0) ### Axiom % 0.11/0.40 46. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0))))) (-. (antisymmetric T_0)) ### ConjTree 45 % 0.11/0.40 47. ((well_ordering T_0) <=> ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0)))))) (-. (antisymmetric T_0)) (well_ordering T_0) ### Equiv 44 46 % 0.11/0.40 48. ((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_0) (-. (antisymmetric T_0)) (relation T_0) ### Imply 43 47 % 0.11/0.40 49. (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_0) (-. (antisymmetric T_0)) (well_ordering T_0) ### All 48 % 0.11/0.40 50. (-. (is_antisymmetric_in T_0 (relation_field T_0))) (is_antisymmetric_in T_0 (relation_field T_0)) ### Axiom % 0.11/0.40 51. ((antisymmetric T_0) <=> (is_antisymmetric_in T_0 (relation_field T_0))) (-. (is_antisymmetric_in T_0 (relation_field T_0))) (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)))))))) ### Equiv 49 50 % 0.11/0.40 52. ((relation T_0) => ((antisymmetric T_0) <=> (is_antisymmetric_in T_0 (relation_field T_0)))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (well_ordering T_0) (-. (is_antisymmetric_in T_0 (relation_field T_0))) (relation T_0) ### Imply 42 51 % 0.11/0.40 53. (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (relation T_0) (-. (is_antisymmetric_in T_0 (relation_field 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)))))))) ### All 52 % 0.11/0.40 54. (relation T_0) (-. (relation T_0)) ### Axiom % 0.11/0.40 55. (relation T_0) (-. (relation T_0)) ### Axiom % 0.11/0.40 56. (well_ordering T_0) (-. (well_ordering T_0)) ### Axiom % 0.11/0.40 57. (-. (connected T_0)) (connected T_0) ### Axiom % 0.11/0.40 58. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0))))) (-. (connected T_0)) ### ConjTree 57 % 0.11/0.40 59. ((well_ordering T_0) <=> ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0)))))) (-. (connected T_0)) (well_ordering T_0) ### Equiv 56 58 % 0.11/0.40 60. ((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_0) (-. (connected T_0)) (relation T_0) ### Imply 55 59 % 0.11/0.40 61. (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_0) (-. (connected T_0)) (well_ordering T_0) ### All 60 % 0.11/0.40 62. (-. (is_connected_in T_0 (relation_field T_0))) (is_connected_in T_0 (relation_field T_0)) ### Axiom % 0.11/0.40 63. ((connected T_0) <=> (is_connected_in T_0 (relation_field T_0))) (-. (is_connected_in T_0 (relation_field T_0))) (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)))))))) ### Equiv 61 62 % 0.11/0.40 64. ((relation T_0) => ((connected T_0) <=> (is_connected_in T_0 (relation_field T_0)))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (well_ordering T_0) (-. (is_connected_in T_0 (relation_field T_0))) (relation T_0) ### Imply 54 63 % 0.11/0.40 65. (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (relation T_0) (-. (is_connected_in T_0 (relation_field 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)))))))) ### All 64 % 0.11/0.40 66. (is_well_founded_in T_0 (relation_field T_0)) (-. (is_well_founded_in T_0 (relation_field T_0))) ### Axiom % 0.11/0.40 67. (-. ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0))))))) (is_well_founded_in T_0 (relation_field T_0)) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (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) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) ### DisjTree 29 41 53 65 66 % 0.11/0.40 68. (-. (well_orders T_0 (relation_field T_0))) (well_orders T_0 (relation_field T_0)) ### Axiom % 0.11/0.40 69. ((well_orders T_0 (relation_field T_0)) <=> ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0))))))) (-. (well_orders T_0 (relation_field T_0))) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (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)))))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (is_well_founded_in T_0 (relation_field T_0)) ### Equiv 67 68 % 0.11/0.40 70. (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B))))))) (is_well_founded_in T_0 (relation_field T_0)) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (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) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (-. (well_orders T_0 (relation_field T_0))) ### All 69 % 0.11/0.40 71. ((relation T_0) => (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B)))))))) (-. (well_orders T_0 (relation_field T_0))) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (well_ordering T_0) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (is_well_founded_in T_0 (relation_field T_0)) (relation T_0) ### Imply 17 70 % 0.11/0.40 72. (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (relation T_0) (is_well_founded_in T_0 (relation_field T_0)) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (well_ordering T_0) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (-. (well_orders T_0 (relation_field T_0))) ### All 71 % 0.17/0.41 73. (relation T_0) (-. (relation T_0)) ### Axiom % 0.17/0.41 74. (relation T_0) (-. (relation T_0)) ### Axiom % 0.17/0.41 75. (relation T_0) (-. (relation T_0)) ### Axiom % 0.17/0.41 76. (well_orders T_0 (relation_field T_0)) (-. (well_orders T_0 (relation_field T_0))) ### Axiom % 0.17/0.41 77. (-. (is_reflexive_in T_0 (relation_field T_0))) (is_reflexive_in T_0 (relation_field T_0)) ### Axiom % 0.17/0.41 78. ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0)))))) (-. (is_reflexive_in T_0 (relation_field T_0))) ### ConjTree 77 % 0.17/0.41 79. ((well_orders T_0 (relation_field T_0)) <=> ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0))))))) (-. (is_reflexive_in T_0 (relation_field T_0))) (well_orders T_0 (relation_field T_0)) ### Equiv 76 78 % 0.17/0.41 80. (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B))))))) (well_orders T_0 (relation_field T_0)) (-. (is_reflexive_in T_0 (relation_field T_0))) ### All 79 % 0.17/0.41 81. ((relation T_0) => (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B)))))))) (-. (is_reflexive_in T_0 (relation_field T_0))) (well_orders T_0 (relation_field T_0)) (relation T_0) ### Imply 75 80 % 0.17/0.41 82. (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (relation T_0) (well_orders T_0 (relation_field T_0)) (-. (is_reflexive_in T_0 (relation_field T_0))) ### All 81 % 0.17/0.41 83. (-. (reflexive T_0)) (reflexive T_0) ### Axiom % 0.17/0.41 84. ((reflexive T_0) <=> (is_reflexive_in T_0 (relation_field T_0))) (-. (reflexive T_0)) (well_orders T_0 (relation_field T_0)) (relation T_0) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) ### Equiv 82 83 % 0.17/0.41 85. ((relation T_0) => ((reflexive T_0) <=> (is_reflexive_in T_0 (relation_field T_0)))) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (well_orders T_0 (relation_field T_0)) (-. (reflexive T_0)) (relation T_0) ### Imply 74 84 % 0.17/0.41 86. (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (relation T_0) (-. (reflexive T_0)) (well_orders T_0 (relation_field T_0)) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) ### All 85 % 0.17/0.41 87. (relation T_0) (-. (relation T_0)) ### Axiom % 0.17/0.41 88. (relation T_0) (-. (relation T_0)) ### Axiom % 0.17/0.41 89. (well_orders T_0 (relation_field T_0)) (-. (well_orders T_0 (relation_field T_0))) ### Axiom % 0.17/0.41 90. (-. (is_transitive_in T_0 (relation_field T_0))) (is_transitive_in T_0 (relation_field T_0)) ### Axiom % 0.17/0.41 91. ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0)))))) (-. (is_transitive_in T_0 (relation_field T_0))) ### ConjTree 90 % 0.17/0.41 92. ((well_orders T_0 (relation_field T_0)) <=> ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0))))))) (-. (is_transitive_in T_0 (relation_field T_0))) (well_orders T_0 (relation_field T_0)) ### Equiv 89 91 % 0.17/0.41 93. (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B))))))) (well_orders T_0 (relation_field T_0)) (-. (is_transitive_in T_0 (relation_field T_0))) ### All 92 % 0.17/0.41 94. ((relation T_0) => (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B)))))))) (-. (is_transitive_in T_0 (relation_field T_0))) (well_orders T_0 (relation_field T_0)) (relation T_0) ### Imply 88 93 % 0.17/0.41 95. (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (relation T_0) (well_orders T_0 (relation_field T_0)) (-. (is_transitive_in T_0 (relation_field T_0))) ### All 94 % 0.17/0.41 96. (-. (transitive T_0)) (transitive T_0) ### Axiom % 0.17/0.41 97. ((transitive T_0) <=> (is_transitive_in T_0 (relation_field T_0))) (-. (transitive T_0)) (well_orders T_0 (relation_field T_0)) (relation T_0) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) ### Equiv 95 96 % 0.17/0.41 98. ((relation T_0) => ((transitive T_0) <=> (is_transitive_in T_0 (relation_field T_0)))) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (well_orders T_0 (relation_field T_0)) (-. (transitive T_0)) (relation T_0) ### Imply 87 97 % 0.17/0.41 99. (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (relation T_0) (-. (transitive T_0)) (well_orders T_0 (relation_field T_0)) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) ### All 98 % 0.17/0.41 100. (relation T_0) (-. (relation T_0)) ### Axiom % 0.17/0.41 101. (relation T_0) (-. (relation T_0)) ### Axiom % 0.17/0.41 102. (well_orders T_0 (relation_field T_0)) (-. (well_orders T_0 (relation_field T_0))) ### Axiom % 0.17/0.41 103. (-. (is_antisymmetric_in T_0 (relation_field T_0))) (is_antisymmetric_in T_0 (relation_field T_0)) ### Axiom % 0.17/0.41 104. ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0)))))) (-. (is_antisymmetric_in T_0 (relation_field T_0))) ### ConjTree 103 % 0.17/0.41 105. ((well_orders T_0 (relation_field T_0)) <=> ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0))))))) (-. (is_antisymmetric_in T_0 (relation_field T_0))) (well_orders T_0 (relation_field T_0)) ### Equiv 102 104 % 0.17/0.41 106. (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B))))))) (well_orders T_0 (relation_field T_0)) (-. (is_antisymmetric_in T_0 (relation_field T_0))) ### All 105 % 0.17/0.41 107. ((relation T_0) => (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B)))))))) (-. (is_antisymmetric_in T_0 (relation_field T_0))) (well_orders T_0 (relation_field T_0)) (relation T_0) ### Imply 101 106 % 0.17/0.41 108. (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (relation T_0) (well_orders T_0 (relation_field T_0)) (-. (is_antisymmetric_in T_0 (relation_field T_0))) ### All 107 % 0.17/0.41 109. (-. (antisymmetric T_0)) (antisymmetric T_0) ### Axiom % 0.17/0.41 110. ((antisymmetric T_0) <=> (is_antisymmetric_in T_0 (relation_field T_0))) (-. (antisymmetric T_0)) (well_orders T_0 (relation_field T_0)) (relation T_0) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) ### Equiv 108 109 % 0.17/0.41 111. ((relation T_0) => ((antisymmetric T_0) <=> (is_antisymmetric_in T_0 (relation_field T_0)))) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (well_orders T_0 (relation_field T_0)) (-. (antisymmetric T_0)) (relation T_0) ### Imply 100 110 % 0.17/0.41 112. (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (relation T_0) (-. (antisymmetric T_0)) (well_orders T_0 (relation_field T_0)) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) ### All 111 % 0.17/0.41 113. (relation T_0) (-. (relation T_0)) ### Axiom % 0.17/0.41 114. (relation T_0) (-. (relation T_0)) ### Axiom % 0.17/0.41 115. (well_orders T_0 (relation_field T_0)) (-. (well_orders T_0 (relation_field T_0))) ### Axiom % 0.17/0.41 116. (-. (is_connected_in T_0 (relation_field T_0))) (is_connected_in T_0 (relation_field T_0)) ### Axiom % 0.17/0.41 117. ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0)))))) (-. (is_connected_in T_0 (relation_field T_0))) ### ConjTree 116 % 0.17/0.41 118. ((well_orders T_0 (relation_field T_0)) <=> ((is_reflexive_in T_0 (relation_field T_0)) /\ ((is_transitive_in T_0 (relation_field T_0)) /\ ((is_antisymmetric_in T_0 (relation_field T_0)) /\ ((is_connected_in T_0 (relation_field T_0)) /\ (is_well_founded_in T_0 (relation_field T_0))))))) (-. (is_connected_in T_0 (relation_field T_0))) (well_orders T_0 (relation_field T_0)) ### Equiv 115 117 % 0.17/0.41 119. (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B))))))) (well_orders T_0 (relation_field T_0)) (-. (is_connected_in T_0 (relation_field T_0))) ### All 118 % 0.17/0.41 120. ((relation T_0) => (All B, ((well_orders T_0 B) <=> ((is_reflexive_in T_0 B) /\ ((is_transitive_in T_0 B) /\ ((is_antisymmetric_in T_0 B) /\ ((is_connected_in T_0 B) /\ (is_well_founded_in T_0 B)))))))) (-. (is_connected_in T_0 (relation_field T_0))) (well_orders T_0 (relation_field T_0)) (relation T_0) ### Imply 114 119 % 0.17/0.41 121. (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (relation T_0) (well_orders T_0 (relation_field T_0)) (-. (is_connected_in T_0 (relation_field T_0))) ### All 120 % 0.17/0.41 122. (-. (connected T_0)) (connected T_0) ### Axiom % 0.17/0.41 123. ((connected T_0) <=> (is_connected_in T_0 (relation_field T_0))) (-. (connected T_0)) (well_orders T_0 (relation_field T_0)) (relation T_0) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) ### Equiv 121 122 % 0.17/0.41 124. ((relation T_0) => ((connected T_0) <=> (is_connected_in T_0 (relation_field T_0)))) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (well_orders T_0 (relation_field T_0)) (-. (connected T_0)) (relation T_0) ### Imply 113 123 % 0.17/0.41 125. (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (relation T_0) (-. (connected T_0)) (well_orders T_0 (relation_field T_0)) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) ### All 124 % 0.17/0.41 126. (well_founded_relation T_0) (-. (well_founded_relation T_0)) ### Axiom % 0.17/0.41 127. (-. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0)))))) (well_founded_relation T_0) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (well_orders T_0 (relation_field T_0)) (relation T_0) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) ### DisjTree 86 99 112 125 126 % 0.17/0.41 128. (-. (well_ordering T_0)) (well_ordering T_0) ### Axiom % 0.17/0.41 129. ((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) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (relation T_0) (well_orders T_0 (relation_field T_0)) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (well_founded_relation T_0) ### Equiv 127 128 % 0.17/0.41 130. ((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_founded_relation T_0) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (well_orders T_0 (relation_field T_0)) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (-. (well_ordering T_0)) (relation T_0) ### Imply 73 129 % 0.17/0.41 131. (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_0) (-. (well_ordering T_0)) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (well_orders T_0 (relation_field T_0)) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (well_founded_relation T_0) ### All 130 % 0.17/0.41 132. (-. ((well_orders T_0 (relation_field T_0)) <=> (well_ordering T_0))) (well_founded_relation T_0) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (is_well_founded_in T_0 (relation_field T_0)) (relation T_0) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) ### NotEquiv 72 131 % 0.17/0.41 133. (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (relation T_0) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (-. ((well_orders T_0 (relation_field T_0)) <=> (well_ordering T_0))) ### Extension/test/t5_wellord1 16 132 % 0.17/0.41 134. (-. ((relation T_0) => ((well_orders T_0 (relation_field T_0)) <=> (well_ordering T_0)))) (All A, ((relation A) => (All B, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) ### NotImply 133 % 0.17/0.41 135. (-. (All A, ((relation A) => ((well_orders A (relation_field A)) <=> (well_ordering A))))) (All A, ((relation A) => ((connected A) <=> (is_connected_in A (relation_field A))))) (All A, ((relation A) => ((antisymmetric A) <=> (is_antisymmetric_in A (relation_field A))))) (All A, ((relation A) => ((transitive A) <=> (is_transitive_in A (relation_field A))))) (All A, ((relation A) => ((reflexive A) <=> (is_reflexive_in A (relation_field A))))) (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, ((well_orders A B) <=> ((is_reflexive_in A B) /\ ((is_transitive_in A B) /\ ((is_antisymmetric_in A B) /\ ((is_connected_in A B) /\ (is_well_founded_in A B))))))))) ### NotAllEx 134 % 0.17/0.41 % SZS output end Proof % 0.17/0.41 (* END-PROOF *) %------------------------------------------------------------------------------