%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU257+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 : n007.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:42 EDT 2022 % Result : Theorem 0.22s 0.44s % Output : Proof 0.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SEU257+1 : TPTP v8.1.0. Released v3.3.0. % 0.07/0.14 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.35 % Computer : n007.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 600 % 0.13/0.36 % DateTime : Mon Jun 20 04:19:59 EDT 2022 % 0.13/0.36 % CPUTime : % 0.22/0.44 % SZS status Theorem % 0.22/0.44 (* PROOF-FOUND *) % 0.22/0.44 (* BEGIN-PROOF *) % 0.22/0.44 % SZS output start Proof % 0.22/0.44 1. (relation T_0) (-. (relation T_0)) ### Axiom % 0.22/0.44 2. (-. (relation (relation_restriction T_0 T_1))) (relation T_0) ### Extension/test/dt_k2_wellord1ctrp 1 % 0.22/0.44 3. (relation T_0) (-. (relation T_0)) ### Axiom % 0.22/0.44 4. (relation T_0) (-. (relation T_0)) ### Axiom % 0.22/0.44 5. (well_ordering T_0) (-. (well_ordering T_0)) ### Axiom % 0.22/0.44 6. (-. (reflexive T_0)) (reflexive T_0) ### Axiom % 0.22/0.44 7. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0))))) (-. (reflexive T_0)) ### ConjTree 6 % 0.22/0.44 8. ((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 5 7 % 0.22/0.44 9. ((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 4 8 % 0.22/0.44 10. (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 9 % 0.22/0.44 11. (-. (reflexive (relation_restriction T_0 T_1))) (reflexive (relation_restriction T_0 T_1)) ### Axiom % 0.22/0.44 12. ((relation T_0) => ((reflexive T_0) => (reflexive (relation_restriction T_0 T_1)))) (-. (reflexive (relation_restriction T_0 T_1))) (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_0) ### DisjTree 3 10 11 % 0.22/0.44 13. (All B, ((relation B) => ((reflexive B) => (reflexive (relation_restriction B T_1))))) (relation 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) (-. (reflexive (relation_restriction T_0 T_1))) ### All 12 % 0.22/0.44 14. (All A, (All B, ((relation B) => ((reflexive B) => (reflexive (relation_restriction B A)))))) (-. (reflexive (relation_restriction T_0 T_1))) (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_0) ### All 13 % 0.22/0.44 15. (relation T_0) (-. (relation T_0)) ### Axiom % 0.22/0.44 16. (relation T_0) (-. (relation T_0)) ### Axiom % 0.22/0.44 17. (well_ordering T_0) (-. (well_ordering T_0)) ### Axiom % 0.22/0.44 18. (-. (transitive T_0)) (transitive T_0) ### Axiom % 0.22/0.44 19. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0))))) (-. (transitive T_0)) ### ConjTree 18 % 0.22/0.44 20. ((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 17 19 % 0.22/0.44 21. ((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 16 20 % 0.22/0.44 22. (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 21 % 0.22/0.44 23. (-. (transitive (relation_restriction T_0 T_1))) (transitive (relation_restriction T_0 T_1)) ### Axiom % 0.22/0.44 24. ((relation T_0) => ((transitive T_0) => (transitive (relation_restriction T_0 T_1)))) (-. (transitive (relation_restriction T_0 T_1))) (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_0) ### DisjTree 15 22 23 % 0.22/0.44 25. (All B, ((relation B) => ((transitive B) => (transitive (relation_restriction B T_1))))) (relation 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) (-. (transitive (relation_restriction T_0 T_1))) ### All 24 % 0.22/0.44 26. (All A, (All B, ((relation B) => ((transitive B) => (transitive (relation_restriction B A)))))) (-. (transitive (relation_restriction T_0 T_1))) (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_0) ### All 25 % 0.22/0.44 27. (relation T_0) (-. (relation T_0)) ### Axiom % 0.22/0.44 28. (relation T_0) (-. (relation T_0)) ### Axiom % 0.22/0.44 29. (well_ordering T_0) (-. (well_ordering T_0)) ### Axiom % 0.22/0.44 30. (-. (antisymmetric T_0)) (antisymmetric T_0) ### Axiom % 0.22/0.44 31. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0))))) (-. (antisymmetric T_0)) ### ConjTree 30 % 0.22/0.44 32. ((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 29 31 % 0.22/0.44 33. ((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 28 32 % 0.22/0.44 34. (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 33 % 0.22/0.44 35. (-. (antisymmetric (relation_restriction T_0 T_1))) (antisymmetric (relation_restriction T_0 T_1)) ### Axiom % 0.22/0.44 36. ((relation T_0) => ((antisymmetric T_0) => (antisymmetric (relation_restriction T_0 T_1)))) (-. (antisymmetric (relation_restriction T_0 T_1))) (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_0) ### DisjTree 27 34 35 % 0.22/0.44 37. (All B, ((relation B) => ((antisymmetric B) => (antisymmetric (relation_restriction B T_1))))) (relation 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) (-. (antisymmetric (relation_restriction T_0 T_1))) ### All 36 % 0.22/0.44 38. (All A, (All B, ((relation B) => ((antisymmetric B) => (antisymmetric (relation_restriction B A)))))) (-. (antisymmetric (relation_restriction T_0 T_1))) (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_0) ### All 37 % 0.22/0.44 39. (relation T_0) (-. (relation T_0)) ### Axiom % 0.22/0.44 40. (relation T_0) (-. (relation T_0)) ### Axiom % 0.22/0.44 41. (well_ordering T_0) (-. (well_ordering T_0)) ### Axiom % 0.22/0.44 42. (-. (connected T_0)) (connected T_0) ### Axiom % 0.22/0.44 43. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0))))) (-. (connected T_0)) ### ConjTree 42 % 0.22/0.44 44. ((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 41 43 % 0.22/0.44 45. ((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 40 44 % 0.22/0.44 46. (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 45 % 0.22/0.44 47. (-. (connected (relation_restriction T_0 T_1))) (connected (relation_restriction T_0 T_1)) ### Axiom % 0.22/0.44 48. ((relation T_0) => ((connected T_0) => (connected (relation_restriction T_0 T_1)))) (-. (connected (relation_restriction T_0 T_1))) (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_0) ### DisjTree 39 46 47 % 0.22/0.44 49. (All B, ((relation B) => ((connected B) => (connected (relation_restriction B T_1))))) (relation 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) (-. (connected (relation_restriction T_0 T_1))) ### All 48 % 0.22/0.44 50. (All A, (All B, ((relation B) => ((connected B) => (connected (relation_restriction B A)))))) (-. (connected (relation_restriction T_0 T_1))) (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_0) ### All 49 % 0.22/0.44 51. (relation T_0) (-. (relation T_0)) ### Axiom % 0.22/0.44 52. (relation T_0) (-. (relation T_0)) ### Axiom % 0.22/0.44 53. (well_ordering T_0) (-. (well_ordering T_0)) ### Axiom % 0.22/0.44 54. (-. (well_founded_relation T_0)) (well_founded_relation T_0) ### Axiom % 0.22/0.44 55. ((reflexive T_0) /\ ((transitive T_0) /\ ((antisymmetric T_0) /\ ((connected T_0) /\ (well_founded_relation T_0))))) (-. (well_founded_relation T_0)) ### ConjTree 54 % 0.22/0.44 56. ((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 53 55 % 0.22/0.44 57. ((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 52 56 % 0.22/0.44 58. (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 57 % 0.22/0.44 59. (-. (well_founded_relation (relation_restriction T_0 T_1))) (well_founded_relation (relation_restriction T_0 T_1)) ### Axiom % 0.22/0.44 60. ((relation T_0) => ((well_founded_relation T_0) => (well_founded_relation (relation_restriction T_0 T_1)))) (-. (well_founded_relation (relation_restriction T_0 T_1))) (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_0) ### DisjTree 51 58 59 % 0.22/0.44 61. (All B, ((relation B) => ((well_founded_relation B) => (well_founded_relation (relation_restriction B T_1))))) (relation 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) (-. (well_founded_relation (relation_restriction T_0 T_1))) ### All 60 % 0.22/0.44 62. (All A, (All B, ((relation B) => ((well_founded_relation B) => (well_founded_relation (relation_restriction B A)))))) (-. (well_founded_relation (relation_restriction T_0 T_1))) (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_0) ### All 61 % 0.22/0.44 63. (-. ((reflexive (relation_restriction T_0 T_1)) /\ ((transitive (relation_restriction T_0 T_1)) /\ ((antisymmetric (relation_restriction T_0 T_1)) /\ ((connected (relation_restriction T_0 T_1)) /\ (well_founded_relation (relation_restriction T_0 T_1))))))) (All A, (All B, ((relation B) => ((well_founded_relation B) => (well_founded_relation (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((connected B) => (connected (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((antisymmetric B) => (antisymmetric (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((transitive B) => (transitive (relation_restriction B A)))))) (relation 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) (All A, (All B, ((relation B) => ((reflexive B) => (reflexive (relation_restriction B A)))))) ### DisjTree 14 26 38 50 62 % 0.22/0.44 64. (-. (well_ordering (relation_restriction T_0 T_1))) (well_ordering (relation_restriction T_0 T_1)) ### Axiom % 0.22/0.44 65. ((well_ordering (relation_restriction T_0 T_1)) <=> ((reflexive (relation_restriction T_0 T_1)) /\ ((transitive (relation_restriction T_0 T_1)) /\ ((antisymmetric (relation_restriction T_0 T_1)) /\ ((connected (relation_restriction T_0 T_1)) /\ (well_founded_relation (relation_restriction T_0 T_1))))))) (-. (well_ordering (relation_restriction T_0 T_1))) (All A, (All B, ((relation B) => ((reflexive B) => (reflexive (relation_restriction B A)))))) (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_0) (All A, (All B, ((relation B) => ((transitive B) => (transitive (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((antisymmetric B) => (antisymmetric (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((connected B) => (connected (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((well_founded_relation B) => (well_founded_relation (relation_restriction B A)))))) ### Equiv 63 64 % 0.22/0.44 66. ((relation (relation_restriction T_0 T_1)) => ((well_ordering (relation_restriction T_0 T_1)) <=> ((reflexive (relation_restriction T_0 T_1)) /\ ((transitive (relation_restriction T_0 T_1)) /\ ((antisymmetric (relation_restriction T_0 T_1)) /\ ((connected (relation_restriction T_0 T_1)) /\ (well_founded_relation (relation_restriction T_0 T_1)))))))) (All A, (All B, ((relation B) => ((well_founded_relation B) => (well_founded_relation (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((connected B) => (connected (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((antisymmetric B) => (antisymmetric (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((transitive B) => (transitive (relation_restriction B 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, (All B, ((relation B) => ((reflexive B) => (reflexive (relation_restriction B A)))))) (-. (well_ordering (relation_restriction T_0 T_1))) (relation T_0) ### Imply 2 65 % 0.22/0.44 67. (relation T_0) (-. (well_ordering (relation_restriction T_0 T_1))) (All A, (All B, ((relation B) => ((reflexive B) => (reflexive (relation_restriction B 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, (All B, ((relation B) => ((transitive B) => (transitive (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((antisymmetric B) => (antisymmetric (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((connected B) => (connected (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((well_founded_relation B) => (well_founded_relation (relation_restriction B A)))))) ### All 66 % 0.22/0.44 68. (-. ((relation T_0) => ((well_ordering T_0) => (well_ordering (relation_restriction T_0 T_1))))) (All A, (All B, ((relation B) => ((well_founded_relation B) => (well_founded_relation (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((connected B) => (connected (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((antisymmetric B) => (antisymmetric (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((transitive B) => (transitive (relation_restriction B A)))))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (All A, (All B, ((relation B) => ((reflexive B) => (reflexive (relation_restriction B A)))))) ### ConjTree 67 % 0.22/0.44 69. (-. (All B, ((relation B) => ((well_ordering B) => (well_ordering (relation_restriction B T_1)))))) (All A, (All B, ((relation B) => ((reflexive B) => (reflexive (relation_restriction B A)))))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (All A, (All B, ((relation B) => ((transitive B) => (transitive (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((antisymmetric B) => (antisymmetric (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((connected B) => (connected (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((well_founded_relation B) => (well_founded_relation (relation_restriction B A)))))) ### NotAllEx 68 % 0.22/0.44 70. (-. (All A, (All B, ((relation B) => ((well_ordering B) => (well_ordering (relation_restriction B A))))))) (All A, (All B, ((relation B) => ((well_founded_relation B) => (well_founded_relation (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((connected B) => (connected (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((antisymmetric B) => (antisymmetric (relation_restriction B A)))))) (All A, (All B, ((relation B) => ((transitive B) => (transitive (relation_restriction B A)))))) (All A, ((relation A) => ((well_ordering A) <=> ((reflexive A) /\ ((transitive A) /\ ((antisymmetric A) /\ ((connected A) /\ (well_founded_relation A)))))))) (All A, (All B, ((relation B) => ((reflexive B) => (reflexive (relation_restriction B A)))))) ### NotAllEx 69 % 0.22/0.44 % SZS output end Proof % 0.22/0.44 (* END-PROOF *) %------------------------------------------------------------------------------