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

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

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

% Result   : Theorem 5.74s 1.14s
% Output   : Refutation 5.74s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :   11
%            Number of leaves      :    4
% Syntax   : Number of formulae    :   27 (   6 unt;   0 typ;   0 def)
%            Number of atoms       :   59 (   0 equ)
%            Maximal formula atoms :    4 (   2 avg)
%            Number of connectives :   62 (  30   ~;  25   |;   1   &)
%                                         (   3 <=>;   3  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   14 (   6 avg)
%            Maximal term depth    :   19 (   2 avg)
%            Number of types       :    9 (   8 usr)
%            Number of type conns  :    0 (   0   >;   0   *;   0   +;   0  <<)
%            Number of predicates  :    7 (   6 usr;   1 prp; 0-5 aty)
%            Number of functors    :   44 (  44 usr;   9 con; 0-10 aty)
%            Number of variables   :   79 (  79   !;   0   ?;  79   :)

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

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

tff(type_def_7,type,
    loc: $tType ).

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

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

tff(type_def_10,type,
    vname: $tType ).

tff(type_def_11,type,
    bool: $tType ).

tff(type_def_12,type,
    hoare_28830079triple: $tType > $tType ).

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

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

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

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

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

tff(func_def_3,type,
    ass: ( vname * fun(state,nat) ) > com1 ).

tff(func_def_4,type,
    cond: ( fun(state,bool) * com1 * com1 ) > com1 ).

tff(func_def_5,type,
    local: ( loc * fun(state,nat) * com1 ) > com1 ).

tff(func_def_6,type,
    skip: com1 ).

tff(func_def_7,type,
    semi: ( com1 * com1 ) > com1 ).

tff(func_def_8,type,
    while: ( fun(state,bool) * com1 ) > com1 ).

tff(func_def_9,type,
    com_case: 
      !>[X0: $tType] : ( ( X0 * fun(vname,fun(fun(state,nat),X0)) * fun(loc,fun(fun(state,nat),fun(com1,X0))) * fun(com1,fun(com1,X0)) * fun(fun(state,bool),fun(com1,fun(com1,X0))) * fun(fun(state,bool),fun(com1,X0)) * fun(pname,X0) * fun(vname,fun(pname,fun(fun(state,nat),X0))) * com1 ) > X0 ) ).

tff(func_def_10,type,
    com_rec: 
      !>[X0: $tType] : ( ( X0 * fun(vname,fun(fun(state,nat),X0)) * fun(loc,fun(fun(state,nat),fun(com1,fun(X0,X0)))) * fun(com1,fun(com1,fun(X0,fun(X0,X0)))) * fun(fun(state,bool),fun(com1,fun(com1,fun(X0,fun(X0,X0))))) * fun(fun(state,bool),fun(com1,fun(X0,X0))) * fun(pname,X0) * fun(vname,fun(pname,fun(fun(state,nat),X0))) * com1 ) > X0 ) ).

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

tff(func_def_12,type,
    hoare_1841697145triple: 
      !>[X0: $tType] : ( ( fun(X0,fun(state,bool)) * com1 * fun(X0,fun(state,bool)) ) > hoare_28830079triple(X0) ) ).

tff(func_def_13,type,
    hoare_376461865e_case: 
      !>[X0: $tType,X1: $tType] : ( ( fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),X1))) * hoare_28830079triple(X0) ) > X1 ) ).

tff(func_def_14,type,
    hoare_678420151le_rec: 
      !>[X0: $tType,X1: $tType] : ( ( fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),X1))) * hoare_28830079triple(X0) ) > X1 ) ).

tff(func_def_15,type,
    hoare_47506394e_size: 
      !>[X0: $tType] : ( ( fun(X0,nat) * hoare_28830079triple(X0) ) > nat ) ).

tff(func_def_16,type,
    suc: nat > nat ).

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

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

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

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

tff(func_def_21,type,
    evaln: fun(com1,fun(state,fun(nat,fun(state,bool)))) ).

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

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

tff(func_def_24,type,
    fFalse: bool ).

tff(func_def_25,type,
    fTrue: bool ).

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

tff(func_def_27,type,
    com: com1 ).

tff(func_def_28,type,
    fun1: fun(a,fun(state,bool)) ).

tff(func_def_29,type,
    fun2: fun(a,fun(state,bool)) ).

tff(func_def_30,type,
    n: nat ).

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

tff(func_def_32,type,
    sK1: 
      !>[X0: $tType] : ( hoare_28830079triple(X0) > com1 ) ).

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

tff(func_def_34,type,
    sK3: 
      !>[X0: $tType] : ( ( fun(X0,fun(state,bool)) * com1 * fun(X0,fun(state,bool)) * nat ) > X0 ) ).

tff(func_def_35,type,
    sK4: 
      !>[X0: $tType] : ( ( fun(X0,fun(state,bool)) * com1 * fun(X0,fun(state,bool)) * nat ) > state ) ).

tff(func_def_36,type,
    sK5: 
      !>[X0: $tType] : ( ( fun(X0,fun(state,bool)) * com1 * fun(X0,fun(state,bool)) * nat ) > state ) ).

tff(func_def_37,type,
    sK6: ( state * state * com1 * state * state * com1 ) > nat ).

tff(func_def_38,type,
    sK7: ( state * nat * state * com1 * com1 ) > state ).

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

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

tff(func_def_41,type,
    sK10: ( state * nat * state * com1 * fun(state,bool) ) > state ).

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

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

tff(pred_def_3,type,
    wt: com1 > $o ).

tff(pred_def_4,type,
    hoare_1442473487ek_and: 
      !>[X0: $tType] : ( ( fun(X0,fun(state,bool)) * fun(state,bool) * X0 * state ) > $o ) ).

tff(pred_def_5,type,
    hoare_1633586161_valid: 
      !>[X0: $tType] : ( ( nat * hoare_28830079triple(X0) ) > $o ) ).

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

