%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS149+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 : n020.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:09 AM UTC 2026
% Result : Theorem 0.11s 0.94s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 15
% Syntax : Number of formulae : 84 ( 20 unt; 0 def)
% Number of atoms : 428 ( 0 equ)
% Maximal formula atoms : 24 ( 5 avg)
% Number of connectives : 663 ( 319 ~; 305 |; 30 &)
% ( 9 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 29 ( 2 sgn 12 !; 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_24,axiom,
! [X] :
( cC14(X)
<=> ( ~ cC2(X)
& ~ cC12(X) ) ),
file('theBenchmark.p',axiom_24) ).
fof(axiom_65,axiom,
! [X] :
( cC216(X)
<=> ( cC64(X)
& ~ cC214(X) ) ),
file('theBenchmark.p',axiom_65) ).
fof(axiom_69,axiom,
! [X] :
( cC28(X)
<=> ( ~ cC16(X)
& ~ cC26(X) ) ),
file('theBenchmark.p',axiom_69) ).
fof(axiom_70,axiom,
! [X] :
( cC30(X)
<=> ( cC28(X)
& cC14(X) ) ),
file('theBenchmark.p',axiom_70) ).
fof(axiom_78,axiom,
! [X] :
( cC46(X)
<=> ( cC44(X)
& cC30(X) ) ),
file('theBenchmark.p',axiom_78) ).
fof(axiom_107,axiom,
! [X] :
( cTEST(X)
<=> ( cC46(X)
& cC216(X) ) ),
file('theBenchmark.p',axiom_107) ).
fof(the_axiom,conjecture,
( cowlThing(iV3102)
& cC14(iV3102)
& cC64(iV3102)
& cC28(iV3102)
& cC44(iV3102)
& cC30(iV3102)
& cC46(iV3102)
& cC216(iV3102)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(the_axiom_neg,negated_conjecture,
~ ( cowlThing(iV3102)
& cC14(iV3102)
& cC64(iV3102)
& cC28(iV3102)
& cC44(iV3102)
& cC30(iV3102)
& cC46(iV3102)
& cC216(iV3102)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
fof(nnf_114,plain,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ? [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,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ( ( 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_114]) ).
fof(sk_the_axiom_neg,plain,
( ( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ) ),
inference(cnf_transformation,[status(thm)],[sk_the_axiom_neg_sk]) ).
cnf(c_115,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_116,plain,
~ cowlNothing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_117,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_118,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| ~ cowlThing(sK0) ),
inference(resolve,[status(thm)],[c_115,c_116]) ).
cnf(c_119,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| ~ cowlThing(sK0) ),
inference(resolve,[status(thm)],[c_117,c_116]) ).
cnf(c_120,plain,
( xsd_integer(A)
| xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_121,plain,
( ~ xsd_integer(A)
| ~ xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_141,plain,
( cC2(A)
| cC12(A)
| cC14(A) ),
inference(clausify,[status(thm)],[axiom_24]) ).
fof(axiom_122,axiom,
~ cC2(iV3102),
file('theBenchmark.p',axiom_122) ).
cnf(c_146,plain,
~ cC2(iV3102),
inference(clausify,[status(thm)],[axiom_122]) ).
cnf(c_235,plain,
( cC14(A)
| ~ cC30(A) ),
inference(clausify,[status(thm)],[axiom_70]) ).
cnf(c_237,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_integer(sK1)
| ~ cowlThing(sK0)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_120,c_119]) ).
cnf(c_238,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC14(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ~ xsd_integer(sK1)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_121,c_118]) ).
cnf(c_239,plain,
( ~ cC28(A)
| ~ cC14(A)
| cC30(A) ),
inference(clausify,[status(thm)],[axiom_70]) ).
cnf(c_248,plain,
( cC12(iV3102)
| cC14(iV3102) ),
inference(resolve,[status(thm)],[c_146,c_141]) ).
cnf(c_412,plain,
( ~ cC64(A)
| cC214(A)
| cC216(A) ),
inference(clausify,[status(thm)],[axiom_65]) ).
fof(axiom_118,axiom,
~ cC214(iV3102),
file('theBenchmark.p',axiom_118) ).
cnf(c_413,plain,
~ cC214(iV3102),
inference(clausify,[status(thm)],[axiom_118]) ).
cnf(c_424,plain,
( ~ cC64(iV3102)
| cC216(iV3102) ),
inference(resolve,[status(thm)],[c_412,c_413]) ).
cnf(c_425,plain,
( cC64(A)
| ~ cC216(A) ),
inference(clausify,[status(thm)],[axiom_65]) ).
cnf(c_426,plain,
( cC216(A)
| ~ cTEST(A) ),
inference(clausify,[status(thm)],[axiom_107]) ).
cnf(c_428,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| xsd_integer(sK1)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_235,c_237]) ).
cnf(c_429,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cC216(iV3102)
| ~ xsd_integer(sK1)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_235,c_238]) ).
cnf(c_436,plain,
( cC16(A)
| cC26(A)
| cC28(A) ),
inference(clausify,[status(thm)],[axiom_69]) ).
cnf(c_439,plain,
( cC28(A)
| ~ cC30(A) ),
inference(clausify,[status(thm)],[axiom_70]) ).
cnf(c_442,plain,
( ~ cC28(iV3102)
| cC30(iV3102)
| cC12(iV3102) ),
inference(resolve,[status(thm)],[c_248,c_239]) ).
cnf(c_445,negated_conjecture,
( ~ cC64(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| xsd_integer(sK1)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_428,c_424]) ).
cnf(c_447,negated_conjecture,
( ~ cC64(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC28(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ xsd_integer(sK1)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_429,c_424]) ).
cnf(c_468,plain,
( cC44(A)
| ~ cC46(A) ),
inference(clausify,[status(thm)],[axiom_78]) ).
cnf(c_471,negated_conjecture,
( ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| xsd_integer(sK1)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_445,c_439]) ).
cnf(c_473,negated_conjecture,
( ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC44(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ xsd_integer(sK1)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_447,c_439]) ).
fof(axiom_108,axiom,
cTEST(iV3102),
file('theBenchmark.p',axiom_108) ).
cnf(c_565,plain,
cTEST(iV3102),
inference(clausify,[status(thm)],[axiom_108]) ).
cnf(c_566,plain,
( cC46(A)
| ~ cTEST(A) ),
inference(clausify,[status(thm)],[axiom_107]) ).
cnf(c_567,plain,
( cC64(A)
| ~ cTEST(A) ),
inference(resolve,[status(thm)],[c_426,c_425]) ).
cnf(c_577,plain,
cC64(iV3102),
inference(resolve,[status(thm)],[c_567,c_565]) ).
cnf(c_578,plain,
cC46(iV3102),
inference(resolve,[status(thm)],[c_565,c_566]) ).
cnf(c_604,negated_conjecture,
( ~ cC46(iV3102)
| ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ xsd_integer(sK1)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_473,c_468]) ).
cnf(c_910,negated_conjecture,
( ~ cC46(iV3102)
| ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(copy,[status(thm)],[c_604]) ).
cnf(c_911,negated_conjecture,
( ~ cC46(iV3102)
| ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(copy,[status(thm)],[c_910]) ).
cnf(c_912,negated_conjecture,
( ~ cC46(iV3102)
| ~ cC30(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(copy,[status(thm)],[c_911]) ).
cnf(c_913,negated_conjecture,
( ~ cC46(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(copy,[status(thm)],[c_912]) ).
cnf(c_914,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(copy,[status(thm)],[c_913]) ).
cnf(c_915,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_578,c_914]) ).
cnf(c_605,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_577,c_915]) ).
cnf(c_606,negated_conjecture,
( ~ cC46(iV3102)
| ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| xsd_integer(sK1)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_471,c_468]) ).
cnf(c_916,negated_conjecture,
( ~ cC46(iV3102)
| ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC30(iV3102)
| ~ cC46(iV3102)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(copy,[status(thm)],[c_606]) ).
cnf(c_917,negated_conjecture,
( ~ cC46(iV3102)
| ~ cC30(iV3102)
| ~ cC64(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(copy,[status(thm)],[c_916]) ).
cnf(c_918,negated_conjecture,
( ~ cC46(iV3102)
| ~ cC30(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(copy,[status(thm)],[c_917]) ).
cnf(c_919,negated_conjecture,
( ~ cC46(iV3102)
| ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(copy,[status(thm)],[c_918]) ).
cnf(c_920,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cC46(iV3102)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(copy,[status(thm)],[c_919]) ).
cnf(c_921,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cC64(iV3102)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_578,c_920]) ).
cnf(c_607,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC30(iV3102) ),
inference(resolve,[status(thm)],[c_577,c_921]) ).
cnf(c_619,plain,
( cC16(iV3102)
| cC26(iV3102)
| cC30(iV3102)
| cC12(iV3102) ),
inference(resolve,[status(thm)],[c_442,c_436]) ).
fof(axiom_121,axiom,
~ cC16(iV3102),
file('theBenchmark.p',axiom_121) ).
cnf(c_749,plain,
~ cC16(iV3102),
inference(clausify,[status(thm)],[axiom_121]) ).
fof(axiom_116,axiom,
~ cC26(iV3102),
file('theBenchmark.p',axiom_116) ).
cnf(c_752,plain,
~ cC26(iV3102),
inference(clausify,[status(thm)],[axiom_116]) ).
fof(axiom_115,axiom,
~ cC12(iV3102),
file('theBenchmark.p',axiom_115) ).
cnf(c_753,plain,
~ cC12(iV3102),
inference(clausify,[status(thm)],[axiom_115]) ).
cnf(c_791,plain,
cowlThing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_922,plain,
( cC16(iV3102)
| cC26(iV3102)
| cC30(iV3102) ),
inference(resolve,[status(thm)],[c_753,c_619]) ).
cnf(c_923,plain,
( cC16(iV3102)
| cC30(iV3102) ),
inference(resolve,[status(thm)],[c_752,c_922]) ).
cnf(c_907,plain,
cC30(iV3102),
inference(resolve,[status(thm)],[c_749,c_923]) ).
cnf(c_924,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK0)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_907,c_607]) ).
cnf(c_925,negated_conjecture,
( ~ cowlThing(iV3102)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_791,c_924]) ).
cnf(c_908,negated_conjecture,
xsd_integer(sK1),
inference(resolve,[status(thm)],[c_791,c_925]) ).
cnf(c_926,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_907,c_605]) ).
cnf(c_927,negated_conjecture,
( ~ cowlThing(iV3102)
| ~ cowlThing(sK0) ),
inference(resolve,[status(thm)],[c_908,c_926]) ).
cnf(c_928,negated_conjecture,
~ cowlThing(iV3102),
inference(resolve,[status(thm)],[c_791,c_927]) ).
cnf(c_909,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_791,c_928]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS149+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.57 % Computer : n020.cluster.edu
% 0.07/0.57 % Model : x86_64 x86_64
% 0.07/0.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.57 % Memory : 8046.5625MB
% 0.07/0.57 % OS : Linux 6.8.0-71-generic
% 0.07/0.57 % CPULimit : 300
% 0.07/0.57 % WCLimit : 300
% 0.07/0.57 % DateTime : Fri Sep 25 19:42:20 UTC 2026
% 0.07/0.57 % CPUTime :
% 0.07/0.57 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.57 % Process 3604251 was started by sandbox on n020,
% 0.07/0.57 % Fri Sep 25 19:42:20 2026
% 0.07/0.57 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/0.60
% 0.07/0.60 % From the command line: assign(max_seconds, 300).
% 0.11/0.94
% 0.11/0.94 % SZS status Theorem for theBenchmark
% 0.11/0.94
% 0.11/0.94 % Proof 1 at 0.32 (+ 0.01) seconds.
% 0.11/0.94 % Length of proof is 55.
% 0.11/0.94 % Level of proof is 10.
% 0.11/0.94 % Maximum clause weight is 13.000.
% 0.11/0.94 % Given clauses 0.
% 0.11/0.94
% 0.11/0.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------