%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : SWW470^1 : TPTP v9.2.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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 : 300s
% DateTime : Wed Feb 25 09:48:05 AM UTC 2026
% Result : Theorem 6.40s 2.43s
% Output : Refutation 6.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 6
% Syntax : Number of formulae : 39 ( 17 unt; 0 typ; 0 def)
% Number of atoms : 321 ( 61 equ; 0 cnn)
% Maximal formula atoms : 7 ( 8 avg)
% Number of connectives : 513 ( 36 ~; 18 |; 24 &; 419 @)
% ( 0 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Number of types : 5 ( 4 usr)
% Number of type conns : 100 ( 100 >; 0 *; 0 +; 0 <<)
% Number of symbols : 74 ( 71 usr; 4 con; 0-6 aty)
% Number of variables : 171 ( 75 ^; 90 !; 6 ?; 171 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
com: $tType ).
thf(type_def_7,type,
hoare_669141180iple_a: $tType ).
thf(type_def_8,type,
x_a: $tType ).
thf(type_def_9,type,
state: $tType ).
thf(func_def_0,type,
x_a: $tType ).
thf(func_def_1,type,
com: $tType ).
thf(func_def_2,type,
state: $tType ).
thf(func_def_3,type,
hoare_669141180iple_a: $tType ).
thf(func_def_4,type,
skip: com ).
thf(func_def_5,type,
semi: com > com > com ).
thf(func_def_6,type,
ex: ( hoare_669141180iple_a > $o ) > $o ).
thf(func_def_7,type,
finite957651855iple_a: ( hoare_669141180iple_a > $o ) > $o ).
thf(func_def_8,type,
finite840267660iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
thf(func_def_9,type,
finite684844060iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_10,type,
finite590756294iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
thf(func_def_11,type,
finite972428089iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ) > $o ).
thf(func_def_12,type,
finite252461622iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ) > $o ).
thf(func_def_13,type,
the_Ho49089901iple_a: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_14,type,
hoare_2128652938rivs_a: ( hoare_669141180iple_a > $o ) > ( hoare_669141180iple_a > $o ) > $o ).
thf(func_def_15,type,
hoare_1295064928iple_a: ( x_a > state > $o ) > com > ( x_a > state > $o ) > hoare_669141180iple_a ).
thf(func_def_16,type,
bot_bo280939947le_a_o: hoare_669141180iple_a > $o ).
thf(func_def_18,type,
collec1717965009iple_a: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
thf(func_def_19,type,
insert175534902iple_a: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
thf(func_def_20,type,
the_el738790235iple_a: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_21,type,
fequal182287803iple_a: hoare_669141180iple_a > hoare_669141180iple_a > $o ).
thf(func_def_22,type,
member1016246415iple_a: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > $o ).
thf(func_def_23,type,
g: hoare_669141180iple_a > $o ).
thf(func_def_24,type,
p: x_a > state > $o ).
thf(func_def_25,type,
b: state > $o ).
thf(func_def_26,type,
c: com ).
thf(func_def_38,type,
sK0:
!>[X0: $tType] : ( ( X0 > $o ) > X0 ) ).
thf(func_def_39,type,
sK1:
!>[X0: $tType] : ( ( X0 > $o ) > X0 ) ).
thf(func_def_42,type,
sP2: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a > hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > $o ).
thf(func_def_43,type,
sK3: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a > $o ).
thf(func_def_44,type,
sK4: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a ).
thf(func_def_45,type,
sK5: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_46,type,
sK6: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > hoare_669141180iple_a ).
thf(func_def_47,type,
sK7: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_48,type,
sK8: ( x_a > state > $o ) > com > ( x_a > state > $o ) > ( hoare_669141180iple_a > $o ) > state ).
thf(func_def_49,type,
sK9: ( x_a > state > $o ) > com > ( x_a > state > $o ) > ( hoare_669141180iple_a > $o ) > x_a ).
thf(func_def_50,type,
sK10: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
thf(func_def_51,type,
sK11: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_52,type,
sK12: ( x_a > state > $o ) > ( x_a > state > $o ) > state ).
thf(func_def_53,type,
sK13: ( x_a > state > $o ) > ( x_a > state > $o ) > x_a ).
thf(func_def_54,type,
sK14: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_55,type,
sK15: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a ).
thf(func_def_56,type,
sK16: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a ).
thf(func_def_57,type,
sK17: hoare_669141180iple_a > com ).
thf(func_def_58,type,
sK18: hoare_669141180iple_a > x_a > state > $o ).
thf(func_def_59,type,
sK19: hoare_669141180iple_a > x_a > state > $o ).
thf(func_def_60,type,
sK20: ( ( hoare_669141180iple_a > $o ) > $o ) > hoare_669141180iple_a > $o ).
thf(func_def_61,type,
sK21: ( ( hoare_669141180iple_a > $o ) > $o ) > hoare_669141180iple_a ).
thf(func_def_62,type,
sK22: com > ( hoare_669141180iple_a > $o ) > ( x_a > state > $o ) > ( x_a > state > $o ) > state ).
thf(func_def_63,type,
sK23: com > ( hoare_669141180iple_a > $o ) > ( x_a > state > $o ) > ( x_a > state > $o ) > x_a ).
thf(func_def_64,type,
sK24: ( x_a > state > $o ) > ( x_a > state > $o ) > com > ( hoare_669141180iple_a > $o ) > ( x_a > state > $o ) > ( x_a > state > $o ) > state ).
thf(func_def_65,type,
sK25: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_66,type,
sK26: ( x_a > state > $o ) > ( x_a > state > $o ) > state ).
thf(func_def_67,type,
sK27: ( x_a > state > $o ) > ( x_a > state > $o ) > x_a ).
thf(func_def_68,type,
sK28: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_69,type,
sK29: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
thf(func_def_70,type,
sK30: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_71,type,
sK31: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_72,type,
sK32: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_73,type,
sK33: ( ( hoare_669141180iple_a > $o ) > $o ) > hoare_669141180iple_a ).
thf(func_def_74,type,
sK34: ( ( hoare_669141180iple_a > $o ) > $o ) > hoare_669141180iple_a > $o ).
thf(func_def_75,type,
sK35: ( ( hoare_669141180iple_a > $o ) > $o ) > hoare_669141180iple_a ).
thf(func_def_76,type,
sK36: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a > hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
thf(func_def_77,type,
sK37: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a > hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_78,type,
sK38: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a > hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_79,type,
sK39: ( x_a > state > $o ) > ( x_a > state > $o ) > ( x_a > state > $o ) > ( x_a > state > $o ) > state ).
thf(func_def_80,type,
sK40: ( x_a > state > $o ) > ( x_a > state > $o ) > ( x_a > state > $o ) > ( x_a > state > $o ) > x_a ).
thf(func_def_81,type,
sK41: ( x_a > state > $o ) > ( x_a > state > $o ) > ( x_a > state > $o ) > ( x_a > state > $o ) > state ).
thf(func_def_82,type,
sK42: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
thf(func_def_83,type,
sK43: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a ).
thf(func_def_84,type,
sK44: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a ).
thf(func_def_85,type,
sK45: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a > $o ).
thf(func_def_86,type,
sK46: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
thf(func_def_87,type,
sK47: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
thf(func_def_89,type,
ph49:
!>[X0: $tType] : X0 ).
thf(f865,plain,
$false,
inference(subsumption_resolution,[status(thm)],[f846,f858]) ).
thf(f858,plain,
! [X1: $o] : ( $true = X1 ),
inference(trivial_inequality_removal,[status(thm)],[f848]) ).
thf(f848,plain,
! [X1: $o] :
( ( $true = X1 )
| ( $true != $true ) ),
inference(superposition,[status(thm)],[f803,f675]) ).
thf(f675,plain,
! [X2: x_a > state > $o,X3: hoare_669141180iple_a > $o,X0: $o,X1: com,X4: x_a > state > $o] :
( ( $true
= ( hoare_2128652938rivs_a @ X3
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [Y0: x_a,Y1: state] :
( ( X2 @ Y0 @ Y1 )
& X0 )
@ X1
@ X4 )
@ ( collec1717965009iple_a
@ ^ [Y0: hoare_669141180iple_a] : $false ) ) ) )
| ( $true = X0 ) ),
inference(definition_unfolding,[status(thm)],[f526,f639]) ).
thf(f639,plain,
( bot_bo280939947le_a_o
= ( collec1717965009iple_a
@ ^ [Y0: hoare_669141180iple_a] : $false ) ),
inference(cnf_transformation,[status(thm)],[f120]) ).
thf(f120,plain,
( bot_bo280939947le_a_o
= ( collec1717965009iple_a
@ ^ [Y0: hoare_669141180iple_a] : $false ) ),
inference(fool_elimination,[status(thm)],[f119]) ).
thf(f119,plain,
( bot_bo280939947le_a_o
= ( collec1717965009iple_a
@ ^ [X0: hoare_669141180iple_a] : $false ) ),
inference(rectify,[status(thm)],[f23]) ).
thf(f23,axiom,
( bot_bo280939947le_a_o
= ( collec1717965009iple_a
@ ^ [X52: hoare_669141180iple_a] : $false ) ),
file('/export/starexec/sandbox/tmp/tmp.oU5Hx1ZbCZ/DTF2THF_26033.p',fact_22_empty__def) ).
thf(f526,plain,
! [X2: x_a > state > $o,X3: hoare_669141180iple_a > $o,X0: $o,X1: com,X4: x_a > state > $o] :
( ( $true
= ( hoare_2128652938rivs_a @ X3
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [Y0: x_a,Y1: state] :
( ( X2 @ Y0 @ Y1 )
& X0 )
@ X1
@ X4 )
@ bot_bo280939947le_a_o ) ) )
| ( $true = X0 ) ),
inference(cnf_transformation,[status(thm)],[f371]) ).
thf(f371,plain,
! [X0: $o,X1: com,X2: x_a > state > $o,X3: hoare_669141180iple_a > $o,X4: x_a > state > $o] :
( ( $true
= ( hoare_2128652938rivs_a @ X3
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [Y0: x_a,Y1: state] :
( ( X2 @ Y0 @ Y1 )
& X0 )
@ X1
@ X4 )
@ bot_bo280939947le_a_o ) ) )
| ( ( $true = X0 )
& ( $true
!= ( hoare_2128652938rivs_a @ X3 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X2 @ X1 @ X4 ) @ bot_bo280939947le_a_o ) ) ) ) ),
inference(ennf_transformation,[status(thm)],[f206]) ).
thf(f206,plain,
! [X0: $o,X1: com,X2: x_a > state > $o,X3: hoare_669141180iple_a > $o,X4: x_a > state > $o] :
( ( ( $true = X0 )
=> ( $true
= ( hoare_2128652938rivs_a @ X3 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X2 @ X1 @ X4 ) @ bot_bo280939947le_a_o ) ) ) )
=> ( $true
= ( hoare_2128652938rivs_a @ X3
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [Y0: x_a,Y1: state] :
( ( X2 @ Y0 @ Y1 )
& X0 )
@ X1
@ X4 )
@ bot_bo280939947le_a_o ) ) ) ),
inference(fool_elimination,[status(thm)],[f205]) ).
thf(f205,plain,
! [X0: $o,X1: com,X2: x_a > state > $o,X3: hoare_669141180iple_a > $o,X4: x_a > state > $o] :
( ( X0
=> ( hoare_2128652938rivs_a @ X3 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X2 @ X1 @ X4 ) @ bot_bo280939947le_a_o ) ) )
=> ( hoare_2128652938rivs_a @ X3
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [X5: x_a,X6: state] :
( ( X2 @ X5 @ X6 )
& X0 )
@ X1
@ X4 )
@ bot_bo280939947le_a_o ) ) ),
inference(rectify,[status(thm)],[f5]) ).
thf(f5,axiom,
! [X17: $o,X15: com,X14: x_a > state > $o,X13: hoare_669141180iple_a > $o,X16: x_a > state > $o] :
( ( X17
=> ( hoare_2128652938rivs_a @ X13 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X14 @ X15 @ X16 ) @ bot_bo280939947le_a_o ) ) )
=> ( hoare_2128652938rivs_a @ X13
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [X18: x_a,X19: state] :
( ( X14 @ X18 @ X19 )
& X17 )
@ X15
@ X16 )
@ bot_bo280939947le_a_o ) ) ),
file('/export/starexec/sandbox/tmp/tmp.oU5Hx1ZbCZ/DTF2THF_26033.p',fact_4_constant) ).
thf(f803,plain,
! [X0: x_a > state > $o] :
( $true
!= ( hoare_2128652938rivs_a @ g
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a @ X0 @ c
@ ^ [Y0: x_a,Y1: state] :
( ( p @ Y0 @ Y1 )
& ~ ( b @ Y1 ) ) )
@ ( collec1717965009iple_a
@ ^ [Y0: hoare_669141180iple_a] : $false ) ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f802]) ).
thf(f802,plain,
! [X0: x_a > state > $o] :
( ( $true = $false )
| ( $true
!= ( hoare_2128652938rivs_a @ g
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a @ X0 @ c
@ ^ [Y0: x_a,Y1: state] :
( ( p @ Y0 @ Y1 )
& ~ ( b @ Y1 ) ) )
@ ( collec1717965009iple_a
@ ^ [Y0: hoare_669141180iple_a] : $false ) ) ) ) ),
inference(beta_eta_normalization,[status(thm)],[f801]) ).
thf(f801,plain,
! [X0: x_a > state > $o] :
( ( $true
= ( ^ [Y0: x_a,Y1: state] : $false
@ ( sK27 @ X0
@ ^ [Y0: x_a,Y1: state] : $false )
@ ( sK26 @ X0
@ ^ [Y0: x_a,Y1: state] : $false ) ) )
| ( $true
!= ( hoare_2128652938rivs_a @ g
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a @ X0 @ c
@ ^ [Y0: x_a,Y1: state] :
( ( p @ Y0 @ Y1 )
& ~ ( b @ Y1 ) ) )
@ ( collec1717965009iple_a
@ ^ [Y0: hoare_669141180iple_a] : $false ) ) ) ) ),
inference(trivial_inequality_removal,[status(thm)],[f798]) ).
thf(f798,plain,
! [X0: x_a > state > $o] :
( ( $true
= ( ^ [Y0: x_a,Y1: state] : $false
@ ( sK27 @ X0
@ ^ [Y0: x_a,Y1: state] : $false )
@ ( sK26 @ X0
@ ^ [Y0: x_a,Y1: state] : $false ) ) )
| ( $true != $true )
| ( $true
!= ( hoare_2128652938rivs_a @ g
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a @ X0 @ c
@ ^ [Y0: x_a,Y1: state] :
( ( p @ Y0 @ Y1 )
& ~ ( b @ Y1 ) ) )
@ ( collec1717965009iple_a
@ ^ [Y0: hoare_669141180iple_a] : $false ) ) ) ) ),
inference(superposition,[status(thm)],[f700,f721]) ).
thf(f721,plain,
! [X2: hoare_669141180iple_a > $o,X3: com,X0: x_a > state > $o,X1: x_a > state > $o,X4: x_a > state > $o] :
( ( $true
= ( hoare_2128652938rivs_a @ X2
@ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X0 @ X3 @ X4 )
@ ( collec1717965009iple_a
@ ^ [Y0: hoare_669141180iple_a] : $false ) ) ) )
| ( $true
!= ( hoare_2128652938rivs_a @ X2
@ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X1 @ X3 @ X4 )
@ ( collec1717965009iple_a
@ ^ [Y0: hoare_669141180iple_a] : $false ) ) ) )
| ( $true
= ( X0 @ ( sK27 @ X1 @ X0 ) @ ( sK26 @ X1 @ X0 ) ) ) ),
inference(definition_unfolding,[status(thm)],[f598,f639,f639]) ).
thf(f598,plain,
! [X2: hoare_669141180iple_a > $o,X3: com,X0: x_a > state > $o,X1: x_a > state > $o,X4: x_a > state > $o] :
( ( $true
!= ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X1 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) ) )
| ( $true
= ( X0 @ ( sK27 @ X1 @ X0 ) @ ( sK26 @ X1 @ X0 ) ) )
| ( $true
= ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X0 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) ) ) ),
inference(cnf_transformation,[status(thm)],[f456]) ).
thf(f456,plain,
! [X0: x_a > state > $o,X1: x_a > state > $o,X2: hoare_669141180iple_a > $o,X3: com,X4: x_a > state > $o] :
( ( $true
!= ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X1 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) ) )
| ( ( ( X1 @ ( sK27 @ X1 @ X0 ) @ ( sK26 @ X1 @ X0 ) )
!= $true )
& ( $true
= ( X0 @ ( sK27 @ X1 @ X0 ) @ ( sK26 @ X1 @ X0 ) ) ) )
| ( $true
= ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X0 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK26,sK27])],[f405,f455]) ).
thf(f455,plain,
! [X0: x_a > state > $o,X1: x_a > state > $o] :
( ? [X5: state,X6: x_a] :
( ( $true
!= ( X1 @ X6 @ X5 ) )
& ( ( X0 @ X6 @ X5 )
= $true ) )
=> ( ( ( X1 @ ( sK27 @ X1 @ X0 ) @ ( sK26 @ X1 @ X0 ) )
!= $true )
& ( $true
= ( X0 @ ( sK27 @ X1 @ X0 ) @ ( sK26 @ X1 @ X0 ) ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f405,plain,
! [X0: x_a > state > $o,X1: x_a > state > $o,X2: hoare_669141180iple_a > $o,X3: com,X4: x_a > state > $o] :
( ( $true
!= ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X1 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) ) )
| ? [X5: state,X6: x_a] :
( ( $true
!= ( X1 @ X6 @ X5 ) )
& ( ( X0 @ X6 @ X5 )
= $true ) )
| ( $true
= ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X0 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) ) ) ),
inference(flattening,[status(thm)],[f404]) ).
thf(f404,plain,
! [X0: x_a > state > $o,X1: x_a > state > $o,X2: hoare_669141180iple_a > $o,X3: com,X4: x_a > state > $o] :
( ( $true
= ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X0 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) ) )
| ? [X5: state,X6: x_a] :
( ( $true
!= ( X1 @ X6 @ X5 ) )
& ( ( X0 @ X6 @ X5 )
= $true ) )
| ( $true
!= ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X1 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) ) ) ),
inference(ennf_transformation,[status(thm)],[f182]) ).
thf(f182,plain,
! [X0: x_a > state > $o,X1: x_a > state > $o,X2: hoare_669141180iple_a > $o,X3: com,X4: x_a > state > $o] :
( ( $true
= ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X1 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) ) )
=> ( ! [X5: state,X6: x_a] :
( ( ( X0 @ X6 @ X5 )
= $true )
=> ( $true
= ( X1 @ X6 @ X5 ) ) )
=> ( $true
= ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X0 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f181]) ).
thf(f181,plain,
! [X0: x_a > state > $o,X1: x_a > state > $o,X2: hoare_669141180iple_a > $o,X3: com,X4: x_a > state > $o] :
( ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X1 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) )
=> ( ! [X5: state,X6: x_a] :
( ( X0 @ X6 @ X5 )
=> ( X1 @ X6 @ X5 ) )
=> ( hoare_2128652938rivs_a @ X2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X0 @ X3 @ X4 ) @ bot_bo280939947le_a_o ) ) ) ),
inference(rectify,[status(thm)],[f8]) ).
thf(f8,axiom,
! [X32: x_a > state > $o,X34: x_a > state > $o,X33: hoare_669141180iple_a > $o,X35: com,X36: x_a > state > $o] :
( ( hoare_2128652938rivs_a @ X33 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X34 @ X35 @ X36 ) @ bot_bo280939947le_a_o ) )
=> ( ! [X19: state,X18: x_a] :
( ( X32 @ X18 @ X19 )
=> ( X34 @ X18 @ X19 ) )
=> ( hoare_2128652938rivs_a @ X33 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ X32 @ X35 @ X36 ) @ bot_bo280939947le_a_o ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.oU5Hx1ZbCZ/DTF2THF_26033.p',fact_7_conseq1) ).
thf(f700,plain,
( $true
!= ( hoare_2128652938rivs_a @ g
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [Y0: x_a,Y1: state] : $false
@ c
@ ^ [Y0: x_a,Y1: state] :
( ( p @ Y0 @ Y1 )
& ~ ( b @ Y1 ) ) )
@ ( collec1717965009iple_a
@ ^ [Y0: hoare_669141180iple_a] : $false ) ) ) ),
inference(definition_unfolding,[status(thm)],[f565,f639]) ).
thf(f565,plain,
( ( hoare_2128652938rivs_a @ g
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [Y0: x_a,Y1: state] : $false
@ c
@ ^ [Y0: x_a,Y1: state] :
( ( p @ Y0 @ Y1 )
& ~ ( b @ Y1 ) ) )
@ bot_bo280939947le_a_o ) )
!= $true ),
inference(cnf_transformation,[status(thm)],[f329]) ).
thf(f329,plain,
( ( hoare_2128652938rivs_a @ g
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [Y0: x_a,Y1: state] : $false
@ c
@ ^ [Y0: x_a,Y1: state] :
( ( p @ Y0 @ Y1 )
& ~ ( b @ Y1 ) ) )
@ bot_bo280939947le_a_o ) )
!= $true ),
inference(flattening,[status(thm)],[f186]) ).
thf(f186,plain,
( ( hoare_2128652938rivs_a @ g
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [Y0: x_a,Y1: state] : $false
@ c
@ ^ [Y0: x_a,Y1: state] :
( ( p @ Y0 @ Y1 )
& ~ ( b @ Y1 ) ) )
@ bot_bo280939947le_a_o ) )
!= $true ),
inference(fool_elimination,[status(thm)],[f185]) ).
thf(f185,plain,
~ ( hoare_2128652938rivs_a @ g
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [X0: x_a,X1: state] : $false
@ c
@ ^ [X2: x_a,X3: state] :
( ( p @ X2 @ X3 )
& ~ ( b @ X3 ) ) )
@ bot_bo280939947le_a_o ) ),
inference(rectify,[status(thm)],[f99]) ).
thf(f99,negated_conjecture,
~ ( hoare_2128652938rivs_a @ g
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [X18: x_a,X19: state] : $false
@ c
@ ^ [X18: x_a,X19: state] :
( ( p @ X18 @ X19 )
& ~ ( b @ X19 ) ) )
@ bot_bo280939947le_a_o ) ),
inference(negated_conjecture,[status(cth)],[f98]) ).
thf(f98,conjecture,
( hoare_2128652938rivs_a @ g
@ ( insert175534902iple_a
@ ( hoare_1295064928iple_a
@ ^ [X18: x_a,X19: state] : $false
@ c
@ ^ [X18: x_a,X19: state] :
( ( p @ X18 @ X19 )
& ~ ( b @ X19 ) ) )
@ bot_bo280939947le_a_o ) ),
file('/export/starexec/sandbox/tmp/tmp.oU5Hx1ZbCZ/DTF2THF_26033.p',conj_0) ).
thf(f846,plain,
! [X0: x_a > state > $o] :
( ( hoare_2128652938rivs_a @ g
@ ( collec1717965009iple_a
@ ( fequal182287803iple_a
@ ( hoare_1295064928iple_a @ X0 @ c
@ ^ [Y0: x_a,Y1: state] :
( ( p @ Y0 @ Y1 )
& ~ ( b @ Y1 ) ) ) ) ) )
!= $true ),
inference(superposition,[status(thm)],[f803,f691]) ).
thf(f691,plain,
! [X0: hoare_669141180iple_a] :
( ( collec1717965009iple_a @ ( fequal182287803iple_a @ X0 ) )
= ( insert175534902iple_a @ X0
@ ( collec1717965009iple_a
@ ^ [Y0: hoare_669141180iple_a] : $false ) ) ),
inference(definition_unfolding,[status(thm)],[f554,f639]) ).
thf(f554,plain,
! [X0: hoare_669141180iple_a] :
( ( insert175534902iple_a @ X0 @ bot_bo280939947le_a_o )
= ( collec1717965009iple_a @ ( fequal182287803iple_a @ X0 ) ) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
thf(f126,plain,
! [X0: hoare_669141180iple_a] :
( ( insert175534902iple_a @ X0 @ bot_bo280939947le_a_o )
= ( collec1717965009iple_a @ ( fequal182287803iple_a @ X0 ) ) ),
inference(fool_elimination,[status(thm)],[f125]) ).
thf(f125,plain,
! [X0: hoare_669141180iple_a] :
( ( insert175534902iple_a @ X0 @ bot_bo280939947le_a_o )
= ( collec1717965009iple_a @ ( fequal182287803iple_a @ X0 ) ) ),
inference(rectify,[status(thm)],[f13]) ).
thf(f13,axiom,
! [X50: hoare_669141180iple_a] :
( ( collec1717965009iple_a @ ( fequal182287803iple_a @ X50 ) )
= ( insert175534902iple_a @ X50 @ bot_bo280939947le_a_o ) ),
file('/export/starexec/sandbox/tmp/tmp.oU5Hx1ZbCZ/DTF2THF_26033.p',fact_12_singleton__conv2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWW470^1 : TPTP v9.2.1. Released v5.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.15/0.33 % Computer : n002.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue Feb 24 13:40:03 EST 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.32/0.47 ---- Original DTF file ---
% 0.32/0.48 thf(spec,logic,$$dhol).
% 0.32/0.48 %------------------------------------------------------------------------------
% 0.32/0.48 % File : SWW470^1 : TPTP v9.2.1. Released v5.3.0.
% 0.32/0.48 % Domain : Software Verification
% 0.32/0.48 % Problem : Hoare's Logic with Procedures line 200, 100 axioms selected
% 0.32/0.48 % Version : Especial.
% 0.32/0.48 % English :
% 0.32/0.48
% 0.32/0.48 % Refs : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day
% 0.32/0.48 % : [Bla11] Blanchette (2011), Email to Geoff Sutcliffe
% 0.32/0.48 % Source : [Bla11]
% 0.32/0.48 % Names : hoare_100_thf_l200 [Bla11]
% 0.32/0.48
% 0.32/0.48 % Status : Theorem
% 0.32/0.48 % Rating : 0.33 v9.1.0, 0.38 v9.0.0, 0.40 v8.2.0, 0.38 v8.1.0, 0.27 v7.5.0, 0.29 v7.4.0, 0.22 v7.2.0, 0.12 v7.1.0, 0.25 v7.0.0, 0.14 v6.4.0, 0.17 v6.3.0, 0.20 v6.2.0, 0.29 v6.0.0, 0.43 v5.5.0, 0.50 v5.4.0, 0.80 v5.3.0
% 0.32/0.48 % Syntax : Number of formulae : 125 ( 25 unt; 27 typ; 0 def)
% 0.32/0.48 % Number of atoms : 422 ( 108 equ; 21 cnn)
% 0.32/0.48 % Maximal formula atoms : 9 ( 4 avg)
% 0.32/0.48 % Number of connectives : 854 ( 47 ~; 11 |; 31 &; 634 @)
% 0.32/0.48 % ( 22 <=>; 109 =>; 0 <=; 0 <~>)
% 0.32/0.48 % Maximal formula depth : 19 ( 8 avg)
% 0.32/0.48 % Number of types : 5 ( 4 usr)
% 0.32/0.48 % Number of type conns : 268 ( 268 >; 0 *; 0 +; 0 <<)
% 0.32/0.48 % Number of symbols : 29 ( 23 usr; 8 con; 0-4 aty)
% 0.32/0.48 % Number of variables : 307 ( 24 ^; 267 !; 16 ?; 307 :)
% 0.32/0.48 % SPC : TH0_THM_EQU_NAR
% 0.32/0.48
% 0.32/0.48 % Comments : This file was generated by Isabelle (most likely Sledgehammer)
% 0.32/0.48 % 2011-08-09 19:02:36
% 0.32/0.48 %------------------------------------------------------------------------------
% 0.32/0.48 %----Should-be-implicit typings (4)
% 0.32/0.48 thf(ty_ty_t__a,type,
% 0.32/0.48 x_a: $tType ).
% 0.32/0.48
% 0.32/0.48 thf(ty_ty_tc__Com__Ocom,type,
% 0.32/0.48 com: $tType ).
% 0.32/0.48
% 0.32/0.48 thf(ty_ty_tc__Com__Ostate,type,
% 0.32/0.48 state: $tType ).
% 0.32/0.48
% 0.32/0.48 thf(ty_ty_tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 0.32/0.48 hoare_669141180iple_a: $tType ).
% 0.32/0.48
% 0.32/0.48 %----Explicit typings (23)
% 0.32/0.48 thf(sy_c_Com_Ocom_OSKIP,type,
% 0.32/0.48 skip: com ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Com_Ocom_OSemi,type,
% 0.32/0.48 semi: com > com > com ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Ex,type,
% 0.32/0.48 ex: ( hoare_669141180iple_a > $o ) > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Finite__Set_Ofinite_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_,type,
% 0.32/0.48 finite957651855iple_a: ( hoare_669141180iple_a > $o ) > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Finite__Set_Ofold1Set_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__,type,
% 0.32/0.48 finite840267660iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Finite__Set_Ofold1_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 0.32/0.48 finite684844060iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Finite__Set_Ofold__graph_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_I,type,
% 0.32/0.48 finite590756294iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Finite__Set_Ofolding__one_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_,type,
% 0.32/0.48 finite972428089iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ) > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Finite__Set_Ofolding__one__idem_000tc__Hoare____Mirabelle____ghhkfsbqqq__Ot,type,
% 0.32/0.48 finite252461622iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ) > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_HOL_OThe_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 0.32/0.48 the_Ho49089901iple_a: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Hoare__Mirabelle__ghhkfsbqqq_Ohoare__derivs_000t__a,type,
% 0.32/0.48 hoare_2128652938rivs_a: ( hoare_669141180iple_a > $o ) > ( hoare_669141180iple_a > $o ) > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Hoare__Mirabelle__ghhkfsbqqq_Otriple_Otriple_000t__a,type,
% 0.32/0.48 hoare_1295064928iple_a: ( x_a > state > $o ) > com > ( x_a > state > $o ) > hoare_669141180iple_a ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Orderings_Obot__class_Obot_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__O,type,
% 0.32/0.48 bot_bo280939947le_a_o: hoare_669141180iple_a > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Orderings_Obot__class_Obot_000_Eo,type,
% 0.32/0.48 bot_bot_o: $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Set_OCollect_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 0.32/0.48 collec1717965009iple_a: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Set_Oinsert_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 0.32/0.48 insert175534902iple_a: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_Set_Othe__elem_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 0.32/0.48 the_el738790235iple_a: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_fequal_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 0.32/0.48 fequal182287803iple_a: hoare_669141180iple_a > hoare_669141180iple_a > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_c_member_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 0.32/0.48 member1016246415iple_a: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_v_G,type,
% 0.32/0.48 g: hoare_669141180iple_a > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_v_P,type,
% 0.32/0.48 p: x_a > state > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_v_b,type,
% 0.32/0.48 b: state > $o ).
% 0.32/0.48
% 0.32/0.48 thf(sy_v_c,type,
% 0.32/0.48 c: com ).
% 0.32/0.48
% 0.32/0.48 %----Relevant facts (95)
% 0.32/0.48 thf(fact_0_empty,axiom,
% 0.32/0.48 ! [G_12: hoare_669141180iple_a > $o] : ( hoare_2128652938rivs_a @ G_12 @ bot_bo280939947le_a_o ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_1_triple_Oinject,axiom,
% 0.32/0.48 ! [Fun1_2: x_a > state > $o,Com_2: com,Fun2_2: x_a > state > $o,Fun1_1: x_a > state > $o,Com_1: com,Fun2_1: x_a > state > $o] :
% 0.32/0.48 ( ( ( hoare_1295064928iple_a @ Fun1_2 @ Com_2 @ Fun2_2 )
% 0.32/0.48 = ( hoare_1295064928iple_a @ Fun1_1 @ Com_1 @ Fun2_1 ) )
% 0.32/0.48 <=> ( ( Fun1_2 = Fun1_1 )
% 0.32/0.48 & ( Com_2 = Com_1 )
% 0.32/0.48 & ( Fun2_2 = Fun2_1 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_2_cut,axiom,
% 0.32/0.48 ! [G_11: hoare_669141180iple_a > $o,G_10: hoare_669141180iple_a > $o,Ts_1: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( hoare_2128652938rivs_a @ G_10 @ Ts_1 )
% 0.32/0.48 => ( ( hoare_2128652938rivs_a @ G_11 @ G_10 )
% 0.32/0.48 => ( hoare_2128652938rivs_a @ G_11 @ Ts_1 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_3_hoare__derivs_Oinsert,axiom,
% 0.32/0.48 ! [Ts: hoare_669141180iple_a > $o,G_9: hoare_669141180iple_a > $o,T: hoare_669141180iple_a] :
% 0.32/0.48 ( ( hoare_2128652938rivs_a @ G_9 @ ( insert175534902iple_a @ T @ bot_bo280939947le_a_o ) )
% 0.32/0.48 => ( ( hoare_2128652938rivs_a @ G_9 @ Ts )
% 0.32/0.48 => ( hoare_2128652938rivs_a @ G_9 @ ( insert175534902iple_a @ T @ Ts ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_4_constant,axiom,
% 0.32/0.48 ! [G_8: hoare_669141180iple_a > $o,P_25: x_a > state > $o,C_9: com,Q_11: x_a > state > $o,C_8: $o] :
% 0.32/0.48 ( ( C_8
% 0.32/0.48 => ( hoare_2128652938rivs_a @ G_8 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_25 @ C_9 @ Q_11 ) @ bot_bo280939947le_a_o ) ) )
% 0.32/0.48 => ( hoare_2128652938rivs_a @ G_8
% 0.32/0.48 @ ( insert175534902iple_a
% 0.32/0.48 @ ( hoare_1295064928iple_a
% 0.32/0.48 @ ^ [Z: x_a,S: state] : ( (&) @ ( P_25 @ Z @ S ) @ C_8 )
% 0.32/0.48 @ C_9
% 0.32/0.48 @ Q_11 )
% 0.32/0.48 @ bot_bo280939947le_a_o ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_5_escape,axiom,
% 0.32/0.48 ! [G_7: hoare_669141180iple_a > $o,C_7: com,Q_10: x_a > state > $o,P_24: x_a > state > $o] :
% 0.32/0.48 ( ! [Z: x_a,S: state] :
% 0.32/0.48 ( ( P_24 @ Z @ S )
% 0.32/0.48 => ( hoare_2128652938rivs_a @ G_7
% 0.32/0.48 @ ( insert175534902iple_a
% 0.32/0.48 @ ( hoare_1295064928iple_a
% 0.32/0.48 @ ^ [Za: x_a,S_1: state] : ( S_1 = S )
% 0.32/0.48 @ C_7
% 0.32/0.48 @ ^ [Z_6: x_a] : ( Q_10 @ Z ) )
% 0.32/0.48 @ bot_bo280939947le_a_o ) ) )
% 0.32/0.48 => ( hoare_2128652938rivs_a @ G_7 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_24 @ C_7 @ Q_10 ) @ bot_bo280939947le_a_o ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_6_conseq2,axiom,
% 0.32/0.48 ! [Q_9: x_a > state > $o,G_6: hoare_669141180iple_a > $o,P_23: x_a > state > $o,C_6: com,Q_8: x_a > state > $o] :
% 0.32/0.48 ( ( hoare_2128652938rivs_a @ G_6 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_23 @ C_6 @ Q_8 ) @ bot_bo280939947le_a_o ) )
% 0.32/0.48 => ( ! [Z: x_a,S: state] :
% 0.32/0.48 ( ( Q_8 @ Z @ S )
% 0.32/0.48 => ( Q_9 @ Z @ S ) )
% 0.32/0.48 => ( hoare_2128652938rivs_a @ G_6 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_23 @ C_6 @ Q_9 ) @ bot_bo280939947le_a_o ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_7_conseq1,axiom,
% 0.32/0.48 ! [P_22: x_a > state > $o,G_5: hoare_669141180iple_a > $o,P_21: x_a > state > $o,C_5: com,Q_7: x_a > state > $o] :
% 0.32/0.48 ( ( hoare_2128652938rivs_a @ G_5 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_21 @ C_5 @ Q_7 ) @ bot_bo280939947le_a_o ) )
% 0.32/0.48 => ( ! [Z: x_a,S: state] :
% 0.32/0.48 ( ( P_22 @ Z @ S )
% 0.32/0.48 => ( P_21 @ Z @ S ) )
% 0.32/0.48 => ( hoare_2128652938rivs_a @ G_5 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_22 @ C_5 @ Q_7 ) @ bot_bo280939947le_a_o ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_8_conseq12,axiom,
% 0.32/0.48 ! [Q_6: x_a > state > $o,P_20: x_a > state > $o,G_4: hoare_669141180iple_a > $o,P_19: x_a > state > $o,C_4: com,Q_5: x_a > state > $o] :
% 0.32/0.48 ( ( hoare_2128652938rivs_a @ G_4 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_19 @ C_4 @ Q_5 ) @ bot_bo280939947le_a_o ) )
% 0.32/0.48 => ( ! [Z: x_a,S: state] :
% 0.32/0.48 ( ( P_20 @ Z @ S )
% 0.32/0.48 => ! [S_1: state] :
% 0.32/0.48 ( ! [Z_6: x_a] :
% 0.32/0.48 ( ( P_19 @ Z_6 @ S )
% 0.32/0.48 => ( Q_5 @ Z_6 @ S_1 ) )
% 0.32/0.48 => ( Q_6 @ Z @ S_1 ) ) )
% 0.32/0.48 => ( hoare_2128652938rivs_a @ G_4 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_20 @ C_4 @ Q_6 ) @ bot_bo280939947le_a_o ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_9_insertE,axiom,
% 0.32/0.48 ! [A_64: hoare_669141180iple_a,B_14: hoare_669141180iple_a,A_63: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( member1016246415iple_a @ A_64 @ ( insert175534902iple_a @ B_14 @ A_63 ) )
% 0.32/0.48 => ( ( A_64 != B_14 )
% 0.32/0.48 => ( member1016246415iple_a @ A_64 @ A_63 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_10_insertCI,axiom,
% 0.32/0.48 ! [B_13: hoare_669141180iple_a,A_62: hoare_669141180iple_a,B_12: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( ~ ( member1016246415iple_a @ A_62 @ B_12 )
% 0.32/0.48 => ( A_62 = B_13 ) )
% 0.32/0.48 => ( member1016246415iple_a @ A_62 @ ( insert175534902iple_a @ B_13 @ B_12 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_11_emptyE,axiom,
% 0.32/0.48 ! [A_61: hoare_669141180iple_a] :
% 0.32/0.48 ~ ( member1016246415iple_a @ A_61 @ bot_bo280939947le_a_o ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_12_singleton__conv2,axiom,
% 0.32/0.48 ! [A_60: hoare_669141180iple_a] :
% 0.32/0.48 ( ( collec1717965009iple_a @ ( fequal182287803iple_a @ A_60 ) )
% 0.32/0.48 = ( insert175534902iple_a @ A_60 @ bot_bo280939947le_a_o ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_13_singleton__conv,axiom,
% 0.32/0.48 ! [A_59: hoare_669141180iple_a] :
% 0.32/0.48 ( ( collec1717965009iple_a
% 0.32/0.48 @ ^ [X_3: hoare_669141180iple_a] : ( X_3 = A_59 ) )
% 0.32/0.48 = ( insert175534902iple_a @ A_59 @ bot_bo280939947le_a_o ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_14_Collect__conv__if2,axiom,
% 0.32/0.48 ! [P_18: hoare_669141180iple_a > $o,A_58: hoare_669141180iple_a] :
% 0.32/0.48 ( ( ( P_18 @ A_58 )
% 0.32/0.48 => ( ( collec1717965009iple_a
% 0.32/0.48 @ ^ [X_3: hoare_669141180iple_a] : ( (&) @ ( A_58 = X_3 ) @ ( P_18 @ X_3 ) ) )
% 0.32/0.48 = ( insert175534902iple_a @ A_58 @ bot_bo280939947le_a_o ) ) )
% 0.32/0.48 & ( ~ ( P_18 @ A_58 )
% 0.32/0.48 => ( ( collec1717965009iple_a
% 0.32/0.48 @ ^ [X_3: hoare_669141180iple_a] : ( (&) @ ( A_58 = X_3 ) @ ( P_18 @ X_3 ) ) )
% 0.32/0.48 = bot_bo280939947le_a_o ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_15_Collect__conv__if,axiom,
% 0.32/0.48 ! [P_17: hoare_669141180iple_a > $o,A_57: hoare_669141180iple_a] :
% 0.32/0.48 ( ( ( P_17 @ A_57 )
% 0.32/0.48 => ( ( collec1717965009iple_a
% 0.32/0.48 @ ^ [X_3: hoare_669141180iple_a] : ( (&) @ ( X_3 = A_57 ) @ ( P_17 @ X_3 ) ) )
% 0.32/0.48 = ( insert175534902iple_a @ A_57 @ bot_bo280939947le_a_o ) ) )
% 0.32/0.48 & ( ~ ( P_17 @ A_57 )
% 0.32/0.48 => ( ( collec1717965009iple_a
% 0.32/0.48 @ ^ [X_3: hoare_669141180iple_a] : ( (&) @ ( X_3 = A_57 ) @ ( P_17 @ X_3 ) ) )
% 0.32/0.48 = bot_bo280939947le_a_o ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_16_equals0D,axiom,
% 0.32/0.48 ! [A_56: hoare_669141180iple_a,A_55: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( A_55 = bot_bo280939947le_a_o )
% 0.32/0.48 => ~ ( member1016246415iple_a @ A_56 @ A_55 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_17_Collect__empty__eq,axiom,
% 0.32/0.48 ! [P_16: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( ( collec1717965009iple_a @ P_16 )
% 0.32/0.48 = bot_bo280939947le_a_o )
% 0.32/0.48 <=> ! [X_3: hoare_669141180iple_a] :
% 0.32/0.48 ~ ( P_16 @ X_3 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_18_empty__iff,axiom,
% 0.32/0.48 ! [C_3: hoare_669141180iple_a] :
% 0.32/0.48 ~ ( member1016246415iple_a @ C_3 @ bot_bo280939947le_a_o ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_19_empty__Collect__eq,axiom,
% 0.32/0.48 ! [P_15: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( bot_bo280939947le_a_o
% 0.32/0.48 = ( collec1717965009iple_a @ P_15 ) )
% 0.32/0.48 <=> ! [X_3: hoare_669141180iple_a] :
% 0.32/0.48 ~ ( P_15 @ X_3 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_20_ex__in__conv,axiom,
% 0.32/0.48 ! [A_54: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ? [X_3: hoare_669141180iple_a] : ( member1016246415iple_a @ X_3 @ A_54 )
% 0.32/0.48 <=> ( A_54 != bot_bo280939947le_a_o ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_21_all__not__in__conv,axiom,
% 0.32/0.48 ! [A_53: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ! [X_3: hoare_669141180iple_a] :
% 0.32/0.48 ~ ( member1016246415iple_a @ X_3 @ A_53 )
% 0.32/0.48 <=> ( A_53 = bot_bo280939947le_a_o ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_22_empty__def,axiom,
% 0.32/0.48 ( bot_bo280939947le_a_o
% 0.32/0.48 = ( collec1717965009iple_a
% 0.32/0.48 @ ^ [X_3: hoare_669141180iple_a] : $false ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_23_insert__absorb,axiom,
% 0.32/0.48 ! [A_52: hoare_669141180iple_a,A_51: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( member1016246415iple_a @ A_52 @ A_51 )
% 0.32/0.48 => ( ( insert175534902iple_a @ A_52 @ A_51 )
% 0.32/0.48 = A_51 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_24_insertI2,axiom,
% 0.32/0.48 ! [B_11: hoare_669141180iple_a,A_50: hoare_669141180iple_a,B_10: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( member1016246415iple_a @ A_50 @ B_10 )
% 0.32/0.48 => ( member1016246415iple_a @ A_50 @ ( insert175534902iple_a @ B_11 @ B_10 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_25_insert__ident,axiom,
% 0.32/0.48 ! [B_9: hoare_669141180iple_a > $o,X_24: hoare_669141180iple_a,A_49: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ~ ( member1016246415iple_a @ X_24 @ A_49 )
% 0.32/0.48 => ( ~ ( member1016246415iple_a @ X_24 @ B_9 )
% 0.32/0.48 => ( ( ( insert175534902iple_a @ X_24 @ A_49 )
% 0.32/0.48 = ( insert175534902iple_a @ X_24 @ B_9 ) )
% 0.32/0.48 <=> ( A_49 = B_9 ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_26_insert__code,axiom,
% 0.32/0.48 ! [Y_6: hoare_669141180iple_a,A_48: hoare_669141180iple_a > $o,X_23: hoare_669141180iple_a] :
% 0.32/0.48 ( ( insert175534902iple_a @ Y_6 @ A_48 @ X_23 )
% 0.32/0.48 <=> ( ( Y_6 = X_23 )
% 0.32/0.48 | ( A_48 @ X_23 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_27_insert__iff,axiom,
% 0.32/0.48 ! [A_47: hoare_669141180iple_a,B_8: hoare_669141180iple_a,A_46: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( member1016246415iple_a @ A_47 @ ( insert175534902iple_a @ B_8 @ A_46 ) )
% 0.32/0.48 <=> ( ( A_47 = B_8 )
% 0.32/0.48 | ( member1016246415iple_a @ A_47 @ A_46 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_28_insert__commute,axiom,
% 0.32/0.48 ! [X_22: hoare_669141180iple_a,Y_5: hoare_669141180iple_a,A_45: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( insert175534902iple_a @ X_22 @ ( insert175534902iple_a @ Y_5 @ A_45 ) )
% 0.32/0.48 = ( insert175534902iple_a @ Y_5 @ ( insert175534902iple_a @ X_22 @ A_45 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_29_insert__absorb2,axiom,
% 0.32/0.48 ! [X_21: hoare_669141180iple_a,A_44: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( insert175534902iple_a @ X_21 @ ( insert175534902iple_a @ X_21 @ A_44 ) )
% 0.32/0.48 = ( insert175534902iple_a @ X_21 @ A_44 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_30_insert__Collect,axiom,
% 0.32/0.48 ! [A_43: hoare_669141180iple_a,P_14: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( insert175534902iple_a @ A_43 @ ( collec1717965009iple_a @ P_14 ) )
% 0.32/0.48 = ( collec1717965009iple_a
% 0.32/0.48 @ ^ [U: hoare_669141180iple_a] : ( (=>) @ ( (~) @ ( U = A_43 ) ) @ ( P_14 @ U ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_31_insert__compr,axiom,
% 0.32/0.48 ! [A_42: hoare_669141180iple_a,B_7: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( insert175534902iple_a @ A_42 @ B_7 )
% 0.32/0.48 = ( collec1717965009iple_a
% 0.32/0.48 @ ^ [X_3: hoare_669141180iple_a] : ( (|) @ ( X_3 = A_42 ) @ ( member1016246415iple_a @ X_3 @ B_7 ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_32_insertI1,axiom,
% 0.32/0.48 ! [A_41: hoare_669141180iple_a,B_6: hoare_669141180iple_a > $o] : ( member1016246415iple_a @ A_41 @ ( insert175534902iple_a @ A_41 @ B_6 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_33_insert__compr__raw,axiom,
% 0.32/0.48 ! [X_3: hoare_669141180iple_a,Xa: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( insert175534902iple_a @ X_3 @ Xa )
% 0.32/0.48 = ( collec1717965009iple_a
% 0.32/0.48 @ ^ [Y_1: hoare_669141180iple_a] : ( (|) @ ( Y_1 = X_3 ) @ ( member1016246415iple_a @ Y_1 @ Xa ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_34_singleton__inject,axiom,
% 0.32/0.48 ! [A_40: hoare_669141180iple_a,B_5: hoare_669141180iple_a] :
% 0.32/0.48 ( ( ( insert175534902iple_a @ A_40 @ bot_bo280939947le_a_o )
% 0.32/0.48 = ( insert175534902iple_a @ B_5 @ bot_bo280939947le_a_o ) )
% 0.32/0.48 => ( A_40 = B_5 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_35_singletonE,axiom,
% 0.32/0.48 ! [B_4: hoare_669141180iple_a,A_39: hoare_669141180iple_a] :
% 0.32/0.48 ( ( member1016246415iple_a @ B_4 @ ( insert175534902iple_a @ A_39 @ bot_bo280939947le_a_o ) )
% 0.32/0.48 => ( B_4 = A_39 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_36_doubleton__eq__iff,axiom,
% 0.32/0.48 ! [A_38: hoare_669141180iple_a,B_3: hoare_669141180iple_a,C_2: hoare_669141180iple_a,D_1: hoare_669141180iple_a] :
% 0.32/0.48 ( ( ( insert175534902iple_a @ A_38 @ ( insert175534902iple_a @ B_3 @ bot_bo280939947le_a_o ) )
% 0.32/0.48 = ( insert175534902iple_a @ C_2 @ ( insert175534902iple_a @ D_1 @ bot_bo280939947le_a_o ) ) )
% 0.32/0.48 <=> ( ( ( A_38 = C_2 )
% 0.32/0.48 & ( B_3 = D_1 ) )
% 0.32/0.48 | ( ( A_38 = D_1 )
% 0.32/0.48 & ( B_3 = C_2 ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_37_singleton__iff,axiom,
% 0.32/0.48 ! [B_2: hoare_669141180iple_a,A_37: hoare_669141180iple_a] :
% 0.32/0.48 ( ( member1016246415iple_a @ B_2 @ ( insert175534902iple_a @ A_37 @ bot_bo280939947le_a_o ) )
% 0.32/0.48 <=> ( B_2 = A_37 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_38_insert__not__empty,axiom,
% 0.32/0.48 ! [A_36: hoare_669141180iple_a,A_35: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( insert175534902iple_a @ A_36 @ A_35 )
% 0.32/0.48 != bot_bo280939947le_a_o ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_39_empty__not__insert,axiom,
% 0.32/0.48 ! [A_34: hoare_669141180iple_a,A_33: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( bot_bo280939947le_a_o
% 0.32/0.48 != ( insert175534902iple_a @ A_34 @ A_33 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_40_the__elem__eq,axiom,
% 0.32/0.48 ! [X_20: hoare_669141180iple_a] :
% 0.32/0.48 ( ( the_el738790235iple_a @ ( insert175534902iple_a @ X_20 @ bot_bo280939947le_a_o ) )
% 0.32/0.48 = X_20 ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_41_bot__apply,axiom,
% 0.32/0.48 ! [X_19: hoare_669141180iple_a] :
% 0.32/0.48 ( ( bot_bo280939947le_a_o @ X_19 )
% 0.32/0.48 <=> bot_bot_o ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_42_bot__fun__def,axiom,
% 0.32/0.48 ! [X_3: hoare_669141180iple_a] :
% 0.32/0.48 ( ( bot_bo280939947le_a_o @ X_3 )
% 0.32/0.48 <=> bot_bot_o ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_43_hoare__derivs_OSkip,axiom,
% 0.32/0.48 ! [G_3: hoare_669141180iple_a > $o,P_13: x_a > state > $o] : ( hoare_2128652938rivs_a @ G_3 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_13 @ skip @ P_13 ) @ bot_bo280939947le_a_o ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_44_Comp,axiom,
% 0.32/0.48 ! [D: com,R: x_a > state > $o,G_2: hoare_669141180iple_a > $o,P_12: x_a > state > $o,C_1: com,Q_4: x_a > state > $o] :
% 0.32/0.48 ( ( hoare_2128652938rivs_a @ G_2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_12 @ C_1 @ Q_4 ) @ bot_bo280939947le_a_o ) )
% 0.32/0.48 => ( ( hoare_2128652938rivs_a @ G_2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ Q_4 @ D @ R ) @ bot_bo280939947le_a_o ) )
% 0.32/0.48 => ( hoare_2128652938rivs_a @ G_2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_12 @ ( semi @ C_1 @ D ) @ R ) @ bot_bo280939947le_a_o ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_45_triple_Oexhaust,axiom,
% 0.32/0.48 ! [Y_4: hoare_669141180iple_a] :
% 0.32/0.48 ~ ! [Fun1: x_a > state > $o,Com: com,Fun2: x_a > state > $o] :
% 0.32/0.48 ( Y_4
% 0.32/0.48 != ( hoare_1295064928iple_a @ Fun1 @ Com @ Fun2 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_46_Set_Oset__insert,axiom,
% 0.32/0.48 ! [X_18: hoare_669141180iple_a,A_32: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( member1016246415iple_a @ X_18 @ A_32 )
% 0.32/0.48 => ~ ! [B_1: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( A_32
% 0.32/0.48 = ( insert175534902iple_a @ X_18 @ B_1 ) )
% 0.32/0.48 => ( member1016246415iple_a @ X_18 @ B_1 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_47_com_Osimps_I13_J,axiom,
% 0.32/0.48 ! [Com1: com,Com2: com] :
% 0.32/0.48 ( ( semi @ Com1 @ Com2 )
% 0.32/0.48 != skip ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_48_com_Osimps_I12_J,axiom,
% 0.32/0.48 ! [Com1: com,Com2: com] :
% 0.32/0.48 ( skip
% 0.32/0.48 != ( semi @ Com1 @ Com2 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_49_the__elem__def,axiom,
% 0.32/0.48 ! [X_17: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( the_el738790235iple_a @ X_17 )
% 0.32/0.48 = ( the_Ho49089901iple_a
% 0.32/0.48 @ ^ [X_3: hoare_669141180iple_a] :
% 0.32/0.48 ( X_17
% 0.32/0.48 = ( insert175534902iple_a @ X_3 @ bot_bo280939947le_a_o ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_50_mk__disjoint__insert,axiom,
% 0.32/0.48 ! [A_31: hoare_669141180iple_a,A_30: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( member1016246415iple_a @ A_31 @ A_30 )
% 0.32/0.48 => ? [B_1: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( A_30
% 0.32/0.48 = ( insert175534902iple_a @ A_31 @ B_1 ) )
% 0.32/0.48 & ~ ( member1016246415iple_a @ A_31 @ B_1 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_51_com_Osimps_I3_J,axiom,
% 0.32/0.48 ! [Com1_1: com,Com2_1: com,Com1: com,Com2: com] :
% 0.32/0.48 ( ( ( semi @ Com1_1 @ Com2_1 )
% 0.32/0.48 = ( semi @ Com1 @ Com2 ) )
% 0.32/0.48 <=> ( ( Com1_1 = Com1 )
% 0.32/0.48 & ( Com2_1 = Com2 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_52_the__sym__eq__trivial,axiom,
% 0.32/0.48 ! [X_16: hoare_669141180iple_a] :
% 0.32/0.48 ( ( the_Ho49089901iple_a @ ( fequal182287803iple_a @ X_16 ) )
% 0.32/0.48 = X_16 ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_53_the__eq__trivial,axiom,
% 0.32/0.48 ! [A_29: hoare_669141180iple_a] :
% 0.32/0.48 ( ( the_Ho49089901iple_a
% 0.32/0.48 @ ^ [X_3: hoare_669141180iple_a] : ( X_3 = A_29 ) )
% 0.32/0.48 = A_29 ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_54_If__def,axiom,
% 0.32/0.48 ! [X_15: hoare_669141180iple_a,Y_3: hoare_669141180iple_a,P_11: $o] :
% 0.32/0.48 ( ( P_11
% 0.32/0.48 => ( X_15
% 0.32/0.48 = ( the_Ho49089901iple_a
% 0.32/0.48 @ ^ [Z_7: hoare_669141180iple_a] : ( (&) @ ( (=>) @ P_11 @ ( Z_7 = X_15 ) ) @ ( (=>) @ ( (~) @ P_11 ) @ ( Z_7 = Y_3 ) ) ) ) ) )
% 0.32/0.48 & ( ~ P_11
% 0.32/0.48 => ( Y_3
% 0.32/0.48 = ( the_Ho49089901iple_a
% 0.32/0.48 @ ^ [Z_7: hoare_669141180iple_a] : ( (&) @ ( (=>) @ P_11 @ ( Z_7 = X_15 ) ) @ ( (=>) @ ( (~) @ P_11 ) @ ( Z_7 = Y_3 ) ) ) ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_55_equals0I,axiom,
% 0.32/0.48 ! [A_28: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ! [Y_1: hoare_669141180iple_a] :
% 0.32/0.48 ~ ( member1016246415iple_a @ Y_1 @ A_28 )
% 0.32/0.48 => ( A_28 = bot_bo280939947le_a_o ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_56_the__equality,axiom,
% 0.32/0.48 ! [P_10: hoare_669141180iple_a > $o,A_27: hoare_669141180iple_a] :
% 0.32/0.48 ( ( P_10 @ A_27 )
% 0.32/0.48 => ( ! [X_3: hoare_669141180iple_a] :
% 0.32/0.48 ( ( P_10 @ X_3 )
% 0.32/0.48 => ( X_3 = A_27 ) )
% 0.32/0.48 => ( ( the_Ho49089901iple_a @ P_10 )
% 0.32/0.48 = A_27 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_57_theI,axiom,
% 0.32/0.48 ! [P_9: hoare_669141180iple_a > $o,A_26: hoare_669141180iple_a] :
% 0.32/0.48 ( ( P_9 @ A_26 )
% 0.32/0.48 => ( ! [X_3: hoare_669141180iple_a] :
% 0.32/0.48 ( ( P_9 @ X_3 )
% 0.32/0.48 => ( X_3 = A_26 ) )
% 0.32/0.48 => ( P_9 @ ( the_Ho49089901iple_a @ P_9 ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_58_the1__equality,axiom,
% 0.32/0.48 ! [A_25: hoare_669141180iple_a,P_8: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ? [X_3: hoare_669141180iple_a] :
% 0.32/0.48 ( ( P_8 @ X_3 )
% 0.32/0.48 & ! [Y_1: hoare_669141180iple_a] :
% 0.32/0.48 ( ( P_8 @ Y_1 )
% 0.32/0.48 => ( Y_1 = X_3 ) ) )
% 0.32/0.48 => ( ( P_8 @ A_25 )
% 0.32/0.48 => ( ( the_Ho49089901iple_a @ P_8 )
% 0.32/0.48 = A_25 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_59_theI_H,axiom,
% 0.32/0.48 ! [P_7: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ? [X_3: hoare_669141180iple_a] :
% 0.32/0.48 ( ( P_7 @ X_3 )
% 0.32/0.48 & ! [Y_1: hoare_669141180iple_a] :
% 0.32/0.48 ( ( P_7 @ Y_1 )
% 0.32/0.48 => ( Y_1 = X_3 ) ) )
% 0.32/0.48 => ( P_7 @ ( the_Ho49089901iple_a @ P_7 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_60_conseq,axiom,
% 0.32/0.48 ! [Q_2: x_a > state > $o,G_1: hoare_669141180iple_a > $o,C: com,P_5: x_a > state > $o] :
% 0.32/0.48 ( ! [Z: x_a,S: state] :
% 0.32/0.48 ( ( P_5 @ Z @ S )
% 0.32/0.48 => ? [P_6: x_a > state > $o,Q_3: x_a > state > $o] :
% 0.32/0.48 ( ( hoare_2128652938rivs_a @ G_1 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_6 @ C @ Q_3 ) @ bot_bo280939947le_a_o ) )
% 0.32/0.48 & ! [S_1: state] :
% 0.32/0.48 ( ! [Z_6: x_a] :
% 0.32/0.48 ( ( P_6 @ Z_6 @ S )
% 0.32/0.48 => ( Q_3 @ Z_6 @ S_1 ) )
% 0.32/0.48 => ( Q_2 @ Z @ S_1 ) ) ) )
% 0.32/0.48 => ( hoare_2128652938rivs_a @ G_1 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_5 @ C @ Q_2 ) @ bot_bo280939947le_a_o ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_61_nonempty__iff,axiom,
% 0.32/0.48 ! [A_24: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( A_24 != bot_bo280939947le_a_o )
% 0.32/0.48 <=> ? [X_3: hoare_669141180iple_a,B_1: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( A_24
% 0.32/0.48 = ( insert175534902iple_a @ X_3 @ B_1 ) )
% 0.32/0.48 & ~ ( member1016246415iple_a @ X_3 @ B_1 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_62_fold1Set__sing,axiom,
% 0.32/0.48 ! [F_31: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_23: hoare_669141180iple_a,B: hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite840267660iple_a @ F_31 @ ( insert175534902iple_a @ A_23 @ bot_bo280939947le_a_o ) @ B )
% 0.32/0.48 <=> ( A_23 = B ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_63_folding__one_Osingleton,axiom,
% 0.32/0.48 ! [X_14: hoare_669141180iple_a,F_30: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_29: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite972428089iple_a @ F_30 @ F_29 )
% 0.32/0.48 => ( ( F_29 @ ( insert175534902iple_a @ X_14 @ bot_bo280939947le_a_o ) )
% 0.32/0.48 = X_14 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_64_bot__empty__eq,axiom,
% 0.32/0.48 ! [X_3: hoare_669141180iple_a] :
% 0.32/0.48 ( ( bot_bo280939947le_a_o @ X_3 )
% 0.32/0.48 <=> ( member1016246415iple_a @ X_3 @ bot_bo280939947le_a_o ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_65_empty__fold1SetE,axiom,
% 0.32/0.48 ! [F_28: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,X_13: hoare_669141180iple_a] :
% 0.32/0.48 ~ ( finite840267660iple_a @ F_28 @ bot_bo280939947le_a_o @ X_13 ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_66_fold1Set__nonempty,axiom,
% 0.32/0.48 ! [F_27: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_22: hoare_669141180iple_a > $o,X_12: hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite840267660iple_a @ F_27 @ A_22 @ X_12 )
% 0.32/0.48 => ( A_22 != bot_bo280939947le_a_o ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_67_fold1Set_Ointros,axiom,
% 0.32/0.48 ! [F_26: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_21: hoare_669141180iple_a,A_20: hoare_669141180iple_a > $o,X_11: hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite590756294iple_a @ F_26 @ A_21 @ A_20 @ X_11 )
% 0.32/0.48 => ( ~ ( member1016246415iple_a @ A_21 @ A_20 )
% 0.32/0.48 => ( finite840267660iple_a @ F_26 @ ( insert175534902iple_a @ A_21 @ A_20 ) @ X_11 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_68_folding__one_Oinsert,axiom,
% 0.32/0.48 ! [X_10: hoare_669141180iple_a,A_19: hoare_669141180iple_a > $o,F_25: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_24: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite972428089iple_a @ F_25 @ F_24 )
% 0.32/0.48 => ( ( finite957651855iple_a @ A_19 )
% 0.32/0.48 => ( ~ ( member1016246415iple_a @ X_10 @ A_19 )
% 0.32/0.48 => ( ( A_19 != bot_bo280939947le_a_o )
% 0.32/0.48 => ( ( F_24 @ ( insert175534902iple_a @ X_10 @ A_19 ) )
% 0.32/0.48 = ( F_25 @ X_10 @ ( F_24 @ A_19 ) ) ) ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_69_fold1__def,axiom,
% 0.32/0.48 ! [F_23: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_18: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( finite684844060iple_a @ F_23 @ A_18 )
% 0.32/0.48 = ( the_Ho49089901iple_a @ ( finite840267660iple_a @ F_23 @ A_18 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_70_finite__Collect__conjI,axiom,
% 0.32/0.48 ! [Q_1: hoare_669141180iple_a > $o,P_4: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( ( finite957651855iple_a @ ( collec1717965009iple_a @ P_4 ) )
% 0.32/0.48 | ( finite957651855iple_a @ ( collec1717965009iple_a @ Q_1 ) ) )
% 0.32/0.48 => ( finite957651855iple_a
% 0.32/0.48 @ ( collec1717965009iple_a
% 0.32/0.48 @ ^ [X_3: hoare_669141180iple_a] : ( (&) @ ( P_4 @ X_3 ) @ ( Q_1 @ X_3 ) ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_71_finite_OemptyI,axiom,
% 0.32/0.48 finite957651855iple_a @ bot_bo280939947le_a_o ).
% 0.32/0.48
% 0.32/0.48 thf(fact_72_finite_OinsertI,axiom,
% 0.32/0.48 ! [A_17: hoare_669141180iple_a,A_16: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( finite957651855iple_a @ A_16 )
% 0.32/0.48 => ( finite957651855iple_a @ ( insert175534902iple_a @ A_17 @ A_16 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_73_mem__def,axiom,
% 0.32/0.48 ! [X_9: hoare_669141180iple_a,A_15: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( member1016246415iple_a @ X_9 @ A_15 )
% 0.32/0.48 <=> ( A_15 @ X_9 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_74_Collect__def,axiom,
% 0.32/0.48 ! [P_3: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( collec1717965009iple_a @ P_3 )
% 0.32/0.48 = P_3 ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_75_folding__one_Oeq__fold,axiom,
% 0.32/0.48 ! [A_14: hoare_669141180iple_a > $o,F_22: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_21: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite972428089iple_a @ F_22 @ F_21 )
% 0.32/0.48 => ( ( finite957651855iple_a @ A_14 )
% 0.32/0.48 => ( ( F_21 @ A_14 )
% 0.32/0.48 = ( finite684844060iple_a @ F_22 @ A_14 ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_76_fold__graph_OemptyI,axiom,
% 0.32/0.48 ! [F_20: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,Z_5: hoare_669141180iple_a] : ( finite590756294iple_a @ F_20 @ Z_5 @ bot_bo280939947le_a_o @ Z_5 ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_77_empty__fold__graphE,axiom,
% 0.32/0.48 ! [F_19: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,Z_4: hoare_669141180iple_a,X_8: hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite590756294iple_a @ F_19 @ Z_4 @ bot_bo280939947le_a_o @ X_8 )
% 0.32/0.48 => ( X_8 = Z_4 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_78_fold__graph_OinsertI,axiom,
% 0.32/0.48 ! [F_18: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,Z_3: hoare_669141180iple_a,Y_2: hoare_669141180iple_a,X_7: hoare_669141180iple_a,A_13: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ~ ( member1016246415iple_a @ X_7 @ A_13 )
% 0.32/0.48 => ( ( finite590756294iple_a @ F_18 @ Z_3 @ A_13 @ Y_2 )
% 0.32/0.48 => ( finite590756294iple_a @ F_18 @ Z_3 @ ( insert175534902iple_a @ X_7 @ A_13 ) @ ( F_18 @ X_7 @ Y_2 ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_79_finite__Collect__disjI,axiom,
% 0.32/0.48 ! [P_2: hoare_669141180iple_a > $o,Q: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( finite957651855iple_a
% 0.32/0.48 @ ( collec1717965009iple_a
% 0.32/0.48 @ ^ [X_3: hoare_669141180iple_a] : ( (|) @ ( P_2 @ X_3 ) @ ( Q @ X_3 ) ) ) )
% 0.32/0.48 <=> ( ( finite957651855iple_a @ ( collec1717965009iple_a @ P_2 ) )
% 0.32/0.48 & ( finite957651855iple_a @ ( collec1717965009iple_a @ Q ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_80_finite__insert,axiom,
% 0.32/0.48 ! [A_12: hoare_669141180iple_a,A_11: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( finite957651855iple_a @ ( insert175534902iple_a @ A_12 @ A_11 ) )
% 0.32/0.48 <=> ( finite957651855iple_a @ A_11 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_81_fold1__singleton__def,axiom,
% 0.32/0.48 ! [A_10: hoare_669141180iple_a,G: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a,F_17: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a] :
% 0.32/0.48 ( ( G
% 0.32/0.48 = ( finite684844060iple_a @ F_17 ) )
% 0.32/0.48 => ( ( G @ ( insert175534902iple_a @ A_10 @ bot_bo280939947le_a_o ) )
% 0.32/0.48 = A_10 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_82_fold1__singleton,axiom,
% 0.32/0.48 ! [F_16: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_9: hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite684844060iple_a @ F_16 @ ( insert175534902iple_a @ A_9 @ bot_bo280939947le_a_o ) )
% 0.32/0.48 = A_9 ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_83_folding__one_Oclosed,axiom,
% 0.32/0.48 ! [A_8: hoare_669141180iple_a > $o,F_15: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_14: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite972428089iple_a @ F_15 @ F_14 )
% 0.32/0.48 => ( ( finite957651855iple_a @ A_8 )
% 0.32/0.48 => ( ( A_8 != bot_bo280939947le_a_o )
% 0.32/0.48 => ( ! [X_3: hoare_669141180iple_a,Y_1: hoare_669141180iple_a] : ( member1016246415iple_a @ ( F_15 @ X_3 @ Y_1 ) @ ( insert175534902iple_a @ X_3 @ ( insert175534902iple_a @ Y_1 @ bot_bo280939947le_a_o ) ) )
% 0.32/0.48 => ( member1016246415iple_a @ ( F_14 @ A_8 ) @ A_8 ) ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_84_insert__fold1SetE,axiom,
% 0.32/0.48 ! [F_13: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_7: hoare_669141180iple_a,X_6: hoare_669141180iple_a > $o,X_5: hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite840267660iple_a @ F_13 @ ( insert175534902iple_a @ A_7 @ X_6 ) @ X_5 )
% 0.32/0.48 => ~ ! [A_3: hoare_669141180iple_a,A_2: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( ( insert175534902iple_a @ A_7 @ X_6 )
% 0.32/0.48 = ( insert175534902iple_a @ A_3 @ A_2 ) )
% 0.32/0.48 => ( ( finite590756294iple_a @ F_13 @ A_3 @ A_2 @ X_5 )
% 0.32/0.48 => ( member1016246415iple_a @ A_3 @ A_2 ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_85_finite__nonempty__imp__fold1Set,axiom,
% 0.32/0.48 ! [F_12: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_6: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( finite957651855iple_a @ A_6 )
% 0.32/0.48 => ( ( A_6 != bot_bo280939947le_a_o )
% 0.32/0.48 => ( ex @ ( finite840267660iple_a @ F_12 @ A_6 ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_86_finite__induct,axiom,
% 0.32/0.48 ! [P_1: ( hoare_669141180iple_a > $o ) > $o,F_11: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( finite957651855iple_a @ F_11 )
% 0.32/0.48 => ( ( P_1 @ bot_bo280939947le_a_o )
% 0.32/0.48 => ( ! [X_3: hoare_669141180iple_a,F_5: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( finite957651855iple_a @ F_5 )
% 0.32/0.48 => ( ~ ( member1016246415iple_a @ X_3 @ F_5 )
% 0.32/0.48 => ( ( P_1 @ F_5 )
% 0.32/0.48 => ( P_1 @ ( insert175534902iple_a @ X_3 @ F_5 ) ) ) ) )
% 0.32/0.48 => ( P_1 @ F_11 ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_87_finite_Osimps,axiom,
% 0.32/0.48 ! [A_5: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( finite957651855iple_a @ A_5 )
% 0.32/0.48 <=> ( ( A_5 = bot_bo280939947le_a_o )
% 0.32/0.48 | ? [A_2: hoare_669141180iple_a > $o,A_3: hoare_669141180iple_a] :
% 0.32/0.48 ( ( A_5
% 0.32/0.48 = ( insert175534902iple_a @ A_3 @ A_2 ) )
% 0.32/0.48 & ( finite957651855iple_a @ A_2 ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_88_finite__imp__fold__graph,axiom,
% 0.32/0.48 ! [F_10: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,Z_2: hoare_669141180iple_a,A_4: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( finite957651855iple_a @ A_4 )
% 0.32/0.48 => ( ex @ ( finite590756294iple_a @ F_10 @ Z_2 @ A_4 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_89_fold1Set_Osimps,axiom,
% 0.32/0.48 ! [F_9: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A1_1: hoare_669141180iple_a > $o,A2_1: hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite840267660iple_a @ F_9 @ A1_1 @ A2_1 )
% 0.32/0.48 <=> ? [A_3: hoare_669141180iple_a,A_2: hoare_669141180iple_a > $o,X_3: hoare_669141180iple_a] :
% 0.32/0.48 ( ( A1_1
% 0.32/0.48 = ( insert175534902iple_a @ A_3 @ A_2 ) )
% 0.32/0.48 & ( A2_1 = X_3 )
% 0.32/0.48 & ( finite590756294iple_a @ F_9 @ A_3 @ A_2 @ X_3 )
% 0.32/0.48 & ~ ( member1016246415iple_a @ A_3 @ A_2 ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_90_fold__graph_Osimps,axiom,
% 0.32/0.48 ! [F_8: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,Z_1: hoare_669141180iple_a,A1: hoare_669141180iple_a > $o,A2: hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite590756294iple_a @ F_8 @ Z_1 @ A1 @ A2 )
% 0.32/0.48 <=> ( ( ( A1 = bot_bo280939947le_a_o )
% 0.32/0.48 & ( A2 = Z_1 ) )
% 0.32/0.48 | ? [X_3: hoare_669141180iple_a,A_2: hoare_669141180iple_a > $o,Y_1: hoare_669141180iple_a] :
% 0.32/0.48 ( ( A1
% 0.32/0.48 = ( insert175534902iple_a @ X_3 @ A_2 ) )
% 0.32/0.48 & ( A2
% 0.32/0.48 = ( F_8 @ X_3 @ Y_1 ) )
% 0.32/0.48 & ~ ( member1016246415iple_a @ X_3 @ A_2 )
% 0.32/0.48 & ( finite590756294iple_a @ F_8 @ Z_1 @ A_2 @ Y_1 ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_91_folding__one__idem_Oinsert__idem,axiom,
% 0.32/0.48 ! [X_4: hoare_669141180iple_a,A_1: hoare_669141180iple_a > $o,F_7: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_6: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite252461622iple_a @ F_7 @ F_6 )
% 0.32/0.48 => ( ( finite957651855iple_a @ A_1 )
% 0.32/0.48 => ( ( A_1 != bot_bo280939947le_a_o )
% 0.32/0.48 => ( ( F_6 @ ( insert175534902iple_a @ X_4 @ A_1 ) )
% 0.32/0.48 = ( F_7 @ X_4 @ ( F_6 @ A_1 ) ) ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_92_finite__ne__induct,axiom,
% 0.32/0.48 ! [P: ( hoare_669141180iple_a > $o ) > $o,F_4: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( finite957651855iple_a @ F_4 )
% 0.32/0.48 => ( ( F_4 != bot_bo280939947le_a_o )
% 0.32/0.48 => ( ! [X_3: hoare_669141180iple_a] : ( P @ ( insert175534902iple_a @ X_3 @ bot_bo280939947le_a_o ) )
% 0.32/0.48 => ( ! [X_3: hoare_669141180iple_a,F_5: hoare_669141180iple_a > $o] :
% 0.32/0.48 ( ( finite957651855iple_a @ F_5 )
% 0.32/0.48 => ( ( F_5 != bot_bo280939947le_a_o )
% 0.32/0.48 => ( ~ ( member1016246415iple_a @ X_3 @ F_5 )
% 0.32/0.48 => ( ( P @ F_5 )
% 0.32/0.48 => ( P @ ( insert175534902iple_a @ X_3 @ F_5 ) ) ) ) ) )
% 0.32/0.48 => ( P @ F_4 ) ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_93_folding__one__idem_Oidem,axiom,
% 0.32/0.48 ! [X_2: hoare_669141180iple_a,F_3: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_2: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite252461622iple_a @ F_3 @ F_2 )
% 0.32/0.48 => ( ( F_3 @ X_2 @ X_2 )
% 0.32/0.48 = X_2 ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(fact_94_folding__one__idem_Oin__idem,axiom,
% 0.32/0.48 ! [X_1: hoare_669141180iple_a,A: hoare_669141180iple_a > $o,F_1: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 0.32/0.48 ( ( finite252461622iple_a @ F_1 @ F )
% 0.32/0.48 => ( ( finite957651855iple_a @ A )
% 0.32/0.48 => ( ( member1016246415iple_a @ X_1 @ A )
% 0.32/0.48 => ( ( F_1 @ X_1 @ ( F @ A ) )
% 0.32/0.48 = ( F @ A ) ) ) ) ) ).
% 0.32/0.48
% 0.32/0.48 %----Helper facts (2)
% 0.32/0.48 thf(help_fequal_1_1_fequal_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J_,axiom,
% 0.32/0.48 ! [X: hoare_669141180iple_a,Y: hoare_669141180iple_a] :
% 0.32/0.48 ( ~ ( fequal182287803iple_a @ X @ Y )
% 0.32/0.48 | ( X = Y ) ) ).
% 0.32/0.48
% 0.32/0.48 thf(help_fequal_2_1_fequal_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J_,axiom,
% 0.32/0.48 ! [X: hoare_669141180iple_a,Y: hoare_669141180iple_a] :
% 0.32/0.48 ( ( X != Y )
% 0.32/0.48 | ( fequal182287803iple_a @ X @ Y ) ) ).
% 0.32/0.48
% 0.32/0.48 %----Conjectures (1)
% 0.32/0.48 thf(conj_0,conjecture,
% 0.32/0.48 ( hoare_2128652938rivs_a @ g
% 0.32/0.48 @ ( insert175534902iple_a
% 0.32/0.48 @ ( hoare_1295064928iple_a
% 0.32/0.48 @ ^ [Z: x_a,S: state] : $false
% 0.32/0.48 @ c
% 0.32/0.48 @ ^ [Z: x_a,S: state] : ( (&) @ ( p @ Z @ S ) @ ( (~) @ ( b @ S ) ) ) )
% 0.32/0.48 @ bot_bo280939947le_a_o ) ) ).
% 0.32/0.48
% 0.32/0.48 %------------------------------------------------------------------------------
% 0.32/0.48 ------------------------
% 2.85/1.82 ---- Embedded in THF ---
% 2.85/1.82 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 2.85/1.82 %%% Generated on Tue Feb 24 13:40:04 EST 2026
% 2.85/1.82 %%% using '$$dhol' embedding, version 1.3.0.
% 2.85/1.82 %%% Logic specification used:
% 2.85/1.82 %%% thf(spec, logic, $$dhol).
% 2.85/1.82
% 2.85/1.82 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.oU5Hx1ZbCZ/DTF2DTF26033.p
% See solution above
% 2.85/1.82 ------------------------
% 2.85/1.84 ---- Cleaned THF ---
% 2.85/1.84 thf(ty_ty_t__a,type,
% 2.85/1.84 x_a: $tType ).
% 2.85/1.84
% 2.85/1.84 thf(ty_ty_tc__Com__Ocom,type,
% 2.85/1.84 com: $tType ).
% 2.85/1.84
% 2.85/1.84 thf(ty_ty_tc__Com__Ostate,type,
% 2.85/1.84 state: $tType ).
% 2.85/1.84
% 2.85/1.84 thf(ty_ty_tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 2.85/1.84 hoare_669141180iple_a: $tType ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Com_Ocom_OSKIP,type,
% 2.85/1.84 skip: com ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Com_Ocom_OSemi,type,
% 2.85/1.84 semi: com > com > com ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Ex,type,
% 2.85/1.84 ex: ( hoare_669141180iple_a > $o ) > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Finite__Set_Ofinite_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_,type,
% 2.85/1.84 finite957651855iple_a: ( hoare_669141180iple_a > $o ) > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Finite__Set_Ofold1Set_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__,type,
% 2.85/1.84 finite840267660iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Finite__Set_Ofold1_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 2.85/1.84 finite684844060iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Finite__Set_Ofold__graph_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_I,type,
% 2.85/1.84 finite590756294iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Finite__Set_Ofolding__one_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_,type,
% 2.85/1.84 finite972428089iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ) > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Finite__Set_Ofolding__one__idem_000tc__Hoare____Mirabelle____ghhkfsbqqq__Ot,type,
% 2.85/1.84 finite252461622iple_a: ( hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a ) > ( ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ) > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_HOL_OThe_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 2.85/1.84 the_Ho49089901iple_a: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Hoare__Mirabelle__ghhkfsbqqq_Ohoare__derivs_000t__a,type,
% 2.85/1.84 hoare_2128652938rivs_a: ( hoare_669141180iple_a > $o ) > ( hoare_669141180iple_a > $o ) > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Hoare__Mirabelle__ghhkfsbqqq_Otriple_Otriple_000t__a,type,
% 2.85/1.84 hoare_1295064928iple_a: ( x_a > state > $o ) > com > ( x_a > state > $o ) > hoare_669141180iple_a ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Orderings_Obot__class_Obot_000_062_Itc__Hoare____Mirabelle____ghhkfsbqqq__O,type,
% 2.85/1.84 bot_bo280939947le_a_o: hoare_669141180iple_a > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Orderings_Obot__class_Obot_000_Eo,type,
% 2.85/1.84 bot_bot_o: $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Set_OCollect_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 2.85/1.84 collec1717965009iple_a: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Set_Oinsert_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 2.85/1.84 insert175534902iple_a: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_Set_Othe__elem_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 2.85/1.84 the_el738790235iple_a: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_fequal_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 2.85/1.84 fequal182287803iple_a: hoare_669141180iple_a > hoare_669141180iple_a > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_c_member_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J,type,
% 2.85/1.84 member1016246415iple_a: hoare_669141180iple_a > ( hoare_669141180iple_a > $o ) > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_v_G,type,
% 2.85/1.84 g: hoare_669141180iple_a > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_v_P,type,
% 2.85/1.84 p: x_a > state > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_v_b,type,
% 2.85/1.84 b: state > $o ).
% 2.85/1.84
% 2.85/1.84 thf(sy_v_c,type,
% 2.85/1.84 c: com ).
% 2.85/1.84
% 2.85/1.84 thf(fact_0_empty,axiom,
% 2.85/1.84 ! [G_12: hoare_669141180iple_a > $o] : ( hoare_2128652938rivs_a @ G_12 @ bot_bo280939947le_a_o ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_1_triple_Oinject,axiom,
% 2.85/1.84 ! [Fun1_2: x_a > state > $o,Com_2: com,Fun2_2: x_a > state > $o,Fun1_1: x_a > state > $o,Com_1: com,Fun2_1: x_a > state > $o] :
% 2.85/1.84 ( ( ( hoare_1295064928iple_a @ Fun1_2 @ Com_2 @ Fun2_2 )
% 2.85/1.84 = ( hoare_1295064928iple_a @ Fun1_1 @ Com_1 @ Fun2_1 ) )
% 2.85/1.84 <=> ( ( Fun1_2 = Fun1_1 )
% 2.85/1.84 & ( Com_2 = Com_1 )
% 2.85/1.84 & ( Fun2_2 = Fun2_1 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_2_cut,axiom,
% 2.85/1.84 ! [G_11: hoare_669141180iple_a > $o,G_10: hoare_669141180iple_a > $o,Ts_1: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( hoare_2128652938rivs_a @ G_10 @ Ts_1 )
% 2.85/1.84 => ( ( hoare_2128652938rivs_a @ G_11 @ G_10 )
% 2.85/1.84 => ( hoare_2128652938rivs_a @ G_11 @ Ts_1 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_3_hoare__derivs_Oinsert,axiom,
% 2.85/1.84 ! [Ts: hoare_669141180iple_a > $o,G_9: hoare_669141180iple_a > $o,T: hoare_669141180iple_a] :
% 2.85/1.84 ( ( hoare_2128652938rivs_a @ G_9 @ ( insert175534902iple_a @ T @ bot_bo280939947le_a_o ) )
% 2.85/1.84 => ( ( hoare_2128652938rivs_a @ G_9 @ Ts )
% 2.85/1.84 => ( hoare_2128652938rivs_a @ G_9 @ ( insert175534902iple_a @ T @ Ts ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_4_constant,axiom,
% 2.85/1.84 ! [G_8: hoare_669141180iple_a > $o,P_25: x_a > state > $o,C_9: com,Q_11: x_a > state > $o,C_8: $o] :
% 2.85/1.84 ( ( C_8
% 2.85/1.84 => ( hoare_2128652938rivs_a @ G_8 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_25 @ C_9 @ Q_11 ) @ bot_bo280939947le_a_o ) ) )
% 2.85/1.84 => ( hoare_2128652938rivs_a @ G_8
% 2.85/1.84 @ ( insert175534902iple_a
% 2.85/1.84 @ ( hoare_1295064928iple_a
% 2.85/1.84 @ ^ [Z: x_a,S: state] : ( (&) @ ( P_25 @ Z @ S ) @ C_8 )
% 2.85/1.84 @ C_9
% 2.85/1.84 @ Q_11 )
% 2.85/1.84 @ bot_bo280939947le_a_o ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_5_escape,axiom,
% 2.85/1.84 ! [G_7: hoare_669141180iple_a > $o,C_7: com,Q_10: x_a > state > $o,P_24: x_a > state > $o] :
% 2.85/1.84 ( ! [Z: x_a,S: state] :
% 2.85/1.84 ( ( P_24 @ Z @ S )
% 2.85/1.84 => ( hoare_2128652938rivs_a @ G_7
% 2.85/1.84 @ ( insert175534902iple_a
% 2.85/1.84 @ ( hoare_1295064928iple_a
% 2.85/1.84 @ ^ [Za: x_a,S_1: state] : ( S_1 = S )
% 2.85/1.84 @ C_7
% 2.85/1.84 @ ^ [Z_6: x_a] : ( Q_10 @ Z ) )
% 2.85/1.84 @ bot_bo280939947le_a_o ) ) )
% 2.85/1.84 => ( hoare_2128652938rivs_a @ G_7 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_24 @ C_7 @ Q_10 ) @ bot_bo280939947le_a_o ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_6_conseq2,axiom,
% 2.85/1.84 ! [Q_9: x_a > state > $o,G_6: hoare_669141180iple_a > $o,P_23: x_a > state > $o,C_6: com,Q_8: x_a > state > $o] :
% 2.85/1.84 ( ( hoare_2128652938rivs_a @ G_6 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_23 @ C_6 @ Q_8 ) @ bot_bo280939947le_a_o ) )
% 2.85/1.84 => ( ! [Z: x_a,S: state] :
% 2.85/1.84 ( ( Q_8 @ Z @ S )
% 2.85/1.84 => ( Q_9 @ Z @ S ) )
% 2.85/1.84 => ( hoare_2128652938rivs_a @ G_6 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_23 @ C_6 @ Q_9 ) @ bot_bo280939947le_a_o ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_7_conseq1,axiom,
% 2.85/1.84 ! [P_22: x_a > state > $o,G_5: hoare_669141180iple_a > $o,P_21: x_a > state > $o,C_5: com,Q_7: x_a > state > $o] :
% 2.85/1.84 ( ( hoare_2128652938rivs_a @ G_5 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_21 @ C_5 @ Q_7 ) @ bot_bo280939947le_a_o ) )
% 2.85/1.84 => ( ! [Z: x_a,S: state] :
% 2.85/1.84 ( ( P_22 @ Z @ S )
% 2.85/1.84 => ( P_21 @ Z @ S ) )
% 2.85/1.84 => ( hoare_2128652938rivs_a @ G_5 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_22 @ C_5 @ Q_7 ) @ bot_bo280939947le_a_o ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_8_conseq12,axiom,
% 2.85/1.84 ! [Q_6: x_a > state > $o,P_20: x_a > state > $o,G_4: hoare_669141180iple_a > $o,P_19: x_a > state > $o,C_4: com,Q_5: x_a > state > $o] :
% 2.85/1.84 ( ( hoare_2128652938rivs_a @ G_4 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_19 @ C_4 @ Q_5 ) @ bot_bo280939947le_a_o ) )
% 2.85/1.84 => ( ! [Z: x_a,S: state] :
% 2.85/1.84 ( ( P_20 @ Z @ S )
% 2.85/1.84 => ! [S_1: state] :
% 2.85/1.84 ( ! [Z_6: x_a] :
% 2.85/1.84 ( ( P_19 @ Z_6 @ S )
% 2.85/1.84 => ( Q_5 @ Z_6 @ S_1 ) )
% 2.85/1.84 => ( Q_6 @ Z @ S_1 ) ) )
% 2.85/1.84 => ( hoare_2128652938rivs_a @ G_4 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_20 @ C_4 @ Q_6 ) @ bot_bo280939947le_a_o ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_9_insertE,axiom,
% 2.85/1.84 ! [A_64: hoare_669141180iple_a,B_14: hoare_669141180iple_a,A_63: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( member1016246415iple_a @ A_64 @ ( insert175534902iple_a @ B_14 @ A_63 ) )
% 2.85/1.84 => ( ( A_64 != B_14 )
% 2.85/1.84 => ( member1016246415iple_a @ A_64 @ A_63 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_10_insertCI,axiom,
% 2.85/1.84 ! [B_13: hoare_669141180iple_a,A_62: hoare_669141180iple_a,B_12: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( ~ ( member1016246415iple_a @ A_62 @ B_12 )
% 2.85/1.84 => ( A_62 = B_13 ) )
% 2.85/1.84 => ( member1016246415iple_a @ A_62 @ ( insert175534902iple_a @ B_13 @ B_12 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_11_emptyE,axiom,
% 2.85/1.84 ! [A_61: hoare_669141180iple_a] :
% 2.85/1.84 ~ ( member1016246415iple_a @ A_61 @ bot_bo280939947le_a_o ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_12_singleton__conv2,axiom,
% 2.85/1.84 ! [A_60: hoare_669141180iple_a] :
% 2.85/1.84 ( ( collec1717965009iple_a @ ( fequal182287803iple_a @ A_60 ) )
% 2.85/1.84 = ( insert175534902iple_a @ A_60 @ bot_bo280939947le_a_o ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_13_singleton__conv,axiom,
% 2.85/1.84 ! [A_59: hoare_669141180iple_a] :
% 2.85/1.84 ( ( collec1717965009iple_a
% 2.85/1.84 @ ^ [X_3: hoare_669141180iple_a] : ( X_3 = A_59 ) )
% 2.85/1.84 = ( insert175534902iple_a @ A_59 @ bot_bo280939947le_a_o ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_14_Collect__conv__if2,axiom,
% 2.85/1.84 ! [P_18: hoare_669141180iple_a > $o,A_58: hoare_669141180iple_a] :
% 2.85/1.84 ( ( ( P_18 @ A_58 )
% 2.85/1.84 => ( ( collec1717965009iple_a
% 2.85/1.84 @ ^ [X_3: hoare_669141180iple_a] : ( (&) @ ( A_58 = X_3 ) @ ( P_18 @ X_3 ) ) )
% 2.85/1.84 = ( insert175534902iple_a @ A_58 @ bot_bo280939947le_a_o ) ) )
% 2.85/1.84 & ( ~ ( P_18 @ A_58 )
% 2.85/1.84 => ( ( collec1717965009iple_a
% 2.85/1.84 @ ^ [X_3: hoare_669141180iple_a] : ( (&) @ ( A_58 = X_3 ) @ ( P_18 @ X_3 ) ) )
% 2.85/1.84 = bot_bo280939947le_a_o ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_15_Collect__conv__if,axiom,
% 2.85/1.84 ! [P_17: hoare_669141180iple_a > $o,A_57: hoare_669141180iple_a] :
% 2.85/1.84 ( ( ( P_17 @ A_57 )
% 2.85/1.84 => ( ( collec1717965009iple_a
% 2.85/1.84 @ ^ [X_3: hoare_669141180iple_a] : ( (&) @ ( X_3 = A_57 ) @ ( P_17 @ X_3 ) ) )
% 2.85/1.84 = ( insert175534902iple_a @ A_57 @ bot_bo280939947le_a_o ) ) )
% 2.85/1.84 & ( ~ ( P_17 @ A_57 )
% 2.85/1.84 => ( ( collec1717965009iple_a
% 2.85/1.84 @ ^ [X_3: hoare_669141180iple_a] : ( (&) @ ( X_3 = A_57 ) @ ( P_17 @ X_3 ) ) )
% 2.85/1.84 = bot_bo280939947le_a_o ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_16_equals0D,axiom,
% 2.85/1.84 ! [A_56: hoare_669141180iple_a,A_55: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( A_55 = bot_bo280939947le_a_o )
% 2.85/1.84 => ~ ( member1016246415iple_a @ A_56 @ A_55 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_17_Collect__empty__eq,axiom,
% 2.85/1.84 ! [P_16: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( ( collec1717965009iple_a @ P_16 )
% 2.85/1.84 = bot_bo280939947le_a_o )
% 2.85/1.84 <=> ! [X_3: hoare_669141180iple_a] :
% 2.85/1.84 ~ ( P_16 @ X_3 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_18_empty__iff,axiom,
% 2.85/1.84 ! [C_3: hoare_669141180iple_a] :
% 2.85/1.84 ~ ( member1016246415iple_a @ C_3 @ bot_bo280939947le_a_o ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_19_empty__Collect__eq,axiom,
% 2.85/1.84 ! [P_15: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( bot_bo280939947le_a_o
% 2.85/1.84 = ( collec1717965009iple_a @ P_15 ) )
% 2.85/1.84 <=> ! [X_3: hoare_669141180iple_a] :
% 2.85/1.84 ~ ( P_15 @ X_3 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_20_ex__in__conv,axiom,
% 2.85/1.84 ! [A_54: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ? [X_3: hoare_669141180iple_a] : ( member1016246415iple_a @ X_3 @ A_54 )
% 2.85/1.84 <=> ( A_54 != bot_bo280939947le_a_o ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_21_all__not__in__conv,axiom,
% 2.85/1.84 ! [A_53: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ! [X_3: hoare_669141180iple_a] :
% 2.85/1.84 ~ ( member1016246415iple_a @ X_3 @ A_53 )
% 2.85/1.84 <=> ( A_53 = bot_bo280939947le_a_o ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_22_empty__def,axiom,
% 2.85/1.84 ( bot_bo280939947le_a_o
% 2.85/1.84 = ( collec1717965009iple_a
% 2.85/1.84 @ ^ [X_3: hoare_669141180iple_a] : $false ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_23_insert__absorb,axiom,
% 2.85/1.84 ! [A_52: hoare_669141180iple_a,A_51: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( member1016246415iple_a @ A_52 @ A_51 )
% 2.85/1.84 => ( ( insert175534902iple_a @ A_52 @ A_51 )
% 2.85/1.84 = A_51 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_24_insertI2,axiom,
% 2.85/1.84 ! [B_11: hoare_669141180iple_a,A_50: hoare_669141180iple_a,B_10: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( member1016246415iple_a @ A_50 @ B_10 )
% 2.85/1.84 => ( member1016246415iple_a @ A_50 @ ( insert175534902iple_a @ B_11 @ B_10 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_25_insert__ident,axiom,
% 2.85/1.84 ! [B_9: hoare_669141180iple_a > $o,X_24: hoare_669141180iple_a,A_49: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ~ ( member1016246415iple_a @ X_24 @ A_49 )
% 2.85/1.84 => ( ~ ( member1016246415iple_a @ X_24 @ B_9 )
% 2.85/1.84 => ( ( ( insert175534902iple_a @ X_24 @ A_49 )
% 2.85/1.84 = ( insert175534902iple_a @ X_24 @ B_9 ) )
% 2.85/1.84 <=> ( A_49 = B_9 ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_26_insert__code,axiom,
% 2.85/1.84 ! [Y_6: hoare_669141180iple_a,A_48: hoare_669141180iple_a > $o,X_23: hoare_669141180iple_a] :
% 2.85/1.84 ( ( insert175534902iple_a @ Y_6 @ A_48 @ X_23 )
% 2.85/1.84 <=> ( ( Y_6 = X_23 )
% 2.85/1.84 | ( A_48 @ X_23 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_27_insert__iff,axiom,
% 2.85/1.84 ! [A_47: hoare_669141180iple_a,B_8: hoare_669141180iple_a,A_46: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( member1016246415iple_a @ A_47 @ ( insert175534902iple_a @ B_8 @ A_46 ) )
% 2.85/1.84 <=> ( ( A_47 = B_8 )
% 2.85/1.84 | ( member1016246415iple_a @ A_47 @ A_46 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_28_insert__commute,axiom,
% 2.85/1.84 ! [X_22: hoare_669141180iple_a,Y_5: hoare_669141180iple_a,A_45: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( insert175534902iple_a @ X_22 @ ( insert175534902iple_a @ Y_5 @ A_45 ) )
% 2.85/1.84 = ( insert175534902iple_a @ Y_5 @ ( insert175534902iple_a @ X_22 @ A_45 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_29_insert__absorb2,axiom,
% 2.85/1.84 ! [X_21: hoare_669141180iple_a,A_44: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( insert175534902iple_a @ X_21 @ ( insert175534902iple_a @ X_21 @ A_44 ) )
% 2.85/1.84 = ( insert175534902iple_a @ X_21 @ A_44 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_30_insert__Collect,axiom,
% 2.85/1.84 ! [A_43: hoare_669141180iple_a,P_14: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( insert175534902iple_a @ A_43 @ ( collec1717965009iple_a @ P_14 ) )
% 2.85/1.84 = ( collec1717965009iple_a
% 2.85/1.84 @ ^ [U: hoare_669141180iple_a] : ( (=>) @ ( (~) @ ( U = A_43 ) ) @ ( P_14 @ U ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_31_insert__compr,axiom,
% 2.85/1.84 ! [A_42: hoare_669141180iple_a,B_7: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( insert175534902iple_a @ A_42 @ B_7 )
% 2.85/1.84 = ( collec1717965009iple_a
% 2.85/1.84 @ ^ [X_3: hoare_669141180iple_a] : ( (|) @ ( X_3 = A_42 ) @ ( member1016246415iple_a @ X_3 @ B_7 ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_32_insertI1,axiom,
% 2.85/1.84 ! [A_41: hoare_669141180iple_a,B_6: hoare_669141180iple_a > $o] : ( member1016246415iple_a @ A_41 @ ( insert175534902iple_a @ A_41 @ B_6 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_33_insert__compr__raw,axiom,
% 2.85/1.84 ! [X_3: hoare_669141180iple_a,Xa: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( insert175534902iple_a @ X_3 @ Xa )
% 2.85/1.84 = ( collec1717965009iple_a
% 2.85/1.84 @ ^ [Y_1: hoare_669141180iple_a] : ( (|) @ ( Y_1 = X_3 ) @ ( member1016246415iple_a @ Y_1 @ Xa ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_34_singleton__inject,axiom,
% 2.85/1.84 ! [A_40: hoare_669141180iple_a,B_5: hoare_669141180iple_a] :
% 2.85/1.84 ( ( ( insert175534902iple_a @ A_40 @ bot_bo280939947le_a_o )
% 2.85/1.84 = ( insert175534902iple_a @ B_5 @ bot_bo280939947le_a_o ) )
% 2.85/1.84 => ( A_40 = B_5 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_35_singletonE,axiom,
% 2.85/1.84 ! [B_4: hoare_669141180iple_a,A_39: hoare_669141180iple_a] :
% 2.85/1.84 ( ( member1016246415iple_a @ B_4 @ ( insert175534902iple_a @ A_39 @ bot_bo280939947le_a_o ) )
% 2.85/1.84 => ( B_4 = A_39 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_36_doubleton__eq__iff,axiom,
% 2.85/1.84 ! [A_38: hoare_669141180iple_a,B_3: hoare_669141180iple_a,C_2: hoare_669141180iple_a,D_1: hoare_669141180iple_a] :
% 2.85/1.84 ( ( ( insert175534902iple_a @ A_38 @ ( insert175534902iple_a @ B_3 @ bot_bo280939947le_a_o ) )
% 2.85/1.84 = ( insert175534902iple_a @ C_2 @ ( insert175534902iple_a @ D_1 @ bot_bo280939947le_a_o ) ) )
% 2.85/1.84 <=> ( ( ( A_38 = C_2 )
% 2.85/1.84 & ( B_3 = D_1 ) )
% 2.85/1.84 | ( ( A_38 = D_1 )
% 2.85/1.84 & ( B_3 = C_2 ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_37_singleton__iff,axiom,
% 2.85/1.84 ! [B_2: hoare_669141180iple_a,A_37: hoare_669141180iple_a] :
% 2.85/1.84 ( ( member1016246415iple_a @ B_2 @ ( insert175534902iple_a @ A_37 @ bot_bo280939947le_a_o ) )
% 2.85/1.84 <=> ( B_2 = A_37 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_38_insert__not__empty,axiom,
% 2.85/1.84 ! [A_36: hoare_669141180iple_a,A_35: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( insert175534902iple_a @ A_36 @ A_35 )
% 2.85/1.84 != bot_bo280939947le_a_o ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_39_empty__not__insert,axiom,
% 2.85/1.84 ! [A_34: hoare_669141180iple_a,A_33: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( bot_bo280939947le_a_o
% 2.85/1.84 != ( insert175534902iple_a @ A_34 @ A_33 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_40_the__elem__eq,axiom,
% 2.85/1.84 ! [X_20: hoare_669141180iple_a] :
% 2.85/1.84 ( ( the_el738790235iple_a @ ( insert175534902iple_a @ X_20 @ bot_bo280939947le_a_o ) )
% 2.85/1.84 = X_20 ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_41_bot__apply,axiom,
% 2.85/1.84 ! [X_19: hoare_669141180iple_a] :
% 2.85/1.84 ( ( bot_bo280939947le_a_o @ X_19 )
% 2.85/1.84 <=> bot_bot_o ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_42_bot__fun__def,axiom,
% 2.85/1.84 ! [X_3: hoare_669141180iple_a] :
% 2.85/1.84 ( ( bot_bo280939947le_a_o @ X_3 )
% 2.85/1.84 <=> bot_bot_o ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_43_hoare__derivs_OSkip,axiom,
% 2.85/1.84 ! [G_3: hoare_669141180iple_a > $o,P_13: x_a > state > $o] : ( hoare_2128652938rivs_a @ G_3 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_13 @ skip @ P_13 ) @ bot_bo280939947le_a_o ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_44_Comp,axiom,
% 2.85/1.84 ! [D: com,R: x_a > state > $o,G_2: hoare_669141180iple_a > $o,P_12: x_a > state > $o,C_1: com,Q_4: x_a > state > $o] :
% 2.85/1.84 ( ( hoare_2128652938rivs_a @ G_2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_12 @ C_1 @ Q_4 ) @ bot_bo280939947le_a_o ) )
% 2.85/1.84 => ( ( hoare_2128652938rivs_a @ G_2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ Q_4 @ D @ R ) @ bot_bo280939947le_a_o ) )
% 2.85/1.84 => ( hoare_2128652938rivs_a @ G_2 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_12 @ ( semi @ C_1 @ D ) @ R ) @ bot_bo280939947le_a_o ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_45_triple_Oexhaust,axiom,
% 2.85/1.84 ! [Y_4: hoare_669141180iple_a] :
% 2.85/1.84 ~ ! [Fun1: x_a > state > $o,Com: com,Fun2: x_a > state > $o] :
% 2.85/1.84 ( Y_4
% 2.85/1.84 != ( hoare_1295064928iple_a @ Fun1 @ Com @ Fun2 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_46_Set_Oset__insert,axiom,
% 2.85/1.84 ! [X_18: hoare_669141180iple_a,A_32: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( member1016246415iple_a @ X_18 @ A_32 )
% 2.85/1.84 => ~ ! [B_1: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( A_32
% 2.85/1.84 = ( insert175534902iple_a @ X_18 @ B_1 ) )
% 2.85/1.84 => ( member1016246415iple_a @ X_18 @ B_1 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_47_com_Osimps_I13_J,axiom,
% 2.85/1.84 ! [Com1: com,Com2: com] :
% 2.85/1.84 ( ( semi @ Com1 @ Com2 )
% 2.85/1.84 != skip ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_48_com_Osimps_I12_J,axiom,
% 2.85/1.84 ! [Com1: com,Com2: com] :
% 2.85/1.84 ( skip
% 2.85/1.84 != ( semi @ Com1 @ Com2 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_49_the__elem__def,axiom,
% 2.85/1.84 ! [X_17: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( the_el738790235iple_a @ X_17 )
% 2.85/1.84 = ( the_Ho49089901iple_a
% 2.85/1.84 @ ^ [X_3: hoare_669141180iple_a] :
% 2.85/1.84 ( X_17
% 2.85/1.84 = ( insert175534902iple_a @ X_3 @ bot_bo280939947le_a_o ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_50_mk__disjoint__insert,axiom,
% 2.85/1.84 ! [A_31: hoare_669141180iple_a,A_30: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( member1016246415iple_a @ A_31 @ A_30 )
% 2.85/1.84 => ? [B_1: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( A_30
% 2.85/1.84 = ( insert175534902iple_a @ A_31 @ B_1 ) )
% 2.85/1.84 & ~ ( member1016246415iple_a @ A_31 @ B_1 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_51_com_Osimps_I3_J,axiom,
% 2.85/1.84 ! [Com1_1: com,Com2_1: com,Com1: com,Com2: com] :
% 2.85/1.84 ( ( ( semi @ Com1_1 @ Com2_1 )
% 2.85/1.84 = ( semi @ Com1 @ Com2 ) )
% 2.85/1.84 <=> ( ( Com1_1 = Com1 )
% 2.85/1.84 & ( Com2_1 = Com2 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_52_the__sym__eq__trivial,axiom,
% 2.85/1.84 ! [X_16: hoare_669141180iple_a] :
% 2.85/1.84 ( ( the_Ho49089901iple_a @ ( fequal182287803iple_a @ X_16 ) )
% 2.85/1.84 = X_16 ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_53_the__eq__trivial,axiom,
% 2.85/1.84 ! [A_29: hoare_669141180iple_a] :
% 2.85/1.84 ( ( the_Ho49089901iple_a
% 2.85/1.84 @ ^ [X_3: hoare_669141180iple_a] : ( X_3 = A_29 ) )
% 2.85/1.84 = A_29 ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_54_If__def,axiom,
% 2.85/1.84 ! [X_15: hoare_669141180iple_a,Y_3: hoare_669141180iple_a,P_11: $o] :
% 2.85/1.84 ( ( P_11
% 2.85/1.84 => ( X_15
% 2.85/1.84 = ( the_Ho49089901iple_a
% 2.85/1.84 @ ^ [Z_7: hoare_669141180iple_a] : ( (&) @ ( (=>) @ P_11 @ ( Z_7 = X_15 ) ) @ ( (=>) @ ( (~) @ P_11 ) @ ( Z_7 = Y_3 ) ) ) ) ) )
% 2.85/1.84 & ( ~ P_11
% 2.85/1.84 => ( Y_3
% 2.85/1.84 = ( the_Ho49089901iple_a
% 2.85/1.84 @ ^ [Z_7: hoare_669141180iple_a] : ( (&) @ ( (=>) @ P_11 @ ( Z_7 = X_15 ) ) @ ( (=>) @ ( (~) @ P_11 ) @ ( Z_7 = Y_3 ) ) ) ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_55_equals0I,axiom,
% 2.85/1.84 ! [A_28: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ! [Y_1: hoare_669141180iple_a] :
% 2.85/1.84 ~ ( member1016246415iple_a @ Y_1 @ A_28 )
% 2.85/1.84 => ( A_28 = bot_bo280939947le_a_o ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_56_the__equality,axiom,
% 2.85/1.84 ! [P_10: hoare_669141180iple_a > $o,A_27: hoare_669141180iple_a] :
% 2.85/1.84 ( ( P_10 @ A_27 )
% 2.85/1.84 => ( ! [X_3: hoare_669141180iple_a] :
% 2.85/1.84 ( ( P_10 @ X_3 )
% 2.85/1.84 => ( X_3 = A_27 ) )
% 2.85/1.84 => ( ( the_Ho49089901iple_a @ P_10 )
% 2.85/1.84 = A_27 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_57_theI,axiom,
% 2.85/1.84 ! [P_9: hoare_669141180iple_a > $o,A_26: hoare_669141180iple_a] :
% 2.85/1.84 ( ( P_9 @ A_26 )
% 2.85/1.84 => ( ! [X_3: hoare_669141180iple_a] :
% 2.85/1.84 ( ( P_9 @ X_3 )
% 2.85/1.84 => ( X_3 = A_26 ) )
% 2.85/1.84 => ( P_9 @ ( the_Ho49089901iple_a @ P_9 ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_58_the1__equality,axiom,
% 2.85/1.84 ! [A_25: hoare_669141180iple_a,P_8: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ? [X_3: hoare_669141180iple_a] :
% 2.85/1.84 ( ( P_8 @ X_3 )
% 2.85/1.84 & ! [Y_1: hoare_669141180iple_a] :
% 2.85/1.84 ( ( P_8 @ Y_1 )
% 2.85/1.84 => ( Y_1 = X_3 ) ) )
% 2.85/1.84 => ( ( P_8 @ A_25 )
% 2.85/1.84 => ( ( the_Ho49089901iple_a @ P_8 )
% 2.85/1.84 = A_25 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_59_theI_H,axiom,
% 2.85/1.84 ! [P_7: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ? [X_3: hoare_669141180iple_a] :
% 2.85/1.84 ( ( P_7 @ X_3 )
% 2.85/1.84 & ! [Y_1: hoare_669141180iple_a] :
% 2.85/1.84 ( ( P_7 @ Y_1 )
% 2.85/1.84 => ( Y_1 = X_3 ) ) )
% 2.85/1.84 => ( P_7 @ ( the_Ho49089901iple_a @ P_7 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_60_conseq,axiom,
% 2.85/1.84 ! [Q_2: x_a > state > $o,G_1: hoare_669141180iple_a > $o,C: com,P_5: x_a > state > $o] :
% 2.85/1.84 ( ! [Z: x_a,S: state] :
% 2.85/1.84 ( ( P_5 @ Z @ S )
% 2.85/1.84 => ? [P_6: x_a > state > $o,Q_3: x_a > state > $o] :
% 2.85/1.84 ( ( hoare_2128652938rivs_a @ G_1 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_6 @ C @ Q_3 ) @ bot_bo280939947le_a_o ) )
% 2.85/1.84 & ! [S_1: state] :
% 2.85/1.84 ( ! [Z_6: x_a] :
% 2.85/1.84 ( ( P_6 @ Z_6 @ S )
% 2.85/1.84 => ( Q_3 @ Z_6 @ S_1 ) )
% 2.85/1.84 => ( Q_2 @ Z @ S_1 ) ) ) )
% 2.85/1.84 => ( hoare_2128652938rivs_a @ G_1 @ ( insert175534902iple_a @ ( hoare_1295064928iple_a @ P_5 @ C @ Q_2 ) @ bot_bo280939947le_a_o ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_61_nonempty__iff,axiom,
% 2.85/1.84 ! [A_24: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( A_24 != bot_bo280939947le_a_o )
% 2.85/1.84 <=> ? [X_3: hoare_669141180iple_a,B_1: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( A_24
% 2.85/1.84 = ( insert175534902iple_a @ X_3 @ B_1 ) )
% 2.85/1.84 & ~ ( member1016246415iple_a @ X_3 @ B_1 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_62_fold1Set__sing,axiom,
% 2.85/1.84 ! [F_31: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_23: hoare_669141180iple_a,B: hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite840267660iple_a @ F_31 @ ( insert175534902iple_a @ A_23 @ bot_bo280939947le_a_o ) @ B )
% 2.85/1.84 <=> ( A_23 = B ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_63_folding__one_Osingleton,axiom,
% 2.85/1.84 ! [X_14: hoare_669141180iple_a,F_30: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_29: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite972428089iple_a @ F_30 @ F_29 )
% 2.85/1.84 => ( ( F_29 @ ( insert175534902iple_a @ X_14 @ bot_bo280939947le_a_o ) )
% 2.85/1.84 = X_14 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_64_bot__empty__eq,axiom,
% 2.85/1.84 ! [X_3: hoare_669141180iple_a] :
% 2.85/1.84 ( ( bot_bo280939947le_a_o @ X_3 )
% 2.85/1.84 <=> ( member1016246415iple_a @ X_3 @ bot_bo280939947le_a_o ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_65_empty__fold1SetE,axiom,
% 2.85/1.84 ! [F_28: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,X_13: hoare_669141180iple_a] :
% 2.85/1.84 ~ ( finite840267660iple_a @ F_28 @ bot_bo280939947le_a_o @ X_13 ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_66_fold1Set__nonempty,axiom,
% 2.85/1.84 ! [F_27: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_22: hoare_669141180iple_a > $o,X_12: hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite840267660iple_a @ F_27 @ A_22 @ X_12 )
% 2.85/1.84 => ( A_22 != bot_bo280939947le_a_o ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_67_fold1Set_Ointros,axiom,
% 2.85/1.84 ! [F_26: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_21: hoare_669141180iple_a,A_20: hoare_669141180iple_a > $o,X_11: hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite590756294iple_a @ F_26 @ A_21 @ A_20 @ X_11 )
% 2.85/1.84 => ( ~ ( member1016246415iple_a @ A_21 @ A_20 )
% 2.85/1.84 => ( finite840267660iple_a @ F_26 @ ( insert175534902iple_a @ A_21 @ A_20 ) @ X_11 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_68_folding__one_Oinsert,axiom,
% 2.85/1.84 ! [X_10: hoare_669141180iple_a,A_19: hoare_669141180iple_a > $o,F_25: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_24: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite972428089iple_a @ F_25 @ F_24 )
% 2.85/1.84 => ( ( finite957651855iple_a @ A_19 )
% 2.85/1.84 => ( ~ ( member1016246415iple_a @ X_10 @ A_19 )
% 2.85/1.84 => ( ( A_19 != bot_bo280939947le_a_o )
% 2.85/1.84 => ( ( F_24 @ ( insert175534902iple_a @ X_10 @ A_19 ) )
% 2.85/1.84 = ( F_25 @ X_10 @ ( F_24 @ A_19 ) ) ) ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_69_fold1__def,axiom,
% 2.85/1.84 ! [F_23: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_18: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( finite684844060iple_a @ F_23 @ A_18 )
% 2.85/1.84 = ( the_Ho49089901iple_a @ ( finite840267660iple_a @ F_23 @ A_18 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_70_finite__Collect__conjI,axiom,
% 2.85/1.84 ! [Q_1: hoare_669141180iple_a > $o,P_4: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( ( finite957651855iple_a @ ( collec1717965009iple_a @ P_4 ) )
% 2.85/1.84 | ( finite957651855iple_a @ ( collec1717965009iple_a @ Q_1 ) ) )
% 2.85/1.84 => ( finite957651855iple_a
% 2.85/1.84 @ ( collec1717965009iple_a
% 2.85/1.84 @ ^ [X_3: hoare_669141180iple_a] : ( (&) @ ( P_4 @ X_3 ) @ ( Q_1 @ X_3 ) ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_71_finite_OemptyI,axiom,
% 2.85/1.84 finite957651855iple_a @ bot_bo280939947le_a_o ).
% 2.85/1.84
% 2.85/1.84 thf(fact_72_finite_OinsertI,axiom,
% 2.85/1.84 ! [A_17: hoare_669141180iple_a,A_16: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( finite957651855iple_a @ A_16 )
% 2.85/1.84 => ( finite957651855iple_a @ ( insert175534902iple_a @ A_17 @ A_16 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_73_mem__def,axiom,
% 2.85/1.84 ! [X_9: hoare_669141180iple_a,A_15: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( member1016246415iple_a @ X_9 @ A_15 )
% 2.85/1.84 <=> ( A_15 @ X_9 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_74_Collect__def,axiom,
% 2.85/1.84 ! [P_3: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( collec1717965009iple_a @ P_3 )
% 2.85/1.84 = P_3 ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_75_folding__one_Oeq__fold,axiom,
% 2.85/1.84 ! [A_14: hoare_669141180iple_a > $o,F_22: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_21: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite972428089iple_a @ F_22 @ F_21 )
% 2.85/1.84 => ( ( finite957651855iple_a @ A_14 )
% 2.85/1.84 => ( ( F_21 @ A_14 )
% 2.85/1.84 = ( finite684844060iple_a @ F_22 @ A_14 ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_76_fold__graph_OemptyI,axiom,
% 2.85/1.84 ! [F_20: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,Z_5: hoare_669141180iple_a] : ( finite590756294iple_a @ F_20 @ Z_5 @ bot_bo280939947le_a_o @ Z_5 ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_77_empty__fold__graphE,axiom,
% 2.85/1.84 ! [F_19: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,Z_4: hoare_669141180iple_a,X_8: hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite590756294iple_a @ F_19 @ Z_4 @ bot_bo280939947le_a_o @ X_8 )
% 2.85/1.84 => ( X_8 = Z_4 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_78_fold__graph_OinsertI,axiom,
% 2.85/1.84 ! [F_18: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,Z_3: hoare_669141180iple_a,Y_2: hoare_669141180iple_a,X_7: hoare_669141180iple_a,A_13: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ~ ( member1016246415iple_a @ X_7 @ A_13 )
% 2.85/1.84 => ( ( finite590756294iple_a @ F_18 @ Z_3 @ A_13 @ Y_2 )
% 2.85/1.84 => ( finite590756294iple_a @ F_18 @ Z_3 @ ( insert175534902iple_a @ X_7 @ A_13 ) @ ( F_18 @ X_7 @ Y_2 ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_79_finite__Collect__disjI,axiom,
% 2.85/1.84 ! [P_2: hoare_669141180iple_a > $o,Q: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( finite957651855iple_a
% 2.85/1.84 @ ( collec1717965009iple_a
% 2.85/1.84 @ ^ [X_3: hoare_669141180iple_a] : ( (|) @ ( P_2 @ X_3 ) @ ( Q @ X_3 ) ) ) )
% 2.85/1.84 <=> ( ( finite957651855iple_a @ ( collec1717965009iple_a @ P_2 ) )
% 2.85/1.84 & ( finite957651855iple_a @ ( collec1717965009iple_a @ Q ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_80_finite__insert,axiom,
% 2.85/1.84 ! [A_12: hoare_669141180iple_a,A_11: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( finite957651855iple_a @ ( insert175534902iple_a @ A_12 @ A_11 ) )
% 2.85/1.84 <=> ( finite957651855iple_a @ A_11 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_81_fold1__singleton__def,axiom,
% 2.85/1.84 ! [A_10: hoare_669141180iple_a,G: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a,F_17: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a] :
% 2.85/1.84 ( ( G
% 2.85/1.84 = ( finite684844060iple_a @ F_17 ) )
% 2.85/1.84 => ( ( G @ ( insert175534902iple_a @ A_10 @ bot_bo280939947le_a_o ) )
% 2.85/1.84 = A_10 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_82_fold1__singleton,axiom,
% 2.85/1.84 ! [F_16: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_9: hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite684844060iple_a @ F_16 @ ( insert175534902iple_a @ A_9 @ bot_bo280939947le_a_o ) )
% 2.85/1.84 = A_9 ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_83_folding__one_Oclosed,axiom,
% 2.85/1.84 ! [A_8: hoare_669141180iple_a > $o,F_15: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_14: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite972428089iple_a @ F_15 @ F_14 )
% 2.85/1.84 => ( ( finite957651855iple_a @ A_8 )
% 2.85/1.84 => ( ( A_8 != bot_bo280939947le_a_o )
% 2.85/1.84 => ( ! [X_3: hoare_669141180iple_a,Y_1: hoare_669141180iple_a] : ( member1016246415iple_a @ ( F_15 @ X_3 @ Y_1 ) @ ( insert175534902iple_a @ X_3 @ ( insert175534902iple_a @ Y_1 @ bot_bo280939947le_a_o ) ) )
% 2.85/1.84 => ( member1016246415iple_a @ ( F_14 @ A_8 ) @ A_8 ) ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_84_insert__fold1SetE,axiom,
% 2.85/1.84 ! [F_13: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_7: hoare_669141180iple_a,X_6: hoare_669141180iple_a > $o,X_5: hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite840267660iple_a @ F_13 @ ( insert175534902iple_a @ A_7 @ X_6 ) @ X_5 )
% 2.85/1.84 => ~ ! [A_3: hoare_669141180iple_a,A_2: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( ( insert175534902iple_a @ A_7 @ X_6 )
% 2.85/1.84 = ( insert175534902iple_a @ A_3 @ A_2 ) )
% 2.85/1.84 => ( ( finite590756294iple_a @ F_13 @ A_3 @ A_2 @ X_5 )
% 2.85/1.84 => ( member1016246415iple_a @ A_3 @ A_2 ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_85_finite__nonempty__imp__fold1Set,axiom,
% 2.85/1.84 ! [F_12: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A_6: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( finite957651855iple_a @ A_6 )
% 2.85/1.84 => ( ( A_6 != bot_bo280939947le_a_o )
% 2.85/1.84 => ( ex @ ( finite840267660iple_a @ F_12 @ A_6 ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_86_finite__induct,axiom,
% 2.85/1.84 ! [P_1: ( hoare_669141180iple_a > $o ) > $o,F_11: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( finite957651855iple_a @ F_11 )
% 2.85/1.84 => ( ( P_1 @ bot_bo280939947le_a_o )
% 2.85/1.84 => ( ! [X_3: hoare_669141180iple_a,F_5: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( finite957651855iple_a @ F_5 )
% 2.85/1.84 => ( ~ ( member1016246415iple_a @ X_3 @ F_5 )
% 2.85/1.84 => ( ( P_1 @ F_5 )
% 2.85/1.84 => ( P_1 @ ( insert175534902iple_a @ X_3 @ F_5 ) ) ) ) )
% 2.85/1.84 => ( P_1 @ F_11 ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_87_finite_Osimps,axiom,
% 2.85/1.84 ! [A_5: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( finite957651855iple_a @ A_5 )
% 2.85/1.84 <=> ( ( A_5 = bot_bo280939947le_a_o )
% 2.85/1.84 | ? [A_2: hoare_669141180iple_a > $o,A_3: hoare_669141180iple_a] :
% 2.85/1.84 ( ( A_5
% 2.85/1.84 = ( insert175534902iple_a @ A_3 @ A_2 ) )
% 2.85/1.84 & ( finite957651855iple_a @ A_2 ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_88_finite__imp__fold__graph,axiom,
% 2.85/1.84 ! [F_10: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,Z_2: hoare_669141180iple_a,A_4: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( finite957651855iple_a @ A_4 )
% 2.85/1.84 => ( ex @ ( finite590756294iple_a @ F_10 @ Z_2 @ A_4 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_89_fold1Set_Osimps,axiom,
% 2.85/1.84 ! [F_9: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,A1_1: hoare_669141180iple_a > $o,A2_1: hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite840267660iple_a @ F_9 @ A1_1 @ A2_1 )
% 2.85/1.84 <=> ? [A_3: hoare_669141180iple_a,A_2: hoare_669141180iple_a > $o,X_3: hoare_669141180iple_a] :
% 2.85/1.84 ( ( A1_1
% 2.85/1.84 = ( insert175534902iple_a @ A_3 @ A_2 ) )
% 2.85/1.84 & ( A2_1 = X_3 )
% 2.85/1.84 & ( finite590756294iple_a @ F_9 @ A_3 @ A_2 @ X_3 )
% 2.85/1.84 & ~ ( member1016246415iple_a @ A_3 @ A_2 ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_90_fold__graph_Osimps,axiom,
% 2.85/1.84 ! [F_8: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,Z_1: hoare_669141180iple_a,A1: hoare_669141180iple_a > $o,A2: hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite590756294iple_a @ F_8 @ Z_1 @ A1 @ A2 )
% 2.85/1.84 <=> ( ( ( A1 = bot_bo280939947le_a_o )
% 2.85/1.84 & ( A2 = Z_1 ) )
% 2.85/1.84 | ? [X_3: hoare_669141180iple_a,A_2: hoare_669141180iple_a > $o,Y_1: hoare_669141180iple_a] :
% 2.85/1.84 ( ( A1
% 2.85/1.84 = ( insert175534902iple_a @ X_3 @ A_2 ) )
% 2.85/1.84 & ( A2
% 2.85/1.84 = ( F_8 @ X_3 @ Y_1 ) )
% 2.85/1.84 & ~ ( member1016246415iple_a @ X_3 @ A_2 )
% 2.85/1.84 & ( finite590756294iple_a @ F_8 @ Z_1 @ A_2 @ Y_1 ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_91_folding__one__idem_Oinsert__idem,axiom,
% 2.85/1.84 ! [X_4: hoare_669141180iple_a,A_1: hoare_669141180iple_a > $o,F_7: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_6: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite252461622iple_a @ F_7 @ F_6 )
% 2.85/1.84 => ( ( finite957651855iple_a @ A_1 )
% 2.85/1.84 => ( ( A_1 != bot_bo280939947le_a_o )
% 2.85/1.84 => ( ( F_6 @ ( insert175534902iple_a @ X_4 @ A_1 ) )
% 2.85/1.84 = ( F_7 @ X_4 @ ( F_6 @ A_1 ) ) ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_92_finite__ne__induct,axiom,
% 2.85/1.84 ! [P: ( hoare_669141180iple_a > $o ) > $o,F_4: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( finite957651855iple_a @ F_4 )
% 2.85/1.84 => ( ( F_4 != bot_bo280939947le_a_o )
% 2.85/1.84 => ( ! [X_3: hoare_669141180iple_a] : ( P @ ( insert175534902iple_a @ X_3 @ bot_bo280939947le_a_o ) )
% 2.85/1.84 => ( ! [X_3: hoare_669141180iple_a,F_5: hoare_669141180iple_a > $o] :
% 2.85/1.84 ( ( finite957651855iple_a @ F_5 )
% 2.85/1.84 => ( ( F_5 != bot_bo280939947le_a_o )
% 2.85/1.84 => ( ~ ( member1016246415iple_a @ X_3 @ F_5 )
% 2.85/1.84 => ( ( P @ F_5 )
% 2.85/1.84 => ( P @ ( insert175534902iple_a @ X_3 @ F_5 ) ) ) ) ) )
% 2.85/1.84 => ( P @ F_4 ) ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_93_folding__one__idem_Oidem,axiom,
% 2.85/1.84 ! [X_2: hoare_669141180iple_a,F_3: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F_2: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite252461622iple_a @ F_3 @ F_2 )
% 2.85/1.84 => ( ( F_3 @ X_2 @ X_2 )
% 2.85/1.84 = X_2 ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(fact_94_folding__one__idem_Oin__idem,axiom,
% 2.85/1.84 ! [X_1: hoare_669141180iple_a,A: hoare_669141180iple_a > $o,F_1: hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a,F: ( hoare_669141180iple_a > $o ) > hoare_669141180iple_a] :
% 2.85/1.84 ( ( finite252461622iple_a @ F_1 @ F )
% 2.85/1.84 => ( ( finite957651855iple_a @ A )
% 2.85/1.84 => ( ( member1016246415iple_a @ X_1 @ A )
% 2.85/1.84 => ( ( F_1 @ X_1 @ ( F @ A ) )
% 2.85/1.84 = ( F @ A ) ) ) ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(help_fequal_1_1_fequal_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J_,axiom,
% 2.85/1.84 ! [X: hoare_669141180iple_a,Y: hoare_669141180iple_a] :
% 2.85/1.84 ( ~ ( fequal182287803iple_a @ X @ Y )
% 2.85/1.84 | ( X = Y ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(help_fequal_2_1_fequal_000tc__Hoare____Mirabelle____ghhkfsbqqq__Otriple_It__a_J_,axiom,
% 2.85/1.84 ! [X: hoare_669141180iple_a,Y: hoare_669141180iple_a] :
% 2.85/1.84 ( ( X != Y )
% 2.85/1.84 | ( fequal182287803iple_a @ X @ Y ) ) ).
% 2.85/1.84
% 2.85/1.84 thf(conj_0,conjecture,
% 2.85/1.84 ( hoare_2128652938rivs_a @ g
% 2.85/1.84 @ ( insert175534902iple_a
% 2.85/1.84 @ ( hoare_1295064928iple_a
% 2.85/1.84 @ ^ [Z: x_a,S: state] : $false
% 2.85/1.84 @ c
% 2.85/1.84 @ ^ [Z: x_a,S: state] : ( (&) @ ( p @ Z @ S ) @ ( (~) @ ( b @ S ) ) ) )
% 2.85/1.84 @ bot_bo280939947le_a_o ) ) ).
% 2.85/1.84 ------------------------
% 2.85/1.87 % (26151)lrs+1002_1:128_aac=none:au=on:cnfonf=lazy_not_gen_be_off:sos=all:i=2:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/2Mi)
% 2.85/1.87 % (26150)lrs+10_1:1_au=on:inj=on:i=2:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/2Mi)
% 2.85/1.87 % (26149)dis+1010_1:1_au=on:cbe=off:chr=on:fsr=off:hfsq=on:nm=64:sos=theory:sp=weighted_frequency:i=27:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/27Mi)
% 2.85/1.87 % (26152)lrs+1002_1:1_au=on:bd=off:e2e=on:sd=2:sos=on:ss=axioms:i=275:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/275Mi)
% 2.85/1.87 % (26147)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/183Mi)
% 2.85/1.87 % (26150)Instruction limit reached!
% 2.85/1.87 % (26150)------------------------------
% 2.85/1.87 % (26150)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.85/1.87 % (26150)Termination reason: Unknown
% 2.85/1.87 % (26150)Termination phase: shuffling
% 2.85/1.87
% 2.85/1.87 % (26151)Instruction limit reached!
% 2.85/1.87 % (26151)------------------------------
% 2.85/1.87 % (26151)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.85/1.87 % (26150)Memory used [KB]: 1151
% 2.85/1.87 % (26150)Time elapsed: 0.003 s
% 2.85/1.87 % (26150)Instructions burned: 2 (million)
% 2.85/1.87 % (26150)------------------------------
% 2.85/1.87 % (26150)------------------------------
% 2.85/1.87 % (26151)Termination reason: Unknown
% 2.85/1.87 % (26151)Termination phase: shuffling
% 2.85/1.87
% 2.85/1.87 % (26151)Memory used [KB]: 1151
% 2.85/1.87 % (26151)Time elapsed: 0.003 s
% 2.85/1.87 % (26151)Instructions burned: 2 (million)
% 2.85/1.87 % (26151)------------------------------
% 2.85/1.87 % (26151)------------------------------
% 2.85/1.87 % (26148)lrs+10_1:1_c=on:cnfonf=conj_eager:fd=off:fe=off:kws=frequency:spb=intro:i=4:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/4Mi)
% 2.85/1.88 % (26153)lrs+1004_1:128_cond=on:e2e=on:sp=weighted_frequency:i=18:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/18Mi)
% 2.85/1.88 % (26148)Instruction limit reached!
% 2.85/1.88 % (26148)------------------------------
% 2.85/1.88 % (26148)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.85/1.88 % (26148)Termination reason: Unknown
% 2.85/1.88 % (26148)Termination phase: shuffling
% 2.85/1.88
% 2.85/1.88 % (26148)Memory used [KB]: 1279
% 2.85/1.88 % (26148)Time elapsed: 0.004 s
% 2.85/1.88 % (26148)Instructions burned: 5 (million)
% 2.85/1.88 % (26148)------------------------------
% 2.85/1.88 % (26148)------------------------------
% 2.85/1.89 % (26149)Instruction limit reached!
% 2.85/1.89 % (26149)------------------------------
% 2.85/1.89 % (26149)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.85/1.89 % (26149)Termination reason: Unknown
% 2.85/1.89 % (26149)Termination phase: Property scanning
% 2.85/1.89
% 2.85/1.89 % (26149)Memory used [KB]: 1663
% 2.85/1.89 % (26149)Time elapsed: 0.015 s
% 2.85/1.89 % (26149)Instructions burned: 27 (million)
% 2.85/1.89 % (26149)------------------------------
% 2.85/1.89 % (26149)------------------------------
% 2.85/1.89 % (26153)Instruction limit reached!
% 2.85/1.89 % (26153)------------------------------
% 2.85/1.89 % (26153)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.85/1.89 % (26153)Termination reason: Unknown
% 2.85/1.89 % (26153)Termination phase: Preprocessing 3
% 2.85/1.89
% 2.85/1.89 % (26153)Memory used [KB]: 1663
% 2.85/1.89 % (26153)Time elapsed: 0.012 s
% 2.85/1.89 % (26153)Instructions burned: 19 (million)
% 2.85/1.89 % (26153)------------------------------
% 2.85/1.89 % (26153)------------------------------
% 2.85/1.89 % (26155)lrs+1002_1:1_cnfonf=lazy_not_be_gen:hud=14:prag=on:sp=weighted_frequency:tnu=1:i=37:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/37Mi)
% 2.85/1.89 % (26154)lrs+10_1:1_bet=on:cnfonf=off:fd=off:hud=5:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/3Mi)
% 2.85/1.89 % (26154)Instruction limit reached!
% 2.85/1.89 % (26154)------------------------------
% 2.85/1.89 % (26154)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.85/1.89 % (26154)Termination reason: Unknown
% 2.85/1.89 % (26154)Termination phase: shuffling
% 2.85/1.89
% 2.85/1.89 % (26154)Memory used [KB]: 1279
% 2.85/1.89 % (26154)Time elapsed: 0.004 s
% 2.85/1.89 % (26154)Instructions burned: 4 (million)
% 2.85/1.89 % (26154)------------------------------
% 2.85/1.89 % (26154)------------------------------
% 2.85/1.89 % (26156)lrs+2_16:1_acc=model:au=on:bd=off:c=on:e2e=on:nm=2:sos=all:i=15:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/15Mi)
% 2.89/1.90 % (26156)Instruction limit reached!
% 2.89/1.90 % (26156)------------------------------
% 2.89/1.90 % (26156)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.90 % (26156)Termination reason: Unknown
% 2.89/1.90 % (26156)Termination phase: Preprocessing 1
% 2.89/1.90
% 2.89/1.90 % (26156)Memory used [KB]: 1535
% 2.89/1.90 % (26156)Time elapsed: 0.010 s
% 2.89/1.90 % (26156)Instructions burned: 16 (million)
% 2.89/1.90 % (26156)------------------------------
% 2.89/1.90 % (26156)------------------------------
% 2.89/1.90 % (26157)dis+21_1:1_cbe=off:cnfonf=off:fs=off:fsr=off:hud=1:inj=on:i=3:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/3Mi)
% 2.89/1.90 % (26157)Instruction limit reached!
% 2.89/1.90 % (26157)------------------------------
% 2.89/1.90 % (26157)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.90 % (26157)Termination reason: Unknown
% 2.89/1.90 % (26157)Termination phase: shuffling
% 2.89/1.90
% 2.89/1.90 % (26157)Memory used [KB]: 1279
% 2.89/1.90 % (26157)Time elapsed: 0.004 s
% 2.89/1.90 % (26157)Instructions burned: 4 (million)
% 2.89/1.90 % (26157)------------------------------
% 2.89/1.90 % (26157)------------------------------
% 2.89/1.91 % (26158)lrs+1002_1:1_aac=none:au=on:cnfonf=lazy_gen:plsq=on:plsqc=1:plsqr=4203469,65536:i=1041:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/1041Mi)
% 2.89/1.91 % (26155)Instruction limit reached!
% 2.89/1.91 % (26155)------------------------------
% 2.89/1.91 % (26155)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.91 % (26155)Termination reason: Unknown
% 2.89/1.91 % (26155)Termination phase: Property scanning
% 2.89/1.91
% 2.89/1.91 % (26155)Memory used [KB]: 1663
% 2.89/1.91 % (26155)Time elapsed: 0.019 s
% 2.89/1.91 % (26155)Instructions burned: 37 (million)
% 2.89/1.91 % (26155)------------------------------
% 2.89/1.91 % (26155)------------------------------
% 2.89/1.91 % (26159)lrs+10_1:1_av=off:chr=on:plsq=on:slsq=on:i=7:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/7Mi)
% 2.89/1.91 % (26159)Instruction limit reached!
% 2.89/1.91 % (26159)------------------------------
% 2.89/1.91 % (26159)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.91 % (26159)Termination reason: Unknown
% 2.89/1.91 % (26159)Termination phase: shuffling
% 2.89/1.91
% 2.89/1.91 % (26159)Memory used [KB]: 1407
% 2.89/1.91 % (26159)Time elapsed: 0.005 s
% 2.89/1.91 % (26159)Instructions burned: 7 (million)
% 2.89/1.91 % (26159)------------------------------
% 2.89/1.91 % (26159)------------------------------
% 2.89/1.92 % (26160)lrs+10_1:1_acc=on:amm=sco:cs=on:tgt=full:i=16:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/16Mi)
% 2.89/1.92 % (26161)lrs+21_1:1_au=on:cnfonf=off:fd=preordered:fe=off:fsr=off:hud=11:inj=on:kws=precedence:s2pl=no:sp=weighted_frequency:tgt=full:i=3:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/3Mi)
% 2.89/1.92 % (26161)Instruction limit reached!
% 2.89/1.92 % (26161)------------------------------
% 2.89/1.92 % (26161)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.92 % (26161)Termination reason: Unknown
% 2.89/1.92 % (26161)Termination phase: shuffling
% 2.89/1.92
% 2.89/1.92 % (26161)Memory used [KB]: 1151
% 2.89/1.92 % (26161)Time elapsed: 0.003 s
% 2.89/1.92 % (26161)Instructions burned: 3 (million)
% 2.89/1.92 % (26161)------------------------------
% 2.89/1.92 % (26161)------------------------------
% 2.89/1.92 % (26162)lrs+2_1:1_apa=on:au=on:bd=preordered:cnfonf=off:cs=on:ixr=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/3Mi)
% 2.89/1.93 % (26160)Instruction limit reached!
% 2.89/1.93 % (26160)------------------------------
% 2.89/1.93 % (26160)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.93 % (26160)Termination reason: Unknown
% 2.89/1.93 % (26160)Termination phase: Preprocessing 2
% 2.89/1.93
% 2.89/1.93 % (26160)Memory used [KB]: 1535
% 2.89/1.93 % (26160)Time elapsed: 0.010 s
% 2.89/1.93 % (26160)Instructions burned: 16 (million)
% 2.89/1.93 % (26160)------------------------------
% 2.89/1.93 % (26160)------------------------------
% 2.89/1.93 % (26162)Instruction limit reached!
% 2.89/1.93 % (26162)------------------------------
% 2.89/1.93 % (26162)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.93 % (26162)Termination reason: Unknown
% 2.89/1.93 % (26162)Termination phase: shuffling
% 2.89/1.93
% 2.89/1.93 % (26162)Memory used [KB]: 1279
% 2.89/1.93 % (26162)Time elapsed: 0.003 s
% 2.89/1.93 % (26162)Instructions burned: 3 (million)
% 2.89/1.93 % (26162)------------------------------
% 2.89/1.93 % (26162)------------------------------
% 2.89/1.93 % (26163)lrs+10_1:1_cnfonf=off:cs=on:hud=3:prag=on:sup=off:i=7:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/7Mi)
% 2.89/1.93 % (26163)Instruction limit reached!
% 2.89/1.93 % (26163)------------------------------
% 2.89/1.93 % (26163)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.93 % (26163)Termination reason: Unknown
% 2.89/1.93 % (26163)Termination phase: shuffling
% 2.89/1.93
% 2.89/1.93 % (26163)Memory used [KB]: 1279
% 2.89/1.93 % (26163)Time elapsed: 0.005 s
% 2.89/1.93 % (26163)Instructions burned: 7 (million)
% 2.89/1.93 % (26163)------------------------------
% 2.89/1.93 % (26163)------------------------------
% 2.89/1.94 % (26164)dis+1002_1:1_add=large:cnfonf=lazy_pi_sigma_gen:fe=off:prag=on:i=3:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/3Mi)
% 2.89/1.94 % (26164)Instruction limit reached!
% 2.89/1.94 % (26164)------------------------------
% 2.89/1.94 % (26164)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.94 % (26164)Termination reason: Unknown
% 2.89/1.94 % (26164)Termination phase: shuffling
% 2.89/1.94
% 2.89/1.94 % (26164)Memory used [KB]: 1151
% 2.89/1.94 % (26164)Time elapsed: 0.003 s
% 2.89/1.94 % (26164)Instructions burned: 3 (million)
% 2.89/1.94 % (26164)------------------------------
% 2.89/1.94 % (26164)------------------------------
% 2.89/1.94 % (26165)dis+1004_1:1_cha=on:cs=on:fe=off:hud=1:i=4:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/4Mi)
% 2.89/1.94 % (26166)lrs+1002_1:1_anc=all_dependent:au=on:cbe=off:fde=unused:ntd=on:i=18:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/18Mi)
% 2.89/1.95 % (26165)Instruction limit reached!
% 2.89/1.95 % (26165)------------------------------
% 2.89/1.95 % (26165)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.95 % (26165)Termination reason: Unknown
% 2.89/1.95 % (26165)Termination phase: shuffling
% 2.89/1.95
% 2.89/1.95 % (26165)Memory used [KB]: 1279
% 2.89/1.95 % (26165)Time elapsed: 0.004 s
% 2.89/1.95 % (26165)Instructions burned: 5 (million)
% 2.89/1.95 % (26165)------------------------------
% 2.89/1.95 % (26165)------------------------------
% 2.89/1.95 % (26166)Instruction limit reached!
% 2.89/1.95 % (26166)------------------------------
% 2.89/1.95 % (26166)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.95 % (26166)Termination reason: Unknown
% 2.89/1.95 % (26166)Termination phase: Preprocessing 3
% 2.89/1.95
% 2.89/1.95 % (26166)Memory used [KB]: 1663
% 2.89/1.95 % (26166)Time elapsed: 0.011 s
% 2.89/1.95 % (26166)Instructions burned: 19 (million)
% 2.89/1.95 % (26166)------------------------------
% 2.89/1.95 % (26166)------------------------------
% 2.89/1.95 % (26167)lrs+10_1:1_e2e=on:sd=1:sgt=8:ss=axioms:i=710:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/710Mi)
% 2.89/1.96 % (26168)lrs+1004_1:1_chr=on:prag=on:i=6:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/6Mi)
% 2.89/1.96 % (26168)Instruction limit reached!
% 2.89/1.96 % (26168)------------------------------
% 2.89/1.96 % (26168)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.96 % (26168)Termination reason: Unknown
% 2.89/1.96 % (26168)Termination phase: shuffling
% 2.89/1.96
% 2.89/1.96 % (26168)Memory used [KB]: 1279
% 2.89/1.96 % (26168)Time elapsed: 0.005 s
% 2.89/1.96 % (26168)Instructions burned: 7 (million)
% 2.89/1.96 % (26168)------------------------------
% 2.89/1.96 % (26168)------------------------------
% 2.89/1.96 % (26169)dis+1002_5:1_au=on:bd=off:e2e=on:fde=none:fs=off:fsr=off:sos=on:i=902:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/902Mi)
% 2.89/1.96 % (26147)Instruction limit reached!
% 2.89/1.96 % (26147)------------------------------
% 2.89/1.96 % (26147)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.96 % (26147)Termination reason: Unknown
% 2.89/1.96 % (26147)Termination phase: Saturation
% 2.89/1.96
% 2.89/1.96 % (26147)Memory used [KB]: 7419
% 2.89/1.96 % (26147)Time elapsed: 0.093 s
% 2.89/1.96 % (26147)Instructions burned: 183 (million)
% 2.89/1.96 % (26147)------------------------------
% 2.89/1.96 % (26147)------------------------------
% 2.89/1.97 % (26170)dis+21_1:8_apa=on:cnfonf=off:fd=off:fsr=off:hud=0:ins=1:kws=inv_frequency:nwc=10.0:ss=axioms:st=5.0:i=21:si=on:rtra=on_0 on DTF2THF_26033 for (2999ds/21Mi)
% 2.89/1.98 % (26171)dis+10_1:1_cnfonf=lazy_gen:fe=off:i=5:si=on:rtra=on_0 on DTF2THF_26033 for (2998ds/5Mi)
% 2.89/1.98 % (26171)Instruction limit reached!
% 2.89/1.98 % (26171)------------------------------
% 2.89/1.98 % (26171)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.98 % (26171)Termination reason: Unknown
% 2.89/1.98 % (26171)Termination phase: shuffling
% 2.89/1.98
% 2.89/1.98 % (26171)Memory used [KB]: 1279
% 2.89/1.98 % (26171)Time elapsed: 0.005 s
% 2.89/1.98 % (26171)Instructions burned: 7 (million)
% 2.89/1.98 % (26171)------------------------------
% 2.89/1.98 % (26171)------------------------------
% 2.89/1.98 % (26170)Instruction limit reached!
% 2.89/1.98 % (26170)------------------------------
% 2.89/1.98 % (26170)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.98 % (26170)Termination reason: Unknown
% 2.89/1.98 % (26170)Termination phase: Preprocessing 3
% 2.89/1.98
% 2.89/1.98 % (26170)Memory used [KB]: 1535
% 2.89/1.98 % (26170)Time elapsed: 0.013 s
% 2.89/1.98 % (26170)Instructions burned: 21 (million)
% 2.89/1.98 % (26170)------------------------------
% 2.89/1.98 % (26170)------------------------------
% 2.89/1.98 % (26172)lrs+2_1:1_cnfonf=lazy_not_gen_be_off:cs=on:fe=off:hud=10:inj=on:ins=3:plsq=on:plsqc=1:sd=10:ss=axioms:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_26033 for (2998ds/6Mi)
% 2.89/1.98 % (26152)Instruction limit reached!
% 2.89/1.98 % (26152)------------------------------
% 2.89/1.98 % (26152)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.98 % (26152)Termination reason: Unknown
% 2.89/1.98 % (26152)Termination phase: Saturation
% 2.89/1.98
% 2.89/1.98 % (26152)Memory used [KB]: 6396
% 2.89/1.98 % (26152)Time elapsed: 0.112 s
% 2.89/1.98 % (26152)Instructions burned: 277 (million)
% 2.89/1.98 % (26152)------------------------------
% 2.89/1.98 % (26152)------------------------------
% 2.89/1.99 % (26172)Instruction limit reached!
% 2.89/1.99 % (26172)------------------------------
% 2.89/1.99 % (26172)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/1.99 % (26172)Termination reason: Unknown
% 2.89/1.99 % (26172)Termination phase: shuffling
% 2.89/1.99
% 2.89/1.99 % (26172)Memory used [KB]: 1407
% 2.89/1.99 % (26172)Time elapsed: 0.005 s
% 2.89/1.99 % (26172)Instructions burned: 7 (million)
% 2.89/1.99 % (26172)------------------------------
% 2.89/1.99 % (26172)------------------------------
% 2.89/1.99 % (26173)lrs+1002_1:128_au=on:c=on:fsr=off:piset=equals:i=377:si=on:rtra=on_0 on DTF2THF_26033 for (2998ds/377Mi)
% 2.89/2.00 % (26174)dis+1010_1:4_atotf=0.2:c=on:cbe=off:cnfonf=lazy_simp:fe=off:ins=2:ntd=on:s2a=on:s2at=5.0:sgt=5:ss=axioms:st=1.5:i=779:si=on:rtra=on_0 on DTF2THF_26033 for (2998ds/779Mi)
% 2.89/2.00 % (26175)lrs+10_1:1_cnfonf=lazy_not_be_gen:ntd=on:sp=const_min:ss=axioms:sup=off:i=19:si=on:rtra=on_0 on DTF2THF_26033 for (2998ds/19Mi)
% 2.89/2.00 % (26176)lrs+1010_1:1_au=on:s2a=on:sd=1:sgt=50:ss=axioms:i=879:si=on:rtra=on_0 on DTF2THF_26033 for (2998ds/879Mi)
% 2.89/2.01 % (26175)Instruction limit reached!
% 2.89/2.01 % (26175)------------------------------
% 2.89/2.01 % (26175)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 2.89/2.01 % (26175)Termination reason: Unknown
% 2.89/2.01 % (26175)Termination phase: Property scanning
% 2.89/2.01
% 2.89/2.01 % (26175)Memory used [KB]: 1663
% 2.89/2.01 % (26175)Time elapsed: 0.011 s
% 2.89/2.01 % (26175)Instructions burned: 19 (million)
% 2.89/2.01 % (26175)------------------------------
% 2.89/2.01 % (26175)------------------------------
% 3.99/2.03 % (26177)dis+1002_1:128_acc=on:er=filter:i=17:si=on:rtra=on_0 on DTF2THF_26033 for (2998ds/17Mi)
% 3.99/2.04 % (26177)Instruction limit reached!
% 3.99/2.04 % (26177)------------------------------
% 3.99/2.04 % (26177)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 3.99/2.04 % (26177)Termination reason: Unknown
% 3.99/2.04 % (26177)Termination phase: Preprocessing 3
% 3.99/2.04
% 3.99/2.04 % (26177)Memory used [KB]: 1535
% 3.99/2.04 % (26177)Time elapsed: 0.012 s
% 3.99/2.04 % (26177)Instructions burned: 17 (million)
% 3.99/2.04 % (26177)------------------------------
% 3.99/2.04 % (26177)------------------------------
% 3.99/2.06 % (26178)ott+21_1:1_apa=on:au=on:cnfonf=off:sos=on:i=3:si=on:rtra=on_0 on DTF2THF_26033 for (2998ds/3Mi)
% 3.99/2.06 % (26178)Instruction limit reached!
% 3.99/2.06 % (26178)------------------------------
% 3.99/2.06 % (26178)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 3.99/2.06 % (26178)Termination reason: Unknown
% 3.99/2.06 % (26178)Termination phase: shuffling
% 3.99/2.06
% 3.99/2.06 % (26178)Memory used [KB]: 1151
% 3.99/2.06 % (26178)Time elapsed: 0.003 s
% 3.99/2.06 % (26178)Instructions burned: 3 (million)
% 3.99/2.06 % (26178)------------------------------
% 3.99/2.06 % (26178)------------------------------
% 3.99/2.08 % (26179)lrs+1010_1:8_cnfonf=off:hud=1:inj=on:tnu=5:i=30:si=on:rtra=on_0 on DTF2THF_26033 for (2997ds/30Mi)
% 3.99/2.09 % (26179)Instruction limit reached!
% 3.99/2.09 % (26179)------------------------------
% 3.99/2.09 % (26179)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 3.99/2.09 % (26179)Termination reason: Unknown
% 3.99/2.09 % (26179)Termination phase: Function definition elimination
% 3.99/2.09
% 3.99/2.09 % (26179)Memory used [KB]: 1663
% 3.99/2.09 % (26179)Time elapsed: 0.016 s
% 3.99/2.09 % (26179)Instructions burned: 30 (million)
% 3.99/2.09 % (26179)------------------------------
% 3.99/2.09 % (26179)------------------------------
% 3.99/2.11 % (26180)dis+10_1:1_ixr=off:plsq=on:plsqc=1:plsqr=32,1:s2a=on:i=127:si=on:rtra=on_0 on DTF2THF_26033 for (2997ds/127Mi)
% 4.67/2.18 % (26180)Instruction limit reached!
% 4.67/2.18 % (26180)------------------------------
% 4.67/2.18 % (26180)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 4.67/2.18 % (26180)Termination reason: Unknown
% 4.67/2.18 % (26180)Termination phase: Saturation
% 4.67/2.18
% 4.67/2.18 % (26180)Memory used [KB]: 6524
% 4.67/2.18 % (26180)Time elapsed: 0.075 s
% 4.67/2.18 % (26180)Instructions burned: 127 (million)
% 4.67/2.18 % (26180)------------------------------
% 4.67/2.18 % (26180)------------------------------
% 4.67/2.19 % (26173)Instruction limit reached!
% 4.67/2.19 % (26173)------------------------------
% 4.67/2.19 % (26173)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 4.67/2.19 % (26173)Termination reason: Unknown
% 4.67/2.19 % (26173)Termination phase: Saturation
% 4.67/2.19
% 4.67/2.19 % (26173)Memory used [KB]: 7036
% 4.67/2.19 % (26173)Time elapsed: 0.195 s
% 4.67/2.19 % (26173)Instructions burned: 378 (million)
% 4.67/2.19 % (26173)------------------------------
% 4.67/2.19 % (26173)------------------------------
% 5.20/2.20 % (26181)lrs+1002_1:1_au=on:cbe=off:cnfonf=conj_eager:cond=on:hi=on:i=100:si=on:rtra=on_0 on DTF2THF_26033 for (2996ds/100Mi)
% 5.20/2.20 % (26182)dis+10_1:1_anc=none:cnfonf=lazy_gen:fd=preordered:fe=off:hud=10:ins=3:ixr=off:nwc=5.0:plsq=on:plsqc=1:plsqr=32,1:sp=const_frequency:uhcvi=on:i=3:si=on:rtra=on_0 on DTF2THF_26033 for (2996ds/3Mi)
% 5.20/2.21 % (26182)Instruction limit reached!
% 5.20/2.21 % (26182)------------------------------
% 5.20/2.21 % (26182)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.20/2.21 % (26182)Termination reason: Unknown
% 5.20/2.21 % (26182)Termination phase: shuffling
% 5.20/2.21
% 5.20/2.21 % (26182)Memory used [KB]: 1279
% 5.20/2.21 % (26182)Time elapsed: 0.003 s
% 5.20/2.21 % (26182)Instructions burned: 4 (million)
% 5.20/2.21 % (26182)------------------------------
% 5.20/2.21 % (26182)------------------------------
% 5.20/2.22 % (26183)lrs+10_8:1_au=on:avsq=on:e2e=on:ins=3:s2a=on:s2at=3.0:ss=axioms:i=20:si=on:rtra=on_0 on DTF2THF_26033 for (2996ds/20Mi)
% 5.20/2.23 % (26183)Instruction limit reached!
% 5.20/2.23 % (26183)------------------------------
% 5.20/2.23 % (26183)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.20/2.23 % (26183)Termination reason: Unknown
% 5.20/2.23 % (26183)Termination phase: Preprocessing 3
% 5.20/2.23
% 5.20/2.23 % (26183)Memory used [KB]: 1535
% 5.20/2.23 % (26183)Time elapsed: 0.012 s
% 5.20/2.23 % (26183)Instructions burned: 21 (million)
% 5.20/2.23 % (26183)------------------------------
% 5.20/2.23 % (26183)------------------------------
% 5.20/2.25 % (26181)Instruction limit reached!
% 5.20/2.25 % (26181)------------------------------
% 5.20/2.25 % (26181)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.20/2.25 % (26181)Termination reason: Unknown
% 5.20/2.25 % (26181)Termination phase: Saturation
% 5.20/2.25
% 5.20/2.25 % (26181)Memory used [KB]: 6524
% 5.20/2.25 % (26181)Time elapsed: 0.049 s
% 5.20/2.25 % (26181)Instructions burned: 100 (million)
% 5.20/2.25 % (26181)------------------------------
% 5.20/2.25 % (26181)------------------------------
% 5.20/2.25 % (26184)dis+1002_1:1_cbe=off:hud=5:nm=4:plsq=on:plsqr=7,1:prag=on:sp=const_max:tnu=1:i=86:si=on:rtra=on_0 on DTF2THF_26033 for (2996ds/86Mi)
% 5.20/2.27 % (26185)lrs+1010_1:1_au=on:cbe=off:nm=2:ntd=on:sd=2:ss=axioms:st=5.0:i=107:si=on:rtra=on_0 on DTF2THF_26033 for (2995ds/107Mi)
% 5.20/2.30 % (26167)Instruction limit reached!
% 5.20/2.30 % (26167)------------------------------
% 5.20/2.30 % (26167)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.20/2.30 % (26167)Termination reason: Unknown
% 5.20/2.30 % (26167)Termination phase: Saturation
% 5.20/2.30
% 5.20/2.30 % (26167)Memory used [KB]: 7164
% 5.20/2.30 % (26167)Time elapsed: 0.344 s
% 5.20/2.30 % (26167)Instructions burned: 710 (million)
% 5.20/2.30 % (26167)------------------------------
% 5.20/2.30 % (26167)------------------------------
% 5.46/2.30 % (26184)Instruction limit reached!
% 5.46/2.30 % (26184)------------------------------
% 5.46/2.30 % (26184)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.46/2.30 % (26184)Termination reason: Unknown
% 5.46/2.30 % (26184)Termination phase: Saturation
% 5.46/2.30
% 5.46/2.30 % (26184)Memory used [KB]: 6524
% 5.46/2.30 % (26184)Time elapsed: 0.052 s
% 5.46/2.30 % (26184)Instructions burned: 86 (million)
% 5.46/2.30 % (26184)------------------------------
% 5.46/2.30 % (26184)------------------------------
% 5.46/2.31 % (26186)lrs+2_1:1024_cnfonf=lazy_gen:fe=off:hud=15:plsq=on:plsqc=1:plsqr=32,1:i=39:si=on:rtra=on_0 on DTF2THF_26033 for (2995ds/39Mi)
% 5.46/2.32 % (26187)dis+10_1:1_cnfonf=lazy_not_gen:fsr=off:kws=precedence:nwc=5.0:s2a=on:ss=axioms:st=1.5:i=448:si=on:rtra=on_0 on DTF2THF_26033 for (2995ds/448Mi)
% 5.46/2.32 % (26185)Instruction limit reached!
% 5.46/2.32 % (26185)------------------------------
% 5.46/2.32 % (26185)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.46/2.32 % (26185)Termination reason: Unknown
% 5.46/2.32 % (26185)Termination phase: Saturation
% 5.46/2.32
% 5.46/2.32 % (26185)Memory used [KB]: 6524
% 5.46/2.32 % (26185)Time elapsed: 0.056 s
% 5.46/2.32 % (26185)Instructions burned: 108 (million)
% 5.46/2.32 % (26185)------------------------------
% 5.46/2.32 % (26185)------------------------------
% 5.46/2.33 % (26186)Instruction limit reached!
% 5.46/2.33 % (26186)------------------------------
% 5.46/2.33 % (26186)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.46/2.33 % (26186)Termination reason: Unknown
% 5.46/2.33 % (26186)Termination phase: Function definition elimination
% 5.46/2.33
% 5.46/2.33 % (26186)Memory used [KB]: 1791
% 5.46/2.33 % (26186)Time elapsed: 0.022 s
% 5.46/2.33 % (26186)Instructions burned: 40 (million)
% 5.46/2.33 % (26186)------------------------------
% 5.46/2.33 % (26186)------------------------------
% 5.46/2.34 % (26188)lrs+10_1:512_au=on:fde=unused:lma=on:nm=32:plsq=on:plsqc=1:plsqr=16121663,131072:sfv=off:sp=const_max:ss=axioms:st=3.0:tgt=full:i=46:si=on:rtra=on_0 on DTF2THF_26033 for (2995ds/46Mi)
% 5.46/2.35 % (26189)lrs+10_1:10_au=on:av=off:cbe=off:cnfonf=lazy_pi_sigma_gen:ntd=on:plsq=on:plsqc=1:plsqr=32,1:i=98:si=on:rtra=on_0 on DTF2THF_26033 for (2995ds/98Mi)
% 5.46/2.36 % (26176)Instruction limit reached!
% 5.46/2.36 % (26176)------------------------------
% 5.46/2.36 % (26176)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.46/2.36 % (26176)Termination reason: Unknown
% 5.46/2.36 % (26176)Termination phase: Saturation
% 5.46/2.36
% 5.46/2.36 % (26176)Memory used [KB]: 6652
% 5.46/2.36 % (26176)Time elapsed: 0.380 s
% 5.46/2.36 % (26176)Instructions burned: 881 (million)
% 5.46/2.36 % (26176)------------------------------
% 5.46/2.36 % (26176)------------------------------
% 5.46/2.36 % (26188)Instruction limit reached!
% 5.46/2.36 % (26188)------------------------------
% 5.46/2.36 % (26188)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.46/2.36 % (26188)Termination reason: Unknown
% 5.46/2.36 % (26188)Termination phase: Saturation
% 5.46/2.36
% 5.46/2.36 % (26188)Memory used [KB]: 6268
% 5.46/2.36 % (26188)Time elapsed: 0.024 s
% 5.46/2.36 % (26188)Instructions burned: 47 (million)
% 5.46/2.36 % (26188)------------------------------
% 5.46/2.36 % (26188)------------------------------
% 5.46/2.38 % (26190)ott+1002_1:1_apa=on:au=on:bd=off:cnfonf=off:fd=off:sos=on:sp=weighted_frequency:i=507:si=on:rtra=on_0 on DTF2THF_26033 for (2994ds/507Mi)
% 5.46/2.38 % (26191)dis+1010_2:3_amm=off:fd=preordered:ixr=off:nm=0:pe=on:piset=equals:prag=on:sac=on:tgt=ground:i=149:si=on:rtra=on_0 on DTF2THF_26033 for (2994ds/149Mi)
% 5.46/2.38 % (26169)Instruction limit reached!
% 5.46/2.38 % (26169)------------------------------
% 5.46/2.38 % (26169)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.46/2.38 % (26169)Termination reason: Unknown
% 5.46/2.38 % (26169)Termination phase: Saturation
% 5.46/2.38
% 5.46/2.38 % (26169)Memory used [KB]: 8699
% 5.46/2.38 % (26169)Time elapsed: 0.417 s
% 5.46/2.38 % (26169)Instructions burned: 903 (million)
% 5.46/2.38 % (26169)------------------------------
% 5.46/2.38 % (26169)------------------------------
% 5.46/2.38 % (26158)Instruction limit reached!
% 5.46/2.38 % (26158)------------------------------
% 5.46/2.38 % (26158)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.46/2.38 % (26158)Termination reason: Unknown
% 5.46/2.38 % (26158)Termination phase: Saturation
% 5.46/2.38
% 5.46/2.38 % (26158)Memory used [KB]: 9338
% 5.46/2.38 % (26158)Time elapsed: 0.479 s
% 5.46/2.38 % (26158)Instructions burned: 1042 (million)
% 5.46/2.38 % (26158)------------------------------
% 5.46/2.38 % (26158)------------------------------
% 5.46/2.38 % (26174)Instruction limit reached!
% 5.46/2.38 % (26174)------------------------------
% 5.46/2.38 % (26174)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.46/2.38 % (26174)Termination reason: Unknown
% 5.46/2.38 % (26174)Termination phase: Saturation
% 5.46/2.38
% 5.46/2.38 % (26174)Memory used [KB]: 7547
% 5.46/2.38 % (26174)Time elapsed: 0.410 s
% 5.46/2.38 % (26174)Instructions burned: 779 (million)
% 5.46/2.38 % (26174)------------------------------
% 5.46/2.38 % (26174)------------------------------
% 5.46/2.39 % (26192)lrs+21_1:16_au=on:bd=off:piset=and:i=39:si=on:rtra=on_0 on DTF2THF_26033 for (2994ds/39Mi)
% 5.46/2.39 % (26193)lrs+1004_1:1_cnfonf=lazy_pi_sigma_gen:fe=off:gs=on:hud=10:prag=on:tnu=1:i=6:si=on:rtra=on_0 on DTF2THF_26033 for (2994ds/6Mi)
% 5.46/2.39 % (26193)Instruction limit reached!
% 5.46/2.39 % (26193)------------------------------
% 5.46/2.39 % (26193)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 5.46/2.39 % (26193)Termination reason: Unknown
% 5.46/2.39 % (26193)Termination phase: shuffling
% 5.46/2.39
% 5.46/2.39 % (26193)Memory used [KB]: 1279
% 5.46/2.39 % (26193)Time elapsed: 0.003 s
% 5.46/2.39 % (26193)Instructions burned: 7 (million)
% 5.46/2.39 % (26193)------------------------------
% 5.46/2.39 % (26193)------------------------------
% 6.40/2.40 % (26189)Instruction limit reached!
% 6.40/2.40 % (26189)------------------------------
% 6.40/2.40 % (26189)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 6.40/2.40 % (26189)Termination reason: Unknown
% 6.40/2.40 % (26189)Termination phase: Saturation
% 6.40/2.40
% 6.40/2.40 % (26189)Memory used [KB]: 2174
% 6.40/2.40 % (26189)Time elapsed: 0.051 s
% 6.40/2.40 % (26189)Instructions burned: 98 (million)
% 6.40/2.40 % (26189)------------------------------
% 6.40/2.40 % (26189)------------------------------
% 6.40/2.40 % (26192)Instruction limit reached!
% 6.40/2.40 % (26192)------------------------------
% 6.40/2.40 % (26192)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 6.40/2.40 % (26192)Termination reason: Unknown
% 6.40/2.40 % (26192)Termination phase: Saturation
% 6.40/2.40
% 6.40/2.40 % (26192)Memory used [KB]: 6140
% 6.40/2.40 % (26192)Time elapsed: 0.013 s
% 6.40/2.40 % (26192)Instructions burned: 42 (million)
% 6.40/2.40 % (26192)------------------------------
% 6.40/2.40 % (26192)------------------------------
% 6.40/2.40 % (26195)dis+10_1:1_aac=none:cs=on:i=47:si=on:rtra=on_0 on DTF2THF_26033 for (2994ds/47Mi)
% 6.40/2.41 % (26197)dis+10_1:1_av=off:bd=off:cnfonf=lazy_gen:fe=off:hud=10:plsq=on:plsqc=1:plsqr=32,1:prag=on:tnu=1:i=432:si=on:rtra=on_0 on DTF2THF_26033 for (2994ds/432Mi)
% 6.40/2.41 % (26194)dis+1002_1:1_aac=none:au=on:e2e=on:nm=2:nwc=10.0:sd=1:ss=axioms:st=3.0:i=1087:si=on:rtra=on_0 on DTF2THF_26033 for (2994ds/1087Mi)
% 6.40/2.42 % (26196)lrs+1010_1:128_av=off:cbe=off:cnfonf=lazy_simp:fsr=off:ntd=on:ss=axioms:st=1.5:i=44:si=on:rtra=on_0 on DTF2THF_26033 for (2994ds/44Mi)
% 6.40/2.42 % (26195)Instruction limit reached!
% 6.40/2.42 % (26195)------------------------------
% 6.40/2.42 % (26195)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 6.40/2.42 % (26195)Termination reason: Unknown
% 6.40/2.42 % (26195)Termination phase: Saturation
% 6.40/2.42
% 6.40/2.42 % (26195)Memory used [KB]: 6268
% 6.40/2.42 % (26195)Time elapsed: 0.015 s
% 6.40/2.42 % (26195)Instructions burned: 48 (million)
% 6.40/2.42 % (26195)------------------------------
% 6.40/2.42 % (26195)------------------------------
% 6.40/2.42 % (26190)First to succeed.
% 6.40/2.43 % (26190)Refutation found. Thanks to Tanya!
% 6.40/2.43 % SZS status Theorem for DTF2THF_26033
% 6.40/2.43 % SZS output start Proof for DTF2THF_26033
% 6.40/2.43 thf(type_def_5, type, com: $tType).
% 6.40/2.43 thf(type_def_7, type, hoare_669141180iple_a: $tType).
% 6.40/2.43 thf(type_def_8, type, x_a: $tType).
% 6.40/2.43 thf(type_def_9, type, state: $tType).
% 6.40/2.43 thf(func_def_0, type, x_a: $tType).
% 6.40/2.43 thf(func_def_1, type, com: $tType).
% 6.40/2.43 thf(func_def_2, type, state: $tType).
% 6.40/2.43 thf(func_def_3, type, hoare_669141180iple_a: $tType).
% 6.40/2.43 thf(func_def_4, type, skip: com).
% 6.40/2.43 thf(func_def_5, type, semi: com > com > com).
% 6.40/2.43 thf(func_def_6, type, ex: (hoare_669141180iple_a > $o) > $o).
% 6.40/2.43 thf(func_def_7, type, finite957651855iple_a: (hoare_669141180iple_a > $o) > $o).
% 6.40/2.43 thf(func_def_8, type, finite840267660iple_a: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_9, type, finite684844060iple_a: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_10, type, finite590756294iple_a: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_11, type, finite972428089iple_a: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > ((hoare_669141180iple_a > $o) > hoare_669141180iple_a) > $o).
% 6.40/2.43 thf(func_def_12, type, finite252461622iple_a: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > ((hoare_669141180iple_a > $o) > hoare_669141180iple_a) > $o).
% 6.40/2.43 thf(func_def_13, type, the_Ho49089901iple_a: (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_14, type, hoare_2128652938rivs_a: (hoare_669141180iple_a > $o) > (hoare_669141180iple_a > $o) > $o).
% 6.40/2.43 thf(func_def_15, type, hoare_1295064928iple_a: (x_a > state > $o) > com > (x_a > state > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_16, type, bot_bo280939947le_a_o: hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_18, type, collec1717965009iple_a: (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_19, type, insert175534902iple_a: hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_20, type, the_el738790235iple_a: (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_21, type, fequal182287803iple_a: hoare_669141180iple_a > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_22, type, member1016246415iple_a: hoare_669141180iple_a > (hoare_669141180iple_a > $o) > $o).
% 6.40/2.43 thf(func_def_23, type, g: hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_24, type, p: x_a > state > $o).
% 6.40/2.43 thf(func_def_25, type, b: state > $o).
% 6.40/2.43 thf(func_def_26, type, c: com).
% 6.40/2.43 thf(func_def_38, type, sK0: !>[X0: $tType]:((X0 > $o) > X0)).
% 6.40/2.43 thf(func_def_39, type, sK1: !>[X0: $tType]:((X0 > $o) > X0)).
% 6.40/2.43 thf(func_def_42, type, sP2: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > hoare_669141180iple_a > (hoare_669141180iple_a > $o) > $o).
% 6.40/2.43 thf(func_def_43, type, sK3: hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_44, type, sK4: hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_45, type, sK5: hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_46, type, sK6: (hoare_669141180iple_a > $o) > hoare_669141180iple_a > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_47, type, sK7: (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_48, type, sK8: (x_a > state > $o) > com > (x_a > state > $o) > (hoare_669141180iple_a > $o) > state).
% 6.40/2.43 thf(func_def_49, type, sK9: (x_a > state > $o) > com > (x_a > state > $o) > (hoare_669141180iple_a > $o) > x_a).
% 6.40/2.43 thf(func_def_50, type, sK10: hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_51, type, sK11: hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_52, type, sK12: (x_a > state > $o) > (x_a > state > $o) > state).
% 6.40/2.43 thf(func_def_53, type, sK13: (x_a > state > $o) > (x_a > state > $o) > x_a).
% 6.40/2.43 thf(func_def_54, type, sK14: (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_55, type, sK15: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_56, type, sK16: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_57, type, sK17: hoare_669141180iple_a > com).
% 6.40/2.43 thf(func_def_58, type, sK18: hoare_669141180iple_a > x_a > state > $o).
% 6.40/2.43 thf(func_def_59, type, sK19: hoare_669141180iple_a > x_a > state > $o).
% 6.40/2.43 thf(func_def_60, type, sK20: ((hoare_669141180iple_a > $o) > $o) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_61, type, sK21: ((hoare_669141180iple_a > $o) > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_62, type, sK22: com > (hoare_669141180iple_a > $o) > (x_a > state > $o) > (x_a > state > $o) > state).
% 6.40/2.43 thf(func_def_63, type, sK23: com > (hoare_669141180iple_a > $o) > (x_a > state > $o) > (x_a > state > $o) > x_a).
% 6.40/2.43 thf(func_def_64, type, sK24: (x_a > state > $o) > (x_a > state > $o) > com > (hoare_669141180iple_a > $o) > (x_a > state > $o) > (x_a > state > $o) > state).
% 6.40/2.43 thf(func_def_65, type, sK25: (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_66, type, sK26: (x_a > state > $o) > (x_a > state > $o) > state).
% 6.40/2.43 thf(func_def_67, type, sK27: (x_a > state > $o) > (x_a > state > $o) > x_a).
% 6.40/2.43 thf(func_def_68, type, sK28: (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_69, type, sK29: (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_70, type, sK30: (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_71, type, sK31: (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_72, type, sK32: hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_73, type, sK33: ((hoare_669141180iple_a > $o) > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_74, type, sK34: ((hoare_669141180iple_a > $o) > $o) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_75, type, sK35: ((hoare_669141180iple_a > $o) > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_76, type, sK36: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_77, type, sK37: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_78, type, sK38: (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_79, type, sK39: (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > state).
% 6.40/2.43 thf(func_def_80, type, sK40: (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > x_a).
% 6.40/2.43 thf(func_def_81, type, sK41: (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > (x_a > state > $o) > state).
% 6.40/2.43 thf(func_def_82, type, sK42: hoare_669141180iple_a > (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_83, type, sK43: (hoare_669141180iple_a > $o) > hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_84, type, sK44: (hoare_669141180iple_a > $o) > hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_85, type, sK45: (hoare_669141180iple_a > $o) > hoare_669141180iple_a > (hoare_669141180iple_a > hoare_669141180iple_a > hoare_669141180iple_a) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_86, type, sK46: (hoare_669141180iple_a > $o) > hoare_669141180iple_a > $o).
% 6.40/2.43 thf(func_def_87, type, sK47: (hoare_669141180iple_a > $o) > hoare_669141180iple_a).
% 6.40/2.43 thf(func_def_89, type, ph49: !>[X0: $tType]:(X0)).
% 6.40/2.43 thf(f865,plain,(
% 6.40/2.43 $false),
% 6.40/2.43 inference(subsumption_resolution,[status(thm)],[f846,f858])).
% 6.40/2.43 thf(f858,plain,(
% 6.40/2.43 ( ! [X1 : $o] : (($true = X1)) )),
% 6.40/2.43 inference(trivial_inequality_removal,[status(thm)],[f848])).
% 6.40/2.43 thf(f848,plain,(
% 6.40/2.43 ( ! [X1 : $o] : (($true = X1) | ($true != $true)) )),
% 6.40/2.43 inference(superposition,[status(thm)],[f803,f675])).
% 6.40/2.43 thf(f675,plain,(
% 6.40/2.43 ( ! [X2 : x_a > state > $o,X3 : hoare_669141180iple_a > $o,X0 : $o,X1 : com,X4 : x_a > state > $o] : (($true = (hoare_2128652938rivs_a @ X3 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ((X2 @ Y0 @ Y1) & X0)))) @ X1 @ X4) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))) | ($true = X0)) )),
% 6.40/2.43 inference(definition_unfolding,[status(thm)],[f526,f639])).
% 6.40/2.43 thf(f639,plain,(
% 6.40/2.43 (bot_bo280939947le_a_o = (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false))))),
% 6.40/2.43 inference(cnf_transformation,[status(thm)],[f120])).
% 6.40/2.43 thf(f120,plain,(
% 6.40/2.43 (bot_bo280939947le_a_o = (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false))))),
% 6.40/2.43 inference(fool_elimination,[status(thm)],[f119])).
% 6.40/2.43 thf(f119,plain,(
% 6.40/2.43 (bot_bo280939947le_a_o = (collec1717965009iple_a @ (^[X0 : hoare_669141180iple_a] : ($false))))),
% 6.40/2.43 inference(rectify,[status(thm)],[f23])).
% 6.40/2.43 thf(f23,axiom,(
% 6.40/2.43 (bot_bo280939947le_a_o = (collec1717965009iple_a @ (^[X52 : hoare_669141180iple_a] : ($false))))),
% 6.40/2.43 file('/export/starexec/sandbox/tmp/tmp.oU5Hx1ZbCZ/DTF2THF_26033.p',fact_22_empty__def)).
% 6.40/2.43 thf(f526,plain,(
% 6.40/2.43 ( ! [X2 : x_a > state > $o,X3 : hoare_669141180iple_a > $o,X0 : $o,X1 : com,X4 : x_a > state > $o] : (($true = (hoare_2128652938rivs_a @ X3 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ((X2 @ Y0 @ Y1) & X0)))) @ X1 @ X4) @ bot_bo280939947le_a_o))) | ($true = X0)) )),
% 6.40/2.43 inference(cnf_transformation,[status(thm)],[f371])).
% 6.40/2.43 thf(f371,plain,(
% 6.40/2.43 ! [X0 : $o,X1 : com,X2 : x_a > state > $o,X3 : hoare_669141180iple_a > $o,X4 : x_a > state > $o] : (($true = (hoare_2128652938rivs_a @ X3 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ((X2 @ Y0 @ Y1) & X0)))) @ X1 @ X4) @ bot_bo280939947le_a_o))) | (($true = X0) & ($true != (hoare_2128652938rivs_a @ X3 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X2 @ X1 @ X4) @ bot_bo280939947le_a_o)))))),
% 6.40/2.43 inference(ennf_transformation,[status(thm)],[f206])).
% 6.40/2.43 thf(f206,plain,(
% 6.40/2.43 ! [X0 : $o,X1 : com,X2 : x_a > state > $o,X3 : hoare_669141180iple_a > $o,X4 : x_a > state > $o] : ((($true = X0) => ($true = (hoare_2128652938rivs_a @ X3 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X2 @ X1 @ X4) @ bot_bo280939947le_a_o)))) => ($true = (hoare_2128652938rivs_a @ X3 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ((X2 @ Y0 @ Y1) & X0)))) @ X1 @ X4) @ bot_bo280939947le_a_o))))),
% 6.40/2.43 inference(fool_elimination,[status(thm)],[f205])).
% 6.40/2.43 thf(f205,plain,(
% 6.40/2.43 ! [X0 : $o,X1 : com,X2 : x_a > state > $o,X3 : hoare_669141180iple_a > $o,X4 : x_a > state > $o] : ((X0 => (hoare_2128652938rivs_a @ X3 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X2 @ X1 @ X4) @ bot_bo280939947le_a_o))) => (hoare_2128652938rivs_a @ X3 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X5 : x_a, X6 : state] : ((X2 @ X5 @ X6) & X0)) @ X1 @ X4) @ bot_bo280939947le_a_o)))),
% 6.40/2.43 inference(rectify,[status(thm)],[f5])).
% 6.40/2.43 thf(f5,axiom,(
% 6.40/2.43 ! [X17 : $o,X15 : com,X14 : x_a > state > $o,X13 : hoare_669141180iple_a > $o,X16 : x_a > state > $o] : ((X17 => (hoare_2128652938rivs_a @ X13 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X14 @ X15 @ X16) @ bot_bo280939947le_a_o))) => (hoare_2128652938rivs_a @ X13 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X18 : x_a, X19 : state] : ((X14 @ X18 @ X19) & X17)) @ X15 @ X16) @ bot_bo280939947le_a_o)))),
% 6.40/2.43 file('/export/starexec/sandbox/tmp/tmp.oU5Hx1ZbCZ/DTF2THF_26033.p',fact_4_constant)).
% 6.40/2.43 thf(f803,plain,(
% 6.40/2.43 ( ! [X0 : x_a > state > $o] : (($true != (hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false))))))) )),
% 6.40/2.43 inference(trivial_inequality_removal,[status(thm)],[f802])).
% 6.40/2.43 thf(f802,plain,(
% 6.40/2.43 ( ! [X0 : x_a > state > $o] : (($true = $false) | ($true != (hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false))))))) )),
% 6.40/2.43 inference(beta_eta_normalization,[status(thm)],[f801])).
% 6.40/2.43 thf(f801,plain,(
% 6.40/2.43 ( ! [X0 : x_a > state > $o] : (($true = ((^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ (sK27 @ X0 @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false))))) @ (sK26 @ X0 @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false))))))) | ($true != (hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false))))))) )),
% 6.40/2.43 inference(trivial_inequality_removal,[status(thm)],[f798])).
% 6.40/2.43 thf(f798,plain,(
% 6.40/2.43 ( ! [X0 : x_a > state > $o] : (($true = ((^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ (sK27 @ X0 @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false))))) @ (sK26 @ X0 @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false))))))) | ($true != $true) | ($true != (hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false))))))) )),
% 6.40/2.43 inference(superposition,[status(thm)],[f700,f721])).
% 6.40/2.43 thf(f721,plain,(
% 6.40/2.43 ( ! [X2 : hoare_669141180iple_a > $o,X3 : com,X0 : x_a > state > $o,X1 : x_a > state > $o,X4 : x_a > state > $o] : (($true = (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ X3 @ X4) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))) | ($true != (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X1 @ X3 @ X4) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))) | ($true = (X0 @ (sK27 @ X1 @ X0) @ (sK26 @ X1 @ X0)))) )),
% 6.40/2.43 inference(definition_unfolding,[status(thm)],[f598,f639,f639])).
% 6.40/2.43 thf(f598,plain,(
% 6.40/2.43 ( ! [X2 : hoare_669141180iple_a > $o,X3 : com,X0 : x_a > state > $o,X1 : x_a > state > $o,X4 : x_a > state > $o] : (($true != (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X1 @ X3 @ X4) @ bot_bo280939947le_a_o))) | ($true = (X0 @ (sK27 @ X1 @ X0) @ (sK26 @ X1 @ X0))) | ($true = (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ X3 @ X4) @ bot_bo280939947le_a_o)))) )),
% 6.40/2.43 inference(cnf_transformation,[status(thm)],[f456])).
% 6.40/2.43 thf(f456,plain,(
% 6.40/2.43 ! [X0 : x_a > state > $o,X1 : x_a > state > $o,X2 : hoare_669141180iple_a > $o,X3 : com,X4 : x_a > state > $o] : (($true != (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X1 @ X3 @ X4) @ bot_bo280939947le_a_o))) | (((X1 @ (sK27 @ X1 @ X0) @ (sK26 @ X1 @ X0)) != $true) & ($true = (X0 @ (sK27 @ X1 @ X0) @ (sK26 @ X1 @ X0)))) | ($true = (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ X3 @ X4) @ bot_bo280939947le_a_o))))),
% 6.40/2.43 inference(skolemisation,[status(esa),new_symbols(skolem,[sK26,sK27])],[f405,f455])).
% 6.40/2.43 thf(f455,plain,(
% 6.40/2.43 ! [X0 : x_a > state > $o,X1 : x_a > state > $o] : (? [X5 : state,X6 : x_a] : (($true != (X1 @ X6 @ X5)) & ((X0 @ X6 @ X5) = $true)) => (((X1 @ (sK27 @ X1 @ X0) @ (sK26 @ X1 @ X0)) != $true) & ($true = (X0 @ (sK27 @ X1 @ X0) @ (sK26 @ X1 @ X0)))))),
% 6.40/2.43 introduced(definition,[],[choice_axiom])).
% 6.40/2.43 thf(f405,plain,(
% 6.40/2.43 ! [X0 : x_a > state > $o,X1 : x_a > state > $o,X2 : hoare_669141180iple_a > $o,X3 : com,X4 : x_a > state > $o] : (($true != (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X1 @ X3 @ X4) @ bot_bo280939947le_a_o))) | ? [X5 : state,X6 : x_a] : (($true != (X1 @ X6 @ X5)) & ((X0 @ X6 @ X5) = $true)) | ($true = (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ X3 @ X4) @ bot_bo280939947le_a_o))))),
% 6.40/2.43 inference(flattening,[status(thm)],[f404])).
% 6.40/2.43 thf(f404,plain,(
% 6.40/2.43 ! [X0 : x_a > state > $o,X1 : x_a > state > $o,X2 : hoare_669141180iple_a > $o,X3 : com,X4 : x_a > state > $o] : ((($true = (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ X3 @ X4) @ bot_bo280939947le_a_o))) | ? [X5 : state,X6 : x_a] : (($true != (X1 @ X6 @ X5)) & ((X0 @ X6 @ X5) = $true))) | ($true != (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X1 @ X3 @ X4) @ bot_bo280939947le_a_o))))),
% 6.40/2.43 inference(ennf_transformation,[status(thm)],[f182])).
% 6.40/2.43 thf(f182,plain,(
% 6.40/2.43 ! [X0 : x_a > state > $o,X1 : x_a > state > $o,X2 : hoare_669141180iple_a > $o,X3 : com,X4 : x_a > state > $o] : (($true = (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X1 @ X3 @ X4) @ bot_bo280939947le_a_o))) => (! [X5 : state,X6 : x_a] : (((X0 @ X6 @ X5) = $true) => ($true = (X1 @ X6 @ X5))) => ($true = (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ X3 @ X4) @ bot_bo280939947le_a_o)))))),
% 6.40/2.43 inference(fool_elimination,[status(thm)],[f181])).
% 6.40/2.43 thf(f181,plain,(
% 6.40/2.43 ! [X0 : x_a > state > $o,X1 : x_a > state > $o,X2 : hoare_669141180iple_a > $o,X3 : com,X4 : x_a > state > $o] : ((hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X1 @ X3 @ X4) @ bot_bo280939947le_a_o)) => (! [X5 : state,X6 : x_a] : ((X0 @ X6 @ X5) => (X1 @ X6 @ X5)) => (hoare_2128652938rivs_a @ X2 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X0 @ X3 @ X4) @ bot_bo280939947le_a_o))))),
% 6.40/2.43 inference(rectify,[status(thm)],[f8])).
% 6.40/2.43 thf(f8,axiom,(
% 6.40/2.43 ! [X32 : x_a > state > $o,X34 : x_a > state > $o,X33 : hoare_669141180iple_a > $o,X35 : com,X36 : x_a > state > $o] : ((hoare_2128652938rivs_a @ X33 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X34 @ X35 @ X36) @ bot_bo280939947le_a_o)) => (! [X19 : state,X18 : x_a] : ((X32 @ X18 @ X19) => (X34 @ X18 @ X19)) => (hoare_2128652938rivs_a @ X33 @ (insert175534902iple_a @ (hoare_1295064928iple_a @ X32 @ X35 @ X36) @ bot_bo280939947le_a_o))))),
% 6.40/2.43 file('/export/starexec/sandbox/tmp/tmp.oU5Hx1ZbCZ/DTF2THF_26033.p',fact_7_conseq1)).
% 6.40/2.43 thf(f700,plain,(
% 6.40/2.43 ($true != (hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false))))))),
% 6.40/2.43 inference(definition_unfolding,[status(thm)],[f565,f639])).
% 6.40/2.43 thf(f565,plain,(
% 6.40/2.43 ((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ bot_bo280939947le_a_o)) != $true)),
% 6.40/2.43 inference(cnf_transformation,[status(thm)],[f329])).
% 6.40/2.43 thf(f329,plain,(
% 6.40/2.43 ((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ bot_bo280939947le_a_o)) != $true)),
% 6.40/2.43 inference(flattening,[status(thm)],[f186])).
% 6.40/2.43 thf(f186,plain,(
% 6.40/2.43 ~((hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[Y0 : x_a]: ((^[Y1 : state]: ($false)))) @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1))))))) @ bot_bo280939947le_a_o)) = $true)),
% 6.40/2.43 inference(fool_elimination,[status(thm)],[f185])).
% 6.40/2.43 thf(f185,plain,(
% 6.40/2.43 ~(hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X0 : x_a, X1 : state] : ($false)) @ c @ (^[X2 : x_a, X3 : state] : ((p @ X2 @ X3) & (~ (b @ X3))))) @ bot_bo280939947le_a_o))),
% 6.40/2.43 inference(rectify,[status(thm)],[f99])).
% 6.40/2.43 thf(f99,negated_conjecture,(
% 6.40/2.43 ~(hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X18 : x_a, X19 : state] : ($false)) @ c @ (^[X18 : x_a, X19 : state] : ((p @ X18 @ X19) & (~ (b @ X19))))) @ bot_bo280939947le_a_o))),
% 6.40/2.43 inference(negated_conjecture,[status(cth)],[f98])).
% 6.40/2.43 thf(f98,conjecture,(
% 6.40/2.43 (hoare_2128652938rivs_a @ g @ (insert175534902iple_a @ (hoare_1295064928iple_a @ (^[X18 : x_a, X19 : state] : ($false)) @ c @ (^[X18 : x_a, X19 : state] : ((p @ X18 @ X19) & (~ (b @ X19))))) @ bot_bo280939947le_a_o))),
% 6.40/2.43 file('/export/starexec/sandbox/tmp/tmp.oU5Hx1ZbCZ/DTF2THF_26033.p',conj_0)).
% 6.40/2.43 thf(f846,plain,(
% 6.40/2.43 ( ! [X0 : x_a > state > $o] : (((hoare_2128652938rivs_a @ g @ (collec1717965009iple_a @ (fequal182287803iple_a @ (hoare_1295064928iple_a @ X0 @ c @ (^[Y0 : x_a]: ((^[Y1 : state]: ((p @ Y0 @ Y1) & (~ (b @ Y1)))))))))) != $true)) )),
% 6.40/2.43 inference(superposition,[status(thm)],[f803,f691])).
% 6.40/2.43 thf(f691,plain,(
% 6.40/2.43 ( ! [X0 : hoare_669141180iple_a] : (((collec1717965009iple_a @ (fequal182287803iple_a @ X0)) = (insert175534902iple_a @ X0 @ (collec1717965009iple_a @ (^[Y0 : hoare_669141180iple_a]: ($false)))))) )),
% 6.40/2.43 inference(definition_unfolding,[status(thm)],[f554,f639])).
% 6.40/2.43 thf(f554,plain,(
% 6.40/2.43 ( ! [X0 : hoare_669141180iple_a] : (((insert175534902iple_a @ X0 @ bot_bo280939947le_a_o) = (collec1717965009iple_a @ (fequal182287803iple_a @ X0)))) )),
% 6.40/2.43 inference(cnf_transformation,[status(thm)],[f126])).
% 6.40/2.43 thf(f126,plain,(
% 6.40/2.43 ! [X0 : hoare_669141180iple_a] : ((insert175534902iple_a @ X0 @ bot_bo280939947le_a_o) = (collec1717965009iple_a @ (fequal182287803iple_a @ X0)))),
% 6.40/2.43 inference(fool_elimination,[status(thm)],[f125])).
% 6.40/2.43 thf(f125,plain,(
% 6.40/2.43 ! [X0 : hoare_669141180iple_a] : ((insert175534902iple_a @ X0 @ bot_bo280939947le_a_o) = (collec1717965009iple_a @ (fequal182287803iple_a @ X0)))),
% 6.40/2.43 inference(rectify,[status(thm)],[f13])).
% 6.40/2.43 thf(f13,axiom,(
% 6.40/2.43 ! [X50 : hoare_669141180iple_a] : ((collec1717965009iple_a @ (fequal182287803iple_a @ X50)) = (insert175534902iple_a @ X50 @ bot_bo280939947le_a_o))),
% 6.40/2.43 file('/export/starexec/sandbox/tmp/tmp.oU5Hx1ZbCZ/DTF2THF_26033.p',fact_12_singleton__conv2)).
% 6.40/2.43 % SZS output end Proof for DTF2THF_26033
% 6.40/2.43 % (26190)------------------------------
% 6.40/2.43 % (26190)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 6.40/2.43 % (26190)Termination reason: Refutation
% 6.40/2.43
% 6.40/2.43 % (26190)Memory used [KB]: 6652
% 6.40/2.43 % (26190)Time elapsed: 0.050 s
% 6.40/2.43 % (26190)Instructions burned: 90 (million)
% 6.40/2.43 % (26190)------------------------------
% 6.40/2.43 % (26190)------------------------------
% 6.40/2.43 % (26146)Success in time 0.574 s
%------------------------------------------------------------------------------