%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV089+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 : n013.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 0.34s 0.78s
% Output : CNFRefutation 0.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% 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 : 66 ( 65 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f321,conjecture,
! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f322,negated_conjecture,
~ ! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
inference(negated_conjecture,[status(cth)],[f321]) ).
fof(f323,axiom,
! [VarCurr] :
( ~ v4(VarCurr)
<=> v3674(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f324,axiom,
! [VarCurr] :
( ~ v3674(VarCurr)
<=> v3675(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f325,axiom,
! [VarCurr] :
( v3675(VarCurr)
<=> ( v3693(VarCurr)
& v3677(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f326,axiom,
! [VarCurr] :
( v3693(VarCurr)
<=> ( v3679(VarCurr,bitIndex1)
| v3679(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f327,axiom,
! [VarCurr] :
( ~ v3677(VarCurr)
<=> v3678(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f328,axiom,
! [VarCurr] :
( v3678(VarCurr)
<=> ( v3679(VarCurr,bitIndex1)
& v3679(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f329,axiom,
! [VarCurr] :
( v3679(VarCurr,bitIndex0)
<=> v3680(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f330,axiom,
! [VarCurr] :
( v3679(VarCurr,bitIndex1)
<=> $true ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f331,axiom,
! [VarCurr] :
( v3680(VarCurr)
<=> ( v3684(VarCurr,bitIndex5)
& v3682(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f332,axiom,
! [VarCurr] :
( v3682(VarCurr)
<=> ( v3684(VarCurr,bitIndex4)
& v3683(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f343,axiom,
! [VarCurr] : ~ v3684(VarCurr,bitIndex4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6910,plain,
? [VarCurr] :
( ~ v4(VarCurr)
& reachableState(VarCurr) ),
inference(pre_NNF_transformation,[status(thm)],[f322]) ).
fof(f6911,plain,
( ~ v4(sK0_skl)
& reachableState(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f6910]) ).
fof(f6913,plain,
~ v4(sK0_skl),
inference(cnf_transformation,[status(thm)],[f6911]) ).
fof(f6914,plain,
! [VarCurr] :
( ( ~ v3674(VarCurr)
| ~ v4(VarCurr) )
& ( v3674(VarCurr)
| v4(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f323]) ).
fof(f6915,plain,
( ! [VarCurr] :
( ~ v3674(VarCurr)
| ~ v4(VarCurr) )
& ! [VarCurr] :
( v3674(VarCurr)
| v4(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f6914]) ).
fof(f6916,plain,
! [X0] :
( v3674(X0)
| v4(X0) ),
inference(cnf_transformation,[status(thm)],[f6915]) ).
fof(f6918,plain,
! [VarCurr] :
( ( ~ v3675(VarCurr)
| ~ v3674(VarCurr) )
& ( v3675(VarCurr)
| v3674(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f324]) ).
fof(f6919,plain,
( ! [VarCurr] :
( ~ v3675(VarCurr)
| ~ v3674(VarCurr) )
& ! [VarCurr] :
( v3675(VarCurr)
| v3674(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f6918]) ).
fof(f6921,plain,
! [X0] :
( ~ v3675(X0)
| ~ v3674(X0) ),
inference(cnf_transformation,[status(thm)],[f6919]) ).
fof(f6922,plain,
! [VarCurr] :
( ( ~ v3693(VarCurr)
| ~ v3677(VarCurr)
| v3675(VarCurr) )
& ( ( v3693(VarCurr)
& v3677(VarCurr) )
| ~ v3675(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f325]) ).
fof(f6923,plain,
( ! [VarCurr] :
( ~ v3693(VarCurr)
| ~ v3677(VarCurr)
| v3675(VarCurr) )
& ! [VarCurr] :
( ( v3693(VarCurr)
& v3677(VarCurr) )
| ~ v3675(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f6922]) ).
fof(f6926,plain,
! [X0] :
( ~ v3693(X0)
| ~ v3677(X0)
| v3675(X0) ),
inference(cnf_transformation,[status(thm)],[f6923]) ).
fof(f6927,plain,
! [VarCurr] :
( ( ( ~ v3679(VarCurr,bitIndex1)
& ~ v3679(VarCurr,bitIndex0) )
| v3693(VarCurr) )
& ( v3679(VarCurr,bitIndex1)
| v3679(VarCurr,bitIndex0)
| ~ v3693(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f326]) ).
fof(f6928,plain,
( ! [VarCurr] :
( ( ~ v3679(VarCurr,bitIndex1)
& ~ v3679(VarCurr,bitIndex0) )
| v3693(VarCurr) )
& ! [VarCurr] :
( v3679(VarCurr,bitIndex1)
| v3679(VarCurr,bitIndex0)
| ~ v3693(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f6927]) ).
fof(f6931,plain,
! [X0] :
( ~ v3679(X0,bitIndex1)
| v3693(X0) ),
inference(cnf_transformation,[status(thm)],[f6928]) ).
fof(f6932,plain,
! [VarCurr] :
( ( ~ v3678(VarCurr)
| ~ v3677(VarCurr) )
& ( v3678(VarCurr)
| v3677(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f327]) ).
fof(f6933,plain,
( ! [VarCurr] :
( ~ v3678(VarCurr)
| ~ v3677(VarCurr) )
& ! [VarCurr] :
( v3678(VarCurr)
| v3677(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f6932]) ).
fof(f6934,plain,
! [X0] :
( v3678(X0)
| v3677(X0) ),
inference(cnf_transformation,[status(thm)],[f6933]) ).
fof(f6936,plain,
! [VarCurr] :
( ( ~ v3679(VarCurr,bitIndex1)
| ~ v3679(VarCurr,bitIndex0)
| v3678(VarCurr) )
& ( ( v3679(VarCurr,bitIndex1)
& v3679(VarCurr,bitIndex0) )
| ~ v3678(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f328]) ).
fof(f6937,plain,
( ! [VarCurr] :
( ~ v3679(VarCurr,bitIndex1)
| ~ v3679(VarCurr,bitIndex0)
| v3678(VarCurr) )
& ! [VarCurr] :
( ( v3679(VarCurr,bitIndex1)
& v3679(VarCurr,bitIndex0) )
| ~ v3678(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f6936]) ).
fof(f6938,plain,
! [X0] :
( v3679(X0,bitIndex0)
| ~ v3678(X0) ),
inference(cnf_transformation,[status(thm)],[f6937]) ).
fof(f6941,plain,
! [VarCurr] :
( ( ~ v3680(VarCurr)
| v3679(VarCurr,bitIndex0) )
& ( v3680(VarCurr)
| ~ v3679(VarCurr,bitIndex0) ) ),
inference(NNF_transformation,[status(thm)],[f329]) ).
fof(f6942,plain,
( ! [VarCurr] :
( ~ v3680(VarCurr)
| v3679(VarCurr,bitIndex0) )
& ! [VarCurr] :
( v3680(VarCurr)
| ~ v3679(VarCurr,bitIndex0) ) ),
inference(miniscoping,[status(thm)],[f6941]) ).
fof(f6943,plain,
! [X0] :
( v3680(X0)
| ~ v3679(X0,bitIndex0) ),
inference(cnf_transformation,[status(thm)],[f6942]) ).
fof(f6945,plain,
! [VarCurr] :
( ( $false
| v3679(VarCurr,bitIndex1) )
& ( $true
| ~ v3679(VarCurr,bitIndex1) ) ),
inference(NNF_transformation,[status(thm)],[f330]) ).
fof(f6946,plain,
( ( $false
| ! [VarCurr] : v3679(VarCurr,bitIndex1) )
& ( $true
| ! [VarCurr] : ~ v3679(VarCurr,bitIndex1) ) ),
inference(miniscoping,[status(thm)],[f6945]) ).
fof(f6947,plain,
! [VarCurr] : v3679(VarCurr,bitIndex1),
inference(true_and_false_simplification,[status(thm)],[f6946]) ).
fof(f6948,plain,
! [X0] : v3679(X0,bitIndex1),
inference(cnf_transformation,[status(thm)],[f6947]) ).
fof(f6949,plain,
! [VarCurr] :
( ( ~ v3684(VarCurr,bitIndex5)
| ~ v3682(VarCurr)
| v3680(VarCurr) )
& ( ( v3684(VarCurr,bitIndex5)
& v3682(VarCurr) )
| ~ v3680(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f331]) ).
fof(f6950,plain,
( ! [VarCurr] :
( ~ v3684(VarCurr,bitIndex5)
| ~ v3682(VarCurr)
| v3680(VarCurr) )
& ! [VarCurr] :
( ( v3684(VarCurr,bitIndex5)
& v3682(VarCurr) )
| ~ v3680(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f6949]) ).
fof(f6951,plain,
! [X0] :
( v3682(X0)
| ~ v3680(X0) ),
inference(cnf_transformation,[status(thm)],[f6950]) ).
fof(f6954,plain,
! [VarCurr] :
( ( ~ v3684(VarCurr,bitIndex4)
| ~ v3683(VarCurr)
| v3682(VarCurr) )
& ( ( v3684(VarCurr,bitIndex4)
& v3683(VarCurr) )
| ~ v3682(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f332]) ).
fof(f6955,plain,
( ! [VarCurr] :
( ~ v3684(VarCurr,bitIndex4)
| ~ v3683(VarCurr)
| v3682(VarCurr) )
& ! [VarCurr] :
( ( v3684(VarCurr,bitIndex4)
& v3683(VarCurr) )
| ~ v3682(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f6954]) ).
fof(f6957,plain,
! [X0] :
( v3684(X0,bitIndex4)
| ~ v3682(X0) ),
inference(cnf_transformation,[status(thm)],[f6955]) ).
fof(f7002,plain,
! [X0] : ~ v3684(X0,bitIndex4),
inference(cnf_transformation,[status(thm)],[f343]) ).
fof(f35926,plain,
! [X0] : v3693(X0),
inference(backward_subsumption_resolution,[status(thm)],[f6931,f6948]) ).
fof(f35927,plain,
! [X0] :
( ~ v3677(X0)
| v3675(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f6926,f35926]) ).
fof(f35936,plain,
! [X0] : ~ v3682(X0),
inference(backward_subsumption_resolution,[status(thm)],[f6957,f7002]) ).
fof(f35938,plain,
! [X0] : ~ v3680(X0),
inference(backward_subsumption_resolution,[status(thm)],[f6951,f35936]) ).
fof(f35939,plain,
! [X0] : ~ v3679(X0,bitIndex0),
inference(backward_subsumption_resolution,[status(thm)],[f6943,f35938]) ).
fof(f36775,plain,
! [X0] : ~ v3678(X0),
inference(backward_subsumption_resolution,[status(thm)],[f6938,f35939]) ).
fof(f36776,plain,
! [X0] : v3677(X0),
inference(backward_subsumption_resolution,[status(thm)],[f6934,f36775]) ).
fof(f37802,plain,
! [X0] : ~ v3674(X0),
inference(backward_subsumption_resolution,[status(thm)],[f6921,f37803]) ).
fof(f37803,plain,
! [X0] : v3675(X0),
inference(forward_subsumption_resolution,[status(thm)],[f35927,f36776]) ).
fof(f37804,plain,
! [X0] : v4(X0),
inference(backward_subsumption_resolution,[status(thm)],[f6916,f37802]) ).
fof(f37807,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f6913,f37804]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV089+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.41 % Computer : n013.cluster.edu
% 0.11/0.41 % Model : x86_64 x86_64
% 0.11/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.41 % Memory : 8046.5625MB
% 0.11/0.41 % OS : Linux 6.8.0-71-generic
% 0.11/0.41 % CPULimit : 300
% 0.11/0.41 % WCLimit : 300
% 0.11/0.41 % DateTime : Sun Sep 20 21:17:50 UTC 2026
% 0.11/0.41 % CPUTime :
% 0.18/0.54 % Drodi V4.1.1
% 0.34/0.78 % Refutation found
% 0.34/0.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.34/0.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.36/0.92 % Elapsed time: 0.485774 seconds
% 0.36/0.92 % CPU time: 2.144646 seconds
% 0.36/0.92 % Total memory used: 696.504 MB
% 0.36/0.92 % Net memory used: 693.018 MB
%------------------------------------------------------------------------------