Vampire---5.0.1.THM-Ref.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : SCT170+6 : TPTP v9.3.1. Released v5.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM

% Computer : n020.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 12:37:07 PM UTC 2026

% Result   : Theorem 33.55s 6.57s
% Output   : Refutation 39.52s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   48
%            Number of leaves      :   45
% Syntax   : Number of formulae    :  255 (  91 unt;  25 def)
%            Number of atoms       :  775 ( 246 equ)
%            Maximal formula atoms :   14 (   3 avg)
%            Number of connectives :  850 ( 330   ~; 444   |;  49   &)
%                                         (  15 <=>;  11  =>;   0  <=;   1 <~>)
%            Maximal formula depth :   14 (   5 avg)
%            Maximal term depth    :    9 (   2 avg)
%            Number of predicates  :    9 (   7 usr;   6 prp; 0-5 aty)
%            Number of functors    :   49 (  49 usr;  30 con; 0-4 aty)
%            Number of variables   :  471 (   0 sgn 463   !;   8   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(f70,axiom,
    ! [X0,X1,X2,X3] : hAPP(X0,X1,X2,ti(X0,X3)) = hAPP(X0,X1,X2,X3),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_c_hAPP_arg2) ).

fof(f77,axiom,
    ti(arrow_490897120le_alt,a) = a,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_v_a_____res) ).

fof(f78,axiom,
    ti(arrow_490897120le_alt,b) = b,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_v_b_____res) ).

fof(f79,axiom,
    ti(arrow_490897120le_alt,c) = c,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',tsy_v_c_____res) ).

fof(f80,axiom,
    hBOOL(hAPP(fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool),bool,hAPP(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),fun(fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool),bool),member(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),p),arrow_1111136790e_Prof)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__096P_A_058_AProf_096) ).

fof(f84,axiom,
    hBOOL(hAPP(list(arrow_490897120le_alt),bool,distinct(arrow_490897120le_alt),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),a),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),b),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),c),nil(arrow_490897120le_alt)))))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_dist) ).

fof(f92,axiom,
    ! [X0,X1,X2,X3,X4] :
      ( ti(arrow_490897120le_alt,X3) != ti(arrow_490897120le_alt,X4)
     => ( hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
       => ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4)))
        <=> ( ti(arrow_490897120le_alt,X0) != ti(arrow_490897120le_alt,X1)
            & ( ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X3)
             => hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2)) )
            & ( ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X3)
             => ( ( ti(arrow_490897120le_alt,X0) = ti(arrow_490897120le_alt,X3)
                 => ( ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X4)
                    | hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X4),X1)),X2)) ) )
                & ( ti(arrow_490897120le_alt,X0) != ti(arrow_490897120le_alt,X3)
                 => hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),X2)) ) ) ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_in__below) ).

fof(f125,axiom,
    ! [X0,X1] :
      ( X1 != nil(X0)
    <=> ? [X2,X3] : X1 = hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_neq__Nil__conv) ).

fof(f135,axiom,
    ! [X0,X1,X2,X3,X4,X5] :
      ( hBOOL(hAPP(fun(fun(X0,X1),bool),bool,hAPP(fun(X0,X1),fun(fun(fun(X0,X1),bool),bool),member(fun(X0,X1)),X3),hAPP(fun(X0,fun(X1,bool)),fun(fun(X0,X1),bool),hAPP(fun(X0,bool),fun(fun(X0,fun(X1,bool)),fun(fun(X0,X1),bool)),pi(X0,X1),X4),X5)))
     => ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X2),X4))
       => hBOOL(hAPP(fun(X1,bool),bool,hAPP(X1,fun(fun(X1,bool),bool),member(X1),hAPP(X0,X1,X3,X2)),hAPP(X0,fun(X1,bool),X5,X2))) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_Pi__mem) ).

fof(f156,axiom,
    ! [X0,X1,X2] :
      ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))
    <=> hBOOL(hAPP(X0,bool,X2,X1)) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_mem__def) ).

fof(f171,axiom,
    arrow_1111136790e_Prof = hAPP(fun(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool)),fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool),hAPP(fun(arrow_660593299e_indi,bool),fun(fun(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool)),fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool)),pi(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),top_top(fun(arrow_660593299e_indi,bool))),hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),fun(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool)),combk(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),arrow_660593299e_indi),arrow_2064824852le_Lin)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_Prof__def) ).

fof(f191,axiom,
    ! [X0,X1] : hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),top_top(fun(X0,bool)))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_iso__tuple__UNIV__I) ).

fof(f310,axiom,
    ! [X0,X1,X2] : hAPP(list(X0),X0,hd(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)) = ti(X0,X1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_hd_Osimps) ).

fof(f364,axiom,
    ! [X0,X1,X2] :
      ( hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))
    <=> ( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
        & hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_284_distinct_Osimps_I2_J) ).

fof(f370,axiom,
    ! [X0,X1] :
      ( X1 != nil(X0)
     => hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),hAPP(list(X0),X0,hd(X0),X1)),hAPP(list(X0),fun(X0,bool),set(X0),X1))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_290_hd__in__set) ).

fof(f450,axiom,
    ! [X0,X1,X2] : hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),hAPP(list(X0),fun(X0,bool),set(X0),X1)),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X1)))),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_370_set__subset__Cons) ).

fof(f460,axiom,
    ! [X0,X1,X2,X3] :
      ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),X2),X3))
     => ( hBOOL(hAPP(X0,bool,X2,X1))
       => hBOOL(hAPP(X0,bool,X3,X1)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_380_predicate1D) ).

fof(f607,axiom,
    ! [X0,X1] : hAPP(X0,X0,combi(X0),X1) = ti(X0,X1),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBI_1_1_U) ).

fof(f608,axiom,
    ! [X0,X1,X2,X3] : hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3) = ti(X1,X2),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_U) ).

fof(f617,conjecture,
    ! [X0] :
      ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),b)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,X0)))
    <=> hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),c)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,X0)),c),b))) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

fof(f618,negated_conjecture,
    ~ ! [X0] :
        ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),b)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,X0)))
      <=> hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),c)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,X0)),c),b))) ),
    inference(negated_conjecture,[status(cth)],[f617]) ).

fof(f635,plain,
    ! [X0,X1,X2,X3,X4] :
      ( ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4)))
      <=> ( ti(arrow_490897120le_alt,X0) != ti(arrow_490897120le_alt,X1)
          & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
            | ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X3) )
          & ( ( ( ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X4)
                | hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X4),X1)),X2))
                | ti(arrow_490897120le_alt,X3) != ti(arrow_490897120le_alt,X0) )
              & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),X2))
                | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X0) ) )
            | ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X3) ) ) )
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X4) ),
    inference(ennf_transformation,[],[f92]) ).

fof(f636,plain,
    ! [X0,X1,X2,X3,X4] :
      ( ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4)))
      <=> ( ti(arrow_490897120le_alt,X0) != ti(arrow_490897120le_alt,X1)
          & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
            | ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X3) )
          & ( ( ( ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X4)
                | hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X4),X1)),X2))
                | ti(arrow_490897120le_alt,X3) != ti(arrow_490897120le_alt,X0) )
              & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),X2))
                | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X0) ) )
            | ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X3) ) ) )
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X4) ),
    inference(flattening,[],[f635]) ).

fof(f667,plain,
    ! [X0,X1,X2,X3,X4,X5] :
      ( hBOOL(hAPP(fun(X1,bool),bool,hAPP(X1,fun(fun(X1,bool),bool),member(X1),hAPP(X0,X1,X3,X2)),hAPP(X0,fun(X1,bool),X5,X2)))
      | ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X2),X4))
      | ~ hBOOL(hAPP(fun(fun(X0,X1),bool),bool,hAPP(fun(X0,X1),fun(fun(fun(X0,X1),bool),bool),member(fun(X0,X1)),X3),hAPP(fun(X0,fun(X1,bool)),fun(fun(X0,X1),bool),hAPP(fun(X0,bool),fun(fun(X0,fun(X1,bool)),fun(fun(X0,X1),bool)),pi(X0,X1),X4),X5))) ),
    inference(ennf_transformation,[],[f135]) ).

fof(f668,plain,
    ! [X0,X1,X2,X3,X4,X5] :
      ( hBOOL(hAPP(fun(X1,bool),bool,hAPP(X1,fun(fun(X1,bool),bool),member(X1),hAPP(X0,X1,X3,X2)),hAPP(X0,fun(X1,bool),X5,X2)))
      | ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X2),X4))
      | ~ hBOOL(hAPP(fun(fun(X0,X1),bool),bool,hAPP(fun(X0,X1),fun(fun(fun(X0,X1),bool),bool),member(fun(X0,X1)),X3),hAPP(fun(X0,fun(X1,bool)),fun(fun(X0,X1),bool),hAPP(fun(X0,bool),fun(fun(X0,fun(X1,bool)),fun(fun(X0,X1),bool)),pi(X0,X1),X4),X5))) ),
    inference(flattening,[],[f667]) ).

fof(f808,plain,
    ! [X0,X1] :
      ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),hAPP(list(X0),X0,hd(X0),X1)),hAPP(list(X0),fun(X0,bool),set(X0),X1)))
      | nil(X0) = X1 ),
    inference(ennf_transformation,[],[f370]) ).

fof(f896,plain,
    ! [X0,X1,X2,X3] :
      ( hBOOL(hAPP(X0,bool,X3,X1))
      | ~ hBOOL(hAPP(X0,bool,X2,X1))
      | ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),X2),X3)) ),
    inference(ennf_transformation,[],[f460]) ).

fof(f897,plain,
    ! [X0,X1,X2,X3] :
      ( hBOOL(hAPP(X0,bool,X3,X1))
      | ~ hBOOL(hAPP(X0,bool,X2,X1))
      | ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),X2),X3)) ),
    inference(flattening,[],[f896]) ).

fof(f1036,plain,
    ? [X0] :
      ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),b)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,X0)))
    <~> hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),c)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,X0)),c),b))) ),
    inference(ennf_transformation,[],[f618]) ).

fof(f1037,definition,
    ! [X4,X1,X2,X0,X3] :
      ( sP0(X4,X1,X2,X0,X3)
    <=> ( ( ( ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X4)
            | hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X4),X1)),X2))
            | ti(arrow_490897120le_alt,X3) != ti(arrow_490897120le_alt,X0) )
          & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),X2))
            | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X0) ) )
        | ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X3) ) ),
    introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).

