%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW474+2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 : Thu Sep 24 03:07:59 PM UTC 2026
% Result : Theorem 42.30s 5.91s
% Output : CNFRefutation 43.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 23
% Syntax : Number of formulae : 103 ( 48 unt; 0 def)
% Number of atoms : 192 ( 60 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 152 ( 63 ~; 75 |; 2 &)
% ( 1 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 36 ( 36 usr; 17 con; 0-2 aty)
% Number of variables : 85 ( 85 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,hypothesis,
is_bool(wT_bodies),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,hypothesis,
is_bool(hoare_298929751gleton),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
is_bool(bot_bot_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
is_bool(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [B_1_1,B_2_1] : is_bool(hAPP_com_bool(B_1_1,B_2_1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,hypothesis,
! [B_1_1,B_2_1] : is_bool(hAPP_f1760790145l_bool(B_1_1,B_2_1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,axiom,
! [G_1,G_2,Ts] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(G_2),Ts))
=> ( hBOOL(hAPP_f1760790145l_bool(hAPP_f854625363l_bool(ord_le1720872323e_bool,G_2),G_1))
=> hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(G_1),Ts)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,axiom,
! [A_1] : hBOOL(hAPP_f1760790145l_bool(hAPP_f854625363l_bool(ord_le1720872323e_bool,bot_bo1055319631e_bool),A_1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f105,axiom,
! [B,F,A_1] :
( hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,A_1))
=> ( hBOOL(hAPP_f1760790145l_bool(hAPP_f854625363l_bool(ord_le1720872323e_bool,B),hAPP_f631639356e_bool(image_275883510_state(F),A_1)))
=> hBOOL(hAPP_f1760790145l_bool(finite784854244_state,B)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f108,axiom,
! [C] :
( hBOOL(hoare_298929751gleton)
=> ( hBOOL(wT_bodies)
=> ( hBOOL(hAPP_com_bool(wt,C))
=> hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,C)),bot_bo1055319631e_bool))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f140,axiom,
bot_bo1055319631e_bool = hAPP_f921536533e_bool(collec727977250_state,cOMBK_1079618832_state(fFalse)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f232,axiom,
! [P_1] : hAPP_f921536533e_bool(collec727977250_state,P_1) = P_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f270,axiom,
! [Pn,B_4] :
( hBOOL(wT_bodies)
=> ( hAPP_p799580910on_com(body,Pn) = some_com(B_4)
=> hBOOL(hAPP_com_bool(wt,B_4)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f291,axiom,
hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,dom_pname_com(body))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f429,axiom,
! [X_1] :
( hBOOL(hAPP_H513860823e_bool(bot_bo1055319631e_bool,X_1))
<=> hBOOL(bot_bot_bool) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f458,axiom,
! [X_1] : set_Ho1831989999_state(some_H1133819688_state(X_1)) = hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X_1),bot_bo1055319631e_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f762,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f763,axiom,
! [P] :
( is_bool(P)
=> ( P = fFalse
| P = fTrue ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f803,axiom,
! [P,Q] :
( is_bool(P)
=> hAPP_H513860823e_bool(cOMBK_1079618832_state(P),Q) = P ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f861,hypothesis,
hBOOL(hoare_298929751gleton),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f862,hypothesis,
hBOOL(wT_bodies),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f866,hypothesis,
hAPP_p799580910on_com(body,pn) = some_com(y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
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') ).
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(f874,plain,
is_bool(wT_bodies),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f887,plain,
is_bool(hoare_298929751gleton),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f893,plain,
is_bool(bot_bot_bool),
inference(cnf_transformation,[status(thm)],[f20]) ).
fof(f896,plain,
is_bool(fFalse),
inference(cnf_transformation,[status(thm)],[f23]) ).
fof(f898,plain,
! [X0,X1] : is_bool(hAPP_com_bool(X0,X1)),
inference(cnf_transformation,[status(thm)],[f25]) ).
fof(f933,plain,
! [X0,X1] : is_bool(hAPP_f1760790145l_bool(X0,X1)),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f956,plain,
! [G_1,G_2,Ts] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(G_1),Ts))
| ~ hBOOL(hAPP_f1760790145l_bool(hAPP_f854625363l_bool(ord_le1720872323e_bool,G_2),G_1))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(G_2),Ts)) ),
inference(pre_NNF_transformation,[status(thm)],[f58]) ).
fof(f957,plain,
! [G_2,Ts] :
( ! [G_1] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(G_1),Ts))
| ~ hBOOL(hAPP_f1760790145l_bool(hAPP_f854625363l_bool(ord_le1720872323e_bool,G_2),G_1)) )
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(G_2),Ts)) ),
inference(miniscoping,[status(thm)],[f956]) ).
fof(f958,plain,
! [X0,X1,X2] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X2),X1))
| ~ hBOOL(hAPP_f1760790145l_bool(hAPP_f854625363l_bool(ord_le1720872323e_bool,X0),X2))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f957]) ).
fof(f1006,plain,
! [X0] : hBOOL(hAPP_f1760790145l_bool(hAPP_f854625363l_bool(ord_le1720872323e_bool,bot_bo1055319631e_bool),X0)),
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f1082,plain,
! [B,F,A_1] :
( hBOOL(hAPP_f1760790145l_bool(finite784854244_state,B))
| ~ hBOOL(hAPP_f1760790145l_bool(hAPP_f854625363l_bool(ord_le1720872323e_bool,B),hAPP_f631639356e_bool(image_275883510_state(F),A_1)))
| ~ hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,A_1)) ),
inference(pre_NNF_transformation,[status(thm)],[f105]) ).
fof(f1083,plain,
! [A_1] :
( ! [B] :
( hBOOL(hAPP_f1760790145l_bool(finite784854244_state,B))
| ! [F] : ~ hBOOL(hAPP_f1760790145l_bool(hAPP_f854625363l_bool(ord_le1720872323e_bool,B),hAPP_f631639356e_bool(image_275883510_state(F),A_1))) )
| ~ hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,A_1)) ),
inference(miniscoping,[status(thm)],[f1082]) ).
fof(f1084,plain,
! [X0,X1,X2] :
( hBOOL(hAPP_f1760790145l_bool(finite784854244_state,X1))
| ~ hBOOL(hAPP_f1760790145l_bool(hAPP_f854625363l_bool(ord_le1720872323e_bool,X1),hAPP_f631639356e_bool(image_275883510_state(X2),X0)))
| ~ hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,X0)) ),
inference(cnf_transformation,[status(thm)],[f1083]) ).
fof(f1090,plain,
! [C] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,C)),bot_bo1055319631e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,C))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_298929751gleton) ),
inference(pre_NNF_transformation,[status(thm)],[f108]) ).
fof(f1091,plain,
( ! [C] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,hAPP_c1546227244_state(hoare_Mirabelle_MGT,C)),bot_bo1055319631e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,C)) )
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_298929751gleton) ),
inference(miniscoping,[status(thm)],[f1090]) ).
fof(f1092,plain,
! [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)))
| ~ hBOOL(hAPP_com_bool(wt,X0))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_298929751gleton) ),
inference(cnf_transformation,[status(thm)],[f1091]) ).
fof(f1203,plain,
bot_bo1055319631e_bool = hAPP_f921536533e_bool(collec727977250_state,cOMBK_1079618832_state(fFalse)),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f1468,plain,
! [X0] : hAPP_f921536533e_bool(collec727977250_state,X0) = X0,
inference(cnf_transformation,[status(thm)],[f232]) ).
fof(f1579,plain,
! [Pn,B_4] :
( hBOOL(hAPP_com_bool(wt,B_4))
| hAPP_p799580910on_com(body,Pn) != some_com(B_4)
| ~ hBOOL(wT_bodies) ),
inference(pre_NNF_transformation,[status(thm)],[f270]) ).
fof(f1580,plain,
( ! [B_4] :
( hBOOL(hAPP_com_bool(wt,B_4))
| ! [Pn] : hAPP_p799580910on_com(body,Pn) != some_com(B_4) )
| ~ hBOOL(wT_bodies) ),
inference(miniscoping,[status(thm)],[f1579]) ).
fof(f1581,plain,
! [X0,X1] :
( hBOOL(hAPP_com_bool(wt,X1))
| hAPP_p799580910on_com(body,X0) != some_com(X1)
| ~ hBOOL(wT_bodies) ),
inference(cnf_transformation,[status(thm)],[f1580]) ).
fof(f1712,plain,
hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,dom_pname_com(body))),
inference(cnf_transformation,[status(thm)],[f291]) ).
fof(f2170,plain,
! [X_1] :
( ( ~ hBOOL(bot_bot_bool)
| hBOOL(hAPP_H513860823e_bool(bot_bo1055319631e_bool,X_1)) )
& ( hBOOL(bot_bot_bool)
| ~ hBOOL(hAPP_H513860823e_bool(bot_bo1055319631e_bool,X_1)) ) ),
inference(NNF_transformation,[status(thm)],[f429]) ).
fof(f2171,plain,
( ( ~ hBOOL(bot_bot_bool)
| ! [X_1] : hBOOL(hAPP_H513860823e_bool(bot_bo1055319631e_bool,X_1)) )
& ( hBOOL(bot_bot_bool)
| ! [X_1] : ~ hBOOL(hAPP_H513860823e_bool(bot_bo1055319631e_bool,X_1)) ) ),
inference(miniscoping,[status(thm)],[f2170]) ).
fof(f2173,plain,
! [X0] :
( ~ hBOOL(bot_bot_bool)
| hBOOL(hAPP_H513860823e_bool(bot_bo1055319631e_bool,X0)) ),
inference(cnf_transformation,[status(thm)],[f2171]) ).
fof(f2272,plain,
! [X0] : set_Ho1831989999_state(some_H1133819688_state(X0)) = hAPP_f921536533e_bool(hAPP_H727730819e_bool(insert1835143293_state,X0),bot_bo1055319631e_bool),
inference(cnf_transformation,[status(thm)],[f458]) ).
fof(f3136,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[status(thm)],[f762]) ).
fof(f3137,plain,
! [P] :
( P = fFalse
| P = fTrue
| ~ is_bool(P) ),
inference(pre_NNF_transformation,[status(thm)],[f763]) ).
fof(f3138,plain,
! [X0] :
( X0 = fFalse
| X0 = fTrue
| ~ is_bool(X0) ),
inference(cnf_transformation,[status(thm)],[f3137]) ).
fof(f3190,plain,
! [P,Q] :
( hAPP_H513860823e_bool(cOMBK_1079618832_state(P),Q) = P
| ~ is_bool(P) ),
inference(pre_NNF_transformation,[status(thm)],[f803]) ).
fof(f3191,plain,
! [P] :
( ! [Q] : hAPP_H513860823e_bool(cOMBK_1079618832_state(P),Q) = P
| ~ is_bool(P) ),
inference(miniscoping,[status(thm)],[f3190]) ).
fof(f3192,plain,
! [X0,X1] :
( hAPP_H513860823e_bool(cOMBK_1079618832_state(X0),X1) = X0
| ~ is_bool(X0) ),
inference(cnf_transformation,[status(thm)],[f3191]) ).
fof(f3254,plain,
hBOOL(hoare_298929751gleton),
inference(cnf_transformation,[status(thm)],[f861]) ).
fof(f3255,plain,
hBOOL(wT_bodies),
inference(cnf_transformation,[status(thm)],[f862]) ).
fof(f3259,plain,
hAPP_p799580910on_com(body,pn) = some_com(y),
inference(cnf_transformation,[status(thm)],[f866]) ).
fof(f3261,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,[status(thm)],[f869]) ).
fof(f3395,plain,
! [X0,X1] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),X0))
| ~ hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),X0)) ),
inference(resolution,[status(thm)],[f958,f1006]) ).
fof(f3463,plain,
! [X0] :
( hBOOL(hAPP_f1760790145l_bool(finite784854244_state,bot_bo1055319631e_bool))
| ~ hBOOL(hAPP_f1664156314l_bool(finite_finite_pname,X0)) ),
inference(resolution,[status(thm)],[f1084,f1006]) ).
fof(f3469,plain,
hBOOL(hAPP_f1760790145l_bool(finite784854244_state,bot_bo1055319631e_bool)),
inference(resolution,[status(thm)],[f3463,f1712]) ).
fof(f3839,plain,
! [X0,X1] :
( hAPP_f1760790145l_bool(X0,X1) = fFalse
| hAPP_f1760790145l_bool(X0,X1) = fTrue ),
inference(resolution,[status(thm)],[f3138,f933]) ).
fof(f3844,plain,
! [X0,X1] :
( hAPP_com_bool(X0,X1) = fFalse
| hAPP_com_bool(X0,X1) = fTrue ),
inference(resolution,[status(thm)],[f3138,f898]) ).
fof(f3855,plain,
( bot_bot_bool = fFalse
| bot_bot_bool = fTrue ),
inference(resolution,[status(thm)],[f3138,f893]) ).
fof(f3856,plain,
( hoare_298929751gleton = fFalse
| hoare_298929751gleton = fTrue ),
inference(resolution,[status(thm)],[f3138,f887]) ).
fof(f3857,plain,
( wT_bodies = fFalse
| wT_bodies = fTrue ),
inference(resolution,[status(thm)],[f3138,f874]) ).
fof(f4328,plain,
bot_bo1055319631e_bool = cOMBK_1079618832_state(fFalse),
inference(forward_demodulation,[status(thm)],[f1468,f1203]) ).
fof(f4906,plain,
! [X0] :
( hAPP_H513860823e_bool(bot_bo1055319631e_bool,X0) = fFalse
| ~ is_bool(fFalse) ),
inference(paramodulation,[status(thm)],[f4328,f3192]) ).
fof(f4907,plain,
! [X0] : hAPP_H513860823e_bool(bot_bo1055319631e_bool,X0) = fFalse,
inference(forward_subsumption_resolution,[status(thm)],[f4906,f896]) ).
fof(f5021,plain,
( ~ hBOOL(bot_bot_bool)
| hBOOL(fFalse) ),
inference(forward_demodulation,[status(thm)],[f4907,f2173]) ).
fof(f5023,plain,
~ hBOOL(bot_bot_bool),
inference(forward_subsumption_resolution,[status(thm)],[f5021,f3136]) ).
fof(f5683,plain,
( hAPP_f1760790145l_bool(finite784854244_state,bot_bo1055319631e_bool) = fFalse
| hBOOL(fTrue) ),
inference(paramodulation,[status(thm)],[f3839,f3469]) ).
fof(f5769,plain,
( 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)) = fFalse
| ~ hBOOL(fTrue) ),
inference(paramodulation,[status(thm)],[f3839,f3261]) ).
fof(f5805,plain,
( hBOOL(fTrue)
| hBOOL(fFalse) ),
inference(paramodulation,[status(thm)],[f5683,f3469]) ).
fof(f5808,plain,
hBOOL(fTrue),
inference(forward_subsumption_resolution,[status(thm)],[f5805,f3136]) ).
fof(f5809,plain,
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)) = fFalse,
inference(backward_subsumption_resolution,[status(thm)],[f5769,f5808]) ).
fof(f5812,plain,
( bot_bot_bool = fFalse
| hBOOL(bot_bot_bool) ),
inference(paramodulation,[status(thm)],[f3855,f5808]) ).
fof(f5813,plain,
bot_bot_bool = fFalse,
inference(forward_subsumption_resolution,[status(thm)],[f5812,f5023]) ).
fof(f5829,plain,
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)) = bot_bot_bool,
inference(backward_demodulation,[status(thm)],[f5813,f5809]) ).
fof(f5843,plain,
( wT_bodies = bot_bot_bool
| wT_bodies = fTrue ),
inference(backward_demodulation,[status(thm)],[f5813,f3857]) ).
fof(f5844,plain,
( hoare_298929751gleton = bot_bot_bool
| hoare_298929751gleton = fTrue ),
inference(backward_demodulation,[status(thm)],[f5813,f3856]) ).
fof(f5872,plain,
( wT_bodies = bot_bot_bool
| hoare_298929751gleton = bot_bot_bool
| hoare_298929751gleton = wT_bodies ),
inference(paramodulation,[status(thm)],[f5843,f5844]) ).
fof(f5971,plain,
! [X0,X1] :
( hAPP_com_bool(X0,X1) = bot_bot_bool
| hAPP_com_bool(X0,X1) = fTrue ),
inference(forward_demodulation,[status(thm)],[f5813,f3844]) ).
fof(f6215,plain,
( wT_bodies = bot_bot_bool
| hoare_298929751gleton = wT_bodies
| ~ hBOOL(hoare_298929751gleton) ),
inference(paramodulation,[status(thm)],[f5872,f5023]) ).
fof(f6218,plain,
( wT_bodies = bot_bot_bool
| hoare_298929751gleton = wT_bodies ),
inference(forward_subsumption_resolution,[status(thm)],[f6215,f3254]) ).
fof(f6223,plain,
( hoare_298929751gleton = wT_bodies
| ~ hBOOL(wT_bodies) ),
inference(paramodulation,[status(thm)],[f6218,f5023]) ).
fof(f6225,plain,
hoare_298929751gleton = wT_bodies,
inference(forward_subsumption_resolution,[status(thm)],[f6223,f3255]) ).
fof(f6932,plain,
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))),set_Ho1831989999_state(some_H1133819688_state(hAPP_c1546227244_state(hoare_Mirabelle_MGT,y)))) = bot_bot_bool,
inference(backward_demodulation,[status(thm)],[f2272,f5829]) ).
fof(f7816,plain,
! [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)))
| ~ hBOOL(hAPP_com_bool(wt,X0))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(wT_bodies) ),
inference(forward_demodulation,[status(thm)],[f6225,f1092]) ).
fof(f7817,plain,
! [X0] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),set_Ho1831989999_state(some_H1133819688_state(hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)))))
| ~ hBOOL(hAPP_com_bool(wt,X0))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(wT_bodies) ),
inference(forward_demodulation,[status(thm)],[f2272,f7816]) ).
fof(f7818,plain,
! [X0] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),set_Ho1831989999_state(some_H1133819688_state(hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)))))
| ~ hBOOL(hAPP_com_bool(wt,X0))
| ~ hBOOL(wT_bodies) ),
inference(duplicate_literals_removal,[status(thm)],[f7817]) ).
fof(f7819,plain,
! [X0] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(bot_bo1055319631e_bool),set_Ho1831989999_state(some_H1133819688_state(hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)))))
| ~ hBOOL(hAPP_com_bool(wt,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f7818,f3255]) ).
fof(f7820,plain,
! [X0,X1] :
( hBOOL(hAPP_f1760790145l_bool(hoare_659004819_state(X1),set_Ho1831989999_state(some_H1133819688_state(hAPP_c1546227244_state(hoare_Mirabelle_MGT,X0)))))
| ~ hBOOL(hAPP_com_bool(wt,X0)) ),
inference(resolution,[status(thm)],[f7819,f3395]) ).
fof(f7852,plain,
( hBOOL(bot_bot_bool)
| ~ hBOOL(hAPP_com_bool(wt,y)) ),
inference(paramodulation,[status(thm)],[f6932,f7820]) ).
fof(f7856,plain,
~ hBOOL(hAPP_com_bool(wt,y)),
inference(forward_subsumption_resolution,[status(thm)],[f7852,f5023]) ).
fof(f7857,plain,
( hAPP_com_bool(wt,y) = bot_bot_bool
| ~ hBOOL(fTrue) ),
inference(paramodulation,[status(thm)],[f5971,f7856]) ).
fof(f7858,plain,
hAPP_com_bool(wt,y) = bot_bot_bool,
inference(forward_subsumption_resolution,[status(thm)],[f7857,f5808]) ).
fof(f28576,plain,
! [X0,X1] :
( hBOOL(hAPP_com_bool(wt,X1))
| hAPP_p799580910on_com(body,X0) != some_com(X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1581,f3255]) ).
fof(f28577,plain,
hBOOL(hAPP_com_bool(wt,y)),
inference(resolution,[status(thm)],[f28576,f3259]) ).
fof(f28579,plain,
hBOOL(bot_bot_bool),
inference(forward_demodulation,[status(thm)],[f7858,f28577]) ).
fof(f28580,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f28579,f5023]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW474+2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.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 : Mon Sep 21 10:03:23 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.44 % Drodi V4.1.1
% 42.30/5.91 % Refutation found
% 42.30/5.91 % SZS status Theorem for theBenchmark: Theorem is valid
% 42.30/5.91 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.32/6.06 % Elapsed time: 5.684509 seconds
% 4.32/6.06 % CPU time: 43.865625 seconds
% 4.32/6.06 % Total memory used: 523.953 MB
% 4.32/6.06 % Net memory used: 492.164 MB
%------------------------------------------------------------------------------