Vampire-SAT---5.0.1.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : LCL803_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT

% Computer : n003.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:00:39 PM UTC 2026

% Result   : Theorem 21.21s 3.51s
% Output   : Refutation 21.21s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    8
%            Number of leaves      :    6
% Syntax   : Number of formulae    :   25 (  14 unt;   0 typ;   2 def)
%            Number of atoms       :   46 (   0 equ)
%            Maximal formula atoms :    6 (   1 avg)
%            Number of connectives :   39 (  18   ~;  13   |;   5   &)
%                                         (   3 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    9 (   3 avg)
%            Maximal term depth    :   28 (   2 avg)
%            Number of types       :    5 (   4 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :    9 (   8 usr;   3 prp; 0-4 aty)
%            Number of functors    :   79 (  79 usr;  28 con; 0-5 aty)
%            Number of variables   :   16 (   0 sgn  16   !;   0   ?;  16   :)

% Comments : 
%------------------------------------------------------------------------------
tff(type_def_5,type,
    bool: $tType ).

tff(type_def_6,type,
    dB: $tType ).

tff(type_def_7,type,
    list: $tType > $tType ).

tff(type_def_8,type,
    nat: $tType ).

tff(type_def_9,type,
    type: $tType ).

tff(type_def_10,type,
    fun: ( $tType * $tType ) > $tType ).

tff(func_def_0,type,
    combb: 
      !>[X0: $tType,X1: $tType,X2: $tType] : fun(fun(X0,X1),fun(fun(X2,X0),fun(X2,X1))) ).

tff(func_def_1,type,
    combc: 
      !>[X0: $tType,X1: $tType,X2: $tType] : fun(fun(X0,fun(X1,X2)),fun(X1,fun(X0,X2))) ).

tff(func_def_2,type,
    combs: 
      !>[X0: $tType,X1: $tType,X2: $tType] : fun(fun(X0,fun(X1,X2)),fun(fun(X0,X1),fun(X0,X2))) ).

tff(func_def_3,type,
    zero_zero: 
      !>[X0: $tType] : X0 ).

tff(func_def_4,type,
    it: fun(dB,bool) ).

tff(func_def_5,type,
    beta: fun(dB,fun(dB,bool)) ).

tff(func_def_6,type,
    abs: dB > dB ).

tff(func_def_7,type,
    app: fun(dB,fun(dB,dB)) ).

tff(func_def_8,type,
    var: nat > dB ).

tff(func_def_9,type,
    dB_size: dB > nat ).

tff(func_def_10,type,
    lift: ( dB * nat ) > dB ).

tff(func_def_11,type,
    subst: fun(dB,fun(dB,fun(nat,dB))) ).

tff(func_def_12,type,
    foldl: 
      !>[X0: $tType,X1: $tType] : ( ( fun(X0,fun(X1,X0)) * X0 * list(X1) ) > X0 ) ).

tff(func_def_13,type,
    foldr: 
      !>[X0: $tType,X1: $tType] : ( ( fun(X0,fun(X1,X1)) * list(X0) * X1 ) > X1 ) ).

tff(func_def_14,type,
    cons: 
      !>[X0: $tType] : fun(X0,fun(list(X0),list(X0))) ).

tff(func_def_15,type,
    list_case: 
      !>[X0: $tType,X1: $tType] : ( ( X0 * fun(X1,fun(list(X1),X0)) * list(X1) ) > X0 ) ).

tff(func_def_16,type,
    listset: 
      !>[X0: $tType] : ( list(fun(X0,bool)) > fun(list(X0),bool) ) ).

tff(func_def_17,type,
    set_Cons: 
      !>[X0: $tType] : ( ( fun(X0,bool) * fun(list(X0),bool) ) > fun(list(X0),bool) ) ).

tff(func_def_18,type,
    size_size: 
      !>[X0: $tType] : ( X0 > nat ) ).

tff(func_def_19,type,
    collect: 
      !>[X0: $tType] : ( fun(X0,bool) > fun(X0,bool) ) ).

tff(func_def_20,type,
    shift: 
      !>[X0: $tType] : fun(fun(nat,X0),fun(nat,fun(X0,fun(nat,X0)))) ).

tff(func_def_21,type,
    fun1: fun(type,fun(type,type)) ).

tff(func_def_22,type,
    type_case: 
      !>[X0: $tType] : ( ( fun(nat,X0) * fun(type,fun(type,X0)) * type ) > X0 ) ).

tff(func_def_23,type,
    typing: fun(fun(nat,type),fun(dB,fun(type,bool))) ).

tff(func_def_24,type,
    typings: ( fun(nat,type) * list(dB) ) > fun(list(type),bool) ).

tff(func_def_25,type,
    aa: 
      !>[X0: $tType,X1: $tType] : ( ( fun(X0,X1) * X0 ) > X1 ) ).

tff(func_def_26,type,
    fAll: 
      !>[X0: $tType] : fun(fun(X0,bool),bool) ).

tff(func_def_27,type,
    fEx: 
      !>[X0: $tType] : fun(fun(X0,bool),bool) ).

tff(func_def_28,type,
    fFalse: bool ).

tff(func_def_29,type,
    fTrue: bool ).

tff(func_def_30,type,
    fconj: fun(bool,fun(bool,bool)) ).

tff(func_def_31,type,
    fequal: 
      !>[X0: $tType] : fun(X0,fun(X0,bool)) ).

tff(func_def_32,type,
    fimplies: fun(bool,fun(bool,bool)) ).

tff(func_def_33,type,
    member: 
      !>[X0: $tType] : fun(X0,fun(fun(X0,bool),bool)) ).

tff(func_def_34,type,
    t2: type ).

tff(func_def_35,type,
    t1: type ).

tff(func_def_36,type,
    t_a: type ).

tff(func_def_37,type,
    t: type ).

tff(func_def_38,type,
    ts: list(type) ).

tff(func_def_39,type,
    a: dB ).

tff(func_def_40,type,
    as: list(dB) ).

tff(func_def_41,type,
    e: fun(nat,type) ).

tff(func_def_42,type,
    ea: fun(nat,type) ).

tff(func_def_43,type,
    i: nat ).

tff(func_def_44,type,
    ia: nat ).

tff(func_def_45,type,
    n: nat ).

tff(func_def_46,type,
    rs: list(dB) ).

tff(func_def_47,type,
    t3: dB ).

tff(func_def_48,type,
    u: dB ).

tff(func_def_49,type,
    ua: dB ).

tff(func_def_50,type,
    sK2: ( type * dB * dB * fun(nat,type) ) > type ).

tff(func_def_51,type,
    sK3: type ).

tff(func_def_52,type,
    sK4: list(type) ).

tff(func_def_53,type,
    sK5: ( type * type * list(dB) * fun(nat,type) ) > list(type) ).

tff(func_def_54,type,
    sK6: ( type * list(dB) * nat * fun(nat,type) ) > list(type) ).

tff(func_def_55,type,
    sK7: ( type * list(dB) * dB * fun(nat,type) ) > list(type) ).

tff(func_def_56,type,
    sK8: ( type * list(dB) * dB * fun(nat,type) ) > list(type) ).

tff(func_def_57,type,
    sK9: 
      !>[X0: $tType,X1: $tType] : ( ( fun(X1,X0) * fun(X1,X0) ) > X1 ) ).

tff(func_def_58,type,
    sK10: ( type * dB * fun(nat,type) ) > type ).

tff(func_def_59,type,
    sK11: ( type * dB * fun(nat,type) ) > type ).

tff(func_def_60,type,
    sK12: ( dB * fun(nat,type) ) > type ).

tff(func_def_61,type,
    sK13: ( dB * fun(nat,type) ) > type ).

tff(func_def_62,type,
    sK14: dB > dB ).

tff(func_def_63,type,
    sK15: dB > dB ).

tff(func_def_64,type,
    sK16: dB > list(dB) ).

tff(func_def_65,type,
    sK17: dB > list(dB) ).

tff(func_def_66,type,
    sK18: dB > nat ).

tff(func_def_67,type,
    sK19: dB > dB ).

tff(func_def_68,type,
    sK20: ( dB * dB ) > dB ).

tff(func_def_69,type,
    sK21: ( dB * dB * dB ) > dB ).

tff(func_def_70,type,
    sK22: ( dB * dB * dB ) > dB ).

tff(func_def_71,type,
    sK23: ( dB * dB * dB ) > dB ).

tff(func_def_72,type,
    sK24: ( dB * list(dB) * dB ) > dB ).

tff(func_def_73,type,
    sK25: ( dB * list(dB) * dB ) > dB ).

tff(func_def_74,type,
    sK26: ( dB * list(dB) * dB ) > list(dB) ).

tff(func_def_75,type,
    sK27: ( dB * list(dB) * dB ) > list(dB) ).

tff(func_def_76,type,
    sK28: ( dB * list(dB) * dB ) > dB ).

tff(pred_def_1,type,
    zero: 
      !>[X0: $tType] : $o ).

tff(pred_def_2,type,
    step1: 
      !>[X0: $tType] : ( ( fun(X0,fun(X0,bool)) * list(X0) * list(X0) ) > $o ) ).

tff(pred_def_3,type,
    listsp: 
      !>[X0: $tType] : ( ( fun(X0,bool) * list(X0) ) > $o ) ).

tff(pred_def_4,type,
    pp: bool > $o ).

tff(pred_def_5,type,
    sP0: dB > $o ).

tff(pred_def_6,type,
    sP1: ( dB * list(dB) * dB ) > $o ).

tff(f5,axiom,
    listsp(dB,aa(fun(dB,fun(type,bool)),fun(dB,bool),aa(fun(fun(type,bool),bool),fun(fun(dB,fun(type,bool)),fun(dB,bool)),combb(fun(type,bool),bool,dB),fEx(type)),aa(fun(nat,type),fun(dB,fun(type,bool)),typing,aa(type,fun(nat,type),aa(nat,fun(type,fun(nat,type)),aa(fun(nat,type),fun(nat,fun(type,fun(nat,type))),shift(type),e),i),t))),as),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4__096listsp_A_I_Ft_O_AEX_AT_H_O_Ae_060i_058T_062_A_092_060turnstile_062_At_A_058_AT_H_J_Aas_096) ).

tff(f7,axiom,
    listsp(dB,aa(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool),aa(fun(fun(fun(nat,type),bool),bool),fun(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool)),combb(fun(fun(nat,type),bool),bool,dB),fAll(fun(nat,type))),aa(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool)),aa(fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),fun(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool))),combb(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool),dB),aa(fun(fun(type,bool),bool),fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),combb(fun(type,bool),bool,fun(nat,type)),fAll(type))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool)))),combb(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool)),dB),aa(fun(fun(type,fun(dB,bool)),fun(type,bool)),fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),combb(fun(type,fun(dB,bool)),fun(type,bool),fun(nat,type)),aa(fun(fun(dB,bool),bool),fun(fun(type,fun(dB,bool)),fun(type,bool)),combb(fun(dB,bool),bool,type),fAll(dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool))))),combb(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool))),dB),aa(fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool)),fun(nat,type)),aa(fun(fun(dB,fun(nat,bool)),fun(dB,bool)),fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),combb(fun(dB,fun(nat,bool)),fun(dB,bool),type),aa(fun(fun(nat,bool),bool),fun(fun(dB,fun(nat,bool)),fun(dB,bool)),combb(fun(nat,bool),bool,dB),fAll(nat))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),combs(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),dB),combs(fun(nat,type),fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))),fun(nat,type)),combc(type,fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(nat,type)),aa(fun(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),type),combb(fun(nat,bool),fun(nat,bool),dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),dB),aa(fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool))),fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool)),type),combs(nat,bool,bool)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),dB),aa(fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),combb(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool))),fun(nat,type)),aa(fun(fun(nat,bool),fun(nat,fun(bool,bool))),fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),combb(fun(nat,bool),fun(nat,fun(bool,bool)),type),aa(fun(bool,fun(bool,bool)),fun(fun(nat,bool),fun(nat,fun(bool,bool))),combb(bool,fun(bool,bool),nat),fimplies)))),aa(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool))))),combb(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool))),dB),aa(fun(fun(nat,fun(type,bool)),fun(type,fun(nat,bool))),fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),combb(fun(nat,fun(type,bool)),fun(type,fun(nat,bool)),fun(nat,type)),combc(nat,type,bool))),aa(fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),combc(fun(nat,type),dB,fun(nat,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),aa(fun(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool))))),combb(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool))),fun(nat,type)),combc(nat,dB,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),aa(fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool))))),combb(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool))),fun(nat,type)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),combb(fun(nat,type),fun(dB,fun(type,bool)),nat),typing)),aa(type,fun(fun(nat,type),fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),fun(type,fun(fun(nat,type),fun(nat,fun(nat,type)))),combc(fun(nat,type),type,fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),aa(fun(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type)))),fun(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type))))),combb(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type))),fun(nat,type)),combc(nat,type,fun(nat,type))),shift(type))),t))))))))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)),fun(nat,type)),aa(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),combs(dB,fun(nat,bool),fun(nat,bool)),aa(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat)),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies),it))))),aa(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combc(fun(nat,type),fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(nat,type)),combs(dB,fun(nat,bool),fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),aa(fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat))),aa(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool))),aa(fun(fun(dB,bool),fun(dB,fun(bool,bool))),fun(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool)))),combb(fun(dB,bool),fun(dB,fun(bool,bool)),fun(nat,type)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies)),aa(type,fun(fun(nat,type),fun(dB,bool)),aa(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(type,fun(fun(nat,type),fun(dB,bool))),combc(fun(nat,type),type,fun(dB,bool)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool))),aa(fun(fun(dB,fun(type,bool)),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(dB,fun(type,bool)),fun(type,fun(dB,bool)),fun(nat,type)),combc(dB,type,bool)),typing)),t)))))),aa(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool))),aa(fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),fun(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool)),dB),aa(fun(fun(nat,dB),fun(nat,bool)),fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),combb(fun(nat,dB),fun(nat,bool),dB),aa(fun(dB,bool),fun(fun(nat,dB),fun(nat,bool)),combb(dB,bool,nat),it))),subst)))))))),as),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6__096listsp_A_I_Ft_O_AALL_Ae_AT_H_Au_Ai_O_Ae_060i_058T_062_A_092_060turnstile_062_At_A_058_AT_H_A_N_N_062_AIT_Au_A_N_N_062_Ae_A_092_060turnstile_062_Au_A_058_AT_A_N_N_062_AIT_A_It_091u_Pi_093_J_J_Aas_096) ).

