%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SET775+4 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n018.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 06:38:29 EDT 2022 % Result : Theorem 0.62s 0.80s % Output : Proof 0.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SET775+4 : TPTP v8.1.0. Released v2.2.0. % 0.11/0.12 % Command : run_zenon %s %d % 0.11/0.33 % Computer : n018.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Sun Jul 10 02:14:27 EDT 2022 % 0.11/0.33 % CPUTime : % 0.62/0.80 (* PROOF-FOUND *) % 0.62/0.80 % SZS status Theorem % 0.62/0.80 (* BEGIN-PROOF *) % 0.62/0.80 % SZS output start Proof % 0.62/0.80 Theorem thIII11 : (forall E : zenon_U, (forall P : zenon_U, (forall R : zenon_U, (((pre_order P E)/\(forall A : zenon_U, (forall B : zenon_U, (((member A E)/\(member B E))->((apply R A B)<->((apply P A B)/\(apply P B A)))))))->(equivalence R E))))). % 0.62/0.80 Proof. % 0.62/0.80 apply NNPP. intro zenon_G. % 0.62/0.80 apply (zenon_notallex_s (fun E : zenon_U => (forall P : zenon_U, (forall R : zenon_U, (((pre_order P E)/\(forall A : zenon_U, (forall B : zenon_U, (((member A E)/\(member B E))->((apply R A B)<->((apply P A B)/\(apply P B A)))))))->(equivalence R E))))) zenon_G); [ zenon_intro zenon_H11; idtac ]. % 0.62/0.80 elim zenon_H11. zenon_intro zenon_TE_s. zenon_intro zenon_H13. % 0.62/0.80 apply (zenon_notallex_s (fun P : zenon_U => (forall R : zenon_U, (((pre_order P zenon_TE_s)/\(forall A : zenon_U, (forall B : zenon_U, (((member A zenon_TE_s)/\(member B zenon_TE_s))->((apply R A B)<->((apply P A B)/\(apply P B A)))))))->(equivalence R zenon_TE_s)))) zenon_H13); [ zenon_intro zenon_H14; idtac ]. % 0.62/0.80 elim zenon_H14. zenon_intro zenon_TP_v. zenon_intro zenon_H16. % 0.62/0.80 apply (zenon_notallex_s (fun R : zenon_U => (((pre_order zenon_TP_v zenon_TE_s)/\(forall A : zenon_U, (forall B : zenon_U, (((member A zenon_TE_s)/\(member B zenon_TE_s))->((apply R A B)<->((apply zenon_TP_v A B)/\(apply zenon_TP_v B A)))))))->(equivalence R zenon_TE_s))) zenon_H16); [ zenon_intro zenon_H17; idtac ]. % 0.62/0.80 elim zenon_H17. zenon_intro zenon_TR_y. zenon_intro zenon_H19. % 0.62/0.80 apply (zenon_notimply_s _ _ zenon_H19). zenon_intro zenon_H1b. zenon_intro zenon_H1a. % 0.62/0.80 apply (zenon_and_s _ _ zenon_H1b). zenon_intro zenon_H1d. zenon_intro zenon_H1c. % 0.62/0.80 generalize (pre_order zenon_TP_v). zenon_intro zenon_H1e. % 0.62/0.80 generalize (zenon_H1e zenon_TE_s). zenon_intro zenon_H1f. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H1f); [ zenon_intro zenon_H22; zenon_intro zenon_H21 | zenon_intro zenon_H1d; zenon_intro zenon_H20 ]. % 0.62/0.80 exact (zenon_H22 zenon_H1d). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H20). zenon_intro zenon_H24. zenon_intro zenon_H23. % 0.62/0.80 generalize (equivalence zenon_TE_s). zenon_intro zenon_H25. % 0.62/0.80 generalize (zenon_H25 zenon_TR_y). zenon_intro zenon_H26. % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H26); [ zenon_intro zenon_H1a; zenon_intro zenon_H29 | zenon_intro zenon_H28; zenon_intro zenon_H27 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H29); [ zenon_intro zenon_H2b | zenon_intro zenon_H2a ]. % 0.62/0.80 apply (zenon_notallex_s (fun X : zenon_U => ((member X zenon_TE_s)->(apply zenon_TR_y X X))) zenon_H2b); [ zenon_intro zenon_H2c; idtac ]. % 0.62/0.80 elim zenon_H2c. zenon_intro zenon_TX_bt. zenon_intro zenon_H2e. % 0.62/0.80 apply (zenon_notimply_s _ _ zenon_H2e). zenon_intro zenon_H30. zenon_intro zenon_H2f. % 0.62/0.80 generalize (zenon_H1c zenon_TX_bt). zenon_intro zenon_H31. % 0.62/0.80 generalize (zenon_H24 zenon_TX_bt). zenon_intro zenon_H32. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H32); [ zenon_intro zenon_H34 | zenon_intro zenon_H33 ]. % 0.62/0.80 exact (zenon_H34 zenon_H30). % 0.62/0.80 generalize (zenon_H31 zenon_TX_bt). zenon_intro zenon_H35. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H35); [ zenon_intro zenon_H37 | zenon_intro zenon_H36 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H37); [ zenon_intro zenon_H34 | zenon_intro zenon_H34 ]. % 0.62/0.80 exact (zenon_H34 zenon_H30). % 0.62/0.80 exact (zenon_H34 zenon_H30). % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H36); [ zenon_intro zenon_H2f; zenon_intro zenon_H3a | zenon_intro zenon_H39; zenon_intro zenon_H38 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H3a); [ zenon_intro zenon_H3b | zenon_intro zenon_H3b ]. % 0.62/0.80 exact (zenon_H3b zenon_H33). % 0.62/0.80 exact (zenon_H3b zenon_H33). % 0.62/0.80 exact (zenon_H2f zenon_H39). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H2a); [ zenon_intro zenon_H3d | zenon_intro zenon_H3c ]. % 0.62/0.80 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, (((member X zenon_TE_s)/\(member Y zenon_TE_s))->((apply zenon_TR_y X Y)->(apply zenon_TR_y Y X))))) zenon_H3d); [ zenon_intro zenon_H3e; idtac ]. % 0.62/0.80 elim zenon_H3e. zenon_intro zenon_TX_cl. zenon_intro zenon_H40. % 0.62/0.80 apply (zenon_notallex_s (fun Y : zenon_U => (((member zenon_TX_cl zenon_TE_s)/\(member Y zenon_TE_s))->((apply zenon_TR_y zenon_TX_cl Y)->(apply zenon_TR_y Y zenon_TX_cl)))) zenon_H40); [ zenon_intro zenon_H41; idtac ]. % 0.62/0.80 elim zenon_H41. zenon_intro zenon_TY_co. zenon_intro zenon_H43. % 0.62/0.80 apply (zenon_notimply_s _ _ zenon_H43). zenon_intro zenon_H45. zenon_intro zenon_H44. % 0.62/0.80 apply (zenon_notimply_s _ _ zenon_H44). zenon_intro zenon_H47. zenon_intro zenon_H46. % 0.62/0.80 apply (zenon_and_s _ _ zenon_H45). zenon_intro zenon_H49. zenon_intro zenon_H48. % 0.62/0.80 generalize (zenon_H1c zenon_TY_co). zenon_intro zenon_H4a. % 0.62/0.80 generalize (zenon_H4a zenon_TX_cl). zenon_intro zenon_H4b. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H4b); [ zenon_intro zenon_H4d | zenon_intro zenon_H4c ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H4d); [ zenon_intro zenon_H4f | zenon_intro zenon_H4e ]. % 0.62/0.80 exact (zenon_H4f zenon_H48). % 0.62/0.80 exact (zenon_H4e zenon_H49). % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H4c); [ zenon_intro zenon_H46; zenon_intro zenon_H52 | zenon_intro zenon_H51; zenon_intro zenon_H50 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H52); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 0.62/0.80 generalize (zenon_H1c zenon_TX_cl). zenon_intro zenon_H55. % 0.62/0.80 generalize (zenon_H55 zenon_TY_co). zenon_intro zenon_H56. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H56); [ zenon_intro zenon_H58 | zenon_intro zenon_H57 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H58); [ zenon_intro zenon_H4e | zenon_intro zenon_H4f ]. % 0.62/0.80 exact (zenon_H4e zenon_H49). % 0.62/0.80 exact (zenon_H4f zenon_H48). % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H57); [ zenon_intro zenon_H5b; zenon_intro zenon_H5a | zenon_intro zenon_H47; zenon_intro zenon_H59 ]. % 0.62/0.80 exact (zenon_H5b zenon_H47). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H5d. zenon_intro zenon_H5c. % 0.62/0.80 exact (zenon_H54 zenon_H5c). % 0.62/0.80 generalize (zenon_H1c zenon_TX_cl). zenon_intro zenon_H55. % 0.62/0.80 generalize (zenon_H55 zenon_TY_co). zenon_intro zenon_H56. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H56); [ zenon_intro zenon_H58 | zenon_intro zenon_H57 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H58); [ zenon_intro zenon_H4e | zenon_intro zenon_H4f ]. % 0.62/0.80 exact (zenon_H4e zenon_H49). % 0.62/0.80 exact (zenon_H4f zenon_H48). % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H57); [ zenon_intro zenon_H5b; zenon_intro zenon_H5a | zenon_intro zenon_H47; zenon_intro zenon_H59 ]. % 0.62/0.80 exact (zenon_H5b zenon_H47). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H5d. zenon_intro zenon_H5c. % 0.62/0.80 exact (zenon_H53 zenon_H5d). % 0.62/0.80 exact (zenon_H46 zenon_H51). % 0.62/0.80 apply (zenon_notallex_s (fun X : zenon_U => (forall Y : zenon_U, (forall Z : zenon_U, (((member X zenon_TE_s)/\((member Y zenon_TE_s)/\(member Z zenon_TE_s)))->(((apply zenon_TR_y X Y)/\(apply zenon_TR_y Y Z))->(apply zenon_TR_y X Z)))))) zenon_H3c); [ zenon_intro zenon_H5e; idtac ]. % 0.62/0.80 elim zenon_H5e. zenon_intro zenon_TX_dr. zenon_intro zenon_H60. % 0.62/0.80 apply (zenon_notallex_s (fun Y : zenon_U => (forall Z : zenon_U, (((member zenon_TX_dr zenon_TE_s)/\((member Y zenon_TE_s)/\(member Z zenon_TE_s)))->(((apply zenon_TR_y zenon_TX_dr Y)/\(apply zenon_TR_y Y Z))->(apply zenon_TR_y zenon_TX_dr Z))))) zenon_H60); [ zenon_intro zenon_H61; idtac ]. % 0.62/0.80 elim zenon_H61. zenon_intro zenon_TY_du. zenon_intro zenon_H63. % 0.62/0.80 apply (zenon_notallex_s (fun Z : zenon_U => (((member zenon_TX_dr zenon_TE_s)/\((member zenon_TY_du zenon_TE_s)/\(member Z zenon_TE_s)))->(((apply zenon_TR_y zenon_TX_dr zenon_TY_du)/\(apply zenon_TR_y zenon_TY_du Z))->(apply zenon_TR_y zenon_TX_dr Z)))) zenon_H63); [ zenon_intro zenon_H64; idtac ]. % 0.62/0.80 elim zenon_H64. zenon_intro zenon_TZ_dx. zenon_intro zenon_H66. % 0.62/0.80 apply (zenon_notimply_s _ _ zenon_H66). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.62/0.80 apply (zenon_notimply_s _ _ zenon_H67). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 0.62/0.80 apply (zenon_and_s _ _ zenon_H6a). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 0.62/0.80 apply (zenon_and_s _ _ zenon_H68). zenon_intro zenon_H6e. zenon_intro zenon_H6d. % 0.62/0.80 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H70. zenon_intro zenon_H6f. % 0.62/0.80 generalize (zenon_H1c zenon_TX_dr). zenon_intro zenon_H71. % 0.62/0.80 generalize (zenon_H71 zenon_TZ_dx). zenon_intro zenon_H72. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H72); [ zenon_intro zenon_H74 | zenon_intro zenon_H73 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H74); [ zenon_intro zenon_H76 | zenon_intro zenon_H75 ]. % 0.62/0.80 exact (zenon_H76 zenon_H6e). % 0.62/0.80 exact (zenon_H75 zenon_H6f). % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H73); [ zenon_intro zenon_H69; zenon_intro zenon_H79 | zenon_intro zenon_H78; zenon_intro zenon_H77 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H79); [ zenon_intro zenon_H7b | zenon_intro zenon_H7a ]. % 0.62/0.80 generalize (zenon_H23 zenon_TX_dr). zenon_intro zenon_H7c. % 0.62/0.80 generalize (zenon_H7c zenon_TY_du). zenon_intro zenon_H7d. % 0.62/0.80 generalize (zenon_H7d zenon_TZ_dx). zenon_intro zenon_H7e. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H7e); [ zenon_intro zenon_H80 | zenon_intro zenon_H7f ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H80); [ zenon_intro zenon_H76 | zenon_intro zenon_H81 ]. % 0.62/0.80 exact (zenon_H76 zenon_H6e). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H81); [ zenon_intro zenon_H82 | zenon_intro zenon_H75 ]. % 0.62/0.80 exact (zenon_H82 zenon_H70). % 0.62/0.80 exact (zenon_H75 zenon_H6f). % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H7f); [ zenon_intro zenon_H84 | zenon_intro zenon_H83 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H84); [ zenon_intro zenon_H86 | zenon_intro zenon_H85 ]. % 0.62/0.80 generalize (zenon_H71 zenon_TY_du). zenon_intro zenon_H87. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H76 | zenon_intro zenon_H82 ]. % 0.62/0.80 exact (zenon_H76 zenon_H6e). % 0.62/0.80 exact (zenon_H82 zenon_H70). % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H88); [ zenon_intro zenon_H8c; zenon_intro zenon_H8b | zenon_intro zenon_H6c; zenon_intro zenon_H8a ]. % 0.62/0.80 exact (zenon_H8c zenon_H6c). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H8a). zenon_intro zenon_H8e. zenon_intro zenon_H8d. % 0.62/0.80 exact (zenon_H86 zenon_H8e). % 0.62/0.80 generalize (zenon_H1c zenon_TY_du). zenon_intro zenon_H8f. % 0.62/0.80 generalize (zenon_H8f zenon_TZ_dx). zenon_intro zenon_H90. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H90); [ zenon_intro zenon_H81 | zenon_intro zenon_H91 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H81); [ zenon_intro zenon_H82 | zenon_intro zenon_H75 ]. % 0.62/0.80 exact (zenon_H82 zenon_H70). % 0.62/0.80 exact (zenon_H75 zenon_H6f). % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H91); [ zenon_intro zenon_H94; zenon_intro zenon_H93 | zenon_intro zenon_H6b; zenon_intro zenon_H92 ]. % 0.62/0.80 exact (zenon_H94 zenon_H6b). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H92). zenon_intro zenon_H96. zenon_intro zenon_H95. % 0.62/0.80 exact (zenon_H85 zenon_H96). % 0.62/0.80 exact (zenon_H7b zenon_H83). % 0.62/0.80 generalize (zenon_H23 zenon_TZ_dx). zenon_intro zenon_H97. % 0.62/0.80 generalize (zenon_H97 zenon_TY_du). zenon_intro zenon_H98. % 0.62/0.80 generalize (zenon_H98 zenon_TX_dr). zenon_intro zenon_H99. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H99); [ zenon_intro zenon_H9b | zenon_intro zenon_H9a ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H9b); [ zenon_intro zenon_H75 | zenon_intro zenon_H9c ]. % 0.62/0.80 exact (zenon_H75 zenon_H6f). % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H9c); [ zenon_intro zenon_H82 | zenon_intro zenon_H76 ]. % 0.62/0.80 exact (zenon_H82 zenon_H70). % 0.62/0.80 exact (zenon_H76 zenon_H6e). % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H9a); [ zenon_intro zenon_H9e | zenon_intro zenon_H9d ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H9e); [ zenon_intro zenon_Ha0 | zenon_intro zenon_H9f ]. % 0.62/0.80 generalize (zenon_H1c zenon_TY_du). zenon_intro zenon_H8f. % 0.62/0.80 generalize (zenon_H8f zenon_TZ_dx). zenon_intro zenon_H90. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H90); [ zenon_intro zenon_H81 | zenon_intro zenon_H91 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H81); [ zenon_intro zenon_H82 | zenon_intro zenon_H75 ]. % 0.62/0.80 exact (zenon_H82 zenon_H70). % 0.62/0.80 exact (zenon_H75 zenon_H6f). % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H91); [ zenon_intro zenon_H94; zenon_intro zenon_H93 | zenon_intro zenon_H6b; zenon_intro zenon_H92 ]. % 0.62/0.80 exact (zenon_H94 zenon_H6b). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H92). zenon_intro zenon_H96. zenon_intro zenon_H95. % 0.62/0.80 exact (zenon_Ha0 zenon_H95). % 0.62/0.80 generalize (zenon_H71 zenon_TY_du). zenon_intro zenon_H87. % 0.62/0.80 apply (zenon_imply_s _ _ zenon_H87); [ zenon_intro zenon_H89 | zenon_intro zenon_H88 ]. % 0.62/0.80 apply (zenon_notand_s _ _ zenon_H89); [ zenon_intro zenon_H76 | zenon_intro zenon_H82 ]. % 0.62/0.80 exact (zenon_H76 zenon_H6e). % 0.62/0.80 exact (zenon_H82 zenon_H70). % 0.62/0.80 apply (zenon_equiv_s _ _ zenon_H88); [ zenon_intro zenon_H8c; zenon_intro zenon_H8b | zenon_intro zenon_H6c; zenon_intro zenon_H8a ]. % 0.62/0.80 exact (zenon_H8c zenon_H6c). % 0.62/0.80 apply (zenon_and_s _ _ zenon_H8a). zenon_intro zenon_H8e. zenon_intro zenon_H8d. % 0.62/0.80 exact (zenon_H9f zenon_H8d). % 0.62/0.80 exact (zenon_H7a zenon_H9d). % 0.62/0.80 exact (zenon_H69 zenon_H78). % 0.62/0.80 exact (zenon_H1a zenon_H28). % 0.62/0.80 Qed. % 0.62/0.80 % SZS output end Proof % 0.62/0.80 (* END-PROOF *) % 0.62/0.80 nodes searched: 11121 % 0.62/0.80 max branch formulas: 1800 % 0.62/0.80 proof nodes created: 641 % 0.62/0.80 formulas created: 50015 % 0.62/0.80 %------------------------------------------------------------------------------