%------------------------------------------------------------------------------ % File : cvc5---1.3.4 % Problem : ITP351_1 : TPTP v9.2.1. Released v8.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 08:26:24 AM UTC 2026 % Result : Theorem 48.68s 48.92s % Output : Proof 48.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP351_1 : TPTP v9.2.1. Released v8.1.0. % 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.18/0.34 % Computer : n010.cluster.edu % 0.18/0.34 % Model : x86_64 x86_64 % 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.34 % Memory : 8042.1875MB % 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.34 % CPULimit : 300 % 0.18/0.34 % WCLimit : 300 % 0.18/0.34 % DateTime : Tue Jun 2 05:01:40 EDT 2026 % 0.18/0.35 % CPUTime : % 0.42/0.66 %----Proving TF0_ARI % 48.68/48.92 --- Run --finite-model-find --decision=internal at 45... % 48.68/48.92 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 60... % 48.68/48.92 % SZS status Theorem % 48.68/48.92 % SZS output start Proof % 48.68/48.92 ( % 48.68/48.92 (declare-sort |tptp.'Real_real_bool_fun_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Real_bool_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Nat_nat_nat_fun_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Real_fps_real_fps_real_fps_fun_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Real_fps_real_fps_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Int_int_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Nat_nat_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Nat_real_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Real_fps_set$'| 0) % 48.68/48.92 (declare-sort |tptp.'Real_real_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Nat$'| 0) % 48.68/48.92 (declare-sort |tptp.'Real_fps_fps$'| 0) % 48.68/48.92 (declare-sort |tptp.'Real_fps$'| 0) % 48.68/48.92 (declare-sort |tptp.'Nat_real_fun_bool_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Int_set$'| 0) % 48.68/48.92 (declare-sort |tptp.'Int_int_int_fun_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Nat_set$'| 0) % 48.68/48.92 (declare-sort |tptp.'Real_set$'| 0) % 48.68/48.92 (declare-sort |tptp.'Real_real_real_fun_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Nat_bool_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Int_fps$'| 0) % 48.68/48.92 (declare-sort |tptp.'Nat_fps$'| 0) % 48.68/48.92 (declare-sort tptp.tlbool 0) % 48.68/48.92 (declare-sort |tptp.'Nat_real_fun_nat_real_fun_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Nat_real_fun_nat_nat_fun_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Int_bool_fun$'| 0) % 48.68/48.92 (declare-sort |tptp.'Int_int_bool_fun_fun$'| 0) % 48.68/48.92 (declare-const tptp.tlfalse tptp.tlbool) % 48.68/48.92 (declare-const |tptp.'fun_app$o'| (-> |tptp.'Real_bool_fun$'| Real Bool)) % 48.68/48.92 (declare-const |tptp.'fun_app$m'| (-> |tptp.'Int_bool_fun$'| Int Bool)) % 48.68/48.92 (declare-const |tptp.'fun_app$n'| (-> |tptp.'Int_int_bool_fun_fun$'| Int |tptp.'Int_bool_fun$'|)) % 48.68/48.92 (declare-const |tptp.'uminus$'| (-> |tptp.'Real_fps$'| |tptp.'Real_fps$'|)) % 48.68/48.92 (declare-const |tptp.'fun_app$j'| (-> |tptp.'Nat_real_fun_bool_fun$'| |tptp.'Nat_real_fun$'| Bool)) % 48.68/48.92 (declare-const |tptp.'fun_app$l'| (-> |tptp.'Nat_real_fun_nat_nat_fun_fun$'| |tptp.'Nat_real_fun$'| |tptp.'Nat_nat_fun$'|)) % 48.68/48.92 (declare-const |tptp.'fun_app$k'| (-> |tptp.'Nat_real_fun_nat_real_fun_fun$'| |tptp.'Nat_real_fun$'| |tptp.'Nat_real_fun$'|)) % 48.68/48.92 (declare-const |tptp.'one$c'| |tptp.'Real_fps_fps$'|) % 48.68/48.92 (declare-const |tptp.'less_eq$'| (-> |tptp.'Nat$'| |tptp.'Nat_bool_fun$'|)) % 48.68/48.92 (declare-const |tptp.'fps_compose$a'| (-> |tptp.'Int_fps$'| |tptp.'Int_fps$'| |tptp.'Int_fps$'|)) % 48.68/48.92 (declare-const |tptp.'fps_X$a'| |tptp.'Int_fps$'|) % 48.68/48.92 (declare-const |tptp.'fps_nth$c'| (-> |tptp.'Nat_fps$'| |tptp.'Nat$'| |tptp.'Nat$'|)) % 48.68/48.92 (declare-const |tptp.'fps_nth$b'| (-> |tptp.'Real_fps_fps$'| |tptp.'Nat$'| |tptp.'Real_fps$'|)) % 48.68/48.92 (declare-const |tptp.'fps_nth$a'| (-> |tptp.'Int_fps$'| |tptp.'Nat$'| Int)) % 48.68/48.92 (declare-const |tptp.'divide$c'| (-> |tptp.'Nat$'| |tptp.'Nat$'| |tptp.'Nat$'|)) % 48.68/48.92 (declare-const |tptp.'divide$a'| (-> Real |tptp.'Real_real_fun$'|)) % 48.68/48.92 (declare-const |tptp.'fun_app$i'| (-> |tptp.'Nat_real_fun$'| |tptp.'Nat$'| Real)) % 48.68/48.92 (declare-const |tptp.'fps_nth$'| (-> |tptp.'Real_fps$'| |tptp.'Nat_real_fun$'|)) % 48.68/48.92 (declare-const |tptp.'divide$'| (-> |tptp.'Real_fps$'| |tptp.'Real_fps$'| |tptp.'Real_fps$'|)) % 48.68/48.92 (declare-const |tptp.'fps_nth_deriv$'| (-> |tptp.'Nat$'| |tptp.'Real_fps$'| |tptp.'Real_fps$'|)) % 48.68/48.92 (declare-const |tptp.'bernoulli_fps$a'| |tptp.'Real_fps$'|) % 48.68/48.92 (declare-const |tptp.'bernoulli_fps$'| |tptp.'Real_fps$'|) % 48.68/48.92 (declare-const |tptp.'of_nat$'| (-> |tptp.'Nat$'| Int)) % 48.68/48.92 (declare-const |tptp.'fps_tan$'| (-> Real |tptp.'Real_fps$'|)) % 48.68/48.92 (declare-const |tptp.'fps_ln$'| (-> Real |tptp.'Real_fps$'|)) % 48.68/48.92 (declare-const |tptp.'minus$b'| (-> |tptp.'Nat$'| |tptp.'Nat$'| |tptp.'Nat$'|)) % 48.68/48.92 (declare-const |tptp.'fun_app$g'| (-> |tptp.'Real_real_real_fun_fun$'| Real |tptp.'Real_real_fun$'|)) % 48.68/48.92 (declare-const |tptp.'one$b'| |tptp.'Int_fps$'|) % 48.68/48.92 (declare-const |tptp.'times$g'| (-> |tptp.'Real_set$'| |tptp.'Real_set$'| |tptp.'Real_set$'|)) % 48.68/48.92 (declare-const |tptp.'member$b'| (-> |tptp.'Nat$'| |tptp.'Nat_set$'| Bool)) % 48.68/48.92 (declare-const |tptp.'minus$a'| (-> |tptp.'Int_fps$'| |tptp.'Int_fps$'| |tptp.'Int_fps$'|)) % 48.68/48.92 (declare-const |tptp.'fun_app$f'| (-> |tptp.'Int_int_int_fun_fun$'| Int |tptp.'Int_int_fun$'|)) % 48.68/48.92 (declare-const |tptp.'fps_Lambert_W$'| |tptp.'Real_fps$'|) % 48.68/48.92 (declare-const |tptp.'times$c'| |tptp.'Int_int_int_fun_fun$'|) % 48.68/48.92 (declare-const |tptp.'times$j'| (-> |tptp.'Nat_fps$'| |tptp.'Nat_fps$'| |tptp.'Nat_fps$'|)) % 48.68/48.92 (declare-const |tptp.'times$d'| (-> |tptp.'Int_set$'| |tptp.'Int_set$'| |tptp.'Int_set$'|)) % 48.68/48.92 (declare-const |tptp.'fun_app$h'| (-> |tptp.'Nat_bool_fun$'| |tptp.'Nat$'| Bool)) % 48.68/48.92 (declare-const |tptp.'member$c'| (-> Real |tptp.'Real_set$'| Bool)) % 48.68/48.92 (declare-const |tptp.'member$a'| (-> Int |tptp.'Int_set$'| Bool)) % 48.68/48.92 (declare-const |tptp.'fun_app$d'| (-> |tptp.'Nat_nat_fun$'| |tptp.'Nat$'| |tptp.'Nat$'|)) % 48.68/48.92 (declare-const |tptp.'times$f'| |tptp.'Real_real_real_fun_fun$'|) % 48.68/48.92 (declare-const |tptp.'minus$'| (-> |tptp.'Real_fps$'| |tptp.'Real_fps$'| |tptp.'Real_fps$'|)) % 48.68/48.92 (declare-const |tptp.'comm_monoid$c'| (-> |tptp.'Real_real_real_fun_fun$'| Real Bool)) % 48.68/48.92 (declare-const |tptp.'fun_app$e'| (-> |tptp.'Nat_nat_nat_fun_fun$'| |tptp.'Nat$'| |tptp.'Nat_nat_fun$'|)) % 48.68/48.92 (declare-const |tptp.'times$a'| |tptp.'Nat_nat_nat_fun_fun$'|) % 48.68/48.92 (declare-const |tptp.'one$'| |tptp.'Real_fps$'|) % 48.68/48.92 (declare-const |tptp.'fps_const$'| (-> Real |tptp.'Real_fps$'|)) % 48.68/48.92 (declare-const |tptp.'times$b'| (-> |tptp.'Real_fps_set$'| |tptp.'Real_fps_set$'| |tptp.'Real_fps_set$'|)) % 48.68/48.92 (declare-const |tptp.'fps_X$'| |tptp.'Real_fps$'|) % 48.68/48.92 (declare-const |tptp.'elt_set_times$a'| (-> Int |tptp.'Int_set$'| |tptp.'Int_set$'|)) % 48.68/48.92 (declare-const |tptp.'fun_app$'| (-> |tptp.'Real_real_fun$'| Real Real)) % 48.68/48.92 (declare-const |tptp.'times$h'| (-> |tptp.'Real_fps_fps$'| |tptp.'Real_fps_fps$'| |tptp.'Real_fps_fps$'|)) % 48.68/48.92 (declare-const |tptp.'uua$'| (-> Int |tptp.'Int_int_fun$'|)) % 48.68/48.92 (declare-const |tptp.'fps_compose$'| (-> |tptp.'Real_fps$'| |tptp.'Real_fps$'| |tptp.'Real_fps$'|)) % 48.68/48.92 (declare-const |tptp.'member$'| (-> |tptp.'Real_fps$'| |tptp.'Real_fps_set$'| Bool)) % 48.68/48.92 (declare-const |tptp.'times$'| |tptp.'Real_fps_real_fps_real_fps_fun_fun$'|) % 48.68/48.92 (declare-const |tptp.'one$a'| |tptp.'Nat$'|) % 48.68/48.92 (declare-const |tptp.'fun_app$a'| (-> |tptp.'Int_int_fun$'| Int Int)) % 48.68/48.92 (declare-const |tptp.'fps_exp$'| (-> Real |tptp.'Real_fps$'|)) % 48.68/48.92 (declare-const |tptp.'times$e'| (-> |tptp.'Nat_set$'| |tptp.'Nat_set$'| |tptp.'Nat_set$'|)) % 48.68/48.93 (declare-const |tptp.'divide$b'| (-> Int |tptp.'Int_int_fun$'|)) % 48.68/48.93 (declare-const |tptp.'elt_set_times$b'| (-> |tptp.'Nat$'| |tptp.'Nat_set$'| |tptp.'Nat_set$'|)) % 48.68/48.93 (declare-const |tptp.'fun_app$b'| (-> |tptp.'Real_fps_real_fps_fun$'| |tptp.'Real_fps$'| |tptp.'Real_fps$'|)) % 48.68/48.93 (declare-const |tptp.'fun_app$c'| (-> |tptp.'Real_fps_real_fps_real_fps_fun_fun$'| |tptp.'Real_fps$'| |tptp.'Real_fps_real_fps_fun$'|)) % 48.68/48.93 (declare-const |tptp.'monoid$b'| (-> |tptp.'Nat_nat_nat_fun_fun$'| |tptp.'Nat_bool_fun$'|)) % 48.68/48.93 (declare-const |tptp.'fps_inv$'| |tptp.'Real_fps_real_fps_fun$'|) % 48.68/48.93 (declare-const |tptp.'fps_ginv$'| (-> |tptp.'Real_fps$'| |tptp.'Real_fps_real_fps_fun$'|)) % 48.68/48.93 (declare-const |tptp.'monoid$'| (-> |tptp.'Real_fps_real_fps_real_fps_fun_fun$'| |tptp.'Real_fps$'| Bool)) % 48.68/48.93 (declare-const |tptp.'monoid$a'| (-> |tptp.'Int_int_int_fun_fun$'| Int Bool)) % 48.68/48.93 (declare-const |tptp.'uu$'| (-> Real |tptp.'Real_real_fun$'|)) % 48.68/48.93 (declare-const |tptp.'monoid$c'| (-> |tptp.'Real_real_real_fun_fun$'| Real Bool)) % 48.68/48.93 (declare-const |tptp.'comm_monoid$'| (-> |tptp.'Real_fps_real_fps_real_fps_fun_fun$'| |tptp.'Real_fps$'| Bool)) % 48.68/48.93 (declare-const |tptp.'elt_set_times$c'| (-> Real |tptp.'Real_set$'| |tptp.'Real_set$'|)) % 48.68/48.93 (declare-const |tptp.'nat$'| (-> Int |tptp.'Nat$'|)) % 48.68/48.93 (declare-const |tptp.'fps_shift$'| (-> |tptp.'Nat$'| |tptp.'Real_fps$'| |tptp.'Real_fps$'|)) % 48.68/48.93 (declare-const |tptp.'fps_const$c'| (-> |tptp.'Nat$'| |tptp.'Nat_fps$'|)) % 48.68/48.93 (declare-const |tptp.'comm_monoid$a'| (-> |tptp.'Int_int_int_fun_fun$'| Int Bool)) % 48.68/48.93 (declare-const |tptp.'comm_monoid$b'| (-> |tptp.'Nat_nat_nat_fun_fun$'| |tptp.'Nat_bool_fun$'|)) % 48.68/48.93 (declare-const |tptp.'zero$a'| |tptp.'Int_fps$'|) % 48.68/48.93 (declare-const |tptp.'fun_app$p'| (-> |tptp.'Real_real_bool_fun_fun$'| Real |tptp.'Real_bool_fun$'|)) % 48.68/48.93 (declare-const |tptp.'zero$'| |tptp.'Real_fps$'|) % 48.68/48.93 (declare-const |tptp.'fps_const$a'| (-> |tptp.'Real_fps$'| |tptp.'Real_fps_fps$'|)) % 48.68/48.93 (declare-const |tptp.'fps_const$b'| (-> Int |tptp.'Int_fps$'|)) % 48.68/48.93 (declare-const |tptp.'elt_set_times$'| (-> |tptp.'Real_fps$'| |tptp.'Real_fps_set$'| |tptp.'Real_fps_set$'|)) % 48.68/48.93 (declare-const |tptp.'times$i'| (-> |tptp.'Int_fps$'| |tptp.'Int_fps$'| |tptp.'Int_fps$'|)) % 48.68/48.93 (declare-const tptp.tltrue tptp.tlbool) % 48.68/48.93 (declare-const |tptp.'zero$b'| |tptp.'Nat$'|) % 48.68/48.93 (define @t1 () (@var "A__questionmark_v1" Real)) % 48.68/48.93 (define @t2 () (@var "A__questionmark_v0" Real)) % 48.68/48.93 (define @t3 () (- @t2 @t1)) % 48.68/48.93 (define @t4 () (@list @t2 @t1)) % 48.68/48.93 (define @t5 () (@var "A__questionmark_v1" Int)) % 48.68/48.93 (define @t6 () (@var "A__questionmark_v0" Int)) % 48.68/48.93 (define @t7 () (- @t6 @t5)) % 48.68/48.93 (define @t8 () (@list @t6 @t5)) % 48.68/48.93 (define @t9 () (|tptp.'fps_exp$'| 1/1)) % 48.68/48.93 (define @t10 () (|tptp.'fun_app$c'| |tptp.'times$'| |tptp.'fps_X$'|)) % 48.68/48.93 (define @t11 () (|tptp.'fun_app$b'| @t10 @t9)) % 48.68/48.93 (define @t12 () (@var "A__questionmark_v0" |tptp.'Real_fps$'|)) % 48.68/48.93 (define @t13 () (@list @t12)) % 48.68/48.93 (define @t14 () (|tptp.'fun_app$c'| |tptp.'times$'| @t12)) % 48.68/48.93 (define @t15 () (|tptp.'fun_app$b'| @t14 |tptp.'one$'|)) % 48.68/48.93 (define @t16 () (forall @t13 (= @t15 @t12))) % 48.68/48.93 (define @t17 () (@list @t6)) % 48.68/48.93 (define @t18 () (@var "A__questionmark_v0" |tptp.'Nat$'|)) % 48.68/48.93 (define @t19 () (|tptp.'fun_app$e'| |tptp.'times$a'| @t18)) % 48.68/48.93 (define @t20 () (@list @t18)) % 48.68/48.93 (define @t21 () (@list @t2)) % 48.68/48.93 (define @t22 () (|tptp.'fun_app$c'| |tptp.'times$'| |tptp.'one$'|)) % 48.68/48.93 (define @t23 () (|tptp.'fun_app$e'| |tptp.'times$a'| |tptp.'one$a'|)) % 48.68/48.93 (define @t24 () (|tptp.'fun_app$b'| |tptp.'fps_inv$'| @t11)) % 48.68/48.93 (define @t25 () (= @t2 @t1)) % 48.68/48.93 (define @t26 () (|tptp.'fps_exp$'| @t2)) % 48.68/48.93 (define @t27 () (@var "A__questionmark_v3" |tptp.'Real_fps_set$'|)) % 48.68/48.93 (define @t28 () (@var "A__questionmark_v1" |tptp.'Real_fps_set$'|)) % 48.68/48.93 (define @t29 () (|tptp.'times$b'| @t28 @t27)) % 48.68/48.93 (define @t30 () (@var "A__questionmark_v2" |tptp.'Real_fps$'|)) % 48.68/48.93 (define @t31 () (|tptp.'fun_app$b'| @t14 @t30)) % 48.68/48.93 (define @t32 () (|tptp.'member$'| @t12 @t28)) % 48.68/48.93 (define @t33 () (@list @t12 @t28 @t30 @t27)) % 48.68/48.93 (define @t34 () (@var "A__questionmark_v3" |tptp.'Int_set$'|)) % 48.68/48.93 (define @t35 () (@var "A__questionmark_v1" |tptp.'Int_set$'|)) % 48.68/48.93 (define @t36 () (|tptp.'times$d'| @t35 @t34)) % 48.68/48.93 (define @t37 () (@var "A__questionmark_v2" Int)) % 48.68/48.93 (define @t38 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t6)) % 48.68/48.93 (define @t39 () (|tptp.'fun_app$a'| @t38 @t37)) % 48.68/48.93 (define @t40 () (|tptp.'member$a'| @t6 @t35)) % 48.68/48.93 (define @t41 () (@list @t6 @t35 @t37 @t34)) % 48.68/48.93 (define @t42 () (@var "A__questionmark_v3" |tptp.'Nat_set$'|)) % 48.68/48.93 (define @t43 () (@var "A__questionmark_v1" |tptp.'Nat_set$'|)) % 48.68/48.93 (define @t44 () (|tptp.'times$e'| @t43 @t42)) % 48.68/48.93 (define @t45 () (@var "A__questionmark_v2" |tptp.'Nat$'|)) % 48.68/48.93 (define @t46 () (|tptp.'fun_app$d'| @t19 @t45)) % 48.68/48.93 (define @t47 () (|tptp.'member$b'| @t18 @t43)) % 48.68/48.93 (define @t48 () (@list @t18 @t43 @t45 @t42)) % 48.68/48.93 (define @t49 () (@var "A__questionmark_v3" |tptp.'Real_set$'|)) % 48.68/48.93 (define @t50 () (@var "A__questionmark_v1" |tptp.'Real_set$'|)) % 48.68/48.93 (define @t51 () (|tptp.'times$g'| @t50 @t49)) % 48.68/48.93 (define @t52 () (@var "A__questionmark_v2" Real)) % 48.68/48.93 (define @t53 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t2)) % 48.68/48.93 (define @t54 () (|tptp.'fun_app$'| @t53 @t52)) % 48.68/48.93 (define @t55 () (|tptp.'member$c'| @t2 @t50)) % 48.68/48.93 (define @t56 () (@list @t2 @t50 @t52 @t49)) % 48.68/48.93 (define @t57 () (|tptp.'fun_app$b'| @t14 |tptp.'fps_X$'|)) % 48.68/48.93 (define @t58 () (|tptp.'fun_app$b'| @t10 @t12)) % 48.68/48.93 (define @t59 () (@var "A__questionmark_v2" |tptp.'Real_fps_set$'|)) % 48.68/48.93 (define @t60 () (@var "A__questionmark_v4" |tptp.'Real_fps$'|)) % 48.68/48.93 (define @t61 () (@var "A__questionmark_v3" |tptp.'Real_fps$'|)) % 48.68/48.93 (define @t62 () (@var "A__questionmark_v2" |tptp.'Int_set$'|)) % 48.68/48.93 (define @t63 () (@var "A__questionmark_v4" Int)) % 48.68/48.93 (define @t64 () (@var "A__questionmark_v3" Int)) % 48.68/48.93 (define @t65 () (@list @t64 @t63)) % 48.68/48.93 (define @t66 () (@var "A__questionmark_v2" |tptp.'Nat_set$'|)) % 48.68/48.93 (define @t67 () (@var "A__questionmark_v4" |tptp.'Nat$'|)) % 48.68/48.93 (define @t68 () (@var "A__questionmark_v3" |tptp.'Nat$'|)) % 48.68/48.93 (define @t69 () (@var "A__questionmark_v2" |tptp.'Real_set$'|)) % 48.68/48.93 (define @t70 () (@var "A__questionmark_v4" Real)) % 48.68/48.93 (define @t71 () (@var "A__questionmark_v3" Real)) % 48.68/48.93 (define @t72 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t71)) % 48.68/48.93 (define @t73 () (@list @t71 @t70)) % 48.68/48.93 (define @t74 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t1)) % 48.68/48.93 (define @t75 () (|tptp.'fun_app$'| @t74 @t52)) % 48.68/48.93 (define @t76 () (|tptp.'fun_app$'| @t53 @t75)) % 48.68/48.93 (define @t77 () (@list @t2 @t1 @t52)) % 48.68/48.93 (define @t78 () (|tptp.'fun_app$'| @t53 @t1)) % 48.68/48.93 (define @t79 () (|tptp.'fun_app$'| (|tptp.'fun_app$g'| |tptp.'times$f'| @t78) @t52)) % 48.68/48.93 (define @t80 () (@var "A__questionmark_v1" |tptp.'Real_fps$'|)) % 48.68/48.93 (define @t81 () (|tptp.'fun_app$c'| |tptp.'times$'| @t80)) % 48.68/48.93 (define @t82 () (|tptp.'fun_app$b'| @t81 @t30)) % 48.68/48.93 (define @t83 () (|tptp.'fun_app$b'| @t14 @t82)) % 48.68/48.93 (define @t84 () (@list @t12 @t80 @t30)) % 48.68/48.93 (define @t85 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t5)) % 48.68/48.93 (define @t86 () (|tptp.'fun_app$a'| @t85 @t37)) % 48.68/48.93 (define @t87 () (|tptp.'fun_app$a'| @t38 @t86)) % 48.68/48.93 (define @t88 () (@list @t6 @t5 @t37)) % 48.68/48.93 (define @t89 () (@var "A__questionmark_v1" |tptp.'Nat$'|)) % 48.68/48.93 (define @t90 () (|tptp.'fun_app$e'| |tptp.'times$a'| @t89)) % 48.68/48.93 (define @t91 () (|tptp.'fun_app$d'| @t90 @t45)) % 48.68/48.93 (define @t92 () (|tptp.'fun_app$d'| @t19 @t91)) % 48.68/48.93 (define @t93 () (@list @t18 @t89 @t45)) % 48.68/48.93 (define @t94 () (|tptp.'fun_app$b'| @t81 @t12)) % 48.68/48.93 (define @t95 () (|tptp.'fun_app$b'| @t14 @t80)) % 48.68/48.93 (define @t96 () (@list @t12 @t80)) % 48.68/48.93 (define @t97 () (|tptp.'fun_app$a'| @t85 @t6)) % 48.68/48.93 (define @t98 () (|tptp.'fun_app$a'| @t38 @t5)) % 48.68/48.93 (define @t99 () (|tptp.'fun_app$d'| @t90 @t18)) % 48.68/48.93 (define @t100 () (|tptp.'fun_app$d'| @t19 @t89)) % 48.68/48.93 (define @t101 () (@list @t18 @t89)) % 48.68/48.93 (define @t102 () (|tptp.'fun_app$'| @t74 @t2)) % 48.68/48.93 (define @t103 () (= @t2 1/1)) % 48.68/48.93 (define @t104 () (= @t6 1)) % 48.68/48.93 (define @t105 () (|tptp.'fps_const$'| @t1)) % 48.68/48.93 (define @t106 () (|tptp.'fun_app$c'| |tptp.'times$'| @t105)) % 48.68/48.93 (define @t107 () (|tptp.'fps_ginv$'| |tptp.'fps_X$'|)) % 48.68/48.93 (define @t108 () (|tptp.'minus$'| @t26 |tptp.'one$'|)) % 48.68/48.93 (define @t109 () (|tptp.'nat$'| 1)) % 48.68/48.93 (define @t110 () (= @t12 |tptp.'zero$'|)) % 48.68/48.93 (define @t111 () (not @t110)) % 48.68/48.93 (define @t112 () (|tptp.'fun_app$b'| |tptp.'fps_inv$'| @t108)) % 48.68/48.93 (define @t113 () (|tptp.'fps_compose$'| @t112 @t108)) % 48.68/48.93 (define @t114 () (= @t2 0/1)) % 48.68/48.93 (define @t115 () (not @t114)) % 48.68/48.93 (define @t116 () (=> @t115 (= @t113 |tptp.'fps_X$'|))) % 48.68/48.93 (define @t117 () (forall @t21 @t116)) % 48.68/48.93 (define @t118 () (= @t1 0/1)) % 48.68/48.93 (define @t119 () (or @t114 @t118)) % 48.68/48.93 (define @t120 () (= @t78 0/1)) % 48.68/48.93 (define @t121 () (forall @t4 (= @t120 @t119))) % 48.68/48.93 (define @t122 () (= @t1 @t52)) % 48.68/48.93 (define @t123 () (= @t78 @t54)) % 48.68/48.93 (define @t124 () (= @t2 @t52)) % 48.68/48.93 (define @t125 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t52)) % 48.68/48.93 (define @t126 () (|tptp.'fun_app$'| @t125 @t1)) % 48.68/48.93 (define @t127 () (= @t78 @t126)) % 48.68/48.93 (define @t128 () (|tptp.'fun_app$c'| |tptp.'times$'| @t30)) % 48.68/48.93 (define @t129 () (|tptp.'fun_app$b'| @t128 @t12)) % 48.68/48.93 (define @t130 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t37)) % 48.68/48.93 (define @t131 () (|tptp.'fun_app$a'| @t130 @t6)) % 48.68/48.93 (define @t132 () (|tptp.'fun_app$e'| |tptp.'times$a'| @t45)) % 48.68/48.93 (define @t133 () (|tptp.'fun_app$d'| @t132 @t18)) % 48.68/48.93 (define @t134 () (|tptp.'fun_app$'| @t125 @t2)) % 48.68/48.93 (define @t135 () (@var "A__questionmark_v0" |tptp.'Real_set$'|)) % 48.68/48.93 (define @t136 () (@var "A__questionmark_v0" |tptp.'Int_set$'|)) % 48.68/48.93 (define @t137 () (|tptp.'fps_const$'| @t2)) % 48.68/48.93 (define @t138 () (|tptp.'fps_const$a'| @t80)) % 48.68/48.93 (define @t139 () (|tptp.'fps_const$a'| @t12)) % 48.68/48.93 (define @t140 () (|tptp.'fps_const$b'| @t5)) % 48.68/48.93 (define @t141 () (|tptp.'fps_const$b'| @t6)) % 48.68/48.93 (define @t142 () (|tptp.'fps_const$c'| @t89)) % 48.68/48.93 (define @t143 () (|tptp.'fps_const$c'| @t18)) % 48.68/48.93 (define @t144 () (|tptp.'fun_app$c'| |tptp.'times$'| @t137)) % 48.68/48.93 (define @t145 () (|tptp.'fps_const$'| 0/1)) % 48.68/48.93 (define @t146 () (|tptp.'fps_const$'| 1/1)) % 48.68/48.93 (define @t147 () (|tptp.'fps_exp$'| 0/1)) % 48.68/48.93 (define @t148 () (= @t1 1/1)) % 48.68/48.93 (define @t149 () (= @t6 @t5)) % 48.68/48.93 (define @t150 () (= @t7 (- @t37 @t64))) % 48.68/48.93 (define @t151 () (@list @t6 @t5 @t37 @t64)) % 48.68/48.93 (define @t152 () (- @t6 @t37)) % 48.68/48.93 (define @t153 () (= @t6 0)) % 48.68/48.93 (define @t154 () (= 0 @t6)) % 48.68/48.93 (define @t155 () (= 0/1 @t2)) % 48.68/48.93 (define @t156 () (not @t153)) % 48.68/48.93 (define @t157 () (- @t1 @t52)) % 48.68/48.93 (define @t158 () (= @t102 @t134)) % 48.68/48.93 (define @t159 () (|tptp.'fun_app$c'| |tptp.'times$'| |tptp.'zero$'|)) % 48.68/48.93 (define @t160 () (|tptp.'fun_app$b'| @t159 @t30)) % 48.68/48.93 (define @t161 () (@var "A__questionmark_v0" tptp.tlbool)) % 48.68/48.93 (define @t162 () (= @t161 tptp.tltrue)) % 48.68/48.93 (define @t163 () (not @t162)) % 48.68/48.93 (define @t164 () (|tptp.'fun_app$f'| |tptp.'times$c'| 0)) % 48.68/48.93 (define @t165 () (|tptp.'fun_app$a'| @t164 @t37)) % 48.68/48.93 (define @t166 () (|tptp.'fun_app$e'| |tptp.'times$a'| |tptp.'zero$b'|)) % 48.68/48.93 (define @t167 () (|tptp.'fun_app$d'| @t166 @t45)) % 48.68/48.93 (define @t168 () (|tptp.'fun_app$g'| |tptp.'times$f'| 0/1)) % 48.68/48.93 (define @t169 () (|tptp.'fun_app$'| @t168 @t52)) % 48.68/48.93 (define @t170 () (|tptp.'fun_app$b'| @t14 |tptp.'zero$'|)) % 48.68/48.93 (define @t171 () (= @t170 |tptp.'zero$'|)) % 48.68/48.93 (define @t172 () (@var "A__questionmark_v1" tptp.tlbool)) % 48.68/48.93 (define @t173 () (= @t172 tptp.tltrue)) % 48.68/48.93 (define @t174 () (not @t173)) % 48.68/48.93 (define @t175 () (|tptp.'fun_app$a'| @t38 0)) % 48.68/48.93 (define @t176 () (|tptp.'fun_app$d'| @t19 |tptp.'zero$b'|)) % 48.68/48.93 (define @t177 () (= @t176 |tptp.'zero$b'|)) % 48.68/48.93 (define @t178 () (|tptp.'fun_app$'| @t53 0/1)) % 48.68/48.93 (define @t179 () (|tptp.'fps_compose$'| @t80 @t30)) % 48.68/48.93 (define @t180 () (|tptp.'minus$'| @t12 @t80)) % 48.68/48.93 (define @t181 () (|tptp.'fun_app$b'| @t144 @t80)) % 48.68/48.93 (define @t182 () (|tptp.'fps_const$'| @t52)) % 48.68/48.93 (define @t183 () (|tptp.'fps_compose$'| @t12 @t80)) % 48.68/48.93 (define @t184 () (or @t110 (= @t80 |tptp.'one$'|))) % 48.68/48.93 (define @t185 () (= @t5 1)) % 48.68/48.93 (define @t186 () (or @t153 @t185)) % 48.68/48.93 (define @t187 () (or @t114 @t148)) % 48.68/48.93 (define @t188 () (= @t12 |tptp.'one$'|)) % 48.68/48.93 (define @t189 () (= @t80 |tptp.'zero$'|)) % 48.68/48.93 (define @t190 () (= @t5 0)) % 48.68/48.93 (define @t191 () (forall @t13 @t171)) % 48.68/48.93 (define @t192 () (or @t110 @t189)) % 48.68/48.93 (define @t193 () (= @t95 |tptp.'zero$'|)) % 48.68/48.93 (define @t194 () (or @t153 @t190)) % 48.68/48.93 (define @t195 () (= @t98 0)) % 48.68/48.93 (define @t196 () (= @t89 |tptp.'zero$b'|)) % 48.68/48.93 (define @t197 () (= @t18 |tptp.'zero$b'|)) % 48.68/48.93 (define @t198 () (or @t197 @t196)) % 48.68/48.93 (define @t199 () (= @t100 |tptp.'zero$b'|)) % 48.68/48.93 (define @t200 () (= @t80 @t30)) % 48.68/48.93 (define @t201 () (= @t95 @t31)) % 48.68/48.93 (define @t202 () (= @t5 @t37)) % 48.68/48.93 (define @t203 () (= @t98 @t39)) % 48.68/48.93 (define @t204 () (= @t89 @t45)) % 48.68/48.93 (define @t205 () (= @t100 @t46)) % 48.68/48.93 (define @t206 () (or @t114 @t122)) % 48.68/48.93 (define @t207 () (|tptp.'fun_app$a'| @t130 @t5)) % 48.68/48.93 (define @t208 () (|tptp.'fun_app$d'| @t132 @t89)) % 48.68/48.93 (define @t209 () (or @t118 @t124)) % 48.68/48.93 (define @t210 () (not @t197)) % 48.68/48.93 (define @t211 () (not @t193)) % 48.68/48.93 (define @t212 () (and @t111 (not @t189))) % 48.68/48.93 (define @t213 () (not @t195)) % 48.68/48.93 (define @t214 () (not @t190)) % 48.68/48.93 (define @t215 () (and @t156 @t214)) % 48.68/48.93 (define @t216 () (not @t199)) % 48.68/48.93 (define @t217 () (and @t210 (not @t196))) % 48.68/48.93 (define @t218 () (not @t120)) % 48.68/48.93 (define @t219 () (not @t118)) % 48.68/48.93 (define @t220 () (and @t115 @t219)) % 48.68/48.93 (define @t221 () (= 0/1 1/1)) % 48.68/48.93 (define @t222 () (- @t5 @t37)) % 48.68/48.93 (define @t223 () (|tptp.'fun_app$'| @t72 @t2)) % 48.68/48.93 (define @t224 () (= @t52 0/1)) % 48.68/48.93 (define @t225 () (@list @t2 @t1 @t52 @t71)) % 48.68/48.93 (define @t226 () (|tptp.'fun_app$b'| @t159 @t80)) % 48.68/48.93 (define @t227 () (|tptp.'fun_app$b'| @t22 @t80)) % 48.68/48.93 (define @t228 () (|tptp.'fun_app$a'| @t164 @t5)) % 48.68/48.93 (define @t229 () (|tptp.'fun_app$a'| (|tptp.'fun_app$f'| |tptp.'times$c'| 1) @t5)) % 48.68/48.93 (define @t230 () (|tptp.'fun_app$d'| @t166 @t89)) % 48.68/48.93 (define @t231 () (|tptp.'fun_app$d'| @t23 @t89)) % 48.68/48.93 (define @t232 () (|tptp.'fun_app$'| @t168 @t1)) % 48.68/48.93 (define @t233 () (|tptp.'fun_app$g'| |tptp.'times$f'| 1/1)) % 48.68/48.93 (define @t234 () (|tptp.'fun_app$'| @t233 @t1)) % 48.68/48.93 (define @t235 () (|tptp.'fps_ln$'| @t2)) % 48.68/48.93 (define @t236 () (=> @t115 (= @t235 @t112))) % 48.68/48.93 (define @t237 () (forall @t21 @t236)) % 48.68/48.93 (define @t238 () (|tptp.'of_nat$'| @t89)) % 48.68/48.93 (define @t239 () (= @t238 1)) % 48.68/48.93 (define @t240 () (|tptp.'of_nat$'| @t18)) % 48.68/48.93 (define @t241 () (= @t240 1)) % 48.68/48.93 (define @t242 () (and @t241 @t239)) % 48.68/48.93 (define @t243 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t240)) % 48.68/48.93 (define @t244 () (|tptp.'fun_app$a'| @t243 @t238)) % 48.68/48.93 (define @t245 () (|tptp.'minus$'| @t9 |tptp.'one$'|)) % 48.68/48.93 (define @t246 () (|tptp.'fun_app$b'| (|tptp.'fun_app$c'| |tptp.'times$'| |tptp.'bernoulli_fps$'|) @t245)) % 48.68/48.93 (define @t247 () (= @t238 0)) % 48.68/48.93 (define @t248 () (= @t240 0)) % 48.68/48.93 (define @t249 () (< 0 @t240)) % 48.68/48.93 (define @t250 () (= 0 0)) % 48.68/48.93 (define @t251 () (< @t240 @t240)) % 48.68/48.93 (define @t252 () (|tptp.'of_nat$'| @t45)) % 48.68/48.93 (define @t253 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t252)) % 48.68/48.93 (define @t254 () (|tptp.'fun_app$a'| @t253 @t238)) % 48.68/48.93 (define @t255 () (= @t238 @t252)) % 48.68/48.93 (define @t256 () (|tptp.'fun_app$a'| @t243 @t252)) % 48.68/48.93 (define @t257 () (= @t244 @t256)) % 48.68/48.93 (define @t258 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t238)) % 48.68/48.93 (define @t259 () (|tptp.'fun_app$a'| @t258 @t252)) % 48.68/48.93 (define @t260 () (- @t256 @t259)) % 48.68/48.93 (define @t261 () (- @t240 @t238)) % 48.68/48.93 (define @t262 () (|tptp.'fun_app$a'| (|tptp.'fun_app$f'| |tptp.'times$c'| @t261) @t252)) % 48.68/48.93 (define @t263 () (< @t256 @t259)) % 48.68/48.93 (define @t264 () (not @t263)) % 48.68/48.93 (define @t265 () (< @t240 @t238)) % 48.68/48.93 (define @t266 () (not @t265)) % 48.68/48.93 (define @t267 () (|tptp.'fun_app$a'| @t164 @t252)) % 48.68/48.93 (define @t268 () (- @t244 @t256)) % 48.68/48.93 (define @t269 () (- @t238 @t252)) % 48.68/48.93 (define @t270 () (|tptp.'fun_app$a'| @t243 @t269)) % 48.68/48.93 (define @t271 () (< @t244 @t256)) % 48.68/48.93 (define @t272 () (not @t271)) % 48.68/48.93 (define @t273 () (< @t238 @t252)) % 48.68/48.93 (define @t274 () (not @t273)) % 48.68/48.93 (define @t275 () (|tptp.'fun_app$a'| @t243 0)) % 48.68/48.93 (define @t276 () (< @t240 0)) % 48.68/48.93 (define @t277 () (= 0 @t240)) % 48.68/48.93 (define @t278 () (not @t248)) % 48.68/48.93 (define @t279 () (= @t240 @t238)) % 48.68/48.93 (define @t280 () (- @t238 @t240)) % 48.68/48.93 (define @t281 () (= @t280 0)) % 48.68/48.93 (define @t282 () (< @t238 @t240)) % 48.68/48.93 (define @t283 () (not @t282)) % 48.68/48.93 (define @t284 () (=> @t266 (= @t261 0))) % 48.68/48.93 (define @t285 () (=> @t265 @t250)) % 48.68/48.93 (define @t286 () (|tptp.'fps_nth_deriv$'| @t18 |tptp.'fps_X$'|)) % 48.68/48.93 (define @t287 () (not @t241)) % 48.68/48.93 (define @t288 () (|tptp.'fps_shift$'| @t18 |tptp.'fps_X$'|)) % 48.68/48.93 (define @t289 () (<= 1 @t240)) % 48.68/48.93 (define @t290 () (|tptp.'fps_compose$'| @t30 @t12)) % 48.68/48.93 (define @t291 () (|tptp.'fun_app$b'| (|tptp.'fps_ginv$'| @t80) @t12)) % 48.68/48.93 (define @t292 () (|tptp.'fps_nth$'| @t80)) % 48.68/48.93 (define @t293 () (|tptp.'nat$'| 0)) % 48.68/48.93 (define @t294 () (|tptp.'fun_app$i'| @t292 @t293)) % 48.68/48.93 (define @t295 () (= @t294 0/1)) % 48.68/48.93 (define @t296 () (|tptp.'fps_nth$'| @t12)) % 48.68/48.93 (define @t297 () (= (|tptp.'fun_app$i'| @t296 @t109) 0/1)) % 48.68/48.93 (define @t298 () (not @t297)) % 48.68/48.93 (define @t299 () (|tptp.'fun_app$i'| @t296 @t293)) % 48.68/48.93 (define @t300 () (= @t299 0/1)) % 48.68/48.93 (define @t301 () (|tptp.'divide$a'| @t2)) % 48.68/48.93 (define @t302 () (|tptp.'divide$b'| @t6)) % 48.68/48.93 (define @t303 () (<= 0 @t240)) % 48.68/48.93 (define @t304 () (and (=> @t282 (< @t238 0)) (=> @t283 (< @t238 @t280)))) % 48.68/48.93 (define @t305 () (<= @t240 @t238)) % 48.68/48.93 (define @t306 () (<= @t5 @t6)) % 48.68/48.93 (define @t307 () (<= @t1 @t2)) % 48.68/48.93 (define @t308 () (|tptp.'divide$a'| @t102)) % 48.68/48.93 (define @t309 () (|tptp.'divide$b'| @t97)) % 48.68/48.93 (define @t310 () (|tptp.'divide$a'| @t78)) % 48.68/48.93 (define @t311 () (|tptp.'divide$b'| @t98)) % 48.68/48.93 (define @t312 () (|tptp.'fun_app$'| @t301 @t2)) % 48.68/48.93 (define @t313 () (=> @t115 (= @t312 1/1))) % 48.68/48.93 (define @t314 () (and @t285 @t284)) % 48.68/48.93 (define @t315 () (@var "A__questionmark_v1" |tptp.'Int_fps$'|)) % 48.68/48.93 (define @t316 () (|tptp.'fps_nth$a'| @t315 @t45)) % 48.68/48.93 (define @t317 () (@var "A__questionmark_v0" |tptp.'Int_fps$'|)) % 48.68/48.93 (define @t318 () (|tptp.'fps_nth$a'| @t317 @t45)) % 48.68/48.93 (define @t319 () (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| @t183) @t293)) % 48.68/48.93 (define @t320 () (= @t319 @t299)) % 48.68/48.93 (define @t321 () (forall @t96 @t320)) % 48.68/48.93 (define @t322 () (@var "A__questionmark_v1" |tptp.'Real_fps_fps$'|)) % 48.68/48.93 (define @t323 () (@var "A__questionmark_v0" |tptp.'Real_fps_fps$'|)) % 48.68/48.93 (define @t324 () (|tptp.'fps_nth$b'| @t323 @t293)) % 48.68/48.93 (define @t325 () (|tptp.'fun_app$c'| |tptp.'times$'| @t324)) % 48.68/48.93 (define @t326 () (|tptp.'times$h'| @t323 @t322)) % 48.68/48.93 (define @t327 () (|tptp.'fps_nth$a'| @t315 @t293)) % 48.68/48.93 (define @t328 () (|tptp.'fps_nth$a'| @t317 @t293)) % 48.68/48.93 (define @t329 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t328)) % 48.68/48.93 (define @t330 () (|tptp.'times$i'| @t317 @t315)) % 48.68/48.93 (define @t331 () (@var "A__questionmark_v1" |tptp.'Nat_fps$'|)) % 48.68/48.93 (define @t332 () (@var "A__questionmark_v0" |tptp.'Nat_fps$'|)) % 48.68/48.93 (define @t333 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t299)) % 48.68/48.93 (define @t334 () (|tptp.'fps_nth$a'| @t141 @t89)) % 48.68/48.93 (define @t335 () (not @t247)) % 48.68/48.93 (define @t336 () (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| @t137) @t89)) % 48.68/48.93 (define @t337 () (= @t336 0/1)) % 48.68/48.93 (define @t338 () (=> @t335 @t337)) % 48.68/48.93 (define @t339 () (= @t336 @t2)) % 48.68/48.93 (define @t340 () (=> @t247 @t339)) % 48.68/48.93 (define @t341 () (and @t340 @t338)) % 48.68/48.93 (define @t342 () (@list @t2 @t89)) % 48.68/48.93 (define @t343 () (forall @t342 @t341)) % 48.68/48.93 (define @t344 () (|tptp.'fps_nth$a'| |tptp.'one$b'| @t18)) % 48.68/48.93 (define @t345 () (|tptp.'fps_nth$'| |tptp.'one$'|)) % 48.68/48.93 (define @t346 () (|tptp.'fun_app$i'| @t345 @t18)) % 48.68/48.93 (define @t347 () (|tptp.'fps_nth$a'| |tptp.'fps_X$a'| @t18)) % 48.68/48.93 (define @t348 () (|tptp.'fps_nth$'| |tptp.'fps_X$'|)) % 48.68/48.93 (define @t349 () (|tptp.'fun_app$i'| @t348 @t18)) % 48.68/48.93 (define @t350 () (not @t300)) % 48.68/48.93 (define @t351 () (= @t328 0)) % 48.68/48.93 (define @t352 () (@list @t317)) % 48.68/48.93 (define @t353 () (forall @t13 (= (|tptp.'fps_compose$'| @t12 |tptp.'zero$'|) (|tptp.'fps_const$'| @t299)))) % 48.68/48.93 (define @t354 () (- @t238 1)) % 48.68/48.93 (define @t355 () (|tptp.'nat$'| @t354)) % 48.68/48.93 (define @t356 () (|tptp.'fps_nth$a'| @t317 @t355)) % 48.68/48.93 (define @t357 () (|tptp.'fps_nth$a'| (|tptp.'times$i'| |tptp.'fps_X$a'| @t317) @t89)) % 48.68/48.93 (define @t358 () (< @t238 1)) % 48.68/48.93 (define @t359 () (not @t358)) % 48.68/48.93 (define @t360 () (@list @t317 @t89)) % 48.68/48.93 (define @t361 () (|tptp.'fun_app$i'| @t296 @t355)) % 48.68/48.93 (define @t362 () (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| @t58) @t89)) % 48.68/48.93 (define @t363 () (= @t362 @t361)) % 48.68/48.93 (define @t364 () (=> @t359 @t363)) % 48.68/48.93 (define @t365 () (= @t362 @t299)) % 48.68/48.93 (define @t366 () (=> @t358 @t365)) % 48.68/48.93 (define @t367 () (and @t366 @t364)) % 48.68/48.93 (define @t368 () (=> @t335 @t367)) % 48.68/48.93 (define @t369 () (= @t362 0/1)) % 48.68/48.93 (define @t370 () (=> @t247 @t369)) % 48.68/48.93 (define @t371 () (and @t370 @t368)) % 48.68/48.93 (define @t372 () (@list @t12 @t89)) % 48.68/48.93 (define @t373 () (forall @t372 @t371)) % 48.68/48.93 (define @t374 () (|tptp.'fps_nth$a'| (|tptp.'times$i'| @t317 |tptp.'fps_X$a'|) @t89)) % 48.68/48.93 (define @t375 () (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| @t57) @t89)) % 48.68/48.93 (define @t376 () (- @t252 @t240)) % 48.68/48.93 (define @t377 () (- @t252 @t238)) % 48.68/48.93 (define @t378 () (< @t252 @t240)) % 48.68/48.93 (define @t379 () (not @t378)) % 48.68/48.93 (define @t380 () (< @t252 @t238)) % 48.68/48.93 (define @t381 () (<= 0 0)) % 48.68/48.93 (define @t382 () (and (=> @t378 @t381) (=> @t379 (<= 0 @t376)))) % 48.68/48.93 (define @t383 () (<= @t280 0)) % 48.68/48.93 (define @t384 () (and (=> @t273 @t381) (=> @t274 (<= 0 @t269)))) % 48.68/48.93 (define @t385 () (- @t240 @t252)) % 48.68/48.93 (define @t386 () (< @t240 @t252)) % 48.68/48.93 (define @t387 () (not @t386)) % 48.68/48.93 (define @t388 () (- @t280 @t376)) % 48.68/48.93 (define @t389 () (- @t280 0)) % 48.68/48.93 (define @t390 () (- 0 @t376)) % 48.68/48.93 (define @t391 () (- 0 0)) % 48.68/48.93 (define @t392 () (and (=> @t282 (and (=> @t378 (< 0 0)) (=> @t379 (< 0 @t376)))) (=> @t283 (and (=> @t378 (< @t280 0)) (=> @t379 (< @t280 @t376)))))) % 48.68/48.93 (define @t393 () (<= @t240 @t252)) % 48.68/48.93 (define @t394 () (and @t305 @t393)) % 48.68/48.93 (define @t395 () (- @t385 @t238)) % 48.68/48.93 (define @t396 () (- @t261 @t252)) % 48.68/48.93 (define @t397 () (- 0 @t238)) % 48.68/48.93 (define @t398 () (and (=> @t386 (< 0 @t238)) (=> @t387 (< @t385 @t238)))) % 48.68/48.93 (define @t399 () (not @t398)) % 48.68/48.93 (define @t400 () (- 0 @t252)) % 48.68/48.93 (define @t401 () (and (=> @t265 (< 0 @t252)) (=> @t266 (< @t261 @t252)))) % 48.68/48.93 (define @t402 () (<= @t238 @t252)) % 48.68/48.93 (define @t403 () (|tptp.'of_nat$'| @t68)) % 48.68/48.93 (define @t404 () (@var "A__questionmark_v0" |tptp.'Nat_bool_fun$'|)) % 48.68/48.93 (define @t405 () (@list @t67)) % 48.68/48.93 (define @t406 () (|tptp.'fun_app$h'| @t404 @t68)) % 48.68/48.93 (define @t407 () (@list @t68)) % 48.68/48.93 (define @t408 () (<= @t238 @t240)) % 48.68/48.93 (define @t409 () (<= @t37 @t64)) % 48.68/48.93 (define @t410 () (<= @t6 @t5)) % 48.68/48.93 (define @t411 () (<= @t52 @t71)) % 48.68/48.93 (define @t412 () (<= @t2 @t1)) % 48.68/48.93 (define @t413 () (<= @t240 0)) % 48.68/48.93 (define @t414 () (@list @t18 @t89 @t45 @t68)) % 48.68/48.93 (define @t415 () (|tptp.'fun_app$a'| @t243 @t240)) % 48.68/48.93 (define @t416 () (|tptp.'fps_compose$'| @t80 @t12)) % 48.68/48.93 (define @t417 () (|tptp.'less_eq$'| |tptp.'zero$b'|)) % 48.68/48.93 (define @t418 () (|tptp.'fun_app$h'| @t417 @t45)) % 48.68/48.93 (define @t419 () (|tptp.'less_eq$'| @t18)) % 48.68/48.93 (define @t420 () (|tptp.'fun_app$h'| @t419 @t89)) % 48.68/48.93 (define @t421 () (and @t420 @t418)) % 48.68/48.93 (define @t422 () (<= 0 @t37)) % 48.68/48.93 (define @t423 () (and @t410 @t422)) % 48.68/48.93 (define @t424 () (<= 0/1 @t52)) % 48.68/48.93 (define @t425 () (and @t412 @t424)) % 48.68/48.93 (define @t426 () (<= @t5 0)) % 48.68/48.93 (define @t427 () (<= @t6 0)) % 48.68/48.93 (define @t428 () (and @t427 @t426)) % 48.68/48.93 (define @t429 () (<= 0 @t5)) % 48.68/48.93 (define @t430 () (<= 0 @t6)) % 48.68/48.93 (define @t431 () (and @t430 @t429)) % 48.68/48.93 (define @t432 () (or @t431 @t428)) % 48.68/48.93 (define @t433 () (<= 0 @t98)) % 48.68/48.93 (define @t434 () (<= @t1 0/1)) % 48.68/48.93 (define @t435 () (<= @t2 0/1)) % 48.68/48.93 (define @t436 () (and @t435 @t434)) % 48.68/48.93 (define @t437 () (<= 0/1 @t1)) % 48.68/48.93 (define @t438 () (<= 0/1 @t2)) % 48.68/48.93 (define @t439 () (and @t438 @t437)) % 48.68/48.93 (define @t440 () (or @t439 @t436)) % 48.68/48.93 (define @t441 () (<= 0/1 @t78)) % 48.68/48.93 (define @t442 () (|tptp.'less_eq$'| @t99)) % 48.68/48.93 (define @t443 () (|tptp.'less_eq$'| @t89)) % 48.68/48.93 (define @t444 () (|tptp.'fun_app$h'| @t417 @t18)) % 48.68/48.93 (define @t445 () (and @t444 (|tptp.'fun_app$h'| @t443 |tptp.'zero$b'|))) % 48.68/48.93 (define @t446 () (and @t430 @t426)) % 48.68/48.93 (define @t447 () (and @t438 @t434)) % 48.68/48.93 (define @t448 () (|tptp.'less_eq$'| @t100)) % 48.68/48.93 (define @t449 () (|tptp.'fun_app$h'| @t448 |tptp.'zero$b'|)) % 48.68/48.93 (define @t450 () (|tptp.'fun_app$h'| @t417 @t89)) % 48.68/48.93 (define @t451 () (and (|tptp.'fun_app$h'| @t419 |tptp.'zero$b'|) @t450)) % 48.68/48.93 (define @t452 () (<= @t98 0)) % 48.68/48.93 (define @t453 () (and @t427 @t429)) % 48.68/48.93 (define @t454 () (<= @t78 0/1)) % 48.68/48.93 (define @t455 () (and @t435 @t437)) % 48.68/48.93 (define @t456 () (or @t446 @t453)) % 48.68/48.93 (define @t457 () (or @t447 @t455)) % 48.68/48.93 (define @t458 () (|tptp.'less_eq$'| @t46)) % 48.68/48.93 (define @t459 () (and @t410 (<= @t37 0))) % 48.68/48.93 (define @t460 () (and @t412 (<= @t52 0/1))) % 48.68/48.93 (define @t461 () (|tptp.'fun_app$a'| @t38 @t6)) % 48.68/48.93 (define @t462 () (|tptp.'fun_app$'| @t53 @t2)) % 48.68/48.93 (define @t463 () (|tptp.'fun_app$h'| @t458 (|tptp.'fun_app$d'| @t90 @t68))) % 48.68/48.93 (define @t464 () (|tptp.'fun_app$h'| (|tptp.'less_eq$'| @t45) @t68)) % 48.68/48.93 (define @t465 () (|tptp.'fun_app$a'| @t85 @t64)) % 48.68/48.93 (define @t466 () (<= @t39 @t465)) % 48.68/48.93 (define @t467 () (|tptp.'fun_app$'| @t74 @t71)) % 48.68/48.93 (define @t468 () (<= @t54 @t467)) % 48.68/48.93 (define @t469 () (not (= (|tptp.'fps_nth$a'| @t317 @t89) 0))) % 48.68/48.93 (define @t470 () (@list @t89)) % 48.68/48.93 (define @t471 () (not (= @t317 |tptp.'zero$a'|))) % 48.68/48.93 (define @t472 () (|tptp.'fun_app$i'| @t296 @t89)) % 48.68/48.93 (define @t473 () (not (= @t472 0/1))) % 48.68/48.93 (define @t474 () (|tptp.'divide$'| @t80 @t30)) % 48.68/48.93 (define @t475 () (|tptp.'fun_app$h'| @t419 |tptp.'one$a'|)) % 48.68/48.93 (define @t476 () (<= @t6 1)) % 48.68/48.93 (define @t477 () (<= @t2 1/1)) % 48.68/48.93 (define @t478 () (|tptp.'fun_app$h'| @t443 |tptp.'one$a'|)) % 48.68/48.93 (define @t479 () (<= @t5 1)) % 48.68/48.93 (define @t480 () (<= @t1 1/1)) % 48.68/48.93 (define @t481 () (and @t430 @t429 @t479)) % 48.68/48.93 (define @t482 () (and @t438 @t437 @t480)) % 48.68/48.93 (define @t483 () (@var "A__questionmark_v2" |tptp.'Int_fps$'|)) % 48.68/48.93 (define @t484 () (|tptp.'fps_compose$a'| @t315 @t317)) % 48.68/48.93 (define @t485 () (@list @t317 @t315 @t483)) % 48.68/48.93 (define @t486 () (|tptp.'fps_compose$a'| @t483 @t317)) % 48.68/48.93 (define @t487 () (and @t300 @t298)) % 48.68/48.93 (define @t488 () (@list @t80)) % 48.68/48.93 (define @t489 () (exists @t488 (= |tptp.'one$'| @t94))) % 48.68/48.93 (define @t490 () (exists @t488 (= |tptp.'one$'| @t95))) % 48.68/48.93 (define @t491 () (|tptp.'fun_app$b'| |tptp.'fps_inv$'| @t12)) % 48.68/48.93 (define @t492 () (|tptp.'fps_shift$'| @t18 (|tptp.'fun_app$b'| @t81 |tptp.'fps_X$'|))) % 48.68/48.93 (define @t493 () (< @t240 1)) % 48.68/48.93 (define @t494 () (@list @t322)) % 48.68/48.93 (define @t495 () (@list @t323)) % 48.68/48.93 (define @t496 () (@list @t5)) % 48.68/48.93 (define @t497 () (@list @t315)) % 48.68/48.93 (define @t498 () (@list @t1)) % 48.68/48.93 (define @t499 () (|tptp.'fps_compose$'| @t291 @t12)) % 48.68/48.93 (define @t500 () (=> @t487 (= @t499 @t80))) % 48.68/48.93 (define @t501 () (forall @t96 @t500)) % 48.68/48.93 (define @t502 () (|tptp.'divide$a'| 1/1)) % 48.68/48.93 (define @t503 () (|tptp.'fun_app$'| @t502 @t1)) % 48.68/48.93 (define @t504 () (|tptp.'fun_app$'| @t502 @t2)) % 48.68/48.93 (define @t505 () (|tptp.'fun_app$'| @t301 @t1)) % 48.68/48.93 (define @t506 () (|tptp.'fun_app$'| @t301 @t52)) % 48.68/48.93 (define @t507 () (|tptp.'divide$a'| @t52)) % 48.68/48.93 (define @t508 () (|tptp.'divide$a'| @t54)) % 48.68/48.93 (define @t509 () (|tptp.'fun_app$'| @t508 @t1)) % 48.68/48.93 (define @t510 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t505)) % 48.68/48.93 (define @t511 () (|tptp.'divide$a'| @t505)) % 48.68/48.93 (define @t512 () (|tptp.'fun_app$'| @t511 @t52)) % 48.68/48.93 (define @t513 () (|tptp.'divide$a'| @t1)) % 48.68/48.93 (define @t514 () (|tptp.'fun_app$'| @t513 @t52)) % 48.68/48.93 (define @t515 () (|tptp.'divide$b'| @t238)) % 48.68/48.93 (define @t516 () (|tptp.'fun_app$a'| @t515 @t252)) % 48.68/48.93 (define @t517 () (|tptp.'fun_app$a'| (|tptp.'divide$b'| @t244) @t256)) % 48.68/48.93 (define @t518 () (|tptp.'fun_app$'| @t310 @t54)) % 48.68/48.93 (define @t519 () (=> @t115 (= @t518 @t514))) % 48.68/48.93 (define @t520 () (and @t219 @t25)) % 48.68/48.93 (define @t521 () (= @t505 1/1)) % 48.68/48.93 (define @t522 () (= 1/1 @t505)) % 48.68/48.93 (define @t523 () (= @t1 @t2)) % 48.68/48.93 (define @t524 () (and @t219 @t523)) % 48.68/48.93 (define @t525 () (|tptp.'fun_app$'| @t507 @t71)) % 48.68/48.93 (define @t526 () (|tptp.'fun_app$'| @t53 @t71)) % 48.68/48.93 (define @t527 () (<= 0/1 @t505)) % 48.68/48.93 (define @t528 () (<= @t505 0/1)) % 48.68/48.93 (define @t529 () (|tptp.'fun_app$'| (|tptp.'divide$a'| @t71) @t1)) % 48.68/48.93 (define @t530 () (|tptp.'fun_app$'| @t507 @t2)) % 48.68/48.93 (define @t531 () (=> (not @t219) @t224)) % 48.68/48.93 (define @t532 () (not @t224)) % 48.68/48.93 (define @t533 () (=> (not @t532) @t114)) % 48.68/48.93 (define @t534 () (|tptp.'fun_app$'| @t513 @t2)) % 48.68/48.93 (define @t535 () (= @t534 @t52)) % 48.68/48.93 (define @t536 () (= @t1 @t134)) % 48.68/48.93 (define @t537 () (= @t1 @t530)) % 48.68/48.93 (define @t538 () (= @t102 @t52)) % 48.68/48.93 (define @t539 () (- @t2 @t514)) % 48.68/48.93 (define @t540 () (|tptp.'fun_app$'| (|tptp.'divide$a'| (- @t126 @t223)) @t78)) % 48.68/48.93 (define @t541 () (|tptp.'divide$'| @t95 @t31)) % 48.68/48.93 (define @t542 () (=> @t111 (= @t541 @t474))) % 48.68/48.93 (define @t543 () (|tptp.'divide$c'| @t89 @t45)) % 48.68/48.93 (define @t544 () (|tptp.'divide$c'| @t100 @t46)) % 48.68/48.93 (define @t545 () (=> @t210 (= @t544 @t543))) % 48.68/48.93 (define @t546 () (|tptp.'divide$b'| @t5)) % 48.68/48.93 (define @t547 () (|tptp.'fun_app$a'| @t546 @t37)) % 48.68/48.93 (define @t548 () (|tptp.'fun_app$a'| @t311 @t39)) % 48.68/48.93 (define @t549 () (=> @t156 (= @t548 @t547))) % 48.68/48.93 (define @t550 () (|tptp.'divide$b'| @t240)) % 48.68/48.93 (define @t551 () (|tptp.'fun_app$a'| @t550 @t238)) % 48.68/48.93 (define @t552 () (@var "A__questionmark_v5" |tptp.'Nat$'|)) % 48.68/48.93 (define @t553 () (@var "A__questionmark_v4" |tptp.'Nat_real_fun$'|)) % 48.68/48.93 (define @t554 () (|tptp.'fun_app$i'| @t553 @t552)) % 48.68/48.93 (define @t555 () (@var "A__questionmark_v1" |tptp.'Nat_real_fun_nat_real_fun_fun$'|)) % 48.68/48.93 (define @t556 () (|tptp.'fun_app$i'| (|tptp.'fun_app$k'| @t555 @t553) @t552)) % 48.68/48.93 (define @t557 () (@var "A__questionmark_v3" |tptp.'Nat_real_fun_nat_nat_fun_fun$'|)) % 48.68/48.93 (define @t558 () (|tptp.'of_nat$'| (|tptp.'fun_app$d'| (|tptp.'fun_app$l'| @t557 @t553) @t552))) % 48.68/48.93 (define @t559 () (= @t558 1)) % 48.68/48.93 (define @t560 () (@var "A__questionmark_v2" |tptp.'Nat_bool_fun$'|)) % 48.68/48.93 (define @t561 () (|tptp.'fun_app$h'| @t560 @t552)) % 48.68/48.93 (define @t562 () (@var "A__questionmark_v0" |tptp.'Nat_real_fun_bool_fun$'|)) % 48.68/48.93 (define @t563 () (|tptp.'fun_app$j'| @t562 @t553)) % 48.68/48.93 (define @t564 () (@list @t553 @t552)) % 48.68/48.93 (define @t565 () (= @t558 0)) % 48.68/48.93 (define @t566 () (@var "A__questionmark_v3" |tptp.'Nat_real_fun$'|)) % 48.68/48.93 (define @t567 () (|tptp.'fun_app$i'| @t566 @t67)) % 48.68/48.93 (define @t568 () (|tptp.'fun_app$j'| @t562 @t566)) % 48.68/48.93 (define @t569 () (@list @t566)) % 48.68/48.93 (define @t570 () (- @t5 @t6)) % 48.68/48.93 (define @t571 () (- @t1 @t2)) % 48.68/48.93 (define @t572 () (@var "A__questionmark_v7" Int)) % 48.68/48.93 (define @t573 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t572)) % 48.68/48.93 (define @t574 () (@var "A__questionmark_v5" Int)) % 48.68/48.93 (define @t575 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t574)) % 48.68/48.93 (define @t576 () (@var "A__questionmark_v6" Int)) % 48.68/48.93 (define @t577 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t576)) % 48.68/48.93 (define @t578 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t63)) % 48.68/48.93 (define @t579 () (@var "A__questionmark_v7" Real)) % 48.68/48.93 (define @t580 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t579)) % 48.68/48.93 (define @t581 () (@var "A__questionmark_v5" Real)) % 48.68/48.93 (define @t582 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t581)) % 48.68/48.93 (define @t583 () (@var "A__questionmark_v6" Real)) % 48.68/48.93 (define @t584 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t583)) % 48.68/48.93 (define @t585 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t70)) % 48.68/48.93 (define @t586 () (|tptp.'fun_app$a'| @t38 @t64)) % 48.68/48.93 (define @t587 () (<= @t64 0)) % 48.68/48.93 (define @t588 () (<= @t71 0/1)) % 48.68/48.93 (define @t589 () (- 1/1)) % 48.68/48.93 (define @t590 () (- @t2)) % 48.68/48.93 (define @t591 () (- @t1)) % 48.68/48.93 (define @t592 () (- @t6)) % 48.68/48.93 (define @t593 () (- @t5)) % 48.68/48.93 (define @t594 () (|tptp.'uminus$'| @t95)) % 48.68/48.93 (define @t595 () (|tptp.'uminus$'| @t80)) % 48.68/48.93 (define @t596 () (|tptp.'fun_app$b'| @t14 @t595)) % 48.68/48.93 (define @t597 () (- @t98)) % 48.68/48.93 (define @t598 () (|tptp.'fun_app$a'| @t38 @t593)) % 48.68/48.93 (define @t599 () (- @t78)) % 48.68/48.93 (define @t600 () (|tptp.'fun_app$'| @t53 @t591)) % 48.68/48.93 (define @t601 () (|tptp.'uminus$'| @t12)) % 48.68/48.93 (define @t602 () (|tptp.'fun_app$c'| |tptp.'times$'| @t601)) % 48.68/48.93 (define @t603 () (|tptp.'fun_app$f'| |tptp.'times$c'| @t592)) % 48.68/48.93 (define @t604 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t590)) % 48.68/48.93 (define @t605 () (|tptp.'fun_app$'| @t604 @t591)) % 48.68/48.93 (define @t606 () (= @t605 @t78)) % 48.68/48.93 (define @t607 () (forall @t4 @t606)) % 48.68/48.93 (define @t608 () (|tptp.'fun_app$b'| @t602 @t80)) % 48.68/48.93 (define @t609 () (|tptp.'fun_app$a'| @t603 @t5)) % 48.68/48.93 (define @t610 () (|tptp.'fun_app$'| @t604 @t1)) % 48.68/48.93 (define @t611 () (|tptp.'divide$b'| @t592)) % 48.68/48.93 (define @t612 () (<= 0/1 @t590)) % 48.68/48.93 (define @t613 () (|tptp.'uminus$'| |tptp.'one$'|)) % 48.68/48.93 (define @t614 () (- 1)) % 48.68/48.93 (define @t615 () (|tptp.'fps_exp$'| @t590)) % 48.68/48.93 (define @t616 () (|tptp.'uminus$'| |tptp.'fps_X$'|)) % 48.68/48.93 (define @t617 () (|tptp.'fps_compose$'| @t26 @t616)) % 48.68/48.93 (define @t618 () (= @t617 @t615)) % 48.68/48.93 (define @t619 () (forall @t21 @t618)) % 48.68/48.93 (define @t620 () (- @t505)) % 48.68/48.93 (define @t621 () (|tptp.'divide$a'| @t590)) % 48.68/48.93 (define @t622 () (= @t2 @t591)) % 48.68/48.93 (define @t623 () (|tptp.'fun_app$b'| @t14 @t12)) % 48.68/48.93 (define @t624 () (|tptp.'fun_app$'| @t74 @t1)) % 48.68/48.93 (define @t625 () (= @t2 @t589)) % 48.68/48.93 (define @t626 () (or @t103 @t625)) % 48.68/48.93 (define @t627 () (= @t462 1/1)) % 48.68/48.93 (define @t628 () (= @t627 @t626)) % 48.68/48.93 (define @t629 () (forall @t21 @t628)) % 48.68/48.93 (define @t630 () (- @t534)) % 48.68/48.93 (define @t631 () (|tptp.'elt_set_times$a'| @t614 @t35)) % 48.68/48.93 (define @t632 () (@list @t6 @t35)) % 48.68/48.93 (define @t633 () (|tptp.'elt_set_times$c'| @t589 @t50)) % 48.68/48.93 (define @t634 () (@list @t2 @t50)) % 48.68/48.93 (define @t635 () (- @t52)) % 48.68/48.93 (define @t636 () (- @t620 @t52)) % 48.68/48.93 (define @t637 () (- @t505 @t52)) % 48.68/48.93 (define @t638 () (= @t5 @t6)) % 48.68/48.93 (define @t639 () (<= @t37 @t6)) % 48.68/48.93 (define @t640 () (<= @t5 @t37)) % 48.68/48.93 (define @t641 () (<= @t37 @t5)) % 48.68/48.93 (define @t642 () (<= @t6 @t37)) % 48.68/48.93 (define @t643 () (and @t410 @t640)) % 48.68/48.93 (define @t644 () (<= @t52 @t2)) % 48.68/48.93 (define @t645 () (<= @t1 @t52)) % 48.68/48.93 (define @t646 () (<= @t52 @t1)) % 48.68/48.93 (define @t647 () (<= @t2 @t52)) % 48.68/48.93 (define @t648 () (and @t412 @t645)) % 48.68/48.93 (define @t649 () (and @t410 @t306)) % 48.68/48.93 (define @t650 () (and @t412 @t307)) % 48.68/48.93 (define @t651 () (@var "A__questionmark_v0" |tptp.'Int_int_bool_fun_fun$'|)) % 48.68/48.93 (define @t652 () (|tptp.'fun_app$m'| (|tptp.'fun_app$n'| @t651 @t64) @t63)) % 48.68/48.93 (define @t653 () (@var "A__questionmark_v0" |tptp.'Real_real_bool_fun_fun$'|)) % 48.68/48.93 (define @t654 () (|tptp.'fun_app$o'| (|tptp.'fun_app$p'| @t653 @t71) @t70)) % 48.68/48.93 (define @t655 () (|tptp.'of_nat$'| (|tptp.'nat$'| @t6))) % 48.68/48.93 (define @t656 () (= @t655 0)) % 48.68/48.93 (define @t657 () (not @t430)) % 48.68/48.93 (define @t658 () (=> @t657 @t656)) % 48.68/48.93 (define @t659 () (= @t655 @t6)) % 48.68/48.93 (define @t660 () (=> @t430 @t659)) % 48.68/48.93 (define @t661 () (and @t660 @t658)) % 48.68/48.93 (define @t662 () (forall @t17 @t661)) % 48.68/48.93 (define @t663 () (@var "B" tptp.tlbool)) % 48.68/48.93 (define @t664 () (@list |tptp.'fps_X$'|)) % 48.68/48.93 (define @t665 () (= |tptp.'fps_X$'| @t113)) % 48.68/48.93 (define @t666 () (not @t115)) % 48.68/48.93 (define @t667 () (|tptp.'fun_app$b'| |tptp.'fps_inv$'| @t245)) % 48.68/48.93 (define @t668 () (|tptp.'fps_compose$'| @t667 @t245)) % 48.68/48.93 (define @t669 () (= |tptp.'fps_X$'| @t668)) % 48.68/48.93 (define @t670 () (= 1/1 0/1)) % 48.68/48.93 (define @t671 () (or @t670 @t669)) % 48.68/48.93 (define @t672 () (forall @t21 (or @t114 @t665))) % 48.68/48.93 (define @t673 () (@list 1/1)) % 48.68/48.93 (define @t674 () (@list false)) % 48.68/48.93 (define @t675 () (= @t112 @t235)) % 48.68/48.93 (define @t676 () (|tptp.'fps_ln$'| 1/1)) % 48.68/48.93 (define @t677 () (= @t667 @t676)) % 48.68/48.93 (define @t678 () (or @t670 @t677)) % 48.68/48.93 (define @t679 () (forall @t21 (or @t114 @t675))) % 48.68/48.93 (define @t680 () (* -1/1 @t2)) % 48.68/48.93 (define @t681 () (|tptp.'fps_compose$'| @t147 @t616)) % 48.68/48.93 (define @t682 () (* -1/1 0/1)) % 48.68/48.93 (define @t683 () (|tptp.'fps_exp$'| @t682)) % 48.68/48.93 (define @t684 () (= @t681 @t683)) % 48.68/48.93 (define @t685 () (forall @t21 (= @t617 (|tptp.'fps_exp$'| @t680)))) % 48.68/48.93 (define @t686 () (= @t147 @t681)) % 48.68/48.93 (define @t687 () (|tptp.'fps_compose$'| @t9 |tptp.'zero$'|)) % 48.68/48.93 (define @t688 () (|tptp.'fps_nth$'| @t9)) % 48.68/48.93 (define @t689 () (|tptp.'fun_app$i'| @t688 @t293)) % 48.68/48.93 (define @t690 () (|tptp.'fps_const$'| @t689)) % 48.68/48.93 (define @t691 () (= @t687 @t690)) % 48.68/48.93 (define @t692 () (@list @t9)) % 48.68/48.93 (define @t693 () (= @t690 @t687)) % 48.68/48.93 (define @t694 () (>= @t6 0)) % 48.68/48.93 (define @t695 () (or @t694 @t656)) % 48.68/48.93 (define @t696 () (forall @t17 @t695)) % 48.68/48.93 (define @t697 () (@list @t6)) % 48.68/48.93 (define @t698 () (= @t6 @t655)) % 48.68/48.93 (define @t699 () (not @t694)) % 48.68/48.93 (define @t700 () (or @t699 @t698)) % 48.68/48.93 (define @t701 () (forall @t17 @t700)) % 48.68/48.93 (define @t702 () (@var "BOUND_VARIABLE_16144" Int)) % 48.68/48.93 (define @t703 () (and @t701 @t696)) % 48.68/48.93 (define @t704 () (and (=> @t694 @t698) (=> @t699 @t656))) % 48.68/48.93 (define @t705 () (|tptp.'of_nat$'| @t109)) % 48.68/48.93 (define @t706 () (= @t705 1)) % 48.68/48.93 (define @t707 () (* 1 (- @t705 1))) % 48.68/48.93 (define @t708 () (= 1 @t705)) % 48.68/48.93 (define @t709 () (>= 1 0)) % 48.68/48.93 (define @t710 () (not @t709)) % 48.68/48.93 (define @t711 () (or @t710 @t708)) % 48.68/48.93 (define @t712 () (forall (@list @t702) (or (not (>= @t702 0)) (= @t702 (|tptp.'of_nat$'| (|tptp.'nat$'| @t702)))))) % 48.68/48.93 (define @t713 () (@list @t712)) % 48.68/48.93 (define @t714 () (= @t80 @t499)) % 48.68/48.93 (define @t715 () (|tptp.'fun_app$b'| @t107 @t11)) % 48.68/48.93 (define @t716 () (|tptp.'fps_compose$'| @t715 @t11)) % 48.68/48.93 (define @t717 () (= |tptp.'fps_X$'| @t716)) % 48.68/48.93 (define @t718 () (+ -1 @t238)) % 48.68/48.93 (define @t719 () (= @t362 (|tptp.'fun_app$i'| @t296 (|tptp.'nat$'| @t718)))) % 48.68/48.93 (define @t720 () (>= @t238 1)) % 48.68/48.93 (define @t721 () (not @t720)) % 48.68/48.93 (define @t722 () (= @t299 @t362)) % 48.68/48.93 (define @t723 () (or @t247 (and (or @t720 @t722) (or @t721 @t719)))) % 48.68/48.93 (define @t724 () (forall @t372 @t723)) % 48.68/48.93 (define @t725 () (@list @t12 @t89)) % 48.68/48.93 (define @t726 () (or @t335 @t369)) % 48.68/48.93 (define @t727 () (forall @t372 @t726)) % 48.68/48.93 (define @t728 () (and @t727 @t724)) % 48.68/48.93 (define @t729 () (and (=> @t721 @t722) (=> @t720 @t719))) % 48.68/48.93 (define @t730 () (not @t335)) % 48.68/48.93 (define @t731 () (and @t370 (=> @t335 @t729))) % 48.68/48.93 (define @t732 () (* -1 1)) % 48.68/48.93 (define @t733 () (+ @t238 @t732)) % 48.68/48.93 (define @t734 () (|tptp.'of_nat$'| @t293)) % 48.68/48.93 (define @t735 () (= @t734 0)) % 48.68/48.93 (define @t736 () (= 0 @t734)) % 48.68/48.93 (define @t737 () (>= 0 0)) % 48.68/48.93 (define @t738 () (not @t737)) % 48.68/48.93 (define @t739 () (or @t738 @t736)) % 48.68/48.93 (define @t740 () (|tptp.'fps_nth$'| @t11)) % 48.68/48.93 (define @t741 () (= (|tptp.'fun_app$i'| @t740 @t293) 0/1)) % 48.68/48.93 (define @t742 () (not @t735)) % 48.68/48.93 (define @t743 () (or @t742 @t741)) % 48.68/48.93 (define @t744 () (@list false false)) % 48.68/48.93 (define @t745 () (|tptp.'fun_app$i'| @t740 @t109)) % 48.68/48.93 (define @t746 () (= @t745 0/1)) % 48.68/48.93 (define @t747 () (not @t741)) % 48.68/48.93 (define @t748 () (or @t747 @t746 @t717)) % 48.68/48.93 (define @t749 () (or @t247 @t337)) % 48.68/48.93 (define @t750 () (forall @t342 @t749)) % 48.68/48.93 (define @t751 () (@list @t2 @t89)) % 48.68/48.93 (define @t752 () (= @t2 @t336)) % 48.68/48.93 (define @t753 () (or @t335 @t752)) % 48.68/48.93 (define @t754 () (forall @t342 @t753)) % 48.68/48.93 (define @t755 () (@var "BOUND_VARIABLE_12609" |tptp.'Nat$'|)) % 48.68/48.93 (define @t756 () (@var "BOUND_VARIABLE_12607" Real)) % 48.68/48.93 (define @t757 () (and @t754 @t750)) % 48.68/48.93 (define @t758 () (and (=> @t247 @t752) @t338)) % 48.68/48.93 (define @t759 () (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| @t146) @t293)) % 48.68/48.93 (define @t760 () (= @t759 1/1)) % 48.68/48.93 (define @t761 () (= 1/1 @t759)) % 48.68/48.93 (define @t762 () (or @t742 @t761)) % 48.68/48.93 (define @t763 () (forall (@list @t756 @t755) (or (not (= (|tptp.'of_nat$'| @t755) 0)) (= @t756 (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| (|tptp.'fps_const$'| @t756)) @t755))))) % 48.68/48.93 (define @t764 () (or @t742 @t760)) % 48.68/48.93 (define @t765 () (= @t705 0)) % 48.68/48.93 (define @t766 () (+ -1 @t705)) % 48.68/48.93 (define @t767 () (|tptp.'nat$'| @t766)) % 48.68/48.93 (define @t768 () (|tptp.'fun_app$i'| @t688 @t767)) % 48.68/48.93 (define @t769 () (= @t745 @t768)) % 48.68/48.93 (define @t770 () (>= @t705 1)) % 48.68/48.93 (define @t771 () (not @t770)) % 48.68/48.93 (define @t772 () (or @t771 @t769)) % 48.68/48.93 (define @t773 () (= @t689 @t745)) % 48.68/48.93 (define @t774 () (or @t770 @t773)) % 48.68/48.93 (define @t775 () (and @t774 @t772)) % 48.68/48.93 (define @t776 () (or @t765 @t775)) % 48.68/48.93 (define @t777 () (@list true false)) % 48.68/48.93 (define @t778 () (not @t775)) % 48.68/48.93 (define @t779 () (@list @t775)) % 48.68/48.93 (define @t780 () (* -1/1 @t1)) % 48.68/48.93 (define @t781 () (|tptp.'fun_app$'| (|tptp.'fun_app$g'| |tptp.'times$f'| @t680) @t780)) % 48.68/48.93 (define @t782 () (= @t78 @t781)) % 48.68/48.93 (define @t783 () (* -1/1 1/1)) % 48.68/48.93 (define @t784 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t783)) % 48.68/48.93 (define @t785 () (|tptp.'fun_app$'| @t784 @t783)) % 48.68/48.93 (define @t786 () (|tptp.'fun_app$'| @t233 1/1)) % 48.68/48.93 (define @t787 () (= @t786 @t785)) % 48.68/48.93 (define @t788 () (forall @t4 @t782)) % 48.68/48.93 (define @t789 () (|tptp.'fun_app$'| (|tptp.'fun_app$g'| |tptp.'times$f'| -1/1) -1/1)) % 48.68/48.93 (define @t790 () (= @t786 @t789)) % 48.68/48.93 (define @t791 () (= @t789 0/1)) % 48.68/48.93 (define @t792 () (= -1/1 0/1)) % 48.68/48.93 (define @t793 () (or @t792 @t792)) % 48.68/48.93 (define @t794 () (= @t791 @t793)) % 48.68/48.93 (define @t795 () (not @t791)) % 48.68/48.93 (define @t796 () (= @t786 1/1)) % 48.68/48.93 (define @t797 () (= 1/1 -1/1)) % 48.68/48.93 (define @t798 () (= 1/1 1/1)) % 48.68/48.93 (define @t799 () (or @t798 @t797)) % 48.68/48.93 (define @t800 () (= @t796 @t799)) % 48.68/48.93 (define @t801 () (forall @t21 (= @t627 (or @t103 (= @t2 -1/1))))) % 48.68/48.93 (define @t802 () (not @t773)) % 48.68/48.93 (define @t803 () (not @t790)) % 48.68/48.93 (define @t804 () (not @t760)) % 48.68/48.93 (define @t805 () (|tptp.'fps_nth$'| @t687)) % 48.68/48.93 (define @t806 () (|tptp.'fun_app$i'| @t805 @t293)) % 48.68/48.93 (define @t807 () (= @t689 @t806)) % 48.68/48.93 (define @t808 () (not @t807)) % 48.68/48.93 (define @t809 () (|tptp.'fun_app$'| @t168 1/1)) % 48.68/48.93 (define @t810 () (|tptp.'fps_exp$'| @t809)) % 48.68/48.93 (define @t811 () (|tptp.'fun_app$c'| |tptp.'times$'| @t145)) % 48.68/48.93 (define @t812 () (|tptp.'fun_app$b'| @t811 |tptp.'fps_X$'|)) % 48.68/48.93 (define @t813 () (|tptp.'fps_compose$'| @t9 @t812)) % 48.68/48.93 (define @t814 () (= @t813 @t810)) % 48.68/48.93 (define @t815 () (not @t814)) % 48.68/48.93 (define @t816 () (not @t796)) % 48.68/48.93 (define @t817 () (not @t693)) % 48.68/48.93 (define @t818 () (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| @t676) @t293)) % 48.68/48.93 (define @t819 () (= @t818 0/1)) % 48.68/48.93 (define @t820 () (not @t819)) % 48.68/48.93 (define @t821 () (|tptp.'fun_app$i'| @t348 @t293)) % 48.68/48.93 (define @t822 () (|tptp.'fun_app$g'| |tptp.'times$f'| @t821)) % 48.68/48.93 (define @t823 () (|tptp.'fun_app$'| @t822 1/1)) % 48.68/48.93 (define @t824 () (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| (|tptp.'fun_app$b'| @t10 @t146)) @t293)) % 48.68/48.93 (define @t825 () (= @t824 @t823)) % 48.68/48.93 (define @t826 () (not @t825)) % 48.68/48.93 (define @t827 () (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| @t668) @t293)) % 48.68/48.93 (define @t828 () (|tptp.'fps_nth$'| @t667)) % 48.68/48.93 (define @t829 () (|tptp.'fun_app$i'| @t828 @t293)) % 48.68/48.93 (define @t830 () (= @t829 @t827)) % 48.68/48.93 (define @t831 () (not @t830)) % 48.68/48.93 (define @t832 () (|tptp.'fun_app$b'| @t159 |tptp.'fps_X$'|)) % 48.68/48.93 (define @t833 () (|tptp.'fun_app$b'| @t10 |tptp.'zero$'|)) % 48.68/48.93 (define @t834 () (= @t833 @t832)) % 48.68/48.93 (define @t835 () (not @t834)) % 48.68/48.93 (define @t836 () (not @t686)) % 48.68/48.93 (define @t837 () (not @t746)) % 48.68/48.93 (define @t838 () (not @t677)) % 48.68/48.93 (define @t839 () (= |tptp.'zero$'| @t833)) % 48.68/48.93 (define @t840 () (not @t839)) % 48.68/48.93 (define @t841 () (not @t669)) % 48.68/48.93 (define @t842 () (|tptp.'fun_app$b'| @t10 |tptp.'one$'|)) % 48.68/48.93 (define @t843 () (= |tptp.'fps_X$'| @t842)) % 48.68/48.93 (define @t844 () (not @t843)) % 48.68/48.93 (define @t845 () (= |tptp.'fps_X$'| @t246)) % 48.68/48.93 (define @t846 () (not @t845)) % 48.68/48.93 (define @t847 () (= |tptp.'one$'| @t147)) % 48.68/48.93 (define @t848 () (not @t847)) % 48.68/48.93 (define @t849 () (= |tptp.'one$'| @t146)) % 48.68/48.93 (define @t850 () (not @t849)) % 48.68/48.93 (define @t851 () (= |tptp.'zero$'| @t145)) % 48.68/48.93 (define @t852 () (not @t851)) % 48.68/48.93 (define @t853 () (|tptp.'fps_nth$'| @t681)) % 48.68/48.93 (define @t854 () (|tptp.'fun_app$i'| @t853 @t293)) % 48.68/48.93 (define @t855 () (= @t854 @t806)) % 48.68/48.93 (define @t856 () (|tptp.'fun_app$i'| @t345 @t293)) % 48.68/48.93 (define @t857 () (|tptp.'fps_nth$'| @t246)) % 48.68/48.93 (define @t858 () (|tptp.'fun_app$i'| @t857 @t293)) % 48.68/48.93 (define @t859 () (= @t858 @t823)) % 48.68/48.93 (define @t860 () (= 0/1 @t858)) % 48.68/48.93 (define @t861 () (|tptp.'fps_nth$'| @t690)) % 48.68/48.93 (define @t862 () (= @t858 @t827)) % 48.68/48.93 (define @t863 () (= @t829 @t818)) % 48.68/48.93 (define @t864 () (= @t858 @t824)) % 48.68/48.93 (define @t865 () (and @t851 @t849 @t847 @t845 @t843 @t669 @t839 @t677 @t746 @t686 @t834 @t830 @t825 @t819 @t693 @t796 @t814 @t795 @t807 @t760 @t790)) % 48.68/48.93 (define @t866 () (= 0 @t766)) % 48.68/48.93 (define @t867 () (= 1/1 @t854)) % 48.68/48.93 (define @t868 () (= 0/1 @t768)) % 48.68/48.93 (define @t869 () (= (* -1 (- 0 @t766)) @t707)) % 48.68/48.93 (define @t870 () (= @t866 @t706)) % 48.68/48.93 (define @t871 () (and @t866 @t851 @t847 @t845 @t839 @t860 @t867 @t834 @t686 @t859 @t814 @t693 @t868 @t807)) % 48.68/48.93 (assume @p1 (forall @t4 (= (|tptp.'fun_app$'| (|tptp.'uu$'| @t2) @t1) @t3))) % 48.68/48.93 (assume @p2 (forall @t8 (= (|tptp.'fun_app$a'| (|tptp.'uua$'| @t6) @t5) @t7))) % 48.68/48.93 (assume @p3 (not (= (|tptp.'fps_compose$'| |tptp.'fps_Lambert_W$'| @t11) |tptp.'fps_X$'|))) % 48.68/48.93 (assume @p4 (forall @t13 (= (|tptp.'fps_compose$'| @t12 |tptp.'fps_X$'|) @t12))) % 48.68/48.93 (assume @p5 @t16) % 48.68/48.93 (assume @p6 (forall @t17 (= (* @t6 1) @t6))) % 48.68/48.93 (assume @p7 (forall @t20 (= (|tptp.'fun_app$d'| @t19 |tptp.'one$a'|) @t18))) % 48.68/48.93 (assume @p8 (forall @t21 (= (* @t2 1/1) @t2))) % 48.68/48.93 (assume @p9 (forall @t21 (= (* 1/1 @t2) @t2))) % 48.68/48.93 (assume @p10 (forall @t13 (= (|tptp.'fun_app$b'| @t22 @t12) @t12))) % 48.68/48.93 (assume @p11 (forall @t17 (= (* 1 @t6) @t6))) % 48.68/48.93 (assume @p12 (forall @t20 (= (|tptp.'fun_app$d'| @t23 @t18) @t18))) % 48.68/48.93 (assume @p13 (= |tptp.'fps_Lambert_W$'| @t24)) % 48.68/48.93 (assume @p14 (forall @t4 (= (= @t26 (|tptp.'fps_exp$'| @t1)) @t25))) % 48.68/48.93 (assume @p15 (forall @t33 (=> (and @t32 (|tptp.'member$'| @t30 @t27)) (|tptp.'member$'| @t31 @t29)))) % 48.68/48.93 (assume @p16 (forall @t41 (=> (and @t40 (|tptp.'member$a'| @t37 @t34)) (|tptp.'member$a'| @t39 @t36)))) % 48.68/48.93 (assume @p17 (forall @t48 (=> (and @t47 (|tptp.'member$b'| @t45 @t42)) (|tptp.'member$b'| @t46 @t44)))) % 48.68/48.93 (assume @p18 (forall @t56 (=> (and @t55 (|tptp.'member$c'| @t52 @t49)) (|tptp.'member$c'| @t54 @t51)))) % 48.68/48.93 (assume @p19 (forall @t13 (= @t58 @t57))) % 48.68/48.93 (assume @p20 (forall @t13 (= (|tptp.'fps_compose$'| |tptp.'one$'| @t12) |tptp.'one$'|))) % 48.68/48.93 (assume @p21 (not (= |tptp.'fps_X$'| |tptp.'one$'|))) % 48.68/48.93 (assume @p22 (forall (@list @t12 @t28 @t59) (=> (and (|tptp.'member$'| @t12 (|tptp.'times$b'| @t28 @t59)) (forall (@list @t61 @t60) (=> (and (= @t12 (|tptp.'fun_app$b'| (|tptp.'fun_app$c'| |tptp.'times$'| @t61) @t60)) (|tptp.'member$'| @t61 @t28) (|tptp.'member$'| @t60 @t59)) false))) false))) % 48.68/48.93 (assume @p23 (forall (@list @t6 @t35 @t62) (=> (and (|tptp.'member$a'| @t6 (|tptp.'times$d'| @t35 @t62)) (forall @t65 (=> (and (= @t6 (|tptp.'fun_app$a'| (|tptp.'fun_app$f'| |tptp.'times$c'| @t64) @t63)) (|tptp.'member$a'| @t64 @t35) (|tptp.'member$a'| @t63 @t62)) false))) false))) % 48.68/48.93 (assume @p24 (forall (@list @t18 @t43 @t66) (=> (and (|tptp.'member$b'| @t18 (|tptp.'times$e'| @t43 @t66)) (forall (@list @t68 @t67) (=> (and (= @t18 (|tptp.'fun_app$d'| (|tptp.'fun_app$e'| |tptp.'times$a'| @t68) @t67)) (|tptp.'member$b'| @t68 @t43) (|tptp.'member$b'| @t67 @t66)) false))) false))) % 48.68/48.93 (assume @p25 (forall (@list @t2 @t50 @t69) (=> (and (|tptp.'member$c'| @t2 (|tptp.'times$g'| @t50 @t69)) (forall @t73 (=> (and (= @t2 (|tptp.'fun_app$'| @t72 @t70)) (|tptp.'member$c'| @t71 @t50) (|tptp.'member$c'| @t70 @t69)) false))) false))) % 48.68/48.93 (assume @p26 (forall @t77 (= @t76 (|tptp.'fun_app$'| @t74 @t54)))) % 48.68/48.93 (assume @p27 (forall @t77 (= @t76 @t79))) % 48.68/48.93 (assume @p28 (forall @t84 (= @t83 (|tptp.'fun_app$b'| @t81 @t31)))) % 48.68/48.93 (assume @p29 (forall @t88 (= @t87 (|tptp.'fun_app$a'| @t85 @t39)))) % 48.68/48.93 (assume @p30 (forall @t93 (= @t92 (|tptp.'fun_app$d'| @t90 @t46)))) % 48.68/48.93 (assume @p31 (forall @t96 (= @t95 @t94))) % 48.68/48.93 (assume @p32 (forall @t8 (= @t98 @t97))) % 48.68/48.93 (assume @p33 (forall @t101 (= @t100 @t99))) % 48.68/48.93 (assume @p34 (forall @t4 (= @t78 @t102))) % 48.68/48.93 (assume @p35 (forall @t84 (= (|tptp.'fun_app$b'| (|tptp.'fun_app$c'| |tptp.'times$'| @t95) @t30) @t83))) % 48.68/48.93 (assume @p36 (forall @t88 (= (|tptp.'fun_app$a'| (|tptp.'fun_app$f'| |tptp.'times$c'| @t98) @t37) @t87))) % 48.68/48.93 (assume @p37 (forall @t93 (= (|tptp.'fun_app$d'| (|tptp.'fun_app$e'| |tptp.'times$a'| @t100) @t45) @t92))) % 48.68/48.93 (assume @p38 (forall @t77 (= @t79 @t76))) % 48.68/48.93 (assume @p39 (forall @t21 (= (= 1/1 @t2) @t103))) % 48.68/48.93 (assume @p40 (forall @t17 (= (= 1 @t6) @t104))) % 48.68/48.93 (assume @p41 (forall @t4 (= (|tptp.'fps_compose$'| @t26 (|tptp.'fun_app$b'| @t106 |tptp.'fps_X$'|)) (|tptp.'fps_exp$'| @t102)))) % 48.68/48.93 (assume @p42 (= |tptp.'fps_inv$'| @t107)) % 48.68/48.93 (assume @p43 (forall @t21 (= (|tptp.'fps_compose$'| |tptp.'fps_X$'| @t26) @t108))) % 48.68/48.93 (assume @p44 (|tptp.'monoid$'| |tptp.'times$'| |tptp.'one$'|)) % 48.68/48.93 (assume @p45 (|tptp.'monoid$a'| |tptp.'times$c'| 1)) % 48.68/48.93 (assume @p46 (|tptp.'fun_app$h'| (|tptp.'monoid$b'| |tptp.'times$a'|) |tptp.'one$a'|)) % 48.68/48.93 (assume @p47 (|tptp.'monoid$c'| |tptp.'times$f'| 1/1)) % 48.68/48.93 (assume @p48 (forall @t33 (= (|tptp.'times$b'| (|tptp.'elt_set_times$'| @t12 @t28) (|tptp.'elt_set_times$'| @t30 @t27)) (|tptp.'elt_set_times$'| @t31 @t29)))) % 48.68/48.93 (assume @p49 (forall @t41 (= (|tptp.'times$d'| (|tptp.'elt_set_times$a'| @t6 @t35) (|tptp.'elt_set_times$a'| @t37 @t34)) (|tptp.'elt_set_times$a'| @t39 @t36)))) % 48.68/48.93 (assume @p50 (forall @t48 (= (|tptp.'times$e'| (|tptp.'elt_set_times$b'| @t18 @t43) (|tptp.'elt_set_times$b'| @t45 @t42)) (|tptp.'elt_set_times$b'| @t46 @t44)))) % 48.68/48.93 (assume @p51 (forall @t56 (= (|tptp.'times$g'| (|tptp.'elt_set_times$c'| @t2 @t50) (|tptp.'elt_set_times$c'| @t52 @t49)) (|tptp.'elt_set_times$c'| @t54 @t51)))) % 48.68/48.93 (assume @p52 (forall @t13 (= (|tptp.'fps_shift$'| @t109 @t57) @t12))) % 48.68/48.93 (assume @p53 (|tptp.'comm_monoid$'| |tptp.'times$'| |tptp.'one$'|)) % 48.68/48.93 (assume @p54 (|tptp.'comm_monoid$a'| |tptp.'times$c'| 1)) % 48.68/48.93 (assume @p55 (|tptp.'fun_app$h'| (|tptp.'comm_monoid$b'| |tptp.'times$a'|) |tptp.'one$a'|)) % 48.68/48.93 (assume @p56 (|tptp.'comm_monoid$c'| |tptp.'times$f'| 1/1)) % 48.68/48.93 (assume @p57 (forall @t13 (=> @t111 (not (= @t58 |tptp.'zero$'|))))) % 48.68/48.93 (assume @p58 (forall @t13 (=> @t111 (not (= @t57 |tptp.'zero$'|))))) % 48.68/48.93 (assume @p59 @t117) % 48.68/48.93 (assume @p60 (forall @t21 (=> @t115 (= (|tptp.'fps_compose$'| @t108 @t112) |tptp.'fps_X$'|)))) % 48.68/48.93 (assume @p61 @t121) % 48.68/48.93 (assume @p62 (forall @t21 (= (* 0/1 @t2) 0/1))) % 48.68/48.93 (assume @p63 (forall @t21 (= (* @t2 0/1) 0/1))) % 48.68/48.93 (assume @p64 (forall @t77 (= @t123 (or @t122 @t114)))) % 48.68/48.93 (assume @p65 (forall @t77 (= @t127 (or @t124 @t118)))) % 48.68/48.93 (assume @p66 (forall @t21 (= (- @t2 @t2) 0/1))) % 48.68/48.93 (assume @p67 (forall @t17 (= (- @t6 @t6) 0))) % 48.68/48.93 (assume @p68 (forall @t21 (= (- @t2 0/1) @t2))) % 48.68/48.93 (assume @p69 (forall @t17 (= (- @t6 0) @t6))) % 48.68/48.93 (assume @p70 (forall (@list @t12 @t28 @t30) (=> @t32 (|tptp.'member$'| @t129 (|tptp.'elt_set_times$'| @t30 @t28))))) % 48.68/48.93 (assume @p71 (forall (@list @t6 @t35 @t37) (=> @t40 (|tptp.'member$a'| @t131 (|tptp.'elt_set_times$a'| @t37 @t35))))) % 48.68/48.93 (assume @p72 (forall (@list @t18 @t43 @t45) (=> @t47 (|tptp.'member$b'| @t133 (|tptp.'elt_set_times$b'| @t45 @t43))))) % 48.68/48.93 (assume @p73 (forall (@list @t2 @t50 @t52) (=> @t55 (|tptp.'member$c'| @t134 (|tptp.'elt_set_times$c'| @t52 @t50))))) % 48.68/48.93 (assume @p74 (forall (@list @t135) (= (|tptp.'elt_set_times$c'| 1/1 @t135) @t135))) % 48.68/48.93 (assume @p75 (forall (@list @t136) (= (|tptp.'elt_set_times$a'| 1 @t136) @t136))) % 48.68/48.93 (assume @p76 (forall (@list @t2 @t80) (= (|tptp.'fps_compose$'| @t137 @t80) @t137))) % 48.68/48.93 (assume @p77 (forall @t13 (= (|tptp.'fps_compose$'| |tptp.'zero$'| @t12) |tptp.'zero$'|))) % 48.68/48.93 (assume @p78 (forall @t96 (= (|tptp.'times$h'| @t139 @t138) (|tptp.'fps_const$a'| @t95)))) % 48.68/48.93 (assume @p79 (forall @t8 (= (|tptp.'times$i'| @t141 @t140) (|tptp.'fps_const$b'| @t98)))) % 48.68/48.93 (assume @p80 (forall @t101 (= (|tptp.'times$j'| @t143 @t142) (|tptp.'fps_const$c'| @t100)))) % 48.68/48.93 (assume @p81 (forall @t4 (= (|tptp.'fun_app$b'| @t144 @t105) (|tptp.'fps_const$'| @t78)))) % 48.68/48.93 (assume @p82 (= (|tptp.'fps_const$b'| 0) |tptp.'zero$a'|)) % 48.68/48.93 (assume @p83 (= @t145 |tptp.'zero$'|)) % 48.68/48.93 (assume @p84 (= @t146 |tptp.'one$'|)) % 48.68/48.93 (assume @p85 (= (|tptp.'fps_const$b'| 1) |tptp.'one$b'|)) % 48.68/48.93 (assume @p86 (forall @t8 (= (|tptp.'minus$a'| @t141 @t140) (|tptp.'fps_const$b'| @t7)))) % 48.68/48.93 (assume @p87 (= @t147 |tptp.'one$'|)) % 48.68/48.93 (assume @p88 (forall @t21 (= (= @t26 |tptp.'one$'|) @t114))) % 48.68/48.93 (assume @p89 (forall @t4 (= (= @t26 @t105) (and @t114 @t148)))) % 48.68/48.93 (assume @p90 (forall @t151 (=> @t150 (= @t149 (= @t37 @t64))))) % 48.68/48.93 (assume @p91 (forall @t4 (= @t25 (= @t3 0/1)))) % 48.68/48.93 (assume @p92 (forall @t8 (= @t149 (= @t7 0)))) % 48.68/48.93 (assume @p93 (forall @t88 (= (- @t7 @t37) (- @t152 @t5)))) % 48.68/48.93 (assume @p94 (forall @t17 (= @t154 @t153))) % 48.68/48.93 (assume @p95 (forall @t21 (= @t155 @t114))) % 48.68/48.93 (assume @p96 (forall @t17 (=> @t156 (not (= @t141 |tptp.'zero$a'|))))) % 48.68/48.93 (assume @p97 (forall @t21 (=> @t115 (not (= @t137 |tptp.'zero$'|))))) % 48.68/48.93 (assume @p98 (forall @t77 (= (|tptp.'fun_app$'| (|tptp.'fun_app$g'| |tptp.'times$f'| @t3) @t52) (- @t54 @t75)))) % 48.68/48.93 (assume @p99 (forall @t77 (= (|tptp.'fun_app$'| @t53 @t157) (- @t78 @t54)))) % 48.68/48.93 (assume @p100 (forall @t21 (not (= |tptp.'fps_X$'| @t137)))) % 48.68/48.93 (assume @p101 (forall @t77 (=> (and @t115 @t123) @t122))) % 48.68/48.93 (assume @p102 (forall @t77 (=> (and @t115 @t158) @t122))) % 48.68/48.93 (assume @p103 (forall (@list @t161 @t80 @t30) (and (=> @t162 (and (=> @t162 (= @t82 @t82)) (=> @t163 (= @t82 |tptp.'zero$'|)))) (=> @t163 (and (=> @t162 (= @t160 @t82)) (=> @t163 (= @t160 |tptp.'zero$'|))))))) % 48.68/48.93 (assume @p104 (forall (@list @t161 @t5 @t37) (and (=> @t162 (and (=> @t162 (= @t86 @t86)) (=> @t163 (= @t86 0)))) (=> @t163 (and (=> @t162 (= @t165 @t86)) (=> @t163 (= @t165 0))))))) % 48.68/48.93 (assume @p105 (forall (@list @t161 @t89 @t45) (and (=> @t162 (and (=> @t162 (= @t91 @t91)) (=> @t163 (= @t91 |tptp.'zero$b'|)))) (=> @t163 (and (=> @t162 (= @t167 @t91)) (=> @t163 (= @t167 |tptp.'zero$b'|))))))) % 48.68/48.93 (assume @p106 (forall (@list @t161 @t1 @t52) (and (=> @t162 (and (=> @t162 (= @t75 @t75)) (=> @t163 (= @t75 0/1)))) (=> @t163 (and (=> @t162 (= @t169 @t75)) (=> @t163 (= @t169 0/1))))))) % 48.68/48.93 (assume @p107 (forall (@list @t12 @t172 @t30) (and (=> @t173 (and (=> @t173 (= @t31 @t31)) (=> @t174 (= @t31 |tptp.'zero$'|)))) (=> @t174 (and (=> @t173 (= @t170 @t31)) (=> @t174 @t171)))))) % 48.68/48.93 (assume @p108 (forall (@list @t6 @t172 @t37) (and (=> @t173 (and (=> @t173 (= @t39 @t39)) (=> @t174 (= @t39 0)))) (=> @t174 (and (=> @t173 (= @t175 @t39)) (=> @t174 (= @t175 0))))))) % 48.68/48.93 (assume @p109 (forall (@list @t18 @t172 @t45) (and (=> @t173 (and (=> @t173 (= @t46 @t46)) (=> @t174 (= @t46 |tptp.'zero$b'|)))) (=> @t174 (and (=> @t173 (= @t176 @t46)) (=> @t174 @t177)))))) % 48.68/48.93 (assume @p110 (forall (@list @t2 @t172 @t52) (and (=> @t173 (and (=> @t173 (= @t54 @t54)) (=> @t174 (= @t54 0/1)))) (=> @t174 (and (=> @t173 (= @t178 @t54)) (=> @t174 (= @t178 0/1))))))) % 48.68/48.93 (assume @p111 (forall @t84 (= (|tptp.'fps_compose$'| @t180 @t30) (|tptp.'minus$'| (|tptp.'fps_compose$'| @t12 @t30) @t179)))) % 48.68/48.93 (assume @p112 (not (= |tptp.'fps_X$'| |tptp.'zero$'|))) % 48.68/48.93 (assume @p113 (forall (@list @t12 @t80 @t59) (= (|tptp.'elt_set_times$'| @t12 (|tptp.'elt_set_times$'| @t80 @t59)) (|tptp.'elt_set_times$'| @t95 @t59)))) % 48.68/48.93 (assume @p114 (forall (@list @t6 @t5 @t62) (= (|tptp.'elt_set_times$a'| @t6 (|tptp.'elt_set_times$a'| @t5 @t62)) (|tptp.'elt_set_times$a'| @t98 @t62)))) % 48.68/48.93 (assume @p115 (forall (@list @t18 @t89 @t66) (= (|tptp.'elt_set_times$b'| @t18 (|tptp.'elt_set_times$b'| @t89 @t66)) (|tptp.'elt_set_times$b'| @t100 @t66)))) % 48.68/48.93 (assume @p116 (forall (@list @t2 @t1 @t69) (= (|tptp.'elt_set_times$c'| @t2 (|tptp.'elt_set_times$c'| @t1 @t69)) (|tptp.'elt_set_times$c'| @t78 @t69)))) % 48.68/48.93 (assume @p117 (forall @t21 (not (= @t26 |tptp.'zero$'|)))) % 48.68/48.93 (assume @p118 (forall (@list @t2 @t80 @t30) (= (|tptp.'fun_app$b'| @t144 @t179) (|tptp.'fps_compose$'| @t181 @t30)))) % 48.68/48.93 (assume @p119 (forall (@list @t12 @t80 @t52) (= (|tptp.'fun_app$b'| (|tptp.'fun_app$c'| |tptp.'times$'| @t183) @t182) (|tptp.'fps_compose$'| (|tptp.'fun_app$b'| (|tptp.'fun_app$c'| |tptp.'times$'| @t182) @t12) @t80)))) % 48.68/48.93 (assume @p120 (= (- 1/1 1/1) 0/1)) % 48.68/48.93 (assume @p121 (= (- 1 1) 0)) % 48.68/48.93 (assume @p122 (forall @t96 (= (= @t12 @t95) @t184))) % 48.68/48.93 (assume @p123 (forall @t8 (= (= @t6 @t98) @t186))) % 48.68/48.93 (assume @p124 (forall @t4 (= (= @t2 @t78) @t187))) % 48.68/48.93 (assume @p125 (forall @t96 (= (= @t95 @t12) @t184))) % 48.68/48.93 (assume @p126 (forall @t8 (= (= @t98 @t6) @t186))) % 48.68/48.93 (assume @p127 (forall @t4 (= (= @t78 @t2) @t187))) % 48.68/48.93 (assume @p128 (forall @t96 (= (= @t12 @t94) @t184))) % 48.68/48.93 (assume @p129 (forall @t8 (= (= @t6 @t97) @t186))) % 48.68/48.93 (assume @p130 (forall @t4 (= (= @t2 @t102) @t187))) % 48.68/48.93 (assume @p131 (forall @t96 (= (= @t95 @t80) (or @t189 @t188)))) % 48.68/48.93 (assume @p132 (forall @t8 (= (= @t98 @t5) (or @t190 @t104)))) % 48.68/48.93 (assume @p133 (forall @t4 (= (= @t78 @t1) (or @t118 @t103)))) % 48.68/48.93 (assume @p134 (forall @t13 (= (|tptp.'fun_app$b'| @t159 @t12) |tptp.'zero$'|))) % 48.68/48.93 (assume @p135 (forall @t17 (= (* 0 @t6) 0))) % 48.68/48.93 (assume @p136 (forall @t20 (= (|tptp.'fun_app$d'| @t166 @t18) |tptp.'zero$b'|))) % 48.68/48.93 (assume @p137 @t191) % 48.68/48.93 (assume @p138 (forall @t17 (= (* @t6 0) 0))) % 48.68/48.93 (assume @p139 (forall @t20 @t177)) % 48.68/48.93 (assume @p140 (forall @t96 (= @t193 @t192))) % 48.68/48.93 (assume @p141 (forall @t8 (= @t195 @t194))) % 48.68/48.93 (assume @p142 (forall @t101 (= @t199 @t198))) % 48.68/48.93 (assume @p143 (forall @t84 (= @t201 (or @t110 @t200)))) % 48.68/48.93 (assume @p144 (forall @t88 (= @t203 (or @t153 @t202)))) % 48.68/48.93 (assume @p145 (forall @t93 (= @t205 (or @t197 @t204)))) % 48.68/48.93 (assume @p146 (forall @t77 (= @t123 @t206))) % 48.68/48.93 (assume @p147 (forall @t84 (= (= @t95 (|tptp.'fun_app$b'| @t128 @t80)) (or @t189 (= @t12 @t30))))) % 48.68/48.93 (assume @p148 (forall @t88 (= (= @t98 @t207) (or @t190 (= @t6 @t37))))) % 48.68/48.93 (assume @p149 (forall @t93 (= (= @t100 @t208) (or @t196 (= @t18 @t45))))) % 48.68/48.93 (assume @p150 (forall @t77 (= @t127 @t209))) % 48.68/48.93 (assume @p151 (forall @t84 (=> @t111 (= (= @t94 @t129) @t200)))) % 48.68/48.93 (assume @p152 (forall @t88 (=> @t156 (= (= @t97 @t131) @t202)))) % 48.68/48.93 (assume @p153 (forall @t93 (=> @t210 (= (= @t99 @t133) @t204)))) % 48.68/48.93 (assume @p154 (forall @t77 (=> @t115 (= @t158 @t122)))) % 48.68/48.93 (assume @p155 (forall @t84 (=> @t111 (= @t201 @t200)))) % 48.68/48.93 (assume @p156 (forall @t88 (=> @t156 (= @t203 @t202)))) % 48.68/48.93 (assume @p157 (forall @t93 (=> @t210 (= @t205 @t204)))) % 48.68/48.93 (assume @p158 (forall @t77 (=> @t115 (= @t123 @t122)))) % 48.68/48.93 (assume @p159 (forall @t96 (=> @t212 @t211))) % 48.68/48.93 (assume @p160 (forall @t8 (=> @t215 @t213))) % 48.68/48.93 (assume @p161 (forall @t101 (=> @t217 @t216))) % 48.68/48.93 (assume @p162 (forall @t4 (=> @t220 @t218))) % 48.68/48.93 (assume @p163 (forall @t96 (=> @t193 @t192))) % 48.68/48.93 (assume @p164 (forall @t8 (=> @t195 @t194))) % 48.68/48.93 (assume @p165 (forall @t101 (=> @t199 @t198))) % 48.68/48.93 (assume @p166 (forall @t4 (=> @t120 @t119))) % 48.68/48.93 (assume @p167 (forall @t96 (=> @t211 @t212))) % 48.68/48.93 (assume @p168 (forall @t8 (=> @t213 @t215))) % 48.68/48.93 (assume @p169 (forall @t101 (=> @t216 @t217))) % 48.68/48.93 (assume @p170 (forall @t4 (=> @t218 @t220))) % 48.68/48.93 (assume @p171 (not (= 0 1))) % 48.68/48.93 (assume @p172 (not @t221)) % 48.68/48.93 (assume @p173 (forall @t84 (= (|tptp.'fun_app$b'| @t14 (|tptp.'minus$'| @t80 @t30)) (|tptp.'minus$'| @t95 @t31)))) % 48.68/48.93 (assume @p174 (forall @t88 (= (|tptp.'fun_app$a'| @t38 @t222) (- @t98 @t39)))) % 48.68/48.93 (assume @p175 (forall @t93 (= (|tptp.'fun_app$d'| @t19 (|tptp.'minus$b'| @t89 @t45)) (|tptp.'minus$b'| @t100 @t46)))) % 48.68/48.93 (assume @p176 (forall @t84 (= (|tptp.'fun_app$b'| (|tptp.'fun_app$c'| |tptp.'times$'| @t180) @t30) (|tptp.'minus$'| @t31 @t82)))) % 48.68/48.93 (assume @p177 (forall @t88 (= (|tptp.'fun_app$a'| (|tptp.'fun_app$f'| |tptp.'times$c'| @t7) @t37) (- @t39 @t86)))) % 48.68/48.93 (assume @p178 (forall @t93 (= (|tptp.'fun_app$d'| (|tptp.'fun_app$e'| |tptp.'times$a'| (|tptp.'minus$b'| @t18 @t89)) @t45) (|tptp.'minus$b'| @t46 @t91)))) % 48.68/48.93 (assume @p179 (forall @t225 (=> (and @t114 @t219) (= @t224 (= (- @t75 @t223) 0/1))))) % 48.68/48.93 (assume @p180 (forall (@list @t161 @t80) (and (=> @t162 (and (=> @t162 (= @t227 @t80)) (=> @t163 (= @t227 |tptp.'zero$'|)))) (=> @t163 (and (=> @t162 (= @t226 @t80)) (=> @t163 (= @t226 |tptp.'zero$'|))))))) % 48.68/48.93 (assume @p181 (forall (@list @t161 @t5) (and (=> @t162 (and (=> @t162 (= @t229 @t5)) (=> @t163 (= @t229 0)))) (=> @t163 (and (=> @t162 (= @t228 @t5)) (=> @t163 (= @t228 0))))))) % 48.68/48.93 (assume @p182 (forall (@list @t161 @t89) (and (=> @t162 (and (=> @t162 (= @t231 @t89)) (=> @t163 (= @t231 |tptp.'zero$b'|)))) (=> @t163 (and (=> @t162 (= @t230 @t89)) (=> @t163 (= @t230 |tptp.'zero$b'|))))))) % 48.68/48.93 (assume @p183 (forall (@list @t161 @t1) (and (=> @t162 (and (=> @t162 (= @t234 @t1)) (=> @t163 (= @t234 0/1)))) (=> @t163 (and (=> @t162 (= @t232 @t1)) (=> @t163 (= @t232 0/1))))))) % 48.68/48.93 (assume @p184 @t237) % 48.68/48.93 (assume @p185 (= (|tptp.'fps_tan$'| 0/1) |tptp.'zero$'|)) % 48.68/48.93 (assume @p186 (forall @t101 (= (= @t244 1) @t242))) % 48.68/48.93 (assume @p187 (forall @t101 (= (= 1 @t244) @t242))) % 48.68/48.93 (assume @p188 (= @t246 |tptp.'fps_X$'|)) % 48.68/48.93 (assume @p189 (forall @t101 (= (= @t244 0) (or @t248 @t247)))) % 48.68/48.93 (assume @p190 (forall @t20 (and (=> @t249 @t250) (=> (not @t249) (= (- 0 @t240) 0))))) % 48.68/48.93 (assume @p191 (forall @t20 (and (=> @t251 @t250) (=> (not @t251) (= (- @t240 @t240) 0))))) % 48.68/48.93 (assume @p192 (forall @t93 (= (= @t244 @t254) (or (= @t240 @t252) @t247)))) % 48.68/48.93 (assume @p193 (forall @t93 (= @t257 (or @t255 @t248)))) % 48.68/48.93 (assume @p194 (forall @t20 (= (* @t240 0) 0))) % 48.68/48.93 (assume @p195 (forall @t93 (and (=> @t265 (and (=> @t263 (= @t267 0)) (=> @t264 (= @t267 @t260)))) (=> @t266 (and (=> @t263 (= @t262 0)) (=> @t264 (= @t262 @t260))))))) % 48.68/48.93 (assume @p196 (forall @t93 (and (=> @t273 (and (=> @t271 (= @t275 0)) (=> @t272 (= @t275 @t268)))) (=> @t274 (and (=> @t271 (= @t270 0)) (=> @t272 (= @t270 @t268))))))) % 48.68/48.93 (assume @p197 (forall @t20 (and (=> @t276 @t277) (=> (not @t276) (= (- @t240 0) @t240))))) % 48.68/48.93 (assume @p198 (forall @t20 (=> (and (=> @t248 false) (=> @t278 false)) false))) % 48.68/48.93 (assume @p199 (forall @t101 (=> (and @t285 @t284 (=> @t282 @t250) (=> @t283 @t281)) @t279))) % 48.68/48.93 (assume @p200 (forall @t20 (= (* 0 @t240) 0))) % 48.68/48.93 (assume @p201 (forall @t20 (= (* 1 @t240) @t240))) % 48.68/48.93 (assume @p202 (forall @t20 (= (* @t240 1) @t240))) % 48.68/48.93 (assume @p203 (forall @t101 (=> (= @t240 @t244) (or @t239 @t248)))) % 48.68/48.93 (assume @p204 (= |tptp.'bernoulli_fps$'| (|tptp.'minus$'| |tptp.'bernoulli_fps$a'| |tptp.'fps_X$'|))) % 48.68/48.93 (assume @p205 (forall @t20 (and (=> @t248 (= @t286 |tptp.'fps_X$'|)) (=> @t278 (and (=> @t241 (= @t286 |tptp.'one$'|)) (=> @t287 (= @t286 |tptp.'zero$'|))))))) % 48.68/48.93 (assume @p206 (= |tptp.'bernoulli_fps$'| (|tptp.'divide$'| |tptp.'fps_X$'| @t245))) % 48.68/48.93 (assume @p207 (forall @t20 (=> @t289 (and (=> @t241 (= @t288 |tptp.'one$'|)) (=> @t287 (= @t288 |tptp.'zero$'|)))))) % 48.68/48.93 (assume @p208 (forall @t84 (=> (and @t300 @t298 @t295 (not (= (|tptp.'fun_app$i'| @t292 @t109) 0/1))) (= (|tptp.'fun_app$b'| (|tptp.'fps_ginv$'| @t30) @t291) (|tptp.'fps_compose$'| @t290 (|tptp.'fun_app$b'| |tptp.'fps_inv$'| @t80)))))) % 48.68/48.93 (assume @p209 (forall @t93 (= @t257 (or @t248 @t255)))) % 48.68/48.93 (assume @p210 (forall @t21 (= (|tptp.'fun_app$'| (|tptp.'divide$a'| 0/1) @t2) 0/1))) % 48.68/48.93 (assume @p211 (forall @t17 (= (|tptp.'fun_app$a'| (|tptp.'divide$b'| 0) @t6) 0))) % 48.68/48.93 (assume @p212 (forall @t21 (= (|tptp.'fun_app$'| @t301 0/1) 0/1))) % 48.68/48.93 (assume @p213 (forall @t17 (= (|tptp.'fun_app$a'| @t302 0) 0))) % 48.68/48.93 (assume @p214 (forall @t21 (= (|tptp.'fun_app$'| @t301 1/1) @t2))) % 48.68/48.93 (assume @p215 (forall @t17 (= (|tptp.'fun_app$a'| @t302 1) @t6))) % 48.68/48.93 (assume @p216 (forall @t20 @t303)) % 48.68/48.93 (assume @p217 (forall @t101 (=> @t305 (and (=> @t304 @t277) (=> (not @t304) (and (=> @t282 (= (- @t238 0) @t240)) (=> @t283 (= (- @t238 @t280) @t240)))))))) % 48.68/48.93 (assume @p218 (forall @t8 (= (<= 0 @t7) @t306))) % 48.68/48.93 (assume @p219 (forall @t4 (= (<= 0/1 @t3) @t307))) % 48.68/48.93 (assume @p220 (forall @t96 (=> @t111 (= (|tptp.'divide$'| @t94 @t12) @t80)))) % 48.68/48.93 (assume @p221 (forall @t101 (=> @t210 (= (|tptp.'divide$c'| @t99 @t18) @t89)))) % 48.68/48.93 (assume @p222 (forall @t4 (=> @t115 (= (|tptp.'fun_app$'| @t308 @t2) @t1)))) % 48.68/48.93 (assume @p223 (forall @t8 (=> @t156 (= (|tptp.'fun_app$a'| @t309 @t6) @t5)))) % 48.68/48.93 (assume @p224 (forall @t96 (=> @t111 (= (|tptp.'divide$'| @t95 @t12) @t80)))) % 48.68/48.93 (assume @p225 (forall @t101 (=> @t210 (= (|tptp.'divide$c'| @t100 @t18) @t89)))) % 48.68/48.93 (assume @p226 (forall @t4 (=> @t115 (= (|tptp.'fun_app$'| @t310 @t2) @t1)))) % 48.68/48.93 (assume @p227 (forall @t8 (=> @t156 (= (|tptp.'fun_app$a'| @t311 @t6) @t5)))) % 48.68/48.93 (assume @p228 (forall @t21 @t313)) % 48.68/48.93 (assume @p229 (forall @t17 (=> @t156 (= (|tptp.'fun_app$a'| @t302 @t6) 1)))) % 48.68/48.93 (assume @p230 (forall @t101 (= @t314 @t305))) % 48.68/48.93 (assume @p231 (forall @t101 (=> @t305 @t314))) % 48.68/48.93 (assume @p232 (forall @t20 (= (|tptp.'fps_nth$a'| |tptp.'zero$a'| @t18) 0))) % 48.68/48.93 (assume @p233 (forall @t20 (= (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| |tptp.'zero$'|) @t18) 0/1))) % 48.68/48.93 (assume @p234 (forall (@list @t317 @t315 @t45) (= (|tptp.'fps_nth$a'| (|tptp.'minus$a'| @t317 @t315) @t45) (- @t318 @t316)))) % 48.68/48.93 (assume @p235 @t321) % 48.68/48.93 (assume @p236 (forall (@list @t18 @t1 @t30) (= (|tptp.'fps_nth_deriv$'| @t18 (|tptp.'fun_app$b'| @t106 @t30)) (|tptp.'fun_app$b'| @t106 (|tptp.'fps_nth_deriv$'| @t18 @t30))))) % 48.68/48.93 (assume @p237 (forall (@list @t18 @t80 @t52) (= (|tptp.'fps_nth_deriv$'| @t18 (|tptp.'fun_app$b'| @t81 @t182)) (|tptp.'fun_app$b'| (|tptp.'fun_app$c'| |tptp.'times$'| (|tptp.'fps_nth_deriv$'| @t18 @t80)) @t182)))) % 48.68/48.93 (assume @p238 (forall (@list @t323 @t322) (= (|tptp.'fps_nth$b'| @t326 @t293) (|tptp.'fun_app$b'| @t325 (|tptp.'fps_nth$b'| @t322 @t293))))) % 48.68/48.93 (assume @p239 (forall (@list @t317 @t315) (= (|tptp.'fps_nth$a'| @t330 @t293) (|tptp.'fun_app$a'| @t329 @t327)))) % 48.68/48.93 (assume @p240 (forall (@list @t332 @t331) (= (|tptp.'fps_nth$c'| (|tptp.'times$j'| @t332 @t331) @t293) (|tptp.'fun_app$d'| (|tptp.'fun_app$e'| |tptp.'times$a'| (|tptp.'fps_nth$c'| @t332 @t293)) (|tptp.'fps_nth$c'| @t331 @t293))))) % 48.68/48.93 (assume @p241 (forall @t96 (= (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| @t95) @t293) (|tptp.'fun_app$'| @t333 @t294)))) % 48.68/48.93 (assume @p242 (forall (@list @t6 @t89) (and (=> @t247 (= @t334 @t6)) (=> @t335 (= @t334 0))))) % 48.68/48.93 (assume @p243 @t343) % 48.68/48.93 (assume @p244 (forall (@list @t323 @t80 @t45) (= (|tptp.'fps_nth$b'| (|tptp.'times$h'| @t323 @t138) @t45) (|tptp.'fun_app$b'| (|tptp.'fun_app$c'| |tptp.'times$'| (|tptp.'fps_nth$b'| @t323 @t45)) @t80)))) % 48.68/48.93 (assume @p245 (forall (@list @t317 @t5 @t45) (= (|tptp.'fps_nth$a'| (|tptp.'times$i'| @t317 @t140) @t45) (|tptp.'fun_app$a'| (|tptp.'fun_app$f'| |tptp.'times$c'| @t318) @t5)))) % 48.68/48.93 (assume @p246 (forall (@list @t332 @t89 @t45) (= (|tptp.'fps_nth$c'| (|tptp.'times$j'| @t332 @t142) @t45) (|tptp.'fun_app$d'| (|tptp.'fun_app$e'| |tptp.'times$a'| (|tptp.'fps_nth$c'| @t332 @t45)) @t89)))) % 48.68/48.93 (assume @p247 (forall (@list @t12 @t1 @t45) (= (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| (|tptp.'fun_app$b'| @t14 @t105)) @t45) (|tptp.'fun_app$'| (|tptp.'fun_app$g'| |tptp.'times$f'| (|tptp.'fun_app$i'| @t296 @t45)) @t1)))) % 48.68/48.93 (assume @p248 (forall (@list @t12 @t322 @t45) (= (|tptp.'fps_nth$b'| (|tptp.'times$h'| @t139 @t322) @t45) (|tptp.'fun_app$b'| @t14 (|tptp.'fps_nth$b'| @t322 @t45))))) % 48.68/48.93 (assume @p249 (forall (@list @t6 @t315 @t45) (= (|tptp.'fps_nth$a'| (|tptp.'times$i'| @t141 @t315) @t45) (|tptp.'fun_app$a'| @t38 @t316)))) % 48.68/48.93 (assume @p250 (forall (@list @t18 @t331 @t45) (= (|tptp.'fps_nth$c'| (|tptp.'times$j'| @t143 @t331) @t45) (|tptp.'fun_app$d'| @t19 (|tptp.'fps_nth$c'| @t331 @t45))))) % 48.68/48.93 (assume @p251 (forall (@list @t2 @t80 @t45) (= (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| @t181) @t45) (|tptp.'fun_app$'| @t53 (|tptp.'fun_app$i'| @t292 @t45))))) % 48.68/48.93 (assume @p252 (forall @t13 (= (|tptp.'divide$'| @t12 |tptp.'fps_X$'|) (|tptp.'fps_shift$'| @t109 @t12)))) % 48.68/48.93 (assume @p253 (forall @t21 (= (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| @t235) @t293) 0/1))) % 48.68/48.93 (assume @p254 (forall @t20 (and (=> @t248 (= @t344 1)) (=> @t278 (= @t344 0))))) % 48.68/48.93 (assume @p255 (forall @t20 (and (=> @t248 (= @t346 1/1)) (=> @t278 (= @t346 0/1))))) % 48.68/48.93 (assume @p256 (forall @t20 (and (=> @t241 (= @t347 1)) (=> @t287 (= @t347 0))))) % 48.68/48.93 (assume @p257 (forall @t20 (and (=> @t241 (= @t349 1/1)) (=> @t287 (= @t349 0/1))))) % 48.68/48.93 (assume @p258 (forall @t96 (=> @t350 (= (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| (|tptp.'divide$'| @t80 @t12)) @t293) (|tptp.'fun_app$'| (|tptp.'divide$a'| @t294) @t299))))) % 48.68/48.93 (assume @p259 (forall @t352 (=> @t351 (= (|tptp.'fps_compose$a'| |tptp.'fps_X$a'| @t317) @t317)))) % 48.68/48.93 (assume @p260 (forall @t13 (=> @t300 (= (|tptp.'fps_compose$'| |tptp.'fps_X$'| @t12) @t12)))) % 48.68/48.93 (assume @p261 @t353) % 48.68/48.93 (assume @p262 (forall @t360 (and (=> @t247 (= @t357 0)) (=> @t335 (and (=> @t358 (= @t357 @t328)) (=> @t359 (= @t357 @t356))))))) % 48.68/48.93 (assume @p263 @t373) % 48.68/48.93 (assume @p264 (forall @t360 (and (=> @t247 (= @t374 0)) (=> @t335 (and (=> @t358 (= @t374 @t328)) (=> @t359 (= @t374 @t356))))))) % 48.68/48.93 (assume @p265 (forall @t372 (and (=> @t247 (= @t375 0/1)) (=> @t335 (and (=> @t358 (= @t375 @t299)) (=> @t359 (= @t375 @t361))))))) % 48.68/48.93 (assume @p266 (forall @t93 (=> @t305 (and (=> @t380 @t382) (=> (not @t380) (and (=> @t378 (<= @t377 0)) (=> @t379 (<= @t377 @t376)))))))) % 48.68/48.93 (assume @p267 (forall @t93 (=> (and @t305 (<= @t252 @t238)) (= (and (=> @t282 @t384) (=> @t283 (and (=> @t273 @t383) (=> @t274 (<= @t280 @t269))))) (<= @t252 @t240))))) % 48.68/48.93 (assume @p268 (forall @t101 (and (=> @t265 @t303) (=> @t266 (<= @t261 @t240))))) % 48.68/48.93 (assume @p269 (forall @t93 (=> @t305 (and (=> @t386 @t384) (=> @t387 (and (=> @t273 (<= @t385 0)) (=> @t274 (<= @t385 @t269)))))))) % 48.68/48.93 (assume @p270 (forall @t93 (=> @t394 (and (=> @t392 (and (=> @t273 @t250) (=> @t274 (= 0 @t269)))) (=> (not @t392) (and (=> @t282 (and (=> @t378 (and (=> @t273 (= @t391 0)) (=> @t274 (= @t391 @t269)))) (=> @t379 (and (=> @t273 (= @t390 0)) (=> @t274 (= @t390 @t269)))))) (=> @t283 (and (=> @t378 (and (=> @t273 (= @t389 0)) (=> @t274 (= @t389 @t269)))) (=> @t379 (and (=> @t273 (= @t388 0)) (=> @t274 (= @t388 @t269)))))))))))) % 48.68/48.93 (assume @p271 (forall @t93 (and (=> @t401 (and (=> @t398 @t250) (=> @t399 (and (=> @t386 (= 0 @t397)) (=> @t387 (= 0 @t395)))))) (=> (not @t401) (and (=> @t265 (and (=> @t398 (= @t400 0)) (=> @t399 (and (=> @t386 (= @t400 @t397)) (=> @t387 (= @t400 @t395)))))) (=> @t266 (and (=> @t398 (= @t396 0)) (=> @t399 (and (=> @t386 (= @t396 @t397)) (=> @t387 (= @t396 @t395))))))))))) % 48.68/48.93 (assume @p272 (forall @t93 (=> @t394 (= (and (=> @t282 @t382) (=> @t283 (and (=> @t378 @t383) (=> @t379 (<= @t280 @t376))))) @t402)))) % 48.68/48.93 (assume @p273 (forall @t93 (=> @t394 (= (and (=> @t282 (and (=> @t378 @t250) (=> @t379 (= 0 @t376)))) (=> @t283 (and (=> @t378 @t281) (=> @t379 (= @t280 @t376))))) @t255)))) % 48.68/48.93 (assume @p274 (forall (@list @t404 @t89 @t45) (=> (and (|tptp.'fun_app$h'| @t404 @t89) (forall @t407 (=> @t406 (<= @t403 @t252)))) (exists @t407 (and @t406 (forall @t405 (=> (|tptp.'fun_app$h'| @t404 @t67) (<= (|tptp.'of_nat$'| @t67) @t403)))))))) % 48.68/48.93 (assume @p275 (forall @t101 (or @t305 @t408))) % 48.68/48.93 (assume @p276 (forall @t101 (=> (and @t305 @t408) @t279))) % 48.68/48.93 (assume @p277 (forall @t101 (=> @t279 @t305))) % 48.68/48.93 (assume @p278 (forall @t93 (=> (and @t305 @t402) @t393))) % 48.68/48.93 (assume @p279 (forall @t20 (<= @t240 @t240))) % 48.68/48.93 (assume @p280 @t381) % 48.68/48.93 (assume @p281 (<= 0/1 0/1)) % 48.68/48.93 (assume @p282 (<= 1 1)) % 48.68/48.93 (assume @p283 (<= 1/1 1/1)) % 48.68/48.93 (assume @p284 (forall @t151 (=> @t150 (= @t410 @t409)))) % 48.68/48.93 (assume @p285 (forall @t225 (=> (= @t3 (- @t52 @t71)) (= @t412 @t411)))) % 48.68/48.93 (assume @p286 (forall @t88 (=> @t410 (<= @t152 @t222)))) % 48.68/48.93 (assume @p287 (forall @t77 (=> @t412 (<= (- @t2 @t52) @t157)))) % 48.68/48.93 (assume @p288 (forall @t88 (=> @t410 (<= (- @t37 @t5) (- @t37 @t6))))) % 48.68/48.93 (assume @p289 (forall @t77 (=> @t412 (<= (- @t52 @t1) (- @t52 @t2))))) % 48.68/48.93 (assume @p290 (forall @t151 (=> (and @t410 @t409) (<= (- @t6 @t64) @t222)))) % 48.68/48.93 (assume @p291 (forall @t225 (=> (and @t412 @t411) (<= (- @t2 @t71) @t157)))) % 48.68/48.93 (assume @p292 (forall @t20 (= @t303 true))) % 48.68/48.93 (assume @p293 (forall @t20 (= @t413 @t248))) % 48.68/48.93 (assume @p294 (forall @t20 (=> @t413 @t248))) % 48.68/48.93 (assume @p295 (forall @t93 (=> @t305 (<= (|tptp.'fun_app$a'| @t253 @t240) @t254)))) % 48.68/48.93 (assume @p296 (forall @t93 (=> @t305 (<= @t256 @t259)))) % 48.68/48.93 (assume @p297 (forall @t414 (=> (and @t305 (<= @t252 @t403)) (<= @t256 (|tptp.'fun_app$a'| @t258 @t403))))) % 48.68/48.93 (assume @p298 (forall @t20 (<= @t240 @t415))) % 48.68/48.93 (assume @p299 (forall @t20 (<= @t240 (|tptp.'fun_app$a'| @t243 @t415)))) % 48.68/48.93 (assume @p300 (forall @t84 (=> (and @t300 (not @t295)) (= (|tptp.'fps_compose$'| (|tptp.'divide$'| @t30 @t80) @t12) (|tptp.'divide$'| @t290 @t416))))) % 48.68/48.93 (assume @p301 (forall @t93 (=> @t421 (|tptp.'fun_app$h'| (|tptp.'less_eq$'| @t133) @t208)))) % 48.68/48.93 (assume @p302 (forall @t88 (=> @t423 (<= @t131 @t207)))) % 48.68/48.93 (assume @p303 (forall @t77 (=> @t425 (<= @t134 @t126)))) % 48.68/48.93 (assume @p304 (forall @t8 (= @t433 @t432))) % 48.68/48.93 (assume @p305 (forall @t4 (= @t441 @t440))) % 48.68/48.93 (assume @p306 (forall @t101 (=> @t445 (|tptp.'fun_app$h'| @t442 |tptp.'zero$b'|)))) % 48.68/48.93 (assume @p307 (forall @t8 (=> @t446 (<= @t97 0)))) % 48.68/48.93 (assume @p308 (forall @t4 (=> @t447 (<= @t102 0/1)))) % 48.68/48.93 (assume @p309 (forall @t101 (=> @t451 @t449))) % 48.68/48.93 (assume @p310 (forall @t8 (=> @t453 @t452))) % 48.68/48.93 (assume @p311 (forall @t4 (=> @t455 @t454))) % 48.68/48.93 (assume @p312 (forall @t101 (=> @t445 @t449))) % 48.68/48.93 (assume @p313 (forall @t8 (=> @t446 @t452))) % 48.68/48.93 (assume @p314 (forall @t4 (=> @t447 @t454))) % 48.68/48.93 (assume @p315 (forall @t101 (=> (and @t444 @t450) (|tptp.'fun_app$h'| @t417 @t100)))) % 48.68/48.93 (assume @p316 (forall @t8 (=> @t431 @t433))) % 48.68/48.93 (assume @p317 (forall @t4 (=> @t439 @t441))) % 48.68/48.93 (assume @p318 (forall @t101 (=> (or @t445 @t451) @t449))) % 48.68/48.93 (assume @p319 (forall @t8 (=> @t456 @t452))) % 48.68/48.93 (assume @p320 (forall @t4 (=> @t457 @t454))) % 48.68/48.93 (assume @p321 (forall @t8 (= @t452 @t456))) % 48.68/48.93 (assume @p322 (forall @t4 (= @t454 @t457))) % 48.68/48.93 (assume @p323 (forall @t93 (=> @t421 (|tptp.'fun_app$h'| @t458 @t91)))) % 48.68/48.93 (assume @p324 (forall @t88 (=> @t423 (<= @t39 @t86)))) % 48.68/48.93 (assume @p325 (forall @t77 (=> @t425 (<= @t54 @t75)))) % 48.68/48.93 (assume @p326 (forall @t88 (=> @t459 (<= @t86 @t39)))) % 48.68/48.93 (assume @p327 (forall @t77 (=> @t460 (<= @t75 @t54)))) % 48.68/48.93 (assume @p328 (forall @t8 (=> @t428 @t433))) % 48.68/48.93 (assume @p329 (forall @t4 (=> @t436 @t441))) % 48.68/48.93 (assume @p330 (forall @t88 (=> @t459 (<= @t207 @t131)))) % 48.68/48.93 (assume @p331 (forall @t77 (=> @t460 (<= @t126 @t134)))) % 48.68/48.93 (assume @p332 (forall @t8 (=> @t432 @t433))) % 48.68/48.93 (assume @p333 (forall @t4 (=> @t440 @t441))) % 48.68/48.93 (assume @p334 (forall @t17 (<= 0 @t461))) % 48.68/48.93 (assume @p335 (forall @t21 (<= 0/1 @t462))) % 48.68/48.93 (assume @p336 (forall @t414 (=> (and @t420 @t464 @t444 @t418) @t463))) % 48.68/48.93 (assume @p337 (forall @t151 (=> (and @t410 @t409 @t430 @t422) @t466))) % 48.68/48.93 (assume @p338 (forall @t225 (=> (and @t412 @t411 @t438 @t424) @t468))) % 48.68/48.93 (assume @p339 (forall @t414 (=> (and @t420 @t464 @t450 @t418) @t463))) % 48.68/48.93 (assume @p340 (forall @t151 (=> (and @t410 @t409 @t429 @t422) @t466))) % 48.68/48.93 (assume @p341 (forall @t225 (=> (and @t412 @t411 @t437 @t424) @t468))) % 48.68/48.93 (assume @p342 (not (<= 1 0))) % 48.68/48.93 (assume @p343 (not (<= 1/1 0/1))) % 48.68/48.93 (assume @p344 (<= 0 1)) % 48.68/48.93 (assume @p345 (<= 0/1 1/1)) % 48.68/48.93 (assume @p346 (forall @t8 (= @t410 (<= @t7 0)))) % 48.68/48.93 (assume @p347 (forall @t4 (= @t412 (<= @t3 0/1)))) % 48.68/48.93 (assume @p348 (forall @t352 (= @t471 (exists @t470 @t469)))) % 48.68/48.93 (assume @p349 (forall @t13 (= @t111 (exists @t470 @t473)))) % 48.68/48.93 (assume @p350 (forall @t360 (=> @t469 @t471))) % 48.68/48.93 (assume @p351 (forall @t372 (=> @t473 @t111))) % 48.68/48.93 (assume @p352 (forall @t84 (=> @t111 (= (|tptp.'divide$'| @t94 @t129) @t474)))) % 48.68/48.93 (assume @p353 (forall @t101 (=> (and @t475 @t450) (|tptp.'fun_app$h'| @t442 @t89)))) % 48.68/48.93 (assume @p354 (forall @t8 (=> (and @t476 @t429) (<= @t97 @t5)))) % 48.68/48.93 (assume @p355 (forall @t4 (=> (and @t477 @t437) (<= @t102 @t1)))) % 48.68/48.93 (assume @p356 (forall @t101 (=> (and @t475 @t450 @t478) (|tptp.'fun_app$h'| @t448 |tptp.'one$a'|)))) % 48.68/48.93 (assume @p357 (forall @t8 (=> (and @t476 @t429 @t479) (<= @t98 1)))) % 48.68/48.93 (assume @p358 (forall @t4 (=> (and @t477 @t437 @t480) (<= @t78 1/1)))) % 48.68/48.93 (assume @p359 (forall @t8 (=> @t481 (<= @t98 @t6)))) % 48.68/48.93 (assume @p360 (forall @t4 (=> @t482 (<= @t78 @t2)))) % 48.68/48.93 (assume @p361 (forall @t8 (=> @t481 (<= @t97 @t6)))) % 48.68/48.93 (assume @p362 (forall @t4 (=> @t482 (<= @t102 @t2)))) % 48.68/48.93 (assume @p363 (forall @t485 (=> (and @t351 (= @t327 0)) (= (|tptp.'fps_compose$a'| @t483 @t484) (|tptp.'fps_compose$a'| (|tptp.'fps_compose$a'| @t483 @t315) @t317))))) % 48.68/48.93 (assume @p364 (forall @t84 (=> (and @t300 @t295) (= (|tptp.'fps_compose$'| @t30 @t416) (|tptp.'fps_compose$'| (|tptp.'fps_compose$'| @t30 @t80) @t12))))) % 48.68/48.93 (assume @p365 (forall @t485 (=> (and @t351 (not (= (|tptp.'fps_nth$a'| @t317 @t109) 0))) (= (= @t484 @t486) (= @t315 @t483))))) % 48.68/48.93 (assume @p366 (forall @t84 (=> @t487 (= (= @t416 @t290) @t200)))) % 48.68/48.93 (assume @p367 (forall @t13 (=> @t350 @t489))) % 48.68/48.93 (assume @p368 (forall @t13 (=> @t350 @t490))) % 48.68/48.93 (assume @p369 (forall @t485 (=> @t351 (= (|tptp.'fps_compose$a'| (|tptp.'times$i'| @t315 @t483) @t317) (|tptp.'times$i'| @t484 @t486))))) % 48.68/48.93 (assume @p370 (forall @t84 (=> @t300 (= (|tptp.'fps_compose$'| @t82 @t12) (|tptp.'fun_app$b'| (|tptp.'fun_app$c'| |tptp.'times$'| @t416) @t290))))) % 48.68/48.93 (assume @p371 (forall @t13 (=> @t487 (= (|tptp.'fun_app$b'| |tptp.'fps_inv$'| @t491) @t12)))) % 48.68/48.93 (assume @p372 (forall (@list @t18 @t80) (=> @t289 (and (=> @t493 (= @t492 (|tptp.'fps_shift$'| @t293 @t80))) (=> (not @t493) (= @t492 (|tptp.'fps_shift$'| (|tptp.'nat$'| (- @t240 1)) @t80))))))) % 48.68/48.93 (assume @p373 (forall @t495 (= (exists @t494 (= |tptp.'one$c'| (|tptp.'times$h'| @t322 @t323))) (exists @t488 (= |tptp.'one$'| (|tptp.'fun_app$b'| @t81 @t324)))))) % 48.68/48.93 (assume @p374 (forall @t352 (= (exists @t497 (= |tptp.'one$b'| (|tptp.'times$i'| @t315 @t317))) (exists @t496 (= 1 (|tptp.'fun_app$a'| @t85 @t328)))))) % 48.68/48.93 (assume @p375 (forall @t13 (= @t489 (exists @t498 (= 1/1 (|tptp.'fun_app$'| @t74 @t299)))))) % 48.68/48.93 (assume @p376 (forall @t495 (= (exists @t494 (= |tptp.'one$c'| @t326)) (exists @t488 (= |tptp.'one$'| (|tptp.'fun_app$b'| @t325 @t80)))))) % 48.68/48.93 (assume @p377 (forall @t352 (= (exists @t497 (= |tptp.'one$b'| @t330)) (exists @t496 (= 1 (|tptp.'fun_app$a'| @t329 @t5)))))) % 48.68/48.93 (assume @p378 (forall @t13 (= @t490 (exists @t498 (= 1/1 (|tptp.'fun_app$'| @t333 @t1)))))) % 48.68/48.93 (assume @p379 @t501) % 48.68/48.93 (assume @p380 (forall @t13 (=> @t487 (= (|tptp.'fps_compose$'| @t491 @t12) |tptp.'fps_X$'|)))) % 48.68/48.93 (assume @p381 (forall @t13 (=> @t487 (= (|tptp.'fps_compose$'| @t12 @t491) |tptp.'fps_X$'|)))) % 48.68/48.93 (assume @p382 (forall @t4 (=> @t115 (= (|tptp.'fun_app$'| @t301 @t102) @t503)))) % 48.68/48.93 (assume @p383 (forall @t4 (=> @t115 (= (|tptp.'fun_app$'| @t301 @t78) @t503)))) % 48.68/48.93 (assume @p384 (forall @t21 (= (<= @t504 0/1) @t435))) % 48.68/48.93 (assume @p385 (forall @t21 (= (<= 0/1 @t504) @t438))) % 48.68/48.93 (assume @p386 (forall @t21 (= (= 0/1 @t504) @t114))) % 48.68/48.93 (assume @p387 (forall @t21 (= (= @t504 0/1) @t114))) % 48.68/48.93 (assume @p388 (forall @t4 (= (= @t505 0/1) @t119))) % 48.68/48.93 (assume @p389 (forall @t77 (= (= @t505 @t506) @t206))) % 48.68/48.93 (assume @p390 (forall @t77 (= (= @t505 (|tptp.'fun_app$'| @t507 @t1)) @t209))) % 48.68/48.93 (assume @p391 (forall @t77 (= (|tptp.'fun_app$'| @t510 @t52) @t509))) % 48.68/48.93 (assume @p392 (forall @t77 (= @t512 (|tptp.'fun_app$'| @t301 @t75)))) % 48.68/48.93 (assume @p393 (forall @t77 (= (|tptp.'fun_app$'| @t301 @t514) @t509))) % 48.68/48.93 (assume @p394 (forall @t77 (= (|tptp.'fun_app$'| @t53 @t514) (|tptp.'fun_app$'| @t310 @t52)))) % 48.68/48.93 (assume @p395 (forall @t93 (and (=> @t248 (= @t517 0)) (=> @t278 (= @t517 @t516))))) % 48.68/48.93 (assume @p396 (forall @t77 (and (=> @t114 (= @t518 0/1)) @t519))) % 48.68/48.93 (assume @p397 (forall @t77 @t519)) % 48.68/48.93 (assume @p398 (forall @t77 (=> @t115 (= (|tptp.'fun_app$'| @t310 @t134) @t514)))) % 48.68/48.93 (assume @p399 (forall @t77 (=> @t115 (= (|tptp.'fun_app$'| @t308 @t134) @t514)))) % 48.68/48.93 (assume @p400 (forall @t77 (=> @t115 (= (|tptp.'fun_app$'| @t308 @t54) @t514)))) % 48.68/48.93 (assume @p401 (forall @t4 (= @t521 @t520))) % 48.68/48.93 (assume @p402 (forall @t4 (= @t522 @t520))) % 48.68/48.93 (assume @p403 (forall @t21 (and (=> @t114 (= @t312 0/1)) @t313))) % 48.68/48.93 (assume @p404 (forall @t4 (= @t521 @t524))) % 48.68/48.93 (assume @p405 (forall @t4 (= @t522 @t524))) % 48.68/48.93 (assume @p406 (forall @t225 (= (|tptp.'fun_app$'| @t510 @t525) (|tptp.'fun_app$'| @t508 @t467)))) % 48.68/48.93 (assume @p407 (forall @t225 (= (|tptp.'fun_app$'| @t511 @t525) (|tptp.'fun_app$'| (|tptp.'divide$a'| @t526) @t75)))) % 48.68/48.93 (assume @p408 (forall @t77 (= @t512 (|tptp.'fun_app$'| @t301 @t126)))) % 48.68/48.93 (assume @p409 (forall @t77 (=> @t460 (<= @t514 @t506)))) % 48.68/48.93 (assume @p410 (forall @t4 (=> @t436 @t527))) % 48.68/48.93 (assume @p411 (forall @t4 (=> @t455 @t528))) % 48.68/48.93 (assume @p412 (forall @t4 (=> @t447 @t528))) % 48.68/48.93 (assume @p413 (forall @t4 (=> @t439 @t527))) % 48.68/48.93 (assume @p414 (forall @t4 (= @t527 @t440))) % 48.68/48.93 (assume @p415 (forall @t77 (=> @t425 (<= @t506 @t514)))) % 48.68/48.93 (assume @p416 (forall @t4 (= @t528 @t457))) % 48.68/48.93 (assume @p417 (forall @t225 (=> @t220 (= (= @t530 @t529) (= @t126 @t223))))) % 48.68/48.93 (assume @p418 (forall @t77 (= (= @t505 @t52) (and (=> @t219 (= @t2 @t126)) @t531)))) % 48.68/48.93 (assume @p419 (forall @t77 (= (= @t2 @t514) (and (=> @t532 (= @t54 @t1)) @t533)))) % 48.68/48.93 (assume @p420 (forall @t77 (=> (and @t115 @t536) @t535))) % 48.68/48.93 (assume @p421 (forall @t77 (=> (and @t115 @t538) @t537))) % 48.68/48.93 (assume @p422 (forall @t77 (=> @t115 (= @t535 @t536)))) % 48.68/48.93 (assume @p423 (forall @t77 (=> @t115 (= @t537 @t538)))) % 48.68/48.93 (assume @p424 (forall @t4 (=> @t115 (= (= @t534 1/1) @t523)))) % 48.68/48.93 (assume @p425 (forall @t77 (and (=> @t224 (= @t539 @t2)) (=> @t532 (= @t539 (|tptp.'fun_app$'| (|tptp.'divide$a'| (- @t54 @t1)) @t52)))))) % 48.68/48.93 (assume @p426 (forall @t225 (=> @t220 (= (- @t530 @t529) @t540)))) % 48.68/48.93 (assume @p427 (forall @t77 (=> @t115 (= (- @t1 @t530) (|tptp.'fun_app$'| (|tptp.'divide$a'| (- @t102 @t52)) @t2))))) % 48.68/48.93 (assume @p428 (forall @t77 (=> @t115 (= (- @t534 @t52) (|tptp.'fun_app$'| (|tptp.'divide$a'| (- @t1 @t134)) @t2))))) % 48.68/48.93 (assume @p429 (forall @t225 (=> @t220 (= (<= @t530 @t529) (<= @t540 0/1))))) % 48.68/48.93 (assume @p430 (forall @t84 @t542)) % 48.68/48.93 (assume @p431 (forall @t93 @t545)) % 48.68/48.93 (assume @p432 (forall @t88 @t549)) % 48.68/48.93 (assume @p433 (forall @t93 (=> @t210 (= (|tptp.'divide$c'| @t99 @t133) @t543)))) % 48.68/48.93 (assume @p434 (forall @t88 (=> @t156 (= (|tptp.'fun_app$a'| @t309 @t131) @t547)))) % 48.68/48.93 (assume @p435 (forall @t84 (and (=> @t110 (= @t541 |tptp.'zero$'|)) @t542))) % 48.68/48.93 (assume @p436 (forall @t93 (and (=> @t197 (= @t544 |tptp.'zero$b'|)) @t545))) % 48.68/48.93 (assume @p437 (forall @t88 (and (=> @t153 (= @t548 0)) @t549))) % 48.68/48.93 (assume @p438 (forall @t101 (<= @t551 @t240))) % 48.68/48.93 (assume @p439 (forall @t93 (=> @t305 (<= (|tptp.'fun_app$a'| @t550 @t252) @t516)))) % 48.68/48.93 (assume @p440 (forall @t93 (= (|tptp.'fun_app$a'| @t550 @t259) (|tptp.'fun_app$a'| (|tptp.'divide$b'| @t551) @t252)))) % 48.68/48.93 (assume @p441 (forall @t101 (<= (|tptp.'fun_app$a'| (|tptp.'fun_app$f'| |tptp.'times$c'| @t551) @t238) @t240))) % 48.68/48.93 (assume @p442 (forall @t101 (<= (|tptp.'fun_app$a'| @t243 (|tptp.'fun_app$a'| @t515 @t240)) @t238))) % 48.68/48.93 (assume @p443 (forall (@list @t562 @t555 @t560) (=> (and (forall @t569 (=> @t568 (|tptp.'fun_app$j'| @t562 (|tptp.'fun_app$k'| @t555 @t566)))) (forall @t569 (=> @t568 (forall @t405 (=> (|tptp.'fun_app$h'| @t560 @t67) (and (<= 0/1 @t567) (<= @t567 1/1))))))) (exists (@list @t557) (and (forall @t564 (<= @t558 1)) (forall @t564 (=> (and @t563 @t561 (= @t554 0/1)) @t565)) (forall @t564 (=> (and @t563 @t561 (= @t554 1/1)) @t559)) (forall @t564 (=> (and @t563 @t561 @t565) (<= @t554 @t556))) (forall @t564 (=> (and @t563 @t561 @t559) (<= @t556 @t554)))))))) % 48.68/48.93 (assume @p444 (forall @t93 (=> @t444 (= (|tptp.'divide$c'| @t89 @t133) (|tptp.'divide$c'| @t543 @t18))))) % 48.68/48.93 (assume @p445 (forall @t88 (=> @t430 (= (|tptp.'fun_app$a'| @t546 @t131) (|tptp.'fun_app$a'| (|tptp.'divide$b'| @t547) @t6))))) % 48.68/48.93 (assume @p446 (forall @t101 (=> (and @t444 @t475 @t478) (= (= @t100 |tptp.'one$a'|) (and (= @t18 |tptp.'one$a'|) (= @t89 |tptp.'one$a'|)))))) % 48.68/48.93 (assume @p447 (forall @t8 (=> (and @t430 @t476 @t479) (= (= @t98 1) (and @t104 @t185))))) % 48.68/48.93 (assume @p448 (forall @t4 (=> (and @t438 @t477 @t480) (= (= @t78 1/1) (and @t103 @t148))))) % 48.68/48.93 (assume @p449 (forall @t8 (= @t410 (<= 0 @t570)))) % 48.68/48.93 (assume @p450 (forall @t4 (= @t412 (<= 0/1 @t571)))) % 48.68/48.93 (assume @p451 (forall (@list @t6 @t5 @t37 @t64 @t63 @t574 @t576 @t572) (=> (and @t156 @t214 (not (= @t37 0)) (not (= @t64 0)) (= (|tptp.'fun_app$a'| @t578 @t5) (|tptp.'fun_app$a'| @t575 @t6)) (= (|tptp.'fun_app$a'| @t577 @t64) (|tptp.'fun_app$a'| @t573 @t37))) (= (<= (|tptp.'fun_app$a'| (|tptp.'fun_app$f'| |tptp.'times$c'| (|tptp.'fun_app$a'| @t578 @t37)) @t39) (|tptp.'fun_app$a'| (|tptp.'fun_app$f'| |tptp.'times$c'| (|tptp.'fun_app$a'| @t577 @t6)) @t39)) (<= (|tptp.'fun_app$a'| (|tptp.'fun_app$f'| |tptp.'times$c'| (|tptp.'fun_app$a'| @t575 @t64)) @t465) (|tptp.'fun_app$a'| (|tptp.'fun_app$f'| |tptp.'times$c'| (|tptp.'fun_app$a'| @t573 @t5)) @t465)))))) % 48.68/48.93 (assume @p452 (forall (@list @t2 @t1 @t52 @t71 @t70 @t581 @t583 @t579) (=> (and @t115 @t219 @t532 (not (= @t71 0/1)) (= (|tptp.'fun_app$'| @t585 @t1) (|tptp.'fun_app$'| @t582 @t2)) (= (|tptp.'fun_app$'| @t584 @t71) (|tptp.'fun_app$'| @t580 @t52))) (= (<= (|tptp.'fun_app$'| (|tptp.'fun_app$g'| |tptp.'times$f'| (|tptp.'fun_app$'| @t585 @t52)) @t54) (|tptp.'fun_app$'| (|tptp.'fun_app$g'| |tptp.'times$f'| (|tptp.'fun_app$'| @t584 @t2)) @t54)) (<= (|tptp.'fun_app$'| (|tptp.'fun_app$g'| |tptp.'times$f'| (|tptp.'fun_app$'| @t582 @t71)) @t467) (|tptp.'fun_app$'| (|tptp.'fun_app$g'| |tptp.'times$f'| (|tptp.'fun_app$'| @t580 @t1)) @t467)))))) % 48.68/48.93 (assume @p453 (forall @t151 (=> (and @t410 @t409 @t429 @t587) (<= @t86 @t586)))) % 48.68/48.93 (assume @p454 (forall @t225 (=> (and @t412 @t411 @t437 @t588) (<= @t75 @t526)))) % 48.68/48.93 (assume @p455 (forall @t21 (=> @t114 @t438))) % 48.68/48.93 (assume @p456 (forall @t151 (=> (and @t410 @t409 @t427 @t587) (<= @t465 @t39)))) % 48.68/48.93 (assume @p457 (forall @t225 (=> (and @t412 @t411 @t435 @t588) (<= @t467 @t54)))) % 48.68/48.93 (assume @p458 (forall @t151 (=> (and @t410 @t409 @t427 @t422) (<= @t586 @t86)))) % 48.68/48.93 (assume @p459 (forall @t225 (=> (and @t412 @t411 @t435 @t424) (<= @t526 @t75)))) % 48.68/48.93 (assume @p460 (= |tptp.'bernoulli_fps$a'| (|tptp.'divide$'| |tptp.'fps_X$'| (|tptp.'minus$'| |tptp.'one$'| (|tptp.'fps_exp$'| @t589))))) % 48.68/48.93 (assume @p461 (forall @t21 (= (- @t590) @t2))) % 48.68/48.93 (assume @p462 (forall @t4 (= (= @t590 @t591) @t25))) % 48.68/48.93 (assume @p463 @t250) % 48.68/48.93 (assume @p464 (= 0/1 0/1)) % 48.68/48.93 (assume @p465 (forall @t17 (= (= 0 @t592) @t154))) % 48.68/48.93 (assume @p466 (forall @t21 (= (= 0/1 @t590) @t155))) % 48.68/48.93 (assume @p467 (forall @t17 (= (= @t592 0) @t153))) % 48.68/48.93 (assume @p468 (forall @t21 (= (= @t590 0/1) @t114))) % 48.68/48.93 (assume @p469 (forall @t17 (= (= @t6 @t592) @t153))) % 48.68/48.93 (assume @p470 (forall @t21 (= (= @t2 @t590) @t114))) % 48.68/48.93 (assume @p471 (forall @t17 (= (= @t592 @t6) @t153))) % 48.68/48.93 (assume @p472 (forall @t21 (= (= @t590 @t2) @t114))) % 48.68/48.93 (assume @p473 (forall @t8 (= (<= @t592 @t593) @t306))) % 48.68/48.93 (assume @p474 (forall @t4 (= (<= @t590 @t591) @t307))) % 48.68/48.93 (assume @p475 (forall @t96 (= @t596 @t594))) % 48.68/48.93 (assume @p476 (forall @t8 (= @t598 @t597))) % 48.68/48.93 (assume @p477 (forall @t4 (= @t600 @t599))) % 48.68/48.93 (assume @p478 (forall @t96 (= (|tptp.'fun_app$b'| @t602 @t595) @t95))) % 48.68/48.93 (assume @p479 (forall @t8 (= (|tptp.'fun_app$a'| @t603 @t593) @t98))) % 48.68/48.93 (assume @p480 @t607) % 48.68/48.93 (assume @p481 (forall @t96 (= @t608 @t594))) % 48.68/48.93 (assume @p482 (forall @t8 (= @t609 @t597))) % 48.68/48.93 (assume @p483 (forall @t4 (= @t610 @t599))) % 48.68/48.93 (assume @p484 (forall @t8 (= (- @t7) @t570))) % 48.68/48.93 (assume @p485 (forall @t4 (= (- @t3) @t571))) % 48.68/48.93 (assume @p486 (forall @t8 (= (|tptp.'fun_app$a'| @t611 @t593) (|tptp.'fun_app$a'| @t302 @t5)))) % 48.68/48.93 (assume @p487 (forall @t372 (= (|tptp.'fun_app$i'| (|tptp.'fps_nth$'| @t601) @t89) (- @t472)))) % 48.68/48.93 (assume @p488 (forall @t21 (= (|tptp.'uminus$'| @t137) (|tptp.'fps_const$'| @t590)))) % 48.68/48.93 (assume @p489 (forall @t17 (= (<= @t592 @t6) @t430))) % 48.68/48.93 (assume @p490 (forall @t21 (= (<= @t590 @t2) @t438))) % 48.68/48.93 (assume @p491 (forall @t17 (= (<= @t6 @t592) @t427))) % 48.68/48.93 (assume @p492 (forall @t21 (= (<= @t2 @t590) @t435))) % 48.68/48.93 (assume @p493 (forall @t17 (= (<= @t592 0) @t430))) % 48.68/48.93 (assume @p494 (forall @t21 (= (<= @t590 0/1) @t438))) % 48.68/48.93 (assume @p495 (forall @t17 (= (<= 0 @t592) @t427))) % 48.68/48.93 (assume @p496 (forall @t21 (= @t612 @t435))) % 48.68/48.93 (assume @p497 (forall @t17 (= (- 0 @t6) @t592))) % 48.68/48.93 (assume @p498 (forall @t21 (= (- 0/1 @t2) @t590))) % 48.68/48.93 (assume @p499 (forall @t13 (= (|tptp.'fun_app$b'| (|tptp.'fun_app$c'| |tptp.'times$'| @t613) @t12) @t601))) % 48.68/48.93 (assume @p500 (forall @t17 (= (* @t614 @t6) @t592))) % 48.68/48.93 (assume @p501 (forall @t21 (= (* @t589 @t2) @t590))) % 48.68/48.93 (assume @p502 (forall @t13 (= (|tptp.'fun_app$b'| @t14 @t613) @t601))) % 48.68/48.93 (assume @p503 (forall @t17 (= (* @t6 @t614) @t592))) % 48.68/48.93 (assume @p504 (forall @t21 (= (* @t2 @t589) @t590))) % 48.68/48.93 (assume @p505 (forall @t21 (= (|tptp.'fun_app$'| @t301 @t589) @t590))) % 48.68/48.93 (assume @p506 (forall @t17 (= (|tptp.'fun_app$a'| @t302 @t614) @t592))) % 48.68/48.93 (assume @p507 (= (- @t614 @t614) 0)) % 48.68/48.93 (assume @p508 (= (- @t589 @t589) 0/1)) % 48.68/48.93 (assume @p509 @t619) % 48.68/48.93 (assume @p510 (forall @t4 (= @t620 (|tptp.'fun_app$'| @t301 @t591)))) % 48.68/48.93 (assume @p511 (forall @t4 (= (|tptp.'fun_app$'| @t621 @t591) @t505))) % 48.68/48.93 (assume @p512 (forall @t4 (= @t620 (|tptp.'fun_app$'| @t621 @t1)))) % 48.68/48.93 (assume @p513 (forall @t8 (= (|tptp.'fun_app$a'| @t302 @t593) (|tptp.'fun_app$a'| @t611 @t5)))) % 48.68/48.93 (assume @p514 (forall @t4 (= @t622 (= @t1 @t590)))) % 48.68/48.93 (assume @p515 (forall @t4 (= (= @t590 @t1) (= @t591 @t2)))) % 48.68/48.93 (assume @p516 (forall @t96 (= (|tptp.'fps_compose$'| @t601 @t80) (|tptp.'uminus$'| @t183)))) % 48.68/48.93 (assume @p517 (forall @t8 (= (- @t592 @t5) (- @t593 @t6)))) % 48.68/48.93 (assume @p518 (forall @t4 (= (- @t590 @t1) (- @t591 @t2)))) % 48.68/48.93 (assume @p519 (not (= 1 @t614))) % 48.68/48.93 (assume @p520 (not (= 1/1 @t589))) % 48.68/48.93 (assume @p521 (forall @t96 (= @t608 @t596))) % 48.68/48.93 (assume @p522 (forall @t8 (= @t609 @t598))) % 48.68/48.93 (assume @p523 (forall @t4 (= @t610 @t600))) % 48.68/48.93 (assume @p524 (forall @t96 (= (= @t623 (|tptp.'fun_app$b'| @t81 @t80)) (or (= @t12 @t80) (= @t12 @t595))))) % 48.68/48.93 (assume @p525 (forall @t8 (= (= @t461 (|tptp.'fun_app$a'| @t85 @t5)) (or @t149 (= @t6 @t593))))) % 48.68/48.93 (assume @p526 (forall @t4 (= (= @t462 @t624) (or @t25 @t622)))) % 48.68/48.93 (assume @p527 (forall @t8 (=> @t410 (<= @t593 @t592)))) % 48.68/48.93 (assume @p528 (forall @t4 (=> @t412 (<= @t591 @t590)))) % 48.68/48.93 (assume @p529 (forall @t8 (= (<= @t592 @t5) (<= @t593 @t6)))) % 48.68/48.93 (assume @p530 (forall @t4 (= (<= @t590 @t1) (<= @t591 @t2)))) % 48.68/48.93 (assume @p531 (forall @t8 (= (<= @t6 @t593) (<= @t5 @t592)))) % 48.68/48.93 (assume @p532 (forall @t4 (= (<= @t2 @t591) (<= @t1 @t590)))) % 48.68/48.93 (assume @p533 (not (= 0 @t614))) % 48.68/48.93 (assume @p534 (not (= 0/1 @t589))) % 48.68/48.93 (assume @p535 (not (<= 1 @t614))) % 48.68/48.93 (assume @p536 (not (<= 1/1 @t589))) % 48.68/48.93 (assume @p537 (<= @t614 1)) % 48.68/48.93 (assume @p538 (<= @t589 1/1)) % 48.68/48.93 (assume @p539 (forall @t13 (= (= @t623 |tptp.'one$'|) (or @t188 (= @t12 @t613))))) % 48.68/48.93 (assume @p540 (forall @t17 (= (= @t461 1) (or @t104 (= @t6 @t614))))) % 48.68/48.93 (assume @p541 @t629) % 48.68/48.93 (assume @p542 (forall @t4 (=> @t115 (= (|tptp.'fun_app$'| (|tptp.'divide$a'| @t591) @t590) @t534)))) % 48.68/48.93 (assume @p543 (forall @t4 (=> @t115 (= @t630 (|tptp.'fun_app$'| @t513 @t590))))) % 48.68/48.93 (assume @p544 (forall @t21 (= @t114 (and @t438 @t612)))) % 48.68/48.93 (assume @p545 (forall @t632 (=> @t40 (|tptp.'member$a'| @t592 @t631)))) % 48.68/48.93 (assume @p546 (forall @t634 (=> @t55 (|tptp.'member$c'| @t590 @t633)))) % 48.68/48.93 (assume @p547 (forall @t632 (=> (|tptp.'member$a'| @t6 @t631) (|tptp.'member$a'| @t592 @t35)))) % 48.68/48.93 (assume @p548 (forall @t634 (=> (|tptp.'member$c'| @t2 @t633) (|tptp.'member$c'| @t590 @t50)))) % 48.68/48.93 (assume @p549 (not (<= 0 @t614))) % 48.68/48.93 (assume @p550 (not (<= 0/1 @t589))) % 48.68/48.93 (assume @p551 (<= @t614 0)) % 48.68/48.93 (assume @p552 (<= @t589 0/1)) % 48.68/48.93 (assume @p553 (forall @t77 (= (= @t2 (- @t514)) (and (=> @t532 (= @t54 @t591)) @t533)))) % 48.68/48.93 (assume @p554 (forall @t77 (= (= @t620 @t52) (and (=> @t219 (= @t590 @t126)) @t531)))) % 48.68/48.93 (assume @p555 (forall @t77 (=> @t115 (= (= @t630 @t52) (= @t591 @t134))))) % 48.68/48.93 (assume @p556 (forall @t77 (=> @t115 (= (= @t1 (- @t530)) (= @t102 @t635))))) % 48.68/48.93 (assume @p557 (forall @t4 (= (= @t505 @t589) (and @t219 @t622)))) % 48.68/48.93 (assume @p558 (forall @t77 (and (=> @t118 (= @t636 @t635)) (=> @t219 (= @t636 (|tptp.'fun_app$'| (|tptp.'divide$a'| (- @t590 @t126)) @t1)))))) % 48.68/48.93 (assume @p559 (forall @t77 (and (=> @t118 (= @t637 @t635)) (=> @t219 (= @t637 (|tptp.'fun_app$'| (|tptp.'divide$a'| (- @t2 @t126)) @t1)))))) % 48.68/48.93 (assume @p560 (forall @t77 (=> @t115 (= (- @t630 @t52) (|tptp.'fun_app$'| (|tptp.'divide$a'| (- @t591 @t134)) @t2))))) % 48.68/48.93 (assume @p561 (forall @t17 (<= @t6 @t6))) % 48.68/48.93 (assume @p562 (forall @t21 (<= @t2 @t2))) % 48.68/48.93 (assume @p563 (forall @t8 (= (not @t410) (and @t306 (not @t638))))) % 48.68/48.93 (assume @p564 (forall @t4 (= (not @t412) (and @t307 (not @t523))))) % 48.68/48.93 (assume @p565 (forall @t88 (=> (and (=> @t643 false) (=> (and @t306 @t642) false) (=> (and @t642 @t641) false) (=> (and @t641 @t306) false) (=> (and @t640 @t639) false) (=> (and @t639 @t410) false)) false))) % 48.68/48.93 (assume @p566 (forall @t77 (=> (and (=> @t648 false) (=> (and @t307 @t647) false) (=> (and @t647 @t646) false) (=> (and @t646 @t307) false) (=> (and @t645 @t644) false) (=> (and @t644 @t412) false)) false))) % 48.68/48.93 (assume @p567 (forall @t8 (= @t149 @t649))) % 48.68/48.93 (assume @p568 (forall @t4 (= @t25 @t650))) % 48.68/48.93 (assume @p569 (forall @t88 (=> (and @t149 @t640) @t642))) % 48.68/48.93 (assume @p570 (forall @t77 (=> (and @t25 @t645) @t647))) % 48.68/48.93 (assume @p571 (forall @t88 (=> (and @t410 @t202) @t642))) % 48.68/48.93 (assume @p572 (forall @t77 (=> (and @t412 @t122) @t647))) % 48.68/48.93 (assume @p573 (forall @t8 (=> @t649 @t149))) % 48.68/48.93 (assume @p574 (forall @t4 (=> @t650 @t25))) % 48.68/48.93 (assume @p575 (forall @t88 (=> @t643 @t642))) % 48.68/48.93 (assume @p576 (forall @t77 (=> @t648 @t647))) % 48.68/48.93 (assume @p577 (forall (@list @t651 @t5 @t37) (=> (and (forall @t65 (=> (<= @t64 @t63) @t652)) (forall @t65 (=> (|tptp.'fun_app$m'| (|tptp.'fun_app$n'| @t651 @t63) @t64) @t652))) (|tptp.'fun_app$m'| (|tptp.'fun_app$n'| @t651 @t5) @t37)))) % 48.68/48.93 (assume @p578 (forall (@list @t653 @t1 @t52) (=> (and (forall @t73 (=> (<= @t71 @t70) @t654)) (forall @t73 (=> (|tptp.'fun_app$o'| (|tptp.'fun_app$p'| @t653 @t70) @t71) @t654))) (|tptp.'fun_app$o'| (|tptp.'fun_app$p'| @t653 @t1) @t52)))) % 48.68/48.93 (assume @p579 (forall @t8 (= @t149 (and @t306 @t410)))) % 48.68/48.93 (assume @p580 (forall @t4 (= @t25 (and @t307 @t412)))) % 48.68/48.93 (assume @p581 (forall @t8 (=> @t649 @t638))) % 48.68/48.93 (assume @p582 (forall @t4 (=> @t650 @t523))) % 48.68/48.93 (assume @p583 (forall @t88 (=> (and @t410 @t639) @t641))) % 48.68/48.93 (assume @p584 (forall @t77 (=> (and @t412 @t644) @t646))) % 48.68/48.93 (assume @p585 (forall @t4 (<= (- @t462) @t624))) % 48.68/48.93 (assume @p586 (forall @t20 (= (|tptp.'nat$'| @t240) @t18))) % 48.68/48.93 (assume @p587 @t662) % 48.68/48.93 (assume @p588 (forall (@list @t663) (or (= @t663 tptp.tltrue) (= @t663 tptp.tlfalse)))) % 48.68/48.93 (assume @p589 (not (= tptp.tltrue tptp.tlfalse))) % 48.68/48.93 (assume @p590 true) % 48.68/48.93 (step @p591 :rule symm :premises (@p83)) % 48.68/48.93 (step @p592 :rule symm :premises (@p84)) % 48.68/48.93 (step @p593 :rule symm :premises (@p87)) % 48.68/48.93 (step @p594 :rule symm :premises (@p188)) % 48.68/48.93 (step @p595 :rule eq-symm :args (@t15 @t12)) % 48.68/48.93 (step @p596 :rule cong :premises (@p595) :args (@t16)) % 48.68/48.93 (step @p597 :rule eq_resolve :premises (@p5 @p596)) % 48.68/48.93 (step @p598 :rule instantiate :premises (@p597) :args (@t664)) % 48.68/48.93 (step @p599 :rule refl :args (@t665)) % 48.68/48.93 (step @p600 :rule bool-double-not-elim :args (@t114)) % 48.68/48.93 (step @p601 :rule nary_cong :premises (@p600 @p599) :args ((or @t666 @t665))) % 48.68/48.93 (step @p602 :rule bool-impl-elim :args (@t115 @t665)) % 48.68/48.93 (step @p603 :rule trans :premises (@p602 @p601)) % 48.68/48.93 (step @p604 :rule cong :premises (@p603) :args ((forall @t21 (=> @t115 @t665)))) % 48.68/48.93 (step @p605 :rule eq-symm :args (@t113 |tptp.'fps_X$'|)) % 48.68/48.93 (step @p606 :rule refl :args (@t115)) % 48.68/48.93 (step @p607 :rule cong :premises (@p606 @p605) :args (@t116)) % 48.68/48.93 (step @p608 :rule cong :premises (@p607) :args (@t117)) % 48.68/48.93 (step @p609 :rule trans :premises (@p608 @p604)) % 48.68/48.93 (step @p610 :rule eq_resolve :premises (@p59 @p609)) % 48.68/48.93 (step @p611 :rule aci_norm :args ((= (or false @t669) @t669))) % 48.68/48.93 (step @p612 :rule refl :args (@t669)) % 48.68/48.93 (step @p613 :rule evaluate :args (@t670)) % 48.68/48.93 (step @p614 :rule nary_cong :premises (@p613 @p612) :args (@t671)) % 48.68/48.93 (step @p615 :rule trans :premises (@p614 @p611)) % 48.68/48.93 (step @p616 :rule refl :args (@t672)) % 48.68/48.93 (step @p617 :rule cong :premises (@p616 @p615) :args ((=> @t672 @t671))) % 48.68/48.93 (assume-push @p1309 @t672) % 48.68/48.93 (step @p619 :rule instantiate :premises (@p610) :args (@t673)) % 48.68/48.93 (step-pop @p1310 :rule scope :premises (@p619)) % 48.68/48.93 (step @p620 :rule process_scope :premises (@p1310) :args (@t671)) % 48.68/48.93 (step @p622 :rule eq_resolve :premises (@p620 @p617)) % 48.68/48.93 (step @p623 :rule implies_elim :premises (@p622)) % 48.68/48.93 (step @p624 :rule chain_m_resolution :premises (@p623 @p610) :args (@t669 @t674 (@list @t672))) % 48.68/48.93 (step @p625 :rule eq-symm :args (@t170 |tptp.'zero$'|)) % 48.68/48.93 (step @p626 :rule cong :premises (@p625) :args (@t191)) % 48.68/48.93 (step @p627 :rule eq_resolve :premises (@p137 @p626)) % 48.68/48.93 (step @p628 :rule instantiate :premises (@p627) :args (@t664)) % 48.68/48.93 (step @p629 :rule refl :args (@t675)) % 48.68/48.93 (step @p630 :rule nary_cong :premises (@p600 @p629) :args ((or @t666 @t675))) % 48.68/48.93 (step @p631 :rule bool-impl-elim :args (@t115 @t675)) % 48.68/48.93 (step @p632 :rule trans :premises (@p631 @p630)) % 48.68/48.93 (step @p633 :rule cong :premises (@p632) :args ((forall @t21 (=> @t115 @t675)))) % 48.68/48.93 (step @p634 :rule eq-symm :args (@t235 @t112)) % 48.68/48.93 (step @p635 :rule cong :premises (@p606 @p634) :args (@t236)) % 48.68/48.93 (step @p636 :rule cong :premises (@p635) :args (@t237)) % 48.68/48.93 (step @p637 :rule trans :premises (@p636 @p633)) % 48.68/48.93 (step @p638 :rule eq_resolve :premises (@p184 @p637)) % 48.68/48.93 (step @p639 :rule aci_norm :args ((= (or false @t677) @t677))) % 48.68/48.93 (step @p640 :rule refl :args (@t677)) % 48.68/48.93 (step @p641 :rule nary_cong :premises (@p613 @p640) :args (@t678)) % 48.68/48.93 (step @p642 :rule trans :premises (@p641 @p639)) % 48.68/48.93 (step @p643 :rule refl :args (@t679)) % 48.68/48.93 (step @p644 :rule cong :premises (@p643 @p642) :args ((=> @t679 @t678))) % 48.68/48.93 (assume-push @p1311 @t679) % 48.68/48.93 (step @p646 :rule instantiate :premises (@p638) :args (@t673)) % 48.68/48.93 (step-pop @p1312 :rule scope :premises (@p646)) % 48.68/48.93 (step @p647 :rule process_scope :premises (@p1312) :args (@t678)) % 48.68/48.93 (step @p649 :rule eq_resolve :premises (@p647 @p644)) % 48.68/48.93 (step @p650 :rule implies_elim :premises (@p649)) % 48.68/48.93 (step @p651 :rule chain_m_resolution :premises (@p650 @p638) :args (@t677 @t674 (@list @t679))) % 48.68/48.93 (step @p652 :rule arith_poly_norm :args ((= @t590 @t680))) % 48.68/48.93 (step @p653 :rule cong :premises (@p652) :args (@t615)) % 48.68/48.93 (step @p654 :rule refl :args (@t617)) % 48.68/48.93 (step @p655 :rule cong :premises (@p654 @p653) :args (@t618)) % 48.68/48.93 (step @p656 :rule cong :premises (@p655) :args (@t619)) % 48.68/48.93 (step @p657 :rule eq_resolve :premises (@p509 @p656)) % 48.68/48.93 (step @p658 :rule eq-symm :args (@t681 @t147)) % 48.68/48.93 (step @p659 :rule evaluate :args (@t682)) % 48.68/48.93 (step @p660 :rule cong :premises (@p659) :args (@t683)) % 48.68/48.93 (step @p661 :rule refl :args (@t681)) % 48.68/48.93 (step @p662 :rule cong :premises (@p661 @p660) :args (@t684)) % 48.68/48.93 (step @p663 :rule trans :premises (@p662 @p658)) % 48.68/48.93 (step @p664 :rule refl :args (@t685)) % 48.68/48.93 (step @p665 :rule cong :premises (@p664 @p663) :args ((=> @t685 @t684))) % 48.68/48.93 (assume-push @p1313 @t685) % 48.68/48.93 (step @p667 :rule instantiate :premises (@p657) :args ((@list 0/1))) % 48.68/48.93 (step-pop @p1314 :rule scope :premises (@p667)) % 48.68/48.93 (step @p668 :rule process_scope :premises (@p1314) :args (@t684)) % 48.68/48.93 (step @p670 :rule eq_resolve :premises (@p668 @p665)) % 48.68/48.93 (step @p671 :rule implies_elim :premises (@p670)) % 48.68/48.93 (step @p672 :rule chain_m_resolution :premises (@p671 @p657) :args (@t686 @t674 (@list @t685))) % 48.68/48.93 (step @p673 :rule instantiate :premises (@p19) :args ((@list |tptp.'zero$'|))) % 48.68/48.93 (step @p674 :rule arith_poly_norm :args ((= (* 1/1 (- @t319 @t299)) (* -1/1 (- @t299 @t319))))) % 48.68/48.93 (step @p675 :rule arith_poly_norm_rel :premises (@p674) :args ((= @t320 (= @t299 @t319)))) % 48.68/48.93 (step @p676 :rule cong :premises (@p675) :args (@t321)) % 48.68/48.93 (step @p677 :rule eq_resolve :premises (@p235 @p676)) % 48.68/48.93 (step @p678 :rule instantiate :premises (@p677) :args ((@list @t667 @t245))) % 48.68/48.93 (step @p679 :rule instantiate :premises (@p247) :args ((@list |tptp.'fps_X$'| 1/1 @t293))) % 48.68/48.93 (step @p680 :rule instantiate :premises (@p253) :args (@t673)) % 48.68/48.93 (step @p681 :rule eq-symm :args (@t687 @t690)) % 48.68/48.93 (step @p682 :rule refl :args (@t353)) % 48.68/48.93 (step @p683 :rule cong :premises (@p682 @p681) :args ((=> @t353 @t691))) % 48.68/48.93 (assume-push @p1315 @t353) % 48.68/48.93 (step @p685 :rule instantiate :premises (@p261) :args (@t692)) % 48.68/48.93 (step-pop @p1316 :rule scope :premises (@p685)) % 48.68/48.93 (step @p686 :rule process_scope :premises (@p1316) :args (@t691)) % 48.68/48.93 (step @p688 :rule eq_resolve :premises (@p686 @p683)) % 48.68/48.93 (step @p689 :rule implies_elim :premises (@p688)) % 48.68/48.93 (step @p690 :rule chain_m_resolution :premises (@p689 @p261) :args (@t693 @t674 (@list @t353))) % 48.68/48.93 (step @p691 :rule alpha_equiv :args (@t696 @t697 (@list (@var "BOUND_VARIABLE_16154" Int)))) % 48.68/48.93 (step @p692 :rule alpha_equiv :args (@t701 @t697 (@list @t702))) % 48.68/48.93 (step @p693 :rule nary_cong :premises (@p692 @p691) :args (@t703)) % 48.68/48.93 (step @p694 :rule quant-miniscope-and :args ((= (forall @t17 (and @t700 @t695)) @t703))) % 48.68/48.93 (step @p695 :rule trans :premises (@p694 @p693)) % 48.68/48.93 (step @p696 :rule refl :args (@t656)) % 48.68/48.93 (step @p697 :rule bool-double-not-elim :args (@t694)) % 48.68/48.93 (step @p698 :rule nary_cong :premises (@p697 @p696) :args ((or (not @t699) @t656))) % 48.68/48.93 (step @p699 :rule bool-impl-elim :args (@t699 @t656)) % 48.68/48.93 (step @p700 :rule trans :premises (@p699 @p698)) % 48.68/48.93 (step @p701 :rule bool-impl-elim :args (@t694 @t698)) % 48.68/48.93 (step @p702 :rule nary_cong :premises (@p701 @p700) :args (@t704)) % 48.68/48.93 (step @p703 :rule cong :premises (@p702) :args ((forall @t17 @t704))) % 48.68/48.93 (step @p704 :rule trans :premises (@p703 @p695)) % 48.68/48.93 (step @p705 :rule refl :args (@t656)) % 48.68/48.93 (step @p706 :rule arith-elim-leq :args (0 @t6)) % 48.68/48.93 (step @p707 :rule cong :premises (@p706) :args (@t657)) % 48.68/48.93 (step @p708 :rule cong :premises (@p707 @p705) :args (@t658)) % 48.68/48.93 (step @p709 :rule arith_poly_norm :args ((= (* 1 (- @t655 @t6)) (* -1 (- @t6 @t655))))) % 48.68/48.93 (step @p710 :rule arith_poly_norm_rel :premises (@p709) :args ((= @t659 @t698))) % 48.68/48.93 (step @p711 :rule cong :premises (@p706 @p710) :args (@t660)) % 48.68/48.93 (step @p712 :rule nary_cong :premises (@p711 @p708) :args (@t661)) % 48.68/48.93 (step @p713 :rule cong :premises (@p712) :args (@t662)) % 48.68/48.93 (step @p714 :rule trans :premises (@p713 @p704)) % 48.68/48.93 (step @p715 :rule eq_resolve :premises (@p587 @p714)) % 48.68/48.93 (step @p716 :rule and_elim :premises (@p715) :args (0)) % 48.68/48.93 (step @p717 :rule aci_norm :args ((= (or false @t706) @t706))) % 48.68/48.93 (step @p718 :rule arith_poly_norm :args ((= (* -1 (- 1 @t705)) @t707))) % 48.68/48.93 (step @p719 :rule arith_poly_norm_rel :premises (@p718) :args ((= @t708 @t706))) % 48.68/48.93 (step @p720 :rule evaluate :args ((not true))) % 48.68/48.93 (step @p721 :rule evaluate :args (@t709)) % 48.68/48.93 (step @p722 :rule cong :premises (@p721) :args (@t710)) % 48.68/48.93 (step @p723 :rule trans :premises (@p722 @p720)) % 48.68/48.93 (step @p724 :rule nary_cong :premises (@p723 @p719) :args (@t711)) % 48.68/48.93 (step @p725 :rule trans :premises (@p724 @p717)) % 48.68/48.93 (step @p726 :rule refl :args (@t712)) % 48.68/48.93 (step @p727 :rule cong :premises (@p726 @p725) :args ((=> @t712 @t711))) % 48.68/48.93 (assume-push @p1317 @t712) % 48.68/48.93 (step @p729 :rule instantiate :premises (@p716) :args ((@list 1))) % 48.68/48.93 (step-pop @p1318 :rule scope :premises (@p729)) % 48.68/48.93 (step @p730 :rule process_scope :premises (@p1318) :args (@t711)) % 48.68/48.93 (step @p732 :rule eq_resolve :premises (@p730 @p727)) % 48.68/48.93 (step @p733 :rule implies_elim :premises (@p732)) % 48.68/48.93 (step @p734 :rule chain_m_resolution :premises (@p733 @p716) :args (@t706 @t674 @t713)) % 48.68/48.93 (step @p735 :rule aci_norm :args ((= (or (or @t350 @t297) @t714) (or @t350 @t297 @t714)))) % 48.68/48.93 (step @p736 :rule refl :args (@t714)) % 48.68/48.93 (step @p737 :rule bool-double-not-elim :args (@t297)) % 48.68/48.93 (step @p738 :rule refl :args (@t350)) % 48.68/48.93 (step @p739 :rule nary_cong :premises (@p738 @p737) :args ((or @t350 (not @t298)))) % 48.68/48.93 (step @p740 :rule bool-and-de-morgan :args (@t300 @t298 true)) % 48.68/48.93 (step @p741 :rule trans :premises (@p740 @p739)) % 48.68/48.93 (step @p742 :rule nary_cong :premises (@p741 @p736) :args ((or (not @t487) @t714))) % 48.68/48.93 (step @p743 :rule trans :premises (@p742 @p735)) % 48.68/48.93 (step @p744 :rule bool-impl-elim :args (@t487 @t714)) % 48.68/48.93 (step @p745 :rule trans :premises (@p744 @p743)) % 48.68/48.93 (step @p746 :rule cong :premises (@p745) :args ((forall @t96 (=> @t487 @t714)))) % 48.68/48.93 (step @p747 :rule eq-symm :args (@t499 @t80)) % 48.68/48.93 (step @p748 :rule refl :args (@t487)) % 48.68/48.93 (step @p749 :rule cong :premises (@p748 @p747) :args (@t500)) % 48.68/48.93 (step @p750 :rule cong :premises (@p749) :args (@t501)) % 48.68/48.93 (step @p751 :rule trans :premises (@p750 @p746)) % 48.68/48.93 (step @p752 :rule eq_resolve :premises (@p379 @p751)) % 48.68/48.93 (step @p753 :rule instantiate :premises (@p752) :args ((@list @t11 |tptp.'fps_X$'|))) % 48.68/48.93 (step @p754 :rule symm :premises (@p3)) % 48.68/48.93 (step @p755 :rule false_intro :premises (@p754)) % 48.68/48.93 (step @p756 :rule refl :args (@t11)) % 48.68/48.93 (step @p757 :rule symm :premises (@p13)) % 48.68/48.93 (step @p758 :rule cong :premises (@p757 @p756) :args ((|tptp.'fps_compose$'| @t24 @t11))) % 48.68/48.93 (step @p759 :rule symm :premises (@p42)) % 48.68/48.93 (step @p760 :rule cong :premises (@p759 @p756) :args (@t715)) % 48.68/48.93 (step @p761 :rule cong :premises (@p760 @p756) :args (@t716)) % 48.68/48.93 (step @p762 :rule trans :premises (@p761 @p758)) % 48.68/48.93 (step @p763 :rule refl :args (|tptp.'fps_X$'|)) % 48.68/48.93 (step @p764 :rule cong :premises (@p763 @p762) :args (@t717)) % 48.68/48.93 (step @p765 :rule trans :premises (@p764 @p755)) % 48.68/48.93 (step @p766 :rule false_elim :premises (@p765)) % 48.68/48.93 (step @p767 :rule alpha_equiv :args (@t724 @t725 (@list (@var "BOUND_VARIABLE_12845" |tptp.'Real_fps$'|) (@var "BOUND_VARIABLE_12847" |tptp.'Nat$'|)))) % 48.68/48.93 (step @p768 :rule alpha_equiv :args (@t727 @t725 (@list (@var "BOUND_VARIABLE_12831" |tptp.'Real_fps$'|) (@var "BOUND_VARIABLE_12833" |tptp.'Nat$'|)))) % 48.68/48.93 (step @p769 :rule nary_cong :premises (@p768 @p767) :args (@t728)) % 48.68/48.93 (step @p770 :rule quant-miniscope-and :args ((= (forall @t372 (and @t726 @t723)) @t728))) % 48.68/48.93 (step @p771 :rule trans :premises (@p770 @p769)) % 48.68/48.93 (step @p772 :rule bool-impl-elim :args (@t720 @t719)) % 48.68/48.93 (step @p773 :rule refl :args (@t722)) % 48.68/48.93 (step @p774 :rule bool-double-not-elim :args (@t720)) % 48.68/48.93 (step @p775 :rule nary_cong :premises (@p774 @p773) :args ((or (not @t721) @t722))) % 48.68/48.93 (step @p776 :rule bool-impl-elim :args (@t721 @t722)) % 48.68/48.93 (step @p777 :rule trans :premises (@p776 @p775)) % 48.68/48.93 (step @p778 :rule nary_cong :premises (@p777 @p772) :args (@t729)) % 48.68/48.93 (step @p779 :rule refl :args (@t247)) % 48.68/48.93 (step @p780 :rule nary_cong :premises (@p779 @p778) :args ((or @t247 @t729))) % 48.68/48.93 (step @p781 :rule refl :args (@t729)) % 48.68/48.93 (step @p782 :rule bool-double-not-elim :args (@t247)) % 48.68/48.93 (step @p783 :rule nary_cong :premises (@p782 @p781) :args ((or @t730 @t729))) % 48.68/48.93 (step @p784 :rule bool-impl-elim :args (@t335 @t729)) % 48.68/48.93 (step @p785 :rule trans :premises (@p784 @p783)) % 48.68/48.93 (step @p786 :rule trans :premises (@p785 @p780)) % 48.68/48.93 (step @p787 :rule bool-impl-elim :args (@t247 @t369)) % 48.68/48.93 (step @p788 :rule nary_cong :premises (@p787 @p786) :args (@t731)) % 48.68/48.93 (step @p789 :rule cong :premises (@p788) :args ((forall @t372 @t731))) % 48.68/48.93 (step @p790 :rule trans :premises (@p789 @p771)) % 48.68/48.93 (step @p791 :rule arith_poly_norm :args ((= (+ @t238 -1) @t718))) % 48.68/48.93 (step @p792 :rule evaluate :args (@t732)) % 48.68/48.93 (step @p793 :rule refl :args (@t238)) % 48.68/48.93 (step @p794 :rule nary_cong :premises (@p793 @p792) :args (@t733)) % 48.68/48.93 (step @p795 :rule trans :premises (@p794 @p791)) % 48.68/48.93 (step @p796 :rule arith_poly_norm :args ((= @t354 @t733))) % 48.68/48.93 (step @p797 :rule trans :premises (@p796 @p795)) % 48.68/48.93 (step @p798 :rule cong :premises (@p797) :args (@t355)) % 48.68/48.93 (step @p799 :rule refl :args (@t296)) % 48.68/48.93 (step @p800 :rule cong :premises (@p799 @p798) :args (@t361)) % 48.68/48.93 (step @p801 :rule refl :args (@t362)) % 48.68/48.93 (step @p802 :rule cong :premises (@p801 @p800) :args (@t363)) % 48.68/48.93 (step @p803 :rule arith-elim-lt :args (@t238 1)) % 48.68/48.93 (step @p804 :rule cong :premises (@p803) :args (@t359)) % 48.68/48.93 (step @p805 :rule trans :premises (@p804 @p774)) % 48.68/48.93 (step @p806 :rule cong :premises (@p805 @p802) :args (@t364)) % 48.68/48.93 (step @p807 :rule arith_poly_norm :args ((= (* 1/1 (- @t362 @t299)) (* -1/1 (- @t299 @t362))))) % 48.68/48.93 (step @p808 :rule arith_poly_norm_rel :premises (@p807) :args ((= @t365 @t722))) % 48.68/48.93 (step @p809 :rule cong :premises (@p803 @p808) :args (@t366)) % 48.68/48.93 (step @p810 :rule nary_cong :premises (@p809 @p806) :args (@t367)) % 48.68/48.93 (step @p811 :rule refl :args (@t335)) % 48.68/48.93 (step @p812 :rule cong :premises (@p811 @p810) :args (@t368)) % 48.68/48.93 (step @p813 :rule refl :args (@t370)) % 48.68/48.93 (step @p814 :rule nary_cong :premises (@p813 @p812) :args (@t371)) % 48.68/48.93 (step @p815 :rule cong :premises (@p814) :args (@t373)) % 48.68/48.93 (step @p816 :rule trans :premises (@p815 @p790)) % 48.68/48.93 (step @p817 :rule eq_resolve :premises (@p263 @p816)) % 48.68/48.93 (step @p818 :rule and_elim :premises (@p817) :args (0)) % 48.68/48.93 (step @p819 :rule instantiate :premises (@p818) :args ((@list @t9 @t293))) % 48.68/48.93 (step @p820 :rule aci_norm :args ((= (or false @t735) @t735))) % 48.68/48.93 (step @p821 :rule arith_poly_norm :args ((= (* 1 (- 0 @t734)) (* -1 (- @t734 0))))) % 48.68/48.93 (step @p822 :rule arith_poly_norm_rel :premises (@p821) :args ((= @t736 @t735))) % 48.68/48.93 (step @p823 :rule evaluate :args (@t737)) % 48.68/48.93 (step @p824 :rule cong :premises (@p823) :args (@t738)) % 48.68/48.93 (step @p825 :rule trans :premises (@p824 @p720)) % 48.68/48.93 (step @p826 :rule nary_cong :premises (@p825 @p822) :args (@t739)) % 48.68/48.93 (step @p827 :rule trans :premises (@p826 @p820)) % 48.68/48.93 (step @p828 :rule cong :premises (@p726 @p827) :args ((=> @t712 @t739))) % 48.68/48.93 (assume-push @p1319 @t712) % 48.68/48.93 (step @p830 :rule instantiate :premises (@p716) :args ((@list 0))) % 48.68/48.93 (step-pop @p1320 :rule scope :premises (@p830)) % 48.68/48.93 (step @p831 :rule process_scope :premises (@p1320) :args (@t739)) % 48.68/48.93 (step @p833 :rule eq_resolve :premises (@p831 @p828)) % 48.68/48.93 (step @p834 :rule implies_elim :premises (@p833)) % 48.68/48.93 (step @p835 :rule chain_m_resolution :premises (@p834 @p716) :args (@t735 @t674 @t713)) % 48.68/48.93 (step @p836 :rule cnf_or_pos :args (@t743)) % 48.68/48.93 (step @p837 :rule reordering :premises (@p836) :args ((or @t741 @t742 (not @t743)))) % 48.68/48.93 (step @p838 :rule chain_m_resolution :premises (@p837 @p835 @p819) :args (@t741 @t744 (@list @t735 @t743))) % 48.68/48.93 (step @p839 :rule cnf_or_pos :args (@t748)) % 48.68/48.93 (step @p840 :rule reordering :premises (@p839) :args ((or @t747 @t746 @t717 (not @t748)))) % 48.68/48.93 (step @p841 :rule chain_m_resolution :premises (@p840 @p838 @p766 @p753) :args (@t746 (@list false true false) (@list @t741 @t717 @t748))) % 48.68/48.93 (step @p842 :rule instantiate :premises (@p41) :args ((@list 1/1 0/1))) % 48.68/48.93 (step @p843 :rule instantiate :premises (@p677) :args ((@list @t9 |tptp.'zero$'|))) % 48.68/48.93 (step @p844 :rule alpha_equiv :args (@t750 @t751 (@list (@var "BOUND_VARIABLE_12621" Real) (@var "BOUND_VARIABLE_12623" |tptp.'Nat$'|)))) % 48.68/48.93 (step @p845 :rule alpha_equiv :args (@t754 @t751 (@list @t756 @t755))) % 48.68/48.93 (step @p846 :rule nary_cong :premises (@p845 @p844) :args (@t757)) % 48.68/48.93 (step @p847 :rule quant-miniscope-and :args ((= (forall @t342 (and @t753 @t749)) @t757))) % 48.68/48.93 (step @p848 :rule trans :premises (@p847 @p846)) % 48.68/48.93 (step @p849 :rule refl :args (@t337)) % 48.68/48.93 (step @p850 :rule nary_cong :premises (@p782 @p849) :args ((or @t730 @t337))) % 48.68/48.93 (step @p851 :rule bool-impl-elim :args (@t335 @t337)) % 48.68/48.93 (step @p852 :rule trans :premises (@p851 @p850)) % 48.68/48.93 (step @p853 :rule bool-impl-elim :args (@t247 @t752)) % 48.68/48.93 (step @p854 :rule nary_cong :premises (@p853 @p852) :args (@t758)) % 48.68/48.93 (step @p855 :rule cong :premises (@p854) :args ((forall @t342 @t758))) % 48.68/48.93 (step @p856 :rule trans :premises (@p855 @p848)) % 48.68/48.93 (step @p857 :rule refl :args (@t338)) % 48.68/48.93 (step @p858 :rule arith_poly_norm :args ((= (* 1/1 (- @t336 @t2)) (* -1/1 (- @t2 @t336))))) % 48.68/48.93 (step @p859 :rule arith_poly_norm_rel :premises (@p858) :args ((= @t339 @t752))) % 48.68/48.93 (step @p860 :rule refl :args (@t247)) % 48.68/48.93 (step @p861 :rule cong :premises (@p860 @p859) :args (@t340)) % 48.68/48.93 (step @p862 :rule nary_cong :premises (@p861 @p857) :args (@t341)) % 48.68/48.93 (step @p863 :rule cong :premises (@p862) :args (@t343)) % 48.68/48.93 (step @p864 :rule trans :premises (@p863 @p856)) % 48.68/48.93 (step @p865 :rule eq_resolve :premises (@p243 @p864)) % 48.68/48.93 (step @p866 :rule and_elim :premises (@p865) :args (0)) % 48.68/48.93 (step @p867 :rule arith_poly_norm :args ((= (* -1/1 (- 1/1 @t759)) (* 1/1 (- @t759 1/1))))) % 48.68/48.93 (step @p868 :rule arith_poly_norm_rel :premises (@p867) :args ((= @t761 @t760))) % 48.68/48.93 (step @p869 :rule refl :args (@t742)) % 48.68/48.93 (step @p870 :rule nary_cong :premises (@p869 @p868) :args (@t762)) % 48.68/48.93 (step @p871 :rule refl :args (@t763)) % 48.68/48.93 (step @p872 :rule cong :premises (@p871 @p870) :args ((=> @t763 @t762))) % 48.68/48.93 (assume-push @p1321 @t763) % 48.68/48.93 (step @p874 :rule instantiate :premises (@p866) :args ((@list 1/1 @t293))) % 48.68/48.93 (step-pop @p1322 :rule scope :premises (@p874)) % 48.68/48.93 (step @p875 :rule process_scope :premises (@p1322) :args (@t762)) % 48.68/48.93 (step @p877 :rule eq_resolve :premises (@p875 @p872)) % 48.68/48.93 (step @p878 :rule implies_elim :premises (@p877)) % 48.68/48.93 (step @p879 :rule chain_m_resolution :premises (@p878 @p866) :args (@t764 @t674 (@list @t763))) % 48.68/48.93 (step @p880 :rule cnf_or_pos :args (@t764)) % 48.68/48.93 (step @p881 :rule reordering :premises (@p880) :args ((or @t742 @t760 (not @t764)))) % 48.68/48.93 (step @p882 :rule chain_m_resolution :premises (@p881 @p835 @p879) :args (@t760 @t744 (@list @t735 @t764))) % 48.68/48.93 (step @p883 :rule and_elim :premises (@p817) :args (1)) % 48.68/48.93 (step @p884 :rule instantiate :premises (@p883) :args ((@list @t9 @t109))) % 48.68/48.93 (step @p885 :rule evaluate :args ((= 1 0))) % 48.68/48.93 (step @p886 :rule refl :args (0)) % 48.68/48.93 (step @p887 :rule cong :premises (@p734 @p886) :args (@t765)) % 48.68/48.93 (step @p888 :rule trans :premises (@p887 @p885)) % 48.68/48.93 (step @p889 :rule false_elim :premises (@p888)) % 48.68/48.93 (step @p890 :rule cnf_or_pos :args (@t776)) % 48.68/48.93 (step @p891 :rule reordering :premises (@p890) :args ((or @t765 @t775 (not @t776)))) % 48.68/48.93 (step @p892 :rule chain_m_resolution :premises (@p891 @p889 @p884) :args (@t775 @t777 (@list @t765 @t776))) % 48.68/48.93 (step @p893 :rule cnf_and_pos :args (@t775 1)) % 48.68/48.93 (step @p894 :rule reordering :premises (@p893) :args ((or @t772 @t778))) % 48.68/48.93 (step @p895 :rule chain_m_resolution :premises (@p894 @p892) :args (@t772 @t674 @t779)) % 48.68/48.93 (step @p896 :rule cnf_and_pos :args (@t775 0)) % 48.68/48.93 (step @p897 :rule reordering :premises (@p896) :args ((or @t774 @t778))) % 48.68/48.93 (step @p898 :rule chain_m_resolution :premises (@p897 @p892) :args (@t774 @t674 @t779)) % 48.68/48.93 (step @p899 :rule arith_poly_norm :args ((= (* 1/1 (- @t781 @t78)) (* -1/1 (- @t78 @t781))))) % 48.68/48.93 (step @p900 :rule arith_poly_norm_rel :premises (@p899) :args ((= (= @t781 @t78) @t782))) % 48.68/48.93 (step @p901 :rule refl :args (@t78)) % 48.68/48.93 (step @p902 :rule arith_poly_norm :args ((= @t591 @t780))) % 48.68/48.93 (step @p903 :rule refl :args (|tptp.'times$f'|)) % 48.68/48.93 (step @p904 :rule cong :premises (@p903 @p652) :args (@t604)) % 48.68/48.93 (step @p905 :rule cong :premises (@p904 @p902) :args (@t605)) % 48.68/48.93 (step @p906 :rule cong :premises (@p905 @p901) :args (@t606)) % 48.68/48.93 (step @p907 :rule trans :premises (@p906 @p900)) % 48.68/48.93 (step @p908 :rule cong :premises (@p907) :args (@t607)) % 48.68/48.93 (step @p909 :rule eq_resolve :premises (@p480 @p908)) % 48.68/48.93 (step @p910 :rule evaluate :args (@t783)) % 48.68/48.93 (step @p911 :rule cong :premises (@p903 @p910) :args (@t784)) % 48.68/48.93 (step @p912 :rule cong :premises (@p911 @p910) :args (@t785)) % 48.68/48.93 (step @p913 :rule refl :args (@t786)) % 48.68/48.93 (step @p914 :rule cong :premises (@p913 @p912) :args (@t787)) % 48.68/48.93 (step @p915 :rule refl :args (@t788)) % 48.68/48.93 (step @p916 :rule cong :premises (@p915 @p914) :args ((=> @t788 @t787))) % 48.68/48.93 (assume-push @p1323 @t788) % 48.68/48.93 (step @p918 :rule instantiate :premises (@p909) :args ((@list 1/1 1/1))) % 48.68/48.93 (step-pop @p1324 :rule scope :premises (@p918)) % 48.68/48.93 (step @p919 :rule process_scope :premises (@p1324) :args (@t787)) % 48.68/48.93 (step @p921 :rule eq_resolve :premises (@p919 @p916)) % 48.68/48.93 (step @p922 :rule implies_elim :premises (@p921)) % 48.68/48.93 (step @p923 :rule chain_m_resolution :premises (@p922 @p909) :args (@t790 @t674 (@list @t788))) % 48.68/48.93 (step @p924 :rule bool-eq-false :args (@t791)) % 48.68/48.93 (step @p925 :rule evaluate :args (@t792)) % 48.68/48.93 (step @p926 :rule evaluate :args (@t792)) % 48.68/48.93 (step @p927 :rule symm :premises (@p926)) % 48.68/48.93 (step @p928 :rule evaluate :args (@t793)) % 48.68/48.93 (step @p929 :rule trans :premises (@p928 @p927)) % 48.68/48.93 (step @p930 :rule trans :premises (@p929 @p925)) % 48.68/48.93 (step @p931 :rule refl :args (@t791)) % 48.68/48.93 (step @p932 :rule cong :premises (@p931 @p930) :args (@t794)) % 48.68/48.93 (step @p933 :rule trans :premises (@p932 @p924)) % 48.68/48.93 (step @p934 :rule refl :args (@t121)) % 48.68/48.93 (step @p935 :rule cong :premises (@p934 @p933) :args ((=> @t121 @t794))) % 48.68/48.93 (assume-push @p1325 @t121) % 48.68/48.93 (step @p937 :rule instantiate :premises (@p61) :args ((@list -1/1 -1/1))) % 48.68/48.93 (step-pop @p1326 :rule scope :premises (@p937)) % 48.68/48.93 (step @p938 :rule process_scope :premises (@p1326) :args (@t794)) % 48.68/48.93 (step @p940 :rule eq_resolve :premises (@p938 @p935)) % 48.68/48.93 (step @p941 :rule implies_elim :premises (@p940)) % 48.68/48.93 (step @p942 :rule chain_m_resolution :premises (@p941 @p61) :args (@t795 @t674 (@list @t121))) % 48.68/48.93 (step @p943 :rule evaluate :args (@t589)) % 48.68/48.93 (step @p944 :rule refl :args (@t2)) % 48.68/48.93 (step @p945 :rule cong :premises (@p944 @p943) :args (@t625)) % 48.68/48.93 (step @p946 :rule refl :args (@t103)) % 48.68/48.93 (step @p947 :rule nary_cong :premises (@p946 @p945) :args (@t626)) % 48.68/48.93 (step @p948 :rule refl :args (@t627)) % 48.68/48.93 (step @p949 :rule cong :premises (@p948 @p947) :args (@t628)) % 48.68/48.93 (step @p950 :rule cong :premises (@p949) :args (@t629)) % 48.68/48.93 (step @p951 :rule eq_resolve :premises (@p541 @p950)) % 48.68/48.93 (step @p952 :rule bool-eq-true :args (@t796)) % 48.68/48.93 (step @p953 :rule evaluate :args ((or true false))) % 48.68/48.93 (step @p954 :rule evaluate :args (@t797)) % 48.68/48.93 (step @p955 :rule evaluate :args (@t798)) % 48.68/48.93 (step @p956 :rule nary_cong :premises (@p955 @p954) :args (@t799)) % 48.68/48.93 (step @p957 :rule trans :premises (@p956 @p953)) % 48.68/48.93 (step @p958 :rule refl :args (@t796)) % 48.68/48.93 (step @p959 :rule cong :premises (@p958 @p957) :args (@t800)) % 48.68/48.93 (step @p960 :rule trans :premises (@p959 @p952)) % 48.68/48.93 (step @p961 :rule refl :args (@t801)) % 48.68/48.93 (step @p962 :rule cong :premises (@p961 @p960) :args ((=> @t801 @t800))) % 48.68/48.93 (assume-push @p1327 @t801) % 48.68/48.93 (step @p964 :rule instantiate :premises (@p951) :args (@t673)) % 48.68/48.93 (step-pop @p1328 :rule scope :premises (@p964)) % 48.68/48.93 (step @p965 :rule process_scope :premises (@p1328) :args (@t800)) % 48.68/48.93 (step @p967 :rule eq_resolve :premises (@p965 @p962)) % 48.68/48.93 (step @p968 :rule implies_elim :premises (@p967)) % 48.68/48.93 (step @p969 :rule chain_m_resolution :premises (@p968 @p951) :args (@t796 @t674 (@list @t801))) % 48.68/48.93 (step @p970 :rule refl :args (@t802)) % 48.68/48.93 (step @p971 :rule refl :args (@t803)) % 48.68/48.93 (step @p972 :rule refl :args (@t804)) % 48.68/48.93 (step @p973 :rule refl :args (@t808)) % 48.68/48.93 (step @p974 :rule bool-double-not-elim :args (@t791)) % 48.68/48.93 (step @p975 :rule refl :args (@t815)) % 48.68/48.93 (step @p976 :rule refl :args (@t816)) % 48.68/48.93 (step @p977 :rule refl :args (@t817)) % 48.68/48.93 (step @p978 :rule refl :args (@t820)) % 48.68/48.93 (step @p979 :rule refl :args (@t826)) % 48.68/48.93 (step @p980 :rule refl :args (@t831)) % 48.68/48.93 (step @p981 :rule refl :args (@t835)) % 48.68/48.93 (step @p982 :rule refl :args (@t836)) % 48.68/48.93 (step @p983 :rule refl :args (@t837)) % 48.68/48.93 (step @p984 :rule refl :args (@t838)) % 48.68/48.93 (step @p985 :rule refl :args (@t840)) % 48.68/48.93 (step @p986 :rule refl :args (@t841)) % 48.68/48.93 (step @p987 :rule refl :args (@t844)) % 48.68/48.93 (step @p988 :rule refl :args (@t846)) % 48.68/48.93 (step @p989 :rule refl :args (@t848)) % 48.68/48.93 (step @p990 :rule refl :args (@t850)) % 48.68/48.93 (step @p991 :rule refl :args (@t852)) % 48.68/48.93 (step @p992 :rule nary_cong :premises (@p991 @p990 @p989 @p988 @p987 @p986 @p985 @p984 @p983 @p982 @p981 @p980 @p979 @p978 @p977 @p976 @p975 @p974 @p973 @p972 @p971 @p970) :args ((or @t852 @t850 @t848 @t846 @t844 @t841 @t840 @t838 @t837 @t836 @t835 @t831 @t826 @t820 @t817 @t816 @t815 (not @t795) @t808 @t804 @t803 @t802))) % 48.68/48.93 (assume-push @p1329 @t851) % 48.68/48.93 (assume-push @p1330 @t849) % 48.68/48.93 (assume-push @p1331 @t847) % 48.68/48.93 (assume-push @p1332 @t845) % 48.68/48.93 (assume-push @p1333 @t843) % 48.68/48.93 (assume-push @p1334 @t669) % 48.68/48.93 (assume-push @p1335 @t839) % 48.68/48.93 (assume-push @p1336 @t677) % 48.68/48.93 (assume-push @p1337 @t746) % 48.68/48.93 (assume-push @p1338 @t686) % 48.68/48.93 (assume-push @p1339 @t834) % 48.68/48.93 (assume-push @p1340 @t830) % 48.68/48.93 (assume-push @p1341 @t825) % 48.68/48.93 (assume-push @p1342 @t819) % 48.68/48.93 (assume-push @p1343 @t693) % 48.68/48.93 (assume-push @p1344 @t796) % 48.68/48.93 (assume-push @p1345 @t814) % 48.68/48.93 (assume-push @p1346 @t795) % 48.68/48.93 (assume-push @p1347 @t807) % 48.68/48.93 (assume-push @p1348 @t760) % 48.68/48.93 (assume-push @p1349 @t790) % 48.68/48.93 (assume-push @p1350 @t807) % 48.68/48.93 (assume-push @p1351 @t855) % 48.68/48.93 (assume-push @p1352 @t760) % 48.68/48.93 (assume-push @p1353 @t795) % 48.68/48.93 (assume-push @p1354 (= @t854 @t759)) % 48.68/48.93 (assume-push @p1355 @t796) % 48.68/48.93 (assume-push @p1356 @t790) % 48.68/48.93 (assume-push @p1357 @t746) % 48.68/48.93 (step @p1022 :rule false_intro :premises (@p942)) % 48.68/48.93 (step @p1023 :rule symm :premises (@p969)) % 48.68/48.93 (step @p1024 :rule refl :args (@t293)) % 48.68/48.93 (step @p1025 :rule cong :premises (@p592) :args (@t345)) % 48.68/48.93 (step @p1026 :rule cong :premises (@p1025 @p1024) :args (@t856)) % 48.68/48.93 (step @p1027 :rule symm :premises (@p672)) % 48.68/48.93 (step @p1028 :rule trans :premises (@p1027 @p87)) % 48.68/48.93 (step @p1029 :rule cong :premises (@p1028) :args (@t853)) % 48.68/48.93 (step @p1030 :rule cong :premises (@p1029 @p1024) :args (@t854)) % 48.68/48.93 (step @p1031 :rule trans :premises (@p1030 @p1026)) % 48.68/48.93 (step @p1032 :rule symm :premises (@p1351)) % 48.68/48.93 (step @p1033 :rule trans :premises (@p843 @p1032 @p1031 @p882 @p1023 @p923)) % 48.68/48.93 (step @p1034 :rule cong :premises (@p1033 @p841) :args (@t773)) % 48.68/48.93 (step @p1035 :rule trans :premises (@p1034 @p1022)) % 48.68/48.93 (step @p1036 :rule false_elim :premises (@p1035)) % 48.68/48.93 (step-pop @p1358 :rule scope :premises (@p1036)) % 48.68/48.93 (step-pop @p1359 :rule scope :premises (@p1358)) % 48.68/48.93 (step-pop @p1360 :rule scope :premises (@p1359)) % 48.68/48.93 (step-pop @p1361 :rule scope :premises (@p1360)) % 48.68/48.93 (step-pop @p1362 :rule scope :premises (@p1361)) % 48.68/48.93 (step-pop @p1363 :rule scope :premises (@p1362)) % 48.68/48.93 (step-pop @p1364 :rule scope :premises (@p1363)) % 48.68/48.93 (step-pop @p1365 :rule scope :premises (@p1364)) % 48.68/48.93 (step @p1037 :rule process_scope :premises (@p1365) :args (@t802)) % 48.68/48.93 (step @p1024 :rule refl :args (@t293)) % 48.68/48.93 (step @p1025 :rule cong :premises (@p592) :args (@t345)) % 48.68/48.93 (step @p1026 :rule cong :premises (@p1025 @p1024) :args (@t856)) % 48.68/48.93 (step @p1027 :rule symm :premises (@p672)) % 48.68/48.93 (step @p1028 :rule trans :premises (@p1027 @p87)) % 48.68/48.93 (step @p1029 :rule cong :premises (@p1028) :args (@t853)) % 48.68/48.93 (step @p1030 :rule cong :premises (@p1029 @p1024) :args (@t854)) % 48.68/48.93 (step @p1046 :rule trans :premises (@p1030 @p1026)) % 48.68/48.93 (assume-push @p1366 @t859) % 48.68/48.93 (assume-push @p1367 @t814) % 48.68/48.93 (assume-push @p1368 @t834) % 48.68/48.93 (assume-push @p1369 @t860) % 48.68/48.93 (assume-push @p1370 @t693) % 48.68/48.93 (assume-push @p1371 @t686) % 48.68/48.93 (assume-push @p1372 @t839) % 48.68/48.93 (assume-push @p1373 @t851) % 48.68/48.93 (assume-push @p1374 @t845) % 48.68/48.93 (assume-push @p1375 @t847) % 48.68/48.93 (step @p1057 :rule cong :premises (@p690) :args (@t861)) % 48.68/48.93 (step @p685 :rule instantiate :premises (@p261) :args (@t692)) % 48.68/48.93 (step @p1058 :rule symm :premises (@p628)) % 48.68/48.93 (step @p1059 :rule symm :premises (@p673)) % 48.68/48.93 (step @p1060 :rule refl :args (|tptp.'times$'|)) % 48.68/48.93 (step @p1061 :rule cong :premises (@p1060 @p83) :args (@t811)) % 48.68/48.93 (step @p1062 :rule cong :premises (@p1061 @p763) :args (@t812)) % 48.68/48.93 (step @p1063 :rule trans :premises (@p1062 @p1059 @p1058)) % 48.68/48.93 (step @p1064 :rule refl :args (@t9)) % 48.68/48.93 (step @p1065 :rule cong :premises (@p1064 @p1063) :args (@t813)) % 48.68/48.93 (step @p1066 :rule symm :premises (@p842)) % 48.68/48.93 (step @p1067 :rule refl :args (1/1)) % 48.68/48.93 (step @p1068 :rule symm :premises (@p1369)) % 48.68/48.93 (step @p1069 :rule cong :premises (@p594) :args (@t348)) % 48.68/48.93 (step @p1070 :rule cong :premises (@p1069 @p1024) :args (@t821)) % 48.68/48.93 (step @p1071 :rule trans :premises (@p1070 @p1068)) % 48.68/48.93 (step @p1072 :rule cong :premises (@p903 @p1071) :args (@t822)) % 48.68/48.93 (step @p1073 :rule cong :premises (@p1072 @p1067) :args (@t823)) % 48.68/48.93 (step @p1074 :rule trans :premises (@p1369 @p1366 @p1073)) % 48.68/48.93 (step @p1075 :rule cong :premises (@p1074) :args (@t147)) % 48.68/48.93 (step @p1076 :rule trans :premises (@p593 @p1075 @p1066 @p1065 @p685)) % 48.68/48.93 (step @p1077 :rule cong :premises (@p1076) :args (@t345)) % 48.68/48.93 (step @p1078 :rule trans :premises (@p1077 @p1057)) % 48.68/48.93 (step @p1079 :rule cong :premises (@p1078 @p1024) :args (@t856)) % 48.68/48.93 (step @p1080 :rule trans :premises (@p1030 @p1079)) % 48.68/48.93 (step-pop @p1376 :rule scope :premises (@p1080)) % 48.68/48.93 (step-pop @p1377 :rule scope :premises (@p1376)) % 48.68/48.93 (step-pop @p1378 :rule scope :premises (@p1377)) % 48.68/48.93 (step-pop @p1379 :rule scope :premises (@p1378)) % 48.68/48.93 (step-pop @p1380 :rule scope :premises (@p1379)) % 48.68/48.93 (step-pop @p1381 :rule scope :premises (@p1380)) % 48.68/48.93 (step-pop @p1382 :rule scope :premises (@p1381)) % 48.68/48.93 (step-pop @p1383 :rule scope :premises (@p1382)) % 48.68/48.93 (step-pop @p1384 :rule scope :premises (@p1383)) % 48.68/48.93 (step-pop @p1385 :rule scope :premises (@p1384)) % 48.68/48.93 (step @p1081 :rule process_scope :premises (@p1385) :args (@t855)) % 48.68/48.93 (assume-push @p1386 @t862) % 48.68/48.93 (assume-push @p1387 @t830) % 48.68/48.93 (assume-push @p1388 @t863) % 48.68/48.93 (assume-push @p1389 @t819) % 48.68/48.93 (step @p1096 :rule refl :args (@t293)) % 48.68/48.93 (step @p1097 :rule cong :premises (@p624) :args (@t348)) % 48.68/48.93 (step @p1098 :rule cong :premises (@p188) :args (@t857)) % 48.68/48.93 (step @p1099 :rule trans :premises (@p1098 @p1097)) % 48.68/48.93 (step @p1100 :rule cong :premises (@p1099 @p1096) :args (@t858)) % 48.68/48.93 (step @p1101 :rule symm :premises (@p1100)) % 48.68/48.93 (step @p1102 :rule refl :args (@t293)) % 48.68/48.93 (step @p1103 :rule cong :premises (@p651) :args (@t828)) % 48.68/48.93 (step @p1104 :rule cong :premises (@p1103 @p1102) :args (@t829)) % 48.68/48.93 (step @p1105 :rule symm :premises (@p1104)) % 48.68/48.93 (step @p1106 :rule symm :premises (@p680)) % 48.68/48.93 (step @p1107 :rule trans :premises (@p1106 @p1105 @p678 @p1101)) % 48.68/48.93 (step-pop @p1390 :rule scope :premises (@p1107)) % 48.68/48.93 (step-pop @p1391 :rule scope :premises (@p1390)) % 48.68/48.93 (step-pop @p1392 :rule scope :premises (@p1391)) % 48.68/48.93 (step-pop @p1393 :rule scope :premises (@p1392)) % 48.68/48.93 (step @p1108 :rule process_scope :premises (@p1393) :args (@t860)) % 48.68/48.93 (step @p1103 :rule cong :premises (@p651) :args (@t828)) % 48.68/48.93 (step @p1113 :rule cong :premises (@p1103 @p1024) :args (@t829)) % 48.68/48.93 (step @p1097 :rule cong :premises (@p624) :args (@t348)) % 48.68/48.93 (step @p1098 :rule cong :premises (@p188) :args (@t857)) % 48.68/48.93 (step @p1099 :rule trans :premises (@p1098 @p1097)) % 48.68/48.93 (step @p1114 :rule cong :premises (@p1099 @p1024) :args (@t858)) % 48.68/48.93 (step @p1115 :rule and_intro :premises (@p1114 @p678 @p1113 @p680)) % 48.68/48.93 (step @p1116 :rule modus_ponens :premises (@p1115 @p1108)) % 48.68/48.93 (assume-push @p1394 @t825) % 48.68/48.93 (assume-push @p1395 @t864) % 48.68/48.93 (step @p1119 :rule refl :args (@t293)) % 48.68/48.93 (step @p1120 :rule refl :args (@t10)) % 48.68/48.93 (step @p1121 :rule cong :premises (@p1120 @p592) :args (@t842)) % 48.68/48.93 (step @p1122 :rule trans :premises (@p598 @p1121)) % 48.68/48.93 (step @p1123 :rule cong :premises (@p1122) :args (@t348)) % 48.68/48.93 (step @p1124 :rule trans :premises (@p1098 @p1123)) % 48.68/48.93 (step @p1125 :rule cong :premises (@p1124 @p1119) :args (@t858)) % 48.68/48.93 (step @p1126 :rule trans :premises (@p1125 @p679)) % 48.68/48.93 (step-pop @p1396 :rule scope :premises (@p1126)) % 48.68/48.93 (step-pop @p1397 :rule scope :premises (@p1396)) % 48.68/48.93 (step @p1127 :rule process_scope :premises (@p1397) :args (@t859)) % 48.68/48.93 (step @p1120 :rule refl :args (@t10)) % 48.68/48.93 (step @p1121 :rule cong :premises (@p1120 @p592) :args (@t842)) % 48.68/48.93 (step @p1122 :rule trans :premises (@p598 @p1121)) % 48.68/48.93 (step @p1123 :rule cong :premises (@p1122) :args (@t348)) % 48.68/48.93 (step @p1124 :rule trans :premises (@p1098 @p1123)) % 48.68/48.93 (step @p1130 :rule cong :premises (@p1124 @p1024) :args (@t858)) % 48.68/48.93 (step @p1131 :rule and_intro :premises (@p679 @p1130)) % 48.68/48.93 (step @p1132 :rule modus_ponens :premises (@p1131 @p1127)) % 48.68/48.93 (step @p1133 :rule and_intro :premises (@p1132 @p842 @p673 @p1116 @p690 @p672 @p628 @p591 @p594 @p593)) % 48.68/48.93 (step @p1134 :rule modus_ponens :premises (@p1133 @p1081)) % 48.68/48.93 (step @p1135 :rule and_intro :premises (@p843 @p1134 @p882 @p942 @p1046 @p969 @p923 @p841)) % 48.68/48.93 (step @p1136 :rule modus_ponens :premises (@p1135 @p1037)) % 48.68/48.93 (step-pop @p1398 :rule scope :premises (@p1136)) % 48.68/48.93 (step-pop @p1399 :rule scope :premises (@p1398)) % 48.68/48.93 (step-pop @p1400 :rule scope :premises (@p1399)) % 48.68/48.93 (step-pop @p1401 :rule scope :premises (@p1400)) % 48.68/48.93 (step-pop @p1402 :rule scope :premises (@p1401)) % 48.68/48.93 (step-pop @p1403 :rule scope :premises (@p1402)) % 48.68/48.93 (step-pop @p1404 :rule scope :premises (@p1403)) % 48.68/48.93 (step-pop @p1405 :rule scope :premises (@p1404)) % 48.68/48.93 (step-pop @p1406 :rule scope :premises (@p1405)) % 48.68/48.93 (step-pop @p1407 :rule scope :premises (@p1406)) % 48.68/48.93 (step-pop @p1408 :rule scope :premises (@p1407)) % 48.68/48.93 (step-pop @p1409 :rule scope :premises (@p1408)) % 48.68/48.93 (step-pop @p1410 :rule scope :premises (@p1409)) % 48.68/48.93 (step-pop @p1411 :rule scope :premises (@p1410)) % 48.68/48.93 (step-pop @p1412 :rule scope :premises (@p1411)) % 48.68/48.93 (step-pop @p1413 :rule scope :premises (@p1412)) % 48.68/48.93 (step-pop @p1414 :rule scope :premises (@p1413)) % 48.68/48.93 (step-pop @p1415 :rule scope :premises (@p1414)) % 48.68/48.93 (step-pop @p1416 :rule scope :premises (@p1415)) % 48.68/48.93 (step-pop @p1417 :rule scope :premises (@p1416)) % 48.68/48.93 (step-pop @p1418 :rule scope :premises (@p1417)) % 48.68/48.93 (step @p1137 :rule process_scope :premises (@p1418) :args (@t802)) % 48.68/48.93 (step @p1159 :rule implies_elim :premises (@p1137)) % 48.68/48.93 (step @p1160 :rule cnf_and_neg :args (@t865)) % 48.68/48.93 (step @p1161 :rule resolution :premises (@p1160 @p1159) :args (true @t865)) % 48.68/48.93 (step @p1162 :rule eq_resolve :premises (@p1161 @p992)) % 48.68/48.93 (step @p1163 :rule reordering :premises (@p1162) :args ((or @t852 @t850 @t848 @t846 @t844 @t841 @t840 @t838 @t837 @t836 @t835 @t831 @t826 @t820 @t817 @t802 @t816 @t791 @t803 @t815 @t808 @t804))) % 48.68/48.93 (step @p1164 :rule chain_m_resolution :premises (@p1163 @p591 @p592 @p593 @p594 @p598 @p624 @p628 @p651 @p841 @p672 @p673 @p678 @p679 @p680 @p690 @p969 @p942 @p923 @p842 @p843 @p882) :args (@t802 (@list false false false false false false false false false false false false false false false false true false false false false) (@list @t851 @t849 @t847 @t845 @t843 @t669 @t839 @t677 @t746 @t686 @t834 @t830 @t825 @t819 @t693 @t796 @t791 @t790 @t814 @t807 @t760))) % 48.68/48.93 (step @p1165 :rule cnf_or_pos :args (@t774)) % 48.68/48.93 (step @p1166 :rule reordering :premises (@p1165) :args ((or @t770 @t773 (not @t774)))) % 48.68/48.93 (step @p1167 :rule chain_m_resolution :premises (@p1166 @p1164 @p898) :args (@t770 @t777 (@list @t773 @t774))) % 48.68/48.93 (step @p1168 :rule cnf_or_pos :args (@t772)) % 48.68/48.93 (step @p1169 :rule reordering :premises (@p1168) :args ((or @t771 @t769 (not @t772)))) % 48.68/48.93 (step @p1170 :rule chain_m_resolution :premises (@p1169 @p1167 @p895) :args (@t769 @t744 (@list @t770 @t772))) % 48.68/48.93 (assume-push @p1419 @t866) % 48.68/48.93 (assume-push @p1420 @t851) % 48.68/48.93 (assume-push @p1421 @t847) % 48.68/48.93 (assume-push @p1422 @t845) % 48.68/48.93 (assume-push @p1423 @t839) % 48.68/48.93 (assume-push @p1424 @t860) % 48.68/48.93 (assume-push @p1425 @t867) % 48.68/48.93 (assume-push @p1426 @t834) % 48.68/48.93 (assume-push @p1427 @t686) % 48.68/48.93 (assume-push @p1428 @t859) % 48.68/48.93 (assume-push @p1429 @t814) % 48.68/48.93 (assume-push @p1430 @t693) % 48.68/48.93 (assume-push @p1431 @t868) % 48.68/48.93 (assume-push @p1432 @t807) % 48.68/48.93 (step @p1185 :rule evaluate :args (@t221)) % 48.68/48.93 (step @p1024 :rule refl :args (@t293)) % 48.68/48.93 (step @p1025 :rule cong :premises (@p592) :args (@t345)) % 48.68/48.93 (step @p1026 :rule cong :premises (@p1025 @p1024) :args (@t856)) % 48.68/48.93 (step @p1027 :rule symm :premises (@p672)) % 48.68/48.93 (step @p1028 :rule trans :premises (@p1027 @p87)) % 48.68/48.93 (step @p1029 :rule cong :premises (@p1028) :args (@t853)) % 48.68/48.93 (step @p1030 :rule cong :premises (@p1029 @p1024) :args (@t854)) % 48.68/48.93 (step @p1046 :rule trans :premises (@p1030 @p1026)) % 48.68/48.93 (step @p1186 :rule symm :premises (@p1046)) % 48.68/48.93 (step @p1187 :rule symm :premises (@p882)) % 48.68/48.93 (step @p1188 :rule trans :premises (@p1187 @p1186)) % 48.68/48.93 (step @p1189 :rule symm :premises (@p1188)) % 48.68/48.93 (step @p1190 :rule trans :premises (@p593 @p672)) % 48.68/48.93 (step @p1191 :rule cong :premises (@p1190) :args (@t345)) % 48.68/48.93 (step @p1192 :rule cong :premises (@p1191 @p1024) :args (@t856)) % 48.68/48.93 (step @p1193 :rule symm :premises (@p1424)) % 48.68/48.93 (step @p1194 :rule symm :premises (@p1428)) % 48.68/48.93 (step @p1067 :rule refl :args (1/1)) % 48.68/48.93 (step @p1098 :rule cong :premises (@p188) :args (@t857)) % 48.68/48.93 (step @p1195 :rule cong :premises (@p1098 @p1024) :args (@t858)) % 48.68/48.93 (step @p1196 :rule trans :premises (@p1424 @p1195)) % 48.68/48.93 (step @p1197 :rule cong :premises (@p903 @p1196) :args (@t168)) % 48.68/48.93 (step @p1198 :rule cong :premises (@p1197 @p1067) :args (@t809)) % 48.68/48.93 (step @p1199 :rule trans :premises (@p1198 @p1194 @p1193)) % 48.68/48.93 (step @p1200 :rule cong :premises (@p1199) :args (@t810)) % 48.68/48.93 (step @p1060 :rule refl :args (|tptp.'times$'|)) % 48.68/48.93 (step @p1201 :rule cong :premises (@p1060 @p591) :args (@t159)) % 48.68/48.93 (step @p1202 :rule cong :premises (@p1201 @p763) :args (@t832)) % 48.68/48.93 (step @p1203 :rule trans :premises (@p628 @p673 @p1202)) % 48.68/48.93 (step @p1064 :rule refl :args (@t9)) % 48.68/48.93 (step @p1204 :rule cong :premises (@p1064 @p1203) :args (@t687)) % 48.68/48.93 (step @p1205 :rule trans :premises (@p690 @p1204 @p842 @p1200 @p87)) % 48.68/48.93 (step @p1206 :rule cong :premises (@p1205) :args (@t861)) % 48.68/48.93 (step @p685 :rule instantiate :premises (@p261) :args (@t692)) % 48.68/48.93 (step @p1207 :rule cong :premises (@p685) :args (@t805)) % 48.68/48.93 (step @p1208 :rule trans :premises (@p1207 @p1206)) % 48.68/48.93 (step @p1209 :rule cong :premises (@p1208 @p1024) :args (@t806)) % 48.68/48.93 (step @p1210 :rule arith_poly_norm :args (@t869)) % 48.68/48.93 (step @p1211 :rule arith_poly_norm_rel :premises (@p1210) :args (@t870)) % 48.68/48.93 (step @p1212 :rule symm :premises (@p1211)) % 48.68/48.93 (step @p1213 :rule chain_m_resolution :premises (@p733 @p716) :args (@t706 @t674 @t713)) % 48.68/48.93 (step @p1214 :rule eq_resolve :premises (@p1213 @p1212)) % 48.68/48.93 (step @p1215 :rule symm :premises (@p1214)) % 48.68/48.93 (step @p1216 :rule cong :premises (@p1215) :args (@t767)) % 48.68/48.93 (step @p1217 :rule refl :args (@t688)) % 48.68/48.93 (step @p1218 :rule cong :premises (@p1217 @p1216) :args (@t768)) % 48.68/48.93 (step @p1219 :rule trans :premises (@p1431 @p1218 @p843 @p1209 @p1192 @p1189)) % 48.68/48.93 (step @p1220 false :rule eq_resolve :premises (@p1219 @p1185)) % 48.68/48.93 (step-pop @p1433 :rule scope :premises (@p1220)) % 48.68/48.93 (step-pop @p1434 :rule scope :premises (@p1433)) % 48.68/48.93 (step-pop @p1435 :rule scope :premises (@p1434)) % 48.68/48.93 (step-pop @p1436 :rule scope :premises (@p1435)) % 48.68/48.93 (step-pop @p1437 :rule scope :premises (@p1436)) % 48.68/48.93 (step-pop @p1438 :rule scope :premises (@p1437)) % 48.68/48.93 (step-pop @p1439 :rule scope :premises (@p1438)) % 48.68/48.93 (step-pop @p1440 :rule scope :premises (@p1439)) % 48.68/48.93 (step-pop @p1441 :rule scope :premises (@p1440)) % 48.68/48.93 (step-pop @p1442 :rule scope :premises (@p1441)) % 48.68/48.93 (step-pop @p1443 :rule scope :premises (@p1442)) % 48.68/48.93 (step-pop @p1444 :rule scope :premises (@p1443)) % 48.68/48.93 (step-pop @p1445 :rule scope :premises (@p1444)) % 48.68/48.93 (step-pop @p1446 :rule scope :premises (@p1445)) % 48.68/48.93 (step @p1221 :rule process_scope :premises (@p1446) :args (false)) % 48.68/48.93 (assume-push @p1447 @t851) % 48.68/48.93 (assume-push @p1448 @t849) % 48.68/48.93 (assume-push @p1449 @t847) % 48.68/48.93 (assume-push @p1450 @t845) % 48.68/48.93 (assume-push @p1451 @t843) % 48.68/48.93 (assume-push @p1452 @t669) % 48.68/48.93 (assume-push @p1453 @t839) % 48.68/48.93 (assume-push @p1454 @t677) % 48.68/48.93 (assume-push @p1455 @t746) % 48.68/48.93 (assume-push @p1456 @t686) % 48.68/48.93 (assume-push @p1457 @t834) % 48.68/48.93 (assume-push @p1458 @t830) % 48.68/48.93 (assume-push @p1459 @t825) % 48.68/48.93 (assume-push @p1460 @t819) % 48.68/48.93 (assume-push @p1461 @t693) % 48.68/48.93 (assume-push @p1462 @t769) % 48.68/48.93 (assume-push @p1463 @t706) % 48.68/48.93 (assume-push @p1464 @t814) % 48.68/48.93 (assume-push @p1465 @t807) % 48.68/48.93 (assume-push @p1466 @t760) % 48.68/48.93 (assume-push @p1467 @t769) % 48.68/48.93 (assume-push @p1468 @t746) % 48.68/48.93 (step @p1258 :rule symm :premises (@p841)) % 48.68/48.93 (step @p1259 :rule trans :premises (@p1258 @p1462)) % 48.68/48.93 (step-pop @p1469 :rule scope :premises (@p1259)) % 48.68/48.93 (step-pop @p1470 :rule scope :premises (@p1469)) % 48.68/48.93 (step @p1260 :rule process_scope :premises (@p1470) :args (@t868)) % 48.68/48.93 (step @p1263 :rule and_intro :premises (@p1462 @p841)) % 48.68/48.93 (step @p1264 :rule modus_ponens :premises (@p1263 @p1260)) % 48.68/48.93 (assume-push @p1471 @t825) % 48.68/48.93 (assume-push @p1472 @t864) % 48.68/48.93 (step @p1119 :rule refl :args (@t293)) % 48.68/48.93 (step @p1120 :rule refl :args (@t10)) % 48.68/48.93 (step @p1121 :rule cong :premises (@p1120 @p592) :args (@t842)) % 48.68/48.93 (step @p1122 :rule trans :premises (@p598 @p1121)) % 48.68/48.93 (step @p1123 :rule cong :premises (@p1122) :args (@t348)) % 48.68/48.93 (step @p1098 :rule cong :premises (@p188) :args (@t857)) % 48.68/48.93 (step @p1124 :rule trans :premises (@p1098 @p1123)) % 48.68/48.93 (step @p1125 :rule cong :premises (@p1124 @p1119) :args (@t858)) % 48.68/48.93 (step @p1126 :rule trans :premises (@p1125 @p679)) % 48.68/48.93 (step-pop @p1473 :rule scope :premises (@p1126)) % 48.68/48.93 (step-pop @p1474 :rule scope :premises (@p1473)) % 48.68/48.93 (step @p1267 :rule process_scope :premises (@p1474) :args (@t859)) % 48.68/48.93 (step @p1024 :rule refl :args (@t293)) % 48.68/48.93 (step @p1120 :rule refl :args (@t10)) % 48.68/48.93 (step @p1121 :rule cong :premises (@p1120 @p592) :args (@t842)) % 48.68/48.93 (step @p1122 :rule trans :premises (@p598 @p1121)) % 48.68/48.93 (step @p1123 :rule cong :premises (@p1122) :args (@t348)) % 48.68/48.93 (step @p1098 :rule cong :premises (@p188) :args (@t857)) % 48.68/48.93 (step @p1124 :rule trans :premises (@p1098 @p1123)) % 48.68/48.93 (step @p1130 :rule cong :premises (@p1124 @p1024) :args (@t858)) % 48.68/48.93 (step @p1131 :rule and_intro :premises (@p679 @p1130)) % 48.68/48.93 (step @p1270 :rule modus_ponens :premises (@p1131 @p1267)) % 48.68/48.93 (step @p1025 :rule cong :premises (@p592) :args (@t345)) % 48.68/48.93 (step @p1026 :rule cong :premises (@p1025 @p1024) :args (@t856)) % 48.68/48.93 (step @p1027 :rule symm :premises (@p672)) % 48.68/48.93 (step @p1028 :rule trans :premises (@p1027 @p87)) % 48.68/48.93 (step @p1029 :rule cong :premises (@p1028) :args (@t853)) % 48.68/48.93 (step @p1030 :rule cong :premises (@p1029 @p1024) :args (@t854)) % 48.68/48.93 (step @p1046 :rule trans :premises (@p1030 @p1026)) % 48.68/48.93 (step @p1186 :rule symm :premises (@p1046)) % 48.68/48.93 (step @p1187 :rule symm :premises (@p882)) % 48.68/48.93 (step @p1271 :rule trans :premises (@p1187 @p1186)) % 48.68/48.93 (assume-push @p1475 @t862) % 48.68/48.93 (assume-push @p1476 @t830) % 48.68/48.93 (assume-push @p1477 @t863) % 48.68/48.93 (assume-push @p1478 @t819) % 48.68/48.93 (step @p1096 :rule refl :args (@t293)) % 48.68/48.93 (step @p1097 :rule cong :premises (@p624) :args (@t348)) % 48.68/48.93 (step @p1099 :rule trans :premises (@p1098 @p1097)) % 48.68/48.93 (step @p1100 :rule cong :premises (@p1099 @p1096) :args (@t858)) % 48.68/48.93 (step @p1101 :rule symm :premises (@p1100)) % 48.68/48.93 (step @p1102 :rule refl :args (@t293)) % 48.68/48.93 (step @p1103 :rule cong :premises (@p651) :args (@t828)) % 48.68/48.93 (step @p1104 :rule cong :premises (@p1103 @p1102) :args (@t829)) % 48.68/48.93 (step @p1105 :rule symm :premises (@p1104)) % 48.68/48.93 (step @p1106 :rule symm :premises (@p680)) % 48.68/48.93 (step @p1107 :rule trans :premises (@p1106 @p1105 @p678 @p1101)) % 48.68/48.93 (step-pop @p1479 :rule scope :premises (@p1107)) % 48.68/48.93 (step-pop @p1480 :rule scope :premises (@p1479)) % 48.68/48.93 (step-pop @p1481 :rule scope :premises (@p1480)) % 48.68/48.93 (step-pop @p1482 :rule scope :premises (@p1481)) % 48.68/48.93 (step @p1276 :rule process_scope :premises (@p1482) :args (@t860)) % 48.68/48.93 (step @p1103 :rule cong :premises (@p651) :args (@t828)) % 48.68/48.93 (step @p1113 :rule cong :premises (@p1103 @p1024) :args (@t829)) % 48.68/48.93 (step @p1097 :rule cong :premises (@p624) :args (@t348)) % 48.68/48.93 (step @p1099 :rule trans :premises (@p1098 @p1097)) % 48.68/48.93 (step @p1114 :rule cong :premises (@p1099 @p1024) :args (@t858)) % 48.68/48.93 (step @p1115 :rule and_intro :premises (@p1114 @p678 @p1113 @p680)) % 48.68/48.93 (step @p1281 :rule modus_ponens :premises (@p1115 @p1276)) % 48.68/48.93 (step @p1210 :rule arith_poly_norm :args (@t869)) % 48.68/48.93 (step @p1211 :rule arith_poly_norm_rel :premises (@p1210) :args (@t870)) % 48.68/48.93 (step @p1212 :rule symm :premises (@p1211)) % 48.68/48.93 (step @p1282 :rule eq_resolve :premises (@p734 @p1212)) % 48.68/48.93 (step @p1283 :rule and_intro :premises (@p1282 @p591 @p593 @p594 @p628 @p1281 @p1271 @p673 @p672 @p1270 @p842 @p690 @p1264 @p843)) % 48.68/48.93 (step-pop @p1483 :rule scope :premises (@p1283)) % 48.68/48.93 (step-pop @p1484 :rule scope :premises (@p1483)) % 48.68/48.93 (step-pop @p1485 :rule scope :premises (@p1484)) % 48.68/48.93 (step-pop @p1486 :rule scope :premises (@p1485)) % 48.68/48.93 (step-pop @p1487 :rule scope :premises (@p1486)) % 48.68/48.93 (step-pop @p1488 :rule scope :premises (@p1487)) % 48.68/48.93 (step-pop @p1489 :rule scope :premises (@p1488)) % 48.68/48.93 (step-pop @p1490 :rule scope :premises (@p1489)) % 48.68/48.93 (step-pop @p1491 :rule scope :premises (@p1490)) % 48.68/48.93 (step-pop @p1492 :rule scope :premises (@p1491)) % 48.68/48.93 (step-pop @p1493 :rule scope :premises (@p1492)) % 48.68/48.93 (step-pop @p1494 :rule scope :premises (@p1493)) % 48.68/48.93 (step-pop @p1495 :rule scope :premises (@p1494)) % 48.68/48.93 (step-pop @p1496 :rule scope :premises (@p1495)) % 48.68/48.93 (step-pop @p1497 :rule scope :premises (@p1496)) % 48.68/48.93 (step-pop @p1498 :rule scope :premises (@p1497)) % 48.68/48.93 (step-pop @p1499 :rule scope :premises (@p1498)) % 48.68/48.93 (step-pop @p1500 :rule scope :premises (@p1499)) % 48.68/48.93 (step-pop @p1501 :rule scope :premises (@p1500)) % 48.68/48.93 (step-pop @p1502 :rule scope :premises (@p1501)) % 48.68/48.93 (step @p1284 :rule process_scope :premises (@p1502) :args (@t871)) % 48.68/48.93 (step @p1305 :rule implies_elim :premises (@p1284)) % 48.68/48.93 (step @p1306 :rule resolution :premises (@p1305 @p1221) :args (true @t871)) % 48.68/48.93 (step @p1307 :rule not_and :premises (@p1306)) % 48.68/48.93 (step @p1308 false :rule chain_m_resolution :premises (@p1307 @p1170 @p882 @p843 @p842 @p841 @p734 @p690 @p680 @p679 @p678 @p673 @p672 @p651 @p628 @p624 @p598 @p594 @p593 @p592 @p591) :args (false (@list false false false false false false false false false false false false false false false false false false false false) (@list @t769 @t760 @t807 @t814 @t746 @t706 @t693 @t819 @t825 @t830 @t834 @t686 @t677 @t839 @t669 @t843 @t845 @t847 @t849 @t851))) % 48.68/48.93 ) % 48.68/48.93 % SZS output end Proof % 48.68/48.93 % cvc5 exiting %------------------------------------------------------------------------------