%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NUM578+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n027.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:01 EDT 2022 % Result : Theorem 0.42s 0.61s % Output : Proof 0.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM578+3 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n027.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 : Thu Jul 7 19:04:29 EDT 2022 % 0.13/0.34 % CPUTime : % 0.42/0.61 (* PROOF-FOUND *) % 0.42/0.61 % SZS status Theorem % 0.42/0.61 (* BEGIN-PROOF *) % 0.42/0.61 % SZS output start Proof % 0.42/0.61 Theorem m__ : ((forall W0 : zenon_U, (forall W1 : zenon_U, (((aElementOf0 W0 (szNzAzT0))/\(aElementOf0 W1 (szNzAzT0)))->((sdtlseqdt0 (szszuzczcdt0 W0) W1)->((aElementOf0 (szmzizndt0 (sdtlpdtrp0 (xN) W0)) (sdtlpdtrp0 (xN) W0))/\((forall W1 : zenon_U, ((aElementOf0 W1 (sdtlpdtrp0 (xN) W0))->(sdtlseqdt0 (szmzizndt0 (sdtlpdtrp0 (xN) W0)) W1)))/\((aSet0 (sdtmndt0 (sdtlpdtrp0 (xN) W0) (szmzizndt0 (sdtlpdtrp0 (xN) W0))))/\((forall W1 : zenon_U, ((aElementOf0 W1 (sdtmndt0 (sdtlpdtrp0 (xN) W0) (szmzizndt0 (sdtlpdtrp0 (xN) W0))))<->((aElement0 W1)/\((aElementOf0 W1 (sdtlpdtrp0 (xN) W0))/\(~(W1 = (szmzizndt0 (sdtlpdtrp0 (xN) W0))))))))/\((forall W2 : zenon_U, ((aElementOf0 W2 (sdtlpdtrp0 (xN) W1))->(aElementOf0 W2 (sdtmndt0 (sdtlpdtrp0 (xN) W0) (szmzizndt0 (sdtlpdtrp0 (xN) W0))))))/\((aSubsetOf0 (sdtlpdtrp0 (xN) W1) (sdtmndt0 (sdtlpdtrp0 (xN) W0) (szmzizndt0 (sdtlpdtrp0 (xN) W0))))/\(~(((aElementOf0 (szmzizndt0 (sdtlpdtrp0 (xN) W1)) (sdtlpdtrp0 (xN) W1))/\(forall W2 : zenon_U, ((aElementOf0 W2 (sdtlpdtrp0 (xN) W1))->(sdtlseqdt0 (szmzizndt0 (sdtlpdtrp0 (xN) W1)) W2))))->(((aElementOf0 (szmzizndt0 (sdtlpdtrp0 (xN) W1)) (sdtlpdtrp0 (xN) W0))/\(forall W2 : zenon_U, ((aElementOf0 W2 (sdtlpdtrp0 (xN) W0))->(sdtlseqdt0 (szmzizndt0 (sdtlpdtrp0 (xN) W1)) W2))))\/((szmzizndt0 (sdtlpdtrp0 (xN) W1)) = (szmzizndt0 (sdtlpdtrp0 (xN) W0))))))))))))))))->((~((xi) = (xj)))->(~((aElementOf0 (szmzizndt0 (sdtlpdtrp0 (xN) (xi))) (sdtlpdtrp0 (xN) (xi)))/\((forall W0 : zenon_U, ((aElementOf0 W0 (sdtlpdtrp0 (xN) (xi)))->(sdtlseqdt0 (szmzizndt0 (sdtlpdtrp0 (xN) (xi))) W0)))/\((aElementOf0 (szmzizndt0 (sdtlpdtrp0 (xN) (xi))) (sdtlpdtrp0 (xN) (xj)))/\((forall W0 : zenon_U, ((aElementOf0 W0 (sdtlpdtrp0 (xN) (xj)))->(sdtlseqdt0 (szmzizndt0 (sdtlpdtrp0 (xN) (xi))) W0)))/\((szmzizndt0 (sdtlpdtrp0 (xN) (xi))) = (szmzizndt0 (sdtlpdtrp0 (xN) (xj))))))))))). % 0.42/0.61 Proof. % 0.42/0.61 assert (zenon_L1_ : ((aElementOf0 (szmzizndt0 (sdtlpdtrp0 (xN) (xj))) (sdtlpdtrp0 (xN) (xj)))/\((forall W1 : zenon_U, ((aElementOf0 W1 (sdtlpdtrp0 (xN) (xj)))->(sdtlseqdt0 (szmzizndt0 (sdtlpdtrp0 (xN) (xj))) W1)))/\((aSet0 (sdtmndt0 (sdtlpdtrp0 (xN) (xj)) (szmzizndt0 (sdtlpdtrp0 (xN) (xj)))))/\((forall W1 : zenon_U, ((aElementOf0 W1 (sdtmndt0 (sdtlpdtrp0 (xN) (xj)) (szmzizndt0 (sdtlpdtrp0 (xN) (xj)))))<->((aElement0 W1)/\((aElementOf0 W1 (sdtlpdtrp0 (xN) (xj)))/\(~(W1 = (szmzizndt0 (sdtlpdtrp0 (xN) (xj)))))))))/\((forall W2 : zenon_U, ((aElementOf0 W2 (sdtlpdtrp0 (xN) (xi)))->(aElementOf0 W2 (sdtmndt0 (sdtlpdtrp0 (xN) (xj)) (szmzizndt0 (sdtlpdtrp0 (xN) (xj)))))))/\((aSubsetOf0 (sdtlpdtrp0 (xN) (xi)) (sdtmndt0 (sdtlpdtrp0 (xN) (xj)) (szmzizndt0 (sdtlpdtrp0 (xN) (xj)))))/\(~(((aElementOf0 (szmzizndt0 (sdtlpdtrp0 (xN) (xi))) (sdtlpdtrp0 (xN) (xi)))/\(forall W0 : zenon_U, ((aElementOf0 W0 (sdtlpdtrp0 (xN) (xi)))->(sdtlseqdt0 (szmzizndt0 (sdtlpdtrp0 (xN) (xi))) W0))))->(((aElementOf0 (szmzizndt0 (sdtlpdtrp0 (xN) (xi))) (sdtlpdtrp0 (xN) (xj)))/\(forall W0 : zenon_U, ((aElementOf0 W0 (sdtlpdtrp0 (xN) (xj)))->(sdtlseqdt0 (szmzizndt0 (sdtlpdtrp0 (xN) (xi))) W0))))\/((szmzizndt0 (sdtlpdtrp0 (xN) (xi))) = (szmzizndt0 (sdtlpdtrp0 (xN) (xj))))))))))))) -> ((szmzizndt0 (sdtlpdtrp0 (xN) (xi))) = (szmzizndt0 (sdtlpdtrp0 (xN) (xj)))) -> False). % 0.42/0.61 do 0 intro. intros zenon_H55 zenon_H56. % 0.42/0.61 apply (zenon_and_s _ _ zenon_H55). zenon_intro zenon_H58. zenon_intro zenon_H57. % 0.42/0.61 apply (zenon_and_s _ _ zenon_H57). zenon_intro zenon_H5a. zenon_intro zenon_H59. % 0.42/0.61 apply (zenon_and_s _ _ zenon_H59). zenon_intro zenon_H5c. zenon_intro zenon_H5b. % 0.42/0.61 apply (zenon_and_s _ _ zenon_H5b). zenon_intro zenon_H5e. zenon_intro zenon_H5d. % 0.42/0.61 apply (zenon_and_s _ _ zenon_H5d). zenon_intro zenon_H60. zenon_intro zenon_H5f. % 0.42/0.61 apply (zenon_and_s _ _ zenon_H5f). zenon_intro zenon_H62. zenon_intro zenon_H61. % 0.42/0.61 apply (zenon_notimply_s _ _ zenon_H61). zenon_intro zenon_H64. zenon_intro zenon_H63. % 0.42/0.61 apply (zenon_notor_s _ _ zenon_H63). zenon_intro zenon_H66. zenon_intro zenon_H65. % 0.42/0.61 exact (zenon_H65 zenon_H56). % 0.42/0.61 (* end of lemma zenon_L1_ *) % 0.42/0.61 apply NNPP. intro zenon_G. % 0.42/0.61 apply (zenon_and_s _ _ m__3856). zenon_intro zenon_H68. zenon_intro zenon_H67. % 0.42/0.62 apply (zenon_notimply_s _ _ zenon_G). zenon_intro zenon_H6a. zenon_intro zenon_H69. % 0.42/0.62 apply (zenon_notimply_s _ _ zenon_H69). zenon_intro zenon_H6c. zenon_intro zenon_H6b. % 0.42/0.62 apply zenon_H6b. zenon_intro zenon_H6d. % 0.42/0.62 apply (zenon_and_s _ _ zenon_H6d). zenon_intro zenon_H6f. zenon_intro zenon_H6e. % 0.42/0.62 apply (zenon_and_s _ _ zenon_H6e). zenon_intro zenon_H71. zenon_intro zenon_H70. % 0.42/0.62 apply (zenon_and_s _ _ zenon_H70). zenon_intro zenon_H73. zenon_intro zenon_H72. % 0.42/0.62 apply (zenon_and_s _ _ zenon_H72). zenon_intro zenon_H74. zenon_intro zenon_H56. % 0.42/0.62 apply (zenon_imply_s _ _ m__3856_02); [ zenon_intro zenon_H76 | zenon_intro zenon_H75 ]. % 0.42/0.62 exact (zenon_H76 zenon_H6c). % 0.42/0.62 apply (zenon_or_s _ _ zenon_H75); [ zenon_intro zenon_H78 | zenon_intro zenon_H77 ]. % 0.42/0.62 generalize (zenon_H6a (xj)). zenon_intro zenon_H79. % 0.42/0.62 generalize (zenon_H79 (xi)). zenon_intro zenon_H7a. % 0.42/0.62 apply (zenon_imply_s _ _ zenon_H7a); [ zenon_intro zenon_H7c | zenon_intro zenon_H7b ]. % 0.42/0.62 apply (zenon_notand_s _ _ zenon_H7c); [ zenon_intro zenon_H7e | zenon_intro zenon_H7d ]. % 0.42/0.62 exact (zenon_H7e zenon_H67). % 0.42/0.62 exact (zenon_H7d zenon_H68). % 0.42/0.62 apply (zenon_imply_s _ _ zenon_H7b); [ zenon_intro zenon_H7f | zenon_intro zenon_H55 ]. % 0.42/0.62 exact (zenon_H7f zenon_H78). % 0.42/0.62 apply (zenon_L1_); trivial. % 0.42/0.62 generalize (zenon_H6a (xi)). zenon_intro zenon_H80. % 0.42/0.62 generalize (zenon_H80 (xj)). zenon_intro zenon_H81. % 0.42/0.62 apply (zenon_imply_s _ _ zenon_H81); [ zenon_intro zenon_H83 | zenon_intro zenon_H82 ]. % 0.42/0.62 apply (zenon_notand_s _ _ zenon_H83); [ zenon_intro zenon_H7d | zenon_intro zenon_H7e ]. % 0.42/0.62 exact (zenon_H7d zenon_H68). % 0.42/0.62 exact (zenon_H7e zenon_H67). % 0.42/0.62 apply (zenon_imply_s _ _ zenon_H82); [ zenon_intro zenon_H85 | zenon_intro zenon_H84 ]. % 0.42/0.62 exact (zenon_H85 zenon_H77). % 0.42/0.62 apply (zenon_and_s _ _ zenon_H84). zenon_intro zenon_H6f. zenon_intro zenon_H86. % 0.42/0.62 apply (zenon_and_s _ _ zenon_H86). zenon_intro zenon_H71. zenon_intro zenon_H87. % 0.42/0.62 apply (zenon_and_s _ _ zenon_H87). zenon_intro zenon_H89. zenon_intro zenon_H88. % 0.42/0.62 apply (zenon_and_s _ _ zenon_H88). zenon_intro zenon_H8b. zenon_intro zenon_H8a. % 0.42/0.62 apply (zenon_and_s _ _ zenon_H8a). zenon_intro zenon_H8d. zenon_intro zenon_H8c. % 0.42/0.62 apply (zenon_and_s _ _ zenon_H8c). zenon_intro zenon_H8f. zenon_intro zenon_H8e. % 0.42/0.62 apply (zenon_notimply_s _ _ zenon_H8e). zenon_intro zenon_H91. zenon_intro zenon_H90. % 0.42/0.62 apply (zenon_notor_s _ _ zenon_H90). zenon_intro zenon_H93. zenon_intro zenon_H92. % 0.42/0.62 apply zenon_H92. apply sym_equal. exact zenon_H56. % 0.42/0.62 Qed. % 0.42/0.62 % SZS output end Proof % 0.42/0.62 (* END-PROOF *) % 0.42/0.62 nodes searched: 2754 % 0.42/0.62 max branch formulas: 1214 % 0.42/0.62 proof nodes created: 82 % 0.42/0.62 formulas created: 21624 % 0.42/0.62 %------------------------------------------------------------------------------