%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : HWV091+1 : TPTP v8.1.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n029.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:11 EDT 2022 % Result : Theorem 9.46s 9.64s % Output : Proof 9.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.15 % Problem : HWV091+1 : TPTP v8.1.0. Released v6.1.0. % 0.10/0.17 % Command : run_zenon %s %d % 0.16/0.38 % Computer : n029.cluster.edu % 0.16/0.38 % Model : x86_64 x86_64 % 0.16/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.38 % Memory : 8042.1875MB % 0.16/0.38 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.38 % CPULimit : 300 % 0.16/0.38 % WCLimit : 600 % 0.16/0.38 % DateTime : Fri Jun 17 07:25:58 EDT 2022 % 0.16/0.38 % CPUTime : % 9.46/9.64 (* PROOF-FOUND *) % 9.46/9.64 % SZS status Theorem % 9.46/9.64 (* BEGIN-PROOF *) % 9.46/9.64 % SZS output start Proof % 9.46/9.64 Theorem addAssertion : (forall VarCurr : zenon_U, ((reachableState VarCurr)->(v4 VarCurr))). % 9.46/9.64 Proof. % 9.46/9.64 apply NNPP. intro zenon_G. % 9.46/9.64 apply (zenon_notallex_s (fun VarCurr : zenon_U => ((reachableState VarCurr)->(v4 VarCurr))) zenon_G); [ zenon_intro zenon_H6839; idtac ]. % 9.46/9.64 elim zenon_H6839. zenon_intro zenon_TVarCurr_bnmg. zenon_intro zenon_H683b. % 9.46/9.64 apply (zenon_notimply_s _ _ zenon_H683b). zenon_intro zenon_H683d. zenon_intro zenon_H683c. % 9.46/9.64 generalize (writeUnaryOperator_2752 zenon_TVarCurr_bnmg). zenon_intro zenon_H683e. % 9.46/9.64 apply (zenon_equiv_s _ _ zenon_H683e); [ zenon_intro zenon_H6842; zenon_intro zenon_H6841 | zenon_intro zenon_H6840; zenon_intro zenon_H683f ]. % 9.46/9.64 generalize (writeBinaryOperatorEqualRangesSingleBits_5375 zenon_TVarCurr_bnmg). zenon_intro zenon_H6843. % 9.46/9.64 apply (zenon_equiv_s _ _ zenon_H6843); [ zenon_intro zenon_H6841; zenon_intro zenon_H6845 | zenon_intro zenon_H683f; zenon_intro zenon_H6844 ]. % 9.46/9.64 apply (zenon_notand_s _ _ zenon_H6845); [ zenon_intro zenon_H6847 | zenon_intro zenon_H6846 ]. % 9.46/9.64 generalize (writeUnaryOperator_2751 zenon_TVarCurr_bnmg). zenon_intro zenon_H6848. % 9.46/9.64 apply (zenon_equiv_s _ _ zenon_H6848); [ zenon_intro zenon_H684b; zenon_intro zenon_H684a | zenon_intro zenon_H6847; zenon_intro zenon_H6849 ]. % 9.46/9.64 exact (zenon_H684b zenon_H6847). % 9.46/9.64 generalize (writeBinaryOperatorShiftedRanges_1474 zenon_TVarCurr_bnmg). zenon_intro zenon_H684c. % 9.46/9.64 apply (zenon_equiv_s _ _ zenon_H684c); [ zenon_intro zenon_H684a; zenon_intro zenon_H684e | zenon_intro zenon_H6849; zenon_intro zenon_H684d ]. % 9.46/9.64 exact (zenon_H684a zenon_H6849). % 9.46/9.64 apply (zenon_and_s _ _ zenon_H684d). zenon_intro zenon_H6850. zenon_intro zenon_H684f. % 9.46/9.64 generalize (addAssignment_8257 zenon_TVarCurr_bnmg). zenon_intro zenon_H6851. % 9.46/9.64 apply (zenon_equiv_s _ _ zenon_H6851); [ zenon_intro zenon_H6854; zenon_intro zenon_H6853 | zenon_intro zenon_H6850; zenon_intro zenon_H6852 ]. % 9.46/9.64 exact (zenon_H6854 zenon_H6850). % 9.46/9.64 generalize (writeBinaryOperatorShiftedRanges_1473 zenon_TVarCurr_bnmg). zenon_intro zenon_H6855. % 9.46/9.64 apply (zenon_equiv_s _ _ zenon_H6855); [ zenon_intro zenon_H6853; zenon_intro zenon_H6857 | zenon_intro zenon_H6852; zenon_intro zenon_H6856 ]. % 9.46/9.64 exact (zenon_H6853 zenon_H6852). % 9.46/9.64 apply (zenon_and_s _ _ zenon_H6856). zenon_intro zenon_H6859. zenon_intro zenon_H6858. % 9.46/9.64 generalize (addZeroExtensionConstraint_8 zenon_TVarCurr_bnmg). zenon_intro zenon_H685a. % 9.46/9.64 exact (zenon_H685a zenon_H6858). % 9.46/9.64 generalize (writeBinaryOperatorShiftedRanges_1475 zenon_TVarCurr_bnmg). zenon_intro zenon_H685b. % 9.46/9.64 apply (zenon_equiv_s _ _ zenon_H685b); [ zenon_intro zenon_H6846; zenon_intro zenon_H685e | zenon_intro zenon_H685d; zenon_intro zenon_H685c ]. % 9.46/9.64 apply (zenon_notor_s _ _ zenon_H685e). zenon_intro zenon_H6854. zenon_intro zenon_H685f. % 9.46/9.64 generalize (addAssignment_8256 zenon_TVarCurr_bnmg). zenon_intro zenon_H6860. % 9.46/9.64 apply (zenon_equiv_s _ _ zenon_H6860); [ zenon_intro zenon_H685f; zenon_intro zenon_H6862 | zenon_intro zenon_H684f; zenon_intro zenon_H6861 ]. % 9.46/9.64 exact (zenon_H6862 I). % 9.46/9.64 exact (zenon_H685f zenon_H684f). % 9.46/9.64 exact (zenon_H6846 zenon_H685d). % 9.46/9.64 exact (zenon_H6841 zenon_H683f). % 9.46/9.64 generalize (writeUnaryOperator_2753 zenon_TVarCurr_bnmg). zenon_intro zenon_H6863. % 9.46/9.64 apply (zenon_equiv_s _ _ zenon_H6863); [ zenon_intro zenon_H6865; zenon_intro zenon_H6840 | zenon_intro zenon_H683c; zenon_intro zenon_H6864 ]. % 9.46/9.64 exact (zenon_H6865 zenon_H683c). % 9.46/9.64 exact (zenon_H6840 zenon_H6864). % 9.46/9.64 Qed. % 9.46/9.64 % SZS output end Proof % 9.46/9.64 (* END-PROOF *) % 9.46/9.64 nodes searched: 114039 % 9.46/9.64 max branch formulas: 142534 % 9.46/9.64 proof nodes created: 3017 % 9.46/9.64 formulas created: 896119 % 9.46/9.64 %------------------------------------------------------------------------------