LEO-II---2.3.1.THM-CRf.s

%------------------------------------------------------------------------------
% File     : LEO-II---2.3.1
% Problem  : ITP234^3 : TPTP v9.3.1. Bugfixed v9.2.1.
% Transfm  : none
% Format   : tptp:raw
% Command  : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p

% Computer : n018.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 Oct  7 10:25:05 AM UTC 2026

% Result   : Theorem 32.15s 6.60s
% Output   : CNFRefutation 32.15s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   20
%            Number of leaves      :   13
% Syntax   : Number of formulae    :  376 (  76 unt;   0 typ;   0 def)
%            Number of atoms       : 3576 (1316 equ;   0 cnn)
%            Maximal formula atoms :    4 (   9 avg)
%            Number of connectives : 2172 ( 506   ~; 956   |;   0   &; 704   @)
%                                         (   0 <=>;   6  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    8 (   4 avg)
%            Number of types       :   81 (  80 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :  805 ( 802 usr;  66 con; 0-5 aty)
%            Number of variables   :  285 (   0   ^; 279   !;   6   ?; 285   :)

% Comments : 
%------------------------------------------------------------------------------
thf(tp_char,type,
    char: $tType ).

thf(tp_complex,type,
    complex: $tType ).

thf(tp_extended_enat,type,
    extended_enat: $tType ).

thf(tp_filter1242075044329608583at_nat,type,
    filter1242075044329608583at_nat: $tType ).

thf(tp_filter_nat,type,
    filter_nat: $tType ).

thf(tp_filter_real,type,
    filter_real: $tType ).

thf(tp_int,type,
    int: $tType ).

thf(tp_list_Extended_enat,type,
    list_Extended_enat: $tType ).

thf(tp_list_P3521021558325789923at_int,type,
    list_P3521021558325789923at_int: $tType ).

thf(tp_list_P4547456442757143711BT_int,type,
    list_P4547456442757143711BT_int: $tType ).

thf(tp_list_P5647936690300460905T_VEBT,type,
    list_P5647936690300460905T_VEBT: $tType ).

thf(tp_list_P5707943133018811711nt_int,type,
    list_P5707943133018811711nt_int: $tType ).

thf(tp_list_P6011104703257516679at_nat,type,
    list_P6011104703257516679at_nat: $tType ).

thf(tp_list_P7037539587688870467BT_nat,type,
    list_P7037539587688870467BT_nat: $tType ).

thf(tp_list_P7413028617227757229T_VEBT,type,
    list_P7413028617227757229T_VEBT: $tType ).

thf(tp_list_P7524865323317820941T_VEBT,type,
    list_P7524865323317820941T_VEBT: $tType ).

thf(tp_list_P8198026277950538467nt_nat,type,
    list_P8198026277950538467nt_nat: $tType ).

thf(tp_list_P8469869581646625389at_nat,type,
    list_P8469869581646625389at_nat: $tType ).

thf(tp_list_VEBT_VEBT,type,
    list_VEBT_VEBT: $tType ).

thf(tp_list_complex,type,
    list_complex: $tType ).

thf(tp_list_int,type,
    list_int: $tType ).

thf(tp_list_nat,type,
    list_nat: $tType ).

thf(tp_list_num,type,
    list_num: $tType ).

thf(tp_list_real,type,
    list_real: $tType ).

thf(tp_list_set_nat,type,
    list_set_nat: $tType ).

thf(tp_nat,type,
    nat: $tType ).

thf(tp_num,type,
    num: $tType ).

thf(tp_option4927543243414619207at_nat,type,
    option4927543243414619207at_nat: $tType ).

thf(tp_option_Extended_enat,type,
    option_Extended_enat: $tType ).

thf(tp_option_VEBT_VEBT,type,
    option_VEBT_VEBT: $tType ).

thf(tp_option_int,type,
    option_int: $tType ).

thf(tp_option_nat,type,
    option_nat: $tType ).

thf(tp_option_num,type,
    option_num: $tType ).

thf(tp_option_real,type,
    option_real: $tType ).

thf(tp_option_set_nat,type,
    option_set_nat: $tType ).

thf(tp_produc1186641810826059865st_int,type,
    produc1186641810826059865st_int: $tType ).

thf(tp_produc1531783533982839933T_VEBT,type,
    produc1531783533982839933T_VEBT: $tType ).

thf(tp_produc1828647624359046049st_nat,type,
    produc1828647624359046049st_nat: $tType ).

thf(tp_produc4471711990508489141at_nat,type,
    produc4471711990508489141at_nat: $tType ).

thf(tp_produc4894624898956917775BT_int,type,
    produc4894624898956917775BT_int: $tType ).

thf(tp_produc6392793444374437607at_nat,type,
    produc6392793444374437607at_nat: $tType ).

thf(tp_produc7248412053542808358at_nat,type,
    produc7248412053542808358at_nat: $tType ).

thf(tp_produc8025551001238799321T_VEBT,type,
    produc8025551001238799321T_VEBT: $tType ).

thf(tp_produc8243902056947475879T_VEBT,type,
    produc8243902056947475879T_VEBT: $tType ).

thf(tp_produc859450856879609959at_nat,type,
    produc859450856879609959at_nat: $tType ).

thf(tp_produc9072475918466114483BT_nat,type,
    produc9072475918466114483BT_nat: $tType ).

thf(tp_produc9211091688327510695T_VEBT,type,
    produc9211091688327510695T_VEBT: $tType ).

thf(tp_product_prod_int_int,type,
    product_prod_int_int: $tType ).

thf(tp_product_prod_int_nat,type,
    product_prod_int_nat: $tType ).

thf(tp_product_prod_nat_int,type,
    product_prod_nat_int: $tType ).

thf(tp_product_prod_nat_nat,type,
    product_prod_nat_nat: $tType ).

thf(tp_real,type,
    real: $tType ).

thf(tp_set_Extended_enat,type,
    set_Extended_enat: $tType ).

thf(tp_set_Pr1261947904930325089at_nat,type,
    set_Pr1261947904930325089at_nat: $tType ).

thf(tp_set_Pr1542805901266377927at_nat,type,
    set_Pr1542805901266377927at_nat: $tType ).

thf(tp_set_Pr1916528119006554503T_VEBT,type,
    set_Pr1916528119006554503T_VEBT: $tType ).

thf(tp_set_Pr3451248702717554689st_nat,type,
    set_Pr3451248702717554689st_nat: $tType ).

thf(tp_set_Pr6192946355708809607T_VEBT,type,
    set_Pr6192946355708809607T_VEBT: $tType ).

thf(tp_set_Pr7556676689462069481BT_nat,type,
    set_Pr7556676689462069481BT_nat: $tType ).

thf(tp_set_Pr765067013931698361st_int,type,
    set_Pr765067013931698361st_int: $tType ).

thf(tp_set_Pr8693737435421807431at_nat,type,
    set_Pr8693737435421807431at_nat: $tType ).

thf(tp_set_Pr958786334691620121nt_int,type,
    set_Pr958786334691620121nt_int: $tType ).

thf(tp_set_Product_unit,type,
    set_Product_unit: $tType ).

thf(tp_set_VEBT_VEBT,type,
    set_VEBT_VEBT: $tType ).

thf(tp_set_char,type,
    set_char: $tType ).

thf(tp_set_complex,type,
    set_complex: $tType ).

thf(tp_set_int,type,
    set_int: $tType ).

thf(tp_set_li5464603477888414924d_enat,type,
    set_li5464603477888414924d_enat: $tType ).

thf(tp_set_list_VEBT_VEBT,type,
    set_list_VEBT_VEBT: $tType ).

thf(tp_set_list_complex,type,
    set_list_complex: $tType ).

thf(tp_set_list_int,type,
    set_list_int: $tType ).

thf(tp_set_list_nat,type,
    set_list_nat: $tType ).

thf(tp_set_nat,type,
    set_nat: $tType ).

thf(tp_set_num,type,
    set_num: $tType ).

thf(tp_set_real,type,
    set_real: $tType ).

thf(tp_set_se7270636423289371942d_enat,type,
    set_se7270636423289371942d_enat: $tType ).

thf(tp_set_set_complex,type,
    set_set_complex: $tType ).

thf(tp_set_set_int,type,
    set_set_int: $tType ).

thf(tp_set_set_nat,type,
    set_set_nat: $tType ).

thf(tp_vEBT_VEBT,type,
    vEBT_VEBT: $tType ).

thf(tp_abs_Integ,type,
    abs_Integ: product_prod_nat_nat > int ).

thf(tp_abs_abs_complex,type,
    abs_abs_complex: complex > complex ).

thf(tp_abs_abs_int,type,
    abs_abs_int: int > int ).

thf(tp_abs_abs_real,type,
    abs_abs_real: real > real ).

thf(tp_accp_P1096762738010456898nt_int,type,
    accp_P1096762738010456898nt_int: ( product_prod_int_int > product_prod_int_int > $o ) > product_prod_int_int > $o ).

thf(tp_accp_P2887432264394892906BT_nat,type,
    accp_P2887432264394892906BT_nat: ( produc9072475918466114483BT_nat > produc9072475918466114483BT_nat > $o ) > produc9072475918466114483BT_nat > $o ).

thf(tp_accp_P4275260045618599050at_nat,type,
    accp_P4275260045618599050at_nat: ( product_prod_nat_nat > product_prod_nat_nat > $o ) > product_prod_nat_nat > $o ).

thf(tp_accp_list_nat,type,
    accp_list_nat: ( list_nat > list_nat > $o ) > list_nat > $o ).

thf(tp_accp_nat,type,
    accp_nat: ( nat > nat > $o ) > nat > $o ).

thf(tp_algebr934650988132801477me_nat,type,
    algebr934650988132801477me_nat: nat > nat > $o ).

thf(tp_append_int,type,
    append_int: list_int > list_int > list_int ).

thf(tp_append_nat,type,
    append_nat: list_nat > list_nat > list_nat ).

thf(tp_archim2898591450579166408c_real,type,
    archim2898591450579166408c_real: real > real ).

thf(tp_archim6058952711729229775r_real,type,
    archim6058952711729229775r_real: real > int ).

thf(tp_archim7802044766580827645g_real,type,
    archim7802044766580827645g_real: real > int ).

thf(tp_archim8280529875227126926d_real,type,
    archim8280529875227126926d_real: real > int ).

thf(tp_arcosh_real,type,
    arcosh_real: real > real ).

thf(tp_arctan,type,
    arctan: real > real ).

thf(tp_arg,type,
    arg: complex > real ).

thf(tp_arsinh_real,type,
    arsinh_real: real > real ).

thf(tp_artanh_real,type,
    artanh_real: real > real ).

thf(tp_at_bot_real,type,
    at_bot_real: filter_real ).

thf(tp_at_top_nat,type,
    at_top_nat: filter_nat ).

thf(tp_at_top_real,type,
    at_top_real: filter_real ).

thf(tp_bNF_Ca8459412986667044542atLess,type,
    bNF_Ca8459412986667044542atLess: set_Pr1261947904930325089at_nat ).

thf(tp_bNF_Ca8665028551170535155natLeq,type,
    bNF_Ca8665028551170535155natLeq: set_Pr1261947904930325089at_nat ).

thf(tp_bNF_We3818239936649020644el_nat,type,
    bNF_We3818239936649020644el_nat: set_Pr1261947904930325089at_nat > $o ).

thf(tp_bNF_re2241393799969408733at_nat,type,
    bNF_re2241393799969408733at_nat: ( product_prod_nat_nat > product_prod_nat_nat > $o ) > ( product_prod_nat_nat > product_prod_nat_nat > $o ) > ( product_prod_nat_nat > product_prod_nat_nat ) > ( product_prod_nat_nat > product_prod_nat_nat ) > $o ).

thf(tp_bNF_re3099431351363272937at_nat,type,
    bNF_re3099431351363272937at_nat: ( product_prod_nat_nat > product_prod_nat_nat > $o ) > ( ( product_prod_nat_nat > product_prod_nat_nat ) > ( product_prod_nat_nat > product_prod_nat_nat ) > $o ) > ( product_prod_nat_nat > product_prod_nat_nat > product_prod_nat_nat ) > ( product_prod_nat_nat > product_prod_nat_nat > product_prod_nat_nat ) > $o ).

thf(tp_bNF_re3666534408544137501at_o_o,type,
    bNF_re3666534408544137501at_o_o: ( product_prod_nat_nat > product_prod_nat_nat > $o ) > ( $o > $o > $o ) > ( product_prod_nat_nat > $o ) > ( product_prod_nat_nat > $o ) > $o ).

thf(tp_bNF_re4202695980764964119_nat_o,type,
    bNF_re4202695980764964119_nat_o: ( product_prod_nat_nat > product_prod_nat_nat > $o ) > ( ( product_prod_nat_nat > $o ) > ( product_prod_nat_nat > $o ) > $o ) > ( product_prod_nat_nat > product_prod_nat_nat > $o ) > ( product_prod_nat_nat > product_prod_nat_nat > $o ) > $o ).

thf(tp_bNF_re4555766996558763186at_nat,type,
    bNF_re4555766996558763186at_nat: ( product_prod_nat_nat > int > $o ) > ( nat > nat > $o ) > ( product_prod_nat_nat > nat ) > ( int > nat ) > $o ).

thf(tp_bNF_re6644619430987730960nt_o_o,type,
    bNF_re6644619430987730960nt_o_o: ( product_prod_nat_nat > int > $o ) > ( $o > $o > $o ) > ( product_prod_nat_nat > $o ) > ( int > $o ) > $o ).

thf(tp_bNF_re6830278522597306478at_int,type,
    bNF_re6830278522597306478at_int: ( nat > nat > $o ) > ( product_prod_nat_nat > int > $o ) > ( nat > product_prod_nat_nat ) > ( nat > int ) > $o ).

thf(tp_bNF_re717283939379294677_int_o,type,
    bNF_re717283939379294677_int_o: ( product_prod_nat_nat > int > $o ) > ( ( product_prod_nat_nat > $o ) > ( int > $o ) > $o ) > ( product_prod_nat_nat > product_prod_nat_nat > $o ) > ( int > int > $o ) > $o ).

thf(tp_bNF_re7400052026677387805at_int,type,
    bNF_re7400052026677387805at_int: ( product_prod_nat_nat > int > $o ) > ( product_prod_nat_nat > int > $o ) > ( product_prod_nat_nat > product_prod_nat_nat ) > ( int > int ) > $o ).

thf(tp_bNF_re7408651293131936558nt_int,type,
    bNF_re7408651293131936558nt_int: ( product_prod_nat_nat > int > $o ) > ( ( product_prod_nat_nat > product_prod_nat_nat ) > ( int > int ) > $o ) > ( product_prod_nat_nat > product_prod_nat_nat > product_prod_nat_nat ) > ( int > int > int ) > $o ).

thf(tp_bNF_re8246922863344978751at_nat,type,
    bNF_re8246922863344978751at_nat: ( product_prod_nat_nat > product_prod_nat_nat > $o ) > ( nat > nat > $o ) > ( product_prod_nat_nat > nat ) > ( product_prod_nat_nat > nat ) > $o ).

thf(tp_bezw,type,
    bezw: nat > nat > product_prod_int_int ).

thf(tp_bezw_rel,type,
    bezw_rel: product_prod_nat_nat > product_prod_nat_nat > $o ).

thf(tp_bi_tot896582865486249351at_int,type,
    bi_tot896582865486249351at_int: ( product_prod_nat_nat > int > $o ) > $o ).

thf(tp_bij_be1856998921033663316omplex,type,
    bij_be1856998921033663316omplex: ( complex > complex ) > set_complex > set_complex > $o ).

thf(tp_bij_betw_nat_complex,type,
    bij_betw_nat_complex: ( nat > complex ) > set_nat > set_complex > $o ).

thf(tp_bij_betw_nat_nat,type,
    bij_betw_nat_nat: ( nat > nat ) > set_nat > set_nat > $o ).

thf(tp_binomial,type,
    binomial: nat > nat > nat ).

thf(tp_bit0,type,
    bit0: num > num ).

thf(tp_bit1,type,
    bit1: num > num ).

thf(tp_bit_and_int_rel,type,
    bit_and_int_rel: product_prod_int_int > product_prod_int_int > $o ).

thf(tp_bit_concat_bit,type,
    bit_concat_bit: nat > int > int > int ).

thf(tp_bit_ri631733984087533419it_int,type,
    bit_ri631733984087533419it_int: nat > int > int ).

thf(tp_bit_se1146084159140164899it_int,type,
    bit_se1146084159140164899it_int: int > nat > $o ).

thf(tp_bit_se1148574629649215175it_nat,type,
    bit_se1148574629649215175it_nat: nat > nat > $o ).

thf(tp_bit_se1412395901928357646or_nat,type,
    bit_se1412395901928357646or_nat: nat > nat > nat ).

thf(tp_bit_se2000444600071755411sk_int,type,
    bit_se2000444600071755411sk_int: nat > int ).

thf(tp_bit_se2002935070580805687sk_nat,type,
    bit_se2002935070580805687sk_nat: nat > nat ).

thf(tp_bit_se2159334234014336723it_int,type,
    bit_se2159334234014336723it_int: nat > int > int ).

thf(tp_bit_se2161824704523386999it_nat,type,
    bit_se2161824704523386999it_nat: nat > nat > nat ).

thf(tp_bit_se2923211474154528505it_int,type,
    bit_se2923211474154528505it_int: nat > int > int ).

thf(tp_bit_se2925701944663578781it_nat,type,
    bit_se2925701944663578781it_nat: nat > nat > nat ).

thf(tp_bit_se4203085406695923979it_int,type,
    bit_se4203085406695923979it_int: nat > int > int ).

thf(tp_bit_se4205575877204974255it_nat,type,
    bit_se4205575877204974255it_nat: nat > nat > nat ).

thf(tp_bit_se545348938243370406it_int,type,
    bit_se545348938243370406it_int: nat > int > int ).

thf(tp_bit_se547839408752420682it_nat,type,
    bit_se547839408752420682it_nat: nat > nat > nat ).

thf(tp_bit_se6528837805403552850or_nat,type,
    bit_se6528837805403552850or_nat: nat > nat > nat ).

thf(tp_bit_se725231765392027082nd_int,type,
    bit_se725231765392027082nd_int: int > int > int ).

thf(tp_bit_se727722235901077358nd_nat,type,
    bit_se727722235901077358nd_nat: nat > nat > nat ).

thf(tp_bit_se7879613467334960850it_int,type,
    bit_se7879613467334960850it_int: nat > int > int ).

thf(tp_bit_se7882103937844011126it_nat,type,
    bit_se7882103937844011126it_nat: nat > nat > nat ).

thf(tp_bit_se8568078237143864401it_int,type,
    bit_se8568078237143864401it_int: nat > int > int ).

thf(tp_bit_se8570568707652914677it_nat,type,
    bit_se8570568707652914677it_nat: nat > nat > nat ).

thf(tp_bit_take_bit_num,type,
    bit_take_bit_num: nat > num > option_num ).

thf(tp_bot_bo1565574316222977092_nat_o,type,
    bot_bo1565574316222977092_nat_o: vEBT_VEBT > nat > $o ).

thf(tp_bot_bo1642239108664514429BT_nat,type,
    bot_bo1642239108664514429BT_nat: set_Pr7556676689462069481BT_nat ).

thf(tp_bot_bo1796632182523588997nt_int,type,
    bot_bo1796632182523588997nt_int: set_Pr958786334691620121nt_int ).

thf(tp_bot_bo1954855461789132331enat_o,type,
    bot_bo1954855461789132331enat_o: extended_enat > $o ).

thf(tp_bot_bo2099793752762293965at_nat,type,
    bot_bo2099793752762293965at_nat: set_Pr1261947904930325089at_nat ).

thf(tp_bot_bo4199563552545308370d_enat,type,
    bot_bo4199563552545308370d_enat: extended_enat ).

thf(tp_bot_bo4898103413517107610_nat_o,type,
    bot_bo4898103413517107610_nat_o: product_prod_nat_nat > product_prod_nat_nat > $o ).

thf(tp_bot_bo5327735625951526323at_nat,type,
    bot_bo5327735625951526323at_nat: set_Pr8693737435421807431at_nat ).

thf(tp_bot_bo7653980558646680370d_enat,type,
    bot_bo7653980558646680370d_enat: set_Extended_enat ).

thf(tp_bot_bo8194388402131092736T_VEBT,type,
    bot_bo8194388402131092736T_VEBT: set_VEBT_VEBT ).

thf(tp_bot_bot_filter_nat,type,
    bot_bot_filter_nat: filter_nat ).

thf(tp_bot_bot_int_int_o,type,
    bot_bot_int_int_o: int > int > $o ).

thf(tp_bot_bot_int_o,type,
    bot_bot_int_o: int > $o ).

thf(tp_bot_bot_list_nat_o,type,
    bot_bot_list_nat_o: list_nat > $o ).

thf(tp_bot_bot_nat,type,
    bot_bot_nat: nat ).

thf(tp_bot_bot_nat_nat_o,type,
    bot_bot_nat_nat_o: nat > nat > $o ).

thf(tp_bot_bot_nat_o,type,
    bot_bot_nat_o: nat > $o ).

thf(tp_bot_bot_real_o,type,
    bot_bot_real_o: real > $o ).

thf(tp_bot_bot_set_complex,type,
    bot_bot_set_complex: set_complex ).

thf(tp_bot_bot_set_int,type,
    bot_bot_set_int: set_int ).

thf(tp_bot_bot_set_list_nat,type,
    bot_bot_set_list_nat: set_list_nat ).

thf(tp_bot_bot_set_nat,type,
    bot_bot_set_nat: set_nat ).

thf(tp_bot_bot_set_nat_o,type,
    bot_bot_set_nat_o: set_nat > $o ).

thf(tp_bot_bot_set_real,type,
    bot_bot_set_real: set_real ).

thf(tp_bot_bot_set_set_int,type,
    bot_bot_set_set_int: set_set_int ).

thf(tp_bot_bot_set_set_nat,type,
    bot_bot_set_set_nat: set_set_nat ).

thf(tp_case_nat_nat,type,
    case_nat_nat: nat > ( nat > nat ) > nat > nat ).

thf(tp_case_nat_o,type,
    case_nat_o: $o > ( nat > $o ) > nat > $o ).

thf(tp_case_o184042715313410164at_nat,type,
    case_o184042715313410164at_nat: $o > ( product_prod_nat_nat > $o ) > option4927543243414619207at_nat > $o ).

thf(tp_case_o6005452278849405969um_num,type,
    case_o6005452278849405969um_num: option_num > ( num > option_num ) > option_num > option_num ).

thf(tp_case_option_num_num,type,
    case_option_num_num: num > ( num > num ) > option_num > num ).

thf(tp_cis,type,
    cis: real > complex ).

thf(tp_collec213857154873943460nt_int,type,
    collec213857154873943460nt_int: ( product_prod_int_int > $o ) > set_Pr958786334691620121nt_int ).

thf(tp_collec2260605976452661553d_enat,type,
    collec2260605976452661553d_enat: ( set_Extended_enat > $o ) > set_se7270636423289371942d_enat ).

thf(tp_collec3392354462482085612at_nat,type,
    collec3392354462482085612at_nat: ( product_prod_nat_nat > $o ) > set_Pr1261947904930325089at_nat ).

thf(tp_collec4429806609662206161d_enat,type,
    collec4429806609662206161d_enat: ( extended_enat > $o ) > set_Extended_enat ).

thf(tp_collec5608196760682091941T_VEBT,type,
    collec5608196760682091941T_VEBT: ( list_VEBT_VEBT > $o ) > set_list_VEBT_VEBT ).

thf(tp_collec8433460942617342167d_enat,type,
    collec8433460942617342167d_enat: ( list_Extended_enat > $o ) > set_li5464603477888414924d_enat ).

thf(tp_collect_complex,type,
    collect_complex: ( complex > $o ) > set_complex ).

thf(tp_collect_int,type,
    collect_int: ( int > $o ) > set_int ).

thf(tp_collect_list_complex,type,
    collect_list_complex: ( list_complex > $o ) > set_list_complex ).

thf(tp_collect_list_int,type,
    collect_list_int: ( list_int > $o ) > set_list_int ).

thf(tp_collect_list_nat,type,
    collect_list_nat: ( list_nat > $o ) > set_list_nat ).

thf(tp_collect_nat,type,
    collect_nat: ( nat > $o ) > set_nat ).

thf(tp_collect_real,type,
    collect_real: ( real > $o ) > set_real ).

thf(tp_collect_set_complex,type,
    collect_set_complex: ( set_complex > $o ) > set_set_complex ).

thf(tp_collect_set_int,type,
    collect_set_int: ( set_int > $o ) > set_set_int ).

thf(tp_collect_set_nat,type,
    collect_set_nat: ( set_nat > $o ) > set_set_nat ).

thf(tp_comm_s2602460028002588243omplex,type,
    comm_s2602460028002588243omplex: complex > nat > complex ).

thf(tp_comm_s3181272606743183617d_enat,type,
    comm_s3181272606743183617d_enat: extended_enat > nat > extended_enat ).

thf(tp_comm_s4660882817536571857er_int,type,
    comm_s4660882817536571857er_int: int > nat > int ).

thf(tp_comm_s4663373288045622133er_nat,type,
    comm_s4663373288045622133er_nat: nat > nat > nat ).

thf(tp_comm_s629917340098488124ar_nat,type,
    comm_s629917340098488124ar_nat: char > nat ).

thf(tp_comm_s7457072308508201937r_real,type,
    comm_s7457072308508201937r_real: real > nat > real ).

thf(tp_comp_int_nat_int,type,
    comp_int_nat_int: ( int > nat ) > ( int > int ) > int > nat ).

thf(tp_comp_nat_nat_nat,type,
    comp_nat_nat_nat: ( nat > nat ) > ( nat > nat ) > nat > nat ).

thf(tp_comple2295165028678016749d_enat,type,
    comple2295165028678016749d_enat: set_Extended_enat > extended_enat ).

thf(tp_comple4398354569131411667d_enat,type,
    comple4398354569131411667d_enat: set_Extended_enat > extended_enat ).

thf(tp_comple7399068483239264473et_nat,type,
    comple7399068483239264473et_nat: set_set_nat > set_nat ).

thf(tp_comple7806235888213564991et_nat,type,
    comple7806235888213564991et_nat: set_set_nat > set_nat ).

thf(tp_complete_Inf_Inf_nat,type,
    complete_Inf_Inf_nat: set_nat > nat ).

thf(tp_complete_Sup_Sup_nat,type,
    complete_Sup_Sup_nat: set_nat > nat ).

thf(tp_compow_nat_nat,type,
    compow_nat_nat: nat > ( nat > nat ) > nat > nat ).

thf(tp_condit2214826472909112428ve_nat,type,
    condit2214826472909112428ve_nat: set_nat > $o ).

thf(tp_cons_int,type,
    cons_int: int > list_int > list_int ).

thf(tp_cons_nat,type,
    cons_nat: nat > list_nat > list_nat ).

thf(tp_cos_coeff,type,
    cos_coeff: nat > real ).

thf(tp_cos_complex,type,
    cos_complex: complex > complex ).

thf(tp_cos_real,type,
    cos_real: real > real ).

thf(tp_count_101369445342291426d_enat,type,
    count_101369445342291426d_enat: list_Extended_enat > extended_enat > nat ).

thf(tp_count_list_VEBT_VEBT,type,
    count_list_VEBT_VEBT: list_VEBT_VEBT > vEBT_VEBT > nat ).

thf(tp_count_list_complex,type,
    count_list_complex: list_complex > complex > nat ).

thf(tp_count_list_int,type,
    count_list_int: list_int > int > nat ).

thf(tp_count_list_nat,type,
    count_list_nat: list_nat > nat > nat ).

thf(tp_count_list_real,type,
    count_list_real: list_real > real > nat ).

thf(tp_count_list_set_nat,type,
    count_list_set_nat: list_set_nat > set_nat > nat ).

thf(tp_deg,type,
    deg: nat ).

thf(tp_diffs_complex,type,
    diffs_complex: ( nat > complex ) > nat > complex ).

thf(tp_diffs_int,type,
    diffs_int: ( nat > int ) > nat > int ).

thf(tp_diffs_real,type,
    diffs_real: ( nat > real ) > nat > real ).

thf(tp_distinct_int,type,
    distinct_int: list_int > $o ).

thf(tp_distinct_nat,type,
    distinct_nat: list_nat > $o ).

thf(tp_divide1717551699836669952omplex,type,
    divide1717551699836669952omplex: complex > complex > complex ).

thf(tp_divide_divide_int,type,
    divide_divide_int: int > int > int ).

thf(tp_divide_divide_nat,type,
    divide_divide_nat: nat > nat > nat ).

thf(tp_divide_divide_real,type,
    divide_divide_real: real > real > real ).

thf(tp_divmod_nat,type,
    divmod_nat: nat > nat > product_prod_nat_nat ).

thf(tp_drop_nat,type,
    drop_nat: nat > list_nat > list_nat ).

thf(tp_dvd_dv3785147216227455552d_enat,type,
    dvd_dv3785147216227455552d_enat: extended_enat > extended_enat > $o ).

thf(tp_dvd_dvd_complex,type,
    dvd_dvd_complex: complex > complex > $o ).

thf(tp_dvd_dvd_int,type,
    dvd_dvd_int: int > int > $o ).

thf(tp_dvd_dvd_nat,type,
    dvd_dvd_nat: nat > nat > $o ).

thf(tp_dvd_dvd_real,type,
    dvd_dvd_real: real > real > $o ).

thf(tp_enumerate_VEBT_VEBT,type,
    enumerate_VEBT_VEBT: nat > list_VEBT_VEBT > list_P5647936690300460905T_VEBT ).

thf(tp_enumerate_int,type,
    enumerate_int: nat > list_int > list_P3521021558325789923at_int ).

thf(tp_enumerate_nat,type,
    enumerate_nat: nat > list_nat > list_P6011104703257516679at_nat ).

thf(tp_eventu1038000079068216329at_nat,type,
    eventu1038000079068216329at_nat: ( product_prod_nat_nat > $o ) > filter1242075044329608583at_nat > $o ).

thf(tp_eventually_nat,type,
    eventually_nat: ( nat > $o ) > filter_nat > $o ).

thf(tp_exp_real,type,
    exp_real: real > real ).

thf(tp_extend3600170679010898289d_enat,type,
    extend3600170679010898289d_enat: ( nat > extended_enat ) > extended_enat > extended_enat > extended_enat ).

thf(tp_extend5688581933313929465d_enat,type,
    extend5688581933313929465d_enat: extended_enat ).

thf(tp_extended_case_enat_o,type,
    extended_case_enat_o: ( nat > $o ) > $o > extended_enat > $o ).

thf(tp_extended_eSuc,type,
    extended_eSuc: extended_enat > extended_enat ).

thf(tp_extended_enat2,type,
    extended_enat2: nat > extended_enat ).

thf(tp_field_5140801741446780682s_real,type,
    field_5140801741446780682s_real: set_real ).

thf(tp_field_nat,type,
    field_nat: set_Pr1261947904930325089at_nat > set_nat ).

thf(tp_filterlim_nat_nat,type,
    filterlim_nat_nat: ( nat > nat ) > filter_nat > filter_nat > $o ).

thf(tp_filterlim_nat_real,type,
    filterlim_nat_real: ( nat > real ) > filter_real > filter_nat > $o ).

thf(tp_filterlim_real_real,type,
    filterlim_real_real: ( real > real ) > filter_real > filter_real > $o ).

thf(tp_find_Extended_enat,type,
    find_Extended_enat: ( extended_enat > $o ) > list_Extended_enat > option_Extended_enat ).

thf(tp_find_P8199882355184865565at_nat,type,
    find_P8199882355184865565at_nat: ( product_prod_nat_nat > $o ) > list_P6011104703257516679at_nat > option4927543243414619207at_nat ).

thf(tp_find_VEBT_VEBT,type,
    find_VEBT_VEBT: ( vEBT_VEBT > $o ) > list_VEBT_VEBT > option_VEBT_VEBT ).

thf(tp_find_int,type,
    find_int: ( int > $o ) > list_int > option_int ).

thf(tp_find_nat,type,
    find_nat: ( nat > $o ) > list_nat > option_nat ).

thf(tp_find_num,type,
    find_num: ( num > $o ) > list_num > option_num ).

thf(tp_find_real,type,
    find_real: ( real > $o ) > list_real > option_real ).

thf(tp_find_set_nat,type,
    find_set_nat: ( set_nat > $o ) > list_set_nat > option_set_nat ).

thf(tp_finite1152437895449049373et_nat,type,
    finite1152437895449049373et_nat: set_set_nat > $o ).

thf(tp_finite1862508098717546133d_enat,type,
    finite1862508098717546133d_enat: set_li5464603477888414924d_enat > $o ).

thf(tp_finite3004134309566078307T_VEBT,type,
    finite3004134309566078307T_VEBT: set_list_VEBT_VEBT > $o ).

thf(tp_finite3207457112153483333omplex,type,
    finite3207457112153483333omplex: set_complex > $o ).

thf(tp_finite3922522038869484883st_int,type,
    finite3922522038869484883st_int: set_list_int > $o ).

thf(tp_finite4001608067531595151d_enat,type,
    finite4001608067531595151d_enat: set_Extended_enat > $o ).

thf(tp_finite410649719033368117t_unit,type,
    finite410649719033368117t_unit: set_Product_unit > nat ).

thf(tp_finite5468666774076196335d_enat,type,
    finite5468666774076196335d_enat: set_se7270636423289371942d_enat > $o ).

thf(tp_finite5795047828879050333T_VEBT,type,
    finite5795047828879050333T_VEBT: set_VEBT_VEBT > $o ).

thf(tp_finite6197958912794628473et_int,type,
    finite6197958912794628473et_int: set_set_int > $o ).

thf(tp_finite6551019134538273531omplex,type,
    finite6551019134538273531omplex: set_set_complex > $o ).

thf(tp_finite8100373058378681591st_nat,type,
    finite8100373058378681591st_nat: set_list_nat > $o ).

thf(tp_finite8712137658972009173omplex,type,
    finite8712137658972009173omplex: set_list_complex > $o ).

thf(tp_finite_card_complex,type,
    finite_card_complex: set_complex > nat ).

thf(tp_finite_card_int,type,
    finite_card_int: set_int > nat ).

thf(tp_finite_card_list_nat,type,
    finite_card_list_nat: set_list_nat > nat ).

thf(tp_finite_card_nat,type,
    finite_card_nat: set_nat > nat ).

thf(tp_finite_card_set_nat,type,
    finite_card_set_nat: set_set_nat > nat ).

thf(tp_finite_finite_int,type,
    finite_finite_int: set_int > $o ).

thf(tp_finite_finite_nat,type,
    finite_finite_nat: set_nat > $o ).

thf(tp_finite_finite_real,type,
    finite_finite_real: set_real > $o ).

thf(tp_fun_is_measure_int,type,
    fun_is_measure_int: ( int > nat ) > $o ).

thf(tp_fun_pair_leq,type,
    fun_pair_leq: set_Pr8693737435421807431at_nat ).

thf(tp_fun_pair_less,type,
    fun_pair_less: set_Pr8693737435421807431at_nat ).

thf(tp_gbinomial_complex,type,
    gbinomial_complex: complex > nat > complex ).

thf(tp_gbinomial_int,type,
    gbinomial_int: int > nat > int ).

thf(tp_gbinomial_nat,type,
    gbinomial_nat: nat > nat > nat ).

thf(tp_gbinomial_real,type,
    gbinomial_real: real > nat > real ).

thf(tp_gcd_Gcd_nat,type,
    gcd_Gcd_nat: set_nat > nat ).

thf(tp_gen_length_VEBT_VEBT,type,
    gen_length_VEBT_VEBT: nat > list_VEBT_VEBT > nat ).

thf(tp_gen_length_int,type,
    gen_length_int: nat > list_int > nat ).

thf(tp_gen_length_nat,type,
    gen_length_nat: nat > list_nat > nat ).

thf(tp_groups129246275422532515t_real,type,
    groups129246275422532515t_real: ( nat > real ) > set_nat > real ).

thf(tp_groups1681761925125756287l_real,type,
    groups1681761925125756287l_real: ( real > real ) > set_real > real ).

thf(tp_groups1705073143266064639nt_int,type,
    groups1705073143266064639nt_int: ( int > int ) > set_int > int ).

thf(tp_groups1707563613775114915nt_nat,type,
    groups1707563613775114915nt_nat: ( int > nat ) > set_int > nat ).

thf(tp_groups1752964319039525884d_enat,type,
    groups1752964319039525884d_enat: ( complex > extended_enat ) > set_complex > extended_enat ).

thf(tp_groups1932886352136224148al_int,type,
    groups1932886352136224148al_int: ( real > int ) > set_real > int ).

thf(tp_groups1935376822645274424al_nat,type,
    groups1935376822645274424al_nat: ( real > nat ) > set_real > nat ).

thf(tp_groups2025484359314973016at_int,type,
    groups2025484359314973016at_int: ( extended_enat > int ) > set_Extended_enat > int ).

thf(tp_groups2027974829824023292at_nat,type,
    groups2027974829824023292at_nat: ( extended_enat > nat ) > set_Extended_enat > nat ).

thf(tp_groups2073611262835488442omplex,type,
    groups2073611262835488442omplex: ( nat > complex ) > set_nat > complex ).

thf(tp_groups2316167850115554303t_real,type,
    groups2316167850115554303t_real: ( int > real ) > set_int > real ).

thf(tp_groups2433450451889696826d_enat,type,
    groups2433450451889696826d_enat: ( extended_enat > extended_enat ) > set_Extended_enat > extended_enat ).

thf(tp_groups2800946370649118462d_enat,type,
    groups2800946370649118462d_enat: ( real > extended_enat ) > set_real > extended_enat ).

thf(tp_groups2878480467620962989at_int,type,
    groups2878480467620962989at_int: ( extended_enat > int ) > set_Extended_enat > int ).

thf(tp_groups2880970938130013265at_nat,type,
    groups2880970938130013265at_nat: ( extended_enat > nat ) > set_Extended_enat > nat ).

thf(tp_groups3539618377306564664at_int,type,
    groups3539618377306564664at_int: ( nat > int ) > set_nat > int ).

thf(tp_groups3542108847815614940at_nat,type,
    groups3542108847815614940at_nat: ( nat > nat ) > set_nat > nat ).

thf(tp_groups3619160379726066777t_real,type,
    groups3619160379726066777t_real: ( set_nat > real ) > set_set_nat > real ).

thf(tp_groups3708469109370488835omplex,type,
    groups3708469109370488835omplex: ( complex > complex ) > set_complex > complex ).

thf(tp_groups4075276357253098568at_int,type,
    groups4075276357253098568at_int: ( product_prod_nat_nat > int ) > set_Pr1261947904930325089at_nat > int ).

thf(tp_groups4077766827762148844at_nat,type,
    groups4077766827762148844at_nat: ( product_prod_nat_nat > nat ) > set_Pr1261947904930325089at_nat > nat ).

thf(tp_groups4148127829035722712t_real,type,
    groups4148127829035722712t_real: ( extended_enat > real ) > set_Extended_enat > real ).

thf(tp_groups4225252721152677374d_enat,type,
    groups4225252721152677374d_enat: ( int > extended_enat ) > set_int > extended_enat ).

thf(tp_groups4538972089207619220nt_int,type,
    groups4538972089207619220nt_int: ( int > int ) > set_int > int ).

thf(tp_groups4541462559716669496nt_nat,type,
    groups4541462559716669496nt_nat: ( int > nat ) > set_int > nat ).

thf(tp_groups4561878855575611511st_nat,type,
    groups4561878855575611511st_nat: list_nat > nat ).

thf(tp_groups4567486121110086003t_real,type,
    groups4567486121110086003t_real: ( product_prod_nat_nat > real ) > set_Pr1261947904930325089at_nat > real ).

thf(tp_groups4622424608036095791omplex,type,
    groups4622424608036095791omplex: ( extended_enat > complex ) > set_Extended_enat > complex ).

thf(tp_groups4694064378042380927al_int,type,
    groups4694064378042380927al_int: ( real > int ) > set_real > int ).

thf(tp_groups4696554848551431203al_nat,type,
    groups4696554848551431203al_nat: ( real > nat ) > set_real > nat ).

thf(tp_groups5078248829458667347d_enat,type,
    groups5078248829458667347d_enat: ( int > extended_enat ) > set_int > extended_enat ).

thf(tp_groups5107569545109728110t_real,type,
    groups5107569545109728110t_real: ( set_nat > real ) > set_set_nat > real ).

thf(tp_groups5690904116761175830ex_int,type,
    groups5690904116761175830ex_int: ( complex > int ) > set_complex > int ).

thf(tp_groups5693394587270226106ex_nat,type,
    groups5693394587270226106ex_nat: ( complex > nat ) > set_complex > nat ).

thf(tp_groups5754745047067104278omplex,type,
    groups5754745047067104278omplex: ( real > complex ) > set_real > complex ).

thf(tp_groups5808333547571424918x_real,type,
    groups5808333547571424918x_real: ( complex > real ) > set_complex > real ).

thf(tp_groups6464643781859351333omplex,type,
    groups6464643781859351333omplex: ( nat > complex ) > set_nat > complex ).

thf(tp_groups6591440286371151544t_real,type,
    groups6591440286371151544t_real: ( nat > real ) > set_nat > real ).

thf(tp_groups6818542070133387226omplex,type,
    groups6818542070133387226omplex: ( extended_enat > complex ) > set_Extended_enat > complex ).

thf(tp_groups705719431365010083at_int,type,
    groups705719431365010083at_int: ( nat > int ) > set_nat > int ).

thf(tp_groups708209901874060359at_nat,type,
    groups708209901874060359at_nat: ( nat > nat ) > set_nat > nat ).

thf(tp_groups7108830773950497114d_enat,type,
    groups7108830773950497114d_enat: ( nat > extended_enat ) > set_nat > extended_enat ).

thf(tp_groups713298508707869441omplex,type,
    groups713298508707869441omplex: ( real > complex ) > set_real > complex ).

thf(tp_groups7440179247065528705omplex,type,
    groups7440179247065528705omplex: ( int > complex ) > set_int > complex ).

thf(tp_groups766887009212190081x_real,type,
    groups766887009212190081x_real: ( complex > real ) > set_complex > real ).

thf(tp_groups771621172384141258BT_nat,type,
    groups771621172384141258BT_nat: ( vEBT_VEBT > nat ) > set_VEBT_VEBT > nat ).

thf(tp_groups7754918857620584856omplex,type,
    groups7754918857620584856omplex: ( complex > complex ) > set_complex > complex ).

thf(tp_groups7961826882256487087d_enat,type,
    groups7961826882256487087d_enat: ( nat > extended_enat ) > set_nat > extended_enat ).

thf(tp_groups7973222482632965587d_enat,type,
    groups7973222482632965587d_enat: ( real > extended_enat ) > set_real > extended_enat ).

thf(tp_groups8097168146408367636l_real,type,
    groups8097168146408367636l_real: ( real > real ) > set_real > real ).

thf(tp_groups8292507037921071086at_int,type,
    groups8292507037921071086at_int: ( set_nat > int ) > set_set_nat > int ).

thf(tp_groups8294997508430121362at_nat,type,
    groups8294997508430121362at_nat: ( set_nat > nat ) > set_set_nat > nat ).

thf(tp_groups858564598930262913ex_int,type,
    groups858564598930262913ex_int: ( complex > int ) > set_complex > int ).

thf(tp_groups861055069439313189ex_nat,type,
    groups861055069439313189ex_nat: ( complex > nat ) > set_complex > nat ).

thf(tp_groups8778361861064173332t_real,type,
    groups8778361861064173332t_real: ( int > real ) > set_int > real ).

thf(tp_groups8780218893797010257d_enat,type,
    groups8780218893797010257d_enat: ( complex > extended_enat ) > set_complex > extended_enat ).

thf(tp_groups8932437906259616549d_enat,type,
    groups8932437906259616549d_enat: ( extended_enat > extended_enat ) > set_Extended_enat > extended_enat ).

thf(tp_groups97031904164794029t_real,type,
    groups97031904164794029t_real: ( extended_enat > real ) > set_Extended_enat > real ).

thf(tp_groups977919841031483927at_nat,type,
    groups977919841031483927at_nat: ( product_prod_nat_nat > nat ) > set_Pr1261947904930325089at_nat > nat ).

thf(tp_has_fi5821293074295781190e_real,type,
    has_fi5821293074295781190e_real: ( real > real ) > real > filter_real > $o ).

thf(tp_hd_nat,type,
    hd_nat: list_nat > nat ).

thf(tp_i,type,
    i: nat ).

thf(tp_id_nat,type,
    id_nat: nat > nat ).

thf(tp_id_o,type,
    id_o: $o > $o ).

thf(tp_if_Extended_enat,type,
    if_Extended_enat: $o > extended_enat > extended_enat > extended_enat ).

thf(tp_if_Pro3027730157355071871nt_int,type,
    if_Pro3027730157355071871nt_int: $o > product_prod_int_int > product_prod_int_int > product_prod_int_int ).

thf(tp_if_Pro6206227464963214023at_nat,type,
    if_Pro6206227464963214023at_nat: $o > product_prod_nat_nat > product_prod_nat_nat > product_prod_nat_nat ).

thf(tp_if_VEBT_VEBT,type,
    if_VEBT_VEBT: $o > vEBT_VEBT > vEBT_VEBT > vEBT_VEBT ).

thf(tp_if_complex,type,
    if_complex: $o > complex > complex > complex ).

thf(tp_if_int,type,
    if_int: $o > int > int > int ).

thf(tp_if_int_int,type,
    if_int_int: $o > ( int > int ) > ( int > int ) > int > int ).

thf(tp_if_list_int,type,
    if_list_int: $o > list_int > list_int > list_int ).

thf(tp_if_list_nat,type,
    if_list_nat: $o > list_nat > list_nat > list_nat ).

thf(tp_if_nat,type,
    if_nat: $o > nat > nat > nat ).

thf(tp_if_option_num,type,
    if_option_num: $o > option_num > option_num > option_num ).

thf(tp_if_real,type,
    if_real: $o > real > real > real ).

thf(tp_if_set_int,type,
    if_set_int: $o > set_int > set_int > set_int ).

thf(tp_if_set_nat,type,
    if_set_nat: $o > set_nat > set_nat > set_nat ).

thf(tp_image_80655429650038917d_enat,type,
    image_80655429650038917d_enat: ( extended_enat > extended_enat ) > set_Extended_enat > set_Extended_enat ).

thf(tp_image_char_nat,type,
    image_char_nat: ( char > nat ) > set_char > set_nat ).

thf(tp_image_int_int,type,
    image_int_int: ( int > int ) > set_int > set_int ).

thf(tp_image_int_nat,type,
    image_int_nat: ( int > nat ) > set_int > set_nat ).

thf(tp_image_nat_char,type,
    image_nat_char: ( nat > char ) > set_nat > set_char ).

thf(tp_image_nat_int,type,
    image_nat_int: ( nat > int ) > set_nat > set_int ).

thf(tp_image_nat_nat,type,
    image_nat_nat: ( nat > nat ) > set_nat > set_nat ).

thf(tp_image_nat_set_nat,type,
    image_nat_set_nat: ( nat > set_nat ) > set_nat > set_set_nat ).

thf(tp_image_real_real,type,
    image_real_real: ( real > real ) > set_real > set_real ).

thf(tp_inc,type,
    inc: num > num ).

thf(tp_inf_in2572325071724192079at_nat,type,
    inf_in2572325071724192079at_nat: set_Pr1261947904930325089at_nat > set_Pr1261947904930325089at_nat > set_Pr1261947904930325089at_nat ).

thf(tp_inf_inf_int,type,
    inf_inf_int: int > int > int ).

thf(tp_inf_inf_nat,type,
    inf_inf_nat: nat > nat > nat ).

thf(tp_infini8530281810654367211te_nat,type,
    infini8530281810654367211te_nat: set_nat > nat > nat ).

thf(tp_inj_on_nat_char,type,
    inj_on_nat_char: ( nat > char ) > set_nat > $o ).

thf(tp_inj_on_nat_nat,type,
    inj_on_nat_nat: ( nat > nat ) > set_nat > $o ).

thf(tp_inj_on_real_real,type,
    inj_on_real_real: ( real > real ) > set_real > $o ).

thf(tp_inj_on_set_nat_nat,type,
    inj_on_set_nat_nat: ( set_nat > nat ) > set_set_nat > $o ).

thf(tp_insert_Extended_enat,type,
    insert_Extended_enat: extended_enat > set_Extended_enat > set_Extended_enat ).

thf(tp_insert_VEBT_VEBT,type,
    insert_VEBT_VEBT: vEBT_VEBT > set_VEBT_VEBT > set_VEBT_VEBT ).

thf(tp_insert_complex,type,
    insert_complex: complex > set_complex > set_complex ).

thf(tp_insert_int,type,
    insert_int: int > set_int > set_int ).

thf(tp_insert_list_nat,type,
    insert_list_nat: list_nat > set_list_nat > set_list_nat ).

thf(tp_insert_nat,type,
    insert_nat: nat > set_nat > set_nat ).

thf(tp_insert_real,type,
    insert_real: real > set_real > set_real ).

thf(tp_insert_set_nat,type,
    insert_set_nat: set_nat > set_set_nat > set_set_nat ).

thf(tp_int_ge_less_than,type,
    int_ge_less_than: int > set_Pr958786334691620121nt_int ).

thf(tp_int_ge_less_than2,type,
    int_ge_less_than2: int > set_Pr958786334691620121nt_int ).

thf(tp_intrel,type,
    intrel: product_prod_nat_nat > product_prod_nat_nat > $o ).

thf(tp_inverse_inverse_real,type,
    inverse_inverse_real: real > real ).

thf(tp_last_nat,type,
    last_nat: list_nat > nat ).

thf(tp_lattic1189837152898106425t_real,type,
    lattic1189837152898106425t_real: ( extended_enat > real ) > set_Extended_enat > extended_enat ).

thf(tp_lattic1996716550891908761d_enat,type,
    lattic1996716550891908761d_enat: ( extended_enat > extended_enat ) > set_Extended_enat > extended_enat ).

thf(tp_lattic2675449441010098035t_real,type,
    lattic2675449441010098035t_real: ( int > real ) > set_int > int ).

thf(tp_lattic3845382081240766429at_nat,type,
    lattic3845382081240766429at_nat: ( extended_enat > nat ) > set_Extended_enat > extended_enat ).

thf(tp_lattic488527866317076247t_real,type,
    lattic488527866317076247t_real: ( nat > real ) > set_nat > nat ).

thf(tp_lattic5055836439445974935al_nat,type,
    lattic5055836439445974935al_nat: ( real > nat ) > set_real > real ).

thf(tp_lattic5364784637807008409ex_nat,type,
    lattic5364784637807008409ex_nat: ( complex > nat ) > set_complex > complex ).

thf(tp_lattic6042659972569420511d_enat,type,
    lattic6042659972569420511d_enat: ( int > extended_enat ) > set_int > int ).

thf(tp_lattic7446932960582359483at_nat,type,
    lattic7446932960582359483at_nat: ( nat > nat ) > set_nat > nat ).

thf(tp_lattic7796887085614042845d_enat,type,
    lattic7796887085614042845d_enat: ( complex > extended_enat ) > set_complex > complex ).

thf(tp_lattic8265883725875713057ax_nat,type,
    lattic8265883725875713057ax_nat: set_nat > nat ).

thf(tp_lattic8440615504127631091l_real,type,
    lattic8440615504127631091l_real: ( real > real ) > set_real > real ).

thf(tp_lattic8446286672483414039nt_nat,type,
    lattic8446286672483414039nt_nat: ( int > nat ) > set_int > int ).

thf(tp_lattic8794016678065449205x_real,type,
    lattic8794016678065449205x_real: ( complex > real ) > set_complex > complex ).

thf(tp_lattic8926238025367240251d_enat,type,
    lattic8926238025367240251d_enat: ( nat > extended_enat ) > set_nat > nat ).

thf(tp_lattic9066027731366277983d_enat,type,
    lattic9066027731366277983d_enat: ( real > extended_enat ) > set_real > real ).

thf(tp_lattic921264341876707157d_enat,type,
    lattic921264341876707157d_enat: set_Extended_enat > extended_enat ).

thf(tp_less_than,type,
    less_than: set_Pr1261947904930325089at_nat ).

thf(tp_linord1735203802627413978nt_int,type,
    linord1735203802627413978nt_int: ( int > int ) > list_int > list_int ).

thf(tp_linord2614967742042102400et_nat,type,
    linord2614967742042102400et_nat: set_nat > list_nat ).

thf(tp_linord738340561235409698at_nat,type,
    linord738340561235409698at_nat: ( nat > nat ) > list_nat > list_nat ).

thf(tp_list_u1324408373059187874T_VEBT,type,
    list_u1324408373059187874T_VEBT: list_VEBT_VEBT > nat > vEBT_VEBT > list_VEBT_VEBT ).

thf(tp_list_u3071683517702156500d_enat,type,
    list_u3071683517702156500d_enat: list_Extended_enat > nat > extended_enat > list_Extended_enat ).

thf(tp_list_u6180841689913720943at_nat,type,
    list_u6180841689913720943at_nat: list_P6011104703257516679at_nat > nat > product_prod_nat_nat > list_P6011104703257516679at_nat ).

thf(tp_list_update_int,type,
    list_update_int: list_int > nat > int > list_int ).

thf(tp_list_update_nat,type,
    list_update_nat: list_nat > nat > nat > list_nat ).

thf(tp_list_update_real,type,
    list_update_real: list_real > nat > real > list_real ).

thf(tp_list_update_set_nat,type,
    list_update_set_nat: list_set_nat > nat > set_nat > list_set_nat ).

thf(tp_listre4828114922151135584at_nat,type,
    listre4828114922151135584at_nat: set_Pr8693737435421807431at_nat > set_Pr1542805901266377927at_nat ).

thf(tp_listrel1_VEBT_VEBT,type,
    listrel1_VEBT_VEBT: set_Pr6192946355708809607T_VEBT > set_Pr1916528119006554503T_VEBT ).

thf(tp_listrel1_int,type,
    listrel1_int: set_Pr958786334691620121nt_int > set_Pr765067013931698361st_int ).

thf(tp_listrel1_nat,type,
    listrel1_nat: set_Pr1261947904930325089at_nat > set_Pr3451248702717554689st_nat ).

thf(tp_listrel1p_int,type,
    listrel1p_int: ( int > int > $o ) > list_int > list_int > $o ).

thf(tp_listrel1p_nat,type,
    listrel1p_nat: ( nat > nat > $o ) > list_nat > list_nat > $o ).

thf(tp_ln_ln_real,type,
    ln_ln_real: real > real ).

thf(tp_log,type,
    log: real > real > real ).

thf(tp_m,type,
    m: nat ).

thf(tp_ma,type,
    ma: nat ).

thf(tp_map_fu2345160673673942751at_nat,type,
    map_fu2345160673673942751at_nat: ( int > product_prod_nat_nat ) > ( nat > nat ) > ( product_prod_nat_nat > nat ) > int > nat ).

thf(tp_map_fu3667384564859982768at_int,type,
    map_fu3667384564859982768at_int: ( int > product_prod_nat_nat ) > ( product_prod_nat_nat > int ) > ( product_prod_nat_nat > product_prod_nat_nat ) > int > int ).

thf(tp_map_fu434086159418415080_int_o,type,
    map_fu434086159418415080_int_o: ( int > product_prod_nat_nat ) > ( ( product_prod_nat_nat > $o ) > int > $o ) > ( product_prod_nat_nat > product_prod_nat_nat > $o ) > int > int > $o ).

thf(tp_map_fu4826362097070443709at_o_o,type,
    map_fu4826362097070443709at_o_o: ( int > product_prod_nat_nat ) > ( $o > $o ) > ( product_prod_nat_nat > $o ) > int > $o ).

thf(tp_map_fu4960017516451851995nt_int,type,
    map_fu4960017516451851995nt_int: ( int > product_prod_nat_nat ) > ( ( product_prod_nat_nat > product_prod_nat_nat ) > int > int ) > ( product_prod_nat_nat > product_prod_nat_nat > product_prod_nat_nat ) > int > int > int ).

thf(tp_map_nat_nat,type,
    map_nat_nat: ( nat > nat ) > list_nat > list_nat ).

thf(tp_member2936631157270082147T_VEBT,type,
    member2936631157270082147T_VEBT: list_VEBT_VEBT > set_list_VEBT_VEBT > $o ).

thf(tp_member373505688050248522BT_nat,type,
    member373505688050248522BT_nat: produc9072475918466114483BT_nat > set_Pr7556676689462069481BT_nat > $o ).

thf(tp_member4439316823752958928T_VEBT,type,
    member4439316823752958928T_VEBT: produc9211091688327510695T_VEBT > set_Pr1916528119006554503T_VEBT > $o ).

thf(tp_member5262025264175285858nt_int,type,
    member5262025264175285858nt_int: product_prod_int_int > set_Pr958786334691620121nt_int > $o ).

thf(tp_member568628332442017744T_VEBT,type,
    member568628332442017744T_VEBT: produc8243902056947475879T_VEBT > set_Pr6192946355708809607T_VEBT > $o ).

thf(tp_member6693912407220327184at_nat,type,
    member6693912407220327184at_nat: produc6392793444374437607at_nat > set_Pr1542805901266377927at_nat > $o ).

thf(tp_member6698963635872716290st_int,type,
    member6698963635872716290st_int: produc1186641810826059865st_int > set_Pr765067013931698361st_int > $o ).

thf(tp_member7340969449405702474st_nat,type,
    member7340969449405702474st_nat: produc1828647624359046049st_nat > set_Pr3451248702717554689st_nat > $o ).

thf(tp_member8206827879206165904at_nat,type,
    member8206827879206165904at_nat: produc859450856879609959at_nat > set_Pr8693737435421807431at_nat > $o ).

thf(tp_member8440522571783428010at_nat,type,
    member8440522571783428010at_nat: product_prod_nat_nat > set_Pr1261947904930325089at_nat > $o ).

thf(tp_member_Extended_enat,type,
    member_Extended_enat: extended_enat > set_Extended_enat > $o ).

thf(tp_member_VEBT_VEBT,type,
    member_VEBT_VEBT: vEBT_VEBT > set_VEBT_VEBT > $o ).

thf(tp_member_complex,type,
    member_complex: complex > set_complex > $o ).

thf(tp_member_int,type,
    member_int: int > set_int > $o ).

thf(tp_member_list_int,type,
    member_list_int: list_int > set_list_int > $o ).

thf(tp_member_list_nat,type,
    member_list_nat: list_nat > set_list_nat > $o ).

thf(tp_member_nat,type,
    member_nat: nat > set_nat > $o ).

thf(tp_member_num,type,
    member_num: num > set_num > $o ).

thf(tp_member_real,type,
    member_real: real > set_real > $o ).

thf(tp_member_set_int,type,
    member_set_int: set_int > set_set_int > $o ).

thf(tp_member_set_nat,type,
    member_set_nat: set_nat > set_set_nat > $o ).

thf(tp_mi,type,
    mi: nat ).

thf(tp_minus_1139252259498527702_nat_o,type,
    minus_1139252259498527702_nat_o: ( list_nat > $o ) > ( list_nat > $o ) > list_nat > $o ).

thf(tp_minus_2020553357622893040enat_o,type,
    minus_2020553357622893040enat_o: ( extended_enat > $o ) > ( extended_enat > $o ) > extended_enat > $o ).

thf(tp_minus_2163939370556025621et_nat,type,
    minus_2163939370556025621et_nat: set_set_nat > set_set_nat > set_set_nat ).

thf(tp_minus_3235023915231533773d_enat,type,
    minus_3235023915231533773d_enat: extended_enat > extended_enat > extended_enat ).

thf(tp_minus_6910147592129066416_nat_o,type,
    minus_6910147592129066416_nat_o: ( set_nat > $o ) > ( set_nat > $o ) > set_nat > $o ).

thf(tp_minus_7954133019191499631st_nat,type,
    minus_7954133019191499631st_nat: set_list_nat > set_list_nat > set_list_nat ).

thf(tp_minus_811609699411566653omplex,type,
    minus_811609699411566653omplex: set_complex > set_complex > set_complex ).

thf(tp_minus_925952699566721837d_enat,type,
    minus_925952699566721837d_enat: set_Extended_enat > set_Extended_enat > set_Extended_enat ).

thf(tp_minus_minus_complex,type,
    minus_minus_complex: complex > complex > complex ).

thf(tp_minus_minus_int,type,
    minus_minus_int: int > int > int ).

thf(tp_minus_minus_int_o,type,
    minus_minus_int_o: ( int > $o ) > ( int > $o ) > int > $o ).

thf(tp_minus_minus_nat,type,
    minus_minus_nat: nat > nat > nat ).

thf(tp_minus_minus_nat_o,type,
    minus_minus_nat_o: ( nat > $o ) > ( nat > $o ) > nat > $o ).

thf(tp_minus_minus_real,type,
    minus_minus_real: real > real > real ).

thf(tp_minus_minus_real_o,type,
    minus_minus_real_o: ( real > $o ) > ( real > $o ) > real > $o ).

thf(tp_minus_minus_set_int,type,
    minus_minus_set_int: set_int > set_int > set_int ).

thf(tp_minus_minus_set_nat,type,
    minus_minus_set_nat: set_nat > set_nat > set_nat ).

thf(tp_minus_minus_set_real,type,
    minus_minus_set_real: set_real > set_real > set_real ).

thf(tp_modulo_modulo_int,type,
    modulo_modulo_int: int > int > int ).

thf(tp_modulo_modulo_nat,type,
    modulo_modulo_nat: nat > nat > nat ).

thf(tp_na,type,
    na: nat ).

thf(tp_nat2,type,
    nat2: int > nat ).

thf(tp_nat_list_decode,type,
    nat_list_decode: nat > list_nat ).

thf(tp_nat_list_decode_rel,type,
    nat_list_decode_rel: nat > nat > $o ).

thf(tp_nat_list_encode,type,
    nat_list_encode: list_nat > nat ).

thf(tp_nat_list_encode_rel,type,
    nat_list_encode_rel: list_nat > list_nat > $o ).

thf(tp_nat_pr5047031295181774490ux_rel,type,
    nat_pr5047031295181774490ux_rel: product_prod_nat_nat > product_prod_nat_nat > $o ).

thf(tp_nat_prod_decode,type,
    nat_prod_decode: nat > product_prod_nat_nat ).

thf(tp_nat_prod_decode_aux,type,
    nat_prod_decode_aux: nat > nat > product_prod_nat_nat ).

thf(tp_nat_prod_encode,type,
    nat_prod_encode: product_prod_nat_nat > nat ).

thf(tp_nat_set_decode,type,
    nat_set_decode: nat > set_nat ).

thf(tp_nat_set_encode,type,
    nat_set_encode: set_nat > nat ).

thf(tp_nat_triangle,type,
    nat_triangle: nat > nat ).

thf(tp_nil_int,type,
    nil_int: list_int ).

thf(tp_nil_nat,type,
    nil_nat: list_nat ).

thf(tp_none_Extended_enat,type,
    none_Extended_enat: option_Extended_enat ).

thf(tp_none_P5556105721700978146at_nat,type,
    none_P5556105721700978146at_nat: option4927543243414619207at_nat ).

thf(tp_none_VEBT_VEBT,type,
    none_VEBT_VEBT: option_VEBT_VEBT ).

thf(tp_none_int,type,
    none_int: option_int ).

thf(tp_none_nat,type,
    none_nat: option_nat ).

thf(tp_none_num,type,
    none_num: option_num ).

thf(tp_none_real,type,
    none_real: option_real ).

thf(tp_none_set_nat,type,
    none_set_nat: option_set_nat ).

thf(tp_nth_Extended_enat,type,
    nth_Extended_enat: list_Extended_enat > nat > extended_enat ).

thf(tp_nth_Pr1791586995822124652BT_nat,type,
    nth_Pr1791586995822124652BT_nat: list_P7037539587688870467BT_nat > nat > produc9072475918466114483BT_nat ).

thf(tp_nth_Pr3440142176431000676at_int,type,
    nth_Pr3440142176431000676at_int: list_P3521021558325789923at_int > nat > product_prod_nat_int ).

thf(tp_nth_Pr3474266648193625910T_VEBT,type,
    nth_Pr3474266648193625910T_VEBT: list_P7524865323317820941T_VEBT > nat > produc1531783533982839933T_VEBT ).

thf(tp_nth_Pr4439495888332055232nt_int,type,
    nth_Pr4439495888332055232nt_int: list_P5707943133018811711nt_int > nat > product_prod_int_int ).

thf(tp_nth_Pr4953567300277697838T_VEBT,type,
    nth_Pr4953567300277697838T_VEBT: list_P7413028617227757229T_VEBT > nat > produc8243902056947475879T_VEBT ).

thf(tp_nth_Pr6744343527793145070at_nat,type,
    nth_Pr6744343527793145070at_nat: list_P8469869581646625389at_nat > nat > produc859450856879609959at_nat ).

thf(tp_nth_Pr6837108013167703752BT_int,type,
    nth_Pr6837108013167703752BT_int: list_P4547456442757143711BT_int > nat > produc4894624898956917775BT_int ).

thf(tp_nth_Pr744662078594809490T_VEBT,type,
    nth_Pr744662078594809490T_VEBT: list_P5647936690300460905T_VEBT > nat > produc8025551001238799321T_VEBT ).

thf(tp_nth_Pr7617993195940197384at_nat,type,
    nth_Pr7617993195940197384at_nat: list_P6011104703257516679at_nat > nat > product_prod_nat_nat ).

thf(tp_nth_Pr8617346907841251940nt_nat,type,
    nth_Pr8617346907841251940nt_nat: list_P8198026277950538467nt_nat > nat > product_prod_int_nat ).

thf(tp_nth_VEBT_VEBT,type,
    nth_VEBT_VEBT: list_VEBT_VEBT > nat > vEBT_VEBT ).

thf(tp_nth_int,type,
    nth_int: list_int > nat > int ).

thf(tp_nth_nat,type,
    nth_nat: list_nat > nat > nat ).

thf(tp_nth_num,type,
    nth_num: list_num > nat > num ).

thf(tp_nth_real,type,
    nth_real: list_real > nat > real ).

thf(tp_nth_set_nat,type,
    nth_set_nat: list_set_nat > nat > set_nat ).

thf(tp_num_of_nat,type,
    num_of_nat: nat > num ).

thf(tp_numera1916890842035813515d_enat,type,
    numera1916890842035813515d_enat: num > extended_enat ).

thf(tp_numera6690914467698888265omplex,type,
    numera6690914467698888265omplex: num > complex ).

thf(tp_numeral_numeral_int,type,
    numeral_numeral_int: num > int ).

thf(tp_numeral_numeral_nat,type,
    numeral_numeral_nat: num > nat ).

thf(tp_numeral_numeral_real,type,
    numeral_numeral_real: num > real ).

thf(tp_one,type,
    one: num ).

thf(tp_one_on7984719198319812577d_enat,type,
    one_on7984719198319812577d_enat: extended_enat ).

thf(tp_one_one_complex,type,
    one_one_complex: complex ).

thf(tp_one_one_int,type,
    one_one_int: int ).

thf(tp_one_one_nat,type,
    one_one_nat: nat ).

thf(tp_one_one_real,type,
    one_one_real: real ).

thf(tp_ord_Le1955565732374568822d_enat,type,
    ord_Le1955565732374568822d_enat: ( extended_enat > $o ) > extended_enat ).

thf(tp_ord_Least_nat,type,
    ord_Least_nat: ( nat > $o ) > nat ).

thf(tp_ord_le100613205991271927enat_o,type,
    ord_le100613205991271927enat_o: ( extended_enat > $o ) > ( extended_enat > $o ) > $o ).

thf(tp_ord_le211207098394363844omplex,type,
    ord_le211207098394363844omplex: set_complex > set_complex > $o ).

thf(tp_ord_le2510731241096832064er_nat,type,
    ord_le2510731241096832064er_nat: filter_nat > filter_nat > $o ).

thf(tp_ord_le2529575680413868914d_enat,type,
    ord_le2529575680413868914d_enat: set_Extended_enat > set_Extended_enat > $o ).

thf(tp_ord_le2932123472753598470d_enat,type,
    ord_le2932123472753598470d_enat: extended_enat > extended_enat > $o ).

thf(tp_ord_le3964352015994296041_nat_o,type,
    ord_le3964352015994296041_nat_o: ( set_nat > $o ) > ( set_nat > $o ) > $o ).

thf(tp_ord_le4337996190870823476T_VEBT,type,
    ord_le4337996190870823476T_VEBT: set_VEBT_VEBT > set_VEBT_VEBT > $o ).

thf(tp_ord_le4403425263959731960et_int,type,
    ord_le4403425263959731960et_int: set_set_int > set_set_int > $o ).

thf(tp_ord_le6045566169113846134st_nat,type,
    ord_le6045566169113846134st_nat: set_list_nat > set_list_nat > $o ).

thf(tp_ord_le6893508408891458716et_nat,type,
    ord_le6893508408891458716et_nat: set_set_nat > set_set_nat > $o ).

thf(tp_ord_le7203529160286727270d_enat,type,
    ord_le7203529160286727270d_enat: set_Extended_enat > set_Extended_enat > $o ).

thf(tp_ord_le72135733267957522d_enat,type,
    ord_le72135733267957522d_enat: extended_enat > extended_enat > $o ).

thf(tp_ord_le8499522857272258027enat_o,type,
    ord_le8499522857272258027enat_o: ( extended_enat > $o ) > ( extended_enat > $o ) > $o ).

thf(tp_ord_less_eq_int,type,
    ord_less_eq_int: int > int > $o ).

thf(tp_ord_less_eq_int_o,type,
    ord_less_eq_int_o: ( int > $o ) > ( int > $o ) > $o ).

thf(tp_ord_less_eq_nat,type,
    ord_less_eq_nat: nat > nat > $o ).

thf(tp_ord_less_eq_nat_o,type,
    ord_less_eq_nat_o: ( nat > $o ) > ( nat > $o ) > $o ).

thf(tp_ord_less_eq_num,type,
    ord_less_eq_num: num > num > $o ).

thf(tp_ord_less_eq_real,type,
    ord_less_eq_real: real > real > $o ).

thf(tp_ord_less_eq_real_o,type,
    ord_less_eq_real_o: ( real > $o ) > ( real > $o ) > $o ).

thf(tp_ord_less_eq_set_int,type,
    ord_less_eq_set_int: set_int > set_int > $o ).

thf(tp_ord_less_eq_set_nat,type,
    ord_less_eq_set_nat: set_nat > set_nat > $o ).

thf(tp_ord_less_eq_set_real,type,
    ord_less_eq_set_real: set_real > set_real > $o ).

thf(tp_ord_less_int,type,
    ord_less_int: int > int > $o ).

thf(tp_ord_less_int_o,type,
    ord_less_int_o: ( int > $o ) > ( int > $o ) > $o ).

thf(tp_ord_less_nat,type,
    ord_less_nat: nat > nat > $o ).

thf(tp_ord_less_nat_o,type,
    ord_less_nat_o: ( nat > $o ) > ( nat > $o ) > $o ).

thf(tp_ord_less_num,type,
    ord_less_num: num > num > $o ).

thf(tp_ord_less_real,type,
    ord_less_real: real > real > $o ).

thf(tp_ord_less_real_o,type,
    ord_less_real_o: ( real > $o ) > ( real > $o ) > $o ).

thf(tp_ord_less_set_complex,type,
    ord_less_set_complex: set_complex > set_complex > $o ).

thf(tp_ord_less_set_int,type,
    ord_less_set_int: set_int > set_int > $o ).

thf(tp_ord_less_set_nat,type,
    ord_less_set_nat: set_nat > set_nat > $o ).

thf(tp_ord_less_set_nat_o,type,
    ord_less_set_nat_o: ( set_nat > $o ) > ( set_nat > $o ) > $o ).

thf(tp_ord_less_set_real,type,
    ord_less_set_real: set_real > set_real > $o ).

thf(tp_ord_less_set_set_int,type,
    ord_less_set_set_int: set_set_int > set_set_int > $o ).

thf(tp_ord_less_set_set_nat,type,
    ord_less_set_set_nat: set_set_nat > set_set_nat > $o ).

thf(tp_ord_ma4205026669011143323d_enat,type,
    ord_ma4205026669011143323d_enat: set_Extended_enat > set_Extended_enat > set_Extended_enat ).

thf(tp_ord_ma741700101516333627d_enat,type,
    ord_ma741700101516333627d_enat: extended_enat > extended_enat > extended_enat ).

thf(tp_ord_max_int,type,
    ord_max_int: int > int > int ).

thf(tp_ord_max_nat,type,
    ord_max_nat: nat > nat > nat ).

thf(tp_ord_max_real,type,
    ord_max_real: real > real > real ).

thf(tp_ord_max_set_int,type,
    ord_max_set_int: set_int > set_int > set_int ).

thf(tp_ord_max_set_nat,type,
    ord_max_set_nat: set_nat > set_nat > set_nat ).

thf(tp_ord_max_set_real,type,
    ord_max_set_real: set_real > set_real > set_real ).

thf(tp_ord_min_int,type,
    ord_min_int: int > int > int ).

thf(tp_ord_min_nat,type,
    ord_min_nat: nat > nat > nat ).

thf(tp_order_2888998067076097458on_nat,type,
    order_2888998067076097458on_nat: set_nat > set_Pr1261947904930325089at_nat > $o ).

thf(tp_order_5726023648592871131at_nat,type,
    order_5726023648592871131at_nat: ( nat > nat ) > $o ).

thf(tp_order_Greatest_nat,type,
    order_Greatest_nat: ( nat > $o ) > nat ).

thf(tp_order_mono_nat_nat,type,
    order_mono_nat_nat: ( nat > nat ) > $o ).

thf(tp_order_underS_nat,type,
    order_underS_nat: set_Pr1261947904930325089at_nat > nat > set_nat ).

thf(tp_ordering_top_nat,type,
    ordering_top_nat: ( nat > nat > $o ) > ( nat > nat > $o ) > nat > $o ).

thf(tp_pcr_int,type,
    pcr_int: product_prod_nat_nat > int > $o ).

thf(tp_pi,type,
    pi: real ).

thf(tp_plus_p3455044024723400733d_enat,type,
    plus_p3455044024723400733d_enat: extended_enat > extended_enat > extended_enat ).

thf(tp_plus_plus_complex,type,
    plus_plus_complex: complex > complex > complex ).

thf(tp_plus_plus_int,type,
    plus_plus_int: int > int > int ).

thf(tp_plus_plus_nat,type,
    plus_plus_nat: nat > nat > nat ).

thf(tp_plus_plus_num,type,
    plus_plus_num: num > num > num ).

thf(tp_plus_plus_real,type,
    plus_plus_real: real > real > real ).

thf(tp_pow_nat,type,
    pow_nat: set_nat > set_set_nat ).

thf(tp_power_8040749407984259932d_enat,type,
    power_8040749407984259932d_enat: extended_enat > nat > extended_enat ).

thf(tp_power_power_complex,type,
    power_power_complex: complex > nat > complex ).

thf(tp_power_power_int,type,
    power_power_int: int > nat > int ).

thf(tp_power_power_nat,type,
    power_power_nat: nat > nat > nat ).

thf(tp_power_power_real,type,
    power_power_real: real > nat > real ).

thf(tp_powr_real,type,
    powr_real: real > real > real ).

thf(tp_pred,type,
    pred: nat > nat ).

thf(tp_pred_nat,type,
    pred_nat: set_Pr1261947904930325089at_nat ).

thf(tp_pred_numeral,type,
    pred_numeral: num > nat ).

thf(tp_prod_filter_nat_nat,type,
    prod_filter_nat_nat: filter_nat > filter_nat > filter1242075044329608583at_nat ).

thf(tp_produc1703576794950452218t_real,type,
    produc1703576794950452218t_real: ( nat > nat > real ) > product_prod_nat_nat > real ).

thf(tp_produc1917071388513777916omplex,type,
    produc1917071388513777916omplex: ( nat > nat > complex ) > product_prod_nat_nat > complex ).

thf(tp_produc2626176000494625587at_nat,type,
    produc2626176000494625587at_nat: ( nat > nat > product_prod_nat_nat ) > product_prod_nat_nat > product_prod_nat_nat ).

thf(tp_produc2676513652042109336d_enat,type,
    produc2676513652042109336d_enat: ( nat > nat > extended_enat ) > product_prod_nat_nat > extended_enat ).

thf(tp_produc2694037385005941721st_nat,type,
    produc2694037385005941721st_nat: list_nat > list_nat > produc1828647624359046049st_nat ).

thf(tp_produc27273713700761075at_nat,type,
    produc27273713700761075at_nat: ( nat > nat > product_prod_nat_nat > product_prod_nat_nat ) > product_prod_nat_nat > product_prod_nat_nat > product_prod_nat_nat ).

thf(tp_produc2761476792215241774st_nat,type,
    produc2761476792215241774st_nat: ( nat > nat > list_nat ) > product_prod_nat_nat > list_nat ).

thf(tp_produc3209952032786966637at_nat,type,
    produc3209952032786966637at_nat: ( nat > nat > nat ) > produc7248412053542808358at_nat > produc4471711990508489141at_nat ).

thf(tp_produc3329399203697025711T_VEBT,type,
    produc3329399203697025711T_VEBT: int > vEBT_VEBT > produc1531783533982839933T_VEBT ).

thf(tp_produc3544356994491977349at_nat,type,
    produc3544356994491977349at_nat: list_P6011104703257516679at_nat > list_P6011104703257516679at_nat > list_P8469869581646625389at_nat ).

thf(tp_produc364263696895485585st_int,type,
    produc364263696895485585st_int: list_int > list_int > produc1186641810826059865st_int ).

thf(tp_produc3897820843166775703T_VEBT,type,
    produc3897820843166775703T_VEBT: list_VEBT_VEBT > list_VEBT_VEBT > produc9211091688327510695T_VEBT ).

thf(tp_produc4245557441103728435nt_int,type,
    produc4245557441103728435nt_int: ( int > int > product_prod_int_int ) > product_prod_int_int > product_prod_int_int ).

thf(tp_produc457027306803732586at_nat,type,
    produc457027306803732586at_nat: set_nat > ( nat > set_nat ) > set_Pr1261947904930325089at_nat ).

thf(tp_produc4743750530478302277T_VEBT,type,
    produc4743750530478302277T_VEBT: list_VEBT_VEBT > list_VEBT_VEBT > list_P7413028617227757229T_VEBT ).

thf(tp_produc487386426758144856at_nat,type,
    produc487386426758144856at_nat: nat > product_prod_nat_nat > produc7248412053542808358at_nat ).

thf(tp_produc4947309494688390418_int_o,type,
    produc4947309494688390418_int_o: ( int > int > $o ) > product_prod_int_int > $o ).

thf(tp_produc537772716801021591T_VEBT,type,
    produc537772716801021591T_VEBT: vEBT_VEBT > vEBT_VEBT > produc8243902056947475879T_VEBT ).

thf(tp_produc5943733680697469783at_nat,type,
    produc5943733680697469783at_nat: list_P6011104703257516679at_nat > list_P6011104703257516679at_nat > produc6392793444374437607at_nat ).

thf(tp_produc599794634098209291T_VEBT,type,
    produc599794634098209291T_VEBT: nat > vEBT_VEBT > produc8025551001238799321T_VEBT ).

thf(tp_produc6081775807080527818_nat_o,type,
    produc6081775807080527818_nat_o: ( nat > nat > $o ) > product_prod_nat_nat > $o ).

thf(tp_produc6161850002892822231at_nat,type,
    produc6161850002892822231at_nat: product_prod_nat_nat > product_prod_nat_nat > produc859450856879609959at_nat ).

thf(tp_produc662631939642741121T_VEBT,type,
    produc662631939642741121T_VEBT: list_int > list_VEBT_VEBT > list_P7524865323317820941T_VEBT ).

thf(tp_produc6840382203811409530at_int,type,
    produc6840382203811409530at_int: ( nat > nat > int ) > product_prod_nat_nat > int ).

thf(tp_produc6842872674320459806at_nat,type,
    produc6842872674320459806at_nat: ( nat > nat > nat ) > product_prod_nat_nat > nat ).

thf(tp_produc7156399406898700509T_VEBT,type,
    produc7156399406898700509T_VEBT: list_nat > list_VEBT_VEBT > list_P5647936690300460905T_VEBT ).

thf(tp_produc7292646706713671643BT_int,type,
    produc7292646706713671643BT_int: list_VEBT_VEBT > list_int > list_P4547456442757143711BT_int ).

thf(tp_produc7295137177222721919BT_nat,type,
    produc7295137177222721919BT_nat: list_VEBT_VEBT > list_nat > list_P7037539587688870467BT_nat ).

thf(tp_produc736041933913180425BT_int,type,
    produc736041933913180425BT_int: vEBT_VEBT > int > produc4894624898956917775BT_int ).

thf(tp_produc738532404422230701BT_nat,type,
    produc738532404422230701BT_nat: vEBT_VEBT > nat > produc9072475918466114483BT_nat ).

thf(tp_produc8739625826339149834_nat_o,type,
    produc8739625826339149834_nat_o: ( nat > nat > product_prod_nat_nat > $o ) > product_prod_nat_nat > product_prod_nat_nat > $o ).

thf(tp_product_Pair_int_int,type,
    product_Pair_int_int: int > int > product_prod_int_int ).

thf(tp_product_Pair_int_nat,type,
    product_Pair_int_nat: int > nat > product_prod_int_nat ).

thf(tp_product_Pair_nat_int,type,
    product_Pair_nat_int: nat > int > product_prod_nat_int ).

thf(tp_product_Pair_nat_nat,type,
    product_Pair_nat_nat: nat > nat > product_prod_nat_nat ).

thf(tp_product_fst_int_int,type,
    product_fst_int_int: product_prod_int_int > int ).

thf(tp_product_fst_nat_nat,type,
    product_fst_nat_nat: product_prod_nat_nat > nat ).

thf(tp_product_int_int,type,
    product_int_int: list_int > list_int > list_P5707943133018811711nt_int ).

thf(tp_product_int_nat,type,
    product_int_nat: list_int > list_nat > list_P8198026277950538467nt_nat ).

thf(tp_product_nat_int,type,
    product_nat_int: list_nat > list_int > list_P3521021558325789923at_int ).

thf(tp_product_nat_nat,type,
    product_nat_nat: list_nat > list_nat > list_P6011104703257516679at_nat ).

thf(tp_product_snd_int_int,type,
    product_snd_int_int: product_prod_int_int > int ).

thf(tp_product_snd_nat_nat,type,
    product_snd_nat_nat: product_prod_nat_nat > nat ).

thf(tp_real_V1022390504157884413omplex,type,
    real_V1022390504157884413omplex: complex > real ).

thf(tp_real_V1485227260804924795R_real,type,
    real_V1485227260804924795R_real: real > real > real ).

thf(tp_real_V1803761363581548252l_real,type,
    real_V1803761363581548252l_real: real > real ).

thf(tp_real_V2046097035970521341omplex,type,
    real_V2046097035970521341omplex: real > complex > complex ).

thf(tp_real_V4546457046886955230omplex,type,
    real_V4546457046886955230omplex: real > complex ).

thf(tp_real_V7735802525324610683m_real,type,
    real_V7735802525324610683m_real: real > real ).

thf(tp_remdups_nat,type,
    remdups_nat: list_nat > list_nat ).

thf(tp_rep_Integ,type,
    rep_Integ: int > product_prod_nat_nat ).

thf(tp_replic7216382294607269926d_enat,type,
    replic7216382294607269926d_enat: nat > extended_enat > list_Extended_enat ).

thf(tp_replicate_VEBT_VEBT,type,
    replicate_VEBT_VEBT: nat > vEBT_VEBT > list_VEBT_VEBT ).

thf(tp_replicate_int,type,
    replicate_int: nat > int > list_int ).

thf(tp_replicate_nat,type,
    replicate_nat: nat > nat > list_nat ).

thf(tp_replicate_real,type,
    replicate_real: nat > real > list_real ).

thf(tp_replicate_set_nat,type,
    replicate_set_nat: nat > set_nat > list_set_nat ).

thf(tp_ring_17405671764205052669omplex,type,
    ring_17405671764205052669omplex: int > complex ).

thf(tp_ring_1_of_int_int,type,
    ring_1_of_int_int: int > int ).

thf(tp_ring_1_of_int_real,type,
    ring_1_of_int_real: int > real ).

thf(tp_root,type,
    root: nat > real > real ).

thf(tp_semila1623282765462674594er_nat,type,
    semila1623282765462674594er_nat: ( nat > nat > nat ) > nat > ( nat > nat > $o ) > ( nat > nat > $o ) > $o ).

thf(tp_semiri1314217659103216013at_int,type,
    semiri1314217659103216013at_int: nat > int ).

thf(tp_semiri1316708129612266289at_nat,type,
    semiri1316708129612266289at_nat: nat > nat ).

thf(tp_semiri1406184849735516958ct_int,type,
    semiri1406184849735516958ct_int: nat > int ).

thf(tp_semiri1408675320244567234ct_nat,type,
    semiri1408675320244567234ct_nat: nat > nat ).

thf(tp_semiri2265585572941072030t_real,type,
    semiri2265585572941072030t_real: nat > real ).

thf(tp_semiri2816024913162550771omplex,type,
    semiri2816024913162550771omplex: ( complex > complex ) > nat > complex > complex ).

thf(tp_semiri4216267220026989637d_enat,type,
    semiri4216267220026989637d_enat: nat > extended_enat ).

thf(tp_semiri4449623510593786356d_enat,type,
    semiri4449623510593786356d_enat: nat > extended_enat ).

thf(tp_semiri5044797733671781792omplex,type,
    semiri5044797733671781792omplex: nat > complex ).

thf(tp_semiri5074537144036343181t_real,type,
    semiri5074537144036343181t_real: nat > real ).

thf(tp_semiri7260567687927622513x_real,type,
    semiri7260567687927622513x_real: ( real > real ) > nat > real > real ).

thf(tp_semiri8010041392384452111omplex,type,
    semiri8010041392384452111omplex: nat > complex ).

thf(tp_semiri8420488043553186161ux_int,type,
    semiri8420488043553186161ux_int: ( int > int ) > nat > int > int ).

thf(tp_semiri8422978514062236437ux_nat,type,
    semiri8422978514062236437ux_nat: ( nat > nat ) > nat > nat > nat ).

thf(tp_semiri8563196900006977889d_enat,type,
    semiri8563196900006977889d_enat: ( extended_enat > extended_enat ) > nat > extended_enat > extended_enat ).

thf(tp_semiring_1_Nats_int,type,
    semiring_1_Nats_int: set_int ).

thf(tp_set_Extended_enat2,type,
    set_Extended_enat2: list_Extended_enat > set_Extended_enat ).

thf(tp_set_Pr5648618587558075414at_nat,type,
    set_Pr5648618587558075414at_nat: list_P6011104703257516679at_nat > set_Pr1261947904930325089at_nat ).

thf(tp_set_VEBT_VEBT2,type,
    set_VEBT_VEBT2: list_VEBT_VEBT > set_VEBT_VEBT ).

thf(tp_set_complex2,type,
    set_complex2: list_complex > set_complex ).

thf(tp_set_fo1517530859248394432omplex,type,
    set_fo1517530859248394432omplex: ( nat > complex > complex ) > nat > nat > complex > complex ).

thf(tp_set_fo2538466533108834004d_enat,type,
    set_fo2538466533108834004d_enat: ( nat > extended_enat > extended_enat ) > nat > nat > extended_enat > extended_enat ).

thf(tp_set_fo2581907887559384638at_int,type,
    set_fo2581907887559384638at_int: ( nat > int > int ) > nat > nat > int > int ).

thf(tp_set_fo2584398358068434914at_nat,type,
    set_fo2584398358068434914at_nat: ( nat > nat > nat ) > nat > nat > nat > nat ).

thf(tp_set_fo3111899725591712190t_real,type,
    set_fo3111899725591712190t_real: ( nat > real > real ) > nat > nat > real > real ).

thf(tp_set_int2,type,
    set_int2: list_int > set_int ).

thf(tp_set_nat2,type,
    set_nat2: list_nat > set_nat ).

thf(tp_set_num2,type,
    set_num2: list_num > set_num ).

thf(tp_set_or1210151606488870762an_nat,type,
    set_or1210151606488870762an_nat: nat > set_nat ).

thf(tp_set_or1222579329274155063t_real,type,
    set_or1222579329274155063t_real: real > real > set_real ).

thf(tp_set_or1266510415728281911st_int,type,
    set_or1266510415728281911st_int: int > int > set_int ).

thf(tp_set_or1269000886237332187st_nat,type,
    set_or1269000886237332187st_nat: nat > nat > set_nat ).

thf(tp_set_or1633881224788618240n_real,type,
    set_or1633881224788618240n_real: real > real > set_real ).

thf(tp_set_or370866239135849197et_int,type,
    set_or370866239135849197et_int: set_int > set_int > set_set_int ).

thf(tp_set_or4236626031148496127et_nat,type,
    set_or4236626031148496127et_nat: set_nat > set_set_nat ).

thf(tp_set_or4548717258645045905et_nat,type,
    set_or4548717258645045905et_nat: set_nat > set_nat > set_set_nat ).

thf(tp_set_or4662586982721622107an_int,type,
    set_or4662586982721622107an_int: int > int > set_int ).

thf(tp_set_or4665077453230672383an_nat,type,
    set_or4665077453230672383an_nat: nat > nat > set_nat ).

thf(tp_set_or5403411693681687835d_enat,type,
    set_or5403411693681687835d_enat: extended_enat > extended_enat > set_Extended_enat ).

thf(tp_set_or5832277885323065728an_int,type,
    set_or5832277885323065728an_int: int > int > set_int ).

thf(tp_set_or5834768355832116004an_nat,type,
    set_or5834768355832116004an_nat: nat > nat > set_nat ).

thf(tp_set_or58775011639299419et_int,type,
    set_or58775011639299419et_int: set_int > set_set_int ).

thf(tp_set_or5984915006950818249n_real,type,
    set_or5984915006950818249n_real: real > set_real ).

thf(tp_set_or6656581121297822940st_int,type,
    set_or6656581121297822940st_int: int > int > set_int ).

thf(tp_set_or6659071591806873216st_nat,type,
    set_or6659071591806873216st_nat: nat > nat > set_nat ).

thf(tp_set_or8332593352340944941d_enat,type,
    set_or8332593352340944941d_enat: extended_enat > set_Extended_enat ).

thf(tp_set_or8419480210114673929d_enat,type,
    set_or8419480210114673929d_enat: extended_enat > set_Extended_enat ).

thf(tp_set_or890127255671739683et_nat,type,
    set_or890127255671739683et_nat: set_nat > set_set_nat ).

thf(tp_set_ord_atLeast_nat,type,
    set_ord_atLeast_nat: nat > set_nat ).

thf(tp_set_ord_atMost_int,type,
    set_ord_atMost_int: int > set_int ).

thf(tp_set_ord_atMost_nat,type,
    set_ord_atMost_nat: nat > set_nat ).

thf(tp_set_ord_atMost_real,type,
    set_ord_atMost_real: real > set_real ).

thf(tp_set_ord_lessThan_int,type,
    set_ord_lessThan_int: int > set_int ).

thf(tp_set_ord_lessThan_nat,type,
    set_ord_lessThan_nat: nat > set_nat ).

thf(tp_set_real2,type,
    set_real2: list_real > set_real ).

thf(tp_set_set_nat2,type,
    set_set_nat2: list_set_nat > set_set_nat ).

thf(tp_sgn_sgn_complex,type,
    sgn_sgn_complex: complex > complex ).

thf(tp_sgn_sgn_int,type,
    sgn_sgn_int: int > int ).

thf(tp_sgn_sgn_real,type,
    sgn_sgn_real: real > real ).

thf(tp_sin_coeff,type,
    sin_coeff: nat > real ).

thf(tp_sin_complex,type,
    sin_complex: complex > complex ).

thf(tp_sin_real,type,
    sin_real: real > real ).

thf(tp_size_list_VEBT_VEBT,type,
    size_list_VEBT_VEBT: ( vEBT_VEBT > nat ) > list_VEBT_VEBT > nat ).

thf(tp_size_num,type,
    size_num: num > nat ).

thf(tp_size_o8335143837870341156at_nat,type,
    size_o8335143837870341156at_nat: ( product_prod_nat_nat > nat ) > option4927543243414619207at_nat > nat ).

thf(tp_size_option_num,type,
    size_option_num: ( num > nat ) > option_num > nat ).

thf(tp_size_s170228958280169651at_nat,type,
    size_s170228958280169651at_nat: option4927543243414619207at_nat > nat ).

thf(tp_size_s2970893825323803983at_int,type,
    size_s2970893825323803983at_int: list_P3521021558325789923at_int > nat ).

thf(tp_size_s3254054031482475050et_nat,type,
    size_s3254054031482475050et_nat: list_set_nat > nat ).

thf(tp_size_s3451745648224563538omplex,type,
    size_s3451745648224563538omplex: list_complex > nat ).

thf(tp_size_s3661962791536183091BT_int,type,
    size_s3661962791536183091BT_int: list_P4547456442757143711BT_int > nat ).

thf(tp_size_s3941691890525107288d_enat,type,
    size_s3941691890525107288d_enat: list_Extended_enat > nat ).

thf(tp_size_s4762443039079500285T_VEBT,type,
    size_s4762443039079500285T_VEBT: list_P5647936690300460905T_VEBT > nat ).

thf(tp_size_s5157815400016825771nt_int,type,
    size_s5157815400016825771nt_int: list_P5707943133018811711nt_int > nat ).

thf(tp_size_s5460976970255530739at_nat,type,
    size_s5460976970255530739at_nat: list_P6011104703257516679at_nat > nat ).

thf(tp_size_s6152045936467909847BT_nat,type,
    size_s6152045936467909847BT_nat: list_P7037539587688870467BT_nat > nat ).

thf(tp_size_s6639371672096860321T_VEBT,type,
    size_s6639371672096860321T_VEBT: list_P7524865323317820941T_VEBT > nat ).

thf(tp_size_s6755466524823107622T_VEBT,type,
    size_s6755466524823107622T_VEBT: list_VEBT_VEBT > nat ).

thf(tp_size_s7466405169056248089T_VEBT,type,
    size_s7466405169056248089T_VEBT: list_P7413028617227757229T_VEBT > nat ).

thf(tp_size_s7647898544948552527nt_nat,type,
    size_s7647898544948552527nt_nat: list_P8198026277950538467nt_nat > nat ).

thf(tp_size_size_VEBT_VEBT,type,
    size_size_VEBT_VEBT: vEBT_VEBT > nat ).

thf(tp_size_size_list_int,type,
    size_size_list_int: list_int > nat ).

thf(tp_size_size_list_nat,type,
    size_size_list_nat: list_nat > nat ).

thf(tp_size_size_list_num,type,
    size_size_list_num: list_num > nat ).

thf(tp_size_size_list_real,type,
    size_size_list_real: list_real > nat ).

thf(tp_size_size_num,type,
    size_size_num: num > nat ).

thf(tp_size_size_option_num,type,
    size_size_option_num: option_num > nat ).

thf(tp_some_P7363390416028606310at_nat,type,
    some_P7363390416028606310at_nat: product_prod_nat_nat > option4927543243414619207at_nat ).

thf(tp_some_VEBT_VEBT,type,
    some_VEBT_VEBT: vEBT_VEBT > option_VEBT_VEBT ).

thf(tp_some_int,type,
    some_int: int > option_int ).

thf(tp_some_nat,type,
    some_nat: nat > option_nat ).

thf(tp_some_num,type,
    some_num: num > option_num ).

thf(tp_sorted_wrt_int,type,
    sorted_wrt_int: ( int > int > $o ) > list_int > $o ).

thf(tp_sorted_wrt_nat,type,
    sorted_wrt_nat: ( nat > nat > $o ) > list_nat > $o ).

thf(tp_strict1292158309912662752at_nat,type,
    strict1292158309912662752at_nat: ( nat > nat ) > set_nat > $o ).

thf(tp_suc,type,
    suc: nat > nat ).

thf(tp_suminf_complex,type,
    suminf_complex: ( nat > complex ) > complex ).

thf(tp_suminf_int,type,
    suminf_int: ( nat > int ) > int ).

thf(tp_suminf_nat,type,
    suminf_nat: ( nat > nat ) > nat ).

thf(tp_suminf_real,type,
    suminf_real: ( nat > real ) > real ).

thf(tp_summable_complex,type,
    summable_complex: ( nat > complex ) > $o ).

thf(tp_summable_int,type,
    summable_int: ( nat > int ) > $o ).

thf(tp_summable_nat,type,
    summable_nat: ( nat > nat ) > $o ).

thf(tp_summable_real,type,
    summable_real: ( nat > real ) > $o ).

thf(tp_summary,type,
    summary: vEBT_VEBT ).

thf(tp_sums_complex,type,
    sums_complex: ( nat > complex ) > complex > $o ).

thf(tp_sums_int,type,
    sums_int: ( nat > int ) > int > $o ).

thf(tp_sums_nat,type,
    sums_nat: ( nat > nat ) > nat > $o ).

thf(tp_sums_real,type,
    sums_real: ( nat > real ) > real > $o ).

thf(tp_sup_sup_int,type,
    sup_sup_int: int > int > int ).

thf(tp_sup_sup_nat,type,
    sup_sup_nat: nat > nat > nat ).

thf(tp_sup_sup_set_nat,type,
    sup_sup_set_nat: set_nat > set_nat > set_nat ).

thf(tp_take_nat,type,
    take_nat: nat > list_nat > list_nat ).

thf(tp_tan_complex,type,
    tan_complex: complex > complex ).

thf(tp_tan_real,type,
    tan_real: real > real ).

thf(tp_the_in5290026491893676941l_real,type,
    the_in5290026491893676941l_real: set_real > ( real > real ) > real > real ).

thf(tp_times_7803423173614009249d_enat,type,
    times_7803423173614009249d_enat: extended_enat > extended_enat > extended_enat ).

thf(tp_times_times_complex,type,
    times_times_complex: complex > complex > complex ).

thf(tp_times_times_int,type,
    times_times_int: int > int > int ).

thf(tp_times_times_nat,type,
    times_times_nat: nat > nat > nat ).

thf(tp_times_times_real,type,
    times_times_real: real > real > real ).

thf(tp_tl_nat,type,
    tl_nat: list_nat > list_nat ).

thf(tp_top_to1996260823553986621t_unit,type,
    top_to1996260823553986621t_unit: set_Product_unit ).

thf(tp_top_top_set_char,type,
    top_top_set_char: set_char ).

thf(tp_top_top_set_int,type,
    top_top_set_int: set_int ).

thf(tp_top_top_set_nat,type,
    top_top_set_nat: set_nat ).

thf(tp_top_top_set_real,type,
    top_top_set_real: set_real ).

thf(tp_topolo2177554685111907308n_real,type,
    topolo2177554685111907308n_real: real > set_real > filter_real ).

thf(tp_topolo2815343760600316023s_real,type,
    topolo2815343760600316023s_real: real > filter_real ).

thf(tp_topolo4055970368930404560y_real,type,
    topolo4055970368930404560y_real: ( nat > real ) > $o ).

thf(tp_topolo6980174941875973593q_real,type,
    topolo6980174941875973593q_real: ( nat > real ) > $o ).

thf(tp_transi2905341329935302413cl_nat,type,
    transi2905341329935302413cl_nat: set_Pr1261947904930325089at_nat > set_Pr1261947904930325089at_nat ).

thf(tp_transi6264000038957366511cl_nat,type,
    transi6264000038957366511cl_nat: set_Pr1261947904930325089at_nat > set_Pr1261947904930325089at_nat ).

thf(tp_treeList,type,
    treeList: list_VEBT_VEBT ).

thf(tp_uminus1482373934393186551omplex,type,
    uminus1482373934393186551omplex: complex > complex ).

thf(tp_uminus1532241313380277803et_int,type,
    uminus1532241313380277803et_int: set_int > set_int ).

thf(tp_uminus3195874150345416415st_nat,type,
    uminus3195874150345416415st_nat: set_list_nat > set_list_nat ).

thf(tp_uminus417252749190364093d_enat,type,
    uminus417252749190364093d_enat: set_Extended_enat > set_Extended_enat ).

thf(tp_uminus5710092332889474511et_nat,type,
    uminus5710092332889474511et_nat: set_nat > set_nat ).

thf(tp_uminus5770388063884162150_nat_o,type,
    uminus5770388063884162150_nat_o: ( list_nat > $o ) > list_nat > $o ).

thf(tp_uminus612125837232591019t_real,type,
    uminus612125837232591019t_real: set_real > set_real ).

thf(tp_uminus613421341184616069et_nat,type,
    uminus613421341184616069et_nat: set_set_nat > set_set_nat ).

thf(tp_uminus6401447641752708672_nat_o,type,
    uminus6401447641752708672_nat_o: ( set_nat > $o ) > set_nat > $o ).

thf(tp_uminus6636779312473996640enat_o,type,
    uminus6636779312473996640enat_o: ( extended_enat > $o ) > extended_enat > $o ).

thf(tp_uminus_uminus_int,type,
    uminus_uminus_int: int > int ).

thf(tp_uminus_uminus_int_o,type,
    uminus_uminus_int_o: ( int > $o ) > int > $o ).

thf(tp_uminus_uminus_nat_o,type,
    uminus_uminus_nat_o: ( nat > $o ) > nat > $o ).

thf(tp_uminus_uminus_real,type,
    uminus_uminus_real: real > real ).

thf(tp_uminus_uminus_real_o,type,
    uminus_uminus_real_o: ( real > $o ) > real > $o ).

thf(tp_unique3096191561947761185of_nat,type,
    unique3096191561947761185of_nat: nat > char ).

thf(tp_unique5024387138958732305ep_int,type,
    unique5024387138958732305ep_int: num > product_prod_int_int > product_prod_int_int ).

thf(tp_unique5026877609467782581ep_nat,type,
    unique5026877609467782581ep_nat: num > product_prod_nat_nat > product_prod_nat_nat ).

thf(tp_unique5052692396658037445od_int,type,
    unique5052692396658037445od_int: num > num > product_prod_int_int ).

thf(tp_unique5055182867167087721od_nat,type,
    unique5055182867167087721od_nat: num > num > product_prod_nat_nat ).

thf(tp_unique6319869463603278526ux_int,type,
    unique6319869463603278526ux_int: product_prod_int_int > $o ).

thf(tp_unique6322359934112328802ux_nat,type,
    unique6322359934112328802ux_nat: product_prod_nat_nat > $o ).

thf(tp_upt,type,
    upt: nat > nat > list_nat ).

thf(tp_upto,type,
    upto: int > int > list_int ).

thf(tp_upto_aux,type,
    upto_aux: int > int > list_int > list_int ).

thf(tp_upto_rel,type,
    upto_rel: product_prod_int_int > product_prod_int_int > $o ).

thf(tp_vEBT_Leaf,type,
    vEBT_Leaf: $o > $o > vEBT_VEBT ).

thf(tp_vEBT_Node,type,
    vEBT_Node: option4927543243414619207at_nat > nat > list_VEBT_VEBT > vEBT_VEBT > vEBT_VEBT ).

thf(tp_vEBT_V4351362008482014158ma_rel,type,
    vEBT_V4351362008482014158ma_rel: produc9072475918466114483BT_nat > produc9072475918466114483BT_nat > $o ).

thf(tp_vEBT_V5719532721284313246member,type,
    vEBT_V5719532721284313246member: vEBT_VEBT > nat > $o ).

thf(tp_vEBT_V5765760719290551771er_rel,type,
    vEBT_V5765760719290551771er_rel: produc9072475918466114483BT_nat > produc9072475918466114483BT_nat > $o ).

thf(tp_vEBT_V5917875025757280293ildren,type,
    vEBT_V5917875025757280293ildren: nat > list_VEBT_VEBT > nat > $o ).

thf(tp_vEBT_V8194947554948674370ptions,type,
    vEBT_V8194947554948674370ptions: vEBT_VEBT > nat > $o ).

thf(tp_vEBT_VEBT_bit_concat,type,
    vEBT_VEBT_bit_concat: nat > nat > nat > nat ).

thf(tp_vEBT_VEBT_elim_dead,type,
    vEBT_VEBT_elim_dead: vEBT_VEBT > extended_enat > vEBT_VEBT ).

thf(tp_vEBT_VEBT_high,type,
    vEBT_VEBT_high: nat > nat > nat ).

thf(tp_vEBT_VEBT_low,type,
    vEBT_VEBT_low: nat > nat > nat ).

thf(tp_vEBT_VEBT_membermima,type,
    vEBT_VEBT_membermima: vEBT_VEBT > nat > $o ).

thf(tp_vEBT_VEBT_minNull,type,
    vEBT_VEBT_minNull: vEBT_VEBT > $o ).

thf(tp_vEBT_VEBT_set_vebt,type,
    vEBT_VEBT_set_vebt: vEBT_VEBT > set_nat ).

thf(tp_vEBT_VEBT_valid,type,
    vEBT_VEBT_valid: vEBT_VEBT > nat > $o ).

thf(tp_vEBT_VEBT_valid_rel,type,
    vEBT_VEBT_valid_rel: produc9072475918466114483BT_nat > produc9072475918466114483BT_nat > $o ).

thf(tp_vEBT_invar_vebt,type,
    vEBT_invar_vebt: vEBT_VEBT > nat > $o ).

thf(tp_vEBT_set_vebt,type,
    vEBT_set_vebt: vEBT_VEBT > set_nat ).

thf(tp_vEBT_size_VEBT,type,
    vEBT_size_VEBT: vEBT_VEBT > nat ).

thf(tp_vEBT_v4011308405150292612up_rel,type,
    vEBT_v4011308405150292612up_rel: nat > nat > $o ).

thf(tp_vEBT_vebt_buildup,type,
    vEBT_vebt_buildup: nat > vEBT_VEBT ).

thf(tp_vEBT_vebt_insert,type,
    vEBT_vebt_insert: vEBT_VEBT > nat > vEBT_VEBT ).

thf(tp_vEBT_vebt_insert_rel,type,
    vEBT_vebt_insert_rel: produc9072475918466114483BT_nat > produc9072475918466114483BT_nat > $o ).

thf(tp_vEBT_vebt_member,type,
    vEBT_vebt_member: vEBT_VEBT > nat > $o ).

thf(tp_vEBT_vebt_member_rel,type,
    vEBT_vebt_member_rel: produc9072475918466114483BT_nat > produc9072475918466114483BT_nat > $o ).

thf(tp_vimage_nat_nat,type,
    vimage_nat_nat: ( nat > nat ) > set_nat > set_nat ).

thf(tp_wf_int,type,
    wf_int: set_Pr958786334691620121nt_int > $o ).

thf(tp_wf_nat,type,
    wf_nat: set_Pr1261947904930325089at_nat > $o ).

thf(tp_xa,type,
    xa: nat ).

thf(tp_zero_n1046097342994218471d_enat,type,
    zero_n1046097342994218471d_enat: $o > extended_enat ).

thf(tp_zero_n1201886186963655149omplex,type,
    zero_n1201886186963655149omplex: $o > complex ).

thf(tp_zero_n2684676970156552555ol_int,type,
    zero_n2684676970156552555ol_int: $o > int ).

thf(tp_zero_n2687167440665602831ol_nat,type,
    zero_n2687167440665602831ol_nat: $o > nat ).

thf(tp_zero_n3304061248610475627l_real,type,
    zero_n3304061248610475627l_real: $o > real ).

thf(tp_zero_z5237406670263579293d_enat,type,
    zero_z5237406670263579293d_enat: extended_enat ).

thf(tp_zero_zero_complex,type,
    zero_zero_complex: complex ).

thf(tp_zero_zero_int,type,
    zero_zero_int: int ).

thf(tp_zero_zero_nat,type,
    zero_zero_nat: nat ).

thf(tp_zero_zero_real,type,
    zero_zero_real: real ).

thf(3,axiom,
    ! [P: $o] :
      ( ( P = $true )
      | ( P = $false ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_3_1_If_001t__Product____Type__Oprod_It__Nat__Onat_Mt__Nat__Onat_J_T) ).

thf(8053,axiom,
    ! [Xs: list_VEBT_VEBT,I: nat,X: vEBT_VEBT] :
      ( ( size_s6755466524823107622T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) )
      = ( size_s6755466524823107622T_VEBT @ Xs ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_length__list__update) ).

thf(8131,axiom,
    ! [I: nat,I2: nat,Xs: list_VEBT_VEBT,X: vEBT_VEBT,X3: vEBT_VEBT] :
      ( ( I != I2 )
     => ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) @ I2 @ X3 )
        = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I2 @ X3 ) @ I @ X ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_list__update__swap) ).

