%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW470+1 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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:09:10 PM UTC 2026
% Result : Theorem 0.25s 0.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW470+1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : drodi -satmode(on) -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.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 21 09:55:06 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.45 % Drodi V4.1.1
% 0.25/0.61 % Refutation found
% 0.25/0.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.25/0.61 % SZS output start CNFRefutation for theBenchmark
% 0.25/0.61 fof(f4,hypothesis,(
% 0.25/0.61 is_bool(fFalse) ),
% 0.25/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.61 fof(f15,axiom,(
% 0.25/0.61 (! [Ga,Ca,Q_1,Pa] :( (! [Z_1,S] :( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Pa,Z_1),S))=> hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),S)),Ca,cOMBK_1458035955bool_a(hAPP_a2036067514e_bool(Q_1,Z_1)))),bot_bo1687970473a_bool))) ))=> hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(Pa,Ca,Q_1)),bot_bo1687970473a_bool))) ) )),
% 0.25/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.61 fof(f22,axiom,(
% 0.25/0.61 (! [A_3] : collec1266446174iple_a(hAPP_H562195827a_bool(fequal1878252616iple_a,A_3)) = hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,A_3),bot_bo1687970473a_bool) )),
% 0.25/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.61 fof(f84,axiom,(
% 0.25/0.61 (! [Pa] : collec1266446174iple_a(Pa) = Pa )),
% 0.25/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.61 fof(f113,axiom,(
% 0.25/0.61 ~ hBOOL(fFalse) ),
% 0.25/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.61 fof(f120,axiom,(
% 0.25/0.61 (! [P,Q] :( is_bool(P)=> hAPP_state_bool(cOMBK_bool_state(P),Q) = P ) )),
% 0.25/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.61 fof(f121,axiom,(
% 0.25/0.61 (! [P,Q] : hAPP_a2036067514e_bool(cOMBK_1458035955bool_a(P),Q) = P )),
% 0.25/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.61 fof(f144,conjecture,(
% 0.25/0.61 hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1687970473a_bool))) ),
% 0.25/0.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.25/0.61 fof(f145,negated_conjecture,(
% 0.25/0.61 ~(hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1687970473a_bool))) )),
% 0.25/0.61 inference(negated_conjecture,[status(cth)],[f144])).
% 0.25/0.61 fof(f149,plain,(
% 0.25/0.61 is_bool(fFalse)),
% 0.25/0.61 inference(cnf_transformation,[status(thm)],[f4])).
% 0.25/0.61 fof(f173,plain,(
% 0.25/0.61 ![Ga,Ca,Q_1,Pa]: ((?[Z_1,S]: (hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(Pa,Z_1),S))&~hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),S)),Ca,cOMBK_1458035955bool_a(hAPP_a2036067514e_bool(Q_1,Z_1)))),bot_bo1687970473a_bool)))))|hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(Pa,Ca,Q_1)),bot_bo1687970473a_bool))))),
% 0.25/0.61 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.25/0.61 fof(f174,plain,(
% 0.25/0.61 ![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_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),sK1_skl(Pa,Q_1,Ca,Ga))),Ca,cOMBK_1458035955bool_a(hAPP_a2036067514e_bool(Q_1,sK0_skl(Pa,Q_1,Ca,Ga))))),bot_bo1687970473a_bool))))|hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(Ga),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(Pa,Ca,Q_1)),bot_bo1687970473a_bool))))),
% 0.25/0.61 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Z_1,sK0_skl(Pa,Q_1,Ca,Ga)),skolemize(S,sK1_skl(Pa,Q_1,Ca,Ga))],[f173])).
% 0.25/0.61 fof(f175,plain,(
% 0.25/0.61 ![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_f1753944735l_bool(hoare_472868247rivs_a(X3),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(X0,X2,X1)),bot_bo1687970473a_bool))))),
% 0.25/0.61 inference(cnf_transformation,[status(thm)],[f174])).
% 0.25/0.61 fof(f199,plain,(
% 0.25/0.61 ![X0]: (collec1266446174iple_a(hAPP_H562195827a_bool(fequal1878252616iple_a,X0))=hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,X0),bot_bo1687970473a_bool))),
% 0.25/0.61 inference(cnf_transformation,[status(thm)],[f22])).
% 0.25/0.61 fof(f379,plain,(
% 0.25/0.61 ![X0]: (collec1266446174iple_a(X0)=X0)),
% 0.25/0.61 inference(cnf_transformation,[status(thm)],[f84])).
% 0.25/0.61 fof(f483,plain,(
% 0.25/0.61 ~hBOOL(fFalse)),
% 0.25/0.61 inference(cnf_transformation,[status(thm)],[f113])).
% 0.25/0.61 fof(f494,plain,(
% 0.25/0.61 ![P,Q]: (~is_bool(P)|hAPP_state_bool(cOMBK_bool_state(P),Q)=P)),
% 0.25/0.61 inference(pre_NNF_transformation,[status(thm)],[f120])).
% 0.25/0.61 fof(f495,plain,(
% 0.25/0.61 ![P]: (~is_bool(P)|(![Q]: hAPP_state_bool(cOMBK_bool_state(P),Q)=P))),
% 0.25/0.61 inference(miniscoping,[status(thm)],[f494])).
% 0.25/0.61 fof(f496,plain,(
% 0.25/0.61 ![X0,X1]: (~is_bool(X0)|hAPP_state_bool(cOMBK_bool_state(X0),X1)=X0)),
% 0.25/0.61 inference(cnf_transformation,[status(thm)],[f495])).
% 0.25/0.61 fof(f497,plain,(
% 0.25/0.61 ![X0,X1]: (hAPP_a2036067514e_bool(cOMBK_1458035955bool_a(X0),X1)=X0)),
% 0.25/0.61 inference(cnf_transformation,[status(thm)],[f121])).
% 0.25/0.61 fof(f522,plain,(
% 0.25/0.61 ~hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1687970473a_bool)))),
% 0.25/0.61 inference(cnf_transformation,[status(thm)],[f145])).
% 0.25/0.61 fof(f589,plain,(
% 0.25/0.61 ![X0,X1,X2,X3]: (hBOOL(hAPP_state_bool(X0,sK1_skl(cOMBK_1458035955bool_a(X0),X1,X2,X3)))|hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(X3),hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(X0),X2,X1)),bot_bo1687970473a_bool))))),
% 0.25/0.61 inference(paramodulation,[status(thm)],[f497,f175])).
% 0.25/0.61 fof(f613,plain,(
% 0.25/0.61 ![X0]: (hAPP_state_bool(cOMBK_bool_state(fFalse),X0)=fFalse)),
% 0.25/0.61 inference(resolution,[status(thm)],[f496,f149])).
% 0.25/0.61 fof(f727,plain,(
% 0.25/0.61 ~hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(g),hAPP_H562195827a_bool(fequal1878252616iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))))),
% 0.25/0.61 inference(backward_demodulation,[status(thm)],[f741,f522])).
% 0.25/0.61 fof(f741,plain,(
% 0.25/0.61 ![X0]: (hAPP_H562195827a_bool(fequal1878252616iple_a,X0)=hAPP_f1400872321a_bool(hAPP_H1816261935a_bool(insert1871499715iple_a,X0),bot_bo1687970473a_bool))),
% 0.25/0.61 inference(forward_demodulation,[status(thm)],[f379,f199])).
% 0.25/0.61 fof(f1184,plain,(
% 0.25/0.61 ![X0,X1,X2,X3]: (hBOOL(hAPP_state_bool(X0,sK1_skl(cOMBK_1458035955bool_a(X0),X1,X2,X3)))|hBOOL(hAPP_f1753944735l_bool(hoare_472868247rivs_a(X3),hAPP_H562195827a_bool(fequal1878252616iple_a,hoare_1050552211iple_a(cOMBK_1458035955bool_a(X0),X2,X1)))))),
% 0.25/0.61 inference(forward_demodulation,[status(thm)],[f741,f589])).
% 0.25/0.61 fof(f1192,plain,(
% 0.25/0.61 hBOOL(hAPP_state_bool(cOMBK_bool_state(fFalse),sK1_skl(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),c,g)))),
% 0.25/0.62 inference(resolution,[status(thm)],[f1184,f727])).
% 0.25/0.62 fof(f1213,plain,(
% 0.25/0.62 hBOOL(fFalse)),
% 0.25/0.62 inference(forward_demodulation,[status(thm)],[f613,f1192])).
% 0.25/0.62 fof(f1214,plain,(
% 0.25/0.62 $false),
% 0.25/0.62 inference(forward_subsumption_resolution,[status(thm)],[f1213,f483])).
% 0.25/0.62 % SZS output end CNFRefutation for theBenchmark.p
% 0.25/0.63 % Elapsed time: 0.211851 seconds
% 0.25/0.63 % CPU time: 1.301714 seconds
% 0.25/0.63 % Total memory used: 132.908 MB
% 0.25/0.63 % Net memory used: 131.603 MB
%------------------------------------------------------------------------------