tff(f3,axiom,
    ! [X0: $tType,X1: hoare_28830079triple(X0),X2: nat] :
      ( hoare_1633586161_valid(X0,X2,X1)
    <=> pp(hoare_376461865e_case(X0,bool,aa(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),bool))),aa(fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(com1,fun(fun(X0,fun(state,bool)),bool))),fun(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),bool)))),combb(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(com1,fun(fun(X0,fun(state,bool)),bool)),fun(X0,fun(state,bool))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(X0,fun(state,bool)),bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(com1,fun(fun(X0,fun(state,bool)),bool))),combb(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(X0,fun(state,bool)),bool),com1),aa(fun(fun(X0,bool),bool),fun(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(X0,fun(state,bool)),bool)),combb(fun(X0,bool),bool,fun(X0,fun(state,bool))),fAll(X0)))),aa(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),aa(fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),fun(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))))),combb(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(X0,fun(state,bool))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,bool)),com1),aa(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,bool))),combb(fun(X0,fun(state,bool)),fun(X0,bool),fun(X0,fun(state,bool))),aa(fun(fun(state,bool),bool),fun(fun(X0,fun(state,bool)),fun(X0,bool)),combb(fun(state,bool),bool,X0),fAll(state))))),aa(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),aa(fun(fun(X0,fun(state,bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),combc(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),aa(fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),aa(fun(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),fun(fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))))),combb(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(X0,fun(state,bool))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),com1)),aa(fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(X0,fun(state,bool))),combb(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),aa(fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),aa(fun(fun(X0,fun(fun(state,bool),fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),combb(fun(X0,fun(fun(state,bool),fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(X0,fun(state,bool))),combs(X0,fun(state,bool),fun(state,bool))),aa(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(bool,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(X0,fun(state,fun(bool,bool))),fun(X0,fun(fun(state,bool),fun(state,bool)))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(bool,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool))))),combb(fun(X0,fun(state,fun(bool,bool))),fun(X0,fun(fun(state,bool),fun(state,bool))),fun(X0,fun(state,bool))),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(X0,fun(state,fun(bool,bool))),fun(X0,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),X0),combs(state,bool,bool))),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),X0),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))))))),aa(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),com1),aa(fun(fun(X0,fun(state,fun(state,bool))),fun(X0,fun(state,bool))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),combb(fun(X0,fun(state,fun(state,bool))),fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),aa(fun(fun(state,fun(state,bool)),fun(state,bool)),fun(fun(X0,fun(state,fun(state,bool))),fun(X0,fun(state,bool))),combb(fun(state,fun(state,bool)),fun(state,bool),X0),aa(fun(fun(state,bool),bool),fun(fun(state,fun(state,bool)),fun(state,bool)),combb(fun(state,bool),bool,state),fAll(state))))),aa(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),aa(fun(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),fun(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))))),combb(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),com1),combb(fun(state,bool),fun(state,fun(state,bool)),X0)),aa(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),aa(fun(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool))))),combb(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool))),com1),combc(state,fun(state,bool),fun(state,bool))),aa(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),fun(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool))))),combb(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool))),com1),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),state),combs(state,bool,bool))),aa(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool)))),aa(fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),fun(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool))))),combb(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool))),com1),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),state),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))),aa(nat,fun(com1,fun(state,fun(state,bool))),aa(fun(com1,fun(nat,fun(state,fun(state,bool)))),fun(nat,fun(com1,fun(state,fun(state,bool)))),combc(com1,nat,fun(state,fun(state,bool))),aa(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool)))),aa(fun(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool))))),combb(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool))),com1),combc(state,nat,fun(state,bool))),evaln)),X2))))))))),X1)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_triple__valid__def) ).

tff(f6,axiom,
    ! [X0: state,X1: nat,X2: state,X3: com1] :
      ( pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X3),X2),X1),X0))
     => pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X3),X2),suc(X1)),X0)) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_evaln__Suc) ).

tff(f8,axiom,
    ! [X0: $tType,X1: fun(X0,fun(state,bool)),X2: com1,X3: fun(X0,fun(state,bool)),X4: nat] :
      ( hoare_1633586161_valid(X0,X4,hoare_1841697145triple(X0,X3,X2,X1))
    <=> ! [X5: X0,X6: state] :
          ( pp(aa(state,bool,aa(X0,fun(state,bool),X3,X5),X6))
         => ! [X7: state] :
              ( pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X2),X6),X4),X7))
             => pp(aa(state,bool,aa(X0,fun(state,bool),X1,X5),X7)) ) ) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_triple__valid__def2) ).

tff(f108,conjecture,
    ( ~ pp(hoare_376461865e_case(a,bool,aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool)))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool)),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),combb(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool),com1),aa(fun(fun(a,bool),bool),fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),combb(fun(a,bool),bool,fun(a,fun(state,bool))),fAll(a)))),aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool)),com1),aa(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),combb(fun(a,fun(state,bool)),fun(a,bool),fun(a,fun(state,bool))),aa(fun(fun(state,bool),bool),fun(fun(a,fun(state,bool)),fun(a,bool)),combb(fun(state,bool),bool,a),fAll(state))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combc(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),aa(fun(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))))),combb(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(a,fun(state,bool))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1)),aa(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(a,fun(state,bool))),combb(fun(a,fun(state,bool)),fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(a,fun(state,bool))),combs(a,fun(state,bool),fun(state,bool))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool))))),combb(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool))),fun(a,fun(state,bool))),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),a),combs(state,bool,bool))),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),a),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1),aa(fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),combb(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool)),fun(a,fun(state,bool))),aa(fun(fun(state,fun(state,bool)),fun(state,bool)),fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),combb(fun(state,fun(state,bool)),fun(state,bool),a),aa(fun(fun(state,bool),bool),fun(fun(state,fun(state,bool)),fun(state,bool)),combb(fun(state,bool),bool,state),fAll(state))))),aa(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),aa(fun(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))))),combb(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),com1),combb(fun(state,bool),fun(state,fun(state,bool)),a)),aa(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),aa(fun(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool))))),combb(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool))),com1),combc(state,fun(state,bool),fun(state,bool))),aa(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),fun(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool))))),combb(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool))),com1),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),state),combs(state,bool,bool))),aa(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool)))),aa(fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),fun(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool))))),combb(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool))),com1),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),state),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))),aa(nat,fun(com1,fun(state,fun(state,bool))),aa(fun(com1,fun(nat,fun(state,fun(state,bool)))),fun(nat,fun(com1,fun(state,fun(state,bool)))),combc(com1,nat,fun(state,fun(state,bool))),aa(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool)))),aa(fun(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool))))),combb(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool))),com1),combc(state,nat,fun(state,bool))),evaln)),suc(n)))))))))),hoare_1841697145triple(a,fun1,com,fun2)))
    | pp(hoare_376461865e_case(a,bool,aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool)))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool)),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),combb(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool),com1),aa(fun(fun(a,bool),bool),fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),combb(fun(a,bool),bool,fun(a,fun(state,bool))),fAll(a)))),aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool)),com1),aa(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),combb(fun(a,fun(state,bool)),fun(a,bool),fun(a,fun(state,bool))),aa(fun(fun(state,bool),bool),fun(fun(a,fun(state,bool)),fun(a,bool)),combb(fun(state,bool),bool,a),fAll(state))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combc(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),aa(fun(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))))),combb(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(a,fun(state,bool))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1)),aa(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(a,fun(state,bool))),combb(fun(a,fun(state,bool)),fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(a,fun(state,bool))),combs(a,fun(state,bool),fun(state,bool))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool))))),combb(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool))),fun(a,fun(state,bool))),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),a),combs(state,bool,bool))),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),a),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1),aa(fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),combb(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool)),fun(a,fun(state,bool))),aa(fun(fun(state,fun(state,bool)),fun(state,bool)),fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),combb(fun(state,fun(state,bool)),fun(state,bool),a),aa(fun(fun(state,bool),bool),fun(fun(state,fun(state,bool)),fun(state,bool)),combb(fun(state,bool),bool,state),fAll(state))))),aa(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),aa(fun(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))))),combb(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),com1),combb(fun(state,bool),fun(state,fun(state,bool)),a)),aa(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),aa(fun(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool))))),combb(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool))),com1),combc(state,fun(state,bool),fun(state,bool))),aa(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),fun(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool))))),combb(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool))),com1),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),state),combs(state,bool,bool))),aa(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool)))),aa(fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),fun(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool))))),combb(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool))),com1),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),state),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))),aa(nat,fun(com1,fun(state,fun(state,bool))),aa(fun(com1,fun(nat,fun(state,fun(state,bool)))),fun(nat,fun(com1,fun(state,fun(state,bool)))),combc(com1,nat,fun(state,fun(state,bool))),aa(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool)))),aa(fun(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool))))),combb(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool))),com1),combc(state,nat,fun(state,bool))),evaln)),n))))))))),hoare_1841697145triple(a,fun1,com,fun2))) ),
    file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).

