%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWW474+2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:29:49 PM UTC 2026
% Result : Theorem 52.78s 9.47s
% Output : CNFRefutation 52.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 32
% Syntax : Number of formulae : 140 ( 68 unt; 9 def)
% Number of atoms : 310 ( 85 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 193 ( 82 ~; 97 |; 3 &)
% ( 1 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 13 ( 11 usr; 10 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 16 con; 0-2 aty)
% Number of variables : 127 ( 0 sgn 125 !; 2 ?; 52 :)
% Comments :
%------------------------------------------------------------------------------
fof(f23,axiom,
is_bool(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_fFalse) ).
fof(f24,axiom,
is_bool(fTrue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_fTrue) ).
fof(f31,axiom,
! [X0,X1] :
( is_bool(X1)
=> is_bool(hAPP_bool_bool(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_hAPP_000tc__HOL__Obool_000tc__HOL__Obool) ).
fof(f44,axiom,
! [X0,X1] : is_bool(hAPP_f1760790145l_bool(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_hAPP_000tc__fun_Itc__Hoare____Mirabelle____ddpglwnxwg__Otriple_Itc__Com__O_004) ).
fof(f55,axiom,
! [X0] : hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),bot_bo1055319631e_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_empty) ).
fof(f59,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X2))
=> ( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X1))
=> hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_cut) ).
fof(f108,axiom,
! [X0] :
( hBOOL(hoare_298929751gleton)
=> ( hBOOL(wT_bodies)
=> ( hBOOL(hAPP_com_bool(wt,X0))
=> hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_MGF) ).
fof(f126,axiom,
! [X0] :
( hAPP_f921536533e_bool(collec727977250_state,X0) = bot_bo1055319631e_bool
<=> ! [X1] : ~ hBOOL(hAPP_H513860823e_bool(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_Collect__empty__eq) ).
fof(f140,axiom,
bot_bo1055319631e_bool = hAPP_f921536533e_bool(collec727977250_state,cOMBK_1079618832_state(fFalse)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_empty__def) ).
fof(f232,axiom,
! [X0] : hAPP_f921536533e_bool(collec727977250_state,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_Collect__def) ).
fof(f268,axiom,
! [X0] : hAPP_f921536533e_bool(collec727977250_state,hAPP_H1645666623e_bool(fequal1531560888_state,X0)) = hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_singleton__conv2) ).
fof(f270,axiom,
! [X0,X1] :
( hBOOL(wT_bodies)
=> ( hAPP_p799580910on_com(body,X0) = some_com(X1)
=> hBOOL(hAPP_com_bool(wt,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_WT__bodiesD) ).
fof(f458,axiom,
! [X0] : set_Ho1831989999_state(some_H1133819688_state(X0)) = hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_403_Option_Oset_Osimps_I2_J) ).
fof(f754,axiom,
! [X0] :
( ~ hBOOL(X0)
| ~ hBOOL(hAPP_bool_bool(fNot,X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fNot_1_1_U) ).
fof(f755,axiom,
! [X0] :
( hBOOL(hAPP_bool_bool(fNot,X0))
| hBOOL(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fNot_2_1_U) ).
fof(f764,axiom,
! [X0,X1] :
( hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,X1),X0))
| hBOOL(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_1_1_U) ).
fof(f766,axiom,
! [X0,X1] :
( hBOOL(X1)
| ~ hBOOL(X0)
| ~ hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,X0),X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fimplies_3_1_U) ).
fof(f789,axiom,
! [X0] :
( is_bool(X0)
=> ( X0 = fFalse
| X0 = fTrue ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_If_000tc__Hoare____Mirabelle____ddpglwnxwg__Otriple_Itc__Com__Ostate) ).
fof(f803,axiom,
! [X0,X1] :
( is_bool(X0)
=> hAPP_H513860823e_bool(cOMBK_1079618832_state(X0),X1) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Hoare____Mirabelle____ddpglwnxwg__) ).
fof(f861,axiom,
hBOOL(hoare_298929751gleton),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f862,axiom,
hBOOL(wT_bodies),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
fof(f866,axiom,
hAPP_p799580910on_com(body,pn) = some_com(y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_5) ).
fof(f868,conjecture,
hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_7) ).
fof(f869,negated_conjecture,
~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
inference(negated_conjecture,[status(cth)],[f868]) ).
fof(f876,plain,
~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
inference(flattening,[],[f869]) ).
fof(f886,plain,
! [X0,X1] :
( ~ is_bool(X1)
| is_bool(hAPP_bool_bool(X0,X1)) ),
inference(ennf_transformation,[],[f31]) ).
fof(f900,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X2))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X1))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X2)) ),
inference(ennf_transformation,[],[f59]) ).
fof(f901,plain,
! [X0,X1,X2] :
( ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X2))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X1))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X2)) ),
inference(flattening,[],[f900]) ).
fof(f958,plain,
! [X0] :
( ~ hBOOL(hoare_298929751gleton)
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hAPP_com_bool(wt,X0))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool))) ),
inference(ennf_transformation,[],[f108]) ).
fof(f959,plain,
! [X0] :
( ~ hBOOL(hoare_298929751gleton)
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hAPP_com_bool(wt,X0))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool))) ),
inference(flattening,[],[f958]) ).
fof(f1082,plain,
! [X0,X1] :
( ~ hBOOL(wT_bodies)
| hAPP_p799580910on_com(body,X0) != some_com(X1)
| hBOOL(hAPP_com_bool(wt,X1)) ),
inference(ennf_transformation,[],[f270]) ).
fof(f1083,plain,
! [X0,X1] :
( ~ hBOOL(wT_bodies)
| hAPP_p799580910on_com(body,X0) != some_com(X1)
| hBOOL(hAPP_com_bool(wt,X1)) ),
inference(flattening,[],[f1082]) ).
fof(f1574,plain,
! [X0] :
( ~ is_bool(X0)
| X0 = fFalse
| X0 = fTrue ),
inference(ennf_transformation,[],[f789]) ).
fof(f1575,plain,
! [X0] :
( ~ is_bool(X0)
| X0 = fFalse
| X0 = fTrue ),
inference(flattening,[],[f1574]) ).
fof(f1576,plain,
! [X0,X1] :
( ~ is_bool(X0)
| hAPP_H513860823e_bool(cOMBK_1079618832_state(X0),X1) = X0 ),
inference(ennf_transformation,[],[f803]) ).
fof(f1592,plain,
! [X0] :
( ( bot_bo1055319631e_bool != hAPP_f921536533e_bool(collec727977250_state,X0)
| ! [X1] : ~ hBOOL(hAPP_H513860823e_bool(X0,X1)) )
& ( ? [X1] : hBOOL(hAPP_H513860823e_bool(X0,X1))
| hAPP_f921536533e_bool(collec727977250_state,X0) = bot_bo1055319631e_bool ) ),
inference(nnf_transformation,[],[f126]) ).
fof(f1593,plain,
! [X0] :
( ( bot_bo1055319631e_bool != hAPP_f921536533e_bool(collec727977250_state,X0)
| ! [X2] : ~ hBOOL(hAPP_H513860823e_bool(X0,X2)) )
& ( ? [X1] : hBOOL(hAPP_H513860823e_bool(X0,X1))
| hAPP_f921536533e_bool(collec727977250_state,X0) = bot_bo1055319631e_bool ) ),
inference(rectify,[],[f1592]) ).
fof(f1594,plain,
! [X0] :
( ( bot_bo1055319631e_bool != hAPP_f921536533e_bool(collec727977250_state,X0)
| ! [X2] : ~ hBOOL(hAPP_H513860823e_bool(X0,X2)) )
& ( hBOOL(hAPP_H513860823e_bool(X0,sK5(X0)))
| hAPP_f921536533e_bool(collec727977250_state,X0) = bot_bo1055319631e_bool ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X1,sK5(X0))],[f1593]) ).
fof(f1917,plain,
is_bool(fFalse),
inference(cnf_transformation,[],[f23]) ).
fof(f1918,plain,
is_bool(fTrue),
inference(cnf_transformation,[],[f24]) ).
fof(f1925,plain,
! [X0,X1] :
( ~ is_bool(X1)
| is_bool(hAPP_bool_bool(X0,X1)) ),
inference(cnf_transformation,[],[f886]) ).
fof(f1938,plain,
! [X0,X1] : is_bool(hAPP_f1760790145l_bool(X0,X1)),
inference(cnf_transformation,[],[f44]) ).
fof(f1949,plain,
! [X0] : hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),bot_bo1055319631e_bool)),
inference(cnf_transformation,[],[f55]) ).
fof(f1953,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X2))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X1))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X2)) ),
inference(cnf_transformation,[],[f901]) ).
fof(f2009,plain,
! [X0] :
( ~ hBOOL(hoare_298929751gleton)
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hAPP_com_bool(wt,X0))
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool))) ),
inference(cnf_transformation,[],[f959]) ).
fof(f2035,plain,
! [X0] :
( hBOOL(hAPP_H513860823e_bool(X0,sK5(X0)))
| bot_bo1055319631e_bool = hAPP_f921536533e_bool(collec727977250_state,X0) ),
inference(cnf_transformation,[],[f1594]) ).
fof(f2061,plain,
bot_bo1055319631e_bool = hAPP_f921536533e_bool(collec727977250_state,cOMBK_1079618832_state(fFalse)),
inference(cnf_transformation,[],[f140]) ).
fof(f2204,plain,
! [X0] : hAPP_f921536533e_bool(collec727977250_state,X0) = X0,
inference(cnf_transformation,[],[f232]) ).
fof(f2259,plain,
! [X0] : hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool) = hAPP_f921536533e_bool(collec727977250_state,hAPP_H1645666623e_bool(fequal1531560888_state,X0)),
inference(cnf_transformation,[],[f268]) ).
fof(f2263,plain,
! [X0,X1] :
( ~ hBOOL(wT_bodies)
| hAPP_p799580910on_com(body,X0) != some_com(X1)
| hBOOL(hAPP_com_bool(wt,X1)) ),
inference(cnf_transformation,[],[f1083]) ).
fof(f2634,plain,
! [X0] : hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool) = set_Ho1831989999_state(some_H1133819688_state(X0)),
inference(cnf_transformation,[],[f458]) ).
fof(f3080,plain,
! [X0] :
( ~ hBOOL(X0)
| ~ hBOOL(hAPP_bool_bool(fNot,X0)) ),
inference(cnf_transformation,[],[f754]) ).
fof(f3081,plain,
! [X0] :
( hBOOL(hAPP_bool_bool(fNot,X0))
| hBOOL(X0) ),
inference(cnf_transformation,[],[f755]) ).
fof(f3090,plain,
! [X0,X1] :
( hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,X1),X0))
| hBOOL(X1) ),
inference(cnf_transformation,[],[f764]) ).
fof(f3092,plain,
! [X0,X1] :
( hBOOL(X1)
| ~ hBOOL(X0)
| ~ hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,X0),X1)) ),
inference(cnf_transformation,[],[f766]) ).
fof(f3115,plain,
! [X0] :
( ~ is_bool(X0)
| fFalse = X0
| fTrue = X0 ),
inference(cnf_transformation,[],[f1575]) ).
fof(f3129,plain,
! [X0,X1] :
( ~ is_bool(X0)
| hAPP_H513860823e_bool(cOMBK_1079618832_state(X0),X1) = X0 ),
inference(cnf_transformation,[],[f1576]) ).
fof(f3187,plain,
hBOOL(hoare_298929751gleton),
inference(cnf_transformation,[],[f861]) ).
fof(f3188,plain,
hBOOL(wT_bodies),
inference(cnf_transformation,[],[f862]) ).
fof(f3192,plain,
hAPP_p799580910on_com(body,pn) = some_com(y),
inference(cnf_transformation,[],[f866]) ).
fof(f3194,plain,
~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
inference(cnf_transformation,[],[f876]) ).
tcf(c_71,plain,
is_bool(fFalse),
inference(cnf_transformation,[],[f1917]) ).
tcf(c_72,plain,
is_bool(fTrue),
inference(cnf_transformation,[],[f1918]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( is_bool(hAPP_bool_bool(X1,X0))
| ~ is_bool(X0) ),
inference(cnf_transformation,[],[f1925]) ).
tcf(c_92,plain,
! [X0: $i,X1: $i] : is_bool(hAPP_f1760790145l_bool(X0,X1)),
inference(cnf_transformation,[],[f1938]) ).
tcf(c_103,plain,
! [X0: $i] : hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),bot_bo1055319631e_bool)),
inference(cnf_transformation,[],[f1949]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X2))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X2))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X1)) ),
inference(cnf_transformation,[],[f1953]) ).
tcf(c_163,plain,
! [X0: $i] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool)))
| ~ hBOOL(hoare_298929751gleton)
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hAPP_com_bool(wt,X0)) ),
inference(cnf_transformation,[],[f2009]) ).
tcf(c_188,plain,
! [X0: $i] :
( hBOOL(hAPP_H513860823e_bool(X0,sK5(X0)))
| ( hAPP_f921536533e_bool(collec727977250_state,X0) = bot_bo1055319631e_bool ) ),
inference(cnf_transformation,[],[f2035]) ).
tcf(c_215,plain,
hAPP_f921536533e_bool(collec727977250_state,cOMBK_1079618832_state(fFalse)) = bot_bo1055319631e_bool,
inference(cnf_transformation,[],[f2061]) ).
tcf(c_357,plain,
! [X0: $i] : hAPP_f921536533e_bool(collec727977250_state,X0) = X0,
inference(cnf_transformation,[],[f2204]) ).
tcf(c_412,plain,
! [X0: $i] : hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool) = hAPP_f921536533e_bool(collec727977250_state,hAPP_H1645666623e_bool(fequal1531560888_state,X0)),
inference(cnf_transformation,[],[f2259]) ).
tcf(c_416,plain,
! [X0: $i,X1: $i] :
( hBOOL(hAPP_com_bool(wt,X1))
| ~ hBOOL(wT_bodies)
| ( hAPP_p799580910on_com(body,X0) != some_com(X1) ) ),
inference(cnf_transformation,[],[f2263]) ).
tcf(c_776,plain,
! [X0: $i] : hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool) = set_Ho1831989999_state(some_H1133819688_state(X0)),
inference(cnf_transformation,[],[f2634]) ).
tcf(c_1219,plain,
! [X0: $i] :
( ~ hBOOL(X0)
| ~ hBOOL(hAPP_bool_bool(fNot,X0)) ),
inference(cnf_transformation,[],[f3080]) ).
tcf(c_1220,plain,
! [X0: $i] :
( hBOOL(X0)
| hBOOL(hAPP_bool_bool(fNot,X0)) ),
inference(cnf_transformation,[],[f3081]) ).
tcf(c_1229,plain,
! [X0: $i,X1: $i] :
( hBOOL(X0)
| hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,X0),X1)) ),
inference(cnf_transformation,[],[f3090]) ).
tcf(c_1231,plain,
! [X0: $i,X1: $i] :
( hBOOL(X1)
| ~ hBOOL(X0)
| ~ hBOOL(hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,X0),X1)) ),
inference(cnf_transformation,[],[f3092]) ).
tcf(c_1254,plain,
! [X0: $i] :
( ( X0 = fTrue )
| ( X0 = fFalse )
| ~ is_bool(X0) ),
inference(cnf_transformation,[],[f3115]) ).
tcf(c_1268,plain,
! [X0: $i,X1: $i] :
( ( hAPP_H513860823e_bool(cOMBK_1079618832_state(X0),X1) = X0 )
| ~ is_bool(X0) ),
inference(cnf_transformation,[],[f3129]) ).
tcf(c_1326,plain,
hBOOL(hoare_298929751gleton),
inference(cnf_transformation,[],[f3187]) ).
tcf(c_1327,plain,
hBOOL(wT_bodies),
inference(cnf_transformation,[],[f3188]) ).
tcf(c_1331,plain,
hAPP_p799580910on_com(body,pn) = some_com(y),
inference(cnf_transformation,[],[f3192]) ).
tcf(c_1333,negated_conjecture,
~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)),bot_bo1055319631e_bool))),
inference(cnf_transformation,[],[f3194]) ).
tcf(c_2277,plain,
! [X0: $i] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,X0)) ),
inference(global_subsumption_just,[status(thm)],[c_163,c_1327,c_1326,c_163]) ).
tcf(c_2635,plain,
! [X0: $i] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)),bot_bo1055319631e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,X0)) ),
inference(prop_impl_just,[status(thm)],[c_2277]) ).
tcf(c_2733,plain,
! [X0: $i] :
( hBOOL(hAPP_H513860823e_bool(X0,sK5(X0)))
| ( hAPP_f921536533e_bool(collec727977250_state,X0) = bot_bo1055319631e_bool ) ),
inference(prop_impl_just,[status(thm)],[c_188]) ).
tcf(c_9994,plain,
cOMBK_1079618832_state(fFalse) = bot_bo1055319631e_bool,
inference(demodulation,[status(thm)],[c_215,c_357]) ).
tcf(c_10309,plain,
! [X0: $i] :
( hBOOL(hAPP_H513860823e_bool(X0,sK5(X0)))
| ( X0 = bot_bo1055319631e_bool ) ),
inference(light_normalisation,[status(thm)],[c_2733,c_357]) ).
tcf(c_10383,plain,
! [X0: $i] : hAPP_f921536533e_bool(collec727977250_state,hAPP_H1645666623e_bool(fequal1531560888_state,X0)) = set_Ho1831989999_state(some_H1133819688_state(X0)),
inference(light_normalisation,[status(thm)],[c_412,c_776]) ).
tcf(c_10384,plain,
! [X0: $i] : hAPP_H1645666623e_bool(fequal1531560888_state,X0) = set_Ho1831989999_state(some_H1133819688_state(X0)),
inference(demodulation,[status(thm)],[c_10383,c_357]) ).
tcf(c_10386,plain,
! [X0: $i] : hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool) = hAPP_H1645666623e_bool(fequal1531560888_state,X0),
inference(demodulation,[status(thm)],[c_776,c_10384]) ).
tcf(c_10865,plain,
! [X0: $i] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_H1645666623e_bool(fequal1531560888_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0))))
| ~ hBOOL(hAPP_com_bool(wt,X0)) ),
inference(demodulation,[status(thm)],[c_2635,c_10386]) ).
tcf(c_11468,plain,
~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(hAPP_f631639356e_bool(image_275883510_state(hAPP_f1758910594_state(cOMBB_422605457_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_H1645666623e_bool(fequal1531560888_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)))),
inference(demodulation,[status(thm)],[c_1333,c_10386]) ).
tcf(c_28962,plain,
! [X0: $i] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_H1645666623e_bool(fequal1531560888_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0))))
| ~ hBOOL(hAPP_com_bool(wt,X0)) ),
inference(prop_impl_just,[status(thm)],[c_10865]) ).
tcf(c_29102,plain,
! [X0: $i,X1: $i] :
( ( hAPP_p799580910on_com(body,X0) != some_com(X1) )
| hBOOL(hAPP_com_bool(wt,X1)) ),
inference(prop_impl_just,[status(thm)],[c_1327,c_416]) ).
tcf(c_29103,plain,
! [X0: $i,X1: $i] :
( hBOOL(hAPP_com_bool(wt,X1))
| ( hAPP_p799580910on_com(body,X0) != some_com(X1) ) ),
inference(renaming,[status(thm)],[c_29102]) ).
tcf(c_29498,plain,
! [X0: $i] :
( hBOOL(hAPP_H513860823e_bool(X0,sK5(X0)))
| ( X0 = bot_bo1055319631e_bool ) ),
inference(prop_impl_just,[status(thm)],[c_10309]) ).
tcf(c_41182,definition,
iPr_def_10 = cOMBB_422605457_pname(hoare_Mirabelle_MGT),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_41183,definition,
iPr_def_11 = hAPP_f1758910594_state(iPr_def_10,body_1),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_41184,definition,
iPr_def_12 = image_275883510_state(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_41185,definition,
iPr_def_13 = dom_pname_com(body),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_41186,definition,
iPr_def_14 = hAPP_f631639356e_bool(iPr_def_12,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_41187,definition,
iPr_def_15 = hoare_659004819_state(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_41188,definition,
iPr_def_16 = hAPP_c1546227244_state(hoare_Mirabelle_MGT,y),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_41189,definition,
iPr_def_17 = hAPP_H1645666623e_bool(fequal1531560888_state,iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_41190,definition,
iPr_def_18 = hAPP_f1760790145l_bool(iPr_def_15,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_41191,plain,
~ hBOOL(iPr_def_18),
inference(demodulation,[status(thm)],[c_11468,c_41188,c_41189,c_41185,c_41182,c_41183,c_41184,c_41186,c_41187,c_41190]) ).
tcf(c_59996,plain,
is_bool(iPr_def_18),
inference(superposition,[status(thm)],[c_41190,c_92]) ).
tcf(c_60607,plain,
! [X0: $i] : hAPP_H513860823e_bool(cOMBK_1079618832_state(fFalse),X0) = fFalse,
inference(superposition,[status(thm)],[c_71,c_1268]) ).
tcf(c_60622,plain,
! [X0: $i] : hAPP_H513860823e_bool(cOMBK_1079618832_state(iPr_def_18),X0) = iPr_def_18,
inference(superposition,[status(thm)],[c_59996,c_1268]) ).
tcf(c_60623,plain,
! [X0: $i] : hAPP_H513860823e_bool(bot_bo1055319631e_bool,X0) = fFalse,
inference(light_normalisation,[status(thm)],[c_60607,c_9994]) ).
tcf(c_60820,plain,
( hBOOL(iPr_def_18)
| ( cOMBK_1079618832_state(iPr_def_18) = bot_bo1055319631e_bool ) ),
inference(superposition,[status(thm)],[c_60622,c_29498]) ).
tcf(c_60822,plain,
cOMBK_1079618832_state(iPr_def_18) = bot_bo1055319631e_bool,
inference(forward_subsumption_resolution,[status(thm)],[c_60820,c_41191]) ).
tcf(c_60823,plain,
! [X0: $i] : hAPP_H513860823e_bool(bot_bo1055319631e_bool,X0) = iPr_def_18,
inference(demodulation,[status(thm)],[c_60622,c_60822]) ).
tcf(c_60824,plain,
fFalse = iPr_def_18,
inference(demodulation,[status(thm)],[c_60623,c_60823]) ).
tcf(c_61341,plain,
! [X0: $i] :
( ( X0 = iPr_def_18 )
| ( X0 = fTrue )
| ~ is_bool(X0) ),
inference(light_normalisation,[status(thm)],[c_1254,c_60824]) ).
tcf(c_61365,plain,
! [X0: $i,X1: $i] :
( ( hAPP_bool_bool(X1,X0) = iPr_def_18 )
| ( hAPP_bool_bool(X1,X0) = fTrue )
| ~ is_bool(X0) ),
inference(superposition,[status(thm)],[c_79,c_61341]) ).
tcf(c_62199,plain,
! [X0: $i] :
( ( hAPP_bool_bool(X0,fTrue) = iPr_def_18 )
| ( hAPP_bool_bool(X0,fTrue) = fTrue ) ),
inference(superposition,[status(thm)],[c_72,c_61365]) ).
tcf(c_62213,plain,
! [X0: $i] :
( ( hAPP_bool_bool(X0,iPr_def_18) = iPr_def_18 )
| ( hAPP_bool_bool(X0,iPr_def_18) = fTrue ) ),
inference(superposition,[status(thm)],[c_59996,c_61365]) ).
tcf(c_62716,plain,
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_H1645666623e_bool(fequal1531560888_state,iPr_def_16)))
| ~ hBOOL(hAPP_com_bool(wt,y)) ),
inference(superposition,[status(thm)],[c_41188,c_28962]) ).
tcf(c_62719,plain,
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),iPr_def_17))
| ~ hBOOL(hAPP_com_bool(wt,y)) ),
inference(light_normalisation,[status(thm)],[c_62716,c_41189]) ).
tcf(c_63560,plain,
( ( hAPP_bool_bool(fNot,fTrue) = iPr_def_18 )
| ~ hBOOL(fTrue) ),
inference(superposition,[status(thm)],[c_62199,c_1219]) ).
tcf(c_63561,plain,
( hBOOL(fTrue)
| ( hAPP_bool_bool(fNot,fTrue) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_62199,c_1220]) ).
tcf(c_63573,plain,
hAPP_bool_bool(fNot,fTrue) = iPr_def_18,
inference(backward_subsumption_resolution,[status(thm)],[c_63561,c_63560]) ).
tcf(c_64004,plain,
! [X0: $i] :
( hBOOL(iPr_def_18)
| ( hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,X0),iPr_def_18) = iPr_def_18 )
| ~ hBOOL(fTrue)
| ~ hBOOL(X0) ),
inference(superposition,[status(thm)],[c_62213,c_1231]) ).
tcf(c_64005,plain,
! [X0: $i] :
( ( hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,X0),iPr_def_18) = iPr_def_18 )
| ~ hBOOL(fTrue)
| ~ hBOOL(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_64004,c_41191]) ).
tcf(c_64014,plain,
( hBOOL(iPr_def_18)
| hBOOL(fTrue) ),
inference(superposition,[status(thm)],[c_63573,c_1220]) ).
tcf(c_64016,plain,
hBOOL(fTrue),
inference(forward_subsumption_resolution,[status(thm)],[c_64014,c_41191]) ).
tcf(c_64041,plain,
! [X0: $i] :
( ( hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,X0),iPr_def_18) = iPr_def_18 )
| ~ hBOOL(X0) ),
inference(global_subsumption_just,[status(thm)],[c_64005,c_64005,c_64016]) ).
tcf(c_65422,plain,
( ( hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),iPr_def_17)),iPr_def_18) = iPr_def_18 )
| ~ hBOOL(hAPP_com_bool(wt,y)) ),
inference(superposition,[status(thm)],[c_62719,c_64041]) ).
tcf(c_69105,plain,
( hBOOL(hAPP_com_bool(wt,y))
| ( hAPP_p799580910on_com(body,pn) != some_com(y) ) ),
inference(instantiation,[status(thm)],[c_29103]) ).
tcf(c_72205,plain,
hAPP_bool_bool(hAPP_b589554111l_bool(fimplies,hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),iPr_def_17)),iPr_def_18) = iPr_def_18,
inference(global_subsumption_just,[status(thm)],[c_65422,c_1331,c_65422,c_69105]) ).
tcf(c_72212,plain,
( hBOOL(iPr_def_18)
| hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),iPr_def_17)) ),
inference(superposition,[status(thm)],[c_72205,c_1229]) ).
tcf(c_72216,plain,
hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),iPr_def_17)),
inference(forward_subsumption_resolution,[status(thm)],[c_72212,c_41191]) ).
tcf(c_97167,plain,
! [X0: $i] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),iPr_def_17))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),bot_bo1055319631e_bool)) ),
inference(superposition,[status(thm)],[c_72216,c_107]) ).
tcf(c_97171,plain,
! [X0: $i] : hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),iPr_def_17)),
inference(forward_subsumption_resolution,[status(thm)],[c_97167,c_103]) ).
tcf(c_97572,plain,
hBOOL(hAPP_f1760790145l_bool(iPr_def_15,iPr_def_17)),
inference(superposition,[status(thm)],[c_41187,c_97171]) ).
tcf(c_97581,plain,
hBOOL(iPr_def_18),
inference(light_normalisation,[status(thm)],[c_97572,c_41190]) ).
tcf(c_97582,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_97581,c_41191]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW474+2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.38 % Computer : n001.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 22:40:39 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 52.78/9.47 % SZS status Started for theBenchmark.p
% 52.78/9.47 % SZS status Theorem for theBenchmark.p
% 52.78/9.47
% 52.78/9.47 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 52.78/9.47
% 52.78/9.47 % ------ iProver source info
% 52.78/9.47
% 52.78/9.47 % git: date: 2026-07-19 20:42:38 +0200
% 52.78/9.47 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 52.78/9.47 % git: non_committed_changes: false
% 52.78/9.47
% 52.78/9.47 % ------ Parsing...
% 52.78/9.47 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 52.78/9.47
% 52.78/9.47 % ------ Preprocessing... sup_sim: 233 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 1 0s sf_e pe_s pe_e %
% 52.78/9.47
% 52.78/9.47 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 52.78/9.47
% 52.78/9.47 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 52.78/9.47 % ------ Proving...
% 52.78/9.47 % ------ Problem Properties
% 52.78/9.47
% 52.78/9.47 %
% 52.78/9.47 % clauses 978
% 52.78/9.47 % conjectures 0
% 52.78/9.47 % EPR 16
% 52.78/9.47 % Horn 725
% 52.78/9.47 % unary 275
% 52.78/9.47 % binary 315
% 52.78/9.47 % lits 2397
% 52.78/9.47 % lits eq 564
% 52.78/9.47 % fd_pure 0
% 52.78/9.47 % fd_pseudo 0
% 52.78/9.47 % fd_cond 86
% 52.78/9.47 % fd_pseudo_cond 48
% 52.78/9.47 % AC symbols 0
% 52.78/9.47
% 52.78/9.47 % ------ Schedule dynamic 5 is on
% 52.78/9.47
% 52.78/9.47 % ------ no conjectures: strip conj schedule
% 52.78/9.47
% 52.78/9.47 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 52.78/9.47
% 52.78/9.47
% 52.78/9.47 % ------
% 52.78/9.47 % Current options:
% 52.78/9.47 % ------
% 52.78/9.47
% 52.78/9.47
% 52.78/9.47 %
% 52.78/9.47
% 52.78/9.47 % ------ Proving...
% 52.78/9.47 %
% 52.78/9.47
% 52.78/9.47 % SZS status Theorem for theBenchmark.p
% 52.78/9.47
% 52.78/9.47 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 52.78/9.48
% 52.78/9.48
%------------------------------------------------------------------------------