%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV092+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 : n016.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:24 PM UTC 2026
% Result : Theorem 112.74s 38.64s
% Output : CNFRefutation 106.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% 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(f989,conjecture,
! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f990,negated_conjecture,
~ ! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
inference(negated_conjecture,[status(cth)],[f989]) ).
fof(f991,axiom,
! [VarCurr] :
( ~ v4(VarCurr)
<=> v75396(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f992,axiom,
! [VarCurr] :
( ~ v75396(VarCurr)
<=> v75397(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f993,axiom,
! [VarCurr] :
( v75397(VarCurr)
<=> ( v75423(VarCurr)
& v75399(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f994,axiom,
! [VarCurr] :
( v75423(VarCurr)
<=> ( v75401(VarCurr,bitIndex1)
| v75401(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f995,axiom,
! [VarCurr] :
( ~ v75399(VarCurr)
<=> v75400(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f996,axiom,
! [VarCurr] :
( v75400(VarCurr)
<=> ( v75401(VarCurr,bitIndex1)
& v75401(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f997,axiom,
! [VarCurr] :
( v75401(VarCurr,bitIndex0)
<=> v75402(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f998,axiom,
! [VarCurr] :
( v75401(VarCurr,bitIndex1)
<=> $true ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f999,axiom,
! [VarCurr] :
( v75402(VarCurr)
<=> ( v75405(VarCurr,bitIndex9)
& v75404(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1023,axiom,
! [VarCurr] : ~ v75405(VarCurr,bitIndex9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f91992,plain,
? [VarCurr] :
( ~ v4(VarCurr)
& reachableState(VarCurr) ),
inference(pre_NNF_transformation,[status(thm)],[f990]) ).
fof(f91993,plain,
( ~ v4(sK0_skl)
& reachableState(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f91992]) ).
fof(f91995,plain,
~ v4(sK0_skl),
inference(cnf_transformation,[status(thm)],[f91993]) ).
fof(f91996,plain,
! [VarCurr] :
( ( ~ v75396(VarCurr)
| ~ v4(VarCurr) )
& ( v75396(VarCurr)
| v4(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f991]) ).
fof(f91997,plain,
( ! [VarCurr] :
( ~ v75396(VarCurr)
| ~ v4(VarCurr) )
& ! [VarCurr] :
( v75396(VarCurr)
| v4(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f91996]) ).
fof(f91998,plain,
! [X0] :
( v75396(X0)
| v4(X0) ),
inference(cnf_transformation,[status(thm)],[f91997]) ).
fof(f92000,plain,
! [VarCurr] :
( ( ~ v75397(VarCurr)
| ~ v75396(VarCurr) )
& ( v75397(VarCurr)
| v75396(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f992]) ).
fof(f92001,plain,
( ! [VarCurr] :
( ~ v75397(VarCurr)
| ~ v75396(VarCurr) )
& ! [VarCurr] :
( v75397(VarCurr)
| v75396(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f92000]) ).
fof(f92003,plain,
! [X0] :
( ~ v75397(X0)
| ~ v75396(X0) ),
inference(cnf_transformation,[status(thm)],[f92001]) ).
fof(f92004,plain,
! [VarCurr] :
( ( ~ v75423(VarCurr)
| ~ v75399(VarCurr)
| v75397(VarCurr) )
& ( ( v75423(VarCurr)
& v75399(VarCurr) )
| ~ v75397(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f993]) ).
fof(f92005,plain,
( ! [VarCurr] :
( ~ v75423(VarCurr)
| ~ v75399(VarCurr)
| v75397(VarCurr) )
& ! [VarCurr] :
( ( v75423(VarCurr)
& v75399(VarCurr) )
| ~ v75397(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f92004]) ).
fof(f92008,plain,
! [X0] :
( ~ v75423(X0)
| v75397(X0)
| ~ v75399(X0) ),
inference(cnf_transformation,[status(thm)],[f92005]) ).
fof(f92009,plain,
! [VarCurr] :
( ( ( ~ v75401(VarCurr,bitIndex1)
& ~ v75401(VarCurr,bitIndex0) )
| v75423(VarCurr) )
& ( v75401(VarCurr,bitIndex1)
| v75401(VarCurr,bitIndex0)
| ~ v75423(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f994]) ).
fof(f92010,plain,
( ! [VarCurr] :
( ( ~ v75401(VarCurr,bitIndex1)
& ~ v75401(VarCurr,bitIndex0) )
| v75423(VarCurr) )
& ! [VarCurr] :
( v75401(VarCurr,bitIndex1)
| v75401(VarCurr,bitIndex0)
| ~ v75423(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f92009]) ).
fof(f92013,plain,
! [X0] :
( ~ v75401(X0,bitIndex1)
| v75423(X0) ),
inference(cnf_transformation,[status(thm)],[f92010]) ).
fof(f92014,plain,
! [VarCurr] :
( ( ~ v75400(VarCurr)
| ~ v75399(VarCurr) )
& ( v75400(VarCurr)
| v75399(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f995]) ).
fof(f92015,plain,
( ! [VarCurr] :
( ~ v75400(VarCurr)
| ~ v75399(VarCurr) )
& ! [VarCurr] :
( v75400(VarCurr)
| v75399(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f92014]) ).
fof(f92016,plain,
! [X0] :
( v75399(X0)
| v75400(X0) ),
inference(cnf_transformation,[status(thm)],[f92015]) ).
fof(f92018,plain,
! [VarCurr] :
( ( ~ v75401(VarCurr,bitIndex1)
| ~ v75401(VarCurr,bitIndex0)
| v75400(VarCurr) )
& ( ( v75401(VarCurr,bitIndex1)
& v75401(VarCurr,bitIndex0) )
| ~ v75400(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f996]) ).
fof(f92019,plain,
( ! [VarCurr] :
( ~ v75401(VarCurr,bitIndex1)
| ~ v75401(VarCurr,bitIndex0)
| v75400(VarCurr) )
& ! [VarCurr] :
( ( v75401(VarCurr,bitIndex1)
& v75401(VarCurr,bitIndex0) )
| ~ v75400(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f92018]) ).
fof(f92020,plain,
! [X0] :
( v75401(X0,bitIndex0)
| ~ v75400(X0) ),
inference(cnf_transformation,[status(thm)],[f92019]) ).
fof(f92023,plain,
! [VarCurr] :
( ( ~ v75402(VarCurr)
| v75401(VarCurr,bitIndex0) )
& ( v75402(VarCurr)
| ~ v75401(VarCurr,bitIndex0) ) ),
inference(NNF_transformation,[status(thm)],[f997]) ).
fof(f92024,plain,
( ! [VarCurr] :
( ~ v75402(VarCurr)
| v75401(VarCurr,bitIndex0) )
& ! [VarCurr] :
( v75402(VarCurr)
| ~ v75401(VarCurr,bitIndex0) ) ),
inference(miniscoping,[status(thm)],[f92023]) ).
fof(f92025,plain,
! [X0] :
( ~ v75401(X0,bitIndex0)
| v75402(X0) ),
inference(cnf_transformation,[status(thm)],[f92024]) ).
fof(f92027,plain,
! [VarCurr] :
( ( $false
| v75401(VarCurr,bitIndex1) )
& ( $true
| ~ v75401(VarCurr,bitIndex1) ) ),
inference(NNF_transformation,[status(thm)],[f998]) ).
fof(f92028,plain,
( ( $false
| ! [VarCurr] : v75401(VarCurr,bitIndex1) )
& ( $true
| ! [VarCurr] : ~ v75401(VarCurr,bitIndex1) ) ),
inference(miniscoping,[status(thm)],[f92027]) ).
fof(f92029,plain,
! [VarCurr] : v75401(VarCurr,bitIndex1),
inference(true_and_false_simplification,[status(thm)],[f92028]) ).
fof(f92030,plain,
! [X0] : v75401(X0,bitIndex1),
inference(cnf_transformation,[status(thm)],[f92029]) ).
fof(f92031,plain,
! [VarCurr] :
( ( ~ v75405(VarCurr,bitIndex9)
| ~ v75404(VarCurr)
| v75402(VarCurr) )
& ( ( v75405(VarCurr,bitIndex9)
& v75404(VarCurr) )
| ~ v75402(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f999]) ).
fof(f92032,plain,
( ! [VarCurr] :
( ~ v75405(VarCurr,bitIndex9)
| ~ v75404(VarCurr)
| v75402(VarCurr) )
& ! [VarCurr] :
( ( v75405(VarCurr,bitIndex9)
& v75404(VarCurr) )
| ~ v75402(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f92031]) ).
fof(f92034,plain,
! [X0] :
( v75405(X0,bitIndex9)
| ~ v75402(X0) ),
inference(cnf_transformation,[status(thm)],[f92032]) ).
fof(f92126,plain,
! [X0] : ~ v75405(X0,bitIndex9),
inference(cnf_transformation,[status(thm)],[f1023]) ).
fof(f1045858,plain,
! [X0] : v75423(X0),
inference(backward_subsumption_resolution,[status(thm)],[f92013,f92030]) ).
fof(f1045860,plain,
! [X0] : ~ v75401(X0,bitIndex0),
inference(backward_subsumption_resolution,[status(thm)],[f92025,f1045861]) ).
fof(f1045861,plain,
! [X0] : ~ v75402(X0),
inference(forward_subsumption_resolution,[status(thm)],[f92034,f92126]) ).
fof(f1045869,plain,
! [X0] :
( ~ v75399(X0)
| v75397(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f92008,f1045858]) ).
fof(f1045874,plain,
! [X0] : v75399(X0),
inference(backward_subsumption_resolution,[status(thm)],[f92016,f1045875]) ).
fof(f1045875,plain,
! [X0] : ~ v75400(X0),
inference(forward_subsumption_resolution,[status(thm)],[f92020,f1045860]) ).
fof(f1045877,plain,
! [X0] : v75397(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1045869,f1045874]) ).
fof(f1045878,plain,
! [X0] : ~ v75396(X0),
inference(backward_subsumption_resolution,[status(thm)],[f92003,f1045877]) ).
fof(f1045881,plain,
! [X0] : v4(X0),
inference(backward_subsumption_resolution,[status(thm)],[f91998,f1045878]) ).
fof(f1045883,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f91995,f1045881]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV092+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.11 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.47 % Computer : n016.cluster.edu
% 0.16/0.47 % Model : x86_64 x86_64
% 0.16/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.47 % Memory : 8046.5625MB
% 0.16/0.47 % OS : Linux 6.8.0-71-generic
% 0.16/0.47 % CPULimit : 300
% 0.16/0.47 % WCLimit : 300
% 0.16/0.47 % DateTime : Sun Sep 20 21:23:53 UTC 2026
% 0.16/0.48 % CPUTime :
% 27.39/27.75 % Drodi V4.1.1
% 112.74/38.64 % Refutation found
% 112.74/38.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 112.74/38.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 31.00/42.74 % Elapsed time: 39.624234 seconds
% 31.00/42.74 % CPU time: 116.823358 seconds
% 31.00/42.74 % Total memory used: 26.255 GB
% 31.00/42.74 % Net memory used: 26.207 GB
%------------------------------------------------------------------------------