thf(8135,axiom,
    ! [Xs: list_VEBT_VEBT,I: nat,X: vEBT_VEBT,Y: vEBT_VEBT] :
      ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) @ I @ Y )
      = ( list_u1324408373059187874T_VEBT @ Xs @ I @ Y ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_list__update__overwrite) ).

thf(8138,axiom,
    ~ ? [X_1: nat] : ( vEBT_V8194947554948674370ptions @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ X_1 ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11__C162_C) ).

thf(8139,axiom,
    ! [I: nat,J: nat,Xs: list_VEBT_VEBT,X: vEBT_VEBT] :
      ( ( I != J )
     => ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) @ J )
        = ( nth_VEBT_VEBT @ Xs @ J ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10_nth__list__update__neq) ).

thf(8142,axiom,
    ! [Xs: list_VEBT_VEBT,I: nat] :
      ( ( list_u1324408373059187874T_VEBT @ Xs @ I @ ( nth_VEBT_VEBT @ Xs @ I ) )
      = Xs ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_list__update__id) ).

thf(8145,axiom,
    ~ ? [X_1: nat] : ( vEBT_vebt_member @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ X_1 ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4__C161_C) ).

thf(8146,axiom,
    vEBT_VEBT_minNull @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_tc) ).

thf(8147,axiom,
    ! [X: nat,D: nat] :
      ( ( vEBT_VEBT_bit_concat @ ( vEBT_VEBT_high @ X @ D ) @ ( vEBT_VEBT_low @ X @ D ) @ D )
      = X ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_bit__split__inv) ).

