%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS154+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/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:46:10 AM UTC 2026
% Result : Theorem 0.08s 0.47s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 23
% Syntax : Number of formulae : 96 ( 38 unt; 0 def)
% Number of atoms : 382 ( 0 equ)
% Maximal formula atoms : 26 ( 3 avg)
% Number of connectives : 527 ( 241 ~; 241 |; 34 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 28 ( 2 sgn 14 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_0,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('theBenchmark.p',axiom_0) ).
fof(axiom_1,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('theBenchmark.p',axiom_1) ).
fof(axiom_15,axiom,
! [X] :
( cC110(X)
<=> ( cC108xcomp(X)
& cC102xcomp(X) ) ),
file('theBenchmark.p',axiom_15) ).
fof(axiom_21,axiom,
! [X] :
( cC114(X)
<=> ( cC96xcomp(X)
& cC112xcomp(X) ) ),
file('theBenchmark.p',axiom_21) ).
fof(axiom_22,axiom,
! [X] :
( cC116(X)
<=> ( cC80(X)
& cC114(X) ) ),
file('theBenchmark.p',axiom_22) ).
fof(axiom_42,axiom,
! [X] :
( cC136(X)
<=> ( cC116(X)
& cC134xcomp(X) ) ),
file('theBenchmark.p',axiom_42) ).
fof(axiom_93,axiom,
! [X] :
( cC56(X)
<=> ( cC10xcomp(X)
& cC4(X) ) ),
file('theBenchmark.p',axiom_93) ).
fof(axiom_94,axiom,
! [X] :
( cC58(X)
<=> ( cC56(X)
& cC34(X) ) ),
file('theBenchmark.p',axiom_94) ).
fof(axiom_117,axiom,
! [X] :
( cC80(X)
<=> ( cC76xcomp(X)
& cC78xcomp(X) ) ),
file('theBenchmark.p',axiom_117) ).
fof(axiom_136,axiom,
! [X] :
( cC94(X)
<=> ( cC92xcomp(X)
& cC86xcomp(X) ) ),
file('theBenchmark.p',axiom_136) ).
fof(the_axiom,conjecture,
( cC56(iV822576)
& cC136(iV822576)
& cC110(iV822576)
& cC80(iV822576)
& cC94(iV822576)
& cowlThing(iV822576)
& cC114(iV822576)
& cC116(iV822576)
& cC58(iV822576)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(the_axiom_neg,negated_conjecture,
~ ( cC56(iV822576)
& cC136(iV822576)
& cC110(iV822576)
& cC80(iV822576)
& cC94(iV822576)
& cowlThing(iV822576)
& cC114(iV822576)
& cC116(iV822576)
& cC58(iV822576)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
cnf(c_163,plain,
cowlThing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_164,plain,
~ cowlNothing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_165,plain,
( ~ xsd_integer(A)
| ~ xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_166,plain,
( xsd_integer(A)
| xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_200,plain,
( ~ cC108xcomp(A)
| ~ cC102xcomp(A)
| cC110(A) ),
inference(clausify,[status(thm)],[axiom_15]) ).
cnf(c_214,plain,
( ~ cC96xcomp(A)
| ~ cC112xcomp(A)
| cC114(A) ),
inference(clausify,[status(thm)],[axiom_21]) ).
cnf(c_217,plain,
( ~ cC80(A)
| ~ cC114(A)
| cC116(A) ),
inference(clausify,[status(thm)],[axiom_22]) ).
cnf(c_268,plain,
( ~ cC116(A)
| ~ cC134xcomp(A)
| cC136(A) ),
inference(clausify,[status(thm)],[axiom_42]) ).
cnf(c_380,plain,
( ~ cC10xcomp(A)
| ~ cC4(A)
| cC56(A) ),
inference(clausify,[status(thm)],[axiom_93]) ).
cnf(c_383,plain,
( ~ cC56(A)
| ~ cC34(A)
| cC58(A) ),
inference(clausify,[status(thm)],[axiom_94]) ).
cnf(c_442,plain,
( ~ cC76xcomp(A)
| ~ cC78xcomp(A)
| cC80(A) ),
inference(clausify,[status(thm)],[axiom_117]) ).
cnf(c_487,plain,
( ~ cC92xcomp(A)
| ~ cC86xcomp(A)
| cC94(A) ),
inference(clausify,[status(thm)],[axiom_136]) ).
fof(axiom_147,axiom,
cC102xcomp(iV822576),
file('theBenchmark.p',axiom_147) ).
cnf(c_510,plain,
cC102xcomp(iV822576),
inference(clausify,[status(thm)],[axiom_147]) ).
fof(axiom_148,axiom,
cC108xcomp(iV822576),
file('theBenchmark.p',axiom_148) ).
cnf(c_511,plain,
cC108xcomp(iV822576),
inference(clausify,[status(thm)],[axiom_148]) ).
fof(axiom_149,axiom,
cC4(iV822576),
file('theBenchmark.p',axiom_149) ).
cnf(c_512,plain,
cC4(iV822576),
inference(clausify,[status(thm)],[axiom_149]) ).
fof(axiom_151,axiom,
cC112xcomp(iV822576),
file('theBenchmark.p',axiom_151) ).
cnf(c_514,plain,
cC112xcomp(iV822576),
inference(clausify,[status(thm)],[axiom_151]) ).
fof(axiom_152,axiom,
cC76xcomp(iV822576),
file('theBenchmark.p',axiom_152) ).
cnf(c_515,plain,
cC76xcomp(iV822576),
inference(clausify,[status(thm)],[axiom_152]) ).
fof(axiom_153,axiom,
cC96xcomp(iV822576),
file('theBenchmark.p',axiom_153) ).
cnf(c_516,plain,
cC96xcomp(iV822576),
inference(clausify,[status(thm)],[axiom_153]) ).
fof(axiom_158,axiom,
cC78xcomp(iV822576),
file('theBenchmark.p',axiom_158) ).
cnf(c_521,plain,
cC78xcomp(iV822576),
inference(clausify,[status(thm)],[axiom_158]) ).
fof(axiom_160,axiom,
cC134xcomp(iV822576),
file('theBenchmark.p',axiom_160) ).
cnf(c_523,plain,
cC134xcomp(iV822576),
inference(clausify,[status(thm)],[axiom_160]) ).
fof(axiom_161,axiom,
cC86xcomp(iV822576),
file('theBenchmark.p',axiom_161) ).
cnf(c_524,plain,
cC86xcomp(iV822576),
inference(clausify,[status(thm)],[axiom_161]) ).
fof(axiom_162,axiom,
cC34(iV822576),
file('theBenchmark.p',axiom_162) ).
cnf(c_525,plain,
cC34(iV822576),
inference(clausify,[status(thm)],[axiom_162]) ).
fof(axiom_167,axiom,
cC10xcomp(iV822576),
file('theBenchmark.p',axiom_167) ).
cnf(c_529,plain,
cC10xcomp(iV822576),
inference(clausify,[status(thm)],[axiom_167]) ).
fof(axiom_168,axiom,
cC92xcomp(iV822576),
file('theBenchmark.p',axiom_168) ).
cnf(c_530,plain,
cC92xcomp(iV822576),
inference(clausify,[status(thm)],[axiom_168]) ).
fof(nnf_150,plain,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ? [X] :
( ( xsd_integer(X)
| ~ xsd_string(X) )
& ( ~ xsd_integer(X)
| xsd_string(X) ) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(fof_nnf,[status(thm)],[the_axiom_neg]) ).
fof(sk_the_axiom_neg_sk,plain,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ( ( xsd_integer(sK1)
| ~ xsd_string(sK1) )
& ( ~ xsd_integer(sK1)
| xsd_string(sK1) ) )
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X,sK1)],[nnf_150]) ).
fof(sk_the_axiom_neg,plain,
( ( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ) ),
inference(cnf_transformation,[status(thm)],[sk_the_axiom_neg_sk]) ).
cnf(c_531,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_568,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_163,c_531]) ).
cnf(c_569,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_164,c_568]) ).
cnf(c_532,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_163,c_569]) ).
cnf(c_533,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_570,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_163,c_533]) ).
cnf(c_571,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_164,c_570]) ).
cnf(c_534,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_163,c_571]) ).
cnf(c_572,negated_conjecture,
( xsd_integer(sK1)
| ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_534,c_166]) ).
cnf(c_536,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1) ),
inference(copy,[status(thm)],[c_572]) ).
cnf(c_573,plain,
( ~ cC102xcomp(iV822576)
| cC110(iV822576) ),
inference(resolve,[status(thm)],[c_511,c_200]) ).
cnf(c_537,plain,
cC110(iV822576),
inference(resolve,[status(thm)],[c_510,c_573]) ).
cnf(c_538,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_537,c_536]) ).
cnf(c_539,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_537,c_532]) ).
cnf(c_574,plain,
( ~ cC78xcomp(iV822576)
| cC80(iV822576) ),
inference(resolve,[status(thm)],[c_515,c_442]) ).
cnf(c_540,plain,
cC80(iV822576),
inference(resolve,[status(thm)],[c_521,c_574]) ).
cnf(c_541,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_540,c_539]) ).
cnf(c_542,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_540,c_538]) ).
cnf(c_543,plain,
( ~ cC114(iV822576)
| cC116(iV822576) ),
inference(resolve,[status(thm)],[c_540,c_217]) ).
cnf(c_575,plain,
( ~ cC112xcomp(iV822576)
| cC114(iV822576) ),
inference(resolve,[status(thm)],[c_516,c_214]) ).
cnf(c_544,plain,
cC114(iV822576),
inference(resolve,[status(thm)],[c_514,c_575]) ).
cnf(c_545,plain,
cC116(iV822576),
inference(resolve,[status(thm)],[c_544,c_543]) ).
cnf(c_576,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC114(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_545,c_542]) ).
cnf(c_546,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_544,c_576]) ).
cnf(c_577,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC114(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_545,c_541]) ).
cnf(c_547,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_544,c_577]) ).
cnf(c_578,plain,
( ~ cC116(iV822576)
| cC136(iV822576) ),
inference(resolve,[status(thm)],[c_523,c_268]) ).
cnf(c_548,plain,
cC136(iV822576),
inference(resolve,[status(thm)],[c_545,c_578]) ).
cnf(c_549,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_548,c_547]) ).
cnf(c_550,negated_conjecture,
( ~ cC56(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_548,c_546]) ).
cnf(c_579,plain,
( ~ cC4(iV822576)
| cC56(iV822576) ),
inference(resolve,[status(thm)],[c_529,c_380]) ).
cnf(c_555,plain,
cC56(iV822576),
inference(resolve,[status(thm)],[c_512,c_579]) ).
cnf(c_557,negated_conjecture,
( ~ cC94(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_555,c_550]) ).
cnf(c_558,negated_conjecture,
( ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_555,c_549]) ).
cnf(c_580,plain,
( ~ cC34(iV822576)
| cC58(iV822576) ),
inference(resolve,[status(thm)],[c_555,c_383]) ).
cnf(c_559,plain,
cC58(iV822576),
inference(resolve,[status(thm)],[c_525,c_580]) ).
cnf(c_560,negated_conjecture,
( ~ cC94(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_559,c_558]) ).
cnf(c_561,negated_conjecture,
( ~ cC94(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_559,c_557]) ).
cnf(c_581,plain,
( ~ cC86xcomp(iV822576)
| cC94(iV822576) ),
inference(resolve,[status(thm)],[c_530,c_487]) ).
cnf(c_563,plain,
cC94(iV822576),
inference(resolve,[status(thm)],[c_524,c_581]) ).
cnf(c_564,negated_conjecture,
xsd_integer(sK1),
inference(resolve,[status(thm)],[c_563,c_561]) ).
cnf(c_582,negated_conjecture,
( ~ cC94(iV822576)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_564,c_560]) ).
cnf(c_565,negated_conjecture,
xsd_string(sK1),
inference(resolve,[status(thm)],[c_563,c_582]) ).
cnf(c_583,negated_conjecture,
~ xsd_integer(sK1),
inference(resolve,[status(thm)],[c_565,c_165]) ).
cnf(c_567,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_564,c_583]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS154+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n008.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 19:42:27 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 1707831 was started by sandbox on n008,
% 0.08/0.36 % Fri Sep 25 19:42:27 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.40
% 0.08/0.40 % From the command line: assign(max_seconds, 300).
% 0.08/0.40
% 0.08/0.40 % SInE: 163 to sos, 6 to usable, of 169 axioms (tolerance 2.00, depth 0 fixpoint).
% 0.08/0.47
% 0.08/0.47 % SZS status Theorem for theBenchmark
% 0.08/0.47
% 0.08/0.47 % Proof 1 at 0.04 (+ 0.01) seconds.
% 0.08/0.47 % Length of proof is 64.
% 0.08/0.47 % Level of proof is 12.
% 0.08/0.47 % Maximum clause weight is 102.000.
% 0.08/0.47 % Given clauses 125.
% 0.08/0.47
% 0.08/0.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------