%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR116+18 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:45:49 AM UTC 2026
% Result : Theorem 176.16s 35.81s
% Output : Refutation 176.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 16
% Syntax : Number of formulae : 137 ( 40 unt; 7 def)
% Number of atoms : 1852 ( 0 equ)
% Maximal formula atoms : 217 ( 13 avg)
% Number of connectives : 1970 ( 255 ~; 224 |;1479 &)
% ( 7 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 217 ( 16 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 38 ( 37 usr; 8 prp; 0-2 aty)
% Number of functors : 64 ( 64 usr; 56 con; 0-3 aty)
% Number of variables : 225 ( 0 sgn 184 !; 41 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',member_first) ).
fof(f11,axiom,
! [X0,X1] :
( fact(X0,X1)
=> has_fact_leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',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/Axioms/CSR004+0.ax',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/Axioms/CSR004+0.ax',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/Axioms/CSR004+0.ax',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/Axioms/CSR004+0.ax',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/Axioms/CSR004+0.ax',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_news_1734) ).
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(aufnahmeantrag_1_1,aufnahme_2_1)
& sub(aufnahmeantrag_1_1,antrag_1_1)
& attr(c11805,c11806)
& sub(c11805,k__366nigin_1_1)
& sub(c11806,eigenname_1_1)
& val(c11806,elisabeth_0)
& attr(c11815,c11816)
& attr(c11815,c11817)
& prop(c11815,s__374dafrikanisch_1_1)
& sub(c11815,pr__344sident_1_1)
& sub(c11816,eigenname_1_1)
& val(c11816,nelson_0)
& sub(c11817,familiename_1_1)
& val(c11817,mandela_0)
& ante(c13598,c13616)
& subs(c13598,wahl_1_1)
& attch(c13603,c13598)
& sub(c13605,aufnahmeantrag_1_1)
& agt(c13616,c11815)
& mannr(c13616,direkt_1_1)
& obj(c13616,c13605)
& subs(c13616,stellen_1_3)
& sub(c13631,gl__374ckwunschstelegramm_1_1)
& agt(c8235,c11805)
& obj(c8235,c13631)
& ornt(c8235,c11815)
& subs(c8235,senden_1_2)
& assoc(gl__374ckwunschstelegramm_1_1,gl__374ckwunsch_1_1)
& sub(gl__374ckwunschstelegramm_1_1,depesche_1_1)
& sort(aufnahmeantrag_1_1,ad)
& sort(aufnahmeantrag_1_1,d)
& sort(aufnahmeantrag_1_1,io)
& card(aufnahmeantrag_1_1,int1)
& etype(aufnahmeantrag_1_1,int0)
& fact(aufnahmeantrag_1_1,real)
& gener(aufnahmeantrag_1_1,ge)
& quant(aufnahmeantrag_1_1,one)
& refer(aufnahmeantrag_1_1,refer_c)
& varia(aufnahmeantrag_1_1,varia_c)
& sort(aufnahme_2_1,ad)
& card(aufnahme_2_1,int1)
& etype(aufnahme_2_1,int0)
& fact(aufnahme_2_1,real)
& gener(aufnahme_2_1,ge)
& quant(aufnahme_2_1,one)
& refer(aufnahme_2_1,refer_c)
& varia(aufnahme_2_1,varia_c)
& sort(antrag_1_1,ad)
& sort(antrag_1_1,d)
& sort(antrag_1_1,io)
& card(antrag_1_1,int1)
& etype(antrag_1_1,int0)
& fact(antrag_1_1,real)
& gener(antrag_1_1,ge)
& quant(antrag_1_1,one)
& refer(antrag_1_1,refer_c)
& varia(antrag_1_1,varia_c)
& sort(c11805,d)
& card(c11805,int1)
& etype(c11805,int0)
& fact(c11805,real)
& gener(c11805,sp)
& quant(c11805,one)
& refer(c11805,det)
& varia(c11805,varia_c)
& sort(c11806,na)
& card(c11806,int1)
& etype(c11806,int0)
& fact(c11806,real)
& gener(c11806,sp)
& quant(c11806,one)
& refer(c11806,det)
& varia(c11806,varia_c)
& sort(k__366nigin_1_1,d)
& card(k__366nigin_1_1,int1)
& etype(k__366nigin_1_1,int0)
& fact(k__366nigin_1_1,real)
& gener(k__366nigin_1_1,ge)
& quant(k__366nigin_1_1,one)
& refer(k__366nigin_1_1,refer_c)
& varia(k__366nigin_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(elisabeth_0,fe)
& sort(c11815,d)
& card(c11815,int1)
& etype(c11815,int0)
& fact(c11815,real)
& gener(c11815,sp)
& quant(c11815,one)
& refer(c11815,det)
& varia(c11815,con)
& sort(c11816,na)
& card(c11816,int1)
& etype(c11816,int0)
& fact(c11816,real)
& gener(c11816,sp)
& quant(c11816,one)
& refer(c11816,indet)
& varia(c11816,varia_c)
& sort(c11817,na)
& card(c11817,int1)
& etype(c11817,int0)
& fact(c11817,real)
& gener(c11817,sp)
& quant(c11817,one)
& refer(c11817,indet)
& varia(c11817,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(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(c13598,ad)
& card(c13598,int1)
& etype(c13598,int0)
& fact(c13598,real)
& gener(c13598,sp)
& quant(c13598,one)
& refer(c13598,det)
& varia(c13598,varia_c)
& sort(c13616,da)
& fact(c13616,real)
& gener(c13616,sp)
& 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(c13603,o)
& card(c13603,int1)
& etype(c13603,int0)
& fact(c13603,real)
& gener(c13603,sp)
& quant(c13603,one)
& refer(c13603,det)
& varia(c13603,varia_c)
& sort(c13605,ad)
& sort(c13605,d)
& sort(c13605,io)
& card(c13605,int1)
& etype(c13605,int0)
& fact(c13605,real)
& gener(c13605,sp)
& quant(c13605,one)
& refer(c13605,det)
& varia(c13605,con)
& sort(direkt_1_1,nq)
& sort(stellen_1_3,da)
& fact(stellen_1_3,real)
& gener(stellen_1_3,ge)
& sort(c13631,d)
& sort(c13631,io)
& card(c13631,int1)
& etype(c13631,int0)
& fact(c13631,real)
& gener(c13631,sp)
& quant(c13631,one)
& refer(c13631,indet)
& varia(c13631,varia_c)
& sort(gl__374ckwunschstelegramm_1_1,d)
& sort(gl__374ckwunschstelegramm_1_1,io)
& card(gl__374ckwunschstelegramm_1_1,int1)
& etype(gl__374ckwunschstelegramm_1_1,int0)
& fact(gl__374ckwunschstelegramm_1_1,real)
& gener(gl__374ckwunschstelegramm_1_1,ge)
& quant(gl__374ckwunschstelegramm_1_1,one)
& refer(gl__374ckwunschstelegramm_1_1,refer_c)
& varia(gl__374ckwunschstelegramm_1_1,varia_c)
& sort(c8235,da)
& fact(c8235,real)
& gener(c8235,sp)
& sort(senden_1_2,da)
& fact(senden_1_2,real)
& gener(senden_1_2,ge)
& sort(gl__374ckwunsch_1_1,ad)
& sort(gl__374ckwunsch_1_1,d)
& sort(gl__374ckwunsch_1_1,io)
& card(gl__374ckwunsch_1_1,int1)
& etype(gl__374ckwunsch_1_1,int0)
& fact(gl__374ckwunsch_1_1,real)
& gener(gl__374ckwunsch_1_1,ge)
& quant(gl__374ckwunsch_1_1,one)
& refer(gl__374ckwunsch_1_1,refer_c)
& varia(gl__374ckwunsch_1_1,varia_c)
& sort(depesche_1_1,d)
& sort(depesche_1_1,io)
& card(depesche_1_1,int1)
& etype(depesche_1_1,int0)
& fact(depesche_1_1,real)
& gener(depesche_1_1,ge)
& quant(depesche_1_1,one)
& refer(depesche_1_1,refer_c)
& varia(depesche_1_1,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_news_1734) ).
fof(f10191,plain,
( assoc(aufnahmeantrag_1_1,aufnahme_2_1)
& sub(aufnahmeantrag_1_1,antrag_1_1)
& attr(c11805,c11806)
& sub(c11805,k__366nigin_1_1)
& sub(c11806,eigenname_1_1)
& val(c11806,elisabeth_0)
& attr(c11815,c11816)
& attr(c11815,c11817)
& prop(c11815,s__374dafrikanisch_1_1)
& sub(c11815,pr__344sident_1_1)
& sub(c11816,eigenname_1_1)
& val(c11816,nelson_0)
& sub(c11817,familiename_1_1)
& val(c11817,mandela_0)
& ante(c13598,c13616)
& subs(c13598,wahl_1_1)
& attch(c13603,c13598)
& sub(c13605,aufnahmeantrag_1_1)
& agt(c13616,c11815)
& obj(c13616,c13605)
& subs(c13616,stellen_1_3)
& sub(c13631,gl__374ckwunschstelegramm_1_1)
& agt(c8235,c11805)
& obj(c8235,c13631)
& ornt(c8235,c11815)
& subs(c8235,senden_1_2)
& assoc(gl__374ckwunschstelegramm_1_1,gl__374ckwunsch_1_1)
& sub(gl__374ckwunschstelegramm_1_1,depesche_1_1)
& sort(aufnahmeantrag_1_1,ad)
& sort(aufnahmeantrag_1_1,d)
& sort(aufnahmeantrag_1_1,io)
& card(aufnahmeantrag_1_1,int1)
& etype(aufnahmeantrag_1_1,int0)
& fact(aufnahmeantrag_1_1,real)
& gener(aufnahmeantrag_1_1,ge)
& quant(aufnahmeantrag_1_1,one)
& refer(aufnahmeantrag_1_1,refer_c)
& varia(aufnahmeantrag_1_1,varia_c)
& sort(aufnahme_2_1,ad)
& card(aufnahme_2_1,int1)
& etype(aufnahme_2_1,int0)
& fact(aufnahme_2_1,real)
& gener(aufnahme_2_1,ge)
& quant(aufnahme_2_1,one)
& refer(aufnahme_2_1,refer_c)
& varia(aufnahme_2_1,varia_c)
& sort(antrag_1_1,ad)
& sort(antrag_1_1,d)
& sort(antrag_1_1,io)
& card(antrag_1_1,int1)
& etype(antrag_1_1,int0)
& fact(antrag_1_1,real)
& gener(antrag_1_1,ge)
& quant(antrag_1_1,one)
& refer(antrag_1_1,refer_c)
& varia(antrag_1_1,varia_c)
& sort(c11805,d)
& card(c11805,int1)
& etype(c11805,int0)
& fact(c11805,real)
& gener(c11805,sp)
& quant(c11805,one)
& refer(c11805,det)
& varia(c11805,varia_c)
& sort(c11806,na)
& card(c11806,int1)
& etype(c11806,int0)
& fact(c11806,real)
& gener(c11806,sp)
& quant(c11806,one)
& refer(c11806,det)
& varia(c11806,varia_c)
& sort(k__366nigin_1_1,d)
& card(k__366nigin_1_1,int1)
& etype(k__366nigin_1_1,int0)
& fact(k__366nigin_1_1,real)
& gener(k__366nigin_1_1,ge)
& quant(k__366nigin_1_1,one)
& refer(k__366nigin_1_1,refer_c)
& varia(k__366nigin_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(elisabeth_0,fe)
& sort(c11815,d)
& card(c11815,int1)
& etype(c11815,int0)
& fact(c11815,real)
& gener(c11815,sp)
& quant(c11815,one)
& refer(c11815,det)
& varia(c11815,con)
& sort(c11816,na)
& card(c11816,int1)
& etype(c11816,int0)
& fact(c11816,real)
& gener(c11816,sp)
& quant(c11816,one)
& refer(c11816,indet)
& varia(c11816,varia_c)
& sort(c11817,na)
& card(c11817,int1)
& etype(c11817,int0)
& fact(c11817,real)
& gener(c11817,sp)
& quant(c11817,one)
& refer(c11817,indet)
& varia(c11817,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(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(c13598,ad)
& card(c13598,int1)
& etype(c13598,int0)
& fact(c13598,real)
& gener(c13598,sp)
& quant(c13598,one)
& refer(c13598,det)
& varia(c13598,varia_c)
& sort(c13616,da)
& fact(c13616,real)
& gener(c13616,sp)
& 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(c13603,o)
& card(c13603,int1)
& etype(c13603,int0)
& fact(c13603,real)
& gener(c13603,sp)
& quant(c13603,one)
& refer(c13603,det)
& varia(c13603,varia_c)
& sort(c13605,ad)
& sort(c13605,d)
& sort(c13605,io)
& card(c13605,int1)
& etype(c13605,int0)
& fact(c13605,real)
& gener(c13605,sp)
& quant(c13605,one)
& refer(c13605,det)
& varia(c13605,con)
& sort(direkt_1_1,nq)
& sort(stellen_1_3,da)
& fact(stellen_1_3,real)
& gener(stellen_1_3,ge)
& sort(c13631,d)
& sort(c13631,io)
& card(c13631,int1)
& etype(c13631,int0)
& fact(c13631,real)
& gener(c13631,sp)
& quant(c13631,one)
& refer(c13631,indet)
& varia(c13631,varia_c)
& sort(gl__374ckwunschstelegramm_1_1,d)
& sort(gl__374ckwunschstelegramm_1_1,io)
& card(gl__374ckwunschstelegramm_1_1,int1)
& etype(gl__374ckwunschstelegramm_1_1,int0)
& fact(gl__374ckwunschstelegramm_1_1,real)
& gener(gl__374ckwunschstelegramm_1_1,ge)
& quant(gl__374ckwunschstelegramm_1_1,one)
& refer(gl__374ckwunschstelegramm_1_1,refer_c)
& varia(gl__374ckwunschstelegramm_1_1,varia_c)
& sort(c8235,da)
& fact(c8235,real)
& gener(c8235,sp)
& sort(senden_1_2,da)
& fact(senden_1_2,real)
& gener(senden_1_2,ge)
& sort(gl__374ckwunsch_1_1,ad)
& sort(gl__374ckwunsch_1_1,d)
& sort(gl__374ckwunsch_1_1,io)
& card(gl__374ckwunsch_1_1,int1)
& etype(gl__374ckwunsch_1_1,int0)
& fact(gl__374ckwunsch_1_1,real)
& gener(gl__374ckwunsch_1_1,ge)
& quant(gl__374ckwunsch_1_1,one)
& refer(gl__374ckwunsch_1_1,refer_c)
& varia(gl__374ckwunsch_1_1,varia_c)
& sort(depesche_1_1,d)
& sort(depesche_1_1,io)
& card(depesche_1_1,int1)
& etype(depesche_1_1,int0)
& fact(depesche_1_1,real)
& gener(depesche_1_1,ge)
& quant(depesche_1_1,one)
& refer(depesche_1_1,refer_c)
& varia(depesche_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10192,plain,
( assoc(aufnahmeantrag_1_1,aufnahme_2_1)
& sub(aufnahmeantrag_1_1,antrag_1_1)
& attr(c11805,c11806)
& sub(c11805,k__366nigin_1_1)
& sub(c11806,eigenname_1_1)
& val(c11806,elisabeth_0)
& attr(c11815,c11816)
& attr(c11815,c11817)
& prop(c11815,s__374dafrikanisch_1_1)
& sub(c11815,pr__344sident_1_1)
& sub(c11816,eigenname_1_1)
& val(c11816,nelson_0)
& sub(c11817,familiename_1_1)
& val(c11817,mandela_0)
& subs(c13598,wahl_1_1)
& attch(c13603,c13598)
& sub(c13605,aufnahmeantrag_1_1)
& agt(c13616,c11815)
& obj(c13616,c13605)
& subs(c13616,stellen_1_3)
& sub(c13631,gl__374ckwunschstelegramm_1_1)
& agt(c8235,c11805)
& obj(c8235,c13631)
& ornt(c8235,c11815)
& subs(c8235,senden_1_2)
& assoc(gl__374ckwunschstelegramm_1_1,gl__374ckwunsch_1_1)
& sub(gl__374ckwunschstelegramm_1_1,depesche_1_1)
& sort(aufnahmeantrag_1_1,ad)
& sort(aufnahmeantrag_1_1,d)
& sort(aufnahmeantrag_1_1,io)
& card(aufnahmeantrag_1_1,int1)
& etype(aufnahmeantrag_1_1,int0)
& fact(aufnahmeantrag_1_1,real)
& gener(aufnahmeantrag_1_1,ge)
& quant(aufnahmeantrag_1_1,one)
& refer(aufnahmeantrag_1_1,refer_c)
& varia(aufnahmeantrag_1_1,varia_c)
& sort(aufnahme_2_1,ad)
& card(aufnahme_2_1,int1)
& etype(aufnahme_2_1,int0)
& fact(aufnahme_2_1,real)
& gener(aufnahme_2_1,ge)
& quant(aufnahme_2_1,one)
& refer(aufnahme_2_1,refer_c)
& varia(aufnahme_2_1,varia_c)
& sort(antrag_1_1,ad)
& sort(antrag_1_1,d)
& sort(antrag_1_1,io)
& card(antrag_1_1,int1)
& etype(antrag_1_1,int0)
& fact(antrag_1_1,real)
& gener(antrag_1_1,ge)
& quant(antrag_1_1,one)
& refer(antrag_1_1,refer_c)
& varia(antrag_1_1,varia_c)
& sort(c11805,d)
& card(c11805,int1)
& etype(c11805,int0)
& fact(c11805,real)
& gener(c11805,sp)
& quant(c11805,one)
& refer(c11805,det)
& varia(c11805,varia_c)
& sort(c11806,na)
& card(c11806,int1)
& etype(c11806,int0)
& fact(c11806,real)
& gener(c11806,sp)
& quant(c11806,one)
& refer(c11806,det)
& varia(c11806,varia_c)
& sort(k__366nigin_1_1,d)
& card(k__366nigin_1_1,int1)
& etype(k__366nigin_1_1,int0)
& fact(k__366nigin_1_1,real)
& gener(k__366nigin_1_1,ge)
& quant(k__366nigin_1_1,one)
& refer(k__366nigin_1_1,refer_c)
& varia(k__366nigin_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(elisabeth_0,fe)
& sort(c11815,d)
& card(c11815,int1)
& etype(c11815,int0)
& fact(c11815,real)
& gener(c11815,sp)
& quant(c11815,one)
& refer(c11815,det)
& varia(c11815,con)
& sort(c11816,na)
& card(c11816,int1)
& etype(c11816,int0)
& fact(c11816,real)
& gener(c11816,sp)
& quant(c11816,one)
& refer(c11816,indet)
& varia(c11816,varia_c)
& sort(c11817,na)
& card(c11817,int1)
& etype(c11817,int0)
& fact(c11817,real)
& gener(c11817,sp)
& quant(c11817,one)
& refer(c11817,indet)
& varia(c11817,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(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(c13598,ad)
& card(c13598,int1)
& etype(c13598,int0)
& fact(c13598,real)
& gener(c13598,sp)
& quant(c13598,one)
& refer(c13598,det)
& varia(c13598,varia_c)
& sort(c13616,da)
& fact(c13616,real)
& gener(c13616,sp)
& 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(c13603,o)
& card(c13603,int1)
& etype(c13603,int0)
& fact(c13603,real)
& gener(c13603,sp)
& quant(c13603,one)
& refer(c13603,det)
& varia(c13603,varia_c)
& sort(c13605,ad)
& sort(c13605,d)
& sort(c13605,io)
& card(c13605,int1)
& etype(c13605,int0)
& fact(c13605,real)
& gener(c13605,sp)
& quant(c13605,one)
& refer(c13605,det)
& varia(c13605,con)
& sort(direkt_1_1,nq)
& sort(stellen_1_3,da)
& fact(stellen_1_3,real)
& gener(stellen_1_3,ge)
& sort(c13631,d)
& sort(c13631,io)
& card(c13631,int1)
& etype(c13631,int0)
& fact(c13631,real)
& gener(c13631,sp)
& quant(c13631,one)
& refer(c13631,indet)
& varia(c13631,varia_c)
& sort(gl__374ckwunschstelegramm_1_1,d)
& sort(gl__374ckwunschstelegramm_1_1,io)
& card(gl__374ckwunschstelegramm_1_1,int1)
& etype(gl__374ckwunschstelegramm_1_1,int0)
& fact(gl__374ckwunschstelegramm_1_1,real)
& gener(gl__374ckwunschstelegramm_1_1,ge)
& quant(gl__374ckwunschstelegramm_1_1,one)
& refer(gl__374ckwunschstelegramm_1_1,refer_c)
& varia(gl__374ckwunschstelegramm_1_1,varia_c)
& sort(c8235,da)
& fact(c8235,real)
& gener(c8235,sp)
& sort(senden_1_2,da)
& fact(senden_1_2,real)
& gener(senden_1_2,ge)
& sort(gl__374ckwunsch_1_1,ad)
& sort(gl__374ckwunsch_1_1,d)
& sort(gl__374ckwunsch_1_1,io)
& card(gl__374ckwunsch_1_1,int1)
& etype(gl__374ckwunsch_1_1,int0)
& fact(gl__374ckwunsch_1_1,real)
& gener(gl__374ckwunsch_1_1,ge)
& quant(gl__374ckwunsch_1_1,one)
& refer(gl__374ckwunsch_1_1,refer_c)
& varia(gl__374ckwunsch_1_1,varia_c)
& sort(depesche_1_1,d)
& sort(depesche_1_1,io)
& card(depesche_1_1,int1)
& etype(depesche_1_1,int0)
& fact(depesche_1_1,real)
& gener(depesche_1_1,ge)
& quant(depesche_1_1,one)
& refer(depesche_1_1,refer_c)
& varia(depesche_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10328,plain,
( assoc(aufnahmeantrag_1_1,aufnahme_2_1)
& sub(aufnahmeantrag_1_1,antrag_1_1)
& attr(c11805,c11806)
& sub(c11805,k__366nigin_1_1)
& sub(c11806,eigenname_1_1)
& val(c11806,elisabeth_0)
& attr(c11815,c11816)
& attr(c11815,c11817)
& prop(c11815,s__374dafrikanisch_1_1)
& sub(c11815,pr__344sident_1_1)
& sub(c11816,eigenname_1_1)
& val(c11816,nelson_0)
& sub(c11817,familiename_1_1)
& val(c11817,mandela_0)
& subs(c13598,wahl_1_1)
& attch(c13603,c13598)
& sub(c13605,aufnahmeantrag_1_1)
& agt(c13616,c11815)
& obj(c13616,c13605)
& subs(c13616,stellen_1_3)
& sub(c13631,gl__374ckwunschstelegramm_1_1)
& agt(c8235,c11805)
& obj(c8235,c13631)
& ornt(c8235,c11815)
& subs(c8235,senden_1_2)
& assoc(gl__374ckwunschstelegramm_1_1,gl__374ckwunsch_1_1)
& sub(gl__374ckwunschstelegramm_1_1,depesche_1_1)
& card(aufnahmeantrag_1_1,int1)
& etype(aufnahmeantrag_1_1,int0)
& fact(aufnahmeantrag_1_1,real)
& gener(aufnahmeantrag_1_1,ge)
& quant(aufnahmeantrag_1_1,one)
& refer(aufnahmeantrag_1_1,refer_c)
& varia(aufnahmeantrag_1_1,varia_c)
& card(aufnahme_2_1,int1)
& etype(aufnahme_2_1,int0)
& fact(aufnahme_2_1,real)
& gener(aufnahme_2_1,ge)
& quant(aufnahme_2_1,one)
& refer(aufnahme_2_1,refer_c)
& varia(aufnahme_2_1,varia_c)
& card(antrag_1_1,int1)
& etype(antrag_1_1,int0)
& fact(antrag_1_1,real)
& gener(antrag_1_1,ge)
& quant(antrag_1_1,one)
& refer(antrag_1_1,refer_c)
& varia(antrag_1_1,varia_c)
& card(c11805,int1)
& etype(c11805,int0)
& fact(c11805,real)
& gener(c11805,sp)
& quant(c11805,one)
& refer(c11805,det)
& varia(c11805,varia_c)
& card(c11806,int1)
& etype(c11806,int0)
& fact(c11806,real)
& gener(c11806,sp)
& quant(c11806,one)
& refer(c11806,det)
& varia(c11806,varia_c)
& card(k__366nigin_1_1,int1)
& etype(k__366nigin_1_1,int0)
& fact(k__366nigin_1_1,real)
& gener(k__366nigin_1_1,ge)
& quant(k__366nigin_1_1,one)
& refer(k__366nigin_1_1,refer_c)
& varia(k__366nigin_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(c11815,int1)
& etype(c11815,int0)
& fact(c11815,real)
& gener(c11815,sp)
& quant(c11815,one)
& refer(c11815,det)
& varia(c11815,con)
& card(c11816,int1)
& etype(c11816,int0)
& fact(c11816,real)
& gener(c11816,sp)
& quant(c11816,one)
& refer(c11816,indet)
& varia(c11816,varia_c)
& card(c11817,int1)
& etype(c11817,int0)
& fact(c11817,real)
& gener(c11817,sp)
& quant(c11817,one)
& refer(c11817,indet)
& varia(c11817,varia_c)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& 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(c13598,int1)
& etype(c13598,int0)
& fact(c13598,real)
& gener(c13598,sp)
& quant(c13598,one)
& refer(c13598,det)
& varia(c13598,varia_c)
& fact(c13616,real)
& gener(c13616,sp)
& 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(c13603,int1)
& etype(c13603,int0)
& fact(c13603,real)
& gener(c13603,sp)
& quant(c13603,one)
& refer(c13603,det)
& varia(c13603,varia_c)
& card(c13605,int1)
& etype(c13605,int0)
& fact(c13605,real)
& gener(c13605,sp)
& quant(c13605,one)
& refer(c13605,det)
& varia(c13605,con)
& fact(stellen_1_3,real)
& gener(stellen_1_3,ge)
& card(c13631,int1)
& etype(c13631,int0)
& fact(c13631,real)
& gener(c13631,sp)
& quant(c13631,one)
& refer(c13631,indet)
& varia(c13631,varia_c)
& card(gl__374ckwunschstelegramm_1_1,int1)
& etype(gl__374ckwunschstelegramm_1_1,int0)
& fact(gl__374ckwunschstelegramm_1_1,real)
& gener(gl__374ckwunschstelegramm_1_1,ge)
& quant(gl__374ckwunschstelegramm_1_1,one)
& refer(gl__374ckwunschstelegramm_1_1,refer_c)
& varia(gl__374ckwunschstelegramm_1_1,varia_c)
& fact(c8235,real)
& gener(c8235,sp)
& fact(senden_1_2,real)
& gener(senden_1_2,ge)
& card(gl__374ckwunsch_1_1,int1)
& etype(gl__374ckwunsch_1_1,int0)
& fact(gl__374ckwunsch_1_1,real)
& gener(gl__374ckwunsch_1_1,ge)
& quant(gl__374ckwunsch_1_1,one)
& refer(gl__374ckwunsch_1_1,refer_c)
& varia(gl__374ckwunsch_1_1,varia_c)
& card(depesche_1_1,int1)
& etype(depesche_1_1,int0)
& fact(depesche_1_1,real)
& gener(depesche_1_1,ge)
& quant(depesche_1_1,one)
& refer(depesche_1_1,refer_c)
& varia(depesche_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10192]) ).
fof(f10331,plain,
( assoc(aufnahmeantrag_1_1,aufnahme_2_1)
& sub(aufnahmeantrag_1_1,antrag_1_1)
& attr(c11805,c11806)
& sub(c11805,k__366nigin_1_1)
& sub(c11806,eigenname_1_1)
& val(c11806,elisabeth_0)
& attr(c11815,c11816)
& attr(c11815,c11817)
& prop(c11815,s__374dafrikanisch_1_1)
& sub(c11815,pr__344sident_1_1)
& sub(c11816,eigenname_1_1)
& val(c11816,nelson_0)
& sub(c11817,familiename_1_1)
& val(c11817,mandela_0)
& subs(c13598,wahl_1_1)
& attch(c13603,c13598)
& sub(c13605,aufnahmeantrag_1_1)
& agt(c13616,c11815)
& obj(c13616,c13605)
& subs(c13616,stellen_1_3)
& sub(c13631,gl__374ckwunschstelegramm_1_1)
& agt(c8235,c11805)
& obj(c8235,c13631)
& ornt(c8235,c11815)
& subs(c8235,senden_1_2)
& assoc(gl__374ckwunschstelegramm_1_1,gl__374ckwunsch_1_1)
& sub(gl__374ckwunschstelegramm_1_1,depesche_1_1)
& card(aufnahmeantrag_1_1,int1)
& etype(aufnahmeantrag_1_1,int0)
& fact(aufnahmeantrag_1_1,real)
& gener(aufnahmeantrag_1_1,ge)
& refer(aufnahmeantrag_1_1,refer_c)
& varia(aufnahmeantrag_1_1,varia_c)
& card(aufnahme_2_1,int1)
& etype(aufnahme_2_1,int0)
& fact(aufnahme_2_1,real)
& gener(aufnahme_2_1,ge)
& refer(aufnahme_2_1,refer_c)
& varia(aufnahme_2_1,varia_c)
& card(antrag_1_1,int1)
& etype(antrag_1_1,int0)
& fact(antrag_1_1,real)
& gener(antrag_1_1,ge)
& refer(antrag_1_1,refer_c)
& varia(antrag_1_1,varia_c)
& card(c11805,int1)
& etype(c11805,int0)
& fact(c11805,real)
& gener(c11805,sp)
& refer(c11805,det)
& varia(c11805,varia_c)
& card(c11806,int1)
& etype(c11806,int0)
& fact(c11806,real)
& gener(c11806,sp)
& refer(c11806,det)
& varia(c11806,varia_c)
& card(k__366nigin_1_1,int1)
& etype(k__366nigin_1_1,int0)
& fact(k__366nigin_1_1,real)
& gener(k__366nigin_1_1,ge)
& refer(k__366nigin_1_1,refer_c)
& varia(k__366nigin_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(c11815,int1)
& etype(c11815,int0)
& fact(c11815,real)
& gener(c11815,sp)
& refer(c11815,det)
& varia(c11815,con)
& card(c11816,int1)
& etype(c11816,int0)
& fact(c11816,real)
& gener(c11816,sp)
& refer(c11816,indet)
& varia(c11816,varia_c)
& card(c11817,int1)
& etype(c11817,int0)
& fact(c11817,real)
& gener(c11817,sp)
& refer(c11817,indet)
& varia(c11817,varia_c)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& 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(c13598,int1)
& etype(c13598,int0)
& fact(c13598,real)
& gener(c13598,sp)
& refer(c13598,det)
& varia(c13598,varia_c)
& fact(c13616,real)
& gener(c13616,sp)
& 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(c13603,int1)
& etype(c13603,int0)
& fact(c13603,real)
& gener(c13603,sp)
& refer(c13603,det)
& varia(c13603,varia_c)
& card(c13605,int1)
& etype(c13605,int0)
& fact(c13605,real)
& gener(c13605,sp)
& refer(c13605,det)
& varia(c13605,con)
& fact(stellen_1_3,real)
& gener(stellen_1_3,ge)
& card(c13631,int1)
& etype(c13631,int0)
& fact(c13631,real)
& gener(c13631,sp)
& refer(c13631,indet)
& varia(c13631,varia_c)
& card(gl__374ckwunschstelegramm_1_1,int1)
& etype(gl__374ckwunschstelegramm_1_1,int0)
& fact(gl__374ckwunschstelegramm_1_1,real)
& gener(gl__374ckwunschstelegramm_1_1,ge)
& refer(gl__374ckwunschstelegramm_1_1,refer_c)
& varia(gl__374ckwunschstelegramm_1_1,varia_c)
& fact(c8235,real)
& gener(c8235,sp)
& fact(senden_1_2,real)
& gener(senden_1_2,ge)
& card(gl__374ckwunsch_1_1,int1)
& etype(gl__374ckwunsch_1_1,int0)
& fact(gl__374ckwunsch_1_1,real)
& gener(gl__374ckwunsch_1_1,ge)
& refer(gl__374ckwunsch_1_1,refer_c)
& varia(gl__374ckwunsch_1_1,varia_c)
& card(depesche_1_1,int1)
& etype(depesche_1_1,int0)
& fact(depesche_1_1,real)
& gener(depesche_1_1,ge)
& refer(depesche_1_1,refer_c)
& varia(depesche_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10328]) ).
fof(f10334,plain,
( assoc(aufnahmeantrag_1_1,aufnahme_2_1)
& sub(aufnahmeantrag_1_1,antrag_1_1)
& attr(c11805,c11806)
& sub(c11805,k__366nigin_1_1)
& sub(c11806,eigenname_1_1)
& val(c11806,elisabeth_0)
& attr(c11815,c11816)
& attr(c11815,c11817)
& prop(c11815,s__374dafrikanisch_1_1)
& sub(c11815,pr__344sident_1_1)
& sub(c11816,eigenname_1_1)
& val(c11816,nelson_0)
& sub(c11817,familiename_1_1)
& val(c11817,mandela_0)
& subs(c13598,wahl_1_1)
& attch(c13603,c13598)
& sub(c13605,aufnahmeantrag_1_1)
& agt(c13616,c11815)
& obj(c13616,c13605)
& subs(c13616,stellen_1_3)
& sub(c13631,gl__374ckwunschstelegramm_1_1)
& agt(c8235,c11805)
& obj(c8235,c13631)
& ornt(c8235,c11815)
& subs(c8235,senden_1_2)
& assoc(gl__374ckwunschstelegramm_1_1,gl__374ckwunsch_1_1)
& sub(gl__374ckwunschstelegramm_1_1,depesche_1_1)
& etype(aufnahmeantrag_1_1,int0)
& fact(aufnahmeantrag_1_1,real)
& gener(aufnahmeantrag_1_1,ge)
& refer(aufnahmeantrag_1_1,refer_c)
& varia(aufnahmeantrag_1_1,varia_c)
& etype(aufnahme_2_1,int0)
& fact(aufnahme_2_1,real)
& gener(aufnahme_2_1,ge)
& refer(aufnahme_2_1,refer_c)
& varia(aufnahme_2_1,varia_c)
& etype(antrag_1_1,int0)
& fact(antrag_1_1,real)
& gener(antrag_1_1,ge)
& refer(antrag_1_1,refer_c)
& varia(antrag_1_1,varia_c)
& etype(c11805,int0)
& fact(c11805,real)
& gener(c11805,sp)
& refer(c11805,det)
& varia(c11805,varia_c)
& etype(c11806,int0)
& fact(c11806,real)
& gener(c11806,sp)
& refer(c11806,det)
& varia(c11806,varia_c)
& etype(k__366nigin_1_1,int0)
& fact(k__366nigin_1_1,real)
& gener(k__366nigin_1_1,ge)
& refer(k__366nigin_1_1,refer_c)
& varia(k__366nigin_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(c11815,int0)
& fact(c11815,real)
& gener(c11815,sp)
& refer(c11815,det)
& varia(c11815,con)
& etype(c11816,int0)
& fact(c11816,real)
& gener(c11816,sp)
& refer(c11816,indet)
& varia(c11816,varia_c)
& etype(c11817,int0)
& fact(c11817,real)
& gener(c11817,sp)
& refer(c11817,indet)
& varia(c11817,varia_c)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& etype(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(c13598,int0)
& fact(c13598,real)
& gener(c13598,sp)
& refer(c13598,det)
& varia(c13598,varia_c)
& fact(c13616,real)
& gener(c13616,sp)
& 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(c13603,int0)
& fact(c13603,real)
& gener(c13603,sp)
& refer(c13603,det)
& varia(c13603,varia_c)
& etype(c13605,int0)
& fact(c13605,real)
& gener(c13605,sp)
& refer(c13605,det)
& varia(c13605,con)
& fact(stellen_1_3,real)
& gener(stellen_1_3,ge)
& etype(c13631,int0)
& fact(c13631,real)
& gener(c13631,sp)
& refer(c13631,indet)
& varia(c13631,varia_c)
& etype(gl__374ckwunschstelegramm_1_1,int0)
& fact(gl__374ckwunschstelegramm_1_1,real)
& gener(gl__374ckwunschstelegramm_1_1,ge)
& refer(gl__374ckwunschstelegramm_1_1,refer_c)
& varia(gl__374ckwunschstelegramm_1_1,varia_c)
& fact(c8235,real)
& gener(c8235,sp)
& fact(senden_1_2,real)
& gener(senden_1_2,ge)
& etype(gl__374ckwunsch_1_1,int0)
& fact(gl__374ckwunsch_1_1,real)
& gener(gl__374ckwunsch_1_1,ge)
& refer(gl__374ckwunsch_1_1,refer_c)
& varia(gl__374ckwunsch_1_1,varia_c)
& etype(depesche_1_1,int0)
& fact(depesche_1_1,real)
& gener(depesche_1_1,ge)
& refer(depesche_1_1,refer_c)
& varia(depesche_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10331]) ).
fof(f10337,plain,
( assoc(aufnahmeantrag_1_1,aufnahme_2_1)
& sub(aufnahmeantrag_1_1,antrag_1_1)
& attr(c11805,c11806)
& sub(c11805,k__366nigin_1_1)
& sub(c11806,eigenname_1_1)
& val(c11806,elisabeth_0)
& attr(c11815,c11816)
& attr(c11815,c11817)
& prop(c11815,s__374dafrikanisch_1_1)
& sub(c11815,pr__344sident_1_1)
& sub(c11816,eigenname_1_1)
& val(c11816,nelson_0)
& sub(c11817,familiename_1_1)
& val(c11817,mandela_0)
& subs(c13598,wahl_1_1)
& attch(c13603,c13598)
& sub(c13605,aufnahmeantrag_1_1)
& agt(c13616,c11815)
& obj(c13616,c13605)
& subs(c13616,stellen_1_3)
& sub(c13631,gl__374ckwunschstelegramm_1_1)
& agt(c8235,c11805)
& obj(c8235,c13631)
& ornt(c8235,c11815)
& subs(c8235,senden_1_2)
& assoc(gl__374ckwunschstelegramm_1_1,gl__374ckwunsch_1_1)
& sub(gl__374ckwunschstelegramm_1_1,depesche_1_1)
& etype(aufnahmeantrag_1_1,int0)
& fact(aufnahmeantrag_1_1,real)
& gener(aufnahmeantrag_1_1,ge)
& varia(aufnahmeantrag_1_1,varia_c)
& etype(aufnahme_2_1,int0)
& fact(aufnahme_2_1,real)
& gener(aufnahme_2_1,ge)
& varia(aufnahme_2_1,varia_c)
& etype(antrag_1_1,int0)
& fact(antrag_1_1,real)
& gener(antrag_1_1,ge)
& varia(antrag_1_1,varia_c)
& etype(c11805,int0)
& fact(c11805,real)
& gener(c11805,sp)
& varia(c11805,varia_c)
& etype(c11806,int0)
& fact(c11806,real)
& gener(c11806,sp)
& varia(c11806,varia_c)
& etype(k__366nigin_1_1,int0)
& fact(k__366nigin_1_1,real)
& gener(k__366nigin_1_1,ge)
& varia(k__366nigin_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(c11815,int0)
& fact(c11815,real)
& gener(c11815,sp)
& varia(c11815,con)
& etype(c11816,int0)
& fact(c11816,real)
& gener(c11816,sp)
& varia(c11816,varia_c)
& etype(c11817,int0)
& fact(c11817,real)
& gener(c11817,sp)
& varia(c11817,varia_c)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& varia(pr__344sident_1_1,varia_c)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& varia(familiename_1_1,varia_c)
& etype(c13598,int0)
& fact(c13598,real)
& gener(c13598,sp)
& varia(c13598,varia_c)
& fact(c13616,real)
& gener(c13616,sp)
& etype(wahl_1_1,int0)
& fact(wahl_1_1,real)
& gener(wahl_1_1,ge)
& varia(wahl_1_1,varia_c)
& etype(c13603,int0)
& fact(c13603,real)
& gener(c13603,sp)
& varia(c13603,varia_c)
& etype(c13605,int0)
& fact(c13605,real)
& gener(c13605,sp)
& varia(c13605,con)
& fact(stellen_1_3,real)
& gener(stellen_1_3,ge)
& etype(c13631,int0)
& fact(c13631,real)
& gener(c13631,sp)
& varia(c13631,varia_c)
& etype(gl__374ckwunschstelegramm_1_1,int0)
& fact(gl__374ckwunschstelegramm_1_1,real)
& gener(gl__374ckwunschstelegramm_1_1,ge)
& varia(gl__374ckwunschstelegramm_1_1,varia_c)
& fact(c8235,real)
& gener(c8235,sp)
& fact(senden_1_2,real)
& gener(senden_1_2,ge)
& etype(gl__374ckwunsch_1_1,int0)
& fact(gl__374ckwunsch_1_1,real)
& gener(gl__374ckwunsch_1_1,ge)
& varia(gl__374ckwunsch_1_1,varia_c)
& etype(depesche_1_1,int0)
& fact(depesche_1_1,real)
& gener(depesche_1_1,ge)
& varia(depesche_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10334]) ).
fof(f10342,plain,
( assoc(aufnahmeantrag_1_1,aufnahme_2_1)
& sub(aufnahmeantrag_1_1,antrag_1_1)
& attr(c11805,c11806)
& sub(c11805,k__366nigin_1_1)
& sub(c11806,eigenname_1_1)
& val(c11806,elisabeth_0)
& attr(c11815,c11816)
& attr(c11815,c11817)
& prop(c11815,s__374dafrikanisch_1_1)
& sub(c11815,pr__344sident_1_1)
& sub(c11816,eigenname_1_1)
& val(c11816,nelson_0)
& sub(c11817,familiename_1_1)
& val(c11817,mandela_0)
& subs(c13598,wahl_1_1)
& attch(c13603,c13598)
& sub(c13605,aufnahmeantrag_1_1)
& agt(c13616,c11815)
& obj(c13616,c13605)
& subs(c13616,stellen_1_3)
& sub(c13631,gl__374ckwunschstelegramm_1_1)
& agt(c8235,c11805)
& obj(c8235,c13631)
& ornt(c8235,c11815)
& subs(c8235,senden_1_2)
& assoc(gl__374ckwunschstelegramm_1_1,gl__374ckwunsch_1_1)
& sub(gl__374ckwunschstelegramm_1_1,depesche_1_1)
& etype(aufnahmeantrag_1_1,int0)
& fact(aufnahmeantrag_1_1,real)
& gener(aufnahmeantrag_1_1,ge)
& etype(aufnahme_2_1,int0)
& fact(aufnahme_2_1,real)
& gener(aufnahme_2_1,ge)
& etype(antrag_1_1,int0)
& fact(antrag_1_1,real)
& gener(antrag_1_1,ge)
& etype(c11805,int0)
& fact(c11805,real)
& gener(c11805,sp)
& etype(c11806,int0)
& fact(c11806,real)
& gener(c11806,sp)
& etype(k__366nigin_1_1,int0)
& fact(k__366nigin_1_1,real)
& gener(k__366nigin_1_1,ge)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& etype(c11815,int0)
& fact(c11815,real)
& gener(c11815,sp)
& etype(c11816,int0)
& fact(c11816,real)
& gener(c11816,sp)
& etype(c11817,int0)
& fact(c11817,real)
& gener(c11817,sp)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& etype(c13598,int0)
& fact(c13598,real)
& gener(c13598,sp)
& fact(c13616,real)
& gener(c13616,sp)
& etype(wahl_1_1,int0)
& fact(wahl_1_1,real)
& gener(wahl_1_1,ge)
& etype(c13603,int0)
& fact(c13603,real)
& gener(c13603,sp)
& etype(c13605,int0)
& fact(c13605,real)
& gener(c13605,sp)
& fact(stellen_1_3,real)
& gener(stellen_1_3,ge)
& etype(c13631,int0)
& fact(c13631,real)
& gener(c13631,sp)
& etype(gl__374ckwunschstelegramm_1_1,int0)
& fact(gl__374ckwunschstelegramm_1_1,real)
& gener(gl__374ckwunschstelegramm_1_1,ge)
& fact(c8235,real)
& gener(c8235,sp)
& fact(senden_1_2,real)
& gener(senden_1_2,ge)
& etype(gl__374ckwunsch_1_1,int0)
& fact(gl__374ckwunsch_1_1,real)
& gener(gl__374ckwunsch_1_1,ge)
& etype(depesche_1_1,int0)
& fact(depesche_1_1,real)
& gener(depesche_1_1,ge) ),
inference(pure_predicate_removal,[],[f10337]) ).
fof(f10347,plain,
( assoc(aufnahmeantrag_1_1,aufnahme_2_1)
& sub(aufnahmeantrag_1_1,antrag_1_1)
& attr(c11805,c11806)
& sub(c11805,k__366nigin_1_1)
& sub(c11806,eigenname_1_1)
& val(c11806,elisabeth_0)
& attr(c11815,c11816)
& attr(c11815,c11817)
& prop(c11815,s__374dafrikanisch_1_1)
& sub(c11815,pr__344sident_1_1)
& sub(c11816,eigenname_1_1)
& val(c11816,nelson_0)
& sub(c11817,familiename_1_1)
& val(c11817,mandela_0)
& subs(c13598,wahl_1_1)
& attch(c13603,c13598)
& sub(c13605,aufnahmeantrag_1_1)
& agt(c13616,c11815)
& obj(c13616,c13605)
& subs(c13616,stellen_1_3)
& sub(c13631,gl__374ckwunschstelegramm_1_1)
& agt(c8235,c11805)
& obj(c8235,c13631)
& ornt(c8235,c11815)
& subs(c8235,senden_1_2)
& assoc(gl__374ckwunschstelegramm_1_1,gl__374ckwunsch_1_1)
& sub(gl__374ckwunschstelegramm_1_1,depesche_1_1)
& etype(aufnahmeantrag_1_1,int0)
& fact(aufnahmeantrag_1_1,real)
& etype(aufnahme_2_1,int0)
& fact(aufnahme_2_1,real)
& etype(antrag_1_1,int0)
& fact(antrag_1_1,real)
& etype(c11805,int0)
& fact(c11805,real)
& etype(c11806,int0)
& fact(c11806,real)
& etype(k__366nigin_1_1,int0)
& fact(k__366nigin_1_1,real)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& etype(c11815,int0)
& fact(c11815,real)
& etype(c11816,int0)
& fact(c11816,real)
& etype(c11817,int0)
& fact(c11817,real)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& etype(c13598,int0)
& fact(c13598,real)
& fact(c13616,real)
& etype(wahl_1_1,int0)
& fact(wahl_1_1,real)
& etype(c13603,int0)
& fact(c13603,real)
& etype(c13605,int0)
& fact(c13605,real)
& fact(stellen_1_3,real)
& etype(c13631,int0)
& fact(c13631,real)
& etype(gl__374ckwunschstelegramm_1_1,int0)
& fact(gl__374ckwunschstelegramm_1_1,real)
& fact(c8235,real)
& fact(senden_1_2,real)
& etype(gl__374ckwunsch_1_1,int0)
& fact(gl__374ckwunsch_1_1,real)
& etype(depesche_1_1,int0)
& fact(depesche_1_1,real) ),
inference(pure_predicate_removal,[],[f10342]) ).
fof(f10351,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f10400,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(f10401,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,[],[f10400]) ).
fof(f10509,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(f10510,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,[],[f10509]) ).
fof(f10515,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(f10516,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,[],[f10515]) ).
fof(f10519,plain,
! [X0,X1,X2] :
( ? [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) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(ennf_transformation,[],[f161]) ).
fof(f10520,plain,
! [X0,X1,X2] :
( ? [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) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(flattening,[],[f10519]) ).
fof(f10552,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(f10555,plain,
! [X0,X1] :
( ( loc(sK2(X0,X1),X0)
& obj(sK2(X0,X1),X1)
& subs(sK2(X0,X1),geben_1_1) )
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X2,sK2(X0,X1))],[f10401]) ).
fof(f10590,plain,
! [X0,X1,X2] :
( ( in(sK49(X0,X2),sK47(X0,X2))
& attr(sK47(X0,X2),sK48(X0,X2))
& loc(X0,sK49(X0,X2))
& sub(sK47(X0,X2),land_1_1)
& sub(sK48(X0,X2),name_1_1)
& val(sK48(X0,X2),X2) )
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47,sK48,sK49]),skolemize(X3,sK47(X0,X2)),skolemize(X4,sK48(X0,X2)),skolemize(X5,sK49(X0,X2))],[f10510]) ).
fof(f10591,plain,
! [X0,X1,X2] :
( ( arg1(sK50(X2),X2)
& arg2(sK50(X2),X2)
& subs(sK50(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,[sK50]),skolemize(X3,sK50(X2))],[f10516]) ).
fof(f10593,plain,
! [X0,X1,X2] :
( ( arg1(sK53(X0,X1,X2),X1)
& arg2(sK53(X0,X1,X2),X2)
& hsit(X0,sK52(X0,X1,X2))
& mcont(sK52(X0,X1,X2),sK53(X0,X1,X2))
& obj(sK52(X0,X1,X2),X1)
& subr(sK53(X0,X1,X2),rprs_0)
& subs(sK52(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,[sK52,sK53]),skolemize(X3,sK52(X0,X1,X2)),skolemize(X4,sK53(X0,X1,X2))],[f10520]) ).
fof(f10601,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[],[f1]) ).
fof(f10603,plain,
! [X0,X1] :
( ~ fact(X0,X1)
| has_fact_leq(X0,X1) ),
inference(cnf_transformation,[],[f10351]) ).
fof(f10687,plain,
! [X0,X1] :
( ~ loc(X1,X0)
| ~ has_fact_leq(X1,real)
| obj(sK2(X0,X1),X1) ),
inference(cnf_transformation,[],[f10555]) ).
fof(f10853,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| val(sK48(X0,X2),X2) ),
inference(cnf_transformation,[],[f10590]) ).
fof(f10854,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| sub(sK48(X0,X2),name_1_1) ),
inference(cnf_transformation,[],[f10590]) ).
fof(f10856,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| loc(X0,sK49(X0,X2)) ),
inference(cnf_transformation,[],[f10590]) ).
fof(f10857,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| attr(sK47(X0,X2),sK48(X0,X2)) ),
inference(cnf_transformation,[],[f10590]) ).
fof(f10858,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| in(sK49(X0,X2),sK47(X0,X2)) ),
inference(cnf_transformation,[],[f10590]) ).
fof(f10861,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0)
| subs(sK50(X2),hei__337en_1_1)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10591]) ).
fof(f10862,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0)
| arg2(sK50(X2),X2)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10591]) ).
fof(f10863,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0)
| arg1(sK50(X2),X2)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10591]) ).
fof(f10869,plain,
! [X2,X0,X1] :
( ~ subs(X0,hei__337en_1_1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| subr(sK53(X0,X1,X2),rprs_0) ),
inference(cnf_transformation,[],[f10593]) ).
fof(f10873,plain,
! [X2,X0,X1] :
( ~ subs(X0,hei__337en_1_1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| arg2(sK53(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f10593]) ).
fof(f10874,plain,
! [X2,X0,X1] :
( ~ subs(X0,hei__337en_1_1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| arg1(sK53(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f10593]) ).
fof(f19790,plain,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
inference(cnf_transformation,[],[f9161]) ).
fof(f20817,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,[],[f10552]) ).
fof(f20846,plain,
fact(c11815,real),
inference(cnf_transformation,[],[f10347]) ).
fof(f20875,plain,
val(c11817,mandela_0),
inference(cnf_transformation,[],[f10347]) ).
fof(f20876,plain,
sub(c11817,familiename_1_1),
inference(cnf_transformation,[],[f10347]) ).
fof(f20877,plain,
val(c11816,nelson_0),
inference(cnf_transformation,[],[f10347]) ).
fof(f20878,plain,
sub(c11816,eigenname_1_1),
inference(cnf_transformation,[],[f10347]) ).
fof(f20879,plain,
sub(c11815,pr__344sident_1_1),
inference(cnf_transformation,[],[f10347]) ).
fof(f20880,plain,
prop(c11815,s__374dafrikanisch_1_1),
inference(cnf_transformation,[],[f10347]) ).
fof(f20881,plain,
attr(c11815,c11817),
inference(cnf_transformation,[],[f10347]) ).
fof(f20882,plain,
attr(c11815,c11816),
inference(cnf_transformation,[],[f10347]) ).
fof(f20890,definition,
( spl63_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,[spl63_1])],[avatar_definition]) ).
fof(f20891,plain,
( ! [X2,X3,X0,X1,X8,X9,X4] :
( ~ arg2(X3,X4)
| ~ 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)
| ~ arg1(X3,X0) )
| ~ spl63_1 ),
inference(avatar_component_clause,[],[f20890]) ).
fof(f20893,definition,
( spl63_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,[spl63_2])],[avatar_definition]) ).
fof(f20894,plain,
( ! [X6,X7,X5] :
( ~ attr(X6,X7)
| ~ val(X7,s__374dafrika_0)
| ~ sub(X7,name_1_1)
| ~ in(X5,X6) )
| ~ spl63_2 ),
inference(avatar_component_clause,[],[f20893]) ).
fof(f20895,plain,
( spl63_1
| spl63_2 ),
inference(avatar_split_clause,[],[f20817,f20893,f20890]) ).
fof(f20942,plain,
has_fact_leq(c11815,real),
inference(resolution,[],[f10603,f20846]) ).
fof(f60210,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| val(sK48(X0,s__374dafrika_0),s__374dafrika_0) ),
inference(resolution,[],[f10853,f19790]) ).
fof(f60396,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| sub(sK48(X0,s__374dafrika_0),name_1_1) ),
inference(resolution,[],[f10854,f19790]) ).
fof(f60768,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| loc(X0,sK49(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10856,f19790]) ).
fof(f63143,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| attr(sK47(X0,s__374dafrika_0),sK48(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10857,f19790]) ).
fof(f63329,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| in(sK49(X0,s__374dafrika_0),sK47(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10858,f19790]) ).
fof(f71655,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| subs(sK50(X0),hei__337en_1_1)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10861,f10601]) ).
fof(f71657,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| arg2(sK50(X0),X0)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10862,f10601]) ).
fof(f71659,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| arg1(sK50(X0),X0)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10863,f10601]) ).
fof(f72789,plain,
val(sK48(c11815,s__374dafrika_0),s__374dafrika_0),
inference(resolution,[],[f60210,f20880]) ).
fof(f72794,plain,
sub(sK48(c11815,s__374dafrika_0),name_1_1),
inference(resolution,[],[f60396,f20880]) ).
fof(f72827,plain,
loc(c11815,sK49(c11815,s__374dafrika_0)),
inference(resolution,[],[f60768,f20880]) ).
fof(f72835,plain,
( ~ has_fact_leq(c11815,real)
| obj(sK2(sK49(c11815,s__374dafrika_0),c11815),c11815) ),
inference(resolution,[],[f72827,f10687]) ).
fof(f72846,plain,
obj(sK2(sK49(c11815,s__374dafrika_0),c11815),c11815),
inference(forward_subsumption_resolution,[],[f72835,f20942]) ).
fof(f73049,plain,
attr(sK47(c11815,s__374dafrika_0),sK48(c11815,s__374dafrika_0)),
inference(resolution,[],[f63143,f20880]) ).
fof(f73050,plain,
( ! [X0] :
( ~ val(sK48(c11815,s__374dafrika_0),s__374dafrika_0)
| ~ sub(sK48(c11815,s__374dafrika_0),name_1_1)
| ~ in(X0,sK47(c11815,s__374dafrika_0)) )
| ~ spl63_2 ),
inference(resolution,[],[f73049,f20894]) ).
fof(f73051,plain,
( ! [X0] :
( ~ sub(sK48(c11815,s__374dafrika_0),name_1_1)
| ~ in(X0,sK47(c11815,s__374dafrika_0)) )
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f73050,f72789]) ).
fof(f73052,plain,
( ! [X0] : ~ in(X0,sK47(c11815,s__374dafrika_0))
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f73051,f72794]) ).
fof(f73053,plain,
in(sK49(c11815,s__374dafrika_0),sK47(c11815,s__374dafrika_0)),
inference(resolution,[],[f63329,f20880]) ).
fof(f73054,plain,
( $false
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f73053,f73052]) ).
fof(f73055,plain,
~ spl63_2,
inference(avatar_contradiction_clause,[],[f73054]) ).
fof(f76561,plain,
! [X0] :
( ~ attr(X0,c11816)
| subs(sK50(X0),hei__337en_1_1) ),
inference(resolution,[],[f71655,f20878]) ).
fof(f76651,plain,
! [X0] :
( ~ attr(X0,c11816)
| arg2(sK50(X0),X0) ),
inference(resolution,[],[f71657,f20878]) ).
fof(f76741,plain,
! [X0] :
( ~ attr(X0,c11816)
| arg1(sK50(X0),X0) ),
inference(resolution,[],[f71659,f20878]) ).
fof(f85419,plain,
subs(sK50(c11815),hei__337en_1_1),
inference(resolution,[],[f76561,f20882]) ).
fof(f85421,plain,
! [X0,X1] :
( ~ arg2(sK50(c11815),X1)
| ~ arg1(sK50(c11815),X0)
| subr(sK53(sK50(c11815),X0,X1),rprs_0) ),
inference(resolution,[],[f85419,f10869]) ).
fof(f85425,plain,
! [X0,X1] :
( ~ arg2(sK50(c11815),X1)
| ~ arg1(sK50(c11815),X0)
| arg2(sK53(sK50(c11815),X0,X1),X1) ),
inference(resolution,[],[f85419,f10873]) ).
fof(f85426,plain,
! [X0,X1] :
( ~ arg2(sK50(c11815),X1)
| ~ arg1(sK50(c11815),X0)
| arg1(sK53(sK50(c11815),X0,X1),X0) ),
inference(resolution,[],[f85419,f10874]) ).
fof(f85460,plain,
arg2(sK50(c11815),c11815),
inference(resolution,[],[f76651,f20882]) ).
fof(f85463,definition,
( spl63_3190
<=> ! [X2] : ~ sub(c11815,X2) ),
introduced(definition,[new_symbols(definition,[spl63_3190])],[avatar_definition]) ).
fof(f85464,plain,
( ! [X2] : ~ sub(c11815,X2)
| ~ spl63_3190 ),
inference(avatar_component_clause,[],[f85463]) ).
fof(f85474,plain,
arg1(sK50(c11815),c11815),
inference(resolution,[],[f76741,f20882]) ).
fof(f87117,plain,
! [X0] :
( ~ arg1(sK50(c11815),X0)
| subr(sK53(sK50(c11815),X0,c11815),rprs_0) ),
inference(resolution,[],[f85421,f85460]) ).
fof(f87118,plain,
subr(sK53(sK50(c11815),c11815,c11815),rprs_0),
inference(resolution,[],[f87117,f85474]) ).
fof(f87123,plain,
! [X0] :
( ~ arg1(sK50(c11815),X0)
| arg2(sK53(sK50(c11815),X0,c11815),c11815) ),
inference(resolution,[],[f85425,f85460]) ).
fof(f87124,plain,
arg2(sK53(sK50(c11815),c11815,c11815),c11815),
inference(resolution,[],[f87123,f85474]) ).
fof(f87126,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ val(X0,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(sK53(sK50(c11815),c11815,c11815),rprs_0)
| ~ sub(c11815,X2)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X3,X4)
| ~ attr(X4,X0)
| ~ attr(X4,X1)
| ~ arg1(sK53(sK50(c11815),c11815,c11815),X4) )
| ~ spl63_1 ),
inference(resolution,[],[f87124,f20891]) ).
fof(f87127,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ val(X0,nelson_0)
| ~ val(X1,mandela_0)
| ~ sub(c11815,X2)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X3,X4)
| ~ attr(X4,X0)
| ~ attr(X4,X1)
| ~ arg1(sK53(sK50(c11815),c11815,c11815),X4) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f87126,f87118]) ).
fof(f87129,definition,
( spl63_3313
<=> ! [X4,X0,X3,X1] :
( ~ val(X0,nelson_0)
| ~ arg1(sK53(sK50(c11815),c11815,c11815),X4)
| ~ attr(X4,X1)
| ~ obj(X3,X4)
| ~ attr(X4,X0)
| ~ sub(X0,eigenname_1_1)
| ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1) ) ),
introduced(definition,[new_symbols(definition,[spl63_3313])],[avatar_definition]) ).
fof(f87130,plain,
( ! [X3,X0,X1,X4] :
( ~ arg1(sK53(sK50(c11815),c11815,c11815),X4)
| ~ val(X0,nelson_0)
| ~ attr(X4,X1)
| ~ obj(X3,X4)
| ~ attr(X4,X0)
| ~ sub(X0,eigenname_1_1)
| ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1) )
| ~ spl63_3313 ),
inference(avatar_component_clause,[],[f87129]) ).
fof(f87131,plain,
( spl63_3190
| spl63_3313
| ~ spl63_1 ),
inference(avatar_split_clause,[],[f87127,f20890,f87129,f85463]) ).
fof(f87132,plain,
( $false
| ~ spl63_3190 ),
inference(resolution,[],[f85464,f20879]) ).
fof(f87133,plain,
~ spl63_3190,
inference(avatar_contradiction_clause,[],[f87132]) ).
fof(f87135,plain,
! [X0] :
( ~ arg1(sK50(c11815),X0)
| arg1(sK53(sK50(c11815),X0,c11815),X0) ),
inference(resolution,[],[f85426,f85460]) ).
fof(f87136,plain,
arg1(sK53(sK50(c11815),c11815,c11815),c11815),
inference(resolution,[],[f87135,f85474]) ).
fof(f87137,plain,
( ! [X2,X0,X1] :
( ~ val(X0,nelson_0)
| ~ attr(c11815,X1)
| ~ obj(X2,c11815)
| ~ attr(c11815,X0)
| ~ sub(X0,eigenname_1_1)
| ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1) )
| ~ spl63_3313 ),
inference(resolution,[],[f87136,f87130]) ).
fof(f87139,definition,
( spl63_3314
<=> ! [X2] : ~ obj(X2,c11815) ),
introduced(definition,[new_symbols(definition,[spl63_3314])],[avatar_definition]) ).
fof(f87140,plain,
( ! [X2] : ~ obj(X2,c11815)
| ~ spl63_3314 ),
inference(avatar_component_clause,[],[f87139]) ).
fof(f87142,definition,
( spl63_3315
<=> ! [X1] :
( ~ attr(c11815,X1)
| ~ sub(X1,familiename_1_1)
| ~ val(X1,mandela_0) ) ),
introduced(definition,[new_symbols(definition,[spl63_3315])],[avatar_definition]) ).
fof(f87143,plain,
( ! [X1] :
( ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1)
| ~ attr(c11815,X1) )
| ~ spl63_3315 ),
inference(avatar_component_clause,[],[f87142]) ).
fof(f87145,definition,
( spl63_3316
<=> ! [X0] :
( ~ val(X0,nelson_0)
| ~ sub(X0,eigenname_1_1)
| ~ attr(c11815,X0) ) ),
introduced(definition,[new_symbols(definition,[spl63_3316])],[avatar_definition]) ).
fof(f87146,plain,
( ! [X0] :
( ~ attr(c11815,X0)
| ~ sub(X0,eigenname_1_1)
| ~ val(X0,nelson_0) )
| ~ spl63_3316 ),
inference(avatar_component_clause,[],[f87145]) ).
fof(f87147,plain,
( spl63_3314
| spl63_3315
| spl63_3316
| ~ spl63_3313 ),
inference(avatar_split_clause,[],[f87137,f87129,f87145,f87142,f87139]) ).
fof(f87148,plain,
( $false
| ~ spl63_3314 ),
inference(resolution,[],[f87140,f72846]) ).
fof(f87153,plain,
~ spl63_3314,
inference(avatar_contradiction_clause,[],[f87148]) ).
fof(f87154,plain,
( ~ sub(c11817,familiename_1_1)
| ~ attr(c11815,c11817)
| ~ spl63_3315 ),
inference(resolution,[],[f87143,f20875]) ).
fof(f87155,plain,
( ~ attr(c11815,c11817)
| ~ spl63_3315 ),
inference(forward_subsumption_resolution,[],[f87154,f20876]) ).
fof(f87156,plain,
( $false
| ~ spl63_3315 ),
inference(forward_subsumption_resolution,[],[f87155,f20881]) ).
fof(f87157,plain,
~ spl63_3315,
inference(avatar_contradiction_clause,[],[f87156]) ).
fof(f87159,plain,
( ~ sub(c11816,eigenname_1_1)
| ~ val(c11816,nelson_0)
| ~ spl63_3316 ),
inference(resolution,[],[f87146,f20882]) ).
fof(f87160,plain,
( ~ val(c11816,nelson_0)
| ~ spl63_3316 ),
inference(forward_subsumption_resolution,[],[f87159,f20878]) ).
fof(f87161,plain,
( $false
| ~ spl63_3316 ),
inference(forward_subsumption_resolution,[],[f87160,f20877]) ).
fof(f87162,plain,
~ spl63_3316,
inference(avatar_contradiction_clause,[],[f87161]) ).
cnf(s1,plain,
( spl63_1
| spl63_2 ),
inference(sat_conversion,[],[f20895]) ).
cnf(s105,plain,
~ spl63_2,
inference(sat_conversion,[],[f73055]) ).
cnf(s1225,plain,
( ~ spl63_1
| spl63_3190
| spl63_3313 ),
inference(sat_conversion,[],[f87131]) ).
cnf(s1226,plain,
~ spl63_3190,
inference(sat_conversion,[],[f87133]) ).
cnf(s1227,plain,
( ~ spl63_3313
| spl63_3314
| spl63_3315
| spl63_3316 ),
inference(sat_conversion,[],[f87147]) ).
cnf(s1230,plain,
~ spl63_3314,
inference(sat_conversion,[],[f87153]) ).
cnf(s1231,plain,
~ spl63_3315,
inference(sat_conversion,[],[f87157]) ).
cnf(s1232,plain,
~ spl63_3316,
inference(sat_conversion,[],[f87162]) ).
cnf(s1233,plain,
~ spl63_3313,
inference(rat,[],[s1227,s1232,s1231,s1230]) ).
cnf(s1234,plain,
~ spl63_1,
inference(rat,[],[s1225,s1233,s1226]) ).
cnf(s1248,plain,
$false,
inference(rat,[],[s1,s105,s1234]) ).
fof(f87163,plain,
$false,
inference(avatar_sat_refutation,[],[s1248]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+18 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n016.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 23:33:04 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.80/4.17 % (4143404)Will run a generic schedule for satisfiability detection.
% 26.80/4.17 % (4143412)dis+10_1_sil=32000:sp=arity:random_seed=2657678298:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 26.80/4.17 % (4143410)% WARNING: option uhcvi not known.
% 26.80/4.17 % (4143409)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=168347654_2998 on theBenchmark for (2998ds/0Mi)
% 26.80/4.17 % (4143410)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=795204780:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 26.80/4.17 % (4143411)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=10598074:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 26.80/4.17 % (4143413)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2609092992:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 26.80/4.17 % (4143414)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=903629881:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 26.80/4.17 % (4143415)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3670930750:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 26.80/4.17 % (4143412)Instruction limit reached!
% 26.80/4.17 % (4143412)------------------------------
% 26.80/4.17 % (4143412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.80/4.17 % (4143412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.80/4.17 % (4143412)CaDiCaL version: 2.1.3
% 26.80/4.17 % (4143412)Termination reason: Instruction limit
% 26.80/4.17 % (4143412)Termination phase: Saturation
% 26.80/4.17 % (4143412)Time elapsed: 0.035 s
% 26.80/4.17 % (4143412)Peak memory usage: 26 MB
% 26.80/4.17 % (4143412)Instructions burned: 109 (million)
% 26.80/4.17 % (4143423)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3473000077:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 26.80/4.17 % (4143414)Instruction limit reached!
% 26.80/4.17 % (4143414)------------------------------
% 26.80/4.17 % (4143414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.80/4.17 % (4143414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.80/4.17 % (4143414)CaDiCaL version: 2.1.3
% 26.80/4.17 % (4143414)Termination reason: Instruction limit
% 26.80/4.17 % (4143414)Termination phase: Saturation
% 26.80/4.17 % (4143414)Time elapsed: 0.071 s
% 26.80/4.17 % (4143414)Peak memory usage: 27 MB
% 26.80/4.17 % (4143414)Instructions burned: 131 (million)
% 26.80/4.17 % (4143413)Instruction limit reached!
% 26.80/4.17 % (4143413)------------------------------
% 26.80/4.17 % (4143413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.80/4.17 % (4143413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.80/4.17 % (4143413)CaDiCaL version: 2.1.3
% 26.80/4.17 % (4143413)Termination reason: Instruction limit
% 26.80/4.17 % (4143413)Termination phase: Blocked clause elimination
% 26.80/4.17 % (4143413)Time elapsed: 0.073 s
% 26.80/4.17 % (4143413)Peak memory usage: 27 MB
% 26.80/4.17 % (4143413)Instructions burned: 116 (million)
% 26.80/4.17 % (4143425)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1184523143:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 26.80/4.17 % (4143426)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=186875441:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 26.80/4.17 % (4143415)Instruction limit reached!
% 26.80/4.17 % (4143415)------------------------------
% 26.80/4.17 % (4143415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.80/4.17 % (4143415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.80/4.17 % (4143415)CaDiCaL version: 2.1.3
% 26.80/4.17 % (4143415)Termination reason: Instruction limit
% 26.80/4.17 % (4143415)Termination phase: Saturation
% 26.80/4.17 % (4143415)Time elapsed: 0.094 s
% 26.80/4.17 % (4143415)Peak memory usage: 30 MB
% 26.80/4.17 % (4143415)Instructions burned: 159 (million)
% 26.80/4.17 % (4143429)ott-21_1_sil=16000:fs=off:random_seed=3469249872:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 26.80/4.17 % TRYING [1]
% 26.80/4.17 % TRYING [2]
% 26.80/4.17 % (4143425)Instruction limit reached!
% 26.80/4.17 % (4143425)------------------------------
% 26.80/4.17 % (4143425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.80/4.17 % (4143425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.07/6.98 % (4143425)CaDiCaL version: 2.1.3
% 46.07/6.98 % (4143425)Termination reason: Instruction limit
% 46.07/6.98 % (4143425)Termination phase: Blocked clause elimination
% 46.07/6.98 % (4143425)Time elapsed: 0.079 s
% 46.07/6.98 % (4143425)Peak memory usage: 28 MB
% 46.07/6.98 % (4143425)Instructions burned: 132 (million)
% 46.07/6.98 % (4143431)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3191806496:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 46.07/6.98 % (4143429)Instruction limit reached!
% 46.07/6.98 % (4143429)------------------------------
% 46.07/6.98 % (4143429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.07/6.98 % (4143429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.07/6.98 % (4143429)CaDiCaL version: 2.1.3
% 46.07/6.98 % (4143429)Termination reason: Instruction limit
% 46.07/6.98 % (4143429)Termination phase: Saturation
% 46.07/6.98 % (4143429)Time elapsed: 0.092 s
% 46.07/6.98 % (4143429)Peak memory usage: 28 MB
% 46.07/6.98 % (4143429)Instructions burned: 180 (million)
% 46.07/6.98 % (4143423)Instruction limit reached!
% 46.07/6.98 % (4143423)------------------------------
% 46.07/6.98 % (4143423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.07/6.98 % (4143423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.07/6.98 % (4143423)CaDiCaL version: 2.1.3
% 46.07/6.98 % (4143423)Termination reason: Instruction limit
% 46.07/6.98 % (4143423)Termination phase: Finite model building constraint generation
% 46.07/6.98 % (4143423)Time elapsed: 0.184 s
% 46.07/6.98 % (4143423)Peak memory usage: 54 MB
% 46.07/6.98 % (4143423)Instructions burned: 717 (million)
% 46.07/6.98 % (4143433)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3904499671:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 46.07/6.98 % (4143434)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=92367648:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 46.07/6.98 % TRYING [1]
% 46.07/6.98 % TRYING [2]
% 46.07/6.98 % TRYING [1]
% 46.07/6.98 % (4143431)Instruction limit reached!
% 46.07/6.98 % (4143431)------------------------------
% 46.07/6.98 % (4143431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.07/6.98 % (4143431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.07/6.98 % (4143431)CaDiCaL version: 2.1.3
% 46.07/6.98 % (4143431)Termination reason: Instruction limit
% 46.07/6.98 % (4143431)Termination phase: Saturation
% 46.07/6.98 % (4143431)Time elapsed: 0.253 s
% 46.07/6.98 % (4143431)Peak memory usage: 37 MB
% 46.07/6.98 % (4143431)Instructions burned: 477 (million)
% 46.07/6.98 % (4143426)Instruction limit reached!
% 46.07/6.98 % (4143426)------------------------------
% 46.07/6.98 % (4143426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.07/6.98 % (4143426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.07/6.98 % (4143426)CaDiCaL version: 2.1.3
% 46.07/6.98 % (4143426)Termination reason: Instruction limit
% 46.07/6.98 % (4143426)Termination phase: Saturation
% 46.07/6.98 % (4143426)Time elapsed: 0.362 s
% 46.07/6.98 % (4143426)Peak memory usage: 33 MB
% 46.07/6.98 % (4143426)Instructions burned: 685 (million)
% 46.07/6.98 % (4143437)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=693464177:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 46.07/6.98 % (4143438)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3908948060:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 46.07/6.98 % TRYING [3]
% 46.07/6.98 % (4143433)Instruction limit reached!
% 46.07/6.98 % (4143433)------------------------------
% 46.07/6.98 % (4143433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.07/6.98 % (4143433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.07/6.98 % (4143433)CaDiCaL version: 2.1.3
% 46.07/6.98 % (4143433)Termination reason: Instruction limit
% 46.07/6.98 % (4143433)Termination phase: Finite model building SAT solving
% 46.07/6.98 % (4143433)Time elapsed: 0.328 s
% 46.07/6.98 % (4143433)Peak memory usage: 38 MB
% 46.07/6.98 % (4143433)Instructions burned: 869 (million)
% 46.07/6.98 % (4143434)Instruction limit reached!
% 46.07/6.98 % (4143434)------------------------------
% 46.07/6.98 % (4143434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.07/6.98 % (4143434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.07/6.98 % (4143434)CaDiCaL version: 2.1.3
% 79.01/11.54 % (4143434)Termination reason: Instruction limit
% 79.01/11.54 % (4143434)Termination phase: Saturation
% 79.01/11.54 % (4143434)Time elapsed: 0.346 s
% 79.01/11.54 % (4143434)Peak memory usage: 54 MB
% 79.01/11.54 % (4143434)Instructions burned: 1180 (million)
% 79.01/11.54 % (4143441)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1602214189:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 79.01/11.54 % (4143443)fmb+10_1_sil=64000:random_seed=2552317661:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 79.01/11.54 % TRYING [1]
% 79.01/11.54 % TRYING [2]
% 79.01/11.54 % (4143438)Instruction limit reached!
% 79.01/11.54 % (4143438)------------------------------
% 79.01/11.54 % (4143438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.01/11.54 % (4143438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.01/11.54 % (4143438)CaDiCaL version: 2.1.3
% 79.01/11.54 % (4143438)Termination reason: Instruction limit
% 79.01/11.54 % (4143438)Termination phase: Saturation
% 79.01/11.54 % (4143438)Time elapsed: 0.382 s
% 79.01/11.54 % (4143438)Peak memory usage: 43 MB
% 79.01/11.54 % (4143438)Instructions burned: 694 (million)
% 79.01/11.54 % (4143445)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2535831320:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 79.01/11.54 % (4143437)Instruction limit reached!
% 79.01/11.54 % (4143437)------------------------------
% 79.01/11.54 % (4143437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.01/11.54 % (4143437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.01/11.54 % (4143437)CaDiCaL version: 2.1.3
% 79.01/11.54 % (4143437)Termination reason: Instruction limit
% 79.01/11.54 % (4143437)Termination phase: Finite model building constraint generation
% 79.01/11.54 % (4143437)Time elapsed: 0.427 s
% 79.01/11.54 % (4143437)Peak memory usage: 93 MB
% 79.01/11.54 % (4143437)Instructions burned: 890 (million)
% 79.01/11.54 % (4143447)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2079782451:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 79.01/11.54 % (4143441)Instruction limit reached!
% 79.01/11.54 % (4143441)------------------------------
% 79.01/11.54 % (4143441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.01/11.54 % (4143441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.01/11.54 % (4143441)CaDiCaL version: 2.1.3
% 79.01/11.54 % (4143441)Termination reason: Instruction limit
% 79.01/11.54 % (4143441)Termination phase: Saturation
% 79.01/11.54 % (4143441)Time elapsed: 0.414 s
% 79.01/11.54 % (4143441)Peak memory usage: 41 MB
% 79.01/11.54 % (4143441)Instructions burned: 882 (million)
% 79.01/11.54 % (4143449)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3466731608:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 79.01/11.54 % TRYING [20]
% 79.01/11.54 % TRYING [8]
% 79.01/11.54 % TRYING [3]
% 79.01/11.54 % (4143447)Instruction limit reached!
% 79.01/11.54 % (4143447)------------------------------
% 79.01/11.54 % (4143447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.01/11.54 % (4143447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.01/11.54 % (4143447)CaDiCaL version: 2.1.3
% 79.01/11.54 % (4143447)Termination reason: Instruction limit
% 79.01/11.54 % (4143447)Termination phase: Finite model building constraint generation
% 79.01/11.54 % (4143447)Time elapsed: 0.360 s
% 79.01/11.54 % (4143447)Peak memory usage: 64 MB
% 79.01/11.54 % (4143447)Instructions burned: 922 (million)
% 79.01/11.54 % (4143451)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1525859763:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 79.01/11.54 % TRYING [4]
% 79.01/11.54 % (4143451)Instruction limit reached!
% 79.01/11.54 % (4143451)------------------------------
% 79.01/11.54 % (4143451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 79.01/11.54 % (4143451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.01/11.54 % (4143451)CaDiCaL version: 2.1.3
% 79.01/11.54 % (4143451)Termination reason: Instruction limit
% 79.01/11.54 % (4143451)Termination phase: Saturation
% 79.01/11.54 % (4143451)Time elapsed: 0.676 s
% 79.01/11.54 % (4143451)Peak memory usage: 35 MB
% 79.01/11.54 % (4143451)Instructions burned: 1472 (million)
% 79.01/11.54 % (4143453)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1771488418:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 79.01/11.54 % TRYING [77]
% 79.01/11.54 % TRYING [4]
% 79.01/11.54 % (4143449)Instruction limit reached!
% 79.01/11.54 % (4143449)------------------------------
% 79.01/11.54 % (4143449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.50/31.06 % (4143449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.50/31.06 % (4143449)CaDiCaL version: 2.1.3
% 217.50/31.06 % (4143449)Termination reason: Instruction limit
% 217.50/31.06 % (4143449)Termination phase: Saturation
% 217.50/31.06 % (4143449)Time elapsed: 2.735 s
% 217.50/31.06 % (4143449)Peak memory usage: 39 MB
% 217.50/31.06 % (4143449)Instructions burned: 5131 (million)
% 217.50/31.06 % (4143455)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1474357041:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 217.50/31.06 % TRYING [16]
% 217.50/31.06 % (4143445)Instruction limit reached!
% 217.50/31.06 % (4143445)------------------------------
% 217.50/31.06 % (4143445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.50/31.06 % (4143445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.50/31.06 % (4143445)CaDiCaL version: 2.1.3
% 217.50/31.06 % (4143445)Termination reason: Instruction limit
% 217.50/31.06 % (4143445)Termination phase: Finite model building constraint generation
% 217.50/31.06 % (4143445)Time elapsed: 3.317 s
% 217.50/31.06 % (4143445)Peak memory usage: 550 MB
% 217.50/31.06 % (4143445)Instructions burned: 9516 (million)
% 217.50/31.06 % TRYING [5]
% 217.50/31.06 % (4143453)Instruction limit reached!
% 217.50/31.06 % (4143453)------------------------------
% 217.50/31.06 % (4143453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.50/31.06 % (4143453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.50/31.06 % (4143453)CaDiCaL version: 2.1.3
% 217.50/31.06 % (4143453)Termination reason: Instruction limit
% 217.50/31.06 % (4143453)Termination phase: Finite model building constraint generation
% 217.50/31.06 % (4143453)Time elapsed: 2.240 s
% 217.50/31.06 % (4143453)Peak memory usage: 417 MB
% 217.50/31.06 % (4143453)Instructions burned: 6324 (million)
% 217.50/31.06 % (4143457)ott-2_1_sil=16000:newcnf=on:random_seed=901048562:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 217.50/31.06 % (4143459)ott+10_1_sil=32000:tgt=ground:random_seed=3891434157:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 217.50/31.06 % (4143455)Instruction limit reached!
% 217.50/31.06 % (4143455)------------------------------
% 217.50/31.06 % (4143455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.50/31.06 % (4143455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.50/31.06 % (4143455)CaDiCaL version: 2.1.3
% 217.50/31.06 % (4143455)Termination reason: Instruction limit
% 217.50/31.06 % (4143455)Termination phase: Finite model building constraint generation
% 217.50/31.06 % (4143455)Time elapsed: 0.760 s
% 217.50/31.06 % (4143455)Peak memory usage: 121 MB
% 217.50/31.06 % (4143455)Instructions burned: 2175 (million)
% 217.50/31.06 % (4143461)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2629778177:i=54282_2952 on theBenchmark for (2952ds/54282Mi)
% 217.50/31.06 % (4143457)Instruction limit reached!
% 217.50/31.06 % (4143457)------------------------------
% 217.50/31.06 % (4143457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.50/31.06 % (4143457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.50/31.06 % (4143457)CaDiCaL version: 2.1.3
% 217.50/31.06 % (4143457)Termination reason: Instruction limit
% 217.50/31.06 % (4143457)Termination phase: Saturation
% 217.50/31.06 % (4143457)Time elapsed: 0.438 s
% 217.50/31.06 % (4143457)Peak memory usage: 37 MB
% 217.50/31.06 % (4143457)Instructions burned: 870 (million)
% 217.50/31.06 % (4143463)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3326668128:i=3512:aac=none_2950 on theBenchmark for (2950ds/3512Mi)
% 217.50/31.06 % TRYING [1]
% 217.50/31.06 % TRYING [2]
% 217.50/31.06 % TRYING [3]
% 217.50/31.06 % TRYING [6]
% 217.50/31.06 % (4143443)Instruction limit reached!
% 217.50/31.06 % (4143443)------------------------------
% 217.50/31.06 % (4143443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 217.50/31.06 % (4143443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 217.50/31.06 % (4143443)CaDiCaL version: 2.1.3
% 217.50/31.06 % (4143443)Termination reason: Instruction limit
% 217.50/31.06 % (4143443)Termination phase: Finite model building constraint generation
% 217.50/31.06 % (4143443)Time elapsed: 5.554 s
% 217.50/31.06 % (4143443)Peak memory usage: 151 MB
% 217.50/31.06 % (4143443)Instructions burned: 22065 (million)
% 217.50/31.06 % (4143466)dis+21_1_sil=32000:sas=cadical:random_seed=564415490:i=3773:amm=off_2936 on theBenchmark for (2936ds/3773Mi)
% 217.50/31.06 % (4143463)Instruction limit reached!
% 217.50/31.06 % (4143463)------------------------------
% 217.50/31.06 % (4143463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143463)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143463)Termination reason: Instruction limit
% 176.16/35.81 % (4143463)Termination phase: Saturation
% 176.16/35.81 % (4143463)Time elapsed: 1.804 s
% 176.16/35.81 % (4143463)Peak memory usage: 41 MB
% 176.16/35.81 % (4143463)Instructions burned: 3512 (million)
% 176.16/35.81 % (4143468)ott+11_1_sil=16000:gs=on:random_seed=3969660210:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2932 on theBenchmark for (2932ds/2251Mi)
% 176.16/35.81 % (4143459)Instruction limit reached!
% 176.16/35.81 % (4143459)------------------------------
% 176.16/35.81 % (4143459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143459)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143459)Termination reason: Instruction limit
% 176.16/35.81 % (4143459)Termination phase: Saturation
% 176.16/35.81 % (4143459)Time elapsed: 2.600 s
% 176.16/35.81 % (4143459)Peak memory usage: 119 MB
% 176.16/35.81 % (4143459)Instructions burned: 5116 (million)
% 176.16/35.81 % (4143470)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3962908949:fmbsr=1.6:i=67534_2928 on theBenchmark for (2928ds/67534Mi)
% 176.16/35.81 % TRYING [4]
% 176.16/35.81 % (4143466)Instruction limit reached!
% 176.16/35.81 % (4143466)------------------------------
% 176.16/35.81 % (4143466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143466)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143466)Termination reason: Instruction limit
% 176.16/35.81 % (4143466)Termination phase: Saturation
% 176.16/35.81 % (4143466)Time elapsed: 1.010 s
% 176.16/35.81 % (4143466)Peak memory usage: 67 MB
% 176.16/35.81 % (4143466)Instructions burned: 3776 (million)
% 176.16/35.81 % (4143472)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1416227903:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2926 on theBenchmark for (2926ds/4591Mi)
% 176.16/35.81 % TRYING [7]
% 176.16/35.81 % (4143468)Instruction limit reached!
% 176.16/35.81 % (4143468)------------------------------
% 176.16/35.81 % (4143468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143468)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143468)Termination reason: Instruction limit
% 176.16/35.81 % (4143468)Termination phase: Saturation
% 176.16/35.81 % (4143468)Time elapsed: 1.186 s
% 176.16/35.81 % (4143468)Peak memory usage: 92 MB
% 176.16/35.81 % (4143468)Instructions burned: 2252 (million)
% 176.16/35.81 % (4143474)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1402180371:i=29340_2920 on theBenchmark for (2920ds/29340Mi)
% 176.16/35.81 % (4143472)Instruction limit reached!
% 176.16/35.81 % (4143472)------------------------------
% 176.16/35.81 % (4143472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143472)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143472)Termination reason: Instruction limit
% 176.16/35.81 % (4143472)Termination phase: Saturation
% 176.16/35.81 % (4143472)Time elapsed: 1.189 s
% 176.16/35.81 % (4143472)Peak memory usage: 59 MB
% 176.16/35.81 % (4143472)Instructions burned: 4594 (million)
% 176.16/35.81 % (4143476)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1907940893:i=5211_2914 on theBenchmark for (2914ds/5211Mi)
% 176.16/35.81 % (4143476)Instruction limit reached!
% 176.16/35.81 % (4143476)------------------------------
% 176.16/35.81 % (4143476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143476)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143476)Termination reason: Instruction limit
% 176.16/35.81 % (4143476)Termination phase: Saturation
% 176.16/35.81 % (4143476)Time elapsed: 1.587 s
% 176.16/35.81 % (4143476)Peak memory usage: 58 MB
% 176.16/35.81 % (4143476)Instructions burned: 5212 (million)
% 176.16/35.81 % (4143478)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=605348640:i=5497:nm=2_2898 on theBenchmark for (2898ds/5497Mi)
% 176.16/35.81 % TRYING [17]
% 176.16/35.81 % (4143478)Instruction limit reached!
% 176.16/35.81 % (4143478)------------------------------
% 176.16/35.81 % (4143478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143478)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143478)Termination reason: Instruction limit
% 176.16/35.81 % (4143478)Termination phase: Finite model building constraint generation
% 176.16/35.81 % (4143478)Time elapsed: 1.115 s
% 176.16/35.81 % (4143478)Peak memory usage: 350 MB
% 176.16/35.81 % (4143478)Instructions burned: 5498 (million)
% 176.16/35.81 % (4143480)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1249294:fmbsr=2:i=46332_2886 on theBenchmark for (2886ds/46332Mi)
% 176.16/35.81 % TRYING [15]
% 176.16/35.81 % TRYING [5]
% 176.16/35.81 % TRYING [5]
% 176.16/35.81 % (4143474)Instruction limit reached!
% 176.16/35.81 % (4143474)------------------------------
% 176.16/35.81 % (4143474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143474)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143474)Termination reason: Instruction limit
% 176.16/35.81 % (4143474)Termination phase: Saturation
% 176.16/35.81 % (4143474)Time elapsed: 13.816 s
% 176.16/35.81 % (4143474)Peak memory usage: 83 MB
% 176.16/35.81 % (4143474)Instructions burned: 29340 (million)
% 176.16/35.81 % (4143482)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=659161693:i=14071_2781 on theBenchmark for (2781ds/14071Mi)
% 176.16/35.81 % TRYING [12]
% 176.16/35.81 % (4143480)Instruction limit reached!
% 176.16/35.81 % (4143480)------------------------------
% 176.16/35.81 % (4143480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143480)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143480)Termination reason: Instruction limit
% 176.16/35.81 % (4143480)Termination phase: Finite model building constraint generation
% 176.16/35.81 % (4143480)Time elapsed: 13.096 s
% 176.16/35.81 % (4143480)Peak memory usage: 3367 MB
% 176.16/35.81 % (4143480)Instructions burned: 46332 (million)
% 176.16/35.81 % (4143484)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2876662621:i=22565:add=on:rawr=on_2753 on theBenchmark for (2753ds/22565Mi)
% 176.16/35.81 % (4143482)Instruction limit reached!
% 176.16/35.81 % (4143482)------------------------------
% 176.16/35.81 % (4143482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143482)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143482)Termination reason: Instruction limit
% 176.16/35.81 % (4143482)Termination phase: Finite model building constraint generation
% 176.16/35.81 % (4143482)Time elapsed: 6.528 s
% 176.16/35.81 % (4143482)Peak memory usage: 1121 MB
% 176.16/35.81 % (4143482)Instructions burned: 14072 (million)
% 176.16/35.81 % (4143486)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2441097092:i=8173:av=off_2714 on theBenchmark for (2714ds/8173Mi)
% 176.16/35.81 % (4143484)Instruction limit reached!
% 176.16/35.81 % (4143484)------------------------------
% 176.16/35.81 % (4143484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143484)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143484)Termination reason: Instruction limit
% 176.16/35.81 % (4143484)Termination phase: Saturation
% 176.16/35.81 % (4143484)Time elapsed: 4.470 s
% 176.16/35.81 % (4143484)Peak memory usage: 116 MB
% 176.16/35.81 % (4143484)Instructions burned: 22568 (million)
% 176.16/35.81 % (4143488)dis+10_16:1_sil=16000:random_seed=1306203841:i=9155:fsr=off_2708 on theBenchmark for (2708ds/9155Mi)
% 176.16/35.81 % (4143411)Instruction limit reached!
% 176.16/35.81 % (4143411)------------------------------
% 176.16/35.81 % (4143411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143411)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143411)Termination reason: Instruction limit
% 176.16/35.81 % (4143411)Termination phase: Saturation
% 176.16/35.81 % (4143411)Time elapsed: 29.679 s
% 176.16/35.81 % (4143411)Peak memory usage: 152 MB
% 176.16/35.81 % (4143411)Instructions burned: 88026 (million)
% 176.16/35.81 % (4143490)ott-3_8_sil=64000:random_seed=541346544:i=20139:bs=on_2701 on theBenchmark for (2701ds/20139Mi)
% 176.16/35.81 % TRYING [6]
% 176.16/35.81 % (4143461)Instruction limit reached!
% 176.16/35.81 % (4143461)------------------------------
% 176.16/35.81 % (4143461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143461)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143461)Termination reason: Instruction limit
% 176.16/35.81 % (4143461)Termination phase: Finite model building SAT solving
% 176.16/35.81 % (4143461)Time elapsed: 26.070 s
% 176.16/35.81 % (4143461)Peak memory usage: 243 MB
% 176.16/35.81 % (4143461)Instructions burned: 54283 (million)
% 176.16/35.81 % (4143492)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4000077250:fmbsr=2:i=32576_2691 on theBenchmark for (2691ds/32576Mi)
% 176.16/35.81 % TRYING [9]
% 176.16/35.81 % (4143488)Instruction limit reached!
% 176.16/35.81 % (4143488)------------------------------
% 176.16/35.81 % (4143488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143488)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143488)Termination reason: Instruction limit
% 176.16/35.81 % (4143488)Termination phase: Saturation
% 176.16/35.81 % (4143488)Time elapsed: 2.101 s
% 176.16/35.81 % (4143488)Peak memory usage: 81 MB
% 176.16/35.81 % (4143488)Instructions burned: 9159 (million)
% 176.16/35.81 % (4143494)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1777269795:i=11404_2686 on theBenchmark for (2686ds/11404Mi)
% 176.16/35.81 % (4143486)Instruction limit reached!
% 176.16/35.81 % (4143486)------------------------------
% 176.16/35.81 % (4143486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143486)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143486)Termination reason: Instruction limit
% 176.16/35.81 % (4143486)Termination phase: Saturation
% 176.16/35.81 % (4143486)Time elapsed: 4.608 s
% 176.16/35.81 % (4143486)Peak memory usage: 192 MB
% 176.16/35.81 % (4143486)Instructions burned: 8173 (million)
% 176.16/35.81 % (4143496)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3498493416:i=14134_2668 on theBenchmark for (2668ds/14134Mi)
% 176.16/35.81 % (4143494)Instruction limit reached!
% 176.16/35.81 % (4143494)------------------------------
% 176.16/35.81 % (4143494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.81 % (4143494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.81 % (4143494)CaDiCaL version: 2.1.3
% 176.16/35.81 % (4143494)Termination reason: Instruction limit
% 176.16/35.81 % (4143494)Termination phase: Saturation
% 176.16/35.81 % (4143494)Time elapsed: 2.710 s
% 176.16/35.81 % (4143494)Peak memory usage: 147 MB
% 176.16/35.81 % (4143494)Instructions burned: 11404 (million)
% 176.16/35.81 % (4143498)dis+33_16_sil=32000:sac=on:random_seed=2458970168:i=15851:nm=0_2659 on theBenchmark for (2659ds/15851Mi)
% 176.16/35.81 % (4143498) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-4143404-4143498"...
% 176.16/35.81 % (4143498)...printing done.
% 176.16/35.81 % (4143498)Refutation found. Thanks to Tanya!
% 176.16/35.81 % SZS status Theorem for theBenchmark
% 176.16/35.81 % SZS output start Proof for theBenchmark
% See solution above
% 176.16/35.83 % (4143498)------------------------------
% 176.16/35.83 % (4143498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.16/35.83 % (4143498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.16/35.83 % (4143498)CaDiCaL version: 2.1.3
% 176.16/35.83 % (4143498)Termination reason: Refutation
% 176.16/35.83 % (4143498)Time elapsed: 1.416 s
% 176.16/35.83 % (4143498)Peak memory usage: 79 MB
% 176.16/35.83 % (4143498)Instructions burned: 5670 (million)
% 176.16/35.83 % (4143404)Success in time 35.586 s
% 176.16/35.83 % Vampire exiting
%------------------------------------------------------------------------------