%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR116+35 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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 274.03s 40.53s
% Output : Refutation 274.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 16
% Syntax : Number of formulae : 136 ( 40 unt; 7 def)
% Number of atoms : 1357 ( 0 equ)
% Maximal formula atoms : 160 ( 9 avg)
% Number of connectives : 1476 ( 255 ~; 224 |; 985 &)
% ( 7 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 160 ( 12 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 39 ( 38 usr; 8 prp; 0-2 aty)
% Number of functors : 64 ( 64 usr; 56 con; 0-3 aty)
% Number of variables : 225 ( 0 sgn 184 !; 41 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',member_first) ).
fof(f11,axiom,
! [X0,X1] :
( fact(X0,X1)
=> has_fact_leq(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',has_fact_eq) ).
fof(f95,axiom,
! [X0,X1] :
( ( has_fact_leq(X1,real)
& loc(X1,X0) )
=> ? [X2] :
( loc(X2,X0)
& obj(X2,X1)
& subs(X2,geben_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',loc__geben_1_1_loc) ).
fof(f155,axiom,
! [X0,X1,X2] :
( ( prop(X0,X1)
& state_adjective_state_binding(X1,X2) )
=> ? [X3,X4,X5] :
( in(X5,X3)
& attr(X3,X4)
& loc(X0,X5)
& sub(X3,land_1_1)
& sub(X4,name_1_1)
& val(X4,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',state_adjective__in_state) ).
fof(f159,axiom,
! [X0,X1,X2] :
( ( attr(X2,X0)
& member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
& sub(X0,X1) )
=> ? [X3] :
( arg1(X3,X2)
& arg2(X3,X2)
& subs(X3,hei__337en_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',attr_name_hei__337en_1_1) ).
fof(f161,axiom,
! [X0,X1,X2] :
( ( arg1(X0,X1)
& arg2(X0,X2)
& subs(X0,hei__337en_1_1) )
=> ? [X3,X4] :
( arg1(X4,X1)
& arg2(X4,X2)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',hei__337en_1_1__bezeichnen_1_1_als) ).
fof(f9161,axiom,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',fact_8980) ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( in(X5,X6)
& arg1(X3,X0)
& arg2(X3,X4)
& attr(X0,X1)
& attr(X0,X2)
& attr(X6,X7)
& obj(X8,X0)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X9)
& sub(X7,name_1_1)
& subr(X3,rprs_0)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X7,s__374dafrika_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_010_mira_wp_714) ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( in(X5,X6)
& arg1(X3,X0)
& arg2(X3,X4)
& attr(X0,X1)
& attr(X0,X2)
& attr(X6,X7)
& obj(X8,X0)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X9)
& sub(X7,name_1_1)
& subr(X3,rprs_0)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X7,s__374dafrika_0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& just(c38,c40)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& sort(amtszeit__1_1,ta)
& card(amtszeit__1_1,int1)
& etype(amtszeit__1_1,int0)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& quant(amtszeit__1_1,one)
& refer(amtszeit__1_1,refer_c)
& varia(amtszeit__1_1,varia_c)
& sort(amt_1_2,ad)
& sort(amt_1_2,io)
& card(amt_1_2,int1)
& etype(amt_1_2,int0)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& quant(amt_1_2,one)
& refer(amt_1_2,refer_c)
& varia(amt_1_2,varia_c)
& sort(zeit_1_1,ta)
& card(zeit_1_1,int1)
& etype(zeit_1_1,int0)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& quant(zeit_1_1,one)
& refer(zeit_1_1,refer_c)
& varia(zeit_1_1,varia_c)
& sort(c16,d)
& card(c16,int1)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& quant(c16,one)
& refer(c16,det)
& varia(c16,con)
& sort(c7,ta)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,det)
& varia(c7,con)
& sort(c17,na)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,indet)
& varia(c17,varia_c)
& sort(c18,na)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,indet)
& varia(c18,varia_c)
& sort(s__374dafrikanisch_1_1,nq)
& sort(pr__344sident_1_1,d)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& sort(eigenname_1_1,na)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& sort(nelson_0,fe)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(mandela_0,fe)
& sort(c24,o)
& card(c24,cons(x_constant,cons(int1,nil)))
& etype(c24,int1)
& etype(c24,int2)
& etype(c24,int3)
& fact(c24,real)
& gener(c24,sp)
& quant(c24,mult)
& refer(c24,indet)
& varia(c24,varia_c)
& sort(mehrere_2_1,o)
& card(mehrere_2_1,cons(x_constant,cons(int1,nil)))
& etype(mehrere_2_1,int1)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& quant(mehrere_2_1,mult)
& refer(mehrere_2_1,refer_c)
& varia(mehrere_2_1,varia_c)
& sort(c34,d)
& card(c34,int100)
& etype(c34,int1)
& fact(c34,real)
& gener(c34,sp)
& quant(c34,nfquant)
& refer(c34,indet)
& varia(c34,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(c38,o)
& card(c38,int1)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,gener_c)
& quant(c38,one)
& refer(c38,refer_c)
& varia(c38,varia_c)
& sort(c40,da)
& fact(c40,real)
& gener(c40,sp)
& sort(geisterglaube_1_1,o)
& card(geisterglaube_1_1,int1)
& etype(geisterglaube_1_1,int0)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& quant(geisterglaube_1_1,one)
& refer(geisterglaube_1_1,refer_c)
& varia(geisterglaube_1_1,varia_c)
& sort(abmurksen_1_1,da)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_wp_714) ).
fof(f10191,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& sort(amtszeit__1_1,ta)
& card(amtszeit__1_1,int1)
& etype(amtszeit__1_1,int0)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& quant(amtszeit__1_1,one)
& refer(amtszeit__1_1,refer_c)
& varia(amtszeit__1_1,varia_c)
& sort(amt_1_2,ad)
& sort(amt_1_2,io)
& card(amt_1_2,int1)
& etype(amt_1_2,int0)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& quant(amt_1_2,one)
& refer(amt_1_2,refer_c)
& varia(amt_1_2,varia_c)
& sort(zeit_1_1,ta)
& card(zeit_1_1,int1)
& etype(zeit_1_1,int0)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& quant(zeit_1_1,one)
& refer(zeit_1_1,refer_c)
& varia(zeit_1_1,varia_c)
& sort(c16,d)
& card(c16,int1)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& quant(c16,one)
& refer(c16,det)
& varia(c16,con)
& sort(c7,ta)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,det)
& varia(c7,con)
& sort(c17,na)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,indet)
& varia(c17,varia_c)
& sort(c18,na)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,indet)
& varia(c18,varia_c)
& sort(s__374dafrikanisch_1_1,nq)
& sort(pr__344sident_1_1,d)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& sort(eigenname_1_1,na)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& sort(nelson_0,fe)
& sort(familiename_1_1,na)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& sort(mandela_0,fe)
& sort(c24,o)
& card(c24,cons(x_constant,cons(int1,nil)))
& etype(c24,int1)
& etype(c24,int2)
& etype(c24,int3)
& fact(c24,real)
& gener(c24,sp)
& quant(c24,mult)
& refer(c24,indet)
& varia(c24,varia_c)
& sort(mehrere_2_1,o)
& card(mehrere_2_1,cons(x_constant,cons(int1,nil)))
& etype(mehrere_2_1,int1)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& quant(mehrere_2_1,mult)
& refer(mehrere_2_1,refer_c)
& varia(mehrere_2_1,varia_c)
& sort(c34,d)
& card(c34,int100)
& etype(c34,int1)
& fact(c34,real)
& gener(c34,sp)
& quant(c34,nfquant)
& refer(c34,indet)
& varia(c34,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(c38,o)
& card(c38,int1)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,gener_c)
& quant(c38,one)
& refer(c38,refer_c)
& varia(c38,varia_c)
& sort(c40,da)
& fact(c40,real)
& gener(c40,sp)
& sort(geisterglaube_1_1,o)
& card(geisterglaube_1_1,int1)
& etype(geisterglaube_1_1,int0)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& quant(geisterglaube_1_1,one)
& refer(geisterglaube_1_1,refer_c)
& varia(geisterglaube_1_1,varia_c)
& sort(abmurksen_1_1,da)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10327,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& card(amtszeit__1_1,int1)
& etype(amtszeit__1_1,int0)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& quant(amtszeit__1_1,one)
& refer(amtszeit__1_1,refer_c)
& varia(amtszeit__1_1,varia_c)
& card(amt_1_2,int1)
& etype(amt_1_2,int0)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& quant(amt_1_2,one)
& refer(amt_1_2,refer_c)
& varia(amt_1_2,varia_c)
& card(zeit_1_1,int1)
& etype(zeit_1_1,int0)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& quant(zeit_1_1,one)
& refer(zeit_1_1,refer_c)
& varia(zeit_1_1,varia_c)
& card(c16,int1)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& quant(c16,one)
& refer(c16,det)
& varia(c16,con)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& quant(c7,one)
& refer(c7,det)
& varia(c7,con)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& quant(c17,one)
& refer(c17,indet)
& varia(c17,varia_c)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,indet)
& varia(c18,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(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(c24,cons(x_constant,cons(int1,nil)))
& etype(c24,int1)
& etype(c24,int2)
& etype(c24,int3)
& fact(c24,real)
& gener(c24,sp)
& quant(c24,mult)
& refer(c24,indet)
& varia(c24,varia_c)
& card(mehrere_2_1,cons(x_constant,cons(int1,nil)))
& etype(mehrere_2_1,int1)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& quant(mehrere_2_1,mult)
& refer(mehrere_2_1,refer_c)
& varia(mehrere_2_1,varia_c)
& card(c34,int100)
& etype(c34,int1)
& fact(c34,real)
& gener(c34,sp)
& quant(c34,nfquant)
& refer(c34,indet)
& varia(c34,varia_c)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& card(c38,int1)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,gener_c)
& quant(c38,one)
& refer(c38,refer_c)
& varia(c38,varia_c)
& fact(c40,real)
& gener(c40,sp)
& card(geisterglaube_1_1,int1)
& etype(geisterglaube_1_1,int0)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& quant(geisterglaube_1_1,one)
& refer(geisterglaube_1_1,refer_c)
& varia(geisterglaube_1_1,varia_c)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10330,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& card(amtszeit__1_1,int1)
& etype(amtszeit__1_1,int0)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& refer(amtszeit__1_1,refer_c)
& varia(amtszeit__1_1,varia_c)
& card(amt_1_2,int1)
& etype(amt_1_2,int0)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& refer(amt_1_2,refer_c)
& varia(amt_1_2,varia_c)
& card(zeit_1_1,int1)
& etype(zeit_1_1,int0)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& refer(zeit_1_1,refer_c)
& varia(zeit_1_1,varia_c)
& card(c16,int1)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& refer(c16,det)
& varia(c16,con)
& card(c7,int1)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& refer(c7,det)
& varia(c7,con)
& card(c17,int1)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& refer(c17,indet)
& varia(c17,varia_c)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& refer(c18,indet)
& varia(c18,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(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(c24,cons(x_constant,cons(int1,nil)))
& etype(c24,int1)
& etype(c24,int2)
& etype(c24,int3)
& fact(c24,real)
& gener(c24,sp)
& refer(c24,indet)
& varia(c24,varia_c)
& card(mehrere_2_1,cons(x_constant,cons(int1,nil)))
& etype(mehrere_2_1,int1)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& refer(mehrere_2_1,refer_c)
& varia(mehrere_2_1,varia_c)
& card(c34,int100)
& etype(c34,int1)
& fact(c34,real)
& gener(c34,sp)
& refer(c34,indet)
& varia(c34,varia_c)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& card(c38,int1)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,gener_c)
& refer(c38,refer_c)
& varia(c38,varia_c)
& fact(c40,real)
& gener(c40,sp)
& card(geisterglaube_1_1,int1)
& etype(geisterglaube_1_1,int0)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& refer(geisterglaube_1_1,refer_c)
& varia(geisterglaube_1_1,varia_c)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10327]) ).
fof(f10333,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& etype(amtszeit__1_1,int0)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& refer(amtszeit__1_1,refer_c)
& varia(amtszeit__1_1,varia_c)
& etype(amt_1_2,int0)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& refer(amt_1_2,refer_c)
& varia(amt_1_2,varia_c)
& etype(zeit_1_1,int0)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& refer(zeit_1_1,refer_c)
& varia(zeit_1_1,varia_c)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& refer(c16,det)
& varia(c16,con)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& refer(c7,det)
& varia(c7,con)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& refer(c17,indet)
& varia(c17,varia_c)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& refer(c18,indet)
& varia(c18,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(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(c24,int1)
& etype(c24,int2)
& etype(c24,int3)
& fact(c24,real)
& gener(c24,sp)
& refer(c24,indet)
& varia(c24,varia_c)
& etype(mehrere_2_1,int1)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& refer(mehrere_2_1,refer_c)
& varia(mehrere_2_1,varia_c)
& etype(c34,int1)
& fact(c34,real)
& gener(c34,sp)
& refer(c34,indet)
& varia(c34,varia_c)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,gener_c)
& refer(c38,refer_c)
& varia(c38,varia_c)
& fact(c40,real)
& gener(c40,sp)
& etype(geisterglaube_1_1,int0)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& refer(geisterglaube_1_1,refer_c)
& varia(geisterglaube_1_1,varia_c)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10330]) ).
fof(f10336,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& etype(amtszeit__1_1,int0)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& varia(amtszeit__1_1,varia_c)
& etype(amt_1_2,int0)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& varia(amt_1_2,varia_c)
& etype(zeit_1_1,int0)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& varia(zeit_1_1,varia_c)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& varia(c16,con)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& varia(c7,con)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& varia(c17,varia_c)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& varia(c18,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(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(c24,int1)
& etype(c24,int2)
& etype(c24,int3)
& fact(c24,real)
& gener(c24,sp)
& varia(c24,varia_c)
& etype(mehrere_2_1,int1)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& varia(mehrere_2_1,varia_c)
& etype(c34,int1)
& fact(c34,real)
& gener(c34,sp)
& varia(c34,varia_c)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& varia(mensch_1_1,varia_c)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,gener_c)
& varia(c38,varia_c)
& fact(c40,real)
& gener(c40,sp)
& etype(geisterglaube_1_1,int0)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& varia(geisterglaube_1_1,varia_c)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10333]) ).
fof(f10341,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& etype(amtszeit__1_1,int0)
& fact(amtszeit__1_1,real)
& gener(amtszeit__1_1,ge)
& etype(amt_1_2,int0)
& fact(amt_1_2,real)
& gener(amt_1_2,ge)
& etype(zeit_1_1,int0)
& fact(zeit_1_1,real)
& gener(zeit_1_1,ge)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& etype(c7,int0)
& fact(c7,real)
& gener(c7,sp)
& etype(c17,int0)
& fact(c17,real)
& gener(c17,sp)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& etype(c24,int1)
& etype(c24,int2)
& etype(c24,int3)
& fact(c24,real)
& gener(c24,sp)
& etype(mehrere_2_1,int1)
& fact(mehrere_2_1,real)
& gener(mehrere_2_1,gener_c)
& etype(c34,int1)
& fact(c34,real)
& gener(c34,sp)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& etype(c38,int0)
& fact(c38,real)
& gener(c38,gener_c)
& fact(c40,real)
& gener(c40,sp)
& etype(geisterglaube_1_1,int0)
& fact(geisterglaube_1_1,real)
& gener(geisterglaube_1_1,ge)
& fact(abmurksen_1_1,real)
& gener(abmurksen_1_1,ge) ),
inference(pure_predicate_removal,[],[f10336]) ).
fof(f10346,plain,
( assoc(amtszeit__1_1,amt_1_2)
& sub(amtszeit__1_1,zeit_1_1)
& attch(c16,c7)
& attr(c16,c17)
& attr(c16,c18)
& prop(c16,s__374dafrikanisch_1_1)
& sub(c16,pr__344sident_1_1)
& sub(c17,eigenname_1_1)
& val(c17,nelson_0)
& sub(c18,familiename_1_1)
& val(c18,mandela_0)
& pred(c24,mehrere_2_1)
& pred(c34,mensch_1_1)
& sub(c38,geisterglaube_1_1)
& aff(c40,c24)
& benf(c40,c34)
& subs(c40,abmurksen_1_1)
& temp(c40,c7)
& sub(c7,amtszeit__1_1)
& etype(amtszeit__1_1,int0)
& fact(amtszeit__1_1,real)
& etype(amt_1_2,int0)
& fact(amt_1_2,real)
& etype(zeit_1_1,int0)
& fact(zeit_1_1,real)
& etype(c16,int0)
& fact(c16,real)
& etype(c7,int0)
& fact(c7,real)
& etype(c17,int0)
& fact(c17,real)
& etype(c18,int0)
& fact(c18,real)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& etype(c24,int1)
& etype(c24,int2)
& etype(c24,int3)
& fact(c24,real)
& etype(mehrere_2_1,int1)
& fact(mehrere_2_1,real)
& etype(c34,int1)
& fact(c34,real)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& etype(c38,int0)
& fact(c38,real)
& fact(c40,real)
& etype(geisterglaube_1_1,int0)
& fact(geisterglaube_1_1,real)
& fact(abmurksen_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(f20845,plain,
fact(c16,real),
inference(cnf_transformation,[],[f10346]) ).
fof(f20861,plain,
val(c18,mandela_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20862,plain,
sub(c18,familiename_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20863,plain,
val(c17,nelson_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20864,plain,
sub(c17,eigenname_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20865,plain,
sub(c16,pr__344sident_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20866,plain,
prop(c16,s__374dafrikanisch_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20867,plain,
attr(c16,c18),
inference(cnf_transformation,[],[f10346]) ).
fof(f20868,plain,
attr(c16,c17),
inference(cnf_transformation,[],[f10346]) ).
fof(f20873,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(f20874,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,[],[f20873]) ).
fof(f20876,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(f20877,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,[],[f20876]) ).
fof(f20878,plain,
( spl63_1
| spl63_2 ),
inference(avatar_split_clause,[],[f20816,f20876,f20873]) ).
fof(f20910,plain,
has_fact_leq(c16,real),
inference(resolution,[],[f10602,f20845]) ).
fof(f60110,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| val(sK48(X0,s__374dafrika_0),s__374dafrika_0) ),
inference(resolution,[],[f10852,f19789]) ).
fof(f60296,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| sub(sK48(X0,s__374dafrika_0),name_1_1) ),
inference(resolution,[],[f10853,f19789]) ).
fof(f60668,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| loc(X0,sK49(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10855,f19789]) ).
fof(f63040,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| attr(sK47(X0,s__374dafrika_0),sK48(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10856,f19789]) ).
fof(f63226,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| in(sK49(X0,s__374dafrika_0),sK47(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10857,f19789]) ).
fof(f71494,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| subs(sK50(X0),hei__337en_1_1)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10860,f10600]) ).
fof(f71496,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| arg2(sK50(X0),X0)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10861,f10600]) ).
fof(f71498,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| arg1(sK50(X0),X0)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10862,f10600]) ).
fof(f72561,plain,
val(sK48(c16,s__374dafrika_0),s__374dafrika_0),
inference(resolution,[],[f60110,f20866]) ).
fof(f72566,plain,
sub(sK48(c16,s__374dafrika_0),name_1_1),
inference(resolution,[],[f60296,f20866]) ).
fof(f72599,plain,
loc(c16,sK49(c16,s__374dafrika_0)),
inference(resolution,[],[f60668,f20866]) ).
fof(f72607,plain,
( ~ has_fact_leq(c16,real)
| obj(sK2(sK49(c16,s__374dafrika_0),c16),c16) ),
inference(resolution,[],[f72599,f10686]) ).
fof(f72618,plain,
obj(sK2(sK49(c16,s__374dafrika_0),c16),c16),
inference(forward_subsumption_resolution,[],[f72607,f20910]) ).
fof(f72850,plain,
attr(sK47(c16,s__374dafrika_0),sK48(c16,s__374dafrika_0)),
inference(resolution,[],[f63040,f20866]) ).
fof(f72851,plain,
( ! [X0] :
( ~ val(sK48(c16,s__374dafrika_0),s__374dafrika_0)
| ~ sub(sK48(c16,s__374dafrika_0),name_1_1)
| ~ in(X0,sK47(c16,s__374dafrika_0)) )
| ~ spl63_2 ),
inference(resolution,[],[f72850,f20877]) ).
fof(f72852,plain,
( ! [X0] :
( ~ sub(sK48(c16,s__374dafrika_0),name_1_1)
| ~ in(X0,sK47(c16,s__374dafrika_0)) )
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f72851,f72561]) ).
fof(f72853,plain,
( ! [X0] : ~ in(X0,sK47(c16,s__374dafrika_0))
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f72852,f72566]) ).
fof(f72854,plain,
in(sK49(c16,s__374dafrika_0),sK47(c16,s__374dafrika_0)),
inference(resolution,[],[f63226,f20866]) ).
fof(f72855,plain,
( $false
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f72854,f72853]) ).
fof(f72856,plain,
~ spl63_2,
inference(avatar_contradiction_clause,[],[f72855]) ).
fof(f76282,plain,
! [X0] :
( ~ attr(X0,c17)
| subs(sK50(X0),hei__337en_1_1) ),
inference(resolution,[],[f71494,f20864]) ).
fof(f76371,plain,
! [X0] :
( ~ attr(X0,c17)
| arg2(sK50(X0),X0) ),
inference(resolution,[],[f71496,f20864]) ).
fof(f76460,plain,
! [X0] :
( ~ attr(X0,c17)
| arg1(sK50(X0),X0) ),
inference(resolution,[],[f71498,f20864]) ).
fof(f85148,plain,
subs(sK50(c16),hei__337en_1_1),
inference(resolution,[],[f76282,f20868]) ).
fof(f85150,plain,
! [X0,X1] :
( ~ arg2(sK50(c16),X1)
| ~ arg1(sK50(c16),X0)
| subr(sK53(sK50(c16),X0,X1),rprs_0) ),
inference(resolution,[],[f85148,f10868]) ).
fof(f85154,plain,
! [X0,X1] :
( ~ arg2(sK50(c16),X1)
| ~ arg1(sK50(c16),X0)
| arg2(sK53(sK50(c16),X0,X1),X1) ),
inference(resolution,[],[f85148,f10872]) ).
fof(f85155,plain,
! [X0,X1] :
( ~ arg2(sK50(c16),X1)
| ~ arg1(sK50(c16),X0)
| arg1(sK53(sK50(c16),X0,X1),X0) ),
inference(resolution,[],[f85148,f10873]) ).
fof(f85168,plain,
arg2(sK50(c16),c16),
inference(resolution,[],[f76371,f20868]) ).
fof(f85171,definition,
( spl63_3132
<=> ! [X2] : ~ sub(c16,X2) ),
introduced(definition,[new_symbols(definition,[spl63_3132])],[avatar_definition]) ).
fof(f85172,plain,
( ! [X2] : ~ sub(c16,X2)
| ~ spl63_3132 ),
inference(avatar_component_clause,[],[f85171]) ).
fof(f85181,plain,
arg1(sK50(c16),c16),
inference(resolution,[],[f76460,f20868]) ).
fof(f89812,plain,
! [X0] :
( ~ arg1(sK50(c16),X0)
| subr(sK53(sK50(c16),X0,c16),rprs_0) ),
inference(resolution,[],[f85150,f85168]) ).
fof(f89813,plain,
subr(sK53(sK50(c16),c16,c16),rprs_0),
inference(resolution,[],[f89812,f85181]) ).
fof(f89845,plain,
! [X0] :
( ~ arg1(sK50(c16),X0)
| arg2(sK53(sK50(c16),X0,c16),c16) ),
inference(resolution,[],[f85154,f85168]) ).
fof(f89847,plain,
arg2(sK53(sK50(c16),c16,c16),c16),
inference(resolution,[],[f89845,f85181]) ).
fof(f89848,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ val(X0,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(sK53(sK50(c16),c16,c16),rprs_0)
| ~ sub(c16,X2)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X3,X4)
| ~ attr(X4,X0)
| ~ attr(X4,X1)
| ~ arg1(sK53(sK50(c16),c16,c16),X4) )
| ~ spl63_1 ),
inference(resolution,[],[f89847,f20874]) ).
fof(f89849,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ val(X0,nelson_0)
| ~ val(X1,mandela_0)
| ~ sub(c16,X2)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X3,X4)
| ~ attr(X4,X0)
| ~ attr(X4,X1)
| ~ arg1(sK53(sK50(c16),c16,c16),X4) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f89848,f89813]) ).
fof(f89851,definition,
( spl63_3229
<=> ! [X4,X0,X3,X1] :
( ~ val(X0,nelson_0)
| ~ arg1(sK53(sK50(c16),c16,c16),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_3229])],[avatar_definition]) ).
fof(f89852,plain,
( ! [X3,X0,X1,X4] :
( ~ arg1(sK53(sK50(c16),c16,c16),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_3229 ),
inference(avatar_component_clause,[],[f89851]) ).
fof(f89853,plain,
( spl63_3132
| spl63_3229
| ~ spl63_1 ),
inference(avatar_split_clause,[],[f89849,f20873,f89851,f85171]) ).
fof(f89880,plain,
! [X0] :
( ~ arg1(sK50(c16),X0)
| arg1(sK53(sK50(c16),X0,c16),X0) ),
inference(resolution,[],[f85155,f85168]) ).
fof(f89881,plain,
arg1(sK53(sK50(c16),c16,c16),c16),
inference(resolution,[],[f89880,f85181]) ).
fof(f89882,plain,
( ! [X2,X0,X1] :
( ~ val(X0,nelson_0)
| ~ attr(c16,X1)
| ~ obj(X2,c16)
| ~ attr(c16,X0)
| ~ sub(X0,eigenname_1_1)
| ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1) )
| ~ spl63_3229 ),
inference(resolution,[],[f89881,f89852]) ).
fof(f89885,definition,
( spl63_3230
<=> ! [X2] : ~ obj(X2,c16) ),
introduced(definition,[new_symbols(definition,[spl63_3230])],[avatar_definition]) ).
fof(f89886,plain,
( ! [X2] : ~ obj(X2,c16)
| ~ spl63_3230 ),
inference(avatar_component_clause,[],[f89885]) ).
fof(f89888,definition,
( spl63_3231
<=> ! [X1] :
( ~ attr(c16,X1)
| ~ sub(X1,familiename_1_1)
| ~ val(X1,mandela_0) ) ),
introduced(definition,[new_symbols(definition,[spl63_3231])],[avatar_definition]) ).
fof(f89889,plain,
( ! [X1] :
( ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1)
| ~ attr(c16,X1) )
| ~ spl63_3231 ),
inference(avatar_component_clause,[],[f89888]) ).
fof(f89891,definition,
( spl63_3232
<=> ! [X0] :
( ~ val(X0,nelson_0)
| ~ sub(X0,eigenname_1_1)
| ~ attr(c16,X0) ) ),
introduced(definition,[new_symbols(definition,[spl63_3232])],[avatar_definition]) ).
fof(f89892,plain,
( ! [X0] :
( ~ attr(c16,X0)
| ~ sub(X0,eigenname_1_1)
| ~ val(X0,nelson_0) )
| ~ spl63_3232 ),
inference(avatar_component_clause,[],[f89891]) ).
fof(f89893,plain,
( spl63_3230
| spl63_3231
| spl63_3232
| ~ spl63_3229 ),
inference(avatar_split_clause,[],[f89882,f89851,f89891,f89888,f89885]) ).
fof(f89894,plain,
( $false
| ~ spl63_3230 ),
inference(resolution,[],[f89886,f72618]) ).
fof(f89901,plain,
~ spl63_3230,
inference(avatar_contradiction_clause,[],[f89894]) ).
fof(f89902,plain,
( ~ sub(c18,familiename_1_1)
| ~ attr(c16,c18)
| ~ spl63_3231 ),
inference(resolution,[],[f89889,f20861]) ).
fof(f89903,plain,
( ~ attr(c16,c18)
| ~ spl63_3231 ),
inference(forward_subsumption_resolution,[],[f89902,f20862]) ).
fof(f89904,plain,
( $false
| ~ spl63_3231 ),
inference(forward_subsumption_resolution,[],[f89903,f20867]) ).
fof(f89905,plain,
~ spl63_3231,
inference(avatar_contradiction_clause,[],[f89904]) ).
fof(f89907,plain,
( ~ sub(c17,eigenname_1_1)
| ~ val(c17,nelson_0)
| ~ spl63_3232 ),
inference(resolution,[],[f89892,f20868]) ).
fof(f89908,plain,
( ~ val(c17,nelson_0)
| ~ spl63_3232 ),
inference(forward_subsumption_resolution,[],[f89907,f20864]) ).
fof(f89909,plain,
( $false
| ~ spl63_3232 ),
inference(forward_subsumption_resolution,[],[f89908,f20863]) ).
fof(f89910,plain,
~ spl63_3232,
inference(avatar_contradiction_clause,[],[f89909]) ).
fof(f89911,plain,
( $false
| ~ spl63_3132 ),
inference(resolution,[],[f85172,f20865]) ).
fof(f89912,plain,
~ spl63_3132,
inference(avatar_contradiction_clause,[],[f89911]) ).
cnf(s1,plain,
( spl63_1
| spl63_2 ),
inference(sat_conversion,[],[f20878]) ).
cnf(s78,plain,
~ spl63_2,
inference(sat_conversion,[],[f72856]) ).
cnf(s1167,plain,
( ~ spl63_1
| spl63_3132
| spl63_3229 ),
inference(sat_conversion,[],[f89853]) ).
cnf(s1168,plain,
( ~ spl63_3229
| spl63_3230
| spl63_3231
| spl63_3232 ),
inference(sat_conversion,[],[f89893]) ).
cnf(s1172,plain,
~ spl63_3230,
inference(sat_conversion,[],[f89901]) ).
cnf(s1173,plain,
~ spl63_3231,
inference(sat_conversion,[],[f89905]) ).
cnf(s1174,plain,
~ spl63_3232,
inference(sat_conversion,[],[f89910]) ).
cnf(s1175,plain,
~ spl63_3132,
inference(sat_conversion,[],[f89912]) ).
cnf(s1176,plain,
~ spl63_3229,
inference(rat,[],[s1168,s1174,s1173,s1172]) ).
cnf(s1177,plain,
~ spl63_1,
inference(rat,[],[s1167,s1176,s1175]) ).
cnf(s1180,plain,
$false,
inference(rat,[],[s1,s78,s1177]) ).
fof(f89913,plain,
$false,
inference(avatar_sat_refutation,[],[s1180]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR116+35 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.28 % Computer : n008.cluster.edu
% 0.13/0.28 % Model : x86_64 x86_64
% 0.13/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.28 % Memory : 8046.5625MB
% 0.13/0.28 % OS : Linux 6.8.0-71-generic
% 0.13/0.28 % CPULimit : 300
% 0.13/0.28 % WCLimit : 300
% 0.13/0.28 % DateTime : Mon Sep 28 23:29:55 UTC 2026
% 0.13/0.29 % CPUTime :
% 0.13/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.30/0.34 Running first-order model finding
% 0.30/0.34 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
% 28.79/4.63 % (2757747)Will run a generic schedule for satisfiability detection.
% 28.79/4.63 % (2757753)% WARNING: option uhcvi not known.
% 28.79/4.63 % (2757753)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2791254564:i=135531:add=off:rawr=on_2997 on theBenchmark for (2997ds/135531Mi)
% 28.79/4.63 % (2757754)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1503180256:i=88024:add=on:rawr=on_2997 on theBenchmark for (2997ds/88024Mi)
% 28.79/4.63 % (2757752)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2207010968_2997 on theBenchmark for (2997ds/0Mi)
% 28.79/4.63 % (2757755)dis+10_1_sil=32000:sp=arity:random_seed=3107503529:i=103:fgj=on_2997 on theBenchmark for (2997ds/103Mi)
% 28.79/4.63 % (2757756)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=974852753:i=116_2997 on theBenchmark for (2997ds/116Mi)
% 28.79/4.63 % (2757757)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3970219245:i=131_2997 on theBenchmark for (2997ds/131Mi)
% 28.79/4.63 % (2757758)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2009789288:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2997 on theBenchmark for (2997ds/159Mi)
% 28.79/4.63 % (2757755)Instruction limit reached!
% 28.79/4.63 % (2757755)------------------------------
% 28.79/4.63 % (2757755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.79/4.63 % (2757755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.79/4.63 % (2757755)CaDiCaL version: 2.1.3
% 28.79/4.63 % (2757755)Termination reason: Instruction limit
% 28.79/4.63 % (2757755)Termination phase: Saturation
% 28.79/4.63 % (2757755)Time elapsed: 0.101 s
% 28.79/4.63 % (2757755)Peak memory usage: 26 MB
% 28.79/4.63 % (2757755)Instructions burned: 103 (million)
% 28.79/4.63 % (2757756)Instruction limit reached!
% 28.79/4.63 % (2757756)------------------------------
% 28.79/4.63 % (2757756)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.79/4.63 % (2757756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.79/4.63 % (2757756)CaDiCaL version: 2.1.3
% 28.79/4.63 % (2757756)Termination reason: Instruction limit
% 28.79/4.63 % (2757756)Termination phase: Blocked clause elimination
% 28.79/4.63 % (2757756)Time elapsed: 0.120 s
% 28.79/4.63 % (2757756)Peak memory usage: 27 MB
% 28.79/4.63 % (2757756)Instructions burned: 117 (million)
% 28.79/4.63 % (2757757)Instruction limit reached!
% 28.79/4.63 % (2757757)------------------------------
% 28.79/4.63 % (2757757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.79/4.63 % (2757757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.79/4.63 % (2757757)CaDiCaL version: 2.1.3
% 28.79/4.63 % (2757757)Termination reason: Instruction limit
% 28.79/4.63 % (2757757)Termination phase: Saturation
% 28.79/4.63 % (2757757)Time elapsed: 0.126 s
% 28.79/4.63 % (2757757)Peak memory usage: 27 MB
% 28.79/4.63 % (2757757)Instructions burned: 131 (million)
% 28.79/4.63 % (2757766)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=971809632:i=714:nm=2_2996 on theBenchmark for (2996ds/714Mi)
% 28.79/4.63 % (2757758)Instruction limit reached!
% 28.79/4.63 % (2757758)------------------------------
% 28.79/4.63 % (2757758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.79/4.63 % (2757758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.79/4.63 % (2757758)CaDiCaL version: 2.1.3
% 28.79/4.63 % (2757758)Termination reason: Instruction limit
% 28.79/4.63 % (2757758)Termination phase: Saturation
% 28.79/4.63 % (2757758)Time elapsed: 0.151 s
% 28.79/4.63 % (2757758)Peak memory usage: 29 MB
% 28.79/4.63 % (2757758)Instructions burned: 159 (million)
% 28.79/4.63 % (2757767)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2844394669:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi)
% 28.79/4.63 % (2757769)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=2932987512:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi)
% 28.79/4.63 % (2757770)ott-21_1_sil=16000:fs=off:random_seed=1074153949:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi)
% 28.79/4.63 % (2757767)Instruction limit reached!
% 28.79/4.63 % (2757767)------------------------------
% 28.79/4.63 % (2757767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.79/4.63 % (2757767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.20/7.27 % (2757767)CaDiCaL version: 2.1.3
% 47.20/7.27 % (2757767)Termination reason: Instruction limit
% 47.20/7.27 % (2757767)Termination phase: Blocked clause elimination
% 47.20/7.27 % (2757767)Time elapsed: 0.133 s
% 47.20/7.27 % (2757767)Peak memory usage: 29 MB
% 47.20/7.27 % (2757767)Instructions burned: 132 (million)
% 47.20/7.27 % (2757774)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=878088254:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi)
% 47.20/7.27 % (2757770)Instruction limit reached!
% 47.20/7.27 % (2757770)------------------------------
% 47.20/7.27 % (2757770)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.20/7.27 % (2757770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.20/7.27 % (2757770)CaDiCaL version: 2.1.3
% 47.20/7.27 % (2757770)Termination reason: Instruction limit
% 47.20/7.27 % (2757770)Termination phase: Saturation
% 47.20/7.27 % (2757770)Time elapsed: 0.162 s
% 47.20/7.27 % (2757770)Peak memory usage: 28 MB
% 47.20/7.27 % (2757770)Instructions burned: 180 (million)
% 47.20/7.27 % (2757776)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=624251997:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi)
% 47.20/7.27 % TRYING [1]
% 47.20/7.27 % (2757774)Instruction limit reached!
% 47.20/7.27 % (2757774)------------------------------
% 47.20/7.27 % (2757774)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.20/7.27 % (2757774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.20/7.27 % (2757774)CaDiCaL version: 2.1.3
% 47.20/7.27 % (2757774)Termination reason: Instruction limit
% 47.20/7.27 % (2757774)Termination phase: Saturation
% 47.20/7.27 % (2757774)Time elapsed: 0.149 s
% 47.20/7.27 % (2757774)Peak memory usage: 37 MB
% 47.20/7.27 % (2757774)Instructions burned: 480 (million)
% 47.20/7.27 % TRYING [1]
% 47.20/7.27 % TRYING [2]
% 47.20/7.27 % (2757778)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2964029892:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 47.20/7.27 % TRYING [2]
% 47.20/7.27 % (2757766)Instruction limit reached!
% 47.20/7.27 % (2757766)------------------------------
% 47.20/7.27 % (2757766)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.20/7.27 % (2757766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.20/7.27 % (2757766)CaDiCaL version: 2.1.3
% 47.20/7.27 % (2757766)Termination reason: Instruction limit
% 47.20/7.27 % (2757766)Termination phase: Finite model building constraint generation
% 47.20/7.27 % (2757766)Time elapsed: 0.440 s
% 47.20/7.27 % (2757766)Peak memory usage: 54 MB
% 47.20/7.27 % (2757766)Instructions burned: 716 (million)
% 47.20/7.27 % (2757780)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1113266290:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi)
% 47.20/7.27 % TRYING [1]
% 47.20/7.27 % (2757769)Instruction limit reached!
% 47.20/7.27 % (2757769)------------------------------
% 47.20/7.27 % (2757769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.20/7.27 % (2757769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.20/7.27 % (2757769)CaDiCaL version: 2.1.3
% 47.20/7.27 % (2757769)Termination reason: Instruction limit
% 47.20/7.27 % (2757769)Termination phase: Saturation
% 47.20/7.27 % (2757769)Time elapsed: 0.567 s
% 47.20/7.27 % (2757769)Peak memory usage: 40 MB
% 47.20/7.27 % (2757769)Instructions burned: 685 (million)
% 47.20/7.27 % (2757782)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=2756143780:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2989 on theBenchmark for (2989ds/692Mi)
% 47.20/7.27 % TRYING [3]
% 47.20/7.27 % (2757776)Instruction limit reached!
% 47.20/7.27 % (2757776)------------------------------
% 47.20/7.27 % (2757776)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 47.20/7.27 % (2757776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.20/7.27 % (2757776)CaDiCaL version: 2.1.3
% 47.20/7.27 % (2757776)Termination reason: Instruction limit
% 47.20/7.27 % (2757776)Termination phase: Finite model building SAT solving
% 47.20/7.27 % (2757776)Time elapsed: 0.367 s
% 47.20/7.27 % (2757776)Peak memory usage: 38 MB
% 47.20/7.27 % (2757776)Instructions burned: 867 (million)
% 47.20/7.27 % (2757784)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3038237618:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi)
% 47.20/7.27 % (2757778)Instruction limit reached!
% 47.20/7.27 % (2757778)------------------------------
% 47.20/7.27 % (2757778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.40/14.80 % (2757778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.80 % (2757778)CaDiCaL version: 2.1.3
% 100.40/14.80 % (2757778)Termination reason: Instruction limit
% 100.40/14.80 % (2757778)Termination phase: Saturation
% 100.40/14.80 % (2757778)Time elapsed: 0.351 s
% 100.40/14.80 % (2757778)Peak memory usage: 54 MB
% 100.40/14.80 % (2757778)Instructions burned: 1182 (million)
% 100.40/14.80 % (2757786)fmb+10_1_sil=64000:random_seed=3031620096:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 100.40/14.80 % TRYING [1]
% 100.40/14.80 % (2757780)Instruction limit reached!
% 100.40/14.80 % (2757780)------------------------------
% 100.40/14.80 % (2757780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.40/14.80 % (2757780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.80 % (2757780)CaDiCaL version: 2.1.3
% 100.40/14.80 % (2757780)Termination reason: Instruction limit
% 100.40/14.80 % (2757780)Termination phase: Finite model building constraint generation
% 100.40/14.80 % (2757780)Time elapsed: 0.428 s
% 100.40/14.80 % (2757780)Peak memory usage: 92 MB
% 100.40/14.80 % (2757780)Instructions burned: 891 (million)
% 100.40/14.80 % TRYING [2]
% 100.40/14.80 % (2757788)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=159609963:i=9515:nm=5_2986 on theBenchmark for (2986ds/9515Mi)
% 100.40/14.80 % (2757782)Instruction limit reached!
% 100.40/14.80 % (2757782)------------------------------
% 100.40/14.80 % (2757782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.40/14.80 % (2757782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.80 % (2757782)CaDiCaL version: 2.1.3
% 100.40/14.80 % (2757782)Termination reason: Instruction limit
% 100.40/14.80 % (2757782)Termination phase: Saturation
% 100.40/14.80 % (2757782)Time elapsed: 0.335 s
% 100.40/14.80 % (2757782)Peak memory usage: 41 MB
% 100.40/14.80 % (2757782)Instructions burned: 694 (million)
% 100.40/14.80 % (2757790)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2067342042:fmbsr=1.7:i=920_2986 on theBenchmark for (2986ds/920Mi)
% 100.40/14.80 % (2757784)Instruction limit reached!
% 100.40/14.80 % (2757784)------------------------------
% 100.40/14.80 % (2757784)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.40/14.80 % (2757784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.80 % (2757784)CaDiCaL version: 2.1.3
% 100.40/14.80 % (2757784)Termination reason: Instruction limit
% 100.40/14.80 % (2757784)Termination phase: Saturation
% 100.40/14.80 % (2757784)Time elapsed: 0.448 s
% 100.40/14.80 % (2757784)Peak memory usage: 43 MB
% 100.40/14.80 % (2757784)Instructions burned: 881 (million)
% 100.40/14.80 % TRYING [20]
% 100.40/14.80 % (2757792)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=257223948:i=5131_2984 on theBenchmark for (2984ds/5131Mi)
% 100.40/14.80 % TRYING [8]
% 100.40/14.80 % TRYING [3]
% 100.40/14.80 % (2757790)Instruction limit reached!
% 100.40/14.80 % (2757790)------------------------------
% 100.40/14.80 % (2757790)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.40/14.80 % (2757790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.80 % (2757790)CaDiCaL version: 2.1.3
% 100.40/14.80 % (2757790)Termination reason: Instruction limit
% 100.40/14.80 % (2757790)Termination phase: Finite model building constraint generation
% 100.40/14.80 % (2757790)Time elapsed: 0.364 s
% 100.40/14.80 % (2757790)Peak memory usage: 64 MB
% 100.40/14.80 % (2757790)Instructions burned: 922 (million)
% 100.40/14.80 % (2757794)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3036864683:i=1472:ins=7:fdi=8:gsp=on_2982 on theBenchmark for (2982ds/1472Mi)
% 100.40/14.80 % TRYING [4]
% 100.40/14.80 % (2757794)Instruction limit reached!
% 100.40/14.80 % (2757794)------------------------------
% 100.40/14.80 % (2757794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 100.40/14.80 % (2757794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 100.40/14.80 % (2757794)CaDiCaL version: 2.1.3
% 100.40/14.80 % (2757794)Termination reason: Instruction limit
% 100.40/14.80 % (2757794)Termination phase: Saturation
% 100.40/14.80 % (2757794)Time elapsed: 0.680 s
% 100.40/14.80 % (2757794)Peak memory usage: 35 MB
% 100.40/14.80 % (2757794)Instructions burned: 1473 (million)
% 100.40/14.80 % (2757796)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1877562679:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 100.40/14.80 % TRYING [77]
% 100.40/14.80 % TRYING [4]
% 100.40/14.80 % TRYING [5]
% 100.40/14.80 % (2757792)Instruction limit reached!
% 100.40/14.80 % (2757792)------------------------------
% 100.40/14.80 % (2757792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.28/31.63 % (2757792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.28/31.63 % (2757792)CaDiCaL version: 2.1.3
% 220.28/31.63 % (2757792)Termination reason: Instruction limit
% 220.28/31.63 % (2757792)Termination phase: Saturation
% 220.28/31.63 % (2757792)Time elapsed: 2.711 s
% 220.28/31.63 % (2757792)Peak memory usage: 39 MB
% 220.28/31.63 % (2757792)Instructions burned: 5131 (million)
% 220.28/31.63 % (2757798)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4041954576:fmbsr=2.30978:i=2174_2957 on theBenchmark for (2957ds/2174Mi)
% 220.28/31.63 % TRYING [16]
% 220.28/31.63 % (2757788)Instruction limit reached!
% 220.28/31.63 % (2757788)------------------------------
% 220.28/31.63 % (2757788)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.28/31.63 % (2757788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.28/31.63 % (2757788)CaDiCaL version: 2.1.3
% 220.28/31.63 % (2757788)Termination reason: Instruction limit
% 220.28/31.63 % (2757788)Termination phase: Finite model building constraint generation
% 220.28/31.63 % (2757788)Time elapsed: 3.302 s
% 220.28/31.63 % (2757788)Peak memory usage: 550 MB
% 220.28/31.63 % (2757788)Instructions burned: 9518 (million)
% 220.28/31.63 % (2757800)ott-2_1_sil=16000:newcnf=on:random_seed=1352829834:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2952 on theBenchmark for (2952ds/869Mi)
% 220.28/31.63 % (2757796)Instruction limit reached!
% 220.28/31.63 % (2757796)------------------------------
% 220.28/31.63 % (2757796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.28/31.63 % (2757796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.28/31.63 % (2757796)CaDiCaL version: 2.1.3
% 220.28/31.63 % (2757796)Termination reason: Instruction limit
% 220.28/31.63 % (2757796)Termination phase: Finite model building constraint generation
% 220.28/31.63 % (2757796)Time elapsed: 2.243 s
% 220.28/31.63 % (2757796)Peak memory usage: 417 MB
% 220.28/31.63 % (2757796)Instructions burned: 6326 (million)
% 220.28/31.63 % (2757802)ott+10_1_sil=32000:tgt=ground:random_seed=2816491019:i=5114:av=off_2951 on theBenchmark for (2951ds/5114Mi)
% 220.28/31.63 % (2757798)Instruction limit reached!
% 220.28/31.63 % (2757798)------------------------------
% 220.28/31.63 % (2757798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.28/31.63 % (2757798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.28/31.63 % (2757798)CaDiCaL version: 2.1.3
% 220.28/31.63 % (2757798)Termination reason: Instruction limit
% 220.28/31.63 % (2757798)Termination phase: Finite model building constraint generation
% 220.28/31.63 % (2757798)Time elapsed: 0.766 s
% 220.28/31.63 % (2757798)Peak memory usage: 121 MB
% 220.28/31.63 % (2757798)Instructions burned: 2176 (million)
% 220.28/31.63 % (2757804)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4236943397:i=54282_2949 on theBenchmark for (2949ds/54282Mi)
% 220.28/31.63 % (2757800)Instruction limit reached!
% 220.28/31.63 % (2757800)------------------------------
% 220.28/31.63 % (2757800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.28/31.63 % (2757800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.28/31.63 % (2757800)CaDiCaL version: 2.1.3
% 220.28/31.63 % (2757800)Termination reason: Instruction limit
% 220.28/31.63 % (2757800)Termination phase: Saturation
% 220.28/31.63 % (2757800)Time elapsed: 0.391 s
% 220.28/31.63 % (2757800)Peak memory usage: 36 MB
% 220.28/31.63 % (2757800)Instructions burned: 871 (million)
% 220.28/31.63 % (2757806)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1549793887:i=3512:aac=none_2948 on theBenchmark for (2948ds/3512Mi)
% 220.28/31.63 % TRYING [1]
% 220.28/31.63 % TRYING [2]
% 220.28/31.63 % TRYING [3]
% 220.28/31.63 % TRYING [6]
% 220.28/31.63 % (2757786)Instruction limit reached!
% 220.28/31.63 % (2757786)------------------------------
% 220.28/31.63 % (2757786)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.28/31.63 % (2757786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.28/31.63 % (2757786)CaDiCaL version: 2.1.3
% 220.28/31.63 % (2757786)Termination reason: Instruction limit
% 220.28/31.63 % (2757786)Termination phase: Finite model building SAT solving
% 220.28/31.63 % (2757786)Time elapsed: 5.262 s
% 220.28/31.63 % (2757786)Peak memory usage: 159 MB
% 220.28/31.63 % (2757786)Instructions burned: 22065 (million)
% 220.28/31.63 % (2757808)dis+21_1_sil=32000:sas=cadical:random_seed=2607581972:i=3773:amm=off_2935 on theBenchmark for (2935ds/3773Mi)
% 220.28/31.63 % (2757806)Instruction limit reached!
% 220.28/31.63 % (2757806)------------------------------
% 220.28/31.63 % (2757806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757806)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757806)Termination reason: Instruction limit
% 274.03/40.53 % (2757806)Termination phase: Saturation
% 274.03/40.53 % (2757806)Time elapsed: 1.767 s
% 274.03/40.53 % (2757806)Peak memory usage: 40 MB
% 274.03/40.53 % (2757806)Instructions burned: 3512 (million)
% 274.03/40.53 % (2757810)ott+11_1_sil=16000:gs=on:random_seed=1510046505:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2930 on theBenchmark for (2930ds/2251Mi)
% 274.03/40.53 % (2757808)Instruction limit reached!
% 274.03/40.53 % (2757808)------------------------------
% 274.03/40.53 % (2757808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757808)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757808)Termination reason: Instruction limit
% 274.03/40.53 % (2757808)Termination phase: Saturation
% 274.03/40.53 % (2757808)Time elapsed: 0.967 s
% 274.03/40.53 % (2757808)Peak memory usage: 65 MB
% 274.03/40.53 % (2757808)Instructions burned: 3775 (million)
% 274.03/40.53 % (2757802)Instruction limit reached!
% 274.03/40.53 % (2757802)------------------------------
% 274.03/40.53 % (2757802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757802)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757802)Termination reason: Instruction limit
% 274.03/40.53 % (2757802)Termination phase: Saturation
% 274.03/40.53 % (2757802)Time elapsed: 2.581 s
% 274.03/40.53 % (2757802)Peak memory usage: 118 MB
% 274.03/40.53 % (2757802)Instructions burned: 5114 (million)
% 274.03/40.53 % (2757812)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2396910395:fmbsr=1.6:i=67534_2925 on theBenchmark for (2925ds/67534Mi)
% 274.03/40.53 % (2757814)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2653038807:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2925 on theBenchmark for (2925ds/4591Mi)
% 274.03/40.53 % TRYING [7]
% 274.03/40.53 % TRYING [4]
% 274.03/40.53 % (2757810)Instruction limit reached!
% 274.03/40.53 % (2757810)------------------------------
% 274.03/40.53 % (2757810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757810)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757810)Termination reason: Instruction limit
% 274.03/40.53 % (2757810)Termination phase: Saturation
% 274.03/40.53 % (2757810)Time elapsed: 1.167 s
% 274.03/40.53 % (2757810)Peak memory usage: 92 MB
% 274.03/40.53 % (2757810)Instructions burned: 2252 (million)
% 274.03/40.53 % (2757816)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3106663145:i=29340_2918 on theBenchmark for (2918ds/29340Mi)
% 274.03/40.53 % (2757814)Instruction limit reached!
% 274.03/40.53 % (2757814)------------------------------
% 274.03/40.53 % (2757814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757814)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757814)Termination reason: Instruction limit
% 274.03/40.53 % (2757814)Termination phase: Saturation
% 274.03/40.53 % (2757814)Time elapsed: 2.069 s
% 274.03/40.53 % (2757814)Peak memory usage: 44 MB
% 274.03/40.53 % (2757814)Instructions burned: 4592 (million)
% 274.03/40.53 % (2757818)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2504913108:i=5211_2904 on theBenchmark for (2904ds/5211Mi)
% 274.03/40.53 % (2757818)Instruction limit reached!
% 274.03/40.53 % (2757818)------------------------------
% 274.03/40.53 % (2757818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757818)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757818)Termination reason: Instruction limit
% 274.03/40.53 % (2757818)Termination phase: Saturation
% 274.03/40.53 % (2757818)Time elapsed: 2.837 s
% 274.03/40.53 % (2757818)Peak memory usage: 57 MB
% 274.03/40.53 % (2757818)Instructions burned: 5212 (million)
% 274.03/40.53 % (2757820)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3424737277:i=5497:nm=2_2876 on theBenchmark for (2876ds/5497Mi)
% 274.03/40.53 % TRYING [17]
% 274.03/40.53 % TRYING [5]
% 274.03/40.53 % (2757820)Instruction limit reached!
% 274.03/40.53 % (2757820)------------------------------
% 274.03/40.53 % (2757820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757820)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757820)Termination reason: Instruction limit
% 274.03/40.53 % (2757820)Termination phase: Finite model building constraint generation
% 274.03/40.53 % (2757820)Time elapsed: 2.017 s
% 274.03/40.53 % (2757820)Peak memory usage: 351 MB
% 274.03/40.53 % (2757820)Instructions burned: 5500 (million)
% 274.03/40.53 % (2757822)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1640223933:fmbsr=2:i=46332_2855 on theBenchmark for (2855ds/46332Mi)
% 274.03/40.53 % TRYING [15]
% 274.03/40.53 % (2757816)Instruction limit reached!
% 274.03/40.53 % (2757816)------------------------------
% 274.03/40.53 % (2757816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757816)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757816)Termination reason: Instruction limit
% 274.03/40.53 % (2757816)Termination phase: Saturation
% 274.03/40.53 % (2757816)Time elapsed: 13.647 s
% 274.03/40.53 % (2757816)Peak memory usage: 83 MB
% 274.03/40.53 % (2757816)Instructions burned: 29340 (million)
% 274.03/40.53 % (2757824)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2484461796:i=14071_2781 on theBenchmark for (2781ds/14071Mi)
% 274.03/40.53 % TRYING [12]
% 274.03/40.53 % TRYING [5]
% 274.03/40.53 % (2757812)Instruction limit reached!
% 274.03/40.53 % (2757812)------------------------------
% 274.03/40.53 % (2757812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757812)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757812)Termination reason: Instruction limit
% 274.03/40.53 % (2757812)Termination phase: Finite model building SAT solving
% 274.03/40.53 % (2757812)Time elapsed: 17.069 s
% 274.03/40.53 % (2757812)Peak memory usage: 287 MB
% 274.03/40.53 % (2757812)Instructions burned: 67537 (million)
% 274.03/40.53 % (2757826)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3159608527:i=22565:add=on:rawr=on_2754 on theBenchmark for (2754ds/22565Mi)
% 274.03/40.53 % (2757824)Instruction limit reached!
% 274.03/40.53 % (2757824)------------------------------
% 274.03/40.53 % (2757824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757824)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757824)Termination reason: Instruction limit
% 274.03/40.53 % (2757824)Termination phase: Finite model building constraint generation
% 274.03/40.53 % (2757824)Time elapsed: 6.515 s
% 274.03/40.53 % (2757824)Peak memory usage: 1121 MB
% 274.03/40.53 % (2757824)Instructions burned: 14072 (million)
% 274.03/40.53 % (2757828)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2894879526:i=8173:av=off_2715 on theBenchmark for (2715ds/8173Mi)
% 274.03/40.53 % (2757826)Instruction limit reached!
% 274.03/40.53 % (2757826)------------------------------
% 274.03/40.53 % (2757826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757826)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757826)Termination reason: Instruction limit
% 274.03/40.53 % (2757826)Termination phase: Saturation
% 274.03/40.53 % (2757826)Time elapsed: 4.633 s
% 274.03/40.53 % (2757826)Peak memory usage: 120 MB
% 274.03/40.53 % (2757826)Instructions burned: 22570 (million)
% 274.03/40.53 % (2757830)dis+10_16:1_sil=16000:random_seed=1901439962:i=9155:fsr=off_2708 on theBenchmark for (2708ds/9155Mi)
% 274.03/40.53 % (2757754)Instruction limit reached!
% 274.03/40.53 % (2757754)------------------------------
% 274.03/40.53 % (2757754)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757754)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757754)Termination reason: Instruction limit
% 274.03/40.53 % (2757754)Termination phase: Saturation
% 274.03/40.53 % (2757754)Time elapsed: 30.279 s
% 274.03/40.53 % (2757754)Peak memory usage: 183 MB
% 274.03/40.53 % (2757754)Instructions burned: 88024 (million)
% 274.03/40.53 % (2757832)ott-3_8_sil=64000:random_seed=2023732227:i=20139:bs=on_2694 on theBenchmark for (2694ds/20139Mi)
% 274.03/40.53 % (2757830)Instruction limit reached!
% 274.03/40.53 % (2757830)------------------------------
% 274.03/40.53 % (2757830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757830)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757830)Termination reason: Instruction limit
% 274.03/40.53 % (2757830)Termination phase: Saturation
% 274.03/40.53 % (2757830)Time elapsed: 2.098 s
% 274.03/40.53 % (2757830)Peak memory usage: 81 MB
% 274.03/40.53 % (2757830)Instructions burned: 9159 (million)
% 274.03/40.53 % (2757834)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2409269660:fmbsr=2:i=32576_2687 on theBenchmark for (2687ds/32576Mi)
% 274.03/40.53 % TRYING [9]
% 274.03/40.53 % (2757804)Instruction limit reached!
% 274.03/40.53 % (2757804)------------------------------
% 274.03/40.53 % (2757804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757804)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757804)Termination reason: Instruction limit
% 274.03/40.53 % (2757804)Termination phase: Finite model building SAT solving
% 274.03/40.53 % (2757804)Time elapsed: 26.702 s
% 274.03/40.53 % (2757804)Peak memory usage: 237 MB
% 274.03/40.53 % (2757804)Instructions burned: 54283 (million)
% 274.03/40.53 % (2757836)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=1287488445:i=11404_2681 on theBenchmark for (2681ds/11404Mi)
% 274.03/40.53 % (2757828)Instruction limit reached!
% 274.03/40.53 % (2757828)------------------------------
% 274.03/40.53 % (2757828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757828)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757828)Termination reason: Instruction limit
% 274.03/40.53 % (2757828)Termination phase: Saturation
% 274.03/40.53 % (2757828)Time elapsed: 4.622 s
% 274.03/40.53 % (2757828)Peak memory usage: 200 MB
% 274.03/40.53 % (2757828)Instructions burned: 8174 (million)
% 274.03/40.53 % (2757838)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2506583089:i=14134_2668 on theBenchmark for (2668ds/14134Mi)
% 274.03/40.53 % TRYING [6]
% 274.03/40.53 % (2757822)Instruction limit reached!
% 274.03/40.53 % (2757822)------------------------------
% 274.03/40.53 % (2757822)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757822)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757822)Termination reason: Instruction limit
% 274.03/40.53 % (2757822)Termination phase: Finite model building constraint generation
% 274.03/40.53 % (2757822)Time elapsed: 22.030 s
% 274.03/40.53 % (2757822)Peak memory usage: 3367 MB
% 274.03/40.53 % (2757822)Instructions burned: 46332 (million)
% 274.03/40.53 % (2757836)Instruction limit reached!
% 274.03/40.53 % (2757836)------------------------------
% 274.03/40.53 % (2757836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.53 % (2757836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.53 % (2757836)CaDiCaL version: 2.1.3
% 274.03/40.53 % (2757836)Termination reason: Instruction limit
% 274.03/40.53 % (2757836)Termination phase: Saturation
% 274.03/40.53 % (2757836)Time elapsed: 4.932 s
% 274.03/40.53 % (2757836)Peak memory usage: 146 MB
% 274.03/40.53 % (2757836)Instructions burned: 11406 (million)
% 274.03/40.53 % (2757842)dis+33_16_sil=32000:sac=on:random_seed=2930036627:i=15851:nm=0_2631 on theBenchmark for (2631ds/15851Mi)
% 274.03/40.53 % (2757844)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2613212010:avsq=on:i=17627:add=on:amm=off_2630 on theBenchmark for (2630ds/17627Mi)
% 274.03/40.53 % (2757842) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2757747-2757842"...
% 274.03/40.53 % (2757842)...printing done.
% 274.03/40.53 % (2757842)Refutation found. Thanks to Tanya!
% 274.03/40.53 % SZS status Theorem for theBenchmark
% 274.03/40.53 % SZS output start Proof for theBenchmark
% See solution above
% 274.03/40.55 % (2757842)------------------------------
% 274.03/40.55 % (2757842)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 274.03/40.55 % (2757842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 274.03/40.55 % (2757842)CaDiCaL version: 2.1.3
% 274.03/40.55 % (2757842)Termination reason: Refutation
% 274.03/40.55 % (2757842)Time elapsed: 3.174 s
% 274.03/40.55 % (2757842)Peak memory usage: 80 MB
% 274.03/40.55 % (2757842)Instructions burned: 6718 (million)
% 274.03/40.55 % (2757747)Success in time 40.17 s
% 274.03/40.55 % Vampire exiting
%------------------------------------------------------------------------------