fof(f1038,plain,
    ! [X0,X1,X2,X3,X4] :
      ( ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4)))
      <=> ( ti(arrow_490897120le_alt,X0) != ti(arrow_490897120le_alt,X1)
          & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
            | ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X3) )
          & sP0(X4,X1,X2,X0,X3) ) )
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X4) ),
    inference(definition_folding,[],[f636,f1037]) ).

fof(f1054,plain,
    ! [X4,X1,X2,X0,X3] :
      ( ( sP0(X4,X1,X2,X0,X3)
        | ( ( ( ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X4)
              & ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X4),X1)),X2))
              & ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X0) )
            | ( ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),X2))
              & ti(arrow_490897120le_alt,X3) != ti(arrow_490897120le_alt,X0) ) )
          & ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X3) ) )
      & ( ( ( ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X4)
            | hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X4),X1)),X2))
            | ti(arrow_490897120le_alt,X3) != ti(arrow_490897120le_alt,X0) )
          & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),X2))
            | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X0) ) )
        | ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X3)
        | ~ sP0(X4,X1,X2,X0,X3) ) ),
    inference(nnf_transformation,[],[f1037]) ).

fof(f1055,plain,
    ! [X4,X1,X2,X0,X3] :
      ( ( sP0(X4,X1,X2,X0,X3)
        | ( ( ( ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X4)
              & ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X4),X1)),X2))
              & ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X0) )
            | ( ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),X2))
              & ti(arrow_490897120le_alt,X3) != ti(arrow_490897120le_alt,X0) ) )
          & ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X3) ) )
      & ( ( ( ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X4)
            | hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X4),X1)),X2))
            | ti(arrow_490897120le_alt,X3) != ti(arrow_490897120le_alt,X0) )
          & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),X2))
            | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X0) ) )
        | ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X3)
        | ~ sP0(X4,X1,X2,X0,X3) ) ),
    inference(flattening,[],[f1054]) ).

fof(f1056,plain,
    ! [X0,X1,X2,X3,X4] :
      ( ( sP0(X0,X1,X2,X3,X4)
        | ( ( ( ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X0)
              & ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),X2))
              & ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X4) )
            | ( ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X3),X1)),X2))
              & ti(arrow_490897120le_alt,X3) != ti(arrow_490897120le_alt,X4) ) )
          & ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X4) ) )
      & ( ( ( ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X0)
            | hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),X2))
            | ti(arrow_490897120le_alt,X3) != ti(arrow_490897120le_alt,X4) )
          & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X3),X1)),X2))
            | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X4) ) )
        | ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X4)
        | ~ sP0(X0,X1,X2,X3,X4) ) ),
    inference(rectify,[],[f1055]) ).

fof(f1057,plain,
    ! [X0,X1,X2,X3,X4] :
      ( ( ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4)))
          | ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X0)
          | ( ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
            & ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X3) )
          | ~ sP0(X4,X1,X2,X0,X3) )
        & ( ( ti(arrow_490897120le_alt,X0) != ti(arrow_490897120le_alt,X1)
            & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
              | ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X3) )
            & sP0(X4,X1,X2,X0,X3) )
          | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4))) ) )
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X4) ),
    inference(nnf_transformation,[],[f1038]) ).

fof(f1058,plain,
    ! [X0,X1,X2,X3,X4] :
      ( ( ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4)))
          | ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X0)
          | ( ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
            & ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X3) )
          | ~ sP0(X4,X1,X2,X0,X3) )
        & ( ( ti(arrow_490897120le_alt,X0) != ti(arrow_490897120le_alt,X1)
            & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
              | ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X3) )
            & sP0(X4,X1,X2,X0,X3) )
          | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4))) ) )
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X4) ),
    inference(flattening,[],[f1057]) ).

fof(f1091,plain,
    ! [X0,X1] :
      ( ( X1 != nil(X0)
        | ! [X2,X3] : hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3) != X1 )
      & ( ? [X2,X3] : X1 = hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3)
        | nil(X0) = X1 ) ),
    inference(nnf_transformation,[],[f125]) ).

fof(f1092,plain,
    ! [X0,X1] :
      ( ( X1 != nil(X0)
        | ! [X2,X3] : hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3) != X1 )
      & ( ? [X4,X5] : hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X4),X5) = X1
        | nil(X0) = X1 ) ),
    inference(rectify,[],[f1091]) ).

fof(f1093,plain,
    ! [X0,X1] :
      ( ( X1 != nil(X0)
        | ! [X2,X3] : hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3) != X1 )
      & ( hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),sK31(X0,X1)),sK32(X0,X1)) = X1
        | nil(X0) = X1 ) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK31,sK32]),skolemize(X4,sK31(X0,X1)),skolemize(X5,sK32(X0,X1))],[f1092]) ).

fof(f1119,plain,
    ! [X0,X1,X2] :
      ( ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))
        | ~ hBOOL(hAPP(X0,bool,X2,X1)) )
      & ( hBOOL(hAPP(X0,bool,X2,X1))
        | ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2)) ) ),
    inference(nnf_transformation,[],[f156]) ).

fof(f1219,plain,
    ! [X0,X1,X2] :
      ( ( hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))
        | hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
        | ~ hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) )
      & ( ( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
          & hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) )
        | ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))) ) ),
    inference(nnf_transformation,[],[f364]) ).

fof(f1220,plain,
    ! [X0,X1,X2] :
      ( ( hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))
        | hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
        | ~ hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) )
      & ( ( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
          & hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) )
        | ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))) ) ),
    inference(flattening,[],[f1219]) ).

fof(f1346,plain,
    ? [X0] :
      ( ( ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),c)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,X0)),c),b)))
        | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),b)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,X0))) )
      & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),c)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,X0)),c),b)))
        | hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),b)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,X0))) ) ),
    inference(nnf_transformation,[],[f1036]) ).

fof(f1347,plain,
    ( ( ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),c)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,sK219)),c),b)))
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),b)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,sK219))) )
    & ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),c)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,sK219)),c),b)))
      | hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),b)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,sK219))) ) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK219]),skolemize(X0,sK219)],[f1346]) ).

fof(f1417,plain,
    ! [X2,X3,X0,X1] : hAPP(X0,X1,X2,X3) = hAPP(X0,X1,X2,ti(X0,X3)),
    inference(cnf_transformation,[],[f70]) ).

fof(f1425,plain,
    a = ti(arrow_490897120le_alt,a),
    inference(cnf_transformation,[],[f77]) ).

fof(f1426,plain,
    b = ti(arrow_490897120le_alt,b),
    inference(cnf_transformation,[],[f78]) ).

fof(f1427,plain,
    c = ti(arrow_490897120le_alt,c),
    inference(cnf_transformation,[],[f79]) ).

fof(f1428,plain,
    hBOOL(hAPP(fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool),bool,hAPP(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),fun(fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool),bool),member(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),p),arrow_1111136790e_Prof)),
    inference(cnf_transformation,[],[f80]) ).

fof(f1432,plain,
    hBOOL(hAPP(list(arrow_490897120le_alt),bool,distinct(arrow_490897120le_alt),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),a),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),b),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),c),nil(arrow_490897120le_alt)))))),
    inference(cnf_transformation,[],[f84]) ).

fof(f1455,plain,
    ! [X2,X3,X0,X1,X4] :
      ( sP0(X0,X1,X2,X3,X4)
      | ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X4) ),
    inference(cnf_transformation,[],[f1056]) ).

fof(f1463,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ti(arrow_490897120le_alt,X1) != ti(arrow_490897120le_alt,X3)
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4)))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X4) ),
    inference(cnf_transformation,[],[f1058]) ).

fof(f1466,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4)))
      | ti(arrow_490897120le_alt,X1) = ti(arrow_490897120le_alt,X0)
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | ti(arrow_490897120le_alt,X3) = ti(arrow_490897120le_alt,X4) ),
    inference(cnf_transformation,[],[f1058]) ).

fof(f1543,plain,
    ! [X2,X3,X0,X1] :
      ( nil(X0) != X1
      | hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3) != X1 ),
    inference(cnf_transformation,[],[f1093]) ).

fof(f1555,plain,
    ! [X2,X3,X0,X1,X4,X5] :
      ( ~ hBOOL(hAPP(fun(fun(X0,X1),bool),bool,hAPP(fun(X0,X1),fun(fun(fun(X0,X1),bool),bool),member(fun(X0,X1)),X3),hAPP(fun(X0,fun(X1,bool)),fun(fun(X0,X1),bool),hAPP(fun(X0,bool),fun(fun(X0,fun(X1,bool)),fun(fun(X0,X1),bool)),pi(X0,X1),X4),X5)))
      | ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X2),X4))
      | hBOOL(hAPP(fun(X1,bool),bool,hAPP(X1,fun(fun(X1,bool),bool),member(X1),hAPP(X0,X1,X3,X2)),hAPP(X0,fun(X1,bool),X5,X2))) ),
    inference(cnf_transformation,[],[f668]) ).

fof(f1586,plain,
    ! [X2,X0,X1] :
      ( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))
      | hBOOL(hAPP(X0,bool,X2,X1)) ),
    inference(cnf_transformation,[],[f1119]) ).

fof(f1587,plain,
    ! [X2,X0,X1] :
      ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),X2))
      | ~ hBOOL(hAPP(X0,bool,X2,X1)) ),
    inference(cnf_transformation,[],[f1119]) ).

fof(f1607,plain,
    arrow_1111136790e_Prof = hAPP(fun(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool)),fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool),hAPP(fun(arrow_660593299e_indi,bool),fun(fun(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool)),fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool)),pi(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),top_top(fun(arrow_660593299e_indi,bool))),hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),fun(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool)),combk(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),arrow_660593299e_indi),arrow_2064824852le_Lin)),
    inference(cnf_transformation,[],[f171]) ).

fof(f1636,plain,
    ! [X0,X1] : hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),top_top(fun(X0,bool)))),
    inference(cnf_transformation,[],[f191]) ).

fof(f1850,plain,
    ! [X2,X0,X1] : ti(X0,X1) = hAPP(list(X0),X0,hd(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)),
    inference(cnf_transformation,[],[f310]) ).

fof(f1928,plain,
    ! [X2,X0,X1] :
      ( ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))
      | hBOOL(hAPP(list(X0),bool,distinct(X0),X2)) ),
    inference(cnf_transformation,[],[f1220]) ).

