%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV093+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 : n005.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:04 PM UTC 2026
% Result : Theorem 0.12s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV093+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n005.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 21:19:24 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.12/0.40 % Drodi V4.1.1
% 0.12/0.59 % Refutation found
% 0.12/0.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.59 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.59 fof(f35,conjecture,(
% 0.12/0.59 (! [VarCurr] :( reachableState(VarCurr)=> v4(VarCurr) ) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f36,negated_conjecture,(
% 0.12/0.59 ~((! [VarCurr] :( reachableState(VarCurr)=> v4(VarCurr) ) ))),
% 0.12/0.59 inference(negated_conjecture,[status(cth)],[f35])).
% 0.12/0.59 fof(f37,axiom,(
% 0.12/0.59 (! [VarCurr] :( ~ v4(VarCurr)<=> v995(VarCurr) ) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f38,axiom,(
% 0.12/0.59 (! [VarCurr] :( ~ v995(VarCurr)<=> v996(VarCurr) ) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f39,axiom,(
% 0.12/0.59 (! [VarCurr] :( v996(VarCurr)<=> ( v998(VarCurr)& v1010(VarCurr) ) ) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f40,axiom,(
% 0.12/0.59 (! [VarCurr] :( v1010(VarCurr)<=> ( v1000(VarCurr,bitIndex0)| v1000(VarCurr,bitIndex1) ) ) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f41,axiom,(
% 0.12/0.59 (! [VarCurr] :( ~ v998(VarCurr)<=> v999(VarCurr) ) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f42,axiom,(
% 0.12/0.59 (! [VarCurr] :( v999(VarCurr)<=> ( v1000(VarCurr,bitIndex0)& v1000(VarCurr,bitIndex1) ) ) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f43,axiom,(
% 0.12/0.59 (! [VarCurr] :( v1000(VarCurr,bitIndex0)<=> v1001(VarCurr) ) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f44,axiom,(
% 0.12/0.59 (! [VarCurr] :( v1000(VarCurr,bitIndex1)<=> $true ) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f45,axiom,(
% 0.12/0.59 (! [VarCurr] :( v1001(VarCurr)<=> ( v1003(VarCurr)& v1007(VarCurr,bitIndex5) ) ) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f46,axiom,(
% 0.12/0.59 (! [VarCurr] :( v1003(VarCurr)<=> ( v1004(VarCurr)& v1007(VarCurr,bitIndex4) ) ) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f52,axiom,(
% 0.12/0.59 (! [VarCurr] : ~ v1007(VarCurr,bitIndex4) )),
% 0.12/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.59 fof(f1198,plain,(
% 0.12/0.59 (?[VarCurr]: (reachableState(VarCurr)&~v4(VarCurr)))),
% 0.12/0.59 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.12/0.59 fof(f1199,plain,(
% 0.12/0.59 (reachableState(sK0_skl)&~v4(sK0_skl))),
% 0.12/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f1198])).
% 0.12/0.59 fof(f1201,plain,(
% 0.12/0.59 ~v4(sK0_skl)),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f1199])).
% 0.12/0.59 fof(f1202,plain,(
% 0.12/0.59 ![VarCurr]: ((v4(VarCurr)|v995(VarCurr))&(~v4(VarCurr)|~v995(VarCurr)))),
% 0.12/0.59 inference(NNF_transformation,[status(thm)],[f37])).
% 0.12/0.59 fof(f1203,plain,(
% 0.12/0.59 (![VarCurr]: (v4(VarCurr)|v995(VarCurr)))&(![VarCurr]: (~v4(VarCurr)|~v995(VarCurr)))),
% 0.12/0.59 inference(miniscoping,[status(thm)],[f1202])).
% 0.12/0.59 fof(f1204,plain,(
% 0.12/0.59 ![X0]: (v4(X0)|v995(X0))),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f1203])).
% 0.12/0.59 fof(f1206,plain,(
% 0.12/0.59 ![VarCurr]: ((v995(VarCurr)|v996(VarCurr))&(~v995(VarCurr)|~v996(VarCurr)))),
% 0.12/0.59 inference(NNF_transformation,[status(thm)],[f38])).
% 0.12/0.59 fof(f1207,plain,(
% 0.12/0.59 (![VarCurr]: (v995(VarCurr)|v996(VarCurr)))&(![VarCurr]: (~v995(VarCurr)|~v996(VarCurr)))),
% 0.12/0.59 inference(miniscoping,[status(thm)],[f1206])).
% 0.12/0.59 fof(f1209,plain,(
% 0.12/0.59 ![X0]: (~v995(X0)|~v996(X0))),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f1207])).
% 0.12/0.59 fof(f1210,plain,(
% 0.12/0.59 ![VarCurr]: ((~v996(VarCurr)|(v998(VarCurr)&v1010(VarCurr)))&(v996(VarCurr)|(~v998(VarCurr)|~v1010(VarCurr))))),
% 0.12/0.59 inference(NNF_transformation,[status(thm)],[f39])).
% 0.12/0.59 fof(f1211,plain,(
% 0.12/0.59 (![VarCurr]: (~v996(VarCurr)|(v998(VarCurr)&v1010(VarCurr))))&(![VarCurr]: (v996(VarCurr)|(~v998(VarCurr)|~v1010(VarCurr))))),
% 0.12/0.59 inference(miniscoping,[status(thm)],[f1210])).
% 0.12/0.59 fof(f1214,plain,(
% 0.12/0.59 ![X0]: (v996(X0)|~v998(X0)|~v1010(X0))),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f1211])).
% 0.12/0.59 fof(f1215,plain,(
% 0.12/0.59 ![VarCurr]: ((~v1010(VarCurr)|(v1000(VarCurr,bitIndex0)|v1000(VarCurr,bitIndex1)))&(v1010(VarCurr)|(~v1000(VarCurr,bitIndex0)&~v1000(VarCurr,bitIndex1))))),
% 0.12/0.59 inference(NNF_transformation,[status(thm)],[f40])).
% 0.12/0.59 fof(f1216,plain,(
% 0.12/0.59 (![VarCurr]: (~v1010(VarCurr)|(v1000(VarCurr,bitIndex0)|v1000(VarCurr,bitIndex1))))&(![VarCurr]: (v1010(VarCurr)|(~v1000(VarCurr,bitIndex0)&~v1000(VarCurr,bitIndex1))))),
% 0.12/0.59 inference(miniscoping,[status(thm)],[f1215])).
% 0.12/0.59 fof(f1219,plain,(
% 0.12/0.59 ![X0]: (v1010(X0)|~v1000(X0,bitIndex1))),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f1216])).
% 0.12/0.59 fof(f1220,plain,(
% 0.12/0.59 ![VarCurr]: ((v998(VarCurr)|v999(VarCurr))&(~v998(VarCurr)|~v999(VarCurr)))),
% 0.12/0.59 inference(NNF_transformation,[status(thm)],[f41])).
% 0.12/0.59 fof(f1221,plain,(
% 0.12/0.59 (![VarCurr]: (v998(VarCurr)|v999(VarCurr)))&(![VarCurr]: (~v998(VarCurr)|~v999(VarCurr)))),
% 0.12/0.59 inference(miniscoping,[status(thm)],[f1220])).
% 0.12/0.59 fof(f1222,plain,(
% 0.12/0.59 ![X0]: (v998(X0)|v999(X0))),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f1221])).
% 0.12/0.59 fof(f1224,plain,(
% 0.12/0.59 ![VarCurr]: ((~v999(VarCurr)|(v1000(VarCurr,bitIndex0)&v1000(VarCurr,bitIndex1)))&(v999(VarCurr)|(~v1000(VarCurr,bitIndex0)|~v1000(VarCurr,bitIndex1))))),
% 0.12/0.59 inference(NNF_transformation,[status(thm)],[f42])).
% 0.12/0.59 fof(f1225,plain,(
% 0.12/0.59 (![VarCurr]: (~v999(VarCurr)|(v1000(VarCurr,bitIndex0)&v1000(VarCurr,bitIndex1))))&(![VarCurr]: (v999(VarCurr)|(~v1000(VarCurr,bitIndex0)|~v1000(VarCurr,bitIndex1))))),
% 0.12/0.59 inference(miniscoping,[status(thm)],[f1224])).
% 0.12/0.59 fof(f1226,plain,(
% 0.12/0.59 ![X0]: (~v999(X0)|v1000(X0,bitIndex0))),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f1225])).
% 0.12/0.59 fof(f1229,plain,(
% 0.12/0.59 ![VarCurr]: ((~v1000(VarCurr,bitIndex0)|v1001(VarCurr))&(v1000(VarCurr,bitIndex0)|~v1001(VarCurr)))),
% 0.12/0.59 inference(NNF_transformation,[status(thm)],[f43])).
% 0.12/0.59 fof(f1230,plain,(
% 0.12/0.59 (![VarCurr]: (~v1000(VarCurr,bitIndex0)|v1001(VarCurr)))&(![VarCurr]: (v1000(VarCurr,bitIndex0)|~v1001(VarCurr)))),
% 0.12/0.59 inference(miniscoping,[status(thm)],[f1229])).
% 0.12/0.59 fof(f1231,plain,(
% 0.12/0.59 ![X0]: (~v1000(X0,bitIndex0)|v1001(X0))),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f1230])).
% 0.12/0.59 fof(f1233,plain,(
% 0.12/0.59 ![VarCurr]: ((~v1000(VarCurr,bitIndex1)|$true)&(v1000(VarCurr,bitIndex1)|$false))),
% 0.12/0.59 inference(NNF_transformation,[status(thm)],[f44])).
% 0.12/0.59 fof(f1234,plain,(
% 0.12/0.59 ((![VarCurr]: ~v1000(VarCurr,bitIndex1))|$true)&((![VarCurr]: v1000(VarCurr,bitIndex1))|$false)),
% 0.12/0.59 inference(miniscoping,[status(thm)],[f1233])).
% 0.12/0.59 fof(f1235,plain,(
% 0.12/0.59 ![VarCurr]: v1000(VarCurr,bitIndex1)),
% 0.12/0.59 inference(true_and_false_simplification,[status(thm)],[f1234])).
% 0.12/0.59 fof(f1236,plain,(
% 0.12/0.59 ![X0]: (v1000(X0,bitIndex1))),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f1235])).
% 0.12/0.59 fof(f1237,plain,(
% 0.12/0.59 ![VarCurr]: ((~v1001(VarCurr)|(v1003(VarCurr)&v1007(VarCurr,bitIndex5)))&(v1001(VarCurr)|(~v1003(VarCurr)|~v1007(VarCurr,bitIndex5))))),
% 0.12/0.59 inference(NNF_transformation,[status(thm)],[f45])).
% 0.12/0.59 fof(f1238,plain,(
% 0.12/0.59 (![VarCurr]: (~v1001(VarCurr)|(v1003(VarCurr)&v1007(VarCurr,bitIndex5))))&(![VarCurr]: (v1001(VarCurr)|(~v1003(VarCurr)|~v1007(VarCurr,bitIndex5))))),
% 0.12/0.59 inference(miniscoping,[status(thm)],[f1237])).
% 0.12/0.59 fof(f1239,plain,(
% 0.12/0.59 ![X0]: (~v1001(X0)|v1003(X0))),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f1238])).
% 0.12/0.59 fof(f1242,plain,(
% 0.12/0.59 ![VarCurr]: ((~v1003(VarCurr)|(v1004(VarCurr)&v1007(VarCurr,bitIndex4)))&(v1003(VarCurr)|(~v1004(VarCurr)|~v1007(VarCurr,bitIndex4))))),
% 0.12/0.59 inference(NNF_transformation,[status(thm)],[f46])).
% 0.12/0.59 fof(f1243,plain,(
% 0.12/0.59 (![VarCurr]: (~v1003(VarCurr)|(v1004(VarCurr)&v1007(VarCurr,bitIndex4))))&(![VarCurr]: (v1003(VarCurr)|(~v1004(VarCurr)|~v1007(VarCurr,bitIndex4))))),
% 0.12/0.59 inference(miniscoping,[status(thm)],[f1242])).
% 0.12/0.59 fof(f1245,plain,(
% 0.12/0.59 ![X0]: (~v1003(X0)|v1007(X0,bitIndex4))),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f1243])).
% 0.12/0.59 fof(f1271,plain,(
% 0.12/0.59 ![X0]: (~v1007(X0,bitIndex4))),
% 0.12/0.59 inference(cnf_transformation,[status(thm)],[f52])).
% 0.12/0.59 fof(f7050,plain,(
% 0.12/0.59 v995(sK0_skl)),
% 0.12/0.59 inference(resolution,[status(thm)],[f1204,f1201])).
% 0.12/0.59 fof(f7136,plain,(
% 0.12/0.59 ~v996(sK0_skl)),
% 0.12/0.59 inference(resolution,[status(thm)],[f1209,f7050])).
% 0.12/0.59 fof(f7142,plain,(
% 0.12/0.59 ![X0]: (v1010(X0))),
% 0.12/0.59 inference(backward_subsumption_resolution,[status(thm)],[f1219,f1236])).
% 0.12/0.59 fof(f7143,plain,(
% 0.12/0.59 ![X0]: (v996(X0)|~v998(X0))),
% 0.12/0.59 inference(backward_subsumption_resolution,[status(thm)],[f1214,f7142])).
% 0.12/0.59 fof(f7146,plain,(
% 0.12/0.59 ![X0]: (~v1003(X0))),
% 0.12/0.59 inference(backward_subsumption_resolution,[status(thm)],[f1245,f1271])).
% 0.12/0.59 fof(f7147,plain,(
% 0.12/0.59 ![X0]: (~v1001(X0))),
% 0.99/0.60 inference(backward_subsumption_resolution,[status(thm)],[f1239,f7146])).
% 0.99/0.60 fof(f7148,plain,(
% 0.99/0.60 ![X0]: (~v1000(X0,bitIndex0))),
% 0.99/0.60 inference(backward_subsumption_resolution,[status(thm)],[f1231,f7147])).
% 0.99/0.60 fof(f7252,plain,(
% 0.99/0.60 ![X0]: (~v999(X0))),
% 0.99/0.60 inference(backward_subsumption_resolution,[status(thm)],[f1226,f7148])).
% 0.99/0.60 fof(f7253,plain,(
% 0.99/0.60 ![X0]: (v998(X0))),
% 0.99/0.60 inference(backward_subsumption_resolution,[status(thm)],[f1222,f7252])).
% 0.99/0.60 fof(f7726,plain,(
% 0.99/0.60 ![X0]: (v996(X0))),
% 0.99/0.60 inference(forward_subsumption_resolution,[status(thm)],[f7143,f7253])).
% 0.99/0.60 fof(f7727,plain,(
% 0.99/0.60 $false),
% 0.99/0.60 inference(backward_subsumption_resolution,[status(thm)],[f7136,f7726])).
% 0.99/0.60 % SZS output end CNFRefutation for theBenchmark.p
% 0.99/0.62 % Elapsed time: 0.252403 seconds
% 0.99/0.62 % CPU time: 1.367581 seconds
% 0.99/0.62 % Total memory used: 225.486 MB
% 0.99/0.62 % Net memory used: 224.994 MB
%------------------------------------------------------------------------------