tff(f14,axiom,
    ! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool),X3: list(X0)] :
      ( listsp(X0,aa(fun(X0,bool),fun(X0,bool),aa(fun(X0,fun(bool,bool)),fun(fun(X0,bool),fun(X0,bool)),combs(X0,bool,bool),aa(fun(X0,bool),fun(X0,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(X0,bool),fun(X0,fun(bool,bool))),combb(bool,fun(bool,bool),X0),fconj),X2)),X1),X3)
    <=> ( listsp(X0,X2,X3)
        & listsp(X0,X1,X3) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_listsp__conj__eq) ).

tff(f118,conjecture,
    listsp(dB,aa(fun(dB,bool),fun(dB,bool),aa(fun(dB,fun(bool,bool)),fun(fun(dB,bool),fun(dB,bool)),combs(dB,bool,bool),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fconj),aa(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool),aa(fun(fun(fun(nat,type),bool),bool),fun(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool)),combb(fun(fun(nat,type),bool),bool,dB),fAll(fun(nat,type))),aa(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool)),aa(fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),fun(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool))),combb(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool),dB),aa(fun(fun(type,bool),bool),fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),combb(fun(type,bool),bool,fun(nat,type)),fAll(type))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool)))),combb(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool)),dB),aa(fun(fun(type,fun(dB,bool)),fun(type,bool)),fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),combb(fun(type,fun(dB,bool)),fun(type,bool),fun(nat,type)),aa(fun(fun(dB,bool),bool),fun(fun(type,fun(dB,bool)),fun(type,bool)),combb(fun(dB,bool),bool,type),fAll(dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool))))),combb(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool))),dB),aa(fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool)),fun(nat,type)),aa(fun(fun(dB,fun(nat,bool)),fun(dB,bool)),fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),combb(fun(dB,fun(nat,bool)),fun(dB,bool),type),aa(fun(fun(nat,bool),bool),fun(fun(dB,fun(nat,bool)),fun(dB,bool)),combb(fun(nat,bool),bool,dB),fAll(nat))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),combs(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),dB),combs(fun(nat,type),fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))),fun(nat,type)),combc(type,fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(nat,type)),aa(fun(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),type),combb(fun(nat,bool),fun(nat,bool),dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),dB),aa(fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool))),fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool)),type),combs(nat,bool,bool)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),dB),aa(fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),combb(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool))),fun(nat,type)),aa(fun(fun(nat,bool),fun(nat,fun(bool,bool))),fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),combb(fun(nat,bool),fun(nat,fun(bool,bool)),type),aa(fun(bool,fun(bool,bool)),fun(fun(nat,bool),fun(nat,fun(bool,bool))),combb(bool,fun(bool,bool),nat),fimplies)))),aa(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool))))),combb(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool))),dB),aa(fun(fun(nat,fun(type,bool)),fun(type,fun(nat,bool))),fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),combb(fun(nat,fun(type,bool)),fun(type,fun(nat,bool)),fun(nat,type)),combc(nat,type,bool))),aa(fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),combc(fun(nat,type),dB,fun(nat,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),aa(fun(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool))))),combb(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool))),fun(nat,type)),combc(nat,dB,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),aa(fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool))))),combb(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool))),fun(nat,type)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),combb(fun(nat,type),fun(dB,fun(type,bool)),nat),typing)),aa(type,fun(fun(nat,type),fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),fun(type,fun(fun(nat,type),fun(nat,fun(nat,type)))),combc(fun(nat,type),type,fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),aa(fun(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type)))),fun(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type))))),combb(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type))),fun(nat,type)),combc(nat,type,fun(nat,type))),shift(type))),t))))))))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)),fun(nat,type)),aa(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),combs(dB,fun(nat,bool),fun(nat,bool)),aa(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat)),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies),it))))),aa(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combc(fun(nat,type),fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(nat,type)),combs(dB,fun(nat,bool),fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),aa(fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat))),aa(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool))),aa(fun(fun(dB,bool),fun(dB,fun(bool,bool))),fun(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool)))),combb(fun(dB,bool),fun(dB,fun(bool,bool)),fun(nat,type)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies)),aa(type,fun(fun(nat,type),fun(dB,bool)),aa(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(type,fun(fun(nat,type),fun(dB,bool))),combc(fun(nat,type),type,fun(dB,bool)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool))),aa(fun(fun(dB,fun(type,bool)),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(dB,fun(type,bool)),fun(type,fun(dB,bool)),fun(nat,type)),combc(dB,type,bool)),typing)),t)))))),aa(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool))),aa(fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),fun(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool)),dB),aa(fun(fun(nat,dB),fun(nat,bool)),fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),combb(fun(nat,dB),fun(nat,bool),dB),aa(fun(dB,bool),fun(fun(nat,dB),fun(nat,bool)),combb(dB,bool,nat),it))),subst)))))))))),aa(fun(dB,fun(type,bool)),fun(dB,bool),aa(fun(fun(type,bool),bool),fun(fun(dB,fun(type,bool)),fun(dB,bool)),combb(fun(type,bool),bool,dB),fEx(type)),aa(fun(nat,type),fun(dB,fun(type,bool)),typing,aa(type,fun(nat,type),aa(nat,fun(type,fun(nat,type)),aa(fun(nat,type),fun(nat,fun(type,fun(nat,type))),shift(type),e),i),t)))),as),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