fof(f1929,plain,
    ! [X2,X0,X1] :
      ( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),X1),hAPP(list(X0),fun(X0,bool),set(X0),X2)))
      | ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))) ),
    inference(cnf_transformation,[],[f1220]) ).

fof(f1939,plain,
    ! [X0,X1] :
      ( hBOOL(hAPP(fun(X0,bool),bool,hAPP(X0,fun(fun(X0,bool),bool),member(X0),hAPP(list(X0),X0,hd(X0),X1)),hAPP(list(X0),fun(X0,bool),set(X0),X1)))
      | nil(X0) = X1 ),
    inference(cnf_transformation,[],[f808]) ).

fof(f2096,plain,
    ! [X2,X0,X1] : hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),hAPP(list(X0),fun(X0,bool),set(X0),X1)),hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X1)))),
    inference(cnf_transformation,[],[f450]) ).

fof(f2109,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),X2),X3))
      | ~ hBOOL(hAPP(X0,bool,X2,X1))
      | hBOOL(hAPP(X0,bool,X3,X1)) ),
    inference(cnf_transformation,[],[f897]) ).

fof(f2312,plain,
    ! [X0,X1] : ti(X0,X1) = hAPP(X0,X0,combi(X0),X1),
    inference(cnf_transformation,[],[f607]) ).

fof(f2313,plain,
    ! [X2,X3,X0,X1] : ti(X1,X2) = hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3),
    inference(cnf_transformation,[],[f608]) ).

fof(f2322,plain,
    ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),c)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,sK219)),c),b)))
    | hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),b)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,sK219))) ),
    inference(cnf_transformation,[],[f1347]) ).

fof(f2323,plain,
    ( ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),c)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,sK219)),c),b)))
    | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),a),b)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),p,sK219))) ),
    inference(cnf_transformation,[],[f1347]) ).

fof(f2393,plain,
    ! [X2,X3,X0,X1] : hAPP(X0,X1,X2,X3) = hAPP(X0,X1,X2,hAPP(X0,X0,combi(X0),X3)),
    inference(definition_unfolding,[],[f1417,f2312]) ).

fof(f2401,plain,
    a = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),a),
    inference(definition_unfolding,[],[f1425,f2312]) ).

fof(f2402,plain,
    b = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),b),
    inference(definition_unfolding,[],[f1426,f2312]) ).

fof(f2403,plain,
    c = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),c),
    inference(definition_unfolding,[],[f1427,f2312]) ).

fof(f2423,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) != hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4)
      | sP0(X0,X1,X2,X3,X4) ),
    inference(definition_unfolding,[],[f1455,f2312,f2312]) ).

fof(f2426,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(definition_unfolding,[],[f1466,f2312,f2312,f2312,f2312]) ).

fof(f2429,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) != hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3)
      | hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X4)))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(definition_unfolding,[],[f1463,f2312,f2312,f2312,f2312]) ).

fof(f2514,plain,
    ! [X2,X0,X1] : hAPP(list(X0),X0,hd(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)) = hAPP(X0,X0,combi(X0),X1),
    inference(definition_unfolding,[],[f1850,f2312]) ).

fof(f2579,plain,
    ! [X2,X3,X0,X1] : hAPP(X0,X1,hAPP(X1,fun(X0,X1),combk(X1,X0),X2),X3) = hAPP(X1,X1,combi(X1),X2),
    inference(definition_unfolding,[],[f2313,f2312]) ).

fof(f2584,plain,
    ! [X2,X3,X0] : nil(X0) != hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X3),
    inference(equality_resolution,[],[f1543]) ).

fof(f2704,definition,
    sF220 = product_prod(arrow_490897120le_alt,arrow_490897120le_alt),
    introduced(definition,[new_symbols(definition,[sF220])],[function_definition]) ).

fof(f2705,plain,
    product_prod(arrow_490897120le_alt,arrow_490897120le_alt) = sF220,
    inference(reorient_equations,[],[f2704]) ).

fof(f2706,definition,
    sF221 = fun(sF220,bool),
    introduced(definition,[new_symbols(definition,[sF221])],[function_definition]) ).

fof(f2707,plain,
    fun(sF220,bool) = sF221,
    inference(reorient_equations,[],[f2706]) ).

fof(f2708,definition,
    sF222 = fun(sF221,bool),
    introduced(definition,[new_symbols(definition,[sF222])],[function_definition]) ).

fof(f2709,plain,
    fun(sF221,bool) = sF222,
    inference(reorient_equations,[],[f2708]) ).

fof(f2710,definition,
    sF223 = member(sF220),
    introduced(definition,[new_symbols(definition,[sF223])],[function_definition]) ).

fof(f2711,plain,
    member(sF220) = sF223,
    inference(reorient_equations,[],[f2710]) ).

fof(f2712,definition,
    sF224 = fun(arrow_490897120le_alt,sF220),
    introduced(definition,[new_symbols(definition,[sF224])],[function_definition]) ).

fof(f2713,plain,
    fun(arrow_490897120le_alt,sF220) = sF224,
    inference(reorient_equations,[],[f2712]) ).

fof(f2714,definition,
    sF225 = product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),
    introduced(definition,[new_symbols(definition,[sF225])],[function_definition]) ).

fof(f2715,plain,
    product_Pair(arrow_490897120le_alt,arrow_490897120le_alt) = sF225,
    inference(reorient_equations,[],[f2714]) ).

fof(f2716,definition,
    sF226 = hAPP(arrow_490897120le_alt,sF224,sF225,a),
    introduced(definition,[new_symbols(definition,[sF226])],[function_definition]) ).

fof(f2717,plain,
    hAPP(arrow_490897120le_alt,sF224,sF225,a) = sF226,
    inference(reorient_equations,[],[f2716]) ).

fof(f2718,definition,
    sF227 = hAPP(arrow_490897120le_alt,sF220,sF226,c),
    introduced(definition,[new_symbols(definition,[sF227])],[function_definition]) ).

fof(f2719,plain,
    hAPP(arrow_490897120le_alt,sF220,sF226,c) = sF227,
    inference(reorient_equations,[],[f2718]) ).

fof(f2720,definition,
    sF228 = hAPP(sF220,sF222,sF223,sF227),
    introduced(definition,[new_symbols(definition,[sF228])],[function_definition]) ).

fof(f2721,plain,
    hAPP(sF220,sF222,sF223,sF227) = sF228,
    inference(reorient_equations,[],[f2720]) ).

fof(f2722,definition,
    sF229 = fun(arrow_490897120le_alt,sF221),
    introduced(definition,[new_symbols(definition,[sF229])],[function_definition]) ).

fof(f2723,plain,
    fun(arrow_490897120le_alt,sF221) = sF229,
    inference(reorient_equations,[],[f2722]) ).

fof(f2724,definition,
    sF230 = fun(arrow_490897120le_alt,sF229),
    introduced(definition,[new_symbols(definition,[sF230])],[function_definition]) ).

fof(f2725,plain,
    fun(arrow_490897120le_alt,sF229) = sF230,
    inference(reorient_equations,[],[f2724]) ).

fof(f2726,definition,
    sF231 = hAPP(arrow_660593299e_indi,sF221,p,sK219),
    introduced(definition,[new_symbols(definition,[sF231])],[function_definition]) ).

fof(f2727,plain,
    hAPP(arrow_660593299e_indi,sF221,p,sK219) = sF231,
    inference(reorient_equations,[],[f2726]) ).

fof(f2728,definition,
    sF232 = hAPP(sF221,sF230,arrow_1322701812_below,sF231),
    introduced(definition,[new_symbols(definition,[sF232])],[function_definition]) ).

fof(f2729,plain,
    hAPP(sF221,sF230,arrow_1322701812_below,sF231) = sF232,
    inference(reorient_equations,[],[f2728]) ).

fof(f2730,definition,
    sF233 = hAPP(arrow_490897120le_alt,sF229,sF232,c),
    introduced(definition,[new_symbols(definition,[sF233])],[function_definition]) ).

fof(f2731,plain,
    hAPP(arrow_490897120le_alt,sF229,sF232,c) = sF233,
    inference(reorient_equations,[],[f2730]) ).

fof(f2732,definition,
    sF234 = hAPP(arrow_490897120le_alt,sF221,sF233,b),
    introduced(definition,[new_symbols(definition,[sF234])],[function_definition]) ).

fof(f2733,plain,
    hAPP(arrow_490897120le_alt,sF221,sF233,b) = sF234,
    inference(reorient_equations,[],[f2732]) ).

fof(f2734,definition,
    sF235 = hAPP(sF221,bool,sF228,sF234),
    introduced(definition,[new_symbols(definition,[sF235])],[function_definition]) ).

fof(f2735,plain,
    hAPP(sF221,bool,sF228,sF234) = sF235,
    inference(reorient_equations,[],[f2734]) ).

fof(f2736,definition,
    sF236 = hAPP(arrow_490897120le_alt,sF220,sF226,b),
    introduced(definition,[new_symbols(definition,[sF236])],[function_definition]) ).

fof(f2737,plain,
    hAPP(arrow_490897120le_alt,sF220,sF226,b) = sF236,
    inference(reorient_equations,[],[f2736]) ).

fof(f2738,definition,
    sF237 = hAPP(sF220,sF222,sF223,sF236),
    introduced(definition,[new_symbols(definition,[sF237])],[function_definition]) ).

fof(f2739,plain,
    hAPP(sF220,sF222,sF223,sF236) = sF237,
    inference(reorient_equations,[],[f2738]) ).

fof(f2740,definition,
    sF238 = hAPP(sF221,bool,sF237,sF231),
    introduced(definition,[new_symbols(definition,[sF238])],[function_definition]) ).

fof(f2741,plain,
    hAPP(sF221,bool,sF237,sF231) = sF238,
    inference(reorient_equations,[],[f2740]) ).

fof(f2742,plain,
    ( ~ hBOOL(sF235)
    | ~ hBOOL(sF238) ),
    inference(definition_folding,[],[f2323,f2741,f2727,f2707,f2705,f2739,f2737,f2717,f2715,f2713,f2705,f2705,f2711,f2705,f2709,f2707,f2705,f2705,f2707,f2705,f2735,f2733,f2731,f2729,f2727,f2707,f2705,f2725,f2723,f2707,f2705,f2707,f2705,f2723,f2707,f2705,f2707,f2705,f2721,f2719,f2717,f2715,f2713,f2705,f2705,f2711,f2705,f2709,f2707,f2705,f2705,f2707,f2705]) ).

