%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : SWV093+1 : TPTP v9.2.1. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n027.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 : Wed Jun 3 09:00:30 AM UTC 2026 % Result : Theorem 0.39s 0.62s % Output : Proof 0.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.13 % Problem : SWV093+1 : TPTP v9.2.1. Bugfixed v3.3.0. % 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.16/0.35 % Computer : n027.cluster.edu % 0.16/0.35 % Model : x86_64 x86_64 % 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.35 % Memory : 8042.1875MB % 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.35 % CPULimit : 300 % 0.16/0.35 % WCLimit : 300 % 0.16/0.35 % DateTime : Tue Jun 2 19:55:06 EDT 2026 % 0.16/0.35 % CPUTime : % 0.32/0.51 %----Proving TF0_NAR, FOF, or CNF % 0.39/0.62 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 0.39/0.62 % SZS status Theorem % 0.39/0.62 % SZS output start Proof % 0.39/0.62 ( % 0.39/0.62 (declare-sort $$unsorted 0) % 0.39/0.62 (declare-const tptp.pv41 $$unsorted) % 0.39/0.62 (declare-const tptp.n6 $$unsorted) % 0.39/0.62 (declare-const tptp.rho_defuse $$unsorted) % 0.39/0.62 (declare-const tptp.xinit_defuse $$unsorted) % 0.39/0.62 (declare-const tptp.xinit_mean_defuse $$unsorted) % 0.39/0.62 (declare-const tptp.n999 $$unsorted) % 0.39/0.62 (declare-const tptp.def $$unsorted) % 0.39/0.62 (declare-const tptp.use $$unsorted) % 0.39/0.62 (declare-const tptp.true Bool) % 0.39/0.62 (declare-const tptp.tptp_update2 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.pv5 $$unsorted) % 0.39/0.62 (declare-const tptp.a_select3 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.gt (-> $$unsorted $$unsorted Bool)) % 0.39/0.62 (declare-const tptp.uniform_int_rnd (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.u_defuse $$unsorted) % 0.39/0.62 (declare-const tptp.n3 $$unsorted) % 0.39/0.62 (declare-const tptp.tptp_const_array1 (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.pred (-> $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.tptp_minus_1 $$unsorted) % 0.39/0.62 (declare-const tptp.n0 $$unsorted) % 0.39/0.62 (declare-const tptp.tptp_msub (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.n1 $$unsorted) % 0.39/0.62 (declare-const tptp.succ (-> $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.n5 $$unsorted) % 0.39/0.62 (declare-const tptp.sigma_defuse $$unsorted) % 0.39/0.62 (declare-const tptp.lt (-> $$unsorted $$unsorted Bool)) % 0.39/0.62 (declare-const tptp.tptp_update3 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.minus (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.xinit_noise_defuse $$unsorted) % 0.39/0.62 (declare-const tptp.tptp_const_array2 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.geq (-> $$unsorted $$unsorted Bool)) % 0.39/0.62 (declare-const tptp.leq (-> $$unsorted $$unsorted Bool)) % 0.39/0.62 (declare-const tptp.trans (-> $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.a_select2 (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.inv (-> $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.dim (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.plus (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.tptp_madd (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.sum (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.tptp_mmul (-> $$unsorted $$unsorted $$unsorted)) % 0.39/0.62 (declare-const tptp.tptp_float_0_0 $$unsorted) % 0.39/0.62 (declare-const tptp.z_defuse $$unsorted) % 0.39/0.62 (declare-const tptp.n4 $$unsorted) % 0.39/0.62 (declare-const tptp.n2 $$unsorted) % 0.39/0.62 (define @t1 () (@var "Y" $$unsorted)) % 0.39/0.62 (define @t2 () (@var "X" $$unsorted)) % 0.39/0.62 (define @t3 () (= @t2 @t1)) % 0.39/0.62 (define @t4 () (tptp.gt @t1 @t2)) % 0.39/0.62 (define @t5 () (tptp.gt @t2 @t1)) % 0.39/0.62 (define @t6 () (@list @t2 @t1)) % 0.39/0.62 (define @t7 () (@var "Z" $$unsorted)) % 0.39/0.62 (define @t8 () (@list @t2 @t1 @t7)) % 0.39/0.62 (define @t9 () (@list @t2)) % 0.39/0.62 (define @t10 () (tptp.leq @t2 @t1)) % 0.39/0.62 (define @t11 () (tptp.succ @t2)) % 0.39/0.62 (define @t12 () (tptp.succ @t1)) % 0.39/0.62 (define @t13 () (@var "C" $$unsorted)) % 0.39/0.62 (define @t14 () (tptp.uniform_int_rnd @t13 @t2)) % 0.39/0.62 (define @t15 () (tptp.leq tptp.n0 @t2)) % 0.39/0.62 (define @t16 () (@list @t2 @t13)) % 0.39/0.62 (define @t17 () (@var "Val" $$unsorted)) % 0.39/0.62 (define @t18 () (@var "I" $$unsorted)) % 0.39/0.62 (define @t19 () (@var "U" $$unsorted)) % 0.39/0.62 (define @t20 () (@var "L" $$unsorted)) % 0.39/0.62 (define @t21 () (tptp.leq @t18 @t19)) % 0.39/0.62 (define @t22 () (@var "J" $$unsorted)) % 0.39/0.62 (define @t23 () (@var "U2" $$unsorted)) % 0.39/0.62 (define @t24 () (@var "L2" $$unsorted)) % 0.39/0.62 (define @t25 () (@var "U1" $$unsorted)) % 0.39/0.62 (define @t26 () (@var "L1" $$unsorted)) % 0.39/0.62 (define @t27 () (@var "A" $$unsorted)) % 0.39/0.62 (define @t28 () (tptp.trans @t27)) % 0.39/0.62 (define @t29 () (@var "N" $$unsorted)) % 0.39/0.62 (define @t30 () (tptp.leq @t22 @t29)) % 0.39/0.62 (define @t31 () (tptp.leq tptp.n0 @t22)) % 0.39/0.62 (define @t32 () (tptp.leq @t18 @t29)) % 0.39/0.62 (define @t33 () (tptp.leq tptp.n0 @t18)) % 0.39/0.62 (define @t34 () (and @t33 @t32 @t31 @t30)) % 0.39/0.62 (define @t35 () (@list @t18 @t22)) % 0.39/0.62 (define @t36 () (forall @t35 (=> @t34 (= (tptp.a_select3 @t27 @t18 @t22) (tptp.a_select3 @t27 @t22 @t18))))) % 0.39/0.62 (define @t37 () (@list @t27 @t29)) % 0.39/0.62 (define @t38 () (tptp.inv @t27)) % 0.39/0.62 (define @t39 () (@var "VAL" $$unsorted)) % 0.39/0.62 (define @t40 () (@var "K" $$unsorted)) % 0.39/0.62 (define @t41 () (tptp.tptp_update3 @t27 @t40 @t40 @t39)) % 0.39/0.62 (define @t42 () (@var "B" $$unsorted)) % 0.39/0.62 (define @t43 () (tptp.tptp_madd @t27 @t42)) % 0.39/0.62 (define @t44 () (= (tptp.a_select3 @t42 @t18 @t22) (tptp.a_select3 @t42 @t22 @t18))) % 0.39/0.62 (define @t45 () (forall @t35 (=> @t34 @t44))) % 0.39/0.62 (define @t46 () (and @t36 @t45)) % 0.39/0.62 (define @t47 () (@list @t27 @t42 @t29)) % 0.39/0.62 (define @t48 () (tptp.tptp_msub @t27 @t42)) % 0.39/0.62 (define @t49 () (tptp.tptp_mmul @t27 (tptp.tptp_mmul @t42 @t28))) % 0.39/0.62 (define @t50 () (forall @t35 (=> @t34 (= (tptp.a_select3 @t49 @t18 @t22) (tptp.a_select3 @t49 @t22 @t18))))) % 0.39/0.62 (define @t51 () (@var "M" $$unsorted)) % 0.39/0.62 (define @t52 () (and @t33 (tptp.leq @t18 @t51) @t31 (tptp.leq @t22 @t51))) % 0.39/0.62 (define @t53 () (@var "E" $$unsorted)) % 0.39/0.62 (define @t54 () (@var "F" $$unsorted)) % 0.39/0.62 (define @t55 () (@var "D" $$unsorted)) % 0.39/0.62 (define @t56 () (tptp.tptp_madd @t27 (tptp.tptp_mmul @t42 (tptp.tptp_mmul (tptp.tptp_madd (tptp.tptp_mmul @t13 (tptp.tptp_mmul @t55 (tptp.trans @t13))) (tptp.tptp_mmul @t53 (tptp.tptp_mmul @t54 (tptp.trans @t53)))) (tptp.trans @t42))))) % 0.39/0.62 (define @t57 () (@var "Body" $$unsorted)) % 0.39/0.62 (define @t58 () (tptp.sum tptp.n0 tptp.tptp_minus_1 @t57)) % 0.39/0.62 (define @t59 () (@list @t57)) % 0.39/0.62 (define @t60 () (tptp.succ @t11)) % 0.39/0.62 (define @t61 () (tptp.succ @t60)) % 0.39/0.62 (define @t62 () (tptp.succ @t61)) % 0.39/0.62 (define @t63 () (tptp.succ @t62)) % 0.39/0.62 (define @t64 () (tptp.pred @t2)) % 0.39/0.62 (define @t65 () (@var "V" $$unsorted)) % 0.39/0.62 (define @t66 () (tptp.tptp_update3 @t2 @t19 @t65 @t39)) % 0.39/0.62 (define @t67 () (@var "VAL2" $$unsorted)) % 0.39/0.62 (define @t68 () (not (= @t18 @t19))) % 0.39/0.62 (define @t69 () (@var "J0" $$unsorted)) % 0.39/0.62 (define @t70 () (@var "I0" $$unsorted)) % 0.39/0.62 (define @t71 () (tptp.leq @t70 @t19)) % 0.39/0.62 (define @t72 () (tptp.leq tptp.n0 @t70)) % 0.39/0.62 (define @t73 () (tptp.tptp_update2 @t2 @t19 @t39)) % 0.39/0.62 (define @t74 () (@var "H" $$unsorted)) % 0.39/0.62 (define @t75 () (@var "G" $$unsorted)) % 0.39/0.62 (define @t76 () (tptp.a_select3 tptp.z_defuse @t75 @t74)) % 0.39/0.62 (define @t77 () (tptp.a_select3 tptp.u_defuse @t75 @t74)) % 0.39/0.62 (define @t78 () (and (= @t77 tptp.use) (= @t76 tptp.use))) % 0.39/0.62 (define @t79 () (tptp.minus tptp.pv5 tptp.n1)) % 0.39/0.62 (define @t80 () (tptp.leq @t74 @t79)) % 0.39/0.62 (define @t81 () (tptp.leq @t75 tptp.n2)) % 0.39/0.62 (define @t82 () (tptp.leq tptp.n0 @t74)) % 0.39/0.62 (define @t83 () (tptp.leq tptp.n0 @t75)) % 0.39/0.62 (define @t84 () (and @t83 @t82 @t81 @t80)) % 0.39/0.62 (define @t85 () (=> @t84 @t78)) % 0.39/0.62 (define @t86 () (@list @t75 @t74)) % 0.39/0.62 (define @t87 () (forall @t86 @t85)) % 0.39/0.62 (define @t88 () (tptp.a_select3 tptp.z_defuse @t53 @t54)) % 0.39/0.62 (define @t89 () (tptp.a_select3 tptp.u_defuse @t53 @t54)) % 0.39/0.62 (define @t90 () (and (= @t89 tptp.use) (= @t88 tptp.use))) % 0.39/0.62 (define @t91 () (tptp.leq @t54 tptp.pv5)) % 0.39/0.62 (define @t92 () (tptp.leq @t53 tptp.n2)) % 0.39/0.62 (define @t93 () (tptp.leq tptp.n0 @t54)) % 0.39/0.62 (define @t94 () (tptp.leq tptp.n0 @t53)) % 0.39/0.62 (define @t95 () (and @t94 @t93 @t92 @t91)) % 0.39/0.62 (define @t96 () (=> @t95 @t90)) % 0.39/0.62 (define @t97 () (@list @t53 @t54)) % 0.39/0.62 (define @t98 () (forall @t97 @t96)) % 0.39/0.62 (define @t99 () (tptp.leq tptp.pv5 (tptp.minus tptp.n999 tptp.n1))) % 0.39/0.62 (define @t100 () (tptp.leq tptp.n0 tptp.pv5)) % 0.39/0.62 (define @t101 () (tptp.a_select2 tptp.xinit_noise_defuse tptp.n5)) % 0.39/0.62 (define @t102 () (= @t101 tptp.use)) % 0.39/0.62 (define @t103 () (tptp.a_select2 tptp.xinit_noise_defuse tptp.n4)) % 0.39/0.62 (define @t104 () (= @t103 tptp.use)) % 0.39/0.62 (define @t105 () (tptp.a_select2 tptp.xinit_noise_defuse tptp.n3)) % 0.39/0.62 (define @t106 () (= @t105 tptp.use)) % 0.39/0.62 (define @t107 () (tptp.a_select2 tptp.xinit_noise_defuse tptp.n2)) % 0.39/0.62 (define @t108 () (= @t107 tptp.use)) % 0.39/0.62 (define @t109 () (tptp.a_select2 tptp.xinit_noise_defuse tptp.n1)) % 0.39/0.62 (define @t110 () (= @t109 tptp.use)) % 0.39/0.62 (define @t111 () (tptp.a_select2 tptp.xinit_noise_defuse tptp.n0)) % 0.39/0.62 (define @t112 () (= @t111 tptp.use)) % 0.39/0.62 (define @t113 () (tptp.a_select2 tptp.xinit_mean_defuse tptp.n5)) % 0.39/0.62 (define @t114 () (= @t113 tptp.use)) % 0.39/0.62 (define @t115 () (tptp.a_select2 tptp.xinit_mean_defuse tptp.n4)) % 0.39/0.62 (define @t116 () (= @t115 tptp.use)) % 0.39/0.62 (define @t117 () (tptp.a_select2 tptp.xinit_mean_defuse tptp.n3)) % 0.39/0.62 (define @t118 () (= @t117 tptp.use)) % 0.39/0.62 (define @t119 () (tptp.a_select2 tptp.xinit_mean_defuse tptp.n2)) % 0.39/0.62 (define @t120 () (= @t119 tptp.use)) % 0.39/0.62 (define @t121 () (tptp.a_select2 tptp.xinit_mean_defuse tptp.n1)) % 0.39/0.62 (define @t122 () (= @t121 tptp.use)) % 0.39/0.62 (define @t123 () (tptp.a_select2 tptp.xinit_mean_defuse tptp.n0)) % 0.39/0.62 (define @t124 () (= @t123 tptp.use)) % 0.39/0.62 (define @t125 () (tptp.a_select2 tptp.xinit_defuse tptp.n5)) % 0.39/0.62 (define @t126 () (= @t125 tptp.use)) % 0.39/0.62 (define @t127 () (tptp.a_select2 tptp.xinit_defuse tptp.n4)) % 0.39/0.62 (define @t128 () (= @t127 tptp.use)) % 0.39/0.62 (define @t129 () (tptp.a_select2 tptp.xinit_defuse tptp.n3)) % 0.39/0.62 (define @t130 () (= @t129 tptp.use)) % 0.39/0.62 (define @t131 () (tptp.a_select3 tptp.u_defuse tptp.n2 tptp.n0)) % 0.39/0.62 (define @t132 () (= @t131 tptp.use)) % 0.39/0.62 (define @t133 () (tptp.a_select3 tptp.u_defuse tptp.n1 tptp.n0)) % 0.39/0.62 (define @t134 () (= @t133 tptp.use)) % 0.39/0.62 (define @t135 () (tptp.a_select3 tptp.u_defuse tptp.n0 tptp.n0)) % 0.39/0.62 (define @t136 () (= @t135 tptp.use)) % 0.39/0.62 (define @t137 () (tptp.a_select2 tptp.sigma_defuse tptp.n5)) % 0.39/0.62 (define @t138 () (= @t137 tptp.use)) % 0.39/0.62 (define @t139 () (tptp.a_select2 tptp.sigma_defuse tptp.n4)) % 0.39/0.62 (define @t140 () (= @t139 tptp.use)) % 0.39/0.62 (define @t141 () (tptp.a_select2 tptp.sigma_defuse tptp.n3)) % 0.39/0.62 (define @t142 () (= @t141 tptp.use)) % 0.39/0.62 (define @t143 () (tptp.a_select2 tptp.sigma_defuse tptp.n2)) % 0.39/0.62 (define @t144 () (= @t143 tptp.use)) % 0.39/0.62 (define @t145 () (tptp.a_select2 tptp.sigma_defuse tptp.n1)) % 0.39/0.62 (define @t146 () (= @t145 tptp.use)) % 0.39/0.62 (define @t147 () (tptp.a_select2 tptp.sigma_defuse tptp.n0)) % 0.39/0.62 (define @t148 () (= @t147 tptp.use)) % 0.39/0.62 (define @t149 () (tptp.a_select2 tptp.rho_defuse tptp.n2)) % 0.39/0.62 (define @t150 () (= @t149 tptp.use)) % 0.39/0.62 (define @t151 () (tptp.a_select2 tptp.rho_defuse tptp.n1)) % 0.39/0.62 (define @t152 () (= @t151 tptp.use)) % 0.39/0.62 (define @t153 () (tptp.a_select2 tptp.rho_defuse tptp.n0)) % 0.39/0.62 (define @t154 () (= @t153 tptp.use)) % 0.39/0.62 (define @t155 () (and @t154 @t152 @t150 @t148 @t146 @t144 @t142 @t140 @t138 @t136 @t134 @t132 @t130 @t128 @t126 @t124 @t122 @t120 @t118 @t116 @t114 @t112 @t110 @t108 @t106 @t104 @t102 @t100 @t99 @t98 @t87)) % 0.39/0.62 (define @t156 () (tptp.a_select3 tptp.z_defuse @t13 @t55)) % 0.39/0.62 (define @t157 () (tptp.a_select3 tptp.u_defuse @t13 @t55)) % 0.39/0.62 (define @t158 () (and (= @t157 tptp.use) (= @t156 tptp.use))) % 0.39/0.62 (define @t159 () (tptp.leq @t55 @t79)) % 0.39/0.62 (define @t160 () (tptp.leq @t13 tptp.n2)) % 0.39/0.62 (define @t161 () (tptp.leq tptp.n0 @t55)) % 0.39/0.62 (define @t162 () (tptp.leq tptp.n0 @t13)) % 0.39/0.62 (define @t163 () (and @t162 @t161 @t160 @t159)) % 0.39/0.62 (define @t164 () (=> @t163 @t158)) % 0.39/0.62 (define @t165 () (@list @t13 @t55)) % 0.39/0.62 (define @t166 () (forall @t165 @t164)) % 0.39/0.62 (define @t167 () (tptp.a_select3 tptp.z_defuse @t27 @t42)) % 0.39/0.62 (define @t168 () (tptp.a_select3 tptp.u_defuse @t27 @t42)) % 0.39/0.62 (define @t169 () (and (= @t168 tptp.use) (= @t167 tptp.use))) % 0.39/0.62 (define @t170 () (tptp.leq @t42 tptp.pv5)) % 0.39/0.62 (define @t171 () (tptp.leq @t27 tptp.n2)) % 0.39/0.62 (define @t172 () (tptp.leq tptp.n0 @t42)) % 0.39/0.62 (define @t173 () (tptp.leq tptp.n0 @t27)) % 0.39/0.62 (define @t174 () (and @t173 @t172 @t171 @t170)) % 0.39/0.62 (define @t175 () (=> @t174 @t169)) % 0.39/0.62 (define @t176 () (@list @t27 @t42)) % 0.39/0.62 (define @t177 () (forall @t176 @t175)) % 0.39/0.62 (define @t178 () (tptp.leq tptp.pv41 (tptp.minus tptp.n6 tptp.n1))) % 0.39/0.62 (define @t179 () (tptp.leq tptp.n0 tptp.pv41)) % 0.39/0.62 (define @t180 () (and @t154 @t152 @t150 @t148 @t146 @t144 @t142 @t140 @t138 @t136 @t134 @t132 @t130 @t128 @t126 @t124 @t122 @t120 @t118 @t116 @t114 @t112 @t110 @t108 @t106 @t104 @t102 @t100 @t179 @t99 @t178 @t177 @t166)) % 0.39/0.62 (define @t181 () (=> @t180 @t155)) % 0.39/0.62 (define @t182 () (not @t181)) % 0.39/0.62 (define @t183 () (= @t2 tptp.n4)) % 0.39/0.62 (define @t184 () (= @t2 tptp.n3)) % 0.39/0.62 (define @t185 () (= @t2 tptp.n2)) % 0.39/0.62 (define @t186 () (= @t2 tptp.n1)) % 0.39/0.62 (define @t187 () (= @t2 tptp.n0)) % 0.39/0.62 (define @t188 () (= @t2 tptp.n5)) % 0.39/0.62 (define @t189 () (tptp.succ tptp.n0)) % 0.39/0.62 (define @t190 () (tptp.succ @t189)) % 0.39/0.62 (define @t191 () (tptp.succ @t190)) % 0.39/0.62 (define @t192 () (tptp.succ @t191)) % 0.39/0.62 (define @t193 () (tptp.succ @t192)) % 0.39/0.62 (define @t194 () (and (= tptp.use @t77) (= tptp.use @t76))) % 0.39/0.62 (define @t195 () (not @t80)) % 0.39/0.62 (define @t196 () (not @t81)) % 0.39/0.62 (define @t197 () (not @t82)) % 0.39/0.62 (define @t198 () (not @t83)) % 0.39/0.62 (define @t199 () (or @t198 @t197 @t196 @t195 @t194)) % 0.39/0.62 (define @t200 () (or @t198 @t197 @t196 @t195)) % 0.39/0.62 (define @t201 () (and (= tptp.use @t89) (= tptp.use @t88))) % 0.39/0.62 (define @t202 () (not @t91)) % 0.39/0.62 (define @t203 () (not @t92)) % 0.39/0.62 (define @t204 () (not @t93)) % 0.39/0.62 (define @t205 () (not @t94)) % 0.39/0.62 (define @t206 () (or @t205 @t204 @t203 @t202 @t201)) % 0.39/0.62 (define @t207 () (or @t205 @t204 @t203 @t202)) % 0.39/0.62 (define @t208 () (and (= tptp.use @t157) (= tptp.use @t156))) % 0.39/0.62 (define @t209 () (not @t159)) % 0.39/0.62 (define @t210 () (not @t160)) % 0.39/0.62 (define @t211 () (not @t161)) % 0.39/0.62 (define @t212 () (not @t162)) % 0.39/0.62 (define @t213 () (or @t212 @t211 @t210 @t209 @t208)) % 0.39/0.62 (define @t214 () (or @t212 @t211 @t210 @t209)) % 0.39/0.62 (define @t215 () (and (= tptp.use @t168) (= tptp.use @t167))) % 0.39/0.62 (define @t216 () (not @t170)) % 0.39/0.62 (define @t217 () (not @t171)) % 0.39/0.62 (define @t218 () (not @t172)) % 0.39/0.62 (define @t219 () (not @t173)) % 0.39/0.62 (define @t220 () (or @t219 @t218 @t217 @t216 @t215)) % 0.39/0.62 (define @t221 () (or @t219 @t218 @t217 @t216)) % 0.39/0.62 (define @t222 () (forall @t176 @t220)) % 0.39/0.62 (define @t223 () (forall @t97 @t206)) % 0.39/0.62 (define @t224 () (@list false)) % 0.39/0.62 (define @t225 () (forall @t165 @t213)) % 0.39/0.62 (define @t226 () (forall @t86 @t199)) % 0.39/0.62 (assume @p1 (forall @t6 (or @t5 @t4 @t3))) % 0.39/0.62 (assume @p2 (forall @t8 (=> (and @t5 (tptp.gt @t1 @t7)) (tptp.gt @t2 @t7)))) % 0.39/0.62 (assume @p3 (forall @t9 (not (tptp.gt @t2 @t2)))) % 0.39/0.62 (assume @p4 (forall @t9 (tptp.leq @t2 @t2))) % 0.39/0.62 (assume @p5 (forall @t8 (=> (and @t10 (tptp.leq @t1 @t7)) (tptp.leq @t2 @t7)))) % 0.39/0.62 (assume @p6 (forall @t6 (= (tptp.lt @t2 @t1) @t4))) % 0.39/0.62 (assume @p7 (forall @t6 (= (tptp.geq @t2 @t1) (tptp.leq @t1 @t2)))) % 0.39/0.62 (assume @p8 (forall @t6 (=> @t4 @t10))) % 0.39/0.62 (assume @p9 (forall @t6 (=> (and @t10 (not @t3)) @t4))) % 0.39/0.62 (assume @p10 (forall @t6 (= (tptp.leq @t2 (tptp.pred @t1)) @t4))) % 0.39/0.62 (assume @p11 (forall @t9 (tptp.gt @t11 @t2))) % 0.39/0.62 (assume @p12 (forall @t6 (=> @t10 (tptp.leq @t2 @t12)))) % 0.39/0.62 (assume @p13 (forall @t6 (= @t10 (tptp.gt @t12 @t2)))) % 0.39/0.62 (assume @p14 (forall @t16 (=> @t15 (tptp.leq @t14 @t2)))) % 0.39/0.62 (assume @p15 (forall @t16 (=> @t15 (tptp.leq tptp.n0 @t14)))) % 0.39/0.62 (assume @p16 (forall (@list @t18 @t20 @t19 @t17) (=> (and (tptp.leq @t20 @t18) @t21) (= (tptp.a_select2 (tptp.tptp_const_array1 (tptp.dim @t20 @t19) @t17) @t18) @t17)))) % 0.39/0.62 (assume @p17 (forall (@list @t18 @t26 @t25 @t22 @t24 @t23 @t17) (=> (and (tptp.leq @t26 @t18) (tptp.leq @t18 @t25) (tptp.leq @t24 @t22) (tptp.leq @t22 @t23)) (= (tptp.a_select3 (tptp.tptp_const_array2 (tptp.dim @t26 @t25) (tptp.dim @t24 @t23) @t17) @t18 @t22) @t17)))) % 0.39/0.62 (assume @p18 (forall @t37 (=> @t36 (forall @t35 (=> @t34 (= (tptp.a_select3 @t28 @t18 @t22) (tptp.a_select3 @t28 @t22 @t18))))))) % 0.39/0.62 (assume @p19 (forall @t37 (=> @t36 (forall @t35 (=> @t34 (= (tptp.a_select3 @t38 @t18 @t22) (tptp.a_select3 @t38 @t22 @t18))))))) % 0.39/0.62 (assume @p20 (forall @t37 (=> @t36 (forall (@list @t18 @t22 @t40 @t39) (=> (and @t33 @t32 @t31 @t30 (tptp.leq tptp.n0 @t40) (tptp.leq @t40 @t29)) (= (tptp.a_select3 @t41 @t18 @t22) (tptp.a_select3 @t41 @t22 @t18))))))) % 0.39/0.62 (assume @p21 (forall @t47 (=> @t46 (forall @t35 (=> @t34 (= (tptp.a_select3 @t43 @t18 @t22) (tptp.a_select3 @t43 @t22 @t18))))))) % 0.39/0.62 (assume @p22 (forall @t47 (=> @t46 (forall @t35 (=> @t34 (= (tptp.a_select3 @t48 @t18 @t22) (tptp.a_select3 @t48 @t22 @t18))))))) % 0.39/0.62 (assume @p23 (forall @t47 (=> @t45 @t50))) % 0.39/0.62 (assume @p24 (forall (@list @t27 @t42 @t29 @t51) (=> (forall @t35 (=> @t52 @t44)) @t50))) % 0.39/0.62 (assume @p25 (forall (@list @t27 @t42 @t13 @t55 @t53 @t54 @t29 @t51) (=> (and (forall @t35 (=> @t52 (= (tptp.a_select3 @t55 @t18 @t22) (tptp.a_select3 @t55 @t22 @t18)))) @t36 (forall @t35 (=> @t34 (= (tptp.a_select3 @t54 @t18 @t22) (tptp.a_select3 @t54 @t22 @t18))))) (forall @t35 (=> @t34 (= (tptp.a_select3 @t56 @t18 @t22) (tptp.a_select3 @t56 @t22 @t18))))))) % 0.39/0.62 (assume @p26 (forall @t59 (= @t58 tptp.n0))) % 0.39/0.62 (assume @p27 (forall @t59 (= tptp.tptp_float_0_0 @t58))) % 0.39/0.62 (assume @p28 (= (tptp.succ tptp.tptp_minus_1) tptp.n0)) % 0.39/0.62 (assume @p29 (forall @t9 (= (tptp.plus @t2 tptp.n1) @t11))) % 0.39/0.62 (assume @p30 (forall @t9 (= (tptp.plus tptp.n1 @t2) @t11))) % 0.39/0.62 (assume @p31 (forall @t9 (= (tptp.plus @t2 tptp.n2) @t60))) % 0.39/0.62 (assume @p32 (forall @t9 (= (tptp.plus tptp.n2 @t2) @t60))) % 0.39/0.62 (assume @p33 (forall @t9 (= (tptp.plus @t2 tptp.n3) @t61))) % 0.39/0.62 (assume @p34 (forall @t9 (= (tptp.plus tptp.n3 @t2) @t61))) % 0.39/0.62 (assume @p35 (forall @t9 (= (tptp.plus @t2 tptp.n4) @t62))) % 0.39/0.62 (assume @p36 (forall @t9 (= (tptp.plus tptp.n4 @t2) @t62))) % 0.39/0.62 (assume @p37 (forall @t9 (= (tptp.plus @t2 tptp.n5) @t63))) % 0.39/0.62 (assume @p38 (forall @t9 (= (tptp.plus tptp.n5 @t2) @t63))) % 0.39/0.62 (assume @p39 (forall @t9 (= (tptp.minus @t2 tptp.n1) @t64))) % 0.39/0.62 (assume @p40 (forall @t9 (= (tptp.pred @t11) @t2))) % 0.39/0.62 (assume @p41 (forall @t9 (= (tptp.succ @t64) @t2))) % 0.39/0.62 (assume @p42 (forall @t6 (= (tptp.leq @t11 @t12) @t10))) % 0.39/0.62 (assume @p43 (forall @t6 (=> (tptp.leq @t11 @t1) @t4))) % 0.39/0.62 (assume @p44 (forall @t6 (=> (tptp.leq (tptp.minus @t2 @t1) @t2) (tptp.leq tptp.n0 @t1)))) % 0.39/0.62 (assume @p45 (forall (@list @t2 @t19 @t65 @t39) (= (tptp.a_select3 @t66 @t19 @t65) @t39))) % 0.39/0.62 (assume @p46 (forall (@list @t18 @t22 @t19 @t65 @t2 @t39 @t67) (=> (and @t68 (= @t22 @t65) (= (tptp.a_select3 @t2 @t19 @t65) @t39)) (= (tptp.a_select3 (tptp.tptp_update3 @t2 @t18 @t22 @t67) @t19 @t65) @t39)))) % 0.39/0.62 (assume @p47 (forall (@list @t18 @t22 @t19 @t65 @t2 @t39) (=> (and (forall (@list @t70 @t69) (=> (and @t72 (tptp.leq tptp.n0 @t69) @t71 (tptp.leq @t69 @t65)) (= (tptp.a_select3 @t2 @t70 @t69) @t39))) @t33 @t21 @t31 (tptp.leq @t22 @t65)) (= (tptp.a_select3 @t66 @t18 @t22) @t39)))) % 0.39/0.62 (assume @p48 (forall (@list @t2 @t19 @t39) (= (tptp.a_select2 @t73 @t19) @t39))) % 0.39/0.62 (assume @p49 (forall (@list @t18 @t19 @t2 @t39 @t67) (=> (and @t68 (= (tptp.a_select2 @t2 @t19) @t39)) (= (tptp.a_select2 (tptp.tptp_update2 @t2 @t18 @t67) @t19) @t39)))) % 0.39/0.62 (assume @p50 (forall (@list @t18 @t19 @t2 @t39) (=> (and (forall (@list @t70) (=> (and @t72 @t71) (= (tptp.a_select2 @t2 @t70) @t39))) @t33 @t21) (= (tptp.a_select2 @t73 @t18) @t39)))) % 0.39/0.62 (assume @p51 tptp.true) % 0.39/0.62 (assume @p52 (not (= tptp.def tptp.use))) % 0.39/0.62 (assume @p53 @t182) % 0.39/0.62 (assume @p54 (tptp.gt tptp.n5 tptp.n4)) % 0.39/0.62 (assume @p55 (tptp.gt tptp.n6 tptp.n4)) % 0.39/0.62 (assume @p56 (tptp.gt tptp.n999 tptp.n4)) % 0.39/0.62 (assume @p57 (tptp.gt tptp.n6 tptp.n5)) % 0.39/0.62 (assume @p58 (tptp.gt tptp.n999 tptp.n5)) % 0.39/0.62 (assume @p59 (tptp.gt tptp.n999 tptp.n6)) % 0.39/0.62 (assume @p60 (tptp.gt tptp.n4 tptp.tptp_minus_1)) % 0.39/0.62 (assume @p61 (tptp.gt tptp.n5 tptp.tptp_minus_1)) % 0.39/0.62 (assume @p62 (tptp.gt tptp.n6 tptp.tptp_minus_1)) % 0.39/0.62 (assume @p63 (tptp.gt tptp.n999 tptp.tptp_minus_1)) % 0.39/0.62 (assume @p64 (tptp.gt tptp.n0 tptp.tptp_minus_1)) % 0.39/0.62 (assume @p65 (tptp.gt tptp.n1 tptp.tptp_minus_1)) % 0.39/0.62 (assume @p66 (tptp.gt tptp.n2 tptp.tptp_minus_1)) % 0.39/0.62 (assume @p67 (tptp.gt tptp.n3 tptp.tptp_minus_1)) % 0.39/0.62 (assume @p68 (tptp.gt tptp.n4 tptp.n0)) % 0.39/0.62 (assume @p69 (tptp.gt tptp.n5 tptp.n0)) % 0.39/0.62 (assume @p70 (tptp.gt tptp.n6 tptp.n0)) % 0.39/0.62 (assume @p71 (tptp.gt tptp.n999 tptp.n0)) % 0.39/0.62 (assume @p72 (tptp.gt tptp.n1 tptp.n0)) % 0.39/0.62 (assume @p73 (tptp.gt tptp.n2 tptp.n0)) % 0.39/0.62 (assume @p74 (tptp.gt tptp.n3 tptp.n0)) % 0.39/0.62 (assume @p75 (tptp.gt tptp.n4 tptp.n1)) % 0.39/0.62 (assume @p76 (tptp.gt tptp.n5 tptp.n1)) % 0.39/0.62 (assume @p77 (tptp.gt tptp.n6 tptp.n1)) % 0.39/0.62 (assume @p78 (tptp.gt tptp.n999 tptp.n1)) % 0.39/0.62 (assume @p79 (tptp.gt tptp.n2 tptp.n1)) % 0.39/0.62 (assume @p80 (tptp.gt tptp.n3 tptp.n1)) % 0.39/0.62 (assume @p81 (tptp.gt tptp.n4 tptp.n2)) % 0.39/0.62 (assume @p82 (tptp.gt tptp.n5 tptp.n2)) % 0.39/0.62 (assume @p83 (tptp.gt tptp.n6 tptp.n2)) % 0.39/0.62 (assume @p84 (tptp.gt tptp.n999 tptp.n2)) % 0.39/0.62 (assume @p85 (tptp.gt tptp.n3 tptp.n2)) % 0.39/0.62 (assume @p86 (tptp.gt tptp.n4 tptp.n3)) % 0.39/0.62 (assume @p87 (tptp.gt tptp.n5 tptp.n3)) % 0.39/0.62 (assume @p88 (tptp.gt tptp.n6 tptp.n3)) % 0.39/0.62 (assume @p89 (tptp.gt tptp.n999 tptp.n3)) % 0.39/0.62 (assume @p90 (forall @t9 (=> (and @t15 (tptp.leq @t2 tptp.n4)) (or @t187 @t186 @t185 @t184 @t183)))) % 0.39/0.62 (assume @p91 (forall @t9 (=> (and @t15 (tptp.leq @t2 tptp.n5)) (or @t187 @t186 @t185 @t184 @t183 @t188)))) % 0.39/0.62 (assume @p92 (forall @t9 (=> (and @t15 (tptp.leq @t2 tptp.n6)) (or @t187 @t186 @t185 @t184 @t183 @t188 (= @t2 tptp.n6))))) % 0.39/0.62 (assume @p93 (forall @t9 (=> (and @t15 (tptp.leq @t2 tptp.n0)) @t187))) % 0.39/0.62 (assume @p94 (forall @t9 (=> (and @t15 (tptp.leq @t2 tptp.n1)) (or @t187 @t186)))) % 0.39/0.62 (assume @p95 (forall @t9 (=> (and @t15 (tptp.leq @t2 tptp.n2)) (or @t187 @t186 @t185)))) % 0.39/0.62 (assume @p96 (forall @t9 (=> (and @t15 (tptp.leq @t2 tptp.n3)) (or @t187 @t186 @t185 @t184)))) % 0.39/0.62 (assume @p97 (= @t192 tptp.n4)) % 0.39/0.62 (assume @p98 (= @t193 tptp.n5)) % 0.39/0.62 (assume @p99 (= (tptp.succ @t193) tptp.n6)) % 0.39/0.62 (assume @p100 (= @t189 tptp.n1)) % 0.39/0.62 (assume @p101 (= @t190 tptp.n2)) % 0.39/0.62 (assume @p102 (= @t191 tptp.n3)) % 0.39/0.62 (assume @p103 true) % 0.39/0.62 (step @p104 :rule aci_norm :args ((= (or @t200 @t194) @t199))) % 0.39/0.62 (step @p105 :rule refl :args (@t194)) % 0.39/0.62 (step @p106 :rule aci_norm :args ((= (or @t198 (or @t197 (or @t196 @t195))) @t200))) % 0.39/0.62 (step @p107 :rule bool-and-de-morgan :args (@t81 @t80 true)) % 0.39/0.62 (step @p108 :rule refl :args (@t197)) % 0.39/0.62 (step @p109 :rule nary_cong :premises (@p108 @p107) :args ((or @t197 (not (and @t81 @t80))))) % 0.39/0.62 (step @p110 :rule bool-and-de-morgan :args (@t82 @t81 (and @t80))) % 0.39/0.62 (step @p111 :rule trans :premises (@p110 @p109)) % 0.39/0.62 (step @p112 :rule refl :args (@t198)) % 0.39/0.62 (step @p113 :rule nary_cong :premises (@p112 @p111) :args ((or @t198 (not (and @t82 @t81 @t80))))) % 0.39/0.62 (step @p114 :rule bool-and-de-morgan :args (@t83 @t82 (and @t81 @t80))) % 0.39/0.62 (step @p115 :rule trans :premises (@p114 @p113)) % 0.39/0.62 (step @p116 :rule trans :premises (@p115 @p106)) % 0.39/0.62 (step @p117 :rule nary_cong :premises (@p116 @p105) :args ((or (not @t84) @t194))) % 0.39/0.62 (step @p118 :rule trans :premises (@p117 @p104)) % 0.39/0.62 (step @p119 :rule bool-impl-elim :args (@t84 @t194)) % 0.39/0.62 (step @p120 :rule trans :premises (@p119 @p118)) % 0.39/0.62 (step @p121 :rule cong :premises (@p120) :args ((forall @t86 (=> @t84 @t194)))) % 0.39/0.62 (step @p122 :rule eq-symm :args (@t76 tptp.use)) % 0.39/0.62 (step @p123 :rule eq-symm :args (@t77 tptp.use)) % 0.39/0.62 (step @p124 :rule nary_cong :premises (@p123 @p122) :args (@t78)) % 0.39/0.62 (step @p125 :rule refl :args (@t84)) % 0.39/0.62 (step @p126 :rule cong :premises (@p125 @p124) :args (@t85)) % 0.39/0.62 (step @p127 :rule cong :premises (@p126) :args (@t87)) % 0.39/0.62 (step @p128 :rule trans :premises (@p127 @p121)) % 0.39/0.62 (step @p129 :rule aci_norm :args ((= (or @t207 @t201) @t206))) % 0.39/0.62 (step @p130 :rule refl :args (@t201)) % 0.39/0.62 (step @p131 :rule aci_norm :args ((= (or @t205 (or @t204 (or @t203 @t202))) @t207))) % 0.39/0.62 (step @p132 :rule bool-and-de-morgan :args (@t92 @t91 true)) % 0.39/0.62 (step @p133 :rule refl :args (@t204)) % 0.39/0.62 (step @p134 :rule nary_cong :premises (@p133 @p132) :args ((or @t204 (not (and @t92 @t91))))) % 0.39/0.62 (step @p135 :rule bool-and-de-morgan :args (@t93 @t92 (and @t91))) % 0.39/0.62 (step @p136 :rule trans :premises (@p135 @p134)) % 0.39/0.62 (step @p137 :rule refl :args (@t205)) % 0.39/0.62 (step @p138 :rule nary_cong :premises (@p137 @p136) :args ((or @t205 (not (and @t93 @t92 @t91))))) % 0.39/0.62 (step @p139 :rule bool-and-de-morgan :args (@t94 @t93 (and @t92 @t91))) % 0.39/0.62 (step @p140 :rule trans :premises (@p139 @p138)) % 0.39/0.62 (step @p141 :rule trans :premises (@p140 @p131)) % 0.39/0.62 (step @p142 :rule nary_cong :premises (@p141 @p130) :args ((or (not @t95) @t201))) % 0.39/0.62 (step @p143 :rule trans :premises (@p142 @p129)) % 0.39/0.62 (step @p144 :rule bool-impl-elim :args (@t95 @t201)) % 0.39/0.62 (step @p145 :rule trans :premises (@p144 @p143)) % 0.39/0.62 (step @p146 :rule cong :premises (@p145) :args ((forall @t97 (=> @t95 @t201)))) % 0.39/0.62 (step @p147 :rule eq-symm :args (@t88 tptp.use)) % 0.39/0.62 (step @p148 :rule eq-symm :args (@t89 tptp.use)) % 0.39/0.62 (step @p149 :rule nary_cong :premises (@p148 @p147) :args (@t90)) % 0.39/0.62 (step @p150 :rule refl :args (@t95)) % 0.39/0.62 (step @p151 :rule cong :premises (@p150 @p149) :args (@t96)) % 0.39/0.62 (step @p152 :rule cong :premises (@p151) :args (@t98)) % 0.39/0.62 (step @p153 :rule trans :premises (@p152 @p146)) % 0.39/0.62 (step @p154 :rule refl :args (@t99)) % 0.39/0.62 (step @p155 :rule refl :args (@t100)) % 0.39/0.62 (step @p156 :rule eq-symm :args (@t101 tptp.use)) % 0.39/0.62 (step @p157 :rule eq-symm :args (@t103 tptp.use)) % 0.39/0.62 (step @p158 :rule eq-symm :args (@t105 tptp.use)) % 0.39/0.62 (step @p159 :rule eq-symm :args (@t107 tptp.use)) % 0.39/0.62 (step @p160 :rule eq-symm :args (@t109 tptp.use)) % 0.39/0.62 (step @p161 :rule eq-symm :args (@t111 tptp.use)) % 0.39/0.62 (step @p162 :rule eq-symm :args (@t113 tptp.use)) % 0.39/0.62 (step @p163 :rule eq-symm :args (@t115 tptp.use)) % 0.39/0.62 (step @p164 :rule eq-symm :args (@t117 tptp.use)) % 0.39/0.62 (step @p165 :rule eq-symm :args (@t119 tptp.use)) % 0.39/0.62 (step @p166 :rule eq-symm :args (@t121 tptp.use)) % 0.39/0.62 (step @p167 :rule eq-symm :args (@t123 tptp.use)) % 0.39/0.62 (step @p168 :rule eq-symm :args (@t125 tptp.use)) % 0.39/0.62 (step @p169 :rule eq-symm :args (@t127 tptp.use)) % 0.39/0.62 (step @p170 :rule eq-symm :args (@t129 tptp.use)) % 0.39/0.62 (step @p171 :rule eq-symm :args (@t131 tptp.use)) % 0.39/0.62 (step @p172 :rule eq-symm :args (@t133 tptp.use)) % 0.39/0.62 (step @p173 :rule eq-symm :args (@t135 tptp.use)) % 0.39/0.62 (step @p174 :rule eq-symm :args (@t137 tptp.use)) % 0.39/0.62 (step @p175 :rule eq-symm :args (@t139 tptp.use)) % 0.39/0.62 (step @p176 :rule eq-symm :args (@t141 tptp.use)) % 0.39/0.62 (step @p177 :rule eq-symm :args (@t143 tptp.use)) % 0.39/0.62 (step @p178 :rule eq-symm :args (@t145 tptp.use)) % 0.39/0.62 (step @p179 :rule eq-symm :args (@t147 tptp.use)) % 0.39/0.62 (step @p180 :rule eq-symm :args (@t149 tptp.use)) % 0.39/0.62 (step @p181 :rule eq-symm :args (@t151 tptp.use)) % 0.39/0.62 (step @p182 :rule eq-symm :args (@t153 tptp.use)) % 0.39/0.62 (step @p183 :rule nary_cong :premises (@p182 @p181 @p180 @p179 @p178 @p177 @p176 @p175 @p174 @p173 @p172 @p171 @p170 @p169 @p168 @p167 @p166 @p165 @p164 @p163 @p162 @p161 @p160 @p159 @p158 @p157 @p156 @p155 @p154 @p153 @p128) :args (@t155)) % 0.39/0.62 (step @p184 :rule aci_norm :args ((= (or @t214 @t208) @t213))) % 0.39/0.62 (step @p185 :rule refl :args (@t208)) % 0.39/0.62 (step @p186 :rule aci_norm :args ((= (or @t212 (or @t211 (or @t210 @t209))) @t214))) % 0.39/0.62 (step @p187 :rule bool-and-de-morgan :args (@t160 @t159 true)) % 0.39/0.62 (step @p188 :rule refl :args (@t211)) % 0.39/0.62 (step @p189 :rule nary_cong :premises (@p188 @p187) :args ((or @t211 (not (and @t160 @t159))))) % 0.39/0.62 (step @p190 :rule bool-and-de-morgan :args (@t161 @t160 (and @t159))) % 0.39/0.62 (step @p191 :rule trans :premises (@p190 @p189)) % 0.39/0.62 (step @p192 :rule refl :args (@t212)) % 0.39/0.62 (step @p193 :rule nary_cong :premises (@p192 @p191) :args ((or @t212 (not (and @t161 @t160 @t159))))) % 0.39/0.62 (step @p194 :rule bool-and-de-morgan :args (@t162 @t161 (and @t160 @t159))) % 0.39/0.62 (step @p195 :rule trans :premises (@p194 @p193)) % 0.39/0.62 (step @p196 :rule trans :premises (@p195 @p186)) % 0.39/0.62 (step @p197 :rule nary_cong :premises (@p196 @p185) :args ((or (not @t163) @t208))) % 0.39/0.62 (step @p198 :rule trans :premises (@p197 @p184)) % 0.39/0.62 (step @p199 :rule bool-impl-elim :args (@t163 @t208)) % 0.39/0.62 (step @p200 :rule trans :premises (@p199 @p198)) % 0.39/0.62 (step @p201 :rule cong :premises (@p200) :args ((forall @t165 (=> @t163 @t208)))) % 0.39/0.62 (step @p202 :rule eq-symm :args (@t156 tptp.use)) % 0.39/0.62 (step @p203 :rule eq-symm :args (@t157 tptp.use)) % 0.39/0.62 (step @p204 :rule nary_cong :premises (@p203 @p202) :args (@t158)) % 0.39/0.62 (step @p205 :rule refl :args (@t163)) % 0.39/0.62 (step @p206 :rule cong :premises (@p205 @p204) :args (@t164)) % 0.39/0.62 (step @p207 :rule cong :premises (@p206) :args (@t166)) % 0.39/0.62 (step @p208 :rule trans :premises (@p207 @p201)) % 0.39/0.62 (step @p209 :rule aci_norm :args ((= (or @t221 @t215) @t220))) % 0.39/0.62 (step @p210 :rule refl :args (@t215)) % 0.39/0.62 (step @p211 :rule aci_norm :args ((= (or @t219 (or @t218 (or @t217 @t216))) @t221))) % 0.39/0.62 (step @p212 :rule bool-and-de-morgan :args (@t171 @t170 true)) % 0.39/0.62 (step @p213 :rule refl :args (@t218)) % 0.39/0.62 (step @p214 :rule nary_cong :premises (@p213 @p212) :args ((or @t218 (not (and @t171 @t170))))) % 0.39/0.62 (step @p215 :rule bool-and-de-morgan :args (@t172 @t171 (and @t170))) % 0.39/0.62 (step @p216 :rule trans :premises (@p215 @p214)) % 0.39/0.62 (step @p217 :rule refl :args (@t219)) % 0.39/0.62 (step @p218 :rule nary_cong :premises (@p217 @p216) :args ((or @t219 (not (and @t172 @t171 @t170))))) % 0.39/0.62 (step @p219 :rule bool-and-de-morgan :args (@t173 @t172 (and @t171 @t170))) % 0.39/0.62 (step @p220 :rule trans :premises (@p219 @p218)) % 0.39/0.62 (step @p221 :rule trans :premises (@p220 @p211)) % 0.39/0.62 (step @p222 :rule nary_cong :premises (@p221 @p210) :args ((or (not @t174) @t215))) % 0.39/0.62 (step @p223 :rule trans :premises (@p222 @p209)) % 0.39/0.62 (step @p224 :rule bool-impl-elim :args (@t174 @t215)) % 0.39/0.62 (step @p225 :rule trans :premises (@p224 @p223)) % 0.39/0.62 (step @p226 :rule cong :premises (@p225) :args ((forall @t176 (=> @t174 @t215)))) % 0.39/0.62 (step @p227 :rule eq-symm :args (@t167 tptp.use)) % 0.39/0.62 (step @p228 :rule eq-symm :args (@t168 tptp.use)) % 0.39/0.62 (step @p229 :rule nary_cong :premises (@p228 @p227) :args (@t169)) % 0.39/0.62 (step @p230 :rule refl :args (@t174)) % 0.39/0.62 (step @p231 :rule cong :premises (@p230 @p229) :args (@t175)) % 0.39/0.62 (step @p232 :rule cong :premises (@p231) :args (@t177)) % 0.39/0.62 (step @p233 :rule trans :premises (@p232 @p226)) % 0.39/0.62 (step @p234 :rule refl :args (@t178)) % 0.39/0.62 (step @p235 :rule refl :args (@t179)) % 0.39/0.62 (step @p236 :rule nary_cong :premises (@p182 @p181 @p180 @p179 @p178 @p177 @p176 @p175 @p174 @p173 @p172 @p171 @p170 @p169 @p168 @p167 @p166 @p165 @p164 @p163 @p162 @p161 @p160 @p159 @p158 @p157 @p156 @p155 @p235 @p154 @p234 @p233 @p208) :args (@t180)) % 0.39/0.62 (step @p237 :rule cong :premises (@p236 @p183) :args (@t181)) % 0.39/0.62 (step @p238 :rule cong :premises (@p237) :args (@t182)) % 0.39/0.62 (step @p239 :rule eq_resolve :premises (@p53 @p238)) % 0.39/0.62 (step @p240 :rule not_implies_elim1 :premises (@p239)) % 0.39/0.62 (step @p241 :rule and_elim :premises (@p240) :args (0)) % 0.39/0.62 (step @p242 :rule and_elim :premises (@p240) :args (1)) % 0.39/0.62 (step @p243 :rule and_elim :premises (@p240) :args (2)) % 0.39/0.62 (step @p244 :rule and_elim :premises (@p240) :args (3)) % 0.39/0.62 (step @p245 :rule and_elim :premises (@p240) :args (4)) % 0.39/0.62 (step @p246 :rule and_elim :premises (@p240) :args (5)) % 0.39/0.62 (step @p247 :rule and_elim :premises (@p240) :args (6)) % 0.39/0.62 (step @p248 :rule and_elim :premises (@p240) :args (7)) % 0.39/0.62 (step @p249 :rule and_elim :premises (@p240) :args (8)) % 0.39/0.62 (step @p250 :rule and_elim :premises (@p240) :args (9)) % 0.39/0.62 (step @p251 :rule and_elim :premises (@p240) :args (10)) % 0.39/0.62 (step @p252 :rule and_elim :premises (@p240) :args (11)) % 0.39/0.62 (step @p253 :rule and_elim :premises (@p240) :args (12)) % 0.39/0.62 (step @p254 :rule and_elim :premises (@p240) :args (13)) % 0.39/0.62 (step @p255 :rule and_elim :premises (@p240) :args (14)) % 0.39/0.62 (step @p256 :rule and_elim :premises (@p240) :args (15)) % 0.39/0.62 (step @p257 :rule and_elim :premises (@p240) :args (16)) % 0.39/0.62 (step @p258 :rule and_elim :premises (@p240) :args (17)) % 0.39/0.62 (step @p259 :rule and_elim :premises (@p240) :args (18)) % 0.39/0.62 (step @p260 :rule and_elim :premises (@p240) :args (19)) % 0.39/0.62 (step @p261 :rule and_elim :premises (@p240) :args (20)) % 0.39/0.62 (step @p262 :rule and_elim :premises (@p240) :args (21)) % 0.39/0.62 (step @p263 :rule and_elim :premises (@p240) :args (22)) % 0.39/0.62 (step @p264 :rule and_elim :premises (@p240) :args (23)) % 0.39/0.62 (step @p265 :rule and_elim :premises (@p240) :args (24)) % 0.39/0.62 (step @p266 :rule and_elim :premises (@p240) :args (25)) % 0.39/0.62 (step @p267 :rule and_elim :premises (@p240) :args (26)) % 0.39/0.62 (step @p268 :rule and_elim :premises (@p240) :args (27)) % 0.39/0.62 (step @p269 :rule and_elim :premises (@p240) :args (29)) % 0.39/0.62 (step @p270 :rule and_elim :premises (@p240) :args (31)) % 0.39/0.62 (step @p271 :rule alpha_equiv :args (@t222 (@list @t27 @t42) (@list @t53 @t54))) % 0.39/0.62 (step @p272 :rule equiv_elim1 :premises (@p271)) % 0.39/0.62 (step @p273 :rule reordering :premises (@p272) :args ((or @t223 (not @t222)))) % 0.39/0.62 (step @p274 :rule chain_m_resolution :premises (@p273 @p270) :args (@t223 @t224 (@list @t222))) % 0.39/0.62 (step @p275 :rule and_elim :premises (@p240) :args (32)) % 0.39/0.62 (step @p276 :rule alpha_equiv :args (@t225 (@list @t13 @t55) (@list @t75 @t74))) % 0.39/0.62 (step @p277 :rule equiv_elim1 :premises (@p276)) % 0.39/0.62 (step @p278 :rule reordering :premises (@p277) :args ((or @t226 (not @t225)))) % 0.39/0.62 (step @p279 :rule chain_m_resolution :premises (@p278 @p275) :args (@t226 @t224 (@list @t225))) % 0.39/0.62 (step @p280 :rule not_implies_elim2 :premises (@p239)) % 0.39/0.62 (step @p281 :rule not_and :premises (@p280)) % 0.39/0.62 (step @p282 false :rule chain_m_resolution :premises (@p281 @p279 @p274 @p269 @p268 @p267 @p266 @p265 @p264 @p263 @p262 @p261 @p260 @p259 @p258 @p257 @p256 @p255 @p254 @p253 @p252 @p251 @p250 @p249 @p248 @p247 @p246 @p245 @p244 @p243 @p242 @p241) :args (false (@list false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false false) (@list @t226 @t223 @t99 @t100 (= tptp.use @t101) (= tptp.use @t103) (= tptp.use @t105) (= tptp.use @t107) (= tptp.use @t109) (= tptp.use @t111) (= tptp.use @t113) (= tptp.use @t115) (= tptp.use @t117) (= tptp.use @t119) (= tptp.use @t121) (= tptp.use @t123) (= tptp.use @t125) (= tptp.use @t127) (= tptp.use @t129) (= tptp.use @t131) (= tptp.use @t133) (= tptp.use @t135) (= tptp.use @t137) (= tptp.use @t139) (= tptp.use @t141) (= tptp.use @t143) (= tptp.use @t145) (= tptp.use @t147) (= tptp.use @t149) (= tptp.use @t151) (= tptp.use @t153)))) % 0.39/0.62 ) % 0.39/0.62 % SZS output end Proof % 0.39/0.62 % cvc5 exiting %------------------------------------------------------------------------------