tff(f119,negated_conjecture,
    ~ listsp(dB,aa(fun(dB,bool),fun(dB,bool),aa(fun(dB,fun(bool,bool)),fun(fun(dB,bool),fun(dB,bool)),combs(dB,bool,bool),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fconj),aa(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool),aa(fun(fun(fun(nat,type),bool),bool),fun(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool)),combb(fun(fun(nat,type),bool),bool,dB),fAll(fun(nat,type))),aa(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool)),aa(fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),fun(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool))),combb(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool),dB),aa(fun(fun(type,bool),bool),fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),combb(fun(type,bool),bool,fun(nat,type)),fAll(type))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool)))),combb(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool)),dB),aa(fun(fun(type,fun(dB,bool)),fun(type,bool)),fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),combb(fun(type,fun(dB,bool)),fun(type,bool),fun(nat,type)),aa(fun(fun(dB,bool),bool),fun(fun(type,fun(dB,bool)),fun(type,bool)),combb(fun(dB,bool),bool,type),fAll(dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool))))),combb(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool))),dB),aa(fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool)),fun(nat,type)),aa(fun(fun(dB,fun(nat,bool)),fun(dB,bool)),fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),combb(fun(dB,fun(nat,bool)),fun(dB,bool),type),aa(fun(fun(nat,bool),bool),fun(fun(dB,fun(nat,bool)),fun(dB,bool)),combb(fun(nat,bool),bool,dB),fAll(nat))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),combs(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),dB),combs(fun(nat,type),fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))),fun(nat,type)),combc(type,fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(nat,type)),aa(fun(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),type),combb(fun(nat,bool),fun(nat,bool),dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),dB),aa(fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool))),fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool)),type),combs(nat,bool,bool)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),dB),aa(fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),combb(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool))),fun(nat,type)),aa(fun(fun(nat,bool),fun(nat,fun(bool,bool))),fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),combb(fun(nat,bool),fun(nat,fun(bool,bool)),type),aa(fun(bool,fun(bool,bool)),fun(fun(nat,bool),fun(nat,fun(bool,bool))),combb(bool,fun(bool,bool),nat),fimplies)))),aa(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool))))),combb(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool))),dB),aa(fun(fun(nat,fun(type,bool)),fun(type,fun(nat,bool))),fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),combb(fun(nat,fun(type,bool)),fun(type,fun(nat,bool)),fun(nat,type)),combc(nat,type,bool))),aa(fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),combc(fun(nat,type),dB,fun(nat,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),aa(fun(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool))))),combb(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool))),fun(nat,type)),combc(nat,dB,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),aa(fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool))))),combb(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool))),fun(nat,type)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),combb(fun(nat,type),fun(dB,fun(type,bool)),nat),typing)),aa(type,fun(fun(nat,type),fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),fun(type,fun(fun(nat,type),fun(nat,fun(nat,type)))),combc(fun(nat,type),type,fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),aa(fun(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type)))),fun(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type))))),combb(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type))),fun(nat,type)),combc(nat,type,fun(nat,type))),shift(type))),t))))))))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)),fun(nat,type)),aa(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),combs(dB,fun(nat,bool),fun(nat,bool)),aa(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat)),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies),it))))),aa(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combc(fun(nat,type),fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(nat,type)),combs(dB,fun(nat,bool),fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),aa(fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat))),aa(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool))),aa(fun(fun(dB,bool),fun(dB,fun(bool,bool))),fun(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool)))),combb(fun(dB,bool),fun(dB,fun(bool,bool)),fun(nat,type)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies)),aa(type,fun(fun(nat,type),fun(dB,bool)),aa(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(type,fun(fun(nat,type),fun(dB,bool))),combc(fun(nat,type),type,fun(dB,bool)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool))),aa(fun(fun(dB,fun(type,bool)),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(dB,fun(type,bool)),fun(type,fun(dB,bool)),fun(nat,type)),combc(dB,type,bool)),typing)),t)))))),aa(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool))),aa(fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),fun(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool)),dB),aa(fun(fun(nat,dB),fun(nat,bool)),fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),combb(fun(nat,dB),fun(nat,bool),dB),aa(fun(dB,bool),fun(fun(nat,dB),fun(nat,bool)),combb(dB,bool,nat),it))),subst)))))))))),aa(fun(dB,fun(type,bool)),fun(dB,bool),aa(fun(fun(type,bool),bool),fun(fun(dB,fun(type,bool)),fun(dB,bool)),combb(fun(type,bool),bool,dB),fEx(type)),aa(fun(nat,type),fun(dB,fun(type,bool)),typing,aa(type,fun(nat,type),aa(nat,fun(type,fun(nat,type)),aa(fun(nat,type),fun(nat,fun(type,fun(nat,type))),shift(type),e),i),t)))),as),
    inference(negated_conjecture,[status(cth)],[f118]) ).

tff(f122,plain,
    ~ listsp(dB,aa(fun(dB,bool),fun(dB,bool),aa(fun(dB,fun(bool,bool)),fun(fun(dB,bool),fun(dB,bool)),combs(dB,bool,bool),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fconj),aa(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool),aa(fun(fun(fun(nat,type),bool),bool),fun(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool)),combb(fun(fun(nat,type),bool),bool,dB),fAll(fun(nat,type))),aa(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool)),aa(fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),fun(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool))),combb(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool),dB),aa(fun(fun(type,bool),bool),fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),combb(fun(type,bool),bool,fun(nat,type)),fAll(type))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool)))),combb(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool)),dB),aa(fun(fun(type,fun(dB,bool)),fun(type,bool)),fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),combb(fun(type,fun(dB,bool)),fun(type,bool),fun(nat,type)),aa(fun(fun(dB,bool),bool),fun(fun(type,fun(dB,bool)),fun(type,bool)),combb(fun(dB,bool),bool,type),fAll(dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool))))),combb(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool))),dB),aa(fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool)),fun(nat,type)),aa(fun(fun(dB,fun(nat,bool)),fun(dB,bool)),fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),combb(fun(dB,fun(nat,bool)),fun(dB,bool),type),aa(fun(fun(nat,bool),bool),fun(fun(dB,fun(nat,bool)),fun(dB,bool)),combb(fun(nat,bool),bool,dB),fAll(nat))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),combs(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),dB),combs(fun(nat,type),fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))),fun(nat,type)),combc(type,fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(nat,type)),aa(fun(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),type),combb(fun(nat,bool),fun(nat,bool),dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),dB),aa(fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool))),fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool)),type),combs(nat,bool,bool)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),dB),aa(fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),combb(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool))),fun(nat,type)),aa(fun(fun(nat,bool),fun(nat,fun(bool,bool))),fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),combb(fun(nat,bool),fun(nat,fun(bool,bool)),type),aa(fun(bool,fun(bool,bool)),fun(fun(nat,bool),fun(nat,fun(bool,bool))),combb(bool,fun(bool,bool),nat),fimplies)))),aa(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool))))),combb(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool))),dB),aa(fun(fun(nat,fun(type,bool)),fun(type,fun(nat,bool))),fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),combb(fun(nat,fun(type,bool)),fun(type,fun(nat,bool)),fun(nat,type)),combc(nat,type,bool))),aa(fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),combc(fun(nat,type),dB,fun(nat,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),aa(fun(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool))))),combb(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool))),fun(nat,type)),combc(nat,dB,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),aa(fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool))))),combb(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool))),fun(nat,type)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),combb(fun(nat,type),fun(dB,fun(type,bool)),nat),typing)),aa(type,fun(fun(nat,type),fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),fun(type,fun(fun(nat,type),fun(nat,fun(nat,type)))),combc(fun(nat,type),type,fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),aa(fun(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type)))),fun(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type))))),combb(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type))),fun(nat,type)),combc(nat,type,fun(nat,type))),shift(type))),t))))))))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)),fun(nat,type)),aa(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),combs(dB,fun(nat,bool),fun(nat,bool)),aa(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat)),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies),it))))),aa(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combc(fun(nat,type),fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(nat,type)),combs(dB,fun(nat,bool),fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),aa(fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat))),aa(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool))),aa(fun(fun(dB,bool),fun(dB,fun(bool,bool))),fun(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool)))),combb(fun(dB,bool),fun(dB,fun(bool,bool)),fun(nat,type)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies)),aa(type,fun(fun(nat,type),fun(dB,bool)),aa(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(type,fun(fun(nat,type),fun(dB,bool))),combc(fun(nat,type),type,fun(dB,bool)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool))),aa(fun(fun(dB,fun(type,bool)),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(dB,fun(type,bool)),fun(type,fun(dB,bool)),fun(nat,type)),combc(dB,type,bool)),typing)),t)))))),aa(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool))),aa(fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),fun(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool)),dB),aa(fun(fun(nat,dB),fun(nat,bool)),fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),combb(fun(nat,dB),fun(nat,bool),dB),aa(fun(dB,bool),fun(fun(nat,dB),fun(nat,bool)),combb(dB,bool,nat),it))),subst)))))))))),aa(fun(dB,fun(type,bool)),fun(dB,bool),aa(fun(fun(type,bool),bool),fun(fun(dB,fun(type,bool)),fun(dB,bool)),combb(fun(type,bool),bool,dB),fEx(type)),aa(fun(nat,type),fun(dB,fun(type,bool)),typing,aa(type,fun(nat,type),aa(nat,fun(type,fun(nat,type)),aa(fun(nat,type),fun(nat,fun(type,fun(nat,type))),shift(type),e),i),t)))),as),
    inference(flattening,[],[f119]) ).

