%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM630+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % 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 : Mon Jul 18 15:57:30 EDT 2022 % Result : Theorem 0.60s 0.77s % Output : Proof 0.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : NUM630+1 : TPTP v8.1.0. Released v4.0.0. % 0.04/0.14 % Command : run_zenon %s %d % 0.14/0.35 % Computer : n007.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Wed Jul 6 09:51:43 EDT 2022 % 0.14/0.35 % CPUTime : % 0.60/0.77 (* PROOF-FOUND *) % 0.60/0.77 % SZS status Theorem % 0.60/0.77 (* BEGIN-PROOF *) % 0.60/0.77 % SZS output start Proof % 0.60/0.77 Theorem m__ : ((sdtlpdtrp0 (xc) (sdtpldt0 (xP) (szmzizndt0 (sdtlpdtrp0 (xN) (xn))))) = (sdtlpdtrp0 (sdtlpdtrp0 (xC) (xn)) (xP))). % 0.60/0.77 Proof. % 0.60/0.77 assert (zenon_L1_ : (~((xP) = (xP))) -> False). % 0.60/0.77 do 0 intro. intros zenon_H73. % 0.60/0.77 apply zenon_H73. apply refl_equal. % 0.60/0.77 (* end of lemma zenon_L1_ *) % 0.60/0.77 assert (zenon_L2_ : (~((xk) = (xk))) -> False). % 0.60/0.77 do 0 intro. intros zenon_H74. % 0.60/0.77 apply zenon_H74. apply refl_equal. % 0.60/0.77 (* end of lemma zenon_L2_ *) % 0.60/0.77 apply NNPP. intro zenon_G. % 0.60/0.77 apply (zenon_and_s _ _ m__4151). zenon_intro zenon_H76. zenon_intro zenon_H75. % 0.60/0.77 apply (zenon_and_s _ _ zenon_H75). zenon_intro zenon_H78. zenon_intro zenon_H77. % 0.60/0.77 apply (zenon_and_s _ _ m__5164). zenon_intro zenon_H7a. zenon_intro zenon_H79. % 0.60/0.77 apply (zenon_and_s _ _ m__5309). zenon_intro zenon_H7c. zenon_intro zenon_H7b. % 0.60/0.77 apply (zenon_and_s _ _ zenon_H7b). zenon_intro zenon_H7e. zenon_intro zenon_H7d. % 0.60/0.77 generalize (zenon_H77 (xn)). zenon_intro zenon_H7f. % 0.60/0.77 apply (zenon_imply_s _ _ zenon_H7f); [ zenon_intro zenon_H81 | zenon_intro zenon_H80 ]. % 0.60/0.77 exact (zenon_H81 zenon_H7e). % 0.60/0.77 apply (zenon_and_s _ _ zenon_H80). zenon_intro zenon_H83. zenon_intro zenon_H82. % 0.60/0.77 apply (zenon_and_s _ _ zenon_H82). zenon_intro zenon_H85. zenon_intro zenon_H84. % 0.60/0.77 generalize (zenon_H84 (xP)). zenon_intro zenon_H86. % 0.60/0.77 apply (zenon_imply_s _ _ zenon_H86); [ zenon_intro zenon_H88 | zenon_intro zenon_H87 ]. % 0.60/0.77 apply (zenon_notand_s _ _ zenon_H88); [ zenon_intro zenon_H8a | zenon_intro zenon_H89 ]. % 0.60/0.77 exact (zenon_H8a zenon_H7a). % 0.60/0.77 cut ((aElementOf0 (xP) (slbdtsldtrb0 (xD) (xk))) = (aElementOf0 (xP) (slbdtsldtrb0 (sdtmndt0 (sdtlpdtrp0 (xN) (xn)) (szmzizndt0 (sdtlpdtrp0 (xN) (xn)))) (xk)))). % 0.60/0.77 intro zenon_D_pnotp. % 0.60/0.77 apply zenon_H89. % 0.60/0.77 rewrite <- zenon_D_pnotp. % 0.60/0.77 exact m__5599. % 0.60/0.77 cut (((slbdtsldtrb0 (xD) (xk)) = (slbdtsldtrb0 (sdtmndt0 (sdtlpdtrp0 (xN) (xn)) (szmzizndt0 (sdtlpdtrp0 (xN) (xn)))) (xk)))); [idtac | apply NNPP; zenon_intro zenon_H8b]. % 0.60/0.77 cut (((xP) = (xP))); [idtac | apply NNPP; zenon_intro zenon_H73]. % 0.60/0.77 congruence. % 0.60/0.77 apply zenon_H73. apply refl_equal. % 0.60/0.77 cut (((xk) = (xk))); [idtac | apply NNPP; zenon_intro zenon_H74]. % 0.60/0.77 cut (((xD) = (sdtmndt0 (sdtlpdtrp0 (xN) (xn)) (szmzizndt0 (sdtlpdtrp0 (xN) (xn)))))); [idtac | apply NNPP; zenon_intro zenon_H8c]. % 0.60/0.77 congruence. % 0.60/0.77 exact (zenon_H8c m__5585). % 0.60/0.77 apply zenon_H74. apply refl_equal. % 0.60/0.77 apply zenon_G. apply sym_equal. exact zenon_H87. % 0.60/0.77 Qed. % 0.60/0.77 % SZS output end Proof % 0.60/0.77 (* END-PROOF *) % 0.60/0.77 nodes searched: 3621 % 0.60/0.77 max branch formulas: 2376 % 0.60/0.77 proof nodes created: 88 % 0.60/0.77 formulas created: 34998 % 0.60/0.77 %------------------------------------------------------------------------------