%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : HWV096+1 : TPTP v9.0.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n001.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 258.69s 258.99s % Output : Proof 258.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : HWV096+1 : TPTP v9.0.0. Released v6.1.0. % 0.12/0.18 % Command : run_zenon %s %d % 0.17/0.38 % Computer : n001.cluster.edu % 0.17/0.38 % Model : x86_64 x86_64 % 0.17/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.38 % Memory : 8042.1875MB % 0.17/0.38 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.38 % CPULimit : 300 % 0.17/0.38 % WCLimit : 300 % 0.17/0.38 % DateTime : Sun Apr 13 23:33:34 EDT 2025 % 0.17/0.38 % CPUTime : % 258.69/258.99 (* PROOF-FOUND *) % 258.69/258.99 % SZS status Theorem % 258.69/258.99 (* BEGIN-PROOF *) % 258.69/258.99 % SZS output start Proof % 258.69/258.99 Theorem addAssertion : (forall VarCurr : zenon_U, ((reachableState VarCurr)->(v4 VarCurr))). % 258.69/258.99 Proof. % 258.69/258.99 apply NNPP. intro zenon_G. % 258.69/258.99 apply (zenon_notallex_s (fun VarCurr : zenon_U => ((reachableState VarCurr)->(v4 VarCurr))) zenon_G); [ zenon_intro zenon_H20df1; idtac ]. % 258.69/258.99 elim zenon_H20df1. zenon_intro zenon_TVarCurr_hreo. zenon_intro zenon_H20df3. % 258.69/258.99 apply (zenon_notimply_s _ _ zenon_H20df3). zenon_intro zenon_H20df5. zenon_intro zenon_H20df4. % 258.69/258.99 generalize (writeUnaryOperator_11137 zenon_TVarCurr_hreo). zenon_intro zenon_H20df6. % 258.69/258.99 apply (zenon_equiv_s _ _ zenon_H20df6); [ zenon_intro zenon_H20dfa; zenon_intro zenon_H20df9 | zenon_intro zenon_H20df8; zenon_intro zenon_H20df7 ]. % 258.69/258.99 generalize (writeBinaryOperatorEqualRangesSingleBits_26827 zenon_TVarCurr_hreo). zenon_intro zenon_H20dfb. % 258.69/258.99 apply (zenon_equiv_s _ _ zenon_H20dfb); [ zenon_intro zenon_H20df9; zenon_intro zenon_H20dfd | zenon_intro zenon_H20df7; zenon_intro zenon_H20dfc ]. % 258.69/258.99 apply (zenon_notand_s _ _ zenon_H20dfd); [ zenon_intro zenon_H20dff | zenon_intro zenon_H20dfe ]. % 258.69/258.99 generalize (writeUnaryOperator_11136 zenon_TVarCurr_hreo). zenon_intro zenon_H20e00. % 258.69/258.99 apply (zenon_equiv_s _ _ zenon_H20e00); [ zenon_intro zenon_H20e03; zenon_intro zenon_H20e02 | zenon_intro zenon_H20dff; zenon_intro zenon_H20e01 ]. % 258.69/258.99 exact (zenon_H20e03 zenon_H20dff). % 258.69/258.99 generalize (writeBinaryOperatorShiftedRanges_3136 zenon_TVarCurr_hreo). zenon_intro zenon_H20e04. % 258.69/258.99 apply (zenon_equiv_s _ _ zenon_H20e04); [ zenon_intro zenon_H20e02; zenon_intro zenon_H20e06 | zenon_intro zenon_H20e01; zenon_intro zenon_H20e05 ]. % 258.69/258.99 exact (zenon_H20e02 zenon_H20e01). % 258.69/258.99 apply (zenon_and_s _ _ zenon_H20e05). zenon_intro zenon_H20e08. zenon_intro zenon_H20e07. % 258.69/258.99 generalize (addAssignment_43639 zenon_TVarCurr_hreo). zenon_intro zenon_H20e09. % 258.69/258.99 apply (zenon_equiv_s _ _ zenon_H20e09); [ zenon_intro zenon_H20e0c; zenon_intro zenon_H20e0b | zenon_intro zenon_H20e08; zenon_intro zenon_H20e0a ]. % 258.69/258.99 exact (zenon_H20e0c zenon_H20e08). % 258.69/258.99 generalize (writeBinaryOperatorShiftedRanges_3135 zenon_TVarCurr_hreo). zenon_intro zenon_H20e0d. % 258.69/258.99 apply (zenon_equiv_s _ _ zenon_H20e0d); [ zenon_intro zenon_H20e0b; zenon_intro zenon_H20e0f | zenon_intro zenon_H20e0a; zenon_intro zenon_H20e0e ]. % 258.69/258.99 exact (zenon_H20e0b zenon_H20e0a). % 258.69/258.99 apply (zenon_and_s _ _ zenon_H20e0e). zenon_intro zenon_H20e11. zenon_intro zenon_H20e10. % 258.69/258.99 generalize (addZeroExtensionConstraint_15 zenon_TVarCurr_hreo). zenon_intro zenon_H20e12. % 258.69/258.99 exact (zenon_H20e12 zenon_H20e10). % 258.69/258.99 generalize (writeBinaryOperatorShiftedRanges_3137 zenon_TVarCurr_hreo). zenon_intro zenon_H20e13. % 258.69/258.99 apply (zenon_equiv_s _ _ zenon_H20e13); [ zenon_intro zenon_H20dfe; zenon_intro zenon_H20e16 | zenon_intro zenon_H20e15; zenon_intro zenon_H20e14 ]. % 258.69/258.99 apply (zenon_notor_s _ _ zenon_H20e16). zenon_intro zenon_H20e0c. zenon_intro zenon_H20e17. % 258.69/258.99 generalize (addAssignment_43638 zenon_TVarCurr_hreo). zenon_intro zenon_H20e18. % 258.69/258.99 apply (zenon_equiv_s _ _ zenon_H20e18); [ zenon_intro zenon_H20e17; zenon_intro zenon_H20e1a | zenon_intro zenon_H20e07; zenon_intro zenon_H20e19 ]. % 258.69/258.99 exact (zenon_H20e1a I). % 258.69/258.99 exact (zenon_H20e17 zenon_H20e07). % 258.69/258.99 exact (zenon_H20dfe zenon_H20e15). % 258.69/258.99 exact (zenon_H20df9 zenon_H20df7). % 258.69/258.99 generalize (writeUnaryOperator_11138 zenon_TVarCurr_hreo). zenon_intro zenon_H20e1b. % 258.69/258.99 apply (zenon_equiv_s _ _ zenon_H20e1b); [ zenon_intro zenon_H20e1d; zenon_intro zenon_H20df8 | zenon_intro zenon_H20df4; zenon_intro zenon_H20e1c ]. % 258.69/258.99 exact (zenon_H20e1d zenon_H20df4). % 258.69/258.99 exact (zenon_H20df8 zenon_H20e1c). % 258.69/258.99 Qed. % 258.69/258.99 % SZS output end Proof % 258.69/258.99 (* END-PROOF *) % 258.69/258.99 nodes searched: 1790390 % 258.69/258.99 max branch formulas: 1015148 % 258.69/258.99 proof nodes created: 26771 % 258.69/258.99 formulas created: 8172555 % 258.69/258.99 %------------------------------------------------------------------------------