tff(f109,negated_conjecture,
    ~ ( ~ pp(hoare_376461865e_case(a,bool,aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool)))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool)),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),combb(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool),com1),aa(fun(fun(a,bool),bool),fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),combb(fun(a,bool),bool,fun(a,fun(state,bool))),fAll(a)))),aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool)),com1),aa(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),combb(fun(a,fun(state,bool)),fun(a,bool),fun(a,fun(state,bool))),aa(fun(fun(state,bool),bool),fun(fun(a,fun(state,bool)),fun(a,bool)),combb(fun(state,bool),bool,a),fAll(state))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combc(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),aa(fun(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))))),combb(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(a,fun(state,bool))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1)),aa(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(a,fun(state,bool))),combb(fun(a,fun(state,bool)),fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(a,fun(state,bool))),combs(a,fun(state,bool),fun(state,bool))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool))))),combb(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool))),fun(a,fun(state,bool))),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),a),combs(state,bool,bool))),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),a),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1),aa(fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),combb(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool)),fun(a,fun(state,bool))),aa(fun(fun(state,fun(state,bool)),fun(state,bool)),fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),combb(fun(state,fun(state,bool)),fun(state,bool),a),aa(fun(fun(state,bool),bool),fun(fun(state,fun(state,bool)),fun(state,bool)),combb(fun(state,bool),bool,state),fAll(state))))),aa(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),aa(fun(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))))),combb(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),com1),combb(fun(state,bool),fun(state,fun(state,bool)),a)),aa(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),aa(fun(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool))))),combb(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool))),com1),combc(state,fun(state,bool),fun(state,bool))),aa(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),fun(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool))))),combb(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool))),com1),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),state),combs(state,bool,bool))),aa(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool)))),aa(fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),fun(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool))))),combb(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool))),com1),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),state),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))),aa(nat,fun(com1,fun(state,fun(state,bool))),aa(fun(com1,fun(nat,fun(state,fun(state,bool)))),fun(nat,fun(com1,fun(state,fun(state,bool)))),combc(com1,nat,fun(state,fun(state,bool))),aa(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool)))),aa(fun(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool))))),combb(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool))),com1),combc(state,nat,fun(state,bool))),evaln)),suc(n)))))))))),hoare_1841697145triple(a,fun1,com,fun2)))
      | pp(hoare_376461865e_case(a,bool,aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool)))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool)),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),combb(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool),com1),aa(fun(fun(a,bool),bool),fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),combb(fun(a,bool),bool,fun(a,fun(state,bool))),fAll(a)))),aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool)),com1),aa(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),combb(fun(a,fun(state,bool)),fun(a,bool),fun(a,fun(state,bool))),aa(fun(fun(state,bool),bool),fun(fun(a,fun(state,bool)),fun(a,bool)),combb(fun(state,bool),bool,a),fAll(state))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combc(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),aa(fun(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))))),combb(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(a,fun(state,bool))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1)),aa(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(a,fun(state,bool))),combb(fun(a,fun(state,bool)),fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(a,fun(state,bool))),combs(a,fun(state,bool),fun(state,bool))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool))))),combb(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool))),fun(a,fun(state,bool))),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),a),combs(state,bool,bool))),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),a),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1),aa(fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),combb(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool)),fun(a,fun(state,bool))),aa(fun(fun(state,fun(state,bool)),fun(state,bool)),fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),combb(fun(state,fun(state,bool)),fun(state,bool),a),aa(fun(fun(state,bool),bool),fun(fun(state,fun(state,bool)),fun(state,bool)),combb(fun(state,bool),bool,state),fAll(state))))),aa(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),aa(fun(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))))),combb(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),com1),combb(fun(state,bool),fun(state,fun(state,bool)),a)),aa(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),aa(fun(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool))))),combb(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool))),com1),combc(state,fun(state,bool),fun(state,bool))),aa(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),fun(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool))))),combb(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool))),com1),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),state),combs(state,bool,bool))),aa(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool)))),aa(fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),fun(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool))))),combb(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool))),com1),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),state),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))),aa(nat,fun(com1,fun(state,fun(state,bool))),aa(fun(com1,fun(nat,fun(state,fun(state,bool)))),fun(nat,fun(com1,fun(state,fun(state,bool)))),combc(com1,nat,fun(state,fun(state,bool))),aa(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool)))),aa(fun(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool))))),combb(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool))),com1),combc(state,nat,fun(state,bool))),evaln)),n))))))))),hoare_1841697145triple(a,fun1,com,fun2))) ),
    inference(negated_conjecture,[status(cth)],[f108]) ).

tff(f112,plain,
    ! [X0: state,X1: nat,X2: state,X3: com1] :
      ( pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X3),X2),suc(X1)),X0))
      | ~ pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X3),X2),X1),X0)) ),
    inference(ennf_transformation,[],[f6]) ).

tff(f114,plain,
    ! [X0: $tType,X1: fun(X0,fun(state,bool)),X2: com1,X3: fun(X0,fun(state,bool)),X4: nat] :
      ( hoare_1633586161_valid(X0,X4,hoare_1841697145triple(X0,X3,X2,X1))
    <=> ! [X5: X0,X6: state] :
          ( ! [X7: state] :
              ( pp(aa(state,bool,aa(X0,fun(state,bool),X1,X5),X7))
              | ~ pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X2),X6),X4),X7)) )
          | ~ pp(aa(state,bool,aa(X0,fun(state,bool),X3,X5),X6)) ) ),
    inference(ennf_transformation,[],[f8]) ).

