%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KRS159+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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 : Tue Sep 29 11:41:47 AM UTC 2026
% Result : Theorem 2.92s 1.32s
% Output : Refutation 3.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 110
% Syntax : Number of formulae : 535 ( 111 unt; 54 def)
% Number of atoms : 1914 ( 0 equ)
% Maximal formula atoms : 56 ( 3 avg)
% Number of connectives : 2329 ( 950 ~; 954 |; 328 &)
% ( 94 <=>; 2 =>; 0 <=; 1 <~>)
% Maximal formula depth : 56 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 118 ( 117 usr; 55 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 11 con; 0-1 aty)
% Number of variables : 249 ( 0 sgn 219 !; 30 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( cowlThing(X0)
& ~ cowlNothing(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(f3,axiom,
! [X0] :
( cC10(X0)
<=> ( cC8(X0)
& cC4(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
fof(f16,axiom,
! [X0] :
( cC110(X0)
<=> ( cC108(X0)
& cTOP(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_15) ).
fof(f17,axiom,
! [X0] :
( cC112(X0)
<=> ( cC110(X0)
& cC90(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_16) ).
fof(f19,axiom,
! [X0] :
( cC116(X0)
<=> ( cC114(X0)
& cC112(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
fof(f41,axiom,
! [X0] :
( cC132(X0)
<=> ( cC130(X0)
& cTOP(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_40) ).
fof(f42,axiom,
! [X0] :
( cC134(X0)
<=> ( cC116(X0)
& cC132(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_41) ).
fof(f44,axiom,
! [X0] :
( cC138(X0)
<=> ( cC136(X0)
& cC134(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_43) ).
fof(f65,axiom,
! [X0] :
( cC154(X0)
<=> ( cC152(X0)
& cTOP(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_64) ).
fof(f66,axiom,
! [X0] :
( cC156(X0)
<=> ( cC154(X0)
& cC138(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_65) ).
fof(f67,axiom,
! [X0] :
( cC158(X0)
<=> ( cC22(X0)
& cC156(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_66) ).
fof(f68,axiom,
! [X0] :
( cC16(X0)
<=> ( cC10(X0)
& cC14(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_67) ).
fof(f88,axiom,
! [X0] :
( cC174(X0)
<=> ( cC172xcomp(X0)
& cC168(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_87) ).
fof(f97,axiom,
! [X0] :
( cC180(X0)
<=> ( cC174(X0)
& cC178xcomp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_96) ).
fof(f101,axiom,
! [X0] :
( cC22(X0)
<=> ( cC20(X0)
& cC16(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_100) ).
fof(f103,axiom,
! [X0] :
( cC24(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_102) ).
fof(f112,axiom,
! [X0] :
( cC30(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC12xcomp(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_111) ).
fof(f121,axiom,
! [X0] :
( cC38(X0)
<=> ( cC36(X0)
& cTOP(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_120) ).
fof(f124,axiom,
! [X0] :
( cC42(X0)
<=> ( cC40(X0)
& cC38(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_123) ).
fof(f126,axiom,
! [X0] :
( cC44(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_125) ).
fof(f134,axiom,
! [X0] :
( cC50(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC12xcomp(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_133) ).
fof(f144,axiom,
! [X0] :
( cC58(X0)
<=> ( cC56(X0)
& cTOP(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_143) ).
fof(f147,axiom,
! [X0] :
( cC60(X0)
<=> ( cC58(X0)
& cC42(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_146) ).
fof(f149,axiom,
! [X0] :
( cC64(X0)
<=> ( cC60(X0)
& cC62(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_148) ).
fof(f151,axiom,
! [X0] :
( cC66(X0)
<=> ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_150) ).
fof(f159,axiom,
! [X0] :
( cC72(X0)
<=> ? [X1] : ra_Px24(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_158) ).
fof(f161,axiom,
! [X0] :
( cC72xcomp(X0)
<=> ~ ? [X1] : ra_Px24(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_160) ).
fof(f162,axiom,
! [X0] :
( cC74(X0)
<=> ( cC72xcomp(X0)
& cC18xcomp(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_161) ).
fof(f163,axiom,
! [X0] :
( cC74(X0)
<=> ? [X1] : ra_Px87(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_162) ).
fof(f164,axiom,
! [X0] :
( cC74xcomp(X0)
<=> ~ ? [X1] : ra_Px87(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_163) ).
fof(f170,axiom,
! [X0] :
( cC80(X0)
<=> ( cC78(X0)
& cTOP(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_169) ).
fof(f171,axiom,
! [X0] :
( cC82(X0)
<=> ( cC64(X0)
& cC80(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_170) ).
fof(f173,axiom,
! [X0] :
( cC86(X0)
<=> ( cC82(X0)
& cC84(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_172) ).
fof(f174,axiom,
! [X0] :
( cC88(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_173) ).
fof(f175,axiom,
! [X0] :
( cC90(X0)
<=> ( cC86(X0)
& cC88(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_174) ).
fof(f187,axiom,
! [X0] :
( cTEST(X0)
<=> ( cC158(X0)
& cC180(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_186) ).
fof(f191,axiom,
cTOP(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_190) ).
fof(f220,axiom,
cowlThing(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_219) ).
fof(f222,axiom,
cTEST(iV21026),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_221) ).
fof(f249,axiom,
cowlThing(iV21027),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_248) ).
fof(f253,axiom,
rR1(iV21027,iV21036),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_252) ).
fof(f254,axiom,
rR1(iV21027,iV21035),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_253) ).
fof(f279,axiom,
cowlThing(iV21029),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_278) ).
fof(f282,axiom,
rR1(iV21029,iV21034),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_281) ).
fof(f283,axiom,
rR1(iV21029,iV21033),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_282) ).
fof(f294,axiom,
cC18xcomp(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_293) ).
fof(f307,axiom,
cowlThing(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_306) ).
fof(f308,axiom,
cC74xcomp(iV21030),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_307) ).
fof(f310,axiom,
rR1(iV21030,iV21032),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_309) ).
fof(f313,axiom,
cC2xcomp(iV21032),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_312) ).
fof(f320,axiom,
cC12xcomp(iV21033),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_319) ).
fof(f326,axiom,
cC2xcomp(iV21034),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_325) ).
fof(f332,axiom,
cC12xcomp(iV21035),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_331) ).
fof(f338,axiom,
cC2xcomp(iV21036),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_337) ).
fof(f343,conjecture,
( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& cC108(iV21026)
& cC40(iV21026)
& cC136(iV21026)
& cC10(iV21026)
& cC90(iV21026)
& cowlThing(iV21026)
& cC58(iV21026)
& cC56(iV21026)
& cC158(iV21026)
& cC110(iV21026)
& cC22(iV21026)
& cC60(iV21026)
& cC154(iV21026)
& cC180(iV21026)
& cC78(iV21026)
& cC16(iV21026)
& cC132(iV21026)
& cC114(iV21026)
& cC20(iV21026)
& cC84(iV21026)
& cC38(iV21026)
& cC138(iV21026)
& cC174(iV21026)
& cC62(iV21026)
& cC8(iV21026)
& cC36(iV21026)
& cC112(iV21026)
& cC64(iV21026)
& cC116(iV21026)
& cC82(iV21026)
& cC14(iV21026)
& cC152(iV21026)
& cC80(iV21026)
& cC88(iV21026)
& cC130(iV21026)
& cC168(iV21026)
& cC4(iV21026)
& cC134(iV21026)
& cC42(iV21026)
& cC156(iV21026)
& cC86(iV21026)
& cC30(iV21027)
& cowlThing(iV21027)
& cC24(iV21027)
& cC50(iV21029)
& cC44(iV21029)
& cowlThing(iV21029)
& cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(f344,negated_conjecture,
~ ( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& cC108(iV21026)
& cC40(iV21026)
& cC136(iV21026)
& cC10(iV21026)
& cC90(iV21026)
& cowlThing(iV21026)
& cC58(iV21026)
& cC56(iV21026)
& cC158(iV21026)
& cC110(iV21026)
& cC22(iV21026)
& cC60(iV21026)
& cC154(iV21026)
& cC180(iV21026)
& cC78(iV21026)
& cC16(iV21026)
& cC132(iV21026)
& cC114(iV21026)
& cC20(iV21026)
& cC84(iV21026)
& cC38(iV21026)
& cC138(iV21026)
& cC174(iV21026)
& cC62(iV21026)
& cC8(iV21026)
& cC36(iV21026)
& cC112(iV21026)
& cC64(iV21026)
& cC116(iV21026)
& cC82(iV21026)
& cC14(iV21026)
& cC152(iV21026)
& cC80(iV21026)
& cC88(iV21026)
& cC130(iV21026)
& cC168(iV21026)
& cC4(iV21026)
& cC134(iV21026)
& cC42(iV21026)
& cC156(iV21026)
& cC86(iV21026)
& cC30(iV21027)
& cowlThing(iV21027)
& cC24(iV21027)
& cC50(iV21029)
& cC44(iV21029)
& cowlThing(iV21029)
& cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030) ),
inference(negated_conjecture,[status(cth)],[f343]) ).
fof(f345,plain,
~ ( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC108(iV21026)
& cC40(iV21026)
& cC136(iV21026)
& cC10(iV21026)
& cC90(iV21026)
& cowlThing(iV21026)
& cC58(iV21026)
& cC56(iV21026)
& cC158(iV21026)
& cC110(iV21026)
& cC22(iV21026)
& cC60(iV21026)
& cC154(iV21026)
& cC180(iV21026)
& cC78(iV21026)
& cC16(iV21026)
& cC132(iV21026)
& cC114(iV21026)
& cC20(iV21026)
& cC84(iV21026)
& cC38(iV21026)
& cC138(iV21026)
& cC174(iV21026)
& cC62(iV21026)
& cC8(iV21026)
& cC36(iV21026)
& cC112(iV21026)
& cC64(iV21026)
& cC116(iV21026)
& cC82(iV21026)
& cC14(iV21026)
& cC152(iV21026)
& cC80(iV21026)
& cC88(iV21026)
& cC130(iV21026)
& cC168(iV21026)
& cC4(iV21026)
& cC134(iV21026)
& cC42(iV21026)
& cC156(iV21026)
& cC86(iV21026)
& cC30(iV21027)
& cowlThing(iV21027)
& cC24(iV21027)
& cC50(iV21029)
& cC44(iV21029)
& cowlThing(iV21029)
& cC72(iV21030)
& cC66(iV21030)
& cowlThing(iV21030) ),
inference(rectify,[],[f344]) ).
fof(f346,plain,
! [X0] :
( cTEST(X0)
=> ( cC158(X0)
& cC180(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(f421,plain,
! [X0] :
( cC72xcomp(X0)
<=> ! [X1] : ~ ra_Px24(X0,X1) ),
inference(ennf_transformation,[],[f161]) ).
fof(f422,plain,
! [X0] :
( ! [X1] : ~ ra_Px87(X0,X1)
| ~ cC74xcomp(X0) ),
inference(ennf_transformation,[],[f349]) ).
fof(f428,plain,
! [X0] :
( ( cC158(X0)
& cC180(X0) )
| ~ cTEST(X0) ),
inference(ennf_transformation,[],[f346]) ).
fof(f457,plain,
( ? [X0] :
( ~ cowlThing(X0)
| cowlNothing(X0) )
| ? [X1] :
( xsd_string(X1)
<~> ~ xsd_integer(X1) )
| ~ cC108(iV21026)
| ~ cC40(iV21026)
| ~ cC136(iV21026)
| ~ cC10(iV21026)
| ~ cC90(iV21026)
| ~ cowlThing(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC158(iV21026)
| ~ cC110(iV21026)
| ~ cC22(iV21026)
| ~ cC60(iV21026)
| ~ cC154(iV21026)
| ~ cC180(iV21026)
| ~ cC78(iV21026)
| ~ cC16(iV21026)
| ~ cC132(iV21026)
| ~ cC114(iV21026)
| ~ cC20(iV21026)
| ~ cC84(iV21026)
| ~ cC38(iV21026)
| ~ cC138(iV21026)
| ~ cC174(iV21026)
| ~ cC62(iV21026)
| ~ cC8(iV21026)
| ~ cC36(iV21026)
| ~ cC112(iV21026)
| ~ cC64(iV21026)
| ~ cC116(iV21026)
| ~ cC82(iV21026)
| ~ cC14(iV21026)
| ~ cC152(iV21026)
| ~ cC80(iV21026)
| ~ cC88(iV21026)
| ~ cC130(iV21026)
| ~ cC168(iV21026)
| ~ cC4(iV21026)
| ~ cC134(iV21026)
| ~ cC42(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC24(iV21027)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cowlThing(iV21029)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030) ),
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)
| ~ cC8(X0)
| ~ cC4(X0) )
& ( ( cC8(X0)
& cC4(X0) )
| ~ cC10(X0) ) ),
inference(nnf_transformation,[],[f3]) ).
fof(f460,plain,
! [X0] :
( ( cC10(X0)
| ~ cC8(X0)
| ~ cC4(X0) )
& ( ( cC8(X0)
& cC4(X0) )
| ~ cC10(X0) ) ),
inference(flattening,[],[f459]) ).
fof(f491,plain,
! [X0] :
( ( cC110(X0)
| ~ cC108(X0)
| ~ cTOP(X0) )
& ( ( cC108(X0)
& cTOP(X0) )
| ~ cC110(X0) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f492,plain,
! [X0] :
( ( cC110(X0)
| ~ cC108(X0)
| ~ cTOP(X0) )
& ( ( cC108(X0)
& cTOP(X0) )
| ~ cC110(X0) ) ),
inference(flattening,[],[f491]) ).
fof(f493,plain,
! [X0] :
( ( cC112(X0)
| ~ cC110(X0)
| ~ cC90(X0) )
& ( ( cC110(X0)
& cC90(X0) )
| ~ cC112(X0) ) ),
inference(nnf_transformation,[],[f17]) ).
fof(f494,plain,
! [X0] :
( ( cC112(X0)
| ~ cC110(X0)
| ~ cC90(X0) )
& ( ( cC110(X0)
& cC90(X0) )
| ~ cC112(X0) ) ),
inference(flattening,[],[f493]) ).
fof(f496,plain,
! [X0] :
( ( cC116(X0)
| ~ cC114(X0)
| ~ cC112(X0) )
& ( ( cC114(X0)
& cC112(X0) )
| ~ cC116(X0) ) ),
inference(nnf_transformation,[],[f19]) ).
fof(f497,plain,
! [X0] :
( ( cC116(X0)
| ~ cC114(X0)
| ~ cC112(X0) )
& ( ( cC114(X0)
& cC112(X0) )
| ~ cC116(X0) ) ),
inference(flattening,[],[f496]) ).
fof(f549,plain,
! [X0] :
( ( cC132(X0)
| ~ cC130(X0)
| ~ cTOP(X0) )
& ( ( cC130(X0)
& cTOP(X0) )
| ~ cC132(X0) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f550,plain,
! [X0] :
( ( cC132(X0)
| ~ cC130(X0)
| ~ cTOP(X0) )
& ( ( cC130(X0)
& cTOP(X0) )
| ~ cC132(X0) ) ),
inference(flattening,[],[f549]) ).
fof(f551,plain,
! [X0] :
( ( cC134(X0)
| ~ cC116(X0)
| ~ cC132(X0) )
& ( ( cC116(X0)
& cC132(X0) )
| ~ cC134(X0) ) ),
inference(nnf_transformation,[],[f42]) ).
fof(f552,plain,
! [X0] :
( ( cC134(X0)
| ~ cC116(X0)
| ~ cC132(X0) )
& ( ( cC116(X0)
& cC132(X0) )
| ~ cC134(X0) ) ),
inference(flattening,[],[f551]) ).
fof(f554,plain,
! [X0] :
( ( cC138(X0)
| ~ cC136(X0)
| ~ cC134(X0) )
& ( ( cC136(X0)
& cC134(X0) )
| ~ cC138(X0) ) ),
inference(nnf_transformation,[],[f44]) ).
fof(f555,plain,
! [X0] :
( ( cC138(X0)
| ~ cC136(X0)
| ~ cC134(X0) )
& ( ( cC136(X0)
& cC134(X0) )
| ~ cC138(X0) ) ),
inference(flattening,[],[f554]) ).
fof(f608,plain,
! [X0] :
( ( cC154(X0)
| ~ cC152(X0)
| ~ cTOP(X0) )
& ( ( cC152(X0)
& cTOP(X0) )
| ~ cC154(X0) ) ),
inference(nnf_transformation,[],[f65]) ).
fof(f609,plain,
! [X0] :
( ( cC154(X0)
| ~ cC152(X0)
| ~ cTOP(X0) )
& ( ( cC152(X0)
& cTOP(X0) )
| ~ cC154(X0) ) ),
inference(flattening,[],[f608]) ).
fof(f610,plain,
! [X0] :
( ( cC156(X0)
| ~ cC154(X0)
| ~ cC138(X0) )
& ( ( cC154(X0)
& cC138(X0) )
| ~ cC156(X0) ) ),
inference(nnf_transformation,[],[f66]) ).
fof(f611,plain,
! [X0] :
( ( cC156(X0)
| ~ cC154(X0)
| ~ cC138(X0) )
& ( ( cC154(X0)
& cC138(X0) )
| ~ cC156(X0) ) ),
inference(flattening,[],[f610]) ).
fof(f612,plain,
! [X0] :
( ( cC158(X0)
| ~ cC22(X0)
| ~ cC156(X0) )
& ( ( cC22(X0)
& cC156(X0) )
| ~ cC158(X0) ) ),
inference(nnf_transformation,[],[f67]) ).
fof(f613,plain,
! [X0] :
( ( cC158(X0)
| ~ cC22(X0)
| ~ cC156(X0) )
& ( ( cC22(X0)
& cC156(X0) )
| ~ cC158(X0) ) ),
inference(flattening,[],[f612]) ).
fof(f614,plain,
! [X0] :
( ( cC16(X0)
| ~ cC10(X0)
| ~ cC14(X0) )
& ( ( cC10(X0)
& cC14(X0) )
| ~ cC16(X0) ) ),
inference(nnf_transformation,[],[f68]) ).
fof(f615,plain,
! [X0] :
( ( cC16(X0)
| ~ cC10(X0)
| ~ cC14(X0) )
& ( ( cC10(X0)
& cC14(X0) )
| ~ cC16(X0) ) ),
inference(flattening,[],[f614]) ).
fof(f664,plain,
! [X0] :
( ( cC174(X0)
| ~ cC172xcomp(X0)
| ~ cC168(X0) )
& ( ( cC172xcomp(X0)
& cC168(X0) )
| ~ cC174(X0) ) ),
inference(nnf_transformation,[],[f88]) ).
fof(f665,plain,
! [X0] :
( ( cC174(X0)
| ~ cC172xcomp(X0)
| ~ cC168(X0) )
& ( ( cC172xcomp(X0)
& cC168(X0) )
| ~ cC174(X0) ) ),
inference(flattening,[],[f664]) ).
fof(f685,plain,
! [X0] :
( ( cC180(X0)
| ~ cC174(X0)
| ~ cC178xcomp(X0) )
& ( ( cC174(X0)
& cC178xcomp(X0) )
| ~ cC180(X0) ) ),
inference(nnf_transformation,[],[f97]) ).
fof(f686,plain,
! [X0] :
( ( cC180(X0)
| ~ cC174(X0)
| ~ cC178xcomp(X0) )
& ( ( cC174(X0)
& cC178xcomp(X0) )
| ~ cC180(X0) ) ),
inference(flattening,[],[f685]) ).
fof(f694,plain,
! [X0] :
( ( cC22(X0)
| ~ cC20(X0)
| ~ cC16(X0) )
& ( ( cC20(X0)
& cC16(X0) )
| ~ cC22(X0) ) ),
inference(nnf_transformation,[],[f101]) ).
fof(f695,plain,
! [X0] :
( ( cC22(X0)
| ~ cC20(X0)
| ~ cC16(X0) )
& ( ( cC20(X0)
& cC16(X0) )
| ~ cC22(X0) ) ),
inference(flattening,[],[f694]) ).
fof(f699,plain,
! [X0] :
( ( cC24(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) )
| ~ cC24(X0) ) ),
inference(nnf_transformation,[],[f103]) ).
fof(f700,plain,
! [X0] :
( ( cC24(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cC2xcomp(X2) )
| ~ cC24(X0) ) ),
inference(rectify,[],[f699]) ).
fof(f701,plain,
! [X0] :
( ( cC24(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ( rR1(X0,sK68(X0))
& cC2xcomp(sK68(X0)) )
| ~ cC24(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK68]),skolemize(X2,sK68(X0))],[f700]) ).
fof(f722,plain,
! [X0] :
( ( cC30(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC12xcomp(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cC12xcomp(X1) )
| ~ cC30(X0) ) ),
inference(nnf_transformation,[],[f112]) ).
fof(f723,plain,
! [X0] :
( ( cC30(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC12xcomp(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cC12xcomp(X2) )
| ~ cC30(X0) ) ),
inference(rectify,[],[f722]) ).
fof(f724,plain,
! [X0] :
( ( cC30(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC12xcomp(X1) ) )
& ( ( rR1(X0,sK75(X0))
& cC12xcomp(sK75(X0)) )
| ~ cC30(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK75]),skolemize(X2,sK75(X0))],[f723]) ).
fof(f745,plain,
! [X0] :
( ( cC38(X0)
| ~ cC36(X0)
| ~ cTOP(X0) )
& ( ( cC36(X0)
& cTOP(X0) )
| ~ cC38(X0) ) ),
inference(nnf_transformation,[],[f121]) ).
fof(f746,plain,
! [X0] :
( ( cC38(X0)
| ~ cC36(X0)
| ~ cTOP(X0) )
& ( ( cC36(X0)
& cTOP(X0) )
| ~ cC38(X0) ) ),
inference(flattening,[],[f745]) ).
fof(f751,plain,
! [X0] :
( ( cC42(X0)
| ~ cC40(X0)
| ~ cC38(X0) )
& ( ( cC40(X0)
& cC38(X0) )
| ~ cC42(X0) ) ),
inference(nnf_transformation,[],[f124]) ).
fof(f752,plain,
! [X0] :
( ( cC42(X0)
| ~ cC40(X0)
| ~ cC38(X0) )
& ( ( cC40(X0)
& cC38(X0) )
| ~ cC42(X0) ) ),
inference(flattening,[],[f751]) ).
fof(f756,plain,
! [X0] :
( ( cC44(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) )
| ~ cC44(X0) ) ),
inference(nnf_transformation,[],[f126]) ).
fof(f757,plain,
! [X0] :
( ( cC44(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cC2xcomp(X2) )
| ~ cC44(X0) ) ),
inference(rectify,[],[f756]) ).
fof(f758,plain,
! [X0] :
( ( cC44(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ( rR1(X0,sK84(X0))
& cC2xcomp(sK84(X0)) )
| ~ cC44(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK84]),skolemize(X2,sK84(X0))],[f757]) ).
fof(f776,plain,
! [X0] :
( ( cC50(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC12xcomp(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cC12xcomp(X1) )
| ~ cC50(X0) ) ),
inference(nnf_transformation,[],[f134]) ).
fof(f777,plain,
! [X0] :
( ( cC50(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC12xcomp(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cC12xcomp(X2) )
| ~ cC50(X0) ) ),
inference(rectify,[],[f776]) ).
fof(f778,plain,
! [X0] :
( ( cC50(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC12xcomp(X1) ) )
& ( ( rR1(X0,sK90(X0))
& cC12xcomp(sK90(X0)) )
| ~ cC50(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK90]),skolemize(X2,sK90(X0))],[f777]) ).
fof(f801,plain,
! [X0] :
( ( cC58(X0)
| ~ cC56(X0)
| ~ cTOP(X0) )
& ( ( cC56(X0)
& cTOP(X0) )
| ~ cC58(X0) ) ),
inference(nnf_transformation,[],[f144]) ).
fof(f802,plain,
! [X0] :
( ( cC58(X0)
| ~ cC56(X0)
| ~ cTOP(X0) )
& ( ( cC56(X0)
& cTOP(X0) )
| ~ cC58(X0) ) ),
inference(flattening,[],[f801]) ).
fof(f807,plain,
! [X0] :
( ( cC60(X0)
| ~ cC58(X0)
| ~ cC42(X0) )
& ( ( cC58(X0)
& cC42(X0) )
| ~ cC60(X0) ) ),
inference(nnf_transformation,[],[f147]) ).
fof(f808,plain,
! [X0] :
( ( cC60(X0)
| ~ cC58(X0)
| ~ cC42(X0) )
& ( ( cC58(X0)
& cC42(X0) )
| ~ cC60(X0) ) ),
inference(flattening,[],[f807]) ).
fof(f810,plain,
! [X0] :
( ( cC64(X0)
| ~ cC60(X0)
| ~ cC62(X0) )
& ( ( cC60(X0)
& cC62(X0) )
| ~ cC64(X0) ) ),
inference(nnf_transformation,[],[f149]) ).
fof(f811,plain,
! [X0] :
( ( cC64(X0)
| ~ cC60(X0)
| ~ cC62(X0) )
& ( ( cC60(X0)
& cC62(X0) )
| ~ cC64(X0) ) ),
inference(flattening,[],[f810]) ).
fof(f815,plain,
! [X0] :
( ( cC66(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& cC2xcomp(X1) )
| ~ cC66(X0) ) ),
inference(nnf_transformation,[],[f151]) ).
fof(f816,plain,
! [X0] :
( ( cC66(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& cC2xcomp(X2) )
| ~ cC66(X0) ) ),
inference(rectify,[],[f815]) ).
fof(f817,plain,
! [X0] :
( ( cC66(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ) )
& ( ( rR1(X0,sK100(X0))
& cC2xcomp(sK100(X0)) )
| ~ cC66(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK100]),skolemize(X2,sK100(X0))],[f816]) ).
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)
| ! [X1] : ~ ra_Px24(X0,X1) )
& ( ? [X2] : ra_Px24(X0,X2)
| ~ cC72(X0) ) ),
inference(rectify,[],[f836]) ).
fof(f838,plain,
! [X0] :
( ( cC72(X0)
| ! [X1] : ~ ra_Px24(X0,X1) )
& ( ra_Px24(X0,sK107(X0))
| ~ 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)
| ? [X1] : ra_Px24(X0,X1) )
& ( ! [X2] : ~ ra_Px24(X0,X2)
| ~ cC72xcomp(X0) ) ),
inference(rectify,[],[f842]) ).
fof(f844,plain,
! [X0] :
( ( cC72xcomp(X0)
| ra_Px24(X0,sK109(X0)) )
& ( ! [X2] : ~ ra_Px24(X0,X2)
| ~ cC72xcomp(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK109]),skolemize(X1,sK109(X0))],[f843]) ).
fof(f845,plain,
! [X0] :
( ( cC74(X0)
| ~ cC72xcomp(X0)
| ~ cC18xcomp(X0) )
& ( ( cC72xcomp(X0)
& cC18xcomp(X0) )
| ~ cC74(X0) ) ),
inference(nnf_transformation,[],[f162]) ).
fof(f846,plain,
! [X0] :
( ( cC74(X0)
| ~ cC72xcomp(X0)
| ~ cC18xcomp(X0) )
& ( ( cC72xcomp(X0)
& cC18xcomp(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)
| ! [X1] : ~ ra_Px87(X0,X1) )
& ( ? [X2] : ra_Px87(X0,X2)
| ~ cC74(X0) ) ),
inference(rectify,[],[f847]) ).
fof(f849,plain,
! [X0] :
( ( cC74(X0)
| ! [X1] : ~ ra_Px87(X0,X1) )
& ( ra_Px87(X0,sK110(X0))
| ~ cC74(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK110]),skolemize(X2,sK110(X0))],[f848]) ).
fof(f864,plain,
! [X0] :
( ( cC80(X0)
| ~ cC78(X0)
| ~ cTOP(X0) )
& ( ( cC78(X0)
& cTOP(X0) )
| ~ cC80(X0) ) ),
inference(nnf_transformation,[],[f170]) ).
fof(f865,plain,
! [X0] :
( ( cC80(X0)
| ~ cC78(X0)
| ~ cTOP(X0) )
& ( ( cC78(X0)
& cTOP(X0) )
| ~ cC80(X0) ) ),
inference(flattening,[],[f864]) ).
fof(f866,plain,
! [X0] :
( ( cC82(X0)
| ~ cC64(X0)
| ~ cC80(X0) )
& ( ( cC64(X0)
& cC80(X0) )
| ~ cC82(X0) ) ),
inference(nnf_transformation,[],[f171]) ).
fof(f867,plain,
! [X0] :
( ( cC82(X0)
| ~ cC64(X0)
| ~ cC80(X0) )
& ( ( cC64(X0)
& cC80(X0) )
| ~ cC82(X0) ) ),
inference(flattening,[],[f866]) ).
fof(f869,plain,
! [X0] :
( ( cC86(X0)
| ~ cC82(X0)
| ~ cC84(X0) )
& ( ( cC82(X0)
& cC84(X0) )
| ~ cC86(X0) ) ),
inference(nnf_transformation,[],[f173]) ).
fof(f870,plain,
! [X0] :
( ( cC86(X0)
| ~ cC82(X0)
| ~ cC84(X0) )
& ( ( cC82(X0)
& cC84(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)
| ~ cC86(X0)
| ~ cC88(X0) )
& ( ( cC86(X0)
& cC88(X0) )
| ~ cC90(X0) ) ),
inference(nnf_transformation,[],[f175]) ).
fof(f873,plain,
! [X0] :
( ( cC90(X0)
| ~ cC86(X0)
| ~ cC88(X0) )
& ( ( cC86(X0)
& cC88(X0) )
| ~ cC90(X0) ) ),
inference(flattening,[],[f872]) ).
fof(f900,plain,
( ? [X0] :
( ~ cowlThing(X0)
| cowlNothing(X0) )
| ? [X1] :
( ( xsd_integer(X1)
| ~ xsd_string(X1) )
& ( ~ xsd_integer(X1)
| xsd_string(X1) ) )
| ~ cC108(iV21026)
| ~ cC40(iV21026)
| ~ cC136(iV21026)
| ~ cC10(iV21026)
| ~ cC90(iV21026)
| ~ cowlThing(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC158(iV21026)
| ~ cC110(iV21026)
| ~ cC22(iV21026)
| ~ cC60(iV21026)
| ~ cC154(iV21026)
| ~ cC180(iV21026)
| ~ cC78(iV21026)
| ~ cC16(iV21026)
| ~ cC132(iV21026)
| ~ cC114(iV21026)
| ~ cC20(iV21026)
| ~ cC84(iV21026)
| ~ cC38(iV21026)
| ~ cC138(iV21026)
| ~ cC174(iV21026)
| ~ cC62(iV21026)
| ~ cC8(iV21026)
| ~ cC36(iV21026)
| ~ cC112(iV21026)
| ~ cC64(iV21026)
| ~ cC116(iV21026)
| ~ cC82(iV21026)
| ~ cC14(iV21026)
| ~ cC152(iV21026)
| ~ cC80(iV21026)
| ~ cC88(iV21026)
| ~ cC130(iV21026)
| ~ cC168(iV21026)
| ~ cC4(iV21026)
| ~ cC134(iV21026)
| ~ cC42(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC24(iV21027)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cowlThing(iV21029)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030) ),
inference(nnf_transformation,[],[f457]) ).
fof(f901,plain,
( ~ cowlThing(sK123)
| cowlNothing(sK123)
| ( ( xsd_integer(sK124)
| ~ xsd_string(sK124) )
& ( ~ xsd_integer(sK124)
| xsd_string(sK124) ) )
| ~ cC108(iV21026)
| ~ cC40(iV21026)
| ~ cC136(iV21026)
| ~ cC10(iV21026)
| ~ cC90(iV21026)
| ~ cowlThing(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC158(iV21026)
| ~ cC110(iV21026)
| ~ cC22(iV21026)
| ~ cC60(iV21026)
| ~ cC154(iV21026)
| ~ cC180(iV21026)
| ~ cC78(iV21026)
| ~ cC16(iV21026)
| ~ cC132(iV21026)
| ~ cC114(iV21026)
| ~ cC20(iV21026)
| ~ cC84(iV21026)
| ~ cC38(iV21026)
| ~ cC138(iV21026)
| ~ cC174(iV21026)
| ~ cC62(iV21026)
| ~ cC8(iV21026)
| ~ cC36(iV21026)
| ~ cC112(iV21026)
| ~ cC64(iV21026)
| ~ cC116(iV21026)
| ~ cC82(iV21026)
| ~ cC14(iV21026)
| ~ cC152(iV21026)
| ~ cC80(iV21026)
| ~ cC88(iV21026)
| ~ cC130(iV21026)
| ~ cC168(iV21026)
| ~ cC4(iV21026)
| ~ cC134(iV21026)
| ~ cC42(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC24(iV21027)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cowlThing(iV21029)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030) ),
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_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[],[f458]) ).
fof(f905,plain,
! [X0] :
( xsd_string(X0)
| xsd_integer(X0) ),
inference(cnf_transformation,[],[f458]) ).
fof(f906,plain,
! [X0] :
( cC4(X0)
| ~ cC10(X0) ),
inference(cnf_transformation,[],[f460]) ).
fof(f907,plain,
! [X0] :
( cC8(X0)
| ~ cC10(X0) ),
inference(cnf_transformation,[],[f460]) ).
fof(f936,plain,
! [X0] :
( ~ cC110(X0)
| cC108(X0) ),
inference(cnf_transformation,[],[f492]) ).
fof(f938,plain,
! [X0] :
( cC90(X0)
| ~ cC112(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] :
( cC22(X0)
| ~ cC158(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] :
( cC20(X0)
| ~ cC22(X0) ),
inference(cnf_transformation,[],[f695]) ).
fof(f1138,plain,
! [X0,X1] :
( cC24(X0)
| ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ),
inference(cnf_transformation,[],[f701]) ).
fof(f1158,plain,
! [X0,X1] :
( cC30(X0)
| ~ rR1(X0,X1)
| ~ cC12xcomp(X1) ),
inference(cnf_transformation,[],[f724]) ).
fof(f1178,plain,
! [X0] :
( ~ cC38(X0)
| cC36(X0) ),
inference(cnf_transformation,[],[f746]) ).
fof(f1185,plain,
! [X0] :
( ~ cC42(X0)
| cC38(X0) ),
inference(cnf_transformation,[],[f752]) ).
fof(f1186,plain,
! [X0] :
( ~ cC42(X0)
| cC40(X0) ),
inference(cnf_transformation,[],[f752]) ).
fof(f1192,plain,
! [X0,X1] :
( cC44(X0)
| ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ),
inference(cnf_transformation,[],[f758]) ).
fof(f1210,plain,
! [X0,X1] :
( cC50(X0)
| ~ rR1(X0,X1)
| ~ cC12xcomp(X1) ),
inference(cnf_transformation,[],[f778]) ).
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(f1242,plain,
! [X0] :
( ~ cC64(X0)
| cC62(X0) ),
inference(cnf_transformation,[],[f811]) ).
fof(f1243,plain,
! [X0] :
( ~ cC64(X0)
| cC60(X0) ),
inference(cnf_transformation,[],[f811]) ).
fof(f1249,plain,
! [X0,X1] :
( cC66(X0)
| ~ rR1(X0,X1)
| ~ cC2xcomp(X1) ),
inference(cnf_transformation,[],[f817]) ).
fof(f1266,plain,
! [X0,X1] :
( cC72(X0)
| ~ ra_Px24(X0,X1) ),
inference(cnf_transformation,[],[f838]) ).
fof(f1271,plain,
! [X0] :
( cC72xcomp(X0)
| ra_Px24(X0,sK109(X0)) ),
inference(cnf_transformation,[],[f844]) ).
fof(f1274,plain,
! [X0] :
( ~ cC72xcomp(X0)
| cC74(X0)
| ~ cC18xcomp(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] :
( ~ ra_Px87(X0,X1)
| ~ cC74xcomp(X0) ),
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(f1299,plain,
! [X0] :
( ~ cC86(X0)
| cC84(X0) ),
inference(cnf_transformation,[],[f870]) ).
fof(f1300,plain,
! [X0] :
( ~ cC86(X0)
| cC82(X0) ),
inference(cnf_transformation,[],[f870]) ).
fof(f1303,plain,
! [X0] :
( cC88(X0)
| ~ cTOP(X0) ),
inference(cnf_transformation,[],[f871]) ).
fof(f1305,plain,
! [X0] :
( ~ cC90(X0)
| cC86(X0) ),
inference(cnf_transformation,[],[f873]) ).
fof(f1306,plain,
! [X0] :
( ~ cC86(X0)
| cC90(X0)
| ~ cC88(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(f1393,plain,
cowlThing(iV21027),
inference(cnf_transformation,[],[f249]) ).
fof(f1397,plain,
rR1(iV21027,iV21036),
inference(cnf_transformation,[],[f253]) ).
fof(f1398,plain,
rR1(iV21027,iV21035),
inference(cnf_transformation,[],[f254]) ).
fof(f1423,plain,
cowlThing(iV21029),
inference(cnf_transformation,[],[f279]) ).
fof(f1426,plain,
rR1(iV21029,iV21034),
inference(cnf_transformation,[],[f282]) ).
fof(f1427,plain,
rR1(iV21029,iV21033),
inference(cnf_transformation,[],[f283]) ).
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(f1454,plain,
rR1(iV21030,iV21032),
inference(cnf_transformation,[],[f310]) ).
fof(f1457,plain,
cC2xcomp(iV21032),
inference(cnf_transformation,[],[f313]) ).
fof(f1464,plain,
cC12xcomp(iV21033),
inference(cnf_transformation,[],[f320]) ).
fof(f1470,plain,
cC2xcomp(iV21034),
inference(cnf_transformation,[],[f326]) ).
fof(f1476,plain,
cC12xcomp(iV21035),
inference(cnf_transformation,[],[f332]) ).
fof(f1482,plain,
cC2xcomp(iV21036),
inference(cnf_transformation,[],[f338]) ).
fof(f1487,plain,
( ~ cowlThing(sK123)
| cowlNothing(sK123)
| ~ xsd_integer(sK124)
| xsd_string(sK124)
| ~ cC108(iV21026)
| ~ cC40(iV21026)
| ~ cC136(iV21026)
| ~ cC10(iV21026)
| ~ cC90(iV21026)
| ~ cowlThing(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC158(iV21026)
| ~ cC110(iV21026)
| ~ cC22(iV21026)
| ~ cC60(iV21026)
| ~ cC154(iV21026)
| ~ cC180(iV21026)
| ~ cC78(iV21026)
| ~ cC16(iV21026)
| ~ cC132(iV21026)
| ~ cC114(iV21026)
| ~ cC20(iV21026)
| ~ cC84(iV21026)
| ~ cC38(iV21026)
| ~ cC138(iV21026)
| ~ cC174(iV21026)
| ~ cC62(iV21026)
| ~ cC8(iV21026)
| ~ cC36(iV21026)
| ~ cC112(iV21026)
| ~ cC64(iV21026)
| ~ cC116(iV21026)
| ~ cC82(iV21026)
| ~ cC14(iV21026)
| ~ cC152(iV21026)
| ~ cC80(iV21026)
| ~ cC88(iV21026)
| ~ cC130(iV21026)
| ~ cC168(iV21026)
| ~ cC4(iV21026)
| ~ cC134(iV21026)
| ~ cC42(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC24(iV21027)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cowlThing(iV21029)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030) ),
inference(cnf_transformation,[],[f901]) ).
fof(f1488,plain,
( ~ cowlThing(sK123)
| cowlNothing(sK123)
| xsd_integer(sK124)
| ~ xsd_string(sK124)
| ~ cC108(iV21026)
| ~ cC40(iV21026)
| ~ cC136(iV21026)
| ~ cC10(iV21026)
| ~ cC90(iV21026)
| ~ cowlThing(iV21026)
| ~ cC58(iV21026)
| ~ cC56(iV21026)
| ~ cC158(iV21026)
| ~ cC110(iV21026)
| ~ cC22(iV21026)
| ~ cC60(iV21026)
| ~ cC154(iV21026)
| ~ cC180(iV21026)
| ~ cC78(iV21026)
| ~ cC16(iV21026)
| ~ cC132(iV21026)
| ~ cC114(iV21026)
| ~ cC20(iV21026)
| ~ cC84(iV21026)
| ~ cC38(iV21026)
| ~ cC138(iV21026)
| ~ cC174(iV21026)
| ~ cC62(iV21026)
| ~ cC8(iV21026)
| ~ cC36(iV21026)
| ~ cC112(iV21026)
| ~ cC64(iV21026)
| ~ cC116(iV21026)
| ~ cC82(iV21026)
| ~ cC14(iV21026)
| ~ cC152(iV21026)
| ~ cC80(iV21026)
| ~ cC88(iV21026)
| ~ cC130(iV21026)
| ~ cC168(iV21026)
| ~ cC4(iV21026)
| ~ cC134(iV21026)
| ~ cC42(iV21026)
| ~ cC156(iV21026)
| ~ cC86(iV21026)
| ~ cC30(iV21027)
| ~ cowlThing(iV21027)
| ~ cC24(iV21027)
| ~ cC50(iV21029)
| ~ cC44(iV21029)
| ~ cowlThing(iV21029)
| ~ cC72(iV21030)
| ~ cC66(iV21030)
| ~ cowlThing(iV21030) ),
inference(cnf_transformation,[],[f901]) ).
fof(f1490,definition,
( spl125_1
<=> cowlThing(iV21030) ),
introduced(definition,[new_symbols(definition,[spl125_1])],[avatar_definition]) ).
fof(f1494,definition,
( spl125_2
<=> cC66(iV21030) ),
introduced(definition,[new_symbols(definition,[spl125_2])],[avatar_definition]) ).
fof(f1496,plain,
( ~ cC66(iV21030)
| spl125_2 ),
inference(avatar_component_clause,[],[f1494]) ).
fof(f1498,definition,
( spl125_3
<=> cC72(iV21030) ),
introduced(definition,[new_symbols(definition,[spl125_3])],[avatar_definition]) ).
fof(f1500,plain,
( ~ cC72(iV21030)
| spl125_3 ),
inference(avatar_component_clause,[],[f1498]) ).
fof(f1502,definition,
( spl125_4
<=> cowlThing(iV21029) ),
introduced(definition,[new_symbols(definition,[spl125_4])],[avatar_definition]) ).
fof(f1506,definition,
( spl125_5
<=> cC44(iV21029) ),
introduced(definition,[new_symbols(definition,[spl125_5])],[avatar_definition]) ).
fof(f1508,plain,
( ~ cC44(iV21029)
| spl125_5 ),
inference(avatar_component_clause,[],[f1506]) ).
fof(f1510,definition,
( spl125_6
<=> cC50(iV21029) ),
introduced(definition,[new_symbols(definition,[spl125_6])],[avatar_definition]) ).
fof(f1512,plain,
( ~ cC50(iV21029)
| spl125_6 ),
inference(avatar_component_clause,[],[f1510]) ).
fof(f1514,definition,
( spl125_7
<=> cC24(iV21027) ),
introduced(definition,[new_symbols(definition,[spl125_7])],[avatar_definition]) ).
fof(f1516,plain,
( ~ cC24(iV21027)
| spl125_7 ),
inference(avatar_component_clause,[],[f1514]) ).
fof(f1518,definition,
( spl125_8
<=> cowlThing(iV21027) ),
introduced(definition,[new_symbols(definition,[spl125_8])],[avatar_definition]) ).
fof(f1522,definition,
( spl125_9
<=> cC30(iV21027) ),
introduced(definition,[new_symbols(definition,[spl125_9])],[avatar_definition]) ).
fof(f1524,plain,
( ~ cC30(iV21027)
| spl125_9 ),
inference(avatar_component_clause,[],[f1522]) ).
fof(f1526,definition,
( spl125_10
<=> cC86(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_10])],[avatar_definition]) ).
fof(f1527,plain,
( cC86(iV21026)
| ~ spl125_10 ),
inference(avatar_component_clause,[],[f1526]) ).
fof(f1530,definition,
( spl125_11
<=> cC156(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_11])],[avatar_definition]) ).
fof(f1531,plain,
( cC156(iV21026)
| ~ spl125_11 ),
inference(avatar_component_clause,[],[f1530]) ).
fof(f1534,definition,
( spl125_12
<=> cC42(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_12])],[avatar_definition]) ).
fof(f1535,plain,
( cC42(iV21026)
| ~ spl125_12 ),
inference(avatar_component_clause,[],[f1534]) ).
fof(f1538,definition,
( spl125_13
<=> cC134(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_13])],[avatar_definition]) ).
fof(f1539,plain,
( cC134(iV21026)
| ~ spl125_13 ),
inference(avatar_component_clause,[],[f1538]) ).
fof(f1542,definition,
( spl125_14
<=> cC4(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_14])],[avatar_definition]) ).
fof(f1544,plain,
( ~ cC4(iV21026)
| spl125_14 ),
inference(avatar_component_clause,[],[f1542]) ).
fof(f1546,definition,
( spl125_15
<=> cC168(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_15])],[avatar_definition]) ).
fof(f1550,definition,
( spl125_16
<=> cC130(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_16])],[avatar_definition]) ).
fof(f1554,definition,
( spl125_17
<=> cC88(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_17])],[avatar_definition]) ).
fof(f1556,plain,
( ~ cC88(iV21026)
| spl125_17 ),
inference(avatar_component_clause,[],[f1554]) ).
fof(f1558,definition,
( spl125_18
<=> cC80(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_18])],[avatar_definition]) ).
fof(f1559,plain,
( cC80(iV21026)
| ~ spl125_18 ),
inference(avatar_component_clause,[],[f1558]) ).
fof(f1562,definition,
( spl125_19
<=> cC152(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_19])],[avatar_definition]) ).
fof(f1566,definition,
( spl125_20
<=> cC14(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_20])],[avatar_definition]) ).
fof(f1570,definition,
( spl125_21
<=> cC82(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_21])],[avatar_definition]) ).
fof(f1571,plain,
( cC82(iV21026)
| ~ spl125_21 ),
inference(avatar_component_clause,[],[f1570]) ).
fof(f1574,definition,
( spl125_22
<=> cC116(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_22])],[avatar_definition]) ).
fof(f1575,plain,
( cC116(iV21026)
| ~ spl125_22 ),
inference(avatar_component_clause,[],[f1574]) ).
fof(f1578,definition,
( spl125_23
<=> cC64(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_23])],[avatar_definition]) ).
fof(f1579,plain,
( cC64(iV21026)
| ~ spl125_23 ),
inference(avatar_component_clause,[],[f1578]) ).
fof(f1582,definition,
( spl125_24
<=> cC112(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_24])],[avatar_definition]) ).
fof(f1583,plain,
( cC112(iV21026)
| ~ spl125_24 ),
inference(avatar_component_clause,[],[f1582]) ).
fof(f1586,definition,
( spl125_25
<=> cC36(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_25])],[avatar_definition]) ).
fof(f1590,definition,
( spl125_26
<=> cC8(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_26])],[avatar_definition]) ).
fof(f1592,plain,
( ~ cC8(iV21026)
| spl125_26 ),
inference(avatar_component_clause,[],[f1590]) ).
fof(f1594,definition,
( spl125_27
<=> cC62(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_27])],[avatar_definition]) ).
fof(f1598,definition,
( spl125_28
<=> cC174(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_28])],[avatar_definition]) ).
fof(f1599,plain,
( cC174(iV21026)
| ~ spl125_28 ),
inference(avatar_component_clause,[],[f1598]) ).
fof(f1602,definition,
( spl125_29
<=> cC138(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_29])],[avatar_definition]) ).
fof(f1603,plain,
( cC138(iV21026)
| ~ spl125_29 ),
inference(avatar_component_clause,[],[f1602]) ).
fof(f1606,definition,
( spl125_30
<=> cC38(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_30])],[avatar_definition]) ).
fof(f1607,plain,
( cC38(iV21026)
| ~ spl125_30 ),
inference(avatar_component_clause,[],[f1606]) ).
fof(f1610,definition,
( spl125_31
<=> cC84(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_31])],[avatar_definition]) ).
fof(f1614,definition,
( spl125_32
<=> cC20(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_32])],[avatar_definition]) ).
fof(f1616,plain,
( ~ cC20(iV21026)
| spl125_32 ),
inference(avatar_component_clause,[],[f1614]) ).
fof(f1618,definition,
( spl125_33
<=> cC114(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_33])],[avatar_definition]) ).
fof(f1622,definition,
( spl125_34
<=> cC132(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_34])],[avatar_definition]) ).
fof(f1623,plain,
( cC132(iV21026)
| ~ spl125_34 ),
inference(avatar_component_clause,[],[f1622]) ).
fof(f1626,definition,
( spl125_35
<=> cC16(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_35])],[avatar_definition]) ).
fof(f1627,plain,
( cC16(iV21026)
| ~ spl125_35 ),
inference(avatar_component_clause,[],[f1626]) ).
fof(f1630,definition,
( spl125_36
<=> cC78(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_36])],[avatar_definition]) ).
fof(f1634,definition,
( spl125_37
<=> cC180(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_37])],[avatar_definition]) ).
fof(f1635,plain,
( cC180(iV21026)
| ~ spl125_37 ),
inference(avatar_component_clause,[],[f1634]) ).
fof(f1638,definition,
( spl125_38
<=> cC154(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_38])],[avatar_definition]) ).
fof(f1639,plain,
( cC154(iV21026)
| ~ spl125_38 ),
inference(avatar_component_clause,[],[f1638]) ).
fof(f1642,definition,
( spl125_39
<=> cC60(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_39])],[avatar_definition]) ).
fof(f1643,plain,
( cC60(iV21026)
| ~ spl125_39 ),
inference(avatar_component_clause,[],[f1642]) ).
fof(f1646,definition,
( spl125_40
<=> cC22(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_40])],[avatar_definition]) ).
fof(f1648,plain,
( ~ cC22(iV21026)
| spl125_40 ),
inference(avatar_component_clause,[],[f1646]) ).
fof(f1650,definition,
( spl125_41
<=> cC110(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_41])],[avatar_definition]) ).
fof(f1651,plain,
( cC110(iV21026)
| ~ spl125_41 ),
inference(avatar_component_clause,[],[f1650]) ).
fof(f1654,definition,
( spl125_42
<=> cC158(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_42])],[avatar_definition]) ).
fof(f1655,plain,
( cC158(iV21026)
| ~ spl125_42 ),
inference(avatar_component_clause,[],[f1654]) ).
fof(f1658,definition,
( spl125_43
<=> cC56(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_43])],[avatar_definition]) ).
fof(f1662,definition,
( spl125_44
<=> cC58(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_44])],[avatar_definition]) ).
fof(f1663,plain,
( cC58(iV21026)
| ~ spl125_44 ),
inference(avatar_component_clause,[],[f1662]) ).
fof(f1666,definition,
( spl125_45
<=> cowlThing(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_45])],[avatar_definition]) ).
fof(f1670,definition,
( spl125_46
<=> cC90(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_46])],[avatar_definition]) ).
fof(f1674,definition,
( spl125_47
<=> cC10(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_47])],[avatar_definition]) ).
fof(f1675,plain,
( cC10(iV21026)
| ~ spl125_47 ),
inference(avatar_component_clause,[],[f1674]) ).
fof(f1678,definition,
( spl125_48
<=> cC136(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_48])],[avatar_definition]) ).
fof(f1682,definition,
( spl125_49
<=> cC40(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_49])],[avatar_definition]) ).
fof(f1686,definition,
( spl125_50
<=> cC108(iV21026) ),
introduced(definition,[new_symbols(definition,[spl125_50])],[avatar_definition]) ).
fof(f1690,definition,
( spl125_51
<=> xsd_string(sK124) ),
introduced(definition,[new_symbols(definition,[spl125_51])],[avatar_definition]) ).
fof(f1691,plain,
( ~ xsd_string(sK124)
| spl125_51 ),
inference(avatar_component_clause,[],[f1690]) ).
fof(f1692,plain,
( xsd_string(sK124)
| ~ spl125_51 ),
inference(avatar_component_clause,[],[f1690]) ).
fof(f1694,definition,
( spl125_52
<=> xsd_integer(sK124) ),
introduced(definition,[new_symbols(definition,[spl125_52])],[avatar_definition]) ).
fof(f1695,plain,
( xsd_integer(sK124)
| ~ spl125_52 ),
inference(avatar_component_clause,[],[f1694]) ).
fof(f1698,definition,
( spl125_53
<=> cowlNothing(sK123) ),
introduced(definition,[new_symbols(definition,[spl125_53])],[avatar_definition]) ).
fof(f1700,plain,
( cowlNothing(sK123)
| ~ spl125_53 ),
inference(avatar_component_clause,[],[f1698]) ).
fof(f1702,definition,
( spl125_54
<=> cowlThing(sK123) ),
introduced(definition,[new_symbols(definition,[spl125_54])],[avatar_definition]) ).
fof(f1704,plain,
( ~ cowlThing(sK123)
| spl125_54 ),
inference(avatar_component_clause,[],[f1702]) ).
fof(f1705,plain,
( ~ spl125_1
| ~ spl125_2
| ~ spl125_3
| ~ spl125_4
| ~ spl125_5
| ~ spl125_6
| ~ spl125_7
| ~ spl125_8
| ~ spl125_9
| ~ spl125_10
| ~ spl125_11
| ~ spl125_12
| ~ spl125_13
| ~ spl125_14
| ~ spl125_15
| ~ spl125_16
| ~ spl125_17
| ~ spl125_18
| ~ spl125_19
| ~ spl125_20
| ~ spl125_21
| ~ spl125_22
| ~ spl125_23
| ~ spl125_24
| ~ spl125_25
| ~ spl125_26
| ~ spl125_27
| ~ spl125_28
| ~ spl125_29
| ~ spl125_30
| ~ spl125_31
| ~ spl125_32
| ~ spl125_33
| ~ spl125_34
| ~ spl125_35
| ~ spl125_36
| ~ spl125_37
| ~ spl125_38
| ~ spl125_39
| ~ spl125_40
| ~ spl125_41
| ~ spl125_42
| ~ spl125_43
| ~ spl125_44
| ~ spl125_45
| ~ spl125_46
| ~ spl125_47
| ~ spl125_48
| ~ spl125_49
| ~ spl125_50
| spl125_51
| ~ spl125_52
| spl125_53
| ~ spl125_54 ),
inference(avatar_split_clause,[],[f1487,f1702,f1698,f1694,f1690,f1686,f1682,f1678,f1674,f1670,f1666,f1662,f1658,f1654,f1650,f1646,f1642,f1638,f1634,f1630,f1626,f1622,f1618,f1614,f1610,f1606,f1602,f1598,f1594,f1590,f1586,f1582,f1578,f1574,f1570,f1566,f1562,f1558,f1554,f1550,f1546,f1542,f1538,f1534,f1530,f1526,f1522,f1518,f1514,f1510,f1506,f1502,f1498,f1494,f1490]) ).
fof(f1706,plain,
( ~ spl125_1
| ~ spl125_2
| ~ spl125_3
| ~ spl125_4
| ~ spl125_5
| ~ spl125_6
| ~ spl125_7
| ~ spl125_8
| ~ spl125_9
| ~ spl125_10
| ~ spl125_11
| ~ spl125_12
| ~ spl125_13
| ~ spl125_14
| ~ spl125_15
| ~ spl125_16
| ~ spl125_17
| ~ spl125_18
| ~ spl125_19
| ~ spl125_20
| ~ spl125_21
| ~ spl125_22
| ~ spl125_23
| ~ spl125_24
| ~ spl125_25
| ~ spl125_26
| ~ spl125_27
| ~ spl125_28
| ~ spl125_29
| ~ spl125_30
| ~ spl125_31
| ~ spl125_32
| ~ spl125_33
| ~ spl125_34
| ~ spl125_35
| ~ spl125_36
| ~ spl125_37
| ~ spl125_38
| ~ spl125_39
| ~ spl125_40
| ~ spl125_41
| ~ spl125_42
| ~ spl125_43
| ~ spl125_44
| ~ spl125_45
| ~ spl125_46
| ~ spl125_47
| ~ spl125_48
| ~ spl125_49
| ~ spl125_50
| ~ spl125_51
| spl125_52
| spl125_53
| ~ spl125_54 ),
inference(avatar_split_clause,[],[f1488,f1702,f1698,f1694,f1690,f1686,f1682,f1678,f1674,f1670,f1666,f1662,f1658,f1654,f1650,f1646,f1642,f1638,f1634,f1630,f1626,f1622,f1618,f1614,f1610,f1606,f1602,f1598,f1594,f1590,f1586,f1582,f1578,f1574,f1570,f1566,f1562,f1558,f1554,f1550,f1546,f1542,f1538,f1534,f1530,f1526,f1522,f1518,f1514,f1510,f1506,f1502,f1498,f1494,f1490]) ).
fof(f1707,plain,
spl125_1,
inference(avatar_split_clause,[],[f1451,f1490]) ).
fof(f1708,plain,
spl125_4,
inference(avatar_split_clause,[],[f1423,f1502]) ).
fof(f1709,plain,
spl125_8,
inference(avatar_split_clause,[],[f1393,f1518]) ).
fof(f1710,plain,
spl125_45,
inference(avatar_split_clause,[],[f1364,f1666]) ).
fof(f1713,plain,
! [X0] :
( ~ cC158(X0)
| cC16(X0) ),
inference(resolution,[],[f1131,f1056]) ).
fof(f1719,plain,
! [X0] :
( ~ cC112(X0)
| cC86(X0) ),
inference(resolution,[],[f1305,f938]) ).
fof(f1720,plain,
cC180(iV21026),
inference(resolution,[],[f1330,f1366]) ).
fof(f1721,plain,
spl125_37,
inference(avatar_split_clause,[],[f1720,f1634]) ).
fof(f1722,plain,
( cC174(iV21026)
| ~ spl125_37 ),
inference(resolution,[],[f1635,f1123]) ).
fof(f1724,plain,
( spl125_28
| ~ spl125_37 ),
inference(avatar_split_clause,[],[f1722,f1634,f1598]) ).
fof(f1726,plain,
( cC168(iV21026)
| ~ spl125_28 ),
inference(resolution,[],[f1599,f1103]) ).
fof(f1727,plain,
( spl125_15
| ~ spl125_28 ),
inference(avatar_split_clause,[],[f1726,f1598,f1546]) ).
fof(f1730,plain,
cC158(iV21026),
inference(resolution,[],[f1331,f1366]) ).
fof(f1731,plain,
spl125_42,
inference(avatar_split_clause,[],[f1730,f1654]) ).
fof(f1732,plain,
( cC156(iV21026)
| ~ spl125_42 ),
inference(resolution,[],[f1655,f1055]) ).
fof(f1733,plain,
( spl125_11
| ~ spl125_42 ),
inference(avatar_split_clause,[],[f1732,f1654,f1530]) ).
fof(f1734,plain,
( cC154(iV21026)
| ~ spl125_11 ),
inference(resolution,[],[f1531,f1053]) ).
fof(f1735,plain,
( cC138(iV21026)
| ~ spl125_11 ),
inference(resolution,[],[f1531,f1052]) ).
fof(f1736,plain,
( spl125_29
| ~ spl125_11 ),
inference(avatar_split_clause,[],[f1735,f1530,f1602]) ).
fof(f1737,plain,
( spl125_38
| ~ spl125_11 ),
inference(avatar_split_clause,[],[f1734,f1530,f1638]) ).
fof(f1738,plain,
( cC136(iV21026)
| ~ spl125_29 ),
inference(resolution,[],[f1603,f1001]) ).
fof(f1739,plain,
( cC134(iV21026)
| ~ spl125_29 ),
inference(resolution,[],[f1603,f1000]) ).
fof(f1740,plain,
( spl125_13
| ~ spl125_29 ),
inference(avatar_split_clause,[],[f1739,f1602,f1538]) ).
fof(f1741,plain,
( spl125_48
| ~ spl125_29 ),
inference(avatar_split_clause,[],[f1738,f1602,f1678]) ).
fof(f1742,plain,
( cC116(iV21026)
| ~ spl125_13 ),
inference(resolution,[],[f1539,f996]) ).
fof(f1743,plain,
( cC132(iV21026)
| ~ spl125_13 ),
inference(resolution,[],[f1539,f995]) ).
fof(f1744,plain,
( spl125_34
| ~ spl125_13 ),
inference(avatar_split_clause,[],[f1743,f1538,f1622]) ).
fof(f1745,plain,
( spl125_22
| ~ spl125_13 ),
inference(avatar_split_clause,[],[f1742,f1538,f1574]) ).
fof(f1746,plain,
( cC114(iV21026)
| ~ spl125_22 ),
inference(resolution,[],[f1575,f944]) ).
fof(f1747,plain,
( cC112(iV21026)
| ~ spl125_22 ),
inference(resolution,[],[f1575,f943]) ).
fof(f1748,plain,
( spl125_24
| ~ spl125_22 ),
inference(avatar_split_clause,[],[f1747,f1574,f1582]) ).
fof(f1749,plain,
( spl125_33
| ~ spl125_22 ),
inference(avatar_split_clause,[],[f1746,f1574,f1618]) ).
fof(f1750,plain,
( cC110(iV21026)
| ~ spl125_24 ),
inference(resolution,[],[f1583,f939]) ).
fof(f1751,plain,
( spl125_41
| ~ spl125_24 ),
inference(avatar_split_clause,[],[f1750,f1582,f1650]) ).
fof(f1753,plain,
( cC130(iV21026)
| ~ spl125_34 ),
inference(resolution,[],[f1623,f993]) ).
fof(f1755,plain,
( spl125_16
| ~ spl125_34 ),
inference(avatar_split_clause,[],[f1753,f1622,f1550]) ).
fof(f1758,plain,
( cC152(iV21026)
| ~ spl125_38 ),
inference(resolution,[],[f1639,f1050]) ).
fof(f1760,plain,
( spl125_19
| ~ spl125_38 ),
inference(avatar_split_clause,[],[f1758,f1638,f1562]) ).
fof(f1763,plain,
( cC108(iV21026)
| ~ spl125_41 ),
inference(resolution,[],[f1651,f936]) ).
fof(f1764,plain,
( spl125_50
| ~ spl125_41 ),
inference(avatar_split_clause,[],[f1763,f1650,f1686]) ).
fof(f1767,plain,
( cC16(iV21026)
| ~ spl125_42 ),
inference(resolution,[],[f1713,f1655]) ).
fof(f1768,plain,
( spl125_35
| ~ spl125_42 ),
inference(avatar_split_clause,[],[f1767,f1654,f1626]) ).
fof(f1769,plain,
( cC10(iV21026)
| ~ spl125_35 ),
inference(resolution,[],[f1627,f1059]) ).
fof(f1770,plain,
( cC14(iV21026)
| ~ spl125_35 ),
inference(resolution,[],[f1627,f1058]) ).
fof(f1771,plain,
( spl125_20
| ~ spl125_35 ),
inference(avatar_split_clause,[],[f1770,f1626,f1566]) ).
fof(f1772,plain,
( spl125_47
| ~ spl125_35 ),
inference(avatar_split_clause,[],[f1769,f1626,f1674]) ).
fof(f1773,plain,
( cC86(iV21026)
| ~ spl125_24 ),
inference(resolution,[],[f1719,f1583]) ).
fof(f1774,plain,
( spl125_10
| ~ spl125_24 ),
inference(avatar_split_clause,[],[f1773,f1582,f1526]) ).
fof(f1775,plain,
( cC82(iV21026)
| ~ spl125_10 ),
inference(resolution,[],[f1527,f1300]) ).
fof(f1776,plain,
( cC84(iV21026)
| ~ spl125_10 ),
inference(resolution,[],[f1527,f1299]) ).
fof(f1777,plain,
( spl125_31
| ~ spl125_10 ),
inference(avatar_split_clause,[],[f1776,f1526,f1610]) ).
fof(f1778,plain,
( spl125_21
| ~ spl125_10 ),
inference(avatar_split_clause,[],[f1775,f1526,f1570]) ).
fof(f1779,plain,
( cC64(iV21026)
| ~ spl125_21 ),
inference(resolution,[],[f1571,f1295]) ).
fof(f1780,plain,
( cC80(iV21026)
| ~ spl125_21 ),
inference(resolution,[],[f1571,f1294]) ).
fof(f1781,plain,
( spl125_18
| ~ spl125_21 ),
inference(avatar_split_clause,[],[f1780,f1570,f1558]) ).
fof(f1782,plain,
( spl125_23
| ~ spl125_21 ),
inference(avatar_split_clause,[],[f1779,f1570,f1578]) ).
fof(f1783,plain,
( cC78(iV21026)
| ~ spl125_18 ),
inference(resolution,[],[f1559,f1292]) ).
fof(f1785,plain,
( spl125_36
| ~ spl125_18 ),
inference(avatar_split_clause,[],[f1783,f1558,f1630]) ).
fof(f1786,plain,
( cC60(iV21026)
| ~ spl125_23 ),
inference(resolution,[],[f1579,f1243]) ).
fof(f1787,plain,
( cC62(iV21026)
| ~ spl125_23 ),
inference(resolution,[],[f1579,f1242]) ).
fof(f1788,plain,
( spl125_27
| ~ spl125_23 ),
inference(avatar_split_clause,[],[f1787,f1578,f1594]) ).
fof(f1789,plain,
( spl125_39
| ~ spl125_23 ),
inference(avatar_split_clause,[],[f1786,f1578,f1642]) ).
fof(f1794,plain,
( cC58(iV21026)
| ~ spl125_39 ),
inference(resolution,[],[f1643,f1238]) ).
fof(f1795,plain,
( cC42(iV21026)
| ~ spl125_39 ),
inference(resolution,[],[f1643,f1237]) ).
fof(f1796,plain,
( spl125_12
| ~ spl125_39 ),
inference(avatar_split_clause,[],[f1795,f1642,f1534]) ).
fof(f1797,plain,
( spl125_44
| ~ spl125_39 ),
inference(avatar_split_clause,[],[f1794,f1642,f1662]) ).
fof(f1798,plain,
( cC40(iV21026)
| ~ spl125_12 ),
inference(resolution,[],[f1535,f1186]) ).
fof(f1799,plain,
( cC38(iV21026)
| ~ spl125_12 ),
inference(resolution,[],[f1535,f1185]) ).
fof(f1800,plain,
( spl125_30
| ~ spl125_12 ),
inference(avatar_split_clause,[],[f1799,f1534,f1606]) ).
fof(f1801,plain,
( spl125_49
| ~ spl125_12 ),
inference(avatar_split_clause,[],[f1798,f1534,f1682]) ).
fof(f1802,plain,
( cC36(iV21026)
| ~ spl125_30 ),
inference(resolution,[],[f1607,f1178]) ).
fof(f1804,plain,
( spl125_25
| ~ spl125_30 ),
inference(avatar_split_clause,[],[f1802,f1606,f1586]) ).
fof(f1807,plain,
( cC56(iV21026)
| ~ spl125_44 ),
inference(resolution,[],[f1663,f1232]) ).
fof(f1809,plain,
( spl125_43
| ~ spl125_44 ),
inference(avatar_split_clause,[],[f1807,f1662,f1658]) ).
fof(f1841,plain,
( cC90(iV21026)
| ~ cC88(iV21026)
| ~ spl125_10 ),
inference(resolution,[],[f1306,f1527]) ).
fof(f1842,plain,
( ~ spl125_17
| spl125_46
| ~ spl125_10 ),
inference(avatar_split_clause,[],[f1841,f1526,f1670,f1554]) ).
fof(f1844,plain,
( ~ cTOP(iV21026)
| spl125_17 ),
inference(resolution,[],[f1556,f1303]) ).
fof(f1845,plain,
( $false
| spl125_17 ),
inference(forward_subsumption_resolution,[],[f1844,f1335]) ).
fof(f1846,plain,
spl125_17,
inference(avatar_contradiction_clause,[],[f1845]) ).
fof(f1857,plain,
( ! [X0] :
( ~ cC2xcomp(X0)
| ~ rR1(iV21030,X0) )
| spl125_2 ),
inference(resolution,[],[f1249,f1496]) ).
fof(f1863,plain,
( ~ rR1(iV21030,iV21032)
| spl125_2 ),
inference(resolution,[],[f1857,f1457]) ).
fof(f1868,plain,
( $false
| spl125_2 ),
inference(forward_subsumption_resolution,[],[f1863,f1454]) ).
fof(f1869,plain,
spl125_2,
inference(avatar_contradiction_clause,[],[f1868]) ).
fof(f1872,plain,
( ! [X0] : ~ ra_Px24(iV21030,X0)
| spl125_3 ),
inference(resolution,[],[f1500,f1266]) ).
fof(f1940,plain,
! [X0] :
( ra_Px24(X0,sK109(X0))
| ~ cC18xcomp(X0)
| cC74(X0) ),
inference(resolution,[],[f1274,f1271]) ).
fof(f2048,plain,
( ~ cC18xcomp(iV21030)
| cC74(iV21030)
| spl125_3 ),
inference(resolution,[],[f1940,f1872]) ).
fof(f2049,plain,
( cC74(iV21030)
| spl125_3 ),
inference(forward_subsumption_resolution,[],[f2048,f1438]) ).
fof(f2051,plain,
( ra_Px87(iV21030,sK110(iV21030))
| spl125_3 ),
inference(resolution,[],[f2049,f1275]) ).
fof(f2059,plain,
( ~ cC74xcomp(iV21030)
| spl125_3 ),
inference(resolution,[],[f2051,f1277]) ).
fof(f2060,plain,
( $false
| spl125_3 ),
inference(forward_subsumption_resolution,[],[f2059,f1452]) ).
fof(f2061,plain,
spl125_3,
inference(avatar_contradiction_clause,[],[f2060]) ).
fof(f2062,plain,
( ! [X0] :
( ~ cC2xcomp(X0)
| ~ rR1(iV21029,X0) )
| spl125_5 ),
inference(resolution,[],[f1508,f1192]) ).
fof(f2066,plain,
( ~ rR1(iV21029,iV21034)
| spl125_5 ),
inference(resolution,[],[f2062,f1470]) ).
fof(f2072,plain,
( $false
| spl125_5 ),
inference(forward_subsumption_resolution,[],[f2066,f1426]) ).
fof(f2073,plain,
spl125_5,
inference(avatar_contradiction_clause,[],[f2072]) ).
fof(f2076,plain,
( ! [X0] :
( ~ cC12xcomp(X0)
| ~ rR1(iV21029,X0) )
| spl125_6 ),
inference(resolution,[],[f1512,f1210]) ).
fof(f2083,plain,
( ~ rR1(iV21029,iV21033)
| spl125_6 ),
inference(resolution,[],[f2076,f1464]) ).
fof(f2088,plain,
( $false
| spl125_6 ),
inference(forward_subsumption_resolution,[],[f2083,f1427]) ).
fof(f2089,plain,
spl125_6,
inference(avatar_contradiction_clause,[],[f2088]) ).
fof(f2092,plain,
( ! [X0] :
( ~ cC2xcomp(X0)
| ~ rR1(iV21027,X0) )
| spl125_7 ),
inference(resolution,[],[f1516,f1138]) ).
fof(f2104,plain,
( ~ rR1(iV21027,iV21036)
| spl125_7 ),
inference(resolution,[],[f2092,f1482]) ).
fof(f2111,plain,
( $false
| spl125_7 ),
inference(forward_subsumption_resolution,[],[f2104,f1397]) ).
fof(f2112,plain,
spl125_7,
inference(avatar_contradiction_clause,[],[f2111]) ).
fof(f2113,plain,
( ! [X0] :
( ~ cC12xcomp(X0)
| ~ rR1(iV21027,X0) )
| spl125_9 ),
inference(resolution,[],[f1524,f1158]) ).
fof(f2121,plain,
( ~ rR1(iV21027,iV21035)
| spl125_9 ),
inference(resolution,[],[f2113,f1476]) ).
fof(f2127,plain,
( $false
| spl125_9 ),
inference(forward_subsumption_resolution,[],[f2121,f1398]) ).
fof(f2128,plain,
spl125_9,
inference(avatar_contradiction_clause,[],[f2127]) ).
fof(f2130,plain,
( ~ cC10(iV21026)
| spl125_14 ),
inference(resolution,[],[f1544,f906]) ).
fof(f2131,plain,
( $false
| spl125_14
| ~ spl125_47 ),
inference(forward_subsumption_resolution,[],[f2130,f1675]) ).
fof(f2132,plain,
( spl125_14
| ~ spl125_47 ),
inference(avatar_contradiction_clause,[],[f2131]) ).
fof(f2134,plain,
( ~ cC10(iV21026)
| spl125_26 ),
inference(resolution,[],[f1592,f907]) ).
fof(f2135,plain,
( $false
| spl125_26
| ~ spl125_47 ),
inference(forward_subsumption_resolution,[],[f2134,f1675]) ).
fof(f2136,plain,
( spl125_26
| ~ spl125_47 ),
inference(avatar_contradiction_clause,[],[f2135]) ).
fof(f2139,plain,
( ~ cC22(iV21026)
| spl125_32 ),
inference(resolution,[],[f1616,f1132]) ).
fof(f2143,plain,
( ~ spl125_40
| spl125_32 ),
inference(avatar_split_clause,[],[f2139,f1614,f1646]) ).
fof(f2144,plain,
( ~ cC158(iV21026)
| spl125_40 ),
inference(resolution,[],[f1648,f1056]) ).
fof(f2145,plain,
( $false
| spl125_40
| ~ spl125_42 ),
inference(forward_subsumption_resolution,[],[f2144,f1655]) ).
fof(f2146,plain,
( spl125_40
| ~ spl125_42 ),
inference(avatar_contradiction_clause,[],[f2145]) ).
fof(f2147,plain,
( $false
| spl125_54 ),
inference(forward_subsumption_resolution,[],[f1704,f903]) ).
fof(f2148,plain,
spl125_54,
inference(avatar_contradiction_clause,[],[f2147]) ).
fof(f2156,plain,
( xsd_integer(sK124)
| spl125_51 ),
inference(resolution,[],[f1691,f905]) ).
fof(f2157,plain,
( spl125_52
| spl125_51 ),
inference(avatar_split_clause,[],[f2156,f1690,f1694]) ).
fof(f2158,plain,
( $false
| ~ spl125_53 ),
inference(forward_subsumption_resolution,[],[f1700,f902]) ).
fof(f2159,plain,
~ spl125_53,
inference(avatar_contradiction_clause,[],[f2158]) ).
fof(f2160,plain,
( ~ xsd_string(sK124)
| ~ spl125_52 ),
inference(resolution,[],[f1695,f904]) ).
fof(f2161,plain,
( $false
| ~ spl125_51
| ~ spl125_52 ),
inference(forward_subsumption_resolution,[],[f2160,f1692]) ).
fof(f2162,plain,
( ~ spl125_51
| ~ spl125_52 ),
inference(avatar_contradiction_clause,[],[f2161]) ).
cnf(s1,plain,
( ~ spl125_1
| ~ spl125_2
| ~ spl125_3
| ~ spl125_4
| ~ spl125_5
| ~ spl125_6
| ~ spl125_7
| ~ spl125_8
| ~ spl125_9
| ~ spl125_10
| ~ spl125_11
| ~ spl125_12
| ~ spl125_13
| ~ spl125_14
| ~ spl125_15
| ~ spl125_16
| ~ spl125_17
| ~ spl125_18
| ~ spl125_19
| ~ spl125_20
| ~ spl125_21
| ~ spl125_22
| ~ spl125_23
| ~ spl125_24
| ~ spl125_25
| ~ spl125_26
| ~ spl125_27
| ~ spl125_28
| ~ spl125_29
| ~ spl125_30
| ~ spl125_31
| ~ spl125_32
| ~ spl125_33
| ~ spl125_34
| ~ spl125_35
| ~ spl125_36
| ~ spl125_37
| ~ spl125_38
| ~ spl125_39
| ~ spl125_40
| ~ spl125_41
| ~ spl125_42
| ~ spl125_43
| ~ spl125_44
| ~ spl125_45
| ~ spl125_46
| ~ spl125_47
| ~ spl125_48
| ~ spl125_49
| ~ spl125_50
| spl125_51
| ~ spl125_52
| spl125_53
| ~ spl125_54 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s2,plain,
( ~ spl125_1
| ~ spl125_2
| ~ spl125_3
| ~ spl125_4
| ~ spl125_5
| ~ spl125_6
| ~ spl125_7
| ~ spl125_8
| ~ spl125_9
| ~ spl125_10
| ~ spl125_11
| ~ spl125_12
| ~ spl125_13
| ~ spl125_14
| ~ spl125_15
| ~ spl125_16
| ~ spl125_17
| ~ spl125_18
| ~ spl125_19
| ~ spl125_20
| ~ spl125_21
| ~ spl125_22
| ~ spl125_23
| ~ spl125_24
| ~ spl125_25
| ~ spl125_26
| ~ spl125_27
| ~ spl125_28
| ~ spl125_29
| ~ spl125_30
| ~ spl125_31
| ~ spl125_32
| ~ spl125_33
| ~ spl125_34
| ~ spl125_35
| ~ spl125_36
| ~ spl125_37
| ~ spl125_38
| ~ spl125_39
| ~ spl125_40
| ~ spl125_41
| ~ spl125_42
| ~ spl125_43
| ~ spl125_44
| ~ spl125_45
| ~ spl125_46
| ~ spl125_47
| ~ spl125_48
| ~ spl125_49
| ~ spl125_50
| ~ spl125_51
| spl125_52
| spl125_53
| ~ spl125_54 ),
inference(sat_conversion,[],[f1706]) ).
cnf(s3,plain,
spl125_1,
inference(sat_conversion,[],[f1707]) ).
cnf(s4,plain,
spl125_4,
inference(sat_conversion,[],[f1708]) ).
cnf(s5,plain,
spl125_8,
inference(sat_conversion,[],[f1709]) ).
cnf(s6,plain,
spl125_45,
inference(sat_conversion,[],[f1710]) ).
cnf(s7,plain,
spl125_37,
inference(sat_conversion,[],[f1721]) ).
cnf(s8,plain,
( spl125_28
| ~ spl125_37 ),
inference(sat_conversion,[],[f1724]) ).
cnf(s9,plain,
( spl125_15
| ~ spl125_28 ),
inference(sat_conversion,[],[f1727]) ).
cnf(s10,plain,
spl125_42,
inference(sat_conversion,[],[f1731]) ).
cnf(s11,plain,
( spl125_11
| ~ spl125_42 ),
inference(sat_conversion,[],[f1733]) ).
cnf(s12,plain,
( ~ spl125_11
| spl125_29 ),
inference(sat_conversion,[],[f1736]) ).
cnf(s13,plain,
( ~ spl125_11
| spl125_38 ),
inference(sat_conversion,[],[f1737]) ).
cnf(s14,plain,
( spl125_13
| ~ spl125_29 ),
inference(sat_conversion,[],[f1740]) ).
cnf(s15,plain,
( ~ spl125_29
| spl125_48 ),
inference(sat_conversion,[],[f1741]) ).
cnf(s16,plain,
( ~ spl125_13
| spl125_34 ),
inference(sat_conversion,[],[f1744]) ).
cnf(s17,plain,
( ~ spl125_13
| spl125_22 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s18,plain,
( ~ spl125_22
| spl125_24 ),
inference(sat_conversion,[],[f1748]) ).
cnf(s19,plain,
( ~ spl125_22
| spl125_33 ),
inference(sat_conversion,[],[f1749]) ).
cnf(s20,plain,
( ~ spl125_24
| spl125_41 ),
inference(sat_conversion,[],[f1751]) ).
cnf(s21,plain,
( spl125_16
| ~ spl125_34 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s22,plain,
( spl125_19
| ~ spl125_38 ),
inference(sat_conversion,[],[f1760]) ).
cnf(s23,plain,
( ~ spl125_41
| spl125_50 ),
inference(sat_conversion,[],[f1764]) ).
cnf(s24,plain,
( spl125_35
| ~ spl125_42 ),
inference(sat_conversion,[],[f1768]) ).
cnf(s25,plain,
( spl125_20
| ~ spl125_35 ),
inference(sat_conversion,[],[f1771]) ).
cnf(s26,plain,
( ~ spl125_35
| spl125_47 ),
inference(sat_conversion,[],[f1772]) ).
cnf(s27,plain,
( spl125_10
| ~ spl125_24 ),
inference(sat_conversion,[],[f1774]) ).
cnf(s28,plain,
( ~ spl125_10
| spl125_31 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s29,plain,
( ~ spl125_10
| spl125_21 ),
inference(sat_conversion,[],[f1778]) ).
cnf(s30,plain,
( spl125_18
| ~ spl125_21 ),
inference(sat_conversion,[],[f1781]) ).
cnf(s31,plain,
( ~ spl125_21
| spl125_23 ),
inference(sat_conversion,[],[f1782]) ).
cnf(s32,plain,
( ~ spl125_18
| spl125_36 ),
inference(sat_conversion,[],[f1785]) ).
cnf(s33,plain,
( ~ spl125_23
| spl125_27 ),
inference(sat_conversion,[],[f1788]) ).
cnf(s34,plain,
( ~ spl125_23
| spl125_39 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s35,plain,
( spl125_12
| ~ spl125_39 ),
inference(sat_conversion,[],[f1796]) ).
cnf(s36,plain,
( ~ spl125_39
| spl125_44 ),
inference(sat_conversion,[],[f1797]) ).
cnf(s37,plain,
( ~ spl125_12
| spl125_30 ),
inference(sat_conversion,[],[f1800]) ).
cnf(s38,plain,
( ~ spl125_12
| spl125_49 ),
inference(sat_conversion,[],[f1801]) ).
cnf(s39,plain,
( spl125_25
| ~ spl125_30 ),
inference(sat_conversion,[],[f1804]) ).
cnf(s40,plain,
( spl125_43
| ~ spl125_44 ),
inference(sat_conversion,[],[f1809]) ).
cnf(s41,plain,
( ~ spl125_10
| ~ spl125_17
| spl125_46 ),
inference(sat_conversion,[],[f1842]) ).
cnf(s42,plain,
spl125_17,
inference(sat_conversion,[],[f1846]) ).
cnf(s44,plain,
spl125_2,
inference(sat_conversion,[],[f1869]) ).
cnf(s46,plain,
spl125_3,
inference(sat_conversion,[],[f2061]) ).
cnf(s47,plain,
spl125_5,
inference(sat_conversion,[],[f2073]) ).
cnf(s48,plain,
spl125_6,
inference(sat_conversion,[],[f2089]) ).
cnf(s49,plain,
spl125_7,
inference(sat_conversion,[],[f2112]) ).
cnf(s50,plain,
spl125_9,
inference(sat_conversion,[],[f2128]) ).
cnf(s51,plain,
( spl125_14
| ~ spl125_47 ),
inference(sat_conversion,[],[f2132]) ).
cnf(s52,plain,
( spl125_26
| ~ spl125_47 ),
inference(sat_conversion,[],[f2136]) ).
cnf(s55,plain,
( spl125_32
| ~ spl125_40 ),
inference(sat_conversion,[],[f2143]) ).
cnf(s56,plain,
( spl125_40
| ~ spl125_42 ),
inference(sat_conversion,[],[f2146]) ).
cnf(s57,plain,
spl125_54,
inference(sat_conversion,[],[f2148]) ).
cnf(s59,plain,
( spl125_51
| spl125_52 ),
inference(sat_conversion,[],[f2157]) ).
cnf(s60,plain,
~ spl125_53,
inference(sat_conversion,[],[f2159]) ).
cnf(s61,plain,
( ~ spl125_51
| ~ spl125_52 ),
inference(sat_conversion,[],[f2162]) ).
cnf(s62,plain,
( ~ spl125_10
| spl125_46 ),
inference(rat,[],[s41,s42]) ).
cnf(s63,plain,
spl125_40,
inference(rat,[],[s56,s10]) ).
cnf(s64,plain,
spl125_35,
inference(rat,[],[s24,s10]) ).
cnf(s65,plain,
spl125_11,
inference(rat,[],[s11,s10]) ).
cnf(s66,plain,
spl125_32,
inference(rat,[],[s55,s63]) ).
cnf(s67,plain,
spl125_47,
inference(rat,[],[s26,s64]) ).
cnf(s68,plain,
spl125_20,
inference(rat,[],[s25,s64]) ).
cnf(s69,plain,
spl125_38,
inference(rat,[],[s13,s65]) ).
cnf(s70,plain,
spl125_29,
inference(rat,[],[s12,s65]) ).
cnf(s71,plain,
spl125_26,
inference(rat,[],[s52,s67]) ).
cnf(s72,plain,
spl125_14,
inference(rat,[],[s51,s67]) ).
cnf(s73,plain,
spl125_19,
inference(rat,[],[s22,s69]) ).
cnf(s74,plain,
spl125_48,
inference(rat,[],[s15,s70]) ).
cnf(s75,plain,
spl125_13,
inference(rat,[],[s14,s70]) ).
cnf(s76,plain,
spl125_22,
inference(rat,[],[s17,s75]) ).
cnf(s77,plain,
spl125_34,
inference(rat,[],[s16,s75]) ).
cnf(s78,plain,
spl125_33,
inference(rat,[],[s19,s76]) ).
cnf(s79,plain,
spl125_24,
inference(rat,[],[s18,s76]) ).
cnf(s80,plain,
spl125_16,
inference(rat,[],[s21,s77]) ).
cnf(s81,plain,
spl125_10,
inference(rat,[],[s27,s79]) ).
cnf(s82,plain,
spl125_41,
inference(rat,[],[s20,s79]) ).
cnf(s83,plain,
spl125_46,
inference(rat,[],[s62,s81]) ).
cnf(s84,plain,
spl125_21,
inference(rat,[],[s29,s81]) ).
cnf(s85,plain,
spl125_31,
inference(rat,[],[s28,s81]) ).
cnf(s86,plain,
spl125_50,
inference(rat,[],[s23,s82]) ).
cnf(s87,plain,
spl125_23,
inference(rat,[],[s31,s84]) ).
cnf(s88,plain,
spl125_18,
inference(rat,[],[s30,s84]) ).
cnf(s89,plain,
spl125_39,
inference(rat,[],[s34,s87]) ).
cnf(s90,plain,
spl125_27,
inference(rat,[],[s33,s87]) ).
cnf(s91,plain,
spl125_36,
inference(rat,[],[s32,s88]) ).
cnf(s92,plain,
spl125_44,
inference(rat,[],[s36,s89]) ).
cnf(s93,plain,
spl125_12,
inference(rat,[],[s35,s89]) ).
cnf(s94,plain,
spl125_43,
inference(rat,[],[s40,s92]) ).
cnf(s95,plain,
spl125_49,
inference(rat,[],[s38,s93]) ).
cnf(s96,plain,
spl125_30,
inference(rat,[],[s37,s93]) ).
cnf(s97,plain,
spl125_25,
inference(rat,[],[s39,s96]) ).
cnf(s98,plain,
spl125_28,
inference(rat,[],[s8,s7]) ).
cnf(s99,plain,
spl125_15,
inference(rat,[],[s9,s98]) ).
cnf(s100,plain,
( ~ spl125_51
| spl125_52 ),
inference(rat,[],[s2,s57,s60,s86,s95,s74,s67,s83,s6,s92,s94,s10,s82,s63,s89,s69,s7,s91,s64,s77,s78,s66,s85,s96,s70,s98,s90,s71,s97,s79,s87,s76,s84,s68,s73,s88,s42,s80,s99,s72,s75,s93,s65,s81,s50,s5,s49,s48,s47,s4,s46,s44,s3]) ).
cnf(s101,plain,
( spl125_51
| ~ spl125_52 ),
inference(rat,[],[s1,s57,s60,s86,s95,s74,s67,s83,s6,s92,s94,s10,s82,s63,s89,s69,s7,s91,s64,s77,s78,s66,s85,s96,s70,s98,s90,s71,s97,s79,s87,s76,s84,s68,s73,s88,s42,s80,s99,s72,s75,s93,s65,s81,s50,s5,s49,s48,s47,s4,s46,s44,s3]) ).
cnf(s102,plain,
spl125_51,
inference(rat,[],[s101,s59]) ).
cnf(s103,plain,
~ spl125_52,
inference(rat,[],[s61,s102]) ).
cnf(s104,plain,
$false,
inference(rat,[],[s100,s103,s102]) ).
fof(f2163,plain,
$false,
inference(avatar_sat_refutation,[],[s104]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KRS159+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n015.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 : Sun Sep 27 13:35:45 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.41 Running first-order theorem proving
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.92/1.32 % (1679291)Detected formulas, will run a generic FOF schedule.
% 2.92/1.32 % (1679296)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4134082970:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.92/1.32 % (1679298)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2348662624:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.92/1.32 % (1679301)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=761852735:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.92/1.32 % (1679300)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=408801494:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.92/1.32 % (1679299)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=896312254:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.92/1.32 % (1679302)dis-21_1_sil=8000:lcm=predicate:random_seed=4121675109:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.92/1.32 % (1679297)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=2806210647:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.92/1.32 % (1679300)Refutation not found, incomplete strategy
% 2.92/1.32 % (1679300)------------------------------
% 2.92/1.32 % (1679300)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.32 % (1679300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.32 % (1679299)Refutation not found, incomplete strategy
% 2.92/1.32 % (1679299)------------------------------
% 2.92/1.32 % (1679299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.32 % (1679299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.32 % (1679300)CaDiCaL version: 2.1.3
% 2.92/1.32 % (1679300)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.32 % (1679300)Time elapsed: 0.002 s
% 2.92/1.32 % (1679300)Peak memory usage: 87 MB
% 2.92/1.32 % (1679299)CaDiCaL version: 2.1.3
% 2.92/1.32 % (1679300)Instructions burned: 2 (million)
% 2.92/1.32 % (1679299)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.32 % (1679299)Time elapsed: 0.002 s
% 2.92/1.32 % (1679299)Peak memory usage: 87 MB
% 2.92/1.32 % (1679299)Instructions burned: 1 (million)
% 2.92/1.32 % (1679301)First to succeed.
% 2.92/1.32 % (1679301)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1679291"
% 2.92/1.32 % (1679302)Instruction limit reached!
% 2.92/1.32 % (1679302)------------------------------
% 2.92/1.32 % (1679302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.32 % (1679302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.32 % (1679302)CaDiCaL version: 2.1.3
% 2.92/1.32 % (1679302)Termination reason: Instruction limit
% 2.92/1.32 % (1679302)Termination phase: Saturation
% 2.92/1.32 % (1679302)Time elapsed: 0.060 s
% 2.92/1.32 % (1679302)Peak memory usage: 89 MB
% 2.92/1.32 % (1679302)Instructions burned: 130 (million)
% 2.92/1.32 % (1679310)lrs+10_1_sil=8000:sp=occurrence:random_seed=183298395:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 2.92/1.32 % (1679310)Refutation not found, incomplete strategy
% 2.92/1.32 % (1679310)------------------------------
% 2.92/1.32 % (1679310)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.92/1.32 % (1679310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/1.32 % (1679310)CaDiCaL version: 2.1.3
% 2.92/1.32 % (1679310)Termination reason: Refutation not found, incomplete strategy
% 2.92/1.32 % (1679310)Time elapsed: 0.019 s
% 2.92/1.32 % (1679310)Peak memory usage: 89 MB
% 2.92/1.32 % (1679310)Instructions burned: 33 (million)
% 2.92/1.32 % (1679299)------------------------------
% 2.92/1.32 % (1679299)------------------------------
% 2.92/1.32 % (1679300)------------------------------
% 2.92/1.32 % (1679300)------------------------------
% 2.92/1.32 % (1679301)Refutation found. Thanks to Tanya!
% 2.92/1.32 % SZS status Theorem for theBenchmark
% 2.92/1.32 % SZS output start Proof for theBenchmark
% See solution above
% 3.79/1.42 % (1679301)------------------------------
% 3.79/1.42 % (1679301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.79/1.42 % (1679301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.79/1.42 % (1679301)CaDiCaL version: 2.1.3
% 3.79/1.42 % (1679301)Termination reason: Refutation
% 3.79/1.42 % (1679301)Time elapsed: 0.028 s
% 3.79/1.42 % (1679301)Peak memory usage: 90 MB
% 3.79/1.42 % (1679301)Instructions burned: 44 (million)
% 3.79/1.42 % (1679301)------------------------------
% 3.79/1.42 % (1679301)------------------------------
% 3.79/1.42 % (1679291)Success in time 0.465 s
% 3.79/1.42 % Vampire exiting
%------------------------------------------------------------------------------