%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS155+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 : n005.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 1.90s 0.76s
% Output : CNFRefutation 1.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 29
% Syntax : Number of formulae : 151 ( 51 unt; 0 def)
% Number of atoms : 730 ( 0 equ)
% Maximal formula atoms : 38 ( 4 avg)
% Number of connectives : 1073 ( 494 ~; 494 |; 69 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-1 aty)
% Number of variables : 91 ( 2 sgn 43 !; 15 ?)
% 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_5,axiom,
! [X] :
( cC14(X)
<=> ? [Y] :
( cTOP(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_5) ).
fof(axiom_13,axiom,
! [X] :
( cC20(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_13) ).
fof(axiom_16,axiom,
! [X] :
( cC22(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_16) ).
fof(axiom_29,axiom,
! [X] :
( cC34(X)
<=> ? [Y] :
( cC32xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_29) ).
fof(axiom_35,axiom,
! [X] :
( cC4(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_35) ).
fof(axiom_44,axiom,
! [X] :
( cC48(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_44) ).
fof(axiom_57,axiom,
! [X] :
( cC58(X)
<=> ? [Y] :
( cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_57) ).
fof(axiom_61,axiom,
! [X] :
( cC60(X)
<=> ( cC58(X)
& cC2xcomp(X) ) ),
file('theBenchmark.p',axiom_61) ).
fof(axiom_62,axiom,
! [X] :
( cC62(X)
<=> ? [Y] :
( cC60(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_62) ).
fof(axiom_79,axiom,
! [X] :
( cC8(X)
<=> ? [Y] :
( cC6xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_79) ).
fof(axiom_80,axiom,
! [X] :
( cC80(X)
<=> ( cC2xcomp(X)
& cC78xcomp(X) ) ),
file('theBenchmark.p',axiom_80) ).
fof(axiom_82,axiom,
! [X] :
( cC82(X)
<=> ? [Y] :
( cC80(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_82) ).
fof(the_axiom,conjecture,
( cowlThing(iV8472)
& cC60(iV8472)
& cC58(iV8472)
& cC80(iV8471)
& cowlThing(iV8471)
& cC48(iV8467)
& cowlThing(iV8467)
& cC10(iV8467)
& cC34(iV8467)
& cC14(iV8467)
& cC62(iV8467)
& cC82(iV8467)
& cC8(iV8467)
& cC4(iV8467)
& cC20(iV8467)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(the_axiom_neg,negated_conjecture,
~ ( cowlThing(iV8472)
& cC60(iV8472)
& cC58(iV8472)
& cC80(iV8471)
& cowlThing(iV8471)
& cC48(iV8467)
& cowlThing(iV8467)
& cC10(iV8467)
& cC34(iV8467)
& cC14(iV8467)
& cC62(iV8467)
& cC82(iV8467)
& cC8(iV8467)
& cC4(iV8467)
& cC20(iV8467)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
cnf(c_115,plain,
cowlThing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_116,plain,
~ cowlNothing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_117,plain,
( ~ xsd_integer(A)
| ~ xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_118,plain,
( xsd_integer(A)
| xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_121,plain,
( ~ cC8(A)
| ~ cC4(A)
| cC10(A) ),
inference(clausify,[status(thm)],[axiom_2]) ).
cnf(c_129,plain,
( ~ cTOP(B)
| ~ rR1(A,B)
| cC14(A) ),
inference(clausify,[status(thm)],[axiom_5]) ).
fof(nnf_12,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC20(X) )
& ( ? [X0] :
( cC2xcomp(X0)
& rR1(X,X0) )
| ~ cC20(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_13]) ).
fof(sk_axiom_13_sk,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC20(X) )
& ( ( cC2xcomp(sK0(X))
& rR1(X,sK0(X)) )
| ~ cC20(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0(X))],[nnf_12]) ).
fof(sk_axiom_13,plain,
( ! [VAR_0,VAR_1] :
( ~ cC2xcomp(VAR_1)
| ~ rR1(VAR_0,VAR_1)
| cC20(VAR_0) )
& ! [VAR_0] :
( cC2xcomp(sK0(VAR_0))
| ~ cC20(VAR_0) )
& ! [VAR_0] :
( rR1(VAR_0,sK0(VAR_0))
| ~ cC20(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_13_sk]) ).
cnf(c_142,plain,
( rR1(A,sK0(A))
| ~ cC20(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_13]) ).
cnf(c_143,plain,
( cC2xcomp(sK0(A))
| ~ cC20(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_13]) ).
cnf(c_144,plain,
( ~ cC2xcomp(B)
| ~ rR1(A,B)
| cC20(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_13]) ).
fof(nnf_15,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC22(X) )
& ( ? [X0] :
( cC2xcomp(X0)
& rR1(X,X0) )
| ~ cC22(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_16]) ).
fof(sk_axiom_16_sk,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC22(X) )
& ( ( cC2xcomp(sK1(X))
& rR1(X,sK1(X)) )
| ~ cC22(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X0,sK1(X))],[nnf_15]) ).
fof(sk_axiom_16,plain,
( ! [VAR_0,VAR_1] :
( ~ cC2xcomp(VAR_1)
| ~ rR1(VAR_0,VAR_1)
| cC22(VAR_0) )
& ! [VAR_0] :
( cC2xcomp(sK1(VAR_0))
| ~ cC22(VAR_0) )
& ! [VAR_0] :
( rR1(VAR_0,sK1(VAR_0))
| ~ cC22(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_16_sk]) ).
cnf(c_149,plain,
( rR1(A,sK1(A))
| ~ cC22(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_16]) ).
cnf(c_150,plain,
( cC2xcomp(sK1(A))
| ~ cC22(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_16]) ).
cnf(c_151,plain,
( ~ cC2xcomp(B)
| ~ rR1(A,B)
| cC22(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_16]) ).
cnf(c_183,plain,
( ~ cC32xcomp(B)
| ~ rR1(A,B)
| cC34(A) ),
inference(clausify,[status(thm)],[axiom_29]) ).
fof(nnf_34,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC4(X) )
& ( ? [X0] :
( cC2xcomp(X0)
& rR1(X,X0) )
| ~ cC4(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_35]) ).
fof(sk_axiom_35_sk,plain,
! [X] :
( ( ! [Y] :
( ~ cC2xcomp(Y)
| ~ rR1(X,Y) )
| cC4(X) )
& ( ( cC2xcomp(sK2(X))
& rR1(X,sK2(X)) )
| ~ cC4(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2(X))],[nnf_34]) ).
fof(sk_axiom_35,plain,
( ! [VAR_0,VAR_1] :
( ~ cC2xcomp(VAR_1)
| ~ rR1(VAR_0,VAR_1)
| cC4(VAR_0) )
& ! [VAR_0] :
( cC2xcomp(sK2(VAR_0))
| ~ cC4(VAR_0) )
& ! [VAR_0] :
( rR1(VAR_0,sK2(VAR_0))
| ~ cC4(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_35_sk]) ).
cnf(c_196,plain,
( rR1(A,sK2(A))
| ~ cC4(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_35]) ).
cnf(c_197,plain,
( cC2xcomp(sK2(A))
| ~ cC4(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_35]) ).
cnf(c_198,plain,
( ~ cC2xcomp(B)
| ~ rR1(A,B)
| cC4(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_35]) ).
cnf(c_221,plain,
( ~ cC2xcomp(B)
| ~ rR1(A,B)
| cC48(A) ),
inference(clausify,[status(thm)],[axiom_44]) ).
cnf(c_252,plain,
( ~ cC2(B)
| ~ rR1(A,B)
| cC58(A) ),
inference(clausify,[status(thm)],[axiom_57]) ).
cnf(c_262,plain,
( ~ cC58(A)
| ~ cC2xcomp(A)
| cC60(A) ),
inference(clausify,[status(thm)],[axiom_61]) ).
cnf(c_265,plain,
( ~ cC60(B)
| ~ rR1(A,B)
| cC62(A) ),
inference(clausify,[status(thm)],[axiom_62]) ).
cnf(c_308,plain,
( ~ cC6xcomp(B)
| ~ rR1(A,B)
| cC8(A) ),
inference(clausify,[status(thm)],[axiom_79]) ).
cnf(c_311,plain,
( ~ cC2xcomp(A)
| ~ cC78xcomp(A)
| cC80(A) ),
inference(clausify,[status(thm)],[axiom_80]) ).
cnf(c_316,plain,
( ~ cC80(B)
| ~ rR1(A,B)
| cC82(A) ),
inference(clausify,[status(thm)],[axiom_82]) ).
fof(axiom_103,axiom,
rR1(iV8467,iV8471),
file('theBenchmark.p',axiom_103) ).
cnf(c_357,plain,
rR1(iV8467,iV8471),
inference(clausify,[status(thm)],[axiom_103]) ).
fof(axiom_104,axiom,
rR1(iV8467,iV8470),
file('theBenchmark.p',axiom_104) ).
cnf(c_358,plain,
rR1(iV8467,iV8470),
inference(clausify,[status(thm)],[axiom_104]) ).
fof(axiom_105,axiom,
rR1(iV8467,iV8469),
file('theBenchmark.p',axiom_105) ).
cnf(c_359,plain,
rR1(iV8467,iV8469),
inference(clausify,[status(thm)],[axiom_105]) ).
fof(axiom_106,axiom,
rR1(iV8467,iV8474),
file('theBenchmark.p',axiom_106) ).
cnf(c_360,plain,
rR1(iV8467,iV8474),
inference(clausify,[status(thm)],[axiom_106]) ).
fof(axiom_110,axiom,
rR1(iV8467,iV8472),
file('theBenchmark.p',axiom_110) ).
cnf(c_361,plain,
rR1(iV8467,iV8472),
inference(clausify,[status(thm)],[axiom_110]) ).
fof(axiom_113,axiom,
cC6xcomp(iV8469),
file('theBenchmark.p',axiom_113) ).
cnf(c_362,plain,
cC6xcomp(iV8469),
inference(clausify,[status(thm)],[axiom_113]) ).
fof(axiom_116,axiom,
cTOP(iV8470),
file('theBenchmark.p',axiom_116) ).
cnf(c_364,plain,
cTOP(iV8470),
inference(clausify,[status(thm)],[axiom_116]) ).
fof(axiom_118,axiom,
cC78xcomp(iV8471),
file('theBenchmark.p',axiom_118) ).
cnf(c_365,plain,
cC78xcomp(iV8471),
inference(clausify,[status(thm)],[axiom_118]) ).
fof(axiom_119,axiom,
cC2xcomp(iV8471),
file('theBenchmark.p',axiom_119) ).
cnf(c_366,plain,
cC2xcomp(iV8471),
inference(clausify,[status(thm)],[axiom_119]) ).
fof(axiom_122,axiom,
cC2xcomp(iV8472),
file('theBenchmark.p',axiom_122) ).
cnf(c_368,plain,
cC2xcomp(iV8472),
inference(clausify,[status(thm)],[axiom_122]) ).
fof(axiom_124,axiom,
rR1(iV8472,iV8476),
file('theBenchmark.p',axiom_124) ).
cnf(c_369,plain,
rR1(iV8472,iV8476),
inference(clausify,[status(thm)],[axiom_124]) ).
fof(axiom_127,axiom,
cC32xcomp(iV8474),
file('theBenchmark.p',axiom_127) ).
cnf(c_370,plain,
cC32xcomp(iV8474),
inference(clausify,[status(thm)],[axiom_127]) ).
fof(axiom_132,axiom,
cC2(iV8476),
file('theBenchmark.p',axiom_132) ).
cnf(c_372,plain,
cC2(iV8476),
inference(clausify,[status(thm)],[axiom_132]) ).
fof(nnf_101,plain,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(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,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ( ( xsd_integer(sK4)
| ~ xsd_string(sK4) )
& ( ~ xsd_integer(sK4)
| xsd_string(sK4) ) )
| cowlNothing(sK3)
| ~ cowlThing(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X0,sK3),skolemize(X,sK4)],[nnf_101]) ).
fof(sk_the_axiom_neg,plain,
( ( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4)
| cowlNothing(sK3)
| ~ cowlThing(sK3) )
& ( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4)
| cowlNothing(sK3)
| ~ cowlThing(sK3) ) ),
inference(cnf_transformation,[status(thm)],[sk_the_axiom_neg_sk]) ).
cnf(c_373,negated_conjecture,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4)
| cowlNothing(sK3)
| ~ cowlThing(sK3) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_2712,negated_conjecture,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4)
| cowlNothing(sK3) ),
inference(resolve,[status(thm)],[c_115,c_373]) ).
cnf(c_2713,negated_conjecture,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_116,c_2712]) ).
cnf(c_2714,negated_conjecture,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_115,c_2713]) ).
cnf(c_2715,negated_conjecture,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_115,c_2714]) ).
cnf(c_374,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_115,c_2715]) ).
cnf(c_375,negated_conjecture,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4)
| cowlNothing(sK3)
| ~ cowlThing(sK3) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_2716,negated_conjecture,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4)
| cowlNothing(sK3) ),
inference(resolve,[status(thm)],[c_115,c_375]) ).
cnf(c_2717,negated_conjecture,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_116,c_2716]) ).
cnf(c_2718,negated_conjecture,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_115,c_2717]) ).
cnf(c_2719,negated_conjecture,
( ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_115,c_2718]) ).
cnf(c_376,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_115,c_2719]) ).
cnf(c_2720,plain,
( ~ cC2xcomp(iV8471)
| cC80(iV8471) ),
inference(resolve,[status(thm)],[c_311,c_365]) ).
cnf(c_391,plain,
cC80(iV8471),
inference(resolve,[status(thm)],[c_366,c_2720]) ).
cnf(c_392,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_391,c_376]) ).
cnf(c_393,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_391,c_374]) ).
cnf(c_2721,plain,
( ~ cC2xcomp(iV8472)
| cC20(iV8467) ),
inference(resolve,[status(thm)],[c_144,c_361]) ).
cnf(c_395,plain,
cC20(iV8467),
inference(resolve,[status(thm)],[c_368,c_2721]) ).
cnf(c_396,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_395,c_393]) ).
cnf(c_397,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_395,c_392]) ).
cnf(c_399,plain,
cC2xcomp(sK0(iV8467)),
inference(resolve,[status(thm)],[c_395,c_143]) ).
cnf(c_400,plain,
rR1(iV8467,sK0(iV8467)),
inference(resolve,[status(thm)],[c_395,c_142]) ).
cnf(c_2722,plain,
( ~ cC2xcomp(sK0(iV8467))
| cC4(iV8467) ),
inference(resolve,[status(thm)],[c_198,c_400]) ).
cnf(c_411,plain,
cC4(iV8467),
inference(resolve,[status(thm)],[c_399,c_2722]) ).
cnf(c_413,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_411,c_397]) ).
cnf(c_414,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC48(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_411,c_396]) ).
cnf(c_415,plain,
cC2xcomp(sK2(iV8467)),
inference(resolve,[status(thm)],[c_411,c_197]) ).
cnf(c_416,plain,
rR1(iV8467,sK2(iV8467)),
inference(resolve,[status(thm)],[c_411,c_196]) ).
cnf(c_2723,plain,
( ~ cC2xcomp(sK2(iV8467))
| cC22(iV8467) ),
inference(resolve,[status(thm)],[c_151,c_416]) ).
cnf(c_501,plain,
cC22(iV8467),
inference(resolve,[status(thm)],[c_415,c_2723]) ).
cnf(c_503,plain,
cC2xcomp(sK1(iV8467)),
inference(resolve,[status(thm)],[c_501,c_150]) ).
cnf(c_504,plain,
rR1(iV8467,sK1(iV8467)),
inference(resolve,[status(thm)],[c_501,c_149]) ).
cnf(c_2724,plain,
( ~ cC2xcomp(sK1(iV8467))
| cC48(iV8467) ),
inference(resolve,[status(thm)],[c_221,c_504]) ).
cnf(c_516,plain,
cC48(iV8467),
inference(resolve,[status(thm)],[c_503,c_2724]) ).
cnf(c_519,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_516,c_414]) ).
cnf(c_520,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_516,c_413]) ).
cnf(c_2725,plain,
( ~ cC2(iV8476)
| cC58(iV8472) ),
inference(resolve,[status(thm)],[c_252,c_369]) ).
cnf(c_560,plain,
cC58(iV8472),
inference(resolve,[status(thm)],[c_372,c_2725]) ).
cnf(c_566,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_560,c_520]) ).
cnf(c_567,negated_conjecture,
( ~ cC60(iV8472)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_560,c_519]) ).
cnf(c_2726,plain,
( ~ cC2xcomp(iV8472)
| cC60(iV8472) ),
inference(resolve,[status(thm)],[c_560,c_262]) ).
cnf(c_569,plain,
cC60(iV8472),
inference(resolve,[status(thm)],[c_368,c_2726]) ).
cnf(c_572,negated_conjecture,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_569,c_567]) ).
cnf(c_573,negated_conjecture,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_569,c_566]) ).
cnf(c_2727,plain,
( ~ cC60(iV8472)
| cC62(iV8467) ),
inference(resolve,[status(thm)],[c_265,c_361]) ).
cnf(c_603,plain,
cC62(iV8467),
inference(resolve,[status(thm)],[c_569,c_2727]) ).
cnf(c_604,negated_conjecture,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_603,c_573]) ).
cnf(c_605,negated_conjecture,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_603,c_572]) ).
cnf(c_2728,plain,
( ~ cC80(iV8471)
| cC82(iV8467) ),
inference(resolve,[status(thm)],[c_316,c_357]) ).
cnf(c_691,plain,
cC82(iV8467),
inference(resolve,[status(thm)],[c_391,c_2728]) ).
cnf(c_692,negated_conjecture,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC8(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_691,c_605]) ).
cnf(c_693,negated_conjecture,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC8(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_691,c_604]) ).
cnf(c_2729,plain,
( ~ cTOP(iV8470)
| cC14(iV8467) ),
inference(resolve,[status(thm)],[c_358,c_129]) ).
cnf(c_2601,plain,
cC14(iV8467),
inference(resolve,[status(thm)],[c_364,c_2729]) ).
cnf(c_2603,negated_conjecture,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC8(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_2601,c_693]) ).
cnf(c_2604,negated_conjecture,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC8(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_2601,c_692]) ).
cnf(c_2730,plain,
( ~ cC6xcomp(iV8469)
| cC8(iV8467) ),
inference(resolve,[status(thm)],[c_359,c_308]) ).
cnf(c_2611,plain,
cC8(iV8467),
inference(resolve,[status(thm)],[c_362,c_2730]) ).
cnf(c_2628,negated_conjecture,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_2611,c_2604]) ).
cnf(c_2629,negated_conjecture,
( ~ cC10(iV8467)
| ~ cC34(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_2611,c_2603]) ).
cnf(c_2731,plain,
( ~ cC4(iV8467)
| cC10(iV8467) ),
inference(resolve,[status(thm)],[c_2611,c_121]) ).
cnf(c_2632,plain,
cC10(iV8467),
inference(resolve,[status(thm)],[c_411,c_2731]) ).
cnf(c_2633,negated_conjecture,
( ~ cC34(iV8467)
| xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_2632,c_2629]) ).
cnf(c_2634,negated_conjecture,
( ~ cC34(iV8467)
| ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_2632,c_2628]) ).
cnf(c_2732,plain,
( ~ cC32xcomp(iV8474)
| cC34(iV8467) ),
inference(resolve,[status(thm)],[c_360,c_183]) ).
cnf(c_2649,plain,
cC34(iV8467),
inference(resolve,[status(thm)],[c_370,c_2732]) ).
cnf(c_2655,negated_conjecture,
( ~ xsd_integer(sK4)
| xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_2649,c_2634]) ).
cnf(c_2656,negated_conjecture,
( xsd_integer(sK4)
| ~ xsd_string(sK4) ),
inference(resolve,[status(thm)],[c_2649,c_2633]) ).
cnf(c_2733,negated_conjecture,
( xsd_integer(sK4)
| xsd_integer(sK4) ),
inference(resolve,[status(thm)],[c_2656,c_118]) ).
cnf(c_2709,negated_conjecture,
xsd_integer(sK4),
inference(copy,[status(thm)],[c_2733]) ).
cnf(c_2710,negated_conjecture,
xsd_string(sK4),
inference(resolve,[status(thm)],[c_2709,c_2655]) ).
cnf(c_2734,negated_conjecture,
~ xsd_integer(sK4),
inference(resolve,[status(thm)],[c_2710,c_117]) ).
cnf(c_2711,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_2709,c_2734]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : KRS155+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n005.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Fri Sep 25 19:41:17 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.45 % Process 7462 was started by sandbox2 on n005,
% 0.17/0.45 % Fri Sep 25 19:41:17 2026
% 0.17/0.45 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.49
% 0.17/0.49 % From the command line: assign(max_seconds, 300).
% 0.17/0.49
% 0.17/0.49 % SInE: 123 to sos, 11 to usable, of 134 axioms (tolerance 2.00, depth 0 fixpoint).
% 1.90/0.76
% 1.90/0.76 % given #500 (T,wt=6): 897 cC36(iV8473) | rR1(iV8467,f27(iV8467)). [resolve(888,a,193,a)].
% 1.90/0.76
% 1.90/0.76 % given #1000 (A,wt=805): 320 -cC84(A) | cC2xcomp(f68(A)) # tptp_name(axiom_84) # sine_depth(9). [clausify(83)].
% 1.90/0.76
% 1.90/0.76 % SZS status Theorem for theBenchmark
% 1.90/0.76
% 1.90/0.76 % Proof 1 at 0.17 (+ 0.07) seconds.
% 1.90/0.76 % Length of proof is 102.
% 1.90/0.76 % Level of proof is 20.
% 1.90/0.76 % Maximum clause weight is 407.000.
% 1.90/0.76 % Given clauses 1319.
% 1.90/0.76
% 1.90/0.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------