%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV090+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 : n009.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 140.13s 21.13s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV090+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.38 % Computer : n009.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:18:59 UTC 2026
% 0.10/0.38 % CPUTime :
% 3.55/3.86 % Drodi V4.1.1
% 140.13/21.13 % Refutation found
% 140.13/21.13 % SZS status Theorem for theBenchmark: Theorem is valid
% 140.13/21.13 % SZS output start CNFRefutation for theBenchmark
% 140.13/21.13 fof(f1199,conjecture,(
% 140.13/21.13 (! [VarCurr] :( reachableState(VarCurr)=> v4(VarCurr) ) )),
% 140.13/21.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.13/21.13 fof(f1200,negated_conjecture,(
% 140.13/21.13 ~((! [VarCurr] :( reachableState(VarCurr)=> v4(VarCurr) ) ))),
% 140.13/21.13 inference(negated_conjecture,[status(cth)],[f1199])).
% 140.13/21.13 fof(f1201,axiom,(
% 140.13/21.13 (! [VarCurr] :( ~ v4(VarCurr)<=> v30850(VarCurr) ) )),
% 140.13/21.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.13/21.13 fof(f1202,axiom,(
% 140.13/21.13 (! [VarCurr] :( ~ v30850(VarCurr)<=> v30851(VarCurr) ) )),
% 140.13/21.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.13/21.13 fof(f1203,axiom,(
% 140.13/21.13 (! [VarCurr] :( v30851(VarCurr)<=> ( v30853(VarCurr)& v30869(VarCurr) ) ) )),
% 140.13/21.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.13/21.13 fof(f1204,axiom,(
% 140.13/21.13 (! [VarCurr] :( v30869(VarCurr)<=> ( v30855(VarCurr,bitIndex0)| v30855(VarCurr,bitIndex1) ) ) )),
% 140.13/21.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.13/21.14 fof(f1205,axiom,(
% 140.13/21.14 (! [VarCurr] :( ~ v30853(VarCurr)<=> v30854(VarCurr) ) )),
% 140.13/21.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.13/21.14 fof(f1206,axiom,(
% 140.13/21.14 (! [VarCurr] :( v30854(VarCurr)<=> ( v30855(VarCurr,bitIndex0)& v30855(VarCurr,bitIndex1) ) ) )),
% 140.13/21.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.13/21.14 fof(f1207,axiom,(
% 140.13/21.14 (! [VarCurr] :( v30855(VarCurr,bitIndex0)<=> v30856(VarCurr) ) )),
% 140.13/21.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.13/21.14 fof(f1208,axiom,(
% 140.13/21.14 (! [VarCurr] :( v30855(VarCurr,bitIndex1)<=> $true ) )),
% 140.13/21.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.13/21.14 fof(f1209,axiom,(
% 140.13/21.14 (! [VarCurr] :( v30856(VarCurr)<=> ( v30858(VarCurr)& v30860(VarCurr,bitIndex5) ) ) )),
% 140.13/21.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.13/21.14 fof(f1222,axiom,(
% 140.13/21.14 (! [VarCurr] : ~ v30860(VarCurr,bitIndex5) )),
% 140.13/21.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 140.13/21.14 fof(f43712,plain,(
% 140.13/21.14 (?[VarCurr]: (reachableState(VarCurr)&~v4(VarCurr)))),
% 140.13/21.14 inference(pre_NNF_transformation,[status(thm)],[f1200])).
% 140.13/21.14 fof(f43713,plain,(
% 140.13/21.14 (reachableState(sK0_skl)&~v4(sK0_skl))),
% 140.13/21.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f43712])).
% 140.13/21.14 fof(f43715,plain,(
% 140.13/21.14 ~v4(sK0_skl)),
% 140.13/21.14 inference(cnf_transformation,[status(thm)],[f43713])).
% 140.13/21.14 fof(f43716,plain,(
% 140.13/21.14 ![VarCurr]: ((v4(VarCurr)|v30850(VarCurr))&(~v4(VarCurr)|~v30850(VarCurr)))),
% 140.13/21.14 inference(NNF_transformation,[status(thm)],[f1201])).
% 140.13/21.14 fof(f43717,plain,(
% 140.13/21.14 (![VarCurr]: (v4(VarCurr)|v30850(VarCurr)))&(![VarCurr]: (~v4(VarCurr)|~v30850(VarCurr)))),
% 140.13/21.14 inference(miniscoping,[status(thm)],[f43716])).
% 140.13/21.14 fof(f43718,plain,(
% 140.13/21.14 ![X0]: (v4(X0)|v30850(X0))),
% 140.13/21.14 inference(cnf_transformation,[status(thm)],[f43717])).
% 140.13/21.14 fof(f43720,plain,(
% 140.13/21.14 ![VarCurr]: ((v30850(VarCurr)|v30851(VarCurr))&(~v30850(VarCurr)|~v30851(VarCurr)))),
% 140.13/21.14 inference(NNF_transformation,[status(thm)],[f1202])).
% 140.13/21.14 fof(f43721,plain,(
% 140.13/21.14 (![VarCurr]: (v30850(VarCurr)|v30851(VarCurr)))&(![VarCurr]: (~v30850(VarCurr)|~v30851(VarCurr)))),
% 140.13/21.14 inference(miniscoping,[status(thm)],[f43720])).
% 140.13/21.14 fof(f43723,plain,(
% 140.13/21.14 ![X0]: (~v30850(X0)|~v30851(X0))),
% 140.13/21.14 inference(cnf_transformation,[status(thm)],[f43721])).
% 140.13/21.14 fof(f43724,plain,(
% 140.13/21.14 ![VarCurr]: ((~v30851(VarCurr)|(v30853(VarCurr)&v30869(VarCurr)))&(v30851(VarCurr)|(~v30853(VarCurr)|~v30869(VarCurr))))),
% 140.13/21.14 inference(NNF_transformation,[status(thm)],[f1203])).
% 140.13/21.14 fof(f43725,plain,(
% 140.13/21.14 (![VarCurr]: (~v30851(VarCurr)|(v30853(VarCurr)&v30869(VarCurr))))&(![VarCurr]: (v30851(VarCurr)|(~v30853(VarCurr)|~v30869(VarCurr))))),
% 140.13/21.14 inference(miniscoping,[status(thm)],[f43724])).
% 140.13/21.14 fof(f43728,plain,(
% 140.13/21.14 ![X0]: (v30851(X0)|~v30853(X0)|~v30869(X0))),
% 140.13/21.14 inference(cnf_transformation,[status(thm)],[f43725])).
% 140.13/21.14 fof(f43729,plain,(
% 140.13/21.14 ![VarCurr]: ((~v30869(VarCurr)|(v30855(VarCurr,bitIndex0)|v30855(VarCurr,bitIndex1)))&(v30869(VarCurr)|(~v30855(VarCurr,bitIndex0)&~v30855(VarCurr,bitIndex1))))),
% 140.13/21.14 inference(NNF_transformation,[status(thm)],[f1204])).
% 140.13/21.14 fof(f43730,plain,(
% 140.13/21.14 (![VarCurr]: (~v30869(VarCurr)|(v30855(VarCurr,bitIndex0)|v30855(VarCurr,bitIndex1))))&(![VarCurr]: (v30869(VarCurr)|(~v30855(VarCurr,bitIndex0)&~v30855(VarCurr,bitIndex1))))),
% 140.13/21.14 inference(miniscoping,[status(thm)],[f43729])).
% 140.13/21.14 fof(f43733,plain,(
% 140.13/21.14 ![X0]: (v30869(X0)|~v30855(X0,bitIndex1))),
% 140.13/21.14 inference(cnf_transformation,[status(thm)],[f43730])).
% 140.13/21.14 fof(f43734,plain,(
% 140.13/21.14 ![VarCurr]: ((v30853(VarCurr)|v30854(VarCurr))&(~v30853(VarCurr)|~v30854(VarCurr)))),
% 140.13/21.14 inference(NNF_transformation,[status(thm)],[f1205])).
% 140.13/21.14 fof(f43735,plain,(
% 140.13/21.14 (![VarCurr]: (v30853(VarCurr)|v30854(VarCurr)))&(![VarCurr]: (~v30853(VarCurr)|~v30854(VarCurr)))),
% 140.13/21.14 inference(miniscoping,[status(thm)],[f43734])).
% 140.13/21.14 fof(f43736,plain,(
% 140.13/21.14 ![X0]: (v30853(X0)|v30854(X0))),
% 140.13/21.14 inference(cnf_transformation,[status(thm)],[f43735])).
% 140.13/21.14 fof(f43738,plain,(
% 140.13/21.14 ![VarCurr]: ((~v30854(VarCurr)|(v30855(VarCurr,bitIndex0)&v30855(VarCurr,bitIndex1)))&(v30854(VarCurr)|(~v30855(VarCurr,bitIndex0)|~v30855(VarCurr,bitIndex1))))),
% 140.13/21.14 inference(NNF_transformation,[status(thm)],[f1206])).
% 140.13/21.14 fof(f43739,plain,(
% 140.13/21.14 (![VarCurr]: (~v30854(VarCurr)|(v30855(VarCurr,bitIndex0)&v30855(VarCurr,bitIndex1))))&(![VarCurr]: (v30854(VarCurr)|(~v30855(VarCurr,bitIndex0)|~v30855(VarCurr,bitIndex1))))),
% 140.13/21.14 inference(miniscoping,[status(thm)],[f43738])).
% 140.13/21.14 fof(f43740,plain,(
% 140.13/21.14 ![X0]: (~v30854(X0)|v30855(X0,bitIndex0))),
% 140.13/21.14 inference(cnf_transformation,[status(thm)],[f43739])).
% 140.13/21.14 fof(f43743,plain,(
% 140.13/21.14 ![VarCurr]: ((~v30855(VarCurr,bitIndex0)|v30856(VarCurr))&(v30855(VarCurr,bitIndex0)|~v30856(VarCurr)))),
% 140.13/21.14 inference(NNF_transformation,[status(thm)],[f1207])).
% 140.13/21.14 fof(f43744,plain,(
% 140.13/21.14 (![VarCurr]: (~v30855(VarCurr,bitIndex0)|v30856(VarCurr)))&(![VarCurr]: (v30855(VarCurr,bitIndex0)|~v30856(VarCurr)))),
% 140.13/21.14 inference(miniscoping,[status(thm)],[f43743])).
% 140.13/21.14 fof(f43745,plain,(
% 140.13/21.14 ![X0]: (~v30855(X0,bitIndex0)|v30856(X0))),
% 140.13/21.14 inference(cnf_transformation,[status(thm)],[f43744])).
% 140.13/21.14 fof(f43747,plain,(
% 140.13/21.14 ![VarCurr]: ((~v30855(VarCurr,bitIndex1)|$true)&(v30855(VarCurr,bitIndex1)|$false))),
% 140.13/21.14 inference(NNF_transformation,[status(thm)],[f1208])).
% 140.13/21.14 fof(f43748,plain,(
% 140.13/21.14 ((![VarCurr]: ~v30855(VarCurr,bitIndex1))|$true)&((![VarCurr]: v30855(VarCurr,bitIndex1))|$false)),
% 140.13/21.14 inference(miniscoping,[status(thm)],[f43747])).
% 140.13/21.14 fof(f43749,plain,(
% 140.13/21.14 ![VarCurr]: v30855(VarCurr,bitIndex1)),
% 140.13/21.14 inference(true_and_false_simplification,[status(thm)],[f43748])).
% 140.13/21.14 fof(f43750,plain,(
% 140.13/21.14 ![X0]: (v30855(X0,bitIndex1))),
% 140.13/21.14 inference(cnf_transformation,[status(thm)],[f43749])).
% 140.13/21.14 fof(f43751,plain,(
% 140.13/21.14 ![VarCurr]: ((~v30856(VarCurr)|(v30858(VarCurr)&v30860(VarCurr,bitIndex5)))&(v30856(VarCurr)|(~v30858(VarCurr)|~v30860(VarCurr,bitIndex5))))),
% 140.13/21.14 inference(NNF_transformation,[status(thm)],[f1209])).
% 140.13/21.14 fof(f43752,plain,(
% 140.13/21.14 (![VarCurr]: (~v30856(VarCurr)|(v30858(VarCurr)&v30860(VarCurr,bitIndex5))))&(![VarCurr]: (v30856(VarCurr)|(~v30858(VarCurr)|~v30860(VarCurr,bitIndex5))))),
% 140.13/21.14 inference(miniscoping,[status(thm)],[f43751])).
% 140.13/21.14 fof(f43754,plain,(
% 140.13/21.14 ![X0]: (~v30856(X0)|v30860(X0,bitIndex5))),
% 140.13/21.14 inference(cnf_transformation,[status(thm)],[f43752])).
% 140.13/21.14 fof(f43805,plain,(
% 140.13/21.14 ![X0]: (~v30860(X0,bitIndex5))),
% 140.13/21.14 inference(cnf_transformation,[status(thm)],[f1222])).
% 140.13/21.14 fof(f304126,plain,(
% 140.13/21.14 v30850(sK0_skl)),
% 140.13/21.14 inference(resolution,[status(thm)],[f43718,f43715])).
% 140.13/21.14 fof(f304251,plain,(
% 140.13/21.14 ~v30851(sK0_skl)),
% 140.13/21.14 inference(resolution,[status(thm)],[f43723,f304126])).
% 140.13/21.14 fof(f304257,plain,(
% 140.13/21.14 ![X0]: (v30869(X0))),
% 140.13/21.14 inference(backward_subsumption_resolution,[status(thm)],[f43733,f43750])).
% 140.13/21.14 fof(f304258,plain,(
% 140.13/21.14 ![X0]: (v30851(X0)|~v30853(X0))),
% 140.13/21.14 inference(backward_subsumption_resolution,[status(thm)],[f43728,f304257])).
% 140.13/21.14 fof(f304268,plain,(
% 140.13/21.14 ![X0]: (~v30856(X0))),
% 140.13/21.14 inference(backward_subsumption_resolution,[status(thm)],[f43754,f43805])).
% 140.13/21.14 fof(f304271,plain,(
% 140.13/21.14 ![X0]: (~v30855(X0,bitIndex0))),
% 140.13/21.14 inference(backward_subsumption_resolution,[status(thm)],[f43745,f304268])).
% 140.13/21.14 fof(f305061,plain,(
% 140.13/21.14 ![X0]: (~v30854(X0))),
% 140.13/21.14 inference(backward_subsumption_resolution,[status(thm)],[f43740,f304271])).
% 140.13/21.14 fof(f305062,plain,(
% 140.13/21.14 ![X0]: (v30853(X0))),
% 140.13/21.14 inference(backward_subsumption_resolution,[status(thm)],[f43736,f305061])).
% 140.13/21.14 fof(f337794,plain,(
% 140.13/21.14 ![X0]: (v30851(X0))),
% 140.13/21.14 inference(forward_subsumption_resolution,[status(thm)],[f304258,f305062])).
% 12.20/22.04 fof(f337795,plain,(
% 12.20/22.04 $false),
% 12.20/22.04 inference(backward_subsumption_resolution,[status(thm)],[f304251,f337794])).
% 12.20/22.04 % SZS output end CNFRefutation for theBenchmark.p
% 7.91/22.11 % Elapsed time: 21.652009 seconds
% 7.91/22.11 % CPU time: 141.365538 seconds
% 7.91/22.11 % Total memory used: 5.876 GB
% 7.91/22.11 % Net memory used: 5.859 GB
%------------------------------------------------------------------------------