%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV093+1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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:46:25 PM UTC 2026
% Result : Theorem 0.16s 0.62s
% Output : CNFRefutation 0.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 12
% Syntax : Number of formulae : 59 ( 15 unt; 0 def)
% Number of atoms : 169 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 182 ( 72 ~; 62 |; 36 &)
% ( 10 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 14 ( 12 usr; 2 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 64 ( 63 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f35,conjecture,
! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
~ ! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
inference(negated_conjecture,[status(cth)],[f35]) ).
fof(f37,axiom,
! [VarCurr] :
( ~ v4(VarCurr)
<=> v995(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [VarCurr] :
( ~ v995(VarCurr)
<=> v996(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [VarCurr] :
( v996(VarCurr)
<=> ( v1010(VarCurr)
& v998(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [VarCurr] :
( v1010(VarCurr)
<=> ( v1000(VarCurr,bitIndex1)
| v1000(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [VarCurr] :
( ~ v998(VarCurr)
<=> v999(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [VarCurr] :
( v999(VarCurr)
<=> ( v1000(VarCurr,bitIndex1)
& v1000(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [VarCurr] :
( v1000(VarCurr,bitIndex0)
<=> v1001(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [VarCurr] :
( v1000(VarCurr,bitIndex1)
<=> $true ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [VarCurr] :
( v1001(VarCurr)
<=> ( v1007(VarCurr,bitIndex5)
& v1003(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [VarCurr] :
( v1003(VarCurr)
<=> ( v1007(VarCurr,bitIndex4)
& v1004(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,axiom,
! [VarCurr] : ~ v1007(VarCurr,bitIndex4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1198,plain,
? [VarCurr] :
( ~ v4(VarCurr)
& reachableState(VarCurr) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f1199,plain,
( ~ v4(sK0_skl)
& reachableState(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f1198]) ).
fof(f1201,plain,
~ v4(sK0_skl),
inference(cnf_transformation,[status(thm)],[f1199]) ).
fof(f1202,plain,
! [VarCurr] :
( ( ~ v995(VarCurr)
| ~ v4(VarCurr) )
& ( v995(VarCurr)
| v4(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f37]) ).
fof(f1203,plain,
( ! [VarCurr] :
( ~ v995(VarCurr)
| ~ v4(VarCurr) )
& ! [VarCurr] :
( v995(VarCurr)
| v4(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1202]) ).
fof(f1204,plain,
! [X0] :
( v995(X0)
| v4(X0) ),
inference(cnf_transformation,[status(thm)],[f1203]) ).
fof(f1206,plain,
! [VarCurr] :
( ( ~ v996(VarCurr)
| ~ v995(VarCurr) )
& ( v996(VarCurr)
| v995(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f38]) ).
fof(f1207,plain,
( ! [VarCurr] :
( ~ v996(VarCurr)
| ~ v995(VarCurr) )
& ! [VarCurr] :
( v996(VarCurr)
| v995(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1206]) ).
fof(f1209,plain,
! [X0] :
( ~ v996(X0)
| ~ v995(X0) ),
inference(cnf_transformation,[status(thm)],[f1207]) ).
fof(f1210,plain,
! [VarCurr] :
( ( ~ v1010(VarCurr)
| ~ v998(VarCurr)
| v996(VarCurr) )
& ( ( v1010(VarCurr)
& v998(VarCurr) )
| ~ v996(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f39]) ).
fof(f1211,plain,
( ! [VarCurr] :
( ~ v1010(VarCurr)
| ~ v998(VarCurr)
| v996(VarCurr) )
& ! [VarCurr] :
( ( v1010(VarCurr)
& v998(VarCurr) )
| ~ v996(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1210]) ).
fof(f1214,plain,
! [X0] :
( ~ v1010(X0)
| ~ v998(X0)
| v996(X0) ),
inference(cnf_transformation,[status(thm)],[f1211]) ).
fof(f1215,plain,
! [VarCurr] :
( ( ( ~ v1000(VarCurr,bitIndex1)
& ~ v1000(VarCurr,bitIndex0) )
| v1010(VarCurr) )
& ( v1000(VarCurr,bitIndex1)
| v1000(VarCurr,bitIndex0)
| ~ v1010(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f40]) ).
fof(f1216,plain,
( ! [VarCurr] :
( ( ~ v1000(VarCurr,bitIndex1)
& ~ v1000(VarCurr,bitIndex0) )
| v1010(VarCurr) )
& ! [VarCurr] :
( v1000(VarCurr,bitIndex1)
| v1000(VarCurr,bitIndex0)
| ~ v1010(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1215]) ).
fof(f1219,plain,
! [X0] :
( ~ v1000(X0,bitIndex1)
| v1010(X0) ),
inference(cnf_transformation,[status(thm)],[f1216]) ).
fof(f1220,plain,
! [VarCurr] :
( ( ~ v999(VarCurr)
| ~ v998(VarCurr) )
& ( v999(VarCurr)
| v998(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f41]) ).
fof(f1221,plain,
( ! [VarCurr] :
( ~ v999(VarCurr)
| ~ v998(VarCurr) )
& ! [VarCurr] :
( v999(VarCurr)
| v998(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1220]) ).
fof(f1222,plain,
! [X0] :
( v999(X0)
| v998(X0) ),
inference(cnf_transformation,[status(thm)],[f1221]) ).
fof(f1224,plain,
! [VarCurr] :
( ( ~ v1000(VarCurr,bitIndex1)
| ~ v1000(VarCurr,bitIndex0)
| v999(VarCurr) )
& ( ( v1000(VarCurr,bitIndex1)
& v1000(VarCurr,bitIndex0) )
| ~ v999(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f1225,plain,
( ! [VarCurr] :
( ~ v1000(VarCurr,bitIndex1)
| ~ v1000(VarCurr,bitIndex0)
| v999(VarCurr) )
& ! [VarCurr] :
( ( v1000(VarCurr,bitIndex1)
& v1000(VarCurr,bitIndex0) )
| ~ v999(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1224]) ).
fof(f1226,plain,
! [X0] :
( v1000(X0,bitIndex0)
| ~ v999(X0) ),
inference(cnf_transformation,[status(thm)],[f1225]) ).
fof(f1229,plain,
! [VarCurr] :
( ( ~ v1001(VarCurr)
| v1000(VarCurr,bitIndex0) )
& ( v1001(VarCurr)
| ~ v1000(VarCurr,bitIndex0) ) ),
inference(NNF_transformation,[status(thm)],[f43]) ).
fof(f1230,plain,
( ! [VarCurr] :
( ~ v1001(VarCurr)
| v1000(VarCurr,bitIndex0) )
& ! [VarCurr] :
( v1001(VarCurr)
| ~ v1000(VarCurr,bitIndex0) ) ),
inference(miniscoping,[status(thm)],[f1229]) ).
fof(f1231,plain,
! [X0] :
( v1001(X0)
| ~ v1000(X0,bitIndex0) ),
inference(cnf_transformation,[status(thm)],[f1230]) ).
fof(f1233,plain,
! [VarCurr] :
( ( $false
| v1000(VarCurr,bitIndex1) )
& ( $true
| ~ v1000(VarCurr,bitIndex1) ) ),
inference(NNF_transformation,[status(thm)],[f44]) ).
fof(f1234,plain,
( ( $false
| ! [VarCurr] : v1000(VarCurr,bitIndex1) )
& ( $true
| ! [VarCurr] : ~ v1000(VarCurr,bitIndex1) ) ),
inference(miniscoping,[status(thm)],[f1233]) ).
fof(f1235,plain,
! [VarCurr] : v1000(VarCurr,bitIndex1),
inference(true_and_false_simplification,[status(thm)],[f1234]) ).
fof(f1236,plain,
! [X0] : v1000(X0,bitIndex1),
inference(cnf_transformation,[status(thm)],[f1235]) ).
fof(f1237,plain,
! [VarCurr] :
( ( ~ v1007(VarCurr,bitIndex5)
| ~ v1003(VarCurr)
| v1001(VarCurr) )
& ( ( v1007(VarCurr,bitIndex5)
& v1003(VarCurr) )
| ~ v1001(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f45]) ).
fof(f1238,plain,
( ! [VarCurr] :
( ~ v1007(VarCurr,bitIndex5)
| ~ v1003(VarCurr)
| v1001(VarCurr) )
& ! [VarCurr] :
( ( v1007(VarCurr,bitIndex5)
& v1003(VarCurr) )
| ~ v1001(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1237]) ).
fof(f1239,plain,
! [X0] :
( v1003(X0)
| ~ v1001(X0) ),
inference(cnf_transformation,[status(thm)],[f1238]) ).
fof(f1242,plain,
! [VarCurr] :
( ( ~ v1007(VarCurr,bitIndex4)
| ~ v1004(VarCurr)
| v1003(VarCurr) )
& ( ( v1007(VarCurr,bitIndex4)
& v1004(VarCurr) )
| ~ v1003(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f46]) ).
fof(f1243,plain,
( ! [VarCurr] :
( ~ v1007(VarCurr,bitIndex4)
| ~ v1004(VarCurr)
| v1003(VarCurr) )
& ! [VarCurr] :
( ( v1007(VarCurr,bitIndex4)
& v1004(VarCurr) )
| ~ v1003(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1242]) ).
fof(f1245,plain,
! [X0] :
( v1007(X0,bitIndex4)
| ~ v1003(X0) ),
inference(cnf_transformation,[status(thm)],[f1243]) ).
fof(f1271,plain,
! [X0] : ~ v1007(X0,bitIndex4),
inference(cnf_transformation,[status(thm)],[f52]) ).
fof(f6843,plain,
v995(sK0_skl),
inference(resolution,[status(thm)],[f1204,f1201]) ).
fof(f6929,plain,
~ v996(sK0_skl),
inference(resolution,[status(thm)],[f1209,f6843]) ).
fof(f6935,plain,
! [X0] : v1010(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1219,f1236]) ).
fof(f6936,plain,
! [X0] :
( ~ v998(X0)
| v996(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1214,f6935]) ).
fof(f6937,plain,
! [X0] : ~ v1003(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1245,f1271]) ).
fof(f6938,plain,
! [X0] : ~ v1001(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1239,f6937]) ).
fof(f6939,plain,
! [X0] : ~ v1000(X0,bitIndex0),
inference(backward_subsumption_resolution,[status(thm)],[f1231,f6938]) ).
fof(f6940,plain,
! [X0] : ~ v999(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1226,f6939]) ).
fof(f6941,plain,
! [X0] : v998(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1222,f6940]) ).
fof(f7710,plain,
! [X0] : v996(X0),
inference(forward_subsumption_resolution,[status(thm)],[f6936,f6941]) ).
fof(f7711,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f6929,f7710]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV093+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.42 % Computer : n010.cluster.edu
% 0.09/0.42 % Model : x86_64 x86_64
% 0.09/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.42 % Memory : 8046.5625MB
% 0.09/0.42 % OS : Linux 6.8.0-71-generic
% 0.09/0.42 % CPULimit : 300
% 0.09/0.42 % WCLimit : 300
% 0.09/0.42 % DateTime : Sun Sep 20 21:19:40 UTC 2026
% 0.09/0.43 % CPUTime :
% 0.16/0.52 % Drodi V4.1.1
% 0.16/0.62 % Refutation found
% 0.16/0.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.16/0.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.70/0.68 % Elapsed time: 0.237251 seconds
% 0.70/0.68 % CPU time: 0.978755 seconds
% 0.70/0.68 % Total memory used: 227.347 MB
% 0.70/0.68 % Net memory used: 226.580 MB
%------------------------------------------------------------------------------