%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM578+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n015.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:00 EDT 2022 % Result : Theorem 4.18s 4.38s % Output : Proof 4.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM578+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n015.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jul 6 09:23:18 EDT 2022 % 0.12/0.33 % CPUTime : % 4.18/4.38 (* PROOF-FOUND *) % 4.18/4.38 % SZS status Theorem % 4.18/4.38 (* BEGIN-PROOF *) % 4.18/4.38 % SZS output start Proof % 4.18/4.38 Theorem m__ : ((forall W0 : zenon_U, (forall W1 : zenon_U, (((aElementOf0 W0 (szNzAzT0))/\(aElementOf0 W1 (szNzAzT0)))->((sdtlseqdt0 (szszuzczcdt0 W0) W1)->((aSubsetOf0 (sdtlpdtrp0 (xN) W1) (sdtmndt0 (sdtlpdtrp0 (xN) W0) (szmzizndt0 (sdtlpdtrp0 (xN) W0))))/\(~((szmzizndt0 (sdtlpdtrp0 (xN) W1)) = (szmzizndt0 (sdtlpdtrp0 (xN) W0)))))))))->((~((xi) = (xj)))->(~((szmzizndt0 (sdtlpdtrp0 (xN) (xi))) = (szmzizndt0 (sdtlpdtrp0 (xN) (xj))))))). % 4.18/4.38 Proof. % 4.18/4.38 assert (zenon_L1_ : ((aSubsetOf0 (sdtlpdtrp0 (xN) (xi)) (sdtmndt0 (sdtlpdtrp0 (xN) (xj)) (szmzizndt0 (sdtlpdtrp0 (xN) (xj)))))/\(~((szmzizndt0 (sdtlpdtrp0 (xN) (xi))) = (szmzizndt0 (sdtlpdtrp0 (xN) (xj)))))) -> ((szmzizndt0 (sdtlpdtrp0 (xN) (xi))) = (szmzizndt0 (sdtlpdtrp0 (xN) (xj)))) -> False). % 4.18/4.38 do 0 intro. intros zenon_H55 zenon_H56. % 4.18/4.38 apply (zenon_and_s _ _ zenon_H55). zenon_intro zenon_H58. zenon_intro zenon_H57. % 4.18/4.38 exact (zenon_H57 zenon_H56). % 4.18/4.38 (* end of lemma zenon_L1_ *) % 4.18/4.38 apply NNPP. intro zenon_G. % 4.18/4.38 apply (zenon_and_s _ _ m__3856). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 4.18/4.38 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H5c. zenon_intro zenon_H5b. % 4.18/4.38 apply (zenon_notimply_s _ _ zenon_H5b). zenon_intro zenon_H5e. zenon_intro zenon_H5d. % 4.18/4.38 apply zenon_H5d. zenon_intro zenon_H56. % 4.18/4.38 apply (zenon_imply_s _ _ m__3856_02); [ zenon_intro zenon_H60 | zenon_intro zenon_H5f ]. % 4.18/4.38 exact (zenon_H60 zenon_H5e). % 4.18/4.38 apply (zenon_or_s _ _ zenon_H5f); [ zenon_intro zenon_H62 | zenon_intro zenon_H61 ]. % 4.18/4.38 generalize (zenon_H5c (xj)). zenon_intro zenon_H63. % 4.18/4.38 generalize (zenon_H63 (xi)). zenon_intro zenon_H64. % 4.18/4.38 apply (zenon_imply_s _ _ zenon_H64); [ zenon_intro zenon_H66 | zenon_intro zenon_H65 ]. % 4.18/4.38 apply (zenon_notand_s _ _ zenon_H66); [ zenon_intro zenon_H68 | zenon_intro zenon_H67 ]. % 4.18/4.38 exact (zenon_H68 zenon_H59). % 4.18/4.38 exact (zenon_H67 zenon_H5a). % 4.18/4.38 apply (zenon_imply_s _ _ zenon_H65); [ zenon_intro zenon_H69 | zenon_intro zenon_H55 ]. % 4.18/4.38 exact (zenon_H69 zenon_H62). % 4.18/4.38 apply (zenon_L1_); trivial. % 4.18/4.38 generalize (zenon_H5c (xi)). zenon_intro zenon_H6a. % 4.18/4.38 generalize (zenon_H6a (xj)). zenon_intro zenon_H6b. % 4.18/4.38 apply (zenon_imply_s _ _ zenon_H6b); [ zenon_intro zenon_H6d | zenon_intro zenon_H6c ]. % 4.18/4.38 apply (zenon_notand_s _ _ zenon_H6d); [ zenon_intro zenon_H67 | zenon_intro zenon_H68 ]. % 4.18/4.38 exact (zenon_H67 zenon_H5a). % 4.18/4.38 exact (zenon_H68 zenon_H59). % 4.18/4.38 apply (zenon_imply_s _ _ zenon_H6c); [ zenon_intro zenon_H6f | zenon_intro zenon_H6e ]. % 4.18/4.38 exact (zenon_H6f zenon_H61). % 4.18/4.38 apply (zenon_and_s _ _ zenon_H6e). zenon_intro zenon_H71. zenon_intro zenon_H70. % 4.18/4.38 apply zenon_H70. apply sym_equal. exact zenon_H56. % 4.18/4.38 Qed. % 4.18/4.38 % SZS output end Proof % 4.18/4.38 (* END-PROOF *) % 4.18/4.38 nodes searched: 121331 % 4.18/4.38 max branch formulas: 5331 % 4.18/4.38 proof nodes created: 4889 % 4.18/4.38 formulas created: 373597 % 4.18/4.38 %------------------------------------------------------------------------------