%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV090+1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:23 PM UTC 2026
% Result : Theorem 57.10s 10.75s
% Output : CNFRefutation 47.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 11
% Syntax : Number of formulae : 54 ( 14 unt; 0 def)
% Number of atoms : 151 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 161 ( 64 ~; 55 |; 31 &)
% ( 9 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 2 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 60 ( 59 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1199,conjecture,
! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1200,negated_conjecture,
~ ! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
inference(negated_conjecture,[status(cth)],[f1199]) ).
fof(f1201,axiom,
! [VarCurr] :
( ~ v4(VarCurr)
<=> v30850(VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1202,axiom,
! [VarCurr] :
( ~ v30850(VarCurr)
<=> v30851(VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1203,axiom,
! [VarCurr] :
( v30851(VarCurr)
<=> ( v30869(VarCurr)
& v30853(VarCurr) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1204,axiom,
! [VarCurr] :
( v30869(VarCurr)
<=> ( v30855(VarCurr,bitIndex1)
| v30855(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1205,axiom,
! [VarCurr] :
( ~ v30853(VarCurr)
<=> v30854(VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1206,axiom,
! [VarCurr] :
( v30854(VarCurr)
<=> ( v30855(VarCurr,bitIndex1)
& v30855(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1207,axiom,
! [VarCurr] :
( v30855(VarCurr,bitIndex0)
<=> v30856(VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1208,axiom,
! [VarCurr] :
( v30855(VarCurr,bitIndex1)
<=> $true ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1209,axiom,
! [VarCurr] :
( v30856(VarCurr)
<=> ( v30860(VarCurr,bitIndex5)
& v30858(VarCurr) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1222,axiom,
! [VarCurr] : ~ v30860(VarCurr,bitIndex5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43712,plain,
? [VarCurr] :
( ~ v4(VarCurr)
& reachableState(VarCurr) ),
inference(pre_NNF_transformation,[status(thm)],[f1200]) ).
fof(f43713,plain,
( ~ v4(sK0_skl)
& reachableState(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f43712]) ).
fof(f43715,plain,
~ v4(sK0_skl),
inference(cnf_transformation,[status(thm)],[f43713]) ).
fof(f43716,plain,
! [VarCurr] :
( ( ~ v30850(VarCurr)
| ~ v4(VarCurr) )
& ( v30850(VarCurr)
| v4(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f1201]) ).
fof(f43717,plain,
( ! [VarCurr] :
( ~ v30850(VarCurr)
| ~ v4(VarCurr) )
& ! [VarCurr] :
( v30850(VarCurr)
| v4(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f43716]) ).
fof(f43718,plain,
! [X0] :
( v30850(X0)
| v4(X0) ),
inference(cnf_transformation,[status(thm)],[f43717]) ).
fof(f43720,plain,
! [VarCurr] :
( ( ~ v30851(VarCurr)
| ~ v30850(VarCurr) )
& ( v30851(VarCurr)
| v30850(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f1202]) ).
fof(f43721,plain,
( ! [VarCurr] :
( ~ v30851(VarCurr)
| ~ v30850(VarCurr) )
& ! [VarCurr] :
( v30851(VarCurr)
| v30850(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f43720]) ).
fof(f43723,plain,
! [X0] :
( ~ v30851(X0)
| ~ v30850(X0) ),
inference(cnf_transformation,[status(thm)],[f43721]) ).
fof(f43724,plain,
! [VarCurr] :
( ( ~ v30869(VarCurr)
| ~ v30853(VarCurr)
| v30851(VarCurr) )
& ( ( v30869(VarCurr)
& v30853(VarCurr) )
| ~ v30851(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f1203]) ).
fof(f43725,plain,
( ! [VarCurr] :
( ~ v30869(VarCurr)
| ~ v30853(VarCurr)
| v30851(VarCurr) )
& ! [VarCurr] :
( ( v30869(VarCurr)
& v30853(VarCurr) )
| ~ v30851(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f43724]) ).
fof(f43728,plain,
! [X0] :
( ~ v30869(X0)
| v30851(X0)
| ~ v30853(X0) ),
inference(cnf_transformation,[status(thm)],[f43725]) ).
fof(f43729,plain,
! [VarCurr] :
( ( ( ~ v30855(VarCurr,bitIndex1)
& ~ v30855(VarCurr,bitIndex0) )
| v30869(VarCurr) )
& ( v30855(VarCurr,bitIndex1)
| v30855(VarCurr,bitIndex0)
| ~ v30869(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f1204]) ).
fof(f43730,plain,
( ! [VarCurr] :
( ( ~ v30855(VarCurr,bitIndex1)
& ~ v30855(VarCurr,bitIndex0) )
| v30869(VarCurr) )
& ! [VarCurr] :
( v30855(VarCurr,bitIndex1)
| v30855(VarCurr,bitIndex0)
| ~ v30869(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f43729]) ).
fof(f43733,plain,
! [X0] :
( v30869(X0)
| ~ v30855(X0,bitIndex1) ),
inference(cnf_transformation,[status(thm)],[f43730]) ).
fof(f43734,plain,
! [VarCurr] :
( ( ~ v30854(VarCurr)
| ~ v30853(VarCurr) )
& ( v30854(VarCurr)
| v30853(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f1205]) ).
fof(f43735,plain,
( ! [VarCurr] :
( ~ v30854(VarCurr)
| ~ v30853(VarCurr) )
& ! [VarCurr] :
( v30854(VarCurr)
| v30853(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f43734]) ).
fof(f43736,plain,
! [X0] :
( v30854(X0)
| v30853(X0) ),
inference(cnf_transformation,[status(thm)],[f43735]) ).
fof(f43738,plain,
! [VarCurr] :
( ( ~ v30855(VarCurr,bitIndex1)
| ~ v30855(VarCurr,bitIndex0)
| v30854(VarCurr) )
& ( ( v30855(VarCurr,bitIndex1)
& v30855(VarCurr,bitIndex0) )
| ~ v30854(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f1206]) ).
fof(f43739,plain,
( ! [VarCurr] :
( ~ v30855(VarCurr,bitIndex1)
| ~ v30855(VarCurr,bitIndex0)
| v30854(VarCurr) )
& ! [VarCurr] :
( ( v30855(VarCurr,bitIndex1)
& v30855(VarCurr,bitIndex0) )
| ~ v30854(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f43738]) ).
fof(f43740,plain,
! [X0] :
( ~ v30854(X0)
| v30855(X0,bitIndex0) ),
inference(cnf_transformation,[status(thm)],[f43739]) ).
fof(f43743,plain,
! [VarCurr] :
( ( ~ v30856(VarCurr)
| v30855(VarCurr,bitIndex0) )
& ( v30856(VarCurr)
| ~ v30855(VarCurr,bitIndex0) ) ),
inference(NNF_transformation,[status(thm)],[f1207]) ).
fof(f43744,plain,
( ! [VarCurr] :
( ~ v30856(VarCurr)
| v30855(VarCurr,bitIndex0) )
& ! [VarCurr] :
( v30856(VarCurr)
| ~ v30855(VarCurr,bitIndex0) ) ),
inference(miniscoping,[status(thm)],[f43743]) ).
fof(f43745,plain,
! [X0] :
( ~ v30855(X0,bitIndex0)
| v30856(X0) ),
inference(cnf_transformation,[status(thm)],[f43744]) ).
fof(f43747,plain,
! [VarCurr] :
( ( $false
| v30855(VarCurr,bitIndex1) )
& ( $true
| ~ v30855(VarCurr,bitIndex1) ) ),
inference(NNF_transformation,[status(thm)],[f1208]) ).
fof(f43748,plain,
( ( $false
| ! [VarCurr] : v30855(VarCurr,bitIndex1) )
& ( $true
| ! [VarCurr] : ~ v30855(VarCurr,bitIndex1) ) ),
inference(miniscoping,[status(thm)],[f43747]) ).
fof(f43749,plain,
! [VarCurr] : v30855(VarCurr,bitIndex1),
inference(true_and_false_simplification,[status(thm)],[f43748]) ).
fof(f43750,plain,
! [X0] : v30855(X0,bitIndex1),
inference(cnf_transformation,[status(thm)],[f43749]) ).
fof(f43751,plain,
! [VarCurr] :
( ( ~ v30860(VarCurr,bitIndex5)
| ~ v30858(VarCurr)
| v30856(VarCurr) )
& ( ( v30860(VarCurr,bitIndex5)
& v30858(VarCurr) )
| ~ v30856(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f1209]) ).
fof(f43752,plain,
( ! [VarCurr] :
( ~ v30860(VarCurr,bitIndex5)
| ~ v30858(VarCurr)
| v30856(VarCurr) )
& ! [VarCurr] :
( ( v30860(VarCurr,bitIndex5)
& v30858(VarCurr) )
| ~ v30856(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f43751]) ).
fof(f43754,plain,
! [X0] :
( v30860(X0,bitIndex5)
| ~ v30856(X0) ),
inference(cnf_transformation,[status(thm)],[f43752]) ).
fof(f43805,plain,
! [X0] : ~ v30860(X0,bitIndex5),
inference(cnf_transformation,[status(thm)],[f1222]) ).
fof(f302531,plain,
! [X0] : ~ v30856(X0),
inference(backward_subsumption_resolution,[status(thm)],[f43754,f43805]) ).
fof(f302532,plain,
! [X0] : v30869(X0),
inference(backward_subsumption_resolution,[status(thm)],[f43733,f43750]) ).
fof(f302535,plain,
! [X0] : ~ v30855(X0,bitIndex0),
inference(backward_subsumption_resolution,[status(thm)],[f43745,f302531]) ).
fof(f302536,plain,
! [X0] : ~ v30854(X0),
inference(backward_subsumption_resolution,[status(thm)],[f43740,f302535]) ).
fof(f302539,plain,
! [X0] : v30853(X0),
inference(backward_subsumption_resolution,[status(thm)],[f43736,f302536]) ).
fof(f302541,plain,
! [X0] :
( v30851(X0)
| ~ v30869(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f43728,f302539]) ).
fof(f302546,plain,
! [X0] : v30851(X0),
inference(backward_subsumption_resolution,[status(thm)],[f302541,f302532]) ).
fof(f302551,plain,
! [X0] : ~ v30850(X0),
inference(backward_subsumption_resolution,[status(thm)],[f43723,f302546]) ).
fof(f302555,plain,
! [X0] : v4(X0),
inference(backward_subsumption_resolution,[status(thm)],[f43718,f302551]) ).
fof(f302559,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f43715,f302555]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV090+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.42 % Computer : n008.cluster.edu
% 0.11/0.42 % Model : x86_64 x86_64
% 0.11/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.42 % Memory : 8046.5625MB
% 0.11/0.42 % OS : Linux 6.8.0-71-generic
% 0.11/0.42 % CPULimit : 300
% 0.11/0.42 % WCLimit : 300
% 0.11/0.42 % DateTime : Sun Sep 20 21:19:40 UTC 2026
% 0.11/0.42 % CPUTime :
% 3.62/3.91 % Drodi V4.1.1
% 57.10/10.75 % Refutation found
% 57.10/10.75 % SZS status Theorem for theBenchmark: Theorem is valid
% 57.10/10.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.28/11.78 % Elapsed time: 11.235168 seconds
% 5.28/11.78 % CPU time: 58.515191 seconds
% 5.28/11.78 % Total memory used: 5.850 GB
% 5.28/11.78 % Net memory used: 5.833 GB
%------------------------------------------------------------------------------