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

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : COM113_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 : n004.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 09:40:19 AM UTC 2026

% Result   : Theorem 0.21s 0.35s
% Output   : Refutation 0.21s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    9
%            Number of leaves      :    7
% Syntax   : Number of formulae    :   31 (  22 unt;   0 typ;   0 def)
%            Number of atoms       :   40 (  28 equ)
%            Maximal formula atoms :    2 (   1 avg)
%            Number of connectives :   23 (  14   ~;   4   |;   2   &)
%                                         (   0 <=>;   3  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    7 (   3 avg)
%            Maximal term depth    :   23 (   2 avg)
%            Number of FOOLs       :    1 (   1 fml;   0 var)
%            Number of types       :    4 (   3 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :   22 (  20 usr;   1 prp; 0-5 aty)
%            Number of functors    :   48 (  48 usr;  12 con; 0-4 aty)
%            Number of variables   :   38 (  36   !;   2   ?;  38   :)

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

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

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

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

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

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

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

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

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

tff(func_def_3,type,
    combk: 
      !>[X0: $tType,X1: $tType] : ( X0 > fun(X1,X0) ) ).

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

tff(func_def_5,type,
    div_mod: 
      !>[X0: $tType] : ( ( X0 * X0 ) > X0 ) ).

tff(func_def_6,type,
    minus_minus: 
      !>[X0: $tType] : fun(X0,fun(X0,X0)) ).

tff(func_def_7,type,
    plus_plus: 
      !>[X0: $tType] : ( X0 > fun(X0,X0) ) ).

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

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

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

tff(func_def_11,type,
    nil: 
      !>[X0: $tType] : list(X0) ).

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

tff(func_def_13,type,
    bot_bot: 
      !>[X0: $tType] : X0 ).

tff(func_def_14,type,
    divisor: atom > int ).

tff(func_def_15,type,
    lbounds: list(atom) > list(product_prod(int,list(int))) ).

tff(func_def_16,type,
    product_Pair: 
      !>[X0: $tType,X1: $tType] : fun(X0,fun(X1,product_prod(X0,X1))) ).

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

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

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

tff(func_def_20,type,
    fFalse: bool ).

tff(func_def_21,type,
    fTrue: bool ).

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

tff(func_def_23,type,
    fdisj: fun(bool,fun(bool,bool)) ).

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

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

tff(func_def_26,type,
    a: atom ).

tff(func_def_27,type,
    as: list(atom) ).

tff(func_def_28,type,
    li: int ).

tff(func_def_29,type,
    lks: list(int) ).

tff(func_def_30,type,
    x: int ).

tff(func_def_31,type,
    xs: list(int) ).

tff(func_def_32,type,
    sK0: int ).

tff(func_def_33,type,
    sK1: list(int) ).

tff(func_def_34,type,
    sK2: 
      !>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > X0 ) ).

tff(func_def_35,type,
    sK3: 
      !>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > X1 ) ).

tff(func_def_36,type,
    sK4: 
      !>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > product_prod(X0,X1) ) ).

tff(func_def_37,type,
    sK5: 
      !>[X0: $tType,X1: $tType] : ( ( fun(X0,fun(X1,bool)) * fun(X1,bool) ) > X1 ) ).

tff(func_def_38,type,
    sK6: 
      !>[X0: $tType] : ( list(X0) > X0 ) ).

tff(func_def_39,type,
    sK7: 
      !>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > product_prod(X0,X1) ) ).

tff(func_def_40,type,
    sK8: 
      !>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > X0 ) ).

tff(func_def_41,type,
    sK9: 
      !>[X0: $tType,X1: $tType] : ( fun(product_prod(X0,X1),bool) > X1 ) ).

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

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

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

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

tff(pred_def_2,type,
    cl_Groups_Oplus: 
      !>[X0: $tType] : $o ).

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

tff(pred_def_4,type,
    cl_Groups_Ominus: 
      !>[X0: $tType] : $o ).

tff(pred_def_5,type,
    ring_div: 
      !>[X0: $tType] : $o ).

tff(pred_def_6,type,
    group_add: 
      !>[X0: $tType] : $o ).

tff(pred_def_7,type,
    finite_finite: 
      !>[X0: $tType] : $o ).

