%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR116+24 : 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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:45:50 AM UTC 2026
% Result : Theorem 183.28s 39.15s
% Output : Refutation 183.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 13
% Syntax : Number of formulae : 114 ( 22 unt; 5 def)
% Number of atoms : 1102 ( 0 equ)
% Maximal formula atoms : 133 ( 9 avg)
% Number of connectives : 1300 ( 312 ~; 270 |; 708 &)
% ( 5 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 133 ( 13 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 34 ( 33 usr; 6 prp; 0-2 aty)
% Number of functors : 57 ( 57 usr; 48 con; 0-3 aty)
% Number of variables : 260 ( 0 sgn 217 !; 43 ?)
% Comments :
%------------------------------------------------------------------------------
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(f162,axiom,
! [X0,X1,X2] :
( ( arg1(X0,X1)
& arg2(X0,X2)
& subr(X0,sub_0) )
=> ? [X3,X4,X5] :
( arg1(X4,X1)
& arg2(X4,X5)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& sub(X5,X2)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',sub__bezeichnen_1_1_als) ).
fof(f163,axiom,
! [X0,X1] :
( sub(X0,X1)
=> ? [X2] :
( arg1(X2,X0)
& arg2(X2,X1)
& subr(X2,sub_0) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',sub__sub_0_expansion) ).
fof(f9161,axiom,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',fact_8980) ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( in(X5,X6)
& arg1(X3,X0)
& arg2(X3,X4)
& attr(X0,X1)
& attr(X0,X2)
& attr(X6,X7)
& obj(X8,X0)
& sub(X1,familiename_1_1)
& sub(X2,eigenname_1_1)
& sub(X4,X9)
& sub(X7,name_1_1)
& subr(X3,rprs_0)
& val(X1,mandela_0)
& val(X2,nelson_0)
& val(X7,s__374dafrika_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_010_mira_news_1788) ).
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,
( origl(c15,c323)
& sub(c15,an_f__374hrer_1_1)
& sub(c15,c15)
& sub(c15,hirte_1_1)
& arg1(c19,c15)
& arg2(c19,c15)
& subr(c19,sub_0)
& pred(c307,autobiographie_1_1)
& attch(c316,c307)
& attr(c316,c317)
& attr(c316,c318)
& prop(c316,s__374dafrikanisch_1_1)
& sub(c316,pr__344sident_1_1)
& sub(c317,eigenname_1_1)
& val(c317,nelson_0)
& sub(c318,familiename_1_1)
& val(c318,mandela_0)
& flp(c323,c307)
& agt(c324,c15)
& subs(c324,f__374hren_1_1)
& sort(c15,d)
& card(c15,int1)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& quant(c15,one)
& refer(c15,indet)
& varia(c15,varia_c)
& sort(c323,l)
& card(c323,cons(x_constant,cons(int1,nil)))
& etype(c323,int1)
& fact(c323,real)
& gener(c323,sp)
& quant(c323,mult)
& refer(c323,det)
& varia(c323,con)
& sort(an_f__374hrer_1_1,d)
& card(an_f__374hrer_1_1,int1)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& quant(an_f__374hrer_1_1,one)
& refer(an_f__374hrer_1_1,refer_c)
& varia(an_f__374hrer_1_1,varia_c)
& sort(hirte_1_1,d)
& card(hirte_1_1,int1)
& etype(hirte_1_1,int0)
& fact(hirte_1_1,real)
& gener(hirte_1_1,ge)
& quant(hirte_1_1,one)
& refer(hirte_1_1,refer_c)
& varia(hirte_1_1,varia_c)
& sort(c19,st)
& fact(c19,real)
& gener(c19,sp)
& sort(sub_0,st)
& fact(sub_0,real)
& gener(sub_0,gener_c)
& sort(c307,d)
& sort(c307,io)
& card(c307,cons(x_constant,cons(int1,nil)))
& etype(c307,int1)
& fact(c307,real)
& gener(c307,sp)
& quant(c307,mult)
& refer(c307,det)
& varia(c307,con)
& sort(autobiographie_1_1,d)
& sort(autobiographie_1_1,io)
& card(autobiographie_1_1,int1)
& etype(autobiographie_1_1,int0)
& fact(autobiographie_1_1,real)
& gener(autobiographie_1_1,ge)
& quant(autobiographie_1_1,one)
& refer(autobiographie_1_1,refer_c)
& varia(autobiographie_1_1,varia_c)
& sort(c316,d)
& card(c316,int1)
& etype(c316,int0)
& fact(c316,real)
& gener(c316,sp)
& quant(c316,one)
& refer(c316,det)
& varia(c316,con)
& sort(c317,na)
& card(c317,int1)
& etype(c317,int0)
& fact(c317,real)
& gener(c317,sp)
& quant(c317,one)
& refer(c317,indet)
& varia(c317,varia_c)
& sort(c318,na)
& card(c318,int1)
& etype(c318,int0)
& fact(c318,real)
& gener(c318,sp)
& quant(c318,one)
& refer(c318,indet)
& varia(c318,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(c324,da)
& fact(c324,real)
& gener(c324,sp)
& sort(f__374hren_1_1,da)
& fact(f__374hren_1_1,real)
& gener(f__374hren_1_1,ge) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_news_1788) ).
fof(f10326,plain,
( origl(c15,c323)
& sub(c15,an_f__374hrer_1_1)
& sub(c15,c15)
& sub(c15,hirte_1_1)
& arg1(c19,c15)
& arg2(c19,c15)
& subr(c19,sub_0)
& pred(c307,autobiographie_1_1)
& attch(c316,c307)
& attr(c316,c317)
& attr(c316,c318)
& prop(c316,s__374dafrikanisch_1_1)
& sub(c316,pr__344sident_1_1)
& sub(c317,eigenname_1_1)
& val(c317,nelson_0)
& sub(c318,familiename_1_1)
& val(c318,mandela_0)
& flp(c323,c307)
& agt(c324,c15)
& subs(c324,f__374hren_1_1)
& card(c15,int1)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& quant(c15,one)
& refer(c15,indet)
& varia(c15,varia_c)
& card(c323,cons(x_constant,cons(int1,nil)))
& etype(c323,int1)
& fact(c323,real)
& gener(c323,sp)
& quant(c323,mult)
& refer(c323,det)
& varia(c323,con)
& card(an_f__374hrer_1_1,int1)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& quant(an_f__374hrer_1_1,one)
& refer(an_f__374hrer_1_1,refer_c)
& varia(an_f__374hrer_1_1,varia_c)
& card(hirte_1_1,int1)
& etype(hirte_1_1,int0)
& fact(hirte_1_1,real)
& gener(hirte_1_1,ge)
& quant(hirte_1_1,one)
& refer(hirte_1_1,refer_c)
& varia(hirte_1_1,varia_c)
& fact(c19,real)
& gener(c19,sp)
& fact(sub_0,real)
& gener(sub_0,gener_c)
& card(c307,cons(x_constant,cons(int1,nil)))
& etype(c307,int1)
& fact(c307,real)
& gener(c307,sp)
& quant(c307,mult)
& refer(c307,det)
& varia(c307,con)
& card(autobiographie_1_1,int1)
& etype(autobiographie_1_1,int0)
& fact(autobiographie_1_1,real)
& gener(autobiographie_1_1,ge)
& quant(autobiographie_1_1,one)
& refer(autobiographie_1_1,refer_c)
& varia(autobiographie_1_1,varia_c)
& card(c316,int1)
& etype(c316,int0)
& fact(c316,real)
& gener(c316,sp)
& quant(c316,one)
& refer(c316,det)
& varia(c316,con)
& card(c317,int1)
& etype(c317,int0)
& fact(c317,real)
& gener(c317,sp)
& quant(c317,one)
& refer(c317,indet)
& varia(c317,varia_c)
& card(c318,int1)
& etype(c318,int0)
& fact(c318,real)
& gener(c318,sp)
& quant(c318,one)
& refer(c318,indet)
& varia(c318,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)
& fact(c324,real)
& gener(c324,sp)
& fact(f__374hren_1_1,real)
& gener(f__374hren_1_1,ge) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10329,plain,
( origl(c15,c323)
& sub(c15,an_f__374hrer_1_1)
& sub(c15,c15)
& sub(c15,hirte_1_1)
& arg1(c19,c15)
& arg2(c19,c15)
& subr(c19,sub_0)
& pred(c307,autobiographie_1_1)
& attch(c316,c307)
& attr(c316,c317)
& attr(c316,c318)
& prop(c316,s__374dafrikanisch_1_1)
& sub(c316,pr__344sident_1_1)
& sub(c317,eigenname_1_1)
& val(c317,nelson_0)
& sub(c318,familiename_1_1)
& val(c318,mandela_0)
& flp(c323,c307)
& agt(c324,c15)
& subs(c324,f__374hren_1_1)
& card(c15,int1)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& refer(c15,indet)
& varia(c15,varia_c)
& card(c323,cons(x_constant,cons(int1,nil)))
& etype(c323,int1)
& fact(c323,real)
& gener(c323,sp)
& refer(c323,det)
& varia(c323,con)
& card(an_f__374hrer_1_1,int1)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& refer(an_f__374hrer_1_1,refer_c)
& varia(an_f__374hrer_1_1,varia_c)
& card(hirte_1_1,int1)
& etype(hirte_1_1,int0)
& fact(hirte_1_1,real)
& gener(hirte_1_1,ge)
& refer(hirte_1_1,refer_c)
& varia(hirte_1_1,varia_c)
& fact(c19,real)
& gener(c19,sp)
& fact(sub_0,real)
& gener(sub_0,gener_c)
& card(c307,cons(x_constant,cons(int1,nil)))
& etype(c307,int1)
& fact(c307,real)
& gener(c307,sp)
& refer(c307,det)
& varia(c307,con)
& card(autobiographie_1_1,int1)
& etype(autobiographie_1_1,int0)
& fact(autobiographie_1_1,real)
& gener(autobiographie_1_1,ge)
& refer(autobiographie_1_1,refer_c)
& varia(autobiographie_1_1,varia_c)
& card(c316,int1)
& etype(c316,int0)
& fact(c316,real)
& gener(c316,sp)
& refer(c316,det)
& varia(c316,con)
& card(c317,int1)
& etype(c317,int0)
& fact(c317,real)
& gener(c317,sp)
& refer(c317,indet)
& varia(c317,varia_c)
& card(c318,int1)
& etype(c318,int0)
& fact(c318,real)
& gener(c318,sp)
& refer(c318,indet)
& varia(c318,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)
& fact(c324,real)
& gener(c324,sp)
& fact(f__374hren_1_1,real)
& gener(f__374hren_1_1,ge) ),
inference(pure_predicate_removal,[],[f10326]) ).
fof(f10332,plain,
( origl(c15,c323)
& sub(c15,an_f__374hrer_1_1)
& sub(c15,c15)
& sub(c15,hirte_1_1)
& arg1(c19,c15)
& arg2(c19,c15)
& subr(c19,sub_0)
& pred(c307,autobiographie_1_1)
& attch(c316,c307)
& attr(c316,c317)
& attr(c316,c318)
& prop(c316,s__374dafrikanisch_1_1)
& sub(c316,pr__344sident_1_1)
& sub(c317,eigenname_1_1)
& val(c317,nelson_0)
& sub(c318,familiename_1_1)
& val(c318,mandela_0)
& flp(c323,c307)
& agt(c324,c15)
& subs(c324,f__374hren_1_1)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& refer(c15,indet)
& varia(c15,varia_c)
& etype(c323,int1)
& fact(c323,real)
& gener(c323,sp)
& refer(c323,det)
& varia(c323,con)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& refer(an_f__374hrer_1_1,refer_c)
& varia(an_f__374hrer_1_1,varia_c)
& etype(hirte_1_1,int0)
& fact(hirte_1_1,real)
& gener(hirte_1_1,ge)
& refer(hirte_1_1,refer_c)
& varia(hirte_1_1,varia_c)
& fact(c19,real)
& gener(c19,sp)
& fact(sub_0,real)
& gener(sub_0,gener_c)
& etype(c307,int1)
& fact(c307,real)
& gener(c307,sp)
& refer(c307,det)
& varia(c307,con)
& etype(autobiographie_1_1,int0)
& fact(autobiographie_1_1,real)
& gener(autobiographie_1_1,ge)
& refer(autobiographie_1_1,refer_c)
& varia(autobiographie_1_1,varia_c)
& etype(c316,int0)
& fact(c316,real)
& gener(c316,sp)
& refer(c316,det)
& varia(c316,con)
& etype(c317,int0)
& fact(c317,real)
& gener(c317,sp)
& refer(c317,indet)
& varia(c317,varia_c)
& etype(c318,int0)
& fact(c318,real)
& gener(c318,sp)
& refer(c318,indet)
& varia(c318,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)
& fact(c324,real)
& gener(c324,sp)
& fact(f__374hren_1_1,real)
& gener(f__374hren_1_1,ge) ),
inference(pure_predicate_removal,[],[f10329]) ).
fof(f10335,plain,
( origl(c15,c323)
& sub(c15,an_f__374hrer_1_1)
& sub(c15,c15)
& sub(c15,hirte_1_1)
& arg1(c19,c15)
& arg2(c19,c15)
& subr(c19,sub_0)
& pred(c307,autobiographie_1_1)
& attch(c316,c307)
& attr(c316,c317)
& attr(c316,c318)
& prop(c316,s__374dafrikanisch_1_1)
& sub(c316,pr__344sident_1_1)
& sub(c317,eigenname_1_1)
& val(c317,nelson_0)
& sub(c318,familiename_1_1)
& val(c318,mandela_0)
& flp(c323,c307)
& agt(c324,c15)
& subs(c324,f__374hren_1_1)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& varia(c15,varia_c)
& etype(c323,int1)
& fact(c323,real)
& gener(c323,sp)
& varia(c323,con)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& varia(an_f__374hrer_1_1,varia_c)
& etype(hirte_1_1,int0)
& fact(hirte_1_1,real)
& gener(hirte_1_1,ge)
& varia(hirte_1_1,varia_c)
& fact(c19,real)
& gener(c19,sp)
& fact(sub_0,real)
& gener(sub_0,gener_c)
& etype(c307,int1)
& fact(c307,real)
& gener(c307,sp)
& varia(c307,con)
& etype(autobiographie_1_1,int0)
& fact(autobiographie_1_1,real)
& gener(autobiographie_1_1,ge)
& varia(autobiographie_1_1,varia_c)
& etype(c316,int0)
& fact(c316,real)
& gener(c316,sp)
& varia(c316,con)
& etype(c317,int0)
& fact(c317,real)
& gener(c317,sp)
& varia(c317,varia_c)
& etype(c318,int0)
& fact(c318,real)
& gener(c318,sp)
& varia(c318,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)
& fact(c324,real)
& gener(c324,sp)
& fact(f__374hren_1_1,real)
& gener(f__374hren_1_1,ge) ),
inference(pure_predicate_removal,[],[f10332]) ).
fof(f10340,plain,
( origl(c15,c323)
& sub(c15,an_f__374hrer_1_1)
& sub(c15,c15)
& sub(c15,hirte_1_1)
& arg1(c19,c15)
& arg2(c19,c15)
& subr(c19,sub_0)
& pred(c307,autobiographie_1_1)
& attch(c316,c307)
& attr(c316,c317)
& attr(c316,c318)
& prop(c316,s__374dafrikanisch_1_1)
& sub(c316,pr__344sident_1_1)
& sub(c317,eigenname_1_1)
& val(c317,nelson_0)
& sub(c318,familiename_1_1)
& val(c318,mandela_0)
& flp(c323,c307)
& agt(c324,c15)
& subs(c324,f__374hren_1_1)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& etype(c323,int1)
& fact(c323,real)
& gener(c323,sp)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& gener(an_f__374hrer_1_1,ge)
& etype(hirte_1_1,int0)
& fact(hirte_1_1,real)
& gener(hirte_1_1,ge)
& fact(c19,real)
& gener(c19,sp)
& fact(sub_0,real)
& gener(sub_0,gener_c)
& etype(c307,int1)
& fact(c307,real)
& gener(c307,sp)
& etype(autobiographie_1_1,int0)
& fact(autobiographie_1_1,real)
& gener(autobiographie_1_1,ge)
& etype(c316,int0)
& fact(c316,real)
& gener(c316,sp)
& etype(c317,int0)
& fact(c317,real)
& gener(c317,sp)
& etype(c318,int0)
& fact(c318,real)
& gener(c318,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)
& fact(c324,real)
& gener(c324,sp)
& fact(f__374hren_1_1,real)
& gener(f__374hren_1_1,ge) ),
inference(pure_predicate_removal,[],[f10335]) ).
fof(f10345,plain,
( origl(c15,c323)
& sub(c15,an_f__374hrer_1_1)
& sub(c15,c15)
& sub(c15,hirte_1_1)
& arg1(c19,c15)
& arg2(c19,c15)
& subr(c19,sub_0)
& pred(c307,autobiographie_1_1)
& attch(c316,c307)
& attr(c316,c317)
& attr(c316,c318)
& prop(c316,s__374dafrikanisch_1_1)
& sub(c316,pr__344sident_1_1)
& sub(c317,eigenname_1_1)
& val(c317,nelson_0)
& sub(c318,familiename_1_1)
& val(c318,mandela_0)
& flp(c323,c307)
& agt(c324,c15)
& subs(c324,f__374hren_1_1)
& etype(c15,int0)
& fact(c15,real)
& etype(c323,int1)
& fact(c323,real)
& etype(an_f__374hrer_1_1,int0)
& fact(an_f__374hrer_1_1,real)
& etype(hirte_1_1,int0)
& fact(hirte_1_1,real)
& fact(c19,real)
& fact(sub_0,real)
& etype(c307,int1)
& fact(c307,real)
& etype(autobiographie_1_1,int0)
& fact(autobiographie_1_1,real)
& etype(c316,int0)
& fact(c316,real)
& etype(c317,int0)
& fact(c317,real)
& etype(c318,int0)
& fact(c318,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)
& fact(c324,real)
& fact(f__374hren_1_1,real) ),
inference(pure_predicate_removal,[],[f10340]) ).
fof(f10349,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f10398,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(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(flattening,[],[f10398]) ).
fof(f10507,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(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(flattening,[],[f10507]) ).
fof(f10519,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( arg1(X4,X1)
& arg2(X4,X5)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& sub(X5,X2)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(ennf_transformation,[],[f162]) ).
fof(f10520,plain,
! [X0,X1,X2] :
( ? [X3,X4,X5] :
( arg1(X4,X1)
& arg2(X4,X5)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& sub(X5,X2)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(flattening,[],[f10519]) ).
fof(f10521,plain,
! [X0,X1] :
( ? [X2] :
( arg1(X2,X0)
& arg2(X2,X1)
& subr(X2,sub_0) )
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f163]) ).
fof(f10550,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8,X9] :
( ~ in(X5,X6)
| ~ arg1(X3,X0)
| ~ arg2(X3,X4)
| ~ attr(X0,X1)
| ~ attr(X0,X2)
| ~ attr(X6,X7)
| ~ obj(X8,X0)
| ~ sub(X1,familiename_1_1)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X4,X9)
| ~ sub(X7,name_1_1)
| ~ subr(X3,rprs_0)
| ~ val(X1,mandela_0)
| ~ val(X2,nelson_0)
| ~ val(X7,s__374dafrika_0) ),
inference(ennf_transformation,[],[f10189]) ).
fof(f10555,plain,
! [X0,X1] :
( ( loc(sK3(X0,X1),X0)
& obj(sK3(X0,X1),X1)
& subs(sK3(X0,X1),geben_1_1) )
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X2,sK3(X0,X1))],[f10399]) ).
fof(f10590,plain,
! [X0,X1,X2] :
( ( in(sK50(X0,X2),sK48(X0,X2))
& attr(sK48(X0,X2),sK49(X0,X2))
& loc(X0,sK50(X0,X2))
& sub(sK48(X0,X2),land_1_1)
& sub(sK49(X0,X2),name_1_1)
& val(sK49(X0,X2),X2) )
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48,sK49,sK50]),skolemize(X3,sK48(X0,X2)),skolemize(X4,sK49(X0,X2)),skolemize(X5,sK50(X0,X2))],[f10508]) ).
fof(f10594,plain,
! [X0,X1,X2] :
( ( arg1(sK56(X0,X1,X2),X1)
& arg2(sK56(X0,X1,X2),sK57(X0,X1,X2))
& hsit(X0,sK55(X0,X1,X2))
& mcont(sK55(X0,X1,X2),sK56(X0,X1,X2))
& obj(sK55(X0,X1,X2),X1)
& sub(sK57(X0,X1,X2),X2)
& subr(sK56(X0,X1,X2),rprs_0)
& subs(sK55(X0,X1,X2),bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55,sK56,sK57]),skolemize(X3,sK55(X0,X1,X2)),skolemize(X4,sK56(X0,X1,X2)),skolemize(X5,sK57(X0,X1,X2))],[f10520]) ).
fof(f10595,plain,
! [X0,X1] :
( ( arg1(sK58(X0,X1),X0)
& arg2(sK58(X0,X1),X1)
& subr(sK58(X0,X1),sub_0) )
| ~ sub(X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58]),skolemize(X2,sK58(X0,X1))],[f10521]) ).
fof(f10605,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(cnf_transformation,[],[f10349]) ).
fof(f10689,plain,
! [X0,X1] :
( obj(sK3(X0,X1),X1)
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(cnf_transformation,[],[f10555]) ).
fof(f10855,plain,
! [X2,X0,X1] :
( val(sK49(X0,X2),X2)
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10590]) ).
fof(f10856,plain,
! [X2,X0,X1] :
( sub(sK49(X0,X2),name_1_1)
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10590]) ).
fof(f10858,plain,
! [X2,X0,X1] :
( loc(X0,sK50(X0,X2))
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10590]) ).
fof(f10859,plain,
! [X2,X0,X1] :
( attr(sK48(X0,X2),sK49(X0,X2))
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10590]) ).
fof(f10860,plain,
! [X2,X0,X1] :
( in(sK50(X0,X2),sK48(X0,X2))
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10590]) ).
fof(f10878,plain,
! [X2,X0,X1] :
( subr(sK56(X0,X1,X2),rprs_0)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10594]) ).
fof(f10879,plain,
! [X2,X0,X1] :
( sub(sK57(X0,X1,X2),X2)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10594]) ).
fof(f10883,plain,
! [X2,X0,X1] :
( arg2(sK56(X0,X1,X2),sK57(X0,X1,X2))
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10594]) ).
fof(f10884,plain,
! [X2,X0,X1] :
( arg1(sK56(X0,X1,X2),X1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10594]) ).
fof(f10885,plain,
! [X0,X1] :
( subr(sK58(X0,X1),sub_0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10595]) ).
fof(f10886,plain,
! [X0,X1] :
( arg2(sK58(X0,X1),X1)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10595]) ).
fof(f10887,plain,
! [X0,X1] :
( arg1(sK58(X0,X1),X0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10595]) ).
fof(f19787,plain,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
inference(cnf_transformation,[],[f9161]) ).
fof(f20814,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,[],[f10550]) ).
fof(f20827,plain,
fact(c316,real),
inference(cnf_transformation,[],[f10345]) ).
fof(f20846,plain,
val(c318,mandela_0),
inference(cnf_transformation,[],[f10345]) ).
fof(f20847,plain,
sub(c318,familiename_1_1),
inference(cnf_transformation,[],[f10345]) ).
fof(f20848,plain,
val(c317,nelson_0),
inference(cnf_transformation,[],[f10345]) ).
fof(f20849,plain,
sub(c317,eigenname_1_1),
inference(cnf_transformation,[],[f10345]) ).
fof(f20850,plain,
sub(c316,pr__344sident_1_1),
inference(cnf_transformation,[],[f10345]) ).
fof(f20851,plain,
prop(c316,s__374dafrikanisch_1_1),
inference(cnf_transformation,[],[f10345]) ).
fof(f20852,plain,
attr(c316,c318),
inference(cnf_transformation,[],[f10345]) ).
fof(f20853,plain,
attr(c316,c317),
inference(cnf_transformation,[],[f10345]) ).
fof(f20864,definition,
( spl64_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,[spl64_1])],[avatar_definition]) ).
fof(f20865,plain,
( ! [X2,X3,X0,X1,X8,X9,X4] :
( ~ arg1(X3,X0)
| ~ val(X2,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(X3,rprs_0)
| ~ sub(X4,X9)
| ~ obj(X8,X0)
| ~ attr(X0,X2)
| ~ attr(X0,X1)
| ~ arg2(X3,X4)
| ~ sub(X2,eigenname_1_1)
| ~ sub(X1,familiename_1_1) )
| ~ spl64_1 ),
inference(avatar_component_clause,[],[f20864]) ).
fof(f20867,definition,
( spl64_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,[spl64_2])],[avatar_definition]) ).
fof(f20868,plain,
( ! [X6,X7,X5] :
( ~ in(X5,X6)
| ~ val(X7,s__374dafrika_0)
| ~ attr(X6,X7)
| ~ sub(X7,name_1_1) )
| ~ spl64_2 ),
inference(avatar_component_clause,[],[f20867]) ).
fof(f20869,plain,
( spl64_1
| spl64_2 ),
inference(avatar_split_clause,[],[f20814,f20867,f20864]) ).
fof(f21434,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ arg1(X0,X1)
| ~ val(X2,nelson_0)
| ~ subr(X0,rprs_0)
| ~ sub(X3,X4)
| ~ obj(X5,X1)
| ~ attr(X1,X2)
| ~ attr(X1,c318)
| ~ arg2(X0,X3)
| ~ sub(X2,eigenname_1_1)
| ~ sub(c318,familiename_1_1) )
| ~ spl64_1 ),
inference(resolution,[],[f20865,f20846]) ).
fof(f21461,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ arg1(X0,X1)
| ~ val(X2,nelson_0)
| ~ subr(X0,rprs_0)
| ~ sub(X3,X4)
| ~ obj(X5,X1)
| ~ attr(X1,X2)
| ~ attr(X1,c318)
| ~ arg2(X0,X3)
| ~ sub(X2,eigenname_1_1) )
| ~ spl64_1 ),
inference(forward_subsumption_resolution,[],[f21434,f20847]) ).
fof(f22012,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ arg1(X0,X1)
| ~ subr(X0,rprs_0)
| ~ sub(X2,X3)
| ~ obj(X4,X1)
| ~ attr(X1,c317)
| ~ attr(X1,c318)
| ~ arg2(X0,X2)
| ~ sub(c317,eigenname_1_1) )
| ~ spl64_1 ),
inference(resolution,[],[f21461,f20848]) ).
fof(f22040,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ arg1(X0,X1)
| ~ subr(X0,rprs_0)
| ~ sub(X2,X3)
| ~ obj(X4,X1)
| ~ attr(X1,c318)
| ~ arg2(X0,X2)
| ~ attr(X1,c317) )
| ~ spl64_1 ),
inference(forward_subsumption_resolution,[],[f22012,f20849]) ).
fof(f22053,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ arg1(X2,X1)
| ~ subr(X2,rprs_0)
| ~ sub(X3,X4)
| ~ arg2(X2,X3)
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0)
| ~ attr(X1,c318)
| ~ attr(X1,c317) )
| ~ spl64_1 ),
inference(resolution,[],[f22040,f10689]) ).
fof(f24214,plain,
( ! [X2,X3,X0,X1] :
( ~ in(X1,X2)
| ~ attr(X2,sK49(X0,s__374dafrika_0))
| ~ sub(sK49(X0,s__374dafrika_0),name_1_1)
| ~ prop(X0,X3)
| ~ state_adjective_state_binding(X3,s__374dafrika_0) )
| ~ spl64_2 ),
inference(resolution,[],[f20868,f10855]) ).
fof(f24225,plain,
( ! [X2,X3,X0,X1] :
( ~ in(X1,X2)
| ~ attr(X2,sK49(X0,s__374dafrika_0))
| ~ prop(X0,X3)
| ~ state_adjective_state_binding(X3,s__374dafrika_0) )
| ~ spl64_2 ),
inference(forward_subsumption_resolution,[],[f24214,f10856]) ).
fof(f24285,plain,
( ! [X2,X3,X0,X1] :
( ~ in(X1,sK48(X0,s__374dafrika_0))
| ~ prop(X0,X2)
| ~ prop(X0,X3)
| ~ state_adjective_state_binding(X2,s__374dafrika_0)
| ~ state_adjective_state_binding(X3,s__374dafrika_0) )
| ~ spl64_2 ),
inference(resolution,[],[f24225,f10859]) ).
fof(f24501,definition,
( spl64_28
<=> ! [X0] : ~ loc(c316,X0) ),
introduced(definition,[new_symbols(definition,[spl64_28])],[avatar_definition]) ).
fof(f24502,plain,
( ! [X0] : ~ loc(c316,X0)
| ~ spl64_28 ),
inference(avatar_component_clause,[],[f24501]) ).
fof(f24736,plain,
( ! [X2,X0,X1] :
( ~ in(X2,sK48(X0,s__374dafrika_0))
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ state_adjective_state_binding(X1,s__374dafrika_0) )
| ~ spl64_2 ),
inference(factoring,[],[f24285]) ).
fof(f24737,plain,
( ! [X2,X0,X1] :
( ~ in(X2,sK48(X0,s__374dafrika_0))
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,s__374dafrika_0) )
| ~ spl64_2 ),
inference(duplicate_literal_removal,[],[f24736]) ).
fof(f24740,plain,
( ! [X2,X0,X1] :
( ~ prop(X0,X1)
| ~ prop(X0,X2)
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ state_adjective_state_binding(X2,s__374dafrika_0) )
| ~ spl64_2 ),
inference(resolution,[],[f24737,f10860]) ).
fof(f24827,plain,
( ! [X0,X1] :
( ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,s__374dafrika_0)
| ~ state_adjective_state_binding(X1,s__374dafrika_0) )
| ~ spl64_2 ),
inference(factoring,[],[f24740]) ).
fof(f24828,plain,
( ! [X0,X1] :
( ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,s__374dafrika_0) )
| ~ spl64_2 ),
inference(duplicate_literal_removal,[],[f24827]) ).
fof(f24835,plain,
( ~ state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0)
| ~ spl64_2 ),
inference(resolution,[],[f24828,f20851]) ).
fof(f24845,plain,
( $false
| ~ spl64_2 ),
inference(forward_subsumption_resolution,[],[f24835,f19787]) ).
fof(f24846,plain,
~ spl64_2,
inference(avatar_contradiction_clause,[],[f24845]) ).
fof(f32965,definition,
( spl64_33
<=> has_fact_leq(c316,real) ),
introduced(definition,[new_symbols(definition,[spl64_33])],[avatar_definition]) ).
fof(f32966,plain,
( has_fact_leq(c316,real)
| ~ spl64_33 ),
inference(avatar_component_clause,[],[f32965]) ).
fof(f32967,plain,
( ~ has_fact_leq(c316,real)
| spl64_33 ),
inference(avatar_component_clause,[],[f32965]) ).
fof(f33017,plain,
( ! [X0,X1] :
( ~ prop(c316,X0)
| ~ state_adjective_state_binding(X0,X1) )
| ~ spl64_28 ),
inference(resolution,[],[f24502,f10858]) ).
fof(f33449,plain,
( ! [X0] : ~ state_adjective_state_binding(s__374dafrikanisch_1_1,X0)
| ~ spl64_28 ),
inference(resolution,[],[f33017,f20851]) ).
fof(f33496,plain,
( $false
| ~ spl64_28 ),
inference(resolution,[],[f33449,f19787]) ).
fof(f33497,plain,
~ spl64_28,
inference(avatar_contradiction_clause,[],[f33496]) ).
fof(f33733,plain,
( ~ fact(c316,real)
| spl64_33 ),
inference(resolution,[],[f32967,f10605]) ).
fof(f33734,plain,
( $false
| spl64_33 ),
inference(forward_subsumption_resolution,[],[f33733,f20827]) ).
fof(f33735,plain,
spl64_33,
inference(avatar_contradiction_clause,[],[f33734]) ).
fof(f33789,plain,
( ! [X2,X3,X0,X1] :
( ~ arg1(X0,c316)
| ~ subr(X0,rprs_0)
| ~ sub(X1,X2)
| ~ arg2(X0,X1)
| ~ loc(c316,X3)
| ~ attr(c316,c318)
| ~ attr(c316,c317) )
| ~ spl64_1
| ~ spl64_33 ),
inference(resolution,[],[f32966,f22053]) ).
fof(f33791,plain,
( ! [X2,X3,X0,X1] :
( ~ arg1(X0,c316)
| ~ subr(X0,rprs_0)
| ~ sub(X1,X2)
| ~ arg2(X0,X1)
| ~ loc(c316,X3)
| ~ attr(c316,c317) )
| ~ spl64_1
| ~ spl64_33 ),
inference(forward_subsumption_resolution,[],[f33789,f20852]) ).
fof(f33794,plain,
( ! [X2,X3,X0,X1] :
( ~ arg1(X0,c316)
| ~ subr(X0,rprs_0)
| ~ sub(X1,X2)
| ~ arg2(X0,X1)
| ~ loc(c316,X3) )
| ~ spl64_1
| ~ spl64_33 ),
inference(forward_subsumption_resolution,[],[f33791,f20853]) ).
fof(f34322,definition,
( spl64_39
<=> ! [X2,X0,X1] :
( ~ arg1(X0,c316)
| ~ arg2(X0,X1)
| ~ sub(X1,X2)
| ~ subr(X0,rprs_0) ) ),
introduced(definition,[new_symbols(definition,[spl64_39])],[avatar_definition]) ).
fof(f34323,plain,
( ! [X2,X0,X1] :
( ~ arg2(X0,X1)
| ~ sub(X1,X2)
| ~ subr(X0,rprs_0)
| ~ arg1(X0,c316) )
| ~ spl64_39 ),
inference(avatar_component_clause,[],[f34322]) ).
fof(f34324,plain,
( spl64_28
| spl64_39
| ~ spl64_1
| ~ spl64_33 ),
inference(avatar_split_clause,[],[f33794,f32965,f20864,f34322,f24501]) ).
fof(f34380,plain,
( ! [X2,X3,X0,X1] :
( ~ arg2(X3,sK57(X0,X1,X2))
| ~ subr(X3,rprs_0)
| ~ arg1(X3,c316)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl64_39 ),
inference(resolution,[],[f34323,f10879]) ).
fof(f38150,plain,
( ! [X2,X0,X1] :
( ~ subr(sK56(X0,X1,X2),rprs_0)
| ~ arg1(sK56(X0,X1,X2),c316)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl64_39 ),
inference(resolution,[],[f34380,f10883]) ).
fof(f38152,plain,
( ! [X2,X0,X1] :
( ~ subr(sK56(X0,X1,X2),rprs_0)
| ~ arg1(sK56(X0,X1,X2),c316)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl64_39 ),
inference(duplicate_literal_removal,[],[f38150]) ).
fof(f38153,plain,
( ! [X2,X0,X1] :
( ~ arg1(sK56(X0,X1,X2),c316)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl64_39 ),
inference(forward_subsumption_resolution,[],[f38152,f10878]) ).
fof(f38228,plain,
( ! [X0,X1] :
( ~ arg1(X0,c316)
| ~ arg2(X0,X1)
| ~ subr(X0,sub_0)
| ~ arg1(X0,c316)
| ~ arg2(X0,X1)
| ~ subr(X0,sub_0) )
| ~ spl64_39 ),
inference(resolution,[],[f38153,f10884]) ).
fof(f38229,plain,
( ! [X0,X1] :
( ~ arg2(X0,X1)
| ~ subr(X0,sub_0)
| ~ arg1(X0,c316) )
| ~ spl64_39 ),
inference(duplicate_literal_removal,[],[f38228]) ).
fof(f38304,plain,
( ! [X0,X1] :
( ~ subr(sK58(X0,X1),sub_0)
| ~ arg1(sK58(X0,X1),c316)
| ~ sub(X0,X1) )
| ~ spl64_39 ),
inference(resolution,[],[f38229,f10886]) ).
fof(f38307,plain,
( ! [X0,X1] :
( ~ arg1(sK58(X0,X1),c316)
| ~ sub(X0,X1) )
| ~ spl64_39 ),
inference(forward_subsumption_resolution,[],[f38304,f10885]) ).
fof(f38377,plain,
( ! [X0] :
( ~ sub(c316,X0)
| ~ sub(c316,X0) )
| ~ spl64_39 ),
inference(resolution,[],[f38307,f10887]) ).
fof(f38378,plain,
( ! [X0] : ~ sub(c316,X0)
| ~ spl64_39 ),
inference(duplicate_literal_removal,[],[f38377]) ).
fof(f38443,plain,
( $false
| ~ spl64_39 ),
inference(resolution,[],[f38378,f20850]) ).
fof(f38455,plain,
~ spl64_39,
inference(avatar_contradiction_clause,[],[f38443]) ).
cnf(s1,plain,
( spl64_1
| spl64_2 ),
inference(sat_conversion,[],[f20869]) ).
cnf(s19,plain,
~ spl64_2,
inference(sat_conversion,[],[f24846]) ).
cnf(s24,plain,
~ spl64_28,
inference(sat_conversion,[],[f33497]) ).
cnf(s26,plain,
spl64_33,
inference(sat_conversion,[],[f33735]) ).
cnf(s29,plain,
( ~ spl64_1
| spl64_28
| ~ spl64_33
| spl64_39 ),
inference(sat_conversion,[],[f34324]) ).
cnf(s31,plain,
~ spl64_39,
inference(sat_conversion,[],[f38455]) ).
cnf(s32,plain,
( ~ spl64_1
| spl64_28
| ~ spl64_33 ),
inference(rat,[],[s29,s31]) ).
cnf(s33,plain,
~ spl64_1,
inference(rat,[],[s32,s26,s24]) ).
cnf(s36,plain,
$false,
inference(rat,[],[s1,s19,s33]) ).
fof(f38456,plain,
$false,
inference(avatar_sat_refutation,[],[s36]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+24 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n002.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 23:31:08 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.08/4.08 % (883394)Will run a generic schedule for satisfiability detection.
% 26.08/4.08 % (883404)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=784746789:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 26.08/4.08 % (883400)% WARNING: option uhcvi not known.
% 26.08/4.08 % (883399)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1772950680_2998 on theBenchmark for (2998ds/0Mi)
% 26.08/4.08 % (883400)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3457836612:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 26.08/4.08 % (883401)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=691188924:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 26.08/4.08 % (883402)dis+10_1_sil=32000:sp=arity:random_seed=2517012990:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 26.08/4.08 % (883403)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3718768317:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 26.08/4.08 % (883405)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2594369747:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 26.08/4.08 % (883404)Instruction limit reached!
% 26.08/4.08 % (883404)------------------------------
% 26.08/4.08 % (883404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.08/4.08 % (883404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.08/4.08 % (883404)CaDiCaL version: 2.1.3
% 26.08/4.08 % (883404)Termination reason: Instruction limit
% 26.08/4.08 % (883404)Termination phase: Saturation
% 26.08/4.08 % (883404)Time elapsed: 0.039 s
% 26.08/4.08 % (883404)Peak memory usage: 28 MB
% 26.08/4.08 % (883404)Instructions burned: 132 (million)
% 26.08/4.08 % (883413)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2677058058:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 26.08/4.08 % (883402)Instruction limit reached!
% 26.08/4.08 % (883402)------------------------------
% 26.08/4.08 % (883402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.08/4.08 % (883402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.08/4.08 % (883402)CaDiCaL version: 2.1.3
% 26.08/4.08 % (883402)Termination reason: Instruction limit
% 26.08/4.08 % (883402)Termination phase: Saturation
% 26.08/4.08 % (883402)Time elapsed: 0.057 s
% 26.08/4.08 % (883402)Peak memory usage: 26 MB
% 26.08/4.08 % (883402)Instructions burned: 104 (million)
% 26.08/4.08 % (883403)Instruction limit reached!
% 26.08/4.08 % (883403)------------------------------
% 26.08/4.08 % (883403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.08/4.08 % (883403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.08/4.08 % (883403)CaDiCaL version: 2.1.3
% 26.08/4.08 % (883403)Termination reason: Instruction limit
% 26.08/4.08 % (883403)Termination phase: Blocked clause elimination
% 26.08/4.08 % (883403)Time elapsed: 0.072 s
% 26.08/4.08 % (883403)Peak memory usage: 27 MB
% 26.08/4.08 % (883403)Instructions burned: 117 (million)
% 26.08/4.08 % (883415)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4173225599:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 26.08/4.08 % (883405)Instruction limit reached!
% 26.08/4.08 % (883405)------------------------------
% 26.08/4.08 % (883405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.08/4.08 % (883405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.08/4.08 % (883405)CaDiCaL version: 2.1.3
% 26.08/4.08 % (883405)Termination reason: Instruction limit
% 26.08/4.08 % (883405)Termination phase: Saturation
% 26.08/4.08 % (883405)Time elapsed: 0.090 s
% 26.08/4.08 % (883405)Peak memory usage: 30 MB
% 26.08/4.08 % (883405)Instructions burned: 160 (million)
% 26.08/4.08 % (883416)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=3039599338:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 26.08/4.08 % (883418)ott-21_1_sil=16000:fs=off:random_seed=3264254531:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 26.08/4.08 % TRYING [1]
% 26.08/4.08 % (883415)Instruction limit reached!
% 26.08/4.08 % (883415)------------------------------
% 26.08/4.08 % (883415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.08/4.08 % (883415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.08/4.08 % (883415)CaDiCaL version: 2.1.3
% 26.08/4.08 % (883415)Termination reason: Instruction limit
% 45.14/6.86 % (883415)Termination phase: Blocked clause elimination
% 45.14/6.86 % (883415)Time elapsed: 0.084 s
% 45.14/6.86 % (883415)Peak memory usage: 28 MB
% 45.14/6.86 % (883415)Instructions burned: 132 (million)
% 45.14/6.86 % TRYING [2]
% 45.14/6.86 % (883421)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=736455278:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 45.14/6.86 % (883418)Instruction limit reached!
% 45.14/6.86 % (883418)------------------------------
% 45.14/6.86 % (883418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.14/6.86 % (883418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.14/6.86 % (883418)CaDiCaL version: 2.1.3
% 45.14/6.86 % (883418)Termination reason: Instruction limit
% 45.14/6.86 % (883418)Termination phase: Saturation
% 45.14/6.86 % (883418)Time elapsed: 0.090 s
% 45.14/6.86 % (883418)Peak memory usage: 28 MB
% 45.14/6.86 % (883418)Instructions burned: 181 (million)
% 45.14/6.86 % (883423)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3831056852:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 45.14/6.86 % (883413)Instruction limit reached!
% 45.14/6.86 % (883413)------------------------------
% 45.14/6.86 % (883413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.14/6.86 % (883413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.14/6.86 % (883413)CaDiCaL version: 2.1.3
% 45.14/6.86 % (883413)Termination reason: Instruction limit
% 45.14/6.86 % (883413)Termination phase: Finite model building SAT solving
% 45.14/6.86 % (883413)Time elapsed: 0.182 s
% 45.14/6.86 % (883413)Peak memory usage: 54 MB
% 45.14/6.86 % (883413)Instructions burned: 717 (million)
% 45.14/6.86 % (883425)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2272571446:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 45.14/6.86 % TRYING [1]
% 45.14/6.86 % TRYING [2]
% 45.14/6.86 % TRYING [1]
% 45.14/6.86 % (883421)Instruction limit reached!
% 45.14/6.86 % (883421)------------------------------
% 45.14/6.86 % (883421)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.14/6.86 % (883421)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.14/6.86 % (883421)CaDiCaL version: 2.1.3
% 45.14/6.86 % (883421)Termination reason: Instruction limit
% 45.14/6.87 % (883421)Termination phase: Saturation
% 45.14/6.87 % (883421)Time elapsed: 0.253 s
% 45.14/6.87 % (883421)Peak memory usage: 38 MB
% 45.14/6.87 % (883421)Instructions burned: 477 (million)
% 45.14/6.87 % (883427)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1259081009:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 45.14/6.87 % (883416)Instruction limit reached!
% 45.14/6.87 % (883416)------------------------------
% 45.14/6.87 % (883416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.14/6.87 % (883416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.14/6.87 % (883416)CaDiCaL version: 2.1.3
% 45.14/6.87 % (883416)Termination reason: Instruction limit
% 45.14/6.87 % (883416)Termination phase: Saturation
% 45.14/6.87 % (883416)Time elapsed: 0.375 s
% 45.14/6.87 % (883416)Peak memory usage: 38 MB
% 45.14/6.87 % (883416)Instructions burned: 685 (million)
% 45.14/6.87 % TRYING [3]
% 45.14/6.87 % (883429)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=2403773964: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.14/6.87 % (883423)Instruction limit reached!
% 45.14/6.87 % (883423)------------------------------
% 45.14/6.87 % (883423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.14/6.87 % (883423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.14/6.87 % (883423)CaDiCaL version: 2.1.3
% 45.14/6.87 % (883423)Termination reason: Instruction limit
% 45.14/6.87 % (883423)Termination phase: Finite model building SAT solving
% 45.14/6.87 % (883423)Time elapsed: 0.322 s
% 45.14/6.87 % (883423)Peak memory usage: 38 MB
% 45.14/6.87 % (883423)Instructions burned: 865 (million)
% 45.14/6.87 % (883431)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4147560460:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 45.14/6.87 % (883425)Instruction limit reached!
% 45.14/6.87 % (883425)------------------------------
% 45.14/6.87 % (883425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 45.14/6.87 % (883425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.75/14.15 % (883425)CaDiCaL version: 2.1.3
% 97.75/14.15 % (883425)Termination reason: Instruction limit
% 97.75/14.15 % (883425)Termination phase: Saturation
% 97.75/14.15 % (883425)Time elapsed: 0.347 s
% 97.75/14.15 % (883425)Peak memory usage: 54 MB
% 97.75/14.15 % (883425)Instructions burned: 1181 (million)
% 97.75/14.15 % (883433)fmb+10_1_sil=64000:random_seed=3608587614:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 97.75/14.15 % TRYING [1]
% 97.75/14.15 % TRYING [2]
% 97.75/14.15 % (883429)Instruction limit reached!
% 97.75/14.15 % (883429)------------------------------
% 97.75/14.15 % (883429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.75/14.15 % (883429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.75/14.15 % (883429)CaDiCaL version: 2.1.3
% 97.75/14.15 % (883429)Termination reason: Instruction limit
% 97.75/14.15 % (883429)Termination phase: Saturation
% 97.75/14.15 % (883429)Time elapsed: 0.372 s
% 97.75/14.15 % (883429)Peak memory usage: 42 MB
% 97.75/14.15 % (883429)Instructions burned: 693 (million)
% 97.75/14.15 % (883427)Instruction limit reached!
% 97.75/14.15 % (883427)------------------------------
% 97.75/14.15 % (883427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.75/14.15 % (883427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.75/14.15 % (883427)CaDiCaL version: 2.1.3
% 97.75/14.15 % (883427)Termination reason: Instruction limit
% 97.75/14.15 % (883427)Termination phase: Finite model building constraint generation
% 97.75/14.15 % (883427)Time elapsed: 0.424 s
% 97.75/14.15 % (883427)Peak memory usage: 92 MB
% 97.75/14.15 % (883427)Instructions burned: 889 (million)
% 97.75/14.15 % (883435)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=453243842:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 97.75/14.15 % (883437)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1316332240:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 97.75/14.15 % (883431)Instruction limit reached!
% 97.75/14.15 % (883431)------------------------------
% 97.75/14.15 % (883431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.75/14.15 % (883431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.75/14.15 % (883431)CaDiCaL version: 2.1.3
% 97.75/14.15 % (883431)Termination reason: Instruction limit
% 97.75/14.15 % (883431)Termination phase: Saturation
% 97.75/14.15 % (883431)Time elapsed: 0.387 s
% 97.75/14.15 % (883431)Peak memory usage: 39 MB
% 97.75/14.15 % (883431)Instructions burned: 881 (million)
% 97.75/14.15 % (883439)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1176623197:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 97.75/14.15 % TRYING [20]
% 97.75/14.15 % TRYING [8]
% 97.75/14.15 % TRYING [3]
% 97.75/14.15 % (883437)Instruction limit reached!
% 97.75/14.15 % (883437)------------------------------
% 97.75/14.15 % (883437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.75/14.15 % (883437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.75/14.15 % (883437)CaDiCaL version: 2.1.3
% 97.75/14.15 % (883437)Termination reason: Instruction limit
% 97.75/14.15 % (883437)Termination phase: Finite model building constraint generation
% 97.75/14.15 % (883437)Time elapsed: 0.366 s
% 97.75/14.15 % (883437)Peak memory usage: 64 MB
% 97.75/14.15 % (883437)Instructions burned: 923 (million)
% 97.75/14.15 % (883441)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1228492702:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 97.75/14.15 % TRYING [4]
% 97.75/14.15 % (883441)Instruction limit reached!
% 97.75/14.15 % (883441)------------------------------
% 97.75/14.15 % (883441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.75/14.15 % (883441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.75/14.15 % (883441)CaDiCaL version: 2.1.3
% 97.75/14.15 % (883441)Termination reason: Instruction limit
% 97.75/14.15 % (883441)Termination phase: Saturation
% 97.75/14.15 % (883441)Time elapsed: 0.675 s
% 97.75/14.15 % (883441)Peak memory usage: 35 MB
% 97.75/14.15 % (883441)Instructions burned: 1473 (million)
% 97.75/14.15 % (883443)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=640630722:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 97.75/14.15 % TRYING [77]
% 97.75/14.15 % TRYING [4]
% 97.75/14.15 % TRYING [5]
% 97.75/14.15 % (883439)Instruction limit reached!
% 97.75/14.15 % (883439)------------------------------
% 97.75/14.15 % (883439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 97.75/14.15 % (883439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 97.75/14.15 % (883439)CaDiCaL version: 2.1.3
% 215.96/30.96 % (883439)Termination reason: Instruction limit
% 215.96/30.96 % (883439)Termination phase: Saturation
% 215.96/30.96 % (883439)Time elapsed: 2.691 s
% 215.96/30.96 % (883439)Peak memory usage: 39 MB
% 215.96/30.96 % (883439)Instructions burned: 5132 (million)
% 215.96/30.96 % (883445)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1528210131:fmbsr=2.30978:i=2174_2961 on theBenchmark for (2961ds/2174Mi)
% 215.96/30.96 % TRYING [16]
% 215.96/30.96 % (883435)Instruction limit reached!
% 215.96/30.96 % (883435)------------------------------
% 215.96/30.96 % (883435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 215.96/30.96 % (883435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.96/30.96 % (883435)CaDiCaL version: 2.1.3
% 215.96/30.96 % (883435)Termination reason: Instruction limit
% 215.96/30.96 % (883435)Termination phase: Finite model building constraint generation
% 215.96/30.96 % (883435)Time elapsed: 3.304 s
% 215.96/30.96 % (883435)Peak memory usage: 551 MB
% 215.96/30.96 % (883435)Instructions burned: 9519 (million)
% 215.96/30.96 % (883443)Instruction limit reached!
% 215.96/30.96 % (883443)------------------------------
% 215.96/30.96 % (883443)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 215.96/30.96 % (883443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.96/30.96 % (883443)CaDiCaL version: 2.1.3
% 215.96/30.96 % (883443)Termination reason: Instruction limit
% 215.96/30.96 % (883443)Termination phase: Finite model building constraint generation
% 215.96/30.96 % (883443)Time elapsed: 2.253 s
% 215.96/30.96 % (883443)Peak memory usage: 417 MB
% 215.96/30.96 % (883443)Instructions burned: 6325 (million)
% 215.96/30.96 % (883447)ott-2_1_sil=16000:newcnf=on:random_seed=1526140829:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2955 on theBenchmark for (2955ds/869Mi)
% 215.96/30.96 % (883449)ott+10_1_sil=32000:tgt=ground:random_seed=2805922877:i=5114:av=off_2955 on theBenchmark for (2955ds/5114Mi)
% 215.96/30.96 % (883445)Instruction limit reached!
% 215.96/30.96 % (883445)------------------------------
% 215.96/30.96 % (883445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 215.96/30.96 % (883445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.96/30.96 % (883445)CaDiCaL version: 2.1.3
% 215.96/30.96 % (883445)Termination reason: Instruction limit
% 215.96/30.96 % (883445)Termination phase: Finite model building constraint generation
% 215.96/30.96 % (883445)Time elapsed: 0.763 s
% 215.96/30.96 % (883445)Peak memory usage: 121 MB
% 215.96/30.96 % (883445)Instructions burned: 2175 (million)
% 215.96/30.96 % (883451)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=319456935:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 215.96/30.96 % (883447)Instruction limit reached!
% 215.96/30.96 % (883447)------------------------------
% 215.96/30.96 % (883447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 215.96/30.96 % (883447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.96/30.96 % (883447)CaDiCaL version: 2.1.3
% 215.96/30.96 % (883447)Termination reason: Instruction limit
% 215.96/30.96 % (883447)Termination phase: Saturation
% 215.96/30.96 % (883447)Time elapsed: 0.389 s
% 215.96/30.96 % (883447)Peak memory usage: 36 MB
% 215.96/30.96 % (883447)Instructions burned: 869 (million)
% 215.96/30.96 % (883453)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3833346281:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 215.96/30.96 % TRYING [1]
% 215.96/30.96 % TRYING [2]
% 215.96/30.96 % TRYING [3]
% 215.96/30.96 % TRYING [6]
% 215.96/30.96 % (883433)Instruction limit reached!
% 215.96/30.96 % (883433)------------------------------
% 215.96/30.96 % (883433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 215.96/30.96 % (883433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.96/30.96 % (883433)CaDiCaL version: 2.1.3
% 215.96/30.96 % (883433)Termination reason: Instruction limit
% 215.96/30.96 % (883433)Termination phase: Finite model building constraint generation
% 215.96/30.96 % (883433)Time elapsed: 5.196 s
% 215.96/30.96 % (883433)Peak memory usage: 150 MB
% 215.96/30.96 % (883433)Instructions burned: 22064 (million)
% 215.96/30.96 % (883455)dis+21_1_sil=32000:sas=cadical:random_seed=1219217843:i=3773:amm=off_2940 on theBenchmark for (2940ds/3773Mi)
% 215.96/30.96 % (883453)Instruction limit reached!
% 215.96/30.96 % (883453)------------------------------
% 215.96/30.96 % (883453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 215.96/30.96 % (883453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 215.96/30.96 % (883453)CaDiCaL version: 2.1.3
% 215.96/30.96 % (883453)Termination reason: Instruction limit
% 183.28/39.15 % (883453)Termination phase: Saturation
% 183.28/39.15 % (883453)Time elapsed: 1.763 s
% 183.28/39.15 % (883453)Peak memory usage: 40 MB
% 183.28/39.15 % (883453)Instructions burned: 3512 (million)
% 183.28/39.15 % (883457)ott+11_1_sil=16000:gs=on:random_seed=198160014:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2933 on theBenchmark for (2933ds/2251Mi)
% 183.28/39.15 % (883455)Instruction limit reached!
% 183.28/39.15 % (883455)------------------------------
% 183.28/39.15 % (883455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883455)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883455)Termination reason: Instruction limit
% 183.28/39.15 % (883455)Termination phase: Saturation
% 183.28/39.15 % (883455)Time elapsed: 0.951 s
% 183.28/39.15 % (883455)Peak memory usage: 65 MB
% 183.28/39.15 % (883455)Instructions burned: 3776 (million)
% 183.28/39.15 % (883459)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3432458028:fmbsr=1.6:i=67534_2930 on theBenchmark for (2930ds/67534Mi)
% 183.28/39.15 % TRYING [4]
% 183.28/39.15 % (883449)Instruction limit reached!
% 183.28/39.15 % (883449)------------------------------
% 183.28/39.15 % (883449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883449)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883449)Termination reason: Instruction limit
% 183.28/39.15 % (883449)Termination phase: Saturation
% 183.28/39.15 % (883449)Time elapsed: 2.592 s
% 183.28/39.15 % (883449)Peak memory usage: 120 MB
% 183.28/39.15 % (883449)Instructions burned: 5115 (million)
% 183.28/39.15 % TRYING [7]
% 183.28/39.15 % (883461)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=4099159109:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2928 on theBenchmark for (2928ds/4591Mi)
% 183.28/39.15 % (883457)Instruction limit reached!
% 183.28/39.15 % (883457)------------------------------
% 183.28/39.15 % (883457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883457)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883457)Termination reason: Instruction limit
% 183.28/39.15 % (883457)Termination phase: Saturation
% 183.28/39.15 % (883457)Time elapsed: 1.175 s
% 183.28/39.15 % (883457)Peak memory usage: 83 MB
% 183.28/39.15 % (883457)Instructions burned: 2251 (million)
% 183.28/39.15 % (883463)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1744182826:i=29340_2921 on theBenchmark for (2921ds/29340Mi)
% 183.28/39.15 % (883461)Instruction limit reached!
% 183.28/39.15 % (883461)------------------------------
% 183.28/39.15 % (883461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883461)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883461)Termination reason: Instruction limit
% 183.28/39.15 % (883461)Termination phase: Saturation
% 183.28/39.15 % (883461)Time elapsed: 2.078 s
% 183.28/39.15 % (883461)Peak memory usage: 43 MB
% 183.28/39.15 % (883461)Instructions burned: 4592 (million)
% 183.28/39.15 % (883465)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1320015528:i=5211_2907 on theBenchmark for (2907ds/5211Mi)
% 183.28/39.15 % (883465)Instruction limit reached!
% 183.28/39.15 % (883465)------------------------------
% 183.28/39.15 % (883465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883465)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883465)Termination reason: Instruction limit
% 183.28/39.15 % (883465)Termination phase: Saturation
% 183.28/39.15 % (883465)Time elapsed: 2.639 s
% 183.28/39.15 % (883465)Peak memory usage: 52 MB
% 183.28/39.15 % (883465)Instructions burned: 5213 (million)
% 183.28/39.15 % (883467)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4032543573:i=5497:nm=2_2881 on theBenchmark for (2881ds/5497Mi)
% 183.28/39.15 % TRYING [17]
% 183.28/39.15 % (883467)Instruction limit reached!
% 183.28/39.15 % (883467)------------------------------
% 183.28/39.15 % (883467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883467)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883467)Termination reason: Instruction limit
% 183.28/39.15 % (883467)Termination phase: Finite model building constraint generation
% 183.28/39.15 % (883467)Time elapsed: 2.008 s
% 183.28/39.15 % (883467)Peak memory usage: 350 MB
% 183.28/39.15 % (883467)Instructions burned: 5499 (million)
% 183.28/39.15 % (883469)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3035083434:fmbsr=2:i=46332_2860 on theBenchmark for (2860ds/46332Mi)
% 183.28/39.15 % TRYING [15]
% 183.28/39.15 % TRYING [5]
% 183.28/39.15 % (883463)Instruction limit reached!
% 183.28/39.15 % (883463)------------------------------
% 183.28/39.15 % (883463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883463)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883463)Termination reason: Instruction limit
% 183.28/39.15 % (883463)Termination phase: Saturation
% 183.28/39.15 % (883463)Time elapsed: 13.0000 s
% 183.28/39.15 % (883463)Peak memory usage: 82 MB
% 183.28/39.15 % (883463)Instructions burned: 29340 (million)
% 183.28/39.15 % (883471)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1250920654:i=14071_2791 on theBenchmark for (2791ds/14071Mi)
% 183.28/39.15 % TRYING [12]
% 183.28/39.15 % TRYING [5]
% 183.28/39.15 % (883459)Instruction limit reached!
% 183.28/39.15 % (883459)------------------------------
% 183.28/39.15 % (883459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883459)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883459)Termination reason: Instruction limit
% 183.28/39.15 % (883459)Termination phase: Finite model building SAT solving
% 183.28/39.15 % (883459)Time elapsed: 16.129 s
% 183.28/39.15 % (883459)Peak memory usage: 291 MB
% 183.28/39.15 % (883459)Instructions burned: 67536 (million)
% 183.28/39.15 % (883473)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3863901448:i=22565:add=on:rawr=on_2768 on theBenchmark for (2768ds/22565Mi)
% 183.28/39.15 % (883471)Instruction limit reached!
% 183.28/39.15 % (883471)------------------------------
% 183.28/39.15 % (883471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883471)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883471)Termination reason: Instruction limit
% 183.28/39.15 % (883471)Termination phase: Finite model building constraint generation
% 183.28/39.15 % (883471)Time elapsed: 6.520 s
% 183.28/39.15 % (883471)Peak memory usage: 1122 MB
% 183.28/39.15 % (883471)Instructions burned: 14072 (million)
% 183.28/39.15 % (883475)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2971490859:i=8173:av=off_2724 on theBenchmark for (2724ds/8173Mi)
% 183.28/39.15 % (883473)Instruction limit reached!
% 183.28/39.15 % (883473)------------------------------
% 183.28/39.15 % (883473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883473)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883473)Termination reason: Instruction limit
% 183.28/39.15 % (883473)Termination phase: Saturation
% 183.28/39.15 % (883473)Time elapsed: 4.699 s
% 183.28/39.15 % (883473)Peak memory usage: 130 MB
% 183.28/39.15 % (883473)Instructions burned: 22566 (million)
% 183.28/39.15 % (883477)dis+10_16:1_sil=16000:random_seed=1140981264:i=9155:fsr=off_2721 on theBenchmark for (2721ds/9155Mi)
% 183.28/39.15 % (883477)Instruction limit reached!
% 183.28/39.15 % (883477)------------------------------
% 183.28/39.15 % (883477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883477)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883477)Termination reason: Instruction limit
% 183.28/39.15 % (883477)Termination phase: Saturation
% 183.28/39.15 % (883477)Time elapsed: 2.104 s
% 183.28/39.15 % (883477)Peak memory usage: 82 MB
% 183.28/39.15 % (883477)Instructions burned: 9156 (million)
% 183.28/39.15 % (883479)ott-3_8_sil=64000:random_seed=2684390730:i=20139:bs=on_2700 on theBenchmark for (2700ds/20139Mi)
% 183.28/39.15 % (883401)Instruction limit reached!
% 183.28/39.15 % (883401)------------------------------
% 183.28/39.15 % (883401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883401)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883401)Termination reason: Instruction limit
% 183.28/39.15 % (883401)Termination phase: Saturation
% 183.28/39.15 % (883401)Time elapsed: 30.560 s
% 183.28/39.15 % (883401)Peak memory usage: 161 MB
% 183.28/39.15 % (883401)Instructions burned: 88027 (million)
% 183.28/39.15 % (883481)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2799923147:fmbsr=2:i=32576_2692 on theBenchmark for (2692ds/32576Mi)
% 183.28/39.15 % TRYING [9]
% 183.28/39.15 % (883451)Instruction limit reached!
% 183.28/39.15 % (883451)------------------------------
% 183.28/39.15 % (883451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883451)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883451)Termination reason: Instruction limit
% 183.28/39.15 % (883451)Termination phase: Finite model building SAT solving
% 183.28/39.15 % (883451)Time elapsed: 26.885 s
% 183.28/39.15 % (883451)Peak memory usage: 246 MB
% 183.28/39.15 % (883451)Instructions burned: 54282 (million)
% 183.28/39.15 % (883483)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3421957928:i=11404_2684 on theBenchmark for (2684ds/11404Mi)
% 183.28/39.15 % (883475)Instruction limit reached!
% 183.28/39.15 % (883475)------------------------------
% 183.28/39.15 % (883475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883475)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883475)Termination reason: Instruction limit
% 183.28/39.15 % (883475)Termination phase: Saturation
% 183.28/39.15 % (883475)Time elapsed: 4.593 s
% 183.28/39.15 % (883475)Peak memory usage: 192 MB
% 183.28/39.15 % (883475)Instructions burned: 8174 (million)
% 183.28/39.15 % (883485)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1615509787:i=14134_2678 on theBenchmark for (2678ds/14134Mi)
% 183.28/39.15 % (883469)Instruction limit reached!
% 183.28/39.15 % (883469)------------------------------
% 183.28/39.15 % (883469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883469)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883469)Termination reason: Instruction limit
% 183.28/39.15 % (883469)Termination phase: Finite model building constraint generation
% 183.28/39.15 % (883469)Time elapsed: 21.883 s
% 183.28/39.15 % (883469)Peak memory usage: 3367 MB
% 183.28/39.15 % (883469)Instructions burned: 46333 (million)
% 183.28/39.15 % (883487)dis+33_16_sil=32000:sac=on:random_seed=2320261748:i=15851:nm=0_2637 on theBenchmark for (2637ds/15851Mi)
% 183.28/39.15 % (883483)Instruction limit reached!
% 183.28/39.15 % (883483)------------------------------
% 183.28/39.15 % (883483)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883483)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883483)Termination reason: Instruction limit
% 183.28/39.15 % (883483)Termination phase: Saturation
% 183.28/39.15 % (883483)Time elapsed: 4.896 s
% 183.28/39.15 % (883483)Peak memory usage: 147 MB
% 183.28/39.15 % (883483)Instructions burned: 11406 (million)
% 183.28/39.15 % (883489)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1913975314:avsq=on:i=17627:add=on:amm=off_2634 on theBenchmark for (2634ds/17627Mi)
% 183.28/39.15 % (883479)Instruction limit reached!
% 183.28/39.15 % (883479)------------------------------
% 183.28/39.15 % (883479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.15 % (883479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.15 % (883479)CaDiCaL version: 2.1.3
% 183.28/39.15 % (883479)Termination reason: Instruction limit
% 183.28/39.15 % (883479)Termination phase: Saturation
% 183.28/39.15 % (883479)Time elapsed: 6.592 s
% 183.28/39.15 % (883479)Peak memory usage: 82 MB
% 183.28/39.15 % (883479)Instructions burned: 20139 (million)
% 183.28/39.15 % (883491)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1086840625:s2a=on:i=53295_2634 on theBenchmark for (2634ds/53295Mi)
% 183.28/39.15 % (883485) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-883394-883485"...
% 183.28/39.15 % (883485)...printing done.
% 183.28/39.15 % (883485)Refutation found. Thanks to Tanya!
% 183.28/39.15 % SZS status Theorem for theBenchmark
% 183.28/39.15 % SZS output start Proof for theBenchmark
% See solution above
% 183.28/39.17 % (883485)------------------------------
% 183.28/39.17 % (883485)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 183.28/39.17 % (883485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 183.28/39.17 % (883485)CaDiCaL version: 2.1.3
% 183.28/39.17 % (883485)Termination reason: Refutation
% 183.28/39.17 % (883485)Time elapsed: 6.573 s
% 183.28/39.17 % (883485)Peak memory usage: 63 MB
% 183.28/39.17 % (883485)Instructions burned: 11989 (million)
% 183.28/39.17 % (883394)Success in time 38.928 s
% 183.28/39.17 % Vampire exiting
%------------------------------------------------------------------------------