%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : HWV095+1 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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 : Sun Sep 27 07:34:43 AM UTC 2026
% Result : Theorem 4.96s 2.49s
% Output : CNFRefutation 4.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 11
% Syntax : Number of formulae : 35 ( 13 unt; 0 def)
% Number of atoms : 62 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 49 ( 22 ~; 11 |; 5 &)
% ( 9 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 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 : 32 ( 10 sgn 12 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(writeUnaryOperator_113,axiom,
! [VarCurr] :
( ~ v4(VarCurr)
<=> v995(VarCurr) ),
file('theBenchmark.p',writeUnaryOperator_113) ).
fof(writeUnaryOperator_112,axiom,
! [VarCurr] :
( ~ v995(VarCurr)
<=> v996(VarCurr) ),
file('theBenchmark.p',writeUnaryOperator_112) ).
fof(writeBinaryOperatorEqualRangesSingleBits_170,axiom,
! [VarCurr] :
( v996(VarCurr)
<=> ( v1010(VarCurr)
& v998(VarCurr) ) ),
file('theBenchmark.p',writeBinaryOperatorEqualRangesSingleBits_170) ).
fof(writeBinaryOperatorShiftedRanges_80,axiom,
! [VarCurr] :
( v1010(VarCurr)
<=> ( v1000(VarCurr,bitIndex1)
| v1000(VarCurr,bitIndex0) ) ),
file('theBenchmark.p',writeBinaryOperatorShiftedRanges_80) ).
fof(writeUnaryOperator_111,axiom,
! [VarCurr] :
( ~ v998(VarCurr)
<=> v999(VarCurr) ),
file('theBenchmark.p',writeUnaryOperator_111) ).
fof(writeBinaryOperatorShiftedRanges_79,axiom,
! [VarCurr] :
( v999(VarCurr)
<=> ( v1000(VarCurr,bitIndex1)
& v1000(VarCurr,bitIndex0) ) ),
file('theBenchmark.p',writeBinaryOperatorShiftedRanges_79) ).
fof(addAssignment_245,axiom,
! [VarCurr] :
( v1000(VarCurr,bitIndex0)
<=> v1001(VarCurr) ),
file('theBenchmark.p',addAssignment_245) ).
fof(addAssignment_244,axiom,
! [VarCurr] :
( v1000(VarCurr,bitIndex1)
<=> $true ),
file('theBenchmark.p',addAssignment_244) ).
fof(writeBinaryOperatorShiftedRanges_78,axiom,
! [VarCurr] :
( v1001(VarCurr)
<=> ( v1007(VarCurr,bitIndex5)
& v1003(VarCurr) ) ),
file('theBenchmark.p',writeBinaryOperatorShiftedRanges_78) ).
fof(addZeroExtensionConstraint_3,axiom,
! [VarCurr] : ~ v1007(VarCurr,bitIndex5),
file('theBenchmark.p',addZeroExtensionConstraint_3) ).
fof(addAssertion,conjecture,
! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
file('theBenchmark.p',addAssertion) ).
fof(addAssertion_neg,negated_conjecture,
~ ! [VarCurr] :
( reachableState(VarCurr)
=> v4(VarCurr) ),
inference(assume_negation,[status(cth)],[addAssertion]) ).
cnf(c_4762,plain,
( v995(A)
| v4(A) ),
inference(clausify,[status(thm)],[writeUnaryOperator_113]) ).
cnf(c_4765,plain,
( ~ v996(A)
| ~ v995(A) ),
inference(clausify,[status(thm)],[writeUnaryOperator_112]) ).
cnf(c_4768,plain,
( ~ v1010(A)
| ~ v998(A)
| v996(A) ),
inference(clausify,[status(thm)],[writeBinaryOperatorEqualRangesSingleBits_170]) ).
cnf(c_4771,plain,
( ~ v1000(A,bitIndex1)
| v1010(A) ),
inference(clausify,[status(thm)],[writeBinaryOperatorShiftedRanges_80]) ).
cnf(c_4772,plain,
( v999(A)
| v998(A) ),
inference(clausify,[status(thm)],[writeUnaryOperator_111]) ).
cnf(c_4774,plain,
( v1000(A,bitIndex0)
| ~ v999(A) ),
inference(clausify,[status(thm)],[writeBinaryOperatorShiftedRanges_79]) ).
cnf(c_4777,plain,
( v1001(A)
| ~ v1000(A,bitIndex0) ),
inference(clausify,[status(thm)],[addAssignment_245]) ).
cnf(c_4779,plain,
v1000(A,bitIndex1),
inference(clausify,[status(thm)],[addAssignment_244]) ).
cnf(c_4781,plain,
( v1007(A,bitIndex5)
| ~ v1001(A) ),
inference(clausify,[status(thm)],[writeBinaryOperatorShiftedRanges_78]) ).
cnf(c_4801,plain,
~ v1007(A,bitIndex5),
inference(clausify,[status(thm)],[addZeroExtensionConstraint_3]) ).
fof(nnf_928,plain,
? [VarCurr] :
( ~ v4(VarCurr)
& reachableState(VarCurr) ),
inference(fof_nnf,[status(thm)],[addAssertion_neg]) ).
fof(sk_addAssertion_neg,plain,
( ~ v4(sK0)
& reachableState(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(VarCurr,sK0)],[nnf_928]) ).
cnf(c_4875,negated_conjecture,
~ v4(sK0),
inference(split_conjunct,[status(thm)],[sk_addAssertion_neg]) ).
cnf(c_4877,plain,
v1010(A),
inference(resolve,[status(thm)],[c_4779,c_4771]) ).
cnf(c_4879,plain,
~ v1001(A),
inference(resolve,[status(thm)],[c_4801,c_4781]) ).
cnf(c_4884,plain,
( ~ v998(A)
| v996(A) ),
inference(resolve,[status(thm)],[c_4877,c_4768]) ).
cnf(c_4885,plain,
~ v1000(A,bitIndex0),
inference(resolve,[status(thm)],[c_4879,c_4777]) ).
cnf(c_4888,plain,
~ v999(A),
inference(resolve,[status(thm)],[c_4885,c_4774]) ).
cnf(c_4891,plain,
v998(A),
inference(resolve,[status(thm)],[c_4888,c_4772]) ).
cnf(c_4892,plain,
v996(A),
inference(resolve,[status(thm)],[c_4891,c_4884]) ).
cnf(c_4893,plain,
~ v995(A),
inference(resolve,[status(thm)],[c_4892,c_4765]) ).
cnf(c_4894,plain,
v4(A),
inference(resolve,[status(thm)],[c_4893,c_4762]) ).
cnf(c_4895,plain,
$false,
inference(resolve,[status(thm)],[c_4894,c_4875]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV095+1 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.39 % Computer : n008.cluster.edu
% 0.09/0.39 % Model : x86_64 x86_64
% 0.09/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.39 % Memory : 8046.5625MB
% 0.09/0.39 % OS : Linux 6.8.0-71-generic
% 0.09/0.39 % CPULimit : 300
% 0.09/0.39 % WCLimit : 300
% 0.09/0.39 % DateTime : Fri Sep 25 16:38:24 UTC 2026
% 0.09/0.39 % CPUTime :
% 0.09/0.40 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.40 % Process 1472185 was started by sandbox2 on n008,
% 0.09/0.40 % Fri Sep 25 16:38:24 2026
% 0.09/0.40 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 1.53/1.84
% 1.53/1.84 % From the command line: assign(max_seconds, 300).
% 1.53/1.84
% 1.53/1.84 % SInE: 55 to sos, 1100 to usable, of 1155 axioms (tolerance 2.00, depth 0 fixpoint).
% 4.96/2.49
% 4.96/2.49 % SZS status Theorem for theBenchmark
% 4.96/2.49
% 4.96/2.49 % Proof 1 at 0.38 (+ 0.11) seconds.
% 4.96/2.49 % Length of proof is 32.
% 4.96/2.49 % Level of proof is 9.
% 4.96/2.49 % Maximum clause weight is 608.000.
% 4.96/2.49 % Given clauses 0.
% 4.96/2.49
% 4.96/2.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------