fof(f2743,plain,
    ( hBOOL(sF235)
    | hBOOL(sF238) ),
    inference(definition_folding,[],[f2322,f2741,f2727,f2707,f2705,f2739,f2737,f2717,f2715,f2713,f2705,f2705,f2711,f2705,f2709,f2707,f2705,f2705,f2707,f2705,f2735,f2733,f2731,f2729,f2727,f2707,f2705,f2725,f2723,f2707,f2705,f2707,f2705,f2723,f2707,f2705,f2707,f2705,f2721,f2719,f2717,f2715,f2713,f2705,f2705,f2711,f2705,f2709,f2707,f2705,f2705,f2707,f2705]) ).

fof(f2749,definition,
    ( spl239_1
  <=> hBOOL(sF238) ),
    introduced(definition,[new_symbols(definition,[spl239_1])],[avatar_definition]) ).

fof(f2750,plain,
    ( ~ hBOOL(sF238)
    | spl239_1 ),
    inference(avatar_component_clause,[],[f2749]) ).

fof(f2751,plain,
    ( hBOOL(sF238)
    | ~ spl239_1 ),
    inference(avatar_component_clause,[],[f2749]) ).

fof(f2753,definition,
    ( spl239_2
  <=> hBOOL(sF235) ),
    introduced(definition,[new_symbols(definition,[spl239_2])],[avatar_definition]) ).

fof(f2754,plain,
    ( ~ hBOOL(sF235)
    | spl239_2 ),
    inference(avatar_component_clause,[],[f2753]) ).

fof(f2755,plain,
    ( hBOOL(sF235)
    | ~ spl239_2 ),
    inference(avatar_component_clause,[],[f2753]) ).

fof(f2756,plain,
    ( spl239_1
    | spl239_2 ),
    inference(avatar_split_clause,[],[f2743,f2753,f2749]) ).

fof(f2757,plain,
    ( ~ spl239_1
    | ~ spl239_2 ),
    inference(avatar_split_clause,[],[f2742,f2753,f2749]) ).

fof(f2888,plain,
    ! [X2,X3,X0,X1] : sP0(X0,X1,X2,X3,X1),
    inference(equality_resolution,[],[f2423]) ).

fof(f3003,plain,
    ! [X2,X0,X1] :
      ( ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X2),X1)))
      | ~ hBOOL(hAPP(X0,bool,hAPP(list(X0),fun(X0,bool),set(X0),X1),X2)) ),
    inference(resolution,[],[f1587,f1929]) ).

fof(f3022,plain,
    hBOOL(hAPP(list(arrow_490897120le_alt),bool,distinct(arrow_490897120le_alt),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),b),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),c),nil(arrow_490897120le_alt))))),
    inference(resolution,[],[f1928,f1432]) ).

fof(f3041,definition,
    ( spl239_4
  <=> b = c ),
    introduced(definition,[new_symbols(definition,[spl239_4])],[avatar_definition]) ).

fof(f3042,plain,
    ( b = c
    | ~ spl239_4 ),
    inference(avatar_component_clause,[],[f3041]) ).

fof(f3043,plain,
    ( b != c
    | spl239_4 ),
    inference(avatar_component_clause,[],[f3041]) ).

fof(f3115,definition,
    ( spl239_6
  <=> a = c ),
    introduced(definition,[new_symbols(definition,[spl239_6])],[avatar_definition]) ).

fof(f3116,plain,
    ( a = c
    | ~ spl239_6 ),
    inference(avatar_component_clause,[],[f3115]) ).

fof(f3117,plain,
    ( a != c
    | spl239_6 ),
    inference(avatar_component_clause,[],[f3115]) ).

fof(f3227,plain,
    ! [X0,X1] :
      ( ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),hAPP(list(X0),X0,hd(X0),X1)),X1)))
      | nil(X0) = X1 ),
    inference(resolution,[],[f1939,f1929]) ).

fof(f3228,plain,
    ! [X0,X1] :
      ( hBOOL(hAPP(X0,bool,hAPP(list(X0),fun(X0,bool),set(X0),X1),hAPP(list(X0),X0,hd(X0),X1)))
      | nil(X0) = X1 ),
    inference(resolution,[],[f1939,f1586]) ).

fof(f3310,plain,
    ~ hBOOL(hAPP(arrow_490897120le_alt,bool,hAPP(list(arrow_490897120le_alt),fun(arrow_490897120le_alt,bool),set(arrow_490897120le_alt),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),b),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),c),nil(arrow_490897120le_alt)))),a)),
    inference(resolution,[],[f3003,f1432]) ).

fof(f3822,definition,
    ( spl239_7
  <=> hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),sF231),arrow_2064824852le_Lin)) ),
    introduced(definition,[new_symbols(definition,[spl239_7])],[avatar_definition]) ).

fof(f3823,plain,
    ( hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),sF231),arrow_2064824852le_Lin))
    | ~ spl239_7 ),
    inference(avatar_component_clause,[],[f3822]) ).

fof(f3824,plain,
    ( ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),sF231),arrow_2064824852le_Lin))
    | spl239_7 ),
    inference(avatar_component_clause,[],[f3822]) ).

fof(f3839,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,fun(sF220,bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(sF220,bool)),hAPP(fun(sF220,bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(sF220,bool))),arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(superposition,[],[f2426,f2705]) ).

fof(f3846,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF221),hAPP(sF221,fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF221)),arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3839,f2707]) ).

fof(f3854,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,fun(arrow_490897120le_alt,sF229),arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3846,f2723]) ).

fof(f3862,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3854,f2725]) ).

fof(f3870,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),sF225,X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3862,f2715]) ).

fof(f3878,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3870,f2713]) ).

fof(f3886,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3878,f2711]) ).

fof(f3894,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X4)),X2))
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3886,f2709]) ).

fof(f3902,plain,
    ! [X2,X3,X0,X1,X4] :
      ( ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),sF225,X0),X4)),X2))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3894,f2715]) ).

fof(f3910,plain,
    ! [X2,X3,X0,X1,X4] :
      ( ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X4)),X2))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3902,f2713]) ).

fof(f3918,plain,
    ! [X2,X3,X0,X1,X4] :
      ( ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X4)),X2))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3910,f2711]) ).

fof(f3926,plain,
    ! [X2,X3,X0,X1,X4] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X4)),X2))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3918,f2707]) ).

fof(f3934,plain,
    ! [X2,X3,X0,X1,X4] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X4)),X2))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ sP0(X4,X1,X2,X0,X3)
      | ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3926,f2709]) ).

fof(f3942,plain,
    ! [X2,X3,X0,X1,X4] :
      ( ~ hBOOL(hAPP(fun(sF221,bool),bool,hAPP(sF221,fun(fun(sF221,bool),bool),member(sF221),X2),arrow_2064824852le_Lin))
      | ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X4)),X2))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ sP0(X4,X1,X2,X0,X3)
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3934,f2707]) ).

fof(f3950,plain,
    ! [X2,X3,X0,X1,X4] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X4)))
      | ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X4)),X2))
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ sP0(X4,X1,X2,X0,X3)
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X4) ),
    inference(forward_demodulation,[],[f3942,f2709]) ).

fof(f3983,plain,
    ! [X2,X3,X0,X1] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X0)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X1),X2),X3)))
      | ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X3)),X1))
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X1),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),a) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ sP0(X3,X0,X1,a,X2)
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X2) ),
    inference(superposition,[],[f3950,f2717]) ).

fof(f3995,plain,
    ! [X2,X3,X0,X1] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X0)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X1),X2),X3)))
      | a = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X3)),X1))
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X1),arrow_2064824852le_Lin))
      | ~ sP0(X3,X0,X1,a,X2)
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X2) ),
    inference(forward_demodulation,[],[f3983,f2401]) ).

fof(f4351,plain,
    hBOOL(hAPP(fun(fun(arrow_660593299e_indi,fun(sF220,bool)),bool),bool,hAPP(fun(arrow_660593299e_indi,fun(sF220,bool)),fun(fun(fun(arrow_660593299e_indi,fun(sF220,bool)),bool),bool),member(fun(arrow_660593299e_indi,fun(sF220,bool))),p),arrow_1111136790e_Prof)),
    inference(superposition,[],[f1428,f2705]) ).

fof(f4352,plain,
    hBOOL(hAPP(fun(fun(arrow_660593299e_indi,sF221),bool),bool,hAPP(fun(arrow_660593299e_indi,sF221),fun(fun(fun(arrow_660593299e_indi,sF221),bool),bool),member(fun(arrow_660593299e_indi,sF221)),p),arrow_1111136790e_Prof)),
    inference(forward_demodulation,[],[f4351,f2707]) ).

fof(f4443,plain,
    ! [X2,X0,X1] :
      ( hBOOL(hAPP(X0,bool,hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)),hAPP(X0,X0,combi(X0),X1)))
      | nil(X0) = hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2) ),
    inference(superposition,[],[f3228,f2514]) ).

fof(f4444,plain,
    ! [X2,X0,X1] :
      ( ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),hAPP(X0,X0,combi(X0),X1)),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2))))
      | nil(X0) = hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2) ),
    inference(superposition,[],[f3227,f2514]) ).

fof(f4452,plain,
    ! [X2,X0,X1] : ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),hAPP(X0,X0,combi(X0),X1)),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))),
    inference(forward_subsumption_resolution,[],[f4444,f2584]) ).

fof(f4453,plain,
    ! [X2,X0,X1] : hBOOL(hAPP(X0,bool,hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)),hAPP(X0,X0,combi(X0),X1))),
    inference(forward_subsumption_resolution,[],[f4443,f2584]) ).

fof(f4457,plain,
    ! [X2,X0,X1] : ~ hBOOL(hAPP(list(X0),bool,distinct(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)))),
    inference(forward_demodulation,[],[f4452,f2393]) ).

fof(f4458,plain,
    ! [X2,X0,X1] : hBOOL(hAPP(X0,bool,hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X1),X2)),X1)),
    inference(forward_demodulation,[],[f4453,f2393]) ).

fof(f6012,plain,
    ! [X2,X0,X1] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,sF227),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X0),X1),X2)))
      | a = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),c)
      | ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X2)),X0))
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X0),arrow_2064824852le_Lin))
      | ~ sP0(X2,c,X0,a,X1)
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X2) ),
    inference(superposition,[],[f3995,f2719]) ).