tff(pred_def_8,type,
    monoid_add: 
      !>[X0: $tType] : $o ).

tff(pred_def_9,type,
    linorder: 
      !>[X0: $tType] : $o ).

tff(pred_def_10,type,
    semiring_div: 
      !>[X0: $tType] : $o ).

tff(pred_def_11,type,
    comm_monoid_add: 
      !>[X0: $tType] : $o ).

tff(pred_def_12,type,
    ab_semigroup_add: 
      !>[X0: $tType] : $o ).

tff(pred_def_13,type,
    cancel_semigroup_add: 
      !>[X0: $tType] : $o ).

tff(pred_def_14,type,
    cancel146912293up_add: 
      !>[X0: $tType] : $o ).

tff(pred_def_15,type,
    linord219039673up_add: 
      !>[X0: $tType] : $o ).

tff(pred_def_16,type,
    linord2061991079up_add: 
      !>[X0: $tType] : $o ).

tff(pred_def_17,type,
    finite_finite1: 
      !>[X0: $tType] : ( fun(X0,bool) > $o ) ).

tff(pred_def_18,type,
    i_Z: ( atom * list(int) ) > $o ).

tff(pred_def_19,type,
    atom_case: 
      !>[X0: $tType] : ( ( fun(int,fun(list(int),X0)) * fun(int,fun(int,fun(list(int),X0))) * fun(int,fun(int,fun(list(int),X0))) * atom ) > $o ) ).

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

tff(f5,axiom,
    big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))) = aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_lm) ).

tff(f7,axiom,
    ~ ! [X0: int,X1: list(int)] :
        ( pp(aa(fun(product_prod(int,list(int)),bool),bool,aa(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),member(product_prod(int,list(int))),aa(list(int),product_prod(int,list(int)),aa(int,fun(list(int),product_prod(int,list(int))),product_Pair(int,list(int)),X0),X1)),set(product_prod(int,list(int)),lbounds(as))))
       => ( big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))) != aa(int,int,aa(int,fun(int,int),minus_minus(int),X0),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),X1),xs)) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6__096_B_Bthesis_O_A_I_B_Bli_Alks_O_A_091_124_A_Ili_M_Alks_J_A_058_Aset_A_Ilbounds_Aas_J_059_AMax_A_123i_A_N_A_092_060langle_062ks_Mxs_092_060rangle_062_A_124ks_Ai_O_A_Ii_M_Aks_J_A_058_Aset_A_Ilbounds_Aas_J_125_A_061_Ali_A_N_A_092_060langle_062lks_Mxs_092_060rangle_062_A_124_093_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096) ).

tff(f37,axiom,
    ! [X0: $tType] :
      ( semiring_div(X0)
     => ! [X1: X0,X2: X0,X3: X0] : ( div_mod(X0,aa(X0,X0,plus_plus(X0,X3),X2),X1) = div_mod(X0,aa(X0,X0,plus_plus(X0,div_mod(X0,X3,X1)),X2),X1) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_mod__add__left__eq) ).

tff(f38,axiom,
    ! [X0: $tType] :
      ( semiring_div(X0)
     => ! [X1: X0,X2: X0,X3: X0] : ( div_mod(X0,aa(X0,X0,plus_plus(X0,X3),X2),X1) = div_mod(X0,aa(X0,X0,plus_plus(X0,X3),div_mod(X0,X2,X1)),X1) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_mod__add__right__eq) ).

tff(f76,axiom,
    ! [X0: $tType,X1: fun(X0,bool)] : ( collect(X0,X1) = X1 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_Collect__def) ).

tff(f108,axiom,
    semiring_div(int),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Divides_Osemiring__div) ).

tff(f142,conjecture,
    div_mod(int,aa(int,int,plus_plus(int,div_mod(int,big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))),divisor(a))),div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),divisor(a))),divisor(a)) = div_mod(int,aa(int,int,plus_plus(int,big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))))),divisor(a)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

tff(f143,negated_conjecture,
    ( ( ~ div_mod(int,aa(int,int,plus_plus(int,div_mod(int,big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))),divisor(a))),div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),divisor(a))),divisor(a)) ) = div_mod(int,aa(int,int,plus_plus(int,big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))))),divisor(a)) ),
    inference(negated_conjecture,[status(cth)],[f142]) ).