thf(8148,axiom,
    ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) @ ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) ) @ ( vEBT_VEBT_high @ mi @ na ) )
    = ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_insprop) ).

thf(8149,axiom,
    ( i
    = ( vEBT_VEBT_high @ mi @ na ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_True) ).

thf(8150,conjecture,
    ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) @ ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) ) @ i )
    = ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).

thf(8151,negated_conjecture,
    ( ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) @ ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) ) @ i )
      = ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) )
    = $false ),
    inference(negate_conjecture,[status(cth)],[8150]) ).

thf(8152,plain,
    ( ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) @ ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) ) @ i )
      = ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) )
    = $false ),
    inference(unfold_def,[status(thm)],[8151]) ).

thf(8153,plain,
    ( ( ! [P: $o] :
          ( ( P = $true )
          | ( P = $false ) ) )
    = $true ),
    inference(unfold_def,[status(thm)],[3]) ).

thf(8154,plain,
    ( ( ! [Xs: list_VEBT_VEBT,I: nat,X: vEBT_VEBT] :
          ( ( size_s6755466524823107622T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) )
          = ( size_s6755466524823107622T_VEBT @ Xs ) ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8053]) ).

thf(8155,plain,
    ( ( ! [I: nat,I2: nat,Xs: list_VEBT_VEBT,X: vEBT_VEBT,X3: vEBT_VEBT] :
          ( ( I != I2 )
         => ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) @ I2 @ X3 )
            = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I2 @ X3 ) @ I @ X ) ) ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8131]) ).

