%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR116+2 : 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 : n011.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:50 AM UTC 2026
% Result : Theorem 37.85s 10.92s
% Output : Refutation 37.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 6
% Syntax : Number of formulae : 83 ( 16 unt; 0 def)
% Number of atoms : 2948 ( 0 equ)
% Maximal formula atoms : 346 ( 35 avg)
% Number of connectives : 3132 ( 267 ~; 235 |;2626 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 346 ( 39 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 28 ( 27 usr; 1 prp; 0-10 aty)
% Number of functors : 84 ( 84 usr; 79 con; 0-3 aty)
% Number of variables : 230 ( 199 !; 31 ?)
% Comments :
%------------------------------------------------------------------------------
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(f177,axiom,
! [X0,X1] :
( name(X1,X0)
=> ? [X2] :
( attr(X1,X2)
& sub(X2,name_1_1)
& val(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',name_rel__attr_val_name_1_1) ).
fof(f178,axiom,
! [X0,X1,X2] :
( ( attr(X2,X0)
& sub(X0,name_1_1)
& val(X0,X1) )
=> name(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',attr_val_name_1_1__name_rel) ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( pmod(X8,erst_1_1,pr__344sident_1_1)
& arg1(X3,X0)
& attr(X0,X1)
& attr(X0,X2)
& attr(X5,X6)
& obj(X7,X0)
& prop(X4,schwarz_1_1)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X8)
& sub(X6,name_1_1)
& subr(X3,rprs_0)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X6,s__374dafrika_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_010_mira_news_1591) ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( pmod(X8,erst_1_1,pr__344sident_1_1)
& arg1(X3,X0)
& attr(X0,X1)
& attr(X0,X2)
& attr(X5,X6)
& obj(X7,X0)
& prop(X4,schwarz_1_1)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X8)
& sub(X6,name_1_1)
& subr(X3,rprs_0)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X6,s__374dafrika_0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( assoc(apartheidsstaat_1_1,apartheid_1_1)
& sub(apartheidsstaat_1_1,land_1_1)
& attr(c6477,c6478)
& attr(c6477,c6479)
& sub(c6477,mensch_1_1)
& sub(c6478,eigenname_1_1)
& val(c6478,nelson_0)
& sub(c6479,familiename_1_1)
& val(c6479,mandela_0)
& prop(c6485,schwarz_1_1)
& sub(c6485,c6492)
& pmod(c6492,erst_1_1,pr__344sident_1_1)
& sub(c6496,abschlu__337_1_1)
& attch(c6499,c6496)
& sub(c6499,apartheidsstaat_1_1)
& sub(c6500,von_2_1)
& attr(c6506,c6507)
& attr(c6506,c6508)
& sub(c6506,mensch_1_1)
& sub(c6507,eigenname_1_1)
& val(c6507,hans_0)
& sub(c6508,familiename_1_1)
& val(c6508,brandt_0)
& sub(c6509,in_2_1)
& attr(c6515,c6516)
& sub(c6515,land_1_1)
& sub(c6516,name_1_1)
& val(c6516,s__374dafrika_0)
& sub(c6519,montag__1_1)
& quant_p3(c6528,c6523,jahr__1_1)
& agt(c6529,c6536)
& dur(c6529,c6528)
& subs(c6529,hegemonie_1_1)
& prop(c6536,wei__337_1_1)
& sub(c6536,minderheit_1_2)
& tupl_p10(c6617,c6477,c6485,c6496,c6500,c6506,c6509,c6515,c6519,c6529)
& assoc(hegemonie_1_1,pr__344_1_1)
& subs(hegemonie_1_1,dominanz_1_1)
& sort(apartheidsstaat_1_1,d)
& sort(apartheidsstaat_1_1,io)
& card(apartheidsstaat_1_1,int1)
& etype(apartheidsstaat_1_1,int0)
& fact(apartheidsstaat_1_1,real)
& gener(apartheidsstaat_1_1,ge)
& quant(apartheidsstaat_1_1,one)
& refer(apartheidsstaat_1_1,refer_c)
& varia(apartheidsstaat_1_1,varia_c)
& sort(apartheid_1_1,io)
& card(apartheid_1_1,int1)
& etype(apartheid_1_1,int0)
& fact(apartheid_1_1,real)
& gener(apartheid_1_1,ge)
& quant(apartheid_1_1,one)
& refer(apartheid_1_1,refer_c)
& varia(apartheid_1_1,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(c6477,d)
& card(c6477,int1)
& etype(c6477,int0)
& fact(c6477,real)
& gener(c6477,sp)
& quant(c6477,one)
& refer(c6477,det)
& varia(c6477,con)
& sort(c6478,na)
& card(c6478,int1)
& etype(c6478,int0)
& fact(c6478,real)
& gener(c6478,sp)
& quant(c6478,one)
& refer(c6478,indet)
& varia(c6478,varia_c)
& sort(c6479,na)
& card(c6479,int1)
& etype(c6479,int0)
& fact(c6479,real)
& gener(c6479,sp)
& quant(c6479,one)
& refer(c6479,indet)
& varia(c6479,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(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(c6485,d)
& card(c6485,int1)
& etype(c6485,int0)
& fact(c6485,real)
& gener(c6485,sp)
& quant(c6485,one)
& refer(c6485,det)
& varia(c6485,con)
& sort(schwarz_1_1,tq)
& sort(c6492,d)
& card(c6492,int1)
& etype(c6492,int0)
& fact(c6492,real)
& gener(c6492,ge)
& quant(c6492,one)
& refer(c6492,refer_c)
& varia(c6492,varia_c)
& sort(erst_1_1,oq)
& card(erst_1_1,int1)
& 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(c6496,ad)
& sort(c6496,io)
& card(c6496,int1)
& etype(c6496,int0)
& fact(c6496,real)
& gener(c6496,sp)
& quant(c6496,one)
& refer(c6496,det)
& varia(c6496,varia_c)
& sort(abschlu__337_1_1,ad)
& sort(abschlu__337_1_1,io)
& card(abschlu__337_1_1,int1)
& etype(abschlu__337_1_1,int0)
& fact(abschlu__337_1_1,real)
& gener(abschlu__337_1_1,ge)
& quant(abschlu__337_1_1,one)
& refer(abschlu__337_1_1,refer_c)
& varia(abschlu__337_1_1,varia_c)
& sort(c6499,d)
& sort(c6499,io)
& card(c6499,int1)
& etype(c6499,int0)
& fact(c6499,real)
& gener(c6499,sp)
& quant(c6499,one)
& refer(c6499,det)
& varia(c6499,con)
& sort(c6500,o)
& card(c6500,int1)
& etype(c6500,int0)
& fact(c6500,real)
& gener(c6500,gener_c)
& quant(c6500,one)
& refer(c6500,refer_c)
& varia(c6500,varia_c)
& sort(von_2_1,o)
& card(von_2_1,int1)
& etype(von_2_1,int0)
& fact(von_2_1,real)
& gener(von_2_1,ge)
& quant(von_2_1,one)
& refer(von_2_1,refer_c)
& varia(von_2_1,varia_c)
& sort(c6506,d)
& card(c6506,int1)
& etype(c6506,int0)
& fact(c6506,real)
& gener(c6506,sp)
& quant(c6506,one)
& refer(c6506,det)
& varia(c6506,con)
& sort(c6507,na)
& card(c6507,int1)
& etype(c6507,int0)
& fact(c6507,real)
& gener(c6507,sp)
& quant(c6507,one)
& refer(c6507,indet)
& varia(c6507,varia_c)
& sort(c6508,na)
& card(c6508,int1)
& etype(c6508,int0)
& fact(c6508,real)
& gener(c6508,sp)
& quant(c6508,one)
& refer(c6508,indet)
& varia(c6508,varia_c)
& sort(hans_0,fe)
& sort(brandt_0,fe)
& sort(c6509,o)
& card(c6509,int1)
& etype(c6509,int0)
& fact(c6509,real)
& gener(c6509,gener_c)
& quant(c6509,one)
& refer(c6509,refer_c)
& varia(c6509,varia_c)
& sort(in_2_1,o)
& card(in_2_1,int1)
& etype(in_2_1,int0)
& fact(in_2_1,real)
& gener(in_2_1,ge)
& quant(in_2_1,one)
& refer(in_2_1,refer_c)
& varia(in_2_1,varia_c)
& sort(c6515,d)
& sort(c6515,io)
& card(c6515,int1)
& etype(c6515,int0)
& fact(c6515,real)
& gener(c6515,sp)
& quant(c6515,one)
& refer(c6515,det)
& varia(c6515,con)
& sort(c6516,na)
& card(c6516,int1)
& etype(c6516,int0)
& fact(c6516,real)
& gener(c6516,sp)
& quant(c6516,one)
& refer(c6516,indet)
& varia(c6516,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(s__374dafrika_0,fe)
& sort(c6519,ta)
& card(c6519,int1)
& etype(c6519,int0)
& fact(c6519,real)
& gener(c6519,sp)
& quant(c6519,one)
& refer(c6519,det)
& varia(c6519,con)
& sort(montag__1_1,ta)
& card(montag__1_1,int1)
& etype(montag__1_1,int0)
& fact(montag__1_1,real)
& gener(montag__1_1,ge)
& quant(montag__1_1,one)
& refer(montag__1_1,refer_c)
& varia(montag__1_1,varia_c)
& sort(c6528,m)
& sort(c6528,ta)
& card(c6528,card_c)
& etype(c6528,etype_c)
& fact(c6528,real)
& gener(c6528,gener_c)
& quant(c6528,quant_c)
& refer(c6528,refer_c)
& varia(c6528,varia_c)
& sort(c6523,nu)
& card(c6523,int342)
& sort(jahr__1_1,me)
& sort(jahr__1_1,oa)
& sort(jahr__1_1,ta)
& card(jahr__1_1,card_c)
& etype(jahr__1_1,etype_c)
& fact(jahr__1_1,real)
& gener(jahr__1_1,ge)
& quant(jahr__1_1,quant_c)
& refer(jahr__1_1,refer_c)
& varia(jahr__1_1,varia_c)
& sort(c6529,ad)
& card(c6529,int1)
& etype(c6529,int0)
& fact(c6529,real)
& gener(c6529,sp)
& quant(c6529,one)
& refer(c6529,det)
& varia(c6529,con)
& sort(c6536,d)
& card(c6536,int1)
& etype(c6536,int1)
& fact(c6536,real)
& gener(c6536,sp)
& quant(c6536,one)
& refer(c6536,det)
& varia(c6536,con)
& sort(hegemonie_1_1,ad)
& card(hegemonie_1_1,int1)
& etype(hegemonie_1_1,int0)
& fact(hegemonie_1_1,real)
& gener(hegemonie_1_1,ge)
& quant(hegemonie_1_1,one)
& refer(hegemonie_1_1,refer_c)
& varia(hegemonie_1_1,varia_c)
& sort(wei__337_1_1,nq)
& sort(minderheit_1_2,d)
& card(minderheit_1_2,card_c)
& etype(minderheit_1_2,int1)
& fact(minderheit_1_2,real)
& gener(minderheit_1_2,ge)
& quant(minderheit_1_2,quant_c)
& refer(minderheit_1_2,refer_c)
& varia(minderheit_1_2,varia_c)
& sort(c6617,ent)
& card(c6617,card_c)
& etype(c6617,etype_c)
& fact(c6617,real)
& gener(c6617,gener_c)
& quant(c6617,quant_c)
& refer(c6617,refer_c)
& varia(c6617,varia_c)
& sort(pr__344_1_1,ent)
& card(pr__344_1_1,card_c)
& etype(pr__344_1_1,etype_c)
& fact(pr__344_1_1,real)
& gener(pr__344_1_1,gener_c)
& quant(pr__344_1_1,quant_c)
& refer(pr__344_1_1,refer_c)
& varia(pr__344_1_1,varia_c)
& sort(dominanz_1_1,ad)
& card(dominanz_1_1,int1)
& etype(dominanz_1_1,int0)
& fact(dominanz_1_1,real)
& gener(dominanz_1_1,ge)
& quant(dominanz_1_1,one)
& refer(dominanz_1_1,refer_c)
& varia(dominanz_1_1,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_news_1591) ).
fof(f10191,plain,
( assoc(apartheidsstaat_1_1,apartheid_1_1)
& sub(apartheidsstaat_1_1,land_1_1)
& attr(c6477,c6478)
& attr(c6477,c6479)
& sub(c6477,mensch_1_1)
& sub(c6478,eigenname_1_1)
& val(c6478,nelson_0)
& sub(c6479,familiename_1_1)
& val(c6479,mandela_0)
& prop(c6485,schwarz_1_1)
& sub(c6485,c6492)
& pmod(c6492,erst_1_1,pr__344sident_1_1)
& sub(c6496,abschlu__337_1_1)
& attch(c6499,c6496)
& sub(c6499,apartheidsstaat_1_1)
& sub(c6500,von_2_1)
& attr(c6506,c6507)
& attr(c6506,c6508)
& sub(c6506,mensch_1_1)
& sub(c6507,eigenname_1_1)
& val(c6507,hans_0)
& sub(c6508,familiename_1_1)
& val(c6508,brandt_0)
& sub(c6509,in_2_1)
& attr(c6515,c6516)
& sub(c6515,land_1_1)
& sub(c6516,name_1_1)
& val(c6516,s__374dafrika_0)
& sub(c6519,montag__1_1)
& quant_p3(c6528,c6523,jahr__1_1)
& agt(c6529,c6536)
& dur(c6529,c6528)
& subs(c6529,hegemonie_1_1)
& prop(c6536,wei__337_1_1)
& sub(c6536,minderheit_1_2)
& assoc(hegemonie_1_1,pr__344_1_1)
& subs(hegemonie_1_1,dominanz_1_1)
& sort(apartheidsstaat_1_1,d)
& sort(apartheidsstaat_1_1,io)
& card(apartheidsstaat_1_1,int1)
& etype(apartheidsstaat_1_1,int0)
& fact(apartheidsstaat_1_1,real)
& gener(apartheidsstaat_1_1,ge)
& quant(apartheidsstaat_1_1,one)
& refer(apartheidsstaat_1_1,refer_c)
& varia(apartheidsstaat_1_1,varia_c)
& sort(apartheid_1_1,io)
& card(apartheid_1_1,int1)
& etype(apartheid_1_1,int0)
& fact(apartheid_1_1,real)
& gener(apartheid_1_1,ge)
& quant(apartheid_1_1,one)
& refer(apartheid_1_1,refer_c)
& varia(apartheid_1_1,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(c6477,d)
& card(c6477,int1)
& etype(c6477,int0)
& fact(c6477,real)
& gener(c6477,sp)
& quant(c6477,one)
& refer(c6477,det)
& varia(c6477,con)
& sort(c6478,na)
& card(c6478,int1)
& etype(c6478,int0)
& fact(c6478,real)
& gener(c6478,sp)
& quant(c6478,one)
& refer(c6478,indet)
& varia(c6478,varia_c)
& sort(c6479,na)
& card(c6479,int1)
& etype(c6479,int0)
& fact(c6479,real)
& gener(c6479,sp)
& quant(c6479,one)
& refer(c6479,indet)
& varia(c6479,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(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(c6485,d)
& card(c6485,int1)
& etype(c6485,int0)
& fact(c6485,real)
& gener(c6485,sp)
& quant(c6485,one)
& refer(c6485,det)
& varia(c6485,con)
& sort(schwarz_1_1,tq)
& sort(c6492,d)
& card(c6492,int1)
& etype(c6492,int0)
& fact(c6492,real)
& gener(c6492,ge)
& quant(c6492,one)
& refer(c6492,refer_c)
& varia(c6492,varia_c)
& sort(erst_1_1,oq)
& card(erst_1_1,int1)
& 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(c6496,ad)
& sort(c6496,io)
& card(c6496,int1)
& etype(c6496,int0)
& fact(c6496,real)
& gener(c6496,sp)
& quant(c6496,one)
& refer(c6496,det)
& varia(c6496,varia_c)
& sort(abschlu__337_1_1,ad)
& sort(abschlu__337_1_1,io)
& card(abschlu__337_1_1,int1)
& etype(abschlu__337_1_1,int0)
& fact(abschlu__337_1_1,real)
& gener(abschlu__337_1_1,ge)
& quant(abschlu__337_1_1,one)
& refer(abschlu__337_1_1,refer_c)
& varia(abschlu__337_1_1,varia_c)
& sort(c6499,d)
& sort(c6499,io)
& card(c6499,int1)
& etype(c6499,int0)
& fact(c6499,real)
& gener(c6499,sp)
& quant(c6499,one)
& refer(c6499,det)
& varia(c6499,con)
& sort(c6500,o)
& card(c6500,int1)
& etype(c6500,int0)
& fact(c6500,real)
& gener(c6500,gener_c)
& quant(c6500,one)
& refer(c6500,refer_c)
& varia(c6500,varia_c)
& sort(von_2_1,o)
& card(von_2_1,int1)
& etype(von_2_1,int0)
& fact(von_2_1,real)
& gener(von_2_1,ge)
& quant(von_2_1,one)
& refer(von_2_1,refer_c)
& varia(von_2_1,varia_c)
& sort(c6506,d)
& card(c6506,int1)
& etype(c6506,int0)
& fact(c6506,real)
& gener(c6506,sp)
& quant(c6506,one)
& refer(c6506,det)
& varia(c6506,con)
& sort(c6507,na)
& card(c6507,int1)
& etype(c6507,int0)
& fact(c6507,real)
& gener(c6507,sp)
& quant(c6507,one)
& refer(c6507,indet)
& varia(c6507,varia_c)
& sort(c6508,na)
& card(c6508,int1)
& etype(c6508,int0)
& fact(c6508,real)
& gener(c6508,sp)
& quant(c6508,one)
& refer(c6508,indet)
& varia(c6508,varia_c)
& sort(hans_0,fe)
& sort(brandt_0,fe)
& sort(c6509,o)
& card(c6509,int1)
& etype(c6509,int0)
& fact(c6509,real)
& gener(c6509,gener_c)
& quant(c6509,one)
& refer(c6509,refer_c)
& varia(c6509,varia_c)
& sort(in_2_1,o)
& card(in_2_1,int1)
& etype(in_2_1,int0)
& fact(in_2_1,real)
& gener(in_2_1,ge)
& quant(in_2_1,one)
& refer(in_2_1,refer_c)
& varia(in_2_1,varia_c)
& sort(c6515,d)
& sort(c6515,io)
& card(c6515,int1)
& etype(c6515,int0)
& fact(c6515,real)
& gener(c6515,sp)
& quant(c6515,one)
& refer(c6515,det)
& varia(c6515,con)
& sort(c6516,na)
& card(c6516,int1)
& etype(c6516,int0)
& fact(c6516,real)
& gener(c6516,sp)
& quant(c6516,one)
& refer(c6516,indet)
& varia(c6516,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(s__374dafrika_0,fe)
& sort(c6519,ta)
& card(c6519,int1)
& etype(c6519,int0)
& fact(c6519,real)
& gener(c6519,sp)
& quant(c6519,one)
& refer(c6519,det)
& varia(c6519,con)
& sort(montag__1_1,ta)
& card(montag__1_1,int1)
& etype(montag__1_1,int0)
& fact(montag__1_1,real)
& gener(montag__1_1,ge)
& quant(montag__1_1,one)
& refer(montag__1_1,refer_c)
& varia(montag__1_1,varia_c)
& sort(c6528,m)
& sort(c6528,ta)
& card(c6528,card_c)
& etype(c6528,etype_c)
& fact(c6528,real)
& gener(c6528,gener_c)
& quant(c6528,quant_c)
& refer(c6528,refer_c)
& varia(c6528,varia_c)
& sort(c6523,nu)
& card(c6523,int342)
& sort(jahr__1_1,me)
& sort(jahr__1_1,oa)
& sort(jahr__1_1,ta)
& card(jahr__1_1,card_c)
& etype(jahr__1_1,etype_c)
& fact(jahr__1_1,real)
& gener(jahr__1_1,ge)
& quant(jahr__1_1,quant_c)
& refer(jahr__1_1,refer_c)
& varia(jahr__1_1,varia_c)
& sort(c6529,ad)
& card(c6529,int1)
& etype(c6529,int0)
& fact(c6529,real)
& gener(c6529,sp)
& quant(c6529,one)
& refer(c6529,det)
& varia(c6529,con)
& sort(c6536,d)
& card(c6536,int1)
& etype(c6536,int1)
& fact(c6536,real)
& gener(c6536,sp)
& quant(c6536,one)
& refer(c6536,det)
& varia(c6536,con)
& sort(hegemonie_1_1,ad)
& card(hegemonie_1_1,int1)
& etype(hegemonie_1_1,int0)
& fact(hegemonie_1_1,real)
& gener(hegemonie_1_1,ge)
& quant(hegemonie_1_1,one)
& refer(hegemonie_1_1,refer_c)
& varia(hegemonie_1_1,varia_c)
& sort(wei__337_1_1,nq)
& sort(minderheit_1_2,d)
& card(minderheit_1_2,card_c)
& etype(minderheit_1_2,int1)
& fact(minderheit_1_2,real)
& gener(minderheit_1_2,ge)
& quant(minderheit_1_2,quant_c)
& refer(minderheit_1_2,refer_c)
& varia(minderheit_1_2,varia_c)
& sort(c6617,ent)
& card(c6617,card_c)
& etype(c6617,etype_c)
& fact(c6617,real)
& gener(c6617,gener_c)
& quant(c6617,quant_c)
& refer(c6617,refer_c)
& varia(c6617,varia_c)
& sort(pr__344_1_1,ent)
& card(pr__344_1_1,card_c)
& etype(pr__344_1_1,etype_c)
& fact(pr__344_1_1,real)
& gener(pr__344_1_1,gener_c)
& quant(pr__344_1_1,quant_c)
& refer(pr__344_1_1,refer_c)
& varia(pr__344_1_1,varia_c)
& sort(dominanz_1_1,ad)
& card(dominanz_1_1,int1)
& etype(dominanz_1_1,int0)
& fact(dominanz_1_1,real)
& gener(dominanz_1_1,ge)
& quant(dominanz_1_1,one)
& refer(dominanz_1_1,refer_c)
& varia(dominanz_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10192,plain,
( assoc(apartheidsstaat_1_1,apartheid_1_1)
& sub(apartheidsstaat_1_1,land_1_1)
& attr(c6477,c6478)
& attr(c6477,c6479)
& sub(c6477,mensch_1_1)
& sub(c6478,eigenname_1_1)
& val(c6478,nelson_0)
& sub(c6479,familiename_1_1)
& val(c6479,mandela_0)
& prop(c6485,schwarz_1_1)
& sub(c6485,c6492)
& pmod(c6492,erst_1_1,pr__344sident_1_1)
& sub(c6496,abschlu__337_1_1)
& attch(c6499,c6496)
& sub(c6499,apartheidsstaat_1_1)
& sub(c6500,von_2_1)
& attr(c6506,c6507)
& attr(c6506,c6508)
& sub(c6506,mensch_1_1)
& sub(c6507,eigenname_1_1)
& val(c6507,hans_0)
& sub(c6508,familiename_1_1)
& val(c6508,brandt_0)
& sub(c6509,in_2_1)
& attr(c6515,c6516)
& sub(c6515,land_1_1)
& sub(c6516,name_1_1)
& val(c6516,s__374dafrika_0)
& sub(c6519,montag__1_1)
& quant_p3(c6528,c6523,jahr__1_1)
& agt(c6529,c6536)
& subs(c6529,hegemonie_1_1)
& prop(c6536,wei__337_1_1)
& sub(c6536,minderheit_1_2)
& assoc(hegemonie_1_1,pr__344_1_1)
& subs(hegemonie_1_1,dominanz_1_1)
& sort(apartheidsstaat_1_1,d)
& sort(apartheidsstaat_1_1,io)
& card(apartheidsstaat_1_1,int1)
& etype(apartheidsstaat_1_1,int0)
& fact(apartheidsstaat_1_1,real)
& gener(apartheidsstaat_1_1,ge)
& quant(apartheidsstaat_1_1,one)
& refer(apartheidsstaat_1_1,refer_c)
& varia(apartheidsstaat_1_1,varia_c)
& sort(apartheid_1_1,io)
& card(apartheid_1_1,int1)
& etype(apartheid_1_1,int0)
& fact(apartheid_1_1,real)
& gener(apartheid_1_1,ge)
& quant(apartheid_1_1,one)
& refer(apartheid_1_1,refer_c)
& varia(apartheid_1_1,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(c6477,d)
& card(c6477,int1)
& etype(c6477,int0)
& fact(c6477,real)
& gener(c6477,sp)
& quant(c6477,one)
& refer(c6477,det)
& varia(c6477,con)
& sort(c6478,na)
& card(c6478,int1)
& etype(c6478,int0)
& fact(c6478,real)
& gener(c6478,sp)
& quant(c6478,one)
& refer(c6478,indet)
& varia(c6478,varia_c)
& sort(c6479,na)
& card(c6479,int1)
& etype(c6479,int0)
& fact(c6479,real)
& gener(c6479,sp)
& quant(c6479,one)
& refer(c6479,indet)
& varia(c6479,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(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(c6485,d)
& card(c6485,int1)
& etype(c6485,int0)
& fact(c6485,real)
& gener(c6485,sp)
& quant(c6485,one)
& refer(c6485,det)
& varia(c6485,con)
& sort(schwarz_1_1,tq)
& sort(c6492,d)
& card(c6492,int1)
& etype(c6492,int0)
& fact(c6492,real)
& gener(c6492,ge)
& quant(c6492,one)
& refer(c6492,refer_c)
& varia(c6492,varia_c)
& sort(erst_1_1,oq)
& card(erst_1_1,int1)
& 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(c6496,ad)
& sort(c6496,io)
& card(c6496,int1)
& etype(c6496,int0)
& fact(c6496,real)
& gener(c6496,sp)
& quant(c6496,one)
& refer(c6496,det)
& varia(c6496,varia_c)
& sort(abschlu__337_1_1,ad)
& sort(abschlu__337_1_1,io)
& card(abschlu__337_1_1,int1)
& etype(abschlu__337_1_1,int0)
& fact(abschlu__337_1_1,real)
& gener(abschlu__337_1_1,ge)
& quant(abschlu__337_1_1,one)
& refer(abschlu__337_1_1,refer_c)
& varia(abschlu__337_1_1,varia_c)
& sort(c6499,d)
& sort(c6499,io)
& card(c6499,int1)
& etype(c6499,int0)
& fact(c6499,real)
& gener(c6499,sp)
& quant(c6499,one)
& refer(c6499,det)
& varia(c6499,con)
& sort(c6500,o)
& card(c6500,int1)
& etype(c6500,int0)
& fact(c6500,real)
& gener(c6500,gener_c)
& quant(c6500,one)
& refer(c6500,refer_c)
& varia(c6500,varia_c)
& sort(von_2_1,o)
& card(von_2_1,int1)
& etype(von_2_1,int0)
& fact(von_2_1,real)
& gener(von_2_1,ge)
& quant(von_2_1,one)
& refer(von_2_1,refer_c)
& varia(von_2_1,varia_c)
& sort(c6506,d)
& card(c6506,int1)
& etype(c6506,int0)
& fact(c6506,real)
& gener(c6506,sp)
& quant(c6506,one)
& refer(c6506,det)
& varia(c6506,con)
& sort(c6507,na)
& card(c6507,int1)
& etype(c6507,int0)
& fact(c6507,real)
& gener(c6507,sp)
& quant(c6507,one)
& refer(c6507,indet)
& varia(c6507,varia_c)
& sort(c6508,na)
& card(c6508,int1)
& etype(c6508,int0)
& fact(c6508,real)
& gener(c6508,sp)
& quant(c6508,one)
& refer(c6508,indet)
& varia(c6508,varia_c)
& sort(hans_0,fe)
& sort(brandt_0,fe)
& sort(c6509,o)
& card(c6509,int1)
& etype(c6509,int0)
& fact(c6509,real)
& gener(c6509,gener_c)
& quant(c6509,one)
& refer(c6509,refer_c)
& varia(c6509,varia_c)
& sort(in_2_1,o)
& card(in_2_1,int1)
& etype(in_2_1,int0)
& fact(in_2_1,real)
& gener(in_2_1,ge)
& quant(in_2_1,one)
& refer(in_2_1,refer_c)
& varia(in_2_1,varia_c)
& sort(c6515,d)
& sort(c6515,io)
& card(c6515,int1)
& etype(c6515,int0)
& fact(c6515,real)
& gener(c6515,sp)
& quant(c6515,one)
& refer(c6515,det)
& varia(c6515,con)
& sort(c6516,na)
& card(c6516,int1)
& etype(c6516,int0)
& fact(c6516,real)
& gener(c6516,sp)
& quant(c6516,one)
& refer(c6516,indet)
& varia(c6516,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(s__374dafrika_0,fe)
& sort(c6519,ta)
& card(c6519,int1)
& etype(c6519,int0)
& fact(c6519,real)
& gener(c6519,sp)
& quant(c6519,one)
& refer(c6519,det)
& varia(c6519,con)
& sort(montag__1_1,ta)
& card(montag__1_1,int1)
& etype(montag__1_1,int0)
& fact(montag__1_1,real)
& gener(montag__1_1,ge)
& quant(montag__1_1,one)
& refer(montag__1_1,refer_c)
& varia(montag__1_1,varia_c)
& sort(c6528,m)
& sort(c6528,ta)
& card(c6528,card_c)
& etype(c6528,etype_c)
& fact(c6528,real)
& gener(c6528,gener_c)
& quant(c6528,quant_c)
& refer(c6528,refer_c)
& varia(c6528,varia_c)
& sort(c6523,nu)
& card(c6523,int342)
& sort(jahr__1_1,me)
& sort(jahr__1_1,oa)
& sort(jahr__1_1,ta)
& card(jahr__1_1,card_c)
& etype(jahr__1_1,etype_c)
& fact(jahr__1_1,real)
& gener(jahr__1_1,ge)
& quant(jahr__1_1,quant_c)
& refer(jahr__1_1,refer_c)
& varia(jahr__1_1,varia_c)
& sort(c6529,ad)
& card(c6529,int1)
& etype(c6529,int0)
& fact(c6529,real)
& gener(c6529,sp)
& quant(c6529,one)
& refer(c6529,det)
& varia(c6529,con)
& sort(c6536,d)
& card(c6536,int1)
& etype(c6536,int1)
& fact(c6536,real)
& gener(c6536,sp)
& quant(c6536,one)
& refer(c6536,det)
& varia(c6536,con)
& sort(hegemonie_1_1,ad)
& card(hegemonie_1_1,int1)
& etype(hegemonie_1_1,int0)
& fact(hegemonie_1_1,real)
& gener(hegemonie_1_1,ge)
& quant(hegemonie_1_1,one)
& refer(hegemonie_1_1,refer_c)
& varia(hegemonie_1_1,varia_c)
& sort(wei__337_1_1,nq)
& sort(minderheit_1_2,d)
& card(minderheit_1_2,card_c)
& etype(minderheit_1_2,int1)
& fact(minderheit_1_2,real)
& gener(minderheit_1_2,ge)
& quant(minderheit_1_2,quant_c)
& refer(minderheit_1_2,refer_c)
& varia(minderheit_1_2,varia_c)
& sort(c6617,ent)
& card(c6617,card_c)
& etype(c6617,etype_c)
& fact(c6617,real)
& gener(c6617,gener_c)
& quant(c6617,quant_c)
& refer(c6617,refer_c)
& varia(c6617,varia_c)
& sort(pr__344_1_1,ent)
& card(pr__344_1_1,card_c)
& etype(pr__344_1_1,etype_c)
& fact(pr__344_1_1,real)
& gener(pr__344_1_1,gener_c)
& quant(pr__344_1_1,quant_c)
& refer(pr__344_1_1,refer_c)
& varia(pr__344_1_1,varia_c)
& sort(dominanz_1_1,ad)
& card(dominanz_1_1,int1)
& etype(dominanz_1_1,int0)
& fact(dominanz_1_1,real)
& gener(dominanz_1_1,ge)
& quant(dominanz_1_1,one)
& refer(dominanz_1_1,refer_c)
& varia(dominanz_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10193,plain,
( assoc(apartheidsstaat_1_1,apartheid_1_1)
& sub(apartheidsstaat_1_1,land_1_1)
& attr(c6477,c6478)
& attr(c6477,c6479)
& sub(c6477,mensch_1_1)
& sub(c6478,eigenname_1_1)
& val(c6478,nelson_0)
& sub(c6479,familiename_1_1)
& val(c6479,mandela_0)
& prop(c6485,schwarz_1_1)
& sub(c6485,c6492)
& pmod(c6492,erst_1_1,pr__344sident_1_1)
& sub(c6496,abschlu__337_1_1)
& attch(c6499,c6496)
& sub(c6499,apartheidsstaat_1_1)
& sub(c6500,von_2_1)
& attr(c6506,c6507)
& attr(c6506,c6508)
& sub(c6506,mensch_1_1)
& sub(c6507,eigenname_1_1)
& val(c6507,hans_0)
& sub(c6508,familiename_1_1)
& val(c6508,brandt_0)
& sub(c6509,in_2_1)
& attr(c6515,c6516)
& sub(c6515,land_1_1)
& sub(c6516,name_1_1)
& val(c6516,s__374dafrika_0)
& sub(c6519,montag__1_1)
& agt(c6529,c6536)
& subs(c6529,hegemonie_1_1)
& prop(c6536,wei__337_1_1)
& sub(c6536,minderheit_1_2)
& assoc(hegemonie_1_1,pr__344_1_1)
& subs(hegemonie_1_1,dominanz_1_1)
& sort(apartheidsstaat_1_1,d)
& sort(apartheidsstaat_1_1,io)
& card(apartheidsstaat_1_1,int1)
& etype(apartheidsstaat_1_1,int0)
& fact(apartheidsstaat_1_1,real)
& gener(apartheidsstaat_1_1,ge)
& quant(apartheidsstaat_1_1,one)
& refer(apartheidsstaat_1_1,refer_c)
& varia(apartheidsstaat_1_1,varia_c)
& sort(apartheid_1_1,io)
& card(apartheid_1_1,int1)
& etype(apartheid_1_1,int0)
& fact(apartheid_1_1,real)
& gener(apartheid_1_1,ge)
& quant(apartheid_1_1,one)
& refer(apartheid_1_1,refer_c)
& varia(apartheid_1_1,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(c6477,d)
& card(c6477,int1)
& etype(c6477,int0)
& fact(c6477,real)
& gener(c6477,sp)
& quant(c6477,one)
& refer(c6477,det)
& varia(c6477,con)
& sort(c6478,na)
& card(c6478,int1)
& etype(c6478,int0)
& fact(c6478,real)
& gener(c6478,sp)
& quant(c6478,one)
& refer(c6478,indet)
& varia(c6478,varia_c)
& sort(c6479,na)
& card(c6479,int1)
& etype(c6479,int0)
& fact(c6479,real)
& gener(c6479,sp)
& quant(c6479,one)
& refer(c6479,indet)
& varia(c6479,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(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(c6485,d)
& card(c6485,int1)
& etype(c6485,int0)
& fact(c6485,real)
& gener(c6485,sp)
& quant(c6485,one)
& refer(c6485,det)
& varia(c6485,con)
& sort(schwarz_1_1,tq)
& sort(c6492,d)
& card(c6492,int1)
& etype(c6492,int0)
& fact(c6492,real)
& gener(c6492,ge)
& quant(c6492,one)
& refer(c6492,refer_c)
& varia(c6492,varia_c)
& sort(erst_1_1,oq)
& card(erst_1_1,int1)
& 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(c6496,ad)
& sort(c6496,io)
& card(c6496,int1)
& etype(c6496,int0)
& fact(c6496,real)
& gener(c6496,sp)
& quant(c6496,one)
& refer(c6496,det)
& varia(c6496,varia_c)
& sort(abschlu__337_1_1,ad)
& sort(abschlu__337_1_1,io)
& card(abschlu__337_1_1,int1)
& etype(abschlu__337_1_1,int0)
& fact(abschlu__337_1_1,real)
& gener(abschlu__337_1_1,ge)
& quant(abschlu__337_1_1,one)
& refer(abschlu__337_1_1,refer_c)
& varia(abschlu__337_1_1,varia_c)
& sort(c6499,d)
& sort(c6499,io)
& card(c6499,int1)
& etype(c6499,int0)
& fact(c6499,real)
& gener(c6499,sp)
& quant(c6499,one)
& refer(c6499,det)
& varia(c6499,con)
& sort(c6500,o)
& card(c6500,int1)
& etype(c6500,int0)
& fact(c6500,real)
& gener(c6500,gener_c)
& quant(c6500,one)
& refer(c6500,refer_c)
& varia(c6500,varia_c)
& sort(von_2_1,o)
& card(von_2_1,int1)
& etype(von_2_1,int0)
& fact(von_2_1,real)
& gener(von_2_1,ge)
& quant(von_2_1,one)
& refer(von_2_1,refer_c)
& varia(von_2_1,varia_c)
& sort(c6506,d)
& card(c6506,int1)
& etype(c6506,int0)
& fact(c6506,real)
& gener(c6506,sp)
& quant(c6506,one)
& refer(c6506,det)
& varia(c6506,con)
& sort(c6507,na)
& card(c6507,int1)
& etype(c6507,int0)
& fact(c6507,real)
& gener(c6507,sp)
& quant(c6507,one)
& refer(c6507,indet)
& varia(c6507,varia_c)
& sort(c6508,na)
& card(c6508,int1)
& etype(c6508,int0)
& fact(c6508,real)
& gener(c6508,sp)
& quant(c6508,one)
& refer(c6508,indet)
& varia(c6508,varia_c)
& sort(hans_0,fe)
& sort(brandt_0,fe)
& sort(c6509,o)
& card(c6509,int1)
& etype(c6509,int0)
& fact(c6509,real)
& gener(c6509,gener_c)
& quant(c6509,one)
& refer(c6509,refer_c)
& varia(c6509,varia_c)
& sort(in_2_1,o)
& card(in_2_1,int1)
& etype(in_2_1,int0)
& fact(in_2_1,real)
& gener(in_2_1,ge)
& quant(in_2_1,one)
& refer(in_2_1,refer_c)
& varia(in_2_1,varia_c)
& sort(c6515,d)
& sort(c6515,io)
& card(c6515,int1)
& etype(c6515,int0)
& fact(c6515,real)
& gener(c6515,sp)
& quant(c6515,one)
& refer(c6515,det)
& varia(c6515,con)
& sort(c6516,na)
& card(c6516,int1)
& etype(c6516,int0)
& fact(c6516,real)
& gener(c6516,sp)
& quant(c6516,one)
& refer(c6516,indet)
& varia(c6516,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(s__374dafrika_0,fe)
& sort(c6519,ta)
& card(c6519,int1)
& etype(c6519,int0)
& fact(c6519,real)
& gener(c6519,sp)
& quant(c6519,one)
& refer(c6519,det)
& varia(c6519,con)
& sort(montag__1_1,ta)
& card(montag__1_1,int1)
& etype(montag__1_1,int0)
& fact(montag__1_1,real)
& gener(montag__1_1,ge)
& quant(montag__1_1,one)
& refer(montag__1_1,refer_c)
& varia(montag__1_1,varia_c)
& sort(c6528,m)
& sort(c6528,ta)
& card(c6528,card_c)
& etype(c6528,etype_c)
& fact(c6528,real)
& gener(c6528,gener_c)
& quant(c6528,quant_c)
& refer(c6528,refer_c)
& varia(c6528,varia_c)
& sort(c6523,nu)
& card(c6523,int342)
& sort(jahr__1_1,me)
& sort(jahr__1_1,oa)
& sort(jahr__1_1,ta)
& card(jahr__1_1,card_c)
& etype(jahr__1_1,etype_c)
& fact(jahr__1_1,real)
& gener(jahr__1_1,ge)
& quant(jahr__1_1,quant_c)
& refer(jahr__1_1,refer_c)
& varia(jahr__1_1,varia_c)
& sort(c6529,ad)
& card(c6529,int1)
& etype(c6529,int0)
& fact(c6529,real)
& gener(c6529,sp)
& quant(c6529,one)
& refer(c6529,det)
& varia(c6529,con)
& sort(c6536,d)
& card(c6536,int1)
& etype(c6536,int1)
& fact(c6536,real)
& gener(c6536,sp)
& quant(c6536,one)
& refer(c6536,det)
& varia(c6536,con)
& sort(hegemonie_1_1,ad)
& card(hegemonie_1_1,int1)
& etype(hegemonie_1_1,int0)
& fact(hegemonie_1_1,real)
& gener(hegemonie_1_1,ge)
& quant(hegemonie_1_1,one)
& refer(hegemonie_1_1,refer_c)
& varia(hegemonie_1_1,varia_c)
& sort(wei__337_1_1,nq)
& sort(minderheit_1_2,d)
& card(minderheit_1_2,card_c)
& etype(minderheit_1_2,int1)
& fact(minderheit_1_2,real)
& gener(minderheit_1_2,ge)
& quant(minderheit_1_2,quant_c)
& refer(minderheit_1_2,refer_c)
& varia(minderheit_1_2,varia_c)
& sort(c6617,ent)
& card(c6617,card_c)
& etype(c6617,etype_c)
& fact(c6617,real)
& gener(c6617,gener_c)
& quant(c6617,quant_c)
& refer(c6617,refer_c)
& varia(c6617,varia_c)
& sort(pr__344_1_1,ent)
& card(pr__344_1_1,card_c)
& etype(pr__344_1_1,etype_c)
& fact(pr__344_1_1,real)
& gener(pr__344_1_1,gener_c)
& quant(pr__344_1_1,quant_c)
& refer(pr__344_1_1,refer_c)
& varia(pr__344_1_1,varia_c)
& sort(dominanz_1_1,ad)
& card(dominanz_1_1,int1)
& etype(dominanz_1_1,int0)
& fact(dominanz_1_1,real)
& gener(dominanz_1_1,ge)
& quant(dominanz_1_1,one)
& refer(dominanz_1_1,refer_c)
& varia(dominanz_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10192]) ).
fof(f10329,plain,
( assoc(apartheidsstaat_1_1,apartheid_1_1)
& sub(apartheidsstaat_1_1,land_1_1)
& attr(c6477,c6478)
& attr(c6477,c6479)
& sub(c6477,mensch_1_1)
& sub(c6478,eigenname_1_1)
& val(c6478,nelson_0)
& sub(c6479,familiename_1_1)
& val(c6479,mandela_0)
& prop(c6485,schwarz_1_1)
& sub(c6485,c6492)
& pmod(c6492,erst_1_1,pr__344sident_1_1)
& sub(c6496,abschlu__337_1_1)
& attch(c6499,c6496)
& sub(c6499,apartheidsstaat_1_1)
& sub(c6500,von_2_1)
& attr(c6506,c6507)
& attr(c6506,c6508)
& sub(c6506,mensch_1_1)
& sub(c6507,eigenname_1_1)
& val(c6507,hans_0)
& sub(c6508,familiename_1_1)
& val(c6508,brandt_0)
& sub(c6509,in_2_1)
& attr(c6515,c6516)
& sub(c6515,land_1_1)
& sub(c6516,name_1_1)
& val(c6516,s__374dafrika_0)
& sub(c6519,montag__1_1)
& agt(c6529,c6536)
& subs(c6529,hegemonie_1_1)
& prop(c6536,wei__337_1_1)
& sub(c6536,minderheit_1_2)
& assoc(hegemonie_1_1,pr__344_1_1)
& subs(hegemonie_1_1,dominanz_1_1)
& card(apartheidsstaat_1_1,int1)
& etype(apartheidsstaat_1_1,int0)
& fact(apartheidsstaat_1_1,real)
& gener(apartheidsstaat_1_1,ge)
& quant(apartheidsstaat_1_1,one)
& refer(apartheidsstaat_1_1,refer_c)
& varia(apartheidsstaat_1_1,varia_c)
& card(apartheid_1_1,int1)
& etype(apartheid_1_1,int0)
& fact(apartheid_1_1,real)
& gener(apartheid_1_1,ge)
& quant(apartheid_1_1,one)
& refer(apartheid_1_1,refer_c)
& varia(apartheid_1_1,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(c6477,int1)
& etype(c6477,int0)
& fact(c6477,real)
& gener(c6477,sp)
& quant(c6477,one)
& refer(c6477,det)
& varia(c6477,con)
& card(c6478,int1)
& etype(c6478,int0)
& fact(c6478,real)
& gener(c6478,sp)
& quant(c6478,one)
& refer(c6478,indet)
& varia(c6478,varia_c)
& card(c6479,int1)
& etype(c6479,int0)
& fact(c6479,real)
& gener(c6479,sp)
& quant(c6479,one)
& refer(c6479,indet)
& varia(c6479,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(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(c6485,int1)
& etype(c6485,int0)
& fact(c6485,real)
& gener(c6485,sp)
& quant(c6485,one)
& refer(c6485,det)
& varia(c6485,con)
& card(c6492,int1)
& etype(c6492,int0)
& fact(c6492,real)
& gener(c6492,ge)
& quant(c6492,one)
& refer(c6492,refer_c)
& varia(c6492,varia_c)
& card(erst_1_1,int1)
& 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(c6496,int1)
& etype(c6496,int0)
& fact(c6496,real)
& gener(c6496,sp)
& quant(c6496,one)
& refer(c6496,det)
& varia(c6496,varia_c)
& card(abschlu__337_1_1,int1)
& etype(abschlu__337_1_1,int0)
& fact(abschlu__337_1_1,real)
& gener(abschlu__337_1_1,ge)
& quant(abschlu__337_1_1,one)
& refer(abschlu__337_1_1,refer_c)
& varia(abschlu__337_1_1,varia_c)
& card(c6499,int1)
& etype(c6499,int0)
& fact(c6499,real)
& gener(c6499,sp)
& quant(c6499,one)
& refer(c6499,det)
& varia(c6499,con)
& card(c6500,int1)
& etype(c6500,int0)
& fact(c6500,real)
& gener(c6500,gener_c)
& quant(c6500,one)
& refer(c6500,refer_c)
& varia(c6500,varia_c)
& card(von_2_1,int1)
& etype(von_2_1,int0)
& fact(von_2_1,real)
& gener(von_2_1,ge)
& quant(von_2_1,one)
& refer(von_2_1,refer_c)
& varia(von_2_1,varia_c)
& card(c6506,int1)
& etype(c6506,int0)
& fact(c6506,real)
& gener(c6506,sp)
& quant(c6506,one)
& refer(c6506,det)
& varia(c6506,con)
& card(c6507,int1)
& etype(c6507,int0)
& fact(c6507,real)
& gener(c6507,sp)
& quant(c6507,one)
& refer(c6507,indet)
& varia(c6507,varia_c)
& card(c6508,int1)
& etype(c6508,int0)
& fact(c6508,real)
& gener(c6508,sp)
& quant(c6508,one)
& refer(c6508,indet)
& varia(c6508,varia_c)
& card(c6509,int1)
& etype(c6509,int0)
& fact(c6509,real)
& gener(c6509,gener_c)
& quant(c6509,one)
& refer(c6509,refer_c)
& varia(c6509,varia_c)
& card(in_2_1,int1)
& etype(in_2_1,int0)
& fact(in_2_1,real)
& gener(in_2_1,ge)
& quant(in_2_1,one)
& refer(in_2_1,refer_c)
& varia(in_2_1,varia_c)
& card(c6515,int1)
& etype(c6515,int0)
& fact(c6515,real)
& gener(c6515,sp)
& quant(c6515,one)
& refer(c6515,det)
& varia(c6515,con)
& card(c6516,int1)
& etype(c6516,int0)
& fact(c6516,real)
& gener(c6516,sp)
& quant(c6516,one)
& refer(c6516,indet)
& varia(c6516,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(c6519,int1)
& etype(c6519,int0)
& fact(c6519,real)
& gener(c6519,sp)
& quant(c6519,one)
& refer(c6519,det)
& varia(c6519,con)
& card(montag__1_1,int1)
& etype(montag__1_1,int0)
& fact(montag__1_1,real)
& gener(montag__1_1,ge)
& quant(montag__1_1,one)
& refer(montag__1_1,refer_c)
& varia(montag__1_1,varia_c)
& card(c6528,card_c)
& etype(c6528,etype_c)
& fact(c6528,real)
& gener(c6528,gener_c)
& quant(c6528,quant_c)
& refer(c6528,refer_c)
& varia(c6528,varia_c)
& card(c6523,int342)
& card(jahr__1_1,card_c)
& etype(jahr__1_1,etype_c)
& fact(jahr__1_1,real)
& gener(jahr__1_1,ge)
& quant(jahr__1_1,quant_c)
& refer(jahr__1_1,refer_c)
& varia(jahr__1_1,varia_c)
& card(c6529,int1)
& etype(c6529,int0)
& fact(c6529,real)
& gener(c6529,sp)
& quant(c6529,one)
& refer(c6529,det)
& varia(c6529,con)
& card(c6536,int1)
& etype(c6536,int1)
& fact(c6536,real)
& gener(c6536,sp)
& quant(c6536,one)
& refer(c6536,det)
& varia(c6536,con)
& card(hegemonie_1_1,int1)
& etype(hegemonie_1_1,int0)
& fact(hegemonie_1_1,real)
& gener(hegemonie_1_1,ge)
& quant(hegemonie_1_1,one)
& refer(hegemonie_1_1,refer_c)
& varia(hegemonie_1_1,varia_c)
& card(minderheit_1_2,card_c)
& etype(minderheit_1_2,int1)
& fact(minderheit_1_2,real)
& gener(minderheit_1_2,ge)
& quant(minderheit_1_2,quant_c)
& refer(minderheit_1_2,refer_c)
& varia(minderheit_1_2,varia_c)
& card(c6617,card_c)
& etype(c6617,etype_c)
& fact(c6617,real)
& gener(c6617,gener_c)
& quant(c6617,quant_c)
& refer(c6617,refer_c)
& varia(c6617,varia_c)
& card(pr__344_1_1,card_c)
& etype(pr__344_1_1,etype_c)
& fact(pr__344_1_1,real)
& gener(pr__344_1_1,gener_c)
& quant(pr__344_1_1,quant_c)
& refer(pr__344_1_1,refer_c)
& varia(pr__344_1_1,varia_c)
& card(dominanz_1_1,int1)
& etype(dominanz_1_1,int0)
& fact(dominanz_1_1,real)
& gener(dominanz_1_1,ge)
& quant(dominanz_1_1,one)
& refer(dominanz_1_1,refer_c)
& varia(dominanz_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10193]) ).
fof(f10332,plain,
( assoc(apartheidsstaat_1_1,apartheid_1_1)
& sub(apartheidsstaat_1_1,land_1_1)
& attr(c6477,c6478)
& attr(c6477,c6479)
& sub(c6477,mensch_1_1)
& sub(c6478,eigenname_1_1)
& val(c6478,nelson_0)
& sub(c6479,familiename_1_1)
& val(c6479,mandela_0)
& prop(c6485,schwarz_1_1)
& sub(c6485,c6492)
& pmod(c6492,erst_1_1,pr__344sident_1_1)
& sub(c6496,abschlu__337_1_1)
& attch(c6499,c6496)
& sub(c6499,apartheidsstaat_1_1)
& sub(c6500,von_2_1)
& attr(c6506,c6507)
& attr(c6506,c6508)
& sub(c6506,mensch_1_1)
& sub(c6507,eigenname_1_1)
& val(c6507,hans_0)
& sub(c6508,familiename_1_1)
& val(c6508,brandt_0)
& sub(c6509,in_2_1)
& attr(c6515,c6516)
& sub(c6515,land_1_1)
& sub(c6516,name_1_1)
& val(c6516,s__374dafrika_0)
& sub(c6519,montag__1_1)
& agt(c6529,c6536)
& subs(c6529,hegemonie_1_1)
& prop(c6536,wei__337_1_1)
& sub(c6536,minderheit_1_2)
& assoc(hegemonie_1_1,pr__344_1_1)
& subs(hegemonie_1_1,dominanz_1_1)
& card(apartheidsstaat_1_1,int1)
& etype(apartheidsstaat_1_1,int0)
& fact(apartheidsstaat_1_1,real)
& gener(apartheidsstaat_1_1,ge)
& refer(apartheidsstaat_1_1,refer_c)
& varia(apartheidsstaat_1_1,varia_c)
& card(apartheid_1_1,int1)
& etype(apartheid_1_1,int0)
& fact(apartheid_1_1,real)
& gener(apartheid_1_1,ge)
& refer(apartheid_1_1,refer_c)
& varia(apartheid_1_1,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(c6477,int1)
& etype(c6477,int0)
& fact(c6477,real)
& gener(c6477,sp)
& refer(c6477,det)
& varia(c6477,con)
& card(c6478,int1)
& etype(c6478,int0)
& fact(c6478,real)
& gener(c6478,sp)
& refer(c6478,indet)
& varia(c6478,varia_c)
& card(c6479,int1)
& etype(c6479,int0)
& fact(c6479,real)
& gener(c6479,sp)
& refer(c6479,indet)
& varia(c6479,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(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(c6485,int1)
& etype(c6485,int0)
& fact(c6485,real)
& gener(c6485,sp)
& refer(c6485,det)
& varia(c6485,con)
& card(c6492,int1)
& etype(c6492,int0)
& fact(c6492,real)
& gener(c6492,ge)
& refer(c6492,refer_c)
& varia(c6492,varia_c)
& card(erst_1_1,int1)
& 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(c6496,int1)
& etype(c6496,int0)
& fact(c6496,real)
& gener(c6496,sp)
& refer(c6496,det)
& varia(c6496,varia_c)
& card(abschlu__337_1_1,int1)
& etype(abschlu__337_1_1,int0)
& fact(abschlu__337_1_1,real)
& gener(abschlu__337_1_1,ge)
& refer(abschlu__337_1_1,refer_c)
& varia(abschlu__337_1_1,varia_c)
& card(c6499,int1)
& etype(c6499,int0)
& fact(c6499,real)
& gener(c6499,sp)
& refer(c6499,det)
& varia(c6499,con)
& card(c6500,int1)
& etype(c6500,int0)
& fact(c6500,real)
& gener(c6500,gener_c)
& refer(c6500,refer_c)
& varia(c6500,varia_c)
& card(von_2_1,int1)
& etype(von_2_1,int0)
& fact(von_2_1,real)
& gener(von_2_1,ge)
& refer(von_2_1,refer_c)
& varia(von_2_1,varia_c)
& card(c6506,int1)
& etype(c6506,int0)
& fact(c6506,real)
& gener(c6506,sp)
& refer(c6506,det)
& varia(c6506,con)
& card(c6507,int1)
& etype(c6507,int0)
& fact(c6507,real)
& gener(c6507,sp)
& refer(c6507,indet)
& varia(c6507,varia_c)
& card(c6508,int1)
& etype(c6508,int0)
& fact(c6508,real)
& gener(c6508,sp)
& refer(c6508,indet)
& varia(c6508,varia_c)
& card(c6509,int1)
& etype(c6509,int0)
& fact(c6509,real)
& gener(c6509,gener_c)
& refer(c6509,refer_c)
& varia(c6509,varia_c)
& card(in_2_1,int1)
& etype(in_2_1,int0)
& fact(in_2_1,real)
& gener(in_2_1,ge)
& refer(in_2_1,refer_c)
& varia(in_2_1,varia_c)
& card(c6515,int1)
& etype(c6515,int0)
& fact(c6515,real)
& gener(c6515,sp)
& refer(c6515,det)
& varia(c6515,con)
& card(c6516,int1)
& etype(c6516,int0)
& fact(c6516,real)
& gener(c6516,sp)
& refer(c6516,indet)
& varia(c6516,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(c6519,int1)
& etype(c6519,int0)
& fact(c6519,real)
& gener(c6519,sp)
& refer(c6519,det)
& varia(c6519,con)
& card(montag__1_1,int1)
& etype(montag__1_1,int0)
& fact(montag__1_1,real)
& gener(montag__1_1,ge)
& refer(montag__1_1,refer_c)
& varia(montag__1_1,varia_c)
& card(c6528,card_c)
& etype(c6528,etype_c)
& fact(c6528,real)
& gener(c6528,gener_c)
& refer(c6528,refer_c)
& varia(c6528,varia_c)
& card(c6523,int342)
& card(jahr__1_1,card_c)
& etype(jahr__1_1,etype_c)
& fact(jahr__1_1,real)
& gener(jahr__1_1,ge)
& refer(jahr__1_1,refer_c)
& varia(jahr__1_1,varia_c)
& card(c6529,int1)
& etype(c6529,int0)
& fact(c6529,real)
& gener(c6529,sp)
& refer(c6529,det)
& varia(c6529,con)
& card(c6536,int1)
& etype(c6536,int1)
& fact(c6536,real)
& gener(c6536,sp)
& refer(c6536,det)
& varia(c6536,con)
& card(hegemonie_1_1,int1)
& etype(hegemonie_1_1,int0)
& fact(hegemonie_1_1,real)
& gener(hegemonie_1_1,ge)
& refer(hegemonie_1_1,refer_c)
& varia(hegemonie_1_1,varia_c)
& card(minderheit_1_2,card_c)
& etype(minderheit_1_2,int1)
& fact(minderheit_1_2,real)
& gener(minderheit_1_2,ge)
& refer(minderheit_1_2,refer_c)
& varia(minderheit_1_2,varia_c)
& card(c6617,card_c)
& etype(c6617,etype_c)
& fact(c6617,real)
& gener(c6617,gener_c)
& refer(c6617,refer_c)
& varia(c6617,varia_c)
& card(pr__344_1_1,card_c)
& etype(pr__344_1_1,etype_c)
& fact(pr__344_1_1,real)
& gener(pr__344_1_1,gener_c)
& refer(pr__344_1_1,refer_c)
& varia(pr__344_1_1,varia_c)
& card(dominanz_1_1,int1)
& etype(dominanz_1_1,int0)
& fact(dominanz_1_1,real)
& gener(dominanz_1_1,ge)
& refer(dominanz_1_1,refer_c)
& varia(dominanz_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10329]) ).
fof(f10335,plain,
( assoc(apartheidsstaat_1_1,apartheid_1_1)
& sub(apartheidsstaat_1_1,land_1_1)
& attr(c6477,c6478)
& attr(c6477,c6479)
& sub(c6477,mensch_1_1)
& sub(c6478,eigenname_1_1)
& val(c6478,nelson_0)
& sub(c6479,familiename_1_1)
& val(c6479,mandela_0)
& prop(c6485,schwarz_1_1)
& sub(c6485,c6492)
& pmod(c6492,erst_1_1,pr__344sident_1_1)
& sub(c6496,abschlu__337_1_1)
& attch(c6499,c6496)
& sub(c6499,apartheidsstaat_1_1)
& sub(c6500,von_2_1)
& attr(c6506,c6507)
& attr(c6506,c6508)
& sub(c6506,mensch_1_1)
& sub(c6507,eigenname_1_1)
& val(c6507,hans_0)
& sub(c6508,familiename_1_1)
& val(c6508,brandt_0)
& sub(c6509,in_2_1)
& attr(c6515,c6516)
& sub(c6515,land_1_1)
& sub(c6516,name_1_1)
& val(c6516,s__374dafrika_0)
& sub(c6519,montag__1_1)
& agt(c6529,c6536)
& subs(c6529,hegemonie_1_1)
& prop(c6536,wei__337_1_1)
& sub(c6536,minderheit_1_2)
& assoc(hegemonie_1_1,pr__344_1_1)
& subs(hegemonie_1_1,dominanz_1_1)
& etype(apartheidsstaat_1_1,int0)
& fact(apartheidsstaat_1_1,real)
& gener(apartheidsstaat_1_1,ge)
& refer(apartheidsstaat_1_1,refer_c)
& varia(apartheidsstaat_1_1,varia_c)
& etype(apartheid_1_1,int0)
& fact(apartheid_1_1,real)
& gener(apartheid_1_1,ge)
& refer(apartheid_1_1,refer_c)
& varia(apartheid_1_1,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(c6477,int0)
& fact(c6477,real)
& gener(c6477,sp)
& refer(c6477,det)
& varia(c6477,con)
& etype(c6478,int0)
& fact(c6478,real)
& gener(c6478,sp)
& refer(c6478,indet)
& varia(c6478,varia_c)
& etype(c6479,int0)
& fact(c6479,real)
& gener(c6479,sp)
& refer(c6479,indet)
& varia(c6479,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(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(c6485,int0)
& fact(c6485,real)
& gener(c6485,sp)
& refer(c6485,det)
& varia(c6485,con)
& etype(c6492,int0)
& fact(c6492,real)
& gener(c6492,ge)
& refer(c6492,refer_c)
& varia(c6492,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(c6496,int0)
& fact(c6496,real)
& gener(c6496,sp)
& refer(c6496,det)
& varia(c6496,varia_c)
& etype(abschlu__337_1_1,int0)
& fact(abschlu__337_1_1,real)
& gener(abschlu__337_1_1,ge)
& refer(abschlu__337_1_1,refer_c)
& varia(abschlu__337_1_1,varia_c)
& etype(c6499,int0)
& fact(c6499,real)
& gener(c6499,sp)
& refer(c6499,det)
& varia(c6499,con)
& etype(c6500,int0)
& fact(c6500,real)
& gener(c6500,gener_c)
& refer(c6500,refer_c)
& varia(c6500,varia_c)
& etype(von_2_1,int0)
& fact(von_2_1,real)
& gener(von_2_1,ge)
& refer(von_2_1,refer_c)
& varia(von_2_1,varia_c)
& etype(c6506,int0)
& fact(c6506,real)
& gener(c6506,sp)
& refer(c6506,det)
& varia(c6506,con)
& etype(c6507,int0)
& fact(c6507,real)
& gener(c6507,sp)
& refer(c6507,indet)
& varia(c6507,varia_c)
& etype(c6508,int0)
& fact(c6508,real)
& gener(c6508,sp)
& refer(c6508,indet)
& varia(c6508,varia_c)
& etype(c6509,int0)
& fact(c6509,real)
& gener(c6509,gener_c)
& refer(c6509,refer_c)
& varia(c6509,varia_c)
& etype(in_2_1,int0)
& fact(in_2_1,real)
& gener(in_2_1,ge)
& refer(in_2_1,refer_c)
& varia(in_2_1,varia_c)
& etype(c6515,int0)
& fact(c6515,real)
& gener(c6515,sp)
& refer(c6515,det)
& varia(c6515,con)
& etype(c6516,int0)
& fact(c6516,real)
& gener(c6516,sp)
& refer(c6516,indet)
& varia(c6516,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(c6519,int0)
& fact(c6519,real)
& gener(c6519,sp)
& refer(c6519,det)
& varia(c6519,con)
& etype(montag__1_1,int0)
& fact(montag__1_1,real)
& gener(montag__1_1,ge)
& refer(montag__1_1,refer_c)
& varia(montag__1_1,varia_c)
& etype(c6528,etype_c)
& fact(c6528,real)
& gener(c6528,gener_c)
& refer(c6528,refer_c)
& varia(c6528,varia_c)
& etype(jahr__1_1,etype_c)
& fact(jahr__1_1,real)
& gener(jahr__1_1,ge)
& refer(jahr__1_1,refer_c)
& varia(jahr__1_1,varia_c)
& etype(c6529,int0)
& fact(c6529,real)
& gener(c6529,sp)
& refer(c6529,det)
& varia(c6529,con)
& etype(c6536,int1)
& fact(c6536,real)
& gener(c6536,sp)
& refer(c6536,det)
& varia(c6536,con)
& etype(hegemonie_1_1,int0)
& fact(hegemonie_1_1,real)
& gener(hegemonie_1_1,ge)
& refer(hegemonie_1_1,refer_c)
& varia(hegemonie_1_1,varia_c)
& etype(minderheit_1_2,int1)
& fact(minderheit_1_2,real)
& gener(minderheit_1_2,ge)
& refer(minderheit_1_2,refer_c)
& varia(minderheit_1_2,varia_c)
& etype(c6617,etype_c)
& fact(c6617,real)
& gener(c6617,gener_c)
& refer(c6617,refer_c)
& varia(c6617,varia_c)
& etype(pr__344_1_1,etype_c)
& fact(pr__344_1_1,real)
& gener(pr__344_1_1,gener_c)
& refer(pr__344_1_1,refer_c)
& varia(pr__344_1_1,varia_c)
& etype(dominanz_1_1,int0)
& fact(dominanz_1_1,real)
& gener(dominanz_1_1,ge)
& refer(dominanz_1_1,refer_c)
& varia(dominanz_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10332]) ).
fof(f10338,plain,
( assoc(apartheidsstaat_1_1,apartheid_1_1)
& sub(apartheidsstaat_1_1,land_1_1)
& attr(c6477,c6478)
& attr(c6477,c6479)
& sub(c6477,mensch_1_1)
& sub(c6478,eigenname_1_1)
& val(c6478,nelson_0)
& sub(c6479,familiename_1_1)
& val(c6479,mandela_0)
& prop(c6485,schwarz_1_1)
& sub(c6485,c6492)
& pmod(c6492,erst_1_1,pr__344sident_1_1)
& sub(c6496,abschlu__337_1_1)
& attch(c6499,c6496)
& sub(c6499,apartheidsstaat_1_1)
& sub(c6500,von_2_1)
& attr(c6506,c6507)
& attr(c6506,c6508)
& sub(c6506,mensch_1_1)
& sub(c6507,eigenname_1_1)
& val(c6507,hans_0)
& sub(c6508,familiename_1_1)
& val(c6508,brandt_0)
& sub(c6509,in_2_1)
& attr(c6515,c6516)
& sub(c6515,land_1_1)
& sub(c6516,name_1_1)
& val(c6516,s__374dafrika_0)
& sub(c6519,montag__1_1)
& agt(c6529,c6536)
& subs(c6529,hegemonie_1_1)
& prop(c6536,wei__337_1_1)
& sub(c6536,minderheit_1_2)
& assoc(hegemonie_1_1,pr__344_1_1)
& subs(hegemonie_1_1,dominanz_1_1)
& etype(apartheidsstaat_1_1,int0)
& fact(apartheidsstaat_1_1,real)
& gener(apartheidsstaat_1_1,ge)
& varia(apartheidsstaat_1_1,varia_c)
& etype(apartheid_1_1,int0)
& fact(apartheid_1_1,real)
& gener(apartheid_1_1,ge)
& varia(apartheid_1_1,varia_c)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& varia(land_1_1,varia_c)
& etype(c6477,int0)
& fact(c6477,real)
& gener(c6477,sp)
& varia(c6477,con)
& etype(c6478,int0)
& fact(c6478,real)
& gener(c6478,sp)
& varia(c6478,varia_c)
& etype(c6479,int0)
& fact(c6479,real)
& gener(c6479,sp)
& varia(c6479,varia_c)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& varia(mensch_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(c6485,int0)
& fact(c6485,real)
& gener(c6485,sp)
& varia(c6485,con)
& etype(c6492,int0)
& fact(c6492,real)
& gener(c6492,ge)
& varia(c6492,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(c6496,int0)
& fact(c6496,real)
& gener(c6496,sp)
& varia(c6496,varia_c)
& etype(abschlu__337_1_1,int0)
& fact(abschlu__337_1_1,real)
& gener(abschlu__337_1_1,ge)
& varia(abschlu__337_1_1,varia_c)
& etype(c6499,int0)
& fact(c6499,real)
& gener(c6499,sp)
& varia(c6499,con)
& etype(c6500,int0)
& fact(c6500,real)
& gener(c6500,gener_c)
& varia(c6500,varia_c)
& etype(von_2_1,int0)
& fact(von_2_1,real)
& gener(von_2_1,ge)
& varia(von_2_1,varia_c)
& etype(c6506,int0)
& fact(c6506,real)
& gener(c6506,sp)
& varia(c6506,con)
& etype(c6507,int0)
& fact(c6507,real)
& gener(c6507,sp)
& varia(c6507,varia_c)
& etype(c6508,int0)
& fact(c6508,real)
& gener(c6508,sp)
& varia(c6508,varia_c)
& etype(c6509,int0)
& fact(c6509,real)
& gener(c6509,gener_c)
& varia(c6509,varia_c)
& etype(in_2_1,int0)
& fact(in_2_1,real)
& gener(in_2_1,ge)
& varia(in_2_1,varia_c)
& etype(c6515,int0)
& fact(c6515,real)
& gener(c6515,sp)
& varia(c6515,con)
& etype(c6516,int0)
& fact(c6516,real)
& gener(c6516,sp)
& varia(c6516,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& varia(name_1_1,varia_c)
& etype(c6519,int0)
& fact(c6519,real)
& gener(c6519,sp)
& varia(c6519,con)
& etype(montag__1_1,int0)
& fact(montag__1_1,real)
& gener(montag__1_1,ge)
& varia(montag__1_1,varia_c)
& etype(c6528,etype_c)
& fact(c6528,real)
& gener(c6528,gener_c)
& varia(c6528,varia_c)
& etype(jahr__1_1,etype_c)
& fact(jahr__1_1,real)
& gener(jahr__1_1,ge)
& varia(jahr__1_1,varia_c)
& etype(c6529,int0)
& fact(c6529,real)
& gener(c6529,sp)
& varia(c6529,con)
& etype(c6536,int1)
& fact(c6536,real)
& gener(c6536,sp)
& varia(c6536,con)
& etype(hegemonie_1_1,int0)
& fact(hegemonie_1_1,real)
& gener(hegemonie_1_1,ge)
& varia(hegemonie_1_1,varia_c)
& etype(minderheit_1_2,int1)
& fact(minderheit_1_2,real)
& gener(minderheit_1_2,ge)
& varia(minderheit_1_2,varia_c)
& etype(c6617,etype_c)
& fact(c6617,real)
& gener(c6617,gener_c)
& varia(c6617,varia_c)
& etype(pr__344_1_1,etype_c)
& fact(pr__344_1_1,real)
& gener(pr__344_1_1,gener_c)
& varia(pr__344_1_1,varia_c)
& etype(dominanz_1_1,int0)
& fact(dominanz_1_1,real)
& gener(dominanz_1_1,ge)
& varia(dominanz_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10335]) ).
fof(f10343,plain,
( assoc(apartheidsstaat_1_1,apartheid_1_1)
& sub(apartheidsstaat_1_1,land_1_1)
& attr(c6477,c6478)
& attr(c6477,c6479)
& sub(c6477,mensch_1_1)
& sub(c6478,eigenname_1_1)
& val(c6478,nelson_0)
& sub(c6479,familiename_1_1)
& val(c6479,mandela_0)
& prop(c6485,schwarz_1_1)
& sub(c6485,c6492)
& pmod(c6492,erst_1_1,pr__344sident_1_1)
& sub(c6496,abschlu__337_1_1)
& attch(c6499,c6496)
& sub(c6499,apartheidsstaat_1_1)
& sub(c6500,von_2_1)
& attr(c6506,c6507)
& attr(c6506,c6508)
& sub(c6506,mensch_1_1)
& sub(c6507,eigenname_1_1)
& val(c6507,hans_0)
& sub(c6508,familiename_1_1)
& val(c6508,brandt_0)
& sub(c6509,in_2_1)
& attr(c6515,c6516)
& sub(c6515,land_1_1)
& sub(c6516,name_1_1)
& val(c6516,s__374dafrika_0)
& sub(c6519,montag__1_1)
& agt(c6529,c6536)
& subs(c6529,hegemonie_1_1)
& prop(c6536,wei__337_1_1)
& sub(c6536,minderheit_1_2)
& assoc(hegemonie_1_1,pr__344_1_1)
& subs(hegemonie_1_1,dominanz_1_1)
& etype(apartheidsstaat_1_1,int0)
& fact(apartheidsstaat_1_1,real)
& gener(apartheidsstaat_1_1,ge)
& etype(apartheid_1_1,int0)
& fact(apartheid_1_1,real)
& gener(apartheid_1_1,ge)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& etype(c6477,int0)
& fact(c6477,real)
& gener(c6477,sp)
& etype(c6478,int0)
& fact(c6478,real)
& gener(c6478,sp)
& etype(c6479,int0)
& fact(c6479,real)
& gener(c6479,sp)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_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(c6485,int0)
& fact(c6485,real)
& gener(c6485,sp)
& etype(c6492,int0)
& fact(c6492,real)
& gener(c6492,ge)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& etype(c6496,int0)
& fact(c6496,real)
& gener(c6496,sp)
& etype(abschlu__337_1_1,int0)
& fact(abschlu__337_1_1,real)
& gener(abschlu__337_1_1,ge)
& etype(c6499,int0)
& fact(c6499,real)
& gener(c6499,sp)
& etype(c6500,int0)
& fact(c6500,real)
& gener(c6500,gener_c)
& etype(von_2_1,int0)
& fact(von_2_1,real)
& gener(von_2_1,ge)
& etype(c6506,int0)
& fact(c6506,real)
& gener(c6506,sp)
& etype(c6507,int0)
& fact(c6507,real)
& gener(c6507,sp)
& etype(c6508,int0)
& fact(c6508,real)
& gener(c6508,sp)
& etype(c6509,int0)
& fact(c6509,real)
& gener(c6509,gener_c)
& etype(in_2_1,int0)
& fact(in_2_1,real)
& gener(in_2_1,ge)
& etype(c6515,int0)
& fact(c6515,real)
& gener(c6515,sp)
& etype(c6516,int0)
& fact(c6516,real)
& gener(c6516,sp)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& etype(c6519,int0)
& fact(c6519,real)
& gener(c6519,sp)
& etype(montag__1_1,int0)
& fact(montag__1_1,real)
& gener(montag__1_1,ge)
& etype(c6528,etype_c)
& fact(c6528,real)
& gener(c6528,gener_c)
& etype(jahr__1_1,etype_c)
& fact(jahr__1_1,real)
& gener(jahr__1_1,ge)
& etype(c6529,int0)
& fact(c6529,real)
& gener(c6529,sp)
& etype(c6536,int1)
& fact(c6536,real)
& gener(c6536,sp)
& etype(hegemonie_1_1,int0)
& fact(hegemonie_1_1,real)
& gener(hegemonie_1_1,ge)
& etype(minderheit_1_2,int1)
& fact(minderheit_1_2,real)
& gener(minderheit_1_2,ge)
& etype(c6617,etype_c)
& fact(c6617,real)
& gener(c6617,gener_c)
& etype(pr__344_1_1,etype_c)
& fact(pr__344_1_1,real)
& gener(pr__344_1_1,gener_c)
& etype(dominanz_1_1,int0)
& fact(dominanz_1_1,real)
& gener(dominanz_1_1,ge) ),
inference(pure_predicate_removal,[],[f10338]) ).
fof(f10348,plain,
( assoc(apartheidsstaat_1_1,apartheid_1_1)
& sub(apartheidsstaat_1_1,land_1_1)
& attr(c6477,c6478)
& attr(c6477,c6479)
& sub(c6477,mensch_1_1)
& sub(c6478,eigenname_1_1)
& val(c6478,nelson_0)
& sub(c6479,familiename_1_1)
& val(c6479,mandela_0)
& prop(c6485,schwarz_1_1)
& sub(c6485,c6492)
& pmod(c6492,erst_1_1,pr__344sident_1_1)
& sub(c6496,abschlu__337_1_1)
& attch(c6499,c6496)
& sub(c6499,apartheidsstaat_1_1)
& sub(c6500,von_2_1)
& attr(c6506,c6507)
& attr(c6506,c6508)
& sub(c6506,mensch_1_1)
& sub(c6507,eigenname_1_1)
& val(c6507,hans_0)
& sub(c6508,familiename_1_1)
& val(c6508,brandt_0)
& sub(c6509,in_2_1)
& attr(c6515,c6516)
& sub(c6515,land_1_1)
& sub(c6516,name_1_1)
& val(c6516,s__374dafrika_0)
& sub(c6519,montag__1_1)
& agt(c6529,c6536)
& subs(c6529,hegemonie_1_1)
& prop(c6536,wei__337_1_1)
& sub(c6536,minderheit_1_2)
& assoc(hegemonie_1_1,pr__344_1_1)
& subs(hegemonie_1_1,dominanz_1_1)
& etype(apartheidsstaat_1_1,int0)
& fact(apartheidsstaat_1_1,real)
& etype(apartheid_1_1,int0)
& fact(apartheid_1_1,real)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& etype(c6477,int0)
& fact(c6477,real)
& etype(c6478,int0)
& fact(c6478,real)
& etype(c6479,int0)
& fact(c6479,real)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& etype(c6485,int0)
& fact(c6485,real)
& etype(c6492,int0)
& fact(c6492,real)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& etype(c6496,int0)
& fact(c6496,real)
& etype(abschlu__337_1_1,int0)
& fact(abschlu__337_1_1,real)
& etype(c6499,int0)
& fact(c6499,real)
& etype(c6500,int0)
& fact(c6500,real)
& etype(von_2_1,int0)
& fact(von_2_1,real)
& etype(c6506,int0)
& fact(c6506,real)
& etype(c6507,int0)
& fact(c6507,real)
& etype(c6508,int0)
& fact(c6508,real)
& etype(c6509,int0)
& fact(c6509,real)
& etype(in_2_1,int0)
& fact(in_2_1,real)
& etype(c6515,int0)
& fact(c6515,real)
& etype(c6516,int0)
& fact(c6516,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& etype(c6519,int0)
& fact(c6519,real)
& etype(montag__1_1,int0)
& fact(montag__1_1,real)
& etype(c6528,etype_c)
& fact(c6528,real)
& etype(jahr__1_1,etype_c)
& fact(jahr__1_1,real)
& etype(c6529,int0)
& fact(c6529,real)
& etype(c6536,int1)
& fact(c6536,real)
& etype(hegemonie_1_1,int0)
& fact(hegemonie_1_1,real)
& etype(minderheit_1_2,int1)
& fact(minderheit_1_2,real)
& etype(c6617,etype_c)
& fact(c6617,real)
& etype(pr__344_1_1,etype_c)
& fact(pr__344_1_1,real)
& etype(dominanz_1_1,int0)
& fact(dominanz_1_1,real) ),
inference(pure_predicate_removal,[],[f10343]) ).
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(f10546,plain,
! [X0,X1] :
( ? [X2] :
( attr(X1,X2)
& sub(X2,name_1_1)
& val(X2,X0) )
| ~ name(X1,X0) ),
inference(ennf_transformation,[],[f177]) ).
fof(f10547,plain,
! [X0,X1,X2] :
( name(X2,X1)
| ~ attr(X2,X0)
| ~ sub(X0,name_1_1)
| ~ val(X0,X1) ),
inference(ennf_transformation,[],[f178]) ).
fof(f10548,plain,
! [X0,X1,X2] :
( name(X2,X1)
| ~ attr(X2,X0)
| ~ sub(X0,name_1_1)
| ~ val(X0,X1) ),
inference(flattening,[],[f10547]) ).
fof(f10553,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ pmod(X8,erst_1_1,pr__344sident_1_1)
| ~ arg1(X3,X0)
| ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ attr(X5,X6)
| ~ obj(X7,X0)
| ~ prop(X4,schwarz_1_1)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X8)
| ~ sub(X6,name_1_1)
| ~ subr(X3,rprs_0)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ val(X6,s__374dafrika_0) ),
inference(ennf_transformation,[],[f10189]) ).
fof(f10597,plain,
! [X0,X1,X2] :
( ( arg1(sK56(X0,X1,X2),X1)
& arg2(sK56(X0,X1,X2),sK57(X0,X1,X2))
& hsit(X0,sK55(X0,X1,X2))
& mcont(sK55(X0,X1,X2),sK56(X0,X1,X2))
& obj(sK55(X0,X1,X2),X1)
& sub(sK57(X0,X1,X2),X2)
& subr(sK56(X0,X1,X2),rprs_0)
& subs(sK55(X0,X1,X2),bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55,sK56,sK57]),skolemize(X3,sK55(X0,X1,X2)),skolemize(X4,sK56(X0,X1,X2)),skolemize(X5,sK57(X0,X1,X2))],[f10523]) ).
fof(f10598,plain,
! [X0,X1] :
( ( arg1(sK58(X0,X1),X0)
& arg2(sK58(X0,X1),X1)
& subr(sK58(X0,X1),sub_0) )
| ~ sub(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58]),skolemize(X2,sK58(X0,X1))],[f10524]) ).
fof(f10603,plain,
! [X0,X1] :
( ( attr(X1,sK61(X0,X1))
& sub(sK61(X0,X1),name_1_1)
& val(sK61(X0,X1),X0) )
| ~ name(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK61]),skolemize(X2,sK61(X0,X1))],[f10546]) ).
fof(f10881,plain,
! [X2,X0,X1] :
( subr(sK56(X0,X1,X2),rprs_0)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10597]) ).
fof(f10883,plain,
! [X2,X0,X1] :
( obj(sK55(X0,X1,X2),X1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10597]) ).
fof(f10887,plain,
! [X2,X0,X1] :
( arg1(sK56(X0,X1,X2),X1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10597]) ).
fof(f10888,plain,
! [X0,X1] :
( subr(sK58(X0,X1),sub_0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10598]) ).
fof(f10889,plain,
! [X0,X1] :
( arg2(sK58(X0,X1),X1)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10598]) ).
fof(f10890,plain,
! [X0,X1] :
( arg1(sK58(X0,X1),X0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10598]) ).
fof(f10918,plain,
! [X0,X1] :
( val(sK61(X0,X1),X0)
| ~ name(X1,X0) ),
inference(cnf_transformation,[],[f10603]) ).
fof(f10919,plain,
! [X0,X1] :
( sub(sK61(X0,X1),name_1_1)
| ~ name(X1,X0) ),
inference(cnf_transformation,[],[f10603]) ).
fof(f10920,plain,
! [X0,X1] :
( attr(X1,sK61(X0,X1))
| ~ name(X1,X0) ),
inference(cnf_transformation,[],[f10603]) ).
fof(f10921,plain,
! [X2,X0,X1] :
( ~ val(X0,X1)
| ~ attr(X2,X0)
| ~ sub(X0,name_1_1)
| name(X2,X1) ),
inference(cnf_transformation,[],[f10548]) ).
fof(f20817,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ pmod(X8,erst_1_1,pr__344sident_1_1)
| ~ arg1(X3,X0)
| ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ attr(X5,X6)
| ~ obj(X7,X0)
| ~ prop(X4,schwarz_1_1)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X8)
| ~ sub(X6,name_1_1)
| ~ subr(X3,rprs_0)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ val(X6,s__374dafrika_0) ),
inference(cnf_transformation,[],[f10553]) ).
fof(f20897,plain,
val(c6516,s__374dafrika_0),
inference(cnf_transformation,[],[f10348]) ).
fof(f20898,plain,
sub(c6516,name_1_1),
inference(cnf_transformation,[],[f10348]) ).
fof(f20900,plain,
attr(c6515,c6516),
inference(cnf_transformation,[],[f10348]) ).
fof(f20913,plain,
pmod(c6492,erst_1_1,pr__344sident_1_1),
inference(cnf_transformation,[],[f10348]) ).
fof(f20914,plain,
sub(c6485,c6492),
inference(cnf_transformation,[],[f10348]) ).
fof(f20915,plain,
prop(c6485,schwarz_1_1),
inference(cnf_transformation,[],[f10348]) ).
fof(f20916,plain,
val(c6479,mandela_0),
inference(cnf_transformation,[],[f10348]) ).
fof(f20917,plain,
sub(c6479,familiename_1_1),
inference(cnf_transformation,[],[f10348]) ).
fof(f20918,plain,
val(c6478,nelson_0),
inference(cnf_transformation,[],[f10348]) ).
fof(f20919,plain,
sub(c6478,eigenname_1_1),
inference(cnf_transformation,[],[f10348]) ).
fof(f20920,plain,
sub(c6477,mensch_1_1),
inference(cnf_transformation,[],[f10348]) ).
fof(f20921,plain,
attr(c6477,c6479),
inference(cnf_transformation,[],[f10348]) ).
fof(f20922,plain,
attr(c6477,c6478),
inference(cnf_transformation,[],[f10348]) ).
fof(f20925,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ val(X5,s__374dafrika_0)
| ~ attr(X1,X2)
| ~ attr(X1,X3)
| ~ attr(X4,X5)
| ~ obj(X6,X1)
| ~ prop(X7,schwarz_1_1)
| ~ sub(X2,familiename_1_1)
| ~ sub(X3,eigenname_1_1)
| ~ sub(X7,c6492)
| ~ sub(X5,name_1_1)
| ~ subr(X0,rprs_0)
| ~ val(X2,mandela_0)
| ~ val(X3,nelson_0)
| ~ arg1(X0,X1) ),
inference(resolution,[],[f20817,f20913]) ).
fof(f21039,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ name(X0,s__374dafrika_0)
| ~ attr(X1,X2)
| ~ attr(X1,X3)
| ~ attr(X4,sK61(s__374dafrika_0,X0))
| ~ obj(X5,X1)
| ~ prop(X6,schwarz_1_1)
| ~ sub(X2,familiename_1_1)
| ~ sub(X3,eigenname_1_1)
| ~ sub(X6,c6492)
| ~ sub(sK61(s__374dafrika_0,X0),name_1_1)
| ~ subr(X7,rprs_0)
| ~ val(X2,mandela_0)
| ~ val(X3,nelson_0)
| ~ arg1(X7,X1) ),
inference(resolution,[],[f10918,f20925]) ).
fof(f21041,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ attr(X4,sK61(s__374dafrika_0,X0))
| ~ attr(X1,X2)
| ~ attr(X1,X3)
| ~ name(X0,s__374dafrika_0)
| ~ obj(X5,X1)
| ~ prop(X6,schwarz_1_1)
| ~ sub(X2,familiename_1_1)
| ~ sub(X3,eigenname_1_1)
| ~ sub(X6,c6492)
| ~ subr(X7,rprs_0)
| ~ val(X2,mandela_0)
| ~ val(X3,nelson_0)
| ~ arg1(X7,X1) ),
inference(forward_subsumption_resolution,[],[f21039,f10919]) ).
fof(f107304,plain,
! [X0] :
( ~ attr(X0,c6516)
| ~ sub(c6516,name_1_1)
| name(X0,s__374dafrika_0) ),
inference(resolution,[],[f10921,f20897]) ).
fof(f107307,plain,
! [X0] :
( ~ attr(X0,c6516)
| name(X0,s__374dafrika_0) ),
inference(forward_subsumption_resolution,[],[f107304,f20898]) ).
fof(f107319,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ name(X3,s__374dafrika_0)
| ~ obj(X4,X0)
| ~ prop(X5,schwarz_1_1)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X5,c6492)
| ~ subr(X6,rprs_0)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ arg1(X6,X0)
| ~ name(X3,s__374dafrika_0) ),
inference(resolution,[],[f21041,f10920]) ).
fof(f107320,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ name(X3,s__374dafrika_0)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ obj(X4,X0)
| ~ prop(X5,schwarz_1_1)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X5,c6492)
| ~ subr(X6,rprs_0)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ arg1(X6,X0) ),
inference(duplicate_literal_removal,[],[f107319]) ).
fof(f107898,plain,
name(c6515,s__374dafrika_0),
inference(resolution,[],[f107307,f20900]) ).
fof(f107900,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ val(X2,mandela_0)
| ~ attr(X0,X2)
| ~ obj(X3,X0)
| ~ prop(X4,schwarz_1_1)
| ~ sub(X2,familiename_1_1)
| ~ sub(X1,eigenname_1_1)
| ~ sub(X4,c6492)
| ~ subr(X5,rprs_0)
| ~ attr(X0,X1)
| ~ val(X1,nelson_0)
| ~ arg1(X5,X0) ),
inference(resolution,[],[f107898,f107320]) ).
fof(f107901,plain,
! [X2,X3,X0,X1,X4] :
( ~ attr(X0,c6479)
| ~ obj(X1,X0)
| ~ prop(X2,schwarz_1_1)
| ~ sub(c6479,familiename_1_1)
| ~ sub(X3,eigenname_1_1)
| ~ sub(X2,c6492)
| ~ subr(X4,rprs_0)
| ~ attr(X0,X3)
| ~ val(X3,nelson_0)
| ~ arg1(X4,X0) ),
inference(resolution,[],[f107900,f20916]) ).
fof(f107903,plain,
! [X2,X3,X0,X1,X4] :
( ~ val(X3,nelson_0)
| ~ obj(X1,X0)
| ~ prop(X2,schwarz_1_1)
| ~ sub(X3,eigenname_1_1)
| ~ sub(X2,c6492)
| ~ subr(X4,rprs_0)
| ~ attr(X0,X3)
| ~ attr(X0,c6479)
| ~ arg1(X4,X0) ),
inference(forward_subsumption_resolution,[],[f107901,f20917]) ).
fof(f107904,plain,
! [X2,X3,X0,X1] :
( ~ obj(X0,X1)
| ~ prop(X2,schwarz_1_1)
| ~ sub(c6478,eigenname_1_1)
| ~ sub(X2,c6492)
| ~ subr(X3,rprs_0)
| ~ attr(X1,c6478)
| ~ attr(X1,c6479)
| ~ arg1(X3,X1) ),
inference(resolution,[],[f107903,f20918]) ).
fof(f107906,plain,
! [X2,X3,X0,X1] :
( ~ prop(X2,schwarz_1_1)
| ~ obj(X0,X1)
| ~ sub(X2,c6492)
| ~ subr(X3,rprs_0)
| ~ attr(X1,c6478)
| ~ attr(X1,c6479)
| ~ arg1(X3,X1) ),
inference(forward_subsumption_resolution,[],[f107904,f20919]) ).
fof(f107909,plain,
! [X2,X0,X1] :
( ~ obj(X0,X1)
| ~ sub(c6485,c6492)
| ~ subr(X2,rprs_0)
| ~ attr(X1,c6478)
| ~ attr(X1,c6479)
| ~ arg1(X2,X1) ),
inference(resolution,[],[f107906,f20915]) ).
fof(f107910,plain,
! [X2,X0,X1] :
( ~ subr(X2,rprs_0)
| ~ obj(X0,X1)
| ~ attr(X1,c6478)
| ~ attr(X1,c6479)
| ~ arg1(X2,X1) ),
inference(forward_subsumption_resolution,[],[f107909,f20914]) ).
fof(f108036,plain,
! [X2,X3,X0,X1,X4] :
( ~ arg1(sK56(X0,X1,X2),X4)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0)
| ~ obj(X3,X4)
| ~ attr(X4,c6478)
| ~ attr(X4,c6479)
| ~ arg1(X0,X1) ),
inference(resolution,[],[f10881,f107910]) ).
fof(f108061,plain,
! [X2,X3,X0,X1] :
( ~ arg2(X0,X1)
| ~ subr(X0,sub_0)
| ~ obj(X2,X3)
| ~ attr(X3,c6478)
| ~ attr(X3,c6479)
| ~ arg1(X0,X3)
| ~ arg1(X0,X3)
| ~ arg2(X0,X1)
| ~ subr(X0,sub_0) ),
inference(resolution,[],[f108036,f10887]) ).
fof(f108062,plain,
! [X2,X3,X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X1)
| ~ obj(X2,X3)
| ~ attr(X3,c6478)
| ~ attr(X3,c6479)
| ~ arg1(X0,X3) ),
inference(duplicate_literal_removal,[],[f108061]) ).
fof(f108076,plain,
! [X2,X3,X0,X1,X4] :
( ~ arg2(sK58(X0,X1),X2)
| ~ obj(X3,X4)
| ~ attr(X4,c6478)
| ~ attr(X4,c6479)
| ~ arg1(sK58(X0,X1),X4)
| ~ sub(X0,X1) ),
inference(resolution,[],[f108062,f10888]) ).
fof(f108090,plain,
! [X2,X3,X0,X1] :
( ~ obj(X0,X1)
| ~ attr(X1,c6478)
| ~ attr(X1,c6479)
| ~ arg1(sK58(X2,X3),X1)
| ~ sub(X2,X3)
| ~ sub(X2,X3) ),
inference(resolution,[],[f108076,f10889]) ).
fof(f108091,plain,
! [X2,X3,X0,X1] :
( ~ arg1(sK58(X2,X3),X1)
| ~ attr(X1,c6478)
| ~ attr(X1,c6479)
| ~ obj(X0,X1)
| ~ sub(X2,X3) ),
inference(duplicate_literal_removal,[],[f108090]) ).
fof(f108105,plain,
! [X2,X0,X1] :
( ~ attr(X0,c6478)
| ~ attr(X0,c6479)
| ~ obj(X1,X0)
| ~ sub(X0,X2)
| ~ sub(X0,X2) ),
inference(resolution,[],[f108091,f10890]) ).
fof(f108106,plain,
! [X2,X0,X1] :
( ~ attr(X0,c6479)
| ~ attr(X0,c6478)
| ~ obj(X1,X0)
| ~ sub(X0,X2) ),
inference(duplicate_literal_removal,[],[f108105]) ).
fof(f108120,plain,
! [X0,X1] :
( ~ attr(c6477,c6478)
| ~ obj(X0,c6477)
| ~ sub(c6477,X1) ),
inference(resolution,[],[f108106,f20921]) ).
fof(f108121,plain,
! [X0,X1] :
( ~ obj(X0,c6477)
| ~ sub(c6477,X1) ),
inference(forward_subsumption_resolution,[],[f108120,f20922]) ).
fof(f108139,plain,
! [X2,X0,X1] :
( ~ subr(X1,sub_0)
| ~ arg1(X1,c6477)
| ~ arg2(X1,X2)
| ~ sub(c6477,X0) ),
inference(resolution,[],[f108121,f10883]) ).
fof(f108174,plain,
! [X2,X3,X0,X1] :
( ~ arg2(sK58(X0,X1),X2)
| ~ arg1(sK58(X0,X1),c6477)
| ~ sub(c6477,X3)
| ~ sub(X0,X1) ),
inference(resolution,[],[f108139,f10888]) ).
fof(f108196,plain,
! [X2,X0,X1] :
( ~ arg1(sK58(X0,X1),c6477)
| ~ sub(c6477,X2)
| ~ sub(X0,X1)
| ~ sub(X0,X1) ),
inference(resolution,[],[f108174,f10889]) ).
fof(f108197,plain,
! [X2,X0,X1] :
( ~ arg1(sK58(X0,X1),c6477)
| ~ sub(c6477,X2)
| ~ sub(X0,X1) ),
inference(duplicate_literal_removal,[],[f108196]) ).
fof(f108199,plain,
! [X0,X1] :
( ~ sub(c6477,X0)
| ~ sub(c6477,X1)
| ~ sub(c6477,X1) ),
inference(resolution,[],[f108197,f10890]) ).
fof(f108200,plain,
! [X0,X1] :
( ~ sub(c6477,X1)
| ~ sub(c6477,X0) ),
inference(duplicate_literal_removal,[],[f108199]) ).
fof(f108202,plain,
! [X0] : ~ sub(c6477,X0),
inference(resolution,[],[f108200,f20920]) ).
fof(f108204,plain,
$false,
inference(resolution,[],[f108202,f20920]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.24 % Computer : n011.cluster.edu
% 0.09/0.24 % Model : x86_64 x86_64
% 0.09/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.24 % Memory : 8046.5625MB
% 0.09/0.24 % OS : Linux 6.8.0-71-generic
% 0.09/0.24 % CPULimit : 300
% 0.09/0.24 % WCLimit : 300
% 0.09/0.24 % DateTime : Mon Sep 28 23:29:01 UTC 2026
% 0.09/0.24 % CPUTime :
% 0.09/0.24 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.29 Running first-order model finding
% 0.09/0.29 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
% 43.61/6.61 % (3886789)Will run a generic schedule for satisfiability detection.
% 43.61/6.61 % (3886797)dis+10_1_sil=32000:sp=arity:random_seed=4128485668:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 43.61/6.61 % (3886800)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4278289383:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 43.61/6.61 % (3886795)% WARNING: option uhcvi not known.
% 43.61/6.61 % (3886795)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2184808080:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 43.61/6.61 % (3886799)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4218307965:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 43.61/6.61 % (3886798)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3903409769:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 43.61/6.61 % (3886796)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1274443422:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 43.61/6.61 % (3886794)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4123027167_2997 on theBenchmark for (2997ds/0Mi)
% 43.61/6.61 % (3886797)Instruction limit reached!
% 43.61/6.61 % (3886797)------------------------------
% 43.61/6.61 % (3886797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.61/6.61 % (3886797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.61/6.61 % (3886797)CaDiCaL version: 2.1.3
% 43.61/6.61 % (3886797)Termination reason: Instruction limit
% 43.61/6.61 % (3886797)Termination phase: Saturation
% 43.61/6.61 % (3886797)Time elapsed: 0.053 s
% 43.61/6.61 % (3886797)Peak memory usage: 26 MB
% 43.61/6.61 % (3886797)Instructions burned: 106 (million)
% 43.61/6.61 % (3886808)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=110981027:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 43.61/6.61 % (3886800)Instruction limit reached!
% 43.61/6.61 % (3886800)------------------------------
% 43.61/6.61 % (3886800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.61/6.61 % (3886800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.61/6.61 % (3886800)CaDiCaL version: 2.1.3
% 43.61/6.61 % (3886800)Termination reason: Instruction limit
% 43.61/6.61 % (3886800)Termination phase: Saturation
% 43.61/6.61 % (3886800)Time elapsed: 0.098 s
% 43.61/6.61 % (3886800)Peak memory usage: 30 MB
% 43.61/6.61 % (3886800)Instructions burned: 160 (million)
% 43.61/6.61 % (3886799)Instruction limit reached!
% 43.61/6.61 % (3886799)------------------------------
% 43.61/6.61 % (3886799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.61/6.61 % (3886799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.61/6.61 % (3886799)CaDiCaL version: 2.1.3
% 43.61/6.61 % (3886799)Termination reason: Instruction limit
% 43.61/6.61 % (3886799)Termination phase: Saturation
% 43.61/6.61 % (3886799)Time elapsed: 0.115 s
% 43.61/6.61 % (3886799)Peak memory usage: 28 MB
% 43.61/6.61 % (3886799)Instructions burned: 131 (million)
% 43.61/6.61 % (3886810)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=47472015:i=131:bd=preordered:fsd=on_2996 on theBenchmark for (2996ds/131Mi)
% 43.61/6.61 % (3886798)Instruction limit reached!
% 43.61/6.61 % (3886798)------------------------------
% 43.61/6.61 % (3886798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.61/6.61 % (3886798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.61/6.61 % (3886798)CaDiCaL version: 2.1.3
% 43.61/6.61 % (3886798)Termination reason: Instruction limit
% 43.61/6.61 % (3886798)Termination phase: Blocked clause elimination
% 43.61/6.61 % (3886798)Time elapsed: 0.120 s
% 43.61/6.61 % (3886798)Peak memory usage: 28 MB
% 43.61/6.61 % (3886798)Instructions burned: 116 (million)
% 43.61/6.61 % (3886811)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=737126376:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2996 on theBenchmark for (2996ds/684Mi)
% 43.61/6.61 % (3886813)ott-21_1_sil=16000:fs=off:random_seed=2610083363:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 43.61/6.61 % (3886810)Instruction limit reached!
% 43.61/6.61 % (3886810)------------------------------
% 43.61/6.61 % (3886810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.61/6.61 % (3886810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.88/10.81 % (3886810)CaDiCaL version: 2.1.3
% 72.88/10.81 % (3886810)Termination reason: Instruction limit
% 72.88/10.81 % (3886810)Termination phase: Blocked clause elimination
% 72.88/10.81 % (3886810)Time elapsed: 0.084 s
% 72.88/10.81 % (3886810)Peak memory usage: 29 MB
% 72.88/10.81 % (3886810)Instructions burned: 131 (million)
% 72.88/10.81 % (3886816)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1415722547:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi)
% 72.88/10.81 % TRYING [1]
% 72.88/10.81 % (3886813)Instruction limit reached!
% 72.88/10.81 % (3886813)------------------------------
% 72.88/10.81 % (3886813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.88/10.81 % (3886813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.88/10.81 % (3886813)CaDiCaL version: 2.1.3
% 72.88/10.81 % (3886813)Termination reason: Instruction limit
% 72.88/10.81 % (3886813)Termination phase: Saturation
% 72.88/10.81 % (3886813)Time elapsed: 0.136 s
% 72.88/10.81 % (3886813)Peak memory usage: 28 MB
% 72.88/10.81 % (3886813)Instructions burned: 182 (million)
% 72.88/10.81 % TRYING [2]
% 72.88/10.81 % (3886818)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1443287738:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 72.88/10.81 % (3886808)Instruction limit reached!
% 72.88/10.81 % (3886808)------------------------------
% 72.88/10.81 % (3886808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.88/10.81 % (3886808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.88/10.81 % (3886808)CaDiCaL version: 2.1.3
% 72.88/10.81 % (3886808)Termination reason: Instruction limit
% 72.88/10.81 % (3886808)Termination phase: Finite model building constraint generation
% 72.88/10.81 % (3886808)Time elapsed: 0.339 s
% 72.88/10.81 % (3886808)Peak memory usage: 54 MB
% 72.88/10.81 % (3886808)Instructions burned: 714 (million)
% 72.88/10.81 % (3886820)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=459582515:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 72.88/10.81 % TRYING [1]
% 72.88/10.81 % TRYING [2]
% 72.88/10.81 % (3886816)Instruction limit reached!
% 72.88/10.81 % (3886816)------------------------------
% 72.88/10.81 % (3886816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.88/10.81 % (3886816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.88/10.81 % (3886816)CaDiCaL version: 2.1.3
% 72.88/10.81 % (3886816)Termination reason: Instruction limit
% 72.88/10.81 % (3886816)Termination phase: Saturation
% 72.88/10.81 % (3886816)Time elapsed: 0.438 s
% 72.88/10.81 % (3886816)Peak memory usage: 39 MB
% 72.88/10.81 % (3886816)Instructions burned: 478 (million)
% 72.88/10.81 % (3886811)Instruction limit reached!
% 72.88/10.81 % (3886811)------------------------------
% 72.88/10.81 % (3886811)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.88/10.81 % (3886811)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.88/10.81 % (3886811)CaDiCaL version: 2.1.3
% 72.88/10.81 % (3886811)Termination reason: Instruction limit
% 72.88/10.81 % (3886811)Termination phase: Saturation
% 72.88/10.81 % (3886811)Time elapsed: 0.555 s
% 72.88/10.81 % (3886811)Peak memory usage: 35 MB
% 72.88/10.81 % (3886811)Instructions burned: 684 (million)
% 72.88/10.81 % TRYING [1]
% 72.88/10.81 % (3886822)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1480580038:i=889:ins=1_2990 on theBenchmark for (2990ds/889Mi)
% 72.88/10.81 % (3886823)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=998145430:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2990 on theBenchmark for (2990ds/692Mi)
% 72.88/10.81 % TRYING [3]
% 72.88/10.81 % (3886818)Instruction limit reached!
% 72.88/10.81 % (3886818)------------------------------
% 72.88/10.81 % (3886818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.88/10.81 % (3886818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.88/10.81 % (3886818)CaDiCaL version: 2.1.3
% 72.88/10.81 % (3886818)Termination reason: Instruction limit
% 72.88/10.81 % (3886818)Termination phase: Finite model building SAT solving
% 72.88/10.81 % (3886818)Time elapsed: 0.600 s
% 72.88/10.81 % (3886818)Peak memory usage: 38 MB
% 72.88/10.81 % (3886818)Instructions burned: 867 (million)
% 72.88/10.81 % (3886826)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1934956940:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi)
% 72.88/10.81 % (3886820)Instruction limit reached!
% 72.88/10.81 % (3886820)------------------------------
% 72.88/10.81 % (3886820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886820)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886820)Termination reason: Instruction limit
% 37.85/10.92 % (3886820)Termination phase: Saturation
% 37.85/10.92 % (3886820)Time elapsed: 0.581 s
% 37.85/10.92 % (3886820)Peak memory usage: 55 MB
% 37.85/10.92 % (3886820)Instructions burned: 1180 (million)
% 37.85/10.92 % (3886828)fmb+10_1_sil=64000:random_seed=1055542339:i=22061:nm=2:gsp=on_2987 on theBenchmark for (2987ds/22061Mi)
% 37.85/10.92 % TRYING [1]
% 37.85/10.92 % (3886823)Instruction limit reached!
% 37.85/10.92 % (3886823)------------------------------
% 37.85/10.92 % (3886823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886823)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886823)Termination reason: Instruction limit
% 37.85/10.92 % (3886823)Termination phase: Saturation
% 37.85/10.92 % (3886823)Time elapsed: 0.595 s
% 37.85/10.92 % (3886823)Peak memory usage: 44 MB
% 37.85/10.92 % (3886823)Instructions burned: 692 (million)
% 37.85/10.92 % TRYING [2]
% 37.85/10.92 % (3886830)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1248076580:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 37.85/10.92 % (3886822)Instruction limit reached!
% 37.85/10.92 % (3886822)------------------------------
% 37.85/10.92 % (3886822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886822)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886822)Termination reason: Instruction limit
% 37.85/10.92 % (3886822)Termination phase: Finite model building constraint generation
% 37.85/10.92 % (3886822)Time elapsed: 0.813 s
% 37.85/10.92 % (3886822)Peak memory usage: 95 MB
% 37.85/10.92 % (3886822)Instructions burned: 889 (million)
% 37.85/10.92 % TRYING [4]
% 37.85/10.92 % (3886832)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4100025494:fmbsr=1.7:i=920_2981 on theBenchmark for (2981ds/920Mi)
% 37.85/10.92 % (3886826)Instruction limit reached!
% 37.85/10.92 % (3886826)------------------------------
% 37.85/10.92 % (3886826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886826)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886826)Termination reason: Instruction limit
% 37.85/10.92 % (3886826)Termination phase: Saturation
% 37.85/10.92 % (3886826)Time elapsed: 0.657 s
% 37.85/10.92 % (3886826)Peak memory usage: 42 MB
% 37.85/10.92 % (3886826)Instructions burned: 880 (million)
% 37.85/10.92 % (3886834)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1656052291:i=5131_2981 on theBenchmark for (2981ds/5131Mi)
% 37.85/10.92 % TRYING [20]
% 37.85/10.92 % TRYING [8]
% 37.85/10.92 % TRYING [3]
% 37.85/10.92 % (3886832)Instruction limit reached!
% 37.85/10.92 % (3886832)------------------------------
% 37.85/10.92 % (3886832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886832)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886832)Termination reason: Instruction limit
% 37.85/10.92 % (3886832)Termination phase: Finite model building constraint generation
% 37.85/10.92 % (3886832)Time elapsed: 0.701 s
% 37.85/10.92 % (3886832)Peak memory usage: 64 MB
% 37.85/10.92 % (3886832)Instructions burned: 921 (million)
% 37.85/10.92 % (3886836)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1449866145:i=1472:ins=7:fdi=8:gsp=on_2974 on theBenchmark for (2974ds/1472Mi)
% 37.85/10.92 % TRYING [5]
% 37.85/10.92 % TRYING [4]
% 37.85/10.92 % (3886836)Instruction limit reached!
% 37.85/10.92 % (3886836)------------------------------
% 37.85/10.92 % (3886836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886836)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886836)Termination reason: Instruction limit
% 37.85/10.92 % (3886836)Termination phase: Saturation
% 37.85/10.92 % (3886836)Time elapsed: 1.176 s
% 37.85/10.92 % (3886836)Peak memory usage: 35 MB
% 37.85/10.92 % (3886836)Instructions burned: 1472 (million)
% 37.85/10.92 % (3886840)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=32270201:i=6324_2961 on theBenchmark for (2961ds/6324Mi)
% 37.85/10.92 % TRYING [77]
% 37.85/10.92 % TRYING [5]
% 37.85/10.92 % (3886834)Instruction limit reached!
% 37.85/10.92 % (3886834)------------------------------
% 37.85/10.92 % (3886834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886834)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886834)Termination reason: Instruction limit
% 37.85/10.92 % (3886834)Termination phase: Saturation
% 37.85/10.92 % (3886834)Time elapsed: 4.362 s
% 37.85/10.92 % (3886834)Peak memory usage: 43 MB
% 37.85/10.92 % (3886834)Instructions burned: 5131 (million)
% 37.85/10.92 % (3886842)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2779558716:fmbsr=2.30978:i=2174_2936 on theBenchmark for (2936ds/2174Mi)
% 37.85/10.92 % TRYING [16]
% 37.85/10.92 % (3886830)Instruction limit reached!
% 37.85/10.92 % (3886830)------------------------------
% 37.85/10.92 % (3886830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886830)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886830)Termination reason: Instruction limit
% 37.85/10.92 % (3886830)Termination phase: Finite model building constraint generation
% 37.85/10.92 % (3886830)Time elapsed: 6.125 s
% 37.85/10.92 % (3886830)Peak memory usage: 550 MB
% 37.85/10.92 % (3886830)Instructions burned: 9516 (million)
% 37.85/10.92 % (3886842)Instruction limit reached!
% 37.85/10.92 % (3886842)------------------------------
% 37.85/10.92 % (3886842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886842)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886842)Termination reason: Instruction limit
% 37.85/10.92 % (3886842)Termination phase: Finite model building constraint generation
% 37.85/10.92 % (3886842)Time elapsed: 1.535 s
% 37.85/10.92 % (3886842)Peak memory usage: 120 MB
% 37.85/10.92 % (3886842)Instructions burned: 2175 (million)
% 37.85/10.92 % (3886846)ott-2_1_sil=16000:newcnf=on:random_seed=2138995107:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2921 on theBenchmark for (2921ds/869Mi)
% 37.85/10.92 % (3886848)ott+10_1_sil=32000:tgt=ground:random_seed=1284839889:i=5114:av=off_2920 on theBenchmark for (2920ds/5114Mi)
% 37.85/10.92 % (3886840)Instruction limit reached!
% 37.85/10.92 % (3886840)------------------------------
% 37.85/10.92 % (3886840)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886840)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886840)Termination reason: Instruction limit
% 37.85/10.92 % (3886840)Termination phase: Finite model building constraint generation
% 37.85/10.92 % (3886840)Time elapsed: 4.569 s
% 37.85/10.92 % (3886840)Peak memory usage: 416 MB
% 37.85/10.92 % (3886840)Instructions burned: 6325 (million)
% 37.85/10.92 % (3886850)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1579889067:i=54282_2914 on theBenchmark for (2914ds/54282Mi)
% 37.85/10.92 % (3886846)Instruction limit reached!
% 37.85/10.92 % (3886846)------------------------------
% 37.85/10.92 % (3886846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886846)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886846)Termination reason: Instruction limit
% 37.85/10.92 % (3886846)Termination phase: Saturation
% 37.85/10.92 % (3886846)Time elapsed: 0.745 s
% 37.85/10.92 % (3886846)Peak memory usage: 42 MB
% 37.85/10.92 % (3886846)Instructions burned: 870 (million)
% 37.85/10.92 % (3886852)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3341537580:i=3512:aac=none_2913 on theBenchmark for (2913ds/3512Mi)
% 37.85/10.92 % TRYING [1]
% 37.85/10.92 % TRYING [2]
% 37.85/10.92 % TRYING [3]
% 37.85/10.92 % (3886828)Instruction limit reached!
% 37.85/10.92 % (3886828)------------------------------
% 37.85/10.92 % (3886828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.92 % (3886828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.92 % (3886828)CaDiCaL version: 2.1.3
% 37.85/10.92 % (3886828)Termination reason: Instruction limit
% 37.85/10.92 % (3886828)Termination phase: Finite model building SAT solving
% 37.85/10.92 % (3886828)Time elapsed: 8.535 s
% 37.85/10.92 % (3886828)Peak memory usage: 151 MB
% 37.85/10.92 % (3886828)Instructions burned: 22063 (million)
% 37.85/10.92 % (3886854)dis+21_1_sil=32000:sas=cadical:random_seed=2839686849:i=3773:amm=off_2901 on theBenchmark for (2901ds/3773Mi)
% 37.85/10.92 % (3886848) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3886789-3886848"...
% 37.85/10.92 % (3886848)...printing done.
% 37.85/10.92 % (3886848)Refutation found. Thanks to Tanya!
% 37.85/10.92 % SZS status Theorem for theBenchmark
% 37.85/10.92 % SZS output start Proof for theBenchmark
% See solution above
% 37.85/10.94 % (3886848)------------------------------
% 37.85/10.94 % (3886848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.85/10.94 % (3886848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.85/10.94 % (3886848)CaDiCaL version: 2.1.3
% 37.85/10.94 % (3886848)Termination reason: Refutation
% 37.85/10.94 % (3886848)Time elapsed: 2.561 s
% 37.85/10.94 % (3886848)Peak memory usage: 96 MB
% 37.85/10.94 % (3886848)Instructions burned: 2837 (million)
% 37.85/10.94 % (3886789)Success in time 10.619 s
% 37.85/10.94 % Vampire exiting
%------------------------------------------------------------------------------