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