thf(8156,plain,
    ( ( ! [Xs: list_VEBT_VEBT,I: nat,X: vEBT_VEBT,Y: vEBT_VEBT] :
          ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) @ I @ Y )
          = ( list_u1324408373059187874T_VEBT @ Xs @ I @ Y ) ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8135]) ).

thf(8157,plain,
    ( ( ~ ? [X_1: nat] : ( vEBT_V8194947554948674370ptions @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ X_1 ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8138]) ).

thf(8158,plain,
    ( ( ! [I: nat,J: nat,Xs: list_VEBT_VEBT,X: vEBT_VEBT] :
          ( ( I != J )
         => ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) @ J )
            = ( nth_VEBT_VEBT @ Xs @ J ) ) ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8139]) ).

thf(8159,plain,
    ( ( ! [Xs: list_VEBT_VEBT,I: nat] :
          ( ( list_u1324408373059187874T_VEBT @ Xs @ I @ ( nth_VEBT_VEBT @ Xs @ I ) )
          = Xs ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8142]) ).

thf(8160,plain,
    ( ( ~ ? [X_1: nat] : ( vEBT_vebt_member @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ X_1 ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8145]) ).

thf(8161,plain,
    ( ( vEBT_VEBT_minNull @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8146]) ).

thf(8162,plain,
    ( ( ! [X: nat,D: nat] :
          ( ( vEBT_VEBT_bit_concat @ ( vEBT_VEBT_high @ X @ D ) @ ( vEBT_VEBT_low @ X @ D ) @ D )
          = X ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8147]) ).

thf(8163,plain,
    ( ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) @ ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) ) @ ( vEBT_VEBT_high @ mi @ na ) )
      = ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8148]) ).

