%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : SYN938+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 13:56:33 EDT 2022 % Result : Theorem 0.20s 0.54s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN938+1 : TPTP v8.1.0. Released v3.1.0. % 0.07/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jul 11 21:20:12 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.54 (* PROOF-FOUND *) % 0.20/0.54 % SZS status Theorem % 0.20/0.54 (* BEGIN-PROOF *) % 0.20/0.54 % SZS output start Proof % 0.20/0.54 Theorem prove_this : False. % 0.20/0.54 Proof. % 0.20/0.54 assert (zenon_L1_ : forall (zenon_TC_bk : zenon_U) (zenon_TB_bl : zenon_U), (~((r1 zenon_TB_bl)->((r1 zenon_TB_bl)/\(r1 zenon_TC_bk)))) -> (~(r1 zenon_TB_bl)) -> False). % 0.20/0.54 do 2 intro. intros zenon_H22 zenon_H23. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H22). zenon_intro zenon_H27. zenon_intro zenon_H26. % 0.20/0.54 exact (zenon_H23 zenon_H27). % 0.20/0.54 (* end of lemma zenon_L1_ *) % 0.20/0.54 assert (zenon_L2_ : forall (zenon_TB_bl : zenon_U) (zenon_TC_bk : zenon_U), (~((r1 zenon_TC_bk)->((r1 zenon_TB_bl)/\(r1 zenon_TC_bk)))) -> (~(r1 zenon_TC_bk)) -> False). % 0.20/0.54 do 2 intro. intros zenon_H28 zenon_H29. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H28). zenon_intro zenon_H2a. zenon_intro zenon_H26. % 0.20/0.54 exact (zenon_H29 zenon_H2a). % 0.20/0.54 (* end of lemma zenon_L2_ *) % 0.20/0.54 assert (zenon_L3_ : forall (zenon_TC_bk : zenon_U) (zenon_TB_bl : zenon_U), (~((r1 zenon_TB_bl)/\(r1 zenon_TC_bk))) -> (~(exists X : zenon_U, (exists Y : zenon_U, (((p1 (f Y))->(p1 X))/\(((r1 Y)->((r1 zenon_TB_bl)/\(r1 zenon_TC_bk)))/\(q1 X)))))) -> (forall Z : zenon_U, (q1 (f Z))) -> False). % 0.20/0.54 do 2 intro. intros zenon_H26 zenon_H2b zenon_H0. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H26); [ zenon_intro zenon_H23 | zenon_intro zenon_H29 ]. % 0.20/0.54 generalize (zenon_H0 zenon_TB_bl). zenon_intro zenon_H2c. % 0.20/0.54 apply zenon_H2b. exists (f zenon_TB_bl). apply NNPP. zenon_intro zenon_H2d. % 0.20/0.54 apply zenon_H2d. exists zenon_TB_bl. apply NNPP. zenon_intro zenon_H2e. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H2e); [ zenon_intro zenon_H30 | zenon_intro zenon_H2f ]. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H30). zenon_intro zenon_H32. zenon_intro zenon_H31. % 0.20/0.54 exact (zenon_H31 zenon_H32). % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H2f); [ zenon_intro zenon_H22 | zenon_intro zenon_H33 ]. % 0.20/0.54 apply (zenon_L1_ zenon_TC_bk zenon_TB_bl); trivial. % 0.20/0.54 exact (zenon_H33 zenon_H2c). % 0.20/0.54 generalize (zenon_H0 zenon_TC_bk). zenon_intro zenon_H34. % 0.20/0.54 apply zenon_H2b. exists (f zenon_TC_bk). apply NNPP. zenon_intro zenon_H35. % 0.20/0.54 apply zenon_H35. exists zenon_TC_bk. apply NNPP. zenon_intro zenon_H36. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H36); [ zenon_intro zenon_H38 | zenon_intro zenon_H37 ]. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H38). zenon_intro zenon_H3a. zenon_intro zenon_H39. % 0.20/0.54 exact (zenon_H39 zenon_H3a). % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H37); [ zenon_intro zenon_H28 | zenon_intro zenon_H3b ]. % 0.20/0.54 apply (zenon_L2_ zenon_TB_bl zenon_TC_bk); trivial. % 0.20/0.54 exact (zenon_H3b zenon_H34). % 0.20/0.54 (* end of lemma zenon_L3_ *) % 0.20/0.54 assert (zenon_L4_ : forall (zenon_TC_ck : zenon_U) (zenon_TB_cl : zenon_U), (~((r1 zenon_TB_cl)->((r1 zenon_TB_cl)/\(r1 zenon_TC_ck)))) -> (~(r1 zenon_TB_cl)) -> False). % 0.20/0.54 do 2 intro. intros zenon_H3c zenon_H3d. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H3c). zenon_intro zenon_H41. zenon_intro zenon_H40. % 0.20/0.54 exact (zenon_H3d zenon_H41). % 0.20/0.54 (* end of lemma zenon_L4_ *) % 0.20/0.54 assert (zenon_L5_ : forall (zenon_TB_cl : zenon_U) (zenon_TC_ck : zenon_U), (~((r1 zenon_TC_ck)->((r1 zenon_TB_cl)/\(r1 zenon_TC_ck)))) -> (~(r1 zenon_TC_ck)) -> False). % 0.20/0.54 do 2 intro. intros zenon_H42 zenon_H43. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H42). zenon_intro zenon_H44. zenon_intro zenon_H40. % 0.20/0.54 exact (zenon_H43 zenon_H44). % 0.20/0.54 (* end of lemma zenon_L5_ *) % 0.20/0.54 assert (zenon_L6_ : forall (zenon_TC_cu : zenon_U) (zenon_TB_cv : zenon_U), (~(exists Y : zenon_U, (((p1 (f Y))->((p1 (f zenon_TB_cv))/\((r1 Y)->((r1 zenon_TB_cv)/\(r1 zenon_TC_cu)))))/\(q1 (f zenon_TB_cv))))) -> (~(p1 (f zenon_TB_cv))) -> (q1 (f zenon_TB_cv)) -> False). % 0.20/0.54 do 2 intro. intros zenon_H45 zenon_H46 zenon_H47. % 0.20/0.54 apply zenon_H45. exists zenon_TB_cv. apply NNPP. zenon_intro zenon_H4a. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H4a); [ zenon_intro zenon_H4c | zenon_intro zenon_H4b ]. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H4c). zenon_intro zenon_H4e. zenon_intro zenon_H4d. % 0.20/0.54 exact (zenon_H46 zenon_H4e). % 0.20/0.54 exact (zenon_H4b zenon_H47). % 0.20/0.54 (* end of lemma zenon_L6_ *) % 0.20/0.54 assert (zenon_L7_ : forall (zenon_TA_de : zenon_U), (~((p1 zenon_TA_de)/\(g zenon_TA_de))) -> (g zenon_TA_de) -> (p1 zenon_TA_de) -> False). % 0.20/0.54 do 1 intro. intros zenon_H4f zenon_H50 zenon_H51. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H4f); [ zenon_intro zenon_H54 | zenon_intro zenon_H53 ]. % 0.20/0.54 exact (zenon_H54 zenon_H51). % 0.20/0.54 exact (zenon_H53 zenon_H50). % 0.20/0.54 (* end of lemma zenon_L7_ *) % 0.20/0.54 assert (zenon_L8_ : (~(forall A : zenon_U, (forall B : zenon_U, (forall C : zenon_U, (((s1 A)/\((s1 B)/\((r B C)/\((forall X : zenon_U, ((s1 X)->(p1 X)))/\(forall X : zenon_U, (forall Y : zenon_U, ((r X Y)->(q X Y))))))))->(exists X : zenon_U, (exists Y : zenon_U, ((p1 X)/\(q X Y))))))))) -> False). % 0.20/0.54 do 0 intro. intros zenon_H55. % 0.20/0.54 apply (zenon_notallex_s (fun A : zenon_U => (forall B : zenon_U, (forall C : zenon_U, (((s1 A)/\((s1 B)/\((r B C)/\((forall X : zenon_U, ((s1 X)->(p1 X)))/\(forall X : zenon_U, (forall Y : zenon_U, ((r X Y)->(q X Y))))))))->(exists X : zenon_U, (exists Y : zenon_U, ((p1 X)/\(q X Y)))))))) zenon_H55); [ zenon_intro zenon_H56; idtac ]. % 0.20/0.54 elim zenon_H56. zenon_intro zenon_TA_dj. zenon_intro zenon_H58. % 0.20/0.54 apply (zenon_notallex_s (fun B : zenon_U => (forall C : zenon_U, (((s1 zenon_TA_dj)/\((s1 B)/\((r B C)/\((forall X : zenon_U, ((s1 X)->(p1 X)))/\(forall X : zenon_U, (forall Y : zenon_U, ((r X Y)->(q X Y))))))))->(exists X : zenon_U, (exists Y : zenon_U, ((p1 X)/\(q X Y))))))) zenon_H58); [ zenon_intro zenon_H59; idtac ]. % 0.20/0.54 elim zenon_H59. zenon_intro zenon_TB_dm. zenon_intro zenon_H5b. % 0.20/0.54 apply (zenon_notallex_s (fun C : zenon_U => (((s1 zenon_TA_dj)/\((s1 zenon_TB_dm)/\((r zenon_TB_dm C)/\((forall X : zenon_U, ((s1 X)->(p1 X)))/\(forall X : zenon_U, (forall Y : zenon_U, ((r X Y)->(q X Y))))))))->(exists X : zenon_U, (exists Y : zenon_U, ((p1 X)/\(q X Y)))))) zenon_H5b); [ zenon_intro zenon_H5c; idtac ]. % 0.20/0.54 elim zenon_H5c. zenon_intro zenon_TC_dp. zenon_intro zenon_H5e. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H5e). zenon_intro zenon_H60. zenon_intro zenon_H5f. % 0.20/0.54 apply (zenon_and_s _ _ zenon_H60). zenon_intro zenon_H62. zenon_intro zenon_H61. % 0.20/0.54 apply (zenon_and_s _ _ zenon_H61). zenon_intro zenon_H64. zenon_intro zenon_H63. % 0.20/0.54 apply (zenon_and_s _ _ zenon_H63). zenon_intro zenon_H66. zenon_intro zenon_H65. % 0.20/0.54 apply (zenon_and_s _ _ zenon_H65). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.20/0.54 apply zenon_H5f. exists zenon_TB_dm. apply NNPP. zenon_intro zenon_H69. % 0.20/0.54 apply zenon_H69. exists zenon_TC_dp. apply NNPP. zenon_intro zenon_H6a. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H6a); [ zenon_intro zenon_H6c | zenon_intro zenon_H6b ]. % 0.20/0.54 generalize (zenon_H68 zenon_TB_dm). zenon_intro zenon_H6d. % 0.20/0.54 apply (zenon_imply_s _ _ zenon_H6d); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 0.20/0.54 exact (zenon_H6f zenon_H64). % 0.20/0.54 exact (zenon_H6c zenon_H6e). % 0.20/0.54 generalize (zenon_H67 zenon_TB_dm). zenon_intro zenon_H70. % 0.20/0.54 generalize (zenon_H70 zenon_TC_dp). zenon_intro zenon_H71. % 0.20/0.54 apply (zenon_imply_s _ _ zenon_H71); [ zenon_intro zenon_H73 | zenon_intro zenon_H72 ]. % 0.20/0.54 exact (zenon_H73 zenon_H66). % 0.20/0.54 exact (zenon_H6b zenon_H72). % 0.20/0.54 (* end of lemma zenon_L8_ *) % 0.20/0.54 assert (zenon_L9_ : forall (zenon_TB_ep : zenon_U) (zenon_TA_eq : zenon_U), (forall Y : zenon_U, ((q1 Y)->(p1 Y))) -> (~(exists X : zenon_U, (((p1 X)->(p1 zenon_TA_eq))/\((q1 X)->(p1 zenon_TB_ep))))) -> (~(p1 zenon_TB_ep)) -> False). % 0.20/0.54 do 2 intro. intros zenon_H74 zenon_H75 zenon_H76. % 0.20/0.54 generalize (zenon_H74 zenon_TB_ep). zenon_intro zenon_H79. % 0.20/0.54 apply (zenon_imply_s _ _ zenon_H79); [ zenon_intro zenon_H7b | zenon_intro zenon_H7a ]. % 0.20/0.54 apply zenon_H75. exists zenon_TB_ep. apply NNPP. zenon_intro zenon_H7c. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H7c); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H7e). zenon_intro zenon_H7a. zenon_intro zenon_H7f. % 0.20/0.54 exact (zenon_H76 zenon_H7a). % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H7d). zenon_intro zenon_H80. zenon_intro zenon_H76. % 0.20/0.54 exact (zenon_H7b zenon_H80). % 0.20/0.54 exact (zenon_H76 zenon_H7a). % 0.20/0.54 (* end of lemma zenon_L9_ *) % 0.20/0.54 assert (zenon_L10_ : (~(forall A : zenon_U, (forall B : zenon_U, ((forall Y : zenon_U, ((q1 Y)->(p1 Y)))->(exists X : zenon_U, (((p1 X)->(p1 A))/\((q1 X)->(p1 B)))))))) -> False). % 0.20/0.54 do 0 intro. intros zenon_H81. % 0.20/0.54 apply (zenon_notallex_s (fun A : zenon_U => (forall B : zenon_U, ((forall Y : zenon_U, ((q1 Y)->(p1 Y)))->(exists X : zenon_U, (((p1 X)->(p1 A))/\((q1 X)->(p1 B))))))) zenon_H81); [ zenon_intro zenon_H82; idtac ]. % 0.20/0.54 elim zenon_H82. zenon_intro zenon_TA_eq. zenon_intro zenon_H83. % 0.20/0.54 apply (zenon_notallex_s (fun B : zenon_U => ((forall Y : zenon_U, ((q1 Y)->(p1 Y)))->(exists X : zenon_U, (((p1 X)->(p1 zenon_TA_eq))/\((q1 X)->(p1 B)))))) zenon_H83); [ zenon_intro zenon_H84; idtac ]. % 0.20/0.54 elim zenon_H84. zenon_intro zenon_TB_ep. zenon_intro zenon_H85. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H85). zenon_intro zenon_H74. zenon_intro zenon_H75. % 0.20/0.54 apply zenon_H75. exists zenon_E. apply NNPP. zenon_intro zenon_H86. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H86); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H88). zenon_intro zenon_H89. zenon_intro zenon_H7f. % 0.20/0.54 apply zenon_H75. exists zenon_TA_eq. apply NNPP. zenon_intro zenon_H8a. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_H8a); [ zenon_intro zenon_H8c | zenon_intro zenon_H8b ]. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H8c). zenon_intro zenon_H8d. zenon_intro zenon_H7f. % 0.20/0.54 exact (zenon_H7f zenon_H8d). % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H8b). zenon_intro zenon_H8e. zenon_intro zenon_H76. % 0.20/0.54 apply (zenon_L9_ zenon_TB_ep zenon_TA_eq); trivial. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H87). zenon_intro zenon_H8f. zenon_intro zenon_H76. % 0.20/0.54 apply (zenon_L9_ zenon_TB_ep zenon_TA_eq); trivial. % 0.20/0.54 (* end of lemma zenon_L10_ *) % 0.20/0.54 assert (zenon_L11_ : (~((exists X : zenon_U, (p1 X))->(exists X : zenon_U, (p1 X)))) -> False). % 0.20/0.54 do 0 intro. intros zenon_H90. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H90). zenon_intro zenon_H92. zenon_intro zenon_H91. % 0.20/0.54 exact (zenon_H91 zenon_H92). % 0.20/0.54 (* end of lemma zenon_L11_ *) % 0.20/0.54 assert (zenon_L12_ : forall (zenon_TX_fs : zenon_U), (~((p zenon_TX_fs zenon_TX_fs)->(exists W : zenon_U, (p W zenon_TX_fs)))) -> False). % 0.20/0.54 do 1 intro. intros zenon_H93. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H93). zenon_intro zenon_H96. zenon_intro zenon_H95. % 0.20/0.54 apply zenon_H95. exists zenon_TX_fs. apply NNPP. zenon_intro zenon_H97. % 0.20/0.54 exact (zenon_H97 zenon_H96). % 0.20/0.54 (* end of lemma zenon_L12_ *) % 0.20/0.54 assert (zenon_L13_ : forall (zenon_TX_fx : zenon_U) (zenon_TX_fs : zenon_U), (~(((p zenon_TX_fs zenon_TX_fs)/\(p zenon_TX_fs zenon_TX_fs))->(p zenon_TX_fs zenon_TX_fx))) -> (~(p zenon_TX_fs zenon_TX_fs)) -> False). % 0.20/0.54 do 2 intro. intros zenon_H98 zenon_H97. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_H98). zenon_intro zenon_H9b. zenon_intro zenon_H9a. % 0.20/0.54 apply (zenon_and_s _ _ zenon_H9b). zenon_intro zenon_H96. zenon_intro zenon_H96. % 0.20/0.54 exact (zenon_H97 zenon_H96). % 0.20/0.54 (* end of lemma zenon_L13_ *) % 0.20/0.54 assert (zenon_L14_ : (~(b0)) -> (b0) -> False). % 0.20/0.54 do 0 intro. intros zenon_H9c zenon_H9d. % 0.20/0.54 exact (zenon_H9c zenon_H9d). % 0.20/0.54 (* end of lemma zenon_L14_ *) % 0.20/0.54 assert (zenon_L15_ : (~(a0)) -> (a0) -> False). % 0.20/0.54 do 0 intro. intros zenon_H9e zenon_H9f. % 0.20/0.54 exact (zenon_H9e zenon_H9f). % 0.20/0.54 (* end of lemma zenon_L15_ *) % 0.20/0.54 assert (zenon_L16_ : forall (zenon_TB_gg : zenon_U), (~((r1 zenon_TB_gg)->(r1 zenon_TB_gg))) -> (r1 zenon_TB_gg) -> False). % 0.20/0.54 do 1 intro. intros zenon_Ha0 zenon_Ha1. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_Ha0). zenon_intro zenon_Ha1. zenon_intro zenon_Ha3. % 0.20/0.54 exact (zenon_Ha3 zenon_Ha1). % 0.20/0.54 (* end of lemma zenon_L16_ *) % 0.20/0.54 assert (zenon_L17_ : forall (zenon_TB_gg : zenon_U), (~((q (f zenon_TB_gg) zenon_TB_gg)->(q (f zenon_TB_gg) zenon_TB_gg))) -> (q (f zenon_TB_gg) zenon_TB_gg) -> False). % 0.20/0.54 do 1 intro. intros zenon_Ha4 zenon_Ha5. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_Ha4). zenon_intro zenon_Ha5. zenon_intro zenon_Ha6. % 0.20/0.54 exact (zenon_Ha6 zenon_Ha5). % 0.20/0.54 (* end of lemma zenon_L17_ *) % 0.20/0.54 assert (zenon_L18_ : forall (zenon_TB_gg : zenon_U), (~(exists X : zenon_U, (exists Y : zenon_U, ((p X Y)/\((q (f zenon_TB_gg) zenon_TB_gg)->(q X Y)))))) -> (q (f zenon_TB_gg) zenon_TB_gg) -> (forall Y : zenon_U, (((r1 zenon_TB_gg)->(r1 Y))->(p (f Y) Y))) -> False). % 0.20/0.54 do 1 intro. intros zenon_Ha7 zenon_Ha5 zenon_H20. % 0.20/0.54 apply zenon_Ha7. exists (f zenon_TB_gg). apply NNPP. zenon_intro zenon_Ha8. % 0.20/0.54 apply zenon_Ha8. exists zenon_TB_gg. apply NNPP. zenon_intro zenon_Ha9. % 0.20/0.54 apply (zenon_notand_s _ _ zenon_Ha9); [ zenon_intro zenon_Haa | zenon_intro zenon_Ha4 ]. % 0.20/0.54 generalize (zenon_H20 zenon_TB_gg). zenon_intro zenon_Hab. % 0.20/0.54 apply (zenon_imply_s _ _ zenon_Hab); [ zenon_intro zenon_Ha0 | zenon_intro zenon_Hac ]. % 0.20/0.54 apply (zenon_notimply_s _ _ zenon_Ha0). zenon_intro zenon_Ha1. zenon_intro zenon_Ha3. % 0.20/0.54 exact (zenon_Ha3 zenon_Ha1). % 0.20/0.54 exact (zenon_Haa zenon_Hac). % 0.20/0.55 apply (zenon_L17_ zenon_TB_gg); trivial. % 0.20/0.55 (* end of lemma zenon_L18_ *) % 0.20/0.55 apply (zenon_notallex_s (fun X : zenon_U => (exists Y : zenon_U, (((p Y X)->(exists W : zenon_U, (p W Y)))/\(((p Zenon error: uncaught exception File "lltocoq.ml", line 117, characters 15-21: Assertion failed %------------------------------------------------------------------------------