Leo-III---1.8.0.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : COM069_5 : TPTP v9.3.1. Released v6.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39

% Computer : n018.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 : Sun Sep 27 06:57:59 AM UTC 2026

% Result   : Theorem 153.65s 121.92s
% Output   : Refutation 154.15s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :    8
%            Number of leaves      :    3
% Syntax   : Number of formulae    :   15 (   9 unt;   0 typ;   0 def)
%            Number of atoms       : 8444 (  11 equ;   0 cnn)
%            Maximal formula atoms :    3 ( 562 avg)
%            Number of connectives : 20931 (  11   ~;   5   |;   0   &;20913   @)
%                                         (   0 <=>;   2  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    8 (   4 avg)
%            Number of types       :    4 (   3 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of symbols     :   40 (  38 usr;  12 con; 0-4 aty)
%            Number of variables   :   19 (   0   ^;  19   !;   0   ?;  19   :)

% Comments : 
%------------------------------------------------------------------------------
thf(bool_type,type,
    bool: $tType ).

thf(int_type,type,
    int: $tType ).

thf(atom_type,type,
    atom: $tType ).

thf(ring_div_decl,type,
    ring_div: 
      !>[TA: $tType] : $o ).

thf(big_linorder_Min_decl,type,
    big_linorder_Min: 
      !>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > TA ) ).

thf(combb_decl,type,
    combb: 
      !>[TA: $tType,TB: $tType,TC: $tType] : ( TB @ ( TA @ fun ) @ ( TC @ ( TA @ fun ) @ fun ) @ ( TB @ ( TC @ fun ) @ fun ) ) ).

thf(combc_decl,type,
    combc: 
      !>[TA: $tType,TB: $tType,TC: $tType] : ( TA @ ( TC @ fun ) @ ( TB @ fun ) @ ( TA @ ( TB @ fun ) @ ( TC @ fun ) @ fun ) ) ).

thf(combk_decl,type,
    combk: 
      !>[TA: $tType,TB: $tType] : ( TB @ ( TA @ fun ) @ ( TB @ fun ) ) ).

thf(combs_decl,type,
    combs: 
      !>[TA: $tType,TB: $tType,TC: $tType] : ( TA @ ( TC @ fun ) @ ( TB @ ( TC @ fun ) @ fun ) @ ( TA @ ( TB @ fun ) @ ( TC @ fun ) @ fun ) ) ).

thf(div_div_decl,type,
    div_div: 
      !>[TA: $tType] : ( TA > TA > TA ) ).

thf(div_mod_decl,type,
    div_mod: 
      !>[TA: $tType] : ( TA > TA > TA ) ).

thf(minus_minus_decl,type,
    minus_minus: 
      !>[TA: $tType] : ( TA @ ( TA @ fun ) @ ( TA @ fun ) ) ).

thf(one_one_decl,type,
    one_one: 
      !>[TA: $tType] : TA ).

thf(plus_plus_decl,type,
    plus_plus: 
      !>[TA: $tType] : ( TA > TA > TA ) ).

thf(times_times_decl,type,
    times_times: 
      !>[TA: $tType] : ( TA > ( TA @ ( TA @ fun ) ) ) ).

thf(zero_zero_decl,type,
    zero_zero: 
      !>[TA: $tType] : TA ).

thf(iprod_decl,type,
    iprod: 
      !>[TA: $tType] : ( TA @ ( TA @ list @ fun ) @ ( TA @ list @ fun ) ) ).

thf(filter_decl,type,
    filter: 
      !>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > ( TA @ list ) > ( TA @ list ) ) ).

thf(list_case_decl,type,
    list_case: 
      !>[TA: $tType,TB: $tType] : ( TB > ( TB @ ( TA @ list @ fun ) @ ( TA @ fun ) ) > ( TB @ ( TA @ list @ fun ) ) ) ).

thf(map_decl,type,
    map: 
      !>[TA: $tType,TB: $tType] : ( ( TA @ ( TB @ fun ) ) > ( TB @ list ) > ( TA @ list ) ) ).

