%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP267^1 : TPTP v9.3.1. Bugfixed v9.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:04:59 AM UTC 2026
% Result : Theorem 107.21s 39.60s
% Output : CNFRefutation 141.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP267^1 : TPTP v9.3.1. Bugfixed v9.2.1.
% 0.00/0.06 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 % Computer : n020.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Tue Sep 29 20:46:49 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.21/0.28 Running higher-order theorem proving
% 3.84/4.02 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.t8uTkq6Zqu/E---3.1_1561182.p
% 107.21/39.60 % Version: 3.5.1-ho
% 107.21/39.60 % partial match(1): HMLMSMSMSSLCHFA
% 107.21/39.60 % Preprocessing class: HMLMSMLMSSLCHFA.
% 107.21/39.60 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 107.21/39.60 % Starting new_ho_10 with 1495s (5) cores
% 107.21/39.60 % Starting sh5l with 299s (1) cores
% 107.21/39.60 % Starting new_bool_1 with 299s (1) cores
% 107.21/39.60 % Starting new_bool_2 with 299s (1) cores
% 107.21/39.60 % new_bool_1 with pid 1561306 completed with status 0
% 107.21/39.60 % Result found by new_bool_1
% 107.21/39.60 % partial match(1): HMLMSMSMSSLCHFA
% 107.21/39.60 % Preprocessing class: HMLMSMLMSSLCHFA.
% 107.21/39.60 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 107.21/39.60 % Starting new_ho_10 with 1495s (5) cores
% 107.21/39.60 % Starting sh5l with 299s (1) cores
% 107.21/39.60 % Starting new_bool_1 with 299s (1) cores
% 107.21/39.60 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 107.21/39.60 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 107.21/39.60 % Search class: HGHSM-SMLM32-DHFFFSBN
% 107.21/39.60 % Scheduled 5 strats onto 1 cores with 297 seconds (297 total)
% 107.21/39.60 % Starting SubtermCWHack with 30s (1) cores
% 107.21/39.60 % SubtermCWHack with pid 1561310 completed with status 8
% 107.21/39.60 % Starting new_ho_10 with 179s (1) cores
% 107.21/39.60 % new_ho_10 with pid 1561324 completed with status 0
% 107.21/39.60 % Result found by new_ho_10
% 107.21/39.60 % partial match(1): HMLMSMSMSSLCHFA
% 107.21/39.60 % Preprocessing class: HMLMSMLMSSLCHFA.
% 107.21/39.60 % Scheduled 4 strats onto 8 cores with 299 seconds (2392 total)
% 107.21/39.60 % Starting new_ho_10 with 1495s (5) cores
% 107.21/39.60 % Starting sh5l with 299s (1) cores
% 107.21/39.60 % Starting new_bool_1 with 299s (1) cores
% 107.21/39.60 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 107.21/39.60 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 107.21/39.60 % Search class: HGHSM-SMLM32-DHFFFSBN
% 107.21/39.60 % Scheduled 5 strats onto 1 cores with 297 seconds (297 total)
% 107.21/39.60 % Starting SubtermCWHack with 30s (1) cores
% 107.21/39.60 % SubtermCWHack with pid 1561310 completed with status 8
% 107.21/39.60 % Starting new_ho_10 with 179s (1) cores
% 107.21/39.60 % Preprocessing time : 0.293 s
% 107.21/39.60 % Presaturation interreduction done
% 107.21/39.60
% 107.21/39.60 % Proof found!
% 107.21/39.60 % SZS status Theorem
% 107.21/39.60 % SZS output start CNFRefutation
% 107.21/39.60 thf(decl_sort1, type, nat: $tType).
% 107.21/39.60 thf(decl_sort2, type, num: $tType).
% 107.21/39.60 thf(decl_sort3, type, vEBT_VEBT: $tType).
% 107.21/39.60 thf(decl_sort4, type, list_VEBT_VEBT: $tType).
% 107.21/39.60 thf(decl_sort5, type, option_nat: $tType).
% 107.21/39.60 thf(decl_210, type, one_one_nat: nat).
% 107.21/39.60 thf(decl_217, type, plus_plus_nat: nat > nat > nat).
% 107.21/39.60 thf(decl_230, type, times_times_nat: nat > nat > nat).
% 107.21/39.60 thf(decl_318, type, if_nat: $o > nat > nat > nat).
% 107.21/39.60 thf(decl_363, type, list_u1324408373059187874T_VEBT: list_VEBT_VEBT > nat > vEBT_VEBT > list_VEBT_VEBT).
% 107.21/39.60 thf(decl_382, type, nth_VEBT_VEBT: list_VEBT_VEBT > nat > vEBT_VEBT).
% 107.21/39.60 thf(decl_410, type, suc: nat > nat).
% 107.21/39.60 thf(decl_477, type, bit0: num > num).
% 107.21/39.60 thf(decl_479, type, one: num).
% 107.21/39.60 thf(decl_487, type, numeral_numeral_nat: num > nat).
% 107.21/39.60 thf(decl_493, type, none_nat: option_nat).
% 107.21/39.60 thf(decl_507, type, the_nat: option_nat > nat).
% 107.21/39.60 thf(decl_528, type, ord_less_nat: nat > nat > $o).
% 107.21/39.60 thf(decl_549, type, ord_less_eq_nat: nat > nat > $o).
% 107.21/39.60 thf(decl_589, type, power_power_nat: nat > nat > nat).
% 107.21/39.60 thf(decl_673, type, divide_divide_nat: nat > nat > nat).
% 107.21/39.60 thf(decl_820, type, vEBT_VEBT_high: nat > nat > nat).
% 141.39/39.60 thf(decl_822, type, vEBT_VEBT_low: nat > nat > nat).
% 141.39/39.60 thf(decl_833, type, vEBT_vebt_delete: vEBT_VEBT > nat > vEBT_VEBT).
% 141.39/39.60 thf(decl_854, type, vEBT_vebt_maxt: vEBT_VEBT > option_nat).
% 141.39/39.60 thf(decl_883, type, deg: nat).
% 141.39/39.60 thf(decl_884, type, lx: nat).
% 141.39/39.60 thf(decl_886, type, ma: nat).
% 141.39/39.60 thf(decl_888, type, na: nat).
% 141.39/39.60 thf(decl_889, type, summary: vEBT_VEBT).
% 141.39/39.60 thf(decl_890, type, summin: nat).
% 141.39/39.60 thf(decl_891, type, treeList: list_VEBT_VEBT).
% 141.39/39.60 thf(decl_893, type, epred1_0: $o).
% 141.39/39.60 thf(decl_894, type, epred2_0: $o).
% 141.39/39.60 thf(conj_0, conjecture, ((ord_less_nat @ (if_nat @ (((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))) @ (if_nat @ (((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))) @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))&(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ (((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))) @ (if_nat @ (((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))) @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))), file('/export/starexec/sandbox/tmp/tmp.t8uTkq6Zqu/E---3.1_1561182.p', conj_0)).
% 141.39/39.60 thf(fact_4__092_060open_062summin_A_K_A2_A_094_An_A_L_Alx_A_061_Ama_092_060close_062, axiom, ((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma)), file('/export/starexec/sandbox/tmp/tmp.t8uTkq6Zqu/E---3.1_1561182.p', fact_4__092_060open_062summin_A_K_A2_A_094_An_A_L_Alx_A_061_Ama_092_060close_062)).
% 141.39/39.60 thf(fact_758_Suc__1, axiom, ((suc @ one_one_nat)=(numeral_numeral_nat @ (bit0 @ one))), file('/export/starexec/sandbox/tmp/tmp.t8uTkq6Zqu/E---3.1_1561182.p', fact_758_Suc__1)).
% 141.39/39.60 thf(fact_8_True, axiom, ((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)), file('/export/starexec/sandbox/tmp/tmp.t8uTkq6Zqu/E---3.1_1561182.p', fact_8_True)).
% 141.39/39.60 thf(fact_10__C9_C, axiom, ((divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))=(na)), file('/export/starexec/sandbox/tmp/tmp.t8uTkq6Zqu/E---3.1_1561182.p', fact_10__C9_C)).
% 141.39/39.60 thf(help_If_1_1_If_001t__Nat__Onat_T, axiom, ![X4:nat, X12:nat]:(((if_nat @ (($true)) @ X4 @ X12)=(X4))), file('/export/starexec/sandbox/tmp/tmp.t8uTkq6Zqu/E---3.1_1561182.p', help_If_1_1_If_001t__Nat__Onat_T)).
% 141.39/39.60 thf(fact_0__C5_Ohyps_C_I8_J, axiom, (ord_less_nat @ ma @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)), file('/export/starexec/sandbox/tmp/tmp.t8uTkq6Zqu/E---3.1_1561182.p', fact_0__C5_Ohyps_C_I8_J)).
% 141.39/39.60 thf(fact_602_le__refl, axiom, ![X10:nat]:((ord_less_eq_nat @ X10 @ X10)), file('/export/starexec/sandbox/tmp/tmp.t8uTkq6Zqu/E---3.1_1561182.p', fact_602_le__refl)).
% 141.39/39.60 thf(c_0_8, plain, ((epred1_0)<=>((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))&(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))))&(((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))&(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))))))), introduced(definition)).
% 141.39/39.60 thf(c_0_9, negated_conjecture, ~(((ord_less_nat @ (if_nat @ (((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))) @ (if_nat @ (((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))) @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))&(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ (((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))) @ (if_nat @ (((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))) @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))), inference(assume_negation,[status(cth)],[conj_0])).
% 141.39/39.60 thf(c_0_10, plain, ((epred2_0)<=>((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))&(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))))&(((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))&(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))))))), introduced(definition)).
% 141.39/39.60 thf(c_0_11, plain, (((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))&(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))))&(((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))&(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))))))=>(epred1_0)), inference(split_equiv,[status(thm)],[c_0_8])).
% 141.39/39.60 thf(c_0_12, plain, ((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma)), inference(split_conjunct,[status(thm)],[fact_4__092_060open_062summin_A_K_A2_A_094_An_A_L_Alx_A_061_Ama_092_060close_062])).
% 141.39/39.60 thf(c_0_13, plain, ((suc @ one_one_nat)=(numeral_numeral_nat @ (bit0 @ one))), inference(split_conjunct,[status(thm)],[fact_758_Suc__1])).
% 141.39/39.60 thf(c_0_14, negated_conjecture, ~(((epred1_0)&(epred2_0))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fool_unroll,[status(thm)],[c_0_9]), c_0_8]), c_0_10])).
% 141.39/39.60 thf(c_0_15, plain, (((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|(epred1_0))&(((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|(epred1_0))&(~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|(epred1_0)))&((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|(epred1_0))&(~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|(epred1_0)))))&((((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred1_0))&(((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred1_0))&(~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred1_0)))&((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred1_0))&(~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred1_0)))))&((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|(~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred1_0))&(((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred1_0))&(~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred1_0)))&((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|(~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred1_0))&(~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|(~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred1_0))))))&(((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))|(epred1_0))&(((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))|(epred1_0))&(~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))|(epred1_0)))&((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))|(epred1_0))&(~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))|(epred1_0)))))&((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|(~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))|(epred1_0))&(((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))|(epred1_0))&(~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))|(epred1_0)))&((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|(~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))|(epred1_0))&(~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|~(ord_less_nat @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|(~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg))|~(ord_less_nat @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))|(epred1_0)))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_11])])])).
% 141.39/39.60 thf(c_0_16, plain, ((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)), inference(split_conjunct,[status(thm)],[fact_8_True])).
% 141.39/39.60 thf(c_0_17, plain, ((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (suc @ one_one_nat) @ na)) @ lx)=(ma)), inference(rw,[status(thm)],[c_0_12, c_0_13])).
% 141.39/39.60 thf(c_0_18, plain, ((divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))=(na)), inference(split_conjunct,[status(thm)],[fact_10__C9_C])).
% 141.39/39.60 thf(c_0_19, plain, ![X28243:nat, X28244:nat]:(((if_nat @ $true @ X28243 @ X28244)=(X28243))), inference(variable_rename,[status(thm)],[help_If_1_1_If_001t__Nat__Onat_T])).
% 141.39/39.60 thf(c_0_20, plain, (ord_less_nat @ ma @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)), inference(split_conjunct,[status(thm)],[fact_0__C5_Ohyps_C_I8_J])).
% 141.39/39.60 thf(c_0_21, plain, (((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))&(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))))&(((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))&(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))))))=>(epred2_0)), inference(split_equiv,[status(thm)],[c_0_10])).
% 141.39/39.60 thf(c_0_22, negated_conjecture, (~(epred1_0)|~(epred2_0)), inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_14])])).
% 141.39/39.60 thf(c_0_23, plain, ((epred1_0)|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~((ord_less_nat @ (if_nat @ (($true)) @ (if_nat @ (($true)) @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma) @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ deg)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 141.39/39.60 thf(c_0_24, plain, ((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ ma @ na)))=(none_nat)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_16, c_0_13]), c_0_17])).
% 141.39/39.60 thf(c_0_25, plain, ((divide_divide_nat @ deg @ (suc @ one_one_nat))=(na)), inference(rw,[status(thm)],[c_0_18, c_0_13])).
% 141.39/39.60 thf(c_0_26, plain, ![X3:nat, X2:nat]:(((if_nat @ (($true)) @ X2 @ X3)=(X2))), inference(split_conjunct,[status(thm)],[c_0_19])).
% 141.39/39.60 thf(c_0_27, plain, (ord_less_nat @ ma @ (power_power_nat @ (suc @ one_one_nat) @ deg)), inference(rw,[status(thm)],[c_0_20, c_0_13])).
% 141.39/39.60 thf(c_0_28, plain, (((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|(epred2_0))&(((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|(epred2_0))&(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|(epred2_0)))&((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|(epred2_0))&(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)=(ma))|(epred2_0)))))&((((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred2_0))&(((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred2_0))&(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred2_0)))&((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred2_0))&(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred2_0)))))&((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred2_0))&(((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred2_0))&(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred2_0)))&((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred2_0))&(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat)))|(epred2_0))))))&(((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))|(epred2_0))&(((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))|(epred2_0))&(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))|(epred2_0)))&((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))|(epred2_0))&(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|(((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))|(epred2_0)))))&((((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))|(epred2_0))&(((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))|(epred2_0))&(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))=(none_nat))|(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))|(epred2_0)))&((((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))|(epred2_0))&(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $false @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|(~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $false @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma))|~(ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ $true @ (if_nat @ $true @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))|(epred2_0)))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_21])])])).
% 141.39/39.60 thf(c_0_29, plain, ![X27809:nat]:((ord_less_eq_nat @ X27809 @ X27809)), inference(variable_rename,[status(thm)],[fact_602_le__refl])).
% 141.39/39.60 thf(c_0_30, negated_conjecture, (~((epred1_0))|~((epred2_0))), inference(split_conjunct,[status(thm)],[c_0_22])).
% 141.39/39.60 thf(c_0_31, plain, (epred1_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_13]), c_0_17]), c_0_13]), c_0_17]), c_0_24]), c_0_13]), c_0_17]), c_0_13]), c_0_13]), c_0_25]), c_0_13]), c_0_17]), c_0_24]), c_0_13]), c_0_17]), c_0_13]), c_0_17]), c_0_13]), c_0_17]), c_0_13]), c_0_17]), c_0_24]), c_0_26]), c_0_26]), c_0_13]), c_0_27])])).
% 141.39/39.60 thf(c_0_32, plain, ((epred2_0)|((plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx)!=(ma))|((vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)))!=(none_nat))|~((ord_less_eq_nat @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (if_nat @ (($true)) @ (if_nat @ (($true)) @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ (plus_plus_nat @ (times_times_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ (divide_divide_nat @ deg @ (numeral_numeral_nat @ (bit0 @ one)))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))) @ (the_nat @ (vEBT_vebt_maxt @ (nth_VEBT_VEBT @ (list_u1324408373059187874T_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na) @ (vEBT_vebt_delete @ (nth_VEBT_VEBT @ treeList @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na)) @ (vEBT_VEBT_low @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))) @ (the_nat @ (vEBT_vebt_maxt @ (vEBT_vebt_delete @ summary @ (vEBT_VEBT_high @ (plus_plus_nat @ (times_times_nat @ summin @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ na)) @ lx) @ na))))))))) @ ma)))), inference(split_conjunct,[status(thm)],[c_0_28])).
% 141.39/39.60 thf(c_0_33, plain, ![X2:nat]:((ord_less_eq_nat @ X2 @ X2)), inference(split_conjunct,[status(thm)],[c_0_29])).
% 141.39/39.60 thf(c_0_34, negated_conjecture, ~((epred2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])])).
% 141.39/39.60 thf(c_0_35, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_32, c_0_13]), c_0_17]), c_0_13]), c_0_17]), c_0_24]), c_0_13]), c_0_17]), c_0_13]), c_0_17]), c_0_13]), c_0_13]), c_0_25]), c_0_13]), c_0_17]), c_0_24]), c_0_13]), c_0_17]), c_0_13]), c_0_17]), c_0_13]), c_0_17]), c_0_13]), c_0_17]), c_0_24]), c_0_26]), c_0_26]), c_0_33])]), c_0_34]), ['proof']).
% 141.39/39.60 % SZS output end CNFRefutation
% 141.39/39.60 % Parsed axioms : 11209
% 141.39/39.60 % Removed by relevancy pruning/SinE : 7268
% 141.39/39.60 % Initial clauses : 10823
% 141.39/39.60 % Removed in clause preprocessing : 2671
% 141.39/39.60 % Initial clauses in saturation : 8152
% 141.39/39.60 % Processed clauses : 1742
% 141.39/39.60 % ...of these trivial : 180
% 141.39/39.60 % ...subsumed : 383
% 141.39/39.60 % ...remaining for further processing : 1178
% 141.39/39.60 % Other redundant clauses eliminated : 281
% 141.39/39.60 % Clauses deleted for lack of memory : 0
% 141.39/39.60 % Backward-subsumed : 3
% 141.39/39.60 % Backward-rewritten : 27
% 141.39/39.60 % Generated clauses : 260
% 141.39/39.60 % ...of the previous two non-redundant : 118
% 141.39/39.60 % ...aggressively subsumed : 0
% 141.39/39.60 % Contextual simplify-reflections : 0
% 141.39/39.60 % Paramodulations : 0
% 141.39/39.60 % Factorizations : 0
% 141.39/39.60 % NegExts : 0
% 141.39/39.60 % Equation resolutions : 281
% 141.39/39.60 % Disequality decompositions : 0
% 141.39/39.60 % Total rewrite steps : 923
% 141.39/39.60 % ...of those cached : 706
% 141.39/39.60 % Propositional unsat checks : 0
% 141.39/39.60 % Propositional check models : 0
% 141.39/39.60 % Propositional check unsatisfiable : 0
% 141.39/39.60 % Propositional clauses : 0
% 141.39/39.60 % Propositional clauses after purity: 0
% 141.39/39.60 % Propositional unsat core size : 0
% 141.39/39.60 % Propositional preprocessing time : 0.000
% 141.39/39.60 % Propositional encoding time : 0.000
% 141.39/39.60 % Propositional solver time : 0.000
% 141.39/39.60 % Success case prop preproc time : 0.000
% 141.39/39.60 % Success case prop encoding time : 0.000
% 141.39/39.60 % Success case prop solver time : 0.000
% 141.39/39.60 % Current number of processed clauses : 888
% 141.39/39.60 % Positive orientable unit clauses : 417
% 141.39/39.60 % Positive unorientable unit clauses: 0
% 141.39/39.60 % Negative unit clauses : 138
% 141.39/39.60 % Non-unit-clauses : 333
% 141.39/39.60 % Current number of unprocessed clauses: 6528
% 141.39/39.60 % ...number of literals in the above : 28095
% 141.39/39.60 % Current number of archived formulas : 0
% 141.39/39.60 % Current number of archived clauses : 30
% 141.39/39.60 % Clause-clause subsumption calls (NU) : 42659
% 141.39/39.60 % Rec. Clause-clause subsumption calls : 21850
% 141.39/39.60 % Non-unit clause-clause subsumptions : 243
% 141.39/39.60 % Unit Clause-clause subsumption calls : 2713
% 141.39/39.60 % Rewrite failures with RHS unbound : 0
% 141.39/39.60 % BW rewrite match attempts : 149
% 141.39/39.60 % BW rewrite match successes : 32
% 141.39/39.60 % Condensation attempts : 1742
% 141.39/39.60 % Condensation successes : 0
% 141.39/39.60 % Termbank termtop insertions : 932622
% 141.39/39.60 % Search garbage collected termcells : 219714
% 141.39/39.60
% 141.39/39.60 % -------------------------------------------------
% 141.39/39.60 % User time : 24.246 s
% 141.39/39.60 % System time : 9.593 s
% 141.39/39.60 % Total time : 33.839 s
% 141.39/39.60 % Maximum resident set size: 50748 pages
% 141.39/39.60
% 141.39/39.60 % -------------------------------------------------
% 141.39/39.60 % User time : 25.702 s
% 141.39/39.60 % System time : 9.639 s
% 141.39/39.60 % Total time : 35.341 s
% 141.39/39.60 % Maximum resident set size: 30208 pages
% 141.39/39.60 % E exiting
%------------------------------------------------------------------------------