%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS146+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 : n002.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:08 AM UTC 2026
% Result : Theorem 17.62s 2.69s
% Output : CNFRefutation 17.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 22
% Syntax : Number of formulae : 104 ( 33 unt; 0 def)
% Number of atoms : 477 ( 0 equ)
% Maximal formula atoms : 26 ( 4 avg)
% Number of connectives : 723 ( 350 ~; 328 |; 34 &)
% ( 11 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 32 ( 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_7,axiom,
! [X] :
( cC110(X)
<=> ( ~ cC108(X)
& ~ cC102(X) ) ),
file('theBenchmark.p',axiom_7) ).
fof(axiom_9,axiom,
! [X] :
( cC114(X)
<=> ( ~ cC112(X)
& ~ cC96(X) ) ),
file('theBenchmark.p',axiom_9) ).
fof(axiom_10,axiom,
! [X] :
( cC116(X)
<=> ( cC80(X)
& cC114(X) ) ),
file('theBenchmark.p',axiom_10) ).
fof(axiom_21,axiom,
! [X] :
( cC136(X)
<=> ( ~ cC134(X)
& cC116(X) ) ),
file('theBenchmark.p',axiom_21) ).
fof(axiom_43,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC10(X)
& cC4(X) ) ),
file('theBenchmark.p',axiom_43) ).
fof(axiom_44,axiom,
! [X] :
( cC58(X)
<=> ( cC56(X)
& cC34(X) ) ),
file('theBenchmark.p',axiom_44) ).
fof(axiom_57,axiom,
! [X] :
( cC80(X)
<=> ( ~ cC76(X)
& ~ cC78(X) ) ),
file('theBenchmark.p',axiom_57) ).
fof(axiom_65,axiom,
! [X] :
( cC96(X)
<=> ( cC2(X)
& ~ cC94(X) ) ),
file('theBenchmark.p',axiom_65) ).
fof(the_axiom,conjecture,
( cC80(iV822576)
& cC136(iV822576)
& cC114(iV822576)
& cC110(iV822576)
& cC56(iV822576)
& cC116(iV822576)
& cC58(iV822576)
& cowlThing(iV822576)
& cC94(iV822576)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(the_axiom_neg,negated_conjecture,
~ ( cC80(iV822576)
& cC136(iV822576)
& cC114(iV822576)
& cC110(iV822576)
& cC56(iV822576)
& cC116(iV822576)
& cC58(iV822576)
& cowlThing(iV822576)
& cC94(iV822576)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
fof(nnf_72,plain,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(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,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(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_72]) ).
fof(sk_the_axiom_neg,plain,
( ( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ) ),
inference(cnf_transformation,[status(thm)],[sk_the_axiom_neg_sk]) ).
cnf(c_73,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_74,plain,
~ cowlNothing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_75,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_76,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| ~ cowlThing(sK0) ),
inference(resolve,[status(thm)],[c_73,c_74]) ).
cnf(c_77,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| ~ cowlThing(sK0) ),
inference(resolve,[status(thm)],[c_75,c_74]) ).
cnf(c_78,plain,
( xsd_integer(A)
| xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_79,plain,
( ~ xsd_integer(A)
| ~ xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
fof(axiom_70,axiom,
~ cC102(iV822576),
file('theBenchmark.p',axiom_70) ).
cnf(c_90,plain,
~ cC102(iV822576),
inference(clausify,[status(thm)],[axiom_70]) ).
cnf(c_91,plain,
( cC108(A)
| cC102(A)
| cC110(A) ),
inference(clausify,[status(thm)],[axiom_7]) ).
cnf(c_114,plain,
( ~ cC56(A)
| ~ cC34(A)
| cC58(A) ),
inference(clausify,[status(thm)],[axiom_44]) ).
fof(axiom_74,axiom,
cC34(iV822576),
file('theBenchmark.p',axiom_74) ).
cnf(c_119,plain,
cC34(iV822576),
inference(clausify,[status(thm)],[axiom_74]) ).
cnf(c_179,plain,
( cC108(iV822576)
| cC110(iV822576) ),
inference(resolve,[status(thm)],[c_91,c_90]) ).
fof(axiom_79,axiom,
~ cC108(iV822576),
file('theBenchmark.p',axiom_79) ).
cnf(c_182,plain,
~ cC108(iV822576),
inference(clausify,[status(thm)],[axiom_79]) ).
cnf(c_211,plain,
( cC112(A)
| cC96(A)
| cC114(A) ),
inference(clausify,[status(thm)],[axiom_9]) ).
fof(axiom_87,axiom,
~ cC112(iV822576),
file('theBenchmark.p',axiom_87) ).
cnf(c_212,plain,
~ cC112(iV822576),
inference(clausify,[status(thm)],[axiom_87]) ).
cnf(c_220,plain,
( cC96(iV822576)
| cC114(iV822576) ),
inference(resolve,[status(thm)],[c_211,c_212]) ).
cnf(c_221,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_integer(sK1)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_79,c_76]) ).
cnf(c_222,negated_conjecture,
( ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC114(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| xsd_integer(sK1)
| ~ cowlThing(sK0)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_78,c_77]) ).
cnf(c_223,plain,
( ~ cC96(A)
| ~ cC114(A) ),
inference(clausify,[status(thm)],[axiom_9]) ).
cnf(c_224,plain,
( cC114(A)
| ~ cC116(A) ),
inference(clausify,[status(thm)],[axiom_10]) ).
cnf(c_225,plain,
( ~ cC80(A)
| ~ cC114(A)
| cC116(A) ),
inference(clausify,[status(thm)],[axiom_10]) ).
cnf(c_226,plain,
( ~ cC96(A)
| ~ cC116(A) ),
inference(resolve,[status(thm)],[c_224,c_223]) ).
cnf(c_227,plain,
( cC96(iV822576)
| ~ cC80(iV822576)
| cC116(iV822576) ),
inference(resolve,[status(thm)],[c_225,c_220]) ).
cnf(c_230,negated_conjecture,
( cC96(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| xsd_integer(sK1)
| ~ cowlThing(sK0)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_222,c_220]) ).
cnf(c_231,negated_conjecture,
( cC96(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_integer(sK1)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_221,c_220]) ).
fof(axiom_76,axiom,
~ cC96(iV822576),
file('theBenchmark.p',axiom_76) ).
cnf(c_232,plain,
~ cC96(iV822576),
inference(clausify,[status(thm)],[axiom_76]) ).
cnf(c_233,plain,
( ~ cC2(A)
| cC94(A)
| cC96(A) ),
inference(clausify,[status(thm)],[axiom_65]) ).
cnf(c_236,plain,
( cC80(A)
| ~ cC116(A) ),
inference(clausify,[status(thm)],[axiom_10]) ).
cnf(c_237,negated_conjecture,
( ~ cC116(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| xsd_integer(sK1)
| ~ cowlThing(sK0)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_230,c_226]) ).
cnf(c_238,negated_conjecture,
( ~ cC116(iV822576)
| ~ cC80(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_integer(sK1)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_231,c_226]) ).
cnf(c_239,plain,
( ~ cC80(iV822576)
| cC116(iV822576) ),
inference(resolve,[status(thm)],[c_232,c_227]) ).
cnf(c_246,plain,
( cC76(A)
| cC78(A)
| cC80(A) ),
inference(clausify,[status(thm)],[axiom_57]) ).
cnf(c_316,plain,
( cC10(A)
| ~ cC4(A)
| cC56(A) ),
inference(clausify,[status(thm)],[axiom_43]) ).
fof(axiom_84,axiom,
~ cC10(iV822576),
file('theBenchmark.p',axiom_84) ).
cnf(c_321,plain,
~ cC10(iV822576),
inference(clausify,[status(thm)],[axiom_84]) ).
cnf(c_670,plain,
cC110(iV822576),
inference(resolve,[status(thm)],[c_182,c_179]) ).
cnf(c_799,negated_conjecture,
( ~ cC116(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| xsd_integer(sK1)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC116(iV822576) ),
inference(resolve,[status(thm)],[c_236,c_237]) ).
cnf(c_2547,negated_conjecture,
( ~ cC116(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC116(iV822576) ),
inference(copy,[status(thm)],[c_799]) ).
cnf(c_2548,negated_conjecture,
( ~ cC116(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC116(iV822576) ),
inference(copy,[status(thm)],[c_2547]) ).
cnf(c_2549,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC116(iV822576) ),
inference(copy,[status(thm)],[c_2548]) ).
cnf(c_800,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC116(iV822576) ),
inference(resolve,[status(thm)],[c_670,c_2549]) ).
cnf(c_801,negated_conjecture,
( ~ cC116(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_integer(sK1)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC116(iV822576) ),
inference(resolve,[status(thm)],[c_236,c_238]) ).
cnf(c_2550,negated_conjecture,
( ~ cC116(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC116(iV822576) ),
inference(copy,[status(thm)],[c_801]) ).
cnf(c_2551,negated_conjecture,
( ~ cC116(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC116(iV822576) ),
inference(copy,[status(thm)],[c_2550]) ).
cnf(c_2552,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC116(iV822576) ),
inference(copy,[status(thm)],[c_2551]) ).
cnf(c_802,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC116(iV822576) ),
inference(resolve,[status(thm)],[c_670,c_2552]) ).
cnf(c_805,plain,
( cC116(iV822576)
| cC76(iV822576)
| cC78(iV822576) ),
inference(resolve,[status(thm)],[c_246,c_239]) ).
cnf(c_820,plain,
( ~ cC4(iV822576)
| cC56(iV822576) ),
inference(resolve,[status(thm)],[c_321,c_316]) ).
cnf(c_2003,plain,
( ~ cC56(iV822576)
| cC58(iV822576) ),
inference(resolve,[status(thm)],[c_119,c_114]) ).
fof(axiom_89,axiom,
cC2(iV822576),
file('theBenchmark.p',axiom_89) ).
cnf(c_2058,plain,
cC2(iV822576),
inference(clausify,[status(thm)],[axiom_89]) ).
fof(axiom_88,axiom,
~ cC78(iV822576),
file('theBenchmark.p',axiom_88) ).
cnf(c_2059,plain,
~ cC78(iV822576),
inference(clausify,[status(thm)],[axiom_88]) ).
fof(axiom_86,axiom,
~ cC76(iV822576),
file('theBenchmark.p',axiom_86) ).
cnf(c_2060,plain,
~ cC76(iV822576),
inference(clausify,[status(thm)],[axiom_86]) ).
fof(axiom_75,axiom,
cC4(iV822576),
file('theBenchmark.p',axiom_75) ).
cnf(c_2066,plain,
cC4(iV822576),
inference(clausify,[status(thm)],[axiom_75]) ).
fof(axiom_71,axiom,
~ cC134(iV822576),
file('theBenchmark.p',axiom_71) ).
cnf(c_2069,plain,
~ cC134(iV822576),
inference(clausify,[status(thm)],[axiom_71]) ).
cnf(c_2182,plain,
( cC134(A)
| ~ cC116(A)
| cC136(A) ),
inference(clausify,[status(thm)],[axiom_21]) ).
cnf(c_2193,plain,
cowlThing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_2241,plain,
( ~ cC2(iV822576)
| cC94(iV822576) ),
inference(resolve,[status(thm)],[c_233,c_232]) ).
cnf(c_2242,plain,
cC94(iV822576),
inference(resolve,[status(thm)],[c_2058,c_2241]) ).
cnf(c_2553,plain,
( cC116(iV822576)
| cC76(iV822576) ),
inference(resolve,[status(thm)],[c_2059,c_805]) ).
cnf(c_2460,plain,
cC116(iV822576),
inference(resolve,[status(thm)],[c_2060,c_2553]) ).
cnf(c_2554,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2460,c_802]) ).
cnf(c_2555,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2193,c_2554]) ).
cnf(c_2556,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2242,c_2555]) ).
cnf(c_2461,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2193,c_2556]) ).
cnf(c_2557,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(sK0)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2460,c_800]) ).
cnf(c_2558,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2193,c_2557]) ).
cnf(c_2559,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2242,c_2558]) ).
cnf(c_2462,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2193,c_2559]) ).
cnf(c_2465,plain,
cC56(iV822576),
inference(resolve,[status(thm)],[c_2066,c_820]) ).
cnf(c_2471,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC58(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2465,c_2462]) ).
cnf(c_2472,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC58(iV822576)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2465,c_2461]) ).
cnf(c_2473,plain,
cC58(iV822576),
inference(resolve,[status(thm)],[c_2465,c_2003]) ).
cnf(c_2474,negated_conjecture,
( ~ cC136(iV822576)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2473,c_2472]) ).
cnf(c_2475,negated_conjecture,
( ~ cC136(iV822576)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_2473,c_2471]) ).
cnf(c_2560,plain,
( cC134(iV822576)
| cC136(iV822576) ),
inference(resolve,[status(thm)],[c_2460,c_2182]) ).
cnf(c_2544,plain,
cC136(iV822576),
inference(resolve,[status(thm)],[c_2069,c_2560]) ).
cnf(c_2545,negated_conjecture,
xsd_integer(sK1),
inference(resolve,[status(thm)],[c_2544,c_2475]) ).
cnf(c_2561,negated_conjecture,
~ cC136(iV822576),
inference(resolve,[status(thm)],[c_2545,c_2474]) ).
cnf(c_2546,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_2544,c_2561]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS146+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.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 19:44:06 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 3975716 was started by sandbox on n002,
% 0.09/0.36 % Fri Sep 25 19:44:06 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 17.62/2.69
% 17.62/2.69 % SZS status Theorem for theBenchmark
% 17.62/2.69
% 17.62/2.69 % Proof 1 at 2.26 (+ 0.03) seconds.
% 17.62/2.69 % Length of proof is 74.
% 17.62/2.69 % Level of proof is 12.
% 17.62/2.69 % Maximum clause weight is 21.000.
% 17.62/2.69 % Given clauses 346.
% 17.62/2.69
% 17.62/2.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------