%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV095+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 : n016.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:05 PM UTC 2026
% Result : Theorem 0.17s 0.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV095+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.40 % Computer : n016.cluster.edu
% 0.10/0.40 % Model : x86_64 x86_64
% 0.10/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.40 % Memory : 8046.5625MB
% 0.10/0.40 % OS : Linux 6.8.0-71-generic
% 0.10/0.40 % CPULimit : 300
% 0.10/0.40 % WCLimit : 300
% 0.10/0.40 % DateTime : Sun Sep 20 21:25:08 UTC 2026
% 0.10/0.40 % CPUTime :
% 0.17/0.49 % Drodi V4.1.1
% 0.17/0.65 % Refutation found
% 0.17/0.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.17/0.65 % SZS output start CNFRefutation for theBenchmark
% 0.17/0.65 fof(f35,conjecture,(
% 0.17/0.65 (! [VarCurr] :( reachableState(VarCurr)=> v4(VarCurr) ) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f36,negated_conjecture,(
% 0.17/0.65 ~((! [VarCurr] :( reachableState(VarCurr)=> v4(VarCurr) ) ))),
% 0.17/0.65 inference(negated_conjecture,[status(cth)],[f35])).
% 0.17/0.65 fof(f37,axiom,(
% 0.17/0.65 (! [VarCurr] :( ~ v4(VarCurr)<=> v995(VarCurr) ) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f38,axiom,(
% 0.17/0.65 (! [VarCurr] :( ~ v995(VarCurr)<=> v996(VarCurr) ) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f39,axiom,(
% 0.17/0.65 (! [VarCurr] :( v996(VarCurr)<=> ( v998(VarCurr)& v1010(VarCurr) ) ) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f40,axiom,(
% 0.17/0.65 (! [VarCurr] :( v1010(VarCurr)<=> ( v1000(VarCurr,bitIndex0)| v1000(VarCurr,bitIndex1) ) ) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f41,axiom,(
% 0.17/0.65 (! [VarCurr] :( ~ v998(VarCurr)<=> v999(VarCurr) ) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f42,axiom,(
% 0.17/0.65 (! [VarCurr] :( v999(VarCurr)<=> ( v1000(VarCurr,bitIndex0)& v1000(VarCurr,bitIndex1) ) ) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f43,axiom,(
% 0.17/0.65 (! [VarCurr] :( v1000(VarCurr,bitIndex0)<=> v1001(VarCurr) ) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f44,axiom,(
% 0.17/0.65 (! [VarCurr] :( v1000(VarCurr,bitIndex1)<=> $true ) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f45,axiom,(
% 0.17/0.65 (! [VarCurr] :( v1001(VarCurr)<=> ( v1003(VarCurr)& v1007(VarCurr,bitIndex5) ) ) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f53,axiom,(
% 0.17/0.65 (! [VarCurr] : ~ v1007(VarCurr,bitIndex5) )),
% 0.17/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.17/0.65 fof(f1198,plain,(
% 0.17/0.65 (?[VarCurr]: (reachableState(VarCurr)&~v4(VarCurr)))),
% 0.17/0.65 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.17/0.65 fof(f1199,plain,(
% 0.17/0.65 (reachableState(sK0_skl)&~v4(sK0_skl))),
% 0.17/0.65 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f1198])).
% 0.17/0.65 fof(f1201,plain,(
% 0.17/0.65 ~v4(sK0_skl)),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f1199])).
% 0.17/0.65 fof(f1202,plain,(
% 0.17/0.65 ![VarCurr]: ((v4(VarCurr)|v995(VarCurr))&(~v4(VarCurr)|~v995(VarCurr)))),
% 0.17/0.65 inference(NNF_transformation,[status(thm)],[f37])).
% 0.17/0.65 fof(f1203,plain,(
% 0.17/0.65 (![VarCurr]: (v4(VarCurr)|v995(VarCurr)))&(![VarCurr]: (~v4(VarCurr)|~v995(VarCurr)))),
% 0.17/0.65 inference(miniscoping,[status(thm)],[f1202])).
% 0.17/0.65 fof(f1204,plain,(
% 0.17/0.65 ![X0]: (v4(X0)|v995(X0))),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f1203])).
% 0.17/0.65 fof(f1206,plain,(
% 0.17/0.65 ![VarCurr]: ((v995(VarCurr)|v996(VarCurr))&(~v995(VarCurr)|~v996(VarCurr)))),
% 0.17/0.65 inference(NNF_transformation,[status(thm)],[f38])).
% 0.17/0.65 fof(f1207,plain,(
% 0.17/0.65 (![VarCurr]: (v995(VarCurr)|v996(VarCurr)))&(![VarCurr]: (~v995(VarCurr)|~v996(VarCurr)))),
% 0.17/0.65 inference(miniscoping,[status(thm)],[f1206])).
% 0.17/0.65 fof(f1209,plain,(
% 0.17/0.65 ![X0]: (~v995(X0)|~v996(X0))),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f1207])).
% 0.17/0.65 fof(f1210,plain,(
% 0.17/0.65 ![VarCurr]: ((~v996(VarCurr)|(v998(VarCurr)&v1010(VarCurr)))&(v996(VarCurr)|(~v998(VarCurr)|~v1010(VarCurr))))),
% 0.17/0.65 inference(NNF_transformation,[status(thm)],[f39])).
% 0.17/0.65 fof(f1211,plain,(
% 0.17/0.65 (![VarCurr]: (~v996(VarCurr)|(v998(VarCurr)&v1010(VarCurr))))&(![VarCurr]: (v996(VarCurr)|(~v998(VarCurr)|~v1010(VarCurr))))),
% 0.17/0.65 inference(miniscoping,[status(thm)],[f1210])).
% 0.17/0.65 fof(f1214,plain,(
% 0.17/0.65 ![X0]: (v996(X0)|~v998(X0)|~v1010(X0))),
% 0.17/0.65 inference(cnf_transformation,[status(thm)],[f1211])).
% 0.17/0.65 fof(f1215,plain,(
% 0.17/0.65 ![VarCurr]: ((~v1010(VarCurr)|(v1000(VarCurr,bitIndex0)|v1000(VarCurr,bitIndex1)))&(v1010(VarCurr)|(~v1000(VarCurr,bitIndex0)&~v1000(VarCurr,bitIndex1))))),
% 0.17/0.65 inference(NNF_transformation,[status(thm)],[f40])).
% 0.17/0.65 fof(f1216,plain,(
% 0.17/0.65 (![VarCurr]: (~v1010(VarCurr)|(v1000(VarCurr,bitIndex0)|v1000(VarCurr,bitIndex1))))&(![VarCurr]: (v1010(VarCurr)|(~v1000(VarCurr,bitIndex0)&~v1000(VarCurr,bitIndex1))))),
% 0.17/0.65 inference(miniscoping,[status(thm)],[f1215])).
% 0.17/0.65 fof(f1219,plain,(
% 1.02/0.68 ![X0]: (v1010(X0)|~v1000(X0,bitIndex1))),
% 1.02/0.68 inference(cnf_transformation,[status(thm)],[f1216])).
% 1.02/0.68 fof(f1220,plain,(
% 1.02/0.68 ![VarCurr]: ((v998(VarCurr)|v999(VarCurr))&(~v998(VarCurr)|~v999(VarCurr)))),
% 1.02/0.68 inference(NNF_transformation,[status(thm)],[f41])).
% 1.02/0.68 fof(f1221,plain,(
% 1.02/0.68 (![VarCurr]: (v998(VarCurr)|v999(VarCurr)))&(![VarCurr]: (~v998(VarCurr)|~v999(VarCurr)))),
% 1.02/0.68 inference(miniscoping,[status(thm)],[f1220])).
% 1.02/0.68 fof(f1222,plain,(
% 1.02/0.68 ![X0]: (v998(X0)|v999(X0))),
% 1.02/0.68 inference(cnf_transformation,[status(thm)],[f1221])).
% 1.02/0.68 fof(f1224,plain,(
% 1.02/0.68 ![VarCurr]: ((~v999(VarCurr)|(v1000(VarCurr,bitIndex0)&v1000(VarCurr,bitIndex1)))&(v999(VarCurr)|(~v1000(VarCurr,bitIndex0)|~v1000(VarCurr,bitIndex1))))),
% 1.02/0.68 inference(NNF_transformation,[status(thm)],[f42])).
% 1.02/0.68 fof(f1225,plain,(
% 1.02/0.68 (![VarCurr]: (~v999(VarCurr)|(v1000(VarCurr,bitIndex0)&v1000(VarCurr,bitIndex1))))&(![VarCurr]: (v999(VarCurr)|(~v1000(VarCurr,bitIndex0)|~v1000(VarCurr,bitIndex1))))),
% 1.02/0.68 inference(miniscoping,[status(thm)],[f1224])).
% 1.02/0.68 fof(f1226,plain,(
% 1.02/0.68 ![X0]: (~v999(X0)|v1000(X0,bitIndex0))),
% 1.02/0.68 inference(cnf_transformation,[status(thm)],[f1225])).
% 1.02/0.68 fof(f1229,plain,(
% 1.02/0.68 ![VarCurr]: ((~v1000(VarCurr,bitIndex0)|v1001(VarCurr))&(v1000(VarCurr,bitIndex0)|~v1001(VarCurr)))),
% 1.02/0.68 inference(NNF_transformation,[status(thm)],[f43])).
% 1.02/0.68 fof(f1230,plain,(
% 1.02/0.68 (![VarCurr]: (~v1000(VarCurr,bitIndex0)|v1001(VarCurr)))&(![VarCurr]: (v1000(VarCurr,bitIndex0)|~v1001(VarCurr)))),
% 1.02/0.68 inference(miniscoping,[status(thm)],[f1229])).
% 1.02/0.68 fof(f1231,plain,(
% 1.02/0.68 ![X0]: (~v1000(X0,bitIndex0)|v1001(X0))),
% 1.02/0.68 inference(cnf_transformation,[status(thm)],[f1230])).
% 1.02/0.68 fof(f1233,plain,(
% 1.02/0.68 ![VarCurr]: ((~v1000(VarCurr,bitIndex1)|$true)&(v1000(VarCurr,bitIndex1)|$false))),
% 1.02/0.68 inference(NNF_transformation,[status(thm)],[f44])).
% 1.02/0.68 fof(f1234,plain,(
% 1.02/0.68 ((![VarCurr]: ~v1000(VarCurr,bitIndex1))|$true)&((![VarCurr]: v1000(VarCurr,bitIndex1))|$false)),
% 1.02/0.68 inference(miniscoping,[status(thm)],[f1233])).
% 1.02/0.68 fof(f1235,plain,(
% 1.02/0.68 ![VarCurr]: v1000(VarCurr,bitIndex1)),
% 1.02/0.68 inference(true_and_false_simplification,[status(thm)],[f1234])).
% 1.02/0.68 fof(f1236,plain,(
% 1.02/0.68 ![X0]: (v1000(X0,bitIndex1))),
% 1.02/0.68 inference(cnf_transformation,[status(thm)],[f1235])).
% 1.02/0.68 fof(f1237,plain,(
% 1.02/0.68 ![VarCurr]: ((~v1001(VarCurr)|(v1003(VarCurr)&v1007(VarCurr,bitIndex5)))&(v1001(VarCurr)|(~v1003(VarCurr)|~v1007(VarCurr,bitIndex5))))),
% 1.02/0.68 inference(NNF_transformation,[status(thm)],[f45])).
% 1.02/0.68 fof(f1238,plain,(
% 1.02/0.68 (![VarCurr]: (~v1001(VarCurr)|(v1003(VarCurr)&v1007(VarCurr,bitIndex5))))&(![VarCurr]: (v1001(VarCurr)|(~v1003(VarCurr)|~v1007(VarCurr,bitIndex5))))),
% 1.02/0.68 inference(miniscoping,[status(thm)],[f1237])).
% 1.02/0.68 fof(f1240,plain,(
% 1.02/0.68 ![X0]: (~v1001(X0)|v1007(X0,bitIndex5))),
% 1.02/0.68 inference(cnf_transformation,[status(thm)],[f1238])).
% 1.02/0.68 fof(f1272,plain,(
% 1.02/0.68 ![X0]: (~v1007(X0,bitIndex5))),
% 1.02/0.68 inference(cnf_transformation,[status(thm)],[f53])).
% 1.02/0.68 fof(f7119,plain,(
% 1.02/0.68 ![X0]: (v1010(X0))),
% 1.02/0.68 inference(backward_subsumption_resolution,[status(thm)],[f1219,f1236])).
% 1.02/0.68 fof(f7120,plain,(
% 1.02/0.68 ![X0]: (v996(X0)|~v998(X0))),
% 1.02/0.68 inference(backward_subsumption_resolution,[status(thm)],[f1214,f7119])).
% 1.02/0.68 fof(f7124,plain,(
% 1.02/0.68 ![X0]: (~v1001(X0))),
% 1.02/0.68 inference(backward_subsumption_resolution,[status(thm)],[f1240,f1272])).
% 1.02/0.68 fof(f7126,plain,(
% 1.02/0.68 ![X0]: (~v1000(X0,bitIndex0))),
% 1.02/0.68 inference(backward_subsumption_resolution,[status(thm)],[f1231,f7124])).
% 1.02/0.68 fof(f7213,plain,(
% 1.02/0.68 ![X0]: (~v999(X0))),
% 1.02/0.68 inference(backward_subsumption_resolution,[status(thm)],[f1226,f7126])).
% 1.02/0.68 fof(f7214,plain,(
% 1.02/0.68 ![X0]: (v998(X0))),
% 1.02/0.68 inference(backward_subsumption_resolution,[status(thm)],[f1222,f7213])).
% 1.02/0.68 fof(f7698,plain,(
% 1.02/0.68 ![X0]: (~v995(X0))),
% 1.02/0.68 inference(backward_subsumption_resolution,[status(thm)],[f1209,f7699])).
% 1.02/0.68 fof(f7699,plain,(
% 1.02/0.68 ![X0]: (v996(X0))),
% 1.02/0.68 inference(forward_subsumption_resolution,[status(thm)],[f7120,f7214])).
% 1.02/0.68 fof(f7700,plain,(
% 1.02/0.68 ![X0]: (v4(X0))),
% 1.02/0.68 inference(backward_subsumption_resolution,[status(thm)],[f1204,f7698])).
% 1.02/0.68 fof(f7702,plain,(
% 1.02/0.68 $false),
% 1.02/0.68 inference(backward_subsumption_resolution,[status(thm)],[f1201,f7700])).
% 1.02/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 1.02/0.69 % Elapsed time: 0.279456 seconds
% 1.02/0.69 % CPU time: 1.288027 seconds
% 1.02/0.69 % Total memory used: 225.939 MB
% 1.02/0.69 % Net memory used: 225.408 MB
%------------------------------------------------------------------------------