%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV094+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 : n018.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 59.88s 16.92s
% Output : CNFRefutation 69.46s
% 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(f615,conjecture,
! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f616,negated_conjecture,
~ ! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
inference(negated_conjecture,[status(cth)],[f615]) ).
fof(f617,axiom,
! [VarCurr] :
( ~ v4(VarCurr)
<=> v133774(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f618,axiom,
! [VarCurr] :
( ~ v133774(VarCurr)
<=> v133775(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f619,axiom,
! [VarCurr] :
( v133775(VarCurr)
<=> ( v133789(VarCurr)
& v133777(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f620,axiom,
! [VarCurr] :
( v133789(VarCurr)
<=> ( v133779(VarCurr,bitIndex1)
| v133779(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f621,axiom,
! [VarCurr] :
( ~ v133777(VarCurr)
<=> v133778(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f622,axiom,
! [VarCurr] :
( v133778(VarCurr)
<=> ( v133779(VarCurr,bitIndex1)
& v133779(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f623,axiom,
! [VarCurr] :
( v133779(VarCurr,bitIndex0)
<=> v133780(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f624,axiom,
! [VarCurr] :
( v133779(VarCurr,bitIndex1)
<=> $true ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f625,axiom,
! [VarCurr] :
( v133780(VarCurr)
<=> ( v133786(VarCurr,bitIndex5)
& v133782(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f626,axiom,
! [VarCurr] :
( v133782(VarCurr)
<=> ( v133786(VarCurr,bitIndex4)
& v133783(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f632,axiom,
! [VarCurr] : ~ v133786(VarCurr,bitIndex4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f135986,plain,
? [VarCurr] :
( ~ v4(VarCurr)
& reachableState(VarCurr) ),
inference(pre_NNF_transformation,[status(thm)],[f616]) ).
fof(f135987,plain,
( ~ v4(sK0_skl)
& reachableState(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f135986]) ).
fof(f135989,plain,
~ v4(sK0_skl),
inference(cnf_transformation,[status(thm)],[f135987]) ).
fof(f135990,plain,
! [VarCurr] :
( ( ~ v133774(VarCurr)
| ~ v4(VarCurr) )
& ( v133774(VarCurr)
| v4(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f617]) ).
fof(f135991,plain,
( ! [VarCurr] :
( ~ v133774(VarCurr)
| ~ v4(VarCurr) )
& ! [VarCurr] :
( v133774(VarCurr)
| v4(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f135990]) ).
fof(f135992,plain,
! [X0] :
( v4(X0)
| v133774(X0) ),
inference(cnf_transformation,[status(thm)],[f135991]) ).
fof(f135994,plain,
! [VarCurr] :
( ( ~ v133775(VarCurr)
| ~ v133774(VarCurr) )
& ( v133775(VarCurr)
| v133774(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f618]) ).
fof(f135995,plain,
( ! [VarCurr] :
( ~ v133775(VarCurr)
| ~ v133774(VarCurr) )
& ! [VarCurr] :
( v133775(VarCurr)
| v133774(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f135994]) ).
fof(f135997,plain,
! [X0] :
( ~ v133775(X0)
| ~ v133774(X0) ),
inference(cnf_transformation,[status(thm)],[f135995]) ).
fof(f135998,plain,
! [VarCurr] :
( ( ~ v133789(VarCurr)
| ~ v133777(VarCurr)
| v133775(VarCurr) )
& ( ( v133789(VarCurr)
& v133777(VarCurr) )
| ~ v133775(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f619]) ).
fof(f135999,plain,
( ! [VarCurr] :
( ~ v133789(VarCurr)
| ~ v133777(VarCurr)
| v133775(VarCurr) )
& ! [VarCurr] :
( ( v133789(VarCurr)
& v133777(VarCurr) )
| ~ v133775(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f135998]) ).
fof(f136002,plain,
! [X0] :
( v133775(X0)
| ~ v133777(X0)
| ~ v133789(X0) ),
inference(cnf_transformation,[status(thm)],[f135999]) ).
fof(f136003,plain,
! [VarCurr] :
( ( ( ~ v133779(VarCurr,bitIndex1)
& ~ v133779(VarCurr,bitIndex0) )
| v133789(VarCurr) )
& ( v133779(VarCurr,bitIndex1)
| v133779(VarCurr,bitIndex0)
| ~ v133789(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f620]) ).
fof(f136004,plain,
( ! [VarCurr] :
( ( ~ v133779(VarCurr,bitIndex1)
& ~ v133779(VarCurr,bitIndex0) )
| v133789(VarCurr) )
& ! [VarCurr] :
( v133779(VarCurr,bitIndex1)
| v133779(VarCurr,bitIndex0)
| ~ v133789(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f136003]) ).
fof(f136007,plain,
! [X0] :
( v133789(X0)
| ~ v133779(X0,bitIndex1) ),
inference(cnf_transformation,[status(thm)],[f136004]) ).
fof(f136008,plain,
! [VarCurr] :
( ( ~ v133778(VarCurr)
| ~ v133777(VarCurr) )
& ( v133778(VarCurr)
| v133777(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f621]) ).
fof(f136009,plain,
( ! [VarCurr] :
( ~ v133778(VarCurr)
| ~ v133777(VarCurr) )
& ! [VarCurr] :
( v133778(VarCurr)
| v133777(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f136008]) ).
fof(f136010,plain,
! [X0] :
( v133778(X0)
| v133777(X0) ),
inference(cnf_transformation,[status(thm)],[f136009]) ).
fof(f136012,plain,
! [VarCurr] :
( ( ~ v133779(VarCurr,bitIndex1)
| ~ v133779(VarCurr,bitIndex0)
| v133778(VarCurr) )
& ( ( v133779(VarCurr,bitIndex1)
& v133779(VarCurr,bitIndex0) )
| ~ v133778(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f622]) ).
fof(f136013,plain,
( ! [VarCurr] :
( ~ v133779(VarCurr,bitIndex1)
| ~ v133779(VarCurr,bitIndex0)
| v133778(VarCurr) )
& ! [VarCurr] :
( ( v133779(VarCurr,bitIndex1)
& v133779(VarCurr,bitIndex0) )
| ~ v133778(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f136012]) ).
fof(f136014,plain,
! [X0] :
( v133779(X0,bitIndex0)
| ~ v133778(X0) ),
inference(cnf_transformation,[status(thm)],[f136013]) ).
fof(f136017,plain,
! [VarCurr] :
( ( ~ v133780(VarCurr)
| v133779(VarCurr,bitIndex0) )
& ( v133780(VarCurr)
| ~ v133779(VarCurr,bitIndex0) ) ),
inference(NNF_transformation,[status(thm)],[f623]) ).
fof(f136018,plain,
( ! [VarCurr] :
( ~ v133780(VarCurr)
| v133779(VarCurr,bitIndex0) )
& ! [VarCurr] :
( v133780(VarCurr)
| ~ v133779(VarCurr,bitIndex0) ) ),
inference(miniscoping,[status(thm)],[f136017]) ).
fof(f136019,plain,
! [X0] :
( v133780(X0)
| ~ v133779(X0,bitIndex0) ),
inference(cnf_transformation,[status(thm)],[f136018]) ).
fof(f136021,plain,
! [VarCurr] :
( ( $false
| v133779(VarCurr,bitIndex1) )
& ( $true
| ~ v133779(VarCurr,bitIndex1) ) ),
inference(NNF_transformation,[status(thm)],[f624]) ).
fof(f136022,plain,
( ( $false
| ! [VarCurr] : v133779(VarCurr,bitIndex1) )
& ( $true
| ! [VarCurr] : ~ v133779(VarCurr,bitIndex1) ) ),
inference(miniscoping,[status(thm)],[f136021]) ).
fof(f136023,plain,
! [VarCurr] : v133779(VarCurr,bitIndex1),
inference(true_and_false_simplification,[status(thm)],[f136022]) ).
fof(f136024,plain,
! [X0] : v133779(X0,bitIndex1),
inference(cnf_transformation,[status(thm)],[f136023]) ).
fof(f136025,plain,
! [VarCurr] :
( ( ~ v133786(VarCurr,bitIndex5)
| ~ v133782(VarCurr)
| v133780(VarCurr) )
& ( ( v133786(VarCurr,bitIndex5)
& v133782(VarCurr) )
| ~ v133780(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f625]) ).
fof(f136026,plain,
( ! [VarCurr] :
( ~ v133786(VarCurr,bitIndex5)
| ~ v133782(VarCurr)
| v133780(VarCurr) )
& ! [VarCurr] :
( ( v133786(VarCurr,bitIndex5)
& v133782(VarCurr) )
| ~ v133780(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f136025]) ).
fof(f136027,plain,
! [X0] :
( v133782(X0)
| ~ v133780(X0) ),
inference(cnf_transformation,[status(thm)],[f136026]) ).
fof(f136030,plain,
! [VarCurr] :
( ( ~ v133786(VarCurr,bitIndex4)
| ~ v133783(VarCurr)
| v133782(VarCurr) )
& ( ( v133786(VarCurr,bitIndex4)
& v133783(VarCurr) )
| ~ v133782(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f626]) ).
fof(f136031,plain,
( ! [VarCurr] :
( ~ v133786(VarCurr,bitIndex4)
| ~ v133783(VarCurr)
| v133782(VarCurr) )
& ! [VarCurr] :
( ( v133786(VarCurr,bitIndex4)
& v133783(VarCurr) )
| ~ v133782(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f136030]) ).
fof(f136033,plain,
! [X0] :
( ~ v133782(X0)
| v133786(X0,bitIndex4) ),
inference(cnf_transformation,[status(thm)],[f136031]) ).
fof(f136059,plain,
! [X0] : ~ v133786(X0,bitIndex4),
inference(cnf_transformation,[status(thm)],[f632]) ).
fof(f924143,plain,
! [X0] : v133789(X0),
inference(backward_subsumption_resolution,[status(thm)],[f136007,f136024]) ).
fof(f924146,plain,
! [X0] : ~ v133782(X0),
inference(backward_subsumption_resolution,[status(thm)],[f136033,f136059]) ).
fof(f924147,plain,
! [X0] :
( ~ v133777(X0)
| v133775(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f136002,f924143]) ).
fof(f924148,plain,
! [X0] : ~ v133779(X0,bitIndex0),
inference(backward_subsumption_resolution,[status(thm)],[f136019,f924149]) ).
fof(f924149,plain,
! [X0] : ~ v133780(X0),
inference(forward_subsumption_resolution,[status(thm)],[f136027,f924146]) ).
fof(f924151,plain,
! [X0] : ~ v133778(X0),
inference(backward_subsumption_resolution,[status(thm)],[f136014,f924148]) ).
fof(f924152,plain,
! [X0] : v133777(X0),
inference(backward_subsumption_resolution,[status(thm)],[f136010,f924151]) ).
fof(f924162,plain,
! [X0] : v133775(X0),
inference(backward_subsumption_resolution,[status(thm)],[f924147,f924152]) ).
fof(f924165,plain,
! [X0] : ~ v133774(X0),
inference(backward_subsumption_resolution,[status(thm)],[f135997,f924162]) ).
fof(f924171,plain,
! [X0] : v4(X0),
inference(backward_subsumption_resolution,[status(thm)],[f135992,f924165]) ).
fof(f924178,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f135989,f924171]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV094+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.09 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.44 % Computer : n018.cluster.edu
% 0.15/0.44 % Model : x86_64 x86_64
% 0.15/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.44 % Memory : 8046.5625MB
% 0.15/0.44 % OS : Linux 6.8.0-71-generic
% 0.15/0.44 % CPULimit : 300
% 0.15/0.44 % WCLimit : 300
% 0.15/0.44 % DateTime : Sun Sep 20 21:21:58 UTC 2026
% 0.15/0.45 % CPUTime :
% 10.21/10.52 % Drodi V4.1.1
% 59.88/16.92 % Refutation found
% 59.88/16.92 % SZS status Theorem for theBenchmark: Theorem is valid
% 59.88/16.92 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 14.49/19.92 % Elapsed time: 17.828524 seconds
% 14.49/19.92 % CPU time: 60.838315 seconds
% 14.49/19.92 % Total memory used: 16.167 GB
% 14.49/19.92 % Net memory used: 16.132 GB
%------------------------------------------------------------------------------