tff(f144,plain,
    div_mod(int,aa(int,int,plus_plus(int,div_mod(int,big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))),divisor(a))),div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),divisor(a))),divisor(a)) != div_mod(int,aa(int,int,plus_plus(int,big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))))),divisor(a)),
    inference(flattening,[],[f143]) ).

tff(f150,plain,
    ? [X0: int,X1: list(int)] :
      ( ( big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))) = aa(int,int,aa(int,fun(int,int),minus_minus(int),X0),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),X1),xs)) )
      & pp(aa(fun(product_prod(int,list(int)),bool),bool,aa(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),member(product_prod(int,list(int))),aa(list(int),product_prod(int,list(int)),aa(int,fun(list(int),product_prod(int,list(int))),product_Pair(int,list(int)),X0),X1)),set(product_prod(int,list(int)),lbounds(as)))) ),
    inference(ennf_transformation,[],[f7]) ).

tff(f176,plain,
    ! [X0: $tType] :
      ( ! [X1: X0,X2: X0,X3: X0] : ( div_mod(X0,aa(X0,X0,plus_plus(X0,X3),X2),X1) = div_mod(X0,aa(X0,X0,plus_plus(X0,div_mod(X0,X3,X1)),X2),X1) )
      | ~ semiring_div(X0) ),
    inference(ennf_transformation,[],[f37]) ).

tff(f177,plain,
    ! [X0: $tType] :
      ( ! [X1: X0,X2: X0,X3: X0] : ( div_mod(X0,aa(X0,X0,plus_plus(X0,X3),X2),X1) = div_mod(X0,aa(X0,X0,plus_plus(X0,X3),div_mod(X0,X2,X1)),X1) )
      | ~ semiring_div(X0) ),
    inference(ennf_transformation,[],[f38]) ).

tff(f226,plain,
    ( ( big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))) = aa(int,int,aa(int,fun(int,int),minus_minus(int),sK0),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),sK1),xs)) )
    & pp(aa(fun(product_prod(int,list(int)),bool),bool,aa(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),member(product_prod(int,list(int))),aa(list(int),product_prod(int,list(int)),aa(int,fun(list(int),product_prod(int,list(int))),product_Pair(int,list(int)),sK0),sK1)),set(product_prod(int,list(int)),lbounds(as)))) ),
    inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f150]) ).

tff(f267,plain,
    big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))) = aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs)),
    inference(cnf_transformation,[],[f5]) ).

tff(f270,plain,
    big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))) = aa(int,int,aa(int,fun(int,int),minus_minus(int),sK0),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),sK1),xs)),
    inference(cnf_transformation,[],[f226]) ).

tff(f307,plain,
    ! [X0: $tType,X2: X0,X3: X0,X1: X0] :
      ( ~ semiring_div(X0)
      | ( div_mod(X0,aa(X0,X0,plus_plus(X0,X3),X2),X1) = div_mod(X0,aa(X0,X0,plus_plus(X0,div_mod(X0,X3,X1)),X2),X1) ) ),
    inference(cnf_transformation,[],[f176]) ).

tff(f308,plain,
    ! [X0: $tType,X2: X0,X3: X0,X1: X0] :
      ( ~ semiring_div(X0)
      | ( div_mod(X0,aa(X0,X0,plus_plus(X0,X3),div_mod(X0,X2,X1)),X1) = div_mod(X0,aa(X0,X0,plus_plus(X0,X3),X2),X1) ) ),
    inference(cnf_transformation,[],[f177]) ).

tff(f359,plain,
    ! [X0: $tType,X1: fun(X0,bool)] : ( collect(X0,X1) = X1 ),
    inference(cnf_transformation,[],[f76]) ).

tff(f395,plain,
    semiring_div(int),
    inference(cnf_transformation,[],[f108]) ).

tff(f429,plain,
    div_mod(int,aa(int,int,plus_plus(int,div_mod(int,big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))),divisor(a))),div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),divisor(a))),divisor(a)) != div_mod(int,aa(int,int,plus_plus(int,big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,collect(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))))),divisor(a)),
    inference(cnf_transformation,[],[f144]) ).