tff(f178,plain,
    ! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool),X3: list(X0)] :
      ( ( listsp(X0,aa(fun(X0,bool),fun(X0,bool),aa(fun(X0,fun(bool,bool)),fun(fun(X0,bool),fun(X0,bool)),combs(X0,bool,bool),aa(fun(X0,bool),fun(X0,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(X0,bool),fun(X0,fun(bool,bool))),combb(bool,fun(bool,bool),X0),fconj),X2)),X1),X3)
        | ~ listsp(X0,X2,X3)
        | ~ listsp(X0,X1,X3) )
      & ( ( listsp(X0,X2,X3)
          & listsp(X0,X1,X3) )
        | ~ listsp(X0,aa(fun(X0,bool),fun(X0,bool),aa(fun(X0,fun(bool,bool)),fun(fun(X0,bool),fun(X0,bool)),combs(X0,bool,bool),aa(fun(X0,bool),fun(X0,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(X0,bool),fun(X0,fun(bool,bool))),combb(bool,fun(bool,bool),X0),fconj),X2)),X1),X3) ) ),
    inference(nnf_transformation,[],[f14]) ).

tff(f179,plain,
    ! [X0: $tType,X1: fun(X0,bool),X2: fun(X0,bool),X3: list(X0)] :
      ( ( listsp(X0,aa(fun(X0,bool),fun(X0,bool),aa(fun(X0,fun(bool,bool)),fun(fun(X0,bool),fun(X0,bool)),combs(X0,bool,bool),aa(fun(X0,bool),fun(X0,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(X0,bool),fun(X0,fun(bool,bool))),combb(bool,fun(bool,bool),X0),fconj),X2)),X1),X3)
        | ~ listsp(X0,X2,X3)
        | ~ listsp(X0,X1,X3) )
      & ( ( listsp(X0,X2,X3)
          & listsp(X0,X1,X3) )
        | ~ listsp(X0,aa(fun(X0,bool),fun(X0,bool),aa(fun(X0,fun(bool,bool)),fun(fun(X0,bool),fun(X0,bool)),combs(X0,bool,bool),aa(fun(X0,bool),fun(X0,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(X0,bool),fun(X0,fun(bool,bool))),combb(bool,fun(bool,bool),X0),fconj),X2)),X1),X3) ) ),
    inference(flattening,[],[f178]) ).

tff(f225,plain,
    listsp(dB,aa(fun(dB,fun(type,bool)),fun(dB,bool),aa(fun(fun(type,bool),bool),fun(fun(dB,fun(type,bool)),fun(dB,bool)),combb(fun(type,bool),bool,dB),fEx(type)),aa(fun(nat,type),fun(dB,fun(type,bool)),typing,aa(type,fun(nat,type),aa(nat,fun(type,fun(nat,type)),aa(fun(nat,type),fun(nat,fun(type,fun(nat,type))),shift(type),e),i),t))),as),
    inference(cnf_transformation,[],[f5]) ).

tff(f227,plain,
    listsp(dB,aa(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool),aa(fun(fun(fun(nat,type),bool),bool),fun(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool)),combb(fun(fun(nat,type),bool),bool,dB),fAll(fun(nat,type))),aa(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool)),aa(fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),fun(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool))),combb(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool),dB),aa(fun(fun(type,bool),bool),fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),combb(fun(type,bool),bool,fun(nat,type)),fAll(type))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool)))),combb(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool)),dB),aa(fun(fun(type,fun(dB,bool)),fun(type,bool)),fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),combb(fun(type,fun(dB,bool)),fun(type,bool),fun(nat,type)),aa(fun(fun(dB,bool),bool),fun(fun(type,fun(dB,bool)),fun(type,bool)),combb(fun(dB,bool),bool,type),fAll(dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool))))),combb(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool))),dB),aa(fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool)),fun(nat,type)),aa(fun(fun(dB,fun(nat,bool)),fun(dB,bool)),fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),combb(fun(dB,fun(nat,bool)),fun(dB,bool),type),aa(fun(fun(nat,bool),bool),fun(fun(dB,fun(nat,bool)),fun(dB,bool)),combb(fun(nat,bool),bool,dB),fAll(nat))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),combs(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),dB),combs(fun(nat,type),fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))),fun(nat,type)),combc(type,fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(nat,type)),aa(fun(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),type),combb(fun(nat,bool),fun(nat,bool),dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),dB),aa(fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool))),fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool)),type),combs(nat,bool,bool)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),dB),aa(fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),combb(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool))),fun(nat,type)),aa(fun(fun(nat,bool),fun(nat,fun(bool,bool))),fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),combb(fun(nat,bool),fun(nat,fun(bool,bool)),type),aa(fun(bool,fun(bool,bool)),fun(fun(nat,bool),fun(nat,fun(bool,bool))),combb(bool,fun(bool,bool),nat),fimplies)))),aa(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool))))),combb(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool))),dB),aa(fun(fun(nat,fun(type,bool)),fun(type,fun(nat,bool))),fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),combb(fun(nat,fun(type,bool)),fun(type,fun(nat,bool)),fun(nat,type)),combc(nat,type,bool))),aa(fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),combc(fun(nat,type),dB,fun(nat,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),aa(fun(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool))))),combb(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool))),fun(nat,type)),combc(nat,dB,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),aa(fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool))))),combb(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool))),fun(nat,type)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),combb(fun(nat,type),fun(dB,fun(type,bool)),nat),typing)),aa(type,fun(fun(nat,type),fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),fun(type,fun(fun(nat,type),fun(nat,fun(nat,type)))),combc(fun(nat,type),type,fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),aa(fun(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type)))),fun(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type))))),combb(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type))),fun(nat,type)),combc(nat,type,fun(nat,type))),shift(type))),t))))))))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)),fun(nat,type)),aa(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),combs(dB,fun(nat,bool),fun(nat,bool)),aa(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat)),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies),it))))),aa(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combc(fun(nat,type),fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(nat,type)),combs(dB,fun(nat,bool),fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),aa(fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat))),aa(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool))),aa(fun(fun(dB,bool),fun(dB,fun(bool,bool))),fun(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool)))),combb(fun(dB,bool),fun(dB,fun(bool,bool)),fun(nat,type)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies)),aa(type,fun(fun(nat,type),fun(dB,bool)),aa(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(type,fun(fun(nat,type),fun(dB,bool))),combc(fun(nat,type),type,fun(dB,bool)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool))),aa(fun(fun(dB,fun(type,bool)),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(dB,fun(type,bool)),fun(type,fun(dB,bool)),fun(nat,type)),combc(dB,type,bool)),typing)),t)))))),aa(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool))),aa(fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),fun(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool)),dB),aa(fun(fun(nat,dB),fun(nat,bool)),fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),combb(fun(nat,dB),fun(nat,bool),dB),aa(fun(dB,bool),fun(fun(nat,dB),fun(nat,bool)),combb(dB,bool,nat),it))),subst)))))))),as),
    inference(cnf_transformation,[],[f7]) ).

