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