tff(f451,plain,
    div_mod(int,aa(int,int,plus_plus(int,div_mod(int,big_linorder_Max(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))),divisor(a))),div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))),divisor(a))),divisor(a)) != div_mod(int,aa(int,int,plus_plus(int,big_linorder_Max(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as)))))))),aa(int,int,aa(int,fun(int,int),minus_minus(int),x),big_linorder_Max(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))))),divisor(a)),
    inference(backward_demodulation,[],[f429,f359]) ).

tff(f466,plain,
    aa(int,int,aa(int,fun(int,int),minus_minus(int),sK0),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),sK1),xs)) = big_linorder_Max(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))),
    inference(forward_demodulation,[],[f270,f359]) ).

tff(f467,plain,
    aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs)) = big_linorder_Max(int,aa(fun(int,fun(list(int),bool)),fun(int,bool),aa(fun(fun(list(int),bool),bool),fun(fun(int,fun(list(int),bool)),fun(int,bool)),combb(fun(list(int),bool),bool,int),fEx(list(int))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool)),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),bool))),combb(fun(list(int),fun(int,bool)),fun(list(int),bool),int),aa(fun(fun(int,bool),bool),fun(fun(list(int),fun(int,bool)),fun(list(int),bool)),combb(fun(int,bool),bool,list(int)),fEx(int))),aa(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,bool)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),aa(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),aa(fun(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(int,fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))))),combb(fun(list(int),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,bool))),int),combs(list(int),fun(int,bool),fun(int,bool))),aa(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool)))),aa(fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),fun(fun(int,fun(list(int),fun(int,fun(bool,bool)))),fun(int,fun(list(int),fun(fun(int,bool),fun(int,bool))))),combb(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool))),int),aa(fun(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(bool,bool))),fun(list(int),fun(fun(int,bool),fun(int,bool)))),combb(fun(int,fun(bool,bool)),fun(fun(int,bool),fun(int,bool)),list(int)),combs(int,bool,bool))),aa(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool)))),aa(fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),fun(fun(int,fun(list(int),fun(int,bool))),fun(int,fun(list(int),fun(int,fun(bool,bool))))),combb(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool))),int),aa(fun(fun(int,bool),fun(int,fun(bool,bool))),fun(fun(list(int),fun(int,bool)),fun(list(int),fun(int,fun(bool,bool)))),combb(fun(int,bool),fun(int,fun(bool,bool)),list(int)),aa(fun(bool,fun(bool,bool)),fun(fun(int,bool),fun(int,fun(bool,bool))),combb(bool,fun(bool,bool),int),fconj))),aa(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(list(int),fun(int,int)),fun(int,fun(list(int),fun(int,bool)))),combc(int,fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),aa(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),aa(fun(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool)))),fun(fun(int,fun(fun(int,int),fun(int,bool))),fun(int,fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))))),combb(fun(fun(int,int),fun(int,bool)),fun(fun(list(int),fun(int,int)),fun(list(int),fun(int,bool))),int),combb(fun(int,int),fun(int,bool),list(int))),aa(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool))),aa(fun(fun(int,bool),fun(fun(int,int),fun(int,bool))),fun(fun(int,fun(int,bool)),fun(int,fun(fun(int,int),fun(int,bool)))),combb(fun(int,bool),fun(fun(int,int),fun(int,bool)),int),combb(int,bool,int)),fequal(int)))),aa(fun(list(int),int),fun(list(int),fun(int,int)),aa(fun(int,fun(int,int)),fun(fun(list(int),int),fun(list(int),fun(int,int))),combb(int,fun(int,int),list(int)),aa(fun(int,fun(int,int)),fun(int,fun(int,int)),combc(int,int,int),minus_minus(int))),aa(list(int),fun(list(int),int),aa(fun(list(int),fun(list(int),int)),fun(list(int),fun(list(int),int)),combc(list(int),list(int),int),iprod(int)),xs))))))),aa(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool)),aa(fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(product_prod(int,list(int)),bool),fun(list(int),fun(int,bool))),combc(list(int),fun(product_prod(int,list(int)),bool),fun(int,bool)),aa(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),aa(fun(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool))),fun(fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(list(int),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)))),combb(fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(product_prod(int,list(int)),bool),fun(int,bool)),list(int)),combc(int,fun(product_prod(int,list(int)),bool),bool)),aa(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),aa(fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),fun(fun(list(int),fun(int,product_prod(int,list(int)))),fun(list(int),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)))),combb(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool)),list(int)),aa(fun(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool)),fun(fun(int,product_prod(int,list(int))),fun(int,fun(fun(product_prod(int,list(int)),bool),bool))),combb(product_prod(int,list(int)),fun(fun(product_prod(int,list(int)),bool),bool),int),member(product_prod(int,list(int))))),aa(fun(int,fun(list(int),product_prod(int,list(int)))),fun(list(int),fun(int,product_prod(int,list(int)))),combc(int,list(int),product_prod(int,list(int))),product_Pair(int,list(int)))))),set(product_prod(int,list(int)),lbounds(as))))))),
    inference(forward_demodulation,[],[f267,f359]) ).

