%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR116+36 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:43:40 AM UTC 2026
% Result : Theorem 2.97s 1.51s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 10
% Syntax : Number of formulae : 105 ( 18 unt; 4 def)
% Number of atoms : 1898 ( 0 equ)
% Maximal formula atoms : 211 ( 18 avg)
% Number of connectives : 2105 ( 312 ~; 269 |;1517 &)
% ( 4 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 211 ( 21 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 32 ( 31 usr; 5 prp; 0-2 aty)
% Number of functors : 61 ( 61 usr; 54 con; 0-3 aty)
% Number of variables : 256 ( 0 sgn 216 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f155,axiom,
! [X0,X1,X2] :
( ( prop(X0,X1)
& state_adjective_state_binding(X1,X2) )
=> ? [X3,X4,X5] :
( in(X5,X3)
& attr(X3,X4)
& loc(X0,X5)
& sub(X3,land_1_1)
& sub(X4,name_1_1)
& val(X4,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',state_adjective__in_state) ).
fof(f162,axiom,
! [X0,X1,X2] :
( ( arg1(X0,X1)
& arg2(X0,X2)
& subr(X0,sub_0) )
=> ? [X3,X4,X5] :
( arg1(X4,X1)
& arg2(X4,X5)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& sub(X5,X2)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sub__bezeichnen_1_1_als) ).
fof(f163,axiom,
! [X0,X1] :
( sub(X0,X1)
=> ? [X2] :
( arg1(X2,X0)
& arg2(X2,X1)
& subr(X2,sub_0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sub__sub_0_expansion) ).
fof(f9161,axiom,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_8980) ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( in(X5,X6)
& arg1(X3,X0)
& arg2(X3,X4)
& attr(X0,X1)
& attr(X0,X2)
& attr(X6,X7)
& obj(X8,X0)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X9)
& sub(X7,name_1_1)
& subr(X3,rprs_0)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X7,s__374dafrika_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_010_mira_wp_716) ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( in(X5,X6)
& arg1(X3,X0)
& arg2(X3,X4)
& attr(X0,X1)
& attr(X0,X2)
& attr(X6,X7)
& obj(X8,X0)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X9)
& sub(X7,name_1_1)
& subr(X3,rprs_0)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X7,s__374dafrika_0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( sub(c11,hauptagentur_1_1)
& attch(c15,c11)
& loc(c15,c32)
& prop(c15,s__374dafrikanisch_1_1)
& sub(c15,pr__344sident_1_1)
& attr(c21,c22)
& sub(c21,stadt__1_1)
& sub(c22,name_1_1)
& val(c22,kapstadt_0)
& agt(c26,c5)
& init(c26,c34)
& obj(c26,c11)
& rslt(c26,c33)
& subs(c26,umbenennen_1_1)
& attr(c28,c29)
& sub(c28,stadt__1_1)
& sub(c29,name_1_1)
& val(c29,genadendal_0)
& in(c32,c21)
& arg1(c33,c11)
& arg2(c33,c28)
& subr(c33,name_0)
& arg1(c34,c11)
& subr(c34,name_0)
& attr(c5,c6)
& attr(c5,c7)
& sub(c5,mensch_1_1)
& sub(c6,eigenname_1_1)
& val(c6,nelson_0)
& sub(c7,familiename_1_1)
& val(c7,mandela_0)
& assoc(hauptagentur_1_1,haupt_1_1)
& sub(hauptagentur_1_1,b__374ro_1_1)
& sort(c11,d)
& sort(c11,io)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,det)
& varia(c11,con)
& sort(hauptagentur_1_1,d)
& sort(hauptagentur_1_1,io)
& card(hauptagentur_1_1,int1)
& etype(hauptagentur_1_1,int0)
& fact(hauptagentur_1_1,real)
& gener(hauptagentur_1_1,ge)
& quant(hauptagentur_1_1,one)
& refer(hauptagentur_1_1,refer_c)
& varia(hauptagentur_1_1,varia_c)
& sort(c15,d)
& card(c15,int1)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& quant(c15,one)
& refer(c15,det)
& varia(c15,con)
& sort(c32,l)
& card(c32,int1)
& etype(c32,int0)
& fact(c32,real)
& gener(c32,sp)
& quant(c32,one)
& refer(c32,det)
& varia(c32,con)
& sort(s__374dafrikanisch_1_1,nq)
& sort(pr__344sident_1_1,d)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& sort(c21,d)
& sort(c21,io)
& card(c21,int1)
& etype(c21,int0)
& fact(c21,real)
& gener(c21,sp)
& quant(c21,one)
& refer(c21,det)
& varia(c21,con)
& sort(c22,na)
& card(c22,int1)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,sp)
& quant(c22,one)
& refer(c22,indet)
& varia(c22,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(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(kapstadt_0,fe)
& sort(c26,da)
& fact(c26,real)
& gener(c26,sp)
& sort(c5,d)
& card(c5,int1)
& etype(c5,int0)
& fact(c5,real)
& gener(c5,sp)
& quant(c5,one)
& refer(c5,det)
& varia(c5,con)
& sort(c34,st)
& fact(c34,real)
& gener(c34,sp)
& sort(c33,st)
& fact(c33,real)
& gener(c33,sp)
& sort(umbenennen_1_1,da)
& fact(umbenennen_1_1,real)
& gener(umbenennen_1_1,ge)
& sort(c28,d)
& sort(c28,io)
& card(c28,int1)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& quant(c28,one)
& refer(c28,det)
& varia(c28,con)
& sort(c29,na)
& card(c29,int1)
& etype(c29,int0)
& fact(c29,real)
& gener(c29,sp)
& quant(c29,one)
& refer(c29,indet)
& varia(c29,varia_c)
& sort(genadendal_0,fe)
& sort(name_0,st)
& fact(name_0,real)
& gener(name_0,gener_c)
& sort(c6,na)
& card(c6,int1)
& etype(c6,int0)
& fact(c6,real)
& gener(c6,sp)
& quant(c6,one)
& refer(c6,indet)
& varia(c6,varia_c)
& sort(c7,na)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,indet)
& varia(c7,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(haupt_1_1,d)
& card(haupt_1_1,int1)
& etype(haupt_1_1,int0)
& fact(haupt_1_1,real)
& gener(haupt_1_1,ge)
& quant(haupt_1_1,one)
& refer(haupt_1_1,refer_c)
& varia(haupt_1_1,varia_c)
& sort(b__374ro_1_1,d)
& sort(b__374ro_1_1,io)
& card(b__374ro_1_1,int1)
& etype(b__374ro_1_1,int0)
& fact(b__374ro_1_1,real)
& gener(b__374ro_1_1,ge)
& quant(b__374ro_1_1,one)
& refer(b__374ro_1_1,refer_c)
& varia(b__374ro_1_1,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_wp_716) ).
fof(f10191,plain,
( sub(c11,hauptagentur_1_1)
& attch(c15,c11)
& loc(c15,c32)
& prop(c15,s__374dafrikanisch_1_1)
& sub(c15,pr__344sident_1_1)
& attr(c21,c22)
& sub(c21,stadt__1_1)
& sub(c22,name_1_1)
& val(c22,kapstadt_0)
& agt(c26,c5)
& obj(c26,c11)
& rslt(c26,c33)
& subs(c26,umbenennen_1_1)
& attr(c28,c29)
& sub(c28,stadt__1_1)
& sub(c29,name_1_1)
& val(c29,genadendal_0)
& in(c32,c21)
& arg1(c33,c11)
& arg2(c33,c28)
& subr(c33,name_0)
& arg1(c34,c11)
& subr(c34,name_0)
& attr(c5,c6)
& attr(c5,c7)
& sub(c5,mensch_1_1)
& sub(c6,eigenname_1_1)
& val(c6,nelson_0)
& sub(c7,familiename_1_1)
& val(c7,mandela_0)
& assoc(hauptagentur_1_1,haupt_1_1)
& sub(hauptagentur_1_1,b__374ro_1_1)
& sort(c11,d)
& sort(c11,io)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,det)
& varia(c11,con)
& sort(hauptagentur_1_1,d)
& sort(hauptagentur_1_1,io)
& card(hauptagentur_1_1,int1)
& etype(hauptagentur_1_1,int0)
& fact(hauptagentur_1_1,real)
& gener(hauptagentur_1_1,ge)
& quant(hauptagentur_1_1,one)
& refer(hauptagentur_1_1,refer_c)
& varia(hauptagentur_1_1,varia_c)
& sort(c15,d)
& card(c15,int1)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& quant(c15,one)
& refer(c15,det)
& varia(c15,con)
& sort(c32,l)
& card(c32,int1)
& etype(c32,int0)
& fact(c32,real)
& gener(c32,sp)
& quant(c32,one)
& refer(c32,det)
& varia(c32,con)
& sort(s__374dafrikanisch_1_1,nq)
& sort(pr__344sident_1_1,d)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& sort(c21,d)
& sort(c21,io)
& card(c21,int1)
& etype(c21,int0)
& fact(c21,real)
& gener(c21,sp)
& quant(c21,one)
& refer(c21,det)
& varia(c21,con)
& sort(c22,na)
& card(c22,int1)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,sp)
& quant(c22,one)
& refer(c22,indet)
& varia(c22,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(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(kapstadt_0,fe)
& sort(c26,da)
& fact(c26,real)
& gener(c26,sp)
& sort(c5,d)
& card(c5,int1)
& etype(c5,int0)
& fact(c5,real)
& gener(c5,sp)
& quant(c5,one)
& refer(c5,det)
& varia(c5,con)
& sort(c34,st)
& fact(c34,real)
& gener(c34,sp)
& sort(c33,st)
& fact(c33,real)
& gener(c33,sp)
& sort(umbenennen_1_1,da)
& fact(umbenennen_1_1,real)
& gener(umbenennen_1_1,ge)
& sort(c28,d)
& sort(c28,io)
& card(c28,int1)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& quant(c28,one)
& refer(c28,det)
& varia(c28,con)
& sort(c29,na)
& card(c29,int1)
& etype(c29,int0)
& fact(c29,real)
& gener(c29,sp)
& quant(c29,one)
& refer(c29,indet)
& varia(c29,varia_c)
& sort(genadendal_0,fe)
& sort(name_0,st)
& fact(name_0,real)
& gener(name_0,gener_c)
& sort(c6,na)
& card(c6,int1)
& etype(c6,int0)
& fact(c6,real)
& gener(c6,sp)
& quant(c6,one)
& refer(c6,indet)
& varia(c6,varia_c)
& sort(c7,na)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,indet)
& varia(c7,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(haupt_1_1,d)
& card(haupt_1_1,int1)
& etype(haupt_1_1,int0)
& fact(haupt_1_1,real)
& gener(haupt_1_1,ge)
& quant(haupt_1_1,one)
& refer(haupt_1_1,refer_c)
& varia(haupt_1_1,varia_c)
& sort(b__374ro_1_1,d)
& sort(b__374ro_1_1,io)
& card(b__374ro_1_1,int1)
& etype(b__374ro_1_1,int0)
& fact(b__374ro_1_1,real)
& gener(b__374ro_1_1,ge)
& quant(b__374ro_1_1,one)
& refer(b__374ro_1_1,refer_c)
& varia(b__374ro_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10195,plain,
( sub(c11,hauptagentur_1_1)
& attch(c15,c11)
& loc(c15,c32)
& prop(c15,s__374dafrikanisch_1_1)
& sub(c15,pr__344sident_1_1)
& attr(c21,c22)
& sub(c21,stadt__1_1)
& sub(c22,name_1_1)
& val(c22,kapstadt_0)
& agt(c26,c5)
& obj(c26,c11)
& rslt(c26,c33)
& subs(c26,umbenennen_1_1)
& attr(c28,c29)
& sub(c28,stadt__1_1)
& sub(c29,name_1_1)
& val(c29,genadendal_0)
& in(c32,c21)
& arg1(c33,c11)
& arg2(c33,c28)
& subr(c33,name_0)
& arg1(c34,c11)
& subr(c34,name_0)
& attr(c5,c6)
& attr(c5,c7)
& sub(c5,mensch_1_1)
& sub(c6,eigenname_1_1)
& val(c6,nelson_0)
& sub(c7,familiename_1_1)
& val(c7,mandela_0)
& assoc(hauptagentur_1_1,haupt_1_1)
& sub(hauptagentur_1_1,b__374ro_1_1)
& sort(c11,d)
& sort(c11,io)
& card(c11,int1)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,det)
& varia(c11,con)
& sort(hauptagentur_1_1,d)
& sort(hauptagentur_1_1,io)
& card(hauptagentur_1_1,int1)
& fact(hauptagentur_1_1,real)
& gener(hauptagentur_1_1,ge)
& quant(hauptagentur_1_1,one)
& refer(hauptagentur_1_1,refer_c)
& varia(hauptagentur_1_1,varia_c)
& sort(c15,d)
& card(c15,int1)
& fact(c15,real)
& gener(c15,sp)
& quant(c15,one)
& refer(c15,det)
& varia(c15,con)
& sort(c32,l)
& card(c32,int1)
& fact(c32,real)
& gener(c32,sp)
& quant(c32,one)
& refer(c32,det)
& varia(c32,con)
& sort(s__374dafrikanisch_1_1,nq)
& sort(pr__344sident_1_1,d)
& card(pr__344sident_1_1,int1)
& 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(c21,d)
& sort(c21,io)
& card(c21,int1)
& fact(c21,real)
& gener(c21,sp)
& quant(c21,one)
& refer(c21,det)
& varia(c21,con)
& sort(c22,na)
& card(c22,int1)
& fact(c22,real)
& gener(c22,sp)
& quant(c22,one)
& refer(c22,indet)
& varia(c22,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& 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(name_1_1,na)
& card(name_1_1,int1)
& 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(kapstadt_0,fe)
& sort(c26,da)
& fact(c26,real)
& gener(c26,sp)
& sort(c5,d)
& card(c5,int1)
& fact(c5,real)
& gener(c5,sp)
& quant(c5,one)
& refer(c5,det)
& varia(c5,con)
& sort(c34,st)
& fact(c34,real)
& gener(c34,sp)
& sort(c33,st)
& fact(c33,real)
& gener(c33,sp)
& sort(umbenennen_1_1,da)
& fact(umbenennen_1_1,real)
& gener(umbenennen_1_1,ge)
& sort(c28,d)
& sort(c28,io)
& card(c28,int1)
& fact(c28,real)
& gener(c28,sp)
& quant(c28,one)
& refer(c28,det)
& varia(c28,con)
& sort(c29,na)
& card(c29,int1)
& fact(c29,real)
& gener(c29,sp)
& quant(c29,one)
& refer(c29,indet)
& varia(c29,varia_c)
& sort(genadendal_0,fe)
& sort(name_0,st)
& fact(name_0,real)
& gener(name_0,gener_c)
& sort(c6,na)
& card(c6,int1)
& fact(c6,real)
& gener(c6,sp)
& quant(c6,one)
& refer(c6,indet)
& varia(c6,varia_c)
& sort(c7,na)
& card(c7,int1)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,indet)
& varia(c7,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& 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)
& 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)
& 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(haupt_1_1,d)
& card(haupt_1_1,int1)
& fact(haupt_1_1,real)
& gener(haupt_1_1,ge)
& quant(haupt_1_1,one)
& refer(haupt_1_1,refer_c)
& varia(haupt_1_1,varia_c)
& sort(b__374ro_1_1,d)
& sort(b__374ro_1_1,io)
& card(b__374ro_1_1,int1)
& fact(b__374ro_1_1,real)
& gener(b__374ro_1_1,ge)
& quant(b__374ro_1_1,one)
& refer(b__374ro_1_1,refer_c)
& varia(b__374ro_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10217,plain,
( sub(c11,hauptagentur_1_1)
& attch(c15,c11)
& loc(c15,c32)
& prop(c15,s__374dafrikanisch_1_1)
& sub(c15,pr__344sident_1_1)
& attr(c21,c22)
& sub(c21,stadt__1_1)
& sub(c22,name_1_1)
& val(c22,kapstadt_0)
& agt(c26,c5)
& obj(c26,c11)
& rslt(c26,c33)
& subs(c26,umbenennen_1_1)
& attr(c28,c29)
& sub(c28,stadt__1_1)
& sub(c29,name_1_1)
& val(c29,genadendal_0)
& in(c32,c21)
& arg1(c33,c11)
& arg2(c33,c28)
& subr(c33,name_0)
& arg1(c34,c11)
& subr(c34,name_0)
& attr(c5,c6)
& attr(c5,c7)
& sub(c5,mensch_1_1)
& sub(c6,eigenname_1_1)
& val(c6,nelson_0)
& sub(c7,familiename_1_1)
& val(c7,mandela_0)
& sub(hauptagentur_1_1,b__374ro_1_1)
& sort(c11,d)
& sort(c11,io)
& card(c11,int1)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,det)
& varia(c11,con)
& sort(hauptagentur_1_1,d)
& sort(hauptagentur_1_1,io)
& card(hauptagentur_1_1,int1)
& fact(hauptagentur_1_1,real)
& gener(hauptagentur_1_1,ge)
& quant(hauptagentur_1_1,one)
& refer(hauptagentur_1_1,refer_c)
& varia(hauptagentur_1_1,varia_c)
& sort(c15,d)
& card(c15,int1)
& fact(c15,real)
& gener(c15,sp)
& quant(c15,one)
& refer(c15,det)
& varia(c15,con)
& sort(c32,l)
& card(c32,int1)
& fact(c32,real)
& gener(c32,sp)
& quant(c32,one)
& refer(c32,det)
& varia(c32,con)
& sort(s__374dafrikanisch_1_1,nq)
& sort(pr__344sident_1_1,d)
& card(pr__344sident_1_1,int1)
& 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(c21,d)
& sort(c21,io)
& card(c21,int1)
& fact(c21,real)
& gener(c21,sp)
& quant(c21,one)
& refer(c21,det)
& varia(c21,con)
& sort(c22,na)
& card(c22,int1)
& fact(c22,real)
& gener(c22,sp)
& quant(c22,one)
& refer(c22,indet)
& varia(c22,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& 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(name_1_1,na)
& card(name_1_1,int1)
& 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(kapstadt_0,fe)
& sort(c26,da)
& fact(c26,real)
& gener(c26,sp)
& sort(c5,d)
& card(c5,int1)
& fact(c5,real)
& gener(c5,sp)
& quant(c5,one)
& refer(c5,det)
& varia(c5,con)
& sort(c34,st)
& fact(c34,real)
& gener(c34,sp)
& sort(c33,st)
& fact(c33,real)
& gener(c33,sp)
& sort(umbenennen_1_1,da)
& fact(umbenennen_1_1,real)
& gener(umbenennen_1_1,ge)
& sort(c28,d)
& sort(c28,io)
& card(c28,int1)
& fact(c28,real)
& gener(c28,sp)
& quant(c28,one)
& refer(c28,det)
& varia(c28,con)
& sort(c29,na)
& card(c29,int1)
& fact(c29,real)
& gener(c29,sp)
& quant(c29,one)
& refer(c29,indet)
& varia(c29,varia_c)
& sort(genadendal_0,fe)
& sort(name_0,st)
& fact(name_0,real)
& gener(name_0,gener_c)
& sort(c6,na)
& card(c6,int1)
& fact(c6,real)
& gener(c6,sp)
& quant(c6,one)
& refer(c6,indet)
& varia(c6,varia_c)
& sort(c7,na)
& card(c7,int1)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,indet)
& varia(c7,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& 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)
& 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)
& 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(haupt_1_1,d)
& card(haupt_1_1,int1)
& fact(haupt_1_1,real)
& gener(haupt_1_1,ge)
& quant(haupt_1_1,one)
& refer(haupt_1_1,refer_c)
& varia(haupt_1_1,varia_c)
& sort(b__374ro_1_1,d)
& sort(b__374ro_1_1,io)
& card(b__374ro_1_1,int1)
& fact(b__374ro_1_1,real)
& gener(b__374ro_1_1,ge)
& quant(b__374ro_1_1,one)
& refer(b__374ro_1_1,refer_c)
& varia(b__374ro_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10195]) ).
fof(f10227,plain,
( sub(c11,hauptagentur_1_1)
& attch(c15,c11)
& loc(c15,c32)
& prop(c15,s__374dafrikanisch_1_1)
& sub(c15,pr__344sident_1_1)
& attr(c21,c22)
& sub(c21,stadt__1_1)
& sub(c22,name_1_1)
& val(c22,kapstadt_0)
& agt(c26,c5)
& obj(c26,c11)
& rslt(c26,c33)
& subs(c26,umbenennen_1_1)
& attr(c28,c29)
& sub(c28,stadt__1_1)
& sub(c29,name_1_1)
& val(c29,genadendal_0)
& in(c32,c21)
& arg1(c33,c11)
& arg2(c33,c28)
& subr(c33,name_0)
& arg1(c34,c11)
& subr(c34,name_0)
& attr(c5,c6)
& attr(c5,c7)
& sub(c5,mensch_1_1)
& sub(c6,eigenname_1_1)
& val(c6,nelson_0)
& sub(c7,familiename_1_1)
& val(c7,mandela_0)
& sub(hauptagentur_1_1,b__374ro_1_1)
& card(c11,int1)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,det)
& varia(c11,con)
& card(hauptagentur_1_1,int1)
& fact(hauptagentur_1_1,real)
& gener(hauptagentur_1_1,ge)
& quant(hauptagentur_1_1,one)
& refer(hauptagentur_1_1,refer_c)
& varia(hauptagentur_1_1,varia_c)
& card(c15,int1)
& fact(c15,real)
& gener(c15,sp)
& quant(c15,one)
& refer(c15,det)
& varia(c15,con)
& card(c32,int1)
& fact(c32,real)
& gener(c32,sp)
& quant(c32,one)
& refer(c32,det)
& varia(c32,con)
& card(pr__344sident_1_1,int1)
& 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(c21,int1)
& fact(c21,real)
& gener(c21,sp)
& quant(c21,one)
& refer(c21,det)
& varia(c21,con)
& card(c22,int1)
& fact(c22,real)
& gener(c22,sp)
& quant(c22,one)
& refer(c22,indet)
& varia(c22,varia_c)
& card(stadt__1_1,int1)
& 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(name_1_1,int1)
& 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(c26,real)
& gener(c26,sp)
& card(c5,int1)
& fact(c5,real)
& gener(c5,sp)
& quant(c5,one)
& refer(c5,det)
& varia(c5,con)
& fact(c34,real)
& gener(c34,sp)
& fact(c33,real)
& gener(c33,sp)
& fact(umbenennen_1_1,real)
& gener(umbenennen_1_1,ge)
& card(c28,int1)
& fact(c28,real)
& gener(c28,sp)
& quant(c28,one)
& refer(c28,det)
& varia(c28,con)
& card(c29,int1)
& fact(c29,real)
& gener(c29,sp)
& quant(c29,one)
& refer(c29,indet)
& varia(c29,varia_c)
& fact(name_0,real)
& gener(name_0,gener_c)
& card(c6,int1)
& fact(c6,real)
& gener(c6,sp)
& quant(c6,one)
& refer(c6,indet)
& varia(c6,varia_c)
& card(c7,int1)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,indet)
& varia(c7,varia_c)
& card(mensch_1_1,int1)
& 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)
& 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)
& 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(haupt_1_1,int1)
& fact(haupt_1_1,real)
& gener(haupt_1_1,ge)
& quant(haupt_1_1,one)
& refer(haupt_1_1,refer_c)
& varia(haupt_1_1,varia_c)
& card(b__374ro_1_1,int1)
& fact(b__374ro_1_1,real)
& gener(b__374ro_1_1,ge)
& quant(b__374ro_1_1,one)
& refer(b__374ro_1_1,refer_c)
& varia(b__374ro_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10217]) ).
fof(f10230,plain,
( sub(c11,hauptagentur_1_1)
& attch(c15,c11)
& loc(c15,c32)
& prop(c15,s__374dafrikanisch_1_1)
& sub(c15,pr__344sident_1_1)
& attr(c21,c22)
& sub(c21,stadt__1_1)
& sub(c22,name_1_1)
& val(c22,kapstadt_0)
& agt(c26,c5)
& obj(c26,c11)
& rslt(c26,c33)
& subs(c26,umbenennen_1_1)
& attr(c28,c29)
& sub(c28,stadt__1_1)
& sub(c29,name_1_1)
& val(c29,genadendal_0)
& in(c32,c21)
& arg1(c33,c11)
& arg2(c33,c28)
& subr(c33,name_0)
& arg1(c34,c11)
& subr(c34,name_0)
& attr(c5,c6)
& attr(c5,c7)
& sub(c5,mensch_1_1)
& sub(c6,eigenname_1_1)
& val(c6,nelson_0)
& sub(c7,familiename_1_1)
& val(c7,mandela_0)
& sub(hauptagentur_1_1,b__374ro_1_1)
& card(c11,int1)
& fact(c11,real)
& gener(c11,sp)
& refer(c11,det)
& varia(c11,con)
& card(hauptagentur_1_1,int1)
& fact(hauptagentur_1_1,real)
& gener(hauptagentur_1_1,ge)
& refer(hauptagentur_1_1,refer_c)
& varia(hauptagentur_1_1,varia_c)
& card(c15,int1)
& fact(c15,real)
& gener(c15,sp)
& refer(c15,det)
& varia(c15,con)
& card(c32,int1)
& fact(c32,real)
& gener(c32,sp)
& refer(c32,det)
& varia(c32,con)
& card(pr__344sident_1_1,int1)
& 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(c21,int1)
& fact(c21,real)
& gener(c21,sp)
& refer(c21,det)
& varia(c21,con)
& card(c22,int1)
& fact(c22,real)
& gener(c22,sp)
& refer(c22,indet)
& varia(c22,varia_c)
& card(stadt__1_1,int1)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& card(name_1_1,int1)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& fact(c26,real)
& gener(c26,sp)
& card(c5,int1)
& fact(c5,real)
& gener(c5,sp)
& refer(c5,det)
& varia(c5,con)
& fact(c34,real)
& gener(c34,sp)
& fact(c33,real)
& gener(c33,sp)
& fact(umbenennen_1_1,real)
& gener(umbenennen_1_1,ge)
& card(c28,int1)
& fact(c28,real)
& gener(c28,sp)
& refer(c28,det)
& varia(c28,con)
& card(c29,int1)
& fact(c29,real)
& gener(c29,sp)
& refer(c29,indet)
& varia(c29,varia_c)
& fact(name_0,real)
& gener(name_0,gener_c)
& card(c6,int1)
& fact(c6,real)
& gener(c6,sp)
& refer(c6,indet)
& varia(c6,varia_c)
& card(c7,int1)
& fact(c7,real)
& gener(c7,sp)
& refer(c7,indet)
& varia(c7,varia_c)
& card(mensch_1_1,int1)
& 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)
& 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)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& card(haupt_1_1,int1)
& fact(haupt_1_1,real)
& gener(haupt_1_1,ge)
& refer(haupt_1_1,refer_c)
& varia(haupt_1_1,varia_c)
& card(b__374ro_1_1,int1)
& fact(b__374ro_1_1,real)
& gener(b__374ro_1_1,ge)
& refer(b__374ro_1_1,refer_c)
& varia(b__374ro_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10227]) ).
fof(f10233,plain,
( sub(c11,hauptagentur_1_1)
& attch(c15,c11)
& loc(c15,c32)
& prop(c15,s__374dafrikanisch_1_1)
& sub(c15,pr__344sident_1_1)
& attr(c21,c22)
& sub(c21,stadt__1_1)
& sub(c22,name_1_1)
& val(c22,kapstadt_0)
& agt(c26,c5)
& obj(c26,c11)
& rslt(c26,c33)
& subs(c26,umbenennen_1_1)
& attr(c28,c29)
& sub(c28,stadt__1_1)
& sub(c29,name_1_1)
& val(c29,genadendal_0)
& in(c32,c21)
& arg1(c33,c11)
& arg2(c33,c28)
& subr(c33,name_0)
& arg1(c34,c11)
& subr(c34,name_0)
& attr(c5,c6)
& attr(c5,c7)
& sub(c5,mensch_1_1)
& sub(c6,eigenname_1_1)
& val(c6,nelson_0)
& sub(c7,familiename_1_1)
& val(c7,mandela_0)
& sub(hauptagentur_1_1,b__374ro_1_1)
& fact(c11,real)
& gener(c11,sp)
& refer(c11,det)
& varia(c11,con)
& fact(hauptagentur_1_1,real)
& gener(hauptagentur_1_1,ge)
& refer(hauptagentur_1_1,refer_c)
& varia(hauptagentur_1_1,varia_c)
& fact(c15,real)
& gener(c15,sp)
& refer(c15,det)
& varia(c15,con)
& fact(c32,real)
& gener(c32,sp)
& refer(c32,det)
& varia(c32,con)
& 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(c21,real)
& gener(c21,sp)
& refer(c21,det)
& varia(c21,con)
& fact(c22,real)
& gener(c22,sp)
& refer(c22,indet)
& varia(c22,varia_c)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& fact(c26,real)
& gener(c26,sp)
& fact(c5,real)
& gener(c5,sp)
& refer(c5,det)
& varia(c5,con)
& fact(c34,real)
& gener(c34,sp)
& fact(c33,real)
& gener(c33,sp)
& fact(umbenennen_1_1,real)
& gener(umbenennen_1_1,ge)
& fact(c28,real)
& gener(c28,sp)
& refer(c28,det)
& varia(c28,con)
& fact(c29,real)
& gener(c29,sp)
& refer(c29,indet)
& varia(c29,varia_c)
& fact(name_0,real)
& gener(name_0,gener_c)
& fact(c6,real)
& gener(c6,sp)
& refer(c6,indet)
& varia(c6,varia_c)
& fact(c7,real)
& gener(c7,sp)
& refer(c7,indet)
& varia(c7,varia_c)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& fact(haupt_1_1,real)
& gener(haupt_1_1,ge)
& refer(haupt_1_1,refer_c)
& varia(haupt_1_1,varia_c)
& fact(b__374ro_1_1,real)
& gener(b__374ro_1_1,ge)
& refer(b__374ro_1_1,refer_c)
& varia(b__374ro_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10230]) ).
fof(f10236,plain,
( sub(c11,hauptagentur_1_1)
& attch(c15,c11)
& loc(c15,c32)
& prop(c15,s__374dafrikanisch_1_1)
& sub(c15,pr__344sident_1_1)
& attr(c21,c22)
& sub(c21,stadt__1_1)
& sub(c22,name_1_1)
& val(c22,kapstadt_0)
& agt(c26,c5)
& obj(c26,c11)
& rslt(c26,c33)
& subs(c26,umbenennen_1_1)
& attr(c28,c29)
& sub(c28,stadt__1_1)
& sub(c29,name_1_1)
& val(c29,genadendal_0)
& in(c32,c21)
& arg1(c33,c11)
& arg2(c33,c28)
& subr(c33,name_0)
& arg1(c34,c11)
& subr(c34,name_0)
& attr(c5,c6)
& attr(c5,c7)
& sub(c5,mensch_1_1)
& sub(c6,eigenname_1_1)
& val(c6,nelson_0)
& sub(c7,familiename_1_1)
& val(c7,mandela_0)
& sub(hauptagentur_1_1,b__374ro_1_1)
& fact(c11,real)
& gener(c11,sp)
& varia(c11,con)
& fact(hauptagentur_1_1,real)
& gener(hauptagentur_1_1,ge)
& varia(hauptagentur_1_1,varia_c)
& fact(c15,real)
& gener(c15,sp)
& varia(c15,con)
& fact(c32,real)
& gener(c32,sp)
& varia(c32,con)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& varia(pr__344sident_1_1,varia_c)
& fact(c21,real)
& gener(c21,sp)
& varia(c21,con)
& fact(c22,real)
& gener(c22,sp)
& varia(c22,varia_c)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& varia(stadt__1_1,varia_c)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& varia(name_1_1,varia_c)
& fact(c26,real)
& gener(c26,sp)
& fact(c5,real)
& gener(c5,sp)
& varia(c5,con)
& fact(c34,real)
& gener(c34,sp)
& fact(c33,real)
& gener(c33,sp)
& fact(umbenennen_1_1,real)
& gener(umbenennen_1_1,ge)
& fact(c28,real)
& gener(c28,sp)
& varia(c28,con)
& fact(c29,real)
& gener(c29,sp)
& varia(c29,varia_c)
& fact(name_0,real)
& gener(name_0,gener_c)
& fact(c6,real)
& gener(c6,sp)
& varia(c6,varia_c)
& fact(c7,real)
& gener(c7,sp)
& varia(c7,varia_c)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& varia(mensch_1_1,varia_c)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& varia(eigenname_1_1,varia_c)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& varia(familiename_1_1,varia_c)
& fact(haupt_1_1,real)
& gener(haupt_1_1,ge)
& varia(haupt_1_1,varia_c)
& fact(b__374ro_1_1,real)
& gener(b__374ro_1_1,ge)
& varia(b__374ro_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10233]) ).
fof(f10241,plain,
( sub(c11,hauptagentur_1_1)
& attch(c15,c11)
& loc(c15,c32)
& prop(c15,s__374dafrikanisch_1_1)
& sub(c15,pr__344sident_1_1)
& attr(c21,c22)
& sub(c21,stadt__1_1)
& sub(c22,name_1_1)
& val(c22,kapstadt_0)
& agt(c26,c5)
& obj(c26,c11)
& rslt(c26,c33)
& subs(c26,umbenennen_1_1)
& attr(c28,c29)
& sub(c28,stadt__1_1)
& sub(c29,name_1_1)
& val(c29,genadendal_0)
& in(c32,c21)
& arg1(c33,c11)
& arg2(c33,c28)
& subr(c33,name_0)
& arg1(c34,c11)
& subr(c34,name_0)
& attr(c5,c6)
& attr(c5,c7)
& sub(c5,mensch_1_1)
& sub(c6,eigenname_1_1)
& val(c6,nelson_0)
& sub(c7,familiename_1_1)
& val(c7,mandela_0)
& sub(hauptagentur_1_1,b__374ro_1_1)
& fact(c11,real)
& gener(c11,sp)
& fact(hauptagentur_1_1,real)
& gener(hauptagentur_1_1,ge)
& fact(c15,real)
& gener(c15,sp)
& fact(c32,real)
& gener(c32,sp)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& fact(c21,real)
& gener(c21,sp)
& fact(c22,real)
& gener(c22,sp)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& fact(c26,real)
& gener(c26,sp)
& fact(c5,real)
& gener(c5,sp)
& fact(c34,real)
& gener(c34,sp)
& fact(c33,real)
& gener(c33,sp)
& fact(umbenennen_1_1,real)
& gener(umbenennen_1_1,ge)
& fact(c28,real)
& gener(c28,sp)
& fact(c29,real)
& gener(c29,sp)
& fact(name_0,real)
& gener(name_0,gener_c)
& fact(c6,real)
& gener(c6,sp)
& fact(c7,real)
& gener(c7,sp)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& fact(haupt_1_1,real)
& gener(haupt_1_1,ge)
& fact(b__374ro_1_1,real)
& gener(b__374ro_1_1,ge) ),
inference(pure_predicate_removal,[],[f10236]) ).
fof(f10246,plain,
( sub(c11,hauptagentur_1_1)
& attch(c15,c11)
& loc(c15,c32)
& prop(c15,s__374dafrikanisch_1_1)
& sub(c15,pr__344sident_1_1)
& attr(c21,c22)
& sub(c21,stadt__1_1)
& sub(c22,name_1_1)
& val(c22,kapstadt_0)
& agt(c26,c5)
& obj(c26,c11)
& rslt(c26,c33)
& subs(c26,umbenennen_1_1)
& attr(c28,c29)
& sub(c28,stadt__1_1)
& sub(c29,name_1_1)
& val(c29,genadendal_0)
& in(c32,c21)
& arg1(c33,c11)
& arg2(c33,c28)
& subr(c33,name_0)
& arg1(c34,c11)
& subr(c34,name_0)
& attr(c5,c6)
& attr(c5,c7)
& sub(c5,mensch_1_1)
& sub(c6,eigenname_1_1)
& val(c6,nelson_0)
& sub(c7,familiename_1_1)
& val(c7,mandela_0)
& sub(hauptagentur_1_1,b__374ro_1_1)
& fact(c11,real)
& fact(hauptagentur_1_1,real)
& fact(c15,real)
& fact(c32,real)
& fact(pr__344sident_1_1,real)
& fact(c21,real)
& fact(c22,real)
& fact(stadt__1_1,real)
& fact(name_1_1,real)
& fact(c26,real)
& fact(c5,real)
& fact(c34,real)
& fact(c33,real)
& fact(umbenennen_1_1,real)
& fact(c28,real)
& fact(c29,real)
& fact(name_0,real)
& fact(c6,real)
& fact(c7,real)
& fact(mensch_1_1,real)
& fact(eigenname_1_1,real)
& fact(familiename_1_1,real)
& fact(haupt_1_1,real)
& fact(b__374ro_1_1,real) ),
inference(pure_predicate_removal,[],[f10241]) ).
fof(f10249,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ in(X5,X6)
| ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ attr(X6,X7)
| ~ obj(X8,X0)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X9)
| ~ sub(X7,name_1_1)
| ~ subr(X3,rprs_0)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ val(X7,s__374dafrika_0) ),
inference(ennf_transformation,[],[f10189]) ).
fof(f10256,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(f10257,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,[],[f10256]) ).
fof(f10309,plain,
! [X0,X1] :
( ? [X2] :
( arg1(X2,X0)
& arg2(X2,X1)
& subr(X2,sub_0) )
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f163]) ).
fof(f10335,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( in(X5,X3)
& attr(X3,X4)
& loc(X0,X5)
& sub(X3,land_1_1)
& sub(X4,name_1_1)
& val(X4,X2) )
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(ennf_transformation,[],[f155]) ).
fof(f10336,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( in(X5,X3)
& attr(X3,X4)
& loc(X0,X5)
& sub(X3,land_1_1)
& sub(X4,name_1_1)
& val(X4,X2) )
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(flattening,[],[f10335]) ).
fof(f10377,plain,
! [X0,X1,X2] :
( ( arg1(sK2(X0,X1,X2),X1)
& arg2(sK2(X0,X1,X2),sK3(X0,X1,X2))
& hsit(X0,sK1(X0,X1,X2))
& mcont(sK1(X0,X1,X2),sK2(X0,X1,X2))
& obj(sK1(X0,X1,X2),X1)
& sub(sK3(X0,X1,X2),X2)
& subr(sK2(X0,X1,X2),rprs_0)
& subs(sK1(X0,X1,X2),bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X3,sK1(X0,X1,X2)),skolemize(X4,sK2(X0,X1,X2)),skolemize(X5,sK3(X0,X1,X2))],[f10257]) ).
fof(f10391,plain,
! [X0,X1] :
( ( arg1(sK22(X0,X1),X0)
& arg2(sK22(X0,X1),X1)
& subr(sK22(X0,X1),sub_0) )
| ~ sub(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(X2,sK22(X0,X1))],[f10309]) ).
fof(f10400,plain,
! [X0,X1,X2] :
( ( in(sK33(X0,X2),sK31(X0,X2))
& attr(sK31(X0,X2),sK32(X0,X2))
& loc(X0,sK33(X0,X2))
& sub(sK31(X0,X2),land_1_1)
& sub(sK32(X0,X2),name_1_1)
& val(sK32(X0,X2),X2) )
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31,sK32,sK33]),skolemize(X3,sK31(X0,X2)),skolemize(X4,sK32(X0,X2)),skolemize(X5,sK33(X0,X2))],[f10336]) ).
fof(f10409,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ in(X5,X6)
| ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ attr(X6,X7)
| ~ obj(X8,X0)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X9)
| ~ sub(X7,name_1_1)
| ~ subr(X3,rprs_0)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ val(X7,s__374dafrika_0) ),
inference(cnf_transformation,[],[f10249]) ).
fof(f10435,plain,
val(c7,mandela_0),
inference(cnf_transformation,[],[f10246]) ).
fof(f10436,plain,
sub(c7,familiename_1_1),
inference(cnf_transformation,[],[f10246]) ).
fof(f10437,plain,
val(c6,nelson_0),
inference(cnf_transformation,[],[f10246]) ).
fof(f10438,plain,
sub(c6,eigenname_1_1),
inference(cnf_transformation,[],[f10246]) ).
fof(f10439,plain,
sub(c5,mensch_1_1),
inference(cnf_transformation,[],[f10246]) ).
fof(f10440,plain,
attr(c5,c7),
inference(cnf_transformation,[],[f10246]) ).
fof(f10441,plain,
attr(c5,c6),
inference(cnf_transformation,[],[f10246]) ).
fof(f10461,plain,
prop(c15,s__374dafrikanisch_1_1),
inference(cnf_transformation,[],[f10246]) ).
fof(f10469,plain,
! [X2,X0,X1] :
( subr(sK2(X0,X1,X2),rprs_0)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10377]) ).
fof(f10470,plain,
! [X2,X0,X1] :
( sub(sK3(X0,X1,X2),X2)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10377]) ).
fof(f10471,plain,
! [X2,X0,X1] :
( obj(sK1(X0,X1,X2),X1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10377]) ).
fof(f10474,plain,
! [X2,X0,X1] :
( arg2(sK2(X0,X1,X2),sK3(X0,X1,X2))
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10377]) ).
fof(f10475,plain,
! [X2,X0,X1] :
( arg1(sK2(X0,X1,X2),X1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10377]) ).
fof(f10491,plain,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
inference(cnf_transformation,[],[f9161]) ).
fof(f10565,plain,
! [X0,X1] :
( subr(sK22(X0,X1),sub_0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10391]) ).
fof(f10566,plain,
! [X0,X1] :
( arg2(sK22(X0,X1),X1)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10391]) ).
fof(f10567,plain,
! [X0,X1] :
( arg1(sK22(X0,X1),X0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10391]) ).
fof(f10631,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| val(sK32(X0,X2),X2) ),
inference(cnf_transformation,[],[f10400]) ).
fof(f10632,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| sub(sK32(X0,X2),name_1_1) ),
inference(cnf_transformation,[],[f10400]) ).
fof(f10635,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| attr(sK31(X0,X2),sK32(X0,X2)) ),
inference(cnf_transformation,[],[f10400]) ).
fof(f10636,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| in(sK33(X0,X2),sK31(X0,X2)) ),
inference(cnf_transformation,[],[f10400]) ).
fof(f10725,definition,
( spl43_1
<=> ! [X4,X9,X0,X8,X3,X2,X1] :
( ~ arg1(X3,X0)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(X3,rprs_0)
| ~ sub(X4,X9)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X8,X0)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4) ) ),
introduced(definition,[new_symbols(definition,[spl43_1])],[avatar_definition]) ).
fof(f10726,plain,
( ! [X2,X3,X0,X1,X8,X9,X4] :
( ~ val(X2,nelson_0)
| ~ arg1(X3,X0)
| ~ val(X1,mandela_0)
| ~ subr(X3,rprs_0)
| ~ sub(X4,X9)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X8,X0)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4) )
| ~ spl43_1 ),
inference(avatar_component_clause,[],[f10725]) ).
fof(f10728,definition,
( spl43_2
<=> ! [X6,X5,X7] :
( ~ in(X5,X6)
| ~ val(X7,s__374dafrika_0)
| ~ sub(X7,name_1_1)
| ~ attr(X6,X7) ) ),
introduced(definition,[new_symbols(definition,[spl43_2])],[avatar_definition]) ).
fof(f10729,plain,
( ! [X6,X7,X5] :
( ~ val(X7,s__374dafrika_0)
| ~ in(X5,X6)
| ~ sub(X7,name_1_1)
| ~ attr(X6,X7) )
| ~ spl43_2 ),
inference(avatar_component_clause,[],[f10728]) ).
fof(f10730,plain,
( spl43_1
| spl43_2 ),
inference(avatar_split_clause,[],[f10409,f10728,f10725]) ).
fof(f11018,plain,
! [X0] :
( val(sK32(X0,s__374dafrika_0),s__374dafrika_0)
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[],[f10631,f10491]) ).
fof(f11019,plain,
! [X0] :
( sub(sK32(X0,s__374dafrika_0),name_1_1)
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[],[f10632,f10491]) ).
fof(f11047,plain,
! [X0] :
( attr(sK31(X0,s__374dafrika_0),sK32(X0,s__374dafrika_0))
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[],[f10635,f10491]) ).
fof(f11072,plain,
! [X0] :
( in(sK33(X0,s__374dafrika_0),sK31(X0,s__374dafrika_0))
| ~ prop(X0,s__374dafrikanisch_1_1) ),
inference(resolution,[],[f10636,f10491]) ).
fof(f13123,plain,
( ! [X2,X0,X1] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| ~ in(X1,X2)
| ~ sub(sK32(X0,s__374dafrika_0),name_1_1)
| ~ attr(X2,sK32(X0,s__374dafrika_0)) )
| ~ spl43_2 ),
inference(resolution,[],[f11018,f10729]) ).
fof(f13124,plain,
( ! [X2,X0,X1] :
( ~ attr(X2,sK32(X0,s__374dafrika_0))
| ~ in(X1,X2)
| ~ prop(X0,s__374dafrikanisch_1_1) )
| ~ spl43_2 ),
inference(forward_subsumption_resolution,[],[f13123,f11019]) ).
fof(f13494,plain,
( ! [X0,X1] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| ~ in(X1,sK31(X0,s__374dafrika_0))
| ~ prop(X0,s__374dafrikanisch_1_1) )
| ~ spl43_2 ),
inference(resolution,[],[f11047,f13124]) ).
fof(f13495,plain,
( ! [X0,X1] :
( ~ in(X1,sK31(X0,s__374dafrika_0))
| ~ prop(X0,s__374dafrikanisch_1_1) )
| ~ spl43_2 ),
inference(duplicate_literal_removal,[],[f13494]) ).
fof(f13496,plain,
( ! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| ~ prop(X0,s__374dafrikanisch_1_1) )
| ~ spl43_2 ),
inference(resolution,[],[f11072,f13495]) ).
fof(f13501,plain,
( ! [X0] : ~ prop(X0,s__374dafrikanisch_1_1)
| ~ spl43_2 ),
inference(duplicate_literal_removal,[],[f13496]) ).
fof(f13502,plain,
( $false
| ~ spl43_2 ),
inference(resolution,[],[f13501,f10461]) ).
fof(f13503,plain,
~ spl43_2,
inference(avatar_contradiction_clause,[],[f13502]) ).
fof(f13504,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ arg1(X0,X1)
| ~ val(X2,mandela_0)
| ~ subr(X0,rprs_0)
| ~ sub(X3,X4)
| ~ sub(c6,eigenname_1_1)
| ~ sub(X2,familiename_1_1)
| ~ obj(X5,X1)
| ~ attr(X1,c6)
| ~ attr(X1,X2)
| ~ arg2(X0,X3) )
| ~ spl43_1 ),
inference(resolution,[],[f10726,f10437]) ).
fof(f13505,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ val(X2,mandela_0)
| ~ arg1(X0,X1)
| ~ subr(X0,rprs_0)
| ~ sub(X3,X4)
| ~ sub(X2,familiename_1_1)
| ~ obj(X5,X1)
| ~ attr(X1,c6)
| ~ attr(X1,X2)
| ~ arg2(X0,X3) )
| ~ spl43_1 ),
inference(forward_subsumption_resolution,[],[f13504,f10438]) ).
fof(f13506,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ arg1(X0,X1)
| ~ subr(X0,rprs_0)
| ~ sub(X2,X3)
| ~ sub(c7,familiename_1_1)
| ~ obj(X4,X1)
| ~ attr(X1,c6)
| ~ attr(X1,c7)
| ~ arg2(X0,X2) )
| ~ spl43_1 ),
inference(resolution,[],[f13505,f10435]) ).
fof(f13507,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ subr(X0,rprs_0)
| ~ arg1(X0,X1)
| ~ sub(X2,X3)
| ~ obj(X4,X1)
| ~ attr(X1,c6)
| ~ attr(X1,c7)
| ~ arg2(X0,X2) )
| ~ spl43_1 ),
inference(forward_subsumption_resolution,[],[f13506,f10436]) ).
fof(f13544,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ arg2(sK2(X0,X1,X2),X4)
| ~ sub(X4,X5)
| ~ obj(X6,X3)
| ~ attr(X3,c6)
| ~ attr(X3,c7)
| ~ arg1(sK2(X0,X1,X2),X3)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl43_1 ),
inference(resolution,[],[f13507,f10469]) ).
fof(f14274,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ sub(sK3(X0,X1,X2),X3)
| ~ obj(X4,X5)
| ~ attr(X5,c6)
| ~ attr(X5,c7)
| ~ arg1(sK2(X0,X1,X2),X5)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl43_1 ),
inference(resolution,[],[f13544,f10474]) ).
fof(f14275,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ arg1(sK2(X0,X1,X2),X5)
| ~ obj(X4,X5)
| ~ attr(X5,c6)
| ~ attr(X5,c7)
| ~ sub(sK3(X0,X1,X2),X3)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl43_1 ),
inference(duplicate_literal_removal,[],[f14274]) ).
fof(f14280,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ obj(X0,X1)
| ~ attr(X1,c6)
| ~ attr(X1,c7)
| ~ sub(sK3(X2,X1,X3),X4)
| ~ arg1(X2,X1)
| ~ arg2(X2,X3)
| ~ subr(X2,sub_0)
| ~ arg1(X2,X1)
| ~ arg2(X2,X3)
| ~ subr(X2,sub_0) )
| ~ spl43_1 ),
inference(resolution,[],[f14275,f10475]) ).
fof(f14281,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ sub(sK3(X2,X1,X3),X4)
| ~ attr(X1,c6)
| ~ attr(X1,c7)
| ~ obj(X0,X1)
| ~ arg1(X2,X1)
| ~ arg2(X2,X3)
| ~ subr(X2,sub_0) )
| ~ spl43_1 ),
inference(duplicate_literal_removal,[],[f14280]) ).
fof(f14286,plain,
( ! [X2,X3,X0,X1] :
( ~ attr(X0,c6)
| ~ attr(X0,c7)
| ~ obj(X1,X0)
| ~ arg1(X2,X0)
| ~ arg2(X2,X3)
| ~ subr(X2,sub_0)
| ~ arg1(X2,X0)
| ~ arg2(X2,X3)
| ~ subr(X2,sub_0) )
| ~ spl43_1 ),
inference(resolution,[],[f14281,f10470]) ).
fof(f14287,plain,
( ! [X2,X3,X0,X1] :
( ~ subr(X2,sub_0)
| ~ attr(X0,c7)
| ~ obj(X1,X0)
| ~ arg1(X2,X0)
| ~ arg2(X2,X3)
| ~ attr(X0,c6) )
| ~ spl43_1 ),
inference(duplicate_literal_removal,[],[f14286]) ).
fof(f14292,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ arg2(sK22(X2,X3),X4)
| ~ obj(X1,X0)
| ~ arg1(sK22(X2,X3),X0)
| ~ attr(X0,c7)
| ~ attr(X0,c6)
| ~ sub(X2,X3) )
| ~ spl43_1 ),
inference(resolution,[],[f14287,f10565]) ).
fof(f14301,plain,
( ! [X2,X3,X0,X1] :
( ~ obj(X0,X1)
| ~ arg1(sK22(X2,X3),X1)
| ~ attr(X1,c7)
| ~ attr(X1,c6)
| ~ sub(X2,X3)
| ~ sub(X2,X3) )
| ~ spl43_1 ),
inference(resolution,[],[f14292,f10566]) ).
fof(f14302,plain,
( ! [X2,X3,X0,X1] :
( ~ arg1(sK22(X2,X3),X1)
| ~ obj(X0,X1)
| ~ attr(X1,c7)
| ~ attr(X1,c6)
| ~ sub(X2,X3) )
| ~ spl43_1 ),
inference(duplicate_literal_removal,[],[f14301]) ).
fof(f14313,plain,
( ! [X2,X0,X1] :
( ~ obj(X0,X1)
| ~ attr(X1,c7)
| ~ attr(X1,c6)
| ~ sub(X1,X2)
| ~ sub(X1,X2) )
| ~ spl43_1 ),
inference(resolution,[],[f14302,f10567]) ).
fof(f14314,plain,
( ! [X2,X0,X1] :
( ~ attr(X1,c7)
| ~ obj(X0,X1)
| ~ attr(X1,c6)
| ~ sub(X1,X2) )
| ~ spl43_1 ),
inference(duplicate_literal_removal,[],[f14313]) ).
fof(f14321,plain,
( ! [X0,X1] :
( ~ obj(X0,c5)
| ~ attr(c5,c6)
| ~ sub(c5,X1) )
| ~ spl43_1 ),
inference(resolution,[],[f14314,f10440]) ).
fof(f14322,plain,
( ! [X0,X1] :
( ~ obj(X0,c5)
| ~ sub(c5,X1) )
| ~ spl43_1 ),
inference(forward_subsumption_resolution,[],[f14321,f10441]) ).
fof(f14324,definition,
( spl43_392
<=> ! [X1] : ~ sub(c5,X1) ),
introduced(definition,[new_symbols(definition,[spl43_392])],[avatar_definition]) ).
fof(f14325,plain,
( ! [X1] : ~ sub(c5,X1)
| ~ spl43_392 ),
inference(avatar_component_clause,[],[f14324]) ).
fof(f14327,definition,
( spl43_393
<=> ! [X0] : ~ obj(X0,c5) ),
introduced(definition,[new_symbols(definition,[spl43_393])],[avatar_definition]) ).
fof(f14328,plain,
( ! [X0] : ~ obj(X0,c5)
| ~ spl43_393 ),
inference(avatar_component_clause,[],[f14327]) ).
fof(f14329,plain,
( spl43_392
| spl43_393
| ~ spl43_1 ),
inference(avatar_split_clause,[],[f14322,f10725,f14327,f14324]) ).
fof(f14332,plain,
( $false
| ~ spl43_392 ),
inference(resolution,[],[f14325,f10439]) ).
fof(f14333,plain,
~ spl43_392,
inference(avatar_contradiction_clause,[],[f14332]) ).
fof(f14336,plain,
( ! [X0,X1] :
( ~ subr(X0,sub_0)
| ~ arg2(X0,X1)
| ~ arg1(X0,c5) )
| ~ spl43_393 ),
inference(resolution,[],[f14328,f10471]) ).
fof(f14415,plain,
( ! [X2,X0,X1] :
( ~ arg2(sK22(X0,X1),X2)
| ~ arg1(sK22(X0,X1),c5)
| ~ sub(X0,X1) )
| ~ spl43_393 ),
inference(resolution,[],[f14336,f10565]) ).
fof(f14519,plain,
( ! [X0,X1] :
( ~ arg1(sK22(X0,X1),c5)
| ~ sub(X0,X1)
| ~ sub(X0,X1) )
| ~ spl43_393 ),
inference(resolution,[],[f14415,f10566]) ).
fof(f14520,plain,
( ! [X0,X1] :
( ~ arg1(sK22(X0,X1),c5)
| ~ sub(X0,X1) )
| ~ spl43_393 ),
inference(duplicate_literal_removal,[],[f14519]) ).
fof(f14525,plain,
( ! [X0] :
( ~ sub(c5,X0)
| ~ sub(c5,X0) )
| ~ spl43_393 ),
inference(resolution,[],[f14520,f10567]) ).
fof(f14526,plain,
( ! [X0] : ~ sub(c5,X0)
| ~ spl43_393 ),
inference(duplicate_literal_removal,[],[f14525]) ).
fof(f14527,plain,
( spl43_392
| ~ spl43_393 ),
inference(avatar_split_clause,[],[f14526,f14327,f14324]) ).
cnf(s1,plain,
( spl43_1
| spl43_2 ),
inference(sat_conversion,[],[f10730]) ).
cnf(s199,plain,
~ spl43_2,
inference(sat_conversion,[],[f13503]) ).
cnf(s238,plain,
( ~ spl43_1
| spl43_392
| spl43_393 ),
inference(sat_conversion,[],[f14329]) ).
cnf(s239,plain,
~ spl43_392,
inference(sat_conversion,[],[f14333]) ).
cnf(s246,plain,
( spl43_392
| ~ spl43_393 ),
inference(sat_conversion,[],[f14527]) ).
cnf(s247,plain,
~ spl43_393,
inference(rat,[],[s246,s239]) ).
cnf(s248,plain,
~ spl43_1,
inference(rat,[],[s238,s247,s239]) ).
cnf(s249,plain,
$false,
inference(rat,[],[s1,s199,s248]) ).
fof(f14528,plain,
$false,
inference(avatar_sat_refutation,[],[s249]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+36 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.19 % Computer : n006.cluster.edu
% 0.06/0.19 % Model : x86_64 x86_64
% 0.06/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.19 % Memory : 8046.5625MB
% 0.06/0.19 % OS : Linux 6.8.0-71-generic
% 0.06/0.20 % CPULimit : 300
% 0.06/0.20 % WCLimit : 300
% 0.06/0.20 % DateTime : Mon Sep 28 23:29:11 UTC 2026
% 0.06/0.20 % CPUTime :
% 0.06/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.23 Running first-order theorem proving
% 0.06/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.97/1.51 % (311462)Detected formulas, will run a generic FOF schedule.
% 2.97/1.51 % (311467)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=4227749551:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 2.97/1.51 % (311469)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3627273970:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 2.97/1.51 % (311470)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3582962887:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 2.97/1.51 % (311468)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3613281919:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 2.97/1.51 % (311471)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1768522575:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 2.97/1.51 % (311472)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1224885471:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 2.97/1.51 % (311473)dis-21_1_sil=8000:lcm=predicate:random_seed=1131134036:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 2.97/1.51 % (311471)Refutation not found, incomplete strategy
% 2.97/1.51 % (311471)------------------------------
% 2.97/1.51 % (311471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.97/1.51 % (311471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.97/1.51 % (311471)CaDiCaL version: 2.1.3
% 2.97/1.51 % (311471)Termination reason: Refutation not found, incomplete strategy
% 2.97/1.51 % (311471)Time elapsed: 0.027 s
% 2.97/1.51 % (311471)Peak memory usage: 97 MB
% 2.97/1.51 % (311471)Instructions burned: 55 (million)
% 2.97/1.51 % (311470)Instruction limit reached!
% 2.97/1.51 % (311470)------------------------------
% 2.97/1.51 % (311470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.97/1.51 % (311470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.97/1.51 % (311470)CaDiCaL version: 2.1.3
% 2.97/1.51 % (311470)Termination reason: Instruction limit
% 2.97/1.51 % (311470)Termination phase: Saturation
% 2.97/1.51 % (311470)Time elapsed: 0.055 s
% 2.97/1.51 % (311470)Peak memory usage: 98 MB
% 2.97/1.51 % (311470)Instructions burned: 111 (million)
% 2.97/1.51 % (311473)Instruction limit reached!
% 2.97/1.51 % (311473)------------------------------
% 2.97/1.51 % (311473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.97/1.51 % (311473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.97/1.51 % (311472)Instruction limit reached!
% 2.97/1.51 % (311472)------------------------------
% 2.97/1.51 % (311472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.97/1.51 % (311472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.97/1.51 % (311473)CaDiCaL version: 2.1.3
% 2.97/1.51 % (311472)CaDiCaL version: 2.1.3
% 2.97/1.51 % (311473)Termination reason: Instruction limit
% 2.97/1.51 % (311473)Termination phase: Saturation
% 2.97/1.51 % (311473)Time elapsed: 0.065 s
% 2.97/1.51 % (311472)Termination reason: Instruction limit
% 2.97/1.51 % (311472)Termination phase: Saturation
% 2.97/1.51 % (311473)Peak memory usage: 98 MB
% 2.97/1.51 % (311472)Time elapsed: 0.065 s
% 2.97/1.51 % (311473)Instructions burned: 131 (million)
% 2.97/1.51 % (311472)Peak memory usage: 97 MB
% 2.97/1.51 % (311472)Instructions burned: 143 (million)
% 2.97/1.51 % (311481)lrs+10_1_sil=8000:sp=occurrence:random_seed=4052773250:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 2.97/1.51 % (311482)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3169077883:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 2.97/1.51 % (311483)lrs+1011_1_sil=32000:sp=occurrence:random_seed=936811297:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 2.97/1.51 % (311482)Refutation not found, incomplete strategy
% 2.97/1.51 % (311482)------------------------------
% 2.97/1.51 % (311482)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.97/1.51 % (311482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.97/1.51 % (311482)CaDiCaL version: 2.1.3
% 2.97/1.51 % (311482)Termination reason: Refutation not found, incomplete strategy
% 2.97/1.51 % (311482)Time elapsed: 0.039 s
% 2.97/1.51 % (311482)Peak memory usage: 98 MB
% 2.97/1.51 % (311482)Instructions burned: 88 (million)
% 2.97/1.51 % (311481)First to succeed.
% 2.97/1.51 % (311481)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-311462"
% 2.97/1.51 % (311483)Also succeeded, but the first one will report.
% 2.97/1.51 % (311471)------------------------------
% 2.97/1.51 % (311471)------------------------------
% 2.97/1.51 % (311487)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=138491486:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 2.97/1.51 % (311482)------------------------------
% 2.97/1.51 % (311482)------------------------------
% 2.97/1.51 % (311481)Refutation found. Thanks to Tanya!
% 2.97/1.51 % SZS status Theorem for theBenchmark
% 2.97/1.51 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/1.71 % (311481)------------------------------
% 0.18/1.71 % (311481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/1.71 % (311481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/1.71 % (311481)CaDiCaL version: 2.1.3
% 0.18/1.71 % (311481)Termination reason: Refutation
% 0.18/1.71 % (311481)Time elapsed: 0.098 s
% 0.18/1.71 % (311481)Peak memory usage: 102 MB
% 0.18/1.71 % (311481)Instructions burned: 167 (million)
% 0.18/1.71 % (311481)------------------------------
% 0.18/1.71 % (311481)------------------------------
% 0.18/1.71 % (311462)Success in time 0.836 s
% 0.18/1.71 % Vampire exiting
%------------------------------------------------------------------------------