thf(8164,plain,
    ( ( i
      = ( vEBT_VEBT_high @ mi @ na ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8149]) ).

thf(8165,plain,
    ( ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) @ ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) ) @ i )
     != ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) )
    = $true ),
    inference(polarity_switch,[status(thm)],[8152]) ).

thf(8166,plain,
    ( ( i
      = ( vEBT_VEBT_high @ mi @ na ) )
    = $true ),
    inference(copy,[status(thm)],[8164]) ).

thf(8167,plain,
    ( ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) @ ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) ) @ ( vEBT_VEBT_high @ mi @ na ) )
      = ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) )
    = $true ),
    inference(copy,[status(thm)],[8163]) ).

thf(8168,plain,
    ( ( ! [X: nat,D: nat] :
          ( ( vEBT_VEBT_bit_concat @ ( vEBT_VEBT_high @ X @ D ) @ ( vEBT_VEBT_low @ X @ D ) @ D )
          = X ) )
    = $true ),
    inference(copy,[status(thm)],[8162]) ).

thf(8169,plain,
    ( ( vEBT_VEBT_minNull @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) )
    = $true ),
    inference(copy,[status(thm)],[8161]) ).

thf(8170,plain,
    ( ( ~ ? [X_1: nat] : ( vEBT_vebt_member @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ X_1 ) )
    = $true ),
    inference(copy,[status(thm)],[8160]) ).

