FindProof---0.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : FindProof---0.1
% Problem  : SCT171+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300

% Computer : n008.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Fri Sep 25 02:40:09 PM UTC 2026

% Result   : Theorem 49.41s 12.18s
% Output   : Proof 49.41s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   10
%            Number of leaves      :    7
% Syntax   : Number of formulae    :   39 (  20 unt;   0 def)
%            Number of atoms       :   68 (  18 equ)
%            Maximal formula atoms :    4 (   1 avg)
%            Number of connectives :   49 (  20   ~;  23   |;   4   &)
%                                         (   2 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    5 (   3 avg)
%            Maximal term depth    :   19 (   2 avg)
%            Number of predicates  :    3 (   1 usr;   1 prp; 0-2 aty)
%            Number of functors    :   28 (  28 usr;  16 con; 0-4 aty)
%            Number of variables   :   32 (   2 sgn  18   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f56,axiom,
    hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),ord_less(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_992993526_mktop),p)),e))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),fequal(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),arrow_1726925404_above),p)),c)),e))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_844286440_mkbot),p)),e)))))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_13__096c_A_060_092_060_094bsub_062F_h92b9bbcc3b733df4) ).

fof(f56_nnf,plain,
    hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),ord_less(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_992993526_mktop),p)),e))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),fequal(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),arrow_1726925404_above),p)),c)),e))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_844286440_mkbot),p)),e)))))),
    inference(nnf_transformation,[status(thm)],[f56]) ).

cnf(c112,plain,
    hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),ord_less(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_992993526_mktop),p)),e))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),fequal(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),arrow_1726925404_above),p)),c)),e))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_844286440_mkbot),p)),e)))))),
    inference(cnf_transformation,[status(esa)],[f56_nnf]) ).

fof(f29,axiom,
    ! [X_c,X_a,B_1_1,B_2_1] : ti(X_c,hAPP(X_a,X_c,B_1_1,B_2_1)) = hAPP(X_a,X_c,B_1_1,B_2_1),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_hAPP_res) ).

fof(f29_nnf,plain,
    ! [X_c,X_a,B_1_1,B_2_1] : ti(X_c,hAPP(X_a,X_c,B_1_1,B_2_1)) = hAPP(X_a,X_c,B_1_1,B_2_1),
    inference(nnf_transformation,[status(thm)],[f29]) ).

fof(f29_sk,plain,
    ! [X_c,X_a,B_1_1,B_2_1] : ti(X_c,hAPP(X_a,X_c,B_1_1,B_2_1)) = hAPP(X_a,X_c,B_1_1,B_2_1),
    inference(skolemisation,[status(esa)],[f29_nnf]) ).

cnf(c29,plain,
    ti(X0,hAPP(X1,X0,X2,X3)) = hAPP(X1,X0,X2,X3),
    inference(cnf_transformation,[status(esa)],[f29_sk]) ).

fof(f158,axiom,
    ! [P] :
      ( ti(bool,P) = fFalse
      | ti(bool,P) = fTrue ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_3_1_T) ).

fof(f158_nnf,plain,
    ! [P] :
      ( ti(bool,P) = fFalse
      | ti(bool,P) = fTrue ),
    inference(nnf_transformation,[status(thm)],[f158]) ).

fof(f158_sk,plain,
    ! [P] :
      ( ti(bool,P) = fFalse
      | ti(bool,P) = fTrue ),
    inference(skolemisation,[status(esa)],[f158_nnf]) ).

cnf(c312,plain,
    ( ti(bool,X0) = fFalse
    | ti(bool,X0) = fTrue ),
    inference(cnf_transformation,[status(esa)],[f158_sk]) ).

cnf(p410,plain,
    ( hAPP(X0,bool,X1,X2) = fFalse
    | hAPP(X0,bool,X1,X2) = fTrue ),
    inference(superposition,[status(thm)],[c29,c312]) ).

fof(f168,conjecture,
    hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p))),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).

fof(f168_neg,negated_conjecture,
    ~ hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p))),
    inference(negated_conjecture,[status(cth)],[f168]) ).

fof(f168_nnf,plain,
    ~ hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p))),
    inference(nnf_transformation,[status(thm)],[f168_neg]) ).

fof(f168_sk,plain,
    ~ hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p))),
    inference(skolemisation,[status(esa)],[f168_nnf]) ).

cnf(c322,plain,
    ~ hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p))),
    inference(cnf_transformation,[status(esa)],[f168_sk]) ).

cnf(p457,plain,
    ( ~ hBOOL(fTrue)
    | hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p)) = fFalse ),
    inference(superposition,[status(thm)],[p410,c322]) ).

fof(f164,axiom,
    hBOOL(fTrue),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_fTrue_1_1_U) ).

fof(f164_nnf,plain,
    hBOOL(fTrue),
    inference(nnf_transformation,[status(thm)],[f164]) ).

cnf(c318,plain,
    hBOOL(fTrue),
    inference(cnf_transformation,[status(esa)],[f164_nnf]) ).

cnf(p463,plain,
    hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p)) = fFalse,
    inference(resolution,[status(thm)],[p457,c318]) ).

fof(f57,axiom,
    ( hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p)))
  <=> hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),ord_less(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_992993526_mktop),p)),e))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),fequal(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),arrow_1726925404_above),p)),c)),e))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_844286440_mkbot),p)),e)))))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_PW) ).

fof(f57_nnf,plain,
    ( ( ~ hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),ord_less(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_992993526_mktop),p)),e))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),fequal(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),arrow_1726925404_above),p)),c)),e))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_844286440_mkbot),p)),e))))))
      | hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p))) )
    & ( hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),ord_less(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_992993526_mktop),p)),e))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),fequal(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),arrow_1726925404_above),p)),c)),e))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_844286440_mkbot),p)),e))))))
      | ~ hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p))) ) ),
    inference(nnf_transformation,[status(thm)],[f57]) ).

