%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR116+19 : 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 : n004.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:49 AM UTC 2026
% Result : Theorem 16.28s 6.32s
% Output : Refutation 16.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 6
% Syntax : Number of formulae : 82 ( 13 unt; 0 def)
% Number of atoms : 2361 ( 0 equ)
% Maximal formula atoms : 299 ( 28 avg)
% Number of connectives : 2563 ( 284 ~; 251 |;2024 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 299 ( 32 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 30 ( 29 usr; 1 prp; 0-2 aty)
% Number of functors : 78 ( 78 usr; 72 con; 0-3 aty)
% Number of variables : 255 ( 224 !; 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] :
( arg1(X3,X0)
& arg2(X3,X4)
& attr(X0,X1)
& attr(X0,X2)
& attr(X5,X6)
& obj(X7,X0)
& 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_1755) ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( arg1(X3,X0)
& arg2(X3,X4)
& attr(X0,X1)
& attr(X0,X2)
& attr(X5,X6)
& obj(X7,X0)
& 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,
( sub(c10,name_1_1)
& val(c10,johannesburg_0)
& loc(c15,c9401)
& subs(c15,bekennen_1_1)
& attr(c9,c10)
& sub(c9,stadt__1_1)
& attr(c9235,c9236)
& attr(c9235,c9237)
& sub(c9235,putschistenf__374hrer_1_1)
& sub(c9236,eigenname_1_1)
& val(c9236,jonas_0)
& sub(c9237,familiename_1_1)
& val(c9237,savimbi_0)
& attch(c9245,c9251)
& attr(c9245,c9246)
& sub(c9245,land_1_1)
& sub(c9246,name_1_1)
& val(c9246,s__374dafrika_0)
& attr(c9251,c9252)
& attr(c9251,c9253)
& sub(c9251,pr__344sident_1_1)
& sub(c9252,eigenname_1_1)
& val(c9252,nelson_0)
& sub(c9253,familiename_1_1)
& val(c9253,mandela_0)
& agt(c9256,c9235)
& ornt(c9256,c9251)
& semrel(c9256,c15)
& subs(c9256,anflehen_1_1)
& loc(c9372,c9397)
& sub(c9372,regierung_1_1)
& attr(c9380,c9381)
& sub(c9380,stadt__1_1)
& sub(c9381,name_1_1)
& val(c9381,luanda_0)
& preds(c9383,angriff_1_1)
& prop(c9383,weit_1_1)
& agt(c9387,c9235)
& mcont(c9387,c9383)
& modl(c9387,sollen_0)
& obj(c9387,c9372)
& semrel(c9387,c9256)
& subs(c9387,abhalten_1_1)
& in(c9397,c9380)
& in(c9401,c9)
& assoc(putschistenf__374hrer_1_1,meuterer_1_1)
& sub(putschistenf__374hrer_1_1,an_f__374hrer_1_1)
& sort(c10,na)
& card(c10,int1)
& etype(c10,int0)
& fact(c10,real)
& gener(c10,sp)
& quant(c10,one)
& refer(c10,indet)
& varia(c10,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(johannesburg_0,fe)
& sort(c15,da)
& fact(c15,real)
& gener(c15,sp)
& sort(c9401,l)
& card(c9401,int1)
& etype(c9401,int0)
& fact(c9401,real)
& gener(c9401,sp)
& quant(c9401,one)
& refer(c9401,det)
& varia(c9401,con)
& sort(bekennen_1_1,da)
& fact(bekennen_1_1,real)
& gener(bekennen_1_1,ge)
& sort(c9,d)
& sort(c9,io)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& quant(c9,one)
& refer(c9,det)
& varia(c9,con)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(c9235,d)
& card(c9235,int1)
& etype(c9235,int0)
& fact(c9235,real)
& gener(c9235,sp)
& quant(c9235,one)
& refer(c9235,det)
& varia(c9235,con)
& sort(c9236,na)
& card(c9236,int1)
& etype(c9236,int0)
& fact(c9236,real)
& gener(c9236,sp)
& quant(c9236,one)
& refer(c9236,indet)
& varia(c9236,varia_c)
& sort(c9237,na)
& card(c9237,int1)
& etype(c9237,int0)
& fact(c9237,real)
& gener(c9237,sp)
& quant(c9237,one)
& refer(c9237,indet)
& varia(c9237,varia_c)
& sort(putschistenf__374hrer_1_1,d)
& card(putschistenf__374hrer_1_1,int1)
& etype(putschistenf__374hrer_1_1,int0)
& fact(putschistenf__374hrer_1_1,real)
& gener(putschistenf__374hrer_1_1,ge)
& quant(putschistenf__374hrer_1_1,one)
& refer(putschistenf__374hrer_1_1,refer_c)
& varia(putschistenf__374hrer_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(jonas_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(savimbi_0,fe)
& sort(c9245,d)
& sort(c9245,io)
& card(c9245,int1)
& etype(c9245,int0)
& fact(c9245,real)
& gener(c9245,sp)
& quant(c9245,one)
& refer(c9245,det)
& varia(c9245,con)
& sort(c9251,d)
& card(c9251,int1)
& etype(c9251,int0)
& fact(c9251,real)
& gener(c9251,sp)
& quant(c9251,one)
& refer(c9251,det)
& varia(c9251,varia_c)
& sort(c9246,na)
& card(c9246,int1)
& etype(c9246,int0)
& fact(c9246,real)
& gener(c9246,sp)
& quant(c9246,one)
& refer(c9246,indet)
& varia(c9246,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(s__374dafrika_0,fe)
& sort(c9252,na)
& card(c9252,int1)
& etype(c9252,int0)
& fact(c9252,real)
& gener(c9252,sp)
& quant(c9252,one)
& refer(c9252,indet)
& varia(c9252,varia_c)
& sort(c9253,na)
& card(c9253,int1)
& etype(c9253,int0)
& fact(c9253,real)
& gener(c9253,sp)
& quant(c9253,one)
& refer(c9253,indet)
& varia(c9253,varia_c)
& 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(nelson_0,fe)
& sort(mandela_0,fe)
& sort(c9256,da)
& fact(c9256,real)
& gener(c9256,sp)
& sort(anflehen_1_1,da)
& fact(anflehen_1_1,real)
& gener(anflehen_1_1,ge)
& sort(c9372,d)
& sort(c9372,io)
& card(c9372,int1)
& etype(c9372,int1)
& fact(c9372,real)
& gener(c9372,sp)
& quant(c9372,one)
& refer(c9372,det)
& varia(c9372,con)
& sort(c9397,l)
& card(c9397,int1)
& etype(c9397,int0)
& fact(c9397,real)
& gener(c9397,sp)
& quant(c9397,one)
& refer(c9397,det)
& varia(c9397,con)
& sort(regierung_1_1,d)
& sort(regierung_1_1,io)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& quant(regierung_1_1,quant_c)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& sort(c9380,d)
& sort(c9380,io)
& card(c9380,int1)
& etype(c9380,int0)
& fact(c9380,real)
& gener(c9380,sp)
& quant(c9380,one)
& refer(c9380,det)
& varia(c9380,con)
& sort(c9381,na)
& card(c9381,int1)
& etype(c9381,int0)
& fact(c9381,real)
& gener(c9381,sp)
& quant(c9381,one)
& refer(c9381,indet)
& varia(c9381,varia_c)
& sort(luanda_0,fe)
& sort(c9383,ad)
& card(c9383,cons(x_constant,cons(int1,nil)))
& etype(c9383,int1)
& fact(c9383,hypo)
& gener(c9383,sp)
& quant(c9383,mult)
& refer(c9383,indet)
& varia(c9383,varia_c)
& sort(angriff_1_1,ad)
& card(angriff_1_1,int1)
& etype(angriff_1_1,int0)
& fact(angriff_1_1,real)
& gener(angriff_1_1,ge)
& quant(angriff_1_1,one)
& refer(angriff_1_1,refer_c)
& varia(angriff_1_1,varia_c)
& sort(weit_1_1,mq)
& sort(c9387,da)
& fact(c9387,real)
& gener(c9387,sp)
& sort(sollen_0,md)
& fact(sollen_0,real)
& gener(sollen_0,gener_c)
& sort(abhalten_1_1,da)
& fact(abhalten_1_1,real)
& gener(abhalten_1_1,ge)
& sort(meuterer_1_1,d)
& card(meuterer_1_1,int1)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& quant(meuterer_1_1,one)
& refer(meuterer_1_1,refer_c)
& varia(meuterer_1_1,varia_c)
& sort(an_f__374hrer_1_1,d)
& card(an_f__374hrer_1_1,int1)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& quant(an_f__374hrer_1_1,one)
& refer(an_f__374hrer_1_1,refer_c)
& varia(an_f__374hrer_1_1,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_news_1755) ).
fof(f10191,plain,
( sub(c10,name_1_1)
& val(c10,johannesburg_0)
& loc(c15,c9401)
& subs(c15,bekennen_1_1)
& attr(c9,c10)
& sub(c9,stadt__1_1)
& attr(c9235,c9236)
& attr(c9235,c9237)
& sub(c9235,putschistenf__374hrer_1_1)
& sub(c9236,eigenname_1_1)
& val(c9236,jonas_0)
& sub(c9237,familiename_1_1)
& val(c9237,savimbi_0)
& attch(c9245,c9251)
& attr(c9245,c9246)
& sub(c9245,land_1_1)
& sub(c9246,name_1_1)
& val(c9246,s__374dafrika_0)
& attr(c9251,c9252)
& attr(c9251,c9253)
& sub(c9251,pr__344sident_1_1)
& sub(c9252,eigenname_1_1)
& val(c9252,nelson_0)
& sub(c9253,familiename_1_1)
& val(c9253,mandela_0)
& agt(c9256,c9235)
& ornt(c9256,c9251)
& semrel(c9256,c15)
& subs(c9256,anflehen_1_1)
& loc(c9372,c9397)
& sub(c9372,regierung_1_1)
& attr(c9380,c9381)
& sub(c9380,stadt__1_1)
& sub(c9381,name_1_1)
& val(c9381,luanda_0)
& preds(c9383,angriff_1_1)
& prop(c9383,weit_1_1)
& agt(c9387,c9235)
& mcont(c9387,c9383)
& obj(c9387,c9372)
& semrel(c9387,c9256)
& subs(c9387,abhalten_1_1)
& in(c9397,c9380)
& in(c9401,c9)
& assoc(putschistenf__374hrer_1_1,meuterer_1_1)
& sub(putschistenf__374hrer_1_1,an_f__374hrer_1_1)
& sort(c10,na)
& card(c10,int1)
& etype(c10,int0)
& fact(c10,real)
& gener(c10,sp)
& quant(c10,one)
& refer(c10,indet)
& varia(c10,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(johannesburg_0,fe)
& sort(c15,da)
& fact(c15,real)
& gener(c15,sp)
& sort(c9401,l)
& card(c9401,int1)
& etype(c9401,int0)
& fact(c9401,real)
& gener(c9401,sp)
& quant(c9401,one)
& refer(c9401,det)
& varia(c9401,con)
& sort(bekennen_1_1,da)
& fact(bekennen_1_1,real)
& gener(bekennen_1_1,ge)
& sort(c9,d)
& sort(c9,io)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& quant(c9,one)
& refer(c9,det)
& varia(c9,con)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(c9235,d)
& card(c9235,int1)
& etype(c9235,int0)
& fact(c9235,real)
& gener(c9235,sp)
& quant(c9235,one)
& refer(c9235,det)
& varia(c9235,con)
& sort(c9236,na)
& card(c9236,int1)
& etype(c9236,int0)
& fact(c9236,real)
& gener(c9236,sp)
& quant(c9236,one)
& refer(c9236,indet)
& varia(c9236,varia_c)
& sort(c9237,na)
& card(c9237,int1)
& etype(c9237,int0)
& fact(c9237,real)
& gener(c9237,sp)
& quant(c9237,one)
& refer(c9237,indet)
& varia(c9237,varia_c)
& sort(putschistenf__374hrer_1_1,d)
& card(putschistenf__374hrer_1_1,int1)
& etype(putschistenf__374hrer_1_1,int0)
& fact(putschistenf__374hrer_1_1,real)
& gener(putschistenf__374hrer_1_1,ge)
& quant(putschistenf__374hrer_1_1,one)
& refer(putschistenf__374hrer_1_1,refer_c)
& varia(putschistenf__374hrer_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(jonas_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(savimbi_0,fe)
& sort(c9245,d)
& sort(c9245,io)
& card(c9245,int1)
& etype(c9245,int0)
& fact(c9245,real)
& gener(c9245,sp)
& quant(c9245,one)
& refer(c9245,det)
& varia(c9245,con)
& sort(c9251,d)
& card(c9251,int1)
& etype(c9251,int0)
& fact(c9251,real)
& gener(c9251,sp)
& quant(c9251,one)
& refer(c9251,det)
& varia(c9251,varia_c)
& sort(c9246,na)
& card(c9246,int1)
& etype(c9246,int0)
& fact(c9246,real)
& gener(c9246,sp)
& quant(c9246,one)
& refer(c9246,indet)
& varia(c9246,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(s__374dafrika_0,fe)
& sort(c9252,na)
& card(c9252,int1)
& etype(c9252,int0)
& fact(c9252,real)
& gener(c9252,sp)
& quant(c9252,one)
& refer(c9252,indet)
& varia(c9252,varia_c)
& sort(c9253,na)
& card(c9253,int1)
& etype(c9253,int0)
& fact(c9253,real)
& gener(c9253,sp)
& quant(c9253,one)
& refer(c9253,indet)
& varia(c9253,varia_c)
& 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(nelson_0,fe)
& sort(mandela_0,fe)
& sort(c9256,da)
& fact(c9256,real)
& gener(c9256,sp)
& sort(anflehen_1_1,da)
& fact(anflehen_1_1,real)
& gener(anflehen_1_1,ge)
& sort(c9372,d)
& sort(c9372,io)
& card(c9372,int1)
& etype(c9372,int1)
& fact(c9372,real)
& gener(c9372,sp)
& quant(c9372,one)
& refer(c9372,det)
& varia(c9372,con)
& sort(c9397,l)
& card(c9397,int1)
& etype(c9397,int0)
& fact(c9397,real)
& gener(c9397,sp)
& quant(c9397,one)
& refer(c9397,det)
& varia(c9397,con)
& sort(regierung_1_1,d)
& sort(regierung_1_1,io)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& quant(regierung_1_1,quant_c)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& sort(c9380,d)
& sort(c9380,io)
& card(c9380,int1)
& etype(c9380,int0)
& fact(c9380,real)
& gener(c9380,sp)
& quant(c9380,one)
& refer(c9380,det)
& varia(c9380,con)
& sort(c9381,na)
& card(c9381,int1)
& etype(c9381,int0)
& fact(c9381,real)
& gener(c9381,sp)
& quant(c9381,one)
& refer(c9381,indet)
& varia(c9381,varia_c)
& sort(luanda_0,fe)
& sort(c9383,ad)
& card(c9383,cons(x_constant,cons(int1,nil)))
& etype(c9383,int1)
& fact(c9383,hypo)
& gener(c9383,sp)
& quant(c9383,mult)
& refer(c9383,indet)
& varia(c9383,varia_c)
& sort(angriff_1_1,ad)
& card(angriff_1_1,int1)
& etype(angriff_1_1,int0)
& fact(angriff_1_1,real)
& gener(angriff_1_1,ge)
& quant(angriff_1_1,one)
& refer(angriff_1_1,refer_c)
& varia(angriff_1_1,varia_c)
& sort(weit_1_1,mq)
& sort(c9387,da)
& fact(c9387,real)
& gener(c9387,sp)
& sort(sollen_0,md)
& fact(sollen_0,real)
& gener(sollen_0,gener_c)
& sort(abhalten_1_1,da)
& fact(abhalten_1_1,real)
& gener(abhalten_1_1,ge)
& sort(meuterer_1_1,d)
& card(meuterer_1_1,int1)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& quant(meuterer_1_1,one)
& refer(meuterer_1_1,refer_c)
& varia(meuterer_1_1,varia_c)
& sort(an_f__374hrer_1_1,d)
& card(an_f__374hrer_1_1,int1)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& quant(an_f__374hrer_1_1,one)
& refer(an_f__374hrer_1_1,refer_c)
& varia(an_f__374hrer_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10192,plain,
( sub(c10,name_1_1)
& val(c10,johannesburg_0)
& loc(c15,c9401)
& subs(c15,bekennen_1_1)
& attr(c9,c10)
& sub(c9,stadt__1_1)
& attr(c9235,c9236)
& attr(c9235,c9237)
& sub(c9235,putschistenf__374hrer_1_1)
& sub(c9236,eigenname_1_1)
& val(c9236,jonas_0)
& sub(c9237,familiename_1_1)
& val(c9237,savimbi_0)
& attch(c9245,c9251)
& attr(c9245,c9246)
& sub(c9245,land_1_1)
& sub(c9246,name_1_1)
& val(c9246,s__374dafrika_0)
& attr(c9251,c9252)
& attr(c9251,c9253)
& sub(c9251,pr__344sident_1_1)
& sub(c9252,eigenname_1_1)
& val(c9252,nelson_0)
& sub(c9253,familiename_1_1)
& val(c9253,mandela_0)
& agt(c9256,c9235)
& ornt(c9256,c9251)
& subs(c9256,anflehen_1_1)
& loc(c9372,c9397)
& sub(c9372,regierung_1_1)
& attr(c9380,c9381)
& sub(c9380,stadt__1_1)
& sub(c9381,name_1_1)
& val(c9381,luanda_0)
& preds(c9383,angriff_1_1)
& prop(c9383,weit_1_1)
& agt(c9387,c9235)
& mcont(c9387,c9383)
& obj(c9387,c9372)
& subs(c9387,abhalten_1_1)
& in(c9397,c9380)
& in(c9401,c9)
& assoc(putschistenf__374hrer_1_1,meuterer_1_1)
& sub(putschistenf__374hrer_1_1,an_f__374hrer_1_1)
& sort(c10,na)
& card(c10,int1)
& etype(c10,int0)
& fact(c10,real)
& gener(c10,sp)
& quant(c10,one)
& refer(c10,indet)
& varia(c10,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(johannesburg_0,fe)
& sort(c15,da)
& fact(c15,real)
& gener(c15,sp)
& sort(c9401,l)
& card(c9401,int1)
& etype(c9401,int0)
& fact(c9401,real)
& gener(c9401,sp)
& quant(c9401,one)
& refer(c9401,det)
& varia(c9401,con)
& sort(bekennen_1_1,da)
& fact(bekennen_1_1,real)
& gener(bekennen_1_1,ge)
& sort(c9,d)
& sort(c9,io)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& quant(c9,one)
& refer(c9,det)
& varia(c9,con)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(c9235,d)
& card(c9235,int1)
& etype(c9235,int0)
& fact(c9235,real)
& gener(c9235,sp)
& quant(c9235,one)
& refer(c9235,det)
& varia(c9235,con)
& sort(c9236,na)
& card(c9236,int1)
& etype(c9236,int0)
& fact(c9236,real)
& gener(c9236,sp)
& quant(c9236,one)
& refer(c9236,indet)
& varia(c9236,varia_c)
& sort(c9237,na)
& card(c9237,int1)
& etype(c9237,int0)
& fact(c9237,real)
& gener(c9237,sp)
& quant(c9237,one)
& refer(c9237,indet)
& varia(c9237,varia_c)
& sort(putschistenf__374hrer_1_1,d)
& card(putschistenf__374hrer_1_1,int1)
& etype(putschistenf__374hrer_1_1,int0)
& fact(putschistenf__374hrer_1_1,real)
& gener(putschistenf__374hrer_1_1,ge)
& quant(putschistenf__374hrer_1_1,one)
& refer(putschistenf__374hrer_1_1,refer_c)
& varia(putschistenf__374hrer_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(jonas_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(savimbi_0,fe)
& sort(c9245,d)
& sort(c9245,io)
& card(c9245,int1)
& etype(c9245,int0)
& fact(c9245,real)
& gener(c9245,sp)
& quant(c9245,one)
& refer(c9245,det)
& varia(c9245,con)
& sort(c9251,d)
& card(c9251,int1)
& etype(c9251,int0)
& fact(c9251,real)
& gener(c9251,sp)
& quant(c9251,one)
& refer(c9251,det)
& varia(c9251,varia_c)
& sort(c9246,na)
& card(c9246,int1)
& etype(c9246,int0)
& fact(c9246,real)
& gener(c9246,sp)
& quant(c9246,one)
& refer(c9246,indet)
& varia(c9246,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(s__374dafrika_0,fe)
& sort(c9252,na)
& card(c9252,int1)
& etype(c9252,int0)
& fact(c9252,real)
& gener(c9252,sp)
& quant(c9252,one)
& refer(c9252,indet)
& varia(c9252,varia_c)
& sort(c9253,na)
& card(c9253,int1)
& etype(c9253,int0)
& fact(c9253,real)
& gener(c9253,sp)
& quant(c9253,one)
& refer(c9253,indet)
& varia(c9253,varia_c)
& 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(nelson_0,fe)
& sort(mandela_0,fe)
& sort(c9256,da)
& fact(c9256,real)
& gener(c9256,sp)
& sort(anflehen_1_1,da)
& fact(anflehen_1_1,real)
& gener(anflehen_1_1,ge)
& sort(c9372,d)
& sort(c9372,io)
& card(c9372,int1)
& etype(c9372,int1)
& fact(c9372,real)
& gener(c9372,sp)
& quant(c9372,one)
& refer(c9372,det)
& varia(c9372,con)
& sort(c9397,l)
& card(c9397,int1)
& etype(c9397,int0)
& fact(c9397,real)
& gener(c9397,sp)
& quant(c9397,one)
& refer(c9397,det)
& varia(c9397,con)
& sort(regierung_1_1,d)
& sort(regierung_1_1,io)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& quant(regierung_1_1,quant_c)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& sort(c9380,d)
& sort(c9380,io)
& card(c9380,int1)
& etype(c9380,int0)
& fact(c9380,real)
& gener(c9380,sp)
& quant(c9380,one)
& refer(c9380,det)
& varia(c9380,con)
& sort(c9381,na)
& card(c9381,int1)
& etype(c9381,int0)
& fact(c9381,real)
& gener(c9381,sp)
& quant(c9381,one)
& refer(c9381,indet)
& varia(c9381,varia_c)
& sort(luanda_0,fe)
& sort(c9383,ad)
& card(c9383,cons(x_constant,cons(int1,nil)))
& etype(c9383,int1)
& fact(c9383,hypo)
& gener(c9383,sp)
& quant(c9383,mult)
& refer(c9383,indet)
& varia(c9383,varia_c)
& sort(angriff_1_1,ad)
& card(angriff_1_1,int1)
& etype(angriff_1_1,int0)
& fact(angriff_1_1,real)
& gener(angriff_1_1,ge)
& quant(angriff_1_1,one)
& refer(angriff_1_1,refer_c)
& varia(angriff_1_1,varia_c)
& sort(weit_1_1,mq)
& sort(c9387,da)
& fact(c9387,real)
& gener(c9387,sp)
& sort(sollen_0,md)
& fact(sollen_0,real)
& gener(sollen_0,gener_c)
& sort(abhalten_1_1,da)
& fact(abhalten_1_1,real)
& gener(abhalten_1_1,ge)
& sort(meuterer_1_1,d)
& card(meuterer_1_1,int1)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& quant(meuterer_1_1,one)
& refer(meuterer_1_1,refer_c)
& varia(meuterer_1_1,varia_c)
& sort(an_f__374hrer_1_1,d)
& card(an_f__374hrer_1_1,int1)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& quant(an_f__374hrer_1_1,one)
& refer(an_f__374hrer_1_1,refer_c)
& varia(an_f__374hrer_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10328,plain,
( sub(c10,name_1_1)
& val(c10,johannesburg_0)
& loc(c15,c9401)
& subs(c15,bekennen_1_1)
& attr(c9,c10)
& sub(c9,stadt__1_1)
& attr(c9235,c9236)
& attr(c9235,c9237)
& sub(c9235,putschistenf__374hrer_1_1)
& sub(c9236,eigenname_1_1)
& val(c9236,jonas_0)
& sub(c9237,familiename_1_1)
& val(c9237,savimbi_0)
& attch(c9245,c9251)
& attr(c9245,c9246)
& sub(c9245,land_1_1)
& sub(c9246,name_1_1)
& val(c9246,s__374dafrika_0)
& attr(c9251,c9252)
& attr(c9251,c9253)
& sub(c9251,pr__344sident_1_1)
& sub(c9252,eigenname_1_1)
& val(c9252,nelson_0)
& sub(c9253,familiename_1_1)
& val(c9253,mandela_0)
& agt(c9256,c9235)
& ornt(c9256,c9251)
& subs(c9256,anflehen_1_1)
& loc(c9372,c9397)
& sub(c9372,regierung_1_1)
& attr(c9380,c9381)
& sub(c9380,stadt__1_1)
& sub(c9381,name_1_1)
& val(c9381,luanda_0)
& preds(c9383,angriff_1_1)
& prop(c9383,weit_1_1)
& agt(c9387,c9235)
& mcont(c9387,c9383)
& obj(c9387,c9372)
& subs(c9387,abhalten_1_1)
& in(c9397,c9380)
& in(c9401,c9)
& assoc(putschistenf__374hrer_1_1,meuterer_1_1)
& sub(putschistenf__374hrer_1_1,an_f__374hrer_1_1)
& card(c10,int1)
& etype(c10,int0)
& fact(c10,real)
& gener(c10,sp)
& quant(c10,one)
& refer(c10,indet)
& varia(c10,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)
& fact(c15,real)
& gener(c15,sp)
& card(c9401,int1)
& etype(c9401,int0)
& fact(c9401,real)
& gener(c9401,sp)
& quant(c9401,one)
& refer(c9401,det)
& varia(c9401,con)
& fact(bekennen_1_1,real)
& gener(bekennen_1_1,ge)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& quant(c9,one)
& refer(c9,det)
& varia(c9,con)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& card(c9235,int1)
& etype(c9235,int0)
& fact(c9235,real)
& gener(c9235,sp)
& quant(c9235,one)
& refer(c9235,det)
& varia(c9235,con)
& card(c9236,int1)
& etype(c9236,int0)
& fact(c9236,real)
& gener(c9236,sp)
& quant(c9236,one)
& refer(c9236,indet)
& varia(c9236,varia_c)
& card(c9237,int1)
& etype(c9237,int0)
& fact(c9237,real)
& gener(c9237,sp)
& quant(c9237,one)
& refer(c9237,indet)
& varia(c9237,varia_c)
& card(putschistenf__374hrer_1_1,int1)
& etype(putschistenf__374hrer_1_1,int0)
& fact(putschistenf__374hrer_1_1,real)
& gener(putschistenf__374hrer_1_1,ge)
& quant(putschistenf__374hrer_1_1,one)
& refer(putschistenf__374hrer_1_1,refer_c)
& varia(putschistenf__374hrer_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(c9245,int1)
& etype(c9245,int0)
& fact(c9245,real)
& gener(c9245,sp)
& quant(c9245,one)
& refer(c9245,det)
& varia(c9245,con)
& card(c9251,int1)
& etype(c9251,int0)
& fact(c9251,real)
& gener(c9251,sp)
& quant(c9251,one)
& refer(c9251,det)
& varia(c9251,varia_c)
& card(c9246,int1)
& etype(c9246,int0)
& fact(c9246,real)
& gener(c9246,sp)
& quant(c9246,one)
& refer(c9246,indet)
& varia(c9246,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(c9252,int1)
& etype(c9252,int0)
& fact(c9252,real)
& gener(c9252,sp)
& quant(c9252,one)
& refer(c9252,indet)
& varia(c9252,varia_c)
& card(c9253,int1)
& etype(c9253,int0)
& fact(c9253,real)
& gener(c9253,sp)
& quant(c9253,one)
& refer(c9253,indet)
& varia(c9253,varia_c)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& fact(c9256,real)
& gener(c9256,sp)
& fact(anflehen_1_1,real)
& gener(anflehen_1_1,ge)
& card(c9372,int1)
& etype(c9372,int1)
& fact(c9372,real)
& gener(c9372,sp)
& quant(c9372,one)
& refer(c9372,det)
& varia(c9372,con)
& card(c9397,int1)
& etype(c9397,int0)
& fact(c9397,real)
& gener(c9397,sp)
& quant(c9397,one)
& refer(c9397,det)
& varia(c9397,con)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& quant(regierung_1_1,quant_c)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& card(c9380,int1)
& etype(c9380,int0)
& fact(c9380,real)
& gener(c9380,sp)
& quant(c9380,one)
& refer(c9380,det)
& varia(c9380,con)
& card(c9381,int1)
& etype(c9381,int0)
& fact(c9381,real)
& gener(c9381,sp)
& quant(c9381,one)
& refer(c9381,indet)
& varia(c9381,varia_c)
& card(c9383,cons(x_constant,cons(int1,nil)))
& etype(c9383,int1)
& fact(c9383,hypo)
& gener(c9383,sp)
& quant(c9383,mult)
& refer(c9383,indet)
& varia(c9383,varia_c)
& card(angriff_1_1,int1)
& etype(angriff_1_1,int0)
& fact(angriff_1_1,real)
& gener(angriff_1_1,ge)
& quant(angriff_1_1,one)
& refer(angriff_1_1,refer_c)
& varia(angriff_1_1,varia_c)
& fact(c9387,real)
& gener(c9387,sp)
& fact(sollen_0,real)
& gener(sollen_0,gener_c)
& fact(abhalten_1_1,real)
& gener(abhalten_1_1,ge)
& card(meuterer_1_1,int1)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& quant(meuterer_1_1,one)
& refer(meuterer_1_1,refer_c)
& varia(meuterer_1_1,varia_c)
& card(an_f__374hrer_1_1,int1)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& quant(an_f__374hrer_1_1,one)
& refer(an_f__374hrer_1_1,refer_c)
& varia(an_f__374hrer_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10192]) ).
fof(f10331,plain,
( sub(c10,name_1_1)
& val(c10,johannesburg_0)
& loc(c15,c9401)
& subs(c15,bekennen_1_1)
& attr(c9,c10)
& sub(c9,stadt__1_1)
& attr(c9235,c9236)
& attr(c9235,c9237)
& sub(c9235,putschistenf__374hrer_1_1)
& sub(c9236,eigenname_1_1)
& val(c9236,jonas_0)
& sub(c9237,familiename_1_1)
& val(c9237,savimbi_0)
& attch(c9245,c9251)
& attr(c9245,c9246)
& sub(c9245,land_1_1)
& sub(c9246,name_1_1)
& val(c9246,s__374dafrika_0)
& attr(c9251,c9252)
& attr(c9251,c9253)
& sub(c9251,pr__344sident_1_1)
& sub(c9252,eigenname_1_1)
& val(c9252,nelson_0)
& sub(c9253,familiename_1_1)
& val(c9253,mandela_0)
& agt(c9256,c9235)
& ornt(c9256,c9251)
& subs(c9256,anflehen_1_1)
& loc(c9372,c9397)
& sub(c9372,regierung_1_1)
& attr(c9380,c9381)
& sub(c9380,stadt__1_1)
& sub(c9381,name_1_1)
& val(c9381,luanda_0)
& preds(c9383,angriff_1_1)
& prop(c9383,weit_1_1)
& agt(c9387,c9235)
& mcont(c9387,c9383)
& obj(c9387,c9372)
& subs(c9387,abhalten_1_1)
& in(c9397,c9380)
& in(c9401,c9)
& assoc(putschistenf__374hrer_1_1,meuterer_1_1)
& sub(putschistenf__374hrer_1_1,an_f__374hrer_1_1)
& card(c10,int1)
& etype(c10,int0)
& fact(c10,real)
& gener(c10,sp)
& refer(c10,indet)
& varia(c10,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)
& fact(c15,real)
& gener(c15,sp)
& card(c9401,int1)
& etype(c9401,int0)
& fact(c9401,real)
& gener(c9401,sp)
& refer(c9401,det)
& varia(c9401,con)
& fact(bekennen_1_1,real)
& gener(bekennen_1_1,ge)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& refer(c9,det)
& varia(c9,con)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& card(c9235,int1)
& etype(c9235,int0)
& fact(c9235,real)
& gener(c9235,sp)
& refer(c9235,det)
& varia(c9235,con)
& card(c9236,int1)
& etype(c9236,int0)
& fact(c9236,real)
& gener(c9236,sp)
& refer(c9236,indet)
& varia(c9236,varia_c)
& card(c9237,int1)
& etype(c9237,int0)
& fact(c9237,real)
& gener(c9237,sp)
& refer(c9237,indet)
& varia(c9237,varia_c)
& card(putschistenf__374hrer_1_1,int1)
& etype(putschistenf__374hrer_1_1,int0)
& fact(putschistenf__374hrer_1_1,real)
& gener(putschistenf__374hrer_1_1,ge)
& refer(putschistenf__374hrer_1_1,refer_c)
& varia(putschistenf__374hrer_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(c9245,int1)
& etype(c9245,int0)
& fact(c9245,real)
& gener(c9245,sp)
& refer(c9245,det)
& varia(c9245,con)
& card(c9251,int1)
& etype(c9251,int0)
& fact(c9251,real)
& gener(c9251,sp)
& refer(c9251,det)
& varia(c9251,varia_c)
& card(c9246,int1)
& etype(c9246,int0)
& fact(c9246,real)
& gener(c9246,sp)
& refer(c9246,indet)
& varia(c9246,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(c9252,int1)
& etype(c9252,int0)
& fact(c9252,real)
& gener(c9252,sp)
& refer(c9252,indet)
& varia(c9252,varia_c)
& card(c9253,int1)
& etype(c9253,int0)
& fact(c9253,real)
& gener(c9253,sp)
& refer(c9253,indet)
& varia(c9253,varia_c)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& fact(c9256,real)
& gener(c9256,sp)
& fact(anflehen_1_1,real)
& gener(anflehen_1_1,ge)
& card(c9372,int1)
& etype(c9372,int1)
& fact(c9372,real)
& gener(c9372,sp)
& refer(c9372,det)
& varia(c9372,con)
& card(c9397,int1)
& etype(c9397,int0)
& fact(c9397,real)
& gener(c9397,sp)
& refer(c9397,det)
& varia(c9397,con)
& card(regierung_1_1,card_c)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& card(c9380,int1)
& etype(c9380,int0)
& fact(c9380,real)
& gener(c9380,sp)
& refer(c9380,det)
& varia(c9380,con)
& card(c9381,int1)
& etype(c9381,int0)
& fact(c9381,real)
& gener(c9381,sp)
& refer(c9381,indet)
& varia(c9381,varia_c)
& card(c9383,cons(x_constant,cons(int1,nil)))
& etype(c9383,int1)
& fact(c9383,hypo)
& gener(c9383,sp)
& refer(c9383,indet)
& varia(c9383,varia_c)
& card(angriff_1_1,int1)
& etype(angriff_1_1,int0)
& fact(angriff_1_1,real)
& gener(angriff_1_1,ge)
& refer(angriff_1_1,refer_c)
& varia(angriff_1_1,varia_c)
& fact(c9387,real)
& gener(c9387,sp)
& fact(sollen_0,real)
& gener(sollen_0,gener_c)
& fact(abhalten_1_1,real)
& gener(abhalten_1_1,ge)
& card(meuterer_1_1,int1)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& refer(meuterer_1_1,refer_c)
& varia(meuterer_1_1,varia_c)
& card(an_f__374hrer_1_1,int1)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& refer(an_f__374hrer_1_1,refer_c)
& varia(an_f__374hrer_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10328]) ).
fof(f10334,plain,
( sub(c10,name_1_1)
& val(c10,johannesburg_0)
& loc(c15,c9401)
& subs(c15,bekennen_1_1)
& attr(c9,c10)
& sub(c9,stadt__1_1)
& attr(c9235,c9236)
& attr(c9235,c9237)
& sub(c9235,putschistenf__374hrer_1_1)
& sub(c9236,eigenname_1_1)
& val(c9236,jonas_0)
& sub(c9237,familiename_1_1)
& val(c9237,savimbi_0)
& attch(c9245,c9251)
& attr(c9245,c9246)
& sub(c9245,land_1_1)
& sub(c9246,name_1_1)
& val(c9246,s__374dafrika_0)
& attr(c9251,c9252)
& attr(c9251,c9253)
& sub(c9251,pr__344sident_1_1)
& sub(c9252,eigenname_1_1)
& val(c9252,nelson_0)
& sub(c9253,familiename_1_1)
& val(c9253,mandela_0)
& agt(c9256,c9235)
& ornt(c9256,c9251)
& subs(c9256,anflehen_1_1)
& loc(c9372,c9397)
& sub(c9372,regierung_1_1)
& attr(c9380,c9381)
& sub(c9380,stadt__1_1)
& sub(c9381,name_1_1)
& val(c9381,luanda_0)
& preds(c9383,angriff_1_1)
& prop(c9383,weit_1_1)
& agt(c9387,c9235)
& mcont(c9387,c9383)
& obj(c9387,c9372)
& subs(c9387,abhalten_1_1)
& in(c9397,c9380)
& in(c9401,c9)
& assoc(putschistenf__374hrer_1_1,meuterer_1_1)
& sub(putschistenf__374hrer_1_1,an_f__374hrer_1_1)
& etype(c10,int0)
& fact(c10,real)
& gener(c10,sp)
& refer(c10,indet)
& varia(c10,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)
& fact(c15,real)
& gener(c15,sp)
& etype(c9401,int0)
& fact(c9401,real)
& gener(c9401,sp)
& refer(c9401,det)
& varia(c9401,con)
& fact(bekennen_1_1,real)
& gener(bekennen_1_1,ge)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& refer(c9,det)
& varia(c9,con)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& etype(c9235,int0)
& fact(c9235,real)
& gener(c9235,sp)
& refer(c9235,det)
& varia(c9235,con)
& etype(c9236,int0)
& fact(c9236,real)
& gener(c9236,sp)
& refer(c9236,indet)
& varia(c9236,varia_c)
& etype(c9237,int0)
& fact(c9237,real)
& gener(c9237,sp)
& refer(c9237,indet)
& varia(c9237,varia_c)
& etype(putschistenf__374hrer_1_1,int0)
& fact(putschistenf__374hrer_1_1,real)
& gener(putschistenf__374hrer_1_1,ge)
& refer(putschistenf__374hrer_1_1,refer_c)
& varia(putschistenf__374hrer_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(c9245,int0)
& fact(c9245,real)
& gener(c9245,sp)
& refer(c9245,det)
& varia(c9245,con)
& etype(c9251,int0)
& fact(c9251,real)
& gener(c9251,sp)
& refer(c9251,det)
& varia(c9251,varia_c)
& etype(c9246,int0)
& fact(c9246,real)
& gener(c9246,sp)
& refer(c9246,indet)
& varia(c9246,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(c9252,int0)
& fact(c9252,real)
& gener(c9252,sp)
& refer(c9252,indet)
& varia(c9252,varia_c)
& etype(c9253,int0)
& fact(c9253,real)
& gener(c9253,sp)
& refer(c9253,indet)
& varia(c9253,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)
& fact(c9256,real)
& gener(c9256,sp)
& fact(anflehen_1_1,real)
& gener(anflehen_1_1,ge)
& etype(c9372,int1)
& fact(c9372,real)
& gener(c9372,sp)
& refer(c9372,det)
& varia(c9372,con)
& etype(c9397,int0)
& fact(c9397,real)
& gener(c9397,sp)
& refer(c9397,det)
& varia(c9397,con)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& refer(regierung_1_1,refer_c)
& varia(regierung_1_1,varia_c)
& etype(c9380,int0)
& fact(c9380,real)
& gener(c9380,sp)
& refer(c9380,det)
& varia(c9380,con)
& etype(c9381,int0)
& fact(c9381,real)
& gener(c9381,sp)
& refer(c9381,indet)
& varia(c9381,varia_c)
& etype(c9383,int1)
& fact(c9383,hypo)
& gener(c9383,sp)
& refer(c9383,indet)
& varia(c9383,varia_c)
& etype(angriff_1_1,int0)
& fact(angriff_1_1,real)
& gener(angriff_1_1,ge)
& refer(angriff_1_1,refer_c)
& varia(angriff_1_1,varia_c)
& fact(c9387,real)
& gener(c9387,sp)
& fact(sollen_0,real)
& gener(sollen_0,gener_c)
& fact(abhalten_1_1,real)
& gener(abhalten_1_1,ge)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& refer(meuterer_1_1,refer_c)
& varia(meuterer_1_1,varia_c)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& refer(an_f__374hrer_1_1,refer_c)
& varia(an_f__374hrer_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10331]) ).
fof(f10337,plain,
( sub(c10,name_1_1)
& val(c10,johannesburg_0)
& loc(c15,c9401)
& subs(c15,bekennen_1_1)
& attr(c9,c10)
& sub(c9,stadt__1_1)
& attr(c9235,c9236)
& attr(c9235,c9237)
& sub(c9235,putschistenf__374hrer_1_1)
& sub(c9236,eigenname_1_1)
& val(c9236,jonas_0)
& sub(c9237,familiename_1_1)
& val(c9237,savimbi_0)
& attch(c9245,c9251)
& attr(c9245,c9246)
& sub(c9245,land_1_1)
& sub(c9246,name_1_1)
& val(c9246,s__374dafrika_0)
& attr(c9251,c9252)
& attr(c9251,c9253)
& sub(c9251,pr__344sident_1_1)
& sub(c9252,eigenname_1_1)
& val(c9252,nelson_0)
& sub(c9253,familiename_1_1)
& val(c9253,mandela_0)
& agt(c9256,c9235)
& ornt(c9256,c9251)
& subs(c9256,anflehen_1_1)
& loc(c9372,c9397)
& sub(c9372,regierung_1_1)
& attr(c9380,c9381)
& sub(c9380,stadt__1_1)
& sub(c9381,name_1_1)
& val(c9381,luanda_0)
& preds(c9383,angriff_1_1)
& prop(c9383,weit_1_1)
& agt(c9387,c9235)
& mcont(c9387,c9383)
& obj(c9387,c9372)
& subs(c9387,abhalten_1_1)
& in(c9397,c9380)
& in(c9401,c9)
& assoc(putschistenf__374hrer_1_1,meuterer_1_1)
& sub(putschistenf__374hrer_1_1,an_f__374hrer_1_1)
& etype(c10,int0)
& fact(c10,real)
& gener(c10,sp)
& varia(c10,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& varia(name_1_1,varia_c)
& fact(c15,real)
& gener(c15,sp)
& etype(c9401,int0)
& fact(c9401,real)
& gener(c9401,sp)
& varia(c9401,con)
& fact(bekennen_1_1,real)
& gener(bekennen_1_1,ge)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& varia(c9,con)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& varia(stadt__1_1,varia_c)
& etype(c9235,int0)
& fact(c9235,real)
& gener(c9235,sp)
& varia(c9235,con)
& etype(c9236,int0)
& fact(c9236,real)
& gener(c9236,sp)
& varia(c9236,varia_c)
& etype(c9237,int0)
& fact(c9237,real)
& gener(c9237,sp)
& varia(c9237,varia_c)
& etype(putschistenf__374hrer_1_1,int0)
& fact(putschistenf__374hrer_1_1,real)
& gener(putschistenf__374hrer_1_1,ge)
& varia(putschistenf__374hrer_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(c9245,int0)
& fact(c9245,real)
& gener(c9245,sp)
& varia(c9245,con)
& etype(c9251,int0)
& fact(c9251,real)
& gener(c9251,sp)
& varia(c9251,varia_c)
& etype(c9246,int0)
& fact(c9246,real)
& gener(c9246,sp)
& varia(c9246,varia_c)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& varia(land_1_1,varia_c)
& etype(c9252,int0)
& fact(c9252,real)
& gener(c9252,sp)
& varia(c9252,varia_c)
& etype(c9253,int0)
& fact(c9253,real)
& gener(c9253,sp)
& varia(c9253,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)
& fact(c9256,real)
& gener(c9256,sp)
& fact(anflehen_1_1,real)
& gener(anflehen_1_1,ge)
& etype(c9372,int1)
& fact(c9372,real)
& gener(c9372,sp)
& varia(c9372,con)
& etype(c9397,int0)
& fact(c9397,real)
& gener(c9397,sp)
& varia(c9397,con)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& varia(regierung_1_1,varia_c)
& etype(c9380,int0)
& fact(c9380,real)
& gener(c9380,sp)
& varia(c9380,con)
& etype(c9381,int0)
& fact(c9381,real)
& gener(c9381,sp)
& varia(c9381,varia_c)
& etype(c9383,int1)
& fact(c9383,hypo)
& gener(c9383,sp)
& varia(c9383,varia_c)
& etype(angriff_1_1,int0)
& fact(angriff_1_1,real)
& gener(angriff_1_1,ge)
& varia(angriff_1_1,varia_c)
& fact(c9387,real)
& gener(c9387,sp)
& fact(sollen_0,real)
& gener(sollen_0,gener_c)
& fact(abhalten_1_1,real)
& gener(abhalten_1_1,ge)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& varia(meuterer_1_1,varia_c)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& varia(an_f__374hrer_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10334]) ).
fof(f10342,plain,
( sub(c10,name_1_1)
& val(c10,johannesburg_0)
& loc(c15,c9401)
& subs(c15,bekennen_1_1)
& attr(c9,c10)
& sub(c9,stadt__1_1)
& attr(c9235,c9236)
& attr(c9235,c9237)
& sub(c9235,putschistenf__374hrer_1_1)
& sub(c9236,eigenname_1_1)
& val(c9236,jonas_0)
& sub(c9237,familiename_1_1)
& val(c9237,savimbi_0)
& attch(c9245,c9251)
& attr(c9245,c9246)
& sub(c9245,land_1_1)
& sub(c9246,name_1_1)
& val(c9246,s__374dafrika_0)
& attr(c9251,c9252)
& attr(c9251,c9253)
& sub(c9251,pr__344sident_1_1)
& sub(c9252,eigenname_1_1)
& val(c9252,nelson_0)
& sub(c9253,familiename_1_1)
& val(c9253,mandela_0)
& agt(c9256,c9235)
& ornt(c9256,c9251)
& subs(c9256,anflehen_1_1)
& loc(c9372,c9397)
& sub(c9372,regierung_1_1)
& attr(c9380,c9381)
& sub(c9380,stadt__1_1)
& sub(c9381,name_1_1)
& val(c9381,luanda_0)
& preds(c9383,angriff_1_1)
& prop(c9383,weit_1_1)
& agt(c9387,c9235)
& mcont(c9387,c9383)
& obj(c9387,c9372)
& subs(c9387,abhalten_1_1)
& in(c9397,c9380)
& in(c9401,c9)
& assoc(putschistenf__374hrer_1_1,meuterer_1_1)
& sub(putschistenf__374hrer_1_1,an_f__374hrer_1_1)
& etype(c10,int0)
& fact(c10,real)
& gener(c10,sp)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& fact(c15,real)
& gener(c15,sp)
& etype(c9401,int0)
& fact(c9401,real)
& gener(c9401,sp)
& fact(bekennen_1_1,real)
& gener(bekennen_1_1,ge)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& etype(c9235,int0)
& fact(c9235,real)
& gener(c9235,sp)
& etype(c9236,int0)
& fact(c9236,real)
& gener(c9236,sp)
& etype(c9237,int0)
& fact(c9237,real)
& gener(c9237,sp)
& etype(putschistenf__374hrer_1_1,int0)
& fact(putschistenf__374hrer_1_1,real)
& gener(putschistenf__374hrer_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(c9245,int0)
& fact(c9245,real)
& gener(c9245,sp)
& etype(c9251,int0)
& fact(c9251,real)
& gener(c9251,sp)
& etype(c9246,int0)
& fact(c9246,real)
& gener(c9246,sp)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& etype(c9252,int0)
& fact(c9252,real)
& gener(c9252,sp)
& etype(c9253,int0)
& fact(c9253,real)
& gener(c9253,sp)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& fact(c9256,real)
& gener(c9256,sp)
& fact(anflehen_1_1,real)
& gener(anflehen_1_1,ge)
& etype(c9372,int1)
& fact(c9372,real)
& gener(c9372,sp)
& etype(c9397,int0)
& fact(c9397,real)
& gener(c9397,sp)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& gener(regierung_1_1,ge)
& etype(c9380,int0)
& fact(c9380,real)
& gener(c9380,sp)
& etype(c9381,int0)
& fact(c9381,real)
& gener(c9381,sp)
& etype(c9383,int1)
& fact(c9383,hypo)
& gener(c9383,sp)
& etype(angriff_1_1,int0)
& fact(angriff_1_1,real)
& gener(angriff_1_1,ge)
& fact(c9387,real)
& gener(c9387,sp)
& fact(sollen_0,real)
& gener(sollen_0,gener_c)
& fact(abhalten_1_1,real)
& gener(abhalten_1_1,ge)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& gener(meuterer_1_1,ge)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge) ),
inference(pure_predicate_removal,[],[f10337]) ).
fof(f10347,plain,
( sub(c10,name_1_1)
& val(c10,johannesburg_0)
& loc(c15,c9401)
& subs(c15,bekennen_1_1)
& attr(c9,c10)
& sub(c9,stadt__1_1)
& attr(c9235,c9236)
& attr(c9235,c9237)
& sub(c9235,putschistenf__374hrer_1_1)
& sub(c9236,eigenname_1_1)
& val(c9236,jonas_0)
& sub(c9237,familiename_1_1)
& val(c9237,savimbi_0)
& attch(c9245,c9251)
& attr(c9245,c9246)
& sub(c9245,land_1_1)
& sub(c9246,name_1_1)
& val(c9246,s__374dafrika_0)
& attr(c9251,c9252)
& attr(c9251,c9253)
& sub(c9251,pr__344sident_1_1)
& sub(c9252,eigenname_1_1)
& val(c9252,nelson_0)
& sub(c9253,familiename_1_1)
& val(c9253,mandela_0)
& agt(c9256,c9235)
& ornt(c9256,c9251)
& subs(c9256,anflehen_1_1)
& loc(c9372,c9397)
& sub(c9372,regierung_1_1)
& attr(c9380,c9381)
& sub(c9380,stadt__1_1)
& sub(c9381,name_1_1)
& val(c9381,luanda_0)
& preds(c9383,angriff_1_1)
& prop(c9383,weit_1_1)
& agt(c9387,c9235)
& mcont(c9387,c9383)
& obj(c9387,c9372)
& subs(c9387,abhalten_1_1)
& in(c9397,c9380)
& in(c9401,c9)
& assoc(putschistenf__374hrer_1_1,meuterer_1_1)
& sub(putschistenf__374hrer_1_1,an_f__374hrer_1_1)
& etype(c10,int0)
& fact(c10,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& fact(c15,real)
& etype(c9401,int0)
& fact(c9401,real)
& fact(bekennen_1_1,real)
& etype(c9,int0)
& fact(c9,real)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& etype(c9235,int0)
& fact(c9235,real)
& etype(c9236,int0)
& fact(c9236,real)
& etype(c9237,int0)
& fact(c9237,real)
& etype(putschistenf__374hrer_1_1,int0)
& fact(putschistenf__374hrer_1_1,real)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& etype(c9245,int0)
& fact(c9245,real)
& etype(c9251,int0)
& fact(c9251,real)
& etype(c9246,int0)
& fact(c9246,real)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& etype(c9252,int0)
& fact(c9252,real)
& etype(c9253,int0)
& fact(c9253,real)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& fact(c9256,real)
& fact(anflehen_1_1,real)
& etype(c9372,int1)
& fact(c9372,real)
& etype(c9397,int0)
& fact(c9397,real)
& etype(regierung_1_1,int1)
& fact(regierung_1_1,real)
& etype(c9380,int0)
& fact(c9380,real)
& etype(c9381,int0)
& fact(c9381,real)
& etype(c9383,int1)
& fact(c9383,hypo)
& etype(angriff_1_1,int0)
& fact(angriff_1_1,real)
& fact(c9387,real)
& fact(sollen_0,real)
& fact(abhalten_1_1,real)
& etype(meuterer_1_1,int0)
& fact(meuterer_1_1,real)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real) ),
inference(pure_predicate_removal,[],[f10342]) ).
fof(f10521,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(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(flattening,[],[f10521]) ).
fof(f10523,plain,
! [X0,X1] :
( ? [X2] :
( arg1(X2,X0)
& arg2(X2,X1)
& subr(X2,sub_0) )
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f163]) ).
fof(f10545,plain,
! [X0,X1] :
( ? [X2] :
( attr(X1,X2)
& sub(X2,name_1_1)
& val(X2,X0) )
| ~ name(X1,X0) ),
inference(ennf_transformation,[],[f177]) ).
fof(f10546,plain,
! [X0,X1,X2] :
( name(X2,X1)
| ~ attr(X2,X0)
| ~ sub(X0,name_1_1)
| ~ val(X0,X1) ),
inference(ennf_transformation,[],[f178]) ).
fof(f10547,plain,
! [X0,X1,X2] :
( name(X2,X1)
| ~ attr(X2,X0)
| ~ sub(X0,name_1_1)
| ~ val(X0,X1) ),
inference(flattening,[],[f10546]) ).
fof(f10552,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ attr(X5,X6)
| ~ obj(X7,X0)
| ~ 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(f10596,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))],[f10522]) ).
fof(f10597,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))],[f10523]) ).
fof(f10602,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))],[f10545]) ).
fof(f10880,plain,
! [X2,X0,X1] :
( subr(sK56(X0,X1,X2),rprs_0)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10596]) ).
fof(f10881,plain,
! [X2,X0,X1] :
( sub(sK57(X0,X1,X2),X2)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10596]) ).
fof(f10882,plain,
! [X2,X0,X1] :
( obj(sK55(X0,X1,X2),X1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10596]) ).
fof(f10885,plain,
! [X2,X0,X1] :
( arg2(sK56(X0,X1,X2),sK57(X0,X1,X2))
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10596]) ).
fof(f10886,plain,
! [X2,X0,X1] :
( arg1(sK56(X0,X1,X2),X1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10596]) ).
fof(f10887,plain,
! [X0,X1] :
( subr(sK58(X0,X1),sub_0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10597]) ).
fof(f10888,plain,
! [X0,X1] :
( arg2(sK58(X0,X1),X1)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10597]) ).
fof(f10889,plain,
! [X0,X1] :
( arg1(sK58(X0,X1),X0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10597]) ).
fof(f10917,plain,
! [X0,X1] :
( val(sK61(X0,X1),X0)
| ~ name(X1,X0) ),
inference(cnf_transformation,[],[f10602]) ).
fof(f10918,plain,
! [X0,X1] :
( sub(sK61(X0,X1),name_1_1)
| ~ name(X1,X0) ),
inference(cnf_transformation,[],[f10602]) ).
fof(f10919,plain,
! [X0,X1] :
( attr(X1,sK61(X0,X1))
| ~ name(X1,X0) ),
inference(cnf_transformation,[],[f10602]) ).
fof(f10920,plain,
! [X2,X0,X1] :
( ~ val(X0,X1)
| ~ attr(X2,X0)
| ~ sub(X0,name_1_1)
| name(X2,X1) ),
inference(cnf_transformation,[],[f10547]) ).
fof(f20816,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ val(X6,s__374dafrika_0)
| ~ arg2(X3,X4)
| ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ attr(X5,X6)
| ~ obj(X7,X0)
| ~ 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)
| ~ arg1(X3,X0) ),
inference(cnf_transformation,[],[f10552]) ).
fof(f20897,plain,
val(c9253,mandela_0),
inference(cnf_transformation,[],[f10347]) ).
fof(f20898,plain,
sub(c9253,familiename_1_1),
inference(cnf_transformation,[],[f10347]) ).
fof(f20899,plain,
val(c9252,nelson_0),
inference(cnf_transformation,[],[f10347]) ).
fof(f20900,plain,
sub(c9252,eigenname_1_1),
inference(cnf_transformation,[],[f10347]) ).
fof(f20901,plain,
sub(c9251,pr__344sident_1_1),
inference(cnf_transformation,[],[f10347]) ).
fof(f20902,plain,
attr(c9251,c9253),
inference(cnf_transformation,[],[f10347]) ).
fof(f20903,plain,
attr(c9251,c9252),
inference(cnf_transformation,[],[f10347]) ).
fof(f20904,plain,
val(c9246,s__374dafrika_0),
inference(cnf_transformation,[],[f10347]) ).
fof(f20905,plain,
sub(c9246,name_1_1),
inference(cnf_transformation,[],[f10347]) ).
fof(f20907,plain,
attr(c9245,c9246),
inference(cnf_transformation,[],[f10347]) ).
fof(f21019,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ name(X0,s__374dafrika_0)
| ~ arg2(X1,X2)
| ~ attr(X3,X4)
| ~ attr(X3,X5)
| ~ attr(X6,sK61(s__374dafrika_0,X0))
| ~ obj(X7,X3)
| ~ sub(X4,familiename_1_1)
| ~ sub(X5,eigenname_1_1)
| ~ sub(X2,X8)
| ~ sub(sK61(s__374dafrika_0,X0),name_1_1)
| ~ subr(X1,rprs_0)
| ~ val(X4,mandela_0)
| ~ val(X5,nelson_0)
| ~ arg1(X1,X3) ),
inference(resolution,[],[f10917,f20816]) ).
fof(f21022,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ attr(X6,sK61(s__374dafrika_0,X0))
| ~ arg2(X1,X2)
| ~ attr(X3,X4)
| ~ attr(X3,X5)
| ~ name(X0,s__374dafrika_0)
| ~ obj(X7,X3)
| ~ sub(X4,familiename_1_1)
| ~ sub(X5,eigenname_1_1)
| ~ sub(X2,X8)
| ~ subr(X1,rprs_0)
| ~ val(X4,mandela_0)
| ~ val(X5,nelson_0)
| ~ arg1(X1,X3) ),
inference(forward_subsumption_resolution,[],[f21019,f10918]) ).
fof(f107299,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ arg2(X0,X1)
| ~ attr(X2,X3)
| ~ attr(X2,X4)
| ~ name(X5,s__374dafrika_0)
| ~ obj(X6,X2)
| ~ sub(X3,familiename_1_1)
| ~ sub(X4,eigenname_1_1)
| ~ sub(X1,X7)
| ~ subr(X0,rprs_0)
| ~ val(X3,mandela_0)
| ~ val(X4,nelson_0)
| ~ arg1(X0,X2)
| ~ name(X5,s__374dafrika_0) ),
inference(resolution,[],[f21022,f10919]) ).
fof(f107300,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ name(X5,s__374dafrika_0)
| ~ attr(X2,X3)
| ~ attr(X2,X4)
| ~ arg2(X0,X1)
| ~ obj(X6,X2)
| ~ sub(X3,familiename_1_1)
| ~ sub(X4,eigenname_1_1)
| ~ sub(X1,X7)
| ~ subr(X0,rprs_0)
| ~ val(X3,mandela_0)
| ~ val(X4,nelson_0)
| ~ arg1(X0,X2) ),
inference(duplicate_literal_removal,[],[f107299]) ).
fof(f107305,plain,
! [X0] :
( ~ attr(X0,c9246)
| ~ sub(c9246,name_1_1)
| name(X0,s__374dafrika_0) ),
inference(resolution,[],[f10920,f20904]) ).
fof(f107312,plain,
! [X0] :
( ~ attr(X0,c9246)
| name(X0,s__374dafrika_0) ),
inference(forward_subsumption_resolution,[],[f107305,f20905]) ).
fof(f107884,plain,
name(c9245,s__374dafrika_0),
inference(resolution,[],[f107312,f20907]) ).
fof(f107889,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ val(X2,nelson_0)
| ~ attr(X0,X2)
| ~ arg2(X3,X4)
| ~ obj(X5,X0)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X6)
| ~ subr(X3,rprs_0)
| ~ val(X1,mandela_0)
| ~ attr(X0,X1)
| ~ arg1(X3,X0) ),
inference(resolution,[],[f107884,f107300]) ).
fof(f107894,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ attr(X0,c9252)
| ~ arg2(X1,X2)
| ~ obj(X3,X0)
| ~ sub(X4,familiename_1_1)
| ~ sub(c9252,eigenname_1_1)
| ~ sub(X2,X5)
| ~ subr(X1,rprs_0)
| ~ val(X4,mandela_0)
| ~ attr(X0,X4)
| ~ arg1(X1,X0) ),
inference(resolution,[],[f107889,f20899]) ).
fof(f107896,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ val(X4,mandela_0)
| ~ arg2(X1,X2)
| ~ obj(X3,X0)
| ~ sub(X4,familiename_1_1)
| ~ sub(X2,X5)
| ~ subr(X1,rprs_0)
| ~ attr(X0,c9252)
| ~ attr(X0,X4)
| ~ arg1(X1,X0) ),
inference(forward_subsumption_resolution,[],[f107894,f20900]) ).
fof(f107900,plain,
! [X2,X3,X0,X1,X4] :
( ~ arg2(X0,X1)
| ~ obj(X2,X3)
| ~ sub(c9253,familiename_1_1)
| ~ sub(X1,X4)
| ~ subr(X0,rprs_0)
| ~ attr(X3,c9252)
| ~ attr(X3,c9253)
| ~ arg1(X0,X3) ),
inference(resolution,[],[f107896,f20897]) ).
fof(f107902,plain,
! [X2,X3,X0,X1,X4] :
( ~ subr(X0,rprs_0)
| ~ obj(X2,X3)
| ~ sub(X1,X4)
| ~ arg2(X0,X1)
| ~ attr(X3,c9252)
| ~ attr(X3,c9253)
| ~ arg1(X0,X3) ),
inference(forward_subsumption_resolution,[],[f107900,f20898]) ).
fof(f108050,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ arg2(sK56(X0,X1,X2),X5)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0)
| ~ obj(X3,X4)
| ~ sub(X5,X6)
| ~ arg1(X0,X1)
| ~ attr(X4,c9252)
| ~ attr(X4,c9253)
| ~ arg1(sK56(X0,X1,X2),X4) ),
inference(resolution,[],[f10880,f107902]) ).
fof(f108246,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0)
| ~ obj(X3,X4)
| ~ sub(sK57(X0,X1,X2),X5)
| ~ arg1(X0,X1)
| ~ attr(X4,c9252)
| ~ attr(X4,c9253)
| ~ arg1(sK56(X0,X1,X2),X4) ),
inference(resolution,[],[f10885,f108050]) ).
fof(f108248,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ arg1(sK56(X0,X1,X2),X4)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0)
| ~ obj(X3,X4)
| ~ sub(sK57(X0,X1,X2),X5)
| ~ attr(X4,c9252)
| ~ attr(X4,c9253)
| ~ arg1(X0,X1) ),
inference(duplicate_literal_removal,[],[f108246]) ).
fof(f108250,plain,
! [X2,X3,X0,X1,X4] :
( ~ arg2(X0,X1)
| ~ subr(X0,sub_0)
| ~ obj(X2,X3)
| ~ sub(sK57(X0,X3,X1),X4)
| ~ attr(X3,c9252)
| ~ attr(X3,c9253)
| ~ arg1(X0,X3)
| ~ arg1(X0,X3)
| ~ arg2(X0,X1)
| ~ subr(X0,sub_0) ),
inference(resolution,[],[f108248,f10886]) ).
fof(f108251,plain,
! [X2,X3,X0,X1,X4] :
( ~ sub(sK57(X0,X3,X1),X4)
| ~ subr(X0,sub_0)
| ~ obj(X2,X3)
| ~ arg2(X0,X1)
| ~ attr(X3,c9252)
| ~ attr(X3,c9253)
| ~ arg1(X0,X3) ),
inference(duplicate_literal_removal,[],[f108250]) ).
fof(f108265,plain,
! [X2,X3,X0,X1] :
( ~ subr(X0,sub_0)
| ~ obj(X1,X2)
| ~ arg2(X0,X3)
| ~ attr(X2,c9252)
| ~ attr(X2,c9253)
| ~ arg1(X0,X2)
| ~ arg1(X0,X2)
| ~ arg2(X0,X3)
| ~ subr(X0,sub_0) ),
inference(resolution,[],[f108251,f10881]) ).
fof(f108266,plain,
! [X2,X3,X0,X1] :
( ~ subr(X0,sub_0)
| ~ obj(X1,X2)
| ~ arg2(X0,X3)
| ~ attr(X2,c9252)
| ~ attr(X2,c9253)
| ~ arg1(X0,X2) ),
inference(duplicate_literal_removal,[],[f108265]) ).
fof(f108280,plain,
! [X2,X3,X0,X1,X4] :
( ~ arg2(sK58(X2,X3),X4)
| ~ obj(X0,X1)
| ~ attr(X1,c9252)
| ~ attr(X1,c9253)
| ~ arg1(sK58(X2,X3),X1)
| ~ sub(X2,X3) ),
inference(resolution,[],[f108266,f10887]) ).
fof(f108294,plain,
! [X2,X3,X0,X1] :
( ~ obj(X0,X1)
| ~ attr(X1,c9252)
| ~ attr(X1,c9253)
| ~ arg1(sK58(X2,X3),X1)
| ~ sub(X2,X3)
| ~ sub(X2,X3) ),
inference(resolution,[],[f108280,f10888]) ).
fof(f108295,plain,
! [X2,X3,X0,X1] :
( ~ arg1(sK58(X2,X3),X1)
| ~ attr(X1,c9252)
| ~ attr(X1,c9253)
| ~ obj(X0,X1)
| ~ sub(X2,X3) ),
inference(duplicate_literal_removal,[],[f108294]) ).
fof(f108309,plain,
! [X2,X0,X1] :
( ~ attr(X0,c9252)
| ~ attr(X0,c9253)
| ~ obj(X1,X0)
| ~ sub(X0,X2)
| ~ sub(X0,X2) ),
inference(resolution,[],[f108295,f10889]) ).
fof(f108310,plain,
! [X2,X0,X1] :
( ~ attr(X0,c9253)
| ~ attr(X0,c9252)
| ~ obj(X1,X0)
| ~ sub(X0,X2) ),
inference(duplicate_literal_removal,[],[f108309]) ).
fof(f108319,plain,
! [X0,X1] :
( ~ attr(c9251,c9252)
| ~ obj(X0,c9251)
| ~ sub(c9251,X1) ),
inference(resolution,[],[f108310,f20902]) ).
fof(f108320,plain,
! [X0,X1] :
( ~ obj(X0,c9251)
| ~ sub(c9251,X1) ),
inference(forward_subsumption_resolution,[],[f108319,f20903]) ).
fof(f108330,plain,
! [X2,X0,X1] :
( ~ subr(X1,sub_0)
| ~ arg1(X1,c9251)
| ~ arg2(X1,X2)
| ~ sub(c9251,X0) ),
inference(resolution,[],[f108320,f10882]) ).
fof(f108369,plain,
! [X2,X3,X0,X1] :
( ~ arg2(sK58(X0,X1),X2)
| ~ arg1(sK58(X0,X1),c9251)
| ~ sub(c9251,X3)
| ~ sub(X0,X1) ),
inference(resolution,[],[f108330,f10887]) ).
fof(f108402,plain,
! [X2,X0,X1] :
( ~ arg1(sK58(X0,X1),c9251)
| ~ sub(c9251,X2)
| ~ sub(X0,X1)
| ~ sub(X0,X1) ),
inference(resolution,[],[f108369,f10888]) ).
fof(f108403,plain,
! [X2,X0,X1] :
( ~ arg1(sK58(X0,X1),c9251)
| ~ sub(c9251,X2)
| ~ sub(X0,X1) ),
inference(duplicate_literal_removal,[],[f108402]) ).
fof(f108407,plain,
! [X0,X1] :
( ~ sub(c9251,X0)
| ~ sub(c9251,X1)
| ~ sub(c9251,X1) ),
inference(resolution,[],[f108403,f10889]) ).
fof(f108408,plain,
! [X0,X1] :
( ~ sub(c9251,X1)
| ~ sub(c9251,X0) ),
inference(duplicate_literal_removal,[],[f108407]) ).
fof(f108412,plain,
! [X0] : ~ sub(c9251,X0),
inference(resolution,[],[f108408,f20901]) ).
fof(f108415,plain,
$false,
inference(resolution,[],[f108412,f20901]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR116+19 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n004.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 23:28:07 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 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
% 26.14/4.08 % (888980)Will run a generic schedule for satisfiability detection.
% 26.14/4.08 % (888988)dis+10_1_sil=32000:sp=arity:random_seed=668370450:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 26.14/4.08 % (888986)% WARNING: option uhcvi not known.
% 26.14/4.08 % (888985)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=902296168_2998 on theBenchmark for (2998ds/0Mi)
% 26.14/4.08 % (888986)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=835460766:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 26.14/4.08 % (888987)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2926897704:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 26.14/4.08 % (888989)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2924872906:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 26.14/4.08 % (888991)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=169078709:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 26.14/4.08 % (888990)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1621997985:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 26.14/4.08 % (888988)Instruction limit reached!
% 26.14/4.08 % (888988)------------------------------
% 26.14/4.08 % (888988)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.14/4.08 % (888988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.14/4.08 % (888988)CaDiCaL version: 2.1.3
% 26.14/4.08 % (888988)Termination reason: Instruction limit
% 26.14/4.08 % (888988)Termination phase: Saturation
% 26.14/4.08 % (888988)Time elapsed: 0.035 s
% 26.14/4.08 % (888988)Peak memory usage: 26 MB
% 26.14/4.08 % (888988)Instructions burned: 107 (million)
% 26.14/4.08 % (888999)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4099588450:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 26.14/4.08 % (888989)Instruction limit reached!
% 26.14/4.08 % (888989)------------------------------
% 26.14/4.08 % (888989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.14/4.08 % (888989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.14/4.08 % (888989)CaDiCaL version: 2.1.3
% 26.14/4.08 % (888989)Termination reason: Instruction limit
% 26.14/4.08 % (888989)Termination phase: Blocked clause elimination
% 26.14/4.08 % (888989)Time elapsed: 0.073 s
% 26.14/4.08 % (888989)Peak memory usage: 28 MB
% 26.14/4.08 % (888989)Instructions burned: 117 (million)
% 26.14/4.08 % (888990)Instruction limit reached!
% 26.14/4.08 % (888990)------------------------------
% 26.14/4.08 % (888990)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.14/4.08 % (888990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.14/4.08 % (888990)CaDiCaL version: 2.1.3
% 26.14/4.08 % (888990)Termination reason: Instruction limit
% 26.14/4.08 % (888990)Termination phase: Saturation
% 26.14/4.08 % (888990)Time elapsed: 0.073 s
% 26.14/4.08 % (888990)Peak memory usage: 28 MB
% 26.14/4.08 % (888990)Instructions burned: 132 (million)
% 26.14/4.08 % (888991)Instruction limit reached!
% 26.14/4.08 % (888991)------------------------------
% 26.14/4.08 % (888991)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.14/4.08 % (888991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.14/4.08 % (888991)CaDiCaL version: 2.1.3
% 26.14/4.08 % (888991)Termination reason: Instruction limit
% 26.14/4.08 % (888991)Termination phase: Saturation
% 26.14/4.08 % (888991)Time elapsed: 0.088 s
% 26.14/4.08 % (888991)Peak memory usage: 30 MB
% 26.14/4.08 % (888991)Instructions burned: 159 (million)
% 26.14/4.08 % (889001)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3658611120:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 26.14/4.08 % (889002)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=1573822083:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 26.14/4.08 % (889003)ott-21_1_sil=16000:fs=off:random_seed=4269051296:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 26.14/4.08 % TRYING [1]
% 26.14/4.08 % TRYING [2]
% 26.14/4.08 % (889001)Instruction limit reached!
% 26.14/4.08 % (889001)------------------------------
% 26.14/4.08 % (889001)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.14/4.08 % (889001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.14/4.08 % (889001)CaDiCaL version: 2.1.3
% 16.28/6.31 % (889001)Termination reason: Instruction limit
% 16.28/6.31 % (889001)Termination phase: Blocked clause elimination
% 16.28/6.31 % (889001)Time elapsed: 0.083 s
% 16.28/6.31 % (889001)Peak memory usage: 29 MB
% 16.28/6.31 % (889001)Instructions burned: 132 (million)
% 16.28/6.31 % (889003)Instruction limit reached!
% 16.28/6.31 % (889003)------------------------------
% 16.28/6.31 % (889003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.31 % (889003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.31 % (889003)CaDiCaL version: 2.1.3
% 16.28/6.31 % (889003)Termination reason: Instruction limit
% 16.28/6.31 % (889003)Termination phase: Saturation
% 16.28/6.31 % (889003)Time elapsed: 0.090 s
% 16.28/6.31 % (889003)Peak memory usage: 28 MB
% 16.28/6.31 % (889003)Instructions burned: 181 (million)
% 16.28/6.31 % (889007)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1020369816:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 16.28/6.31 % (889009)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1277155138:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 16.28/6.31 % (888999)Instruction limit reached!
% 16.28/6.31 % (888999)------------------------------
% 16.28/6.31 % (888999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.31 % (888999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.31 % (888999)CaDiCaL version: 2.1.3
% 16.28/6.31 % (888999)Termination reason: Instruction limit
% 16.28/6.31 % (888999)Termination phase: Finite model building constraint generation
% 16.28/6.31 % (888999)Time elapsed: 0.184 s
% 16.28/6.31 % (888999)Peak memory usage: 54 MB
% 16.28/6.31 % (888999)Instructions burned: 719 (million)
% 16.28/6.31 % (889011)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1976106650:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 16.28/6.31 % TRYING [1]
% 16.28/6.31 % TRYING [2]
% 16.28/6.31 % TRYING [1]
% 16.28/6.31 % (889002)Instruction limit reached!
% 16.28/6.31 % (889002)------------------------------
% 16.28/6.31 % (889002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.31 % (889002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.31 % (889002)CaDiCaL version: 2.1.3
% 16.28/6.31 % (889002)Termination reason: Instruction limit
% 16.28/6.31 % (889002)Termination phase: Saturation
% 16.28/6.31 % (889002)Time elapsed: 0.356 s
% 16.28/6.31 % (889002)Peak memory usage: 36 MB
% 16.28/6.31 % (889002)Instructions burned: 684 (million)
% 16.28/6.31 % (889007)Instruction limit reached!
% 16.28/6.31 % (889007)------------------------------
% 16.28/6.31 % (889007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.31 % (889007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.31 % (889007)CaDiCaL version: 2.1.3
% 16.28/6.31 % (889007)Termination reason: Instruction limit
% 16.28/6.31 % (889007)Termination phase: Saturation
% 16.28/6.31 % (889007)Time elapsed: 0.250 s
% 16.28/6.31 % (889007)Peak memory usage: 36 MB
% 16.28/6.31 % (889007)Instructions burned: 477 (million)
% 16.28/6.31 % TRYING [3]
% 16.28/6.31 % (889014)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=2315380783:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 16.28/6.31 % (889013)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2745617876:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 16.28/6.31 % (889009)Instruction limit reached!
% 16.28/6.31 % (889009)------------------------------
% 16.28/6.31 % (889009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.31 % (889009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.31 % (889009)CaDiCaL version: 2.1.3
% 16.28/6.31 % (889009)Termination reason: Instruction limit
% 16.28/6.31 % (889009)Termination phase: Finite model building SAT solving
% 16.28/6.31 % (889009)Time elapsed: 0.330 s
% 16.28/6.31 % (889009)Peak memory usage: 39 MB
% 16.28/6.31 % (889009)Instructions burned: 867 (million)
% 16.28/6.31 % (889017)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=214359415:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 16.28/6.31 % (889011)Instruction limit reached!
% 16.28/6.31 % (889011)------------------------------
% 16.28/6.31 % (889011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.31 % (889011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.31 % (889011)CaDiCaL version: 2.1.3
% 16.28/6.31 % (889011)Termination reason: Instruction limit
% 16.28/6.31 % (889011)Termination phase: Saturation
% 16.28/6.31 % (889011)Time elapsed: 0.341 s
% 16.28/6.31 % (889011)Peak memory usage: 54 MB
% 16.28/6.31 % (889011)Instructions burned: 1180 (million)
% 16.28/6.31 % (889019)fmb+10_1_sil=64000:random_seed=1595420053:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 16.28/6.31 % TRYING [1]
% 16.28/6.31 % (889014)Instruction limit reached!
% 16.28/6.31 % (889014)------------------------------
% 16.28/6.31 % (889014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.31 % (889014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.31 % (889014)CaDiCaL version: 2.1.3
% 16.28/6.31 % (889014)Termination reason: Instruction limit
% 16.28/6.31 % (889014)Termination phase: Saturation
% 16.28/6.31 % (889014)Time elapsed: 0.365 s
% 16.28/6.31 % (889014)Peak memory usage: 39 MB
% 16.28/6.31 % (889014)Instructions burned: 694 (million)
% 16.28/6.31 % (889021)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=117905123:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 16.28/6.31 % TRYING [2]
% 16.28/6.31 % (889013)Instruction limit reached!
% 16.28/6.31 % (889013)------------------------------
% 16.28/6.31 % (889013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.31 % (889013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.31 % (889013)CaDiCaL version: 2.1.3
% 16.28/6.31 % (889013)Termination reason: Instruction limit
% 16.28/6.31 % (889013)Termination phase: Finite model building constraint generation
% 16.28/6.31 % (889013)Time elapsed: 0.426 s
% 16.28/6.31 % (889013)Peak memory usage: 93 MB
% 16.28/6.31 % (889013)Instructions burned: 891 (million)
% 16.28/6.31 % (889023)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1405619830:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 16.28/6.31 % (889017)Instruction limit reached!
% 16.28/6.31 % (889017)------------------------------
% 16.28/6.31 % (889017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.31 % (889017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.31 % (889017)CaDiCaL version: 2.1.3
% 16.28/6.31 % (889017)Termination reason: Instruction limit
% 16.28/6.31 % (889017)Termination phase: Saturation
% 16.28/6.31 % (889017)Time elapsed: 0.378 s
% 16.28/6.31 % (889017)Peak memory usage: 42 MB
% 16.28/6.31 % (889017)Instructions burned: 880 (million)
% 16.28/6.31 % (889025)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=87340558:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 16.28/6.31 % TRYING [20]
% 16.28/6.31 % TRYING [8]
% 16.28/6.31 % TRYING [3]
% 16.28/6.31 % (889023)Instruction limit reached!
% 16.28/6.31 % (889023)------------------------------
% 16.28/6.31 % (889023)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.31 % (889023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.31 % (889023)CaDiCaL version: 2.1.3
% 16.28/6.31 % (889023)Termination reason: Instruction limit
% 16.28/6.31 % (889023)Termination phase: Finite model building constraint generation
% 16.28/6.31 % (889023)Time elapsed: 0.361 s
% 16.28/6.31 % (889023)Peak memory usage: 64 MB
% 16.28/6.31 % (889023)Instructions burned: 930 (million)
% 16.28/6.31 % (889027)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3386043053:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 16.28/6.32 % TRYING [4]
% 16.28/6.32 % (889027)Instruction limit reached!
% 16.28/6.32 % (889027)------------------------------
% 16.28/6.32 % (889027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.32 % (889027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.32 % (889027)CaDiCaL version: 2.1.3
% 16.28/6.32 % (889027)Termination reason: Instruction limit
% 16.28/6.32 % (889027)Termination phase: Saturation
% 16.28/6.32 % (889027)Time elapsed: 0.669 s
% 16.28/6.32 % (889027)Peak memory usage: 35 MB
% 16.28/6.32 % (889027)Instructions burned: 1473 (million)
% 16.28/6.32 % (889029)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=970241038:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 16.28/6.32 % TRYING [77]
% 16.28/6.32 % TRYING [4]
% 16.28/6.32 % (889025)Instruction limit reached!
% 16.28/6.32 % (889025)------------------------------
% 16.28/6.32 % (889025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.32 % (889025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.32 % (889025)CaDiCaL version: 2.1.3
% 16.28/6.32 % (889025)Termination reason: Instruction limit
% 16.28/6.32 % (889025)Termination phase: Saturation
% 16.28/6.32 % (889025)Time elapsed: 2.694 s
% 16.28/6.32 % (889025)Peak memory usage: 39 MB
% 16.28/6.32 % (889025)Instructions burned: 5131 (million)
% 16.28/6.32 % (889031)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1271512122:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 16.28/6.32 % TRYING [16]
% 16.28/6.32 % (889021)Instruction limit reached!
% 16.28/6.32 % (889021)------------------------------
% 16.28/6.32 % (889021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.32 % (889021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.32 % (889021)CaDiCaL version: 2.1.3
% 16.28/6.32 % (889021)Termination reason: Instruction limit
% 16.28/6.32 % (889021)Termination phase: Finite model building constraint generation
% 16.28/6.32 % (889021)Time elapsed: 3.293 s
% 16.28/6.32 % (889021)Peak memory usage: 550 MB
% 16.28/6.32 % (889021)Instructions burned: 9518 (million)
% 16.28/6.32 % (889033)ott-2_1_sil=16000:newcnf=on:random_seed=2694117923:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 16.28/6.32 % (889029)Instruction limit reached!
% 16.28/6.32 % (889029)------------------------------
% 16.28/6.32 % (889029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.32 % (889029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.32 % (889029)CaDiCaL version: 2.1.3
% 16.28/6.32 % (889029)Termination reason: Instruction limit
% 16.28/6.32 % (889029)Termination phase: Finite model building constraint generation
% 16.28/6.32 % (889029)Time elapsed: 2.260 s
% 16.28/6.32 % (889029)Peak memory usage: 417 MB
% 16.28/6.32 % (889029)Instructions burned: 6326 (million)
% 16.28/6.32 % (889035)ott+10_1_sil=32000:tgt=ground:random_seed=2814988008:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 16.28/6.32 % TRYING [5]
% 16.28/6.32 % (889031)Instruction limit reached!
% 16.28/6.32 % (889031)------------------------------
% 16.28/6.32 % (889031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.32 % (889031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.32 % (889031)CaDiCaL version: 2.1.3
% 16.28/6.32 % (889031)Termination reason: Instruction limit
% 16.28/6.32 % (889031)Termination phase: Finite model building constraint generation
% 16.28/6.32 % (889031)Time elapsed: 0.750 s
% 16.28/6.32 % (889031)Peak memory usage: 121 MB
% 16.28/6.32 % (889031)Instructions burned: 2176 (million)
% 16.28/6.32 % (889037)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4280625496:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 16.28/6.32 % (889033)Instruction limit reached!
% 16.28/6.32 % (889033)------------------------------
% 16.28/6.32 % (889033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.32 % (889033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.32 % (889033)CaDiCaL version: 2.1.3
% 16.28/6.32 % (889033)Termination reason: Instruction limit
% 16.28/6.32 % (889033)Termination phase: Saturation
% 16.28/6.32 % (889033)Time elapsed: 0.453 s
% 16.28/6.32 % (889033)Peak memory usage: 34 MB
% 16.28/6.32 % (889033)Instructions burned: 869 (million)
% 16.28/6.32 % (889039)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2920245205:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 16.28/6.32 % TRYING [1]
% 16.28/6.32 % TRYING [2]
% 16.28/6.32 % TRYING [3]
% 16.28/6.32 % (889035) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-888980-889035"...
% 16.28/6.32 % (889035)...printing done.
% 16.28/6.32 % (889035)Refutation found. Thanks to Tanya!
% 16.28/6.32 % SZS status Theorem for theBenchmark
% 16.28/6.32 % SZS output start Proof for theBenchmark
% See solution above
% 16.28/6.33 % (889035)------------------------------
% 16.28/6.33 % (889035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 16.28/6.33 % (889035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.28/6.33 % (889035)CaDiCaL version: 2.1.3
% 16.28/6.33 % (889035)Termination reason: Refutation
% 16.28/6.33 % (889035)Time elapsed: 1.511 s
% 16.28/6.33 % (889035)Peak memory usage: 96 MB
% 16.28/6.33 % (889035)Instructions burned: 2849 (million)
% 16.28/6.33 % (888980)Success in time 6.096 s
% 16.28/6.33 % Vampire exiting
%------------------------------------------------------------------------------