%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS161+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:11 AM UTC 2026
% Result : Theorem 2.90s 0.94s
% Output : CNFRefutation 2.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 57
% Number of leaves : 61
% Syntax : Number of formulae : 283 ( 112 unt; 0 def)
% Number of atoms : 3028 ( 0 equ)
% Maximal formula atoms : 98 ( 10 avg)
% Number of connectives : 5351 (2606 ~;2606 |; 115 &)
% ( 20 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 51 ( 11 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 46 ( 45 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 15 con; 0-0 aty)
% Number of variables : 63 ( 2 sgn 27 !; 5 ?)
% 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_10,axiom,
! [X] :
( cC104(X)
<=> ? [Y] :
( cC102xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_10) ).
fof(axiom_11,axiom,
! [X] :
( cC106(X)
<=> ( cC100xcomp(X)
& cC104(X) ) ),
file('theBenchmark.p',axiom_11) ).
fof(axiom_12,axiom,
! [X] :
( cC108(X)
<=> ( cC106(X)
& cC28(X) ) ),
file('theBenchmark.p',axiom_12) ).
fof(axiom_52,axiom,
! [X] :
( cC34(X)
<=> ( cC32xcomp(X)
& cC30xcomp(X) ) ),
file('theBenchmark.p',axiom_52) ).
fof(axiom_57,axiom,
! [X] :
( cC38(X)
<=> ( cC36xcomp(X)
& cTOP(X) ) ),
file('theBenchmark.p',axiom_57) ).
fof(axiom_65,axiom,
! [X] :
( cC42(X)
<=> ? [Y] :
( cC8xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_65) ).
fof(axiom_66,axiom,
! [X] :
( cC44(X)
<=> ( cC42(X)
& cC40xcomp(X) ) ),
file('theBenchmark.p',axiom_66) ).
fof(axiom_73,axiom,
! [X] :
( cC50(X)
<=> ( cC48xcomp(X)
& cC46xcomp(X) ) ),
file('theBenchmark.p',axiom_73) ).
fof(axiom_82,axiom,
! [X] :
( cC56(X)
<=> ( cC44(X)
& cC54xcomp(X) ) ),
file('theBenchmark.p',axiom_82) ).
fof(axiom_91,axiom,
! [X] :
( cC60(X)
<=> ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_91) ).
fof(axiom_92,axiom,
! [X] :
( cC62(X)
<=> ( cC58xcomp(X)
& cC60(X) ) ),
file('theBenchmark.p',axiom_92) ).
fof(axiom_100,axiom,
! [X] :
( cC68(X)
<=> ( cC66xcomp(X)
& cC64xcomp(X) ) ),
file('theBenchmark.p',axiom_100) ).
fof(axiom_112,axiom,
! [X] :
( cC76(X)
<=> ( cC62(X)
& cC74xcomp(X) ) ),
file('theBenchmark.p',axiom_112) ).
fof(axiom_120,axiom,
! [X] :
( cC82(X)
<=> ( cC78xcomp(X)
& cC80(X) ) ),
file('theBenchmark.p',axiom_120) ).
fof(axiom_128,axiom,
! [X] :
( cC88(X)
<=> ( cC86xcomp(X)
& cC84xcomp(X) ) ),
file('theBenchmark.p',axiom_128) ).
fof(axiom_143,axiom,
! [X] :
( cC98(X)
<=> ( cC82(X)
& cC96xcomp(X) ) ),
file('theBenchmark.p',axiom_143) ).
fof(axiom_145,axiom,
! [X] :
( cTEST(X)
<=> ( cC130(X)
& cC108(X) ) ),
file('theBenchmark.p',axiom_145) ).
fof(axiom_146,axiom,
! [X] :
( rR1(iV16439,X)
=> cC98(X) ),
file('theBenchmark.p',axiom_146) ).
fof(axiom_156,axiom,
! [X] :
( rR1(iV16440,X)
=> cC76(X) ),
file('theBenchmark.p',axiom_156) ).
fof(axiom_178,axiom,
! [X] :
( rR1(iV16453,X)
=> cC56(X) ),
file('theBenchmark.p',axiom_178) ).
fof(axiom_261,axiom,
! [X] :
( rR1(iV16463,X)
=> cC56(X) ),
file('theBenchmark.p',axiom_261) ).
fof(the_axiom,conjecture,
( cowlThing(iV16465)
& cC38(iV16465)
& cowlThing(iV16464)
& cC44(iV16464)
& cC42(iV16464)
& cC56(iV16464)
& cC60(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC76(iV16463)
& cowlThing(iV16462)
& cC38(iV16462)
& cowlThing(iV16461)
& cC44(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16460)
& cC38(iV16460)
& cowlThing(iV16459)
& cC68(iV16459)
& cC34(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cowlThing(iV16457)
& cC38(iV16457)
& cowlThing(iV16455)
& cC42(iV16455)
& cC44(iV16455)
& cC56(iV16455)
& cC60(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC76(iV16453)
& cowlThing(iV16448)
& cC38(iV16448)
& cowlThing(iV16440)
& cC82(iV16440)
& cC80(iV16440)
& cC98(iV16440)
& cowlThing(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& cC104(iV16439)
& cC108(iV16439)
& cC130(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(the_axiom_neg,negated_conjecture,
~ ( cowlThing(iV16465)
& cC38(iV16465)
& cowlThing(iV16464)
& cC44(iV16464)
& cC42(iV16464)
& cC56(iV16464)
& cC60(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC76(iV16463)
& cowlThing(iV16462)
& cC38(iV16462)
& cowlThing(iV16461)
& cC44(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16460)
& cC38(iV16460)
& cowlThing(iV16459)
& cC68(iV16459)
& cC34(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cowlThing(iV16457)
& cC38(iV16457)
& cowlThing(iV16455)
& cC42(iV16455)
& cC44(iV16455)
& cC56(iV16455)
& cC60(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC76(iV16453)
& cowlThing(iV16448)
& cC38(iV16448)
& cowlThing(iV16440)
& cC82(iV16440)
& cC80(iV16440)
& cC98(iV16440)
& cowlThing(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& cC104(iV16439)
& cC108(iV16439)
& cC130(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
cnf(c_239,plain,
cowlThing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_240,plain,
~ cowlNothing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_241,plain,
( ~ xsd_integer(A)
| ~ xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_242,plain,
( xsd_integer(A)
| xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_263,plain,
( ~ cC102xcomp(B)
| ~ rR1(A,B)
| cC104(A) ),
inference(clausify,[status(thm)],[axiom_10]) ).
cnf(c_266,plain,
( ~ cC100xcomp(A)
| ~ cC104(A)
| cC106(A) ),
inference(clausify,[status(thm)],[axiom_11]) ).
cnf(c_267,plain,
( cC28(A)
| ~ cC108(A) ),
inference(clausify,[status(thm)],[axiom_12]) ).
cnf(c_362,plain,
( ~ cC32xcomp(A)
| ~ cC30xcomp(A)
| cC34(A) ),
inference(clausify,[status(thm)],[axiom_52]) ).
cnf(c_365,plain,
( ~ cC36xcomp(A)
| ~ cTOP(A)
| cC38(A) ),
inference(clausify,[status(thm)],[axiom_57]) ).
cnf(c_372,plain,
( ~ cC8xcomp(B)
| ~ rR1(A,B)
| cC42(A) ),
inference(clausify,[status(thm)],[axiom_65]) ).
cnf(c_375,plain,
( ~ cC42(A)
| ~ cC40xcomp(A)
| cC44(A) ),
inference(clausify,[status(thm)],[axiom_66]) ).
cnf(c_392,plain,
( ~ cC48xcomp(A)
| ~ cC46xcomp(A)
| cC50(A) ),
inference(clausify,[status(thm)],[axiom_73]) ).
cnf(c_394,plain,
( cC44(A)
| ~ cC56(A) ),
inference(clausify,[status(thm)],[axiom_82]) ).
cnf(c_395,plain,
( ~ cC44(A)
| ~ cC54xcomp(A)
| cC56(A) ),
inference(clausify,[status(thm)],[axiom_82]) ).
cnf(c_416,plain,
( ~ cC12xcomp(B)
| ~ rR1(A,B)
| cC60(A) ),
inference(clausify,[status(thm)],[axiom_91]) ).
cnf(c_419,plain,
( ~ cC58xcomp(A)
| ~ cC60(A)
| cC62(A) ),
inference(clausify,[status(thm)],[axiom_92]) ).
cnf(c_438,plain,
( ~ cC66xcomp(A)
| ~ cC64xcomp(A)
| cC68(A) ),
inference(clausify,[status(thm)],[axiom_100]) ).
cnf(c_465,plain,
( cC62(A)
| ~ cC76(A) ),
inference(clausify,[status(thm)],[axiom_112]) ).
cnf(c_466,plain,
( ~ cC62(A)
| ~ cC74xcomp(A)
| cC76(A) ),
inference(clausify,[status(thm)],[axiom_112]) ).
cnf(c_483,plain,
( cC80(A)
| ~ cC82(A) ),
inference(clausify,[status(thm)],[axiom_120]) ).
cnf(c_504,plain,
( ~ cC86xcomp(A)
| ~ cC84xcomp(A)
| cC88(A) ),
inference(clausify,[status(thm)],[axiom_128]) ).
cnf(c_538,plain,
( cC82(A)
| ~ cC98(A) ),
inference(clausify,[status(thm)],[axiom_143]) ).
cnf(c_542,plain,
( cC108(A)
| ~ cTEST(A) ),
inference(clausify,[status(thm)],[axiom_145]) ).
cnf(c_543,plain,
( cC130(A)
| ~ cTEST(A) ),
inference(clausify,[status(thm)],[axiom_145]) ).
cnf(c_545,plain,
( cC98(A)
| ~ rR1(iV16439,A) ),
inference(clausify,[status(thm)],[axiom_146]) ).
fof(axiom_148,axiom,
cC100xcomp(iV16439),
file('theBenchmark.p',axiom_148) ).
cnf(c_546,plain,
cC100xcomp(iV16439),
inference(clausify,[status(thm)],[axiom_148]) ).
fof(axiom_149,axiom,
cTEST(iV16439),
file('theBenchmark.p',axiom_149) ).
cnf(c_547,plain,
cTEST(iV16439),
inference(clausify,[status(thm)],[axiom_149]) ).
fof(axiom_150,axiom,
rR1(iV16439,iV16440),
file('theBenchmark.p',axiom_150) ).
cnf(c_548,plain,
rR1(iV16439,iV16440),
inference(clausify,[status(thm)],[axiom_150]) ).
cnf(c_551,plain,
( cC76(A)
| ~ rR1(iV16440,A) ),
inference(clausify,[status(thm)],[axiom_156]) ).
fof(axiom_157,axiom,
cC102xcomp(iV16440),
file('theBenchmark.p',axiom_157) ).
cnf(c_552,plain,
cC102xcomp(iV16440),
inference(clausify,[status(thm)],[axiom_157]) ).
fof(axiom_159,axiom,
rR1(iV16440,iV16463),
file('theBenchmark.p',axiom_159) ).
cnf(c_554,plain,
rR1(iV16440,iV16463),
inference(clausify,[status(thm)],[axiom_159]) ).
fof(axiom_163,axiom,
cTOP(iV16448),
file('theBenchmark.p',axiom_163) ).
cnf(c_555,plain,
cTOP(iV16448),
inference(clausify,[status(thm)],[axiom_163]) ).
fof(axiom_168,axiom,
cC36xcomp(iV16448),
file('theBenchmark.p',axiom_168) ).
cnf(c_560,plain,
cC36xcomp(iV16448),
inference(clausify,[status(thm)],[axiom_168]) ).
fof(axiom_174,axiom,
cC74xcomp(iV16453),
file('theBenchmark.p',axiom_174) ).
cnf(c_564,plain,
cC74xcomp(iV16453),
inference(clausify,[status(thm)],[axiom_174]) ).
cnf(c_567,plain,
( cC56(A)
| ~ rR1(iV16453,A) ),
inference(clausify,[status(thm)],[axiom_178]) ).
fof(axiom_181,axiom,
cC58xcomp(iV16453),
file('theBenchmark.p',axiom_181) ).
cnf(c_570,plain,
cC58xcomp(iV16453),
inference(clausify,[status(thm)],[axiom_181]) ).
fof(axiom_182,axiom,
rR1(iV16453,iV16461),
file('theBenchmark.p',axiom_182) ).
cnf(c_571,plain,
rR1(iV16453,iV16461),
inference(clausify,[status(thm)],[axiom_182]) ).
fof(axiom_185,axiom,
cC40xcomp(iV16455),
file('theBenchmark.p',axiom_185) ).
cnf(c_573,plain,
cC40xcomp(iV16455),
inference(clausify,[status(thm)],[axiom_185]) ).
fof(axiom_190,axiom,
cC54xcomp(iV16455),
file('theBenchmark.p',axiom_190) ).
cnf(c_578,plain,
cC54xcomp(iV16455),
inference(clausify,[status(thm)],[axiom_190]) ).
fof(axiom_193,axiom,
rR1(iV16455,iV16460),
file('theBenchmark.p',axiom_193) ).
cnf(c_581,plain,
rR1(iV16455,iV16460),
inference(clausify,[status(thm)],[axiom_193]) ).
fof(axiom_197,axiom,
cTOP(iV16457),
file('theBenchmark.p',axiom_197) ).
cnf(c_584,plain,
cTOP(iV16457),
inference(clausify,[status(thm)],[axiom_197]) ).
fof(axiom_201,axiom,
cC36xcomp(iV16457),
file('theBenchmark.p',axiom_201) ).
cnf(c_588,plain,
cC36xcomp(iV16457),
inference(clausify,[status(thm)],[axiom_201]) ).
fof(axiom_209,axiom,
cC30xcomp(iV16459),
file('theBenchmark.p',axiom_209) ).
cnf(c_595,plain,
cC30xcomp(iV16459),
inference(clausify,[status(thm)],[axiom_209]) ).
fof(axiom_210,axiom,
cC84xcomp(iV16459),
file('theBenchmark.p',axiom_210) ).
cnf(c_596,plain,
cC84xcomp(iV16459),
inference(clausify,[status(thm)],[axiom_210]) ).
fof(axiom_212,axiom,
cC46xcomp(iV16459),
file('theBenchmark.p',axiom_212) ).
cnf(c_598,plain,
cC46xcomp(iV16459),
inference(clausify,[status(thm)],[axiom_212]) ).
fof(axiom_213,axiom,
cC64xcomp(iV16459),
file('theBenchmark.p',axiom_213) ).
cnf(c_599,plain,
cC64xcomp(iV16459),
inference(clausify,[status(thm)],[axiom_213]) ).
fof(axiom_215,axiom,
cC86xcomp(iV16459),
file('theBenchmark.p',axiom_215) ).
cnf(c_601,plain,
cC86xcomp(iV16459),
inference(clausify,[status(thm)],[axiom_215]) ).
fof(axiom_216,axiom,
cC32xcomp(iV16459),
file('theBenchmark.p',axiom_216) ).
cnf(c_602,plain,
cC32xcomp(iV16459),
inference(clausify,[status(thm)],[axiom_216]) ).
fof(axiom_217,axiom,
cC48xcomp(iV16459),
file('theBenchmark.p',axiom_217) ).
cnf(c_603,plain,
cC48xcomp(iV16459),
inference(clausify,[status(thm)],[axiom_217]) ).
fof(axiom_221,axiom,
cC66xcomp(iV16459),
file('theBenchmark.p',axiom_221) ).
cnf(c_607,plain,
cC66xcomp(iV16459),
inference(clausify,[status(thm)],[axiom_221]) ).
fof(axiom_225,axiom,
cTOP(iV16460),
file('theBenchmark.p',axiom_225) ).
cnf(c_610,plain,
cTOP(iV16460),
inference(clausify,[status(thm)],[axiom_225]) ).
fof(axiom_227,axiom,
cC8xcomp(iV16460),
file('theBenchmark.p',axiom_227) ).
cnf(c_612,plain,
cC8xcomp(iV16460),
inference(clausify,[status(thm)],[axiom_227]) ).
fof(axiom_228,axiom,
cC36xcomp(iV16460),
file('theBenchmark.p',axiom_228) ).
cnf(c_613,plain,
cC36xcomp(iV16460),
inference(clausify,[status(thm)],[axiom_228]) ).
fof(axiom_237,axiom,
cC12xcomp(iV16461),
file('theBenchmark.p',axiom_237) ).
cnf(c_621,plain,
cC12xcomp(iV16461),
inference(clausify,[status(thm)],[axiom_237]) ).
fof(axiom_243,axiom,
rR1(iV16461,iV16462),
file('theBenchmark.p',axiom_243) ).
cnf(c_627,plain,
rR1(iV16461,iV16462),
inference(clausify,[status(thm)],[axiom_243]) ).
fof(axiom_247,axiom,
cTOP(iV16462),
file('theBenchmark.p',axiom_247) ).
cnf(c_630,plain,
cTOP(iV16462),
inference(clausify,[status(thm)],[axiom_247]) ).
fof(axiom_249,axiom,
cC8xcomp(iV16462),
file('theBenchmark.p',axiom_249) ).
cnf(c_632,plain,
cC8xcomp(iV16462),
inference(clausify,[status(thm)],[axiom_249]) ).
fof(axiom_252,axiom,
cC36xcomp(iV16462),
file('theBenchmark.p',axiom_252) ).
cnf(c_635,plain,
cC36xcomp(iV16462),
inference(clausify,[status(thm)],[axiom_252]) ).
cnf(c_643,plain,
( cC56(A)
| ~ rR1(iV16463,A) ),
inference(clausify,[status(thm)],[axiom_261]) ).
fof(axiom_263,axiom,
rR1(iV16463,iV16464),
file('theBenchmark.p',axiom_263) ).
cnf(c_645,plain,
rR1(iV16463,iV16464),
inference(clausify,[status(thm)],[axiom_263]) ).
fof(axiom_267,axiom,
cC12xcomp(iV16464),
file('theBenchmark.p',axiom_267) ).
cnf(c_648,plain,
cC12xcomp(iV16464),
inference(clausify,[status(thm)],[axiom_267]) ).
fof(axiom_274,axiom,
rR1(iV16464,iV16465),
file('theBenchmark.p',axiom_274) ).
cnf(c_655,plain,
rR1(iV16464,iV16465),
inference(clausify,[status(thm)],[axiom_274]) ).
fof(axiom_277,axiom,
cTOP(iV16465),
file('theBenchmark.p',axiom_277) ).
cnf(c_657,plain,
cTOP(iV16465),
inference(clausify,[status(thm)],[axiom_277]) ).
fof(axiom_280,axiom,
cC8xcomp(iV16465),
file('theBenchmark.p',axiom_280) ).
cnf(c_660,plain,
cC8xcomp(iV16465),
inference(clausify,[status(thm)],[axiom_280]) ).
fof(axiom_282,axiom,
cC36xcomp(iV16465),
file('theBenchmark.p',axiom_282) ).
cnf(c_662,plain,
cC36xcomp(iV16465),
inference(clausify,[status(thm)],[axiom_282]) ).
fof(nnf_188,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [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(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ( ( 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_188]) ).
fof(sk_the_axiom_neg,plain,
( ( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ) ),
inference(cnf_transformation,[status(thm)],[sk_the_axiom_neg_sk]) ).
cnf(c_666,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_1632,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_239,c_666]) ).
cnf(c_1633,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_240,c_1632]) ).
cnf(c_1634,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1633]) ).
cnf(c_1635,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1634]) ).
cnf(c_1636,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1635]) ).
cnf(c_1637,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1636]) ).
cnf(c_1638,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1637]) ).
cnf(c_1639,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1638]) ).
cnf(c_1640,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1639]) ).
cnf(c_1641,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1640]) ).
cnf(c_1642,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1641]) ).
cnf(c_1643,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1642]) ).
cnf(c_1644,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1643]) ).
cnf(c_1645,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1644]) ).
cnf(c_667,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1645]) ).
cnf(c_668,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_1646,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_239,c_668]) ).
cnf(c_1647,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_240,c_1646]) ).
cnf(c_1648,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1647]) ).
cnf(c_1649,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1648]) ).
cnf(c_1650,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1649]) ).
cnf(c_1651,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1650]) ).
cnf(c_1652,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1651]) ).
cnf(c_1653,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1652]) ).
cnf(c_1654,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1653]) ).
cnf(c_1655,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1654]) ).
cnf(c_1656,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1655]) ).
cnf(c_1657,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1656]) ).
cnf(c_1658,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1657]) ).
cnf(c_1659,negated_conjecture,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1658]) ).
cnf(c_669,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_239,c_1659]) ).
cnf(c_1660,plain,
( ~ cC102xcomp(iV16440)
| cC104(iV16439) ),
inference(resolve,[status(thm)],[c_263,c_548]) ).
cnf(c_697,plain,
cC104(iV16439),
inference(resolve,[status(thm)],[c_552,c_1660]) ).
cnf(c_699,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_697,c_669]) ).
cnf(c_700,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_697,c_667]) ).
cnf(c_1661,plain,
( ~ cC36xcomp(iV16465)
| cC38(iV16465) ),
inference(resolve,[status(thm)],[c_365,c_657]) ).
cnf(c_911,plain,
cC38(iV16465),
inference(resolve,[status(thm)],[c_662,c_1661]) ).
cnf(c_1662,plain,
( ~ cC36xcomp(iV16462)
| cC38(iV16462) ),
inference(resolve,[status(thm)],[c_365,c_630]) ).
cnf(c_912,plain,
cC38(iV16462),
inference(resolve,[status(thm)],[c_635,c_1662]) ).
cnf(c_1663,plain,
( ~ cC36xcomp(iV16460)
| cC38(iV16460) ),
inference(resolve,[status(thm)],[c_365,c_610]) ).
cnf(c_913,plain,
cC38(iV16460),
inference(resolve,[status(thm)],[c_613,c_1663]) ).
cnf(c_1664,plain,
( ~ cC36xcomp(iV16457)
| cC38(iV16457) ),
inference(resolve,[status(thm)],[c_365,c_584]) ).
cnf(c_914,plain,
cC38(iV16457),
inference(resolve,[status(thm)],[c_588,c_1664]) ).
cnf(c_1665,plain,
( ~ cC36xcomp(iV16448)
| cC38(iV16448) ),
inference(resolve,[status(thm)],[c_365,c_555]) ).
cnf(c_915,plain,
cC38(iV16448),
inference(resolve,[status(thm)],[c_560,c_1665]) ).
cnf(c_1666,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_915,c_700]) ).
cnf(c_1667,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_914,c_1666]) ).
cnf(c_1668,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_913,c_1667]) ).
cnf(c_1669,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_912,c_1668]) ).
cnf(c_916,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_911,c_1669]) ).
cnf(c_1670,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_915,c_699]) ).
cnf(c_1671,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_914,c_1670]) ).
cnf(c_1672,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC38(iV16462)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_913,c_1671]) ).
cnf(c_1673,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_912,c_1672]) ).
cnf(c_917,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_911,c_1673]) ).
cnf(c_1674,plain,
( ~ cC8xcomp(iV16465)
| cC42(iV16464) ),
inference(resolve,[status(thm)],[c_372,c_655]) ).
cnf(c_924,plain,
cC42(iV16464),
inference(resolve,[status(thm)],[c_660,c_1674]) ).
cnf(c_1675,plain,
( ~ cC8xcomp(iV16462)
| cC42(iV16461) ),
inference(resolve,[status(thm)],[c_372,c_627]) ).
cnf(c_926,plain,
cC42(iV16461),
inference(resolve,[status(thm)],[c_632,c_1675]) ).
cnf(c_1676,plain,
( ~ cC8xcomp(iV16460)
| cC42(iV16455) ),
inference(resolve,[status(thm)],[c_372,c_581]) ).
cnf(c_927,plain,
cC42(iV16455),
inference(resolve,[status(thm)],[c_612,c_1676]) ).
cnf(c_1677,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_927,c_917]) ).
cnf(c_1678,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_926,c_1677]) ).
cnf(c_934,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_924,c_1678]) ).
cnf(c_1679,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_927,c_916]) ).
cnf(c_1680,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_926,c_1679]) ).
cnf(c_935,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_924,c_1680]) ).
cnf(c_1681,plain,
( ~ cC12xcomp(iV16464)
| cC60(iV16463) ),
inference(resolve,[status(thm)],[c_416,c_645]) ).
cnf(c_1034,plain,
cC60(iV16463),
inference(resolve,[status(thm)],[c_648,c_1681]) ).
cnf(c_1682,plain,
( ~ cC12xcomp(iV16461)
| cC60(iV16453) ),
inference(resolve,[status(thm)],[c_416,c_571]) ).
cnf(c_1037,plain,
cC60(iV16453),
inference(resolve,[status(thm)],[c_621,c_1682]) ).
cnf(c_1683,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1037,c_935]) ).
cnf(c_1043,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1034,c_1683]) ).
cnf(c_1684,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1037,c_934]) ).
cnf(c_1044,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1034,c_1684]) ).
cnf(c_1097,plain,
cC98(iV16440),
inference(resolve,[status(thm)],[c_545,c_548]) ).
cnf(c_1100,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1097,c_1044]) ).
cnf(c_1101,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1097,c_1043]) ).
cnf(c_1102,plain,
cC82(iV16440),
inference(resolve,[status(thm)],[c_1097,c_538]) ).
cnf(c_1103,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC80(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1102,c_1101]) ).
cnf(c_1104,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC80(iV16440)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1102,c_1100]) ).
cnf(c_1119,plain,
cC80(iV16440),
inference(resolve,[status(thm)],[c_1102,c_483]) ).
cnf(c_1120,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1119,c_1104]) ).
cnf(c_1121,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1119,c_1103]) ).
cnf(c_1685,plain,
( ~ cC104(iV16439)
| cC106(iV16439) ),
inference(resolve,[status(thm)],[c_546,c_266]) ).
cnf(c_1446,plain,
cC106(iV16439),
inference(resolve,[status(thm)],[c_697,c_1685]) ).
cnf(c_1448,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1446,c_1121]) ).
cnf(c_1449,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1446,c_1120]) ).
cnf(c_1450,plain,
cC130(iV16439),
inference(resolve,[status(thm)],[c_547,c_543]) ).
cnf(c_1451,plain,
cC108(iV16439),
inference(resolve,[status(thm)],[c_547,c_542]) ).
cnf(c_1686,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1450,c_1449]) ).
cnf(c_1452,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1451,c_1686]) ).
cnf(c_1687,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1450,c_1448]) ).
cnf(c_1453,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1451,c_1687]) ).
cnf(c_1456,plain,
cC28(iV16439),
inference(resolve,[status(thm)],[c_1451,c_267]) ).
cnf(c_1457,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1456,c_1453]) ).
cnf(c_1458,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1456,c_1452]) ).
cnf(c_1466,plain,
cC76(iV16463),
inference(resolve,[status(thm)],[c_551,c_554]) ).
cnf(c_1467,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1466,c_1458]) ).
cnf(c_1468,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC62(iV16463)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1466,c_1457]) ).
cnf(c_1469,plain,
cC62(iV16463),
inference(resolve,[status(thm)],[c_1466,c_465]) ).
cnf(c_1471,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1469,c_1468]) ).
cnf(c_1472,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1469,c_1467]) ).
cnf(c_1500,plain,
( ~ cC62(iV16453)
| cC76(iV16453) ),
inference(resolve,[status(thm)],[c_564,c_466]) ).
cnf(c_1510,plain,
cC56(iV16461),
inference(resolve,[status(thm)],[c_567,c_571]) ).
cnf(c_1511,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1510,c_1472]) ).
cnf(c_1512,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16461)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1510,c_1471]) ).
cnf(c_1514,plain,
cC44(iV16461),
inference(resolve,[status(thm)],[c_1510,c_394]) ).
cnf(c_1515,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1514,c_1512]) ).
cnf(c_1516,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1514,c_1511]) ).
cnf(c_1688,plain,
( ~ cC60(iV16453)
| cC62(iV16453) ),
inference(resolve,[status(thm)],[c_570,c_419]) ).
cnf(c_1527,plain,
cC62(iV16453),
inference(resolve,[status(thm)],[c_1037,c_1688]) ).
cnf(c_1529,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC76(iV16453)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1527,c_1516]) ).
cnf(c_1530,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC76(iV16453)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1527,c_1515]) ).
cnf(c_1531,plain,
cC76(iV16453),
inference(resolve,[status(thm)],[c_1527,c_1500]) ).
cnf(c_1532,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1531,c_1530]) ).
cnf(c_1533,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1531,c_1529]) ).
cnf(c_1689,plain,
( ~ cC42(iV16455)
| cC44(iV16455) ),
inference(resolve,[status(thm)],[c_573,c_375]) ).
cnf(c_1535,plain,
cC44(iV16455),
inference(resolve,[status(thm)],[c_927,c_1689]) ).
cnf(c_1537,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC56(iV16455)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1535,c_1533]) ).
cnf(c_1538,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC56(iV16455)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1535,c_1532]) ).
cnf(c_1690,plain,
( ~ cC44(iV16455)
| cC56(iV16455) ),
inference(resolve,[status(thm)],[c_578,c_395]) ).
cnf(c_1539,plain,
cC56(iV16455),
inference(resolve,[status(thm)],[c_1535,c_1690]) ).
cnf(c_1541,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1539,c_1538]) ).
cnf(c_1542,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1539,c_1537]) ).
cnf(c_1691,plain,
( ~ cC84xcomp(iV16459)
| cC88(iV16459) ),
inference(resolve,[status(thm)],[c_601,c_504]) ).
cnf(c_1601,plain,
cC88(iV16459),
inference(resolve,[status(thm)],[c_596,c_1691]) ).
cnf(c_1602,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1601,c_1542]) ).
cnf(c_1603,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1601,c_1541]) ).
cnf(c_1692,plain,
( ~ cC30xcomp(iV16459)
| cC34(iV16459) ),
inference(resolve,[status(thm)],[c_602,c_362]) ).
cnf(c_1604,plain,
cC34(iV16459),
inference(resolve,[status(thm)],[c_595,c_1692]) ).
cnf(c_1605,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC50(iV16459)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1604,c_1603]) ).
cnf(c_1606,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ cC50(iV16459)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1604,c_1602]) ).
cnf(c_1693,plain,
( ~ cC46xcomp(iV16459)
| cC50(iV16459) ),
inference(resolve,[status(thm)],[c_603,c_392]) ).
cnf(c_1607,plain,
cC50(iV16459),
inference(resolve,[status(thm)],[c_598,c_1693]) ).
cnf(c_1608,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1607,c_1606]) ).
cnf(c_1609,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC56(iV16464)
| ~ cC68(iV16459)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1607,c_1605]) ).
cnf(c_1616,plain,
cC56(iV16464),
inference(resolve,[status(thm)],[c_643,c_645]) ).
cnf(c_1617,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC68(iV16459)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1616,c_1609]) ).
cnf(c_1618,negated_conjecture,
( ~ cC44(iV16464)
| ~ cC68(iV16459)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1616,c_1608]) ).
cnf(c_1620,plain,
cC44(iV16464),
inference(resolve,[status(thm)],[c_1616,c_394]) ).
cnf(c_1621,negated_conjecture,
( ~ cC68(iV16459)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1620,c_1618]) ).
cnf(c_1622,negated_conjecture,
( ~ cC68(iV16459)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1620,c_1617]) ).
cnf(c_1694,plain,
( ~ cC64xcomp(iV16459)
| cC68(iV16459) ),
inference(resolve,[status(thm)],[c_607,c_438]) ).
cnf(c_1623,plain,
cC68(iV16459),
inference(resolve,[status(thm)],[c_599,c_1694]) ).
cnf(c_1624,negated_conjecture,
( ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1623,c_1622]) ).
cnf(c_1625,negated_conjecture,
( xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1623,c_1621]) ).
cnf(c_1695,negated_conjecture,
( xsd_integer(sK1)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_1625,c_242]) ).
cnf(c_1629,negated_conjecture,
xsd_integer(sK1),
inference(copy,[status(thm)],[c_1695]) ).
cnf(c_1630,negated_conjecture,
xsd_string(sK1),
inference(resolve,[status(thm)],[c_1629,c_1624]) ).
cnf(c_1696,negated_conjecture,
~ xsd_integer(sK1),
inference(resolve,[status(thm)],[c_1630,c_241]) ).
cnf(c_1631,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1629,c_1696]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : KRS161+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.15/0.42 % Computer : n005.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Fri Sep 25 19:41:33 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.43 % Process 7852 was started by sandbox2 on n005,
% 0.15/0.43 % Fri Sep 25 19:41:33 2026
% 0.15/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/0.50
% 0.15/0.50 % From the command line: assign(max_seconds, 300).
% 0.15/0.50
% 0.15/0.50 % SInE: 260 to sos, 26 to usable, of 286 axioms (tolerance 2.00, depth 0 fixpoint).
% 2.90/0.94
% 2.90/0.94 % given #500 (T,wt=9): 1007 cC14(iV16465) | cC22(iV16463). [resolve(958,b,838,b)].
% 2.90/0.94
% 2.90/0.94 % SZS status Theorem for theBenchmark
% 2.90/0.94
% 2.90/0.94 % Proof 1 at 0.29 (+ 0.08) seconds.
% 2.90/0.94 % Length of proof is 177.
% 2.90/0.94 % Level of proof is 29.
% 2.90/0.94 % Maximum clause weight is 1007.000.
% 2.90/0.94 % Given clauses 924.
% 2.90/0.94
% 2.90/0.94 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------