thf(set_decl,type,
    set: 
      !>[TA: $tType] : ( ( TA @ list ) > ( bool @ ( TA @ fun ) ) ) ).

thf(tl_decl,type,
    tl: 
      !>[TA: $tType] : ( TA @ list @ ( TA @ list @ fun ) ) ).

thf(ord_less_decl,type,
    ord_less: 
      !>[TA: $tType] : ( bool @ ( TA @ fun ) @ ( TA @ fun ) ) ).

thf(c_PresArith_Oatom_OLe_decl,type,
    c_PresArith_Oatom_OLe: atom @ ( int @ list @ fun ) @ ( int @ fun ) ).

thf(atom_case_decl,type,
    atom_case: 
      !>[TA: $tType] : ( ( TA @ ( int @ list @ fun ) @ ( int @ fun ) ) > ( TA @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) ) > ( TA @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) ) > ( TA @ ( atom @ fun ) ) ) ).

thf(divisor_decl,type,
    divisor: int @ ( atom @ fun ) ).

thf(zlcms_decl,type,
    zlcms: ( int @ list ) > int ).

thf(collect_decl,type,
    collect: 
      !>[TA: $tType] : ( ( bool @ ( TA @ fun ) ) > ( bool @ ( TA @ fun ) ) ) ).

thf(aa_decl,type,
    aa: 
      !>[TA: $tType,TB: $tType] : ( ( TA @ ( TB @ fun ) ) > TB > TA ) ).

thf(fEx_decl,type,
    fEx: 
      !>[TA: $tType] : ( bool @ ( bool @ ( TA @ fun ) @ fun ) ) ).

thf(fFalse_decl,type,
    fFalse: bool ).

thf(fTrue_decl,type,
    fTrue: bool ).

thf(fconj_decl,type,
    fconj: bool @ ( bool @ fun ) @ ( bool @ fun ) ).

thf(fequal_decl,type,
    fequal: 
      !>[TA: $tType] : ( bool @ ( TA @ fun ) @ ( TA @ fun ) ) ).

thf(member_decl,type,
    member: 
      !>[TA: $tType] : ( bool @ ( bool @ ( TA @ fun ) @ fun ) @ ( TA @ fun ) ) ).

thf(a_decl,type,
    a: atom ).

thf(as_decl,type,
    as: atom @ list ).

thf(n_decl,type,
    n: int ).

thf(xs_decl,type,
    xs: int @ list ).

thf(134,axiom,
    int @ ring_div,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',arity_Int_Oint___Divides_Oring__div) ).

thf(534,plain,
    int @ ring_div,
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[134]) ).

