%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : HWV089+1 : TPTP v8.1.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n019.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:09 EDT 2022 % Result : Theorem 1.03s 1.20s % Output : Proof 1.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : HWV089+1 : TPTP v8.1.0. Released v6.1.0. % 0.04/0.13 % Command : run_zenon %s %d % 0.13/0.33 % Computer : n019.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Thu Jun 16 22:21:09 EDT 2022 % 0.13/0.34 % CPUTime : % 1.03/1.20 (* PROOF-FOUND *) % 1.03/1.20 % SZS status Theorem % 1.03/1.20 (* BEGIN-PROOF *) % 1.03/1.20 % SZS output start Proof % 1.03/1.20 Theorem addAssertion : (forall VarCurr : zenon_U, ((reachableState VarCurr)->(v4 VarCurr))). % 1.03/1.20 Proof. % 1.03/1.20 apply NNPP. intro zenon_G. % 1.03/1.20 apply (zenon_notallex_s (fun VarCurr : zenon_U => ((reachableState VarCurr)->(v4 VarCurr))) zenon_G); [ zenon_intro zenon_H185b; idtac ]. % 1.03/1.20 elim zenon_H185b. zenon_intro zenon_TVarCurr_jfw. zenon_intro zenon_H185d. % 1.03/1.20 apply (zenon_notimply_s _ _ zenon_H185d). zenon_intro zenon_H185f. zenon_intro zenon_H185e. % 1.03/1.20 generalize (writeUnaryOperator_346 zenon_TVarCurr_jfw). zenon_intro zenon_H1860. % 1.03/1.20 apply (zenon_equiv_s _ _ zenon_H1860); [ zenon_intro zenon_H1864; zenon_intro zenon_H1863 | zenon_intro zenon_H1862; zenon_intro zenon_H1861 ]. % 1.03/1.20 generalize (writeBinaryOperatorEqualRangesSingleBits_740 zenon_TVarCurr_jfw). zenon_intro zenon_H1865. % 1.03/1.20 apply (zenon_equiv_s _ _ zenon_H1865); [ zenon_intro zenon_H1863; zenon_intro zenon_H1867 | zenon_intro zenon_H1861; zenon_intro zenon_H1866 ]. % 1.03/1.20 apply (zenon_notand_s _ _ zenon_H1867); [ zenon_intro zenon_H1869 | zenon_intro zenon_H1868 ]. % 1.03/1.20 generalize (writeUnaryOperator_345 zenon_TVarCurr_jfw). zenon_intro zenon_H186a. % 1.03/1.20 apply (zenon_equiv_s _ _ zenon_H186a); [ zenon_intro zenon_H186d; zenon_intro zenon_H186c | zenon_intro zenon_H1869; zenon_intro zenon_H186b ]. % 1.03/1.20 exact (zenon_H186d zenon_H1869). % 1.03/1.20 generalize (writeBinaryOperatorShiftedRanges_554 zenon_TVarCurr_jfw). zenon_intro zenon_H186e. % 1.03/1.20 apply (zenon_equiv_s _ _ zenon_H186e); [ zenon_intro zenon_H186c; zenon_intro zenon_H1870 | zenon_intro zenon_H186b; zenon_intro zenon_H186f ]. % 1.03/1.20 exact (zenon_H186c zenon_H186b). % 1.03/1.20 apply (zenon_and_s _ _ zenon_H186f). zenon_intro zenon_H1872. zenon_intro zenon_H1871. % 1.03/1.20 generalize (addAssignment_2619 zenon_TVarCurr_jfw). zenon_intro zenon_H1873. % 1.03/1.20 apply (zenon_equiv_s _ _ zenon_H1873); [ zenon_intro zenon_H1876; zenon_intro zenon_H1875 | zenon_intro zenon_H1872; zenon_intro zenon_H1874 ]. % 1.03/1.20 exact (zenon_H1876 zenon_H1872). % 1.03/1.20 generalize (writeBinaryOperatorShiftedRanges_553 zenon_TVarCurr_jfw). zenon_intro zenon_H1877. % 1.03/1.20 apply (zenon_equiv_s _ _ zenon_H1877); [ zenon_intro zenon_H1875; zenon_intro zenon_H1879 | zenon_intro zenon_H1874; zenon_intro zenon_H1878 ]. % 1.03/1.20 exact (zenon_H1875 zenon_H1874). % 1.03/1.20 apply (zenon_and_s _ _ zenon_H1878). zenon_intro zenon_H187b. zenon_intro zenon_H187a. % 1.03/1.20 generalize (addZeroExtensionConstraint_5 zenon_TVarCurr_jfw). zenon_intro zenon_H187c. % 1.03/1.20 exact (zenon_H187c zenon_H187a). % 1.03/1.20 generalize (writeBinaryOperatorShiftedRanges_555 zenon_TVarCurr_jfw). zenon_intro zenon_H187d. % 1.03/1.20 apply (zenon_equiv_s _ _ zenon_H187d); [ zenon_intro zenon_H1868; zenon_intro zenon_H1880 | zenon_intro zenon_H187f; zenon_intro zenon_H187e ]. % 1.03/1.20 apply (zenon_notor_s _ _ zenon_H1880). zenon_intro zenon_H1876. zenon_intro zenon_H1881. % 1.03/1.20 generalize (addAssignment_2618 zenon_TVarCurr_jfw). zenon_intro zenon_H1882. % 1.03/1.20 apply (zenon_equiv_s _ _ zenon_H1882); [ zenon_intro zenon_H1881; zenon_intro zenon_H1884 | zenon_intro zenon_H1871; zenon_intro zenon_H1883 ]. % 1.03/1.20 exact (zenon_H1884 I). % 1.03/1.20 exact (zenon_H1881 zenon_H1871). % 1.03/1.20 exact (zenon_H1868 zenon_H187f). % 1.03/1.20 exact (zenon_H1863 zenon_H1861). % 1.03/1.20 generalize (writeUnaryOperator_347 zenon_TVarCurr_jfw). zenon_intro zenon_H1885. % 1.03/1.20 apply (zenon_equiv_s _ _ zenon_H1885); [ zenon_intro zenon_H1887; zenon_intro zenon_H1862 | zenon_intro zenon_H185e; zenon_intro zenon_H1886 ]. % 1.03/1.20 exact (zenon_H1887 zenon_H185e). % 1.03/1.20 exact (zenon_H1862 zenon_H1886). % 1.03/1.20 Qed. % 1.03/1.20 % SZS output end Proof % 1.03/1.20 (* END-PROOF *) % 1.03/1.20 nodes searched: 22349 % 1.03/1.20 max branch formulas: 29311 % 1.03/1.20 proof nodes created: 442 % 1.03/1.20 formulas created: 195072 % 1.03/1.20 %------------------------------------------------------------------------------