%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR116+37 : 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 : n012.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:51 AM UTC 2026
% Result : Theorem 119.73s 24.74s
% Output : Refutation 119.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 16
% Syntax : Number of formulae : 136 ( 40 unt; 7 def)
% Number of atoms : 1315 ( 0 equ)
% Maximal formula atoms : 154 ( 9 avg)
% Number of connectives : 1434 ( 255 ~; 224 |; 943 &)
% ( 7 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 154 ( 12 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 38 ( 37 usr; 8 prp; 0-3 aty)
% Number of functors : 65 ( 65 usr; 57 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_wp_720) ).
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,
( pmod(c1,fr__374h_1_1,pr__344sident_1_1)
& equ(c3,c588)
& sub(c3,einh__366hepunkt_1_1)
& subs(c588,auftritt_1_1)
& attch(c598,c588)
& attr(c598,c599)
& attr(c598,c600)
& prop(c598,s__374dafrikanisch_1_1)
& sub(c598,c1)
& sub(c599,eigenname_1_1)
& val(c599,nelson_0)
& sub(c600,familiename_1_1)
& val(c600,mandela_0)
& sub(c627,ansprache_1_1)
& benf(c630,c598)
& purp(c630,c627)
& subs(c630,einladen_2_1)
& arg1(c7,c3)
& arg2(c7,c588)
& subr(c7,equ_0)
& assoc(einh__366hepunkt_1_1,ein_4_1)
& sub(einh__366hepunkt_1_1,h__366hepunkt_1_1)
& sort(c1,ent)
& card(c1,card_c)
& etype(c1,etype_c)
& fact(c1,fact_c)
& gener(c1,gener_c)
& quant(c1,quant_c)
& refer(c1,refer_c)
& varia(c1,varia_c)
& sort(fr__374h_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(c3,io)
& card(c3,int1)
& etype(c3,int0)
& fact(c3,real)
& gener(c3,gener_c)
& quant(c3,one)
& refer(c3,refer_c)
& varia(c3,varia_c)
& sort(c588,ad)
& card(c588,int1)
& etype(c588,int0)
& fact(c588,real)
& gener(c588,sp)
& quant(c588,one)
& refer(c588,det)
& varia(c588,con)
& sort(einh__366hepunkt_1_1,io)
& card(einh__366hepunkt_1_1,int1)
& etype(einh__366hepunkt_1_1,int0)
& fact(einh__366hepunkt_1_1,real)
& gener(einh__366hepunkt_1_1,ge)
& quant(einh__366hepunkt_1_1,one)
& refer(einh__366hepunkt_1_1,refer_c)
& varia(einh__366hepunkt_1_1,varia_c)
& sort(auftritt_1_1,ad)
& card(auftritt_1_1,int1)
& etype(auftritt_1_1,int0)
& fact(auftritt_1_1,real)
& gener(auftritt_1_1,ge)
& quant(auftritt_1_1,one)
& refer(auftritt_1_1,refer_c)
& varia(auftritt_1_1,varia_c)
& sort(c598,d)
& card(c598,int1)
& etype(c598,int0)
& fact(c598,real)
& gener(c598,sp)
& quant(c598,one)
& refer(c598,det)
& varia(c598,con)
& sort(c599,na)
& card(c599,int1)
& etype(c599,int0)
& fact(c599,real)
& gener(c599,sp)
& quant(c599,one)
& refer(c599,indet)
& varia(c599,varia_c)
& sort(c600,na)
& card(c600,int1)
& etype(c600,int0)
& fact(c600,real)
& gener(c600,sp)
& quant(c600,one)
& refer(c600,indet)
& varia(c600,varia_c)
& sort(s__374dafrikanisch_1_1,nq)
& sort(eigenname_1_1,na)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& sort(nelson_0,fe)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(mandela_0,fe)
& sort(c627,ad)
& sort(c627,io)
& card(c627,int1)
& etype(c627,int0)
& fact(c627,real)
& gener(c627,sp)
& quant(c627,one)
& refer(c627,indet)
& varia(c627,varia_c)
& sort(ansprache_1_1,ad)
& sort(ansprache_1_1,io)
& card(ansprache_1_1,int1)
& etype(ansprache_1_1,int0)
& fact(ansprache_1_1,real)
& gener(ansprache_1_1,ge)
& quant(ansprache_1_1,one)
& refer(ansprache_1_1,refer_c)
& varia(ansprache_1_1,varia_c)
& sort(c630,da)
& fact(c630,real)
& gener(c630,sp)
& sort(einladen_2_1,da)
& fact(einladen_2_1,real)
& gener(einladen_2_1,ge)
& sort(c7,st)
& fact(c7,real)
& gener(c7,sp)
& sort(equ_0,st)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& sort(ein_4_1,nu)
& card(ein_4_1,int1)
& sort(h__366hepunkt_1_1,io)
& card(h__366hepunkt_1_1,int1)
& etype(h__366hepunkt_1_1,int0)
& fact(h__366hepunkt_1_1,real)
& gener(h__366hepunkt_1_1,ge)
& quant(h__366hepunkt_1_1,one)
& refer(h__366hepunkt_1_1,refer_c)
& varia(h__366hepunkt_1_1,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_wp_720) ).
fof(f10191,plain,
( pmod(c1,fr__374h_1_1,pr__344sident_1_1)
& sub(c3,einh__366hepunkt_1_1)
& subs(c588,auftritt_1_1)
& attch(c598,c588)
& attr(c598,c599)
& attr(c598,c600)
& prop(c598,s__374dafrikanisch_1_1)
& sub(c598,c1)
& sub(c599,eigenname_1_1)
& val(c599,nelson_0)
& sub(c600,familiename_1_1)
& val(c600,mandela_0)
& sub(c627,ansprache_1_1)
& benf(c630,c598)
& purp(c630,c627)
& subs(c630,einladen_2_1)
& arg1(c7,c3)
& arg2(c7,c588)
& subr(c7,equ_0)
& assoc(einh__366hepunkt_1_1,ein_4_1)
& sub(einh__366hepunkt_1_1,h__366hepunkt_1_1)
& sort(c1,ent)
& card(c1,card_c)
& etype(c1,etype_c)
& fact(c1,fact_c)
& gener(c1,gener_c)
& quant(c1,quant_c)
& refer(c1,refer_c)
& varia(c1,varia_c)
& sort(fr__374h_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(c3,io)
& card(c3,int1)
& etype(c3,int0)
& fact(c3,real)
& gener(c3,gener_c)
& quant(c3,one)
& refer(c3,refer_c)
& varia(c3,varia_c)
& sort(c588,ad)
& card(c588,int1)
& etype(c588,int0)
& fact(c588,real)
& gener(c588,sp)
& quant(c588,one)
& refer(c588,det)
& varia(c588,con)
& sort(einh__366hepunkt_1_1,io)
& card(einh__366hepunkt_1_1,int1)
& etype(einh__366hepunkt_1_1,int0)
& fact(einh__366hepunkt_1_1,real)
& gener(einh__366hepunkt_1_1,ge)
& quant(einh__366hepunkt_1_1,one)
& refer(einh__366hepunkt_1_1,refer_c)
& varia(einh__366hepunkt_1_1,varia_c)
& sort(auftritt_1_1,ad)
& card(auftritt_1_1,int1)
& etype(auftritt_1_1,int0)
& fact(auftritt_1_1,real)
& gener(auftritt_1_1,ge)
& quant(auftritt_1_1,one)
& refer(auftritt_1_1,refer_c)
& varia(auftritt_1_1,varia_c)
& sort(c598,d)
& card(c598,int1)
& etype(c598,int0)
& fact(c598,real)
& gener(c598,sp)
& quant(c598,one)
& refer(c598,det)
& varia(c598,con)
& sort(c599,na)
& card(c599,int1)
& etype(c599,int0)
& fact(c599,real)
& gener(c599,sp)
& quant(c599,one)
& refer(c599,indet)
& varia(c599,varia_c)
& sort(c600,na)
& card(c600,int1)
& etype(c600,int0)
& fact(c600,real)
& gener(c600,sp)
& quant(c600,one)
& refer(c600,indet)
& varia(c600,varia_c)
& sort(s__374dafrikanisch_1_1,nq)
& sort(eigenname_1_1,na)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& sort(nelson_0,fe)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(mandela_0,fe)
& sort(c627,ad)
& sort(c627,io)
& card(c627,int1)
& etype(c627,int0)
& fact(c627,real)
& gener(c627,sp)
& quant(c627,one)
& refer(c627,indet)
& varia(c627,varia_c)
& sort(ansprache_1_1,ad)
& sort(ansprache_1_1,io)
& card(ansprache_1_1,int1)
& etype(ansprache_1_1,int0)
& fact(ansprache_1_1,real)
& gener(ansprache_1_1,ge)
& quant(ansprache_1_1,one)
& refer(ansprache_1_1,refer_c)
& varia(ansprache_1_1,varia_c)
& sort(c630,da)
& fact(c630,real)
& gener(c630,sp)
& sort(einladen_2_1,da)
& fact(einladen_2_1,real)
& gener(einladen_2_1,ge)
& sort(c7,st)
& fact(c7,real)
& gener(c7,sp)
& sort(equ_0,st)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& sort(ein_4_1,nu)
& card(ein_4_1,int1)
& sort(h__366hepunkt_1_1,io)
& card(h__366hepunkt_1_1,int1)
& etype(h__366hepunkt_1_1,int0)
& fact(h__366hepunkt_1_1,real)
& gener(h__366hepunkt_1_1,ge)
& quant(h__366hepunkt_1_1,one)
& refer(h__366hepunkt_1_1,refer_c)
& varia(h__366hepunkt_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10327,plain,
( pmod(c1,fr__374h_1_1,pr__344sident_1_1)
& sub(c3,einh__366hepunkt_1_1)
& subs(c588,auftritt_1_1)
& attch(c598,c588)
& attr(c598,c599)
& attr(c598,c600)
& prop(c598,s__374dafrikanisch_1_1)
& sub(c598,c1)
& sub(c599,eigenname_1_1)
& val(c599,nelson_0)
& sub(c600,familiename_1_1)
& val(c600,mandela_0)
& sub(c627,ansprache_1_1)
& benf(c630,c598)
& purp(c630,c627)
& subs(c630,einladen_2_1)
& arg1(c7,c3)
& arg2(c7,c588)
& subr(c7,equ_0)
& assoc(einh__366hepunkt_1_1,ein_4_1)
& sub(einh__366hepunkt_1_1,h__366hepunkt_1_1)
& card(c1,card_c)
& etype(c1,etype_c)
& fact(c1,fact_c)
& gener(c1,gener_c)
& quant(c1,quant_c)
& refer(c1,refer_c)
& varia(c1,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(c3,int1)
& etype(c3,int0)
& fact(c3,real)
& gener(c3,gener_c)
& quant(c3,one)
& refer(c3,refer_c)
& varia(c3,varia_c)
& card(c588,int1)
& etype(c588,int0)
& fact(c588,real)
& gener(c588,sp)
& quant(c588,one)
& refer(c588,det)
& varia(c588,con)
& card(einh__366hepunkt_1_1,int1)
& etype(einh__366hepunkt_1_1,int0)
& fact(einh__366hepunkt_1_1,real)
& gener(einh__366hepunkt_1_1,ge)
& quant(einh__366hepunkt_1_1,one)
& refer(einh__366hepunkt_1_1,refer_c)
& varia(einh__366hepunkt_1_1,varia_c)
& card(auftritt_1_1,int1)
& etype(auftritt_1_1,int0)
& fact(auftritt_1_1,real)
& gener(auftritt_1_1,ge)
& quant(auftritt_1_1,one)
& refer(auftritt_1_1,refer_c)
& varia(auftritt_1_1,varia_c)
& card(c598,int1)
& etype(c598,int0)
& fact(c598,real)
& gener(c598,sp)
& quant(c598,one)
& refer(c598,det)
& varia(c598,con)
& card(c599,int1)
& etype(c599,int0)
& fact(c599,real)
& gener(c599,sp)
& quant(c599,one)
& refer(c599,indet)
& varia(c599,varia_c)
& card(c600,int1)
& etype(c600,int0)
& fact(c600,real)
& gener(c600,sp)
& quant(c600,one)
& refer(c600,indet)
& varia(c600,varia_c)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& card(c627,int1)
& etype(c627,int0)
& fact(c627,real)
& gener(c627,sp)
& quant(c627,one)
& refer(c627,indet)
& varia(c627,varia_c)
& card(ansprache_1_1,int1)
& etype(ansprache_1_1,int0)
& fact(ansprache_1_1,real)
& gener(ansprache_1_1,ge)
& quant(ansprache_1_1,one)
& refer(ansprache_1_1,refer_c)
& varia(ansprache_1_1,varia_c)
& fact(c630,real)
& gener(c630,sp)
& fact(einladen_2_1,real)
& gener(einladen_2_1,ge)
& fact(c7,real)
& gener(c7,sp)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& card(ein_4_1,int1)
& card(h__366hepunkt_1_1,int1)
& etype(h__366hepunkt_1_1,int0)
& fact(h__366hepunkt_1_1,real)
& gener(h__366hepunkt_1_1,ge)
& quant(h__366hepunkt_1_1,one)
& refer(h__366hepunkt_1_1,refer_c)
& varia(h__366hepunkt_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10330,plain,
( pmod(c1,fr__374h_1_1,pr__344sident_1_1)
& sub(c3,einh__366hepunkt_1_1)
& subs(c588,auftritt_1_1)
& attch(c598,c588)
& attr(c598,c599)
& attr(c598,c600)
& prop(c598,s__374dafrikanisch_1_1)
& sub(c598,c1)
& sub(c599,eigenname_1_1)
& val(c599,nelson_0)
& sub(c600,familiename_1_1)
& val(c600,mandela_0)
& sub(c627,ansprache_1_1)
& benf(c630,c598)
& purp(c630,c627)
& subs(c630,einladen_2_1)
& arg1(c7,c3)
& arg2(c7,c588)
& subr(c7,equ_0)
& assoc(einh__366hepunkt_1_1,ein_4_1)
& sub(einh__366hepunkt_1_1,h__366hepunkt_1_1)
& card(c1,card_c)
& etype(c1,etype_c)
& fact(c1,fact_c)
& gener(c1,gener_c)
& refer(c1,refer_c)
& varia(c1,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(c3,int1)
& etype(c3,int0)
& fact(c3,real)
& gener(c3,gener_c)
& refer(c3,refer_c)
& varia(c3,varia_c)
& card(c588,int1)
& etype(c588,int0)
& fact(c588,real)
& gener(c588,sp)
& refer(c588,det)
& varia(c588,con)
& card(einh__366hepunkt_1_1,int1)
& etype(einh__366hepunkt_1_1,int0)
& fact(einh__366hepunkt_1_1,real)
& gener(einh__366hepunkt_1_1,ge)
& refer(einh__366hepunkt_1_1,refer_c)
& varia(einh__366hepunkt_1_1,varia_c)
& card(auftritt_1_1,int1)
& etype(auftritt_1_1,int0)
& fact(auftritt_1_1,real)
& gener(auftritt_1_1,ge)
& refer(auftritt_1_1,refer_c)
& varia(auftritt_1_1,varia_c)
& card(c598,int1)
& etype(c598,int0)
& fact(c598,real)
& gener(c598,sp)
& refer(c598,det)
& varia(c598,con)
& card(c599,int1)
& etype(c599,int0)
& fact(c599,real)
& gener(c599,sp)
& refer(c599,indet)
& varia(c599,varia_c)
& card(c600,int1)
& etype(c600,int0)
& fact(c600,real)
& gener(c600,sp)
& refer(c600,indet)
& varia(c600,varia_c)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& card(c627,int1)
& etype(c627,int0)
& fact(c627,real)
& gener(c627,sp)
& refer(c627,indet)
& varia(c627,varia_c)
& card(ansprache_1_1,int1)
& etype(ansprache_1_1,int0)
& fact(ansprache_1_1,real)
& gener(ansprache_1_1,ge)
& refer(ansprache_1_1,refer_c)
& varia(ansprache_1_1,varia_c)
& fact(c630,real)
& gener(c630,sp)
& fact(einladen_2_1,real)
& gener(einladen_2_1,ge)
& fact(c7,real)
& gener(c7,sp)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& card(ein_4_1,int1)
& card(h__366hepunkt_1_1,int1)
& etype(h__366hepunkt_1_1,int0)
& fact(h__366hepunkt_1_1,real)
& gener(h__366hepunkt_1_1,ge)
& refer(h__366hepunkt_1_1,refer_c)
& varia(h__366hepunkt_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10327]) ).
fof(f10333,plain,
( pmod(c1,fr__374h_1_1,pr__344sident_1_1)
& sub(c3,einh__366hepunkt_1_1)
& subs(c588,auftritt_1_1)
& attch(c598,c588)
& attr(c598,c599)
& attr(c598,c600)
& prop(c598,s__374dafrikanisch_1_1)
& sub(c598,c1)
& sub(c599,eigenname_1_1)
& val(c599,nelson_0)
& sub(c600,familiename_1_1)
& val(c600,mandela_0)
& sub(c627,ansprache_1_1)
& benf(c630,c598)
& purp(c630,c627)
& subs(c630,einladen_2_1)
& arg1(c7,c3)
& arg2(c7,c588)
& subr(c7,equ_0)
& assoc(einh__366hepunkt_1_1,ein_4_1)
& sub(einh__366hepunkt_1_1,h__366hepunkt_1_1)
& etype(c1,etype_c)
& fact(c1,fact_c)
& gener(c1,gener_c)
& refer(c1,refer_c)
& varia(c1,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(c3,int0)
& fact(c3,real)
& gener(c3,gener_c)
& refer(c3,refer_c)
& varia(c3,varia_c)
& etype(c588,int0)
& fact(c588,real)
& gener(c588,sp)
& refer(c588,det)
& varia(c588,con)
& etype(einh__366hepunkt_1_1,int0)
& fact(einh__366hepunkt_1_1,real)
& gener(einh__366hepunkt_1_1,ge)
& refer(einh__366hepunkt_1_1,refer_c)
& varia(einh__366hepunkt_1_1,varia_c)
& etype(auftritt_1_1,int0)
& fact(auftritt_1_1,real)
& gener(auftritt_1_1,ge)
& refer(auftritt_1_1,refer_c)
& varia(auftritt_1_1,varia_c)
& etype(c598,int0)
& fact(c598,real)
& gener(c598,sp)
& refer(c598,det)
& varia(c598,con)
& etype(c599,int0)
& fact(c599,real)
& gener(c599,sp)
& refer(c599,indet)
& varia(c599,varia_c)
& etype(c600,int0)
& fact(c600,real)
& gener(c600,sp)
& refer(c600,indet)
& varia(c600,varia_c)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& etype(c627,int0)
& fact(c627,real)
& gener(c627,sp)
& refer(c627,indet)
& varia(c627,varia_c)
& etype(ansprache_1_1,int0)
& fact(ansprache_1_1,real)
& gener(ansprache_1_1,ge)
& refer(ansprache_1_1,refer_c)
& varia(ansprache_1_1,varia_c)
& fact(c630,real)
& gener(c630,sp)
& fact(einladen_2_1,real)
& gener(einladen_2_1,ge)
& fact(c7,real)
& gener(c7,sp)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& etype(h__366hepunkt_1_1,int0)
& fact(h__366hepunkt_1_1,real)
& gener(h__366hepunkt_1_1,ge)
& refer(h__366hepunkt_1_1,refer_c)
& varia(h__366hepunkt_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10330]) ).
fof(f10336,plain,
( pmod(c1,fr__374h_1_1,pr__344sident_1_1)
& sub(c3,einh__366hepunkt_1_1)
& subs(c588,auftritt_1_1)
& attch(c598,c588)
& attr(c598,c599)
& attr(c598,c600)
& prop(c598,s__374dafrikanisch_1_1)
& sub(c598,c1)
& sub(c599,eigenname_1_1)
& val(c599,nelson_0)
& sub(c600,familiename_1_1)
& val(c600,mandela_0)
& sub(c627,ansprache_1_1)
& benf(c630,c598)
& purp(c630,c627)
& subs(c630,einladen_2_1)
& arg1(c7,c3)
& arg2(c7,c588)
& subr(c7,equ_0)
& assoc(einh__366hepunkt_1_1,ein_4_1)
& sub(einh__366hepunkt_1_1,h__366hepunkt_1_1)
& etype(c1,etype_c)
& fact(c1,fact_c)
& gener(c1,gener_c)
& varia(c1,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(c3,int0)
& fact(c3,real)
& gener(c3,gener_c)
& varia(c3,varia_c)
& etype(c588,int0)
& fact(c588,real)
& gener(c588,sp)
& varia(c588,con)
& etype(einh__366hepunkt_1_1,int0)
& fact(einh__366hepunkt_1_1,real)
& gener(einh__366hepunkt_1_1,ge)
& varia(einh__366hepunkt_1_1,varia_c)
& etype(auftritt_1_1,int0)
& fact(auftritt_1_1,real)
& gener(auftritt_1_1,ge)
& varia(auftritt_1_1,varia_c)
& etype(c598,int0)
& fact(c598,real)
& gener(c598,sp)
& varia(c598,con)
& etype(c599,int0)
& fact(c599,real)
& gener(c599,sp)
& varia(c599,varia_c)
& etype(c600,int0)
& fact(c600,real)
& gener(c600,sp)
& varia(c600,varia_c)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& varia(eigenname_1_1,varia_c)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& varia(familiename_1_1,varia_c)
& etype(c627,int0)
& fact(c627,real)
& gener(c627,sp)
& varia(c627,varia_c)
& etype(ansprache_1_1,int0)
& fact(ansprache_1_1,real)
& gener(ansprache_1_1,ge)
& varia(ansprache_1_1,varia_c)
& fact(c630,real)
& gener(c630,sp)
& fact(einladen_2_1,real)
& gener(einladen_2_1,ge)
& fact(c7,real)
& gener(c7,sp)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& etype(h__366hepunkt_1_1,int0)
& fact(h__366hepunkt_1_1,real)
& gener(h__366hepunkt_1_1,ge)
& varia(h__366hepunkt_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10333]) ).
fof(f10341,plain,
( pmod(c1,fr__374h_1_1,pr__344sident_1_1)
& sub(c3,einh__366hepunkt_1_1)
& subs(c588,auftritt_1_1)
& attch(c598,c588)
& attr(c598,c599)
& attr(c598,c600)
& prop(c598,s__374dafrikanisch_1_1)
& sub(c598,c1)
& sub(c599,eigenname_1_1)
& val(c599,nelson_0)
& sub(c600,familiename_1_1)
& val(c600,mandela_0)
& sub(c627,ansprache_1_1)
& benf(c630,c598)
& purp(c630,c627)
& subs(c630,einladen_2_1)
& arg1(c7,c3)
& arg2(c7,c588)
& subr(c7,equ_0)
& assoc(einh__366hepunkt_1_1,ein_4_1)
& sub(einh__366hepunkt_1_1,h__366hepunkt_1_1)
& etype(c1,etype_c)
& fact(c1,fact_c)
& gener(c1,gener_c)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& etype(c3,int0)
& fact(c3,real)
& gener(c3,gener_c)
& etype(c588,int0)
& fact(c588,real)
& gener(c588,sp)
& etype(einh__366hepunkt_1_1,int0)
& fact(einh__366hepunkt_1_1,real)
& gener(einh__366hepunkt_1_1,ge)
& etype(auftritt_1_1,int0)
& fact(auftritt_1_1,real)
& gener(auftritt_1_1,ge)
& etype(c598,int0)
& fact(c598,real)
& gener(c598,sp)
& etype(c599,int0)
& fact(c599,real)
& gener(c599,sp)
& etype(c600,int0)
& fact(c600,real)
& gener(c600,sp)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& etype(c627,int0)
& fact(c627,real)
& gener(c627,sp)
& etype(ansprache_1_1,int0)
& fact(ansprache_1_1,real)
& gener(ansprache_1_1,ge)
& fact(c630,real)
& gener(c630,sp)
& fact(einladen_2_1,real)
& gener(einladen_2_1,ge)
& fact(c7,real)
& gener(c7,sp)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& etype(h__366hepunkt_1_1,int0)
& fact(h__366hepunkt_1_1,real)
& gener(h__366hepunkt_1_1,ge) ),
inference(pure_predicate_removal,[],[f10336]) ).
fof(f10346,plain,
( pmod(c1,fr__374h_1_1,pr__344sident_1_1)
& sub(c3,einh__366hepunkt_1_1)
& subs(c588,auftritt_1_1)
& attch(c598,c588)
& attr(c598,c599)
& attr(c598,c600)
& prop(c598,s__374dafrikanisch_1_1)
& sub(c598,c1)
& sub(c599,eigenname_1_1)
& val(c599,nelson_0)
& sub(c600,familiename_1_1)
& val(c600,mandela_0)
& sub(c627,ansprache_1_1)
& benf(c630,c598)
& purp(c630,c627)
& subs(c630,einladen_2_1)
& arg1(c7,c3)
& arg2(c7,c588)
& subr(c7,equ_0)
& assoc(einh__366hepunkt_1_1,ein_4_1)
& sub(einh__366hepunkt_1_1,h__366hepunkt_1_1)
& etype(c1,etype_c)
& fact(c1,fact_c)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& etype(c3,int0)
& fact(c3,real)
& etype(c588,int0)
& fact(c588,real)
& etype(einh__366hepunkt_1_1,int0)
& fact(einh__366hepunkt_1_1,real)
& etype(auftritt_1_1,int0)
& fact(auftritt_1_1,real)
& etype(c598,int0)
& fact(c598,real)
& etype(c599,int0)
& fact(c599,real)
& etype(c600,int0)
& fact(c600,real)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& etype(c627,int0)
& fact(c627,real)
& etype(ansprache_1_1,int0)
& fact(ansprache_1_1,real)
& fact(c630,real)
& fact(einladen_2_1,real)
& fact(c7,real)
& fact(equ_0,real)
& etype(h__366hepunkt_1_1,int0)
& fact(h__366hepunkt_1_1,real) ),
inference(pure_predicate_removal,[],[f10341]) ).
fof(f10350,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f10399,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(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(flattening,[],[f10399]) ).
fof(f10508,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(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(flattening,[],[f10508]) ).
fof(f10514,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(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(flattening,[],[f10514]) ).
fof(f10518,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(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(flattening,[],[f10518]) ).
fof(f10551,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(f10554,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))],[f10400]) ).
fof(f10589,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))],[f10509]) ).
fof(f10590,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))],[f10515]) ).
fof(f10592,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))],[f10519]) ).
fof(f10600,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[],[f1]) ).
fof(f10602,plain,
! [X0,X1] :
( ~ fact(X0,X1)
| has_fact_leq(X0,X1) ),
inference(cnf_transformation,[],[f10350]) ).
fof(f10686,plain,
! [X0,X1] :
( ~ loc(X1,X0)
| ~ has_fact_leq(X1,real)
| obj(sK2(X0,X1),X1) ),
inference(cnf_transformation,[],[f10554]) ).
fof(f10852,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| val(sK48(X0,X2),X2) ),
inference(cnf_transformation,[],[f10589]) ).
fof(f10853,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| sub(sK48(X0,X2),name_1_1) ),
inference(cnf_transformation,[],[f10589]) ).
fof(f10855,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| loc(X0,sK49(X0,X2)) ),
inference(cnf_transformation,[],[f10589]) ).
fof(f10856,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| attr(sK47(X0,X2),sK48(X0,X2)) ),
inference(cnf_transformation,[],[f10589]) ).
fof(f10857,plain,
! [X2,X0,X1] :
( ~ state_adjective_state_binding(X1,X2)
| ~ prop(X0,X1)
| in(sK49(X0,X2),sK47(X0,X2)) ),
inference(cnf_transformation,[],[f10589]) ).
fof(f10860,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,[],[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)
| arg2(sK50(X2),X2)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10590]) ).
fof(f10862,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,[],[f10590]) ).
fof(f10868,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,[],[f10592]) ).
fof(f10872,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,[],[f10592]) ).
fof(f10873,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,[],[f10592]) ).
fof(f19789,plain,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
inference(cnf_transformation,[],[f9161]) ).
fof(f20816,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,[],[f10551]) ).
fof(f20835,plain,
fact(c598,real),
inference(cnf_transformation,[],[f10346]) ).
fof(f20858,plain,
val(c600,mandela_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20859,plain,
sub(c600,familiename_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20860,plain,
val(c599,nelson_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20861,plain,
sub(c599,eigenname_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20862,plain,
sub(c598,c1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20863,plain,
prop(c598,s__374dafrikanisch_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20864,plain,
attr(c598,c600),
inference(cnf_transformation,[],[f10346]) ).
fof(f20865,plain,
attr(c598,c599),
inference(cnf_transformation,[],[f10346]) ).
fof(f20871,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(f20872,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,[],[f20871]) ).
fof(f20874,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(f20875,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,[],[f20874]) ).
fof(f20876,plain,
( spl63_1
| spl63_2 ),
inference(avatar_split_clause,[],[f20816,f20874,f20871]) ).
fof(f20907,plain,
has_fact_leq(c598,real),
inference(resolution,[],[f10602,f20835]) ).
fof(f60093,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| val(sK48(X0,s__374dafrika_0),s__374dafrika_0) ),
inference(resolution,[],[f10852,f19789]) ).
fof(f60279,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| sub(sK48(X0,s__374dafrika_0),name_1_1) ),
inference(resolution,[],[f10853,f19789]) ).
fof(f60651,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| loc(X0,sK49(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10855,f19789]) ).
fof(f63020,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| attr(sK47(X0,s__374dafrika_0),sK48(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10856,f19789]) ).
fof(f63206,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| in(sK49(X0,s__374dafrika_0),sK47(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10857,f19789]) ).
fof(f71478,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| subs(sK50(X0),hei__337en_1_1)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10860,f10600]) ).
fof(f71480,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| arg2(sK50(X0),X0)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10861,f10600]) ).
fof(f71482,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| arg1(sK50(X0),X0)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10862,f10600]) ).
fof(f72333,plain,
val(sK48(c598,s__374dafrika_0),s__374dafrika_0),
inference(resolution,[],[f60093,f20863]) ).
fof(f72338,plain,
sub(sK48(c598,s__374dafrika_0),name_1_1),
inference(resolution,[],[f60279,f20863]) ).
fof(f72371,plain,
loc(c598,sK49(c598,s__374dafrika_0)),
inference(resolution,[],[f60651,f20863]) ).
fof(f72379,plain,
( ~ has_fact_leq(c598,real)
| obj(sK2(sK49(c598,s__374dafrika_0),c598),c598) ),
inference(resolution,[],[f72371,f10686]) ).
fof(f72390,plain,
obj(sK2(sK49(c598,s__374dafrika_0),c598),c598),
inference(forward_subsumption_resolution,[],[f72379,f20907]) ).
fof(f72593,plain,
attr(sK47(c598,s__374dafrika_0),sK48(c598,s__374dafrika_0)),
inference(resolution,[],[f63020,f20863]) ).
fof(f72594,plain,
( ! [X0] :
( ~ val(sK48(c598,s__374dafrika_0),s__374dafrika_0)
| ~ sub(sK48(c598,s__374dafrika_0),name_1_1)
| ~ in(X0,sK47(c598,s__374dafrika_0)) )
| ~ spl63_2 ),
inference(resolution,[],[f72593,f20875]) ).
fof(f72595,plain,
( ! [X0] :
( ~ sub(sK48(c598,s__374dafrika_0),name_1_1)
| ~ in(X0,sK47(c598,s__374dafrika_0)) )
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f72594,f72333]) ).
fof(f72596,plain,
( ! [X0] : ~ in(X0,sK47(c598,s__374dafrika_0))
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f72595,f72338]) ).
fof(f72597,plain,
in(sK49(c598,s__374dafrika_0),sK47(c598,s__374dafrika_0)),
inference(resolution,[],[f63206,f20863]) ).
fof(f72598,plain,
( $false
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f72597,f72596]) ).
fof(f72599,plain,
~ spl63_2,
inference(avatar_contradiction_clause,[],[f72598]) ).
fof(f76070,plain,
! [X0] :
( ~ attr(X0,c599)
| subs(sK50(X0),hei__337en_1_1) ),
inference(resolution,[],[f71478,f20861]) ).
fof(f76159,plain,
! [X0] :
( ~ attr(X0,c599)
| arg2(sK50(X0),X0) ),
inference(resolution,[],[f71480,f20861]) ).
fof(f76248,plain,
! [X0] :
( ~ attr(X0,c599)
| arg1(sK50(X0),X0) ),
inference(resolution,[],[f71482,f20861]) ).
fof(f84899,plain,
subs(sK50(c598),hei__337en_1_1),
inference(resolution,[],[f76070,f20865]) ).
fof(f84901,plain,
! [X0,X1] :
( ~ arg2(sK50(c598),X1)
| ~ arg1(sK50(c598),X0)
| subr(sK53(sK50(c598),X0,X1),rprs_0) ),
inference(resolution,[],[f84899,f10868]) ).
fof(f84905,plain,
! [X0,X1] :
( ~ arg2(sK50(c598),X1)
| ~ arg1(sK50(c598),X0)
| arg2(sK53(sK50(c598),X0,X1),X1) ),
inference(resolution,[],[f84899,f10872]) ).
fof(f84906,plain,
! [X0,X1] :
( ~ arg2(sK50(c598),X1)
| ~ arg1(sK50(c598),X0)
| arg1(sK53(sK50(c598),X0,X1),X0) ),
inference(resolution,[],[f84899,f10873]) ).
fof(f84919,plain,
arg2(sK50(c598),c598),
inference(resolution,[],[f76159,f20865]) ).
fof(f84922,definition,
( spl63_3138
<=> ! [X2] : ~ sub(c598,X2) ),
introduced(definition,[new_symbols(definition,[spl63_3138])],[avatar_definition]) ).
fof(f84923,plain,
( ! [X2] : ~ sub(c598,X2)
| ~ spl63_3138 ),
inference(avatar_component_clause,[],[f84922]) ).
fof(f84932,plain,
arg1(sK50(c598),c598),
inference(resolution,[],[f76248,f20865]) ).
fof(f86462,plain,
! [X0] :
( ~ arg1(sK50(c598),X0)
| subr(sK53(sK50(c598),X0,c598),rprs_0) ),
inference(resolution,[],[f84901,f84919]) ).
fof(f86463,plain,
subr(sK53(sK50(c598),c598,c598),rprs_0),
inference(resolution,[],[f86462,f84932]) ).
fof(f86472,plain,
! [X0] :
( ~ arg1(sK50(c598),X0)
| arg2(sK53(sK50(c598),X0,c598),c598) ),
inference(resolution,[],[f84905,f84919]) ).
fof(f86473,plain,
arg2(sK53(sK50(c598),c598,c598),c598),
inference(resolution,[],[f86472,f84932]) ).
fof(f86474,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ val(X0,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(sK53(sK50(c598),c598,c598),rprs_0)
| ~ sub(c598,X2)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X3,X4)
| ~ attr(X4,X0)
| ~ attr(X4,X1)
| ~ arg1(sK53(sK50(c598),c598,c598),X4) )
| ~ spl63_1 ),
inference(resolution,[],[f86473,f20872]) ).
fof(f86475,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ val(X0,nelson_0)
| ~ val(X1,mandela_0)
| ~ sub(c598,X2)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X3,X4)
| ~ attr(X4,X0)
| ~ attr(X4,X1)
| ~ arg1(sK53(sK50(c598),c598,c598),X4) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f86474,f86463]) ).
fof(f86477,definition,
( spl63_3243
<=> ! [X4,X0,X3,X1] :
( ~ val(X0,nelson_0)
| ~ arg1(sK53(sK50(c598),c598,c598),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_3243])],[avatar_definition]) ).
fof(f86478,plain,
( ! [X3,X0,X1,X4] :
( ~ arg1(sK53(sK50(c598),c598,c598),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_3243 ),
inference(avatar_component_clause,[],[f86477]) ).
fof(f86479,plain,
( spl63_3138
| spl63_3243
| ~ spl63_1 ),
inference(avatar_split_clause,[],[f86475,f20871,f86477,f84922]) ).
fof(f86480,plain,
( $false
| ~ spl63_3138 ),
inference(resolution,[],[f84923,f20862]) ).
fof(f86481,plain,
~ spl63_3138,
inference(avatar_contradiction_clause,[],[f86480]) ).
fof(f86482,plain,
! [X0] :
( ~ arg1(sK50(c598),X0)
| arg1(sK53(sK50(c598),X0,c598),X0) ),
inference(resolution,[],[f84906,f84919]) ).
fof(f86483,plain,
arg1(sK53(sK50(c598),c598,c598),c598),
inference(resolution,[],[f86482,f84932]) ).
fof(f86484,plain,
( ! [X2,X0,X1] :
( ~ val(X0,nelson_0)
| ~ attr(c598,X1)
| ~ obj(X2,c598)
| ~ attr(c598,X0)
| ~ sub(X0,eigenname_1_1)
| ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1) )
| ~ spl63_3243 ),
inference(resolution,[],[f86483,f86478]) ).
fof(f86487,definition,
( spl63_3244
<=> ! [X2] : ~ obj(X2,c598) ),
introduced(definition,[new_symbols(definition,[spl63_3244])],[avatar_definition]) ).
fof(f86488,plain,
( ! [X2] : ~ obj(X2,c598)
| ~ spl63_3244 ),
inference(avatar_component_clause,[],[f86487]) ).
fof(f86490,definition,
( spl63_3245
<=> ! [X1] :
( ~ attr(c598,X1)
| ~ sub(X1,familiename_1_1)
| ~ val(X1,mandela_0) ) ),
introduced(definition,[new_symbols(definition,[spl63_3245])],[avatar_definition]) ).
fof(f86491,plain,
( ! [X1] :
( ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1)
| ~ attr(c598,X1) )
| ~ spl63_3245 ),
inference(avatar_component_clause,[],[f86490]) ).
fof(f86493,definition,
( spl63_3246
<=> ! [X0] :
( ~ val(X0,nelson_0)
| ~ sub(X0,eigenname_1_1)
| ~ attr(c598,X0) ) ),
introduced(definition,[new_symbols(definition,[spl63_3246])],[avatar_definition]) ).
fof(f86494,plain,
( ! [X0] :
( ~ attr(c598,X0)
| ~ sub(X0,eigenname_1_1)
| ~ val(X0,nelson_0) )
| ~ spl63_3246 ),
inference(avatar_component_clause,[],[f86493]) ).
fof(f86495,plain,
( spl63_3244
| spl63_3245
| spl63_3246
| ~ spl63_3243 ),
inference(avatar_split_clause,[],[f86484,f86477,f86493,f86490,f86487]) ).
fof(f86496,plain,
( $false
| ~ spl63_3244 ),
inference(resolution,[],[f86488,f72390]) ).
fof(f86503,plain,
~ spl63_3244,
inference(avatar_contradiction_clause,[],[f86496]) ).
fof(f86504,plain,
( ~ sub(c600,familiename_1_1)
| ~ attr(c598,c600)
| ~ spl63_3245 ),
inference(resolution,[],[f86491,f20858]) ).
fof(f86505,plain,
( ~ attr(c598,c600)
| ~ spl63_3245 ),
inference(forward_subsumption_resolution,[],[f86504,f20859]) ).
fof(f86506,plain,
( $false
| ~ spl63_3245 ),
inference(forward_subsumption_resolution,[],[f86505,f20864]) ).
fof(f86507,plain,
~ spl63_3245,
inference(avatar_contradiction_clause,[],[f86506]) ).
fof(f86509,plain,
( ~ sub(c599,eigenname_1_1)
| ~ val(c599,nelson_0)
| ~ spl63_3246 ),
inference(resolution,[],[f86494,f20865]) ).
fof(f86510,plain,
( ~ val(c599,nelson_0)
| ~ spl63_3246 ),
inference(forward_subsumption_resolution,[],[f86509,f20861]) ).
fof(f86511,plain,
( $false
| ~ spl63_3246 ),
inference(forward_subsumption_resolution,[],[f86510,f20860]) ).
fof(f86512,plain,
~ spl63_3246,
inference(avatar_contradiction_clause,[],[f86511]) ).
cnf(s1,plain,
( spl63_1
| spl63_2 ),
inference(sat_conversion,[],[f20876]) ).
cnf(s75,plain,
~ spl63_2,
inference(sat_conversion,[],[f72599]) ).
cnf(s1174,plain,
( ~ spl63_1
| spl63_3138
| spl63_3243 ),
inference(sat_conversion,[],[f86479]) ).
cnf(s1175,plain,
~ spl63_3138,
inference(sat_conversion,[],[f86481]) ).
cnf(s1176,plain,
( ~ spl63_3243
| spl63_3244
| spl63_3245
| spl63_3246 ),
inference(sat_conversion,[],[f86495]) ).
cnf(s1180,plain,
~ spl63_3244,
inference(sat_conversion,[],[f86503]) ).
cnf(s1181,plain,
~ spl63_3245,
inference(sat_conversion,[],[f86507]) ).
cnf(s1182,plain,
~ spl63_3246,
inference(sat_conversion,[],[f86512]) ).
cnf(s1183,plain,
~ spl63_3243,
inference(rat,[],[s1176,s1182,s1181,s1180]) ).
cnf(s1184,plain,
~ spl63_1,
inference(rat,[],[s1174,s1183,s1175]) ).
cnf(s1191,plain,
$false,
inference(rat,[],[s1,s75,s1184]) ).
fof(f86513,plain,
$false,
inference(avatar_sat_refutation,[],[s1191]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR116+37 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Mon Sep 28 23:29:04 UTC 2026
% 0.08/0.11 % CPUTime :
% 0.08/0.11 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.13 Running first-order model finding
% 0.08/0.13 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
% 14.72/2.33 % (3898438)Will run a generic schedule for satisfiability detection.
% 14.72/2.33 % (3898444)% WARNING: option uhcvi not known.
% 14.72/2.33 % (3898443)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3031830088_2999 on theBenchmark for (2999ds/0Mi)
% 14.72/2.33 % (3898445)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1776695118:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 14.72/2.33 % (3898447)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=166614604:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 14.72/2.33 % (3898444)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2506751966:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 14.72/2.33 % (3898446)dis+10_1_sil=32000:sp=arity:random_seed=3951827697:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 14.72/2.33 % (3898448)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=112898022:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 14.72/2.33 % (3898449)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1561036417:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 14.72/2.33 % (3898446)Instruction limit reached!
% 14.72/2.33 % (3898446)------------------------------
% 14.72/2.33 % (3898446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.72/2.33 % (3898446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.33 % (3898446)CaDiCaL version: 2.1.3
% 14.72/2.33 % (3898446)Termination reason: Instruction limit
% 14.72/2.33 % (3898446)Termination phase: Saturation
% 14.72/2.33 % (3898446)Time elapsed: 0.034 s
% 14.72/2.33 % (3898446)Peak memory usage: 26 MB
% 14.72/2.33 % (3898446)Instructions burned: 107 (million)
% 14.72/2.33 % (3898447)Instruction limit reached!
% 14.72/2.33 % (3898447)------------------------------
% 14.72/2.33 % (3898447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.72/2.33 % (3898447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.33 % (3898447)CaDiCaL version: 2.1.3
% 14.72/2.33 % (3898447)Termination reason: Instruction limit
% 14.72/2.33 % (3898447)Termination phase: Blocked clause elimination
% 14.72/2.33 % (3898447)Time elapsed: 0.040 s
% 14.72/2.33 % (3898447)Peak memory usage: 27 MB
% 14.72/2.33 % (3898447)Instructions burned: 118 (million)
% 14.72/2.33 % (3898448)Instruction limit reached!
% 14.72/2.33 % (3898448)------------------------------
% 14.72/2.33 % (3898448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.72/2.33 % (3898448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.33 % (3898448)CaDiCaL version: 2.1.3
% 14.72/2.33 % (3898448)Termination reason: Instruction limit
% 14.72/2.33 % (3898448)Termination phase: Saturation
% 14.72/2.33 % (3898448)Time elapsed: 0.041 s
% 14.72/2.33 % (3898448)Peak memory usage: 28 MB
% 14.72/2.33 % (3898448)Instructions burned: 133 (million)
% 14.72/2.33 % (3898457)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1498554554:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 14.72/2.33 % (3898449)Instruction limit reached!
% 14.72/2.33 % (3898449)------------------------------
% 14.72/2.33 % (3898449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.72/2.33 % (3898449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.72/2.33 % (3898449)CaDiCaL version: 2.1.3
% 14.72/2.33 % (3898449)Termination reason: Instruction limit
% 14.72/2.33 % (3898449)Termination phase: Saturation
% 14.72/2.33 % (3898449)Time elapsed: 0.049 s
% 14.72/2.33 % (3898449)Peak memory usage: 30 MB
% 14.72/2.33 % (3898449)Instructions burned: 161 (million)
% 14.72/2.33 % (3898458)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3909439001:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.72/2.33 % (3898459)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=1112020514:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.72/2.33 % (3898461)ott-21_1_sil=16000:fs=off:random_seed=377881936:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 14.72/2.33 % (3898458)Instruction limit reached!
% 14.72/2.33 % (3898458)------------------------------
% 14.72/2.33 % (3898458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.72/2.33 % (3898458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.55/4.14 % (3898458)CaDiCaL version: 2.1.3
% 27.55/4.14 % (3898458)Termination reason: Instruction limit
% 27.55/4.14 % (3898458)Termination phase: Blocked clause elimination
% 27.55/4.14 % (3898458)Time elapsed: 0.044 s
% 27.55/4.14 % (3898458)Peak memory usage: 28 MB
% 27.55/4.14 % (3898458)Instructions burned: 134 (million)
% 27.55/4.14 % (3898465)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1036891191:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 27.55/4.14 % (3898461)Instruction limit reached!
% 27.55/4.14 % (3898461)------------------------------
% 27.55/4.14 % (3898461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.55/4.14 % (3898461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.55/4.14 % (3898461)CaDiCaL version: 2.1.3
% 27.55/4.14 % (3898461)Termination reason: Instruction limit
% 27.55/4.14 % (3898461)Termination phase: Saturation
% 27.55/4.14 % (3898461)Time elapsed: 0.051 s
% 27.55/4.14 % (3898461)Peak memory usage: 28 MB
% 27.55/4.14 % (3898461)Instructions burned: 182 (million)
% 27.55/4.14 % (3898467)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=166907582:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 27.55/4.14 % TRYING [1]
% 27.55/4.14 % TRYING [1]
% 27.55/4.14 % TRYING [2]
% 27.55/4.14 % TRYING [2]
% 27.55/4.14 % (3898457)Instruction limit reached!
% 27.55/4.14 % (3898457)------------------------------
% 27.55/4.14 % (3898457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.55/4.14 % (3898457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.55/4.14 % (3898457)CaDiCaL version: 2.1.3
% 27.55/4.14 % (3898457)Termination reason: Instruction limit
% 27.55/4.14 % (3898457)Termination phase: Finite model building constraint generation
% 27.55/4.14 % (3898457)Time elapsed: 0.191 s
% 27.55/4.14 % (3898457)Peak memory usage: 54 MB
% 27.55/4.14 % (3898457)Instructions burned: 715 (million)
% 27.55/4.14 % TRYING [1]
% 27.55/4.14 % (3898459)Instruction limit reached!
% 27.55/4.14 % (3898459)------------------------------
% 27.55/4.14 % (3898459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.55/4.14 % (3898459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.55/4.14 % (3898459)CaDiCaL version: 2.1.3
% 27.55/4.14 % (3898459)Termination reason: Instruction limit
% 27.55/4.14 % (3898459)Termination phase: Saturation
% 27.55/4.14 % (3898459)Time elapsed: 0.196 s
% 27.55/4.14 % (3898459)Peak memory usage: 33 MB
% 27.55/4.14 % (3898459)Instructions burned: 687 (million)
% 27.55/4.14 % (3898465)Instruction limit reached!
% 27.55/4.14 % (3898465)------------------------------
% 27.55/4.14 % (3898465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.55/4.14 % (3898465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.55/4.14 % (3898465)CaDiCaL version: 2.1.3
% 27.55/4.14 % (3898465)Termination reason: Instruction limit
% 27.55/4.14 % (3898465)Termination phase: Saturation
% 27.55/4.14 % (3898465)Time elapsed: 0.143 s
% 27.55/4.14 % (3898465)Peak memory usage: 39 MB
% 27.55/4.14 % (3898465)Instructions burned: 477 (million)
% 27.55/4.14 % (3898469)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1976970758:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 27.55/4.14 % (3898470)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2509976946:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 27.55/4.14 % (3898471)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=614689146:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 27.55/4.14 % (3898467)Instruction limit reached!
% 27.55/4.14 % (3898467)------------------------------
% 27.55/4.14 % (3898467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 27.55/4.14 % (3898467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.55/4.14 % (3898467)CaDiCaL version: 2.1.3
% 27.55/4.14 % (3898467)Termination reason: Instruction limit
% 27.55/4.14 % (3898467)Termination phase: Finite model building SAT solving
% 27.55/4.14 % (3898467)Time elapsed: 0.181 s
% 27.55/4.14 % (3898467)Peak memory usage: 38 MB
% 27.55/4.14 % (3898467)Instructions burned: 873 (million)
% 27.55/4.14 % TRYING [3]
% 27.55/4.14 % (3898475)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=716290753:i=879:kws=inv_precedence:fsr=off_2995 on theBenchmark for (2995ds/879Mi)
% 27.55/4.14 % (3898471)Instruction limit reached!
% 27.55/4.14 % (3898471)------------------------------
% 27.55/4.14 % (3898471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.09/9.37 % (3898471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.09/9.37 % (3898471)CaDiCaL version: 2.1.3
% 64.09/9.37 % (3898471)Termination reason: Instruction limit
% 64.09/9.37 % (3898471)Termination phase: Saturation
% 64.09/9.37 % (3898471)Time elapsed: 0.203 s
% 64.09/9.37 % (3898471)Peak memory usage: 42 MB
% 64.09/9.37 % (3898471)Instructions burned: 693 (million)
% 64.09/9.37 % (3898477)fmb+10_1_sil=64000:random_seed=598112472:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 64.09/9.37 % (3898470)Instruction limit reached!
% 64.09/9.37 % (3898470)------------------------------
% 64.09/9.37 % (3898470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.09/9.37 % (3898470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.09/9.37 % (3898470)CaDiCaL version: 2.1.3
% 64.09/9.37 % (3898470)Termination reason: Instruction limit
% 64.09/9.37 % (3898470)Termination phase: Finite model building constraint generation
% 64.09/9.37 % (3898470)Time elapsed: 0.255 s
% 64.09/9.37 % (3898470)Peak memory usage: 91 MB
% 64.09/9.37 % (3898470)Instructions burned: 892 (million)
% 64.09/9.37 % (3898479)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1845611246:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 64.09/9.37 % (3898475)Instruction limit reached!
% 64.09/9.37 % (3898475)------------------------------
% 64.09/9.37 % (3898475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.09/9.37 % (3898475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.09/9.37 % (3898475)CaDiCaL version: 2.1.3
% 64.09/9.37 % (3898475)Termination reason: Instruction limit
% 64.09/9.37 % (3898475)Termination phase: Saturation
% 64.09/9.37 % (3898475)Time elapsed: 0.230 s
% 64.09/9.37 % (3898475)Peak memory usage: 41 MB
% 64.09/9.37 % (3898475)Instructions burned: 883 (million)
% 64.09/9.37 % (3898481)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4195085728:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 64.09/9.37 % TRYING [1]
% 64.09/9.37 % (3898469)Instruction limit reached!
% 64.09/9.37 % (3898469)------------------------------
% 64.09/9.37 % (3898469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.09/9.37 % (3898469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.09/9.37 % (3898469)CaDiCaL version: 2.1.3
% 64.09/9.37 % (3898469)Termination reason: Instruction limit
% 64.09/9.37 % (3898469)Termination phase: Saturation
% 64.09/9.37 % (3898469)Time elapsed: 0.352 s
% 64.09/9.37 % (3898469)Peak memory usage: 54 MB
% 64.09/9.37 % (3898469)Instructions burned: 1179 (million)
% 64.09/9.37 % (3898483)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4078107739:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 64.09/9.37 % TRYING [20]
% 64.09/9.37 % TRYING [8]
% 64.09/9.37 % (3898481)Instruction limit reached!
% 64.09/9.37 % (3898481)------------------------------
% 64.09/9.37 % (3898481)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.09/9.37 % (3898481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.09/9.37 % (3898481)CaDiCaL version: 2.1.3
% 64.09/9.37 % (3898481)Termination reason: Instruction limit
% 64.09/9.37 % (3898481)Termination phase: Finite model building constraint generation
% 64.09/9.37 % (3898481)Time elapsed: 0.203 s
% 64.09/9.37 % (3898481)Peak memory usage: 64 MB
% 64.09/9.37 % (3898481)Instructions burned: 923 (million)
% 64.09/9.37 % (3898485)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=754253909:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 64.09/9.37 % TRYING [2]
% 64.09/9.37 % (3898485)Instruction limit reached!
% 64.09/9.37 % (3898485)------------------------------
% 64.09/9.37 % (3898485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 64.09/9.37 % (3898485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.09/9.37 % (3898485)CaDiCaL version: 2.1.3
% 64.09/9.37 % (3898485)Termination reason: Instruction limit
% 64.09/9.37 % (3898485)Termination phase: Saturation
% 64.09/9.37 % (3898485)Time elapsed: 0.359 s
% 64.09/9.37 % (3898485)Peak memory usage: 35 MB
% 64.09/9.37 % (3898485)Instructions burned: 1472 (million)
% 64.09/9.37 % (3898489)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3965961230:i=6324_2987 on theBenchmark for (2987ds/6324Mi)
% 64.09/9.37 % TRYING [3]
% 64.09/9.37 % TRYING [77]
% 64.09/9.37 % TRYING [4]
% 64.09/9.37 % TRYING [4]
% 64.09/9.37 % (3898483)Instruction limit reached!
% 64.09/9.37 % (3898483)------------------------------
% 64.09/9.37 % (3898483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.43/21.40 % (3898483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.43/21.40 % (3898483)CaDiCaL version: 2.1.3
% 149.43/21.40 % (3898483)Termination reason: Instruction limit
% 149.43/21.40 % (3898483)Termination phase: Saturation
% 149.43/21.40 % (3898483)Time elapsed: 1.473 s
% 149.43/21.40 % (3898483)Peak memory usage: 39 MB
% 149.43/21.40 % (3898483)Instructions burned: 5134 (million)
% 149.43/21.40 % (3898491)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1247930636:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 149.43/21.40 % TRYING [16]
% 149.43/21.40 % (3898479)Instruction limit reached!
% 149.43/21.40 % (3898479)------------------------------
% 149.43/21.40 % (3898479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.43/21.40 % (3898479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.43/21.40 % (3898479)CaDiCaL version: 2.1.3
% 149.43/21.40 % (3898479)Termination reason: Instruction limit
% 149.43/21.40 % (3898479)Termination phase: Finite model building constraint generation
% 149.43/21.40 % (3898479)Time elapsed: 1.837 s
% 149.43/21.40 % (3898479)Peak memory usage: 551 MB
% 149.43/21.40 % (3898479)Instructions burned: 9517 (million)
% 149.43/21.40 % (3898489)Instruction limit reached!
% 149.43/21.40 % (3898489)------------------------------
% 149.43/21.40 % (3898489)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.43/21.40 % (3898489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.43/21.40 % (3898489)CaDiCaL version: 2.1.3
% 149.43/21.40 % (3898489)Termination reason: Instruction limit
% 149.43/21.40 % (3898489)Termination phase: Finite model building constraint generation
% 149.43/21.40 % (3898489)Time elapsed: 1.250 s
% 149.43/21.40 % (3898489)Peak memory usage: 417 MB
% 149.43/21.40 % (3898489)Instructions burned: 6324 (million)
% 149.43/21.40 % (3898493)ott-2_1_sil=16000:newcnf=on:random_seed=3984714191:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2974 on theBenchmark for (2974ds/869Mi)
% 149.43/21.40 % (3898495)ott+10_1_sil=32000:tgt=ground:random_seed=3845256075:i=5114:av=off_2974 on theBenchmark for (2974ds/5114Mi)
% 149.43/21.40 % (3898491)Instruction limit reached!
% 149.43/21.40 % (3898491)------------------------------
% 149.43/21.40 % (3898491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.43/21.40 % (3898491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.43/21.40 % (3898491)CaDiCaL version: 2.1.3
% 149.43/21.40 % (3898491)Termination reason: Instruction limit
% 149.43/21.40 % (3898491)Termination phase: Finite model building constraint generation
% 149.43/21.40 % (3898491)Time elapsed: 0.422 s
% 149.43/21.40 % (3898491)Peak memory usage: 121 MB
% 149.43/21.40 % (3898491)Instructions burned: 2176 (million)
% 149.43/21.40 % (3898497)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3749215429:i=54282_2973 on theBenchmark for (2973ds/54282Mi)
% 149.43/21.40 % (3898493)Instruction limit reached!
% 149.43/21.40 % (3898493)------------------------------
% 149.43/21.40 % (3898493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.43/21.40 % (3898493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.43/21.40 % (3898493)CaDiCaL version: 2.1.3
% 149.43/21.40 % (3898493)Termination reason: Instruction limit
% 149.43/21.40 % (3898493)Termination phase: Saturation
% 149.43/21.40 % (3898493)Time elapsed: 0.237 s
% 149.43/21.40 % (3898493)Peak memory usage: 38 MB
% 149.43/21.40 % (3898493)Instructions burned: 870 (million)
% 149.43/21.40 % (3898499)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2437450045:i=3512:aac=none_2972 on theBenchmark for (2972ds/3512Mi)
% 149.43/21.40 % TRYING [1]
% 149.43/21.40 % TRYING [2]
% 149.43/21.40 % TRYING [3]
% 149.43/21.40 % (3898499)Instruction limit reached!
% 149.43/21.40 % (3898499)------------------------------
% 149.43/21.40 % (3898499)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 149.43/21.40 % (3898499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 149.43/21.40 % (3898499)CaDiCaL version: 2.1.3
% 149.43/21.40 % (3898499)Termination reason: Instruction limit
% 149.43/21.40 % (3898499)Termination phase: Saturation
% 149.43/21.40 % (3898499)Time elapsed: 0.947 s
% 149.43/21.40 % (3898499)Peak memory usage: 41 MB
% 149.43/21.40 % (3898499)Instructions burned: 3512 (million)
% 149.43/21.40 % (3898501)dis+21_1_sil=32000:sas=cadical:random_seed=112850378:i=3773:amm=off_2962 on theBenchmark for (2962ds/3773Mi)
% 149.43/21.40 % (3898495)Instruction limit reached!
% 149.43/21.40 % (3898495)------------------------------
% 149.43/21.40 % (3898495)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898495)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898495)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898495)Termination reason: Instruction limit
% 119.73/24.74 % (3898495)Termination phase: Saturation
% 119.73/24.74 % (3898495)Time elapsed: 1.446 s
% 119.73/24.74 % (3898495)Peak memory usage: 120 MB
% 119.73/24.74 % (3898495)Instructions burned: 5114 (million)
% 119.73/24.74 % (3898503)ott+11_1_sil=16000:gs=on:random_seed=672130282:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2959 on theBenchmark for (2959ds/2251Mi)
% 119.73/24.74 % TRYING [4]
% 119.73/24.74 % (3898503)Instruction limit reached!
% 119.73/24.74 % (3898503)------------------------------
% 119.73/24.74 % (3898503)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898503)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898503)Termination reason: Instruction limit
% 119.73/24.74 % (3898503)Termination phase: Saturation
% 119.73/24.74 % (3898503)Time elapsed: 0.618 s
% 119.73/24.74 % (3898503)Peak memory usage: 68 MB
% 119.73/24.74 % (3898503)Instructions burned: 2253 (million)
% 119.73/24.74 % (3898505)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4043821760:fmbsr=1.6:i=67534_2953 on theBenchmark for (2953ds/67534Mi)
% 119.73/24.74 % (3898501)Instruction limit reached!
% 119.73/24.74 % (3898501)------------------------------
% 119.73/24.74 % (3898501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898501)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898501)Termination reason: Instruction limit
% 119.73/24.74 % (3898501)Termination phase: Saturation
% 119.73/24.74 % (3898501)Time elapsed: 0.987 s
% 119.73/24.74 % (3898501)Peak memory usage: 67 MB
% 119.73/24.74 % (3898501)Instructions burned: 3775 (million)
% 119.73/24.74 % (3898507)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2073686742:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2952 on theBenchmark for (2952ds/4591Mi)
% 119.73/24.74 % TRYING [7]
% 119.73/24.74 % TRYING [5]
% 119.73/24.74 % (3898507)Instruction limit reached!
% 119.73/24.74 % (3898507)------------------------------
% 119.73/24.74 % (3898507)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898507)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898507)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898507)Termination reason: Instruction limit
% 119.73/24.74 % (3898507)Termination phase: Saturation
% 119.73/24.74 % (3898507)Time elapsed: 1.122 s
% 119.73/24.74 % (3898507)Peak memory usage: 45 MB
% 119.73/24.74 % (3898507)Instructions burned: 4595 (million)
% 119.73/24.74 % (3898509)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3780092193:i=29340_2941 on theBenchmark for (2941ds/29340Mi)
% 119.73/24.74 % (3898477)Instruction limit reached!
% 119.73/24.74 % (3898477)------------------------------
% 119.73/24.74 % (3898477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898477)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898477)Termination reason: Instruction limit
% 119.73/24.74 % (3898477)Termination phase: Finite model building SAT solving
% 119.73/24.74 % (3898477)Time elapsed: 6.004 s
% 119.73/24.74 % (3898477)Peak memory usage: 104 MB
% 119.73/24.74 % (3898477)Instructions burned: 22063 (million)
% 119.73/24.74 % (3898511)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=706018344:i=5211_2934 on theBenchmark for (2934ds/5211Mi)
% 119.73/24.74 % (3898511)Instruction limit reached!
% 119.73/24.74 % (3898511)------------------------------
% 119.73/24.74 % (3898511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898511)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898511)Termination reason: Instruction limit
% 119.73/24.74 % (3898511)Termination phase: Saturation
% 119.73/24.74 % (3898511)Time elapsed: 1.479 s
% 119.73/24.74 % (3898511)Peak memory usage: 51 MB
% 119.73/24.74 % (3898511)Instructions burned: 5215 (million)
% 119.73/24.74 % (3898513)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2058079791:i=5497:nm=2_2919 on theBenchmark for (2919ds/5497Mi)
% 119.73/24.74 % TRYING [17]
% 119.73/24.74 % (3898513)Instruction limit reached!
% 119.73/24.74 % (3898513)------------------------------
% 119.73/24.74 % (3898513)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898513)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898513)Termination reason: Instruction limit
% 119.73/24.74 % (3898513)Termination phase: Finite model building constraint generation
% 119.73/24.74 % (3898513)Time elapsed: 1.125 s
% 119.73/24.74 % (3898513)Peak memory usage: 351 MB
% 119.73/24.74 % (3898513)Instructions burned: 5499 (million)
% 119.73/24.74 % (3898515)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2963557846:fmbsr=2:i=46332_2907 on theBenchmark for (2907ds/46332Mi)
% 119.73/24.74 % TRYING [15]
% 119.73/24.74 % TRYING [5]
% 119.73/24.74 % (3898509)Instruction limit reached!
% 119.73/24.74 % (3898509)------------------------------
% 119.73/24.74 % (3898509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898509)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898509)Termination reason: Instruction limit
% 119.73/24.74 % (3898509)Termination phase: Saturation
% 119.73/24.74 % (3898509)Time elapsed: 7.140 s
% 119.73/24.74 % (3898509)Peak memory usage: 78 MB
% 119.73/24.74 % (3898509)Instructions burned: 29340 (million)
% 119.73/24.74 % (3898517)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3038573158:i=14071_2869 on theBenchmark for (2869ds/14071Mi)
% 119.73/24.74 % TRYING [12]
% 119.73/24.74 % TRYING [6]
% 119.73/24.74 % (3898445)Instruction limit reached!
% 119.73/24.74 % (3898445)------------------------------
% 119.73/24.74 % (3898445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898445)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898445)Termination reason: Instruction limit
% 119.73/24.74 % (3898445)Termination phase: Saturation
% 119.73/24.74 % (3898445)Time elapsed: 16.529 s
% 119.73/24.74 % (3898445)Peak memory usage: 143 MB
% 119.73/24.74 % (3898445)Instructions burned: 88026 (million)
% 119.73/24.74 % (3898519)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=407913934:i=22565:add=on:rawr=on_2833 on theBenchmark for (2833ds/22565Mi)
% 119.73/24.74 % (3898517)Instruction limit reached!
% 119.73/24.74 % (3898517)------------------------------
% 119.73/24.74 % (3898517)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898517)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898517)Termination reason: Instruction limit
% 119.73/24.74 % (3898517)Termination phase: Finite model building constraint generation
% 119.73/24.74 % (3898517)Time elapsed: 3.922 s
% 119.73/24.74 % (3898517)Peak memory usage: 1122 MB
% 119.73/24.74 % (3898517)Instructions burned: 14073 (million)
% 119.73/24.74 % (3898521)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4282064409:i=8173:av=off_2829 on theBenchmark for (2829ds/8173Mi)
% 119.73/24.74 % (3898497)Instruction limit reached!
% 119.73/24.74 % (3898497)------------------------------
% 119.73/24.74 % (3898497)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898497)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898497)Termination reason: Instruction limit
% 119.73/24.74 % (3898497)Termination phase: Finite model building SAT solving
% 119.73/24.74 % (3898497)Time elapsed: 16.471 s
% 119.73/24.74 % (3898497)Peak memory usage: 258 MB
% 119.73/24.74 % (3898497)Instructions burned: 54284 (million)
% 119.73/24.74 % (3898523)dis+10_16:1_sil=16000:random_seed=718982040:i=9155:fsr=off_2808 on theBenchmark for (2808ds/9155Mi)
% 119.73/24.74 % (3898521)Instruction limit reached!
% 119.73/24.74 % (3898521)------------------------------
% 119.73/24.74 % (3898521)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898521)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898521)Termination reason: Instruction limit
% 119.73/24.74 % (3898521)Termination phase: Saturation
% 119.73/24.74 % (3898521)Time elapsed: 2.591 s
% 119.73/24.74 % (3898521)Peak memory usage: 192 MB
% 119.73/24.74 % (3898521)Instructions burned: 8174 (million)
% 119.73/24.74 % (3898525)ott-3_8_sil=64000:random_seed=2397293879:i=20139:bs=on_2802 on theBenchmark for (2802ds/20139Mi)
% 119.73/24.74 % (3898523)Instruction limit reached!
% 119.73/24.74 % (3898523)------------------------------
% 119.73/24.74 % (3898523)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898523)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898523)Termination reason: Instruction limit
% 119.73/24.74 % (3898523)Termination phase: Saturation
% 119.73/24.74 % (3898523)Time elapsed: 2.105 s
% 119.73/24.74 % (3898523)Peak memory usage: 82 MB
% 119.73/24.74 % (3898523)Instructions burned: 9159 (million)
% 119.73/24.74 % (3898527)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=294306478:fmbsr=2:i=32576_2787 on theBenchmark for (2787ds/32576Mi)
% 119.73/24.74 % (3898519)Instruction limit reached!
% 119.73/24.74 % (3898519)------------------------------
% 119.73/24.74 % (3898519)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898519)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898519)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898519)Termination reason: Instruction limit
% 119.73/24.74 % (3898519)Termination phase: Saturation
% 119.73/24.74 % (3898519)Time elapsed: 4.642 s
% 119.73/24.74 % (3898519)Peak memory usage: 130 MB
% 119.73/24.74 % (3898519)Instructions burned: 22568 (million)
% 119.73/24.74 % (3898529)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3193336395:i=11404_2786 on theBenchmark for (2786ds/11404Mi)
% 119.73/24.74 % (3898505)Instruction limit reached!
% 119.73/24.74 % (3898505)------------------------------
% 119.73/24.74 % (3898505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898505)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898505)Termination reason: Instruction limit
% 119.73/24.74 % (3898505)Termination phase: Finite model building SAT solving
% 119.73/24.74 % (3898505)Time elapsed: 16.720 s
% 119.73/24.74 % (3898505)Peak memory usage: 288 MB
% 119.73/24.74 % (3898505)Instructions burned: 67538 (million)
% 119.73/24.74 % (3898531)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=3447083054:i=14134_2785 on theBenchmark for (2785ds/14134Mi)
% 119.73/24.74 % TRYING [9]
% 119.73/24.74 % (3898515)Instruction limit reached!
% 119.73/24.74 % (3898515)------------------------------
% 119.73/24.74 % (3898515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898515)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898515)Termination reason: Instruction limit
% 119.73/24.74 % (3898515)Termination phase: Finite model building constraint generation
% 119.73/24.74 % (3898515)Time elapsed: 13.532 s
% 119.73/24.74 % (3898515)Peak memory usage: 3369 MB
% 119.73/24.74 % (3898515)Instructions burned: 46333 (million)
% 119.73/24.74 % (3898533)dis+33_16_sil=32000:sac=on:random_seed=3793033402:i=15851:nm=0_2768 on theBenchmark for (2768ds/15851Mi)
% 119.73/24.74 % (3898529)Instruction limit reached!
% 119.73/24.74 % (3898529)------------------------------
% 119.73/24.74 % (3898529)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.74 % (3898529)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.74 % (3898529)CaDiCaL version: 2.1.3
% 119.73/24.74 % (3898529)Termination reason: Instruction limit
% 119.73/24.74 % (3898529)Termination phase: Saturation
% 119.73/24.74 % (3898529)Time elapsed: 2.841 s
% 119.73/24.74 % (3898529)Peak memory usage: 147 MB
% 119.73/24.74 % (3898529)Instructions burned: 11407 (million)
% 119.73/24.74 % (3898535)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1915248475:avsq=on:i=17627:add=on:amm=off_2758 on theBenchmark for (2758ds/17627Mi)
% 119.73/24.74 % (3898533) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3898438-3898533"...
% 119.73/24.74 % (3898533)...printing done.
% 119.73/24.74 % (3898533)Refutation found. Thanks to Tanya!
% 119.73/24.74 % SZS status Theorem for theBenchmark
% 119.73/24.74 % SZS output start Proof for theBenchmark
% See solution above
% 119.73/24.75 % (3898533)------------------------------
% 119.73/24.75 % (3898533)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 119.73/24.75 % (3898533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 119.73/24.75 % (3898533)CaDiCaL version: 2.1.3
% 119.73/24.75 % (3898533)Termination reason: Refutation
% 119.73/24.75 % (3898533)Time elapsed: 1.389 s
% 119.73/24.75 % (3898533)Peak memory usage: 79 MB
% 119.73/24.75 % (3898533)Instructions burned: 5381 (million)
% 119.73/24.75 % (3898438)Success in time 24.604 s
% 119.73/24.75 % Vampire exiting
%------------------------------------------------------------------------------