tff(f236,plain,
    ! [X0: $tType,X2: fun(X0,bool),X3: list(X0),X1: fun(X0,bool)] :
      ( listsp(X0,aa(fun(X0,bool),fun(X0,bool),aa(fun(X0,fun(bool,bool)),fun(fun(X0,bool),fun(X0,bool)),combs(X0,bool,bool),aa(fun(X0,bool),fun(X0,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(X0,bool),fun(X0,fun(bool,bool))),combb(bool,fun(bool,bool),X0),fconj),X2)),X1),X3)
      | ~ listsp(X0,X2,X3)
      | ~ listsp(X0,X1,X3) ),
    inference(cnf_transformation,[],[f179]) ).

tff(f388,plain,
    ~ listsp(dB,aa(fun(dB,bool),fun(dB,bool),aa(fun(dB,fun(bool,bool)),fun(fun(dB,bool),fun(dB,bool)),combs(dB,bool,bool),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fconj),aa(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool),aa(fun(fun(fun(nat,type),bool),bool),fun(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool)),combb(fun(fun(nat,type),bool),bool,dB),fAll(fun(nat,type))),aa(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool)),aa(fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),fun(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool))),combb(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool),dB),aa(fun(fun(type,bool),bool),fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),combb(fun(type,bool),bool,fun(nat,type)),fAll(type))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool)))),combb(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool)),dB),aa(fun(fun(type,fun(dB,bool)),fun(type,bool)),fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),combb(fun(type,fun(dB,bool)),fun(type,bool),fun(nat,type)),aa(fun(fun(dB,bool),bool),fun(fun(type,fun(dB,bool)),fun(type,bool)),combb(fun(dB,bool),bool,type),fAll(dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool))))),combb(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool))),dB),aa(fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool)),fun(nat,type)),aa(fun(fun(dB,fun(nat,bool)),fun(dB,bool)),fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),combb(fun(dB,fun(nat,bool)),fun(dB,bool),type),aa(fun(fun(nat,bool),bool),fun(fun(dB,fun(nat,bool)),fun(dB,bool)),combb(fun(nat,bool),bool,dB),fAll(nat))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),combs(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),dB),combs(fun(nat,type),fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))),fun(nat,type)),combc(type,fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(nat,type)),aa(fun(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),type),combb(fun(nat,bool),fun(nat,bool),dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),dB),aa(fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool))),fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool)),type),combs(nat,bool,bool)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),dB),aa(fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),combb(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool))),fun(nat,type)),aa(fun(fun(nat,bool),fun(nat,fun(bool,bool))),fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),combb(fun(nat,bool),fun(nat,fun(bool,bool)),type),aa(fun(bool,fun(bool,bool)),fun(fun(nat,bool),fun(nat,fun(bool,bool))),combb(bool,fun(bool,bool),nat),fimplies)))),aa(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool))))),combb(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool))),dB),aa(fun(fun(nat,fun(type,bool)),fun(type,fun(nat,bool))),fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),combb(fun(nat,fun(type,bool)),fun(type,fun(nat,bool)),fun(nat,type)),combc(nat,type,bool))),aa(fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),combc(fun(nat,type),dB,fun(nat,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),aa(fun(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool))))),combb(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool))),fun(nat,type)),combc(nat,dB,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),aa(fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool))))),combb(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool))),fun(nat,type)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),combb(fun(nat,type),fun(dB,fun(type,bool)),nat),typing)),aa(type,fun(fun(nat,type),fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),fun(type,fun(fun(nat,type),fun(nat,fun(nat,type)))),combc(fun(nat,type),type,fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),aa(fun(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type)))),fun(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type))))),combb(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type))),fun(nat,type)),combc(nat,type,fun(nat,type))),shift(type))),t))))))))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)),fun(nat,type)),aa(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),combs(dB,fun(nat,bool),fun(nat,bool)),aa(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat)),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies),it))))),aa(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combc(fun(nat,type),fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(nat,type)),combs(dB,fun(nat,bool),fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),aa(fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat))),aa(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool))),aa(fun(fun(dB,bool),fun(dB,fun(bool,bool))),fun(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool)))),combb(fun(dB,bool),fun(dB,fun(bool,bool)),fun(nat,type)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies)),aa(type,fun(fun(nat,type),fun(dB,bool)),aa(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(type,fun(fun(nat,type),fun(dB,bool))),combc(fun(nat,type),type,fun(dB,bool)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool))),aa(fun(fun(dB,fun(type,bool)),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(dB,fun(type,bool)),fun(type,fun(dB,bool)),fun(nat,type)),combc(dB,type,bool)),typing)),t)))))),aa(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool))),aa(fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),fun(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool)),dB),aa(fun(fun(nat,dB),fun(nat,bool)),fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),combb(fun(nat,dB),fun(nat,bool),dB),aa(fun(dB,bool),fun(fun(nat,dB),fun(nat,bool)),combb(dB,bool,nat),it))),subst)))))))))),aa(fun(dB,fun(type,bool)),fun(dB,bool),aa(fun(fun(type,bool),bool),fun(fun(dB,fun(type,bool)),fun(dB,bool)),combb(fun(type,bool),bool,dB),fEx(type)),aa(fun(nat,type),fun(dB,fun(type,bool)),typing,aa(type,fun(nat,type),aa(nat,fun(type,fun(nat,type)),aa(fun(nat,type),fun(nat,fun(type,fun(nat,type))),shift(type),e),i),t)))),as),
    inference(cnf_transformation,[],[f122]) ).

tff(f1557,plain,
    ( ~ listsp(dB,aa(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool),aa(fun(fun(fun(nat,type),bool),bool),fun(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool)),combb(fun(fun(nat,type),bool),bool,dB),fAll(fun(nat,type))),aa(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool)),aa(fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),fun(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool))),combb(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool),dB),aa(fun(fun(type,bool),bool),fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),combb(fun(type,bool),bool,fun(nat,type)),fAll(type))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool)))),combb(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool)),dB),aa(fun(fun(type,fun(dB,bool)),fun(type,bool)),fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),combb(fun(type,fun(dB,bool)),fun(type,bool),fun(nat,type)),aa(fun(fun(dB,bool),bool),fun(fun(type,fun(dB,bool)),fun(type,bool)),combb(fun(dB,bool),bool,type),fAll(dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool))))),combb(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool))),dB),aa(fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool)),fun(nat,type)),aa(fun(fun(dB,fun(nat,bool)),fun(dB,bool)),fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),combb(fun(dB,fun(nat,bool)),fun(dB,bool),type),aa(fun(fun(nat,bool),bool),fun(fun(dB,fun(nat,bool)),fun(dB,bool)),combb(fun(nat,bool),bool,dB),fAll(nat))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),combs(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),dB),combs(fun(nat,type),fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))),fun(nat,type)),combc(type,fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(nat,type)),aa(fun(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),type),combb(fun(nat,bool),fun(nat,bool),dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),dB),aa(fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool))),fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool)),type),combs(nat,bool,bool)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),dB),aa(fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),combb(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool))),fun(nat,type)),aa(fun(fun(nat,bool),fun(nat,fun(bool,bool))),fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),combb(fun(nat,bool),fun(nat,fun(bool,bool)),type),aa(fun(bool,fun(bool,bool)),fun(fun(nat,bool),fun(nat,fun(bool,bool))),combb(bool,fun(bool,bool),nat),fimplies)))),aa(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool))))),combb(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool))),dB),aa(fun(fun(nat,fun(type,bool)),fun(type,fun(nat,bool))),fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),combb(fun(nat,fun(type,bool)),fun(type,fun(nat,bool)),fun(nat,type)),combc(nat,type,bool))),aa(fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),combc(fun(nat,type),dB,fun(nat,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),aa(fun(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool))))),combb(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool))),fun(nat,type)),combc(nat,dB,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),aa(fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool))))),combb(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool))),fun(nat,type)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),combb(fun(nat,type),fun(dB,fun(type,bool)),nat),typing)),aa(type,fun(fun(nat,type),fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),fun(type,fun(fun(nat,type),fun(nat,fun(nat,type)))),combc(fun(nat,type),type,fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),aa(fun(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type)))),fun(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type))))),combb(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type))),fun(nat,type)),combc(nat,type,fun(nat,type))),shift(type))),t))))))))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)),fun(nat,type)),aa(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),combs(dB,fun(nat,bool),fun(nat,bool)),aa(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat)),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies),it))))),aa(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combc(fun(nat,type),fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(nat,type)),combs(dB,fun(nat,bool),fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),aa(fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat))),aa(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool))),aa(fun(fun(dB,bool),fun(dB,fun(bool,bool))),fun(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool)))),combb(fun(dB,bool),fun(dB,fun(bool,bool)),fun(nat,type)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies)),aa(type,fun(fun(nat,type),fun(dB,bool)),aa(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(type,fun(fun(nat,type),fun(dB,bool))),combc(fun(nat,type),type,fun(dB,bool)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool))),aa(fun(fun(dB,fun(type,bool)),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(dB,fun(type,bool)),fun(type,fun(dB,bool)),fun(nat,type)),combc(dB,type,bool)),typing)),t)))))),aa(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool))),aa(fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),fun(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool)),dB),aa(fun(fun(nat,dB),fun(nat,bool)),fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),combb(fun(nat,dB),fun(nat,bool),dB),aa(fun(dB,bool),fun(fun(nat,dB),fun(nat,bool)),combb(dB,bool,nat),it))),subst)))))))),as)
    | ~ listsp(dB,aa(fun(dB,fun(type,bool)),fun(dB,bool),aa(fun(fun(type,bool),bool),fun(fun(dB,fun(type,bool)),fun(dB,bool)),combb(fun(type,bool),bool,dB),fEx(type)),aa(fun(nat,type),fun(dB,fun(type,bool)),typing,aa(type,fun(nat,type),aa(nat,fun(type,fun(nat,type)),aa(fun(nat,type),fun(nat,fun(type,fun(nat,type))),shift(type),e),i),t))),as) ),
    inference(resolution,[],[f388,f236]) ).

