%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR116+10 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:45:47 AM UTC 2026
% Result : Theorem 5.70s 1.15s
% Output : Refutation 5.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 15
% Syntax : Number of formulae : 135 ( 31 unt; 7 def)
% Number of atoms : 2849 ( 0 equ)
% Maximal formula atoms : 367 ( 21 avg)
% Number of connectives : 2963 ( 249 ~; 273 |;2430 &)
% ( 7 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 367 ( 24 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 36 usr; 8 prp; 0-12 aty)
% Number of functors : 94 ( 94 usr; 86 con; 0-3 aty)
% Number of variables : 267 ( 0 sgn 224 !; 43 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',member_first) ).
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/Axioms/CSR004+0.ax',state_adjective__in_state) ).
fof(f160,axiom,
! [X0,X1,X2] :
( ( attr(X2,X0)
& member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
& sub(X0,X1) )
=> ? [X3] :
( mcont(X3,X2)
& obj(X3,X2)
& scar(X3,X2)
& subs(X3,stehen_1_b) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',attr_name__abk__374rzung_stehen_1_b_f__374r) ).
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/Axioms/CSR004+0.ax',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/Axioms/CSR004+0.ax',sub__sub_0_expansion) ).
fof(f9161,axiom,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',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_1665) ).
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,
( attr(c28444,c28445)
& attr(c28444,c28446)
& prop(c28444,s__374dafrikanisch_1_1)
& sub(c28444,pr__344sident_1_1)
& sub(c28445,eigenname_1_1)
& val(c28445,nelson_0)
& sub(c28446,familiename_1_1)
& val(c28446,mandela_0)
& attr(c28457,c28458)
& sub(c28457,land_1_1)
& sub(c28458,name_1_1)
& val(c28458,botswana_0)
& sub(c28459,quett_1_1)
& sub(c28460,masire_1_1)
& sub(c28468,generalsekretaer_1_1)
& attch(c28473,c28468)
& sub(c28473,organisation_1_1)
& attch(c28477,c28473)
& prop(c28477,afrikanisch__1_1)
& sub(c28477,einheit_1_1)
& attr(c28487,c28488)
& attr(c28487,c28490)
& sub(c28487,mensch_1_1)
& sub(c28488,eigenname_1_1)
& val(c28488,c28489)
& tupl(c28489,salim_0,ahmed_0)
& sub(c28490,familiename_1_1)
& val(c28490,salim_0)
& attr(c28496,c28497)
& sub(c28496,mensch_1_1)
& sub(c28497,familiename_1_1)
& val(c28497,mugabe_0)
& attr(c28502,c28503)
& sub(c28502,stadt__1_1)
& sub(c28503,name_1_1)
& val(c28503,pretoria_0)
& quant_p3(c28511,c28504,stunde_1_1)
& subs(c28514,krise_1_1)
& attr(c28534,c28535)
& sub(c28534,land_1_1)
& sub(c28535,name_1_1)
& val(c28535,lesotho_0)
& tupl_p12(c28553,c28444,c28457,c28459,c28460,c28468,c28487,c28496,c28502,c28511,c28514,c28534)
& assoc(generalsekretaer_1_1,allgemein_1_1)
& sub(generalsekretaer_1_1,sekret__344r_1_1)
& sort(c28444,d)
& card(c28444,int1)
& etype(c28444,int0)
& fact(c28444,real)
& gener(c28444,sp)
& quant(c28444,one)
& refer(c28444,det)
& varia(c28444,con)
& sort(c28445,na)
& card(c28445,int1)
& etype(c28445,int0)
& fact(c28445,real)
& gener(c28445,sp)
& quant(c28445,one)
& refer(c28445,indet)
& varia(c28445,varia_c)
& sort(c28446,na)
& card(c28446,int1)
& etype(c28446,int0)
& fact(c28446,real)
& gener(c28446,sp)
& quant(c28446,one)
& refer(c28446,indet)
& varia(c28446,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(c28457,d)
& sort(c28457,io)
& card(c28457,int1)
& etype(c28457,int0)
& fact(c28457,real)
& gener(c28457,sp)
& quant(c28457,one)
& refer(c28457,det)
& varia(c28457,con)
& sort(c28458,na)
& card(c28458,int1)
& etype(c28458,int0)
& fact(c28458,real)
& gener(c28458,sp)
& quant(c28458,one)
& refer(c28458,indet)
& varia(c28458,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(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(botswana_0,fe)
& sort(c28459,o)
& card(c28459,int1)
& etype(c28459,int0)
& fact(c28459,real)
& gener(c28459,gener_c)
& quant(c28459,one)
& refer(c28459,refer_c)
& varia(c28459,varia_c)
& sort(quett_1_1,o)
& card(quett_1_1,int1)
& etype(quett_1_1,int0)
& fact(quett_1_1,real)
& gener(quett_1_1,ge)
& quant(quett_1_1,one)
& refer(quett_1_1,refer_c)
& varia(quett_1_1,varia_c)
& sort(c28460,o)
& card(c28460,int1)
& etype(c28460,int0)
& fact(c28460,real)
& gener(c28460,gener_c)
& quant(c28460,one)
& refer(c28460,refer_c)
& varia(c28460,varia_c)
& sort(masire_1_1,o)
& card(masire_1_1,int1)
& etype(masire_1_1,int0)
& fact(masire_1_1,real)
& gener(masire_1_1,ge)
& quant(masire_1_1,one)
& refer(masire_1_1,refer_c)
& varia(masire_1_1,varia_c)
& sort(c28468,d)
& card(c28468,int1)
& etype(c28468,int0)
& fact(c28468,real)
& gener(c28468,sp)
& quant(c28468,one)
& refer(c28468,det)
& varia(c28468,con)
& sort(generalsekretaer_1_1,d)
& card(generalsekretaer_1_1,int1)
& etype(generalsekretaer_1_1,int0)
& fact(generalsekretaer_1_1,real)
& gener(generalsekretaer_1_1,ge)
& quant(generalsekretaer_1_1,one)
& refer(generalsekretaer_1_1,refer_c)
& varia(generalsekretaer_1_1,varia_c)
& sort(c28473,d)
& sort(c28473,io)
& card(c28473,int1)
& etype(c28473,int1)
& fact(c28473,real)
& gener(c28473,sp)
& quant(c28473,one)
& refer(c28473,det)
& varia(c28473,con)
& sort(organisation_1_1,d)
& sort(organisation_1_1,io)
& card(organisation_1_1,card_c)
& etype(organisation_1_1,int1)
& fact(organisation_1_1,real)
& gener(organisation_1_1,ge)
& quant(organisation_1_1,quant_c)
& refer(organisation_1_1,refer_c)
& varia(organisation_1_1,varia_c)
& sort(c28477,io)
& sort(c28477,oa)
& card(c28477,int1)
& etype(c28477,int0)
& fact(c28477,real)
& gener(c28477,gener_c)
& quant(c28477,one)
& refer(c28477,refer_c)
& varia(c28477,varia_c)
& sort(afrikanisch__1_1,nq)
& sort(einheit_1_1,io)
& sort(einheit_1_1,oa)
& card(einheit_1_1,int1)
& etype(einheit_1_1,int0)
& fact(einheit_1_1,real)
& gener(einheit_1_1,ge)
& quant(einheit_1_1,one)
& refer(einheit_1_1,refer_c)
& varia(einheit_1_1,varia_c)
& sort(c28487,d)
& card(c28487,int1)
& etype(c28487,int0)
& fact(c28487,real)
& gener(c28487,sp)
& quant(c28487,one)
& refer(c28487,det)
& varia(c28487,con)
& sort(c28488,na)
& card(c28488,int1)
& etype(c28488,int0)
& fact(c28488,real)
& gener(c28488,sp)
& quant(c28488,one)
& refer(c28488,indet)
& varia(c28488,varia_c)
& sort(c28490,na)
& card(c28490,int1)
& etype(c28490,int0)
& fact(c28490,real)
& gener(c28490,sp)
& quant(c28490,one)
& refer(c28490,indet)
& varia(c28490,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(c28489,fe)
& sort(salim_0,fe)
& sort(ahmed_0,fe)
& sort(c28496,d)
& card(c28496,int1)
& etype(c28496,int0)
& fact(c28496,real)
& gener(c28496,sp)
& quant(c28496,one)
& refer(c28496,det)
& varia(c28496,con)
& sort(c28497,na)
& card(c28497,int1)
& etype(c28497,int0)
& fact(c28497,real)
& gener(c28497,sp)
& quant(c28497,one)
& refer(c28497,indet)
& varia(c28497,varia_c)
& sort(mugabe_0,fe)
& sort(c28502,d)
& sort(c28502,io)
& card(c28502,int1)
& etype(c28502,int0)
& fact(c28502,real)
& gener(c28502,sp)
& quant(c28502,one)
& refer(c28502,det)
& varia(c28502,con)
& sort(c28503,na)
& card(c28503,int1)
& etype(c28503,int0)
& fact(c28503,real)
& gener(c28503,sp)
& quant(c28503,one)
& refer(c28503,indet)
& varia(c28503,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(pretoria_0,fe)
& sort(c28511,m)
& sort(c28511,ta)
& card(c28511,card_c)
& etype(c28511,etype_c)
& fact(c28511,real)
& gener(c28511,gener_c)
& quant(c28511,quant_c)
& refer(c28511,refer_c)
& varia(c28511,varia_c)
& sort(c28504,nu)
& card(c28504,int6)
& sort(stunde_1_1,me)
& sort(stunde_1_1,oa)
& sort(stunde_1_1,ta)
& card(stunde_1_1,card_c)
& etype(stunde_1_1,etype_c)
& fact(stunde_1_1,real)
& gener(stunde_1_1,ge)
& quant(stunde_1_1,quant_c)
& refer(stunde_1_1,refer_c)
& varia(stunde_1_1,varia_c)
& sort(c28514,ad)
& card(c28514,int1)
& etype(c28514,int0)
& fact(c28514,real)
& gener(c28514,sp)
& quant(c28514,one)
& refer(c28514,det)
& varia(c28514,con)
& sort(krise_1_1,ad)
& card(krise_1_1,int1)
& etype(krise_1_1,int0)
& fact(krise_1_1,real)
& gener(krise_1_1,ge)
& quant(krise_1_1,one)
& refer(krise_1_1,refer_c)
& varia(krise_1_1,varia_c)
& sort(c28534,d)
& sort(c28534,io)
& card(c28534,int1)
& etype(c28534,int0)
& fact(c28534,real)
& gener(c28534,sp)
& quant(c28534,one)
& refer(c28534,det)
& varia(c28534,con)
& sort(c28535,na)
& card(c28535,int1)
& etype(c28535,int0)
& fact(c28535,real)
& gener(c28535,sp)
& quant(c28535,one)
& refer(c28535,indet)
& varia(c28535,varia_c)
& sort(lesotho_0,fe)
& sort(c28553,ent)
& card(c28553,card_c)
& etype(c28553,etype_c)
& fact(c28553,real)
& gener(c28553,gener_c)
& quant(c28553,quant_c)
& refer(c28553,refer_c)
& varia(c28553,varia_c)
& sort(allgemein_1_1,tq)
& sort(sekret__344r_1_1,d)
& card(sekret__344r_1_1,int1)
& etype(sekret__344r_1_1,int0)
& fact(sekret__344r_1_1,real)
& gener(sekret__344r_1_1,ge)
& quant(sekret__344r_1_1,one)
& refer(sekret__344r_1_1,refer_c)
& varia(sekret__344r_1_1,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_news_1665) ).
fof(f10191,plain,
( attr(c28444,c28445)
& attr(c28444,c28446)
& prop(c28444,s__374dafrikanisch_1_1)
& sub(c28444,pr__344sident_1_1)
& sub(c28445,eigenname_1_1)
& val(c28445,nelson_0)
& sub(c28446,familiename_1_1)
& val(c28446,mandela_0)
& attr(c28457,c28458)
& sub(c28457,land_1_1)
& sub(c28458,name_1_1)
& val(c28458,botswana_0)
& sub(c28459,quett_1_1)
& sub(c28460,masire_1_1)
& sub(c28468,generalsekretaer_1_1)
& attch(c28473,c28468)
& sub(c28473,organisation_1_1)
& attch(c28477,c28473)
& prop(c28477,afrikanisch__1_1)
& sub(c28477,einheit_1_1)
& attr(c28487,c28488)
& attr(c28487,c28490)
& sub(c28487,mensch_1_1)
& sub(c28488,eigenname_1_1)
& val(c28488,c28489)
& tupl(c28489,salim_0,ahmed_0)
& sub(c28490,familiename_1_1)
& val(c28490,salim_0)
& attr(c28496,c28497)
& sub(c28496,mensch_1_1)
& sub(c28497,familiename_1_1)
& val(c28497,mugabe_0)
& attr(c28502,c28503)
& sub(c28502,stadt__1_1)
& sub(c28503,name_1_1)
& val(c28503,pretoria_0)
& quant_p3(c28511,c28504,stunde_1_1)
& subs(c28514,krise_1_1)
& attr(c28534,c28535)
& sub(c28534,land_1_1)
& sub(c28535,name_1_1)
& val(c28535,lesotho_0)
& assoc(generalsekretaer_1_1,allgemein_1_1)
& sub(generalsekretaer_1_1,sekret__344r_1_1)
& sort(c28444,d)
& card(c28444,int1)
& etype(c28444,int0)
& fact(c28444,real)
& gener(c28444,sp)
& quant(c28444,one)
& refer(c28444,det)
& varia(c28444,con)
& sort(c28445,na)
& card(c28445,int1)
& etype(c28445,int0)
& fact(c28445,real)
& gener(c28445,sp)
& quant(c28445,one)
& refer(c28445,indet)
& varia(c28445,varia_c)
& sort(c28446,na)
& card(c28446,int1)
& etype(c28446,int0)
& fact(c28446,real)
& gener(c28446,sp)
& quant(c28446,one)
& refer(c28446,indet)
& varia(c28446,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(c28457,d)
& sort(c28457,io)
& card(c28457,int1)
& etype(c28457,int0)
& fact(c28457,real)
& gener(c28457,sp)
& quant(c28457,one)
& refer(c28457,det)
& varia(c28457,con)
& sort(c28458,na)
& card(c28458,int1)
& etype(c28458,int0)
& fact(c28458,real)
& gener(c28458,sp)
& quant(c28458,one)
& refer(c28458,indet)
& varia(c28458,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(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(botswana_0,fe)
& sort(c28459,o)
& card(c28459,int1)
& etype(c28459,int0)
& fact(c28459,real)
& gener(c28459,gener_c)
& quant(c28459,one)
& refer(c28459,refer_c)
& varia(c28459,varia_c)
& sort(quett_1_1,o)
& card(quett_1_1,int1)
& etype(quett_1_1,int0)
& fact(quett_1_1,real)
& gener(quett_1_1,ge)
& quant(quett_1_1,one)
& refer(quett_1_1,refer_c)
& varia(quett_1_1,varia_c)
& sort(c28460,o)
& card(c28460,int1)
& etype(c28460,int0)
& fact(c28460,real)
& gener(c28460,gener_c)
& quant(c28460,one)
& refer(c28460,refer_c)
& varia(c28460,varia_c)
& sort(masire_1_1,o)
& card(masire_1_1,int1)
& etype(masire_1_1,int0)
& fact(masire_1_1,real)
& gener(masire_1_1,ge)
& quant(masire_1_1,one)
& refer(masire_1_1,refer_c)
& varia(masire_1_1,varia_c)
& sort(c28468,d)
& card(c28468,int1)
& etype(c28468,int0)
& fact(c28468,real)
& gener(c28468,sp)
& quant(c28468,one)
& refer(c28468,det)
& varia(c28468,con)
& sort(generalsekretaer_1_1,d)
& card(generalsekretaer_1_1,int1)
& etype(generalsekretaer_1_1,int0)
& fact(generalsekretaer_1_1,real)
& gener(generalsekretaer_1_1,ge)
& quant(generalsekretaer_1_1,one)
& refer(generalsekretaer_1_1,refer_c)
& varia(generalsekretaer_1_1,varia_c)
& sort(c28473,d)
& sort(c28473,io)
& card(c28473,int1)
& etype(c28473,int1)
& fact(c28473,real)
& gener(c28473,sp)
& quant(c28473,one)
& refer(c28473,det)
& varia(c28473,con)
& sort(organisation_1_1,d)
& sort(organisation_1_1,io)
& card(organisation_1_1,card_c)
& etype(organisation_1_1,int1)
& fact(organisation_1_1,real)
& gener(organisation_1_1,ge)
& quant(organisation_1_1,quant_c)
& refer(organisation_1_1,refer_c)
& varia(organisation_1_1,varia_c)
& sort(c28477,io)
& sort(c28477,oa)
& card(c28477,int1)
& etype(c28477,int0)
& fact(c28477,real)
& gener(c28477,gener_c)
& quant(c28477,one)
& refer(c28477,refer_c)
& varia(c28477,varia_c)
& sort(afrikanisch__1_1,nq)
& sort(einheit_1_1,io)
& sort(einheit_1_1,oa)
& card(einheit_1_1,int1)
& etype(einheit_1_1,int0)
& fact(einheit_1_1,real)
& gener(einheit_1_1,ge)
& quant(einheit_1_1,one)
& refer(einheit_1_1,refer_c)
& varia(einheit_1_1,varia_c)
& sort(c28487,d)
& card(c28487,int1)
& etype(c28487,int0)
& fact(c28487,real)
& gener(c28487,sp)
& quant(c28487,one)
& refer(c28487,det)
& varia(c28487,con)
& sort(c28488,na)
& card(c28488,int1)
& etype(c28488,int0)
& fact(c28488,real)
& gener(c28488,sp)
& quant(c28488,one)
& refer(c28488,indet)
& varia(c28488,varia_c)
& sort(c28490,na)
& card(c28490,int1)
& etype(c28490,int0)
& fact(c28490,real)
& gener(c28490,sp)
& quant(c28490,one)
& refer(c28490,indet)
& varia(c28490,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(c28489,fe)
& sort(salim_0,fe)
& sort(ahmed_0,fe)
& sort(c28496,d)
& card(c28496,int1)
& etype(c28496,int0)
& fact(c28496,real)
& gener(c28496,sp)
& quant(c28496,one)
& refer(c28496,det)
& varia(c28496,con)
& sort(c28497,na)
& card(c28497,int1)
& etype(c28497,int0)
& fact(c28497,real)
& gener(c28497,sp)
& quant(c28497,one)
& refer(c28497,indet)
& varia(c28497,varia_c)
& sort(mugabe_0,fe)
& sort(c28502,d)
& sort(c28502,io)
& card(c28502,int1)
& etype(c28502,int0)
& fact(c28502,real)
& gener(c28502,sp)
& quant(c28502,one)
& refer(c28502,det)
& varia(c28502,con)
& sort(c28503,na)
& card(c28503,int1)
& etype(c28503,int0)
& fact(c28503,real)
& gener(c28503,sp)
& quant(c28503,one)
& refer(c28503,indet)
& varia(c28503,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(pretoria_0,fe)
& sort(c28511,m)
& sort(c28511,ta)
& card(c28511,card_c)
& etype(c28511,etype_c)
& fact(c28511,real)
& gener(c28511,gener_c)
& quant(c28511,quant_c)
& refer(c28511,refer_c)
& varia(c28511,varia_c)
& sort(c28504,nu)
& card(c28504,int6)
& sort(stunde_1_1,me)
& sort(stunde_1_1,oa)
& sort(stunde_1_1,ta)
& card(stunde_1_1,card_c)
& etype(stunde_1_1,etype_c)
& fact(stunde_1_1,real)
& gener(stunde_1_1,ge)
& quant(stunde_1_1,quant_c)
& refer(stunde_1_1,refer_c)
& varia(stunde_1_1,varia_c)
& sort(c28514,ad)
& card(c28514,int1)
& etype(c28514,int0)
& fact(c28514,real)
& gener(c28514,sp)
& quant(c28514,one)
& refer(c28514,det)
& varia(c28514,con)
& sort(krise_1_1,ad)
& card(krise_1_1,int1)
& etype(krise_1_1,int0)
& fact(krise_1_1,real)
& gener(krise_1_1,ge)
& quant(krise_1_1,one)
& refer(krise_1_1,refer_c)
& varia(krise_1_1,varia_c)
& sort(c28534,d)
& sort(c28534,io)
& card(c28534,int1)
& etype(c28534,int0)
& fact(c28534,real)
& gener(c28534,sp)
& quant(c28534,one)
& refer(c28534,det)
& varia(c28534,con)
& sort(c28535,na)
& card(c28535,int1)
& etype(c28535,int0)
& fact(c28535,real)
& gener(c28535,sp)
& quant(c28535,one)
& refer(c28535,indet)
& varia(c28535,varia_c)
& sort(lesotho_0,fe)
& sort(c28553,ent)
& card(c28553,card_c)
& etype(c28553,etype_c)
& fact(c28553,real)
& gener(c28553,gener_c)
& quant(c28553,quant_c)
& refer(c28553,refer_c)
& varia(c28553,varia_c)
& sort(allgemein_1_1,tq)
& sort(sekret__344r_1_1,d)
& card(sekret__344r_1_1,int1)
& etype(sekret__344r_1_1,int0)
& fact(sekret__344r_1_1,real)
& gener(sekret__344r_1_1,ge)
& quant(sekret__344r_1_1,one)
& refer(sekret__344r_1_1,refer_c)
& varia(sekret__344r_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10192,plain,
( attr(c28444,c28445)
& attr(c28444,c28446)
& prop(c28444,s__374dafrikanisch_1_1)
& sub(c28444,pr__344sident_1_1)
& sub(c28445,eigenname_1_1)
& val(c28445,nelson_0)
& sub(c28446,familiename_1_1)
& val(c28446,mandela_0)
& attr(c28457,c28458)
& sub(c28457,land_1_1)
& sub(c28458,name_1_1)
& val(c28458,botswana_0)
& sub(c28459,quett_1_1)
& sub(c28460,masire_1_1)
& sub(c28468,generalsekretaer_1_1)
& attch(c28473,c28468)
& sub(c28473,organisation_1_1)
& attch(c28477,c28473)
& prop(c28477,afrikanisch__1_1)
& sub(c28477,einheit_1_1)
& attr(c28487,c28488)
& attr(c28487,c28490)
& sub(c28487,mensch_1_1)
& sub(c28488,eigenname_1_1)
& val(c28488,c28489)
& tupl(c28489,salim_0,ahmed_0)
& sub(c28490,familiename_1_1)
& val(c28490,salim_0)
& attr(c28496,c28497)
& sub(c28496,mensch_1_1)
& sub(c28497,familiename_1_1)
& val(c28497,mugabe_0)
& attr(c28502,c28503)
& sub(c28502,stadt__1_1)
& sub(c28503,name_1_1)
& val(c28503,pretoria_0)
& subs(c28514,krise_1_1)
& attr(c28534,c28535)
& sub(c28534,land_1_1)
& sub(c28535,name_1_1)
& val(c28535,lesotho_0)
& assoc(generalsekretaer_1_1,allgemein_1_1)
& sub(generalsekretaer_1_1,sekret__344r_1_1)
& sort(c28444,d)
& card(c28444,int1)
& etype(c28444,int0)
& fact(c28444,real)
& gener(c28444,sp)
& quant(c28444,one)
& refer(c28444,det)
& varia(c28444,con)
& sort(c28445,na)
& card(c28445,int1)
& etype(c28445,int0)
& fact(c28445,real)
& gener(c28445,sp)
& quant(c28445,one)
& refer(c28445,indet)
& varia(c28445,varia_c)
& sort(c28446,na)
& card(c28446,int1)
& etype(c28446,int0)
& fact(c28446,real)
& gener(c28446,sp)
& quant(c28446,one)
& refer(c28446,indet)
& varia(c28446,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(c28457,d)
& sort(c28457,io)
& card(c28457,int1)
& etype(c28457,int0)
& fact(c28457,real)
& gener(c28457,sp)
& quant(c28457,one)
& refer(c28457,det)
& varia(c28457,con)
& sort(c28458,na)
& card(c28458,int1)
& etype(c28458,int0)
& fact(c28458,real)
& gener(c28458,sp)
& quant(c28458,one)
& refer(c28458,indet)
& varia(c28458,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(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(botswana_0,fe)
& sort(c28459,o)
& card(c28459,int1)
& etype(c28459,int0)
& fact(c28459,real)
& gener(c28459,gener_c)
& quant(c28459,one)
& refer(c28459,refer_c)
& varia(c28459,varia_c)
& sort(quett_1_1,o)
& card(quett_1_1,int1)
& etype(quett_1_1,int0)
& fact(quett_1_1,real)
& gener(quett_1_1,ge)
& quant(quett_1_1,one)
& refer(quett_1_1,refer_c)
& varia(quett_1_1,varia_c)
& sort(c28460,o)
& card(c28460,int1)
& etype(c28460,int0)
& fact(c28460,real)
& gener(c28460,gener_c)
& quant(c28460,one)
& refer(c28460,refer_c)
& varia(c28460,varia_c)
& sort(masire_1_1,o)
& card(masire_1_1,int1)
& etype(masire_1_1,int0)
& fact(masire_1_1,real)
& gener(masire_1_1,ge)
& quant(masire_1_1,one)
& refer(masire_1_1,refer_c)
& varia(masire_1_1,varia_c)
& sort(c28468,d)
& card(c28468,int1)
& etype(c28468,int0)
& fact(c28468,real)
& gener(c28468,sp)
& quant(c28468,one)
& refer(c28468,det)
& varia(c28468,con)
& sort(generalsekretaer_1_1,d)
& card(generalsekretaer_1_1,int1)
& etype(generalsekretaer_1_1,int0)
& fact(generalsekretaer_1_1,real)
& gener(generalsekretaer_1_1,ge)
& quant(generalsekretaer_1_1,one)
& refer(generalsekretaer_1_1,refer_c)
& varia(generalsekretaer_1_1,varia_c)
& sort(c28473,d)
& sort(c28473,io)
& card(c28473,int1)
& etype(c28473,int1)
& fact(c28473,real)
& gener(c28473,sp)
& quant(c28473,one)
& refer(c28473,det)
& varia(c28473,con)
& sort(organisation_1_1,d)
& sort(organisation_1_1,io)
& card(organisation_1_1,card_c)
& etype(organisation_1_1,int1)
& fact(organisation_1_1,real)
& gener(organisation_1_1,ge)
& quant(organisation_1_1,quant_c)
& refer(organisation_1_1,refer_c)
& varia(organisation_1_1,varia_c)
& sort(c28477,io)
& sort(c28477,oa)
& card(c28477,int1)
& etype(c28477,int0)
& fact(c28477,real)
& gener(c28477,gener_c)
& quant(c28477,one)
& refer(c28477,refer_c)
& varia(c28477,varia_c)
& sort(afrikanisch__1_1,nq)
& sort(einheit_1_1,io)
& sort(einheit_1_1,oa)
& card(einheit_1_1,int1)
& etype(einheit_1_1,int0)
& fact(einheit_1_1,real)
& gener(einheit_1_1,ge)
& quant(einheit_1_1,one)
& refer(einheit_1_1,refer_c)
& varia(einheit_1_1,varia_c)
& sort(c28487,d)
& card(c28487,int1)
& etype(c28487,int0)
& fact(c28487,real)
& gener(c28487,sp)
& quant(c28487,one)
& refer(c28487,det)
& varia(c28487,con)
& sort(c28488,na)
& card(c28488,int1)
& etype(c28488,int0)
& fact(c28488,real)
& gener(c28488,sp)
& quant(c28488,one)
& refer(c28488,indet)
& varia(c28488,varia_c)
& sort(c28490,na)
& card(c28490,int1)
& etype(c28490,int0)
& fact(c28490,real)
& gener(c28490,sp)
& quant(c28490,one)
& refer(c28490,indet)
& varia(c28490,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(c28489,fe)
& sort(salim_0,fe)
& sort(ahmed_0,fe)
& sort(c28496,d)
& card(c28496,int1)
& etype(c28496,int0)
& fact(c28496,real)
& gener(c28496,sp)
& quant(c28496,one)
& refer(c28496,det)
& varia(c28496,con)
& sort(c28497,na)
& card(c28497,int1)
& etype(c28497,int0)
& fact(c28497,real)
& gener(c28497,sp)
& quant(c28497,one)
& refer(c28497,indet)
& varia(c28497,varia_c)
& sort(mugabe_0,fe)
& sort(c28502,d)
& sort(c28502,io)
& card(c28502,int1)
& etype(c28502,int0)
& fact(c28502,real)
& gener(c28502,sp)
& quant(c28502,one)
& refer(c28502,det)
& varia(c28502,con)
& sort(c28503,na)
& card(c28503,int1)
& etype(c28503,int0)
& fact(c28503,real)
& gener(c28503,sp)
& quant(c28503,one)
& refer(c28503,indet)
& varia(c28503,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(pretoria_0,fe)
& sort(c28511,m)
& sort(c28511,ta)
& card(c28511,card_c)
& etype(c28511,etype_c)
& fact(c28511,real)
& gener(c28511,gener_c)
& quant(c28511,quant_c)
& refer(c28511,refer_c)
& varia(c28511,varia_c)
& sort(c28504,nu)
& card(c28504,int6)
& sort(stunde_1_1,me)
& sort(stunde_1_1,oa)
& sort(stunde_1_1,ta)
& card(stunde_1_1,card_c)
& etype(stunde_1_1,etype_c)
& fact(stunde_1_1,real)
& gener(stunde_1_1,ge)
& quant(stunde_1_1,quant_c)
& refer(stunde_1_1,refer_c)
& varia(stunde_1_1,varia_c)
& sort(c28514,ad)
& card(c28514,int1)
& etype(c28514,int0)
& fact(c28514,real)
& gener(c28514,sp)
& quant(c28514,one)
& refer(c28514,det)
& varia(c28514,con)
& sort(krise_1_1,ad)
& card(krise_1_1,int1)
& etype(krise_1_1,int0)
& fact(krise_1_1,real)
& gener(krise_1_1,ge)
& quant(krise_1_1,one)
& refer(krise_1_1,refer_c)
& varia(krise_1_1,varia_c)
& sort(c28534,d)
& sort(c28534,io)
& card(c28534,int1)
& etype(c28534,int0)
& fact(c28534,real)
& gener(c28534,sp)
& quant(c28534,one)
& refer(c28534,det)
& varia(c28534,con)
& sort(c28535,na)
& card(c28535,int1)
& etype(c28535,int0)
& fact(c28535,real)
& gener(c28535,sp)
& quant(c28535,one)
& refer(c28535,indet)
& varia(c28535,varia_c)
& sort(lesotho_0,fe)
& sort(c28553,ent)
& card(c28553,card_c)
& etype(c28553,etype_c)
& fact(c28553,real)
& gener(c28553,gener_c)
& quant(c28553,quant_c)
& refer(c28553,refer_c)
& varia(c28553,varia_c)
& sort(allgemein_1_1,tq)
& sort(sekret__344r_1_1,d)
& card(sekret__344r_1_1,int1)
& etype(sekret__344r_1_1,int0)
& fact(sekret__344r_1_1,real)
& gener(sekret__344r_1_1,ge)
& quant(sekret__344r_1_1,one)
& refer(sekret__344r_1_1,refer_c)
& varia(sekret__344r_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10327,plain,
( attr(c28444,c28445)
& attr(c28444,c28446)
& prop(c28444,s__374dafrikanisch_1_1)
& sub(c28444,pr__344sident_1_1)
& sub(c28445,eigenname_1_1)
& val(c28445,nelson_0)
& sub(c28446,familiename_1_1)
& val(c28446,mandela_0)
& attr(c28457,c28458)
& sub(c28457,land_1_1)
& sub(c28458,name_1_1)
& val(c28458,botswana_0)
& sub(c28459,quett_1_1)
& sub(c28460,masire_1_1)
& sub(c28468,generalsekretaer_1_1)
& attch(c28473,c28468)
& sub(c28473,organisation_1_1)
& attch(c28477,c28473)
& prop(c28477,afrikanisch__1_1)
& sub(c28477,einheit_1_1)
& attr(c28487,c28488)
& attr(c28487,c28490)
& sub(c28487,mensch_1_1)
& sub(c28488,eigenname_1_1)
& val(c28488,c28489)
& tupl(c28489,salim_0,ahmed_0)
& sub(c28490,familiename_1_1)
& val(c28490,salim_0)
& attr(c28496,c28497)
& sub(c28496,mensch_1_1)
& sub(c28497,familiename_1_1)
& val(c28497,mugabe_0)
& attr(c28502,c28503)
& sub(c28502,stadt__1_1)
& sub(c28503,name_1_1)
& val(c28503,pretoria_0)
& subs(c28514,krise_1_1)
& attr(c28534,c28535)
& sub(c28534,land_1_1)
& sub(c28535,name_1_1)
& val(c28535,lesotho_0)
& assoc(generalsekretaer_1_1,allgemein_1_1)
& sub(generalsekretaer_1_1,sekret__344r_1_1)
& card(c28444,int1)
& etype(c28444,int0)
& fact(c28444,real)
& gener(c28444,sp)
& quant(c28444,one)
& refer(c28444,det)
& varia(c28444,con)
& card(c28445,int1)
& etype(c28445,int0)
& fact(c28445,real)
& gener(c28445,sp)
& quant(c28445,one)
& refer(c28445,indet)
& varia(c28445,varia_c)
& card(c28446,int1)
& etype(c28446,int0)
& fact(c28446,real)
& gener(c28446,sp)
& quant(c28446,one)
& refer(c28446,indet)
& varia(c28446,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(c28457,int1)
& etype(c28457,int0)
& fact(c28457,real)
& gener(c28457,sp)
& quant(c28457,one)
& refer(c28457,det)
& varia(c28457,con)
& card(c28458,int1)
& etype(c28458,int0)
& fact(c28458,real)
& gener(c28458,sp)
& quant(c28458,one)
& refer(c28458,indet)
& varia(c28458,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(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(c28459,int1)
& etype(c28459,int0)
& fact(c28459,real)
& gener(c28459,gener_c)
& quant(c28459,one)
& refer(c28459,refer_c)
& varia(c28459,varia_c)
& card(quett_1_1,int1)
& etype(quett_1_1,int0)
& fact(quett_1_1,real)
& gener(quett_1_1,ge)
& quant(quett_1_1,one)
& refer(quett_1_1,refer_c)
& varia(quett_1_1,varia_c)
& card(c28460,int1)
& etype(c28460,int0)
& fact(c28460,real)
& gener(c28460,gener_c)
& quant(c28460,one)
& refer(c28460,refer_c)
& varia(c28460,varia_c)
& card(masire_1_1,int1)
& etype(masire_1_1,int0)
& fact(masire_1_1,real)
& gener(masire_1_1,ge)
& quant(masire_1_1,one)
& refer(masire_1_1,refer_c)
& varia(masire_1_1,varia_c)
& card(c28468,int1)
& etype(c28468,int0)
& fact(c28468,real)
& gener(c28468,sp)
& quant(c28468,one)
& refer(c28468,det)
& varia(c28468,con)
& card(generalsekretaer_1_1,int1)
& etype(generalsekretaer_1_1,int0)
& fact(generalsekretaer_1_1,real)
& gener(generalsekretaer_1_1,ge)
& quant(generalsekretaer_1_1,one)
& refer(generalsekretaer_1_1,refer_c)
& varia(generalsekretaer_1_1,varia_c)
& card(c28473,int1)
& etype(c28473,int1)
& fact(c28473,real)
& gener(c28473,sp)
& quant(c28473,one)
& refer(c28473,det)
& varia(c28473,con)
& card(organisation_1_1,card_c)
& etype(organisation_1_1,int1)
& fact(organisation_1_1,real)
& gener(organisation_1_1,ge)
& quant(organisation_1_1,quant_c)
& refer(organisation_1_1,refer_c)
& varia(organisation_1_1,varia_c)
& card(c28477,int1)
& etype(c28477,int0)
& fact(c28477,real)
& gener(c28477,gener_c)
& quant(c28477,one)
& refer(c28477,refer_c)
& varia(c28477,varia_c)
& card(einheit_1_1,int1)
& etype(einheit_1_1,int0)
& fact(einheit_1_1,real)
& gener(einheit_1_1,ge)
& quant(einheit_1_1,one)
& refer(einheit_1_1,refer_c)
& varia(einheit_1_1,varia_c)
& card(c28487,int1)
& etype(c28487,int0)
& fact(c28487,real)
& gener(c28487,sp)
& quant(c28487,one)
& refer(c28487,det)
& varia(c28487,con)
& card(c28488,int1)
& etype(c28488,int0)
& fact(c28488,real)
& gener(c28488,sp)
& quant(c28488,one)
& refer(c28488,indet)
& varia(c28488,varia_c)
& card(c28490,int1)
& etype(c28490,int0)
& fact(c28490,real)
& gener(c28490,sp)
& quant(c28490,one)
& refer(c28490,indet)
& varia(c28490,varia_c)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& card(c28496,int1)
& etype(c28496,int0)
& fact(c28496,real)
& gener(c28496,sp)
& quant(c28496,one)
& refer(c28496,det)
& varia(c28496,con)
& card(c28497,int1)
& etype(c28497,int0)
& fact(c28497,real)
& gener(c28497,sp)
& quant(c28497,one)
& refer(c28497,indet)
& varia(c28497,varia_c)
& card(c28502,int1)
& etype(c28502,int0)
& fact(c28502,real)
& gener(c28502,sp)
& quant(c28502,one)
& refer(c28502,det)
& varia(c28502,con)
& card(c28503,int1)
& etype(c28503,int0)
& fact(c28503,real)
& gener(c28503,sp)
& quant(c28503,one)
& refer(c28503,indet)
& varia(c28503,varia_c)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& card(c28511,card_c)
& etype(c28511,etype_c)
& fact(c28511,real)
& gener(c28511,gener_c)
& quant(c28511,quant_c)
& refer(c28511,refer_c)
& varia(c28511,varia_c)
& card(c28504,int6)
& card(stunde_1_1,card_c)
& etype(stunde_1_1,etype_c)
& fact(stunde_1_1,real)
& gener(stunde_1_1,ge)
& quant(stunde_1_1,quant_c)
& refer(stunde_1_1,refer_c)
& varia(stunde_1_1,varia_c)
& card(c28514,int1)
& etype(c28514,int0)
& fact(c28514,real)
& gener(c28514,sp)
& quant(c28514,one)
& refer(c28514,det)
& varia(c28514,con)
& card(krise_1_1,int1)
& etype(krise_1_1,int0)
& fact(krise_1_1,real)
& gener(krise_1_1,ge)
& quant(krise_1_1,one)
& refer(krise_1_1,refer_c)
& varia(krise_1_1,varia_c)
& card(c28534,int1)
& etype(c28534,int0)
& fact(c28534,real)
& gener(c28534,sp)
& quant(c28534,one)
& refer(c28534,det)
& varia(c28534,con)
& card(c28535,int1)
& etype(c28535,int0)
& fact(c28535,real)
& gener(c28535,sp)
& quant(c28535,one)
& refer(c28535,indet)
& varia(c28535,varia_c)
& card(c28553,card_c)
& etype(c28553,etype_c)
& fact(c28553,real)
& gener(c28553,gener_c)
& quant(c28553,quant_c)
& refer(c28553,refer_c)
& varia(c28553,varia_c)
& card(sekret__344r_1_1,int1)
& etype(sekret__344r_1_1,int0)
& fact(sekret__344r_1_1,real)
& gener(sekret__344r_1_1,ge)
& quant(sekret__344r_1_1,one)
& refer(sekret__344r_1_1,refer_c)
& varia(sekret__344r_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10192]) ).
fof(f10330,plain,
( attr(c28444,c28445)
& attr(c28444,c28446)
& prop(c28444,s__374dafrikanisch_1_1)
& sub(c28444,pr__344sident_1_1)
& sub(c28445,eigenname_1_1)
& val(c28445,nelson_0)
& sub(c28446,familiename_1_1)
& val(c28446,mandela_0)
& attr(c28457,c28458)
& sub(c28457,land_1_1)
& sub(c28458,name_1_1)
& val(c28458,botswana_0)
& sub(c28459,quett_1_1)
& sub(c28460,masire_1_1)
& sub(c28468,generalsekretaer_1_1)
& attch(c28473,c28468)
& sub(c28473,organisation_1_1)
& attch(c28477,c28473)
& prop(c28477,afrikanisch__1_1)
& sub(c28477,einheit_1_1)
& attr(c28487,c28488)
& attr(c28487,c28490)
& sub(c28487,mensch_1_1)
& sub(c28488,eigenname_1_1)
& val(c28488,c28489)
& tupl(c28489,salim_0,ahmed_0)
& sub(c28490,familiename_1_1)
& val(c28490,salim_0)
& attr(c28496,c28497)
& sub(c28496,mensch_1_1)
& sub(c28497,familiename_1_1)
& val(c28497,mugabe_0)
& attr(c28502,c28503)
& sub(c28502,stadt__1_1)
& sub(c28503,name_1_1)
& val(c28503,pretoria_0)
& subs(c28514,krise_1_1)
& attr(c28534,c28535)
& sub(c28534,land_1_1)
& sub(c28535,name_1_1)
& val(c28535,lesotho_0)
& assoc(generalsekretaer_1_1,allgemein_1_1)
& sub(generalsekretaer_1_1,sekret__344r_1_1)
& card(c28444,int1)
& etype(c28444,int0)
& fact(c28444,real)
& gener(c28444,sp)
& refer(c28444,det)
& varia(c28444,con)
& card(c28445,int1)
& etype(c28445,int0)
& fact(c28445,real)
& gener(c28445,sp)
& refer(c28445,indet)
& varia(c28445,varia_c)
& card(c28446,int1)
& etype(c28446,int0)
& fact(c28446,real)
& gener(c28446,sp)
& refer(c28446,indet)
& varia(c28446,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(c28457,int1)
& etype(c28457,int0)
& fact(c28457,real)
& gener(c28457,sp)
& refer(c28457,det)
& varia(c28457,con)
& card(c28458,int1)
& etype(c28458,int0)
& fact(c28458,real)
& gener(c28458,sp)
& refer(c28458,indet)
& varia(c28458,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(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(c28459,int1)
& etype(c28459,int0)
& fact(c28459,real)
& gener(c28459,gener_c)
& refer(c28459,refer_c)
& varia(c28459,varia_c)
& card(quett_1_1,int1)
& etype(quett_1_1,int0)
& fact(quett_1_1,real)
& gener(quett_1_1,ge)
& refer(quett_1_1,refer_c)
& varia(quett_1_1,varia_c)
& card(c28460,int1)
& etype(c28460,int0)
& fact(c28460,real)
& gener(c28460,gener_c)
& refer(c28460,refer_c)
& varia(c28460,varia_c)
& card(masire_1_1,int1)
& etype(masire_1_1,int0)
& fact(masire_1_1,real)
& gener(masire_1_1,ge)
& refer(masire_1_1,refer_c)
& varia(masire_1_1,varia_c)
& card(c28468,int1)
& etype(c28468,int0)
& fact(c28468,real)
& gener(c28468,sp)
& refer(c28468,det)
& varia(c28468,con)
& card(generalsekretaer_1_1,int1)
& etype(generalsekretaer_1_1,int0)
& fact(generalsekretaer_1_1,real)
& gener(generalsekretaer_1_1,ge)
& refer(generalsekretaer_1_1,refer_c)
& varia(generalsekretaer_1_1,varia_c)
& card(c28473,int1)
& etype(c28473,int1)
& fact(c28473,real)
& gener(c28473,sp)
& refer(c28473,det)
& varia(c28473,con)
& card(organisation_1_1,card_c)
& etype(organisation_1_1,int1)
& fact(organisation_1_1,real)
& gener(organisation_1_1,ge)
& refer(organisation_1_1,refer_c)
& varia(organisation_1_1,varia_c)
& card(c28477,int1)
& etype(c28477,int0)
& fact(c28477,real)
& gener(c28477,gener_c)
& refer(c28477,refer_c)
& varia(c28477,varia_c)
& card(einheit_1_1,int1)
& etype(einheit_1_1,int0)
& fact(einheit_1_1,real)
& gener(einheit_1_1,ge)
& refer(einheit_1_1,refer_c)
& varia(einheit_1_1,varia_c)
& card(c28487,int1)
& etype(c28487,int0)
& fact(c28487,real)
& gener(c28487,sp)
& refer(c28487,det)
& varia(c28487,con)
& card(c28488,int1)
& etype(c28488,int0)
& fact(c28488,real)
& gener(c28488,sp)
& refer(c28488,indet)
& varia(c28488,varia_c)
& card(c28490,int1)
& etype(c28490,int0)
& fact(c28490,real)
& gener(c28490,sp)
& refer(c28490,indet)
& varia(c28490,varia_c)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& card(c28496,int1)
& etype(c28496,int0)
& fact(c28496,real)
& gener(c28496,sp)
& refer(c28496,det)
& varia(c28496,con)
& card(c28497,int1)
& etype(c28497,int0)
& fact(c28497,real)
& gener(c28497,sp)
& refer(c28497,indet)
& varia(c28497,varia_c)
& card(c28502,int1)
& etype(c28502,int0)
& fact(c28502,real)
& gener(c28502,sp)
& refer(c28502,det)
& varia(c28502,con)
& card(c28503,int1)
& etype(c28503,int0)
& fact(c28503,real)
& gener(c28503,sp)
& refer(c28503,indet)
& varia(c28503,varia_c)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& card(c28511,card_c)
& etype(c28511,etype_c)
& fact(c28511,real)
& gener(c28511,gener_c)
& refer(c28511,refer_c)
& varia(c28511,varia_c)
& card(c28504,int6)
& card(stunde_1_1,card_c)
& etype(stunde_1_1,etype_c)
& fact(stunde_1_1,real)
& gener(stunde_1_1,ge)
& refer(stunde_1_1,refer_c)
& varia(stunde_1_1,varia_c)
& card(c28514,int1)
& etype(c28514,int0)
& fact(c28514,real)
& gener(c28514,sp)
& refer(c28514,det)
& varia(c28514,con)
& card(krise_1_1,int1)
& etype(krise_1_1,int0)
& fact(krise_1_1,real)
& gener(krise_1_1,ge)
& refer(krise_1_1,refer_c)
& varia(krise_1_1,varia_c)
& card(c28534,int1)
& etype(c28534,int0)
& fact(c28534,real)
& gener(c28534,sp)
& refer(c28534,det)
& varia(c28534,con)
& card(c28535,int1)
& etype(c28535,int0)
& fact(c28535,real)
& gener(c28535,sp)
& refer(c28535,indet)
& varia(c28535,varia_c)
& card(c28553,card_c)
& etype(c28553,etype_c)
& fact(c28553,real)
& gener(c28553,gener_c)
& refer(c28553,refer_c)
& varia(c28553,varia_c)
& card(sekret__344r_1_1,int1)
& etype(sekret__344r_1_1,int0)
& fact(sekret__344r_1_1,real)
& gener(sekret__344r_1_1,ge)
& refer(sekret__344r_1_1,refer_c)
& varia(sekret__344r_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10327]) ).
fof(f10333,plain,
( attr(c28444,c28445)
& attr(c28444,c28446)
& prop(c28444,s__374dafrikanisch_1_1)
& sub(c28444,pr__344sident_1_1)
& sub(c28445,eigenname_1_1)
& val(c28445,nelson_0)
& sub(c28446,familiename_1_1)
& val(c28446,mandela_0)
& attr(c28457,c28458)
& sub(c28457,land_1_1)
& sub(c28458,name_1_1)
& val(c28458,botswana_0)
& sub(c28459,quett_1_1)
& sub(c28460,masire_1_1)
& sub(c28468,generalsekretaer_1_1)
& attch(c28473,c28468)
& sub(c28473,organisation_1_1)
& attch(c28477,c28473)
& prop(c28477,afrikanisch__1_1)
& sub(c28477,einheit_1_1)
& attr(c28487,c28488)
& attr(c28487,c28490)
& sub(c28487,mensch_1_1)
& sub(c28488,eigenname_1_1)
& val(c28488,c28489)
& tupl(c28489,salim_0,ahmed_0)
& sub(c28490,familiename_1_1)
& val(c28490,salim_0)
& attr(c28496,c28497)
& sub(c28496,mensch_1_1)
& sub(c28497,familiename_1_1)
& val(c28497,mugabe_0)
& attr(c28502,c28503)
& sub(c28502,stadt__1_1)
& sub(c28503,name_1_1)
& val(c28503,pretoria_0)
& subs(c28514,krise_1_1)
& attr(c28534,c28535)
& sub(c28534,land_1_1)
& sub(c28535,name_1_1)
& val(c28535,lesotho_0)
& assoc(generalsekretaer_1_1,allgemein_1_1)
& sub(generalsekretaer_1_1,sekret__344r_1_1)
& etype(c28444,int0)
& fact(c28444,real)
& gener(c28444,sp)
& refer(c28444,det)
& varia(c28444,con)
& etype(c28445,int0)
& fact(c28445,real)
& gener(c28445,sp)
& refer(c28445,indet)
& varia(c28445,varia_c)
& etype(c28446,int0)
& fact(c28446,real)
& gener(c28446,sp)
& refer(c28446,indet)
& varia(c28446,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(c28457,int0)
& fact(c28457,real)
& gener(c28457,sp)
& refer(c28457,det)
& varia(c28457,con)
& etype(c28458,int0)
& fact(c28458,real)
& gener(c28458,sp)
& refer(c28458,indet)
& varia(c28458,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(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(c28459,int0)
& fact(c28459,real)
& gener(c28459,gener_c)
& refer(c28459,refer_c)
& varia(c28459,varia_c)
& etype(quett_1_1,int0)
& fact(quett_1_1,real)
& gener(quett_1_1,ge)
& refer(quett_1_1,refer_c)
& varia(quett_1_1,varia_c)
& etype(c28460,int0)
& fact(c28460,real)
& gener(c28460,gener_c)
& refer(c28460,refer_c)
& varia(c28460,varia_c)
& etype(masire_1_1,int0)
& fact(masire_1_1,real)
& gener(masire_1_1,ge)
& refer(masire_1_1,refer_c)
& varia(masire_1_1,varia_c)
& etype(c28468,int0)
& fact(c28468,real)
& gener(c28468,sp)
& refer(c28468,det)
& varia(c28468,con)
& etype(generalsekretaer_1_1,int0)
& fact(generalsekretaer_1_1,real)
& gener(generalsekretaer_1_1,ge)
& refer(generalsekretaer_1_1,refer_c)
& varia(generalsekretaer_1_1,varia_c)
& etype(c28473,int1)
& fact(c28473,real)
& gener(c28473,sp)
& refer(c28473,det)
& varia(c28473,con)
& etype(organisation_1_1,int1)
& fact(organisation_1_1,real)
& gener(organisation_1_1,ge)
& refer(organisation_1_1,refer_c)
& varia(organisation_1_1,varia_c)
& etype(c28477,int0)
& fact(c28477,real)
& gener(c28477,gener_c)
& refer(c28477,refer_c)
& varia(c28477,varia_c)
& etype(einheit_1_1,int0)
& fact(einheit_1_1,real)
& gener(einheit_1_1,ge)
& refer(einheit_1_1,refer_c)
& varia(einheit_1_1,varia_c)
& etype(c28487,int0)
& fact(c28487,real)
& gener(c28487,sp)
& refer(c28487,det)
& varia(c28487,con)
& etype(c28488,int0)
& fact(c28488,real)
& gener(c28488,sp)
& refer(c28488,indet)
& varia(c28488,varia_c)
& etype(c28490,int0)
& fact(c28490,real)
& gener(c28490,sp)
& refer(c28490,indet)
& varia(c28490,varia_c)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& etype(c28496,int0)
& fact(c28496,real)
& gener(c28496,sp)
& refer(c28496,det)
& varia(c28496,con)
& etype(c28497,int0)
& fact(c28497,real)
& gener(c28497,sp)
& refer(c28497,indet)
& varia(c28497,varia_c)
& etype(c28502,int0)
& fact(c28502,real)
& gener(c28502,sp)
& refer(c28502,det)
& varia(c28502,con)
& etype(c28503,int0)
& fact(c28503,real)
& gener(c28503,sp)
& refer(c28503,indet)
& varia(c28503,varia_c)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& etype(c28511,etype_c)
& fact(c28511,real)
& gener(c28511,gener_c)
& refer(c28511,refer_c)
& varia(c28511,varia_c)
& etype(stunde_1_1,etype_c)
& fact(stunde_1_1,real)
& gener(stunde_1_1,ge)
& refer(stunde_1_1,refer_c)
& varia(stunde_1_1,varia_c)
& etype(c28514,int0)
& fact(c28514,real)
& gener(c28514,sp)
& refer(c28514,det)
& varia(c28514,con)
& etype(krise_1_1,int0)
& fact(krise_1_1,real)
& gener(krise_1_1,ge)
& refer(krise_1_1,refer_c)
& varia(krise_1_1,varia_c)
& etype(c28534,int0)
& fact(c28534,real)
& gener(c28534,sp)
& refer(c28534,det)
& varia(c28534,con)
& etype(c28535,int0)
& fact(c28535,real)
& gener(c28535,sp)
& refer(c28535,indet)
& varia(c28535,varia_c)
& etype(c28553,etype_c)
& fact(c28553,real)
& gener(c28553,gener_c)
& refer(c28553,refer_c)
& varia(c28553,varia_c)
& etype(sekret__344r_1_1,int0)
& fact(sekret__344r_1_1,real)
& gener(sekret__344r_1_1,ge)
& refer(sekret__344r_1_1,refer_c)
& varia(sekret__344r_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10330]) ).
fof(f10336,plain,
( attr(c28444,c28445)
& attr(c28444,c28446)
& prop(c28444,s__374dafrikanisch_1_1)
& sub(c28444,pr__344sident_1_1)
& sub(c28445,eigenname_1_1)
& val(c28445,nelson_0)
& sub(c28446,familiename_1_1)
& val(c28446,mandela_0)
& attr(c28457,c28458)
& sub(c28457,land_1_1)
& sub(c28458,name_1_1)
& val(c28458,botswana_0)
& sub(c28459,quett_1_1)
& sub(c28460,masire_1_1)
& sub(c28468,generalsekretaer_1_1)
& attch(c28473,c28468)
& sub(c28473,organisation_1_1)
& attch(c28477,c28473)
& prop(c28477,afrikanisch__1_1)
& sub(c28477,einheit_1_1)
& attr(c28487,c28488)
& attr(c28487,c28490)
& sub(c28487,mensch_1_1)
& sub(c28488,eigenname_1_1)
& val(c28488,c28489)
& tupl(c28489,salim_0,ahmed_0)
& sub(c28490,familiename_1_1)
& val(c28490,salim_0)
& attr(c28496,c28497)
& sub(c28496,mensch_1_1)
& sub(c28497,familiename_1_1)
& val(c28497,mugabe_0)
& attr(c28502,c28503)
& sub(c28502,stadt__1_1)
& sub(c28503,name_1_1)
& val(c28503,pretoria_0)
& subs(c28514,krise_1_1)
& attr(c28534,c28535)
& sub(c28534,land_1_1)
& sub(c28535,name_1_1)
& val(c28535,lesotho_0)
& assoc(generalsekretaer_1_1,allgemein_1_1)
& sub(generalsekretaer_1_1,sekret__344r_1_1)
& etype(c28444,int0)
& fact(c28444,real)
& gener(c28444,sp)
& varia(c28444,con)
& etype(c28445,int0)
& fact(c28445,real)
& gener(c28445,sp)
& varia(c28445,varia_c)
& etype(c28446,int0)
& fact(c28446,real)
& gener(c28446,sp)
& varia(c28446,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(c28457,int0)
& fact(c28457,real)
& gener(c28457,sp)
& varia(c28457,con)
& etype(c28458,int0)
& fact(c28458,real)
& gener(c28458,sp)
& varia(c28458,varia_c)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& varia(land_1_1,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& varia(name_1_1,varia_c)
& etype(c28459,int0)
& fact(c28459,real)
& gener(c28459,gener_c)
& varia(c28459,varia_c)
& etype(quett_1_1,int0)
& fact(quett_1_1,real)
& gener(quett_1_1,ge)
& varia(quett_1_1,varia_c)
& etype(c28460,int0)
& fact(c28460,real)
& gener(c28460,gener_c)
& varia(c28460,varia_c)
& etype(masire_1_1,int0)
& fact(masire_1_1,real)
& gener(masire_1_1,ge)
& varia(masire_1_1,varia_c)
& etype(c28468,int0)
& fact(c28468,real)
& gener(c28468,sp)
& varia(c28468,con)
& etype(generalsekretaer_1_1,int0)
& fact(generalsekretaer_1_1,real)
& gener(generalsekretaer_1_1,ge)
& varia(generalsekretaer_1_1,varia_c)
& etype(c28473,int1)
& fact(c28473,real)
& gener(c28473,sp)
& varia(c28473,con)
& etype(organisation_1_1,int1)
& fact(organisation_1_1,real)
& gener(organisation_1_1,ge)
& varia(organisation_1_1,varia_c)
& etype(c28477,int0)
& fact(c28477,real)
& gener(c28477,gener_c)
& varia(c28477,varia_c)
& etype(einheit_1_1,int0)
& fact(einheit_1_1,real)
& gener(einheit_1_1,ge)
& varia(einheit_1_1,varia_c)
& etype(c28487,int0)
& fact(c28487,real)
& gener(c28487,sp)
& varia(c28487,con)
& etype(c28488,int0)
& fact(c28488,real)
& gener(c28488,sp)
& varia(c28488,varia_c)
& etype(c28490,int0)
& fact(c28490,real)
& gener(c28490,sp)
& varia(c28490,varia_c)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& varia(mensch_1_1,varia_c)
& etype(c28496,int0)
& fact(c28496,real)
& gener(c28496,sp)
& varia(c28496,con)
& etype(c28497,int0)
& fact(c28497,real)
& gener(c28497,sp)
& varia(c28497,varia_c)
& etype(c28502,int0)
& fact(c28502,real)
& gener(c28502,sp)
& varia(c28502,con)
& etype(c28503,int0)
& fact(c28503,real)
& gener(c28503,sp)
& varia(c28503,varia_c)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& varia(stadt__1_1,varia_c)
& etype(c28511,etype_c)
& fact(c28511,real)
& gener(c28511,gener_c)
& varia(c28511,varia_c)
& etype(stunde_1_1,etype_c)
& fact(stunde_1_1,real)
& gener(stunde_1_1,ge)
& varia(stunde_1_1,varia_c)
& etype(c28514,int0)
& fact(c28514,real)
& gener(c28514,sp)
& varia(c28514,con)
& etype(krise_1_1,int0)
& fact(krise_1_1,real)
& gener(krise_1_1,ge)
& varia(krise_1_1,varia_c)
& etype(c28534,int0)
& fact(c28534,real)
& gener(c28534,sp)
& varia(c28534,con)
& etype(c28535,int0)
& fact(c28535,real)
& gener(c28535,sp)
& varia(c28535,varia_c)
& etype(c28553,etype_c)
& fact(c28553,real)
& gener(c28553,gener_c)
& varia(c28553,varia_c)
& etype(sekret__344r_1_1,int0)
& fact(sekret__344r_1_1,real)
& gener(sekret__344r_1_1,ge)
& varia(sekret__344r_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10333]) ).
fof(f10341,plain,
( attr(c28444,c28445)
& attr(c28444,c28446)
& prop(c28444,s__374dafrikanisch_1_1)
& sub(c28444,pr__344sident_1_1)
& sub(c28445,eigenname_1_1)
& val(c28445,nelson_0)
& sub(c28446,familiename_1_1)
& val(c28446,mandela_0)
& attr(c28457,c28458)
& sub(c28457,land_1_1)
& sub(c28458,name_1_1)
& val(c28458,botswana_0)
& sub(c28459,quett_1_1)
& sub(c28460,masire_1_1)
& sub(c28468,generalsekretaer_1_1)
& attch(c28473,c28468)
& sub(c28473,organisation_1_1)
& attch(c28477,c28473)
& prop(c28477,afrikanisch__1_1)
& sub(c28477,einheit_1_1)
& attr(c28487,c28488)
& attr(c28487,c28490)
& sub(c28487,mensch_1_1)
& sub(c28488,eigenname_1_1)
& val(c28488,c28489)
& tupl(c28489,salim_0,ahmed_0)
& sub(c28490,familiename_1_1)
& val(c28490,salim_0)
& attr(c28496,c28497)
& sub(c28496,mensch_1_1)
& sub(c28497,familiename_1_1)
& val(c28497,mugabe_0)
& attr(c28502,c28503)
& sub(c28502,stadt__1_1)
& sub(c28503,name_1_1)
& val(c28503,pretoria_0)
& subs(c28514,krise_1_1)
& attr(c28534,c28535)
& sub(c28534,land_1_1)
& sub(c28535,name_1_1)
& val(c28535,lesotho_0)
& assoc(generalsekretaer_1_1,allgemein_1_1)
& sub(generalsekretaer_1_1,sekret__344r_1_1)
& etype(c28444,int0)
& fact(c28444,real)
& gener(c28444,sp)
& etype(c28445,int0)
& fact(c28445,real)
& gener(c28445,sp)
& etype(c28446,int0)
& fact(c28446,real)
& gener(c28446,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(c28457,int0)
& fact(c28457,real)
& gener(c28457,sp)
& etype(c28458,int0)
& fact(c28458,real)
& gener(c28458,sp)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& etype(c28459,int0)
& fact(c28459,real)
& gener(c28459,gener_c)
& etype(quett_1_1,int0)
& fact(quett_1_1,real)
& gener(quett_1_1,ge)
& etype(c28460,int0)
& fact(c28460,real)
& gener(c28460,gener_c)
& etype(masire_1_1,int0)
& fact(masire_1_1,real)
& gener(masire_1_1,ge)
& etype(c28468,int0)
& fact(c28468,real)
& gener(c28468,sp)
& etype(generalsekretaer_1_1,int0)
& fact(generalsekretaer_1_1,real)
& gener(generalsekretaer_1_1,ge)
& etype(c28473,int1)
& fact(c28473,real)
& gener(c28473,sp)
& etype(organisation_1_1,int1)
& fact(organisation_1_1,real)
& gener(organisation_1_1,ge)
& etype(c28477,int0)
& fact(c28477,real)
& gener(c28477,gener_c)
& etype(einheit_1_1,int0)
& fact(einheit_1_1,real)
& gener(einheit_1_1,ge)
& etype(c28487,int0)
& fact(c28487,real)
& gener(c28487,sp)
& etype(c28488,int0)
& fact(c28488,real)
& gener(c28488,sp)
& etype(c28490,int0)
& fact(c28490,real)
& gener(c28490,sp)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& etype(c28496,int0)
& fact(c28496,real)
& gener(c28496,sp)
& etype(c28497,int0)
& fact(c28497,real)
& gener(c28497,sp)
& etype(c28502,int0)
& fact(c28502,real)
& gener(c28502,sp)
& etype(c28503,int0)
& fact(c28503,real)
& gener(c28503,sp)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& etype(c28511,etype_c)
& fact(c28511,real)
& gener(c28511,gener_c)
& etype(stunde_1_1,etype_c)
& fact(stunde_1_1,real)
& gener(stunde_1_1,ge)
& etype(c28514,int0)
& fact(c28514,real)
& gener(c28514,sp)
& etype(krise_1_1,int0)
& fact(krise_1_1,real)
& gener(krise_1_1,ge)
& etype(c28534,int0)
& fact(c28534,real)
& gener(c28534,sp)
& etype(c28535,int0)
& fact(c28535,real)
& gener(c28535,sp)
& etype(c28553,etype_c)
& fact(c28553,real)
& gener(c28553,gener_c)
& etype(sekret__344r_1_1,int0)
& fact(sekret__344r_1_1,real)
& gener(sekret__344r_1_1,ge) ),
inference(pure_predicate_removal,[],[f10336]) ).
fof(f10346,plain,
( attr(c28444,c28445)
& attr(c28444,c28446)
& prop(c28444,s__374dafrikanisch_1_1)
& sub(c28444,pr__344sident_1_1)
& sub(c28445,eigenname_1_1)
& val(c28445,nelson_0)
& sub(c28446,familiename_1_1)
& val(c28446,mandela_0)
& attr(c28457,c28458)
& sub(c28457,land_1_1)
& sub(c28458,name_1_1)
& val(c28458,botswana_0)
& sub(c28459,quett_1_1)
& sub(c28460,masire_1_1)
& sub(c28468,generalsekretaer_1_1)
& attch(c28473,c28468)
& sub(c28473,organisation_1_1)
& attch(c28477,c28473)
& prop(c28477,afrikanisch__1_1)
& sub(c28477,einheit_1_1)
& attr(c28487,c28488)
& attr(c28487,c28490)
& sub(c28487,mensch_1_1)
& sub(c28488,eigenname_1_1)
& val(c28488,c28489)
& tupl(c28489,salim_0,ahmed_0)
& sub(c28490,familiename_1_1)
& val(c28490,salim_0)
& attr(c28496,c28497)
& sub(c28496,mensch_1_1)
& sub(c28497,familiename_1_1)
& val(c28497,mugabe_0)
& attr(c28502,c28503)
& sub(c28502,stadt__1_1)
& sub(c28503,name_1_1)
& val(c28503,pretoria_0)
& subs(c28514,krise_1_1)
& attr(c28534,c28535)
& sub(c28534,land_1_1)
& sub(c28535,name_1_1)
& val(c28535,lesotho_0)
& assoc(generalsekretaer_1_1,allgemein_1_1)
& sub(generalsekretaer_1_1,sekret__344r_1_1)
& etype(c28444,int0)
& fact(c28444,real)
& etype(c28445,int0)
& fact(c28445,real)
& etype(c28446,int0)
& fact(c28446,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(c28457,int0)
& fact(c28457,real)
& etype(c28458,int0)
& fact(c28458,real)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& etype(c28459,int0)
& fact(c28459,real)
& etype(quett_1_1,int0)
& fact(quett_1_1,real)
& etype(c28460,int0)
& fact(c28460,real)
& etype(masire_1_1,int0)
& fact(masire_1_1,real)
& etype(c28468,int0)
& fact(c28468,real)
& etype(generalsekretaer_1_1,int0)
& fact(generalsekretaer_1_1,real)
& etype(c28473,int1)
& fact(c28473,real)
& etype(organisation_1_1,int1)
& fact(organisation_1_1,real)
& etype(c28477,int0)
& fact(c28477,real)
& etype(einheit_1_1,int0)
& fact(einheit_1_1,real)
& etype(c28487,int0)
& fact(c28487,real)
& etype(c28488,int0)
& fact(c28488,real)
& etype(c28490,int0)
& fact(c28490,real)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& etype(c28496,int0)
& fact(c28496,real)
& etype(c28497,int0)
& fact(c28497,real)
& etype(c28502,int0)
& fact(c28502,real)
& etype(c28503,int0)
& fact(c28503,real)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& etype(c28511,etype_c)
& fact(c28511,real)
& etype(stunde_1_1,etype_c)
& fact(stunde_1_1,real)
& etype(c28514,int0)
& fact(c28514,real)
& etype(krise_1_1,int0)
& fact(krise_1_1,real)
& etype(c28534,int0)
& fact(c28534,real)
& etype(c28535,int0)
& fact(c28535,real)
& etype(c28553,etype_c)
& fact(c28553,real)
& etype(sekret__344r_1_1,int0)
& fact(sekret__344r_1_1,real) ),
inference(pure_predicate_removal,[],[f10341]) ).
fof(f10508,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(f10509,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,[],[f10508]) ).
fof(f10518,plain,
! [X0,X1,X2] :
( ? [X3] :
( mcont(X3,X2)
& obj(X3,X2)
& scar(X3,X2)
& subs(X3,stehen_1_b) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f160]) ).
fof(f10519,plain,
! [X0,X1,X2] :
( ? [X3] :
( mcont(X3,X2)
& obj(X3,X2)
& scar(X3,X2)
& subs(X3,stehen_1_b) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(flattening,[],[f10518]) ).
fof(f10522,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(f10523,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,[],[f10522]) ).
fof(f10524,plain,
! [X0,X1] :
( ? [X2] :
( arg1(X2,X0)
& arg2(X2,X1)
& subr(X2,sub_0) )
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f163]) ).
fof(f10553,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(f10554,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[],[f1]) ).
fof(f10806,plain,
! [X2,X0,X1] :
( ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2)
| val(sK48(X0,X2),X2) ),
inference(cnf_transformation,[],[f10509]) ).
fof(f10807,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| sub(sK48(X0,X2),name_1_1) ),
inference(cnf_transformation,[],[f10509]) ).
fof(f10810,plain,
! [X2,X0,X1] :
( ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2)
| attr(sK47(X0,X2),sK48(X0,X2)) ),
inference(cnf_transformation,[],[f10509]) ).
fof(f10811,plain,
! [X2,X0,X1] :
( ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2)
| in(sK49(X0,X2),sK47(X0,X2)) ),
inference(cnf_transformation,[],[f10509]) ).
fof(f10820,plain,
! [X2,X0,X1] :
( ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0)
| obj(sK51(X2),X2) ),
inference(cnf_transformation,[],[f10519]) ).
fof(f10830,plain,
! [X2,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| subr(sK55(X0,X1,X2),rprs_0) ),
inference(cnf_transformation,[],[f10523]) ).
fof(f10831,plain,
! [X2,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| sub(sK56(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f10523]) ).
fof(f10835,plain,
! [X2,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| arg2(sK55(X0,X1,X2),sK56(X0,X1,X2)) ),
inference(cnf_transformation,[],[f10523]) ).
fof(f10836,plain,
! [X2,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| arg1(sK55(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f10523]) ).
fof(f10837,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| subr(sK57(X0,X1),sub_0) ),
inference(cnf_transformation,[],[f10524]) ).
fof(f10838,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| arg2(sK57(X0,X1),X1) ),
inference(cnf_transformation,[],[f10524]) ).
fof(f10839,plain,
! [X0,X1] :
( ~ sub(X0,X1)
| arg1(sK57(X0,X1),X0) ),
inference(cnf_transformation,[],[f10524]) ).
fof(f19744,plain,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
inference(cnf_transformation,[],[f9161]) ).
fof(f20771,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ val(X7,s__374dafrika_0)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(X3,rprs_0)
| ~ sub(X7,name_1_1)
| ~ sub(X4,X9)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X8,X0)
| ~ attr(X6,X7)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ~ in(X5,X6) ),
inference(cnf_transformation,[],[f10553]) ).
fof(f20881,plain,
val(c28446,mandela_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20882,plain,
sub(c28446,familiename_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20883,plain,
val(c28445,nelson_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20884,plain,
sub(c28445,eigenname_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20885,plain,
sub(c28444,pr__344sident_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20886,plain,
prop(c28444,s__374dafrikanisch_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20887,plain,
attr(c28444,c28446),
inference(cnf_transformation,[],[f10346]) ).
fof(f20888,plain,
attr(c28444,c28445),
inference(cnf_transformation,[],[f10346]) ).
fof(f21064,plain,
! [X2,X0,X1] :
( ~ sub(sK48(X0,X2),name_1_1)
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(consistent_polarity_flipping,[],[f10807]) ).
fof(f21072,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| sub(X0,X1)
| ~ attr(X2,X0)
| obj(sK51(X2),X2) ),
inference(consistent_polarity_flipping,[],[f10820]) ).
fof(f21077,plain,
! [X2,X0,X1] :
( arg1(sK55(X0,X1,X2),X1)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| subr(X0,sub_0) ),
inference(consistent_polarity_flipping,[],[f10836]) ).
fof(f21078,plain,
! [X2,X0,X1] :
( arg2(sK55(X0,X1,X2),sK56(X0,X1,X2))
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| subr(X0,sub_0) ),
inference(consistent_polarity_flipping,[],[f10835]) ).
fof(f21082,plain,
! [X2,X0,X1] :
( ~ sub(sK56(X0,X1,X2),X2)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| subr(X0,sub_0) ),
inference(consistent_polarity_flipping,[],[f10831]) ).
fof(f21083,plain,
! [X2,X0,X1] :
( ~ subr(sK55(X0,X1,X2),rprs_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| subr(X0,sub_0) ),
inference(consistent_polarity_flipping,[],[f10830]) ).
fof(f21085,plain,
! [X0,X1] :
( arg1(sK57(X0,X1),X0)
| sub(X0,X1) ),
inference(consistent_polarity_flipping,[],[f10839]) ).
fof(f21086,plain,
! [X0,X1] :
( arg2(sK57(X0,X1),X1)
| sub(X0,X1) ),
inference(consistent_polarity_flipping,[],[f10838]) ).
fof(f21087,plain,
! [X0,X1] :
( ~ subr(sK57(X0,X1),sub_0)
| sub(X0,X1) ),
inference(consistent_polarity_flipping,[],[f10837]) ).
fof(f30624,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ val(X7,s__374dafrika_0)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| subr(X3,rprs_0)
| sub(X7,name_1_1)
| sub(X4,X9)
| sub(X2,eigenname_1_1)
| sub(X1,familiename_1_1)
| ~ obj(X8,X0)
| ~ attr(X6,X7)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ arg1(X3,X0)
| ~ in(X5,X6) ),
inference(consistent_polarity_flipping,[],[f20771]) ).
fof(f30625,plain,
~ sub(c28444,pr__344sident_1_1),
inference(consistent_polarity_flipping,[],[f20885]) ).
fof(f30626,plain,
~ sub(c28445,eigenname_1_1),
inference(consistent_polarity_flipping,[],[f20884]) ).
fof(f30627,plain,
~ sub(c28446,familiename_1_1),
inference(consistent_polarity_flipping,[],[f20882]) ).
fof(f30687,definition,
( spl63_1
<=> ! [X4,X9,X0,X8,X3,X2,X1] :
( ~ val(X2,nelson_0)
| ~ attr(X0,X1)
| ~ obj(X8,X0)
| ~ attr(X0,X2)
| sub(X2,eigenname_1_1)
| subr(X3,rprs_0)
| ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| sub(X4,X9)
| ~ val(X1,mandela_0)
| sub(X1,familiename_1_1) ) ),
introduced(definition,[new_symbols(definition,[spl63_1])],[avatar_definition]) ).
fof(f30688,plain,
( ! [X2,X3,X0,X1,X8,X9,X4] :
( ~ val(X2,nelson_0)
| ~ attr(X0,X1)
| ~ obj(X8,X0)
| ~ attr(X0,X2)
| sub(X2,eigenname_1_1)
| subr(X3,rprs_0)
| ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| sub(X4,X9)
| ~ val(X1,mandela_0)
| sub(X1,familiename_1_1) )
| ~ spl63_1 ),
inference(avatar_component_clause,[],[f30687]) ).
fof(f30690,definition,
( spl63_2
<=> ! [X6,X5,X7] :
( ~ val(X7,s__374dafrika_0)
| ~ in(X5,X6)
| ~ attr(X6,X7)
| sub(X7,name_1_1) ) ),
introduced(definition,[new_symbols(definition,[spl63_2])],[avatar_definition]) ).
fof(f30691,plain,
( ! [X6,X7,X5] :
( ~ val(X7,s__374dafrika_0)
| ~ in(X5,X6)
| ~ attr(X6,X7)
| sub(X7,name_1_1) )
| ~ spl63_2 ),
inference(avatar_component_clause,[],[f30690]) ).
fof(f30692,plain,
( spl63_1
| spl63_2 ),
inference(avatar_split_clause,[],[f30624,f30690,f30687]) ).
fof(f30884,plain,
! [X0] :
( ~ state_adjective_state_binding(s__374dafrikanisch_1_1,X0)
| val(sK48(c28444,X0),X0) ),
inference(resolution,[],[f10806,f20886]) ).
fof(f31163,plain,
val(sK48(c28444,s__374dafrika_0),s__374dafrika_0),
inference(resolution,[],[f30884,f19744]) ).
fof(f31164,plain,
( ! [X0,X1] :
( ~ in(X0,X1)
| ~ attr(X1,sK48(c28444,s__374dafrika_0))
| sub(sK48(c28444,s__374dafrika_0),name_1_1) )
| ~ spl63_2 ),
inference(resolution,[],[f31163,f30691]) ).
fof(f31166,definition,
( spl63_35
<=> sub(sK48(c28444,s__374dafrika_0),name_1_1) ),
introduced(definition,[new_symbols(definition,[spl63_35])],[avatar_definition]) ).
fof(f31167,plain,
( ~ sub(sK48(c28444,s__374dafrika_0),name_1_1)
| spl63_35 ),
inference(avatar_component_clause,[],[f31166]) ).
fof(f31168,plain,
( sub(sK48(c28444,s__374dafrika_0),name_1_1)
| ~ spl63_35 ),
inference(avatar_component_clause,[],[f31166]) ).
fof(f31170,definition,
( spl63_36
<=> ! [X0,X1] :
( ~ in(X0,X1)
| ~ attr(X1,sK48(c28444,s__374dafrika_0)) ) ),
introduced(definition,[new_symbols(definition,[spl63_36])],[avatar_definition]) ).
fof(f31171,plain,
( ! [X0,X1] :
( ~ attr(X1,sK48(c28444,s__374dafrika_0))
| ~ in(X0,X1) )
| ~ spl63_36 ),
inference(avatar_component_clause,[],[f31170]) ).
fof(f31173,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ attr(X0,X1)
| ~ obj(X2,X0)
| ~ attr(X0,c28445)
| sub(c28445,eigenname_1_1)
| subr(X3,rprs_0)
| ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| sub(X4,X5)
| ~ val(X1,mandela_0)
| sub(X1,familiename_1_1) )
| ~ spl63_1 ),
inference(resolution,[],[f30688,f20883]) ).
fof(f31174,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ val(X1,mandela_0)
| ~ obj(X2,X0)
| ~ attr(X0,c28445)
| subr(X3,rprs_0)
| ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| sub(X4,X5)
| ~ attr(X0,X1)
| sub(X1,familiename_1_1) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f31173,f30626]) ).
fof(f31175,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ obj(X0,X1)
| ~ attr(X1,c28445)
| subr(X2,rprs_0)
| ~ arg1(X2,X1)
| ~ arg2(X2,X3)
| sub(X3,X4)
| ~ attr(X1,c28446)
| sub(c28446,familiename_1_1) )
| ~ spl63_1 ),
inference(resolution,[],[f31174,f20881]) ).
fof(f31176,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ attr(X1,c28446)
| ~ attr(X1,c28445)
| subr(X2,rprs_0)
| ~ arg1(X2,X1)
| ~ arg2(X2,X3)
| sub(X3,X4)
| ~ obj(X0,X1) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f31175,f30627]) ).
fof(f31234,plain,
( ! [X0] :
( ~ state_adjective_state_binding(X0,s__374dafrika_0)
| ~ prop(c28444,X0) )
| ~ spl63_35 ),
inference(resolution,[],[f31168,f21064]) ).
fof(f31241,plain,
( ~ prop(c28444,s__374dafrikanisch_1_1)
| ~ spl63_35 ),
inference(resolution,[],[f31234,f19744]) ).
fof(f31242,plain,
( $false
| ~ spl63_35 ),
inference(forward_subsumption_resolution,[],[f31241,f20886]) ).
fof(f31243,plain,
~ spl63_35,
inference(avatar_contradiction_clause,[],[f31242]) ).
fof(f31246,plain,
! [X0] :
( attr(sK47(c28444,X0),sK48(c28444,X0))
| ~ state_adjective_state_binding(s__374dafrikanisch_1_1,X0) ),
inference(resolution,[],[f10810,f20886]) ).
fof(f31251,plain,
! [X0] :
( ~ state_adjective_state_binding(s__374dafrikanisch_1_1,X0)
| in(sK49(c28444,X0),sK47(c28444,X0)) ),
inference(resolution,[],[f10811,f20886]) ).
fof(f31255,plain,
( ! [X2,X3,X0,X1] :
( ~ attr(c28444,c28445)
| subr(X0,rprs_0)
| ~ arg1(X0,c28444)
| ~ arg2(X0,X1)
| sub(X1,X2)
| ~ obj(X3,c28444) )
| ~ spl63_1 ),
inference(resolution,[],[f31176,f20887]) ).
fof(f31256,plain,
( ! [X2,X3,X0,X1] :
( subr(X0,rprs_0)
| ~ arg1(X0,c28444)
| ~ arg2(X0,X1)
| sub(X1,X2)
| ~ obj(X3,c28444) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f31255,f20888]) ).
fof(f31258,definition,
( spl63_48
<=> ! [X3] : ~ obj(X3,c28444) ),
introduced(definition,[new_symbols(definition,[spl63_48])],[avatar_definition]) ).
fof(f31259,plain,
( ! [X3] : ~ obj(X3,c28444)
| ~ spl63_48 ),
inference(avatar_component_clause,[],[f31258]) ).
fof(f31261,definition,
( spl63_49
<=> ! [X2,X0,X1] :
( subr(X0,rprs_0)
| sub(X1,X2)
| ~ arg2(X0,X1)
| ~ arg1(X0,c28444) ) ),
introduced(definition,[new_symbols(definition,[spl63_49])],[avatar_definition]) ).
fof(f31262,plain,
( ! [X2,X0,X1] :
( ~ arg1(X0,c28444)
| sub(X1,X2)
| ~ arg2(X0,X1)
| subr(X0,rprs_0) )
| ~ spl63_49 ),
inference(avatar_component_clause,[],[f31261]) ).
fof(f31264,plain,
( ! [X0,X1] :
( ~ in(X0,X1)
| ~ attr(X1,sK48(c28444,s__374dafrika_0)) )
| ~ spl63_2
| spl63_35 ),
inference(forward_subsumption_resolution,[],[f31164,f31167]) ).
fof(f31265,plain,
( spl63_36
| ~ spl63_2
| spl63_35 ),
inference(avatar_split_clause,[],[f31264,f31166,f30690,f31170]) ).
fof(f32557,plain,
! [X0,X1] :
( ~ attr(X1,X0)
| sub(X0,eigenname_1_1)
| obj(sK51(X1),X1) ),
inference(resolution,[],[f21072,f10554]) ).
fof(f38864,plain,
( ! [X0] :
( ~ state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0)
| ~ in(X0,sK47(c28444,s__374dafrika_0)) )
| ~ spl63_36 ),
inference(resolution,[],[f31246,f31171]) ).
fof(f38865,plain,
( ! [X0] : ~ in(X0,sK47(c28444,s__374dafrika_0))
| ~ spl63_36 ),
inference(forward_subsumption_resolution,[],[f38864,f19744]) ).
fof(f38866,plain,
in(sK49(c28444,s__374dafrika_0),sK47(c28444,s__374dafrika_0)),
inference(resolution,[],[f31251,f19744]) ).
fof(f39057,plain,
( sub(c28445,eigenname_1_1)
| obj(sK51(c28444),c28444) ),
inference(resolution,[],[f32557,f20888]) ).
fof(f39079,plain,
obj(sK51(c28444),c28444),
inference(forward_subsumption_resolution,[],[f39057,f30626]) ).
fof(f39081,definition,
( spl63_1159
<=> obj(sK51(c28444),c28444) ),
introduced(definition,[new_symbols(definition,[spl63_1159])],[avatar_definition]) ).
fof(f39083,plain,
( obj(sK51(c28444),c28444)
| ~ spl63_1159 ),
inference(avatar_component_clause,[],[f39081]) ).
fof(f39086,plain,
spl63_1159,
inference(avatar_split_clause,[],[f39079,f39081]) ).
fof(f60702,plain,
( $false
| ~ spl63_36 ),
inference(forward_subsumption_resolution,[],[f38866,f38865]) ).
fof(f60703,plain,
~ spl63_36,
inference(avatar_contradiction_clause,[],[f60702]) ).
fof(f60704,plain,
( spl63_48
| spl63_49
| ~ spl63_1 ),
inference(avatar_split_clause,[],[f31256,f30687,f31261,f31258]) ).
fof(f60709,plain,
( $false
| ~ spl63_48
| ~ spl63_1159 ),
inference(backward_subsumption_resolution,[],[f39083,f31259]) ).
fof(f60740,plain,
( ~ spl63_48
| ~ spl63_1159 ),
inference(avatar_contradiction_clause,[],[f60709]) ).
fof(f60860,plain,
( ! [X2,X3,X0,X1] :
( sub(X0,X1)
| ~ arg2(sK55(X2,c28444,X3),X0)
| subr(sK55(X2,c28444,X3),rprs_0)
| ~ arg2(X2,X3)
| ~ arg1(X2,c28444)
| subr(X2,sub_0) )
| ~ spl63_49 ),
inference(resolution,[],[f31262,f21077]) ).
fof(f60862,plain,
( ! [X2,X3,X0,X1] :
( ~ arg2(sK55(X2,c28444,X3),X0)
| sub(X0,X1)
| ~ arg2(X2,X3)
| ~ arg1(X2,c28444)
| subr(X2,sub_0) )
| ~ spl63_49 ),
inference(forward_subsumption_resolution,[],[f60860,f21083]) ).
fof(f60980,plain,
( ! [X2,X0,X1] :
( sub(sK56(X0,c28444,X1),X2)
| ~ arg2(X0,X1)
| ~ arg1(X0,c28444)
| subr(X0,sub_0)
| ~ arg2(X0,X1)
| ~ arg1(X0,c28444)
| subr(X0,sub_0) )
| ~ spl63_49 ),
inference(resolution,[],[f60862,f21078]) ).
fof(f60981,plain,
( ! [X2,X0,X1] :
( ~ arg1(X0,c28444)
| ~ arg2(X0,X1)
| sub(sK56(X0,c28444,X1),X2)
| subr(X0,sub_0) )
| ~ spl63_49 ),
inference(duplicate_literal_removal,[],[f60980]) ).
fof(f60988,plain,
( ! [X2,X0,X1] :
( ~ arg2(sK57(c28444,X0),X1)
| sub(sK56(sK57(c28444,X0),c28444,X1),X2)
| subr(sK57(c28444,X0),sub_0)
| sub(c28444,X0) )
| ~ spl63_49 ),
inference(resolution,[],[f60981,f21085]) ).
fof(f60992,plain,
( ! [X2,X0,X1] :
( ~ arg2(sK57(c28444,X0),X1)
| sub(sK56(sK57(c28444,X0),c28444,X1),X2)
| sub(c28444,X0) )
| ~ spl63_49 ),
inference(forward_subsumption_resolution,[],[f60988,f21087]) ).
fof(f60997,plain,
( ! [X0,X1] :
( sub(sK56(sK57(c28444,X0),c28444,X0),X1)
| sub(c28444,X0)
| sub(c28444,X0) )
| ~ spl63_49 ),
inference(resolution,[],[f60992,f21086]) ).
fof(f60998,plain,
( ! [X0,X1] :
( sub(sK56(sK57(c28444,X0),c28444,X0),X1)
| sub(c28444,X0) )
| ~ spl63_49 ),
inference(duplicate_literal_removal,[],[f60997]) ).
fof(f61034,plain,
( ! [X0] :
( sub(c28444,X0)
| ~ arg2(sK57(c28444,X0),X0)
| ~ arg1(sK57(c28444,X0),c28444)
| subr(sK57(c28444,X0),sub_0) )
| ~ spl63_49 ),
inference(resolution,[],[f60998,f21082]) ).
fof(f61046,plain,
( ! [X0] :
( sub(c28444,X0)
| ~ arg1(sK57(c28444,X0),c28444)
| subr(sK57(c28444,X0),sub_0) )
| ~ spl63_49 ),
inference(forward_subsumption_resolution,[],[f61034,f21086]) ).
fof(f61047,plain,
( ! [X0] :
( sub(c28444,X0)
| subr(sK57(c28444,X0),sub_0) )
| ~ spl63_49 ),
inference(forward_subsumption_resolution,[],[f61046,f21085]) ).
fof(f61048,plain,
( ! [X0] : sub(c28444,X0)
| ~ spl63_49 ),
inference(forward_subsumption_resolution,[],[f61047,f21087]) ).
fof(f61051,plain,
( $false
| ~ spl63_49 ),
inference(backward_subsumption_resolution,[],[f30625,f61048]) ).
fof(f61063,plain,
~ spl63_49,
inference(avatar_contradiction_clause,[],[f61051]) ).
cnf(s1,plain,
( spl63_1
| spl63_2 ),
inference(sat_conversion,[],[f30692]) ).
cnf(s34,plain,
~ spl63_35,
inference(sat_conversion,[],[f31243]) ).
cnf(s36,plain,
( ~ spl63_2
| spl63_35
| spl63_36 ),
inference(sat_conversion,[],[f31265]) ).
cnf(s858,plain,
spl63_1159,
inference(sat_conversion,[],[f39086]) ).
cnf(s3160,plain,
~ spl63_36,
inference(sat_conversion,[],[f60703]) ).
cnf(s3161,plain,
( ~ spl63_1
| spl63_48
| spl63_49 ),
inference(sat_conversion,[],[f60704]) ).
cnf(s3162,plain,
( ~ spl63_48
| ~ spl63_1159 ),
inference(sat_conversion,[],[f60740]) ).
cnf(s3194,plain,
~ spl63_49,
inference(sat_conversion,[],[f61063]) ).
cnf(s3196,plain,
( ~ spl63_1
| spl63_48 ),
inference(rat,[],[s3161,s3194]) ).
cnf(s3225,plain,
~ spl63_48,
inference(rat,[],[s3162,s858]) ).
cnf(s3226,plain,
~ spl63_1,
inference(rat,[],[s3196,s3225]) ).
cnf(s3235,plain,
( ~ spl63_2
| spl63_35 ),
inference(rat,[],[s36,s3160]) ).
cnf(s3236,plain,
~ spl63_2,
inference(rat,[],[s3235,s34]) ).
cnf(s3241,plain,
$false,
inference(rat,[],[s1,s3236,s3226]) ).
fof(f61072,plain,
$false,
inference(avatar_sat_refutation,[],[s3241]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+10 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.16 % Computer : n003.cluster.edu
% 0.09/0.16 % Model : x86_64 x86_64
% 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.16 % Memory : 8046.5625MB
% 0.09/0.16 % OS : Linux 6.8.0-71-generic
% 0.09/0.16 % CPULimit : 300
% 0.09/0.16 % WCLimit : 300
% 0.09/0.16 % DateTime : Mon Sep 28 23:26:13 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 Running first-order model finding
% 0.09/0.19 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.70/1.15 % (2126547)Will run a generic schedule for satisfiability detection.
% 5.70/1.15 % (2126553)% WARNING: option uhcvi not known.
% 5.70/1.15 % (2126553)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2268598450:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 5.70/1.15 % (2126552)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2845210470_2998 on theBenchmark for (2998ds/0Mi)
% 5.70/1.15 % (2126554)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1305965259:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 5.70/1.15 % (2126555)dis+10_1_sil=32000:sp=arity:random_seed=385671149:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 5.70/1.15 % (2126556)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1567934:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 5.70/1.15 % (2126557)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2313340970:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 5.70/1.15 % (2126558)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=638428348:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 5.70/1.15 % (2126555)Instruction limit reached!
% 5.70/1.15 % (2126555)------------------------------
% 5.70/1.15 % (2126555)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.15 % (2126555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.15 % (2126555)CaDiCaL version: 2.1.3
% 5.70/1.15 % (2126555)Termination reason: Instruction limit
% 5.70/1.15 % (2126555)Termination phase: Saturation
% 5.70/1.15 % (2126555)Time elapsed: 0.057 s
% 5.70/1.15 % (2126555)Peak memory usage: 26 MB
% 5.70/1.15 % (2126555)Instructions burned: 106 (million)
% 5.70/1.15 % (2126556)Instruction limit reached!
% 5.70/1.15 % (2126556)------------------------------
% 5.70/1.15 % (2126556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.15 % (2126556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.15 % (2126556)CaDiCaL version: 2.1.3
% 5.70/1.15 % (2126556)Termination reason: Instruction limit
% 5.70/1.15 % (2126556)Termination phase: Blocked clause elimination
% 5.70/1.15 % (2126556)Time elapsed: 0.071 s
% 5.70/1.15 % (2126556)Peak memory usage: 28 MB
% 5.70/1.15 % (2126556)Instructions burned: 116 (million)
% 5.70/1.15 % (2126557)Instruction limit reached!
% 5.70/1.15 % (2126557)------------------------------
% 5.70/1.15 % (2126557)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.15 % (2126557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.15 % (2126557)CaDiCaL version: 2.1.3
% 5.70/1.15 % (2126557)Termination reason: Instruction limit
% 5.70/1.15 % (2126557)Termination phase: Saturation
% 5.70/1.15 % (2126557)Time elapsed: 0.072 s
% 5.70/1.15 % (2126557)Peak memory usage: 28 MB
% 5.70/1.15 % (2126557)Instructions burned: 131 (million)
% 5.70/1.15 % (2126566)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3159042852:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 5.70/1.15 % (2126558)Instruction limit reached!
% 5.70/1.15 % (2126558)------------------------------
% 5.70/1.15 % (2126558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.15 % (2126558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.15 % (2126558)CaDiCaL version: 2.1.3
% 5.70/1.15 % (2126558)Termination reason: Instruction limit
% 5.70/1.15 % (2126558)Termination phase: Saturation
% 5.70/1.15 % (2126558)Time elapsed: 0.091 s
% 5.70/1.15 % (2126558)Peak memory usage: 29 MB
% 5.70/1.15 % (2126558)Instructions burned: 161 (million)
% 5.70/1.15 % (2126567)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1038682703:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 5.70/1.15 % (2126568)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3659719648:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 5.70/1.15 % (2126572)ott-21_1_sil=16000:fs=off:random_seed=2761601802:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 5.70/1.15 % (2126567)Instruction limit reached!
% 5.70/1.15 % (2126567)------------------------------
% 5.70/1.15 % (2126567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.15 % (2126567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.15 % (2126567)CaDiCaL version: 2.1.3
% 5.70/1.15 % (2126567)Termination reason: Instruction limit
% 5.70/1.15 % (2126567)Termination phase: Blocked clause elimination
% 5.70/1.15 % (2126567)Time elapsed: 0.078 s
% 5.70/1.15 % (2126567)Peak memory usage: 29 MB
% 5.70/1.15 % (2126567)Instructions burned: 132 (million)
% 5.70/1.15 % (2126574)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1214767254:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 5.70/1.15 % (2126572)Instruction limit reached!
% 5.70/1.15 % (2126572)------------------------------
% 5.70/1.15 % (2126572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.15 % (2126572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.15 % (2126572)CaDiCaL version: 2.1.3
% 5.70/1.15 % (2126572)Termination reason: Instruction limit
% 5.70/1.15 % (2126572)Termination phase: Saturation
% 5.70/1.15 % (2126572)Time elapsed: 0.089 s
% 5.70/1.15 % (2126572)Peak memory usage: 28 MB
% 5.70/1.15 % (2126572)Instructions burned: 181 (million)
% 5.70/1.15 % (2126576)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2970089920:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 5.70/1.15 % TRYING [1]
% 5.70/1.15 % TRYING [1]
% 5.70/1.15 % TRYING [2]
% 5.70/1.15 % TRYING [2]
% 5.70/1.15 % (2126566)Instruction limit reached!
% 5.70/1.15 % (2126566)------------------------------
% 5.70/1.15 % (2126566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.15 % (2126566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.15 % (2126566)CaDiCaL version: 2.1.3
% 5.70/1.15 % (2126566)Termination reason: Instruction limit
% 5.70/1.15 % (2126566)Termination phase: Finite model building constraint generation
% 5.70/1.15 % (2126566)Time elapsed: 0.322 s
% 5.70/1.15 % (2126566)Peak memory usage: 54 MB
% 5.70/1.15 % (2126566)Instructions burned: 715 (million)
% 5.70/1.15 % (2126578)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1413035881:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 5.70/1.15 % TRYING [1]
% 5.70/1.15 % (2126568)Instruction limit reached!
% 5.70/1.15 % (2126568)------------------------------
% 5.70/1.15 % (2126568)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.15 % (2126568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.15 % (2126568)CaDiCaL version: 2.1.3
% 5.70/1.15 % (2126568)Termination reason: Instruction limit
% 5.70/1.15 % (2126568)Termination phase: Saturation
% 5.70/1.15 % (2126568)Time elapsed: 0.350 s
% 5.70/1.15 % (2126568)Peak memory usage: 34 MB
% 5.70/1.15 % (2126568)Instructions burned: 686 (million)
% 5.70/1.15 % (2126574)Instruction limit reached!
% 5.70/1.15 % (2126574)------------------------------
% 5.70/1.15 % (2126574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.15 % (2126574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.15 % (2126574)CaDiCaL version: 2.1.3
% 5.70/1.15 % (2126574)Termination reason: Instruction limit
% 5.70/1.15 % (2126574)Termination phase: Saturation
% 5.70/1.15 % (2126574)Time elapsed: 0.251 s
% 5.70/1.15 % (2126574)Peak memory usage: 37 MB
% 5.70/1.15 % (2126574)Instructions burned: 477 (million)
% 5.70/1.15 % (2126580)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=455126412:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 5.70/1.15 % (2126581)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=447837739:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 5.70/1.15 % TRYING [3]
% 5.70/1.15 % (2126576)Instruction limit reached!
% 5.70/1.15 % (2126576)------------------------------
% 5.70/1.15 % (2126576)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.15 % (2126576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.15 % (2126576)CaDiCaL version: 2.1.3
% 5.70/1.15 % (2126576)Termination reason: Instruction limit
% 5.70/1.15 % (2126576)Termination phase: Finite model building SAT solving
% 5.70/1.15 % (2126576)Time elapsed: 0.321 s
% 5.70/1.15 % (2126576)Peak memory usage: 38 MB
% 5.70/1.15 % (2126576)Instructions burned: 867 (million)
% 5.70/1.15 % (2126584)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4013612862:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 5.70/1.15 % (2126553) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2126547-2126553"...
% 5.70/1.15 % (2126553)...printing done.
% 5.70/1.15 % (2126553)Refutation found. Thanks to Tanya!
% 5.70/1.15 % SZS status Theorem for theBenchmark
% 5.70/1.15 % SZS output start Proof for theBenchmark
% See solution above
% 5.70/1.17 % (2126553)------------------------------
% 5.70/1.17 % (2126553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.70/1.17 % (2126553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.70/1.17 % (2126553)CaDiCaL version: 2.1.3
% 5.70/1.17 % (2126553)Termination reason: Refutation
% 5.70/1.17 % (2126553)Time elapsed: 0.753 s
% 5.70/1.17 % (2126553)Peak memory usage: 55 MB
% 5.70/1.17 % (2126553)Instructions burned: 2408 (million)
% 5.70/1.17 % (2126547)Success in time 0.952 s
% 5.70/1.17 % Vampire exiting
%------------------------------------------------------------------------------