thf(8171,plain,
    ( ( ! [Xs: list_VEBT_VEBT,I: nat] :
          ( ( list_u1324408373059187874T_VEBT @ Xs @ I @ ( nth_VEBT_VEBT @ Xs @ I ) )
          = Xs ) )
    = $true ),
    inference(copy,[status(thm)],[8159]) ).

thf(8172,plain,
    ( ( ! [I: nat,J: nat,Xs: list_VEBT_VEBT,X: vEBT_VEBT] :
          ( ( I != J )
         => ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) @ J )
            = ( nth_VEBT_VEBT @ Xs @ J ) ) ) )
    = $true ),
    inference(copy,[status(thm)],[8158]) ).

thf(8173,plain,
    ( ( ~ ? [X_1: nat] : ( vEBT_V8194947554948674370ptions @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ X_1 ) )
    = $true ),
    inference(copy,[status(thm)],[8157]) ).

thf(8174,plain,
    ( ( ! [Xs: list_VEBT_VEBT,I: nat,X: vEBT_VEBT,Y: vEBT_VEBT] :
          ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) @ I @ Y )
          = ( list_u1324408373059187874T_VEBT @ Xs @ I @ Y ) ) )
    = $true ),
    inference(copy,[status(thm)],[8156]) ).

thf(8175,plain,
    ( ( ! [I: nat,I2: nat,Xs: list_VEBT_VEBT,X: vEBT_VEBT,X3: vEBT_VEBT] :
          ( ( I != I2 )
         => ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) @ I2 @ X3 )
            = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I2 @ X3 ) @ I @ X ) ) ) )
    = $true ),
    inference(copy,[status(thm)],[8155]) ).

thf(8176,plain,
    ( ( ! [Xs: list_VEBT_VEBT,I: nat,X: vEBT_VEBT] :
          ( ( size_s6755466524823107622T_VEBT @ ( list_u1324408373059187874T_VEBT @ Xs @ I @ X ) )
          = ( size_s6755466524823107622T_VEBT @ Xs ) ) )
    = $true ),
    inference(copy,[status(thm)],[8154]) ).

thf(8177,plain,
    ( ( ! [P: $o] :
          ( ( P = $true )
          | ( P = $false ) ) )
    = $true ),
    inference(copy,[status(thm)],[8153]) ).

thf(8178,plain,
    ( ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) @ ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) ) @ i )
     != ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) )
    = $true ),
    inference(copy,[status(thm)],[8165]) ).

thf(8179,plain,
    ( ( ! [SX0: nat,SX1: nat,SX2: list_VEBT_VEBT,SX3: vEBT_VEBT] :
          ( ~ ( ( SX0 != SX1 ) )
          | ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ SX2 @ SX0 @ SX3 ) @ SX1 )
            = ( nth_VEBT_VEBT @ SX2 @ SX1 ) ) ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8172]) ).

thf(8180,plain,
    ( ( ~ ~ ! [SX0: nat] :
              ~ ( vEBT_vebt_member @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ SX0 ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8170]) ).

thf(8181,plain,
    ( ( ~ ~ ! [SX0: nat] :
              ~ ( vEBT_V8194947554948674370ptions @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ SX0 ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8173]) ).

thf(8182,plain,
    ( ( ! [SX0: nat,SX1: nat,SX2: list_VEBT_VEBT,SX3: vEBT_VEBT,SX4: vEBT_VEBT] :
          ( ~ ( ( SX0 != SX1 ) )
          | ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SX2 @ SX0 @ SX3 ) @ SX1 @ SX4 )
            = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SX2 @ SX1 @ SX4 ) @ SX0 @ SX3 ) ) ) )
    = $true ),
    inference(unfold_def,[status(thm)],[8175]) ).