tff(f1559,definition,
    ( spl29_72
  <=> listsp(dB,aa(fun(dB,fun(type,bool)),fun(dB,bool),aa(fun(fun(type,bool),bool),fun(fun(dB,fun(type,bool)),fun(dB,bool)),combb(fun(type,bool),bool,dB),fEx(type)),aa(fun(nat,type),fun(dB,fun(type,bool)),typing,aa(type,fun(nat,type),aa(nat,fun(type,fun(nat,type)),aa(fun(nat,type),fun(nat,fun(type,fun(nat,type))),shift(type),e),i),t))),as) ),
    introduced(definition,[new_symbols(definition,[spl29_72])],[avatar_definition]) ).

tff(f1561,plain,
    ( ~ listsp(dB,aa(fun(dB,fun(type,bool)),fun(dB,bool),aa(fun(fun(type,bool),bool),fun(fun(dB,fun(type,bool)),fun(dB,bool)),combb(fun(type,bool),bool,dB),fEx(type)),aa(fun(nat,type),fun(dB,fun(type,bool)),typing,aa(type,fun(nat,type),aa(nat,fun(type,fun(nat,type)),aa(fun(nat,type),fun(nat,fun(type,fun(nat,type))),shift(type),e),i),t))),as)
    | spl29_72 ),
    inference(avatar_component_clause,[],[f1559]) ).

tff(f1563,definition,
    ( spl29_73
  <=> listsp(dB,aa(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool),aa(fun(fun(fun(nat,type),bool),bool),fun(fun(dB,fun(fun(nat,type),bool)),fun(dB,bool)),combb(fun(fun(nat,type),bool),bool,dB),fAll(fun(nat,type))),aa(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool)),aa(fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),fun(fun(dB,fun(fun(nat,type),fun(type,bool))),fun(dB,fun(fun(nat,type),bool))),combb(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool),dB),aa(fun(fun(type,bool),bool),fun(fun(fun(nat,type),fun(type,bool)),fun(fun(nat,type),bool)),combb(fun(type,bool),bool,fun(nat,type)),fAll(type))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(dB,fun(fun(nat,type),fun(type,bool)))),combb(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool)),dB),aa(fun(fun(type,fun(dB,bool)),fun(type,bool)),fun(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(fun(nat,type),fun(type,bool))),combb(fun(type,fun(dB,bool)),fun(type,bool),fun(nat,type)),aa(fun(fun(dB,bool),bool),fun(fun(type,fun(dB,bool)),fun(type,bool)),combb(fun(dB,bool),bool,type),fAll(dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool)))),aa(fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,bool))))),combb(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool))),dB),aa(fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool)),fun(nat,type)),aa(fun(fun(dB,fun(nat,bool)),fun(dB,bool)),fun(fun(type,fun(dB,fun(nat,bool))),fun(type,fun(dB,bool))),combb(fun(dB,fun(nat,bool)),fun(dB,bool),type),aa(fun(fun(nat,bool),bool),fun(fun(dB,fun(nat,bool)),fun(dB,bool)),combb(fun(nat,bool),bool,dB),fAll(nat))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),combs(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(dB,fun(nat,bool))))),dB),combs(fun(nat,type),fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(dB,fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(type,fun(dB,fun(nat,bool)))),fun(nat,type)),combc(type,fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),aa(fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))))),combb(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),dB),aa(fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),fun(fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))))),combb(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(nat,type)),aa(fun(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(type,fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,bool),fun(nat,bool)),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),type),combb(fun(nat,bool),fun(nat,bool),dB)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(dB,fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool)))),dB),aa(fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),fun(fun(nat,type),fun(type,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool))),fun(fun(type,fun(nat,fun(bool,bool))),fun(type,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(nat,fun(bool,bool)),fun(fun(nat,bool),fun(nat,bool)),type),combs(nat,bool,bool)))),aa(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),aa(fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),fun(fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))))),combb(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool)))),dB),aa(fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),fun(fun(fun(nat,type),fun(type,fun(nat,bool))),fun(fun(nat,type),fun(type,fun(nat,fun(bool,bool))))),combb(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool))),fun(nat,type)),aa(fun(fun(nat,bool),fun(nat,fun(bool,bool))),fun(fun(type,fun(nat,bool)),fun(type,fun(nat,fun(bool,bool)))),combb(fun(nat,bool),fun(nat,fun(bool,bool)),type),aa(fun(bool,fun(bool,bool)),fun(fun(nat,bool),fun(nat,fun(bool,bool))),combb(bool,fun(bool,bool),nat),fimplies)))),aa(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(type,fun(nat,bool))))),combb(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool))),dB),aa(fun(fun(nat,fun(type,bool)),fun(type,fun(nat,bool))),fun(fun(fun(nat,type),fun(nat,fun(type,bool))),fun(fun(nat,type),fun(type,fun(nat,bool)))),combb(fun(nat,fun(type,bool)),fun(type,fun(nat,bool)),fun(nat,type)),combc(nat,type,bool))),aa(fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),fun(dB,fun(fun(nat,type),fun(nat,fun(type,bool)))),combc(fun(nat,type),dB,fun(nat,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool)))),aa(fun(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),fun(fun(nat,type),fun(dB,fun(nat,fun(type,bool))))),combb(fun(nat,fun(dB,fun(type,bool))),fun(dB,fun(nat,fun(type,bool))),fun(nat,type)),combc(nat,dB,fun(type,bool))),aa(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool)))),aa(fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),fun(fun(fun(nat,type),fun(nat,fun(nat,type))),fun(fun(nat,type),fun(nat,fun(dB,fun(type,bool))))),combb(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool))),fun(nat,type)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,fun(nat,type)),fun(nat,fun(dB,fun(type,bool)))),combb(fun(nat,type),fun(dB,fun(type,bool)),nat),typing)),aa(type,fun(fun(nat,type),fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),fun(type,fun(fun(nat,type),fun(nat,fun(nat,type)))),combc(fun(nat,type),type,fun(nat,fun(nat,type))),aa(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type)))),aa(fun(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type)))),fun(fun(fun(nat,type),fun(nat,fun(type,fun(nat,type)))),fun(fun(nat,type),fun(type,fun(nat,fun(nat,type))))),combb(fun(nat,fun(type,fun(nat,type))),fun(type,fun(nat,fun(nat,type))),fun(nat,type)),combc(nat,type,fun(nat,type))),shift(type))),t))))))))))),aa(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(fun(fun(nat,type),fun(dB,fun(nat,bool))),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)),fun(nat,type)),aa(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),combs(dB,fun(nat,bool),fun(nat,bool)),aa(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat)),aa(fun(dB,bool),fun(dB,fun(bool,bool)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies),it))))),aa(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(dB,fun(nat,bool))),fun(dB,fun(fun(nat,type),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool))),dB),aa(fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(dB,fun(nat,bool)),fun(fun(nat,type),fun(dB,fun(nat,bool)))),combc(fun(nat,type),fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),aa(fun(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(nat,type),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))))),combb(fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(nat,bool)),fun(dB,fun(nat,bool))),fun(nat,type)),combs(dB,fun(nat,bool),fun(nat,bool))),aa(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),aa(fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),fun(fun(fun(nat,type),fun(dB,fun(bool,bool))),fun(fun(nat,type),fun(dB,fun(fun(nat,bool),fun(nat,bool))))),combb(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool))),fun(nat,type)),aa(fun(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool))),fun(fun(dB,fun(bool,bool)),fun(dB,fun(fun(nat,bool),fun(nat,bool)))),combb(fun(bool,bool),fun(fun(nat,bool),fun(nat,bool)),dB),combb(bool,bool,nat))),aa(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool))),aa(fun(fun(dB,bool),fun(dB,fun(bool,bool))),fun(fun(fun(nat,type),fun(dB,bool)),fun(fun(nat,type),fun(dB,fun(bool,bool)))),combb(fun(dB,bool),fun(dB,fun(bool,bool)),fun(nat,type)),aa(fun(bool,fun(bool,bool)),fun(fun(dB,bool),fun(dB,fun(bool,bool))),combb(bool,fun(bool,bool),dB),fimplies)),aa(type,fun(fun(nat,type),fun(dB,bool)),aa(fun(fun(nat,type),fun(type,fun(dB,bool))),fun(type,fun(fun(nat,type),fun(dB,bool))),combc(fun(nat,type),type,fun(dB,bool)),aa(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool))),aa(fun(fun(dB,fun(type,bool)),fun(type,fun(dB,bool))),fun(fun(fun(nat,type),fun(dB,fun(type,bool))),fun(fun(nat,type),fun(type,fun(dB,bool)))),combb(fun(dB,fun(type,bool)),fun(type,fun(dB,bool)),fun(nat,type)),combc(dB,type,bool)),typing)),t)))))),aa(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool))),aa(fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),fun(fun(dB,fun(dB,fun(nat,dB))),fun(dB,fun(dB,fun(nat,bool)))),combb(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool)),dB),aa(fun(fun(nat,dB),fun(nat,bool)),fun(fun(dB,fun(nat,dB)),fun(dB,fun(nat,bool))),combb(fun(nat,dB),fun(nat,bool),dB),aa(fun(dB,bool),fun(fun(nat,dB),fun(nat,bool)),combb(dB,bool,nat),it))),subst)))))))),as) ),
    introduced(definition,[new_symbols(definition,[spl29_73])],[avatar_definition]) ).

