%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : HWV095+1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:26 PM UTC 2026
% Result : Theorem 0.20s 0.64s
% Output : CNFRefutation 0.20s
% 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(f35,conjecture,
! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
~ ! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
inference(negated_conjecture,[status(cth)],[f35]) ).
fof(f37,axiom,
! [VarCurr] :
( ~ v4(VarCurr)
<=> v995(VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
! [VarCurr] :
( ~ v995(VarCurr)
<=> v996(VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [VarCurr] :
( v996(VarCurr)
<=> ( v1010(VarCurr)
& v998(VarCurr) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [VarCurr] :
( v1010(VarCurr)
<=> ( v1000(VarCurr,bitIndex1)
| v1000(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [VarCurr] :
( ~ v998(VarCurr)
<=> v999(VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [VarCurr] :
( v999(VarCurr)
<=> ( v1000(VarCurr,bitIndex1)
& v1000(VarCurr,bitIndex0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [VarCurr] :
( v1000(VarCurr,bitIndex0)
<=> v1001(VarCurr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [VarCurr] :
( v1000(VarCurr,bitIndex1)
<=> $true ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [VarCurr] :
( v1001(VarCurr)
<=> ( v1007(VarCurr,bitIndex5)
& v1003(VarCurr) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
! [VarCurr] : ~ v1007(VarCurr,bitIndex5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1198,plain,
? [VarCurr] :
( ~ v4(VarCurr)
& reachableState(VarCurr) ),
inference(pre_NNF_transformation,[status(thm)],[f36]) ).
fof(f1199,plain,
( ~ v4(sK0_skl)
& reachableState(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(VarCurr,sK0_skl)],[f1198]) ).
fof(f1201,plain,
~ v4(sK0_skl),
inference(cnf_transformation,[status(thm)],[f1199]) ).
fof(f1202,plain,
! [VarCurr] :
( ( ~ v995(VarCurr)
| ~ v4(VarCurr) )
& ( v995(VarCurr)
| v4(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f37]) ).
fof(f1203,plain,
( ! [VarCurr] :
( ~ v995(VarCurr)
| ~ v4(VarCurr) )
& ! [VarCurr] :
( v995(VarCurr)
| v4(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1202]) ).
fof(f1204,plain,
! [X0] :
( v995(X0)
| v4(X0) ),
inference(cnf_transformation,[status(thm)],[f1203]) ).
fof(f1206,plain,
! [VarCurr] :
( ( ~ v996(VarCurr)
| ~ v995(VarCurr) )
& ( v996(VarCurr)
| v995(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f38]) ).
fof(f1207,plain,
( ! [VarCurr] :
( ~ v996(VarCurr)
| ~ v995(VarCurr) )
& ! [VarCurr] :
( v996(VarCurr)
| v995(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1206]) ).
fof(f1209,plain,
! [X0] :
( ~ v996(X0)
| ~ v995(X0) ),
inference(cnf_transformation,[status(thm)],[f1207]) ).
fof(f1210,plain,
! [VarCurr] :
( ( ~ v1010(VarCurr)
| ~ v998(VarCurr)
| v996(VarCurr) )
& ( ( v1010(VarCurr)
& v998(VarCurr) )
| ~ v996(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f39]) ).
fof(f1211,plain,
( ! [VarCurr] :
( ~ v1010(VarCurr)
| ~ v998(VarCurr)
| v996(VarCurr) )
& ! [VarCurr] :
( ( v1010(VarCurr)
& v998(VarCurr) )
| ~ v996(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1210]) ).
fof(f1214,plain,
! [X0] :
( ~ v1010(X0)
| ~ v998(X0)
| v996(X0) ),
inference(cnf_transformation,[status(thm)],[f1211]) ).
fof(f1215,plain,
! [VarCurr] :
( ( ( ~ v1000(VarCurr,bitIndex1)
& ~ v1000(VarCurr,bitIndex0) )
| v1010(VarCurr) )
& ( v1000(VarCurr,bitIndex1)
| v1000(VarCurr,bitIndex0)
| ~ v1010(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f40]) ).
fof(f1216,plain,
( ! [VarCurr] :
( ( ~ v1000(VarCurr,bitIndex1)
& ~ v1000(VarCurr,bitIndex0) )
| v1010(VarCurr) )
& ! [VarCurr] :
( v1000(VarCurr,bitIndex1)
| v1000(VarCurr,bitIndex0)
| ~ v1010(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1215]) ).
fof(f1219,plain,
! [X0] :
( ~ v1000(X0,bitIndex1)
| v1010(X0) ),
inference(cnf_transformation,[status(thm)],[f1216]) ).
fof(f1220,plain,
! [VarCurr] :
( ( ~ v999(VarCurr)
| ~ v998(VarCurr) )
& ( v999(VarCurr)
| v998(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f41]) ).
fof(f1221,plain,
( ! [VarCurr] :
( ~ v999(VarCurr)
| ~ v998(VarCurr) )
& ! [VarCurr] :
( v999(VarCurr)
| v998(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1220]) ).
fof(f1222,plain,
! [X0] :
( v999(X0)
| v998(X0) ),
inference(cnf_transformation,[status(thm)],[f1221]) ).
fof(f1224,plain,
! [VarCurr] :
( ( ~ v1000(VarCurr,bitIndex1)
| ~ v1000(VarCurr,bitIndex0)
| v999(VarCurr) )
& ( ( v1000(VarCurr,bitIndex1)
& v1000(VarCurr,bitIndex0) )
| ~ v999(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f42]) ).
fof(f1225,plain,
( ! [VarCurr] :
( ~ v1000(VarCurr,bitIndex1)
| ~ v1000(VarCurr,bitIndex0)
| v999(VarCurr) )
& ! [VarCurr] :
( ( v1000(VarCurr,bitIndex1)
& v1000(VarCurr,bitIndex0) )
| ~ v999(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1224]) ).
fof(f1226,plain,
! [X0] :
( v1000(X0,bitIndex0)
| ~ v999(X0) ),
inference(cnf_transformation,[status(thm)],[f1225]) ).
fof(f1229,plain,
! [VarCurr] :
( ( ~ v1001(VarCurr)
| v1000(VarCurr,bitIndex0) )
& ( v1001(VarCurr)
| ~ v1000(VarCurr,bitIndex0) ) ),
inference(NNF_transformation,[status(thm)],[f43]) ).
fof(f1230,plain,
( ! [VarCurr] :
( ~ v1001(VarCurr)
| v1000(VarCurr,bitIndex0) )
& ! [VarCurr] :
( v1001(VarCurr)
| ~ v1000(VarCurr,bitIndex0) ) ),
inference(miniscoping,[status(thm)],[f1229]) ).
fof(f1231,plain,
! [X0] :
( v1001(X0)
| ~ v1000(X0,bitIndex0) ),
inference(cnf_transformation,[status(thm)],[f1230]) ).
fof(f1233,plain,
! [VarCurr] :
( ( $false
| v1000(VarCurr,bitIndex1) )
& ( $true
| ~ v1000(VarCurr,bitIndex1) ) ),
inference(NNF_transformation,[status(thm)],[f44]) ).
fof(f1234,plain,
( ( $false
| ! [VarCurr] : v1000(VarCurr,bitIndex1) )
& ( $true
| ! [VarCurr] : ~ v1000(VarCurr,bitIndex1) ) ),
inference(miniscoping,[status(thm)],[f1233]) ).
fof(f1235,plain,
! [VarCurr] : v1000(VarCurr,bitIndex1),
inference(true_and_false_simplification,[status(thm)],[f1234]) ).
fof(f1236,plain,
! [X0] : v1000(X0,bitIndex1),
inference(cnf_transformation,[status(thm)],[f1235]) ).
fof(f1237,plain,
! [VarCurr] :
( ( ~ v1007(VarCurr,bitIndex5)
| ~ v1003(VarCurr)
| v1001(VarCurr) )
& ( ( v1007(VarCurr,bitIndex5)
& v1003(VarCurr) )
| ~ v1001(VarCurr) ) ),
inference(NNF_transformation,[status(thm)],[f45]) ).
fof(f1238,plain,
( ! [VarCurr] :
( ~ v1007(VarCurr,bitIndex5)
| ~ v1003(VarCurr)
| v1001(VarCurr) )
& ! [VarCurr] :
( ( v1007(VarCurr,bitIndex5)
& v1003(VarCurr) )
| ~ v1001(VarCurr) ) ),
inference(miniscoping,[status(thm)],[f1237]) ).
fof(f1240,plain,
! [X0] :
( v1007(X0,bitIndex5)
| ~ v1001(X0) ),
inference(cnf_transformation,[status(thm)],[f1238]) ).
fof(f1272,plain,
! [X0] : ~ v1007(X0,bitIndex5),
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f7101,plain,
! [X0] : v1010(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1219,f1236]) ).
fof(f7102,plain,
! [X0] :
( ~ v998(X0)
| v996(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f1214,f7101]) ).
fof(f7104,plain,
! [X0] : ~ v1001(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1240,f1272]) ).
fof(f7106,plain,
! [X0] : ~ v1000(X0,bitIndex0),
inference(backward_subsumption_resolution,[status(thm)],[f1231,f7104]) ).
fof(f7149,plain,
! [X0] : ~ v999(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1226,f7106]) ).
fof(f7150,plain,
! [X0] : v998(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1222,f7149]) ).
fof(f7218,plain,
! [X0] : ~ v995(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1209,f7219]) ).
fof(f7219,plain,
! [X0] : v996(X0),
inference(forward_subsumption_resolution,[status(thm)],[f7102,f7150]) ).
fof(f7220,plain,
! [X0] : v4(X0),
inference(backward_subsumption_resolution,[status(thm)],[f1204,f7218]) ).
fof(f7222,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f1201,f7220]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV095+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n007.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 20 21:18:21 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.20/0.46 % Drodi V4.1.1
% 0.20/0.64 % Refutation found
% 0.20/0.64 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/0.64 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.27/0.67 % Elapsed time: 0.284345 seconds
% 0.27/0.67 % CPU time: 1.351339 seconds
% 0.27/0.67 % Total memory used: 233.850 MB
% 0.27/0.67 % Net memory used: 233.182 MB
%------------------------------------------------------------------------------