%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : GEO535+1 : TPTP v9.2.1. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n025.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 08:17:22 AM UTC 2026 % Result : Theorem 34.54s 34.73s % Output : Proof 34.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : GEO535+1 : TPTP v9.2.1. Released v7.0.0. % 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.17/0.34 % Computer : n025.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 00:00:16 EDT 2026 % 0.17/0.34 % CPUTime : % 0.39/0.56 %----Proving TF0_NAR, FOF, or CNF % 34.54/34.73 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 15... % 34.54/34.73 --- Run --no-e-matching --full-saturate-quant at 6... % 34.54/34.73 --- Run --no-e-matching --enum-inst-sum --full-saturate-quant at 6... % 34.54/34.73 --- Run --finite-model-find --uf-ss=no-minimal at 6... % 34.54/34.73 --- Run --multi-trigger-when-single --full-saturate-quant at 30... % 34.54/34.73 % SZS status Theorem % 34.54/34.73 % SZS output start Proof % 34.54/34.73 ( % 34.54/34.73 (declare-sort $$unsorted 0) % 34.54/34.73 (declare-const tptp.ss1 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.g813 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.c63 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.crossbar (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.perpAt (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.f813 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.triangle (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.pointOffLine (-> $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.isomidpoint (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.xb $$unsorted) % 34.54/34.73 (declare-const tptp.alpha $$unsorted) % 34.54/34.73 (declare-const tptp.s_e (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.s_r (-> $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.beta $$unsorted) % 34.54/34.73 (declare-const tptp.s_fs (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.ext (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.erectAux (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.gamma $$unsorted) % 34.54/34.73 (declare-const tptp.insert (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.s_m (-> $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.il (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.s_t (-> $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.s_afs (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.g811 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.s_e3 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.s_ifs (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.f113c (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.s_col (-> $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.erect21a (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.s_kf (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.f113f (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.insert5 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.foot (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.ss3 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.erectAux21a (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.erect (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.ins (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.congruent (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.midpointAux (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.sameside (-> $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.midpoint (-> $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.xd $$unsorted) % 34.54/34.73 (declare-const tptp.s (-> $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.xa $$unsorted) % 34.54/34.73 (declare-const tptp.xc $$unsorted) % 34.54/34.73 (declare-const tptp.erectsameside (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.xq $$unsorted) % 34.54/34.73 (declare-const tptp.xp $$unsorted) % 34.54/34.73 (declare-const tptp.le (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.ip (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.samesideline (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.opposite (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.constructAngle (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.op (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.reflect (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.perp (-> $$unsorted $$unsorted $$unsorted $$unsorted Bool)) % 34.54/34.73 (declare-const tptp.f113d (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.f113a (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.f811 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (declare-const tptp.ss2 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 34.54/34.73 (define @t1 () (@var "X" $$unsorted)) % 34.54/34.73 (define @t2 () (@var "Y" $$unsorted)) % 34.54/34.73 (define @t3 () (@list @t1 @t2)) % 34.54/34.73 (define @t4 () (@var "V2" $$unsorted)) % 34.54/34.73 (define @t5 () (@var "Z2" $$unsorted)) % 34.54/34.73 (define @t6 () (@var "V" $$unsorted)) % 34.54/34.73 (define @t7 () (@var "Z" $$unsorted)) % 34.54/34.73 (define @t8 () (= @t1 @t2)) % 34.54/34.73 (define @t9 () (@var "W" $$unsorted)) % 34.54/34.73 (define @t10 () (tptp.ext @t1 @t2 @t9 @t6)) % 34.54/34.73 (define @t11 () (tptp.s_e @t2 @t10 @t9 @t6)) % 34.54/34.73 (define @t12 () (tptp.s_t @t1 @t2 @t10)) % 34.54/34.73 (define @t13 () (@list @t1 @t2 @t9 @t6)) % 34.54/34.73 (define @t14 () (forall @t13 (and @t12 @t11))) % 34.54/34.73 (define @t15 () (@var "V1" $$unsorted)) % 34.54/34.73 (define @t16 () (@var "Z1" $$unsorted)) % 34.54/34.73 (define @t17 () (@var "Y1" $$unsorted)) % 34.54/34.73 (define @t18 () (@var "X1" $$unsorted)) % 34.54/34.73 (define @t19 () (forall @t3 (or (not (tptp.s_t @t1 @t2 @t1)) @t8))) % 34.54/34.73 (define @t20 () (@var "Xa" $$unsorted)) % 34.54/34.73 (define @t21 () (@var "Xq" $$unsorted)) % 34.54/34.73 (define @t22 () (@var "Xb" $$unsorted)) % 34.54/34.73 (define @t23 () (@var "Xc" $$unsorted)) % 34.54/34.73 (define @t24 () (@var "Xp" $$unsorted)) % 34.54/34.73 (define @t25 () (tptp.ip @t20 @t24 @t23 @t22 @t21)) % 34.54/34.73 (define @t26 () (not (tptp.s_t @t22 @t21 @t23))) % 34.54/34.73 (define @t27 () (not (tptp.s_t @t20 @t24 @t23))) % 34.54/34.73 (define @t28 () (@list @t20 @t22)) % 34.54/34.73 (define @t29 () (@var "Xd" $$unsorted)) % 34.54/34.73 (define @t30 () (tptp.s_e @t20 @t22 @t23 @t29)) % 34.54/34.73 (define @t31 () (not @t30)) % 34.54/34.73 (define @t32 () (@list @t20 @t22 @t23 @t29)) % 34.54/34.73 (define @t33 () (@var "Xf" $$unsorted)) % 34.54/34.73 (define @t34 () (@var "Xe" $$unsorted)) % 34.54/34.73 (define @t35 () (@list @t20 @t22 @t23 @t29 @t34 @t33)) % 34.54/34.73 (define @t36 () (@var "Xc1" $$unsorted)) % 34.54/34.73 (define @t37 () (@var "Xa1" $$unsorted)) % 34.54/34.73 (define @t38 () (tptp.s_e @t20 @t23 @t37 @t36)) % 34.54/34.73 (define @t39 () (@var "Xb1" $$unsorted)) % 34.54/34.73 (define @t40 () (not (tptp.s_e @t22 @t23 @t39 @t36))) % 34.54/34.73 (define @t41 () (tptp.s_e @t20 @t22 @t37 @t39)) % 34.54/34.73 (define @t42 () (not @t41)) % 34.54/34.73 (define @t43 () (tptp.s_t @t37 @t39 @t36)) % 34.54/34.73 (define @t44 () (not @t43)) % 34.54/34.73 (define @t45 () (tptp.s_t @t20 @t22 @t23)) % 34.54/34.73 (define @t46 () (not @t45)) % 34.54/34.73 (define @t47 () (@list @t20 @t22 @t23 @t37 @t39 @t36)) % 34.54/34.73 (define @t48 () (= @t22 @t23)) % 34.54/34.73 (define @t49 () (@var "XC" $$unsorted)) % 34.54/34.73 (define @t50 () (@var "XA" $$unsorted)) % 34.54/34.73 (define @t51 () (@var "XB" $$unsorted)) % 34.54/34.73 (define @t52 () (@list @t20 @t22 @t23)) % 34.54/34.73 (define @t53 () (= @t20 @t22)) % 34.54/34.73 (define @t54 () (tptp.s_t @t22 @t23 @t29)) % 34.54/34.73 (define @t55 () (not @t54)) % 34.54/34.73 (define @t56 () (tptp.s_t @t20 @t22 @t29)) % 34.54/34.73 (define @t57 () (not @t56)) % 34.54/34.73 (define @t58 () (@list @t20 @t22 @t29 @t23)) % 34.54/34.73 (define @t59 () (tptp.s_t @t20 @t23 @t29)) % 34.54/34.73 (define @t60 () (not @t59)) % 34.54/34.73 (define @t61 () (tptp.ext @t20 @t22 tptp.alpha tptp.gamma)) % 34.54/34.73 (define @t62 () (tptp.crossbar @t20 @t22 @t23 @t37 @t39 @t24)) % 34.54/34.73 (define @t63 () (not (tptp.s_t @t20 @t24 @t37))) % 34.54/34.73 (define @t64 () (not (tptp.s_t @t37 @t39 @t23))) % 34.54/34.73 (define @t65 () (@list @t20 @t22 @t23 @t37 @t39 @t24)) % 34.54/34.73 (define @t66 () (@var "Xd1" $$unsorted)) % 34.54/34.73 (define @t67 () (tptp.s_e @t22 @t29 @t39 @t66)) % 34.54/34.73 (define @t68 () (@list @t20 @t22 @t23 @t29 @t37 @t39 @t36 @t66)) % 34.54/34.73 (define @t69 () (not @t38)) % 34.54/34.73 (define @t70 () (tptp.insert @t20 @t22 @t37 @t36)) % 34.54/34.73 (define @t71 () (@list @t20 @t22 @t23 @t37 @t36)) % 34.54/34.73 (define @t72 () (tptp.s_e3 @t20 @t22 @t23 @t37 @t39 @t36)) % 34.54/34.73 (define @t73 () (not @t72)) % 34.54/34.73 (define @t74 () (tptp.s_col @t22 @t23 @t20)) % 34.54/34.73 (define @t75 () (tptp.s_col @t20 @t22 @t23)) % 34.54/34.73 (define @t76 () (not @t75)) % 34.54/34.73 (define @t77 () (tptp.s_col @t23 @t20 @t22)) % 34.54/34.73 (define @t78 () (tptp.s_e @t23 @t29 @t36 @t66)) % 34.54/34.73 (define @t79 () (tptp.s_fs @t20 @t22 @t23 @t29 @t37 @t39 @t36 @t66)) % 34.54/34.73 (define @t80 () (not @t79)) % 34.54/34.73 (define @t81 () (@list @t20 @t22 @t23 @t24 @t21)) % 34.54/34.73 (define @t82 () (= @t23 @t36)) % 34.54/34.73 (define @t83 () (not (tptp.s_e @t22 @t23 @t22 @t36))) % 34.54/34.73 (define @t84 () (not (tptp.s_e @t20 @t23 @t20 @t36))) % 34.54/34.73 (define @t85 () (tptp.s_t @t20 @t23 @t22)) % 34.54/34.73 (define @t86 () (tptp.insert @t20 @t22 @t23 @t29)) % 34.54/34.73 (define @t87 () (tptp.ins @t23 @t29 @t20 @t22)) % 34.54/34.73 (define @t88 () (tptp.le @t20 @t22 @t23 @t29)) % 34.54/34.73 (define @t89 () (not @t88)) % 34.54/34.73 (define @t90 () (or @t89 (= @t87 (tptp.ext @t20 @t22 @t86 @t29)))) % 34.54/34.73 (define @t91 () (or @t89 (tptp.s_e @t20 @t87 @t23 @t29))) % 34.54/34.73 (define @t92 () (or @t89 (tptp.s_t @t20 @t22 @t87))) % 34.54/34.73 (define @t93 () (forall @t32 (and @t92 @t91 @t90))) % 34.54/34.73 (define @t94 () (tptp.le @t23 @t29 @t20 @t22)) % 34.54/34.73 (define @t95 () (tptp.le @t20 @t22 @t20 @t23)) % 34.54/34.73 (define @t96 () (tptp.le @t22 @t23 @t20 @t23)) % 34.54/34.73 (define @t97 () (= @t23 @t22)) % 34.54/34.73 (define @t98 () (forall @t52 (or @t46 (not (tptp.s_e @t20 @t23 @t20 @t22)) @t97))) % 34.54/34.73 (define @t99 () (tptp.sameside @t20 @t24 @t22)) % 34.54/34.73 (define @t100 () (tptp.s_t @t22 @t24 @t23)) % 34.54/34.73 (define @t101 () (not @t100)) % 34.54/34.73 (define @t102 () (= @t23 @t24)) % 34.54/34.73 (define @t103 () (= @t22 @t24)) % 34.54/34.73 (define @t104 () (= @t20 @t24)) % 34.54/34.73 (define @t105 () (or @t104 @t103 @t102 @t27 @t101 @t99)) % 34.54/34.73 (define @t106 () (@list @t20 @t24 @t22 @t23)) % 34.54/34.73 (define @t107 () (forall @t106 @t105)) % 34.54/34.73 (define @t108 () (not @t99)) % 34.54/34.73 (define @t109 () (tptp.c63 @t20 @t24 @t22)) % 34.54/34.73 (define @t110 () (or @t108 (tptp.s_t @t22 @t24 @t109))) % 34.54/34.73 (define @t111 () (or @t108 (tptp.s_t @t20 @t24 @t109))) % 34.54/34.73 (define @t112 () (not (= @t109 @t24))) % 34.54/34.73 (define @t113 () (or @t108 @t112)) % 34.54/34.73 (define @t114 () (not @t103)) % 34.54/34.73 (define @t115 () (or @t108 @t114)) % 34.54/34.73 (define @t116 () (not @t104)) % 34.54/34.73 (define @t117 () (or @t108 @t116)) % 34.54/34.73 (define @t118 () (and @t117 @t115 @t113 @t111 @t110)) % 34.54/34.73 (define @t119 () (@list @t20 @t24 @t22)) % 34.54/34.73 (define @t120 () (forall @t119 @t118)) % 34.54/34.73 (define @t121 () (tptp.s_t @t20 @t24 @t22)) % 34.54/34.73 (define @t122 () (or @t108 (not @t121))) % 34.54/34.73 (define @t123 () (tptp.s_col @t20 @t24 @t22)) % 34.54/34.73 (define @t124 () (or @t108 @t123)) % 34.54/34.73 (define @t125 () (forall @t119 (and @t124 @t122))) % 34.54/34.73 (define @t126 () (@list @t20 @t24)) % 34.54/34.73 (define @t127 () (@var "Xr" $$unsorted)) % 34.54/34.73 (define @t128 () (tptp.insert @t22 @t23 @t20 @t127)) % 34.54/34.73 (define @t129 () (= @t127 @t20)) % 34.54/34.73 (define @t130 () (= @t24 @t21)) % 34.54/34.73 (define @t131 () (tptp.s_t @t24 @t20 @t22)) % 34.54/34.73 (define @t132 () (tptp.le @t24 @t20 @t24 @t22)) % 34.54/34.73 (define @t133 () (not @t131)) % 34.54/34.73 (define @t134 () (tptp.sameside @t20 @t24 @t127)) % 34.54/34.73 (define @t135 () (tptp.sameside @t20 @t24 @t21)) % 34.54/34.73 (define @t136 () (tptp.s_col @t20 @t24 @t21)) % 34.54/34.73 (define @t137 () (not (tptp.s_t @t21 @t24 @t127))) % 34.54/34.73 (define @t138 () (= @t24 @t127)) % 34.54/34.73 (define @t139 () (@list @t24 @t21 @t127 @t20)) % 34.54/34.73 (define @t140 () (tptp.s_t @t23 @t20 @t22)) % 34.54/34.73 (define @t141 () (not @t140)) % 34.54/34.73 (define @t142 () (@var "Xcs" $$unsorted)) % 34.54/34.73 (define @t143 () (tptp.s_col @t24 @t21 @t127)) % 34.54/34.73 (define @t144 () (not @t143)) % 34.54/34.73 (define @t145 () (tptp.s_col @t24 @t21 @t142)) % 34.54/34.73 (define @t146 () (not @t145)) % 34.54/34.73 (define @t147 () (tptp.s_col @t24 @t21 @t22)) % 34.54/34.73 (define @t148 () (not @t147)) % 34.54/34.73 (define @t149 () (tptp.s_col @t24 @t21 @t20)) % 34.54/34.73 (define @t150 () (not @t149)) % 34.54/34.73 (define @t151 () (@list @t20 @t22 @t24 @t21 @t127)) % 34.54/34.73 (define @t152 () (= @t23 @t29)) % 34.54/34.73 (define @t153 () (not (tptp.s_col @t20 @t22 @t29))) % 34.54/34.73 (define @t154 () (tptp.s_col @t24 @t21 @t23)) % 34.54/34.73 (define @t155 () (not @t154)) % 34.54/34.73 (define @t156 () (not (tptp.s_e @t22 @t20 @t39 @t37))) % 34.54/34.73 (define @t157 () (not (tptp.sameside @t20 @t22 @t23))) % 34.54/34.73 (define @t158 () (@var "Xm" $$unsorted)) % 34.54/34.73 (define @t159 () (tptp.s_m @t20 @t158 @t22)) % 34.54/34.73 (define @t160 () (not @t159)) % 34.54/34.73 (define @t161 () (@list @t20 @t158 @t22)) % 34.54/34.73 (define @t162 () (= @t158 @t20)) % 34.54/34.73 (define @t163 () (tptp.s_m @t20 @t158 @t20)) % 34.54/34.73 (define @t164 () (@list @t20 @t158)) % 34.54/34.73 (define @t165 () (tptp.s @t20 @t24)) % 34.54/34.73 (define @t166 () (not (tptp.s_m @t24 @t20 @t21))) % 34.54/34.73 (define @t167 () (tptp.s @t20 @t21)) % 34.54/34.73 (define @t168 () (= @t24 @t20)) % 34.54/34.73 (define @t169 () (= @t165 @t24)) % 34.54/34.73 (define @t170 () (tptp.s @t20 @t127)) % 34.54/34.73 (define @t171 () (tptp.s_t @t165 @t167 @t170)) % 34.54/34.73 (define @t172 () (tptp.s_t @t24 @t21 @t127)) % 34.54/34.73 (define @t173 () (tptp.s_e @t165 @t167 @t170 (tptp.s @t20 @t142))) % 34.54/34.73 (define @t174 () (tptp.s_e @t24 @t21 @t127 @t142)) % 34.54/34.73 (define @t175 () (@list @t24 @t21 @t127 @t142 @t20)) % 34.54/34.73 (define @t176 () (tptp.s @t22 @t24)) % 34.54/34.73 (define @t177 () (@list @t20 @t22 @t24)) % 34.54/34.73 (define @t178 () (tptp.s_e @t158 @t20 @t158 @t22)) % 34.54/34.73 (define @t179 () (not @t178)) % 34.54/34.73 (define @t180 () (@list @t20 @t22 @t23 @t29 @t24)) % 34.54/34.73 (define @t181 () (@var "Xa2" $$unsorted)) % 34.54/34.73 (define @t182 () (@var "Xm2" $$unsorted)) % 34.54/34.73 (define @t183 () (@var "Xm1" $$unsorted)) % 34.54/34.73 (define @t184 () (tptp.s_t @t183 @t23 @t182)) % 34.54/34.73 (define @t185 () (@var "Xb2" $$unsorted)) % 34.54/34.73 (define @t186 () (tptp.s_kf @t37 @t183 @t39 @t23 @t185 @t182 @t181)) % 34.54/34.73 (define @t187 () (not @t186)) % 34.54/34.73 (define @t188 () (@list @t37 @t183 @t39 @t23 @t185 @t182 @t181)) % 34.54/34.73 (define @t189 () (tptp.s_m @t181 @t182 @t185)) % 34.54/34.73 (define @t190 () (not @t189)) % 34.54/34.73 (define @t191 () (tptp.s_m @t37 @t183 @t39)) % 34.54/34.73 (define @t192 () (not @t191)) % 34.54/34.73 (define @t193 () (tptp.s_e @t23 @t181 @t23 @t185)) % 34.54/34.73 (define @t194 () (not @t193)) % 34.54/34.73 (define @t195 () (tptp.s_e @t23 @t37 @t23 @t39)) % 34.54/34.73 (define @t196 () (not @t195)) % 34.54/34.73 (define @t197 () (tptp.s_t @t39 @t23 @t185)) % 34.54/34.73 (define @t198 () (not @t197)) % 34.54/34.73 (define @t199 () (tptp.s_t @t37 @t23 @t181)) % 34.54/34.73 (define @t200 () (not @t199)) % 34.54/34.73 (define @t201 () (tptp.s_r @t20 @t22 @t23)) % 34.54/34.73 (define @t202 () (not @t201)) % 34.54/34.73 (define @t203 () (tptp.s_r @t37 @t22 @t23)) % 34.54/34.73 (define @t204 () (@list @t20 @t22 @t23 @t37)) % 34.54/34.73 (define @t205 () (tptp.s @t22 @t23)) % 34.54/34.73 (define @t206 () (not @t203)) % 34.54/34.73 (define @t207 () (tptp.s_r @t37 @t39 @t36)) % 34.54/34.73 (define @t208 () (tptp.perpAt @t20 @t22 @t23 @t24 @t21)) % 34.54/34.73 (define @t209 () (not @t208)) % 34.54/34.73 (define @t210 () (not (tptp.perp @t20 @t22 @t24 @t21))) % 34.54/34.73 (define @t211 () (@list @t20 @t22 @t24 @t21)) % 34.54/34.73 (define @t212 () (tptp.g813 @t20 @t22 @t24 @t21 @t23)) % 34.54/34.73 (define @t213 () (tptp.f813 @t20 @t22 @t24 @t21 @t23)) % 34.54/34.73 (define @t214 () (not @t130)) % 34.54/34.73 (define @t215 () (@var "Xcx" $$unsorted)) % 34.54/34.73 (define @t216 () (@var "U" $$unsorted)) % 34.54/34.73 (define @t217 () (not (tptp.s_col @t20 @t22 @t216))) % 34.54/34.73 (define @t218 () (not (tptp.s_col @t20 @t22 @t21))) % 34.54/34.73 (define @t219 () (tptp.s_col @t20 @t22 @t24)) % 34.54/34.73 (define @t220 () (not @t219)) % 34.54/34.73 (define @t221 () (@list @t20 @t22 @t24 @t21 @t23)) % 34.54/34.73 (define @t222 () (tptp.il @t20 @t22 @t24 @t21)) % 34.54/34.73 (define @t223 () (tptp.perp @t20 @t22 @t23 @t29)) % 34.54/34.73 (define @t224 () (not @t223)) % 34.54/34.73 (define @t225 () (tptp.perp @t20 @t22 @t23 @t24)) % 34.54/34.73 (define @t226 () (not @t225)) % 34.54/34.73 (define @t227 () (tptp.s_r @t23 @t24 @t21)) % 34.54/34.73 (define @t228 () (= @t21 @t24)) % 34.54/34.73 (define @t229 () (tptp.foot @t20 @t22 @t23)) % 34.54/34.73 (define @t230 () (not (tptp.s_m (tptp.s @t20 @t23) @t24 @t205))) % 34.54/34.73 (define @t231 () (@list @t20 @t22 @t23 @t24)) % 34.54/34.73 (define @t232 () (not (tptp.s_col @t23 @t29 @t24))) % 34.54/34.73 (define @t233 () (tptp.erect21a @t20 @t22 @t23)) % 34.54/34.73 (define @t234 () (tptp.erectAux21a @t20 @t22 @t23)) % 34.54/34.73 (define @t235 () (tptp.erect @t20 @t22 @t23)) % 34.54/34.73 (define @t236 () (tptp.erectAux @t20 @t22 @t23)) % 34.54/34.73 (define @t237 () (@var "Xt" $$unsorted)) % 34.54/34.73 (define @t238 () (not (tptp.s_col @t20 @t22 @t237))) % 34.54/34.73 (define @t239 () (not (tptp.s_t @t24 @t237 @t21))) % 34.54/34.73 (define @t240 () (tptp.midpoint @t20 @t22)) % 34.54/34.73 (define @t241 () (not (= @t215 (tptp.ip @t24 @t237 @t21 @t22 @t127)))) % 34.54/34.73 (define @t242 () (not (tptp.s_e @t20 @t24 @t22 @t127))) % 34.54/34.73 (define @t243 () (not (tptp.s_t @t22 @t127 @t21))) % 34.54/34.73 (define @t244 () (not (tptp.perp @t21 @t22 @t20 @t22))) % 34.54/34.73 (define @t245 () (not (tptp.perp @t24 @t20 @t20 @t22))) % 34.54/34.73 (define @t246 () (@list @t24 @t20 @t22 @t21 @t237 @t127 @t215)) % 34.54/34.73 (define @t247 () (tptp.s_col @t20 @t23 @t29)) % 34.54/34.73 (define @t248 () (tptp.perp @t24 @t21 @t23 @t29)) % 34.54/34.73 (define @t249 () (@list @t20 @t22 @t24 @t21 @t23 @t29)) % 34.54/34.73 (define @t250 () (= @t20 @t23)) % 34.54/34.73 (define @t251 () (not (tptp.samesideline @t24 @t21 @t20 @t22))) % 34.54/34.73 (define @t252 () (tptp.samesideline @t24 @t21 @t22 @t20)) % 34.54/34.73 (define @t253 () (tptp.opposite @t20 @t24 @t21 @t22)) % 34.54/34.73 (define @t254 () (not @t253)) % 34.54/34.73 (define @t255 () (@list @t20 @t24 @t21 @t22)) % 34.54/34.73 (define @t256 () (tptp.opposite @t22 @t24 @t21 @t23)) % 34.54/34.73 (define @t257 () (not (tptp.sameside @t20 @t127 @t22))) % 34.54/34.73 (define @t258 () (not (tptp.s_m @t20 @t158 @t23))) % 34.54/34.73 (define @t259 () (not (tptp.s_col @t24 @t21 @t158))) % 34.54/34.73 (define @t260 () (tptp.opposite @t20 @t24 @t21 @t23)) % 34.54/34.73 (define @t261 () (not @t260)) % 34.54/34.73 (define @t262 () (@list @t20 @t24 @t21 @t23 @t158 @t127 @t22)) % 34.54/34.73 (define @t263 () (tptp.sameside (tptp.s @t158 @t216) @t142 @t23)) % 34.54/34.73 (define @t264 () (= @t127 @t142)) % 34.54/34.73 (define @t265 () (not (tptp.le @t142 @t23 @t127 @t20))) % 34.54/34.73 (define @t266 () (tptp.sameside @t216 @t127 @t20)) % 34.54/34.73 (define @t267 () (not @t266)) % 34.54/34.73 (define @t268 () (not (tptp.s_m @t127 @t158 @t142))) % 34.54/34.73 (define @t269 () (not (tptp.perp @t24 @t21 @t23 @t142))) % 34.54/34.73 (define @t270 () (not (tptp.perp @t24 @t21 @t20 @t127))) % 34.54/34.73 (define @t271 () (@list @t20 @t24 @t21 @t23 @t142 @t127 @t158 @t216)) % 34.54/34.73 (define @t272 () (tptp.op @t21 @t22 @t24 @t23 @t20)) % 34.54/34.73 (define @t273 () (not (tptp.s_t @t20 @t23 @t24))) % 34.54/34.73 (define @t274 () (tptp.samesideline @t20 @t22 @t24 @t21)) % 34.54/34.73 (define @t275 () (not @t274)) % 34.54/34.73 (define @t276 () (not (tptp.samesideline @t22 @t23 @t24 @t21))) % 34.54/34.73 (define @t277 () (= @t29 @t34)) % 34.54/34.73 (define @t278 () (= @t24 (tptp.foot @t24 @t21 @t127))) % 34.54/34.73 (define @t279 () (tptp.opposite @t127 @t24 @t21 @t142)) % 34.54/34.73 (define @t280 () (tptp.samesideline @t127 @t142 @t24 @t21)) % 34.54/34.73 (define @t281 () (@list @t24 @t21 @t127 @t142)) % 34.54/34.73 (define @t282 () (tptp.reflect @t20 @t22 @t24)) % 34.54/34.73 (define @t283 () (@var "Xp1" $$unsorted)) % 34.54/34.73 (define @t284 () (= @t283 @t282)) % 34.54/34.73 (define @t285 () (not (tptp.s_col @t20 @t22 (tptp.midpoint @t24 @t283)))) % 34.54/34.73 (define @t286 () (@list @t20 @t22 @t24 @t283)) % 34.54/34.73 (define @t287 () (tptp.reflect @t20 @t22 @t283)) % 34.54/34.73 (define @t288 () (not (= @t282 @t283))) % 34.54/34.73 (define @t289 () (tptp.reflect @t20 @t22 @t21)) % 34.54/34.73 (define @t290 () (= @t282 @t24)) % 34.54/34.73 (define @t291 () (tptp.s_e @t24 @t21 @t282 @t289)) % 34.54/34.73 (define @t292 () (not (tptp.s_e @t20 @t22 @t37 @t22))) % 34.54/34.73 (define @t293 () (not (tptp.s_r @t37 @t22 @t36))) % 34.54/34.73 (define @t294 () (tptp.erectsameside @t22 @t23 @t20 @t21)) % 34.54/34.73 (define @t295 () (tptp.s_col @t22 @t23 @t21)) % 34.54/34.73 (define @t296 () (not @t74)) % 34.54/34.73 (define @t297 () (tptp.triangle @t20 @t22 @t23 @t37 @t39 @t24)) % 34.54/34.73 (define @t298 () (tptp.s_col @t37 @t39 @t24)) % 34.54/34.73 (define @t299 () (@var "Xc2" $$unsorted)) % 34.54/34.73 (define @t300 () (tptp.ext @t34 @t33 @t22 @t23)) % 34.54/34.73 (define @t301 () (tptp.ext @t34 @t29 @t22 @t20)) % 34.54/34.73 (define @t302 () (tptp.ext @t22 @t23 @t34 @t33)) % 34.54/34.73 (define @t303 () (tptp.ext @t22 @t20 @t34 @t29)) % 34.54/34.73 (define @t304 () (tptp.congruent @t20 @t22 @t23 @t29 @t34 @t33)) % 34.54/34.73 (define @t305 () (not @t304)) % 34.54/34.73 (define @t306 () (or @t305 (tptp.s_e3 @t303 @t22 @t302 @t301 @t34 @t300))) % 34.54/34.73 (define @t307 () (or @t305 (tptp.sameside @t300 @t34 @t33))) % 34.54/34.73 (define @t308 () (or @t305 (tptp.sameside @t301 @t34 @t29))) % 34.54/34.73 (define @t309 () (or @t305 (tptp.sameside @t302 @t22 @t23))) % 34.54/34.73 (define @t310 () (or @t305 (tptp.sameside @t303 @t22 @t20))) % 34.54/34.73 (define @t311 () (forall @t35 (and @t310 @t309 @t308 @t307 @t306))) % 34.54/34.73 (define @t312 () (@var "Xf1" $$unsorted)) % 34.54/34.73 (define @t313 () (not (tptp.s_e3 @t37 @t22 @t36 @t66 @t34 @t312))) % 34.54/34.73 (define @t314 () (tptp.f113f @t20 @t22 @t23 @t29 @t34 @t33)) % 34.54/34.73 (define @t315 () (tptp.f113d @t20 @t22 @t23 @t29 @t34 @t33)) % 34.54/34.73 (define @t316 () (tptp.f113c @t20 @t22 @t23 @t29 @t34 @t33)) % 34.54/34.73 (define @t317 () (tptp.f113a @t20 @t22 @t23 @t29 @t34 @t33)) % 34.54/34.73 (define @t318 () (= @t33 @t34)) % 34.54/34.73 (define @t319 () (@var "Xf2" $$unsorted)) % 34.54/34.73 (define @t320 () (@var "Xd2" $$unsorted)) % 34.54/34.73 (define @t321 () (tptp.s_e @t181 @t299 @t320 @t319)) % 34.54/34.73 (define @t322 () (not (tptp.s_e @t22 @t299 @t34 @t319))) % 34.54/34.73 (define @t323 () (not (tptp.s_e @t22 @t181 @t34 @t320))) % 34.54/34.73 (define @t324 () (not (tptp.sameside @t319 @t34 @t33))) % 34.54/34.73 (define @t325 () (not (tptp.sameside @t320 @t34 @t29))) % 34.54/34.73 (define @t326 () (not (tptp.sameside @t299 @t22 @t23))) % 34.54/34.73 (define @t327 () (not (tptp.sameside @t181 @t22 @t20))) % 34.54/34.73 (define @t328 () (tptp.sameside @t312 @t34 @t319)) % 34.54/34.73 (define @t329 () (not @t328)) % 34.54/34.73 (define @t330 () (not (tptp.sameside @t66 @t34 @t320))) % 34.54/34.73 (define @t331 () (not (tptp.sameside @t36 @t22 @t299))) % 34.54/34.73 (define @t332 () (not (tptp.sameside @t37 @t22 @t181))) % 34.54/34.73 (define @t333 () (or @t332 @t331 @t330 @t329 @t313 @t53 @t97 @t277 @t318 @t327 @t326 @t325 @t324 @t323 @t322 @t321)) % 34.54/34.73 (define @t334 () (@list @t37 @t22 @t181 @t36 @t299 @t66 @t34 @t320 @t312 @t319 @t20 @t23 @t29 @t33)) % 34.54/34.73 (define @t335 () (forall @t334 @t333)) % 34.54/34.73 (define @t336 () (@var "Xc3" $$unsorted)) % 34.54/34.73 (define @t337 () (@var "Xb3" $$unsorted)) % 34.54/34.73 (define @t338 () (@var "Xa3" $$unsorted)) % 34.54/34.73 (define @t339 () (tptp.constructAngle @t20 @t22 @t23 @t29 @t34 @t24)) % 34.54/34.73 (define @t340 () (tptp.s_col @t29 @t34 @t24)) % 34.54/34.73 (define @t341 () (forall @t47 (or (not (tptp.congruent @t20 @t22 @t23 @t37 @t39 @t36)) @t156 @t40 @t38))) % 34.54/34.73 (define @t342 () (not @t341)) % 34.54/34.73 (define @t343 () (@var "Zd" $$unsorted)) % 34.54/34.73 (define @t344 () (@var "Zc" $$unsorted)) % 34.54/34.73 (define @t345 () (@var "Zb" $$unsorted)) % 34.54/34.73 (define @t346 () (@var "Za" $$unsorted)) % 34.54/34.73 (define @t347 () (tptp.s_afs @t20 @t22 @t23 @t29 @t346 @t345 @t344 @t343)) % 34.54/34.73 (define @t348 () (tptp.s_e @t22 @t29 @t345 @t343)) % 34.54/34.73 (define @t349 () (tptp.s_e @t20 @t29 @t346 @t343)) % 34.54/34.73 (define @t350 () (not @t349)) % 34.54/34.73 (define @t351 () (tptp.s_e @t22 @t23 @t345 @t344)) % 34.54/34.73 (define @t352 () (not @t351)) % 34.54/34.73 (define @t353 () (tptp.s_e @t20 @t22 @t346 @t345)) % 34.54/34.73 (define @t354 () (tptp.s_t @t346 @t345 @t344)) % 34.54/34.73 (define @t355 () (not @t354)) % 34.54/34.73 (define @t356 () (not @t347)) % 34.54/34.73 (define @t357 () (@list @t20 @t22 @t23 @t29 @t346 @t345 @t344 @t343)) % 34.54/34.73 (define @t358 () (tptp.s_ifs @t20 @t22 @t23 @t29 @t346 @t345 @t344 @t343)) % 34.54/34.73 (define @t359 () (tptp.s_e @t23 @t29 @t344 @t343)) % 34.54/34.73 (define @t360 () (tptp.s_e @t20 @t23 @t346 @t344)) % 34.54/34.73 (define @t361 () (not @t358)) % 34.54/34.73 (define @t362 () (tptp.s_e3 @t37 @t181 @t338 @t39 @t185 @t337)) % 34.54/34.73 (define @t363 () (tptp.s_e @t181 @t338 @t185 @t337)) % 34.54/34.73 (define @t364 () (tptp.s_e @t37 @t338 @t39 @t337)) % 34.54/34.73 (define @t365 () (tptp.s_e @t37 @t181 @t39 @t185)) % 34.54/34.73 (define @t366 () (not @t362)) % 34.54/34.73 (define @t367 () (tptp.s_t @t22 @t23 @t20)) % 34.54/34.73 (define @t368 () (tptp.s_e @t20 @t29 @t37 @t66)) % 34.54/34.73 (define @t369 () (tptp.s_t @t24 @t22 @t20)) % 34.54/34.73 (define @t370 () (tptp.s_t @t20 @t158 @t22)) % 34.54/34.73 (define @t371 () (tptp.s_e @t20 @t23 @t20 @t205)) % 34.54/34.73 (define @t372 () (tptp.g811 @t2 @t7 @t17 @t16 @t1)) % 34.54/34.73 (define @t373 () (tptp.f811 @t2 @t7 @t17 @t16 @t1)) % 34.54/34.73 (define @t374 () (tptp.s_col @t17 @t16 @t1)) % 34.54/34.73 (define @t375 () (not @t374)) % 34.54/34.73 (define @t376 () (tptp.s_col @t2 @t7 @t1)) % 34.54/34.73 (define @t377 () (not @t376)) % 34.54/34.73 (define @t378 () (= @t17 @t16)) % 34.54/34.73 (define @t379 () (= @t2 @t7)) % 34.54/34.73 (define @t380 () (tptp.perpAt @t2 @t7 @t1 @t17 @t16)) % 34.54/34.73 (define @t381 () (not @t380)) % 34.54/34.73 (define @t382 () (@var "Xq1" $$unsorted)) % 34.54/34.73 (define @t383 () (tptp.perp @t24 @t21 @t283 @t382)) % 34.54/34.73 (define @t384 () (@var "Xv" $$unsorted)) % 34.54/34.73 (define @t385 () (@var "Xu" $$unsorted)) % 34.54/34.73 (define @t386 () (tptp.ss2 @t20 @t22 @t24 @t21)) % 34.54/34.73 (define @t387 () (tptp.ss3 @t20 @t22 @t24 @t21)) % 34.54/34.73 (define @t388 () (tptp.ss1 @t20 @t22 @t24 @t21)) % 34.54/34.73 (define @t389 () (@quantifiers_skolemize @t341 3)) % 34.54/34.73 (define @t390 () (@quantifiers_skolemize @t341 4)) % 34.54/34.73 (define @t391 () (@quantifiers_skolemize @t341 0)) % 34.54/34.73 (define @t392 () (@quantifiers_skolemize @t341 1)) % 34.54/34.73 (define @t393 () (tptp.s_e @t392 @t391 @t390 @t389)) % 34.54/34.73 (define @t394 () (@quantifiers_skolemize @t341 5)) % 34.54/34.73 (define @t395 () (@quantifiers_skolemize @t341 2)) % 34.54/34.73 (define @t396 () (tptp.s_e @t391 @t395 @t389 @t394)) % 34.54/34.73 (define @t397 () (tptp.s_e @t392 @t395 @t390 @t394)) % 34.54/34.73 (define @t398 () (not @t397)) % 34.54/34.73 (define @t399 () (not @t393)) % 34.54/34.73 (define @t400 () (tptp.congruent @t391 @t392 @t395 @t389 @t390 @t394)) % 34.54/34.73 (define @t401 () (not @t400)) % 34.54/34.73 (define @t402 () (or @t401 @t399 @t398 @t396)) % 34.54/34.73 (define @t403 () (@list true)) % 34.54/34.73 (define @t404 () (@list @t402)) % 34.54/34.73 (define @t405 () (forall @t35 @t306)) % 34.54/34.73 (define @t406 () (@list @t20 @t22 @t23 @t29 @t34 @t33)) % 34.54/34.73 (define @t407 () (forall @t35 @t307)) % 34.54/34.73 (define @t408 () (@var "BOUND_VARIABLE_10167" $$unsorted)) % 34.54/34.73 (define @t409 () (@var "BOUND_VARIABLE_10165" $$unsorted)) % 34.54/34.73 (define @t410 () (@var "BOUND_VARIABLE_10163" $$unsorted)) % 34.54/34.73 (define @t411 () (@var "BOUND_VARIABLE_10161" $$unsorted)) % 34.54/34.73 (define @t412 () (@var "BOUND_VARIABLE_10159" $$unsorted)) % 34.54/34.73 (define @t413 () (@var "BOUND_VARIABLE_10157" $$unsorted)) % 34.54/34.73 (define @t414 () (forall @t35 @t308)) % 34.54/34.73 (define @t415 () (forall @t35 @t309)) % 34.54/34.73 (define @t416 () (forall @t35 @t310)) % 34.54/34.73 (define @t417 () (and @t416 @t415 @t414 @t407 @t405)) % 34.54/34.73 (define @t418 () (@list @t391 @t392 @t395 @t389 @t390 @t394)) % 34.54/34.73 (define @t419 () (tptp.ext @t392 @t391 @t390 @t389)) % 34.54/34.73 (define @t420 () (tptp.sameside @t419 @t392 @t391)) % 34.54/34.73 (define @t421 () (or @t401 @t420)) % 34.54/34.73 (define @t422 () (@list false false)) % 34.54/34.73 (define @t423 () (tptp.ext @t392 @t395 @t390 @t394)) % 34.54/34.73 (define @t424 () (tptp.sameside @t423 @t392 @t395)) % 34.54/34.73 (define @t425 () (or @t401 @t424)) % 34.54/34.73 (define @t426 () (tptp.ext @t390 @t389 @t392 @t391)) % 34.54/34.73 (define @t427 () (tptp.sameside @t426 @t390 @t389)) % 34.54/34.73 (define @t428 () (or @t401 @t427)) % 34.54/34.73 (define @t429 () (tptp.ext @t390 @t394 @t392 @t395)) % 34.54/34.73 (define @t430 () (tptp.sameside @t429 @t390 @t394)) % 34.54/34.73 (define @t431 () (or @t401 @t430)) % 34.54/34.73 (define @t432 () (tptp.s_e3 @t419 @t392 @t423 @t426 @t390 @t429)) % 34.54/34.73 (define @t433 () (or @t401 @t432)) % 34.54/34.73 (define @t434 () (@list @t419 @t392 @t391)) % 34.54/34.73 (define @t435 () (tptp.sameside @t391 @t392 @t419)) % 34.54/34.73 (define @t436 () (not @t420)) % 34.54/34.73 (define @t437 () (or @t436 @t435)) % 34.54/34.73 (define @t438 () (@list @t423 @t392 @t395)) % 34.54/34.73 (define @t439 () (tptp.sameside @t395 @t392 @t423)) % 34.54/34.73 (define @t440 () (not @t424)) % 34.54/34.73 (define @t441 () (or @t440 @t439)) % 34.54/34.73 (define @t442 () (@list @t429 @t390 @t394)) % 34.54/34.73 (define @t443 () (tptp.sameside @t394 @t390 @t429)) % 34.54/34.73 (define @t444 () (not @t430)) % 34.54/34.73 (define @t445 () (or @t444 @t443)) % 34.54/34.73 (define @t446 () (tptp.ins @t390 @t394 @t390 @t394)) % 34.54/34.73 (define @t447 () (tptp.s_e @t390 @t446 @t390 @t394)) % 34.54/34.73 (define @t448 () (not @t447)) % 34.54/34.73 (define @t449 () (tptp.s_t @t390 @t394 @t446)) % 34.54/34.73 (define @t450 () (not @t449)) % 34.54/34.73 (define @t451 () (or @t450 @t448 (= @t446 @t394))) % 34.54/34.73 (define @t452 () (= @t394 @t446)) % 34.54/34.73 (define @t453 () (or @t450 @t448 @t452)) % 34.54/34.73 (define @t454 () (@list false)) % 34.54/34.73 (define @t455 () (@list @t98)) % 34.54/34.73 (define @t456 () (forall @t32 @t90)) % 34.54/34.73 (define @t457 () (@list @t20 @t22 @t23 @t29)) % 34.54/34.73 (define @t458 () (forall @t32 @t91)) % 34.54/34.73 (define @t459 () (forall @t32 @t92)) % 34.54/34.73 (define @t460 () (and @t459 @t458 @t456)) % 34.54/34.73 (define @t461 () (@list @t390 @t394 @t390 @t394)) % 34.54/34.73 (define @t462 () (@list @t392 @t395)) % 34.54/34.73 (define @t463 () (tptp.le @t390 @t394 @t390 @t394)) % 34.54/34.73 (define @t464 () (tptp.le @t392 @t395 @t392 @t395)) % 34.54/34.73 (define @t465 () (not @t464)) % 34.54/34.73 (define @t466 () (or @t465 @t398 @t398 @t463)) % 34.54/34.73 (define @t467 () (@list false false false)) % 34.54/34.73 (define @t468 () (not @t463)) % 34.54/34.73 (define @t469 () (or @t468 @t447)) % 34.54/34.73 (define @t470 () (or @t468 @t449)) % 34.54/34.73 (define @t471 () (@var "BOUND_VARIABLE_9265" $$unsorted)) % 34.54/34.73 (define @t472 () (@var "BOUND_VARIABLE_9263" $$unsorted)) % 34.54/34.73 (define @t473 () (@var "BOUND_VARIABLE_9261" $$unsorted)) % 34.54/34.73 (define @t474 () (forall (@list @t473 @t472 @t471) (or (not (tptp.sameside @t473 @t472 @t471)) (tptp.s_t @t471 @t472 (tptp.c63 @t473 @t472 @t471))))) % 34.54/34.73 (define @t475 () (@var "BOUND_VARIABLE_9251" $$unsorted)) % 34.54/34.73 (define @t476 () (@var "BOUND_VARIABLE_9249" $$unsorted)) % 34.54/34.73 (define @t477 () (@var "BOUND_VARIABLE_9247" $$unsorted)) % 34.54/34.73 (define @t478 () (forall (@list @t477 @t476 @t475) (or (not (tptp.sameside @t477 @t476 @t475)) (tptp.s_t @t477 @t476 (tptp.c63 @t477 @t476 @t475))))) % 34.54/34.73 (define @t479 () (@var "BOUND_VARIABLE_9236" $$unsorted)) % 34.54/34.73 (define @t480 () (@var "BOUND_VARIABLE_9234" $$unsorted)) % 34.54/34.73 (define @t481 () (@var "BOUND_VARIABLE_9232" $$unsorted)) % 34.54/34.73 (define @t482 () (forall (@list @t481 @t480 @t479) (or (not (tptp.sameside @t481 @t480 @t479)) (not (= @t480 (tptp.c63 @t481 @t480 @t479)))))) % 34.54/34.73 (define @t483 () (@var "BOUND_VARIABLE_9223" $$unsorted)) % 34.54/34.73 (define @t484 () (@var "BOUND_VARIABLE_9219" $$unsorted)) % 34.54/34.73 (define @t485 () (not (tptp.sameside @t484 @t483 @t483))) % 34.54/34.73 (define @t486 () (not (= @t483 @t483))) % 34.54/34.73 (define @t487 () (or @t485 @t486)) % 34.54/34.73 (define @t488 () (@list @t484 @t483)) % 34.54/34.73 (define @t489 () (@var "BOUND_VARIABLE_9221" $$unsorted)) % 34.54/34.73 (define @t490 () (not (= @t489 @t483))) % 34.54/34.73 (define @t491 () (not (tptp.sameside @t484 @t489 @t483))) % 34.54/34.73 (define @t492 () (or @t490 @t491 @t490)) % 34.54/34.73 (define @t493 () (@list @t489)) % 34.54/34.73 (define @t494 () (or @t491 @t490)) % 34.54/34.73 (define @t495 () (forall @t493 @t494)) % 34.54/34.73 (define @t496 () (forall @t488 @t495)) % 34.54/34.73 (define @t497 () (forall (@list @t484 @t483 @t489) @t494)) % 34.54/34.73 (define @t498 () (forall (@list @t484 @t489 @t483) @t494)) % 34.54/34.73 (define @t499 () (@var "BOUND_VARIABLE_9210" $$unsorted)) % 34.54/34.73 (define @t500 () (@var "BOUND_VARIABLE_9208" $$unsorted)) % 34.54/34.73 (define @t501 () (not (tptp.sameside @t500 @t500 @t499))) % 34.54/34.73 (define @t502 () (not (= @t500 @t500))) % 34.54/34.73 (define @t503 () (or @t501 @t502)) % 34.54/34.73 (define @t504 () (@list @t500 @t499)) % 34.54/34.73 (define @t505 () (@var "BOUND_VARIABLE_9206" $$unsorted)) % 34.54/34.73 (define @t506 () (not (= @t505 @t500))) % 34.54/34.73 (define @t507 () (not (tptp.sameside @t505 @t500 @t499))) % 34.54/34.73 (define @t508 () (or @t506 @t507 @t506)) % 34.54/34.73 (define @t509 () (@list @t505)) % 34.54/34.73 (define @t510 () (or @t507 @t506)) % 34.54/34.73 (define @t511 () (forall @t509 @t510)) % 34.54/34.73 (define @t512 () (forall @t504 @t511)) % 34.54/34.73 (define @t513 () (forall (@list @t500 @t499 @t505) @t510)) % 34.54/34.73 (define @t514 () (forall (@list @t505 @t500 @t499) @t510)) % 34.54/34.73 (define @t515 () (forall @t119 @t110)) % 34.54/34.73 (define @t516 () (@list @t20 @t24 @t22)) % 34.54/34.73 (define @t517 () (forall @t119 @t111)) % 34.54/34.73 (define @t518 () (or @t108 (not (= @t24 @t109)))) % 34.54/34.73 (define @t519 () (forall @t119 @t518)) % 34.54/34.73 (define @t520 () (= @t24 @t22)) % 34.54/34.73 (define @t521 () (or @t108 (not @t520))) % 34.54/34.73 (define @t522 () (forall @t119 @t521)) % 34.54/34.73 (define @t523 () (forall @t119 @t117)) % 34.54/34.73 (define @t524 () (and @t523 @t522 @t519 @t517 @t515)) % 34.54/34.73 (define @t525 () (tptp.c63 @t429 @t390 @t394)) % 34.54/34.73 (define @t526 () (= @t390 @t525)) % 34.54/34.73 (define @t527 () (not @t526)) % 34.54/34.73 (define @t528 () (or @t444 @t527)) % 34.54/34.73 (define @t529 () (tptp.s_t @t394 @t390 @t525)) % 34.54/34.73 (define @t530 () (or @t444 @t529)) % 34.54/34.73 (define @t531 () (tptp.sameside @t394 @t390 @t394)) % 34.54/34.73 (define @t532 () (not @t529)) % 34.54/34.73 (define @t533 () (= @t390 @t394)) % 34.54/34.73 (define @t534 () (or (= @t394 @t390) @t533 @t526 @t532 @t532 @t531)) % 34.54/34.73 (define @t535 () (forall @t106 (or @t104 @t520 (= @t24 @t23) @t27 @t101 @t99))) % 34.54/34.73 (define @t536 () (or @t533 @t533 @t526 @t532 @t532 @t531)) % 34.54/34.73 (define @t537 () (@list @t535)) % 34.54/34.73 (define @t538 () (forall @t13 @t11)) % 34.54/34.73 (define @t539 () (@list @t1 @t2 @t9 @t6)) % 34.54/34.73 (define @t540 () (forall @t13 @t12)) % 34.54/34.73 (define @t541 () (and @t540 @t538)) % 34.54/34.73 (define @t542 () (= @t392 @t423)) % 34.54/34.73 (define @t543 () (not @t542)) % 34.54/34.73 (define @t544 () (tptp.s_t @t392 @t395 @t392)) % 34.54/34.73 (define @t545 () (tptp.s_t @t392 @t395 @t423)) % 34.54/34.73 (define @t546 () (not @t545)) % 34.54/34.73 (define @t547 () (not @t544)) % 34.54/34.73 (define @t548 () (= true false)) % 34.54/34.73 (define @t549 () (and @t547 @t542 @t545)) % 34.54/34.73 (define @t550 () (= @t392 @t395)) % 34.54/34.73 (define @t551 () (or @t547 @t550)) % 34.54/34.73 (define @t552 () (forall @t119 @t122)) % 34.54/34.73 (define @t553 () (forall @t119 @t124)) % 34.54/34.73 (define @t554 () (and @t553 @t552)) % 34.54/34.73 (define @t555 () (tptp.s_t @t423 @t392 @t395)) % 34.54/34.73 (define @t556 () (not @t555)) % 34.54/34.73 (define @t557 () (or @t440 @t556)) % 34.54/34.73 (define @t558 () (tptp.s_t @t392 @t395 @t395)) % 34.54/34.73 (define @t559 () (not @t558)) % 34.54/34.73 (define @t560 () (not @t550)) % 34.54/34.73 (define @t561 () (and @t556 @t542 @t550 @t558)) % 34.54/34.73 (define @t562 () (@list false true false false false false)) % 34.54/34.73 (define @t563 () (forall (@list @t413 @t412 @t411 @t410 @t409 @t408) (or (not (tptp.congruent @t413 @t412 @t411 @t410 @t409 @t408)) (tptp.sameside (tptp.ext @t409 @t408 @t412 @t411) @t409 @t408)))) % 34.54/34.73 (define @t564 () (not @t402)) % 34.54/34.73 (define @t565 () (@list @t426 @t390 @t389)) % 34.54/34.73 (define @t566 () (tptp.c63 @t426 @t390 @t389)) % 34.54/34.73 (define @t567 () (= @t390 @t566)) % 34.54/34.73 (define @t568 () (not @t567)) % 34.54/34.73 (define @t569 () (not @t427)) % 34.54/34.73 (define @t570 () (or @t569 @t568)) % 34.54/34.73 (define @t571 () (tptp.s_t @t389 @t390 @t566)) % 34.54/34.73 (define @t572 () (or @t569 @t571)) % 34.54/34.73 (define @t573 () (tptp.sameside @t389 @t390 @t389)) % 34.54/34.73 (define @t574 () (not @t571)) % 34.54/34.73 (define @t575 () (= @t389 @t390)) % 34.54/34.73 (define @t576 () (or @t575 (= @t390 @t389) @t567 @t574 @t574 @t573)) % 34.54/34.73 (define @t577 () (or @t575 @t575 @t567 @t574 @t574 @t573)) % 34.54/34.73 (define @t578 () (tptp.s_t @t392 @t391 @t392)) % 34.54/34.73 (define @t579 () (= @t392 @t419)) % 34.54/34.73 (define @t580 () (not @t579)) % 34.54/34.73 (define @t581 () (tptp.s_t @t392 @t391 @t419)) % 34.54/34.73 (define @t582 () (not @t581)) % 34.54/34.73 (define @t583 () (not @t578)) % 34.54/34.73 (define @t584 () (and @t583 @t579 @t581)) % 34.54/34.73 (define @t585 () (or @t583 (= @t392 @t391))) % 34.54/34.73 (define @t586 () (@list @t392 @t391)) % 34.54/34.73 (define @t587 () (= @t391 @t392)) % 34.54/34.73 (define @t588 () (or @t583 @t587)) % 34.54/34.73 (define @t589 () (tptp.s_t @t419 @t392 @t391)) % 34.54/34.73 (define @t590 () (not @t589)) % 34.54/34.73 (define @t591 () (or @t436 @t590)) % 34.54/34.73 (define @t592 () (tptp.s_t @t392 @t391 @t391)) % 34.54/34.73 (define @t593 () (not @t592)) % 34.54/34.73 (define @t594 () (not @t587)) % 34.54/34.73 (define @t595 () (and @t590 @t579 @t587 @t592)) % 34.54/34.73 (define @t596 () (not @t531)) % 34.54/34.73 (define @t597 () (not @t573)) % 34.54/34.73 (define @t598 () (not @t439)) % 34.54/34.73 (define @t599 () (not @t435)) % 34.54/34.73 (define @t600 () (not @t432)) % 34.54/34.73 (define @t601 () (= @t423 @t392)) % 34.54/34.73 (define @t602 () (= @t419 @t392)) % 34.54/34.73 (define @t603 () (or @t436 @t440 @t569 @t444 @t600 @t602 @t601 @t575 @t533 @t599 @t598 @t597 @t596 @t399 @t398 @t396)) % 34.54/34.73 (define @t604 () (forall @t334 (or @t332 @t331 @t330 @t329 @t313 @t53 @t97 @t277 (= @t34 @t33) @t327 @t326 @t325 @t324 @t323 @t322 @t321))) % 34.54/34.73 (define @t605 () (or @t436 @t440 @t569 @t444 @t600 @t579 @t542 @t575 @t533 @t599 @t598 @t597 @t596 @t399 @t398 @t396)) % 34.54/34.73 (define @t606 () (@list @t604)) % 34.54/34.73 (define @t607 () (tptp.sameside @t389 @t390 @t426)) % 34.54/34.73 (define @t608 () (or @t569 @t607)) % 34.54/34.73 (define @t609 () (not @t607)) % 34.54/34.73 (define @t610 () (= @t426 @t390)) % 34.54/34.73 (define @t611 () (or @t436 @t440 @t569 @t444 @t600 @t602 @t601 @t610 @t533 @t599 @t598 @t609 @t596 @t399 @t398 @t396)) % 34.54/34.73 (define @t612 () (= @t390 @t426)) % 34.54/34.73 (define @t613 () (or @t436 @t440 @t569 @t444 @t600 @t579 @t542 @t612 @t533 @t599 @t598 @t609 @t596 @t399 @t398 @t396)) % 34.54/34.73 (define @t614 () (@list @t390 @t389 @t390 @t389)) % 34.54/34.73 (define @t615 () (tptp.le @t390 @t389 @t390 @t389)) % 34.54/34.73 (define @t616 () (tptp.le @t392 @t391 @t392 @t391)) % 34.54/34.73 (define @t617 () (not @t616)) % 34.54/34.73 (define @t618 () (or @t617 @t399 @t399 @t615)) % 34.54/34.73 (define @t619 () (tptp.ins @t390 @t389 @t390 @t389)) % 34.54/34.73 (define @t620 () (tptp.s_t @t390 @t389 @t619)) % 34.54/34.73 (define @t621 () (not @t615)) % 34.54/34.73 (define @t622 () (or @t621 @t620)) % 34.54/34.73 (define @t623 () (tptp.s_t @t426 @t390 @t389)) % 34.54/34.73 (define @t624 () (not @t623)) % 34.54/34.73 (define @t625 () (or @t569 @t624)) % 34.54/34.73 (define @t626 () (tptp.s_e @t390 @t619 @t390 @t389)) % 34.54/34.73 (define @t627 () (not @t626)) % 34.54/34.73 (define @t628 () (not @t620)) % 34.54/34.73 (define @t629 () (or @t628 @t627 (= @t619 @t389))) % 34.54/34.73 (define @t630 () (= @t389 @t619)) % 34.54/34.73 (define @t631 () (or @t628 @t627 @t630)) % 34.54/34.73 (define @t632 () (or @t621 @t626)) % 34.54/34.73 (define @t633 () (not @t612)) % 34.54/34.73 (define @t634 () (not @t630)) % 34.54/34.73 (define @t635 () (not @t575)) % 34.54/34.73 (define @t636 () (= false true)) % 34.54/34.73 (define @t637 () (and @t620 @t575 @t612 @t630 @t624)) % 34.54/34.73 (define @t638 () (tptp.s_t @t429 @t390 @t394)) % 34.54/34.73 (define @t639 () (not @t638)) % 34.54/34.73 (define @t640 () (or @t444 @t639)) % 34.54/34.73 (define @t641 () (= @t390 @t429)) % 34.54/34.73 (define @t642 () (not @t641)) % 34.54/34.73 (define @t643 () (not @t452)) % 34.54/34.73 (define @t644 () (not @t533)) % 34.54/34.73 (define @t645 () (and @t449 @t533 @t641 @t452 @t639)) % 34.54/34.73 (define @t646 () (@list true false false false)) % 34.54/34.73 (define @t647 () (not @t443)) % 34.54/34.73 (define @t648 () (or @t436 @t440 @t569 @t444 @t600 @t602 @t601 @t575 @t641 @t599 @t598 @t597 @t647 @t399 @t398 @t396)) % 34.54/34.73 (define @t649 () (or @t436 @t440 @t569 @t444 @t600 @t579 @t542 @t575 @t641 @t599 @t598 @t597 @t647 @t399 @t398 @t396)) % 34.54/34.73 (define @t650 () (or @t436 @t440 @t569 @t444 @t600 @t602 @t601 @t610 @t641 @t599 @t598 @t609 @t647 @t399 @t398 @t396)) % 34.54/34.73 (define @t651 () (or @t436 @t440 @t569 @t444 @t600 @t579 @t542 @t612 @t641 @t599 @t598 @t609 @t647 @t399 @t398 @t396)) % 34.54/34.73 (assume @p1 (forall @t3 (tptp.s_e @t1 @t2 @t2 @t1))) % 34.54/34.73 (assume @p2 (forall (@list @t1 @t2 @t7 @t6 @t5 @t4) (or (not (tptp.s_e @t1 @t2 @t7 @t6)) (not (tptp.s_e @t1 @t2 @t5 @t4)) (tptp.s_e @t7 @t6 @t5 @t4)))) % 34.54/34.73 (assume @p3 (forall (@list @t1 @t2 @t7) (or (not (tptp.s_e @t1 @t2 @t7 @t7)) @t8))) % 34.54/34.73 (assume @p4 @t14) % 34.54/34.73 (assume @p5 (forall (@list @t1 @t2 @t18 @t17 @t7 @t16 @t6 @t15) (or (not (tptp.s_e @t1 @t2 @t18 @t17)) (not (tptp.s_e @t2 @t7 @t17 @t16)) (not (tptp.s_e @t1 @t6 @t18 @t15)) (not (tptp.s_e @t2 @t6 @t17 @t15)) (not (tptp.s_t @t1 @t2 @t7)) (not (tptp.s_t @t18 @t17 @t16)) @t8 (tptp.s_e @t7 @t6 @t16 @t15)))) % 34.54/34.73 (assume @p6 @t19) % 34.54/34.73 (assume @p7 (forall (@list @t20 @t24 @t23 @t22 @t21) (and (or @t27 @t26 (tptp.s_t @t24 @t25 @t22)) (or @t27 @t26 (tptp.s_t @t21 @t25 @t20))))) % 34.54/34.73 (assume @p8 (and (not (tptp.s_t tptp.alpha tptp.beta tptp.gamma)) (not (tptp.s_t tptp.beta tptp.gamma tptp.alpha)) (not (tptp.s_t tptp.gamma tptp.alpha tptp.beta)))) % 34.54/34.73 (assume @p9 (forall @t28 (tptp.s_e @t20 @t22 @t20 @t22))) % 34.54/34.73 (assume @p10 (forall @t32 (or @t31 (tptp.s_e @t23 @t29 @t20 @t22)))) % 34.54/34.73 (assume @p11 (forall @t35 (or @t31 (not (tptp.s_e @t23 @t29 @t34 @t33)) (tptp.s_e @t20 @t22 @t34 @t33)))) % 34.54/34.73 (assume @p12 (forall @t32 (or @t31 (tptp.s_e @t22 @t20 @t23 @t29)))) % 34.54/34.73 (assume @p13 (forall @t32 (or @t31 (tptp.s_e @t20 @t22 @t29 @t23)))) % 34.54/34.73 (assume @p14 (forall @t28 (tptp.s_e @t20 @t20 @t22 @t22))) % 34.54/34.73 (assume @p15 (forall @t47 (or @t46 @t44 @t42 @t40 @t38))) % 34.54/34.73 (assume @p16 (forall (@list @t21 @t20 @t29 @t22 @t23) (or (= @t21 @t20) (not (tptp.s_t @t21 @t20 @t29)) (not (tptp.s_e @t20 @t29 @t22 @t23)) (= @t29 (tptp.ext @t21 @t20 @t22 @t23))))) % 34.54/34.73 (assume @p17 (forall (@list @t22 @t23 @t20) (or (not (tptp.s_e @t22 @t23 @t20 @t20)) @t48))) % 34.54/34.73 (assume @p18 (forall @t32 (or @t31 (tptp.s_e @t22 @t20 @t29 @t23)))) % 34.54/34.73 (assume @p19 (forall (@list @t20 @t22 @t23 @t50 @t51 @t49) (or @t46 (not (tptp.s_t @t50 @t51 @t49)) (not (tptp.s_e @t20 @t22 @t51 @t49)) (not (tptp.s_e @t22 @t23 @t50 @t51)) (tptp.s_e @t20 @t23 @t50 @t49)))) % 34.54/34.73 (assume @p20 (forall @t28 (tptp.s_t @t20 @t22 @t22))) % 34.54/34.73 (assume @p21 (forall @t52 (or @t46 (tptp.s_t @t23 @t22 @t20)))) % 34.54/34.73 (assume @p22 (forall (@list @t37 @t39) (tptp.s_t @t37 @t37 @t39))) % 34.54/34.73 (assume @p23 (forall @t52 (or @t46 (not (tptp.s_t @t22 @t20 @t23)) @t53))) % 34.54/34.73 (assume @p24 (forall @t58 (or @t57 @t55 @t45))) % 34.54/34.73 (assume @p25 (forall @t32 (or @t46 @t60 @t54))) % 34.54/34.73 (assume @p26 (forall @t32 (or @t46 @t55 @t48 @t59))) % 34.54/34.73 (assume @p27 (forall @t58 (or @t57 @t55 @t59))) % 34.54/34.73 (assume @p28 (forall @t32 (or @t46 @t60 @t56))) % 34.54/34.73 (assume @p29 (forall @t32 (or @t46 @t55 @t48 @t56))) % 34.54/34.73 (assume @p30 (not (= tptp.alpha tptp.beta))) % 34.54/34.73 (assume @p31 (not (= tptp.beta tptp.gamma))) % 34.54/34.73 (assume @p32 (not (= tptp.alpha tptp.gamma))) % 34.54/34.73 (assume @p33 (forall @t28 (tptp.s_t @t20 @t22 @t61))) % 34.54/34.73 (assume @p34 (forall (@list @t22 @t20) (not (= @t22 @t61)))) % 34.54/34.73 (assume @p35 (forall @t65 (and (or @t46 @t64 @t63 (tptp.s_t @t24 @t62 @t23)) (or @t46 @t64 @t63 (tptp.s_t @t22 @t62 @t39))))) % 34.54/34.73 (assume @p36 (forall @t68 (or (not (tptp.s_ifs @t20 @t22 @t23 @t29 @t37 @t39 @t36 @t66)) @t67))) % 34.54/34.73 (assume @p37 (forall @t47 (or @t46 @t44 @t69 @t40 @t41))) % 34.54/34.73 (assume @p38 (forall @t71 (and (or @t46 @t69 (tptp.s_t @t37 @t70 @t36)) (or @t46 @t69 (tptp.s_e3 @t20 @t22 @t23 @t37 @t70 @t36))))) % 34.54/34.73 (assume @p39 (forall @t47 (or @t46 @t73 @t43))) % 34.54/34.73 (assume @p40 (forall @t52 (or @t76 @t74))) % 34.54/34.73 (assume @p41 (forall @t52 (or @t76 @t77))) % 34.54/34.73 (assume @p42 (forall @t52 (or @t76 (tptp.s_col @t23 @t22 @t20)))) % 34.54/34.73 (assume @p43 (forall @t52 (or @t76 (tptp.s_col @t22 @t20 @t23)))) % 34.54/34.73 (assume @p44 (forall @t52 (or @t76 (tptp.s_col @t20 @t23 @t22)))) % 34.54/34.73 (assume @p45 (forall @t28 (tptp.s_col @t20 @t20 @t22))) % 34.54/34.73 (assume @p46 (forall @t28 (tptp.s_col @t20 @t22 @t20))) % 34.54/34.73 (assume @p47 (forall @t47 (or @t76 @t73 (tptp.s_col @t37 @t39 @t36)))) % 34.54/34.73 (assume @p48 (forall (@list @t20 @t22 @t23 @t37 @t39) (or @t76 @t42 (tptp.s_e3 @t20 @t22 @t23 @t37 @t39 (tptp.insert5 @t20 @t22 @t23 @t37 @t39))))) % 34.54/34.73 (assume @p49 (forall @t68 (or @t80 @t53 @t78))) % 34.54/34.73 (assume @p50 (forall @t81 (or @t53 @t76 (not (tptp.s_e @t20 @t24 @t20 @t21)) (not (tptp.s_e @t22 @t24 @t22 @t21)) (tptp.s_e @t23 @t24 @t23 @t21)))) % 34.54/34.73 (assume @p51 (forall (@list @t20 @t22 @t23 @t36) (or @t53 @t76 @t84 @t83 @t82))) % 34.54/34.73 (assume @p52 (forall (@list @t20 @t23 @t22 @t36) (or (not @t85) @t84 @t83 @t82))) % 34.54/34.73 (assume @p53 (forall @t32 (or @t53 @t46 @t57 @t59 (tptp.s_t @t20 @t29 @t23)))) % 34.54/34.73 (assume @p54 (forall @t32 (or @t53 @t46 @t57 @t54 (tptp.s_t @t22 @t29 @t23)))) % 34.54/34.73 (assume @p55 (forall @t58 (or @t57 @t60 @t45 @t85))) % 34.54/34.73 (assume @p56 @t93) % 34.54/34.73 (assume @p57 (forall (@list @t20 @t22 @t23 @t29 @t34) (or @t88 (not (tptp.s_t @t20 @t22 @t34)) (not (tptp.s_e @t20 @t34 @t23 @t29))))) % 34.54/34.73 (assume @p58 (forall @t68 (or @t89 @t42 (not @t78) (tptp.le @t37 @t39 @t36 @t66)))) % 34.54/34.73 (assume @p59 (forall @t28 (tptp.le @t20 @t22 @t20 @t22))) % 34.54/34.73 (assume @p60 (forall @t35 (or @t89 (not (tptp.le @t23 @t29 @t34 @t33)) (tptp.le @t20 @t22 @t34 @t33)))) % 34.54/34.73 (assume @p61 (forall @t32 (or @t89 (not @t94) @t30))) % 34.54/34.73 (assume @p62 (forall @t32 (or @t88 @t94))) % 34.54/34.73 (assume @p63 (forall (@list @t20 @t23 @t29) (tptp.le @t20 @t20 @t23 @t29))) % 34.54/34.73 (assume @p64 (forall @t52 (or @t76 @t46 @t95))) % 34.54/34.73 (assume @p65 (forall @t52 (or @t76 @t46 @t96))) % 34.54/34.73 (assume @p66 @t98) % 34.54/34.73 (assume @p67 (forall @t52 (or @t76 @t45 (not @t95) (not @t96)))) % 34.54/34.73 (assume @p68 @t107) % 34.54/34.73 (assume @p69 (forall @t106 (or @t104 @t103 @t102 @t27 @t100 @t108))) % 34.54/34.73 (assume @p70 @t120) % 34.54/34.73 (assume @p71 (forall @t106 (or @t99 @t104 @t103 @t102 @t27 @t101))) % 34.54/34.73 (assume @p72 @t125) % 34.54/34.73 (assume @p73 (forall @t119 (or @t99 (not @t123) @t121))) % 34.54/34.73 (assume @p74 (forall @t126 (or @t104 (tptp.sameside @t20 @t24 @t20)))) % 34.54/34.73 (assume @p75 (forall @t119 (or @t108 (tptp.sameside @t22 @t24 @t20)))) % 34.54/34.73 (assume @p76 (forall @t106 (or @t108 (not (tptp.sameside @t22 @t24 @t23)) (tptp.sameside @t20 @t24 @t23)))) % 34.54/34.73 (assume @p77 (forall (@list @t127 @t20 @t22 @t23) (and (or @t129 @t48 (tptp.sameside @t128 @t20 @t127)) (or @t129 @t48 (tptp.s_e @t20 @t128 @t22 @t23))))) % 34.54/34.73 (assume @p78 (forall (@list @t127 @t20 @t22 @t23 @t24 @t21) (or @t129 @t48 (not (tptp.sameside @t24 @t20 @t127)) (not (tptp.s_e @t20 @t24 @t22 @t23)) (not (tptp.sameside @t21 @t20 @t127)) (not (tptp.s_e @t20 @t21 @t22 @t23)) @t130))) % 34.54/34.73 (assume @p79 (forall @t119 (or @t108 (not @t132) @t131))) % 34.54/34.73 (assume @p80 (forall @t119 (or @t108 @t132 @t133))) % 34.54/34.73 (assume @p81 (forall @t139 (or @t130 @t138 @t137 (not @t136) @t104 @t135 @t134))) % 34.54/34.73 (assume @p82 (forall @t139 (or @t130 @t138 @t137 (not @t135) @t136))) % 34.54/34.73 (assume @p83 (forall @t139 (or @t130 @t138 @t137 (not @t134) @t136))) % 34.54/34.73 (assume @p84 (forall @t139 (or @t130 @t138 @t137 @t116 @t136))) % 34.54/34.73 (assume @p85 (forall @t32 (or @t53 @t141 (not (tptp.s_t @t29 @t20 @t22)) (tptp.s_t @t29 @t23 @t22) (tptp.s_t @t23 @t29 @t22)))) % 34.54/34.73 (assume @p86 (forall (@list @t24 @t21 @t142 @t127) (or @t130 (= @t142 @t24) @t146 @t144 (tptp.s_col @t24 @t142 @t127)))) % 34.54/34.73 (assume @p87 (forall (@list @t24 @t21) (or @t130 (tptp.s_col @t24 @t21 @t24)))) % 34.54/34.73 (assume @p88 (forall (@list @t24 @t21 @t127) (or @t130 @t144 (tptp.s_col @t21 @t24 @t127)))) % 34.54/34.73 (assume @p89 (forall @t151 (or @t53 @t130 @t150 @t148 @t144 (tptp.s_col @t20 @t22 @t127)))) % 34.54/34.73 (assume @p90 (forall (@list @t20 @t22 @t24 @t21 @t23 @t29 @t34) (or @t53 @t130 @t76 @t155 @t153 (not (tptp.s_col @t24 @t21 @t29)) @t152 (not (tptp.s_col @t20 @t22 @t34)) (tptp.s_col @t24 @t21 @t34)))) % 34.54/34.73 (assume @p91 (forall @t28 (or @t53 (not (tptp.s_col @t20 @t22 (tptp.pointOffLine @t20 @t22)))))) % 34.54/34.73 (assume @p92 (forall @t47 (or @t157 (not (tptp.sameside @t37 @t39 @t36)) @t156 @t40 @t38))) % 34.54/34.73 (assume @p93 (forall @t161 (or @t160 (tptp.s_m @t22 @t158 @t20)))) % 34.54/34.73 (assume @p94 (forall @t164 (or (not @t163) @t162))) % 34.54/34.73 (assume @p95 (forall @t164 (or @t163 (not @t162)))) % 34.54/34.73 (assume @p96 (forall (@list @t24 @t20) (tptp.s_m @t24 @t20 @t165))) % 34.54/34.73 (assume @p97 (forall (@list @t24 @t20 @t127 @t21) (or (not (tptp.s_m @t24 @t20 @t127)) @t166 (= @t127 @t21)))) % 34.54/34.73 (assume @p98 (forall (@list @t24 @t20 @t21) (or @t166 (= @t21 @t165)))) % 34.54/34.73 (assume @p99 (forall @t126 (= (tptp.s @t20 @t165) @t24))) % 34.54/34.73 (assume @p100 (forall (@list @t20 @t24 @t127 @t21) (or (not (= @t165 @t127)) (not (= @t167 @t127)) @t130))) % 34.54/34.73 (assume @p101 (forall (@list @t20 @t24 @t21) (or (not (= @t165 @t167)) @t130))) % 34.54/34.73 (assume @p102 (forall @t126 (or (not @t169) @t168))) % 34.54/34.73 (assume @p103 (forall @t126 (or @t169 (not @t168)))) % 34.54/34.73 (assume @p104 (forall (@list @t24 @t21 @t20) (tptp.s_e @t24 @t21 @t165 @t167))) % 34.54/34.73 (assume @p105 (forall @t139 (or (not @t172) @t171))) % 34.54/34.73 (assume @p106 (forall @t139 (or @t172 (not @t171)))) % 34.54/34.73 (assume @p107 (forall @t175 (or (not @t174) @t173))) % 34.54/34.73 (assume @p108 (forall @t175 (or @t174 (not @t173)))) % 34.54/34.73 (assume @p109 (forall (@list @t24 @t20 @t21 @t22) (or @t166 (not (tptp.s_m @t24 @t22 @t21)) @t53))) % 34.54/34.73 (assume @p110 (forall @t119 (or (not (= @t165 @t176)) @t53))) % 34.54/34.73 (assume @p111 (forall @t177 (or (not (= (tptp.s @t20 @t176) (tptp.s @t22 @t165))) @t53))) % 34.54/34.73 (assume @p112 (forall @t161 (or (not (tptp.s_col @t20 @t158 @t22)) @t179 @t53 @t159))) % 34.54/34.73 (assume @p113 (forall @t180 (or @t75 (= @t22 @t29) @t31 (not (tptp.s_e @t22 @t23 @t29 @t20)) (not (tptp.s_col @t20 @t24 @t23)) (not (tptp.s_col @t22 @t24 @t29)) (tptp.s_m @t20 @t24 @t23)))) % 34.54/34.73 (assume @p114 (forall @t188 (or @t187 @t184 (not (tptp.le @t23 @t37 @t23 @t181))))) % 34.54/34.73 (assume @p115 (forall @t188 (or @t187 @t184))) % 34.54/34.73 (assume @p116 (forall (@list @t37 @t23 @t181 @t39 @t185 @t183 @t182) (or @t200 @t198 @t196 @t194 @t192 @t190 @t184))) % 34.54/34.73 (assume @p117 (forall (@list @t23 @t20 @t22) (or (not (tptp.s_e @t23 @t20 @t23 @t22)) (tptp.s_m @t20 (tptp.isomidpoint @t20 @t22 @t23) @t22)))) % 34.54/34.73 (assume @p118 (forall @t52 (or @t202 (tptp.s_r @t23 @t22 @t20)))) % 34.54/34.73 (assume @p119 (forall @t204 (or @t202 @t53 (not (tptp.s_col @t22 @t20 @t37)) @t203))) % 34.54/34.73 (assume @p120 (forall @t52 (or @t202 (tptp.s_r @t20 @t22 @t205)))) % 34.54/34.73 (assume @p121 (forall @t28 (tptp.s_r @t20 @t22 @t22))) % 34.54/34.73 (assume @p122 (forall @t204 (or @t202 @t206 (not (tptp.s_t @t20 @t23 @t37)) @t48))) % 34.54/34.73 (assume @p123 (forall @t52 (or @t202 (not (tptp.s_r @t20 @t23 @t22)) @t48))) % 34.54/34.73 (assume @p124 (forall @t28 (or (not (tptp.s_r @t20 @t22 @t20)) @t53))) % 34.54/34.73 (assume @p125 (forall @t52 (or @t202 @t76 @t53 @t97))) % 34.54/34.73 (assume @p126 (forall @t47 (or @t202 @t73 @t207))) % 34.54/34.73 (assume @p127 (forall @t81 (or @t209 (tptp.perpAt @t24 @t21 @t23 @t20 @t22)))) % 34.54/34.73 (assume @p128 (forall @t211 (or @t210 (tptp.perp @t24 @t21 @t20 @t22)))) % 34.54/34.73 (assume @p129 (forall @t81 (and (or @t209 (not @t53)) (or @t209 @t214) (or @t209 @t154) (or @t209 @t75) (or @t209 (tptp.s_col @t20 @t22 @t213)) (or @t209 (tptp.s_col @t24 @t21 @t212)) (or @t209 (not (= @t23 @t213))) (or @t209 (not (= @t23 @t212))) (or @t209 (tptp.s_r @t213 @t23 @t212))))) % 34.54/34.73 (assume @p130 (forall (@list @t20 @t22 @t24 @t21 @t215 @t216 @t6) (or @t53 @t130 (not (tptp.s_col @t24 @t21 @t215)) (not (tptp.s_col @t20 @t22 @t215)) @t217 (not (tptp.s_col @t24 @t21 @t6)) (= @t215 @t216) (= @t215 @t6) (not (tptp.s_r @t216 @t215 @t6)) (tptp.perpAt @t20 @t22 @t215 @t24 @t21)))) % 34.54/34.73 (assume @p131 (forall @t211 (or @t210 @t220 @t218))) % 34.54/34.73 (assume @p132 (forall @t221 (or @t210 @t76 @t155 @t208))) % 34.54/34.73 (assume @p133 (forall @t81 (or @t209 (= @t23 @t222)))) % 34.54/34.73 (assume @p134 (forall @t58 (or @t53 @t153 @t224 (tptp.perpAt @t20 @t22 @t29 @t23 @t29)))) % 34.54/34.73 (assume @p135 (forall @t221 (and (or @t53 @t220 @t218 @t228 @t76 @t226) (or @t53 @t220 @t218 @t228 @t227 @t226)))) % 34.54/34.73 (assume @p136 (forall @t221 (or @t53 @t220 @t218 @t228 @t225 @t75 (not @t227)))) % 34.54/34.73 (assume @p137 (forall @t81 (or @t75 @t220 @t218 @t226 (not (tptp.perp @t20 @t22 @t23 @t21)) @t130))) % 34.54/34.73 (assume @p138 (forall @t52 (and (or @t75 (tptp.s_col @t20 @t22 @t229)) (or @t75 (tptp.perp @t20 @t22 @t23 @t229))))) % 34.54/34.73 (assume @p139 (forall @t231 (or @t202 @t230 (tptp.s_r @t22 @t20 @t24)))) % 34.54/34.73 (assume @p140 (forall @t231 (or @t202 @t230 @t48 @t116))) % 34.54/34.73 (assume @p141 (forall @t211 (or @t210 (tptp.perp @t22 @t20 @t24 @t21)))) % 34.54/34.73 (assume @p142 (forall @t180 (or @t53 @t152 @t76 @t153 @t232 @t219))) % 34.54/34.73 (assume @p143 (forall @t52 (and (or @t53 (tptp.perp @t20 @t22 @t233 @t20) @t75) (or @t53 (tptp.s_col @t20 @t22 @t234) @t75) (or @t53 (tptp.s_t @t23 @t234 @t233) @t75)))) % 34.54/34.73 (assume @p144 (forall @t52 (and (or @t53 (tptp.perp @t20 @t22 @t235 @t20)) (or @t53 (tptp.s_col @t20 @t22 @t236)) (or @t53 (tptp.s_t @t23 @t236 @t235))))) % 34.54/34.73 (assume @p145 (forall (@list @t20 @t24 @t22 @t21 @t237) (or (not (tptp.le @t20 @t24 @t22 @t21)) (not (tptp.perp @t20 @t22 @t20 @t24)) (not (tptp.perp @t20 @t22 @t22 @t21)) @t239 @t238 (tptp.s_m @t20 (tptp.midpointAux @t20 @t22 @t24 @t21 @t237) @t22)))) % 34.54/34.73 (assume @p146 (forall @t28 (tptp.s_m @t20 @t240 @t22))) % 34.54/34.73 (assume @p147 (forall @t246 (or @t245 @t244 @t238 @t239 @t243 @t242 @t241 (tptp.s_m @t20 @t215 @t22)))) % 34.54/34.73 (assume @p148 (forall @t246 (or @t245 @t244 @t238 @t239 @t243 @t242 @t241 (tptp.s_m @t24 @t215 @t127)))) % 34.54/34.73 (assume @p149 (forall (@list @t24 @t20 @t22 @t21 @t237 @t127) (or @t245 @t244 @t238 @t239 @t243 @t242 (tptp.s_m @t24 @t240 @t127)))) % 34.54/34.73 (assume @p150 (forall @t32 (or @t76 @t153 @t53 @t247))) % 34.54/34.73 (assume @p151 (forall (@list @t20 @t22 @t24 @t21 @t127 @t23 @t29) (or @t220 @t218 @t130 @t53 (not (tptp.perpAt @t24 @t21 @t127 @t23 @t29)) (tptp.perpAt @t20 @t22 @t127 @t23 @t29)))) % 34.54/34.73 (assume @p152 (forall @t249 (or @t220 @t218 @t130 @t53 (not @t248) @t223))) % 34.54/34.73 (assume @p153 (forall @t32 (or @t53 @t250 @t48 (= @t29 @t23) (= @t20 @t29) (not (tptp.perp @t22 @t20 @t20 @t23)) (not @t247) (tptp.perp @t22 @t20 @t20 @t29)))) % 34.54/34.73 (assume @p154 (forall @t211 (or @t210 (tptp.perp @t20 @t22 @t21 @t24)))) % 34.54/34.73 (assume @p155 (forall @t249 (or @t220 @t218 @t130 @t53 @t248 @t224))) % 34.54/34.73 (assume @p156 (or (not (tptp.s_col tptp.xa tptp.xb tptp.xp)) (not (tptp.s_col tptp.xa tptp.xb tptp.xq)) (= tptp.xp tptp.xq) (= tptp.xa tptp.xb) (tptp.perp tptp.xc tptp.xd tptp.xp tptp.xq) (not (tptp.perp tptp.xc tptp.xd tptp.xa tptp.xb)))) % 34.54/34.73 (assume @p157 (forall @t81 (or @t76 @t53 @t250 @t251 (tptp.samesideline @t24 @t21 @t20 @t23)))) % 34.54/34.73 (assume @p158 (forall @t211 (or @t53 @t251 @t252))) % 34.54/34.73 (assume @p159 (forall @t255 (or @t254 (tptp.opposite @t22 @t24 @t21 @t20)))) % 34.54/34.73 (assume @p160 (forall @t262 (or @t261 @t259 @t258 @t144 @t257 @t256 (not (tptp.s_t @t127 @t22 @t20))))) % 34.54/34.73 (assume @p161 (forall @t262 (or @t261 @t259 @t258 @t144 @t257 @t256))) % 34.54/34.73 (assume @p162 (forall (@list @t20 @t22 @t23 @t158) (or @t157 (tptp.sameside (tptp.s @t158 @t20) (tptp.s @t158 @t22) (tptp.s @t158 @t23))))) % 34.54/34.73 (assume @p163 (forall @t271 (or @t261 @t130 @t146 @t144 @t270 @t269 @t268 @t267 @t265 @t264 @t263))) % 34.54/34.73 (assume @p164 (forall @t271 (or @t261 @t130 @t146 @t144 @t270 @t269 @t268 @t266 @t265 @t264 (not @t263)))) % 34.54/34.73 (assume @p165 (forall @t271 (or @t261 @t130 @t146 @t144 @t270 @t269 @t268 @t267 (not @t264) @t263))) % 34.54/34.73 (assume @p166 (forall @t271 (or @t261 @t130 @t146 @t144 @t270 @t269 @t268 @t267 @t263))) % 34.54/34.73 (assume @p167 (forall (@list @t20 @t24 @t21 @t23 @t142 @t127 @t158 @t216 @t6) (or @t261 @t130 @t146 @t144 @t270 @t269 @t268 @t267 (not (tptp.sameside @t6 @t142 @t23)) (tptp.opposite @t216 @t24 @t21 @t6)))) % 34.54/34.73 (assume @p168 (forall (@list @t20 @t24 @t21 @t23 @t127 @t22) (or @t261 @t144 @t257 @t256))) % 34.54/34.73 (assume @p169 (forall (@list @t20 @t23 @t24 @t22 @t21) (and (or @t273 @t26 (tptp.s_t @t20 @t272 @t22)) (or @t273 @t26 (tptp.s_t @t24 @t21 @t272))))) % 34.54/34.73 (assume @p170 (forall (@list @t20 @t24 @t21 @t23 @t22) (or @t261 @t256 @t275))) % 34.54/34.73 (assume @p171 (forall @t255 (or @t254 @t275))) % 34.54/34.73 (assume @p172 (forall (@list @t24 @t21 @t20 @t22 @t23) (or @t130 @t275 @t276 (tptp.samesideline @t20 @t23 @t24 @t21)))) % 34.54/34.73 (assume @p173 (forall (@list @t24 @t21 @t20 @t22) (or @t251 @t252))) % 34.54/34.73 (assume @p174 (forall (@list @t20 @t22 @t216 @t6 @t9) (or @t53 (not (tptp.s_m @t216 @t6 @t9)) @t217 (not (tptp.s_col @t20 @t22 @t9)) (tptp.s_col @t20 @t22 @t6)))) % 34.54/34.73 (assume @p175 (forall (@list @t29 @t34 @t66 @t20 @t22) (or @t277 (not (tptp.s_t @t34 @t29 @t66)) (not (tptp.samesideline @t20 @t22 @t66 @t34)) (tptp.samesideline @t20 @t22 @t29 @t34)))) % 34.54/34.73 (assume @p176 (forall @t211 (or @t53 @t251 (tptp.samesideline @t21 @t24 @t20 @t22)))) % 34.54/34.73 (assume @p177 (forall (@list @t20 @t24 @t21 @t22 @t23) (or @t254 @t276 @t260))) % 34.54/34.73 (assume @p178 (forall (@list @t24 @t21 @t23 @t20 @t22) (or @t130 (not (tptp.perpAt @t24 @t21 @t23 @t20 @t23)) (not (tptp.perpAt @t24 @t21 @t23 @t22 @t23)) @t250 @t77))) % 34.54/34.73 (assume @p179 (forall @t281 (or @t130 @t143 @t145 @t280 @t279 (not @t278)))) % 34.54/34.73 (assume @p180 (forall @t281 (or @t130 @t143 @t145 @t280 @t279 @t278))) % 34.54/34.73 (assume @p181 (forall @t281 (or @t130 @t143 @t145 @t280 @t279))) % 34.54/34.73 (assume @p182 (forall @t151 (or @t275 (not (tptp.sameside @t20 @t21 @t127)) (tptp.samesideline @t127 @t22 @t24 @t21)))) % 34.54/34.73 (assume @p183 (forall (@list @t23 @t29 @t24 @t20 @t22) (or @t152 @t232 @t220 @t108 (tptp.s_col @t23 @t29 @t20) (tptp.samesideline @t20 @t22 @t23 @t29)))) % 34.54/34.73 (assume @p184 (forall @t177 (and (or @t53 (tptp.s_col @t20 @t22 (tptp.midpoint @t24 @t282))) (or @t53 (= @t24 @t282) (tptp.perp @t20 @t22 @t24 @t282))))) % 34.54/34.73 (assume @p185 (forall @t286 (and (or @t53 @t285 (not (tptp.perp @t20 @t22 @t24 @t283)) @t284) (or @t53 @t285 (not (= @t24 @t283)) @t284)))) % 34.54/34.73 (assume @p186 (forall @t286 (or @t53 @t288 (= @t287 @t24)))) % 34.54/34.73 (assume @p187 (forall @t177 (or @t53 (= (tptp.reflect @t20 @t22 @t282) @t24)))) % 34.54/34.73 (assume @p188 (forall @t286 (or @t53 @t288 (= @t24 @t287)))) % 34.54/34.73 (assume @p189 (forall @t211 (or @t53 (not (= @t282 @t289)) @t130))) % 34.54/34.73 (assume @p190 (forall @t177 (or @t53 (not @t290) @t219))) % 34.54/34.73 (assume @p191 (forall @t177 (or @t53 @t220 @t290))) % 34.54/34.73 (assume @p192 (forall @t211 (or @t53 @t220 @t291))) % 34.54/34.73 (assume @p193 (forall @t211 (or @t53 @t291))) % 34.54/34.73 (assume @p194 (forall @t204 (or @t202 @t206 @t292 (tptp.s_e @t20 @t23 @t37 @t23)))) % 34.54/34.73 (assume @p195 (forall @t71 (or @t202 @t293 @t292 @t83 @t38 (not (= @t22 (tptp.midpoint @t23 @t36))) @t82))) % 34.54/34.73 (assume @p196 (forall @t71 (or @t202 @t293 @t292 @t83 @t38))) % 34.54/34.73 (assume @p197 (forall @t47 (or @t202 (not @t207) @t42 @t40 @t38))) % 34.54/34.73 (assume @p198 (forall @t286 (or @t53 @t288 @t219 (tptp.opposite @t24 @t20 @t22 @t283)))) % 34.54/34.73 (assume @p199 (forall (@list @t22 @t23 @t20 @t21) (and (or @t48 @t296 @t295 (tptp.perp @t22 @t23 @t294 @t20)) (or @t48 @t296 @t295 (tptp.samesideline @t294 @t21 @t22 @t23))))) % 34.54/34.73 (assume @p200 (forall @t65 (and (or @t53 @t75 @t298 @t42 (tptp.s_e3 @t20 @t22 @t23 @t37 @t39 @t297)) (or @t53 @t75 @t298 @t42 (tptp.samesideline @t297 @t24 @t37 @t39))))) % 34.54/34.73 (assume @p201 (forall (@list @t20 @t22 @t23 @t37 @t39 @t24 @t36 @t299) (or @t53 @t75 @t298 @t42 @t73 (not (tptp.samesideline @t36 @t24 @t37 @t39)) (not (tptp.s_e3 @t20 @t22 @t23 @t37 @t39 @t299)) (not (tptp.samesideline @t299 @t24 @t37 @t39)) (= @t36 @t299)))) % 34.54/34.73 (assume @p202 @t311) % 34.54/34.73 (assume @p203 (forall (@list @t37 @t22 @t20 @t36 @t23 @t66 @t34 @t29 @t312 @t33) (or (not (tptp.sameside @t37 @t22 @t20)) (not (tptp.sameside @t36 @t22 @t23)) (not (tptp.sameside @t66 @t34 @t29)) (not (tptp.sameside @t312 @t34 @t33)) @t313 @t304))) % 34.54/34.73 (assume @p204 (forall @t35 (and (or @t53 @t97 @t277 @t318 (tptp.sameside @t317 @t22 @t20) @t304) (or @t53 @t97 @t277 @t318 (tptp.sameside @t316 @t22 @t23) @t304) (or @t53 @t97 @t277 @t318 (tptp.sameside @t315 @t34 @t29) @t304) (or @t53 @t97 @t277 @t318 (tptp.sameside @t314 @t34 @t33) @t304) (or @t53 @t97 @t277 @t318 (tptp.s_e @t22 @t317 @t34 @t315) @t304) (or @t53 @t97 @t277 @t318 (tptp.s_e @t22 @t316 @t34 @t314) @t304) (or @t53 @t97 @t277 @t318 (not (tptp.s_e @t317 @t316 @t315 @t314)) @t304)))) % 34.54/34.73 (assume @p205 (forall (@list @t20 @t22 @t23 @t29 @t34 @t33 @t181 @t299 @t320 @t319) (or @t305 @t327 @t326 @t325 @t324 @t323 @t322 @t321))) % 34.54/34.73 (assume @p206 @t335) % 34.54/34.73 (assume @p207 (forall @t52 (or @t53 @t97 (tptp.congruent @t20 @t22 @t23 @t20 @t22 @t23)))) % 34.54/34.73 (assume @p208 (forall @t35 (or @t305 (tptp.congruent @t29 @t34 @t33 @t20 @t22 @t23)))) % 34.54/34.73 (assume @p209 (forall (@list @t37 @t39 @t36 @t181 @t185 @t299 @t338 @t337 @t336) (or (not (tptp.congruent @t37 @t39 @t36 @t181 @t185 @t299)) (not (tptp.congruent @t181 @t185 @t299 @t338 @t337 @t336)) (tptp.congruent @t37 @t39 @t36 @t338 @t337 @t336)))) % 34.54/34.73 (assume @p210 (forall @t52 (or @t53 @t97 (tptp.congruent @t20 @t22 @t23 @t23 @t22 @t20)))) % 34.54/34.73 (assume @p211 (forall (@list @t20 @t22 @t23 @t29 @t34 @t24) (and (or @t75 @t340 (tptp.congruent @t20 @t22 @t23 @t29 @t34 @t339)) (or @t75 @t340 (tptp.samesideline @t339 @t24 @t29 @t34))))) % 34.54/34.73 (assume @p212 (forall (@list @t20 @t22 @t23 @t29 @t34 @t24 @t312 @t319) (or @t75 @t340 (not (tptp.congruent @t20 @t22 @t23 @t29 @t34 @t312)) (not (tptp.samesideline @t312 @t24 @t34 @t29)) (not (tptp.congruent @t20 @t22 @t23 @t29 @t34 @t319)) (not (tptp.samesideline @t319 @t24 @t34 @t29)) @t328))) % 34.54/34.73 (assume @p213 @t342) % 34.54/34.73 (assume @p214 (forall (@list @t20 @t22 @t37 @t36) (= @t70 (tptp.ext (tptp.ext @t36 @t37 tptp.alpha tptp.gamma) @t37 @t20 @t22)))) % 34.54/34.73 (assume @p215 (forall @t357 (and (or @t356 @t45) (or @t356 @t354) (or @t356 @t353) (or @t356 @t351) (or @t356 @t349) (or @t356 @t348) (or @t46 @t355 (not @t353) @t352 @t350 (not @t348) @t347)))) % 34.54/34.73 (assume @p216 (forall @t357 (and (or @t361 @t45) (or @t361 @t354) (or @t361 @t360) (or @t361 @t351) (or @t361 @t349) (or @t361 @t359) (or @t46 @t355 (not @t360) @t352 @t350 (not @t359) @t358)))) % 34.54/34.73 (assume @p217 (forall (@list @t37 @t181 @t338 @t39 @t185 @t337) (and (or @t366 @t365) (or @t366 @t364) (or @t366 @t363) (or (not @t365) (not @t364) (not @t363) @t362)))) % 34.54/34.73 (assume @p218 (forall @t52 (and (or @t76 @t45 @t367 @t140) (or @t75 @t46) (or @t75 (not @t367)) (or @t75 @t141)))) % 34.54/34.73 (assume @p219 (forall @t68 (and (or @t80 @t75) (or @t80 @t72) (or @t80 @t368) (or @t80 @t67) (or @t76 @t73 (not @t368) (not @t67) @t79)))) % 34.54/34.73 (assume @p220 (forall (@list @t20 @t22 @t23 @t29 @t2) (and (or @t89 (tptp.s_t @t23 @t86 @t29)) (or @t89 (tptp.s_e @t20 @t22 @t23 @t86)) (or (not (tptp.s_t @t23 @t2 @t29)) (not (tptp.s_e @t20 @t22 @t23 @t2)) @t88)))) % 34.54/34.73 (assume @p221 (forall @t119 (and @t117 @t115 (or @t108 @t131 @t369) (or @t133 @t104 (= tptp.xb @t24) @t99) (or (not @t369) @t104 @t103 @t99)))) % 34.54/34.73 (assume @p222 (forall @t161 (and (or @t160 @t370) (or @t160 @t178) (or (not @t370) @t179 @t159)))) % 34.54/34.73 (assume @p223 (forall @t188 (and (or @t187 @t199) (or @t187 @t197) (or @t187 @t195) (or @t187 @t193) (or @t187 @t191) (or @t187 @t189) (or @t200 @t198 @t196 @t194 @t192 @t190 @t186)))) % 34.54/34.73 (assume @p224 (forall @t52 (and (or @t202 @t371) (or @t201 (not @t371))))) % 34.54/34.73 (assume @p225 (forall (@list @t2 @t7 @t1 @t17 @t16 @t216 @t6) (and (or @t381 @t376) (or @t381 @t374) (or @t381 (not @t379)) (or @t381 (not @t378)) (or @t381 (not (tptp.s_col @t2 @t7 @t216)) (not (tptp.s_col @t17 @t16 @t6)) (tptp.s_r @t216 @t1 @t6)) (or @t380 @t379 @t378 @t377 @t375 (tptp.s_col @t2 @t7 @t373)) (or @t380 @t379 @t378 @t377 @t375 (tptp.s_col @t17 @t16 @t372)) (or @t380 @t379 @t378 @t377 @t375 (not (tptp.s_r @t373 @t1 @t372)))))) % 34.54/34.73 (assume @p226 (forall (@list @t24 @t21 @t283 @t382 @t1) (and (or (not @t383) (tptp.perpAt @t24 @t21 (tptp.il @t24 @t21 @t283 @t382) @t283 @t382)) (or @t383 (not (tptp.perpAt @t24 @t21 @t1 @t283 @t382)))))) % 34.54/34.73 (assume @p227 (forall (@list @t24 @t21 @t20 @t22 @t237) (and (or @t130 @t149 @t147 (not (tptp.s_t @t20 @t237 @t22)) (not (tptp.s_col @t24 @t21 @t237)) @t253) (or @t254 @t150) (or @t254 @t148) (or @t254 (tptp.s_t @t20 @t222 @t22)) (or @t254 (tptp.s_col @t24 @t21 @t222))))) % 34.54/34.73 (assume @p228 (forall (@list @t20 @t22 @t24 @t21 @t385 @t23 @t384) (and (or @t275 (tptp.s_col @t24 @t21 @t388)) (or @t275 (tptp.s_col @t24 @t21 @t386)) (or @t275 (tptp.s_t @t20 @t388 @t387)) (or @t275 (tptp.s_t @t22 @t386 @t387)) (or @t275 (not (= @t20 @t388))) (or @t275 (not (= @t22 @t386))) (or @t275 (not (= @t387 @t388))) (or @t275 (not (= @t387 @t386))) (or @t275 @t214) (or @t275 @t150) (or @t275 @t148) (or (not (tptp.s_t @t20 @t385 @t23)) (not (tptp.s_t @t22 @t384 @t23)) (not (tptp.s_col @t24 @t21 @t385)) (not (tptp.s_col @t24 @t21 @t384)) @t130 (= @t23 @t385) (= @t23 @t384) (= @t20 @t385) (= @t22 @t384) @t149 @t147 @t274)))) % 34.54/34.73 (assume @p229 true) % 34.54/34.73 (step @p230 :rule skolemize :premises (@p213)) % 34.54/34.73 (step @p231 :rule bool-double-not-elim :args (@t393)) % 34.54/34.73 (step @p232 :rule refl :args (@t402)) % 34.54/34.73 (step @p233 :rule nary_cong :premises (@p232 @p231) :args ((or @t402 (not @t399)))) % 34.54/34.73 (step @p234 :rule cnf_or_neg :args (@t402 1)) % 34.54/34.73 (step @p235 :rule eq_resolve :premises (@p234 @p233)) % 34.54/34.73 (step @p236 :rule reordering :premises (@p235) :args ((or @t393 @t402))) % 34.54/34.73 (step @p237 :rule chain_m_resolution :premises (@p236 @p230) :args (@t393 @t403 @t404)) % 34.54/34.73 (step @p238 :rule bool-double-not-elim :args (@t397)) % 34.54/34.73 (step @p239 :rule nary_cong :premises (@p232 @p238) :args ((or @t402 (not @t398)))) % 34.54/34.73 (step @p240 :rule cnf_or_neg :args (@t402 2)) % 34.54/34.73 (step @p241 :rule eq_resolve :premises (@p240 @p239)) % 34.54/34.73 (step @p242 :rule reordering :premises (@p241) :args ((or @t397 @t402))) % 34.54/34.73 (step @p243 :rule chain_m_resolution :premises (@p242 @p230) :args (@t397 @t403 @t404)) % 34.54/34.73 (step @p244 :rule cnf_or_neg :args (@t402 3)) % 34.54/34.73 (step @p245 :rule chain_m_resolution :premises (@p244 @p230) :args ((not @t396) @t403 @t404)) % 34.54/34.73 (step @p246 :rule alpha_equiv :args (@t405 @t406 (@list (@var "BOUND_VARIABLE_10176" $$unsorted) (@var "BOUND_VARIABLE_10178" $$unsorted) (@var "BOUND_VARIABLE_10180" $$unsorted) (@var "BOUND_VARIABLE_10182" $$unsorted) (@var "BOUND_VARIABLE_10184" $$unsorted) (@var "BOUND_VARIABLE_10186" $$unsorted)))) % 34.54/34.73 (step @p247 :rule alpha_equiv :args (@t407 @t406 (@list @t413 @t412 @t411 @t410 @t409 @t408))) % 34.54/34.73 (step @p248 :rule alpha_equiv :args (@t414 @t406 (@list (@var "BOUND_VARIABLE_10138" $$unsorted) (@var "BOUND_VARIABLE_10140" $$unsorted) (@var "BOUND_VARIABLE_10142" $$unsorted) (@var "BOUND_VARIABLE_10144" $$unsorted) (@var "BOUND_VARIABLE_10146" $$unsorted) (@var "BOUND_VARIABLE_10148" $$unsorted)))) % 34.54/34.73 (step @p249 :rule alpha_equiv :args (@t415 @t406 (@list (@var "BOUND_VARIABLE_10119" $$unsorted) (@var "BOUND_VARIABLE_10121" $$unsorted) (@var "BOUND_VARIABLE_10123" $$unsorted) (@var "BOUND_VARIABLE_10125" $$unsorted) (@var "BOUND_VARIABLE_10127" $$unsorted) (@var "BOUND_VARIABLE_10129" $$unsorted)))) % 34.54/34.73 (step @p250 :rule alpha_equiv :args (@t416 @t406 (@list (@var "BOUND_VARIABLE_10100" $$unsorted) (@var "BOUND_VARIABLE_10102" $$unsorted) (@var "BOUND_VARIABLE_10104" $$unsorted) (@var "BOUND_VARIABLE_10106" $$unsorted) (@var "BOUND_VARIABLE_10108" $$unsorted) (@var "BOUND_VARIABLE_10110" $$unsorted)))) % 34.54/34.73 (step @p251 :rule nary_cong :premises (@p250 @p249 @p248 @p247 @p246) :args (@t417)) % 34.54/34.73 (step @p252 :rule quant-miniscope-and :args ((= @t311 @t417))) % 34.54/34.73 (step @p253 :rule trans :premises (@p252 @p251)) % 34.54/34.73 (step @p254 :rule eq_resolve :premises (@p202 @p253)) % 34.54/34.73 (step @p255 :rule and_elim :premises (@p254) :args (0)) % 34.54/34.73 (step @p256 :rule instantiate :premises (@p255) :args (@t418)) % 34.54/34.73 (step @p257 :rule bool-double-not-elim :args (@t400)) % 34.54/34.73 (step @p258 :rule nary_cong :premises (@p232 @p257) :args ((or @t402 (not @t401)))) % 34.54/34.73 (step @p259 :rule cnf_or_neg :args (@t402 0)) % 34.54/34.73 (step @p260 :rule eq_resolve :premises (@p259 @p258)) % 34.54/34.73 (step @p261 :rule reordering :premises (@p260) :args ((or @t400 @t402))) % 34.54/34.73 (step @p262 :rule chain_m_resolution :premises (@p261 @p230) :args (@t400 @t403 @t404)) % 34.54/34.73 (step @p263 :rule cnf_or_pos :args (@t421)) % 34.54/34.73 (step @p264 :rule reordering :premises (@p263) :args ((or @t401 @t420 (not @t421)))) % 34.54/34.73 (step @p265 :rule chain_m_resolution :premises (@p264 @p262 @p256) :args (@t420 @t422 (@list @t400 @t421))) % 34.54/34.73 (step @p266 :rule and_elim :premises (@p254) :args (1)) % 34.54/34.73 (step @p267 :rule instantiate :premises (@p266) :args (@t418)) % 34.54/34.73 (step @p268 :rule cnf_or_pos :args (@t425)) % 34.54/34.73 (step @p269 :rule reordering :premises (@p268) :args ((or @t401 @t424 (not @t425)))) % 34.54/34.73 (step @p270 :rule chain_m_resolution :premises (@p269 @p262 @p267) :args (@t424 @t422 (@list @t400 @t425))) % 34.54/34.73 (step @p271 :rule and_elim :premises (@p254) :args (2)) % 34.54/34.73 (step @p272 :rule instantiate :premises (@p271) :args (@t418)) % 34.54/34.73 (step @p273 :rule cnf_or_pos :args (@t428)) % 34.54/34.73 (step @p274 :rule reordering :premises (@p273) :args ((or @t401 @t427 (not @t428)))) % 34.54/34.73 (step @p275 :rule chain_m_resolution :premises (@p274 @p262 @p272) :args (@t427 @t422 (@list @t400 @t428))) % 34.54/34.73 (step @p276 :rule and_elim :premises (@p254) :args (3)) % 34.54/34.73 (step @p277 :rule instantiate :premises (@p276) :args (@t418)) % 34.54/34.73 (step @p278 :rule cnf_or_pos :args (@t431)) % 34.54/34.73 (step @p279 :rule reordering :premises (@p278) :args ((or @t401 @t430 (not @t431)))) % 34.54/34.73 (step @p280 :rule chain_m_resolution :premises (@p279 @p262 @p277) :args (@t430 @t422 (@list @t400 @t431))) % 34.54/34.73 (step @p281 :rule and_elim :premises (@p254) :args (4)) % 34.54/34.73 (step @p282 :rule instantiate :premises (@p281) :args (@t418)) % 34.54/34.73 (step @p283 :rule cnf_or_pos :args (@t433)) % 34.54/34.73 (step @p284 :rule reordering :premises (@p283) :args ((or @t401 @t432 (not @t433)))) % 34.54/34.73 (step @p285 :rule chain_m_resolution :premises (@p284 @p262 @p282) :args (@t432 @t422 (@list @t400 @t433))) % 34.54/34.73 (step @p286 :rule instantiate :premises (@p75) :args (@t434)) % 34.54/34.73 (step @p287 :rule cnf_or_pos :args (@t437)) % 34.54/34.73 (step @p288 :rule reordering :premises (@p287) :args ((or @t436 @t435 (not @t437)))) % 34.54/34.73 (step @p289 :rule chain_m_resolution :premises (@p288 @p265 @p286) :args (@t435 @t422 (@list @t420 @t437))) % 34.54/34.73 (step @p290 :rule instantiate :premises (@p75) :args (@t438)) % 34.54/34.73 (step @p291 :rule cnf_or_pos :args (@t441)) % 34.54/34.73 (step @p292 :rule reordering :premises (@p291) :args ((or @t440 @t439 (not @t441)))) % 34.54/34.73 (step @p293 :rule chain_m_resolution :premises (@p292 @p270 @p290) :args (@t439 @t422 (@list @t424 @t441))) % 34.54/34.73 (step @p294 :rule instantiate :premises (@p75) :args (@t442)) % 34.54/34.73 (step @p295 :rule cnf_or_pos :args (@t445)) % 34.54/34.73 (step @p296 :rule reordering :premises (@p295) :args ((or @t444 @t443 (not @t445)))) % 34.54/34.73 (step @p297 :rule chain_m_resolution :premises (@p296 @p280 @p294) :args (@t443 @t422 (@list @t430 @t445))) % 34.54/34.73 (step @p298 :rule eq-symm :args (@t446 @t394)) % 34.54/34.73 (step @p299 :rule refl :args (@t448)) % 34.54/34.73 (step @p300 :rule refl :args (@t450)) % 34.54/34.73 (step @p301 :rule nary_cong :premises (@p300 @p299 @p298) :args (@t451)) % 34.54/34.73 (step @p302 :rule refl :args (@t98)) % 34.54/34.73 (step @p303 :rule cong :premises (@p302 @p301) :args ((=> @t98 @t451))) % 34.54/34.73 (assume-push @p874 @t98) % 34.54/34.73 (step @p305 :rule instantiate :premises (@p66) :args ((@list @t390 @t394 @t446))) % 34.54/34.73 (step-pop @p875 :rule scope :premises (@p305)) % 34.54/34.73 (step @p306 :rule process_scope :premises (@p875) :args (@t451)) % 34.54/34.73 (step @p308 :rule eq_resolve :premises (@p306 @p303)) % 34.54/34.73 (step @p309 :rule implies_elim :premises (@p308)) % 34.54/34.73 (step @p310 :rule chain_m_resolution :premises (@p309 @p66) :args (@t453 @t454 @t455)) % 34.54/34.73 (step @p311 :rule alpha_equiv :args (@t456 @t457 (@list (@var "BOUND_VARIABLE_9172" $$unsorted) (@var "BOUND_VARIABLE_9174" $$unsorted) (@var "BOUND_VARIABLE_9176" $$unsorted) (@var "BOUND_VARIABLE_9178" $$unsorted)))) % 34.54/34.73 (step @p312 :rule alpha_equiv :args (@t458 @t457 (@list (@var "BOUND_VARIABLE_9157" $$unsorted) (@var "BOUND_VARIABLE_9159" $$unsorted) (@var "BOUND_VARIABLE_9161" $$unsorted) (@var "BOUND_VARIABLE_9163" $$unsorted)))) % 34.54/34.73 (step @p313 :rule alpha_equiv :args (@t459 @t457 (@list (@var "BOUND_VARIABLE_9142" $$unsorted) (@var "BOUND_VARIABLE_9144" $$unsorted) (@var "BOUND_VARIABLE_9146" $$unsorted) (@var "BOUND_VARIABLE_9148" $$unsorted)))) % 34.54/34.73 (step @p314 :rule nary_cong :premises (@p313 @p312 @p311) :args (@t460)) % 34.54/34.73 (step @p315 :rule quant-miniscope-and :args ((= @t93 @t460))) % 34.54/34.73 (step @p316 :rule trans :premises (@p315 @p314)) % 34.54/34.73 (step @p317 :rule eq_resolve :premises (@p56 @p316)) % 34.54/34.73 (step @p318 :rule and_elim :premises (@p317) :args (1)) % 34.54/34.73 (step @p319 :rule instantiate :premises (@p318) :args (@t461)) % 34.54/34.73 (step @p320 :rule instantiate :premises (@p58) :args ((@list @t392 @t395 @t392 @t395 @t390 @t394 @t390 @t394))) % 34.54/34.73 (step @p321 :rule instantiate :premises (@p59) :args (@t462)) % 34.54/34.73 (step @p322 :rule cnf_or_pos :args (@t466)) % 34.54/34.73 (step @p323 :rule factoring :premises (@p322)) % 34.54/34.73 (step @p324 :rule reordering :premises (@p323) :args ((or @t398 @t465 @t463 (not @t466)))) % 34.54/34.73 (step @p325 :rule chain_m_resolution :premises (@p324 @p243 @p321 @p320) :args (@t463 @t467 (@list @t397 @t464 @t466))) % 34.54/34.73 (step @p326 :rule cnf_or_pos :args (@t469)) % 34.54/34.73 (step @p327 :rule reordering :premises (@p326) :args ((or @t468 @t447 (not @t469)))) % 34.54/34.73 (step @p328 :rule chain_m_resolution :premises (@p327 @p325 @p319) :args (@t447 @t422 (@list @t463 @t469))) % 34.54/34.73 (step @p329 :rule and_elim :premises (@p317) :args (0)) % 34.54/34.73 (step @p330 :rule instantiate :premises (@p329) :args (@t461)) % 34.54/34.73 (step @p331 :rule cnf_or_pos :args (@t470)) % 34.54/34.73 (step @p332 :rule reordering :premises (@p331) :args ((or @t468 @t449 (not @t470)))) % 34.54/34.73 (step @p333 :rule chain_m_resolution :premises (@p332 @p325 @p330) :args (@t449 @t422 (@list @t463 @t470))) % 34.54/34.73 (step @p334 :rule cnf_or_pos :args (@t453)) % 34.54/34.73 (step @p335 :rule reordering :premises (@p334) :args ((or @t450 @t448 @t452 (not @t453)))) % 34.54/34.73 (step @p336 :rule chain_m_resolution :premises (@p335 @p333 @p328 @p310) :args (@t452 @t467 (@list @t449 @t447 @t453))) % 34.54/34.73 (step @p337 :rule refl :args (@t474)) % 34.54/34.73 (step @p338 :rule refl :args (@t478)) % 34.54/34.73 (step @p339 :rule refl :args (@t482)) % 34.54/34.73 (step @p340 :rule aci_norm :args ((= (or @t485 false) @t485))) % 34.54/34.73 (step @p341 :rule evaluate :args ((not true))) % 34.54/34.73 (step @p342 :rule eq-refl :args (@t483)) % 34.54/34.73 (step @p343 :rule cong :premises (@p342) :args (@t486)) % 34.54/34.73 (step @p344 :rule trans :premises (@p343 @p341)) % 34.54/34.73 (step @p345 :rule refl :args (@t485)) % 34.54/34.73 (step @p346 :rule nary_cong :premises (@p345 @p344) :args (@t487)) % 34.54/34.73 (step @p347 :rule trans :premises (@p346 @p340)) % 34.54/34.73 (step @p348 :rule cong :premises (@p347) :args ((forall @t488 @t487))) % 34.54/34.73 (step @p349 :rule quant-var-elim-eq :args ((= (forall @t493 @t492) @t487))) % 34.54/34.73 (step @p350 :rule aci_norm :args ((= @t494 @t492))) % 34.54/34.73 (step @p351 :rule cong :premises (@p350) :args (@t495)) % 34.54/34.73 (step @p352 :rule trans :premises (@p351 @p349)) % 34.54/34.73 (step @p353 :rule cong :premises (@p352) :args (@t496)) % 34.54/34.73 (step @p354 :rule quant-merge-prenex :args ((= @t496 @t497))) % 34.54/34.73 (step @p355 :rule symm :premises (@p354)) % 34.54/34.73 (step @p356 :rule quant_var_reordering :args ((= @t498 @t497))) % 34.54/34.73 (step @p357 :rule trans :premises (@p356 @p355 @p353)) % 34.54/34.73 (step @p358 :rule trans :premises (@p357 @p348)) % 34.54/34.73 (step @p359 :rule aci_norm :args ((= (or @t501 false) @t501))) % 34.54/34.73 (step @p360 :rule eq-refl :args (@t500)) % 34.54/34.73 (step @p361 :rule cong :premises (@p360) :args (@t502)) % 34.54/34.73 (step @p362 :rule trans :premises (@p361 @p341)) % 34.54/34.73 (step @p363 :rule refl :args (@t501)) % 34.54/34.73 (step @p364 :rule nary_cong :premises (@p363 @p362) :args (@t503)) % 34.54/34.73 (step @p365 :rule trans :premises (@p364 @p359)) % 34.54/34.73 (step @p366 :rule cong :premises (@p365) :args ((forall @t504 @t503))) % 34.54/34.73 (step @p367 :rule quant-var-elim-eq :args ((= (forall @t509 @t508) @t503))) % 34.54/34.73 (step @p368 :rule aci_norm :args ((= @t510 @t508))) % 34.54/34.73 (step @p369 :rule cong :premises (@p368) :args (@t511)) % 34.54/34.73 (step @p370 :rule trans :premises (@p369 @p367)) % 34.54/34.73 (step @p371 :rule cong :premises (@p370) :args (@t512)) % 34.54/34.73 (step @p372 :rule quant-merge-prenex :args ((= @t512 @t513))) % 34.54/34.73 (step @p373 :rule symm :premises (@p372)) % 34.54/34.73 (step @p374 :rule quant_var_reordering :args ((= @t514 @t513))) % 34.54/34.73 (step @p375 :rule trans :premises (@p374 @p373 @p371)) % 34.54/34.73 (step @p376 :rule trans :premises (@p375 @p366)) % 34.54/34.73 (step @p377 :rule nary_cong :premises (@p376 @p358 @p339 @p338 @p337) :args ((and @t514 @t498 @t482 @t478 @t474))) % 34.54/34.73 (step @p378 :rule alpha_equiv :args (@t515 @t516 (@list @t473 @t472 @t471))) % 34.54/34.73 (step @p379 :rule alpha_equiv :args (@t517 @t516 (@list @t477 @t476 @t475))) % 34.54/34.73 (step @p380 :rule alpha_equiv :args (@t519 @t516 (@list @t481 @t480 @t479))) % 34.54/34.73 (step @p381 :rule alpha_equiv :args (@t522 @t516 (@list @t484 @t489 @t483))) % 34.54/34.73 (step @p382 :rule alpha_equiv :args (@t523 @t516 (@list @t505 @t500 @t499))) % 34.54/34.73 (step @p383 :rule nary_cong :premises (@p382 @p381 @p380 @p379 @p378) :args (@t524)) % 34.54/34.73 (step @p384 :rule quant-miniscope-and :args ((= (forall @t119 (and @t117 @t521 @t518 @t111 @t110)) @t524))) % 34.54/34.73 (step @p385 :rule trans :premises (@p384 @p383)) % 34.54/34.73 (step @p386 :rule trans :premises (@p385 @p377)) % 34.54/34.73 (step @p387 :rule refl :args (@t110)) % 34.54/34.73 (step @p388 :rule refl :args (@t111)) % 34.54/34.73 (step @p389 :rule eq-symm :args (@t109 @t24)) % 34.54/34.73 (step @p390 :rule cong :premises (@p389) :args (@t112)) % 34.54/34.73 (step @p391 :rule refl :args (@t108)) % 34.54/34.73 (step @p392 :rule nary_cong :premises (@p391 @p390) :args (@t113)) % 34.54/34.73 (step @p393 :rule eq-symm :args (@t22 @t24)) % 34.54/34.73 (step @p394 :rule cong :premises (@p393) :args (@t114)) % 34.54/34.73 (step @p395 :rule nary_cong :premises (@p391 @p394) :args (@t115)) % 34.54/34.73 (step @p396 :rule refl :args (@t117)) % 34.54/34.73 (step @p397 :rule nary_cong :premises (@p396 @p395 @p392 @p388 @p387) :args (@t118)) % 34.54/34.73 (step @p398 :rule cong :premises (@p397) :args (@t120)) % 34.54/34.73 (step @p399 :rule trans :premises (@p398 @p386)) % 34.54/34.73 (step @p400 :rule eq_resolve :premises (@p70 @p399)) % 34.54/34.73 (step @p401 :rule and_elim :premises (@p400) :args (2)) % 34.54/34.73 (step @p402 :rule instantiate :premises (@p401) :args (@t442)) % 34.54/34.73 (step @p403 :rule cnf_or_pos :args (@t528)) % 34.54/34.73 (step @p404 :rule reordering :premises (@p403) :args ((or @t444 @t527 (not @t528)))) % 34.54/34.73 (step @p405 :rule chain_m_resolution :premises (@p404 @p280 @p402) :args (@t527 @t422 (@list @t430 @t528))) % 34.54/34.73 (step @p406 :rule and_elim :premises (@p400) :args (4)) % 34.54/34.73 (step @p407 :rule instantiate :premises (@p406) :args (@t442)) % 34.54/34.73 (step @p408 :rule cnf_or_pos :args (@t530)) % 34.54/34.73 (step @p409 :rule reordering :premises (@p408) :args ((or @t444 @t529 (not @t530)))) % 34.54/34.73 (step @p410 :rule chain_m_resolution :premises (@p409 @p280 @p407) :args (@t529 @t422 (@list @t430 @t530))) % 34.54/34.73 (step @p411 :rule refl :args (@t99)) % 34.54/34.73 (step @p412 :rule refl :args (@t101)) % 34.54/34.73 (step @p413 :rule refl :args (@t27)) % 34.54/34.73 (step @p414 :rule eq-symm :args (@t23 @t24)) % 34.54/34.73 (step @p415 :rule refl :args (@t104)) % 34.54/34.73 (step @p416 :rule nary_cong :premises (@p415 @p393 @p414 @p413 @p412 @p411) :args (@t105)) % 34.54/34.73 (step @p417 :rule cong :premises (@p416) :args (@t107)) % 34.54/34.73 (step @p418 :rule eq_resolve :premises (@p68 @p417)) % 34.54/34.73 (step @p419 :rule refl :args (@t531)) % 34.54/34.73 (step @p420 :rule refl :args (@t532)) % 34.54/34.73 (step @p421 :rule refl :args (@t526)) % 34.54/34.73 (step @p422 :rule refl :args (@t533)) % 34.54/34.73 (step @p423 :rule eq-symm :args (@t394 @t390)) % 34.54/34.73 (step @p424 :rule nary_cong :premises (@p423 @p422 @p421 @p420 @p420 @p419) :args (@t534)) % 34.54/34.73 (step @p425 :rule refl :args (@t535)) % 34.54/34.73 (step @p426 :rule cong :premises (@p425 @p424) :args ((=> @t535 @t534))) % 34.54/34.73 (assume-push @p876 @t535) % 34.54/34.73 (step @p428 :rule instantiate :premises (@p418) :args ((@list @t394 @t390 @t394 @t525))) % 34.54/34.73 (step-pop @p877 :rule scope :premises (@p428)) % 34.54/34.73 (step @p429 :rule process_scope :premises (@p877) :args (@t534)) % 34.54/34.73 (step @p431 :rule eq_resolve :premises (@p429 @p426)) % 34.54/34.73 (step @p432 :rule implies_elim :premises (@p431)) % 34.54/34.73 (step @p433 :rule chain_m_resolution :premises (@p432 @p418) :args (@t536 @t454 @t537)) % 34.54/34.73 (step @p434 :rule cnf_or_pos :args (@t536)) % 34.54/34.73 (step @p435 :rule factoring :premises (@p434)) % 34.54/34.73 (step @p436 :rule reordering :premises (@p435) :args ((or @t526 @t533 @t531 @t532 (not @t536)))) % 34.54/34.73 (step @p437 :rule alpha_equiv :args (@t538 @t539 (@list (@var "BOUND_VARIABLE_8987" $$unsorted) (@var "BOUND_VARIABLE_8989" $$unsorted) (@var "BOUND_VARIABLE_8991" $$unsorted) (@var "BOUND_VARIABLE_8993" $$unsorted)))) % 34.54/34.73 (step @p438 :rule alpha_equiv :args (@t540 @t539 (@list (@var "BOUND_VARIABLE_8975" $$unsorted) (@var "BOUND_VARIABLE_8977" $$unsorted) (@var "BOUND_VARIABLE_8979" $$unsorted) (@var "BOUND_VARIABLE_8981" $$unsorted)))) % 34.54/34.73 (step @p439 :rule nary_cong :premises (@p438 @p437) :args (@t541)) % 34.54/34.73 (step @p440 :rule quant-miniscope-and :args ((= @t14 @t541))) % 34.54/34.73 (step @p441 :rule trans :premises (@p440 @p439)) % 34.54/34.73 (step @p442 :rule eq_resolve :premises (@p4 @p441)) % 34.54/34.73 (step @p443 :rule and_elim :premises (@p442) :args (0)) % 34.54/34.73 (step @p444 :rule instantiate :premises (@p443) :args ((@list @t392 @t395 @t390 @t394))) % 34.54/34.73 (step @p445 :rule refl :args (@t543)) % 34.54/34.73 (step @p446 :rule bool-double-not-elim :args (@t544)) % 34.54/34.73 (step @p447 :rule refl :args (@t546)) % 34.54/34.73 (step @p448 :rule nary_cong :premises (@p447 @p446 @p445) :args ((or @t546 (not @t547) @t543))) % 34.54/34.73 (assume-push @p878 @t547) % 34.54/34.73 (assume-push @p879 @t542) % 34.54/34.73 (assume-push @p880 @t545) % 34.54/34.73 (step @p452 :rule evaluate :args (@t548)) % 34.54/34.73 (step @p453 :rule false_intro :premises (@p878)) % 34.54/34.73 (step @p454 :rule symm :premises (@p879)) % 34.54/34.73 (step @p455 :rule refl :args (@t395)) % 34.54/34.73 (step @p456 :rule refl :args (@t392)) % 34.54/34.73 (step @p457 :rule cong :premises (@p456 @p455 @p454) :args (@t545)) % 34.54/34.73 (step @p458 :rule true_intro :premises (@p444)) % 34.54/34.73 (step @p459 :rule symm :premises (@p458)) % 34.54/34.73 (step @p460 :rule trans :premises (@p459 @p457 @p453)) % 34.54/34.73 (step @p461 false :rule eq_resolve :premises (@p460 @p452)) % 34.54/34.73 (step-pop @p881 :rule scope :premises (@p461)) % 34.54/34.73 (step-pop @p882 :rule scope :premises (@p881)) % 34.54/34.73 (step-pop @p883 :rule scope :premises (@p882)) % 34.54/34.73 (step @p462 :rule process_scope :premises (@p883) :args (false)) % 34.54/34.73 (assume-push @p884 @t545) % 34.54/34.73 (assume-push @p885 @t547) % 34.54/34.73 (assume-push @p886 @t542) % 34.54/34.73 (step @p469 :rule and_intro :premises (@p885 @p886 @p444)) % 34.54/34.73 (step-pop @p887 :rule scope :premises (@p469)) % 34.54/34.73 (step-pop @p888 :rule scope :premises (@p887)) % 34.54/34.73 (step-pop @p889 :rule scope :premises (@p888)) % 34.54/34.73 (step @p470 :rule process_scope :premises (@p889) :args (@t549)) % 34.54/34.73 (step @p474 :rule implies_elim :premises (@p470)) % 34.54/34.73 (step @p475 :rule resolution :premises (@p474 @p462) :args (true @t549)) % 34.54/34.73 (step @p476 :rule not_and :premises (@p475)) % 34.54/34.73 (step @p477 :rule eq_resolve :premises (@p476 @p448)) % 34.54/34.73 (step @p478 :rule reordering :premises (@p477) :args ((or @t544 @t546 @t543))) % 34.54/34.73 (step @p479 :rule instantiate :premises (@p6) :args (@t462)) % 34.54/34.73 (step @p480 :rule cnf_or_pos :args (@t551)) % 34.54/34.73 (step @p481 :rule reordering :premises (@p480) :args ((or @t550 @t547 (not @t551)))) % 34.54/34.73 (step @p482 :rule alpha_equiv :args (@t552 @t516 (@list (@var "BOUND_VARIABLE_9310" $$unsorted) (@var "BOUND_VARIABLE_9312" $$unsorted) (@var "BOUND_VARIABLE_9314" $$unsorted)))) % 34.54/34.73 (step @p483 :rule alpha_equiv :args (@t553 @t516 (@list (@var "BOUND_VARIABLE_9298" $$unsorted) (@var "BOUND_VARIABLE_9300" $$unsorted) (@var "BOUND_VARIABLE_9302" $$unsorted)))) % 34.54/34.73 (step @p484 :rule nary_cong :premises (@p483 @p482) :args (@t554)) % 34.54/34.73 (step @p485 :rule quant-miniscope-and :args ((= @t125 @t554))) % 34.54/34.73 (step @p486 :rule trans :premises (@p485 @p484)) % 34.54/34.73 (step @p487 :rule eq_resolve :premises (@p72 @p486)) % 34.54/34.73 (step @p488 :rule and_elim :premises (@p487) :args (1)) % 34.54/34.73 (step @p489 :rule instantiate :premises (@p488) :args (@t438)) % 34.54/34.73 (step @p490 :rule cnf_or_pos :args (@t557)) % 34.54/34.73 (step @p491 :rule reordering :premises (@p490) :args ((or @t440 @t556 (not @t557)))) % 34.54/34.73 (step @p492 :rule chain_m_resolution :premises (@p491 @p270 @p489) :args (@t556 @t422 (@list @t424 @t557))) % 34.54/34.73 (step @p493 :rule instantiate :premises (@p20) :args (@t462)) % 34.54/34.73 (step @p494 :rule bool-double-not-elim :args (@t555)) % 34.54/34.73 (step @p495 :rule refl :args (@t559)) % 34.54/34.73 (step @p496 :rule refl :args (@t560)) % 34.54/34.73 (step @p497 :rule nary_cong :premises (@p496 @p495 @p494 @p445) :args ((or @t560 @t559 (not @t556) @t543))) % 34.54/34.73 (assume-push @p890 @t556) % 34.54/34.73 (assume-push @p891 @t542) % 34.54/34.73 (assume-push @p892 @t550) % 34.54/34.73 (assume-push @p893 @t558) % 34.54/34.73 (step @p452 :rule evaluate :args (@t548)) % 34.54/34.73 (step @p502 :rule false_intro :premises (@p492)) % 34.54/34.73 (step @p455 :rule refl :args (@t395)) % 34.54/34.73 (step @p456 :rule refl :args (@t392)) % 34.54/34.73 (step @p503 :rule cong :premises (@p891 @p456 @p455) :args ((tptp.s_t @t392 @t392 @t395))) % 34.54/34.73 (step @p504 :rule symm :premises (@p892)) % 34.54/34.73 (step @p505 :rule cong :premises (@p456 @p504 @p455) :args (@t558)) % 34.54/34.73 (step @p506 :rule true_intro :premises (@p493)) % 34.54/34.73 (step @p507 :rule symm :premises (@p506)) % 34.54/34.73 (step @p508 :rule trans :premises (@p507 @p505 @p503 @p502)) % 34.54/34.73 (step @p509 false :rule eq_resolve :premises (@p508 @p452)) % 34.54/34.73 (step-pop @p894 :rule scope :premises (@p509)) % 34.54/34.73 (step-pop @p895 :rule scope :premises (@p894)) % 34.54/34.73 (step-pop @p896 :rule scope :premises (@p895)) % 34.54/34.73 (step-pop @p897 :rule scope :premises (@p896)) % 34.54/34.73 (step @p510 :rule process_scope :premises (@p897) :args (false)) % 34.54/34.73 (assume-push @p898 @t550) % 34.54/34.73 (assume-push @p899 @t558) % 34.54/34.73 (assume-push @p900 @t556) % 34.54/34.73 (assume-push @p901 @t542) % 34.54/34.73 (step @p519 :rule and_intro :premises (@p492 @p901 @p898 @p493)) % 34.54/34.73 (step-pop @p902 :rule scope :premises (@p519)) % 34.54/34.73 (step-pop @p903 :rule scope :premises (@p902)) % 34.54/34.73 (step-pop @p904 :rule scope :premises (@p903)) % 34.54/34.73 (step-pop @p905 :rule scope :premises (@p904)) % 34.54/34.73 (step @p520 :rule process_scope :premises (@p905) :args (@t561)) % 34.54/34.73 (step @p525 :rule implies_elim :premises (@p520)) % 34.54/34.73 (step @p526 :rule resolution :premises (@p525 @p510) :args (true @t561)) % 34.54/34.73 (step @p527 :rule not_and :premises (@p526)) % 34.54/34.73 (step @p528 :rule eq_resolve :premises (@p527 @p497)) % 34.54/34.73 (step @p529 :rule reordering :premises (@p528) :args ((or @t559 @t555 @t560 @t543))) % 34.54/34.73 (step @p530 :rule chain_m_resolution :premises (@p529 @p493 @p492 @p481 @p479 @p478 @p444) :args (@t543 @t562 (@list @t558 @t555 @t550 @t551 @t544 @t545))) % 34.54/34.73 (assume-push @p906 @t474) % 34.54/34.73 (step-pop @p907 :rule scope :premises (@p407)) % 34.54/34.73 (step @p532 :rule process_scope :premises (@p907) :args (@t530)) % 34.54/34.73 (step @p534 :rule implies_elim :premises (@p532)) % 34.54/34.73 (assume-push @p908 @t563) % 34.54/34.73 (step-pop @p909 :rule scope :premises (@p277)) % 34.54/34.73 (step @p536 :rule process_scope :premises (@p909) :args (@t431)) % 34.54/34.73 (step @p538 :rule implies_elim :premises (@p536)) % 34.54/34.73 (step @p539 :rule refl :args (@t564)) % 34.54/34.73 (step @p540 :rule bool-double-not-elim :args (@t341)) % 34.54/34.73 (step @p541 :rule nary_cong :premises (@p540 @p539) :args ((or (not @t342) @t564))) % 34.54/34.73 (assume-push @p910 @t342) % 34.54/34.73 (step-pop @p911 :rule scope :premises (@p230)) % 34.54/34.73 (step @p543 :rule process_scope :premises (@p911) :args (@t564)) % 34.54/34.73 (step @p545 :rule implies_elim :premises (@p543)) % 34.54/34.73 (step @p546 :rule eq_resolve :premises (@p545 @p541)) % 34.54/34.73 (assume-push @p912 @t482) % 34.54/34.73 (step-pop @p913 :rule scope :premises (@p402)) % 34.54/34.73 (step @p548 :rule process_scope :premises (@p913) :args (@t528)) % 34.54/34.73 (step @p550 :rule implies_elim :premises (@p548)) % 34.54/34.73 (step @p551 :rule instantiate :premises (@p401) :args (@t565)) % 34.54/34.73 (step @p552 :rule cnf_or_pos :args (@t570)) % 34.54/34.73 (step @p553 :rule reordering :premises (@p552) :args ((or @t569 @t568 (not @t570)))) % 34.54/34.73 (step @p554 :rule chain_m_resolution :premises (@p553 @p275 @p551) :args (@t568 @t422 (@list @t427 @t570))) % 34.54/34.73 (step @p555 :rule instantiate :premises (@p406) :args (@t565)) % 34.54/34.73 (step @p556 :rule cnf_or_pos :args (@t572)) % 34.54/34.73 (step @p557 :rule reordering :premises (@p556) :args ((or @t569 @t571 (not @t572)))) % 34.54/34.73 (step @p558 :rule chain_m_resolution :premises (@p557 @p275 @p555) :args (@t571 @t422 (@list @t427 @t572))) % 34.54/34.73 (step @p559 :rule refl :args (@t573)) % 34.54/34.73 (step @p560 :rule refl :args (@t574)) % 34.54/34.73 (step @p561 :rule refl :args (@t567)) % 34.54/34.73 (step @p562 :rule eq-symm :args (@t390 @t389)) % 34.54/34.73 (step @p563 :rule refl :args (@t575)) % 34.54/34.73 (step @p564 :rule nary_cong :premises (@p563 @p562 @p561 @p560 @p560 @p559) :args (@t576)) % 34.54/34.73 (step @p565 :rule cong :premises (@p425 @p564) :args ((=> @t535 @t576))) % 34.54/34.73 (assume-push @p914 @t535) % 34.54/34.73 (step @p567 :rule instantiate :premises (@p418) :args ((@list @t389 @t390 @t389 @t566))) % 34.54/34.73 (step-pop @p915 :rule scope :premises (@p567)) % 34.54/34.73 (step @p568 :rule process_scope :premises (@p915) :args (@t576)) % 34.54/34.73 (step @p570 :rule eq_resolve :premises (@p568 @p565)) % 34.54/34.73 (step @p571 :rule implies_elim :premises (@p570)) % 34.54/34.73 (step @p572 :rule chain_m_resolution :premises (@p571 @p418) :args (@t577 @t454 @t537)) % 34.54/34.73 (step @p573 :rule cnf_or_pos :args (@t577)) % 34.54/34.73 (step @p574 :rule factoring :premises (@p573)) % 34.54/34.73 (step @p575 :rule reordering :premises (@p574) :args ((or @t567 @t575 @t573 @t574 (not @t577)))) % 34.54/34.73 (step @p576 :rule instantiate :premises (@p443) :args ((@list @t392 @t391 @t390 @t389))) % 34.54/34.73 (step @p577 :rule bool-double-not-elim :args (@t578)) % 34.54/34.73 (step @p578 :rule refl :args (@t580)) % 34.54/34.73 (step @p579 :rule refl :args (@t582)) % 34.54/34.73 (step @p580 :rule nary_cong :premises (@p579 @p578 @p577) :args ((or @t582 @t580 (not @t583)))) % 34.54/34.73 (assume-push @p916 @t583) % 34.54/34.73 (assume-push @p917 @t579) % 34.54/34.73 (assume-push @p918 @t581) % 34.54/34.73 (step @p452 :rule evaluate :args (@t548)) % 34.54/34.73 (step @p584 :rule false_intro :premises (@p916)) % 34.54/34.73 (step @p585 :rule symm :premises (@p917)) % 34.54/34.73 (step @p586 :rule refl :args (@t391)) % 34.54/34.73 (step @p456 :rule refl :args (@t392)) % 34.54/34.73 (step @p587 :rule cong :premises (@p456 @p586 @p585) :args (@t581)) % 34.54/34.73 (step @p588 :rule true_intro :premises (@p576)) % 34.54/34.73 (step @p589 :rule symm :premises (@p588)) % 34.54/34.73 (step @p590 :rule trans :premises (@p589 @p587 @p584)) % 34.54/34.73 (step @p591 false :rule eq_resolve :premises (@p590 @p452)) % 34.54/34.73 (step-pop @p919 :rule scope :premises (@p591)) % 34.54/34.73 (step-pop @p920 :rule scope :premises (@p919)) % 34.54/34.73 (step-pop @p921 :rule scope :premises (@p920)) % 34.54/34.73 (step @p592 :rule process_scope :premises (@p921) :args (false)) % 34.54/34.73 (assume-push @p922 @t581) % 34.54/34.73 (assume-push @p923 @t579) % 34.54/34.73 (assume-push @p924 @t583) % 34.54/34.73 (step @p599 :rule and_intro :premises (@p924 @p923 @p576)) % 34.54/34.73 (step-pop @p925 :rule scope :premises (@p599)) % 34.54/34.73 (step-pop @p926 :rule scope :premises (@p925)) % 34.54/34.73 (step-pop @p927 :rule scope :premises (@p926)) % 34.54/34.73 (step @p600 :rule process_scope :premises (@p927) :args (@t584)) % 34.54/34.73 (step @p604 :rule implies_elim :premises (@p600)) % 34.54/34.73 (step @p605 :rule resolution :premises (@p604 @p592) :args (true @t584)) % 34.54/34.73 (step @p606 :rule not_and :premises (@p605)) % 34.54/34.73 (step @p607 :rule eq_resolve :premises (@p606 @p580)) % 34.54/34.73 (step @p608 :rule eq-symm :args (@t392 @t391)) % 34.54/34.73 (step @p609 :rule refl :args (@t583)) % 34.54/34.73 (step @p610 :rule nary_cong :premises (@p609 @p608) :args (@t585)) % 34.54/34.73 (step @p611 :rule refl :args (@t19)) % 34.54/34.73 (step @p612 :rule cong :premises (@p611 @p610) :args ((=> @t19 @t585))) % 34.54/34.73 (assume-push @p928 @t19) % 34.54/34.73 (step @p614 :rule instantiate :premises (@p6) :args (@t586)) % 34.54/34.73 (step-pop @p929 :rule scope :premises (@p614)) % 34.54/34.73 (step @p615 :rule process_scope :premises (@p929) :args (@t585)) % 34.54/34.73 (step @p617 :rule eq_resolve :premises (@p615 @p612)) % 34.54/34.73 (step @p618 :rule implies_elim :premises (@p617)) % 34.54/34.73 (step @p619 :rule chain_m_resolution :premises (@p618 @p6) :args (@t588 @t454 (@list @t19))) % 34.54/34.73 (step @p620 :rule cnf_or_pos :args (@t588)) % 34.54/34.73 (step @p621 :rule reordering :premises (@p620) :args ((or @t587 @t583 (not @t588)))) % 34.54/34.73 (step @p622 :rule instantiate :premises (@p488) :args (@t434)) % 34.54/34.73 (step @p623 :rule cnf_or_pos :args (@t591)) % 34.54/34.73 (step @p624 :rule reordering :premises (@p623) :args ((or @t436 @t590 (not @t591)))) % 34.54/34.73 (step @p625 :rule chain_m_resolution :premises (@p624 @p265 @p622) :args (@t590 @t422 (@list @t420 @t591))) % 34.54/34.73 (step @p626 :rule instantiate :premises (@p20) :args (@t586)) % 34.54/34.73 (step @p627 :rule bool-double-not-elim :args (@t589)) % 34.54/34.73 (step @p628 :rule refl :args (@t593)) % 34.54/34.73 (step @p629 :rule refl :args (@t594)) % 34.54/34.73 (step @p630 :rule nary_cong :premises (@p629 @p628 @p627 @p578) :args ((or @t594 @t593 (not @t590) @t580))) % 34.54/34.73 (assume-push @p930 @t590) % 34.54/34.73 (assume-push @p931 @t579) % 34.54/34.73 (assume-push @p932 @t587) % 34.54/34.73 (assume-push @p933 @t592) % 34.54/34.73 (step @p452 :rule evaluate :args (@t548)) % 34.54/34.73 (step @p635 :rule false_intro :premises (@p625)) % 34.54/34.73 (step @p586 :rule refl :args (@t391)) % 34.54/34.73 (step @p636 :rule cong :premises (@p931 @p932 @p586) :args (@t592)) % 34.54/34.73 (step @p637 :rule true_intro :premises (@p626)) % 34.54/34.73 (step @p638 :rule symm :premises (@p637)) % 34.54/34.73 (step @p639 :rule trans :premises (@p638 @p636 @p635)) % 34.54/34.73 (step @p640 false :rule eq_resolve :premises (@p639 @p452)) % 34.54/34.73 (step-pop @p934 :rule scope :premises (@p640)) % 34.54/34.73 (step-pop @p935 :rule scope :premises (@p934)) % 34.54/34.73 (step-pop @p936 :rule scope :premises (@p935)) % 34.54/34.73 (step-pop @p937 :rule scope :premises (@p936)) % 34.54/34.73 (step @p641 :rule process_scope :premises (@p937) :args (false)) % 34.54/34.73 (assume-push @p938 @t587) % 34.54/34.73 (assume-push @p939 @t592) % 34.54/34.73 (assume-push @p940 @t590) % 34.54/34.73 (assume-push @p941 @t579) % 34.54/34.73 (step @p650 :rule and_intro :premises (@p625 @p941 @p938 @p626)) % 34.54/34.73 (step-pop @p942 :rule scope :premises (@p650)) % 34.54/34.73 (step-pop @p943 :rule scope :premises (@p942)) % 34.54/34.73 (step-pop @p944 :rule scope :premises (@p943)) % 34.54/34.73 (step-pop @p945 :rule scope :premises (@p944)) % 34.54/34.73 (step @p651 :rule process_scope :premises (@p945) :args (@t595)) % 34.54/34.73 (step @p656 :rule implies_elim :premises (@p651)) % 34.54/34.73 (step @p657 :rule resolution :premises (@p656 @p641) :args (true @t595)) % 34.54/34.73 (step @p658 :rule not_and :premises (@p657)) % 34.54/34.73 (step @p659 :rule eq_resolve :premises (@p658 @p630)) % 34.54/34.73 (step @p660 :rule reordering :premises (@p659) :args ((or @t593 @t589 @t594 @t580))) % 34.54/34.73 (step @p661 :rule chain_m_resolution :premises (@p660 @p626 @p625 @p621 @p619 @p607 @p576) :args (@t580 @t562 (@list @t592 @t589 @t587 @t588 @t578 @t581))) % 34.54/34.73 (step @p662 :rule refl :args (@t321)) % 34.54/34.73 (step @p663 :rule refl :args (@t322)) % 34.54/34.73 (step @p664 :rule refl :args (@t323)) % 34.54/34.73 (step @p665 :rule refl :args (@t324)) % 34.54/34.73 (step @p666 :rule refl :args (@t325)) % 34.54/34.73 (step @p667 :rule refl :args (@t326)) % 34.54/34.73 (step @p668 :rule refl :args (@t327)) % 34.54/34.73 (step @p669 :rule eq-symm :args (@t33 @t34)) % 34.54/34.73 (step @p670 :rule refl :args (@t277)) % 34.54/34.73 (step @p671 :rule refl :args (@t97)) % 34.54/34.73 (step @p672 :rule refl :args (@t53)) % 34.54/34.73 (step @p673 :rule refl :args (@t313)) % 34.54/34.73 (step @p674 :rule refl :args (@t329)) % 34.54/34.73 (step @p675 :rule refl :args (@t330)) % 34.54/34.73 (step @p676 :rule refl :args (@t331)) % 34.54/34.73 (step @p677 :rule refl :args (@t332)) % 34.54/34.73 (step @p678 :rule nary_cong :premises (@p677 @p676 @p675 @p674 @p673 @p672 @p671 @p670 @p669 @p668 @p667 @p666 @p665 @p664 @p663 @p662) :args (@t333)) % 34.54/34.73 (step @p679 :rule cong :premises (@p678) :args (@t335)) % 34.54/34.73 (step @p680 :rule eq_resolve :premises (@p206 @p679)) % 34.54/34.73 (step @p681 :rule refl :args (@t396)) % 34.54/34.73 (step @p682 :rule refl :args (@t398)) % 34.54/34.73 (step @p683 :rule refl :args (@t399)) % 34.54/34.73 (step @p684 :rule refl :args (@t596)) % 34.54/34.73 (step @p685 :rule refl :args (@t597)) % 34.54/34.73 (step @p686 :rule refl :args (@t598)) % 34.54/34.73 (step @p687 :rule refl :args (@t599)) % 34.54/34.73 (step @p688 :rule eq-symm :args (@t423 @t392)) % 34.54/34.73 (step @p689 :rule eq-symm :args (@t419 @t392)) % 34.54/34.73 (step @p690 :rule refl :args (@t600)) % 34.54/34.73 (step @p691 :rule refl :args (@t444)) % 34.54/34.73 (step @p692 :rule refl :args (@t569)) % 34.54/34.73 (step @p693 :rule refl :args (@t440)) % 34.54/34.73 (step @p694 :rule refl :args (@t436)) % 34.54/34.73 (step @p695 :rule nary_cong :premises (@p694 @p693 @p692 @p691 @p690 @p689 @p688 @p563 @p422 @p687 @p686 @p685 @p684 @p683 @p682 @p681) :args (@t603)) % 34.54/34.73 (step @p696 :rule refl :args (@t604)) % 34.54/34.73 (step @p697 :rule cong :premises (@p696 @p695) :args ((=> @t604 @t603))) % 34.54/34.73 (assume-push @p946 @t604) % 34.54/34.73 (step @p699 :rule instantiate :premises (@p680) :args ((@list @t419 @t392 @t391 @t423 @t395 @t426 @t390 @t389 @t429 @t394 @t419 @t423 @t389 @t394))) % 34.54/34.73 (step-pop @p947 :rule scope :premises (@p699)) % 34.54/34.73 (step @p700 :rule process_scope :premises (@p947) :args (@t603)) % 34.54/34.73 (step @p702 :rule eq_resolve :premises (@p700 @p697)) % 34.54/34.73 (step @p703 :rule implies_elim :premises (@p702)) % 34.54/34.73 (step @p704 :rule chain_m_resolution :premises (@p703 @p680) :args (@t605 @t454 @t606)) % 34.54/34.73 (step @p705 :rule cnf_or_pos :args (@t605)) % 34.54/34.73 (step @p706 :rule reordering :premises (@p705) :args ((or @t399 @t398 @t396 @t436 @t440 @t569 @t444 @t600 @t575 @t533 @t596 @t597 @t599 @t598 @t579 @t542 (not @t605)))) % 34.54/34.73 (step @p707 :rule chain_m_resolution :premises (@p706 @p704 @p661 @p293 @p289 @p285 @p280 @p275 @p270 @p265 @p245 @p243 @p237 @p575 @p572 @p558 @p554 @p436 @p404 @p550 @p401 @p409 @p279 @p261 @p546 @p213 @p538 @p276 @p534 @p406 @p432 @p418) :args ((or @t575 @t533 @t542) (@list false true false false false false false false false true false false false false false true false true false false false false false true true false false false false false false) (@list @t605 @t579 @t439 @t435 @t432 @t430 @t427 @t424 @t420 @t396 @t397 @t393 @t573 @t577 @t571 @t567 @t531 @t526 @t528 @t482 @t529 @t430 @t400 @t402 @t341 @t431 @t563 @t530 @t474 @t536 @t535))) % 34.54/34.73 (step @p708 :rule instantiate :premises (@p75) :args (@t565)) % 34.54/34.73 (step @p709 :rule cnf_or_pos :args (@t608)) % 34.54/34.73 (step @p710 :rule reordering :premises (@p709) :args ((or @t569 @t607 (not @t608)))) % 34.54/34.73 (step @p711 :rule chain_m_resolution :premises (@p710 @p275 @p708) :args (@t607 @t422 (@list @t427 @t608))) % 34.54/34.73 (step @p712 :rule refl :args (@t609)) % 34.54/34.73 (step @p713 :rule eq-symm :args (@t426 @t390)) % 34.54/34.73 (step @p714 :rule nary_cong :premises (@p694 @p693 @p692 @p691 @p690 @p689 @p688 @p713 @p422 @p687 @p686 @p712 @p684 @p683 @p682 @p681) :args (@t611)) % 34.54/34.73 (step @p715 :rule cong :premises (@p696 @p714) :args ((=> @t604 @t611))) % 34.54/34.73 (assume-push @p948 @t604) % 34.54/34.73 (step @p717 :rule instantiate :premises (@p680) :args ((@list @t419 @t392 @t391 @t423 @t395 @t426 @t390 @t389 @t429 @t394 @t419 @t423 @t426 @t394))) % 34.54/34.73 (step-pop @p949 :rule scope :premises (@p717)) % 34.54/34.73 (step @p718 :rule process_scope :premises (@p949) :args (@t611)) % 34.54/34.73 (step @p720 :rule eq_resolve :premises (@p718 @p715)) % 34.54/34.73 (step @p721 :rule implies_elim :premises (@p720)) % 34.54/34.73 (step @p722 :rule chain_m_resolution :premises (@p721 @p680) :args (@t613 @t454 @t606)) % 34.54/34.73 (step @p723 :rule cnf_or_pos :args (@t613)) % 34.54/34.73 (step @p724 :rule reordering :premises (@p723) :args ((or @t399 @t398 @t396 @t436 @t440 @t569 @t444 @t600 @t533 @t596 @t599 @t598 @t609 @t579 @t542 @t612 (not @t613)))) % 34.54/34.73 (step @p725 :rule instantiate :premises (@p329) :args (@t614)) % 34.54/34.73 (step @p726 :rule instantiate :premises (@p58) :args ((@list @t392 @t391 @t392 @t391 @t390 @t389 @t390 @t389))) % 34.54/34.73 (step @p727 :rule instantiate :premises (@p59) :args (@t586)) % 34.54/34.73 (step @p728 :rule cnf_or_pos :args (@t618)) % 34.54/34.73 (step @p729 :rule factoring :premises (@p728)) % 34.54/34.73 (step @p730 :rule reordering :premises (@p729) :args ((or @t399 @t617 @t615 (not @t618)))) % 34.54/34.73 (step @p731 :rule chain_m_resolution :premises (@p730 @p237 @p727 @p726) :args (@t615 @t467 (@list @t393 @t616 @t618))) % 34.54/34.73 (step @p732 :rule cnf_or_pos :args (@t622)) % 34.54/34.73 (step @p733 :rule reordering :premises (@p732) :args ((or @t621 @t620 (not @t622)))) % 34.54/34.73 (step @p734 :rule chain_m_resolution :premises (@p733 @p731 @p725) :args (@t620 @t422 (@list @t615 @t622))) % 34.54/34.73 (step @p735 :rule instantiate :premises (@p488) :args (@t565)) % 34.54/34.73 (step @p736 :rule cnf_or_pos :args (@t625)) % 34.54/34.73 (step @p737 :rule reordering :premises (@p736) :args ((or @t569 @t624 (not @t625)))) % 34.54/34.73 (step @p738 :rule chain_m_resolution :premises (@p737 @p275 @p735) :args (@t624 @t422 (@list @t427 @t625))) % 34.54/34.73 (step @p739 :rule eq-symm :args (@t619 @t389)) % 34.54/34.73 (step @p740 :rule refl :args (@t627)) % 34.54/34.73 (step @p741 :rule refl :args (@t628)) % 34.54/34.73 (step @p742 :rule nary_cong :premises (@p741 @p740 @p739) :args (@t629)) % 34.54/34.73 (step @p743 :rule cong :premises (@p302 @p742) :args ((=> @t98 @t629))) % 34.54/34.73 (assume-push @p950 @t98) % 34.54/34.73 (step @p745 :rule instantiate :premises (@p66) :args ((@list @t390 @t389 @t619))) % 34.54/34.73 (step-pop @p951 :rule scope :premises (@p745)) % 34.54/34.73 (step @p746 :rule process_scope :premises (@p951) :args (@t629)) % 34.54/34.73 (step @p748 :rule eq_resolve :premises (@p746 @p743)) % 34.54/34.73 (step @p749 :rule implies_elim :premises (@p748)) % 34.54/34.73 (step @p750 :rule chain_m_resolution :premises (@p749 @p66) :args (@t631 @t454 @t455)) % 34.54/34.73 (step @p751 :rule instantiate :premises (@p318) :args (@t614)) % 34.54/34.73 (step @p752 :rule cnf_or_pos :args (@t632)) % 34.54/34.73 (step @p753 :rule reordering :premises (@p752) :args ((or @t621 @t626 (not @t632)))) % 34.54/34.73 (step @p754 :rule chain_m_resolution :premises (@p753 @p731 @p751) :args (@t626 @t422 (@list @t615 @t632))) % 34.54/34.73 (step @p755 :rule cnf_or_pos :args (@t631)) % 34.54/34.73 (step @p756 :rule reordering :premises (@p755) :args ((or @t628 @t627 @t630 (not @t631)))) % 34.54/34.73 (step @p757 :rule chain_m_resolution :premises (@p756 @p734 @p754 @p750) :args (@t630 @t467 (@list @t620 @t626 @t631))) % 34.54/34.73 (step @p758 :rule refl :args (@t633)) % 34.54/34.73 (step @p759 :rule refl :args (@t634)) % 34.54/34.73 (step @p760 :rule refl :args (@t635)) % 34.54/34.73 (step @p761 :rule bool-double-not-elim :args (@t623)) % 34.54/34.73 (step @p762 :rule nary_cong :premises (@p741 @p761 @p760 @p759 @p758) :args ((or @t628 (not @t624) @t635 @t634 @t633))) % 34.54/34.73 (assume-push @p952 @t620) % 34.54/34.73 (assume-push @p953 @t575) % 34.54/34.73 (assume-push @p954 @t612) % 34.54/34.73 (assume-push @p955 @t630) % 34.54/34.73 (assume-push @p956 @t624) % 34.54/34.73 (step @p768 :rule evaluate :args (@t636)) % 34.54/34.73 (step @p769 :rule true_intro :premises (@p734)) % 34.54/34.73 (step @p770 :rule symm :premises (@p953)) % 34.54/34.73 (step @p771 :rule symm :premises (@p954)) % 34.54/34.73 (step @p772 :rule cong :premises (@p771 @p770 @p757) :args (@t623)) % 34.54/34.73 (step @p773 :rule false_intro :premises (@p738)) % 34.54/34.73 (step @p774 :rule symm :premises (@p773)) % 34.54/34.73 (step @p775 :rule trans :premises (@p774 @p772 @p769)) % 34.54/34.73 (step @p776 false :rule eq_resolve :premises (@p775 @p768)) % 34.54/34.73 (step-pop @p957 :rule scope :premises (@p776)) % 34.54/34.73 (step-pop @p958 :rule scope :premises (@p957)) % 34.54/34.73 (step-pop @p959 :rule scope :premises (@p958)) % 34.54/34.73 (step-pop @p960 :rule scope :premises (@p959)) % 34.54/34.73 (step-pop @p961 :rule scope :premises (@p960)) % 34.54/34.73 (step @p777 :rule process_scope :premises (@p961) :args (false)) % 34.54/34.73 (assume-push @p962 @t620) % 34.54/34.73 (assume-push @p963 @t624) % 34.54/34.73 (assume-push @p964 @t575) % 34.54/34.73 (assume-push @p965 @t630) % 34.54/34.73 (assume-push @p966 @t612) % 34.54/34.73 (step @p788 :rule and_intro :premises (@p734 @p964 @p966 @p757 @p738)) % 34.54/34.73 (step-pop @p967 :rule scope :premises (@p788)) % 34.54/34.73 (step-pop @p968 :rule scope :premises (@p967)) % 34.54/34.73 (step-pop @p969 :rule scope :premises (@p968)) % 34.54/34.73 (step-pop @p970 :rule scope :premises (@p969)) % 34.54/34.73 (step-pop @p971 :rule scope :premises (@p970)) % 34.54/34.73 (step @p789 :rule process_scope :premises (@p971) :args (@t637)) % 34.54/34.73 (step @p795 :rule implies_elim :premises (@p789)) % 34.54/34.73 (step @p796 :rule resolution :premises (@p795 @p777) :args (true @t637)) % 34.54/34.73 (step @p797 :rule not_and :premises (@p796)) % 34.54/34.73 (step @p798 :rule eq_resolve :premises (@p797 @p762)) % 34.54/34.73 (step @p799 :rule reordering :premises (@p798) :args ((or @t623 @t628 @t635 @t634 @t633))) % 34.54/34.73 (step @p800 :rule chain_m_resolution :premises (@p799 @p757 @p738 @p734 @p724 @p661 @p722 @p530 @p711 @p293 @p289 @p285 @p280 @p275 @p270 @p265 @p245 @p243 @p237 @p707 @p530 @p436 @p433 @p410 @p405) :args (@t533 (@list false true false false true false true false false false false false false false false true false false false true false false false true) (@list @t630 @t623 @t620 @t612 @t579 @t613 @t542 @t607 @t439 @t435 @t432 @t430 @t427 @t424 @t420 @t396 @t397 @t393 @t575 @t542 @t531 @t536 @t529 @t526))) % 34.54/34.73 (step @p801 :rule instantiate :premises (@p488) :args (@t442)) % 34.54/34.73 (step @p802 :rule cnf_or_pos :args (@t640)) % 34.54/34.73 (step @p803 :rule reordering :premises (@p802) :args ((or @t444 @t639 (not @t640)))) % 34.54/34.73 (step @p804 :rule chain_m_resolution :premises (@p803 @p280 @p801) :args (@t639 @t422 (@list @t430 @t640))) % 34.54/34.73 (step @p805 :rule refl :args (@t642)) % 34.54/34.73 (step @p806 :rule refl :args (@t643)) % 34.54/34.73 (step @p807 :rule refl :args (@t644)) % 34.54/34.73 (step @p808 :rule bool-double-not-elim :args (@t638)) % 34.54/34.73 (step @p809 :rule nary_cong :premises (@p300 @p808 @p807 @p806 @p805) :args ((or @t450 (not @t639) @t644 @t643 @t642))) % 34.54/34.73 (assume-push @p972 @t449) % 34.54/34.73 (assume-push @p973 @t533) % 34.54/34.73 (assume-push @p974 @t641) % 34.54/34.73 (assume-push @p975 @t452) % 34.54/34.73 (assume-push @p976 @t639) % 34.54/34.73 (step @p768 :rule evaluate :args (@t636)) % 34.54/34.73 (step @p815 :rule true_intro :premises (@p333)) % 34.54/34.73 (step @p816 :rule symm :premises (@p974)) % 34.54/34.73 (step @p817 :rule cong :premises (@p816 @p973 @p336) :args (@t638)) % 34.54/34.73 (step @p818 :rule false_intro :premises (@p804)) % 34.54/34.73 (step @p819 :rule symm :premises (@p818)) % 34.54/34.73 (step @p820 :rule trans :premises (@p819 @p817 @p815)) % 34.54/34.73 (step @p821 false :rule eq_resolve :premises (@p820 @p768)) % 34.54/34.73 (step-pop @p977 :rule scope :premises (@p821)) % 34.54/34.73 (step-pop @p978 :rule scope :premises (@p977)) % 34.54/34.73 (step-pop @p979 :rule scope :premises (@p978)) % 34.54/34.73 (step-pop @p980 :rule scope :premises (@p979)) % 34.54/34.73 (step-pop @p981 :rule scope :premises (@p980)) % 34.54/34.73 (step @p822 :rule process_scope :premises (@p981) :args (false)) % 34.54/34.73 (assume-push @p982 @t449) % 34.54/34.73 (assume-push @p983 @t639) % 34.54/34.73 (assume-push @p984 @t533) % 34.54/34.73 (assume-push @p985 @t452) % 34.54/34.73 (assume-push @p986 @t641) % 34.54/34.73 (step @p833 :rule and_intro :premises (@p333 @p984 @p986 @p336 @p804)) % 34.54/34.73 (step-pop @p987 :rule scope :premises (@p833)) % 34.54/34.73 (step-pop @p988 :rule scope :premises (@p987)) % 34.54/34.73 (step-pop @p989 :rule scope :premises (@p988)) % 34.54/34.73 (step-pop @p990 :rule scope :premises (@p989)) % 34.54/34.73 (step-pop @p991 :rule scope :premises (@p990)) % 34.54/34.73 (step @p834 :rule process_scope :premises (@p991) :args (@t645)) % 34.54/34.73 (step @p840 :rule implies_elim :premises (@p834)) % 34.54/34.73 (step @p841 :rule resolution :premises (@p840 @p822) :args (true @t645)) % 34.54/34.73 (step @p842 :rule not_and :premises (@p841)) % 34.54/34.73 (step @p843 :rule eq_resolve :premises (@p842 @p809)) % 34.54/34.73 (step @p844 :rule reordering :premises (@p843) :args ((or @t638 @t450 @t644 @t643 @t642))) % 34.54/34.73 (step @p845 :rule chain_m_resolution :premises (@p844 @p804 @p333 @p800 @p336) :args (@t642 @t646 (@list @t638 @t449 @t533 @t452))) % 34.54/34.73 (step @p846 :rule refl :args (@t647)) % 34.54/34.73 (step @p847 :rule refl :args (@t641)) % 34.54/34.73 (step @p848 :rule nary_cong :premises (@p694 @p693 @p692 @p691 @p690 @p689 @p688 @p563 @p847 @p687 @p686 @p685 @p846 @p683 @p682 @p681) :args (@t648)) % 34.54/34.73 (step @p849 :rule cong :premises (@p696 @p848) :args ((=> @t604 @t648))) % 34.54/34.73 (assume-push @p992 @t604) % 34.54/34.73 (step @p851 :rule instantiate :premises (@p680) :args ((@list @t419 @t392 @t391 @t423 @t395 @t426 @t390 @t389 @t429 @t394 @t419 @t423 @t389 @t429))) % 34.54/34.73 (step-pop @p993 :rule scope :premises (@p851)) % 34.54/34.73 (step @p852 :rule process_scope :premises (@p993) :args (@t648)) % 34.54/34.73 (step @p854 :rule eq_resolve :premises (@p852 @p849)) % 34.54/34.73 (step @p855 :rule implies_elim :premises (@p854)) % 34.54/34.73 (step @p856 :rule chain_m_resolution :premises (@p855 @p680) :args (@t649 @t454 @t606)) % 34.54/34.73 (step @p857 :rule nary_cong :premises (@p694 @p693 @p692 @p691 @p690 @p689 @p688 @p713 @p847 @p687 @p686 @p712 @p846 @p683 @p682 @p681) :args (@t650)) % 34.54/34.73 (step @p858 :rule cong :premises (@p696 @p857) :args ((=> @t604 @t650))) % 34.54/34.73 (assume-push @p994 @t604) % 34.54/34.73 (step @p860 :rule instantiate :premises (@p680) :args ((@list @t419 @t392 @t391 @t423 @t395 @t426 @t390 @t389 @t429 @t394 @t419 @t423 @t426 @t429))) % 34.54/34.73 (step-pop @p995 :rule scope :premises (@p860)) % 34.54/34.73 (step @p861 :rule process_scope :premises (@p995) :args (@t650)) % 34.54/34.73 (step @p863 :rule eq_resolve :premises (@p861 @p858)) % 34.54/34.73 (step @p864 :rule implies_elim :premises (@p863)) % 34.54/34.73 (step @p865 :rule chain_m_resolution :premises (@p864 @p680) :args (@t651 @t454 @t606)) % 34.54/34.73 (step @p866 :rule cnf_or_pos :args (@t651)) % 34.54/34.73 (step @p867 :rule reordering :premises (@p866) :args ((or @t399 @t398 @t396 @t436 @t440 @t569 @t444 @t600 @t599 @t598 @t609 @t647 @t579 @t542 @t641 @t612 (not @t651)))) % 34.54/34.73 (step @p868 :rule chain_m_resolution :premises (@p867 @p237 @p243 @p245 @p265 @p270 @p275 @p280 @p285 @p289 @p293 @p711 @p297 @p661 @p530 @p845 @p865) :args (@t612 (@list false false true false false false false false false false false false true true true false) (@list @t393 @t397 @t396 @t420 @t424 @t427 @t430 @t432 @t435 @t439 @t607 @t443 @t579 @t542 @t641 @t651))) % 34.54/34.73 (step @p869 :rule chain_m_resolution :premises (@p799 @p738 @p734 @p757 @p868) :args (@t635 @t646 (@list @t623 @t620 @t630 @t612))) % 34.54/34.73 (step @p870 :rule chain_m_resolution :premises (@p575 @p554 @p869 @p558 @p572) :args (@t573 (@list true true false false) (@list @t567 @t575 @t571 @t577))) % 34.54/34.73 (step @p871 :rule cnf_or_pos :args (@t649)) % 34.54/34.73 (step @p872 :rule reordering :premises (@p871) :args ((or @t399 @t398 @t396 @t436 @t440 @t569 @t444 @t600 @t575 @t597 @t599 @t598 @t647 @t579 @t542 @t641 (not @t649)))) % 34.54/34.73 (step @p873 false :rule chain_m_resolution :premises (@p872 @p870 @p869 @p661 @p856 @p530 @p845 @p297 @p293 @p289 @p285 @p280 @p275 @p270 @p265 @p245 @p243 @p237) :args (false (@list false true true false true true false false false false false false false false true false false) (@list @t573 @t575 @t579 @t649 @t542 @t641 @t443 @t439 @t435 @t432 @t430 @t427 @t424 @t420 @t396 @t397 @t393))) % 34.54/34.73 ) % 34.54/34.73 % SZS output end Proof % 34.54/34.73 % cvc5 exiting %------------------------------------------------------------------------------