fof(f6024,plain,
    ! [X2,X0,X1] :
      ( hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X0),X1),X2)))
      | a = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),c)
      | ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X2)),X0))
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X0),arrow_2064824852le_Lin))
      | ~ sP0(X2,c,X0,a,X1)
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X2) ),
    inference(forward_demodulation,[],[f6012,f2721]) ).

fof(f6028,plain,
    ! [X2,X0,X1] :
      ( a = c
      | hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X0),X1),X2)))
      | ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X2)),X0))
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X0),arrow_2064824852le_Lin))
      | ~ sP0(X2,c,X0,a,X1)
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X2) ),
    inference(forward_demodulation,[],[f6024,f2403]) ).

fof(f6030,plain,
    ( ! [X2,X0,X1] :
        ( hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X0),X1),X2)))
        | ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X2)),X0))
        | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X0),arrow_2064824852le_Lin))
        | ~ sP0(X2,c,X0,a,X1)
        | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X2) )
    | spl239_6 ),
    inference(forward_subsumption_resolution,[],[f6028,f3117]) ).

fof(f6042,plain,
    ( ! [X0,X1] :
        ( hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,sF232,X0),X1)))
        | ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X1)),sF231))
        | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),sF231),arrow_2064824852le_Lin))
        | ~ sP0(X1,c,sF231,a,X0)
        | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0) )
    | spl239_6 ),
    inference(superposition,[],[f6030,f2729]) ).

fof(f6889,plain,
    ! [X2,X3,X0,X1] :
      ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X3)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X1)))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(equality_resolution,[],[f2429]) ).

fof(f6890,plain,
    ! [X2,X3,X0,X1] :
      ( hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X3)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X1)))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f6889,f2715]) ).

fof(f6903,plain,
    ! [X2,X3,X0,X1] :
      ( hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X3)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X1)))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f6890,f2705]) ).

fof(f6916,plain,
    ! [X2,X3,X0,X1] :
      ( hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X3)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X1)))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f6903,f2713]) ).

fof(f6929,plain,
    ! [X2,X3,X0,X1] :
      ( hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X3)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X1)))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f6916,f2711]) ).

fof(f6942,plain,
    ! [X2,X3,X0,X1] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X3)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X1)))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f6929,f2707]) ).

fof(f6955,plain,
    ! [X2,X3,X0,X1] :
      ( hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool,hAPP(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),member(product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),hAPP(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,product_prod(arrow_490897120le_alt,arrow_490897120le_alt)),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X3)),hAPP(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),arrow_1322701812_below,X2),X3),X1)))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f6942,f2709]) ).

fof(f6968,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(fun(sF220,bool),bool,hAPP(sF220,fun(fun(sF220,bool),bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X3)),hAPP(arrow_490897120le_alt,fun(sF220,bool),hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(sF220,bool)),hAPP(fun(sF220,bool),fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,fun(sF220,bool))),arrow_1322701812_below,X2),X3),X1)))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f6955,f2705]) ).

fof(f6981,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X3)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF221),hAPP(sF221,fun(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF221)),arrow_1322701812_below,X2),X3),X1)))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f6968,f2707]) ).

fof(f6994,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X3)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,fun(arrow_490897120le_alt,sF229),arrow_1322701812_below,X2),X3),X1)))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f6981,f2723]) ).

fof(f7007,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),product_Pair(arrow_490897120le_alt,arrow_490897120le_alt),X0),X3)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X1)))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f6994,f2725]) ).

fof(f7020,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,fun(arrow_490897120le_alt,sF220),sF225,X0),X3)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X1)))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f7007,f2715]) ).

fof(f7033,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),member(sF220),hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X3)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X1)))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f7020,f2713]) ).

fof(f7046,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,fun(sF221,bool),sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X3)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X1)))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f7033,f2711]) ).

fof(f7059,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X3)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X1)))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | ~ hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),X2),arrow_2064824852le_Lin))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f7046,f2709]) ).

fof(f7072,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),X2),arrow_2064824852le_Lin))
      | ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X3)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X1)))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f7059,f2705]) ).

fof(f7085,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(fun(sF221,bool),bool,hAPP(sF221,fun(fun(sF221,bool),bool),member(sF221),X2),arrow_2064824852le_Lin))
      | ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X3)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X1)))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f7072,f2707]) ).

fof(f7098,plain,
    ! [X2,X3,X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X3)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X2),X3),X1)))
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X2),arrow_2064824852le_Lin))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,hAPP(arrow_490897120le_alt,sF224,sF225,X0),X1)),X2))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X3) ),
    inference(forward_demodulation,[],[f7085,f2709]) ).

fof(f7127,plain,
    ! [X2,X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X0)),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X1),X0),X2)))
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X1),arrow_2064824852le_Lin))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X2)),X1))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X2) ),
    inference(superposition,[],[f7098,f2717]) ).

fof(f7254,plain,
    ! [X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,sF227),hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X0),c),X1)))
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X0),arrow_2064824852le_Lin))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X1)),X0))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),c) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) ),
    inference(superposition,[],[f7127,f2719]) ).

fof(f7268,plain,
    ! [X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X0),c),X1)))
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X0),arrow_2064824852le_Lin))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X1)),X0))
      | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),c) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) ),
    inference(forward_demodulation,[],[f7254,f2721]) ).

fof(f7274,plain,
    ! [X0,X1] :
      ( ~ hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,hAPP(sF221,sF230,arrow_1322701812_below,X0),c),X1)))
      | c = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1)
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),X0),arrow_2064824852le_Lin))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X1)),X0)) ),
    inference(forward_demodulation,[],[f7268,f2403]) ).

fof(f7295,plain,
    ! [X0] :
      ( ~ hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,sF232,c),X0)))
      | c = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
      | ~ hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),sF231),arrow_2064824852le_Lin))
      | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X0)),sF231)) ),
    inference(superposition,[],[f7274,f2729]) ).

fof(f10459,plain,
    ! [X2,X3,X0,X1] :
      ( hBOOL(hAPP(X0,bool,hAPP(list(X0),fun(X0,bool),set(X0),hAPP(list(X0),list(X0),hAPP(X0,fun(list(X0),list(X0)),cons(X0),X3),X1)),X2))
      | ~ hBOOL(hAPP(X0,bool,hAPP(list(X0),fun(X0,bool),set(X0),X1),X2)) ),
    inference(resolution,[],[f2109,f2096]) ).

fof(f10493,plain,
    ~ hBOOL(hAPP(arrow_490897120le_alt,bool,hAPP(list(arrow_490897120le_alt),fun(arrow_490897120le_alt,bool),set(arrow_490897120le_alt),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),c),nil(arrow_490897120le_alt))),a)),
    inference(resolution,[],[f10459,f3310]) ).

fof(f13387,plain,
    ! [X0,X1] :
      ( ~ hBOOL(hAPP(fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool),bool,hAPP(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),fun(fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool),bool),member(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),X0),arrow_1111136790e_Prof))
      | ~ hBOOL(hAPP(fun(arrow_660593299e_indi,bool),bool,hAPP(arrow_660593299e_indi,fun(fun(arrow_660593299e_indi,bool),bool),member(arrow_660593299e_indi),X1),top_top(fun(arrow_660593299e_indi,bool))))
      | hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),X0,X1)),hAPP(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),fun(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool)),combk(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),arrow_660593299e_indi),arrow_2064824852le_Lin),X1))) ),
    inference(superposition,[],[f1555,f1607]) ).

fof(f13391,plain,
    ! [X0,X1] :
      ( ~ hBOOL(hAPP(fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool),bool,hAPP(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),fun(fun(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),bool),bool),member(fun(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool))),X0),arrow_1111136790e_Prof))
      | hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),X0,X1)),hAPP(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),fun(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool)),combk(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),arrow_660593299e_indi),arrow_2064824852le_Lin),X1))) ),
    inference(forward_subsumption_resolution,[],[f13387,f1636]) ).

fof(f13400,plain,
    ! [X0,X1] :
      ( ~ hBOOL(hAPP(fun(fun(arrow_660593299e_indi,fun(sF220,bool)),bool),bool,hAPP(fun(arrow_660593299e_indi,fun(sF220,bool)),fun(fun(fun(arrow_660593299e_indi,fun(sF220,bool)),bool),bool),member(fun(arrow_660593299e_indi,fun(sF220,bool))),X0),arrow_1111136790e_Prof))
      | hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),X0,X1)),hAPP(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),fun(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool)),combk(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),arrow_660593299e_indi),arrow_2064824852le_Lin),X1))) ),
    inference(forward_demodulation,[],[f13391,f2705]) ).

fof(f13407,plain,
    ! [X0,X1] :
      ( ~ hBOOL(hAPP(fun(fun(arrow_660593299e_indi,sF221),bool),bool,hAPP(fun(arrow_660593299e_indi,sF221),fun(fun(fun(arrow_660593299e_indi,sF221),bool),bool),member(fun(arrow_660593299e_indi,sF221)),X0),arrow_1111136790e_Prof))
      | hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),X0,X1)),hAPP(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),fun(arrow_660593299e_indi,fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool)),combk(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),arrow_660593299e_indi),arrow_2064824852le_Lin),X1))) ),
    inference(forward_demodulation,[],[f13400,f2707]) ).

fof(f13411,plain,
    ! [X0,X1] :
      ( hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),X0,X1)),hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),combi(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool)),arrow_2064824852le_Lin)))
      | ~ hBOOL(hAPP(fun(fun(arrow_660593299e_indi,sF221),bool),bool,hAPP(fun(arrow_660593299e_indi,sF221),fun(fun(fun(arrow_660593299e_indi,sF221),bool),bool),member(fun(arrow_660593299e_indi,sF221)),X0),arrow_1111136790e_Prof)) ),
    inference(forward_demodulation,[],[f13407,f2579]) ).

fof(f13414,plain,
    ! [X0,X1] :
      ( hBOOL(hAPP(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool,hAPP(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),fun(fun(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),bool),bool),member(fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool)),hAPP(arrow_660593299e_indi,fun(product_prod(arrow_490897120le_alt,arrow_490897120le_alt),bool),X0,X1)),arrow_2064824852le_Lin))
      | ~ hBOOL(hAPP(fun(fun(arrow_660593299e_indi,sF221),bool),bool,hAPP(fun(arrow_660593299e_indi,sF221),fun(fun(fun(arrow_660593299e_indi,sF221),bool),bool),member(fun(arrow_660593299e_indi,sF221)),X0),arrow_1111136790e_Prof)) ),
    inference(forward_demodulation,[],[f13411,f2393]) ).