thf(4,axiom,
    ! [TA: $tType] :
      ( ( TA @ ring_div )
     => ! [A: TA,B: TA,C: TA] :
          ( ( A @ ( B @ ( C @ ( TA @ minus_minus @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( TA @ div_mod ) ) )
          = ( A @ ( A @ ( B @ ( TA @ div_mod ) ) @ ( A @ ( C @ ( TA @ div_mod ) ) @ ( TA @ minus_minus @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( TA @ div_mod ) ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_mod__diff__eq) ).

thf(139,plain,
    ! [TA: $tType] :
      ( ( TA @ ring_div )
     => ! [A: TA,B: TA,C: TA] :
          ( ( A @ ( B @ ( C @ ( TA @ minus_minus @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( TA @ div_mod ) ) )
          = ( A @ ( A @ ( B @ ( TA @ div_mod ) ) @ ( A @ ( C @ ( TA @ div_mod ) ) @ ( TA @ minus_minus @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( TA @ div_mod ) ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).

thf(140,plain,
    ! [TA: $tType,C: TA,B: TA,A: TA] :
      ( ( ( A @ ( B @ ( C @ ( TA @ minus_minus @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( TA @ div_mod ) ) )
        = ( A @ ( A @ ( B @ ( TA @ div_mod ) ) @ ( A @ ( C @ ( TA @ div_mod ) ) @ ( TA @ minus_minus @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( TA @ div_mod ) ) ) )
      | ~ ( TA @ ring_div ) ),
    inference(cnf,[status(esa)],[139]) ).

thf(141,plain,
    ! [TA: $tType,C: TA,B: TA,A: TA] :
      ( ~ ( TA @ ring_div )
      | ( ( A @ ( A @ ( B @ ( TA @ div_mod ) ) @ ( A @ ( C @ ( TA @ div_mod ) ) @ ( TA @ minus_minus @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( TA @ div_mod ) ) )
        = ( A @ ( B @ ( C @ ( TA @ minus_minus @ ( TA @ ( TA @ fun ) @ ( TA @ aa ) ) ) @ ( TA @ ( TA @ aa ) ) ) @ ( TA @ div_mod ) ) ) ) ),
    inference(lifteq,[status(thm)],[140]) ).

thf(1,conjecture,
    ( ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) )
    = ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) @ ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( n @ ( int @ div_mod ) ) @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) ) ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).

thf(2,negated_conjecture,
    ( ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) )
   != ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) @ ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( n @ ( int @ div_mod ) ) @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) ) ),
    inference(neg_conjecture,[status(cth)],[1]) ).

thf(136,plain,
    ( ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) )
   != ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) @ ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( n @ ( int @ div_mod ) ) @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) ) ),
    inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).

thf(137,plain,
    ( ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) @ ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( n @ ( int @ div_mod ) ) @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) )
   != ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) ) ),
    inference(lifteq,[status(thm)],[136]) ).

thf(542,plain,
    ! [C: int,B: int,A: int] :
      ( ( ( A @ ( A @ ( B @ ( int @ div_mod ) ) @ ( A @ ( C @ ( int @ div_mod ) ) @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) )
       != ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) @ ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( n @ ( int @ div_mod ) ) @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) ) )
      | ( ( A @ ( B @ ( C @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) )
       != ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) ) )
      | ~ ( int @ ring_div ) ),
    inference(paramod_ordered,[status(thm)],[141,137]) ).