thf(8183,plain,
    ! [SV1: nat] :
      ( ( ! [SY23: nat] :
            ( ( vEBT_VEBT_bit_concat @ ( vEBT_VEBT_high @ SV1 @ SY23 ) @ ( vEBT_VEBT_low @ SV1 @ SY23 ) @ SY23 )
            = SV1 ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8168]) ).

thf(8184,plain,
    ! [SV2: list_VEBT_VEBT] :
      ( ( ! [SY24: nat] :
            ( ( list_u1324408373059187874T_VEBT @ SV2 @ SY24 @ ( nth_VEBT_VEBT @ SV2 @ SY24 ) )
            = SV2 ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8171]) ).

thf(8185,plain,
    ! [SV3: list_VEBT_VEBT] :
      ( ( ! [SY25: nat,SY26: vEBT_VEBT,SY27: vEBT_VEBT] :
            ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV3 @ SY25 @ SY26 ) @ SY25 @ SY27 )
            = ( list_u1324408373059187874T_VEBT @ SV3 @ SY25 @ SY27 ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8174]) ).

thf(8186,plain,
    ! [SV4: list_VEBT_VEBT] :
      ( ( ! [SY28: nat,SY29: vEBT_VEBT] :
            ( ( size_s6755466524823107622T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV4 @ SY28 @ SY29 ) )
            = ( size_s6755466524823107622T_VEBT @ SV4 ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8176]) ).

thf(8187,plain,
    ! [SV5: $o] :
      ( ( ( SV5 = $true )
        | ( SV5 = $false ) )
      = $true ),
    inference(extcnf_forall_special_pos,[status(thm)],[8177]) ).

thf(8188,plain,
    ( ( ( $true = $true )
      | ( $true = $false ) )
    = $true ),
    inference(extcnf_forall_special_pos,[status(thm)],[8177]) ).

thf(8189,plain,
    ( ( ( $false = $true )
      | ( $false = $false ) )
    = $true ),
    inference(extcnf_forall_special_pos,[status(thm)],[8177]) ).

thf(8190,plain,
    ( ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) @ ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) ) @ i )
      = ( vEBT_vebt_insert @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ ( vEBT_VEBT_low @ mi @ na ) ) )
    = $false ),
    inference(extcnf_not_pos,[status(thm)],[8178]) ).

thf(8191,plain,
    ! [SV6: nat] :
      ( ( ! [SY30: nat,SY31: list_VEBT_VEBT,SY32: vEBT_VEBT] :
            ( ~ ( ( SV6 != SY30 ) )
            | ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ SY31 @ SV6 @ SY32 ) @ SY30 )
              = ( nth_VEBT_VEBT @ SY31 @ SY30 ) ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8179]) ).

thf(8192,plain,
    ( ( ~ ! [SX0: nat] :
            ~ ( vEBT_vebt_member @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ SX0 ) )
    = $false ),
    inference(extcnf_not_pos,[status(thm)],[8180]) ).

thf(8193,plain,
    ( ( ~ ! [SX0: nat] :
            ~ ( vEBT_V8194947554948674370ptions @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ SX0 ) )
    = $false ),
    inference(extcnf_not_pos,[status(thm)],[8181]) ).

thf(8194,plain,
    ! [SV7: nat] :
      ( ( ! [SY33: nat,SY34: list_VEBT_VEBT,SY35: vEBT_VEBT,SY36: vEBT_VEBT] :
            ( ~ ( ( SV7 != SY33 ) )
            | ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SY34 @ SV7 @ SY35 ) @ SY33 @ SY36 )
              = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SY34 @ SY33 @ SY36 ) @ SV7 @ SY35 ) ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8182]) ).

thf(8195,plain,
    ! [SV8: nat,SV1: nat] :
      ( ( ( vEBT_VEBT_bit_concat @ ( vEBT_VEBT_high @ SV1 @ SV8 ) @ ( vEBT_VEBT_low @ SV1 @ SV8 ) @ SV8 )
        = SV1 )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8183]) ).

thf(8196,plain,
    ! [SV9: nat,SV2: list_VEBT_VEBT] :
      ( ( ( list_u1324408373059187874T_VEBT @ SV2 @ SV9 @ ( nth_VEBT_VEBT @ SV2 @ SV9 ) )
        = SV2 )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8184]) ).

thf(8197,plain,
    ! [SV10: nat,SV3: list_VEBT_VEBT] :
      ( ( ! [SY37: vEBT_VEBT,SY38: vEBT_VEBT] :
            ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV3 @ SV10 @ SY37 ) @ SV10 @ SY38 )
            = ( list_u1324408373059187874T_VEBT @ SV3 @ SV10 @ SY38 ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8185]) ).

thf(8198,plain,
    ! [SV11: nat,SV4: list_VEBT_VEBT] :
      ( ( ! [SY39: vEBT_VEBT] :
            ( ( size_s6755466524823107622T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV4 @ SV11 @ SY39 ) )
            = ( size_s6755466524823107622T_VEBT @ SV4 ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8186]) ).

thf(8199,plain,
    ! [SV5: $o] :
      ( ( ( SV5 = $true )
        = $true )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8187]) ).

thf(8200,plain,
    ( ( ( $true = $true )
      = $true )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8188]) ).

thf(8201,plain,
    ( ( ( $false = $true )
      = $true )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8189]) ).

thf(8202,plain,
    ! [SV12: nat,SV6: nat] :
      ( ( ! [SY40: list_VEBT_VEBT,SY41: vEBT_VEBT] :
            ( ~ ( ( SV6 != SV12 ) )
            | ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ SY40 @ SV6 @ SY41 ) @ SV12 )
              = ( nth_VEBT_VEBT @ SY40 @ SV12 ) ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8191]) ).

thf(8203,plain,
    ( ( ! [SX0: nat] :
          ~ ( vEBT_vebt_member @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ SX0 ) )
    = $true ),
    inference(extcnf_not_neg,[status(thm)],[8192]) ).

thf(8204,plain,
    ( ( ! [SX0: nat] :
          ~ ( vEBT_V8194947554948674370ptions @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ SX0 ) )
    = $true ),
    inference(extcnf_not_neg,[status(thm)],[8193]) ).

thf(8205,plain,
    ! [SV13: nat,SV7: nat] :
      ( ( ! [SY42: list_VEBT_VEBT,SY43: vEBT_VEBT,SY44: vEBT_VEBT] :
            ( ~ ( ( SV7 != SV13 ) )
            | ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SY42 @ SV7 @ SY43 ) @ SV13 @ SY44 )
              = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SY42 @ SV13 @ SY44 ) @ SV7 @ SY43 ) ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8194]) ).

thf(8206,plain,
    ! [SV14: vEBT_VEBT,SV10: nat,SV3: list_VEBT_VEBT] :
      ( ( ! [SY45: vEBT_VEBT] :
            ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV3 @ SV10 @ SV14 ) @ SV10 @ SY45 )
            = ( list_u1324408373059187874T_VEBT @ SV3 @ SV10 @ SY45 ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8197]) ).

thf(8207,plain,
    ! [SV15: vEBT_VEBT,SV11: nat,SV4: list_VEBT_VEBT] :
      ( ( ( size_s6755466524823107622T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV4 @ SV11 @ SV15 ) )
        = ( size_s6755466524823107622T_VEBT @ SV4 ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8198]) ).

thf(8208,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $true )
          | ~ ( ~ SV5
              | ~ $true ) )
        = $true )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8199]) ).

thf(8209,plain,
    ! [SV5: $o] :
      ( ( ( SV5 = $true )
        = $true )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8199]) ).

thf(8210,plain,
    ( ( ( ~ ( $true
            | $true )
        | ~ ( ~ $true
            | ~ $true ) )
      = $true )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8200]) ).

thf(8211,plain,
    ( ( ( $true = $true )
      = $true )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8200]) ).

thf(8212,plain,
    ( ( ( ~ ( $false
            | $true )
        | ~ ( ~ $false
            | ~ $true ) )
      = $true )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8201]) ).

thf(8213,plain,
    ( ( ( $false = $true )
      = $true )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8201]) ).

thf(8214,plain,
    ! [SV16: list_VEBT_VEBT,SV12: nat,SV6: nat] :
      ( ( ! [SY46: vEBT_VEBT] :
            ( ~ ( ( SV6 != SV12 ) )
            | ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ SV16 @ SV6 @ SY46 ) @ SV12 )
              = ( nth_VEBT_VEBT @ SV16 @ SV12 ) ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8202]) ).

thf(8215,plain,
    ! [SV17: nat] :
      ( ( ~ ( vEBT_vebt_member @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ SV17 ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8203]) ).

thf(8216,plain,
    ! [SV18: nat] :
      ( ( ~ ( vEBT_V8194947554948674370ptions @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ SV18 ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8204]) ).

thf(8217,plain,
    ! [SV19: list_VEBT_VEBT,SV13: nat,SV7: nat] :
      ( ( ! [SY47: vEBT_VEBT,SY48: vEBT_VEBT] :
            ( ~ ( ( SV7 != SV13 ) )
            | ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV7 @ SY47 ) @ SV13 @ SY48 )
              = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV13 @ SY48 ) @ SV7 @ SY47 ) ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8205]) ).

thf(8218,plain,
    ! [SV20: vEBT_VEBT,SV14: vEBT_VEBT,SV10: nat,SV3: list_VEBT_VEBT] :
      ( ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV3 @ SV10 @ SV14 ) @ SV10 @ SV20 )
        = ( list_u1324408373059187874T_VEBT @ SV3 @ SV10 @ SV20 ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8206]) ).

thf(8219,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $true ) )
        = $true )
      | ( ( ~ ( ~ SV5
              | ~ $true ) )
        = $true )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8208]) ).

thf(8220,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $false )
          | ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8209]) ).

thf(8221,plain,
    ! [SV5: $o] :
      ( ( ( SV5 = $false )
        = $true )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8209]) ).

thf(8222,plain,
    ( ( ( ~ ( $true
            | $true ) )
      = $true )
    | ( ( ~ ( ~ $true
            | ~ $true ) )
      = $true )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8210]) ).

thf(8223,plain,
    ( ( ( ~ ( $true
            | $false )
        | ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8211]) ).

thf(8224,plain,
    ( ( ( $true = $false )
      = $true )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8211]) ).

thf(8225,plain,
    ( ( ( ~ ( $false
            | $true ) )
      = $true )
    | ( ( ~ ( ~ $false
            | ~ $true ) )
      = $true )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8212]) ).

thf(8226,plain,
    ( ( ( ~ ( $false
            | $false )
        | ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8213]) ).

thf(8227,plain,
    ( ( ( $false = $false )
      = $true )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8213]) ).

thf(8228,plain,
    ! [SV21: vEBT_VEBT,SV16: list_VEBT_VEBT,SV12: nat,SV6: nat] :
      ( ( ~ ( ( SV6 != SV12 ) )
        | ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ SV16 @ SV6 @ SV21 ) @ SV12 )
          = ( nth_VEBT_VEBT @ SV16 @ SV12 ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8214]) ).

thf(8229,plain,
    ! [SV17: nat] :
      ( ( vEBT_vebt_member @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ SV17 )
      = $false ),
    inference(extcnf_not_pos,[status(thm)],[8215]) ).

thf(8230,plain,
    ! [SV18: nat] :
      ( ( vEBT_V8194947554948674370ptions @ ( nth_VEBT_VEBT @ treeList @ ( vEBT_VEBT_high @ mi @ na ) ) @ SV18 )
      = $false ),
    inference(extcnf_not_pos,[status(thm)],[8216]) ).

thf(8231,plain,
    ! [SV22: vEBT_VEBT,SV19: list_VEBT_VEBT,SV13: nat,SV7: nat] :
      ( ( ! [SY49: vEBT_VEBT] :
            ( ~ ( ( SV7 != SV13 ) )
            | ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV7 @ SV22 ) @ SV13 @ SY49 )
              = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV13 @ SY49 ) @ SV7 @ SV22 ) ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8217]) ).

thf(8232,plain,
    ! [SV5: $o] :
      ( ( ( SV5
          | $true )
        = $false )
      | ( ( ~ ( ~ SV5
              | ~ $true ) )
        = $true )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8219]) ).

thf(8233,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $false ) )
        = $true )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8220]) ).

thf(8234,plain,
    ( ( ( $true
        | $true )
      = $false )
    | ( ( ~ ( ~ $true
            | ~ $true ) )
      = $true )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8222]) ).

thf(8235,plain,
    ( ( ( ~ ( $true
            | $false ) )
      = $true )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8223]) ).

thf(8236,plain,
    ( ( ( $false
        | $true )
      = $false )
    | ( ( ~ ( ~ $false
            | ~ $true ) )
      = $true )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8225]) ).

thf(8237,plain,
    ( ( ( ~ ( $false
            | $false ) )
      = $true )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8226]) ).

thf(8238,plain,
    ! [SV21: vEBT_VEBT,SV16: list_VEBT_VEBT,SV12: nat,SV6: nat] :
      ( ( ( ~ ( ( SV6 != SV12 ) ) )
        = $true )
      | ( ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ SV16 @ SV6 @ SV21 ) @ SV12 )
          = ( nth_VEBT_VEBT @ SV16 @ SV12 ) )
        = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8228]) ).

thf(8239,plain,
    ! [SV23: vEBT_VEBT,SV22: vEBT_VEBT,SV19: list_VEBT_VEBT,SV13: nat,SV7: nat] :
      ( ( ~ ( ( SV7 != SV13 ) )
        | ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV7 @ SV22 ) @ SV13 @ SV23 )
          = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV13 @ SV23 ) @ SV7 @ SV22 ) ) )
      = $true ),
    inference(extcnf_forall_pos,[status(thm)],[8231]) ).

thf(8240,plain,
    ! [SV5: $o] :
      ( ( SV5 = $false )
      | ( ( ~ ( ~ SV5
              | ~ $true ) )
        = $true )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8232]) ).

thf(8241,plain,
    ! [SV5: $o] :
      ( ( $true = $false )
      | ( ( ~ ( ~ SV5
              | ~ $true ) )
        = $true )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8232]) ).

thf(8242,plain,
    ! [SV5: $o] :
      ( ( ( SV5
          | $false )
        = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8233]) ).

thf(8243,plain,
    ( ( $true = $false )
    | ( ( ~ ( ~ $true
            | ~ $true ) )
      = $true )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8234]) ).

thf(8244,plain,
    ( ( $true = $false )
    | ( ( ~ ( ~ $true
            | ~ $true ) )
      = $true )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8234]) ).

thf(8245,plain,
    ( ( ( $true
        | $false )
      = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8235]) ).

thf(8246,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $false
            | ~ $true ) )
      = $true )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8236]) ).

thf(8247,plain,
    ( ( $true = $false )
    | ( ( ~ ( ~ $false
            | ~ $true ) )
      = $true )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8236]) ).

thf(8248,plain,
    ( ( ( $false
        | $false )
      = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8237]) ).

thf(8249,plain,
    ! [SV21: vEBT_VEBT,SV16: list_VEBT_VEBT,SV12: nat,SV6: nat] :
      ( ( ( SV6 != SV12 )
        = $false )
      | ( ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ SV16 @ SV6 @ SV21 ) @ SV12 )
          = ( nth_VEBT_VEBT @ SV16 @ SV12 ) )
        = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8238]) ).

thf(8250,plain,
    ! [SV23: vEBT_VEBT,SV22: vEBT_VEBT,SV19: list_VEBT_VEBT,SV13: nat,SV7: nat] :
      ( ( ( ~ ( ( SV7 != SV13 ) ) )
        = $true )
      | ( ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV7 @ SV22 ) @ SV13 @ SV23 )
          = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV13 @ SV23 ) @ SV7 @ SV22 ) )
        = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8239]) ).

thf(8251,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $true )
        = $false )
      | ( SV5 = $false )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8240]) ).

thf(8252,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $true )
        = $false )
      | ( $true = $false )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8241]) ).

thf(8253,plain,
    ! [SV5: $o] :
      ( ( SV5 = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8242]) ).

thf(8254,plain,
    ! [SV5: $o] :
      ( ( $false = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8242]) ).

thf(8255,plain,
    ( ( ( ~ $true
        | ~ $true )
      = $false )
    | ( $true = $false )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8243]) ).

thf(8256,plain,
    ( ( ( ~ $true
        | ~ $true )
      = $false )
    | ( $true = $false )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8244]) ).

thf(8257,plain,
    ( ( $true = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8245]) ).

thf(8258,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8245]) ).

thf(8259,plain,
    ( ( ( ~ $false
        | ~ $true )
      = $false )
    | ( $false = $false )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8246]) ).

thf(8260,plain,
    ( ( ( ~ $false
        | ~ $true )
      = $false )
    | ( $true = $false )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8247]) ).

thf(8261,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8248]) ).

thf(8262,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8248]) ).

thf(8263,plain,
    ! [SV21: vEBT_VEBT,SV16: list_VEBT_VEBT,SV12: nat,SV6: nat] :
      ( ( ( SV6 = SV12 )
        = $true )
      | ( ( ( nth_VEBT_VEBT @ ( list_u1324408373059187874T_VEBT @ SV16 @ SV6 @ SV21 ) @ SV12 )
          = ( nth_VEBT_VEBT @ SV16 @ SV12 ) )
        = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8249]) ).

thf(8264,plain,
    ! [SV23: vEBT_VEBT,SV22: vEBT_VEBT,SV19: list_VEBT_VEBT,SV13: nat,SV7: nat] :
      ( ( ( SV7 != SV13 )
        = $false )
      | ( ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV7 @ SV22 ) @ SV13 @ SV23 )
          = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV13 @ SV23 ) @ SV7 @ SV22 ) )
        = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8250]) ).

thf(8265,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( SV5 = $false )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8251]) ).

thf(8266,plain,
    ! [SV5: $o] :
      ( ( ( ~ $true ) = $false )
      | ( SV5 = $false )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8251]) ).

thf(8267,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( $true = $false )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8252]) ).

thf(8268,plain,
    ! [SV5: $o] :
      ( ( ( ~ $true ) = $false )
      | ( $true = $false )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8252]) ).

thf(8269,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $false )
        = $false )
      | ( SV5 = $false )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8253]) ).

thf(8270,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $false )
        = $false )
      | ( $false = $false )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8254]) ).

thf(8271,plain,
    ( ( ( ~ $true ) = $false )
    | ( $true = $false )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8255]) ).

thf(8272,plain,
    ( ( ( ~ $true ) = $false )
    | ( $true = $false )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8255]) ).

thf(8273,plain,
    ( ( ( ~ $true ) = $false )
    | ( $true = $false )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8256]) ).

thf(8274,plain,
    ( ( ( ~ $true ) = $false )
    | ( $true = $false )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8256]) ).

thf(8275,plain,
    ( ( ( ~ $true
        | ~ $false )
      = $false )
    | ( $true = $false )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8257]) ).

thf(8276,plain,
    ( ( ( ~ $true
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8258]) ).

thf(8277,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8259]) ).

thf(8278,plain,
    ( ( ( ~ $true ) = $false )
    | ( $false = $false )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8259]) ).

thf(8279,plain,
    ( ( ( ~ $false ) = $false )
    | ( $true = $false )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8260]) ).

thf(8280,plain,
    ( ( ( ~ $true ) = $false )
    | ( $true = $false )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8260]) ).

thf(8281,plain,
    ( ( ( ~ $false
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8261]) ).

thf(8282,plain,
    ( ( ( ~ $false
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8262]) ).

thf(8283,plain,
    ! [SV23: vEBT_VEBT,SV22: vEBT_VEBT,SV19: list_VEBT_VEBT,SV13: nat,SV7: nat] :
      ( ( ( SV7 = SV13 )
        = $true )
      | ( ( ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV7 @ SV22 ) @ SV13 @ SV23 )
          = ( list_u1324408373059187874T_VEBT @ ( list_u1324408373059187874T_VEBT @ SV19 @ SV13 @ SV23 ) @ SV7 @ SV22 ) )
        = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8264]) ).

thf(8284,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( SV5 = $false )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8265]) ).

thf(8285,plain,
    ! [SV5: $o] :
      ( ( $true = $true )
      | ( SV5 = $false )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8266]) ).

thf(8286,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( $true = $false )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8267]) ).

thf(8287,plain,
    ! [SV5: $o] :
      ( ( $true = $true )
      | ( $true = $false )
      | ( ( SV5 = $false )
        = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8268]) ).

thf(8288,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( SV5 = $false )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8269]) ).

thf(8289,plain,
    ! [SV5: $o] :
      ( ( ( ~ $false ) = $false )
      | ( SV5 = $false )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8269]) ).

thf(8290,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( $false = $false )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8270]) ).