tff(f1566,plain,
    ( ~ spl29_72
    | ~ spl29_73 ),
    inference(avatar_split_clause,[],[f1557,f1563,f1559]) ).

tff(f1579,plain,
    spl29_73,
    inference(avatar_split_clause,[],[f227,f1563]) ).

tff(f1582,plain,
    ( $false
    | spl29_72 ),
    inference(resolution,[],[f1561,f225]) ).

tff(f1583,plain,
    spl29_72,
    inference(avatar_contradiction_clause,[],[f1582]) ).

cnf(s118,plain,
    ( ~ spl29_72
    | ~ spl29_73 ),
    inference(sat_conversion,[],[f1566]) ).

cnf(s119,plain,
    spl29_73,
    inference(sat_conversion,[],[f1579]) ).

cnf(s120,plain,
    spl29_72,
    inference(sat_conversion,[],[f1583]) ).

cnf(s121,plain,
    $false,
    inference(rat,[],[s118,s119,s120]) ).

tff(f1584,plain,
    $false,
    inference(avatar_sat_refutation,[],[s121]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : LCL803_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38  % Computer : n003.cluster.edu
% 0.10/0.38  % Model    : x86_64 x86_64
% 0.10/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38  % Memory   : 8046.5625MB
% 0.10/0.38  % OS       : Linux 6.8.0-71-generic
% 0.10/0.38  % CPULimit : 300
% 0.10/0.38  % WCLimit  : 300
% 0.10/0.38  % DateTime : Sun Sep 27 16:54:41 UTC 2026
% 0.10/0.39  % CPUTime  : 
% 0.10/0.39  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.42  Running first-order model finding
% 0.10/0.42  Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.70/1.35  % (777453)Will run a generic schedule for satisfiability detection.
% 5.70/1.35  % (777470)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3784893656_2999 on theBenchmark for (2999ds/0Mi)
% 5.70/1.35  % (777471)% WARNING: option uhcvi not known.
% 5.70/1.35  % Exception at run slice level
% 5.70/1.35  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.70/1.35  % (777471)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1320379841:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.70/1.35  % (777472)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2445802851:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.70/1.35  % (777473)dis+10_1_sil=32000:sp=arity:random_seed=2476726507:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.70/1.35  % (777474)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2082754401:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.70/1.35  % (777476)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4187798875:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.70/1.35  % (777477)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1817422601:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.70/1.35  % (777479)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3316038178:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.70/1.35  % Exception at run slice level
% 5.70/1.35  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.70/1.35  % (777492)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3340926931:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.70/1.35  % (777474)Instruction limit reached! 
% 5.70/1.35  % (777474)------------------------------
% 5.70/1.35  % (777474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.35  % (777474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.35  % (777474)CaDiCaL version: 2.1.3
% 5.70/1.35  % (777474)Termination reason: Instruction limit
% 5.70/1.35  % (777474)Termination phase: Saturation
% 5.70/1.35  % (777474)Time elapsed: 0.056 s
% 5.70/1.35  % (777474)Peak memory usage: 12 MB
% 5.70/1.35  % (777474)Instructions burned: 116 (million)
% 5.70/1.35  % (777473)Instruction limit reached! 
% 5.70/1.35  % (777473)------------------------------
% 5.70/1.35  % (777473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.35  % (777473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.35  % (777473)CaDiCaL version: 2.1.3
% 5.70/1.35  % (777473)Termination reason: Instruction limit
% 5.70/1.35  % (777473)Termination phase: Saturation
% 5.70/1.35  % (777473)Time elapsed: 0.058 s
% 5.70/1.35  % (777473)Peak memory usage: 12 MB
% 5.70/1.35  % (777473)Instructions burned: 104 (million)
% 5.70/1.35  % (777476)Instruction limit reached! 
% 5.70/1.35  % (777476)------------------------------
% 5.70/1.35  % (777476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.35  % (777476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.35  % (777476)CaDiCaL version: 2.1.3
% 5.70/1.35  % (777476)Termination reason: Instruction limit
% 5.70/1.35  % (777476)Termination phase: Saturation
% 5.70/1.35  % (777476)Time elapsed: 0.072 s
% 5.70/1.35  % (777476)Peak memory usage: 12 MB
% 5.70/1.35  % (777476)Instructions burned: 131 (million)
% 5.70/1.35  % (777496)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3632895543:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.70/1.35  % (777497)ott-21_1_sil=16000:fs=off:random_seed=2131729908:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.70/1.35  % (777492)Instruction limit reached! 
% 5.70/1.35  % (777492)------------------------------
% 5.70/1.35  % (777492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.35  % (777492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.35  % (777492)CaDiCaL version: 2.1.3
% 5.70/1.35  % (777492)Termination reason: Instruction limit
% 5.70/1.35  % (777492)Termination phase: Saturation
% 5.70/1.35  % (777492)Time elapsed: 0.037 s
% 5.70/1.35  % (777492)Peak memory usage: 14 MB
% 5.70/1.35  % (777492)Instructions burned: 133 (million)
% 5.70/1.35  % (777477)Instruction limit reached! 
% 5.70/1.35  % (777477)------------------------------
% 20.18/3.35  % (777477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.18/3.35  % (777477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.18/3.35  % (777477)CaDiCaL version: 2.1.3
% 20.18/3.35  % (777477)Termination reason: Instruction limit
% 20.18/3.35  % (777477)Termination phase: Saturation
% 20.18/3.35  % (777477)Time elapsed: 0.083 s
% 20.18/3.35  % (777477)Peak memory usage: 12 MB
% 20.18/3.35  % (777477)Instructions burned: 160 (million)
% 20.18/3.35  % (777505)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1717401030:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 20.18/3.35  % (777500)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3646988478:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 20.18/3.35  % Exception at run slice level
% 20.18/3.35  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 20.18/3.35  % (777508)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=592081974:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 20.18/3.35  % (777515)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1354261829:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 20.18/3.35  % Exception at run slice level
% 20.18/3.35  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 20.18/3.35  % (777523)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2191349079:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 20.18/3.35  % (777497)Instruction limit reached! 
% 20.18/3.35  % (777497)------------------------------
% 20.18/3.35  % (777497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.18/3.35  % (777497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.18/3.35  % (777497)CaDiCaL version: 2.1.3
% 20.18/3.35  % (777497)Termination reason: Instruction limit
% 20.18/3.35  % (777497)Termination phase: Saturation
% 20.18/3.35  % (777497)Time elapsed: 0.090 s
% 20.18/3.35  % (777497)Peak memory usage: 13 MB
% 20.18/3.35  % (777497)Instructions burned: 180 (million)
% 20.18/3.35  % (777544)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1530280417:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 20.18/3.35  % (777500)Instruction limit reached! 
% 20.18/3.35  % (777500)------------------------------
% 20.18/3.35  % (777500)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.18/3.35  % (777500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.18/3.35  % (777500)CaDiCaL version: 2.1.3
% 20.18/3.35  % (777500)Termination reason: Instruction limit
% 20.18/3.35  % (777500)Termination phase: Saturation
% 20.18/3.35  % (777500)Time elapsed: 0.244 s
% 20.18/3.35  % (777500)Peak memory usage: 13 MB
% 20.18/3.35  % (777500)Instructions burned: 478 (million)
% 20.18/3.35  % (777523)Instruction limit reached! 
% 20.18/3.35  % (777523)------------------------------
% 20.18/3.35  % (777523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.18/3.35  % (777523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.18/3.35  % (777523)CaDiCaL version: 2.1.3
% 20.18/3.35  % (777523)Termination reason: Instruction limit
% 20.18/3.35  % (777523)Termination phase: Saturation
% 20.18/3.35  % (777523)Time elapsed: 0.212 s
% 20.18/3.35  % (777523)Peak memory usage: 15 MB
% 20.18/3.35  % (777523)Instructions burned: 694 (million)
% 20.18/3.35  % (777570)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2226618567:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 20.18/3.35  % (777569)fmb+10_1_sil=64000:random_seed=605256445:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 20.18/3.35  % Exception at run slice level
% 20.18/3.35  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 20.18/3.35  % (777569)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 20.18/3.35  % Exception at run slice level
% 20.18/3.35  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 20.18/3.35  % (777573)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2136152975:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 20.18/3.35  % (777574)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1360912350:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 21.21/3.51  % Exception at run slice level
% 21.21/3.51  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.21/3.51  % (777496)Instruction limit reached! 
% 21.21/3.51  % (777496)------------------------------
% 21.21/3.51  % (777496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777496)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777496)Termination reason: Instruction limit
% 21.21/3.51  % (777496)Termination phase: Saturation
% 21.21/3.51  % (777496)Time elapsed: 0.315 s
% 21.21/3.51  % (777496)Peak memory usage: 15 MB
% 21.21/3.51  % (777496)Instructions burned: 686 (million)
% 21.21/3.51  % (777577)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3761992751:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 21.21/3.51  % (777578)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2007083224:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 21.21/3.51  % (777577)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 21.21/3.51  % Exception at run slice level
% 21.21/3.51  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.21/3.51  % (777581)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1126183506:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 21.21/3.51  % Exception at run slice level
% 21.21/3.51  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.21/3.51  % (777583)ott-2_1_sil=16000:newcnf=on:random_seed=950180015:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 21.21/3.51  % (777508)Instruction limit reached! 
% 21.21/3.51  % (777508)------------------------------
% 21.21/3.51  % (777508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777508)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777508)Termination reason: Instruction limit
% 21.21/3.51  % (777508)Termination phase: Saturation
% 21.21/3.51  % (777508)Time elapsed: 0.552 s
% 21.21/3.51  % (777508)Peak memory usage: 15 MB
% 21.21/3.51  % (777508)Instructions burned: 1180 (million)
% 21.21/3.51  % (777544)Instruction limit reached! 
% 21.21/3.51  % (777544)------------------------------
% 21.21/3.51  % (777544)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777544)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777544)Termination reason: Instruction limit
% 21.21/3.51  % (777544)Termination phase: Saturation
% 21.21/3.51  % (777544)Time elapsed: 0.479 s
% 21.21/3.51  % (777544)Peak memory usage: 18 MB
% 21.21/3.51  % (777544)Instructions burned: 879 (million)
% 21.21/3.51  % (777585)ott+10_1_sil=32000:tgt=ground:random_seed=3341168628:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 21.21/3.51  % (777586)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=239516341:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 21.21/3.51  % Exception at run slice level
% 21.21/3.51  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.21/3.51  % (777589)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3460616987:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 21.21/3.51  % (777577)Instruction limit reached! 
% 21.21/3.51  % (777577)------------------------------
% 21.21/3.51  % (777577)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777577)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777577)Termination reason: Instruction limit
% 21.21/3.51  % (777577)Termination phase: Saturation
% 21.21/3.51  % (777577)Time elapsed: 0.363 s
% 21.21/3.51  % (777577)Peak memory usage: 20 MB
% 21.21/3.51  % (777577)Instructions burned: 1475 (million)
% 21.21/3.51  % (777591)dis+21_1_sil=32000:sas=cadical:random_seed=3429869825:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi)
% 21.21/3.51  % (777583)Instruction limit reached! 
% 21.21/3.51  % (777583)------------------------------
% 21.21/3.51  % (777583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777583)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777583)Termination reason: Instruction limit
% 21.21/3.51  % (777583)Termination phase: Saturation
% 21.21/3.51  % (777583)Time elapsed: 0.394 s
% 21.21/3.51  % (777583)Peak memory usage: 14 MB
% 21.21/3.51  % (777583)Instructions burned: 869 (million)
% 21.21/3.51  % (777593)ott+11_1_sil=16000:gs=on:random_seed=4250075679:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2990 on theBenchmark for (2990ds/2251Mi)
% 21.21/3.51  % (777591)Instruction limit reached! 
% 21.21/3.51  % (777591)------------------------------
% 21.21/3.51  % (777591)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777591)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777591)Termination reason: Instruction limit
% 21.21/3.51  % (777591)Termination phase: Saturation
% 21.21/3.51  % (777591)Time elapsed: 1.026 s
% 21.21/3.51  % (777591)Peak memory usage: 29 MB
% 21.21/3.51  % (777591)Instructions burned: 3776 (million)
% 21.21/3.51  % (777595)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3807058544:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi)
% 21.21/3.51  % Exception at run slice level
% 21.21/3.51  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.21/3.51  % (777597)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=269111752:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi)
% 21.21/3.51  % (777593)Instruction limit reached! 
% 21.21/3.51  % (777593)------------------------------
% 21.21/3.51  % (777593)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777593)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777593)Termination reason: Instruction limit
% 21.21/3.51  % (777593)Termination phase: Saturation
% 21.21/3.51  % (777593)Time elapsed: 1.272 s
% 21.21/3.51  % (777593)Peak memory usage: 27 MB
% 21.21/3.51  % (777593)Instructions burned: 2252 (million)
% 21.21/3.51  % (777599)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2085515784:i=29340_2977 on theBenchmark for (2977ds/29340Mi)
% 21.21/3.51  % (777589)Instruction limit reached! 
% 21.21/3.51  % (777589)------------------------------
% 21.21/3.51  % (777589)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777589)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777589)Termination reason: Instruction limit
% 21.21/3.51  % (777589)Termination phase: Saturation
% 21.21/3.51  % (777589)Time elapsed: 1.656 s
% 21.21/3.51  % (777589)Peak memory usage: 23 MB
% 21.21/3.51  % (777589)Instructions burned: 3513 (million)
% 21.21/3.51  % (777601)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3953156236:i=5211_2975 on theBenchmark for (2975ds/5211Mi)
% 21.21/3.51  % (777597)Instruction limit reached! 
% 21.21/3.51  % (777597)------------------------------
% 21.21/3.51  % (777597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777597)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777597)Termination reason: Instruction limit
% 21.21/3.51  % (777597)Termination phase: Saturation
% 21.21/3.51  % (777597)Time elapsed: 0.993 s
% 21.21/3.51  % (777597)Peak memory usage: 18 MB
% 21.21/3.51  % (777597)Instructions burned: 4595 (million)
% 21.21/3.51  % (777603)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2382270532:i=5497:nm=2_2971 on theBenchmark for (2971ds/5497Mi)
% 21.21/3.51  % (777585)Instruction limit reached! 
% 21.21/3.51  % (777585)------------------------------
% 21.21/3.51  % (777585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777585)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777585)Termination reason: Instruction limit
% 21.21/3.51  % (777585)Termination phase: Saturation
% 21.21/3.51  % (777585)Time elapsed: 2.169 s
% 21.21/3.51  % (777585)Peak memory usage: 14 MB
% 21.21/3.51  % (777585)Instructions burned: 5116 (million)
% 21.21/3.51  % Exception at run slice level
% 21.21/3.51  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.21/3.51  % (777606)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1539881990:i=14071_2970 on theBenchmark for (2970ds/14071Mi)
% 21.21/3.51  % Exception at run slice level
% 21.21/3.51  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.21/3.51  % (777605)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3099695241:fmbsr=2:i=46332_2970 on theBenchmark for (2970ds/46332Mi)
% 21.21/3.51  % (777574)Instruction limit reached! 
% 21.21/3.51  % (777574)------------------------------
% 21.21/3.51  % (777574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777574)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777574)Termination reason: Instruction limit
% 21.21/3.51  % (777574)Termination phase: Saturation
% 21.21/3.51  % (777574)Time elapsed: 2.492 s
% 21.21/3.51  % (777574)Peak memory usage: 28 MB
% 21.21/3.51  % (777574)Instructions burned: 5132 (million)
% 21.21/3.51  % (777609)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2486532009:i=22565:add=on:rawr=on_2970 on theBenchmark for (2970ds/22565Mi)
% 21.21/3.51  % Exception at run slice level
% 21.21/3.51  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 21.21/3.51  % (777611)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4052306172:i=8173:av=off_2970 on theBenchmark for (2970ds/8173Mi)
% 21.21/3.51  % (777612)dis+10_16:1_sil=16000:random_seed=487299698:i=9155:fsr=off_2970 on theBenchmark for (2970ds/9155Mi)
% 21.21/3.51  % (777612) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-777453-777612"...
% 21.21/3.51  % (777612)...printing done.
% 21.21/3.51  % (777612)Refutation found. Thanks to Tanya!
% 21.21/3.51  % SZS status Theorem for theBenchmark
% 21.21/3.51  % SZS output start Proof for theBenchmark
% See solution above
% 21.21/3.51  % (777612)------------------------------
% 21.21/3.51  % (777612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.21/3.51  % (777612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.21/3.51  % (777612)CaDiCaL version: 2.1.3
% 21.21/3.51  % (777612)Termination reason: Refutation
% 21.21/3.51  % (777612)Time elapsed: 0.115 s
% 21.21/3.51  % (777612)Peak memory usage: 14 MB
% 21.21/3.51  % (777612)Instructions burned: 201 (million)
% 21.21/3.51  % (777453)Success in time 3.08 s
% 21.21/3.51  % Vampire exiting
%------------------------------------------------------------------------------