%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW470+2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:09:11 PM UTC 2026
% Result : Theorem 0.26s 0.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470+2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n013.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 09:55:21 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.14/0.48 % Drodi V4.1.1
% 0.26/0.69 % Refutation found
% 0.26/0.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.26/0.69 % SZS output start CNFRefutation for theBenchmark
% 0.26/0.69 fof(f18,hypothesis,(
% 0.26/0.69 is_bool(fFalse) ),
% 0.26/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f39,axiom,(
% 0.26/0.69 (! [Ga,Ca,Q_1,Pa] :( (! [Z_7,S_2] :( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Pa,Z_7),S_2))=> hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(Ga),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),S_2)),Ca,hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_a2036067514e_bool(Q_1,Z_7)))),bot_bo1181479936a_bool))) ))=> hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(Ga),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(Pa,Ca,Q_1)),bot_bo1181479936a_bool))) ) )),
% 0.26/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f737,axiom,(
% 0.26/0.69 ~ hBOOL(fFalse) ),
% 0.26/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f749,axiom,(
% 0.26/0.69 (! [P,Q] :( is_bool(P)=> hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,P),Q) = P ) )),
% 0.26/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f755,axiom,(
% 0.26/0.69 (! [P,Q] : hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,P),Q) = P )),
% 0.26/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f830,conjecture,(
% 0.26/0.69 hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo1181479936a_bool))) ),
% 0.26/0.69 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.26/0.69 fof(f831,negated_conjecture,(
% 0.26/0.69 ~(hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo1181479936a_bool))) )),
% 0.26/0.69 inference(negated_conjecture,[status(cth)],[f830])).
% 0.26/0.69 fof(f851,plain,(
% 0.26/0.69 is_bool(fFalse)),
% 0.26/0.69 inference(cnf_transformation,[status(thm)],[f18])).
% 0.26/0.69 fof(f896,plain,(
% 0.26/0.69 ![Ga,Ca,Q_1,Pa]: ((?[Z_7,S_2]: (hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Pa,Z_7),S_2))&~hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(Ga),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),S_2)),Ca,hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_a2036067514e_bool(Q_1,Z_7)))),bot_bo1181479936a_bool)))))|hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(Ga),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(Pa,Ca,Q_1)),bot_bo1181479936a_bool))))),
% 0.26/0.69 inference(pre_NNF_transformation,[status(thm)],[f39])).
% 0.26/0.69 fof(f897,plain,(
% 0.26/0.69 ![Ga,Ca,Q_1,Pa]: ((hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Pa,sK0_skl(Pa,Q_1,Ca,Ga)),sK1_skl(Pa,Q_1,Ca,Ga)))&~hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(Ga),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),sK1_skl(Pa,Q_1,Ca,Ga))),Ca,hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_a2036067514e_bool(Q_1,sK0_skl(Pa,Q_1,Ca,Ga))))),bot_bo1181479936a_bool))))|hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(Ga),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(Pa,Ca,Q_1)),bot_bo1181479936a_bool))))),
% 0.26/0.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Z_7,sK0_skl(Pa,Q_1,Ca,Ga)),skolemize(S_2,sK1_skl(Pa,Q_1,Ca,Ga))],[f896])).
% 0.26/0.72 fof(f898,plain,(
% 0.26/0.72 ![X0,X1,X2,X3]: (hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X0,sK0_skl(X0,X1,X2,X3)),sK1_skl(X0,X1,X2,X3)))|hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X3),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(X0,X2,X1)),bot_bo1181479936a_bool))))),
% 0.26/0.72 inference(cnf_transformation,[status(thm)],[f897])).
% 0.26/0.72 fof(f2982,plain,(
% 0.26/0.72 ~hBOOL(fFalse)),
% 0.26/0.72 inference(cnf_transformation,[status(thm)],[f737])).
% 0.26/0.72 fof(f3000,plain,(
% 0.26/0.72 ![P,Q]: (~is_bool(P)|hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,P),Q)=P)),
% 0.26/0.72 inference(pre_NNF_transformation,[status(thm)],[f749])).
% 0.26/0.72 fof(f3001,plain,(
% 0.26/0.72 ![P]: (~is_bool(P)|(![Q]: hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,P),Q)=P))),
% 0.26/0.72 inference(miniscoping,[status(thm)],[f3000])).
% 0.26/0.72 fof(f3002,plain,(
% 0.26/0.72 ![X0,X1]: (~is_bool(X0)|hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,X0),X1)=X0)),
% 0.26/0.72 inference(cnf_transformation,[status(thm)],[f3001])).
% 0.26/0.72 fof(f3008,plain,(
% 0.26/0.72 ![X0,X1]: (hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X1)=X0)),
% 0.26/0.72 inference(cnf_transformation,[status(thm)],[f755])).
% 0.26/0.72 fof(f3089,plain,(
% 0.26/0.72 ~hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo1181479936a_bool)))),
% 0.26/0.72 inference(cnf_transformation,[status(thm)],[f831])).
% 0.26/0.72 fof(f3358,plain,(
% 0.26/0.72 ![X0]: (hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse),X0)=fFalse)),
% 0.26/0.72 inference(resolution,[status(thm)],[f3002,f851])).
% 0.26/0.72 fof(f3568,plain,(
% 0.26/0.72 ![X0,X1,X2,X3]: (hBOOL(hAPP_state_bool(X0,sK1_skl(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X1,X2,X3)))|hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X3),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X2,X1)),bot_bo1181479936a_bool))))),
% 0.26/0.72 inference(paramodulation,[status(thm)],[f3008,f898])).
% 0.26/0.72 fof(f3824,plain,(
% 0.26/0.72 hBOOL(hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse),sK1_skl(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),c,g)))),
% 0.26/0.72 inference(resolution,[status(thm)],[f3568,f3089])).
% 0.26/0.72 fof(f3859,plain,(
% 0.26/0.72 hBOOL(fFalse)),
% 0.26/0.72 inference(forward_demodulation,[status(thm)],[f3358,f3824])).
% 0.26/0.72 fof(f3860,plain,(
% 0.26/0.72 $false),
% 0.26/0.72 inference(forward_subsumption_resolution,[status(thm)],[f3859,f2982])).
% 0.26/0.72 % SZS output end CNFRefutation for theBenchmark.p
% 0.33/0.77 % Elapsed time: 0.391612 seconds
% 0.33/0.77 % CPU time: 1.879250 seconds
% 0.33/0.77 % Total memory used: 194.663 MB
% 0.33/0.77 % Net memory used: 193.359 MB
%------------------------------------------------------------------------------