fof(f13417,plain,
    ! [X0,X1] :
      ( hBOOL(hAPP(fun(fun(sF220,bool),bool),bool,hAPP(fun(sF220,bool),fun(fun(fun(sF220,bool),bool),bool),member(fun(sF220,bool)),hAPP(arrow_660593299e_indi,fun(sF220,bool),X0,X1)),arrow_2064824852le_Lin))
      | ~ hBOOL(hAPP(fun(fun(arrow_660593299e_indi,sF221),bool),bool,hAPP(fun(arrow_660593299e_indi,sF221),fun(fun(fun(arrow_660593299e_indi,sF221),bool),bool),member(fun(arrow_660593299e_indi,sF221)),X0),arrow_1111136790e_Prof)) ),
    inference(forward_demodulation,[],[f13414,f2705]) ).

fof(f13419,plain,
    ! [X0,X1] :
      ( hBOOL(hAPP(fun(sF221,bool),bool,hAPP(sF221,fun(fun(sF221,bool),bool),member(sF221),hAPP(arrow_660593299e_indi,sF221,X0,X1)),arrow_2064824852le_Lin))
      | ~ hBOOL(hAPP(fun(fun(arrow_660593299e_indi,sF221),bool),bool,hAPP(fun(arrow_660593299e_indi,sF221),fun(fun(fun(arrow_660593299e_indi,sF221),bool),bool),member(fun(arrow_660593299e_indi,sF221)),X0),arrow_1111136790e_Prof)) ),
    inference(forward_demodulation,[],[f13417,f2707]) ).

fof(f13421,plain,
    ! [X0,X1] :
      ( ~ hBOOL(hAPP(fun(fun(arrow_660593299e_indi,sF221),bool),bool,hAPP(fun(arrow_660593299e_indi,sF221),fun(fun(fun(arrow_660593299e_indi,sF221),bool),bool),member(fun(arrow_660593299e_indi,sF221)),X0),arrow_1111136790e_Prof))
      | hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),hAPP(arrow_660593299e_indi,sF221,X0,X1)),arrow_2064824852le_Lin)) ),
    inference(forward_demodulation,[],[f13419,f2709]) ).

fof(f13422,plain,
    ! [X0] : hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),hAPP(arrow_660593299e_indi,sF221,p,X0)),arrow_2064824852le_Lin)),
    inference(resolution,[],[f13421,f4352]) ).

fof(f13466,plain,
    hBOOL(hAPP(sF222,bool,hAPP(sF221,fun(sF222,bool),member(sF221),sF231),arrow_2064824852le_Lin)),
    inference(superposition,[],[f13422,f2727]) ).

fof(f13468,plain,
    ( $false
    | spl239_7 ),
    inference(forward_subsumption_resolution,[],[f13466,f3824]) ).

fof(f13469,plain,
    spl239_7,
    inference(avatar_contradiction_clause,[],[f13468]) ).

fof(f13483,plain,
    ( ! [X0,X1] :
        ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X1)),sF231))
        | hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,sF232,X0),X1)))
        | ~ sP0(X1,c,sF231,a,X0)
        | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X1) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0) )
    | spl239_6
    | ~ spl239_7 ),
    inference(forward_subsumption_resolution,[],[f6042,f3823]) ).

fof(f13488,plain,
    ( ! [X0] :
        ( ~ hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,sF232,c),X0)))
        | c = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
        | hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X0)),sF231)) )
    | ~ spl239_7 ),
    inference(forward_subsumption_resolution,[],[f7295,f3823]) ).

fof(f13502,plain,
    ( ! [X0] :
        ( hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,hAPP(arrow_490897120le_alt,sF220,sF226,X0)),sF231))
        | c = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
        | ~ hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,sF233,X0))) )
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13488,f2731]) ).

fof(f13578,plain,
    ( hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,sF236),sF231))
    | c = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),b)
    | ~ hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,sF233,b)))
    | ~ spl239_7 ),
    inference(superposition,[],[f13502,f2737]) ).

fof(f13581,plain,
    ( hBOOL(hAPP(sF221,bool,sF237,sF231))
    | c = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),b)
    | ~ hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,sF233,b)))
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13578,f2739]) ).

fof(f13583,plain,
    ( hBOOL(sF238)
    | c = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),b)
    | ~ hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,sF233,b)))
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13581,f2741]) ).

fof(f13584,plain,
    ( c = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),b)
    | ~ hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,sF233,b)))
    | spl239_1
    | ~ spl239_7 ),
    inference(forward_subsumption_resolution,[],[f13583,f2750]) ).

fof(f13585,plain,
    ( b = c
    | ~ hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,sF233,b)))
    | spl239_1
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13584,f2402]) ).

fof(f13586,plain,
    ( ~ hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,sF233,b)))
    | spl239_1
    | spl239_4
    | ~ spl239_7 ),
    inference(forward_subsumption_resolution,[],[f13585,f3043]) ).

fof(f13587,plain,
    ( ~ hBOOL(hAPP(sF221,bool,sF228,sF234))
    | spl239_1
    | spl239_4
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13586,f2733]) ).

fof(f13588,plain,
    ( ~ hBOOL(sF235)
    | spl239_1
    | spl239_4
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13587,f2735]) ).

fof(f13589,plain,
    ( $false
    | spl239_1
    | ~ spl239_2
    | spl239_4
    | ~ spl239_7 ),
    inference(forward_subsumption_resolution,[],[f13588,f2755]) ).

fof(f13590,plain,
    ( spl239_1
    | ~ spl239_2
    | spl239_4
    | ~ spl239_7 ),
    inference(avatar_contradiction_clause,[],[f13589]) ).

fof(f13862,plain,
    ( ! [X0] :
        ( ~ hBOOL(hAPP(sF221,bool,hAPP(sF220,sF222,sF223,sF236),sF231))
        | hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,sF232,X0),b)))
        | ~ sP0(b,c,sF231,a,X0)
        | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),b) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0) )
    | spl239_6
    | ~ spl239_7 ),
    inference(superposition,[],[f13483,f2737]) ).

fof(f13865,plain,
    ( ! [X0] :
        ( ~ hBOOL(hAPP(sF221,bool,sF237,sF231))
        | hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,sF232,X0),b)))
        | ~ sP0(b,c,sF231,a,X0)
        | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),b) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0) )
    | spl239_6
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13862,f2739]) ).

fof(f13869,plain,
    ( ! [X0] :
        ( ~ hBOOL(sF238)
        | hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,sF232,X0),b)))
        | ~ sP0(b,c,sF231,a,X0)
        | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),b) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0) )
    | spl239_6
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13865,f2741]) ).

fof(f13870,plain,
    ( ! [X0] :
        ( hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,sF232,X0),b)))
        | ~ sP0(b,c,sF231,a,X0)
        | hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),b) = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0) )
    | ~ spl239_1
    | spl239_6
    | ~ spl239_7 ),
    inference(forward_subsumption_resolution,[],[f13869,f2751]) ).

fof(f13871,plain,
    ( ! [X0] :
        ( hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,hAPP(arrow_490897120le_alt,sF229,sF232,X0),b)))
        | b = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),X0)
        | ~ sP0(b,c,sF231,a,X0) )
    | ~ spl239_1
    | spl239_6
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13870,f2402]) ).

fof(f13874,plain,
    ( hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,sF233,b)))
    | b = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),c)
    | ~ sP0(b,c,sF231,a,c)
    | ~ spl239_1
    | spl239_6
    | ~ spl239_7 ),
    inference(superposition,[],[f13871,f2731]) ).

fof(f13877,plain,
    ( hBOOL(hAPP(sF221,bool,sF228,hAPP(arrow_490897120le_alt,sF221,sF233,b)))
    | b = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),c)
    | ~ spl239_1
    | spl239_6
    | ~ spl239_7 ),
    inference(forward_subsumption_resolution,[],[f13874,f2888]) ).

fof(f13878,plain,
    ( hBOOL(hAPP(sF221,bool,sF228,sF234))
    | b = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),c)
    | ~ spl239_1
    | spl239_6
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13877,f2733]) ).

fof(f13879,plain,
    ( hBOOL(sF235)
    | b = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),c)
    | ~ spl239_1
    | spl239_6
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13878,f2735]) ).

fof(f13880,plain,
    ( b = hAPP(arrow_490897120le_alt,arrow_490897120le_alt,combi(arrow_490897120le_alt),c)
    | ~ spl239_1
    | spl239_2
    | spl239_6
    | ~ spl239_7 ),
    inference(forward_subsumption_resolution,[],[f13879,f2754]) ).

fof(f13881,plain,
    ( b = c
    | ~ spl239_1
    | spl239_2
    | spl239_6
    | ~ spl239_7 ),
    inference(forward_demodulation,[],[f13880,f2403]) ).

fof(f13882,plain,
    ( $false
    | ~ spl239_1
    | spl239_2
    | spl239_4
    | spl239_6
    | ~ spl239_7 ),
    inference(forward_subsumption_resolution,[],[f13881,f3043]) ).

fof(f13883,plain,
    ( ~ spl239_1
    | spl239_2
    | spl239_4
    | spl239_6
    | ~ spl239_7 ),
    inference(avatar_contradiction_clause,[],[f13882]) ).

fof(f13956,plain,
    ( ~ hBOOL(hAPP(arrow_490897120le_alt,bool,hAPP(list(arrow_490897120le_alt),fun(arrow_490897120le_alt,bool),set(arrow_490897120le_alt),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),a),nil(arrow_490897120le_alt))),a))
    | ~ spl239_6 ),
    inference(superposition,[],[f10493,f3116]) ).

fof(f13974,plain,
    ( $false
    | ~ spl239_6 ),
    inference(forward_subsumption_resolution,[],[f13956,f4458]) ).

fof(f13975,plain,
    ~ spl239_6,
    inference(avatar_contradiction_clause,[],[f13974]) ).

