%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV091+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 : n026.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 14.95s 4.15s
% Output : CNFRefutation 14.95s
% 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(f447,conjecture,
! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f448,negated_conjecture,
~ ! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
inference(negated_conjecture,[status(cth)],[f447]) ).
fof(f449,axiom,
! [VarCurr] :
( ~ v4(VarCurr)
<=> v22287(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f450,axiom,
! [VarCurr] :
( ~ v22287(VarCurr)
<=> v22288(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f451,axiom,
! [VarCurr] :
( v22288(VarCurr)
<=> ( v22314(VarCurr)
& v22290(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f452,axiom,
! [VarCurr] :
( v22314(VarCurr)
<=> ( v22292(VarCurr,bitIndex1)
| v22292(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f453,axiom,
! [VarCurr] :
( ~ v22290(VarCurr)
<=> v22291(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f454,axiom,
! [VarCurr] :
( v22291(VarCurr)
<=> ( v22292(VarCurr,bitIndex1)
& v22292(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f455,axiom,
! [VarCurr] :
( v22292(VarCurr,bitIndex0)
<=> v22293(VarCurr) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f456,axiom,
! [VarCurr] :
( v22292(VarCurr,bitIndex1)
<=> $true ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f457,axiom,
! [VarCurr] :
( v22293(VarCurr)
<=> ( v22296(VarCurr,bitIndex9)
& v22295(VarCurr) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f481,axiom,
! [VarCurr] : ~ v22296(VarCurr,bitIndex9),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27564,plain,
? [VarCurr] :
( ~ v4(VarCurr)
& reachableState(VarCurr) ),
inference(pre_NNF_transformation,[status(thm)],[f448]) ).
fof(f27565,plain,
( ~ v4(sK0_skl)
& reachableState(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f27564]) ).
fof(f27567,plain,
~ v4(sK0_skl),
inference(cnf_transformation,[status(thm)],[f27565]) ).
fof(f27568,plain,
! [VarCurr] :
( ( ~ v22287(VarCurr)
| ~ v4(VarCurr) )
& ( v22287(VarCurr)
| v4(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f449]) ).
fof(f27569,plain,
( ! [VarCurr] :
( ~ v22287(VarCurr)
| ~ v4(VarCurr) )
& ! [VarCurr] :
( v22287(VarCurr)
| v4(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f27568]) ).
fof(f27570,plain,
! [X0] :
( v22287(X0)
| v4(X0) ),
inference(cnf_transformation,[status(thm)],[f27569]) ).
fof(f27572,plain,
! [VarCurr] :
( ( ~ v22288(VarCurr)
| ~ v22287(VarCurr) )
& ( v22288(VarCurr)
| v22287(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f450]) ).
fof(f27573,plain,
( ! [VarCurr] :
( ~ v22288(VarCurr)
| ~ v22287(VarCurr) )
& ! [VarCurr] :
( v22288(VarCurr)
| v22287(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f27572]) ).
fof(f27575,plain,
! [X0] :
( ~ v22288(X0)
| ~ v22287(X0) ),
inference(cnf_transformation,[status(thm)],[f27573]) ).
fof(f27576,plain,
! [VarCurr] :
( ( ~ v22314(VarCurr)
| ~ v22290(VarCurr)
| v22288(VarCurr) )
& ( ( v22314(VarCurr)
& v22290(VarCurr) )
| ~ v22288(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f451]) ).
fof(f27577,plain,
( ! [VarCurr] :
( ~ v22314(VarCurr)
| ~ v22290(VarCurr)
| v22288(VarCurr) )
& ! [VarCurr] :
( ( v22314(VarCurr)
& v22290(VarCurr) )
| ~ v22288(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f27576]) ).
fof(f27580,plain,
! [X0] :
( ~ v22314(X0)
| ~ v22290(X0)
| v22288(X0) ),
inference(cnf_transformation,[status(thm)],[f27577]) ).
fof(f27581,plain,
! [VarCurr] :
( ( ( ~ v22292(VarCurr,bitIndex1)
& ~ v22292(VarCurr,bitIndex0) )
| v22314(VarCurr) )
& ( v22292(VarCurr,bitIndex1)
| v22292(VarCurr,bitIndex0)
| ~ v22314(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f452]) ).
fof(f27582,plain,
( ! [VarCurr] :
( ( ~ v22292(VarCurr,bitIndex1)
& ~ v22292(VarCurr,bitIndex0) )
| v22314(VarCurr) )
& ! [VarCurr] :
( v22292(VarCurr,bitIndex1)
| v22292(VarCurr,bitIndex0)
| ~ v22314(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f27581]) ).
fof(f27585,plain,
! [X0] :
( ~ v22292(X0,bitIndex1)
| v22314(X0) ),
inference(cnf_transformation,[status(thm)],[f27582]) ).
fof(f27586,plain,
! [VarCurr] :
( ( ~ v22291(VarCurr)
| ~ v22290(VarCurr) )
& ( v22291(VarCurr)
| v22290(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f453]) ).
fof(f27587,plain,
( ! [VarCurr] :
( ~ v22291(VarCurr)
| ~ v22290(VarCurr) )
& ! [VarCurr] :
( v22291(VarCurr)
| v22290(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f27586]) ).
fof(f27588,plain,
! [X0] :
( v22291(X0)
| v22290(X0) ),
inference(cnf_transformation,[status(thm)],[f27587]) ).
fof(f27590,plain,
! [VarCurr] :
( ( ~ v22292(VarCurr,bitIndex1)
| ~ v22292(VarCurr,bitIndex0)
| v22291(VarCurr) )
& ( ( v22292(VarCurr,bitIndex1)
& v22292(VarCurr,bitIndex0) )
| ~ v22291(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f454]) ).
fof(f27591,plain,
( ! [VarCurr] :
( ~ v22292(VarCurr,bitIndex1)
| ~ v22292(VarCurr,bitIndex0)
| v22291(VarCurr) )
& ! [VarCurr] :
( ( v22292(VarCurr,bitIndex1)
& v22292(VarCurr,bitIndex0) )
| ~ v22291(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f27590]) ).
fof(f27592,plain,
! [X0] :
( v22292(X0,bitIndex0)
| ~ v22291(X0) ),
inference(cnf_transformation,[status(thm)],[f27591]) ).
fof(f27595,plain,
! [VarCurr] :
( ( ~ v22293(VarCurr)
| v22292(VarCurr,bitIndex0) )
& ( v22293(VarCurr)
| ~ v22292(VarCurr,bitIndex0) ) ),
inference(NNF_transformation,[status(thm)],[f455]) ).
fof(f27596,plain,
( ! [VarCurr] :
( ~ v22293(VarCurr)
| v22292(VarCurr,bitIndex0) )
& ! [VarCurr] :
( v22293(VarCurr)
| ~ v22292(VarCurr,bitIndex0) ) ),
inference(miniscoping,[status(thm)],[f27595]) ).
fof(f27597,plain,
! [X0] :
( v22293(X0)
| ~ v22292(X0,bitIndex0) ),
inference(cnf_transformation,[status(thm)],[f27596]) ).
fof(f27599,plain,
! [VarCurr] :
( ( $false
| v22292(VarCurr,bitIndex1) )
& ( $true
| ~ v22292(VarCurr,bitIndex1) ) ),
inference(NNF_transformation,[status(thm)],[f456]) ).
fof(f27600,plain,
( ( $false
| ! [VarCurr] : v22292(VarCurr,bitIndex1) )
& ( $true
| ! [VarCurr] : ~ v22292(VarCurr,bitIndex1) ) ),
inference(miniscoping,[status(thm)],[f27599]) ).
fof(f27601,plain,
! [VarCurr] : v22292(VarCurr,bitIndex1),
inference(true_and_false_simplification,[status(thm)],[f27600]) ).
fof(f27602,plain,
! [X0] : v22292(X0,bitIndex1),
inference(cnf_transformation,[status(thm)],[f27601]) ).
fof(f27603,plain,
! [VarCurr] :
( ( ~ v22296(VarCurr,bitIndex9)
| ~ v22295(VarCurr)
| v22293(VarCurr) )
& ( ( v22296(VarCurr,bitIndex9)
& v22295(VarCurr) )
| ~ v22293(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f457]) ).
fof(f27604,plain,
( ! [VarCurr] :
( ~ v22296(VarCurr,bitIndex9)
| ~ v22295(VarCurr)
| v22293(VarCurr) )
& ! [VarCurr] :
( ( v22296(VarCurr,bitIndex9)
& v22295(VarCurr) )
| ~ v22293(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f27603]) ).
fof(f27606,plain,
! [X0] :
( v22296(X0,bitIndex9)
| ~ v22293(X0) ),
inference(cnf_transformation,[status(thm)],[f27604]) ).
fof(f27698,plain,
! [X0] : ~ v22296(X0,bitIndex9),
inference(cnf_transformation,[status(thm)],[f481]) ).
fof(f185951,plain,
! [X0] : v22314(X0),
inference(backward_subsumption_resolution,[status(thm)],[f27585,f27602]) ).
fof(f185952,plain,
! [X0] :
( ~ v22290(X0)
| v22288(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f27580,f185951]) ).
fof(f185989,plain,
! [X0] : ~ v22293(X0),
inference(backward_subsumption_resolution,[status(thm)],[f27606,f27698]) ).
fof(f185990,plain,
! [X0] : ~ v22292(X0,bitIndex0),
inference(backward_subsumption_resolution,[status(thm)],[f27597,f185989]) ).
fof(f186226,plain,
! [X0] : ~ v22291(X0),
inference(backward_subsumption_resolution,[status(thm)],[f27592,f185990]) ).
fof(f186227,plain,
! [X0] : v22290(X0),
inference(backward_subsumption_resolution,[status(thm)],[f27588,f186226]) ).
fof(f188386,plain,
! [X0] : ~ v22287(X0),
inference(backward_subsumption_resolution,[status(thm)],[f27575,f188387]) ).
fof(f188387,plain,
! [X0] : v22288(X0),
inference(forward_subsumption_resolution,[status(thm)],[f185952,f186227]) ).
fof(f188388,plain,
! [X0] : v4(X0),
inference(backward_subsumption_resolution,[status(thm)],[f27570,f188386]) ).
fof(f188390,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f27567,f188388]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV091+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.42 % Computer : n026.cluster.edu
% 0.13/0.42 % Model : x86_64 x86_64
% 0.13/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.42 % Memory : 8046.5625MB
% 0.13/0.42 % OS : Linux 6.8.0-71-generic
% 0.13/0.42 % CPULimit : 300
% 0.13/0.42 % WCLimit : 300
% 0.13/0.42 % DateTime : Sun Sep 20 21:21:37 UTC 2026
% 0.13/0.42 % CPUTime :
% 2.14/2.47 % Drodi V4.1.1
% 14.95/4.15 % Refutation found
% 14.95/4.15 % SZS status Theorem for theBenchmark: Theorem is valid
% 14.95/4.15 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.88/4.94 % Elapsed time: 4.412838 seconds
% 2.88/4.94 % CPU time: 15.951180 seconds
% 2.88/4.94 % Total memory used: 3.527 GB
% 2.88/4.94 % Net memory used: 3.519 GB
%------------------------------------------------------------------------------