Z3---4.15.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : Z3---4.15.1
% Problem  : SCT171+7 : TPTP v9.0.0. Released v5.3.0.
% Transfm  : none
% Format   : tptp
% Command  : run_E %s %d THM

% Computer : n008.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Sat Jun 21 05:24:37 AM UTC 2025

% Result   : Theorem 0.91s 1.10s
% Output   : Proof 1.09s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    4
%            Number of leaves      :    7
% Syntax   : Number of formulae    :   13 (   6 unt;   0 typ;   0 def)
%            Number of atoms       :   24 (   0 equ)
%            Maximal formula atoms :    4 (   1 avg)
%            Number of connectives :   18 (   7   ~;   3   |;   0   &)
%                                         (   8 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    5 (   2 avg)
%            Maximal term depth    :   19 (   2 avg)
%            Number of types       :    2 (   0 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :    2 (   1 usr;   1 prp; 0-1 aty)
%            Number of functors    :   25 (  25 usr;  14 con; 0-4 aty)
%            Number of variables   :    0 (   0   !;   0   ?;   0   :)

% Comments : 
%------------------------------------------------------------------------------
tff(hBOOL_type,type,
    hBOOL: $i > $o ).

tff(hAPP_type,type,
    hAPP: ( $i * $i * $i * $i ) > $i ).

tff(p_type,type,
    p: $i ).

tff(f_type,type,
    f: $i ).

tff(fun_type,type,
    fun: ( $i * $i ) > $i ).

tff(bool_type,type,
    bool: $i ).

tff(product_prod_type,type,
    product_prod: ( $i * $i ) > $i ).

tff(arrow_2142409994le_alt_type,type,
    arrow_2142409994le_alt: $i ).

tff(arrow_1998540521e_indi_type,type,
    arrow_1998540521e_indi: $i ).

tff(d_type,type,
    d: $i ).

tff(c_type,type,
    c: $i ).

tff(product_Pair_type,type,
    product_Pair: ( $i * $i ) > $i ).

tff(member_type,type,
    member: $i > $i ).

tff(e_type,type,
    e: $i ).

tff(arrow_1622070166_mkbot_type,type,
    arrow_1622070166_mkbot: $i ).

tff(combb_type,type,
    combb: ( $i * $i * $i ) > $i ).

tff(combc_type,type,
    combc: ( $i * $i * $i ) > $i ).

tff(arrow_357225482_above_type,type,
    arrow_357225482_above: $i ).

tff(n_type,type,
    n: $i ).

tff(h_type,type,
    h: $i ).

tff(fequal_type,type,
    fequal: $i > $i ).

tff(nat_type,type,
    nat: $i ).

tff(if_type,type,
    if: $i > $i ).

tff(combs_type,type,
    combs: ( $i * $i * $i ) > $i ).

tff(arrow_1770777252_mktop_type,type,
    arrow_1770777252_mktop: $i ).

tff(ord_less_type,type,
    ord_less: $i > $i ).

tff(1,plain,
    ( ~ hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p)))
  <=> ~ hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p))) ),
    inference(rewrite,[status(thm)],[]) ).

tff(2,axiom,
    ~ hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).

tff(3,plain,
    ~ hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p))),
    inference(modus_ponens,[status(thm)],[2,1]) ).

tff(4,plain,
    ( hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e))))))
  <=> hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e)))))) ),
    inference(rewrite,[status(thm)],[]) ).

tff(5,axiom,
    hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e)))))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_13__096c_A_060_092_060_094bsub_062F_A_I_Fi_O_Aif_Ah_Ai_A_060_An_Athen_Amkto) ).

tff(6,plain,
    hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e)))))),
    inference(modus_ponens,[status(thm)],[5,4]) ).

tff(7,plain,
    ( ( hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p)))
    <=> hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e)))))) )
  <=> ( hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p)))
    <=> hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e)))))) ) ),
    inference(rewrite,[status(thm)],[]) ).

tff(8,axiom,
    ( hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p)))
  <=> hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e)))))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_PW) ).

tff(9,plain,
    ( hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p)))
  <=> hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e)))))) ),
    inference(modus_ponens,[status(thm)],[8,7]) ).

tff(10,plain,
    ( hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p)))
    | ~ hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e))))))
    | ~ ( hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p)))
      <=> hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e)))))) ) ),
    inference(tautology,[status(thm)],[]) ).

tff(11,plain,
    ( hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p)))
    | ~ hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),ord_less(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1770777252_mktop),p)),e))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combs(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,bool),fun(arrow_1998540521e_indi,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),if(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(nat,fun(arrow_1998540521e_indi,bool),hAPP(fun(arrow_1998540521e_indi,fun(nat,bool)),fun(nat,fun(arrow_1998540521e_indi,bool)),combc(arrow_1998540521e_indi,nat,bool),hAPP(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1998540521e_indi,nat),fun(arrow_1998540521e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1998540521e_indi),fequal(nat)),h)),n))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),arrow_1998540521e_indi),arrow_357225482_above),p)),c)),e))),hAPP(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(arrow_2142409994le_alt,fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),combc(arrow_1998540521e_indi,arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),hAPP(fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool))),fun(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(arrow_1998540521e_indi,fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)))),combb(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),fun(arrow_2142409994le_alt,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),arrow_1998540521e_indi),arrow_1622070166_mkbot),p)),e)))))) ),
    inference(unit_resolution,[status(thm)],[10,9]) ).

tff(12,plain,
    hBOOL(hAPP(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool,hAPP(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),fun(fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),bool),member(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),hAPP(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),hAPP(arrow_2142409994le_alt,fun(arrow_2142409994le_alt,product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt)),product_Pair(arrow_2142409994le_alt,arrow_2142409994le_alt),c),d)),hAPP(fun(arrow_1998540521e_indi,fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool)),fun(product_prod(arrow_2142409994le_alt,arrow_2142409994le_alt),bool),f,p))),
    inference(unit_resolution,[status(thm)],[11,6]) ).

tff(13,plain,
    $false,
    inference(unit_resolution,[status(thm)],[12,3]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13  % Problem    : SCT171+7 : TPTP v9.0.0. Released v5.3.0.
% 0.08/0.13  % Command    : run_E %s %d THM
% 0.13/0.35  % Computer : n008.cluster.edu
% 0.13/0.35  % Model    : x86_64 x86_64
% 0.13/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35  % Memory   : 8042.1875MB
% 0.13/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35  % CPULimit   : 300
% 0.13/0.35  % WCLimit    : 300
% 0.13/0.35  % DateTime   : Fri Jun 20 03:58:48 EDT 2025
% 0.13/0.35  % CPUTime    : 
% 0.91/1.10  % SZS status Theorem
% 0.91/1.10  % SZS output start Proof
% See solution above
% 1.09/1.32  % E exiting
%------------------------------------------------------------------------------