tff(f147,plain,
    ( pp(hoare_376461865e_case(a,bool,aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool)))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool)),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),combb(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool),com1),aa(fun(fun(a,bool),bool),fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),combb(fun(a,bool),bool,fun(a,fun(state,bool))),fAll(a)))),aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool)),com1),aa(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),combb(fun(a,fun(state,bool)),fun(a,bool),fun(a,fun(state,bool))),aa(fun(fun(state,bool),bool),fun(fun(a,fun(state,bool)),fun(a,bool)),combb(fun(state,bool),bool,a),fAll(state))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combc(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),aa(fun(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))))),combb(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(a,fun(state,bool))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1)),aa(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(a,fun(state,bool))),combb(fun(a,fun(state,bool)),fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(a,fun(state,bool))),combs(a,fun(state,bool),fun(state,bool))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool))))),combb(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool))),fun(a,fun(state,bool))),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),a),combs(state,bool,bool))),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),a),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1),aa(fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),combb(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool)),fun(a,fun(state,bool))),aa(fun(fun(state,fun(state,bool)),fun(state,bool)),fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),combb(fun(state,fun(state,bool)),fun(state,bool),a),aa(fun(fun(state,bool),bool),fun(fun(state,fun(state,bool)),fun(state,bool)),combb(fun(state,bool),bool,state),fAll(state))))),aa(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),aa(fun(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))))),combb(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),com1),combb(fun(state,bool),fun(state,fun(state,bool)),a)),aa(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),aa(fun(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool))))),combb(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool))),com1),combc(state,fun(state,bool),fun(state,bool))),aa(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),fun(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool))))),combb(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool))),com1),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),state),combs(state,bool,bool))),aa(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool)))),aa(fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),fun(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool))))),combb(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool))),com1),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),state),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))),aa(nat,fun(com1,fun(state,fun(state,bool))),aa(fun(com1,fun(nat,fun(state,fun(state,bool)))),fun(nat,fun(com1,fun(state,fun(state,bool)))),combc(com1,nat,fun(state,fun(state,bool))),aa(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool)))),aa(fun(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool))))),combb(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool))),com1),combc(state,nat,fun(state,bool))),evaln)),suc(n)))))))))),hoare_1841697145triple(a,fun1,com,fun2)))
    & ~ pp(hoare_376461865e_case(a,bool,aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool)))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool)),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),combb(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool),com1),aa(fun(fun(a,bool),bool),fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),combb(fun(a,bool),bool,fun(a,fun(state,bool))),fAll(a)))),aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool)),com1),aa(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),combb(fun(a,fun(state,bool)),fun(a,bool),fun(a,fun(state,bool))),aa(fun(fun(state,bool),bool),fun(fun(a,fun(state,bool)),fun(a,bool)),combb(fun(state,bool),bool,a),fAll(state))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combc(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),aa(fun(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))))),combb(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(a,fun(state,bool))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1)),aa(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(a,fun(state,bool))),combb(fun(a,fun(state,bool)),fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(a,fun(state,bool))),combs(a,fun(state,bool),fun(state,bool))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool))))),combb(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool))),fun(a,fun(state,bool))),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),a),combs(state,bool,bool))),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),a),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1),aa(fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),combb(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool)),fun(a,fun(state,bool))),aa(fun(fun(state,fun(state,bool)),fun(state,bool)),fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),combb(fun(state,fun(state,bool)),fun(state,bool),a),aa(fun(fun(state,bool),bool),fun(fun(state,fun(state,bool)),fun(state,bool)),combb(fun(state,bool),bool,state),fAll(state))))),aa(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),aa(fun(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))))),combb(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),com1),combb(fun(state,bool),fun(state,fun(state,bool)),a)),aa(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),aa(fun(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool))))),combb(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool))),com1),combc(state,fun(state,bool),fun(state,bool))),aa(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),fun(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool))))),combb(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool))),com1),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),state),combs(state,bool,bool))),aa(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool)))),aa(fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),fun(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool))))),combb(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool))),com1),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),state),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))),aa(nat,fun(com1,fun(state,fun(state,bool))),aa(fun(com1,fun(nat,fun(state,fun(state,bool)))),fun(nat,fun(com1,fun(state,fun(state,bool)))),combc(com1,nat,fun(state,fun(state,bool))),aa(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool)))),aa(fun(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool))))),combb(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool))),com1),combc(state,nat,fun(state,bool))),evaln)),n))))))))),hoare_1841697145triple(a,fun1,com,fun2))) ),
    inference(ennf_transformation,[],[f109]) ).

tff(f153,plain,
    ! [X0: $tType,X2: nat,X1: hoare_28830079triple(X0)] :
      ( ~ pp(hoare_376461865e_case(X0,bool,aa(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),bool))),aa(fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(com1,fun(fun(X0,fun(state,bool)),bool))),fun(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),bool)))),combb(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(com1,fun(fun(X0,fun(state,bool)),bool)),fun(X0,fun(state,bool))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(X0,fun(state,bool)),bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(com1,fun(fun(X0,fun(state,bool)),bool))),combb(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(X0,fun(state,bool)),bool),com1),aa(fun(fun(X0,bool),bool),fun(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(X0,fun(state,bool)),bool)),combb(fun(X0,bool),bool,fun(X0,fun(state,bool))),fAll(X0)))),aa(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),aa(fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),fun(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))))),combb(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(X0,fun(state,bool))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,bool)),com1),aa(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,bool))),combb(fun(X0,fun(state,bool)),fun(X0,bool),fun(X0,fun(state,bool))),aa(fun(fun(state,bool),bool),fun(fun(X0,fun(state,bool)),fun(X0,bool)),combb(fun(state,bool),bool,X0),fAll(state))))),aa(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),aa(fun(fun(X0,fun(state,bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),combc(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),aa(fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),aa(fun(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),fun(fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))))),combb(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(X0,fun(state,bool))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),com1)),aa(fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(X0,fun(state,bool))),combb(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),aa(fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),aa(fun(fun(X0,fun(fun(state,bool),fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),combb(fun(X0,fun(fun(state,bool),fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(X0,fun(state,bool))),combs(X0,fun(state,bool),fun(state,bool))),aa(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(bool,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(X0,fun(state,fun(bool,bool))),fun(X0,fun(fun(state,bool),fun(state,bool)))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(bool,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool))))),combb(fun(X0,fun(state,fun(bool,bool))),fun(X0,fun(fun(state,bool),fun(state,bool))),fun(X0,fun(state,bool))),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(X0,fun(state,fun(bool,bool))),fun(X0,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),X0),combs(state,bool,bool))),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),X0),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))))))),aa(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),com1),aa(fun(fun(X0,fun(state,fun(state,bool))),fun(X0,fun(state,bool))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),combb(fun(X0,fun(state,fun(state,bool))),fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),aa(fun(fun(state,fun(state,bool)),fun(state,bool)),fun(fun(X0,fun(state,fun(state,bool))),fun(X0,fun(state,bool))),combb(fun(state,fun(state,bool)),fun(state,bool),X0),aa(fun(fun(state,bool),bool),fun(fun(state,fun(state,bool)),fun(state,bool)),combb(fun(state,bool),bool,state),fAll(state))))),aa(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),aa(fun(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),fun(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))))),combb(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),com1),combb(fun(state,bool),fun(state,fun(state,bool)),X0)),aa(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),aa(fun(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool))))),combb(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool))),com1),combc(state,fun(state,bool),fun(state,bool))),aa(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),fun(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool))))),combb(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool))),com1),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),state),combs(state,bool,bool))),aa(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool)))),aa(fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),fun(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool))))),combb(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool))),com1),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),state),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))),aa(nat,fun(com1,fun(state,fun(state,bool))),aa(fun(com1,fun(nat,fun(state,fun(state,bool)))),fun(nat,fun(com1,fun(state,fun(state,bool)))),combc(com1,nat,fun(state,fun(state,bool))),aa(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool)))),aa(fun(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool))))),combb(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool))),com1),combc(state,nat,fun(state,bool))),evaln)),X2))))))))),X1))
      | hoare_1633586161_valid(X0,X2,X1) ),
    inference(cnf_transformation,[],[f3]) ).

