%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KRS161+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n018.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 : Fri Sep 25 01:54:18 PM UTC 2026
% Result : Theorem 6.71s 1.65s
% Output : CNFRefutation 6.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 80
% Syntax : Number of formulae : 480 ( 165 unt; 0 def)
% Number of atoms : 2358 ( 0 equ)
% Maximal formula atoms : 51 ( 4 avg)
% Number of connectives : 3474 (1596 ~;1576 |; 265 &)
% ( 34 <=>; 2 =>; 0 <=; 1 <~>)
% Maximal formula depth : 50 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 53 ( 52 usr; 1 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 15 con; 0-1 aty)
% Number of variables : 339 ( 0 sgn 299 !; 40 ?; 109 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_0) ).
fof(f2,axiom,
! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
fof(f12,axiom,
! [X0] :
( cC106(X0)
<=> ( cC100xcomp(X0)
& cC104(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_11) ).
fof(f13,axiom,
! [X0] :
( cC108(X0)
<=> ( cC106(X0)
& cC28(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_12) ).
fof(f53,axiom,
! [X0] :
( cC34(X0)
<=> ( cC32xcomp(X0)
& cC30xcomp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_52) ).
fof(f58,axiom,
! [X0] :
( cC38(X0)
<=> ( cC36xcomp(X0)
& cTOP(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_57) ).
fof(f66,axiom,
! [X0] :
( cC42(X0)
<=> ? [X1] :
( cC8xcomp(X1)
& rR1(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_65) ).
fof(f67,axiom,
! [X0] :
( cC44(X0)
<=> ( cC42(X0)
& cC40xcomp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_66) ).
fof(f74,axiom,
! [X0] :
( cC50(X0)
<=> ( cC48xcomp(X0)
& cC46xcomp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_73) ).
fof(f83,axiom,
! [X0] :
( cC56(X0)
<=> ( cC44(X0)
& cC54xcomp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_82) ).
fof(f84,axiom,
! [X0] :
( cC56(X0)
<=> ? [X1] : ra_Px17(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_83) ).
fof(f85,axiom,
! [X0] :
( cC56xcomp(X0)
<=> ~ ? [X1] : ra_Px17(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_84) ).
fof(f86,axiom,
! [X0] :
( cC58(X0)
<=> ? [X1] :
( cC56xcomp(X1)
& rR1(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_85) ).
fof(f87,axiom,
! [X0] :
( cC58(X0)
<=> ~ ? [X1] : ra_Px19(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_86) ).
fof(f88,axiom,
! [X0] :
( cC58xcomp(X0)
<=> ? [X1] : ra_Px19(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_87) ).
fof(f92,axiom,
! [X0] :
( cC60(X0)
<=> ? [X1] :
( cC12xcomp(X1)
& rR1(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_91) ).
fof(f93,axiom,
! [X0] :
( cC62(X0)
<=> ( cC58xcomp(X0)
& cC60(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_92) ).
fof(f101,axiom,
! [X0] :
( cC68(X0)
<=> ( cC66xcomp(X0)
& cC64xcomp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_100) ).
fof(f112,axiom,
! [X0] :
( cC76(X0)
<=> ? [X1] : ra_Px26(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_111) ).
fof(f113,axiom,
! [X0] :
( cC76(X0)
<=> ( cC62(X0)
& cC74xcomp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_112) ).
fof(f114,axiom,
! [X0] :
( cC76xcomp(X0)
<=> ~ ? [X1] : ra_Px26(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_113) ).
fof(f115,axiom,
! [X0] :
( cC78(X0)
<=> ? [X1] :
( cC76xcomp(X1)
& rR1(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_114) ).
fof(f116,axiom,
! [X0] :
( cC78(X0)
<=> ~ ? [X1] : ra_Px28(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_115) ).
fof(f117,axiom,
! [X0] :
( cC78xcomp(X0)
<=> ? [X1] : ra_Px28(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_116) ).
fof(f121,axiom,
! [X0] :
( cC82(X0)
<=> ( cC78xcomp(X0)
& cC80(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_120) ).
fof(f129,axiom,
! [X0] :
( cC88(X0)
<=> ( cC86xcomp(X0)
& cC84xcomp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_128) ).
fof(f144,axiom,
! [X0] :
( cC98(X0)
<=> ( cC82(X0)
& cC96xcomp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_143) ).
fof(f146,axiom,
! [X0] :
( cTEST(X0)
<=> ( cC130(X0)
& cC108(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_145) ).
fof(f147,axiom,
! [X0] :
( rR1(iV16439,X0)
=> cC98(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_146) ).
fof(f148,axiom,
cowlThing(iV16439),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_147) ).
fof(f150,axiom,
cTEST(iV16439),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_149) ).
fof(f151,axiom,
rR1(iV16439,iV16440),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_150) ).
fof(f154,axiom,
cowlThing(iV16440),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_153) ).
fof(f159,axiom,
cC78xcomp(iV16440),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_158) ).
fof(f160,axiom,
rR1(iV16440,iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_159) ).
fof(f163,axiom,
cowlThing(iV16448),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_162) ).
fof(f164,axiom,
cTOP(iV16448),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_163) ).
fof(f169,axiom,
cC36xcomp(iV16448),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_168) ).
fof(f175,axiom,
cC74xcomp(iV16453),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_174) ).
fof(f176,axiom,
cowlThing(iV16453),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_175) ).
fof(f182,axiom,
cC58xcomp(iV16453),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_181) ).
fof(f183,axiom,
rR1(iV16453,iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_182) ).
fof(f185,axiom,
cowlThing(iV16455),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_184) ).
fof(f186,axiom,
cC40xcomp(iV16455),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_185) ).
fof(f191,axiom,
cC54xcomp(iV16455),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_190) ).
fof(f194,axiom,
rR1(iV16455,iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_193) ).
fof(f196,axiom,
cowlThing(iV16457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_195) ).
fof(f198,axiom,
cTOP(iV16457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_197) ).
fof(f202,axiom,
cC36xcomp(iV16457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_201) ).
fof(f206,axiom,
cowlThing(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_205) ).
fof(f210,axiom,
cC30xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_209) ).
fof(f211,axiom,
cC84xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_210) ).
fof(f213,axiom,
cC46xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_212) ).
fof(f214,axiom,
cC64xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_213) ).
fof(f216,axiom,
cC86xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_215) ).
fof(f217,axiom,
cC32xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_216) ).
fof(f218,axiom,
cC48xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_217) ).
fof(f222,axiom,
cC66xcomp(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_221) ).
fof(f224,axiom,
cowlThing(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_223) ).
fof(f226,axiom,
cTOP(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_225) ).
fof(f228,axiom,
cC8xcomp(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_227) ).
fof(f229,axiom,
cC36xcomp(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_228) ).
fof(f234,axiom,
cowlThing(iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_233) ).
fof(f235,axiom,
cC40xcomp(iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_234) ).
fof(f238,axiom,
cC12xcomp(iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_237) ).
fof(f241,axiom,
cC54xcomp(iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_240) ).
fof(f247,axiom,
cowlThing(iV16462),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_246) ).
fof(f248,axiom,
cTOP(iV16462),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_247) ).
fof(f253,axiom,
cC36xcomp(iV16462),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_252) ).
fof(f256,axiom,
cC74xcomp(iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_255) ).
fof(f257,axiom,
cowlThing(iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_256) ).
fof(f263,axiom,
cC58xcomp(iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_262) ).
fof(f264,axiom,
rR1(iV16463,iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_263) ).
fof(f265,axiom,
cowlThing(iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_264) ).
fof(f267,axiom,
cC40xcomp(iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_266) ).
fof(f271,axiom,
cC54xcomp(iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_270) ).
fof(f277,axiom,
cowlThing(iV16465),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_276) ).
fof(f278,axiom,
cTOP(iV16465),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_277) ).
fof(f283,axiom,
cC36xcomp(iV16465),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_282) ).
fof(f287,conjecture,
( cowlThing(iV16465)
& cC38(iV16465)
& cowlThing(iV16464)
& cC44(iV16464)
& cC42(iV16464)
& cC56(iV16464)
& cC60(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC76(iV16463)
& cowlThing(iV16462)
& cC38(iV16462)
& cowlThing(iV16461)
& cC44(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16460)
& cC38(iV16460)
& cowlThing(iV16459)
& cC68(iV16459)
& cC34(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cowlThing(iV16457)
& cC38(iV16457)
& cowlThing(iV16455)
& cC42(iV16455)
& cC44(iV16455)
& cC56(iV16455)
& cC60(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC76(iV16453)
& cowlThing(iV16448)
& cC38(iV16448)
& cowlThing(iV16440)
& cC82(iV16440)
& cC80(iV16440)
& cC98(iV16440)
& cowlThing(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& cC104(iV16439)
& cC108(iV16439)
& cC130(iV16439)
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(f288,negated_conjecture,
~ ( cowlThing(iV16465)
& cC38(iV16465)
& cowlThing(iV16464)
& cC44(iV16464)
& cC42(iV16464)
& cC56(iV16464)
& cC60(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC76(iV16463)
& cowlThing(iV16462)
& cC38(iV16462)
& cowlThing(iV16461)
& cC44(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16460)
& cC38(iV16460)
& cowlThing(iV16459)
& cC68(iV16459)
& cC34(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cowlThing(iV16457)
& cC38(iV16457)
& cowlThing(iV16455)
& cC42(iV16455)
& cC44(iV16455)
& cC56(iV16455)
& cC60(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC76(iV16453)
& cowlThing(iV16448)
& cC38(iV16448)
& cowlThing(iV16440)
& cC82(iV16440)
& cC80(iV16440)
& cC98(iV16440)
& cowlThing(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& cC104(iV16439)
& cC108(iV16439)
& cC130(iV16439)
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
inference(negated_conjecture,[status(cth)],[f287]) ).
fof(f289,plain,
~ ( cowlThing(iV16465)
& cC38(iV16465)
& cowlThing(iV16464)
& cC44(iV16464)
& cC42(iV16464)
& cC56(iV16464)
& cC60(iV16463)
& cowlThing(iV16463)
& cC62(iV16463)
& cC76(iV16463)
& cowlThing(iV16462)
& cC38(iV16462)
& cowlThing(iV16461)
& cC44(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16460)
& cC38(iV16460)
& cowlThing(iV16459)
& cC68(iV16459)
& cC34(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cowlThing(iV16457)
& cC38(iV16457)
& cowlThing(iV16455)
& cC42(iV16455)
& cC44(iV16455)
& cC56(iV16455)
& cC60(iV16453)
& cowlThing(iV16453)
& cC62(iV16453)
& cC76(iV16453)
& cowlThing(iV16448)
& cC38(iV16448)
& cowlThing(iV16440)
& cC82(iV16440)
& cC80(iV16440)
& cC98(iV16440)
& cowlThing(iV16439)
& cC28(iV16439)
& cC106(iV16439)
& cC104(iV16439)
& cC108(iV16439)
& cC130(iV16439)
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
inference(rectify,[],[f288]) ).
fof(f290,plain,
! [X0] :
( cTEST(X0)
=> ( cC130(X0)
& cC108(X0) ) ),
inference(unused_predicate_definition_removal,[],[f146]) ).
fof(f325,plain,
! [X0] :
( cC56xcomp(X0)
<=> ! [X1] : ~ ra_Px17(X0,X1) ),
inference(ennf_transformation,[],[f85]) ).
fof(f326,plain,
! [X0] :
( cC58(X0)
<=> ! [X1] : ~ ra_Px19(X0,X1) ),
inference(ennf_transformation,[],[f87]) ).
fof(f335,plain,
! [X0] :
( cC76xcomp(X0)
<=> ! [X1] : ~ ra_Px26(X0,X1) ),
inference(ennf_transformation,[],[f114]) ).
fof(f336,plain,
! [X0] :
( cC78(X0)
<=> ! [X1] : ~ ra_Px28(X0,X1) ),
inference(ennf_transformation,[],[f116]) ).
fof(f346,plain,
! [X0] :
( ~ cTEST(X0)
| ( cC130(X0)
& cC108(X0) ) ),
inference(ennf_transformation,[],[f290]) ).
fof(f347,plain,
! [X0] :
( ~ rR1(iV16439,X0)
| cC98(X0) ),
inference(ennf_transformation,[],[f147]) ).
fof(f388,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [X1] :
( xsd_string(X1)
<~> ~ xsd_integer(X1) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(ennf_transformation,[],[f289]) ).
fof(f389,plain,
! [X0] :
( ( ~ xsd_string(X0)
| ~ xsd_integer(X0) )
& ( xsd_integer(X0)
| xsd_string(X0) ) ),
inference(nnf_transformation,[],[f2]) ).
fof(f411,plain,
! [X0] :
( ( ~ cC106(X0)
| ( cC100xcomp(X0)
& cC104(X0) ) )
& ( ~ cC100xcomp(X0)
| ~ cC104(X0)
| cC106(X0) ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f412,plain,
! [X0] :
( ( ~ cC106(X0)
| ( cC100xcomp(X0)
& cC104(X0) ) )
& ( ~ cC100xcomp(X0)
| ~ cC104(X0)
| cC106(X0) ) ),
inference(flattening,[],[f411]) ).
fof(f413,plain,
! [X0] :
( ( ~ cC108(X0)
| ( cC106(X0)
& cC28(X0) ) )
& ( ~ cC106(X0)
| ~ cC28(X0)
| cC108(X0) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f414,plain,
! [X0] :
( ( ~ cC108(X0)
| ( cC106(X0)
& cC28(X0) ) )
& ( ~ cC106(X0)
| ~ cC28(X0)
| cC108(X0) ) ),
inference(flattening,[],[f413]) ).
fof(f515,plain,
! [X0] :
( ( ~ cC34(X0)
| ( cC32xcomp(X0)
& cC30xcomp(X0) ) )
& ( ~ cC32xcomp(X0)
| ~ cC30xcomp(X0)
| cC34(X0) ) ),
inference(nnf_transformation,[],[f53]) ).
fof(f516,plain,
! [X0] :
( ( ~ cC34(X0)
| ( cC32xcomp(X0)
& cC30xcomp(X0) ) )
& ( ~ cC32xcomp(X0)
| ~ cC30xcomp(X0)
| cC34(X0) ) ),
inference(flattening,[],[f515]) ).
fof(f529,plain,
! [X0] :
( ( ~ cC38(X0)
| ( cC36xcomp(X0)
& cTOP(X0) ) )
& ( ~ cC36xcomp(X0)
| ~ cTOP(X0)
| cC38(X0) ) ),
inference(nnf_transformation,[],[f58]) ).
fof(f530,plain,
! [X0] :
( ( ~ cC38(X0)
| ( cC36xcomp(X0)
& cTOP(X0) ) )
& ( ~ cC36xcomp(X0)
| ~ cTOP(X0)
| cC38(X0) ) ),
inference(flattening,[],[f529]) ).
fof(f552,plain,
! [X0] :
( ( ~ cC42(X0)
| ? [X1] :
( cC8xcomp(X1)
& rR1(X0,X1) ) )
& ( ! [X1] :
( ~ cC8xcomp(X1)
| ~ rR1(X0,X1) )
| cC42(X0) ) ),
inference(nnf_transformation,[],[f66]) ).
fof(f553,plain,
! [X0] :
( ( ~ cC42(X0)
| ? [X2] :
( cC8xcomp(X2)
& rR1(X0,X2) ) )
& ( ! [X1] :
( ~ cC8xcomp(X1)
| ~ rR1(X0,X1) )
| cC42(X0) ) ),
inference(rectify,[],[f552]) ).
fof(f554,plain,
! [X0] :
( ( ~ cC42(X0)
| ( cC8xcomp(sK46(X0))
& rR1(X0,sK46(X0)) ) )
& ( ! [X1] :
( ~ cC8xcomp(X1)
| ~ rR1(X0,X1) )
| cC42(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46]),skolemize(X2,sK46(X0))],[f553]) ).
fof(f555,plain,
! [X0] :
( ( ~ cC44(X0)
| ( cC42(X0)
& cC40xcomp(X0) ) )
& ( ~ cC42(X0)
| ~ cC40xcomp(X0)
| cC44(X0) ) ),
inference(nnf_transformation,[],[f67]) ).
fof(f556,plain,
! [X0] :
( ( ~ cC44(X0)
| ( cC42(X0)
& cC40xcomp(X0) ) )
& ( ~ cC42(X0)
| ~ cC40xcomp(X0)
| cC44(X0) ) ),
inference(flattening,[],[f555]) ).
fof(f573,plain,
! [X0] :
( ( ~ cC50(X0)
| ( cC48xcomp(X0)
& cC46xcomp(X0) ) )
& ( ~ cC48xcomp(X0)
| ~ cC46xcomp(X0)
| cC50(X0) ) ),
inference(nnf_transformation,[],[f74]) ).
fof(f574,plain,
! [X0] :
( ( ~ cC50(X0)
| ( cC48xcomp(X0)
& cC46xcomp(X0) ) )
& ( ~ cC48xcomp(X0)
| ~ cC46xcomp(X0)
| cC50(X0) ) ),
inference(flattening,[],[f573]) ).
fof(f597,plain,
! [X0] :
( ( ~ cC56(X0)
| ( cC44(X0)
& cC54xcomp(X0) ) )
& ( ~ cC44(X0)
| ~ cC54xcomp(X0)
| cC56(X0) ) ),
inference(nnf_transformation,[],[f83]) ).
fof(f598,plain,
! [X0] :
( ( ~ cC56(X0)
| ( cC44(X0)
& cC54xcomp(X0) ) )
& ( ~ cC44(X0)
| ~ cC54xcomp(X0)
| cC56(X0) ) ),
inference(flattening,[],[f597]) ).
fof(f599,plain,
! [X0] :
( ( ~ cC56(X0)
| ? [X1] : ra_Px17(X0,X1) )
& ( ! [X1] : ~ ra_Px17(X0,X1)
| cC56(X0) ) ),
inference(nnf_transformation,[],[f84]) ).
fof(f600,plain,
! [X0] :
( ( ~ cC56(X0)
| ? [X2] : ra_Px17(X0,X2) )
& ( ! [X1] : ~ ra_Px17(X0,X1)
| cC56(X0) ) ),
inference(rectify,[],[f599]) ).
fof(f601,plain,
! [X0] :
( ( ~ cC56(X0)
| ra_Px17(X0,sK59(X0)) )
& ( ! [X1] : ~ ra_Px17(X0,X1)
| cC56(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59]),skolemize(X2,sK59(X0))],[f600]) ).
fof(f602,plain,
! [X0] :
( ( ~ cC56xcomp(X0)
| ! [X1] : ~ ra_Px17(X0,X1) )
& ( ? [X1] : ra_Px17(X0,X1)
| cC56xcomp(X0) ) ),
inference(nnf_transformation,[],[f325]) ).
fof(f603,plain,
! [X0] :
( ( ~ cC56xcomp(X0)
| ! [X2] : ~ ra_Px17(X0,X2) )
& ( ? [X1] : ra_Px17(X0,X1)
| cC56xcomp(X0) ) ),
inference(rectify,[],[f602]) ).
fof(f604,plain,
! [X0] :
( ( ~ cC56xcomp(X0)
| ! [X2] : ~ ra_Px17(X0,X2) )
& ( ra_Px17(X0,sK60(X0))
| cC56xcomp(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60]),skolemize(X1,sK60(X0))],[f603]) ).
fof(f605,plain,
! [X0] :
( ( ~ cC58(X0)
| ? [X1] :
( cC56xcomp(X1)
& rR1(X0,X1) ) )
& ( ! [X1] :
( ~ cC56xcomp(X1)
| ~ rR1(X0,X1) )
| cC58(X0) ) ),
inference(nnf_transformation,[],[f86]) ).
fof(f606,plain,
! [X0] :
( ( ~ cC58(X0)
| ? [X2] :
( cC56xcomp(X2)
& rR1(X0,X2) ) )
& ( ! [X1] :
( ~ cC56xcomp(X1)
| ~ rR1(X0,X1) )
| cC58(X0) ) ),
inference(rectify,[],[f605]) ).
fof(f607,plain,
! [X0] :
( ( ~ cC58(X0)
| ( cC56xcomp(sK61(X0))
& rR1(X0,sK61(X0)) ) )
& ( ! [X1] :
( ~ cC56xcomp(X1)
| ~ rR1(X0,X1) )
| cC58(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK61]),skolemize(X2,sK61(X0))],[f606]) ).
fof(f608,plain,
! [X0] :
( ( ~ cC58(X0)
| ! [X1] : ~ ra_Px19(X0,X1) )
& ( ? [X1] : ra_Px19(X0,X1)
| cC58(X0) ) ),
inference(nnf_transformation,[],[f326]) ).
fof(f609,plain,
! [X0] :
( ( ~ cC58(X0)
| ! [X2] : ~ ra_Px19(X0,X2) )
& ( ? [X1] : ra_Px19(X0,X1)
| cC58(X0) ) ),
inference(rectify,[],[f608]) ).
fof(f610,plain,
! [X0] :
( ( ~ cC58(X0)
| ! [X2] : ~ ra_Px19(X0,X2) )
& ( ra_Px19(X0,sK62(X0))
| cC58(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62]),skolemize(X1,sK62(X0))],[f609]) ).
fof(f611,plain,
! [X0] :
( ( ~ cC58xcomp(X0)
| ? [X1] : ra_Px19(X0,X1) )
& ( ! [X1] : ~ ra_Px19(X0,X1)
| cC58xcomp(X0) ) ),
inference(nnf_transformation,[],[f88]) ).
fof(f612,plain,
! [X0] :
( ( ~ cC58xcomp(X0)
| ? [X2] : ra_Px19(X0,X2) )
& ( ! [X1] : ~ ra_Px19(X0,X1)
| cC58xcomp(X0) ) ),
inference(rectify,[],[f611]) ).
fof(f613,plain,
! [X0] :
( ( ~ cC58xcomp(X0)
| ra_Px19(X0,sK63(X0)) )
& ( ! [X1] : ~ ra_Px19(X0,X1)
| cC58xcomp(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK63]),skolemize(X2,sK63(X0))],[f612]) ).
fof(f619,plain,
! [X0] :
( ( ~ cC60(X0)
| ? [X1] :
( cC12xcomp(X1)
& rR1(X0,X1) ) )
& ( ! [X1] :
( ~ cC12xcomp(X1)
| ~ rR1(X0,X1) )
| cC60(X0) ) ),
inference(nnf_transformation,[],[f92]) ).
fof(f620,plain,
! [X0] :
( ( ~ cC60(X0)
| ? [X2] :
( cC12xcomp(X2)
& rR1(X0,X2) ) )
& ( ! [X1] :
( ~ cC12xcomp(X1)
| ~ rR1(X0,X1) )
| cC60(X0) ) ),
inference(rectify,[],[f619]) ).
fof(f621,plain,
! [X0] :
( ( ~ cC60(X0)
| ( cC12xcomp(sK65(X0))
& rR1(X0,sK65(X0)) ) )
& ( ! [X1] :
( ~ cC12xcomp(X1)
| ~ rR1(X0,X1) )
| cC60(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65]),skolemize(X2,sK65(X0))],[f620]) ).
fof(f622,plain,
! [X0] :
( ( ~ cC62(X0)
| ( cC58xcomp(X0)
& cC60(X0) ) )
& ( ~ cC58xcomp(X0)
| ~ cC60(X0)
| cC62(X0) ) ),
inference(nnf_transformation,[],[f93]) ).
fof(f623,plain,
! [X0] :
( ( ~ cC62(X0)
| ( cC58xcomp(X0)
& cC60(X0) ) )
& ( ~ cC58xcomp(X0)
| ~ cC60(X0)
| cC62(X0) ) ),
inference(flattening,[],[f622]) ).
fof(f643,plain,
! [X0] :
( ( ~ cC68(X0)
| ( cC66xcomp(X0)
& cC64xcomp(X0) ) )
& ( ~ cC66xcomp(X0)
| ~ cC64xcomp(X0)
| cC68(X0) ) ),
inference(nnf_transformation,[],[f101]) ).
fof(f644,plain,
! [X0] :
( ( ~ cC68(X0)
| ( cC66xcomp(X0)
& cC64xcomp(X0) ) )
& ( ~ cC66xcomp(X0)
| ~ cC64xcomp(X0)
| cC68(X0) ) ),
inference(flattening,[],[f643]) ).
fof(f670,plain,
! [X0] :
( ( ~ cC76(X0)
| ? [X1] : ra_Px26(X0,X1) )
& ( ! [X1] : ~ ra_Px26(X0,X1)
| cC76(X0) ) ),
inference(nnf_transformation,[],[f112]) ).
fof(f671,plain,
! [X0] :
( ( ~ cC76(X0)
| ? [X2] : ra_Px26(X0,X2) )
& ( ! [X1] : ~ ra_Px26(X0,X1)
| cC76(X0) ) ),
inference(rectify,[],[f670]) ).
fof(f672,plain,
! [X0] :
( ( ~ cC76(X0)
| ra_Px26(X0,sK80(X0)) )
& ( ! [X1] : ~ ra_Px26(X0,X1)
| cC76(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK80]),skolemize(X2,sK80(X0))],[f671]) ).
fof(f673,plain,
! [X0] :
( ( ~ cC76(X0)
| ( cC62(X0)
& cC74xcomp(X0) ) )
& ( ~ cC62(X0)
| ~ cC74xcomp(X0)
| cC76(X0) ) ),
inference(nnf_transformation,[],[f113]) ).
fof(f674,plain,
! [X0] :
( ( ~ cC76(X0)
| ( cC62(X0)
& cC74xcomp(X0) ) )
& ( ~ cC62(X0)
| ~ cC74xcomp(X0)
| cC76(X0) ) ),
inference(flattening,[],[f673]) ).
fof(f675,plain,
! [X0] :
( ( ~ cC76xcomp(X0)
| ! [X1] : ~ ra_Px26(X0,X1) )
& ( ? [X1] : ra_Px26(X0,X1)
| cC76xcomp(X0) ) ),
inference(nnf_transformation,[],[f335]) ).
fof(f676,plain,
! [X0] :
( ( ~ cC76xcomp(X0)
| ! [X2] : ~ ra_Px26(X0,X2) )
& ( ? [X1] : ra_Px26(X0,X1)
| cC76xcomp(X0) ) ),
inference(rectify,[],[f675]) ).
fof(f677,plain,
! [X0] :
( ( ~ cC76xcomp(X0)
| ! [X2] : ~ ra_Px26(X0,X2) )
& ( ra_Px26(X0,sK81(X0))
| cC76xcomp(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK81]),skolemize(X1,sK81(X0))],[f676]) ).
fof(f678,plain,
! [X0] :
( ( ~ cC78(X0)
| ? [X1] :
( cC76xcomp(X1)
& rR1(X0,X1) ) )
& ( ! [X1] :
( ~ cC76xcomp(X1)
| ~ rR1(X0,X1) )
| cC78(X0) ) ),
inference(nnf_transformation,[],[f115]) ).
fof(f679,plain,
! [X0] :
( ( ~ cC78(X0)
| ? [X2] :
( cC76xcomp(X2)
& rR1(X0,X2) ) )
& ( ! [X1] :
( ~ cC76xcomp(X1)
| ~ rR1(X0,X1) )
| cC78(X0) ) ),
inference(rectify,[],[f678]) ).
fof(f680,plain,
! [X0] :
( ( ~ cC78(X0)
| ( cC76xcomp(sK82(X0))
& rR1(X0,sK82(X0)) ) )
& ( ! [X1] :
( ~ cC76xcomp(X1)
| ~ rR1(X0,X1) )
| cC78(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK82]),skolemize(X2,sK82(X0))],[f679]) ).
fof(f681,plain,
! [X0] :
( ( ~ cC78(X0)
| ! [X1] : ~ ra_Px28(X0,X1) )
& ( ? [X1] : ra_Px28(X0,X1)
| cC78(X0) ) ),
inference(nnf_transformation,[],[f336]) ).
fof(f682,plain,
! [X0] :
( ( ~ cC78(X0)
| ! [X2] : ~ ra_Px28(X0,X2) )
& ( ? [X1] : ra_Px28(X0,X1)
| cC78(X0) ) ),
inference(rectify,[],[f681]) ).
fof(f683,plain,
! [X0] :
( ( ~ cC78(X0)
| ! [X2] : ~ ra_Px28(X0,X2) )
& ( ra_Px28(X0,sK83(X0))
| cC78(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK83]),skolemize(X1,sK83(X0))],[f682]) ).
fof(f684,plain,
! [X0] :
( ( ~ cC78xcomp(X0)
| ? [X1] : ra_Px28(X0,X1) )
& ( ! [X1] : ~ ra_Px28(X0,X1)
| cC78xcomp(X0) ) ),
inference(nnf_transformation,[],[f117]) ).
fof(f685,plain,
! [X0] :
( ( ~ cC78xcomp(X0)
| ? [X2] : ra_Px28(X0,X2) )
& ( ! [X1] : ~ ra_Px28(X0,X1)
| cC78xcomp(X0) ) ),
inference(rectify,[],[f684]) ).
fof(f686,plain,
! [X0] :
( ( ~ cC78xcomp(X0)
| ra_Px28(X0,sK84(X0)) )
& ( ! [X1] : ~ ra_Px28(X0,X1)
| cC78xcomp(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK84]),skolemize(X2,sK84(X0))],[f685]) ).
fof(f696,plain,
! [X0] :
( ( ~ cC82(X0)
| ( cC78xcomp(X0)
& cC80(X0) ) )
& ( ~ cC78xcomp(X0)
| ~ cC80(X0)
| cC82(X0) ) ),
inference(nnf_transformation,[],[f121]) ).
fof(f697,plain,
! [X0] :
( ( ~ cC82(X0)
| ( cC78xcomp(X0)
& cC80(X0) ) )
& ( ~ cC78xcomp(X0)
| ~ cC80(X0)
| cC82(X0) ) ),
inference(flattening,[],[f696]) ).
fof(f717,plain,
! [X0] :
( ( ~ cC88(X0)
| ( cC86xcomp(X0)
& cC84xcomp(X0) ) )
& ( ~ cC86xcomp(X0)
| ~ cC84xcomp(X0)
| cC88(X0) ) ),
inference(nnf_transformation,[],[f129]) ).
fof(f718,plain,
! [X0] :
( ( ~ cC88(X0)
| ( cC86xcomp(X0)
& cC84xcomp(X0) ) )
& ( ~ cC86xcomp(X0)
| ~ cC84xcomp(X0)
| cC88(X0) ) ),
inference(flattening,[],[f717]) ).
fof(f752,plain,
! [X0] :
( ( ~ cC98(X0)
| ( cC82(X0)
& cC96xcomp(X0) ) )
& ( ~ cC82(X0)
| ~ cC96xcomp(X0)
| cC98(X0) ) ),
inference(nnf_transformation,[],[f144]) ).
fof(f753,plain,
! [X0] :
( ( ~ cC98(X0)
| ( cC82(X0)
& cC96xcomp(X0) ) )
& ( ~ cC82(X0)
| ~ cC96xcomp(X0)
| cC98(X0) ) ),
inference(flattening,[],[f752]) ).
fof(f757,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ? [X1] :
( ( xsd_string(X1)
| ~ xsd_integer(X1) )
& ( ~ xsd_string(X1)
| xsd_integer(X1) ) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(nnf_transformation,[],[f388]) ).
fof(f758,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ( ( xsd_string(sK106)
| ~ xsd_integer(sK106) )
& ( ~ xsd_string(sK106)
| xsd_integer(sK106) ) )
| cowlNothing(sK105)
| ~ cowlThing(sK105) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK105,sK106]),skolemize(X0,sK105),skolemize(X1,sK106)],[f757]) ).
fof(f759,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f760,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f761,plain,
! [X0] :
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(cnf_transformation,[],[f389]) ).
fof(f762,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f389]) ).
fof(f782,plain,
! [X0] :
( ~ cC106(X0)
| cC104(X0) ),
inference(cnf_transformation,[],[f412]) ).
fof(f784,plain,
! [X0] :
( ~ cC108(X0)
| cC106(X0) ),
inference(cnf_transformation,[],[f414]) ).
fof(f785,plain,
! [X0] :
( ~ cC108(X0)
| cC28(X0) ),
inference(cnf_transformation,[],[f414]) ).
fof(f880,plain,
! [X0] :
( ~ cC32xcomp(X0)
| ~ cC30xcomp(X0)
| cC34(X0) ),
inference(cnf_transformation,[],[f516]) ).
fof(f892,plain,
! [X0] :
( ~ cC36xcomp(X0)
| ~ cTOP(X0)
| cC38(X0) ),
inference(cnf_transformation,[],[f530]) ).
fof(f910,plain,
! [X0,X1] :
( ~ cC8xcomp(X1)
| ~ rR1(X0,X1)
| cC42(X0) ),
inference(cnf_transformation,[],[f554]) ).
fof(f911,plain,
! [X0] :
( ~ cC44(X0)
| cC42(X0) ),
inference(cnf_transformation,[],[f556]) ).
fof(f913,plain,
! [X0] :
( ~ cC42(X0)
| ~ cC40xcomp(X0)
| cC44(X0) ),
inference(cnf_transformation,[],[f556]) ).
fof(f930,plain,
! [X0] :
( ~ cC48xcomp(X0)
| ~ cC46xcomp(X0)
| cC50(X0) ),
inference(cnf_transformation,[],[f574]) ).
fof(f948,plain,
! [X0] :
( ~ cC56(X0)
| cC44(X0) ),
inference(cnf_transformation,[],[f598]) ).
fof(f950,plain,
! [X0] :
( ~ cC44(X0)
| ~ cC54xcomp(X0)
| cC56(X0) ),
inference(cnf_transformation,[],[f598]) ).
fof(f952,plain,
! [X0,X1] :
( ~ ra_Px17(X0,X1)
| cC56(X0) ),
inference(cnf_transformation,[],[f601]) ).
fof(f954,plain,
! [X0] :
( ra_Px17(X0,sK60(X0))
| cC56xcomp(X0) ),
inference(cnf_transformation,[],[f604]) ).
fof(f957,plain,
! [X0,X1] :
( ~ cC56xcomp(X1)
| ~ rR1(X0,X1)
| cC58(X0) ),
inference(cnf_transformation,[],[f607]) ).
fof(f958,plain,
! [X2,X0] :
( ~ cC58(X0)
| ~ ra_Px19(X0,X2) ),
inference(cnf_transformation,[],[f610]) ).
fof(f960,plain,
! [X0] :
( ~ cC58xcomp(X0)
| ra_Px19(X0,sK63(X0)) ),
inference(cnf_transformation,[],[f613]) ).
fof(f970,plain,
! [X0,X1] :
( ~ cC12xcomp(X1)
| ~ rR1(X0,X1)
| cC60(X0) ),
inference(cnf_transformation,[],[f621]) ).
fof(f972,plain,
! [X0] :
( ~ cC62(X0)
| cC60(X0) ),
inference(cnf_transformation,[],[f623]) ).
fof(f973,plain,
! [X0] :
( ~ cC58xcomp(X0)
| ~ cC60(X0)
| cC62(X0) ),
inference(cnf_transformation,[],[f623]) ).
fof(f992,plain,
! [X0] :
( ~ cC66xcomp(X0)
| ~ cC64xcomp(X0)
| cC68(X0) ),
inference(cnf_transformation,[],[f644]) ).
fof(f1015,plain,
! [X0,X1] :
( ~ ra_Px26(X0,X1)
| cC76(X0) ),
inference(cnf_transformation,[],[f672]) ).
fof(f1016,plain,
! [X0] :
( ~ cC76(X0)
| cC62(X0) ),
inference(cnf_transformation,[],[f674]) ).
fof(f1018,plain,
! [X0] :
( ~ cC62(X0)
| ~ cC74xcomp(X0)
| cC76(X0) ),
inference(cnf_transformation,[],[f674]) ).
fof(f1020,plain,
! [X0] :
( ra_Px26(X0,sK81(X0))
| cC76xcomp(X0) ),
inference(cnf_transformation,[],[f677]) ).
fof(f1023,plain,
! [X0,X1] :
( ~ cC76xcomp(X1)
| ~ rR1(X0,X1)
| cC78(X0) ),
inference(cnf_transformation,[],[f680]) ).
fof(f1024,plain,
! [X2,X0] :
( ~ cC78(X0)
| ~ ra_Px28(X0,X2) ),
inference(cnf_transformation,[],[f683]) ).
fof(f1026,plain,
! [X0] :
( ~ cC78xcomp(X0)
| ra_Px28(X0,sK84(X0)) ),
inference(cnf_transformation,[],[f686]) ).
fof(f1036,plain,
! [X0] :
( ~ cC82(X0)
| cC80(X0) ),
inference(cnf_transformation,[],[f697]) ).
fof(f1056,plain,
! [X0] :
( ~ cC86xcomp(X0)
| ~ cC84xcomp(X0)
| cC88(X0) ),
inference(cnf_transformation,[],[f718]) ).
fof(f1086,plain,
! [X0] :
( ~ cC98(X0)
| cC82(X0) ),
inference(cnf_transformation,[],[f753]) ).
fof(f1091,plain,
! [X0] :
( ~ cTEST(X0)
| cC130(X0) ),
inference(cnf_transformation,[],[f346]) ).
fof(f1092,plain,
! [X0] :
( ~ cTEST(X0)
| cC108(X0) ),
inference(cnf_transformation,[],[f346]) ).
fof(f1093,plain,
! [X0] :
( ~ rR1(iV16439,X0)
| cC98(X0) ),
inference(cnf_transformation,[],[f347]) ).
fof(f1094,plain,
cowlThing(iV16439),
inference(cnf_transformation,[],[f148]) ).
fof(f1096,plain,
cTEST(iV16439),
inference(cnf_transformation,[],[f150]) ).
fof(f1097,plain,
rR1(iV16439,iV16440),
inference(cnf_transformation,[],[f151]) ).
fof(f1100,plain,
cowlThing(iV16440),
inference(cnf_transformation,[],[f154]) ).
fof(f1105,plain,
cC78xcomp(iV16440),
inference(cnf_transformation,[],[f159]) ).
fof(f1106,plain,
rR1(iV16440,iV16463),
inference(cnf_transformation,[],[f160]) ).
fof(f1109,plain,
cowlThing(iV16448),
inference(cnf_transformation,[],[f163]) ).
fof(f1110,plain,
cTOP(iV16448),
inference(cnf_transformation,[],[f164]) ).
fof(f1115,plain,
cC36xcomp(iV16448),
inference(cnf_transformation,[],[f169]) ).
fof(f1121,plain,
cC74xcomp(iV16453),
inference(cnf_transformation,[],[f175]) ).
fof(f1122,plain,
cowlThing(iV16453),
inference(cnf_transformation,[],[f176]) ).
fof(f1128,plain,
cC58xcomp(iV16453),
inference(cnf_transformation,[],[f182]) ).
fof(f1129,plain,
rR1(iV16453,iV16461),
inference(cnf_transformation,[],[f183]) ).
fof(f1131,plain,
cowlThing(iV16455),
inference(cnf_transformation,[],[f185]) ).
fof(f1132,plain,
cC40xcomp(iV16455),
inference(cnf_transformation,[],[f186]) ).
fof(f1137,plain,
cC54xcomp(iV16455),
inference(cnf_transformation,[],[f191]) ).
fof(f1140,plain,
rR1(iV16455,iV16460),
inference(cnf_transformation,[],[f194]) ).
fof(f1142,plain,
cowlThing(iV16457),
inference(cnf_transformation,[],[f196]) ).
fof(f1144,plain,
cTOP(iV16457),
inference(cnf_transformation,[],[f198]) ).
fof(f1148,plain,
cC36xcomp(iV16457),
inference(cnf_transformation,[],[f202]) ).
fof(f1152,plain,
cowlThing(iV16459),
inference(cnf_transformation,[],[f206]) ).
fof(f1156,plain,
cC30xcomp(iV16459),
inference(cnf_transformation,[],[f210]) ).
fof(f1157,plain,
cC84xcomp(iV16459),
inference(cnf_transformation,[],[f211]) ).
fof(f1159,plain,
cC46xcomp(iV16459),
inference(cnf_transformation,[],[f213]) ).
fof(f1160,plain,
cC64xcomp(iV16459),
inference(cnf_transformation,[],[f214]) ).
fof(f1162,plain,
cC86xcomp(iV16459),
inference(cnf_transformation,[],[f216]) ).
fof(f1163,plain,
cC32xcomp(iV16459),
inference(cnf_transformation,[],[f217]) ).
fof(f1164,plain,
cC48xcomp(iV16459),
inference(cnf_transformation,[],[f218]) ).
fof(f1168,plain,
cC66xcomp(iV16459),
inference(cnf_transformation,[],[f222]) ).
fof(f1170,plain,
cowlThing(iV16460),
inference(cnf_transformation,[],[f224]) ).
fof(f1172,plain,
cTOP(iV16460),
inference(cnf_transformation,[],[f226]) ).
fof(f1174,plain,
cC8xcomp(iV16460),
inference(cnf_transformation,[],[f228]) ).
fof(f1175,plain,
cC36xcomp(iV16460),
inference(cnf_transformation,[],[f229]) ).
fof(f1180,plain,
cowlThing(iV16461),
inference(cnf_transformation,[],[f234]) ).
fof(f1181,plain,
cC40xcomp(iV16461),
inference(cnf_transformation,[],[f235]) ).
fof(f1184,plain,
cC12xcomp(iV16461),
inference(cnf_transformation,[],[f238]) ).
fof(f1187,plain,
cC54xcomp(iV16461),
inference(cnf_transformation,[],[f241]) ).
fof(f1193,plain,
cowlThing(iV16462),
inference(cnf_transformation,[],[f247]) ).
fof(f1194,plain,
cTOP(iV16462),
inference(cnf_transformation,[],[f248]) ).
fof(f1199,plain,
cC36xcomp(iV16462),
inference(cnf_transformation,[],[f253]) ).
fof(f1202,plain,
cC74xcomp(iV16463),
inference(cnf_transformation,[],[f256]) ).
fof(f1203,plain,
cowlThing(iV16463),
inference(cnf_transformation,[],[f257]) ).
fof(f1209,plain,
cC58xcomp(iV16463),
inference(cnf_transformation,[],[f263]) ).
fof(f1210,plain,
rR1(iV16463,iV16464),
inference(cnf_transformation,[],[f264]) ).
fof(f1211,plain,
cowlThing(iV16464),
inference(cnf_transformation,[],[f265]) ).
fof(f1213,plain,
cC40xcomp(iV16464),
inference(cnf_transformation,[],[f267]) ).
fof(f1217,plain,
cC54xcomp(iV16464),
inference(cnf_transformation,[],[f271]) ).
fof(f1223,plain,
cowlThing(iV16465),
inference(cnf_transformation,[],[f277]) ).
fof(f1224,plain,
cTOP(iV16465),
inference(cnf_transformation,[],[f278]) ).
fof(f1229,plain,
cC36xcomp(iV16465),
inference(cnf_transformation,[],[f283]) ).
fof(f1233,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| xsd_string(sK106)
| ~ xsd_integer(sK106)
| cowlNothing(sK105)
| ~ cowlThing(sK105) ),
inference(cnf_transformation,[],[f758]) ).
fof(f1234,plain,
( ~ cowlThing(iV16465)
| ~ cC38(iV16465)
| ~ cowlThing(iV16464)
| ~ cC44(iV16464)
| ~ cC42(iV16464)
| ~ cC56(iV16464)
| ~ cC60(iV16463)
| ~ cowlThing(iV16463)
| ~ cC62(iV16463)
| ~ cC76(iV16463)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cowlThing(iV16461)
| ~ cC44(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cowlThing(iV16459)
| ~ cC68(iV16459)
| ~ cC34(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cowlThing(iV16455)
| ~ cC42(iV16455)
| ~ cC44(iV16455)
| ~ cC56(iV16455)
| ~ cC60(iV16453)
| ~ cowlThing(iV16453)
| ~ cC62(iV16453)
| ~ cC76(iV16453)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16439)
| ~ cC28(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ cC108(iV16439)
| ~ cC130(iV16439)
| ~ xsd_string(sK106)
| xsd_integer(sK106)
| cowlNothing(sK105)
| ~ cowlThing(sK105) ),
inference(cnf_transformation,[],[f758]) ).
tcf(c_49,plain,
! [X0: $i] : cowlThing(X0),
inference(cnf_transformation,[],[f760]) ).
tcf(c_50,plain,
! [X0: $i] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f759]) ).
tcf(c_51,plain,
! [X0: $i] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f762]) ).
tcf(c_52,plain,
! [X0: $i] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[],[f761]) ).
tcf(c_72,plain,
! [X0: $i] :
( cC104(X0)
| ~ cC106(X0) ),
inference(cnf_transformation,[],[f782]) ).
tcf(c_75,plain,
! [X0: $i] :
( cC28(X0)
| ~ cC108(X0) ),
inference(cnf_transformation,[],[f785]) ).
tcf(c_76,plain,
! [X0: $i] :
( cC106(X0)
| ~ cC108(X0) ),
inference(cnf_transformation,[],[f784]) ).
tcf(c_168,plain,
! [X0: $i] :
( cC34(X0)
| ~ cC32xcomp(X0)
| ~ cC30xcomp(X0) ),
inference(cnf_transformation,[],[f880]) ).
tcf(c_180,plain,
! [X0: $i] :
( cC38(X0)
| ~ cTOP(X0)
| ~ cC36xcomp(X0) ),
inference(cnf_transformation,[],[f892]) ).
tcf(c_198,plain,
! [X0: $i,X1: $i] :
( cC42(X0)
| ~ cC8xcomp(X1)
| ~ rR1(X0,X1) ),
inference(cnf_transformation,[],[f910]) ).
tcf(c_201,plain,
! [X0: $i] :
( cC44(X0)
| ~ cC42(X0)
| ~ cC40xcomp(X0) ),
inference(cnf_transformation,[],[f913]) ).
tcf(c_203,plain,
! [X0: $i] :
( cC42(X0)
| ~ cC44(X0) ),
inference(cnf_transformation,[],[f911]) ).
tcf(c_218,plain,
! [X0: $i] :
( cC50(X0)
| ~ cC48xcomp(X0)
| ~ cC46xcomp(X0) ),
inference(cnf_transformation,[],[f930]) ).
tcf(c_238,plain,
! [X0: $i] :
( cC56(X0)
| ~ cC54xcomp(X0)
| ~ cC44(X0) ),
inference(cnf_transformation,[],[f950]) ).
tcf(c_240,plain,
! [X0: $i] :
( cC44(X0)
| ~ cC56(X0) ),
inference(cnf_transformation,[],[f948]) ).
tcf(c_241,plain,
! [X0: $i,X1: $i] :
( cC56(X0)
| ~ ra_Px17(X0,X1) ),
inference(cnf_transformation,[],[f952]) ).
tcf(c_243,plain,
! [X0: $i] :
( cC56xcomp(X0)
| ra_Px17(X0,sK60(X0)) ),
inference(cnf_transformation,[],[f954]) ).
tcf(c_245,plain,
! [X0: $i,X1: $i] :
( cC58(X0)
| ~ cC56xcomp(X1)
| ~ rR1(X0,X1) ),
inference(cnf_transformation,[],[f957]) ).
tcf(c_249,plain,
! [X0: $i,X1: $i] :
( ~ cC58(X0)
| ~ ra_Px19(X0,X1) ),
inference(cnf_transformation,[],[f958]) ).
tcf(c_251,plain,
! [X0: $i] :
( ra_Px19(X0,sK63(X0))
| ~ cC58xcomp(X0) ),
inference(cnf_transformation,[],[f960]) ).
tcf(c_258,plain,
! [X0: $i,X1: $i] :
( cC60(X0)
| ~ cC12xcomp(X1)
| ~ rR1(X0,X1) ),
inference(cnf_transformation,[],[f970]) ).
tcf(c_261,plain,
! [X0: $i] :
( cC62(X0)
| ~ cC60(X0)
| ~ cC58xcomp(X0) ),
inference(cnf_transformation,[],[f973]) ).
tcf(c_262,plain,
! [X0: $i] :
( cC60(X0)
| ~ cC62(X0) ),
inference(cnf_transformation,[],[f972]) ).
tcf(c_280,plain,
! [X0: $i] :
( cC68(X0)
| ~ cC66xcomp(X0)
| ~ cC64xcomp(X0) ),
inference(cnf_transformation,[],[f992]) ).
tcf(c_304,plain,
! [X0: $i,X1: $i] :
( cC76(X0)
| ~ ra_Px26(X0,X1) ),
inference(cnf_transformation,[],[f1015]) ).
tcf(c_306,plain,
! [X0: $i] :
( cC76(X0)
| ~ cC74xcomp(X0)
| ~ cC62(X0) ),
inference(cnf_transformation,[],[f1018]) ).
tcf(c_308,plain,
! [X0: $i] :
( cC62(X0)
| ~ cC76(X0) ),
inference(cnf_transformation,[],[f1016]) ).
tcf(c_309,plain,
! [X0: $i] :
( cC76xcomp(X0)
| ra_Px26(X0,sK81(X0)) ),
inference(cnf_transformation,[],[f1020]) ).
tcf(c_311,plain,
! [X0: $i,X1: $i] :
( cC78(X0)
| ~ cC76xcomp(X1)
| ~ rR1(X0,X1) ),
inference(cnf_transformation,[],[f1023]) ).
tcf(c_315,plain,
! [X0: $i,X1: $i] :
( ~ cC78(X0)
| ~ ra_Px28(X0,X1) ),
inference(cnf_transformation,[],[f1024]) ).
tcf(c_317,plain,
! [X0: $i] :
( ra_Px28(X0,sK84(X0))
| ~ cC78xcomp(X0) ),
inference(cnf_transformation,[],[f1026]) ).
tcf(c_326,plain,
! [X0: $i] :
( cC80(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[],[f1036]) ).
tcf(c_344,plain,
! [X0: $i] :
( cC88(X0)
| ~ cC86xcomp(X0)
| ~ cC84xcomp(X0) ),
inference(cnf_transformation,[],[f1056]) ).
tcf(c_378,plain,
! [X0: $i] :
( cC82(X0)
| ~ cC98(X0) ),
inference(cnf_transformation,[],[f1086]) ).
tcf(c_381,plain,
! [X0: $i] :
( cC108(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[],[f1092]) ).
tcf(c_382,plain,
! [X0: $i] :
( cC130(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[],[f1091]) ).
tcf(c_383,plain,
! [X0: $i] :
( cC98(X0)
| ~ rR1(iV16439,X0) ),
inference(cnf_transformation,[],[f1093]) ).
tcf(c_384,plain,
cowlThing(iV16439),
inference(cnf_transformation,[],[f1094]) ).
tcf(c_386,plain,
cTEST(iV16439),
inference(cnf_transformation,[],[f1096]) ).
tcf(c_387,plain,
rR1(iV16439,iV16440),
inference(cnf_transformation,[],[f1097]) ).
tcf(c_390,plain,
cowlThing(iV16440),
inference(cnf_transformation,[],[f1100]) ).
tcf(c_395,plain,
cC78xcomp(iV16440),
inference(cnf_transformation,[],[f1105]) ).
tcf(c_396,plain,
rR1(iV16440,iV16463),
inference(cnf_transformation,[],[f1106]) ).
tcf(c_399,plain,
cowlThing(iV16448),
inference(cnf_transformation,[],[f1109]) ).
tcf(c_400,plain,
cTOP(iV16448),
inference(cnf_transformation,[],[f1110]) ).
tcf(c_405,plain,
cC36xcomp(iV16448),
inference(cnf_transformation,[],[f1115]) ).
tcf(c_411,plain,
cC74xcomp(iV16453),
inference(cnf_transformation,[],[f1121]) ).
tcf(c_412,plain,
cowlThing(iV16453),
inference(cnf_transformation,[],[f1122]) ).
tcf(c_418,plain,
cC58xcomp(iV16453),
inference(cnf_transformation,[],[f1128]) ).
tcf(c_419,plain,
rR1(iV16453,iV16461),
inference(cnf_transformation,[],[f1129]) ).
tcf(c_421,plain,
cowlThing(iV16455),
inference(cnf_transformation,[],[f1131]) ).
tcf(c_422,plain,
cC40xcomp(iV16455),
inference(cnf_transformation,[],[f1132]) ).
tcf(c_427,plain,
cC54xcomp(iV16455),
inference(cnf_transformation,[],[f1137]) ).
tcf(c_430,plain,
rR1(iV16455,iV16460),
inference(cnf_transformation,[],[f1140]) ).
tcf(c_432,plain,
cowlThing(iV16457),
inference(cnf_transformation,[],[f1142]) ).
tcf(c_434,plain,
cTOP(iV16457),
inference(cnf_transformation,[],[f1144]) ).
tcf(c_438,plain,
cC36xcomp(iV16457),
inference(cnf_transformation,[],[f1148]) ).
tcf(c_442,plain,
cowlThing(iV16459),
inference(cnf_transformation,[],[f1152]) ).
tcf(c_446,plain,
cC30xcomp(iV16459),
inference(cnf_transformation,[],[f1156]) ).
tcf(c_447,plain,
cC84xcomp(iV16459),
inference(cnf_transformation,[],[f1157]) ).
tcf(c_449,plain,
cC46xcomp(iV16459),
inference(cnf_transformation,[],[f1159]) ).
tcf(c_450,plain,
cC64xcomp(iV16459),
inference(cnf_transformation,[],[f1160]) ).
tcf(c_452,plain,
cC86xcomp(iV16459),
inference(cnf_transformation,[],[f1162]) ).
tcf(c_453,plain,
cC32xcomp(iV16459),
inference(cnf_transformation,[],[f1163]) ).
tcf(c_454,plain,
cC48xcomp(iV16459),
inference(cnf_transformation,[],[f1164]) ).
tcf(c_458,plain,
cC66xcomp(iV16459),
inference(cnf_transformation,[],[f1168]) ).
tcf(c_460,plain,
cowlThing(iV16460),
inference(cnf_transformation,[],[f1170]) ).
tcf(c_462,plain,
cTOP(iV16460),
inference(cnf_transformation,[],[f1172]) ).
tcf(c_464,plain,
cC8xcomp(iV16460),
inference(cnf_transformation,[],[f1174]) ).
tcf(c_465,plain,
cC36xcomp(iV16460),
inference(cnf_transformation,[],[f1175]) ).
tcf(c_470,plain,
cowlThing(iV16461),
inference(cnf_transformation,[],[f1180]) ).
tcf(c_471,plain,
cC40xcomp(iV16461),
inference(cnf_transformation,[],[f1181]) ).
tcf(c_474,plain,
cC12xcomp(iV16461),
inference(cnf_transformation,[],[f1184]) ).
tcf(c_477,plain,
cC54xcomp(iV16461),
inference(cnf_transformation,[],[f1187]) ).
tcf(c_483,plain,
cowlThing(iV16462),
inference(cnf_transformation,[],[f1193]) ).
tcf(c_484,plain,
cTOP(iV16462),
inference(cnf_transformation,[],[f1194]) ).
tcf(c_489,plain,
cC36xcomp(iV16462),
inference(cnf_transformation,[],[f1199]) ).
tcf(c_492,plain,
cC74xcomp(iV16463),
inference(cnf_transformation,[],[f1202]) ).
tcf(c_493,plain,
cowlThing(iV16463),
inference(cnf_transformation,[],[f1203]) ).
tcf(c_499,plain,
cC58xcomp(iV16463),
inference(cnf_transformation,[],[f1209]) ).
tcf(c_500,plain,
rR1(iV16463,iV16464),
inference(cnf_transformation,[],[f1210]) ).
tcf(c_501,plain,
cowlThing(iV16464),
inference(cnf_transformation,[],[f1211]) ).
tcf(c_503,plain,
cC40xcomp(iV16464),
inference(cnf_transformation,[],[f1213]) ).
tcf(c_507,plain,
cC54xcomp(iV16464),
inference(cnf_transformation,[],[f1217]) ).
tcf(c_513,plain,
cowlThing(iV16465),
inference(cnf_transformation,[],[f1223]) ).
tcf(c_514,plain,
cTOP(iV16465),
inference(cnf_transformation,[],[f1224]) ).
tcf(c_519,plain,
cC36xcomp(iV16465),
inference(cnf_transformation,[],[f1229]) ).
tcf(c_523,negated_conjecture,
( xsd_integer(sK106)
| cowlNothing(sK105)
| ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ xsd_string(sK106)
| ~ cowlThing(sK105)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440)
| ~ cowlThing(iV16439) ),
inference(cnf_transformation,[],[f1234]) ).
tcf(c_524,negated_conjecture,
( xsd_string(sK106)
| cowlNothing(sK105)
| ~ cC98(iV16440)
| ~ cC88(iV16459)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC68(iV16459)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC50(iV16459)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC34(iV16459)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ xsd_integer(sK106)
| ~ cowlThing(sK105)
| ~ cowlThing(iV16465)
| ~ cowlThing(iV16464)
| ~ cowlThing(iV16462)
| ~ cowlThing(iV16459)
| ~ cowlThing(iV16457)
| ~ cowlThing(iV16460)
| ~ cowlThing(iV16455)
| ~ cowlThing(iV16461)
| ~ cowlThing(iV16453)
| ~ cowlThing(iV16448)
| ~ cowlThing(iV16463)
| ~ cowlThing(iV16440)
| ~ cowlThing(iV16439) ),
inference(cnf_transformation,[],[f1233]) ).
tcf(c_812,plain,
( cC88(iV16459)
| ~ cC86xcomp(iV16459)
| ~ cC84xcomp(iV16459) ),
inference(instantiation,[status(thm)],[c_344]) ).
tcf(c_817,plain,
( cC68(iV16459)
| ~ cC66xcomp(iV16459)
| ~ cC64xcomp(iV16459) ),
inference(instantiation,[status(thm)],[c_280]) ).
tcf(c_823,plain,
( cC50(iV16459)
| ~ cC48xcomp(iV16459)
| ~ cC46xcomp(iV16459) ),
inference(instantiation,[status(thm)],[c_218]) ).
tcf(c_828,plain,
( cC34(iV16459)
| ~ cC32xcomp(iV16459)
| ~ cC30xcomp(iV16459) ),
inference(instantiation,[status(thm)],[c_168]) ).
tcf(c_868,plain,
( xsd_string(sK106)
| cowlNothing(sK105)
| ~ cC98(iV16440)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ xsd_integer(sK106)
| ~ cowlThing(sK105)
| ~ cC38(iV16448)
| ~ cC38(iV16460)
| ~ cC38(iV16457)
| ~ cC38(iV16462)
| ~ cC38(iV16465)
| ~ cC42(iV16461)
| ~ cC42(iV16455)
| ~ cC42(iV16464)
| ~ cC44(iV16461)
| ~ cC44(iV16455)
| ~ cC44(iV16464)
| ~ cC76(iV16463)
| ~ cC76(iV16453)
| ~ cC80(iV16440)
| ~ cC82(iV16440) ),
inference(global_subsumption_just,[status(thm)],[c_524,c_513,c_501,c_493,c_483,c_470,c_460,c_458,c_454,c_453,c_452,c_450,c_449,c_447,c_446,c_442,c_432,c_421,c_412,c_399,c_390,c_384,c_812,c_817,c_823,c_828,c_524]) ).
tcf(c_869,negated_conjecture,
( xsd_string(sK106)
| cowlNothing(sK105)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ xsd_integer(sK106)
| ~ cowlThing(sK105) ),
inference(renaming,[status(thm)],[c_868]) ).
tcf(c_870,plain,
( xsd_integer(sK106)
| cowlNothing(sK105)
| ~ cC98(iV16440)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ xsd_string(sK106)
| ~ cowlThing(sK105)
| ~ cC38(iV16448)
| ~ cC38(iV16460)
| ~ cC38(iV16457)
| ~ cC38(iV16462)
| ~ cC38(iV16465)
| ~ cC42(iV16461)
| ~ cC42(iV16455)
| ~ cC42(iV16464)
| ~ cC44(iV16461)
| ~ cC44(iV16455)
| ~ cC44(iV16464)
| ~ cC76(iV16463)
| ~ cC76(iV16453)
| ~ cC80(iV16440)
| ~ cC82(iV16440) ),
inference(global_subsumption_just,[status(thm)],[c_523,c_513,c_501,c_493,c_483,c_470,c_460,c_458,c_454,c_453,c_452,c_450,c_449,c_447,c_446,c_442,c_432,c_421,c_412,c_399,c_390,c_384,c_812,c_817,c_823,c_828,c_523]) ).
tcf(c_871,negated_conjecture,
( xsd_integer(sK106)
| cowlNothing(sK105)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ xsd_string(sK106)
| ~ cowlThing(sK105) ),
inference(renaming,[status(thm)],[c_870]) ).
tcf(c_872,plain,
! [X0: $i] :
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(prop_impl_just,[status(thm)],[c_52]) ).
tcf(c_873,plain,
! [X0: $i] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(renaming,[status(thm)],[c_872]) ).
tcf(c_874,plain,
! [X0: $i] :
( xsd_string(X0)
| xsd_integer(X0) ),
inference(prop_impl_just,[status(thm)],[c_51]) ).
tcf(c_875,plain,
! [X0: $i] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(renaming,[status(thm)],[c_874]) ).
tcf(c_940,plain,
! [X0: $i] :
( ~ cC106(X0)
| cC104(X0) ),
inference(prop_impl_just,[status(thm)],[c_72]) ).
tcf(c_941,plain,
! [X0: $i] :
( cC104(X0)
| ~ cC106(X0) ),
inference(renaming,[status(thm)],[c_940]) ).
tcf(c_946,plain,
! [X0: $i] :
( ~ cC108(X0)
| cC106(X0) ),
inference(prop_impl_just,[status(thm)],[c_76]) ).
tcf(c_947,plain,
! [X0: $i] :
( cC106(X0)
| ~ cC108(X0) ),
inference(renaming,[status(thm)],[c_946]) ).
tcf(c_950,plain,
! [X0: $i] :
( cC28(X0)
| ~ cC108(X0) ),
inference(prop_impl_just,[status(thm)],[c_75]) ).
tcf(c_958,plain,
! [X0: $i] :
( ~ cTEST(X0)
| cC108(X0) ),
inference(prop_impl_just,[status(thm)],[c_381]) ).
tcf(c_959,plain,
! [X0: $i] :
( cC108(X0)
| ~ cTEST(X0) ),
inference(renaming,[status(thm)],[c_958]) ).
tcf(c_1064,plain,
! [X0: $i] :
( ~ cTEST(X0)
| cC130(X0) ),
inference(prop_impl_just,[status(thm)],[c_382]) ).
tcf(c_1065,plain,
! [X0: $i] :
( cC130(X0)
| ~ cTEST(X0) ),
inference(renaming,[status(thm)],[c_1064]) ).
tcf(c_1290,plain,
! [X0: $i] :
( ~ cC44(X0)
| cC42(X0) ),
inference(prop_impl_just,[status(thm)],[c_203]) ).
tcf(c_1291,plain,
! [X0: $i] :
( cC42(X0)
| ~ cC44(X0) ),
inference(renaming,[status(thm)],[c_1290]) ).
tcf(c_1296,plain,
! [X0: $i] :
( ~ cC56(X0)
| cC44(X0) ),
inference(prop_impl_just,[status(thm)],[c_240]) ).
tcf(c_1297,plain,
! [X0: $i] :
( cC44(X0)
| ~ cC56(X0) ),
inference(renaming,[status(thm)],[c_1296]) ).
tcf(c_1410,plain,
! [X0: $i,X1: $i] :
( ~ ra_Px17(X0,X1)
| cC56(X0) ),
inference(prop_impl_just,[status(thm)],[c_241]) ).
tcf(c_1411,plain,
! [X0: $i,X1: $i] :
( cC56(X0)
| ~ ra_Px17(X0,X1) ),
inference(renaming,[status(thm)],[c_1410]) ).
tcf(c_1422,plain,
! [X0: $i] :
( ra_Px17(X0,sK60(X0))
| cC56xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_243]) ).
tcf(c_1423,plain,
! [X0: $i] :
( cC56xcomp(X0)
| ra_Px17(X0,sK60(X0)) ),
inference(renaming,[status(thm)],[c_1422]) ).
tcf(c_1428,plain,
! [X0: $i,X1: $i] :
( ~ ra_Px19(X0,X1)
| ~ cC58(X0) ),
inference(prop_impl_just,[status(thm)],[c_249]) ).
tcf(c_1429,plain,
! [X0: $i,X1: $i] :
( ~ cC58(X0)
| ~ ra_Px19(X0,X1) ),
inference(renaming,[status(thm)],[c_1428]) ).
tcf(c_1436,plain,
! [X0: $i] :
( ra_Px19(X0,sK63(X0))
| ~ cC58xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_251]) ).
tcf(c_1452,plain,
! [X0: $i] :
( ~ cC62(X0)
| cC60(X0) ),
inference(prop_impl_just,[status(thm)],[c_262]) ).
tcf(c_1453,plain,
! [X0: $i] :
( cC60(X0)
| ~ cC62(X0) ),
inference(renaming,[status(thm)],[c_1452]) ).
tcf(c_1458,plain,
! [X0: $i] :
( ~ cC76(X0)
| cC62(X0) ),
inference(prop_impl_just,[status(thm)],[c_308]) ).
tcf(c_1459,plain,
! [X0: $i] :
( cC62(X0)
| ~ cC76(X0) ),
inference(renaming,[status(thm)],[c_1458]) ).
tcf(c_1582,plain,
! [X0: $i,X1: $i] :
( cC76(X0)
| ~ ra_Px26(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_304]) ).
tcf(c_1592,plain,
! [X0: $i] :
( ra_Px26(X0,sK81(X0))
| cC76xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_309]) ).
tcf(c_1593,plain,
! [X0: $i] :
( cC76xcomp(X0)
| ra_Px26(X0,sK81(X0)) ),
inference(renaming,[status(thm)],[c_1592]) ).
tcf(c_1598,plain,
! [X0: $i,X1: $i] :
( ~ ra_Px28(X0,X1)
| ~ cC78(X0) ),
inference(prop_impl_just,[status(thm)],[c_315]) ).
tcf(c_1599,plain,
! [X0: $i,X1: $i] :
( ~ cC78(X0)
| ~ ra_Px28(X0,X1) ),
inference(renaming,[status(thm)],[c_1598]) ).
tcf(c_1606,plain,
! [X0: $i] :
( ra_Px28(X0,sK84(X0))
| ~ cC78xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_317]) ).
tcf(c_1620,plain,
! [X0: $i] :
( ~ cC82(X0)
| cC80(X0) ),
inference(prop_impl_just,[status(thm)],[c_326]) ).
tcf(c_1621,plain,
! [X0: $i] :
( cC80(X0)
| ~ cC82(X0) ),
inference(renaming,[status(thm)],[c_1620]) ).
tcf(c_1626,plain,
! [X0: $i] :
( ~ cC98(X0)
| cC82(X0) ),
inference(prop_impl_just,[status(thm)],[c_378]) ).
tcf(c_1627,plain,
! [X0: $i] :
( cC82(X0)
| ~ cC98(X0) ),
inference(renaming,[status(thm)],[c_1626]) ).
tcf(c_2702,plain,
( xsd_integer(sK106)
| cowlNothing(sK105)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ xsd_string(sK106) ),
inference(backward_subsumption_resolution,[status(thm)],[c_871,c_49]) ).
tcf(c_2703,plain,
( xsd_string(sK106)
| cowlNothing(sK105)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ xsd_integer(sK106) ),
inference(backward_subsumption_resolution,[status(thm)],[c_869,c_49]) ).
tcf(c_2852,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ xsd_integer(sK106) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2703,c_50]) ).
tcf(c_2853,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439)
| ~ xsd_string(sK106) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2702,c_50]) ).
tcf(c_2877,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2853,c_875]) ).
tcf(c_2879,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439)
| ~ cC104(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2852,c_875]) ).
tcf(c_2920,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2877,c_941]) ).
tcf(c_2921,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439)
| ~ cC106(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2879,c_941]) ).
tcf(c_2926,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2921,c_947]) ).
tcf(c_2927,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC28(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2920,c_947]) ).
tcf(c_2932,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2927,c_950]) ).
tcf(c_2933,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC42(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2926,c_950]) ).
tcf(c_3054,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2933,c_1291]) ).
tcf(c_3055,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC44(iV16461)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2932,c_1291]) ).
tcf(c_3060,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3055,c_1297]) ).
tcf(c_3061,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC60(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3054,c_1297]) ).
tcf(c_3090,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3061,c_1453]) ).
tcf(c_3091,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC62(iV16463)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3060,c_1453]) ).
tcf(c_3096,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3091,c_1459]) ).
tcf(c_3097,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC80(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3090,c_1459]) ).
tcf(c_3118,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3097,c_1621]) ).
tcf(c_3119,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC82(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3096,c_1621]) ).
tcf(c_3124,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3119,c_1627]) ).
tcf(c_3125,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC62(iV16453)
| ~ cC60(iV16453)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC44(iV16464)
| ~ cC44(iV16455)
| ~ cC42(iV16464)
| ~ cC42(iV16455)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3118,c_1627]) ).
tcf(c_4520,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3124,c_1459,c_1453,c_1297,c_1297,c_1291,c_1291]) ).
tcf(c_4583,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC130(iV16439)
| ~ cC108(iV16439) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3125,c_1459,c_1453,c_1297,c_1297,c_1291,c_1291]) ).
tcf(c_4646,plain,
cC130(iV16439),
inference(resolution,[status(thm)],[c_1065,c_386]) ).
tcf(c_4650,plain,
cC108(iV16439),
inference(resolution,[status(thm)],[c_959,c_386]) ).
tcf(c_4655,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4520,c_4646]) ).
tcf(c_4656,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448)
| ~ cC108(iV16439) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4583,c_4646]) ).
tcf(c_4658,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4656,c_4650]) ).
tcf(c_4659,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460)
| ~ cC38(iV16448) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4655,c_4650]) ).
tcf(c_5458,plain,
! [X0: $i] :
( cC56xcomp(X0)
| cC56(X0) ),
inference(resolution,[status(thm)],[c_1411,c_1423]) ).
tcf(c_5480,plain,
! [X0: $i] :
( ~ cC58xcomp(X0)
| ~ cC58(X0) ),
inference(resolution,[status(thm)],[c_1429,c_1436]) ).
tcf(c_5588,plain,
! [X0: $i] :
( cC76xcomp(X0)
| cC76(X0) ),
inference(resolution,[status(thm)],[c_1582,c_1593]) ).
tcf(c_5610,plain,
! [X0: $i] :
( ~ cC78xcomp(X0)
| ~ cC78(X0) ),
inference(resolution,[status(thm)],[c_1599,c_1606]) ).
tcf(c_6544,plain,
( cC38(iV16448)
| ~ cC36xcomp(iV16448) ),
inference(resolution,[status(thm)],[c_180,c_400]) ).
tcf(c_6545,plain,
cC38(iV16448),
inference(global_subsumption_just,[status(thm)],[c_6544,c_405,c_6544]) ).
tcf(c_6550,plain,
( cC38(iV16457)
| ~ cC36xcomp(iV16457) ),
inference(resolution,[status(thm)],[c_180,c_434]) ).
tcf(c_6551,plain,
cC38(iV16457),
inference(global_subsumption_just,[status(thm)],[c_6550,c_438,c_6550]) ).
tcf(c_6556,plain,
( cC38(iV16460)
| ~ cC36xcomp(iV16460) ),
inference(resolution,[status(thm)],[c_180,c_462]) ).
tcf(c_6557,plain,
cC38(iV16460),
inference(global_subsumption_just,[status(thm)],[c_6556,c_465,c_6556]) ).
tcf(c_6562,plain,
( cC38(iV16462)
| ~ cC36xcomp(iV16462) ),
inference(resolution,[status(thm)],[c_180,c_484]) ).
tcf(c_6563,plain,
cC38(iV16462),
inference(global_subsumption_just,[status(thm)],[c_6562,c_489,c_6562]) ).
tcf(c_6568,plain,
( cC38(iV16465)
| ~ cC36xcomp(iV16465) ),
inference(resolution,[status(thm)],[c_180,c_514]) ).
tcf(c_6569,plain,
cC38(iV16465),
inference(global_subsumption_just,[status(thm)],[c_6568,c_519,c_6568]) ).
tcf(c_6575,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4659,c_6545]) ).
tcf(c_6576,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16457)
| ~ cC38(iV16460) ),
inference(backward_subsumption_resolution,[status(thm)],[c_4658,c_6545]) ).
tcf(c_6578,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16460) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6576,c_6551]) ).
tcf(c_6579,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462)
| ~ cC38(iV16460) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6575,c_6551]) ).
tcf(c_6581,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6579,c_6557]) ).
tcf(c_6582,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465)
| ~ cC38(iV16462) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6578,c_6557]) ).
tcf(c_6584,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6582,c_6563]) ).
tcf(c_6585,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ cC38(iV16465) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6581,c_6563]) ).
tcf(c_6587,plain,
( xsd_integer(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6585,c_6569]) ).
tcf(c_6588,plain,
( xsd_string(sK106)
| ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6584,c_6569]) ).
tcf(c_6590,plain,
( ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461)
| ~ xsd_integer(sK106) ),
inference(resolution,[status(thm)],[c_873,c_6588]) ).
tcf(c_6591,plain,
( ~ cC98(iV16440)
| ~ cC76(iV16453)
| ~ cC76(iV16463)
| ~ cC56(iV16464)
| ~ cC56(iV16455)
| ~ cC56(iV16461) ),
inference(global_subsumption_just,[status(thm)],[c_6590,c_6587,c_6590]) ).
tcf(c_6812,plain,
~ cC78(iV16440),
inference(resolution,[status(thm)],[c_5610,c_395]) ).
tcf(c_7247,plain,
~ cC58(iV16453),
inference(resolution,[status(thm)],[c_5480,c_418]) ).
tcf(c_7251,plain,
( cC62(iV16453)
| ~ cC60(iV16453) ),
inference(resolution,[status(thm)],[c_261,c_418]) ).
tcf(c_7258,plain,
~ cC58(iV16463),
inference(resolution,[status(thm)],[c_5480,c_499]) ).
tcf(c_7262,plain,
( cC62(iV16463)
| ~ cC60(iV16463) ),
inference(resolution,[status(thm)],[c_261,c_499]) ).
tcf(c_7305,plain,
( cC76(iV16453)
| ~ cC62(iV16453) ),
inference(resolution,[status(thm)],[c_306,c_411]) ).
tcf(c_7316,plain,
( cC76(iV16463)
| ~ cC62(iV16463) ),
inference(resolution,[status(thm)],[c_306,c_492]) ).
tcf(c_8034,plain,
! [X0: $i] :
( cC42(X0)
| ~ cC56(X0) ),
inference(resolution,[status(thm)],[c_1297,c_1291]) ).
tcf(c_8050,plain,
! [X0: $i] :
( cC56(X0)
| ~ cC54xcomp(X0)
| ~ cC42(X0)
| ~ cC40xcomp(X0) ),
inference(resolution,[status(thm)],[c_201,c_238]) ).
tcf(c_8659,plain,
! [X0: $i] :
( ~ cC76xcomp(X0)
| ~ rR1(iV16440,X0) ),
inference(resolution,[status(thm)],[c_311,c_6812]) ).
tcf(c_8907,plain,
( cC56(iV16455)
| ~ cC54xcomp(iV16455)
| ~ cC42(iV16455) ),
inference(resolution,[status(thm)],[c_8050,c_422]) ).
tcf(c_8920,plain,
( cC56(iV16461)
| ~ cC54xcomp(iV16461)
| ~ cC42(iV16461) ),
inference(resolution,[status(thm)],[c_8050,c_471]) ).
tcf(c_8933,plain,
( cC56(iV16464)
| ~ cC54xcomp(iV16464)
| ~ cC42(iV16464) ),
inference(resolution,[status(thm)],[c_8050,c_503]) ).
tcf(c_8934,plain,
( cC56(iV16464)
| ~ cC42(iV16464) ),
inference(global_subsumption_just,[status(thm)],[c_8933,c_507,c_8933]) ).
tcf(c_9171,plain,
! [X0: $i] :
( ~ cC56xcomp(X0)
| ~ rR1(iV16453,X0) ),
inference(resolution,[status(thm)],[c_245,c_7247]) ).
tcf(c_9180,plain,
! [X0: $i] :
( ~ cC56xcomp(X0)
| ~ rR1(iV16463,X0) ),
inference(resolution,[status(thm)],[c_245,c_7258]) ).
tcf(c_11865,plain,
! [X0: $i] :
( cC60(X0)
| ~ cC76(X0) ),
inference(resolution,[status(thm)],[c_1459,c_1453]) ).
tcf(c_11873,plain,
( cC76(iV16453)
| ~ cC60(iV16453) ),
inference(resolution,[status(thm)],[c_7251,c_7305]) ).
tcf(c_11880,plain,
( cC76(iV16463)
| ~ cC60(iV16463) ),
inference(resolution,[status(thm)],[c_7262,c_7316]) ).
tcf(c_15189,plain,
! [X0: $i] :
( cC56xcomp(X0)
| cC42(X0) ),
inference(prop_impl_just,[status(thm)],[c_5458,c_8034]) ).
tcf(c_15239,plain,
! [X0: $i] :
( cC76xcomp(X0)
| cC60(X0) ),
inference(prop_impl_just,[status(thm)],[c_5588,c_11865]) ).
tcf(c_15437,plain,
( cC56(iV16461)
| ~ cC42(iV16461) ),
inference(prop_impl_just,[status(thm)],[c_477,c_8920]) ).
tcf(c_15441,plain,
( ~ cC60(iV16463)
| cC76(iV16463) ),
inference(prop_impl_just,[status(thm)],[c_11880]) ).
tcf(c_15442,plain,
( cC76(iV16463)
| ~ cC60(iV16463) ),
inference(renaming,[status(thm)],[c_15441]) ).
tcf(c_15445,plain,
( ~ cC42(iV16464)
| cC56(iV16464) ),
inference(prop_impl_just,[status(thm)],[c_8934]) ).
tcf(c_15446,plain,
( cC56(iV16464)
| ~ cC42(iV16464) ),
inference(renaming,[status(thm)],[c_15445]) ).
tcf(c_18578,plain,
( cC76xcomp(iV16463)
| cC76(iV16463) ),
inference(resolution,[status(thm)],[c_15239,c_15442]) ).
tcf(c_18877,plain,
( cC56xcomp(iV16461)
| cC56(iV16461) ),
inference(resolution,[status(thm)],[c_15189,c_15437]) ).
tcf(c_18888,plain,
( cC56xcomp(iV16464)
| cC56(iV16464) ),
inference(resolution,[status(thm)],[c_15189,c_15446]) ).
tcf(c_23256,plain,
! [X0: $i] :
( ~ rR1(iV16453,X0)
| ~ cC56xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_9171]) ).
tcf(c_23257,plain,
! [X0: $i] :
( ~ cC56xcomp(X0)
| ~ rR1(iV16453,X0) ),
inference(renaming,[status(thm)],[c_23256]) ).
tcf(c_23258,plain,
! [X0: $i] :
( ~ rR1(iV16463,X0)
| ~ cC56xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_9180]) ).
tcf(c_23259,plain,
! [X0: $i] :
( ~ cC56xcomp(X0)
| ~ rR1(iV16463,X0) ),
inference(renaming,[status(thm)],[c_23258]) ).
tcf(c_23312,plain,
! [X0: $i] :
( ~ rR1(iV16440,X0)
| ~ cC76xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_8659]) ).
tcf(c_23313,plain,
! [X0: $i] :
( ~ cC76xcomp(X0)
| ~ rR1(iV16440,X0) ),
inference(renaming,[status(thm)],[c_23312]) ).
tcf(c_30877,plain,
( cC98(iV16440)
| ~ rR1(iV16439,iV16440) ),
inference(instantiation,[status(thm)],[c_383]) ).
tcf(c_30890,plain,
( ~ cC56xcomp(iV16461)
| ~ rR1(iV16453,iV16461) ),
inference(instantiation,[status(thm)],[c_23257]) ).
tcf(c_30891,plain,
( ~ cC56xcomp(iV16464)
| ~ rR1(iV16463,iV16464) ),
inference(instantiation,[status(thm)],[c_23259]) ).
tcf(c_30892,plain,
( ~ cC76xcomp(iV16463)
| ~ rR1(iV16440,iV16463) ),
inference(instantiation,[status(thm)],[c_23313]) ).
tcf(c_30952,plain,
( cC42(iV16455)
| ~ cC8xcomp(iV16460)
| ~ rR1(iV16455,iV16460) ),
inference(instantiation,[status(thm)],[c_198]) ).
tcf(c_30967,plain,
! [X0: $i] :
( cC60(X0)
| ~ cC12xcomp(iV16461)
| ~ rR1(X0,iV16461) ),
inference(instantiation,[status(thm)],[c_258]) ).
tcf(c_31256,plain,
( cC60(iV16453)
| ~ cC12xcomp(iV16461)
| ~ rR1(iV16453,iV16461) ),
inference(instantiation,[status(thm)],[c_30967]) ).
tcf(c_31257,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_31256,c_30952,c_30892,c_30891,c_30890,c_30877,c_18888,c_18877,c_18578,c_11873,c_8907,c_6591,c_387,c_396,c_419,c_430,c_500,c_427,c_464,c_474]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS161+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n018.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 19:35:33 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.42
% 0.10/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.42
% 0.10/0.42 % Detected problem language: tptp
% 0.10/0.43 % Proving...
% 6.71/1.65 % SZS status Started for theBenchmark.p
% 6.71/1.65 % SZS status Theorem for theBenchmark.p
% 6.71/1.65
% 6.71/1.65 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.71/1.65
% 6.71/1.65 % ------ iProver source info
% 6.71/1.65
% 6.71/1.65 % git: date: 2026-07-19 20:42:38 +0200
% 6.71/1.65 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.71/1.65 % git: non_committed_changes: false
% 6.71/1.65
% 6.71/1.65 % ------ Parsing...
% 6.71/1.65 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.71/1.65
% 6.71/1.65 % ------ Preprocessing... sf_s rm: 2 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe:32:0s pe:64:0s pe_e sf_s rm: 0 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 6.71/1.65
% 6.71/1.65 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 6.71/1.65 % ------ Proving...
% 6.71/1.65 % ------ Problem Properties
% 6.71/1.65
% 6.71/1.65 %
% 6.71/1.65 % clauses 257
% 6.71/1.65 % conjectures 0
% 6.71/1.65 % EPR 201
% 6.71/1.65 % Horn 232
% 6.71/1.65 % unary 79
% 6.71/1.65 % binary 129
% 6.71/1.65 % lits 492
% 6.71/1.65 % lits eq 0
% 6.71/1.65 % fd_pure 0
% 6.71/1.65 % fd_pseudo 0
% 6.71/1.65 % fd_cond 0
% 6.71/1.65 % fd_pseudo_cond 0
% 6.71/1.65 % AC symbols 0
% 6.71/1.65
% 6.71/1.65 % ------ Schedule dynamic 5 is on
% 6.71/1.65
% 6.71/1.65 % ------ no conjectures: strip conj schedule
% 6.71/1.65
% 6.71/1.65 % ------ no equalities: superposition off
% 6.71/1.65
% 6.71/1.65 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 6.71/1.65
% 6.71/1.65
% 6.71/1.65 % ------
% 6.71/1.65 % Current options:
% 6.71/1.65 % ------
% 6.71/1.65
% 6.71/1.65
% 6.71/1.65 %
% 6.71/1.65
% 6.71/1.65 % ------ Proving...
% 6.71/1.65 %
% 6.71/1.65
% 6.71/1.65 % SZS status Theorem for theBenchmark.p
% 6.71/1.65
% 6.71/1.65 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.71/1.66
% 6.71/1.66
%------------------------------------------------------------------------------