%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR116+22 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:45:49 AM UTC 2026
% Result : Theorem 202.08s 42.63s
% Output : Refutation 202.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 16
% Syntax : Number of formulae : 136 ( 40 unt; 7 def)
% Number of atoms : 946 ( 0 equ)
% Maximal formula atoms : 90 ( 6 avg)
% Number of connectives : 1065 ( 255 ~; 224 |; 574 &)
% ( 7 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 90 ( 9 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 36 ( 35 usr; 8 prp; 0-2 aty)
% Number of functors : 49 ( 49 usr; 41 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/sandbox/benchmark/Axioms/CSR004+0.ax',member_first) ).
fof(f11,axiom,
! [X0,X1] :
( fact(X0,X1)
=> has_fact_leq(X0,X1) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/CSR004+0.ax',attr_name_hei__337en_1_1) ).
fof(f161,axiom,
! [X0,X1,X2] :
( ( arg1(X0,X1)
& arg2(X0,X2)
& subs(X0,hei__337en_1_1) )
=> ? [X3,X4] :
( arg1(X4,X1)
& arg2(X4,X2)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR004+0.ax',hei__337en_1_1__bezeichnen_1_1_als) ).
fof(f9161,axiom,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',synth_qa07_010_mira_news_1784) ).
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,
( pars(c124,c9)
& pred(c124,autobiographie_1_1)
& attch(c133,c124)
& attr(c133,c134)
& attr(c133,c135)
& prop(c133,s__374dafrikanisch_1_1)
& sub(c133,pr__344sident_1_1)
& sub(c134,eigenname_1_1)
& val(c134,nelson_0)
& sub(c135,familiename_1_1)
& val(c135,mandela_0)
& name(c9,ein_f__374hrer_ist_ein_hirte_0)
& sort(c124,d)
& sort(c124,io)
& card(c124,cons(x_constant,cons(int1,nil)))
& etype(c124,int1)
& fact(c124,real)
& gener(c124,sp)
& quant(c124,mult)
& refer(c124,det)
& varia(c124,con)
& sort(c9,o)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,gener_c)
& quant(c9,one)
& refer(c9,refer_c)
& varia(c9,varia_c)
& 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(c133,d)
& card(c133,int1)
& etype(c133,int0)
& fact(c133,real)
& gener(c133,sp)
& quant(c133,one)
& refer(c133,det)
& varia(c133,con)
& sort(c134,na)
& card(c134,int1)
& etype(c134,int0)
& fact(c134,real)
& gener(c134,sp)
& quant(c134,one)
& refer(c134,indet)
& varia(c134,varia_c)
& sort(c135,na)
& card(c135,int1)
& etype(c135,int0)
& fact(c135,real)
& gener(c135,sp)
& quant(c135,one)
& refer(c135,indet)
& varia(c135,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(ein_f__374hrer_ist_ein_hirte_0,fe) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_news_1784) ).
fof(f10191,plain,
( pred(c124,autobiographie_1_1)
& attch(c133,c124)
& attr(c133,c134)
& attr(c133,c135)
& prop(c133,s__374dafrikanisch_1_1)
& sub(c133,pr__344sident_1_1)
& sub(c134,eigenname_1_1)
& val(c134,nelson_0)
& sub(c135,familiename_1_1)
& val(c135,mandela_0)
& name(c9,ein_f__374hrer_ist_ein_hirte_0)
& sort(c124,d)
& sort(c124,io)
& card(c124,cons(x_constant,cons(int1,nil)))
& etype(c124,int1)
& fact(c124,real)
& gener(c124,sp)
& quant(c124,mult)
& refer(c124,det)
& varia(c124,con)
& sort(c9,o)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,gener_c)
& quant(c9,one)
& refer(c9,refer_c)
& varia(c9,varia_c)
& 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(c133,d)
& card(c133,int1)
& etype(c133,int0)
& fact(c133,real)
& gener(c133,sp)
& quant(c133,one)
& refer(c133,det)
& varia(c133,con)
& sort(c134,na)
& card(c134,int1)
& etype(c134,int0)
& fact(c134,real)
& gener(c134,sp)
& quant(c134,one)
& refer(c134,indet)
& varia(c134,varia_c)
& sort(c135,na)
& card(c135,int1)
& etype(c135,int0)
& fact(c135,real)
& gener(c135,sp)
& quant(c135,one)
& refer(c135,indet)
& varia(c135,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(ein_f__374hrer_ist_ein_hirte_0,fe) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10327,plain,
( pred(c124,autobiographie_1_1)
& attch(c133,c124)
& attr(c133,c134)
& attr(c133,c135)
& prop(c133,s__374dafrikanisch_1_1)
& sub(c133,pr__344sident_1_1)
& sub(c134,eigenname_1_1)
& val(c134,nelson_0)
& sub(c135,familiename_1_1)
& val(c135,mandela_0)
& name(c9,ein_f__374hrer_ist_ein_hirte_0)
& card(c124,cons(x_constant,cons(int1,nil)))
& etype(c124,int1)
& fact(c124,real)
& gener(c124,sp)
& quant(c124,mult)
& refer(c124,det)
& varia(c124,con)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,gener_c)
& quant(c9,one)
& refer(c9,refer_c)
& varia(c9,varia_c)
& 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(c133,int1)
& etype(c133,int0)
& fact(c133,real)
& gener(c133,sp)
& quant(c133,one)
& refer(c133,det)
& varia(c133,con)
& card(c134,int1)
& etype(c134,int0)
& fact(c134,real)
& gener(c134,sp)
& quant(c134,one)
& refer(c134,indet)
& varia(c134,varia_c)
& card(c135,int1)
& etype(c135,int0)
& fact(c135,real)
& gener(c135,sp)
& quant(c135,one)
& refer(c135,indet)
& varia(c135,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) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10330,plain,
( pred(c124,autobiographie_1_1)
& attch(c133,c124)
& attr(c133,c134)
& attr(c133,c135)
& prop(c133,s__374dafrikanisch_1_1)
& sub(c133,pr__344sident_1_1)
& sub(c134,eigenname_1_1)
& val(c134,nelson_0)
& sub(c135,familiename_1_1)
& val(c135,mandela_0)
& name(c9,ein_f__374hrer_ist_ein_hirte_0)
& card(c124,cons(x_constant,cons(int1,nil)))
& etype(c124,int1)
& fact(c124,real)
& gener(c124,sp)
& refer(c124,det)
& varia(c124,con)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,gener_c)
& refer(c9,refer_c)
& varia(c9,varia_c)
& 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(c133,int1)
& etype(c133,int0)
& fact(c133,real)
& gener(c133,sp)
& refer(c133,det)
& varia(c133,con)
& card(c134,int1)
& etype(c134,int0)
& fact(c134,real)
& gener(c134,sp)
& refer(c134,indet)
& varia(c134,varia_c)
& card(c135,int1)
& etype(c135,int0)
& fact(c135,real)
& gener(c135,sp)
& refer(c135,indet)
& varia(c135,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) ),
inference(pure_predicate_removal,[],[f10327]) ).
fof(f10333,plain,
( pred(c124,autobiographie_1_1)
& attch(c133,c124)
& attr(c133,c134)
& attr(c133,c135)
& prop(c133,s__374dafrikanisch_1_1)
& sub(c133,pr__344sident_1_1)
& sub(c134,eigenname_1_1)
& val(c134,nelson_0)
& sub(c135,familiename_1_1)
& val(c135,mandela_0)
& name(c9,ein_f__374hrer_ist_ein_hirte_0)
& etype(c124,int1)
& fact(c124,real)
& gener(c124,sp)
& refer(c124,det)
& varia(c124,con)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,gener_c)
& refer(c9,refer_c)
& varia(c9,varia_c)
& 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(c133,int0)
& fact(c133,real)
& gener(c133,sp)
& refer(c133,det)
& varia(c133,con)
& etype(c134,int0)
& fact(c134,real)
& gener(c134,sp)
& refer(c134,indet)
& varia(c134,varia_c)
& etype(c135,int0)
& fact(c135,real)
& gener(c135,sp)
& refer(c135,indet)
& varia(c135,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) ),
inference(pure_predicate_removal,[],[f10330]) ).
fof(f10336,plain,
( pred(c124,autobiographie_1_1)
& attch(c133,c124)
& attr(c133,c134)
& attr(c133,c135)
& prop(c133,s__374dafrikanisch_1_1)
& sub(c133,pr__344sident_1_1)
& sub(c134,eigenname_1_1)
& val(c134,nelson_0)
& sub(c135,familiename_1_1)
& val(c135,mandela_0)
& name(c9,ein_f__374hrer_ist_ein_hirte_0)
& etype(c124,int1)
& fact(c124,real)
& gener(c124,sp)
& varia(c124,con)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,gener_c)
& varia(c9,varia_c)
& etype(autobiographie_1_1,int0)
& fact(autobiographie_1_1,real)
& gener(autobiographie_1_1,ge)
& varia(autobiographie_1_1,varia_c)
& etype(c133,int0)
& fact(c133,real)
& gener(c133,sp)
& varia(c133,con)
& etype(c134,int0)
& fact(c134,real)
& gener(c134,sp)
& varia(c134,varia_c)
& etype(c135,int0)
& fact(c135,real)
& gener(c135,sp)
& varia(c135,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) ),
inference(pure_predicate_removal,[],[f10333]) ).
fof(f10341,plain,
( pred(c124,autobiographie_1_1)
& attch(c133,c124)
& attr(c133,c134)
& attr(c133,c135)
& prop(c133,s__374dafrikanisch_1_1)
& sub(c133,pr__344sident_1_1)
& sub(c134,eigenname_1_1)
& val(c134,nelson_0)
& sub(c135,familiename_1_1)
& val(c135,mandela_0)
& name(c9,ein_f__374hrer_ist_ein_hirte_0)
& etype(c124,int1)
& fact(c124,real)
& gener(c124,sp)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,gener_c)
& etype(autobiographie_1_1,int0)
& fact(autobiographie_1_1,real)
& gener(autobiographie_1_1,ge)
& etype(c133,int0)
& fact(c133,real)
& gener(c133,sp)
& etype(c134,int0)
& fact(c134,real)
& gener(c134,sp)
& etype(c135,int0)
& fact(c135,real)
& gener(c135,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) ),
inference(pure_predicate_removal,[],[f10336]) ).
fof(f10346,plain,
( pred(c124,autobiographie_1_1)
& attch(c133,c124)
& attr(c133,c134)
& attr(c133,c135)
& prop(c133,s__374dafrikanisch_1_1)
& sub(c133,pr__344sident_1_1)
& sub(c134,eigenname_1_1)
& val(c134,nelson_0)
& sub(c135,familiename_1_1)
& val(c135,mandela_0)
& name(c9,ein_f__374hrer_ist_ein_hirte_0)
& etype(c124,int1)
& fact(c124,real)
& etype(c9,int0)
& fact(c9,real)
& etype(autobiographie_1_1,int0)
& fact(autobiographie_1_1,real)
& etype(c133,int0)
& fact(c133,real)
& etype(c134,int0)
& fact(c134,real)
& etype(c135,int0)
& fact(c135,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) ),
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(f20827,plain,
fact(c133,real),
inference(cnf_transformation,[],[f10346]) ).
fof(f20836,plain,
val(c135,mandela_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20837,plain,
sub(c135,familiename_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20838,plain,
val(c134,nelson_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20839,plain,
sub(c134,eigenname_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20840,plain,
sub(c133,pr__344sident_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20841,plain,
prop(c133,s__374dafrikanisch_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20842,plain,
attr(c133,c135),
inference(cnf_transformation,[],[f10346]) ).
fof(f20843,plain,
attr(c133,c134),
inference(cnf_transformation,[],[f10346]) ).
fof(f20847,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(f20848,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,[],[f20847]) ).
fof(f20850,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(f20851,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,[],[f20850]) ).
fof(f20852,plain,
( spl63_1
| spl63_2 ),
inference(avatar_split_clause,[],[f20816,f20850,f20847]) ).
fof(f20882,plain,
has_fact_leq(c133,real),
inference(resolution,[],[f10602,f20827]) ).
fof(f59993,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| val(sK48(X0,s__374dafrika_0),s__374dafrika_0) ),
inference(resolution,[],[f10852,f19789]) ).
fof(f60179,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| sub(sK48(X0,s__374dafrika_0),name_1_1) ),
inference(resolution,[],[f10853,f19789]) ).
fof(f60551,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| loc(X0,sK49(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10855,f19789]) ).
fof(f62919,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| attr(sK47(X0,s__374dafrika_0),sK48(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10856,f19789]) ).
fof(f63105,plain,
! [X0] :
( ~ prop(X0,s__374dafrikanisch_1_1)
| in(sK49(X0,s__374dafrika_0),sK47(X0,s__374dafrika_0)) ),
inference(resolution,[],[f10857,f19789]) ).
fof(f71319,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| subs(sK50(X0),hei__337en_1_1)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10860,f10600]) ).
fof(f71321,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| arg2(sK50(X0),X0)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10861,f10600]) ).
fof(f71323,plain,
! [X0,X1] :
( ~ sub(X1,eigenname_1_1)
| arg1(sK50(X0),X0)
| ~ attr(X0,X1) ),
inference(resolution,[],[f10862,f10600]) ).
fof(f71886,plain,
val(sK48(c133,s__374dafrika_0),s__374dafrika_0),
inference(resolution,[],[f59993,f20841]) ).
fof(f71891,plain,
sub(sK48(c133,s__374dafrika_0),name_1_1),
inference(resolution,[],[f60179,f20841]) ).
fof(f71924,plain,
loc(c133,sK49(c133,s__374dafrika_0)),
inference(resolution,[],[f60551,f20841]) ).
fof(f71932,plain,
( ~ has_fact_leq(c133,real)
| obj(sK2(sK49(c133,s__374dafrika_0),c133),c133) ),
inference(resolution,[],[f71924,f10686]) ).
fof(f71943,plain,
obj(sK2(sK49(c133,s__374dafrika_0),c133),c133),
inference(forward_subsumption_resolution,[],[f71932,f20882]) ).
fof(f72147,plain,
attr(sK47(c133,s__374dafrika_0),sK48(c133,s__374dafrika_0)),
inference(resolution,[],[f62919,f20841]) ).
fof(f72148,plain,
( ! [X0] :
( ~ val(sK48(c133,s__374dafrika_0),s__374dafrika_0)
| ~ sub(sK48(c133,s__374dafrika_0),name_1_1)
| ~ in(X0,sK47(c133,s__374dafrika_0)) )
| ~ spl63_2 ),
inference(resolution,[],[f72147,f20851]) ).
fof(f72149,plain,
( ! [X0] :
( ~ sub(sK48(c133,s__374dafrika_0),name_1_1)
| ~ in(X0,sK47(c133,s__374dafrika_0)) )
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f72148,f71886]) ).
fof(f72150,plain,
( ! [X0] : ~ in(X0,sK47(c133,s__374dafrika_0))
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f72149,f71891]) ).
fof(f72151,plain,
in(sK49(c133,s__374dafrika_0),sK47(c133,s__374dafrika_0)),
inference(resolution,[],[f63105,f20841]) ).
fof(f72152,plain,
( $false
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f72151,f72150]) ).
fof(f72153,plain,
~ spl63_2,
inference(avatar_contradiction_clause,[],[f72152]) ).
fof(f75609,plain,
! [X0] :
( ~ attr(X0,c134)
| subs(sK50(X0),hei__337en_1_1) ),
inference(resolution,[],[f71319,f20839]) ).
fof(f75698,plain,
! [X0] :
( ~ attr(X0,c134)
| arg2(sK50(X0),X0) ),
inference(resolution,[],[f71321,f20839]) ).
fof(f75787,plain,
! [X0] :
( ~ attr(X0,c134)
| arg1(sK50(X0),X0) ),
inference(resolution,[],[f71323,f20839]) ).
fof(f84336,plain,
subs(sK50(c133),hei__337en_1_1),
inference(resolution,[],[f75609,f20843]) ).
fof(f84338,plain,
! [X0,X1] :
( ~ arg2(sK50(c133),X1)
| ~ arg1(sK50(c133),X0)
| subr(sK53(sK50(c133),X0,X1),rprs_0) ),
inference(resolution,[],[f84336,f10868]) ).
fof(f84342,plain,
! [X0,X1] :
( ~ arg2(sK50(c133),X1)
| ~ arg1(sK50(c133),X0)
| arg2(sK53(sK50(c133),X0,X1),X1) ),
inference(resolution,[],[f84336,f10872]) ).
fof(f84343,plain,
! [X0,X1] :
( ~ arg2(sK50(c133),X1)
| ~ arg1(sK50(c133),X0)
| arg1(sK53(sK50(c133),X0,X1),X0) ),
inference(resolution,[],[f84336,f10873]) ).
fof(f84356,plain,
arg2(sK50(c133),c133),
inference(resolution,[],[f75698,f20843]) ).
fof(f84359,definition,
( spl63_3069
<=> ! [X2] : ~ sub(c133,X2) ),
introduced(definition,[new_symbols(definition,[spl63_3069])],[avatar_definition]) ).
fof(f84360,plain,
( ! [X2] : ~ sub(c133,X2)
| ~ spl63_3069 ),
inference(avatar_component_clause,[],[f84359]) ).
fof(f84369,plain,
arg1(sK50(c133),c133),
inference(resolution,[],[f75787,f20843]) ).
fof(f85919,plain,
! [X0] :
( ~ arg1(sK50(c133),X0)
| subr(sK53(sK50(c133),X0,c133),rprs_0) ),
inference(resolution,[],[f84338,f84356]) ).
fof(f85920,plain,
subr(sK53(sK50(c133),c133,c133),rprs_0),
inference(resolution,[],[f85919,f84369]) ).
fof(f85952,plain,
! [X0] :
( ~ arg1(sK50(c133),X0)
| arg2(sK53(sK50(c133),X0,c133),c133) ),
inference(resolution,[],[f84342,f84356]) ).
fof(f85953,plain,
arg2(sK53(sK50(c133),c133,c133),c133),
inference(resolution,[],[f85952,f84369]) ).
fof(f85954,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ val(X0,nelson_0)
| ~ val(X1,mandela_0)
| ~ subr(sK53(sK50(c133),c133,c133),rprs_0)
| ~ sub(c133,X2)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X3,X4)
| ~ attr(X4,X0)
| ~ attr(X4,X1)
| ~ arg1(sK53(sK50(c133),c133,c133),X4) )
| ~ spl63_1 ),
inference(resolution,[],[f85953,f20848]) ).
fof(f85955,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ val(X0,nelson_0)
| ~ val(X1,mandela_0)
| ~ sub(c133,X2)
| ~ sub(X0,eigenname_1_1)
| ~ sub(X1,familiename_1_1)
| ~ obj(X3,X4)
| ~ attr(X4,X0)
| ~ attr(X4,X1)
| ~ arg1(sK53(sK50(c133),c133,c133),X4) )
| ~ spl63_1 ),
inference(forward_subsumption_resolution,[],[f85954,f85920]) ).
fof(f85957,definition,
( spl63_3147
<=> ! [X4,X0,X3,X1] :
( ~ val(X0,nelson_0)
| ~ arg1(sK53(sK50(c133),c133,c133),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_3147])],[avatar_definition]) ).
fof(f85958,plain,
( ! [X3,X0,X1,X4] :
( ~ arg1(sK53(sK50(c133),c133,c133),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_3147 ),
inference(avatar_component_clause,[],[f85957]) ).
fof(f85959,plain,
( spl63_3069
| spl63_3147
| ~ spl63_1 ),
inference(avatar_split_clause,[],[f85955,f20847,f85957,f84359]) ).
fof(f85987,plain,
! [X0] :
( ~ arg1(sK50(c133),X0)
| arg1(sK53(sK50(c133),X0,c133),X0) ),
inference(resolution,[],[f84343,f84356]) ).
fof(f85988,plain,
arg1(sK53(sK50(c133),c133,c133),c133),
inference(resolution,[],[f85987,f84369]) ).
fof(f85989,plain,
( ! [X2,X0,X1] :
( ~ val(X0,nelson_0)
| ~ attr(c133,X1)
| ~ obj(X2,c133)
| ~ attr(c133,X0)
| ~ sub(X0,eigenname_1_1)
| ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1) )
| ~ spl63_3147 ),
inference(resolution,[],[f85988,f85958]) ).
fof(f85991,definition,
( spl63_3148
<=> ! [X2] : ~ obj(X2,c133) ),
introduced(definition,[new_symbols(definition,[spl63_3148])],[avatar_definition]) ).
fof(f85992,plain,
( ! [X2] : ~ obj(X2,c133)
| ~ spl63_3148 ),
inference(avatar_component_clause,[],[f85991]) ).
fof(f85994,definition,
( spl63_3149
<=> ! [X1] :
( ~ attr(c133,X1)
| ~ sub(X1,familiename_1_1)
| ~ val(X1,mandela_0) ) ),
introduced(definition,[new_symbols(definition,[spl63_3149])],[avatar_definition]) ).
fof(f85995,plain,
( ! [X1] :
( ~ val(X1,mandela_0)
| ~ sub(X1,familiename_1_1)
| ~ attr(c133,X1) )
| ~ spl63_3149 ),
inference(avatar_component_clause,[],[f85994]) ).
fof(f85997,definition,
( spl63_3150
<=> ! [X0] :
( ~ val(X0,nelson_0)
| ~ sub(X0,eigenname_1_1)
| ~ attr(c133,X0) ) ),
introduced(definition,[new_symbols(definition,[spl63_3150])],[avatar_definition]) ).
fof(f85998,plain,
( ! [X0] :
( ~ attr(c133,X0)
| ~ sub(X0,eigenname_1_1)
| ~ val(X0,nelson_0) )
| ~ spl63_3150 ),
inference(avatar_component_clause,[],[f85997]) ).
fof(f85999,plain,
( spl63_3148
| spl63_3149
| spl63_3150
| ~ spl63_3147 ),
inference(avatar_split_clause,[],[f85989,f85957,f85997,f85994,f85991]) ).
fof(f86000,plain,
( $false
| ~ spl63_3148 ),
inference(resolution,[],[f85992,f71943]) ).
fof(f86007,plain,
~ spl63_3148,
inference(avatar_contradiction_clause,[],[f86000]) ).
fof(f86008,plain,
( ~ sub(c135,familiename_1_1)
| ~ attr(c133,c135)
| ~ spl63_3149 ),
inference(resolution,[],[f85995,f20836]) ).
fof(f86009,plain,
( ~ attr(c133,c135)
| ~ spl63_3149 ),
inference(forward_subsumption_resolution,[],[f86008,f20837]) ).
fof(f86010,plain,
( $false
| ~ spl63_3149 ),
inference(forward_subsumption_resolution,[],[f86009,f20842]) ).
fof(f86011,plain,
~ spl63_3149,
inference(avatar_contradiction_clause,[],[f86010]) ).
fof(f86013,plain,
( ~ sub(c134,eigenname_1_1)
| ~ val(c134,nelson_0)
| ~ spl63_3150 ),
inference(resolution,[],[f85998,f20843]) ).
fof(f86014,plain,
( ~ val(c134,nelson_0)
| ~ spl63_3150 ),
inference(forward_subsumption_resolution,[],[f86013,f20839]) ).
fof(f86015,plain,
( $false
| ~ spl63_3150 ),
inference(forward_subsumption_resolution,[],[f86014,f20838]) ).
fof(f86016,plain,
~ spl63_3150,
inference(avatar_contradiction_clause,[],[f86015]) ).
fof(f86018,plain,
( $false
| ~ spl63_3069 ),
inference(resolution,[],[f84360,f20840]) ).
fof(f86019,plain,
~ spl63_3069,
inference(avatar_contradiction_clause,[],[f86018]) ).
cnf(s1,plain,
( spl63_1
| spl63_2 ),
inference(sat_conversion,[],[f20852]) ).
cnf(s42,plain,
~ spl63_2,
inference(sat_conversion,[],[f72153]) ).
cnf(s1114,plain,
( ~ spl63_1
| spl63_3069
| spl63_3147 ),
inference(sat_conversion,[],[f85959]) ).
cnf(s1115,plain,
( ~ spl63_3147
| spl63_3148
| spl63_3149
| spl63_3150 ),
inference(sat_conversion,[],[f85999]) ).
cnf(s1119,plain,
~ spl63_3148,
inference(sat_conversion,[],[f86007]) ).
cnf(s1120,plain,
~ spl63_3149,
inference(sat_conversion,[],[f86011]) ).
cnf(s1121,plain,
~ spl63_3150,
inference(sat_conversion,[],[f86016]) ).
cnf(s1122,plain,
~ spl63_3069,
inference(sat_conversion,[],[f86019]) ).
cnf(s1123,plain,
~ spl63_3147,
inference(rat,[],[s1115,s1121,s1120,s1119]) ).
cnf(s1124,plain,
~ spl63_1,
inference(rat,[],[s1114,s1123,s1122]) ).
cnf(s1125,plain,
$false,
inference(rat,[],[s1,s42,s1124]) ).
fof(f86020,plain,
$false,
inference(avatar_sat_refutation,[],[s1125]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+22 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n005.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:28:16 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 26.75/4.17 % (1276939)Will run a generic schedule for satisfiability detection.
% 26.75/4.17 % (1277006)% WARNING: option uhcvi not known.
% 26.75/4.17 % (1277006)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1513698333:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 26.75/4.17 % (1277005)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1898702645_2998 on theBenchmark for (2998ds/0Mi)
% 26.75/4.17 % (1277007)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2401533484:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 26.75/4.17 % (1277008)dis+10_1_sil=32000:sp=arity:random_seed=3696269279:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 26.75/4.17 % (1277009)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=848867418:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 26.75/4.17 % (1277010)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3271379175:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 26.75/4.17 % (1277011)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3218869684:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 26.75/4.17 % (1277008)Instruction limit reached!
% 26.75/4.17 % (1277008)------------------------------
% 26.75/4.17 % (1277008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.75/4.17 % (1277008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.75/4.17 % (1277008)CaDiCaL version: 2.1.3
% 26.75/4.17 % (1277008)Termination reason: Instruction limit
% 26.75/4.17 % (1277008)Termination phase: Saturation
% 26.75/4.17 % (1277008)Time elapsed: 0.060 s
% 26.75/4.17 % (1277008)Peak memory usage: 26 MB
% 26.75/4.17 % (1277008)Instructions burned: 105 (million)
% 26.75/4.17 % (1277009)Instruction limit reached!
% 26.75/4.17 % (1277009)------------------------------
% 26.75/4.17 % (1277009)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.75/4.17 % (1277009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.75/4.17 % (1277009)CaDiCaL version: 2.1.3
% 26.75/4.17 % (1277009)Termination reason: Instruction limit
% 26.75/4.17 % (1277009)Termination phase: Blocked clause elimination
% 26.75/4.17 % (1277009)Time elapsed: 0.073 s
% 26.75/4.17 % (1277009)Peak memory usage: 27 MB
% 26.75/4.17 % (1277009)Instructions burned: 116 (million)
% 26.75/4.17 % (1277010)Instruction limit reached!
% 26.75/4.17 % (1277010)------------------------------
% 26.75/4.17 % (1277010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.75/4.17 % (1277010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.75/4.17 % (1277010)CaDiCaL version: 2.1.3
% 26.75/4.17 % (1277010)Termination reason: Instruction limit
% 26.75/4.17 % (1277010)Termination phase: Saturation
% 26.75/4.17 % (1277010)Time elapsed: 0.074 s
% 26.75/4.17 % (1277010)Peak memory usage: 27 MB
% 26.75/4.17 % (1277010)Instructions burned: 132 (million)
% 26.75/4.17 % (1277019)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1036113893:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 26.75/4.17 % (1277020)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2333397126:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 26.75/4.17 % (1277011)Instruction limit reached!
% 26.75/4.17 % (1277011)------------------------------
% 26.75/4.17 % (1277011)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.75/4.17 % (1277011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.75/4.17 % (1277011)CaDiCaL version: 2.1.3
% 26.75/4.17 % (1277011)Termination reason: Instruction limit
% 26.75/4.17 % (1277011)Termination phase: Saturation
% 26.75/4.17 % (1277011)Time elapsed: 0.094 s
% 26.75/4.17 % (1277011)Peak memory usage: 30 MB
% 26.75/4.17 % (1277011)Instructions burned: 160 (million)
% 26.75/4.17 % (1277021)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=1502580115:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 26.75/4.17 % (1277025)ott-21_1_sil=16000:fs=off:random_seed=1015173147:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 26.75/4.17 % (1277020)Instruction limit reached!
% 26.75/4.17 % (1277020)------------------------------
% 26.75/4.17 % (1277020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.75/4.17 % (1277020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.89/7.46 % (1277020)CaDiCaL version: 2.1.3
% 49.89/7.46 % (1277020)Termination reason: Instruction limit
% 49.89/7.46 % (1277020)Termination phase: Blocked clause elimination
% 49.89/7.46 % (1277020)Time elapsed: 0.078 s
% 49.89/7.46 % (1277020)Peak memory usage: 28 MB
% 49.89/7.46 % (1277020)Instructions burned: 131 (million)
% 49.89/7.46 % (1277027)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3853962824:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 49.89/7.46 % (1277025)Instruction limit reached!
% 49.89/7.46 % (1277025)------------------------------
% 49.89/7.46 % (1277025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.89/7.46 % (1277025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.89/7.46 % (1277025)CaDiCaL version: 2.1.3
% 49.89/7.46 % (1277025)Termination reason: Instruction limit
% 49.89/7.46 % (1277025)Termination phase: Saturation
% 49.89/7.46 % (1277025)Time elapsed: 0.096 s
% 49.89/7.46 % (1277025)Peak memory usage: 28 MB
% 49.89/7.46 % (1277025)Instructions burned: 181 (million)
% 49.89/7.46 % (1277029)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=689849081:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 49.89/7.46 % TRYING [1]
% 49.89/7.46 % TRYING [1]
% 49.89/7.46 % TRYING [2]
% 49.89/7.46 % TRYING [2]
% 49.89/7.46 % (1277019)Instruction limit reached!
% 49.89/7.46 % (1277019)------------------------------
% 49.89/7.46 % (1277019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.89/7.46 % (1277019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.89/7.46 % (1277019)CaDiCaL version: 2.1.3
% 49.89/7.46 % (1277019)Termination reason: Instruction limit
% 49.89/7.46 % (1277019)Termination phase: Finite model building SAT solving
% 49.89/7.46 % (1277019)Time elapsed: 0.323 s
% 49.89/7.46 % (1277019)Peak memory usage: 54 MB
% 49.89/7.46 % (1277019)Instructions burned: 716 (million)
% 49.89/7.46 % (1277031)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2730200768:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 49.89/7.46 % TRYING [1]
% 49.89/7.46 % (1277027)Instruction limit reached!
% 49.89/7.46 % (1277027)------------------------------
% 49.89/7.46 % (1277027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.89/7.46 % (1277027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.89/7.46 % (1277027)CaDiCaL version: 2.1.3
% 49.89/7.46 % (1277027)Termination reason: Instruction limit
% 49.89/7.46 % (1277027)Termination phase: Saturation
% 49.89/7.46 % (1277027)Time elapsed: 0.251 s
% 49.89/7.46 % (1277027)Peak memory usage: 37 MB
% 49.89/7.46 % (1277027)Instructions burned: 478 (million)
% 49.89/7.46 % (1277021)Instruction limit reached!
% 49.89/7.46 % (1277021)------------------------------
% 49.89/7.46 % (1277021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.89/7.46 % (1277021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.89/7.46 % (1277021)CaDiCaL version: 2.1.3
% 49.89/7.46 % (1277021)Termination reason: Instruction limit
% 49.89/7.46 % (1277021)Termination phase: Saturation
% 49.89/7.46 % (1277021)Time elapsed: 0.355 s
% 49.89/7.46 % (1277021)Peak memory usage: 36 MB
% 49.89/7.46 % (1277021)Instructions burned: 684 (million)
% 49.89/7.46 % (1277033)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3294397606:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 49.89/7.46 % (1277034)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=825135445: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)
% 49.89/7.46 % TRYING [3]
% 49.89/7.46 % (1277029)Instruction limit reached!
% 49.89/7.46 % (1277029)------------------------------
% 49.89/7.46 % (1277029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.89/7.46 % (1277029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.89/7.46 % (1277029)CaDiCaL version: 2.1.3
% 49.89/7.46 % (1277029)Termination reason: Instruction limit
% 49.89/7.46 % (1277029)Termination phase: Finite model building SAT solving
% 49.89/7.46 % (1277029)Time elapsed: 0.321 s
% 49.89/7.46 % (1277029)Peak memory usage: 38 MB
% 49.89/7.46 % (1277029)Instructions burned: 868 (million)
% 49.89/7.46 % (1277037)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2356415800:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 49.89/7.46 % (1277034)Instruction limit reached!
% 49.89/7.46 % (1277034)------------------------------
% 49.89/7.46 % (1277034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.27/17.09 % (1277034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.27/17.09 % (1277034)CaDiCaL version: 2.1.3
% 118.27/17.09 % (1277034)Termination reason: Instruction limit
% 118.27/17.09 % (1277034)Termination phase: Saturation
% 118.27/17.09 % (1277034)Time elapsed: 0.361 s
% 118.27/17.09 % (1277034)Peak memory usage: 41 MB
% 118.27/17.09 % (1277034)Instructions burned: 694 (million)
% 118.27/17.09 % (1277039)fmb+10_1_sil=64000:random_seed=588540495:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 118.27/17.09 % (1277033)Instruction limit reached!
% 118.27/17.09 % (1277033)------------------------------
% 118.27/17.09 % (1277033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.27/17.09 % (1277033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.27/17.09 % (1277033)CaDiCaL version: 2.1.3
% 118.27/17.09 % (1277033)Termination reason: Instruction limit
% 118.27/17.09 % (1277033)Termination phase: Finite model building constraint generation
% 118.27/17.09 % (1277033)Time elapsed: 0.429 s
% 118.27/17.09 % (1277033)Peak memory usage: 90 MB
% 118.27/17.09 % (1277033)Instructions burned: 891 (million)
% 118.27/17.09 % (1277041)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2876514922:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 118.27/17.09 % (1277037)Instruction limit reached!
% 118.27/17.09 % (1277037)------------------------------
% 118.27/17.09 % (1277037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.27/17.09 % (1277037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.27/17.09 % (1277037)CaDiCaL version: 2.1.3
% 118.27/17.09 % (1277037)Termination reason: Instruction limit
% 118.27/17.09 % (1277037)Termination phase: Saturation
% 118.27/17.09 % (1277037)Time elapsed: 0.416 s
% 118.27/17.09 % (1277037)Peak memory usage: 43 MB
% 118.27/17.09 % (1277037)Instructions burned: 881 (million)
% 118.27/17.09 % (1277043)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1883054020:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 118.27/17.09 % (1277031)Instruction limit reached!
% 118.27/17.09 % (1277031)------------------------------
% 118.27/17.09 % (1277031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.27/17.09 % (1277031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.27/17.09 % (1277031)CaDiCaL version: 2.1.3
% 118.27/17.09 % (1277031)Termination reason: Instruction limit
% 118.27/17.09 % (1277031)Termination phase: Saturation
% 118.27/17.09 % (1277031)Time elapsed: 0.619 s
% 118.27/17.09 % (1277031)Peak memory usage: 54 MB
% 118.27/17.09 % (1277031)Instructions burned: 1180 (million)
% 118.27/17.09 % TRYING [1]
% 118.27/17.09 % (1277045)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1667034213:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 118.27/17.09 % TRYING [20]
% 118.27/17.09 % TRYING [8]
% 118.27/17.09 % (1277043)Instruction limit reached!
% 118.27/17.09 % (1277043)------------------------------
% 118.27/17.09 % (1277043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.27/17.09 % (1277043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.27/17.09 % (1277043)CaDiCaL version: 2.1.3
% 118.27/17.09 % (1277043)Termination reason: Instruction limit
% 118.27/17.09 % (1277043)Termination phase: Finite model building constraint generation
% 118.27/17.09 % (1277043)Time elapsed: 0.361 s
% 118.27/17.09 % (1277043)Peak memory usage: 64 MB
% 118.27/17.09 % (1277043)Instructions burned: 920 (million)
% 118.27/17.09 % (1277047)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=314191179:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 118.27/17.09 % TRYING [2]
% 118.27/17.09 % (1277047)Instruction limit reached!
% 118.27/17.09 % (1277047)------------------------------
% 118.27/17.09 % (1277047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 118.27/17.09 % (1277047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.27/17.09 % (1277047)CaDiCaL version: 2.1.3
% 118.27/17.09 % (1277047)Termination reason: Instruction limit
% 118.27/17.09 % (1277047)Termination phase: Saturation
% 118.27/17.09 % (1277047)Time elapsed: 0.680 s
% 118.27/17.09 % (1277047)Peak memory usage: 34 MB
% 118.27/17.09 % (1277047)Instructions burned: 1473 (million)
% 118.27/17.09 % TRYING [3]
% 118.27/17.09 % (1277049)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=710149669:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 118.27/17.09 % TRYING [77]
% 118.27/17.09 % TRYING [4]
% 118.27/17.09 % TRYING [4]
% 118.27/17.09 % (1277045)Instruction limit reached!
% 118.27/17.09 % (1277045)------------------------------
% 118.27/17.09 % (1277045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 256.34/36.50 % (1277045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 256.34/36.50 % (1277045)CaDiCaL version: 2.1.3
% 256.34/36.50 % (1277045)Termination reason: Instruction limit
% 256.34/36.50 % (1277045)Termination phase: Saturation
% 256.34/36.50 % (1277045)Time elapsed: 2.678 s
% 256.34/36.50 % (1277045)Peak memory usage: 39 MB
% 256.34/36.50 % (1277045)Instructions burned: 5131 (million)
% 256.34/36.50 % (1277051)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2316136625:fmbsr=2.30978:i=2174_2960 on theBenchmark for (2960ds/2174Mi)
% 256.34/36.50 % TRYING [16]
% 256.34/36.50 % (1277041)Instruction limit reached!
% 256.34/36.50 % (1277041)------------------------------
% 256.34/36.50 % (1277041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 256.34/36.50 % (1277041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 256.34/36.50 % (1277041)CaDiCaL version: 2.1.3
% 256.34/36.50 % (1277041)Termination reason: Instruction limit
% 256.34/36.50 % (1277041)Termination phase: Finite model building constraint generation
% 256.34/36.50 % (1277041)Time elapsed: 3.324 s
% 256.34/36.50 % (1277041)Peak memory usage: 551 MB
% 256.34/36.50 % (1277041)Instructions burned: 9516 (million)
% 256.34/36.50 % (1277053)ott-2_1_sil=16000:newcnf=on:random_seed=1592623059:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2954 on theBenchmark for (2954ds/869Mi)
% 256.34/36.50 % (1277049)Instruction limit reached!
% 256.34/36.50 % (1277049)------------------------------
% 256.34/36.50 % (1277049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 256.34/36.50 % (1277049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 256.34/36.50 % (1277049)CaDiCaL version: 2.1.3
% 256.34/36.50 % (1277049)Termination reason: Instruction limit
% 256.34/36.50 % (1277049)Termination phase: Finite model building constraint generation
% 256.34/36.50 % (1277049)Time elapsed: 2.247 s
% 256.34/36.50 % (1277049)Peak memory usage: 417 MB
% 256.34/36.50 % (1277049)Instructions burned: 6324 (million)
% 256.34/36.50 % (1277055)ott+10_1_sil=32000:tgt=ground:random_seed=1449025733:i=5114:av=off_2953 on theBenchmark for (2953ds/5114Mi)
% 256.34/36.50 % (1277051)Instruction limit reached!
% 256.34/36.50 % (1277051)------------------------------
% 256.34/36.50 % (1277051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 256.34/36.50 % (1277051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 256.34/36.50 % (1277051)CaDiCaL version: 2.1.3
% 256.34/36.50 % (1277051)Termination reason: Instruction limit
% 256.34/36.50 % (1277051)Termination phase: Finite model building constraint generation
% 256.34/36.50 % (1277051)Time elapsed: 0.768 s
% 256.34/36.50 % (1277051)Peak memory usage: 121 MB
% 256.34/36.50 % (1277051)Instructions burned: 2176 (million)
% 256.34/36.50 % (1277057)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1041977953:i=54282_2952 on theBenchmark for (2952ds/54282Mi)
% 256.34/36.50 % (1277053)Instruction limit reached!
% 256.34/36.50 % (1277053)------------------------------
% 256.34/36.50 % (1277053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 256.34/36.50 % (1277053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 256.34/36.50 % (1277053)CaDiCaL version: 2.1.3
% 256.34/36.50 % (1277053)Termination reason: Instruction limit
% 256.34/36.50 % (1277053)Termination phase: Saturation
% 256.34/36.50 % (1277053)Time elapsed: 0.398 s
% 256.34/36.50 % (1277053)Peak memory usage: 36 MB
% 256.34/36.50 % (1277053)Instructions burned: 872 (million)
% 256.34/36.50 % (1277059)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2323025227:i=3512:aac=none_2950 on theBenchmark for (2950ds/3512Mi)
% 256.34/36.50 % TRYING [1]
% 256.34/36.50 % TRYING [2]
% 256.34/36.50 % TRYING [3]
% 256.34/36.50 % TRYING [5]
% 256.34/36.50 % (1277059)Instruction limit reached!
% 256.34/36.50 % (1277059)------------------------------
% 256.34/36.50 % (1277059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 256.34/36.50 % (1277059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 256.34/36.50 % (1277059)CaDiCaL version: 2.1.3
% 256.34/36.50 % (1277059)Termination reason: Instruction limit
% 256.34/36.50 % (1277059)Termination phase: Saturation
% 256.34/36.50 % (1277059)Time elapsed: 1.741 s
% 256.34/36.50 % (1277059)Peak memory usage: 40 MB
% 256.34/36.50 % (1277059)Instructions burned: 3512 (million)
% 256.34/36.50 % (1277061)dis+21_1_sil=32000:sas=cadical:random_seed=815993856:i=3773:amm=off_2932 on theBenchmark for (2932ds/3773Mi)
% 256.34/36.50 % (1277055)Instruction limit reached!
% 256.34/36.50 % (1277055)------------------------------
% 256.34/36.50 % (1277055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277055)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277055)Termination reason: Instruction limit
% 202.08/42.63 % (1277055)Termination phase: Saturation
% 202.08/42.63 % (1277055)Time elapsed: 2.605 s
% 202.08/42.63 % (1277055)Peak memory usage: 120 MB
% 202.08/42.63 % (1277055)Instructions burned: 5115 (million)
% 202.08/42.63 % (1277063)ott+11_1_sil=16000:gs=on:random_seed=3717591935:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2927 on theBenchmark for (2927ds/2251Mi)
% 202.08/42.63 % TRYING [4]
% 202.08/42.63 % (1277063)Instruction limit reached!
% 202.08/42.63 % (1277063)------------------------------
% 202.08/42.63 % (1277063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277063)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277063)Termination reason: Instruction limit
% 202.08/42.63 % (1277063)Termination phase: Saturation
% 202.08/42.63 % (1277063)Time elapsed: 1.013 s
% 202.08/42.63 % (1277063)Peak memory usage: 34 MB
% 202.08/42.63 % (1277063)Instructions burned: 2252 (million)
% 202.08/42.63 % (1277065)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4155511397:fmbsr=1.6:i=67534_2917 on theBenchmark for (2917ds/67534Mi)
% 202.08/42.63 % (1277061)Instruction limit reached!
% 202.08/42.63 % (1277061)------------------------------
% 202.08/42.63 % (1277061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277061)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277061)Termination reason: Instruction limit
% 202.08/42.63 % (1277061)Termination phase: Saturation
% 202.08/42.63 % (1277061)Time elapsed: 1.618 s
% 202.08/42.63 % (1277061)Peak memory usage: 85 MB
% 202.08/42.63 % (1277061)Instructions burned: 3776 (million)
% 202.08/42.63 % (1277067)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3455122078:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2916 on theBenchmark for (2916ds/4591Mi)
% 202.08/42.63 % TRYING [7]
% 202.08/42.63 % TRYING [5]
% 202.08/42.63 % (1277067)Instruction limit reached!
% 202.08/42.63 % (1277067)------------------------------
% 202.08/42.63 % (1277067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277067)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277067)Termination reason: Instruction limit
% 202.08/42.63 % (1277067)Termination phase: Saturation
% 202.08/42.63 % (1277067)Time elapsed: 2.074 s
% 202.08/42.63 % (1277067)Peak memory usage: 46 MB
% 202.08/42.63 % (1277067)Instructions burned: 4593 (million)
% 202.08/42.63 % (1277069)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2715411738:i=29340_2895 on theBenchmark for (2895ds/29340Mi)
% 202.08/42.63 % (1277039)Instruction limit reached!
% 202.08/42.63 % (1277039)------------------------------
% 202.08/42.63 % (1277039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277039)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277039)Termination reason: Instruction limit
% 202.08/42.63 % (1277039)Termination phase: Finite model building SAT solving
% 202.08/42.63 % (1277039)Time elapsed: 9.731 s
% 202.08/42.63 % (1277039)Peak memory usage: 152 MB
% 202.08/42.63 % (1277039)Instructions burned: 22061 (million)
% 202.08/42.63 % (1277071)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3928905167:i=5211_2892 on theBenchmark for (2892ds/5211Mi)
% 202.08/42.63 % (1277071)Instruction limit reached!
% 202.08/42.63 % (1277071)------------------------------
% 202.08/42.63 % (1277071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277071)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277071)Termination reason: Instruction limit
% 202.08/42.63 % (1277071)Termination phase: Saturation
% 202.08/42.63 % (1277071)Time elapsed: 2.908 s
% 202.08/42.63 % (1277071)Peak memory usage: 52 MB
% 202.08/42.63 % (1277071)Instructions burned: 5212 (million)
% 202.08/42.63 % (1277074)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=796154802:i=5497:nm=2_2862 on theBenchmark for (2862ds/5497Mi)
% 202.08/42.63 % TRYING [17]
% 202.08/42.63 % (1277074)Instruction limit reached!
% 202.08/42.63 % (1277074)------------------------------
% 202.08/42.63 % (1277074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277074)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277074)Termination reason: Instruction limit
% 202.08/42.63 % (1277074)Termination phase: Finite model building constraint generation
% 202.08/42.63 % (1277074)Time elapsed: 3.109 s
% 202.08/42.63 % (1277074)Peak memory usage: 350 MB
% 202.08/42.63 % (1277074)Instructions burned: 5498 (million)
% 202.08/42.63 % (1277356)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1084242055:fmbsr=2:i=46332_2830 on theBenchmark for (2830ds/46332Mi)
% 202.08/42.63 % TRYING [15]
% 202.08/42.63 % TRYING [5]
% 202.08/42.63 % (1277069)Instruction limit reached!
% 202.08/42.63 % (1277069)------------------------------
% 202.08/42.63 % (1277069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277069)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277069)Termination reason: Instruction limit
% 202.08/42.63 % (1277069)Termination phase: Saturation
% 202.08/42.63 % (1277069)Time elapsed: 14.673 s
% 202.08/42.63 % (1277069)Peak memory usage: 83 MB
% 202.08/42.63 % (1277069)Instructions burned: 29341 (million)
% 202.08/42.63 % (1277358)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4268725971:i=14071_2748 on theBenchmark for (2748ds/14071Mi)
% 202.08/42.63 % TRYING [12]
% 202.08/42.63 % (1277007)Instruction limit reached!
% 202.08/42.63 % (1277007)------------------------------
% 202.08/42.63 % (1277007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277007)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277007)Termination reason: Instruction limit
% 202.08/42.63 % (1277007)Termination phase: Saturation
% 202.08/42.63 % (1277007)Time elapsed: 31.324 s
% 202.08/42.63 % (1277007)Peak memory usage: 165 MB
% 202.08/42.63 % (1277007)Instructions burned: 88026 (million)
% 202.08/42.63 % (1277360)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1941377768:i=22565:add=on:rawr=on_2684 on theBenchmark for (2684ds/22565Mi)
% 202.08/42.63 % (1277057)Instruction limit reached!
% 202.08/42.63 % (1277057)------------------------------
% 202.08/42.63 % (1277057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277057)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277057)Termination reason: Instruction limit
% 202.08/42.63 % (1277057)Termination phase: Finite model building SAT solving
% 202.08/42.63 % (1277057)Time elapsed: 26.915 s
% 202.08/42.63 % (1277057)Peak memory usage: 235 MB
% 202.08/42.63 % (1277057)Instructions burned: 54284 (million)
% 202.08/42.63 % (1277362)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1882026488:i=8173:av=off_2682 on theBenchmark for (2682ds/8173Mi)
% 202.08/42.63 % (1277358)Instruction limit reached!
% 202.08/42.63 % (1277358)------------------------------
% 202.08/42.63 % (1277358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277358)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277358)Termination reason: Instruction limit
% 202.08/42.63 % (1277358)Termination phase: Finite model building constraint generation
% 202.08/42.63 % (1277358)Time elapsed: 6.547 s
% 202.08/42.63 % (1277358)Peak memory usage: 1122 MB
% 202.08/42.63 % (1277358)Instructions burned: 14072 (million)
% 202.08/42.63 % (1277364)dis+10_16:1_sil=16000:random_seed=3282985718:i=9155:fsr=off_2681 on theBenchmark for (2681ds/9155Mi)
% 202.08/42.63 % TRYING [6]
% 202.08/42.63 % (1277364)Instruction limit reached!
% 202.08/42.63 % (1277364)------------------------------
% 202.08/42.63 % (1277364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277364)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277364)Termination reason: Instruction limit
% 202.08/42.63 % (1277364)Termination phase: Saturation
% 202.08/42.63 % (1277364)Time elapsed: 3.747 s
% 202.08/42.63 % (1277364)Peak memory usage: 82 MB
% 202.08/42.63 % (1277364)Instructions burned: 9155 (million)
% 202.08/42.63 % (1277366)ott-3_8_sil=64000:random_seed=145398096:i=20139:bs=on_2643 on theBenchmark for (2643ds/20139Mi)
% 202.08/42.63 % (1277362)Instruction limit reached!
% 202.08/42.63 % (1277362)------------------------------
% 202.08/42.63 % (1277362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277362)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277362)Termination reason: Instruction limit
% 202.08/42.63 % (1277362)Termination phase: Saturation
% 202.08/42.63 % (1277362)Time elapsed: 4.541 s
% 202.08/42.63 % (1277362)Peak memory usage: 191 MB
% 202.08/42.63 % (1277362)Instructions burned: 8174 (million)
% 202.08/42.63 % (1277368)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1240481330:fmbsr=2:i=32576_2637 on theBenchmark for (2637ds/32576Mi)
% 202.08/42.63 % TRYING [9]
% 202.08/42.63 % (1277356)Instruction limit reached!
% 202.08/42.63 % (1277356)------------------------------
% 202.08/42.63 % (1277356)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277356)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277356)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277356)Termination reason: Instruction limit
% 202.08/42.63 % (1277356)Termination phase: Finite model building constraint generation
% 202.08/42.63 % (1277356)Time elapsed: 21.931 s
% 202.08/42.63 % (1277356)Peak memory usage: 3366 MB
% 202.08/42.63 % (1277356)Instructions burned: 46332 (million)
% 202.08/42.63 % (1277370)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=93125365:i=11404_2607 on theBenchmark for (2607ds/11404Mi)
% 202.08/42.63 % (1277065)Instruction limit reached!
% 202.08/42.63 % (1277065)------------------------------
% 202.08/42.63 % (1277065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277065)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277065)Termination reason: Instruction limit
% 202.08/42.63 % (1277065)Termination phase: Finite model building SAT solving
% 202.08/42.63 % (1277065)Time elapsed: 31.251 s
% 202.08/42.63 % (1277065)Peak memory usage: 292 MB
% 202.08/42.63 % (1277065)Instructions burned: 67535 (million)
% 202.08/42.63 % (1277372)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=943161640:i=14134_2603 on theBenchmark for (2603ds/14134Mi)
% 202.08/42.63 % (1277360)Instruction limit reached!
% 202.08/42.63 % (1277360)------------------------------
% 202.08/42.63 % (1277360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.63 % (1277360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.63 % (1277360)CaDiCaL version: 2.1.3
% 202.08/42.63 % (1277360)Termination reason: Instruction limit
% 202.08/42.63 % (1277360)Termination phase: Saturation
% 202.08/42.63 % (1277360)Time elapsed: 8.203 s
% 202.08/42.63 % (1277360)Peak memory usage: 117 MB
% 202.08/42.63 % (1277360)Instructions burned: 22566 (million)
% 202.08/42.63 % (1277374)dis+33_16_sil=32000:sac=on:random_seed=848722915:i=15851:nm=0_2602 on theBenchmark for (2602ds/15851Mi)
% 202.08/42.63 % (1277374) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1276939-1277374"...
% 202.08/42.63 % (1277374)...printing done.
% 202.08/42.63 % (1277374)Refutation found. Thanks to Tanya!
% 202.08/42.63 % SZS status Theorem for theBenchmark
% 202.08/42.63 % SZS output start Proof for theBenchmark
% See solution above
% 202.08/42.65 % (1277374)------------------------------
% 202.08/42.65 % (1277374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 202.08/42.65 % (1277374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.08/42.65 % (1277374)CaDiCaL version: 2.1.3
% 202.08/42.65 % (1277374)Termination reason: Refutation
% 202.08/42.65 % (1277374)Time elapsed: 2.463 s
% 202.08/42.65 % (1277374)Peak memory usage: 79 MB
% 202.08/42.65 % (1277374)Instructions burned: 5227 (million)
% 202.08/42.65 % (1276939)Success in time 42.405 s
% 202.08/42.65 % Vampire exiting
%------------------------------------------------------------------------------