tff(f478,plain,
    div_mod(int,aa(int,int,plus_plus(int,div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),sK0),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),sK1),xs)),divisor(a))),div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),x),aa(int,int,aa(int,fun(int,int),minus_minus(int),sK0),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),sK1),xs))),divisor(a))),divisor(a)) != div_mod(int,aa(int,int,plus_plus(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),sK0),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),sK1),xs))),aa(int,int,aa(int,fun(int,int),minus_minus(int),x),aa(int,int,aa(int,fun(int,int),minus_minus(int),sK0),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),sK1),xs)))),divisor(a)),
    inference(backward_demodulation,[],[f451,f466]) ).

tff(f479,plain,
    aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs)) = aa(int,int,aa(int,fun(int,int),minus_minus(int),sK0),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),sK1),xs)),
    inference(backward_demodulation,[],[f466,f467]) ).

tff(f484,plain,
    div_mod(int,aa(int,int,plus_plus(int,div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs)),divisor(a))),div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),x),aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs))),divisor(a))),divisor(a)) != div_mod(int,aa(int,int,plus_plus(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs))),aa(int,int,aa(int,fun(int,int),minus_minus(int),x),aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs)))),divisor(a)),
    inference(backward_demodulation,[],[f478,f479]) ).

tff(f904,plain,
    ! [X2: int,X0: int,X1: int] : ( div_mod(int,aa(int,int,plus_plus(int,X0),X1),X2) = div_mod(int,aa(int,int,plus_plus(int,div_mod(int,X0,X2)),X1),X2) ),
    inference(resolution,[],[f307,f395]) ).

tff(f905,plain,
    div_mod(int,aa(int,int,plus_plus(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs))),aa(int,int,aa(int,fun(int,int),minus_minus(int),x),aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs)))),divisor(a)) != div_mod(int,aa(int,int,plus_plus(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs))),div_mod(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),x),aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs))),divisor(a))),divisor(a)),
    inference(backward_demodulation,[],[f484,f904]) ).

tff(f924,plain,
    ! [X2: int,X0: int,X1: int] : ( div_mod(int,aa(int,int,plus_plus(int,X0),X1),X2) = div_mod(int,aa(int,int,plus_plus(int,X0),div_mod(int,X1,X2)),X2) ),
    inference(resolution,[],[f308,f395]) ).

tff(f925,plain,
    div_mod(int,aa(int,int,plus_plus(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs))),aa(int,int,aa(int,fun(int,int),minus_minus(int),x),aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs)))),divisor(a)) != div_mod(int,aa(int,int,plus_plus(int,aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs))),aa(int,int,aa(int,fun(int,int),minus_minus(int),x),aa(int,int,aa(int,fun(int,int),minus_minus(int),li),aa(list(int),int,aa(list(int),fun(list(int),int),iprod(int),lks),xs)))),divisor(a)),
    inference(backward_demodulation,[],[f905,f924]) ).

