Leo-III---1.8.0.THM-Ref.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : SCT224_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39

% Computer : n001.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 : Sun Sep 27 08:27:35 AM UTC 2026

% Result   : Theorem 43.92s 27.70s
% Output   : Refutation 44.75s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    3
%            Number of leaves      :  111
% Syntax   : Number of formulae    :  224 (  81 unt;   0 typ;   0 def)
%            Number of atoms       : 2624 ( 207 equ;   0 cnn)
%            Maximal formula atoms :  138 (  11 avg)
%            Number of connectives : 10256 ( 135   ~;   8   |;  81   &;9737   @)
%                                         (  35 <=>; 260  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   29 (  12 avg)
%            Number of types       :    4 (   3 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :   44 (  42 usr;  15 con; 0-6 aty)
%            Number of variables   :  831 (   0   ^; 804   !;  27   ?; 831   :)

% Comments : 
%------------------------------------------------------------------------------
thf(arrow_411405190le_alt_type,type,
    arrow_411405190le_alt: $tType ).

thf(arrow_159774573e_indi_type,type,
    arrow_159774573e_indi: $tType ).

thf(bool_type,type,
    bool: $tType ).

thf(top_decl,type,
    top: 
      !>[TA: $tType] : $o ).

thf(arrow_1958449194le_IIA_decl,type,
    arrow_1958449194le_IIA: ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun ) ) > $o ).

thf(arrow_1985332922le_Lin_decl,type,
    arrow_1985332922le_Lin: bool @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ fun ) ).

thf(arrow_610318064e_Prof_decl,type,
    arrow_610318064e_Prof: bool @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun ) ).

thf(arrow_1158827142_above_decl,type,
    arrow_1158827142_above: ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) ) > arrow_411405190le_alt > arrow_411405190le_alt > ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) ) ).

thf(arrow_319942042_below_decl,type,
    arrow_319942042_below: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ fun ) ).

thf(arrow_987702531ctator_decl,type,
    arrow_987702531ctator: ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun ) ) > arrow_159774573e_indi > $o ).

thf(arrow_276188178_mkbot_decl,type,
    arrow_276188178_mkbot: ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) ) > arrow_411405190le_alt > ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) ) ).

thf(arrow_424895264_mktop_decl,type,
    arrow_424895264_mktop: ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) ) > arrow_411405190le_alt > ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) ) ).

thf(arrow_2069624013nimity_decl,type,
    arrow_2069624013nimity: ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun ) ) > $o ).

thf(combb_decl,type,
    combb: 
      !>[TA: $tType,TB: $tType,TC: $tType] : ( ( TB @ ( TC @ fun ) ) > ( TC @ ( TA @ fun ) ) > ( TB @ ( TA @ fun ) ) ) ).

thf(combc_decl,type,
    combc: 
      !>[TA: $tType,TB: $tType,TC: $tType] : ( ( TA @ ( TB @ fun ) @ ( TC @ fun ) ) > TB > ( TA @ ( TC @ fun ) ) ) ).

thf(combi_decl,type,
    combi: 
      !>[TA: $tType] : ( TA @ ( TA @ fun ) ) ).

thf(combk_decl,type,
    combk: 
      !>[TA: $tType,TB: $tType] : ( TB > ( TB @ ( TA @ fun ) ) ) ).

thf(pi_decl,type,
    pi: 
      !>[TA: $tType,TB: $tType] : ( ( bool @ ( TB @ fun ) ) > ( bool @ ( TA @ fun ) @ ( TB @ fun ) ) > ( bool @ ( TA @ ( TB @ fun ) @ fun ) ) ) ).

thf(distinct_decl,type,
    distinct: 
      !>[TA: $tType] : ( ( TA @ list ) > $o ) ).

thf(insert_decl,type,
    insert: 
      !>[TA: $tType] : ( TA > ( TA @ list ) > ( TA @ list ) ) ).

thf(cons_decl,type,
    cons: 
      !>[TA: $tType] : ( TA > ( TA @ list ) > ( TA @ list ) ) ).

thf(nil_decl,type,
    nil: 
      !>[TA: $tType] : ( TA @ list ) ).

thf(list_case_decl,type,
    list_case: 
      !>[TA: $tType,TB: $tType] : ( TB > ( TB @ ( TA @ list @ fun ) @ ( TA @ fun ) ) > ( TA @ list ) > TB ) ).

thf(splice_decl,type,
    splice: 
      !>[TA: $tType] : ( ( TA @ list ) > ( TA @ list ) > ( TA @ list ) ) ).

thf(top_top_decl,type,
    top_top: 
      !>[TA: $tType] : TA ).

thf(inv_imagep_decl,type,
    inv_imagep: 
      !>[TA: $tType,TB: $tType] : ( ( bool @ ( TB @ fun ) @ ( TB @ fun ) ) > ( TB @ ( TA @ fun ) ) > TA > TA > $o ) ).

thf(product_Pair_decl,type,
    product_Pair: 
      !>[TA: $tType,TB: $tType] : ( TB > TA > ( TA @ ( TB @ product_prod ) ) ) ).

thf(product_curry_decl,type,
    product_curry: 
      !>[TA: $tType,TB: $tType,TC: $tType] : ( ( TA @ ( TB @ ( TC @ product_prod ) @ fun ) ) > TC > TB > TA ) ).

thf(produc1605651328_split_decl,type,
    produc1605651328_split: 
      !>[TA: $tType,TB: $tType,TC: $tType] : ( ( TA @ ( TB @ fun ) @ ( TC @ fun ) ) > ( TB @ ( TC @ product_prod ) ) > TA ) ).

thf(product_prod_rec_decl,type,
    product_prod_rec: 
      !>[TA: $tType,TB: $tType,TC: $tType] : ( ( TA @ ( TB @ fun ) @ ( TC @ fun ) ) > ( TB @ ( TC @ product_prod ) ) > TA ) ).

thf(collect_decl,type,
    collect: 
      !>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > ( bool @ ( TA @ fun ) ) ) ).

thf(aa_decl,type,
    aa: 
      !>[TA: $tType,TB: $tType] : ( ( TA @ ( TB @ fun ) ) > TB > TA ) ).

thf(fFalse_decl,type,
    fFalse: bool ).

thf(fTrue_decl,type,
    fTrue: bool ).

thf(member_decl,type,
    member: 
      !>[TA: $tType] : ( TA > ( bool @ ( TA @ fun ) ) > $o ) ).

thf(pp_decl,type,
    pp: bool > $o ).

thf(f_decl,type,
    f: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun ) ).

thf(p_decl,type,
    p: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) ).

thf(p1_decl,type,
    p1: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) ).

thf(a_decl,type,
    a: arrow_411405190le_alt ).

thf(b_decl,type,
    b: arrow_411405190le_alt ).

thf(c_decl,type,
    c: arrow_411405190le_alt ).

