%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV089+1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 12:47:03 PM UTC 2026
% Result : Theorem 2.51s 1.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : HWV089+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.22/0.52 % Computer : n006.cluster.edu
% 0.22/0.52 % Model : x86_64 x86_64
% 0.22/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.22/0.52 % Memory : 8046.5625MB
% 0.22/0.52 % OS : Linux 6.8.0-71-generic
% 0.22/0.52 % CPULimit : 300
% 0.22/0.52 % WCLimit : 300
% 0.22/0.52 % DateTime : Sun Sep 20 21:18:14 UTC 2026
% 0.22/0.52 % CPUTime :
% 0.69/1.05 % Drodi V4.1.1
% 2.51/1.60 % Refutation found
% 2.51/1.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.51/1.60 % SZS output start CNFRefutation for theBenchmark
% 2.51/1.60 fof(f321,conjecture,(
% 2.51/1.60 (! [VarCurr] :( reachableState(VarCurr)=> v4(VarCurr) ) )),
% 2.51/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/1.60 fof(f322,negated_conjecture,(
% 2.51/1.60 ~((! [VarCurr] :( reachableState(VarCurr)=> v4(VarCurr) ) ))),
% 2.51/1.60 inference(negated_conjecture,[status(cth)],[f321])).
% 2.51/1.60 fof(f323,axiom,(
% 2.51/1.60 (! [VarCurr] :( ~ v4(VarCurr)<=> v3674(VarCurr) ) )),
% 2.51/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/1.60 fof(f324,axiom,(
% 2.51/1.60 (! [VarCurr] :( ~ v3674(VarCurr)<=> v3675(VarCurr) ) )),
% 2.51/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/1.60 fof(f325,axiom,(
% 2.51/1.60 (! [VarCurr] :( v3675(VarCurr)<=> ( v3677(VarCurr)& v3693(VarCurr) ) ) )),
% 2.51/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/1.60 fof(f326,axiom,(
% 2.51/1.60 (! [VarCurr] :( v3693(VarCurr)<=> ( v3679(VarCurr,bitIndex0)| v3679(VarCurr,bitIndex1) ) ) )),
% 2.51/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/1.60 fof(f327,axiom,(
% 2.51/1.60 (! [VarCurr] :( ~ v3677(VarCurr)<=> v3678(VarCurr) ) )),
% 2.51/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/1.60 fof(f328,axiom,(
% 2.51/1.60 (! [VarCurr] :( v3678(VarCurr)<=> ( v3679(VarCurr,bitIndex0)& v3679(VarCurr,bitIndex1) ) ) )),
% 2.51/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/1.60 fof(f329,axiom,(
% 2.51/1.60 (! [VarCurr] :( v3679(VarCurr,bitIndex0)<=> v3680(VarCurr) ) )),
% 2.51/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/1.60 fof(f330,axiom,(
% 2.51/1.60 (! [VarCurr] :( v3679(VarCurr,bitIndex1)<=> $true ) )),
% 2.51/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/1.60 fof(f331,axiom,(
% 2.51/1.60 (! [VarCurr] :( v3680(VarCurr)<=> ( v3682(VarCurr)& v3684(VarCurr,bitIndex5) ) ) )),
% 2.51/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/1.60 fof(f344,axiom,(
% 2.51/1.60 (! [VarCurr] : ~ v3684(VarCurr,bitIndex5) )),
% 2.51/1.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.51/1.60 fof(f6910,plain,(
% 2.51/1.60 (?[VarCurr]: (reachableState(VarCurr)&~v4(VarCurr)))),
% 2.51/1.60 inference(pre_NNF_transformation,[status(thm)],[f322])).
% 2.51/1.60 fof(f6911,plain,(
% 2.51/1.60 (reachableState(sK0_skl)&~v4(sK0_skl))),
% 2.51/1.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f6910])).
% 2.51/1.60 fof(f6913,plain,(
% 2.51/1.60 ~v4(sK0_skl)),
% 2.51/1.60 inference(cnf_transformation,[status(thm)],[f6911])).
% 2.51/1.60 fof(f6914,plain,(
% 2.51/1.60 ![VarCurr]: ((v4(VarCurr)|v3674(VarCurr))&(~v4(VarCurr)|~v3674(VarCurr)))),
% 2.51/1.60 inference(NNF_transformation,[status(thm)],[f323])).
% 2.51/1.60 fof(f6915,plain,(
% 2.51/1.60 (![VarCurr]: (v4(VarCurr)|v3674(VarCurr)))&(![VarCurr]: (~v4(VarCurr)|~v3674(VarCurr)))),
% 2.51/1.60 inference(miniscoping,[status(thm)],[f6914])).
% 2.51/1.60 fof(f6916,plain,(
% 2.51/1.60 ![X0]: (v4(X0)|v3674(X0))),
% 2.51/1.60 inference(cnf_transformation,[status(thm)],[f6915])).
% 2.51/1.60 fof(f6918,plain,(
% 2.51/1.60 ![VarCurr]: ((v3674(VarCurr)|v3675(VarCurr))&(~v3674(VarCurr)|~v3675(VarCurr)))),
% 2.51/1.60 inference(NNF_transformation,[status(thm)],[f324])).
% 2.51/1.60 fof(f6919,plain,(
% 2.51/1.60 (![VarCurr]: (v3674(VarCurr)|v3675(VarCurr)))&(![VarCurr]: (~v3674(VarCurr)|~v3675(VarCurr)))),
% 2.51/1.60 inference(miniscoping,[status(thm)],[f6918])).
% 2.51/1.60 fof(f6921,plain,(
% 2.51/1.60 ![X0]: (~v3674(X0)|~v3675(X0))),
% 2.51/1.60 inference(cnf_transformation,[status(thm)],[f6919])).
% 2.51/1.60 fof(f6922,plain,(
% 2.51/1.60 ![VarCurr]: ((~v3675(VarCurr)|(v3677(VarCurr)&v3693(VarCurr)))&(v3675(VarCurr)|(~v3677(VarCurr)|~v3693(VarCurr))))),
% 2.51/1.60 inference(NNF_transformation,[status(thm)],[f325])).
% 2.51/1.60 fof(f6923,plain,(
% 2.51/1.60 (![VarCurr]: (~v3675(VarCurr)|(v3677(VarCurr)&v3693(VarCurr))))&(![VarCurr]: (v3675(VarCurr)|(~v3677(VarCurr)|~v3693(VarCurr))))),
% 2.51/1.60 inference(miniscoping,[status(thm)],[f6922])).
% 2.51/1.60 fof(f6926,plain,(
% 2.51/1.60 ![X0]: (v3675(X0)|~v3677(X0)|~v3693(X0))),
% 2.51/1.60 inference(cnf_transformation,[status(thm)],[f6923])).
% 2.51/1.60 fof(f6927,plain,(
% 2.51/1.60 ![VarCurr]: ((~v3693(VarCurr)|(v3679(VarCurr,bitIndex0)|v3679(VarCurr,bitIndex1)))&(v3693(VarCurr)|(~v3679(VarCurr,bitIndex0)&~v3679(VarCurr,bitIndex1))))),
% 2.51/1.60 inference(NNF_transformation,[status(thm)],[f326])).
% 2.51/1.60 fof(f6928,plain,(
% 2.51/1.60 (![VarCurr]: (~v3693(VarCurr)|(v3679(VarCurr,bitIndex0)|v3679(VarCurr,bitIndex1))))&(![VarCurr]: (v3693(VarCurr)|(~v3679(VarCurr,bitIndex0)&~v3679(VarCurr,bitIndex1))))),
% 2.51/1.60 inference(miniscoping,[status(thm)],[f6927])).
% 2.51/1.60 fof(f6931,plain,(
% 2.51/1.60 ![X0]: (v3693(X0)|~v3679(X0,bitIndex1))),
% 2.51/1.60 inference(cnf_transformation,[status(thm)],[f6928])).
% 2.51/1.60 fof(f6932,plain,(
% 2.51/1.60 ![VarCurr]: ((v3677(VarCurr)|v3678(VarCurr))&(~v3677(VarCurr)|~v3678(VarCurr)))),
% 2.51/1.60 inference(NNF_transformation,[status(thm)],[f327])).
% 2.51/1.60 fof(f6933,plain,(
% 2.51/1.60 (![VarCurr]: (v3677(VarCurr)|v3678(VarCurr)))&(![VarCurr]: (~v3677(VarCurr)|~v3678(VarCurr)))),
% 2.51/1.60 inference(miniscoping,[status(thm)],[f6932])).
% 2.51/1.60 fof(f6934,plain,(
% 2.51/1.60 ![X0]: (v3677(X0)|v3678(X0))),
% 2.51/1.60 inference(cnf_transformation,[status(thm)],[f6933])).
% 2.51/1.60 fof(f6936,plain,(
% 2.51/1.60 ![VarCurr]: ((~v3678(VarCurr)|(v3679(VarCurr,bitIndex0)&v3679(VarCurr,bitIndex1)))&(v3678(VarCurr)|(~v3679(VarCurr,bitIndex0)|~v3679(VarCurr,bitIndex1))))),
% 2.51/1.60 inference(NNF_transformation,[status(thm)],[f328])).
% 2.51/1.60 fof(f6937,plain,(
% 2.51/1.60 (![VarCurr]: (~v3678(VarCurr)|(v3679(VarCurr,bitIndex0)&v3679(VarCurr,bitIndex1))))&(![VarCurr]: (v3678(VarCurr)|(~v3679(VarCurr,bitIndex0)|~v3679(VarCurr,bitIndex1))))),
% 2.51/1.60 inference(miniscoping,[status(thm)],[f6936])).
% 2.51/1.60 fof(f6938,plain,(
% 2.51/1.60 ![X0]: (~v3678(X0)|v3679(X0,bitIndex0))),
% 2.51/1.60 inference(cnf_transformation,[status(thm)],[f6937])).
% 2.51/1.60 fof(f6941,plain,(
% 2.51/1.60 ![VarCurr]: ((~v3679(VarCurr,bitIndex0)|v3680(VarCurr))&(v3679(VarCurr,bitIndex0)|~v3680(VarCurr)))),
% 2.51/1.60 inference(NNF_transformation,[status(thm)],[f329])).
% 2.51/1.60 fof(f6942,plain,(
% 2.51/1.60 (![VarCurr]: (~v3679(VarCurr,bitIndex0)|v3680(VarCurr)))&(![VarCurr]: (v3679(VarCurr,bitIndex0)|~v3680(VarCurr)))),
% 2.51/1.60 inference(miniscoping,[status(thm)],[f6941])).
% 2.51/1.60 fof(f6943,plain,(
% 2.51/1.60 ![X0]: (~v3679(X0,bitIndex0)|v3680(X0))),
% 2.51/1.60 inference(cnf_transformation,[status(thm)],[f6942])).
% 2.51/1.60 fof(f6945,plain,(
% 2.51/1.60 ![VarCurr]: ((~v3679(VarCurr,bitIndex1)|$true)&(v3679(VarCurr,bitIndex1)|$false))),
% 2.51/1.60 inference(NNF_transformation,[status(thm)],[f330])).
% 2.51/1.60 fof(f6946,plain,(
% 2.51/1.60 ((![VarCurr]: ~v3679(VarCurr,bitIndex1))|$true)&((![VarCurr]: v3679(VarCurr,bitIndex1))|$false)),
% 2.51/1.60 inference(miniscoping,[status(thm)],[f6945])).
% 2.51/1.60 fof(f6947,plain,(
% 2.51/1.60 ![VarCurr]: v3679(VarCurr,bitIndex1)),
% 2.51/1.61 inference(true_and_false_simplification,[status(thm)],[f6946])).
% 2.51/1.61 fof(f6948,plain,(
% 2.51/1.61 ![X0]: (v3679(X0,bitIndex1))),
% 2.51/1.61 inference(cnf_transformation,[status(thm)],[f6947])).
% 2.51/1.61 fof(f6949,plain,(
% 2.51/1.61 ![VarCurr]: ((~v3680(VarCurr)|(v3682(VarCurr)&v3684(VarCurr,bitIndex5)))&(v3680(VarCurr)|(~v3682(VarCurr)|~v3684(VarCurr,bitIndex5))))),
% 2.51/1.61 inference(NNF_transformation,[status(thm)],[f331])).
% 2.51/1.61 fof(f6950,plain,(
% 2.51/1.61 (![VarCurr]: (~v3680(VarCurr)|(v3682(VarCurr)&v3684(VarCurr,bitIndex5))))&(![VarCurr]: (v3680(VarCurr)|(~v3682(VarCurr)|~v3684(VarCurr,bitIndex5))))),
% 2.51/1.61 inference(miniscoping,[status(thm)],[f6949])).
% 2.51/1.61 fof(f6952,plain,(
% 2.51/1.61 ![X0]: (~v3680(X0)|v3684(X0,bitIndex5))),
% 2.51/1.61 inference(cnf_transformation,[status(thm)],[f6950])).
% 2.51/1.61 fof(f7003,plain,(
% 2.51/1.61 ![X0]: (~v3684(X0,bitIndex5))),
% 2.51/1.61 inference(cnf_transformation,[status(thm)],[f344])).
% 2.51/1.61 fof(f34521,plain,(
% 2.51/1.61 ![X0]: (v3693(X0))),
% 2.51/1.61 inference(backward_subsumption_resolution,[status(thm)],[f6931,f6948])).
% 2.51/1.61 fof(f34522,plain,(
% 2.51/1.61 ![X0]: (v3675(X0)|~v3677(X0))),
% 2.51/1.61 inference(backward_subsumption_resolution,[status(thm)],[f6926,f34521])).
% 2.51/1.61 fof(f34541,plain,(
% 2.51/1.61 ![X0]: (~v3680(X0))),
% 2.51/1.61 inference(backward_subsumption_resolution,[status(thm)],[f6952,f7003])).
% 2.51/1.61 fof(f34546,plain,(
% 2.51/1.61 ![X0]: (~v3679(X0,bitIndex0))),
% 2.51/1.61 inference(backward_subsumption_resolution,[status(thm)],[f6943,f34541])).
% 2.51/1.61 fof(f34766,plain,(
% 2.51/1.61 ![X0]: (~v3678(X0))),
% 2.51/1.61 inference(backward_subsumption_resolution,[status(thm)],[f6938,f34546])).
% 2.51/1.61 fof(f34767,plain,(
% 2.51/1.61 ![X0]: (v3677(X0))),
% 2.51/1.61 inference(backward_subsumption_resolution,[status(thm)],[f6934,f34766])).
% 2.51/1.61 fof(f38711,plain,(
% 2.51/1.61 ![X0]: (~v3674(X0))),
% 2.51/1.61 inference(backward_subsumption_resolution,[status(thm)],[f6921,f38712])).
% 2.51/1.61 fof(f38712,plain,(
% 2.51/1.61 ![X0]: (v3675(X0))),
% 2.51/1.61 inference(forward_subsumption_resolution,[status(thm)],[f34522,f34767])).
% 2.51/1.61 fof(f38713,plain,(
% 2.51/1.61 ![X0]: (v4(X0))),
% 2.51/1.61 inference(backward_subsumption_resolution,[status(thm)],[f6916,f38711])).
% 2.51/1.61 fof(f38716,plain,(
% 2.51/1.61 $false),
% 2.51/1.61 inference(backward_subsumption_resolution,[status(thm)],[f6913,f38713])).
% 2.51/1.61 % SZS output end CNFRefutation for theBenchmark.p
% 1.04/1.86 % Elapsed time: 1.309199 seconds
% 1.04/1.86 % CPU time: 4.973646 seconds
% 1.04/1.86 % Total memory used: 702.634 MB
% 1.04/1.86 % Net memory used: 700.366 MB
%------------------------------------------------------------------------------