%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SWW474+5 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n017.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:50 PM UTC 2026
% Result : Theorem 14.87s 2.70s
% Output : CNFRefutation 14.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 10
% Syntax : Number of formulae : 58 ( 28 unt; 0 def)
% Number of atoms : 111 ( 21 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 104 ( 51 ~; 46 |; 0 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 4 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 12 con; 0-4 aty)
% Number of variables : 86 ( 0 sgn 86 !; 0 ?; 38 :)
% Comments :
%------------------------------------------------------------------------------
fof(f41,axiom,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),X3))
=> ( hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),ord_less_eq(fun(hoare_509422987triple(X0),bool)),X2),X1))
=> hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X1),X3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_thin) ).
fof(f48,axiom,
! [X0,X1] : hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),bot_bot(fun(X0,bool))),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10_empty__subsetI) ).
fof(f57,axiom,
! [X0] :
( hBOOL(hoare_1883395792gleton)
=> ( hBOOL(wT_bodies)
=> ( hBOOL(hAPP(com,bool,wt,X0))
=> hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_509422987triple(state),bool))))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_19_MGF) ).
fof(f98,axiom,
! [X0,X1,X2,X3,X4,X5] : hAPP(fun(X0,bool),fun(X1,bool),hAPP(fun(X0,X1),fun(fun(X0,bool),fun(X1,bool)),image(X0,X1),X3),hAPP(fun(X2,bool),fun(X0,bool),hAPP(fun(X2,X0),fun(fun(X2,bool),fun(X0,bool)),image(X2,X0),X4),X5)) = hAPP(fun(X2,bool),fun(X1,bool),hAPP(fun(X2,X1),fun(fun(X2,bool),fun(X1,bool)),image(X2,X1),hAPP(fun(X2,X0),fun(X2,X1),hAPP(fun(X0,X1),fun(fun(X2,X0),fun(X2,X1)),combb(X0,X1,X2),X3),X4)),X5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_60_image__image) ).
fof(f128,axiom,
! [X0,X1] : hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)) = hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_90_singleton__conv2) ).
fof(f130,axiom,
! [X0,X1] :
( hBOOL(wT_bodies)
=> ( hAPP(pname,option(com),body,X0) = hAPP(com,option(com),some(com),X1)
=> hBOOL(hAPP(com,bool,wt,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_92_WT__bodiesD) ).
fof(f162,axiom,
hBOOL(hoare_1883395792gleton),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f163,axiom,
hBOOL(wT_bodies),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
fof(f167,axiom,
hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_5) ).
fof(f169,conjecture,
hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_7) ).
fof(f170,negated_conjecture,
~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool))))),
inference(negated_conjecture,[status(cth)],[f169]) ).
fof(f171,plain,
~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool))))),
inference(flattening,[],[f170]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),X3))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),ord_less_eq(fun(hoare_509422987triple(X0),bool)),X2),X1))
| hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X1),X3)) ),
inference(ennf_transformation,[],[f41]) ).
fof(f176,plain,
! [X0,X1,X2,X3] :
( ~ hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),X3))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),ord_less_eq(fun(hoare_509422987triple(X0),bool)),X2),X1))
| hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X1),X3)) ),
inference(flattening,[],[f175]) ).
fof(f194,plain,
! [X0] :
( ~ hBOOL(hoare_1883395792gleton)
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hAPP(com,bool,wt,X0))
| hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_509422987triple(state),bool))))) ),
inference(ennf_transformation,[],[f57]) ).
fof(f195,plain,
! [X0] :
( ~ hBOOL(hoare_1883395792gleton)
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hAPP(com,bool,wt,X0))
| hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_509422987triple(state),bool))))) ),
inference(flattening,[],[f194]) ).
fof(f243,plain,
! [X0,X1] :
( ~ hBOOL(wT_bodies)
| hAPP(pname,option(com),body,X0) != hAPP(com,option(com),some(com),X1)
| hBOOL(hAPP(com,bool,wt,X1)) ),
inference(ennf_transformation,[],[f130]) ).
fof(f244,plain,
! [X0,X1] :
( ~ hBOOL(wT_bodies)
| hAPP(pname,option(com),body,X0) != hAPP(com,option(com),some(com),X1)
| hBOOL(hAPP(com,bool,wt,X1)) ),
inference(flattening,[],[f243]) ).
fof(f343,plain,
! [X2,X3,X0,X1] :
( ~ hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),X3))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),ord_less_eq(fun(hoare_509422987triple(X0),bool)),X2),X1))
| hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X1),X3)) ),
inference(cnf_transformation,[],[f176]) ).
fof(f351,plain,
! [X0,X1] : hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),bot_bot(fun(X0,bool))),X1)),
inference(cnf_transformation,[],[f48]) ).
fof(f362,plain,
! [X0] :
( ~ hBOOL(hoare_1883395792gleton)
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hAPP(com,bool,wt,X0))
| hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_509422987triple(state),bool))))) ),
inference(cnf_transformation,[],[f195]) ).
fof(f420,plain,
! [X2,X3,X0,X1,X4,X5] : hAPP(fun(X0,bool),fun(X1,bool),hAPP(fun(X0,X1),fun(fun(X0,bool),fun(X1,bool)),image(X0,X1),X3),hAPP(fun(X2,bool),fun(X0,bool),hAPP(fun(X2,X0),fun(fun(X2,bool),fun(X0,bool)),image(X2,X0),X4),X5)) = hAPP(fun(X2,bool),fun(X1,bool),hAPP(fun(X2,X1),fun(fun(X2,bool),fun(X1,bool)),image(X2,X1),hAPP(fun(X2,X0),fun(X2,X1),hAPP(fun(X0,X1),fun(fun(X2,X0),fun(X2,X1)),combb(X0,X1,X2),X3),X4)),X5),
inference(cnf_transformation,[],[f98]) ).
fof(f468,plain,
! [X0,X1] : hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool))) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)),
inference(cnf_transformation,[],[f128]) ).
fof(f471,plain,
! [X0,X1] :
( ~ hBOOL(wT_bodies)
| hAPP(pname,option(com),body,X0) != hAPP(com,option(com),some(com),X1)
| hBOOL(hAPP(com,bool,wt,X1)) ),
inference(cnf_transformation,[],[f244]) ).
fof(f512,plain,
hBOOL(hoare_1883395792gleton),
inference(cnf_transformation,[],[f162]) ).
fof(f513,plain,
hBOOL(wT_bodies),
inference(cnf_transformation,[],[f163]) ).
fof(f517,plain,
hAPP(pname,option(com),body,pn) = hAPP(com,option(com),some(com),y),
inference(cnf_transformation,[],[f167]) ).
fof(f519,plain,
~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool))))),
inference(cnf_transformation,[],[f171]) ).
tcf(c_90,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X2),X3))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),hoare_122391849derivs(X0),X1),X3))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(X0),bool),bool,hAPP(fun(hoare_509422987triple(X0),bool),fun(fun(hoare_509422987triple(X0),bool),bool),ord_less_eq(fun(hoare_509422987triple(X0),bool)),X1),X2)) ),
inference(cnf_transformation,[],[f343]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i] : hBOOL(hAPP(fun(X0,bool),bool,hAPP(fun(X0,bool),fun(fun(X0,bool),bool),ord_less_eq(fun(X0,bool)),bot_bot(fun(X0,bool))),X1)),
inference(cnf_transformation,[],[f351]) ).
tcf(c_109,plain,
! [X0: $i] :
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_509422987triple(state),bool)))))
| ~ hBOOL(hoare_1883395792gleton)
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hAPP(com,bool,wt,X0)) ),
inference(cnf_transformation,[],[f362]) ).
tcf(c_167,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : hAPP(fun(X0,bool),fun(X1,bool),hAPP(fun(X0,X1),fun(fun(X0,bool),fun(X1,bool)),image(X0,X1),hAPP(fun(X0,X2),fun(X0,X1),hAPP(fun(X2,X1),fun(fun(X0,X2),fun(X0,X1)),combb(X2,X1,X0),X3),X4)),X5) = hAPP(fun(X2,bool),fun(X1,bool),hAPP(fun(X2,X1),fun(fun(X2,bool),fun(X1,bool)),image(X2,X1),X3),hAPP(fun(X0,bool),fun(X2,bool),hAPP(fun(X0,X2),fun(fun(X0,bool),fun(X2,bool)),image(X0,X2),X4),X5)),
inference(cnf_transformation,[],[f420]) ).
tcf(c_215,plain,
! [X0: $i,X1: $i] : hAPP(fun(X0,bool),fun(X0,bool),hAPP(X0,fun(fun(X0,bool),fun(X0,bool)),insert(X0),X1),bot_bot(fun(X0,bool))) = hAPP(fun(X0,bool),fun(X0,bool),collect(X0),hAPP(X0,fun(X0,bool),fequal(X0),X1)),
inference(cnf_transformation,[],[f468]) ).
tcf(c_218,plain,
! [X0: $i,X1: $i] :
( hBOOL(hAPP(com,bool,wt,X0))
| ~ hBOOL(wT_bodies)
| ( hAPP(com,option(com),some(com),X0) != hAPP(pname,option(com),body,X1) ) ),
inference(cnf_transformation,[],[f471]) ).
tcf(c_258,plain,
hBOOL(hoare_1883395792gleton),
inference(cnf_transformation,[],[f512]) ).
tcf(c_259,plain,
hBOOL(wT_bodies),
inference(cnf_transformation,[],[f513]) ).
tcf(c_263,plain,
hAPP(com,option(com),some(com),y) = hAPP(pname,option(com),body,pn),
inference(cnf_transformation,[],[f517]) ).
tcf(c_265,negated_conjecture,
~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(pname,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(pname,hoare_509422987triple(state)),fun(fun(pname,bool),fun(hoare_509422987triple(state),bool)),image(pname,hoare_509422987triple(state)),hAPP(fun(pname,com),fun(pname,hoare_509422987triple(state)),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(pname,com),fun(pname,hoare_509422987triple(state))),combb(com,hoare_509422987triple(state),pname),hoare_Mirabelle_MGT),body_1)),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)),bot_bot(fun(hoare_509422987triple(state),bool))))),
inference(cnf_transformation,[],[f519]) ).
tcf(c_404,plain,
! [X0: $i,X1: $i] :
( hBOOL(hAPP(com,bool,wt,X0))
| ( hAPP(com,option(com),some(com),X0) != hAPP(pname,option(com),body,X1) ) ),
inference(global_subsumption_just,[status(thm)],[c_218,c_259,c_218]) ).
tcf(c_407,plain,
! [X0: $i] :
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_509422987triple(state),bool)))))
| ~ hBOOL(hAPP(com,bool,wt,X0)) ),
inference(global_subsumption_just,[status(thm)],[c_109,c_259,c_258,c_109]) ).
tcf(c_508,plain,
! [X0: $i] :
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),hAPP(hoare_509422987triple(state),fun(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool)),insert(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)),bot_bot(fun(hoare_509422987triple(state),bool)))))
| ~ hBOOL(hAPP(com,bool,wt,X0)) ),
inference(prop_impl_just,[status(thm)],[c_407]) ).
tcf(c_1719,plain,
! [X0: $i] :
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),collect(hoare_509422987triple(state)),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)))))
| ~ hBOOL(hAPP(com,bool,wt,X0)) ),
inference(demodulation,[status(thm)],[c_508,c_215]) ).
tcf(c_1744,plain,
~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(com,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(com,bool),fun(hoare_509422987triple(state),bool)),image(com,hoare_509422987triple(state)),hoare_Mirabelle_MGT),hAPP(fun(pname,bool),fun(com,bool),hAPP(fun(pname,com),fun(fun(pname,bool),fun(com,bool)),image(pname,com),body_1),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body)))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),collect(hoare_509422987triple(state)),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y))))),
inference(demodulation,[status(thm)],[c_265,c_167,c_215]) ).
tcf(c_1881,plain,
! [X0: $i] :
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),collect(hoare_509422987triple(state)),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0)))))
| ~ hBOOL(hAPP(com,bool,wt,X0)) ),
inference(prop_impl_just,[status(thm)],[c_1719]) ).
tcf(c_1883,plain,
! [X0: $i,X1: $i] :
( ( hAPP(com,option(com),some(com),X0) != hAPP(pname,option(com),body,X1) )
| hBOOL(hAPP(com,bool,wt,X0)) ),
inference(prop_impl_just,[status(thm)],[c_404]) ).
tcf(c_1884,plain,
! [X0: $i,X1: $i] :
( hBOOL(hAPP(com,bool,wt,X0))
| ( hAPP(com,option(com),some(com),X0) != hAPP(pname,option(com),body,X1) ) ),
inference(renaming,[status(thm)],[c_1883]) ).
tcf(c_3121,plain,
! [X0_iProver_hBOOL_1: iProver_hBOOL_1] :
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),collect(hoare_509422987triple(state)),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,X0_iProver_hBOOL_1)))))
| ~ hBOOL(hAPP(com,bool,wt,X0_iProver_hBOOL_1)) ),
inference(subtyping,[status(esa)],[c_1881]) ).
tcf(c_3140,plain,
! [X0_iProver_hBOOL_1: iProver_hBOOL_1,X1_iProver_hBOOL_1: iProver_hBOOL_1] :
( hBOOL(hAPP(com,bool,wt,X0_iProver_hBOOL_1))
| ( hAPP(com,option(com),some(com),X0_iProver_hBOOL_1) != hAPP(pname,option(com),body,X1_iProver_hBOOL_1) ) ),
inference(subtyping,[status(esa)],[c_1884]) ).
tcf(c_3142,plain,
hAPP(com,option(com),some(com),y) = hAPP(pname,option(com),body,pn),
inference(subtyping,[status(esa)],[c_263]) ).
tcf(c_3235,plain,
! [X0_iProver_hBOOL_1: iProver_hBOOL_1,X0_iProver_hAPP_2: iProver_hAPP_2] : hBOOL(hAPP(fun(X0_iProver_hAPP_2,bool),bool,hAPP(fun(X0_iProver_hAPP_2,bool),fun(fun(X0_iProver_hAPP_2,bool),bool),ord_less_eq(fun(X0_iProver_hAPP_2,bool)),bot_bot(fun(X0_iProver_hAPP_2,bool))),X0_iProver_hBOOL_1)),
inference(subtyping,[status(esa)],[c_98]) ).
tcf(c_3240,plain,
! [X0_iProver_hBOOL_1: iProver_hBOOL_1,X0_iProver_hoare_509422987triple_1: iProver_hoare_509422987triple_1,X1_iProver_hBOOL_1: iProver_hBOOL_1,X2_iProver_hBOOL_1: iProver_hBOOL_1] :
( hBOOL(hAPP(fun(hoare_509422987triple(X0_iProver_hoare_509422987triple_1),bool),bool,hAPP(fun(hoare_509422987triple(X0_iProver_hoare_509422987triple_1),bool),fun(fun(hoare_509422987triple(X0_iProver_hoare_509422987triple_1),bool),bool),hoare_122391849derivs(X0_iProver_hoare_509422987triple_1),X1_iProver_hBOOL_1),X2_iProver_hBOOL_1))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(X0_iProver_hoare_509422987triple_1),bool),bool,hAPP(fun(hoare_509422987triple(X0_iProver_hoare_509422987triple_1),bool),fun(fun(hoare_509422987triple(X0_iProver_hoare_509422987triple_1),bool),bool),hoare_122391849derivs(X0_iProver_hoare_509422987triple_1),X0_iProver_hBOOL_1),X2_iProver_hBOOL_1))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(X0_iProver_hoare_509422987triple_1),bool),bool,hAPP(fun(hoare_509422987triple(X0_iProver_hoare_509422987triple_1),bool),fun(fun(hoare_509422987triple(X0_iProver_hoare_509422987triple_1),bool),bool),ord_less_eq(fun(hoare_509422987triple(X0_iProver_hoare_509422987triple_1),bool)),X0_iProver_hBOOL_1),X1_iProver_hBOOL_1)) ),
inference(subtyping,[status(esa)],[c_90]) ).
tcf(c_6029,plain,
! [X0_iProver_hBOOL_1: iProver_hBOOL_1] :
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(com,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(com,bool),fun(hoare_509422987triple(state),bool)),image(com,hoare_509422987triple(state)),hoare_Mirabelle_MGT),hAPP(fun(pname,bool),fun(com,bool),hAPP(fun(pname,com),fun(fun(pname,bool),fun(com,bool)),image(pname,com),body_1),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body)))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),collect(hoare_509422987triple(state)),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)))))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),X0_iProver_hBOOL_1),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),collect(hoare_509422987triple(state)),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)))))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),ord_less_eq(fun(hoare_509422987triple(state),bool)),X0_iProver_hBOOL_1),hAPP(fun(com,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(com,bool),fun(hoare_509422987triple(state),bool)),image(com,hoare_509422987triple(state)),hoare_Mirabelle_MGT),hAPP(fun(pname,bool),fun(com,bool),hAPP(fun(pname,com),fun(fun(pname,bool),fun(com,bool)),image(pname,com),body_1),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))))) ),
inference(instantiation,[status(thm)],[c_3240]) ).
tcf(c_6034,plain,
! [X0_iProver_hBOOL_1: iProver_hBOOL_1] :
( hBOOL(hAPP(com,bool,wt,y))
| ( hAPP(com,option(com),some(com),y) != hAPP(pname,option(com),body,X0_iProver_hBOOL_1) ) ),
inference(instantiation,[status(thm)],[c_3140]) ).
tcf(c_6446,plain,
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),hAPP(fun(com,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(com,bool),fun(hoare_509422987triple(state),bool)),image(com,hoare_509422987triple(state)),hoare_Mirabelle_MGT),hAPP(fun(pname,bool),fun(com,bool),hAPP(fun(pname,com),fun(fun(pname,bool),fun(com,bool)),image(pname,com),body_1),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body)))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),collect(hoare_509422987triple(state)),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)))))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),collect(hoare_509422987triple(state)),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)))))
| ~ hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),ord_less_eq(fun(hoare_509422987triple(state),bool)),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(com,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(com,bool),fun(hoare_509422987triple(state),bool)),image(com,hoare_509422987triple(state)),hoare_Mirabelle_MGT),hAPP(fun(pname,bool),fun(com,bool),hAPP(fun(pname,com),fun(fun(pname,bool),fun(com,bool)),image(pname,com),body_1),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))))) ),
inference(instantiation,[status(thm)],[c_6029]) ).
tcf(c_6611,plain,
( hBOOL(hAPP(com,bool,wt,y))
| ( hAPP(com,option(com),some(com),y) != hAPP(pname,option(com),body,pn) ) ),
inference(instantiation,[status(thm)],[c_6034]) ).
tcf(c_6665,plain,
( hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),hoare_122391849derivs(state),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(hoare_509422987triple(state),bool),fun(hoare_509422987triple(state),bool),collect(hoare_509422987triple(state)),hAPP(hoare_509422987triple(state),fun(hoare_509422987triple(state),bool),fequal(hoare_509422987triple(state)),hAPP(com,hoare_509422987triple(state),hoare_Mirabelle_MGT,y)))))
| ~ hBOOL(hAPP(com,bool,wt,y)) ),
inference(instantiation,[status(thm)],[c_3121]) ).
tcf(c_7056,plain,
hBOOL(hAPP(fun(hoare_509422987triple(state),bool),bool,hAPP(fun(hoare_509422987triple(state),bool),fun(fun(hoare_509422987triple(state),bool),bool),ord_less_eq(fun(hoare_509422987triple(state),bool)),bot_bot(fun(hoare_509422987triple(state),bool))),hAPP(fun(com,bool),fun(hoare_509422987triple(state),bool),hAPP(fun(com,hoare_509422987triple(state)),fun(fun(com,bool),fun(hoare_509422987triple(state),bool)),image(com,hoare_509422987triple(state)),hoare_Mirabelle_MGT),hAPP(fun(pname,bool),fun(com,bool),hAPP(fun(pname,com),fun(fun(pname,bool),fun(com,bool)),image(pname,com),body_1),hAPP(fun(pname,option(com)),fun(pname,bool),dom(pname,com),body))))),
inference(instantiation,[status(thm)],[c_3235]) ).
tcf(c_7057,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_7056,c_6665,c_6611,c_6446,c_3142,c_1744]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW474+5 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 22:31:18 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.41
% 0.09/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.41
% 0.09/0.41 % Detected problem language: tptp
% 0.09/0.42 % Proving...
% 14.87/2.70 % SZS status Started for theBenchmark.p
% 14.87/2.70 % SZS status Theorem for theBenchmark.p
% 14.87/2.70
% 14.87/2.70 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 14.87/2.70
% 14.87/2.70 % ------ iProver source info
% 14.87/2.70
% 14.87/2.70 % git: date: 2026-07-19 20:42:38 +0200
% 14.87/2.70 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 14.87/2.70 % git: non_committed_changes: false
% 14.87/2.70
% 14.87/2.70 % ------ Parsing...
% 14.87/2.70 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 14.87/2.70
% 14.87/2.70 % ------ Preprocessing... sup_sim: 35 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 %
% 14.87/2.70
% 14.87/2.70 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 14.87/2.70
% 14.87/2.70 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 14.87/2.70 % ------ Proving...
% 14.87/2.70 % ------ Problem Properties
% 14.87/2.70
% 14.87/2.70 %
% 14.87/2.70 % clauses 188
% 14.87/2.70 % conjectures 0
% 14.87/2.70 % EPR 4
% 14.87/2.70 % Horn 162
% 14.87/2.70 % unary 71
% 14.87/2.70 % binary 78
% 14.87/2.70 % lits 355
% 14.87/2.70 % lits eq 113
% 14.87/2.70 % fd_pure 0
% 14.87/2.70 % fd_pseudo 0
% 14.87/2.70 % fd_cond 0
% 14.87/2.70 % fd_pseudo_cond 0
% 14.87/2.70 % AC symbols 0
% 14.87/2.70
% 14.87/2.70 % ------ Input Options Time Limit: Unbounded
% 14.87/2.70
% 14.87/2.70
% 14.87/2.70 % ------
% 14.87/2.70 % Current options:
% 14.87/2.70 % ------
% 14.87/2.70
% 14.87/2.70
% 14.87/2.70 %
% 14.87/2.70
% 14.87/2.70 % ------ Proving...
% 14.87/2.70 %
% 14.87/2.70
% 14.87/2.70 % SZS status Theorem for theBenchmark.p
% 14.87/2.70
% 14.87/2.70 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 14.87/2.70
% 14.87/2.70
%------------------------------------------------------------------------------