%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV096+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 : n009.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:27 PM UTC 2026
% Result : Theorem 63.53s 17.59s
% Output : CNFRefutation 71.30s
% 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(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(f633,axiom,
! [VarCurr] : ~ v133786(VarCurr,bitIndex5),
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] :
( v133774(X0)
| v4(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] :
( ~ v133774(X0)
| ~ v133775(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] :
( ~ v133789(X0)
| v133775(X0)
| ~ v133777(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] :
( ~ v133779(X0,bitIndex1)
| v133789(X0) ),
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] :
( ~ v133778(X0)
| v133779(X0,bitIndex0) ),
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] :
( ~ v133779(X0,bitIndex0)
| v133780(X0) ),
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(f136028,plain,
! [X0] :
( v133786(X0,bitIndex5)
| ~ v133780(X0) ),
inference(cnf_transformation,[status(thm)],[f136026]) ).
fof(f136060,plain,
! [X0] : ~ v133786(X0,bitIndex5),
inference(cnf_transformation,[status(thm)],[f633]) ).
fof(f924143,plain,
! [X0] : ~ v133779(X0,bitIndex0),
inference(backward_subsumption_resolution,[status(thm)],[f136019,f924144]) ).
fof(f924144,plain,
! [X0] : ~ v133780(X0),
inference(forward_subsumption_resolution,[status(thm)],[f136028,f136060]) ).
fof(f924145,plain,
! [X0] : v133789(X0),
inference(backward_subsumption_resolution,[status(thm)],[f136007,f136024]) ).
fof(f924147,plain,
! [X0] : ~ v133778(X0),
inference(backward_subsumption_resolution,[status(thm)],[f136014,f924143]) ).
fof(f924150,plain,
! [X0] :
( ~ v133777(X0)
| v133775(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f136002,f924145]) ).
fof(f924159,plain,
! [X0] : v133775(X0),
inference(backward_subsumption_resolution,[status(thm)],[f924150,f924160]) ).
fof(f924160,plain,
! [X0] : v133777(X0),
inference(forward_subsumption_resolution,[status(thm)],[f136010,f924147]) ).
fof(f924161,plain,
! [X0] : ~ v133774(X0),
inference(backward_subsumption_resolution,[status(thm)],[f135997,f924159]) ).
fof(f924163,plain,
! [X0] : v4(X0),
inference(backward_subsumption_resolution,[status(thm)],[f135992,f924161]) ).
fof(f924165,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f135989,f924163]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV096+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.42 % Computer : n009.cluster.edu
% 0.10/0.42 % Model : x86_64 x86_64
% 0.10/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.42 % Memory : 8046.5625MB
% 0.10/0.42 % OS : Linux 6.8.0-71-generic
% 0.10/0.42 % CPULimit : 300
% 0.10/0.42 % WCLimit : 300
% 0.10/0.42 % DateTime : Sun Sep 20 21:20:44 UTC 2026
% 0.10/0.42 % CPUTime :
% 10.31/10.62 % Drodi V4.1.1
% 63.53/17.59 % Refutation found
% 63.53/17.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 63.53/17.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 43.51/20.51 % Elapsed time: 18.461057 seconds
% 43.51/20.51 % CPU time: 65.489450 seconds
% 43.51/20.51 % Total memory used: 16.178 GB
% 43.51/20.51 % Net memory used: 16.143 GB
%------------------------------------------------------------------------------