%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS151+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 0.71s 0.50s
% Output : CNFRefutation 0.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 78
% Syntax : Number of formulae : 353 ( 112 unt; 0 def)
% Number of atoms : 3741 ( 0 equ)
% Maximal formula atoms : 108 ( 10 avg)
% Number of connectives : 6613 (3225 ~;3193 |; 147 &)
% ( 48 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 56 ( 11 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 79 ( 78 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 109 ( 2 sgn 51 !; 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_2,axiom,
! [X] :
( cC10(X)
<=> ( cC4(X)
& cC8(X) ) ),
file('theBenchmark.p',axiom_2) ).
fof(axiom_6,axiom,
! [X] :
( cC108(X)
<=> ( ~ cC98(X)
& ~ cC106(X) ) ),
file('theBenchmark.p',axiom_6) ).
fof(axiom_7,axiom,
! [X] :
( cC110(X)
<=> ( cTOP(X)
& cC108(X) ) ),
file('theBenchmark.p',axiom_7) ).
fof(axiom_8,axiom,
! [X] :
( cC112(X)
<=> ( cC110(X)
& cC90(X) ) ),
file('theBenchmark.p',axiom_8) ).
fof(axiom_9,axiom,
! [X] :
( cC114(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_9) ).
fof(axiom_10,axiom,
! [X] :
( cC116(X)
<=> ( cC112(X)
& cC114(X) ) ),
file('theBenchmark.p',axiom_10) ).
fof(axiom_17,axiom,
! [X] :
( cC130(X)
<=> ( ~ cC128(X)
& ~ cC122(X) ) ),
file('theBenchmark.p',axiom_17) ).
fof(axiom_18,axiom,
! [X] :
( cC132(X)
<=> ( cC130(X)
& cTOP(X) ) ),
file('theBenchmark.p',axiom_18) ).
fof(axiom_19,axiom,
! [X] :
( cC134(X)
<=> ( cC116(X)
& cC132(X) ) ),
file('theBenchmark.p',axiom_19) ).
fof(axiom_20,axiom,
! [X] :
( cC136(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_20) ).
fof(axiom_21,axiom,
! [X] :
( cC138(X)
<=> ( cC134(X)
& cC136(X) ) ),
file('theBenchmark.p',axiom_21) ).
fof(axiom_22,axiom,
! [X] :
( cC14(X)
<=> ? [Y] :
( ~ cC12(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_22) ).
fof(axiom_29,axiom,
! [X] :
( cC152(X)
<=> ( ~ cC144(X)
& ~ cC150(X) ) ),
file('theBenchmark.p',axiom_29) ).
fof(axiom_30,axiom,
! [X] :
( cC154(X)
<=> ( cC152(X)
& cTOP(X) ) ),
file('theBenchmark.p',axiom_30) ).
fof(axiom_32,axiom,
! [X] :
( cC158(X)
<=> ( cC156(X)
& cC22(X) ) ),
file('theBenchmark.p',axiom_32) ).
fof(axiom_33,axiom,
! [X] :
( cC16(X)
<=> ( cC10(X)
& cC14(X) ) ),
file('theBenchmark.p',axiom_33) ).
fof(axiom_38,axiom,
! [X] :
( cC168(X)
<=> ( ~ cC162(X)
& ~ cC166(X) ) ),
file('theBenchmark.p',axiom_38) ).
fof(axiom_41,axiom,
! [X] :
( cC174(X)
<=> ( ~ cC172(X)
& cC168(X) ) ),
file('theBenchmark.p',axiom_41) ).
fof(axiom_44,axiom,
! [X] :
( cC180(X)
<=> ( cC174(X)
& ~ cC178(X) ) ),
file('theBenchmark.p',axiom_44) ).
fof(axiom_45,axiom,
! [X] :
( cC20(X)
<=> ? [Y] :
( ~ cC18(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_45) ).
fof(axiom_46,axiom,
! [X] :
( cC22(X)
<=> ( cC20(X)
& cC16(X) ) ),
file('theBenchmark.p',axiom_46) ).
fof(axiom_48,axiom,
! [X] :
( cC26(X)
<=> ( ~ cC2(X)
& ~ cC24(X) ) ),
file('theBenchmark.p',axiom_48) ).
fof(axiom_51,axiom,
! [X] :
( cC32(X)
<=> ( ~ cC30(X)
& ~ cC2(X) ) ),
file('theBenchmark.p',axiom_51) ).
fof(axiom_53,axiom,
! [X] :
( cC36(X)
<=> ( ~ cC34(X)
& ~ cC28(X) ) ),
file('theBenchmark.p',axiom_53) ).
fof(axiom_54,axiom,
! [X] :
( cC38(X)
<=> ( cTOP(X)
& cC36(X) ) ),
file('theBenchmark.p',axiom_54) ).
fof(axiom_55,axiom,
! [X] :
( cC4(X)
<=> ? [Y] :
( ~ cC2(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_55) ).
fof(axiom_56,axiom,
! [X] :
( cC40(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_56) ).
fof(axiom_57,axiom,
! [X] :
( cC42(X)
<=> ( cC38(X)
& cC40(X) ) ),
file('theBenchmark.p',axiom_57) ).
fof(axiom_59,axiom,
! [X] :
( cC46(X)
<=> ( ~ cC44(X)
& ~ cC12(X) ) ),
file('theBenchmark.p',axiom_59) ).
fof(axiom_62,axiom,
! [X] :
( cC52(X)
<=> ( ~ cC50(X)
& ~ cC12(X) ) ),
file('theBenchmark.p',axiom_62) ).
fof(axiom_64,axiom,
! [X] :
( cC56(X)
<=> ( ~ cC54(X)
& ~ cC48(X) ) ),
file('theBenchmark.p',axiom_64) ).
fof(axiom_65,axiom,
! [X] :
( cC58(X)
<=> ( cTOP(X)
& cC56(X) ) ),
file('theBenchmark.p',axiom_65) ).
fof(axiom_66,axiom,
! [X] :
( cC60(X)
<=> ( cC42(X)
& cC58(X) ) ),
file('theBenchmark.p',axiom_66) ).
fof(axiom_67,axiom,
! [X] :
( cC62(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_67) ).
fof(axiom_68,axiom,
! [X] :
( cC64(X)
<=> ( cC60(X)
& cC62(X) ) ),
file('theBenchmark.p',axiom_68) ).
fof(axiom_70,axiom,
! [X] :
( cC68(X)
<=> ( ~ cC18(X)
& ~ cC66(X) ) ),
file('theBenchmark.p',axiom_70) ).
fof(axiom_73,axiom,
! [X] :
( cC74(X)
<=> ( ~ cC72(X)
& ~ cC18(X) ) ),
file('theBenchmark.p',axiom_73) ).
fof(axiom_75,axiom,
! [X] :
( cC78(X)
<=> ( ~ cC76(X)
& ~ cC70(X) ) ),
file('theBenchmark.p',axiom_75) ).
fof(axiom_77,axiom,
! [X] :
( cC80(X)
<=> ( cC78(X)
& cTOP(X) ) ),
file('theBenchmark.p',axiom_77) ).
fof(axiom_78,axiom,
! [X] :
( cC82(X)
<=> ( cC64(X)
& cC80(X) ) ),
file('theBenchmark.p',axiom_78) ).
fof(axiom_79,axiom,
! [X] :
( cC84(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_79) ).
fof(axiom_80,axiom,
! [X] :
( cC86(X)
<=> ( cC84(X)
& cC82(X) ) ),
file('theBenchmark.p',axiom_80) ).
fof(axiom_81,axiom,
! [X] :
( cC88(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_81) ).
fof(axiom_82,axiom,
! [X] :
( cC90(X)
<=> ( cC86(X)
& cC88(X) ) ),
file('theBenchmark.p',axiom_82) ).
fof(axiom_86,axiom,
! [X] :
( cTEST(X)
<=> ( cC180(X)
& cC158(X) ) ),
file('theBenchmark.p',axiom_86) ).
fof(the_axiom,conjecture,
( cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030)
& cC44(iV21029)
& cC50(iV21029)
& cowlThing(iV21029)
& cC24(iV21027)
& cC30(iV21027)
& cowlThing(iV21027)
& cC90(iV21026)
& cC14(iV21026)
& cC108(iV21026)
& cC4(iV21026)
& cC138(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC110(iV21026)
& cC64(iV21026)
& cC114(iV21026)
& cC180(iV21026)
& cC112(iV21026)
& cC136(iV21026)
& cC8(iV21026)
& cC80(iV21026)
& cC154(iV21026)
& cC62(iV21026)
& cC130(iV21026)
& cC132(iV21026)
& cC40(iV21026)
& cC152(iV21026)
& cC58(iV21026)
& cC78(iV21026)
& cC56(iV21026)
& cC168(iV21026)
& cC22(iV21026)
& cC134(iV21026)
& cC10(iV21026)
& cC158(iV21026)
& cC38(iV21026)
& cC60(iV21026)
& cC156(iV21026)
& cC20(iV21026)
& cC174(iV21026)
& cC86(iV21026)
& cC88(iV21026)
& cC42(iV21026)
& cC36(iV21026)
& cC16(iV21026)
& cC84(iV21026)
& cowlThing(iV21026)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(the_axiom_neg,negated_conjecture,
~ ( cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030)
& cC44(iV21029)
& cC50(iV21029)
& cowlThing(iV21029)
& cC24(iV21027)
& cC30(iV21027)
& cowlThing(iV21027)
& cC90(iV21026)
& cC14(iV21026)
& cC108(iV21026)
& cC4(iV21026)
& cC138(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC110(iV21026)
& cC64(iV21026)
& cC114(iV21026)
& cC180(iV21026)
& cC112(iV21026)
& cC136(iV21026)
& cC8(iV21026)
& cC80(iV21026)
& cC154(iV21026)
& cC62(iV21026)
& cC130(iV21026)
& cC132(iV21026)
& cC40(iV21026)
& cC152(iV21026)
& cC58(iV21026)
& cC78(iV21026)
& cC56(iV21026)
& cC168(iV21026)
& cC22(iV21026)
& cC134(iV21026)
& cC10(iV21026)
& cC158(iV21026)
& cC38(iV21026)
& cC60(iV21026)
& cC156(iV21026)
& cC20(iV21026)
& cC174(iV21026)
& cC86(iV21026)
& cC88(iV21026)
& cC42(iV21026)
& cC36(iV21026)
& cC16(iV21026)
& cC84(iV21026)
& cowlThing(iV21026)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
cnf(c_157,plain,
cowlThing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_158,plain,
~ cowlNothing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_159,plain,
( ~ xsd_integer(A)
| ~ xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_160,plain,
( xsd_integer(A)
| xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_161,plain,
( cC8(A)
| ~ cC10(A) ),
inference(clausify,[status(thm)],[axiom_2]) ).
cnf(c_169,plain,
( cC98(A)
| cC106(A)
| cC108(A) ),
inference(clausify,[status(thm)],[axiom_6]) ).
cnf(c_172,plain,
( ~ cTOP(A)
| ~ cC108(A)
| cC110(A) ),
inference(clausify,[status(thm)],[axiom_7]) ).
cnf(c_175,plain,
( ~ cC110(A)
| ~ cC90(A)
| cC112(A) ),
inference(clausify,[status(thm)],[axiom_8]) ).
cnf(c_177,plain,
( ~ cTOP(A)
| cC114(A) ),
inference(clausify,[status(thm)],[axiom_9]) ).
cnf(c_180,plain,
( ~ cC112(A)
| ~ cC114(A)
| cC116(A) ),
inference(clausify,[status(thm)],[axiom_10]) ).
cnf(c_189,plain,
( cC128(A)
| cC122(A)
| cC130(A) ),
inference(clausify,[status(thm)],[axiom_17]) ).
cnf(c_192,plain,
( ~ cC130(A)
| ~ cTOP(A)
| cC132(A) ),
inference(clausify,[status(thm)],[axiom_18]) ).
cnf(c_195,plain,
( ~ cC116(A)
| ~ cC132(A)
| cC134(A) ),
inference(clausify,[status(thm)],[axiom_19]) ).
cnf(c_197,plain,
( ~ cTOP(A)
| cC136(A) ),
inference(clausify,[status(thm)],[axiom_20]) ).
cnf(c_200,plain,
( ~ cC134(A)
| ~ cC136(A)
| cC138(A) ),
inference(clausify,[status(thm)],[axiom_21]) ).
cnf(c_203,plain,
( cC12(B)
| ~ rR1(A,B)
| cC14(A) ),
inference(clausify,[status(thm)],[axiom_22]) ).
cnf(c_212,plain,
( cC144(A)
| cC150(A)
| cC152(A) ),
inference(clausify,[status(thm)],[axiom_29]) ).
cnf(c_215,plain,
( ~ cC152(A)
| ~ cTOP(A)
| cC154(A) ),
inference(clausify,[status(thm)],[axiom_30]) ).
cnf(c_219,plain,
( cC22(A)
| ~ cC158(A) ),
inference(clausify,[status(thm)],[axiom_32]) ).
cnf(c_220,plain,
( cC156(A)
| ~ cC158(A) ),
inference(clausify,[status(thm)],[axiom_32]) ).
cnf(c_223,plain,
( cC10(A)
| ~ cC16(A) ),
inference(clausify,[status(thm)],[axiom_33]) ).
cnf(c_239,plain,
( cC162(A)
| cC166(A)
| cC168(A) ),
inference(clausify,[status(thm)],[axiom_38]) ).
cnf(c_248,plain,
( cC172(A)
| ~ cC168(A)
| cC174(A) ),
inference(clausify,[status(thm)],[axiom_41]) ).
cnf(c_257,plain,
( ~ cC174(A)
| cC178(A)
| cC180(A) ),
inference(clausify,[status(thm)],[axiom_44]) ).
cnf(c_260,plain,
( cC18(B)
| ~ rR1(A,B)
| cC20(A) ),
inference(clausify,[status(thm)],[axiom_45]) ).
cnf(c_261,plain,
( cC16(A)
| ~ cC22(A) ),
inference(clausify,[status(thm)],[axiom_46]) ).
cnf(c_269,plain,
( cC2(A)
| cC24(A)
| cC26(A) ),
inference(clausify,[status(thm)],[axiom_48]) ).
cnf(c_278,plain,
( cC30(A)
| cC2(A)
| cC32(A) ),
inference(clausify,[status(thm)],[axiom_51]) ).
cnf(c_284,plain,
( cC34(A)
| cC28(A)
| cC36(A) ),
inference(clausify,[status(thm)],[axiom_53]) ).
cnf(c_287,plain,
( ~ cTOP(A)
| ~ cC36(A)
| cC38(A) ),
inference(clausify,[status(thm)],[axiom_54]) ).
cnf(c_290,plain,
( cC2(B)
| ~ rR1(A,B)
| cC4(A) ),
inference(clausify,[status(thm)],[axiom_55]) ).
cnf(c_292,plain,
( ~ cTOP(A)
| cC40(A) ),
inference(clausify,[status(thm)],[axiom_56]) ).
cnf(c_295,plain,
( ~ cC38(A)
| ~ cC40(A)
| cC42(A) ),
inference(clausify,[status(thm)],[axiom_57]) ).
cnf(c_301,plain,
( cC44(A)
| cC12(A)
| cC46(A) ),
inference(clausify,[status(thm)],[axiom_59]) ).
cnf(c_310,plain,
( cC50(A)
| cC12(A)
| cC52(A) ),
inference(clausify,[status(thm)],[axiom_62]) ).
cnf(c_316,plain,
( cC54(A)
| cC48(A)
| cC56(A) ),
inference(clausify,[status(thm)],[axiom_64]) ).
cnf(c_319,plain,
( ~ cTOP(A)
| ~ cC56(A)
| cC58(A) ),
inference(clausify,[status(thm)],[axiom_65]) ).
cnf(c_322,plain,
( ~ cC42(A)
| ~ cC58(A)
| cC60(A) ),
inference(clausify,[status(thm)],[axiom_66]) ).
cnf(c_324,plain,
( ~ cTOP(A)
| cC62(A) ),
inference(clausify,[status(thm)],[axiom_67]) ).
cnf(c_327,plain,
( ~ cC60(A)
| ~ cC62(A)
| cC64(A) ),
inference(clausify,[status(thm)],[axiom_68]) ).
cnf(c_333,plain,
( cC18(A)
| cC66(A)
| cC68(A) ),
inference(clausify,[status(thm)],[axiom_70]) ).
cnf(c_342,plain,
( cC72(A)
| cC18(A)
| cC74(A) ),
inference(clausify,[status(thm)],[axiom_73]) ).
cnf(c_348,plain,
( cC76(A)
| cC70(A)
| cC78(A) ),
inference(clausify,[status(thm)],[axiom_75]) ).
cnf(c_354,plain,
( ~ cC78(A)
| ~ cTOP(A)
| cC80(A) ),
inference(clausify,[status(thm)],[axiom_77]) ).
cnf(c_357,plain,
( ~ cC64(A)
| ~ cC80(A)
| cC82(A) ),
inference(clausify,[status(thm)],[axiom_78]) ).
cnf(c_359,plain,
( ~ cTOP(A)
| cC84(A) ),
inference(clausify,[status(thm)],[axiom_79]) ).
cnf(c_362,plain,
( ~ cC84(A)
| ~ cC82(A)
| cC86(A) ),
inference(clausify,[status(thm)],[axiom_80]) ).
cnf(c_364,plain,
( ~ cTOP(A)
| cC88(A) ),
inference(clausify,[status(thm)],[axiom_81]) ).
cnf(c_367,plain,
( ~ cC86(A)
| ~ cC88(A)
| cC90(A) ),
inference(clausify,[status(thm)],[axiom_82]) ).
cnf(c_371,plain,
( cC158(A)
| ~ cTEST(A) ),
inference(clausify,[status(thm)],[axiom_86]) ).
fof(axiom_88,axiom,
cTOP(iV21026),
file('theBenchmark.p',axiom_88) ).
cnf(c_375,plain,
cTOP(iV21026),
inference(clausify,[status(thm)],[axiom_88]) ).
fof(axiom_89,axiom,
cTEST(iV21026),
file('theBenchmark.p',axiom_89) ).
cnf(c_376,plain,
cTEST(iV21026),
inference(clausify,[status(thm)],[axiom_89]) ).
fof(axiom_91,axiom,
~ cC98(iV21026),
file('theBenchmark.p',axiom_91) ).
cnf(c_378,plain,
~ cC98(iV21026),
inference(clausify,[status(thm)],[axiom_91]) ).
fof(axiom_92,axiom,
~ cC122(iV21026),
file('theBenchmark.p',axiom_92) ).
cnf(c_379,plain,
~ cC122(iV21026),
inference(clausify,[status(thm)],[axiom_92]) ).
fof(axiom_95,axiom,
~ cC34(iV21026),
file('theBenchmark.p',axiom_95) ).
cnf(c_382,plain,
~ cC34(iV21026),
inference(clausify,[status(thm)],[axiom_95]) ).
fof(axiom_96,axiom,
~ cC28(iV21026),
file('theBenchmark.p',axiom_96) ).
cnf(c_383,plain,
~ cC28(iV21026),
inference(clausify,[status(thm)],[axiom_96]) ).
fof(axiom_98,axiom,
~ cC70(iV21026),
file('theBenchmark.p',axiom_98) ).
cnf(c_385,plain,
~ cC70(iV21026),
inference(clausify,[status(thm)],[axiom_98]) ).
fof(axiom_99,axiom,
~ cC178(iV21026),
file('theBenchmark.p',axiom_99) ).
cnf(c_386,plain,
~ cC178(iV21026),
inference(clausify,[status(thm)],[axiom_99]) ).
fof(axiom_100,axiom,
~ cC162(iV21026),
file('theBenchmark.p',axiom_100) ).
cnf(c_387,plain,
~ cC162(iV21026),
inference(clausify,[status(thm)],[axiom_100]) ).
fof(axiom_101,axiom,
~ cC166(iV21026),
file('theBenchmark.p',axiom_101) ).
cnf(c_388,plain,
~ cC166(iV21026),
inference(clausify,[status(thm)],[axiom_101]) ).
fof(axiom_108,axiom,
~ cC150(iV21026),
file('theBenchmark.p',axiom_108) ).
cnf(c_395,plain,
~ cC150(iV21026),
inference(clausify,[status(thm)],[axiom_108]) ).
fof(axiom_109,axiom,
~ cC54(iV21026),
file('theBenchmark.p',axiom_109) ).
cnf(c_396,plain,
~ cC54(iV21026),
inference(clausify,[status(thm)],[axiom_109]) ).
fof(axiom_110,axiom,
~ cC106(iV21026),
file('theBenchmark.p',axiom_110) ).
cnf(c_397,plain,
~ cC106(iV21026),
inference(clausify,[status(thm)],[axiom_110]) ).
fof(axiom_111,axiom,
~ cC144(iV21026),
file('theBenchmark.p',axiom_111) ).
cnf(c_398,plain,
~ cC144(iV21026),
inference(clausify,[status(thm)],[axiom_111]) ).
fof(axiom_112,axiom,
~ cC48(iV21026),
file('theBenchmark.p',axiom_112) ).
cnf(c_399,plain,
~ cC48(iV21026),
inference(clausify,[status(thm)],[axiom_112]) ).
fof(axiom_113,axiom,
~ cC76(iV21026),
file('theBenchmark.p',axiom_113) ).
cnf(c_400,plain,
~ cC76(iV21026),
inference(clausify,[status(thm)],[axiom_113]) ).
fof(axiom_115,axiom,
~ cC128(iV21026),
file('theBenchmark.p',axiom_115) ).
cnf(c_402,plain,
~ cC128(iV21026),
inference(clausify,[status(thm)],[axiom_115]) ).
fof(axiom_116,axiom,
~ cC172(iV21026),
file('theBenchmark.p',axiom_116) ).
cnf(c_403,plain,
~ cC172(iV21026),
inference(clausify,[status(thm)],[axiom_116]) ).
fof(axiom_122,axiom,
rR1(iV21026,iV21030),
file('theBenchmark.p',axiom_122) ).
cnf(c_408,plain,
rR1(iV21026,iV21030),
inference(clausify,[status(thm)],[axiom_122]) ).
fof(axiom_123,axiom,
rR1(iV21026,iV21027),
file('theBenchmark.p',axiom_123) ).
cnf(c_409,plain,
rR1(iV21026,iV21027),
inference(clausify,[status(thm)],[axiom_123]) ).
fof(axiom_125,axiom,
rR1(iV21026,iV21029),
file('theBenchmark.p',axiom_125) ).
cnf(c_410,plain,
rR1(iV21026,iV21029),
inference(clausify,[status(thm)],[axiom_125]) ).
fof(axiom_126,axiom,
~ cC26(iV21027),
file('theBenchmark.p',axiom_126) ).
cnf(c_411,plain,
~ cC26(iV21027),
inference(clausify,[status(thm)],[axiom_126]) ).
fof(axiom_136,axiom,
~ cC32(iV21027),
file('theBenchmark.p',axiom_136) ).
cnf(c_421,plain,
~ cC32(iV21027),
inference(clausify,[status(thm)],[axiom_136]) ).
fof(axiom_150,axiom,
~ cC2(iV21027),
file('theBenchmark.p',axiom_150) ).
cnf(c_435,plain,
~ cC2(iV21027),
inference(clausify,[status(thm)],[axiom_150]) ).
fof(axiom_157,axiom,
~ cC46(iV21029),
file('theBenchmark.p',axiom_157) ).
cnf(c_440,plain,
~ cC46(iV21029),
inference(clausify,[status(thm)],[axiom_157]) ).
fof(axiom_163,axiom,
~ cC12(iV21029),
file('theBenchmark.p',axiom_163) ).
cnf(c_446,plain,
~ cC12(iV21029),
inference(clausify,[status(thm)],[axiom_163]) ).
fof(axiom_168,axiom,
~ cC52(iV21029),
file('theBenchmark.p',axiom_168) ).
cnf(c_451,plain,
~ cC52(iV21029),
inference(clausify,[status(thm)],[axiom_168]) ).
fof(axiom_191,axiom,
~ cC68(iV21030),
file('theBenchmark.p',axiom_191) ).
cnf(c_473,plain,
~ cC68(iV21030),
inference(clausify,[status(thm)],[axiom_191]) ).
fof(axiom_192,axiom,
~ cC74(iV21030),
file('theBenchmark.p',axiom_192) ).
cnf(c_474,plain,
~ cC74(iV21030),
inference(clausify,[status(thm)],[axiom_192]) ).
fof(axiom_202,axiom,
~ cC18(iV21030),
file('theBenchmark.p',axiom_202) ).
cnf(c_484,plain,
~ cC18(iV21030),
inference(clausify,[status(thm)],[axiom_202]) ).
fof(nnf_116,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ? [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,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ( ( 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_116]) ).
fof(sk_the_axiom_neg,plain,
( ( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) )
& ( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ) ),
inference(cnf_transformation,[status(thm)],[sk_the_axiom_neg_sk]) ).
cnf(c_516,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_926,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_157,c_516]) ).
cnf(c_927,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_158,c_926]) ).
cnf(c_928,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_157,c_927]) ).
cnf(c_929,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_157,c_928]) ).
cnf(c_930,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_157,c_929]) ).
cnf(c_517,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_157,c_930]) ).
cnf(c_518,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0)
| ~ cowlThing(sK0) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_931,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1)
| cowlNothing(sK0) ),
inference(resolve,[status(thm)],[c_157,c_518]) ).
cnf(c_932,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ cowlThing(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_158,c_931]) ).
cnf(c_933,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_157,c_932]) ).
cnf(c_934,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cowlThing(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_157,c_933]) ).
cnf(c_935,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_157,c_934]) ).
cnf(c_519,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC14(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_157,c_935]) ).
cnf(c_936,plain,
( cC12(iV21029)
| cC14(iV21026) ),
inference(resolve,[status(thm)],[c_203,c_410]) ).
cnf(c_537,plain,
cC14(iV21026),
inference(resolve,[status(thm)],[c_446,c_936]) ).
cnf(c_539,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_537,c_519]) ).
cnf(c_540,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_537,c_517]) ).
cnf(c_937,plain,
( cC106(iV21026)
| cC108(iV21026) ),
inference(resolve,[status(thm)],[c_378,c_169]) ).
cnf(c_551,plain,
cC108(iV21026),
inference(resolve,[status(thm)],[c_397,c_937]) ).
cnf(c_552,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_551,c_540]) ).
cnf(c_553,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC110(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_551,c_539]) ).
cnf(c_938,plain,
( ~ cTOP(iV21026)
| cC110(iV21026) ),
inference(resolve,[status(thm)],[c_551,c_172]) ).
cnf(c_554,plain,
cC110(iV21026),
inference(resolve,[status(thm)],[c_375,c_938]) ).
cnf(c_555,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_554,c_553]) ).
cnf(c_556,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC152(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_554,c_552]) ).
cnf(c_939,plain,
( cC144(iV21026)
| cC152(iV21026) ),
inference(resolve,[status(thm)],[c_395,c_212]) ).
cnf(c_578,plain,
cC152(iV21026),
inference(resolve,[status(thm)],[c_398,c_939]) ).
cnf(c_579,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_578,c_556]) ).
cnf(c_580,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC154(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_578,c_555]) ).
cnf(c_940,plain,
( ~ cTOP(iV21026)
| cC154(iV21026) ),
inference(resolve,[status(thm)],[c_578,c_215]) ).
cnf(c_581,plain,
cC154(iV21026),
inference(resolve,[status(thm)],[c_375,c_940]) ).
cnf(c_582,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_581,c_580]) ).
cnf(c_583,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC130(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_581,c_579]) ).
cnf(c_941,plain,
( cC122(iV21026)
| cC130(iV21026) ),
inference(resolve,[status(thm)],[c_402,c_189]) ).
cnf(c_591,plain,
cC130(iV21026),
inference(resolve,[status(thm)],[c_379,c_941]) ).
cnf(c_592,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_591,c_583]) ).
cnf(c_593,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC132(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_591,c_582]) ).
cnf(c_942,plain,
( ~ cTOP(iV21026)
| cC132(iV21026) ),
inference(resolve,[status(thm)],[c_591,c_192]) ).
cnf(c_594,plain,
cC132(iV21026),
inference(resolve,[status(thm)],[c_375,c_942]) ).
cnf(c_595,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_594,c_593]) ).
cnf(c_596,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC168(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_594,c_592]) ).
cnf(c_597,plain,
( ~ cC116(iV21026)
| cC134(iV21026) ),
inference(resolve,[status(thm)],[c_594,c_195]) ).
cnf(c_943,plain,
( cC162(iV21026)
| cC168(iV21026) ),
inference(resolve,[status(thm)],[c_239,c_388]) ).
cnf(c_617,plain,
cC168(iV21026),
inference(resolve,[status(thm)],[c_387,c_943]) ).
cnf(c_620,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_617,c_596]) ).
cnf(c_621,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC174(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_617,c_595]) ).
cnf(c_944,plain,
( cC172(iV21026)
| cC174(iV21026) ),
inference(resolve,[status(thm)],[c_248,c_617]) ).
cnf(c_634,plain,
cC174(iV21026),
inference(resolve,[status(thm)],[c_403,c_944]) ).
cnf(c_635,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_634,c_621]) ).
cnf(c_636,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC180(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_634,c_620]) ).
cnf(c_945,plain,
( cC178(iV21026)
| cC180(iV21026) ),
inference(resolve,[status(thm)],[c_257,c_634]) ).
cnf(c_638,plain,
cC180(iV21026),
inference(resolve,[status(thm)],[c_386,c_945]) ).
cnf(c_639,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_638,c_636]) ).
cnf(c_640,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_638,c_635]) ).
cnf(c_946,plain,
( cC2(iV21027)
| cC24(iV21027) ),
inference(resolve,[status(thm)],[c_269,c_411]) ).
cnf(c_644,plain,
cC24(iV21027),
inference(resolve,[status(thm)],[c_435,c_946]) ).
cnf(c_645,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_644,c_640]) ).
cnf(c_646,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC30(iV21027)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_644,c_639]) ).
cnf(c_947,plain,
( cC30(iV21027)
| cC2(iV21027) ),
inference(resolve,[status(thm)],[c_278,c_421]) ).
cnf(c_648,plain,
cC30(iV21027),
inference(resolve,[status(thm)],[c_435,c_947]) ).
cnf(c_649,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_648,c_646]) ).
cnf(c_650,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC20(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_648,c_645]) ).
cnf(c_948,plain,
( cC18(iV21030)
| cC20(iV21026) ),
inference(resolve,[status(thm)],[c_260,c_408]) ).
cnf(c_654,plain,
cC20(iV21026),
inference(resolve,[status(thm)],[c_484,c_948]) ).
cnf(c_655,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_654,c_650]) ).
cnf(c_656,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC36(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_654,c_649]) ).
cnf(c_949,plain,
( cC28(iV21026)
| cC36(iV21026) ),
inference(resolve,[status(thm)],[c_284,c_382]) ).
cnf(c_660,plain,
cC36(iV21026),
inference(resolve,[status(thm)],[c_383,c_949]) ).
cnf(c_661,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_660,c_656]) ).
cnf(c_662,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC38(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_660,c_655]) ).
cnf(c_950,plain,
( ~ cTOP(iV21026)
| cC38(iV21026) ),
inference(resolve,[status(thm)],[c_287,c_660]) ).
cnf(c_663,plain,
cC38(iV21026),
inference(resolve,[status(thm)],[c_375,c_950]) ).
cnf(c_664,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_663,c_662]) ).
cnf(c_665,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_663,c_661]) ).
cnf(c_951,plain,
( cC44(iV21029)
| cC12(iV21029) ),
inference(resolve,[status(thm)],[c_301,c_440]) ).
cnf(c_673,plain,
cC44(iV21029),
inference(resolve,[status(thm)],[c_446,c_951]) ).
cnf(c_674,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_673,c_665]) ).
cnf(c_675,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_673,c_664]) ).
cnf(c_952,plain,
( cC50(iV21029)
| cC12(iV21029) ),
inference(resolve,[status(thm)],[c_310,c_451]) ).
cnf(c_684,plain,
cC50(iV21029),
inference(resolve,[status(thm)],[c_446,c_952]) ).
cnf(c_685,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_684,c_675]) ).
cnf(c_686,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC56(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_684,c_674]) ).
cnf(c_953,plain,
( cC48(iV21026)
| cC56(iV21026) ),
inference(resolve,[status(thm)],[c_316,c_396]) ).
cnf(c_688,plain,
cC56(iV21026),
inference(resolve,[status(thm)],[c_399,c_953]) ).
cnf(c_689,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_688,c_686]) ).
cnf(c_690,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC58(iV21026)
| ~ cC78(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_688,c_685]) ).
cnf(c_954,plain,
( ~ cTOP(iV21026)
| cC58(iV21026) ),
inference(resolve,[status(thm)],[c_319,c_688]) ).
cnf(c_700,plain,
cC58(iV21026),
inference(resolve,[status(thm)],[c_375,c_954]) ).
cnf(c_701,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC78(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_700,c_690]) ).
cnf(c_702,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC90(iV21026)
| ~ cC4(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC78(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_700,c_689]) ).
cnf(c_703,plain,
( ~ cC42(iV21026)
| cC60(iV21026) ),
inference(resolve,[status(thm)],[c_322,c_700]) ).
cnf(c_955,plain,
( cC2(iV21027)
| cC4(iV21026) ),
inference(resolve,[status(thm)],[c_290,c_409]) ).
cnf(c_706,plain,
cC4(iV21026),
inference(resolve,[status(thm)],[c_435,c_955]) ).
cnf(c_708,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC78(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_706,c_702]) ).
cnf(c_709,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC78(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_706,c_701]) ).
cnf(c_956,plain,
( cC18(iV21030)
| cC66(iV21030) ),
inference(resolve,[status(thm)],[c_333,c_473]) ).
cnf(c_733,plain,
cC66(iV21030),
inference(resolve,[status(thm)],[c_484,c_956]) ).
cnf(c_734,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC78(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_733,c_709]) ).
cnf(c_735,negated_conjecture,
( ~ cC72(iV21030)
| ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC78(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_733,c_708]) ).
cnf(c_957,plain,
( cC72(iV21030)
| cC18(iV21030) ),
inference(resolve,[status(thm)],[c_342,c_474]) ).
cnf(c_744,plain,
cC72(iV21030),
inference(resolve,[status(thm)],[c_484,c_957]) ).
cnf(c_745,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC78(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_744,c_735]) ).
cnf(c_746,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC78(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_744,c_734]) ).
cnf(c_958,plain,
( cC70(iV21026)
| cC78(iV21026) ),
inference(resolve,[status(thm)],[c_348,c_400]) ).
cnf(c_749,plain,
cC78(iV21026),
inference(resolve,[status(thm)],[c_385,c_958]) ).
cnf(c_750,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_749,c_746]) ).
cnf(c_751,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC80(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_749,c_745]) ).
cnf(c_959,plain,
( ~ cTOP(iV21026)
| cC80(iV21026) ),
inference(resolve,[status(thm)],[c_354,c_749]) ).
cnf(c_760,plain,
cC80(iV21026),
inference(resolve,[status(thm)],[c_375,c_959]) ).
cnf(c_761,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_760,c_751]) ).
cnf(c_762,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ cC84(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_760,c_750]) ).
cnf(c_763,plain,
( ~ cC64(iV21026)
| cC82(iV21026) ),
inference(resolve,[status(thm)],[c_357,c_760]) ).
cnf(c_821,plain,
cC88(iV21026),
inference(resolve,[status(thm)],[c_375,c_364]) ).
cnf(c_822,plain,
cC84(iV21026),
inference(resolve,[status(thm)],[c_375,c_359]) ).
cnf(c_823,plain,
cC62(iV21026),
inference(resolve,[status(thm)],[c_375,c_324]) ).
cnf(c_824,plain,
cC40(iV21026),
inference(resolve,[status(thm)],[c_375,c_292]) ).
cnf(c_825,plain,
cC136(iV21026),
inference(resolve,[status(thm)],[c_375,c_197]) ).
cnf(c_826,plain,
cC114(iV21026),
inference(resolve,[status(thm)],[c_375,c_177]) ).
cnf(c_960,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_822,c_762]) ).
cnf(c_961,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_821,c_960]) ).
cnf(c_962,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_824,c_961]) ).
cnf(c_963,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_823,c_962]) ).
cnf(c_964,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_825,c_963]) ).
cnf(c_827,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_826,c_964]) ).
cnf(c_965,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC88(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_822,c_761]) ).
cnf(c_966,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC40(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_821,c_965]) ).
cnf(c_967,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_824,c_966]) ).
cnf(c_968,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC136(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_823,c_967]) ).
cnf(c_969,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC114(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_825,c_968]) ).
cnf(c_828,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC158(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_826,c_969]) ).
cnf(c_829,plain,
cC158(iV21026),
inference(resolve,[status(thm)],[c_376,c_371]) ).
cnf(c_830,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_829,c_828]) ).
cnf(c_831,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC42(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_829,c_827]) ).
cnf(c_832,plain,
( ~ cC86(iV21026)
| cC90(iV21026) ),
inference(resolve,[status(thm)],[c_821,c_367]) ).
cnf(c_833,plain,
( ~ cC82(iV21026)
| cC86(iV21026) ),
inference(resolve,[status(thm)],[c_822,c_362]) ).
cnf(c_834,plain,
( ~ cC60(iV21026)
| cC64(iV21026) ),
inference(resolve,[status(thm)],[c_823,c_327]) ).
cnf(c_970,plain,
( ~ cC38(iV21026)
| cC42(iV21026) ),
inference(resolve,[status(thm)],[c_824,c_295]) ).
cnf(c_835,plain,
cC42(iV21026),
inference(resolve,[status(thm)],[c_663,c_970]) ).
cnf(c_836,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_835,c_831]) ).
cnf(c_837,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC60(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_835,c_830]) ).
cnf(c_838,plain,
cC60(iV21026),
inference(resolve,[status(thm)],[c_835,c_703]) ).
cnf(c_839,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_838,c_837]) ).
cnf(c_840,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_838,c_836]) ).
cnf(c_841,plain,
cC64(iV21026),
inference(resolve,[status(thm)],[c_838,c_834]) ).
cnf(c_842,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_841,c_840]) ).
cnf(c_843,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_841,c_839]) ).
cnf(c_844,plain,
cC82(iV21026),
inference(resolve,[status(thm)],[c_841,c_763]) ).
cnf(c_845,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_844,c_843]) ).
cnf(c_846,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_844,c_842]) ).
cnf(c_847,plain,
cC86(iV21026),
inference(resolve,[status(thm)],[c_844,c_833]) ).
cnf(c_848,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC156(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_847,c_846]) ).
cnf(c_849,negated_conjecture,
( ~ cC90(iV21026)
| ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC156(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_847,c_845]) ).
cnf(c_850,plain,
cC90(iV21026),
inference(resolve,[status(thm)],[c_847,c_832]) ).
cnf(c_851,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC156(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_850,c_849]) ).
cnf(c_852,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC156(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_850,c_848]) ).
cnf(c_853,plain,
( ~ cC134(iV21026)
| cC138(iV21026) ),
inference(resolve,[status(thm)],[c_825,c_200]) ).
cnf(c_854,plain,
( ~ cC112(iV21026)
| cC116(iV21026) ),
inference(resolve,[status(thm)],[c_826,c_180]) ).
cnf(c_855,plain,
cC156(iV21026),
inference(resolve,[status(thm)],[c_829,c_220]) ).
cnf(c_856,plain,
cC22(iV21026),
inference(resolve,[status(thm)],[c_829,c_219]) ).
cnf(c_971,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_855,c_852]) ).
cnf(c_857,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_856,c_971]) ).
cnf(c_972,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC22(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_855,c_851]) ).
cnf(c_858,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_856,c_972]) ).
cnf(c_973,plain,
( ~ cC110(iV21026)
| cC112(iV21026) ),
inference(resolve,[status(thm)],[c_850,c_175]) ).
cnf(c_859,plain,
cC112(iV21026),
inference(resolve,[status(thm)],[c_554,c_973]) ).
cnf(c_860,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC8(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_859,c_858]) ).
cnf(c_861,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC116(iV21026)
| ~ cC8(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_859,c_857]) ).
cnf(c_862,plain,
cC116(iV21026),
inference(resolve,[status(thm)],[c_859,c_854]) ).
cnf(c_863,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC8(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_862,c_861]) ).
cnf(c_864,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC8(iV21026)
| ~ cC134(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_862,c_860]) ).
cnf(c_865,plain,
cC134(iV21026),
inference(resolve,[status(thm)],[c_862,c_597]) ).
cnf(c_866,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_865,c_864]) ).
cnf(c_867,negated_conjecture,
( ~ cC138(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_865,c_863]) ).
cnf(c_868,plain,
cC138(iV21026),
inference(resolve,[status(thm)],[c_865,c_853]) ).
cnf(c_869,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_868,c_867]) ).
cnf(c_870,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ cC16(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_868,c_866]) ).
cnf(c_871,plain,
cC16(iV21026),
inference(resolve,[status(thm)],[c_856,c_261]) ).
cnf(c_872,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_871,c_870]) ).
cnf(c_873,negated_conjecture,
( ~ cC8(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_871,c_869]) ).
cnf(c_874,plain,
cC10(iV21026),
inference(resolve,[status(thm)],[c_871,c_223]) ).
cnf(c_875,negated_conjecture,
( ~ cC8(iV21026)
| xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_874,c_873]) ).
cnf(c_876,negated_conjecture,
( ~ cC8(iV21026)
| ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_874,c_872]) ).
cnf(c_877,plain,
cC8(iV21026),
inference(resolve,[status(thm)],[c_874,c_161]) ).
cnf(c_878,negated_conjecture,
( ~ xsd_integer(sK1)
| xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_877,c_876]) ).
cnf(c_879,negated_conjecture,
( xsd_integer(sK1)
| ~ xsd_string(sK1) ),
inference(resolve,[status(thm)],[c_877,c_875]) ).
cnf(c_974,negated_conjecture,
( xsd_integer(sK1)
| xsd_integer(sK1) ),
inference(resolve,[status(thm)],[c_879,c_160]) ).
cnf(c_882,negated_conjecture,
xsd_integer(sK1),
inference(copy,[status(thm)],[c_974]) ).
cnf(c_883,negated_conjecture,
xsd_string(sK1),
inference(resolve,[status(thm)],[c_882,c_878]) ).
cnf(c_975,negated_conjecture,
~ xsd_integer(sK1),
inference(resolve,[status(thm)],[c_883,c_159]) ).
cnf(c_925,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_882,c_975]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS151+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 19:41:34 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 3497789 was started by sandbox on n019,
% 0.10/0.37 % Fri Sep 25 19:41:34 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.40
% 0.10/0.40 % From the command line: assign(max_seconds, 300).
% 0.10/0.40
% 0.10/0.40 % SInE: 226 to sos, 16 to usable, of 242 axioms (tolerance 2.00, depth 0 fixpoint).
% 0.71/0.50
% 0.71/0.50 % SZS status Theorem for theBenchmark
% 0.71/0.50
% 0.71/0.50 % Proof 1 at 0.07 (+ 0.01) seconds.
% 0.71/0.50 % Length of proof is 269.
% 0.71/0.50 % Level of proof is 45.
% 0.71/0.50 % Maximum clause weight is 107.000.
% 0.71/0.50 % Given clauses 496.
% 0.71/0.50
% 0.71/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------