%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS153+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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:46:09 AM UTC 2026
% Result : Theorem 2.16s 0.75s
% Output : CNFRefutation 2.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 57
% Number of leaves : 57
% Syntax : Number of formulae : 273 ( 94 unt; 0 def)
% Number of atoms : 3030 ( 0 equ)
% Maximal formula atoms : 98 ( 11 avg)
% Number of connectives : 5392 (2635 ~;2611 |; 117 &)
% ( 22 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 51 ( 12 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 47 ( 46 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 15 con; 0-0 aty)
% Number of variables : 77 ( 2 sgn 32 !; 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_4,axiom,
! [X] :
( cC104(X)
<=> ? [Y] :
( ~ cC102(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_4) ).
fof(axiom_5,axiom,
! [X] :
( cC106(X)
<=> ( cC104(X)
& ~ cC100(X) ) ),
file('theBenchmark.p',axiom_5) ).
fof(axiom_6,axiom,
! [X] :
( cC108(X)
<=> ( cC106(X)
& cC28(X) ) ),
file('theBenchmark.p',axiom_6) ).
fof(axiom_25,axiom,
! [X] :
( cC34(X)
<=> ( ~ cC30(X)
& ~ cC32(X) ) ),
file('theBenchmark.p',axiom_25) ).
fof(axiom_27,axiom,
! [X] :
( cC38(X)
<=> ( cTOP(X)
& ~ cC36(X) ) ),
file('theBenchmark.p',axiom_27) ).
fof(axiom_29,axiom,
! [X] :
( cC42(X)
<=> ? [Y] :
( ~ cC8(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_29) ).
fof(axiom_30,axiom,
! [X] :
( cC44(X)
<=> ( cC42(X)
& ~ cC40(X) ) ),
file('theBenchmark.p',axiom_30) ).
fof(axiom_36,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC54(X)
& cC44(X) ) ),
file('theBenchmark.p',axiom_36) ).
fof(axiom_39,axiom,
! [X] :
( cC60(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_39) ).
fof(axiom_40,axiom,
! [X] :
( cC62(X)
<=> ( ~ cC58(X)
& cC60(X) ) ),
file('theBenchmark.p',axiom_40) ).
fof(axiom_47,axiom,
! [X] :
( cC76(X)
<=> ( cC62(X)
& ~ cC74(X) ) ),
file('theBenchmark.p',axiom_47) ).
fof(axiom_50,axiom,
! [X] :
( cC82(X)
<=> ( cC80(X)
& ~ cC78(X) ) ),
file('theBenchmark.p',axiom_50) ).
fof(axiom_53,axiom,
! [X] :
( cC88(X)
<=> ( ~ cC86(X)
& ~ cC84(X) ) ),
file('theBenchmark.p',axiom_53) ).
fof(axiom_58,axiom,
! [X] :
( cC98(X)
<=> ( cC82(X)
& ~ cC96(X) ) ),
file('theBenchmark.p',axiom_58) ).
fof(axiom_59,axiom,
! [X] :
( cTEST(X)
<=> ( cC130(X)
& cC108(X) ) ),
file('theBenchmark.p',axiom_59) ).
fof(axiom_60,axiom,
! [X] :
( rR1(iV16439,X)
=> cC98(X) ),
file('theBenchmark.p',axiom_60) ).
fof(axiom_67,axiom,
! [X] :
( rR1(iV16440,X)
=> cC76(X) ),
file('theBenchmark.p',axiom_67) ).
fof(axiom_93,axiom,
! [X] :
( rR1(iV16453,X)
=> cC56(X) ),
file('theBenchmark.p',axiom_93) ).
fof(axiom_106,axiom,
! [X] :
( rR1(iV16455,X)
=> cC38(X) ),
file('theBenchmark.p',axiom_106) ).
fof(axiom_154,axiom,
! [X] :
( rR1(iV16461,X)
=> cC38(X) ),
file('theBenchmark.p',axiom_154) ).
fof(axiom_171,axiom,
! [X] :
( rR1(iV16463,X)
=> cC56(X) ),
file('theBenchmark.p',axiom_171) ).
fof(axiom_182,axiom,
! [X] :
( rR1(iV16464,X)
=> cC38(X) ),
file('theBenchmark.p',axiom_182) ).
fof(axiom_32,axiom,
! [X] :
( cC48(X)
<=> ( ~ cC4(X)
& ~ cC8(X) ) ),
file('theBenchmark.p',axiom_32) ).
fof(axiom_33,axiom,
! [X] :
( cC50(X)
<=> ( ~ cC48(X)
& ~ cC46(X) ) ),
file('theBenchmark.p',axiom_33) ).
fof(axiom_42,axiom,
! [X] :
( cC66(X)
<=> ( ~ cC12(X)
& ~ cC8(X) ) ),
file('theBenchmark.p',axiom_42) ).
fof(axiom_43,axiom,
! [X] :
( cC68(X)
<=> ( ~ cC66(X)
& ~ cC64(X) ) ),
file('theBenchmark.p',axiom_43) ).
fof(the_axiom,conjecture,
( cC38(iV16465)
& cowlThing(iV16465)
& cC42(iV16464)
& cC56(iV16464)
& cowlThing(iV16464)
& cC44(iV16464)
& cC60(iV16463)
& cC76(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC38(iV16462)
& cowlThing(iV16462)
& cC42(iV16461)
& cC56(iV16461)
& cowlThing(iV16461)
& cC44(iV16461)
& cC38(iV16460)
& cowlThing(iV16460)
& cC34(iV16459)
& cC50(iV16459)
& cC88(iV16459)
& cowlThing(iV16459)
& cC68(iV16459)
& cC38(iV16457)
& cowlThing(iV16457)
& cC42(iV16455)
& cC56(iV16455)
& cowlThing(iV16455)
& cC44(iV16455)
& cC60(iV16453)
& cC76(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC38(iV16448)
& cowlThing(iV16448)
& cC98(iV16440)
& cC82(iV16440)
& cowlThing(iV16440)
& cC80(iV16440)
& cC104(iV16439)
& cC108(iV16439)
& cowlThing(iV16439)
& cC130(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(the_axiom_neg,negated_conjecture,
~ ( cC38(iV16465)
& cowlThing(iV16465)
& cC42(iV16464)
& cC56(iV16464)
& cowlThing(iV16464)
& cC44(iV16464)
& cC60(iV16463)
& cC76(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC38(iV16462)
& cowlThing(iV16462)
& cC42(iV16461)
& cC56(iV16461)
& cowlThing(iV16461)
& cC44(iV16461)
& cC38(iV16460)
& cowlThing(iV16460)
& cC34(iV16459)
& cC50(iV16459)
& cC88(iV16459)
& cowlThing(iV16459)
& cC68(iV16459)
& cC38(iV16457)
& cowlThing(iV16457)
& cC42(iV16455)
& cC56(iV16455)
& cowlThing(iV16455)
& cC44(iV16455)
& cC60(iV16453)
& cC76(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC38(iV16448)
& cowlThing(iV16448)
& cC98(iV16440)
& cC82(iV16440)
& cowlThing(iV16440)
& cC80(iV16440)
& cC104(iV16439)
& cC108(iV16439)
& cowlThing(iV16439)
& cC130(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
cnf(c_107,plain,
( ~ cC4(A)
| ~ cC48(A) ),
inference(clausify,[status(thm)],[axiom_32]) ).
cnf(c_111,plain,
( cC48(A)
| cC46(A)
| cC50(A) ),
inference(clausify,[status(thm)],[axiom_33]) ).
cnf(c_116,plain,
( ~ cC12(A)
| ~ cC66(A) ),
inference(clausify,[status(thm)],[axiom_42]) ).
cnf(c_120,plain,
( cC66(A)
| cC64(A)
| cC68(A) ),
inference(clausify,[status(thm)],[axiom_43]) ).
fof(axiom_124,axiom,
~ cC46(iV16459),
file('theBenchmark.p',axiom_124) ).
cnf(c_128,plain,
~ cC46(iV16459),
inference(clausify,[status(thm)],[axiom_124]) ).
fof(axiom_133,axiom,
~ cC64(iV16459),
file('theBenchmark.p',axiom_133) ).
cnf(c_130,plain,
~ cC64(iV16459),
inference(clausify,[status(thm)],[axiom_133]) ).
cnf(c_131,plain,
cowlThing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_132,plain,
~ cowlNothing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_133,plain,
( ~ xsd_integer(A)
| ~ xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_134,plain,
( xsd_integer(A)
| xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_143,plain,
( cC102(B)
| ~ rR1(A,B)
| cC104(A) ),
inference(clausify,[status(thm)],[axiom_4]) ).
cnf(c_146,plain,
( ~ cC104(A)
| cC100(A)
| cC106(A) ),
inference(clausify,[status(thm)],[axiom_5]) ).
cnf(c_147,plain,
( cC28(A)
| ~ cC108(A) ),
inference(clausify,[status(thm)],[axiom_6]) ).
cnf(c_206,plain,
( cC30(A)
| cC32(A)
| cC34(A) ),
inference(clausify,[status(thm)],[axiom_25]) ).
cnf(c_212,plain,
( ~ cTOP(A)
| cC36(A)
| cC38(A) ),
inference(clausify,[status(thm)],[axiom_27]) ).
cnf(c_218,plain,
( cC8(B)
| ~ rR1(A,B)
| cC42(A) ),
inference(clausify,[status(thm)],[axiom_29]) ).
cnf(c_220,plain,
( cC42(A)
| ~ cC44(A) ),
inference(clausify,[status(thm)],[axiom_30]) ).
cnf(c_221,plain,
( ~ cC42(A)
| cC40(A)
| cC44(A) ),
inference(clausify,[status(thm)],[axiom_30]) ).
cnf(c_228,plain,
( cC44(A)
| ~ cC56(A) ),
inference(clausify,[status(thm)],[axiom_36]) ).
cnf(c_230,plain,
( cC54(A)
| ~ cC44(A)
| cC56(A) ),
inference(clausify,[status(thm)],[axiom_36]) ).
cnf(c_239,plain,
( cC12(B)
| ~ rR1(A,B)
| cC60(A) ),
inference(clausify,[status(thm)],[axiom_39]) ).
cnf(c_240,plain,
( cC60(A)
| ~ cC62(A) ),
inference(clausify,[status(thm)],[axiom_40]) ).
cnf(c_242,plain,
( cC58(A)
| ~ cC60(A)
| cC62(A) ),
inference(clausify,[status(thm)],[axiom_40]) ).
cnf(c_253,plain,
( cC62(A)
| ~ cC76(A) ),
inference(clausify,[status(thm)],[axiom_47]) ).
cnf(c_254,plain,
( ~ cC62(A)
| cC74(A)
| cC76(A) ),
inference(clausify,[status(thm)],[axiom_47]) ).
cnf(c_262,plain,
( cC80(A)
| ~ cC82(A) ),
inference(clausify,[status(thm)],[axiom_50]) ).
cnf(c_272,plain,
( cC86(A)
| cC84(A)
| cC88(A) ),
inference(clausify,[status(thm)],[axiom_53]) ).
cnf(c_286,plain,
( cC82(A)
| ~ cC98(A) ),
inference(clausify,[status(thm)],[axiom_58]) ).
cnf(c_288,plain,
( cC108(A)
| ~ cTEST(A) ),
inference(clausify,[status(thm)],[axiom_59]) ).
cnf(c_289,plain,
( cC130(A)
| ~ cTEST(A) ),
inference(clausify,[status(thm)],[axiom_59]) ).
cnf(c_291,plain,
( cC98(A)
| ~ rR1(iV16439,A) ),
inference(clausify,[status(thm)],[axiom_60]) ).
fof(axiom_61,axiom,
cTEST(iV16439),
file('theBenchmark.p',axiom_61) ).
cnf(c_292,plain,
cTEST(iV16439),
inference(clausify,[status(thm)],[axiom_61]) ).
fof(axiom_62,axiom,
~ cC100(iV16439),
file('theBenchmark.p',axiom_62) ).
cnf(c_293,plain,
~ cC100(iV16439),
inference(clausify,[status(thm)],[axiom_62]) ).
fof(axiom_64,axiom,
rR1(iV16439,iV16440),
file('theBenchmark.p',axiom_64) ).
cnf(c_294,plain,
rR1(iV16439,iV16440),
inference(clausify,[status(thm)],[axiom_64]) ).
cnf(c_295,plain,
( cC76(A)
| ~ rR1(iV16440,A) ),
inference(clausify,[status(thm)],[axiom_67]) ).
fof(axiom_69,axiom,
~ cC102(iV16440),
file('theBenchmark.p',axiom_69) ).
cnf(c_297,plain,
~ cC102(iV16440),
inference(clausify,[status(thm)],[axiom_69]) ).
fof(axiom_73,axiom,
rR1(iV16440,iV16463),
file('theBenchmark.p',axiom_73) ).
cnf(c_300,plain,
rR1(iV16440,iV16463),
inference(clausify,[status(thm)],[axiom_73]) ).
fof(axiom_76,axiom,
~ cC36(iV16448),
file('theBenchmark.p',axiom_76) ).
cnf(c_301,plain,
~ cC36(iV16448),
inference(clausify,[status(thm)],[axiom_76]) ).
fof(axiom_79,axiom,
cTOP(iV16448),
file('theBenchmark.p',axiom_79) ).
cnf(c_304,plain,
cTOP(iV16448),
inference(clausify,[status(thm)],[axiom_79]) ).
fof(axiom_91,axiom,
~ cC58(iV16453),
file('theBenchmark.p',axiom_91) ).
cnf(c_313,plain,
~ cC58(iV16453),
inference(clausify,[status(thm)],[axiom_91]) ).
fof(axiom_92,axiom,
~ cC74(iV16453),
file('theBenchmark.p',axiom_92) ).
cnf(c_314,plain,
~ cC74(iV16453),
inference(clausify,[status(thm)],[axiom_92]) ).
cnf(c_315,plain,
( cC56(A)
| ~ rR1(iV16453,A) ),
inference(clausify,[status(thm)],[axiom_93]) ).
fof(axiom_96,axiom,
rR1(iV16453,iV16461),
file('theBenchmark.p',axiom_96) ).
cnf(c_317,plain,
rR1(iV16453,iV16461),
inference(clausify,[status(thm)],[axiom_96]) ).
fof(axiom_98,axiom,
~ cC40(iV16455),
file('theBenchmark.p',axiom_98) ).
cnf(c_319,plain,
~ cC40(iV16455),
inference(clausify,[status(thm)],[axiom_98]) ).
fof(axiom_103,axiom,
~ cC54(iV16455),
file('theBenchmark.p',axiom_103) ).
cnf(c_324,plain,
~ cC54(iV16455),
inference(clausify,[status(thm)],[axiom_103]) ).
cnf(c_326,plain,
( cC38(A)
| ~ rR1(iV16455,A) ),
inference(clausify,[status(thm)],[axiom_106]) ).
fof(axiom_107,axiom,
rR1(iV16455,iV16460),
file('theBenchmark.p',axiom_107) ).
cnf(c_327,plain,
rR1(iV16455,iV16460),
inference(clausify,[status(thm)],[axiom_107]) ).
fof(axiom_108,axiom,
~ cC36(iV16457),
file('theBenchmark.p',axiom_108) ).
cnf(c_328,plain,
~ cC36(iV16457),
inference(clausify,[status(thm)],[axiom_108]) ).
fof(axiom_113,axiom,
cTOP(iV16457),
file('theBenchmark.p',axiom_113) ).
cnf(c_333,plain,
cTOP(iV16457),
inference(clausify,[status(thm)],[axiom_113]) ).
fof(axiom_119,axiom,
cC4(iV16459),
file('theBenchmark.p',axiom_119) ).
cnf(c_338,plain,
cC4(iV16459),
inference(clausify,[status(thm)],[axiom_119]) ).
fof(axiom_121,axiom,
~ cC30(iV16459),
file('theBenchmark.p',axiom_121) ).
cnf(c_339,plain,
~ cC30(iV16459),
inference(clausify,[status(thm)],[axiom_121]) ).
fof(axiom_123,axiom,
~ cC86(iV16459),
file('theBenchmark.p',axiom_123) ).
cnf(c_341,plain,
~ cC86(iV16459),
inference(clausify,[status(thm)],[axiom_123]) ).
fof(axiom_128,axiom,
cC12(iV16459),
file('theBenchmark.p',axiom_128) ).
cnf(c_344,plain,
cC12(iV16459),
inference(clausify,[status(thm)],[axiom_128]) ).
fof(axiom_132,axiom,
~ cC84(iV16459),
file('theBenchmark.p',axiom_132) ).
cnf(c_348,plain,
~ cC84(iV16459),
inference(clausify,[status(thm)],[axiom_132]) ).
fof(axiom_135,axiom,
~ cC32(iV16459),
file('theBenchmark.p',axiom_135) ).
cnf(c_349,plain,
~ cC32(iV16459),
inference(clausify,[status(thm)],[axiom_135]) ).
fof(axiom_141,axiom,
~ cC8(iV16460),
file('theBenchmark.p',axiom_141) ).
cnf(c_355,plain,
~ cC8(iV16460),
inference(clausify,[status(thm)],[axiom_141]) ).
fof(axiom_151,axiom,
~ cC12(iV16461),
file('theBenchmark.p',axiom_151) ).
cnf(c_364,plain,
~ cC12(iV16461),
inference(clausify,[status(thm)],[axiom_151]) ).
cnf(c_367,plain,
( cC38(A)
| ~ rR1(iV16461,A) ),
inference(clausify,[status(thm)],[axiom_154]) ).
fof(axiom_157,axiom,
rR1(iV16461,iV16462),
file('theBenchmark.p',axiom_157) ).
cnf(c_369,plain,
rR1(iV16461,iV16462),
inference(clausify,[status(thm)],[axiom_157]) ).
cnf(c_382,plain,
( cC56(A)
| ~ rR1(iV16463,A) ),
inference(clausify,[status(thm)],[axiom_171]) ).
fof(axiom_177,axiom,
rR1(iV16463,iV16464),
file('theBenchmark.p',axiom_177) ).
cnf(c_387,plain,
rR1(iV16463,iV16464),
inference(clausify,[status(thm)],[axiom_177]) ).
cnf(c_392,plain,
( cC38(A)
| ~ rR1(iV16464,A) ),
inference(clausify,[status(thm)],[axiom_182]) ).
fof(axiom_188,axiom,
rR1(iV16464,iV16465),
file('theBenchmark.p',axiom_188) ).
cnf(c_397,plain,
rR1(iV16464,iV16465),
inference(clausify,[status(thm)],[axiom_188]) ).
fof(nnf_102,plain,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(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,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(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_102]) ).
fof(sk_the_axiom_neg,plain,
( ( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ) ),
inference(cnf_transformation,[status(thm)],[sk_the_axiom_neg_sk]) ).
cnf(c_408,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_1406,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_131,c_408]) ).
cnf(c_1407,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_132,c_1406]) ).
cnf(c_1408,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1407]) ).
cnf(c_1409,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1408]) ).
cnf(c_1410,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1409]) ).
cnf(c_1411,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1410]) ).
cnf(c_1412,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1411]) ).
cnf(c_1413,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1412]) ).
cnf(c_1414,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1413]) ).
cnf(c_1415,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1414]) ).
cnf(c_1416,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1415]) ).
cnf(c_1417,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1416]) ).
cnf(c_1418,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1417]) ).
cnf(c_1419,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1418]) ).
cnf(c_409,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1419]) ).
cnf(c_410,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_1420,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_131,c_410]) ).
cnf(c_1421,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cowlThing(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_132,c_1420]) ).
cnf(c_1422,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cowlThing(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1421]) ).
cnf(c_1423,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cowlThing(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1422]) ).
cnf(c_1424,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1423]) ).
cnf(c_1425,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cowlThing(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1424]) ).
cnf(c_1426,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cowlThing(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1425]) ).
cnf(c_1427,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1426]) ).
cnf(c_1428,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cowlThing(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1427]) ).
cnf(c_1429,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1428]) ).
cnf(c_1430,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cowlThing(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1429]) ).
cnf(c_1431,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1430]) ).
cnf(c_1432,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1431]) ).
cnf(c_1433,negated_conjecture,
( ~ cC38(iV16465)
| ~ cowlThing(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1432]) ).
cnf(c_411,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC68(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_131,c_1433]) ).
cnf(c_1434,plain,
( cC64(A)
| cC68(A)
| ~ cC12(A) ),
inference(resolve,[status(thm)],[c_116,c_120]) ).
cnf(c_1435,plain,
( cC64(iV16459)
| cC68(iV16459) ),
inference(resolve,[status(thm)],[c_1434,c_344]) ).
cnf(c_412,plain,
cC68(iV16459),
inference(resolve,[status(thm)],[c_130,c_1435]) ).
cnf(c_413,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_412,c_411]) ).
cnf(c_414,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_412,c_409]) ).
cnf(c_415,plain,
cC98(iV16440),
inference(resolve,[status(thm)],[c_291,c_294]) ).
cnf(c_418,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_415,c_414]) ).
cnf(c_419,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_415,c_413]) ).
cnf(c_420,plain,
cC82(iV16440),
inference(resolve,[status(thm)],[c_415,c_286]) ).
cnf(c_421,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_420,c_419]) ).
cnf(c_422,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC80(iV16440)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_420,c_418]) ).
cnf(c_425,plain,
cC80(iV16440),
inference(resolve,[status(thm)],[c_420,c_262]) ).
cnf(c_426,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_425,c_422]) ).
cnf(c_427,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC76(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_425,c_421]) ).
cnf(c_458,plain,
cC76(iV16463),
inference(resolve,[status(thm)],[c_295,c_300]) ).
cnf(c_459,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_458,c_427]) ).
cnf(c_460,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC62(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_458,c_426]) ).
cnf(c_461,plain,
cC62(iV16463),
inference(resolve,[status(thm)],[c_458,c_253]) ).
cnf(c_462,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_461,c_460]) ).
cnf(c_463,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC60(iV16463)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_461,c_459]) ).
cnf(c_464,plain,
cC60(iV16463),
inference(resolve,[status(thm)],[c_461,c_240]) ).
cnf(c_465,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_464,c_463]) ).
cnf(c_466,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_464,c_462]) ).
cnf(c_1436,plain,
( cC102(iV16440)
| cC104(iV16439) ),
inference(resolve,[status(thm)],[c_143,c_294]) ).
cnf(c_473,plain,
cC104(iV16439),
inference(resolve,[status(thm)],[c_297,c_1436]) ).
cnf(c_475,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_473,c_466]) ).
cnf(c_476,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_473,c_465]) ).
cnf(c_1437,plain,
( cC100(iV16439)
| cC106(iV16439) ),
inference(resolve,[status(thm)],[c_146,c_473]) ).
cnf(c_478,plain,
cC106(iV16439),
inference(resolve,[status(thm)],[c_293,c_1437]) ).
cnf(c_479,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_478,c_476]) ).
cnf(c_480,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC56(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_478,c_475]) ).
cnf(c_492,plain,
cC56(iV16461),
inference(resolve,[status(thm)],[c_315,c_317]) ).
cnf(c_493,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_492,c_480]) ).
cnf(c_494,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC44(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_492,c_479]) ).
cnf(c_495,plain,
cC44(iV16461),
inference(resolve,[status(thm)],[c_492,c_228]) ).
cnf(c_496,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_495,c_494]) ).
cnf(c_497,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC42(iV16461)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_495,c_493]) ).
cnf(c_498,plain,
cC42(iV16461),
inference(resolve,[status(thm)],[c_495,c_220]) ).
cnf(c_499,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_498,c_497]) ).
cnf(c_500,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC38(iV16460)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_498,c_496]) ).
cnf(c_501,plain,
cC38(iV16460),
inference(resolve,[status(thm)],[c_326,c_327]) ).
cnf(c_502,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_501,c_500]) ).
cnf(c_503,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC38(iV16462)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_501,c_499]) ).
cnf(c_504,plain,
cC38(iV16462),
inference(resolve,[status(thm)],[c_367,c_369]) ).
cnf(c_505,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_504,c_503]) ).
cnf(c_506,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC44(iV16464)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_504,c_502]) ).
cnf(c_514,plain,
cC56(iV16464),
inference(resolve,[status(thm)],[c_382,c_387]) ).
cnf(c_515,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_514,c_506]) ).
cnf(c_516,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC44(iV16464)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_514,c_505]) ).
cnf(c_518,plain,
cC44(iV16464),
inference(resolve,[status(thm)],[c_514,c_228]) ).
cnf(c_519,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_518,c_516]) ).
cnf(c_520,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC42(iV16464)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_518,c_515]) ).
cnf(c_521,plain,
cC42(iV16464),
inference(resolve,[status(thm)],[c_518,c_220]) ).
cnf(c_522,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_521,c_520]) ).
cnf(c_523,negated_conjecture,
( ~ cC38(iV16465)
| ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_521,c_519]) ).
cnf(c_524,plain,
cC38(iV16465),
inference(resolve,[status(thm)],[c_392,c_397]) ).
cnf(c_525,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_524,c_523]) ).
cnf(c_526,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC38(iV16448)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_524,c_522]) ).
cnf(c_1438,plain,
( cC36(iV16457)
| cC38(iV16457) ),
inference(resolve,[status(thm)],[c_212,c_333]) ).
cnf(c_527,plain,
cC38(iV16457),
inference(resolve,[status(thm)],[c_328,c_1438]) ).
cnf(c_1439,plain,
( cC36(iV16448)
| cC38(iV16448) ),
inference(resolve,[status(thm)],[c_212,c_304]) ).
cnf(c_528,plain,
cC38(iV16448),
inference(resolve,[status(thm)],[c_301,c_1439]) ).
cnf(c_1440,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_528,c_526]) ).
cnf(c_529,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_527,c_1440]) ).
cnf(c_1441,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC38(iV16457)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_528,c_525]) ).
cnf(c_530,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC42(iV16455)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_527,c_1441]) ).
cnf(c_1442,plain,
( cC8(iV16460)
| cC42(iV16455) ),
inference(resolve,[status(thm)],[c_218,c_327]) ).
cnf(c_734,plain,
cC42(iV16455),
inference(resolve,[status(thm)],[c_355,c_1442]) ).
cnf(c_741,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_734,c_530]) ).
cnf(c_742,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC56(iV16455)
| ~ cC44(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_734,c_529]) ).
cnf(c_1443,plain,
( cC40(iV16455)
| cC44(iV16455) ),
inference(resolve,[status(thm)],[c_734,c_221]) ).
cnf(c_757,plain,
cC44(iV16455),
inference(resolve,[status(thm)],[c_319,c_1443]) ).
cnf(c_758,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_757,c_742]) ).
cnf(c_759,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_757,c_741]) ).
cnf(c_1444,plain,
( cC54(iV16455)
| cC56(iV16455) ),
inference(resolve,[status(thm)],[c_757,c_230]) ).
cnf(c_760,plain,
cC56(iV16455),
inference(resolve,[status(thm)],[c_324,c_1444]) ).
cnf(c_761,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_760,c_759]) ).
cnf(c_762,negated_conjecture,
( ~ cC34(iV16459)
| ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_760,c_758]) ).
cnf(c_1445,plain,
( cC30(iV16459)
| cC34(iV16459) ),
inference(resolve,[status(thm)],[c_206,c_349]) ).
cnf(c_843,plain,
cC34(iV16459),
inference(resolve,[status(thm)],[c_339,c_1445]) ).
cnf(c_846,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_843,c_762]) ).
cnf(c_847,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC60(iV16453)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_843,c_761]) ).
cnf(c_1446,plain,
( cC12(iV16461)
| cC60(iV16453) ),
inference(resolve,[status(thm)],[c_239,c_317]) ).
cnf(c_954,plain,
cC60(iV16453),
inference(resolve,[status(thm)],[c_364,c_1446]) ).
cnf(c_960,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_954,c_847]) ).
cnf(c_961,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC62(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_954,c_846]) ).
cnf(c_1447,plain,
( cC58(iV16453)
| cC62(iV16453) ),
inference(resolve,[status(thm)],[c_954,c_242]) ).
cnf(c_962,plain,
cC62(iV16453),
inference(resolve,[status(thm)],[c_313,c_1447]) ).
cnf(c_964,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_962,c_961]) ).
cnf(c_965,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC76(iV16453)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_962,c_960]) ).
cnf(c_1448,plain,
( cC74(iV16453)
| cC76(iV16453) ),
inference(resolve,[status(thm)],[c_962,c_254]) ).
cnf(c_966,plain,
cC76(iV16453),
inference(resolve,[status(thm)],[c_314,c_1448]) ).
cnf(c_967,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_966,c_965]) ).
cnf(c_968,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC88(iV16459)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_966,c_964]) ).
cnf(c_1449,plain,
( cC84(iV16459)
| cC88(iV16459) ),
inference(resolve,[status(thm)],[c_272,c_341]) ).
cnf(c_1144,plain,
cC88(iV16459),
inference(resolve,[status(thm)],[c_348,c_1449]) ).
cnf(c_1147,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1144,c_968]) ).
cnf(c_1148,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1144,c_967]) ).
cnf(c_1386,plain,
cC130(iV16439),
inference(resolve,[status(thm)],[c_292,c_289]) ).
cnf(c_1387,plain,
cC108(iV16439),
inference(resolve,[status(thm)],[c_292,c_288]) ).
cnf(c_1450,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC108(iV16439)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1386,c_1148]) ).
cnf(c_1388,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC28(iV16439)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1387,c_1450]) ).
cnf(c_1451,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC108(iV16439)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1386,c_1147]) ).
cnf(c_1389,negated_conjecture,
( ~ cC50(iV16459)
| ~ cC28(iV16439)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1387,c_1451]) ).
cnf(c_1392,plain,
cC28(iV16439),
inference(resolve,[status(thm)],[c_1387,c_147]) ).
cnf(c_1393,negated_conjecture,
( ~ cC50(iV16459)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1392,c_1389]) ).
cnf(c_1394,negated_conjecture,
( ~ cC50(iV16459)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1392,c_1388]) ).
cnf(c_1452,plain,
( cC46(A)
| cC50(A)
| ~ cC4(A) ),
inference(resolve,[status(thm)],[c_107,c_111]) ).
cnf(c_1453,plain,
( cC46(iV16459)
| cC50(iV16459) ),
inference(resolve,[status(thm)],[c_1452,c_338]) ).
cnf(c_1397,plain,
cC50(iV16459),
inference(resolve,[status(thm)],[c_128,c_1453]) ).
cnf(c_1398,negated_conjecture,
( ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1397,c_1394]) ).
cnf(c_1399,negated_conjecture,
( xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_1397,c_1393]) ).
cnf(c_1454,negated_conjecture,
( xsd_integer(sK1)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_1399,c_134]) ).
cnf(c_1403,negated_conjecture,
xsd_integer(sK1),
inference(copy,[status(thm)],[c_1454]) ).
cnf(c_1404,negated_conjecture,
xsd_string(sK1),
inference(resolve,[status(thm)],[c_1403,c_1398]) ).
cnf(c_1455,negated_conjecture,
~ xsd_integer(sK1),
inference(resolve,[status(thm)],[c_1404,c_133]) ).
cnf(c_1405,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1403,c_1455]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS153+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n003.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 19:43:24 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 920345 was started by sandbox2 on n003,
% 0.09/0.36 % Fri Sep 25 19:43:24 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.39
% 0.12/0.39 % From the command line: assign(max_seconds, 300).
% 0.12/0.39
% 0.12/0.39 % SInE: 184 to sos, 16 to usable, of 200 axioms (tolerance 2.00, depth 0 fixpoint).
% 2.16/0.75
% 2.16/0.75 % given #500 (W,wt=11): 771 cC68(iV16463) | cC64(iV16463) | cC42(iV16440). [hyper(115,a,120,c,b,736,b)].
% 2.16/0.75
% 2.16/0.75 % SZS status Theorem for theBenchmark
% 2.16/0.75
% 2.16/0.75 % Proof 1 at 0.11 (+ 0.05) seconds.
% 2.16/0.75 % Length of proof is 191.
% 2.16/0.75 % Level of proof is 35.
% 2.16/0.75 % Maximum clause weight is 611.000.
% 2.16/0.75 % Given clauses 797.
% 2.16/0.75
% 2.16/0.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------