%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : LCL954^19 : TPTP v9.3.1. Released v8.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % Computer : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:24:15 AM UTC 2026 % Result : Theorem 2.21s 2.57s % Output : Proof 2.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL954^19 : TPTP v9.3.1. Released v8.1.0. % 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM % 0.09/0.37 % Computer : n027.cluster.edu % 0.09/0.37 % Model : x86_64 x86_64 % 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.37 % Memory : 8046.5625MB % 0.09/0.37 % OS : Linux 6.8.0-71-generic % 0.09/0.37 % CPULimit : 300 % 0.09/0.37 % WCLimit : 300 % 0.09/0.37 % DateTime : Fri Sep 4 14:30:42 UTC 2026 % 0.09/0.37 % CPUTime : % 0.20/0.53 %----Proving TH0 % 2.21/2.57 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s... % 2.21/2.57 % SZS status Theorem % 2.21/2.57 % SZS output start Proof % 2.21/2.57 ( % 2.21/2.57 (declare-sort $$unsorted 0) % 2.21/2.57 (declare-sort tptp.mworld 0) % 2.21/2.57 (declare-const tptp.mactual tptp.mworld) % 2.21/2.57 (declare-const tptp.mrel (-> tptp.mworld tptp.mworld Bool)) % 2.21/2.57 (declare-const tptp.eiw_di (-> $$unsorted tptp.mworld Bool)) % 2.21/2.57 (declare-const tptp.def $$unsorted) % 2.21/2.57 (declare-const tptp.true (-> tptp.mworld Bool)) % 2.21/2.57 (declare-const tptp.n5 $$unsorted) % 2.21/2.57 (declare-const tptp.n4 $$unsorted) % 2.21/2.57 (declare-const tptp.n3 $$unsorted) % 2.21/2.57 (declare-const tptp.n2 $$unsorted) % 2.21/2.57 (declare-const tptp.n1 $$unsorted) % 2.21/2.57 (declare-const tptp.tptp_float_0_0 $$unsorted) % 2.21/2.57 (declare-const tptp.tptp_minus_1 $$unsorted) % 2.21/2.57 (declare-const tptp.n0 $$unsorted) % 2.21/2.57 (declare-const tptp.minus (-> $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.inv (-> $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.dim (-> $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.a_select3 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.uniform_int_rnd (-> $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.plus (-> $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.a_select2 (-> $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.pred (-> $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.use $$unsorted) % 2.21/2.57 (declare-const tptp.customqmltpeq (-> $$unsorted $$unsorted tptp.mworld Bool)) % 2.21/2.57 (declare-const tptp.tptp_update2 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.succ (-> $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.sum (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.tptp_const_array1 (-> $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.tptp_const_array2 (-> $$unsorted $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.tptp_madd (-> $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.tptp_mmul (-> $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.tptp_msub (-> $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.tptp_update3 (-> $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.trans (-> $$unsorted $$unsorted)) % 2.21/2.57 (declare-const tptp.geq (-> $$unsorted $$unsorted tptp.mworld Bool)) % 2.21/2.57 (declare-const tptp.gt (-> $$unsorted $$unsorted tptp.mworld Bool)) % 2.21/2.57 (declare-const tptp.leq (-> $$unsorted $$unsorted tptp.mworld Bool)) % 2.21/2.57 (declare-const tptp.lt (-> $$unsorted $$unsorted tptp.mworld Bool)) % 2.21/2.57 (define tptp.mlocal () (let ((_let_1 (@var "Phi" (-> tptp.mworld Bool)))) (lambda (@list _let_1) (_ _let_1 tptp.mactual)))) % 2.21/2.57 (define tptp.mnot () (let ((_let_1 (@var "W" tptp.mworld))) (let ((_let_2 (@var "A" (-> tptp.mworld Bool)))) (lambda (@list _let_2 _let_1) (not (_ _let_2 _let_1)))))) % 2.21/2.57 (define tptp.mand () (let ((_let_1 (@var "W" tptp.mworld))) (let ((_let_2 (@var "B" (-> tptp.mworld Bool)))) (let ((_let_3 (@var "A" (-> tptp.mworld Bool)))) (lambda (@list _let_3 _let_2 _let_1) (and (_ _let_3 _let_1) (_ _let_2 _let_1))))))) % 2.21/2.57 (define tptp.mor () (let ((_let_1 (@var "W" tptp.mworld))) (let ((_let_2 (@var "B" (-> tptp.mworld Bool)))) (let ((_let_3 (@var "A" (-> tptp.mworld Bool)))) (lambda (@list _let_3 _let_2 _let_1) (or (_ _let_3 _let_1) (_ _let_2 _let_1))))))) % 2.21/2.57 (define tptp.mimplies () (let ((_let_1 (@var "W" tptp.mworld))) (let ((_let_2 (@var "B" (-> tptp.mworld Bool)))) (let ((_let_3 (@var "A" (-> tptp.mworld Bool)))) (lambda (@list _let_3 _let_2 _let_1) (=> (_ _let_3 _let_1) (_ _let_2 _let_1))))))) % 2.21/2.57 (define tptp.mequiv () (let ((_let_1 (@var "W" tptp.mworld))) (let ((_let_2 (@var "B" (-> tptp.mworld Bool)))) (let ((_let_3 (@var "A" (-> tptp.mworld Bool)))) (lambda (@list _let_3 _let_2 _let_1) (= (_ _let_3 _let_1) (_ _let_2 _let_1))))))) % 2.21/2.57 (define tptp.mbox () (let ((_let_1 (@var "V" tptp.mworld))) (let ((_let_2 (@var "Phi" (-> tptp.mworld Bool)))) (let ((_let_3 (@var "W" tptp.mworld))) (lambda (@list _let_2 _let_3) (forall (@list _let_1) (=> (_ (_ tptp.mrel _let_3) _let_1) (_ _let_2 _let_1)))))))) % 2.21/2.57 (define tptp.mdia () (let ((_let_1 (@var "V" tptp.mworld))) (let ((_let_2 (@var "Phi" (-> tptp.mworld Bool)))) (let ((_let_3 (@var "W" tptp.mworld))) (lambda (@list _let_2 _let_3) (exists (@list _let_1) (and (_ (_ tptp.mrel _let_3) _let_1) (_ _let_2 _let_1)))))))) % 2.21/2.57 (define tptp.mforall_di () (let ((_let_1 (@var "W" tptp.mworld))) (let ((_let_2 (@var "X" $$unsorted))) (let ((_let_3 (@var "A" (-> $$unsorted tptp.mworld Bool)))) (lambda (@list _let_3 _let_1) (forall (@list _let_2) (=> (_ (_ tptp.eiw_di _let_2) _let_1) (_ (_ _let_3 _let_2) _let_1)))))))) % 2.21/2.57 (define tptp.mexists_di () (let ((_let_1 (@var "W" tptp.mworld))) (let ((_let_2 (@var "X" $$unsorted))) (let ((_let_3 (@var "A" (-> $$unsorted tptp.mworld Bool)))) (lambda (@list _let_3 _let_1) (exists (@list _let_2) (and (_ (_ tptp.eiw_di _let_2) _let_1) (_ (_ _let_3 _let_2) _let_1)))))))) % 2.21/2.57 (define @t1 () (@var "W" tptp.mworld)) % 2.21/2.57 (define @t2 () (_ tptp.mrel @t1)) % 2.21/2.57 (define @t3 () (@list @t1)) % 2.21/2.57 (define @t4 () (@var "U" tptp.mworld)) % 2.21/2.57 (define @t5 () (@var "V" tptp.mworld)) % 2.21/2.57 (define @t6 () (_ @t2 @t5)) % 2.21/2.57 (define @t7 () (@var "X" $$unsorted)) % 2.21/2.57 (define @t8 () (_ (_ tptp.eiw_di @t7) @t1)) % 2.21/2.57 (define @t9 () (@list @t7)) % 2.21/2.57 (define @t10 () (@var "__flatten_var_0" tptp.mworld)) % 2.21/2.57 (define @t11 () (_ tptp.customqmltpeq @t7)) % 2.21/2.57 (define @t12 () (@list @t7 @t10)) % 2.21/2.57 (define @t13 () (@var "Y" $$unsorted)) % 2.21/2.57 (define @t14 () (_ tptp.customqmltpeq @t13)) % 2.21/2.57 (define @t15 () (_ tptp.mbox (_ @t11 @t13))) % 2.21/2.57 (define @t16 () (@list @t13 @t10)) % 2.21/2.57 (define @t17 () (@var "Z" $$unsorted)) % 2.21/2.57 (define @t18 () (@list @t17 @t10)) % 2.21/2.57 (define @t19 () (@var "C" $$unsorted)) % 2.21/2.57 (define @t20 () (@var "B" $$unsorted)) % 2.21/2.57 (define @t21 () (@var "A" $$unsorted)) % 2.21/2.57 (define @t22 () (_ tptp.mbox (_ (_ tptp.customqmltpeq @t21) @t20))) % 2.21/2.57 (define @t23 () (_ tptp.mimplies @t22)) % 2.21/2.57 (define @t24 () (@list @t19 @t10)) % 2.21/2.57 (define @t25 () (@list @t20 @t10)) % 2.21/2.57 (define @t26 () (@list @t21 @t10)) % 2.21/2.57 (define @t27 () (_ tptp.a_select2 @t19)) % 2.21/2.57 (define @t28 () (@var "D" $$unsorted)) % 2.21/2.57 (define @t29 () (_ tptp.a_select3 @t20)) % 2.21/2.57 (define @t30 () (_ tptp.a_select3 @t21)) % 2.21/2.57 (define @t31 () (@list @t28 @t10)) % 2.21/2.57 (define @t32 () (_ tptp.a_select3 @t19)) % 2.21/2.57 (define @t33 () (_ @t32 @t28)) % 2.21/2.57 (define @t34 () (_ tptp.dim @t19)) % 2.21/2.57 (define @t35 () (_ tptp.inv @t21)) % 2.21/2.58 (define @t36 () (_ tptp.minus @t19)) % 2.21/2.58 (define @t37 () (_ tptp.plus @t19)) % 2.21/2.58 (define @t38 () (_ tptp.sum @t19)) % 2.21/2.58 (define @t39 () (_ @t38 @t28)) % 2.21/2.58 (define @t40 () (_ tptp.tptp_const_array1 @t19)) % 2.21/2.58 (define @t41 () (_ tptp.tptp_const_array2 @t19)) % 2.21/2.58 (define @t42 () (_ @t41 @t28)) % 2.21/2.58 (define @t43 () (_ tptp.tptp_madd @t21)) % 2.21/2.58 (define @t44 () (_ tptp.tptp_madd @t19)) % 2.21/2.58 (define @t45 () (_ tptp.tptp_mmul @t20)) % 2.21/2.58 (define @t46 () (_ tptp.tptp_mmul @t21)) % 2.21/2.58 (define @t47 () (_ tptp.tptp_mmul @t19)) % 2.21/2.58 (define @t48 () (_ tptp.tptp_msub @t21)) % 2.21/2.58 (define @t49 () (_ tptp.tptp_msub @t19)) % 2.21/2.58 (define @t50 () (_ tptp.tptp_update2 @t19)) % 2.21/2.58 (define @t51 () (_ @t50 @t28)) % 2.21/2.58 (define @t52 () (@var "E" $$unsorted)) % 2.21/2.58 (define @t53 () (_ tptp.tptp_update3 @t21)) % 2.21/2.58 (define @t54 () (@list @t52 @t10)) % 2.21/2.58 (define @t55 () (_ tptp.tptp_update3 @t19)) % 2.21/2.58 (define @t56 () (_ @t55 @t28)) % 2.21/2.58 (define @t57 () (_ @t56 @t52)) % 2.21/2.58 (define @t58 () (_ tptp.trans @t20)) % 2.21/2.58 (define @t59 () (_ tptp.trans @t21)) % 2.21/2.58 (define @t60 () (_ tptp.uniform_int_rnd @t19)) % 2.21/2.58 (define @t61 () (_ tptp.mand @t22)) % 2.21/2.58 (define @t62 () (_ tptp.geq @t19)) % 2.21/2.58 (define @t63 () (_ tptp.gt @t19)) % 2.21/2.58 (define @t64 () (_ tptp.leq @t19)) % 2.21/2.58 (define @t65 () (_ tptp.lt @t19)) % 2.21/2.58 (define @t66 () (_ tptp.gt @t13)) % 2.21/2.58 (define @t67 () (_ tptp.mbox (_ @t66 @t7))) % 2.21/2.58 (define @t68 () (_ tptp.gt @t7)) % 2.21/2.58 (define @t69 () (_ tptp.mbox (_ @t68 @t13))) % 2.21/2.58 (define @t70 () (_ tptp.leq @t7)) % 2.21/2.58 (define @t71 () (_ tptp.leq @t13)) % 2.21/2.58 (define @t72 () (_ tptp.mbox (_ @t70 @t13))) % 2.21/2.58 (define @t73 () (_ tptp.mand @t72)) % 2.21/2.58 (define @t74 () (_ tptp.mbox (_ (_ tptp.lt @t7) @t13))) % 2.21/2.58 (define @t75 () (_ tptp.mimplies @t67)) % 2.21/2.58 (define @t76 () (_ tptp.mbox (_ (_ tptp.geq @t7) @t13))) % 2.21/2.58 (define @t77 () (_ tptp.mbox (_ @t71 @t7))) % 2.21/2.58 (define @t78 () (_ tptp.mbox (_ @t70 (_ tptp.pred @t13)))) % 2.21/2.58 (define @t79 () (_ tptp.succ @t7)) % 2.21/2.58 (define @t80 () (_ tptp.succ @t13)) % 2.21/2.58 (define @t81 () (_ tptp.mimplies @t72)) % 2.21/2.58 (define @t82 () (_ tptp.mbox (_ (_ tptp.gt @t80) @t7))) % 2.21/2.58 (define @t83 () (_ @t60 @t7)) % 2.21/2.58 (define @t84 () (_ tptp.leq tptp.n0)) % 2.21/2.58 (define @t85 () (_ tptp.mbox (_ @t84 @t7))) % 2.21/2.58 (define @t86 () (_ tptp.mimplies @t85)) % 2.21/2.58 (define @t87 () (@var "Val" $$unsorted)) % 2.21/2.58 (define @t88 () (@var "I" $$unsorted)) % 2.21/2.58 (define @t89 () (@var "U" $$unsorted)) % 2.21/2.58 (define @t90 () (@var "L" $$unsorted)) % 2.21/2.58 (define @t91 () (_ tptp.leq @t88)) % 2.21/2.58 (define @t92 () (_ tptp.mbox (_ @t91 @t89))) % 2.21/2.58 (define @t93 () (@list @t87 @t10)) % 2.21/2.58 (define @t94 () (@list @t89 @t10)) % 2.21/2.58 (define @t95 () (@list @t88 @t10)) % 2.21/2.58 (define @t96 () (@var "J" $$unsorted)) % 2.21/2.58 (define @t97 () (@var "U2" $$unsorted)) % 2.21/2.58 (define @t98 () (@var "L2" $$unsorted)) % 2.21/2.58 (define @t99 () (@var "U1" $$unsorted)) % 2.21/2.58 (define @t100 () (@var "L1" $$unsorted)) % 2.21/2.58 (define @t101 () (_ tptp.leq @t96)) % 2.21/2.58 (define @t102 () (@list @t96 @t10)) % 2.21/2.58 (define @t103 () (_ tptp.a_select3 @t59)) % 2.21/2.58 (define @t104 () (@var "N" $$unsorted)) % 2.21/2.58 (define @t105 () (_ tptp.mbox (_ @t101 @t104))) % 2.21/2.58 (define @t106 () (_ tptp.mand (_ tptp.mbox (_ @t84 @t96)))) % 2.21/2.58 (define @t107 () (_ tptp.mand (_ tptp.mbox (_ @t91 @t104)))) % 2.21/2.58 (define @t108 () (_ tptp.mand (_ tptp.mbox (_ @t84 @t88)))) % 2.21/2.58 (define @t109 () (_ tptp.mimplies (_ @t108 (_ @t107 (_ @t106 @t105))))) % 2.21/2.58 (define @t110 () (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ @t109 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t30 @t88) @t96)) (_ (_ @t30 @t96) @t88))))) @t10)))) @t10))))) % 2.21/2.58 (define @t111 () (_ tptp.mimplies @t110)) % 2.21/2.58 (define @t112 () (@list @t104 @t10)) % 2.21/2.58 (define @t113 () (_ tptp.a_select3 @t35)) % 2.21/2.58 (define @t114 () (@var "VAL" $$unsorted)) % 2.21/2.58 (define @t115 () (@var "K" $$unsorted)) % 2.21/2.58 (define @t116 () (_ tptp.a_select3 (_ (_ (_ @t53 @t115) @t115) @t114))) % 2.21/2.58 (define @t117 () (@list @t114 @t10)) % 2.21/2.58 (define @t118 () (_ tptp.a_select3 (_ @t43 @t20))) % 2.21/2.58 (define @t119 () (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t29 @t88) @t96)) (_ (_ @t29 @t96) @t88)))) % 2.21/2.58 (define @t120 () (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ @t109 @t119)) @t10)))) @t10))))) % 2.21/2.58 (define @t121 () (_ tptp.mand @t110)) % 2.21/2.58 (define @t122 () (_ tptp.mimplies (_ @t121 @t120))) % 2.21/2.58 (define @t123 () (_ tptp.a_select3 (_ @t48 @t20))) % 2.21/2.58 (define @t124 () (_ tptp.a_select3 (_ @t46 (_ @t45 @t59)))) % 2.21/2.58 (define @t125 () (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ @t109 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t124 @t88) @t96)) (_ (_ @t124 @t96) @t88))))) @t10)))) @t10))))) % 2.21/2.58 (define @t126 () (@var "M" $$unsorted)) % 2.21/2.58 (define @t127 () (_ tptp.mimplies (_ @t108 (_ (_ tptp.mand (_ tptp.mbox (_ @t91 @t126))) (_ @t106 (_ tptp.mbox (_ @t101 @t126))))))) % 2.21/2.58 (define @t128 () (@list @t126 @t10)) % 2.21/2.58 (define @t129 () (@var "F" $$unsorted)) % 2.21/2.58 (define @t130 () (_ tptp.a_select3 (_ @t43 (_ @t45 (_ (_ tptp.tptp_mmul (_ (_ tptp.tptp_madd (_ @t47 (_ (_ tptp.tptp_mmul @t28) (_ tptp.trans @t19)))) (_ (_ tptp.tptp_mmul @t52) (_ (_ tptp.tptp_mmul @t129) (_ tptp.trans @t52))))) @t58))))) % 2.21/2.58 (define @t131 () (_ tptp.a_select3 @t129)) % 2.21/2.58 (define @t132 () (_ tptp.a_select3 @t28)) % 2.21/2.58 (define @t133 () (@var "Body" $$unsorted)) % 2.21/2.58 (define @t134 () (_ (_ (_ tptp.sum tptp.n0) tptp.tptp_minus_1) @t133)) % 2.21/2.58 (define @t135 () (@list @t133 @t10)) % 2.21/2.58 (define @t136 () (_ tptp.plus @t7)) % 2.21/2.58 (define @t137 () (_ tptp.succ @t79)) % 2.21/2.58 (define @t138 () (_ tptp.succ @t137)) % 2.21/2.58 (define @t139 () (_ tptp.succ @t138)) % 2.21/2.58 (define @t140 () (_ tptp.succ @t139)) % 2.21/2.58 (define @t141 () (_ tptp.pred @t7)) % 2.21/2.58 (define @t142 () (_ tptp.minus @t7)) % 2.21/2.58 (define @t143 () (_ tptp.leq @t79)) % 2.21/2.58 (define @t144 () (_ tptp.mbox (_ @t143 @t80))) % 2.21/2.58 (define @t145 () (@var "V" $$unsorted)) % 2.21/2.58 (define @t146 () (_ tptp.tptp_update3 @t7)) % 2.21/2.58 (define @t147 () (_ tptp.a_select3 (_ (_ (_ @t146 @t89) @t145) @t114))) % 2.21/2.58 (define @t148 () (@list @t145 @t10)) % 2.21/2.58 (define @t149 () (@var "VAL2" $$unsorted)) % 2.21/2.58 (define @t150 () (_ tptp.a_select3 @t7)) % 2.21/2.58 (define @t151 () (_ tptp.mand (_ tptp.mbox (_ tptp.mnot (_ tptp.mbox (_ (_ tptp.customqmltpeq @t88) @t89)))))) % 2.21/2.58 (define @t152 () (@list @t149 @t10)) % 2.21/2.58 (define @t153 () (@var "J0" $$unsorted)) % 2.21/2.58 (define @t154 () (@var "I0" $$unsorted)) % 2.21/2.58 (define @t155 () (_ tptp.mbox (_ (_ tptp.leq @t154) @t89))) % 2.21/2.58 (define @t156 () (_ tptp.mand (_ tptp.mbox (_ @t84 @t154)))) % 2.21/2.58 (define @t157 () (@list @t154 @t10)) % 2.21/2.58 (define @t158 () (_ tptp.tptp_update2 @t7)) % 2.21/2.58 (define @t159 () (_ tptp.a_select2 (_ (_ @t158 @t89) @t114))) % 2.21/2.58 (define @t160 () (_ tptp.a_select2 @t7)) % 2.21/2.58 (define @t161 () (_ tptp.mbox tptp.true)) % 2.21/2.58 (define @t162 () (not (_ tptp.mlocal (_ tptp.mbox (_ (_ tptp.mimplies @t161) @t161))))) % 2.21/2.58 (define @t163 () (_ tptp.gt tptp.n5)) % 2.21/2.58 (define @t164 () (_ tptp.gt tptp.n4)) % 2.21/2.58 (define @t165 () (_ tptp.gt tptp.n1)) % 2.21/2.58 (define @t166 () (_ tptp.gt tptp.n2)) % 2.21/2.58 (define @t167 () (_ tptp.gt tptp.n3)) % 2.21/2.58 (define @t168 () (_ tptp.mbox (_ @t11 tptp.n4))) % 2.21/2.58 (define @t169 () (_ tptp.mbox (_ @t11 tptp.n3))) % 2.21/2.58 (define @t170 () (_ tptp.mor @t169)) % 2.21/2.58 (define @t171 () (_ tptp.mbox (_ @t11 tptp.n2))) % 2.21/2.58 (define @t172 () (_ tptp.mor @t171)) % 2.21/2.58 (define @t173 () (_ tptp.mbox (_ @t11 tptp.n1))) % 2.21/2.58 (define @t174 () (_ tptp.mor @t173)) % 2.21/2.58 (define @t175 () (_ tptp.mbox (_ @t11 tptp.n0))) % 2.21/2.58 (define @t176 () (_ tptp.mor @t175)) % 2.21/2.58 (define @t177 () (_ tptp.mand @t85)) % 2.21/2.58 (define @t178 () (_ tptp.succ tptp.n0)) % 2.21/2.58 (define @t179 () (_ tptp.succ @t178)) % 2.21/2.58 (define @t180 () (_ tptp.succ @t179)) % 2.21/2.58 (define @t181 () (_ tptp.succ @t180)) % 2.21/2.58 (define @t182 () (@var "Phi" (-> tptp.mworld Bool))) % 2.21/2.58 (define @t183 () (lambda (@list @t182) (_ @t182 tptp.mactual))) % 2.21/2.58 (define @t184 () (@var "A" (-> tptp.mworld Bool))) % 2.21/2.58 (define @t185 () (_ @t184 @t1)) % 2.21/2.58 (define @t186 () (lambda (@list @t184 @t1) (not @t185))) % 2.21/2.58 (define @t187 () (@var "B" (-> tptp.mworld Bool))) % 2.21/2.58 (define @t188 () (_ @t187 @t1)) % 2.21/2.58 (define @t189 () (@list @t184 @t187 @t1)) % 2.21/2.58 (define @t190 () (lambda @t189 (and @t185 @t188))) % 2.21/2.58 (define @t191 () (lambda @t189 (or @t185 @t188))) % 2.21/2.58 (define @t192 () (lambda @t189 (=> @t185 @t188))) % 2.21/2.58 (define @t193 () (lambda @t189 (= @t185 @t188))) % 2.21/2.58 (define @t194 () (_ @t182 @t5)) % 2.21/2.58 (define @t195 () (@list @t5)) % 2.21/2.58 (define @t196 () (forall @t195 (=> @t6 @t194))) % 2.21/2.58 (define @t197 () (@list @t182 @t1)) % 2.21/2.58 (define @t198 () (lambda @t197 @t196)) % 2.21/2.58 (define @t199 () (lambda @t197 (exists @t195 (and @t6 @t194)))) % 2.21/2.58 (define @t200 () (@var "A" (-> $$unsorted tptp.mworld Bool))) % 2.21/2.58 (define @t201 () (_ (_ @t200 @t7) @t1)) % 2.21/2.58 (define @t202 () (@list @t200 @t1)) % 2.21/2.58 (define @t203 () (lambda @t202 (forall @t9 (=> @t8 @t201)))) % 2.21/2.58 (define @t204 () (lambda @t202 (exists @t9 (and @t8 @t201)))) % 2.21/2.58 (define @t205 () (@var "BOUND_VARIABLE_59359" tptp.mworld)) % 2.21/2.58 (define @t206 () (lambda (@list @t205) true)) % 2.21/2.58 (define @t207 () (_ @t206 tptp.mactual)) % 2.21/2.58 (define @t208 () (tptp.mrel @t1 @t5)) % 2.21/2.58 (define @t209 () (not @t208)) % 2.21/2.58 (define @t210 () (or @t209 true)) % 2.21/2.58 (define @t211 () (@var "BOUND_VARIABLE_59331" tptp.mworld)) % 2.21/2.58 (define @t212 () (tptp.true @t211)) % 2.21/2.58 (define @t213 () (@list @t211)) % 2.21/2.58 (define @t214 () (forall @t213 (or (not (tptp.mrel @t5 @t211)) @t212))) % 2.21/2.58 (define @t215 () (=> @t214 @t214)) % 2.21/2.58 (define @t216 () (or @t209 @t215)) % 2.21/2.58 (define @t217 () (forall @t213 (or (not (tptp.mrel @t1 @t211)) @t212))) % 2.21/2.58 (define @t218 () (forall @t195 (or @t209 (tptp.true @t5)))) % 2.21/2.58 (define @t219 () (=> @t218 @t218)) % 2.21/2.58 (define @t220 () (lambda @t3 @t219)) % 2.21/2.58 (define @t221 () (or @t209 (_ @t220 @t5))) % 2.21/2.58 (define @t222 () (forall @t195 @t221)) % 2.21/2.58 (define @t223 () (lambda @t3 @t222)) % 2.21/2.58 (define @t224 () (_ @t182 @t5)) % 2.21/2.58 (define @t225 () (lambda @t197 (forall @t195 (or @t209 @t224)))) % 2.21/2.58 (define @t226 () (lambda @t3 @t218)) % 2.21/2.58 (define @t227 () (_ @t226 @t1)) % 2.21/2.58 (define @t228 () (=> @t218 @t227)) % 2.21/2.58 (define @t229 () (lambda @t3 @t228)) % 2.21/2.58 (define @t230 () (@list @t187 @t1)) % 2.21/2.58 (define @t231 () (_ @t225 tptp.true)) % 2.21/2.58 (define @t232 () (=> @t227 @t188)) % 2.21/2.58 (define @t233 () (lambda @t230 @t232)) % 2.21/2.58 (define @t234 () (not @t6)) % 2.21/2.58 (define @t235 () (or @t234 @t194)) % 2.21/2.58 (assume @p1 (forall @t3 (_ @t2 @t1))) % 2.21/2.58 (assume @p2 (forall (@list @t1 @t5 @t4) (=> (and @t6 (_ (_ tptp.mrel @t5) @t4)) (_ @t2 @t4)))) % 2.21/2.58 (assume @p3 (forall @t3 (exists @t9 @t8))) % 2.21/2.58 (assume @p4 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ @t11 @t7)) @t10)))))) % 2.21/2.58 (assume @p5 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ tptp.mbox (_ (_ tptp.mimplies @t15) (_ tptp.mbox (_ @t14 @t7)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p6 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t18 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ (_ tptp.mand @t15) (_ tptp.mbox (_ @t14 @t17)))) (_ tptp.mbox (_ @t11 @t17)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p7 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.a_select2 @t21) @t19)) (_ (_ tptp.a_select2 @t20) @t19))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p8 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t27 @t21)) (_ @t27 @t20))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p9 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t30 @t19) @t28)) (_ (_ @t29 @t19) @t28))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p10 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t32 @t21) @t28)) (_ (_ @t32 @t20) @t28))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p11 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t33 @t21)) (_ @t33 @t20))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p12 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.dim @t21) @t19)) (_ (_ tptp.dim @t20) @t19))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p13 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t34 @t21)) (_ @t34 @t20))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p14 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq @t35) (_ tptp.inv @t20))))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p15 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.minus @t21) @t19)) (_ (_ tptp.minus @t20) @t19))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p16 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t36 @t21)) (_ @t36 @t20))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p17 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.plus @t21) @t19)) (_ (_ tptp.plus @t20) @t19))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p18 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t37 @t21)) (_ @t37 @t20))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p19 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ tptp.pred @t21)) (_ tptp.pred @t20))))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p20 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ tptp.succ @t21)) (_ tptp.succ @t20))))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p21 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ (_ tptp.sum @t21) @t19) @t28)) (_ (_ (_ tptp.sum @t20) @t19) @t28))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p22 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t38 @t21) @t28)) (_ (_ @t38 @t20) @t28))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p23 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t39 @t21)) (_ @t39 @t20))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p24 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.tptp_const_array1 @t21) @t19)) (_ (_ tptp.tptp_const_array1 @t20) @t19))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p25 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t40 @t21)) (_ @t40 @t20))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p26 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ (_ tptp.tptp_const_array2 @t21) @t19) @t28)) (_ (_ (_ tptp.tptp_const_array2 @t20) @t19) @t28))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p27 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t41 @t21) @t28)) (_ (_ @t41 @t20) @t28))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p28 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t42 @t21)) (_ @t42 @t20))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p29 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t43 @t19)) (_ (_ tptp.tptp_madd @t20) @t19))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p30 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t44 @t21)) (_ @t44 @t20))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p31 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t46 @t19)) (_ @t45 @t19))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p32 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t47 @t21)) (_ @t47 @t20))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p33 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t48 @t19)) (_ (_ tptp.tptp_msub @t20) @t19))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p34 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t49 @t21)) (_ @t49 @t20))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p35 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ (_ tptp.tptp_update2 @t21) @t19) @t28)) (_ (_ (_ tptp.tptp_update2 @t20) @t19) @t28))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p36 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t50 @t21) @t28)) (_ (_ @t50 @t20) @t28))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p37 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t51 @t21)) (_ @t51 @t20))))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p38 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t54 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ (_ @t53 @t19) @t28) @t52)) (_ (_ (_ (_ tptp.tptp_update3 @t20) @t19) @t28) @t52))))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p39 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t54 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ (_ @t55 @t21) @t28) @t52)) (_ (_ (_ @t55 @t20) @t28) @t52))))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p40 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t54 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t56 @t21) @t52)) (_ (_ @t56 @t20) @t52))))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p41 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t54 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t57 @t21)) (_ @t57 @t20))))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p42 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq @t59) @t58)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p43 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.uniform_int_rnd @t21) @t19)) (_ (_ tptp.uniform_int_rnd @t20) @t19))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p44 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t23 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t60 @t21)) (_ @t60 @t20))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p45 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t61 (_ tptp.mbox (_ (_ tptp.geq @t21) @t19)))) (_ tptp.mbox (_ (_ tptp.geq @t20) @t19)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p46 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t61 (_ tptp.mbox (_ @t62 @t21)))) (_ tptp.mbox (_ @t62 @t20)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p47 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t61 (_ tptp.mbox (_ (_ tptp.gt @t21) @t19)))) (_ tptp.mbox (_ (_ tptp.gt @t20) @t19)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p48 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t61 (_ tptp.mbox (_ @t63 @t21)))) (_ tptp.mbox (_ @t63 @t20)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p49 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t61 (_ tptp.mbox (_ (_ tptp.leq @t21) @t19)))) (_ tptp.mbox (_ (_ tptp.leq @t20) @t19)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p50 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t61 (_ tptp.mbox (_ @t64 @t21)))) (_ tptp.mbox (_ @t64 @t20)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p51 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t61 (_ tptp.mbox (_ (_ tptp.lt @t21) @t19)))) (_ tptp.mbox (_ (_ tptp.lt @t20) @t19)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p52 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t61 (_ tptp.mbox (_ @t65 @t21)))) (_ tptp.mbox (_ @t65 @t20)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p53 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ (_ tptp.mor @t69) (_ (_ tptp.mor @t67) @t15)) @t10)))) @t10)))))) % 2.21/2.58 (assume @p54 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t18 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ (_ tptp.mand @t69) (_ tptp.mbox (_ @t66 @t17)))) (_ tptp.mbox (_ @t68 @t17)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p55 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mnot (_ tptp.mbox (_ @t68 @t7)))) @t10)))))) % 2.21/2.58 (assume @p56 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ @t70 @t7)) @t10)))))) % 2.21/2.58 (assume @p57 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t18 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t73 (_ tptp.mbox (_ @t71 @t17)))) (_ tptp.mbox (_ @t70 @t17)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p58 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ (_ tptp.mand (_ tptp.mbox (_ (_ tptp.mimplies @t74) @t67))) (_ tptp.mbox (_ @t75 @t74))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p59 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ (_ tptp.mand (_ tptp.mbox (_ (_ tptp.mimplies @t76) @t77))) (_ tptp.mbox (_ (_ tptp.mimplies @t77) @t76))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p60 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ tptp.mbox (_ @t75 @t72)) @t10)))) @t10)))))) % 2.21/2.58 (assume @p61 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t73 (_ tptp.mbox (_ tptp.mnot @t15)))) @t67)) @t10)))) @t10)))))) % 2.21/2.58 (assume @p62 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ (_ tptp.mand (_ tptp.mbox (_ (_ tptp.mimplies @t78) @t67))) (_ tptp.mbox (_ @t75 @t78))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p63 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.gt @t79) @t7)) @t10)))))) % 2.21/2.58 (assume @p64 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ tptp.mbox (_ @t81 (_ tptp.mbox (_ @t70 @t80)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p65 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ (_ tptp.mand (_ tptp.mbox (_ @t81 @t82))) (_ tptp.mbox (_ (_ tptp.mimplies @t82) @t72))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p66 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t86 (_ tptp.mbox (_ (_ tptp.leq @t83) @t7)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p67 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ @t86 (_ tptp.mbox (_ @t84 @t83)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p68 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda (@list @t90 @t10) (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t94 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t93 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ (_ tptp.mand (_ tptp.mbox (_ (_ tptp.leq @t90) @t88))) @t92)) (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.a_select2 (_ (_ tptp.tptp_const_array1 (_ (_ tptp.dim @t90) @t89)) @t87)) @t88)) @t87)))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p69 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda (@list @t100 @t10) (_ (_ tptp.mbox (_ tptp.mforall_di (lambda (@list @t99 @t10) (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda (@list @t98 @t10) (_ (_ tptp.mbox (_ tptp.mforall_di (lambda (@list @t97 @t10) (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t93 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ (_ tptp.mand (_ tptp.mbox (_ (_ tptp.leq @t100) @t88))) (_ (_ tptp.mand (_ tptp.mbox (_ @t91 @t99))) (_ (_ tptp.mand (_ tptp.mbox (_ (_ tptp.leq @t98) @t96))) (_ tptp.mbox (_ @t101 @t97)))))) (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ (_ tptp.a_select3 (_ (_ (_ tptp.tptp_const_array2 (_ (_ tptp.dim @t100) @t99)) (_ (_ tptp.dim @t98) @t97)) @t87)) @t88) @t96)) @t87)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p70 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t112 (_ (_ tptp.mbox (_ @t111 (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ @t109 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t103 @t88) @t96)) (_ (_ @t103 @t96) @t88))))) @t10)))) @t10)))))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p71 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t112 (_ (_ tptp.mbox (_ @t111 (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ @t109 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t113 @t88) @t96)) (_ (_ @t113 @t96) @t88))))) @t10)))) @t10)))))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p72 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t112 (_ (_ tptp.mbox (_ @t111 (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda (@list @t115 @t10) (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t117 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t108 (_ @t107 (_ @t106 (_ (_ tptp.mand @t105) (_ (_ tptp.mand (_ tptp.mbox (_ @t84 @t115))) (_ tptp.mbox (_ (_ tptp.leq @t115) @t104)))))))) (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t116 @t88) @t96)) (_ (_ @t116 @t96) @t88))))) @t10)))) @t10)))) @t10)))) @t10)))))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p73 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t112 (_ (_ tptp.mbox (_ @t122 (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ @t109 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t118 @t88) @t96)) (_ (_ @t118 @t96) @t88))))) @t10)))) @t10)))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p74 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t112 (_ (_ tptp.mbox (_ @t122 (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ @t109 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t123 @t88) @t96)) (_ (_ @t123 @t96) @t88))))) @t10)))) @t10)))))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p75 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t112 (_ (_ tptp.mbox (_ (_ tptp.mimplies @t120) @t125)) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p76 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t112 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t128 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ @t127 @t119)) @t10)))) @t10))))) @t125)) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p77 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t26 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t25 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t24 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t31 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t54 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda (@list @t129 @t10) (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t112 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t128 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ (_ tptp.mand (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ @t127 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t132 @t88) @t96)) (_ (_ @t132 @t96) @t88))))) @t10)))) @t10))))) (_ @t121 (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ @t109 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t131 @t88) @t96)) (_ (_ @t131 @t96) @t88))))) @t10)))) @t10))))))) (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ @t109 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t130 @t88) @t96)) (_ (_ @t130 @t96) @t88))))) @t10)))) @t10)))))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p78 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t135 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq @t134) tptp.n0)) @t10)))))) % 2.21/2.58 (assume @p79 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t135 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq tptp.tptp_float_0_0) @t134)) @t10)))))) % 2.21/2.58 (assume @p80 (_ tptp.mlocal (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ tptp.succ tptp.tptp_minus_1)) tptp.n0)))) % 2.21/2.58 (assume @p81 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t136 tptp.n1)) @t79)) @t10)))))) % 2.21/2.58 (assume @p82 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.plus tptp.n1) @t7)) @t79)) @t10)))))) % 2.21/2.58 (assume @p83 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t136 tptp.n2)) @t137)) @t10)))))) % 2.21/2.58 (assume @p84 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.plus tptp.n2) @t7)) @t137)) @t10)))))) % 2.21/2.58 (assume @p85 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t136 tptp.n3)) @t138)) @t10)))))) % 2.21/2.58 (assume @p86 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.plus tptp.n3) @t7)) @t138)) @t10)))))) % 2.21/2.58 (assume @p87 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t136 tptp.n4)) @t139)) @t10)))))) % 2.21/2.58 (assume @p88 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.plus tptp.n4) @t7)) @t139)) @t10)))))) % 2.21/2.58 (assume @p89 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t136 tptp.n5)) @t140)) @t10)))))) % 2.21/2.58 (assume @p90 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.plus tptp.n5) @t7)) @t140)) @t10)))))) % 2.21/2.58 (assume @p91 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t142 tptp.n1)) @t141)) @t10)))))) % 2.21/2.58 (assume @p92 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ tptp.pred @t79)) @t7)) @t10)))))) % 2.21/2.58 (assume @p93 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ tptp.succ @t141)) @t7)) @t10)))))) % 2.21/2.58 (assume @p94 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ (_ tptp.mand (_ tptp.mbox (_ (_ tptp.mimplies @t144) @t72))) (_ tptp.mbox (_ @t81 @t144))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p95 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ tptp.mbox (_ @t143 @t13))) @t67)) @t10)))) @t10)))))) % 2.21/2.58 (assume @p96 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t16 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ tptp.mbox (_ (_ tptp.leq (_ @t142 @t13)) @t7))) (_ tptp.mbox (_ @t84 @t13)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p97 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t94 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t148 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t117 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t147 @t89) @t145)) @t114)) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p98 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t94 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t148 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t117 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t152 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t151 (_ (_ tptp.mand (_ tptp.mbox (_ (_ tptp.customqmltpeq @t96) @t145))) (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t150 @t89) @t145)) @t114))))) (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ (_ tptp.a_select3 (_ (_ (_ @t146 @t88) @t96) @t149)) @t89) @t145)) @t114)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p99 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t102 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t94 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t148 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t117 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ (_ tptp.mand (_ tptp.mbox (_ tptp.mforall_di (lambda @t157 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda (@list @t153 @t10) (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t156 (_ (_ tptp.mand (_ tptp.mbox (_ @t84 @t153))) (_ (_ tptp.mand @t155) (_ tptp.mbox (_ (_ tptp.leq @t153) @t145)))))) (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t150 @t154) @t153)) @t114)))) @t10)))) @t10))))) (_ @t108 (_ (_ tptp.mand @t92) (_ @t106 (_ tptp.mbox (_ @t101 @t145))))))) (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ @t147 @t88) @t96)) @t114)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p100 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t94 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t117 (_ (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t159 @t89)) @t114)) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p101 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t94 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t117 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t152 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t151 (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t160 @t89)) @t114)))) (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ (_ tptp.a_select2 (_ (_ @t158 @t88) @t149)) @t89)) @t114)))) @t10)))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p102 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t95 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t94 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ tptp.mforall_di (lambda @t117 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ (_ tptp.mand (_ tptp.mbox (_ tptp.mforall_di (lambda @t157 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t156 @t155)) (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t160 @t154)) @t114)))) @t10))))) (_ @t108 @t92))) (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ @t159 @t88)) @t114)))) @t10)))) @t10)))) @t10)))) @t10)))))) % 2.21/2.58 (assume @p103 (_ tptp.mlocal @t161)) % 2.21/2.58 (assume @p104 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mnot (_ tptp.mbox (_ (_ tptp.customqmltpeq tptp.def) tptp.use)))))) % 2.21/2.58 (assume @p105 @t162) % 2.21/2.58 (assume @p106 (_ tptp.mlocal (_ tptp.mbox (_ @t163 tptp.n4)))) % 2.21/2.58 (assume @p107 (_ tptp.mlocal (_ tptp.mbox (_ @t164 tptp.tptp_minus_1)))) % 2.21/2.58 (assume @p108 (_ tptp.mlocal (_ tptp.mbox (_ @t163 tptp.tptp_minus_1)))) % 2.21/2.58 (assume @p109 (_ tptp.mlocal (_ tptp.mbox (_ (_ tptp.gt tptp.n0) tptp.tptp_minus_1)))) % 2.21/2.58 (assume @p110 (_ tptp.mlocal (_ tptp.mbox (_ @t165 tptp.tptp_minus_1)))) % 2.21/2.58 (assume @p111 (_ tptp.mlocal (_ tptp.mbox (_ @t166 tptp.tptp_minus_1)))) % 2.21/2.58 (assume @p112 (_ tptp.mlocal (_ tptp.mbox (_ @t167 tptp.tptp_minus_1)))) % 2.21/2.58 (assume @p113 (_ tptp.mlocal (_ tptp.mbox (_ @t164 tptp.n0)))) % 2.21/2.58 (assume @p114 (_ tptp.mlocal (_ tptp.mbox (_ @t163 tptp.n0)))) % 2.21/2.58 (assume @p115 (_ tptp.mlocal (_ tptp.mbox (_ @t165 tptp.n0)))) % 2.21/2.58 (assume @p116 (_ tptp.mlocal (_ tptp.mbox (_ @t166 tptp.n0)))) % 2.21/2.58 (assume @p117 (_ tptp.mlocal (_ tptp.mbox (_ @t167 tptp.n0)))) % 2.21/2.58 (assume @p118 (_ tptp.mlocal (_ tptp.mbox (_ @t164 tptp.n1)))) % 2.21/2.58 (assume @p119 (_ tptp.mlocal (_ tptp.mbox (_ @t163 tptp.n1)))) % 2.21/2.58 (assume @p120 (_ tptp.mlocal (_ tptp.mbox (_ @t166 tptp.n1)))) % 2.21/2.58 (assume @p121 (_ tptp.mlocal (_ tptp.mbox (_ @t167 tptp.n1)))) % 2.21/2.58 (assume @p122 (_ tptp.mlocal (_ tptp.mbox (_ @t164 tptp.n2)))) % 2.21/2.58 (assume @p123 (_ tptp.mlocal (_ tptp.mbox (_ @t163 tptp.n2)))) % 2.21/2.58 (assume @p124 (_ tptp.mlocal (_ tptp.mbox (_ @t167 tptp.n2)))) % 2.21/2.58 (assume @p125 (_ tptp.mlocal (_ tptp.mbox (_ @t164 tptp.n3)))) % 2.21/2.58 (assume @p126 (_ tptp.mlocal (_ tptp.mbox (_ @t163 tptp.n3)))) % 2.21/2.58 (assume @p127 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t177 (_ tptp.mbox (_ @t70 tptp.n4)))) (_ @t176 (_ @t174 (_ @t172 (_ @t170 @t168)))))) @t10)))))) % 2.21/2.58 (assume @p128 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t177 (_ tptp.mbox (_ @t70 tptp.n5)))) (_ @t176 (_ @t174 (_ @t172 (_ @t170 (_ (_ tptp.mor @t168) (_ tptp.mbox (_ @t11 tptp.n5))))))))) @t10)))))) % 2.21/2.58 (assume @p129 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t177 (_ tptp.mbox (_ @t70 tptp.n0)))) @t175)) @t10)))))) % 2.21/2.58 (assume @p130 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t177 (_ tptp.mbox (_ @t70 tptp.n1)))) (_ @t176 @t173))) @t10)))))) % 2.21/2.58 (assume @p131 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t177 (_ tptp.mbox (_ @t70 tptp.n2)))) (_ @t176 (_ @t174 @t171)))) @t10)))))) % 2.21/2.58 (assume @p132 (_ tptp.mlocal (_ tptp.mbox (_ tptp.mforall_di (lambda @t12 (_ (_ tptp.mbox (_ (_ tptp.mimplies (_ @t177 (_ tptp.mbox (_ @t70 tptp.n3)))) (_ @t176 (_ @t174 (_ @t172 @t169))))) @t10)))))) % 2.21/2.58 (assume @p133 (_ tptp.mlocal (_ tptp.mbox (_ (_ tptp.customqmltpeq @t181) tptp.n4)))) % 2.21/2.58 (assume @p134 (_ tptp.mlocal (_ tptp.mbox (_ (_ tptp.customqmltpeq (_ tptp.succ @t181)) tptp.n5)))) % 2.21/2.58 (assume @p135 (_ tptp.mlocal (_ tptp.mbox (_ (_ tptp.customqmltpeq @t178) tptp.n1)))) % 2.21/2.58 (assume @p136 (_ tptp.mlocal (_ tptp.mbox (_ (_ tptp.customqmltpeq @t179) tptp.n2)))) % 2.21/2.58 (assume @p137 (_ tptp.mlocal (_ tptp.mbox (_ (_ tptp.customqmltpeq @t180) tptp.n3)))) % 2.21/2.58 (assume @p138 true) % 2.21/2.58 (step @p139 (= tptp.mlocal @t183) :rule refl :args (@t183)) % 2.21/2.58 (step @p140 (= tptp.mnot @t186) :rule refl :args (@t186)) % 2.21/2.58 (step @p141 (= tptp.mand @t190) :rule refl :args (@t190)) % 2.21/2.58 (step @p142 (= tptp.mor @t191) :rule refl :args (@t191)) % 2.21/2.58 (step @p143 (= tptp.mimplies @t192) :rule refl :args (@t192)) % 2.21/2.58 (step @p144 (= tptp.mequiv @t193) :rule refl :args (@t193)) % 2.21/2.58 (step @p145 (= tptp.mbox @t198) :rule refl :args (@t198)) % 2.21/2.58 (step @p146 (= tptp.mdia @t199) :rule refl :args (@t199)) % 2.21/2.58 (step @p147 (= tptp.mforall_di @t203) :rule refl :args (@t203)) % 2.21/2.58 (step @p148 (= tptp.mexists_di @t204) :rule refl :args (@t204)) % 2.21/2.58 (step @p149 :rule evaluate :args ((not true))) % 2.21/2.58 (step @p150 :rule beta-reduce :args ((= @t207 true))) % 2.21/2.58 (step @p151 :rule beta-reduce :args ((= (_ @t183 @t206) @t207))) % 2.21/2.58 (step @p152 :rule trans :premises (@p151 @p150)) % 2.21/2.58 (step @p153 :rule refl :args (@t206)) % 2.21/2.58 (step @p154 :rule symm :premises (@p153)) % 2.21/2.58 (step @p155 :rule alpha_equiv :args ((lambda @t3 true) (@list @t1) (@list @t205))) % 2.21/2.58 (step @p156 :rule trans :premises (@p155 @p154)) % 2.21/2.58 (step @p157 :rule quant-unused-vars :args ((= (forall @t195 true) true))) % 2.21/2.58 (step @p158 :rule absorb :args ((= @t210 true))) % 2.21/2.58 (step @p159 :rule cong :premises (@p158) :args ((forall @t195 @t210))) % 2.21/2.58 (step @p160 :rule trans :premises (@p159 @p157)) % 2.21/2.58 (step @p161 :rule bool-or-taut2 :args (false @t214 false false)) % 2.21/2.58 (step @p162 :rule bool-impl-elim :args (@t214 @t214)) % 2.21/2.58 (step @p163 :rule trans :premises (@p162 @p161)) % 2.21/2.58 (step @p164 :rule refl :args (@t209)) % 2.21/2.58 (step @p165 :rule nary_cong :premises (@p164 @p163) :args (@t216)) % 2.21/2.58 (step @p166 :rule cong :premises (@p165) :args ((forall @t195 @t216))) % 2.21/2.58 (step @p167 :rule trans :premises (@p166 @p160)) % 2.21/2.58 (step @p168 :rule beta-reduce :args ((= (_ (lambda @t3 (=> @t217 @t217)) @t5) @t215))) % 2.21/2.58 (step @p169 :rule refl :args (@t5)) % 2.21/2.58 (step @p170 :rule alpha_equiv :args (@t218 (@list @t5) (@list @t211))) % 2.21/2.58 (step @p171 :rule cong :premises (@p170 @p170) :args (@t219)) % 2.21/2.58 (step @p172 :rule cong :premises (@p171) :args (@t220)) % 2.21/2.58 (step @p173 :rule ho_cong :premises (@p172 @p169)) % 2.21/2.58 (step @p174 :rule trans :premises (@p173 @p168)) % 2.21/2.58 (step @p175 :rule refl :args (@t209)) % 2.21/2.58 (step @p176 :rule nary_cong :premises (@p175 @p174) :args (@t221)) % 2.21/2.58 (step @p177 :rule cong :premises (@p176) :args (@t222)) % 2.21/2.58 (step @p178 :rule trans :premises (@p177 @p167)) % 2.21/2.58 (step @p179 :rule cong :premises (@p178) :args (@t223)) % 2.21/2.58 (step @p180 :rule trans :premises (@p179 @p156)) % 2.21/2.58 (step @p181 :rule beta-reduce :args ((= (_ @t225 @t220) @t223))) % 2.21/2.58 (step @p182 :rule trans :premises (@p181 @p180)) % 2.21/2.58 (step @p183 :rule beta-reduce :args ((= @t227 @t218))) % 2.21/2.58 (step @p184 :rule refl :args (@t218)) % 2.21/2.58 (step @p185 :rule cong :premises (@p184 @p183) :args (@t228)) % 2.21/2.58 (step @p186 :rule cong :premises (@p185) :args (@t229)) % 2.21/2.58 (step @p187 :rule beta-reduce :args ((= (_ (lambda @t230 (=> @t218 @t188)) @t226) @t229))) % 2.21/2.58 (step @p188 :rule trans :premises (@p187 @p186)) % 2.21/2.58 (step @p189 :rule beta-reduce :args ((= @t231 @t226))) % 2.21/2.58 (step @p190 :rule refl :args (@t188)) % 2.21/2.58 (step @p191 :rule cong :premises (@p183 @p190) :args (@t232)) % 2.21/2.58 (step @p192 :rule cong :premises (@p191) :args (@t233)) % 2.21/2.58 (step @p193 :rule beta-reduce :args ((= (_ @t192 @t226) @t233))) % 2.21/2.58 (step @p194 :rule trans :premises (@p193 @p192)) % 2.21/2.58 (step @p195 :rule refl :args (@t192)) % 2.21/2.58 (step @p196 :rule ho_cong :premises (@p195 @p189)) % 2.21/2.58 (step @p197 :rule trans :premises (@p196 @p194)) % 2.21/2.58 (step @p198 :rule ho_cong :premises (@p197 @p189)) % 2.21/2.58 (step @p199 :rule trans :premises (@p198 @p188)) % 2.21/2.58 (step @p200 :rule refl :args (@t225)) % 2.21/2.58 (step @p201 :rule ho_cong :premises (@p200 @p199)) % 2.21/2.58 (step @p202 :rule trans :premises (@p201 @p182)) % 2.21/2.58 (step @p203 :rule refl :args (@t183)) % 2.21/2.58 (step @p204 :rule ho_cong :premises (@p203 @p202)) % 2.21/2.58 (step @p205 :rule trans :premises (@p204 @p152)) % 2.21/2.58 (step @p206 :rule cong :premises (@p205) :args ((not (_ @t183 (_ @t225 (_ (_ @t192 @t231) @t231)))))) % 2.21/2.58 (step @p207 :rule trans :premises (@p206 @p149)) % 2.21/2.58 (step @p208 :rule refl :args (tptp.true)) % 2.21/2.58 (step @p209 :rule refl :args (@t224)) % 2.21/2.58 (step @p210 :rule refl :args (@t194)) % 2.21/2.58 (step @p211 :rule cong :premises (@p210 @p209) :args ((= @t194 @t224))) % 2.21/2.58 (step @p212 :rule symm :premises (@p211)) % 2.21/2.58 (step @p213 :rule eq_resolve :premises (@p210 @p212)) % 2.21/2.58 (step @p214 :rule refl :args (@t208)) % 2.21/2.58 (step @p215 :rule refl :args (@t6)) % 2.21/2.58 (step @p216 :rule cong :premises (@p215 @p214) :args ((= @t6 @t208))) % 2.21/2.58 (step @p217 :rule symm :premises (@p216)) % 2.21/2.58 (step @p218 :rule eq_resolve :premises (@p215 @p217)) % 2.21/2.58 (step @p219 :rule cong :premises (@p218) :args (@t234)) % 2.21/2.58 (step @p220 :rule nary_cong :premises (@p219 @p213) :args (@t235)) % 2.21/2.58 (step @p221 :rule cong :premises (@p220) :args ((forall @t195 @t235))) % 2.21/2.58 (step @p222 :rule bool-impl-elim :args (@t6 @t194)) % 2.21/2.58 (step @p223 :rule cong :premises (@p222) :args (@t196)) % 2.21/2.58 (step @p224 :rule trans :premises (@p223 @p221)) % 2.21/2.58 (step @p225 :rule cong :premises (@p224) :args (@t198)) % 2.21/2.58 (step @p226 :rule trans :premises (@p145 @p225)) % 2.21/2.58 (step @p227 :rule ho_cong :premises (@p226 @p208)) % 2.21/2.58 (step @p228 :rule ho_cong :premises (@p143 @p227)) % 2.21/2.58 (step @p229 :rule ho_cong :premises (@p228 @p227)) % 2.21/2.58 (step @p230 :rule ho_cong :premises (@p226 @p229)) % 2.21/2.58 (step @p231 :rule ho_cong :premises (@p139 @p230)) % 2.21/2.58 (step @p232 :rule cong :premises (@p231) :args (@t162)) % 2.21/2.58 (step @p233 :rule trans :premises (@p232 @p207)) % 2.21/2.58 (step @p234 false :rule eq_resolve :premises (@p105 @p233)) % 2.21/2.58 ) % 2.21/2.58 % SZS output end Proof % 2.21/2.58 % cvc5 exiting %------------------------------------------------------------------------------