%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n009.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:42:25 AM UTC 2026
% Result : Theorem 0.18s 0.50s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 117
% Syntax : Number of formulae : 533 ( 130 unt; 56 def)
% Number of atoms : 1890 ( 0 equ)
% Maximal formula atoms : 56 ( 3 avg)
% Number of connectives : 2282 ( 925 ~; 920 |; 333 &)
% ( 101 <=>; 2 =>; 0 <=; 1 <~>)
% Maximal formula depth : 56 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 120 ( 119 usr; 57 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 11 con; 0-1 aty)
% Number of variables : 256 ( 0 sgn 226 !; 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(f18,axiom,
! [X0] :
( cC114(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_17) ).
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(f43,axiom,
! [X0] :
( cC136(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_42) ).
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(f123,axiom,
! [X0] :
( cC40(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_122) ).
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(f148,axiom,
! [X0] :
( cC62(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_147) ).
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(f172,axiom,
! [X0] :
( cC84(X0)
<=> cTOP(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_171) ).
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(f495,plain,
! [X0] :
( ( cC114(X0)
| ~ cTOP(X0) )
& ( cTOP(X0)
| ~ cC114(X0) ) ),
inference(nnf_transformation,[],[f18]) ).
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(f553,plain,
! [X0] :
( ( cC136(X0)
| ~ cTOP(X0) )
& ( cTOP(X0)
| ~ cC136(X0) ) ),
inference(nnf_transformation,[],[f43]) ).
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(f750,plain,
! [X0] :
( ( cC40(X0)
| ~ cTOP(X0) )
& ( cTOP(X0)
| ~ cC40(X0) ) ),
inference(nnf_transformation,[],[f123]) ).
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(f809,plain,
! [X0] :
( ( cC62(X0)
| ~ cTOP(X0) )
& ( cTOP(X0)
| ~ cC62(X0) ) ),
inference(nnf_transformation,[],[f148]) ).
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(f868,plain,
! [X0] :
( ( cC84(X0)
| ~ cTOP(X0) )
& ( cTOP(X0)
| ~ cC84(X0) ) ),
inference(nnf_transformation,[],[f172]) ).
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_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(f942,plain,
! [X0] :
( ~ cTOP(X0)
| cC114(X0) ),
inference(cnf_transformation,[],[f495]) ).
fof(f943,plain,
! [X0] :
( ~ cC116(X0)
| cC112(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(f999,plain,
! [X0] :
( ~ cTOP(X0)
| cC136(X0) ),
inference(cnf_transformation,[],[f553]) ).
fof(f1000,plain,
! [X0] :
( ~ cC138(X0)
| cC134(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(f1138,plain,
! [X0,X1] :
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC24(X0) ),
inference(cnf_transformation,[],[f701]) ).
fof(f1158,plain,
! [X0,X1] :
( ~ cC12xcomp(X1)
| ~ rR1(X0,X1)
| cC30(X0) ),
inference(cnf_transformation,[],[f724]) ).
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(f1192,plain,
! [X0,X1] :
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC44(X0) ),
inference(cnf_transformation,[],[f758]) ).
fof(f1210,plain,
! [X0,X1] :
( ~ cC12xcomp(X1)
| ~ rR1(X0,X1)
| cC50(X0) ),
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(f1241,plain,
! [X0] :
( ~ cTOP(X0)
| cC62(X0) ),
inference(cnf_transformation,[],[f809]) ).
fof(f1243,plain,
! [X0] :
( ~ cC64(X0)
| cC60(X0) ),
inference(cnf_transformation,[],[f811]) ).
fof(f1249,plain,
! [X0,X1] :
( ~ cC2xcomp(X1)
| ~ rR1(X0,X1)
| cC66(X0) ),
inference(cnf_transformation,[],[f817]) ).
fof(f1266,plain,
! [X0,X1] :
( ~ ra_Px24(X0,X1)
| cC72(X0) ),
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] :
( ~ 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(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(f1510,definition,
( spl125_6
<=> cC50(iV21029) ),
introduced(definition,[new_symbols(definition,[spl125_6])],[avatar_definition]) ).
fof(f1514,definition,
( spl125_7
<=> cC24(iV21027) ),
introduced(definition,[new_symbols(definition,[spl125_7])],[avatar_definition]) ).
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(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(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(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(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(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(f1647,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(f1671,plain,
( cC90(iV21026)
| ~ spl125_46 ),
inference(avatar_component_clause,[],[f1670]) ).
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(f1696,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(f1712,plain,
cC114(iV21026),
inference(resolution,[],[f942,f1335]) ).
fof(f1713,plain,
spl125_33,
inference(avatar_split_clause,[],[f1712,f1618]) ).
fof(f1715,plain,
cC136(iV21026),
inference(resolution,[],[f999,f1335]) ).
fof(f1716,plain,
spl125_48,
inference(avatar_split_clause,[],[f1715,f1678]) ).
fof(f1718,plain,
cC40(iV21026),
inference(resolution,[],[f1184,f1335]) ).
fof(f1719,plain,
spl125_49,
inference(avatar_split_clause,[],[f1718,f1682]) ).
fof(f1721,plain,
cC62(iV21026),
inference(resolution,[],[f1241,f1335]) ).
fof(f1722,plain,
spl125_27,
inference(avatar_split_clause,[],[f1721,f1594]) ).
fof(f1724,plain,
cC84(iV21026),
inference(resolution,[],[f1298,f1335]) ).
fof(f1725,plain,
spl125_31,
inference(avatar_split_clause,[],[f1724,f1610]) ).
fof(f1727,plain,
cC88(iV21026),
inference(resolution,[],[f1303,f1335]) ).
fof(f1728,plain,
spl125_17,
inference(avatar_split_clause,[],[f1727,f1554]) ).
fof(f1730,plain,
cC180(iV21026),
inference(resolution,[],[f1330,f1366]) ).
fof(f1731,plain,
spl125_37,
inference(avatar_split_clause,[],[f1730,f1634]) ).
fof(f1732,plain,
( cC174(iV21026)
| ~ spl125_37 ),
inference(resolution,[],[f1635,f1123]) ).
fof(f1734,plain,
( spl125_28
| ~ spl125_37 ),
inference(avatar_split_clause,[],[f1732,f1634,f1598]) ).
fof(f1736,plain,
( cC168(iV21026)
| ~ spl125_28 ),
inference(resolution,[],[f1599,f1103]) ).
fof(f1737,plain,
( spl125_15
| ~ spl125_28 ),
inference(avatar_split_clause,[],[f1736,f1598,f1546]) ).
fof(f1740,plain,
cC158(iV21026),
inference(resolution,[],[f1331,f1366]) ).
fof(f1741,plain,
spl125_42,
inference(avatar_split_clause,[],[f1740,f1654]) ).
fof(f1742,plain,
( cC22(iV21026)
| ~ spl125_42 ),
inference(resolution,[],[f1655,f1056]) ).
fof(f1743,plain,
( cC156(iV21026)
| ~ spl125_42 ),
inference(resolution,[],[f1655,f1055]) ).
fof(f1744,plain,
( spl125_11
| ~ spl125_42 ),
inference(avatar_split_clause,[],[f1743,f1654,f1530]) ).
fof(f1745,plain,
( spl125_40
| ~ spl125_42 ),
inference(avatar_split_clause,[],[f1742,f1654,f1646]) ).
fof(f1746,plain,
( cC154(iV21026)
| ~ spl125_11 ),
inference(resolution,[],[f1531,f1053]) ).
fof(f1747,plain,
( cC138(iV21026)
| ~ spl125_11 ),
inference(resolution,[],[f1531,f1052]) ).
fof(f1748,plain,
( spl125_29
| ~ spl125_11 ),
inference(avatar_split_clause,[],[f1747,f1530,f1602]) ).
fof(f1749,plain,
( spl125_38
| ~ spl125_11 ),
inference(avatar_split_clause,[],[f1746,f1530,f1638]) ).
fof(f1751,plain,
( cC134(iV21026)
| ~ spl125_29 ),
inference(resolution,[],[f1603,f1000]) ).
fof(f1752,plain,
( spl125_13
| ~ spl125_29 ),
inference(avatar_split_clause,[],[f1751,f1602,f1538]) ).
fof(f1753,plain,
( cC116(iV21026)
| ~ spl125_13 ),
inference(resolution,[],[f1539,f996]) ).
fof(f1754,plain,
( cC132(iV21026)
| ~ spl125_13 ),
inference(resolution,[],[f1539,f995]) ).
fof(f1755,plain,
( spl125_34
| ~ spl125_13 ),
inference(avatar_split_clause,[],[f1754,f1538,f1622]) ).
fof(f1756,plain,
( spl125_22
| ~ spl125_13 ),
inference(avatar_split_clause,[],[f1753,f1538,f1574]) ).
fof(f1758,plain,
( cC112(iV21026)
| ~ spl125_22 ),
inference(resolution,[],[f1575,f943]) ).
fof(f1759,plain,
( spl125_24
| ~ spl125_22 ),
inference(avatar_split_clause,[],[f1758,f1574,f1582]) ).
fof(f1760,plain,
( cC110(iV21026)
| ~ spl125_24 ),
inference(resolution,[],[f1583,f939]) ).
fof(f1761,plain,
( cC90(iV21026)
| ~ spl125_24 ),
inference(resolution,[],[f1583,f938]) ).
fof(f1762,plain,
( spl125_46
| ~ spl125_24 ),
inference(avatar_split_clause,[],[f1761,f1582,f1670]) ).
fof(f1763,plain,
( spl125_41
| ~ spl125_24 ),
inference(avatar_split_clause,[],[f1760,f1582,f1650]) ).
fof(f1764,plain,
( cC130(iV21026)
| ~ spl125_34 ),
inference(resolution,[],[f1623,f993]) ).
fof(f1766,plain,
( spl125_16
| ~ spl125_34 ),
inference(avatar_split_clause,[],[f1764,f1622,f1550]) ).
fof(f1769,plain,
( cC152(iV21026)
| ~ spl125_38 ),
inference(resolution,[],[f1639,f1050]) ).
fof(f1771,plain,
( spl125_19
| ~ spl125_38 ),
inference(avatar_split_clause,[],[f1769,f1638,f1562]) ).
fof(f1774,plain,
( cC20(iV21026)
| ~ spl125_40 ),
inference(resolution,[],[f1647,f1132]) ).
fof(f1775,plain,
( cC16(iV21026)
| ~ spl125_40 ),
inference(resolution,[],[f1647,f1131]) ).
fof(f1776,plain,
( spl125_35
| ~ spl125_40 ),
inference(avatar_split_clause,[],[f1775,f1646,f1626]) ).
fof(f1777,plain,
( spl125_32
| ~ spl125_40 ),
inference(avatar_split_clause,[],[f1774,f1646,f1614]) ).
fof(f1778,plain,
( cC10(iV21026)
| ~ spl125_35 ),
inference(resolution,[],[f1627,f1059]) ).
fof(f1779,plain,
( cC14(iV21026)
| ~ spl125_35 ),
inference(resolution,[],[f1627,f1058]) ).
fof(f1780,plain,
( spl125_20
| ~ spl125_35 ),
inference(avatar_split_clause,[],[f1779,f1626,f1566]) ).
fof(f1781,plain,
( spl125_47
| ~ spl125_35 ),
inference(avatar_split_clause,[],[f1778,f1626,f1674]) ).
fof(f1782,plain,
( cC108(iV21026)
| ~ spl125_41 ),
inference(resolution,[],[f1651,f936]) ).
fof(f1784,plain,
( spl125_50
| ~ spl125_41 ),
inference(avatar_split_clause,[],[f1782,f1650,f1686]) ).
fof(f1785,plain,
( cC86(iV21026)
| ~ spl125_46 ),
inference(resolution,[],[f1671,f1305]) ).
fof(f1787,plain,
( spl125_10
| ~ spl125_46 ),
inference(avatar_split_clause,[],[f1785,f1670,f1526]) ).
fof(f1788,plain,
( cC82(iV21026)
| ~ spl125_10 ),
inference(resolution,[],[f1527,f1300]) ).
fof(f1790,plain,
( spl125_21
| ~ spl125_10 ),
inference(avatar_split_clause,[],[f1788,f1526,f1570]) ).
fof(f1791,plain,
( cC64(iV21026)
| ~ spl125_21 ),
inference(resolution,[],[f1571,f1295]) ).
fof(f1792,plain,
( cC80(iV21026)
| ~ spl125_21 ),
inference(resolution,[],[f1571,f1294]) ).
fof(f1793,plain,
( spl125_18
| ~ spl125_21 ),
inference(avatar_split_clause,[],[f1792,f1570,f1558]) ).
fof(f1794,plain,
( spl125_23
| ~ spl125_21 ),
inference(avatar_split_clause,[],[f1791,f1570,f1578]) ).
fof(f1795,plain,
( cC78(iV21026)
| ~ spl125_18 ),
inference(resolution,[],[f1559,f1292]) ).
fof(f1797,plain,
( spl125_36
| ~ spl125_18 ),
inference(avatar_split_clause,[],[f1795,f1558,f1630]) ).
fof(f1798,plain,
( cC60(iV21026)
| ~ spl125_23 ),
inference(resolution,[],[f1579,f1243]) ).
fof(f1800,plain,
( spl125_39
| ~ spl125_23 ),
inference(avatar_split_clause,[],[f1798,f1578,f1642]) ).
fof(f1803,plain,
( cC58(iV21026)
| ~ spl125_39 ),
inference(resolution,[],[f1643,f1238]) ).
fof(f1804,plain,
( cC42(iV21026)
| ~ spl125_39 ),
inference(resolution,[],[f1643,f1237]) ).
fof(f1805,plain,
( spl125_12
| ~ spl125_39 ),
inference(avatar_split_clause,[],[f1804,f1642,f1534]) ).
fof(f1806,plain,
( spl125_44
| ~ spl125_39 ),
inference(avatar_split_clause,[],[f1803,f1642,f1662]) ).
fof(f1808,plain,
( cC38(iV21026)
| ~ spl125_12 ),
inference(resolution,[],[f1535,f1185]) ).
fof(f1809,plain,
( spl125_30
| ~ spl125_12 ),
inference(avatar_split_clause,[],[f1808,f1534,f1606]) ).
fof(f1810,plain,
( cC36(iV21026)
| ~ spl125_30 ),
inference(resolution,[],[f1607,f1178]) ).
fof(f1812,plain,
( spl125_25
| ~ spl125_30 ),
inference(avatar_split_clause,[],[f1810,f1606,f1586]) ).
fof(f1815,plain,
( cC56(iV21026)
| ~ spl125_44 ),
inference(resolution,[],[f1663,f1232]) ).
fof(f1817,plain,
( spl125_43
| ~ spl125_44 ),
inference(avatar_split_clause,[],[f1815,f1662,f1658]) ).
fof(f1820,plain,
( cC8(iV21026)
| ~ spl125_47 ),
inference(resolution,[],[f1675,f907]) ).
fof(f1821,plain,
( cC4(iV21026)
| ~ spl125_47 ),
inference(resolution,[],[f1675,f906]) ).
fof(f1822,plain,
( spl125_14
| ~ spl125_47 ),
inference(avatar_split_clause,[],[f1821,f1674,f1542]) ).
fof(f1823,plain,
( spl125_26
| ~ spl125_47 ),
inference(avatar_split_clause,[],[f1820,f1674,f1590]) ).
fof(f1875,plain,
! [X0] : ~ ra_Px87(iV21030,X0),
inference(resolution,[],[f1277,f1452]) ).
fof(f2251,plain,
! [X0] :
( ~ cC18xcomp(X0)
| cC74(X0)
| ra_Px24(X0,sK109(X0)) ),
inference(resolution,[],[f1274,f1271]) ).
fof(f2342,plain,
! [X0] :
( ~ rR1(X0,iV21036)
| cC24(X0) ),
inference(resolution,[],[f1138,f1482]) ).
fof(f2349,plain,
! [X0] :
( ~ rR1(X0,iV21035)
| cC30(X0) ),
inference(resolution,[],[f1158,f1476]) ).
fof(f2365,plain,
! [X0] :
( ~ rR1(X0,iV21034)
| cC44(X0) ),
inference(resolution,[],[f1192,f1470]) ).
fof(f2372,plain,
! [X0] :
( ~ rR1(X0,iV21033)
| cC50(X0) ),
inference(resolution,[],[f1210,f1464]) ).
fof(f2380,plain,
! [X0] :
( ~ rR1(X0,iV21032)
| cC66(X0) ),
inference(resolution,[],[f1249,f1457]) ).
fof(f2441,plain,
cC24(iV21027),
inference(resolution,[],[f2342,f1397]) ).
fof(f2442,plain,
spl125_7,
inference(avatar_split_clause,[],[f2441,f1514]) ).
fof(f2465,plain,
cC30(iV21027),
inference(resolution,[],[f2349,f1398]) ).
fof(f2466,plain,
spl125_9,
inference(avatar_split_clause,[],[f2465,f1522]) ).
fof(f2497,plain,
cC44(iV21029),
inference(resolution,[],[f2365,f1426]) ).
fof(f2498,plain,
spl125_5,
inference(avatar_split_clause,[],[f2497,f1506]) ).
fof(f2518,plain,
cC50(iV21029),
inference(resolution,[],[f2372,f1427]) ).
fof(f2519,plain,
spl125_6,
inference(avatar_split_clause,[],[f2518,f1510]) ).
fof(f2539,plain,
cC66(iV21030),
inference(resolution,[],[f2380,f1454]) ).
fof(f2540,plain,
( $false
| spl125_2 ),
inference(forward_subsumption_resolution,[],[f2539,f1496]) ).
fof(f2541,plain,
spl125_2,
inference(avatar_contradiction_clause,[],[f2540]) ).
fof(f3052,plain,
( cC74(iV21030)
| ra_Px24(iV21030,sK109(iV21030)) ),
inference(resolution,[],[f2251,f1438]) ).
fof(f3066,definition,
( spl125_102
<=> ra_Px24(iV21030,sK109(iV21030)) ),
introduced(definition,[new_symbols(definition,[spl125_102])],[avatar_definition]) ).
fof(f3068,plain,
( ra_Px24(iV21030,sK109(iV21030))
| ~ spl125_102 ),
inference(avatar_component_clause,[],[f3066]) ).
fof(f3070,definition,
( spl125_103
<=> cC74(iV21030) ),
introduced(definition,[new_symbols(definition,[spl125_103])],[avatar_definition]) ).
fof(f3072,plain,
( cC74(iV21030)
| ~ spl125_103 ),
inference(avatar_component_clause,[],[f3070]) ).
fof(f3073,plain,
( spl125_102
| spl125_103 ),
inference(avatar_split_clause,[],[f3052,f3070,f3066]) ).
fof(f6084,plain,
( cC72(iV21030)
| ~ spl125_102 ),
inference(resolution,[],[f3068,f1266]) ).
fof(f6085,plain,
( $false
| spl125_3
| ~ spl125_102 ),
inference(forward_subsumption_resolution,[],[f6084,f1500]) ).
fof(f6086,plain,
( spl125_3
| ~ spl125_102 ),
inference(avatar_contradiction_clause,[],[f6085]) ).
fof(f6091,plain,
( ra_Px87(iV21030,sK110(iV21030))
| ~ spl125_103 ),
inference(resolution,[],[f3072,f1275]) ).
fof(f6094,plain,
( $false
| ~ spl125_103 ),
inference(forward_subsumption_resolution,[],[f6091,f1875]) ).
fof(f6095,plain,
~ spl125_103,
inference(avatar_contradiction_clause,[],[f6094]) ).
fof(f6096,plain,
( $false
| spl125_54 ),
inference(forward_subsumption_resolution,[],[f1704,f903]) ).
fof(f6097,plain,
spl125_54,
inference(avatar_contradiction_clause,[],[f6096]) ).
fof(f6101,plain,
( xsd_string(sK124)
| spl125_52 ),
inference(resolution,[],[f1696,f905]) ).
fof(f6102,plain,
( $false
| spl125_51
| spl125_52 ),
inference(forward_subsumption_resolution,[],[f6101,f1691]) ).
fof(f6103,plain,
( spl125_51
| spl125_52 ),
inference(avatar_contradiction_clause,[],[f6102]) ).
fof(f6104,plain,
( ~ xsd_string(sK124)
| ~ spl125_52 ),
inference(resolution,[],[f1695,f904]) ).
fof(f6105,plain,
( $false
| ~ spl125_51
| ~ spl125_52 ),
inference(forward_subsumption_resolution,[],[f6104,f1692]) ).
fof(f6106,plain,
( ~ spl125_51
| ~ spl125_52 ),
inference(avatar_contradiction_clause,[],[f6105]) ).
fof(f6107,plain,
( $false
| ~ spl125_53 ),
inference(forward_subsumption_resolution,[],[f1700,f902]) ).
fof(f6108,plain,
~ spl125_53,
inference(avatar_contradiction_clause,[],[f6107]) ).
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_33,
inference(sat_conversion,[],[f1713]) ).
cnf(s8,plain,
spl125_48,
inference(sat_conversion,[],[f1716]) ).
cnf(s9,plain,
spl125_49,
inference(sat_conversion,[],[f1719]) ).
cnf(s10,plain,
spl125_27,
inference(sat_conversion,[],[f1722]) ).
cnf(s11,plain,
spl125_31,
inference(sat_conversion,[],[f1725]) ).
cnf(s12,plain,
spl125_17,
inference(sat_conversion,[],[f1728]) ).
cnf(s13,plain,
spl125_37,
inference(sat_conversion,[],[f1731]) ).
cnf(s14,plain,
( spl125_28
| ~ spl125_37 ),
inference(sat_conversion,[],[f1734]) ).
cnf(s15,plain,
( spl125_15
| ~ spl125_28 ),
inference(sat_conversion,[],[f1737]) ).
cnf(s16,plain,
spl125_42,
inference(sat_conversion,[],[f1741]) ).
cnf(s17,plain,
( spl125_11
| ~ spl125_42 ),
inference(sat_conversion,[],[f1744]) ).
cnf(s18,plain,
( spl125_40
| ~ spl125_42 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s19,plain,
( ~ spl125_11
| spl125_29 ),
inference(sat_conversion,[],[f1748]) ).
cnf(s20,plain,
( ~ spl125_11
| spl125_38 ),
inference(sat_conversion,[],[f1749]) ).
cnf(s21,plain,
( spl125_13
| ~ spl125_29 ),
inference(sat_conversion,[],[f1752]) ).
cnf(s22,plain,
( ~ spl125_13
| spl125_34 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s23,plain,
( ~ spl125_13
| spl125_22 ),
inference(sat_conversion,[],[f1756]) ).
cnf(s24,plain,
( ~ spl125_22
| spl125_24 ),
inference(sat_conversion,[],[f1759]) ).
cnf(s25,plain,
( ~ spl125_24
| spl125_46 ),
inference(sat_conversion,[],[f1762]) ).
cnf(s26,plain,
( ~ spl125_24
| spl125_41 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s27,plain,
( spl125_16
| ~ spl125_34 ),
inference(sat_conversion,[],[f1766]) ).
cnf(s28,plain,
( spl125_19
| ~ spl125_38 ),
inference(sat_conversion,[],[f1771]) ).
cnf(s29,plain,
( spl125_35
| ~ spl125_40 ),
inference(sat_conversion,[],[f1776]) ).
cnf(s30,plain,
( spl125_32
| ~ spl125_40 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s31,plain,
( spl125_20
| ~ spl125_35 ),
inference(sat_conversion,[],[f1780]) ).
cnf(s32,plain,
( ~ spl125_35
| spl125_47 ),
inference(sat_conversion,[],[f1781]) ).
cnf(s33,plain,
( ~ spl125_41
| spl125_50 ),
inference(sat_conversion,[],[f1784]) ).
cnf(s34,plain,
( spl125_10
| ~ spl125_46 ),
inference(sat_conversion,[],[f1787]) ).
cnf(s35,plain,
( ~ spl125_10
| spl125_21 ),
inference(sat_conversion,[],[f1790]) ).
cnf(s36,plain,
( spl125_18
| ~ spl125_21 ),
inference(sat_conversion,[],[f1793]) ).
cnf(s37,plain,
( ~ spl125_21
| spl125_23 ),
inference(sat_conversion,[],[f1794]) ).
cnf(s38,plain,
( ~ spl125_18
| spl125_36 ),
inference(sat_conversion,[],[f1797]) ).
cnf(s39,plain,
( ~ spl125_23
| spl125_39 ),
inference(sat_conversion,[],[f1800]) ).
cnf(s40,plain,
( spl125_12
| ~ spl125_39 ),
inference(sat_conversion,[],[f1805]) ).
cnf(s41,plain,
( ~ spl125_39
| spl125_44 ),
inference(sat_conversion,[],[f1806]) ).
cnf(s42,plain,
( ~ spl125_12
| spl125_30 ),
inference(sat_conversion,[],[f1809]) ).
cnf(s43,plain,
( spl125_25
| ~ spl125_30 ),
inference(sat_conversion,[],[f1812]) ).
cnf(s44,plain,
( spl125_43
| ~ spl125_44 ),
inference(sat_conversion,[],[f1817]) ).
cnf(s45,plain,
( spl125_14
| ~ spl125_47 ),
inference(sat_conversion,[],[f1822]) ).
cnf(s46,plain,
( spl125_26
| ~ spl125_47 ),
inference(sat_conversion,[],[f1823]) ).
cnf(s47,plain,
spl125_7,
inference(sat_conversion,[],[f2442]) ).
cnf(s48,plain,
spl125_9,
inference(sat_conversion,[],[f2466]) ).
cnf(s49,plain,
spl125_5,
inference(sat_conversion,[],[f2498]) ).
cnf(s50,plain,
spl125_6,
inference(sat_conversion,[],[f2519]) ).
cnf(s51,plain,
spl125_2,
inference(sat_conversion,[],[f2541]) ).
cnf(s80,plain,
( spl125_102
| spl125_103 ),
inference(sat_conversion,[],[f3073]) ).
cnf(s367,plain,
( spl125_3
| ~ spl125_102 ),
inference(sat_conversion,[],[f6086]) ).
cnf(s368,plain,
~ spl125_103,
inference(sat_conversion,[],[f6095]) ).
cnf(s369,plain,
spl125_54,
inference(sat_conversion,[],[f6097]) ).
cnf(s370,plain,
( spl125_51
| spl125_52 ),
inference(sat_conversion,[],[f6103]) ).
cnf(s371,plain,
( ~ spl125_51
| ~ spl125_52 ),
inference(sat_conversion,[],[f6106]) ).
cnf(s372,plain,
~ spl125_53,
inference(sat_conversion,[],[f6108]) ).
cnf(s418,plain,
spl125_102,
inference(rat,[],[s80,s368]) ).
cnf(s419,plain,
spl125_3,
inference(rat,[],[s367,s418]) ).
cnf(s430,plain,
spl125_40,
inference(rat,[],[s18,s16]) ).
cnf(s431,plain,
spl125_11,
inference(rat,[],[s17,s16]) ).
cnf(s432,plain,
spl125_32,
inference(rat,[],[s30,s430]) ).
cnf(s433,plain,
spl125_35,
inference(rat,[],[s29,s430]) ).
cnf(s434,plain,
spl125_38,
inference(rat,[],[s20,s431]) ).
cnf(s435,plain,
spl125_29,
inference(rat,[],[s19,s431]) ).
cnf(s437,plain,
spl125_47,
inference(rat,[],[s32,s433]) ).
cnf(s438,plain,
spl125_20,
inference(rat,[],[s31,s433]) ).
cnf(s439,plain,
spl125_19,
inference(rat,[],[s28,s434]) ).
cnf(s440,plain,
spl125_13,
inference(rat,[],[s21,s435]) ).
cnf(s442,plain,
spl125_26,
inference(rat,[],[s46,s437]) ).
cnf(s443,plain,
spl125_14,
inference(rat,[],[s45,s437]) ).
cnf(s445,plain,
spl125_22,
inference(rat,[],[s23,s440]) ).
cnf(s446,plain,
spl125_34,
inference(rat,[],[s22,s440]) ).
cnf(s473,plain,
spl125_24,
inference(rat,[],[s24,s445]) ).
cnf(s474,plain,
spl125_16,
inference(rat,[],[s27,s446]) ).
cnf(s475,plain,
spl125_41,
inference(rat,[],[s26,s473]) ).
cnf(s476,plain,
spl125_46,
inference(rat,[],[s25,s473]) ).
cnf(s477,plain,
spl125_50,
inference(rat,[],[s33,s475]) ).
cnf(s478,plain,
spl125_10,
inference(rat,[],[s34,s476]) ).
cnf(s479,plain,
spl125_21,
inference(rat,[],[s35,s478]) ).
cnf(s480,plain,
spl125_23,
inference(rat,[],[s37,s479]) ).
cnf(s481,plain,
spl125_18,
inference(rat,[],[s36,s479]) ).
cnf(s482,plain,
spl125_39,
inference(rat,[],[s39,s480]) ).
cnf(s483,plain,
spl125_36,
inference(rat,[],[s38,s481]) ).
cnf(s484,plain,
spl125_44,
inference(rat,[],[s41,s482]) ).
cnf(s485,plain,
spl125_12,
inference(rat,[],[s40,s482]) ).
cnf(s486,plain,
spl125_43,
inference(rat,[],[s44,s484]) ).
cnf(s487,plain,
spl125_30,
inference(rat,[],[s42,s485]) ).
cnf(s488,plain,
spl125_25,
inference(rat,[],[s43,s487]) ).
cnf(s489,plain,
spl125_28,
inference(rat,[],[s14,s13]) ).
cnf(s490,plain,
spl125_15,
inference(rat,[],[s15,s489]) ).
cnf(s491,plain,
( ~ spl125_51
| spl125_52 ),
inference(rat,[],[s2,s369,s372,s477,s9,s8,s437,s476,s6,s484,s486,s16,s475,s430,s482,s434,s13,s483,s433,s446,s7,s432,s11,s487,s435,s489,s10,s442,s488,s473,s480,s445,s479,s438,s439,s481,s12,s474,s490,s443,s440,s485,s431,s478,s48,s5,s47,s50,s49,s4,s419,s51,s3]) ).
cnf(s492,plain,
( spl125_51
| ~ spl125_52 ),
inference(rat,[],[s1,s369,s372,s477,s9,s8,s437,s476,s6,s484,s486,s16,s475,s430,s482,s434,s13,s483,s433,s446,s7,s432,s11,s487,s435,s489,s10,s442,s488,s473,s480,s445,s479,s438,s439,s481,s12,s474,s490,s443,s440,s485,s431,s478,s48,s5,s47,s50,s49,s4,s419,s51,s3]) ).
cnf(s493,plain,
spl125_51,
inference(rat,[],[s492,s370]) ).
cnf(s494,plain,
~ spl125_52,
inference(rat,[],[s371,s493]) ).
cnf(s495,plain,
$false,
inference(rat,[],[s491,s494,s493]) ).
fof(f6109,plain,
$false,
inference(avatar_sat_refutation,[],[s495]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS159+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n009.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 13:32:30 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.50 % (2038725)Will run a generic schedule for satisfiability detection.
% 0.18/0.50 % (2038735)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2354053341:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.50 % (2038731)% WARNING: option uhcvi not known.
% 0.18/0.50 % (2038730)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1035128242_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.50 % (2038731)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3931331934:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.50 % (2038732)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3508149412:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.50 % (2038733)dis+10_1_sil=32000:sp=arity:random_seed=516230198:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.50 % (2038734)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1534149102:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.50 % (2038736)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1599368152:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.50 % (2038735) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2038725-2038735"...
% 0.18/0.50 % TRYING [1]
% 0.18/0.50 % TRYING [2]
% 0.18/0.50 % (2038735)...printing done.
% 0.18/0.50 % (2038735)Refutation found. Thanks to Tanya!
% 0.18/0.50 % SZS status Theorem for theBenchmark
% 0.18/0.50 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.51 % (2038735)------------------------------
% 0.18/0.51 % (2038735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.51 % (2038735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.51 % (2038735)CaDiCaL version: 2.1.3
% 0.18/0.51 % (2038735)Termination reason: Refutation
% 0.18/0.51 % (2038735)Time elapsed: 0.033 s
% 0.18/0.51 % (2038735)Peak memory usage: 15 MB
% 0.18/0.51 % (2038735)Instructions burned: 92 (million)
% 0.18/0.51 % (2038725)Success in time 0.074 s
% 0.18/0.51 % Vampire exiting
%------------------------------------------------------------------------------