%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR115+29 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:35 AM UTC 2026
% Result : Theorem 6.24s 1.81s
% Output : Refutation 6.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 8
% Syntax : Number of formulae : 54 ( 16 unt; 3 def)
% Number of atoms : 577 ( 0 equ)
% Maximal formula atoms : 106 ( 10 avg)
% Number of connectives : 569 ( 46 ~; 58 |; 460 &)
% ( 3 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 106 ( 13 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 21 ( 20 usr; 4 prp; 0-3 aty)
% Number of functors : 46 ( 46 usr; 44 con; 0-2 aty)
% Number of variables : 95 ( 0 sgn 78 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : member(X0,cons(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',member_first) ).
fof(f2,axiom,
! [X0,X1,X2] :
( member(X0,X2)
=> member(X0,cons(X1,X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',member_second) ).
fof(f160,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] :
( mcont(X3,X2)
& obj(X3,X2)
& scar(X3,X2)
& subs(X3,stehen_1_b) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',attr_name__abk__374rzung_stehen_1_b_f__374r) ).
fof(f10188,conjecture,
? [X0,X1,X2,X3,X4,X5,X6] :
( attr(X0,X1)
& attr(X3,X2)
& attr(X5,X6)
& obj(X4,X0)
& sub(X1,name_1_1)
& sub(X2,name_1_1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_007_mira_news_1203_a462) ).
fof(f10189,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6] :
( attr(X0,X1)
& attr(X3,X2)
& attr(X5,X6)
& obj(X4,X0)
& sub(X1,name_1_1)
& sub(X2,name_1_1) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( attr(c15,c16)
& sub(c15,stadt__1_1)
& sub(c16,name_1_1)
& val(c16,genf_0)
& attr(c22,c23)
& attr(c22,c24)
& sub(c23,tag_1_1)
& val(c23,c20)
& sub(c24,monat_1_1)
& val(c24,c21)
& tupl(c75,c15,c22)
& sort(c15,d)
& sort(c15,io)
& card(c15,int1)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& quant(c15,one)
& refer(c15,det)
& varia(c15,con)
& sort(c16,na)
& card(c16,int1)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& quant(c16,one)
& refer(c16,indet)
& varia(c16,varia_c)
& sort(stadt__1_1,d)
& sort(stadt__1_1,io)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& sort(name_1_1,na)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& sort(genf_0,fe)
& sort(c22,t)
& card(c22,int1)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,sp)
& quant(c22,one)
& refer(c22,det)
& varia(c22,con)
& sort(c23,me)
& sort(c23,oa)
& sort(c23,ta)
& card(c23,card_c)
& etype(c23,etype_c)
& fact(c23,real)
& gener(c23,sp)
& quant(c23,quant_c)
& refer(c23,refer_c)
& varia(c23,varia_c)
& sort(c24,me)
& sort(c24,oa)
& sort(c24,ta)
& card(c24,card_c)
& etype(c24,etype_c)
& fact(c24,real)
& gener(c24,sp)
& quant(c24,quant_c)
& refer(c24,refer_c)
& varia(c24,varia_c)
& sort(tag_1_1,me)
& sort(tag_1_1,oa)
& sort(tag_1_1,ta)
& card(tag_1_1,card_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& quant(tag_1_1,quant_c)
& refer(tag_1_1,refer_c)
& varia(tag_1_1,varia_c)
& sort(c20,nu)
& card(c20,int7)
& sort(monat_1_1,me)
& sort(monat_1_1,oa)
& sort(monat_1_1,ta)
& card(monat_1_1,card_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& quant(monat_1_1,quant_c)
& refer(monat_1_1,refer_c)
& varia(monat_1_1,varia_c)
& sort(c21,nu)
& card(c21,int3)
& sort(c75,ent)
& card(c75,card_c)
& etype(c75,etype_c)
& fact(c75,real)
& gener(c75,gener_c)
& quant(c75,quant_c)
& refer(c75,refer_c)
& varia(c75,varia_c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_007_mira_news_1203_a462) ).
fof(f10325,plain,
( attr(c15,c16)
& sub(c15,stadt__1_1)
& sub(c16,name_1_1)
& val(c16,genf_0)
& attr(c22,c23)
& attr(c22,c24)
& sub(c23,tag_1_1)
& val(c23,c20)
& sub(c24,monat_1_1)
& val(c24,c21)
& tupl(c75,c15,c22)
& card(c15,int1)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& quant(c15,one)
& refer(c15,det)
& varia(c15,con)
& card(c16,int1)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& quant(c16,one)
& refer(c16,indet)
& varia(c16,varia_c)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& quant(stadt__1_1,one)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& quant(name_1_1,one)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& card(c22,int1)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,sp)
& quant(c22,one)
& refer(c22,det)
& varia(c22,con)
& card(c23,card_c)
& etype(c23,etype_c)
& fact(c23,real)
& gener(c23,sp)
& quant(c23,quant_c)
& refer(c23,refer_c)
& varia(c23,varia_c)
& card(c24,card_c)
& etype(c24,etype_c)
& fact(c24,real)
& gener(c24,sp)
& quant(c24,quant_c)
& refer(c24,refer_c)
& varia(c24,varia_c)
& card(tag_1_1,card_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& quant(tag_1_1,quant_c)
& refer(tag_1_1,refer_c)
& varia(tag_1_1,varia_c)
& card(c20,int7)
& card(monat_1_1,card_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& quant(monat_1_1,quant_c)
& refer(monat_1_1,refer_c)
& varia(monat_1_1,varia_c)
& card(c21,int3)
& card(c75,card_c)
& etype(c75,etype_c)
& fact(c75,real)
& gener(c75,gener_c)
& quant(c75,quant_c)
& refer(c75,refer_c)
& varia(c75,varia_c) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10328,plain,
( attr(c15,c16)
& sub(c15,stadt__1_1)
& sub(c16,name_1_1)
& val(c16,genf_0)
& attr(c22,c23)
& attr(c22,c24)
& sub(c23,tag_1_1)
& val(c23,c20)
& sub(c24,monat_1_1)
& val(c24,c21)
& tupl(c75,c15,c22)
& card(c15,int1)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& refer(c15,det)
& varia(c15,con)
& card(c16,int1)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& refer(c16,indet)
& varia(c16,varia_c)
& card(stadt__1_1,int1)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& card(name_1_1,int1)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& card(c22,int1)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,sp)
& refer(c22,det)
& varia(c22,con)
& card(c23,card_c)
& etype(c23,etype_c)
& fact(c23,real)
& gener(c23,sp)
& refer(c23,refer_c)
& varia(c23,varia_c)
& card(c24,card_c)
& etype(c24,etype_c)
& fact(c24,real)
& gener(c24,sp)
& refer(c24,refer_c)
& varia(c24,varia_c)
& card(tag_1_1,card_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& refer(tag_1_1,refer_c)
& varia(tag_1_1,varia_c)
& card(c20,int7)
& card(monat_1_1,card_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& refer(monat_1_1,refer_c)
& varia(monat_1_1,varia_c)
& card(c21,int3)
& card(c75,card_c)
& etype(c75,etype_c)
& fact(c75,real)
& gener(c75,gener_c)
& refer(c75,refer_c)
& varia(c75,varia_c) ),
inference(pure_predicate_removal,[],[f10325]) ).
fof(f10331,plain,
( attr(c15,c16)
& sub(c15,stadt__1_1)
& sub(c16,name_1_1)
& val(c16,genf_0)
& attr(c22,c23)
& attr(c22,c24)
& sub(c23,tag_1_1)
& val(c23,c20)
& sub(c24,monat_1_1)
& val(c24,c21)
& tupl(c75,c15,c22)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& refer(c15,det)
& varia(c15,con)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& refer(c16,indet)
& varia(c16,varia_c)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& refer(stadt__1_1,refer_c)
& varia(stadt__1_1,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& refer(name_1_1,refer_c)
& varia(name_1_1,varia_c)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,sp)
& refer(c22,det)
& varia(c22,con)
& etype(c23,etype_c)
& fact(c23,real)
& gener(c23,sp)
& refer(c23,refer_c)
& varia(c23,varia_c)
& etype(c24,etype_c)
& fact(c24,real)
& gener(c24,sp)
& refer(c24,refer_c)
& varia(c24,varia_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& refer(tag_1_1,refer_c)
& varia(tag_1_1,varia_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& refer(monat_1_1,refer_c)
& varia(monat_1_1,varia_c)
& etype(c75,etype_c)
& fact(c75,real)
& gener(c75,gener_c)
& refer(c75,refer_c)
& varia(c75,varia_c) ),
inference(pure_predicate_removal,[],[f10328]) ).
fof(f10334,plain,
( attr(c15,c16)
& sub(c15,stadt__1_1)
& sub(c16,name_1_1)
& val(c16,genf_0)
& attr(c22,c23)
& attr(c22,c24)
& sub(c23,tag_1_1)
& val(c23,c20)
& sub(c24,monat_1_1)
& val(c24,c21)
& tupl(c75,c15,c22)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& varia(c15,con)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& varia(c16,varia_c)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& varia(stadt__1_1,varia_c)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& varia(name_1_1,varia_c)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,sp)
& varia(c22,con)
& etype(c23,etype_c)
& fact(c23,real)
& gener(c23,sp)
& varia(c23,varia_c)
& etype(c24,etype_c)
& fact(c24,real)
& gener(c24,sp)
& varia(c24,varia_c)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& varia(tag_1_1,varia_c)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& varia(monat_1_1,varia_c)
& etype(c75,etype_c)
& fact(c75,real)
& gener(c75,gener_c)
& varia(c75,varia_c) ),
inference(pure_predicate_removal,[],[f10331]) ).
fof(f10339,plain,
( attr(c15,c16)
& sub(c15,stadt__1_1)
& sub(c16,name_1_1)
& val(c16,genf_0)
& attr(c22,c23)
& attr(c22,c24)
& sub(c23,tag_1_1)
& val(c23,c20)
& sub(c24,monat_1_1)
& val(c24,c21)
& tupl(c75,c15,c22)
& etype(c15,int0)
& fact(c15,real)
& gener(c15,sp)
& etype(c16,int0)
& fact(c16,real)
& gener(c16,sp)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& etype(c22,int0)
& fact(c22,real)
& gener(c22,sp)
& etype(c23,etype_c)
& fact(c23,real)
& gener(c23,sp)
& etype(c24,etype_c)
& fact(c24,real)
& gener(c24,sp)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& gener(tag_1_1,ge)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& gener(monat_1_1,ge)
& etype(c75,etype_c)
& fact(c75,real)
& gener(c75,gener_c) ),
inference(pure_predicate_removal,[],[f10334]) ).
fof(f10344,plain,
( attr(c15,c16)
& sub(c15,stadt__1_1)
& sub(c16,name_1_1)
& val(c16,genf_0)
& attr(c22,c23)
& attr(c22,c24)
& sub(c23,tag_1_1)
& val(c23,c20)
& sub(c24,monat_1_1)
& val(c24,c21)
& tupl(c75,c15,c22)
& etype(c15,int0)
& fact(c15,real)
& etype(c16,int0)
& fact(c16,real)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& etype(c22,int0)
& fact(c22,real)
& etype(c23,etype_c)
& fact(c23,real)
& etype(c24,etype_c)
& fact(c24,real)
& etype(tag_1_1,etype_c)
& fact(tag_1_1,real)
& etype(monat_1_1,etype_c)
& fact(monat_1_1,real)
& etype(c75,etype_c)
& fact(c75,real) ),
inference(pure_predicate_removal,[],[f10339]) ).
fof(f10347,plain,
! [X0,X1,X2] :
( member(X0,cons(X1,X2))
| ~ member(X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f10516,plain,
! [X0,X1,X2] :
( ? [X3] :
( mcont(X3,X2)
& obj(X3,X2)
& scar(X3,X2)
& subs(X3,stehen_1_b) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f160]) ).
fof(f10517,plain,
! [X0,X1,X2] :
( ? [X3] :
( mcont(X3,X2)
& obj(X3,X2)
& scar(X3,X2)
& subs(X3,stehen_1_b) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(flattening,[],[f10516]) ).
fof(f10551,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ attr(X0,X1)
| ~ attr(X3,X2)
| ~ attr(X5,X6)
| ~ obj(X4,X0)
| ~ sub(X1,name_1_1)
| ~ sub(X2,name_1_1) ),
inference(ennf_transformation,[],[f10189]) ).
fof(f10552,plain,
! [X0,X1] : member(X0,cons(X0,X1)),
inference(cnf_transformation,[],[f1]) ).
fof(f10553,plain,
! [X2,X0,X1] :
( ~ member(X0,X2)
| member(X0,cons(X1,X2)) ),
inference(cnf_transformation,[],[f10347]) ).
fof(f10818,plain,
! [X2,X0,X1] :
( ~ sub(X0,X1)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0)
| obj(sK51(X2),X2) ),
inference(cnf_transformation,[],[f10517]) ).
fof(f20769,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ sub(X2,name_1_1)
| ~ sub(X1,name_1_1)
| ~ obj(X4,X0)
| ~ attr(X5,X6)
| ~ attr(X3,X2)
| ~ attr(X0,X1) ),
inference(cnf_transformation,[],[f10551]) ).
fof(f20795,plain,
attr(c22,c24),
inference(cnf_transformation,[],[f10344]) ).
fof(f20798,plain,
sub(c16,name_1_1),
inference(cnf_transformation,[],[f10344]) ).
fof(f20800,plain,
attr(c15,c16),
inference(cnf_transformation,[],[f10344]) ).
fof(f20801,plain,
! [X0,X1] : ~ member(X0,cons(X0,X1)),
inference(consistent_polarity_flipping,[],[f10552]) ).
fof(f20802,plain,
! [X2,X0,X1] :
( ~ member(X0,cons(X1,X2))
| member(X0,X2) ),
inference(consistent_polarity_flipping,[],[f10553]) ).
fof(f21001,plain,
! [X2,X0,X1] :
( sub(X0,X1)
| member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| attr(X2,X0)
| obj(sK51(X2),X2) ),
inference(consistent_polarity_flipping,[],[f10818]) ).
fof(f30551,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( sub(X2,name_1_1)
| sub(X1,name_1_1)
| ~ obj(X4,X0)
| attr(X5,X6)
| attr(X3,X2)
| attr(X0,X1) ),
inference(consistent_polarity_flipping,[],[f20769]) ).
fof(f30552,plain,
~ attr(c15,c16),
inference(consistent_polarity_flipping,[],[f20800]) ).
fof(f30554,plain,
~ sub(c16,name_1_1),
inference(consistent_polarity_flipping,[],[f20798]) ).
fof(f30556,plain,
~ attr(c22,c24),
inference(consistent_polarity_flipping,[],[f20795]) ).
fof(f30570,definition,
( spl63_1
<=> ! [X6,X5] : attr(X5,X6) ),
introduced(definition,[new_symbols(definition,[spl63_1])],[avatar_definition]) ).
fof(f30571,plain,
( ! [X6,X5] : attr(X5,X6)
| ~ spl63_1 ),
inference(avatar_component_clause,[],[f30570]) ).
fof(f30573,definition,
( spl63_2
<=> ! [X4,X0,X1] :
( sub(X1,name_1_1)
| ~ obj(X4,X0)
| attr(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl63_2])],[avatar_definition]) ).
fof(f30574,plain,
( ! [X0,X1,X4] :
( ~ obj(X4,X0)
| sub(X1,name_1_1)
| attr(X0,X1) )
| ~ spl63_2 ),
inference(avatar_component_clause,[],[f30573]) ).
fof(f30576,definition,
( spl63_3
<=> ! [X2,X3] :
( sub(X2,name_1_1)
| attr(X3,X2) ) ),
introduced(definition,[new_symbols(definition,[spl63_3])],[avatar_definition]) ).
fof(f30577,plain,
( ! [X2,X3] :
( attr(X3,X2)
| sub(X2,name_1_1) )
| ~ spl63_3 ),
inference(avatar_component_clause,[],[f30576]) ).
fof(f30578,plain,
( spl63_1
| spl63_2
| spl63_3 ),
inference(avatar_split_clause,[],[f30551,f30576,f30573,f30570]) ).
fof(f30777,plain,
( $false
| ~ spl63_1 ),
inference(backward_subsumption_resolution,[],[f30556,f30571]) ).
fof(f30781,plain,
~ spl63_1,
inference(avatar_contradiction_clause,[],[f30777]) ).
fof(f30782,plain,
( sub(c16,name_1_1)
| ~ spl63_3 ),
inference(resolution,[],[f30552,f30577]) ).
fof(f30783,plain,
( $false
| ~ spl63_3 ),
inference(forward_subsumption_resolution,[],[f30782,f30554]) ).
fof(f30784,plain,
~ spl63_3,
inference(avatar_contradiction_clause,[],[f30783]) ).
fof(f32526,plain,
! [X2,X0,X1] :
( sub(X1,X0)
| attr(X2,X1)
| obj(sK51(X2),X2)
| member(X0,cons(familiename_1_1,cons(name_1_1,nil))) ),
inference(resolution,[],[f21001,f20802]) ).
fof(f33769,plain,
! [X2,X0,X1] :
( sub(X1,X0)
| attr(X2,X1)
| obj(sK51(X2),X2)
| member(X0,cons(name_1_1,nil)) ),
inference(resolution,[],[f32526,f20802]) ).
fof(f38442,plain,
! [X0,X1] :
( sub(X0,name_1_1)
| attr(X1,X0)
| obj(sK51(X1),X1) ),
inference(resolution,[],[f33769,f20801]) ).
fof(f38444,plain,
( ! [X0,X1] :
( sub(X0,name_1_1)
| attr(X1,X0) )
| ~ spl63_2 ),
inference(forward_subsumption_resolution,[],[f38442,f30574]) ).
fof(f38445,plain,
( spl63_3
| ~ spl63_2 ),
inference(avatar_split_clause,[],[f38444,f30573,f30576]) ).
cnf(s1,plain,
( spl63_1
| spl63_2
| spl63_3 ),
inference(sat_conversion,[],[f30578]) ).
cnf(s24,plain,
~ spl63_1,
inference(sat_conversion,[],[f30781]) ).
cnf(s25,plain,
~ spl63_3,
inference(sat_conversion,[],[f30784]) ).
cnf(s853,plain,
( ~ spl63_2
| spl63_3 ),
inference(sat_conversion,[],[f38445]) ).
cnf(s855,plain,
~ spl63_2,
inference(rat,[],[s853,s25]) ).
cnf(s856,plain,
$false,
inference(rat,[],[s1,s25,s855,s24]) ).
fof(f38446,plain,
$false,
inference(avatar_sat_refutation,[],[s856]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+29 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.19 % Computer : n013.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 23:12:07 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.07/0.22 Running first-order model finding
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.24/1.81 % (1679038)Will run a generic schedule for satisfiability detection.
% 6.24/1.81 % (1679045)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3292452399:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 6.24/1.81 % (1679044)% WARNING: option uhcvi not known.
% 6.24/1.81 % (1679043)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4167532006_2998 on theBenchmark for (2998ds/0Mi)
% 6.24/1.81 % (1679044)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2156923366:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 6.24/1.81 % (1679046)dis+10_1_sil=32000:sp=arity:random_seed=3031617764:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 6.24/1.81 % (1679047)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=500863630:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 6.24/1.81 % (1679048)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3234868676:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 6.24/1.81 % (1679049)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3639777064:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 6.24/1.81 % (1679046)Instruction limit reached!
% 6.24/1.81 % (1679046)------------------------------
% 6.24/1.81 % (1679046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679046)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679046)Termination reason: Instruction limit
% 6.24/1.81 % (1679046)Termination phase: Saturation
% 6.24/1.81 % (1679046)Time elapsed: 0.060 s
% 6.24/1.81 % (1679046)Peak memory usage: 26 MB
% 6.24/1.81 % (1679046)Instructions burned: 104 (million)
% 6.24/1.81 % (1679047)Instruction limit reached!
% 6.24/1.81 % (1679047)------------------------------
% 6.24/1.81 % (1679047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679047)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679047)Termination reason: Instruction limit
% 6.24/1.81 % (1679047)Termination phase: Blocked clause elimination
% 6.24/1.81 % (1679047)Time elapsed: 0.074 s
% 6.24/1.81 % (1679047)Peak memory usage: 27 MB
% 6.24/1.81 % (1679047)Instructions burned: 117 (million)
% 6.24/1.81 % (1679048)Instruction limit reached!
% 6.24/1.81 % (1679048)------------------------------
% 6.24/1.81 % (1679048)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679048)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679048)Termination reason: Instruction limit
% 6.24/1.81 % (1679048)Termination phase: Saturation
% 6.24/1.81 % (1679048)Time elapsed: 0.074 s
% 6.24/1.81 % (1679048)Peak memory usage: 28 MB
% 6.24/1.81 % (1679048)Instructions burned: 133 (million)
% 6.24/1.81 % (1679057)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3050688688:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 6.24/1.81 % (1679049)Instruction limit reached!
% 6.24/1.81 % (1679049)------------------------------
% 6.24/1.81 % (1679049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679049)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679049)Termination reason: Instruction limit
% 6.24/1.81 % (1679049)Termination phase: Saturation
% 6.24/1.81 % (1679049)Time elapsed: 0.092 s
% 6.24/1.81 % (1679049)Peak memory usage: 30 MB
% 6.24/1.81 % (1679049)Instructions burned: 159 (million)
% 6.24/1.81 % (1679058)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3088022901:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 6.24/1.81 % (1679059)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=514566914:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 6.24/1.81 % (1679062)ott-21_1_sil=16000:fs=off:random_seed=1218687494:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 6.24/1.81 % (1679058)Instruction limit reached!
% 6.24/1.81 % (1679058)------------------------------
% 6.24/1.81 % (1679058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679058)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679058)Termination reason: Instruction limit
% 6.24/1.81 % (1679058)Termination phase: Blocked clause elimination
% 6.24/1.81 % (1679058)Time elapsed: 0.076 s
% 6.24/1.81 % (1679058)Peak memory usage: 28 MB
% 6.24/1.81 % (1679058)Instructions burned: 131 (million)
% 6.24/1.81 % (1679065)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4117689192:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 6.24/1.81 % (1679062)Instruction limit reached!
% 6.24/1.81 % (1679062)------------------------------
% 6.24/1.81 % (1679062)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679062)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679062)Termination reason: Instruction limit
% 6.24/1.81 % (1679062)Termination phase: Saturation
% 6.24/1.81 % (1679062)Time elapsed: 0.092 s
% 6.24/1.81 % (1679062)Peak memory usage: 28 MB
% 6.24/1.81 % (1679062)Instructions burned: 181 (million)
% 6.24/1.81 % (1679067)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2232350389:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 6.24/1.81 % TRYING [1]
% 6.24/1.81 % TRYING [1]
% 6.24/1.81 % TRYING [2]
% 6.24/1.81 % TRYING [2]
% 6.24/1.81 % (1679057)Instruction limit reached!
% 6.24/1.81 % (1679057)------------------------------
% 6.24/1.81 % (1679057)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679057)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679057)Termination reason: Instruction limit
% 6.24/1.81 % (1679057)Termination phase: Finite model building constraint generation
% 6.24/1.81 % (1679057)Time elapsed: 0.331 s
% 6.24/1.81 % (1679057)Peak memory usage: 54 MB
% 6.24/1.81 % (1679057)Instructions burned: 714 (million)
% 6.24/1.81 % TRYING [3]
% 6.24/1.81 % TRYING [1]
% 6.24/1.81 % (1679059)Instruction limit reached!
% 6.24/1.81 % (1679059)------------------------------
% 6.24/1.81 % (1679059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679059)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679059)Termination reason: Instruction limit
% 6.24/1.81 % (1679059)Termination phase: Saturation
% 6.24/1.81 % (1679059)Time elapsed: 0.341 s
% 6.24/1.81 % (1679059)Peak memory usage: 33 MB
% 6.24/1.81 % (1679059)Instructions burned: 685 (million)
% 6.24/1.81 % (1679069)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2524984214:i=1179_2993 on theBenchmark for (2993ds/1179Mi)
% 6.24/1.81 % (1679065)Instruction limit reached!
% 6.24/1.81 % (1679065)------------------------------
% 6.24/1.81 % (1679065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679065)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679065)Termination reason: Instruction limit
% 6.24/1.81 % (1679065)Termination phase: Saturation
% 6.24/1.81 % (1679065)Time elapsed: 0.254 s
% 6.24/1.81 % (1679065)Peak memory usage: 38 MB
% 6.24/1.81 % (1679065)Instructions burned: 477 (million)
% 6.24/1.81 % (1679071)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3313515431:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 6.24/1.81 % (1679072)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=1191011477: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)
% 6.24/1.81 % (1679067)Instruction limit reached!
% 6.24/1.81 % (1679067)------------------------------
% 6.24/1.81 % (1679067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679067)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679067)Termination reason: Instruction limit
% 6.24/1.81 % (1679067)Termination phase: Finite model building SAT solving
% 6.24/1.81 % (1679067)Time elapsed: 0.311 s
% 6.24/1.81 % (1679067)Peak memory usage: 38 MB
% 6.24/1.81 % (1679067)Instructions burned: 866 (million)
% 6.24/1.81 % (1679075)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1000929831:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 6.24/1.81 % TRYING [4]
% 6.24/1.81 % (1679072)Instruction limit reached!
% 6.24/1.81 % (1679072)------------------------------
% 6.24/1.81 % (1679072)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679072)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679072)Termination reason: Instruction limit
% 6.24/1.81 % (1679072)Termination phase: Saturation
% 6.24/1.81 % (1679072)Time elapsed: 0.371 s
% 6.24/1.81 % (1679072)Peak memory usage: 43 MB
% 6.24/1.81 % (1679072)Instructions burned: 693 (million)
% 6.24/1.81 % (1679077)fmb+10_1_sil=64000:random_seed=3081960485:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 6.24/1.81 % (1679071)Instruction limit reached!
% 6.24/1.81 % (1679071)------------------------------
% 6.24/1.81 % (1679071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679071)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679071)Termination reason: Instruction limit
% 6.24/1.81 % (1679071)Termination phase: Finite model building constraint generation
% 6.24/1.81 % (1679071)Time elapsed: 0.427 s
% 6.24/1.81 % (1679071)Peak memory usage: 92 MB
% 6.24/1.81 % (1679071)Instructions burned: 889 (million)
% 6.24/1.81 % (1679079)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2625061277:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 6.24/1.81 % (1679075)Instruction limit reached!
% 6.24/1.81 % (1679075)------------------------------
% 6.24/1.81 % (1679075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679075)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679075)Termination reason: Instruction limit
% 6.24/1.81 % (1679075)Termination phase: Saturation
% 6.24/1.81 % (1679075)Time elapsed: 0.431 s
% 6.24/1.81 % (1679075)Peak memory usage: 44 MB
% 6.24/1.81 % (1679075)Instructions burned: 879 (million)
% 6.24/1.81 % (1679081)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3106962924:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 6.24/1.81 % (1679069)Instruction limit reached!
% 6.24/1.81 % (1679069)------------------------------
% 6.24/1.81 % (1679069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.81 % (1679069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.81 % (1679069)CaDiCaL version: 2.1.3
% 6.24/1.81 % (1679069)Termination reason: Instruction limit
% 6.24/1.81 % (1679069)Termination phase: Saturation
% 6.24/1.81 % (1679069)Time elapsed: 0.633 s
% 6.24/1.81 % (1679069)Peak memory usage: 54 MB
% 6.24/1.81 % (1679069)Instructions burned: 1180 (million)
% 6.24/1.81 % TRYING [1]
% 6.24/1.81 % (1679083)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2601013323:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 6.24/1.81 % TRYING [20]
% 6.24/1.81 % TRYING [2]
% 6.24/1.81 % TRYING [8]
% 6.24/1.81 % TRYING [5]
% 6.24/1.81 % (1679044) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1679038-1679044"...
% 6.24/1.81 % (1679044)...printing done.
% 6.24/1.81 % (1679044)Refutation found. Thanks to Tanya!
% 6.24/1.81 % SZS status Theorem for theBenchmark
% 6.24/1.81 % SZS output start Proof for theBenchmark
% See solution above
% 6.24/1.82 % (1679044)------------------------------
% 6.24/1.82 % (1679044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.24/1.82 % (1679044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.24/1.82 % (1679044)CaDiCaL version: 2.1.3
% 6.24/1.82 % (1679044)Termination reason: Refutation
% 6.24/1.82 % (1679044)Time elapsed: 1.353 s
% 6.24/1.82 % (1679044)Peak memory usage: 51 MB
% 6.24/1.82 % (1679044)Instructions burned: 2325 (million)
% 6.24/1.82 % (1679038)Success in time 1.581 s
% 6.24/1.82 % Vampire exiting
%------------------------------------------------------------------------------