%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : SWW470+5 : TPTP v8.1.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Wed Jul 20 23:22:11 EDT 2022
% Result : Timeout 300.04s 300.43s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SWW470+5 : TPTP v8.1.0. Released v5.3.0.
% 0.12/0.14 % Command : bliksem %s
% 0.14/0.35 % Computer : n028.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % DateTime : Sat Jun 4 14:14:41 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.89/1.37 *** allocated 10000 integers for termspace/termends
% 0.89/1.37 *** allocated 10000 integers for clauses
% 0.89/1.37 *** allocated 10000 integers for justifications
% 0.89/1.37 *** allocated 15000 integers for termspace/termends
% 0.89/1.37 Bliksem 1.12
% 0.89/1.37
% 0.89/1.37
% 0.89/1.37 Automatic Strategy Selection
% 0.89/1.37
% 0.89/1.37 *** allocated 22500 integers for termspace/termends
% 0.89/1.37 *** allocated 33750 integers for termspace/termends
% 0.89/1.37 *** allocated 50625 integers for termspace/termends
% 0.89/1.37
% 0.89/1.37 Clauses:
% 0.89/1.37
% 0.89/1.37 { ti( fun( fun( X, Y ), fun( fun( Z, X ), fun( Z, Y ) ) ), combb( X, Y, Z )
% 0.89/1.37 ) = combb( X, Y, Z ) }.
% 0.89/1.37 { ti( fun( fun( X, fun( Y, Z ) ), fun( Y, fun( X, Z ) ) ), combc( X, Y, Z )
% 0.89/1.37 ) = combc( X, Y, Z ) }.
% 0.89/1.37 { ti( fun( X, fun( Y, X ) ), combk( X, Y ) ) = combk( X, Y ) }.
% 0.89/1.37 { ti( fun( fun( X, fun( Y, Z ) ), fun( fun( X, Y ), fun( X, Z ) ) ), combs
% 0.89/1.37 ( X, Y, Z ) ) = combs( X, Y, Z ) }.
% 0.89/1.37 { ti( com, skip ) = skip }.
% 0.89/1.37 { ti( fun( com, fun( com, com ) ), semi ) = semi }.
% 0.89/1.37 { ti( fun( fun( X, bool ), bool ), finite_finite_1( X ) ) = finite_finite_1
% 0.89/1.37 ( X ) }.
% 0.89/1.37 { ti( fun( fun( X, fun( X, X ) ), fun( fun( X, bool ), X ) ), finite_fold1
% 0.89/1.37 ( X ) ) = finite_fold1( X ) }.
% 0.89/1.37 { ti( fun( fun( X, fun( X, X ) ), fun( fun( X, bool ), fun( X, bool ) ) ),
% 0.89/1.37 finite_fold1Set( X ) ) = finite_fold1Set( X ) }.
% 0.89/1.37 { ti( fun( fun( X, fun( Y, Y ) ), fun( Y, fun( fun( X, bool ), fun( Y, bool
% 0.89/1.37 ) ) ) ), finite_fold_graph( X, Y ) ) = finite_fold_graph( X, Y ) }.
% 0.89/1.37 { ti( fun( fun( X, fun( X, X ) ), fun( fun( fun( X, bool ), X ), bool ) ),
% 0.89/1.37 finite_folding_one( X ) ) = finite_folding_one( X ) }.
% 0.89/1.37 { ti( fun( fun( X, fun( X, X ) ), fun( fun( fun( X, bool ), X ), bool ) ),
% 0.89/1.37 finite2073411215e_idem( X ) ) = finite2073411215e_idem( X ) }.
% 0.89/1.37 { ti( fun( fun( X, bool ), X ), the( X ) ) = the( X ) }.
% 0.89/1.37 { ti( X, undefined( X ) ) = undefined( X ) }.
% 0.89/1.37 { ti( fun( fun( hoare_509422987triple( X ), bool ), fun( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool ) ), hoare_122391849derivs( X )
% 0.89/1.37 ) = hoare_122391849derivs( X ) }.
% 0.89/1.37 { ti( fun( fun( X, fun( state, bool ) ), fun( com, fun( fun( X, fun( state
% 0.89/1.37 , bool ) ), hoare_509422987triple( X ) ) ) ), hoare_1008221573triple( X )
% 0.89/1.37 ) = hoare_1008221573triple( X ) }.
% 0.89/1.37 { ti( fun( fun( fun( X, fun( state, bool ) ), fun( com, fun( fun( X, fun(
% 0.89/1.37 state, bool ) ), Y ) ) ), fun( hoare_509422987triple( X ), Y ) ),
% 0.89/1.37 hoare_885240885e_case( X, Y ) ) = hoare_885240885e_case( X, Y ) }.
% 0.89/1.37 { ti( fun( fun( fun( X, fun( state, bool ) ), fun( com, fun( fun( X, fun(
% 0.89/1.37 state, bool ) ), Y ) ) ), fun( hoare_509422987triple( X ), Y ) ),
% 0.89/1.37 hoare_728318379le_rec( X, Y ) ) = hoare_728318379le_rec( X, Y ) }.
% 0.89/1.37 { ! bot( X ), ti( X, bot_bot( X ) ) = bot_bot( X ) }.
% 0.89/1.37 { ti( fun( fun( X, bool ), fun( X, bool ) ), collect( X ) ) = collect( X )
% 0.89/1.37 }.
% 0.89/1.37 { ti( fun( X, fun( fun( X, bool ), fun( X, bool ) ) ), insert( X ) ) =
% 0.89/1.37 insert( X ) }.
% 0.89/1.37 { ti( fun( fun( X, bool ), X ), the_elem( X ) ) = the_elem( X ) }.
% 0.89/1.37 { ti( bool, fFalse ) = fFalse }.
% 0.89/1.37 { ti( fun( bool, bool ), fNot ) = fNot }.
% 0.89/1.37 { ti( bool, fTrue ) = fTrue }.
% 0.89/1.37 { ti( fun( bool, fun( bool, bool ) ), fconj ) = fconj }.
% 0.89/1.37 { ti( fun( bool, fun( bool, bool ) ), fdisj ) = fdisj }.
% 0.89/1.37 { ti( fun( X, fun( X, bool ) ), fequal( X ) ) = fequal( X ) }.
% 0.89/1.37 { ti( fun( bool, fun( bool, bool ) ), fimplies ) = fimplies }.
% 0.89/1.37 { hAPP( X, Y, ti( fun( X, Y ), Z ), T ) = hAPP( X, Y, Z, T ) }.
% 0.89/1.37 { hAPP( X, Y, Z, ti( X, T ) ) = hAPP( X, Y, Z, T ) }.
% 0.89/1.37 { ti( X, hAPP( Y, X, Z, T ) ) = hAPP( Y, X, Z, T ) }.
% 0.89/1.37 { ! hBOOL( ti( bool, X ) ), hBOOL( X ) }.
% 0.89/1.37 { ! hBOOL( X ), hBOOL( ti( bool, X ) ) }.
% 0.89/1.37 { ti( fun( X, fun( fun( X, bool ), bool ) ), member( X ) ) = member( X ) }
% 0.89/1.37 .
% 0.89/1.37 { ti( fun( hoare_509422987triple( x_a ), bool ), g ) = g }.
% 0.89/1.37 { ti( fun( x_a, fun( state, bool ) ), p ) = p }.
% 0.89/1.37 { ti( fun( state, bool ), b ) = b }.
% 0.89/1.37 { ti( com, c ) = c }.
% 0.89/1.37 { hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) }.
% 0.89/1.37 { ! hAPP( fun( X, fun( state, bool ) ), hoare_509422987triple( X ), hAPP(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ),
% 0.89/1.37 hAPP( fun( X, fun( state, bool ) ), fun( com, fun( fun( X, fun( state,
% 0.89/1.37 bool ) ), hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ), Y
% 0.89/1.37 ), Z ), T ) = hAPP( fun( X, fun( state, bool ) ), hoare_509422987triple
% 0.89/1.37 ( X ), hAPP( com, fun( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), U ), W ), V0 ), Y = U }.
% 0.89/1.37 { ! hAPP( fun( X, fun( state, bool ) ), hoare_509422987triple( X ), hAPP(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ),
% 0.89/1.37 hAPP( fun( X, fun( state, bool ) ), fun( com, fun( fun( X, fun( state,
% 0.89/1.37 bool ) ), hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ), Y
% 0.89/1.37 ), Z ), T ) = hAPP( fun( X, fun( state, bool ) ), hoare_509422987triple
% 0.89/1.37 ( X ), hAPP( com, fun( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), U ), W ), V0 ), alpha1( Z, T, W, V0 ) }.
% 0.89/1.37 { ! Y = U, ! alpha1( Z, T, W, V0 ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Y ), Z ), T ) = hAPP( fun( X, fun( state,
% 0.89/1.37 bool ) ), hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state
% 0.89/1.37 , bool ) ), hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool
% 0.89/1.37 ) ), fun( com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple
% 0.89/1.37 ( X ) ) ), hoare_1008221573triple( X ), U ), W ), V0 ) }.
% 0.89/1.37 { ! alpha1( X, Y, Z, T ), X = Z }.
% 0.89/1.37 { ! alpha1( X, Y, Z, T ), Y = T }.
% 0.89/1.37 { ! X = Z, ! Y = T, alpha1( X, Y, Z, T ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), Z ) ), ! hBOOL( hAPP(
% 0.89/1.37 fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), T ), Y ) ), hBOOL( hAPP(
% 0.89/1.37 fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), T ), Z ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), Z ), bot_bot( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ) ) ) ) ), ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), bool, hAPP( fun( hoare_509422987triple( X ), bool ), fun( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool ), hoare_122391849derivs( X ), Y
% 0.89/1.37 ), T ) ), hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool,
% 0.89/1.37 hAPP( fun( hoare_509422987triple( X ), bool ), fun( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool ), hoare_122391849derivs( X ), Y
% 0.89/1.37 ), hAPP( fun( hoare_509422987triple( X ), bool ), fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), hAPP( hoare_509422987triple( X ), fun
% 0.89/1.37 ( fun( hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ) ), insert( hoare_509422987triple( X ) ), Z ), T ) ) ) }.
% 0.89/1.37 { hBOOL( W ), hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool,
% 0.89/1.37 hAPP( fun( hoare_509422987triple( X ), bool ), fun( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool ), hoare_122391849derivs( X ), Y
% 0.89/1.37 ), hAPP( fun( hoare_509422987triple( X ), bool ), fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), hAPP( hoare_509422987triple( X ), fun
% 0.89/1.37 ( fun( hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ) ), insert( hoare_509422987triple( X ) ), hAPP( fun( X, fun(
% 0.89/1.37 state, bool ) ), hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun
% 0.89/1.37 ( state, bool ) ), hoare_509422987triple( X ) ), hAPP( fun( X, fun( state
% 0.89/1.37 , bool ) ), fun( com, fun( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ), hAPP( bool,
% 0.89/1.37 fun( X, fun( state, bool ) ), hAPP( fun( X, fun( bool, fun( state, bool )
% 0.89/1.37 ) ), fun( bool, fun( X, fun( state, bool ) ) ), combc( X, bool, fun(
% 0.89/1.37 state, bool ) ), hAPP( fun( X, fun( state, fun( bool, bool ) ) ), fun( X
% 0.89/1.37 , fun( bool, fun( state, bool ) ) ), hAPP( fun( fun( state, fun( bool,
% 0.89/1.37 bool ) ), fun( bool, fun( state, bool ) ) ), fun( fun( X, fun( state, fun
% 0.89/1.37 ( bool, bool ) ) ), fun( X, fun( bool, fun( state, bool ) ) ) ), combb(
% 0.89/1.37 fun( state, fun( bool, bool ) ), fun( bool, fun( state, bool ) ), X ),
% 0.89/1.37 combc( state, bool, bool ) ), hAPP( fun( X, fun( state, bool ) ), fun( X
% 0.89/1.37 , fun( state, fun( bool, bool ) ) ), hAPP( fun( fun( state, bool ), fun(
% 0.89/1.37 state, fun( bool, bool ) ) ), fun( fun( X, fun( state, bool ) ), fun( X,
% 0.89/1.37 fun( state, fun( bool, bool ) ) ) ), combb( fun( state, bool ), fun(
% 0.89/1.37 state, fun( bool, bool ) ), X ), hAPP( fun( bool, fun( bool, bool ) ),
% 0.89/1.37 fun( fun( state, bool ), fun( state, fun( bool, bool ) ) ), combb( bool,
% 0.89/1.37 fun( bool, bool ), state ), fconj ) ), Z ) ) ), W ) ), T ), U ) ),
% 0.89/1.37 bot_bot( fun( hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), T ), U ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), hBOOL( hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), hAPP( bool, fun( X, fun( state, bool ) ),
% 0.89/1.37 hAPP( fun( X, fun( bool, fun( state, bool ) ) ), fun( bool, fun( X, fun(
% 0.89/1.37 state, bool ) ) ), combc( X, bool, fun( state, bool ) ), hAPP( fun( X,
% 0.89/1.37 fun( state, fun( bool, bool ) ) ), fun( X, fun( bool, fun( state, bool )
% 0.89/1.37 ) ), hAPP( fun( fun( state, fun( bool, bool ) ), fun( bool, fun( state,
% 0.89/1.37 bool ) ) ), fun( fun( X, fun( state, fun( bool, bool ) ) ), fun( X, fun(
% 0.89/1.37 bool, fun( state, bool ) ) ) ), combb( fun( state, fun( bool, bool ) ),
% 0.89/1.37 fun( bool, fun( state, bool ) ), X ), combc( state, bool, bool ) ), hAPP
% 0.89/1.37 ( fun( X, fun( state, bool ) ), fun( X, fun( state, fun( bool, bool ) ) )
% 0.89/1.37 , hAPP( fun( fun( state, bool ), fun( state, fun( bool, bool ) ) ), fun(
% 0.89/1.37 fun( X, fun( state, bool ) ), fun( X, fun( state, fun( bool, bool ) ) ) )
% 0.89/1.37 , combb( fun( state, bool ), fun( state, fun( bool, bool ) ), X ), hAPP(
% 0.89/1.37 fun( bool, fun( bool, bool ) ), fun( fun( state, bool ), fun( state, fun
% 0.89/1.37 ( bool, bool ) ) ), combb( bool, fun( bool, bool ), state ), fconj ) ), Z
% 0.89/1.37 ) ) ), W ) ), T ), U ) ), bot_bot( fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ) ) ) ) ) }.
% 0.89/1.37 { hBOOL( hAPP( state, bool, hAPP( X, fun( state, bool ), U, skol1( X, Y, Z
% 0.89/1.37 , T, U ) ), skol33( X, Y, Z, T, U ) ) ), hBOOL( hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), U ), Z ), T ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), hAPP( fun( state, bool ), fun( X, fun( state
% 0.89/1.37 , bool ) ), combk( fun( state, bool ), X ), hAPP( state, fun( state, bool
% 0.89/1.37 ), hAPP( fun( state, fun( state, bool ) ), fun( state, fun( state, bool
% 0.89/1.37 ) ), combc( state, state, bool ), fequal( state ) ), skol33( X, Y, Z, T
% 0.89/1.37 , U ) ) ) ), Z ), hAPP( fun( state, bool ), fun( X, fun( state, bool ) )
% 0.89/1.37 , combk( fun( state, bool ), X ), hAPP( X, fun( state, bool ), T, skol1(
% 0.89/1.37 X, Y, Z, T, U ) ) ) ) ), bot_bot( fun( hoare_509422987triple( X ), bool )
% 0.89/1.37 ) ) ) ), hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool,
% 0.89/1.37 hAPP( fun( hoare_509422987triple( X ), bool ), fun( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool ), hoare_122391849derivs( X ), Y
% 0.89/1.37 ), hAPP( fun( hoare_509422987triple( X ), bool ), fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), hAPP( hoare_509422987triple( X ), fun
% 0.89/1.37 ( fun( hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ) ), insert( hoare_509422987triple( X ) ), hAPP( fun( X, fun(
% 0.89/1.37 state, bool ) ), hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun
% 0.89/1.37 ( state, bool ) ), hoare_509422987triple( X ) ), hAPP( fun( X, fun( state
% 0.89/1.37 , bool ) ), fun( com, fun( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ), U ), Z ), T
% 0.89/1.37 ) ), bot_bot( fun( hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), T ), U ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), hBOOL( hAPP( state, bool,
% 0.89/1.37 hAPP( X, fun( state, bool ), U, skol2( X, U, W ) ), skol34( X, U, W ) ) )
% 0.89/1.37 , hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), T ), W ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), T ), U ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), ! hBOOL( hAPP( state, bool,
% 0.89/1.37 hAPP( X, fun( state, bool ), W, skol2( X, U, W ) ), skol34( X, U, W ) ) )
% 0.89/1.37 , hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), T ), W ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), T ), U ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), hBOOL( hAPP( state, bool,
% 0.89/1.37 hAPP( X, fun( state, bool ), W, skol3( X, Z, W ) ), skol35( X, Z, W ) ) )
% 0.89/1.37 , hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), W ), T ), U ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), T ), U ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), ! hBOOL( hAPP( state, bool,
% 0.89/1.37 hAPP( X, fun( state, bool ), Z, skol3( X, Z, W ) ), skol35( X, Z, W ) ) )
% 0.89/1.37 , hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), W ), T ), U ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), T ), U ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), hBOOL( hAPP( state, bool,
% 0.89/1.37 hAPP( X, fun( state, bool ), V0, skol4( X, Z, U, W, V0 ) ), skol36( X, Z
% 0.89/1.37 , U, W, V0 ) ) ), hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ),
% 0.89/1.37 bool, hAPP( fun( hoare_509422987triple( X ), bool ), fun( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool ), hoare_122391849derivs( X ), Y
% 0.89/1.37 ), hAPP( fun( hoare_509422987triple( X ), bool ), fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), hAPP( hoare_509422987triple( X ), fun
% 0.89/1.37 ( fun( hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ) ), insert( hoare_509422987triple( X ) ), hAPP( fun( X, fun(
% 0.89/1.37 state, bool ) ), hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun
% 0.89/1.37 ( state, bool ) ), hoare_509422987triple( X ) ), hAPP( fun( X, fun( state
% 0.89/1.37 , bool ) ), fun( com, fun( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ), V0 ), T ), W
% 0.89/1.37 ) ), bot_bot( fun( hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), T ), U ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), ! hBOOL( hAPP( state, bool,
% 0.89/1.37 hAPP( X, fun( state, bool ), Z, V1 ), skol36( X, Z, U, W, V0 ) ) ), hBOOL
% 0.89/1.37 ( hAPP( state, bool, hAPP( X, fun( state, bool ), U, V1 ), skol46( X, Z,
% 0.89/1.37 U, W, V0 ) ) ), hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ),
% 0.89/1.37 bool, hAPP( fun( hoare_509422987triple( X ), bool ), fun( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool ), hoare_122391849derivs( X ), Y
% 0.89/1.37 ), hAPP( fun( hoare_509422987triple( X ), bool ), fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), hAPP( hoare_509422987triple( X ), fun
% 0.89/1.37 ( fun( hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ) ), insert( hoare_509422987triple( X ) ), hAPP( fun( X, fun(
% 0.89/1.37 state, bool ) ), hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun
% 0.89/1.37 ( state, bool ) ), hoare_509422987triple( X ) ), hAPP( fun( X, fun( state
% 0.89/1.37 , bool ) ), fun( com, fun( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ), V0 ), T ), W
% 0.89/1.37 ) ), bot_bot( fun( hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), T ), U ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), ! hBOOL( hAPP( state, bool,
% 0.89/1.37 hAPP( X, fun( state, bool ), W, skol4( X, Z, U, W, V0 ) ), skol46( X, Z,
% 0.89/1.37 U, W, V0 ) ) ), hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ),
% 0.89/1.37 bool, hAPP( fun( hoare_509422987triple( X ), bool ), fun( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool ), hoare_122391849derivs( X ), Y
% 0.89/1.37 ), hAPP( fun( hoare_509422987triple( X ), bool ), fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), hAPP( hoare_509422987triple( X ), fun
% 0.89/1.37 ( fun( hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ) ), insert( hoare_509422987triple( X ) ), hAPP( fun( X, fun(
% 0.89/1.37 state, bool ) ), hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun
% 0.89/1.37 ( state, bool ) ), hoare_509422987triple( X ) ), hAPP( fun( X, fun( state
% 0.89/1.37 , bool ) ), fun( com, fun( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ), V0 ), T ), W
% 0.89/1.37 ) ), bot_bot( fun( hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun(
% 0.89/1.37 fun( X, bool ), fun( X, bool ) ), insert( X ), Z ), T ) ) ), ti( X, Y ) =
% 0.89/1.37 ti( X, Z ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X,
% 0.89/1.37 bool ), bool ), member( X ), Y ), T ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Z ), T ) ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), bool ), member( X ), Z ), hAPP( fun( X, bool ), fun
% 0.89/1.37 ( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X )
% 0.89/1.37 , Y ), T ) ) ) }.
% 0.89/1.37 { ! ti( X, Z ) = ti( X, Y ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), bool ), member( X ), Z ), hAPP( fun( X, bool ), fun
% 0.89/1.37 ( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X )
% 0.89/1.37 , Y ), T ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), bot_bot( fun( X, bool ) ) ) ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), fun( X, bool ), collect( X ), hAPP( X, fun( X, bool
% 0.89/1.37 ), fequal( X ), Y ) ) = hAPP( fun( X, bool ), fun( X, bool ), hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Y ), bot_bot( fun( X
% 0.89/1.37 , bool ) ) ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), fun( X, bool ), collect( X ), hAPP( X, fun( X, bool
% 0.89/1.37 ), hAPP( fun( X, fun( X, bool ) ), fun( X, fun( X, bool ) ), combc( X, X
% 0.89/1.37 , bool ), fequal( X ) ), Y ) ) = hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Y ), bot_bot
% 0.89/1.37 ( fun( X, bool ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Y, Z ) ), hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 collect( X ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun(
% 0.89/1.37 bool, bool ) ), fun( fun( X, bool ), fun( X, bool ) ), combs( X, bool,
% 0.89/1.37 bool ), hAPP( fun( X, bool ), fun( X, fun( bool, bool ) ), hAPP( fun(
% 0.89/1.37 bool, fun( bool, bool ) ), fun( fun( X, bool ), fun( X, fun( bool, bool )
% 0.89/1.37 ) ), combb( bool, fun( bool, bool ), X ), fconj ), hAPP( X, fun( X, bool
% 0.89/1.37 ), fequal( X ), Z ) ) ), Y ) ) = hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Z ), bot_bot
% 0.89/1.37 ( fun( X, bool ) ) ) }.
% 0.89/1.37 { hBOOL( hAPP( X, bool, Y, Z ) ), hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 collect( X ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun(
% 0.89/1.37 bool, bool ) ), fun( fun( X, bool ), fun( X, bool ) ), combs( X, bool,
% 0.89/1.37 bool ), hAPP( fun( X, bool ), fun( X, fun( bool, bool ) ), hAPP( fun(
% 0.89/1.37 bool, fun( bool, bool ) ), fun( fun( X, bool ), fun( X, fun( bool, bool )
% 0.89/1.37 ) ), combb( bool, fun( bool, bool ), X ), fconj ), hAPP( X, fun( X, bool
% 0.89/1.37 ), fequal( X ), Z ) ) ), Y ) ) = bot_bot( fun( X, bool ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Y, Z ) ), hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 collect( X ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun(
% 0.89/1.37 bool, bool ) ), fun( fun( X, bool ), fun( X, bool ) ), combs( X, bool,
% 0.89/1.37 bool ), hAPP( fun( X, bool ), fun( X, fun( bool, bool ) ), hAPP( fun(
% 0.89/1.37 bool, fun( bool, bool ) ), fun( fun( X, bool ), fun( X, fun( bool, bool )
% 0.89/1.37 ) ), combb( bool, fun( bool, bool ), X ), fconj ), hAPP( X, fun( X, bool
% 0.89/1.37 ), hAPP( fun( X, fun( X, bool ) ), fun( X, fun( X, bool ) ), combc( X, X
% 0.89/1.37 , bool ), fequal( X ) ), Z ) ) ), Y ) ) = hAPP( fun( X, bool ), fun( X,
% 0.89/1.37 bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Z )
% 0.89/1.37 , bot_bot( fun( X, bool ) ) ) }.
% 0.89/1.37 { hBOOL( hAPP( X, bool, Y, Z ) ), hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 collect( X ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun(
% 0.89/1.37 bool, bool ) ), fun( fun( X, bool ), fun( X, bool ) ), combs( X, bool,
% 0.89/1.37 bool ), hAPP( fun( X, bool ), fun( X, fun( bool, bool ) ), hAPP( fun(
% 0.89/1.37 bool, fun( bool, bool ) ), fun( fun( X, bool ), fun( X, fun( bool, bool )
% 0.89/1.37 ) ), combb( bool, fun( bool, bool ), X ), fconj ), hAPP( X, fun( X, bool
% 0.89/1.37 ), hAPP( fun( X, fun( X, bool ) ), fun( X, fun( X, bool ) ), combc( X, X
% 0.89/1.37 , bool ), fequal( X ) ), Z ) ) ), Y ) ) = bot_bot( fun( X, bool ) ) }.
% 0.89/1.37 { hAPP( hoare_509422987triple( X ), Y, hAPP( fun( fun( X, fun( state, bool
% 0.89/1.37 ) ), fun( com, fun( fun( X, fun( state, bool ) ), Y ) ) ), fun(
% 0.89/1.37 hoare_509422987triple( X ), Y ), hoare_728318379le_rec( X, Y ), Z ), hAPP
% 0.89/1.37 ( fun( X, fun( state, bool ) ), hoare_509422987triple( X ), hAPP( com,
% 0.89/1.37 fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ), hAPP(
% 0.89/1.37 fun( X, fun( state, bool ) ), fun( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ), T ), U ),
% 0.89/1.37 W ) ) = hAPP( fun( X, fun( state, bool ) ), Y, hAPP( com, fun( fun( X,
% 0.89/1.37 fun( state, bool ) ), Y ), hAPP( fun( X, fun( state, bool ) ), fun( com,
% 0.89/1.37 fun( fun( X, fun( state, bool ) ), Y ) ), Z, T ), U ), W ) }.
% 0.89/1.37 { ! ti( fun( X, bool ), Y ) = bot_bot( fun( X, bool ) ), ! hBOOL( hAPP( fun
% 0.89/1.37 ( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ), member( X ), Z )
% 0.89/1.37 , Y ) ) }.
% 0.89/1.37 { ! hAPP( fun( X, bool ), fun( X, bool ), collect( X ), Y ) = bot_bot( fun
% 0.89/1.37 ( X, bool ) ), ! hBOOL( hAPP( X, bool, Y, Z ) ) }.
% 0.89/1.37 { hBOOL( hAPP( X, bool, Y, skol5( X, Y ) ) ), hAPP( fun( X, bool ), fun( X
% 0.89/1.37 , bool ), collect( X ), Y ) = bot_bot( fun( X, bool ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), bot_bot( fun( X, bool ) ) ) ) }.
% 0.89/1.37 { ! bot_bot( fun( X, bool ) ) = hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 collect( X ), Y ), ! hBOOL( hAPP( X, bool, Y, Z ) ) }.
% 0.89/1.37 { hBOOL( hAPP( X, bool, Y, skol6( X, Y ) ) ), bot_bot( fun( X, bool ) ) =
% 0.89/1.37 hAPP( fun( X, bool ), fun( X, bool ), collect( X ), Y ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Z ), Y ) ), ! ti( fun( X, bool ), Y ) = bot_bot( fun( X,
% 0.89/1.37 bool ) ) }.
% 0.89/1.37 { ti( fun( X, bool ), Y ) = bot_bot( fun( X, bool ) ), hBOOL( hAPP( fun( X
% 0.89/1.37 , bool ), bool, hAPP( X, fun( fun( X, bool ), bool ), member( X ), skol7
% 0.89/1.37 ( X, Y ) ), Y ) ) }.
% 0.89/1.37 { hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ),
% 0.89/1.37 member( X ), skol8( X, Y ) ), Y ) ), ti( fun( X, bool ), Y ) = bot_bot(
% 0.89/1.37 fun( X, bool ) ) }.
% 0.89/1.37 { ! ti( fun( X, bool ), Y ) = bot_bot( fun( X, bool ) ), ! hBOOL( hAPP( fun
% 0.89/1.37 ( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ), member( X ), Z )
% 0.89/1.37 , Y ) ) }.
% 0.89/1.37 { bot_bot( fun( X, bool ) ) = hAPP( fun( X, bool ), fun( X, bool ), collect
% 0.89/1.37 ( X ), hAPP( bool, fun( X, bool ), combk( bool, X ), fFalse ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), Z ) ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X
% 0.89/1.37 , fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Y ), Z ) = ti( fun
% 0.89/1.37 ( X, bool ), Z ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), Z ) ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), bool ), member( X ), Y ), hAPP( fun( X, bool ), fun
% 0.89/1.37 ( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X )
% 0.89/1.37 , T ), Z ) ) ) }.
% 0.89/1.37 { hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ),
% 0.89/1.37 member( X ), Y ), Z ) ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun
% 0.89/1.37 ( fun( X, bool ), bool ), member( X ), Y ), T ) ), ! hAPP( fun( X, bool )
% 0.89/1.37 , fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert
% 0.89/1.37 ( X ), Y ), Z ) = hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun
% 0.89/1.37 ( X, bool ), fun( X, bool ) ), insert( X ), Y ), T ), ti( fun( X, bool )
% 0.89/1.37 , Z ) = ti( fun( X, bool ), T ) }.
% 0.89/1.37 { hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ),
% 0.89/1.37 member( X ), Y ), Z ) ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun
% 0.89/1.37 ( fun( X, bool ), bool ), member( X ), Y ), T ) ), ! ti( fun( X, bool ),
% 0.89/1.37 Z ) = ti( fun( X, bool ), T ), hAPP( fun( X, bool ), fun( X, bool ), hAPP
% 0.89/1.37 ( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Y ), Z ) = hAPP
% 0.89/1.37 ( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X,
% 0.89/1.37 bool ) ), insert( X ), Y ), T ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Y ), Z ), T ) ), ti(
% 0.89/1.37 X, Y ) = ti( X, T ), hBOOL( hAPP( X, bool, Z, T ) ) }.
% 0.89/1.37 { ! ti( X, Y ) = ti( X, T ), hBOOL( hAPP( X, bool, hAPP( fun( X, bool ),
% 0.89/1.37 fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X
% 0.89/1.37 ), Y ), Z ), T ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Z, T ) ), hBOOL( hAPP( X, bool, hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ),
% 0.89/1.37 insert( X ), Y ), Z ), T ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun(
% 0.89/1.37 fun( X, bool ), fun( X, bool ) ), insert( X ), Z ), T ) ) ), ti( X, Y ) =
% 0.89/1.37 ti( X, Z ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X,
% 0.89/1.37 bool ), bool ), member( X ), Y ), T ) ) }.
% 0.89/1.37 { ! ti( X, Y ) = ti( X, Z ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), bool ), member( X ), Y ), hAPP( fun( X, bool ), fun
% 0.89/1.37 ( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X )
% 0.89/1.37 , Z ), T ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), T ) ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), bool ), member( X ), Y ), hAPP( fun( X, bool ), fun
% 0.89/1.37 ( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X )
% 0.89/1.37 , Z ), T ) ) ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun(
% 0.89/1.37 X, bool ) ), insert( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP
% 0.89/1.37 ( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Z ), T ) ) =
% 0.89/1.37 hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun(
% 0.89/1.37 X, bool ) ), insert( X ), Z ), hAPP( fun( X, bool ), fun( X, bool ), hAPP
% 0.89/1.37 ( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Y ), T ) ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun(
% 0.89/1.37 X, bool ) ), insert( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP
% 0.89/1.37 ( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Y ), Z ) ) =
% 0.89/1.37 hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun(
% 0.89/1.37 X, bool ) ), insert( X ), Y ), Z ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun(
% 0.89/1.37 X, bool ) ), insert( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 collect( X ), Z ) ) = hAPP( fun( X, bool ), fun( X, bool ), collect( X )
% 0.89/1.37 , hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun( bool, bool ) )
% 0.89/1.37 , fun( fun( X, bool ), fun( X, bool ) ), combs( X, bool, bool ), hAPP(
% 0.89/1.37 fun( X, bool ), fun( X, fun( bool, bool ) ), hAPP( fun( bool, fun( bool,
% 0.89/1.37 bool ) ), fun( fun( X, bool ), fun( X, fun( bool, bool ) ) ), combb( bool
% 0.89/1.37 , fun( bool, bool ), X ), fimplies ), hAPP( fun( X, bool ), fun( X, bool
% 0.89/1.37 ), hAPP( fun( bool, bool ), fun( fun( X, bool ), fun( X, bool ) ), combb
% 0.89/1.37 ( bool, bool, X ), fNot ), hAPP( X, fun( X, bool ), hAPP( fun( X, fun( X
% 0.89/1.37 , bool ) ), fun( X, fun( X, bool ) ), combc( X, X, bool ), fequal( X ) )
% 0.89/1.37 , Y ) ) ) ), Z ) ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun(
% 0.89/1.37 X, bool ) ), insert( X ), Y ), Z ) = hAPP( fun( X, bool ), fun( X, bool )
% 0.89/1.37 , collect( X ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun(
% 0.89/1.37 bool, bool ) ), fun( fun( X, bool ), fun( X, bool ) ), combs( X, bool,
% 0.89/1.37 bool ), hAPP( fun( X, bool ), fun( X, fun( bool, bool ) ), hAPP( fun(
% 0.89/1.37 bool, fun( bool, bool ) ), fun( fun( X, bool ), fun( X, fun( bool, bool )
% 0.89/1.37 ) ), combb( bool, fun( bool, bool ), X ), fdisj ), hAPP( X, fun( X, bool
% 0.89/1.37 ), hAPP( fun( X, fun( X, bool ) ), fun( X, fun( X, bool ) ), combc( X, X
% 0.89/1.37 , bool ), fequal( X ) ), Y ) ) ), hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 hAPP( fun( X, fun( fun( X, bool ), bool ) ), fun( fun( X, bool ), fun( X
% 0.89/1.37 , bool ) ), combc( X, fun( X, bool ), bool ), member( X ) ), Z ) ) ) }.
% 0.89/1.37 { hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ),
% 0.89/1.37 member( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun
% 0.89/1.37 ( X, bool ), fun( X, bool ) ), insert( X ), Y ), Z ) ) ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun(
% 0.89/1.37 X, bool ) ), insert( X ), Y ), Z ) = hAPP( fun( X, bool ), fun( X, bool )
% 0.89/1.37 , collect( X ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun(
% 0.89/1.37 bool, bool ) ), fun( fun( X, bool ), fun( X, bool ) ), combs( X, bool,
% 0.89/1.37 bool ), hAPP( fun( X, bool ), fun( X, fun( bool, bool ) ), hAPP( fun(
% 0.89/1.37 bool, fun( bool, bool ) ), fun( fun( X, bool ), fun( X, fun( bool, bool )
% 0.89/1.37 ) ), combb( bool, fun( bool, bool ), X ), fdisj ), hAPP( X, fun( X, bool
% 0.89/1.37 ), hAPP( fun( X, fun( X, bool ) ), fun( X, fun( X, bool ) ), combc( X, X
% 0.89/1.37 , bool ), fequal( X ) ), Y ) ) ), hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 hAPP( fun( X, fun( fun( X, bool ), bool ) ), fun( fun( X, bool ), fun( X
% 0.89/1.37 , bool ) ), combc( X, fun( X, bool ), bool ), member( X ) ), Z ) ) ) }.
% 0.89/1.37 { ! hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun
% 0.89/1.37 ( X, bool ) ), insert( X ), Y ), bot_bot( fun( X, bool ) ) ) = hAPP( fun
% 0.89/1.37 ( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool )
% 0.89/1.37 ), insert( X ), Z ), bot_bot( fun( X, bool ) ) ), ti( X, Y ) = ti( X, Z
% 0.89/1.37 ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun(
% 0.89/1.37 fun( X, bool ), fun( X, bool ) ), insert( X ), Z ), bot_bot( fun( X, bool
% 0.89/1.37 ) ) ) ) ), ti( X, Y ) = ti( X, Z ) }.
% 0.89/1.37 { ! hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun
% 0.89/1.37 ( X, bool ) ), insert( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Z ), bot_bot
% 0.89/1.37 ( fun( X, bool ) ) ) ) = hAPP( fun( X, bool ), fun( X, bool ), hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), fun( X, bool ) ), insert( X ), T ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ),
% 0.89/1.37 insert( X ), U ), bot_bot( fun( X, bool ) ) ) ), alpha2( X, Y, Z, T, U )
% 0.89/1.37 , alpha6( X, Y, Z, T, U ) }.
% 0.89/1.37 { ! alpha2( X, Y, Z, T, U ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X
% 0.89/1.37 , fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Y ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ),
% 0.89/1.37 insert( X ), Z ), bot_bot( fun( X, bool ) ) ) ) = hAPP( fun( X, bool ),
% 0.89/1.37 fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X
% 0.89/1.37 ), T ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool
% 0.89/1.37 ), fun( X, bool ) ), insert( X ), U ), bot_bot( fun( X, bool ) ) ) ) }.
% 0.89/1.37 { ! alpha6( X, Y, Z, T, U ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X
% 0.89/1.37 , fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Y ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ),
% 0.89/1.37 insert( X ), Z ), bot_bot( fun( X, bool ) ) ) ) = hAPP( fun( X, bool ),
% 0.89/1.37 fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X
% 0.89/1.37 ), T ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool
% 0.89/1.37 ), fun( X, bool ) ), insert( X ), U ), bot_bot( fun( X, bool ) ) ) ) }.
% 0.89/1.37 { ! alpha6( X, Y, Z, T, U ), ti( X, Y ) = ti( X, U ) }.
% 0.89/1.37 { ! alpha6( X, Y, Z, T, U ), ti( X, Z ) = ti( X, T ) }.
% 0.89/1.37 { ! ti( X, Y ) = ti( X, U ), ! ti( X, Z ) = ti( X, T ), alpha6( X, Y, Z, T
% 0.89/1.37 , U ) }.
% 0.89/1.37 { ! alpha2( X, Y, Z, T, U ), ti( X, Y ) = ti( X, T ) }.
% 0.89/1.37 { ! alpha2( X, Y, Z, T, U ), ti( X, Z ) = ti( X, U ) }.
% 0.89/1.37 { ! ti( X, Y ) = ti( X, T ), ! ti( X, Z ) = ti( X, U ), alpha2( X, Y, Z, T
% 0.89/1.37 , U ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun(
% 0.89/1.37 fun( X, bool ), fun( X, bool ) ), insert( X ), Z ), bot_bot( fun( X, bool
% 0.89/1.37 ) ) ) ) ), ti( X, Y ) = ti( X, Z ) }.
% 0.89/1.37 { ! ti( X, Y ) = ti( X, Z ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), bool ), member( X ), Y ), hAPP( fun( X, bool ), fun
% 0.89/1.37 ( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X )
% 0.89/1.37 , Z ), bot_bot( fun( X, bool ) ) ) ) ) }.
% 0.89/1.37 { ! hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun
% 0.89/1.37 ( X, bool ) ), insert( X ), Y ), Z ) = bot_bot( fun( X, bool ) ) }.
% 0.89/1.37 { ! bot_bot( fun( X, bool ) ) = hAPP( fun( X, bool ), fun( X, bool ), hAPP
% 0.89/1.37 ( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Y ), Z ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), X, the_elem( X ), hAPP( fun( X, bool ), fun( X,
% 0.89/1.37 bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Y )
% 0.89/1.37 , bot_bot( fun( X, bool ) ) ) ) = ti( X, Y ) }.
% 0.89/1.37 { hAPP( hoare_509422987triple( X ), Y, hAPP( fun( fun( X, fun( state, bool
% 0.89/1.37 ) ), fun( com, fun( fun( X, fun( state, bool ) ), Y ) ) ), fun(
% 0.89/1.37 hoare_509422987triple( X ), Y ), hoare_885240885e_case( X, Y ), Z ), hAPP
% 0.89/1.37 ( fun( X, fun( state, bool ) ), hoare_509422987triple( X ), hAPP( com,
% 0.89/1.37 fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ), hAPP(
% 0.89/1.37 fun( X, fun( state, bool ) ), fun( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ), T ), U ),
% 0.89/1.37 W ) ) = hAPP( fun( X, fun( state, bool ) ), Y, hAPP( com, fun( fun( X,
% 0.89/1.37 fun( state, bool ) ), Y ), hAPP( fun( X, fun( state, bool ) ), fun( com,
% 0.89/1.37 fun( fun( X, fun( state, bool ) ), Y ) ), Z, T ), U ), W ) }.
% 0.89/1.37 { ! bot( X ), hAPP( Y, X, bot_bot( fun( Y, X ) ), Z ) = bot_bot( X ) }.
% 0.89/1.37 { ! bot( X ), hAPP( Y, X, bot_bot( fun( Y, X ) ), Z ) = bot_bot( X ) }.
% 0.89/1.37 { hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), skip ), Z ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), T ), U ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), ! hBOOL( hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), U ), W ), V0 ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), hBOOL( hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Y ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), Z ), hAPP( com, com, hAPP( com, fun( com,
% 0.89/1.37 com ), semi, T ), W ) ), V0 ) ), bot_bot( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ) ) ) ) ) }.
% 0.89/1.37 { Y = hAPP( fun( X, fun( state, bool ) ), hoare_509422987triple( X ), hAPP
% 0.89/1.37 ( com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ),
% 0.89/1.37 hAPP( fun( X, fun( state, bool ) ), fun( com, fun( fun( X, fun( state,
% 0.89/1.37 bool ) ), hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ),
% 0.89/1.37 skol9( X, Y ) ), skol37( X, Y ) ), skol47( X, Y ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), Z ) ), ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), bool ), member( X ), Y ), skol10( X, Y, T ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), Z ) ), ti( fun( X, bool ), Z ) = hAPP( fun( X, bool )
% 0.89/1.37 , fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert
% 0.89/1.37 ( X ), Y ), skol10( X, Y, Z ) ) }.
% 0.89/1.37 { ! hAPP( com, com, hAPP( com, fun( com, com ), semi, X ), Y ) = skip }.
% 0.89/1.37 { ! skip = hAPP( com, com, hAPP( com, fun( com, com ), semi, X ), Y ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), X, the_elem( X ), Y ) = hAPP( fun( X, bool ), X,
% 0.89/1.37 the( X ), hAPP( fun( X, fun( X, bool ) ), fun( X, bool ), hAPP( fun( fun
% 0.89/1.37 ( X, bool ), bool ), fun( fun( X, fun( X, bool ) ), fun( X, bool ) ),
% 0.89/1.37 combb( fun( X, bool ), bool, X ), hAPP( fun( X, bool ), fun( fun( X, bool
% 0.89/1.37 ), bool ), fequal( fun( X, bool ) ), Y ) ), hAPP( fun( X, bool ), fun( X
% 0.89/1.37 , fun( X, bool ) ), hAPP( fun( X, fun( fun( X, bool ), fun( X, bool ) ) )
% 0.89/1.37 , fun( fun( X, bool ), fun( X, fun( X, bool ) ) ), combc( X, fun( X, bool
% 0.89/1.37 ), fun( X, bool ) ), insert( X ) ), bot_bot( fun( X, bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), Z ) ), ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), bool ), member( X ), Y ), skol11( X, Y, T ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), Z ) ), ti( fun( X, bool ), Z ) = hAPP( fun( X, bool )
% 0.89/1.37 , fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert
% 0.89/1.37 ( X ), Y ), skol11( X, Y, Z ) ) }.
% 0.89/1.37 { ! hAPP( com, com, hAPP( com, fun( com, com ), semi, X ), Y ) = hAPP( com
% 0.89/1.37 , com, hAPP( com, fun( com, com ), semi, Z ), T ), X = Z }.
% 0.89/1.37 { ! hAPP( com, com, hAPP( com, fun( com, com ), semi, X ), Y ) = hAPP( com
% 0.89/1.37 , com, hAPP( com, fun( com, com ), semi, Z ), T ), Y = T }.
% 0.89/1.37 { ! X = Z, ! Y = T, hAPP( com, com, hAPP( com, fun( com, com ), semi, X ),
% 0.89/1.37 Y ) = hAPP( com, com, hAPP( com, fun( com, com ), semi, Z ), T ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), X, the( X ), hAPP( X, fun( X, bool ), fequal( X ),
% 0.89/1.37 Y ) ) = ti( X, Y ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), X, the( X ), hAPP( X, fun( X, bool ), hAPP( fun( X
% 0.89/1.37 , fun( X, bool ) ), fun( X, fun( X, bool ) ), combc( X, X, bool ), fequal
% 0.89/1.37 ( X ) ), Y ) ) = ti( X, Y ) }.
% 0.89/1.37 { ! hBOOL( T ), ti( X, Y ) = hAPP( fun( X, bool ), X, the( X ), hAPP( fun(
% 0.89/1.37 X, bool ), fun( X, bool ), hAPP( fun( X, fun( bool, bool ) ), fun( fun( X
% 0.89/1.37 , bool ), fun( X, bool ) ), combs( X, bool, bool ), hAPP( fun( X, bool )
% 0.89/1.37 , fun( X, fun( bool, bool ) ), hAPP( fun( bool, fun( bool, bool ) ), fun
% 0.89/1.37 ( fun( X, bool ), fun( X, fun( bool, bool ) ) ), combb( bool, fun( bool,
% 0.89/1.37 bool ), X ), fconj ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun(
% 0.89/1.37 bool, bool ), fun( fun( X, bool ), fun( X, bool ) ), combb( bool, bool, X
% 0.89/1.37 ), hAPP( bool, fun( bool, bool ), fimplies, T ) ), hAPP( X, fun( X, bool
% 0.89/1.37 ), hAPP( fun( X, fun( X, bool ) ), fun( X, fun( X, bool ) ), combc( X, X
% 0.89/1.37 , bool ), fequal( X ) ), Y ) ) ) ), hAPP( fun( X, bool ), fun( X, bool )
% 0.89/1.37 , hAPP( fun( bool, bool ), fun( fun( X, bool ), fun( X, bool ) ), combb(
% 0.89/1.37 bool, bool, X ), hAPP( bool, fun( bool, bool ), fimplies, hAPP( bool,
% 0.89/1.37 bool, fNot, T ) ) ), hAPP( X, fun( X, bool ), hAPP( fun( X, fun( X, bool
% 0.89/1.37 ) ), fun( X, fun( X, bool ) ), combc( X, X, bool ), fequal( X ) ), Z ) )
% 0.89/1.37 ) ) }.
% 0.89/1.37 { hBOOL( T ), ti( X, Z ) = hAPP( fun( X, bool ), X, the( X ), hAPP( fun( X
% 0.89/1.37 , bool ), fun( X, bool ), hAPP( fun( X, fun( bool, bool ) ), fun( fun( X
% 0.89/1.37 , bool ), fun( X, bool ) ), combs( X, bool, bool ), hAPP( fun( X, bool )
% 0.89/1.37 , fun( X, fun( bool, bool ) ), hAPP( fun( bool, fun( bool, bool ) ), fun
% 0.89/1.37 ( fun( X, bool ), fun( X, fun( bool, bool ) ) ), combb( bool, fun( bool,
% 0.89/1.37 bool ), X ), fconj ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun(
% 0.89/1.37 bool, bool ), fun( fun( X, bool ), fun( X, bool ) ), combb( bool, bool, X
% 0.89/1.37 ), hAPP( bool, fun( bool, bool ), fimplies, T ) ), hAPP( X, fun( X, bool
% 0.89/1.37 ), hAPP( fun( X, fun( X, bool ) ), fun( X, fun( X, bool ) ), combc( X, X
% 0.89/1.37 , bool ), fequal( X ) ), Y ) ) ) ), hAPP( fun( X, bool ), fun( X, bool )
% 0.89/1.37 , hAPP( fun( bool, bool ), fun( fun( X, bool ), fun( X, bool ) ), combb(
% 0.89/1.37 bool, bool, X ), hAPP( bool, fun( bool, bool ), fimplies, hAPP( bool,
% 0.89/1.37 bool, fNot, T ) ) ), hAPP( X, fun( X, bool ), hAPP( fun( X, fun( X, bool
% 0.89/1.37 ) ), fun( X, fun( X, bool ) ), combc( X, X, bool ), fequal( X ) ), Z ) )
% 0.89/1.37 ) ) }.
% 0.89/1.37 { hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ),
% 0.89/1.37 member( X ), skol12( X, Y ) ), Y ) ), ti( fun( X, bool ), Y ) = bot_bot(
% 0.89/1.37 fun( X, bool ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Y, Z ) ), hBOOL( hAPP( X, bool, Y, skol13( X, Y,
% 0.89/1.37 T ) ) ), hAPP( fun( X, bool ), X, the( X ), Y ) = ti( X, Z ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Y, Z ) ), ! ti( X, skol13( X, Y, Z ) ) = ti( X, Z
% 0.89/1.37 ), hAPP( fun( X, bool ), X, the( X ), Y ) = ti( X, Z ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Y, Z ) ), hBOOL( hAPP( X, bool, Y, skol14( X, Y,
% 0.89/1.37 T ) ) ), hBOOL( hAPP( X, bool, Y, hAPP( fun( X, bool ), X, the( X ), Y )
% 0.89/1.37 ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Y, Z ) ), ! ti( X, skol14( X, Y, Z ) ) = ti( X, Z
% 0.89/1.37 ), hBOOL( hAPP( X, bool, Y, hAPP( fun( X, bool ), X, the( X ), Y ) ) ) }
% 0.89/1.37 .
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Y, Z ) ), hBOOL( hAPP( X, bool, Y, skol15( X, Y,
% 0.89/1.37 T ) ) ), ! hBOOL( hAPP( X, bool, Y, U ) ), hAPP( fun( X, bool ), X, the(
% 0.89/1.37 X ), Y ) = ti( X, U ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Y, Z ) ), ! ti( X, skol15( X, Y, Z ) ) = ti( X, Z
% 0.89/1.37 ), ! hBOOL( hAPP( X, bool, Y, T ) ), hAPP( fun( X, bool ), X, the( X ),
% 0.89/1.37 Y ) = ti( X, T ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Y, Z ) ), hBOOL( hAPP( X, bool, Y, skol16( X, Y,
% 0.89/1.37 T ) ) ), hBOOL( hAPP( X, bool, Y, hAPP( fun( X, bool ), X, the( X ), Y )
% 0.89/1.37 ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Y, Z ) ), ! ti( X, skol16( X, Y, Z ) ) = ti( X, Z
% 0.89/1.37 ), hBOOL( hAPP( X, bool, Y, hAPP( fun( X, bool ), X, the( X ), Y ) ) ) }
% 0.89/1.37 .
% 0.89/1.37 { hBOOL( hAPP( state, bool, hAPP( X, fun( state, bool ), U, skol17( X, Y, Z
% 0.89/1.37 , T, U ) ), skol38( X, Y, Z, T, U ) ) ), hBOOL( hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Z ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), U ), T ), Y ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Z ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), W ), T ), V0 ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), ! hBOOL( hAPP( state, bool,
% 0.89/1.37 hAPP( X, fun( state, bool ), Y, skol17( X, Y, Z, T, U ) ), skol48( X, Y,
% 0.89/1.37 Z, T, U, V1, V2 ) ) ), hBOOL( hAPP( fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), bool, hAPP( fun( hoare_509422987triple( X ), bool ), fun( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool ), hoare_122391849derivs( X ), Z
% 0.89/1.37 ), hAPP( fun( hoare_509422987triple( X ), bool ), fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), hAPP( hoare_509422987triple( X ), fun
% 0.89/1.37 ( fun( hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ) ), insert( hoare_509422987triple( X ) ), hAPP( fun( X, fun(
% 0.89/1.37 state, bool ) ), hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun
% 0.89/1.37 ( state, bool ) ), hoare_509422987triple( X ) ), hAPP( fun( X, fun( state
% 0.89/1.37 , bool ) ), fun( com, fun( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ), U ), T ), Y
% 0.89/1.37 ) ), bot_bot( fun( hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( X ), bool ), bool, hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( fun( hoare_509422987triple( X )
% 0.89/1.37 , bool ), bool ), hoare_122391849derivs( X ), Z ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X ), bool
% 0.89/1.37 ), hAPP( hoare_509422987triple( X ), fun( fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ), fun( hoare_509422987triple( X ), bool ) ), insert(
% 0.89/1.37 hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun( state, bool ) )
% 0.89/1.37 , hoare_509422987triple( X ) ), hAPP( fun( X, fun( state, bool ) ), fun(
% 0.89/1.37 com, fun( fun( X, fun( state, bool ) ), hoare_509422987triple( X ) ) ),
% 0.89/1.37 hoare_1008221573triple( X ), W ), T ), V0 ) ), bot_bot( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ) ) ) ) ), ! hBOOL( hAPP( state, bool,
% 0.89/1.37 hAPP( X, fun( state, bool ), W, V1 ), skol38( X, Y, Z, T, U ) ) ), hBOOL
% 0.89/1.37 ( hAPP( state, bool, hAPP( X, fun( state, bool ), V0, V1 ), skol48( X, Y
% 0.89/1.37 , Z, T, U, W, V0 ) ) ), hBOOL( hAPP( fun( hoare_509422987triple( X ),
% 0.89/1.37 bool ), bool, hAPP( fun( hoare_509422987triple( X ), bool ), fun( fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), bool ), hoare_122391849derivs( X ), Z
% 0.89/1.37 ), hAPP( fun( hoare_509422987triple( X ), bool ), fun(
% 0.89/1.37 hoare_509422987triple( X ), bool ), hAPP( hoare_509422987triple( X ), fun
% 0.89/1.37 ( fun( hoare_509422987triple( X ), bool ), fun( hoare_509422987triple( X
% 0.89/1.37 ), bool ) ), insert( hoare_509422987triple( X ) ), hAPP( fun( X, fun(
% 0.89/1.37 state, bool ) ), hoare_509422987triple( X ), hAPP( com, fun( fun( X, fun
% 0.89/1.37 ( state, bool ) ), hoare_509422987triple( X ) ), hAPP( fun( X, fun( state
% 0.89/1.37 , bool ) ), fun( com, fun( fun( X, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( X ) ) ), hoare_1008221573triple( X ), U ), T ), Y
% 0.89/1.37 ) ), bot_bot( fun( hoare_509422987triple( X ), bool ) ) ) ) ) }.
% 0.89/1.37 { ti( fun( X, bool ), Y ) = bot_bot( fun( X, bool ) ), ti( fun( X, bool ),
% 0.89/1.37 Y ) = hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool )
% 0.89/1.37 , fun( X, bool ) ), insert( X ), skol18( X, Y ) ), skol39( X, Y ) ) }.
% 0.89/1.37 { ti( fun( X, bool ), Y ) = bot_bot( fun( X, bool ) ), ! hBOOL( hAPP( fun(
% 0.89/1.37 X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ), member( X ),
% 0.89/1.37 skol18( X, Y ) ), skol39( X, Y ) ) ) }.
% 0.89/1.37 { ! ti( fun( X, bool ), Y ) = hAPP( fun( X, bool ), fun( X, bool ), hAPP( X
% 0.89/1.37 , fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Z ), T ), hBOOL(
% 0.89/1.37 hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ), member
% 0.89/1.37 ( X ), Z ), T ) ), ! ti( fun( X, bool ), Y ) = bot_bot( fun( X, bool ) )
% 0.89/1.37 }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun(
% 0.89/1.37 X, fun( X, X ) ), fun( fun( X, bool ), fun( X, bool ) ), finite_fold1Set
% 0.89/1.37 ( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X,
% 0.89/1.37 bool ), fun( X, bool ) ), insert( X ), Z ), bot_bot( fun( X, bool ) ) ) )
% 0.89/1.37 , T ) ), ti( X, Z ) = ti( X, T ) }.
% 0.89/1.37 { ! ti( X, Z ) = ti( X, T ), hBOOL( hAPP( X, bool, hAPP( fun( X, bool ),
% 0.89/1.37 fun( X, bool ), hAPP( fun( X, fun( X, X ) ), fun( fun( X, bool ), fun( X
% 0.89/1.37 , bool ) ), finite_fold1Set( X ), Y ), hAPP( fun( X, bool ), fun( X, bool
% 0.89/1.37 ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Z ),
% 0.89/1.37 bot_bot( fun( X, bool ) ) ) ), T ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( fun( X, bool ), X ), bool, hAPP( fun( X, fun( X, X )
% 0.89/1.37 ), fun( fun( fun( X, bool ), X ), bool ), finite_folding_one( X ), Z ),
% 0.89/1.37 Y ) ), hAPP( fun( X, bool ), X, Y, hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), T ), bot_bot
% 0.89/1.37 ( fun( X, bool ) ) ) ) = ti( X, T ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, bot_bot( fun( X, bool ) ), Y ) ), hBOOL( hAPP(
% 0.89/1.37 fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ), member( X ),
% 0.89/1.37 Y ), bot_bot( fun( X, bool ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), bot_bot( fun( X, bool ) ) ) ), hBOOL( hAPP( X, bool,
% 0.89/1.37 bot_bot( fun( X, bool ) ), Y ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun(
% 0.89/1.37 X, fun( X, X ) ), fun( fun( X, bool ), fun( X, bool ) ), finite_fold1Set
% 0.89/1.37 ( X ), Y ), bot_bot( fun( X, bool ) ) ), Z ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun(
% 0.89/1.37 X, fun( X, X ) ), fun( fun( X, bool ), fun( X, bool ) ), finite_fold1Set
% 0.89/1.37 ( X ), Z ), Y ), T ) ), ! ti( fun( X, bool ), Y ) = bot_bot( fun( X, bool
% 0.89/1.37 ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), fun( X, bool ) ), hAPP( fun( X, fun( X, X ) ), fun(
% 0.89/1.37 X, fun( fun( X, bool ), fun( X, bool ) ) ), finite_fold_graph( X, X ), Y
% 0.89/1.37 ), Z ), T ), U ) ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun
% 0.89/1.37 ( X, bool ), bool ), member( X ), Z ), T ) ), hBOOL( hAPP( X, bool, hAPP
% 0.89/1.37 ( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun( X, X ) ), fun( fun(
% 0.89/1.37 X, bool ), fun( X, bool ) ), finite_fold1Set( X ), Y ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ),
% 0.89/1.37 insert( X ), Z ), T ) ), U ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( fun( X, bool ), X ), bool, hAPP( fun( X, fun( X, X )
% 0.89/1.37 ), fun( fun( fun( X, bool ), X ), bool ), finite_folding_one( X ), Y ),
% 0.89/1.37 Z ) ), ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), T ) ),
% 0.89/1.37 hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ),
% 0.89/1.37 member( X ), U ), T ) ), ti( fun( X, bool ), T ) = bot_bot( fun( X, bool
% 0.89/1.37 ) ), hAPP( fun( X, bool ), X, Z, hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), U ), T ) ) =
% 0.89/1.37 hAPP( X, X, hAPP( X, fun( X, X ), Y, U ), hAPP( fun( X, bool ), X, Z, T
% 0.89/1.37 ) ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), X, hAPP( fun( X, fun( X, X ) ), fun( fun( X, bool )
% 0.89/1.37 , X ), finite_fold1( X ), Y ), Z ) = hAPP( fun( X, bool ), X, the( X ),
% 0.89/1.37 hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun( X, X ) ), fun(
% 0.89/1.37 fun( X, bool ), fun( X, bool ) ), finite_fold1Set( X ), Y ), Z ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), collect( X ), Z ) ) ), hBOOL( hAPP( fun( X, bool
% 0.89/1.37 ), bool, finite_finite_1( X ), hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 collect( X ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun(
% 0.89/1.37 bool, bool ) ), fun( fun( X, bool ), fun( X, bool ) ), combs( X, bool,
% 0.89/1.37 bool ), hAPP( fun( X, bool ), fun( X, fun( bool, bool ) ), hAPP( fun(
% 0.89/1.37 bool, fun( bool, bool ) ), fun( fun( X, bool ), fun( X, fun( bool, bool )
% 0.89/1.37 ) ), combb( bool, fun( bool, bool ), X ), fconj ), Z ) ), Y ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), collect( X ), Y ) ) ), hBOOL( hAPP( fun( X, bool
% 0.89/1.37 ), bool, finite_finite_1( X ), hAPP( fun( X, bool ), fun( X, bool ),
% 0.89/1.37 collect( X ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun(
% 0.89/1.37 bool, bool ) ), fun( fun( X, bool ), fun( X, bool ) ), combs( X, bool,
% 0.89/1.37 bool ), hAPP( fun( X, bool ), fun( X, fun( bool, bool ) ), hAPP( fun(
% 0.89/1.37 bool, fun( bool, bool ) ), fun( fun( X, bool ), fun( X, fun( bool, bool )
% 0.89/1.37 ) ), combb( bool, fun( bool, bool ), X ), fconj ), Z ) ), Y ) ) ) ) }.
% 0.89/1.37 { hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), bot_bot( fun( X
% 0.89/1.37 , bool ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), Y ) ), hBOOL(
% 0.89/1.37 hAPP( fun( X, bool ), bool, finite_finite_1( X ), hAPP( fun( X, bool ),
% 0.89/1.37 fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X
% 0.89/1.37 ), Z ), Y ) ) ) }.
% 0.89/1.37 { ! hAPP( X, Y, Z, skol19( X, Y, Z, T ) ) = hAPP( X, Y, T, skol19( X, Y, Z
% 0.89/1.37 , T ) ), ti( fun( X, Y ), Z ) = ti( fun( X, Y ), T ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool )
% 0.89/1.37 , member( X ), Y ), Z ) ), hBOOL( hAPP( X, bool, Z, Y ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, Z, Y ) ), hBOOL( hAPP( fun( X, bool ), bool, hAPP
% 0.89/1.37 ( X, fun( fun( X, bool ), bool ), member( X ), Y ), Z ) ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), fun( X, bool ), collect( X ), Y ) = ti( fun( X,
% 0.89/1.37 bool ), Y ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( fun( X, bool ), X ), bool, hAPP( fun( X, fun( X, X )
% 0.89/1.37 ), fun( fun( fun( X, bool ), X ), bool ), finite_folding_one( X ), Y ),
% 0.89/1.37 Z ) ), ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), T ) ),
% 0.89/1.37 hAPP( fun( X, bool ), X, Z, T ) = hAPP( fun( X, bool ), X, hAPP( fun( X,
% 0.89/1.37 fun( X, X ) ), fun( fun( X, bool ), X ), finite_fold1( X ), Y ), T ) }.
% 0.89/1.37 { hBOOL( hAPP( X, bool, hAPP( fun( Y, bool ), fun( X, bool ), hAPP( X, fun
% 0.89/1.37 ( fun( Y, bool ), fun( X, bool ) ), hAPP( fun( Y, fun( X, X ) ), fun( X,
% 0.89/1.37 fun( fun( Y, bool ), fun( X, bool ) ) ), finite_fold_graph( Y, X ), Z ),
% 0.89/1.37 T ), bot_bot( fun( Y, bool ) ) ), T ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( T, bool ), fun( X, bool ), hAPP( X,
% 0.89/1.37 fun( fun( T, bool ), fun( X, bool ) ), hAPP( fun( T, fun( X, X ) ), fun(
% 0.89/1.37 X, fun( fun( T, bool ), fun( X, bool ) ) ), finite_fold_graph( T, X ), U
% 0.89/1.37 ), Y ), bot_bot( fun( T, bool ) ) ), Z ) ), ti( X, Z ) = ti( X, Y ) }.
% 0.89/1.37 { hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ),
% 0.89/1.37 member( X ), Y ), Z ) ), ! hBOOL( hAPP( T, bool, hAPP( fun( X, bool ),
% 0.89/1.37 fun( T, bool ), hAPP( T, fun( fun( X, bool ), fun( T, bool ) ), hAPP( fun
% 0.89/1.37 ( X, fun( T, T ) ), fun( T, fun( fun( X, bool ), fun( T, bool ) ) ),
% 0.89/1.37 finite_fold_graph( X, T ), U ), W ), Z ), V0 ) ), hBOOL( hAPP( T, bool,
% 0.89/1.37 hAPP( fun( X, bool ), fun( T, bool ), hAPP( T, fun( fun( X, bool ), fun(
% 0.89/1.37 T, bool ) ), hAPP( fun( X, fun( T, T ) ), fun( T, fun( fun( X, bool ),
% 0.89/1.37 fun( T, bool ) ) ), finite_fold_graph( X, T ), U ), W ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ),
% 0.89/1.37 insert( X ), Y ), Z ) ), hAPP( T, T, hAPP( X, fun( T, T ), U, Y ), V0 ) )
% 0.89/1.37 ) }.
% 0.89/1.37 { ! finite_finite( X ), hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1
% 0.89/1.37 ( X ), Y ) ) }.
% 0.89/1.37 { ! finite_finite( X ), hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1
% 0.89/1.37 ( X ), Y ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), collect( X ), hAPP( fun( X, bool ), fun( X, bool
% 0.89/1.37 ), hAPP( fun( X, fun( bool, bool ) ), fun( fun( X, bool ), fun( X, bool
% 0.89/1.37 ) ), combs( X, bool, bool ), hAPP( fun( X, bool ), fun( X, fun( bool,
% 0.89/1.37 bool ) ), hAPP( fun( bool, fun( bool, bool ) ), fun( fun( X, bool ), fun
% 0.89/1.37 ( X, fun( bool, bool ) ) ), combb( bool, fun( bool, bool ), X ), fdisj )
% 0.89/1.37 , Y ) ), Z ) ) ) ), hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X
% 0.89/1.37 ), hAPP( fun( X, bool ), fun( X, bool ), collect( X ), Y ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), collect( X ), hAPP( fun( X, bool ), fun( X, bool
% 0.89/1.37 ), hAPP( fun( X, fun( bool, bool ) ), fun( fun( X, bool ), fun( X, bool
% 0.89/1.37 ) ), combs( X, bool, bool ), hAPP( fun( X, bool ), fun( X, fun( bool,
% 0.89/1.37 bool ) ), hAPP( fun( bool, fun( bool, bool ) ), fun( fun( X, bool ), fun
% 0.89/1.37 ( X, fun( bool, bool ) ) ), combb( bool, fun( bool, bool ), X ), fdisj )
% 0.89/1.37 , Y ) ), Z ) ) ) ), hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X
% 0.89/1.37 ), hAPP( fun( X, bool ), fun( X, bool ), collect( X ), Z ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), collect( X ), Y ) ) ), ! hBOOL( hAPP( fun( X,
% 0.89/1.37 bool ), bool, finite_finite_1( X ), hAPP( fun( X, bool ), fun( X, bool )
% 0.89/1.37 , collect( X ), Z ) ) ), hBOOL( hAPP( fun( X, bool ), bool,
% 0.89/1.37 finite_finite_1( X ), hAPP( fun( X, bool ), fun( X, bool ), collect( X )
% 0.89/1.37 , hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun( bool, bool ) )
% 0.89/1.37 , fun( fun( X, bool ), fun( X, bool ) ), combs( X, bool, bool ), hAPP(
% 0.89/1.37 fun( X, bool ), fun( X, fun( bool, bool ) ), hAPP( fun( bool, fun( bool,
% 0.89/1.37 bool ) ), fun( fun( X, bool ), fun( X, fun( bool, bool ) ) ), combb( bool
% 0.89/1.37 , fun( bool, bool ), X ), fdisj ), Y ) ), Z ) ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ),
% 0.89/1.37 insert( X ), Y ), Z ) ) ), hBOOL( hAPP( fun( X, bool ), bool,
% 0.89/1.37 finite_finite_1( X ), Z ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), Z ) ), hBOOL(
% 0.89/1.37 hAPP( fun( X, bool ), bool, finite_finite_1( X ), hAPP( fun( X, bool ),
% 0.89/1.37 fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X
% 0.89/1.37 ), Y ), Z ) ) ) }.
% 0.89/1.37 { ! Y = hAPP( fun( X, fun( X, X ) ), fun( fun( X, bool ), X ), finite_fold1
% 0.89/1.37 ( X ), Z ), hAPP( fun( X, bool ), X, Y, hAPP( fun( X, bool ), fun( X,
% 0.89/1.37 bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), T )
% 0.89/1.37 , bot_bot( fun( X, bool ) ) ) ) = ti( X, T ) }.
% 0.89/1.37 { hAPP( fun( X, bool ), X, hAPP( fun( X, fun( X, X ) ), fun( fun( X, bool )
% 0.89/1.37 , X ), finite_fold1( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP
% 0.89/1.37 ( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), Z ), bot_bot(
% 0.89/1.37 fun( X, bool ) ) ) ) = ti( X, Z ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( fun( X, bool ), X ), bool, hAPP( fun( X, fun( X, X )
% 0.89/1.37 ), fun( fun( fun( X, bool ), X ), bool ), finite_folding_one( X ), Y ),
% 0.89/1.37 Z ) ), ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), T ) ),
% 0.89/1.37 ti( fun( X, bool ), T ) = bot_bot( fun( X, bool ) ), ! hBOOL( hAPP( fun(
% 0.89/1.37 X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ), member( X ), hAPP
% 0.89/1.37 ( X, X, hAPP( X, fun( X, X ), Y, skol20( X, Y ) ), skol40( X, Y ) ) ),
% 0.89/1.37 hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun(
% 0.89/1.37 X, bool ) ), insert( X ), skol20( X, Y ) ), hAPP( fun( X, bool ), fun( X
% 0.89/1.37 , bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ),
% 0.89/1.37 skol40( X, Y ) ), bot_bot( fun( X, bool ) ) ) ) ) ), hBOOL( hAPP( fun( X
% 0.89/1.37 , bool ), bool, hAPP( X, fun( fun( X, bool ), bool ), member( X ), hAPP(
% 0.89/1.37 fun( X, bool ), X, Z, T ) ), T ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun(
% 0.89/1.37 X, fun( X, X ) ), fun( fun( X, bool ), fun( X, bool ) ), finite_fold1Set
% 0.89/1.37 ( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X,
% 0.89/1.37 bool ), fun( X, bool ) ), insert( X ), Z ), T ) ), U ) ), hAPP( fun( X,
% 0.89/1.37 bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ),
% 0.89/1.37 insert( X ), Z ), T ) = hAPP( fun( X, bool ), fun( X, bool ), hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), fun( X, bool ) ), insert( X ), skol21( X, Y, Z, T, U
% 0.89/1.37 ) ), skol41( X, Y, Z, T, U ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun(
% 0.89/1.37 X, fun( X, X ) ), fun( fun( X, bool ), fun( X, bool ) ), finite_fold1Set
% 0.89/1.37 ( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X,
% 0.89/1.37 bool ), fun( X, bool ) ), insert( X ), Z ), T ) ), U ) ), hBOOL( hAPP( X
% 0.89/1.37 , bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool
% 0.89/1.37 ), fun( X, bool ) ), hAPP( fun( X, fun( X, X ) ), fun( X, fun( fun( X,
% 0.89/1.37 bool ), fun( X, bool ) ) ), finite_fold_graph( X, X ), Y ), skol21( X, Y
% 0.89/1.37 , Z, T, U ) ), skol41( X, Y, Z, T, U ) ), U ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun(
% 0.89/1.37 X, fun( X, X ) ), fun( fun( X, bool ), fun( X, bool ) ), finite_fold1Set
% 0.89/1.37 ( X ), Y ), hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X,
% 0.89/1.37 bool ), fun( X, bool ) ), insert( X ), Z ), T ) ), U ) ), ! hBOOL( hAPP(
% 0.89/1.37 fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ), member( X ),
% 0.89/1.37 skol21( X, Y, Z, T, U ) ), skol41( X, Y, Z, T, U ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), Y ) ), ti( fun
% 0.89/1.37 ( X, bool ), Y ) = bot_bot( fun( X, bool ) ), hBOOL( hAPP( X, bool, hAPP
% 0.89/1.37 ( fun( X, bool ), fun( X, bool ), hAPP( fun( X, fun( X, X ) ), fun( fun(
% 0.89/1.37 X, bool ), fun( X, bool ) ), finite_fold1Set( X ), Z ), Y ), skol22( X, Y
% 0.89/1.37 , Z ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), Y ) ), ! hBOOL
% 0.89/1.37 ( hAPP( fun( X, bool ), bool, Z, bot_bot( fun( X, bool ) ) ) ), hBOOL(
% 0.89/1.37 hAPP( fun( X, bool ), bool, finite_finite_1( X ), skol23( X, T ) ) ),
% 0.89/1.37 hBOOL( hAPP( fun( X, bool ), bool, Z, Y ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), Y ) ), ! hBOOL
% 0.89/1.37 ( hAPP( fun( X, bool ), bool, Z, bot_bot( fun( X, bool ) ) ) ), alpha11(
% 0.89/1.37 X, Z, skol23( X, Z ) ), hBOOL( hAPP( fun( X, bool ), bool, Z, Y ) ) }.
% 0.89/1.37 { ! alpha11( X, Y, Z ), ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun(
% 0.89/1.37 fun( X, bool ), bool ), member( X ), skol24( X, T, Z ) ), Z ) ) }.
% 0.89/1.37 { ! alpha11( X, Y, Z ), hBOOL( hAPP( fun( X, bool ), bool, Y, Z ) ) }.
% 0.89/1.37 { ! alpha11( X, Y, Z ), ! hBOOL( hAPP( fun( X, bool ), bool, Y, hAPP( fun(
% 0.89/1.37 X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) )
% 0.89/1.37 , insert( X ), skol24( X, Y, Z ) ), Z ) ) ) }.
% 0.89/1.37 { hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ),
% 0.89/1.37 member( X ), T ), Z ) ), ! hBOOL( hAPP( fun( X, bool ), bool, Y, Z ) ),
% 0.89/1.37 hBOOL( hAPP( fun( X, bool ), bool, Y, hAPP( fun( X, bool ), fun( X, bool
% 0.89/1.37 ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), T ), Z )
% 0.89/1.37 ) ), alpha11( X, Y, Z ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), Y ) ), ti( fun
% 0.89/1.37 ( X, bool ), Y ) = bot_bot( fun( X, bool ) ), alpha3( X, Y ) }.
% 0.89/1.37 { ! ti( fun( X, bool ), Y ) = bot_bot( fun( X, bool ) ), hBOOL( hAPP( fun(
% 0.89/1.37 X, bool ), bool, finite_finite_1( X ), Y ) ) }.
% 0.89/1.37 { ! alpha3( X, Y ), hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X )
% 0.89/1.37 , Y ) ) }.
% 0.89/1.37 { ! alpha3( X, Y ), hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X )
% 0.89/1.37 , skol25( X, Z ) ) ) }.
% 0.89/1.37 { ! alpha3( X, Y ), ti( fun( X, bool ), Y ) = hAPP( fun( X, bool ), fun( X
% 0.89/1.37 , bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ),
% 0.89/1.37 skol42( X, Y ) ), skol25( X, Y ) ) }.
% 0.89/1.37 { ! ti( fun( X, bool ), Y ) = hAPP( fun( X, bool ), fun( X, bool ), hAPP( X
% 0.89/1.37 , fun( fun( X, bool ), fun( X, bool ) ), insert( X ), T ), Z ), ! hBOOL(
% 0.89/1.37 hAPP( fun( X, bool ), bool, finite_finite_1( X ), Z ) ), alpha3( X, Y ) }
% 0.89/1.37 .
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), Y ) ), hBOOL(
% 0.89/1.37 hAPP( Z, bool, hAPP( fun( X, bool ), fun( Z, bool ), hAPP( Z, fun( fun( X
% 0.89/1.37 , bool ), fun( Z, bool ) ), hAPP( fun( X, fun( Z, Z ) ), fun( Z, fun( fun
% 0.89/1.37 ( X, bool ), fun( Z, bool ) ) ), finite_fold_graph( X, Z ), T ), U ), Y )
% 0.89/1.37 , skol26( X, Y, Z, T, U ) ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun(
% 0.89/1.37 X, fun( X, X ) ), fun( fun( X, bool ), fun( X, bool ) ), finite_fold1Set
% 0.89/1.37 ( X ), Y ), Z ), T ) ), ti( fun( X, bool ), Z ) = hAPP( fun( X, bool ),
% 0.89/1.37 fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X
% 0.89/1.37 ), skol27( X, Y, Z, T ) ), skol43( X, Y, Z, T ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( fun(
% 0.89/1.37 X, fun( X, X ) ), fun( fun( X, bool ), fun( X, bool ) ), finite_fold1Set
% 0.89/1.37 ( X ), Y ), Z ), T ) ), alpha4( X, Y, T, skol27( X, Y, Z, T ), skol43( X
% 0.89/1.37 , Y, Z, T ) ) }.
% 0.89/1.37 { ! ti( fun( X, bool ), Z ) = hAPP( fun( X, bool ), fun( X, bool ), hAPP( X
% 0.89/1.37 , fun( fun( X, bool ), fun( X, bool ) ), insert( X ), U ), W ), ! alpha4
% 0.89/1.37 ( X, Y, T, U, W ), hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X,
% 0.89/1.37 bool ), hAPP( fun( X, fun( X, X ) ), fun( fun( X, bool ), fun( X, bool )
% 0.89/1.37 ), finite_fold1Set( X ), Y ), Z ), T ) ) }.
% 0.89/1.37 { ! alpha4( X, Y, Z, T, U ), ti( X, Z ) = ti( X, skol28( X, W, Z, V0, V1 )
% 0.89/1.37 ) }.
% 0.89/1.37 { ! alpha4( X, Y, Z, T, U ), alpha7( X, Y, T, U, skol28( X, Y, Z, T, U ) )
% 0.89/1.37 }.
% 0.89/1.37 { ! ti( X, Z ) = ti( X, W ), ! alpha7( X, Y, T, U, W ), alpha4( X, Y, Z, T
% 0.89/1.37 , U ) }.
% 0.89/1.37 { ! alpha7( X, Y, Z, T, U ), hBOOL( hAPP( X, bool, hAPP( fun( X, bool ),
% 0.89/1.37 fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), hAPP( fun
% 0.89/1.37 ( X, fun( X, X ) ), fun( X, fun( fun( X, bool ), fun( X, bool ) ) ),
% 0.89/1.37 finite_fold_graph( X, X ), Y ), Z ), T ), U ) ) }.
% 0.89/1.37 { ! alpha7( X, Y, Z, T, U ), ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), bool ), member( X ), Z ), T ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( X, bool ), fun( X, bool ), hAPP( X,
% 0.89/1.37 fun( fun( X, bool ), fun( X, bool ) ), hAPP( fun( X, fun( X, X ) ), fun(
% 0.89/1.37 X, fun( fun( X, bool ), fun( X, bool ) ) ), finite_fold_graph( X, X ), Y
% 0.89/1.37 ), Z ), T ), U ) ), hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun
% 0.89/1.37 ( X, bool ), bool ), member( X ), Z ), T ) ), alpha7( X, Y, Z, T, U ) }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( fun( Y, bool ), fun( X, bool ), hAPP( X,
% 0.89/1.37 fun( fun( Y, bool ), fun( X, bool ) ), hAPP( fun( Y, fun( X, X ) ), fun(
% 0.89/1.37 X, fun( fun( Y, bool ), fun( X, bool ) ) ), finite_fold_graph( Y, X ), Z
% 0.89/1.37 ), T ), U ), W ) ), alpha5( X, Y, T, U, W ), alpha8( X, Y, Z, T, U, W )
% 0.89/1.37 }.
% 0.89/1.37 { ! alpha5( X, Y, T, U, W ), hBOOL( hAPP( X, bool, hAPP( fun( Y, bool ),
% 0.89/1.37 fun( X, bool ), hAPP( X, fun( fun( Y, bool ), fun( X, bool ) ), hAPP( fun
% 0.89/1.37 ( Y, fun( X, X ) ), fun( X, fun( fun( Y, bool ), fun( X, bool ) ) ),
% 0.89/1.37 finite_fold_graph( Y, X ), Z ), T ), U ), W ) ) }.
% 0.89/1.37 { ! alpha8( X, Y, Z, T, U, W ), hBOOL( hAPP( X, bool, hAPP( fun( Y, bool )
% 0.89/1.37 , fun( X, bool ), hAPP( X, fun( fun( Y, bool ), fun( X, bool ) ), hAPP(
% 0.89/1.37 fun( Y, fun( X, X ) ), fun( X, fun( fun( Y, bool ), fun( X, bool ) ) ),
% 0.89/1.37 finite_fold_graph( Y, X ), Z ), T ), U ), W ) ) }.
% 0.89/1.37 { ! alpha8( X, Y, Z, T, U, W ), ti( fun( Y, bool ), U ) = hAPP( fun( Y,
% 0.89/1.37 bool ), fun( Y, bool ), hAPP( Y, fun( fun( Y, bool ), fun( Y, bool ) ),
% 0.89/1.37 insert( Y ), skol29( X, Y, Z, T, U, W ) ), skol44( X, Y, Z, T, U, W ) ) }
% 0.89/1.37 .
% 0.89/1.37 { ! alpha8( X, Y, Z, T, U, W ), alpha9( X, Y, Z, T, W, skol29( X, Y, Z, T,
% 0.89/1.37 U, W ), skol44( X, Y, Z, T, U, W ) ) }.
% 0.89/1.37 { ! ti( fun( Y, bool ), U ) = hAPP( fun( Y, bool ), fun( Y, bool ), hAPP( Y
% 0.89/1.37 , fun( fun( Y, bool ), fun( Y, bool ) ), insert( Y ), V0 ), V1 ), !
% 0.89/1.37 alpha9( X, Y, Z, T, W, V0, V1 ), alpha8( X, Y, Z, T, U, W ) }.
% 0.89/1.37 { ! alpha9( X, Y, Z, T, U, W, V0 ), ti( X, U ) = hAPP( X, X, hAPP( Y, fun(
% 0.89/1.37 X, X ), Z, W ), skol30( X, Y, Z, V1, U, W, V2 ) ) }.
% 0.89/1.37 { ! alpha9( X, Y, Z, T, U, W, V0 ), alpha10( X, Y, Z, T, W, V0, skol30( X,
% 0.89/1.37 Y, Z, T, U, W, V0 ) ) }.
% 0.89/1.37 { ! ti( X, U ) = hAPP( X, X, hAPP( Y, fun( X, X ), Z, W ), V1 ), ! alpha10
% 0.89/1.37 ( X, Y, Z, T, W, V0, V1 ), alpha9( X, Y, Z, T, U, W, V0 ) }.
% 0.89/1.37 { ! alpha10( X, Y, Z, T, U, W, V0 ), ! hBOOL( hAPP( fun( Y, bool ), bool,
% 0.89/1.37 hAPP( Y, fun( fun( Y, bool ), bool ), member( Y ), U ), W ) ) }.
% 0.89/1.37 { ! alpha10( X, Y, Z, T, U, W, V0 ), hBOOL( hAPP( X, bool, hAPP( fun( Y,
% 0.89/1.37 bool ), fun( X, bool ), hAPP( X, fun( fun( Y, bool ), fun( X, bool ) ),
% 0.89/1.37 hAPP( fun( Y, fun( X, X ) ), fun( X, fun( fun( Y, bool ), fun( X, bool )
% 0.89/1.37 ) ), finite_fold_graph( Y, X ), Z ), T ), W ), V0 ) ) }.
% 0.89/1.37 { hBOOL( hAPP( fun( Y, bool ), bool, hAPP( Y, fun( fun( Y, bool ), bool ),
% 0.89/1.37 member( Y ), U ), W ) ), ! hBOOL( hAPP( X, bool, hAPP( fun( Y, bool ),
% 0.89/1.37 fun( X, bool ), hAPP( X, fun( fun( Y, bool ), fun( X, bool ) ), hAPP( fun
% 0.89/1.37 ( Y, fun( X, X ) ), fun( X, fun( fun( Y, bool ), fun( X, bool ) ) ),
% 0.89/1.37 finite_fold_graph( Y, X ), Z ), T ), W ), V0 ) ), alpha10( X, Y, Z, T, U
% 0.89/1.37 , W, V0 ) }.
% 0.89/1.37 { ! alpha5( X, Y, Z, T, U ), ti( fun( Y, bool ), T ) = bot_bot( fun( Y,
% 0.89/1.37 bool ) ) }.
% 0.89/1.37 { ! alpha5( X, Y, Z, T, U ), ti( X, U ) = ti( X, Z ) }.
% 0.89/1.37 { ! ti( fun( Y, bool ), T ) = bot_bot( fun( Y, bool ) ), ! ti( X, U ) = ti
% 0.89/1.37 ( X, Z ), alpha5( X, Y, Z, T, U ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( fun( X, bool ), X ), bool, hAPP( fun( X, fun( X, X )
% 0.89/1.37 ), fun( fun( fun( X, bool ), X ), bool ), finite2073411215e_idem( X ), Y
% 0.89/1.37 ), Z ) ), ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), T )
% 0.89/1.37 ), ti( fun( X, bool ), T ) = bot_bot( fun( X, bool ) ), hAPP( fun( X,
% 0.89/1.37 bool ), X, Z, hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X
% 0.89/1.37 , bool ), fun( X, bool ) ), insert( X ), U ), T ) ) = hAPP( X, X, hAPP( X
% 0.89/1.37 , fun( X, X ), Y, U ), hAPP( fun( X, bool ), X, Z, T ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), Y ) ), ti( fun
% 0.89/1.37 ( X, bool ), Y ) = bot_bot( fun( X, bool ) ), ! hBOOL( hAPP( fun( X, bool
% 0.89/1.37 ), bool, Z, hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X,
% 0.89/1.37 bool ), fun( X, bool ) ), insert( X ), skol31( X, Z ) ), bot_bot( fun( X
% 0.89/1.37 , bool ) ) ) ) ), alpha12( X, skol45( X, T ) ), hBOOL( hAPP( fun( X, bool
% 0.89/1.37 ), bool, Z, Y ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), Y ) ), ti( fun
% 0.89/1.37 ( X, bool ), Y ) = bot_bot( fun( X, bool ) ), ! hBOOL( hAPP( fun( X, bool
% 0.89/1.37 ), bool, Z, hAPP( fun( X, bool ), fun( X, bool ), hAPP( X, fun( fun( X,
% 0.89/1.37 bool ), fun( X, bool ) ), insert( X ), skol31( X, Z ) ), bot_bot( fun( X
% 0.89/1.37 , bool ) ) ) ) ), alpha13( X, Z, skol45( X, Z ) ), hBOOL( hAPP( fun( X,
% 0.89/1.37 bool ), bool, Z, Y ) ) }.
% 0.89/1.37 { ! alpha13( X, Y, Z ), ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun(
% 0.89/1.37 fun( X, bool ), bool ), member( X ), skol32( X, T, Z ) ), Z ) ) }.
% 0.89/1.37 { ! alpha13( X, Y, Z ), hBOOL( hAPP( fun( X, bool ), bool, Y, Z ) ) }.
% 0.89/1.37 { ! alpha13( X, Y, Z ), ! hBOOL( hAPP( fun( X, bool ), bool, Y, hAPP( fun(
% 0.89/1.37 X, bool ), fun( X, bool ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) )
% 0.89/1.37 , insert( X ), skol32( X, Y, Z ) ), Z ) ) ) }.
% 0.89/1.37 { hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ), bool ),
% 0.89/1.37 member( X ), T ), Z ) ), ! hBOOL( hAPP( fun( X, bool ), bool, Y, Z ) ),
% 0.89/1.37 hBOOL( hAPP( fun( X, bool ), bool, Y, hAPP( fun( X, bool ), fun( X, bool
% 0.89/1.37 ), hAPP( X, fun( fun( X, bool ), fun( X, bool ) ), insert( X ), T ), Z )
% 0.89/1.37 ) ), alpha13( X, Y, Z ) }.
% 0.89/1.37 { ! alpha12( X, Y ), hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X
% 0.89/1.37 ), Y ) ) }.
% 0.89/1.37 { ! alpha12( X, Y ), ! ti( fun( X, bool ), Y ) = bot_bot( fun( X, bool ) )
% 0.89/1.37 }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), Y ) ), ti( fun
% 0.89/1.37 ( X, bool ), Y ) = bot_bot( fun( X, bool ) ), alpha12( X, Y ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( fun( X, bool ), X ), bool, hAPP( fun( X, fun( X, X )
% 0.89/1.37 ), fun( fun( fun( X, bool ), X ), bool ), finite2073411215e_idem( X ), Y
% 0.89/1.37 ), Z ) ), hAPP( X, X, hAPP( X, fun( X, X ), Y, T ), T ) = ti( X, T ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( fun( X, bool ), X ), bool, hAPP( fun( X, fun( X, X )
% 0.89/1.37 ), fun( fun( fun( X, bool ), X ), bool ), finite2073411215e_idem( X ), Y
% 0.89/1.37 ), Z ) ), ! hBOOL( hAPP( fun( X, bool ), bool, finite_finite_1( X ), T )
% 0.89/1.37 ), ! hBOOL( hAPP( fun( X, bool ), bool, hAPP( X, fun( fun( X, bool ),
% 0.89/1.37 bool ), member( X ), U ), T ) ), hAPP( X, X, hAPP( X, fun( X, X ), Y, U )
% 0.89/1.37 , hAPP( fun( X, bool ), X, Z, T ) ) = hAPP( fun( X, bool ), X, Z, T ) }.
% 0.89/1.37 { ! finite_finite( Y ), ! finite_finite( X ), finite_finite( fun( X, Y ) )
% 0.89/1.37 }.
% 0.89/1.37 { ! bot( X ), bot( fun( Y, X ) ) }.
% 0.89/1.37 { finite_finite( bool ) }.
% 0.89/1.37 { bot( bool ) }.
% 0.89/1.37 { ti( X, ti( X, Y ) ) = ti( X, Y ) }.
% 0.89/1.37 { ! hBOOL( hAPP( bool, bool, fNot, X ) ), ! hBOOL( X ) }.
% 0.89/1.37 { hBOOL( X ), hBOOL( hAPP( bool, bool, fNot, X ) ) }.
% 0.89/1.37 { hAPP( X, Y, hAPP( fun( X, Z ), fun( X, Y ), hAPP( fun( Z, Y ), fun( fun(
% 0.89/1.37 X, Z ), fun( X, Y ) ), combb( Z, Y, X ), T ), U ), W ) = hAPP( Z, Y, T,
% 0.89/1.37 hAPP( X, Z, U, W ) ) }.
% 0.89/1.37 { hAPP( X, Y, hAPP( Z, fun( X, Y ), hAPP( fun( X, fun( Z, Y ) ), fun( Z,
% 0.89/1.37 fun( X, Y ) ), combc( X, Z, Y ), T ), U ), W ) = hAPP( Z, Y, hAPP( X, fun
% 0.89/1.37 ( Z, Y ), T, W ), U ) }.
% 0.89/1.37 { hAPP( X, Y, hAPP( Y, fun( X, Y ), combk( Y, X ), Z ), T ) = ti( Y, Z ) }
% 0.89/1.37 .
% 0.89/1.37 { hAPP( X, Y, hAPP( fun( X, Z ), fun( X, Y ), hAPP( fun( X, fun( Z, Y ) ),
% 0.89/1.37 fun( fun( X, Z ), fun( X, Y ) ), combs( X, Z, Y ), T ), U ), W ) = hAPP(
% 0.89/1.37 Z, Y, hAPP( X, fun( Z, Y ), T, W ), hAPP( X, Z, U, W ) ) }.
% 0.89/1.37 { ! hBOOL( X ), ! hBOOL( Y ), hBOOL( hAPP( bool, bool, hAPP( bool, fun(
% 0.89/1.37 bool, bool ), fconj, X ), Y ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( bool, bool, hAPP( bool, fun( bool, bool ), fconj, X ), Y )
% 0.89/1.37 ), hBOOL( X ) }.
% 0.89/1.37 { ! hBOOL( hAPP( bool, bool, hAPP( bool, fun( bool, bool ), fconj, Y ), X )
% 0.89/1.37 ), hBOOL( X ) }.
% 0.89/1.37 { ! hBOOL( X ), hBOOL( hAPP( bool, bool, hAPP( bool, fun( bool, bool ),
% 0.89/1.37 fdisj, X ), Y ) ) }.
% 0.89/1.37 { ! hBOOL( X ), hBOOL( hAPP( bool, bool, hAPP( bool, fun( bool, bool ),
% 0.89/1.37 fdisj, Y ), X ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( bool, bool, hAPP( bool, fun( bool, bool ), fdisj, X ), Y )
% 0.89/1.37 ), hBOOL( X ), hBOOL( Y ) }.
% 0.89/1.37 { ! hBOOL( fFalse ) }.
% 0.89/1.37 { ti( bool, X ) = fTrue, ti( bool, X ) = fFalse }.
% 0.89/1.37 { ! hBOOL( hAPP( X, bool, hAPP( X, fun( X, bool ), fequal( X ), Y ), Z ) )
% 0.89/1.37 , ti( X, Y ) = ti( X, Z ) }.
% 0.89/1.37 { ! ti( X, Y ) = ti( X, Z ), hBOOL( hAPP( X, bool, hAPP( X, fun( X, bool )
% 0.89/1.37 , fequal( X ), Y ), Z ) ) }.
% 0.89/1.37 { hBOOL( X ), hBOOL( hAPP( bool, bool, hAPP( bool, fun( bool, bool ),
% 0.89/1.37 fimplies, X ), Y ) ) }.
% 0.89/1.37 { ! hBOOL( X ), hBOOL( hAPP( bool, bool, hAPP( bool, fun( bool, bool ),
% 0.89/1.37 fimplies, Y ), X ) ) }.
% 0.89/1.37 { ! hBOOL( hAPP( bool, bool, hAPP( bool, fun( bool, bool ), fimplies, X ),
% 0.89/1.37 Y ) ), ! hBOOL( X ), hBOOL( Y ) }.
% 0.89/1.37 { ! hBOOL( hAPP( fun( hoare_509422987triple( x_a ), bool ), bool, hAPP( fun
% 0.89/1.37 ( hoare_509422987triple( x_a ), bool ), fun( fun( hoare_509422987triple(
% 0.89/1.37 x_a ), bool ), bool ), hoare_122391849derivs( x_a ), g ), hAPP( fun(
% 0.89/1.37 hoare_509422987triple( x_a ), bool ), fun( hoare_509422987triple( x_a ),
% 0.89/1.37 bool ), hAPP( hoare_509422987triple( x_a ), fun( fun(
% 0.89/1.37 hoare_509422987triple( x_a ), bool ), fun( hoare_509422987triple( x_a ),
% 0.89/1.37 bool ) ), insert( hoare_509422987triple( x_a ) ), hAPP( fun( x_a, fun(
% 0.89/1.37 state, bool ) ), hoare_509422987triple( x_a ), hAPP( com, fun( fun( x_a,
% 0.89/1.37 fun( state, bool ) ), hoare_509422987triple( x_a ) ), hAPP( fun( x_a, fun
% 0.89/1.37 ( state, bool ) ), fun( com, fun( fun( x_a, fun( state, bool ) ),
% 0.89/1.37 hoare_509422987triple( x_a ) ) ), hoare_1008221573triple( x_a ), hAPP(
% 0.89/1.37 fun( state, bool ), fun( x_a, fun( state, bool ) ), combk( fun( state,
% 0.89/1.37 bool ), x_a ), hAPP( bool, fun( state, bool ), combk( bool, state ),
% 0.89/1.37 fFalse ) ) ), c ), hAPP( fun( state, bool ), fun( x_a, fun( state, bool )
% 0.89/1.37 ), hAPP( fun( x_a, fun( fun( state, bool ), fun( state, bool ) ) ), fun
% 0.89/1.37 ( fun( state, bool ), fun( x_a, fun( state, bool ) ) ), combc( x_a, fun(
% 0.89/1.37 state, bool ), fun( state, bool ) ), hAPP( fun( x_a, fun( state, fun(
% 0.89/1.37 bool, bool ) ) ), fun( x_a, fun( fun( state, bool ), fun( state, bool ) )
% 0.89/1.37 ), hAPP( fun( fun( state, fun( bool, bool ) ), fun( fun( state, bool ),
% 0.89/1.37 fun( state, bool ) ) ), fun( fun( x_a, fun( state, fun( bool, bool ) ) )
% 0.89/1.37 , fun( x_a, fun( fun( state, bool ), fun( state, bool ) ) ) ), combb( fun
% 0.89/1.37 ( state, fun( bool, bool ) ), fun( fun( state, bool ), fun( state, bool )
% 0.89/1.37 ), x_a ), combs( state, bool, bool ) ), hAPP( fun( x_a, fun( state, bool
% 0.89/1.37 ) ), fun( x_a, fun( state, fun( bool, bool ) ) ), hAPP( fun( fun( state
% 0.89/1.37 , bool ), fun( state, fun( bool, bool ) ) ), fun( fun( x_a, fun( state,
% 0.89/1.37 bool ) ), fun( x_a, fun( state, fun( bool, bool ) ) ) ), combb( fun(
% 0.89/1.37 state, bool ), fun( state, fun( bool, bool ) ), x_a ), hAPP( fun( bool,
% 0.89/1.37 fun( bool, bool ) ), fun( fun( state, bool ), fun( state, fun( bool, bool
% 0.89/1.37 ) ) ), combb( bool, fun( bool, bool ), state ), fconj ) ), p ) ) ), hAPP
% 0.89/1.37 ( fun( state, bool ), fun( state, bool ), hAPP( fun( bool, bool ), fun(
% 0.89/1.37 fun( state, bool ), fun( state, bool ) ), combb( bool, bool, state ),
% 0.89/1.37 fNot ), b ) ) ) ), bot_bot( fun( hoare_509422987triple( x_a ), bool ) ) )
% 0.89/1.37 ) ) }.
% 0.89/1.37
% 0.89/1.37 *** allocated 15000 integers for clauses
% 0.89/1.37 *** allocated 22500 integers for clauses
% 0.89/1.37 *** allocated 33750 integers for clauses
% 0.89/1.37 percentage equality = 0.352823, percentage horn = 0.807377
% 0.89/1.37 This is a problem with some equality
% 0.89/1.37
% 0.89/1.37
% 0.89/1.37
% 0.89/1.37 Options Used:
% 0.89/1.37
% 0.89/1.37 useres = 1
% 0.89/1.37 useparamod = 1
% 0.89/1.37 useeqrefl = 1
% 0.89/1.37 useeqfact = 1
% 0.89/1.37 usefactor = 1
% 0.89/1.37 usesimpsplitting = 0
% 0.89/1.37 usesimpdemod = 5
% 0.89/1.37 usesimpres = 3
% 0.89/1.37
% 0.89/1.37 resimpinuse = 1000
% 0.89/1.37 resimpclauses = 20000
% 0.89/1.37 substype = eqrewr
% 0.89/1.37 backwardsubs = 1
% 0.89/1.37 selectoldest = 5
% 0.89/1.37
% 0.89/1.37 litorderings [0] = split
% 0.89/1.37 litorderings [1] = extend the termordering, first sorting on arguments
% 0.89/1.37
% 0.89/1.37 termordering = kbo
% 0.89/1.37
% 0.89/1.37 litapriori = 0
% 0.89/1.37 termapriori = 1
% 0.89/1.37 litaposteriori = 0
% 0.89/1.37 termaposteriori = 0
% 0.89/1.37 demodaposteriori = 0
% 0.89/1.37 ordereqreflfact = 0
% 0.89/1.37
% 0.89/1.37 litselect = negord
% 0.89/1.37
% 0.89/1.37 maxweight = 15
% 0.89/1.37 maxdepth = 30000
% 0.89/1.37 maxlength = 115
% 0.89/1.37 maxnrvars = 195
% 0.89/1.37 excuselevel = 1
% 0.89/1.37 increasemaxweight = 1
% 0.89/1.37
% 0.89/1.37 maxselected = 10000000
% 0.89/1.37 maxnrclauses = 10000000
% 0.89/1.37
% 0.89/1.37 showgenerated = 0
% 0.89/1.37 showkept = 0
% 0.89/1.37 showselected = 0
% 0.89/1.37 showdeleted = 0
% 0.89/1.37 showresimp = 1
% 0.89/1.37 showstatus = 2000
% 0.89/1.37
% 0.89/1.37 prologoutput = 0
% 0.89/1.37 nrgoals = 5000000
% 0.89/1.37 totalproof = 1
% 0.89/1.37
% 0.89/1.37 Symbols occurring in the translation:
% 0.89/1.37
% 0.89/1.37 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 0.89/1.37 . [1, 2] (w:1, o:115, a:1, s:1, b:0),
% 0.89/1.37 ! [4, 1] (w:0, o:91, a:1, s:1, b:0),
% 0.89/1.37 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.89/1.37 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 0.89/1.37 fun [38, 2] (w:1, o:139, a:1, s:1, b:0),
% 0.89/1.37 combb [39, 3] (w:1, o:164, a:1, s:1, b:0),
% 2.57/2.94 ti [40, 2] (w:1, o:157, a:1, s:1, b:0),
% 2.57/2.94 combc [41, 3] (w:1, o:165, a:1, s:1, b:0),
% 2.57/2.94 combk [42, 2] (w:1, o:158, a:1, s:1, b:0),
% 2.57/2.94 combs [43, 3] (w:1, o:166, a:1, s:1, b:0),
% 2.57/2.94 com [44, 0] (w:1, o:11, a:1, s:1, b:0),
% 2.57/2.94 skip [45, 0] (w:1, o:12, a:1, s:1, b:0),
% 2.57/2.94 semi [46, 0] (w:1, o:13, a:1, s:1, b:0),
% 2.57/2.94 bool [47, 0] (w:1, o:9, a:1, s:1, b:0),
% 2.57/2.94 finite_finite_1 [48, 1] (w:1, o:96, a:1, s:1, b:0),
% 2.57/2.94 finite_fold1 [49, 1] (w:1, o:97, a:1, s:1, b:0),
% 2.57/2.94 finite_fold1Set [50, 1] (w:1, o:98, a:1, s:1, b:0),
% 2.57/2.94 finite_fold_graph [51, 2] (w:1, o:159, a:1, s:1, b:0),
% 2.57/2.94 finite_folding_one [52, 1] (w:1, o:99, a:1, s:1, b:0),
% 2.57/2.94 finite2073411215e_idem [53, 1] (w:1, o:100, a:1, s:1, b:0),
% 2.57/2.94 the [54, 1] (w:1, o:101, a:1, s:1, b:0),
% 2.57/2.94 undefined [55, 1] (w:1, o:103, a:1, s:1, b:0),
% 2.57/2.94 hoare_509422987triple [56, 1] (w:1, o:104, a:1, s:1, b:0),
% 2.57/2.94 hoare_122391849derivs [57, 1] (w:1, o:105, a:1, s:1, b:0),
% 2.57/2.94 state [58, 0] (w:1, o:14, a:1, s:1, b:0),
% 2.57/2.94 hoare_1008221573triple [59, 1] (w:1, o:106, a:1, s:1, b:0),
% 2.57/2.94 hoare_885240885e_case [60, 2] (w:1, o:161, a:1, s:1, b:0),
% 2.57/2.94 hoare_728318379le_rec [61, 2] (w:1, o:160, a:1, s:1, b:0),
% 2.57/2.94 bot [62, 1] (w:1, o:107, a:1, s:1, b:0),
% 2.57/2.94 bot_bot [63, 1] (w:1, o:108, a:1, s:1, b:0),
% 2.57/2.94 collect [64, 1] (w:1, o:109, a:1, s:1, b:0),
% 2.57/2.94 insert [65, 1] (w:1, o:111, a:1, s:1, b:0),
% 2.57/2.94 the_elem [66, 1] (w:1, o:102, a:1, s:1, b:0),
% 2.57/2.94 fFalse [67, 0] (w:1, o:15, a:1, s:1, b:0),
% 2.57/2.94 fNot [68, 0] (w:1, o:16, a:1, s:1, b:0),
% 2.57/2.94 fTrue [69, 0] (w:1, o:17, a:1, s:1, b:0),
% 2.57/2.94 fconj [70, 0] (w:1, o:18, a:1, s:1, b:0),
% 2.57/2.94 fdisj [71, 0] (w:1, o:19, a:1, s:1, b:0),
% 2.57/2.94 fequal [72, 1] (w:1, o:112, a:1, s:1, b:0),
% 2.57/2.94 fimplies [73, 0] (w:1, o:20, a:1, s:1, b:0),
% 2.57/2.94 hAPP [76, 4] (w:1, o:182, a:1, s:1, b:0),
% 2.57/2.94 hBOOL [77, 1] (w:1, o:110, a:1, s:1, b:0),
% 2.57/2.94 member [78, 1] (w:1, o:113, a:1, s:1, b:0),
% 2.57/2.94 x_a [79, 0] (w:1, o:31, a:1, s:1, b:0),
% 2.57/2.94 g [80, 0] (w:1, o:32, a:1, s:1, b:0),
% 2.57/2.94 p [81, 0] (w:1, o:33, a:1, s:1, b:0),
% 2.57/2.94 b [82, 0] (w:1, o:10, a:1, s:1, b:0),
% 2.57/2.94 c [83, 0] (w:1, o:34, a:1, s:1, b:0),
% 2.57/2.94 finite_finite [133, 1] (w:1, o:114, a:1, s:1, b:0),
% 2.57/2.94 alpha1 [149, 4] (w:1, o:183, a:1, s:1, b:1),
% 2.57/2.94 alpha2 [150, 5] (w:1, o:187, a:1, s:1, b:1),
% 2.57/2.94 alpha3 [151, 2] (w:1, o:162, a:1, s:1, b:1),
% 2.57/2.94 alpha4 [152, 5] (w:1, o:188, a:1, s:1, b:1),
% 2.57/2.94 alpha5 [153, 5] (w:1, o:189, a:1, s:1, b:1),
% 2.57/2.94 alpha6 [154, 5] (w:1, o:190, a:1, s:1, b:1),
% 2.57/2.94 alpha7 [155, 5] (w:1, o:191, a:1, s:1, b:1),
% 2.57/2.94 alpha8 [156, 6] (w:1, o:203, a:1, s:1, b:1),
% 2.57/2.94 alpha9 [157, 7] (w:1, o:206, a:1, s:1, b:1),
% 2.57/2.94 alpha10 [158, 7] (w:1, o:207, a:1, s:1, b:1),
% 2.57/2.94 alpha11 [159, 3] (w:1, o:167, a:1, s:1, b:1),
% 2.57/2.94 alpha12 [160, 2] (w:1, o:163, a:1, s:1, b:1),
% 2.57/2.94 alpha13 [161, 3] (w:1, o:168, a:1, s:1, b:1),
% 2.57/2.94 skol1 [162, 5] (w:1, o:192, a:1, s:1, b:1),
% 2.57/2.94 skol2 [163, 3] (w:1, o:175, a:1, s:1, b:1),
% 2.57/2.94 skol3 [164, 3] (w:1, o:178, a:1, s:1, b:1),
% 2.57/2.94 skol4 [165, 5] (w:1, o:196, a:1, s:1, b:1),
% 2.57/2.94 skol5 [166, 2] (w:1, o:144, a:1, s:1, b:1),
% 2.57/2.94 skol6 [167, 2] (w:1, o:145, a:1, s:1, b:1),
% 2.57/2.94 skol7 [168, 2] (w:1, o:146, a:1, s:1, b:1),
% 2.57/2.94 skol8 [169, 2] (w:1, o:147, a:1, s:1, b:1),
% 2.57/2.94 skol9 [170, 2] (w:1, o:148, a:1, s:1, b:1),
% 2.57/2.94 skol10 [171, 3] (w:1, o:169, a:1, s:1, b:1),
% 2.57/2.94 skol11 [172, 3] (w:1, o:170, a:1, s:1, b:1),
% 2.57/2.94 skol12 [173, 2] (w:1, o:149, a:1, s:1, b:1),
% 2.57/2.94 skol13 [174, 3] (w:1, o:171, a:1, s:1, b:1),
% 2.57/2.94 skol14 [175, 3] (w:1, o:172, a:1, s:1, b:1),
% 2.57/2.94 skol15 [176, 3] (w:1, o:173, a:1, s:1, b:1),
% 2.57/2.94 skol16 [177, 3] (w:1, o:174, a:1, s:1, b:1),
% 2.57/2.94 skol17 [178, 5] (w:1, o:197, a:1, s:1, b:1),
% 2.57/2.94 skol18 [179, 2] (w:1, o:150, a:1, s:1, b:1),
% 2.57/2.94 skol19 [180, 4] (w:1, o:184, a:1, s:1, b:1),
% 2.57/2.94 skol20 [181, 2] (w:1, o:151, a:1, s:1, b:1),
% 2.57/2.94 skol21 [182, 5] (w:1, o:198, a:1, s:1, b:1),
% 2.57/2.94 skol22 [183, 3] (w:1, o:176, a:1, s:1, b:1),
% 12.15/12.58 skol23 [184, 2] (w:1, o:152, a:1, s:1, b:1),
% 12.15/12.58 skol24 [185, 3] (w:1, o:177, a:1, s:1, b:1),
% 12.15/12.58 skol25 [186, 2] (w:1, o:153, a:1, s:1, b:1),
% 12.15/12.58 skol26 [187, 5] (w:1, o:199, a:1, s:1, b:1),
% 12.15/12.58 skol27 [188, 4] (w:1, o:185, a:1, s:1, b:1),
% 12.15/12.58 skol28 [189, 5] (w:1, o:200, a:1, s:1, b:1),
% 12.15/12.58 skol29 [190, 6] (w:1, o:204, a:1, s:1, b:1),
% 12.15/12.58 skol30 [191, 7] (w:1, o:208, a:1, s:1, b:1),
% 12.15/12.58 skol31 [192, 2] (w:1, o:154, a:1, s:1, b:1),
% 12.15/12.58 skol32 [193, 3] (w:1, o:179, a:1, s:1, b:1),
% 12.15/12.58 skol33 [194, 5] (w:1, o:193, a:1, s:1, b:1),
% 12.15/12.58 skol34 [195, 3] (w:1, o:180, a:1, s:1, b:1),
% 12.15/12.58 skol35 [196, 3] (w:1, o:181, a:1, s:1, b:1),
% 12.15/12.58 skol36 [197, 5] (w:1, o:194, a:1, s:1, b:1),
% 12.15/12.58 skol37 [198, 2] (w:1, o:155, a:1, s:1, b:1),
% 12.15/12.58 skol38 [199, 5] (w:1, o:195, a:1, s:1, b:1),
% 12.15/12.58 skol39 [200, 2] (w:1, o:156, a:1, s:1, b:1),
% 12.15/12.58 skol40 [201, 2] (w:1, o:140, a:1, s:1, b:1),
% 12.15/12.58 skol41 [202, 5] (w:1, o:201, a:1, s:1, b:1),
% 12.15/12.58 skol42 [203, 2] (w:1, o:141, a:1, s:1, b:1),
% 12.15/12.58 skol43 [204, 4] (w:1, o:186, a:1, s:1, b:1),
% 12.15/12.58 skol44 [205, 6] (w:1, o:205, a:1, s:1, b:1),
% 12.15/12.58 skol45 [206, 2] (w:1, o:142, a:1, s:1, b:1),
% 12.15/12.58 skol46 [207, 5] (w:1, o:202, a:1, s:1, b:1),
% 12.15/12.58 skol47 [208, 2] (w:1, o:143, a:1, s:1, b:1),
% 12.15/12.58 skol48 [209, 7] (w:1, o:209, a:1, s:1, b:1).
% 12.15/12.58
% 12.15/12.58
% 12.15/12.58 Starting Search:
% 12.15/12.58
% 12.15/12.58 *** allocated 50625 integers for clauses
% 12.15/12.58 *** allocated 75937 integers for clauses
% 12.15/12.58 *** allocated 113905 integers for clauses
% 12.15/12.58 *** allocated 75937 integers for termspace/termends
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 *** allocated 170857 integers for clauses
% 12.15/12.58
% 12.15/12.58 Intermediate Status:
% 12.15/12.58 Generated: 3330
% 12.15/12.58 Kept: 2000
% 12.15/12.58 Inuse: 139
% 12.15/12.58 Deleted: 12
% 12.15/12.58 Deletedinuse: 8
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 *** allocated 113905 integers for termspace/termends
% 12.15/12.58 *** allocated 256285 integers for clauses
% 12.15/12.58 *** allocated 170857 integers for termspace/termends
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 *** allocated 384427 integers for clauses
% 12.15/12.58
% 12.15/12.58 Intermediate Status:
% 12.15/12.58 Generated: 10250
% 12.15/12.58 Kept: 4002
% 12.15/12.58 Inuse: 246
% 12.15/12.58 Deleted: 38
% 12.15/12.58 Deletedinuse: 12
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 *** allocated 256285 integers for termspace/termends
% 12.15/12.58 *** allocated 576640 integers for clauses
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 *** allocated 384427 integers for termspace/termends
% 12.15/12.58
% 12.15/12.58 Intermediate Status:
% 12.15/12.58 Generated: 16474
% 12.15/12.58 Kept: 6002
% 12.15/12.58 Inuse: 351
% 12.15/12.58 Deleted: 54
% 12.15/12.58 Deletedinuse: 13
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 *** allocated 864960 integers for clauses
% 12.15/12.58
% 12.15/12.58 Intermediate Status:
% 12.15/12.58 Generated: 24182
% 12.15/12.58 Kept: 8109
% 12.15/12.58 Inuse: 382
% 12.15/12.58 Deleted: 58
% 12.15/12.58 Deletedinuse: 13
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58
% 12.15/12.58 Intermediate Status:
% 12.15/12.58 Generated: 32721
% 12.15/12.58 Kept: 10685
% 12.15/12.58 Inuse: 406
% 12.15/12.58 Deleted: 68
% 12.15/12.58 Deletedinuse: 22
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 *** allocated 576640 integers for termspace/termends
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58
% 12.15/12.58 Intermediate Status:
% 12.15/12.58 Generated: 43994
% 12.15/12.58 Kept: 12691
% 12.15/12.58 Inuse: 465
% 12.15/12.58 Deleted: 73
% 12.15/12.58 Deletedinuse: 22
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 *** allocated 1297440 integers for clauses
% 12.15/12.58 *** allocated 864960 integers for termspace/termends
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58
% 12.15/12.58 Intermediate Status:
% 12.15/12.58 Generated: 58174
% 12.15/12.58 Kept: 14697
% 12.15/12.58 Inuse: 509
% 12.15/12.58 Deleted: 74
% 12.15/12.58 Deletedinuse: 22
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58
% 12.15/12.58 Intermediate Status:
% 12.15/12.58 Generated: 64571
% 12.15/12.58 Kept: 16733
% 12.15/12.58 Inuse: 538
% 12.15/12.58 Deleted: 76
% 12.15/12.58 Deletedinuse: 22
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58
% 12.15/12.58 Intermediate Status:
% 12.15/12.58 Generated: 70054
% 12.15/12.58 Kept: 18764
% 12.15/12.58 Inuse: 559
% 12.15/12.58 Deleted: 79
% 12.15/12.58 Deletedinuse: 22
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 Resimplifying clauses:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58
% 12.15/12.58 Intermediate Status:
% 12.15/12.58 Generated: 77345
% 12.15/12.58 Kept: 20831
% 12.15/12.58 Inuse: 590
% 12.15/12.58 Deleted: 402
% 12.15/12.58 Deletedinuse: 22
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58 *** allocated 1946160 integers for clauses
% 12.15/12.58 *** allocated 1297440 integers for termspace/termends
% 12.15/12.58 Resimplifying inuse:
% 12.15/12.58 Done
% 12.15/12.58
% 12.15/12.58
% 12.15/12.58 Intermediate Status:
% 12.15/12.58 Generated: 85544
% 12.15/12.58 Kept: 22980
% 12.15/12.58 Inuse: 629
% 12.15/12.58 Deleted: 408
% 12.15/12.58 Deletedinuse: 22
% 12.15/12.58
% 12.15/12.58 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 97072
% 35.53/35.95 Kept: 24991
% 35.53/35.95 Inuse: 670
% 35.53/35.95 Deleted: 408
% 35.53/35.95 Deletedinuse: 22
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 109223
% 35.53/35.95 Kept: 27032
% 35.53/35.95 Inuse: 703
% 35.53/35.95 Deleted: 417
% 35.53/35.95 Deletedinuse: 22
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 118690
% 35.53/35.95 Kept: 29135
% 35.53/35.95 Inuse: 756
% 35.53/35.95 Deleted: 421
% 35.53/35.95 Deletedinuse: 22
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 *** allocated 1946160 integers for termspace/termends
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 127036
% 35.53/35.95 Kept: 31168
% 35.53/35.95 Inuse: 798
% 35.53/35.95 Deleted: 421
% 35.53/35.95 Deletedinuse: 22
% 35.53/35.95
% 35.53/35.95 *** allocated 2919240 integers for clauses
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 132565
% 35.53/35.95 Kept: 33281
% 35.53/35.95 Inuse: 809
% 35.53/35.95 Deleted: 421
% 35.53/35.95 Deletedinuse: 22
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 139690
% 35.53/35.95 Kept: 35373
% 35.53/35.95 Inuse: 823
% 35.53/35.95 Deleted: 421
% 35.53/35.95 Deletedinuse: 22
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 148092
% 35.53/35.95 Kept: 37573
% 35.53/35.95 Inuse: 871
% 35.53/35.95 Deleted: 421
% 35.53/35.95 Deletedinuse: 22
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 158550
% 35.53/35.95 Kept: 39587
% 35.53/35.95 Inuse: 881
% 35.53/35.95 Deleted: 421
% 35.53/35.95 Deletedinuse: 22
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying clauses:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 171253
% 35.53/35.95 Kept: 41906
% 35.53/35.95 Inuse: 953
% 35.53/35.95 Deleted: 1296
% 35.53/35.95 Deletedinuse: 22
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 178923
% 35.53/35.95 Kept: 44041
% 35.53/35.95 Inuse: 983
% 35.53/35.95 Deleted: 1324
% 35.53/35.95 Deletedinuse: 50
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 188301
% 35.53/35.95 Kept: 46064
% 35.53/35.95 Inuse: 1033
% 35.53/35.95 Deleted: 1479
% 35.53/35.95 Deletedinuse: 198
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 200731
% 35.53/35.95 Kept: 48242
% 35.53/35.95 Inuse: 1125
% 35.53/35.95 Deleted: 1539
% 35.53/35.95 Deletedinuse: 238
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 *** allocated 4378860 integers for clauses
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 213628
% 35.53/35.95 Kept: 50604
% 35.53/35.95 Inuse: 1185
% 35.53/35.95 Deleted: 1581
% 35.53/35.95 Deletedinuse: 276
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 *** allocated 2919240 integers for termspace/termends
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 224802
% 35.53/35.95 Kept: 52605
% 35.53/35.95 Inuse: 1225
% 35.53/35.95 Deleted: 1625
% 35.53/35.95 Deletedinuse: 276
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 230915
% 35.53/35.95 Kept: 54701
% 35.53/35.95 Inuse: 1275
% 35.53/35.95 Deleted: 1627
% 35.53/35.95 Deletedinuse: 276
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 236178
% 35.53/35.95 Kept: 56724
% 35.53/35.95 Inuse: 1313
% 35.53/35.95 Deleted: 1629
% 35.53/35.95 Deletedinuse: 276
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 242287
% 35.53/35.95 Kept: 58736
% 35.53/35.95 Inuse: 1356
% 35.53/35.95 Deleted: 1636
% 35.53/35.95 Deletedinuse: 276
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying clauses:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 253051
% 35.53/35.95 Kept: 60777
% 35.53/35.95 Inuse: 1394
% 35.53/35.95 Deleted: 14817
% 35.53/35.95 Deletedinuse: 276
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 258454
% 35.53/35.95 Kept: 62786
% 35.53/35.95 Inuse: 1429
% 35.53/35.95 Deleted: 14823
% 35.53/35.95 Deletedinuse: 282
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 266526
% 35.53/35.95 Kept: 64799
% 35.53/35.95 Inuse: 1491
% 35.53/35.95 Deleted: 14825
% 35.53/35.95 Deletedinuse: 284
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 272617
% 35.53/35.95 Kept: 66800
% 35.53/35.95 Inuse: 1531
% 35.53/35.95 Deleted: 14825
% 35.53/35.95 Deletedinuse: 284
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 35.53/35.95 Generated: 278949
% 35.53/35.95 Kept: 68814
% 35.53/35.95 Inuse: 1560
% 35.53/35.95 Deleted: 14825
% 35.53/35.95 Deletedinuse: 284
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95 Resimplifying inuse:
% 35.53/35.95 Done
% 35.53/35.95
% 35.53/35.95
% 35.53/35.95 Intermediate Status:
% 92.57/92.95 Generated: 285192
% 92.57/92.95 Kept: 70879
% 92.57/92.95 Inuse: 1590
% 92.57/92.95 Deleted: 14825
% 92.57/92.95 Deletedinuse: 284
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 292753
% 92.57/92.95 Kept: 72932
% 92.57/92.95 Inuse: 1629
% 92.57/92.95 Deleted: 14825
% 92.57/92.95 Deletedinuse: 284
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 307102
% 92.57/92.95 Kept: 75035
% 92.57/92.95 Inuse: 1641
% 92.57/92.95 Deleted: 14825
% 92.57/92.95 Deletedinuse: 284
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 316316
% 92.57/92.95 Kept: 77116
% 92.57/92.95 Inuse: 1664
% 92.57/92.95 Deleted: 14825
% 92.57/92.95 Deletedinuse: 284
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 331287
% 92.57/92.95 Kept: 79118
% 92.57/92.95 Inuse: 1771
% 92.57/92.95 Deleted: 14827
% 92.57/92.95 Deletedinuse: 286
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying clauses:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 350324
% 92.57/92.95 Kept: 81529
% 92.57/92.95 Inuse: 1785
% 92.57/92.95 Deleted: 17034
% 92.57/92.95 Deletedinuse: 290
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 364538
% 92.57/92.95 Kept: 83553
% 92.57/92.95 Inuse: 1804
% 92.57/92.95 Deleted: 17039
% 92.57/92.95 Deletedinuse: 295
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 375284
% 92.57/92.95 Kept: 85555
% 92.57/92.95 Inuse: 1827
% 92.57/92.95 Deleted: 17044
% 92.57/92.95 Deletedinuse: 300
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 384082
% 92.57/92.95 Kept: 87652
% 92.57/92.95 Inuse: 1838
% 92.57/92.95 Deleted: 17044
% 92.57/92.95 Deletedinuse: 300
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 389266
% 92.57/92.95 Kept: 89783
% 92.57/92.95 Inuse: 1860
% 92.57/92.95 Deleted: 17044
% 92.57/92.95 Deletedinuse: 300
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 *** allocated 6568290 integers for clauses
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 394850
% 92.57/92.95 Kept: 91852
% 92.57/92.95 Inuse: 1888
% 92.57/92.95 Deleted: 17044
% 92.57/92.95 Deletedinuse: 300
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 400466
% 92.57/92.95 Kept: 93907
% 92.57/92.95 Inuse: 1908
% 92.57/92.95 Deleted: 17044
% 92.57/92.95 Deletedinuse: 300
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 409603
% 92.57/92.95 Kept: 95993
% 92.57/92.95 Inuse: 1940
% 92.57/92.95 Deleted: 17044
% 92.57/92.95 Deletedinuse: 300
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 417276
% 92.57/92.95 Kept: 98000
% 92.57/92.95 Inuse: 1971
% 92.57/92.95 Deleted: 17044
% 92.57/92.95 Deletedinuse: 300
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 433925
% 92.57/92.95 Kept: 100041
% 92.57/92.95 Inuse: 2045
% 92.57/92.95 Deleted: 17060
% 92.57/92.95 Deletedinuse: 316
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying clauses:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 457143
% 92.57/92.95 Kept: 102145
% 92.57/92.95 Inuse: 2104
% 92.57/92.95 Deleted: 19801
% 92.57/92.95 Deletedinuse: 344
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 497872
% 92.57/92.95 Kept: 104150
% 92.57/92.95 Inuse: 2135
% 92.57/92.95 Deleted: 19824
% 92.57/92.95 Deletedinuse: 359
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 528603
% 92.57/92.95 Kept: 106191
% 92.57/92.95 Inuse: 2180
% 92.57/92.95 Deleted: 19839
% 92.57/92.95 Deletedinuse: 366
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 539365
% 92.57/92.95 Kept: 108201
% 92.57/92.95 Inuse: 2224
% 92.57/92.95 Deleted: 19839
% 92.57/92.95 Deletedinuse: 366
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 551370
% 92.57/92.95 Kept: 110245
% 92.57/92.95 Inuse: 2258
% 92.57/92.95 Deleted: 19855
% 92.57/92.95 Deletedinuse: 366
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 567930
% 92.57/92.95 Kept: 112405
% 92.57/92.95 Inuse: 2290
% 92.57/92.95 Deleted: 19855
% 92.57/92.95 Deletedinuse: 366
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 595829
% 92.57/92.95 Kept: 114406
% 92.57/92.95 Inuse: 2323
% 92.57/92.95 Deleted: 19855
% 92.57/92.95 Deletedinuse: 366
% 92.57/92.95
% 92.57/92.95 *** allocated 4378860 integers for termspace/termends
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95
% 92.57/92.95 Intermediate Status:
% 92.57/92.95 Generated: 626568
% 92.57/92.95 Kept: 116433
% 92.57/92.95 Inuse: 2364
% 92.57/92.95 Deleted: 19855
% 92.57/92.95 Deletedinuse: 366
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 92.57/92.95 Done
% 92.57/92.95
% 92.57/92.95 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 638714
% 231.52/231.93 Kept: 118459
% 231.52/231.93 Inuse: 2397
% 231.52/231.93 Deleted: 19855
% 231.52/231.93 Deletedinuse: 366
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 648156
% 231.52/231.93 Kept: 120485
% 231.52/231.93 Inuse: 2424
% 231.52/231.93 Deleted: 19855
% 231.52/231.93 Deletedinuse: 366
% 231.52/231.93
% 231.52/231.93 Resimplifying clauses:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 661033
% 231.52/231.93 Kept: 122555
% 231.52/231.93 Inuse: 2462
% 231.52/231.93 Deleted: 21836
% 231.52/231.93 Deletedinuse: 366
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 677553
% 231.52/231.93 Kept: 124876
% 231.52/231.93 Inuse: 2469
% 231.52/231.93 Deleted: 21836
% 231.52/231.93 Deletedinuse: 366
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 687172
% 231.52/231.93 Kept: 126918
% 231.52/231.93 Inuse: 2508
% 231.52/231.93 Deleted: 21837
% 231.52/231.93 Deletedinuse: 367
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 692237
% 231.52/231.93 Kept: 128958
% 231.52/231.93 Inuse: 2546
% 231.52/231.93 Deleted: 22046
% 231.52/231.93 Deletedinuse: 576
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 698371
% 231.52/231.93 Kept: 131029
% 231.52/231.93 Inuse: 2567
% 231.52/231.93 Deleted: 22046
% 231.52/231.93 Deletedinuse: 576
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 717664
% 231.52/231.93 Kept: 133786
% 231.52/231.93 Inuse: 2579
% 231.52/231.93 Deleted: 22046
% 231.52/231.93 Deletedinuse: 576
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 726777
% 231.52/231.93 Kept: 135928
% 231.52/231.93 Inuse: 2598
% 231.52/231.93 Deleted: 22046
% 231.52/231.93 Deletedinuse: 576
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 736462
% 231.52/231.93 Kept: 138033
% 231.52/231.93 Inuse: 2617
% 231.52/231.93 Deleted: 22046
% 231.52/231.93 Deletedinuse: 576
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 822757
% 231.52/231.93 Kept: 140268
% 231.52/231.93 Inuse: 2876
% 231.52/231.93 Deleted: 22049
% 231.52/231.93 Deletedinuse: 579
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying clauses:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 832908
% 231.52/231.93 Kept: 142384
% 231.52/231.93 Inuse: 2894
% 231.52/231.93 Deleted: 33995
% 231.52/231.93 Deletedinuse: 579
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 844855
% 231.52/231.93 Kept: 144403
% 231.52/231.93 Inuse: 2919
% 231.52/231.93 Deleted: 33995
% 231.52/231.93 Deletedinuse: 579
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 856331
% 231.52/231.93 Kept: 146650
% 231.52/231.93 Inuse: 2944
% 231.52/231.93 Deleted: 33995
% 231.52/231.93 Deletedinuse: 579
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 863977
% 231.52/231.93 Kept: 148724
% 231.52/231.93 Inuse: 2953
% 231.52/231.93 Deleted: 33995
% 231.52/231.93 Deletedinuse: 579
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 *** allocated 9852435 integers for clauses
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 879061
% 231.52/231.93 Kept: 151123
% 231.52/231.93 Inuse: 2962
% 231.52/231.93 Deleted: 33995
% 231.52/231.93 Deletedinuse: 579
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 903991
% 231.52/231.93 Kept: 153430
% 231.52/231.93 Inuse: 2995
% 231.52/231.93 Deleted: 34007
% 231.52/231.93 Deletedinuse: 583
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 921838
% 231.52/231.93 Kept: 155440
% 231.52/231.93 Inuse: 3013
% 231.52/231.93 Deleted: 34023
% 231.52/231.93 Deletedinuse: 591
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 963284
% 231.52/231.93 Kept: 157871
% 231.52/231.93 Inuse: 3035
% 231.52/231.93 Deleted: 34028
% 231.52/231.93 Deletedinuse: 596
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 997878
% 231.52/231.93 Kept: 159903
% 231.52/231.93 Inuse: 3043
% 231.52/231.93 Deleted: 34034
% 231.52/231.93 Deletedinuse: 600
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying clauses:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 1027962
% 231.52/231.93 Kept: 161906
% 231.52/231.93 Inuse: 3057
% 231.52/231.93 Deleted: 37031
% 231.52/231.93 Deletedinuse: 629
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 1039368
% 231.52/231.93 Kept: 163968
% 231.52/231.93 Inuse: 3076
% 231.52/231.93 Deleted: 37057
% 231.52/231.93 Deletedinuse: 655
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93 Resimplifying inuse:
% 231.52/231.93 Done
% 231.52/231.93
% 231.52/231.93
% 231.52/231.93 Intermediate Status:
% 231.52/231.93 Generated: 1059118
% 231.52/231.93 Kept: 166025
% 231.52/231.93 Inuse: 3092
% 231.52/231.93 Deleted: 3705Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------