%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KRS159+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 : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:46:10 AM UTC 2026
% Result : Theorem 0.14s 6.00s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 61
% Number of leaves : 97
% Syntax : Number of formulae : 439 ( 116 unt; 0 def)
% Number of atoms : 4014 ( 0 equ)
% Maximal formula atoms : 108 ( 9 avg)
% Number of connectives : 6903 (3328 ~;3330 |; 176 &)
% ( 69 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 56 ( 10 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 93 ( 92 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 8 con; 0-1 aty)
% Number of variables : 260 ( 12 sgn 128 !; 35 ?)
% 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_14,axiom,
! [X] :
( cC108(X)
<=> ( cC106xcomp(X)
& cC98xcomp(X) ) ),
file('theBenchmark.p',axiom_14) ).
fof(axiom_15,axiom,
! [X] :
( cC110(X)
<=> ( cTOP(X)
& cC108(X) ) ),
file('theBenchmark.p',axiom_15) ).
fof(axiom_16,axiom,
! [X] :
( cC112(X)
<=> ( cC90(X)
& cC110(X) ) ),
file('theBenchmark.p',axiom_16) ).
fof(axiom_17,axiom,
! [X] :
( cC114(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_17) ).
fof(axiom_18,axiom,
! [X] :
( cC116(X)
<=> ( cC112(X)
& cC114(X) ) ),
file('theBenchmark.p',axiom_18) ).
fof(axiom_39,axiom,
! [X] :
( cC130(X)
<=> ( cC122xcomp(X)
& cC128xcomp(X) ) ),
file('theBenchmark.p',axiom_39) ).
fof(axiom_40,axiom,
! [X] :
( cC132(X)
<=> ( cTOP(X)
& cC130(X) ) ),
file('theBenchmark.p',axiom_40) ).
fof(axiom_41,axiom,
! [X] :
( cC134(X)
<=> ( cC132(X)
& cC116(X) ) ),
file('theBenchmark.p',axiom_41) ).
fof(axiom_42,axiom,
! [X] :
( cC136(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_42) ).
fof(axiom_43,axiom,
! [X] :
( cC138(X)
<=> ( cC134(X)
& cC136(X) ) ),
file('theBenchmark.p',axiom_43) ).
fof(axiom_44,axiom,
! [X] :
( cC14(X)
<=> ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_44) ).
fof(axiom_63,axiom,
! [X] :
( cC152(X)
<=> ( cC150xcomp(X)
& cC144xcomp(X) ) ),
file('theBenchmark.p',axiom_63) ).
fof(axiom_64,axiom,
! [X] :
( cC154(X)
<=> ( cTOP(X)
& cC152(X) ) ),
file('theBenchmark.p',axiom_64) ).
fof(axiom_65,axiom,
! [X] :
( cC156(X)
<=> ( cC138(X)
& cC154(X) ) ),
file('theBenchmark.p',axiom_65) ).
fof(axiom_66,axiom,
! [X] :
( cC158(X)
<=> ( cC156(X)
& cC22(X) ) ),
file('theBenchmark.p',axiom_66) ).
fof(axiom_67,axiom,
! [X] :
( cC16(X)
<=> ( cC14(X)
& cC10(X) ) ),
file('theBenchmark.p',axiom_67) ).
fof(axiom_80,axiom,
! [X] :
( cC168(X)
<=> ( cC166xcomp(X)
& cC162xcomp(X) ) ),
file('theBenchmark.p',axiom_80) ).
fof(axiom_87,axiom,
! [X] :
( cC174(X)
<=> ( cC168(X)
& cC172xcomp(X) ) ),
file('theBenchmark.p',axiom_87) ).
fof(axiom_96,axiom,
! [X] :
( cC180(X)
<=> ( cC178xcomp(X)
& cC174(X) ) ),
file('theBenchmark.p',axiom_96) ).
fof(axiom_99,axiom,
! [X] :
( cC20(X)
<=> ? [Y] :
( cC18xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_99) ).
fof(axiom_100,axiom,
! [X] :
( cC22(X)
<=> ( cC16(X)
& cC20(X) ) ),
file('theBenchmark.p',axiom_100) ).
fof(axiom_101,axiom,
! [X] :
( cC24(X)
<=> ? [Y0] : ra_Px5(X,Y0) ),
file('theBenchmark.p',axiom_101) ).
fof(axiom_103,axiom,
! [X] :
( cC24xcomp(X)
<=> ~ ? [Y] : ra_Px5(X,Y) ),
file('theBenchmark.p',axiom_103) ).
fof(axiom_105,axiom,
! [X] :
( cC26(X)
<=> ( cC2xcomp(X)
& cC24xcomp(X) ) ),
file('theBenchmark.p',axiom_105) ).
fof(axiom_107,axiom,
! [X] :
( cC28(X)
<=> ? [Y] :
( cC26(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_107) ).
fof(axiom_108,axiom,
! [X] :
( cC28(X)
<=> ? [Y0] : ra_Px9(X,Y0) ),
file('theBenchmark.p',axiom_108) ).
fof(axiom_109,axiom,
! [X] :
( cC28xcomp(X)
<=> ~ ? [Y] : ra_Px9(X,Y) ),
file('theBenchmark.p',axiom_109) ).
fof(axiom_110,axiom,
! [X] :
( cC30(X)
<=> ? [Y0] : ra_Px8(X,Y0) ),
file('theBenchmark.p',axiom_110) ).
fof(axiom_112,axiom,
! [X] :
( cC30xcomp(X)
<=> ~ ? [Y] : ra_Px8(X,Y) ),
file('theBenchmark.p',axiom_112) ).
fof(axiom_114,axiom,
! [X] :
( cC32(X)
<=> ( cC30xcomp(X)
& cC2xcomp(X) ) ),
file('theBenchmark.p',axiom_114) ).
fof(axiom_116,axiom,
! [X] :
( cC34(X)
<=> ~ ? [Y] : ra_Px10(X,Y) ),
file('theBenchmark.p',axiom_116) ).
fof(axiom_117,axiom,
! [X] :
( cC34(X)
<=> ? [Y] :
( cC32(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_117) ).
fof(axiom_118,axiom,
! [X] :
( cC34xcomp(X)
<=> ? [Y0] : ra_Px10(X,Y0) ),
file('theBenchmark.p',axiom_118) ).
fof(axiom_119,axiom,
! [X] :
( cC36(X)
<=> ( cC28xcomp(X)
& cC34xcomp(X) ) ),
file('theBenchmark.p',axiom_119) ).
fof(axiom_120,axiom,
! [X] :
( cC38(X)
<=> ( cTOP(X)
& cC36(X) ) ),
file('theBenchmark.p',axiom_120) ).
fof(axiom_121,axiom,
! [X] :
( cC4(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_121) ).
fof(axiom_122,axiom,
! [X] :
( cC40(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_122) ).
fof(axiom_123,axiom,
! [X] :
( cC42(X)
<=> ( cC38(X)
& cC40(X) ) ),
file('theBenchmark.p',axiom_123) ).
fof(axiom_125,axiom,
! [X] :
( cC44(X)
<=> ? [Y] :
( cC2xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_125) ).
fof(axiom_133,axiom,
! [X] :
( cC50(X)
<=> ? [Y] :
( cC12xcomp(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_133) ).
fof(axiom_142,axiom,
! [X] :
( cC56(X)
<=> ( cC54xcomp(X)
& cC48xcomp(X) ) ),
file('theBenchmark.p',axiom_142) ).
fof(axiom_143,axiom,
! [X] :
( cC58(X)
<=> ( cTOP(X)
& cC56(X) ) ),
file('theBenchmark.p',axiom_143) ).
fof(axiom_146,axiom,
! [X] :
( cC60(X)
<=> ( cC42(X)
& cC58(X) ) ),
file('theBenchmark.p',axiom_146) ).
fof(axiom_147,axiom,
! [X] :
( cC62(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_147) ).
fof(axiom_148,axiom,
! [X] :
( cC64(X)
<=> ( cC62(X)
& cC60(X) ) ),
file('theBenchmark.p',axiom_148) ).
fof(axiom_149,axiom,
! [X] :
( cC66(X)
<=> ? [Y0] : ra_Px21(X,Y0) ),
file('theBenchmark.p',axiom_149) ).
fof(axiom_151,axiom,
! [X] :
( cC66xcomp(X)
<=> ~ ? [Y] : ra_Px21(X,Y) ),
file('theBenchmark.p',axiom_151) ).
fof(axiom_153,axiom,
! [X] :
( cC68(X)
<=> ( cC66xcomp(X)
& cC18xcomp(X) ) ),
file('theBenchmark.p',axiom_153) ).
fof(axiom_155,axiom,
! [X] :
( cC70(X)
<=> ? [Y] :
( cC68(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_155) ).
fof(axiom_156,axiom,
! [X] :
( cC70(X)
<=> ~ ? [Y] : ra_Px25(X,Y) ),
file('theBenchmark.p',axiom_156) ).
fof(axiom_157,axiom,
! [X] :
( cC70xcomp(X)
<=> ? [Y0] : ra_Px25(X,Y0) ),
file('theBenchmark.p',axiom_157) ).
fof(axiom_158,axiom,
! [X] :
( cC72(X)
<=> ? [Y0] : ra_Px24(X,Y0) ),
file('theBenchmark.p',axiom_158) ).
fof(axiom_160,axiom,
! [X] :
( cC72xcomp(X)
<=> ~ ? [Y] : ra_Px24(X,Y) ),
file('theBenchmark.p',axiom_160) ).
fof(axiom_161,axiom,
! [X] :
( cC74(X)
<=> ( cC18xcomp(X)
& cC72xcomp(X) ) ),
file('theBenchmark.p',axiom_161) ).
fof(axiom_164,axiom,
! [X] :
( cC76(X)
<=> ? [Y] :
( cC74(Y)
& rR1(X,Y) ) ),
file('theBenchmark.p',axiom_164) ).
fof(axiom_165,axiom,
! [X] :
( cC76(X)
<=> ? [Y0] : ra_Px26(X,Y0) ),
file('theBenchmark.p',axiom_165) ).
fof(axiom_166,axiom,
! [X] :
( cC76xcomp(X)
<=> ~ ? [Y] : ra_Px26(X,Y) ),
file('theBenchmark.p',axiom_166) ).
fof(axiom_167,axiom,
! [X] :
( cC78(X)
<=> ( cC76xcomp(X)
& cC70xcomp(X) ) ),
file('theBenchmark.p',axiom_167) ).
fof(axiom_169,axiom,
! [X] :
( cC80(X)
<=> ( cTOP(X)
& cC78(X) ) ),
file('theBenchmark.p',axiom_169) ).
fof(axiom_170,axiom,
! [X] :
( cC82(X)
<=> ( cC80(X)
& cC64(X) ) ),
file('theBenchmark.p',axiom_170) ).
fof(axiom_171,axiom,
! [X] :
( cC84(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_171) ).
fof(axiom_172,axiom,
! [X] :
( cC86(X)
<=> ( cC84(X)
& cC82(X) ) ),
file('theBenchmark.p',axiom_172) ).
fof(axiom_173,axiom,
! [X] :
( cC88(X)
<=> cTOP(X) ),
file('theBenchmark.p',axiom_173) ).
fof(axiom_174,axiom,
! [X] :
( cC90(X)
<=> ( cC88(X)
& cC86(X) ) ),
file('theBenchmark.p',axiom_174) ).
fof(axiom_186,axiom,
! [X] :
( cTEST(X)
<=> ( cC180(X)
& cC158(X) ) ),
file('theBenchmark.p',axiom_186) ).
fof(the_axiom,conjecture,
( cowlThing(iV21030)
& cC66(iV21030)
& cC72(iV21030)
& cowlThing(iV21029)
& cC44(iV21029)
& cC50(iV21029)
& cC24(iV21027)
& cowlThing(iV21027)
& cC30(iV21027)
& cC86(iV21026)
& cC156(iV21026)
& cC42(iV21026)
& cC134(iV21026)
& cC4(iV21026)
& cC168(iV21026)
& cC130(iV21026)
& cC88(iV21026)
& cC80(iV21026)
& cC152(iV21026)
& cC14(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC64(iV21026)
& cC112(iV21026)
& cC36(iV21026)
& cC8(iV21026)
& cC62(iV21026)
& cC174(iV21026)
& cC138(iV21026)
& cC38(iV21026)
& cC84(iV21026)
& cC20(iV21026)
& cC114(iV21026)
& cC132(iV21026)
& cC16(iV21026)
& cC78(iV21026)
& cC180(iV21026)
& cC154(iV21026)
& cC60(iV21026)
& cC22(iV21026)
& cC110(iV21026)
& cC158(iV21026)
& cC56(iV21026)
& cC58(iV21026)
& cowlThing(iV21026)
& cC90(iV21026)
& cC10(iV21026)
& cC136(iV21026)
& cC40(iV21026)
& cC108(iV21026)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
file('theBenchmark.p',the_axiom) ).
fof(the_axiom_neg,negated_conjecture,
~ ( cowlThing(iV21030)
& cC66(iV21030)
& cC72(iV21030)
& cowlThing(iV21029)
& cC44(iV21029)
& cC50(iV21029)
& cC24(iV21027)
& cowlThing(iV21027)
& cC30(iV21027)
& cC86(iV21026)
& cC156(iV21026)
& cC42(iV21026)
& cC134(iV21026)
& cC4(iV21026)
& cC168(iV21026)
& cC130(iV21026)
& cC88(iV21026)
& cC80(iV21026)
& cC152(iV21026)
& cC14(iV21026)
& cC82(iV21026)
& cC116(iV21026)
& cC64(iV21026)
& cC112(iV21026)
& cC36(iV21026)
& cC8(iV21026)
& cC62(iV21026)
& cC174(iV21026)
& cC138(iV21026)
& cC38(iV21026)
& cC84(iV21026)
& cC20(iV21026)
& cC114(iV21026)
& cC132(iV21026)
& cC16(iV21026)
& cC78(iV21026)
& cC180(iV21026)
& cC154(iV21026)
& cC60(iV21026)
& cC22(iV21026)
& cC110(iV21026)
& cC158(iV21026)
& cC56(iV21026)
& cC58(iV21026)
& cowlThing(iV21026)
& cC90(iV21026)
& cC10(iV21026)
& cC136(iV21026)
& cC40(iV21026)
& cC108(iV21026)
& ! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) )
& ! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ) ),
inference(assume_negation,[status(cth)],[the_axiom]) ).
cnf(c_249,plain,
cowlThing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_250,plain,
~ cowlNothing(A),
inference(clausify,[status(thm)],[axiom_0]) ).
cnf(c_251,plain,
( ~ xsd_integer(A)
| ~ xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_252,plain,
( xsd_integer(A)
| xsd_string(A) ),
inference(clausify,[status(thm)],[axiom_1]) ).
cnf(c_253,plain,
( cC8(A)
| ~ cC10(A) ),
inference(clausify,[status(thm)],[axiom_2]) ).
cnf(c_279,plain,
( ~ cC106xcomp(A)
| ~ cC98xcomp(A)
| cC108(A) ),
inference(clausify,[status(thm)],[axiom_14]) ).
cnf(c_282,plain,
( ~ cTOP(A)
| ~ cC108(A)
| cC110(A) ),
inference(clausify,[status(thm)],[axiom_15]) ).
cnf(c_285,plain,
( ~ cC90(A)
| ~ cC110(A)
| cC112(A) ),
inference(clausify,[status(thm)],[axiom_16]) ).
cnf(c_287,plain,
( ~ cTOP(A)
| cC114(A) ),
inference(clausify,[status(thm)],[axiom_17]) ).
cnf(c_290,plain,
( ~ cC112(A)
| ~ cC114(A)
| cC116(A) ),
inference(clausify,[status(thm)],[axiom_18]) ).
cnf(c_335,plain,
( ~ cC122xcomp(A)
| ~ cC128xcomp(A)
| cC130(A) ),
inference(clausify,[status(thm)],[axiom_39]) ).
cnf(c_338,plain,
( ~ cTOP(A)
| ~ cC130(A)
| cC132(A) ),
inference(clausify,[status(thm)],[axiom_40]) ).
cnf(c_341,plain,
( ~ cC132(A)
| ~ cC116(A)
| cC134(A) ),
inference(clausify,[status(thm)],[axiom_41]) ).
cnf(c_343,plain,
( ~ cTOP(A)
| cC136(A) ),
inference(clausify,[status(thm)],[axiom_42]) ).
cnf(c_346,plain,
( ~ cC134(A)
| ~ cC136(A)
| cC138(A) ),
inference(clausify,[status(thm)],[axiom_43]) ).
cnf(c_349,plain,
( ~ cC12xcomp(B)
| ~ rR1(A,B)
| cC14(A) ),
inference(clausify,[status(thm)],[axiom_44]) ).
cnf(c_394,plain,
( ~ cC150xcomp(A)
| ~ cC144xcomp(A)
| cC152(A) ),
inference(clausify,[status(thm)],[axiom_63]) ).
cnf(c_397,plain,
( ~ cTOP(A)
| ~ cC152(A)
| cC154(A) ),
inference(clausify,[status(thm)],[axiom_64]) ).
cnf(c_400,plain,
( ~ cC138(A)
| ~ cC154(A)
| cC156(A) ),
inference(clausify,[status(thm)],[axiom_65]) ).
cnf(c_401,plain,
( cC22(A)
| ~ cC158(A) ),
inference(clausify,[status(thm)],[axiom_66]) ).
cnf(c_404,plain,
( cC10(A)
| ~ cC16(A) ),
inference(clausify,[status(thm)],[axiom_67]) ).
cnf(c_437,plain,
( ~ cC166xcomp(A)
| ~ cC162xcomp(A)
| cC168(A) ),
inference(clausify,[status(thm)],[axiom_80]) ).
cnf(c_454,plain,
( ~ cC168(A)
| ~ cC172xcomp(A)
| cC174(A) ),
inference(clausify,[status(thm)],[axiom_87]) ).
cnf(c_471,plain,
( ~ cC178xcomp(A)
| ~ cC174(A)
| cC180(A) ),
inference(clausify,[status(thm)],[axiom_96]) ).
cnf(c_474,plain,
( ~ cC18xcomp(B)
| ~ rR1(A,B)
| cC20(A) ),
inference(clausify,[status(thm)],[axiom_99]) ).
cnf(c_476,plain,
( cC16(A)
| ~ cC22(A) ),
inference(clausify,[status(thm)],[axiom_100]) ).
cnf(c_479,plain,
( ~ ra_Px5(A,B)
| cC24(A) ),
inference(clausify,[status(thm)],[axiom_101]) ).
fof(nnf_96,plain,
! [X] :
( ( ? [Y] : ra_Px5(X,Y)
| cC24xcomp(X) )
& ( ! [X0] : ~ ra_Px5(X,X0)
| ~ cC24xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_103]) ).
fof(sk_axiom_103_sk,plain,
! [X] :
( ( ra_Px5(X,sK0(X))
| cC24xcomp(X) )
& ( ! [X0] : ~ ra_Px5(X,X0)
| ~ cC24xcomp(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(Y,sK0(X))],[nnf_96]) ).
fof(sk_axiom_103,plain,
( ! [VAR_0] :
( ra_Px5(VAR_0,sK0(VAR_0))
| cC24xcomp(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ ra_Px5(VAR_0,VAR_1)
| ~ cC24xcomp(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_103_sk]) ).
cnf(c_484,plain,
( ra_Px5(A,sK0(A))
| cC24xcomp(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_103]) ).
cnf(c_489,plain,
( ~ cC2xcomp(A)
| ~ cC24xcomp(A)
| cC26(A) ),
inference(clausify,[status(thm)],[axiom_105]) ).
cnf(c_494,plain,
( ~ cC26(B)
| ~ rR1(A,B)
| cC28(A) ),
inference(clausify,[status(thm)],[axiom_107]) ).
fof(nnf_101,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px9(X,Y0)
| cC28(X) )
& ( ? [X0] : ra_Px9(X,X0)
| ~ cC28(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_108]) ).
fof(sk_axiom_108_sk,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px9(X,Y0)
| cC28(X) )
& ( ra_Px9(X,sK1(X))
| ~ cC28(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X0,sK1(X))],[nnf_101]) ).
fof(sk_axiom_108,plain,
( ! [VAR_0,VAR_1] :
( ~ ra_Px9(VAR_0,VAR_1)
| cC28(VAR_0) )
& ! [VAR_0] :
( ra_Px9(VAR_0,sK1(VAR_0))
| ~ cC28(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_108_sk]) ).
cnf(c_495,plain,
( ra_Px9(A,sK1(A))
| ~ cC28(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_108]) ).
cnf(c_497,plain,
( ~ ra_Px9(A,B)
| ~ cC28xcomp(A) ),
inference(clausify,[status(thm)],[axiom_109]) ).
cnf(c_500,plain,
( ~ ra_Px8(A,B)
| cC30(A) ),
inference(clausify,[status(thm)],[axiom_110]) ).
fof(nnf_105,plain,
! [X] :
( ( ? [Y] : ra_Px8(X,Y)
| cC30xcomp(X) )
& ( ! [X0] : ~ ra_Px8(X,X0)
| ~ cC30xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_112]) ).
fof(sk_axiom_112_sk,plain,
! [X] :
( ( ra_Px8(X,sK2(X))
| cC30xcomp(X) )
& ( ! [X0] : ~ ra_Px8(X,X0)
| ~ cC30xcomp(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(Y,sK2(X))],[nnf_105]) ).
fof(sk_axiom_112,plain,
( ! [VAR_0] :
( ra_Px8(VAR_0,sK2(VAR_0))
| cC30xcomp(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ ra_Px8(VAR_0,VAR_1)
| ~ cC30xcomp(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_112_sk]) ).
cnf(c_505,plain,
( ra_Px8(A,sK2(A))
| cC30xcomp(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_112]) ).
cnf(c_510,plain,
( ~ cC30xcomp(A)
| ~ cC2xcomp(A)
| cC32(A) ),
inference(clausify,[status(thm)],[axiom_114]) ).
cnf(c_513,plain,
( ~ ra_Px10(A,B)
| ~ cC34(A) ),
inference(clausify,[status(thm)],[axiom_116]) ).
cnf(c_517,plain,
( ~ cC32(B)
| ~ rR1(A,B)
| cC34(A) ),
inference(clausify,[status(thm)],[axiom_117]) ).
fof(nnf_111,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px10(X,Y0)
| cC34xcomp(X) )
& ( ? [X0] : ra_Px10(X,X0)
| ~ cC34xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_118]) ).
fof(sk_axiom_118_sk,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px10(X,Y0)
| cC34xcomp(X) )
& ( ra_Px10(X,sK3(X))
| ~ cC34xcomp(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3(X))],[nnf_111]) ).
fof(sk_axiom_118,plain,
( ! [VAR_0,VAR_1] :
( ~ ra_Px10(VAR_0,VAR_1)
| cC34xcomp(VAR_0) )
& ! [VAR_0] :
( ra_Px10(VAR_0,sK3(VAR_0))
| ~ cC34xcomp(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_118_sk]) ).
cnf(c_518,plain,
( ra_Px10(A,sK3(A))
| ~ cC34xcomp(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_118]) ).
cnf(c_522,plain,
( ~ cC28xcomp(A)
| ~ cC34xcomp(A)
| cC36(A) ),
inference(clausify,[status(thm)],[axiom_119]) ).
cnf(c_525,plain,
( ~ cTOP(A)
| ~ cC36(A)
| cC38(A) ),
inference(clausify,[status(thm)],[axiom_120]) ).
cnf(c_528,plain,
( ~ cC2xcomp(B)
| ~ rR1(A,B)
| cC4(A) ),
inference(clausify,[status(thm)],[axiom_121]) ).
cnf(c_530,plain,
( ~ cTOP(A)
| cC40(A) ),
inference(clausify,[status(thm)],[axiom_122]) ).
cnf(c_533,plain,
( ~ cC38(A)
| ~ cC40(A)
| cC42(A) ),
inference(clausify,[status(thm)],[axiom_123]) ).
cnf(c_538,plain,
( ~ cC2xcomp(B)
| ~ rR1(A,B)
| cC44(A) ),
inference(clausify,[status(thm)],[axiom_125]) ).
cnf(c_557,plain,
( ~ cC12xcomp(B)
| ~ rR1(A,B)
| cC50(A) ),
inference(clausify,[status(thm)],[axiom_133]) ).
cnf(c_578,plain,
( ~ cC54xcomp(A)
| ~ cC48xcomp(A)
| cC56(A) ),
inference(clausify,[status(thm)],[axiom_142]) ).
cnf(c_581,plain,
( ~ cTOP(A)
| ~ cC56(A)
| cC58(A) ),
inference(clausify,[status(thm)],[axiom_143]) ).
cnf(c_584,plain,
( ~ cC42(A)
| ~ cC58(A)
| cC60(A) ),
inference(clausify,[status(thm)],[axiom_146]) ).
cnf(c_586,plain,
( ~ cTOP(A)
| cC62(A) ),
inference(clausify,[status(thm)],[axiom_147]) ).
cnf(c_589,plain,
( ~ cC62(A)
| ~ cC60(A)
| cC64(A) ),
inference(clausify,[status(thm)],[axiom_148]) ).
cnf(c_591,plain,
( ~ ra_Px21(A,B)
| cC66(A) ),
inference(clausify,[status(thm)],[axiom_149]) ).
fof(nnf_142,plain,
! [X] :
( ( ? [Y] : ra_Px21(X,Y)
| cC66xcomp(X) )
& ( ! [X0] : ~ ra_Px21(X,X0)
| ~ cC66xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_151]) ).
fof(sk_axiom_151_sk,plain,
! [X] :
( ( ra_Px21(X,sK4(X))
| cC66xcomp(X) )
& ( ! [X0] : ~ ra_Px21(X,X0)
| ~ cC66xcomp(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(Y,sK4(X))],[nnf_142]) ).
fof(sk_axiom_151,plain,
( ! [VAR_0] :
( ra_Px21(VAR_0,sK4(VAR_0))
| cC66xcomp(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ ra_Px21(VAR_0,VAR_1)
| ~ cC66xcomp(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_151_sk]) ).
cnf(c_596,plain,
( ra_Px21(A,sK4(A))
| cC66xcomp(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_151]) ).
cnf(c_601,plain,
( ~ cC66xcomp(A)
| ~ cC18xcomp(A)
| cC68(A) ),
inference(clausify,[status(thm)],[axiom_153]) ).
cnf(c_606,plain,
( ~ cC68(B)
| ~ rR1(A,B)
| cC70(A) ),
inference(clausify,[status(thm)],[axiom_155]) ).
cnf(c_607,plain,
( ~ ra_Px25(A,B)
| ~ cC70(A) ),
inference(clausify,[status(thm)],[axiom_156]) ).
fof(nnf_148,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px25(X,Y0)
| cC70xcomp(X) )
& ( ? [X0] : ra_Px25(X,X0)
| ~ cC70xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_157]) ).
fof(sk_axiom_157_sk,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px25(X,Y0)
| cC70xcomp(X) )
& ( ra_Px25(X,sK5(X))
| ~ cC70xcomp(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X0,sK5(X))],[nnf_148]) ).
fof(sk_axiom_157,plain,
( ! [VAR_0,VAR_1] :
( ~ ra_Px25(VAR_0,VAR_1)
| cC70xcomp(VAR_0) )
& ! [VAR_0] :
( ra_Px25(VAR_0,sK5(VAR_0))
| ~ cC70xcomp(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_157_sk]) ).
cnf(c_609,plain,
( ra_Px25(A,sK5(A))
| ~ cC70xcomp(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_157]) ).
cnf(c_612,plain,
( ~ ra_Px24(A,B)
| cC72(A) ),
inference(clausify,[status(thm)],[axiom_158]) ).
fof(nnf_151,plain,
! [X] :
( ( ? [Y] : ra_Px24(X,Y)
| cC72xcomp(X) )
& ( ! [X0] : ~ ra_Px24(X,X0)
| ~ cC72xcomp(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_160]) ).
fof(sk_axiom_160_sk,plain,
! [X] :
( ( ra_Px24(X,sK6(X))
| cC72xcomp(X) )
& ( ! [X0] : ~ ra_Px24(X,X0)
| ~ cC72xcomp(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(Y,sK6(X))],[nnf_151]) ).
fof(sk_axiom_160,plain,
( ! [VAR_0] :
( ra_Px24(VAR_0,sK6(VAR_0))
| cC72xcomp(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ ra_Px24(VAR_0,VAR_1)
| ~ cC72xcomp(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_160_sk]) ).
cnf(c_617,plain,
( ra_Px24(A,sK6(A))
| cC72xcomp(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_160]) ).
cnf(c_620,plain,
( ~ cC18xcomp(A)
| ~ cC72xcomp(A)
| cC74(A) ),
inference(clausify,[status(thm)],[axiom_161]) ).
cnf(c_627,plain,
( ~ cC74(B)
| ~ rR1(A,B)
| cC76(A) ),
inference(clausify,[status(thm)],[axiom_164]) ).
fof(nnf_156,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px26(X,Y0)
| cC76(X) )
& ( ? [X0] : ra_Px26(X,X0)
| ~ cC76(X) ) ),
inference(fof_nnf,[status(thm)],[axiom_165]) ).
fof(sk_axiom_165_sk,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px26(X,Y0)
| cC76(X) )
& ( ra_Px26(X,sK7(X))
| ~ cC76(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(X0,sK7(X))],[nnf_156]) ).
fof(sk_axiom_165,plain,
( ! [VAR_0,VAR_1] :
( ~ ra_Px26(VAR_0,VAR_1)
| cC76(VAR_0) )
& ! [VAR_0] :
( ra_Px26(VAR_0,sK7(VAR_0))
| ~ cC76(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_axiom_165_sk]) ).
cnf(c_628,plain,
( ra_Px26(A,sK7(A))
| ~ cC76(A) ),
inference(split_conjunct,[status(thm)],[sk_axiom_165]) ).
cnf(c_630,plain,
( ~ ra_Px26(A,B)
| ~ cC76xcomp(A) ),
inference(clausify,[status(thm)],[axiom_166]) ).
cnf(c_634,plain,
( ~ cC76xcomp(A)
| ~ cC70xcomp(A)
| cC78(A) ),
inference(clausify,[status(thm)],[axiom_167]) ).
cnf(c_640,plain,
( ~ cTOP(A)
| ~ cC78(A)
| cC80(A) ),
inference(clausify,[status(thm)],[axiom_169]) ).
cnf(c_643,plain,
( ~ cC80(A)
| ~ cC64(A)
| cC82(A) ),
inference(clausify,[status(thm)],[axiom_170]) ).
cnf(c_645,plain,
( ~ cTOP(A)
| cC84(A) ),
inference(clausify,[status(thm)],[axiom_171]) ).
cnf(c_648,plain,
( ~ cC84(A)
| ~ cC82(A)
| cC86(A) ),
inference(clausify,[status(thm)],[axiom_172]) ).
cnf(c_650,plain,
( ~ cTOP(A)
| cC88(A) ),
inference(clausify,[status(thm)],[axiom_173]) ).
cnf(c_653,plain,
( ~ cC88(A)
| ~ cC86(A)
| cC90(A) ),
inference(clausify,[status(thm)],[axiom_174]) ).
cnf(c_675,plain,
( cC158(A)
| ~ cTEST(A) ),
inference(clausify,[status(thm)],[axiom_186]) ).
fof(axiom_187,axiom,
cC150xcomp(iV21026),
file('theBenchmark.p',axiom_187) ).
cnf(c_678,plain,
cC150xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_187]) ).
fof(axiom_190,axiom,
cTOP(iV21026),
file('theBenchmark.p',axiom_190) ).
cnf(c_681,plain,
cTOP(iV21026),
inference(clausify,[status(thm)],[axiom_190]) ).
fof(axiom_195,axiom,
cC76xcomp(iV21026),
file('theBenchmark.p',axiom_195) ).
cnf(c_686,plain,
cC76xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_195]) ).
fof(axiom_196,axiom,
cC98xcomp(iV21026),
file('theBenchmark.p',axiom_196) ).
cnf(c_687,plain,
cC98xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_196]) ).
fof(axiom_197,axiom,
cC128xcomp(iV21026),
file('theBenchmark.p',axiom_197) ).
cnf(c_688,plain,
cC128xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_197]) ).
fof(axiom_198,axiom,
cC166xcomp(iV21026),
file('theBenchmark.p',axiom_198) ).
cnf(c_689,plain,
cC166xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_198]) ).
fof(axiom_199,axiom,
cC106xcomp(iV21026),
file('theBenchmark.p',axiom_199) ).
cnf(c_690,plain,
cC106xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_199]) ).
fof(axiom_203,axiom,
cC34xcomp(iV21026),
file('theBenchmark.p',axiom_203) ).
cnf(c_694,plain,
cC34xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_203]) ).
fof(axiom_204,axiom,
cC144xcomp(iV21026),
file('theBenchmark.p',axiom_204) ).
cnf(c_695,plain,
cC144xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_204]) ).
fof(axiom_205,axiom,
cC28xcomp(iV21026),
file('theBenchmark.p',axiom_205) ).
cnf(c_696,plain,
cC28xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_205]) ).
fof(axiom_209,axiom,
cC54xcomp(iV21026),
file('theBenchmark.p',axiom_209) ).
cnf(c_700,plain,
cC54xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_209]) ).
fof(axiom_210,axiom,
cC122xcomp(iV21026),
file('theBenchmark.p',axiom_210) ).
cnf(c_701,plain,
cC122xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_210]) ).
fof(axiom_213,axiom,
cC162xcomp(iV21026),
file('theBenchmark.p',axiom_213) ).
cnf(c_704,plain,
cC162xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_213]) ).
fof(axiom_215,axiom,
cC70xcomp(iV21026),
file('theBenchmark.p',axiom_215) ).
cnf(c_706,plain,
cC70xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_215]) ).
fof(axiom_216,axiom,
cC172xcomp(iV21026),
file('theBenchmark.p',axiom_216) ).
cnf(c_707,plain,
cC172xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_216]) ).
fof(axiom_217,axiom,
cC48xcomp(iV21026),
file('theBenchmark.p',axiom_217) ).
cnf(c_708,plain,
cC48xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_217]) ).
fof(axiom_220,axiom,
cC178xcomp(iV21026),
file('theBenchmark.p',axiom_220) ).
cnf(c_710,plain,
cC178xcomp(iV21026),
inference(clausify,[status(thm)],[axiom_220]) ).
fof(axiom_221,axiom,
cTEST(iV21026),
file('theBenchmark.p',axiom_221) ).
cnf(c_711,plain,
cTEST(iV21026),
inference(clausify,[status(thm)],[axiom_221]) ).
fof(axiom_222,axiom,
rR1(iV21026,iV21030),
file('theBenchmark.p',axiom_222) ).
cnf(c_712,plain,
rR1(iV21026,iV21030),
inference(clausify,[status(thm)],[axiom_222]) ).
fof(axiom_223,axiom,
rR1(iV21026,iV21027),
file('theBenchmark.p',axiom_223) ).
cnf(c_713,plain,
rR1(iV21026,iV21027),
inference(clausify,[status(thm)],[axiom_223]) ).
fof(axiom_225,axiom,
rR1(iV21026,iV21029),
file('theBenchmark.p',axiom_225) ).
cnf(c_714,plain,
rR1(iV21026,iV21029),
inference(clausify,[status(thm)],[axiom_225]) ).
fof(axiom_237,axiom,
cC2xcomp(iV21027),
file('theBenchmark.p',axiom_237) ).
cnf(c_725,plain,
cC2xcomp(iV21027),
inference(clausify,[status(thm)],[axiom_237]) ).
fof(axiom_265,axiom,
cC12xcomp(iV21029),
file('theBenchmark.p',axiom_265) ).
cnf(c_751,plain,
cC12xcomp(iV21029),
inference(clausify,[status(thm)],[axiom_265]) ).
fof(axiom_281,axiom,
rR1(iV21029,iV21034),
file('theBenchmark.p',axiom_281) ).
cnf(c_765,plain,
rR1(iV21029,iV21034),
inference(clausify,[status(thm)],[axiom_281]) ).
fof(axiom_282,axiom,
rR1(iV21029,iV21033),
file('theBenchmark.p',axiom_282) ).
cnf(c_766,plain,
rR1(iV21029,iV21033),
inference(clausify,[status(thm)],[axiom_282]) ).
fof(axiom_293,axiom,
cC18xcomp(iV21030),
file('theBenchmark.p',axiom_293) ).
cnf(c_776,plain,
cC18xcomp(iV21030),
inference(clausify,[status(thm)],[axiom_293]) ).
fof(axiom_319,axiom,
cC12xcomp(iV21033),
file('theBenchmark.p',axiom_319) ).
cnf(c_797,plain,
cC12xcomp(iV21033),
inference(clausify,[status(thm)],[axiom_319]) ).
fof(axiom_325,axiom,
cC2xcomp(iV21034),
file('theBenchmark.p',axiom_325) ).
cnf(c_802,plain,
cC2xcomp(iV21034),
inference(clausify,[status(thm)],[axiom_325]) ).
fof(nnf_216,plain,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(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,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ( ( xsd_integer(sK9)
| ~ xsd_string(sK9) )
& ( ~ xsd_integer(sK9)
| xsd_string(sK9) ) )
| cowlNothing(sK8)
| ~ cowlThing(sK8) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9]),skolemize(X0,sK8),skolemize(X,sK9)],[nnf_216]) ).
fof(sk_the_axiom_neg,plain,
( ( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9)
| ~ xsd_string(sK9)
| cowlNothing(sK8)
| ~ cowlThing(sK8) )
& ( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9)
| cowlNothing(sK8)
| ~ cowlThing(sK8) ) ),
inference(cnf_transformation,[status(thm)],[sk_the_axiom_neg_sk]) ).
cnf(c_816,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9)
| cowlNothing(sK8)
| ~ cowlThing(sK8) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_3979,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9)
| cowlNothing(sK8) ),
inference(resolve,[status(thm)],[c_249,c_816]) ).
cnf(c_3980,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_250,c_3979]) ).
cnf(c_3981,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_249,c_3980]) ).
cnf(c_3982,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_249,c_3981]) ).
cnf(c_3983,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_249,c_3982]) ).
cnf(c_817,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_249,c_3983]) ).
cnf(c_818,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9)
| ~ xsd_string(sK9)
| cowlNothing(sK8)
| ~ cowlThing(sK8) ),
inference(split_conjunct,[status(thm)],[sk_the_axiom_neg]) ).
cnf(c_3984,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9)
| ~ xsd_string(sK9)
| cowlNothing(sK8) ),
inference(resolve,[status(thm)],[c_249,c_818]) ).
cnf(c_3985,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cowlThing(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9)
| ~ xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_250,c_3984]) ).
cnf(c_3986,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cowlThing(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9)
| ~ xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_249,c_3985]) ).
cnf(c_3987,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cowlThing(iV21029)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9)
| ~ xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_249,c_3986]) ).
cnf(c_3988,negated_conjecture,
( ~ cowlThing(iV21030)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9)
| ~ xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_249,c_3987]) ).
cnf(c_819,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9)
| ~ xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_249,c_3988]) ).
cnf(c_3989,plain,
( ~ cC12xcomp(iV21029)
| cC14(iV21026) ),
inference(resolve,[status(thm)],[c_349,c_714]) ).
cnf(c_837,plain,
cC14(iV21026),
inference(resolve,[status(thm)],[c_751,c_3989]) ).
cnf(c_839,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9)
| ~ xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_837,c_819]) ).
cnf(c_840,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC20(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_837,c_817]) ).
cnf(c_3990,plain,
( ~ cC18xcomp(iV21030)
| cC20(iV21026) ),
inference(resolve,[status(thm)],[c_474,c_712]) ).
cnf(c_844,plain,
cC20(iV21026),
inference(resolve,[status(thm)],[c_776,c_3990]) ).
cnf(c_846,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_844,c_840]) ).
cnf(c_847,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC4(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9)
| ~ xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_844,c_839]) ).
cnf(c_3991,plain,
( ~ cC2xcomp(iV21027)
| cC4(iV21026) ),
inference(resolve,[status(thm)],[c_528,c_713]) ).
cnf(c_860,plain,
cC4(iV21026),
inference(resolve,[status(thm)],[c_725,c_3991]) ).
cnf(c_862,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9)
| ~ xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_860,c_847]) ).
cnf(c_863,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_860,c_846]) ).
cnf(c_3992,negated_conjecture,
( xsd_integer(sK9)
| ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_862,c_252]) ).
cnf(c_1102,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC152(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(copy,[status(thm)],[c_3992]) ).
cnf(c_3993,plain,
( ~ cC144xcomp(iV21026)
| cC152(iV21026) ),
inference(resolve,[status(thm)],[c_678,c_394]) ).
cnf(c_1103,plain,
cC152(iV21026),
inference(resolve,[status(thm)],[c_695,c_3993]) ).
cnf(c_1104,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1103,c_1102]) ).
cnf(c_1105,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC154(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1103,c_863]) ).
cnf(c_3994,plain,
( ~ cTOP(iV21026)
| cC154(iV21026) ),
inference(resolve,[status(thm)],[c_1103,c_397]) ).
cnf(c_1106,plain,
cC154(iV21026),
inference(resolve,[status(thm)],[c_681,c_3994]) ).
cnf(c_1107,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1106,c_1105]) ).
cnf(c_1108,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC40(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1106,c_1104]) ).
cnf(c_1109,plain,
( ~ cC138(iV21026)
| cC156(iV21026) ),
inference(resolve,[status(thm)],[c_1106,c_400]) ).
cnf(c_1113,plain,
cC88(iV21026),
inference(resolve,[status(thm)],[c_681,c_650]) ).
cnf(c_1114,plain,
cC84(iV21026),
inference(resolve,[status(thm)],[c_681,c_645]) ).
cnf(c_1115,plain,
( ~ cC78(iV21026)
| cC80(iV21026) ),
inference(resolve,[status(thm)],[c_681,c_640]) ).
cnf(c_1116,plain,
cC62(iV21026),
inference(resolve,[status(thm)],[c_681,c_586]) ).
cnf(c_1117,plain,
( ~ cC56(iV21026)
| cC58(iV21026) ),
inference(resolve,[status(thm)],[c_681,c_581]) ).
cnf(c_1118,plain,
cC40(iV21026),
inference(resolve,[status(thm)],[c_681,c_530]) ).
cnf(c_1119,plain,
( ~ cC36(iV21026)
| cC38(iV21026) ),
inference(resolve,[status(thm)],[c_681,c_525]) ).
cnf(c_1120,plain,
cC136(iV21026),
inference(resolve,[status(thm)],[c_681,c_343]) ).
cnf(c_1121,plain,
( ~ cC130(iV21026)
| cC132(iV21026) ),
inference(resolve,[status(thm)],[c_681,c_338]) ).
cnf(c_1122,plain,
cC114(iV21026),
inference(resolve,[status(thm)],[c_681,c_287]) ).
cnf(c_1123,plain,
( ~ cC108(iV21026)
| cC110(iV21026) ),
inference(resolve,[status(thm)],[c_681,c_282]) ).
cnf(c_3995,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1118,c_1108]) ).
cnf(c_3996,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1120,c_3995]) ).
cnf(c_3997,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1122,c_3996]) ).
cnf(c_3998,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1114,c_3997]) ).
cnf(c_3999,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1116,c_3998]) ).
cnf(c_1126,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1113,c_3999]) ).
cnf(c_4000,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC136(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1118,c_1107]) ).
cnf(c_4001,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC114(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1120,c_4000]) ).
cnf(c_4002,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC84(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1122,c_4001]) ).
cnf(c_4003,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC62(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1114,c_4002]) ).
cnf(c_4004,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC88(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1116,c_4003]) ).
cnf(c_1127,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC78(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1113,c_4004]) ).
cnf(c_1128,plain,
( ~ cC86(iV21026)
| cC90(iV21026) ),
inference(resolve,[status(thm)],[c_1113,c_653]) ).
cnf(c_1129,plain,
( ~ cC82(iV21026)
| cC86(iV21026) ),
inference(resolve,[status(thm)],[c_1114,c_648]) ).
cnf(c_1130,plain,
( ~ cC60(iV21026)
| cC64(iV21026) ),
inference(resolve,[status(thm)],[c_1116,c_589]) ).
cnf(c_1131,plain,
( ~ cC38(iV21026)
| cC42(iV21026) ),
inference(resolve,[status(thm)],[c_1118,c_533]) ).
cnf(c_1148,plain,
( ~ cC134(iV21026)
| cC138(iV21026) ),
inference(resolve,[status(thm)],[c_1120,c_346]) ).
cnf(c_1149,plain,
( ~ cC112(iV21026)
| cC116(iV21026) ),
inference(resolve,[status(thm)],[c_1122,c_290]) ).
cnf(c_4005,plain,
( ~ cC70xcomp(iV21026)
| cC78(iV21026) ),
inference(resolve,[status(thm)],[c_686,c_634]) ).
cnf(c_1157,plain,
cC78(iV21026),
inference(resolve,[status(thm)],[c_706,c_4005]) ).
cnf(c_1158,plain,
~ ra_Px26(iV21026,A),
inference(resolve,[status(thm)],[c_686,c_630]) ).
cnf(c_1161,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1157,c_1127]) ).
cnf(c_1162,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC80(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1157,c_1126]) ).
cnf(c_1163,plain,
cC80(iV21026),
inference(resolve,[status(thm)],[c_1157,c_1115]) ).
cnf(c_1164,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1163,c_1162]) ).
cnf(c_1165,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ cC108(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1163,c_1161]) ).
cnf(c_1168,plain,
( ~ cC64(iV21026)
| cC82(iV21026) ),
inference(resolve,[status(thm)],[c_1163,c_643]) ).
cnf(c_4006,plain,
( ~ cC106xcomp(iV21026)
| cC108(iV21026) ),
inference(resolve,[status(thm)],[c_687,c_279]) ).
cnf(c_1188,plain,
cC108(iV21026),
inference(resolve,[status(thm)],[c_690,c_4006]) ).
cnf(c_1191,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1188,c_1165]) ).
cnf(c_1192,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC110(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1188,c_1164]) ).
cnf(c_1193,plain,
cC110(iV21026),
inference(resolve,[status(thm)],[c_1188,c_1123]) ).
cnf(c_1194,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1193,c_1192]) ).
cnf(c_1195,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC130(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1193,c_1191]) ).
cnf(c_1198,plain,
( ~ cC90(iV21026)
| cC112(iV21026) ),
inference(resolve,[status(thm)],[c_1193,c_285]) ).
cnf(c_4007,plain,
( ~ cC122xcomp(iV21026)
| cC130(iV21026) ),
inference(resolve,[status(thm)],[c_688,c_335]) ).
cnf(c_1200,plain,
cC130(iV21026),
inference(resolve,[status(thm)],[c_701,c_4007]) ).
cnf(c_1202,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1200,c_1195]) ).
cnf(c_1203,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC132(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1200,c_1194]) ).
cnf(c_1204,plain,
cC132(iV21026),
inference(resolve,[status(thm)],[c_1200,c_1121]) ).
cnf(c_1205,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1204,c_1203]) ).
cnf(c_1206,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC168(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1204,c_1202]) ).
cnf(c_1207,plain,
( ~ cC116(iV21026)
| cC134(iV21026) ),
inference(resolve,[status(thm)],[c_1204,c_341]) ).
cnf(c_4008,plain,
( ~ cC162xcomp(iV21026)
| cC168(iV21026) ),
inference(resolve,[status(thm)],[c_689,c_437]) ).
cnf(c_1208,plain,
cC168(iV21026),
inference(resolve,[status(thm)],[c_704,c_4008]) ).
cnf(c_1210,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1208,c_1206]) ).
cnf(c_1211,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC174(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1208,c_1205]) ).
cnf(c_4009,plain,
( ~ cC172xcomp(iV21026)
| cC174(iV21026) ),
inference(resolve,[status(thm)],[c_1208,c_454]) ).
cnf(c_1213,plain,
cC174(iV21026),
inference(resolve,[status(thm)],[c_707,c_4009]) ).
cnf(c_1214,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1213,c_1211]) ).
cnf(c_1215,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC16(iV21026)
| ~ cC180(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1213,c_1210]) ).
cnf(c_4010,plain,
( ~ cC178xcomp(iV21026)
| cC180(iV21026) ),
inference(resolve,[status(thm)],[c_1213,c_471]) ).
cnf(c_1216,plain,
cC180(iV21026),
inference(resolve,[status(thm)],[c_710,c_4010]) ).
cnf(c_1217,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1216,c_1215]) ).
cnf(c_1218,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC36(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1216,c_1214]) ).
cnf(c_4011,plain,
( ~ cC28xcomp(iV21026)
| cC36(iV21026) ),
inference(resolve,[status(thm)],[c_694,c_522]) ).
cnf(c_1221,plain,
cC36(iV21026),
inference(resolve,[status(thm)],[c_696,c_4011]) ).
cnf(c_1222,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1221,c_1218]) ).
cnf(c_1223,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC38(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1221,c_1217]) ).
cnf(c_1224,plain,
cC38(iV21026),
inference(resolve,[status(thm)],[c_1221,c_1119]) ).
cnf(c_1225,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1224,c_1223]) ).
cnf(c_1226,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC42(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1224,c_1222]) ).
cnf(c_1227,plain,
cC42(iV21026),
inference(resolve,[status(thm)],[c_1224,c_1131]) ).
cnf(c_1228,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1227,c_1226]) ).
cnf(c_1229,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC56(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1227,c_1225]) ).
cnf(c_1230,plain,
( ~ cC58(iV21026)
| cC60(iV21026) ),
inference(resolve,[status(thm)],[c_1227,c_584]) ).
cnf(c_1232,plain,
~ ra_Px9(iV21026,A),
inference(resolve,[status(thm)],[c_696,c_497]) ).
cnf(c_4012,plain,
( ~ cC48xcomp(iV21026)
| cC56(iV21026) ),
inference(resolve,[status(thm)],[c_700,c_578]) ).
cnf(c_1233,plain,
cC56(iV21026),
inference(resolve,[status(thm)],[c_708,c_4012]) ).
cnf(c_1235,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1233,c_1229]) ).
cnf(c_1236,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC58(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1233,c_1228]) ).
cnf(c_1237,plain,
cC58(iV21026),
inference(resolve,[status(thm)],[c_1233,c_1117]) ).
cnf(c_1238,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1237,c_1236]) ).
cnf(c_1239,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC60(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1237,c_1235]) ).
cnf(c_1240,plain,
cC60(iV21026),
inference(resolve,[status(thm)],[c_1237,c_1230]) ).
cnf(c_1241,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1240,c_1239]) ).
cnf(c_1242,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC64(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1240,c_1238]) ).
cnf(c_1243,plain,
cC64(iV21026),
inference(resolve,[status(thm)],[c_1240,c_1130]) ).
cnf(c_1244,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1243,c_1242]) ).
cnf(c_1245,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC82(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1243,c_1241]) ).
cnf(c_1246,plain,
cC82(iV21026),
inference(resolve,[status(thm)],[c_1243,c_1168]) ).
cnf(c_1247,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1246,c_1245]) ).
cnf(c_1248,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC86(iV21026)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1246,c_1244]) ).
cnf(c_1249,plain,
cC86(iV21026),
inference(resolve,[status(thm)],[c_1246,c_1129]) ).
cnf(c_1250,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1249,c_1248]) ).
cnf(c_1251,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC90(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1249,c_1247]) ).
cnf(c_1252,plain,
cC90(iV21026),
inference(resolve,[status(thm)],[c_1249,c_1128]) ).
cnf(c_1253,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1252,c_1251]) ).
cnf(c_1254,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC116(iV21026)
| ~ cC112(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1252,c_1250]) ).
cnf(c_1255,plain,
cC112(iV21026),
inference(resolve,[status(thm)],[c_1252,c_1198]) ).
cnf(c_1256,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC116(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1255,c_1254]) ).
cnf(c_1257,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC116(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1255,c_1253]) ).
cnf(c_1258,plain,
cC116(iV21026),
inference(resolve,[status(thm)],[c_1255,c_1149]) ).
cnf(c_1259,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1258,c_1257]) ).
cnf(c_1260,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC134(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1258,c_1256]) ).
cnf(c_1261,plain,
cC134(iV21026),
inference(resolve,[status(thm)],[c_1258,c_1207]) ).
cnf(c_1262,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1261,c_1260]) ).
cnf(c_1263,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC8(iV21026)
| ~ cC138(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1261,c_1259]) ).
cnf(c_1264,plain,
cC138(iV21026),
inference(resolve,[status(thm)],[c_1261,c_1148]) ).
cnf(c_1265,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC8(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1264,c_1263]) ).
cnf(c_1266,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC156(iV21026)
| ~ cC8(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1264,c_1262]) ).
cnf(c_1267,plain,
cC156(iV21026),
inference(resolve,[status(thm)],[c_1264,c_1109]) ).
cnf(c_1268,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC8(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_1267,c_1266]) ).
cnf(c_1269,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC8(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_1267,c_1265]) ).
cnf(c_1631,plain,
( cC24(A)
| cC24xcomp(A) ),
inference(resolve,[status(thm)],[c_484,c_479]) ).
cnf(c_1632,plain,
( cC24(A)
| ~ cC2xcomp(A)
| cC26(A) ),
inference(resolve,[status(thm)],[c_489,c_1631]) ).
cnf(c_1671,plain,
( ~ cC26(iV21027)
| cC28(iV21026) ),
inference(resolve,[status(thm)],[c_494,c_713]) ).
cnf(c_1698,plain,
( cC30(A)
| cC30xcomp(A) ),
inference(resolve,[status(thm)],[c_505,c_500]) ).
cnf(c_1767,plain,
( cC30(A)
| ~ cC2xcomp(A)
| cC32(A) ),
inference(resolve,[status(thm)],[c_510,c_1698]) ).
cnf(c_1914,plain,
( ~ cC32(iV21027)
| cC34(iV21026) ),
inference(resolve,[status(thm)],[c_517,c_713]) ).
cnf(c_1922,plain,
ra_Px10(iV21026,sK3(iV21026)),
inference(resolve,[status(thm)],[c_518,c_694]) ).
cnf(c_1923,plain,
~ cC34(iV21026),
inference(resolve,[status(thm)],[c_1922,c_513]) ).
cnf(c_1926,plain,
~ cC32(iV21027),
inference(resolve,[status(thm)],[c_1923,c_1914]) ).
cnf(c_2203,plain,
( cC66(A)
| cC66xcomp(A) ),
inference(resolve,[status(thm)],[c_596,c_591]) ).
cnf(c_2274,plain,
( cC66(A)
| ~ cC18xcomp(A)
| cC68(A) ),
inference(resolve,[status(thm)],[c_601,c_2203]) ).
cnf(c_2307,plain,
( ~ cC68(iV21030)
| cC70(iV21026) ),
inference(resolve,[status(thm)],[c_606,c_712]) ).
cnf(c_2365,plain,
( cC72(A)
| cC72xcomp(A) ),
inference(resolve,[status(thm)],[c_617,c_612]) ).
cnf(c_2418,plain,
( cC72(A)
| ~ cC18xcomp(A)
| cC74(A) ),
inference(resolve,[status(thm)],[c_620,c_2365]) ).
cnf(c_2455,plain,
( ~ cC74(iV21030)
| cC76(iV21026) ),
inference(resolve,[status(thm)],[c_627,c_712]) ).
cnf(c_2848,plain,
ra_Px25(iV21026,sK5(iV21026)),
inference(resolve,[status(thm)],[c_706,c_609]) ).
cnf(c_2894,plain,
cC158(iV21026),
inference(resolve,[status(thm)],[c_711,c_675]) ).
cnf(c_2895,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC8(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_2894,c_1269]) ).
cnf(c_2896,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC8(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_2894,c_1268]) ).
cnf(c_2897,plain,
cC22(iV21026),
inference(resolve,[status(thm)],[c_2894,c_401]) ).
cnf(c_2898,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC8(iV21026)
| ~ cC16(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_2897,c_2896]) ).
cnf(c_2899,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC8(iV21026)
| ~ cC16(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_2897,c_2895]) ).
cnf(c_2900,plain,
cC16(iV21026),
inference(resolve,[status(thm)],[c_2897,c_476]) ).
cnf(c_2901,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_2900,c_2899]) ).
cnf(c_2902,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_2900,c_2898]) ).
cnf(c_2903,plain,
cC10(iV21026),
inference(resolve,[status(thm)],[c_2900,c_404]) ).
cnf(c_2904,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC8(iV21026)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_2903,c_2902]) ).
cnf(c_2905,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC8(iV21026)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_2903,c_2901]) ).
cnf(c_2906,plain,
cC8(iV21026),
inference(resolve,[status(thm)],[c_2903,c_253]) ).
cnf(c_2907,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_2906,c_2905]) ).
cnf(c_2908,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_2906,c_2904]) ).
cnf(c_4013,plain,
( cC30(iV21027)
| cC32(iV21027) ),
inference(resolve,[status(thm)],[c_725,c_1767]) ).
cnf(c_3006,plain,
cC30(iV21027),
inference(resolve,[status(thm)],[c_1926,c_4013]) ).
cnf(c_3007,plain,
( cC24(iV21027)
| cC26(iV21027) ),
inference(resolve,[status(thm)],[c_725,c_1632]) ).
cnf(c_3015,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_3006,c_2908]) ).
cnf(c_3016,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ cC24(iV21027)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_3006,c_2907]) ).
cnf(c_3020,plain,
( cC28(iV21026)
| cC24(iV21027) ),
inference(resolve,[status(thm)],[c_3007,c_1671]) ).
cnf(c_4014,plain,
( ra_Px9(iV21026,sK1(iV21026))
| cC24(iV21027) ),
inference(resolve,[status(thm)],[c_3020,c_495]) ).
cnf(c_3023,plain,
cC24(iV21027),
inference(resolve,[status(thm)],[c_1232,c_4014]) ).
cnf(c_3024,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_3023,c_3016]) ).
cnf(c_3025,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC44(iV21029)
| ~ cC50(iV21029)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_3023,c_3015]) ).
cnf(c_3102,plain,
~ cC70(iV21026),
inference(resolve,[status(thm)],[c_2848,c_607]) ).
cnf(c_3103,plain,
~ cC68(iV21030),
inference(resolve,[status(thm)],[c_3102,c_2307]) ).
cnf(c_4015,plain,
( ~ cC2xcomp(iV21034)
| cC44(iV21029) ),
inference(resolve,[status(thm)],[c_765,c_538]) ).
cnf(c_3849,plain,
cC44(iV21029),
inference(resolve,[status(thm)],[c_802,c_4015]) ).
cnf(c_3874,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC50(iV21029)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_3849,c_3025]) ).
cnf(c_3875,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ cC50(iV21029)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_3849,c_3024]) ).
cnf(c_4016,plain,
( ~ cC12xcomp(iV21033)
| cC50(iV21029) ),
inference(resolve,[status(thm)],[c_766,c_557]) ).
cnf(c_3895,plain,
cC50(iV21029),
inference(resolve,[status(thm)],[c_797,c_4016]) ).
cnf(c_3919,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_3895,c_3875]) ).
cnf(c_3920,negated_conjecture,
( ~ cC66(iV21030)
| ~ cC72(iV21030)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_3895,c_3874]) ).
cnf(c_3955,plain,
( cC72(iV21030)
| cC74(iV21030) ),
inference(resolve,[status(thm)],[c_776,c_2418]) ).
cnf(c_4017,plain,
( cC66(iV21030)
| cC68(iV21030) ),
inference(resolve,[status(thm)],[c_776,c_2274]) ).
cnf(c_3956,plain,
cC66(iV21030),
inference(resolve,[status(thm)],[c_3103,c_4017]) ).
cnf(c_3962,negated_conjecture,
( ~ cC72(iV21030)
| xsd_integer(sK9) ),
inference(resolve,[status(thm)],[c_3956,c_3920]) ).
cnf(c_3963,negated_conjecture,
( ~ cC72(iV21030)
| ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_3956,c_3919]) ).
cnf(c_3967,plain,
( cC76(iV21026)
| cC72(iV21030) ),
inference(resolve,[status(thm)],[c_3955,c_2455]) ).
cnf(c_4018,plain,
( ra_Px26(iV21026,sK7(iV21026))
| cC72(iV21030) ),
inference(resolve,[status(thm)],[c_3967,c_628]) ).
cnf(c_3970,plain,
cC72(iV21030),
inference(resolve,[status(thm)],[c_1158,c_4018]) ).
cnf(c_3971,negated_conjecture,
( ~ xsd_integer(sK9)
| xsd_string(sK9) ),
inference(resolve,[status(thm)],[c_3970,c_3963]) ).
cnf(c_3972,negated_conjecture,
xsd_integer(sK9),
inference(resolve,[status(thm)],[c_3970,c_3962]) ).
cnf(c_3973,negated_conjecture,
xsd_string(sK9),
inference(resolve,[status(thm)],[c_3972,c_3971]) ).
cnf(c_4019,plain,
~ xsd_string(sK9),
inference(resolve,[status(thm)],[c_3972,c_251]) ).
cnf(c_3978,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3973,c_4019]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS159+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.11/5.57 % Computer : n003.cluster.edu
% 0.11/5.57 % Model : x86_64 x86_64
% 0.11/5.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.57 % Memory : 8046.5625MB
% 0.11/5.57 % OS : Linux 6.8.0-71-generic
% 0.11/5.57 % CPULimit : 300
% 0.11/5.57 % WCLimit : 300
% 0.11/5.57 % DateTime : Fri Sep 25 19:43:44 UTC 2026
% 0.11/5.58 % CPUTime :
% 0.11/5.58 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/5.58 % Process 921485 was started by sandbox on n003,
% 0.11/5.58 % Fri Sep 25 19:43:44 2026
% 0.11/5.58 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/5.63
% 0.14/5.63 % From the command line: assign(max_seconds, 300).
% 0.14/5.63
% 0.14/5.63 % SInE: 322 to sos, 20 to usable, of 342 axioms (tolerance 2.00, depth 0 fixpoint).
% 0.14/6.00
% 0.14/6.00 % given #500 (A,wt=409): 358 -cC142(A) | cC92xcomp(A) # tptp_name(axiom_48) # sine_depth(5). [clausify(45)].
% 0.14/6.00
% 0.14/6.00 % given #1000 (W,wt=17): 1572 cC172xcomp(A) | cC160(A) | -cC6xcomp(f58(A)). [resolve(1556,b,411,b)].
% 0.14/6.00
% 0.14/6.00 % given #1500 (T,wt=19): 2225 cC48(A) | cC56(A) | cC146(A) | -cC100xcomp(f97(A)). [resolve(2199,c,375,b)].
% 0.14/6.00
% 0.14/6.00 % given #2000 (F,wt=14): 2893 -ra_Px83(f85(iV21026),A). [resolve(2748,a,324,a)].
% 0.14/6.00
% 0.14/6.00 % given #2500 (W,wt=7): 3698 -cC92xcomp(iV21035). [back_unit_del(3409),unit_del(a,3697)].
% 0.14/6.00
% 0.14/6.00 % SZS status Theorem for theBenchmark
% 0.14/6.00
% 0.14/6.00 % Proof 1 at 0.25 (+ 0.08) seconds.
% 0.14/6.00 % Length of proof is 342.
% 0.14/6.00 % Level of proof is 46.
% 0.14/6.00 % Maximum clause weight is 312.000.
% 0.14/6.00 % Given clauses 2669.
% 0.14/6.00
% 0.14/6.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------