tff(f154,plain,
    ! [X0: $tType,X2: nat,X1: hoare_28830079triple(X0)] :
      ( pp(hoare_376461865e_case(X0,bool,aa(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),bool))),aa(fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(com1,fun(fun(X0,fun(state,bool)),bool))),fun(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),bool)))),combb(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(com1,fun(fun(X0,fun(state,bool)),bool)),fun(X0,fun(state,bool))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(X0,fun(state,bool)),bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(com1,fun(fun(X0,fun(state,bool)),bool))),combb(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(X0,fun(state,bool)),bool),com1),aa(fun(fun(X0,bool),bool),fun(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(X0,fun(state,bool)),bool)),combb(fun(X0,bool),bool,fun(X0,fun(state,bool))),fAll(X0)))),aa(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),aa(fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),fun(fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))))),combb(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(X0,fun(state,bool))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,bool))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,bool)))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,bool)),com1),aa(fun(fun(X0,fun(state,bool)),fun(X0,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,bool))),combb(fun(X0,fun(state,bool)),fun(X0,bool),fun(X0,fun(state,bool))),aa(fun(fun(state,bool),bool),fun(fun(X0,fun(state,bool)),fun(X0,bool)),combb(fun(state,bool),bool,X0),fAll(state))))),aa(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),aa(fun(fun(X0,fun(state,bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),combc(fun(X0,fun(state,bool)),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),aa(fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),aa(fun(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),fun(fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(X0,fun(state,bool)),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))))),combb(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(X0,fun(state,bool))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),com1)),aa(fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),fun(fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(X0,fun(state,bool))),combb(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),aa(fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),aa(fun(fun(X0,fun(fun(state,bool),fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),combb(fun(X0,fun(fun(state,bool),fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),fun(X0,fun(state,bool))),combs(X0,fun(state,bool),fun(state,bool))),aa(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(bool,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(X0,fun(state,fun(bool,bool))),fun(X0,fun(fun(state,bool),fun(state,bool)))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(bool,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(fun(state,bool),fun(state,bool))))),combb(fun(X0,fun(state,fun(bool,bool))),fun(X0,fun(fun(state,bool),fun(state,bool))),fun(X0,fun(state,bool))),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(X0,fun(state,fun(bool,bool))),fun(X0,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),X0),combs(state,bool,bool))),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),X0),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))))))),aa(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),aa(fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),fun(fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))))),combb(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),com1),aa(fun(fun(X0,fun(state,fun(state,bool))),fun(X0,fun(state,bool))),fun(fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,bool)))),combb(fun(X0,fun(state,fun(state,bool))),fun(X0,fun(state,bool)),fun(X0,fun(state,bool))),aa(fun(fun(state,fun(state,bool)),fun(state,bool)),fun(fun(X0,fun(state,fun(state,bool))),fun(X0,fun(state,bool))),combb(fun(state,fun(state,bool)),fun(state,bool),X0),aa(fun(fun(state,bool),bool),fun(fun(state,fun(state,bool)),fun(state,bool)),combb(fun(state,bool),bool,state),fAll(state))))),aa(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),aa(fun(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool))))),fun(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))))),combb(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(X0,fun(state,bool)),fun(X0,fun(state,fun(state,bool)))),com1),combb(fun(state,bool),fun(state,fun(state,bool)),X0)),aa(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),aa(fun(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool))))),combb(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool))),com1),combc(state,fun(state,bool),fun(state,bool))),aa(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),fun(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool))))),combb(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool))),com1),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),state),combs(state,bool,bool))),aa(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool)))),aa(fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),fun(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool))))),combb(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool))),com1),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),state),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))),aa(nat,fun(com1,fun(state,fun(state,bool))),aa(fun(com1,fun(nat,fun(state,fun(state,bool)))),fun(nat,fun(com1,fun(state,fun(state,bool)))),combc(com1,nat,fun(state,fun(state,bool))),aa(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool)))),aa(fun(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool))))),combb(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool))),com1),combc(state,nat,fun(state,bool))),evaln)),X2))))))))),X1))
      | ~ hoare_1633586161_valid(X0,X2,X1) ),
    inference(cnf_transformation,[],[f3]) ).

tff(f158,plain,
    ! [X2: state,X3: com1,X0: state,X1: nat] :
      ( pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X3),X2),suc(X1)),X0))
      | ~ pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X3),X2),X1),X0)) ),
    inference(cnf_transformation,[],[f112]) ).

tff(f160,plain,
    ! [X0: $tType,X2: com1,X3: fun(X0,fun(state,bool)),X1: fun(X0,fun(state,bool)),X4: nat] :
      ( pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X2),sK4(X0,X1,X2,X3,X4)),X4),sK5(X0,X1,X2,X3,X4)))
      | hoare_1633586161_valid(X0,X4,hoare_1841697145triple(X0,X3,X2,X1)) ),
    inference(cnf_transformation,[],[f114]) ).

tff(f161,plain,
    ! [X0: $tType,X2: com1,X3: fun(X0,fun(state,bool)),X1: fun(X0,fun(state,bool)),X4: nat] :
      ( ~ pp(aa(state,bool,aa(X0,fun(state,bool),X1,sK3(X0,X1,X2,X3,X4)),sK5(X0,X1,X2,X3,X4)))
      | hoare_1633586161_valid(X0,X4,hoare_1841697145triple(X0,X3,X2,X1)) ),
    inference(cnf_transformation,[],[f114]) ).

tff(f162,plain,
    ! [X0: $tType,X2: com1,X3: fun(X0,fun(state,bool)),X1: fun(X0,fun(state,bool)),X6: state,X7: state,X4: nat,X5: X0] :
      ( pp(aa(state,bool,aa(X0,fun(state,bool),X1,X5),X7))
      | ~ pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X2),X6),X4),X7))
      | ~ pp(aa(state,bool,aa(X0,fun(state,bool),X3,X5),X6))
      | ~ hoare_1633586161_valid(X0,X4,hoare_1841697145triple(X0,X3,X2,X1)) ),
    inference(cnf_transformation,[],[f114]) ).

tff(f163,plain,
    ! [X0: $tType,X2: com1,X3: fun(X0,fun(state,bool)),X1: fun(X0,fun(state,bool)),X4: nat] :
      ( pp(aa(state,bool,aa(X0,fun(state,bool),X3,sK3(X0,X1,X2,X3,X4)),sK4(X0,X1,X2,X3,X4)))
      | hoare_1633586161_valid(X0,X4,hoare_1841697145triple(X0,X3,X2,X1)) ),
    inference(cnf_transformation,[],[f114]) ).