thf(8291,plain,
    ! [SV5: $o] :
      ( ( ( ~ $false ) = $false )
      | ( $false = $false )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8270]) ).

thf(8292,plain,
    ( ( $true = $true )
    | ( $true = $false )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8271]) ).

thf(8293,plain,
    ( ( $true = $true )
    | ( $true = $false )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8272]) ).

thf(8294,plain,
    ( ( $true = $true )
    | ( $true = $false )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8273]) ).

thf(8295,plain,
    ( ( $true = $true )
    | ( $true = $false )
    | ( ( $true = $false )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8274]) ).

thf(8296,plain,
    ( ( ( ~ $true ) = $false )
    | ( $true = $false )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8275]) ).

thf(8297,plain,
    ( ( ( ~ $false ) = $false )
    | ( $true = $false )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8275]) ).

thf(8298,plain,
    ( ( ( ~ $true ) = $false )
    | ( $false = $false )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8276]) ).

thf(8299,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8276]) ).

thf(8300,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8277]) ).

thf(8301,plain,
    ( ( $true = $true )
    | ( $false = $false )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8278]) ).

thf(8302,plain,
    ( ( $false = $true )
    | ( $true = $false )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8279]) ).

thf(8303,plain,
    ( ( $true = $true )
    | ( $true = $false )
    | ( ( $false = $false )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8280]) ).

thf(8304,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8281]) ).

thf(8305,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8281]) ).

thf(8306,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8282]) ).

thf(8307,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8282]) ).

thf(8308,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $false )
          | ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8284]) ).

thf(8309,plain,
    ! [SV5: $o] :
      ( ( ( SV5 = $false )
        = $true )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8284]) ).

thf(8310,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $false )
          | ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8285]) ).

thf(8311,plain,
    ! [SV5: $o] :
      ( ( ( SV5 = $false )
        = $true )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8285]) ).

thf(8312,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $false )
          | ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8286]) ).

thf(8313,plain,
    ! [SV5: $o] :
      ( ( ( SV5 = $false )
        = $true )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8286]) ).

thf(8314,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $false )
          | ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8287]) ).

thf(8315,plain,
    ! [SV5: $o] :
      ( ( ( SV5 = $false )
        = $true )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8287]) ).

thf(8316,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( SV5 = $false )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8288]) ).

thf(8317,plain,
    ! [SV5: $o] :
      ( ( $false = $true )
      | ( SV5 = $false )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8289]) ).

thf(8318,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( $false = $false )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8290]) ).

thf(8319,plain,
    ! [SV5: $o] :
      ( ( $false = $true )
      | ( $false = $false )
      | ( ( SV5 = $true )
        = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8291]) ).

thf(8320,plain,
    ( ( ( ~ ( $true
            | $false )
        | ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8292]) ).

thf(8321,plain,
    ( ( ( $true = $false )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8292]) ).

thf(8322,plain,
    ( ( ( ~ ( $true
            | $false )
        | ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8293]) ).

thf(8323,plain,
    ( ( ( $true = $false )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8293]) ).

thf(8324,plain,
    ( ( ( ~ ( $true
            | $false )
        | ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8294]) ).

thf(8325,plain,
    ( ( ( $true = $false )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8294]) ).

thf(8326,plain,
    ( ( ( ~ ( $true
            | $false )
        | ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8295]) ).

thf(8327,plain,
    ( ( ( $true = $false )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8295]) ).

thf(8328,plain,
    ( ( $true = $true )
    | ( $true = $false )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8296]) ).

thf(8329,plain,
    ( ( $false = $true )
    | ( $true = $false )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8297]) ).

thf(8330,plain,
    ( ( $true = $true )
    | ( $false = $false )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8298]) ).

thf(8331,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( ( $true = $true )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8299]) ).

thf(8332,plain,
    ( ( ( ~ ( $false
            | $false )
        | ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8300]) ).

thf(8333,plain,
    ( ( ( $false = $false )
      = $true )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8300]) ).

thf(8334,plain,
    ( ( ( ~ ( $false
            | $false )
        | ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8301]) ).

thf(8335,plain,
    ( ( ( $false = $false )
      = $true )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8301]) ).

thf(8336,plain,
    ( ( ( ~ ( $false
            | $false )
        | ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8302]) ).

thf(8337,plain,
    ( ( ( $false = $false )
      = $true )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8302]) ).

thf(8338,plain,
    ( ( ( ~ ( $false
            | $false )
        | ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8303]) ).

thf(8339,plain,
    ( ( ( $false = $false )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_equal_pos,[status(thm)],[8303]) ).

thf(8340,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8304]) ).

thf(8341,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8305]) ).

thf(8342,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8306]) ).

thf(8343,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( ( $false = $true )
      = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8307]) ).

thf(8344,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $false ) )
        = $true )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8308]) ).

thf(8345,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $false ) )
        = $true )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8310]) ).

thf(8346,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $false ) )
        = $true )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8312]) ).

thf(8347,plain,
    ! [SV5: $o] :
      ( ( ( ~ ( SV5
              | $false ) )
        = $true )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8314]) ).

thf(8348,plain,
    ( ( ( ~ ( $true
            | $false ) )
      = $true )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8320]) ).

thf(8349,plain,
    ( ( ( ~ ( $true
            | $false ) )
      = $true )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8322]) ).

thf(8350,plain,
    ( ( ( ~ ( $true
            | $false ) )
      = $true )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8324]) ).

thf(8351,plain,
    ( ( ( ~ ( $true
            | $false ) )
      = $true )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8326]) ).

thf(8352,plain,
    ( ( ( ~ ( $false
            | $false ) )
      = $true )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8332]) ).

thf(8353,plain,
    ( ( ( ~ ( $false
            | $false ) )
      = $true )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8334]) ).

thf(8354,plain,
    ( ( ( ~ ( $false
            | $false ) )
      = $true )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8336]) ).

thf(8355,plain,
    ( ( ( ~ ( $false
            | $false ) )
      = $true )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_pos,[status(thm)],[8338]) ).

thf(8356,plain,
    ! [SV5: $o] :
      ( ( ( SV5
          | $false )
        = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8344]) ).

thf(8357,plain,
    ! [SV5: $o] :
      ( ( ( SV5
          | $false )
        = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8345]) ).

thf(8358,plain,
    ! [SV5: $o] :
      ( ( ( SV5
          | $false )
        = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8346]) ).

thf(8359,plain,
    ! [SV5: $o] :
      ( ( ( SV5
          | $false )
        = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8347]) ).

thf(8360,plain,
    ( ( ( $true
        | $false )
      = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8348]) ).

thf(8361,plain,
    ( ( ( $true
        | $false )
      = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8349]) ).

thf(8362,plain,
    ( ( ( $true
        | $false )
      = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8350]) ).

thf(8363,plain,
    ( ( ( $true
        | $false )
      = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8351]) ).

thf(8364,plain,
    ( ( ( $false
        | $false )
      = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8352]) ).

thf(8365,plain,
    ( ( ( $false
        | $false )
      = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8353]) ).

thf(8366,plain,
    ( ( ( $false
        | $false )
      = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8354]) ).

thf(8367,plain,
    ( ( ( $false
        | $false )
      = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8355]) ).

thf(8368,plain,
    ! [SV5: $o] :
      ( ( SV5 = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8356]) ).

thf(8369,plain,
    ! [SV5: $o] :
      ( ( $false = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8356]) ).

thf(8370,plain,
    ! [SV5: $o] :
      ( ( SV5 = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8357]) ).

thf(8371,plain,
    ! [SV5: $o] :
      ( ( $false = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8357]) ).

thf(8372,plain,
    ! [SV5: $o] :
      ( ( SV5 = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8358]) ).

thf(8373,plain,
    ! [SV5: $o] :
      ( ( $false = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8358]) ).

thf(8374,plain,
    ! [SV5: $o] :
      ( ( SV5 = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8359]) ).

thf(8375,plain,
    ! [SV5: $o] :
      ( ( $false = $false )
      | ( ( ~ ( ~ SV5
              | ~ $false ) )
        = $true )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8359]) ).

thf(8376,plain,
    ( ( $true = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8360]) ).

thf(8377,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8360]) ).

thf(8378,plain,
    ( ( $true = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8361]) ).

thf(8379,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8361]) ).

thf(8380,plain,
    ( ( $true = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8362]) ).

thf(8381,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8362]) ).

thf(8382,plain,
    ( ( $true = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8363]) ).

thf(8383,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $true
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8363]) ).

thf(8384,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8364]) ).

thf(8385,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8364]) ).

thf(8386,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8365]) ).

thf(8387,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8365]) ).

thf(8388,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8366]) ).

thf(8389,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8366]) ).

thf(8390,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8367]) ).

thf(8391,plain,
    ( ( $false = $false )
    | ( ( ~ ( ~ $false
            | ~ $false ) )
      = $true )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8367]) ).

thf(8392,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $false )
        = $false )
      | ( SV5 = $false )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8368]) ).

thf(8393,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $false )
        = $false )
      | ( $false = $false )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8369]) ).

thf(8394,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $false )
        = $false )
      | ( SV5 = $false )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8370]) ).

thf(8395,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $false )
        = $false )
      | ( $false = $false )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8371]) ).

thf(8396,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $false )
        = $false )
      | ( SV5 = $false )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8372]) ).

thf(8397,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $false )
        = $false )
      | ( $false = $false )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8373]) ).

thf(8398,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $false )
        = $false )
      | ( SV5 = $false )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8374]) ).

thf(8399,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5
          | ~ $false )
        = $false )
      | ( $false = $false )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8375]) ).

thf(8400,plain,
    ( ( ( ~ $true
        | ~ $false )
      = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8376]) ).

thf(8401,plain,
    ( ( ( ~ $true
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8377]) ).

thf(8402,plain,
    ( ( ( ~ $true
        | ~ $false )
      = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8378]) ).

thf(8403,plain,
    ( ( ( ~ $true
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8379]) ).

thf(8404,plain,
    ( ( ( ~ $true
        | ~ $false )
      = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8380]) ).

thf(8405,plain,
    ( ( ( ~ $true
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8381]) ).

thf(8406,plain,
    ( ( ( ~ $true
        | ~ $false )
      = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8382]) ).

thf(8407,plain,
    ( ( ( ~ $true
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8383]) ).

thf(8408,plain,
    ( ( ( ~ $false
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8384]) ).

thf(8409,plain,
    ( ( ( ~ $false
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8385]) ).

thf(8410,plain,
    ( ( ( ~ $false
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8386]) ).

thf(8411,plain,
    ( ( ( ~ $false
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8387]) ).

thf(8412,plain,
    ( ( ( ~ $false
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8388]) ).

thf(8413,plain,
    ( ( ( ~ $false
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8389]) ).

thf(8414,plain,
    ( ( ( ~ $false
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8390]) ).

thf(8415,plain,
    ( ( ( ~ $false
        | ~ $false )
      = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_pos,[status(thm)],[8391]) ).

thf(8416,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( SV5 = $false )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8392]) ).

thf(8417,plain,
    ! [SV5: $o] :
      ( ( ( ~ $false ) = $false )
      | ( SV5 = $false )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8392]) ).

thf(8418,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( $false = $false )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8393]) ).

thf(8419,plain,
    ! [SV5: $o] :
      ( ( ( ~ $false ) = $false )
      | ( $false = $false )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8393]) ).

thf(8420,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( SV5 = $false )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8394]) ).

thf(8421,plain,
    ! [SV5: $o] :
      ( ( ( ~ $false ) = $false )
      | ( SV5 = $false )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8394]) ).

thf(8422,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( $false = $false )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8395]) ).

thf(8423,plain,
    ! [SV5: $o] :
      ( ( ( ~ $false ) = $false )
      | ( $false = $false )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8395]) ).

thf(8424,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( SV5 = $false )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8396]) ).

thf(8425,plain,
    ! [SV5: $o] :
      ( ( ( ~ $false ) = $false )
      | ( SV5 = $false )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8396]) ).

thf(8426,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( $false = $false )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8397]) ).

thf(8427,plain,
    ! [SV5: $o] :
      ( ( ( ~ $false ) = $false )
      | ( $false = $false )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8397]) ).

thf(8428,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( SV5 = $false )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8398]) ).

thf(8429,plain,
    ! [SV5: $o] :
      ( ( ( ~ $false ) = $false )
      | ( SV5 = $false )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8398]) ).

thf(8430,plain,
    ! [SV5: $o] :
      ( ( ( ~ SV5 ) = $false )
      | ( $false = $false )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8399]) ).

thf(8431,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8399]) ).

thf(8432,plain,
    ( ( ( ~ $true ) = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8400]) ).

thf(8433,plain,
    ( ( ( ~ $false ) = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8400]) ).

thf(8434,plain,
    ( ( ( ~ $true ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8401]) ).

thf(8435,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8401]) ).

thf(8436,plain,
    ( ( ( ~ $true ) = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8402]) ).

thf(8437,plain,
    ( ( ( ~ $false ) = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8402]) ).

thf(8438,plain,
    ( ( ( ~ $true ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8403]) ).

thf(8439,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8403]) ).

thf(8440,plain,
    ( ( ( ~ $true ) = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8404]) ).

thf(8441,plain,
    ( ( ( ~ $false ) = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8404]) ).

thf(8442,plain,
    ( ( ( ~ $true ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8405]) ).

thf(8443,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8405]) ).

thf(8444,plain,
    ( ( ( ~ $true ) = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8406]) ).

thf(8445,plain,
    ( ( ( ~ $false ) = $false )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8406]) ).

thf(8446,plain,
    ( ( ( ~ $true ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8407]) ).

thf(8447,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8407]) ).

thf(8448,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8408]) ).

thf(8449,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8408]) ).

thf(8450,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8409]) ).

thf(8451,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8409]) ).

thf(8452,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8410]) ).

thf(8453,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8410]) ).

thf(8454,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8411]) ).

thf(8455,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8411]) ).

thf(8456,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8412]) ).

thf(8457,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8412]) ).

thf(8458,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8413]) ).

thf(8459,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8413]) ).

thf(8460,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8414]) ).

thf(8461,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8414]) ).

thf(8462,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8415]) ).

thf(8463,plain,
    ( ( ( ~ $false ) = $false )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_or_neg,[status(thm)],[8415]) ).

thf(8464,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( SV5 = $false )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8416]) ).

thf(8465,plain,
    ! [SV5: $o] :
      ( ( $false = $true )
      | ( SV5 = $false )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8417]) ).

thf(8466,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( $false = $false )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8418]) ).

thf(8467,plain,
    ! [SV5: $o] :
      ( ( $false = $true )
      | ( $false = $false )
      | ( SV5 = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8419]) ).

thf(8468,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( SV5 = $false )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8420]) ).

thf(8469,plain,
    ! [SV5: $o] :
      ( ( $false = $true )
      | ( SV5 = $false )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8421]) ).

thf(8470,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( $false = $false )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8422]) ).

thf(8471,plain,
    ! [SV5: $o] :
      ( ( $false = $true )
      | ( $false = $false )
      | ( SV5 = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8423]) ).

thf(8472,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( SV5 = $false )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8424]) ).

thf(8473,plain,
    ! [SV5: $o] :
      ( ( $false = $true )
      | ( SV5 = $false )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8425]) ).

thf(8474,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( $false = $false )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8426]) ).

thf(8475,plain,
    ! [SV5: $o] :
      ( ( $false = $true )
      | ( $false = $false )
      | ( $true = $false )
      | ( SV5 = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8427]) ).

thf(8476,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( SV5 = $false )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8428]) ).

thf(8477,plain,
    ! [SV5: $o] :
      ( ( $false = $true )
      | ( SV5 = $false )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8429]) ).

thf(8478,plain,
    ! [SV5: $o] :
      ( ( SV5 = $true )
      | ( $false = $false )
      | ( $true = $false )
      | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8430]) ).

thf(8479,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8431]) ).

thf(8480,plain,
    ( ( $true = $true )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8432]) ).

thf(8481,plain,
    ( ( $false = $true )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8433]) ).

thf(8482,plain,
    ( ( $true = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8434]) ).

thf(8483,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8435]) ).

thf(8484,plain,
    ( ( $true = $true )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8436]) ).

thf(8485,plain,
    ( ( $false = $true )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8437]) ).

thf(8486,plain,
    ( ( $true = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8438]) ).

thf(8487,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8439]) ).

thf(8488,plain,
    ( ( $true = $true )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8440]) ).

thf(8489,plain,
    ( ( $false = $true )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8441]) ).

thf(8490,plain,
    ( ( $true = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8442]) ).

thf(8491,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8443]) ).

thf(8492,plain,
    ( ( $true = $true )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8444]) ).

thf(8493,plain,
    ( ( $false = $true )
    | ( $true = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8445]) ).

thf(8494,plain,
    ( ( $true = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8446]) ).

thf(8495,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8447]) ).

thf(8496,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8448]) ).

thf(8497,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8449]) ).

thf(8498,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8450]) ).

thf(8499,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $false = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8451]) ).

thf(8500,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8452]) ).

thf(8501,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8453]) ).

thf(8502,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8454]) ).

thf(8503,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $false = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8455]) ).

thf(8504,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8456]) ).

thf(8505,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8457]) ).

thf(8506,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8458]) ).

thf(8507,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $false = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8459]) ).

thf(8508,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8460]) ).

thf(8509,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8461]) ).

thf(8510,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8462]) ).

thf(8511,plain,
    ( ( $false = $true )
    | ( $false = $false )
    | ( $true = $false )
    | ( $true = $true ) ),
    inference(extcnf_not_neg,[status(thm)],[8463]) ).

thf(8512,plain,
    $false = $true,
    inference(fo_atp_e,[status(thm)],[8166,8511,8510,8509,8508,8507,8506,8505,8504,8503,8502,8501,8500,8499,8498,8497,8496,8495,8494,8493,8492,8491,8490,8489,8488,8487,8486,8485,8484,8483,8482,8481,8480,8479,8478,8477,8476,8475,8474,8473,8472,8471,8470,8469,8468,8467,8466,8465,8464,8343,8342,8341,8340,8339,8337,8335,8333,8331,8330,8329,8328,8327,8325,8323,8321,8319,8318,8317,8316,8315,8313,8311,8309,8283,8263,8230,8229,8227,8224,8221,8218,8207,8196,8195,8190,8169,8167]) ).

thf(8513,plain,
    $false,
    inference(solved_all_splits,[solved_all_splits(join,[])],[8512]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP234^3 : TPTP v9.3.1. Bugfixed v9.2.1.
% 0.00/0.04  % Command  : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.17  % Computer : n018.cluster.edu
% 0.09/0.17  % Model    : x86_64 x86_64
% 0.09/0.17  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17  % Memory   : 8046.5625MB
% 0.09/0.17  % OS       : Linux 6.8.0-71-generic
% 0.09/0.17  % CPULimit : 300
% 0.09/0.17  % WCLimit  : 300
% 0.09/0.17  % DateTime : Tue Oct  6 11:25:38 UTC 2026
% 0.09/0.18  % CPUTime  : 
% 0.09/0.18  Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 32.15/6.60  .............................................................
% 32.15/6.60  
% 32.15/6.60   No.of.Axioms: 12
% 32.15/6.60  
% 32.15/6.60   Length.of.Defs: 0
% 32.15/6.60  
% 32.15/6.60   Contains.Choice.Funs: true
% 32.15/6.60  ..................................................................
% 32.15/6.60  
% 32.15/6.60  ********************************
% 32.15/6.60  *   All subproblems solved!    *
% 32.15/6.60  ********************************
% 32.15/6.60  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:12,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:8512,loop_count:0,foatp_calls:1,translation:fof_full)
% 32.15/6.60  
% 32.15/6.60  %**** Beginning of derivation protocol ****
% 32.15/6.60  % SZS output start CNFRefutation
% See solution above
% 32.15/6.61  
% 32.15/6.61  %**** End of derivation protocol ****
% 32.15/6.61  %**** no. of clauses in derivation: 376 ****
% 32.15/6.61  %**** clause counter: 8512 ****
% 32.15/6.61  
% 32.15/6.61  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:12,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:8512,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------