tff(f926,plain,
    $false,
    inference(trivial_inequality_removal,[],[f925]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : COM113_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.07/0.16  % Computer : n004.cluster.edu
% 0.07/0.16  % Model    : x86_64 x86_64
% 0.07/0.16  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.16  % Memory   : 8046.5625MB
% 0.07/0.16  % OS       : Linux 6.8.0-71-generic
% 0.07/0.16  % CPULimit : 300
% 0.07/0.16  % WCLimit  : 300
% 0.07/0.16  % DateTime : Mon Sep 28 21:54:37 UTC 2026
% 0.07/0.16  % CPUTime  : 
% 0.07/0.16  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.20  Running first-order model finding
% 0.07/0.20  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
% 0.21/0.35  % (825404)Will run a generic schedule for satisfiability detection.
% 0.21/0.35  % (825413)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=468100359:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.21/0.35  % (825410)% WARNING: option uhcvi not known.
% 0.21/0.35  % (825410)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3299893573:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.21/0.35  % (825409)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3644703373_2999 on theBenchmark for (2999ds/0Mi)
% 0.21/0.35  % (825412)dis+10_1_sil=32000:sp=arity:random_seed=150957630:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.21/0.35  % (825411)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3148275867:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.21/0.35  % (825414)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2767407332:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.35  % Exception at run slice level
% 0.21/0.35  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.21/0.35  % (825415)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1363875422:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.21/0.35  % (825413)Instruction limit reached! 
% 0.21/0.35  % (825413)------------------------------
% 0.21/0.35  % (825413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35  % (825413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35  % (825413)CaDiCaL version: 2.1.3
% 0.21/0.35  % (825413)Termination reason: Instruction limit
% 0.21/0.35  % (825413)Termination phase: Saturation
% 0.21/0.35  % (825413)Time elapsed: 0.036 s
% 0.21/0.35  % (825413)Peak memory usage: 13 MB
% 0.21/0.35  % (825413)Instructions burned: 116 (million)
% 0.21/0.35  % (825423)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3814157288:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.21/0.35  % Exception at run slice level
% 0.21/0.35  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 0.21/0.35  % (825425)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1520390798:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 0.21/0.35  % (825412)Instruction limit reached! 
% 0.21/0.35  % (825412)------------------------------
% 0.21/0.35  % (825412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35  % (825412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35  % (825412)CaDiCaL version: 2.1.3
% 0.21/0.35  % (825412)Termination reason: Instruction limit
% 0.21/0.35  % (825412)Termination phase: Saturation
% 0.21/0.35  % (825412)Time elapsed: 0.053 s
% 0.21/0.35  % (825412)Peak memory usage: 12 MB
% 0.21/0.35  % (825412)Instructions burned: 103 (million)
% 0.21/0.35  % (825426)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=878233537:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 0.21/0.35  % (825425) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-825404-825425"...
% 0.21/0.35  % (825428)ott-21_1_sil=16000:fs=off:random_seed=18510957:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 0.21/0.35  % (825414)Instruction limit reached! 
% 0.21/0.35  % (825414)------------------------------
% 0.21/0.35  % (825414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35  % (825414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35  % (825414)CaDiCaL version: 2.1.3
% 0.21/0.35  % (825414)Termination reason: Instruction limit
% 0.21/0.35  % (825414)Termination phase: Saturation
% 0.21/0.35  % (825414)Time elapsed: 0.071 s
% 0.21/0.35  % (825414)Peak memory usage: 12 MB
% 0.21/0.35  % (825414)Instructions burned: 132 (million)
% 0.21/0.35  % (825425)...printing done.
% 0.21/0.35  % (825425)Refutation found. Thanks to Tanya!
% 0.21/0.35  % SZS status Theorem for theBenchmark
% 0.21/0.35  % SZS output start Proof for theBenchmark
% See solution above
% 0.21/0.35  % (825425)------------------------------
% 0.21/0.35  % (825425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.21/0.35  % (825425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/0.35  % (825425)CaDiCaL version: 2.1.3
% 0.21/0.35  % (825425)Termination reason: Refutation
% 0.21/0.35  % (825425)Time elapsed: 0.042 s
% 0.21/0.35  % (825425)Peak memory usage: 13 MB
% 0.21/0.35  % (825425)Instructions burned: 164 (million)
% 0.21/0.35  % (825404)Success in time 0.144 s
% 0.21/0.35  % Vampire exiting
%------------------------------------------------------------------------------