tff(f283,plain,
    ~ pp(hoare_376461865e_case(a,bool,aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool)))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool)),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),combb(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool),com1),aa(fun(fun(a,bool),bool),fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),combb(fun(a,bool),bool,fun(a,fun(state,bool))),fAll(a)))),aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool)),com1),aa(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),combb(fun(a,fun(state,bool)),fun(a,bool),fun(a,fun(state,bool))),aa(fun(fun(state,bool),bool),fun(fun(a,fun(state,bool)),fun(a,bool)),combb(fun(state,bool),bool,a),fAll(state))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combc(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),aa(fun(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))))),combb(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(a,fun(state,bool))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1)),aa(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(a,fun(state,bool))),combb(fun(a,fun(state,bool)),fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(a,fun(state,bool))),combs(a,fun(state,bool),fun(state,bool))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool))))),combb(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool))),fun(a,fun(state,bool))),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),a),combs(state,bool,bool))),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),a),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1),aa(fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),combb(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool)),fun(a,fun(state,bool))),aa(fun(fun(state,fun(state,bool)),fun(state,bool)),fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),combb(fun(state,fun(state,bool)),fun(state,bool),a),aa(fun(fun(state,bool),bool),fun(fun(state,fun(state,bool)),fun(state,bool)),combb(fun(state,bool),bool,state),fAll(state))))),aa(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),aa(fun(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))))),combb(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),com1),combb(fun(state,bool),fun(state,fun(state,bool)),a)),aa(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),aa(fun(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool))))),combb(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool))),com1),combc(state,fun(state,bool),fun(state,bool))),aa(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),fun(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool))))),combb(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool))),com1),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),state),combs(state,bool,bool))),aa(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool)))),aa(fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),fun(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool))))),combb(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool))),com1),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),state),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))),aa(nat,fun(com1,fun(state,fun(state,bool))),aa(fun(com1,fun(nat,fun(state,fun(state,bool)))),fun(nat,fun(com1,fun(state,fun(state,bool)))),combc(com1,nat,fun(state,fun(state,bool))),aa(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool)))),aa(fun(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool))))),combb(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool))),com1),combc(state,nat,fun(state,bool))),evaln)),n))))))))),hoare_1841697145triple(a,fun1,com,fun2))),
    inference(cnf_transformation,[],[f147]) ).

tff(f284,plain,
    pp(hoare_376461865e_case(a,bool,aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),bool)))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool)),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(com1,fun(fun(a,fun(state,bool)),bool))),combb(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool),com1),aa(fun(fun(a,bool),bool),fun(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(a,fun(state,bool)),bool)),combb(fun(a,bool),bool,fun(a,fun(state,bool))),fAll(a)))),aa(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),aa(fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),fun(fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))))),combb(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool))),fun(a,fun(state,bool))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,bool)))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool)),com1),aa(fun(fun(a,fun(state,bool)),fun(a,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,bool))),combb(fun(a,fun(state,bool)),fun(a,bool),fun(a,fun(state,bool))),aa(fun(fun(state,bool),bool),fun(fun(a,fun(state,bool)),fun(a,bool)),combb(fun(state,bool),bool,a),fAll(state))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combc(fun(a,fun(state,bool)),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),aa(fun(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),fun(fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(a,fun(state,bool)),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))))),combb(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(a,fun(state,bool))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1)),aa(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),fun(fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(a,fun(state,bool))),combb(fun(a,fun(state,bool)),fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(a,fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),fun(a,fun(state,bool))),combs(a,fun(state,bool),fun(state,bool))),aa(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(fun(state,bool),fun(state,bool))))),combb(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool))),fun(a,fun(state,bool))),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(a,fun(state,fun(bool,bool))),fun(a,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),a),combs(state,bool,bool))),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),a),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))))))),aa(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),aa(fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),fun(fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))))),combb(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool))),com1),aa(fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),fun(fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),fun(fun(a,fun(state,bool)),fun(a,fun(state,bool)))),combb(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool)),fun(a,fun(state,bool))),aa(fun(fun(state,fun(state,bool)),fun(state,bool)),fun(fun(a,fun(state,fun(state,bool))),fun(a,fun(state,bool))),combb(fun(state,fun(state,bool)),fun(state,bool),a),aa(fun(fun(state,bool),bool),fun(fun(state,fun(state,bool)),fun(state,bool)),combb(fun(state,bool),bool,state),fAll(state))))),aa(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),aa(fun(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool))))),fun(fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),fun(com1,fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))))),combb(fun(fun(state,bool),fun(state,fun(state,bool))),fun(fun(a,fun(state,bool)),fun(a,fun(state,fun(state,bool)))),com1),combb(fun(state,bool),fun(state,fun(state,bool)),a)),aa(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool)))),aa(fun(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),fun(com1,fun(fun(state,bool),fun(state,fun(state,bool))))),combb(fun(state,fun(fun(state,bool),fun(state,bool))),fun(fun(state,bool),fun(state,fun(state,bool))),com1),combc(state,fun(state,bool),fun(state,bool))),aa(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool)))),aa(fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),fun(fun(com1,fun(state,fun(state,fun(bool,bool)))),fun(com1,fun(state,fun(fun(state,bool),fun(state,bool))))),combb(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool))),com1),aa(fun(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool))),fun(fun(state,fun(state,fun(bool,bool))),fun(state,fun(fun(state,bool),fun(state,bool)))),combb(fun(state,fun(bool,bool)),fun(fun(state,bool),fun(state,bool)),state),combs(state,bool,bool))),aa(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool)))),aa(fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),fun(fun(com1,fun(state,fun(state,bool))),fun(com1,fun(state,fun(state,fun(bool,bool))))),combb(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool))),com1),aa(fun(fun(state,bool),fun(state,fun(bool,bool))),fun(fun(state,fun(state,bool)),fun(state,fun(state,fun(bool,bool)))),combb(fun(state,bool),fun(state,fun(bool,bool)),state),aa(fun(bool,fun(bool,bool)),fun(fun(state,bool),fun(state,fun(bool,bool))),combb(bool,fun(bool,bool),state),fimplies))),aa(nat,fun(com1,fun(state,fun(state,bool))),aa(fun(com1,fun(nat,fun(state,fun(state,bool)))),fun(nat,fun(com1,fun(state,fun(state,bool)))),combc(com1,nat,fun(state,fun(state,bool))),aa(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool)))),aa(fun(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool)))),fun(fun(com1,fun(state,fun(nat,fun(state,bool)))),fun(com1,fun(nat,fun(state,fun(state,bool))))),combb(fun(state,fun(nat,fun(state,bool))),fun(nat,fun(state,fun(state,bool))),com1),combc(state,nat,fun(state,bool))),evaln)),suc(n)))))))))),hoare_1841697145triple(a,fun1,com,fun2))),
    inference(cnf_transformation,[],[f147]) ).

