%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR116+33 : 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.14s 0.82s
% Output : Refutation 2.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 17
% Syntax : Number of formulae : 116 ( 44 unt; 15 def)
% Number of atoms : 1623 ( 0 equ)
% Maximal formula atoms : 231 ( 13 avg)
% Number of connectives : 1709 ( 202 ~; 181 |;1311 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 231 ( 15 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 42 ( 41 usr; 16 prp; 0-3 aty)
% Number of functors : 60 ( 60 usr; 59 con; 0-2 aty)
% Number of variables : 86 ( 0 sgn 66 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
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)
& rslt(X8,X3)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X9)
& sub(X7,name_1_1)
& subr(X3,rprs_0)
& subs(X8,w__344hlen_1_2)
& 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_676) ).
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)
& rslt(X8,X3)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X9)
& sub(X7,name_1_1)
& subr(X3,rprs_0)
& subs(X8,w__344hlen_1_2)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X7,s__374dafrika_0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( attr(c13,c14)
& sub(c13,einrichtung_1_2)
& sub(c14,name_1_1)
& val(c14,anc_0)
& loc(c20,c54)
& preds(c20,c22)
& prop(c20,demokratisch__1_1)
& pmod(c22,erst_1_1,wahl_1_1)
& attr(c28,c29)
& sub(c28,land_1_1)
& sub(c29,name_1_1)
& val(c29,s__374dafrika_0)
& attr(c33,c34)
& attr(c33,c35)
& sub(c33,mensch_1_1)
& sub(c34,eigenname_1_1)
& val(c34,nelson_0)
& sub(c35,familiename_1_1)
& val(c35,mandela_0)
& sub(c38,pr__344sident_1_1)
& obj(c43,c33)
& rslt(c43,c55)
& subs(c43,w__344hlen_1_2)
& in(c54,c28)
& arg1(c55,c33)
& arg2(c55,c38)
& subr(c55,rprs_0)
& ante(c7,c43)
& circ(c7,c20)
& exp(c7,c13)
& subs(c7,gewinn_2_1)
& assoc(demokratisch__1_1,demokratie__1_1)
& sort(c13,d)
& sort(c13,io)
& card(c13,int1)
& etype(c13,int1)
& fact(c13,real)
& gener(c13,sp)
& quant(c13,one)
& refer(c13,det)
& varia(c13,con)
& sort(c14,na)
& card(c14,int1)
& etype(c14,int0)
& fact(c14,real)
& gener(c14,sp)
& quant(c14,one)
& refer(c14,indet)
& varia(c14,varia_c)
& sort(einrichtung_1_2,d)
& sort(einrichtung_1_2,io)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& quant(einrichtung_1_2,quant_c)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,varia_c)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(anc_0,fe)
& sort(c20,ad)
& card(c20,cons(x_constant,cons(int1,nil)))
& etype(c20,int1)
& fact(c20,real)
& gener(c20,sp)
& quant(c20,mult)
& refer(c20,det)
& varia(c20,con)
& sort(c54,l)
& card(c54,int1)
& etype(c54,int0)
& fact(c54,real)
& gener(c54,sp)
& quant(c54,one)
& refer(c54,det)
& varia(c54,con)
& sort(c22,ad)
& card(c22,int1)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,ge)
& quant(c22,one)
& refer(c22,refer_c)
& varia(c22,varia_c)
& sort(demokratisch__1_1,nq)
& sort(erst_1_1,oq)
& card(erst_1_1,int1)
& sort(wahl_1_1,ad)
& card(wahl_1_1,int1)
& etype(wahl_1_1,int0)
& fact(wahl_1_1,real)
& gener(wahl_1_1,ge)
& quant(wahl_1_1,one)
& refer(wahl_1_1,refer_c)
& varia(wahl_1_1,varia_c)
& 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(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(c33,d)
& card(c33,int1)
& etype(c33,int0)
& fact(c33,real)
& gener(c33,sp)
& quant(c33,one)
& refer(c33,det)
& varia(c33,con)
& sort(c34,na)
& card(c34,int1)
& etype(c34,int0)
& fact(c34,real)
& gener(c34,sp)
& quant(c34,one)
& refer(c34,indet)
& varia(c34,varia_c)
& sort(c35,na)
& card(c35,int1)
& etype(c35,int0)
& fact(c35,real)
& gener(c35,sp)
& quant(c35,one)
& refer(c35,indet)
& varia(c35,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(c38,d)
& card(c38,int1)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,sp)
& quant(c38,one)
& refer(c38,det)
& varia(c38,con)
& 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(c43,da)
& fact(c43,real)
& gener(c43,sp)
& sort(c55,st)
& fact(c55,real)
& gener(c55,sp)
& sort(w__344hlen_1_2,da)
& fact(w__344hlen_1_2,real)
& gener(w__344hlen_1_2,ge)
& sort(rprs_0,st)
& fact(rprs_0,real)
& gener(rprs_0,gener_c)
& sort(c7,ad)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,det)
& varia(c7,con)
& sort(gewinn_2_1,ad)
& card(gewinn_2_1,int1)
& etype(gewinn_2_1,int0)
& fact(gewinn_2_1,real)
& gener(gewinn_2_1,ge)
& quant(gewinn_2_1,one)
& refer(gewinn_2_1,refer_c)
& varia(gewinn_2_1,varia_c)
& sort(demokratie__1_1,io)
& card(demokratie__1_1,int1)
& etype(demokratie__1_1,int0)
& fact(demokratie__1_1,real)
& gener(demokratie__1_1,ge)
& quant(demokratie__1_1,one)
& refer(demokratie__1_1,refer_c)
& varia(demokratie__1_1,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_wp_676) ).
fof(f10191,plain,
( attr(c13,c14)
& sub(c13,einrichtung_1_2)
& sub(c14,name_1_1)
& val(c14,anc_0)
& loc(c20,c54)
& preds(c20,c22)
& prop(c20,demokratisch__1_1)
& pmod(c22,erst_1_1,wahl_1_1)
& attr(c28,c29)
& sub(c28,land_1_1)
& sub(c29,name_1_1)
& val(c29,s__374dafrika_0)
& attr(c33,c34)
& attr(c33,c35)
& sub(c33,mensch_1_1)
& sub(c34,eigenname_1_1)
& val(c34,nelson_0)
& sub(c35,familiename_1_1)
& val(c35,mandela_0)
& sub(c38,pr__344sident_1_1)
& obj(c43,c33)
& rslt(c43,c55)
& subs(c43,w__344hlen_1_2)
& in(c54,c28)
& arg1(c55,c33)
& arg2(c55,c38)
& subr(c55,rprs_0)
& circ(c7,c20)
& exp(c7,c13)
& subs(c7,gewinn_2_1)
& assoc(demokratisch__1_1,demokratie__1_1)
& sort(c13,d)
& sort(c13,io)
& card(c13,int1)
& etype(c13,int1)
& fact(c13,real)
& gener(c13,sp)
& quant(c13,one)
& refer(c13,det)
& varia(c13,con)
& sort(c14,na)
& card(c14,int1)
& etype(c14,int0)
& fact(c14,real)
& gener(c14,sp)
& quant(c14,one)
& refer(c14,indet)
& varia(c14,varia_c)
& sort(einrichtung_1_2,d)
& sort(einrichtung_1_2,io)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& quant(einrichtung_1_2,quant_c)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,varia_c)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(anc_0,fe)
& sort(c20,ad)
& card(c20,cons(x_constant,cons(int1,nil)))
& etype(c20,int1)
& fact(c20,real)
& gener(c20,sp)
& quant(c20,mult)
& refer(c20,det)
& varia(c20,con)
& sort(c54,l)
& card(c54,int1)
& etype(c54,int0)
& fact(c54,real)
& gener(c54,sp)
& quant(c54,one)
& refer(c54,det)
& varia(c54,con)
& sort(c22,ad)
& card(c22,int1)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,ge)
& quant(c22,one)
& refer(c22,refer_c)
& varia(c22,varia_c)
& sort(demokratisch__1_1,nq)
& sort(erst_1_1,oq)
& card(erst_1_1,int1)
& sort(wahl_1_1,ad)
& card(wahl_1_1,int1)
& etype(wahl_1_1,int0)
& fact(wahl_1_1,real)
& gener(wahl_1_1,ge)
& quant(wahl_1_1,one)
& refer(wahl_1_1,refer_c)
& varia(wahl_1_1,varia_c)
& 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(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(c33,d)
& card(c33,int1)
& etype(c33,int0)
& fact(c33,real)
& gener(c33,sp)
& quant(c33,one)
& refer(c33,det)
& varia(c33,con)
& sort(c34,na)
& card(c34,int1)
& etype(c34,int0)
& fact(c34,real)
& gener(c34,sp)
& quant(c34,one)
& refer(c34,indet)
& varia(c34,varia_c)
& sort(c35,na)
& card(c35,int1)
& etype(c35,int0)
& fact(c35,real)
& gener(c35,sp)
& quant(c35,one)
& refer(c35,indet)
& varia(c35,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(c38,d)
& card(c38,int1)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,sp)
& quant(c38,one)
& refer(c38,det)
& varia(c38,con)
& 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(c43,da)
& fact(c43,real)
& gener(c43,sp)
& sort(c55,st)
& fact(c55,real)
& gener(c55,sp)
& sort(w__344hlen_1_2,da)
& fact(w__344hlen_1_2,real)
& gener(w__344hlen_1_2,ge)
& sort(rprs_0,st)
& fact(rprs_0,real)
& gener(rprs_0,gener_c)
& sort(c7,ad)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,det)
& varia(c7,con)
& sort(gewinn_2_1,ad)
& card(gewinn_2_1,int1)
& etype(gewinn_2_1,int0)
& fact(gewinn_2_1,real)
& gener(gewinn_2_1,ge)
& quant(gewinn_2_1,one)
& refer(gewinn_2_1,refer_c)
& varia(gewinn_2_1,varia_c)
& sort(demokratie__1_1,io)
& card(demokratie__1_1,int1)
& etype(demokratie__1_1,int0)
& fact(demokratie__1_1,real)
& gener(demokratie__1_1,ge)
& quant(demokratie__1_1,one)
& refer(demokratie__1_1,refer_c)
& varia(demokratie__1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10207,plain,
( attr(c13,c14)
& sub(c13,einrichtung_1_2)
& sub(c14,name_1_1)
& val(c14,anc_0)
& loc(c20,c54)
& preds(c20,c22)
& prop(c20,demokratisch__1_1)
& pmod(c22,erst_1_1,wahl_1_1)
& attr(c28,c29)
& sub(c28,land_1_1)
& sub(c29,name_1_1)
& val(c29,s__374dafrika_0)
& attr(c33,c34)
& attr(c33,c35)
& sub(c33,mensch_1_1)
& sub(c34,eigenname_1_1)
& val(c34,nelson_0)
& sub(c35,familiename_1_1)
& val(c35,mandela_0)
& sub(c38,pr__344sident_1_1)
& obj(c43,c33)
& rslt(c43,c55)
& subs(c43,w__344hlen_1_2)
& in(c54,c28)
& arg1(c55,c33)
& arg2(c55,c38)
& subr(c55,rprs_0)
& circ(c7,c20)
& exp(c7,c13)
& subs(c7,gewinn_2_1)
& assoc(demokratisch__1_1,demokratie__1_1)
& card(c13,int1)
& etype(c13,int1)
& fact(c13,real)
& gener(c13,sp)
& quant(c13,one)
& refer(c13,det)
& varia(c13,con)
& card(c14,int1)
& etype(c14,int0)
& fact(c14,real)
& gener(c14,sp)
& quant(c14,one)
& refer(c14,indet)
& varia(c14,varia_c)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& quant(einrichtung_1_2,quant_c)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,varia_c)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& card(c20,cons(x_constant,cons(int1,nil)))
& etype(c20,int1)
& fact(c20,real)
& gener(c20,sp)
& quant(c20,mult)
& refer(c20,det)
& varia(c20,con)
& card(c54,int1)
& etype(c54,int0)
& fact(c54,real)
& gener(c54,sp)
& quant(c54,one)
& refer(c54,det)
& varia(c54,con)
& card(c22,int1)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,ge)
& quant(c22,one)
& refer(c22,refer_c)
& varia(c22,varia_c)
& card(erst_1_1,int1)
& card(wahl_1_1,int1)
& etype(wahl_1_1,int0)
& fact(wahl_1_1,real)
& gener(wahl_1_1,ge)
& quant(wahl_1_1,one)
& refer(wahl_1_1,refer_c)
& varia(wahl_1_1,varia_c)
& card(c28,int1)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& quant(c28,one)
& refer(c28,det)
& varia(c28,con)
& card(c29,int1)
& etype(c29,int0)
& fact(c29,real)
& gener(c29,sp)
& quant(c29,one)
& refer(c29,indet)
& varia(c29,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(c33,int1)
& etype(c33,int0)
& fact(c33,real)
& gener(c33,sp)
& quant(c33,one)
& refer(c33,det)
& varia(c33,con)
& card(c34,int1)
& etype(c34,int0)
& fact(c34,real)
& gener(c34,sp)
& quant(c34,one)
& refer(c34,indet)
& varia(c34,varia_c)
& card(c35,int1)
& etype(c35,int0)
& fact(c35,real)
& gener(c35,sp)
& quant(c35,one)
& refer(c35,indet)
& varia(c35,varia_c)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& card(c38,int1)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,sp)
& quant(c38,one)
& refer(c38,det)
& varia(c38,con)
& 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(c43,real)
& gener(c43,sp)
& fact(c55,real)
& gener(c55,sp)
& fact(w__344hlen_1_2,real)
& gener(w__344hlen_1_2,ge)
& fact(rprs_0,real)
& gener(rprs_0,gener_c)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,det)
& varia(c7,con)
& card(gewinn_2_1,int1)
& etype(gewinn_2_1,int0)
& fact(gewinn_2_1,real)
& gener(gewinn_2_1,ge)
& quant(gewinn_2_1,one)
& refer(gewinn_2_1,refer_c)
& varia(gewinn_2_1,varia_c)
& card(demokratie__1_1,int1)
& etype(demokratie__1_1,int0)
& fact(demokratie__1_1,real)
& gener(demokratie__1_1,ge)
& quant(demokratie__1_1,one)
& refer(demokratie__1_1,refer_c)
& varia(demokratie__1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10210,plain,
( attr(c13,c14)
& sub(c13,einrichtung_1_2)
& sub(c14,name_1_1)
& val(c14,anc_0)
& loc(c20,c54)
& preds(c20,c22)
& prop(c20,demokratisch__1_1)
& pmod(c22,erst_1_1,wahl_1_1)
& attr(c28,c29)
& sub(c28,land_1_1)
& sub(c29,name_1_1)
& val(c29,s__374dafrika_0)
& attr(c33,c34)
& attr(c33,c35)
& sub(c33,mensch_1_1)
& sub(c34,eigenname_1_1)
& val(c34,nelson_0)
& sub(c35,familiename_1_1)
& val(c35,mandela_0)
& sub(c38,pr__344sident_1_1)
& obj(c43,c33)
& rslt(c43,c55)
& subs(c43,w__344hlen_1_2)
& in(c54,c28)
& arg1(c55,c33)
& arg2(c55,c38)
& subr(c55,rprs_0)
& circ(c7,c20)
& exp(c7,c13)
& subs(c7,gewinn_2_1)
& assoc(demokratisch__1_1,demokratie__1_1)
& card(c13,int1)
& etype(c13,int1)
& fact(c13,real)
& gener(c13,sp)
& refer(c13,det)
& varia(c13,con)
& card(c14,int1)
& etype(c14,int0)
& fact(c14,real)
& gener(c14,sp)
& refer(c14,indet)
& varia(c14,varia_c)
& card(einrichtung_1_2,card_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,varia_c)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& card(c20,cons(x_constant,cons(int1,nil)))
& etype(c20,int1)
& fact(c20,real)
& gener(c20,sp)
& refer(c20,det)
& varia(c20,con)
& card(c54,int1)
& etype(c54,int0)
& fact(c54,real)
& gener(c54,sp)
& refer(c54,det)
& varia(c54,con)
& card(c22,int1)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,ge)
& refer(c22,refer_c)
& varia(c22,varia_c)
& card(erst_1_1,int1)
& card(wahl_1_1,int1)
& etype(wahl_1_1,int0)
& fact(wahl_1_1,real)
& gener(wahl_1_1,ge)
& refer(wahl_1_1,refer_c)
& varia(wahl_1_1,varia_c)
& card(c28,int1)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& refer(c28,det)
& varia(c28,con)
& card(c29,int1)
& etype(c29,int0)
& fact(c29,real)
& gener(c29,sp)
& refer(c29,indet)
& varia(c29,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(c33,int1)
& etype(c33,int0)
& fact(c33,real)
& gener(c33,sp)
& refer(c33,det)
& varia(c33,con)
& card(c34,int1)
& etype(c34,int0)
& fact(c34,real)
& gener(c34,sp)
& refer(c34,indet)
& varia(c34,varia_c)
& card(c35,int1)
& etype(c35,int0)
& fact(c35,real)
& gener(c35,sp)
& refer(c35,indet)
& varia(c35,varia_c)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& card(c38,int1)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,sp)
& refer(c38,det)
& varia(c38,con)
& 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(c43,real)
& gener(c43,sp)
& fact(c55,real)
& gener(c55,sp)
& fact(w__344hlen_1_2,real)
& gener(w__344hlen_1_2,ge)
& fact(rprs_0,real)
& gener(rprs_0,gener_c)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& refer(c7,det)
& varia(c7,con)
& card(gewinn_2_1,int1)
& etype(gewinn_2_1,int0)
& fact(gewinn_2_1,real)
& gener(gewinn_2_1,ge)
& refer(gewinn_2_1,refer_c)
& varia(gewinn_2_1,varia_c)
& card(demokratie__1_1,int1)
& etype(demokratie__1_1,int0)
& fact(demokratie__1_1,real)
& gener(demokratie__1_1,ge)
& refer(demokratie__1_1,refer_c)
& varia(demokratie__1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10207]) ).
fof(f10213,plain,
( attr(c13,c14)
& sub(c13,einrichtung_1_2)
& sub(c14,name_1_1)
& val(c14,anc_0)
& loc(c20,c54)
& preds(c20,c22)
& prop(c20,demokratisch__1_1)
& pmod(c22,erst_1_1,wahl_1_1)
& attr(c28,c29)
& sub(c28,land_1_1)
& sub(c29,name_1_1)
& val(c29,s__374dafrika_0)
& attr(c33,c34)
& attr(c33,c35)
& sub(c33,mensch_1_1)
& sub(c34,eigenname_1_1)
& val(c34,nelson_0)
& sub(c35,familiename_1_1)
& val(c35,mandela_0)
& sub(c38,pr__344sident_1_1)
& obj(c43,c33)
& rslt(c43,c55)
& subs(c43,w__344hlen_1_2)
& in(c54,c28)
& arg1(c55,c33)
& arg2(c55,c38)
& subr(c55,rprs_0)
& circ(c7,c20)
& exp(c7,c13)
& subs(c7,gewinn_2_1)
& assoc(demokratisch__1_1,demokratie__1_1)
& etype(c13,int1)
& fact(c13,real)
& gener(c13,sp)
& refer(c13,det)
& varia(c13,con)
& etype(c14,int0)
& fact(c14,real)
& gener(c14,sp)
& refer(c14,indet)
& varia(c14,varia_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& refer(einrichtung_1_2,refer_c)
& varia(einrichtung_1_2,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& etype(c20,int1)
& fact(c20,real)
& gener(c20,sp)
& refer(c20,det)
& varia(c20,con)
& etype(c54,int0)
& fact(c54,real)
& gener(c54,sp)
& refer(c54,det)
& varia(c54,con)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,ge)
& refer(c22,refer_c)
& varia(c22,varia_c)
& etype(wahl_1_1,int0)
& fact(wahl_1_1,real)
& gener(wahl_1_1,ge)
& refer(wahl_1_1,refer_c)
& varia(wahl_1_1,varia_c)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& refer(c28,det)
& varia(c28,con)
& etype(c29,int0)
& fact(c29,real)
& gener(c29,sp)
& refer(c29,indet)
& varia(c29,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(c33,int0)
& fact(c33,real)
& gener(c33,sp)
& refer(c33,det)
& varia(c33,con)
& etype(c34,int0)
& fact(c34,real)
& gener(c34,sp)
& refer(c34,indet)
& varia(c34,varia_c)
& etype(c35,int0)
& fact(c35,real)
& gener(c35,sp)
& refer(c35,indet)
& varia(c35,varia_c)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,sp)
& refer(c38,det)
& varia(c38,con)
& 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(c43,real)
& gener(c43,sp)
& fact(c55,real)
& gener(c55,sp)
& fact(w__344hlen_1_2,real)
& gener(w__344hlen_1_2,ge)
& fact(rprs_0,real)
& gener(rprs_0,gener_c)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& refer(c7,det)
& varia(c7,con)
& etype(gewinn_2_1,int0)
& fact(gewinn_2_1,real)
& gener(gewinn_2_1,ge)
& refer(gewinn_2_1,refer_c)
& varia(gewinn_2_1,varia_c)
& etype(demokratie__1_1,int0)
& fact(demokratie__1_1,real)
& gener(demokratie__1_1,ge)
& refer(demokratie__1_1,refer_c)
& varia(demokratie__1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10210]) ).
fof(f10216,plain,
( attr(c13,c14)
& sub(c13,einrichtung_1_2)
& sub(c14,name_1_1)
& val(c14,anc_0)
& loc(c20,c54)
& preds(c20,c22)
& prop(c20,demokratisch__1_1)
& pmod(c22,erst_1_1,wahl_1_1)
& attr(c28,c29)
& sub(c28,land_1_1)
& sub(c29,name_1_1)
& val(c29,s__374dafrika_0)
& attr(c33,c34)
& attr(c33,c35)
& sub(c33,mensch_1_1)
& sub(c34,eigenname_1_1)
& val(c34,nelson_0)
& sub(c35,familiename_1_1)
& val(c35,mandela_0)
& sub(c38,pr__344sident_1_1)
& obj(c43,c33)
& rslt(c43,c55)
& subs(c43,w__344hlen_1_2)
& in(c54,c28)
& arg1(c55,c33)
& arg2(c55,c38)
& subr(c55,rprs_0)
& circ(c7,c20)
& exp(c7,c13)
& subs(c7,gewinn_2_1)
& assoc(demokratisch__1_1,demokratie__1_1)
& etype(c13,int1)
& fact(c13,real)
& gener(c13,sp)
& varia(c13,con)
& etype(c14,int0)
& fact(c14,real)
& gener(c14,sp)
& varia(c14,varia_c)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& varia(einrichtung_1_2,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& varia(name_1_1,varia_c)
& etype(c20,int1)
& fact(c20,real)
& gener(c20,sp)
& varia(c20,con)
& etype(c54,int0)
& fact(c54,real)
& gener(c54,sp)
& varia(c54,con)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,ge)
& varia(c22,varia_c)
& etype(wahl_1_1,int0)
& fact(wahl_1_1,real)
& gener(wahl_1_1,ge)
& varia(wahl_1_1,varia_c)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& varia(c28,con)
& etype(c29,int0)
& fact(c29,real)
& gener(c29,sp)
& varia(c29,varia_c)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& varia(land_1_1,varia_c)
& etype(c33,int0)
& fact(c33,real)
& gener(c33,sp)
& varia(c33,con)
& etype(c34,int0)
& fact(c34,real)
& gener(c34,sp)
& varia(c34,varia_c)
& etype(c35,int0)
& fact(c35,real)
& gener(c35,sp)
& varia(c35,varia_c)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& varia(mensch_1_1,varia_c)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& varia(eigenname_1_1,varia_c)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& varia(familiename_1_1,varia_c)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,sp)
& varia(c38,con)
& 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(c43,real)
& gener(c43,sp)
& fact(c55,real)
& gener(c55,sp)
& fact(w__344hlen_1_2,real)
& gener(w__344hlen_1_2,ge)
& fact(rprs_0,real)
& gener(rprs_0,gener_c)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& varia(c7,con)
& etype(gewinn_2_1,int0)
& fact(gewinn_2_1,real)
& gener(gewinn_2_1,ge)
& varia(gewinn_2_1,varia_c)
& etype(demokratie__1_1,int0)
& fact(demokratie__1_1,real)
& gener(demokratie__1_1,ge)
& varia(demokratie__1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10213]) ).
fof(f10221,plain,
( attr(c13,c14)
& sub(c13,einrichtung_1_2)
& sub(c14,name_1_1)
& val(c14,anc_0)
& loc(c20,c54)
& preds(c20,c22)
& prop(c20,demokratisch__1_1)
& pmod(c22,erst_1_1,wahl_1_1)
& attr(c28,c29)
& sub(c28,land_1_1)
& sub(c29,name_1_1)
& val(c29,s__374dafrika_0)
& attr(c33,c34)
& attr(c33,c35)
& sub(c33,mensch_1_1)
& sub(c34,eigenname_1_1)
& val(c34,nelson_0)
& sub(c35,familiename_1_1)
& val(c35,mandela_0)
& sub(c38,pr__344sident_1_1)
& obj(c43,c33)
& rslt(c43,c55)
& subs(c43,w__344hlen_1_2)
& in(c54,c28)
& arg1(c55,c33)
& arg2(c55,c38)
& subr(c55,rprs_0)
& circ(c7,c20)
& exp(c7,c13)
& subs(c7,gewinn_2_1)
& assoc(demokratisch__1_1,demokratie__1_1)
& etype(c13,int1)
& fact(c13,real)
& gener(c13,sp)
& etype(c14,int0)
& fact(c14,real)
& gener(c14,sp)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& gener(einrichtung_1_2,ge)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& etype(c20,int1)
& fact(c20,real)
& gener(c20,sp)
& etype(c54,int0)
& fact(c54,real)
& gener(c54,sp)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,ge)
& etype(wahl_1_1,int0)
& fact(wahl_1_1,real)
& gener(wahl_1_1,ge)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& etype(c29,int0)
& fact(c29,real)
& gener(c29,sp)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& etype(c33,int0)
& fact(c33,real)
& gener(c33,sp)
& etype(c34,int0)
& fact(c34,real)
& gener(c34,sp)
& etype(c35,int0)
& fact(c35,real)
& gener(c35,sp)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,sp)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& fact(c43,real)
& gener(c43,sp)
& fact(c55,real)
& gener(c55,sp)
& fact(w__344hlen_1_2,real)
& gener(w__344hlen_1_2,ge)
& fact(rprs_0,real)
& gener(rprs_0,gener_c)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& etype(gewinn_2_1,int0)
& fact(gewinn_2_1,real)
& gener(gewinn_2_1,ge)
& etype(demokratie__1_1,int0)
& fact(demokratie__1_1,real)
& gener(demokratie__1_1,ge) ),
inference(pure_predicate_removal,[],[f10216]) ).
fof(f10226,plain,
( attr(c13,c14)
& sub(c13,einrichtung_1_2)
& sub(c14,name_1_1)
& val(c14,anc_0)
& loc(c20,c54)
& preds(c20,c22)
& prop(c20,demokratisch__1_1)
& pmod(c22,erst_1_1,wahl_1_1)
& attr(c28,c29)
& sub(c28,land_1_1)
& sub(c29,name_1_1)
& val(c29,s__374dafrika_0)
& attr(c33,c34)
& attr(c33,c35)
& sub(c33,mensch_1_1)
& sub(c34,eigenname_1_1)
& val(c34,nelson_0)
& sub(c35,familiename_1_1)
& val(c35,mandela_0)
& sub(c38,pr__344sident_1_1)
& obj(c43,c33)
& rslt(c43,c55)
& subs(c43,w__344hlen_1_2)
& in(c54,c28)
& arg1(c55,c33)
& arg2(c55,c38)
& subr(c55,rprs_0)
& circ(c7,c20)
& exp(c7,c13)
& subs(c7,gewinn_2_1)
& assoc(demokratisch__1_1,demokratie__1_1)
& etype(c13,int1)
& fact(c13,real)
& etype(c14,int0)
& fact(c14,real)
& etype(einrichtung_1_2,int1)
& fact(einrichtung_1_2,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& etype(c20,int1)
& fact(c20,real)
& etype(c54,int0)
& fact(c54,real)
& etype(c22,int0)
& fact(c22,real)
& etype(wahl_1_1,int0)
& fact(wahl_1_1,real)
& etype(c28,int0)
& fact(c28,real)
& etype(c29,int0)
& fact(c29,real)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& etype(c33,int0)
& fact(c33,real)
& etype(c34,int0)
& fact(c34,real)
& etype(c35,int0)
& fact(c35,real)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& etype(c38,int0)
& fact(c38,real)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& fact(c43,real)
& fact(c55,real)
& fact(w__344hlen_1_2,real)
& fact(rprs_0,real)
& etype(c7,int0)
& fact(c7,real)
& etype(gewinn_2_1,int0)
& fact(gewinn_2_1,real)
& etype(demokratie__1_1,int0)
& fact(demokratie__1_1,real) ),
inference(pure_predicate_removal,[],[f10221]) ).
fof(f10229,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)
| ~ rslt(X8,X3)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X9)
| ~ sub(X7,name_1_1)
| ~ subr(X3,rprs_0)
| ~ subs(X8,w__344hlen_1_2)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ val(X7,s__374dafrika_0) ),
inference(ennf_transformation,[],[f10189]) ).
fof(f10442,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)
| ~ rslt(X8,X3)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X9)
| ~ sub(X7,name_1_1)
| ~ subr(X3,rprs_0)
| ~ subs(X8,w__344hlen_1_2)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ val(X7,s__374dafrika_0) ),
inference(cnf_transformation,[],[f10229]) ).
fof(f10495,plain,
subr(c55,rprs_0),
inference(cnf_transformation,[],[f10226]) ).
fof(f10496,plain,
arg2(c55,c38),
inference(cnf_transformation,[],[f10226]) ).
fof(f10497,plain,
arg1(c55,c33),
inference(cnf_transformation,[],[f10226]) ).
fof(f10498,plain,
in(c54,c28),
inference(cnf_transformation,[],[f10226]) ).
fof(f10499,plain,
subs(c43,w__344hlen_1_2),
inference(cnf_transformation,[],[f10226]) ).
fof(f10500,plain,
rslt(c43,c55),
inference(cnf_transformation,[],[f10226]) ).
fof(f10501,plain,
obj(c43,c33),
inference(cnf_transformation,[],[f10226]) ).
fof(f10502,plain,
sub(c38,pr__344sident_1_1),
inference(cnf_transformation,[],[f10226]) ).
fof(f10503,plain,
val(c35,mandela_0),
inference(cnf_transformation,[],[f10226]) ).
fof(f10504,plain,
sub(c35,familiename_1_1),
inference(cnf_transformation,[],[f10226]) ).
fof(f10505,plain,
val(c34,nelson_0),
inference(cnf_transformation,[],[f10226]) ).
fof(f10506,plain,
sub(c34,eigenname_1_1),
inference(cnf_transformation,[],[f10226]) ).
fof(f10508,plain,
attr(c33,c35),
inference(cnf_transformation,[],[f10226]) ).
fof(f10509,plain,
attr(c33,c34),
inference(cnf_transformation,[],[f10226]) ).
fof(f10510,plain,
val(c29,s__374dafrika_0),
inference(cnf_transformation,[],[f10226]) ).
fof(f10511,plain,
sub(c29,name_1_1),
inference(cnf_transformation,[],[f10226]) ).
fof(f10513,plain,
attr(c28,c29),
inference(cnf_transformation,[],[f10226]) ).
fof(f10864,definition,
( spl52_1
<=> ! [X4,X9,X0,X8,X3,X2,X1] :
( ~ arg1(X3,X0)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ subs(X8,w__344hlen_1_2)
| ~ subr(X3,rprs_0)
| ~ sub(X4,X9)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ rslt(X8,X3)
| ~ obj(X8,X0)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4) ) ),
introduced(definition,[new_symbols(definition,[spl52_1])],[avatar_definition]) ).
fof(f10865,plain,
( ! [X2,X3,X0,X1,X8,X9,X4] :
( ~ rslt(X8,X3)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ subs(X8,w__344hlen_1_2)
| ~ subr(X3,rprs_0)
| ~ sub(X4,X9)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ arg1(X3,X0)
| ~ obj(X8,X0)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4) )
| ~ spl52_1 ),
inference(avatar_component_clause,[],[f10864]) ).
fof(f10867,definition,
( spl52_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,[spl52_2])],[avatar_definition]) ).
fof(f10868,plain,
( ! [X6,X7,X5] :
( ~ in(X5,X6)
| ~ val(X7,s__374dafrika_0)
| ~ sub(X7,name_1_1)
| ~ attr(X6,X7) )
| ~ spl52_2 ),
inference(avatar_component_clause,[],[f10867]) ).
fof(f10869,plain,
( spl52_1
| spl52_2 ),
inference(avatar_split_clause,[],[f10442,f10867,f10864]) ).
fof(f10870,plain,
( ! [X0] :
( ~ val(X0,s__374dafrika_0)
| ~ sub(X0,name_1_1)
| ~ attr(c28,X0) )
| ~ spl52_2 ),
inference(resolution,[],[f10498,f10868]) ).
fof(f10871,plain,
( ~ sub(c29,name_1_1)
| ~ attr(c28,c29)
| ~ spl52_2 ),
inference(resolution,[],[f10510,f10870]) ).
fof(f10873,definition,
( spl52_3
<=> attr(c28,c29) ),
introduced(definition,[new_symbols(definition,[spl52_3])],[avatar_definition]) ).
fof(f10874,plain,
( ~ attr(c28,c29)
| spl52_3 ),
inference(avatar_component_clause,[],[f10873]) ).
fof(f10876,definition,
( spl52_4
<=> sub(c29,name_1_1) ),
introduced(definition,[new_symbols(definition,[spl52_4])],[avatar_definition]) ).
fof(f10877,plain,
( ~ sub(c29,name_1_1)
| spl52_4 ),
inference(avatar_component_clause,[],[f10876]) ).
fof(f10878,plain,
( ~ spl52_3
| ~ spl52_4
| ~ spl52_2 ),
inference(avatar_split_clause,[],[f10871,f10867,f10876,f10873]) ).
fof(f10879,plain,
( $false
| spl52_3 ),
inference(resolution,[],[f10513,f10874]) ).
fof(f10880,plain,
spl52_3,
inference(avatar_contradiction_clause,[],[f10879]) ).
fof(f10881,plain,
( $false
| spl52_4 ),
inference(resolution,[],[f10877,f10511]) ).
fof(f10882,plain,
spl52_4,
inference(avatar_contradiction_clause,[],[f10881]) ).
fof(f10883,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ val(X0,nelson_0)
| ~ val(X1,mandela_0)
| ~ subs(c43,w__344hlen_1_2)
| ~ subr(c55,rprs_0)
| ~ sub(X2,X3)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ arg1(c55,X4)
| ~ obj(c43,X4)
| ~ attr(X4,X0)
| ~ attr(X4,X1)
| ~ arg2(c55,X2) )
| ~ spl52_1 ),
inference(resolution,[],[f10865,f10500]) ).
fof(f10885,definition,
( spl52_5
<=> ! [X2,X3] :
( ~ sub(X2,X3)
| ~ arg2(c55,X2) ) ),
introduced(definition,[new_symbols(definition,[spl52_5])],[avatar_definition]) ).
fof(f10886,plain,
( ! [X2,X3] :
( ~ arg2(c55,X2)
| ~ sub(X2,X3) )
| ~ spl52_5 ),
inference(avatar_component_clause,[],[f10885]) ).
fof(f10888,definition,
( spl52_6
<=> subr(c55,rprs_0) ),
introduced(definition,[new_symbols(definition,[spl52_6])],[avatar_definition]) ).
fof(f10889,plain,
( ~ subr(c55,rprs_0)
| spl52_6 ),
inference(avatar_component_clause,[],[f10888]) ).
fof(f10891,definition,
( spl52_7
<=> subs(c43,w__344hlen_1_2) ),
introduced(definition,[new_symbols(definition,[spl52_7])],[avatar_definition]) ).
fof(f10892,plain,
( ~ subs(c43,w__344hlen_1_2)
| spl52_7 ),
inference(avatar_component_clause,[],[f10891]) ).
fof(f10894,definition,
( spl52_8
<=> ! [X4,X0,X1] :
( ~ val(X0,nelson_0)
| ~ attr(X4,X1)
| ~ arg1(c55,X4)
| ~ attr(X4,X0)
| ~ obj(c43,X4)
| ~ sub(X0,eigenname_1_1)
| ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1) ) ),
introduced(definition,[new_symbols(definition,[spl52_8])],[avatar_definition]) ).
fof(f10895,plain,
( ! [X0,X1,X4] :
( ~ val(X0,nelson_0)
| ~ val(X1,mandela_0)
| ~ arg1(c55,X4)
| ~ attr(X4,X0)
| ~ obj(c43,X4)
| ~ sub(X0,eigenname_1_1)
| ~ attr(X4,X1)
| ~ sub(X1,familiename_1_1) )
| ~ spl52_8 ),
inference(avatar_component_clause,[],[f10894]) ).
fof(f10896,plain,
( spl52_5
| ~ spl52_6
| ~ spl52_7
| spl52_8
| ~ spl52_1 ),
inference(avatar_split_clause,[],[f10883,f10864,f10894,f10891,f10888,f10885]) ).
fof(f10897,plain,
( $false
| spl52_6 ),
inference(resolution,[],[f10889,f10495]) ).
fof(f10898,plain,
spl52_6,
inference(avatar_contradiction_clause,[],[f10897]) ).
fof(f10899,plain,
( $false
| spl52_7 ),
inference(resolution,[],[f10892,f10499]) ).
fof(f10900,plain,
spl52_7,
inference(avatar_contradiction_clause,[],[f10899]) ).
fof(f10904,definition,
( spl52_9
<=> sub(c35,familiename_1_1) ),
introduced(definition,[new_symbols(definition,[spl52_9])],[avatar_definition]) ).
fof(f10905,plain,
( ~ sub(c35,familiename_1_1)
| spl52_9 ),
inference(avatar_component_clause,[],[f10904]) ).
fof(f10907,definition,
( spl52_10
<=> ! [X0,X1] :
( ~ val(X0,nelson_0)
| ~ attr(X1,c35)
| ~ sub(X0,eigenname_1_1)
| ~ obj(c43,X1)
| ~ arg1(c55,X1)
| ~ attr(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_10])],[avatar_definition]) ).
fof(f10908,plain,
( ! [X0,X1] :
( ~ val(X0,nelson_0)
| ~ attr(X1,c35)
| ~ sub(X0,eigenname_1_1)
| ~ obj(c43,X1)
| ~ arg1(c55,X1)
| ~ attr(X1,X0) )
| ~ spl52_10 ),
inference(avatar_component_clause,[],[f10907]) ).
fof(f10911,definition,
( spl52_11
<=> sub(c34,eigenname_1_1) ),
introduced(definition,[new_symbols(definition,[spl52_11])],[avatar_definition]) ).
fof(f10912,plain,
( ~ sub(c34,eigenname_1_1)
| spl52_11 ),
inference(avatar_component_clause,[],[f10911]) ).
fof(f10917,plain,
( $false
| spl52_9 ),
inference(resolution,[],[f10905,f10504]) ).
fof(f10918,plain,
spl52_9,
inference(avatar_contradiction_clause,[],[f10917]) ).
fof(f10919,plain,
( $false
| spl52_11 ),
inference(resolution,[],[f10912,f10506]) ).
fof(f10920,plain,
spl52_11,
inference(avatar_contradiction_clause,[],[f10919]) ).
fof(f10921,plain,
( ! [X0] :
( ~ attr(X0,c35)
| ~ sub(c34,eigenname_1_1)
| ~ obj(c43,X0)
| ~ arg1(c55,X0)
| ~ attr(X0,c34) )
| ~ spl52_10 ),
inference(resolution,[],[f10908,f10505]) ).
fof(f10923,definition,
( spl52_13
<=> ! [X0] :
( ~ attr(X0,c35)
| ~ attr(X0,c34)
| ~ arg1(c55,X0)
| ~ obj(c43,X0) ) ),
introduced(definition,[new_symbols(definition,[spl52_13])],[avatar_definition]) ).
fof(f10924,plain,
( ! [X0] :
( ~ attr(X0,c35)
| ~ attr(X0,c34)
| ~ arg1(c55,X0)
| ~ obj(c43,X0) )
| ~ spl52_13 ),
inference(avatar_component_clause,[],[f10923]) ).
fof(f10926,plain,
( ! [X0] : ~ sub(c38,X0)
| ~ spl52_5 ),
inference(resolution,[],[f10886,f10496]) ).
fof(f10927,plain,
( $false
| ~ spl52_5 ),
inference(resolution,[],[f10926,f10502]) ).
fof(f10928,plain,
~ spl52_5,
inference(avatar_contradiction_clause,[],[f10927]) ).
fof(f10931,plain,
( ~ spl52_11
| spl52_13
| ~ spl52_10 ),
inference(avatar_split_clause,[],[f10921,f10907,f10923,f10911]) ).
fof(f10933,plain,
( ! [X0,X1] :
( ~ val(X0,nelson_0)
| ~ arg1(c55,X1)
| ~ attr(X1,X0)
| ~ obj(c43,X1)
| ~ sub(X0,eigenname_1_1)
| ~ attr(X1,c35)
| ~ sub(c35,familiename_1_1) )
| ~ spl52_8 ),
inference(resolution,[],[f10895,f10503]) ).
fof(f10934,plain,
( ~ spl52_9
| spl52_10
| ~ spl52_8 ),
inference(avatar_split_clause,[],[f10933,f10894,f10907,f10904]) ).
fof(f10936,plain,
( ~ attr(c33,c34)
| ~ arg1(c55,c33)
| ~ obj(c43,c33)
| ~ spl52_13 ),
inference(resolution,[],[f10924,f10508]) ).
fof(f10938,definition,
( spl52_14
<=> obj(c43,c33) ),
introduced(definition,[new_symbols(definition,[spl52_14])],[avatar_definition]) ).
fof(f10939,plain,
( ~ obj(c43,c33)
| spl52_14 ),
inference(avatar_component_clause,[],[f10938]) ).
fof(f10941,definition,
( spl52_15
<=> arg1(c55,c33) ),
introduced(definition,[new_symbols(definition,[spl52_15])],[avatar_definition]) ).
fof(f10942,plain,
( ~ arg1(c55,c33)
| spl52_15 ),
inference(avatar_component_clause,[],[f10941]) ).
fof(f10944,definition,
( spl52_16
<=> attr(c33,c34) ),
introduced(definition,[new_symbols(definition,[spl52_16])],[avatar_definition]) ).
fof(f10945,plain,
( ~ attr(c33,c34)
| spl52_16 ),
inference(avatar_component_clause,[],[f10944]) ).
fof(f10946,plain,
( ~ spl52_14
| ~ spl52_15
| ~ spl52_16
| ~ spl52_13 ),
inference(avatar_split_clause,[],[f10936,f10923,f10944,f10941,f10938]) ).
fof(f10948,plain,
( $false
| spl52_14 ),
inference(resolution,[],[f10939,f10501]) ).
fof(f10949,plain,
spl52_14,
inference(avatar_contradiction_clause,[],[f10948]) ).
fof(f10951,plain,
( $false
| spl52_15 ),
inference(resolution,[],[f10942,f10497]) ).
fof(f10952,plain,
spl52_15,
inference(avatar_contradiction_clause,[],[f10951]) ).
fof(f10953,plain,
( $false
| spl52_16 ),
inference(resolution,[],[f10945,f10509]) ).
fof(f10954,plain,
spl52_16,
inference(avatar_contradiction_clause,[],[f10953]) ).
cnf(s1,plain,
( spl52_1
| spl52_2 ),
inference(sat_conversion,[],[f10869]) ).
cnf(s2,plain,
( ~ spl52_2
| ~ spl52_3
| ~ spl52_4 ),
inference(sat_conversion,[],[f10878]) ).
cnf(s3,plain,
spl52_3,
inference(sat_conversion,[],[f10880]) ).
cnf(s4,plain,
spl52_4,
inference(sat_conversion,[],[f10882]) ).
cnf(s5,plain,
( ~ spl52_1
| spl52_5
| ~ spl52_6
| ~ spl52_7
| spl52_8 ),
inference(sat_conversion,[],[f10896]) ).
cnf(s6,plain,
spl52_6,
inference(sat_conversion,[],[f10898]) ).
cnf(s7,plain,
spl52_7,
inference(sat_conversion,[],[f10900]) ).
cnf(s10,plain,
spl52_9,
inference(sat_conversion,[],[f10918]) ).
cnf(s11,plain,
spl52_11,
inference(sat_conversion,[],[f10920]) ).
cnf(s13,plain,
~ spl52_5,
inference(sat_conversion,[],[f10928]) ).
cnf(s16,plain,
( ~ spl52_10
| ~ spl52_11
| spl52_13 ),
inference(sat_conversion,[],[f10931]) ).
cnf(s17,plain,
( ~ spl52_8
| ~ spl52_9
| spl52_10 ),
inference(sat_conversion,[],[f10934]) ).
cnf(s19,plain,
( ~ spl52_13
| ~ spl52_14
| ~ spl52_15
| ~ spl52_16 ),
inference(sat_conversion,[],[f10946]) ).
cnf(s20,plain,
spl52_14,
inference(sat_conversion,[],[f10949]) ).
cnf(s21,plain,
spl52_15,
inference(sat_conversion,[],[f10952]) ).
cnf(s22,plain,
spl52_16,
inference(sat_conversion,[],[f10954]) ).
cnf(s23,plain,
~ spl52_13,
inference(rat,[],[s19,s22,s21,s20]) ).
cnf(s24,plain,
( ~ spl52_10
| ~ spl52_11 ),
inference(rat,[],[s16,s23]) ).
cnf(s26,plain,
~ spl52_10,
inference(rat,[],[s24,s11]) ).
cnf(s27,plain,
~ spl52_8,
inference(rat,[],[s17,s26,s10]) ).
cnf(s28,plain,
~ spl52_1,
inference(rat,[],[s5,s27,s7,s6,s13]) ).
cnf(s29,plain,
~ spl52_2,
inference(rat,[],[s2,s4,s3]) ).
cnf(s30,plain,
$false,
inference(rat,[],[s1,s29,s28]) ).
fof(f10955,plain,
$false,
inference(avatar_sat_refutation,[],[s30]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+33 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n006.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % 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:55 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 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.14/0.82 % (311025)Detected formulas, will run a generic FOF schedule.
% 2.14/0.82 % (311036)dis-21_1_sil=8000:lcm=predicate:random_seed=3628543977:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 2.14/0.82 % (311034)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2107732967:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 2.14/0.82 % (311035)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4063964526:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 2.14/0.82 % (311031)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=3779431286:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 2.14/0.82 % (311033)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1373708696:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 2.14/0.82 % (311030)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=2482402560:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 2.14/0.82 % (311032)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=323833330:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 2.14/0.82 % (311036)First to succeed.
% 2.14/0.82 % (311036)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-311025"
% 2.14/0.82 % (311034)Also succeeded, but the first one will report.
% 2.14/0.82 % (311033)Also succeeded, but the first one will report.
% 2.14/0.82 % (311035)Instruction limit reached!
% 2.14/0.82 % (311035)------------------------------
% 2.14/0.82 % (311035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.14/0.82 % (311035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.14/0.82 % (311035)CaDiCaL version: 2.1.3
% 2.14/0.82 % (311035)Termination reason: Instruction limit
% 2.14/0.82 % (311035)Termination phase: Saturation
% 2.14/0.82 % (311035)Time elapsed: 0.067 s
% 2.14/0.82 % (311035)Peak memory usage: 97 MB
% 2.14/0.82 % (311035)Instructions burned: 142 (million)
% 2.14/0.82 % (311036)Refutation found. Thanks to Tanya!
% 2.14/0.82 % SZS status Theorem for theBenchmark
% 2.14/0.82 % SZS output start Proof for theBenchmark
% See solution above
% 2.75/1.02 % (311036)------------------------------
% 2.75/1.02 % (311036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.75/1.02 % (311036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.75/1.02 % (311036)CaDiCaL version: 2.1.3
% 2.75/1.02 % (311036)Termination reason: Refutation
% 2.75/1.02 % (311036)Time elapsed: 0.023 s
% 2.75/1.02 % (311036)Peak memory usage: 99 MB
% 2.75/1.02 % (311036)Instructions burned: 88 (million)
% 2.75/1.02 % (311036)------------------------------
% 2.75/1.02 % (311036)------------------------------
% 2.75/1.02 % (311025)Success in time 0.402 s
% 2.75/1.02 % Vampire exiting
%------------------------------------------------------------------------------