fof(f14121,plain,
    ( hBOOL(hAPP(list(arrow_490897120le_alt),bool,distinct(arrow_490897120le_alt),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),b),hAPP(list(arrow_490897120le_alt),list(arrow_490897120le_alt),hAPP(arrow_490897120le_alt,fun(list(arrow_490897120le_alt),list(arrow_490897120le_alt)),cons(arrow_490897120le_alt),b),nil(arrow_490897120le_alt)))))
    | ~ spl239_4 ),
    inference(superposition,[],[f3022,f3042]) ).

fof(f14143,plain,
    ( $false
    | ~ spl239_4 ),
    inference(forward_subsumption_resolution,[],[f14121,f4457]) ).

fof(f14144,plain,
    ~ spl239_4,
    inference(avatar_contradiction_clause,[],[f14143]) ).

cnf(s1,plain,
    ( spl239_1
    | spl239_2 ),
    inference(sat_conversion,[],[f2756]) ).

cnf(s2,plain,
    ( ~ spl239_1
    | ~ spl239_2 ),
    inference(sat_conversion,[],[f2757]) ).

cnf(s47,plain,
    spl239_7,
    inference(sat_conversion,[],[f13469]) ).

cnf(s48,plain,
    ( spl239_1
    | ~ spl239_2
    | spl239_4
    | ~ spl239_7 ),
    inference(sat_conversion,[],[f13590]) ).

cnf(s51,plain,
    ( ~ spl239_1
    | spl239_2
    | spl239_4
    | spl239_6
    | ~ spl239_7 ),
    inference(sat_conversion,[],[f13883]) ).

cnf(s53,plain,
    ~ spl239_6,
    inference(sat_conversion,[],[f13975]) ).

cnf(s57,plain,
    ~ spl239_4,
    inference(sat_conversion,[],[f14144]) ).

cnf(s58,plain,
    ( ~ spl239_1
    | spl239_2
    | ~ spl239_7 ),
    inference(rat,[],[s51,s53,s57]) ).

cnf(s60,plain,
    ( spl239_1
    | ~ spl239_2
    | ~ spl239_7 ),
    inference(rat,[],[s48,s57]) ).

cnf(s62,plain,
    spl239_1,
    inference(rat,[],[s1,s60,s47]) ).

cnf(s63,plain,
    spl239_2,
    inference(rat,[],[s58,s47,s62]) ).

cnf(s64,plain,
    $false,
    inference(rat,[],[s2,s63,s62]) ).