thf(543,plain,
    ( ( ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) )
     != ( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_mod ) ) ) )
    | ~ ( int @ ring_div ) ),
    inference(pattern_uni,[status(thm)],[542:[bind(A,$thf( a @ ( divisor @ ( int @ ( atom @ aa ) ) ) )),bind(B,$thf( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( int @ one_one @ ( as @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fTrue @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( atom @ filter ) ) @ ( divisor @ ( int @ ( atom @ map ) ) ) @ zlcms @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ list @ ( bool @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ zero_zero @ ( int @ ord_less @ ( bool @ ( int @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ list @ ( bool @ combk ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ aa ) ) ) @ ( fFalse @ ( int @ ( bool @ list_case ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ combk ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ atom_case ) ) ) @ ( as @ ( atom @ set ) @ ( atom @ member @ ( bool @ ( bool @ ( atom @ fun ) @ ( atom @ combc ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( fconj @ ( atom @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ combs ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( bool @ ( atom @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( atom @ collect ) @ ( c_PresArith_Oatom_OLe @ ( atom @ ( int @ list @ ( int @ combc ) ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( atom @ member @ ( int @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( atom @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( atom @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( atom @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( atom @ fun ) @ ( int @ combc ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ ( int @ list @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( atom @ fun ) @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( atom @ fun ) @ aa ) ) ) @ ( xs @ ( int @ tl @ ( int @ iprod @ ( int @ list @ ( int @ ( int @ list @ fun ) @ ( int @ list @ combb ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ list @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ ( int @ list @ combc ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ ( int @ list @ fun ) @ ( int @ list @ aa ) ) ) @ ( int @ minus_minus @ ( int @ list @ ( int @ ( int @ fun ) @ ( int @ combb ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ fun ) @ ( int @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fequal @ ( int @ ( bool @ ( int @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ combb ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ ( int @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( int @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( fconj @ ( int @ ( bool @ ( bool @ fun ) @ ( bool @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( bool @ fun ) @ aa ) ) ) @ ( int @ list @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( bool @ ( int @ combs ) ) @ ( int @ list @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( bool @ fun ) @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ combs ) ) @ ( int @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ combc ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ aa ) ) ) @ ( int @ fEx @ ( int @ list @ ( bool @ ( bool @ ( int @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ fun ) @ fun ) @ aa ) ) ) @ ( int @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ ( bool @ ( int @ fun ) @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ list @ fEx @ ( int @ ( bool @ ( bool @ ( int @ list @ fun ) @ combb ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ fun ) @ ( bool @ ( bool @ ( int @ list @ fun ) @ fun ) @ aa ) ) ) @ ( bool @ ( int @ fun ) @ ( bool @ ( int @ list @ fun ) @ ( int @ fun ) @ aa ) ) ) @ ( int @ collect ) @ ( int @ big_linorder_Min ) @ ( n @ ( int @ minus_minus @ ( int @ ( int @ fun ) @ ( int @ aa ) ) ) @ ( int @ ( int @ aa ) ) ) @ ( int @ div_div ) ) @ ( int @ plus_plus ) ) @ ( int @ times_times ) @ ( int @ ( int @ aa ) ) ) )),bind(C,$thf( n ))]]) ).

thf(576,plain,
    ~ ( int @ ring_div ),
    inference(simp,[status(thm)],[543]) ).

thf(838,plain,
    $false,
    inference(rewrite,[status(thm)],[534,576]) ).

thf(839,plain,
    $false,
    inference(simp,[status(thm)],[838]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : COM069_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.08  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.16/0.41  % Computer : n018.cluster.edu
% 0.16/0.41  % Model    : x86_64 x86_64
% 0.16/0.41  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41  % Memory   : 8046.5625MB
% 0.16/0.41  % OS       : Linux 6.8.0-71-generic
% 0.16/0.41  % CPULimit : 300
% 0.16/0.41  % WCLimit  : 300
% 0.16/0.41  % DateTime : Sat Sep 26 23:28:07 UTC 2026
% 0.16/0.41  % CPUTime  : 
% 0.16/0.41  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.89/0.97  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 1.95/1.37  % [INFO] 	 Parsing done (398ms). 
% 1.95/1.38  % [INFO] 	 Running in sequential loop mode. 
% 3.27/1.78  % [INFO] 	 eprover registered as external prover. 
% 3.27/1.79  % [INFO] 	 Scanning for conjecture ... 
% 4.27/2.08  % [INFO] 	 Found a conjecture (or negated_conjecture) and 133 axioms. Running axiom selection ... 
% 5.04/2.25  % [INFO] 	 Axiom selection finished. Selected 133 axioms (removed 0 axioms). 
% 5.74/2.43  % [INFO] 	 Problem is typed first-order (TPTP TFF). 
% 5.74/2.48  % [INFO] 	 Type checking passed. 
% 5.74/2.49  % [CONFIG] 	 Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>.  Searching for refutation ... 
% 9.46/3.46  % [INFO] 	 [Domain constraints] Detected constraint on bool 
% 9.46/3.46  % [INFO] 	 [Domain constraints] dom(bool) ⊆ {fTrue,fFalse} 
% 9.82/3.59  % [INFO] 	 [Domain constraints] Detected constraint on bool 
% 9.82/3.59  % [INFO] 	 [Domain constraints] dom(bool) ⊆ {fTrue,fFalse} 
% 153.65/121.91  % [INFO] 	 Killing All external provers ... 
% 153.65/121.92  % Time passed: 121355ms (effective reasoning time: 120526ms)
% 153.65/121.92  % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 153.65/121.92  % Axioms used in derivation (2): arity_Int_Oint___Divides_Oring__div, fact_72_mod__diff__eq
% 153.65/121.92  % No. of inferences in proof: 15
% 153.65/121.92  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 121355 ms resp. 120526 ms w/o parsing
% 154.15/122.11  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 154.15/122.12  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------