%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR116+29 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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 09:43:39 AM UTC 2026
% Result : Theorem 7.02s 2.09s
% Output : Refutation 7.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 12
% Syntax : Number of formulae : 111 ( 21 unt; 4 def)
% Number of atoms : 2488 ( 0 equ)
% Maximal formula atoms : 370 ( 22 avg)
% Number of connectives : 2686 ( 309 ~; 268 |;2100 &)
% ( 4 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 370 ( 25 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 32 ( 31 usr; 5 prp; 0-12 aty)
% Number of functors : 89 ( 89 usr; 80 con; 0-3 aty)
% Number of variables : 267 ( 0 sgn 224 !; 43 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [X0,X1] :
( fact(X0,X1)
=> has_fact_leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',has_fact_eq) ).
fof(f95,axiom,
! [X0,X1] :
( ( has_fact_leq(X1,real)
& loc(X1,X0) )
=> ? [X2] :
( loc(X2,X0)
& obj(X2,X1)
& subs(X2,geben_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',loc__geben_1_1_loc) ).
fof(f155,axiom,
! [X0,X1,X2] :
( ( prop(X0,X1)
& state_adjective_state_binding(X1,X2) )
=> ? [X3,X4,X5] :
( in(X5,X3)
& attr(X3,X4)
& loc(X0,X5)
& sub(X3,land_1_1)
& sub(X4,name_1_1)
& val(X4,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',state_adjective__in_state) ).
fof(f162,axiom,
! [X0,X1,X2] :
( ( arg1(X0,X1)
& arg2(X0,X2)
& subr(X0,sub_0) )
=> ? [X3,X4,X5] :
( arg1(X4,X1)
& arg2(X4,X5)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& sub(X5,X2)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sub__bezeichnen_1_1_als) ).
fof(f163,axiom,
! [X0,X1] :
( sub(X0,X1)
=> ? [X2] :
( arg1(X2,X0)
& arg2(X2,X1)
& subr(X2,sub_0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sub__sub_0_expansion) ).
fof(f9161,axiom,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_8980) ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( in(X5,X6)
& arg1(X3,X0)
& arg2(X3,X4)
& attr(X0,X1)
& attr(X0,X2)
& attr(X6,X7)
& obj(X8,X0)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X9)
& sub(X7,name_1_1)
& subr(X3,rprs_0)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X7,s__374dafrika_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_010_mira_news_1824) ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( in(X5,X6)
& arg1(X3,X0)
& arg2(X3,X4)
& attr(X0,X1)
& attr(X0,X2)
& attr(X6,X7)
& obj(X8,X0)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X9)
& sub(X7,name_1_1)
& subr(X3,rprs_0)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X7,s__374dafrika_0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( sub(c9434,abkommen_1_1)
& pred(c9443,verfechter_1_1)
& attch(c9448,c9443)
& prop(c9448,angolanisch_1_1)
& sub(c9448,regierung_1_1)
& attr(c9456,c9457)
& sub(c9456,einrichtung_1_2)
& sub(c9457,name_1_1)
& val(c9457,unita_0)
& pred(c9458,meuterer_1_1)
& sub(c9464,druck_1_1)
& attr(c9473,c9464)
& attr(c9473,c9474)
& attr(c9473,c9475)
& prop(c9473,s__374dafrikanisch_1_1)
& sub(c9473,pr__344sident_1_1)
& sub(c9474,eigenname_1_1)
& val(c9474,nelson_0)
& sub(c9475,familiename_1_1)
& val(c9475,mandela_0)
& attr(c9484,c9485)
& sub(c9484,land_1_1)
& sub(c9485,name_1_1)
& val(c9485,simbabwe_0)
& attr(c9488,c9489)
& attr(c9488,c9490)
& sub(c9488,pr__344sident_1_1)
& sub(c9489,eigenname_1_1)
& val(c9489,robert_0)
& sub(c9490,familiename_1_1)
& val(c9490,mugabe_0)
& pred(c9495,garantiemacht_1_2)
& attr(c9500,c9501)
& sub(c9500,land_1_1)
& sub(c9501,name_1_1)
& val(c9501,usa_0)
& attr(c9505,c9506)
& sub(c9505,land_1_1)
& sub(c9506,name_1_1)
& val(c9506,portugal_0)
& attr(c9518,c9519)
& sub(c9518,land_1_1)
& sub(c9519,name_1_1)
& val(c9519,russland_0)
& tupl_p12(c9590,c9434,c9443,c9456,c9458,c9464,c9488,c9484,c9495,c9500,c9505,c9518)
& assoc(garantiemacht_1_2,b__374rgschaft_1_1)
& sub(garantiemacht_1_2,macht_1_2)
& sort(c9434,d)
& sort(c9434,io)
& card(c9434,int1)
& etype(c9434,int0)
& fact(c9434,real)
& gener(c9434,sp)
& quant(c9434,one)
& refer(c9434,det)
& varia(c9434,con)
& sort(abkommen_1_1,d)
& sort(abkommen_1_1,io)
& card(abkommen_1_1,int1)
& etype(abkommen_1_1,int0)
& fact(abkommen_1_1,real)
& gener(abkommen_1_1,ge)
& quant(abkommen_1_1,one)
& refer(abkommen_1_1,refer_c)
& varia(abkommen_1_1,varia_c)
& sort(c9443,d)
& sort(c9443,io)
& card(c9443,cons(x_constant,cons(int1,nil)))
& etype(c9443,int1)
& fact(c9443,real)
& gener(c9443,sp)
& quant(c9443,mult)
& refer(c9443,indet)
& varia(c9443,varia_c)
& sort(verfechter_1_1,d)
& sort(verfechter_1_1,io)
& card(verfechter_1_1,int1)
& etype(verfechter_1_1,int0)
& fact(verfechter_1_1,real)
& gener(verfechter_1_1,ge)
& quant(verfechter_1_1,one)
& refer(verfechter_1_1,refer_c)
& varia(verfechter_1_1,varia_c)
& sort(c9448,d)
& sort(c9448,io)
& card(c9448,int1)
& etype(c9448,int1)
& fact(c9448,real)
& gener(c9448,sp)
& quant(c9448,one)
& refer(c9448,det)
& varia(c9448,con)
& sort(angolanisch_1_1,nq)
& sort(regierung_1_1,d)
& sort(regierung_1_1,io)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& quant(regierung_1_1,quant_c)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& sort(c9456,d)
& sort(c9456,io)
& card(c9456,int1)
& etype(c9456,int1)
& fact(c9456,real)
& gener(c9456,sp)
& quant(c9456,one)
& refer(c9456,det)
& varia(c9456,con)
& sort(c9457,na)
& card(c9457,int1)
& etype(c9457,int0)
& fact(c9457,real)
& gener(c9457,sp)
& quant(c9457,one)
& refer(c9457,indet)
& varia(c9457,varia_c)
& sort(einrichtung_1_2,d)
& sort(einrichtung_1_2,io)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& quant(einrichtung_1_2,quant_c)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,varia_c)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(unita_0,fe)
& sort(c9458,d)
& card(c9458,cons(x_constant,cons(int1,nil)))
& etype(c9458,int1)
& fact(c9458,real)
& gener(c9458,gener_c)
& quant(c9458,mult)
& refer(c9458,indet)
& varia(c9458,varia_c)
& sort(meuterer_1_1,d)
& card(meuterer_1_1,int1)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& quant(meuterer_1_1,one)
& refer(meuterer_1_1,refer_c)
& varia(meuterer_1_1,varia_c)
& sort(c9464,oa)
& card(c9464,int1)
& etype(c9464,int0)
& fact(c9464,real)
& gener(c9464,sp)
& quant(c9464,one)
& refer(c9464,det)
& varia(c9464,varia_c)
& sort(druck_1_1,oa)
& card(druck_1_1,int1)
& etype(druck_1_1,int0)
& fact(druck_1_1,real)
& gener(druck_1_1,ge)
& quant(druck_1_1,one)
& refer(druck_1_1,refer_c)
& varia(druck_1_1,varia_c)
& sort(c9473,d)
& card(c9473,int1)
& etype(c9473,int0)
& fact(c9473,real)
& gener(c9473,sp)
& quant(c9473,one)
& refer(c9473,det)
& varia(c9473,con)
& sort(c9474,na)
& card(c9474,int1)
& etype(c9474,int0)
& fact(c9474,real)
& gener(c9474,sp)
& quant(c9474,one)
& refer(c9474,indet)
& varia(c9474,varia_c)
& sort(c9475,na)
& card(c9475,int1)
& etype(c9475,int0)
& fact(c9475,real)
& gener(c9475,sp)
& quant(c9475,one)
& refer(c9475,indet)
& varia(c9475,varia_c)
& sort(s__374dafrikanisch_1_1,nq)
& sort(pr__344sident_1_1,d)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& sort(eigenname_1_1,na)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& sort(nelson_0,fe)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(mandela_0,fe)
& sort(c9484,d)
& sort(c9484,io)
& card(c9484,int1)
& etype(c9484,int0)
& fact(c9484,real)
& gener(c9484,sp)
& quant(c9484,one)
& refer(c9484,det)
& varia(c9484,con)
& sort(c9485,na)
& card(c9485,int1)
& etype(c9485,int0)
& fact(c9485,real)
& gener(c9485,sp)
& quant(c9485,one)
& refer(c9485,indet)
& varia(c9485,varia_c)
& sort(land_1_1,d)
& sort(land_1_1,io)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& quant(land_1_1,one)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& sort(simbabwe_0,fe)
& sort(c9488,d)
& card(c9488,int1)
& etype(c9488,int0)
& fact(c9488,real)
& gener(c9488,sp)
& quant(c9488,one)
& refer(c9488,det)
& varia(c9488,con)
& sort(c9489,na)
& card(c9489,int1)
& etype(c9489,int0)
& fact(c9489,real)
& gener(c9489,sp)
& quant(c9489,one)
& refer(c9489,indet)
& varia(c9489,varia_c)
& sort(c9490,na)
& card(c9490,int1)
& etype(c9490,int0)
& fact(c9490,real)
& gener(c9490,sp)
& quant(c9490,one)
& refer(c9490,indet)
& varia(c9490,varia_c)
& sort(robert_0,fe)
& sort(mugabe_0,fe)
& sort(c9495,d)
& sort(c9495,io)
& card(c9495,int3)
& etype(c9495,int1)
& fact(c9495,real)
& gener(c9495,sp)
& quant(c9495,nfquant)
& refer(c9495,det)
& varia(c9495,con)
& sort(garantiemacht_1_2,d)
& sort(garantiemacht_1_2,io)
& card(garantiemacht_1_2,int1)
& etype(garantiemacht_1_2,int0)
& fact(garantiemacht_1_2,real)
& gener(garantiemacht_1_2,ge)
& quant(garantiemacht_1_2,one)
& refer(garantiemacht_1_2,refer_c)
& varia(garantiemacht_1_2,varia_c)
& sort(c9500,d)
& sort(c9500,io)
& card(c9500,int1)
& etype(c9500,int0)
& fact(c9500,real)
& gener(c9500,sp)
& quant(c9500,one)
& refer(c9500,det)
& varia(c9500,con)
& sort(c9501,na)
& card(c9501,int1)
& etype(c9501,int0)
& fact(c9501,real)
& gener(c9501,sp)
& quant(c9501,one)
& refer(c9501,indet)
& varia(c9501,varia_c)
& sort(usa_0,fe)
& sort(c9505,d)
& sort(c9505,io)
& card(c9505,int1)
& etype(c9505,int0)
& fact(c9505,real)
& gener(c9505,sp)
& quant(c9505,one)
& refer(c9505,det)
& varia(c9505,con)
& sort(c9506,na)
& card(c9506,int1)
& etype(c9506,int0)
& fact(c9506,real)
& gener(c9506,sp)
& quant(c9506,one)
& refer(c9506,indet)
& varia(c9506,varia_c)
& sort(portugal_0,fe)
& sort(c9518,d)
& sort(c9518,io)
& card(c9518,int1)
& etype(c9518,int0)
& fact(c9518,real)
& gener(c9518,sp)
& quant(c9518,one)
& refer(c9518,det)
& varia(c9518,con)
& sort(c9519,na)
& card(c9519,int1)
& etype(c9519,int0)
& fact(c9519,real)
& gener(c9519,sp)
& quant(c9519,one)
& refer(c9519,indet)
& varia(c9519,varia_c)
& sort(russland_0,fe)
& sort(c9590,ent)
& card(c9590,card_c)
& etype(c9590,etype_c)
& fact(c9590,real)
& gener(c9590,gener_c)
& quant(c9590,quant_c)
& refer(c9590,refer_c)
& varia(c9590,varia_c)
& sort(b__374rgschaft_1_1,io)
& card(b__374rgschaft_1_1,int1)
& etype(b__374rgschaft_1_1,int0)
& fact(b__374rgschaft_1_1,real)
& gener(b__374rgschaft_1_1,ge)
& quant(b__374rgschaft_1_1,one)
& refer(b__374rgschaft_1_1,refer_c)
& varia(b__374rgschaft_1_1,varia_c)
& sort(macht_1_2,d)
& sort(macht_1_2,io)
& card(macht_1_2,int1)
& etype(macht_1_2,int0)
& fact(macht_1_2,real)
& gener(macht_1_2,ge)
& quant(macht_1_2,one)
& refer(macht_1_2,refer_c)
& varia(macht_1_2,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_news_1824) ).
fof(f10191,plain,
( sub(c9434,abkommen_1_1)
& pred(c9443,verfechter_1_1)
& attch(c9448,c9443)
& prop(c9448,angolanisch_1_1)
& sub(c9448,regierung_1_1)
& attr(c9456,c9457)
& sub(c9456,einrichtung_1_2)
& sub(c9457,name_1_1)
& val(c9457,unita_0)
& pred(c9458,meuterer_1_1)
& sub(c9464,druck_1_1)
& attr(c9473,c9464)
& attr(c9473,c9474)
& attr(c9473,c9475)
& prop(c9473,s__374dafrikanisch_1_1)
& sub(c9473,pr__344sident_1_1)
& sub(c9474,eigenname_1_1)
& val(c9474,nelson_0)
& sub(c9475,familiename_1_1)
& val(c9475,mandela_0)
& attr(c9484,c9485)
& sub(c9484,land_1_1)
& sub(c9485,name_1_1)
& val(c9485,simbabwe_0)
& attr(c9488,c9489)
& attr(c9488,c9490)
& sub(c9488,pr__344sident_1_1)
& sub(c9489,eigenname_1_1)
& val(c9489,robert_0)
& sub(c9490,familiename_1_1)
& val(c9490,mugabe_0)
& pred(c9495,garantiemacht_1_2)
& attr(c9500,c9501)
& sub(c9500,land_1_1)
& sub(c9501,name_1_1)
& val(c9501,usa_0)
& attr(c9505,c9506)
& sub(c9505,land_1_1)
& sub(c9506,name_1_1)
& val(c9506,portugal_0)
& attr(c9518,c9519)
& sub(c9518,land_1_1)
& sub(c9519,name_1_1)
& val(c9519,russland_0)
& assoc(garantiemacht_1_2,b__374rgschaft_1_1)
& sub(garantiemacht_1_2,macht_1_2)
& sort(c9434,d)
& sort(c9434,io)
& card(c9434,int1)
& etype(c9434,int0)
& fact(c9434,real)
& gener(c9434,sp)
& quant(c9434,one)
& refer(c9434,det)
& varia(c9434,con)
& sort(abkommen_1_1,d)
& sort(abkommen_1_1,io)
& card(abkommen_1_1,int1)
& etype(abkommen_1_1,int0)
& fact(abkommen_1_1,real)
& gener(abkommen_1_1,ge)
& quant(abkommen_1_1,one)
& refer(abkommen_1_1,refer_c)
& varia(abkommen_1_1,varia_c)
& sort(c9443,d)
& sort(c9443,io)
& card(c9443,cons(x_constant,cons(int1,nil)))
& etype(c9443,int1)
& fact(c9443,real)
& gener(c9443,sp)
& quant(c9443,mult)
& refer(c9443,indet)
& varia(c9443,varia_c)
& sort(verfechter_1_1,d)
& sort(verfechter_1_1,io)
& card(verfechter_1_1,int1)
& etype(verfechter_1_1,int0)
& fact(verfechter_1_1,real)
& gener(verfechter_1_1,ge)
& quant(verfechter_1_1,one)
& refer(verfechter_1_1,refer_c)
& varia(verfechter_1_1,varia_c)
& sort(c9448,d)
& sort(c9448,io)
& card(c9448,int1)
& etype(c9448,int1)
& fact(c9448,real)
& gener(c9448,sp)
& quant(c9448,one)
& refer(c9448,det)
& varia(c9448,con)
& sort(angolanisch_1_1,nq)
& sort(regierung_1_1,d)
& sort(regierung_1_1,io)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& quant(regierung_1_1,quant_c)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& sort(c9456,d)
& sort(c9456,io)
& card(c9456,int1)
& etype(c9456,int1)
& fact(c9456,real)
& gener(c9456,sp)
& quant(c9456,one)
& refer(c9456,det)
& varia(c9456,con)
& sort(c9457,na)
& card(c9457,int1)
& etype(c9457,int0)
& fact(c9457,real)
& gener(c9457,sp)
& quant(c9457,one)
& refer(c9457,indet)
& varia(c9457,varia_c)
& sort(einrichtung_1_2,d)
& sort(einrichtung_1_2,io)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& quant(einrichtung_1_2,quant_c)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,varia_c)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(unita_0,fe)
& sort(c9458,d)
& card(c9458,cons(x_constant,cons(int1,nil)))
& etype(c9458,int1)
& fact(c9458,real)
& gener(c9458,gener_c)
& quant(c9458,mult)
& refer(c9458,indet)
& varia(c9458,varia_c)
& sort(meuterer_1_1,d)
& card(meuterer_1_1,int1)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& quant(meuterer_1_1,one)
& refer(meuterer_1_1,refer_c)
& varia(meuterer_1_1,varia_c)
& sort(c9464,oa)
& card(c9464,int1)
& etype(c9464,int0)
& fact(c9464,real)
& gener(c9464,sp)
& quant(c9464,one)
& refer(c9464,det)
& varia(c9464,varia_c)
& sort(druck_1_1,oa)
& card(druck_1_1,int1)
& etype(druck_1_1,int0)
& fact(druck_1_1,real)
& gener(druck_1_1,ge)
& quant(druck_1_1,one)
& refer(druck_1_1,refer_c)
& varia(druck_1_1,varia_c)
& sort(c9473,d)
& card(c9473,int1)
& etype(c9473,int0)
& fact(c9473,real)
& gener(c9473,sp)
& quant(c9473,one)
& refer(c9473,det)
& varia(c9473,con)
& sort(c9474,na)
& card(c9474,int1)
& etype(c9474,int0)
& fact(c9474,real)
& gener(c9474,sp)
& quant(c9474,one)
& refer(c9474,indet)
& varia(c9474,varia_c)
& sort(c9475,na)
& card(c9475,int1)
& etype(c9475,int0)
& fact(c9475,real)
& gener(c9475,sp)
& quant(c9475,one)
& refer(c9475,indet)
& varia(c9475,varia_c)
& sort(s__374dafrikanisch_1_1,nq)
& sort(pr__344sident_1_1,d)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& sort(eigenname_1_1,na)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& sort(nelson_0,fe)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(mandela_0,fe)
& sort(c9484,d)
& sort(c9484,io)
& card(c9484,int1)
& etype(c9484,int0)
& fact(c9484,real)
& gener(c9484,sp)
& quant(c9484,one)
& refer(c9484,det)
& varia(c9484,con)
& sort(c9485,na)
& card(c9485,int1)
& etype(c9485,int0)
& fact(c9485,real)
& gener(c9485,sp)
& quant(c9485,one)
& refer(c9485,indet)
& varia(c9485,varia_c)
& sort(land_1_1,d)
& sort(land_1_1,io)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& quant(land_1_1,one)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& sort(simbabwe_0,fe)
& sort(c9488,d)
& card(c9488,int1)
& etype(c9488,int0)
& fact(c9488,real)
& gener(c9488,sp)
& quant(c9488,one)
& refer(c9488,det)
& varia(c9488,con)
& sort(c9489,na)
& card(c9489,int1)
& etype(c9489,int0)
& fact(c9489,real)
& gener(c9489,sp)
& quant(c9489,one)
& refer(c9489,indet)
& varia(c9489,varia_c)
& sort(c9490,na)
& card(c9490,int1)
& etype(c9490,int0)
& fact(c9490,real)
& gener(c9490,sp)
& quant(c9490,one)
& refer(c9490,indet)
& varia(c9490,varia_c)
& sort(robert_0,fe)
& sort(mugabe_0,fe)
& sort(c9495,d)
& sort(c9495,io)
& card(c9495,int3)
& etype(c9495,int1)
& fact(c9495,real)
& gener(c9495,sp)
& quant(c9495,nfquant)
& refer(c9495,det)
& varia(c9495,con)
& sort(garantiemacht_1_2,d)
& sort(garantiemacht_1_2,io)
& card(garantiemacht_1_2,int1)
& etype(garantiemacht_1_2,int0)
& fact(garantiemacht_1_2,real)
& gener(garantiemacht_1_2,ge)
& quant(garantiemacht_1_2,one)
& refer(garantiemacht_1_2,refer_c)
& varia(garantiemacht_1_2,varia_c)
& sort(c9500,d)
& sort(c9500,io)
& card(c9500,int1)
& etype(c9500,int0)
& fact(c9500,real)
& gener(c9500,sp)
& quant(c9500,one)
& refer(c9500,det)
& varia(c9500,con)
& sort(c9501,na)
& card(c9501,int1)
& etype(c9501,int0)
& fact(c9501,real)
& gener(c9501,sp)
& quant(c9501,one)
& refer(c9501,indet)
& varia(c9501,varia_c)
& sort(usa_0,fe)
& sort(c9505,d)
& sort(c9505,io)
& card(c9505,int1)
& etype(c9505,int0)
& fact(c9505,real)
& gener(c9505,sp)
& quant(c9505,one)
& refer(c9505,det)
& varia(c9505,con)
& sort(c9506,na)
& card(c9506,int1)
& etype(c9506,int0)
& fact(c9506,real)
& gener(c9506,sp)
& quant(c9506,one)
& refer(c9506,indet)
& varia(c9506,varia_c)
& sort(portugal_0,fe)
& sort(c9518,d)
& sort(c9518,io)
& card(c9518,int1)
& etype(c9518,int0)
& fact(c9518,real)
& gener(c9518,sp)
& quant(c9518,one)
& refer(c9518,det)
& varia(c9518,con)
& sort(c9519,na)
& card(c9519,int1)
& etype(c9519,int0)
& fact(c9519,real)
& gener(c9519,sp)
& quant(c9519,one)
& refer(c9519,indet)
& varia(c9519,varia_c)
& sort(russland_0,fe)
& sort(c9590,ent)
& card(c9590,card_c)
& etype(c9590,etype_c)
& fact(c9590,real)
& gener(c9590,gener_c)
& quant(c9590,quant_c)
& refer(c9590,refer_c)
& varia(c9590,varia_c)
& sort(b__374rgschaft_1_1,io)
& card(b__374rgschaft_1_1,int1)
& etype(b__374rgschaft_1_1,int0)
& fact(b__374rgschaft_1_1,real)
& gener(b__374rgschaft_1_1,ge)
& quant(b__374rgschaft_1_1,one)
& refer(b__374rgschaft_1_1,refer_c)
& varia(b__374rgschaft_1_1,varia_c)
& sort(macht_1_2,d)
& sort(macht_1_2,io)
& card(macht_1_2,int1)
& etype(macht_1_2,int0)
& fact(macht_1_2,real)
& gener(macht_1_2,ge)
& quant(macht_1_2,one)
& refer(macht_1_2,refer_c)
& varia(macht_1_2,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10206,plain,
( sub(c9434,abkommen_1_1)
& pred(c9443,verfechter_1_1)
& attch(c9448,c9443)
& prop(c9448,angolanisch_1_1)
& sub(c9448,regierung_1_1)
& attr(c9456,c9457)
& sub(c9456,einrichtung_1_2)
& sub(c9457,name_1_1)
& val(c9457,unita_0)
& pred(c9458,meuterer_1_1)
& sub(c9464,druck_1_1)
& attr(c9473,c9464)
& attr(c9473,c9474)
& attr(c9473,c9475)
& prop(c9473,s__374dafrikanisch_1_1)
& sub(c9473,pr__344sident_1_1)
& sub(c9474,eigenname_1_1)
& val(c9474,nelson_0)
& sub(c9475,familiename_1_1)
& val(c9475,mandela_0)
& attr(c9484,c9485)
& sub(c9484,land_1_1)
& sub(c9485,name_1_1)
& val(c9485,simbabwe_0)
& attr(c9488,c9489)
& attr(c9488,c9490)
& sub(c9488,pr__344sident_1_1)
& sub(c9489,eigenname_1_1)
& val(c9489,robert_0)
& sub(c9490,familiename_1_1)
& val(c9490,mugabe_0)
& pred(c9495,garantiemacht_1_2)
& attr(c9500,c9501)
& sub(c9500,land_1_1)
& sub(c9501,name_1_1)
& val(c9501,usa_0)
& attr(c9505,c9506)
& sub(c9505,land_1_1)
& sub(c9506,name_1_1)
& val(c9506,portugal_0)
& attr(c9518,c9519)
& sub(c9518,land_1_1)
& sub(c9519,name_1_1)
& val(c9519,russland_0)
& assoc(garantiemacht_1_2,b__374rgschaft_1_1)
& sub(garantiemacht_1_2,macht_1_2)
& card(c9434,int1)
& etype(c9434,int0)
& fact(c9434,real)
& gener(c9434,sp)
& quant(c9434,one)
& refer(c9434,det)
& varia(c9434,con)
& card(abkommen_1_1,int1)
& etype(abkommen_1_1,int0)
& fact(abkommen_1_1,real)
& gener(abkommen_1_1,ge)
& quant(abkommen_1_1,one)
& refer(abkommen_1_1,refer_c)
& varia(abkommen_1_1,varia_c)
& card(c9443,cons(x_constant,cons(int1,nil)))
& etype(c9443,int1)
& fact(c9443,real)
& gener(c9443,sp)
& quant(c9443,mult)
& refer(c9443,indet)
& varia(c9443,varia_c)
& card(verfechter_1_1,int1)
& etype(verfechter_1_1,int0)
& fact(verfechter_1_1,real)
& gener(verfechter_1_1,ge)
& quant(verfechter_1_1,one)
& refer(verfechter_1_1,refer_c)
& varia(verfechter_1_1,varia_c)
& card(c9448,int1)
& etype(c9448,int1)
& fact(c9448,real)
& gener(c9448,sp)
& quant(c9448,one)
& refer(c9448,det)
& varia(c9448,con)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& quant(regierung_1_1,quant_c)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& card(c9456,int1)
& etype(c9456,int1)
& fact(c9456,real)
& gener(c9456,sp)
& quant(c9456,one)
& refer(c9456,det)
& varia(c9456,con)
& card(c9457,int1)
& etype(c9457,int0)
& fact(c9457,real)
& gener(c9457,sp)
& quant(c9457,one)
& refer(c9457,indet)
& varia(c9457,varia_c)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& quant(einrichtung_1_2,quant_c)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,varia_c)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& card(c9458,cons(x_constant,cons(int1,nil)))
& etype(c9458,int1)
& fact(c9458,real)
& gener(c9458,gener_c)
& quant(c9458,mult)
& refer(c9458,indet)
& varia(c9458,varia_c)
& card(meuterer_1_1,int1)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& quant(meuterer_1_1,one)
& refer(meuterer_1_1,refer_c)
& varia(meuterer_1_1,varia_c)
& card(c9464,int1)
& etype(c9464,int0)
& fact(c9464,real)
& gener(c9464,sp)
& quant(c9464,one)
& refer(c9464,det)
& varia(c9464,varia_c)
& card(druck_1_1,int1)
& etype(druck_1_1,int0)
& fact(druck_1_1,real)
& gener(druck_1_1,ge)
& quant(druck_1_1,one)
& refer(druck_1_1,refer_c)
& varia(druck_1_1,varia_c)
& card(c9473,int1)
& etype(c9473,int0)
& fact(c9473,real)
& gener(c9473,sp)
& quant(c9473,one)
& refer(c9473,det)
& varia(c9473,con)
& card(c9474,int1)
& etype(c9474,int0)
& fact(c9474,real)
& gener(c9474,sp)
& quant(c9474,one)
& refer(c9474,indet)
& varia(c9474,varia_c)
& card(c9475,int1)
& etype(c9475,int0)
& fact(c9475,real)
& gener(c9475,sp)
& quant(c9475,one)
& refer(c9475,indet)
& varia(c9475,varia_c)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& card(c9484,int1)
& etype(c9484,int0)
& fact(c9484,real)
& gener(c9484,sp)
& quant(c9484,one)
& refer(c9484,det)
& varia(c9484,con)
& card(c9485,int1)
& etype(c9485,int0)
& fact(c9485,real)
& gener(c9485,sp)
& quant(c9485,one)
& refer(c9485,indet)
& varia(c9485,varia_c)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& quant(land_1_1,one)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& card(c9488,int1)
& etype(c9488,int0)
& fact(c9488,real)
& gener(c9488,sp)
& quant(c9488,one)
& refer(c9488,det)
& varia(c9488,con)
& card(c9489,int1)
& etype(c9489,int0)
& fact(c9489,real)
& gener(c9489,sp)
& quant(c9489,one)
& refer(c9489,indet)
& varia(c9489,varia_c)
& card(c9490,int1)
& etype(c9490,int0)
& fact(c9490,real)
& gener(c9490,sp)
& quant(c9490,one)
& refer(c9490,indet)
& varia(c9490,varia_c)
& card(c9495,int3)
& etype(c9495,int1)
& fact(c9495,real)
& gener(c9495,sp)
& quant(c9495,nfquant)
& refer(c9495,det)
& varia(c9495,con)
& card(garantiemacht_1_2,int1)
& etype(garantiemacht_1_2,int0)
& fact(garantiemacht_1_2,real)
& gener(garantiemacht_1_2,ge)
& quant(garantiemacht_1_2,one)
& refer(garantiemacht_1_2,refer_c)
& varia(garantiemacht_1_2,varia_c)
& card(c9500,int1)
& etype(c9500,int0)
& fact(c9500,real)
& gener(c9500,sp)
& quant(c9500,one)
& refer(c9500,det)
& varia(c9500,con)
& card(c9501,int1)
& etype(c9501,int0)
& fact(c9501,real)
& gener(c9501,sp)
& quant(c9501,one)
& refer(c9501,indet)
& varia(c9501,varia_c)
& card(c9505,int1)
& etype(c9505,int0)
& fact(c9505,real)
& gener(c9505,sp)
& quant(c9505,one)
& refer(c9505,det)
& varia(c9505,con)
& card(c9506,int1)
& etype(c9506,int0)
& fact(c9506,real)
& gener(c9506,sp)
& quant(c9506,one)
& refer(c9506,indet)
& varia(c9506,varia_c)
& card(c9518,int1)
& etype(c9518,int0)
& fact(c9518,real)
& gener(c9518,sp)
& quant(c9518,one)
& refer(c9518,det)
& varia(c9518,con)
& card(c9519,int1)
& etype(c9519,int0)
& fact(c9519,real)
& gener(c9519,sp)
& quant(c9519,one)
& refer(c9519,indet)
& varia(c9519,varia_c)
& card(c9590,card_c)
& etype(c9590,etype_c)
& fact(c9590,real)
& gener(c9590,gener_c)
& quant(c9590,quant_c)
& refer(c9590,refer_c)
& varia(c9590,varia_c)
& card(b__374rgschaft_1_1,int1)
& etype(b__374rgschaft_1_1,int0)
& fact(b__374rgschaft_1_1,real)
& gener(b__374rgschaft_1_1,ge)
& quant(b__374rgschaft_1_1,one)
& refer(b__374rgschaft_1_1,refer_c)
& varia(b__374rgschaft_1_1,varia_c)
& card(macht_1_2,int1)
& etype(macht_1_2,int0)
& fact(macht_1_2,real)
& gener(macht_1_2,ge)
& quant(macht_1_2,one)
& refer(macht_1_2,refer_c)
& varia(macht_1_2,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10209,plain,
( sub(c9434,abkommen_1_1)
& pred(c9443,verfechter_1_1)
& attch(c9448,c9443)
& prop(c9448,angolanisch_1_1)
& sub(c9448,regierung_1_1)
& attr(c9456,c9457)
& sub(c9456,einrichtung_1_2)
& sub(c9457,name_1_1)
& val(c9457,unita_0)
& pred(c9458,meuterer_1_1)
& sub(c9464,druck_1_1)
& attr(c9473,c9464)
& attr(c9473,c9474)
& attr(c9473,c9475)
& prop(c9473,s__374dafrikanisch_1_1)
& sub(c9473,pr__344sident_1_1)
& sub(c9474,eigenname_1_1)
& val(c9474,nelson_0)
& sub(c9475,familiename_1_1)
& val(c9475,mandela_0)
& attr(c9484,c9485)
& sub(c9484,land_1_1)
& sub(c9485,name_1_1)
& val(c9485,simbabwe_0)
& attr(c9488,c9489)
& attr(c9488,c9490)
& sub(c9488,pr__344sident_1_1)
& sub(c9489,eigenname_1_1)
& val(c9489,robert_0)
& sub(c9490,familiename_1_1)
& val(c9490,mugabe_0)
& pred(c9495,garantiemacht_1_2)
& attr(c9500,c9501)
& sub(c9500,land_1_1)
& sub(c9501,name_1_1)
& val(c9501,usa_0)
& attr(c9505,c9506)
& sub(c9505,land_1_1)
& sub(c9506,name_1_1)
& val(c9506,portugal_0)
& attr(c9518,c9519)
& sub(c9518,land_1_1)
& sub(c9519,name_1_1)
& val(c9519,russland_0)
& assoc(garantiemacht_1_2,b__374rgschaft_1_1)
& sub(garantiemacht_1_2,macht_1_2)
& card(c9434,int1)
& etype(c9434,int0)
& fact(c9434,real)
& gener(c9434,sp)
& refer(c9434,det)
& varia(c9434,con)
& card(abkommen_1_1,int1)
& etype(abkommen_1_1,int0)
& fact(abkommen_1_1,real)
& gener(abkommen_1_1,ge)
& refer(abkommen_1_1,refer_c)
& varia(abkommen_1_1,varia_c)
& card(c9443,cons(x_constant,cons(int1,nil)))
& etype(c9443,int1)
& fact(c9443,real)
& gener(c9443,sp)
& refer(c9443,indet)
& varia(c9443,varia_c)
& card(verfechter_1_1,int1)
& etype(verfechter_1_1,int0)
& fact(verfechter_1_1,real)
& gener(verfechter_1_1,ge)
& refer(verfechter_1_1,refer_c)
& varia(verfechter_1_1,varia_c)
& card(c9448,int1)
& etype(c9448,int1)
& fact(c9448,real)
& gener(c9448,sp)
& refer(c9448,det)
& varia(c9448,con)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& card(c9456,int1)
& etype(c9456,int1)
& fact(c9456,real)
& gener(c9456,sp)
& refer(c9456,det)
& varia(c9456,con)
& card(c9457,int1)
& etype(c9457,int0)
& fact(c9457,real)
& gener(c9457,sp)
& refer(c9457,indet)
& varia(c9457,varia_c)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,varia_c)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& card(c9458,cons(x_constant,cons(int1,nil)))
& etype(c9458,int1)
& fact(c9458,real)
& gener(c9458,gener_c)
& refer(c9458,indet)
& varia(c9458,varia_c)
& card(meuterer_1_1,int1)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& refer(meuterer_1_1,refer_c)
& varia(meuterer_1_1,varia_c)
& card(c9464,int1)
& etype(c9464,int0)
& fact(c9464,real)
& gener(c9464,sp)
& refer(c9464,det)
& varia(c9464,varia_c)
& card(druck_1_1,int1)
& etype(druck_1_1,int0)
& fact(druck_1_1,real)
& gener(druck_1_1,ge)
& refer(druck_1_1,refer_c)
& varia(druck_1_1,varia_c)
& card(c9473,int1)
& etype(c9473,int0)
& fact(c9473,real)
& gener(c9473,sp)
& refer(c9473,det)
& varia(c9473,con)
& card(c9474,int1)
& etype(c9474,int0)
& fact(c9474,real)
& gener(c9474,sp)
& refer(c9474,indet)
& varia(c9474,varia_c)
& card(c9475,int1)
& etype(c9475,int0)
& fact(c9475,real)
& gener(c9475,sp)
& refer(c9475,indet)
& varia(c9475,varia_c)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& card(c9484,int1)
& etype(c9484,int0)
& fact(c9484,real)
& gener(c9484,sp)
& refer(c9484,det)
& varia(c9484,con)
& card(c9485,int1)
& etype(c9485,int0)
& fact(c9485,real)
& gener(c9485,sp)
& refer(c9485,indet)
& varia(c9485,varia_c)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& card(c9488,int1)
& etype(c9488,int0)
& fact(c9488,real)
& gener(c9488,sp)
& refer(c9488,det)
& varia(c9488,con)
& card(c9489,int1)
& etype(c9489,int0)
& fact(c9489,real)
& gener(c9489,sp)
& refer(c9489,indet)
& varia(c9489,varia_c)
& card(c9490,int1)
& etype(c9490,int0)
& fact(c9490,real)
& gener(c9490,sp)
& refer(c9490,indet)
& varia(c9490,varia_c)
& card(c9495,int3)
& etype(c9495,int1)
& fact(c9495,real)
& gener(c9495,sp)
& refer(c9495,det)
& varia(c9495,con)
& card(garantiemacht_1_2,int1)
& etype(garantiemacht_1_2,int0)
& fact(garantiemacht_1_2,real)
& gener(garantiemacht_1_2,ge)
& refer(garantiemacht_1_2,refer_c)
& varia(garantiemacht_1_2,varia_c)
& card(c9500,int1)
& etype(c9500,int0)
& fact(c9500,real)
& gener(c9500,sp)
& refer(c9500,det)
& varia(c9500,con)
& card(c9501,int1)
& etype(c9501,int0)
& fact(c9501,real)
& gener(c9501,sp)
& refer(c9501,indet)
& varia(c9501,varia_c)
& card(c9505,int1)
& etype(c9505,int0)
& fact(c9505,real)
& gener(c9505,sp)
& refer(c9505,det)
& varia(c9505,con)
& card(c9506,int1)
& etype(c9506,int0)
& fact(c9506,real)
& gener(c9506,sp)
& refer(c9506,indet)
& varia(c9506,varia_c)
& card(c9518,int1)
& etype(c9518,int0)
& fact(c9518,real)
& gener(c9518,sp)
& refer(c9518,det)
& varia(c9518,con)
& card(c9519,int1)
& etype(c9519,int0)
& fact(c9519,real)
& gener(c9519,sp)
& refer(c9519,indet)
& varia(c9519,varia_c)
& card(c9590,card_c)
& etype(c9590,etype_c)
& fact(c9590,real)
& gener(c9590,gener_c)
& refer(c9590,refer_c)
& varia(c9590,varia_c)
& card(b__374rgschaft_1_1,int1)
& etype(b__374rgschaft_1_1,int0)
& fact(b__374rgschaft_1_1,real)
& gener(b__374rgschaft_1_1,ge)
& refer(b__374rgschaft_1_1,refer_c)
& varia(b__374rgschaft_1_1,varia_c)
& card(macht_1_2,int1)
& etype(macht_1_2,int0)
& fact(macht_1_2,real)
& gener(macht_1_2,ge)
& refer(macht_1_2,refer_c)
& varia(macht_1_2,varia_c) ),
inference(pure_predicate_removal,[],[f10206]) ).
fof(f10212,plain,
( sub(c9434,abkommen_1_1)
& pred(c9443,verfechter_1_1)
& attch(c9448,c9443)
& prop(c9448,angolanisch_1_1)
& sub(c9448,regierung_1_1)
& attr(c9456,c9457)
& sub(c9456,einrichtung_1_2)
& sub(c9457,name_1_1)
& val(c9457,unita_0)
& pred(c9458,meuterer_1_1)
& sub(c9464,druck_1_1)
& attr(c9473,c9464)
& attr(c9473,c9474)
& attr(c9473,c9475)
& prop(c9473,s__374dafrikanisch_1_1)
& sub(c9473,pr__344sident_1_1)
& sub(c9474,eigenname_1_1)
& val(c9474,nelson_0)
& sub(c9475,familiename_1_1)
& val(c9475,mandela_0)
& attr(c9484,c9485)
& sub(c9484,land_1_1)
& sub(c9485,name_1_1)
& val(c9485,simbabwe_0)
& attr(c9488,c9489)
& attr(c9488,c9490)
& sub(c9488,pr__344sident_1_1)
& sub(c9489,eigenname_1_1)
& val(c9489,robert_0)
& sub(c9490,familiename_1_1)
& val(c9490,mugabe_0)
& pred(c9495,garantiemacht_1_2)
& attr(c9500,c9501)
& sub(c9500,land_1_1)
& sub(c9501,name_1_1)
& val(c9501,usa_0)
& attr(c9505,c9506)
& sub(c9505,land_1_1)
& sub(c9506,name_1_1)
& val(c9506,portugal_0)
& attr(c9518,c9519)
& sub(c9518,land_1_1)
& sub(c9519,name_1_1)
& val(c9519,russland_0)
& assoc(garantiemacht_1_2,b__374rgschaft_1_1)
& sub(garantiemacht_1_2,macht_1_2)
& etype(c9434,int0)
& fact(c9434,real)
& gener(c9434,sp)
& refer(c9434,det)
& varia(c9434,con)
& etype(abkommen_1_1,int0)
& fact(abkommen_1_1,real)
& gener(abkommen_1_1,ge)
& refer(abkommen_1_1,refer_c)
& varia(abkommen_1_1,varia_c)
& etype(c9443,int1)
& fact(c9443,real)
& gener(c9443,sp)
& refer(c9443,indet)
& varia(c9443,varia_c)
& etype(verfechter_1_1,int0)
& fact(verfechter_1_1,real)
& gener(verfechter_1_1,ge)
& refer(verfechter_1_1,refer_c)
& varia(verfechter_1_1,varia_c)
& etype(c9448,int1)
& fact(c9448,real)
& gener(c9448,sp)
& refer(c9448,det)
& varia(c9448,con)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& etype(c9456,int1)
& fact(c9456,real)
& gener(c9456,sp)
& refer(c9456,det)
& varia(c9456,con)
& etype(c9457,int0)
& fact(c9457,real)
& gener(c9457,sp)
& refer(c9457,indet)
& varia(c9457,varia_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& etype(c9458,int1)
& fact(c9458,real)
& gener(c9458,gener_c)
& refer(c9458,indet)
& varia(c9458,varia_c)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& refer(meuterer_1_1,refer_c)
& varia(meuterer_1_1,varia_c)
& etype(c9464,int0)
& fact(c9464,real)
& gener(c9464,sp)
& refer(c9464,det)
& varia(c9464,varia_c)
& etype(druck_1_1,int0)
& fact(druck_1_1,real)
& gener(druck_1_1,ge)
& refer(druck_1_1,refer_c)
& varia(druck_1_1,varia_c)
& etype(c9473,int0)
& fact(c9473,real)
& gener(c9473,sp)
& refer(c9473,det)
& varia(c9473,con)
& etype(c9474,int0)
& fact(c9474,real)
& gener(c9474,sp)
& refer(c9474,indet)
& varia(c9474,varia_c)
& etype(c9475,int0)
& fact(c9475,real)
& gener(c9475,sp)
& refer(c9475,indet)
& varia(c9475,varia_c)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& etype(c9484,int0)
& fact(c9484,real)
& gener(c9484,sp)
& refer(c9484,det)
& varia(c9484,con)
& etype(c9485,int0)
& fact(c9485,real)
& gener(c9485,sp)
& refer(c9485,indet)
& varia(c9485,varia_c)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& etype(c9488,int0)
& fact(c9488,real)
& gener(c9488,sp)
& refer(c9488,det)
& varia(c9488,con)
& etype(c9489,int0)
& fact(c9489,real)
& gener(c9489,sp)
& refer(c9489,indet)
& varia(c9489,varia_c)
& etype(c9490,int0)
& fact(c9490,real)
& gener(c9490,sp)
& refer(c9490,indet)
& varia(c9490,varia_c)
& etype(c9495,int1)
& fact(c9495,real)
& gener(c9495,sp)
& refer(c9495,det)
& varia(c9495,con)
& etype(garantiemacht_1_2,int0)
& fact(garantiemacht_1_2,real)
& gener(garantiemacht_1_2,ge)
& refer(garantiemacht_1_2,refer_c)
& varia(garantiemacht_1_2,varia_c)
& etype(c9500,int0)
& fact(c9500,real)
& gener(c9500,sp)
& refer(c9500,det)
& varia(c9500,con)
& etype(c9501,int0)
& fact(c9501,real)
& gener(c9501,sp)
& refer(c9501,indet)
& varia(c9501,varia_c)
& etype(c9505,int0)
& fact(c9505,real)
& gener(c9505,sp)
& refer(c9505,det)
& varia(c9505,con)
& etype(c9506,int0)
& fact(c9506,real)
& gener(c9506,sp)
& refer(c9506,indet)
& varia(c9506,varia_c)
& etype(c9518,int0)
& fact(c9518,real)
& gener(c9518,sp)
& refer(c9518,det)
& varia(c9518,con)
& etype(c9519,int0)
& fact(c9519,real)
& gener(c9519,sp)
& refer(c9519,indet)
& varia(c9519,varia_c)
& etype(c9590,etype_c)
& fact(c9590,real)
& gener(c9590,gener_c)
& refer(c9590,refer_c)
& varia(c9590,varia_c)
& etype(b__374rgschaft_1_1,int0)
& fact(b__374rgschaft_1_1,real)
& gener(b__374rgschaft_1_1,ge)
& refer(b__374rgschaft_1_1,refer_c)
& varia(b__374rgschaft_1_1,varia_c)
& etype(macht_1_2,int0)
& fact(macht_1_2,real)
& gener(macht_1_2,ge)
& refer(macht_1_2,refer_c)
& varia(macht_1_2,varia_c) ),
inference(pure_predicate_removal,[],[f10209]) ).
fof(f10215,plain,
( sub(c9434,abkommen_1_1)
& pred(c9443,verfechter_1_1)
& attch(c9448,c9443)
& prop(c9448,angolanisch_1_1)
& sub(c9448,regierung_1_1)
& attr(c9456,c9457)
& sub(c9456,einrichtung_1_2)
& sub(c9457,name_1_1)
& val(c9457,unita_0)
& pred(c9458,meuterer_1_1)
& sub(c9464,druck_1_1)
& attr(c9473,c9464)
& attr(c9473,c9474)
& attr(c9473,c9475)
& prop(c9473,s__374dafrikanisch_1_1)
& sub(c9473,pr__344sident_1_1)
& sub(c9474,eigenname_1_1)
& val(c9474,nelson_0)
& sub(c9475,familiename_1_1)
& val(c9475,mandela_0)
& attr(c9484,c9485)
& sub(c9484,land_1_1)
& sub(c9485,name_1_1)
& val(c9485,simbabwe_0)
& attr(c9488,c9489)
& attr(c9488,c9490)
& sub(c9488,pr__344sident_1_1)
& sub(c9489,eigenname_1_1)
& val(c9489,robert_0)
& sub(c9490,familiename_1_1)
& val(c9490,mugabe_0)
& pred(c9495,garantiemacht_1_2)
& attr(c9500,c9501)
& sub(c9500,land_1_1)
& sub(c9501,name_1_1)
& val(c9501,usa_0)
& attr(c9505,c9506)
& sub(c9505,land_1_1)
& sub(c9506,name_1_1)
& val(c9506,portugal_0)
& attr(c9518,c9519)
& sub(c9518,land_1_1)
& sub(c9519,name_1_1)
& val(c9519,russland_0)
& assoc(garantiemacht_1_2,b__374rgschaft_1_1)
& sub(garantiemacht_1_2,macht_1_2)
& etype(c9434,int0)
& fact(c9434,real)
& gener(c9434,sp)
& varia(c9434,con)
& etype(abkommen_1_1,int0)
& fact(abkommen_1_1,real)
& gener(abkommen_1_1,ge)
& varia(abkommen_1_1,varia_c)
& etype(c9443,int1)
& fact(c9443,real)
& gener(c9443,sp)
& varia(c9443,varia_c)
& etype(verfechter_1_1,int0)
& fact(verfechter_1_1,real)
& gener(verfechter_1_1,ge)
& varia(verfechter_1_1,varia_c)
& etype(c9448,int1)
& fact(c9448,real)
& gener(c9448,sp)
& varia(c9448,con)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& varia(regierung_1_1,varia_c)
& etype(c9456,int1)
& fact(c9456,real)
& gener(c9456,sp)
& varia(c9456,con)
& etype(c9457,int0)
& fact(c9457,real)
& gener(c9457,sp)
& varia(c9457,varia_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& varia(einrichtung_1_2,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& varia(name_1_1,varia_c)
& etype(c9458,int1)
& fact(c9458,real)
& gener(c9458,gener_c)
& varia(c9458,varia_c)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& varia(meuterer_1_1,varia_c)
& etype(c9464,int0)
& fact(c9464,real)
& gener(c9464,sp)
& varia(c9464,varia_c)
& etype(druck_1_1,int0)
& fact(druck_1_1,real)
& gener(druck_1_1,ge)
& varia(druck_1_1,varia_c)
& etype(c9473,int0)
& fact(c9473,real)
& gener(c9473,sp)
& varia(c9473,con)
& etype(c9474,int0)
& fact(c9474,real)
& gener(c9474,sp)
& varia(c9474,varia_c)
& etype(c9475,int0)
& fact(c9475,real)
& gener(c9475,sp)
& varia(c9475,varia_c)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& varia(pr__344sident_1_1,varia_c)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& varia(eigenname_1_1,varia_c)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& varia(familiename_1_1,varia_c)
& etype(c9484,int0)
& fact(c9484,real)
& gener(c9484,sp)
& varia(c9484,con)
& etype(c9485,int0)
& fact(c9485,real)
& gener(c9485,sp)
& varia(c9485,varia_c)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& varia(land_1_1,varia_c)
& etype(c9488,int0)
& fact(c9488,real)
& gener(c9488,sp)
& varia(c9488,con)
& etype(c9489,int0)
& fact(c9489,real)
& gener(c9489,sp)
& varia(c9489,varia_c)
& etype(c9490,int0)
& fact(c9490,real)
& gener(c9490,sp)
& varia(c9490,varia_c)
& etype(c9495,int1)
& fact(c9495,real)
& gener(c9495,sp)
& varia(c9495,con)
& etype(garantiemacht_1_2,int0)
& fact(garantiemacht_1_2,real)
& gener(garantiemacht_1_2,ge)
& varia(garantiemacht_1_2,varia_c)
& etype(c9500,int0)
& fact(c9500,real)
& gener(c9500,sp)
& varia(c9500,con)
& etype(c9501,int0)
& fact(c9501,real)
& gener(c9501,sp)
& varia(c9501,varia_c)
& etype(c9505,int0)
& fact(c9505,real)
& gener(c9505,sp)
& varia(c9505,con)
& etype(c9506,int0)
& fact(c9506,real)
& gener(c9506,sp)
& varia(c9506,varia_c)
& etype(c9518,int0)
& fact(c9518,real)
& gener(c9518,sp)
& varia(c9518,con)
& etype(c9519,int0)
& fact(c9519,real)
& gener(c9519,sp)
& varia(c9519,varia_c)
& etype(c9590,etype_c)
& fact(c9590,real)
& gener(c9590,gener_c)
& varia(c9590,varia_c)
& etype(b__374rgschaft_1_1,int0)
& fact(b__374rgschaft_1_1,real)
& gener(b__374rgschaft_1_1,ge)
& varia(b__374rgschaft_1_1,varia_c)
& etype(macht_1_2,int0)
& fact(macht_1_2,real)
& gener(macht_1_2,ge)
& varia(macht_1_2,varia_c) ),
inference(pure_predicate_removal,[],[f10212]) ).
fof(f10220,plain,
( sub(c9434,abkommen_1_1)
& pred(c9443,verfechter_1_1)
& attch(c9448,c9443)
& prop(c9448,angolanisch_1_1)
& sub(c9448,regierung_1_1)
& attr(c9456,c9457)
& sub(c9456,einrichtung_1_2)
& sub(c9457,name_1_1)
& val(c9457,unita_0)
& pred(c9458,meuterer_1_1)
& sub(c9464,druck_1_1)
& attr(c9473,c9464)
& attr(c9473,c9474)
& attr(c9473,c9475)
& prop(c9473,s__374dafrikanisch_1_1)
& sub(c9473,pr__344sident_1_1)
& sub(c9474,eigenname_1_1)
& val(c9474,nelson_0)
& sub(c9475,familiename_1_1)
& val(c9475,mandela_0)
& attr(c9484,c9485)
& sub(c9484,land_1_1)
& sub(c9485,name_1_1)
& val(c9485,simbabwe_0)
& attr(c9488,c9489)
& attr(c9488,c9490)
& sub(c9488,pr__344sident_1_1)
& sub(c9489,eigenname_1_1)
& val(c9489,robert_0)
& sub(c9490,familiename_1_1)
& val(c9490,mugabe_0)
& pred(c9495,garantiemacht_1_2)
& attr(c9500,c9501)
& sub(c9500,land_1_1)
& sub(c9501,name_1_1)
& val(c9501,usa_0)
& attr(c9505,c9506)
& sub(c9505,land_1_1)
& sub(c9506,name_1_1)
& val(c9506,portugal_0)
& attr(c9518,c9519)
& sub(c9518,land_1_1)
& sub(c9519,name_1_1)
& val(c9519,russland_0)
& assoc(garantiemacht_1_2,b__374rgschaft_1_1)
& sub(garantiemacht_1_2,macht_1_2)
& etype(c9434,int0)
& fact(c9434,real)
& gener(c9434,sp)
& etype(abkommen_1_1,int0)
& fact(abkommen_1_1,real)
& gener(abkommen_1_1,ge)
& etype(c9443,int1)
& fact(c9443,real)
& gener(c9443,sp)
& etype(verfechter_1_1,int0)
& fact(verfechter_1_1,real)
& gener(verfechter_1_1,ge)
& etype(c9448,int1)
& fact(c9448,real)
& gener(c9448,sp)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& etype(c9456,int1)
& fact(c9456,real)
& gener(c9456,sp)
& etype(c9457,int0)
& fact(c9457,real)
& gener(c9457,sp)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& etype(c9458,int1)
& fact(c9458,real)
& gener(c9458,gener_c)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& etype(c9464,int0)
& fact(c9464,real)
& gener(c9464,sp)
& etype(druck_1_1,int0)
& fact(druck_1_1,real)
& gener(druck_1_1,ge)
& etype(c9473,int0)
& fact(c9473,real)
& gener(c9473,sp)
& etype(c9474,int0)
& fact(c9474,real)
& gener(c9474,sp)
& etype(c9475,int0)
& fact(c9475,real)
& gener(c9475,sp)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& etype(c9484,int0)
& fact(c9484,real)
& gener(c9484,sp)
& etype(c9485,int0)
& fact(c9485,real)
& gener(c9485,sp)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& etype(c9488,int0)
& fact(c9488,real)
& gener(c9488,sp)
& etype(c9489,int0)
& fact(c9489,real)
& gener(c9489,sp)
& etype(c9490,int0)
& fact(c9490,real)
& gener(c9490,sp)
& etype(c9495,int1)
& fact(c9495,real)
& gener(c9495,sp)
& etype(garantiemacht_1_2,int0)
& fact(garantiemacht_1_2,real)
& gener(garantiemacht_1_2,ge)
& etype(c9500,int0)
& fact(c9500,real)
& gener(c9500,sp)
& etype(c9501,int0)
& fact(c9501,real)
& gener(c9501,sp)
& etype(c9505,int0)
& fact(c9505,real)
& gener(c9505,sp)
& etype(c9506,int0)
& fact(c9506,real)
& gener(c9506,sp)
& etype(c9518,int0)
& fact(c9518,real)
& gener(c9518,sp)
& etype(c9519,int0)
& fact(c9519,real)
& gener(c9519,sp)
& etype(c9590,etype_c)
& fact(c9590,real)
& gener(c9590,gener_c)
& etype(b__374rgschaft_1_1,int0)
& fact(b__374rgschaft_1_1,real)
& gener(b__374rgschaft_1_1,ge)
& etype(macht_1_2,int0)
& fact(macht_1_2,real)
& gener(macht_1_2,ge) ),
inference(pure_predicate_removal,[],[f10215]) ).
fof(f10225,plain,
( sub(c9434,abkommen_1_1)
& pred(c9443,verfechter_1_1)
& attch(c9448,c9443)
& prop(c9448,angolanisch_1_1)
& sub(c9448,regierung_1_1)
& attr(c9456,c9457)
& sub(c9456,einrichtung_1_2)
& sub(c9457,name_1_1)
& val(c9457,unita_0)
& pred(c9458,meuterer_1_1)
& sub(c9464,druck_1_1)
& attr(c9473,c9464)
& attr(c9473,c9474)
& attr(c9473,c9475)
& prop(c9473,s__374dafrikanisch_1_1)
& sub(c9473,pr__344sident_1_1)
& sub(c9474,eigenname_1_1)
& val(c9474,nelson_0)
& sub(c9475,familiename_1_1)
& val(c9475,mandela_0)
& attr(c9484,c9485)
& sub(c9484,land_1_1)
& sub(c9485,name_1_1)
& val(c9485,simbabwe_0)
& attr(c9488,c9489)
& attr(c9488,c9490)
& sub(c9488,pr__344sident_1_1)
& sub(c9489,eigenname_1_1)
& val(c9489,robert_0)
& sub(c9490,familiename_1_1)
& val(c9490,mugabe_0)
& pred(c9495,garantiemacht_1_2)
& attr(c9500,c9501)
& sub(c9500,land_1_1)
& sub(c9501,name_1_1)
& val(c9501,usa_0)
& attr(c9505,c9506)
& sub(c9505,land_1_1)
& sub(c9506,name_1_1)
& val(c9506,portugal_0)
& attr(c9518,c9519)
& sub(c9518,land_1_1)
& sub(c9519,name_1_1)
& val(c9519,russland_0)
& assoc(garantiemacht_1_2,b__374rgschaft_1_1)
& sub(garantiemacht_1_2,macht_1_2)
& etype(c9434,int0)
& fact(c9434,real)
& etype(abkommen_1_1,int0)
& fact(abkommen_1_1,real)
& etype(c9443,int1)
& fact(c9443,real)
& etype(verfechter_1_1,int0)
& fact(verfechter_1_1,real)
& etype(c9448,int1)
& fact(c9448,real)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& etype(c9456,int1)
& fact(c9456,real)
& etype(c9457,int0)
& fact(c9457,real)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& etype(c9458,int1)
& fact(c9458,real)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& etype(c9464,int0)
& fact(c9464,real)
& etype(druck_1_1,int0)
& fact(druck_1_1,real)
& etype(c9473,int0)
& fact(c9473,real)
& etype(c9474,int0)
& fact(c9474,real)
& etype(c9475,int0)
& fact(c9475,real)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& etype(c9484,int0)
& fact(c9484,real)
& etype(c9485,int0)
& fact(c9485,real)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& etype(c9488,int0)
& fact(c9488,real)
& etype(c9489,int0)
& fact(c9489,real)
& etype(c9490,int0)
& fact(c9490,real)
& etype(c9495,int1)
& fact(c9495,real)
& etype(garantiemacht_1_2,int0)
& fact(garantiemacht_1_2,real)
& etype(c9500,int0)
& fact(c9500,real)
& etype(c9501,int0)
& fact(c9501,real)
& etype(c9505,int0)
& fact(c9505,real)
& etype(c9506,int0)
& fact(c9506,real)
& etype(c9518,int0)
& fact(c9518,real)
& etype(c9519,int0)
& fact(c9519,real)
& etype(c9590,etype_c)
& fact(c9590,real)
& etype(b__374rgschaft_1_1,int0)
& fact(b__374rgschaft_1_1,real)
& etype(macht_1_2,int0)
& fact(macht_1_2,real) ),
inference(pure_predicate_removal,[],[f10220]) ).
fof(f10228,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ in(X5,X6)
| ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ attr(X6,X7)
| ~ obj(X8,X0)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X9)
| ~ sub(X7,name_1_1)
| ~ subr(X3,rprs_0)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ val(X7,s__374dafrika_0) ),
inference(ennf_transformation,[],[f10189]) ).
fof(f10235,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( arg1(X4,X1)
& arg2(X4,X5)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& sub(X5,X2)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(ennf_transformation,[],[f162]) ).
fof(f10236,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( arg1(X4,X1)
& arg2(X4,X5)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& sub(X5,X2)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(flattening,[],[f10235]) ).
fof(f10245,plain,
! [X0,X1] :
( ? [X2] :
( loc(X2,X0)
& obj(X2,X1)
& subs(X2,geben_1_1) )
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(ennf_transformation,[],[f95]) ).
fof(f10246,plain,
! [X0,X1] :
( ? [X2] :
( loc(X2,X0)
& obj(X2,X1)
& subs(X2,geben_1_1) )
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(flattening,[],[f10245]) ).
fof(f10253,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f10273,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( in(X5,X3)
& attr(X3,X4)
& loc(X0,X5)
& sub(X3,land_1_1)
& sub(X4,name_1_1)
& val(X4,X2) )
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(ennf_transformation,[],[f155]) ).
fof(f10274,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( in(X5,X3)
& attr(X3,X4)
& loc(X0,X5)
& sub(X3,land_1_1)
& sub(X4,name_1_1)
& val(X4,X2) )
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(flattening,[],[f10273]) ).
fof(f10299,plain,
! [X0,X1] :
( ? [X2] :
( arg1(X2,X0)
& arg2(X2,X1)
& subr(X2,sub_0) )
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f163]) ).
fof(f10381,plain,
! [X0,X1,X2] :
( ( arg1(sK2(X0,X1,X2),X1)
& arg2(sK2(X0,X1,X2),sK3(X0,X1,X2))
& hsit(X0,sK1(X0,X1,X2))
& mcont(sK1(X0,X1,X2),sK2(X0,X1,X2))
& obj(sK1(X0,X1,X2),X1)
& sub(sK3(X0,X1,X2),X2)
& subr(sK2(X0,X1,X2),rprs_0)
& subs(sK1(X0,X1,X2),bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X3,sK1(X0,X1,X2)),skolemize(X4,sK2(X0,X1,X2)),skolemize(X5,sK3(X0,X1,X2))],[f10236]) ).
fof(f10385,plain,
! [X0,X1] :
( ( loc(sK8(X0,X1),X0)
& obj(sK8(X0,X1),X1)
& subs(sK8(X0,X1),geben_1_1) )
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(X2,sK8(X0,X1))],[f10246]) ).
fof(f10392,plain,
! [X0,X1,X2] :
( ( in(sK19(X0,X2),sK17(X0,X2))
& attr(sK17(X0,X2),sK18(X0,X2))
& loc(X0,sK19(X0,X2))
& sub(sK17(X0,X2),land_1_1)
& sub(sK18(X0,X2),name_1_1)
& val(sK18(X0,X2),X2) )
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17,sK18,sK19]),skolemize(X3,sK17(X0,X2)),skolemize(X4,sK18(X0,X2)),skolemize(X5,sK19(X0,X2))],[f10274]) ).
fof(f10402,plain,
! [X0,X1] :
( ( arg1(sK33(X0,X1),X0)
& arg2(sK33(X0,X1),X1)
& subr(sK33(X0,X1),sub_0) )
| ~ sub(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33]),skolemize(X2,sK33(X0,X1))],[f10299]) ).
fof(f10421,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ in(X5,X6)
| ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ attr(X6,X7)
| ~ obj(X8,X0)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X9)
| ~ sub(X7,name_1_1)
| ~ subr(X3,rprs_0)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ val(X7,s__374dafrika_0) ),
inference(cnf_transformation,[],[f10228]) ).
fof(f10466,plain,
fact(c9473,real),
inference(cnf_transformation,[],[f10225]) ).
fof(f10522,plain,
val(c9475,mandela_0),
inference(cnf_transformation,[],[f10225]) ).
fof(f10523,plain,
sub(c9475,familiename_1_1),
inference(cnf_transformation,[],[f10225]) ).
fof(f10524,plain,
val(c9474,nelson_0),
inference(cnf_transformation,[],[f10225]) ).
fof(f10525,plain,
sub(c9474,eigenname_1_1),
inference(cnf_transformation,[],[f10225]) ).
fof(f10526,plain,
sub(c9473,pr__344sident_1_1),
inference(cnf_transformation,[],[f10225]) ).
fof(f10527,plain,
prop(c9473,s__374dafrikanisch_1_1),
inference(cnf_transformation,[],[f10225]) ).
fof(f10528,plain,
attr(c9473,c9475),
inference(cnf_transformation,[],[f10225]) ).
fof(f10529,plain,
attr(c9473,c9474),
inference(cnf_transformation,[],[f10225]) ).
fof(f10546,plain,
! [X2,X0,X1] :
( subr(sK2(X0,X1,X2),rprs_0)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10381]) ).
fof(f10547,plain,
! [X2,X0,X1] :
( sub(sK3(X0,X1,X2),X2)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10381]) ).
fof(f10551,plain,
! [X2,X0,X1] :
( arg2(sK2(X0,X1,X2),sK3(X0,X1,X2))
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10381]) ).
fof(f10552,plain,
! [X2,X0,X1] :
( arg1(sK2(X0,X1,X2),X1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10381]) ).
fof(f10568,plain,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
inference(cnf_transformation,[],[f9161]) ).
fof(f10570,plain,
! [X0,X1] :
( obj(sK8(X0,X1),X1)
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(cnf_transformation,[],[f10385]) ).
fof(f10582,plain,
! [X0,X1] :
( ~ fact(X0,X1)
| has_fact_leq(X0,X1) ),
inference(cnf_transformation,[],[f10253]) ).
fof(f10624,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| val(sK18(X0,X2),X2) ),
inference(cnf_transformation,[],[f10392]) ).
fof(f10625,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| sub(sK18(X0,X2),name_1_1) ),
inference(cnf_transformation,[],[f10392]) ).
fof(f10627,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| loc(X0,sK19(X0,X2)) ),
inference(cnf_transformation,[],[f10392]) ).
fof(f10628,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| attr(sK17(X0,X2),sK18(X0,X2)) ),
inference(cnf_transformation,[],[f10392]) ).
fof(f10629,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| in(sK19(X0,X2),sK17(X0,X2)) ),
inference(cnf_transformation,[],[f10392]) ).
fof(f10680,plain,
! [X0,X1] :
( subr(sK33(X0,X1),sub_0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10402]) ).
fof(f10681,plain,
! [X0,X1] :
( arg2(sK33(X0,X1),X1)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10402]) ).
fof(f10682,plain,
! [X0,X1] :
( arg1(sK33(X0,X1),X0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10402]) ).
fof(f10867,definition,
( spl50_1
<=> ! [X4,X9,X0,X8,X3,X2,X1] :
( ~ arg1(X3,X0)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(X3,rprs_0)
| ~ sub(X4,X9)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X8,X0)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4) ) ),
introduced(definition,[new_symbols(definition,[spl50_1])],[avatar_definition]) ).
fof(f10868,plain,
( ! [X2,X3,X0,X1,X8,X9,X4] :
( ~ val(X2,nelson_0)
| ~ arg1(X3,X0)
| ~ val(X1,mandela_0)
| ~ subr(X3,rprs_0)
| ~ sub(X4,X9)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X8,X0)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4) )
| ~ spl50_1 ),
inference(avatar_component_clause,[],[f10867]) ).
fof(f10870,definition,
( spl50_2
<=> ! [X6,X5,X7] :
( ~ in(X5,X6)
| ~ val(X7,s__374dafrika_0)
| ~ sub(X7,name_1_1)
| ~ attr(X6,X7) ) ),
introduced(definition,[new_symbols(definition,[spl50_2])],[avatar_definition]) ).
fof(f10871,plain,
( ! [X6,X7,X5] :
( ~ val(X7,s__374dafrika_0)
| ~ in(X5,X6)
| ~ sub(X7,name_1_1)
| ~ attr(X6,X7) )
| ~ spl50_2 ),
inference(avatar_component_clause,[],[f10870]) ).
fof(f10872,plain,
( spl50_1
| spl50_2 ),
inference(avatar_split_clause,[],[f10421,f10870,f10867]) ).
fof(f10891,plain,
has_fact_leq(c9473,real),
inference(resolution,[],[f10582,f10466]) ).
fof(f11219,plain,
! [X0] :
( val(sK18(X0,s__374dafrika_0),s__374dafrika_0)
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[],[f10624,f10568]) ).
fof(f11225,plain,
! [X0] :
( sub(sK18(X0,s__374dafrika_0),name_1_1)
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[],[f10625,f10568]) ).
fof(f11237,plain,
! [X0] :
( loc(X0,sK19(X0,s__374dafrika_0))
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[],[f10627,f10568]) ).
fof(f11454,plain,
! [X0] :
( attr(sK17(X0,s__374dafrika_0),sK18(X0,s__374dafrika_0))
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[],[f10628,f10568]) ).
fof(f11460,plain,
! [X0] :
( in(sK19(X0,s__374dafrika_0),sK17(X0,s__374dafrika_0))
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[],[f10629,f10568]) ).
fof(f12019,plain,
( ! [X2,X0,X1] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| ~ in(X1,X2)
| ~ sub(sK18(X0,s__374dafrika_0),name_1_1)
| ~ attr(X2,sK18(X0,s__374dafrika_0)) )
| ~ spl50_2 ),
inference(resolution,[],[f11219,f10871]) ).
fof(f12020,plain,
( ! [X2,X0,X1] :
( ~ attr(X2,sK18(X0,s__374dafrika_0))
| ~ in(X1,X2)
| ~ prop(X0,s__374dafrikanisch_1_1) )
| ~ spl50_2 ),
inference(forward_subsumption_resolution,[],[f12019,f11225]) ).
fof(f14555,plain,
( ! [X0,X1] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| ~ in(X1,sK17(X0,s__374dafrika_0))
| ~ prop(X0,s__374dafrikanisch_1_1) )
| ~ spl50_2 ),
inference(resolution,[],[f11454,f12020]) ).
fof(f14556,plain,
( ! [X0,X1] :
( ~ in(X1,sK17(X0,s__374dafrika_0))
| ~ prop(X0,s__374dafrikanisch_1_1) )
| ~ spl50_2 ),
inference(duplicate_literal_removal,[],[f14555]) ).
fof(f14582,plain,
( ! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| ~ prop(X0,s__374dafrikanisch_1_1) )
| ~ spl50_2 ),
inference(resolution,[],[f11460,f14556]) ).
fof(f14588,plain,
( ! [X0] : ~ prop(X0,s__374dafrikanisch_1_1)
| ~ spl50_2 ),
inference(duplicate_literal_removal,[],[f14582]) ).
fof(f14589,plain,
( $false
| ~ spl50_2 ),
inference(resolution,[],[f14588,f10527]) ).
fof(f14590,plain,
~ spl50_2,
inference(avatar_contradiction_clause,[],[f14589]) ).
fof(f14591,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ arg1(X0,X1)
| ~ val(X2,mandela_0)
| ~ subr(X0,rprs_0)
| ~ sub(X3,X4)
| ~ sub(c9474,eigenname_1_1)
| ~ sub(X2,familiename_1_1)
| ~ obj(X5,X1)
| ~ attr(X1,c9474)
| ~ attr(X1,X2)
| ~ arg2(X0,X3) )
| ~ spl50_1 ),
inference(resolution,[],[f10868,f10524]) ).
fof(f14592,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ val(X2,mandela_0)
| ~ arg1(X0,X1)
| ~ subr(X0,rprs_0)
| ~ sub(X3,X4)
| ~ sub(X2,familiename_1_1)
| ~ obj(X5,X1)
| ~ attr(X1,c9474)
| ~ attr(X1,X2)
| ~ arg2(X0,X3) )
| ~ spl50_1 ),
inference(forward_subsumption_resolution,[],[f14591,f10525]) ).
fof(f14593,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ arg1(X0,X1)
| ~ subr(X0,rprs_0)
| ~ sub(X2,X3)
| ~ sub(c9475,familiename_1_1)
| ~ obj(X4,X1)
| ~ attr(X1,c9474)
| ~ attr(X1,c9475)
| ~ arg2(X0,X2) )
| ~ spl50_1 ),
inference(resolution,[],[f14592,f10522]) ).
fof(f14594,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ subr(X0,rprs_0)
| ~ arg1(X0,X1)
| ~ sub(X2,X3)
| ~ obj(X4,X1)
| ~ attr(X1,c9474)
| ~ attr(X1,c9475)
| ~ arg2(X0,X2) )
| ~ spl50_1 ),
inference(forward_subsumption_resolution,[],[f14593,f10523]) ).
fof(f14601,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ arg2(sK2(X0,X1,X2),X4)
| ~ sub(X4,X5)
| ~ obj(X6,X3)
| ~ attr(X3,c9474)
| ~ attr(X3,c9475)
| ~ arg1(sK2(X0,X1,X2),X3)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl50_1 ),
inference(resolution,[],[f14594,f10546]) ).
fof(f15302,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ sub(sK3(X0,X1,X2),X3)
| ~ obj(X4,X5)
| ~ attr(X5,c9474)
| ~ attr(X5,c9475)
| ~ arg1(sK2(X0,X1,X2),X5)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl50_1 ),
inference(resolution,[],[f14601,f10551]) ).
fof(f15303,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ arg1(sK2(X0,X1,X2),X5)
| ~ obj(X4,X5)
| ~ attr(X5,c9474)
| ~ attr(X5,c9475)
| ~ sub(sK3(X0,X1,X2),X3)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl50_1 ),
inference(duplicate_literal_removal,[],[f15302]) ).
fof(f15306,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ obj(X0,X1)
| ~ attr(X1,c9474)
| ~ attr(X1,c9475)
| ~ sub(sK3(X2,X1,X3),X4)
| ~ arg1(X2,X1)
| ~ arg2(X2,X3)
| ~ subr(X2,sub_0)
| ~ arg1(X2,X1)
| ~ arg2(X2,X3)
| ~ subr(X2,sub_0) )
| ~ spl50_1 ),
inference(resolution,[],[f15303,f10552]) ).
fof(f15307,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ sub(sK3(X2,X1,X3),X4)
| ~ attr(X1,c9474)
| ~ attr(X1,c9475)
| ~ obj(X0,X1)
| ~ arg1(X2,X1)
| ~ arg2(X2,X3)
| ~ subr(X2,sub_0) )
| ~ spl50_1 ),
inference(duplicate_literal_removal,[],[f15306]) ).
fof(f15308,plain,
( ! [X2,X3,X0,X1] :
( ~ attr(X0,c9474)
| ~ attr(X0,c9475)
| ~ obj(X1,X0)
| ~ arg1(X2,X0)
| ~ arg2(X2,X3)
| ~ subr(X2,sub_0)
| ~ arg1(X2,X0)
| ~ arg2(X2,X3)
| ~ subr(X2,sub_0) )
| ~ spl50_1 ),
inference(resolution,[],[f15307,f10547]) ).
fof(f15309,plain,
( ! [X2,X3,X0,X1] :
( ~ subr(X2,sub_0)
| ~ attr(X0,c9475)
| ~ obj(X1,X0)
| ~ arg1(X2,X0)
| ~ arg2(X2,X3)
| ~ attr(X0,c9474) )
| ~ spl50_1 ),
inference(duplicate_literal_removal,[],[f15308]) ).
fof(f15311,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ arg2(sK33(X2,X3),X4)
| ~ obj(X1,X0)
| ~ arg1(sK33(X2,X3),X0)
| ~ attr(X0,c9475)
| ~ attr(X0,c9474)
| ~ sub(X2,X3) )
| ~ spl50_1 ),
inference(resolution,[],[f15309,f10680]) ).
fof(f15331,plain,
( ! [X2,X3,X0,X1] :
( ~ obj(X0,X1)
| ~ arg1(sK33(X2,X3),X1)
| ~ attr(X1,c9475)
| ~ attr(X1,c9474)
| ~ sub(X2,X3)
| ~ sub(X2,X3) )
| ~ spl50_1 ),
inference(resolution,[],[f15311,f10681]) ).
fof(f15332,plain,
( ! [X2,X3,X0,X1] :
( ~ arg1(sK33(X2,X3),X1)
| ~ obj(X0,X1)
| ~ attr(X1,c9475)
| ~ attr(X1,c9474)
| ~ sub(X2,X3) )
| ~ spl50_1 ),
inference(duplicate_literal_removal,[],[f15331]) ).
fof(f15351,plain,
( ! [X2,X0,X1] :
( ~ obj(X0,X1)
| ~ attr(X1,c9475)
| ~ attr(X1,c9474)
| ~ sub(X1,X2)
| ~ sub(X1,X2) )
| ~ spl50_1 ),
inference(resolution,[],[f15332,f10682]) ).
fof(f15352,plain,
( ! [X2,X0,X1] :
( ~ attr(X1,c9475)
| ~ obj(X0,X1)
| ~ attr(X1,c9474)
| ~ sub(X1,X2) )
| ~ spl50_1 ),
inference(duplicate_literal_removal,[],[f15351]) ).
fof(f15353,plain,
( ! [X0,X1] :
( ~ obj(X0,c9473)
| ~ attr(c9473,c9474)
| ~ sub(c9473,X1) )
| ~ spl50_1 ),
inference(resolution,[],[f15352,f10528]) ).
fof(f15354,plain,
( ! [X0,X1] :
( ~ obj(X0,c9473)
| ~ sub(c9473,X1) )
| ~ spl50_1 ),
inference(forward_subsumption_resolution,[],[f15353,f10529]) ).
fof(f15356,definition,
( spl50_470
<=> ! [X1] : ~ sub(c9473,X1) ),
introduced(definition,[new_symbols(definition,[spl50_470])],[avatar_definition]) ).
fof(f15357,plain,
( ! [X1] : ~ sub(c9473,X1)
| ~ spl50_470 ),
inference(avatar_component_clause,[],[f15356]) ).
fof(f15359,definition,
( spl50_471
<=> ! [X0] : ~ obj(X0,c9473) ),
introduced(definition,[new_symbols(definition,[spl50_471])],[avatar_definition]) ).
fof(f15360,plain,
( ! [X0] : ~ obj(X0,c9473)
| ~ spl50_471 ),
inference(avatar_component_clause,[],[f15359]) ).
fof(f15361,plain,
( spl50_470
| spl50_471
| ~ spl50_1 ),
inference(avatar_split_clause,[],[f15354,f10867,f15359,f15356]) ).
fof(f15381,plain,
( $false
| ~ spl50_470 ),
inference(resolution,[],[f15357,f10526]) ).
fof(f15382,plain,
~ spl50_470,
inference(avatar_contradiction_clause,[],[f15381]) ).
fof(f15403,plain,
( ! [X0] :
( ~ has_fact_leq(c9473,real)
| ~ loc(c9473,X0) )
| ~ spl50_471 ),
inference(resolution,[],[f15360,f10570]) ).
fof(f15410,plain,
( ! [X0] : ~ loc(c9473,X0)
| ~ spl50_471 ),
inference(forward_subsumption_resolution,[],[f15403,f10891]) ).
fof(f15416,plain,
( ~ prop(c9473,s__374dafrikanisch_1_1)
| ~ spl50_471 ),
inference(resolution,[],[f15410,f11237]) ).
fof(f15417,plain,
( $false
| ~ spl50_471 ),
inference(forward_subsumption_resolution,[],[f15416,f10527]) ).
fof(f15418,plain,
~ spl50_471,
inference(avatar_contradiction_clause,[],[f15417]) ).
cnf(s1,plain,
( spl50_1
| spl50_2 ),
inference(sat_conversion,[],[f10872]) ).
cnf(s243,plain,
~ spl50_2,
inference(sat_conversion,[],[f14590]) ).
cnf(s284,plain,
( ~ spl50_1
| spl50_470
| spl50_471 ),
inference(sat_conversion,[],[f15361]) ).
cnf(s285,plain,
~ spl50_470,
inference(sat_conversion,[],[f15382]) ).
cnf(s286,plain,
~ spl50_471,
inference(sat_conversion,[],[f15418]) ).
cnf(s287,plain,
~ spl50_1,
inference(rat,[],[s284,s286,s285]) ).
cnf(s288,plain,
$false,
inference(rat,[],[s1,s243,s287]) ).
fof(f15419,plain,
$false,
inference(avatar_sat_refutation,[],[s288]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR116+29 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.29 % Computer : n008.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8046.5625MB
% 0.10/0.29 % OS : Linux 6.8.0-71-generic
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Mon Sep 28 23:29:24 UTC 2026
% 0.25/0.29 % CPUTime :
% 0.25/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.25/0.34 Running first-order theorem proving
% 0.25/0.34 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
% 7.02/2.08 % (2755988)Detected formulas, will run a generic FOF schedule.
% 7.02/2.08 % (2755997)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2194221089:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 7.02/2.08 % (2755996)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3923370213:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 7.02/2.08 % (2755994)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=241200331:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 7.02/2.08 % (2755997)Refutation not found, incomplete strategy
% 7.02/2.08 % (2755997)------------------------------
% 7.02/2.08 % (2755997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.02/2.08 % (2755997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.02/2.08 % (2755997)CaDiCaL version: 2.1.3
% 7.02/2.08 % (2755997)Termination reason: Refutation not found, incomplete strategy
% 7.02/2.08 % (2755997)Time elapsed: 0.027 s
% 7.02/2.08 % (2755997)Peak memory usage: 97 MB
% 7.02/2.08 % (2755997)Instructions burned: 62 (million)
% 7.02/2.08 % (2755996)Refutation not found, incomplete strategy
% 7.02/2.08 % (2755996)------------------------------
% 7.02/2.08 % (2755996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.02/2.08 % (2755996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.02/2.08 % (2755996)CaDiCaL version: 2.1.3
% 7.02/2.08 % (2755996)Termination reason: Refutation not found, incomplete strategy
% 7.02/2.08 % (2755996)Time elapsed: 0.050 s
% 7.02/2.08 % (2755996)Peak memory usage: 97 MB
% 7.02/2.08 % (2755996)Instructions burned: 65 (million)
% 7.02/2.08 % (2755995)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=2983466846:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 7.02/2.08 % (2755993)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=1441299700:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 7.02/2.08 % (2755999)dis-21_1_sil=8000:lcm=predicate:random_seed=1712701716:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 7.02/2.08 % (2755998)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1913558846:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 7.02/2.08 % (2755999)Instruction limit reached!
% 7.02/2.08 % (2755999)------------------------------
% 7.02/2.08 % (2755999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.02/2.08 % (2755999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.02/2.08 % (2755999)CaDiCaL version: 2.1.3
% 7.02/2.08 % (2755999)Termination reason: Instruction limit
% 7.02/2.08 % (2755999)Termination phase: Saturation
% 7.02/2.08 % (2755999)Time elapsed: 0.101 s
% 7.02/2.08 % (2755999)Peak memory usage: 98 MB
% 7.02/2.08 % (2755999)Instructions burned: 129 (million)
% 7.02/2.08 % (2755998)Instruction limit reached!
% 7.02/2.08 % (2755998)------------------------------
% 7.02/2.08 % (2755998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.02/2.09 % (2755998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.02/2.09 % (2755998)CaDiCaL version: 2.1.3
% 7.02/2.09 % (2755998)Termination reason: Instruction limit
% 7.02/2.09 % (2755998)Termination phase: Property scanning
% 7.02/2.09 % (2755998)Time elapsed: 0.120 s
% 7.02/2.09 % (2755998)Peak memory usage: 96 MB
% 7.02/2.09 % (2755998)Instructions burned: 139 (million)
% 7.02/2.09 % (2755997)------------------------------
% 7.02/2.09 % (2755997)------------------------------
% 7.02/2.09 % (2756007)lrs+10_1_sil=8000:sp=occurrence:random_seed=3046861448:i=285:sd=3:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/285Mi)
% 7.02/2.09 % (2755996)------------------------------
% 7.02/2.09 % (2755996)------------------------------
% 7.02/2.09 % (2756007)First to succeed.
% 7.02/2.09 % (2756007)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2755988"
% 7.02/2.09 % (2756008)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1653970220:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 7.02/2.09 % (2756009)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2409195584:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 7.02/2.09 % (2756008)Refutation not found, incomplete strategy
% 7.02/2.09 % (2756008)------------------------------
% 7.02/2.09 % (2756008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.02/2.09 % (2756008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.02/2.09 % (2756008)CaDiCaL version: 2.1.3
% 7.02/2.09 % (2756008)Termination reason: Refutation not found, incomplete strategy
% 7.02/2.09 % (2756008)Time elapsed: 0.076 s
% 7.02/2.09 % (2756008)Peak memory usage: 98 MB
% 7.02/2.09 % (2756008)Instructions burned: 97 (million)
% 7.02/2.09 % (2756009)Also succeeded, but the first one will report.
% 7.02/2.09 % (2756007)Refutation found. Thanks to Tanya!
% 7.02/2.09 % SZS status Theorem for theBenchmark
% 7.02/2.09 % SZS output start Proof for theBenchmark
% See solution above
% 7.93/2.30 % (2756007)------------------------------
% 7.93/2.30 % (2756007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.93/2.30 % (2756007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.93/2.30 % (2756007)CaDiCaL version: 2.1.3
% 7.93/2.30 % (2756007)Termination reason: Refutation
% 7.93/2.30 % (2756007)Time elapsed: 0.124 s
% 7.93/2.30 % (2756007)Peak memory usage: 102 MB
% 7.93/2.30 % (2756007)Instructions burned: 194 (million)
% 7.93/2.30 % (2756007)------------------------------
% 7.93/2.30 % (2756007)------------------------------
% 7.93/2.30 % (2755988)Success in time 1.152 s
% 7.93/2.30 % Vampire exiting
%------------------------------------------------------------------------------