%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR116+35 : 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 : n002.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 3.22s 1.61s
% Output : Refutation 6.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 22
% Syntax : Number of formulae : 160 ( 38 unt; 13 def)
% Number of atoms : 1527 ( 0 equ)
% Maximal formula atoms : 160 ( 9 avg)
% Number of connectives : 1743 ( 376 ~; 327 |;1021 &)
% ( 13 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 160 ( 12 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 45 ( 44 usr; 14 prp; 0-2 aty)
% Number of functors : 64 ( 64 usr; 56 con; 0-3 aty)
% Number of variables : 286 ( 0 sgn 243 !; 43 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',member_first) ).
fof(f11,axiom,
! [X0,X1] :
( fact(X0,X1)
=> has_fact_leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',has_fact_eq) ).
fof(f95,axiom,
! [X0,X1] :
( ( has_fact_leq(X1,real)
& loc(X1,X0) )
=> ? [X2] :
( loc(X2,X0)
& obj(X2,X1)
& subs(X2,geben_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',loc__geben_1_1_loc) ).
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(f159,axiom,
! [X0,X1,X2] :
( ( attr(X2,X0)
& member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
& sub(X0,X1) )
=> ? [X3] :
( arg1(X3,X2)
& arg2(X3,X2)
& subs(X3,hei__337en_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',attr_name_hei__337en_1_1) ).
fof(f161,axiom,
! [X0,X1,X2] :
( ( arg1(X0,X1)
& arg2(X0,X2)
& subs(X0,hei__337en_1_1) )
=> ? [X3,X4] :
( arg1(X4,X1)
& arg2(X4,X2)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hei__337en_1_1__bezeichnen_1_1_als) ).
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_714) ).
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,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& just(c38,c40)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& sort(amtszeit__1_1,ta)
& card(amtszeit__1_1,int1)
& etype(amtszeit__1_1,int0)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& quant(amtszeit__1_1,one)
& refer(amtszeit__1_1,refer_c)
& varia(amtszeit__1_1,varia_c)
& sort(amt_1_2,ad)
& sort(amt_1_2,io)
& card(amt_1_2,int1)
& etype(amt_1_2,int0)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& quant(amt_1_2,one)
& refer(amt_1_2,refer_c)
& varia(amt_1_2,varia_c)
& sort(zeit_1_1,ta)
& card(zeit_1_1,int1)
& etype(zeit_1_1,int0)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& quant(zeit_1_1,one)
& refer(zeit_1_1,refer_c)
& varia(zeit_1_1,varia_c)
& sort(c16,d)
& card(c16,int1)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& quant(c16,one)
& refer(c16,det)
& varia(c16,con)
& sort(c7,ta)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,det)
& varia(c7,con)
& sort(c17,na)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,indet)
& varia(c17,varia_c)
& sort(c18,na)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,indet)
& varia(c18,varia_c)
& sort(s__374dafrikanisch_1_1,nq)
& sort(pr__344sident_1_1,d)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& sort(eigenname_1_1,na)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& sort(nelson_0,fe)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(mandela_0,fe)
& sort(c24,o)
& card(c24,cons(x_constant,cons(int1,nil)))
& etype(c24,int1)
& etype(c24,int2)
& etype(c24,int3)
& fact(c24,real)
& gener(c24,sp)
& quant(c24,mult)
& refer(c24,indet)
& varia(c24,varia_c)
& sort(mehrere_2_1,o)
& card(mehrere_2_1,cons(x_constant,cons(int1,nil)))
& etype(mehrere_2_1,int1)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& quant(mehrere_2_1,mult)
& refer(mehrere_2_1,refer_c)
& varia(mehrere_2_1,varia_c)
& sort(c34,d)
& card(c34,int100)
& etype(c34,int1)
& fact(c34,real)
& gener(c34,sp)
& quant(c34,nfquant)
& refer(c34,indet)
& varia(c34,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(c38,o)
& card(c38,int1)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,gener_c)
& quant(c38,one)
& refer(c38,refer_c)
& varia(c38,varia_c)
& sort(c40,da)
& fact(c40,real)
& gener(c40,sp)
& sort(geisterglaube_1_1,o)
& card(geisterglaube_1_1,int1)
& etype(geisterglaube_1_1,int0)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& quant(geisterglaube_1_1,one)
& refer(geisterglaube_1_1,refer_c)
& varia(geisterglaube_1_1,varia_c)
& sort(abmurksen_1_1,da)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_wp_714) ).
fof(f10191,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& sort(amtszeit__1_1,ta)
& card(amtszeit__1_1,int1)
& etype(amtszeit__1_1,int0)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& quant(amtszeit__1_1,one)
& refer(amtszeit__1_1,refer_c)
& varia(amtszeit__1_1,varia_c)
& sort(amt_1_2,ad)
& sort(amt_1_2,io)
& card(amt_1_2,int1)
& etype(amt_1_2,int0)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& quant(amt_1_2,one)
& refer(amt_1_2,refer_c)
& varia(amt_1_2,varia_c)
& sort(zeit_1_1,ta)
& card(zeit_1_1,int1)
& etype(zeit_1_1,int0)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& quant(zeit_1_1,one)
& refer(zeit_1_1,refer_c)
& varia(zeit_1_1,varia_c)
& sort(c16,d)
& card(c16,int1)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& quant(c16,one)
& refer(c16,det)
& varia(c16,con)
& sort(c7,ta)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,det)
& varia(c7,con)
& sort(c17,na)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,indet)
& varia(c17,varia_c)
& sort(c18,na)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,indet)
& varia(c18,varia_c)
& sort(s__374dafrikanisch_1_1,nq)
& sort(pr__344sident_1_1,d)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& sort(eigenname_1_1,na)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& sort(nelson_0,fe)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(mandela_0,fe)
& sort(c24,o)
& card(c24,cons(x_constant,cons(int1,nil)))
& etype(c24,int1)
& etype(c24,int2)
& etype(c24,int3)
& fact(c24,real)
& gener(c24,sp)
& quant(c24,mult)
& refer(c24,indet)
& varia(c24,varia_c)
& sort(mehrere_2_1,o)
& card(mehrere_2_1,cons(x_constant,cons(int1,nil)))
& etype(mehrere_2_1,int1)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& quant(mehrere_2_1,mult)
& refer(mehrere_2_1,refer_c)
& varia(mehrere_2_1,varia_c)
& sort(c34,d)
& card(c34,int100)
& etype(c34,int1)
& fact(c34,real)
& gener(c34,sp)
& quant(c34,nfquant)
& refer(c34,indet)
& varia(c34,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(c38,o)
& card(c38,int1)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,gener_c)
& quant(c38,one)
& refer(c38,refer_c)
& varia(c38,varia_c)
& sort(c40,da)
& fact(c40,real)
& gener(c40,sp)
& sort(geisterglaube_1_1,o)
& card(geisterglaube_1_1,int1)
& etype(geisterglaube_1_1,int0)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& quant(geisterglaube_1_1,one)
& refer(geisterglaube_1_1,refer_c)
& varia(geisterglaube_1_1,varia_c)
& sort(abmurksen_1_1,da)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10195,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& sort(amtszeit__1_1,ta)
& card(amtszeit__1_1,int1)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& quant(amtszeit__1_1,one)
& refer(amtszeit__1_1,refer_c)
& varia(amtszeit__1_1,varia_c)
& sort(amt_1_2,ad)
& sort(amt_1_2,io)
& card(amt_1_2,int1)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& quant(amt_1_2,one)
& refer(amt_1_2,refer_c)
& varia(amt_1_2,varia_c)
& sort(zeit_1_1,ta)
& card(zeit_1_1,int1)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& quant(zeit_1_1,one)
& refer(zeit_1_1,refer_c)
& varia(zeit_1_1,varia_c)
& sort(c16,d)
& card(c16,int1)
& fact(c16,real)
& gener(c16,sp)
& quant(c16,one)
& refer(c16,det)
& varia(c16,con)
& sort(c7,ta)
& card(c7,int1)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,det)
& varia(c7,con)
& sort(c17,na)
& card(c17,int1)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,indet)
& varia(c17,varia_c)
& sort(c18,na)
& card(c18,int1)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,indet)
& varia(c18,varia_c)
& 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(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(c24,o)
& card(c24,cons(x_constant,cons(int1,nil)))
& fact(c24,real)
& gener(c24,sp)
& quant(c24,mult)
& refer(c24,indet)
& varia(c24,varia_c)
& sort(mehrere_2_1,o)
& card(mehrere_2_1,cons(x_constant,cons(int1,nil)))
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& quant(mehrere_2_1,mult)
& refer(mehrere_2_1,refer_c)
& varia(mehrere_2_1,varia_c)
& sort(c34,d)
& card(c34,int100)
& fact(c34,real)
& gener(c34,sp)
& quant(c34,nfquant)
& refer(c34,indet)
& varia(c34,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(c38,o)
& card(c38,int1)
& fact(c38,real)
& gener(c38,gener_c)
& quant(c38,one)
& refer(c38,refer_c)
& varia(c38,varia_c)
& sort(c40,da)
& fact(c40,real)
& gener(c40,sp)
& sort(geisterglaube_1_1,o)
& card(geisterglaube_1_1,int1)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& quant(geisterglaube_1_1,one)
& refer(geisterglaube_1_1,refer_c)
& varia(geisterglaube_1_1,varia_c)
& sort(abmurksen_1_1,da)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10215,plain,
! [X0,X1,X2] :
( ( arg1(X0,X1)
& arg2(X0,X2)
& subs(X0,hei__337en_1_1) )
=> ? [X3,X4] :
( arg1(X4,X1)
& arg2(X4,X2)
& hsit(X0,X3)
& obj(X3,X1)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) ) ),
inference(pure_predicate_removal,[],[f161]) ).
fof(f10238,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& card(amtszeit__1_1,int1)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& quant(amtszeit__1_1,one)
& refer(amtszeit__1_1,refer_c)
& varia(amtszeit__1_1,varia_c)
& card(amt_1_2,int1)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& quant(amt_1_2,one)
& refer(amt_1_2,refer_c)
& varia(amt_1_2,varia_c)
& card(zeit_1_1,int1)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& quant(zeit_1_1,one)
& refer(zeit_1_1,refer_c)
& varia(zeit_1_1,varia_c)
& card(c16,int1)
& fact(c16,real)
& gener(c16,sp)
& quant(c16,one)
& refer(c16,det)
& varia(c16,con)
& card(c7,int1)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,det)
& varia(c7,con)
& card(c17,int1)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,indet)
& varia(c17,varia_c)
& card(c18,int1)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,indet)
& varia(c18,varia_c)
& 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(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(c24,cons(x_constant,cons(int1,nil)))
& fact(c24,real)
& gener(c24,sp)
& quant(c24,mult)
& refer(c24,indet)
& varia(c24,varia_c)
& card(mehrere_2_1,cons(x_constant,cons(int1,nil)))
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& quant(mehrere_2_1,mult)
& refer(mehrere_2_1,refer_c)
& varia(mehrere_2_1,varia_c)
& card(c34,int100)
& fact(c34,real)
& gener(c34,sp)
& quant(c34,nfquant)
& refer(c34,indet)
& varia(c34,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(c38,int1)
& fact(c38,real)
& gener(c38,gener_c)
& quant(c38,one)
& refer(c38,refer_c)
& varia(c38,varia_c)
& fact(c40,real)
& gener(c40,sp)
& card(geisterglaube_1_1,int1)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& quant(geisterglaube_1_1,one)
& refer(geisterglaube_1_1,refer_c)
& varia(geisterglaube_1_1,varia_c)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10195]) ).
fof(f10241,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& card(amtszeit__1_1,int1)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& refer(amtszeit__1_1,refer_c)
& varia(amtszeit__1_1,varia_c)
& card(amt_1_2,int1)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& refer(amt_1_2,refer_c)
& varia(amt_1_2,varia_c)
& card(zeit_1_1,int1)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& refer(zeit_1_1,refer_c)
& varia(zeit_1_1,varia_c)
& card(c16,int1)
& fact(c16,real)
& gener(c16,sp)
& refer(c16,det)
& varia(c16,con)
& card(c7,int1)
& fact(c7,real)
& gener(c7,sp)
& refer(c7,det)
& varia(c7,con)
& card(c17,int1)
& fact(c17,real)
& gener(c17,sp)
& refer(c17,indet)
& varia(c17,varia_c)
& card(c18,int1)
& fact(c18,real)
& gener(c18,sp)
& refer(c18,indet)
& varia(c18,varia_c)
& 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(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(c24,cons(x_constant,cons(int1,nil)))
& fact(c24,real)
& gener(c24,sp)
& refer(c24,indet)
& varia(c24,varia_c)
& card(mehrere_2_1,cons(x_constant,cons(int1,nil)))
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& refer(mehrere_2_1,refer_c)
& varia(mehrere_2_1,varia_c)
& card(c34,int100)
& fact(c34,real)
& gener(c34,sp)
& refer(c34,indet)
& varia(c34,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(c38,int1)
& fact(c38,real)
& gener(c38,gener_c)
& refer(c38,refer_c)
& varia(c38,varia_c)
& fact(c40,real)
& gener(c40,sp)
& card(geisterglaube_1_1,int1)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& refer(geisterglaube_1_1,refer_c)
& varia(geisterglaube_1_1,varia_c)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10238]) ).
fof(f10244,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& refer(amtszeit__1_1,refer_c)
& varia(amtszeit__1_1,varia_c)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& refer(amt_1_2,refer_c)
& varia(amt_1_2,varia_c)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& refer(zeit_1_1,refer_c)
& varia(zeit_1_1,varia_c)
& fact(c16,real)
& gener(c16,sp)
& refer(c16,det)
& varia(c16,con)
& fact(c7,real)
& gener(c7,sp)
& refer(c7,det)
& varia(c7,con)
& fact(c17,real)
& gener(c17,sp)
& refer(c17,indet)
& varia(c17,varia_c)
& fact(c18,real)
& gener(c18,sp)
& refer(c18,indet)
& varia(c18,varia_c)
& 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(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(c24,real)
& gener(c24,sp)
& refer(c24,indet)
& varia(c24,varia_c)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& refer(mehrere_2_1,refer_c)
& varia(mehrere_2_1,varia_c)
& fact(c34,real)
& gener(c34,sp)
& refer(c34,indet)
& varia(c34,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(c38,real)
& gener(c38,gener_c)
& refer(c38,refer_c)
& varia(c38,varia_c)
& fact(c40,real)
& gener(c40,sp)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& refer(geisterglaube_1_1,refer_c)
& varia(geisterglaube_1_1,varia_c)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10241]) ).
fof(f10247,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& varia(amtszeit__1_1,varia_c)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& varia(amt_1_2,varia_c)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& varia(zeit_1_1,varia_c)
& fact(c16,real)
& gener(c16,sp)
& varia(c16,con)
& fact(c7,real)
& gener(c7,sp)
& varia(c7,con)
& fact(c17,real)
& gener(c17,sp)
& varia(c17,varia_c)
& fact(c18,real)
& gener(c18,sp)
& varia(c18,varia_c)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& varia(pr__344sident_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(c24,real)
& gener(c24,sp)
& varia(c24,varia_c)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& varia(mehrere_2_1,varia_c)
& fact(c34,real)
& gener(c34,sp)
& varia(c34,varia_c)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& varia(mensch_1_1,varia_c)
& fact(c38,real)
& gener(c38,gener_c)
& varia(c38,varia_c)
& fact(c40,real)
& gener(c40,sp)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& varia(geisterglaube_1_1,varia_c)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10244]) ).
fof(f10252,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& fact(c16,real)
& gener(c16,sp)
& fact(c7,real)
& gener(c7,sp)
& fact(c17,real)
& gener(c17,sp)
& fact(c18,real)
& gener(c18,sp)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& fact(c24,real)
& gener(c24,sp)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& fact(c34,real)
& gener(c34,sp)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& fact(c38,real)
& gener(c38,gener_c)
& fact(c40,real)
& gener(c40,sp)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10247]) ).
fof(f10257,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& fact(amtszeit__1_1,real)
& fact(amt_1_2,real)
& fact(zeit_1_1,real)
& fact(c16,real)
& fact(c7,real)
& fact(c17,real)
& fact(c18,real)
& fact(pr__344sident_1_1,real)
& fact(eigenname_1_1,real)
& fact(familiename_1_1,real)
& fact(c24,real)
& fact(mehrere_2_1,real)
& fact(c34,real)
& fact(mensch_1_1,real)
& fact(c38,real)
& fact(c40,real)
& fact(geisterglaube_1_1,real)
& fact(abmurksen_1_1,real) ),
inference(pure_predicate_removal,[],[f10252]) ).
fof(f10260,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(f10265,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( arg1(X4,X1)
& arg2(X4,X2)
& hsit(X0,X3)
& obj(X3,X1)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(ennf_transformation,[],[f10215]) ).
fof(f10266,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( arg1(X4,X1)
& arg2(X4,X2)
& hsit(X0,X3)
& obj(X3,X1)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(flattening,[],[f10265]) ).
fof(f10305,plain,
! [X0,X1] :
( ? [X2] :
( loc(X2,X0)
& obj(X2,X1)
& subs(X2,geben_1_1) )
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(ennf_transformation,[],[f95]) ).
fof(f10306,plain,
! [X0,X1] :
( ? [X2] :
( loc(X2,X0)
& obj(X2,X1)
& subs(X2,geben_1_1) )
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(flattening,[],[f10305]) ).
fof(f10309,plain,
! [X0,X1,X2] :
( ? [X3] :
( arg1(X3,X2)
& arg2(X3,X2)
& subs(X3,hei__337en_1_1) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f159]) ).
fof(f10310,plain,
! [X0,X1,X2] :
( ? [X3] :
( arg1(X3,X2)
& arg2(X3,X2)
& subs(X3,hei__337en_1_1) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(flattening,[],[f10309]) ).
fof(f10320,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(f10321,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,[],[f10320]) ).
fof(f10340,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f10401,plain,
! [X0,X1,X2] :
( ( arg1(sK4(X0,X1,X2),X1)
& arg2(sK4(X0,X1,X2),X2)
& hsit(X0,sK3(X0,X1,X2))
& obj(sK3(X0,X1,X2),X1)
& subr(sK4(X0,X1,X2),rprs_0)
& subs(sK3(X0,X1,X2),bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X3,sK3(X0,X1,X2)),skolemize(X4,sK4(X0,X1,X2))],[f10266]) ).
fof(f10416,plain,
! [X0,X1] :
( ( loc(sK21(X0,X1),X0)
& obj(sK21(X0,X1),X1)
& subs(sK21(X0,X1),geben_1_1) )
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(X2,sK21(X0,X1))],[f10306]) ).
fof(f10419,plain,
! [X0,X1,X2] :
( ( arg1(sK24(X2),X2)
& arg2(sK24(X2),X2)
& subs(sK24(X2),hei__337en_1_1) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(X3,sK24(X2))],[f10310]) ).
fof(f10424,plain,
! [X0,X1,X2] :
( ( in(sK32(X0,X2),sK30(X0,X2))
& attr(sK30(X0,X2),sK31(X0,X2))
& loc(X0,sK32(X0,X2))
& sub(sK30(X0,X2),land_1_1)
& sub(sK31(X0,X2),name_1_1)
& val(sK31(X0,X2),X2) )
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30,sK31,sK32]),skolemize(X3,sK30(X0,X2)),skolemize(X4,sK31(X0,X2)),skolemize(X5,sK32(X0,X2))],[f10321]) ).
fof(f10439,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,[],[f10260]) ).
fof(f10454,plain,
fact(c16,real),
inference(cnf_transformation,[],[f10257]) ).
fof(f10466,plain,
val(c18,mandela_0),
inference(cnf_transformation,[],[f10257]) ).
fof(f10467,plain,
sub(c18,familiename_1_1),
inference(cnf_transformation,[],[f10257]) ).
fof(f10468,plain,
val(c17,nelson_0),
inference(cnf_transformation,[],[f10257]) ).
fof(f10469,plain,
sub(c17,eigenname_1_1),
inference(cnf_transformation,[],[f10257]) ).
fof(f10470,plain,
sub(c16,pr__344sident_1_1),
inference(cnf_transformation,[],[f10257]) ).
fof(f10471,plain,
prop(c16,s__374dafrikanisch_1_1),
inference(cnf_transformation,[],[f10257]) ).
fof(f10472,plain,
attr(c16,c18),
inference(cnf_transformation,[],[f10257]) ).
fof(f10473,plain,
attr(c16,c17),
inference(cnf_transformation,[],[f10257]) ).
fof(f10486,plain,
! [X2,X0,X1] :
( subr(sK4(X0,X1,X2),rprs_0)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(cnf_transformation,[],[f10401]) ).
fof(f10489,plain,
! [X2,X0,X1] :
( arg2(sK4(X0,X1,X2),X2)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(cnf_transformation,[],[f10401]) ).
fof(f10490,plain,
! [X2,X0,X1] :
( arg1(sK4(X0,X1,X2),X1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(cnf_transformation,[],[f10401]) ).
fof(f10556,plain,
! [X0,X1] :
( obj(sK21(X0,X1),X1)
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(cnf_transformation,[],[f10416]) ).
fof(f10564,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0)
| subs(sK24(X2),hei__337en_1_1)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10419]) ).
fof(f10565,plain,
! [X2,X0,X1] :
( arg2(sK24(X2),X2)
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10419]) ).
fof(f10566,plain,
! [X2,X0,X1] :
( arg1(sK24(X2),X2)
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10419]) ).
fof(f10585,plain,
! [X2,X0,X1] :
( val(sK31(X0,X2),X2)
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10424]) ).
fof(f10586,plain,
! [X2,X0,X1] :
( sub(sK31(X0,X2),name_1_1)
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10424]) ).
fof(f10588,plain,
! [X2,X0,X1] :
( loc(X0,sK32(X0,X2))
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10424]) ).
fof(f10589,plain,
! [X2,X0,X1] :
( attr(sK30(X0,X2),sK31(X0,X2))
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10424]) ).
fof(f10590,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| in(sK32(X0,X2),sK30(X0,X2)) ),
inference(cnf_transformation,[],[f10424]) ).
fof(f10602,plain,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
inference(cnf_transformation,[],[f9161]) ).
fof(f10606,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[],[f1]) ).
fof(f10613,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(cnf_transformation,[],[f10340]) ).
fof(f10684,definition,
( spl47_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,[spl47_1])],[avatar_definition]) ).
fof(f10685,plain,
( ! [X2,X3,X0,X1,X8,X9,X4] :
( ~ subr(X3,rprs_0)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ arg1(X3,X0)
| ~ 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) )
| ~ spl47_1 ),
inference(avatar_component_clause,[],[f10684]) ).
fof(f10687,definition,
( spl47_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,[spl47_2])],[avatar_definition]) ).
fof(f10688,plain,
( ! [X6,X7,X5] :
( ~ val(X7,s__374dafrika_0)
| ~ in(X5,X6)
| ~ sub(X7,name_1_1)
| ~ attr(X6,X7) )
| ~ spl47_2 ),
inference(avatar_component_clause,[],[f10687]) ).
fof(f10689,plain,
( spl47_1
| spl47_2 ),
inference(avatar_split_clause,[],[f10439,f10687,f10684]) ).
fof(f10691,plain,
( ! [X2,X3,X0,X1] :
( ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ in(X2,X3)
| ~ sub(sK31(X0,s__374dafrika_0),name_1_1)
| ~ attr(X3,sK31(X0,s__374dafrika_0)) )
| ~ spl47_2 ),
inference(resolution,[],[f10585,f10688]) ).
fof(f10692,plain,
( ! [X2,X3,X0,X1] :
( ~ attr(X3,sK31(X0,s__374dafrika_0))
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ in(X2,X3)
| ~ prop(X0,X1) )
| ~ spl47_2 ),
inference(forward_subsumption_resolution,[],[f10691,f10586]) ).
fof(f10698,plain,
( ! [X2,X3,X0,X1] :
( ~ in(X3,sK30(X0,s__374dafrika_0))
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ state_adjective_state_binding(X2,s__374dafrika_0)
| ~ prop(X0,X1)
| ~ prop(X0,X2) )
| ~ spl47_2 ),
inference(resolution,[],[f10589,f10692]) ).
fof(f10699,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| in(sK32(X0,s__374dafrika_0),sK30(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10590,f10602]) ).
fof(f10700,plain,
in(sK32(c16,s__374dafrika_0),sK30(c16,s__374dafrika_0)),
inference(resolution,[],[f10699,f10471]) ).
fof(f10704,plain,
( ! [X0,X1] :
( ~ state_adjective_state_binding(X0,s__374dafrika_0)
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ prop(c16,X0)
| ~ prop(c16,X1) )
| ~ spl47_2 ),
inference(resolution,[],[f10700,f10698]) ).
fof(f10708,definition,
( spl47_3
<=> ! [X1] :
( ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ prop(c16,X1) ) ),
introduced(definition,[new_symbols(definition,[spl47_3])],[avatar_definition]) ).
fof(f10709,plain,
( ! [X1] :
( ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ prop(c16,X1) )
| ~ spl47_3 ),
inference(avatar_component_clause,[],[f10708]) ).
fof(f10710,plain,
( spl47_3
| spl47_3
| ~ spl47_2 ),
inference(avatar_split_clause,[],[f10704,f10687,f10708,f10708]) ).
fof(f10711,plain,
( ~ prop(c16,s__374dafrikanisch_1_1)
| ~ spl47_3 ),
inference(resolution,[],[f10709,f10602]) ).
fof(f10712,plain,
( $false
| ~ spl47_3 ),
inference(forward_subsumption_resolution,[],[f10711,f10471]) ).
fof(f10713,plain,
~ spl47_3,
inference(avatar_contradiction_clause,[],[f10712]) ).
fof(f10721,plain,
( ! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ arg2(sK4(X0,X1,X2),X6)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1)
| ~ val(X3,nelson_0)
| ~ val(X4,mandela_0)
| ~ arg1(sK4(X0,X1,X2),X5)
| ~ sub(X6,X7)
| ~ sub(X3,eigenname_1_1)
| ~ sub(X4,familiename_1_1)
| ~ obj(X8,X5)
| ~ attr(X5,X3)
| ~ attr(X5,X4)
| ~ arg1(X0,X1) )
| ~ spl47_1 ),
inference(resolution,[],[f10486,f10685]) ).
fof(f10722,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1)
| ~ val(X3,nelson_0)
| ~ val(X4,mandela_0)
| ~ arg1(sK4(X0,X1,X2),X5)
| ~ sub(X2,X6)
| ~ sub(X3,eigenname_1_1)
| ~ sub(X4,familiename_1_1)
| ~ obj(X7,X5)
| ~ attr(X5,X3)
| ~ attr(X5,X4)
| ~ arg1(X0,X1) )
| ~ spl47_1 ),
inference(resolution,[],[f10489,f10721]) ).
fof(f10723,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ arg1(sK4(X0,X1,X2),X5)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1)
| ~ val(X3,nelson_0)
| ~ val(X4,mandela_0)
| ~ arg1(X0,X1)
| ~ sub(X2,X6)
| ~ sub(X3,eigenname_1_1)
| ~ sub(X4,familiename_1_1)
| ~ obj(X7,X5)
| ~ attr(X5,X3)
| ~ attr(X5,X4) )
| ~ spl47_1 ),
inference(duplicate_literal_removal,[],[f10722]) ).
fof(f10724,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ arg2(X0,X1)
| ~ subs(X0,hei__337en_1_1)
| ~ val(X2,nelson_0)
| ~ val(X3,mandela_0)
| ~ arg1(X0,X4)
| ~ sub(X1,X5)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X3,familiename_1_1)
| ~ obj(X6,X4)
| ~ attr(X4,X2)
| ~ attr(X4,X3)
| ~ arg1(X0,X4)
| ~ arg2(X0,X1)
| ~ subs(X0,hei__337en_1_1) )
| ~ spl47_1 ),
inference(resolution,[],[f10723,f10490]) ).
fof(f10725,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ val(X3,mandela_0)
| ~ subs(X0,hei__337en_1_1)
| ~ val(X2,nelson_0)
| ~ arg2(X0,X1)
| ~ arg1(X0,X4)
| ~ sub(X1,X5)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X3,familiename_1_1)
| ~ obj(X6,X4)
| ~ attr(X4,X2)
| ~ attr(X4,X3) )
| ~ spl47_1 ),
inference(duplicate_literal_removal,[],[f10724]) ).
fof(f10726,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ subs(X0,hei__337en_1_1)
| ~ val(X1,nelson_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X3)
| ~ sub(X2,X4)
| ~ sub(X1,eigenname_1_1)
| ~ sub(c18,familiename_1_1)
| ~ obj(X5,X3)
| ~ attr(X3,X1)
| ~ attr(X3,c18) )
| ~ spl47_1 ),
inference(resolution,[],[f10725,f10466]) ).
fof(f10729,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ attr(X3,c18)
| ~ val(X1,nelson_0)
| ~ arg2(X0,X2)
| ~ arg1(X0,X3)
| ~ sub(X2,X4)
| ~ sub(X1,eigenname_1_1)
| ~ obj(X5,X3)
| ~ attr(X3,X1)
| ~ subs(X0,hei__337en_1_1) )
| ~ spl47_1 ),
inference(forward_subsumption_resolution,[],[f10726,f10467]) ).
fof(f10730,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ val(X0,nelson_0)
| ~ arg2(X1,X2)
| ~ arg1(X1,c16)
| ~ sub(X2,X3)
| ~ sub(X0,eigenname_1_1)
| ~ obj(X4,c16)
| ~ attr(c16,X0)
| ~ subs(X1,hei__337en_1_1) )
| ~ spl47_1 ),
inference(resolution,[],[f10729,f10472]) ).
fof(f10732,definition,
( spl47_4
<=> ! [X4] : ~ obj(X4,c16) ),
introduced(definition,[new_symbols(definition,[spl47_4])],[avatar_definition]) ).
fof(f10733,plain,
( ! [X4] : ~ obj(X4,c16)
| ~ spl47_4 ),
inference(avatar_component_clause,[],[f10732]) ).
fof(f10735,definition,
( spl47_5
<=> ! [X2,X1,X3] :
( ~ arg2(X1,X2)
| ~ subs(X1,hei__337en_1_1)
| ~ sub(X2,X3)
| ~ arg1(X1,c16) ) ),
introduced(definition,[new_symbols(definition,[spl47_5])],[avatar_definition]) ).
fof(f10736,plain,
( ! [X2,X3,X1] :
( ~ subs(X1,hei__337en_1_1)
| ~ arg2(X1,X2)
| ~ sub(X2,X3)
| ~ arg1(X1,c16) )
| ~ spl47_5 ),
inference(avatar_component_clause,[],[f10735]) ).
fof(f10738,definition,
( spl47_6
<=> ! [X0] :
( ~ val(X0,nelson_0)
| ~ attr(c16,X0)
| ~ sub(X0,eigenname_1_1) ) ),
introduced(definition,[new_symbols(definition,[spl47_6])],[avatar_definition]) ).
fof(f10739,plain,
( ! [X0] :
( ~ val(X0,nelson_0)
| ~ attr(c16,X0)
| ~ sub(X0,eigenname_1_1) )
| ~ spl47_6 ),
inference(avatar_component_clause,[],[f10738]) ).
fof(f10740,plain,
( spl47_4
| spl47_5
| spl47_6
| ~ spl47_1 ),
inference(avatar_split_clause,[],[f10730,f10684,f10738,f10735,f10732]) ).
fof(f10828,plain,
! [X0,X1] :
( ~ attr(X0,X1)
| subs(sK24(X0),hei__337en_1_1)
| ~ sub(X1,eigenname_1_1) ),
inference(resolution,[],[f10564,f10606]) ).
fof(f10878,plain,
( subs(sK24(c16),hei__337en_1_1)
| ~ sub(c17,eigenname_1_1) ),
inference(resolution,[],[f10828,f10473]) ).
fof(f10881,plain,
subs(sK24(c16),hei__337en_1_1),
inference(forward_subsumption_resolution,[],[f10878,f10469]) ).
fof(f10887,definition,
( spl47_8
<=> subs(sK24(c16),hei__337en_1_1) ),
introduced(definition,[new_symbols(definition,[spl47_8])],[avatar_definition]) ).
fof(f10889,plain,
( subs(sK24(c16),hei__337en_1_1)
| ~ spl47_8 ),
inference(avatar_component_clause,[],[f10887]) ).
fof(f10891,plain,
spl47_8,
inference(avatar_split_clause,[],[f10881,f10887]) ).
fof(f10892,plain,
( ! [X0,X1] :
( ~ arg2(sK24(c16),X0)
| ~ sub(X0,X1)
| ~ arg1(sK24(c16),c16) )
| ~ spl47_5
| ~ spl47_8 ),
inference(resolution,[],[f10889,f10736]) ).
fof(f10904,definition,
( spl47_9
<=> arg1(sK24(c16),c16) ),
introduced(definition,[new_symbols(definition,[spl47_9])],[avatar_definition]) ).
fof(f10905,plain,
( arg1(sK24(c16),c16)
| ~ spl47_9 ),
inference(avatar_component_clause,[],[f10904]) ).
fof(f10906,plain,
( ~ arg1(sK24(c16),c16)
| spl47_9 ),
inference(avatar_component_clause,[],[f10904]) ).
fof(f10908,definition,
( spl47_10
<=> ! [X0,X1] :
( ~ arg2(sK24(c16),X0)
| ~ sub(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl47_10])],[avatar_definition]) ).
fof(f10909,plain,
( ! [X0,X1] :
( ~ arg2(sK24(c16),X0)
| ~ sub(X0,X1) )
| ~ spl47_10 ),
inference(avatar_component_clause,[],[f10908]) ).
fof(f10911,plain,
( ! [X0,X1] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c16,X0)
| ~ sub(X0,X1) )
| spl47_9 ),
inference(resolution,[],[f10906,f10566]) ).
fof(f10917,plain,
( ! [X0] :
( ~ attr(c16,X0)
| ~ sub(X0,eigenname_1_1) )
| spl47_9 ),
inference(resolution,[],[f10911,f10606]) ).
fof(f10924,plain,
( ~ sub(c17,eigenname_1_1)
| spl47_9 ),
inference(resolution,[],[f10917,f10473]) ).
fof(f10926,plain,
( $false
| spl47_9 ),
inference(forward_subsumption_resolution,[],[f10924,f10469]) ).
fof(f10927,plain,
spl47_9,
inference(avatar_contradiction_clause,[],[f10926]) ).
fof(f10931,plain,
( ~ attr(c16,c17)
| ~ sub(c17,eigenname_1_1)
| ~ spl47_6 ),
inference(resolution,[],[f10739,f10468]) ).
fof(f10934,plain,
( ~ sub(c17,eigenname_1_1)
| ~ spl47_6 ),
inference(forward_subsumption_resolution,[],[f10931,f10473]) ).
fof(f10935,plain,
( $false
| ~ spl47_6 ),
inference(forward_subsumption_resolution,[],[f10934,f10469]) ).
fof(f10936,plain,
~ spl47_6,
inference(avatar_contradiction_clause,[],[f10935]) ).
fof(f10937,plain,
( ! [X0,X1] :
( ~ arg2(sK24(c16),X0)
| ~ sub(X0,X1) )
| ~ spl47_5
| ~ spl47_8
| ~ spl47_9 ),
inference(forward_subsumption_resolution,[],[f10892,f10905]) ).
fof(f10938,plain,
( ! [X2,X0,X1] :
( ~ sub(c16,X0)
| ~ attr(c16,X1)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X1,X2) )
| ~ spl47_10 ),
inference(resolution,[],[f10909,f10565]) ).
fof(f10940,definition,
( spl47_11
<=> ! [X2,X1] :
( ~ attr(c16,X1)
| ~ sub(X1,X2)
| ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) ) ),
introduced(definition,[new_symbols(definition,[spl47_11])],[avatar_definition]) ).
fof(f10941,plain,
( ! [X2,X1] :
( ~ member(X2,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X1,X2)
| ~ attr(c16,X1) )
| ~ spl47_11 ),
inference(avatar_component_clause,[],[f10940]) ).
fof(f10943,definition,
( spl47_12
<=> ! [X0] : ~ sub(c16,X0) ),
introduced(definition,[new_symbols(definition,[spl47_12])],[avatar_definition]) ).
fof(f10944,plain,
( ! [X0] : ~ sub(c16,X0)
| ~ spl47_12 ),
inference(avatar_component_clause,[],[f10943]) ).
fof(f10945,plain,
( spl47_11
| spl47_12
| ~ spl47_10 ),
inference(avatar_split_clause,[],[f10938,f10908,f10943,f10940]) ).
fof(f10953,plain,
( ! [X0] :
( ~ has_fact_leq(c16,real)
| ~ loc(c16,X0) )
| ~ spl47_4 ),
inference(resolution,[],[f10733,f10556]) ).
fof(f10968,definition,
( spl47_15
<=> ! [X0] : ~ loc(c16,X0) ),
introduced(definition,[new_symbols(definition,[spl47_15])],[avatar_definition]) ).
fof(f10969,plain,
( ! [X0] : ~ loc(c16,X0)
| ~ spl47_15 ),
inference(avatar_component_clause,[],[f10968]) ).
fof(f10971,definition,
( spl47_16
<=> has_fact_leq(c16,real) ),
introduced(definition,[new_symbols(definition,[spl47_16])],[avatar_definition]) ).
fof(f10973,plain,
( ~ has_fact_leq(c16,real)
| spl47_16 ),
inference(avatar_component_clause,[],[f10971]) ).
fof(f10974,plain,
( spl47_15
| ~ spl47_16
| ~ spl47_4 ),
inference(avatar_split_clause,[],[f10953,f10732,f10971,f10968]) ).
fof(f10976,plain,
( ~ fact(c16,real)
| spl47_16 ),
inference(resolution,[],[f10973,f10613]) ).
fof(f10977,plain,
( $false
| spl47_16 ),
inference(forward_subsumption_resolution,[],[f10976,f10454]) ).
fof(f10978,plain,
spl47_16,
inference(avatar_contradiction_clause,[],[f10977]) ).
fof(f10980,plain,
( ! [X0,X1] :
( ~ state_adjective_state_binding(X0,X1)
| ~ prop(c16,X0) )
| ~ spl47_15 ),
inference(resolution,[],[f10969,f10588]) ).
fof(f10997,plain,
( ~ prop(c16,s__374dafrikanisch_1_1)
| ~ spl47_15 ),
inference(resolution,[],[f10980,f10602]) ).
fof(f10998,plain,
( $false
| ~ spl47_15 ),
inference(forward_subsumption_resolution,[],[f10997,f10471]) ).
fof(f10999,plain,
~ spl47_15,
inference(avatar_contradiction_clause,[],[f10998]) ).
fof(f11001,plain,
( spl47_10
| ~ spl47_5
| ~ spl47_8
| ~ spl47_9 ),
inference(avatar_split_clause,[],[f10937,f10904,f10887,f10735,f10908]) ).
fof(f11293,plain,
( ! [X0] :
( ~ attr(c16,X0)
| ~ sub(X0,eigenname_1_1) )
| ~ spl47_11 ),
inference(resolution,[],[f10941,f10606]) ).
fof(f11299,plain,
( ~ sub(c17,eigenname_1_1)
| ~ spl47_11 ),
inference(resolution,[],[f11293,f10473]) ).
fof(f11301,plain,
( $false
| ~ spl47_11 ),
inference(forward_subsumption_resolution,[],[f11299,f10469]) ).
fof(f11302,plain,
~ spl47_11,
inference(avatar_contradiction_clause,[],[f11301]) ).
fof(f11305,plain,
( $false
| ~ spl47_12 ),
inference(resolution,[],[f10944,f10470]) ).
fof(f11311,plain,
~ spl47_12,
inference(avatar_contradiction_clause,[],[f11305]) ).
cnf(s1,plain,
( spl47_1
| spl47_2 ),
inference(sat_conversion,[],[f10689]) ).
cnf(s2,plain,
( spl47_3
| ~ spl47_2
| spl47_3 ),
inference(sat_conversion,[],[f10710]) ).
cnf(s3,plain,
( ~ spl47_2
| spl47_3 ),
inference(rat,[],[s2]) ).
cnf(s4,plain,
~ spl47_3,
inference(sat_conversion,[],[f10713]) ).
cnf(s5,plain,
( ~ spl47_1
| spl47_4
| spl47_5
| spl47_6 ),
inference(sat_conversion,[],[f10740]) ).
cnf(s7,plain,
spl47_8,
inference(sat_conversion,[],[f10891]) ).
cnf(s9,plain,
spl47_9,
inference(sat_conversion,[],[f10927]) ).
cnf(s11,plain,
~ spl47_6,
inference(sat_conversion,[],[f10936]) ).
cnf(s12,plain,
( ~ spl47_10
| spl47_11
| spl47_12 ),
inference(sat_conversion,[],[f10945]) ).
cnf(s15,plain,
( ~ spl47_4
| spl47_15
| ~ spl47_16 ),
inference(sat_conversion,[],[f10974]) ).
cnf(s16,plain,
spl47_16,
inference(sat_conversion,[],[f10978]) ).
cnf(s18,plain,
~ spl47_15,
inference(sat_conversion,[],[f10999]) ).
cnf(s19,plain,
( ~ spl47_5
| ~ spl47_8
| ~ spl47_9
| spl47_10 ),
inference(sat_conversion,[],[f11001]) ).
cnf(s22,plain,
~ spl47_11,
inference(sat_conversion,[],[f11302]) ).
cnf(s24,plain,
~ spl47_12,
inference(sat_conversion,[],[f11311]) ).
cnf(s25,plain,
~ spl47_4,
inference(rat,[],[s15,s16,s18]) ).
cnf(s26,plain,
~ spl47_10,
inference(rat,[],[s12,s24,s22]) ).
cnf(s28,plain,
~ spl47_5,
inference(rat,[],[s19,s26,s9,s7]) ).
cnf(s29,plain,
~ spl47_1,
inference(rat,[],[s5,s11,s28,s25]) ).
cnf(s30,plain,
~ spl47_2,
inference(rat,[],[s3,s4]) ).
cnf(s31,plain,
$false,
inference(rat,[],[s1,s30,s29]) ).
fof(f11312,plain,
$false,
inference(avatar_sat_refutation,[],[s31]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+35 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n002.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 23:31:52 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 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
% 3.22/1.61 % (883911)Detected formulas, will run a generic FOF schedule.
% 3.22/1.61 % (883922)dis-21_1_sil=8000:lcm=predicate:random_seed=543585571: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)
% 3.22/1.61 % (883922)Instruction limit reached!
% 3.22/1.61 % (883922)------------------------------
% 3.22/1.61 % (883922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.61 % (883922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.61 % (883922)CaDiCaL version: 2.1.3
% 3.22/1.61 % (883922)Termination reason: Instruction limit
% 3.22/1.61 % (883922)Termination phase: Saturation
% 3.22/1.61 % (883922)Time elapsed: 0.038 s
% 3.22/1.61 % (883922)Peak memory usage: 98 MB
% 3.22/1.61 % (883922)Instructions burned: 133 (million)
% 3.22/1.61 % (883920)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2425344749:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 3.22/1.61 % (883919)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1208332545:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 3.22/1.61 % (883917)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=570777667:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 3.22/1.61 % (883921)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=152364798:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 3.22/1.61 % (883916)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=2815359416:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 3.22/1.61 % (883918)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=2812569654:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 3.22/1.61 % (883920)Refutation not found, incomplete strategy
% 3.22/1.61 % (883920)------------------------------
% 3.22/1.61 % (883920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.61 % (883920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.61 % (883920)CaDiCaL version: 2.1.3
% 3.22/1.61 % (883920)Termination reason: Refutation not found, incomplete strategy
% 3.22/1.61 % (883920)Time elapsed: 0.027 s
% 3.22/1.61 % (883920)Peak memory usage: 97 MB
% 3.22/1.61 % (883920)Instructions burned: 55 (million)
% 3.22/1.61 % (883919)Instruction limit reached!
% 3.22/1.61 % (883919)------------------------------
% 3.22/1.61 % (883919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.61 % (883919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.61 % (883919)CaDiCaL version: 2.1.3
% 3.22/1.61 % (883919)Termination reason: Instruction limit
% 3.22/1.61 % (883919)Termination phase: Saturation
% 3.22/1.61 % (883919)Time elapsed: 0.056 s
% 3.22/1.61 % (883919)Peak memory usage: 97 MB
% 3.22/1.61 % (883919)Instructions burned: 110 (million)
% 3.22/1.61 % (883921)Instruction limit reached!
% 3.22/1.61 % (883921)------------------------------
% 3.22/1.61 % (883921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.61 % (883921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.61 % (883921)CaDiCaL version: 2.1.3
% 3.22/1.61 % (883921)Termination reason: Instruction limit
% 3.22/1.61 % (883921)Termination phase: Saturation
% 3.22/1.61 % (883921)Time elapsed: 0.072 s
% 3.22/1.61 % (883921)Peak memory usage: 97 MB
% 3.22/1.61 % (883921)Instructions burned: 142 (million)
% 3.22/1.61 % (883924)lrs+10_1_sil=8000:sp=occurrence:random_seed=3048615617:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 3.22/1.61 % (883924)Instruction limit reached!
% 3.22/1.61 % (883924)------------------------------
% 3.22/1.61 % (883924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.61 % (883924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.61 % (883924)CaDiCaL version: 2.1.3
% 3.22/1.61 % (883924)Termination reason: Instruction limit
% 3.22/1.61 % (883924)Termination phase: Saturation
% 3.22/1.61 % (883924)Time elapsed: 0.091 s
% 3.22/1.61 % (883924)Peak memory usage: 102 MB
% 3.22/1.61 % (883924)Instructions burned: 287 (million)
% 3.22/1.61 % (883931)lrs+10_1_sil=32000:urr=on:br=off:random_seed=227996108:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 3.22/1.61 % (883932)lrs+1011_1_sil=32000:sp=occurrence:random_seed=87239265:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 3.22/1.61 % (883931)Refutation not found, incomplete strategy
% 3.22/1.61 % (883931)------------------------------
% 3.22/1.61 % (883931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.61 % (883931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.61 % (883931)CaDiCaL version: 2.1.3
% 3.22/1.61 % (883931)Termination reason: Refutation not found, incomplete strategy
% 3.22/1.61 % (883931)Time elapsed: 0.039 s
% 3.22/1.61 % (883931)Peak memory usage: 98 MB
% 3.22/1.61 % (883931)Instructions burned: 86 (million)
% 3.22/1.61 % (883920)------------------------------
% 3.22/1.61 % (883920)------------------------------
% 3.22/1.61 % (883935)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=3163746188:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 3.22/1.61 % (883932)First to succeed.
% 3.22/1.61 % (883932)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-883911"
% 3.22/1.61 % (883935)Instruction limit reached!
% 3.22/1.61 % (883935)------------------------------
% 3.22/1.61 % (883935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.22/1.61 % (883935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.22/1.61 % (883935)CaDiCaL version: 2.1.3
% 3.22/1.61 % (883935)Termination reason: Instruction limit
% 3.22/1.61 % (883935)Termination phase: Saturation
% 3.22/1.61 % (883935)Time elapsed: 0.061 s
% 3.22/1.61 % (883935)Peak memory usage: 100 MB
% 3.22/1.61 % (883935)Instructions burned: 250 (million)
% 3.22/1.61 % (883937)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=14836346:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 3.22/1.61 % (883937)Also succeeded, but the first one will report.
% 3.22/1.61 % (883931)------------------------------
% 3.22/1.61 % (883931)------------------------------
% 3.22/1.61 % (883939)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2870245608:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 3.22/1.61 % (883932)Refutation found. Thanks to Tanya!
% 3.22/1.61 % SZS status Theorem for theBenchmark
% 3.22/1.61 % SZS output start Proof for theBenchmark
% See solution above
% 6.40/1.82 % (883932)------------------------------
% 6.40/1.82 % (883932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.40/1.82 % (883932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.40/1.82 % (883932)CaDiCaL version: 2.1.3
% 6.40/1.82 % (883932)Termination reason: Refutation
% 6.40/1.82 % (883932)Time elapsed: 0.111 s
% 6.40/1.82 % (883932)Peak memory usage: 100 MB
% 6.40/1.82 % (883932)Instructions burned: 207 (million)
% 6.40/1.82 % (883932)------------------------------
% 6.40/1.82 % (883932)------------------------------
% 6.40/1.82 % (883911)Success in time 0.947 s
% 6.40/1.82 % Vampire exiting
%------------------------------------------------------------------------------