%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : KRS153+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 : n020.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 0.50s 1.02s
% Output : Refutation 2.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 108
% Syntax : Number of formulae : 476 ( 152 unt; 55 def)
% Number of atoms : 1534 ( 0 equ)
% Maximal formula atoms : 51 ( 3 avg)
% Number of connectives : 1812 ( 754 ~; 747 |; 227 &)
% ( 75 <=>; 8 =>; 0 <=; 1 <~>)
% Maximal formula depth : 51 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 100 ( 99 usr; 56 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 15 con; 0-1 aty)
% Number of variables : 131 ( 0 sgn 121 !; 10 ?)
% 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(f6,axiom,
! [X0] :
( cC106(X0)
<=> ( ~ cC100(X0)
& cC104(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
fof(f7,axiom,
! [X0] :
( cC108(X0)
<=> ( cC28(X0)
& cC106(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6) ).
fof(f26,axiom,
! [X0] :
( cC34(X0)
<=> ( ~ cC32(X0)
& ~ cC30(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_25) ).
fof(f28,axiom,
! [X0] :
( cC38(X0)
<=> ( ~ cC36(X0)
& cTOP(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_27) ).
fof(f30,axiom,
! [X0] :
( cC42(X0)
<=> ? [X1] :
( rR1(X0,X1)
& ~ cC8(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_29) ).
fof(f31,axiom,
! [X0] :
( cC44(X0)
<=> ( ~ cC40(X0)
& cC42(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_30) ).
fof(f34,axiom,
! [X0] :
( cC50(X0)
<=> ( ~ cC46(X0)
& ~ cC48(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_33) ).
fof(f37,axiom,
! [X0] :
( cC56(X0)
<=> ( cC44(X0)
& ~ cC54(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_36) ).
fof(f40,axiom,
! [X0] :
( cC60(X0)
<=> ? [X1] :
( rR1(X0,X1)
& ~ cC12(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_39) ).
fof(f41,axiom,
! [X0] :
( cC62(X0)
<=> ( cC60(X0)
& ~ cC58(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_40) ).
fof(f44,axiom,
! [X0] :
( cC68(X0)
<=> ( ~ cC64(X0)
& ~ cC66(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_43) ).
fof(f48,axiom,
! [X0] :
( cC76(X0)
<=> ( ~ cC74(X0)
& cC62(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_47) ).
fof(f51,axiom,
! [X0] :
( cC82(X0)
<=> ( ~ cC78(X0)
& cC80(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_50) ).
fof(f54,axiom,
! [X0] :
( cC88(X0)
<=> ( ~ cC84(X0)
& ~ cC86(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_53) ).
fof(f59,axiom,
! [X0] :
( cC98(X0)
<=> ( ~ cC96(X0)
& cC82(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_58) ).
fof(f60,axiom,
! [X0] :
( cTEST(X0)
<=> ( cC108(X0)
& cC130(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_59) ).
fof(f61,axiom,
! [X0] :
( rR1(iV16439,X0)
=> cC98(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_60) ).
fof(f62,axiom,
cTEST(iV16439),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_61) ).
fof(f65,axiom,
rR1(iV16439,iV16440),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_64) ).
fof(f68,axiom,
! [X0] :
( rR1(iV16440,X0)
=> cC76(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_67) ).
fof(f71,axiom,
~ cC78(iV16440),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_70) ).
fof(f74,axiom,
rR1(iV16440,iV16463),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_73) ).
fof(f77,axiom,
~ cC36(iV16448),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_76) ).
fof(f80,axiom,
cTOP(iV16448),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_79) ).
fof(f92,axiom,
~ cC58(iV16453),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_91) ).
fof(f93,axiom,
~ cC74(iV16453),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_92) ).
fof(f94,axiom,
! [X0] :
( rR1(iV16453,X0)
=> cC56(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_93) ).
fof(f97,axiom,
rR1(iV16453,iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_96) ).
fof(f99,axiom,
~ cC40(iV16455),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_98) ).
fof(f104,axiom,
~ cC54(iV16455),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_103) ).
fof(f107,axiom,
! [X0] :
( rR1(iV16455,X0)
=> cC38(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_106) ).
fof(f108,axiom,
rR1(iV16455,iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_107) ).
fof(f109,axiom,
~ cC36(iV16457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_108) ).
fof(f114,axiom,
cTOP(iV16457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_113) ).
fof(f121,axiom,
~ cC48(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_120) ).
fof(f122,axiom,
~ cC30(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_121) ).
fof(f124,axiom,
~ cC86(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_123) ).
fof(f125,axiom,
~ cC46(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_124) ).
fof(f128,axiom,
~ cC66(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_127) ).
fof(f133,axiom,
~ cC84(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_132) ).
fof(f134,axiom,
~ cC64(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_133) ).
fof(f136,axiom,
~ cC32(iV16459),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_135) ).
fof(f142,axiom,
~ cC8(iV16460),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_141) ).
fof(f152,axiom,
~ cC12(iV16461),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_151) ).
fof(f155,axiom,
! [X0] :
( rR1(iV16461,X0)
=> cC38(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_154) ).
fof(f158,axiom,
rR1(iV16461,iV16462),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_157) ).
fof(f172,axiom,
! [X0] :
( rR1(iV16463,X0)
=> cC56(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_171) ).
fof(f178,axiom,
rR1(iV16463,iV16464),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_177) ).
fof(f183,axiom,
! [X0] :
( rR1(iV16464,X0)
=> cC38(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_182) ).
fof(f189,axiom,
rR1(iV16464,iV16465),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_188) ).
fof(f201,conjecture,
( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& cC106(iV16439)
& cC28(iV16439)
& cC130(iV16439)
& cowlThing(iV16439)
& cC108(iV16439)
& cC104(iV16439)
& cC80(iV16440)
& cowlThing(iV16440)
& cC82(iV16440)
& cC98(iV16440)
& cowlThing(iV16448)
& cC38(iV16448)
& cC62(iV16453)
& cowlThing(iV16453)
& cC76(iV16453)
& cC60(iV16453)
& cC44(iV16455)
& cowlThing(iV16455)
& cC56(iV16455)
& cC42(iV16455)
& cowlThing(iV16457)
& cC38(iV16457)
& cC68(iV16459)
& cowlThing(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cC34(iV16459)
& cowlThing(iV16460)
& cC38(iV16460)
& cC44(iV16461)
& cowlThing(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16462)
& cC38(iV16462)
& cC62(iV16463)
& cowlThing(iV16463)
& cC76(iV16463)
& cC60(iV16463)
& cC44(iV16464)
& cowlThing(iV16464)
& cC56(iV16464)
& cC42(iV16464)
& cowlThing(iV16465)
& cC38(iV16465) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',the_axiom) ).
fof(f202,negated_conjecture,
~ ( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X0] :
( xsd_string(X0)
<=> ~ xsd_integer(X0) )
& cC106(iV16439)
& cC28(iV16439)
& cC130(iV16439)
& cowlThing(iV16439)
& cC108(iV16439)
& cC104(iV16439)
& cC80(iV16440)
& cowlThing(iV16440)
& cC82(iV16440)
& cC98(iV16440)
& cowlThing(iV16448)
& cC38(iV16448)
& cC62(iV16453)
& cowlThing(iV16453)
& cC76(iV16453)
& cC60(iV16453)
& cC44(iV16455)
& cowlThing(iV16455)
& cC56(iV16455)
& cC42(iV16455)
& cowlThing(iV16457)
& cC38(iV16457)
& cC68(iV16459)
& cowlThing(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cC34(iV16459)
& cowlThing(iV16460)
& cC38(iV16460)
& cC44(iV16461)
& cowlThing(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16462)
& cC38(iV16462)
& cC62(iV16463)
& cowlThing(iV16463)
& cC76(iV16463)
& cC60(iV16463)
& cC44(iV16464)
& cowlThing(iV16464)
& cC56(iV16464)
& cC42(iV16464)
& cowlThing(iV16465)
& cC38(iV16465) ),
inference(negated_conjecture,[status(cth)],[f201]) ).
fof(f203,plain,
~ ( ! [X0] :
( cowlThing(X0)
& ~ cowlNothing(X0) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC106(iV16439)
& cC28(iV16439)
& cC130(iV16439)
& cowlThing(iV16439)
& cC108(iV16439)
& cC104(iV16439)
& cC80(iV16440)
& cowlThing(iV16440)
& cC82(iV16440)
& cC98(iV16440)
& cowlThing(iV16448)
& cC38(iV16448)
& cC62(iV16453)
& cowlThing(iV16453)
& cC76(iV16453)
& cC60(iV16453)
& cC44(iV16455)
& cowlThing(iV16455)
& cC56(iV16455)
& cC42(iV16455)
& cowlThing(iV16457)
& cC38(iV16457)
& cC68(iV16459)
& cowlThing(iV16459)
& cC88(iV16459)
& cC50(iV16459)
& cC34(iV16459)
& cowlThing(iV16460)
& cC38(iV16460)
& cC44(iV16461)
& cowlThing(iV16461)
& cC56(iV16461)
& cC42(iV16461)
& cowlThing(iV16462)
& cC38(iV16462)
& cC62(iV16463)
& cowlThing(iV16463)
& cC76(iV16463)
& cC60(iV16463)
& cC44(iV16464)
& cowlThing(iV16464)
& cC56(iV16464)
& cC42(iV16464)
& cowlThing(iV16465)
& cC38(iV16465) ),
inference(rectify,[],[f202]) ).
fof(f204,plain,
! [X0] :
( cTEST(X0)
=> ( cC108(X0)
& cC130(X0) ) ),
inference(unused_predicate_definition_removal,[],[f60]) ).
fof(f205,plain,
! [X0] :
( ( cC108(X0)
& cC130(X0) )
| ~ cTEST(X0) ),
inference(ennf_transformation,[],[f204]) ).
fof(f206,plain,
! [X0] :
( cC98(X0)
| ~ rR1(iV16439,X0) ),
inference(ennf_transformation,[],[f61]) ).
fof(f207,plain,
! [X0] :
( cC76(X0)
| ~ rR1(iV16440,X0) ),
inference(ennf_transformation,[],[f68]) ).
fof(f215,plain,
! [X0] :
( cC56(X0)
| ~ rR1(iV16453,X0) ),
inference(ennf_transformation,[],[f94]) ).
fof(f219,plain,
! [X0] :
( cC38(X0)
| ~ rR1(iV16455,X0) ),
inference(ennf_transformation,[],[f107]) ).
fof(f231,plain,
! [X0] :
( cC38(X0)
| ~ rR1(iV16461,X0) ),
inference(ennf_transformation,[],[f155]) ).
fof(f237,plain,
! [X0] :
( cC56(X0)
| ~ rR1(iV16463,X0) ),
inference(ennf_transformation,[],[f172]) ).
fof(f240,plain,
! [X0] :
( cC38(X0)
| ~ rR1(iV16464,X0) ),
inference(ennf_transformation,[],[f183]) ).
fof(f247,plain,
( ? [X0] :
( ~ cowlThing(X0)
| cowlNothing(X0) )
| ? [X1] :
( xsd_string(X1)
<~> ~ xsd_integer(X1) )
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC130(iV16439)
| ~ cowlThing(iV16439)
| ~ cC108(iV16439)
| ~ cC104(iV16439)
| ~ cC80(iV16440)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cC62(iV16453)
| ~ cowlThing(iV16453)
| ~ cC76(iV16453)
| ~ cC60(iV16453)
| ~ cC44(iV16455)
| ~ cowlThing(iV16455)
| ~ cC56(iV16455)
| ~ cC42(iV16455)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cC68(iV16459)
| ~ cowlThing(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC34(iV16459)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cC44(iV16461)
| ~ cowlThing(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cowlThing(iV16463)
| ~ cC76(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464)
| ~ cowlThing(iV16464)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cowlThing(iV16465)
| ~ cC38(iV16465) ),
inference(ennf_transformation,[],[f203]) ).
fof(f248,plain,
! [X0] :
( ( xsd_string(X0)
| xsd_integer(X0) )
& ( ~ xsd_integer(X0)
| ~ xsd_string(X0) ) ),
inference(nnf_transformation,[],[f2]) ).
fof(f257,plain,
! [X0] :
( ( cC106(X0)
| cC100(X0)
| ~ cC104(X0) )
& ( ( ~ cC100(X0)
& cC104(X0) )
| ~ cC106(X0) ) ),
inference(nnf_transformation,[],[f6]) ).
fof(f258,plain,
! [X0] :
( ( cC106(X0)
| cC100(X0)
| ~ cC104(X0) )
& ( ( ~ cC100(X0)
& cC104(X0) )
| ~ cC106(X0) ) ),
inference(flattening,[],[f257]) ).
fof(f259,plain,
! [X0] :
( ( cC108(X0)
| ~ cC28(X0)
| ~ cC106(X0) )
& ( ( cC28(X0)
& cC106(X0) )
| ~ cC108(X0) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f260,plain,
! [X0] :
( ( cC108(X0)
| ~ cC28(X0)
| ~ cC106(X0) )
& ( ( cC28(X0)
& cC106(X0) )
| ~ cC108(X0) ) ),
inference(flattening,[],[f259]) ).
fof(f307,plain,
! [X0] :
( ( cC34(X0)
| cC32(X0)
| cC30(X0) )
& ( ( ~ cC32(X0)
& ~ cC30(X0) )
| ~ cC34(X0) ) ),
inference(nnf_transformation,[],[f26]) ).
fof(f308,plain,
! [X0] :
( ( cC34(X0)
| cC32(X0)
| cC30(X0) )
& ( ( ~ cC32(X0)
& ~ cC30(X0) )
| ~ cC34(X0) ) ),
inference(flattening,[],[f307]) ).
fof(f312,plain,
! [X0] :
( ( cC38(X0)
| cC36(X0)
| ~ cTOP(X0) )
& ( ( ~ cC36(X0)
& cTOP(X0) )
| ~ cC38(X0) ) ),
inference(nnf_transformation,[],[f28]) ).
fof(f313,plain,
! [X0] :
( ( cC38(X0)
| cC36(X0)
| ~ cTOP(X0) )
& ( ( ~ cC36(X0)
& cTOP(X0) )
| ~ cC38(X0) ) ),
inference(flattening,[],[f312]) ).
fof(f317,plain,
! [X0] :
( ( cC42(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| cC8(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& ~ cC8(X1) )
| ~ cC42(X0) ) ),
inference(nnf_transformation,[],[f30]) ).
fof(f318,plain,
! [X0] :
( ( cC42(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| cC8(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& ~ cC8(X2) )
| ~ cC42(X0) ) ),
inference(rectify,[],[f317]) ).
fof(f319,plain,
! [X0] :
( ( cC42(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| cC8(X1) ) )
& ( ( rR1(X0,sK14(X0))
& ~ cC8(sK14(X0)) )
| ~ cC42(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(X2,sK14(X0))],[f318]) ).
fof(f320,plain,
! [X0] :
( ( cC44(X0)
| cC40(X0)
| ~ cC42(X0) )
& ( ( ~ cC40(X0)
& cC42(X0) )
| ~ cC44(X0) ) ),
inference(nnf_transformation,[],[f31]) ).
fof(f321,plain,
! [X0] :
( ( cC44(X0)
| cC40(X0)
| ~ cC42(X0) )
& ( ( ~ cC40(X0)
& cC42(X0) )
| ~ cC44(X0) ) ),
inference(flattening,[],[f320]) ).
fof(f326,plain,
! [X0] :
( ( cC50(X0)
| cC46(X0)
| cC48(X0) )
& ( ( ~ cC46(X0)
& ~ cC48(X0) )
| ~ cC50(X0) ) ),
inference(nnf_transformation,[],[f34]) ).
fof(f327,plain,
! [X0] :
( ( cC50(X0)
| cC46(X0)
| cC48(X0) )
& ( ( ~ cC46(X0)
& ~ cC48(X0) )
| ~ cC50(X0) ) ),
inference(flattening,[],[f326]) ).
fof(f334,plain,
! [X0] :
( ( cC56(X0)
| ~ cC44(X0)
| cC54(X0) )
& ( ( cC44(X0)
& ~ cC54(X0) )
| ~ cC56(X0) ) ),
inference(nnf_transformation,[],[f37]) ).
fof(f335,plain,
! [X0] :
( ( cC56(X0)
| ~ cC44(X0)
| cC54(X0) )
& ( ( cC44(X0)
& ~ cC54(X0) )
| ~ cC56(X0) ) ),
inference(flattening,[],[f334]) ).
fof(f341,plain,
! [X0] :
( ( cC60(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| cC12(X1) ) )
& ( ? [X1] :
( rR1(X0,X1)
& ~ cC12(X1) )
| ~ cC60(X0) ) ),
inference(nnf_transformation,[],[f40]) ).
fof(f342,plain,
! [X0] :
( ( cC60(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| cC12(X1) ) )
& ( ? [X2] :
( rR1(X0,X2)
& ~ cC12(X2) )
| ~ cC60(X0) ) ),
inference(rectify,[],[f341]) ).
fof(f343,plain,
! [X0] :
( ( cC60(X0)
| ! [X1] :
( ~ rR1(X0,X1)
| cC12(X1) ) )
& ( ( rR1(X0,sK18(X0))
& ~ cC12(sK18(X0)) )
| ~ cC60(X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(X2,sK18(X0))],[f342]) ).
fof(f344,plain,
! [X0] :
( ( cC62(X0)
| ~ cC60(X0)
| cC58(X0) )
& ( ( cC60(X0)
& ~ cC58(X0) )
| ~ cC62(X0) ) ),
inference(nnf_transformation,[],[f41]) ).
fof(f345,plain,
! [X0] :
( ( cC62(X0)
| ~ cC60(X0)
| cC58(X0) )
& ( ( cC60(X0)
& ~ cC58(X0) )
| ~ cC62(X0) ) ),
inference(flattening,[],[f344]) ).
fof(f350,plain,
! [X0] :
( ( cC68(X0)
| cC64(X0)
| cC66(X0) )
& ( ( ~ cC64(X0)
& ~ cC66(X0) )
| ~ cC68(X0) ) ),
inference(nnf_transformation,[],[f44]) ).
fof(f351,plain,
! [X0] :
( ( cC68(X0)
| cC64(X0)
| cC66(X0) )
& ( ( ~ cC64(X0)
& ~ cC66(X0) )
| ~ cC68(X0) ) ),
inference(flattening,[],[f350]) ).
fof(f361,plain,
! [X0] :
( ( cC76(X0)
| cC74(X0)
| ~ cC62(X0) )
& ( ( ~ cC74(X0)
& cC62(X0) )
| ~ cC76(X0) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f362,plain,
! [X0] :
( ( cC76(X0)
| cC74(X0)
| ~ cC62(X0) )
& ( ( ~ cC74(X0)
& cC62(X0) )
| ~ cC76(X0) ) ),
inference(flattening,[],[f361]) ).
fof(f369,plain,
! [X0] :
( ( cC82(X0)
| cC78(X0)
| ~ cC80(X0) )
& ( ( ~ cC78(X0)
& cC80(X0) )
| ~ cC82(X0) ) ),
inference(nnf_transformation,[],[f51]) ).
fof(f370,plain,
! [X0] :
( ( cC82(X0)
| cC78(X0)
| ~ cC80(X0) )
& ( ( ~ cC78(X0)
& cC80(X0) )
| ~ cC82(X0) ) ),
inference(flattening,[],[f369]) ).
fof(f375,plain,
! [X0] :
( ( cC88(X0)
| cC84(X0)
| cC86(X0) )
& ( ( ~ cC84(X0)
& ~ cC86(X0) )
| ~ cC88(X0) ) ),
inference(nnf_transformation,[],[f54]) ).
fof(f376,plain,
! [X0] :
( ( cC88(X0)
| cC84(X0)
| cC86(X0) )
& ( ( ~ cC84(X0)
& ~ cC86(X0) )
| ~ cC88(X0) ) ),
inference(flattening,[],[f375]) ).
fof(f389,plain,
! [X0] :
( ( cC98(X0)
| cC96(X0)
| ~ cC82(X0) )
& ( ( ~ cC96(X0)
& cC82(X0) )
| ~ cC98(X0) ) ),
inference(nnf_transformation,[],[f59]) ).
fof(f390,plain,
! [X0] :
( ( cC98(X0)
| cC96(X0)
| ~ cC82(X0) )
& ( ( ~ cC96(X0)
& cC82(X0) )
| ~ cC98(X0) ) ),
inference(flattening,[],[f389]) ).
fof(f391,plain,
( ? [X0] :
( ~ cowlThing(X0)
| cowlNothing(X0) )
| ? [X1] :
( ( xsd_integer(X1)
| ~ xsd_string(X1) )
& ( ~ xsd_integer(X1)
| xsd_string(X1) ) )
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC130(iV16439)
| ~ cowlThing(iV16439)
| ~ cC108(iV16439)
| ~ cC104(iV16439)
| ~ cC80(iV16440)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cC62(iV16453)
| ~ cowlThing(iV16453)
| ~ cC76(iV16453)
| ~ cC60(iV16453)
| ~ cC44(iV16455)
| ~ cowlThing(iV16455)
| ~ cC56(iV16455)
| ~ cC42(iV16455)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cC68(iV16459)
| ~ cowlThing(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC34(iV16459)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cC44(iV16461)
| ~ cowlThing(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cowlThing(iV16463)
| ~ cC76(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464)
| ~ cowlThing(iV16464)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cowlThing(iV16465)
| ~ cC38(iV16465) ),
inference(nnf_transformation,[],[f247]) ).
fof(f392,plain,
( ~ cowlThing(sK28)
| cowlNothing(sK28)
| ( ( xsd_integer(sK29)
| ~ xsd_string(sK29) )
& ( ~ xsd_integer(sK29)
| xsd_string(sK29) ) )
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC130(iV16439)
| ~ cowlThing(iV16439)
| ~ cC108(iV16439)
| ~ cC104(iV16439)
| ~ cC80(iV16440)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cC62(iV16453)
| ~ cowlThing(iV16453)
| ~ cC76(iV16453)
| ~ cC60(iV16453)
| ~ cC44(iV16455)
| ~ cowlThing(iV16455)
| ~ cC56(iV16455)
| ~ cC42(iV16455)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cC68(iV16459)
| ~ cowlThing(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC34(iV16459)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cC44(iV16461)
| ~ cowlThing(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cowlThing(iV16463)
| ~ cC76(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464)
| ~ cowlThing(iV16464)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cowlThing(iV16465)
| ~ cC38(iV16465) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28,sK29]),skolemize(X0,sK28),skolemize(X1,sK29)],[f391]) ).
fof(f393,plain,
! [X0] : ~ cowlNothing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f394,plain,
! [X0] : cowlThing(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f395,plain,
! [X0] :
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f396,plain,
! [X0] :
( xsd_integer(X0)
| xsd_string(X0) ),
inference(cnf_transformation,[],[f248]) ).
fof(f406,plain,
! [X0] :
( ~ cC106(X0)
| cC104(X0) ),
inference(cnf_transformation,[],[f258]) ).
fof(f409,plain,
! [X0] :
( ~ cC108(X0)
| cC106(X0) ),
inference(cnf_transformation,[],[f260]) ).
fof(f410,plain,
! [X0] :
( ~ cC108(X0)
| cC28(X0) ),
inference(cnf_transformation,[],[f260]) ).
fof(f411,plain,
! [X0] :
( cC108(X0)
| ~ cC28(X0)
| ~ cC106(X0) ),
inference(cnf_transformation,[],[f260]) ).
fof(f468,plain,
! [X0] :
( cC32(X0)
| cC34(X0)
| cC30(X0) ),
inference(cnf_transformation,[],[f308]) ).
fof(f474,plain,
! [X0] :
( ~ cTOP(X0)
| cC36(X0)
| cC38(X0) ),
inference(cnf_transformation,[],[f313]) ).
fof(f480,plain,
! [X0,X1] :
( cC42(X0)
| ~ rR1(X0,X1)
| cC8(X1) ),
inference(cnf_transformation,[],[f319]) ).
fof(f481,plain,
! [X0] :
( ~ cC44(X0)
| cC42(X0) ),
inference(cnf_transformation,[],[f321]) ).
fof(f483,plain,
! [X0] :
( cC40(X0)
| cC44(X0)
| ~ cC42(X0) ),
inference(cnf_transformation,[],[f321]) ).
fof(f492,plain,
! [X0] :
( cC48(X0)
| cC46(X0)
| cC50(X0) ),
inference(cnf_transformation,[],[f327]) ).
fof(f500,plain,
! [X0] :
( cC44(X0)
| ~ cC56(X0) ),
inference(cnf_transformation,[],[f335]) ).
fof(f501,plain,
! [X0] :
( cC54(X0)
| ~ cC44(X0)
| cC56(X0) ),
inference(cnf_transformation,[],[f335]) ).
fof(f510,plain,
! [X0,X1] :
( cC60(X0)
| ~ rR1(X0,X1)
| cC12(X1) ),
inference(cnf_transformation,[],[f343]) ).
fof(f512,plain,
! [X0] :
( ~ cC62(X0)
| cC60(X0) ),
inference(cnf_transformation,[],[f345]) ).
fof(f513,plain,
! [X0] :
( cC58(X0)
| ~ cC60(X0)
| cC62(X0) ),
inference(cnf_transformation,[],[f345]) ).
fof(f522,plain,
! [X0] :
( cC66(X0)
| cC64(X0)
| cC68(X0) ),
inference(cnf_transformation,[],[f351]) ).
fof(f532,plain,
! [X0] :
( cC62(X0)
| ~ cC76(X0) ),
inference(cnf_transformation,[],[f362]) ).
fof(f534,plain,
! [X0] :
( cC74(X0)
| cC76(X0)
| ~ cC62(X0) ),
inference(cnf_transformation,[],[f362]) ).
fof(f541,plain,
! [X0] :
( ~ cC82(X0)
| cC80(X0) ),
inference(cnf_transformation,[],[f370]) ).
fof(f543,plain,
! [X0] :
( cC78(X0)
| cC82(X0)
| ~ cC80(X0) ),
inference(cnf_transformation,[],[f370]) ).
fof(f552,plain,
! [X0] :
( cC86(X0)
| cC84(X0)
| cC88(X0) ),
inference(cnf_transformation,[],[f376]) ).
fof(f565,plain,
! [X0] :
( cC82(X0)
| ~ cC98(X0) ),
inference(cnf_transformation,[],[f390]) ).
fof(f568,plain,
! [X0] :
( ~ cTEST(X0)
| cC130(X0) ),
inference(cnf_transformation,[],[f205]) ).
fof(f569,plain,
! [X0] :
( ~ cTEST(X0)
| cC108(X0) ),
inference(cnf_transformation,[],[f205]) ).
fof(f570,plain,
! [X0] :
( cC98(X0)
| ~ rR1(iV16439,X0) ),
inference(cnf_transformation,[],[f206]) ).
fof(f571,plain,
cTEST(iV16439),
inference(cnf_transformation,[],[f62]) ).
fof(f574,plain,
rR1(iV16439,iV16440),
inference(cnf_transformation,[],[f65]) ).
fof(f577,plain,
! [X0] :
( cC76(X0)
| ~ rR1(iV16440,X0) ),
inference(cnf_transformation,[],[f207]) ).
fof(f580,plain,
~ cC78(iV16440),
inference(cnf_transformation,[],[f71]) ).
fof(f583,plain,
rR1(iV16440,iV16463),
inference(cnf_transformation,[],[f74]) ).
fof(f586,plain,
~ cC36(iV16448),
inference(cnf_transformation,[],[f77]) ).
fof(f589,plain,
cTOP(iV16448),
inference(cnf_transformation,[],[f80]) ).
fof(f601,plain,
~ cC58(iV16453),
inference(cnf_transformation,[],[f92]) ).
fof(f602,plain,
~ cC74(iV16453),
inference(cnf_transformation,[],[f93]) ).
fof(f603,plain,
! [X0] :
( cC56(X0)
| ~ rR1(iV16453,X0) ),
inference(cnf_transformation,[],[f215]) ).
fof(f606,plain,
rR1(iV16453,iV16461),
inference(cnf_transformation,[],[f97]) ).
fof(f608,plain,
~ cC40(iV16455),
inference(cnf_transformation,[],[f99]) ).
fof(f613,plain,
~ cC54(iV16455),
inference(cnf_transformation,[],[f104]) ).
fof(f616,plain,
! [X0] :
( cC38(X0)
| ~ rR1(iV16455,X0) ),
inference(cnf_transformation,[],[f219]) ).
fof(f617,plain,
rR1(iV16455,iV16460),
inference(cnf_transformation,[],[f108]) ).
fof(f618,plain,
~ cC36(iV16457),
inference(cnf_transformation,[],[f109]) ).
fof(f623,plain,
cTOP(iV16457),
inference(cnf_transformation,[],[f114]) ).
fof(f630,plain,
~ cC48(iV16459),
inference(cnf_transformation,[],[f121]) ).
fof(f631,plain,
~ cC30(iV16459),
inference(cnf_transformation,[],[f122]) ).
fof(f633,plain,
~ cC86(iV16459),
inference(cnf_transformation,[],[f124]) ).
fof(f634,plain,
~ cC46(iV16459),
inference(cnf_transformation,[],[f125]) ).
fof(f637,plain,
~ cC66(iV16459),
inference(cnf_transformation,[],[f128]) ).
fof(f642,plain,
~ cC84(iV16459),
inference(cnf_transformation,[],[f133]) ).
fof(f643,plain,
~ cC64(iV16459),
inference(cnf_transformation,[],[f134]) ).
fof(f645,plain,
~ cC32(iV16459),
inference(cnf_transformation,[],[f136]) ).
fof(f651,plain,
~ cC8(iV16460),
inference(cnf_transformation,[],[f142]) ).
fof(f661,plain,
~ cC12(iV16461),
inference(cnf_transformation,[],[f152]) ).
fof(f664,plain,
! [X0] :
( cC38(X0)
| ~ rR1(iV16461,X0) ),
inference(cnf_transformation,[],[f231]) ).
fof(f667,plain,
rR1(iV16461,iV16462),
inference(cnf_transformation,[],[f158]) ).
fof(f681,plain,
! [X0] :
( cC56(X0)
| ~ rR1(iV16463,X0) ),
inference(cnf_transformation,[],[f237]) ).
fof(f687,plain,
rR1(iV16463,iV16464),
inference(cnf_transformation,[],[f178]) ).
fof(f692,plain,
! [X0] :
( cC38(X0)
| ~ rR1(iV16464,X0) ),
inference(cnf_transformation,[],[f240]) ).
fof(f698,plain,
rR1(iV16464,iV16465),
inference(cnf_transformation,[],[f189]) ).
fof(f710,plain,
( ~ cowlThing(sK28)
| cowlNothing(sK28)
| ~ xsd_integer(sK29)
| xsd_string(sK29)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC130(iV16439)
| ~ cowlThing(iV16439)
| ~ cC108(iV16439)
| ~ cC104(iV16439)
| ~ cC80(iV16440)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cC62(iV16453)
| ~ cowlThing(iV16453)
| ~ cC76(iV16453)
| ~ cC60(iV16453)
| ~ cC44(iV16455)
| ~ cowlThing(iV16455)
| ~ cC56(iV16455)
| ~ cC42(iV16455)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cC68(iV16459)
| ~ cowlThing(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC34(iV16459)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cC44(iV16461)
| ~ cowlThing(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cowlThing(iV16463)
| ~ cC76(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464)
| ~ cowlThing(iV16464)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cowlThing(iV16465)
| ~ cC38(iV16465) ),
inference(cnf_transformation,[],[f392]) ).
fof(f711,plain,
( ~ cowlThing(sK28)
| cowlNothing(sK28)
| xsd_integer(sK29)
| ~ xsd_string(sK29)
| ~ cC106(iV16439)
| ~ cC28(iV16439)
| ~ cC130(iV16439)
| ~ cowlThing(iV16439)
| ~ cC108(iV16439)
| ~ cC104(iV16439)
| ~ cC80(iV16440)
| ~ cowlThing(iV16440)
| ~ cC82(iV16440)
| ~ cC98(iV16440)
| ~ cowlThing(iV16448)
| ~ cC38(iV16448)
| ~ cC62(iV16453)
| ~ cowlThing(iV16453)
| ~ cC76(iV16453)
| ~ cC60(iV16453)
| ~ cC44(iV16455)
| ~ cowlThing(iV16455)
| ~ cC56(iV16455)
| ~ cC42(iV16455)
| ~ cowlThing(iV16457)
| ~ cC38(iV16457)
| ~ cC68(iV16459)
| ~ cowlThing(iV16459)
| ~ cC88(iV16459)
| ~ cC50(iV16459)
| ~ cC34(iV16459)
| ~ cowlThing(iV16460)
| ~ cC38(iV16460)
| ~ cC44(iV16461)
| ~ cowlThing(iV16461)
| ~ cC56(iV16461)
| ~ cC42(iV16461)
| ~ cowlThing(iV16462)
| ~ cC38(iV16462)
| ~ cC62(iV16463)
| ~ cowlThing(iV16463)
| ~ cC76(iV16463)
| ~ cC60(iV16463)
| ~ cC44(iV16464)
| ~ cowlThing(iV16464)
| ~ cC56(iV16464)
| ~ cC42(iV16464)
| ~ cowlThing(iV16465)
| ~ cC38(iV16465) ),
inference(cnf_transformation,[],[f392]) ).
fof(f713,definition,
( spl30_1
<=> cC38(iV16465) ),
introduced(definition,[new_symbols(definition,[spl30_1])],[avatar_definition]) ).
fof(f714,plain,
( ~ cC38(iV16465)
| spl30_1 ),
inference(avatar_component_clause,[],[f713]) ).
fof(f716,definition,
( spl30_2
<=> cowlThing(iV16465) ),
introduced(definition,[new_symbols(definition,[spl30_2])],[avatar_definition]) ).
fof(f717,plain,
( ~ cowlThing(iV16465)
| spl30_2 ),
inference(avatar_component_clause,[],[f716]) ).
fof(f719,definition,
( spl30_3
<=> cC42(iV16464) ),
introduced(definition,[new_symbols(definition,[spl30_3])],[avatar_definition]) ).
fof(f720,plain,
( ~ cC42(iV16464)
| spl30_3 ),
inference(avatar_component_clause,[],[f719]) ).
fof(f722,definition,
( spl30_4
<=> cC56(iV16464) ),
introduced(definition,[new_symbols(definition,[spl30_4])],[avatar_definition]) ).
fof(f723,plain,
( ~ cC56(iV16464)
| spl30_4 ),
inference(avatar_component_clause,[],[f722]) ).
fof(f725,definition,
( spl30_5
<=> cowlThing(iV16464) ),
introduced(definition,[new_symbols(definition,[spl30_5])],[avatar_definition]) ).
fof(f726,plain,
( ~ cowlThing(iV16464)
| spl30_5 ),
inference(avatar_component_clause,[],[f725]) ).
fof(f728,definition,
( spl30_6
<=> cC44(iV16464) ),
introduced(definition,[new_symbols(definition,[spl30_6])],[avatar_definition]) ).
fof(f729,plain,
( ~ cC44(iV16464)
| spl30_6 ),
inference(avatar_component_clause,[],[f728]) ).
fof(f731,definition,
( spl30_7
<=> cC60(iV16463) ),
introduced(definition,[new_symbols(definition,[spl30_7])],[avatar_definition]) ).
fof(f732,plain,
( ~ cC60(iV16463)
| spl30_7 ),
inference(avatar_component_clause,[],[f731]) ).
fof(f734,definition,
( spl30_8
<=> cC76(iV16463) ),
introduced(definition,[new_symbols(definition,[spl30_8])],[avatar_definition]) ).
fof(f735,plain,
( ~ cC76(iV16463)
| spl30_8 ),
inference(avatar_component_clause,[],[f734]) ).
fof(f737,definition,
( spl30_9
<=> cowlThing(iV16463) ),
introduced(definition,[new_symbols(definition,[spl30_9])],[avatar_definition]) ).
fof(f738,plain,
( ~ cowlThing(iV16463)
| spl30_9 ),
inference(avatar_component_clause,[],[f737]) ).
fof(f740,definition,
( spl30_10
<=> cC62(iV16463) ),
introduced(definition,[new_symbols(definition,[spl30_10])],[avatar_definition]) ).
fof(f741,plain,
( ~ cC62(iV16463)
| spl30_10 ),
inference(avatar_component_clause,[],[f740]) ).
fof(f743,definition,
( spl30_11
<=> cC38(iV16462) ),
introduced(definition,[new_symbols(definition,[spl30_11])],[avatar_definition]) ).
fof(f744,plain,
( ~ cC38(iV16462)
| spl30_11 ),
inference(avatar_component_clause,[],[f743]) ).
fof(f746,definition,
( spl30_12
<=> cowlThing(iV16462) ),
introduced(definition,[new_symbols(definition,[spl30_12])],[avatar_definition]) ).
fof(f747,plain,
( ~ cowlThing(iV16462)
| spl30_12 ),
inference(avatar_component_clause,[],[f746]) ).
fof(f749,definition,
( spl30_13
<=> cC42(iV16461) ),
introduced(definition,[new_symbols(definition,[spl30_13])],[avatar_definition]) ).
fof(f750,plain,
( ~ cC42(iV16461)
| spl30_13 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f752,definition,
( spl30_14
<=> cC56(iV16461) ),
introduced(definition,[new_symbols(definition,[spl30_14])],[avatar_definition]) ).
fof(f753,plain,
( ~ cC56(iV16461)
| spl30_14 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f755,definition,
( spl30_15
<=> cowlThing(iV16461) ),
introduced(definition,[new_symbols(definition,[spl30_15])],[avatar_definition]) ).
fof(f756,plain,
( ~ cowlThing(iV16461)
| spl30_15 ),
inference(avatar_component_clause,[],[f755]) ).
fof(f758,definition,
( spl30_16
<=> cC44(iV16461) ),
introduced(definition,[new_symbols(definition,[spl30_16])],[avatar_definition]) ).
fof(f759,plain,
( ~ cC44(iV16461)
| spl30_16 ),
inference(avatar_component_clause,[],[f758]) ).
fof(f761,definition,
( spl30_17
<=> cC38(iV16460) ),
introduced(definition,[new_symbols(definition,[spl30_17])],[avatar_definition]) ).
fof(f762,plain,
( ~ cC38(iV16460)
| spl30_17 ),
inference(avatar_component_clause,[],[f761]) ).
fof(f764,definition,
( spl30_18
<=> cowlThing(iV16460) ),
introduced(definition,[new_symbols(definition,[spl30_18])],[avatar_definition]) ).
fof(f765,plain,
( ~ cowlThing(iV16460)
| spl30_18 ),
inference(avatar_component_clause,[],[f764]) ).
fof(f767,definition,
( spl30_19
<=> cC34(iV16459) ),
introduced(definition,[new_symbols(definition,[spl30_19])],[avatar_definition]) ).
fof(f770,definition,
( spl30_20
<=> cC50(iV16459) ),
introduced(definition,[new_symbols(definition,[spl30_20])],[avatar_definition]) ).
fof(f773,definition,
( spl30_21
<=> cC88(iV16459) ),
introduced(definition,[new_symbols(definition,[spl30_21])],[avatar_definition]) ).
fof(f776,definition,
( spl30_22
<=> cowlThing(iV16459) ),
introduced(definition,[new_symbols(definition,[spl30_22])],[avatar_definition]) ).
fof(f777,plain,
( ~ cowlThing(iV16459)
| spl30_22 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f779,definition,
( spl30_23
<=> cC68(iV16459) ),
introduced(definition,[new_symbols(definition,[spl30_23])],[avatar_definition]) ).
fof(f782,definition,
( spl30_24
<=> cC38(iV16457) ),
introduced(definition,[new_symbols(definition,[spl30_24])],[avatar_definition]) ).
fof(f785,definition,
( spl30_25
<=> cowlThing(iV16457) ),
introduced(definition,[new_symbols(definition,[spl30_25])],[avatar_definition]) ).
fof(f786,plain,
( ~ cowlThing(iV16457)
| spl30_25 ),
inference(avatar_component_clause,[],[f785]) ).
fof(f788,definition,
( spl30_26
<=> cC42(iV16455) ),
introduced(definition,[new_symbols(definition,[spl30_26])],[avatar_definition]) ).
fof(f789,plain,
( ~ cC42(iV16455)
| spl30_26 ),
inference(avatar_component_clause,[],[f788]) ).
fof(f791,definition,
( spl30_27
<=> cC56(iV16455) ),
introduced(definition,[new_symbols(definition,[spl30_27])],[avatar_definition]) ).
fof(f794,definition,
( spl30_28
<=> cowlThing(iV16455) ),
introduced(definition,[new_symbols(definition,[spl30_28])],[avatar_definition]) ).
fof(f795,plain,
( ~ cowlThing(iV16455)
| spl30_28 ),
inference(avatar_component_clause,[],[f794]) ).
fof(f797,definition,
( spl30_29
<=> cC44(iV16455) ),
introduced(definition,[new_symbols(definition,[spl30_29])],[avatar_definition]) ).
fof(f800,definition,
( spl30_30
<=> cC60(iV16453) ),
introduced(definition,[new_symbols(definition,[spl30_30])],[avatar_definition]) ).
fof(f801,plain,
( ~ cC60(iV16453)
| spl30_30 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f803,definition,
( spl30_31
<=> cC76(iV16453) ),
introduced(definition,[new_symbols(definition,[spl30_31])],[avatar_definition]) ).
fof(f806,definition,
( spl30_32
<=> cowlThing(iV16453) ),
introduced(definition,[new_symbols(definition,[spl30_32])],[avatar_definition]) ).
fof(f807,plain,
( ~ cowlThing(iV16453)
| spl30_32 ),
inference(avatar_component_clause,[],[f806]) ).
fof(f809,definition,
( spl30_33
<=> cC62(iV16453) ),
introduced(definition,[new_symbols(definition,[spl30_33])],[avatar_definition]) ).
fof(f812,definition,
( spl30_34
<=> cC38(iV16448) ),
introduced(definition,[new_symbols(definition,[spl30_34])],[avatar_definition]) ).
fof(f815,definition,
( spl30_35
<=> cowlThing(iV16448) ),
introduced(definition,[new_symbols(definition,[spl30_35])],[avatar_definition]) ).
fof(f816,plain,
( ~ cowlThing(iV16448)
| spl30_35 ),
inference(avatar_component_clause,[],[f815]) ).
fof(f818,definition,
( spl30_36
<=> cC98(iV16440) ),
introduced(definition,[new_symbols(definition,[spl30_36])],[avatar_definition]) ).
fof(f819,plain,
( ~ cC98(iV16440)
| spl30_36 ),
inference(avatar_component_clause,[],[f818]) ).
fof(f821,definition,
( spl30_37
<=> cC82(iV16440) ),
introduced(definition,[new_symbols(definition,[spl30_37])],[avatar_definition]) ).
fof(f824,definition,
( spl30_38
<=> cowlThing(iV16440) ),
introduced(definition,[new_symbols(definition,[spl30_38])],[avatar_definition]) ).
fof(f825,plain,
( ~ cowlThing(iV16440)
| spl30_38 ),
inference(avatar_component_clause,[],[f824]) ).
fof(f827,definition,
( spl30_39
<=> cC80(iV16440) ),
introduced(definition,[new_symbols(definition,[spl30_39])],[avatar_definition]) ).
fof(f828,plain,
( ~ cC80(iV16440)
| spl30_39 ),
inference(avatar_component_clause,[],[f827]) ).
fof(f830,definition,
( spl30_40
<=> cC104(iV16439) ),
introduced(definition,[new_symbols(definition,[spl30_40])],[avatar_definition]) ).
fof(f831,plain,
( ~ cC104(iV16439)
| spl30_40 ),
inference(avatar_component_clause,[],[f830]) ).
fof(f833,definition,
( spl30_41
<=> cC108(iV16439) ),
introduced(definition,[new_symbols(definition,[spl30_41])],[avatar_definition]) ).
fof(f834,plain,
( ~ cC108(iV16439)
| spl30_41 ),
inference(avatar_component_clause,[],[f833]) ).
fof(f836,definition,
( spl30_42
<=> cowlThing(iV16439) ),
introduced(definition,[new_symbols(definition,[spl30_42])],[avatar_definition]) ).
fof(f837,plain,
( ~ cowlThing(iV16439)
| spl30_42 ),
inference(avatar_component_clause,[],[f836]) ).
fof(f839,definition,
( spl30_43
<=> cC130(iV16439) ),
introduced(definition,[new_symbols(definition,[spl30_43])],[avatar_definition]) ).
fof(f840,plain,
( ~ cC130(iV16439)
| spl30_43 ),
inference(avatar_component_clause,[],[f839]) ).
fof(f842,definition,
( spl30_44
<=> cC28(iV16439) ),
introduced(definition,[new_symbols(definition,[spl30_44])],[avatar_definition]) ).
fof(f843,plain,
( ~ cC28(iV16439)
| spl30_44 ),
inference(avatar_component_clause,[],[f842]) ).
fof(f845,definition,
( spl30_45
<=> cC106(iV16439) ),
introduced(definition,[new_symbols(definition,[spl30_45])],[avatar_definition]) ).
fof(f846,plain,
( ~ cC106(iV16439)
| spl30_45 ),
inference(avatar_component_clause,[],[f845]) ).
fof(f848,definition,
( spl30_46
<=> xsd_string(sK29) ),
introduced(definition,[new_symbols(definition,[spl30_46])],[avatar_definition]) ).
fof(f851,definition,
( spl30_47
<=> xsd_integer(sK29) ),
introduced(definition,[new_symbols(definition,[spl30_47])],[avatar_definition]) ).
fof(f852,plain,
( ~ xsd_integer(sK29)
| spl30_47 ),
inference(avatar_component_clause,[],[f851]) ).
fof(f854,definition,
( spl30_48
<=> cowlNothing(sK28) ),
introduced(definition,[new_symbols(definition,[spl30_48])],[avatar_definition]) ).
fof(f855,plain,
( cowlNothing(sK28)
| ~ spl30_48 ),
inference(avatar_component_clause,[],[f854]) ).
fof(f857,definition,
( spl30_49
<=> cowlThing(sK28) ),
introduced(definition,[new_symbols(definition,[spl30_49])],[avatar_definition]) ).
fof(f858,plain,
( ~ cowlThing(sK28)
| spl30_49 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f859,plain,
( ~ spl30_1
| ~ spl30_2
| ~ spl30_3
| ~ spl30_4
| ~ spl30_5
| ~ spl30_6
| ~ spl30_7
| ~ spl30_8
| ~ spl30_9
| ~ spl30_10
| ~ spl30_11
| ~ spl30_12
| ~ spl30_13
| ~ spl30_14
| ~ spl30_15
| ~ spl30_16
| ~ spl30_17
| ~ spl30_18
| ~ spl30_19
| ~ spl30_20
| ~ spl30_21
| ~ spl30_22
| ~ spl30_23
| ~ spl30_24
| ~ spl30_25
| ~ spl30_26
| ~ spl30_27
| ~ spl30_28
| ~ spl30_29
| ~ spl30_30
| ~ spl30_31
| ~ spl30_32
| ~ spl30_33
| ~ spl30_34
| ~ spl30_35
| ~ spl30_36
| ~ spl30_37
| ~ spl30_38
| ~ spl30_39
| ~ spl30_40
| ~ spl30_41
| ~ spl30_42
| ~ spl30_43
| ~ spl30_44
| ~ spl30_45
| spl30_46
| ~ spl30_47
| spl30_48
| ~ spl30_49 ),
inference(avatar_split_clause,[],[f710,f857,f854,f851,f848,f845,f842,f839,f836,f833,f830,f827,f824,f821,f818,f815,f812,f809,f806,f803,f800,f797,f794,f791,f788,f785,f782,f779,f776,f773,f770,f767,f764,f761,f758,f755,f752,f749,f746,f743,f740,f737,f734,f731,f728,f725,f722,f719,f716,f713]) ).
fof(f861,plain,
( xsd_integer(sK29)
| ~ spl30_47 ),
inference(avatar_component_clause,[],[f851]) ).
fof(f862,plain,
( ~ spl30_1
| ~ spl30_2
| ~ spl30_3
| ~ spl30_4
| ~ spl30_5
| ~ spl30_6
| ~ spl30_7
| ~ spl30_8
| ~ spl30_9
| ~ spl30_10
| ~ spl30_11
| ~ spl30_12
| ~ spl30_13
| ~ spl30_14
| ~ spl30_15
| ~ spl30_16
| ~ spl30_17
| ~ spl30_18
| ~ spl30_19
| ~ spl30_20
| ~ spl30_21
| ~ spl30_22
| ~ spl30_23
| ~ spl30_24
| ~ spl30_25
| ~ spl30_26
| ~ spl30_27
| ~ spl30_28
| ~ spl30_29
| ~ spl30_30
| ~ spl30_31
| ~ spl30_32
| ~ spl30_33
| ~ spl30_34
| ~ spl30_35
| ~ spl30_36
| ~ spl30_37
| ~ spl30_38
| ~ spl30_39
| ~ spl30_40
| ~ spl30_41
| ~ spl30_42
| ~ spl30_43
| ~ spl30_44
| ~ spl30_45
| ~ spl30_46
| spl30_47
| spl30_48
| ~ spl30_49 ),
inference(avatar_split_clause,[],[f711,f857,f854,f851,f848,f845,f842,f839,f836,f833,f830,f827,f824,f821,f818,f815,f812,f809,f806,f803,f800,f797,f794,f791,f788,f785,f782,f779,f776,f773,f770,f767,f764,f761,f758,f755,f752,f749,f746,f743,f740,f737,f734,f731,f728,f725,f722,f719,f716,f713]) ).
fof(f867,plain,
! [X0] :
( cC42(X0)
| ~ cC56(X0) ),
inference(resolution,[],[f500,f481]) ).
fof(f870,plain,
! [X0] :
( cC60(X0)
| ~ cC76(X0) ),
inference(resolution,[],[f532,f512]) ).
fof(f871,plain,
! [X0] :
( cC80(X0)
| ~ cC98(X0) ),
inference(resolution,[],[f565,f541]) ).
fof(f872,plain,
cC130(iV16439),
inference(resolution,[],[f568,f571]) ).
fof(f873,plain,
cC108(iV16439),
inference(resolution,[],[f569,f571]) ).
fof(f874,plain,
cC28(iV16439),
inference(resolution,[],[f873,f410]) ).
fof(f875,plain,
cC106(iV16439),
inference(resolution,[],[f873,f409]) ).
fof(f876,plain,
cC104(iV16439),
inference(resolution,[],[f875,f406]) ).
fof(f896,plain,
( ~ rR1(iV16464,iV16465)
| spl30_1 ),
inference(resolution,[],[f692,f714]) ).
fof(f897,plain,
( $false
| spl30_1 ),
inference(resolution,[],[f896,f698]) ).
fof(f898,plain,
spl30_1,
inference(avatar_contradiction_clause,[],[f897]) ).
fof(f899,plain,
( $false
| spl30_2 ),
inference(resolution,[],[f717,f394]) ).
fof(f900,plain,
spl30_2,
inference(avatar_contradiction_clause,[],[f899]) ).
fof(f901,plain,
( ~ cC56(iV16464)
| spl30_3 ),
inference(resolution,[],[f720,f867]) ).
fof(f902,plain,
( ~ spl30_4
| spl30_3 ),
inference(avatar_split_clause,[],[f901,f719,f722]) ).
fof(f903,plain,
( ~ rR1(iV16463,iV16464)
| spl30_4 ),
inference(resolution,[],[f723,f681]) ).
fof(f905,plain,
( $false
| spl30_4 ),
inference(resolution,[],[f903,f687]) ).
fof(f906,plain,
spl30_4,
inference(avatar_contradiction_clause,[],[f905]) ).
fof(f907,plain,
( $false
| spl30_5 ),
inference(resolution,[],[f726,f394]) ).
fof(f908,plain,
spl30_5,
inference(avatar_contradiction_clause,[],[f907]) ).
fof(f909,plain,
( ~ cC56(iV16464)
| spl30_6 ),
inference(resolution,[],[f729,f500]) ).
fof(f910,plain,
( ~ spl30_4
| spl30_6 ),
inference(avatar_split_clause,[],[f909,f728,f722]) ).
fof(f911,plain,
( ~ cC76(iV16463)
| spl30_7 ),
inference(resolution,[],[f732,f870]) ).
fof(f912,plain,
( ~ spl30_8
| spl30_7 ),
inference(avatar_split_clause,[],[f911,f731,f734]) ).
fof(f913,plain,
( ~ rR1(iV16440,iV16463)
| spl30_8 ),
inference(resolution,[],[f735,f577]) ).
fof(f914,plain,
( $false
| spl30_8 ),
inference(resolution,[],[f913,f583]) ).
fof(f915,plain,
spl30_8,
inference(avatar_contradiction_clause,[],[f914]) ).
fof(f916,plain,
( $false
| spl30_9 ),
inference(resolution,[],[f738,f394]) ).
fof(f917,plain,
spl30_9,
inference(avatar_contradiction_clause,[],[f916]) ).
fof(f918,plain,
( ~ cC76(iV16463)
| spl30_10 ),
inference(resolution,[],[f741,f532]) ).
fof(f919,plain,
( ~ spl30_8
| spl30_10 ),
inference(avatar_split_clause,[],[f918,f740,f734]) ).
fof(f921,plain,
( ~ rR1(iV16461,iV16462)
| spl30_11 ),
inference(resolution,[],[f744,f664]) ).
fof(f923,plain,
( $false
| spl30_11 ),
inference(resolution,[],[f921,f667]) ).
fof(f924,plain,
spl30_11,
inference(avatar_contradiction_clause,[],[f923]) ).
fof(f925,plain,
( $false
| spl30_12 ),
inference(resolution,[],[f747,f394]) ).
fof(f926,plain,
spl30_12,
inference(avatar_contradiction_clause,[],[f925]) ).
fof(f927,plain,
( ~ cC56(iV16461)
| spl30_13 ),
inference(resolution,[],[f750,f867]) ).
fof(f928,plain,
( ~ spl30_14
| spl30_13 ),
inference(avatar_split_clause,[],[f927,f749,f752]) ).
fof(f930,plain,
( ~ rR1(iV16453,iV16461)
| spl30_14 ),
inference(resolution,[],[f753,f603]) ).
fof(f931,plain,
( $false
| spl30_14 ),
inference(resolution,[],[f930,f606]) ).
fof(f932,plain,
spl30_14,
inference(avatar_contradiction_clause,[],[f931]) ).
fof(f933,plain,
( $false
| spl30_15 ),
inference(resolution,[],[f756,f394]) ).
fof(f934,plain,
spl30_15,
inference(avatar_contradiction_clause,[],[f933]) ).
fof(f935,plain,
( ~ cC56(iV16461)
| spl30_16 ),
inference(resolution,[],[f759,f500]) ).
fof(f936,plain,
( ~ spl30_14
| spl30_16 ),
inference(avatar_split_clause,[],[f935,f758,f752]) ).
fof(f939,plain,
( ~ rR1(iV16455,iV16460)
| spl30_17 ),
inference(resolution,[],[f762,f616]) ).
fof(f940,plain,
( $false
| spl30_17 ),
inference(resolution,[],[f939,f617]) ).
fof(f941,plain,
spl30_17,
inference(avatar_contradiction_clause,[],[f940]) ).
fof(f942,plain,
( $false
| spl30_18 ),
inference(resolution,[],[f765,f394]) ).
fof(f943,plain,
spl30_18,
inference(avatar_contradiction_clause,[],[f942]) ).
fof(f985,plain,
( cC34(iV16459)
| cC30(iV16459) ),
inference(resolution,[],[f468,f645]) ).
fof(f990,definition,
( spl30_50
<=> cC30(iV16459) ),
introduced(definition,[new_symbols(definition,[spl30_50])],[avatar_definition]) ).
fof(f991,plain,
( cC30(iV16459)
| ~ spl30_50 ),
inference(avatar_component_clause,[],[f990]) ).
fof(f993,plain,
( spl30_50
| spl30_19 ),
inference(avatar_split_clause,[],[f985,f767,f990]) ).
fof(f1000,plain,
( cC36(iV16448)
| cC38(iV16448) ),
inference(resolution,[],[f474,f589]) ).
fof(f1002,plain,
( cC36(iV16457)
| cC38(iV16457) ),
inference(resolution,[],[f474,f623]) ).
fof(f1017,definition,
( spl30_53
<=> cC36(iV16457) ),
introduced(definition,[new_symbols(definition,[spl30_53])],[avatar_definition]) ).
fof(f1018,plain,
( cC36(iV16457)
| ~ spl30_53 ),
inference(avatar_component_clause,[],[f1017]) ).
fof(f1019,plain,
( spl30_24
| spl30_53 ),
inference(avatar_split_clause,[],[f1002,f1017,f782]) ).
fof(f1027,definition,
( spl30_55
<=> cC36(iV16448) ),
introduced(definition,[new_symbols(definition,[spl30_55])],[avatar_definition]) ).
fof(f1028,plain,
( cC36(iV16448)
| ~ spl30_55 ),
inference(avatar_component_clause,[],[f1027]) ).
fof(f1029,plain,
( spl30_34
| spl30_55 ),
inference(avatar_split_clause,[],[f1000,f1027,f812]) ).
fof(f1035,plain,
( cC44(iV16455)
| ~ cC42(iV16455) ),
inference(resolution,[],[f483,f608]) ).
fof(f1040,plain,
( ~ spl30_26
| spl30_29 ),
inference(avatar_split_clause,[],[f1035,f797,f788]) ).
fof(f1061,plain,
( cC46(iV16459)
| cC50(iV16459) ),
inference(resolution,[],[f492,f630]) ).
fof(f1067,definition,
( spl30_56
<=> cC46(iV16459) ),
introduced(definition,[new_symbols(definition,[spl30_56])],[avatar_definition]) ).
fof(f1068,plain,
( cC46(iV16459)
| ~ spl30_56 ),
inference(avatar_component_clause,[],[f1067]) ).
fof(f1069,plain,
( spl30_20
| spl30_56 ),
inference(avatar_split_clause,[],[f1061,f1067,f770]) ).
fof(f1074,plain,
( ~ cC44(iV16455)
| cC56(iV16455) ),
inference(resolution,[],[f501,f613]) ).
fof(f1079,plain,
( spl30_27
| ~ spl30_29 ),
inference(avatar_split_clause,[],[f1074,f797,f791]) ).
fof(f1090,plain,
( ~ cC60(iV16453)
| cC62(iV16453) ),
inference(resolution,[],[f513,f601]) ).
fof(f1098,plain,
( spl30_33
| ~ spl30_30 ),
inference(avatar_split_clause,[],[f1090,f800,f809]) ).
fof(f1113,plain,
( cC64(iV16459)
| cC68(iV16459) ),
inference(resolution,[],[f522,f637]) ).
fof(f1119,definition,
( spl30_57
<=> cC64(iV16459) ),
introduced(definition,[new_symbols(definition,[spl30_57])],[avatar_definition]) ).
fof(f1120,plain,
( cC64(iV16459)
| ~ spl30_57 ),
inference(avatar_component_clause,[],[f1119]) ).
fof(f1121,plain,
( spl30_23
| spl30_57 ),
inference(avatar_split_clause,[],[f1113,f1119,f779]) ).
fof(f1122,plain,
( cC76(iV16453)
| ~ cC62(iV16453) ),
inference(resolution,[],[f534,f602]) ).
fof(f1130,plain,
( ~ spl30_33
| spl30_31 ),
inference(avatar_split_clause,[],[f1122,f803,f809]) ).
fof(f1134,plain,
( cC82(iV16440)
| ~ cC80(iV16440) ),
inference(resolution,[],[f543,f580]) ).
fof(f1139,plain,
( ~ spl30_39
| spl30_37 ),
inference(avatar_split_clause,[],[f1134,f821,f827]) ).
fof(f1140,plain,
( ~ cC98(iV16440)
| spl30_39 ),
inference(resolution,[],[f828,f871]) ).
fof(f1141,plain,
( ~ spl30_36
| spl30_39 ),
inference(avatar_split_clause,[],[f1140,f827,f818]) ).
fof(f1146,plain,
( ~ rR1(iV16439,iV16440)
| spl30_36 ),
inference(resolution,[],[f819,f570]) ).
fof(f1147,plain,
( $false
| spl30_36 ),
inference(resolution,[],[f1146,f574]) ).
fof(f1148,plain,
spl30_36,
inference(avatar_contradiction_clause,[],[f1147]) ).
fof(f1155,plain,
( cC84(iV16459)
| cC88(iV16459) ),
inference(resolution,[],[f552,f633]) ).
fof(f1161,definition,
( spl30_58
<=> cC84(iV16459) ),
introduced(definition,[new_symbols(definition,[spl30_58])],[avatar_definition]) ).
fof(f1162,plain,
( cC84(iV16459)
| ~ spl30_58 ),
inference(avatar_component_clause,[],[f1161]) ).
fof(f1163,plain,
( spl30_21
| spl30_58 ),
inference(avatar_split_clause,[],[f1155,f1161,f773]) ).
fof(f1164,plain,
( $false
| ~ spl30_58 ),
inference(resolution,[],[f1162,f642]) ).
fof(f1168,plain,
~ spl30_58,
inference(avatar_contradiction_clause,[],[f1164]) ).
fof(f1223,plain,
( ! [X0] :
( cC8(X0)
| ~ rR1(iV16455,X0) )
| spl30_26 ),
inference(resolution,[],[f480,f789]) ).
fof(f1224,plain,
( ~ rR1(iV16455,iV16460)
| spl30_26 ),
inference(resolution,[],[f1223,f651]) ).
fof(f1231,plain,
( $false
| spl30_26 ),
inference(resolution,[],[f1224,f617]) ).
fof(f1232,plain,
spl30_26,
inference(avatar_contradiction_clause,[],[f1231]) ).
fof(f1251,plain,
( ! [X0] :
( cC12(X0)
| ~ rR1(iV16453,X0) )
| spl30_30 ),
inference(resolution,[],[f510,f801]) ).
fof(f1252,plain,
( ~ rR1(iV16453,iV16461)
| spl30_30 ),
inference(resolution,[],[f1251,f661]) ).
fof(f1256,plain,
( $false
| spl30_30 ),
inference(resolution,[],[f1252,f606]) ).
fof(f1257,plain,
spl30_30,
inference(avatar_contradiction_clause,[],[f1256]) ).
fof(f1258,plain,
( $false
| spl30_22 ),
inference(resolution,[],[f777,f394]) ).
fof(f1259,plain,
spl30_22,
inference(avatar_contradiction_clause,[],[f1258]) ).
fof(f1260,plain,
( $false
| spl30_25 ),
inference(resolution,[],[f786,f394]) ).
fof(f1261,plain,
spl30_25,
inference(avatar_contradiction_clause,[],[f1260]) ).
fof(f1262,plain,
( $false
| spl30_28 ),
inference(resolution,[],[f795,f394]) ).
fof(f1263,plain,
spl30_28,
inference(avatar_contradiction_clause,[],[f1262]) ).
fof(f1264,plain,
( $false
| spl30_32 ),
inference(resolution,[],[f807,f394]) ).
fof(f1265,plain,
spl30_32,
inference(avatar_contradiction_clause,[],[f1264]) ).
fof(f1266,plain,
( $false
| spl30_35 ),
inference(resolution,[],[f816,f394]) ).
fof(f1267,plain,
spl30_35,
inference(avatar_contradiction_clause,[],[f1266]) ).
fof(f1268,plain,
( $false
| spl30_38 ),
inference(resolution,[],[f825,f394]) ).
fof(f1269,plain,
spl30_38,
inference(avatar_contradiction_clause,[],[f1268]) ).
fof(f1270,plain,
( $false
| spl30_40 ),
inference(resolution,[],[f831,f876]) ).
fof(f1272,plain,
spl30_40,
inference(avatar_contradiction_clause,[],[f1270]) ).
fof(f1274,plain,
( ~ cC28(iV16439)
| ~ cC106(iV16439)
| spl30_41 ),
inference(resolution,[],[f834,f411]) ).
fof(f1276,plain,
( ~ spl30_45
| ~ spl30_44
| spl30_41 ),
inference(avatar_split_clause,[],[f1274,f833,f842,f845]) ).
fof(f1277,plain,
( $false
| spl30_42 ),
inference(resolution,[],[f837,f394]) ).
fof(f1278,plain,
spl30_42,
inference(avatar_contradiction_clause,[],[f1277]) ).
fof(f1279,plain,
( $false
| spl30_43 ),
inference(resolution,[],[f840,f872]) ).
fof(f1280,plain,
spl30_43,
inference(avatar_contradiction_clause,[],[f1279]) ).
fof(f1281,plain,
( $false
| spl30_44 ),
inference(resolution,[],[f843,f874]) ).
fof(f1282,plain,
spl30_44,
inference(avatar_contradiction_clause,[],[f1281]) ).
fof(f1283,plain,
( $false
| spl30_45 ),
inference(resolution,[],[f846,f875]) ).
fof(f1284,plain,
spl30_45,
inference(avatar_contradiction_clause,[],[f1283]) ).
fof(f1285,plain,
( $false
| spl30_49 ),
inference(resolution,[],[f858,f394]) ).
fof(f1286,plain,
spl30_49,
inference(avatar_contradiction_clause,[],[f1285]) ).
fof(f1287,plain,
( xsd_string(sK29)
| spl30_47 ),
inference(resolution,[],[f852,f396]) ).
fof(f1288,plain,
( spl30_46
| spl30_47 ),
inference(avatar_split_clause,[],[f1287,f851,f848]) ).
fof(f1289,plain,
( ~ xsd_string(sK29)
| ~ spl30_47 ),
inference(resolution,[],[f861,f395]) ).
fof(f1290,plain,
( ~ spl30_46
| ~ spl30_47 ),
inference(avatar_split_clause,[],[f1289,f851,f848]) ).
fof(f1300,plain,
( $false
| ~ spl30_53 ),
inference(resolution,[],[f1018,f618]) ).
fof(f1304,plain,
~ spl30_53,
inference(avatar_contradiction_clause,[],[f1300]) ).
fof(f1310,plain,
( $false
| ~ spl30_50 ),
inference(resolution,[],[f991,f631]) ).
fof(f1314,plain,
~ spl30_50,
inference(avatar_contradiction_clause,[],[f1310]) ).
fof(f1338,plain,
( $false
| ~ spl30_56 ),
inference(resolution,[],[f1068,f634]) ).
fof(f1342,plain,
~ spl30_56,
inference(avatar_contradiction_clause,[],[f1338]) ).
fof(f1363,plain,
( $false
| ~ spl30_57 ),
inference(resolution,[],[f1120,f643]) ).
fof(f1367,plain,
~ spl30_57,
inference(avatar_contradiction_clause,[],[f1363]) ).
fof(f1375,plain,
( $false
| ~ spl30_48 ),
inference(resolution,[],[f855,f393]) ).
fof(f1376,plain,
~ spl30_48,
inference(avatar_contradiction_clause,[],[f1375]) ).
fof(f1380,plain,
( $false
| ~ spl30_55 ),
inference(resolution,[],[f1028,f586]) ).
fof(f1384,plain,
~ spl30_55,
inference(avatar_contradiction_clause,[],[f1380]) ).
cnf(s1,plain,
( ~ spl30_1
| ~ spl30_2
| ~ spl30_3
| ~ spl30_4
| ~ spl30_5
| ~ spl30_6
| ~ spl30_7
| ~ spl30_8
| ~ spl30_9
| ~ spl30_10
| ~ spl30_11
| ~ spl30_12
| ~ spl30_13
| ~ spl30_14
| ~ spl30_15
| ~ spl30_16
| ~ spl30_17
| ~ spl30_18
| ~ spl30_19
| ~ spl30_20
| ~ spl30_21
| ~ spl30_22
| ~ spl30_23
| ~ spl30_24
| ~ spl30_25
| ~ spl30_26
| ~ spl30_27
| ~ spl30_28
| ~ spl30_29
| ~ spl30_30
| ~ spl30_31
| ~ spl30_32
| ~ spl30_33
| ~ spl30_34
| ~ spl30_35
| ~ spl30_36
| ~ spl30_37
| ~ spl30_38
| ~ spl30_39
| ~ spl30_40
| ~ spl30_41
| ~ spl30_42
| ~ spl30_43
| ~ spl30_44
| ~ spl30_45
| spl30_46
| ~ spl30_47
| spl30_48
| ~ spl30_49 ),
inference(sat_conversion,[],[f859]) ).
cnf(s2,plain,
( ~ spl30_1
| ~ spl30_2
| ~ spl30_3
| ~ spl30_4
| ~ spl30_5
| ~ spl30_6
| ~ spl30_7
| ~ spl30_8
| ~ spl30_9
| ~ spl30_10
| ~ spl30_11
| ~ spl30_12
| ~ spl30_13
| ~ spl30_14
| ~ spl30_15
| ~ spl30_16
| ~ spl30_17
| ~ spl30_18
| ~ spl30_19
| ~ spl30_20
| ~ spl30_21
| ~ spl30_22
| ~ spl30_23
| ~ spl30_24
| ~ spl30_25
| ~ spl30_26
| ~ spl30_27
| ~ spl30_28
| ~ spl30_29
| ~ spl30_30
| ~ spl30_31
| ~ spl30_32
| ~ spl30_33
| ~ spl30_34
| ~ spl30_35
| ~ spl30_36
| ~ spl30_37
| ~ spl30_38
| ~ spl30_39
| ~ spl30_40
| ~ spl30_41
| ~ spl30_42
| ~ spl30_43
| ~ spl30_44
| ~ spl30_45
| ~ spl30_46
| spl30_47
| spl30_48
| ~ spl30_49 ),
inference(sat_conversion,[],[f862]) ).
cnf(s3,plain,
spl30_1,
inference(sat_conversion,[],[f898]) ).
cnf(s4,plain,
spl30_2,
inference(sat_conversion,[],[f900]) ).
cnf(s5,plain,
( spl30_3
| ~ spl30_4 ),
inference(sat_conversion,[],[f902]) ).
cnf(s6,plain,
spl30_4,
inference(sat_conversion,[],[f906]) ).
cnf(s7,plain,
spl30_5,
inference(sat_conversion,[],[f908]) ).
cnf(s8,plain,
( ~ spl30_4
| spl30_6 ),
inference(sat_conversion,[],[f910]) ).
cnf(s9,plain,
( spl30_7
| ~ spl30_8 ),
inference(sat_conversion,[],[f912]) ).
cnf(s10,plain,
spl30_8,
inference(sat_conversion,[],[f915]) ).
cnf(s11,plain,
spl30_9,
inference(sat_conversion,[],[f917]) ).
cnf(s12,plain,
( ~ spl30_8
| spl30_10 ),
inference(sat_conversion,[],[f919]) ).
cnf(s13,plain,
spl30_11,
inference(sat_conversion,[],[f924]) ).
cnf(s14,plain,
spl30_12,
inference(sat_conversion,[],[f926]) ).
cnf(s15,plain,
( spl30_13
| ~ spl30_14 ),
inference(sat_conversion,[],[f928]) ).
cnf(s16,plain,
spl30_14,
inference(sat_conversion,[],[f932]) ).
cnf(s17,plain,
spl30_15,
inference(sat_conversion,[],[f934]) ).
cnf(s18,plain,
( ~ spl30_14
| spl30_16 ),
inference(sat_conversion,[],[f936]) ).
cnf(s19,plain,
spl30_17,
inference(sat_conversion,[],[f941]) ).
cnf(s20,plain,
spl30_18,
inference(sat_conversion,[],[f943]) ).
cnf(s21,plain,
( spl30_19
| spl30_50 ),
inference(sat_conversion,[],[f993]) ).
cnf(s24,plain,
( spl30_24
| spl30_53 ),
inference(sat_conversion,[],[f1019]) ).
cnf(s26,plain,
( spl30_34
| spl30_55 ),
inference(sat_conversion,[],[f1029]) ).
cnf(s28,plain,
( ~ spl30_26
| spl30_29 ),
inference(sat_conversion,[],[f1040]) ).
cnf(s31,plain,
( spl30_20
| spl30_56 ),
inference(sat_conversion,[],[f1069]) ).
cnf(s33,plain,
( spl30_27
| ~ spl30_29 ),
inference(sat_conversion,[],[f1079]) ).
cnf(s36,plain,
( ~ spl30_30
| spl30_33 ),
inference(sat_conversion,[],[f1098]) ).
cnf(s38,plain,
( spl30_23
| spl30_57 ),
inference(sat_conversion,[],[f1121]) ).
cnf(s40,plain,
( spl30_31
| ~ spl30_33 ),
inference(sat_conversion,[],[f1130]) ).
cnf(s41,plain,
( spl30_37
| ~ spl30_39 ),
inference(sat_conversion,[],[f1139]) ).
cnf(s42,plain,
( ~ spl30_36
| spl30_39 ),
inference(sat_conversion,[],[f1141]) ).
cnf(s43,plain,
spl30_36,
inference(sat_conversion,[],[f1148]) ).
cnf(s44,plain,
( spl30_21
| spl30_58 ),
inference(sat_conversion,[],[f1163]) ).
cnf(s45,plain,
~ spl30_58,
inference(sat_conversion,[],[f1168]) ).
cnf(s48,plain,
spl30_26,
inference(sat_conversion,[],[f1232]) ).
cnf(s49,plain,
spl30_30,
inference(sat_conversion,[],[f1257]) ).
cnf(s50,plain,
spl30_22,
inference(sat_conversion,[],[f1259]) ).
cnf(s51,plain,
spl30_25,
inference(sat_conversion,[],[f1261]) ).
cnf(s52,plain,
spl30_28,
inference(sat_conversion,[],[f1263]) ).
cnf(s53,plain,
spl30_32,
inference(sat_conversion,[],[f1265]) ).
cnf(s54,plain,
spl30_35,
inference(sat_conversion,[],[f1267]) ).
cnf(s55,plain,
spl30_38,
inference(sat_conversion,[],[f1269]) ).
cnf(s56,plain,
spl30_40,
inference(sat_conversion,[],[f1272]) ).
cnf(s58,plain,
( spl30_41
| ~ spl30_44
| ~ spl30_45 ),
inference(sat_conversion,[],[f1276]) ).
cnf(s59,plain,
spl30_42,
inference(sat_conversion,[],[f1278]) ).
cnf(s60,plain,
spl30_43,
inference(sat_conversion,[],[f1280]) ).
cnf(s61,plain,
spl30_44,
inference(sat_conversion,[],[f1282]) ).
cnf(s62,plain,
spl30_45,
inference(sat_conversion,[],[f1284]) ).
cnf(s63,plain,
spl30_49,
inference(sat_conversion,[],[f1286]) ).
cnf(s64,plain,
( spl30_46
| spl30_47 ),
inference(sat_conversion,[],[f1288]) ).
cnf(s65,plain,
( ~ spl30_46
| ~ spl30_47 ),
inference(sat_conversion,[],[f1290]) ).
cnf(s66,plain,
~ spl30_53,
inference(sat_conversion,[],[f1304]) ).
cnf(s67,plain,
~ spl30_50,
inference(sat_conversion,[],[f1314]) ).
cnf(s68,plain,
~ spl30_56,
inference(sat_conversion,[],[f1342]) ).
cnf(s69,plain,
~ spl30_57,
inference(sat_conversion,[],[f1367]) ).
cnf(s70,plain,
~ spl30_48,
inference(sat_conversion,[],[f1376]) ).
cnf(s71,plain,
~ spl30_55,
inference(sat_conversion,[],[f1384]) ).
cnf(s72,plain,
spl30_41,
inference(rat,[],[s58,s62,s61]) ).
cnf(s73,plain,
spl30_21,
inference(rat,[],[s44,s45]) ).
cnf(s74,plain,
spl30_39,
inference(rat,[],[s42,s43]) ).
cnf(s75,plain,
spl30_37,
inference(rat,[],[s41,s74]) ).
cnf(s76,plain,
spl30_23,
inference(rat,[],[s38,s69]) ).
cnf(s77,plain,
spl30_33,
inference(rat,[],[s36,s49]) ).
cnf(s78,plain,
spl30_31,
inference(rat,[],[s40,s77]) ).
cnf(s79,plain,
spl30_20,
inference(rat,[],[s31,s68]) ).
cnf(s80,plain,
spl30_29,
inference(rat,[],[s28,s48]) ).
cnf(s81,plain,
spl30_27,
inference(rat,[],[s33,s80]) ).
cnf(s82,plain,
spl30_34,
inference(rat,[],[s26,s71]) ).
cnf(s83,plain,
spl30_24,
inference(rat,[],[s24,s66]) ).
cnf(s84,plain,
spl30_19,
inference(rat,[],[s21,s67]) ).
cnf(s85,plain,
spl30_16,
inference(rat,[],[s18,s16]) ).
cnf(s86,plain,
spl30_13,
inference(rat,[],[s15,s16]) ).
cnf(s87,plain,
spl30_10,
inference(rat,[],[s12,s10]) ).
cnf(s88,plain,
spl30_7,
inference(rat,[],[s9,s10]) ).
cnf(s89,plain,
spl30_6,
inference(rat,[],[s8,s6]) ).
cnf(s90,plain,
spl30_3,
inference(rat,[],[s5,s6]) ).
cnf(s91,plain,
( ~ spl30_46
| spl30_47 ),
inference(rat,[],[s2,s63,s70,s62,s61,s60,s59,s72,s56,s74,s55,s75,s43,s54,s82,s77,s53,s78,s49,s80,s52,s81,s48,s51,s83,s76,s50,s73,s79,s84,s20,s19,s85,s17,s16,s86,s14,s13,s87,s11,s10,s88,s89,s7,s6,s90,s4,s3]) ).
cnf(s92,plain,
( spl30_46
| ~ spl30_47 ),
inference(rat,[],[s1,s63,s70,s62,s61,s60,s59,s72,s56,s74,s55,s75,s43,s54,s82,s77,s53,s78,s49,s80,s52,s81,s48,s51,s83,s76,s50,s73,s79,s84,s20,s19,s85,s17,s16,s86,s14,s13,s87,s11,s10,s88,s89,s7,s6,s90,s4,s3]) ).
cnf(s93,plain,
spl30_46,
inference(rat,[],[s92,s64]) ).
cnf(s94,plain,
~ spl30_47,
inference(rat,[],[s65,s93]) ).
cnf(s95,plain,
$false,
inference(rat,[],[s91,s94,s93]) ).
fof(f1385,plain,
$false,
inference(avatar_sat_refutation,[],[s95]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS153+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.11/0.36 % Computer : n020.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 13:31:05 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.42 Running first-order theorem proving
% 0.15/0.42 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
% 0.50/1.02 % (3387613)Detected formulas, will run a generic FOF schedule.
% 0.50/1.02 % (3387626)dis-21_1_sil=8000:lcm=predicate:random_seed=3603765579: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)
% 0.50/1.02 % (3387626)First to succeed.
% 0.50/1.02 % (3387626)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3387613"
% 0.50/1.02 % (3387624)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2006219573:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 0.50/1.02 % (3387623)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1503410945:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 0.50/1.02 % (3387620)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=1914420137:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 0.50/1.02 % (3387621)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=2909776996:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 0.50/1.02 % (3387622)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=3415927251:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 0.50/1.02 % (3387623)Refutation not found, incomplete strategy
% 0.50/1.02 % (3387623)------------------------------
% 0.50/1.02 % (3387623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.50/1.02 % (3387623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/1.02 % (3387623)CaDiCaL version: 2.1.3
% 0.50/1.02 % (3387623)Termination reason: Refutation not found, incomplete strategy
% 0.50/1.02 % (3387623)Time elapsed: 0.002 s
% 0.50/1.02 % (3387623)Peak memory usage: 88 MB
% 0.50/1.02 % (3387623)Instructions burned: 1 (million)
% 0.50/1.02 % (3387624)Refutation not found, incomplete strategy
% 0.50/1.02 % (3387624)------------------------------
% 0.50/1.02 % (3387624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.50/1.02 % (3387624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.50/1.02 % (3387624)CaDiCaL version: 2.1.3
% 0.50/1.02 % (3387624)Termination reason: Refutation not found, incomplete strategy
% 0.50/1.02 % (3387624)Time elapsed: 0.003 s
% 0.50/1.02 % (3387624)Peak memory usage: 88 MB
% 0.50/1.02 % (3387624)Instructions burned: 4 (million)
% 0.50/1.02 % (3387625)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1263600168:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 0.50/1.02 % (3387625)Also succeeded, but the first one will report.
% 0.50/1.02 % (3387626)Refutation found. Thanks to Tanya!
% 0.50/1.02 % SZS status Theorem for theBenchmark
% 0.50/1.02 % SZS output start Proof for theBenchmark
% See solution above
% 2.29/1.12 % (3387626)------------------------------
% 2.29/1.12 % (3387626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.29/1.12 % (3387626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.29/1.12 % (3387626)CaDiCaL version: 2.1.3
% 2.29/1.12 % (3387626)Termination reason: Refutation
% 2.29/1.12 % (3387626)Time elapsed: 0.009 s
% 2.29/1.12 % (3387626)Peak memory usage: 90 MB
% 2.29/1.12 % (3387626)Instructions burned: 26 (million)
% 2.29/1.12 % (3387626)------------------------------
% 2.29/1.12 % (3387626)------------------------------
% 2.29/1.12 % (3387613)Success in time 0.264 s
% 2.29/1.12 % Vampire exiting
%------------------------------------------------------------------------------