%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV091+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 : 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 12:47:03 PM UTC 2026
% Result : Theorem 50.89s 7.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV091+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n001.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 20 21:24:27 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.95/1.29 % Drodi V4.1.1
% 50.89/7.62 % Refutation found
% 50.89/7.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 50.89/7.62 % SZS output start CNFRefutation for theBenchmark
% 50.89/7.62 fof(f447,conjecture,(
% 50.89/7.62 (! [VarCurr] :( reachableState(VarCurr)=> v4(VarCurr) ) )),
% 50.89/7.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.89/7.62 fof(f448,negated_conjecture,(
% 50.89/7.62 ~((! [VarCurr] :( reachableState(VarCurr)=> v4(VarCurr) ) ))),
% 50.89/7.62 inference(negated_conjecture,[status(cth)],[f447])).
% 50.89/7.62 fof(f449,axiom,(
% 50.89/7.62 (! [VarCurr] :( ~ v4(VarCurr)<=> v22287(VarCurr) ) )),
% 50.89/7.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.89/7.62 fof(f450,axiom,(
% 50.89/7.62 (! [VarCurr] :( ~ v22287(VarCurr)<=> v22288(VarCurr) ) )),
% 50.89/7.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.89/7.62 fof(f451,axiom,(
% 50.89/7.62 (! [VarCurr] :( v22288(VarCurr)<=> ( v22290(VarCurr)& v22314(VarCurr) ) ) )),
% 50.89/7.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.89/7.62 fof(f452,axiom,(
% 50.89/7.62 (! [VarCurr] :( v22314(VarCurr)<=> ( v22292(VarCurr,bitIndex0)| v22292(VarCurr,bitIndex1) ) ) )),
% 50.89/7.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.89/7.62 fof(f453,axiom,(
% 50.89/7.62 (! [VarCurr] :( ~ v22290(VarCurr)<=> v22291(VarCurr) ) )),
% 50.89/7.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.89/7.62 fof(f454,axiom,(
% 50.89/7.62 (! [VarCurr] :( v22291(VarCurr)<=> ( v22292(VarCurr,bitIndex0)& v22292(VarCurr,bitIndex1) ) ) )),
% 50.89/7.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.89/7.62 fof(f455,axiom,(
% 50.89/7.62 (! [VarCurr] :( v22292(VarCurr,bitIndex0)<=> v22293(VarCurr) ) )),
% 50.89/7.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.89/7.62 fof(f456,axiom,(
% 50.89/7.62 (! [VarCurr] :( v22292(VarCurr,bitIndex1)<=> $true ) )),
% 50.89/7.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.89/7.62 fof(f457,axiom,(
% 50.89/7.62 (! [VarCurr] :( v22293(VarCurr)<=> ( v22295(VarCurr)& v22296(VarCurr,bitIndex9) ) ) )),
% 50.89/7.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.89/7.62 fof(f481,axiom,(
% 50.89/7.62 (! [VarCurr] : ~ v22296(VarCurr,bitIndex9) )),
% 50.89/7.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 50.89/7.62 fof(f27564,plain,(
% 50.89/7.62 (?[VarCurr]: (reachableState(VarCurr)&~v4(VarCurr)))),
% 50.89/7.62 inference(pre_NNF_transformation,[status(thm)],[f448])).
% 50.89/7.62 fof(f27565,plain,(
% 50.89/7.62 (reachableState(sK0_skl)&~v4(sK0_skl))),
% 50.89/7.62 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f27564])).
% 50.89/7.62 fof(f27567,plain,(
% 50.89/7.62 ~v4(sK0_skl)),
% 50.89/7.62 inference(cnf_transformation,[status(thm)],[f27565])).
% 50.89/7.62 fof(f27568,plain,(
% 50.89/7.62 ![VarCurr]: ((v4(VarCurr)|v22287(VarCurr))&(~v4(VarCurr)|~v22287(VarCurr)))),
% 50.89/7.62 inference(NNF_transformation,[status(thm)],[f449])).
% 50.89/7.62 fof(f27569,plain,(
% 50.89/7.62 (![VarCurr]: (v4(VarCurr)|v22287(VarCurr)))&(![VarCurr]: (~v4(VarCurr)|~v22287(VarCurr)))),
% 50.89/7.62 inference(miniscoping,[status(thm)],[f27568])).
% 50.89/7.62 fof(f27570,plain,(
% 50.89/7.62 ![X0]: (v4(X0)|v22287(X0))),
% 50.89/7.62 inference(cnf_transformation,[status(thm)],[f27569])).
% 50.89/7.62 fof(f27572,plain,(
% 50.89/7.62 ![VarCurr]: ((v22287(VarCurr)|v22288(VarCurr))&(~v22287(VarCurr)|~v22288(VarCurr)))),
% 50.89/7.62 inference(NNF_transformation,[status(thm)],[f450])).
% 50.89/7.62 fof(f27573,plain,(
% 50.89/7.62 (![VarCurr]: (v22287(VarCurr)|v22288(VarCurr)))&(![VarCurr]: (~v22287(VarCurr)|~v22288(VarCurr)))),
% 50.89/7.62 inference(miniscoping,[status(thm)],[f27572])).
% 50.89/7.62 fof(f27575,plain,(
% 50.89/7.62 ![X0]: (~v22287(X0)|~v22288(X0))),
% 50.89/7.62 inference(cnf_transformation,[status(thm)],[f27573])).
% 50.89/7.62 fof(f27576,plain,(
% 50.89/7.62 ![VarCurr]: ((~v22288(VarCurr)|(v22290(VarCurr)&v22314(VarCurr)))&(v22288(VarCurr)|(~v22290(VarCurr)|~v22314(VarCurr))))),
% 50.89/7.62 inference(NNF_transformation,[status(thm)],[f451])).
% 50.89/7.62 fof(f27577,plain,(
% 50.89/7.62 (![VarCurr]: (~v22288(VarCurr)|(v22290(VarCurr)&v22314(VarCurr))))&(![VarCurr]: (v22288(VarCurr)|(~v22290(VarCurr)|~v22314(VarCurr))))),
% 50.89/7.62 inference(miniscoping,[status(thm)],[f27576])).
% 50.89/7.62 fof(f27580,plain,(
% 50.89/7.62 ![X0]: (v22288(X0)|~v22290(X0)|~v22314(X0))),
% 50.89/7.62 inference(cnf_transformation,[status(thm)],[f27577])).
% 50.89/7.62 fof(f27581,plain,(
% 50.89/7.62 ![VarCurr]: ((~v22314(VarCurr)|(v22292(VarCurr,bitIndex0)|v22292(VarCurr,bitIndex1)))&(v22314(VarCurr)|(~v22292(VarCurr,bitIndex0)&~v22292(VarCurr,bitIndex1))))),
% 50.89/7.62 inference(NNF_transformation,[status(thm)],[f452])).
% 50.89/7.62 fof(f27582,plain,(
% 50.89/7.62 (![VarCurr]: (~v22314(VarCurr)|(v22292(VarCurr,bitIndex0)|v22292(VarCurr,bitIndex1))))&(![VarCurr]: (v22314(VarCurr)|(~v22292(VarCurr,bitIndex0)&~v22292(VarCurr,bitIndex1))))),
% 50.89/7.62 inference(miniscoping,[status(thm)],[f27581])).
% 50.89/7.62 fof(f27585,plain,(
% 50.89/7.62 ![X0]: (v22314(X0)|~v22292(X0,bitIndex1))),
% 50.89/7.62 inference(cnf_transformation,[status(thm)],[f27582])).
% 50.89/7.62 fof(f27586,plain,(
% 50.89/7.62 ![VarCurr]: ((v22290(VarCurr)|v22291(VarCurr))&(~v22290(VarCurr)|~v22291(VarCurr)))),
% 50.89/7.62 inference(NNF_transformation,[status(thm)],[f453])).
% 50.89/7.62 fof(f27587,plain,(
% 50.89/7.62 (![VarCurr]: (v22290(VarCurr)|v22291(VarCurr)))&(![VarCurr]: (~v22290(VarCurr)|~v22291(VarCurr)))),
% 50.89/7.62 inference(miniscoping,[status(thm)],[f27586])).
% 50.89/7.62 fof(f27588,plain,(
% 50.89/7.62 ![X0]: (v22290(X0)|v22291(X0))),
% 50.89/7.62 inference(cnf_transformation,[status(thm)],[f27587])).
% 50.89/7.62 fof(f27590,plain,(
% 50.89/7.62 ![VarCurr]: ((~v22291(VarCurr)|(v22292(VarCurr,bitIndex0)&v22292(VarCurr,bitIndex1)))&(v22291(VarCurr)|(~v22292(VarCurr,bitIndex0)|~v22292(VarCurr,bitIndex1))))),
% 50.89/7.62 inference(NNF_transformation,[status(thm)],[f454])).
% 50.89/7.62 fof(f27591,plain,(
% 50.89/7.62 (![VarCurr]: (~v22291(VarCurr)|(v22292(VarCurr,bitIndex0)&v22292(VarCurr,bitIndex1))))&(![VarCurr]: (v22291(VarCurr)|(~v22292(VarCurr,bitIndex0)|~v22292(VarCurr,bitIndex1))))),
% 50.89/7.62 inference(miniscoping,[status(thm)],[f27590])).
% 50.89/7.62 fof(f27592,plain,(
% 50.89/7.62 ![X0]: (~v22291(X0)|v22292(X0,bitIndex0))),
% 50.89/7.62 inference(cnf_transformation,[status(thm)],[f27591])).
% 50.89/7.62 fof(f27595,plain,(
% 50.89/7.62 ![VarCurr]: ((~v22292(VarCurr,bitIndex0)|v22293(VarCurr))&(v22292(VarCurr,bitIndex0)|~v22293(VarCurr)))),
% 50.89/7.62 inference(NNF_transformation,[status(thm)],[f455])).
% 50.89/7.62 fof(f27596,plain,(
% 50.89/7.62 (![VarCurr]: (~v22292(VarCurr,bitIndex0)|v22293(VarCurr)))&(![VarCurr]: (v22292(VarCurr,bitIndex0)|~v22293(VarCurr)))),
% 50.89/7.62 inference(miniscoping,[status(thm)],[f27595])).
% 50.89/7.62 fof(f27597,plain,(
% 50.89/7.62 ![X0]: (~v22292(X0,bitIndex0)|v22293(X0))),
% 50.89/7.62 inference(cnf_transformation,[status(thm)],[f27596])).
% 50.89/7.62 fof(f27599,plain,(
% 50.89/7.62 ![VarCurr]: ((~v22292(VarCurr,bitIndex1)|$true)&(v22292(VarCurr,bitIndex1)|$false))),
% 50.89/7.62 inference(NNF_transformation,[status(thm)],[f456])).
% 50.89/7.62 fof(f27600,plain,(
% 50.89/7.62 ((![VarCurr]: ~v22292(VarCurr,bitIndex1))|$true)&((![VarCurr]: v22292(VarCurr,bitIndex1))|$false)),
% 50.89/7.62 inference(miniscoping,[status(thm)],[f27599])).
% 50.89/7.62 fof(f27601,plain,(
% 50.89/7.62 ![VarCurr]: v22292(VarCurr,bitIndex1)),
% 50.89/7.62 inference(true_and_false_simplification,[status(thm)],[f27600])).
% 50.89/7.62 fof(f27602,plain,(
% 50.89/7.62 ![X0]: (v22292(X0,bitIndex1))),
% 50.89/7.62 inference(cnf_transformation,[status(thm)],[f27601])).
% 50.89/7.62 fof(f27603,plain,(
% 50.89/7.62 ![VarCurr]: ((~v22293(VarCurr)|(v22295(VarCurr)&v22296(VarCurr,bitIndex9)))&(v22293(VarCurr)|(~v22295(VarCurr)|~v22296(VarCurr,bitIndex9))))),
% 50.89/7.62 inference(NNF_transformation,[status(thm)],[f457])).
% 50.89/7.62 fof(f27604,plain,(
% 50.89/7.62 (![VarCurr]: (~v22293(VarCurr)|(v22295(VarCurr)&v22296(VarCurr,bitIndex9))))&(![VarCurr]: (v22293(VarCurr)|(~v22295(VarCurr)|~v22296(VarCurr,bitIndex9))))),
% 50.89/7.62 inference(miniscoping,[status(thm)],[f27603])).
% 50.89/7.62 fof(f27606,plain,(
% 50.89/7.62 ![X0]: (~v22293(X0)|v22296(X0,bitIndex9))),
% 50.89/7.62 inference(cnf_transformation,[status(thm)],[f27604])).
% 50.89/7.62 fof(f27698,plain,(
% 50.89/7.62 ![X0]: (~v22296(X0,bitIndex9))),
% 50.89/7.62 inference(cnf_transformation,[status(thm)],[f481])).
% 50.89/7.62 fof(f185881,plain,(
% 50.89/7.62 v22287(sK0_skl)),
% 50.89/7.62 inference(resolution,[status(thm)],[f27570,f27567])).
% 50.89/7.62 fof(f185968,plain,(
% 50.89/7.62 ~v22288(sK0_skl)),
% 50.89/7.62 inference(resolution,[status(thm)],[f27575,f185881])).
% 50.89/7.62 fof(f185974,plain,(
% 50.89/7.62 ![X0]: (v22314(X0))),
% 50.89/7.62 inference(backward_subsumption_resolution,[status(thm)],[f27585,f27602])).
% 50.89/7.62 fof(f185975,plain,(
% 50.89/7.62 ![X0]: (v22288(X0)|~v22290(X0))),
% 50.89/7.62 inference(backward_subsumption_resolution,[status(thm)],[f27580,f185974])).
% 50.89/7.62 fof(f185997,plain,(
% 50.89/7.62 ![X0]: (~v22293(X0))),
% 50.89/7.62 inference(backward_subsumption_resolution,[status(thm)],[f27606,f27698])).
% 50.89/7.62 fof(f185999,plain,(
% 50.89/7.62 ![X0]: (~v22292(X0,bitIndex0))),
% 50.89/7.62 inference(backward_subsumption_resolution,[status(thm)],[f27597,f185997])).
% 50.89/7.62 fof(f187453,plain,(
% 50.89/7.62 ![X0]: (~v22291(X0))),
% 50.89/7.62 inference(backward_subsumption_resolution,[status(thm)],[f27592,f185999])).
% 50.89/7.62 fof(f187454,plain,(
% 50.89/7.62 ![X0]: (v22290(X0))),
% 50.89/7.62 inference(backward_subsumption_resolution,[status(thm)],[f27588,f187453])).
% 50.89/7.62 fof(f216641,plain,(
% 50.89/7.62 ![X0]: (v22288(X0))),
% 50.89/7.62 inference(forward_subsumption_resolution,[status(thm)],[f185975,f187454])).
% 28.04/8.20 fof(f216642,plain,(
% 28.04/8.20 $false),
% 28.04/8.20 inference(backward_subsumption_resolution,[status(thm)],[f185968,f216641])).
% 28.04/8.20 % SZS output end CNFRefutation for theBenchmark.p
% 2.39/8.28 % Elapsed time: 7.813978 seconds
% 2.39/8.28 % CPU time: 51.683509 seconds
% 2.39/8.28 % Total memory used: 3.621 GB
% 2.39/8.28 % Net memory used: 3.616 GB
%------------------------------------------------------------------------------