fof(f14150,plain,
    $false,
    inference(avatar_sat_refutation,[],[s64]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SCT170+6 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.40  % Computer : n020.cluster.edu
% 0.13/0.40  % Model    : x86_64 x86_64
% 0.13/0.40  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40  % Memory   : 8046.5625MB
% 0.13/0.40  % OS       : Linux 6.8.0-71-generic
% 0.13/0.40  % CPULimit : 300
% 0.13/0.40  % WCLimit  : 300
% 0.13/0.40  % DateTime : Sun Sep 27 23:57:24 UTC 2026
% 0.13/0.40  % CPUTime  : 
% 0.13/0.40  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.45  Running first-order theorem proving
% 0.13/0.45  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.32/4.15  % (3892854)Detected formulas, will run a generic FOF schedule.
% 22.32/4.15  % (3892861)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1779597453:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 22.32/4.15  % (3892865)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1040931137:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 22.32/4.15  % (3892862)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1245406384:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 22.32/4.15  % (3892867)dis-21_1_sil=8000:lcm=predicate:random_seed=3117458257:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 22.32/4.15  % (3892864)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=200355824:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 22.32/4.15  % (3892866)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3546845850:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 22.32/4.15  % (3892863)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=4126850323:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 22.32/4.15  % (3892865)Instruction limit reached! 
% 22.32/4.15  % (3892865)------------------------------
% 22.32/4.15  % (3892865)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.32/4.15  % (3892865)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.32/4.15  % (3892865)CaDiCaL version: 2.1.3
% 22.32/4.15  % (3892865)Termination reason: Instruction limit
% 22.32/4.15  % (3892865)Termination phase: Saturation
% 22.32/4.15  % (3892865)Time elapsed: 0.113 s
% 22.32/4.15  % (3892865)Peak memory usage: 89 MB
% 22.32/4.15  % (3892865)Instructions burned: 119 (million)
% 22.32/4.15  % (3892867)Instruction limit reached! 
% 22.32/4.15  % (3892867)------------------------------
% 22.32/4.15  % (3892867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.32/4.15  % (3892867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.32/4.15  % (3892867)CaDiCaL version: 2.1.3
% 22.32/4.15  % (3892867)Termination reason: Instruction limit
% 22.32/4.15  % (3892867)Termination phase: Property scanning
% 22.32/4.15  % (3892867)Time elapsed: 0.097 s
% 22.32/4.15  % (3892867)Peak memory usage: 87 MB
% 22.32/4.15  % (3892867)Instructions burned: 130 (million)
% 22.32/4.15  % (3892864)Instruction limit reached! 
% 22.32/4.15  % (3892864)------------------------------
% 22.32/4.15  % (3892864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.32/4.15  % (3892864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.32/4.15  % (3892864)CaDiCaL version: 2.1.3
% 22.32/4.15  % (3892864)Termination reason: Instruction limit
% 22.32/4.15  % (3892864)Termination phase: Saturation
% 22.32/4.15  % (3892864)Time elapsed: 0.100 s
% 22.32/4.15  % (3892864)Peak memory usage: 89 MB
% 22.32/4.15  % (3892864)Instructions burned: 110 (million)
% 22.32/4.15  % (3892866)Instruction limit reached! 
% 22.32/4.15  % (3892866)------------------------------
% 22.32/4.15  % (3892866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.32/4.15  % (3892866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.32/4.15  % (3892866)CaDiCaL version: 2.1.3
% 22.32/4.15  % (3892866)Termination reason: Instruction limit
% 22.32/4.15  % (3892866)Termination phase: Property scanning
% 22.32/4.15  % (3892866)Time elapsed: 0.106 s
% 22.32/4.15  % (3892866)Peak memory usage: 87 MB
% 22.32/4.15  % (3892866)Instructions burned: 139 (million)
% 22.32/4.15  % (3892878)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3382385037:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 22.32/4.15  % (3892875)lrs+10_1_sil=8000:sp=occurrence:random_seed=3327061366:i=285:sd=3:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/285Mi)
% 22.32/4.15  % (3892877)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2370189958:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 22.32/4.15  % (3892876)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2991299638:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 22.32/4.15  % (3892878)Instruction limit reached! 
% 31.82/5.64  % (3892878)------------------------------
% 31.82/5.64  % (3892878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.82/5.64  % (3892878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.82/5.64  % (3892878)CaDiCaL version: 2.1.3
% 31.82/5.64  % (3892878)Termination reason: Instruction limit
% 31.82/5.64  % (3892878)Termination phase: Saturation
% 31.82/5.64  % (3892878)Time elapsed: 0.148 s
% 31.82/5.64  % (3892878)Peak memory usage: 91 MB
% 31.82/5.64  % (3892878)Instructions burned: 249 (million)
% 31.82/5.64  % (3892876)Instruction limit reached! 
% 31.82/5.64  % (3892876)------------------------------
% 31.82/5.64  % (3892876)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.82/5.64  % (3892876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.82/5.64  % (3892876)CaDiCaL version: 2.1.3
% 31.82/5.64  % (3892876)Termination reason: Instruction limit
% 31.82/5.64  % (3892876)Termination phase: Saturation
% 31.82/5.64  % (3892876)Time elapsed: 0.139 s
% 31.82/5.64  % (3892876)Peak memory usage: 90 MB
% 31.82/5.64  % (3892876)Instructions burned: 158 (million)
% 31.82/5.64  % (3892875)Instruction limit reached! 
% 31.82/5.64  % (3892875)------------------------------
% 31.82/5.64  % (3892875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.82/5.64  % (3892875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.82/5.64  % (3892875)CaDiCaL version: 2.1.3
% 31.82/5.64  % (3892875)Termination reason: Instruction limit
% 31.82/5.64  % (3892875)Termination phase: Saturation
% 31.82/5.64  % (3892875)Time elapsed: 0.282 s
% 31.82/5.64  % (3892875)Peak memory usage: 91 MB
% 31.82/5.64  % (3892875)Instructions burned: 286 (million)
% 31.82/5.64  % (3892877)Instruction limit reached! 
% 31.82/5.64  % (3892877)------------------------------
% 31.82/5.64  % (3892877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.82/5.64  % (3892877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.82/5.64  % (3892877)CaDiCaL version: 2.1.3
% 31.82/5.64  % (3892877)Termination reason: Instruction limit
% 31.82/5.64  % (3892877)Termination phase: Saturation
% 31.82/5.64  % (3892877)Time elapsed: 0.273 s
% 31.82/5.64  % (3892877)Peak memory usage: 91 MB
% 31.82/5.64  % (3892877)Instructions burned: 326 (million)
% 31.82/5.64  % (3892883)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=566194970:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2991 on theBenchmark for (2991ds/294Mi)
% 31.82/5.64  % (3892884)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2054040701:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 31.82/5.64  % (3892886)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1714822358:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 31.82/5.64  % (3892885)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1096872784:cts=off:i=113:fsr=off:ss=included:sgt=4_2990 on theBenchmark for (2990ds/113Mi)
% 31.82/5.64  % (3892886)Instruction limit reached! 
% 31.82/5.64  % (3892886)------------------------------
% 31.82/5.64  % (3892886)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.82/5.64  % (3892886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.82/5.64  % (3892886)CaDiCaL version: 2.1.3
% 31.82/5.64  % (3892886)Termination reason: Instruction limit
% 31.82/5.64  % (3892886)Termination phase: Property scanning
% 31.82/5.64  % (3892886)Time elapsed: 0.049 s
% 31.82/5.64  % (3892886)Peak memory usage: 87 MB
% 31.82/5.64  % (3892886)Instructions burned: 130 (million)
% 31.82/5.64  % (3892883)Instruction limit reached! 
% 31.82/5.64  % (3892883)------------------------------
% 31.82/5.64  % (3892883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.82/5.64  % (3892883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.82/5.64  % (3892883)CaDiCaL version: 2.1.3
% 31.82/5.64  % (3892883)Termination reason: Instruction limit
% 31.82/5.64  % (3892883)Termination phase: Saturation
% 31.82/5.64  % (3892883)Time elapsed: 0.219 s
% 31.82/5.64  % (3892883)Peak memory usage: 91 MB
% 31.82/5.64  % (3892883)Instructions burned: 295 (million)
% 31.82/5.64  % (3892885)Instruction limit reached! 
% 31.82/5.64  % (3892885)------------------------------
% 31.82/5.64  % (3892885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.82/5.64  % (3892885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.82/5.64  % (3892885)CaDiCaL version: 2.1.3
% 31.82/5.64  % (3892885)Termination reason: Instruction limit
% 33.55/6.57  % (3892885)Termination phase: Property scanning
% 33.55/6.57  % (3892885)Time elapsed: 0.086 s
% 33.55/6.57  % (3892885)Peak memory usage: 87 MB
% 33.55/6.57  % (3892885)Instructions burned: 113 (million)
% 33.55/6.57  % (3892892)lrs+10_1_sil=8000:sp=occurrence:random_seed=3947507263:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2987 on theBenchmark for (2987ds/907Mi)
% 33.55/6.57  % (3892891)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=497207016:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2987 on theBenchmark for (2987ds/114Mi)
% 33.55/6.57  % (3892891)Instruction limit reached! 
% 33.55/6.57  % (3892891)------------------------------
% 33.55/6.57  % (3892891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.55/6.57  % (3892891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.55/6.57  % (3892891)CaDiCaL version: 2.1.3
% 33.55/6.57  % (3892891)Termination reason: Instruction limit
% 33.55/6.57  % (3892891)Termination phase: Saturation
% 33.55/6.57  % (3892891)Time elapsed: 0.089 s
% 33.55/6.57  % (3892891)Peak memory usage: 89 MB
% 33.55/6.57  % (3892891)Instructions burned: 114 (million)
% 33.55/6.57  % (3892893)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1737878322:i=437:sd=1:aac=none:ss=included_2986 on theBenchmark for (2986ds/437Mi)
% 33.55/6.57  % (3892896)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1403846850:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 33.55/6.57  % (3892893)Instruction limit reached! 
% 33.55/6.57  % (3892893)------------------------------
% 33.55/6.57  % (3892893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.55/6.57  % (3892893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.55/6.57  % (3892893)CaDiCaL version: 2.1.3
% 33.55/6.57  % (3892893)Termination reason: Instruction limit
% 33.55/6.57  % (3892893)Termination phase: Saturation
% 33.55/6.57  % (3892893)Time elapsed: 0.365 s
% 33.55/6.57  % (3892893)Peak memory usage: 93 MB
% 33.55/6.57  % (3892893)Instructions burned: 437 (million)
% 33.55/6.57  % (3892901)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3131394679:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 33.55/6.57  % (3892892)Instruction limit reached! 
% 33.55/6.57  % (3892892)------------------------------
% 33.55/6.57  % (3892892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.55/6.57  % (3892892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.55/6.57  % (3892892)CaDiCaL version: 2.1.3
% 33.55/6.57  % (3892892)Termination reason: Instruction limit
% 33.55/6.57  % (3892892)Termination phase: Saturation
% 33.55/6.57  % (3892892)Time elapsed: 0.787 s
% 33.55/6.57  % (3892892)Peak memory usage: 96 MB
% 33.55/6.57  % (3892892)Instructions burned: 908 (million)
% 33.55/6.57  % (3892901)Instruction limit reached! 
% 33.55/6.57  % (3892901)------------------------------
% 33.55/6.57  % (3892901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.55/6.57  % (3892901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.55/6.57  % (3892901)CaDiCaL version: 2.1.3
% 33.55/6.57  % (3892901)Termination reason: Instruction limit
% 33.55/6.57  % (3892901)Termination phase: Property scanning
% 33.55/6.57  % (3892901)Time elapsed: 0.054 s
% 33.55/6.57  % (3892901)Peak memory usage: 87 MB
% 33.55/6.57  % (3892901)Instructions burned: 134 (million)
% 33.55/6.57  % (3892903)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1932192200:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 33.55/6.57  % (3892904)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1714039478:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 33.55/6.57  % (3892903)Instruction limit reached! 
% 33.55/6.57  % (3892903)------------------------------
% 33.55/6.57  % (3892903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.55/6.57  % (3892903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.55/6.57  % (3892903)CaDiCaL version: 2.1.3
% 33.55/6.57  % (3892903)Termination reason: Instruction limit
% 33.55/6.57  % (3892903)Termination phase: Saturation
% 33.55/6.57  % (3892903)Time elapsed: 0.489 s
% 33.55/6.57  % (3892903)Peak memory usage: 95 MB
% 33.55/6.57  % (3892903)Instructions burned: 592 (million)
% 33.55/6.57  % (3892909)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=214618067:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2970 on theBenchmark for (2970ds/125Mi)
% 33.55/6.57  % (3892909)Instruction limit reached! 
% 33.55/6.57  % (3892909)------------------------------
% 33.55/6.57  % (3892909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.55/6.57  % (3892909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.55/6.57  % (3892909)CaDiCaL version: 2.1.3
% 33.55/6.57  % (3892909)Termination reason: Instruction limit
% 33.55/6.57  % (3892909)Termination phase: Saturation
% 33.55/6.57  % (3892909)Time elapsed: 0.102 s
% 33.55/6.57  % (3892909)Peak memory usage: 89 MB
% 33.55/6.57  % (3892909)Instructions burned: 125 (million)
% 33.55/6.57  % (3892884)Instruction limit reached! 
% 33.55/6.57  % (3892884)------------------------------
% 33.55/6.57  % (3892884)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.55/6.57  % (3892884)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.55/6.57  % (3892884)CaDiCaL version: 2.1.3
% 33.55/6.57  % (3892884)Termination reason: Instruction limit
% 33.55/6.57  % (3892884)Termination phase: Saturation
% 33.55/6.57  % (3892884)Time elapsed: 2.359 s
% 33.55/6.57  % (3892884)Peak memory usage: 154 MB
% 33.55/6.57  % (3892884)Instructions burned: 2350 (million)
% 33.55/6.57  % (3892913)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3013557248:i=134:gtgl=5:slsql=off:gtg=exists_sym_2966 on theBenchmark for (2966ds/134Mi)
% 33.55/6.57  % (3892914)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1132432313:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/141Mi)
% 33.55/6.57  % (3892913)Instruction limit reached! 
% 33.55/6.57  % (3892913)------------------------------
% 33.55/6.57  % (3892913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.55/6.57  % (3892913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.55/6.57  % (3892913)CaDiCaL version: 2.1.3
% 33.55/6.57  % (3892913)Termination reason: Instruction limit
% 33.55/6.57  % (3892913)Termination phase: Property scanning
% 33.55/6.57  % (3892913)Time elapsed: 0.103 s
% 33.55/6.57  % (3892913)Peak memory usage: 87 MB
% 33.55/6.57  % (3892913)Instructions burned: 134 (million)
% 33.55/6.57  % (3892914)Refutation not found, incomplete strategy
% 33.55/6.57  % (3892914)------------------------------
% 33.55/6.57  % (3892914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.55/6.57  % (3892914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.55/6.57  % (3892914)CaDiCaL version: 2.1.3
% 33.55/6.57  % (3892914)Termination reason: Refutation not found, incomplete strategy
% 33.55/6.57  % (3892914)Time elapsed: 0.018 s
% 33.55/6.57  % (3892914)Peak memory usage: 89 MB
% 33.55/6.57  % (3892914)Instructions burned: 19 (million)
% 33.55/6.57  % (3892917)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=238911772:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2962 on theBenchmark for (2962ds/431Mi)
% 33.55/6.57  % (3892914)------------------------------
% 33.55/6.57  % (3892914)------------------------------
% 33.55/6.57  % (3892919)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1156507159:i=6060:aac=none:ins=25_2958 on theBenchmark for (2958ds/6060Mi)
% 33.55/6.57  % (3892917)Instruction limit reached! 
% 33.55/6.57  % (3892917)------------------------------
% 33.55/6.57  % (3892917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.55/6.57  % (3892917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.55/6.57  % (3892917)CaDiCaL version: 2.1.3
% 33.55/6.57  % (3892917)Termination reason: Instruction limit
% 33.55/6.57  % (3892917)Termination phase: Saturation
% 33.55/6.57  % (3892917)Time elapsed: 0.369 s
% 33.55/6.57  % (3892917)Peak memory usage: 91 MB
% 33.55/6.57  % (3892917)Instructions burned: 432 (million)
% 33.55/6.57  % (3892921)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=551468689:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2956 on theBenchmark for (2956ds/150Mi)
% 33.55/6.57  % (3892921)Instruction limit reached! 
% 33.55/6.57  % (3892921)------------------------------
% 33.55/6.57  % (3892921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.55/6.57  % (3892921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.55/6.57  % (3892921)CaDiCaL version: 2.1.3
% 33.55/6.57  % (3892921)Termination reason: Instruction limit
% 33.55/6.57  % (3892921)Termination phase: Property scanning
% 33.55/6.57  % (3892921)Time elapsed: 0.113 s
% 33.55/6.57  % (3892921)Peak memory usage: 88 MB
% 33.55/6.57  % (3892921)Instructions burned: 150 (million)
% 33.55/6.57  % (3892925)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2944053685:i=14155:bd=all_2952 on theBenchmark for (2952ds/14155Mi)
% 33.55/6.57  % (3892861)First to succeed.
% 33.55/6.57  % (3892861)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3892854"
% 33.55/6.57  % (3892861)Refutation found. Thanks to Tanya!
% 33.55/6.57  % SZS status Theorem for theBenchmark
% 33.55/6.57  % SZS output start Proof for theBenchmark
% See solution above
% 39.52/6.77  % (3892861)------------------------------
% 39.52/6.77  % (3892861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.52/6.77  % (3892861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.52/6.77  % (3892861)CaDiCaL version: 2.1.3
% 39.52/6.77  % (3892861)Termination reason: Refutation
% 39.52/6.77  % (3892861)Time elapsed: 4.877 s
% 39.52/6.77  % (3892861)Peak memory usage: 168 MB
% 39.52/6.77  % (3892861)Instructions burned: 6138 (million)
% 39.52/6.77  % (3892861)------------------------------
% 39.52/6.77  % (3892861)------------------------------
% 39.52/6.77  % (3892854)Success in time 5.646 s
% 39.52/6.77  % Vampire exiting
%------------------------------------------------------------------------------