tff(f655,plain,
    ! [X3: $tType,X2: nat,X0: com1,X1: state,X8: fun(X3,fun(state,bool)),X6: fun(X3,fun(state,bool)),X7: nat,X4: fun(X3,fun(state,bool)),X5: com1] :
      ( hoare_1633586161_valid(X3,X7,hoare_1841697145triple(X3,X6,X5,X4))
      | ~ pp(aa(state,bool,aa(X3,fun(state,bool),X8,sK3(X3,X4,X5,X6,X7)),X1))
      | ~ hoare_1633586161_valid(X3,X2,hoare_1841697145triple(X3,X8,X0,X4))
      | ~ pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X0),X1),X2),sK5(X3,X4,X5,X6,X7))) ),
    inference(resolution,[],[f162,f161]) ).

tff(f862,plain,
    hoare_1633586161_valid(a,suc(n),hoare_1841697145triple(a,fun1,com,fun2)),
    inference(resolution,[],[f153,f284]) ).

tff(f864,plain,
    ~ hoare_1633586161_valid(a,n,hoare_1841697145triple(a,fun1,com,fun2)),
    inference(resolution,[],[f154,f283]) ).

tff(f5078,plain,
    ! [X2: nat,X3: com1,X0: fun(a,fun(state,bool)),X1: state] :
      ( ~ pp(aa(state,bool,aa(a,fun(state,bool),X0,sK3(a,fun2,com,fun1,n)),X1))
      | ~ hoare_1633586161_valid(a,X2,hoare_1841697145triple(a,X0,X3,fun2))
      | ~ pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X3),X1),X2),sK5(a,fun2,com,fun1,n))) ),
    inference(resolution,[],[f655,f864]) ).

tff(f5100,plain,
    ! [X2: nat,X3: fun(a,fun(state,bool)),X0: com1,X1: state] :
      ( ~ pp(aa(state,bool,aa(a,fun(state,bool),X3,sK3(a,fun2,com,fun1,n)),X1))
      | ~ hoare_1633586161_valid(a,suc(X2),hoare_1841697145triple(a,X3,X0,fun2))
      | ~ pp(aa(state,bool,aa(nat,fun(state,bool),aa(state,fun(nat,fun(state,bool)),aa(com1,fun(state,fun(nat,fun(state,bool))),evaln,X0),X1),X2),sK5(a,fun2,com,fun1,n))) ),
    inference(resolution,[],[f5078,f158]) ).

tff(f9476,plain,
    ! [X0: fun(a,fun(state,bool))] :
      ( ~ pp(aa(state,bool,aa(a,fun(state,bool),X0,sK3(a,fun2,com,fun1,n)),sK4(a,fun2,com,fun1,n)))
      | ~ hoare_1633586161_valid(a,suc(n),hoare_1841697145triple(a,X0,com,fun2))
      | hoare_1633586161_valid(a,n,hoare_1841697145triple(a,fun1,com,fun2)) ),
    inference(resolution,[],[f5100,f160]) ).

tff(f9524,plain,
    ! [X0: fun(a,fun(state,bool))] :
      ( ~ pp(aa(state,bool,aa(a,fun(state,bool),X0,sK3(a,fun2,com,fun1,n)),sK4(a,fun2,com,fun1,n)))
      | ~ hoare_1633586161_valid(a,suc(n),hoare_1841697145triple(a,X0,com,fun2)) ),
    inference(forward_subsumption_resolution,[],[f9476,f864]) ).

tff(f9572,plain,
    ( ~ hoare_1633586161_valid(a,suc(n),hoare_1841697145triple(a,fun1,com,fun2))
    | hoare_1633586161_valid(a,n,hoare_1841697145triple(a,fun1,com,fun2)) ),
    inference(resolution,[],[f9524,f163]) ).

tff(f9587,plain,
    hoare_1633586161_valid(a,n,hoare_1841697145triple(a,fun1,com,fun2)),
    inference(forward_subsumption_resolution,[],[f9572,f862]) ).

