%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : HWV092+1 : TPTP v9.0.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n002.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 : 300s % DateTime : Mon Apr 14 09:10:31 AM UTC 2025 % Result : Theorem 246.57s 246.80s % Output : Proof 246.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.15 % Problem : HWV092+1 : TPTP v9.0.0. Released v6.1.0. % 0.12/0.22 % Command : run_zenon %s %d % 0.19/0.44 % Computer : n002.cluster.edu % 0.19/0.44 % Model : x86_64 x86_64 % 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.19/0.44 % Memory : 8042.1875MB % 0.19/0.44 % OS : Linux 3.10.0-693.el7.x86_64 % 0.19/0.44 % CPULimit : 300 % 0.19/0.44 % WCLimit : 300 % 0.19/0.44 % DateTime : Sun Apr 13 23:31:06 EDT 2025 % 0.19/0.44 % CPUTime : % 246.57/246.80 (* PROOF-FOUND *) % 246.57/246.80 % SZS status Theorem % 246.57/246.80 (* BEGIN-PROOF *) % 246.57/246.80 % SZS output start Proof % 246.57/246.80 Theorem addAssertion : (forall VarCurr : zenon_U, ((reachableState VarCurr)->(v4 VarCurr))). % 246.57/246.80 Proof. % 246.57/246.80 apply NNPP. intro zenon_G. % 246.57/246.80 apply (zenon_notallex_s (fun VarCurr : zenon_U => ((reachableState VarCurr)->(v4 VarCurr))) zenon_G); [ zenon_intro zenon_H15ccf; idtac ]. % 246.57/246.80 elim zenon_H15ccf. zenon_intro zenon_TVarCurr_fccm. zenon_intro zenon_H15cd1. % 246.57/246.80 apply (zenon_notimply_s _ _ zenon_H15cd1). zenon_intro zenon_H15cd3. zenon_intro zenon_H15cd2. % 246.57/246.80 generalize (writeUnaryOperator_6623 zenon_TVarCurr_fccm). zenon_intro zenon_H15cd4. % 246.57/246.80 apply (zenon_equiv_s _ _ zenon_H15cd4); [ zenon_intro zenon_H15cd8; zenon_intro zenon_H15cd7 | zenon_intro zenon_H15cd6; zenon_intro zenon_H15cd5 ]. % 246.57/246.80 generalize (writeBinaryOperatorEqualRangesSingleBits_13943 zenon_TVarCurr_fccm). zenon_intro zenon_H15cd9. % 246.57/246.80 apply (zenon_equiv_s _ _ zenon_H15cd9); [ zenon_intro zenon_H15cd7; zenon_intro zenon_H15cdb | zenon_intro zenon_H15cd5; zenon_intro zenon_H15cda ]. % 246.57/246.80 apply (zenon_notand_s _ _ zenon_H15cdb); [ zenon_intro zenon_H15cdd | zenon_intro zenon_H15cdc ]. % 246.57/246.80 generalize (writeUnaryOperator_6622 zenon_TVarCurr_fccm). zenon_intro zenon_H15cde. % 246.57/246.80 apply (zenon_equiv_s _ _ zenon_H15cde); [ zenon_intro zenon_H15ce1; zenon_intro zenon_H15ce0 | zenon_intro zenon_H15cdd; zenon_intro zenon_H15cdf ]. % 246.57/246.80 exact (zenon_H15ce1 zenon_H15cdd). % 246.57/246.80 generalize (writeBinaryOperatorShiftedRanges_3076 zenon_TVarCurr_fccm). zenon_intro zenon_H15ce2. % 246.57/246.80 apply (zenon_equiv_s _ _ zenon_H15ce2); [ zenon_intro zenon_H15ce0; zenon_intro zenon_H15ce4 | zenon_intro zenon_H15cdf; zenon_intro zenon_H15ce3 ]. % 246.57/246.80 exact (zenon_H15ce0 zenon_H15cdf). % 246.57/246.80 apply (zenon_and_s _ _ zenon_H15ce3). zenon_intro zenon_H15ce6. zenon_intro zenon_H15ce5. % 246.57/246.80 generalize (addAssignment_28826 zenon_TVarCurr_fccm). zenon_intro zenon_H15ce7. % 246.57/246.80 apply (zenon_equiv_s _ _ zenon_H15ce7); [ zenon_intro zenon_H15cea; zenon_intro zenon_H15ce9 | zenon_intro zenon_H15ce6; zenon_intro zenon_H15ce8 ]. % 246.57/246.80 exact (zenon_H15cea zenon_H15ce6). % 246.57/246.80 generalize (writeBinaryOperatorShiftedRanges_3075 zenon_TVarCurr_fccm). zenon_intro zenon_H15ceb. % 246.57/246.80 apply (zenon_equiv_s _ _ zenon_H15ceb); [ zenon_intro zenon_H15ce9; zenon_intro zenon_H15ced | zenon_intro zenon_H15ce8; zenon_intro zenon_H15cec ]. % 246.57/246.80 exact (zenon_H15ce9 zenon_H15ce8). % 246.57/246.80 apply (zenon_and_s _ _ zenon_H15cec). zenon_intro zenon_H15cef. zenon_intro zenon_H15cee. % 246.57/246.80 generalize (addZeroExtensionConstraint_44 zenon_TVarCurr_fccm). zenon_intro zenon_H15cf0. % 246.57/246.80 exact (zenon_H15cf0 zenon_H15cee). % 246.57/246.80 generalize (writeBinaryOperatorShiftedRanges_3077 zenon_TVarCurr_fccm). zenon_intro zenon_H15cf1. % 246.57/246.80 apply (zenon_equiv_s _ _ zenon_H15cf1); [ zenon_intro zenon_H15cdc; zenon_intro zenon_H15cf4 | zenon_intro zenon_H15cf3; zenon_intro zenon_H15cf2 ]. % 246.57/246.80 apply (zenon_notor_s _ _ zenon_H15cf4). zenon_intro zenon_H15cea. zenon_intro zenon_H15cf5. % 246.57/246.80 generalize (addAssignment_28825 zenon_TVarCurr_fccm). zenon_intro zenon_H15cf6. % 246.57/246.80 apply (zenon_equiv_s _ _ zenon_H15cf6); [ zenon_intro zenon_H15cf5; zenon_intro zenon_H15cf8 | zenon_intro zenon_H15ce5; zenon_intro zenon_H15cf7 ]. % 246.57/246.80 exact (zenon_H15cf8 I). % 246.57/246.80 exact (zenon_H15cf5 zenon_H15ce5). % 246.57/246.80 exact (zenon_H15cdc zenon_H15cf3). % 246.57/246.80 exact (zenon_H15cd7 zenon_H15cd5). % 246.57/246.80 generalize (writeUnaryOperator_6624 zenon_TVarCurr_fccm). zenon_intro zenon_H15cf9. % 246.57/246.80 apply (zenon_equiv_s _ _ zenon_H15cf9); [ zenon_intro zenon_H15cfb; zenon_intro zenon_H15cd6 | zenon_intro zenon_H15cd2; zenon_intro zenon_H15cfa ]. % 246.57/246.80 exact (zenon_H15cfb zenon_H15cd2). % 246.57/246.80 exact (zenon_H15cd6 zenon_H15cfa). % 246.57/246.80 Qed. % 246.57/246.80 % SZS output end Proof % 246.57/246.80 (* END-PROOF *) % 246.57/246.80 nodes searched: 15173321 % 246.57/246.80 max branch formulas: 1888827 % 246.57/246.80 proof nodes created: 12193 % 246.57/246.80 formulas created: 33962522 % 246.57/246.80 %------------------------------------------------------------------------------