%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS147+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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 33.26s 10.30s
% Output : CNFRefutation 33.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 30
% Syntax : Number of formulae : 136 ( 46 unt; 0 def)
% Number of atoms : 764 ( 0 equ)
% Maximal formula atoms : 38 ( 5 avg)
% Number of connectives : 1210 ( 582 ~; 563 |; 50 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 23 ( 22 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 54 ( 2 sgn 18 !; 11 ?)
% 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_2,axiom,
! [X] :
( cC10(X)
<=> ( cC8(X)
& cC4(X) ) ),
file('theBenchmark.p',axiom_2) ).
fof(axiom_4,axiom,
! [X] :
( cC14(X)
<=> ? [Y] :
( cTOP(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_4) ).
fof(axiom_7,axiom,
! [X] :
( cC20(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_7) ).
fof(axiom_14,axiom,
! [X] :
( cC34(X)
<=> ? [Y] :
( ~ cC32(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_14) ).
fof(axiom_17,axiom,
! [X] :
( cC4(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_17) ).
fof(axiom_22,axiom,
! [X] :
( cC48(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_22) ).
fof(axiom_27,axiom,
! [X] :
( cC58(X)
<=> ? [Y] :
( cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_27) ).
fof(axiom_29,axiom,
! [X] :
( cC60(X)
<=> ( ~ cC2(X)
& cC58(X) ) ),
file('theBenchmark.p',axiom_29) ).
fof(axiom_30,axiom,
! [X] :
( cC62(X)
<=> ? [Y] :
( cC60(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_30) ).
fof(axiom_39,axiom,
! [X] :
( cC8(X)
<=> ? [Y] :
( ~ cC6(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_39) ).
fof(axiom_40,axiom,
! [X] :
( cC80(X)
<=> ( ~ cC78(X)
& ~ cC2(X) ) ),
file('theBenchmark.p',axiom_40) ).
fof(axiom_41,axiom,
! [X] :
( cC82(X)
<=> ? [Y] :
( cC80(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_41) ).
fof(the_axiom,conjecture,
( cC58(iV8472)
& cowlThing(iV8472)
& cC60(iV8472)
& cC80(iV8471)
& cowlThing(iV8471)
& cC34(iV8467)
& cC62(iV8467)
& cowlThing(iV8467)
& cC20(iV8467)
& cC8(iV8467)
& cC14(iV8467)
& cC82(iV8467)
& cC4(iV8467)
& cC48(iV8467)
& cC10(iV8467)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(the_axiom_neg,negated_conjecture,
~ ( cC58(iV8472)
& cowlThing(iV8472)
& cC60(iV8472)
& cC80(iV8471)
& cowlThing(iV8471)
& cC34(iV8467)
& cC62(iV8467)
& cowlThing(iV8467)
& cC20(iV8467)
& cC8(iV8467)
& cC14(iV8467)
& cC82(iV8467)
& cC4(iV8467)
& cC48(iV8467)
& cC10(iV8467)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
fof(nnf_53,plain,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ? [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,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ( ( 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_53]) ).
fof(sk_the_axiom_neg,plain,
( ( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ) ),
inference(cnf_transformation,[status(thm)],[sk_the_axiom_neg_sk]) ).
cnf(c_54,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_55,plain,
~ cowlNothing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_56,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_57,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| ~ cowlThing(sK0) ),
inference(resolve,[status(thm)],[c_54,c_55]) ).
cnf(c_58,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| ~ cowlThing(sK0) ),
inference(resolve,[status(thm)],[c_56,c_55]) ).
cnf(c_59,plain,
( xsd_integer(A)
| xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_60,plain,
( ~ xsd_integer(A)
| ~ xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_61,plain,
( ~ cC8(A)
| ~ cC4(A)
| cC10(A) ),
inference(clausify,[status(thm)],[axiom_2]) ).
cnf(c_64,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| xsd_integer(sK1)
| ~ cowlThing(sK0)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_59,c_58]) ).
cnf(c_65,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ xsd_integer(sK1)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_60,c_57]) ).
fof(axiom_76,axiom,
rR1(iV8472,iV8476),
file('theBenchmark.p',axiom_76) ).
cnf(c_68,plain,
rR1(iV8472,iV8476),
inference(clausify,[status(thm)],[axiom_76]) ).
fof(axiom_62,axiom,
rR1(iV8467,iV8470),
file('theBenchmark.p',axiom_62) ).
cnf(c_74,plain,
rR1(iV8467,iV8470),
inference(clausify,[status(thm)],[axiom_62]) ).
fof(axiom_61,axiom,
rR1(iV8467,iV8474),
file('theBenchmark.p',axiom_61) ).
cnf(c_75,plain,
rR1(iV8467,iV8474),
inference(clausify,[status(thm)],[axiom_61]) ).
fof(axiom_60,axiom,
rR1(iV8467,iV8472),
file('theBenchmark.p',axiom_60) ).
cnf(c_76,plain,
rR1(iV8467,iV8472),
inference(clausify,[status(thm)],[axiom_60]) ).
fof(axiom_58,axiom,
rR1(iV8467,iV8469),
file('theBenchmark.p',axiom_58) ).
cnf(c_78,plain,
rR1(iV8467,iV8469),
inference(clausify,[status(thm)],[axiom_58]) ).
fof(axiom_57,axiom,
rR1(iV8467,iV8468),
file('theBenchmark.p',axiom_57) ).
cnf(c_79,plain,
rR1(iV8467,iV8468),
inference(clausify,[status(thm)],[axiom_57]) ).
fof(axiom_55,axiom,
rR1(iV8467,iV8471),
file('theBenchmark.p',axiom_55) ).
cnf(c_81,plain,
rR1(iV8467,iV8471),
inference(clausify,[status(thm)],[axiom_55]) ).
cnf(c_90,plain,
( ~ cC80(B)
| ~ rR1(A,B)
| cC82(A) ),
inference(clausify,[status(thm)],[axiom_41]) ).
cnf(c_92,plain,
( cC6(B)
| ~ rR1(A,B)
| cC8(A) ),
inference(clausify,[status(thm)],[axiom_39]) ).
cnf(c_104,plain,
( ~ cC60(B)
| ~ rR1(A,B)
| cC62(A) ),
inference(clausify,[status(thm)],[axiom_30]) ).
cnf(c_108,plain,
( ~ cC2(B)
| ~ rR1(A,B)
| cC58(A) ),
inference(clausify,[status(thm)],[axiom_27]) ).
cnf(c_114,plain,
( cC2(B)
| ~ rR1(A,B)
| cC48(A) ),
inference(clausify,[status(thm)],[axiom_22]) ).
cnf(c_120,plain,
( cC2(B)
| ~ rR1(A,B)
| cC4(A) ),
inference(clausify,[status(thm)],[axiom_17]) ).
cnf(c_126,plain,
( cC32(B)
| ~ rR1(A,B)
| cC34(A) ),
inference(clausify,[status(thm)],[axiom_14]) ).
cnf(c_136,plain,
( cC2(B)
| ~ rR1(A,B)
| cC20(A) ),
inference(clausify,[status(thm)],[axiom_7]) ).
cnf(c_140,plain,
( ~ cTOP(B)
| ~ rR1(A,B)
| cC14(A) ),
inference(clausify,[status(thm)],[axiom_4]) ).
fof(axiom_68,axiom,
cTOP(iV8470),
file('theBenchmark.p',axiom_68) ).
cnf(c_219,plain,
cTOP(iV8470),
inference(clausify,[status(thm)],[axiom_68]) ).
cnf(c_296,plain,
( ~ cTOP(iV8470)
| cC14(iV8467) ),
inference(resolve,[status(thm)],[c_140,c_74]) ).
cnf(c_461,plain,
cC14(iV8467),
inference(resolve,[status(thm)],[c_296,c_219]) ).
cnf(c_501,plain,
( cC2(iV8468)
| cC20(iV8467) ),
inference(resolve,[status(thm)],[c_136,c_79]) ).
cnf(c_802,plain,
( cC32(iV8474)
| cC34(iV8467) ),
inference(resolve,[status(thm)],[c_126,c_75]) ).
cnf(c_965,plain,
( cC2(iV8468)
| cC4(iV8467) ),
inference(resolve,[status(thm)],[c_120,c_79]) ).
cnf(c_1106,plain,
( cC2(iV8468)
| cC48(iV8467) ),
inference(resolve,[status(thm)],[c_114,c_79]) ).
cnf(c_1223,plain,
( ~ cC2(iV8476)
| cC58(iV8472) ),
inference(resolve,[status(thm)],[c_108,c_68]) ).
cnf(c_1298,plain,
( ~ cC60(iV8472)
| cC62(iV8467) ),
inference(resolve,[status(thm)],[c_104,c_76]) ).
cnf(c_1468,plain,
( cC6(iV8469)
| cC8(iV8467) ),
inference(resolve,[status(thm)],[c_92,c_78]) ).
cnf(c_1492,plain,
( ~ cC80(iV8471)
| cC82(iV8467) ),
inference(resolve,[status(thm)],[c_90,c_81]) ).
cnf(c_1557,plain,
cowlThing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_1596,plain,
( cC2(A)
| ~ cC58(A)
| cC60(A) ),
inference(clausify,[status(thm)],[axiom_29]) ).
cnf(c_1615,plain,
( cC78(A)
| cC2(A)
| cC80(A) ),
inference(clausify,[status(thm)],[axiom_40]) ).
fof(axiom_63,axiom,
~ cC2(iV8468),
file('theBenchmark.p',axiom_63) ).
cnf(c_1635,plain,
~ cC2(iV8468),
inference(clausify,[status(thm)],[axiom_63]) ).
fof(axiom_65,axiom,
~ cC6(iV8469),
file('theBenchmark.p',axiom_65) ).
cnf(c_1636,plain,
~ cC6(iV8469),
inference(clausify,[status(thm)],[axiom_65]) ).
fof(axiom_70,axiom,
~ cC2(iV8471),
file('theBenchmark.p',axiom_70) ).
cnf(c_1637,plain,
~ cC2(iV8471),
inference(clausify,[status(thm)],[axiom_70]) ).
fof(axiom_71,axiom,
~ cC78(iV8471),
file('theBenchmark.p',axiom_71) ).
cnf(c_1638,plain,
~ cC78(iV8471),
inference(clausify,[status(thm)],[axiom_71]) ).
fof(axiom_74,axiom,
~ cC2(iV8472),
file('theBenchmark.p',axiom_74) ).
cnf(c_1639,plain,
~ cC2(iV8472),
inference(clausify,[status(thm)],[axiom_74]) ).
fof(axiom_80,axiom,
~ cC32(iV8474),
file('theBenchmark.p',axiom_80) ).
cnf(c_1641,plain,
~ cC32(iV8474),
inference(clausify,[status(thm)],[axiom_80]) ).
fof(axiom_84,axiom,
cC2(iV8476),
file('theBenchmark.p',axiom_84) ).
cnf(c_1643,plain,
cC2(iV8476),
inference(clausify,[status(thm)],[axiom_84]) ).
cnf(c_1644,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| xsd_integer(sK1)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_61,c_64]) ).
cnf(c_6137,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(copy,[status(thm)],[c_1644]) ).
cnf(c_6138,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(copy,[status(thm)],[c_6137]) ).
cnf(c_6139,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(sK0)
| xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(copy,[status(thm)],[c_6138]) ).
cnf(c_6140,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_1557,c_6139]) ).
cnf(c_6141,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_461,c_6140]) ).
cnf(c_6142,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_1557,c_6141]) ).
cnf(c_6143,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_1557,c_6142]) ).
cnf(c_1645,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_1557,c_6143]) ).
cnf(c_1646,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ xsd_integer(sK1)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_61,c_65]) ).
cnf(c_6144,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC4(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(copy,[status(thm)],[c_1646]) ).
cnf(c_6145,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC8(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(copy,[status(thm)],[c_6144]) ).
cnf(c_6146,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(sK0)
| ~ xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(copy,[status(thm)],[c_6145]) ).
cnf(c_6147,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| ~ xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_1557,c_6146]) ).
cnf(c_6148,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cowlThing(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| ~ xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_461,c_6147]) ).
cnf(c_6149,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| ~ xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_1557,c_6148]) ).
cnf(c_6150,negated_conjecture,
( ~ cC58(iV8472)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| ~ xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_1557,c_6149]) ).
cnf(c_1647,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| ~ xsd_integer(sK1)
| ~ cC8(iV8467)
| ~ cC4(iV8467) ),
inference(resolve,[status(thm)],[c_1557,c_6150]) ).
cnf(c_4020,plain,
cC48(iV8467),
inference(resolve,[status(thm)],[c_1635,c_1106]) ).
cnf(c_4021,plain,
cC4(iV8467),
inference(resolve,[status(thm)],[c_1635,c_965]) ).
cnf(c_4023,plain,
cC20(iV8467),
inference(resolve,[status(thm)],[c_1635,c_501]) ).
cnf(c_4024,plain,
cC8(iV8467),
inference(resolve,[status(thm)],[c_1636,c_1468]) ).
cnf(c_4025,plain,
cC34(iV8467),
inference(resolve,[status(thm)],[c_1641,c_802]) ).
cnf(c_4027,plain,
cC58(iV8472),
inference(resolve,[status(thm)],[c_1643,c_1223]) ).
cnf(c_6151,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| ~ xsd_integer(sK1)
| ~ cC8(iV8467) ),
inference(resolve,[status(thm)],[c_4021,c_1647]) ).
cnf(c_6152,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4024,c_6151]) ).
cnf(c_6153,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4020,c_6152]) ).
cnf(c_6154,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4023,c_6153]) ).
cnf(c_6155,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4025,c_6154]) ).
cnf(c_4031,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4027,c_6155]) ).
cnf(c_6156,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| xsd_integer(sK1)
| ~ cC8(iV8467) ),
inference(resolve,[status(thm)],[c_4021,c_1645]) ).
cnf(c_6157,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| ~ cC48(iV8467)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4024,c_6156]) ).
cnf(c_6158,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC82(iV8467)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4020,c_6157]) ).
cnf(c_6159,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4023,c_6158]) ).
cnf(c_6160,negated_conjecture,
( ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4025,c_6159]) ).
cnf(c_4032,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4027,c_6160]) ).
cnf(c_6161,plain,
( cC82(iV8467)
| cC78(iV8471)
| cC2(iV8471) ),
inference(resolve,[status(thm)],[c_1615,c_1492]) ).
cnf(c_6162,plain,
( cC82(iV8467)
| cC78(iV8471) ),
inference(resolve,[status(thm)],[c_1637,c_6161]) ).
cnf(c_4196,plain,
cC82(iV8467),
inference(resolve,[status(thm)],[c_1638,c_6162]) ).
cnf(c_4217,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC62(iV8467)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4196,c_4032]) ).
cnf(c_4218,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC80(iV8471)
| ~ cC62(iV8467)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_4196,c_4031]) ).
cnf(c_6163,plain,
( cC2(iV8472)
| cC60(iV8472) ),
inference(resolve,[status(thm)],[c_4027,c_1596]) ).
cnf(c_5485,plain,
cC60(iV8472),
inference(resolve,[status(thm)],[c_1639,c_6163]) ).
cnf(c_5495,negated_conjecture,
( ~ cC80(iV8471)
| ~ cC62(iV8467)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_5485,c_4218]) ).
cnf(c_5496,negated_conjecture,
( ~ cC80(iV8471)
| ~ cC62(iV8467)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_5485,c_4217]) ).
cnf(c_5497,plain,
cC62(iV8467),
inference(resolve,[status(thm)],[c_5485,c_1298]) ).
cnf(c_5498,negated_conjecture,
( ~ cC80(iV8471)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_5497,c_5496]) ).
cnf(c_5499,negated_conjecture,
( ~ cC80(iV8471)
| ~ xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_5497,c_5495]) ).
cnf(c_6164,negated_conjecture,
( cC78(iV8471)
| cC2(iV8471)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_5498,c_1615]) ).
cnf(c_6165,negated_conjecture,
( cC78(iV8471)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_1637,c_6164]) ).
cnf(c_6020,negated_conjecture,
xsd_integer(sK1),
inference(resolve,[status(thm)],[c_1638,c_6165]) ).
cnf(c_6021,negated_conjecture,
~ cC80(iV8471),
inference(resolve,[status(thm)],[c_6020,c_5499]) ).
cnf(c_6166,negated_conjecture,
( cC78(iV8471)
| cC2(iV8471) ),
inference(resolve,[status(thm)],[c_6021,c_1615]) ).
cnf(c_6167,negated_conjecture,
cC78(iV8471),
inference(resolve,[status(thm)],[c_1637,c_6166]) ).
cnf(c_6136,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1638,c_6167]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : KRS147+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/5.46 % Computer : n010.cluster.edu
% 0.20/5.46 % Model : x86_64 x86_64
% 0.20/5.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/5.46 % Memory : 8046.5625MB
% 0.20/5.46 % OS : Linux 6.8.0-71-generic
% 0.20/5.46 % CPULimit : 300
% 0.20/5.46 % WCLimit : 300
% 0.20/5.46 % DateTime : Fri Sep 25 19:41:37 UTC 2026
% 0.20/5.47 % CPUTime :
% 0.20/5.47 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.20/5.47 % Process 1489729 was started by sandbox2 on n010,
% 0.20/5.47 % Fri Sep 25 19:41:37 2026
% 0.20/5.47 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.20/5.50
% 0.20/5.50 % From the command line: assign(max_seconds, 300).
% 33.26/10.30
% 33.26/10.30 % given #500 (I,wt=17): 951 -cC4(A) | cC62(A) | -cC60(f12(A)). [resolve(121,b,104,b)].
% 33.26/10.30
% 33.26/10.30 % given #1000 (I,wt=9): 1563 -cC26(A) | -cC20(A) # tptp_name(axiom_10). [clausify(11)].
% 33.26/10.30
% 33.26/10.30 % given #1500 (I,wt=23): 2067 -cC48(A) | -cC4(f15(A)) | -cC8(f15(A)) | cC62(A) | -cC60(f1(A)). [resolve(189,b,162,a)].
% 33.26/10.30
% 33.26/10.30 % given #2000 (I,wt=23): 2567 -cC94(A) | -cC4(f31(A)) | -cC8(f31(A)) | cC78(A) | cC2(f1(A)). [resolve(205,b,167,a)].
% 33.26/10.30
% 33.26/10.30 % given #2500 (I,wt=17): 3220 cC14(iV8473) | cC36(iV8467) | -cC2(f3(iV8467)). [resolve(337,a,323,a)].
% 33.26/10.30
% 33.26/10.30 % given #3000 (I,wt=20): 3737 cC14(f16(A)) | -cC50(A) | cC74(A) | -cC72(f3(A)). [resolve(354,a,309,a)].
% 33.26/10.30
% 33.26/10.30 % SZS status Theorem for theBenchmark
% 33.26/10.30
% 33.26/10.30 % Proof 1 at 4.44 (+ 0.26) seconds.
% 33.26/10.30 % Length of proof is 86.
% 33.26/10.30 % Level of proof is 12.
% 33.26/10.30 % Maximum clause weight is 27.000.
% 33.26/10.30 % Given clauses 3323.
% 33.26/10.30
% 33.26/10.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------