%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW470+3 : 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 : 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 : Thu Sep 24 03:09:11 PM UTC 2026
% Result : Theorem 0.20s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470+3 : 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.37 % Computer : n001.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 10:01:30 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.20/0.49 % Drodi V4.1.1
% 0.20/0.58 % Refutation found
% 0.20/0.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/0.58 % SZS output start CNFRefutation for theBenchmark
% 0.20/0.58 fof(f23,hypothesis,(
% 0.20/0.58 is_bool(fFalse) ),
% 0.20/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.58 fof(f41,axiom,(
% 0.20/0.58 (! [Ga,Ca,Q_1,Pa] :( (! [Z_11,S_2] :( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Pa,Z_11),S_2))=> hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(Ga),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_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_11)))),bot_bo797238721a_bool))) ))=> hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(Ga),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(Pa,Ca,Q_1)),bot_bo797238721a_bool))) ) )),
% 0.20/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.58 fof(f55,axiom,(
% 0.20/0.58 (! [A_13] : hAPP_f20753329a_bool(collec351493750iple_a,hAPP_H426895267a_bool(fequal963300192iple_a,A_13)) = hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,A_13),bot_bo797238721a_bool) )),
% 0.20/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.58 fof(f235,axiom,(
% 0.20/0.58 (! [Pa] : hAPP_f20753329a_bool(collec351493750iple_a,Pa) = Pa )),
% 0.20/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.58 fof(f1242,axiom,(
% 0.20/0.58 ~ hBOOL(fFalse) ),
% 0.20/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.58 fof(f1264,axiom,(
% 0.20/0.58 (! [P,Q] :( is_bool(P)=> hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,P),Q) = P ) )),
% 0.20/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.58 fof(f1287,axiom,(
% 0.20/0.58 (! [P,Q] : hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,P),Q) = P )),
% 0.20/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.58 fof(f1399,conjecture,(
% 0.20/0.58 hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(g),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_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_bo797238721a_bool))) ),
% 0.20/0.58 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.20/0.58 fof(f1400,negated_conjecture,(
% 0.20/0.58 ~(hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(g),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_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_bo797238721a_bool))) )),
% 0.20/0.58 inference(negated_conjecture,[status(cth)],[f1399])).
% 0.20/0.58 fof(f1423,plain,(
% 0.20/0.58 is_bool(fFalse)),
% 0.20/0.58 inference(cnf_transformation,[status(thm)],[f23])).
% 0.20/0.58 fof(f1454,plain,(
% 0.20/0.58 ![Ga,Ca,Q_1,Pa]: ((?[Z_11,S_2]: (hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Pa,Z_11),S_2))&~hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(Ga),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_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_11)))),bot_bo797238721a_bool)))))|hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(Ga),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(Pa,Ca,Q_1)),bot_bo797238721a_bool))))),
% 0.20/0.58 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.20/0.58 fof(f1455,plain,(
% 0.20/0.58 ![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_f1695230391l_bool(hoare_2102800559rivs_a(Ga),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_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_bo797238721a_bool))))|hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(Ga),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(Pa,Ca,Q_1)),bot_bo797238721a_bool))))),
% 0.20/0.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Z_11,sK0_skl(Pa,Q_1,Ca,Ga)),skolemize(S_2,sK1_skl(Pa,Q_1,Ca,Ga))],[f1454])).
% 0.20/0.58 fof(f1456,plain,(
% 0.20/0.58 ![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_f1695230391l_bool(hoare_2102800559rivs_a(X3),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(X0,X2,X1)),bot_bo797238721a_bool))))),
% 0.20/0.58 inference(cnf_transformation,[status(thm)],[f1455])).
% 0.20/0.58 fof(f1493,plain,(
% 0.20/0.58 ![X0]: (hAPP_f20753329a_bool(collec351493750iple_a,hAPP_H426895267a_bool(fequal963300192iple_a,X0))=hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,X0),bot_bo797238721a_bool))),
% 0.20/0.58 inference(cnf_transformation,[status(thm)],[f55])).
% 0.20/0.58 fof(f2025,plain,(
% 0.20/0.58 ![X0]: (hAPP_f20753329a_bool(collec351493750iple_a,X0)=X0)),
% 0.20/0.58 inference(cnf_transformation,[status(thm)],[f235])).
% 0.20/0.58 fof(f4947,plain,(
% 0.20/0.58 ~hBOOL(fFalse)),
% 0.20/0.58 inference(cnf_transformation,[status(thm)],[f1242])).
% 0.20/0.58 fof(f4978,plain,(
% 0.20/0.58 ![P,Q]: (~is_bool(P)|hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,P),Q)=P)),
% 0.20/0.58 inference(pre_NNF_transformation,[status(thm)],[f1264])).
% 0.20/0.58 fof(f4979,plain,(
% 0.20/0.58 ![P]: (~is_bool(P)|(![Q]: hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,P),Q)=P))),
% 0.20/0.58 inference(miniscoping,[status(thm)],[f4978])).
% 0.20/0.58 fof(f4980,plain,(
% 0.20/0.58 ![X0,X1]: (~is_bool(X0)|hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,X0),X1)=X0)),
% 0.20/0.58 inference(cnf_transformation,[status(thm)],[f4979])).
% 0.20/0.58 fof(f5003,plain,(
% 0.20/0.58 ![X0,X1]: (hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X1)=X0)),
% 0.20/0.58 inference(cnf_transformation,[status(thm)],[f1287])).
% 0.20/0.58 fof(f5117,plain,(
% 0.20/0.58 ~hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(g),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_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_bo797238721a_bool)))),
% 0.20/0.58 inference(cnf_transformation,[status(thm)],[f1400])).
% 0.20/0.58 fof(f5306,plain,(
% 0.20/0.58 ![X0]: (hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse),X0)=fFalse)),
% 0.20/0.58 inference(resolution,[status(thm)],[f4980,f1423])).
% 0.20/0.58 fof(f5529,plain,(
% 0.20/0.58 ![X0,X1,X2,X3]: (hBOOL(hAPP_state_bool(X0,sK1_skl(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X1,X2,X3)))|hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(X3),hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,hoare_1916936827iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X2,X1)),bot_bo797238721a_bool))))),
% 0.20/0.58 inference(paramodulation,[status(thm)],[f5003,f1456])).
% 0.20/0.58 fof(f5650,plain,(
% 0.20/0.58 ~hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(g),hAPP_H426895267a_bool(fequal963300192iple_a,hoare_1916936827iple_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))))))),
% 0.20/0.59 inference(backward_demodulation,[status(thm)],[f5665,f5117])).
% 0.20/0.59 fof(f5665,plain,(
% 0.20/0.59 ![X0]: (hAPP_H426895267a_bool(fequal963300192iple_a,X0)=hAPP_f20753329a_bool(hAPP_H1743777351a_bool(insert956547291iple_a,X0),bot_bo797238721a_bool))),
% 0.20/0.59 inference(forward_demodulation,[status(thm)],[f2025,f1493])).
% 0.20/0.59 fof(f6002,plain,(
% 0.20/0.59 ![X0,X1,X2,X3]: (hBOOL(hAPP_state_bool(X0,sK1_skl(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X1,X2,X3)))|hBOOL(hAPP_f1695230391l_bool(hoare_2102800559rivs_a(X3),hAPP_H426895267a_bool(fequal963300192iple_a,hoare_1916936827iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X2,X1)))))),
% 0.20/0.59 inference(forward_demodulation,[status(thm)],[f5665,f5529])).
% 0.20/0.59 fof(f6004,plain,(
% 0.20/0.59 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.20/0.59 inference(resolution,[status(thm)],[f6002,f5650])).
% 0.20/0.59 fof(f6052,plain,(
% 0.20/0.59 hBOOL(fFalse)),
% 0.20/0.59 inference(forward_demodulation,[status(thm)],[f5306,f6004])).
% 0.20/0.59 fof(f6053,plain,(
% 0.20/0.59 $false),
% 0.20/0.59 inference(forward_subsumption_resolution,[status(thm)],[f6052,f4947])).
% 0.20/0.59 % SZS output end CNFRefutation for theBenchmark.p
% 0.20/0.61 % Elapsed time: 0.236720 seconds
% 0.20/0.61 % CPU time: 0.761299 seconds
% 0.20/0.61 % Total memory used: 236.833 MB
% 0.20/0.61 % Net memory used: 235.393 MB
%------------------------------------------------------------------------------