%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KRS159+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 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 : Fri Sep 25 01:54:18 PM UTC 2026
% Result : Theorem 3.51s 1.18s
% Output : CNFRefutation 3.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 76
% Syntax : Number of formulae : 522 ( 56 unt; 0 def)
% Number of atoms : 1984 ( 0 equ)
% Maximal formula atoms : 56 ( 3 avg)
% Number of connectives : 2506 (1044 ~;1018 |; 366 &)
% ( 70 <=>; 7 =>; 0 <=; 1 <~>)
% Maximal formula depth : 55 ( 5 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 : 88 ( 87 usr; 1 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 6 con; 0-1 aty)
% Number of variables : 585 ( 0 sgn 513 !; 72 ?; 154 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
fof(f2,axiom,
! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f3,axiom,
! [X0] :
( cC10(X0)
<=> ( cC4(X0)
& cC8(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
fof(f16,axiom,
! [X0] :
( cC110(X0)
<=> ( cTOP(X0)
& cC108(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_15) ).
fof(f17,axiom,
! [X0] :
( cC112(X0)
<=> ( cC90(X0)
& cC110(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_16) ).
fof(f19,axiom,
! [X0] :
( cC116(X0)
<=> ( cC112(X0)
& cC114(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_18) ).
fof(f41,axiom,
! [X0] :
( cC132(X0)
<=> ( cTOP(X0)
& cC130(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_40) ).
fof(f42,axiom,
! [X0] :
( cC134(X0)
<=> ( cC132(X0)
& cC116(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_41) ).
fof(f44,axiom,
! [X0] :
( cC138(X0)
<=> ( cC134(X0)
& cC136(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_43) ).
fof(f65,axiom,
! [X0] :
( cC154(X0)
<=> ( cTOP(X0)
& cC152(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_64) ).
fof(f66,axiom,
! [X0] :
( cC156(X0)
<=> ( cC138(X0)
& cC154(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_65) ).
fof(f67,axiom,
! [X0] :
( cC158(X0)
<=> ( cC156(X0)
& cC22(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_66) ).
fof(f68,axiom,
! [X0] :
( cC16(X0)
<=> ( cC14(X0)
& cC10(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_67) ).
fof(f88,axiom,
! [X0] :
( cC174(X0)
<=> ( cC168(X0)
& cC172xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_87) ).
fof(f97,axiom,
! [X0] :
( cC180(X0)
<=> ( cC178xcomp(X0)
& cC174(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_96) ).
fof(f101,axiom,
! [X0] :
( cC22(X0)
<=> ( cC16(X0)
& cC20(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_100) ).
fof(f102,axiom,
! [X0] :
( cC24(X0)
<=> ? [X1] : ra_Px5(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_101) ).
fof(f104,axiom,
! [X0] :
( cC24xcomp(X0)
<=> ~ ? [X1] : ra_Px5(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_103) ).
fof(f105,axiom,
! [X0] :
( cC26(X0)
<=> ? [X1] : ra_Px92(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_104) ).
fof(f106,axiom,
! [X0] :
( cC26(X0)
<=> ( cC2xcomp(X0)
& cC24xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_105) ).
fof(f107,axiom,
! [X0] :
( cC26xcomp(X0)
<=> ~ ? [X1] : ra_Px92(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_106) ).
fof(f111,axiom,
! [X0] :
( cC30(X0)
<=> ? [X1] : ra_Px8(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_110) ).
fof(f113,axiom,
! [X0] :
( cC30xcomp(X0)
<=> ~ ? [X1] : ra_Px8(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_112) ).
fof(f114,axiom,
! [X0] :
( cC32(X0)
<=> ~ ? [X1] : ra_Px91(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_113) ).
fof(f115,axiom,
! [X0] :
( cC32(X0)
<=> ( cC30xcomp(X0)
& cC2xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_114) ).
fof(f116,axiom,
! [X0] :
( cC32xcomp(X0)
<=> ? [X1] : ra_Px91(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_115) ).
fof(f121,axiom,
! [X0] :
( cC38(X0)
<=> ( cTOP(X0)
& cC36(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_120) ).
fof(f123,axiom,
! [X0] :
( cC40(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_122) ).
fof(f124,axiom,
! [X0] :
( cC42(X0)
<=> ( cC38(X0)
& cC40(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_123) ).
fof(f125,axiom,
! [X0] :
( cC44(X0)
<=> ~ ? [X1] : ra_Px13(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_124) ).
fof(f127,axiom,
! [X0] :
( cC44xcomp(X0)
<=> ? [X1] : ra_Px13(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_126) ).
fof(f128,axiom,
! [X0] :
( cC46(X0)
<=> ? [X1] : ra_Px90(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_127) ).
fof(f129,axiom,
! [X0] :
( cC46(X0)
<=> ( cC12xcomp(X0)
& cC44xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_128) ).
fof(f130,axiom,
! [X0] :
( cC46xcomp(X0)
<=> ~ ? [X1] : ra_Px90(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_129) ).
fof(f135,axiom,
! [X0] :
( cC50(X0)
<=> ~ ? [X1] : ra_Px16(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_134) ).
fof(f136,axiom,
! [X0] :
( cC50xcomp(X0)
<=> ? [X1] : ra_Px16(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_135) ).
fof(f137,axiom,
! [X0] :
( cC52(X0)
<=> ? [X1] : ra_Px89(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_136) ).
fof(f138,axiom,
! [X0] :
( cC52(X0)
<=> ( cC12xcomp(X0)
& cC50xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_137) ).
fof(f139,axiom,
! [X0] :
( cC52xcomp(X0)
<=> ~ ? [X1] : ra_Px89(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_138) ).
fof(f144,axiom,
! [X0] :
( cC58(X0)
<=> ( cTOP(X0)
& cC56(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_143) ).
fof(f147,axiom,
! [X0] :
( cC60(X0)
<=> ( cC42(X0)
& cC58(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_146) ).
fof(f148,axiom,
! [X0] :
( cC62(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_147) ).
fof(f149,axiom,
! [X0] :
( cC64(X0)
<=> ( cC62(X0)
& cC60(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_148) ).
fof(f150,axiom,
! [X0] :
( cC66(X0)
<=> ? [X1] : ra_Px21(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_149) ).
fof(f152,axiom,
! [X0] :
( cC66xcomp(X0)
<=> ~ ? [X1] : ra_Px21(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_151) ).
fof(f153,axiom,
! [X0] :
( cC68(X0)
<=> ~ ? [X1] : ra_Px88(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_152) ).
fof(f154,axiom,
! [X0] :
( cC68(X0)
<=> ( cC66xcomp(X0)
& cC18xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_153) ).
fof(f155,axiom,
! [X0] :
( cC68xcomp(X0)
<=> ? [X1] : ra_Px88(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_154) ).
fof(f159,axiom,
! [X0] :
( cC72(X0)
<=> ? [X1] : ra_Px24(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_158) ).
fof(f161,axiom,
! [X0] :
( cC72xcomp(X0)
<=> ~ ? [X1] : ra_Px24(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_160) ).
fof(f162,axiom,
! [X0] :
( cC74(X0)
<=> ( cC18xcomp(X0)
& cC72xcomp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_161) ).
fof(f163,axiom,
! [X0] :
( cC74(X0)
<=> ? [X1] : ra_Px87(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_162) ).
fof(f164,axiom,
! [X0] :
( cC74xcomp(X0)
<=> ~ ? [X1] : ra_Px87(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_163) ).
fof(f170,axiom,
! [X0] :
( cC80(X0)
<=> ( cTOP(X0)
& cC78(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_169) ).
fof(f171,axiom,
! [X0] :
( cC82(X0)
<=> ( cC80(X0)
& cC64(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_170) ).
fof(f172,axiom,
! [X0] :
( cC84(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_171) ).
fof(f173,axiom,
! [X0] :
( cC86(X0)
<=> ( cC84(X0)
& cC82(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_172) ).
fof(f174,axiom,
! [X0] :
( cC88(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_173) ).
fof(f175,axiom,
! [X0] :
( cC90(X0)
<=> ( cC88(X0)
& cC86(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_174) ).
fof(f187,axiom,
! [X0] :
( cTEST(X0)
<=> ( cC180(X0)
& cC158(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_186) ).
fof(f191,axiom,
cTOP(iV21026),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_190) ).
fof(f220,axiom,
cowlThing(iV21026),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_219) ).
fof(f222,axiom,
cTEST(iV21026),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_221) ).
fof(f238,axiom,
cC2xcomp(iV21027),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_237) ).
fof(f243,axiom,
cC26xcomp(iV21027),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_242) ).
fof(f249,axiom,
cowlThing(iV21027),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_248) ).
fof(f251,axiom,
cC32xcomp(iV21027),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_250) ).
fof(f266,axiom,
cC12xcomp(iV21029),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_265) ).
fof(f269,axiom,
cC52xcomp(iV21029),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_268) ).
fof(f273,axiom,
cC46xcomp(iV21029),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_272) ).
fof(f279,axiom,
cowlThing(iV21029),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_278) ).
fof(f292,axiom,
cC68xcomp(iV21030),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_291) ).
fof(f294,axiom,
cC18xcomp(iV21030),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_293) ).
fof(f307,axiom,
cowlThing(iV21030),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_306) ).
fof(f308,axiom,
cC74xcomp(iV21030),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_307) ).
fof(f343,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)
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',the_axiom) ).
fof(f344,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)
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
inference(negated_conjecture,[status(cth)],[f343]) ).
fof(f345,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)
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& ! [X0] :
( ~ cowlNothing(X0)
& cowlThing(X0) ) ),
inference(rectify,[],[f344]) ).
fof(f346,plain,
! [X0] :
( cTEST(X0)
=> ( cC180(X0)
& cC158(X0) ) ),
inference(unused_predicate_definition_removal,[],[f187]) ).
fof(f349,plain,
! [X0] :
( cC74xcomp(X0)
=> ~ ? [X1] : ra_Px87(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f164]) ).
fof(f350,plain,
! [X0] :
( cC68xcomp(X0)
=> ? [X1] : ra_Px88(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f155]) ).
fof(f352,plain,
! [X0] :
( cC52xcomp(X0)
=> ~ ? [X1] : ra_Px89(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f139]) ).
fof(f353,plain,
! [X0] :
( cC46xcomp(X0)
=> ~ ? [X1] : ra_Px90(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f130]) ).
fof(f354,plain,
! [X0] :
( cC32xcomp(X0)
=> ? [X1] : ra_Px91(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f116]) ).
fof(f355,plain,
! [X0] :
( cC26xcomp(X0)
=> ~ ? [X1] : ra_Px92(X0,X1) ),
inference(unused_predicate_definition_removal,[],[f107]) ).
fof(f402,plain,
! [X0] :
( cC24xcomp(X0)
<=> ! [X1] : ~ ra_Px5(X0,X1) ),
inference(ennf_transformation,[],[f104]) ).
fof(f403,plain,
! [X0] :
( ~ cC26xcomp(X0)
| ! [X1] : ~ ra_Px92(X0,X1) ),
inference(ennf_transformation,[],[f355]) ).
fof(f405,plain,
! [X0] :
( cC30xcomp(X0)
<=> ! [X1] : ~ ra_Px8(X0,X1) ),
inference(ennf_transformation,[],[f113]) ).
fof(f406,plain,
! [X0] :
( cC32(X0)
<=> ! [X1] : ~ ra_Px91(X0,X1) ),
inference(ennf_transformation,[],[f114]) ).
fof(f407,plain,
! [X0] :
( ~ cC32xcomp(X0)
| ? [X1] : ra_Px91(X0,X1) ),
inference(ennf_transformation,[],[f354]) ).
fof(f409,plain,
! [X0] :
( cC44(X0)
<=> ! [X1] : ~ ra_Px13(X0,X1) ),
inference(ennf_transformation,[],[f125]) ).
fof(f410,plain,
! [X0] :
( ~ cC46xcomp(X0)
| ! [X1] : ~ ra_Px90(X0,X1) ),
inference(ennf_transformation,[],[f353]) ).
fof(f412,plain,
! [X0] :
( cC50(X0)
<=> ! [X1] : ~ ra_Px16(X0,X1) ),
inference(ennf_transformation,[],[f135]) ).
fof(f413,plain,
! [X0] :
( ~ cC52xcomp(X0)
| ! [X1] : ~ ra_Px89(X0,X1) ),
inference(ennf_transformation,[],[f352]) ).
fof(f417,plain,
! [X0] :
( cC66xcomp(X0)
<=> ! [X1] : ~ ra_Px21(X0,X1) ),
inference(ennf_transformation,[],[f152]) ).
fof(f418,plain,
! [X0] :
( cC68(X0)
<=> ! [X1] : ~ ra_Px88(X0,X1) ),
inference(ennf_transformation,[],[f153]) ).
fof(f419,plain,
! [X0] :
( ~ cC68xcomp(X0)
| ? [X1] : ra_Px88(X0,X1) ),
inference(ennf_transformation,[],[f350]) ).
fof(f421,plain,
! [X0] :
( cC72xcomp(X0)
<=> ! [X1] : ~ ra_Px24(X0,X1) ),
inference(ennf_transformation,[],[f161]) ).
fof(f422,plain,
! [X0] :
( ~ cC74xcomp(X0)
| ! [X1] : ~ ra_Px87(X0,X1) ),
inference(ennf_transformation,[],[f349]) ).
fof(f428,plain,
! [X0] :
( ~ cTEST(X0)
| ( cC180(X0)
& cC158(X0) ) ),
inference(ennf_transformation,[],[f346]) ).
fof(f457,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)
| ? [X1] :
( xsd_string(X1)
<~> ~ xsd_integer(X1) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(ennf_transformation,[],[f345]) ).
fof(f458,plain,
! [X0] :
( ( ~ xsd_string(X0)
| ~ xsd_integer(X0) )
& ( xsd_integer(X0)
| xsd_string(X0) ) ),
inference(nnf_transformation,[],[f2]) ).
fof(f459,plain,
! [X0] :
( ( ~ cC10(X0)
| ( cC4(X0)
& cC8(X0) ) )
& ( ~ cC4(X0)
| ~ cC8(X0)
| cC10(X0) ) ),
inference(nnf_transformation,[],[f3]) ).
fof(f460,plain,
! [X0] :
( ( ~ cC10(X0)
| ( cC4(X0)
& cC8(X0) ) )
& ( ~ cC4(X0)
| ~ cC8(X0)
| cC10(X0) ) ),
inference(flattening,[],[f459]) ).
fof(f491,plain,
! [X0] :
( ( ~ cC110(X0)
| ( cTOP(X0)
& cC108(X0) ) )
& ( ~ cTOP(X0)
| ~ cC108(X0)
| cC110(X0) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f492,plain,
! [X0] :
( ( ~ cC110(X0)
| ( cTOP(X0)
& cC108(X0) ) )
& ( ~ cTOP(X0)
| ~ cC108(X0)
| cC110(X0) ) ),
inference(flattening,[],[f491]) ).
fof(f493,plain,
! [X0] :
( ( ~ cC112(X0)
| ( cC90(X0)
& cC110(X0) ) )
& ( ~ cC90(X0)
| ~ cC110(X0)
| cC112(X0) ) ),
inference(nnf_transformation,[],[f17]) ).
fof(f494,plain,
! [X0] :
( ( ~ cC112(X0)
| ( cC90(X0)
& cC110(X0) ) )
& ( ~ cC90(X0)
| ~ cC110(X0)
| cC112(X0) ) ),
inference(flattening,[],[f493]) ).
fof(f496,plain,
! [X0] :
( ( ~ cC116(X0)
| ( cC112(X0)
& cC114(X0) ) )
& ( ~ cC112(X0)
| ~ cC114(X0)
| cC116(X0) ) ),
inference(nnf_transformation,[],[f19]) ).
fof(f497,plain,
! [X0] :
( ( ~ cC116(X0)
| ( cC112(X0)
& cC114(X0) ) )
& ( ~ cC112(X0)
| ~ cC114(X0)
| cC116(X0) ) ),
inference(flattening,[],[f496]) ).
fof(f549,plain,
! [X0] :
( ( ~ cC132(X0)
| ( cTOP(X0)
& cC130(X0) ) )
& ( ~ cTOP(X0)
| ~ cC130(X0)
| cC132(X0) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f550,plain,
! [X0] :
( ( ~ cC132(X0)
| ( cTOP(X0)
& cC130(X0) ) )
& ( ~ cTOP(X0)
| ~ cC130(X0)
| cC132(X0) ) ),
inference(flattening,[],[f549]) ).
fof(f551,plain,
! [X0] :
( ( ~ cC134(X0)
| ( cC132(X0)
& cC116(X0) ) )
& ( ~ cC132(X0)
| ~ cC116(X0)
| cC134(X0) ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f552,plain,
! [X0] :
( ( ~ cC134(X0)
| ( cC132(X0)
& cC116(X0) ) )
& ( ~ cC132(X0)
| ~ cC116(X0)
| cC134(X0) ) ),
inference(flattening,[],[f551]) ).
fof(f554,plain,
! [X0] :
( ( ~ cC138(X0)
| ( cC134(X0)
& cC136(X0) ) )
& ( ~ cC134(X0)
| ~ cC136(X0)
| cC138(X0) ) ),
inference(nnf_transformation,[],[f44]) ).
fof(f555,plain,
! [X0] :
( ( ~ cC138(X0)
| ( cC134(X0)
& cC136(X0) ) )
& ( ~ cC134(X0)
| ~ cC136(X0)
| cC138(X0) ) ),
inference(flattening,[],[f554]) ).
fof(f608,plain,
! [X0] :
( ( ~ cC154(X0)
| ( cTOP(X0)
& cC152(X0) ) )
& ( ~ cTOP(X0)
| ~ cC152(X0)
| cC154(X0) ) ),
inference(nnf_transformation,[],[f65]) ).
fof(f609,plain,
! [X0] :
( ( ~ cC154(X0)
| ( cTOP(X0)
& cC152(X0) ) )
& ( ~ cTOP(X0)
| ~ cC152(X0)
| cC154(X0) ) ),
inference(flattening,[],[f608]) ).
fof(f610,plain,
! [X0] :
( ( ~ cC156(X0)
| ( cC138(X0)
& cC154(X0) ) )
& ( ~ cC138(X0)
| ~ cC154(X0)
| cC156(X0) ) ),
inference(nnf_transformation,[],[f66]) ).
fof(f611,plain,
! [X0] :
( ( ~ cC156(X0)
| ( cC138(X0)
& cC154(X0) ) )
& ( ~ cC138(X0)
| ~ cC154(X0)
| cC156(X0) ) ),
inference(flattening,[],[f610]) ).
fof(f612,plain,
! [X0] :
( ( ~ cC158(X0)
| ( cC156(X0)
& cC22(X0) ) )
& ( ~ cC156(X0)
| ~ cC22(X0)
| cC158(X0) ) ),
inference(nnf_transformation,[],[f67]) ).
fof(f613,plain,
! [X0] :
( ( ~ cC158(X0)
| ( cC156(X0)
& cC22(X0) ) )
& ( ~ cC156(X0)
| ~ cC22(X0)
| cC158(X0) ) ),
inference(flattening,[],[f612]) ).
fof(f614,plain,
! [X0] :
( ( ~ cC16(X0)
| ( cC14(X0)
& cC10(X0) ) )
& ( ~ cC14(X0)
| ~ cC10(X0)
| cC16(X0) ) ),
inference(nnf_transformation,[],[f68]) ).
fof(f615,plain,
! [X0] :
( ( ~ cC16(X0)
| ( cC14(X0)
& cC10(X0) ) )
& ( ~ cC14(X0)
| ~ cC10(X0)
| cC16(X0) ) ),
inference(flattening,[],[f614]) ).
fof(f664,plain,
! [X0] :
( ( ~ cC174(X0)
| ( cC168(X0)
& cC172xcomp(X0) ) )
& ( ~ cC168(X0)
| ~ cC172xcomp(X0)
| cC174(X0) ) ),
inference(nnf_transformation,[],[f88]) ).
fof(f665,plain,
! [X0] :
( ( ~ cC174(X0)
| ( cC168(X0)
& cC172xcomp(X0) ) )
& ( ~ cC168(X0)
| ~ cC172xcomp(X0)
| cC174(X0) ) ),
inference(flattening,[],[f664]) ).
fof(f685,plain,
! [X0] :
( ( ~ cC180(X0)
| ( cC178xcomp(X0)
& cC174(X0) ) )
& ( ~ cC178xcomp(X0)
| ~ cC174(X0)
| cC180(X0) ) ),
inference(nnf_transformation,[],[f97]) ).
fof(f686,plain,
! [X0] :
( ( ~ cC180(X0)
| ( cC178xcomp(X0)
& cC174(X0) ) )
& ( ~ cC178xcomp(X0)
| ~ cC174(X0)
| cC180(X0) ) ),
inference(flattening,[],[f685]) ).
fof(f694,plain,
! [X0] :
( ( ~ cC22(X0)
| ( cC16(X0)
& cC20(X0) ) )
& ( ~ cC16(X0)
| ~ cC20(X0)
| cC22(X0) ) ),
inference(nnf_transformation,[],[f101]) ).
fof(f695,plain,
! [X0] :
( ( ~ cC22(X0)
| ( cC16(X0)
& cC20(X0) ) )
& ( ~ cC16(X0)
| ~ cC20(X0)
| cC22(X0) ) ),
inference(flattening,[],[f694]) ).
fof(f696,plain,
! [X0] :
( ( ~ cC24(X0)
| ? [X1] : ra_Px5(X0,X1) )
& ( ! [X1] : ~ ra_Px5(X0,X1)
| cC24(X0) ) ),
inference(nnf_transformation,[],[f102]) ).
fof(f697,plain,
! [X0] :
( ( ~ cC24(X0)
| ? [X2] : ra_Px5(X0,X2) )
& ( ! [X1] : ~ ra_Px5(X0,X1)
| cC24(X0) ) ),
inference(rectify,[],[f696]) ).
fof(f698,plain,
! [X0] :
( ( ~ cC24(X0)
| ra_Px5(X0,sK67(X0)) )
& ( ! [X1] : ~ ra_Px5(X0,X1)
| cC24(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67]),skolemize(X2,sK67(X0))],[f697]) ).
fof(f702,plain,
! [X0] :
( ( ~ cC24xcomp(X0)
| ! [X1] : ~ ra_Px5(X0,X1) )
& ( ? [X1] : ra_Px5(X0,X1)
| cC24xcomp(X0) ) ),
inference(nnf_transformation,[],[f402]) ).
fof(f703,plain,
! [X0] :
( ( ~ cC24xcomp(X0)
| ! [X2] : ~ ra_Px5(X0,X2) )
& ( ? [X1] : ra_Px5(X0,X1)
| cC24xcomp(X0) ) ),
inference(rectify,[],[f702]) ).
fof(f704,plain,
! [X0] :
( ( ~ cC24xcomp(X0)
| ! [X2] : ~ ra_Px5(X0,X2) )
& ( ra_Px5(X0,sK69(X0))
| cC24xcomp(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK69]),skolemize(X1,sK69(X0))],[f703]) ).
fof(f705,plain,
! [X0] :
( ( ~ cC26(X0)
| ? [X1] : ra_Px92(X0,X1) )
& ( ! [X1] : ~ ra_Px92(X0,X1)
| cC26(X0) ) ),
inference(nnf_transformation,[],[f105]) ).
fof(f706,plain,
! [X0] :
( ( ~ cC26(X0)
| ? [X2] : ra_Px92(X0,X2) )
& ( ! [X1] : ~ ra_Px92(X0,X1)
| cC26(X0) ) ),
inference(rectify,[],[f705]) ).
fof(f707,plain,
! [X0] :
( ( ~ cC26(X0)
| ra_Px92(X0,sK70(X0)) )
& ( ! [X1] : ~ ra_Px92(X0,X1)
| cC26(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70]),skolemize(X2,sK70(X0))],[f706]) ).
fof(f708,plain,
! [X0] :
( ( ~ cC26(X0)
| ( cC2xcomp(X0)
& cC24xcomp(X0) ) )
& ( ~ cC2xcomp(X0)
| ~ cC24xcomp(X0)
| cC26(X0) ) ),
inference(nnf_transformation,[],[f106]) ).
fof(f709,plain,
! [X0] :
( ( ~ cC26(X0)
| ( cC2xcomp(X0)
& cC24xcomp(X0) ) )
& ( ~ cC2xcomp(X0)
| ~ cC24xcomp(X0)
| cC26(X0) ) ),
inference(flattening,[],[f708]) ).
fof(f719,plain,
! [X0] :
( ( ~ cC30(X0)
| ? [X1] : ra_Px8(X0,X1) )
& ( ! [X1] : ~ ra_Px8(X0,X1)
| cC30(X0) ) ),
inference(nnf_transformation,[],[f111]) ).
fof(f720,plain,
! [X0] :
( ( ~ cC30(X0)
| ? [X2] : ra_Px8(X0,X2) )
& ( ! [X1] : ~ ra_Px8(X0,X1)
| cC30(X0) ) ),
inference(rectify,[],[f719]) ).
fof(f721,plain,
! [X0] :
( ( ~ cC30(X0)
| ra_Px8(X0,sK74(X0)) )
& ( ! [X1] : ~ ra_Px8(X0,X1)
| cC30(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK74]),skolemize(X2,sK74(X0))],[f720]) ).
fof(f725,plain,
! [X0] :
( ( ~ cC30xcomp(X0)
| ! [X1] : ~ ra_Px8(X0,X1) )
& ( ? [X1] : ra_Px8(X0,X1)
| cC30xcomp(X0) ) ),
inference(nnf_transformation,[],[f405]) ).
fof(f726,plain,
! [X0] :
( ( ~ cC30xcomp(X0)
| ! [X2] : ~ ra_Px8(X0,X2) )
& ( ? [X1] : ra_Px8(X0,X1)
| cC30xcomp(X0) ) ),
inference(rectify,[],[f725]) ).
fof(f727,plain,
! [X0] :
( ( ~ cC30xcomp(X0)
| ! [X2] : ~ ra_Px8(X0,X2) )
& ( ra_Px8(X0,sK76(X0))
| cC30xcomp(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK76]),skolemize(X1,sK76(X0))],[f726]) ).
fof(f728,plain,
! [X0] :
( ( ~ cC32(X0)
| ! [X1] : ~ ra_Px91(X0,X1) )
& ( ? [X1] : ra_Px91(X0,X1)
| cC32(X0) ) ),
inference(nnf_transformation,[],[f406]) ).
fof(f729,plain,
! [X0] :
( ( ~ cC32(X0)
| ! [X2] : ~ ra_Px91(X0,X2) )
& ( ? [X1] : ra_Px91(X0,X1)
| cC32(X0) ) ),
inference(rectify,[],[f728]) ).
fof(f730,plain,
! [X0] :
( ( ~ cC32(X0)
| ! [X2] : ~ ra_Px91(X0,X2) )
& ( ra_Px91(X0,sK77(X0))
| cC32(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK77]),skolemize(X1,sK77(X0))],[f729]) ).
fof(f731,plain,
! [X0] :
( ( ~ cC32(X0)
| ( cC30xcomp(X0)
& cC2xcomp(X0) ) )
& ( ~ cC30xcomp(X0)
| ~ cC2xcomp(X0)
| cC32(X0) ) ),
inference(nnf_transformation,[],[f115]) ).
fof(f732,plain,
! [X0] :
( ( ~ cC32(X0)
| ( cC30xcomp(X0)
& cC2xcomp(X0) ) )
& ( ~ cC30xcomp(X0)
| ~ cC2xcomp(X0)
| cC32(X0) ) ),
inference(flattening,[],[f731]) ).
fof(f733,plain,
! [X0] :
( ~ cC32xcomp(X0)
| ra_Px91(X0,sK78(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK78]),skolemize(X1,sK78(X0))],[f407]) ).
fof(f745,plain,
! [X0] :
( ( ~ cC38(X0)
| ( cTOP(X0)
& cC36(X0) ) )
& ( ~ cTOP(X0)
| ~ cC36(X0)
| cC38(X0) ) ),
inference(nnf_transformation,[],[f121]) ).
fof(f746,plain,
! [X0] :
( ( ~ cC38(X0)
| ( cTOP(X0)
& cC36(X0) ) )
& ( ~ cTOP(X0)
| ~ cC36(X0)
| cC38(X0) ) ),
inference(flattening,[],[f745]) ).
fof(f750,plain,
! [X0] :
( ( ~ cC40(X0)
| cTOP(X0) )
& ( ~ cTOP(X0)
| cC40(X0) ) ),
inference(nnf_transformation,[],[f123]) ).
fof(f751,plain,
! [X0] :
( ( ~ cC42(X0)
| ( cC38(X0)
& cC40(X0) ) )
& ( ~ cC38(X0)
| ~ cC40(X0)
| cC42(X0) ) ),
inference(nnf_transformation,[],[f124]) ).
fof(f752,plain,
! [X0] :
( ( ~ cC42(X0)
| ( cC38(X0)
& cC40(X0) ) )
& ( ~ cC38(X0)
| ~ cC40(X0)
| cC42(X0) ) ),
inference(flattening,[],[f751]) ).
fof(f753,plain,
! [X0] :
( ( ~ cC44(X0)
| ! [X1] : ~ ra_Px13(X0,X1) )
& ( ? [X1] : ra_Px13(X0,X1)
| cC44(X0) ) ),
inference(nnf_transformation,[],[f409]) ).
fof(f754,plain,
! [X0] :
( ( ~ cC44(X0)
| ! [X2] : ~ ra_Px13(X0,X2) )
& ( ? [X1] : ra_Px13(X0,X1)
| cC44(X0) ) ),
inference(rectify,[],[f753]) ).
fof(f755,plain,
! [X0] :
( ( ~ cC44(X0)
| ! [X2] : ~ ra_Px13(X0,X2) )
& ( ra_Px13(X0,sK83(X0))
| cC44(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK83]),skolemize(X1,sK83(X0))],[f754]) ).
fof(f759,plain,
! [X0] :
( ( ~ cC44xcomp(X0)
| ? [X1] : ra_Px13(X0,X1) )
& ( ! [X1] : ~ ra_Px13(X0,X1)
| cC44xcomp(X0) ) ),
inference(nnf_transformation,[],[f127]) ).
fof(f760,plain,
! [X0] :
( ( ~ cC44xcomp(X0)
| ? [X2] : ra_Px13(X0,X2) )
& ( ! [X1] : ~ ra_Px13(X0,X1)
| cC44xcomp(X0) ) ),
inference(rectify,[],[f759]) ).
fof(f761,plain,
! [X0] :
( ( ~ cC44xcomp(X0)
| ra_Px13(X0,sK85(X0)) )
& ( ! [X1] : ~ ra_Px13(X0,X1)
| cC44xcomp(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK85]),skolemize(X2,sK85(X0))],[f760]) ).
fof(f762,plain,
! [X0] :
( ( ~ cC46(X0)
| ? [X1] : ra_Px90(X0,X1) )
& ( ! [X1] : ~ ra_Px90(X0,X1)
| cC46(X0) ) ),
inference(nnf_transformation,[],[f128]) ).
fof(f763,plain,
! [X0] :
( ( ~ cC46(X0)
| ? [X2] : ra_Px90(X0,X2) )
& ( ! [X1] : ~ ra_Px90(X0,X1)
| cC46(X0) ) ),
inference(rectify,[],[f762]) ).
fof(f764,plain,
! [X0] :
( ( ~ cC46(X0)
| ra_Px90(X0,sK86(X0)) )
& ( ! [X1] : ~ ra_Px90(X0,X1)
| cC46(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK86]),skolemize(X2,sK86(X0))],[f763]) ).
fof(f765,plain,
! [X0] :
( ( ~ cC46(X0)
| ( cC12xcomp(X0)
& cC44xcomp(X0) ) )
& ( ~ cC12xcomp(X0)
| ~ cC44xcomp(X0)
| cC46(X0) ) ),
inference(nnf_transformation,[],[f129]) ).
fof(f766,plain,
! [X0] :
( ( ~ cC46(X0)
| ( cC12xcomp(X0)
& cC44xcomp(X0) ) )
& ( ~ cC12xcomp(X0)
| ~ cC44xcomp(X0)
| cC46(X0) ) ),
inference(flattening,[],[f765]) ).
fof(f779,plain,
! [X0] :
( ( ~ cC50(X0)
| ! [X1] : ~ ra_Px16(X0,X1) )
& ( ? [X1] : ra_Px16(X0,X1)
| cC50(X0) ) ),
inference(nnf_transformation,[],[f412]) ).
fof(f780,plain,
! [X0] :
( ( ~ cC50(X0)
| ! [X2] : ~ ra_Px16(X0,X2) )
& ( ? [X1] : ra_Px16(X0,X1)
| cC50(X0) ) ),
inference(rectify,[],[f779]) ).
fof(f781,plain,
! [X0] :
( ( ~ cC50(X0)
| ! [X2] : ~ ra_Px16(X0,X2) )
& ( ra_Px16(X0,sK91(X0))
| cC50(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK91]),skolemize(X1,sK91(X0))],[f780]) ).
fof(f782,plain,
! [X0] :
( ( ~ cC50xcomp(X0)
| ? [X1] : ra_Px16(X0,X1) )
& ( ! [X1] : ~ ra_Px16(X0,X1)
| cC50xcomp(X0) ) ),
inference(nnf_transformation,[],[f136]) ).
fof(f783,plain,
! [X0] :
( ( ~ cC50xcomp(X0)
| ? [X2] : ra_Px16(X0,X2) )
& ( ! [X1] : ~ ra_Px16(X0,X1)
| cC50xcomp(X0) ) ),
inference(rectify,[],[f782]) ).
fof(f784,plain,
! [X0] :
( ( ~ cC50xcomp(X0)
| ra_Px16(X0,sK92(X0)) )
& ( ! [X1] : ~ ra_Px16(X0,X1)
| cC50xcomp(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK92]),skolemize(X2,sK92(X0))],[f783]) ).
fof(f785,plain,
! [X0] :
( ( ~ cC52(X0)
| ? [X1] : ra_Px89(X0,X1) )
& ( ! [X1] : ~ ra_Px89(X0,X1)
| cC52(X0) ) ),
inference(nnf_transformation,[],[f137]) ).
fof(f786,plain,
! [X0] :
( ( ~ cC52(X0)
| ? [X2] : ra_Px89(X0,X2) )
& ( ! [X1] : ~ ra_Px89(X0,X1)
| cC52(X0) ) ),
inference(rectify,[],[f785]) ).
fof(f787,plain,
! [X0] :
( ( ~ cC52(X0)
| ra_Px89(X0,sK93(X0)) )
& ( ! [X1] : ~ ra_Px89(X0,X1)
| cC52(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK93]),skolemize(X2,sK93(X0))],[f786]) ).
fof(f788,plain,
! [X0] :
( ( ~ cC52(X0)
| ( cC12xcomp(X0)
& cC50xcomp(X0) ) )
& ( ~ cC12xcomp(X0)
| ~ cC50xcomp(X0)
| cC52(X0) ) ),
inference(nnf_transformation,[],[f138]) ).
fof(f789,plain,
! [X0] :
( ( ~ cC52(X0)
| ( cC12xcomp(X0)
& cC50xcomp(X0) ) )
& ( ~ cC12xcomp(X0)
| ~ cC50xcomp(X0)
| cC52(X0) ) ),
inference(flattening,[],[f788]) ).
fof(f801,plain,
! [X0] :
( ( ~ cC58(X0)
| ( cTOP(X0)
& cC56(X0) ) )
& ( ~ cTOP(X0)
| ~ cC56(X0)
| cC58(X0) ) ),
inference(nnf_transformation,[],[f144]) ).
fof(f802,plain,
! [X0] :
( ( ~ cC58(X0)
| ( cTOP(X0)
& cC56(X0) ) )
& ( ~ cTOP(X0)
| ~ cC56(X0)
| cC58(X0) ) ),
inference(flattening,[],[f801]) ).
fof(f807,plain,
! [X0] :
( ( ~ cC60(X0)
| ( cC42(X0)
& cC58(X0) ) )
& ( ~ cC42(X0)
| ~ cC58(X0)
| cC60(X0) ) ),
inference(nnf_transformation,[],[f147]) ).
fof(f808,plain,
! [X0] :
( ( ~ cC60(X0)
| ( cC42(X0)
& cC58(X0) ) )
& ( ~ cC42(X0)
| ~ cC58(X0)
| cC60(X0) ) ),
inference(flattening,[],[f807]) ).
fof(f809,plain,
! [X0] :
( ( ~ cC62(X0)
| cTOP(X0) )
& ( ~ cTOP(X0)
| cC62(X0) ) ),
inference(nnf_transformation,[],[f148]) ).
fof(f810,plain,
! [X0] :
( ( ~ cC64(X0)
| ( cC62(X0)
& cC60(X0) ) )
& ( ~ cC62(X0)
| ~ cC60(X0)
| cC64(X0) ) ),
inference(nnf_transformation,[],[f149]) ).
fof(f811,plain,
! [X0] :
( ( ~ cC64(X0)
| ( cC62(X0)
& cC60(X0) ) )
& ( ~ cC62(X0)
| ~ cC60(X0)
| cC64(X0) ) ),
inference(flattening,[],[f810]) ).
fof(f812,plain,
! [X0] :
( ( ~ cC66(X0)
| ? [X1] : ra_Px21(X0,X1) )
& ( ! [X1] : ~ ra_Px21(X0,X1)
| cC66(X0) ) ),
inference(nnf_transformation,[],[f150]) ).
fof(f813,plain,
! [X0] :
( ( ~ cC66(X0)
| ? [X2] : ra_Px21(X0,X2) )
& ( ! [X1] : ~ ra_Px21(X0,X1)
| cC66(X0) ) ),
inference(rectify,[],[f812]) ).
fof(f814,plain,
! [X0] :
( ( ~ cC66(X0)
| ra_Px21(X0,sK99(X0)) )
& ( ! [X1] : ~ ra_Px21(X0,X1)
| cC66(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK99]),skolemize(X2,sK99(X0))],[f813]) ).
fof(f818,plain,
! [X0] :
( ( ~ cC66xcomp(X0)
| ! [X1] : ~ ra_Px21(X0,X1) )
& ( ? [X1] : ra_Px21(X0,X1)
| cC66xcomp(X0) ) ),
inference(nnf_transformation,[],[f417]) ).
fof(f819,plain,
! [X0] :
( ( ~ cC66xcomp(X0)
| ! [X2] : ~ ra_Px21(X0,X2) )
& ( ? [X1] : ra_Px21(X0,X1)
| cC66xcomp(X0) ) ),
inference(rectify,[],[f818]) ).
fof(f820,plain,
! [X0] :
( ( ~ cC66xcomp(X0)
| ! [X2] : ~ ra_Px21(X0,X2) )
& ( ra_Px21(X0,sK101(X0))
| cC66xcomp(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK101]),skolemize(X1,sK101(X0))],[f819]) ).
fof(f821,plain,
! [X0] :
( ( ~ cC68(X0)
| ! [X1] : ~ ra_Px88(X0,X1) )
& ( ? [X1] : ra_Px88(X0,X1)
| cC68(X0) ) ),
inference(nnf_transformation,[],[f418]) ).
fof(f822,plain,
! [X0] :
( ( ~ cC68(X0)
| ! [X2] : ~ ra_Px88(X0,X2) )
& ( ? [X1] : ra_Px88(X0,X1)
| cC68(X0) ) ),
inference(rectify,[],[f821]) ).
fof(f823,plain,
! [X0] :
( ( ~ cC68(X0)
| ! [X2] : ~ ra_Px88(X0,X2) )
& ( ra_Px88(X0,sK102(X0))
| cC68(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK102]),skolemize(X1,sK102(X0))],[f822]) ).
fof(f824,plain,
! [X0] :
( ( ~ cC68(X0)
| ( cC66xcomp(X0)
& cC18xcomp(X0) ) )
& ( ~ cC66xcomp(X0)
| ~ cC18xcomp(X0)
| cC68(X0) ) ),
inference(nnf_transformation,[],[f154]) ).
fof(f825,plain,
! [X0] :
( ( ~ cC68(X0)
| ( cC66xcomp(X0)
& cC18xcomp(X0) ) )
& ( ~ cC66xcomp(X0)
| ~ cC18xcomp(X0)
| cC68(X0) ) ),
inference(flattening,[],[f824]) ).
fof(f826,plain,
! [X0] :
( ~ cC68xcomp(X0)
| ra_Px88(X0,sK103(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK103]),skolemize(X1,sK103(X0))],[f419]) ).
fof(f836,plain,
! [X0] :
( ( ~ cC72(X0)
| ? [X1] : ra_Px24(X0,X1) )
& ( ! [X1] : ~ ra_Px24(X0,X1)
| cC72(X0) ) ),
inference(nnf_transformation,[],[f159]) ).
fof(f837,plain,
! [X0] :
( ( ~ cC72(X0)
| ? [X2] : ra_Px24(X0,X2) )
& ( ! [X1] : ~ ra_Px24(X0,X1)
| cC72(X0) ) ),
inference(rectify,[],[f836]) ).
fof(f838,plain,
! [X0] :
( ( ~ cC72(X0)
| ra_Px24(X0,sK107(X0)) )
& ( ! [X1] : ~ ra_Px24(X0,X1)
| cC72(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK107]),skolemize(X2,sK107(X0))],[f837]) ).
fof(f842,plain,
! [X0] :
( ( ~ cC72xcomp(X0)
| ! [X1] : ~ ra_Px24(X0,X1) )
& ( ? [X1] : ra_Px24(X0,X1)
| cC72xcomp(X0) ) ),
inference(nnf_transformation,[],[f421]) ).
fof(f843,plain,
! [X0] :
( ( ~ cC72xcomp(X0)
| ! [X2] : ~ ra_Px24(X0,X2) )
& ( ? [X1] : ra_Px24(X0,X1)
| cC72xcomp(X0) ) ),
inference(rectify,[],[f842]) ).
fof(f844,plain,
! [X0] :
( ( ~ cC72xcomp(X0)
| ! [X2] : ~ ra_Px24(X0,X2) )
& ( ra_Px24(X0,sK109(X0))
| cC72xcomp(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK109]),skolemize(X1,sK109(X0))],[f843]) ).
fof(f845,plain,
! [X0] :
( ( ~ cC74(X0)
| ( cC18xcomp(X0)
& cC72xcomp(X0) ) )
& ( ~ cC18xcomp(X0)
| ~ cC72xcomp(X0)
| cC74(X0) ) ),
inference(nnf_transformation,[],[f162]) ).
fof(f846,plain,
! [X0] :
( ( ~ cC74(X0)
| ( cC18xcomp(X0)
& cC72xcomp(X0) ) )
& ( ~ cC18xcomp(X0)
| ~ cC72xcomp(X0)
| cC74(X0) ) ),
inference(flattening,[],[f845]) ).
fof(f847,plain,
! [X0] :
( ( ~ cC74(X0)
| ? [X1] : ra_Px87(X0,X1) )
& ( ! [X1] : ~ ra_Px87(X0,X1)
| cC74(X0) ) ),
inference(nnf_transformation,[],[f163]) ).
fof(f848,plain,
! [X0] :
( ( ~ cC74(X0)
| ? [X2] : ra_Px87(X0,X2) )
& ( ! [X1] : ~ ra_Px87(X0,X1)
| cC74(X0) ) ),
inference(rectify,[],[f847]) ).
fof(f849,plain,
! [X0] :
( ( ~ cC74(X0)
| ra_Px87(X0,sK110(X0)) )
& ( ! [X1] : ~ ra_Px87(X0,X1)
| cC74(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK110]),skolemize(X2,sK110(X0))],[f848]) ).
fof(f864,plain,
! [X0] :
( ( ~ cC80(X0)
| ( cTOP(X0)
& cC78(X0) ) )
& ( ~ cTOP(X0)
| ~ cC78(X0)
| cC80(X0) ) ),
inference(nnf_transformation,[],[f170]) ).
fof(f865,plain,
! [X0] :
( ( ~ cC80(X0)
| ( cTOP(X0)
& cC78(X0) ) )
& ( ~ cTOP(X0)
| ~ cC78(X0)
| cC80(X0) ) ),
inference(flattening,[],[f864]) ).
fof(f866,plain,
! [X0] :
( ( ~ cC82(X0)
| ( cC80(X0)
& cC64(X0) ) )
& ( ~ cC80(X0)
| ~ cC64(X0)
| cC82(X0) ) ),
inference(nnf_transformation,[],[f171]) ).
fof(f867,plain,
! [X0] :
( ( ~ cC82(X0)
| ( cC80(X0)
& cC64(X0) ) )
& ( ~ cC80(X0)
| ~ cC64(X0)
| cC82(X0) ) ),
inference(flattening,[],[f866]) ).
fof(f868,plain,
! [X0] :
( ( ~ cC84(X0)
| cTOP(X0) )
& ( ~ cTOP(X0)
| cC84(X0) ) ),
inference(nnf_transformation,[],[f172]) ).
fof(f869,plain,
! [X0] :
( ( ~ cC86(X0)
| ( cC84(X0)
& cC82(X0) ) )
& ( ~ cC84(X0)
| ~ cC82(X0)
| cC86(X0) ) ),
inference(nnf_transformation,[],[f173]) ).
fof(f870,plain,
! [X0] :
( ( ~ cC86(X0)
| ( cC84(X0)
& cC82(X0) ) )
& ( ~ cC84(X0)
| ~ cC82(X0)
| cC86(X0) ) ),
inference(flattening,[],[f869]) ).
fof(f871,plain,
! [X0] :
( ( ~ cC88(X0)
| cTOP(X0) )
& ( ~ cTOP(X0)
| cC88(X0) ) ),
inference(nnf_transformation,[],[f174]) ).
fof(f872,plain,
! [X0] :
( ( ~ cC90(X0)
| ( cC88(X0)
& cC86(X0) ) )
& ( ~ cC88(X0)
| ~ cC86(X0)
| cC90(X0) ) ),
inference(nnf_transformation,[],[f175]) ).
fof(f873,plain,
! [X0] :
( ( ~ cC90(X0)
| ( cC88(X0)
& cC86(X0) ) )
& ( ~ cC88(X0)
| ~ cC86(X0)
| cC90(X0) ) ),
inference(flattening,[],[f872]) ).
fof(f900,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)
| ? [X1] :
( ( xsd_string(X1)
| ~ xsd_integer(X1) )
& ( ~ xsd_string(X1)
| xsd_integer(X1) ) )
| ? [X0] :
( cowlNothing(X0)
| ~ cowlThing(X0) ) ),
inference(nnf_transformation,[],[f457]) ).
fof(f901,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_string(sK124)
| ~ xsd_integer(sK124) )
& ( ~ xsd_string(sK124)
| xsd_integer(sK124) ) )
| cowlNothing(sK123)
| ~ cowlThing(sK123) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK123,sK124]),skolemize(X0,sK123),skolemize(X1,sK124)],[f900]) ).
fof(f902,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f903,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f904,plain,
! [X0] :
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(cnf_transformation,[],[f458]) ).
fof(f905,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f458]) ).
fof(f906,plain,
! [X0] :
( ~ cC10(X0)
| cC4(X0) ),
inference(cnf_transformation,[],[f460]) ).
fof(f907,plain,
! [X0] :
( ~ cC10(X0)
| cC8(X0) ),
inference(cnf_transformation,[],[f460]) ).
fof(f936,plain,
! [X0] :
( ~ cC110(X0)
| cC108(X0) ),
inference(cnf_transformation,[],[f492]) ).
fof(f938,plain,
! [X0] :
( ~ cC112(X0)
| cC90(X0) ),
inference(cnf_transformation,[],[f494]) ).
fof(f939,plain,
! [X0] :
( ~ cC112(X0)
| cC110(X0) ),
inference(cnf_transformation,[],[f494]) ).
fof(f943,plain,
! [X0] :
( ~ cC116(X0)
| cC112(X0) ),
inference(cnf_transformation,[],[f497]) ).
fof(f944,plain,
! [X0] :
( ~ cC116(X0)
| cC114(X0) ),
inference(cnf_transformation,[],[f497]) ).
fof(f993,plain,
! [X0] :
( ~ cC132(X0)
| cC130(X0) ),
inference(cnf_transformation,[],[f550]) ).
fof(f995,plain,
! [X0] :
( ~ cC134(X0)
| cC132(X0) ),
inference(cnf_transformation,[],[f552]) ).
fof(f996,plain,
! [X0] :
( ~ cC134(X0)
| cC116(X0) ),
inference(cnf_transformation,[],[f552]) ).
fof(f1000,plain,
! [X0] :
( ~ cC138(X0)
| cC134(X0) ),
inference(cnf_transformation,[],[f555]) ).
fof(f1001,plain,
! [X0] :
( ~ cC138(X0)
| cC136(X0) ),
inference(cnf_transformation,[],[f555]) ).
fof(f1050,plain,
! [X0] :
( ~ cC154(X0)
| cC152(X0) ),
inference(cnf_transformation,[],[f609]) ).
fof(f1052,plain,
! [X0] :
( ~ cC156(X0)
| cC138(X0) ),
inference(cnf_transformation,[],[f611]) ).
fof(f1053,plain,
! [X0] :
( ~ cC156(X0)
| cC154(X0) ),
inference(cnf_transformation,[],[f611]) ).
fof(f1055,plain,
! [X0] :
( ~ cC158(X0)
| cC156(X0) ),
inference(cnf_transformation,[],[f613]) ).
fof(f1056,plain,
! [X0] :
( ~ cC158(X0)
| cC22(X0) ),
inference(cnf_transformation,[],[f613]) ).
fof(f1058,plain,
! [X0] :
( ~ cC16(X0)
| cC14(X0) ),
inference(cnf_transformation,[],[f615]) ).
fof(f1059,plain,
! [X0] :
( ~ cC16(X0)
| cC10(X0) ),
inference(cnf_transformation,[],[f615]) ).
fof(f1103,plain,
! [X0] :
( ~ cC174(X0)
| cC168(X0) ),
inference(cnf_transformation,[],[f665]) ).
fof(f1123,plain,
! [X0] :
( ~ cC180(X0)
| cC174(X0) ),
inference(cnf_transformation,[],[f686]) ).
fof(f1131,plain,
! [X0] :
( ~ cC22(X0)
| cC16(X0) ),
inference(cnf_transformation,[],[f695]) ).
fof(f1132,plain,
! [X0] :
( ~ cC22(X0)
| cC20(X0) ),
inference(cnf_transformation,[],[f695]) ).
fof(f1135,plain,
! [X0,X1] :
( ~ ra_Px5(X0,X1)
| cC24(X0) ),
inference(cnf_transformation,[],[f698]) ).
fof(f1140,plain,
! [X0] :
( ra_Px5(X0,sK69(X0))
| cC24xcomp(X0) ),
inference(cnf_transformation,[],[f704]) ).
fof(f1141,plain,
! [X0] :
( ~ cC26(X0)
| ra_Px92(X0,sK70(X0)) ),
inference(cnf_transformation,[],[f707]) ).
fof(f1145,plain,
! [X0] :
( ~ cC2xcomp(X0)
| ~ cC24xcomp(X0)
| cC26(X0) ),
inference(cnf_transformation,[],[f709]) ).
fof(f1146,plain,
! [X0,X1] :
( ~ cC26xcomp(X0)
| ~ ra_Px92(X0,X1) ),
inference(cnf_transformation,[],[f403]) ).
fof(f1155,plain,
! [X0,X1] :
( ~ ra_Px8(X0,X1)
| cC30(X0) ),
inference(cnf_transformation,[],[f721]) ).
fof(f1160,plain,
! [X0] :
( ra_Px8(X0,sK76(X0))
| cC30xcomp(X0) ),
inference(cnf_transformation,[],[f727]) ).
fof(f1161,plain,
! [X2,X0] :
( ~ cC32(X0)
| ~ ra_Px91(X0,X2) ),
inference(cnf_transformation,[],[f730]) ).
fof(f1165,plain,
! [X0] :
( ~ cC30xcomp(X0)
| ~ cC2xcomp(X0)
| cC32(X0) ),
inference(cnf_transformation,[],[f732]) ).
fof(f1166,plain,
! [X0] :
( ~ cC32xcomp(X0)
| ra_Px91(X0,sK78(X0)) ),
inference(cnf_transformation,[],[f733]) ).
fof(f1178,plain,
! [X0] :
( ~ cC38(X0)
| cC36(X0) ),
inference(cnf_transformation,[],[f746]) ).
fof(f1184,plain,
! [X0] :
( ~ cTOP(X0)
| cC40(X0) ),
inference(cnf_transformation,[],[f750]) ).
fof(f1185,plain,
! [X0] :
( ~ cC42(X0)
| cC38(X0) ),
inference(cnf_transformation,[],[f752]) ).
fof(f1189,plain,
! [X0] :
( ra_Px13(X0,sK83(X0))
| cC44(X0) ),
inference(cnf_transformation,[],[f755]) ).
fof(f1194,plain,
! [X0,X1] :
( ~ ra_Px13(X0,X1)
| cC44xcomp(X0) ),
inference(cnf_transformation,[],[f761]) ).
fof(f1195,plain,
! [X0] :
( ~ cC46(X0)
| ra_Px90(X0,sK86(X0)) ),
inference(cnf_transformation,[],[f764]) ).
fof(f1199,plain,
! [X0] :
( ~ cC12xcomp(X0)
| ~ cC44xcomp(X0)
| cC46(X0) ),
inference(cnf_transformation,[],[f766]) ).
fof(f1200,plain,
! [X0,X1] :
( ~ cC46xcomp(X0)
| ~ ra_Px90(X0,X1) ),
inference(cnf_transformation,[],[f410]) ).
fof(f1212,plain,
! [X0] :
( ra_Px16(X0,sK91(X0))
| cC50(X0) ),
inference(cnf_transformation,[],[f781]) ).
fof(f1214,plain,
! [X0,X1] :
( ~ ra_Px16(X0,X1)
| cC50xcomp(X0) ),
inference(cnf_transformation,[],[f784]) ).
fof(f1215,plain,
! [X0] :
( ~ cC52(X0)
| ra_Px89(X0,sK93(X0)) ),
inference(cnf_transformation,[],[f787]) ).
fof(f1219,plain,
! [X0] :
( ~ cC12xcomp(X0)
| ~ cC50xcomp(X0)
| cC52(X0) ),
inference(cnf_transformation,[],[f789]) ).
fof(f1220,plain,
! [X0,X1] :
( ~ cC52xcomp(X0)
| ~ ra_Px89(X0,X1) ),
inference(cnf_transformation,[],[f413]) ).
fof(f1232,plain,
! [X0] :
( ~ cC58(X0)
| cC56(X0) ),
inference(cnf_transformation,[],[f802]) ).
fof(f1237,plain,
! [X0] :
( ~ cC60(X0)
| cC42(X0) ),
inference(cnf_transformation,[],[f808]) ).
fof(f1238,plain,
! [X0] :
( ~ cC60(X0)
| cC58(X0) ),
inference(cnf_transformation,[],[f808]) ).
fof(f1241,plain,
! [X0] :
( ~ cTOP(X0)
| cC62(X0) ),
inference(cnf_transformation,[],[f809]) ).
fof(f1243,plain,
! [X0] :
( ~ cC64(X0)
| cC60(X0) ),
inference(cnf_transformation,[],[f811]) ).
fof(f1246,plain,
! [X0,X1] :
( ~ ra_Px21(X0,X1)
| cC66(X0) ),
inference(cnf_transformation,[],[f814]) ).
fof(f1251,plain,
! [X0] :
( ra_Px21(X0,sK101(X0))
| cC66xcomp(X0) ),
inference(cnf_transformation,[],[f820]) ).
fof(f1252,plain,
! [X2,X0] :
( ~ cC68(X0)
| ~ ra_Px88(X0,X2) ),
inference(cnf_transformation,[],[f823]) ).
fof(f1256,plain,
! [X0] :
( ~ cC66xcomp(X0)
| ~ cC18xcomp(X0)
| cC68(X0) ),
inference(cnf_transformation,[],[f825]) ).
fof(f1257,plain,
! [X0] :
( ~ cC68xcomp(X0)
| ra_Px88(X0,sK103(X0)) ),
inference(cnf_transformation,[],[f826]) ).
fof(f1266,plain,
! [X0,X1] :
( ~ ra_Px24(X0,X1)
| cC72(X0) ),
inference(cnf_transformation,[],[f838]) ).
fof(f1271,plain,
! [X0] :
( ra_Px24(X0,sK109(X0))
| cC72xcomp(X0) ),
inference(cnf_transformation,[],[f844]) ).
fof(f1274,plain,
! [X0] :
( ~ cC18xcomp(X0)
| ~ cC72xcomp(X0)
| cC74(X0) ),
inference(cnf_transformation,[],[f846]) ).
fof(f1275,plain,
! [X0] :
( ~ cC74(X0)
| ra_Px87(X0,sK110(X0)) ),
inference(cnf_transformation,[],[f849]) ).
fof(f1277,plain,
! [X0,X1] :
( ~ cC74xcomp(X0)
| ~ ra_Px87(X0,X1) ),
inference(cnf_transformation,[],[f422]) ).
fof(f1292,plain,
! [X0] :
( ~ cC80(X0)
| cC78(X0) ),
inference(cnf_transformation,[],[f865]) ).
fof(f1294,plain,
! [X0] :
( ~ cC82(X0)
| cC80(X0) ),
inference(cnf_transformation,[],[f867]) ).
fof(f1295,plain,
! [X0] :
( ~ cC82(X0)
| cC64(X0) ),
inference(cnf_transformation,[],[f867]) ).
fof(f1298,plain,
! [X0] :
( ~ cTOP(X0)
| cC84(X0) ),
inference(cnf_transformation,[],[f868]) ).
fof(f1300,plain,
! [X0] :
( ~ cC86(X0)
| cC82(X0) ),
inference(cnf_transformation,[],[f870]) ).
fof(f1303,plain,
! [X0] :
( ~ cTOP(X0)
| cC88(X0) ),
inference(cnf_transformation,[],[f871]) ).
fof(f1305,plain,
! [X0] :
( ~ cC90(X0)
| cC86(X0) ),
inference(cnf_transformation,[],[f873]) ).
fof(f1330,plain,
! [X0] :
( ~ cTEST(X0)
| cC180(X0) ),
inference(cnf_transformation,[],[f428]) ).
fof(f1331,plain,
! [X0] :
( ~ cTEST(X0)
| cC158(X0) ),
inference(cnf_transformation,[],[f428]) ).
fof(f1335,plain,
cTOP(iV21026),
inference(cnf_transformation,[],[f191]) ).
fof(f1364,plain,
cowlThing(iV21026),
inference(cnf_transformation,[],[f220]) ).
fof(f1366,plain,
cTEST(iV21026),
inference(cnf_transformation,[],[f222]) ).
fof(f1382,plain,
cC2xcomp(iV21027),
inference(cnf_transformation,[],[f238]) ).
fof(f1387,plain,
cC26xcomp(iV21027),
inference(cnf_transformation,[],[f243]) ).
fof(f1393,plain,
cowlThing(iV21027),
inference(cnf_transformation,[],[f249]) ).
fof(f1395,plain,
cC32xcomp(iV21027),
inference(cnf_transformation,[],[f251]) ).
fof(f1410,plain,
cC12xcomp(iV21029),
inference(cnf_transformation,[],[f266]) ).
fof(f1413,plain,
cC52xcomp(iV21029),
inference(cnf_transformation,[],[f269]) ).
fof(f1417,plain,
cC46xcomp(iV21029),
inference(cnf_transformation,[],[f273]) ).
fof(f1423,plain,
cowlThing(iV21029),
inference(cnf_transformation,[],[f279]) ).
fof(f1436,plain,
cC68xcomp(iV21030),
inference(cnf_transformation,[],[f292]) ).
fof(f1438,plain,
cC18xcomp(iV21030),
inference(cnf_transformation,[],[f294]) ).
fof(f1451,plain,
cowlThing(iV21030),
inference(cnf_transformation,[],[f307]) ).
fof(f1452,plain,
cC74xcomp(iV21030),
inference(cnf_transformation,[],[f308]) ).
fof(f1487,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_string(sK124)
| ~ xsd_integer(sK124)
| cowlNothing(sK123)
| ~ cowlThing(sK123) ),
inference(cnf_transformation,[],[f901]) ).
fof(f1488,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_string(sK124)
| xsd_integer(sK124)
| cowlNothing(sK123)
| ~ cowlThing(sK123) ),
inference(cnf_transformation,[],[f901]) ).
tcf(c_49,plain,
! [X0: $i] : cowlThing(X0),
inference(cnf_transformation,[],[f903]) ).
tcf(c_50,plain,
! [X0: $i] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f902]) ).
tcf(c_51,plain,
! [X0: $i] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f905]) ).
tcf(c_52,plain,
! [X0: $i] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[],[f904]) ).
tcf(c_54,plain,
! [X0: $i] :
( cC8(X0)
| ~ cC10(X0) ),
inference(cnf_transformation,[],[f907]) ).
tcf(c_55,plain,
! [X0: $i] :
( cC4(X0)
| ~ cC10(X0) ),
inference(cnf_transformation,[],[f906]) ).
tcf(c_83,plain,
! [X0: $i] :
( cC108(X0)
| ~ cC110(X0) ),
inference(cnf_transformation,[],[f936]) ).
tcf(c_86,plain,
! [X0: $i] :
( cC110(X0)
| ~ cC112(X0) ),
inference(cnf_transformation,[],[f939]) ).
tcf(c_87,plain,
! [X0: $i] :
( cC90(X0)
| ~ cC112(X0) ),
inference(cnf_transformation,[],[f938]) ).
tcf(c_91,plain,
! [X0: $i] :
( cC114(X0)
| ~ cC116(X0) ),
inference(cnf_transformation,[],[f944]) ).
tcf(c_92,plain,
! [X0: $i] :
( cC112(X0)
| ~ cC116(X0) ),
inference(cnf_transformation,[],[f943]) ).
tcf(c_140,plain,
! [X0: $i] :
( cC130(X0)
| ~ cC132(X0) ),
inference(cnf_transformation,[],[f993]) ).
tcf(c_143,plain,
! [X0: $i] :
( cC116(X0)
| ~ cC134(X0) ),
inference(cnf_transformation,[],[f996]) ).
tcf(c_144,plain,
! [X0: $i] :
( cC132(X0)
| ~ cC134(X0) ),
inference(cnf_transformation,[],[f995]) ).
tcf(c_148,plain,
! [X0: $i] :
( cC136(X0)
| ~ cC138(X0) ),
inference(cnf_transformation,[],[f1001]) ).
tcf(c_149,plain,
! [X0: $i] :
( cC134(X0)
| ~ cC138(X0) ),
inference(cnf_transformation,[],[f1000]) ).
tcf(c_197,plain,
! [X0: $i] :
( cC152(X0)
| ~ cC154(X0) ),
inference(cnf_transformation,[],[f1050]) ).
tcf(c_200,plain,
! [X0: $i] :
( cC154(X0)
| ~ cC156(X0) ),
inference(cnf_transformation,[],[f1053]) ).
tcf(c_201,plain,
! [X0: $i] :
( cC138(X0)
| ~ cC156(X0) ),
inference(cnf_transformation,[],[f1052]) ).
tcf(c_203,plain,
! [X0: $i] :
( cC22(X0)
| ~ cC158(X0) ),
inference(cnf_transformation,[],[f1056]) ).
tcf(c_204,plain,
! [X0: $i] :
( cC156(X0)
| ~ cC158(X0) ),
inference(cnf_transformation,[],[f1055]) ).
tcf(c_206,plain,
! [X0: $i] :
( cC10(X0)
| ~ cC16(X0) ),
inference(cnf_transformation,[],[f1059]) ).
tcf(c_207,plain,
! [X0: $i] :
( cC14(X0)
| ~ cC16(X0) ),
inference(cnf_transformation,[],[f1058]) ).
tcf(c_252,plain,
! [X0: $i] :
( cC168(X0)
| ~ cC174(X0) ),
inference(cnf_transformation,[],[f1103]) ).
tcf(c_270,plain,
! [X0: $i] :
( cC174(X0)
| ~ cC180(X0) ),
inference(cnf_transformation,[],[f1123]) ).
tcf(c_279,plain,
! [X0: $i] :
( cC20(X0)
| ~ cC22(X0) ),
inference(cnf_transformation,[],[f1132]) ).
tcf(c_280,plain,
! [X0: $i] :
( cC16(X0)
| ~ cC22(X0) ),
inference(cnf_transformation,[],[f1131]) ).
tcf(c_281,plain,
! [X0: $i,X1: $i] :
( cC24(X0)
| ~ ra_Px5(X0,X1) ),
inference(cnf_transformation,[],[f1135]) ).
tcf(c_286,plain,
! [X0: $i] :
( cC24xcomp(X0)
| ra_Px5(X0,sK69(X0)) ),
inference(cnf_transformation,[],[f1140]) ).
tcf(c_289,plain,
! [X0: $i] :
( ra_Px92(X0,sK70(X0))
| ~ cC26(X0) ),
inference(cnf_transformation,[],[f1141]) ).
tcf(c_290,plain,
! [X0: $i] :
( cC26(X0)
| ~ cC24xcomp(X0)
| ~ cC2xcomp(X0) ),
inference(cnf_transformation,[],[f1145]) ).
tcf(c_293,plain,
! [X0: $i,X1: $i] :
( ~ cC26xcomp(X0)
| ~ ra_Px92(X0,X1) ),
inference(cnf_transformation,[],[f1146]) ).
tcf(c_301,plain,
! [X0: $i,X1: $i] :
( cC30(X0)
| ~ ra_Px8(X0,X1) ),
inference(cnf_transformation,[],[f1155]) ).
tcf(c_306,plain,
! [X0: $i] :
( cC30xcomp(X0)
| ra_Px8(X0,sK76(X0)) ),
inference(cnf_transformation,[],[f1160]) ).
tcf(c_309,plain,
! [X0: $i,X1: $i] :
( ~ cC32(X0)
| ~ ra_Px91(X0,X1) ),
inference(cnf_transformation,[],[f1161]) ).
tcf(c_310,plain,
! [X0: $i] :
( cC32(X0)
| ~ cC30xcomp(X0)
| ~ cC2xcomp(X0) ),
inference(cnf_transformation,[],[f1165]) ).
tcf(c_313,plain,
! [X0: $i] :
( ra_Px91(X0,sK78(X0))
| ~ cC32xcomp(X0) ),
inference(cnf_transformation,[],[f1166]) ).
tcf(c_325,plain,
! [X0: $i] :
( cC36(X0)
| ~ cC38(X0) ),
inference(cnf_transformation,[],[f1178]) ).
tcf(c_330,plain,
! [X0: $i] :
( cC40(X0)
| ~ cTOP(X0) ),
inference(cnf_transformation,[],[f1184]) ).
tcf(c_334,plain,
! [X0: $i] :
( cC38(X0)
| ~ cC42(X0) ),
inference(cnf_transformation,[],[f1185]) ).
tcf(c_335,plain,
! [X0: $i] :
( cC44(X0)
| ra_Px13(X0,sK83(X0)) ),
inference(cnf_transformation,[],[f1189]) ).
tcf(c_340,plain,
! [X0: $i,X1: $i] :
( cC44xcomp(X0)
| ~ ra_Px13(X0,X1) ),
inference(cnf_transformation,[],[f1194]) ).
tcf(c_343,plain,
! [X0: $i] :
( ra_Px90(X0,sK86(X0))
| ~ cC46(X0) ),
inference(cnf_transformation,[],[f1195]) ).
tcf(c_344,plain,
! [X0: $i] :
( cC46(X0)
| ~ cC44xcomp(X0)
| ~ cC12xcomp(X0) ),
inference(cnf_transformation,[],[f1199]) ).
tcf(c_347,plain,
! [X0: $i,X1: $i] :
( ~ cC46xcomp(X0)
| ~ ra_Px90(X0,X1) ),
inference(cnf_transformation,[],[f1200]) ).
tcf(c_358,plain,
! [X0: $i] :
( cC50(X0)
| ra_Px16(X0,sK91(X0)) ),
inference(cnf_transformation,[],[f1212]) ).
tcf(c_360,plain,
! [X0: $i,X1: $i] :
( cC50xcomp(X0)
| ~ ra_Px16(X0,X1) ),
inference(cnf_transformation,[],[f1214]) ).
tcf(c_363,plain,
! [X0: $i] :
( ra_Px89(X0,sK93(X0))
| ~ cC52(X0) ),
inference(cnf_transformation,[],[f1215]) ).
tcf(c_364,plain,
! [X0: $i] :
( cC52(X0)
| ~ cC50xcomp(X0)
| ~ cC12xcomp(X0) ),
inference(cnf_transformation,[],[f1219]) ).
tcf(c_367,plain,
! [X0: $i,X1: $i] :
( ~ cC52xcomp(X0)
| ~ ra_Px89(X0,X1) ),
inference(cnf_transformation,[],[f1220]) ).
tcf(c_379,plain,
! [X0: $i] :
( cC56(X0)
| ~ cC58(X0) ),
inference(cnf_transformation,[],[f1232]) ).
tcf(c_385,plain,
! [X0: $i] :
( cC58(X0)
| ~ cC60(X0) ),
inference(cnf_transformation,[],[f1238]) ).
tcf(c_386,plain,
! [X0: $i] :
( cC42(X0)
| ~ cC60(X0) ),
inference(cnf_transformation,[],[f1237]) ).
tcf(c_387,plain,
! [X0: $i] :
( cC62(X0)
| ~ cTOP(X0) ),
inference(cnf_transformation,[],[f1241]) ).
tcf(c_390,plain,
! [X0: $i] :
( cC60(X0)
| ~ cC64(X0) ),
inference(cnf_transformation,[],[f1243]) ).
tcf(c_392,plain,
! [X0: $i,X1: $i] :
( cC66(X0)
| ~ ra_Px21(X0,X1) ),
inference(cnf_transformation,[],[f1246]) ).
tcf(c_397,plain,
! [X0: $i] :
( cC66xcomp(X0)
| ra_Px21(X0,sK101(X0)) ),
inference(cnf_transformation,[],[f1251]) ).
tcf(c_400,plain,
! [X0: $i,X1: $i] :
( ~ cC68(X0)
| ~ ra_Px88(X0,X1) ),
inference(cnf_transformation,[],[f1252]) ).
tcf(c_401,plain,
! [X0: $i] :
( cC68(X0)
| ~ cC66xcomp(X0)
| ~ cC18xcomp(X0) ),
inference(cnf_transformation,[],[f1256]) ).
tcf(c_404,plain,
! [X0: $i] :
( ra_Px88(X0,sK103(X0))
| ~ cC68xcomp(X0) ),
inference(cnf_transformation,[],[f1257]) ).
tcf(c_412,plain,
! [X0: $i,X1: $i] :
( cC72(X0)
| ~ ra_Px24(X0,X1) ),
inference(cnf_transformation,[],[f1266]) ).
tcf(c_417,plain,
! [X0: $i] :
( cC72xcomp(X0)
| ra_Px24(X0,sK109(X0)) ),
inference(cnf_transformation,[],[f1271]) ).
tcf(c_419,plain,
! [X0: $i] :
( cC74(X0)
| ~ cC72xcomp(X0)
| ~ cC18xcomp(X0) ),
inference(cnf_transformation,[],[f1274]) ).
tcf(c_423,plain,
! [X0: $i] :
( ra_Px87(X0,sK110(X0))
| ~ cC74(X0) ),
inference(cnf_transformation,[],[f1275]) ).
tcf(c_424,plain,
! [X0: $i,X1: $i] :
( ~ cC74xcomp(X0)
| ~ ra_Px87(X0,X1) ),
inference(cnf_transformation,[],[f1277]) ).
tcf(c_439,plain,
! [X0: $i] :
( cC78(X0)
| ~ cC80(X0) ),
inference(cnf_transformation,[],[f1292]) ).
tcf(c_442,plain,
! [X0: $i] :
( cC64(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[],[f1295]) ).
tcf(c_443,plain,
! [X0: $i] :
( cC80(X0)
| ~ cC82(X0) ),
inference(cnf_transformation,[],[f1294]) ).
tcf(c_444,plain,
! [X0: $i] :
( cC84(X0)
| ~ cTOP(X0) ),
inference(cnf_transformation,[],[f1298]) ).
tcf(c_447,plain,
! [X0: $i] :
( cC82(X0)
| ~ cC86(X0) ),
inference(cnf_transformation,[],[f1300]) ).
tcf(c_449,plain,
! [X0: $i] :
( cC88(X0)
| ~ cTOP(X0) ),
inference(cnf_transformation,[],[f1303]) ).
tcf(c_452,plain,
! [X0: $i] :
( cC86(X0)
| ~ cC90(X0) ),
inference(cnf_transformation,[],[f1305]) ).
tcf(c_477,plain,
! [X0: $i] :
( cC158(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[],[f1331]) ).
tcf(c_478,plain,
! [X0: $i] :
( cC180(X0)
| ~ cTEST(X0) ),
inference(cnf_transformation,[],[f1330]) ).
tcf(c_482,plain,
cTOP(iV21026),
inference(cnf_transformation,[],[f1335]) ).
tcf(c_511,plain,
cowlThing(iV21026),
inference(cnf_transformation,[],[f1364]) ).
tcf(c_513,plain,
cTEST(iV21026),
inference(cnf_transformation,[],[f1366]) ).
tcf(c_529,plain,
cC2xcomp(iV21027),
inference(cnf_transformation,[],[f1382]) ).
tcf(c_534,plain,
cC26xcomp(iV21027),
inference(cnf_transformation,[],[f1387]) ).
tcf(c_540,plain,
cowlThing(iV21027),
inference(cnf_transformation,[],[f1393]) ).
tcf(c_542,plain,
cC32xcomp(iV21027),
inference(cnf_transformation,[],[f1395]) ).
tcf(c_557,plain,
cC12xcomp(iV21029),
inference(cnf_transformation,[],[f1410]) ).
tcf(c_560,plain,
cC52xcomp(iV21029),
inference(cnf_transformation,[],[f1413]) ).
tcf(c_564,plain,
cC46xcomp(iV21029),
inference(cnf_transformation,[],[f1417]) ).
tcf(c_570,plain,
cowlThing(iV21029),
inference(cnf_transformation,[],[f1423]) ).
tcf(c_583,plain,
cC68xcomp(iV21030),
inference(cnf_transformation,[],[f1436]) ).
tcf(c_585,plain,
cC18xcomp(iV21030),
inference(cnf_transformation,[],[f1438]) ).
tcf(c_598,plain,
cowlThing(iV21030),
inference(cnf_transformation,[],[f1451]) ).
tcf(c_599,plain,
cC74xcomp(iV21030),
inference(cnf_transformation,[],[f1452]) ).
tcf(c_634,negated_conjecture,
( xsd_integer(sK124)
| cowlNothing(sK123)
| ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC136(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC114(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ xsd_string(sK124)
| ~ cowlThing(sK123)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030)
| ~ cowlThing(iV21026) ),
inference(cnf_transformation,[],[f1488]) ).
tcf(c_635,negated_conjecture,
( xsd_string(sK124)
| cowlNothing(sK123)
| ~ cC88(iV21026)
| ~ cC86(iV21026)
| ~ cC84(iV21026)
| ~ cC82(iV21026)
| ~ cC80(iV21026)
| ~ cC78(iV21026)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC64(iV21026)
| ~ cC62(iV21026)
| ~ cC60(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC42(iV21026)
| ~ cC40(iV21026)
| ~ cC38(iV21026)
| ~ cC36(iV21026)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ cC20(iV21026)
| ~ cC180(iV21026)
| ~ cC174(iV21026)
| ~ cC168(iV21026)
| ~ cC16(iV21026)
| ~ cC22(iV21026)
| ~ cC158(iV21026)
| ~ cC156(iV21026)
| ~ cC154(iV21026)
| ~ cC152(iV21026)
| ~ cC14(iV21026)
| ~ cC138(iV21026)
| ~ cC136(iV21026)
| ~ cC134(iV21026)
| ~ cC132(iV21026)
| ~ cC130(iV21026)
| ~ cC116(iV21026)
| ~ cC114(iV21026)
| ~ cC90(iV21026)
| ~ cC112(iV21026)
| ~ cC110(iV21026)
| ~ cC108(iV21026)
| ~ cC4(iV21026)
| ~ cC8(iV21026)
| ~ cC10(iV21026)
| ~ xsd_integer(sK124)
| ~ cowlThing(sK123)
| ~ cowlThing(iV21029)
| ~ cowlThing(iV21027)
| ~ cowlThing(iV21030)
| ~ cowlThing(iV21026) ),
inference(cnf_transformation,[],[f1487]) ).
tcf(c_638,plain,
( cC180(iV21026)
| ~ cTEST(iV21026) ),
inference(instantiation,[status(thm)],[c_478]) ).
tcf(c_639,plain,
( cC158(iV21026)
| ~ cTEST(iV21026) ),
inference(instantiation,[status(thm)],[c_477]) ).
tcf(c_643,plain,
( cC86(iV21026)
| ~ cC90(iV21026) ),
inference(instantiation,[status(thm)],[c_452]) ).
tcf(c_644,plain,
( cC88(iV21026)
| ~ cTOP(iV21026) ),
inference(instantiation,[status(thm)],[c_449]) ).
tcf(c_646,plain,
( cC82(iV21026)
| ~ cC86(iV21026) ),
inference(instantiation,[status(thm)],[c_447]) ).
tcf(c_647,plain,
( cC84(iV21026)
| ~ cTOP(iV21026) ),
inference(instantiation,[status(thm)],[c_444]) ).
tcf(c_648,plain,
( cC80(iV21026)
| ~ cC82(iV21026) ),
inference(instantiation,[status(thm)],[c_443]) ).
tcf(c_649,plain,
( cC64(iV21026)
| ~ cC82(iV21026) ),
inference(instantiation,[status(thm)],[c_442]) ).
tcf(c_650,plain,
( cC78(iV21026)
| ~ cC80(iV21026) ),
inference(instantiation,[status(thm)],[c_439]) ).
tcf(c_656,plain,
( cC60(iV21026)
| ~ cC64(iV21026) ),
inference(instantiation,[status(thm)],[c_390]) ).
tcf(c_657,plain,
( cC62(iV21026)
| ~ cTOP(iV21026) ),
inference(instantiation,[status(thm)],[c_387]) ).
tcf(c_658,plain,
( cC42(iV21026)
| ~ cC60(iV21026) ),
inference(instantiation,[status(thm)],[c_386]) ).
tcf(c_659,plain,
( cC58(iV21026)
| ~ cC60(iV21026) ),
inference(instantiation,[status(thm)],[c_385]) ).
tcf(c_660,plain,
( cC56(iV21026)
| ~ cC58(iV21026) ),
inference(instantiation,[status(thm)],[c_379]) ).
tcf(c_665,plain,
( cC38(iV21026)
| ~ cC42(iV21026) ),
inference(instantiation,[status(thm)],[c_334]) ).
tcf(c_667,plain,
( cC40(iV21026)
| ~ cTOP(iV21026) ),
inference(instantiation,[status(thm)],[c_330]) ).
tcf(c_668,plain,
( cC36(iV21026)
| ~ cC38(iV21026) ),
inference(instantiation,[status(thm)],[c_325]) ).
tcf(c_673,plain,
( cC16(iV21026)
| ~ cC22(iV21026) ),
inference(instantiation,[status(thm)],[c_280]) ).
tcf(c_674,plain,
( cC20(iV21026)
| ~ cC22(iV21026) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_675,plain,
( cC174(iV21026)
| ~ cC180(iV21026) ),
inference(instantiation,[status(thm)],[c_270]) ).
tcf(c_676,plain,
( cC168(iV21026)
| ~ cC174(iV21026) ),
inference(instantiation,[status(thm)],[c_252]) ).
tcf(c_677,plain,
( cC14(iV21026)
| ~ cC16(iV21026) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_678,plain,
( cC10(iV21026)
| ~ cC16(iV21026) ),
inference(instantiation,[status(thm)],[c_206]) ).
tcf(c_679,plain,
( cC156(iV21026)
| ~ cC158(iV21026) ),
inference(instantiation,[status(thm)],[c_204]) ).
tcf(c_680,plain,
( cC22(iV21026)
| ~ cC158(iV21026) ),
inference(instantiation,[status(thm)],[c_203]) ).
tcf(c_681,plain,
( cC138(iV21026)
| ~ cC156(iV21026) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_682,plain,
( cC154(iV21026)
| ~ cC156(iV21026) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_683,plain,
( cC152(iV21026)
| ~ cC154(iV21026) ),
inference(instantiation,[status(thm)],[c_197]) ).
tcf(c_688,plain,
( cC134(iV21026)
| ~ cC138(iV21026) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_689,plain,
( cC136(iV21026)
| ~ cC138(iV21026) ),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_691,plain,
( cC132(iV21026)
| ~ cC134(iV21026) ),
inference(instantiation,[status(thm)],[c_144]) ).
tcf(c_692,plain,
( cC116(iV21026)
| ~ cC134(iV21026) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_693,plain,
( cC130(iV21026)
| ~ cC132(iV21026) ),
inference(instantiation,[status(thm)],[c_140]) ).
tcf(c_698,plain,
( cC112(iV21026)
| ~ cC116(iV21026) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_699,plain,
( cC114(iV21026)
| ~ cC116(iV21026) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_701,plain,
( cC90(iV21026)
| ~ cC112(iV21026) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_702,plain,
( cC110(iV21026)
| ~ cC112(iV21026) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_703,plain,
( cC108(iV21026)
| ~ cC110(iV21026) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_706,plain,
( cC4(iV21026)
| ~ cC10(iV21026) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_707,plain,
( cC8(iV21026)
| ~ cC10(iV21026) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_1067,plain,
( xsd_string(sK124)
| cowlNothing(sK123)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ xsd_integer(sK124)
| ~ cowlThing(sK123)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC44(iV21029)
| ~ cC50(iV21029) ),
inference(global_subsumption_just,[status(thm)],[c_635,c_598,c_570,c_540,c_513,c_511,c_482,c_638,c_639,c_643,c_644,c_646,c_647,c_648,c_649,c_650,c_656,c_657,c_658,c_659,c_660,c_665,c_667,c_668,c_673,c_674,c_675,c_676,c_677,c_678,c_679,c_680,c_681,c_682,c_683,c_688,c_689,c_691,c_692,c_693,c_698,c_699,c_701,c_702,c_703,c_706,c_707,c_635]) ).
tcf(c_1068,negated_conjecture,
( xsd_string(sK124)
| cowlNothing(sK123)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_integer(sK124)
| ~ cowlThing(sK123) ),
inference(renaming,[status(thm)],[c_1067]) ).
tcf(c_1069,plain,
( xsd_integer(sK124)
| cowlNothing(sK123)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ xsd_string(sK124)
| ~ cowlThing(sK123)
| ~ cC24(iV21027)
| ~ cC30(iV21027)
| ~ cC44(iV21029)
| ~ cC50(iV21029) ),
inference(global_subsumption_just,[status(thm)],[c_634,c_598,c_570,c_540,c_513,c_511,c_482,c_638,c_639,c_643,c_644,c_646,c_647,c_648,c_649,c_650,c_656,c_657,c_658,c_659,c_660,c_665,c_667,c_668,c_673,c_674,c_675,c_676,c_677,c_678,c_679,c_680,c_681,c_682,c_683,c_688,c_689,c_691,c_692,c_693,c_698,c_699,c_701,c_702,c_703,c_706,c_707,c_634]) ).
tcf(c_1070,negated_conjecture,
( xsd_integer(sK124)
| cowlNothing(sK123)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_string(sK124)
| ~ cowlThing(sK123) ),
inference(renaming,[status(thm)],[c_1069]) ).
tcf(c_1071,plain,
! [X0: $i] :
( ~ xsd_string(X0)
| ~ xsd_integer(X0) ),
inference(prop_impl_just,[status(thm)],[c_52]) ).
tcf(c_1072,plain,
! [X0: $i] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(renaming,[status(thm)],[c_1071]) ).
tcf(c_1073,plain,
! [X0: $i] :
( xsd_string(X0)
| xsd_integer(X0) ),
inference(prop_impl_just,[status(thm)],[c_51]) ).
tcf(c_1074,plain,
! [X0: $i] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(renaming,[status(thm)],[c_1073]) ).
tcf(c_1723,plain,
! [X0: $i,X1: $i] :
( cC24(X0)
| ~ ra_Px5(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_281]) ).
tcf(c_1731,plain,
! [X0: $i] :
( ra_Px5(X0,sK69(X0))
| cC24xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_286]) ).
tcf(c_1732,plain,
! [X0: $i] :
( cC24xcomp(X0)
| ra_Px5(X0,sK69(X0)) ),
inference(renaming,[status(thm)],[c_1731]) ).
tcf(c_1739,plain,
! [X0: $i] :
( ra_Px92(X0,sK70(X0))
| ~ cC26(X0) ),
inference(prop_impl_just,[status(thm)],[c_289]) ).
tcf(c_1743,plain,
! [X0: $i,X1: $i] :
( ~ cC26xcomp(X0)
| ~ ra_Px92(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_293]) ).
tcf(c_1775,plain,
! [X0: $i,X1: $i] :
( cC30(X0)
| ~ ra_Px8(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_301]) ).
tcf(c_1783,plain,
! [X0: $i] :
( ra_Px8(X0,sK76(X0))
| cC30xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_306]) ).
tcf(c_1784,plain,
! [X0: $i] :
( cC30xcomp(X0)
| ra_Px8(X0,sK76(X0)) ),
inference(renaming,[status(thm)],[c_1783]) ).
tcf(c_1791,plain,
! [X0: $i,X1: $i] :
( ~ ra_Px91(X0,X1)
| ~ cC32(X0) ),
inference(prop_impl_just,[status(thm)],[c_309]) ).
tcf(c_1792,plain,
! [X0: $i,X1: $i] :
( ~ cC32(X0)
| ~ ra_Px91(X0,X1) ),
inference(renaming,[status(thm)],[c_1791]) ).
tcf(c_1797,plain,
! [X0: $i] :
( ra_Px91(X0,sK78(X0))
| ~ cC32xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_313]) ).
tcf(c_1839,plain,
! [X0: $i,X1: $i] :
( cC44xcomp(X0)
| ~ ra_Px13(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_340]) ).
tcf(c_1841,plain,
! [X0: $i] :
( ra_Px13(X0,sK83(X0))
| cC44(X0) ),
inference(prop_impl_just,[status(thm)],[c_335]) ).
tcf(c_1842,plain,
! [X0: $i] :
( cC44(X0)
| ra_Px13(X0,sK83(X0)) ),
inference(renaming,[status(thm)],[c_1841]) ).
tcf(c_1853,plain,
! [X0: $i] :
( ra_Px90(X0,sK86(X0))
| ~ cC46(X0) ),
inference(prop_impl_just,[status(thm)],[c_343]) ).
tcf(c_1857,plain,
! [X0: $i,X1: $i] :
( ~ cC46xcomp(X0)
| ~ ra_Px90(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_347]) ).
tcf(c_1889,plain,
! [X0: $i] :
( ra_Px16(X0,sK91(X0))
| cC50(X0) ),
inference(prop_impl_just,[status(thm)],[c_358]) ).
tcf(c_1890,plain,
! [X0: $i] :
( cC50(X0)
| ra_Px16(X0,sK91(X0)) ),
inference(renaming,[status(thm)],[c_1889]) ).
tcf(c_1893,plain,
! [X0: $i,X1: $i] :
( cC50xcomp(X0)
| ~ ra_Px16(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_360]) ).
tcf(c_1905,plain,
! [X0: $i] :
( ra_Px89(X0,sK93(X0))
| ~ cC52(X0) ),
inference(prop_impl_just,[status(thm)],[c_363]) ).
tcf(c_1909,plain,
! [X0: $i,X1: $i] :
( ~ cC52xcomp(X0)
| ~ ra_Px89(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_367]) ).
tcf(c_1975,plain,
! [X0: $i,X1: $i] :
( cC66(X0)
| ~ ra_Px21(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_392]) ).
tcf(c_1983,plain,
! [X0: $i] :
( ra_Px21(X0,sK101(X0))
| cC66xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_397]) ).
tcf(c_1984,plain,
! [X0: $i] :
( cC66xcomp(X0)
| ra_Px21(X0,sK101(X0)) ),
inference(renaming,[status(thm)],[c_1983]) ).
tcf(c_1991,plain,
! [X0: $i,X1: $i] :
( ~ ra_Px88(X0,X1)
| ~ cC68(X0) ),
inference(prop_impl_just,[status(thm)],[c_400]) ).
tcf(c_1992,plain,
! [X0: $i,X1: $i] :
( ~ cC68(X0)
| ~ ra_Px88(X0,X1) ),
inference(renaming,[status(thm)],[c_1991]) ).
tcf(c_1997,plain,
! [X0: $i] :
( ra_Px88(X0,sK103(X0))
| ~ cC68xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_404]) ).
tcf(c_2025,plain,
! [X0: $i,X1: $i] :
( cC72(X0)
| ~ ra_Px24(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_412]) ).
tcf(c_2033,plain,
! [X0: $i] :
( ra_Px24(X0,sK109(X0))
| cC72xcomp(X0) ),
inference(prop_impl_just,[status(thm)],[c_417]) ).
tcf(c_2034,plain,
! [X0: $i] :
( cC72xcomp(X0)
| ra_Px24(X0,sK109(X0)) ),
inference(renaming,[status(thm)],[c_2033]) ).
tcf(c_2041,plain,
! [X0: $i] :
( ra_Px87(X0,sK110(X0))
| ~ cC74(X0) ),
inference(prop_impl_just,[status(thm)],[c_423]) ).
tcf(c_2047,plain,
! [X0: $i,X1: $i] :
( ~ cC74xcomp(X0)
| ~ ra_Px87(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_424]) ).
tcf(c_3286,plain,
( xsd_integer(sK124)
| cowlNothing(sK123)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_string(sK124) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1070,c_49]) ).
tcf(c_3287,plain,
( xsd_string(sK124)
| cowlNothing(sK123)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_integer(sK124) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1068,c_49]) ).
tcf(c_3502,plain,
( xsd_string(sK124)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_integer(sK124) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3287,c_50]) ).
tcf(c_3503,plain,
( xsd_integer(sK124)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_string(sK124) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3286,c_50]) ).
tcf(c_3529,plain,
( xsd_string(sK124)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3502,c_1074]) ).
tcf(c_5706,plain,
! [X0: $i] :
( ~ cC26xcomp(X0)
| ~ cC26(X0) ),
inference(resolution,[status(thm)],[c_1743,c_1739]) ).
tcf(c_5718,plain,
! [X0: $i] :
( ~ cC32xcomp(X0)
| ~ cC32(X0) ),
inference(resolution,[status(thm)],[c_1792,c_1797]) ).
tcf(c_5728,plain,
! [X0: $i] :
( ~ cC46xcomp(X0)
| ~ cC46(X0) ),
inference(resolution,[status(thm)],[c_1857,c_1853]) ).
tcf(c_5739,plain,
! [X0: $i] :
( ~ cC52xcomp(X0)
| ~ cC52(X0) ),
inference(resolution,[status(thm)],[c_1909,c_1905]) ).
tcf(c_5762,plain,
! [X0: $i] :
( ~ cC68xcomp(X0)
| ~ cC68(X0) ),
inference(resolution,[status(thm)],[c_1992,c_1997]) ).
tcf(c_5772,plain,
! [X0: $i] :
( ~ cC74xcomp(X0)
| ~ cC74(X0) ),
inference(resolution,[status(thm)],[c_2047,c_2041]) ).
tcf(c_6038,plain,
~ cC26(iV21027),
inference(resolution,[status(thm)],[c_5706,c_534]) ).
tcf(c_6063,plain,
~ cC32(iV21027),
inference(resolution,[status(thm)],[c_5718,c_542]) ).
tcf(c_6092,plain,
~ cC46(iV21029),
inference(resolution,[status(thm)],[c_5728,c_564]) ).
tcf(c_6117,plain,
~ cC52(iV21029),
inference(resolution,[status(thm)],[c_5739,c_560]) ).
tcf(c_6146,plain,
~ cC68(iV21030),
inference(resolution,[status(thm)],[c_5762,c_583]) ).
tcf(c_6171,plain,
~ cC74(iV21030),
inference(resolution,[status(thm)],[c_5772,c_599]) ).
tcf(c_6960,plain,
! [X0: $i] :
( cC24xcomp(X0)
| cC24(X0) ),
inference(resolution,[status(thm)],[c_1723,c_1732]) ).
tcf(c_7003,plain,
! [X0: $i] :
( cC30xcomp(X0)
| cC30(X0) ),
inference(resolution,[status(thm)],[c_1775,c_1784]) ).
tcf(c_7036,plain,
! [X0: $i] :
( cC44xcomp(X0)
| cC44(X0) ),
inference(resolution,[status(thm)],[c_1842,c_1839]) ).
tcf(c_7079,plain,
! [X0: $i] :
( cC50xcomp(X0)
| cC50(X0) ),
inference(resolution,[status(thm)],[c_1890,c_1893]) ).
tcf(c_7132,plain,
! [X0: $i] :
( cC66xcomp(X0)
| cC66(X0) ),
inference(resolution,[status(thm)],[c_1975,c_1984]) ).
tcf(c_7175,plain,
! [X0: $i] :
( cC72xcomp(X0)
| cC72(X0) ),
inference(resolution,[status(thm)],[c_2025,c_2034]) ).
tcf(c_7252,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027)
| ~ xsd_integer(sK124) ),
inference(resolution,[status(thm)],[c_1072,c_3529]) ).
tcf(c_7253,plain,
( ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cC30(iV21027)
| ~ cC24(iV21027) ),
inference(global_subsumption_just,[status(thm)],[c_7252,c_3503,c_3529,c_7252]) ).
tcf(c_7410,plain,
! [X0: $i] :
( cC26(X0)
| cC24(X0)
| ~ cC2xcomp(X0) ),
inference(resolution,[status(thm)],[c_6960,c_290]) ).
tcf(c_7436,plain,
! [X0: $i] :
( cC32(X0)
| cC30(X0)
| ~ cC2xcomp(X0) ),
inference(resolution,[status(thm)],[c_7003,c_310]) ).
tcf(c_7462,plain,
! [X0: $i] :
( cC46(X0)
| cC44(X0)
| ~ cC12xcomp(X0) ),
inference(resolution,[status(thm)],[c_7036,c_344]) ).
tcf(c_7488,plain,
! [X0: $i] :
( cC52(X0)
| cC50(X0)
| ~ cC12xcomp(X0) ),
inference(resolution,[status(thm)],[c_7079,c_364]) ).
tcf(c_7514,plain,
! [X0: $i] :
( cC68(X0)
| cC66(X0)
| ~ cC18xcomp(X0) ),
inference(resolution,[status(thm)],[c_7132,c_401]) ).
tcf(c_7540,plain,
! [X0: $i] :
( cC74(X0)
| cC72(X0)
| ~ cC18xcomp(X0) ),
inference(resolution,[status(thm)],[c_7175,c_419]) ).
tcf(c_9547,plain,
( cC24(iV21027)
| ~ cC2xcomp(iV21027) ),
inference(resolution,[status(thm)],[c_7410,c_6038]) ).
tcf(c_9630,plain,
( cC30(iV21027)
| ~ cC2xcomp(iV21027) ),
inference(resolution,[status(thm)],[c_7436,c_6063]) ).
tcf(c_9714,plain,
( cC44(iV21029)
| ~ cC12xcomp(iV21029) ),
inference(resolution,[status(thm)],[c_7462,c_6092]) ).
tcf(c_9796,plain,
( cC50(iV21029)
| ~ cC12xcomp(iV21029) ),
inference(resolution,[status(thm)],[c_7488,c_6117]) ).
tcf(c_9878,plain,
( cC66(iV21030)
| ~ cC18xcomp(iV21030) ),
inference(resolution,[status(thm)],[c_7514,c_6146]) ).
tcf(c_9959,plain,
( cC72(iV21030)
| ~ cC18xcomp(iV21030) ),
inference(resolution,[status(thm)],[c_7540,c_6171]) ).
tcf(c_9960,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_9959,c_9878,c_9796,c_9714,c_9630,c_9547,c_7253,c_529,c_557,c_585]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS159+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 19:34:49 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 3.51/1.18 % SZS status Started for theBenchmark.p
% 3.51/1.18 % SZS status Theorem for theBenchmark.p
% 3.51/1.18
% 3.51/1.18 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.51/1.18
% 3.51/1.18 % ------ iProver source info
% 3.51/1.18
% 3.51/1.18 % git: date: 2026-07-19 20:42:38 +0200
% 3.51/1.18 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.51/1.18 % git: non_committed_changes: false
% 3.51/1.18
% 3.51/1.18 % ------ Parsing...
% 3.51/1.18 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.51/1.18
% 3.51/1.18 % ------ 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:128:0s%
% 3.51/1.18
% 3.51/1.18 % SZS status Theorem for theBenchmark.p
% 3.51/1.18
% 3.51/1.18 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.51/1.19
% 3.51/1.19
%------------------------------------------------------------------------------