cvc5---1.3.4.THM-Prf.s

%------------------------------------------------------------------------------
% File     : cvc5---1.3.4
% Problem  : ITP044^1 : TPTP v9.2.1. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n009.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:24:53 AM UTC 2026

% Result   : Theorem 0.43s 0.85s
% Output   : Proof 0.43s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : ITP044^1 : TPTP v9.2.1. Released v7.5.0.
% 0.11/0.14  % Command  : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.18/0.35  % Computer : n009.cluster.edu
% 0.18/0.35  % Model    : x86_64 x86_64
% 0.18/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.35  % Memory   : 8042.1875MB
% 0.18/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.18/0.35  % CPULimit : 300
% 0.18/0.35  % WCLimit  : 300
% 0.18/0.35  % DateTime : Tue Jun  2 04:11:44 EDT 2026
% 0.18/0.35  % CPUTime  : 
% 0.36/0.60  %----Proving TH0
% 0.43/0.85  --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --sygus-grammar-ho-partial --no-cegqi --no-sygus-inst at 90s...
% 0.43/0.85  % SZS status Theorem
% 0.43/0.85  % SZS output start Proof
% 0.43/0.85  (
% 0.43/0.85  (declare-sort tptp.list_a 0)
% 0.43/0.85  (declare-sort tptp.list_list_a 0)
% 0.43/0.85  (declare-sort tptp.a 0)
% 0.43/0.85  (declare-sort tptp.list_nat 0)
% 0.43/0.85  (declare-sort tptp.poly_nat 0)
% 0.43/0.85  (declare-sort tptp.list_poly_a 0)
% 0.43/0.85  (declare-sort tptp.nat 0)
% 0.43/0.85  (declare-sort tptp.poly_a 0)
% 0.43/0.85  (declare-sort tptp.poly_poly_a 0)
% 0.43/0.85  (declare-const tptp.coeffs_a (-> tptp.poly_a tptp.list_a))
% 0.43/0.85  (declare-const tptp.descar2095969287nges_a (-> tptp.list_a tptp.nat))
% 0.43/0.85  (declare-const tptp.coeffs_poly_a (-> tptp.poly_poly_a tptp.list_poly_a))
% 0.43/0.85  (declare-const tptp.null_poly_a (-> tptp.list_poly_a Bool))
% 0.43/0.85  (declare-const tptp.null_a (-> tptp.list_a Bool))
% 0.43/0.85  (declare-const tptp.nil_list_a tptp.list_list_a)
% 0.43/0.85  (declare-const tptp.cons_list_a (-> tptp.list_a tptp.list_list_a tptp.list_list_a))
% 0.43/0.85  (declare-const tptp.ord_less_nat (-> tptp.nat tptp.nat Bool))
% 0.43/0.85  (declare-const tptp.append_nat (-> tptp.list_nat tptp.list_nat tptp.list_nat))
% 0.43/0.85  (declare-const tptp.poly_nat2 (-> tptp.list_nat tptp.poly_nat))
% 0.43/0.85  (declare-const tptp.append_poly_a (-> tptp.list_poly_a tptp.list_poly_a tptp.list_poly_a))
% 0.43/0.85  (declare-const tptp.coeffs_nat (-> tptp.poly_nat tptp.list_nat))
% 0.43/0.85  (declare-const tptp.nil_nat tptp.list_nat)
% 0.43/0.85  (declare-const tptp.one_one_poly_poly_a tptp.poly_poly_a)
% 0.43/0.85  (declare-const tptp.cons_nat (-> tptp.nat tptp.list_nat tptp.list_nat))
% 0.43/0.85  (declare-const tptp.descar226543321ms_nat (-> tptp.list_nat tptp.list_nat))
% 0.43/0.85  (declare-const tptp.descar282223555poly_a (-> tptp.list_poly_a tptp.list_poly_a))
% 0.43/0.85  (declare-const tptp.one_one_poly_a tptp.poly_a)
% 0.43/0.85  (declare-const tptp.one_one_poly_nat tptp.poly_nat)
% 0.43/0.85  (declare-const tptp.pCons_poly_a (-> tptp.poly_a tptp.poly_poly_a tptp.poly_poly_a))
% 0.43/0.85  (declare-const tptp.zero_z2096148049poly_a tptp.poly_poly_a)
% 0.43/0.85  (declare-const tptp.cons_a (-> tptp.a tptp.list_a tptp.list_a))
% 0.43/0.85  (declare-const tptp.one_one_a tptp.a)
% 0.43/0.85  (declare-const tptp.nil_a tptp.list_a)
% 0.43/0.85  (declare-const tptp.poly_a2 (-> tptp.list_a tptp.poly_a))
% 0.43/0.85  (declare-const tptp.descar466059845root_a (-> tptp.a tptp.poly_a tptp.poly_a))
% 0.43/0.85  (declare-const tptp.append_a (-> tptp.list_a tptp.list_a tptp.list_a))
% 0.43/0.85  (declare-const tptp.poly_poly_a2 (-> tptp.list_poly_a tptp.poly_poly_a))
% 0.43/0.85  (declare-const tptp.descar434775507poly_a (-> tptp.poly_a tptp.poly_poly_a tptp.poly_poly_a))
% 0.43/0.85  (declare-const tptp.descar357075861poly_a (-> tptp.list_poly_a tptp.nat))
% 0.43/0.85  (declare-const tptp.zero_zero_poly_nat tptp.poly_nat)
% 0.43/0.85  (declare-const tptp.ys tptp.list_a)
% 0.43/0.85  (declare-const tptp.descar1375166517sums_a (-> tptp.list_a tptp.list_a))
% 0.43/0.85  (declare-const tptp.ord_less_poly_a (-> tptp.poly_a tptp.poly_a Bool))
% 0.43/0.85  (declare-const tptp.zero_zero_a tptp.a)
% 0.43/0.85  (declare-const tptp.zero_zero_poly_a tptp.poly_a)
% 0.43/0.85  (declare-const tptp.ord_less_a (-> tptp.a tptp.a Bool))
% 0.43/0.85  (declare-const tptp.xs tptp.list_a)
% 0.43/0.85  (declare-const tptp.zero_zero_nat tptp.nat)
% 0.43/0.85  (declare-const tptp.nil_poly_a tptp.list_poly_a)
% 0.43/0.85  (declare-const tptp.uminus_uminus_a (-> tptp.a tptp.a))
% 0.43/0.85  (declare-const tptp.times_times_poly_a (-> tptp.poly_a tptp.poly_a tptp.poly_a))
% 0.43/0.85  (declare-const tptp.pCons_a (-> tptp.a tptp.poly_a tptp.poly_a))
% 0.43/0.85  (declare-const tptp.smult_a (-> tptp.a tptp.poly_a tptp.poly_a))
% 0.43/0.85  (declare-const tptp.g tptp.poly_a)
% 0.43/0.85  (declare-const tptp.uminus_uminus_poly_a (-> tptp.poly_a tptp.poly_a))
% 0.43/0.85  (declare-const tptp.times_times_a (-> tptp.a tptp.a tptp.a))
% 0.43/0.85  (declare-const tptp.smult_poly_a (-> tptp.poly_a tptp.poly_poly_a tptp.poly_poly_a))
% 0.43/0.85  (declare-const tptp.cons_poly_a (-> tptp.poly_a tptp.list_poly_a tptp.list_poly_a))
% 0.43/0.85  (declare-const tptp.pCons_nat (-> tptp.nat tptp.poly_nat tptp.poly_nat))
% 0.43/0.85  (declare-const tptp.times_times_nat (-> tptp.nat tptp.nat tptp.nat))
% 0.43/0.85  (declare-const tptp.smult_nat (-> tptp.nat tptp.poly_nat tptp.poly_nat))
% 0.43/0.85  (declare-const tptp.one_one_nat tptp.nat)
% 0.43/0.85  (define tptp.v () (let ((_let_1 (@var "F" tptp.poly_a))) (lambda (@list _let_1) (_ tptp.descar2095969287nges_a (_ tptp.coeffs_a _let_1)))))
% 0.43/0.85  (define tptp.is_zero_poly_a () (let ((_let_1 (@var "P" tptp.poly_poly_a))) (lambda (@list _let_1) (_ tptp.null_poly_a (_ tptp.coeffs_poly_a _let_1)))))
% 0.43/0.85  (define tptp.is_zero_a () (let ((_let_1 (@var "P" tptp.poly_a))) (lambda (@list _let_1) (_ tptp.null_a (_ tptp.coeffs_a _let_1)))))
% 0.43/0.85  (define @t1 () (@var "Q" tptp.poly_poly_a))
% 0.43/0.85  (define @t2 () (@var "P" tptp.poly_poly_a))
% 0.43/0.85  (define @t3 () (_ tptp.coeffs_poly_a @t2))
% 0.43/0.85  (define @t4 () (@var "Z" tptp.poly_poly_a))
% 0.43/0.85  (define @t5 () (@var "Y" tptp.poly_poly_a))
% 0.43/0.85  (define @t6 () (@var "Q" tptp.poly_a))
% 0.43/0.85  (define @t7 () (@var "P" tptp.poly_a))
% 0.43/0.85  (define @t8 () (_ tptp.coeffs_a @t7))
% 0.43/0.85  (define @t9 () (@var "Z" tptp.poly_a))
% 0.43/0.85  (define @t10 () (@var "Y" tptp.poly_a))
% 0.43/0.85  (define @t11 () (@var "P2" tptp.poly_poly_a))
% 0.43/0.85  (define @t12 () (_ tptp.coeffs_poly_a @t11))
% 0.43/0.85  (define @t13 () (_ tptp.descar357075861poly_a @t12))
% 0.43/0.85  (define @t14 () (@var "Xs" tptp.list_poly_a))
% 0.43/0.85  (define @t15 () (_ tptp.descar357075861poly_a @t14))
% 0.43/0.85  (define @t16 () (@var "P2" tptp.poly_a))
% 0.43/0.85  (define @t17 () (_ tptp.coeffs_a @t16))
% 0.43/0.85  (define @t18 () (_ tptp.descar2095969287nges_a @t17))
% 0.43/0.85  (define @t19 () (@var "Xs" tptp.list_a))
% 0.43/0.85  (define @t20 () (_ tptp.descar2095969287nges_a @t19))
% 0.43/0.85  (define @t21 () (= @t20 @t18))
% 0.43/0.85  (define @t22 () (_ tptp.poly_a2 @t19))
% 0.43/0.85  (define @t23 () (=> (= @t22 @t16) @t21))
% 0.43/0.85  (define @t24 () (@list @t19 @t16))
% 0.43/0.85  (define @t25 () (forall @t24 @t23))
% 0.43/0.85  (define @t26 () (_ tptp.cons_a tptp.zero_zero_a))
% 0.43/0.85  (define @t27 () (_ @t26 tptp.nil_a))
% 0.43/0.85  (define @t28 () (_ tptp.coeffs_a tptp.g))
% 0.43/0.85  (define @t29 () (_ tptp.append_a @t28))
% 0.43/0.85  (define @t30 () (= tptp.ys (_ @t29 @t27)))
% 0.43/0.85  (define @t31 () (@var "A" tptp.poly_a))
% 0.43/0.85  (define @t32 () (_ tptp.descar434775507poly_a @t31))
% 0.43/0.85  (define @t33 () (_ @t32 @t11))
% 0.43/0.85  (define @t34 () (_ tptp.ord_less_poly_a tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t35 () (_ @t34 @t31))
% 0.43/0.85  (define @t36 () (@list @t31 @t11))
% 0.43/0.85  (define @t37 () (@var "A" tptp.a))
% 0.43/0.85  (define @t38 () (_ tptp.descar466059845root_a @t37))
% 0.43/0.85  (define @t39 () (_ @t38 @t16))
% 0.43/0.85  (define @t40 () (_ tptp.ord_less_a tptp.zero_zero_a))
% 0.43/0.85  (define @t41 () (_ @t40 @t37))
% 0.43/0.85  (define @t42 () (@list @t37 @t16))
% 0.43/0.85  (define @t43 () (@list @t11))
% 0.43/0.85  (define @t44 () (_ tptp.poly_a2 @t17))
% 0.43/0.85  (define @t45 () (@list @t16))
% 0.43/0.85  (define @t46 () (forall @t45 (= @t44 @t16)))
% 0.43/0.85  (define @t47 () (_ tptp.uminus_uminus_a tptp.one_one_a))
% 0.43/0.85  (define @t48 () (_ (_ tptp.pCons_a @t47) tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t49 () (_ tptp.pCons_a tptp.one_one_a))
% 0.43/0.85  (define @t50 () (_ @t49 @t48))
% 0.43/0.85  (define @t51 () (_ (_ tptp.times_times_poly_a @t50) tptp.g))
% 0.43/0.85  (define @t52 () (_ tptp.coeffs_a @t51))
% 0.43/0.85  (define @t53 () (_ tptp.smult_a @t37))
% 0.43/0.85  (define @t54 () (_ @t53 @t16))
% 0.43/0.85  (define @t55 () (_ tptp.smult_poly_a @t31))
% 0.43/0.85  (define @t56 () (_ @t55 @t11))
% 0.43/0.85  (define @t57 () (_ @t26 @t19))
% 0.43/0.85  (define @t58 () (@list @t19))
% 0.43/0.85  (define @t59 () (_ tptp.cons_poly_a tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t60 () (_ @t59 @t14))
% 0.43/0.85  (define @t61 () (@list @t14))
% 0.43/0.85  (define @t62 () (@var "X" tptp.a))
% 0.43/0.85  (define @t63 () (_ tptp.cons_a @t62))
% 0.43/0.85  (define @t64 () (_ @t63 @t19))
% 0.43/0.85  (define @t65 () (@list @t62 @t19))
% 0.43/0.85  (define @t66 () (@var "X" tptp.poly_a))
% 0.43/0.85  (define @t67 () (_ tptp.cons_poly_a @t66))
% 0.43/0.85  (define @t68 () (@var "Q2" tptp.poly_a))
% 0.43/0.85  (define @t69 () (@var "B" tptp.a))
% 0.43/0.85  (define @t70 () (= @t37 @t69))
% 0.43/0.85  (define @t71 () (_ tptp.pCons_a @t69))
% 0.43/0.85  (define @t72 () (_ tptp.pCons_a @t37))
% 0.43/0.85  (define @t73 () (_ @t72 @t16))
% 0.43/0.85  (define @t74 () (_ tptp.uminus_uminus_a @t37))
% 0.43/0.85  (define @t75 () (@var "B" tptp.poly_a))
% 0.43/0.85  (define @t76 () (_ tptp.times_times_poly_a @t31))
% 0.43/0.85  (define @t77 () (_ @t76 @t75))
% 0.43/0.85  (define @t78 () (@list @t31 @t75 @t11))
% 0.43/0.85  (define @t79 () (@var "P2" tptp.poly_nat))
% 0.43/0.85  (define @t80 () (@var "B" tptp.nat))
% 0.43/0.85  (define @t81 () (@var "A" tptp.nat))
% 0.43/0.85  (define @t82 () (_ tptp.times_times_nat @t81))
% 0.43/0.85  (define @t83 () (_ @t82 @t80))
% 0.43/0.85  (define @t84 () (_ tptp.smult_nat @t81))
% 0.43/0.85  (define @t85 () (@list @t81 @t80 @t79))
% 0.43/0.85  (define @t86 () (@list @t79))
% 0.43/0.85  (define @t87 () (@list @t37))
% 0.43/0.85  (define @t88 () (_ tptp.times_times_poly_a @t16))
% 0.43/0.85  (define @t89 () (_ @t53 (_ @t88 @t68)))
% 0.43/0.85  (define @t90 () (= @t11 tptp.zero_z2096148049poly_a))
% 0.43/0.85  (define @t91 () (= @t31 tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t92 () (= @t79 tptp.zero_zero_poly_nat))
% 0.43/0.85  (define @t93 () (= @t81 tptp.zero_zero_nat))
% 0.43/0.85  (define @t94 () (@list @t81 @t79))
% 0.43/0.85  (define @t95 () (= @t16 tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t96 () (= @t37 tptp.zero_zero_a))
% 0.43/0.85  (define @t97 () (_ (_ tptp.pCons_nat tptp.one_one_nat) tptp.zero_zero_poly_nat))
% 0.43/0.85  (define @t98 () (_ @t49 tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t99 () (_ @t84 @t79))
% 0.43/0.85  (define @t100 () (_ tptp.times_times_a @t37))
% 0.43/0.85  (define @t101 () (_ @t100 @t69))
% 0.43/0.85  (define @t102 () (= @t12 tptp.nil_poly_a))
% 0.43/0.85  (define @t103 () (= @t17 tptp.nil_a))
% 0.43/0.85  (define @t104 () (_ tptp.coeffs_a tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t105 () (@var "Xs" tptp.list_nat))
% 0.43/0.85  (define @t106 () (_ tptp.cons_nat tptp.zero_zero_nat))
% 0.43/0.85  (define @t107 () (_ @t63 tptp.nil_a))
% 0.43/0.85  (define @t108 () (@list @t62))
% 0.43/0.85  (define @t109 () (@list @t66))
% 0.43/0.85  (define @t110 () (@var "As" tptp.list_poly_a))
% 0.43/0.85  (define @t111 () (@var "As" tptp.list_a))
% 0.43/0.85  (define @t112 () (_ tptp.poly_a2 @t111))
% 0.43/0.85  (define @t113 () (_ tptp.append_a @t111))
% 0.43/0.85  (define @t114 () (_ @t113 @t27))
% 0.43/0.85  (define @t115 () (_ tptp.poly_a2 @t114))
% 0.43/0.85  (define @t116 () (= @t115 @t112))
% 0.43/0.85  (define @t117 () (@list @t111))
% 0.43/0.85  (define @t118 () (forall @t117 @t116))
% 0.43/0.85  (define @t119 () (@var "As" tptp.list_nat))
% 0.43/0.85  (define @t120 () (@var "Q3" tptp.poly_a))
% 0.43/0.85  (define @t121 () (@var "A2" tptp.a))
% 0.43/0.85  (define @t122 () (_ tptp.pCons_a @t121))
% 0.43/0.85  (define @t123 () (@list @t7))
% 0.43/0.85  (define @t124 () (@var "P3" (-> tptp.poly_poly_a Bool)))
% 0.43/0.85  (define @t125 () (@var "P4" tptp.poly_poly_a))
% 0.43/0.85  (define @t126 () (@var "A2" tptp.poly_a))
% 0.43/0.85  (define @t127 () (@var "P3" (-> tptp.poly_nat Bool)))
% 0.43/0.85  (define @t128 () (@var "P4" tptp.poly_nat))
% 0.43/0.85  (define @t129 () (@var "A2" tptp.nat))
% 0.43/0.85  (define @t130 () (@var "P3" (-> tptp.poly_a Bool)))
% 0.43/0.85  (define @t131 () (@var "P4" tptp.poly_a))
% 0.43/0.85  (define @t132 () (_ @t122 @t131))
% 0.43/0.85  (define @t133 () (_ @t130 @t132))
% 0.43/0.85  (define @t134 () (_ @t130 @t131))
% 0.43/0.85  (define @t135 () (not (= @t131 tptp.zero_zero_poly_a)))
% 0.43/0.85  (define @t136 () (@list @t121 @t131))
% 0.43/0.85  (define @t137 () (@var "P3" (-> tptp.poly_a tptp.poly_a Bool)))
% 0.43/0.85  (define @t138 () (@var "B2" tptp.a))
% 0.43/0.85  (define @t139 () (@var "A0" tptp.poly_a))
% 0.43/0.85  (define @t140 () (_ tptp.times_times_poly_a tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t141 () (@var "A1" tptp.list_a))
% 0.43/0.85  (define @t142 () (@var "A0" tptp.list_a))
% 0.43/0.85  (define @t143 () (@var "P3" (-> tptp.list_a tptp.list_a Bool)))
% 0.43/0.85  (define @t144 () (_ (_ @t143 @t142) @t141))
% 0.43/0.85  (define @t145 () (@var "Ys" tptp.list_a))
% 0.43/0.85  (define @t146 () (@var "Y2" tptp.a))
% 0.43/0.85  (define @t147 () (_ tptp.cons_a @t146))
% 0.43/0.85  (define @t148 () (_ @t147 @t145))
% 0.43/0.85  (define @t149 () (@var "Xs2" tptp.list_a))
% 0.43/0.85  (define @t150 () (@var "X2" tptp.a))
% 0.43/0.85  (define @t151 () (_ tptp.cons_a @t150))
% 0.43/0.85  (define @t152 () (_ @t151 @t149))
% 0.43/0.85  (define @t153 () (_ @t143 @t152))
% 0.43/0.85  (define @t154 () (_ @t153 @t148))
% 0.43/0.85  (define @t155 () (_ @t143 @t149))
% 0.43/0.85  (define @t156 () (@list @t150 @t149 @t146 @t145))
% 0.43/0.85  (define @t157 () (forall @t156 (=> (_ @t155 @t145) @t154)))
% 0.43/0.85  (define @t158 () (@var "Va" tptp.list_a))
% 0.43/0.85  (define @t159 () (@var "V" tptp.a))
% 0.43/0.85  (define @t160 () (_ @t143 tptp.nil_a))
% 0.43/0.85  (define @t161 () (forall (@list @t149) (_ @t155 tptp.nil_a)))
% 0.43/0.85  (define @t162 () (@list @t143 @t142 @t141))
% 0.43/0.85  (define @t163 () (not @t90))
% 0.43/0.85  (define @t164 () (not @t95))
% 0.43/0.85  (define @t165 () (forall (@list @t146 @t145) (_ @t160 @t148)))
% 0.43/0.85  (define @t166 () (@var "C" tptp.a))
% 0.43/0.85  (define @t167 () (_ tptp.smult_a @t166))
% 0.43/0.85  (define @t168 () (_ @t147 @t149))
% 0.43/0.85  (define @t169 () (_ @t151 @t168))
% 0.43/0.85  (define @t170 () (@var "X" tptp.list_a))
% 0.43/0.85  (define @t171 () (@list @t150 @t146 @t149))
% 0.43/0.85  (define @t172 () (_ @t151 tptp.nil_a))
% 0.43/0.85  (define @t173 () (@list @t150))
% 0.43/0.85  (define @t174 () (= @t170 tptp.nil_a))
% 0.43/0.85  (define @t175 () (not @t174))
% 0.43/0.85  (define @t176 () (@list @t170))
% 0.43/0.85  (define @t177 () (_ tptp.pCons_a @t166))
% 0.43/0.85  (define @t178 () (@var "C" tptp.poly_a))
% 0.43/0.85  (define @t179 () (_ tptp.pCons_poly_a @t178))
% 0.43/0.85  (define @t180 () (not @t96))
% 0.43/0.85  (define @t181 () (not @t91))
% 0.43/0.85  (define @t182 () (@var "Y3" tptp.a))
% 0.43/0.85  (define @t183 () (_ tptp.cons_a @t182))
% 0.43/0.85  (define @t184 () (_ @t183 @t19))
% 0.43/0.85  (define @t185 () (@var "Y3" tptp.poly_a))
% 0.43/0.85  (define @t186 () (_ tptp.cons_poly_a @t185))
% 0.43/0.85  (define @t187 () (_ @t186 @t14))
% 0.43/0.85  (define @t188 () (= @t62 @t182))
% 0.43/0.85  (define @t189 () (@var "Ys2" tptp.list_a))
% 0.43/0.85  (define @t190 () (= @t19 @t189))
% 0.43/0.85  (define @t191 () (_ @t183 tptp.nil_a))
% 0.43/0.85  (define @t192 () (_ tptp.append_a @t189))
% 0.43/0.85  (define @t193 () (_ tptp.append_a @t19))
% 0.43/0.85  (define @t194 () (@var "Z2" tptp.poly_a))
% 0.43/0.85  (define @t195 () (_ tptp.uminus_uminus_poly_a @t194))
% 0.43/0.85  (define @t196 () (_ tptp.uminus_uminus_poly_a tptp.one_one_poly_a))
% 0.43/0.85  (define @t197 () (@list @t194))
% 0.43/0.85  (define @t198 () (@var "Z2" tptp.a))
% 0.43/0.85  (define @t199 () (_ tptp.uminus_uminus_a @t198))
% 0.43/0.85  (define @t200 () (@list @t198))
% 0.43/0.85  (define @t201 () (_ tptp.ord_less_poly_a @t31))
% 0.43/0.85  (define @t202 () (_ @t201 tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t203 () (_ tptp.uminus_uminus_poly_a @t31))
% 0.43/0.85  (define @t204 () (@list @t31))
% 0.43/0.85  (define @t205 () (_ tptp.ord_less_a @t37))
% 0.43/0.85  (define @t206 () (_ @t205 tptp.zero_zero_a))
% 0.43/0.85  (define @t207 () (_ tptp.ord_less_poly_a @t203))
% 0.43/0.85  (define @t208 () (_ tptp.ord_less_a @t74))
% 0.43/0.85  (define @t209 () (= @t166 tptp.zero_zero_a))
% 0.43/0.85  (define @t210 () (or @t209 (= @t69 tptp.one_one_a)))
% 0.43/0.85  (define @t211 () (_ tptp.times_times_a @t166))
% 0.43/0.85  (define @t212 () (_ @t211 @t69))
% 0.43/0.85  (define @t213 () (@list @t166 @t69))
% 0.43/0.85  (define @t214 () (= @t178 tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t215 () (or @t214 (= @t75 tptp.one_one_poly_a)))
% 0.43/0.85  (define @t216 () (_ tptp.times_times_poly_a @t178))
% 0.43/0.85  (define @t217 () (_ @t216 @t75))
% 0.43/0.85  (define @t218 () (@list @t178 @t75))
% 0.43/0.85  (define @t219 () (or @t209 (= @t37 tptp.one_one_a)))
% 0.43/0.85  (define @t220 () (_ @t211 @t37))
% 0.43/0.85  (define @t221 () (or @t214 (= @t31 tptp.one_one_poly_a)))
% 0.43/0.85  (define @t222 () (_ @t216 @t31))
% 0.43/0.85  (define @t223 () (_ tptp.times_times_a @t69))
% 0.43/0.85  (define @t224 () (_ @t223 @t166))
% 0.43/0.85  (define @t225 () (_ tptp.times_times_poly_a @t75))
% 0.43/0.85  (define @t226 () (_ @t225 @t178))
% 0.43/0.85  (define @t227 () (_ @t100 @t166))
% 0.43/0.85  (define @t228 () (_ @t76 @t178))
% 0.43/0.85  (define @t229 () (_ tptp.uminus_uminus_a @t69))
% 0.43/0.85  (define @t230 () (@list @t37 @t69))
% 0.43/0.85  (define @t231 () (@var "Y22" tptp.list_a))
% 0.43/0.85  (define @t232 () (@var "X22" tptp.list_a))
% 0.43/0.85  (define @t233 () (@var "Y21" tptp.a))
% 0.43/0.85  (define @t234 () (@var "X21" tptp.a))
% 0.43/0.85  (define @t235 () (_ (_ tptp.cons_a @t234) @t232))
% 0.43/0.85  (define @t236 () (@var "Zs" tptp.list_a))
% 0.43/0.85  (define @t237 () (= @t189 @t236))
% 0.43/0.85  (define @t238 () (_ @t193 @t189))
% 0.43/0.85  (define @t239 () (@list @t19 @t189 @t236))
% 0.43/0.85  (define @t240 () (_ tptp.append_a @t236))
% 0.43/0.85  (define @t241 () (_ @t192 @t236))
% 0.43/0.85  (define @t242 () (@var "C" tptp.list_a))
% 0.43/0.85  (define @t243 () (@var "B" tptp.list_a))
% 0.43/0.85  (define @t244 () (@var "A" tptp.list_a))
% 0.43/0.85  (define @t245 () (_ tptp.append_a @t244))
% 0.43/0.85  (define @t246 () (@var "N" tptp.nat))
% 0.43/0.85  (define @t247 () (= @t246 tptp.zero_zero_nat))
% 0.43/0.85  (define @t248 () (_ tptp.ord_less_nat tptp.zero_zero_nat))
% 0.43/0.85  (define @t249 () (_ @t248 @t246))
% 0.43/0.85  (define @t250 () (@list @t246))
% 0.43/0.85  (define @t251 () (or @t209 @t70))
% 0.43/0.85  (define @t252 () (= @t227 @t224))
% 0.43/0.85  (define @t253 () (@list @t37 @t166 @t69))
% 0.43/0.85  (define @t254 () (= @t31 @t75))
% 0.43/0.85  (define @t255 () (or @t214 @t254))
% 0.43/0.85  (define @t256 () (= @t228 @t226))
% 0.43/0.85  (define @t257 () (@list @t31 @t178 @t75))
% 0.43/0.85  (define @t258 () (= @t81 @t80))
% 0.43/0.85  (define @t259 () (@var "C" tptp.nat))
% 0.43/0.85  (define @t260 () (= @t259 tptp.zero_zero_nat))
% 0.43/0.85  (define @t261 () (or @t260 @t258))
% 0.43/0.85  (define @t262 () (_ tptp.times_times_nat @t80))
% 0.43/0.85  (define @t263 () (_ @t262 @t259))
% 0.43/0.85  (define @t264 () (_ @t82 @t259))
% 0.43/0.85  (define @t265 () (= @t264 @t263))
% 0.43/0.85  (define @t266 () (= @t220 @t212))
% 0.43/0.85  (define @t267 () (@list @t166 @t37 @t69))
% 0.43/0.85  (define @t268 () (= @t222 @t217))
% 0.43/0.85  (define @t269 () (@list @t178 @t31 @t75))
% 0.43/0.85  (define @t270 () (_ tptp.times_times_nat @t259))
% 0.43/0.85  (define @t271 () (_ @t270 @t80))
% 0.43/0.85  (define @t272 () (_ @t270 @t81))
% 0.43/0.85  (define @t273 () (= @t272 @t271))
% 0.43/0.85  (define @t274 () (@list @t259 @t81 @t80))
% 0.43/0.85  (define @t275 () (= @t69 tptp.zero_zero_a))
% 0.43/0.85  (define @t276 () (or @t96 @t275))
% 0.43/0.85  (define @t277 () (= @t101 tptp.zero_zero_a))
% 0.43/0.85  (define @t278 () (= @t75 tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t279 () (or @t91 @t278))
% 0.43/0.85  (define @t280 () (= @t77 tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t281 () (@list @t31 @t75))
% 0.43/0.85  (define @t282 () (= @t80 tptp.zero_zero_nat))
% 0.43/0.85  (define @t283 () (or @t93 @t282))
% 0.43/0.85  (define @t284 () (= @t83 tptp.zero_zero_nat))
% 0.43/0.85  (define @t285 () (@list @t81 @t80))
% 0.43/0.85  (define @t286 () (@list @t81))
% 0.43/0.85  (define @t287 () (_ tptp.times_times_nat tptp.zero_zero_nat))
% 0.43/0.85  (define @t288 () (_ tptp.times_times_nat tptp.one_one_nat))
% 0.43/0.85  (define @t289 () (_ @t201 @t75))
% 0.43/0.85  (define @t290 () (_ tptp.uminus_uminus_poly_a @t75))
% 0.43/0.85  (define @t291 () (_ tptp.ord_less_poly_a @t290))
% 0.43/0.85  (define @t292 () (@list @t75 @t31))
% 0.43/0.85  (define @t293 () (_ @t205 @t69))
% 0.43/0.85  (define @t294 () (_ tptp.ord_less_a @t229))
% 0.43/0.85  (define @t295 () (@list @t69 @t37))
% 0.43/0.85  (define @t296 () (_ tptp.uminus_uminus_poly_a @t77))
% 0.43/0.85  (define @t297 () (_ @t76 @t290))
% 0.43/0.85  (define @t298 () (_ tptp.uminus_uminus_a @t101))
% 0.43/0.85  (define @t299 () (_ @t100 @t229))
% 0.43/0.85  (define @t300 () (_ tptp.times_times_poly_a @t203))
% 0.43/0.85  (define @t301 () (_ tptp.times_times_a @t74))
% 0.43/0.85  (define @t302 () (_ @t300 @t75))
% 0.43/0.85  (define @t303 () (_ @t301 @t69))
% 0.43/0.85  (define @t304 () (@list @t244))
% 0.43/0.85  (define @t305 () (= @t189 tptp.nil_a))
% 0.43/0.85  (define @t306 () (= @t19 tptp.nil_a))
% 0.43/0.85  (define @t307 () (and @t306 @t305))
% 0.43/0.85  (define @t308 () (@list @t19 @t189))
% 0.43/0.85  (define @t309 () (@var "X" tptp.nat))
% 0.43/0.85  (define @t310 () (@list @t309))
% 0.43/0.85  (define @t311 () (_ tptp.ord_less_a @t182))
% 0.43/0.85  (define @t312 () (_ tptp.ord_less_a @t62))
% 0.43/0.85  (define @t313 () (@list @t62 @t182))
% 0.43/0.85  (define @t314 () (_ tptp.ord_less_poly_a @t185))
% 0.43/0.85  (define @t315 () (_ tptp.ord_less_poly_a @t66))
% 0.43/0.85  (define @t316 () (@list @t66 @t185))
% 0.43/0.85  (define @t317 () (_ @t76 @t226))
% 0.43/0.85  (define @t318 () (@list @t75 @t31 @t178))
% 0.43/0.85  (define @t319 () (_ @t82 @t263))
% 0.43/0.85  (define @t320 () (@var "A3" tptp.poly_a))
% 0.43/0.85  (define @t321 () (@var "B3" tptp.poly_a))
% 0.43/0.85  (define @t322 () (@var "A3" tptp.nat))
% 0.43/0.85  (define @t323 () (@var "B3" tptp.nat))
% 0.43/0.85  (define @t324 () (@list @t31 @t75 @t178))
% 0.43/0.85  (define @t325 () (@list @t81 @t80 @t259))
% 0.43/0.85  (define @t326 () (= @t37 @t229))
% 0.43/0.85  (define @t327 () (@var "Ts" tptp.list_a))
% 0.43/0.85  (define @t328 () (@var "Us" tptp.list_a))
% 0.43/0.85  (define @t329 () (_ tptp.append_a @t328))
% 0.43/0.85  (define @t330 () (@var "Us2" tptp.list_a))
% 0.43/0.85  (define @t331 () (@var "Xs1" tptp.list_a))
% 0.43/0.85  (define @t332 () (_ tptp.append_a @t331))
% 0.43/0.85  (define @t333 () (_ tptp.descar2095969287nges_a (_ @t63 @t191)))
% 0.43/0.85  (define @t334 () (or (and (_ @t40 @t62) (_ @t311 tptp.zero_zero_a)) (and (_ @t312 tptp.zero_zero_a) (_ @t40 @t182))))
% 0.43/0.85  (define @t335 () (_ tptp.descar357075861poly_a (_ @t67 (_ @t186 tptp.nil_poly_a))))
% 0.43/0.85  (define @t336 () (or (and (_ @t34 @t66) (_ @t314 tptp.zero_zero_poly_a)) (and (_ @t315 tptp.zero_zero_poly_a) (_ @t34 @t185))))
% 0.43/0.85  (define @t337 () (not @t247))
% 0.43/0.85  (define @t338 () (@var "M" tptp.nat))
% 0.43/0.85  (define @t339 () (_ (_ tptp.ord_less_nat @t338) @t246))
% 0.43/0.85  (define @t340 () (@list @t338 @t246))
% 0.43/0.85  (define @t341 () (_ tptp.ord_less_nat @t246))
% 0.43/0.85  (define @t342 () (not @t209))
% 0.43/0.85  (define @t343 () (not @t214))
% 0.43/0.85  (define @t344 () (not @t260))
% 0.43/0.85  (define @t345 () (not @t277))
% 0.43/0.85  (define @t346 () (not @t275))
% 0.43/0.85  (define @t347 () (not @t280))
% 0.43/0.85  (define @t348 () (not @t278))
% 0.43/0.85  (define @t349 () (not @t284))
% 0.43/0.85  (define @t350 () (not @t282))
% 0.43/0.85  (define @t351 () (not @t93))
% 0.43/0.85  (define @t352 () (_ tptp.ord_less_poly_a @t75))
% 0.43/0.85  (define @t353 () (_ tptp.ord_less_a @t69))
% 0.43/0.85  (define @t354 () (@var "P3" (-> tptp.list_a Bool)))
% 0.43/0.85  (define @t355 () (_ @t354 @t142))
% 0.43/0.85  (define @t356 () (_ @t151 @t145))
% 0.43/0.85  (define @t357 () (@list @t150 @t145))
% 0.43/0.85  (define @t358 () (_ @t354 tptp.nil_a))
% 0.43/0.85  (define @t359 () (@list @t354 @t142))
% 0.43/0.85  (define @t360 () (@var "A22" tptp.list_a))
% 0.43/0.85  (define @t361 () (@var "A0" (-> tptp.a tptp.a)))
% 0.43/0.85  (define @t362 () (@var "P3" (-> (-> tptp.a tptp.a) tptp.list_a tptp.list_a Bool)))
% 0.43/0.85  (define @t363 () (@var "Bs" tptp.list_a))
% 0.43/0.85  (define @t364 () (@var "As2" tptp.list_a))
% 0.43/0.85  (define @t365 () (@var "F2" (-> tptp.a tptp.a)))
% 0.43/0.85  (define @t366 () (_ @t362 @t365))
% 0.43/0.85  (define @t367 () (@var "X_1" tptp.list_a))
% 0.43/0.85  (define @t368 () (_ @t354 @t19))
% 0.43/0.85  (define @t369 () (_ @t354 @t152))
% 0.43/0.85  (define @t370 () (_ @t354 @t149))
% 0.43/0.85  (define @t371 () (@list @t150 @t149))
% 0.43/0.85  (define @t372 () (forall @t173 (_ @t354 @t172)))
% 0.43/0.85  (define @t373 () (not @t306))
% 0.43/0.85  (define @t374 () (@var "A0" (-> tptp.a tptp.a Bool)))
% 0.43/0.85  (define @t375 () (@var "P3" (-> (-> tptp.a tptp.a Bool) tptp.list_a Bool)))
% 0.43/0.85  (define @t376 () (_ (_ @t375 @t374) @t141))
% 0.43/0.85  (define @t377 () (@var "P5" (-> tptp.a tptp.a Bool)))
% 0.43/0.85  (define @t378 () (_ @t375 @t377))
% 0.43/0.85  (define @t379 () (forall (@list @t377) (_ @t378 tptp.nil_a)))
% 0.43/0.85  (define @t380 () (@list @t375 @t374 @t141))
% 0.43/0.85  (define @t381 () (= @t150 @t146))
% 0.43/0.85  (define @t382 () (@var "Xss" tptp.list_list_a))
% 0.43/0.85  (define @t383 () (@var "X" tptp.list_list_a))
% 0.43/0.85  (define @t384 () (_ @t153 @t145))
% 0.43/0.85  (define @t385 () (forall (@list @t367) (_ @t160 @t367)))
% 0.43/0.85  (define @t386 () (@var "X222" tptp.list_a))
% 0.43/0.85  (define @t387 () (@var "X212" tptp.a))
% 0.43/0.85  (define @t388 () (@var "Zs2" tptp.list_a))
% 0.43/0.85  (define @t389 () (_ @t147 @t388))
% 0.43/0.85  (define @t390 () (@var "Ys3" tptp.list_a))
% 0.43/0.85  (define @t391 () (@var "Y4" tptp.a))
% 0.43/0.85  (define @t392 () (@var "List" tptp.list_a))
% 0.43/0.85  (define @t393 () (@var "X23" tptp.list_a))
% 0.43/0.85  (define @t394 () (@var "X1" tptp.a))
% 0.43/0.85  (define @t395 () (@var "X223" tptp.list_a))
% 0.43/0.85  (define @t396 () (@var "X213" tptp.a))
% 0.43/0.85  (define @t397 () (@var "Y3" tptp.list_a))
% 0.43/0.85  (define @t398 () (_ tptp.append_a tptp.nil_a))
% 0.43/0.85  (define @t399 () (_ @t398 @t189))
% 0.43/0.85  (define @t400 () (_ @t248 @t259))
% 0.43/0.85  (define @t401 () (_ tptp.ord_less_nat @t81))
% 0.43/0.85  (define @t402 () (_ @t401 @t80))
% 0.43/0.85  (define @t403 () (_ (_ tptp.ord_less_a @t220) @t212))
% 0.43/0.85  (define @t404 () (_ @t40 @t166))
% 0.43/0.85  (define @t405 () (@list @t37 @t69 @t166))
% 0.43/0.85  (define @t406 () (_ (_ tptp.ord_less_poly_a @t222) @t217))
% 0.43/0.85  (define @t407 () (_ @t34 @t178))
% 0.43/0.85  (define @t408 () (_ @t353 @t37))
% 0.43/0.85  (define @t409 () (_ (_ tptp.ord_less_a @t166) tptp.zero_zero_a))
% 0.43/0.85  (define @t410 () (or (and @t404 @t293) (and @t409 @t408)))
% 0.43/0.85  (define @t411 () (_ (_ tptp.ord_less_a @t227) @t224))
% 0.43/0.85  (define @t412 () (_ @t352 @t31))
% 0.43/0.85  (define @t413 () (_ (_ tptp.ord_less_poly_a @t178) tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t414 () (or (and @t407 @t289) (and @t413 @t412)))
% 0.43/0.85  (define @t415 () (_ (_ tptp.ord_less_poly_a @t228) @t226))
% 0.43/0.85  (define @t416 () (@list @t69 @t37 @t166))
% 0.43/0.85  (define @t417 () (_ @t248 @t80))
% 0.43/0.85  (define @t418 () (_ @t248 @t81))
% 0.43/0.85  (define @t419 () (=> @t418 @t417))
% 0.43/0.85  (define @t420 () (_ @t262 @t81))
% 0.43/0.85  (define @t421 () (_ @t40 @t69))
% 0.43/0.85  (define @t422 () (=> @t41 @t421))
% 0.43/0.85  (define @t423 () (_ @t223 @t37))
% 0.43/0.85  (define @t424 () (_ @t34 @t75))
% 0.43/0.85  (define @t425 () (=> @t35 @t424))
% 0.43/0.85  (define @t426 () (_ @t225 @t31))
% 0.43/0.85  (define @t427 () (_ @t248 @t83))
% 0.43/0.85  (define @t428 () (_ @t40 @t101))
% 0.43/0.85  (define @t429 () (_ @t34 @t77))
% 0.43/0.85  (define @t430 () (_ @t353 tptp.zero_zero_a))
% 0.43/0.85  (define @t431 () (_ @t352 tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t432 () (_ (_ tptp.ord_less_nat @t80) tptp.zero_zero_nat))
% 0.43/0.85  (define @t433 () (_ (_ tptp.ord_less_nat @t83) tptp.zero_zero_nat))
% 0.43/0.85  (define @t434 () (_ (_ tptp.ord_less_a @t101) tptp.zero_zero_a))
% 0.43/0.85  (define @t435 () (_ (_ tptp.ord_less_poly_a @t77) tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t436 () (_ @t401 tptp.zero_zero_nat))
% 0.43/0.85  (define @t437 () (@var "K" tptp.nat))
% 0.43/0.85  (define @t438 () (_ @t248 @t437))
% 0.43/0.85  (define @t439 () (and @t438 @t339))
% 0.43/0.85  (define @t440 () (_ tptp.times_times_nat @t437))
% 0.43/0.85  (define @t441 () (_ @t440 @t246))
% 0.43/0.85  (define @t442 () (_ @t440 @t338))
% 0.43/0.85  (define @t443 () (_ (_ tptp.ord_less_nat @t442) @t441))
% 0.43/0.85  (define @t444 () (@list @t437 @t338 @t246))
% 0.43/0.85  (define @t445 () (_ tptp.times_times_nat @t338))
% 0.43/0.85  (define @t446 () (_ @t445 @t246))
% 0.43/0.85  (define @t447 () (_ tptp.times_times_nat @t246))
% 0.43/0.85  (define @t448 () (_ @t447 @t437))
% 0.43/0.85  (define @t449 () (_ @t445 @t437))
% 0.43/0.85  (define @t450 () (@list @t338 @t437 @t246))
% 0.43/0.85  (define @t451 () (= @t437 tptp.zero_zero_nat))
% 0.43/0.85  (define @t452 () (= @t338 @t246))
% 0.43/0.85  (define @t453 () (or @t452 @t451))
% 0.43/0.85  (define @t454 () (= @t338 tptp.zero_zero_nat))
% 0.43/0.85  (define @t455 () (= @t442 @t441))
% 0.43/0.85  (define @t456 () (= @t246 tptp.one_one_nat))
% 0.43/0.85  (define @t457 () (and (= @t338 tptp.one_one_nat) @t456))
% 0.43/0.85  (define @t458 () (@var "Y3" tptp.nat))
% 0.43/0.85  (define @t459 () (@var "P3" (-> tptp.nat Bool)))
% 0.43/0.85  (define @t460 () (_ @t459 @t246))
% 0.43/0.85  (define @t461 () (@var "M2" tptp.nat))
% 0.43/0.85  (define @t462 () (_ @t459 @t461))
% 0.43/0.85  (define @t463 () (@var "N2" tptp.nat))
% 0.43/0.85  (define @t464 () (_ (_ tptp.ord_less_nat @t461) @t463))
% 0.43/0.85  (define @t465 () (@list @t461))
% 0.43/0.85  (define @t466 () (_ @t459 @t463))
% 0.43/0.85  (define @t467 () (=> (not @t466) (exists @t465 (and @t464 (not @t462)))))
% 0.43/0.85  (define @t468 () (@list @t463))
% 0.43/0.85  (define @t469 () (@list @t459 @t246))
% 0.43/0.85  (define @t470 () (@var "T" tptp.nat))
% 0.43/0.85  (define @t471 () (@var "S" tptp.nat))
% 0.43/0.85  (define @t472 () (not @t452))
% 0.43/0.85  (define @t473 () (_ @t341 @t338))
% 0.43/0.85  (define @t474 () (@var "J" tptp.nat))
% 0.43/0.85  (define @t475 () (@var "I" tptp.nat))
% 0.43/0.85  (define @t476 () (_ (_ tptp.ord_less_nat @t475) @t474))
% 0.43/0.85  (define @t477 () (@list @t475 @t474 @t437))
% 0.43/0.85  (define @t478 () (_ tptp.descar2095969287nges_a @t28))
% 0.43/0.85  (define @t479 () (= (_ tptp.descar2095969287nges_a tptp.ys) @t478))
% 0.43/0.85  (define @t480 () (not @t479))
% 0.43/0.85  (define @t481 () (@var "F" tptp.poly_a))
% 0.43/0.85  (define @t482 () (lambda (@list @t481) (_ tptp.descar2095969287nges_a (_ tptp.coeffs_a @t481))))
% 0.43/0.85  (define @t483 () (lambda (@list @t2) (_ tptp.null_poly_a @t3)))
% 0.43/0.85  (define @t484 () (lambda @t123 (_ tptp.null_a @t8)))
% 0.43/0.85  (define @t485 () (tptp.uminus_uminus_a tptp.one_one_a))
% 0.43/0.85  (define @t486 () (tptp.pCons_a @t485 tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t487 () (tptp.pCons_a tptp.one_one_a @t486))
% 0.43/0.85  (define @t488 () (tptp.times_times_poly_a @t487 tptp.g))
% 0.43/0.85  (define @t489 () (tptp.coeffs_a @t488))
% 0.43/0.85  (define @t490 () (tptp.descar1375166517sums_a @t489))
% 0.43/0.85  (define @t491 () (tptp.coeffs_a tptp.zero_zero_poly_a))
% 0.43/0.85  (define @t492 () (tptp.cons_a tptp.zero_zero_a @t491))
% 0.43/0.85  (define @t493 () (tptp.coeffs_a tptp.g))
% 0.43/0.85  (define @t494 () (tptp.append_a @t493 @t492))
% 0.43/0.85  (define @t495 () (_ @t26 @t104))
% 0.43/0.85  (define @t496 () (tptp.cons_a tptp.zero_zero_a @t104))
% 0.43/0.85  (define @t497 () (_ @t29 @t495))
% 0.43/0.85  (define @t498 () (_ tptp.descar1375166517sums_a @t52))
% 0.43/0.85  (define @t499 () (tptp.descar2095969287nges_a @t493))
% 0.43/0.85  (define @t500 () (tptp.descar2095969287nges_a @t490))
% 0.43/0.85  (define @t501 () (_ tptp.descar2095969287nges_a @t498))
% 0.43/0.85  (define @t502 () (= @t478 @t501))
% 0.43/0.85  (define @t503 () (tptp.coeffs_a @t16))
% 0.43/0.85  (define @t504 () (tptp.poly_a2 @t503))
% 0.43/0.85  (define @t505 () (= @t16 @t44))
% 0.43/0.85  (define @t506 () (tptp.append_a @t111 @t496))
% 0.43/0.85  (define @t507 () (tptp.poly_a2 @t506))
% 0.43/0.85  (define @t508 () (tptp.poly_a2 @t111))
% 0.43/0.85  (define @t509 () (= @t508 @t507))
% 0.43/0.85  (define @t510 () (tptp.cons_a tptp.zero_zero_a tptp.nil_a))
% 0.43/0.85  (define @t511 () (tptp.append_a @t111 @t510))
% 0.43/0.85  (define @t512 () (tptp.poly_a2 @t511))
% 0.43/0.85  (define @t513 () (= @t512 @t508))
% 0.43/0.85  (define @t514 () (tptp.poly_a2 @t19))
% 0.43/0.85  (define @t515 () (tptp.descar2095969287nges_a @t19))
% 0.43/0.85  (define @t516 () (= @t515 (tptp.descar2095969287nges_a (tptp.coeffs_a @t514))))
% 0.43/0.85  (define @t517 () (not (= @t514 @t514)))
% 0.43/0.85  (define @t518 () (or @t517 @t516))
% 0.43/0.85  (define @t519 () (tptp.descar2095969287nges_a @t503))
% 0.43/0.85  (define @t520 () (= @t515 @t519))
% 0.43/0.85  (define @t521 () (not (= @t16 @t514)))
% 0.43/0.85  (define @t522 () (or @t521 @t521 @t520))
% 0.43/0.85  (define @t523 () (or @t521 @t520))
% 0.43/0.85  (define @t524 () (forall @t45 @t523))
% 0.43/0.85  (define @t525 () (forall @t58 @t524))
% 0.43/0.85  (define @t526 () (= @t16 @t22))
% 0.43/0.85  (define @t527 () (not @t526))
% 0.43/0.85  (define @t528 () (or @t527 @t21))
% 0.43/0.85  (define @t529 () (tptp.poly_a2 @t490))
% 0.43/0.85  (define @t530 () (tptp.coeffs_a @t529))
% 0.43/0.85  (define @t531 () (tptp.descar2095969287nges_a @t530))
% 0.43/0.85  (define @t532 () (= @t500 @t531))
% 0.43/0.85  (define @t533 () (not @t532))
% 0.43/0.85  (define @t534 () (tptp.poly_a2 @t493))
% 0.43/0.85  (define @t535 () (= @t534 (tptp.poly_a2 @t494)))
% 0.43/0.85  (define @t536 () (not @t535))
% 0.43/0.85  (define @t537 () (= tptp.g @t534))
% 0.43/0.85  (define @t538 () (not @t537))
% 0.43/0.85  (define @t539 () (= @t500 @t499))
% 0.43/0.85  (define @t540 () (= @t494 @t490))
% 0.43/0.85  (define @t541 () (not @t540))
% 0.43/0.85  (define @t542 () (not @t539))
% 0.43/0.85  (define @t543 () (and @t532 @t533))
% 0.43/0.85  (assume @p1 (not (= tptp.g tptp.zero_zero_poly_a)))
% 0.43/0.85  (assume @p2 (= (lambda (@list @t5 @t4) (= @t5 @t4)) (lambda (@list @t2 @t1) (= @t3 (_ tptp.coeffs_poly_a @t1)))))
% 0.43/0.85  (assume @p3 (= (lambda (@list @t10 @t9) (= @t10 @t9)) (lambda (@list @t7 @t6) (= @t8 (_ tptp.coeffs_a @t6)))))
% 0.43/0.85  (assume @p4 (= tptp.ys (_ tptp.descar1375166517sums_a tptp.xs)))
% 0.43/0.85  (assume @p5 (forall (@list @t14 @t11) (=> (= (_ tptp.poly_poly_a2 @t14) @t11) (= @t15 @t13))))
% 0.43/0.85  (assume @p6 @t25)
% 0.43/0.85  (assume @p7 @t30)
% 0.43/0.85  (assume @p8 (forall @t36 (=> @t35 (= (_ tptp.descar357075861poly_a (_ tptp.coeffs_poly_a @t33)) @t13))))
% 0.43/0.85  (assume @p9 (forall @t42 (=> @t41 (= (_ tptp.descar2095969287nges_a (_ tptp.coeffs_a @t39)) @t18))))
% 0.43/0.85  (assume @p10 (forall @t43 (= (_ tptp.poly_poly_a2 @t12) @t11)))
% 0.43/0.85  (assume @p11 @t46)
% 0.43/0.85  (assume @p12 (= (_ tptp.descar357075861poly_a tptp.nil_poly_a) tptp.zero_zero_nat))
% 0.43/0.85  (assume @p13 (= (_ tptp.descar2095969287nges_a tptp.nil_a) tptp.zero_zero_nat))
% 0.43/0.85  (assume @p14 (= tptp.xs @t52))
% 0.43/0.85  (assume @p15 (forall @t42 (=> @t41 (= (_ tptp.descar2095969287nges_a (_ tptp.coeffs_a @t54)) @t18))))
% 0.43/0.85  (assume @p16 (forall @t36 (=> @t35 (= (_ tptp.descar357075861poly_a (_ tptp.coeffs_poly_a @t56)) @t13))))
% 0.43/0.85  (assume @p17 (forall @t58 (= (_ tptp.descar2095969287nges_a @t57) @t20)))
% 0.43/0.85  (assume @p18 (forall @t61 (= (_ tptp.descar357075861poly_a @t60) @t15)))
% 0.43/0.85  (assume @p19 (forall @t65 (= (_ tptp.descar2095969287nges_a (_ @t63 @t57)) (_ tptp.descar2095969287nges_a @t64))))
% 0.43/0.85  (assume @p20 (forall (@list @t66 @t14) (= (_ tptp.descar357075861poly_a (_ @t67 @t60)) (_ tptp.descar357075861poly_a (_ @t67 @t14)))))
% 0.43/0.85  (assume @p21 (forall (@list @t37 @t16 @t69 @t68) (= (= @t73 (_ @t71 @t68)) (and @t70 (= @t16 @t68)))))
% 0.43/0.85  (assume @p22 (forall @t42 (= (_ tptp.uminus_uminus_poly_a @t73) (_ (_ tptp.pCons_a @t74) (_ tptp.uminus_uminus_poly_a @t16)))))
% 0.43/0.85  (assume @p23 (forall @t78 (= (_ @t55 (_ (_ tptp.smult_poly_a @t75) @t11)) (_ (_ tptp.smult_poly_a @t77) @t11))))
% 0.43/0.85  (assume @p24 (forall @t85 (= (_ @t84 (_ (_ tptp.smult_nat @t80) @t79)) (_ (_ tptp.smult_nat @t83) @t79))))
% 0.43/0.85  (assume @p25 (forall @t45 (= (_ (_ tptp.smult_a tptp.one_one_a) @t16) @t16)))
% 0.43/0.85  (assume @p26 (forall @t86 (= (_ (_ tptp.smult_nat tptp.one_one_nat) @t79) @t79)))
% 0.43/0.85  (assume @p27 (forall @t42 (= (_ (_ tptp.smult_a @t74) @t16) (_ tptp.uminus_uminus_poly_a @t54))))
% 0.43/0.85  (assume @p28 (forall @t87 (= (_ @t53 tptp.zero_zero_poly_a) tptp.zero_zero_poly_a)))
% 0.43/0.85  (assume @p29 (forall (@list @t37 @t16 @t68) (= (_ (_ tptp.times_times_poly_a @t54) @t68) @t89)))
% 0.43/0.85  (assume @p30 (forall (@list @t16 @t37 @t68) (= (_ @t88 (_ @t53 @t68)) @t89)))
% 0.43/0.85  (assume @p31 (= (_ (_ tptp.pCons_poly_a tptp.zero_zero_poly_a) tptp.zero_z2096148049poly_a) tptp.zero_z2096148049poly_a))
% 0.43/0.85  (assume @p32 (= (_ (_ tptp.pCons_a tptp.zero_zero_a) tptp.zero_zero_poly_a) tptp.zero_zero_poly_a))
% 0.43/0.85  (assume @p33 (= (_ (_ tptp.pCons_nat tptp.zero_zero_nat) tptp.zero_zero_poly_nat) tptp.zero_zero_poly_nat))
% 0.43/0.85  (assume @p34 (forall @t36 (= (= (_ (_ tptp.pCons_poly_a @t31) @t11) tptp.zero_z2096148049poly_a) (and @t91 @t90))))
% 0.43/0.85  (assume @p35 (forall @t94 (= (= (_ (_ tptp.pCons_nat @t81) @t79) tptp.zero_zero_poly_nat) (and @t93 @t92))))
% 0.43/0.85  (assume @p36 (forall @t42 (= (= @t73 tptp.zero_zero_poly_a) (and @t96 @t95))))
% 0.43/0.85  (assume @p37 (= @t97 tptp.one_one_poly_nat))
% 0.43/0.85  (assume @p38 (= @t98 tptp.one_one_poly_a))
% 0.43/0.85  (assume @p39 (= tptp.one_one_poly_nat @t97))
% 0.43/0.85  (assume @p40 (= tptp.one_one_poly_a @t98))
% 0.43/0.85  (assume @p41 (forall @t43 (= (_ (_ tptp.smult_poly_a tptp.zero_zero_poly_a) @t11) tptp.zero_z2096148049poly_a)))
% 0.43/0.85  (assume @p42 (forall @t45 (= (_ (_ tptp.smult_a tptp.zero_zero_a) @t16) tptp.zero_zero_poly_a)))
% 0.43/0.85  (assume @p43 (forall @t86 (= (_ (_ tptp.smult_nat tptp.zero_zero_nat) @t79) tptp.zero_zero_poly_nat)))
% 0.43/0.85  (assume @p44 (forall @t36 (= (= @t56 tptp.zero_z2096148049poly_a) (or @t91 @t90))))
% 0.43/0.85  (assume @p45 (forall @t94 (= (= @t99 tptp.zero_zero_poly_nat) (or @t93 @t92))))
% 0.43/0.85  (assume @p46 (forall @t42 (= (= @t54 tptp.zero_zero_poly_a) (or @t96 @t95))))
% 0.43/0.85  (assume @p47 (forall (@list @t37 @t69 @t16) (= (_ @t53 (_ @t71 @t16)) (_ (_ tptp.pCons_a @t101) @t54))))
% 0.43/0.85  (assume @p48 (forall @t78 (= (_ @t55 (_ (_ tptp.pCons_poly_a @t75) @t11)) (_ (_ tptp.pCons_poly_a @t77) @t56))))
% 0.43/0.85  (assume @p49 (forall @t85 (= (_ @t84 (_ (_ tptp.pCons_nat @t80) @t79)) (_ (_ tptp.pCons_nat @t83) @t99))))
% 0.43/0.85  (assume @p50 (forall @t43 (= @t102 @t90)))
% 0.43/0.85  (assume @p51 (forall @t45 (= @t103 @t95)))
% 0.43/0.85  (assume @p52 (= (_ tptp.coeffs_poly_a tptp.zero_z2096148049poly_a) tptp.nil_poly_a))
% 0.43/0.85  (assume @p53 (= @t104 tptp.nil_a))
% 0.43/0.85  (assume @p54 (forall @t61 (= (_ tptp.descar282223555poly_a @t60) (_ @t59 (_ tptp.descar282223555poly_a @t14)))))
% 0.43/0.85  (assume @p55 (forall (@list @t105) (= (_ tptp.descar226543321ms_nat (_ @t106 @t105)) (_ @t106 (_ tptp.descar226543321ms_nat @t105)))))
% 0.43/0.85  (assume @p56 (forall @t58 (= (_ tptp.descar1375166517sums_a @t57) (_ @t26 (_ tptp.descar1375166517sums_a @t19)))))
% 0.43/0.85  (assume @p57 (= (_ tptp.coeffs_poly_a tptp.one_one_poly_poly_a) (_ (_ tptp.cons_poly_a tptp.one_one_poly_a) tptp.nil_poly_a)))
% 0.43/0.85  (assume @p58 (= (_ tptp.coeffs_a tptp.one_one_poly_a) (_ (_ tptp.cons_a tptp.one_one_a) tptp.nil_a)))
% 0.43/0.85  (assume @p59 (= (_ tptp.coeffs_nat tptp.one_one_poly_nat) (_ (_ tptp.cons_nat tptp.one_one_nat) tptp.nil_nat)))
% 0.43/0.85  (assume @p60 (forall @t108 (= (_ tptp.descar2095969287nges_a @t107) tptp.zero_zero_nat)))
% 0.43/0.85  (assume @p61 (forall @t109 (= (_ tptp.descar357075861poly_a (_ @t67 tptp.nil_poly_a)) tptp.zero_zero_nat)))
% 0.43/0.85  (assume @p62 (= (_ tptp.descar2095969287nges_a tptp.xs) (_ tptp.v @t51)))
% 0.43/0.85  (assume @p63 (forall (@list @t110) (= (_ tptp.poly_poly_a2 (_ (_ tptp.append_poly_a @t110) (_ @t59 tptp.nil_poly_a))) (_ tptp.poly_poly_a2 @t110))))
% 0.43/0.85  (assume @p64 @t118)
% 0.43/0.85  (assume @p65 (forall (@list @t119) (= (_ tptp.poly_nat2 (_ (_ tptp.append_nat @t119) (_ @t106 tptp.nil_nat))) (_ tptp.poly_nat2 @t119))))
% 0.43/0.85  (assume @p66 (forall (@list @t37 @t111) (= (_ tptp.poly_a2 (_ (_ tptp.cons_a @t37) @t111)) (_ @t72 @t112))))
% 0.43/0.85  (assume @p67 (= (_ tptp.poly_a2 tptp.nil_a) tptp.zero_zero_poly_a))
% 0.43/0.85  (assume @p68 (forall @t108 (= (_ tptp.descar1375166517sums_a @t107) @t107)))
% 0.43/0.85  (assume @p69 (= (_ tptp.descar1375166517sums_a tptp.nil_a) tptp.nil_a))
% 0.43/0.85  (assume @p70 (forall @t45 (not (forall (@list @t121 @t120) (not (= @t16 (_ @t122 @t120)))))))
% 0.43/0.85  (assume @p71 (= tptp.is_zero_a (lambda @t123 (= @t7 tptp.zero_zero_poly_a))))
% 0.43/0.85  (assume @p72 (forall (@list @t124 @t11) (=> (_ @t124 tptp.zero_z2096148049poly_a) (=> (forall (@list @t126 @t125) (=> (or (not (= @t126 tptp.zero_zero_poly_a)) (not (= @t125 tptp.zero_z2096148049poly_a))) (=> (_ @t124 @t125) (_ @t124 (_ (_ tptp.pCons_poly_a @t126) @t125))))) (_ @t124 @t11)))))
% 0.43/0.85  (assume @p73 (forall (@list @t127 @t79) (=> (_ @t127 tptp.zero_zero_poly_nat) (=> (forall (@list @t129 @t128) (=> (or (not (= @t129 tptp.zero_zero_nat)) (not (= @t128 tptp.zero_zero_poly_nat))) (=> (_ @t127 @t128) (_ @t127 (_ (_ tptp.pCons_nat @t129) @t128))))) (_ @t127 @t79)))))
% 0.43/0.85  (assume @p74 (forall (@list @t130 @t16) (=> (_ @t130 tptp.zero_zero_poly_a) (=> (forall @t136 (=> (or (not (= @t121 tptp.zero_zero_a)) @t135) (=> @t134 @t133))) (_ @t130 @t16)))))
% 0.43/0.85  (assume @p75 (forall @t109 (not (forall @t136 (not (= @t66 @t132))))))
% 0.43/0.85  (assume @p76 (forall (@list @t137 @t16 @t68) (=> (_ (_ @t137 tptp.zero_zero_poly_a) tptp.zero_zero_poly_a) (=> (forall (@list @t121 @t131 @t138 @t120) (=> (_ (_ @t137 @t131) @t120) (_ (_ @t137 @t132) (_ (_ tptp.pCons_a @t138) @t120)))) (_ (_ @t137 @t16) @t68)))))
% 0.43/0.85  (assume @p77 (forall (@list @t130 @t139) (=> (forall @t136 (=> (=> @t135 @t134) @t133)) (_ @t130 @t139))))
% 0.43/0.85  (assume @p78 (forall (@list @t68) (= (_ @t140 @t68) tptp.zero_zero_poly_a)))
% 0.43/0.85  (assume @p79 (forall @t45 (= (_ @t88 tptp.zero_zero_poly_a) tptp.zero_zero_poly_a)))
% 0.43/0.85  (assume @p80 (forall @t162 (=> @t161 (=> (forall (@list @t159 @t158) (_ @t160 (_ (_ tptp.cons_a @t159) @t158))) (=> @t157 @t144)))))
% 0.43/0.85  (assume @p81 (forall @t43 (=> @t163 (not @t102))))
% 0.43/0.85  (assume @p82 (forall @t45 (=> @t164 (not @t103))))
% 0.43/0.85  (assume @p83 (forall @t162 (=> @t157 (=> @t161 (=> @t165 @t144)))))
% 0.43/0.85  (assume @p84 (forall (@list @t166 @t16 @t37) (=> (= (_ @t167 @t16) @t73) @t95)))
% 0.43/0.85  (assume @p85 (forall @t176 (=> @t175 (=> (forall @t173 (not (= @t170 @t172))) (not (forall @t171 (not (= @t170 @t169))))))))
% 0.43/0.85  (assume @p86 (forall (@list @t37 @t166 @t16) (= (_ @t38 (_ @t177 @t16)) (_ @t177 (_ @t53 @t39)))))
% 0.43/0.85  (assume @p87 (forall (@list @t31 @t178 @t11) (= (_ @t32 (_ @t179 @t11)) (_ @t179 (_ @t55 @t33)))))
% 0.43/0.85  (assume @p88 (forall @t42 (=> @t180 (=> @t164 (not (= @t39 tptp.zero_zero_poly_a))))))
% 0.43/0.85  (assume @p89 (forall @t36 (=> @t181 (=> @t163 (not (= @t33 tptp.zero_z2096148049poly_a))))))
% 0.43/0.85  (assume @p90 (forall (@list @t62 @t182 @t19) (=> (_ @t40 (_ (_ tptp.times_times_a @t62) @t182)) (= (_ tptp.descar2095969287nges_a (_ @t63 @t184)) (_ tptp.descar2095969287nges_a @t184)))))
% 0.43/0.85  (assume @p91 (forall (@list @t66 @t185 @t14) (=> (_ @t34 (_ (_ tptp.times_times_poly_a @t66) @t185)) (= (_ tptp.descar357075861poly_a (_ @t67 @t187)) (_ tptp.descar357075861poly_a @t187)))))
% 0.43/0.85  (assume @p92 (forall (@list @t19 @t62 @t189 @t182) (= (= (_ @t193 @t107) (_ @t192 @t191)) (and @t190 @t188))))
% 0.43/0.85  (assume @p93 (forall @t197 (= (_ (_ tptp.times_times_poly_a @t196) @t194) @t195)))
% 0.43/0.85  (assume @p94 (forall @t200 (= (_ (_ tptp.times_times_a @t47) @t198) @t199)))
% 0.43/0.85  (assume @p95 (forall @t197 (= (_ (_ tptp.times_times_poly_a @t194) @t196) @t195)))
% 0.43/0.85  (assume @p96 (forall @t200 (= (_ (_ tptp.times_times_a @t198) @t47) @t199)))
% 0.43/0.85  (assume @p97 (forall @t204 (= (_ @t201 @t203) @t202)))
% 0.43/0.85  (assume @p98 (forall @t87 (= (_ @t205 @t74) @t206)))
% 0.43/0.85  (assume @p99 (forall @t204 (= (_ @t207 @t31) @t35)))
% 0.43/0.85  (assume @p100 (forall @t87 (= (_ @t208 @t37) @t41)))
% 0.43/0.85  (assume @p101 (forall @t204 (= (_ @t34 @t203) @t202)))
% 0.43/0.85  (assume @p102 (forall @t87 (= (_ @t40 @t74) @t206)))
% 0.43/0.85  (assume @p103 (forall @t204 (= (_ @t207 tptp.zero_zero_poly_a) @t35)))
% 0.43/0.85  (assume @p104 (forall @t87 (= (_ @t208 tptp.zero_zero_a) @t41)))
% 0.43/0.85  (assume @p105 (forall @t213 (= (= @t166 @t212) @t210)))
% 0.43/0.85  (assume @p106 (forall @t218 (= (= @t178 @t217) @t215)))
% 0.43/0.85  (assume @p107 (forall (@list @t166 @t37) (= (= @t220 @t166) @t219)))
% 0.43/0.85  (assume @p108 (forall (@list @t178 @t31) (= (= @t222 @t178) @t221)))
% 0.43/0.85  (assume @p109 (forall @t213 (= (= @t166 @t224) @t210)))
% 0.43/0.85  (assume @p110 (forall @t218 (= (= @t178 @t226) @t215)))
% 0.43/0.85  (assume @p111 (forall (@list @t37 @t166) (= (= @t227 @t166) @t219)))
% 0.43/0.85  (assume @p112 (forall (@list @t31 @t178) (= (= @t228 @t178) @t221)))
% 0.43/0.85  (assume @p113 (forall @t230 (= (= @t74 @t229) @t70)))
% 0.43/0.85  (assume @p114 (forall @t87 (= (_ tptp.uminus_uminus_a @t74) @t37)))
% 0.43/0.85  (assume @p115 (forall (@list @t234 @t232 @t233 @t231) (= (= @t235 (_ (_ tptp.cons_a @t233) @t231)) (and (= @t234 @t233) (= @t232 @t231)))))
% 0.43/0.85  (assume @p116 (forall @t239 (= (= @t238 (_ @t193 @t236)) @t237)))
% 0.43/0.85  (assume @p117 (forall (@list @t189 @t19 @t236) (= (= (_ @t192 @t19) (_ @t240 @t19)) @t237)))
% 0.43/0.85  (assume @p118 (forall @t239 (= (_ (_ tptp.append_a @t238) @t236) (_ @t193 @t241))))
% 0.43/0.85  (assume @p119 (forall (@list @t244 @t243 @t242) (= (_ (_ tptp.append_a (_ @t245 @t243)) @t242) (_ @t245 (_ (_ tptp.append_a @t243) @t242)))))
% 0.43/0.85  (assume @p120 (forall @t250 (= (not @t249) @t247)))
% 0.43/0.85  (assume @p121 (forall @t253 (= @t252 @t251)))
% 0.43/0.85  (assume @p122 (forall @t257 (= @t256 @t255)))
% 0.43/0.85  (assume @p123 (forall (@list @t81 @t259 @t80) (= @t265 @t261)))
% 0.43/0.85  (assume @p124 (forall @t267 (= @t266 @t251)))
% 0.43/0.85  (assume @p125 (forall @t269 (= @t268 @t255)))
% 0.43/0.85  (assume @p126 (forall @t274 (= @t273 @t261)))
% 0.43/0.85  (assume @p127 (forall @t230 (= @t277 @t276)))
% 0.43/0.85  (assume @p128 (forall @t281 (= @t280 @t279)))
% 0.43/0.85  (assume @p129 (forall @t285 (= @t284 @t283)))
% 0.43/0.85  (assume @p130 (forall @t87 (= (_ @t100 tptp.zero_zero_a) tptp.zero_zero_a)))
% 0.43/0.85  (assume @p131 (forall @t204 (= (_ @t76 tptp.zero_zero_poly_a) tptp.zero_zero_poly_a)))
% 0.43/0.85  (assume @p132 (forall @t286 (= (_ @t82 tptp.zero_zero_nat) tptp.zero_zero_nat)))
% 0.43/0.85  (assume @p133 (forall @t87 (= (_ (_ tptp.times_times_a tptp.zero_zero_a) @t37) tptp.zero_zero_a)))
% 0.43/0.85  (assume @p134 (forall @t204 (= (_ @t140 @t31) tptp.zero_zero_poly_a)))
% 0.43/0.85  (assume @p135 (forall @t286 (= (_ @t287 @t81) tptp.zero_zero_nat)))
% 0.43/0.85  (assume @p136 (forall @t204 (= (= @t203 @t31) @t91)))
% 0.43/0.85  (assume @p137 (forall @t87 (= (= @t74 @t37) @t96)))
% 0.43/0.85  (assume @p138 (forall @t204 (= (= @t31 @t203) @t91)))
% 0.43/0.85  (assume @p139 (forall @t87 (= (= @t37 @t74) @t96)))
% 0.43/0.85  (assume @p140 (forall @t204 (= (= @t203 tptp.zero_zero_poly_a) @t91)))
% 0.43/0.85  (assume @p141 (forall @t87 (= (= @t74 tptp.zero_zero_a) @t96)))
% 0.43/0.85  (assume @p142 (forall @t204 (= (= tptp.zero_zero_poly_a @t203) (= tptp.zero_zero_poly_a @t31))))
% 0.43/0.85  (assume @p143 (forall @t87 (= (= tptp.zero_zero_a @t74) (= tptp.zero_zero_a @t37))))
% 0.43/0.85  (assume @p144 (= (_ tptp.uminus_uminus_poly_a tptp.zero_zero_poly_a) tptp.zero_zero_poly_a))
% 0.43/0.85  (assume @p145 (= (_ tptp.uminus_uminus_a tptp.zero_zero_a) tptp.zero_zero_a))
% 0.43/0.85  (assume @p146 (forall @t87 (= (_ @t100 tptp.one_one_a) @t37)))
% 0.43/0.85  (assume @p147 (forall @t204 (= (_ @t76 tptp.one_one_poly_a) @t31)))
% 0.43/0.85  (assume @p148 (forall @t286 (= (_ @t82 tptp.one_one_nat) @t81)))
% 0.43/0.85  (assume @p149 (forall @t87 (= (_ (_ tptp.times_times_a tptp.one_one_a) @t37) @t37)))
% 0.43/0.85  (assume @p150 (forall @t204 (= (_ (_ tptp.times_times_poly_a tptp.one_one_poly_a) @t31) @t31)))
% 0.43/0.85  (assume @p151 (forall @t286 (= (_ @t288 @t81) @t81)))
% 0.43/0.85  (assume @p152 (forall @t292 (= (_ @t291 @t203) @t289)))
% 0.43/0.85  (assume @p153 (forall @t295 (= (_ @t294 @t74) @t293)))
% 0.43/0.85  (assume @p154 (forall @t281 (= @t297 @t296)))
% 0.43/0.85  (assume @p155 (forall @t230 (= @t299 @t298)))
% 0.43/0.85  (assume @p156 (forall @t281 (= (_ @t300 @t290) @t77)))
% 0.43/0.85  (assume @p157 (forall @t230 (= (_ @t301 @t229) @t101)))
% 0.43/0.85  (assume @p158 (forall @t281 (= @t302 @t296)))
% 0.43/0.85  (assume @p159 (forall @t230 (= @t303 @t298)))
% 0.43/0.85  (assume @p160 (forall @t304 (= (_ @t245 tptp.nil_a) @t244)))
% 0.43/0.85  (assume @p161 (forall @t308 (= (= @t238 tptp.nil_a) @t307)))
% 0.43/0.85  (assume @p162 (forall @t308 (= (= tptp.nil_a @t238) @t307)))
% 0.43/0.85  (assume @p163 (forall (@list @t189 @t19) (= (= @t189 @t238) @t306)))
% 0.43/0.85  (assume @p164 (forall @t308 (= (= @t238 @t189) @t306)))
% 0.43/0.85  (assume @p165 (forall @t308 (= (= @t19 @t238) @t305)))
% 0.43/0.85  (assume @p166 (forall @t308 (= (= @t238 @t19) @t305)))
% 0.43/0.85  (assume @p167 (forall @t58 (= (_ @t193 tptp.nil_a) @t19)))
% 0.43/0.85  (assume @p168 (forall (@list @t166) (= (_ @t167 tptp.one_one_poly_a) (_ @t177 tptp.zero_zero_poly_a))))
% 0.43/0.85  (assume @p169 (forall @t109 (= (= tptp.zero_zero_poly_a @t66) (= @t66 tptp.zero_zero_poly_a))))
% 0.43/0.85  (assume @p170 (forall @t108 (= (= tptp.zero_zero_a @t62) (= @t62 tptp.zero_zero_a))))
% 0.43/0.85  (assume @p171 (forall @t310 (= (= tptp.zero_zero_nat @t309) (= @t309 tptp.zero_zero_nat))))
% 0.43/0.85  (assume @p172 (forall @t313 (=> (not @t188) (=> (not (_ @t312 @t182)) (_ @t311 @t62)))))
% 0.43/0.85  (assume @p173 (forall @t316 (=> (not (= @t66 @t185)) (=> (not (_ @t315 @t185)) (_ @t314 @t66)))))
% 0.43/0.85  (assume @p174 (forall @t318 (= (_ @t225 @t228) @t317)))
% 0.43/0.85  (assume @p175 (forall (@list @t80 @t81 @t259) (= (_ @t262 @t264) @t319)))
% 0.43/0.85  (assume @p176 (= tptp.times_times_poly_a (lambda (@list @t320 @t321) (_ (_ tptp.times_times_poly_a @t321) @t320))))
% 0.43/0.85  (assume @p177 (= tptp.times_times_nat (lambda (@list @t322 @t323) (_ (_ tptp.times_times_nat @t323) @t322))))
% 0.43/0.85  (assume @p178 (forall @t324 (= (_ (_ tptp.times_times_poly_a @t77) @t178) @t317)))
% 0.43/0.85  (assume @p179 (forall @t325 (= (_ (_ tptp.times_times_nat @t83) @t259) @t319)))
% 0.43/0.85  (assume @p180 (forall @t108 (= (= tptp.one_one_a @t62) (= @t62 tptp.one_one_a))))
% 0.43/0.85  (assume @p181 (forall @t310 (= (= tptp.one_one_nat @t309) (= @t309 tptp.one_one_nat))))
% 0.43/0.85  (assume @p182 (forall @t230 (= (= @t74 @t69) (= @t229 @t37))))
% 0.43/0.85  (assume @p183 (forall @t230 (= @t326 (= @t69 @t74))))
% 0.43/0.85  (assume @p184 (forall @t65 (not (= @t64 @t19))))
% 0.43/0.85  (assume @p185 (forall (@list @t19 @t189 @t236 @t327) (= (= @t238 (_ @t240 @t327)) (exists (@list @t328) (or (and (= @t19 (_ @t240 @t328)) (= (_ @t329 @t189) @t327)) (and (= (_ @t193 @t328) @t236) (= @t189 (_ @t329 @t327))))))))
% 0.43/0.85  (assume @p186 (forall (@list @t19 @t331 @t236 @t189 @t330) (=> (= (_ @t193 @t331) @t236) (=> (= @t189 (_ @t332 @t330)) (= @t238 (_ @t240 @t330))))))
% 0.43/0.85  (assume @p187 (forall @t313 (and (=> @t334 (= @t333 tptp.one_one_nat)) (=> (not @t334) (= @t333 tptp.zero_zero_nat)))))
% 0.43/0.85  (assume @p188 (forall @t316 (and (=> @t336 (= @t335 tptp.one_one_nat)) (=> (not @t336) (= @t335 tptp.zero_zero_nat)))))
% 0.43/0.85  (assume @p189 (forall @t250 (= @t249 @t337)))
% 0.43/0.85  (assume @p190 (forall @t340 (=> @t339 @t337)))
% 0.43/0.85  (assume @p191 (forall @t250 (not (_ @t341 tptp.zero_zero_nat))))
% 0.43/0.85  (assume @p192 (forall @t250 (=> @t337 @t249)))
% 0.43/0.85  (assume @p193 (not (_ @t248 tptp.zero_zero_nat)))
% 0.43/0.85  (assume @p194 (not (_ @t40 tptp.zero_zero_a)))
% 0.43/0.85  (assume @p195 (not (_ @t34 tptp.zero_zero_poly_a)))
% 0.43/0.85  (assume @p196 (forall @t267 (=> @t342 (= @t252 @t70))))
% 0.43/0.85  (assume @p197 (forall @t269 (=> @t343 (= @t256 @t254))))
% 0.43/0.85  (assume @p198 (forall @t274 (=> @t344 (= @t265 @t258))))
% 0.43/0.85  (assume @p199 (forall @t267 (=> @t342 (= @t266 @t70))))
% 0.43/0.85  (assume @p200 (forall @t269 (=> @t343 (= @t268 @t254))))
% 0.43/0.85  (assume @p201 (forall @t274 (=> @t344 (= @t273 @t258))))
% 0.43/0.85  (assume @p202 (forall @t230 (=> @t180 (=> @t346 @t345))))
% 0.43/0.85  (assume @p203 (forall @t281 (=> @t181 (=> @t348 @t347))))
% 0.43/0.85  (assume @p204 (forall @t285 (=> @t351 (=> @t350 @t349))))
% 0.43/0.85  (assume @p205 (forall @t230 (=> @t277 @t276)))
% 0.43/0.85  (assume @p206 (forall @t281 (=> @t280 @t279)))
% 0.43/0.85  (assume @p207 (forall @t285 (=> @t284 @t283)))
% 0.43/0.85  (assume @p208 (forall @t230 (=> @t345 (and @t180 @t346))))
% 0.43/0.85  (assume @p209 (forall @t281 (=> @t347 (and @t181 @t348))))
% 0.43/0.85  (assume @p210 (forall @t285 (=> @t349 (and @t351 @t350))))
% 0.43/0.85  (assume @p211 (not (= tptp.zero_zero_poly_a tptp.one_one_poly_a)))
% 0.43/0.85  (assume @p212 (not (= tptp.zero_zero_a tptp.one_one_a)))
% 0.43/0.85  (assume @p213 (not (= tptp.zero_zero_nat tptp.one_one_nat)))
% 0.43/0.85  (assume @p214 (not (_ (_ tptp.ord_less_nat tptp.one_one_nat) tptp.one_one_nat)))
% 0.43/0.85  (assume @p215 (not (_ (_ tptp.ord_less_a tptp.one_one_a) tptp.one_one_a)))
% 0.43/0.85  (assume @p216 (not (_ (_ tptp.ord_less_poly_a tptp.one_one_poly_a) tptp.one_one_poly_a)))
% 0.43/0.85  (assume @p217 (forall @t281 (= (_ @t207 @t75) (_ @t291 @t31))))
% 0.43/0.85  (assume @p218 (forall @t230 (= (_ @t208 @t69) (_ @t294 @t37))))
% 0.43/0.85  (assume @p219 (forall @t281 (= (_ @t201 @t290) (_ @t352 @t203))))
% 0.43/0.85  (assume @p220 (forall @t230 (= (_ @t205 @t229) (_ @t353 @t74))))
% 0.43/0.85  (assume @p221 (forall @t281 (= @t302 @t297)))
% 0.43/0.85  (assume @p222 (forall @t230 (= @t303 @t299)))
% 0.43/0.85  (assume @p223 (forall @t281 (= (= (_ @t76 @t31) (_ @t225 @t75)) (or @t254 (= @t31 @t290)))))
% 0.43/0.85  (assume @p224 (forall @t230 (= (= (_ @t100 @t37) (_ @t223 @t69)) (or @t70 @t326))))
% 0.43/0.85  (assume @p225 (not (= tptp.one_one_a @t47)))
% 0.43/0.85  (assume @p226 (forall @t359 (=> @t358 (=> (forall @t357 (=> (_ @t354 @t145) (_ @t354 @t356))) @t355))))
% 0.43/0.85  (assume @p227 (forall @t176 (=> @t175 (not (forall @t357 (not (= @t170 @t356)))))))
% 0.43/0.85  (assume @p228 (forall (@list @t362 @t361 @t141 @t360) (=> (forall (@list @t365 @t367) (_ (_ @t366 tptp.nil_a) @t367)) (=> (forall (@list @t365 @t121 @t364 @t363) (=> (_ (_ @t366 @t364) (_ (_ tptp.cons_a (_ @t365 @t121)) @t363)) (_ (_ @t366 (_ (_ tptp.cons_a @t121) @t364)) @t363))) (_ (_ (_ @t362 @t361) @t141) @t360)))))
% 0.43/0.85  (assume @p229 (forall (@list @t19 @t354) (=> @t373 (=> @t372 (=> (forall @t371 (=> (not (= @t149 tptp.nil_a)) (=> @t370 @t369))) @t368)))))
% 0.43/0.85  (assume @p230 (forall @t380 (=> @t379 (=> (forall (@list @t377 @t150) (_ @t378 @t172)) (=> (forall (@list @t377 @t150 @t146 @t149) (=> (_ @t378 @t168) (_ @t378 @t169))) @t376)))))
% 0.43/0.85  (assume @p231 (forall @t359 (=> @t358 (=> @t372 (=> (forall @t171 (=> (=> @t381 @t369) (=> (=> (not @t381) (_ @t354 @t168)) (_ @t354 @t169)))) @t355)))))
% 0.43/0.85  (assume @p232 (forall @t380 (=> @t379 (=> (forall (@list @t377 @t150 @t145) (=> (_ @t378 @t145) (_ @t378 @t356))) @t376))))
% 0.43/0.85  (assume @p233 (forall (@list @t383) (=> (not (= @t383 tptp.nil_list_a)) (=> (forall (@list @t382) (not (= @t383 (_ (_ tptp.cons_list_a tptp.nil_a) @t382)))) (not (forall (@list @t150 @t149 @t382) (not (= @t383 (_ (_ tptp.cons_list_a @t152) @t382)))))))))
% 0.43/0.85  (assume @p234 (forall @t162 (=> @t385 (=> @t161 (=> (forall @t156 (=> (_ @t155 @t148) (=> @t384 @t154))) @t144)))))
% 0.43/0.85  (assume @p235 (forall @t359 (=> (forall @t371 (=> (forall (@list @t387 @t386) (=> (= @t149 (_ (_ tptp.cons_a @t387) @t386)) @t370)) @t369)) (=> @t358 @t355))))
% 0.43/0.85  (assume @p236 (forall @t176 (=> (forall @t371 (not (= @t170 @t152))) @t174)))
% 0.43/0.85  (assume @p237 (forall (@list @t354 @t19) (=> @t358 (=> @t372 (=> (forall (@list @t150 @t146 @t388) (=> (_ @t354 @t388) (=> (_ @t354 @t389) (_ @t354 (_ @t151 @t389))))) @t368)))))
% 0.43/0.85  (assume @p238 (forall @t162 (=> @t385 (=> (forall (@list @t150 @t149 @t145) (=> (_ (_ @t143 @t145) @t149) @t384)) @t144))))
% 0.43/0.85  (assume @p239 (forall (@list @t143 @t19 @t189) (=> (_ @t160 tptp.nil_a) (=> (forall @t371 (_ @t153 tptp.nil_a)) (=> @t165 (=> @t157 (_ (_ @t143 @t19) @t189)))))))
% 0.43/0.85  (assume @p240 (forall @t58 (= @t373 (exists (@list @t391 @t390) (= @t19 (_ (_ tptp.cons_a @t391) @t390))))))
% 0.43/0.85  (assume @p241 (forall (@list @t354 @t392) (=> @t358 (=> (forall (@list @t394 @t393) (=> (_ @t354 @t393) (_ @t354 (_ (_ tptp.cons_a @t394) @t393)))) (_ @t354 @t392)))))
% 0.43/0.85  (assume @p242 (forall (@list @t397) (=> (not (= @t397 tptp.nil_a)) (not (forall (@list @t396 @t395) (not (= @t397 (_ (_ tptp.cons_a @t396) @t395))))))))
% 0.43/0.85  (assume @p243 (forall (@list @t392 @t234 @t232) (=> (= @t392 @t235) (not (= @t392 tptp.nil_a)))))
% 0.43/0.85  (assume @p244 (forall (@list @t234 @t232) (not (= tptp.nil_a @t235))))
% 0.43/0.85  (assume @p245 (forall (@list @t62 @t19 @t189) (= (_ (_ tptp.append_a @t64) @t189) (_ @t63 @t238))))
% 0.43/0.85  (assume @p246 (forall (@list @t62 @t331 @t189 @t19 @t236) (=> (= (_ @t63 @t331) @t189) (=> (= @t19 (_ @t332 @t236)) (= @t64 @t241)))))
% 0.43/0.85  (assume @p247 (forall @t304 (= (_ @t398 @t244) @t244)))
% 0.43/0.85  (assume @p248 (forall (@list @t189) (= @t399 @t189)))
% 0.43/0.85  (assume @p249 (forall @t308 (=> @t190 (= @t19 @t399))))
% 0.43/0.85  (assume @p250 (forall @t65 (not (_ tptp.null_a @t64))))
% 0.43/0.85  (assume @p251 (forall @t58 (= @t306 (_ tptp.null_a @t19))))
% 0.43/0.85  (assume @p252 (_ tptp.null_a tptp.nil_a))
% 0.43/0.85  (assume @p253 (forall @t325 (=> @t402 (=> @t400 (_ (_ tptp.ord_less_nat @t272) @t271)))))
% 0.43/0.85  (assume @p254 (forall @t405 (=> @t293 (=> @t404 @t403))))
% 0.43/0.85  (assume @p255 (forall @t324 (=> @t289 (=> @t407 @t406))))
% 0.43/0.85  (assume @p256 (forall @t253 (= @t411 @t410)))
% 0.43/0.85  (assume @p257 (forall @t257 (= @t415 @t414)))
% 0.43/0.85  (assume @p258 (forall @t325 (=> @t402 (=> @t400 (_ (_ tptp.ord_less_nat @t264) @t263)))))
% 0.43/0.85  (assume @p259 (forall @t405 (=> @t293 (=> @t404 @t411))))
% 0.43/0.85  (assume @p260 (forall @t324 (=> @t289 (=> @t407 @t415))))
% 0.43/0.85  (assume @p261 (forall @t416 (=> @t408 (=> @t409 @t411))))
% 0.43/0.85  (assume @p262 (forall @t318 (=> @t412 (=> @t413 @t415))))
% 0.43/0.85  (assume @p263 (forall @t267 (= @t403 @t410)))
% 0.43/0.85  (assume @p264 (forall @t269 (= @t406 @t414)))
% 0.43/0.85  (assume @p265 (forall @t416 (=> @t408 (=> @t409 @t403))))
% 0.43/0.85  (assume @p266 (forall @t318 (=> @t412 (=> @t413 @t406))))
% 0.43/0.85  (assume @p267 (forall @t267 (=> @t404 (= @t403 @t293))))
% 0.43/0.85  (assume @p268 (forall @t269 (=> @t407 (= @t406 @t289))))
% 0.43/0.85  (assume @p269 (forall @t267 (=> @t409 (= @t403 @t408))))
% 0.43/0.85  (assume @p270 (forall @t269 (=> @t413 (= @t406 @t412))))
% 0.43/0.85  (assume @p271 (forall (@list @t80 @t81) (=> (_ @t248 @t420) @t419)))
% 0.43/0.85  (assume @p272 (forall @t295 (=> (_ @t40 @t423) @t422)))
% 0.43/0.85  (assume @p273 (forall @t292 (=> (_ @t34 @t426) @t425)))
% 0.43/0.85  (assume @p274 (forall @t285 (=> @t427 @t419)))
% 0.43/0.85  (assume @p275 (forall @t230 (=> @t428 @t422)))
% 0.43/0.85  (assume @p276 (forall @t281 (=> @t429 @t425)))
% 0.43/0.85  (assume @p277 (forall @t230 (= @t428 (or (and @t41 @t421) (and @t206 @t430)))))
% 0.43/0.85  (assume @p278 (forall @t281 (= @t429 (or (and @t35 @t424) (and @t202 @t431)))))
% 0.43/0.85  (assume @p279 (forall @t285 (=> @t418 (=> @t432 (_ (_ tptp.ord_less_nat @t420) tptp.zero_zero_nat)))))
% 0.43/0.85  (assume @p280 (forall @t230 (=> @t41 (=> @t430 (_ (_ tptp.ord_less_a @t423) tptp.zero_zero_a)))))
% 0.43/0.85  (assume @p281 (forall @t281 (=> @t35 (=> @t431 (_ (_ tptp.ord_less_poly_a @t426) tptp.zero_zero_poly_a)))))
% 0.43/0.85  (assume @p282 (forall @t285 (=> @t418 (=> @t417 @t427))))
% 0.43/0.85  (assume @p283 (forall @t230 (=> @t41 (=> @t421 @t428))))
% 0.43/0.85  (assume @p284 (forall @t281 (=> @t35 (=> @t424 @t429))))
% 0.43/0.85  (assume @p285 (forall @t285 (=> @t418 (=> @t432 @t433))))
% 0.43/0.85  (assume @p286 (forall @t230 (=> @t41 (=> @t430 @t434))))
% 0.43/0.85  (assume @p287 (forall @t281 (=> @t35 (=> @t431 @t435))))
% 0.43/0.85  (assume @p288 (forall @t285 (=> @t436 (=> @t417 @t433))))
% 0.43/0.85  (assume @p289 (forall @t230 (=> @t206 (=> @t421 @t434))))
% 0.43/0.85  (assume @p290 (forall @t281 (=> @t202 (=> @t424 @t435))))
% 0.43/0.85  (assume @p291 (forall @t230 (= @t434 (or (and @t41 @t430) (and @t206 @t421)))))
% 0.43/0.85  (assume @p292 (forall @t281 (= @t435 (or (and @t35 @t431) (and @t202 @t424)))))
% 0.43/0.85  (assume @p293 (forall @t444 (= @t443 @t439)))
% 0.43/0.85  (assume @p294 (forall @t340 (= (_ @t248 @t446) (and (_ @t248 @t338) @t249))))
% 0.43/0.85  (assume @p295 (forall @t450 (= (_ (_ tptp.ord_less_nat @t449) @t448) @t439)))
% 0.43/0.85  (assume @p296 (forall @t450 (= (= @t449 @t448) @t453)))
% 0.43/0.85  (assume @p297 (forall @t250 (= @t337 @t249)))
% 0.43/0.85  (assume @p298 (forall @t286 (= @t351 @t418)))
% 0.43/0.85  (assume @p299 (forall @t340 (= (= @t446 tptp.zero_zero_nat) (or @t454 @t247))))
% 0.43/0.85  (assume @p300 (forall (@list @t338) (= (_ @t445 tptp.zero_zero_nat) tptp.zero_zero_nat)))
% 0.43/0.85  (assume @p301 (forall @t444 (= @t455 @t453)))
% 0.43/0.85  (assume @p302 (forall @t340 (= (= tptp.one_one_nat @t446) @t457)))
% 0.43/0.85  (assume @p303 (forall @t340 (= (= @t446 tptp.one_one_nat) @t457)))
% 0.43/0.85  (assume @p304 (forall @t250 (= (_ @t341 tptp.one_one_nat) @t247)))
% 0.43/0.85  (assume @p305 (forall @t250 (= (_ @t288 @t246) @t246)))
% 0.43/0.85  (assume @p306 (forall @t250 (= (_ @t447 tptp.one_one_nat) @t246)))
% 0.43/0.85  (assume @p307 (forall (@list @t309 @t458) (=> (not (= @t309 @t458)) (=> (not (_ (_ tptp.ord_less_nat @t309) @t458)) (_ (_ tptp.ord_less_nat @t458) @t309)))))
% 0.43/0.85  (assume @p308 (forall @t469 (=> (forall @t468 @t467) @t460)))
% 0.43/0.85  (assume @p309 (forall @t469 (=> (forall @t468 (=> (forall @t465 (=> @t464 @t462)) @t466)) @t460)))
% 0.43/0.85  (assume @p310 (forall @t250 (not (_ @t341 @t246))))
% 0.43/0.85  (assume @p311 (forall (@list @t471 @t470) (=> (_ (_ tptp.ord_less_nat @t471) @t470) (not (= @t471 @t470)))))
% 0.43/0.85  (assume @p312 (forall (@list @t246 @t338) (=> @t473 @t472)))
% 0.43/0.85  (assume @p313 (forall @t340 (= @t472 (or @t339 @t473))))
% 0.43/0.85  (assume @p314 (forall @t469 (=> (_ @t459 tptp.zero_zero_nat) (=> (forall @t468 (=> (_ @t248 @t463) @t467)) @t460))))
% 0.43/0.85  (assume @p315 (forall @t286 (not @t436)))
% 0.43/0.85  (assume @p316 (forall @t477 (=> @t476 (=> @t438 (_ (_ tptp.ord_less_nat (_ (_ tptp.times_times_nat @t475) @t437)) (_ (_ tptp.times_times_nat @t474) @t437))))))
% 0.43/0.85  (assume @p317 (forall @t477 (=> @t476 (=> @t438 (_ (_ tptp.ord_less_nat (_ @t440 @t475)) (_ @t440 @t474))))))
% 0.43/0.85  (assume @p318 (forall @t250 (= (_ @t287 @t246) tptp.zero_zero_nat)))
% 0.43/0.85  (assume @p319 (forall @t444 (=> @t438 (= @t455 @t452))))
% 0.43/0.85  (assume @p320 (forall @t444 (=> @t438 (= @t443 @t339))))
% 0.43/0.85  (assume @p321 (forall @t444 (= @t455 (or @t451 @t452))))
% 0.43/0.85  (assume @p322 (forall @t340 (=> (= @t338 @t446) (or @t456 @t454))))
% 0.43/0.85  (assume @p323 @t480)
% 0.43/0.85  (assume @p324 true)
% 0.43/0.85  (step @p325 (= tptp.v @t482) :rule refl :args (@t482))
% 0.43/0.85  (step @p326 (= tptp.is_zero_poly_a @t483) :rule refl :args (@t483))
% 0.43/0.85  (step @p327 (= tptp.is_zero_a @t484) :rule refl :args (@t484))
% 0.43/0.85  (step @p328 :rule eq-symm :args (@t490 @t494))
% 0.43/0.85  (step @p329 :rule refl :args ((tptp.append_a @t28 @t495)))
% 0.43/0.85  (step @p330 :rule refl :args (@t496))
% 0.43/0.85  (step @p331 :rule refl :args (@t491))
% 0.43/0.85  (step @p332 :rule refl :args (tptp.zero_zero_a))
% 0.43/0.85  (step @p333 :rule cong :premises (@p332 @p331) :args (@t492))
% 0.43/0.85  (step @p334 :rule trans :premises (@p333 @p330))
% 0.43/0.85  (step @p335 :rule refl :args (@t493))
% 0.43/0.85  (step @p336 :rule cong :premises (@p335 @p334) :args (@t494))
% 0.43/0.85  (step @p337 :rule trans :premises (@p336 @p329))
% 0.43/0.85  (step @p338 :rule refl :args (tptp.append_a))
% 0.43/0.85  (step @p339 :rule ho_cong :premises (@p338 @p335))
% 0.43/0.85  (step @p340 :rule ho_cong :premises (@p339 @p334))
% 0.43/0.85  (step @p341 :rule cong :premises (@p340 @p337) :args ((= (_ (_ tptp.append_a @t493) @t492) @t494)))
% 0.43/0.85  (step @p342 :rule symm :premises (@p341))
% 0.43/0.85  (step @p343 :rule refl :args (@t497))
% 0.43/0.85  (step @p344 :rule eq_resolve :premises (@p343 @p342))
% 0.43/0.85  (step @p345 :rule refl :args (@t26))
% 0.43/0.85  (step @p346 :rule ho_cong :premises (@p345 @p331))
% 0.43/0.85  (step @p347 :rule cong :premises (@p346 @p334) :args ((= (_ @t26 @t491) @t492)))
% 0.43/0.85  (step @p348 :rule symm :premises (@p347))
% 0.43/0.85  (step @p349 :rule refl :args (@t495))
% 0.43/0.85  (step @p350 :rule eq_resolve :premises (@p349 @p348))
% 0.43/0.85  (step @p351 :rule refl :args (@t104))
% 0.43/0.85  (step @p352 :rule cong :premises (@p351 @p331) :args ((= @t104 @t491)))
% 0.43/0.85  (step @p353 :rule symm :premises (@p352))
% 0.43/0.85  (step @p354 :rule eq_resolve :premises (@p351 @p353))
% 0.43/0.85  (step @p355 :rule refl :args (@t26))
% 0.43/0.85  (step @p356 :rule ho_cong :premises (@p355 @p354))
% 0.43/0.85  (step @p357 :rule trans :premises (@p356 @p350))
% 0.43/0.85  (step @p358 :rule refl :args (@t28))
% 0.43/0.85  (step @p359 :rule cong :premises (@p358 @p335) :args ((= @t28 @t493)))
% 0.43/0.85  (step @p360 :rule symm :premises (@p359))
% 0.43/0.85  (step @p361 :rule eq_resolve :premises (@p358 @p360))
% 0.43/0.85  (step @p362 :rule refl :args (tptp.append_a))
% 0.43/0.85  (step @p363 :rule ho_cong :premises (@p362 @p361))
% 0.43/0.85  (step @p364 :rule ho_cong :premises (@p363 @p357))
% 0.43/0.85  (step @p365 :rule trans :premises (@p364 @p344))
% 0.43/0.85  (step @p366 :rule refl :args ((tptp.descar1375166517sums_a @t52)))
% 0.43/0.85  (step @p367 :rule refl :args ((tptp.coeffs_a @t51)))
% 0.43/0.85  (step @p368 :rule refl :args ((tptp.times_times_poly_a @t50 tptp.g)))
% 0.43/0.85  (step @p369 :rule refl :args (tptp.g))
% 0.43/0.85  (step @p370 :rule refl :args ((tptp.pCons_a tptp.one_one_a @t48)))
% 0.43/0.85  (step @p371 :rule refl :args ((tptp.pCons_a @t47 tptp.zero_zero_poly_a)))
% 0.43/0.85  (step @p372 :rule refl :args (tptp.zero_zero_poly_a))
% 0.43/0.85  (step @p373 :rule refl :args (@t485))
% 0.43/0.85  (step @p374 :rule cong :premises (@p373 @p372) :args (@t486))
% 0.43/0.85  (step @p375 :rule trans :premises (@p374 @p371))
% 0.43/0.85  (step @p376 :rule refl :args (tptp.one_one_a))
% 0.43/0.85  (step @p377 :rule cong :premises (@p376 @p375) :args (@t487))
% 0.43/0.85  (step @p378 :rule trans :premises (@p377 @p370))
% 0.43/0.85  (step @p379 :rule cong :premises (@p378 @p369) :args (@t488))
% 0.43/0.85  (step @p380 :rule trans :premises (@p379 @p368))
% 0.43/0.85  (step @p381 :rule cong :premises (@p380) :args (@t489))
% 0.43/0.85  (step @p382 :rule trans :premises (@p381 @p367))
% 0.43/0.85  (step @p383 :rule cong :premises (@p382) :args (@t490))
% 0.43/0.85  (step @p384 :rule trans :premises (@p383 @p366))
% 0.43/0.85  (step @p385 :rule refl :args (tptp.descar1375166517sums_a))
% 0.43/0.85  (step @p386 :rule ho_cong :premises (@p385 @p382))
% 0.43/0.85  (step @p387 :rule cong :premises (@p386 @p384) :args ((= (_ tptp.descar1375166517sums_a @t489) @t490)))
% 0.43/0.85  (step @p388 :rule symm :premises (@p387))
% 0.43/0.85  (step @p389 :rule refl :args (@t498))
% 0.43/0.85  (step @p390 :rule eq_resolve :premises (@p389 @p388))
% 0.43/0.85  (step @p391 :rule refl :args (tptp.coeffs_a))
% 0.43/0.85  (step @p392 :rule ho_cong :premises (@p391 @p380))
% 0.43/0.85  (step @p393 :rule cong :premises (@p392 @p382) :args ((= (_ tptp.coeffs_a @t488) @t489)))
% 0.43/0.85  (step @p394 :rule symm :premises (@p393))
% 0.43/0.85  (step @p395 :rule refl :args (@t52))
% 0.43/0.85  (step @p396 :rule eq_resolve :premises (@p395 @p394))
% 0.43/0.85  (step @p397 :rule refl :args (tptp.times_times_poly_a))
% 0.43/0.85  (step @p398 :rule ho_cong :premises (@p397 @p378))
% 0.43/0.85  (step @p399 :rule ho_cong :premises (@p398 @p369))
% 0.43/0.85  (step @p400 :rule cong :premises (@p399 @p380) :args ((= (_ (_ tptp.times_times_poly_a @t487) tptp.g) @t488)))
% 0.43/0.85  (step @p401 :rule symm :premises (@p400))
% 0.43/0.85  (step @p402 :rule refl :args (@t51))
% 0.43/0.85  (step @p403 :rule eq_resolve :premises (@p402 @p401))
% 0.43/0.85  (step @p404 :rule refl :args (tptp.g))
% 0.43/0.85  (step @p405 :rule refl :args (@t49))
% 0.43/0.85  (step @p406 :rule ho_cong :premises (@p405 @p375))
% 0.43/0.85  (step @p407 :rule cong :premises (@p406 @p378) :args ((= (_ @t49 @t486) @t487)))
% 0.43/0.85  (step @p408 :rule symm :premises (@p407))
% 0.43/0.85  (step @p409 :rule refl :args (@t50))
% 0.43/0.85  (step @p410 :rule eq_resolve :premises (@p409 @p408))
% 0.43/0.85  (step @p411 :rule refl :args (tptp.pCons_a))
% 0.43/0.85  (step @p412 :rule ho_cong :premises (@p411 @p373))
% 0.43/0.85  (step @p413 :rule ho_cong :premises (@p412 @p372))
% 0.43/0.85  (step @p414 :rule cong :premises (@p413 @p375) :args ((= (_ (_ tptp.pCons_a @t485) tptp.zero_zero_poly_a) @t486)))
% 0.43/0.85  (step @p415 :rule symm :premises (@p414))
% 0.43/0.85  (step @p416 :rule refl :args (@t48))
% 0.43/0.85  (step @p417 :rule eq_resolve :premises (@p416 @p415))
% 0.43/0.85  (step @p418 :rule refl :args (tptp.zero_zero_poly_a))
% 0.43/0.85  (step @p419 :rule refl :args (@t47))
% 0.43/0.85  (step @p420 :rule cong :premises (@p419 @p373) :args ((= @t47 @t485)))
% 0.43/0.85  (step @p421 :rule symm :premises (@p420))
% 0.43/0.85  (step @p422 :rule eq_resolve :premises (@p419 @p421))
% 0.43/0.85  (step @p423 :rule refl :args (tptp.pCons_a))
% 0.43/0.85  (step @p424 :rule ho_cong :premises (@p423 @p422))
% 0.43/0.85  (step @p425 :rule ho_cong :premises (@p424 @p418))
% 0.43/0.85  (step @p426 :rule trans :premises (@p425 @p417))
% 0.43/0.85  (step @p427 :rule refl :args (@t49))
% 0.43/0.85  (step @p428 :rule ho_cong :premises (@p427 @p426))
% 0.43/0.85  (step @p429 :rule trans :premises (@p428 @p410))
% 0.43/0.85  (step @p430 :rule refl :args (tptp.times_times_poly_a))
% 0.43/0.85  (step @p431 :rule ho_cong :premises (@p430 @p429))
% 0.43/0.85  (step @p432 :rule ho_cong :premises (@p431 @p404))
% 0.43/0.85  (step @p433 :rule trans :premises (@p432 @p403))
% 0.43/0.85  (step @p434 :rule refl :args (tptp.coeffs_a))
% 0.43/0.85  (step @p435 :rule ho_cong :premises (@p434 @p433))
% 0.43/0.85  (step @p436 :rule trans :premises (@p435 @p396))
% 0.43/0.85  (step @p437 :rule refl :args (tptp.descar1375166517sums_a))
% 0.43/0.85  (step @p438 :rule ho_cong :premises (@p437 @p436))
% 0.43/0.85  (step @p439 :rule trans :premises (@p438 @p390))
% 0.43/0.85  (step @p440 :rule cong :premises (@p439 @p365) :args ((= @t498 @t497)))
% 0.43/0.85  (step @p441 :rule trans :premises (@p440 @p328))
% 0.43/0.85  (step @p442 :rule symm :premises (@p53))
% 0.43/0.85  (step @p443 :rule ho_cong :premises (@p355 @p442))
% 0.43/0.85  (step @p444 :rule refl :args (@t29))
% 0.43/0.85  (step @p445 :rule ho_cong :premises (@p444 @p443))
% 0.43/0.85  (step @p446 :rule ho_cong :premises (@p437 @p14))
% 0.43/0.85  (step @p447 :rule trans :premises (@p4 @p446))
% 0.43/0.85  (step @p448 :rule cong :premises (@p447 @p445) :args (@t30))
% 0.43/0.85  (step @p449 :rule trans :premises (@p448 @p441))
% 0.43/0.85  (step @p450 :rule eq_resolve :premises (@p7 @p449))
% 0.43/0.85  (step @p451 :rule eq-symm :args (@t499 @t500))
% 0.43/0.85  (step @p452 :rule refl :args ((tptp.descar2095969287nges_a @t498)))
% 0.43/0.85  (step @p453 :rule cong :premises (@p384) :args (@t500))
% 0.43/0.85  (step @p454 :rule trans :premises (@p453 @p452))
% 0.43/0.85  (step @p455 :rule refl :args (tptp.descar2095969287nges_a))
% 0.43/0.85  (step @p456 :rule ho_cong :premises (@p455 @p384))
% 0.43/0.85  (step @p457 :rule cong :premises (@p456 @p454) :args ((= (_ tptp.descar2095969287nges_a @t490) @t500)))
% 0.43/0.85  (step @p458 :rule symm :premises (@p457))
% 0.43/0.85  (step @p459 :rule refl :args (@t501))
% 0.43/0.85  (step @p460 :rule eq_resolve :premises (@p459 @p458))
% 0.43/0.85  (step @p461 :rule refl :args (tptp.descar2095969287nges_a))
% 0.43/0.85  (step @p462 :rule ho_cong :premises (@p461 @p439))
% 0.43/0.85  (step @p463 :rule trans :premises (@p462 @p460))
% 0.43/0.85  (step @p464 :rule refl :args ((tptp.descar2095969287nges_a @t28)))
% 0.43/0.85  (step @p465 :rule cong :premises (@p335) :args (@t499))
% 0.43/0.85  (step @p466 :rule trans :premises (@p465 @p464))
% 0.43/0.85  (step @p467 :rule ho_cong :premises (@p455 @p335))
% 0.43/0.85  (step @p468 :rule cong :premises (@p467 @p466) :args ((= (_ tptp.descar2095969287nges_a @t493) @t499)))
% 0.43/0.85  (step @p469 :rule symm :premises (@p468))
% 0.43/0.85  (step @p470 :rule refl :args (@t478))
% 0.43/0.85  (step @p471 :rule eq_resolve :premises (@p470 @p469))
% 0.43/0.85  (step @p472 :rule ho_cong :premises (@p461 @p361))
% 0.43/0.85  (step @p473 :rule trans :premises (@p472 @p471))
% 0.43/0.85  (step @p474 :rule cong :premises (@p473 @p463) :args (@t502))
% 0.43/0.85  (step @p475 :rule trans :premises (@p474 @p451))
% 0.43/0.85  (step @p476 :rule cong :premises (@p475) :args ((not @t502)))
% 0.43/0.85  (step @p477 :rule eq-symm :args (@t501 @t478))
% 0.43/0.85  (step @p478 :rule cong :premises (@p477) :args ((not (= @t501 @t478))))
% 0.43/0.85  (step @p479 :rule refl :args (@t478))
% 0.43/0.85  (step @p480 :rule ho_cong :premises (@p461 @p447))
% 0.43/0.85  (step @p481 :rule cong :premises (@p480 @p479) :args (@t479))
% 0.43/0.85  (step @p482 :rule cong :premises (@p481) :args (@t480))
% 0.43/0.85  (step @p483 :rule trans :premises (@p482 @p478))
% 0.43/0.85  (step @p484 :rule trans :premises (@p483 @p476))
% 0.43/0.85  (step @p485 :rule eq_resolve :premises (@p323 @p484))
% 0.43/0.85  (step @p486 :rule refl :args ((tptp.poly_a2 @t17)))
% 0.43/0.85  (step @p487 :rule refl :args (@t503))
% 0.43/0.85  (step @p488 :rule cong :premises (@p487) :args (@t504))
% 0.43/0.85  (step @p489 :rule trans :premises (@p488 @p486))
% 0.43/0.85  (step @p490 :rule refl :args (tptp.poly_a2))
% 0.43/0.85  (step @p491 :rule ho_cong :premises (@p490 @p487))
% 0.43/0.85  (step @p492 :rule cong :premises (@p491 @p489) :args ((= (_ tptp.poly_a2 @t503) @t504)))
% 0.43/0.85  (step @p493 :rule symm :premises (@p492))
% 0.43/0.85  (step @p494 :rule refl :args (@t44))
% 0.43/0.85  (step @p495 :rule eq_resolve :premises (@p494 @p493))
% 0.43/0.85  (step @p496 :rule refl :args (@t17))
% 0.43/0.85  (step @p497 :rule cong :premises (@p496 @p487) :args ((= @t17 @t503)))
% 0.43/0.85  (step @p498 :rule symm :premises (@p497))
% 0.43/0.85  (step @p499 :rule eq_resolve :premises (@p496 @p498))
% 0.43/0.85  (step @p500 :rule ho_cong :premises (@p490 @p499))
% 0.43/0.85  (step @p501 :rule trans :premises (@p500 @p495))
% 0.43/0.85  (step @p502 :rule refl :args (@t16))
% 0.43/0.85  (step @p503 :rule cong :premises (@p502 @p501) :args (@t505))
% 0.43/0.85  (step @p504 :rule cong :premises (@p503) :args ((forall @t45 @t505)))
% 0.43/0.85  (step @p505 :rule eq-symm :args (@t44 @t16))
% 0.43/0.85  (step @p506 :rule cong :premises (@p505) :args (@t46))
% 0.43/0.85  (step @p507 :rule trans :premises (@p506 @p504))
% 0.43/0.85  (step @p508 :rule eq_resolve :premises (@p11 @p507))
% 0.43/0.85  (step @p509 :rule instantiate :premises (@p508) :args ((@list tptp.g)))
% 0.43/0.85  (step @p510 :rule eq_resolve :premises (@p351 @p353))
% 0.43/0.85  (step @p511 :rule cong :premises (@p332 @p510) :args (@t496))
% 0.43/0.85  (step @p512 :rule refl :args (@t111))
% 0.43/0.85  (step @p513 :rule cong :premises (@p512 @p511) :args (@t506))
% 0.43/0.85  (step @p514 :rule cong :premises (@p513) :args (@t507))
% 0.43/0.85  (step @p515 :rule refl :args (@t508))
% 0.43/0.85  (step @p516 :rule cong :premises (@p515 @p514) :args (@t509))
% 0.43/0.85  (step @p517 :rule cong :premises (@p516) :args ((forall @t117 @t509)))
% 0.43/0.85  (step @p518 :rule eq-symm :args (@t507 @t508))
% 0.43/0.85  (step @p519 :rule cong :premises (@p518) :args ((forall @t117 (= @t507 @t508))))
% 0.43/0.85  (step @p520 :rule trans :premises (@p519 @p517))
% 0.43/0.85  (step @p521 :rule refl :args (@t508))
% 0.43/0.85  (step @p522 :rule refl :args (tptp.zero_zero_a))
% 0.43/0.85  (step @p523 :rule cong :premises (@p522 @p442) :args (@t510))
% 0.43/0.85  (step @p524 :rule refl :args (@t111))
% 0.43/0.85  (step @p525 :rule cong :premises (@p524 @p523) :args (@t511))
% 0.43/0.85  (step @p526 :rule cong :premises (@p525) :args (@t512))
% 0.43/0.85  (step @p527 :rule cong :premises (@p526 @p521) :args (@t513))
% 0.43/0.85  (step @p528 :rule cong :premises (@p527) :args ((forall @t117 @t513)))
% 0.43/0.85  (step @p529 :rule trans :premises (@p528 @p520))
% 0.43/0.85  (step @p530 :rule refl :args (@t508))
% 0.43/0.85  (step @p531 :rule refl :args (@t112))
% 0.43/0.85  (step @p532 :rule cong :premises (@p531 @p530) :args ((= @t112 @t508)))
% 0.43/0.85  (step @p533 :rule symm :premises (@p532))
% 0.43/0.85  (step @p534 :rule eq_resolve :premises (@p531 @p533))
% 0.43/0.85  (step @p535 :rule refl :args ((tptp.poly_a2 @t114)))
% 0.43/0.85  (step @p536 :rule refl :args ((tptp.append_a @t111 @t27)))
% 0.43/0.85  (step @p537 :rule refl :args (@t510))
% 0.43/0.85  (step @p538 :rule cong :premises (@p512 @p537) :args (@t511))
% 0.43/0.85  (step @p539 :rule trans :premises (@p538 @p536))
% 0.43/0.85  (step @p540 :rule cong :premises (@p539) :args (@t512))
% 0.43/0.85  (step @p541 :rule trans :premises (@p540 @p535))
% 0.43/0.85  (step @p542 :rule ho_cong :premises (@p490 @p539))
% 0.43/0.85  (step @p543 :rule cong :premises (@p542 @p541) :args ((= (_ tptp.poly_a2 @t511) @t512)))
% 0.43/0.85  (step @p544 :rule symm :premises (@p543))
% 0.43/0.85  (step @p545 :rule refl :args (@t115))
% 0.43/0.85  (step @p546 :rule eq_resolve :premises (@p545 @p544))
% 0.43/0.85  (step @p547 :rule refl :args (@t113))
% 0.43/0.85  (step @p548 :rule ho_cong :premises (@p547 @p537))
% 0.43/0.85  (step @p549 :rule cong :premises (@p548 @p539) :args ((= (_ @t113 @t510) @t511)))
% 0.43/0.85  (step @p550 :rule symm :premises (@p549))
% 0.43/0.85  (step @p551 :rule refl :args (@t114))
% 0.43/0.85  (step @p552 :rule eq_resolve :premises (@p551 @p550))
% 0.43/0.85  (step @p553 :rule refl :args (@t27))
% 0.43/0.85  (step @p554 :rule cong :premises (@p553 @p537) :args ((= @t27 @t510)))
% 0.43/0.85  (step @p555 :rule symm :premises (@p554))
% 0.43/0.85  (step @p556 :rule eq_resolve :premises (@p553 @p555))
% 0.43/0.85  (step @p557 :rule ho_cong :premises (@p547 @p556))
% 0.43/0.85  (step @p558 :rule trans :premises (@p557 @p552))
% 0.43/0.85  (step @p559 :rule ho_cong :premises (@p490 @p558))
% 0.43/0.85  (step @p560 :rule trans :premises (@p559 @p546))
% 0.43/0.85  (step @p561 :rule cong :premises (@p560 @p534) :args (@t116))
% 0.43/0.85  (step @p562 :rule cong :premises (@p561) :args (@t118))
% 0.43/0.85  (step @p563 :rule trans :premises (@p562 @p529))
% 0.43/0.85  (step @p564 :rule eq_resolve :premises (@p64 @p563))
% 0.43/0.85  (step @p565 :rule instantiate :premises (@p564) :args ((@list @t493)))
% 0.43/0.85  (step @p566 :rule aci_norm :args ((= (or false @t516) @t516)))
% 0.43/0.85  (step @p567 :rule refl :args (@t516))
% 0.43/0.85  (step @p568 :rule evaluate :args ((not true)))
% 0.43/0.85  (step @p569 :rule eq-refl :args (@t514))
% 0.43/0.85  (step @p570 :rule cong :premises (@p569) :args (@t517))
% 0.43/0.85  (step @p571 :rule trans :premises (@p570 @p568))
% 0.43/0.85  (step @p572 :rule nary_cong :premises (@p571 @p567) :args (@t518))
% 0.43/0.85  (step @p573 :rule trans :premises (@p572 @p566))
% 0.43/0.85  (step @p574 :rule cong :premises (@p573) :args ((forall @t58 @t518)))
% 0.43/0.85  (step @p575 :rule quant-var-elim-eq :args ((= (forall @t45 @t522) @t518)))
% 0.43/0.85  (step @p576 :rule aci_norm :args ((= @t523 @t522)))
% 0.43/0.85  (step @p577 :rule cong :premises (@p576) :args (@t524))
% 0.43/0.85  (step @p578 :rule trans :premises (@p577 @p575))
% 0.43/0.85  (step @p579 :rule cong :premises (@p578) :args (@t525))
% 0.43/0.85  (step @p580 :rule quant-merge-prenex :args ((= @t525 (forall @t24 @t523))))
% 0.43/0.85  (step @p581 :rule symm :premises (@p580))
% 0.43/0.85  (step @p582 :rule trans :premises (@p581 @p579))
% 0.43/0.85  (step @p583 :rule trans :premises (@p582 @p574))
% 0.43/0.85  (step @p584 :rule refl :args ((tptp.descar2095969287nges_a @t17)))
% 0.43/0.85  (step @p585 :rule cong :premises (@p487) :args (@t519))
% 0.43/0.85  (step @p586 :rule trans :premises (@p585 @p584))
% 0.43/0.85  (step @p587 :rule ho_cong :premises (@p455 @p487))
% 0.43/0.85  (step @p588 :rule cong :premises (@p587 @p586) :args ((= (_ tptp.descar2095969287nges_a @t503) @t519)))
% 0.43/0.85  (step @p589 :rule symm :premises (@p588))
% 0.43/0.85  (step @p590 :rule refl :args (@t18))
% 0.43/0.85  (step @p591 :rule eq_resolve :premises (@p590 @p589))
% 0.43/0.85  (step @p592 :rule ho_cong :premises (@p455 @p499))
% 0.43/0.85  (step @p593 :rule trans :premises (@p592 @p591))
% 0.43/0.85  (step @p594 :rule refl :args (@t515))
% 0.43/0.85  (step @p595 :rule refl :args (@t20))
% 0.43/0.85  (step @p596 :rule cong :premises (@p595 @p594) :args ((= @t20 @t515)))
% 0.43/0.85  (step @p597 :rule symm :premises (@p596))
% 0.43/0.85  (step @p598 :rule eq_resolve :premises (@p595 @p597))
% 0.43/0.85  (step @p599 :rule cong :premises (@p598 @p593) :args (@t21))
% 0.43/0.85  (step @p600 :rule refl :args (@t514))
% 0.43/0.85  (step @p601 :rule refl :args (@t22))
% 0.43/0.85  (step @p602 :rule cong :premises (@p601 @p600) :args ((= @t22 @t514)))
% 0.43/0.85  (step @p603 :rule symm :premises (@p602))
% 0.43/0.85  (step @p604 :rule eq_resolve :premises (@p601 @p603))
% 0.43/0.85  (step @p605 :rule cong :premises (@p502 @p604) :args (@t526))
% 0.43/0.85  (step @p606 :rule cong :premises (@p605) :args (@t527))
% 0.43/0.85  (step @p607 :rule nary_cong :premises (@p606 @p599) :args (@t528))
% 0.43/0.85  (step @p608 :rule cong :premises (@p607) :args ((forall @t24 @t528)))
% 0.43/0.85  (step @p609 :rule trans :premises (@p608 @p583))
% 0.43/0.85  (step @p610 :rule bool-impl-elim :args (@t526 @t21))
% 0.43/0.85  (step @p611 :rule cong :premises (@p610) :args ((forall @t24 (=> @t526 @t21))))
% 0.43/0.85  (step @p612 :rule trans :premises (@p611 @p609))
% 0.43/0.85  (step @p613 :rule refl :args (@t21))
% 0.43/0.85  (step @p614 :rule eq-symm :args (@t22 @t16))
% 0.43/0.85  (step @p615 :rule cong :premises (@p614 @p613) :args (@t23))
% 0.43/0.85  (step @p616 :rule cong :premises (@p615) :args (@t25))
% 0.43/0.85  (step @p617 :rule trans :premises (@p616 @p612))
% 0.43/0.85  (step @p618 :rule eq_resolve :premises (@p6 @p617))
% 0.43/0.85  (step @p619 :rule instantiate :premises (@p618) :args ((@list @t490)))
% 0.43/0.85  (step @p620 :rule refl :args (@t533))
% 0.43/0.85  (step @p621 :rule refl :args (@t536))
% 0.43/0.85  (step @p622 :rule refl :args (@t538))
% 0.43/0.85  (step @p623 :rule bool-double-not-elim :args (@t539))
% 0.43/0.85  (step @p624 :rule refl :args (@t541))
% 0.43/0.85  (step @p625 :rule nary_cong :premises (@p624 @p623 @p622 @p621 @p620) :args ((or @t541 (not @t542) @t538 @t536 @t533)))
% 0.43/0.85  (assume-push @p667 @t532)
% 0.43/0.85  (assume-push @p668 @t533)
% 0.43/0.85  (step @p628 :rule evaluate :args ((= false true)))
% 0.43/0.85  (step @p629 :rule true_intro :premises (@p619))
% 0.43/0.85  (step @p630 :rule false_intro :premises (@p485))
% 0.43/0.85  (step @p631 :rule symm :premises (@p509))
% 0.43/0.85  (step @p632 :rule symm :premises (@p565))
% 0.43/0.85  (step @p633 :rule symm :premises (@p450))
% 0.43/0.85  (step @p634 :rule cong :premises (@p633) :args (@t529))
% 0.43/0.85  (step @p635 :rule trans :premises (@p634 @p632 @p631))
% 0.43/0.85  (step @p636 :rule cong :premises (@p635) :args (@t530))
% 0.43/0.85  (step @p637 :rule cong :premises (@p636) :args (@t531))
% 0.43/0.85  (step @p638 :rule refl :args (@t500))
% 0.43/0.85  (step @p639 :rule cong :premises (@p638 @p637) :args (@t532))
% 0.43/0.85  (step @p640 :rule trans :premises (@p639 @p630))
% 0.43/0.85  (step @p641 :rule symm :premises (@p640))
% 0.43/0.85  (step @p642 :rule trans :premises (@p641 @p629))
% 0.43/0.85  (step @p643 false :rule eq_resolve :premises (@p642 @p628))
% 0.43/0.85  (step-pop @p669 :rule scope :premises (@p643))
% 0.43/0.85  (step-pop @p670 :rule scope :premises (@p669))
% 0.43/0.85  (step @p644 :rule process_scope :premises (@p670) :args (false))
% 0.43/0.85  (assume-push @p671 @t540)
% 0.43/0.85  (assume-push @p672 @t542)
% 0.43/0.85  (assume-push @p673 @t537)
% 0.43/0.85  (assume-push @p674 @t535)
% 0.43/0.85  (assume-push @p675 @t532)
% 0.43/0.85  (step @p630 :rule false_intro :premises (@p485))
% 0.43/0.85  (step @p631 :rule symm :premises (@p509))
% 0.43/0.85  (step @p632 :rule symm :premises (@p565))
% 0.43/0.85  (step @p633 :rule symm :premises (@p450))
% 0.43/0.85  (step @p634 :rule cong :premises (@p633) :args (@t529))
% 0.43/0.85  (step @p635 :rule trans :premises (@p634 @p632 @p631))
% 0.43/0.85  (step @p636 :rule cong :premises (@p635) :args (@t530))
% 0.43/0.85  (step @p637 :rule cong :premises (@p636) :args (@t531))
% 0.43/0.85  (step @p638 :rule refl :args (@t500))
% 0.43/0.85  (step @p639 :rule cong :premises (@p638 @p637) :args (@t532))
% 0.43/0.85  (step @p652 :rule trans :premises (@p639 @p630))
% 0.43/0.85  (step @p653 :rule false_elim :premises (@p652))
% 0.43/0.85  (step @p654 :rule and_intro :premises (@p619 @p653))
% 0.43/0.85  (step-pop @p676 :rule scope :premises (@p654))
% 0.43/0.85  (step-pop @p677 :rule scope :premises (@p676))
% 0.43/0.85  (step-pop @p678 :rule scope :premises (@p677))
% 0.43/0.85  (step-pop @p679 :rule scope :premises (@p678))
% 0.43/0.85  (step-pop @p680 :rule scope :premises (@p679))
% 0.43/0.85  (step @p655 :rule process_scope :premises (@p680) :args (@t543))
% 0.43/0.85  (step @p661 :rule implies_elim :premises (@p655))
% 0.43/0.85  (step @p662 :rule resolution :premises (@p661 @p644) :args (true @t543))
% 0.43/0.85  (step @p663 :rule not_and :premises (@p662))
% 0.43/0.85  (step @p664 :rule eq_resolve :premises (@p663 @p625))
% 0.43/0.85  (step @p665 :rule reordering :premises (@p664) :args ((or @t539 @t541 @t538 @t536 @t533)))
% 0.43/0.85  (step @p666 false :rule chain_m_resolution :premises (@p665 @p619 @p565 @p509 @p485 @p450) :args (false (@list false false false true false) (@list @t532 @t535 @t537 @t539 @t540)))
% 0.43/0.85  )
% 0.43/0.85  % SZS output end Proof
% 0.43/0.85  % cvc5 exiting
%------------------------------------------------------------------------------