%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW474+3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:08:00 PM UTC 2026
% Result : Theorem 192.37s 25.02s
% Output : CNFRefutation 130.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 20
% Syntax : Number of formulae : 85 ( 39 unt; 0 def)
% Number of atoms : 160 ( 49 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 129 ( 54 ~; 60 |; 4 &)
% ( 2 <=>; 9 =>; 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 : 35 ( 35 usr; 18 con; 0-2 aty)
% Number of variables : 79 ( 79 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f30,axiom,
! [B_1_1] : is_bool(is_none_com(B_1_1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
is_bool(bot_bot_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
is_bool(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,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(f72,hypothesis,
! [B_1_1,B_2_1] : is_bool(hAPP_f1378282496l_bool(B_1_1,B_2_1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
! [G_2,G_3,Ts] :
( hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(G_3),Ts))
=> ( hBOOL(hAPP_f1378282496l_bool(hAPP_f849457489l_bool(ord_le1449778818e_bool,G_3),G_2))
=> hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(G_2),Ts)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f106,axiom,
! [A] : hBOOL(hAPP_f1378282496l_bool(hAPP_f849457489l_bool(ord_le1449778818e_bool,bot_bo784226126e_bool),A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f149,axiom,
! [C] :
( hBOOL(hoare_1795711768gleton)
=> ( hBOOL(wT_bodies)
=> ( hBOOL(hAPP_com_bool(wt,C))
=> hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(bot_bo784226126e_bool),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,C)),bot_bo784226126e_bool))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f195,axiom,
bot_bo784226126e_bool = hAPP_f806699093e_bool(collec637225377_state,hAPP_b974863576e_bool(cOMBK_988866959_state,fFalse)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f323,axiom,
! [P_1] : hAPP_f806699093e_bool(collec637225377_state,P_1) = P_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f380,axiom,
! [Pn,B_4] :
( hBOOL(wT_bodies)
=> ( hAPP_p799580910on_com(body,Pn) = hAPP_com_option_com(some_com,B_4)
=> hBOOL(hAPP_com_bool(wt,B_4)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f606,axiom,
! [X_1] :
( hBOOL(hAPP_H242767318e_bool(bot_bo784226126e_bool,X_1))
<=> hBOOL(bot_bot_bool) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1205,axiom,
! [X_1] :
( hBOOL(is_none_com(X_1))
<=> X_1 = none_com ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1290,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1291,axiom,
! [P] :
( is_bool(P)
=> ( P = fFalse
| P = fTrue ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1352,axiom,
! [P,Q] :
( is_bool(P)
=> hAPP_H242767318e_bool(hAPP_b974863576e_bool(cOMBK_988866959_state,P),Q) = P ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1434,hypothesis,
hBOOL(hoare_1795711768gleton),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1435,hypothesis,
hBOOL(wT_bodies),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1439,hypothesis,
hAPP_p799580910on_com(body,pn) = hAPP_com_option_com(some_com,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1441,conjecture,
hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(hAPP_f360545851e_bool(image_185131637_state(hAPP_f1377420673_state(cOMBB_271860050_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,y)),bot_bo784226126e_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1442,negated_conjecture,
~ hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(hAPP_f360545851e_bool(image_185131637_state(hAPP_f1377420673_state(cOMBB_271860050_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,y)),bot_bo784226126e_bool))),
inference(negated_conjecture,[status(cth)],[f1441]) ).
fof(f1472,plain,
! [X0] : is_bool(is_none_com(X0)),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f1479,plain,
is_bool(bot_bot_bool),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f1484,plain,
is_bool(fFalse),
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f1487,plain,
! [X0,X1] : is_bool(hAPP_com_bool(X0,X1)),
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f1540,plain,
! [X0,X1] : is_bool(hAPP_f1378282496l_bool(X0,X1)),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f1563,plain,
! [G_2,G_3,Ts] :
( hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(G_2),Ts))
| ~ hBOOL(hAPP_f1378282496l_bool(hAPP_f849457489l_bool(ord_le1449778818e_bool,G_3),G_2))
| ~ hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(G_3),Ts)) ),
inference(pre_NNF_transformation,[status(thm)],[f86]) ).
fof(f1564,plain,
! [G_3,Ts] :
( ! [G_2] :
( hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(G_2),Ts))
| ~ hBOOL(hAPP_f1378282496l_bool(hAPP_f849457489l_bool(ord_le1449778818e_bool,G_3),G_2)) )
| ~ hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(G_3),Ts)) ),
inference(miniscoping,[status(thm)],[f1563]) ).
fof(f1565,plain,
! [X0,X1,X2] :
( hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(X2),X1))
| ~ hBOOL(hAPP_f1378282496l_bool(hAPP_f849457489l_bool(ord_le1449778818e_bool,X0),X2))
| ~ hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f1564]) ).
fof(f1614,plain,
! [X0] : hBOOL(hAPP_f1378282496l_bool(hAPP_f849457489l_bool(ord_le1449778818e_bool,bot_bo784226126e_bool),X0)),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f1733,plain,
! [C] :
( hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(bot_bo784226126e_bool),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,C)),bot_bo784226126e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,C))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_1795711768gleton) ),
inference(pre_NNF_transformation,[status(thm)],[f149]) ).
fof(f1734,plain,
( ! [C] :
( hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(bot_bo784226126e_bool),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,C)),bot_bo784226126e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,C)) )
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_1795711768gleton) ),
inference(miniscoping,[status(thm)],[f1733]) ).
fof(f1735,plain,
! [X0] :
( hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(bot_bo784226126e_bool),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,X0)),bot_bo784226126e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,X0))
| ~ hBOOL(wT_bodies)
| ~ hBOOL(hoare_1795711768gleton) ),
inference(cnf_transformation,[status(thm)],[f1734]) ).
fof(f1889,plain,
bot_bo784226126e_bool = hAPP_f806699093e_bool(collec637225377_state,hAPP_b974863576e_bool(cOMBK_988866959_state,fFalse)),
inference(cnf_transformation,[status(thm)],[f195]) ).
fof(f2258,plain,
! [X0] : hAPP_f806699093e_bool(collec637225377_state,X0) = X0,
inference(cnf_transformation,[status(thm)],[f323]) ).
fof(f2422,plain,
! [Pn,B_4] :
( hBOOL(hAPP_com_bool(wt,B_4))
| hAPP_p799580910on_com(body,Pn) != hAPP_com_option_com(some_com,B_4)
| ~ hBOOL(wT_bodies) ),
inference(pre_NNF_transformation,[status(thm)],[f380]) ).
fof(f2423,plain,
( ! [B_4] :
( hBOOL(hAPP_com_bool(wt,B_4))
| ! [Pn] : hAPP_p799580910on_com(body,Pn) != hAPP_com_option_com(some_com,B_4) )
| ~ hBOOL(wT_bodies) ),
inference(miniscoping,[status(thm)],[f2422]) ).
fof(f2424,plain,
! [X0,X1] :
( hBOOL(hAPP_com_bool(wt,X1))
| hAPP_p799580910on_com(body,X0) != hAPP_com_option_com(some_com,X1)
| ~ hBOOL(wT_bodies) ),
inference(cnf_transformation,[status(thm)],[f2423]) ).
fof(f3256,plain,
! [X_1] :
( ( ~ hBOOL(bot_bot_bool)
| hBOOL(hAPP_H242767318e_bool(bot_bo784226126e_bool,X_1)) )
& ( hBOOL(bot_bot_bool)
| ~ hBOOL(hAPP_H242767318e_bool(bot_bo784226126e_bool,X_1)) ) ),
inference(NNF_transformation,[status(thm)],[f606]) ).
fof(f3257,plain,
( ( ~ hBOOL(bot_bot_bool)
| ! [X_1] : hBOOL(hAPP_H242767318e_bool(bot_bo784226126e_bool,X_1)) )
& ( hBOOL(bot_bot_bool)
| ! [X_1] : ~ hBOOL(hAPP_H242767318e_bool(bot_bo784226126e_bool,X_1)) ) ),
inference(miniscoping,[status(thm)],[f3256]) ).
fof(f3259,plain,
! [X0] :
( ~ hBOOL(bot_bot_bool)
| hBOOL(hAPP_H242767318e_bool(bot_bo784226126e_bool,X0)) ),
inference(cnf_transformation,[status(thm)],[f3257]) ).
fof(f5033,plain,
! [X_1] :
( ( X_1 != none_com
| hBOOL(is_none_com(X_1)) )
& ( X_1 = none_com
| ~ hBOOL(is_none_com(X_1)) ) ),
inference(NNF_transformation,[status(thm)],[f1205]) ).
fof(f5034,plain,
( ! [X_1] :
( X_1 != none_com
| hBOOL(is_none_com(X_1)) )
& ! [X_1] :
( X_1 = none_com
| ~ hBOOL(is_none_com(X_1)) ) ),
inference(miniscoping,[status(thm)],[f5033]) ).
fof(f5036,plain,
! [X0] :
( X0 != none_com
| hBOOL(is_none_com(X0)) ),
inference(cnf_transformation,[status(thm)],[f5034]) ).
fof(f5298,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[status(thm)],[f1290]) ).
fof(f5299,plain,
! [P] :
( P = fFalse
| P = fTrue
| ~ is_bool(P) ),
inference(pre_NNF_transformation,[status(thm)],[f1291]) ).
fof(f5300,plain,
! [X0] :
( X0 = fFalse
| X0 = fTrue
| ~ is_bool(X0) ),
inference(cnf_transformation,[status(thm)],[f5299]) ).
fof(f5377,plain,
! [P,Q] :
( hAPP_H242767318e_bool(hAPP_b974863576e_bool(cOMBK_988866959_state,P),Q) = P
| ~ is_bool(P) ),
inference(pre_NNF_transformation,[status(thm)],[f1352]) ).
fof(f5378,plain,
! [P] :
( ! [Q] : hAPP_H242767318e_bool(hAPP_b974863576e_bool(cOMBK_988866959_state,P),Q) = P
| ~ is_bool(P) ),
inference(miniscoping,[status(thm)],[f5377]) ).
fof(f5379,plain,
! [X0,X1] :
( hAPP_H242767318e_bool(hAPP_b974863576e_bool(cOMBK_988866959_state,X0),X1) = X0
| ~ is_bool(X0) ),
inference(cnf_transformation,[status(thm)],[f5378]) ).
fof(f5465,plain,
hBOOL(hoare_1795711768gleton),
inference(cnf_transformation,[status(thm)],[f1434]) ).
fof(f5466,plain,
hBOOL(wT_bodies),
inference(cnf_transformation,[status(thm)],[f1435]) ).
fof(f5470,plain,
hAPP_p799580910on_com(body,pn) = hAPP_com_option_com(some_com,y),
inference(cnf_transformation,[status(thm)],[f1439]) ).
fof(f5472,plain,
~ hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(hAPP_f360545851e_bool(image_185131637_state(hAPP_f1377420673_state(cOMBB_271860050_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,y)),bot_bo784226126e_bool))),
inference(cnf_transformation,[status(thm)],[f1442]) ).
fof(f5707,plain,
hBOOL(is_none_com(none_com)),
inference(destructive_equality_resolution,[status(thm)],[f5036]) ).
fof(f5730,plain,
! [X0,X1] :
( hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(X1),X0))
| ~ hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(bot_bo784226126e_bool),X0)) ),
inference(resolution,[status(thm)],[f1565,f1614]) ).
fof(f7163,plain,
! [X0,X1] :
( hAPP_f1378282496l_bool(X0,X1) = fFalse
| hAPP_f1378282496l_bool(X0,X1) = fTrue ),
inference(resolution,[status(thm)],[f5300,f1540]) ).
fof(f7171,plain,
! [X0,X1] :
( hAPP_com_bool(X0,X1) = fFalse
| hAPP_com_bool(X0,X1) = fTrue ),
inference(resolution,[status(thm)],[f5300,f1487]) ).
fof(f7184,plain,
! [X0] :
( is_none_com(X0) = fFalse
| is_none_com(X0) = fTrue ),
inference(resolution,[status(thm)],[f5300,f1472]) ).
fof(f7194,plain,
( bot_bot_bool = fFalse
| bot_bot_bool = fTrue ),
inference(resolution,[status(thm)],[f5300,f1479]) ).
fof(f8652,plain,
( is_none_com(none_com) = fFalse
| hBOOL(fTrue) ),
inference(paramodulation,[status(thm)],[f7184,f5707]) ).
fof(f8682,plain,
( hBOOL(fTrue)
| hBOOL(fFalse) ),
inference(paramodulation,[status(thm)],[f8652,f5707]) ).
fof(f8687,plain,
hBOOL(fTrue),
inference(forward_subsumption_resolution,[status(thm)],[f8682,f5298]) ).
fof(f8690,plain,
( bot_bot_bool = fFalse
| hBOOL(bot_bot_bool) ),
inference(paramodulation,[status(thm)],[f7194,f8687]) ).
fof(f10994,plain,
bot_bo784226126e_bool = hAPP_b974863576e_bool(cOMBK_988866959_state,fFalse),
inference(forward_demodulation,[status(thm)],[f2258,f1889]) ).
fof(f11992,plain,
! [X0] :
( hAPP_H242767318e_bool(bot_bo784226126e_bool,X0) = fFalse
| ~ is_bool(fFalse) ),
inference(paramodulation,[status(thm)],[f10994,f5379]) ).
fof(f11993,plain,
! [X0] : hAPP_H242767318e_bool(bot_bo784226126e_bool,X0) = fFalse,
inference(forward_subsumption_resolution,[status(thm)],[f11992,f1484]) ).
fof(f11994,plain,
( ~ hBOOL(bot_bot_bool)
| hBOOL(fFalse) ),
inference(backward_demodulation,[status(thm)],[f11993,f3259]) ).
fof(f11997,plain,
~ hBOOL(bot_bot_bool),
inference(forward_subsumption_resolution,[status(thm)],[f11994,f5298]) ).
fof(f12002,plain,
bot_bot_bool = fFalse,
inference(backward_subsumption_resolution,[status(thm)],[f8690,f11997]) ).
fof(f12964,plain,
! [X0,X1] :
( hAPP_f1378282496l_bool(X0,X1) = bot_bot_bool
| hAPP_f1378282496l_bool(X0,X1) = fTrue ),
inference(forward_demodulation,[status(thm)],[f12002,f7163]) ).
fof(f13128,plain,
( hAPP_f1378282496l_bool(hoare_512830354_state(hAPP_f360545851e_bool(image_185131637_state(hAPP_f1377420673_state(cOMBB_271860050_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,y)),bot_bo784226126e_bool)) = bot_bot_bool
| ~ hBOOL(fTrue) ),
inference(paramodulation,[status(thm)],[f12964,f5472]) ).
fof(f13214,plain,
hAPP_f1378282496l_bool(hoare_512830354_state(hAPP_f360545851e_bool(image_185131637_state(hAPP_f1377420673_state(cOMBB_271860050_pname(hoare_Mirabelle_MGT),body_1)),dom_pname_com(body))),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,y)),bot_bo784226126e_bool)) = bot_bot_bool,
inference(forward_subsumption_resolution,[status(thm)],[f13128,f8687]) ).
fof(f14538,plain,
! [X0,X1] :
( hAPP_com_bool(X0,X1) = bot_bot_bool
| hAPP_com_bool(X0,X1) = fTrue ),
inference(forward_demodulation,[status(thm)],[f12002,f7171]) ).
fof(f14569,plain,
! [X0] :
( hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(bot_bo784226126e_bool),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,X0)),bot_bo784226126e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,X0))
| ~ hBOOL(wT_bodies) ),
inference(forward_subsumption_resolution,[status(thm)],[f1735,f5465]) ).
fof(f14573,plain,
! [X0,X1] :
( hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(X1),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,X0)),bot_bo784226126e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,X0))
| ~ hBOOL(wT_bodies) ),
inference(resolution,[status(thm)],[f14569,f5730]) ).
fof(f14595,plain,
! [X0,X1] :
( hBOOL(hAPP_f1378282496l_bool(hoare_512830354_state(X1),hAPP_f806699093e_bool(hAPP_H1902130436e_bool(insert1744391420_state,hAPP_c1455475371_state(hoare_Mirabelle_MGT,X0)),bot_bo784226126e_bool)))
| ~ hBOOL(hAPP_com_bool(wt,X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f14573,f5466]) ).
fof(f14640,plain,
( hBOOL(bot_bot_bool)
| ~ hBOOL(hAPP_com_bool(wt,y)) ),
inference(paramodulation,[status(thm)],[f13214,f14595]) ).
fof(f14647,plain,
~ hBOOL(hAPP_com_bool(wt,y)),
inference(forward_subsumption_resolution,[status(thm)],[f14640,f11997]) ).
fof(f14649,plain,
( hAPP_com_bool(wt,y) = bot_bot_bool
| ~ hBOOL(fTrue) ),
inference(paramodulation,[status(thm)],[f14538,f14647]) ).
fof(f14650,plain,
hAPP_com_bool(wt,y) = bot_bot_bool,
inference(forward_subsumption_resolution,[status(thm)],[f14649,f8687]) ).
fof(f80795,plain,
! [X0,X1] :
( hBOOL(hAPP_com_bool(wt,X1))
| hAPP_p799580910on_com(body,X0) != hAPP_com_option_com(some_com,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f2424,f5466]) ).
fof(f80796,plain,
hBOOL(hAPP_com_bool(wt,y)),
inference(resolution,[status(thm)],[f80795,f5470]) ).
fof(f80820,plain,
hBOOL(bot_bot_bool),
inference(forward_demodulation,[status(thm)],[f14650,f80796]) ).
fof(f80821,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f80820,f11997]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW474+3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.41 % Computer : n013.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 09:58:36 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.38/0.63 % Drodi V4.1.1
% 192.37/25.02 % Refutation found
% 192.37/25.02 % SZS status Theorem for theBenchmark: Theorem is valid
% 192.37/25.02 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 84.14/25.20 % Elapsed time: 24.761674 seconds
% 84.14/25.20 % CPU time: 193.644304 seconds
% 84.14/25.20 % Total memory used: 797.907 MB
% 84.14/25.20 % Net memory used: 749.784 MB
%------------------------------------------------------------------------------