fof(f57_sk,plain,
    ( ( ~ hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),ord_less(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_992993526_mktop),p)),e))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),fequal(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),arrow_1726925404_above),p)),c)),e))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_844286440_mkbot),p)),e))))))
      | hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p))) )
    & ( hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),ord_less(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_992993526_mktop),p)),e))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),fequal(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),arrow_1726925404_above),p)),c)),e))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_844286440_mkbot),p)),e))))))
      | ~ hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p))) ) ),
    inference(skolemisation,[status(esa)],[f57_nnf]) ).

cnf(c114,plain,
    ( ~ hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),ord_less(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_992993526_mktop),p)),e))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),fequal(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),arrow_1726925404_above),p)),c)),e))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_844286440_mkbot),p)),e))))))
    | hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,p))) ),
    inference(cnf_transformation,[status(esa)],[f57_sk]) ).

cnf(p464,plain,
    ( ~ hBOOL(hAPP(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool,hAPP(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),bool),member(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),hAPP(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),hAPP(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt)),product_Pair(arrow_1212486748le_alt,arrow_1212486748le_alt),c),d)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),f,hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),ord_less(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_992993526_mktop),p)),e))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combs(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,bool),fun(arrow_1384031255e_indi,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(bool,fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),if(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(nat,fun(arrow_1384031255e_indi,bool),hAPP(fun(arrow_1384031255e_indi,fun(nat,bool)),fun(nat,fun(arrow_1384031255e_indi,bool)),combc(arrow_1384031255e_indi,nat,bool),hAPP(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool)),hAPP(fun(nat,fun(nat,bool)),fun(fun(arrow_1384031255e_indi,nat),fun(arrow_1384031255e_indi,fun(nat,bool))),combb(nat,fun(nat,bool),arrow_1384031255e_indi),fequal(nat)),h)),n))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),arrow_1384031255e_indi),arrow_1726925404_above),p)),c)),e))),hAPP(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(arrow_1212486748le_alt,fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),combc(arrow_1384031255e_indi,arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),hAPP(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),hAPP(fun(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool))),fun(fun(arrow_1384031255e_indi,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),fun(arrow_1384031255e_indi,fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)))),combb(fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool),fun(arrow_1212486748le_alt,fun(product_prod(arrow_1212486748le_alt,arrow_1212486748le_alt),bool)),arrow_1384031255e_indi),arrow_844286440_mkbot),p)),e))))))
    | hBOOL(fFalse) ),
    inference(demodulation,[status(thm)],[p463,c114]) ).

cnf(p1763,plain,
    hBOOL(fFalse),
    inference(resolution,[status(thm)],[c112,p464]) ).

fof(f30,hypothesis,
    ! [B_1_1] :
      ( hBOOL(ti(bool,B_1_1))
    <=> hBOOL(B_1_1) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tsy_c_hBOOL_arg1) ).

fof(f30_nnf,plain,
    ! [B_1_1] :
      ( ( ~ hBOOL(B_1_1)
        | hBOOL(ti(bool,B_1_1)) )
      & ( hBOOL(B_1_1)
        | ~ hBOOL(ti(bool,B_1_1)) ) ),
    inference(nnf_transformation,[status(thm)],[f30]) ).

fof(f30_sk,plain,
    ! [B_1_1] :
      ( ( ~ hBOOL(B_1_1)
        | hBOOL(ti(bool,B_1_1)) )
      & ( hBOOL(B_1_1)
        | ~ hBOOL(ti(bool,B_1_1)) ) ),
    inference(skolemisation,[status(esa)],[f30_nnf]) ).

cnf(c30,plain,
    ( hBOOL(X0)
    | ~ hBOOL(ti(bool,X0)) ),
    inference(cnf_transformation,[status(esa)],[f30_sk]) ).

cnf(p368,plain,
    ( hBOOL(X0)
    | ~ hBOOL(fTrue)
    | ti(bool,X0) = fFalse ),
    inference(superposition,[status(thm)],[c312,c30]) ).

cnf(p390,plain,
    ( hBOOL(X0)
    | ti(bool,X0) = fFalse ),
    inference(resolution,[status(thm)],[p368,c318]) ).

cnf(p393,plain,
    ( hBOOL(X0)
    | ~ hBOOL(fFalse)
    | hBOOL(X0) ),
    inference(superposition,[status(thm)],[p390,c30]) ).

cnf(p399,plain,
    ( ~ hBOOL(fFalse)
    | hBOOL(X0) ),
    inference(factoring,[status(thm)],[p393]) ).

cnf(p1768,plain,
    hBOOL(X0),
    inference(resolution,[status(thm)],[p1763,p399]) ).

cnf(p465,plain,
    ~ hBOOL(fFalse),
    inference(demodulation,[status(thm)],[p463,c322]) ).

cnf(p1770,plain,
    $false,
    inference(resolution,[status(thm)],[p1768,p465]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SCT171+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04  % Command  : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/5.59  % Computer : n008.cluster.edu
% 0.13/5.59  % Model    : x86_64 x86_64
% 0.13/5.59  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.59  % Memory   : 8046.5625MB
% 0.13/5.59  % OS       : Linux 6.8.0-71-generic
% 0.13/5.59  % CPULimit : 300
% 0.13/5.59  % WCLimit  : 300
% 0.13/5.59  % DateTime : Thu Sep 24 09:01:01 UTC 2026
% 0.13/5.59  % CPUTime  : 
% 0.13/5.59  Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 49.41/12.18  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 49.41/12.18  % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------