tff(f9588,plain,
    $false,
    inference(forward_subsumption_resolution,[],[f9587,f864]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWW507_5 : TPTP v9.3.1. Released v6.0.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19  % Computer : n009.cluster.edu
% 0.09/0.19  % Model    : x86_64 x86_64
% 0.09/0.19  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19  % Memory   : 8046.5625MB
% 0.09/0.19  % OS       : Linux 6.8.0-71-generic
% 0.09/0.19  % CPULimit : 300
% 0.09/0.19  % WCLimit  : 300
% 0.09/0.19  % DateTime : Mon Sep 28 14:15:31 UTC 2026
% 0.09/0.19  % CPUTime  : 
% 0.09/0.19  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22  Running first-order model finding
% 0.09/0.22  Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.74/1.14  % (3051808)Will run a generic schedule for satisfiability detection.
% 5.74/1.14  % (3051813)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3420692902_2999 on theBenchmark for (2999ds/0Mi)
% 5.74/1.14  % Exception at run slice level
% 5.74/1.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.74/1.14  % (3051814)% WARNING: option uhcvi not known.
% 5.74/1.14  % (3051818)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3372939403:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.74/1.14  % (3051814)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3771608048:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.74/1.14  % (3051815)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1502336339:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.74/1.14  % (3051816)dis+10_1_sil=32000:sp=arity:random_seed=2549430773:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.74/1.14  % (3051817)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1402524029:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.74/1.14  % (3051819)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1038231067:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.74/1.14  % (3051821)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4055102281:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.74/1.14  % Exception at run slice level
% 5.74/1.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.74/1.14  % (3051829)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3547837382:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.74/1.14  % (3051829)Instruction limit reached! 
% 5.74/1.14  % (3051829)------------------------------
% 5.74/1.14  % (3051829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051829)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051829)Termination reason: Instruction limit
% 5.74/1.14  % (3051829)Termination phase: Saturation
% 5.74/1.14  % (3051829)Time elapsed: 0.039 s
% 5.74/1.14  % (3051829)Peak memory usage: 14 MB
% 5.74/1.14  % (3051829)Instructions burned: 133 (million)
% 5.74/1.14  % (3051816)Instruction limit reached! 
% 5.74/1.14  % (3051816)------------------------------
% 5.74/1.14  % (3051816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051816)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051816)Termination reason: Instruction limit
% 5.74/1.14  % (3051816)Termination phase: Saturation
% 5.74/1.14  % (3051816)Time elapsed: 0.062 s
% 5.74/1.14  % (3051816)Peak memory usage: 12 MB
% 5.74/1.14  % (3051816)Instructions burned: 103 (million)
% 5.74/1.14  % (3051818)Instruction limit reached! 
% 5.74/1.14  % (3051818)------------------------------
% 5.74/1.14  % (3051818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051818)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051818)Termination reason: Instruction limit
% 5.74/1.14  % (3051818)Termination phase: Saturation
% 5.74/1.14  % (3051818)Time elapsed: 0.067 s
% 5.74/1.14  % (3051818)Peak memory usage: 11 MB
% 5.74/1.14  % (3051818)Instructions burned: 131 (million)
% 5.74/1.14  % (3051831)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3775040889:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.74/1.14  % (3051817)Instruction limit reached! 
% 5.74/1.14  % (3051817)------------------------------
% 5.74/1.14  % (3051817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051817)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051817)Termination reason: Instruction limit
% 5.74/1.14  % (3051817)Termination phase: Saturation
% 5.74/1.14  % (3051817)Time elapsed: 0.072 s
% 5.74/1.14  % (3051817)Peak memory usage: 13 MB
% 5.74/1.14  % (3051817)Instructions burned: 116 (million)
% 5.74/1.14  % (3051832)ott-21_1_sil=16000:fs=off:random_seed=130583011:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.74/1.14  % (3051833)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3673444053:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.74/1.14  % (3051819)Instruction limit reached! 
% 5.74/1.14  % (3051819)------------------------------
% 5.74/1.14  % (3051819)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051819)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051819)Termination reason: Instruction limit
% 5.74/1.14  % (3051819)Termination phase: Saturation
% 5.74/1.14  % (3051819)Time elapsed: 0.088 s
% 5.74/1.14  % (3051819)Peak memory usage: 13 MB
% 5.74/1.14  % (3051819)Instructions burned: 160 (million)
% 5.74/1.14  % (3051835)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=303871065:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 5.74/1.14  % Exception at run slice level
% 5.74/1.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.74/1.14  % (3051838)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3986279945:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 5.74/1.14  % (3051840)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1363180851:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 5.74/1.14  % Exception at run slice level
% 5.74/1.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.74/1.14  % (3051843)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=609304804:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 5.74/1.14  % (3051832)Instruction limit reached! 
% 5.74/1.14  % (3051832)------------------------------
% 5.74/1.14  % (3051832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051832)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051832)Termination reason: Instruction limit
% 5.74/1.14  % (3051832)Termination phase: Saturation
% 5.74/1.14  % (3051832)Time elapsed: 0.099 s
% 5.74/1.14  % (3051832)Peak memory usage: 13 MB
% 5.74/1.14  % (3051832)Instructions burned: 180 (million)
% 5.74/1.14  % (3051845)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=267220050:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 5.74/1.14  % (3051831)Instruction limit reached! 
% 5.74/1.14  % (3051831)------------------------------
% 5.74/1.14  % (3051831)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051831)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051831)Termination reason: Instruction limit
% 5.74/1.14  % (3051831)Termination phase: Saturation
% 5.74/1.14  % (3051831)Time elapsed: 0.202 s
% 5.74/1.14  % (3051831)Peak memory usage: 17 MB
% 5.74/1.14  % (3051831)Instructions burned: 685 (million)
% 5.74/1.14  % (3051847)fmb+10_1_sil=64000:random_seed=4265927885:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 5.74/1.14  % (3051847)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 5.74/1.14  % Exception at run slice level
% 5.74/1.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.74/1.14  % (3051849)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=86967080:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 5.74/1.14  % Exception at run slice level
% 5.74/1.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.74/1.14  % (3051851)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2781665697:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 5.74/1.14  % Exception at run slice level
% 5.74/1.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.74/1.14  % (3051853)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1476167351:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 5.74/1.14  % (3051833)Instruction limit reached! 
% 5.74/1.14  % (3051833)------------------------------
% 5.74/1.14  % (3051833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051833)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051833)Termination reason: Instruction limit
% 5.74/1.14  % (3051833)Termination phase: Saturation
% 5.74/1.14  % (3051833)Time elapsed: 0.295 s
% 5.74/1.14  % (3051833)Peak memory usage: 16 MB
% 5.74/1.14  % (3051833)Instructions burned: 478 (million)
% 5.74/1.14  % (3051855)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2122397293:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 5.74/1.14  % (3051855)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 5.74/1.14  % (3051843)Instruction limit reached! 
% 5.74/1.14  % (3051843)------------------------------
% 5.74/1.14  % (3051843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051843)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051843)Termination reason: Instruction limit
% 5.74/1.14  % (3051843)Termination phase: Saturation
% 5.74/1.14  % (3051843)Time elapsed: 0.361 s
% 5.74/1.14  % (3051843)Peak memory usage: 22 MB
% 5.74/1.14  % (3051843)Instructions burned: 693 (million)
% 5.74/1.14  % (3051857)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3330688427:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 5.74/1.14  % Exception at run slice level
% 5.74/1.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.74/1.14  % (3051859)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3292124953:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 5.74/1.14  % Exception at run slice level
% 5.74/1.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.74/1.14  % (3051861)ott-2_1_sil=16000:newcnf=on:random_seed=3500417265:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 5.74/1.14  % (3051845)Instruction limit reached! 
% 5.74/1.14  % (3051845)------------------------------
% 5.74/1.14  % (3051845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051845)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051845)Termination reason: Instruction limit
% 5.74/1.14  % (3051845)Termination phase: Saturation
% 5.74/1.14  % (3051845)Time elapsed: 0.507 s
% 5.74/1.14  % (3051845)Peak memory usage: 17 MB
% 5.74/1.14  % (3051845)Instructions burned: 879 (million)
% 5.74/1.14  % (3051863)ott+10_1_sil=32000:tgt=ground:random_seed=3735733888:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 5.74/1.14  % (3051838)Instruction limit reached! 
% 5.74/1.14  % (3051838)------------------------------
% 5.74/1.14  % (3051838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051838)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051838)Termination reason: Instruction limit
% 5.74/1.14  % (3051838)Termination phase: Saturation
% 5.74/1.14  % (3051838)Time elapsed: 0.638 s
% 5.74/1.14  % (3051838)Peak memory usage: 20 MB
% 5.74/1.14  % (3051838)Instructions burned: 1179 (million)
% 5.74/1.14  % (3051865)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=160877455:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 5.74/1.14  % Exception at run slice level
% 5.74/1.14  User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 5.74/1.14  % (3051867)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4217037648:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 5.74/1.14  % (3051853) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3051808-3051853"...
% 5.74/1.14  % (3051853)...printing done.
% 5.74/1.14  % (3051853)Refutation found. Thanks to Tanya!
% 5.74/1.14  % SZS status Theorem for theBenchmark
% 5.74/1.14  % SZS output start Proof for theBenchmark
% See solution above
% 5.74/1.14  % (3051853)------------------------------
% 5.74/1.14  % (3051853)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.74/1.14  % (3051853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.74/1.14  % (3051853)CaDiCaL version: 2.1.3
% 5.74/1.14  % (3051853)Termination reason: Refutation
% 5.74/1.14  % (3051853)Time elapsed: 0.510 s
% 5.74/1.14  % (3051853)Peak memory usage: 25 MB
% 5.74/1.14  % (3051853)Instructions burned: 1681 (million)
% 5.74/1.14  % (3051808)Success in time 0.909 s
% 5.74/1.14  % Vampire exiting
%------------------------------------------------------------------------------