%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR116+16 : 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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:45:48 AM UTC 2026
% Result : Theorem 147.60s 36.42s
% Output : Refutation 147.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 12
% Syntax : Number of formulae : 111 ( 20 unt; 4 def)
% Number of atoms : 1394 ( 0 equ)
% Maximal formula atoms : 124 ( 12 avg)
% Number of connectives : 1595 ( 312 ~; 268 |;1006 &)
% ( 4 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 124 ( 16 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 36 ( 35 usr; 5 prp; 0-2 aty)
% Number of functors : 56 ( 56 usr; 48 con; 0-3 aty)
% Number of variables : 265 ( 0 sgn 222 !; 43 ?)
% Comments :
%------------------------------------------------------------------------------
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(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/sandbox/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/sandbox/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/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_1726) ).
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,
( attr(c18,c19)
& attr(c18,c20)
& prop(c18,s__374dafrikanisch_1_1)
& sub(c18,pr__344sident_1_1)
& sub(c19,eigenname_1_1)
& val(c19,nelson_0)
& sub(c20,familiename_1_1)
& val(c20,mandela_0)
& agt(c28,c292)
& subs(c28,besuch_1_1)
& circ(c31,c9)
& exp(c31,c292)
& mannr(c31,c1)
& subs(c31,zeigen_1_4)
& attch(c9,c18)
& ornt(c9,c28)
& prop(c9,hoch_1_1)
& reas(c9,c31)
& subs(c9,interesse_1_1)
& chsp2(erfreuen_1_2,c1)
& sort(c18,d)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,det)
& varia(c18,con)
& sort(c19,na)
& card(c19,int1)
& etype(c19,int0)
& fact(c19,real)
& gener(c19,sp)
& quant(c19,one)
& refer(c19,indet)
& varia(c19,varia_c)
& sort(c20,na)
& card(c20,int1)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& quant(c20,one)
& refer(c20,indet)
& varia(c20,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(c28,ad)
& sort(c28,as)
& card(c28,int1)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& quant(c28,one)
& refer(c28,det)
& varia(c28,varia_c)
& sort(c292,o)
& card(c292,int1)
& etype(c292,int0)
& fact(c292,real)
& gener(c292,sp)
& quant(c292,one)
& refer(c292,det)
& varia(c292,varia_c)
& sort(besuch_1_1,ad)
& sort(besuch_1_1,as)
& card(besuch_1_1,int1)
& etype(besuch_1_1,int0)
& fact(besuch_1_1,real)
& gener(besuch_1_1,ge)
& quant(besuch_1_1,one)
& refer(besuch_1_1,refer_c)
& varia(besuch_1_1,varia_c)
& sort(c31,dn)
& fact(c31,real)
& gener(c31,sp)
& sort(c9,as)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& quant(c9,one)
& refer(c9,det)
& varia(c9,con)
& sort(c1,tq)
& sort(zeigen_1_4,dn)
& fact(zeigen_1_4,real)
& gener(zeigen_1_4,ge)
& sort(hoch_1_1,mq)
& sort(interesse_1_1,as)
& card(interesse_1_1,int1)
& etype(interesse_1_1,int0)
& fact(interesse_1_1,real)
& gener(interesse_1_1,ge)
& quant(interesse_1_1,one)
& refer(interesse_1_1,refer_c)
& varia(interesse_1_1,varia_c)
& sort(erfreuen_1_2,da)
& fact(erfreuen_1_2,real)
& gener(erfreuen_1_2,ge) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ave07_era5_synth_qa07_010_mira_news_1726) ).
fof(f10191,plain,
( attr(c18,c19)
& attr(c18,c20)
& prop(c18,s__374dafrikanisch_1_1)
& sub(c18,pr__344sident_1_1)
& sub(c19,eigenname_1_1)
& val(c19,nelson_0)
& sub(c20,familiename_1_1)
& val(c20,mandela_0)
& agt(c28,c292)
& subs(c28,besuch_1_1)
& circ(c31,c9)
& exp(c31,c292)
& mannr(c31,c1)
& subs(c31,zeigen_1_4)
& attch(c9,c18)
& ornt(c9,c28)
& prop(c9,hoch_1_1)
& subs(c9,interesse_1_1)
& chsp2(erfreuen_1_2,c1)
& sort(c18,d)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,det)
& varia(c18,con)
& sort(c19,na)
& card(c19,int1)
& etype(c19,int0)
& fact(c19,real)
& gener(c19,sp)
& quant(c19,one)
& refer(c19,indet)
& varia(c19,varia_c)
& sort(c20,na)
& card(c20,int1)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& quant(c20,one)
& refer(c20,indet)
& varia(c20,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(c28,ad)
& sort(c28,as)
& card(c28,int1)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& quant(c28,one)
& refer(c28,det)
& varia(c28,varia_c)
& sort(c292,o)
& card(c292,int1)
& etype(c292,int0)
& fact(c292,real)
& gener(c292,sp)
& quant(c292,one)
& refer(c292,det)
& varia(c292,varia_c)
& sort(besuch_1_1,ad)
& sort(besuch_1_1,as)
& card(besuch_1_1,int1)
& etype(besuch_1_1,int0)
& fact(besuch_1_1,real)
& gener(besuch_1_1,ge)
& quant(besuch_1_1,one)
& refer(besuch_1_1,refer_c)
& varia(besuch_1_1,varia_c)
& sort(c31,dn)
& fact(c31,real)
& gener(c31,sp)
& sort(c9,as)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& quant(c9,one)
& refer(c9,det)
& varia(c9,con)
& sort(c1,tq)
& sort(zeigen_1_4,dn)
& fact(zeigen_1_4,real)
& gener(zeigen_1_4,ge)
& sort(hoch_1_1,mq)
& sort(interesse_1_1,as)
& card(interesse_1_1,int1)
& etype(interesse_1_1,int0)
& fact(interesse_1_1,real)
& gener(interesse_1_1,ge)
& quant(interesse_1_1,one)
& refer(interesse_1_1,refer_c)
& varia(interesse_1_1,varia_c)
& sort(erfreuen_1_2,da)
& fact(erfreuen_1_2,real)
& gener(erfreuen_1_2,ge) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10192,plain,
( attr(c18,c19)
& attr(c18,c20)
& prop(c18,s__374dafrikanisch_1_1)
& sub(c18,pr__344sident_1_1)
& sub(c19,eigenname_1_1)
& val(c19,nelson_0)
& sub(c20,familiename_1_1)
& val(c20,mandela_0)
& agt(c28,c292)
& subs(c28,besuch_1_1)
& circ(c31,c9)
& exp(c31,c292)
& subs(c31,zeigen_1_4)
& attch(c9,c18)
& ornt(c9,c28)
& prop(c9,hoch_1_1)
& subs(c9,interesse_1_1)
& chsp2(erfreuen_1_2,c1)
& sort(c18,d)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,det)
& varia(c18,con)
& sort(c19,na)
& card(c19,int1)
& etype(c19,int0)
& fact(c19,real)
& gener(c19,sp)
& quant(c19,one)
& refer(c19,indet)
& varia(c19,varia_c)
& sort(c20,na)
& card(c20,int1)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& quant(c20,one)
& refer(c20,indet)
& varia(c20,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(c28,ad)
& sort(c28,as)
& card(c28,int1)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& quant(c28,one)
& refer(c28,det)
& varia(c28,varia_c)
& sort(c292,o)
& card(c292,int1)
& etype(c292,int0)
& fact(c292,real)
& gener(c292,sp)
& quant(c292,one)
& refer(c292,det)
& varia(c292,varia_c)
& sort(besuch_1_1,ad)
& sort(besuch_1_1,as)
& card(besuch_1_1,int1)
& etype(besuch_1_1,int0)
& fact(besuch_1_1,real)
& gener(besuch_1_1,ge)
& quant(besuch_1_1,one)
& refer(besuch_1_1,refer_c)
& varia(besuch_1_1,varia_c)
& sort(c31,dn)
& fact(c31,real)
& gener(c31,sp)
& sort(c9,as)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& quant(c9,one)
& refer(c9,det)
& varia(c9,con)
& sort(c1,tq)
& sort(zeigen_1_4,dn)
& fact(zeigen_1_4,real)
& gener(zeigen_1_4,ge)
& sort(hoch_1_1,mq)
& sort(interesse_1_1,as)
& card(interesse_1_1,int1)
& etype(interesse_1_1,int0)
& fact(interesse_1_1,real)
& gener(interesse_1_1,ge)
& quant(interesse_1_1,one)
& refer(interesse_1_1,refer_c)
& varia(interesse_1_1,varia_c)
& sort(erfreuen_1_2,da)
& fact(erfreuen_1_2,real)
& gener(erfreuen_1_2,ge) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10323,plain,
( attr(c18,c19)
& attr(c18,c20)
& prop(c18,s__374dafrikanisch_1_1)
& sub(c18,pr__344sident_1_1)
& sub(c19,eigenname_1_1)
& val(c19,nelson_0)
& sub(c20,familiename_1_1)
& val(c20,mandela_0)
& agt(c28,c292)
& subs(c28,besuch_1_1)
& circ(c31,c9)
& exp(c31,c292)
& subs(c31,zeigen_1_4)
& attch(c9,c18)
& ornt(c9,c28)
& prop(c9,hoch_1_1)
& subs(c9,interesse_1_1)
& sort(c18,d)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,det)
& varia(c18,con)
& sort(c19,na)
& card(c19,int1)
& etype(c19,int0)
& fact(c19,real)
& gener(c19,sp)
& quant(c19,one)
& refer(c19,indet)
& varia(c19,varia_c)
& sort(c20,na)
& card(c20,int1)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& quant(c20,one)
& refer(c20,indet)
& varia(c20,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(c28,ad)
& sort(c28,as)
& card(c28,int1)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& quant(c28,one)
& refer(c28,det)
& varia(c28,varia_c)
& sort(c292,o)
& card(c292,int1)
& etype(c292,int0)
& fact(c292,real)
& gener(c292,sp)
& quant(c292,one)
& refer(c292,det)
& varia(c292,varia_c)
& sort(besuch_1_1,ad)
& sort(besuch_1_1,as)
& card(besuch_1_1,int1)
& etype(besuch_1_1,int0)
& fact(besuch_1_1,real)
& gener(besuch_1_1,ge)
& quant(besuch_1_1,one)
& refer(besuch_1_1,refer_c)
& varia(besuch_1_1,varia_c)
& sort(c31,dn)
& fact(c31,real)
& gener(c31,sp)
& sort(c9,as)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& quant(c9,one)
& refer(c9,det)
& varia(c9,con)
& sort(c1,tq)
& sort(zeigen_1_4,dn)
& fact(zeigen_1_4,real)
& gener(zeigen_1_4,ge)
& sort(hoch_1_1,mq)
& sort(interesse_1_1,as)
& card(interesse_1_1,int1)
& etype(interesse_1_1,int0)
& fact(interesse_1_1,real)
& gener(interesse_1_1,ge)
& quant(interesse_1_1,one)
& refer(interesse_1_1,refer_c)
& varia(interesse_1_1,varia_c)
& sort(erfreuen_1_2,da)
& fact(erfreuen_1_2,real)
& gener(erfreuen_1_2,ge) ),
inference(pure_predicate_removal,[],[f10192]) ).
fof(f10329,plain,
( attr(c18,c19)
& attr(c18,c20)
& prop(c18,s__374dafrikanisch_1_1)
& sub(c18,pr__344sident_1_1)
& sub(c19,eigenname_1_1)
& val(c19,nelson_0)
& sub(c20,familiename_1_1)
& val(c20,mandela_0)
& agt(c28,c292)
& subs(c28,besuch_1_1)
& circ(c31,c9)
& exp(c31,c292)
& subs(c31,zeigen_1_4)
& attch(c9,c18)
& ornt(c9,c28)
& prop(c9,hoch_1_1)
& subs(c9,interesse_1_1)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& quant(c18,one)
& refer(c18,det)
& varia(c18,con)
& card(c19,int1)
& etype(c19,int0)
& fact(c19,real)
& gener(c19,sp)
& quant(c19,one)
& refer(c19,indet)
& varia(c19,varia_c)
& card(c20,int1)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& quant(c20,one)
& refer(c20,indet)
& varia(c20,varia_c)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& quant(pr__344sident_1_1,one)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& quant(eigenname_1_1,one)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& quant(familiename_1_1,one)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& card(c28,int1)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& quant(c28,one)
& refer(c28,det)
& varia(c28,varia_c)
& card(c292,int1)
& etype(c292,int0)
& fact(c292,real)
& gener(c292,sp)
& quant(c292,one)
& refer(c292,det)
& varia(c292,varia_c)
& card(besuch_1_1,int1)
& etype(besuch_1_1,int0)
& fact(besuch_1_1,real)
& gener(besuch_1_1,ge)
& quant(besuch_1_1,one)
& refer(besuch_1_1,refer_c)
& varia(besuch_1_1,varia_c)
& fact(c31,real)
& gener(c31,sp)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& quant(c9,one)
& refer(c9,det)
& varia(c9,con)
& fact(zeigen_1_4,real)
& gener(zeigen_1_4,ge)
& card(interesse_1_1,int1)
& etype(interesse_1_1,int0)
& fact(interesse_1_1,real)
& gener(interesse_1_1,ge)
& quant(interesse_1_1,one)
& refer(interesse_1_1,refer_c)
& varia(interesse_1_1,varia_c)
& fact(erfreuen_1_2,real)
& gener(erfreuen_1_2,ge) ),
inference(pure_predicate_removal,[],[f10323]) ).
fof(f10332,plain,
( attr(c18,c19)
& attr(c18,c20)
& prop(c18,s__374dafrikanisch_1_1)
& sub(c18,pr__344sident_1_1)
& sub(c19,eigenname_1_1)
& val(c19,nelson_0)
& sub(c20,familiename_1_1)
& val(c20,mandela_0)
& agt(c28,c292)
& subs(c28,besuch_1_1)
& circ(c31,c9)
& exp(c31,c292)
& subs(c31,zeigen_1_4)
& attch(c9,c18)
& ornt(c9,c28)
& prop(c9,hoch_1_1)
& subs(c9,interesse_1_1)
& card(c18,int1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& refer(c18,det)
& varia(c18,con)
& card(c19,int1)
& etype(c19,int0)
& fact(c19,real)
& gener(c19,sp)
& refer(c19,indet)
& varia(c19,varia_c)
& card(c20,int1)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& refer(c20,indet)
& varia(c20,varia_c)
& card(pr__344sident_1_1,int1)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& card(eigenname_1_1,int1)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& card(familiename_1_1,int1)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& card(c28,int1)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& refer(c28,det)
& varia(c28,varia_c)
& card(c292,int1)
& etype(c292,int0)
& fact(c292,real)
& gener(c292,sp)
& refer(c292,det)
& varia(c292,varia_c)
& card(besuch_1_1,int1)
& etype(besuch_1_1,int0)
& fact(besuch_1_1,real)
& gener(besuch_1_1,ge)
& refer(besuch_1_1,refer_c)
& varia(besuch_1_1,varia_c)
& fact(c31,real)
& gener(c31,sp)
& card(c9,int1)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& refer(c9,det)
& varia(c9,con)
& fact(zeigen_1_4,real)
& gener(zeigen_1_4,ge)
& card(interesse_1_1,int1)
& etype(interesse_1_1,int0)
& fact(interesse_1_1,real)
& gener(interesse_1_1,ge)
& refer(interesse_1_1,refer_c)
& varia(interesse_1_1,varia_c)
& fact(erfreuen_1_2,real)
& gener(erfreuen_1_2,ge) ),
inference(pure_predicate_removal,[],[f10329]) ).
fof(f10335,plain,
( attr(c18,c19)
& attr(c18,c20)
& prop(c18,s__374dafrikanisch_1_1)
& sub(c18,pr__344sident_1_1)
& sub(c19,eigenname_1_1)
& val(c19,nelson_0)
& sub(c20,familiename_1_1)
& val(c20,mandela_0)
& agt(c28,c292)
& subs(c28,besuch_1_1)
& circ(c31,c9)
& exp(c31,c292)
& subs(c31,zeigen_1_4)
& attch(c9,c18)
& ornt(c9,c28)
& prop(c9,hoch_1_1)
& subs(c9,interesse_1_1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& refer(c18,det)
& varia(c18,con)
& etype(c19,int0)
& fact(c19,real)
& gener(c19,sp)
& refer(c19,indet)
& varia(c19,varia_c)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& refer(c20,indet)
& varia(c20,varia_c)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& refer(pr__344sident_1_1,refer_c)
& varia(pr__344sident_1_1,varia_c)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& refer(eigenname_1_1,refer_c)
& varia(eigenname_1_1,varia_c)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& refer(familiename_1_1,refer_c)
& varia(familiename_1_1,varia_c)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& refer(c28,det)
& varia(c28,varia_c)
& etype(c292,int0)
& fact(c292,real)
& gener(c292,sp)
& refer(c292,det)
& varia(c292,varia_c)
& etype(besuch_1_1,int0)
& fact(besuch_1_1,real)
& gener(besuch_1_1,ge)
& refer(besuch_1_1,refer_c)
& varia(besuch_1_1,varia_c)
& fact(c31,real)
& gener(c31,sp)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& refer(c9,det)
& varia(c9,con)
& fact(zeigen_1_4,real)
& gener(zeigen_1_4,ge)
& etype(interesse_1_1,int0)
& fact(interesse_1_1,real)
& gener(interesse_1_1,ge)
& refer(interesse_1_1,refer_c)
& varia(interesse_1_1,varia_c)
& fact(erfreuen_1_2,real)
& gener(erfreuen_1_2,ge) ),
inference(pure_predicate_removal,[],[f10332]) ).
fof(f10338,plain,
( attr(c18,c19)
& attr(c18,c20)
& prop(c18,s__374dafrikanisch_1_1)
& sub(c18,pr__344sident_1_1)
& sub(c19,eigenname_1_1)
& val(c19,nelson_0)
& sub(c20,familiename_1_1)
& val(c20,mandela_0)
& agt(c28,c292)
& subs(c28,besuch_1_1)
& circ(c31,c9)
& exp(c31,c292)
& subs(c31,zeigen_1_4)
& attch(c9,c18)
& ornt(c9,c28)
& prop(c9,hoch_1_1)
& subs(c9,interesse_1_1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& varia(c18,con)
& etype(c19,int0)
& fact(c19,real)
& gener(c19,sp)
& varia(c19,varia_c)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& varia(c20,varia_c)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& varia(pr__344sident_1_1,varia_c)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& varia(eigenname_1_1,varia_c)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& varia(familiename_1_1,varia_c)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& varia(c28,varia_c)
& etype(c292,int0)
& fact(c292,real)
& gener(c292,sp)
& varia(c292,varia_c)
& etype(besuch_1_1,int0)
& fact(besuch_1_1,real)
& gener(besuch_1_1,ge)
& varia(besuch_1_1,varia_c)
& fact(c31,real)
& gener(c31,sp)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& varia(c9,con)
& fact(zeigen_1_4,real)
& gener(zeigen_1_4,ge)
& etype(interesse_1_1,int0)
& fact(interesse_1_1,real)
& gener(interesse_1_1,ge)
& varia(interesse_1_1,varia_c)
& fact(erfreuen_1_2,real)
& gener(erfreuen_1_2,ge) ),
inference(pure_predicate_removal,[],[f10335]) ).
fof(f10343,plain,
( attr(c18,c19)
& attr(c18,c20)
& prop(c18,s__374dafrikanisch_1_1)
& sub(c18,pr__344sident_1_1)
& sub(c19,eigenname_1_1)
& val(c19,nelson_0)
& sub(c20,familiename_1_1)
& val(c20,mandela_0)
& agt(c28,c292)
& subs(c28,besuch_1_1)
& circ(c31,c9)
& exp(c31,c292)
& subs(c31,zeigen_1_4)
& attch(c9,c18)
& ornt(c9,c28)
& prop(c9,hoch_1_1)
& subs(c9,interesse_1_1)
& etype(c18,int0)
& fact(c18,real)
& gener(c18,sp)
& etype(c19,int0)
& fact(c19,real)
& gener(c19,sp)
& etype(c20,int0)
& fact(c20,real)
& gener(c20,sp)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& gener(pr__344sident_1_1,ge)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& gener(eigenname_1_1,ge)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& etype(c28,int0)
& fact(c28,real)
& gener(c28,sp)
& etype(c292,int0)
& fact(c292,real)
& gener(c292,sp)
& etype(besuch_1_1,int0)
& fact(besuch_1_1,real)
& gener(besuch_1_1,ge)
& fact(c31,real)
& gener(c31,sp)
& etype(c9,int0)
& fact(c9,real)
& gener(c9,sp)
& fact(zeigen_1_4,real)
& gener(zeigen_1_4,ge)
& etype(interesse_1_1,int0)
& fact(interesse_1_1,real)
& gener(interesse_1_1,ge)
& fact(erfreuen_1_2,real)
& gener(erfreuen_1_2,ge) ),
inference(pure_predicate_removal,[],[f10338]) ).
fof(f10348,plain,
( attr(c18,c19)
& attr(c18,c20)
& prop(c18,s__374dafrikanisch_1_1)
& sub(c18,pr__344sident_1_1)
& sub(c19,eigenname_1_1)
& val(c19,nelson_0)
& sub(c20,familiename_1_1)
& val(c20,mandela_0)
& agt(c28,c292)
& subs(c28,besuch_1_1)
& circ(c31,c9)
& exp(c31,c292)
& subs(c31,zeigen_1_4)
& attch(c9,c18)
& ornt(c9,c28)
& prop(c9,hoch_1_1)
& subs(c9,interesse_1_1)
& etype(c18,int0)
& fact(c18,real)
& etype(c19,int0)
& fact(c19,real)
& etype(c20,int0)
& fact(c20,real)
& etype(pr__344sident_1_1,int0)
& fact(pr__344sident_1_1,real)
& etype(eigenname_1_1,int0)
& fact(eigenname_1_1,real)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& etype(c28,int0)
& fact(c28,real)
& etype(c292,int0)
& fact(c292,real)
& etype(besuch_1_1,int0)
& fact(besuch_1_1,real)
& fact(c31,real)
& etype(c9,int0)
& fact(c9,real)
& fact(zeigen_1_4,real)
& etype(interesse_1_1,int0)
& fact(interesse_1_1,real)
& fact(erfreuen_1_2,real) ),
inference(pure_predicate_removal,[],[f10343]) ).
fof(f10352,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(ennf_transformation,[],[f11]) ).
fof(f10401,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(f10402,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,[],[f10401]) ).
fof(f10510,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(f10511,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,[],[f10510]) ).
fof(f10522,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(f10523,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,[],[f10522]) ).
fof(f10524,plain,
! [X0,X1] :
( ? [X2] :
( arg1(X2,X0)
& arg2(X2,X1)
& subr(X2,sub_0) )
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f163]) ).
fof(f10553,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(f10558,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))],[f10402]) ).
fof(f10593,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))],[f10511]) ).
fof(f10597,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))],[f10523]) ).
fof(f10598,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))],[f10524]) ).
fof(f10608,plain,
! [X0,X1] :
( has_fact_leq(X0,X1)
| ~ fact(X0,X1) ),
inference(cnf_transformation,[],[f10352]) ).
fof(f10692,plain,
! [X0,X1] :
( obj(sK3(X0,X1),X1)
| ~ has_fact_leq(X1,real)
| ~ loc(X1,X0) ),
inference(cnf_transformation,[],[f10558]) ).
fof(f10858,plain,
! [X2,X0,X1] :
( val(sK49(X0,X2),X2)
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10593]) ).
fof(f10859,plain,
! [X2,X0,X1] :
( sub(sK49(X0,X2),name_1_1)
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10593]) ).
fof(f10861,plain,
! [X2,X0,X1] :
( loc(X0,sK50(X0,X2))
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10593]) ).
fof(f10862,plain,
! [X2,X0,X1] :
( attr(sK48(X0,X2),sK49(X0,X2))
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10593]) ).
fof(f10863,plain,
! [X2,X0,X1] :
( in(sK50(X0,X2),sK48(X0,X2))
| ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,X2) ),
inference(cnf_transformation,[],[f10593]) ).
fof(f10881,plain,
! [X2,X0,X1] :
( subr(sK56(X0,X1,X2),rprs_0)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10597]) ).
fof(f10882,plain,
! [X2,X0,X1] :
( sub(sK57(X0,X1,X2),X2)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10597]) ).
fof(f10886,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,[],[f10597]) ).
fof(f10887,plain,
! [X2,X0,X1] :
( arg1(sK56(X0,X1,X2),X1)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) ),
inference(cnf_transformation,[],[f10597]) ).
fof(f10888,plain,
! [X0,X1] :
( subr(sK58(X0,X1),sub_0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10598]) ).
fof(f10889,plain,
! [X0,X1] :
( arg2(sK58(X0,X1),X1)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10598]) ).
fof(f10890,plain,
! [X0,X1] :
( arg1(sK58(X0,X1),X0)
| ~ sub(X0,X1) ),
inference(cnf_transformation,[],[f10598]) ).
fof(f19790,plain,
state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0),
inference(cnf_transformation,[],[f9161]) ).
fof(f20817,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,[],[f10553]) ).
fof(f20841,plain,
fact(c18,real),
inference(cnf_transformation,[],[f10348]) ).
fof(f20852,plain,
val(c20,mandela_0),
inference(cnf_transformation,[],[f10348]) ).
fof(f20853,plain,
sub(c20,familiename_1_1),
inference(cnf_transformation,[],[f10348]) ).
fof(f20854,plain,
val(c19,nelson_0),
inference(cnf_transformation,[],[f10348]) ).
fof(f20855,plain,
sub(c19,eigenname_1_1),
inference(cnf_transformation,[],[f10348]) ).
fof(f20856,plain,
sub(c18,pr__344sident_1_1),
inference(cnf_transformation,[],[f10348]) ).
fof(f20857,plain,
prop(c18,s__374dafrikanisch_1_1),
inference(cnf_transformation,[],[f10348]) ).
fof(f20858,plain,
attr(c18,c20),
inference(cnf_transformation,[],[f10348]) ).
fof(f20859,plain,
attr(c18,c19),
inference(cnf_transformation,[],[f10348]) ).
fof(f20861,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(f20862,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,[],[f20861]) ).
fof(f20864,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(f20865,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,[],[f20864]) ).
fof(f20866,plain,
( spl64_1
| spl64_2 ),
inference(avatar_split_clause,[],[f20817,f20864,f20861]) ).
fof(f21437,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,c20)
| ~ arg2(X0,X3)
| ~ sub(X2,eigenname_1_1)
| ~ sub(c20,familiename_1_1) )
| ~ spl64_1 ),
inference(resolution,[],[f20862,f20852]) ).
fof(f21464,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,c20)
| ~ arg2(X0,X3)
| ~ sub(X2,eigenname_1_1) )
| ~ spl64_1 ),
inference(forward_subsumption_resolution,[],[f21437,f20853]) ).
fof(f21704,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ arg1(X0,X1)
| ~ subr(X0,rprs_0)
| ~ sub(X2,X3)
| ~ obj(X4,X1)
| ~ attr(X1,c19)
| ~ attr(X1,c20)
| ~ arg2(X0,X2)
| ~ sub(c19,eigenname_1_1) )
| ~ spl64_1 ),
inference(resolution,[],[f21464,f20854]) ).
fof(f21729,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ arg1(X0,X1)
| ~ subr(X0,rprs_0)
| ~ sub(X2,X3)
| ~ obj(X4,X1)
| ~ attr(X1,c20)
| ~ arg2(X0,X2)
| ~ attr(X1,c19) )
| ~ spl64_1 ),
inference(forward_subsumption_resolution,[],[f21704,f20855]) ).
fof(f21741,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,c20)
| ~ attr(X1,c19) )
| ~ spl64_1 ),
inference(resolution,[],[f21729,f10692]) ).
fof(f22218,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ arg1(X1,X0)
| ~ subr(X1,rprs_0)
| ~ sub(X2,X3)
| ~ arg2(X1,X2)
| ~ loc(X0,X4)
| ~ fact(X0,real)
| ~ attr(X0,c19)
| ~ attr(X0,c20) )
| ~ spl64_1 ),
inference(resolution,[],[f21741,f10608]) ).
fof(f22275,plain,
( ! [X2,X3,X0,X1] :
( ~ arg1(X0,c18)
| ~ subr(X0,rprs_0)
| ~ sub(X1,X2)
| ~ arg2(X0,X1)
| ~ loc(c18,X3)
| ~ attr(c18,c19)
| ~ attr(c18,c20) )
| ~ spl64_1 ),
inference(resolution,[],[f22218,f20841]) ).
fof(f22285,plain,
( ! [X2,X3,X0,X1] :
( ~ arg1(X0,c18)
| ~ subr(X0,rprs_0)
| ~ sub(X1,X2)
| ~ arg2(X0,X1)
| ~ loc(c18,X3)
| ~ attr(c18,c20) )
| ~ spl64_1 ),
inference(forward_subsumption_resolution,[],[f22275,f20859]) ).
fof(f22289,plain,
( ! [X2,X3,X0,X1] :
( ~ arg1(X0,c18)
| ~ subr(X0,rprs_0)
| ~ sub(X1,X2)
| ~ arg2(X0,X1)
| ~ loc(c18,X3) )
| ~ spl64_1 ),
inference(forward_subsumption_resolution,[],[f22285,f20858]) ).
fof(f22293,definition,
( spl64_22
<=> ! [X3] : ~ loc(c18,X3) ),
introduced(definition,[new_symbols(definition,[spl64_22])],[avatar_definition]) ).
fof(f22294,plain,
( ! [X3] : ~ loc(c18,X3)
| ~ spl64_22 ),
inference(avatar_component_clause,[],[f22293]) ).
fof(f22296,definition,
( spl64_23
<=> ! [X2,X0,X1] :
( ~ arg1(X0,c18)
| ~ arg2(X0,X1)
| ~ sub(X1,X2)
| ~ subr(X0,rprs_0) ) ),
introduced(definition,[new_symbols(definition,[spl64_23])],[avatar_definition]) ).
fof(f22297,plain,
( ! [X2,X0,X1] :
( ~ arg2(X0,X1)
| ~ sub(X1,X2)
| ~ subr(X0,rprs_0)
| ~ arg1(X0,c18) )
| ~ spl64_23 ),
inference(avatar_component_clause,[],[f22296]) ).
fof(f22314,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,[],[f20865,f10858]) ).
fof(f22325,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,[],[f22314,f10859]) ).
fof(f22484,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,[],[f22325,f10862]) ).
fof(f23026,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,[],[f22484]) ).
fof(f23027,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,[],[f23026]) ).
fof(f23048,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,[],[f23027,f10863]) ).
fof(f23075,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,[],[f23048]) ).
fof(f23076,plain,
( ! [X0,X1] :
( ~ prop(X0,X1)
| ~ state_adjective_state_binding(X1,s__374dafrika_0) )
| ~ spl64_2 ),
inference(duplicate_literal_removal,[],[f23075]) ).
fof(f23078,plain,
( ~ state_adjective_state_binding(s__374dafrikanisch_1_1,s__374dafrika_0)
| ~ spl64_2 ),
inference(resolution,[],[f23076,f20857]) ).
fof(f23088,plain,
( $false
| ~ spl64_2 ),
inference(forward_subsumption_resolution,[],[f23078,f19790]) ).
fof(f23089,plain,
~ spl64_2,
inference(avatar_contradiction_clause,[],[f23088]) ).
fof(f23166,plain,
( ! [X0,X1] :
( ~ prop(c18,X0)
| ~ state_adjective_state_binding(X0,X1) )
| ~ spl64_22 ),
inference(resolution,[],[f22294,f10861]) ).
fof(f23229,plain,
( ! [X0] : ~ state_adjective_state_binding(s__374dafrikanisch_1_1,X0)
| ~ spl64_22 ),
inference(resolution,[],[f23166,f20857]) ).
fof(f23239,plain,
( $false
| ~ spl64_22 ),
inference(resolution,[],[f23229,f19790]) ).
fof(f23240,plain,
~ spl64_22,
inference(avatar_contradiction_clause,[],[f23239]) ).
fof(f23256,plain,
( ! [X2,X3,X0,X1] :
( ~ arg2(X3,sK57(X0,X1,X2))
| ~ subr(X3,rprs_0)
| ~ arg1(X3,c18)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl64_23 ),
inference(resolution,[],[f22297,f10882]) ).
fof(f23261,plain,
( spl64_22
| spl64_23
| ~ spl64_1 ),
inference(avatar_split_clause,[],[f22289,f20861,f22296,f22293]) ).
fof(f30372,plain,
( ! [X2,X0,X1] :
( ~ subr(sK56(X0,X1,X2),rprs_0)
| ~ arg1(sK56(X0,X1,X2),c18)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl64_23 ),
inference(resolution,[],[f23256,f10886]) ).
fof(f30374,plain,
( ! [X2,X0,X1] :
( ~ subr(sK56(X0,X1,X2),rprs_0)
| ~ arg1(sK56(X0,X1,X2),c18)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl64_23 ),
inference(duplicate_literal_removal,[],[f30372]) ).
fof(f30375,plain,
( ! [X2,X0,X1] :
( ~ arg1(sK56(X0,X1,X2),c18)
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subr(X0,sub_0) )
| ~ spl64_23 ),
inference(forward_subsumption_resolution,[],[f30374,f10881]) ).
fof(f30415,plain,
( ! [X0,X1] :
( ~ arg1(X0,c18)
| ~ arg2(X0,X1)
| ~ subr(X0,sub_0)
| ~ arg1(X0,c18)
| ~ arg2(X0,X1)
| ~ subr(X0,sub_0) )
| ~ spl64_23 ),
inference(resolution,[],[f30375,f10887]) ).
fof(f30416,plain,
( ! [X0,X1] :
( ~ arg2(X0,X1)
| ~ subr(X0,sub_0)
| ~ arg1(X0,c18) )
| ~ spl64_23 ),
inference(duplicate_literal_removal,[],[f30415]) ).
fof(f30474,plain,
( ! [X0,X1] :
( ~ subr(sK58(X0,X1),sub_0)
| ~ arg1(sK58(X0,X1),c18)
| ~ sub(X0,X1) )
| ~ spl64_23 ),
inference(resolution,[],[f30416,f10889]) ).
fof(f30476,plain,
( ! [X0,X1] :
( ~ arg1(sK58(X0,X1),c18)
| ~ sub(X0,X1) )
| ~ spl64_23 ),
inference(forward_subsumption_resolution,[],[f30474,f10888]) ).
fof(f30537,plain,
( ! [X0] :
( ~ sub(c18,X0)
| ~ sub(c18,X0) )
| ~ spl64_23 ),
inference(resolution,[],[f30476,f10890]) ).
fof(f30538,plain,
( ! [X0] : ~ sub(c18,X0)
| ~ spl64_23 ),
inference(duplicate_literal_removal,[],[f30537]) ).
fof(f30595,plain,
( $false
| ~ spl64_23 ),
inference(resolution,[],[f30538,f20856]) ).
fof(f30607,plain,
~ spl64_23,
inference(avatar_contradiction_clause,[],[f30595]) ).
cnf(s1,plain,
( spl64_1
| spl64_2 ),
inference(sat_conversion,[],[f20866]) ).
cnf(s19,plain,
~ spl64_2,
inference(sat_conversion,[],[f23089]) ).
cnf(s20,plain,
~ spl64_22,
inference(sat_conversion,[],[f23240]) ).
cnf(s21,plain,
( ~ spl64_1
| spl64_22
| spl64_23 ),
inference(sat_conversion,[],[f23261]) ).
cnf(s39,plain,
~ spl64_23,
inference(sat_conversion,[],[f30607]) ).
cnf(s40,plain,
( ~ spl64_1
| spl64_22 ),
inference(rat,[],[s21,s39]) ).
cnf(s41,plain,
~ spl64_1,
inference(rat,[],[s40,s20]) ).
cnf(s42,plain,
$false,
inference(rat,[],[s1,s19,s41]) ).
fof(f30608,plain,
$false,
inference(avatar_sat_refutation,[],[s42]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR116+16 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n008.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 23:28:50 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 Running first-order model finding
% 0.09/0.20 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
% 29.27/4.48 % (2755005)Will run a generic schedule for satisfiability detection.
% 29.27/4.48 % (2755016)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3599709482:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 29.27/4.48 % (2755011)% WARNING: option uhcvi not known.
% 29.27/4.48 % (2755010)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=586269203_2999 on theBenchmark for (2999ds/0Mi)
% 29.27/4.48 % (2755011)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3049526239:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 29.27/4.48 % (2755012)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4185037902:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 29.27/4.48 % (2755013)dis+10_1_sil=32000:sp=arity:random_seed=583865488:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 29.27/4.48 % (2755014)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1470346605:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 29.27/4.48 % (2755015)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1410478644:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 29.27/4.48 % (2755016)Instruction limit reached!
% 29.27/4.48 % (2755016)------------------------------
% 29.27/4.48 % (2755016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.27/4.48 % (2755016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.27/4.48 % (2755016)CaDiCaL version: 2.1.3
% 29.27/4.48 % (2755016)Termination reason: Instruction limit
% 29.27/4.48 % (2755016)Termination phase: Saturation
% 29.27/4.48 % (2755016)Time elapsed: 0.047 s
% 29.27/4.48 % (2755016)Peak memory usage: 29 MB
% 29.27/4.48 % (2755016)Instructions burned: 162 (million)
% 29.27/4.48 % (2755024)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=271871909:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 29.27/4.48 % (2755013)Instruction limit reached!
% 29.27/4.48 % (2755013)------------------------------
% 29.27/4.48 % (2755013)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.27/4.48 % (2755013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.27/4.48 % (2755013)CaDiCaL version: 2.1.3
% 29.27/4.48 % (2755013)Termination reason: Instruction limit
% 29.27/4.48 % (2755013)Termination phase: Saturation
% 29.27/4.48 % (2755013)Time elapsed: 0.058 s
% 29.27/4.48 % (2755013)Peak memory usage: 26 MB
% 29.27/4.48 % (2755013)Instructions burned: 104 (million)
% 29.27/4.48 % (2755014)Instruction limit reached!
% 29.27/4.48 % (2755014)------------------------------
% 29.27/4.48 % (2755014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.27/4.48 % (2755014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.27/4.48 % (2755014)CaDiCaL version: 2.1.3
% 29.27/4.48 % (2755014)Termination reason: Instruction limit
% 29.27/4.48 % (2755014)Termination phase: Blocked clause elimination
% 29.27/4.48 % (2755014)Time elapsed: 0.077 s
% 29.27/4.48 % (2755014)Peak memory usage: 27 MB
% 29.27/4.48 % (2755014)Instructions burned: 117 (million)
% 29.27/4.48 % (2755015)Instruction limit reached!
% 29.27/4.48 % (2755015)------------------------------
% 29.27/4.48 % (2755015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.27/4.48 % (2755015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.27/4.48 % (2755015)CaDiCaL version: 2.1.3
% 29.27/4.48 % (2755015)Termination reason: Instruction limit
% 29.27/4.48 % (2755015)Termination phase: Saturation
% 29.27/4.48 % (2755015)Time elapsed: 0.101 s
% 29.27/4.48 % (2755015)Peak memory usage: 27 MB
% 29.27/4.48 % (2755015)Instructions burned: 131 (million)
% 29.27/4.48 % (2755029)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1625161911:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 29.27/4.48 % (2755034)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=1722735726:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 29.27/4.48 % (2755037)ott-21_1_sil=16000:fs=off:random_seed=1792254693:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 29.27/4.48 % (2755029)Instruction limit reached!
% 29.27/4.48 % (2755029)------------------------------
% 29.27/4.48 % (2755029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.27/4.48 % (2755029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.11/7.24 % (2755029)CaDiCaL version: 2.1.3
% 49.11/7.24 % (2755029)Termination reason: Instruction limit
% 49.11/7.24 % (2755029)Termination phase: Blocked clause elimination
% 49.11/7.24 % (2755029)Time elapsed: 0.119 s
% 49.11/7.24 % (2755029)Peak memory usage: 29 MB
% 49.11/7.24 % (2755029)Instructions burned: 131 (million)
% 49.11/7.24 % TRYING [1]
% 49.11/7.24 % (2755037)Instruction limit reached!
% 49.11/7.24 % (2755037)------------------------------
% 49.11/7.24 % (2755037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.11/7.24 % (2755037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.11/7.24 % (2755037)CaDiCaL version: 2.1.3
% 49.11/7.24 % (2755037)Termination reason: Instruction limit
% 49.11/7.24 % (2755037)Termination phase: Saturation
% 49.11/7.24 % (2755037)Time elapsed: 0.101 s
% 49.11/7.24 % (2755037)Peak memory usage: 28 MB
% 49.11/7.24 % (2755037)Instructions burned: 180 (million)
% 49.11/7.24 % (2755040)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3078573334:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 49.11/7.24 % TRYING [2]
% 49.11/7.24 % (2755041)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4265296678:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 49.11/7.24 % (2755024)Instruction limit reached!
% 49.11/7.24 % (2755024)------------------------------
% 49.11/7.24 % (2755024)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.11/7.24 % (2755024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.11/7.24 % (2755024)CaDiCaL version: 2.1.3
% 49.11/7.24 % (2755024)Termination reason: Instruction limit
% 49.11/7.24 % (2755024)Termination phase: Finite model building constraint generation
% 49.11/7.24 % (2755024)Time elapsed: 0.322 s
% 49.11/7.24 % (2755024)Peak memory usage: 54 MB
% 49.11/7.24 % (2755024)Instructions burned: 716 (million)
% 49.11/7.24 % TRYING [1]
% 49.11/7.24 % (2755050)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3681174190:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 49.11/7.24 % TRYING [2]
% 49.11/7.24 % TRYING [1]
% 49.11/7.24 % (2755040)Instruction limit reached!
% 49.11/7.24 % (2755040)------------------------------
% 49.11/7.24 % (2755040)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.11/7.24 % (2755040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.11/7.24 % (2755040)CaDiCaL version: 2.1.3
% 49.11/7.24 % (2755040)Termination reason: Instruction limit
% 49.11/7.24 % (2755040)Termination phase: Saturation
% 49.11/7.24 % (2755040)Time elapsed: 0.435 s
% 49.11/7.24 % (2755040)Peak memory usage: 37 MB
% 49.11/7.24 % (2755040)Instructions burned: 477 (million)
% 49.11/7.24 % (2755034)Instruction limit reached!
% 49.11/7.24 % (2755034)------------------------------
% 49.11/7.24 % (2755034)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.11/7.24 % (2755034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.11/7.24 % (2755034)CaDiCaL version: 2.1.3
% 49.11/7.24 % (2755034)Termination reason: Instruction limit
% 49.11/7.24 % (2755034)Termination phase: Saturation
% 49.11/7.24 % (2755034)Time elapsed: 0.593 s
% 49.11/7.24 % (2755034)Peak memory usage: 41 MB
% 49.11/7.24 % (2755034)Instructions burned: 688 (million)
% 49.11/7.24 % (2755041)Instruction limit reached!
% 49.11/7.24 % (2755041)------------------------------
% 49.11/7.24 % (2755041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 49.11/7.24 % (2755041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.11/7.24 % (2755041)CaDiCaL version: 2.1.3
% 49.11/7.24 % (2755041)Termination reason: Instruction limit
% 49.11/7.24 % (2755041)Termination phase: Finite model building SAT solving
% 49.11/7.24 % (2755041)Time elapsed: 0.429 s
% 49.11/7.24 % (2755041)Peak memory usage: 38 MB
% 49.11/7.24 % (2755041)Instructions burned: 866 (million)
% 49.11/7.24 % TRYING [3]
% 49.11/7.24 % (2755057)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1449539645:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 49.11/7.24 % (2755058)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=2462327923:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 49.11/7.24 % (2755059)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2504159207:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi)
% 49.11/7.24 % (2755050)Instruction limit reached!
% 49.11/7.24 % (2755050)------------------------------
% 49.11/7.24 % (2755050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.30/14.71 % (2755050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.30/14.71 % (2755050)CaDiCaL version: 2.1.3
% 102.30/14.71 % (2755050)Termination reason: Instruction limit
% 102.30/14.71 % (2755050)Termination phase: Saturation
% 102.30/14.71 % (2755050)Time elapsed: 0.624 s
% 102.30/14.71 % (2755050)Peak memory usage: 55 MB
% 102.30/14.71 % (2755050)Instructions burned: 1181 (million)
% 102.30/14.71 % (2755065)fmb+10_1_sil=64000:random_seed=3917801489:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi)
% 102.30/14.71 % TRYING [1]
% 102.30/14.71 % (2755058)Instruction limit reached!
% 102.30/14.71 % (2755058)------------------------------
% 102.30/14.71 % (2755058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.30/14.71 % (2755058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.30/14.71 % (2755058)CaDiCaL version: 2.1.3
% 102.30/14.71 % (2755058)Termination reason: Instruction limit
% 102.30/14.71 % (2755058)Termination phase: Saturation
% 102.30/14.71 % (2755058)Time elapsed: 0.596 s
% 102.30/14.71 % (2755058)Peak memory usage: 43 MB
% 102.30/14.71 % (2755058)Instructions burned: 692 (million)
% 102.30/14.71 % (2755070)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1118659615:i=9515:nm=5_2985 on theBenchmark for (2985ds/9515Mi)
% 102.30/14.71 % TRYING [2]
% 102.30/14.71 % (2755057)Instruction limit reached!
% 102.30/14.71 % (2755057)------------------------------
% 102.30/14.71 % (2755057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.30/14.71 % (2755057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.30/14.71 % (2755057)CaDiCaL version: 2.1.3
% 102.30/14.71 % (2755057)Termination reason: Instruction limit
% 102.30/14.71 % (2755057)Termination phase: Finite model building constraint generation
% 102.30/14.71 % (2755057)Time elapsed: 0.670 s
% 102.30/14.71 % (2755057)Peak memory usage: 95 MB
% 102.30/14.71 % (2755057)Instructions burned: 892 (million)
% 102.30/14.71 % (2755059)Instruction limit reached!
% 102.30/14.71 % (2755059)------------------------------
% 102.30/14.71 % (2755059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.30/14.71 % (2755059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.30/14.71 % (2755059)CaDiCaL version: 2.1.3
% 102.30/14.71 % (2755059)Termination reason: Instruction limit
% 102.30/14.71 % (2755059)Termination phase: Saturation
% 102.30/14.71 % (2755059)Time elapsed: 0.674 s
% 102.30/14.71 % (2755059)Peak memory usage: 41 MB
% 102.30/14.71 % (2755059)Instructions burned: 881 (million)
% 102.30/14.71 % (2755072)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=205083204:fmbsr=1.7:i=920_2984 on theBenchmark for (2984ds/920Mi)
% 102.30/14.71 % (2755073)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2899324553:i=5131_2984 on theBenchmark for (2984ds/5131Mi)
% 102.30/14.71 % TRYING [20]
% 102.30/14.71 % TRYING [8]
% 102.30/14.71 % TRYING [3]
% 102.30/14.71 % (2755072)Instruction limit reached!
% 102.30/14.71 % (2755072)------------------------------
% 102.30/14.71 % (2755072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.30/14.71 % (2755072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.30/14.71 % (2755072)CaDiCaL version: 2.1.3
% 102.30/14.71 % (2755072)Termination reason: Instruction limit
% 102.30/14.71 % (2755072)Termination phase: Finite model building constraint generation
% 102.30/14.71 % (2755072)Time elapsed: 0.359 s
% 102.30/14.71 % (2755072)Peak memory usage: 64 MB
% 102.30/14.71 % (2755072)Instructions burned: 923 (million)
% 102.30/14.71 % (2755112)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2417957621:i=1472:ins=7:fdi=8:gsp=on_2981 on theBenchmark for (2981ds/1472Mi)
% 102.30/14.71 % TRYING [4]
% 102.30/14.71 % (2755112)Instruction limit reached!
% 102.30/14.71 % (2755112)------------------------------
% 102.30/14.71 % (2755112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 102.30/14.71 % (2755112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 102.30/14.71 % (2755112)CaDiCaL version: 2.1.3
% 102.30/14.71 % (2755112)Termination reason: Instruction limit
% 102.30/14.71 % (2755112)Termination phase: Saturation
% 102.30/14.71 % (2755112)Time elapsed: 0.668 s
% 102.30/14.71 % (2755112)Peak memory usage: 34 MB
% 102.30/14.71 % (2755112)Instructions burned: 1474 (million)
% 102.30/14.71 % (2755231)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=451083285:i=6324_2974 on theBenchmark for (2974ds/6324Mi)
% 102.30/14.71 % TRYING [77]
% 102.30/14.71 % TRYING [4]
% 102.30/14.71 % TRYING [5]
% 102.30/14.71 % (2755073)Instruction limit reached!
% 102.30/14.71 % (2755073)------------------------------
% 102.30/14.71 % (2755073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.59/31.84 % (2755073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.59/31.84 % (2755073)CaDiCaL version: 2.1.3
% 223.59/31.84 % (2755073)Termination reason: Instruction limit
% 223.59/31.84 % (2755073)Termination phase: Saturation
% 223.59/31.84 % (2755073)Time elapsed: 2.745 s
% 223.59/31.84 % (2755073)Peak memory usage: 39 MB
% 223.59/31.84 % (2755073)Instructions burned: 5132 (million)
% 223.59/31.84 % (2755233)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1057275375:fmbsr=2.30978:i=2174_2957 on theBenchmark for (2957ds/2174Mi)
% 223.59/31.84 % TRYING [16]
% 223.59/31.84 % (2755070)Instruction limit reached!
% 223.59/31.84 % (2755070)------------------------------
% 223.59/31.84 % (2755070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.59/31.84 % (2755070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.59/31.84 % (2755070)CaDiCaL version: 2.1.3
% 223.59/31.84 % (2755070)Termination reason: Instruction limit
% 223.59/31.84 % (2755070)Termination phase: Finite model building constraint generation
% 223.59/31.84 % (2755070)Time elapsed: 3.301 s
% 223.59/31.84 % (2755070)Peak memory usage: 550 MB
% 223.59/31.84 % (2755070)Instructions burned: 9517 (million)
% 223.59/31.84 % (2755235)ott-2_1_sil=16000:newcnf=on:random_seed=595896589:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2951 on theBenchmark for (2951ds/869Mi)
% 223.59/31.84 % (2755231)Instruction limit reached!
% 223.59/31.84 % (2755231)------------------------------
% 223.59/31.84 % (2755231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.59/31.84 % (2755231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.59/31.84 % (2755231)CaDiCaL version: 2.1.3
% 223.59/31.84 % (2755231)Termination reason: Instruction limit
% 223.59/31.84 % (2755231)Termination phase: Finite model building constraint generation
% 223.59/31.84 % (2755231)Time elapsed: 2.268 s
% 223.59/31.84 % (2755231)Peak memory usage: 417 MB
% 223.59/31.84 % (2755231)Instructions burned: 6324 (million)
% 223.59/31.84 % (2755237)ott+10_1_sil=32000:tgt=ground:random_seed=3716250551:i=5114:av=off_2950 on theBenchmark for (2950ds/5114Mi)
% 223.59/31.84 % (2755233)Instruction limit reached!
% 223.59/31.84 % (2755233)------------------------------
% 223.59/31.84 % (2755233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.59/31.84 % (2755233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.59/31.84 % (2755233)CaDiCaL version: 2.1.3
% 223.59/31.84 % (2755233)Termination reason: Instruction limit
% 223.59/31.84 % (2755233)Termination phase: Finite model building constraint generation
% 223.59/31.84 % (2755233)Time elapsed: 0.760 s
% 223.59/31.84 % (2755233)Peak memory usage: 121 MB
% 223.59/31.84 % (2755233)Instructions burned: 2176 (million)
% 223.59/31.84 % (2755239)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3565611983:i=54282_2949 on theBenchmark for (2949ds/54282Mi)
% 223.59/31.84 % (2755235)Instruction limit reached!
% 223.59/31.84 % (2755235)------------------------------
% 223.59/31.84 % (2755235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.59/31.84 % (2755235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.59/31.84 % (2755235)CaDiCaL version: 2.1.3
% 223.59/31.84 % (2755235)Termination reason: Instruction limit
% 223.59/31.84 % (2755235)Termination phase: Saturation
% 223.59/31.84 % (2755235)Time elapsed: 0.423 s
% 223.59/31.84 % (2755235)Peak memory usage: 38 MB
% 223.59/31.84 % (2755235)Instructions burned: 871 (million)
% 223.59/31.84 % (2755241)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2409186838:i=3512:aac=none_2947 on theBenchmark for (2947ds/3512Mi)
% 223.59/31.84 % TRYING [1]
% 223.59/31.84 % TRYING [2]
% 223.59/31.84 % TRYING [3]
% 223.59/31.84 % TRYING [6]
% 223.59/31.84 % (2755065)Instruction limit reached!
% 223.59/31.84 % (2755065)------------------------------
% 223.59/31.84 % (2755065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 223.59/31.84 % (2755065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 223.59/31.84 % (2755065)CaDiCaL version: 2.1.3
% 223.59/31.84 % (2755065)Termination reason: Instruction limit
% 223.59/31.84 % (2755065)Termination phase: Finite model building SAT solving
% 223.59/31.84 % (2755065)Time elapsed: 5.323 s
% 223.59/31.84 % (2755065)Peak memory usage: 183 MB
% 223.59/31.84 % (2755065)Instructions burned: 22062 (million)
% 223.59/31.84 % (2755243)dis+21_1_sil=32000:sas=cadical:random_seed=684008562:i=3773:amm=off_2934 on theBenchmark for (2934ds/3773Mi)
% 223.59/31.84 % (2755241)Instruction limit reached!
% 223.59/31.84 % (2755241)------------------------------
% 223.59/31.84 % (2755241)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755241)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755241)Termination reason: Instruction limit
% 147.60/36.42 % (2755241)Termination phase: Saturation
% 147.60/36.42 % (2755241)Time elapsed: 1.753 s
% 147.60/36.42 % (2755241)Peak memory usage: 40 MB
% 147.60/36.42 % (2755241)Instructions burned: 3513 (million)
% 147.60/36.42 % (2755245)ott+11_1_sil=16000:gs=on:random_seed=368973957:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2929 on theBenchmark for (2929ds/2251Mi)
% 147.60/36.42 % (2755243)Instruction limit reached!
% 147.60/36.42 % (2755243)------------------------------
% 147.60/36.42 % (2755243)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755243)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755243)Termination reason: Instruction limit
% 147.60/36.42 % (2755243)Termination phase: Saturation
% 147.60/36.42 % (2755243)Time elapsed: 0.986 s
% 147.60/36.42 % (2755243)Peak memory usage: 68 MB
% 147.60/36.42 % (2755243)Instructions burned: 3777 (million)
% 147.60/36.42 % (2755247)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2415353414:fmbsr=1.6:i=67534_2924 on theBenchmark for (2924ds/67534Mi)
% 147.60/36.42 % (2755237)Instruction limit reached!
% 147.60/36.42 % (2755237)------------------------------
% 147.60/36.42 % (2755237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755237)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755237)Termination reason: Instruction limit
% 147.60/36.42 % (2755237)Termination phase: Saturation
% 147.60/36.42 % (2755237)Time elapsed: 2.595 s
% 147.60/36.42 % (2755237)Peak memory usage: 119 MB
% 147.60/36.42 % (2755237)Instructions burned: 5114 (million)
% 147.60/36.42 % (2755249)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3596900535:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2924 on theBenchmark for (2924ds/4591Mi)
% 147.60/36.42 % TRYING [4]
% 147.60/36.42 % TRYING [7]
% 147.60/36.42 % (2755245)Instruction limit reached!
% 147.60/36.42 % (2755245)------------------------------
% 147.60/36.42 % (2755245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755245)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755245)Termination reason: Instruction limit
% 147.60/36.42 % (2755245)Termination phase: Saturation
% 147.60/36.42 % (2755245)Time elapsed: 1.160 s
% 147.60/36.42 % (2755245)Peak memory usage: 63 MB
% 147.60/36.42 % (2755245)Instructions burned: 2253 (million)
% 147.60/36.42 % (2755251)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2376776461:i=29340_2917 on theBenchmark for (2917ds/29340Mi)
% 147.60/36.42 % (2755249)Instruction limit reached!
% 147.60/36.42 % (2755249)------------------------------
% 147.60/36.42 % (2755249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755249)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755249)Termination reason: Instruction limit
% 147.60/36.42 % (2755249)Termination phase: Saturation
% 147.60/36.42 % (2755249)Time elapsed: 2.082 s
% 147.60/36.42 % (2755249)Peak memory usage: 43 MB
% 147.60/36.42 % (2755249)Instructions burned: 4593 (million)
% 147.60/36.42 % (2755253)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3087487101:i=5211_2903 on theBenchmark for (2903ds/5211Mi)
% 147.60/36.42 % (2755253)Instruction limit reached!
% 147.60/36.42 % (2755253)------------------------------
% 147.60/36.42 % (2755253)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755253)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755253)Termination reason: Instruction limit
% 147.60/36.42 % (2755253)Termination phase: Saturation
% 147.60/36.42 % (2755253)Time elapsed: 2.772 s
% 147.60/36.42 % (2755253)Peak memory usage: 54 MB
% 147.60/36.42 % (2755253)Instructions burned: 5213 (million)
% 147.60/36.42 % (2755255)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1340703548:i=5497:nm=2_2875 on theBenchmark for (2875ds/5497Mi)
% 147.60/36.42 % TRYING [17]
% 147.60/36.42 % (2755255)Instruction limit reached!
% 147.60/36.42 % (2755255)------------------------------
% 147.60/36.42 % (2755255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755255)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755255)Termination reason: Instruction limit
% 147.60/36.42 % (2755255)Termination phase: Finite model building constraint generation
% 147.60/36.42 % (2755255)Time elapsed: 2.018 s
% 147.60/36.42 % (2755255)Peak memory usage: 350 MB
% 147.60/36.42 % (2755255)Instructions burned: 5499 (million)
% 147.60/36.42 % (2755257)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3103776863:fmbsr=2:i=46332_2854 on theBenchmark for (2854ds/46332Mi)
% 147.60/36.42 % TRYING [15]
% 147.60/36.42 % TRYING [5]
% 147.60/36.42 % (2755251)Instruction limit reached!
% 147.60/36.42 % (2755251)------------------------------
% 147.60/36.42 % (2755251)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755251)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755251)Termination reason: Instruction limit
% 147.60/36.42 % (2755251)Termination phase: Saturation
% 147.60/36.42 % (2755251)Time elapsed: 14.227 s
% 147.60/36.42 % (2755251)Peak memory usage: 83 MB
% 147.60/36.42 % (2755251)Instructions burned: 29340 (million)
% 147.60/36.42 % (2755708)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=657151177:i=14071_2775 on theBenchmark for (2775ds/14071Mi)
% 147.60/36.42 % TRYING [12]
% 147.60/36.42 % (2755247)Instruction limit reached!
% 147.60/36.42 % (2755247)------------------------------
% 147.60/36.42 % (2755247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755247)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755247)Termination reason: Instruction limit
% 147.60/36.42 % (2755247)Termination phase: Finite model building SAT solving
% 147.60/36.42 % (2755247)Time elapsed: 17.027 s
% 147.60/36.42 % (2755247)Peak memory usage: 287 MB
% 147.60/36.42 % (2755247)Instructions burned: 67538 (million)
% 147.60/36.42 % (2755710)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2011082180:i=22565:add=on:rawr=on_2754 on theBenchmark for (2754ds/22565Mi)
% 147.60/36.42 % TRYING [5]
% 147.60/36.42 % (2755708)Instruction limit reached!
% 147.60/36.42 % (2755708)------------------------------
% 147.60/36.42 % (2755708)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755708)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755708)Termination reason: Instruction limit
% 147.60/36.42 % (2755708)Termination phase: Finite model building constraint generation
% 147.60/36.42 % (2755708)Time elapsed: 6.478 s
% 147.60/36.42 % (2755708)Peak memory usage: 1122 MB
% 147.60/36.42 % (2755708)Instructions burned: 14073 (million)
% 147.60/36.42 % (2755710)Instruction limit reached!
% 147.60/36.42 % (2755710)------------------------------
% 147.60/36.42 % (2755710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755710)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755710)Termination reason: Instruction limit
% 147.60/36.42 % (2755710)Termination phase: Saturation
% 147.60/36.42 % (2755710)Time elapsed: 4.446 s
% 147.60/36.42 % (2755710)Peak memory usage: 119 MB
% 147.60/36.42 % (2755710)Instructions burned: 22566 (million)
% 147.60/36.42 % (2755712)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=4239605415:i=8173:av=off_2709 on theBenchmark for (2709ds/8173Mi)
% 147.60/36.42 % (2755714)dis+10_16:1_sil=16000:random_seed=2974958587:i=9155:fsr=off_2708 on theBenchmark for (2708ds/9155Mi)
% 147.60/36.42 % (2755239)Instruction limit reached!
% 147.60/36.42 % (2755239)------------------------------
% 147.60/36.42 % (2755239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755239)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755239)Termination reason: Instruction limit
% 147.60/36.42 % (2755239)Termination phase: Finite model building SAT solving
% 147.60/36.42 % (2755239)Time elapsed: 26.458 s
% 147.60/36.42 % (2755239)Peak memory usage: 244 MB
% 147.60/36.42 % (2755239)Instructions burned: 54282 (million)
% 147.60/36.42 % (2755716)ott-3_8_sil=64000:random_seed=1090727181:i=20139:bs=on_2684 on theBenchmark for (2684ds/20139Mi)
% 147.60/36.42 % (2755712)Instruction limit reached!
% 147.60/36.42 % (2755712)------------------------------
% 147.60/36.42 % (2755712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755712)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755712)Termination reason: Instruction limit
% 147.60/36.42 % (2755712)Termination phase: Saturation
% 147.60/36.42 % (2755712)Time elapsed: 2.583 s
% 147.60/36.42 % (2755712)Peak memory usage: 192 MB
% 147.60/36.42 % (2755712)Instructions burned: 8176 (million)
% 147.60/36.42 % (2755718)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1024539479:fmbsr=2:i=32576_2683 on theBenchmark for (2683ds/32576Mi)
% 147.60/36.42 % TRYING [9]
% 147.60/36.42 % (2755012)Instruction limit reached!
% 147.60/36.42 % (2755012)------------------------------
% 147.60/36.42 % (2755012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755012)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755012)Termination reason: Instruction limit
% 147.60/36.42 % (2755012)Termination phase: Saturation
% 147.60/36.42 % (2755012)Time elapsed: 32.082 s
% 147.60/36.42 % (2755012)Peak memory usage: 161 MB
% 147.60/36.42 % (2755012)Instructions burned: 88026 (million)
% 147.60/36.42 % (2755720)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=950109752:i=11404_2678 on theBenchmark for (2678ds/11404Mi)
% 147.60/36.42 % (2755714)Instruction limit reached!
% 147.60/36.42 % (2755714)------------------------------
% 147.60/36.42 % (2755714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.42 % (2755714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.42 % (2755714)CaDiCaL version: 2.1.3
% 147.60/36.42 % (2755714)Termination reason: Instruction limit
% 147.60/36.42 % (2755714)Termination phase: Saturation
% 147.60/36.42 % (2755714)Time elapsed: 3.763 s
% 147.60/36.42 % (2755714)Peak memory usage: 82 MB
% 147.60/36.42 % (2755714)Instructions burned: 9156 (million)
% 147.60/36.42 % (2755778)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2442794786:i=14134_2670 on theBenchmark for (2670ds/14134Mi)
% 147.60/36.42 % (2755778) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2755005-2755778"...
% 147.60/36.42 % (2755778)...printing done.
% 147.60/36.42 % (2755778)Refutation found. Thanks to Tanya!
% 147.60/36.42 % SZS status Theorem for theBenchmark
% 147.60/36.42 % SZS output start Proof for theBenchmark
% See solution above
% 147.60/36.44 % (2755778)------------------------------
% 147.60/36.44 % (2755778)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 147.60/36.44 % (2755778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 147.60/36.44 % (2755778)CaDiCaL version: 2.1.3
% 147.60/36.44 % (2755778)Termination reason: Refutation
% 147.60/36.44 % (2755778)Time elapsed: 2.778 s
% 147.60/36.44 % (2755778)Peak memory usage: 51 MB
% 147.60/36.44 % (2755778)Instructions burned: 4560 (million)
% 147.60/36.44 % (2755005)Success in time 36.214 s
% 147.60/36.44 % Vampire exiting
%------------------------------------------------------------------------------