%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : HWV095+1 : TPTP v8.1.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n016.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 : Sat Jul 16 21:31:15 EDT 2022 % Result : Theorem 0.49s 0.66s % Output : Proof 0.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : HWV095+1 : TPTP v8.1.0. Released v6.1.0. % 0.03/0.13 % Command : run_zenon %s %d % 0.13/0.34 % Computer : n016.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 : Fri Jun 17 10:09:20 EDT 2022 % 0.13/0.34 % CPUTime : % 0.49/0.66 (* PROOF-FOUND *) % 0.49/0.66 % SZS status Theorem % 0.49/0.66 (* BEGIN-PROOF *) % 0.49/0.66 % SZS output start Proof % 0.49/0.66 Theorem addAssertion : (forall VarCurr : zenon_U, ((reachableState VarCurr)->(v4 VarCurr))). % 0.49/0.66 Proof. % 0.49/0.66 apply NNPP. intro zenon_G. % 0.49/0.66 apply (zenon_notallex_s (fun VarCurr : zenon_U => ((reachableState VarCurr)->(v4 VarCurr))) zenon_G); [ zenon_intro zenon_H484; idtac ]. % 0.49/0.66 elim zenon_H484. zenon_intro zenon_TVarCurr_bsn. zenon_intro zenon_H486. % 0.49/0.66 apply (zenon_notimply_s _ _ zenon_H486). zenon_intro zenon_H488. zenon_intro zenon_H487. % 0.49/0.66 generalize (writeUnaryOperator_112 zenon_TVarCurr_bsn). zenon_intro zenon_H489. % 0.49/0.66 apply (zenon_equiv_s _ _ zenon_H489); [ zenon_intro zenon_H48d; zenon_intro zenon_H48c | zenon_intro zenon_H48b; zenon_intro zenon_H48a ]. % 0.49/0.66 generalize (writeBinaryOperatorEqualRangesSingleBits_170 zenon_TVarCurr_bsn). zenon_intro zenon_H48e. % 0.49/0.66 apply (zenon_equiv_s _ _ zenon_H48e); [ zenon_intro zenon_H48c; zenon_intro zenon_H490 | zenon_intro zenon_H48a; zenon_intro zenon_H48f ]. % 0.49/0.66 apply (zenon_notand_s _ _ zenon_H490); [ zenon_intro zenon_H492 | zenon_intro zenon_H491 ]. % 0.49/0.66 generalize (writeUnaryOperator_111 zenon_TVarCurr_bsn). zenon_intro zenon_H493. % 0.49/0.66 apply (zenon_equiv_s _ _ zenon_H493); [ zenon_intro zenon_H496; zenon_intro zenon_H495 | zenon_intro zenon_H492; zenon_intro zenon_H494 ]. % 0.49/0.66 exact (zenon_H496 zenon_H492). % 0.49/0.66 generalize (writeBinaryOperatorShiftedRanges_79 zenon_TVarCurr_bsn). zenon_intro zenon_H497. % 0.49/0.66 apply (zenon_equiv_s _ _ zenon_H497); [ zenon_intro zenon_H495; zenon_intro zenon_H499 | zenon_intro zenon_H494; zenon_intro zenon_H498 ]. % 0.49/0.66 exact (zenon_H495 zenon_H494). % 0.49/0.66 apply (zenon_and_s _ _ zenon_H498). zenon_intro zenon_H49b. zenon_intro zenon_H49a. % 0.49/0.66 generalize (addAssignment_245 zenon_TVarCurr_bsn). zenon_intro zenon_H49c. % 0.49/0.66 apply (zenon_equiv_s _ _ zenon_H49c); [ zenon_intro zenon_H49f; zenon_intro zenon_H49e | zenon_intro zenon_H49b; zenon_intro zenon_H49d ]. % 0.49/0.66 exact (zenon_H49f zenon_H49b). % 0.49/0.66 generalize (writeBinaryOperatorShiftedRanges_78 zenon_TVarCurr_bsn). zenon_intro zenon_H4a0. % 0.49/0.66 apply (zenon_equiv_s _ _ zenon_H4a0); [ zenon_intro zenon_H49e; zenon_intro zenon_H4a2 | zenon_intro zenon_H49d; zenon_intro zenon_H4a1 ]. % 0.49/0.66 exact (zenon_H49e zenon_H49d). % 0.49/0.66 apply (zenon_and_s _ _ zenon_H4a1). zenon_intro zenon_H4a4. zenon_intro zenon_H4a3. % 0.49/0.66 generalize (addZeroExtensionConstraint_3 zenon_TVarCurr_bsn). zenon_intro zenon_H4a5. % 0.49/0.66 exact (zenon_H4a5 zenon_H4a3). % 0.49/0.66 generalize (writeBinaryOperatorShiftedRanges_80 zenon_TVarCurr_bsn). zenon_intro zenon_H4a6. % 0.49/0.66 apply (zenon_equiv_s _ _ zenon_H4a6); [ zenon_intro zenon_H491; zenon_intro zenon_H4a9 | zenon_intro zenon_H4a8; zenon_intro zenon_H4a7 ]. % 0.49/0.66 apply (zenon_notor_s _ _ zenon_H4a9). zenon_intro zenon_H49f. zenon_intro zenon_H4aa. % 0.49/0.66 generalize (addAssignment_244 zenon_TVarCurr_bsn). zenon_intro zenon_H4ab. % 0.49/0.66 apply (zenon_equiv_s _ _ zenon_H4ab); [ zenon_intro zenon_H4aa; zenon_intro zenon_H4ad | zenon_intro zenon_H49a; zenon_intro zenon_H4ac ]. % 0.49/0.66 exact (zenon_H4ad I). % 0.49/0.66 exact (zenon_H4aa zenon_H49a). % 0.49/0.66 exact (zenon_H491 zenon_H4a8). % 0.49/0.66 exact (zenon_H48c zenon_H48a). % 0.49/0.66 generalize (writeUnaryOperator_113 zenon_TVarCurr_bsn). zenon_intro zenon_H4ae. % 0.49/0.66 apply (zenon_equiv_s _ _ zenon_H4ae); [ zenon_intro zenon_H4b0; zenon_intro zenon_H48b | zenon_intro zenon_H487; zenon_intro zenon_H4af ]. % 0.49/0.66 exact (zenon_H4b0 zenon_H487). % 0.49/0.66 exact (zenon_H48b zenon_H4af). % 0.49/0.66 Qed. % 0.49/0.66 % SZS output end Proof % 0.49/0.66 (* END-PROOF *) % 0.49/0.66 nodes searched: 4731 % 0.49/0.66 max branch formulas: 6510 % 0.49/0.66 proof nodes created: 124 % 0.49/0.66 formulas created: 38771 % 0.49/0.66 %------------------------------------------------------------------------------