thf(26,axiom,
    ! [TA: $tType,A: TA @ list] :
      ( ( A
       != ( TA @ nil ) )
     => ~ ! [B: TA,C: TA @ list] :
            ( A
           != ( C @ ( B @ ( TA @ cons ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_list_Oexhaust) ).

thf(193,plain,
    ! [TA: $tType,A: TA @ list] :
      ( ( A
       != ( TA @ nil ) )
     => ~ ! [B: TA,C: TA @ list] :
            ( A
           != ( C @ ( B @ ( TA @ cons ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).

thf(50,axiom,
    ! [TA: $tType,TB: $tType,A: bool @ ( TB @ fun ) @ ( TA @ fun ),B: TB @ ( TA @ fun ),C: bool @ ( TA @ fun )] :
      ( ! [D: TA] :
          ( ( C @ ( D @ ( TA @ member ) ) )
         => ( D @ ( A @ ( bool @ ( TB @ fun ) @ ( TA @ aa ) ) ) @ ( D @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ member ) ) ) )
     => ( A @ ( C @ ( TB @ ( TA @ pi ) ) ) @ ( B @ ( TB @ ( TA @ fun ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_Pi__I) ).

thf(311,plain,
    ! [TA: $tType,TB: $tType,A: bool @ ( TB @ fun ) @ ( TA @ fun ),B: TB @ ( TA @ fun ),C: bool @ ( TA @ fun )] :
      ( ! [D: TA] :
          ( ( C @ ( D @ ( TA @ member ) ) )
         => ( D @ ( A @ ( bool @ ( TB @ fun ) @ ( TA @ aa ) ) ) @ ( D @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ member ) ) ) )
     => ( A @ ( C @ ( TB @ ( TA @ pi ) ) ) @ ( B @ ( TB @ ( TA @ fun ) @ member ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).

thf(12,axiom,
    fTrue @ pp,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_pp_2_1_U) ).

thf(149,plain,
    fTrue @ pp,
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).

thf(13,axiom,
    ! [TA: $tType,A: TA @ list,B: TA,C: TA @ list,D: TA] :
      ( ( A @ ( B @ ( TA @ cons ) ) @ ( C @ ( D @ ( TA @ cons ) ) @ ( TA @ splice ) ) )
      = ( A @ ( C @ ( TA @ splice ) ) @ ( B @ ( TA @ cons ) ) @ ( D @ ( TA @ cons ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_splice_Osimps_I3_J) ).

thf(150,plain,
    ! [TA: $tType,A: TA @ list,B: TA,C: TA @ list,D: TA] :
      ( ( A @ ( B @ ( TA @ cons ) ) @ ( C @ ( D @ ( TA @ cons ) ) @ ( TA @ splice ) ) )
      = ( A @ ( C @ ( TA @ splice ) ) @ ( B @ ( TA @ cons ) ) @ ( D @ ( TA @ cons ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).

thf(10,axiom,
    ! [TA: $tType,A: TA] : ( TA @ nil @ ( A @ ( TA @ cons ) ) @ ( TA @ distinct ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_distinct__singleton) ).

thf(138,plain,
    ! [TA: $tType,A: TA] : ( TA @ nil @ ( A @ ( TA @ cons ) ) @ ( TA @ distinct ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).

thf(56,axiom,
    ! [TA: $tType,A: TA] :
      ( ( A @ ( TA @ combi @ ( TA @ ( TA @ aa ) ) ) )
      = A ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBI_1_1_U) ).

thf(333,plain,
    ! [TA: $tType,A: TA] :
      ( ( A @ ( TA @ combi @ ( TA @ ( TA @ aa ) ) ) )
      = A ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).

thf(39,axiom,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt] :
      ( ( B != A )
     => ? [C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
          ( ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
          & ( arrow_1985332922le_Lin @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_complete__Lin) ).

thf(249,plain,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt] :
      ( ( B != A )
     => ? [C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
          ( ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
          & ( arrow_1985332922le_Lin @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).

thf(68,axiom,
    ? [A: arrow_411405190le_alt,B: arrow_411405190le_alt,C: arrow_411405190le_alt] : ( arrow_411405190le_alt @ nil @ ( C @ ( arrow_411405190le_alt @ cons ) ) @ ( B @ ( arrow_411405190le_alt @ cons ) ) @ ( A @ ( arrow_411405190le_alt @ cons ) ) @ ( arrow_411405190le_alt @ distinct ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_alt3) ).

thf(408,plain,
    ? [A: arrow_411405190le_alt,B: arrow_411405190le_alt,C: arrow_411405190le_alt] : ( arrow_411405190le_alt @ nil @ ( C @ ( arrow_411405190le_alt @ cons ) ) @ ( B @ ( arrow_411405190le_alt @ cons ) ) @ ( A @ ( arrow_411405190le_alt @ cons ) ) @ ( arrow_411405190le_alt @ distinct ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).

thf(36,axiom,
    ! [A: arrow_159774573e_indi] :
      ( ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
    <=> ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7__096ALL_Ai_O_A_Ib_A_060_092_060_094bsub_062below_A_Ibelow_A_IP_Ai_J_Ac_Ab_J_Ab_Aa_092_060_094esub_062_Ac_J_A_061_A_Ib_A_060_092_060_094bsub_062below_A_Ibelow_A_Ibelow_A_IP_Ai_J_Ac_Ab_J_Ab_Aa_J_Aa_Ac_092_060_094esub_062_Aa_J_096) ).

thf(217,plain,
    ! [A: arrow_159774573e_indi] :
      ( ( ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
      & ( ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).

thf(49,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TC,C: TB @ ( TA @ fun ) @ ( TC @ fun )] :
      ( ( A @ ( B @ ( TA @ ( TC @ product_Pair ) ) ) @ ( C @ ( TB @ ( TA @ ( TC @ product_prod_rec ) ) ) ) )
      = ( A @ ( B @ ( C @ ( TB @ ( TA @ fun ) @ ( TC @ aa ) ) ) @ ( TB @ ( TA @ aa ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_prod_Orecs) ).

thf(308,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TC,C: TB @ ( TA @ fun ) @ ( TC @ fun )] :
      ( ( A @ ( B @ ( TA @ ( TC @ product_Pair ) ) ) @ ( C @ ( TB @ ( TA @ ( TC @ product_prod_rec ) ) ) ) )
      = ( A @ ( B @ ( C @ ( TB @ ( TA @ fun ) @ ( TC @ aa ) ) ) @ ( TB @ ( TA @ aa ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).

thf(3,axiom,
    ! [TA: $tType,A: TA @ list,B: TA] :
      ( ( A @ ( B @ ( TA @ cons ) ) )
     != ( TA @ nil ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_list_Osimps_I3_J) ).

thf(120,plain,
    ! [TA: $tType,A: TA @ list,B: TA] :
      ( ( A @ ( B @ ( TA @ cons ) ) )
     != ( TA @ nil ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).

thf(63,axiom,
    ! [TA: $tType,TB: $tType,A: TA,B: TB,C: TA,D: TB] :
      ( ( ( C @ ( D @ ( TA @ ( TB @ product_Pair ) ) ) )
        = ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) ) )
    <=> ( ( C = A )
        & ( D = B ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_Pair__eq) ).

thf(385,plain,
    ! [TA: $tType,TB: $tType,A: TA,B: TB,C: TA,D: TB] :
      ( ( ( ( C = A )
          & ( D = B ) )
       => ( ( C @ ( D @ ( TA @ ( TB @ product_Pair ) ) ) )
          = ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) ) ) )
      & ( ( ( C @ ( D @ ( TA @ ( TB @ product_Pair ) ) ) )
          = ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) ) )
       => ( ( C = A )
          & ( D = B ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).

thf(81,axiom,
    ! [TA: $tType,TB: $tType,A: TA,B: TB,C: TA,D: TB] :
      ( ( ( C @ ( D @ ( TA @ ( TB @ product_Pair ) ) ) )
        = ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) ) )
     => ~ ( ( D = B )
         => ( C != A ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_Pair__inject) ).

thf(472,plain,
    ! [TA: $tType,TB: $tType,A: TA,B: TB,C: TA,D: TB] :
      ( ( ( C @ ( D @ ( TA @ ( TB @ product_Pair ) ) ) )
        = ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) ) )
     => ~ ( ( D = B )
         => ( C != A ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).

thf(90,axiom,
    ! [A: arrow_159774573e_indi] :
      ( ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
    <=> ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2__096ALL_Ai_O_A_Ib_A_060_092_060_094bsub_062below_A_Ibelow_A_Ibelow_A_IP_Ai_J_Ac_Ab_J_Ab_Aa_J_Aa_Ac_092_060_094esub_062_Aa_J_A_061_A_Ia_A_060_092_060_094bsub_062P_Ai_092_060_094esub_062_Ab_J_096) ).

thf(538,plain,
    ! [A: arrow_159774573e_indi] :
      ( ( ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
      & ( ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).

thf(14,axiom,
    ! [TA: $tType,A: TA] :
      ( ( TA @ nil @ ( A @ ( TA @ insert ) ) )
      = ( TA @ nil @ ( A @ ( TA @ cons ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_insert__Nil) ).

thf(153,plain,
    ! [TA: $tType,A: TA] :
      ( ( TA @ nil @ ( A @ ( TA @ insert ) ) )
      = ( TA @ nil @ ( A @ ( TA @ cons ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).

thf(22,axiom,
    ~ ( fFalse @ pp ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_pp_1_1_U) ).

thf(185,plain,
    ~ ( fFalse @ pp ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).

thf(71,axiom,
    arrow_610318064e_Prof @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__096P_A_058_AProf_096) ).

thf(436,plain,
    arrow_610318064e_Prof @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).

thf(41,axiom,
    arrow_610318064e_Prof @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21__096_I_Fp_O_Abelow_A_IP_Ap_J_Ac_Ab_J_A_058_AProf_096) ).

thf(257,plain,
    arrow_610318064e_Prof @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).

thf(106,axiom,
    ! [TA: $tType,TB: $tType,A: TB @ ( TA @ fun ),B: TB @ ( TA @ fun )] :
      ( ! [C: TA] :
          ( ( C @ ( B @ ( TB @ ( TA @ aa ) ) ) )
          = ( C @ ( A @ ( TB @ ( TA @ aa ) ) ) ) )
     => ( B = A ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_ext) ).

thf(619,plain,
    ! [TA: $tType,TB: $tType,A: TB @ ( TA @ fun ),B: TB @ ( TA @ fun )] :
      ( ! [C: TA] :
          ( ( C @ ( B @ ( TB @ ( TA @ aa ) ) ) )
          = ( C @ ( A @ ( TB @ ( TA @ aa ) ) ) ) )
     => ( B = A ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).

thf(27,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TC,C: TB @ ( TA @ fun ) @ ( TC @ fun )] :
      ( ( A @ ( B @ ( TA @ ( TC @ product_Pair ) ) ) @ ( C @ ( TB @ ( TA @ ( TC @ produc1605651328_split ) ) ) ) )
      = ( A @ ( B @ ( C @ ( TB @ ( TA @ fun ) @ ( TC @ aa ) ) ) @ ( TB @ ( TA @ aa ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_internal__split__conv) ).

thf(196,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TC,C: TB @ ( TA @ fun ) @ ( TC @ fun )] :
      ( ( A @ ( B @ ( TA @ ( TC @ product_Pair ) ) ) @ ( C @ ( TB @ ( TA @ ( TC @ produc1605651328_split ) ) ) ) )
      = ( A @ ( B @ ( C @ ( TB @ ( TA @ fun ) @ ( TC @ aa ) ) ) @ ( TB @ ( TA @ aa ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).

thf(76,axiom,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
     => ( arrow_610318064e_Prof @ ( A @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combk ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_const__Lin__Prof) ).

thf(460,plain,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
     => ( arrow_610318064e_Prof @ ( A @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combk ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).

thf(95,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType,A: TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod ) @ ( TE @ product_prod )] :
      ~ ! [B: TE,C: TD,D: TC,E: TB,F: TA] :
          ( A
         != ( F @ ( E @ ( TA @ ( TB @ product_Pair ) ) ) @ ( D @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_Pair ) ) ) @ ( C @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_Pair ) ) ) @ ( B @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod ) @ ( TE @ product_Pair ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_prod__cases5) ).

thf(559,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType,A: TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod ) @ ( TE @ product_prod )] :
      ~ ! [B: TE,C: TD,D: TC,E: TB,F: TA] :
          ( A
         != ( F @ ( E @ ( TA @ ( TB @ product_Pair ) ) ) @ ( D @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_Pair ) ) ) @ ( C @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_Pair ) ) ) @ ( B @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod ) @ ( TE @ product_Pair ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).

thf(111,axiom,
    ! [TA: $tType,TB: $tType,A: TB,B: TA] :
      ( ( A @ ( B @ ( TB @ ( TA @ combk ) ) @ ( TA @ ( TB @ aa ) ) ) )
      = B ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_U) ).

thf(638,plain,
    ! [TA: $tType,TB: $tType,A: TB,B: TA] :
      ( ( A @ ( B @ ( TB @ ( TA @ combk ) ) @ ( TA @ ( TB @ aa ) ) ) )
      = B ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).

thf(74,axiom,
    ! [A: arrow_159774573e_indi] :
      ( ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
    <=> ( A @ ( p @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_iff) ).

thf(448,plain,
    ! [A: arrow_159774573e_indi] :
      ( ( ( A @ ( p @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
      & ( ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( A @ ( p @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).

thf(85,axiom,
    ! [TA: $tType,TB: $tType,A: TA,B: bool @ ( TB @ fun ) @ ( TA @ fun ),C: bool @ ( TA @ fun ),D: TB @ ( TA @ fun )] :
      ( ( B @ ( C @ ( TB @ ( TA @ pi ) ) ) @ ( D @ ( TB @ ( TA @ fun ) @ member ) ) )
     => ( ( C @ ( A @ ( TA @ member ) ) )
       => ( A @ ( B @ ( bool @ ( TB @ fun ) @ ( TA @ aa ) ) ) @ ( A @ ( D @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ member ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_Pi__mem) ).

thf(492,plain,
    ! [TA: $tType,TB: $tType,A: TA,B: bool @ ( TB @ fun ) @ ( TA @ fun ),C: bool @ ( TA @ fun ),D: TB @ ( TA @ fun )] :
      ( ( B @ ( C @ ( TB @ ( TA @ pi ) ) ) @ ( D @ ( TB @ ( TA @ fun ) @ member ) ) )
     => ( ( C @ ( A @ ( TA @ member ) ) )
       => ( A @ ( B @ ( bool @ ( TB @ fun ) @ ( TA @ aa ) ) ) @ ( A @ ( D @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).

thf(20,axiom,
    ! [TA: $tType,A: TA,B: TA @ list] :
      ( B
     != ( B @ ( A @ ( TA @ cons ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_not__Cons__self) ).

thf(179,plain,
    ! [TA: $tType,A: TA,B: TA @ list] :
      ( B
     != ( B @ ( A @ ( TA @ cons ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).

thf(33,axiom,
    ? [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] : ( arrow_1985332922le_Lin @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_linear__alt) ).

thf(211,plain,
    ? [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] : ( arrow_1985332922le_Lin @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).

thf(38,axiom,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ),B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ),C: arrow_411405190le_alt,D: arrow_411405190le_alt,E: arrow_411405190le_alt,F: arrow_411405190le_alt] :
      ( ( F != E )
     => ( ( D != C )
       => ( ( F != C )
         => ( ( E != D )
           => ( ( arrow_610318064e_Prof @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
             => ( ( arrow_610318064e_Prof @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
               => ( ! [G: arrow_159774573e_indi] :
                      ( ( G @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( F @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                    <=> ( G @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                 => ( ( B @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( F @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                   => ( A @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22__C1_C) ).

thf(238,plain,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ),B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ),C: arrow_411405190le_alt,D: arrow_411405190le_alt,E: arrow_411405190le_alt,F: arrow_411405190le_alt] :
      ( ( F != E )
     => ( ( D != C )
       => ( ( F != C )
         => ( ( E != D )
           => ( ( arrow_610318064e_Prof @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
             => ( ( arrow_610318064e_Prof @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
               => ( ! [G: arrow_159774573e_indi] :
                      ( ( ( G @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                       => ( G @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( F @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                      & ( ( G @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( F @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                       => ( G @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) )
                 => ( ( B @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( F @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                   => ( A @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).

thf(83,axiom,
    ! [A: arrow_159774573e_indi,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun )] :
      ( ( A @ ( B @ arrow_987702531ctator ) )
    <=> ! [C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
          ( ( arrow_610318064e_Prof @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
         => ( ( C @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) )
            = ( A @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_dictator__def) ).

thf(480,plain,
    ! [A: arrow_159774573e_indi,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun )] :
      ( ( ! [C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
            ( ( arrow_610318064e_Prof @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
           => ( ( C @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) )
              = ( A @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) ) ) )
       => ( A @ ( B @ arrow_987702531ctator ) ) )
      & ( ( A @ ( B @ arrow_987702531ctator ) )
       => ! [C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
            ( ( arrow_610318064e_Prof @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
           => ( ( C @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) )
              = ( A @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).

thf(47,axiom,
    ! [TA: $tType] :
      ( ( bool @ ( TA @ fun ) @ top_top )
      = ( fTrue @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_UNIV__def) ).

thf(280,plain,
    ! [TA: $tType] :
      ( ( bool @ ( TA @ fun ) @ top_top )
      = ( fTrue @ ( TA @ ( bool @ combk ) ) @ ( TA @ collect ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).

thf(110,axiom,
    ( ( p1 @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
  <=> ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_ab) ).

thf(634,plain,
    ( ( ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
     => ( p1 @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
    & ( ( p1 @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
     => ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).

thf(7,axiom,
    f @ arrow_2069624013nimity,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_u) ).

thf(132,plain,
    f @ arrow_2069624013nimity,
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).

thf(65,axiom,
    ! [TA: $tType,TB: $tType,A: bool @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ! [B: TA @ ( TB @ product_prod )] : ( B @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp )
    <=> ! [B: TB,C: TA] : ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_split__paired__All) ).

thf(396,plain,
    ! [TA: $tType,TB: $tType,A: bool @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ( ! [B: TB,C: TA] : ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp )
       => ! [B: TA @ ( TB @ product_prod )] : ( B @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp ) )
      & ( ! [B: TA @ ( TB @ product_prod )] : ( B @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp )
       => ! [B: TB,C: TA] : ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).

thf(8,axiom,
    ! [TA: $tType] : ( TA @ nil @ ( TA @ distinct ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_distinct_Osimps_I1_J) ).

thf(133,plain,
    ! [TA: $tType] : ( TA @ nil @ ( TA @ distinct ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).

thf(61,axiom,
    ! [TA: $tType,TB: $tType,A: TA @ ( TB @ product_prod )] :
      ~ ! [B: TB,C: TA] :
          ( A
         != ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_PairE) ).

thf(380,plain,
    ! [TA: $tType,TB: $tType,A: TA @ ( TB @ product_prod )] :
      ~ ! [B: TB,C: TA] :
          ( A
         != ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).

thf(88,axiom,
    ! [TA: $tType,TB: $tType,A: bool @ ( TA @ fun )] :
      ( ( bool @ ( TB @ fun ) @ top_top @ ( TA @ ( bool @ ( TB @ fun ) @ combk ) ) @ ( A @ ( TB @ ( TA @ pi ) ) ) )
      = ( bool @ ( TB @ ( TA @ fun ) @ fun ) @ top_top ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_Pi__UNIV) ).

thf(512,plain,
    ! [TA: $tType,TB: $tType,A: bool @ ( TA @ fun )] :
      ( ( bool @ ( TB @ fun ) @ top_top @ ( TA @ ( bool @ ( TB @ fun ) @ combk ) ) @ ( A @ ( TB @ ( TA @ pi ) ) ) )
      = ( bool @ ( TB @ ( TA @ fun ) @ fun ) @ top_top ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).

thf(92,axiom,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt,C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
     => ( ( B != A )
       => ( ~ ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
        <=> ( C @ ( B @ ( A @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_notin__Lin__iff) ).

thf(546,plain,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt,C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
     => ( ( B != A )
       => ( ( ( C @ ( B @ ( A @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
           => ~ ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
          & ( ~ ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
           => ( C @ ( B @ ( A @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).

thf(17,axiom,
    ! [TA: $tType,A: TA @ list,B: TA,C: TA @ list,D: TA] :
      ( ( ( C @ ( D @ ( TA @ cons ) ) )
        = ( A @ ( B @ ( TA @ cons ) ) ) )
    <=> ( ( C = A )
        & ( D = B ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_list_Oinject) ).

thf(160,plain,
    ! [TA: $tType,A: TA @ list,B: TA,C: TA @ list,D: TA] :
      ( ( ( ( C = A )
          & ( D = B ) )
       => ( ( C @ ( D @ ( TA @ cons ) ) )
          = ( A @ ( B @ ( TA @ cons ) ) ) ) )
      & ( ( ( C @ ( D @ ( TA @ cons ) ) )
          = ( A @ ( B @ ( TA @ cons ) ) ) )
       => ( ( C = A )
          & ( D = B ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).

thf(25,axiom,
    f @ arrow_1958449194le_IIA,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_assms_I3_J) ).

thf(192,plain,
    f @ arrow_1958449194le_IIA,
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).

thf(45,axiom,
    ! [TA: $tType,TB: $tType,A: TA,B: TB,C: bool @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( C @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp )
     => ( A @ ( B @ ( C @ ( bool @ ( TA @ ( TB @ product_curry ) ) ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_curryI) ).

thf(275,plain,
    ! [TA: $tType,TB: $tType,A: TA,B: TB,C: bool @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( C @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp )
     => ( A @ ( B @ ( C @ ( bool @ ( TA @ ( TB @ product_curry ) ) ) ) ) @ pp ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).

thf(18,axiom,
    ! [TA: $tType,A: TA @ list] :
      ( ( A
       != ( TA @ nil ) )
    <=> ? [B: TA,C: TA @ list] :
          ( A
          = ( C @ ( B @ ( TA @ cons ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_neq__Nil__conv) ).

thf(169,plain,
    ! [TA: $tType,A: TA @ list] :
      ( ( ? [B: TA,C: TA @ list] :
            ( A
            = ( C @ ( B @ ( TA @ cons ) ) ) )
       => ( A
         != ( TA @ nil ) ) )
      & ( ( A
         != ( TA @ nil ) )
       => ? [B: TA,C: TA @ list] :
            ( A
            = ( C @ ( B @ ( TA @ cons ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).

thf(101,axiom,
    arrow_610318064e_Prof @ ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16__096_I_Fp_O_Abelow_A_Ibelow_A_Ibelow_A_IP_Ap_J_Ac_Ab_J_Ab_Aa_J_Aa_Ac_J_A_058_AProf_096) ).

thf(610,plain,
    arrow_610318064e_Prof @ ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).

thf(15,axiom,
    ! [TA: $tType,A: TA @ list,B: TA] :
      ( ( TA @ nil @ ( A @ ( B @ ( TA @ cons ) ) @ ( TA @ splice ) ) )
      = ( A @ ( B @ ( TA @ cons ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_splice_Osimps_I2_J) ).

thf(156,plain,
    ! [TA: $tType,A: TA @ list,B: TA] :
      ( ( TA @ nil @ ( A @ ( B @ ( TA @ cons ) ) @ ( TA @ splice ) ) )
      = ( A @ ( B @ ( TA @ cons ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).

thf(104,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType,A: TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ),B: bool @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ fun )] :
      ( ! [C: TA,D: TB,E: TC,F: TD,G: TE] : ( G @ ( F @ ( TE @ ( TD @ product_Pair ) ) ) @ ( E @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_Pair ) ) ) @ ( D @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_Pair ) ) ) @ ( C @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_Pair ) ) ) @ ( B @ ( bool @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp )
     => ( A @ ( B @ ( bool @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_prod__induct5) ).

thf(615,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType,A: TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ),B: bool @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ fun )] :
      ( ! [C: TA,D: TB,E: TC,F: TD,G: TE] : ( G @ ( F @ ( TE @ ( TD @ product_Pair ) ) ) @ ( E @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_Pair ) ) ) @ ( D @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_Pair ) ) ) @ ( C @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_Pair ) ) ) @ ( B @ ( bool @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp )
     => ( A @ ( B @ ( bool @ ( TE @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).

thf(107,axiom,
    ! [TA: $tType,TB: $tType,A: TA,B: TB,C: bool @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ( A @ ( B @ ( C @ ( bool @ ( TA @ ( TB @ product_curry ) ) ) ) ) @ pp )
     => ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( C @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_curryE) ).

thf(622,plain,
    ! [TA: $tType,TB: $tType,A: TA,B: TB,C: bool @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ( A @ ( B @ ( C @ ( bool @ ( TA @ ( TB @ product_curry ) ) ) ) ) @ pp )
     => ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( C @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).

thf(89,axiom,
    ! [A: arrow_411405190le_alt,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),C: arrow_411405190le_alt,D: arrow_411405190le_alt] :
      ( ( A @ ( B @ arrow_276188178_mkbot ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
    <=> ( ( ( D != A )
         => ( B @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
        & ( ( D = A )
         => ( D != C ) )
        & ( C != A ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_in__mkbot) ).

thf(515,plain,
    ! [A: arrow_411405190le_alt,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),C: arrow_411405190le_alt,D: arrow_411405190le_alt] :
      ( ( ( ( ( D != A )
           => ( B @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
          & ( ( D = A )
           => ( D != C ) )
          & ( C != A ) )
       => ( A @ ( B @ arrow_276188178_mkbot ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
      & ( ( A @ ( B @ arrow_276188178_mkbot ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( ( ( D != A )
           => ( B @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
          & ( ( D = A )
           => ( D != C ) )
          & ( C != A ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).

thf(6,axiom,
    ! [TA: $tType,A: TA @ list] :
      ( ( TA @ nil @ ( A @ ( TA @ splice ) ) )
      = A ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_splice__Nil2) ).

thf(129,plain,
    ! [TA: $tType,A: TA @ list] :
      ( ( TA @ nil @ ( A @ ( TA @ splice ) ) )
      = A ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).

thf(96,axiom,
    ! [TA: $tType,A: TA] : ( bool @ ( TA @ fun ) @ top_top @ ( A @ ( TA @ member ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_UNIV__I) ).

thf(562,plain,
    ! [TA: $tType,A: TA] : ( bool @ ( TA @ fun ) @ top_top @ ( A @ ( TA @ member ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).

thf(19,axiom,
    ! [TA: $tType,TB: $tType,A: TA @ ( TB @ list @ fun ) @ ( TB @ fun ),B: TA] :
      ( ( TB @ nil @ ( A @ ( B @ ( TB @ ( TA @ list_case ) ) ) ) )
      = B ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_list_Osimps_I4_J) ).

thf(176,plain,
    ! [TA: $tType,TB: $tType,A: TA @ ( TB @ list @ fun ) @ ( TB @ fun ),B: TA] :
      ( ( TB @ nil @ ( A @ ( B @ ( TB @ ( TA @ list_case ) ) ) ) )
      = B ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).

thf(112,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TB,C: TC @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ( A @ ( B @ ( C @ ( TC @ ( TA @ ( TB @ product_curry ) ) ) ) ) )
      = ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( C @ ( TC @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_curry__conv) ).

thf(641,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TB,C: TC @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ( A @ ( B @ ( C @ ( TC @ ( TA @ ( TB @ product_curry ) ) ) ) ) )
      = ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( C @ ( TC @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).

thf(102,axiom,
    arrow_411405190le_alt @ nil @ ( c @ ( arrow_411405190le_alt @ cons ) ) @ ( b @ ( arrow_411405190le_alt @ cons ) ) @ ( a @ ( arrow_411405190le_alt @ cons ) ) @ ( arrow_411405190le_alt @ distinct ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_dist) ).

thf(611,plain,
    arrow_411405190le_alt @ nil @ ( c @ ( arrow_411405190le_alt @ cons ) ) @ ( b @ ( arrow_411405190le_alt @ cons ) ) @ ( a @ ( arrow_411405190le_alt @ cons ) ) @ ( arrow_411405190le_alt @ distinct ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).

thf(16,axiom,
    fTrue @ pp,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fTrue_1_1_U) ).

thf(159,plain,
    fTrue @ pp,
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).

thf(99,axiom,
    ! [TA: $tType,A: bool @ ( TA @ fun )] :
      ( ! [B: TA] : ( A @ ( B @ ( TA @ member ) ) )
     => ( ( bool @ ( TA @ fun ) @ top_top )
        = A ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_UNIV__eq__I) ).

thf(604,plain,
    ! [TA: $tType,A: bool @ ( TA @ fun )] :
      ( ! [B: TA] : ( A @ ( B @ ( TA @ member ) ) )
     => ( ( bool @ ( TA @ fun ) @ top_top )
        = A ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).

thf(23,axiom,
    ! [TA: $tType,A: TA @ list,B: TA] :
      ( ( TA @ nil )
     != ( A @ ( B @ ( TA @ cons ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_list_Osimps_I2_J) ).

thf(187,plain,
    ! [TA: $tType,A: TA @ list,B: TA] :
      ( ( TA @ nil )
     != ( A @ ( B @ ( TA @ cons ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).

thf(1,conjecture,
    ! [A: arrow_159774573e_indi] :
      ( ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
    <=> ( A @ ( p @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

thf(2,negated_conjecture,
    ~ ! [A: arrow_159774573e_indi] :
        ( ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
      <=> ( A @ ( p @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ),
    inference(neg_conjecture,[status(cth)],[1]) ).

thf(113,plain,
    ~ ! [A: arrow_159774573e_indi] :
        ( ( ( A @ ( p @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
         => ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
        & ( ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
         => ( A @ ( p @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).

thf(60,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,A: TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod )] :
      ~ ! [B: TD,C: TC,D: TB,E: TA] :
          ( A
         != ( E @ ( D @ ( TA @ ( TB @ product_Pair ) ) ) @ ( C @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_Pair ) ) ) @ ( B @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_Pair ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_prod__cases4) ).

thf(377,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,A: TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod )] :
      ~ ! [B: TD,C: TC,D: TB,E: TA] :
          ( A
         != ( E @ ( D @ ( TA @ ( TB @ product_Pair ) ) ) @ ( C @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_Pair ) ) ) @ ( B @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_Pair ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).

thf(86,axiom,
    ! [TA: $tType,A: TA] : ( A @ ( bool @ ( TA @ fun ) @ top_top @ ( bool @ ( TA @ aa ) ) ) @ pp ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_top1I) ).

thf(494,plain,
    ! [TA: $tType,A: TA] : ( A @ ( bool @ ( TA @ fun ) @ top_top @ ( bool @ ( TA @ aa ) ) ) @ pp ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).

thf(93,axiom,
    ~ ! [A: arrow_411405190le_alt] :
        ~ ( arrow_411405190le_alt @ nil @ ( A @ ( arrow_411405190le_alt @ cons ) ) @ ( b @ ( arrow_411405190le_alt @ cons ) ) @ ( a @ ( arrow_411405190le_alt @ cons ) ) @ ( arrow_411405190le_alt @ distinct ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71__096_B_Bthesis_O_A_I_B_Bc_O_Adistinct_A_091a_M_Ab_M_Ac_093_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096) ).

thf(552,plain,
    ~ ! [A: arrow_411405190le_alt] :
        ~ ( arrow_411405190le_alt @ nil @ ( A @ ( arrow_411405190le_alt @ cons ) ) @ ( b @ ( arrow_411405190le_alt @ cons ) ) @ ( a @ ( arrow_411405190le_alt @ cons ) ) @ ( arrow_411405190le_alt @ distinct ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).

thf(53,axiom,
    ! [TA: $tType,TB: $tType,A: TA @ ( TB @ product_prod )] :
      ~ ! [B: TB,C: TA] :
          ( A
         != ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_prod_Oexhaust) ).

thf(323,plain,
    ! [TA: $tType,TB: $tType,A: TA @ ( TB @ product_prod )] :
      ~ ! [B: TB,C: TA] :
          ( A
         != ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).

thf(11,axiom,
    ! [TA: $tType,A: TA @ list,B: TA,C: TA] :
      ( ( A @ ( B @ ( TA @ cons ) ) @ ( C @ ( TA @ cons ) ) @ ( TA @ distinct ) )
    <=> ( ( A @ ( B @ ( TA @ cons ) ) @ ( TA @ distinct ) )
        & ( A @ ( C @ ( TA @ cons ) ) @ ( TA @ distinct ) )
        & ( C != B ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_distinct__length__2__or__more) ).

thf(140,plain,
    ! [TA: $tType,A: TA @ list,B: TA,C: TA] :
      ( ( ( ( A @ ( B @ ( TA @ cons ) ) @ ( TA @ distinct ) )
          & ( A @ ( C @ ( TA @ cons ) ) @ ( TA @ distinct ) )
          & ( C != B ) )
       => ( A @ ( B @ ( TA @ cons ) ) @ ( C @ ( TA @ cons ) ) @ ( TA @ distinct ) ) )
      & ( ( A @ ( B @ ( TA @ cons ) ) @ ( C @ ( TA @ cons ) ) @ ( TA @ distinct ) )
       => ( ( A @ ( B @ ( TA @ cons ) ) @ ( TA @ distinct ) )
          & ( A @ ( C @ ( TA @ cons ) ) @ ( TA @ distinct ) )
          & ( C != B ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).

thf(34,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TC @ ( TB @ product_prod ) @ ( TA @ product_prod ),B: bool @ ( TC @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ fun )] :
      ( ! [C: TA,D: TB,E: TC] : ( E @ ( D @ ( TC @ ( TB @ product_Pair ) ) ) @ ( C @ ( TC @ ( TB @ product_prod ) @ ( TA @ product_Pair ) ) ) @ ( B @ ( bool @ ( TC @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp )
     => ( A @ ( B @ ( bool @ ( TC @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_prod__induct3) ).

thf(213,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TC @ ( TB @ product_prod ) @ ( TA @ product_prod ),B: bool @ ( TC @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ fun )] :
      ( ! [C: TA,D: TB,E: TC] : ( E @ ( D @ ( TC @ ( TB @ product_Pair ) ) ) @ ( C @ ( TC @ ( TB @ product_prod ) @ ( TA @ product_Pair ) ) ) @ ( B @ ( bool @ ( TC @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp )
     => ( A @ ( B @ ( bool @ ( TC @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).

thf(109,axiom,
    ! [TA: $tType,TB: $tType,A: bool @ ( TB @ fun ) @ ( TA @ fun ),B: TB @ ( TA @ fun ),C: TB @ ( TA @ fun ),D: bool @ ( TA @ fun )] :
      ( ! [E: TA] :
          ( ( D @ ( E @ ( TA @ member ) ) )
         => ( ( E @ ( C @ ( TB @ ( TA @ aa ) ) ) )
            = ( E @ ( B @ ( TB @ ( TA @ aa ) ) ) ) ) )
     => ( ( A @ ( D @ ( TB @ ( TA @ pi ) ) ) @ ( C @ ( TB @ ( TA @ fun ) @ member ) ) )
      <=> ( A @ ( D @ ( TB @ ( TA @ pi ) ) ) @ ( B @ ( TB @ ( TA @ fun ) @ member ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_Pi__cong) ).

thf(626,plain,
    ! [TA: $tType,TB: $tType,A: bool @ ( TB @ fun ) @ ( TA @ fun ),B: TB @ ( TA @ fun ),C: TB @ ( TA @ fun ),D: bool @ ( TA @ fun )] :
      ( ! [E: TA] :
          ( ( D @ ( E @ ( TA @ member ) ) )
         => ( ( E @ ( C @ ( TB @ ( TA @ aa ) ) ) )
            = ( E @ ( B @ ( TB @ ( TA @ aa ) ) ) ) ) )
     => ( ( ( A @ ( D @ ( TB @ ( TA @ pi ) ) ) @ ( B @ ( TB @ ( TA @ fun ) @ member ) ) )
         => ( A @ ( D @ ( TB @ ( TA @ pi ) ) ) @ ( C @ ( TB @ ( TA @ fun ) @ member ) ) ) )
        & ( ( A @ ( D @ ( TB @ ( TA @ pi ) ) ) @ ( C @ ( TB @ ( TA @ fun ) @ member ) ) )
         => ( A @ ( D @ ( TB @ ( TA @ pi ) ) ) @ ( B @ ( TB @ ( TA @ fun ) @ member ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).

thf(77,axiom,
    ! [TA: $tType,TB: $tType,A: TA,B: TB,C: bool @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ( A @ ( B @ ( C @ ( bool @ ( TA @ ( TB @ product_curry ) ) ) ) ) @ pp )
     => ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( C @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_curryD) ).

thf(462,plain,
    ! [TA: $tType,TB: $tType,A: TA,B: TB,C: bool @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ( A @ ( B @ ( C @ ( bool @ ( TA @ ( TB @ product_curry ) ) ) ) ) @ pp )
     => ( A @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( C @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).

thf(37,axiom,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ),B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ),C: arrow_411405190le_alt,D: arrow_411405190le_alt,E: arrow_411405190le_alt,F: arrow_411405190le_alt] :
      ( ( F != E )
     => ( ( D != C )
       => ( ( F != C )
         => ( ( E != D )
           => ( ( arrow_610318064e_Prof @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
             => ( ( arrow_610318064e_Prof @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
               => ( ! [G: arrow_159774573e_indi] :
                      ( ( G @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( F @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                    <=> ( G @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                 => ( ( B @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( F @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                  <=> ( A @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23__C2_C) ).

thf(223,plain,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ),B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ),C: arrow_411405190le_alt,D: arrow_411405190le_alt,E: arrow_411405190le_alt,F: arrow_411405190le_alt] :
      ( ( F != E )
     => ( ( D != C )
       => ( ( F != C )
         => ( ( E != D )
           => ( ( arrow_610318064e_Prof @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
             => ( ( arrow_610318064e_Prof @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
               => ( ! [G: arrow_159774573e_indi] :
                      ( ( ( G @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                       => ( G @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( F @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                      & ( ( G @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( F @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                       => ( G @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) )
                 => ( ( ( A @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                     => ( B @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( F @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                    & ( ( B @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( F @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                     => ( A @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) ) ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).

thf(64,axiom,
    ! [A: arrow_411405190le_alt,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
     => ( arrow_1985332922le_Lin @ ( A @ ( B @ arrow_276188178_mkbot ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_mkbot__Lin) ).

thf(394,plain,
    ! [A: arrow_411405190le_alt,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
     => ( arrow_1985332922le_Lin @ ( A @ ( B @ arrow_276188178_mkbot ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).

thf(9,axiom,
    ! [A: bool] :
      ( ( A = fFalse )
      | ( A = fTrue ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fTrue_1_1_T) ).

thf(135,plain,
    ! [A: bool] :
      ( ( A = fFalse )
      | ( A = fTrue ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).

thf(84,axiom,
    ! [A: arrow_411405190le_alt,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
     => ( arrow_1985332922le_Lin @ ( A @ ( B @ arrow_424895264_mktop ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_mktop__Lin) ).

thf(490,plain,
    ! [A: arrow_411405190le_alt,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
     => ( arrow_1985332922le_Lin @ ( A @ ( B @ arrow_424895264_mktop ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).

thf(40,axiom,
    ( arrow_610318064e_Prof
    = ( arrow_1985332922le_Lin @ ( arrow_159774573e_indi @ ( bool @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ fun ) @ combk ) ) @ ( bool @ ( arrow_159774573e_indi @ fun ) @ top_top @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ pi ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_Prof__def) ).

thf(255,plain,
    ( arrow_610318064e_Prof
    = ( arrow_1985332922le_Lin @ ( arrow_159774573e_indi @ ( bool @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ fun ) @ combk ) ) @ ( bool @ ( arrow_159774573e_indi @ fun ) @ top_top @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ pi ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).

thf(105,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,A: TD @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ),B: bool @ ( TD @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ fun )] :
      ( ! [C: TA,D: TB,E: TC,F: TD] : ( F @ ( E @ ( TD @ ( TC @ product_Pair ) ) ) @ ( D @ ( TD @ ( TC @ product_prod ) @ ( TB @ product_Pair ) ) ) @ ( C @ ( TD @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_Pair ) ) ) @ ( B @ ( bool @ ( TD @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp )
     => ( A @ ( B @ ( bool @ ( TD @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_prod__induct4) ).

thf(617,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,A: TD @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ),B: bool @ ( TD @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ fun )] :
      ( ! [C: TA,D: TB,E: TC,F: TD] : ( F @ ( E @ ( TD @ ( TC @ product_Pair ) ) ) @ ( D @ ( TD @ ( TC @ product_prod ) @ ( TB @ product_Pair ) ) ) @ ( C @ ( TD @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_Pair ) ) ) @ ( B @ ( bool @ ( TD @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp )
     => ( A @ ( B @ ( bool @ ( TD @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).

thf(4,axiom,
    ! [TA: $tType,A: TA @ list] :
      ( ( A @ ( TA @ nil @ ( TA @ splice ) ) )
      = A ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_splice_Osimps_I1_J) ).

thf(123,plain,
    ! [TA: $tType,A: TA @ list] :
      ( ( A @ ( TA @ nil @ ( TA @ splice ) ) )
      = A ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).

thf(28,axiom,
    bool @ top,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_HOL_Obool___Orderings_Otop) ).

thf(199,plain,
    bool @ top,
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).

thf(21,axiom,
    ! [TA: $tType,A: TA @ list,B: TA] :
      ( ( A @ ( B @ ( TA @ cons ) ) )
     != A ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_not__Cons__self2) ).

thf(182,plain,
    ! [TA: $tType,A: TA @ list,B: TA] :
      ( ( A @ ( B @ ( TA @ cons ) ) )
     != A ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).

thf(73,axiom,
    ! [A: arrow_159774573e_indi,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ ( bool @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ fun ) @ combk ) ) @ ( arrow_610318064e_Prof @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ pi ) ) ) @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun ) @ member ) ) )
     => ( ! [C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
            ( ( arrow_610318064e_Prof @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
           => ! [D: arrow_411405190le_alt,E: arrow_411405190le_alt] :
                ( ( D != E )
               => ( ( A @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                 => ( C @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) )
       => ( A @ ( B @ arrow_987702531ctator ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_dictatorI) ).

thf(441,plain,
    ! [A: arrow_159774573e_indi,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ ( bool @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ fun ) @ combk ) ) @ ( arrow_610318064e_Prof @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ pi ) ) ) @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun ) @ member ) ) )
     => ( ! [C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
            ( ( arrow_610318064e_Prof @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
           => ! [D: arrow_411405190le_alt,E: arrow_411405190le_alt] :
                ( ( D != E )
               => ( ( A @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                 => ( C @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) )
       => ( A @ ( B @ arrow_987702531ctator ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).

thf(58,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TB @ ( TA @ fun ),C: TC @ ( TB @ fun )] :
      ( ( A @ ( B @ ( C @ ( TA @ ( TC @ ( TB @ combb ) ) ) ) @ ( TC @ ( TA @ aa ) ) ) )
      = ( A @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( C @ ( TC @ ( TB @ aa ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBB_1_1_U) ).

thf(338,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TA,B: TB @ ( TA @ fun ),C: TC @ ( TB @ fun )] :
      ( ( A @ ( B @ ( C @ ( TA @ ( TC @ ( TB @ combb ) ) ) ) @ ( TC @ ( TA @ aa ) ) ) )
      = ( A @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( C @ ( TC @ ( TB @ aa ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).

thf(91,axiom,
    ! [TA: $tType,A: bool @ ( TA @ fun )] : ( A @ ( TA @ ( bool @ ( TA @ fun ) @ combk ) ) @ ( A @ ( TA @ ( TA @ pi ) ) ) @ ( TA @ combi @ ( TA @ ( TA @ fun ) @ member ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_funcset__id) ).

thf(544,plain,
    ! [TA: $tType,A: bool @ ( TA @ fun )] : ( A @ ( TA @ ( bool @ ( TA @ fun ) @ combk ) ) @ ( A @ ( TA @ ( TA @ pi ) ) ) @ ( TA @ combi @ ( TA @ ( TA @ fun ) @ member ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).

thf(57,axiom,
    ! [TA: $tType,A: TA] : ( bool @ ( TA @ fun ) @ top_top @ ( A @ ( TA @ member ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_iso__tuple__UNIV__I) ).

thf(336,plain,
    ! [TA: $tType,A: TA] : ( bool @ ( TA @ fun ) @ top_top @ ( A @ ( TA @ member ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).

thf(103,axiom,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt] :
      ( ( B != A )
     => ? [C: arrow_411405190le_alt] : ( arrow_411405190le_alt @ nil @ ( C @ ( arrow_411405190le_alt @ cons ) ) @ ( A @ ( arrow_411405190le_alt @ cons ) ) @ ( B @ ( arrow_411405190le_alt @ cons ) ) @ ( arrow_411405190le_alt @ distinct ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_third__alt) ).

thf(612,plain,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt] :
      ( ( B != A )
     => ? [C: arrow_411405190le_alt] : ( arrow_411405190le_alt @ nil @ ( C @ ( arrow_411405190le_alt @ cons ) ) @ ( A @ ( arrow_411405190le_alt @ cons ) ) @ ( B @ ( arrow_411405190le_alt @ cons ) ) @ ( arrow_411405190le_alt @ distinct ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).

thf(79,axiom,
    ! [TA: $tType,TB: $tType,A: TB @ ( TA @ fun ),B: bool @ ( TB @ fun ) @ ( TB @ fun ),C: TA,D: TA] :
      ( ( D @ ( C @ ( A @ ( B @ ( TA @ ( TB @ inv_imagep ) ) ) ) ) )
    <=> ( D @ ( A @ ( TB @ ( TA @ aa ) ) ) @ ( C @ ( A @ ( TB @ ( TA @ aa ) ) ) @ ( B @ ( bool @ ( TB @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( TB @ aa ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_inv__imagep__def) ).

thf(465,plain,
    ! [TA: $tType,TB: $tType,A: TB @ ( TA @ fun ),B: bool @ ( TB @ fun ) @ ( TB @ fun ),C: TA,D: TA] :
      ( ( ( D @ ( A @ ( TB @ ( TA @ aa ) ) ) @ ( C @ ( A @ ( TB @ ( TA @ aa ) ) ) @ ( B @ ( bool @ ( TB @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( TB @ aa ) ) ) @ pp )
       => ( D @ ( C @ ( A @ ( B @ ( TA @ ( TB @ inv_imagep ) ) ) ) ) ) )
      & ( ( D @ ( C @ ( A @ ( B @ ( TA @ ( TB @ inv_imagep ) ) ) ) ) )
       => ( D @ ( A @ ( TB @ ( TA @ aa ) ) ) @ ( C @ ( A @ ( TB @ ( TA @ aa ) ) ) @ ( B @ ( bool @ ( TB @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( TB @ aa ) ) ) @ pp ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).

thf(94,axiom,
    ! [TA: $tType,TB: $tType] :
      ( ( TA @ top )
     => ! [A: TB] :
          ( ( A @ ( TA @ ( TB @ fun ) @ top_top @ ( TA @ ( TB @ aa ) ) ) )
          = ( TA @ top_top ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_top__apply) ).

thf(556,plain,
    ! [TA: $tType,TB: $tType] :
      ( ( TA @ top )
     => ! [A: TB] :
          ( ( A @ ( TA @ ( TB @ fun ) @ top_top @ ( TA @ ( TB @ aa ) ) ) )
          = ( TA @ top_top ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).

thf(30,axiom,
    ! [TA: $tType,TB: $tType,A: bool @ ( TA @ fun ),B: TA @ ( TB @ fun ),C: bool @ ( TB @ fun )] :
      ( ! [D: TB] :
          ( ( C @ ( D @ ( TB @ member ) ) )
         => ( A @ ( D @ ( B @ ( TA @ ( TB @ aa ) ) ) @ ( TA @ member ) ) ) )
     => ( A @ ( TB @ ( bool @ ( TA @ fun ) @ combk ) ) @ ( C @ ( TA @ ( TB @ pi ) ) ) @ ( B @ ( TA @ ( TB @ fun ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_funcsetI) ).

thf(203,plain,
    ! [TA: $tType,TB: $tType,A: bool @ ( TA @ fun ),B: TA @ ( TB @ fun ),C: bool @ ( TB @ fun )] :
      ( ! [D: TB] :
          ( ( C @ ( D @ ( TB @ member ) ) )
         => ( A @ ( D @ ( B @ ( TA @ ( TB @ aa ) ) ) @ ( TA @ member ) ) ) )
     => ( A @ ( TB @ ( bool @ ( TA @ fun ) @ combk ) ) @ ( C @ ( TA @ ( TB @ pi ) ) ) @ ( B @ ( TA @ ( TB @ fun ) @ member ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).

thf(52,axiom,
    ( ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
  <=> ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_ac) ).

thf(319,plain,
    ( ( ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
     => ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
    & ( ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
     => ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).

thf(42,axiom,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun )] :
      ( ( A @ arrow_2069624013nimity )
    <=> ! [B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
          ( ( arrow_610318064e_Prof @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
         => ! [C: arrow_411405190le_alt,D: arrow_411405190le_alt] :
              ( ! [E: arrow_159774573e_indi] : ( E @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( D @ ( C @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
             => ( B @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( D @ ( C @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_unanimity__def) ).

thf(258,plain,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun )] :
      ( ( ! [B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
            ( ( arrow_610318064e_Prof @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
           => ! [C: arrow_411405190le_alt,D: arrow_411405190le_alt] :
                ( ! [E: arrow_159774573e_indi] : ( E @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( D @ ( C @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
               => ( B @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( D @ ( C @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) )
       => ( A @ arrow_2069624013nimity ) )
      & ( ( A @ arrow_2069624013nimity )
       => ! [B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
            ( ( arrow_610318064e_Prof @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
           => ! [C: arrow_411405190le_alt,D: arrow_411405190le_alt] :
                ( ! [E: arrow_159774573e_indi] : ( E @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( D @ ( C @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
               => ( B @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( D @ ( C @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).

thf(66,axiom,
    ( ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
  <=> ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_bc) ).

thf(401,plain,
    ( ( ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
     => ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
    & ( ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
     => ( c @ ( a @ ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( a @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).

thf(98,axiom,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt,C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),D: arrow_411405190le_alt,E: arrow_411405190le_alt] :
      ( ( E != D )
     => ( ( arrow_1985332922le_Lin @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
       => ( ( D @ ( E @ ( C @ arrow_1158827142_above ) ) @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
        <=> ( ( ( B != D )
             => ( ( ( A != D )
                 => ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                & ( ( A = D )
                 => ( ( C @ ( E @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                    | ( B = E ) ) ) ) )
            & ( ( B = D )
             => ( C @ ( A @ ( E @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
            & ( B != A ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_in__above) ).

thf(568,plain,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt,C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),D: arrow_411405190le_alt,E: arrow_411405190le_alt] :
      ( ( E != D )
     => ( ( arrow_1985332922le_Lin @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
       => ( ( ( ( ( B != D )
               => ( ( ( A != D )
                   => ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                  & ( ( A = D )
                   => ( ( C @ ( E @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                      | ( B = E ) ) ) ) )
              & ( ( B = D )
               => ( C @ ( A @ ( E @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
              & ( B != A ) )
           => ( D @ ( E @ ( C @ arrow_1158827142_above ) ) @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
          & ( ( D @ ( E @ ( C @ arrow_1158827142_above ) ) @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
           => ( ( ( B != D )
               => ( ( ( A != D )
                   => ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                  & ( ( A = D )
                   => ( ( C @ ( E @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                      | ( B = E ) ) ) ) )
              & ( ( B = D )
               => ( C @ ( A @ ( E @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
              & ( B != A ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).

thf(70,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TC,B: TA,C: TB @ ( TA @ fun ) @ ( TC @ fun )] :
      ( ( A @ ( B @ ( C @ ( TB @ ( TA @ ( TC @ combc ) ) ) ) @ ( TB @ ( TC @ aa ) ) ) )
      = ( B @ ( A @ ( C @ ( TB @ ( TA @ fun ) @ ( TC @ aa ) ) ) @ ( TB @ ( TA @ aa ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBC_1_1_U) ).

thf(433,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TC,B: TA,C: TB @ ( TA @ fun ) @ ( TC @ fun )] :
      ( ( A @ ( B @ ( C @ ( TB @ ( TA @ ( TC @ combc ) ) ) ) @ ( TB @ ( TC @ aa ) ) ) )
      = ( B @ ( A @ ( C @ ( TB @ ( TA @ fun ) @ ( TC @ aa ) ) ) @ ( TB @ ( TA @ aa ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).

thf(31,axiom,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),B: arrow_411405190le_alt,C: arrow_411405190le_alt] :
      ( ( C != B )
     => ( ( arrow_1985332922le_Lin @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
       => ( arrow_1985332922le_Lin @ ( B @ ( C @ ( A @ arrow_1158827142_above ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_above__Lin) ).

thf(207,plain,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),B: arrow_411405190le_alt,C: arrow_411405190le_alt] :
      ( ( C != B )
     => ( ( arrow_1985332922le_Lin @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
       => ( arrow_1985332922le_Lin @ ( B @ ( C @ ( A @ arrow_1158827142_above ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).

thf(82,axiom,
    ! [TA: $tType,TB: $tType,A: TB,B: bool @ ( TA @ fun ),C: bool @ ( TB @ fun ),D: TA @ ( TB @ fun )] :
      ( ( B @ ( TB @ ( bool @ ( TA @ fun ) @ combk ) ) @ ( C @ ( TA @ ( TB @ pi ) ) ) @ ( D @ ( TA @ ( TB @ fun ) @ member ) ) )
     => ( ( C @ ( A @ ( TB @ member ) ) )
       => ( B @ ( A @ ( D @ ( TA @ ( TB @ aa ) ) ) @ ( TA @ member ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_funcset__mem) ).

thf(478,plain,
    ! [TA: $tType,TB: $tType,A: TB,B: bool @ ( TA @ fun ),C: bool @ ( TB @ fun ),D: TA @ ( TB @ fun )] :
      ( ( B @ ( TB @ ( bool @ ( TA @ fun ) @ combk ) ) @ ( C @ ( TA @ ( TB @ pi ) ) ) @ ( D @ ( TA @ ( TB @ fun ) @ member ) ) )
     => ( ( C @ ( A @ ( TB @ member ) ) )
       => ( B @ ( A @ ( D @ ( TA @ ( TB @ aa ) ) ) @ ( TA @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).

thf(62,axiom,
    ! [TA: $tType,TB: $tType] :
      ( ( TA @ top )
     => ( TA @ ( TB @ fun ) @ top ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_fun___Orderings_Otop) ).

thf(383,plain,
    ! [TA: $tType,TB: $tType] :
      ( ( TA @ top )
     => ( TA @ ( TB @ fun ) @ top ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).

thf(51,axiom,
    ! [TA: $tType,TB: $tType,A: TA,B: TA,C: TB @ ( TA @ fun ),D: bool @ ( TB @ fun ) @ ( TB @ fun )] :
      ( ( A @ ( B @ ( C @ ( D @ ( TA @ ( TB @ inv_imagep ) ) ) ) ) )
    <=> ( A @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( B @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( D @ ( bool @ ( TB @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( TB @ aa ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_in__inv__imagep) ).

thf(315,plain,
    ! [TA: $tType,TB: $tType,A: TA,B: TA,C: TB @ ( TA @ fun ),D: bool @ ( TB @ fun ) @ ( TB @ fun )] :
      ( ( ( A @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( B @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( D @ ( bool @ ( TB @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( TB @ aa ) ) ) @ pp )
       => ( A @ ( B @ ( C @ ( D @ ( TA @ ( TB @ inv_imagep ) ) ) ) ) ) )
      & ( ( A @ ( B @ ( C @ ( D @ ( TA @ ( TB @ inv_imagep ) ) ) ) ) )
       => ( A @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( B @ ( C @ ( TB @ ( TA @ aa ) ) ) @ ( D @ ( bool @ ( TB @ fun ) @ ( TB @ aa ) ) ) @ ( bool @ ( TB @ aa ) ) ) @ pp ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).

thf(69,axiom,
    ! [A: arrow_411405190le_alt,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),C: arrow_411405190le_alt,D: arrow_411405190le_alt] :
      ( ( A @ ( B @ arrow_424895264_mktop ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
    <=> ( ( ( C != A )
         => ( B @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
        & ( ( C = A )
         => ( D != C ) )
        & ( D != A ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_in__mktop) ).

thf(410,plain,
    ! [A: arrow_411405190le_alt,B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),C: arrow_411405190le_alt,D: arrow_411405190le_alt] :
      ( ( ( ( ( C != A )
           => ( B @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
          & ( ( C = A )
           => ( D != C ) )
          & ( D != A ) )
       => ( A @ ( B @ arrow_424895264_mktop ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
      & ( ( A @ ( B @ arrow_424895264_mktop ) @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( ( ( C != A )
           => ( B @ ( C @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
          & ( ( C = A )
           => ( D != C ) )
          & ( D != A ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).

thf(67,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TA @ ( TB @ product_prod ) @ ( TC @ product_prod )] :
      ~ ! [B: TC,C: TB,D: TA] :
          ( A
         != ( D @ ( C @ ( TA @ ( TB @ product_Pair ) ) ) @ ( B @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_Pair ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_prod__cases3) ).

thf(405,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TA @ ( TB @ product_prod ) @ ( TC @ product_prod )] :
      ~ ! [B: TC,C: TB,D: TA] :
          ( A
         != ( D @ ( C @ ( TA @ ( TB @ product_Pair ) ) ) @ ( B @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_Pair ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).

thf(24,axiom,
    ! [TA: $tType,A: TA,B: TA @ list] :
      ( ( B @ ( TA @ distinct ) )
     => ( B @ ( A @ ( TA @ insert ) ) @ ( TA @ distinct ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_distinct__insert) ).

thf(190,plain,
    ! [TA: $tType,A: TA,B: TA @ list] :
      ( ( B @ ( TA @ distinct ) )
     => ( B @ ( A @ ( TA @ insert ) ) @ ( TA @ distinct ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).

thf(44,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType,TF: $tType,A: TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ),B: bool @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ fun )] :
      ( ! [C: TA,D: TB,E: TC,F: TD,G: TE,H: TF] : ( H @ ( G @ ( TF @ ( TE @ product_Pair ) ) ) @ ( F @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_Pair ) ) ) @ ( E @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_Pair ) ) ) @ ( D @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_Pair ) ) ) @ ( C @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_Pair ) ) ) @ ( B @ ( bool @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp )
     => ( A @ ( B @ ( bool @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_prod__induct6) ).

thf(273,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType,TF: $tType,A: TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ),B: bool @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ fun )] :
      ( ! [C: TA,D: TB,E: TC,F: TD,G: TE,H: TF] : ( H @ ( G @ ( TF @ ( TE @ product_Pair ) ) ) @ ( F @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_Pair ) ) ) @ ( E @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_Pair ) ) ) @ ( D @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_Pair ) ) ) @ ( C @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_Pair ) ) ) @ ( B @ ( bool @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp )
     => ( A @ ( B @ ( bool @ ( TF @ ( TE @ product_prod ) @ ( TD @ product_prod ) @ ( TC @ product_prod ) @ ( TB @ product_prod ) @ ( TA @ product_prod ) @ aa ) ) ) @ pp ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).

thf(97,axiom,
    ! [TA: $tType,TB: $tType,A: bool @ ( TB @ fun ) @ ( TA @ fun ),B: TB @ ( TA @ fun ),C: bool @ ( TA @ fun )] :
      ( ! [D: TA] :
          ( ( C @ ( D @ ( TA @ member ) ) )
         => ( D @ ( A @ ( bool @ ( TB @ fun ) @ ( TA @ aa ) ) ) @ ( D @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ member ) ) ) )
     => ( A @ ( C @ ( TB @ ( TA @ pi ) ) ) @ ( B @ ( TB @ ( TA @ fun ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_Pi__I_H) ).

thf(564,plain,
    ! [TA: $tType,TB: $tType,A: bool @ ( TB @ fun ) @ ( TA @ fun ),B: TB @ ( TA @ fun ),C: bool @ ( TA @ fun )] :
      ( ! [D: TA] :
          ( ( C @ ( D @ ( TA @ member ) ) )
         => ( D @ ( A @ ( bool @ ( TB @ fun ) @ ( TA @ aa ) ) ) @ ( D @ ( B @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ member ) ) ) )
     => ( A @ ( C @ ( TB @ ( TA @ pi ) ) ) @ ( B @ ( TB @ ( TA @ fun ) @ member ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).

thf(32,axiom,
    arrow_610318064e_Prof @ ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15__096_I_Fp_O_Abelow_A_Ibelow_A_IP_Ap_J_Ac_Ab_J_Ab_Aa_J_A_058_AProf_096) ).

thf(210,plain,
    arrow_610318064e_Prof @ ( a @ ( b @ ( b @ ( c @ ( p1 @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( arrow_319942042_below @ ( arrow_159774573e_indi @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ combb ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ ( arrow_159774573e_indi @ combc ) ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).

thf(54,axiom,
    ! [A: arrow_159774573e_indi] :
      ( ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
    <=> ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5__096ALL_Ai_O_A_Ia_A_060_092_060_094bsub_062P_Ai_092_060_094esub_062_Ab_J_A_061_A_Ia_A_060_092_060_094bsub_062below_A_IP_Ai_J_Ac_Ab_092_060_094esub_062_Ac_J_096) ).

thf(326,plain,
    ! [A: arrow_159774573e_indi] :
      ( ( ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
      & ( ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( b @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).

thf(5,axiom,
    ! [TA: $tType,A: bool @ ( TA @ fun )] :
      ( ( A @ ( TA @ collect ) )
      = A ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_Collect__def) ).

thf(126,plain,
    ! [TA: $tType,A: bool @ ( TA @ fun )] :
      ( ( A @ ( TA @ collect ) )
      = A ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).

thf(59,axiom,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt,C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),D: arrow_411405190le_alt,E: arrow_411405190le_alt] :
      ( ( E != D )
     => ( ( arrow_1985332922le_Lin @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
       => ( ( D @ ( E @ ( C @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
        <=> ( ( ( A != E )
             => ( ( ( B != E )
                 => ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                & ( ( B = E )
                 => ( ( C @ ( A @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                    | ( A = D ) ) ) ) )
            & ( ( A = E )
             => ( C @ ( D @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
            & ( B != A ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_in__below) ).

thf(341,plain,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt,C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),D: arrow_411405190le_alt,E: arrow_411405190le_alt] :
      ( ( E != D )
     => ( ( arrow_1985332922le_Lin @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
       => ( ( ( ( ( A != E )
               => ( ( ( B != E )
                   => ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                  & ( ( B = E )
                   => ( ( C @ ( A @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                      | ( A = D ) ) ) ) )
              & ( ( A = E )
               => ( C @ ( D @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
              & ( B != A ) )
           => ( D @ ( E @ ( C @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
          & ( ( D @ ( E @ ( C @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
           => ( ( ( A != E )
               => ( ( ( B != E )
                   => ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                  & ( ( B = E )
                   => ( ( C @ ( A @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                      | ( A = D ) ) ) ) )
              & ( ( A = E )
               => ( C @ ( D @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
              & ( B != A ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).

thf(43,axiom,
    ! [TA: $tType,TB: $tType,A: bool @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ? [B: TA @ ( TB @ product_prod )] : ( B @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp )
    <=> ? [B: TB,C: TA] : ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_split__paired__Ex) ).

thf(268,plain,
    ! [TA: $tType,TB: $tType,A: bool @ ( TA @ ( TB @ product_prod ) @ fun )] :
      ( ( ? [B: TB,C: TA] : ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp )
       => ? [B: TA @ ( TB @ product_prod )] : ( B @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp ) )
      & ( ? [B: TA @ ( TB @ product_prod )] : ( B @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp )
       => ? [B: TB,C: TA] : ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( A @ ( bool @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) @ pp ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).

thf(72,axiom,
    ! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
      ( ( A @ ( B @ ( TA @ member ) ) )
    <=> ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_mem__def) ).

thf(437,plain,
    ! [TA: $tType,A: bool @ ( TA @ fun ),B: TA] :
      ( ( ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp )
       => ( A @ ( B @ ( TA @ member ) ) ) )
      & ( ( A @ ( B @ ( TA @ member ) ) )
       => ( B @ ( A @ ( bool @ ( TA @ aa ) ) ) @ pp ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).

thf(48,axiom,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun )] :
      ( ( A @ arrow_1958449194le_IIA )
    <=> ! [B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
          ( ( arrow_610318064e_Prof @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
         => ! [C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
              ( ( arrow_610318064e_Prof @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
             => ! [D: arrow_411405190le_alt,E: arrow_411405190le_alt] :
                  ( ! [F: arrow_159774573e_indi] :
                      ( ( F @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                    <=> ( F @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                 => ( ( B @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                  <=> ( C @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_IIA__def) ).

thf(283,plain,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun )] :
      ( ( ! [B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
            ( ( arrow_610318064e_Prof @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
           => ! [C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
                ( ( arrow_610318064e_Prof @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
               => ! [D: arrow_411405190le_alt,E: arrow_411405190le_alt] :
                    ( ! [F: arrow_159774573e_indi] :
                        ( ( ( F @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                         => ( F @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                        & ( ( F @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                         => ( F @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) )
                   => ( ( ( C @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                       => ( B @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                      & ( ( B @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                       => ( C @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) ) ) )
       => ( A @ arrow_1958449194le_IIA ) )
      & ( ( A @ arrow_1958449194le_IIA )
       => ! [B: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
            ( ( arrow_610318064e_Prof @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
           => ! [C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun )] :
                ( ( arrow_610318064e_Prof @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ) )
               => ! [D: arrow_411405190le_alt,E: arrow_411405190le_alt] :
                    ( ! [F: arrow_159774573e_indi] :
                        ( ( ( F @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                         => ( F @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                        & ( ( F @ ( B @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                         => ( F @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) )
                   => ( ( ( C @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                       => ( B @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
                      & ( ( B @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
                       => ( C @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ aa ) ) ) @ ( E @ ( D @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ) ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).

thf(108,axiom,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt,C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
     => ( ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ~ ( C @ ( B @ ( A @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_Lin__irrefl) ).

thf(624,plain,
    ! [A: arrow_411405190le_alt,B: arrow_411405190le_alt,C: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun )] :
      ( ( arrow_1985332922le_Lin @ ( C @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
     => ( ( C @ ( A @ ( B @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ~ ( C @ ( B @ ( A @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).

thf(78,axiom,
    arrow_610318064e_Prof @ ( p @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4__096P_H_A_058_AProf_096) ).

thf(464,plain,
    arrow_610318064e_Prof @ ( p @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ member ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).

thf(55,axiom,
    arrow_1985332922le_Lin @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ ( bool @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ fun ) @ combk ) ) @ ( arrow_610318064e_Prof @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ pi ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun ) @ member ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_assms_I1_J) ).

thf(332,plain,
    arrow_1985332922le_Lin @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ ( bool @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ fun ) @ combk ) ) @ ( arrow_610318064e_Prof @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ pi ) ) ) @ ( f @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ fun ) @ fun ) @ member ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).

thf(29,axiom,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),B: arrow_411405190le_alt,C: arrow_411405190le_alt] :
      ( ( C != B )
     => ( ( arrow_1985332922le_Lin @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
       => ( arrow_1985332922le_Lin @ ( B @ ( C @ ( A @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_below__Lin) ).

thf(200,plain,
    ! [A: bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ),B: arrow_411405190le_alt,C: arrow_411405190le_alt] :
      ( ( C != B )
     => ( ( arrow_1985332922le_Lin @ ( A @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) )
       => ( arrow_1985332922le_Lin @ ( B @ ( C @ ( A @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).

thf(46,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType,TF: $tType,A: TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod ) @ ( TE @ product_prod ) @ ( TF @ product_prod )] :
      ~ ! [B: TF,C: TE,D: TD,E: TC,F: TB,G: TA] :
          ( A
         != ( G @ ( F @ ( TA @ ( TB @ product_Pair ) ) ) @ ( E @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_Pair ) ) ) @ ( D @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_Pair ) ) ) @ ( C @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod ) @ ( TE @ product_Pair ) ) ) @ ( B @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod ) @ ( TE @ product_prod ) @ ( TF @ product_Pair ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_prod__cases6) ).

thf(277,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType,TF: $tType,A: TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod ) @ ( TE @ product_prod ) @ ( TF @ product_prod )] :
      ~ ! [B: TF,C: TE,D: TD,E: TC,F: TB,G: TA] :
          ( A
         != ( G @ ( F @ ( TA @ ( TB @ product_Pair ) ) ) @ ( E @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_Pair ) ) ) @ ( D @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_Pair ) ) ) @ ( C @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod ) @ ( TE @ product_Pair ) ) ) @ ( B @ ( TA @ ( TB @ product_prod ) @ ( TC @ product_prod ) @ ( TD @ product_prod ) @ ( TE @ product_prod ) @ ( TF @ product_Pair ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).

thf(100,axiom,
    a != b,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__096a_A_126_061_Ab_096) ).

thf(607,plain,
    a != b,
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).

thf(80,axiom,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TC @ ( TA @ ( TB @ product_prod ) @ fun ),B: TB,C: TA] :
      ( ( C @ ( B @ ( A @ ( TC @ ( TA @ ( TB @ product_curry ) ) ) ) ) )
      = ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( A @ ( TC @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_curry__def) ).

thf(469,plain,
    ! [TA: $tType,TB: $tType,TC: $tType,A: TC @ ( TA @ ( TB @ product_prod ) @ fun ),B: TB,C: TA] :
      ( ( C @ ( B @ ( A @ ( TC @ ( TA @ ( TB @ product_curry ) ) ) ) ) )
      = ( C @ ( B @ ( TA @ ( TB @ product_Pair ) ) ) @ ( A @ ( TC @ ( TA @ ( TB @ product_prod ) @ aa ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).

thf(35,axiom,
    ! [TA: $tType,TB: $tType,A: TA,B: bool @ ( TB @ fun ) @ ( TA @ fun ),C: bool @ ( TA @ fun ),D: TB @ ( TA @ fun )] :
      ( ( B @ ( C @ ( TB @ ( TA @ pi ) ) ) @ ( D @ ( TB @ ( TA @ fun ) @ member ) ) )
     => ( ~ ( A @ ( B @ ( bool @ ( TB @ fun ) @ ( TA @ aa ) ) ) @ ( A @ ( D @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ member ) ) )
       => ~ ( C @ ( A @ ( TA @ member ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_PiE) ).

thf(215,plain,
    ! [TA: $tType,TB: $tType,A: TA,B: bool @ ( TB @ fun ) @ ( TA @ fun ),C: bool @ ( TA @ fun ),D: TB @ ( TA @ fun )] :
      ( ( B @ ( C @ ( TB @ ( TA @ pi ) ) ) @ ( D @ ( TB @ ( TA @ fun ) @ member ) ) )
     => ( ~ ( A @ ( B @ ( bool @ ( TB @ fun ) @ ( TA @ aa ) ) ) @ ( A @ ( D @ ( TB @ ( TA @ aa ) ) ) @ ( TB @ member ) ) )
       => ~ ( C @ ( A @ ( TA @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).

thf(87,axiom,
    ! [TA: $tType,TB: $tType,A: bool @ ( TB @ ( TA @ product_prod ) @ fun ),B: bool @ ( TB @ ( TA @ product_prod ) @ fun )] :
      ( ! [C: TA,D: TB] :
          ( ( B @ ( D @ ( C @ ( TB @ ( TA @ product_Pair ) ) ) @ ( TB @ ( TA @ product_prod ) @ member ) ) )
        <=> ( A @ ( D @ ( C @ ( TB @ ( TA @ product_Pair ) ) ) @ ( TB @ ( TA @ product_prod ) @ member ) ) ) )
    <=> ( B = A ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_pred__equals__eq2) ).

thf(496,plain,
    ! [TA: $tType,TB: $tType,A: bool @ ( TB @ ( TA @ product_prod ) @ fun ),B: bool @ ( TB @ ( TA @ product_prod ) @ fun )] :
      ( ( ( B = A )
       => ! [C: TA,D: TB] :
            ( ( ( A @ ( D @ ( C @ ( TB @ ( TA @ product_Pair ) ) ) @ ( TB @ ( TA @ product_prod ) @ member ) ) )
             => ( B @ ( D @ ( C @ ( TB @ ( TA @ product_Pair ) ) ) @ ( TB @ ( TA @ product_prod ) @ member ) ) ) )
            & ( ( B @ ( D @ ( C @ ( TB @ ( TA @ product_Pair ) ) ) @ ( TB @ ( TA @ product_prod ) @ member ) ) )
             => ( A @ ( D @ ( C @ ( TB @ ( TA @ product_Pair ) ) ) @ ( TB @ ( TA @ product_prod ) @ member ) ) ) ) ) )
      & ( ! [C: TA,D: TB] :
            ( ( ( A @ ( D @ ( C @ ( TB @ ( TA @ product_Pair ) ) ) @ ( TB @ ( TA @ product_prod ) @ member ) ) )
             => ( B @ ( D @ ( C @ ( TB @ ( TA @ product_Pair ) ) ) @ ( TB @ ( TA @ product_prod ) @ member ) ) ) )
            & ( ( B @ ( D @ ( C @ ( TB @ ( TA @ product_Pair ) ) ) @ ( TB @ ( TA @ product_prod ) @ member ) ) )
             => ( A @ ( D @ ( C @ ( TB @ ( TA @ product_Pair ) ) ) @ ( TB @ ( TA @ product_prod ) @ member ) ) ) ) )
       => ( B = A ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).

thf(75,axiom,
    ! [A: arrow_159774573e_indi] :
      ( ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
    <=> ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6__096ALL_Ai_O_A_Ia_A_060_092_060_094bsub_062below_A_IP_Ai_J_Ac_Ab_092_060_094esub_062_Ac_J_A_061_A_Ib_A_060_092_060_094bsub_062below_A_Ibelow_A_IP_Ai_J_Ac_Ab_J_Ab_Aa_092_060_094esub_062_Ac_J_096) ).

thf(454,plain,
    ! [A: arrow_159774573e_indi] :
      ( ( ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) )
      & ( ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( a @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) )
       => ( a @ ( b @ ( b @ ( c @ ( A @ ( p1 @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_159774573e_indi @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( arrow_319942042_below @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( bool @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ fun ) @ ( arrow_411405190le_alt @ aa ) ) ) @ ( c @ ( b @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_Pair ) ) ) @ ( arrow_411405190le_alt @ ( arrow_411405190le_alt @ product_prod ) @ member ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).

thf(644,plain,
    $false,
    inference(e,[status(thm)],[193,311,149,150,138,333,249,408,217,308,120,385,472,538,153,185,436,257,619,196,460,559,638,448,492,179,211,238,480,280,634,132,396,133,380,512,546,160,192,275,169,610,156,615,622,515,129,562,176,641,611,159,604,187,113,377,494,552,323,140,213,626,462,223,394,135,490,255,617,123,199,182,441,338,544,336,612,465,556,203,319,258,401,568,433,207,478,383,315,410,405,190,273,564,210,326,126,341,268,437,283,624,464,332,200,277,607,469,215,496,454]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SCT224_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.08  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.15/0.42  % Computer : n001.cluster.edu
% 0.15/0.42  % Model    : x86_64 x86_64
% 0.15/0.42  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42  % Memory   : 8046.5625MB
% 0.15/0.42  % OS       : Linux 6.8.0-71-generic
% 0.15/0.42  % CPULimit : 300
% 0.15/0.42  % WCLimit  : 300
% 0.15/0.42  % DateTime : Sat Sep 26 06:49:13 UTC 2026
% 0.15/0.42  % CPUTime  : 
% 0.15/0.42  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.81/0.99  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 1.82/1.30  % [INFO] 	 Parsing done (310ms). 
% 1.82/1.31  % [INFO] 	 Running in sequential loop mode. 
% 2.39/1.69  % [INFO] 	 eprover registered as external prover. 
% 2.61/1.70  % [INFO] 	 Scanning for conjecture ... 
% 2.79/1.89  % [INFO] 	 Found a conjecture (or negated_conjecture) and 110 axioms. Running axiom selection ... 
% 3.55/2.04  % [INFO] 	 Axiom selection finished. Selected 110 axioms (removed 0 axioms). 
% 4.31/2.26  % [INFO] 	 Problem is typed first-order (TPTP TFF). 
% 4.31/2.29  % [INFO] 	 Type checking passed. 
% 4.31/2.30  % [CONFIG] 	 Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>.  Searching for refutation ... 
% 5.96/2.61  % [INFO] 	 [Domain constraints] Detected constraint on bool 
% 5.96/2.61  % [INFO] 	 [Domain constraints] dom(bool) ⊆ {fTrue,fFalse} 
% 43.92/27.69  % External prover 'e' found a proof!
% 43.92/27.69  % [INFO] 	 Killing All external provers ... 
% 43.92/27.69  % Time passed: 27136ms (effective reasoning time: 26372ms)
% 43.92/27.69  % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 43.92/27.70  % Axioms used in derivation (110): fact_83_list_Osimps_I2_J, fact_16__096_I_Fp_O_Abelow_A_Ibelow_A_Ibelow_A_IP_Ap_J_Ac_Ab_J_Ab_Aa_J_Aa_Ac_J_A_058_AProf_096, fact_34_in__above, fact_81_not__Cons__self, fact_21__096_I_Fp_O_Abelow_A_IP_Ap_J_Ac_Ab_J_A_058_AProf_096, fact_63_curryI, fact_10_in__mkbot, fact_19_assms_I3_J, fact_54_funcsetI, fact_97_splice_Osimps_I1_J, fact_48_prod__induct5, fact_14_bc, fact_29_notin__Lin__iff, fact_49_Pi__I, fact_61_curry__conv, fact_66_in__inv__imagep, help_COMBI_1_1_U, fact_94_splice_Osimps_I2_J, fact_23__C2_C, fact_3_iff, fact_96_splice__Nil2, fact_85_iso__tuple__UNIV__I, fact_1__096P_A_058_AProf_096, help_fTrue_1_1_T, fact_41_PiE, fact_8_split__paired__All, fact_38_unanimity__def, fact_9_Pair__eq, fact_47_prod__cases5, fact_20_u, fact_51_prod__cases4, fact_18_Pair__inject, help_fTrue_1_1_U, fact_70_Pi__UNIV, fact_79_list_Oinject, fact_37_dictator__def, fact_95_splice_Osimps_I3_J, fact_65_curryE, fact_84_distinct__length__2__or__more, fact_25_const__Lin__Prof, fact_78_distinct__singleton, fact_73_distinct_Osimps_I1_J, fact_36_linear__alt, fact_68_dist, help_COMBB_1_1_U, fact_64_curryD, fact_98_list_Osimps_I4_J, fact_74_third__alt, fact_11_in__mktop, fact_62_curry__def, fact_43_funcset__mem, fact_13_ac, fact_40_dictatorI, fact_2__096ALL_Ai_O_A_Ib_A_060_092_060_094bsub_062below_A_Ibelow_A_Ibelow_A_IP_Ai_J_Ac_Ab_J_Ab_Aa_J_Aa_Ac_092_060_094esub_062_Aa_J_A_061_A_Ia_A_060_092_060_094bsub_062P_Ai_092_060_094esub_062_Ab_J_096, fact_44_prod__induct6, fact_82_list_Osimps_I3_J, fact_53_prod__cases3, fact_30_below__Lin, fact_5__096ALL_Ai_O_A_Ia_A_060_092_060_094bsub_062P_Ai_092_060_094esub_062_Ab_J_A_061_A_Ia_A_060_092_060_094bsub_062below_A_IP_Ai_J_Ac_Ab_092_060_094esub_062_Ac_J_096, fact_80_not__Cons__self2, fact_46_prod__cases6, fact_39_above__Lin, arity_HOL_Obool___Orderings_Otop, fact_60_internal__split__conv, fact_89_list_Oexhaust, fact_6__096ALL_Ai_O_A_Ia_A_060_092_060_094bsub_062below_A_IP_Ai_J_Ac_Ab_092_060_094esub_062_Ac_J_A_061_A_Ib_A_060_092_060_094bsub_062below_A_Ibelow_A_IP_Ai_J_Ac_Ab_J_Ab_Aa_092_060_094esub_062_Ac_J_096, fact_93_alt3, fact_24_assms_I1_J, fact_22__C1_C, fact_76_mem__def, fact_88_neq__Nil__conv, fact_56_Pi__cong, help_COMBK_1_1_U, fact_17_in__below, fact_90_top__apply, fact_67_Prof__def, help_COMBC_1_1_U, fact_26_mkbot__Lin, fact_57_pred__equals__eq2, fact_71__096_B_Bthesis_O_A_I_B_Bc_O_Adistinct_A_091a_M_Ab_M_Ac_093_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096, fact_31_IIA__def, fact_27_mktop__Lin, fact_15__096_I_Fp_O_Abelow_A_Ibelow_A_IP_Ap_J_Ac_Ab_J_Ab_Aa_J_A_058_AProf_096, fact_42_funcset__id, fact_69_top1I, fact_86_UNIV__I, fact_33_complete__Lin, fact_77_Collect__def, fact_55_Pi__I_H, fact_45_Pi__mem, help_pp_1_1_U, fact_72_inv__imagep__def, fact_12_ab, fact_75_ext, arity_fun___Orderings_Otop, fact_52_prod__induct3, fact_50_prod__induct4, help_pp_2_1_U, fact_4__096P_H_A_058_AProf_096, fact_58_PairE, fact_32_split__paired__Ex, fact_59_prod_Oexhaust, fact_99_UNIV__eq__I, fact_35_prod_Orecs, fact_91_insert__Nil, fact_28_Lin__irrefl, fact_7__096ALL_Ai_O_A_Ib_A_060_092_060_094bsub_062below_A_Ibelow_A_IP_Ai_J_Ac_Ab_J_Ab_Aa_092_060_094esub_062_Ac_J_A_061_A_Ib_A_060_092_060_094bsub_062below_A_Ibelow_A_Ibelow_A_IP_Ai_J_Ac_Ab_J_Ab_Aa_J_Aa_Ac_092_060_094esub_062_Aa_J_096, fact_0__096a_A_126_061_Ab_096, fact_87_UNIV__def, fact_92_distinct__insert
% 43.92/27.70  % No. of inferences in proof: 224
% 43.92/27.70  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 27136 ms resp. 26372 ms w/o parsing
% 44.75/27.87  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 44.75/27.87  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------