%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR116+41 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n011.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:52 AM UTC 2026
% Result : Theorem 273.22s 41.03s
% Output : Refutation 273.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 10
% Syntax : Number of formulae : 100 ( 32 unt; 5 def)
% Number of atoms : 1737 ( 0 equ)
% Maximal formula atoms : 247 ( 17 avg)
% Number of connectives : 1868 ( 231 ~; 203 |;1427 &)
% ( 5 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 247 ( 20 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 32 ( 31 usr; 6 prp; 0-3 aty)
% Number of functors : 70 ( 70 usr; 66 con; 0-3 aty)
% Number of variables : 160 ( 0 sgn 133 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax',member_first) ).
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/sandbox/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/sandbox/benchmark/Axioms/CSR004+0.ax',hei__337en_1_1__bezeichnen_1_1_als) ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( pmod(X8,erst_1_1,pr__344sident_1_1)
& arg1(X3,X0)
& arg2(X3,X4)
& attr(X0,X1)
& attr(X0,X2)
& attr(X5,X6)
& obj(X7,X0)
& prop(X4,schwarz_1_1)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X8)
& sub(X6,name_1_1)
& subr(X3,rprs_0)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X6,s__374dafrika_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',synth_qa07_010_mn3_283) ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( pmod(X8,erst_1_1,pr__344sident_1_1)
& arg1(X3,X0)
& arg2(X3,X4)
& attr(X0,X1)
& attr(X0,X2)
& attr(X5,X6)
& obj(X7,X0)
& prop(X4,schwarz_1_1)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X8)
& sub(X6,name_1_1)
& subr(X3,rprs_0)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X6,s__374dafrika_0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( equ(c11,c11)
& obj(c11,c161)
& prop(c11,afrikanisch__1_1)
& subs(c11,feier__1_1)
& subs(c11,vereidigung_1_1)
& temp(c11,c167)
& pmod(c151,erst_1_1,pr__344sident_1_1)
& attch(c155,c161)
& attr(c155,c156)
& sub(c155,land_1_1)
& sub(c156,name_1_1)
& val(c156,s__374dafrika_0)
& attr(c161,c162)
& attr(c161,c163)
& loc(c161,c180)
& prop(c161,schwarz_1_1)
& sub(c161,c151)
& sub(c162,eigenname_1_1)
& val(c162,nelson_0)
& sub(c163,familiename_1_1)
& val(c163,mandela_0)
& sub(c167,dienstag__1_1)
& attr(c177,c178)
& sub(c177,hauptsstadt_1_1)
& sub(c178,name_1_1)
& val(c178,pretoria_0)
& in(c180,c177)
& attch(c20,c11)
& prop(c20,ausgelassen_1_1)
& subs(c20,freude_1_1)
& arg1(c23,c11)
& arg2(c23,c11)
& subr(c23,equ_0)
& sub(hauptsstadt_1_1,stadt__1_1)
& sub(pr__344sident_1_1,mensch_1_1)
& sort(c11,ad)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,indet)
& varia(c11,varia_c)
& sort(c161,d)
& card(c161,int1)
& etype(c161,int0)
& fact(c161,real)
& gener(c161,sp)
& quant(c161,one)
& refer(c161,det)
& varia(c161,con)
& sort(afrikanisch__1_1,nq)
& sort(feier__1_1,ad)
& card(feier__1_1,int1)
& etype(feier__1_1,int0)
& fact(feier__1_1,real)
& gener(feier__1_1,ge)
& quant(feier__1_1,one)
& refer(feier__1_1,refer_c)
& varia(feier__1_1,varia_c)
& sort(vereidigung_1_1,ad)
& card(vereidigung_1_1,int1)
& etype(vereidigung_1_1,int0)
& fact(vereidigung_1_1,real)
& gener(vereidigung_1_1,ge)
& quant(vereidigung_1_1,one)
& refer(vereidigung_1_1,refer_c)
& varia(vereidigung_1_1,varia_c)
& sort(c167,ta)
& card(c167,int1)
& etype(c167,int0)
& fact(c167,real)
& gener(c167,sp)
& quant(c167,one)
& refer(c167,det)
& varia(c167,con)
& sort(c151,d)
& card(c151,int1)
& etype(c151,int0)
& fact(c151,real)
& gener(c151,ge)
& quant(c151,one)
& refer(c151,refer_c)
& varia(c151,varia_c)
& sort(erst_1_1,oq)
& card(erst_1_1,int1)
& 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(c155,d)
& sort(c155,io)
& card(c155,int1)
& etype(c155,int0)
& fact(c155,real)
& gener(c155,sp)
& quant(c155,one)
& refer(c155,det)
& varia(c155,con)
& sort(c156,na)
& card(c156,int1)
& etype(c156,int0)
& fact(c156,real)
& gener(c156,sp)
& quant(c156,one)
& refer(c156,indet)
& varia(c156,varia_c)
& sort(land_1_1,d)
& sort(land_1_1,io)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& quant(land_1_1,one)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(s__374dafrika_0,fe)
& sort(c162,na)
& card(c162,int1)
& etype(c162,int0)
& fact(c162,real)
& gener(c162,sp)
& quant(c162,one)
& refer(c162,indet)
& varia(c162,varia_c)
& sort(c163,na)
& card(c163,int1)
& etype(c163,int0)
& fact(c163,real)
& gener(c163,sp)
& quant(c163,one)
& refer(c163,indet)
& varia(c163,varia_c)
& sort(c180,l)
& card(c180,int1)
& etype(c180,int0)
& fact(c180,real)
& gener(c180,sp)
& quant(c180,one)
& refer(c180,det)
& varia(c180,con)
& sort(schwarz_1_1,tq)
& 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(dienstag__1_1,ta)
& card(dienstag__1_1,int1)
& etype(dienstag__1_1,int0)
& fact(dienstag__1_1,real)
& gener(dienstag__1_1,ge)
& quant(dienstag__1_1,one)
& refer(dienstag__1_1,refer_c)
& varia(dienstag__1_1,varia_c)
& sort(c177,d)
& sort(c177,io)
& card(c177,int1)
& etype(c177,int0)
& fact(c177,real)
& gener(c177,sp)
& quant(c177,one)
& refer(c177,det)
& varia(c177,con)
& sort(c178,na)
& card(c178,int1)
& etype(c178,int0)
& fact(c178,real)
& gener(c178,sp)
& quant(c178,one)
& refer(c178,indet)
& varia(c178,varia_c)
& sort(hauptsstadt_1_1,d)
& sort(hauptsstadt_1_1,io)
& card(hauptsstadt_1_1,int1)
& etype(hauptsstadt_1_1,int0)
& fact(hauptsstadt_1_1,real)
& gener(hauptsstadt_1_1,ge)
& quant(hauptsstadt_1_1,one)
& refer(hauptsstadt_1_1,refer_c)
& varia(hauptsstadt_1_1,varia_c)
& sort(pretoria_0,fe)
& sort(c20,ad)
& card(c20,int1)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& quant(c20,one)
& refer(c20,det)
& varia(c20,con)
& sort(ausgelassen_1_1,ql)
& sort(freude_1_1,ad)
& card(freude_1_1,int1)
& etype(freude_1_1,int0)
& fact(freude_1_1,real)
& gener(freude_1_1,ge)
& quant(freude_1_1,one)
& refer(freude_1_1,refer_c)
& varia(freude_1_1,varia_c)
& sort(c23,st)
& fact(c23,real)
& gener(c23,sp)
& sort(equ_0,st)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(mensch_1_1,ent)
& card(mensch_1_1,card_c)
& etype(mensch_1_1,etype_c)
& fact(mensch_1_1,real)
& gener(mensch_1_1,gener_c)
& quant(mensch_1_1,quant_c)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mn3_283) ).
fof(f10191,plain,
( obj(c11,c161)
& prop(c11,afrikanisch__1_1)
& subs(c11,feier__1_1)
& subs(c11,vereidigung_1_1)
& temp(c11,c167)
& pmod(c151,erst_1_1,pr__344sident_1_1)
& attch(c155,c161)
& attr(c155,c156)
& sub(c155,land_1_1)
& sub(c156,name_1_1)
& val(c156,s__374dafrika_0)
& attr(c161,c162)
& attr(c161,c163)
& loc(c161,c180)
& prop(c161,schwarz_1_1)
& sub(c161,c151)
& sub(c162,eigenname_1_1)
& val(c162,nelson_0)
& sub(c163,familiename_1_1)
& val(c163,mandela_0)
& sub(c167,dienstag__1_1)
& attr(c177,c178)
& sub(c177,hauptsstadt_1_1)
& sub(c178,name_1_1)
& val(c178,pretoria_0)
& in(c180,c177)
& attch(c20,c11)
& prop(c20,ausgelassen_1_1)
& subs(c20,freude_1_1)
& arg1(c23,c11)
& arg2(c23,c11)
& subr(c23,equ_0)
& sub(hauptsstadt_1_1,stadt__1_1)
& sub(pr__344sident_1_1,mensch_1_1)
& sort(c11,ad)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,indet)
& varia(c11,varia_c)
& sort(c161,d)
& card(c161,int1)
& etype(c161,int0)
& fact(c161,real)
& gener(c161,sp)
& quant(c161,one)
& refer(c161,det)
& varia(c161,con)
& sort(afrikanisch__1_1,nq)
& sort(feier__1_1,ad)
& card(feier__1_1,int1)
& etype(feier__1_1,int0)
& fact(feier__1_1,real)
& gener(feier__1_1,ge)
& quant(feier__1_1,one)
& refer(feier__1_1,refer_c)
& varia(feier__1_1,varia_c)
& sort(vereidigung_1_1,ad)
& card(vereidigung_1_1,int1)
& etype(vereidigung_1_1,int0)
& fact(vereidigung_1_1,real)
& gener(vereidigung_1_1,ge)
& quant(vereidigung_1_1,one)
& refer(vereidigung_1_1,refer_c)
& varia(vereidigung_1_1,varia_c)
& sort(c167,ta)
& card(c167,int1)
& etype(c167,int0)
& fact(c167,real)
& gener(c167,sp)
& quant(c167,one)
& refer(c167,det)
& varia(c167,con)
& sort(c151,d)
& card(c151,int1)
& etype(c151,int0)
& fact(c151,real)
& gener(c151,ge)
& quant(c151,one)
& refer(c151,refer_c)
& varia(c151,varia_c)
& sort(erst_1_1,oq)
& card(erst_1_1,int1)
& 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(c155,d)
& sort(c155,io)
& card(c155,int1)
& etype(c155,int0)
& fact(c155,real)
& gener(c155,sp)
& quant(c155,one)
& refer(c155,det)
& varia(c155,con)
& sort(c156,na)
& card(c156,int1)
& etype(c156,int0)
& fact(c156,real)
& gener(c156,sp)
& quant(c156,one)
& refer(c156,indet)
& varia(c156,varia_c)
& sort(land_1_1,d)
& sort(land_1_1,io)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& quant(land_1_1,one)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(s__374dafrika_0,fe)
& sort(c162,na)
& card(c162,int1)
& etype(c162,int0)
& fact(c162,real)
& gener(c162,sp)
& quant(c162,one)
& refer(c162,indet)
& varia(c162,varia_c)
& sort(c163,na)
& card(c163,int1)
& etype(c163,int0)
& fact(c163,real)
& gener(c163,sp)
& quant(c163,one)
& refer(c163,indet)
& varia(c163,varia_c)
& sort(c180,l)
& card(c180,int1)
& etype(c180,int0)
& fact(c180,real)
& gener(c180,sp)
& quant(c180,one)
& refer(c180,det)
& varia(c180,con)
& sort(schwarz_1_1,tq)
& 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(dienstag__1_1,ta)
& card(dienstag__1_1,int1)
& etype(dienstag__1_1,int0)
& fact(dienstag__1_1,real)
& gener(dienstag__1_1,ge)
& quant(dienstag__1_1,one)
& refer(dienstag__1_1,refer_c)
& varia(dienstag__1_1,varia_c)
& sort(c177,d)
& sort(c177,io)
& card(c177,int1)
& etype(c177,int0)
& fact(c177,real)
& gener(c177,sp)
& quant(c177,one)
& refer(c177,det)
& varia(c177,con)
& sort(c178,na)
& card(c178,int1)
& etype(c178,int0)
& fact(c178,real)
& gener(c178,sp)
& quant(c178,one)
& refer(c178,indet)
& varia(c178,varia_c)
& sort(hauptsstadt_1_1,d)
& sort(hauptsstadt_1_1,io)
& card(hauptsstadt_1_1,int1)
& etype(hauptsstadt_1_1,int0)
& fact(hauptsstadt_1_1,real)
& gener(hauptsstadt_1_1,ge)
& quant(hauptsstadt_1_1,one)
& refer(hauptsstadt_1_1,refer_c)
& varia(hauptsstadt_1_1,varia_c)
& sort(pretoria_0,fe)
& sort(c20,ad)
& card(c20,int1)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& quant(c20,one)
& refer(c20,det)
& varia(c20,con)
& sort(ausgelassen_1_1,ql)
& sort(freude_1_1,ad)
& card(freude_1_1,int1)
& etype(freude_1_1,int0)
& fact(freude_1_1,real)
& gener(freude_1_1,ge)
& quant(freude_1_1,one)
& refer(freude_1_1,refer_c)
& varia(freude_1_1,varia_c)
& sort(c23,st)
& fact(c23,real)
& gener(c23,sp)
& sort(equ_0,st)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(mensch_1_1,ent)
& card(mensch_1_1,card_c)
& etype(mensch_1_1,etype_c)
& fact(mensch_1_1,real)
& gener(mensch_1_1,gener_c)
& quant(mensch_1_1,quant_c)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10327,plain,
( obj(c11,c161)
& prop(c11,afrikanisch__1_1)
& subs(c11,feier__1_1)
& subs(c11,vereidigung_1_1)
& temp(c11,c167)
& pmod(c151,erst_1_1,pr__344sident_1_1)
& attch(c155,c161)
& attr(c155,c156)
& sub(c155,land_1_1)
& sub(c156,name_1_1)
& val(c156,s__374dafrika_0)
& attr(c161,c162)
& attr(c161,c163)
& loc(c161,c180)
& prop(c161,schwarz_1_1)
& sub(c161,c151)
& sub(c162,eigenname_1_1)
& val(c162,nelson_0)
& sub(c163,familiename_1_1)
& val(c163,mandela_0)
& sub(c167,dienstag__1_1)
& attr(c177,c178)
& sub(c177,hauptsstadt_1_1)
& sub(c178,name_1_1)
& val(c178,pretoria_0)
& in(c180,c177)
& attch(c20,c11)
& prop(c20,ausgelassen_1_1)
& subs(c20,freude_1_1)
& arg1(c23,c11)
& arg2(c23,c11)
& subr(c23,equ_0)
& sub(hauptsstadt_1_1,stadt__1_1)
& sub(pr__344sident_1_1,mensch_1_1)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& quant(c11,one)
& refer(c11,indet)
& varia(c11,varia_c)
& card(c161,int1)
& etype(c161,int0)
& fact(c161,real)
& gener(c161,sp)
& quant(c161,one)
& refer(c161,det)
& varia(c161,con)
& card(feier__1_1,int1)
& etype(feier__1_1,int0)
& fact(feier__1_1,real)
& gener(feier__1_1,ge)
& quant(feier__1_1,one)
& refer(feier__1_1,refer_c)
& varia(feier__1_1,varia_c)
& card(vereidigung_1_1,int1)
& etype(vereidigung_1_1,int0)
& fact(vereidigung_1_1,real)
& gener(vereidigung_1_1,ge)
& quant(vereidigung_1_1,one)
& refer(vereidigung_1_1,refer_c)
& varia(vereidigung_1_1,varia_c)
& card(c167,int1)
& etype(c167,int0)
& fact(c167,real)
& gener(c167,sp)
& quant(c167,one)
& refer(c167,det)
& varia(c167,con)
& card(c151,int1)
& etype(c151,int0)
& fact(c151,real)
& gener(c151,ge)
& quant(c151,one)
& refer(c151,refer_c)
& varia(c151,varia_c)
& card(erst_1_1,int1)
& 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(c155,int1)
& etype(c155,int0)
& fact(c155,real)
& gener(c155,sp)
& quant(c155,one)
& refer(c155,det)
& varia(c155,con)
& card(c156,int1)
& etype(c156,int0)
& fact(c156,real)
& gener(c156,sp)
& quant(c156,one)
& refer(c156,indet)
& varia(c156,varia_c)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& quant(land_1_1,one)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& card(c162,int1)
& etype(c162,int0)
& fact(c162,real)
& gener(c162,sp)
& quant(c162,one)
& refer(c162,indet)
& varia(c162,varia_c)
& card(c163,int1)
& etype(c163,int0)
& fact(c163,real)
& gener(c163,sp)
& quant(c163,one)
& refer(c163,indet)
& varia(c163,varia_c)
& card(c180,int1)
& etype(c180,int0)
& fact(c180,real)
& gener(c180,sp)
& quant(c180,one)
& refer(c180,det)
& varia(c180,con)
& 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(dienstag__1_1,int1)
& etype(dienstag__1_1,int0)
& fact(dienstag__1_1,real)
& gener(dienstag__1_1,ge)
& quant(dienstag__1_1,one)
& refer(dienstag__1_1,refer_c)
& varia(dienstag__1_1,varia_c)
& card(c177,int1)
& etype(c177,int0)
& fact(c177,real)
& gener(c177,sp)
& quant(c177,one)
& refer(c177,det)
& varia(c177,con)
& card(c178,int1)
& etype(c178,int0)
& fact(c178,real)
& gener(c178,sp)
& quant(c178,one)
& refer(c178,indet)
& varia(c178,varia_c)
& card(hauptsstadt_1_1,int1)
& etype(hauptsstadt_1_1,int0)
& fact(hauptsstadt_1_1,real)
& gener(hauptsstadt_1_1,ge)
& quant(hauptsstadt_1_1,one)
& refer(hauptsstadt_1_1,refer_c)
& varia(hauptsstadt_1_1,varia_c)
& card(c20,int1)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& quant(c20,one)
& refer(c20,det)
& varia(c20,con)
& card(freude_1_1,int1)
& etype(freude_1_1,int0)
& fact(freude_1_1,real)
& gener(freude_1_1,ge)
& quant(freude_1_1,one)
& refer(freude_1_1,refer_c)
& varia(freude_1_1,varia_c)
& fact(c23,real)
& gener(c23,sp)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& card(mensch_1_1,card_c)
& etype(mensch_1_1,etype_c)
& fact(mensch_1_1,real)
& gener(mensch_1_1,gener_c)
& quant(mensch_1_1,quant_c)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10330,plain,
( obj(c11,c161)
& prop(c11,afrikanisch__1_1)
& subs(c11,feier__1_1)
& subs(c11,vereidigung_1_1)
& temp(c11,c167)
& pmod(c151,erst_1_1,pr__344sident_1_1)
& attch(c155,c161)
& attr(c155,c156)
& sub(c155,land_1_1)
& sub(c156,name_1_1)
& val(c156,s__374dafrika_0)
& attr(c161,c162)
& attr(c161,c163)
& loc(c161,c180)
& prop(c161,schwarz_1_1)
& sub(c161,c151)
& sub(c162,eigenname_1_1)
& val(c162,nelson_0)
& sub(c163,familiename_1_1)
& val(c163,mandela_0)
& sub(c167,dienstag__1_1)
& attr(c177,c178)
& sub(c177,hauptsstadt_1_1)
& sub(c178,name_1_1)
& val(c178,pretoria_0)
& in(c180,c177)
& attch(c20,c11)
& prop(c20,ausgelassen_1_1)
& subs(c20,freude_1_1)
& arg1(c23,c11)
& arg2(c23,c11)
& subr(c23,equ_0)
& sub(hauptsstadt_1_1,stadt__1_1)
& sub(pr__344sident_1_1,mensch_1_1)
& card(c11,int1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& refer(c11,indet)
& varia(c11,varia_c)
& card(c161,int1)
& etype(c161,int0)
& fact(c161,real)
& gener(c161,sp)
& refer(c161,det)
& varia(c161,con)
& card(feier__1_1,int1)
& etype(feier__1_1,int0)
& fact(feier__1_1,real)
& gener(feier__1_1,ge)
& refer(feier__1_1,refer_c)
& varia(feier__1_1,varia_c)
& card(vereidigung_1_1,int1)
& etype(vereidigung_1_1,int0)
& fact(vereidigung_1_1,real)
& gener(vereidigung_1_1,ge)
& refer(vereidigung_1_1,refer_c)
& varia(vereidigung_1_1,varia_c)
& card(c167,int1)
& etype(c167,int0)
& fact(c167,real)
& gener(c167,sp)
& refer(c167,det)
& varia(c167,con)
& card(c151,int1)
& etype(c151,int0)
& fact(c151,real)
& gener(c151,ge)
& refer(c151,refer_c)
& varia(c151,varia_c)
& card(erst_1_1,int1)
& 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(c155,int1)
& etype(c155,int0)
& fact(c155,real)
& gener(c155,sp)
& refer(c155,det)
& varia(c155,con)
& card(c156,int1)
& etype(c156,int0)
& fact(c156,real)
& gener(c156,sp)
& refer(c156,indet)
& varia(c156,varia_c)
& card(land_1_1,int1)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& card(c162,int1)
& etype(c162,int0)
& fact(c162,real)
& gener(c162,sp)
& refer(c162,indet)
& varia(c162,varia_c)
& card(c163,int1)
& etype(c163,int0)
& fact(c163,real)
& gener(c163,sp)
& refer(c163,indet)
& varia(c163,varia_c)
& card(c180,int1)
& etype(c180,int0)
& fact(c180,real)
& gener(c180,sp)
& refer(c180,det)
& varia(c180,con)
& 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(dienstag__1_1,int1)
& etype(dienstag__1_1,int0)
& fact(dienstag__1_1,real)
& gener(dienstag__1_1,ge)
& refer(dienstag__1_1,refer_c)
& varia(dienstag__1_1,varia_c)
& card(c177,int1)
& etype(c177,int0)
& fact(c177,real)
& gener(c177,sp)
& refer(c177,det)
& varia(c177,con)
& card(c178,int1)
& etype(c178,int0)
& fact(c178,real)
& gener(c178,sp)
& refer(c178,indet)
& varia(c178,varia_c)
& card(hauptsstadt_1_1,int1)
& etype(hauptsstadt_1_1,int0)
& fact(hauptsstadt_1_1,real)
& gener(hauptsstadt_1_1,ge)
& refer(hauptsstadt_1_1,refer_c)
& varia(hauptsstadt_1_1,varia_c)
& card(c20,int1)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& refer(c20,det)
& varia(c20,con)
& card(freude_1_1,int1)
& etype(freude_1_1,int0)
& fact(freude_1_1,real)
& gener(freude_1_1,ge)
& refer(freude_1_1,refer_c)
& varia(freude_1_1,varia_c)
& fact(c23,real)
& gener(c23,sp)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& card(mensch_1_1,card_c)
& etype(mensch_1_1,etype_c)
& fact(mensch_1_1,real)
& gener(mensch_1_1,gener_c)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10327]) ).
fof(f10333,plain,
( obj(c11,c161)
& prop(c11,afrikanisch__1_1)
& subs(c11,feier__1_1)
& subs(c11,vereidigung_1_1)
& temp(c11,c167)
& pmod(c151,erst_1_1,pr__344sident_1_1)
& attch(c155,c161)
& attr(c155,c156)
& sub(c155,land_1_1)
& sub(c156,name_1_1)
& val(c156,s__374dafrika_0)
& attr(c161,c162)
& attr(c161,c163)
& loc(c161,c180)
& prop(c161,schwarz_1_1)
& sub(c161,c151)
& sub(c162,eigenname_1_1)
& val(c162,nelson_0)
& sub(c163,familiename_1_1)
& val(c163,mandela_0)
& sub(c167,dienstag__1_1)
& attr(c177,c178)
& sub(c177,hauptsstadt_1_1)
& sub(c178,name_1_1)
& val(c178,pretoria_0)
& in(c180,c177)
& attch(c20,c11)
& prop(c20,ausgelassen_1_1)
& subs(c20,freude_1_1)
& arg1(c23,c11)
& arg2(c23,c11)
& subr(c23,equ_0)
& sub(hauptsstadt_1_1,stadt__1_1)
& sub(pr__344sident_1_1,mensch_1_1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& refer(c11,indet)
& varia(c11,varia_c)
& etype(c161,int0)
& fact(c161,real)
& gener(c161,sp)
& refer(c161,det)
& varia(c161,con)
& etype(feier__1_1,int0)
& fact(feier__1_1,real)
& gener(feier__1_1,ge)
& refer(feier__1_1,refer_c)
& varia(feier__1_1,varia_c)
& etype(vereidigung_1_1,int0)
& fact(vereidigung_1_1,real)
& gener(vereidigung_1_1,ge)
& refer(vereidigung_1_1,refer_c)
& varia(vereidigung_1_1,varia_c)
& etype(c167,int0)
& fact(c167,real)
& gener(c167,sp)
& refer(c167,det)
& varia(c167,con)
& etype(c151,int0)
& fact(c151,real)
& gener(c151,ge)
& refer(c151,refer_c)
& varia(c151,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(c155,int0)
& fact(c155,real)
& gener(c155,sp)
& refer(c155,det)
& varia(c155,con)
& etype(c156,int0)
& fact(c156,real)
& gener(c156,sp)
& refer(c156,indet)
& varia(c156,varia_c)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& refer(land_1_1,refer_c)
& varia(land_1_1,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& etype(c162,int0)
& fact(c162,real)
& gener(c162,sp)
& refer(c162,indet)
& varia(c162,varia_c)
& etype(c163,int0)
& fact(c163,real)
& gener(c163,sp)
& refer(c163,indet)
& varia(c163,varia_c)
& etype(c180,int0)
& fact(c180,real)
& gener(c180,sp)
& refer(c180,det)
& varia(c180,con)
& 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(dienstag__1_1,int0)
& fact(dienstag__1_1,real)
& gener(dienstag__1_1,ge)
& refer(dienstag__1_1,refer_c)
& varia(dienstag__1_1,varia_c)
& etype(c177,int0)
& fact(c177,real)
& gener(c177,sp)
& refer(c177,det)
& varia(c177,con)
& etype(c178,int0)
& fact(c178,real)
& gener(c178,sp)
& refer(c178,indet)
& varia(c178,varia_c)
& etype(hauptsstadt_1_1,int0)
& fact(hauptsstadt_1_1,real)
& gener(hauptsstadt_1_1,ge)
& refer(hauptsstadt_1_1,refer_c)
& varia(hauptsstadt_1_1,varia_c)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& refer(c20,det)
& varia(c20,con)
& etype(freude_1_1,int0)
& fact(freude_1_1,real)
& gener(freude_1_1,ge)
& refer(freude_1_1,refer_c)
& varia(freude_1_1,varia_c)
& fact(c23,real)
& gener(c23,sp)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& etype(mensch_1_1,etype_c)
& fact(mensch_1_1,real)
& gener(mensch_1_1,gener_c)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10330]) ).
fof(f10336,plain,
( obj(c11,c161)
& prop(c11,afrikanisch__1_1)
& subs(c11,feier__1_1)
& subs(c11,vereidigung_1_1)
& temp(c11,c167)
& pmod(c151,erst_1_1,pr__344sident_1_1)
& attch(c155,c161)
& attr(c155,c156)
& sub(c155,land_1_1)
& sub(c156,name_1_1)
& val(c156,s__374dafrika_0)
& attr(c161,c162)
& attr(c161,c163)
& loc(c161,c180)
& prop(c161,schwarz_1_1)
& sub(c161,c151)
& sub(c162,eigenname_1_1)
& val(c162,nelson_0)
& sub(c163,familiename_1_1)
& val(c163,mandela_0)
& sub(c167,dienstag__1_1)
& attr(c177,c178)
& sub(c177,hauptsstadt_1_1)
& sub(c178,name_1_1)
& val(c178,pretoria_0)
& in(c180,c177)
& attch(c20,c11)
& prop(c20,ausgelassen_1_1)
& subs(c20,freude_1_1)
& arg1(c23,c11)
& arg2(c23,c11)
& subr(c23,equ_0)
& sub(hauptsstadt_1_1,stadt__1_1)
& sub(pr__344sident_1_1,mensch_1_1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& varia(c11,varia_c)
& etype(c161,int0)
& fact(c161,real)
& gener(c161,sp)
& varia(c161,con)
& etype(feier__1_1,int0)
& fact(feier__1_1,real)
& gener(feier__1_1,ge)
& varia(feier__1_1,varia_c)
& etype(vereidigung_1_1,int0)
& fact(vereidigung_1_1,real)
& gener(vereidigung_1_1,ge)
& varia(vereidigung_1_1,varia_c)
& etype(c167,int0)
& fact(c167,real)
& gener(c167,sp)
& varia(c167,con)
& etype(c151,int0)
& fact(c151,real)
& gener(c151,ge)
& varia(c151,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(c155,int0)
& fact(c155,real)
& gener(c155,sp)
& varia(c155,con)
& etype(c156,int0)
& fact(c156,real)
& gener(c156,sp)
& varia(c156,varia_c)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& varia(land_1_1,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& varia(name_1_1,varia_c)
& etype(c162,int0)
& fact(c162,real)
& gener(c162,sp)
& varia(c162,varia_c)
& etype(c163,int0)
& fact(c163,real)
& gener(c163,sp)
& varia(c163,varia_c)
& etype(c180,int0)
& fact(c180,real)
& gener(c180,sp)
& varia(c180,con)
& 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(dienstag__1_1,int0)
& fact(dienstag__1_1,real)
& gener(dienstag__1_1,ge)
& varia(dienstag__1_1,varia_c)
& etype(c177,int0)
& fact(c177,real)
& gener(c177,sp)
& varia(c177,con)
& etype(c178,int0)
& fact(c178,real)
& gener(c178,sp)
& varia(c178,varia_c)
& etype(hauptsstadt_1_1,int0)
& fact(hauptsstadt_1_1,real)
& gener(hauptsstadt_1_1,ge)
& varia(hauptsstadt_1_1,varia_c)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& varia(c20,con)
& etype(freude_1_1,int0)
& fact(freude_1_1,real)
& gener(freude_1_1,ge)
& varia(freude_1_1,varia_c)
& fact(c23,real)
& gener(c23,sp)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& varia(stadt__1_1,varia_c)
& etype(mensch_1_1,etype_c)
& fact(mensch_1_1,real)
& gener(mensch_1_1,gener_c)
& varia(mensch_1_1,varia_c) ),
inference(pure_predicate_removal,[],[f10333]) ).
fof(f10341,plain,
( obj(c11,c161)
& prop(c11,afrikanisch__1_1)
& subs(c11,feier__1_1)
& subs(c11,vereidigung_1_1)
& temp(c11,c167)
& pmod(c151,erst_1_1,pr__344sident_1_1)
& attch(c155,c161)
& attr(c155,c156)
& sub(c155,land_1_1)
& sub(c156,name_1_1)
& val(c156,s__374dafrika_0)
& attr(c161,c162)
& attr(c161,c163)
& loc(c161,c180)
& prop(c161,schwarz_1_1)
& sub(c161,c151)
& sub(c162,eigenname_1_1)
& val(c162,nelson_0)
& sub(c163,familiename_1_1)
& val(c163,mandela_0)
& sub(c167,dienstag__1_1)
& attr(c177,c178)
& sub(c177,hauptsstadt_1_1)
& sub(c178,name_1_1)
& val(c178,pretoria_0)
& in(c180,c177)
& attch(c20,c11)
& prop(c20,ausgelassen_1_1)
& subs(c20,freude_1_1)
& arg1(c23,c11)
& arg2(c23,c11)
& subr(c23,equ_0)
& sub(hauptsstadt_1_1,stadt__1_1)
& sub(pr__344sident_1_1,mensch_1_1)
& etype(c11,int0)
& fact(c11,real)
& gener(c11,sp)
& etype(c161,int0)
& fact(c161,real)
& gener(c161,sp)
& etype(feier__1_1,int0)
& fact(feier__1_1,real)
& gener(feier__1_1,ge)
& etype(vereidigung_1_1,int0)
& fact(vereidigung_1_1,real)
& gener(vereidigung_1_1,ge)
& etype(c167,int0)
& fact(c167,real)
& gener(c167,sp)
& etype(c151,int0)
& fact(c151,real)
& gener(c151,ge)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& etype(c155,int0)
& fact(c155,real)
& gener(c155,sp)
& etype(c156,int0)
& fact(c156,real)
& gener(c156,sp)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& gener(land_1_1,ge)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& etype(c162,int0)
& fact(c162,real)
& gener(c162,sp)
& etype(c163,int0)
& fact(c163,real)
& gener(c163,sp)
& etype(c180,int0)
& fact(c180,real)
& gener(c180,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(dienstag__1_1,int0)
& fact(dienstag__1_1,real)
& gener(dienstag__1_1,ge)
& etype(c177,int0)
& fact(c177,real)
& gener(c177,sp)
& etype(c178,int0)
& fact(c178,real)
& gener(c178,sp)
& etype(hauptsstadt_1_1,int0)
& fact(hauptsstadt_1_1,real)
& gener(hauptsstadt_1_1,ge)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& etype(freude_1_1,int0)
& fact(freude_1_1,real)
& gener(freude_1_1,ge)
& fact(c23,real)
& gener(c23,sp)
& fact(equ_0,real)
& gener(equ_0,gener_c)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& etype(mensch_1_1,etype_c)
& fact(mensch_1_1,real)
& gener(mensch_1_1,gener_c) ),
inference(pure_predicate_removal,[],[f10336]) ).
fof(f10346,plain,
( obj(c11,c161)
& prop(c11,afrikanisch__1_1)
& subs(c11,feier__1_1)
& subs(c11,vereidigung_1_1)
& temp(c11,c167)
& pmod(c151,erst_1_1,pr__344sident_1_1)
& attch(c155,c161)
& attr(c155,c156)
& sub(c155,land_1_1)
& sub(c156,name_1_1)
& val(c156,s__374dafrika_0)
& attr(c161,c162)
& attr(c161,c163)
& loc(c161,c180)
& prop(c161,schwarz_1_1)
& sub(c161,c151)
& sub(c162,eigenname_1_1)
& val(c162,nelson_0)
& sub(c163,familiename_1_1)
& val(c163,mandela_0)
& sub(c167,dienstag__1_1)
& attr(c177,c178)
& sub(c177,hauptsstadt_1_1)
& sub(c178,name_1_1)
& val(c178,pretoria_0)
& in(c180,c177)
& attch(c20,c11)
& prop(c20,ausgelassen_1_1)
& subs(c20,freude_1_1)
& arg1(c23,c11)
& arg2(c23,c11)
& subr(c23,equ_0)
& sub(hauptsstadt_1_1,stadt__1_1)
& sub(pr__344sident_1_1,mensch_1_1)
& etype(c11,int0)
& fact(c11,real)
& etype(c161,int0)
& fact(c161,real)
& etype(feier__1_1,int0)
& fact(feier__1_1,real)
& etype(vereidigung_1_1,int0)
& fact(vereidigung_1_1,real)
& etype(c167,int0)
& fact(c167,real)
& etype(c151,int0)
& fact(c151,real)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& etype(c155,int0)
& fact(c155,real)
& etype(c156,int0)
& fact(c156,real)
& etype(land_1_1,int0)
& fact(land_1_1,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& etype(c162,int0)
& fact(c162,real)
& etype(c163,int0)
& fact(c163,real)
& etype(c180,int0)
& fact(c180,real)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& etype(dienstag__1_1,int0)
& fact(dienstag__1_1,real)
& etype(c177,int0)
& fact(c177,real)
& etype(c178,int0)
& fact(c178,real)
& etype(hauptsstadt_1_1,int0)
& fact(hauptsstadt_1_1,real)
& etype(c20,int0)
& fact(c20,real)
& etype(freude_1_1,int0)
& fact(freude_1_1,real)
& fact(c23,real)
& fact(equ_0,real)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& etype(mensch_1_1,etype_c)
& fact(mensch_1_1,real) ),
inference(pure_predicate_removal,[],[f10341]) ).
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] :
( ~ pmod(X8,erst_1_1,pr__344sident_1_1)
| ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ attr(X5,X6)
| ~ obj(X7,X0)
| ~ prop(X4,schwarz_1_1)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X8)
| ~ sub(X6,name_1_1)
| ~ subr(X3,rprs_0)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ val(X6,s__374dafrika_0) ),
inference(ennf_transformation,[],[f10189]) ).
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(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(f20816,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ pmod(X8,erst_1_1,pr__344sident_1_1)
| ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ attr(X5,X6)
| ~ obj(X7,X0)
| ~ prop(X4,schwarz_1_1)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X8)
| ~ sub(X6,name_1_1)
| ~ subr(X3,rprs_0)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ val(X6,s__374dafrika_0) ),
inference(cnf_transformation,[],[f10551]) ).
fof(f20881,plain,
val(c163,mandela_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20882,plain,
sub(c163,familiename_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20883,plain,
val(c162,nelson_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20884,plain,
sub(c162,eigenname_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20885,plain,
sub(c161,c151),
inference(cnf_transformation,[],[f10346]) ).
fof(f20886,plain,
prop(c161,schwarz_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20888,plain,
attr(c161,c163),
inference(cnf_transformation,[],[f10346]) ).
fof(f20889,plain,
attr(c161,c162),
inference(cnf_transformation,[],[f10346]) ).
fof(f20890,plain,
val(c156,s__374dafrika_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20891,plain,
sub(c156,name_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20893,plain,
attr(c155,c156),
inference(cnf_transformation,[],[f10346]) ).
fof(f20895,plain,
pmod(c151,erst_1_1,pr__344sident_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20900,plain,
obj(c11,c161),
inference(cnf_transformation,[],[f10346]) ).
fof(f20902,definition,
( spl63_1
<=> ! [X6,X5] :
( ~ attr(X5,X6)
| ~ val(X6,s__374dafrika_0)
| ~ sub(X6,name_1_1) ) ),
introduced(definition,[new_symbols(definition,[spl63_1])],[avatar_definition]) ).
fof(f20903,plain,
( ! [X6,X5] :
( ~ sub(X6,name_1_1)
| ~ val(X6,s__374dafrika_0)
| ~ attr(X5,X6) )
| ~ spl63_1 ),
inference(avatar_component_clause,[],[f20902]) ).
fof(f20905,definition,
( spl63_2
<=> ! [X7,X4,X0,X8,X3,X2,X1] :
( ~ pmod(X8,erst_1_1,pr__344sident_1_1)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(X3,rprs_0)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg1(X3,X0)
| ~ sub(X4,X8)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ prop(X4,schwarz_1_1)
| ~ obj(X7,X0)
| ~ arg2(X3,X4) ) ),
introduced(definition,[new_symbols(definition,[spl63_2])],[avatar_definition]) ).
fof(f20906,plain,
( ! [X2,X3,X0,X1,X8,X7,X4] :
( ~ pmod(X8,erst_1_1,pr__344sident_1_1)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(X3,rprs_0)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg1(X3,X0)
| ~ sub(X4,X8)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ prop(X4,schwarz_1_1)
| ~ obj(X7,X0)
| ~ arg2(X3,X4) )
| ~ spl63_2 ),
inference(avatar_component_clause,[],[f20905]) ).
fof(f20907,plain,
( spl63_1
| spl63_2 ),
inference(avatar_split_clause,[],[f20816,f20905,f20902]) ).
fof(f20908,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ arg2(X2,X4)
| ~ val(X1,mandela_0)
| ~ subr(X2,rprs_0)
| ~ attr(X3,X0)
| ~ attr(X3,X1)
| ~ arg1(X2,X3)
| ~ sub(X4,c151)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ prop(X4,schwarz_1_1)
| ~ obj(X5,X3)
| ~ val(X0,nelson_0) )
| ~ spl63_2 ),
inference(resolution,[],[f20906,f20895]) ).
fof(f86237,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| subs(sK50(X0),hei__337en_1_1)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10860,f10600]) ).
fof(f86340,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| arg2(sK50(X0),X0)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10861,f10600]) ).
fof(f86427,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| arg1(sK50(X0),X0)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10862,f10600]) ).
fof(f91444,plain,
! [X0] :
( ~ attr(X0,c162)
| subs(sK50(X0),hei__337en_1_1) ),
inference(resolution,[],[f86237,f20884]) ).
fof(f91445,plain,
subs(sK50(c161),hei__337en_1_1),
inference(resolution,[],[f91444,f20889]) ).
fof(f91447,plain,
! [X0,X1] :
( ~ arg2(sK50(c161),X1)
| ~ arg1(sK50(c161),X0)
| subr(sK53(sK50(c161),X0,X1),rprs_0) ),
inference(resolution,[],[f91445,f10868]) ).
fof(f91451,plain,
! [X0,X1] :
( ~ arg2(sK50(c161),X1)
| ~ arg1(sK50(c161),X0)
| arg2(sK53(sK50(c161),X0,X1),X1) ),
inference(resolution,[],[f91445,f10872]) ).
fof(f91452,plain,
! [X0,X1] :
( ~ arg2(sK50(c161),X1)
| ~ arg1(sK50(c161),X0)
| arg1(sK53(sK50(c161),X0,X1),X0) ),
inference(resolution,[],[f91445,f10873]) ).
fof(f91465,plain,
! [X0] :
( ~ attr(X0,c162)
| arg2(sK50(X0),X0) ),
inference(resolution,[],[f86340,f20884]) ).
fof(f91466,plain,
arg2(sK50(c161),c161),
inference(resolution,[],[f91465,f20889]) ).
fof(f91478,plain,
! [X0] :
( ~ attr(X0,c162)
| arg1(sK50(X0),X0) ),
inference(resolution,[],[f86427,f20884]) ).
fof(f91479,plain,
arg1(sK50(c161),c161),
inference(resolution,[],[f91478,f20889]) ).
fof(f108093,plain,
! [X0] :
( ~ arg1(sK50(c161),X0)
| subr(sK53(sK50(c161),X0,c161),rprs_0) ),
inference(resolution,[],[f91447,f91466]) ).
fof(f108094,plain,
subr(sK53(sK50(c161),c161,c161),rprs_0),
inference(resolution,[],[f108093,f91479]) ).
fof(f108126,plain,
! [X0] :
( ~ arg1(sK50(c161),X0)
| arg2(sK53(sK50(c161),X0,c161),c161) ),
inference(resolution,[],[f91451,f91466]) ).
fof(f108127,plain,
arg2(sK53(sK50(c161),c161,c161),c161),
inference(resolution,[],[f108126,f91479]) ).
fof(f108129,plain,
( ! [X2,X3,X0,X1] :
( ~ val(X0,mandela_0)
| ~ subr(sK53(sK50(c161),c161,c161),rprs_0)
| ~ attr(X1,X2)
| ~ attr(X1,X0)
| ~ arg1(sK53(sK50(c161),c161,c161),X1)
| ~ sub(c161,c151)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X0,familiename_1_1)
| ~ prop(c161,schwarz_1_1)
| ~ obj(X3,X1)
| ~ val(X2,nelson_0) )
| ~ spl63_2 ),
inference(resolution,[],[f108127,f20908]) ).
fof(f108130,plain,
( ! [X2,X3,X0,X1] :
( ~ val(X0,mandela_0)
| ~ attr(X1,X2)
| ~ attr(X1,X0)
| ~ arg1(sK53(sK50(c161),c161,c161),X1)
| ~ sub(c161,c151)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X0,familiename_1_1)
| ~ prop(c161,schwarz_1_1)
| ~ obj(X3,X1)
| ~ val(X2,nelson_0) )
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f108129,f108094]) ).
fof(f108131,plain,
( ! [X2,X3,X0,X1] :
( ~ val(X0,mandela_0)
| ~ attr(X1,X2)
| ~ attr(X1,X0)
| ~ arg1(sK53(sK50(c161),c161,c161),X1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X0,familiename_1_1)
| ~ prop(c161,schwarz_1_1)
| ~ obj(X3,X1)
| ~ val(X2,nelson_0) )
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f108130,f20885]) ).
fof(f108132,plain,
( ! [X2,X3,X0,X1] :
( ~ arg1(sK53(sK50(c161),c161,c161),X1)
| ~ attr(X1,X2)
| ~ attr(X1,X0)
| ~ val(X0,mandela_0)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X0,familiename_1_1)
| ~ obj(X3,X1)
| ~ val(X2,nelson_0) )
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f108131,f20886]) ).
fof(f108159,plain,
! [X0] :
( ~ arg1(sK50(c161),X0)
| arg1(sK53(sK50(c161),X0,c161),X0) ),
inference(resolution,[],[f91452,f91466]) ).
fof(f108160,plain,
arg1(sK53(sK50(c161),c161,c161),c161),
inference(resolution,[],[f108159,f91479]) ).
fof(f108161,plain,
( ! [X2,X0,X1] :
( ~ attr(c161,X0)
| ~ attr(c161,X1)
| ~ val(X1,mandela_0)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X2,c161)
| ~ val(X0,nelson_0) )
| ~ spl63_2 ),
inference(resolution,[],[f108160,f108132]) ).
fof(f108163,definition,
( spl63_4311
<=> ! [X2] : ~ obj(X2,c161) ),
introduced(definition,[new_symbols(definition,[spl63_4311])],[avatar_definition]) ).
fof(f108164,plain,
( ! [X2] : ~ obj(X2,c161)
| ~ spl63_4311 ),
inference(avatar_component_clause,[],[f108163]) ).
fof(f108166,definition,
( spl63_4312
<=> ! [X1] :
( ~ attr(c161,X1)
| ~ sub(X1,familiename_1_1)
| ~ val(X1,mandela_0) ) ),
introduced(definition,[new_symbols(definition,[spl63_4312])],[avatar_definition]) ).
fof(f108167,plain,
( ! [X1] :
( ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1)
| ~ attr(c161,X1) )
| ~ spl63_4312 ),
inference(avatar_component_clause,[],[f108166]) ).
fof(f108169,definition,
( spl63_4313
<=> ! [X0] :
( ~ attr(c161,X0)
| ~ val(X0,nelson_0)
| ~ sub(X0,eigenname_1_1) ) ),
introduced(definition,[new_symbols(definition,[spl63_4313])],[avatar_definition]) ).
fof(f108170,plain,
( ! [X0] :
( ~ sub(X0,eigenname_1_1)
| ~ val(X0,nelson_0)
| ~ attr(c161,X0) )
| ~ spl63_4313 ),
inference(avatar_component_clause,[],[f108169]) ).
fof(f108171,plain,
( spl63_4311
| spl63_4312
| spl63_4313
| ~ spl63_2 ),
inference(avatar_split_clause,[],[f108161,f20905,f108169,f108166,f108163]) ).
fof(f108174,plain,
( ! [X0] :
( ~ val(c156,s__374dafrika_0)
| ~ attr(X0,c156) )
| ~ spl63_1 ),
inference(resolution,[],[f20903,f20891]) ).
fof(f108181,plain,
( ! [X0] : ~ attr(X0,c156)
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f108174,f20890]) ).
fof(f108182,plain,
( $false
| ~ spl63_1 ),
inference(resolution,[],[f108181,f20893]) ).
fof(f108183,plain,
~ spl63_1,
inference(avatar_contradiction_clause,[],[f108182]) ).
fof(f108184,plain,
( $false
| ~ spl63_4311 ),
inference(resolution,[],[f108164,f20900]) ).
fof(f108197,plain,
~ spl63_4311,
inference(avatar_contradiction_clause,[],[f108184]) ).
fof(f108198,plain,
( ~ sub(c163,familiename_1_1)
| ~ attr(c161,c163)
| ~ spl63_4312 ),
inference(resolution,[],[f108167,f20881]) ).
fof(f108199,plain,
( ~ attr(c161,c163)
| ~ spl63_4312 ),
inference(forward_subsumption_resolution,[],[f108198,f20882]) ).
fof(f108200,plain,
( $false
| ~ spl63_4312 ),
inference(forward_subsumption_resolution,[],[f108199,f20888]) ).
fof(f108201,plain,
~ spl63_4312,
inference(avatar_contradiction_clause,[],[f108200]) ).
fof(f108202,plain,
( ~ val(c162,nelson_0)
| ~ attr(c161,c162)
| ~ spl63_4313 ),
inference(resolution,[],[f108170,f20884]) ).
fof(f108204,plain,
( ~ attr(c161,c162)
| ~ spl63_4313 ),
inference(forward_subsumption_resolution,[],[f108202,f20883]) ).
fof(f108205,plain,
( $false
| ~ spl63_4313 ),
inference(forward_subsumption_resolution,[],[f108204,f20889]) ).
fof(f108206,plain,
~ spl63_4313,
inference(avatar_contradiction_clause,[],[f108205]) ).
cnf(s1,plain,
( spl63_1
| spl63_2 ),
inference(sat_conversion,[],[f20907]) ).
cnf(s1255,plain,
( ~ spl63_2
| spl63_4311
| spl63_4312
| spl63_4313 ),
inference(sat_conversion,[],[f108171]) ).
cnf(s1256,plain,
~ spl63_1,
inference(sat_conversion,[],[f108183]) ).
cnf(s1263,plain,
~ spl63_4311,
inference(sat_conversion,[],[f108197]) ).
cnf(s1264,plain,
~ spl63_4312,
inference(sat_conversion,[],[f108201]) ).
cnf(s1265,plain,
~ spl63_4313,
inference(sat_conversion,[],[f108206]) ).
cnf(s1266,plain,
~ spl63_2,
inference(rat,[],[s1255,s1265,s1264,s1263]) ).
cnf(s1277,plain,
$false,
inference(rat,[],[s1,s1266,s1256]) ).
fof(f108207,plain,
$false,
inference(avatar_sat_refutation,[],[s1277]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR116+41 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n011.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 23:30:46 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.07/4.08 % (3888199)Will run a generic schedule for satisfiability detection.
% 26.07/4.08 % (3888208)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=150772113:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 26.07/4.08 % (3888205)% WARNING: option uhcvi not known.
% 26.07/4.08 % (3888204)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1899599915_2998 on theBenchmark for (2998ds/0Mi)
% 26.07/4.08 % (3888205)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=299477543:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 26.07/4.08 % (3888206)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2062646128:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 26.07/4.08 % (3888207)dis+10_1_sil=32000:sp=arity:random_seed=1357812148:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 26.07/4.08 % (3888209)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=287957696:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 26.07/4.08 % (3888210)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3949469713:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 26.07/4.08 % (3888208)Instruction limit reached!
% 26.07/4.08 % (3888208)------------------------------
% 26.07/4.08 % (3888208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.07/4.08 % (3888208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.07/4.08 % (3888208)CaDiCaL version: 2.1.3
% 26.07/4.08 % (3888208)Termination reason: Instruction limit
% 26.07/4.08 % (3888208)Termination phase: Blocked clause elimination
% 26.07/4.08 % (3888208)Time elapsed: 0.044 s
% 26.07/4.08 % (3888208)Peak memory usage: 27 MB
% 26.07/4.08 % (3888208)Instructions burned: 119 (million)
% 26.07/4.08 % (3888218)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1635529476:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 26.07/4.08 % (3888207)Instruction limit reached!
% 26.07/4.08 % (3888207)------------------------------
% 26.07/4.08 % (3888207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.07/4.08 % (3888207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.07/4.08 % (3888207)CaDiCaL version: 2.1.3
% 26.07/4.08 % (3888207)Termination reason: Instruction limit
% 26.07/4.08 % (3888207)Termination phase: Saturation
% 26.07/4.08 % (3888207)Time elapsed: 0.060 s
% 26.07/4.08 % (3888207)Peak memory usage: 26 MB
% 26.07/4.08 % (3888207)Instructions burned: 104 (million)
% 26.07/4.08 % (3888209)Instruction limit reached!
% 26.07/4.08 % (3888209)------------------------------
% 26.07/4.08 % (3888209)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.07/4.08 % (3888209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.07/4.08 % (3888209)CaDiCaL version: 2.1.3
% 26.07/4.08 % (3888209)Termination reason: Instruction limit
% 26.07/4.08 % (3888209)Termination phase: Saturation
% 26.07/4.08 % (3888209)Time elapsed: 0.074 s
% 26.07/4.08 % (3888209)Peak memory usage: 28 MB
% 26.07/4.08 % (3888209)Instructions burned: 132 (million)
% 26.07/4.08 % (3888220)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2901900111:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 26.07/4.08 % (3888221)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=2295203101:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 26.07/4.08 % (3888210)Instruction limit reached!
% 26.07/4.08 % (3888210)------------------------------
% 26.07/4.08 % (3888210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.07/4.08 % (3888210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.07/4.08 % (3888210)CaDiCaL version: 2.1.3
% 26.07/4.08 % (3888210)Termination reason: Instruction limit
% 26.07/4.08 % (3888210)Termination phase: Saturation
% 26.07/4.08 % (3888210)Time elapsed: 0.097 s
% 26.07/4.08 % (3888210)Peak memory usage: 29 MB
% 26.07/4.08 % (3888210)Instructions burned: 160 (million)
% 26.07/4.08 % (3888224)ott-21_1_sil=16000:fs=off:random_seed=698759837:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 26.07/4.08 % TRYING [1]
% 26.07/4.08 % (3888220)Instruction limit reached!
% 26.07/4.08 % (3888220)------------------------------
% 26.07/4.08 % (3888220)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.07/4.08 % (3888220)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.60/6.99 % (3888220)CaDiCaL version: 2.1.3
% 45.60/6.99 % (3888220)Termination reason: Instruction limit
% 45.60/6.99 % (3888220)Termination phase: Blocked clause elimination
% 45.60/6.99 % (3888220)Time elapsed: 0.078 s
% 45.60/6.99 % (3888220)Peak memory usage: 28 MB
% 45.60/6.99 % (3888220)Instructions burned: 131 (million)
% 45.60/6.99 % (3888226)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1537328452:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 45.60/6.99 % TRYING [2]
% 45.60/6.99 % (3888224)Instruction limit reached!
% 45.60/6.99 % (3888224)------------------------------
% 45.60/6.99 % (3888224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.60/6.99 % (3888224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.60/6.99 % (3888224)CaDiCaL version: 2.1.3
% 45.60/6.99 % (3888224)Termination reason: Instruction limit
% 45.60/6.99 % (3888224)Termination phase: Saturation
% 45.60/6.99 % (3888224)Time elapsed: 0.093 s
% 45.60/6.99 % (3888224)Peak memory usage: 28 MB
% 45.60/6.99 % (3888224)Instructions burned: 181 (million)
% 45.60/6.99 % (3888228)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1777845876:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 45.60/6.99 % (3888218)Instruction limit reached!
% 45.60/6.99 % (3888218)------------------------------
% 45.60/6.99 % (3888218)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.60/6.99 % (3888218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.60/6.99 % (3888218)CaDiCaL version: 2.1.3
% 45.60/6.99 % (3888218)Termination reason: Instruction limit
% 45.60/6.99 % (3888218)Termination phase: Finite model building constraint generation
% 45.60/6.99 % (3888218)Time elapsed: 0.188 s
% 45.60/6.99 % (3888218)Peak memory usage: 54 MB
% 45.60/6.99 % (3888218)Instructions burned: 716 (million)
% 45.60/6.99 % (3888230)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=782939944:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 45.60/6.99 % TRYING [1]
% 45.60/6.99 % TRYING [2]
% 45.60/6.99 % (3888226)Instruction limit reached!
% 45.60/6.99 % (3888226)------------------------------
% 45.60/6.99 % (3888226)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.60/6.99 % (3888226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.60/6.99 % (3888226)CaDiCaL version: 2.1.3
% 45.60/6.99 % (3888226)Termination reason: Instruction limit
% 45.60/6.99 % (3888226)Termination phase: Saturation
% 45.60/6.99 % (3888226)Time elapsed: 0.253 s
% 45.60/6.99 % (3888226)Peak memory usage: 36 MB
% 45.60/6.99 % (3888226)Instructions burned: 478 (million)
% 45.60/6.99 % TRYING [1]
% 45.60/6.99 % (3888232)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=732894814:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 45.60/6.99 % (3888221)Instruction limit reached!
% 45.60/6.99 % (3888221)------------------------------
% 45.60/6.99 % (3888221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.60/6.99 % (3888221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.60/6.99 % (3888221)CaDiCaL version: 2.1.3
% 45.60/6.99 % (3888221)Termination reason: Instruction limit
% 45.60/6.99 % (3888221)Termination phase: Saturation
% 45.60/6.99 % (3888221)Time elapsed: 0.372 s
% 45.60/6.99 % (3888221)Peak memory usage: 35 MB
% 45.60/6.99 % (3888221)Instructions burned: 684 (million)
% 45.60/6.99 % (3888234)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=3518160317: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)
% 45.60/6.99 % TRYING [3]
% 45.60/6.99 % (3888228)Instruction limit reached!
% 45.60/6.99 % (3888228)------------------------------
% 45.60/6.99 % (3888228)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.60/6.99 % (3888228)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.60/6.99 % (3888228)CaDiCaL version: 2.1.3
% 45.60/6.99 % (3888228)Termination reason: Instruction limit
% 45.60/6.99 % (3888228)Termination phase: Finite model building SAT solving
% 45.60/6.99 % (3888228)Time elapsed: 0.321 s
% 45.60/6.99 % (3888228)Peak memory usage: 38 MB
% 45.60/6.99 % (3888228)Instructions burned: 869 (million)
% 45.60/6.99 % (3888236)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2852939559:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 45.60/6.99 % (3888230)Instruction limit reached!
% 45.60/6.99 % (3888230)------------------------------
% 45.60/6.99 % (3888230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.57/14.46 % (3888230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.57/14.46 % (3888230)CaDiCaL version: 2.1.3
% 99.57/14.46 % (3888230)Termination reason: Instruction limit
% 99.57/14.46 % (3888230)Termination phase: Saturation
% 99.57/14.46 % (3888230)Time elapsed: 0.350 s
% 99.57/14.46 % (3888230)Peak memory usage: 54 MB
% 99.57/14.46 % (3888230)Instructions burned: 1183 (million)
% 99.57/14.46 % (3888238)fmb+10_1_sil=64000:random_seed=124440139:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 99.57/14.46 % TRYING [1]
% 99.57/14.46 % TRYING [2]
% 99.57/14.46 % (3888234)Instruction limit reached!
% 99.57/14.46 % (3888234)------------------------------
% 99.57/14.46 % (3888234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.57/14.46 % (3888234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.57/14.46 % (3888234)CaDiCaL version: 2.1.3
% 99.57/14.46 % (3888234)Termination reason: Instruction limit
% 99.57/14.46 % (3888234)Termination phase: Saturation
% 99.57/14.46 % (3888234)Time elapsed: 0.381 s
% 99.57/14.46 % (3888234)Peak memory usage: 40 MB
% 99.57/14.46 % (3888234)Instructions burned: 693 (million)
% 99.57/14.46 % (3888232)Instruction limit reached!
% 99.57/14.46 % (3888232)------------------------------
% 99.57/14.46 % (3888232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.57/14.46 % (3888232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.57/14.46 % (3888232)CaDiCaL version: 2.1.3
% 99.57/14.46 % (3888232)Termination reason: Instruction limit
% 99.57/14.46 % (3888232)Termination phase: Finite model building constraint generation
% 99.57/14.46 % (3888232)Time elapsed: 0.424 s
% 99.57/14.46 % (3888232)Peak memory usage: 91 MB
% 99.57/14.46 % (3888232)Instructions burned: 890 (million)
% 99.57/14.46 % (3888240)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3046835593:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 99.57/14.46 % (3888241)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2950902009:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 99.57/14.46 % (3888236)Instruction limit reached!
% 99.57/14.46 % (3888236)------------------------------
% 99.57/14.46 % (3888236)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.57/14.46 % (3888236)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.57/14.46 % (3888236)CaDiCaL version: 2.1.3
% 99.57/14.46 % (3888236)Termination reason: Instruction limit
% 99.57/14.46 % (3888236)Termination phase: Saturation
% 99.57/14.46 % (3888236)Time elapsed: 0.409 s
% 99.57/14.46 % (3888236)Peak memory usage: 47 MB
% 99.57/14.46 % (3888236)Instructions burned: 880 (million)
% 99.57/14.46 % (3888244)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2777460723:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 99.57/14.46 % TRYING [4]
% 99.57/14.46 % TRYING [20]
% 99.57/14.46 % TRYING [8]
% 99.57/14.46 % TRYING [3]
% 99.57/14.46 % (3888241)Instruction limit reached!
% 99.57/14.46 % (3888241)------------------------------
% 99.57/14.46 % (3888241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.57/14.46 % (3888241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.57/14.46 % (3888241)CaDiCaL version: 2.1.3
% 99.57/14.46 % (3888241)Termination reason: Instruction limit
% 99.57/14.46 % (3888241)Termination phase: Finite model building constraint generation
% 99.57/14.46 % (3888241)Time elapsed: 0.360 s
% 99.57/14.46 % (3888241)Peak memory usage: 64 MB
% 99.57/14.46 % (3888241)Instructions burned: 922 (million)
% 99.57/14.46 % (3888246)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2682644944:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 99.57/14.46 % TRYING [4]
% 99.57/14.46 % (3888246)Instruction limit reached!
% 99.57/14.46 % (3888246)------------------------------
% 99.57/14.46 % (3888246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 99.57/14.46 % (3888246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 99.57/14.46 % (3888246)CaDiCaL version: 2.1.3
% 99.57/14.46 % (3888246)Termination reason: Instruction limit
% 99.57/14.46 % (3888246)Termination phase: Saturation
% 99.57/14.46 % (3888246)Time elapsed: 0.669 s
% 99.57/14.46 % (3888246)Peak memory usage: 34 MB
% 99.57/14.46 % (3888246)Instructions burned: 1476 (million)
% 99.57/14.46 % (3888248)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1776656834:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 99.57/14.46 % TRYING [77]
% 99.57/14.46 % TRYING [5]
% 99.57/14.46 % (3888244)Instruction limit reached!
% 99.57/14.46 % (3888244)------------------------------
% 99.57/14.46 % (3888244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.34/29.68 % (3888244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.34/29.68 % (3888244)CaDiCaL version: 2.1.3
% 207.34/29.68 % (3888244)Termination reason: Instruction limit
% 207.34/29.68 % (3888244)Termination phase: Saturation
% 207.34/29.68 % (3888244)Time elapsed: 2.647 s
% 207.34/29.68 % (3888244)Peak memory usage: 39 MB
% 207.34/29.68 % (3888244)Instructions burned: 5132 (million)
% 207.34/29.68 % (3888251)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1200925151:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 207.34/29.68 % TRYING [16]
% 207.34/29.68 % TRYING [6]
% 207.34/29.68 % (3888248)Instruction limit reached!
% 207.34/29.68 % (3888248)------------------------------
% 207.34/29.68 % (3888248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.34/29.68 % (3888248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.34/29.68 % (3888248)CaDiCaL version: 2.1.3
% 207.34/29.68 % (3888248)Termination reason: Instruction limit
% 207.34/29.68 % (3888248)Termination phase: Finite model building constraint generation
% 207.34/29.68 % (3888248)Time elapsed: 2.253 s
% 207.34/29.68 % (3888248)Peak memory usage: 419 MB
% 207.34/29.68 % (3888248)Instructions burned: 6325 (million)
% 207.34/29.68 % (3888240)Instruction limit reached!
% 207.34/29.68 % (3888240)------------------------------
% 207.34/29.68 % (3888240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.34/29.68 % (3888240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.34/29.68 % (3888240)CaDiCaL version: 2.1.3
% 207.34/29.68 % (3888240)Termination reason: Instruction limit
% 207.34/29.68 % (3888240)Termination phase: Finite model building constraint generation
% 207.34/29.68 % (3888240)Time elapsed: 3.346 s
% 207.34/29.68 % (3888240)Peak memory usage: 550 MB
% 207.34/29.68 % (3888240)Instructions burned: 9515 (million)
% 207.34/29.68 % (3888253)ott-2_1_sil=16000:newcnf=on:random_seed=1316445606:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 207.34/29.68 % (3888255)ott+10_1_sil=32000:tgt=ground:random_seed=2015035680:i=5114:av=off_2954 on theBenchmark for (2954ds/5114Mi)
% 207.34/29.68 % (3888251)Instruction limit reached!
% 207.34/29.68 % (3888251)------------------------------
% 207.34/29.68 % (3888251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.34/29.68 % (3888251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.34/29.68 % (3888251)CaDiCaL version: 2.1.3
% 207.34/29.68 % (3888251)Termination reason: Instruction limit
% 207.34/29.68 % (3888251)Termination phase: Finite model building constraint generation
% 207.34/29.68 % (3888251)Time elapsed: 0.770 s
% 207.34/29.68 % (3888251)Peak memory usage: 121 MB
% 207.34/29.68 % (3888251)Instructions burned: 2174 (million)
% 207.34/29.68 % (3888257)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1498639568:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 207.34/29.68 % TRYING [1]
% 207.34/29.68 % (3888253)Instruction limit reached!
% 207.34/29.68 % (3888253)------------------------------
% 207.34/29.68 % (3888253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.34/29.68 % (3888253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.34/29.68 % (3888253)CaDiCaL version: 2.1.3
% 207.34/29.68 % (3888253)Termination reason: Instruction limit
% 207.34/29.68 % (3888253)Termination phase: Saturation
% 207.34/29.68 % (3888253)Time elapsed: 0.474 s
% 207.34/29.68 % (3888253)Peak memory usage: 33 MB
% 207.34/29.68 % (3888253)Instructions burned: 869 (million)
% 207.34/29.68 % TRYING [2]
% 207.34/29.68 % (3888259)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1646359014:i=3512:aac=none_2950 on theBenchmark for (2950ds/3512Mi)
% 207.34/29.68 % TRYING [5]
% 207.34/29.68 % TRYING [3]
% 207.34/29.68 % (3888238)Instruction limit reached!
% 207.34/29.68 % (3888238)------------------------------
% 207.34/29.68 % (3888238)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 207.34/29.68 % (3888238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 207.34/29.68 % (3888238)CaDiCaL version: 2.1.3
% 207.34/29.68 % (3888238)Termination reason: Instruction limit
% 207.34/29.68 % (3888238)Termination phase: Finite model building SAT solving
% 207.34/29.68 % (3888238)Time elapsed: 5.058 s
% 207.34/29.68 % (3888238)Peak memory usage: 221 MB
% 207.34/29.68 % (3888238)Instructions burned: 22061 (million)
% 207.34/29.68 % (3888261)dis+21_1_sil=32000:sas=cadical:random_seed=3277949645:i=3773:amm=off_2941 on theBenchmark for (2941ds/3773Mi)
% 207.34/29.68 % (3888261)Instruction limit reached!
% 207.34/29.68 % (3888261)------------------------------
% 273.22/41.03 % (3888261)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888261)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888261)Termination reason: Instruction limit
% 273.22/41.03 % (3888261)Termination phase: Saturation
% 273.22/41.03 % (3888261)Time elapsed: 0.866 s
% 273.22/41.03 % (3888261)Peak memory usage: 57 MB
% 273.22/41.03 % (3888261)Instructions burned: 3773 (million)
% 273.22/41.03 % (3888263)ott+11_1_sil=16000:gs=on:random_seed=971097758:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2932 on theBenchmark for (2932ds/2251Mi)
% 273.22/41.03 % (3888259)Instruction limit reached!
% 273.22/41.03 % (3888259)------------------------------
% 273.22/41.03 % (3888259)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888259)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888259)Termination reason: Instruction limit
% 273.22/41.03 % (3888259)Termination phase: Saturation
% 273.22/41.03 % (3888259)Time elapsed: 1.836 s
% 273.22/41.03 % (3888259)Peak memory usage: 66 MB
% 273.22/41.03 % (3888259)Instructions burned: 3513 (million)
% 273.22/41.03 % (3888265)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3742311140:fmbsr=1.6:i=67534_2931 on theBenchmark for (2931ds/67534Mi)
% 273.22/41.03 % TRYING [4]
% 273.22/41.03 % TRYING [7]
% 273.22/41.03 % (3888255)Instruction limit reached!
% 273.22/41.03 % (3888255)------------------------------
% 273.22/41.03 % (3888255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888255)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888255)Termination reason: Instruction limit
% 273.22/41.03 % (3888255)Termination phase: Saturation
% 273.22/41.03 % (3888255)Time elapsed: 2.659 s
% 273.22/41.03 % (3888255)Peak memory usage: 119 MB
% 273.22/41.03 % (3888255)Instructions burned: 5115 (million)
% 273.22/41.03 % (3888267)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2780591278:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2927 on theBenchmark for (2927ds/4591Mi)
% 273.22/41.03 % (3888263)Instruction limit reached!
% 273.22/41.03 % (3888263)------------------------------
% 273.22/41.03 % (3888263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888263)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888263)Termination reason: Instruction limit
% 273.22/41.03 % (3888263)Termination phase: Saturation
% 273.22/41.03 % (3888263)Time elapsed: 0.695 s
% 273.22/41.03 % (3888263)Peak memory usage: 54 MB
% 273.22/41.03 % (3888263)Instructions burned: 2252 (million)
% 273.22/41.03 % (3888269)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1469467054:i=29340_2925 on theBenchmark for (2925ds/29340Mi)
% 273.22/41.03 % (3888267)Instruction limit reached!
% 273.22/41.03 % (3888267)------------------------------
% 273.22/41.03 % (3888267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888267)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888267)Termination reason: Instruction limit
% 273.22/41.03 % (3888267)Termination phase: Saturation
% 273.22/41.03 % (3888267)Time elapsed: 2.448 s
% 273.22/41.03 % (3888267)Peak memory usage: 64 MB
% 273.22/41.03 % (3888267)Instructions burned: 4591 (million)
% 273.22/41.03 % (3888271)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2295532060:i=5211_2903 on theBenchmark for (2903ds/5211Mi)
% 273.22/41.03 % TRYING [5]
% 273.22/41.03 % (3888271)Instruction limit reached!
% 273.22/41.03 % (3888271)------------------------------
% 273.22/41.03 % (3888271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888271)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888271)Termination reason: Instruction limit
% 273.22/41.03 % (3888271)Termination phase: Saturation
% 273.22/41.03 % (3888271)Time elapsed: 2.489 s
% 273.22/41.03 % (3888271)Peak memory usage: 49 MB
% 273.22/41.03 % (3888271)Instructions burned: 5211 (million)
% 273.22/41.03 % (3888273)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=250298497:i=5497:nm=2_2877 on theBenchmark for (2877ds/5497Mi)
% 273.22/41.03 % TRYING [17]
% 273.22/41.03 % TRYING [6]
% 273.22/41.03 % (3888273)Instruction limit reached!
% 273.22/41.03 % (3888273)------------------------------
% 273.22/41.03 % (3888273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888273)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888273)Termination reason: Instruction limit
% 273.22/41.03 % (3888273)Termination phase: Finite model building constraint generation
% 273.22/41.03 % (3888273)Time elapsed: 2.015 s
% 273.22/41.03 % (3888273)Peak memory usage: 350 MB
% 273.22/41.03 % (3888273)Instructions burned: 5498 (million)
% 273.22/41.03 % (3888275)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2496347297:fmbsr=2:i=46332_2857 on theBenchmark for (2857ds/46332Mi)
% 273.22/41.03 % TRYING [15]
% 273.22/41.03 % (3888269)Instruction limit reached!
% 273.22/41.03 % (3888269)------------------------------
% 273.22/41.03 % (3888269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888269)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888269)Termination reason: Instruction limit
% 273.22/41.03 % (3888269)Termination phase: Saturation
% 273.22/41.03 % (3888269)Time elapsed: 7.353 s
% 273.22/41.03 % (3888269)Peak memory usage: 79 MB
% 273.22/41.03 % (3888269)Instructions burned: 29344 (million)
% 273.22/41.03 % (3888277)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=712355028:i=14071_2851 on theBenchmark for (2851ds/14071Mi)
% 273.22/41.03 % TRYING [12]
% 273.22/41.03 % (3888277)Instruction limit reached!
% 273.22/41.03 % (3888277)------------------------------
% 273.22/41.03 % (3888277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888277)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888277)Termination reason: Instruction limit
% 273.22/41.03 % (3888277)Termination phase: Finite model building constraint generation
% 273.22/41.03 % (3888277)Time elapsed: 3.782 s
% 273.22/41.03 % (3888277)Peak memory usage: 1121 MB
% 273.22/41.03 % (3888277)Instructions burned: 14072 (million)
% 273.22/41.03 % (3888279)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=918681361:i=22565:add=on:rawr=on_2812 on theBenchmark for (2812ds/22565Mi)
% 273.22/41.03 % TRYING [6]
% 273.22/41.03 % (3888279)Instruction limit reached!
% 273.22/41.03 % (3888279)------------------------------
% 273.22/41.03 % (3888279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888279)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888279)Termination reason: Instruction limit
% 273.22/41.03 % (3888279)Termination phase: Saturation
% 273.22/41.03 % (3888279)Time elapsed: 4.773 s
% 273.22/41.03 % (3888279)Peak memory usage: 152 MB
% 273.22/41.03 % (3888279)Instructions burned: 22565 (million)
% 273.22/41.03 % (3888281)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3943505833:i=8173:av=off_2764 on theBenchmark for (2764ds/8173Mi)
% 273.22/41.03 % (3888281)Instruction limit reached!
% 273.22/41.03 % (3888281)------------------------------
% 273.22/41.03 % (3888281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888281)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888281)Termination reason: Instruction limit
% 273.22/41.03 % (3888281)Termination phase: Saturation
% 273.22/41.03 % (3888281)Time elapsed: 2.717 s
% 273.22/41.03 % (3888281)Peak memory usage: 214 MB
% 273.22/41.03 % (3888281)Instructions burned: 8174 (million)
% 273.22/41.03 % (3888283)dis+10_16:1_sil=16000:random_seed=3157726595:i=9155:fsr=off_2737 on theBenchmark for (2737ds/9155Mi)
% 273.22/41.03 % TRYING [7]
% 273.22/41.03 % TRYING [7]
% 273.22/41.03 % (3888283)Instruction limit reached!
% 273.22/41.03 % (3888283)------------------------------
% 273.22/41.03 % (3888283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888283)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888283)Termination reason: Instruction limit
% 273.22/41.03 % (3888283)Termination phase: Saturation
% 273.22/41.03 % (3888283)Time elapsed: 2.147 s
% 273.22/41.03 % (3888283)Peak memory usage: 82 MB
% 273.22/41.03 % (3888283)Instructions burned: 9158 (million)
% 273.22/41.03 % (3888285)ott-3_8_sil=64000:random_seed=1899103118:i=20139:bs=on_2715 on theBenchmark for (2715ds/20139Mi)
% 273.22/41.03 % (3888257)Instruction limit reached!
% 273.22/41.03 % (3888257)------------------------------
% 273.22/41.03 % (3888257)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888257)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888257)Termination reason: Instruction limit
% 273.22/41.03 % (3888257)Termination phase: Finite model building constraint generation
% 273.22/41.03 % (3888257)Time elapsed: 24.773 s
% 273.22/41.03 % (3888257)Peak memory usage: 364 MB
% 273.22/41.03 % (3888257)Instructions burned: 54284 (million)
% 273.22/41.03 % (3888287)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4102758224:fmbsr=2:i=32576_2704 on theBenchmark for (2704ds/32576Mi)
% 273.22/41.03 % TRYING [9]
% 273.22/41.03 % (3888285)Instruction limit reached!
% 273.22/41.03 % (3888285)------------------------------
% 273.22/41.03 % (3888285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888285)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888285)Termination reason: Instruction limit
% 273.22/41.03 % (3888285)Termination phase: Saturation
% 273.22/41.03 % (3888285)Time elapsed: 6.291 s
% 273.22/41.03 % (3888285)Peak memory usage: 97 MB
% 273.22/41.03 % (3888285)Instructions burned: 20140 (million)
% 273.22/41.03 % (3888289)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3920652874:i=11404_2652 on theBenchmark for (2652ds/11404Mi)
% 273.22/41.03 % (3888206)Instruction limit reached!
% 273.22/41.03 % (3888206)------------------------------
% 273.22/41.03 % (3888206)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888206)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888206)Termination reason: Instruction limit
% 273.22/41.03 % (3888206)Termination phase: Saturation
% 273.22/41.03 % (3888206)Time elapsed: 35.997 s
% 273.22/41.03 % (3888206)Peak memory usage: 271 MB
% 273.22/41.03 % (3888206)Instructions burned: 88025 (million)
% 273.22/41.03 % (3888291)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=843439769:i=14134_2637 on theBenchmark for (2637ds/14134Mi)
% 273.22/41.03 % (3888275)Instruction limit reached!
% 273.22/41.03 % (3888275)------------------------------
% 273.22/41.03 % (3888275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888275)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888275)Termination reason: Instruction limit
% 273.22/41.03 % (3888275)Termination phase: Finite model building constraint generation
% 273.22/41.03 % (3888275)Time elapsed: 22.007 s
% 273.22/41.03 % (3888275)Peak memory usage: 3367 MB
% 273.22/41.03 % (3888275)Instructions burned: 46333 (million)
% 273.22/41.03 % (3888293)dis+33_16_sil=32000:sac=on:random_seed=2165653997:i=15851:nm=0_2632 on theBenchmark for (2632ds/15851Mi)
% 273.22/41.03 % (3888289)Instruction limit reached!
% 273.22/41.03 % (3888289)------------------------------
% 273.22/41.03 % (3888289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888289)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888289)Termination reason: Instruction limit
% 273.22/41.03 % (3888289)Termination phase: Saturation
% 273.22/41.03 % (3888289)Time elapsed: 2.726 s
% 273.22/41.03 % (3888289)Peak memory usage: 146 MB
% 273.22/41.03 % (3888289)Instructions burned: 11409 (million)
% 273.22/41.03 % (3888295)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3641478972:avsq=on:i=17627:add=on:amm=off_2624 on theBenchmark for (2624ds/17627Mi)
% 273.22/41.03 % (3888265)Instruction limit reached!
% 273.22/41.03 % (3888265)------------------------------
% 273.22/41.03 % (3888265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.03 % (3888265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.03 % (3888265)CaDiCaL version: 2.1.3
% 273.22/41.03 % (3888265)Termination reason: Instruction limit
% 273.22/41.03 % (3888265)Termination phase: Finite model building SAT solving
% 273.22/41.03 % (3888265)Time elapsed: 31.177 s
% 273.22/41.03 % (3888265)Peak memory usage: 288 MB
% 273.22/41.03 % (3888265)Instructions burned: 67534 (million)
% 273.22/41.03 % (3888297)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2882059921:s2a=on:i=53295_2618 on theBenchmark for (2618ds/53295Mi)
% 273.22/41.03 % (3888293) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3888199-3888293"...
% 273.22/41.03 % (3888293)...printing done.
% 273.22/41.03 % (3888293)Refutation found. Thanks to Tanya!
% 273.22/41.03 % SZS status Theorem for theBenchmark
% 273.22/41.03 % SZS output start Proof for theBenchmark
% See solution above
% 273.22/41.05 % (3888293)------------------------------
% 273.22/41.05 % (3888293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 273.22/41.05 % (3888293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 273.22/41.05 % (3888293)CaDiCaL version: 2.1.3
% 273.22/41.05 % (3888293)Termination reason: Refutation
% 273.22/41.05 % (3888293)Time elapsed: 3.886 s
% 273.22/41.05 % (3888293)Peak memory usage: 87 MB
% 273.22/41.05 % (3888293)Instructions burned: 8427 (million)
% 273.22/41.05 % (3888199)Success in time 40.814 s
% 273.22/41.05 % Vampire exiting
%------------------------------------------------------------------------------