%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR115+44 : 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 : n018.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:38 AM UTC 2026
% Result : Theorem 3.47s 0.92s
% Output : Refutation 3.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 13
% Syntax : Number of formulae : 97 ( 19 unt; 7 def)
% Number of atoms : 1354 ( 0 equ)
% Maximal formula atoms : 195 ( 13 avg)
% Number of connectives : 1437 ( 180 ~; 150 |;1097 &)
% ( 7 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 195 ( 16 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 31 ( 30 usr; 8 prp; 0-8 aty)
% Number of functors : 59 ( 59 usr; 56 con; 0-3 aty)
% Number of variables : 139 ( 0 sgn 116 !; 23 ?)
% 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(f159,axiom,
! [X0,X1,X2] :
( ( attr(X2,X0)
& member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
& sub(X0,X1) )
=> ? [X3] :
( arg1(X3,X2)
& arg2(X3,X2)
& subs(X3,hei__337en_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',attr_name_hei__337en_1_1) ).
fof(f161,axiom,
! [X0,X1,X2] :
( ( arg1(X0,X1)
& arg2(X0,X2)
& subs(X0,hei__337en_1_1) )
=> ? [X3,X4] :
( arg1(X4,X1)
& arg2(X4,X2)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR004+0.ax',hei__337en_1_1__bezeichnen_1_1_als) ).
fof(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(X0,firma_1_1)
& sub(X2,name_1_1)
& val(X1,bmw_0)
& val(X2,bmw_0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',synth_qa07_007_mira_news_1253) ).
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(X0,firma_1_1)
& sub(X2,name_1_1)
& val(X1,bmw_0)
& val(X2,bmw_0) ),
inference(negated_conjecture,[status(cth)],[f10188]) ).
fof(f10190,axiom,
( attr(c557,c558)
& sub(c557,firma_1_1)
& sub(c558,name_1_1)
& val(c558,bmw_0)
& attr(c564,c565)
& sub(c564,mensch_1_1)
& sub(c565,familiename_1_1)
& val(c565,roll_0)
& attr(c570,c571)
& sub(c570,mensch_1_1)
& sub(c571,familiename_1_1)
& val(c571,royce_0)
& pred(c572,kei_1_1)
& subs(c573,einstieg_1_1)
& prop(c582,britisch__1_1)
& sub(c582,nobelfirma_1_1)
& attr(c590,c591)
& sub(c590,stadt__1_1)
& sub(c591,name_1_1)
& val(c591,london_0)
& tupl_p8(c699,c557,c564,c570,c572,c573,c582,c590)
& assoc(nobelfirma_1_1,gro__337m__374tig_1_1)
& sub(nobelfirma_1_1,firma_1_1)
& sort(c557,d)
& sort(c557,io)
& card(c557,int1)
& etype(c557,int0)
& fact(c557,real)
& gener(c557,sp)
& quant(c557,one)
& refer(c557,det)
& varia(c557,con)
& sort(c558,na)
& card(c558,int1)
& etype(c558,int0)
& fact(c558,real)
& gener(c558,sp)
& quant(c558,one)
& refer(c558,indet)
& varia(c558,varia_c)
& sort(firma_1_1,d)
& sort(firma_1_1,io)
& card(firma_1_1,int1)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& quant(firma_1_1,one)
& refer(firma_1_1,refer_c)
& varia(firma_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(bmw_0,fe)
& sort(c564,d)
& card(c564,int1)
& etype(c564,int0)
& fact(c564,real)
& gener(c564,sp)
& quant(c564,one)
& refer(c564,det)
& varia(c564,con)
& sort(c565,na)
& card(c565,int1)
& etype(c565,int0)
& fact(c565,real)
& gener(c565,sp)
& quant(c565,one)
& refer(c565,indet)
& varia(c565,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(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(roll_0,fe)
& sort(c570,d)
& card(c570,int1)
& etype(c570,int0)
& fact(c570,real)
& gener(c570,sp)
& quant(c570,one)
& refer(c570,det)
& varia(c570,con)
& sort(c571,na)
& card(c571,int1)
& etype(c571,int0)
& fact(c571,real)
& gener(c571,sp)
& quant(c571,one)
& refer(c571,indet)
& varia(c571,varia_c)
& sort(royce_0,fe)
& sort(c572,o)
& card(c572,cons(x_constant,cons(int1,nil)))
& etype(c572,int1)
& fact(c572,real)
& gener(c572,gener_c)
& quant(c572,mult)
& refer(c572,indet)
& varia(c572,varia_c)
& sort(kei_1_1,o)
& card(kei_1_1,int1)
& etype(kei_1_1,int0)
& fact(kei_1_1,real)
& gener(kei_1_1,ge)
& quant(kei_1_1,one)
& refer(kei_1_1,refer_c)
& varia(kei_1_1,varia_c)
& sort(c573,ad)
& card(c573,int1)
& etype(c573,int0)
& fact(c573,real)
& gener(c573,gener_c)
& quant(c573,one)
& refer(c573,refer_c)
& varia(c573,varia_c)
& sort(einstieg_1_1,ad)
& card(einstieg_1_1,int1)
& etype(einstieg_1_1,int0)
& fact(einstieg_1_1,real)
& gener(einstieg_1_1,ge)
& quant(einstieg_1_1,one)
& refer(einstieg_1_1,refer_c)
& varia(einstieg_1_1,varia_c)
& sort(c582,d)
& sort(c582,io)
& card(c582,int1)
& etype(c582,int0)
& fact(c582,real)
& gener(c582,sp)
& quant(c582,one)
& refer(c582,det)
& varia(c582,con)
& sort(britisch__1_1,nq)
& sort(nobelfirma_1_1,d)
& sort(nobelfirma_1_1,io)
& card(nobelfirma_1_1,int1)
& etype(nobelfirma_1_1,int0)
& fact(nobelfirma_1_1,real)
& gener(nobelfirma_1_1,ge)
& quant(nobelfirma_1_1,one)
& refer(nobelfirma_1_1,refer_c)
& varia(nobelfirma_1_1,varia_c)
& sort(c590,d)
& sort(c590,io)
& card(c590,int1)
& etype(c590,int0)
& fact(c590,real)
& gener(c590,sp)
& quant(c590,one)
& refer(c590,det)
& varia(c590,con)
& sort(c591,na)
& card(c591,int1)
& etype(c591,int0)
& fact(c591,real)
& gener(c591,sp)
& quant(c591,one)
& refer(c591,indet)
& varia(c591,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(london_0,fe)
& sort(c699,ent)
& card(c699,card_c)
& etype(c699,etype_c)
& fact(c699,real)
& gener(c699,gener_c)
& quant(c699,quant_c)
& refer(c699,refer_c)
& varia(c699,varia_c)
& sort(gro__337m__374tig_1_1,nq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ave07_era5_synth_qa07_007_mira_news_1253) ).
fof(f10191,plain,
( attr(c557,c558)
& sub(c557,firma_1_1)
& sub(c558,name_1_1)
& val(c558,bmw_0)
& attr(c564,c565)
& sub(c564,mensch_1_1)
& sub(c565,familiename_1_1)
& val(c565,roll_0)
& attr(c570,c571)
& sub(c570,mensch_1_1)
& sub(c571,familiename_1_1)
& val(c571,royce_0)
& pred(c572,kei_1_1)
& subs(c573,einstieg_1_1)
& prop(c582,britisch__1_1)
& sub(c582,nobelfirma_1_1)
& attr(c590,c591)
& sub(c590,stadt__1_1)
& sub(c591,name_1_1)
& val(c591,london_0)
& assoc(nobelfirma_1_1,gro__337m__374tig_1_1)
& sub(nobelfirma_1_1,firma_1_1)
& sort(c557,d)
& sort(c557,io)
& card(c557,int1)
& etype(c557,int0)
& fact(c557,real)
& gener(c557,sp)
& quant(c557,one)
& refer(c557,det)
& varia(c557,con)
& sort(c558,na)
& card(c558,int1)
& etype(c558,int0)
& fact(c558,real)
& gener(c558,sp)
& quant(c558,one)
& refer(c558,indet)
& varia(c558,varia_c)
& sort(firma_1_1,d)
& sort(firma_1_1,io)
& card(firma_1_1,int1)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& quant(firma_1_1,one)
& refer(firma_1_1,refer_c)
& varia(firma_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(bmw_0,fe)
& sort(c564,d)
& card(c564,int1)
& etype(c564,int0)
& fact(c564,real)
& gener(c564,sp)
& quant(c564,one)
& refer(c564,det)
& varia(c564,con)
& sort(c565,na)
& card(c565,int1)
& etype(c565,int0)
& fact(c565,real)
& gener(c565,sp)
& quant(c565,one)
& refer(c565,indet)
& varia(c565,varia_c)
& sort(mensch_1_1,d)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& sort(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(roll_0,fe)
& sort(c570,d)
& card(c570,int1)
& etype(c570,int0)
& fact(c570,real)
& gener(c570,sp)
& quant(c570,one)
& refer(c570,det)
& varia(c570,con)
& sort(c571,na)
& card(c571,int1)
& etype(c571,int0)
& fact(c571,real)
& gener(c571,sp)
& quant(c571,one)
& refer(c571,indet)
& varia(c571,varia_c)
& sort(royce_0,fe)
& sort(c572,o)
& card(c572,cons(x_constant,cons(int1,nil)))
& etype(c572,int1)
& fact(c572,real)
& gener(c572,gener_c)
& quant(c572,mult)
& refer(c572,indet)
& varia(c572,varia_c)
& sort(kei_1_1,o)
& card(kei_1_1,int1)
& etype(kei_1_1,int0)
& fact(kei_1_1,real)
& gener(kei_1_1,ge)
& quant(kei_1_1,one)
& refer(kei_1_1,refer_c)
& varia(kei_1_1,varia_c)
& sort(c573,ad)
& card(c573,int1)
& etype(c573,int0)
& fact(c573,real)
& gener(c573,gener_c)
& quant(c573,one)
& refer(c573,refer_c)
& varia(c573,varia_c)
& sort(einstieg_1_1,ad)
& card(einstieg_1_1,int1)
& etype(einstieg_1_1,int0)
& fact(einstieg_1_1,real)
& gener(einstieg_1_1,ge)
& quant(einstieg_1_1,one)
& refer(einstieg_1_1,refer_c)
& varia(einstieg_1_1,varia_c)
& sort(c582,d)
& sort(c582,io)
& card(c582,int1)
& etype(c582,int0)
& fact(c582,real)
& gener(c582,sp)
& quant(c582,one)
& refer(c582,det)
& varia(c582,con)
& sort(britisch__1_1,nq)
& sort(nobelfirma_1_1,d)
& sort(nobelfirma_1_1,io)
& card(nobelfirma_1_1,int1)
& etype(nobelfirma_1_1,int0)
& fact(nobelfirma_1_1,real)
& gener(nobelfirma_1_1,ge)
& quant(nobelfirma_1_1,one)
& refer(nobelfirma_1_1,refer_c)
& varia(nobelfirma_1_1,varia_c)
& sort(c590,d)
& sort(c590,io)
& card(c590,int1)
& etype(c590,int0)
& fact(c590,real)
& gener(c590,sp)
& quant(c590,one)
& refer(c590,det)
& varia(c590,con)
& sort(c591,na)
& card(c591,int1)
& etype(c591,int0)
& fact(c591,real)
& gener(c591,sp)
& quant(c591,one)
& refer(c591,indet)
& varia(c591,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(london_0,fe)
& sort(c699,ent)
& card(c699,card_c)
& etype(c699,etype_c)
& fact(c699,real)
& gener(c699,gener_c)
& quant(c699,quant_c)
& refer(c699,refer_c)
& varia(c699,varia_c)
& sort(gro__337m__374tig_1_1,nq) ),
inference(pure_predicate_removal,[],[f10190]) ).
fof(f10327,plain,
( attr(c557,c558)
& sub(c557,firma_1_1)
& sub(c558,name_1_1)
& val(c558,bmw_0)
& attr(c564,c565)
& sub(c564,mensch_1_1)
& sub(c565,familiename_1_1)
& val(c565,roll_0)
& attr(c570,c571)
& sub(c570,mensch_1_1)
& sub(c571,familiename_1_1)
& val(c571,royce_0)
& pred(c572,kei_1_1)
& subs(c573,einstieg_1_1)
& prop(c582,britisch__1_1)
& sub(c582,nobelfirma_1_1)
& attr(c590,c591)
& sub(c590,stadt__1_1)
& sub(c591,name_1_1)
& val(c591,london_0)
& assoc(nobelfirma_1_1,gro__337m__374tig_1_1)
& sub(nobelfirma_1_1,firma_1_1)
& card(c557,int1)
& etype(c557,int0)
& fact(c557,real)
& gener(c557,sp)
& quant(c557,one)
& refer(c557,det)
& varia(c557,con)
& card(c558,int1)
& etype(c558,int0)
& fact(c558,real)
& gener(c558,sp)
& quant(c558,one)
& refer(c558,indet)
& varia(c558,varia_c)
& card(firma_1_1,int1)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& quant(firma_1_1,one)
& refer(firma_1_1,refer_c)
& varia(firma_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(c564,int1)
& etype(c564,int0)
& fact(c564,real)
& gener(c564,sp)
& quant(c564,one)
& refer(c564,det)
& varia(c564,con)
& card(c565,int1)
& etype(c565,int0)
& fact(c565,real)
& gener(c565,sp)
& quant(c565,one)
& refer(c565,indet)
& varia(c565,varia_c)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& quant(mensch_1_1,one)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& card(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(c570,int1)
& etype(c570,int0)
& fact(c570,real)
& gener(c570,sp)
& quant(c570,one)
& refer(c570,det)
& varia(c570,con)
& card(c571,int1)
& etype(c571,int0)
& fact(c571,real)
& gener(c571,sp)
& quant(c571,one)
& refer(c571,indet)
& varia(c571,varia_c)
& card(c572,cons(x_constant,cons(int1,nil)))
& etype(c572,int1)
& fact(c572,real)
& gener(c572,gener_c)
& quant(c572,mult)
& refer(c572,indet)
& varia(c572,varia_c)
& card(kei_1_1,int1)
& etype(kei_1_1,int0)
& fact(kei_1_1,real)
& gener(kei_1_1,ge)
& quant(kei_1_1,one)
& refer(kei_1_1,refer_c)
& varia(kei_1_1,varia_c)
& card(c573,int1)
& etype(c573,int0)
& fact(c573,real)
& gener(c573,gener_c)
& quant(c573,one)
& refer(c573,refer_c)
& varia(c573,varia_c)
& card(einstieg_1_1,int1)
& etype(einstieg_1_1,int0)
& fact(einstieg_1_1,real)
& gener(einstieg_1_1,ge)
& quant(einstieg_1_1,one)
& refer(einstieg_1_1,refer_c)
& varia(einstieg_1_1,varia_c)
& card(c582,int1)
& etype(c582,int0)
& fact(c582,real)
& gener(c582,sp)
& quant(c582,one)
& refer(c582,det)
& varia(c582,con)
& card(nobelfirma_1_1,int1)
& etype(nobelfirma_1_1,int0)
& fact(nobelfirma_1_1,real)
& gener(nobelfirma_1_1,ge)
& quant(nobelfirma_1_1,one)
& refer(nobelfirma_1_1,refer_c)
& varia(nobelfirma_1_1,varia_c)
& card(c590,int1)
& etype(c590,int0)
& fact(c590,real)
& gener(c590,sp)
& quant(c590,one)
& refer(c590,det)
& varia(c590,con)
& card(c591,int1)
& etype(c591,int0)
& fact(c591,real)
& gener(c591,sp)
& quant(c591,one)
& refer(c591,indet)
& varia(c591,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(c699,card_c)
& etype(c699,etype_c)
& fact(c699,real)
& gener(c699,gener_c)
& quant(c699,quant_c)
& refer(c699,refer_c)
& varia(c699,varia_c) ),
inference(pure_predicate_removal,[],[f10191]) ).
fof(f10330,plain,
( attr(c557,c558)
& sub(c557,firma_1_1)
& sub(c558,name_1_1)
& val(c558,bmw_0)
& attr(c564,c565)
& sub(c564,mensch_1_1)
& sub(c565,familiename_1_1)
& val(c565,roll_0)
& attr(c570,c571)
& sub(c570,mensch_1_1)
& sub(c571,familiename_1_1)
& val(c571,royce_0)
& pred(c572,kei_1_1)
& subs(c573,einstieg_1_1)
& prop(c582,britisch__1_1)
& sub(c582,nobelfirma_1_1)
& attr(c590,c591)
& sub(c590,stadt__1_1)
& sub(c591,name_1_1)
& val(c591,london_0)
& assoc(nobelfirma_1_1,gro__337m__374tig_1_1)
& sub(nobelfirma_1_1,firma_1_1)
& card(c557,int1)
& etype(c557,int0)
& fact(c557,real)
& gener(c557,sp)
& refer(c557,det)
& varia(c557,con)
& card(c558,int1)
& etype(c558,int0)
& fact(c558,real)
& gener(c558,sp)
& refer(c558,indet)
& varia(c558,varia_c)
& card(firma_1_1,int1)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& refer(firma_1_1,refer_c)
& varia(firma_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(c564,int1)
& etype(c564,int0)
& fact(c564,real)
& gener(c564,sp)
& refer(c564,det)
& varia(c564,con)
& card(c565,int1)
& etype(c565,int0)
& fact(c565,real)
& gener(c565,sp)
& refer(c565,indet)
& varia(c565,varia_c)
& card(mensch_1_1,int1)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& card(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(c570,int1)
& etype(c570,int0)
& fact(c570,real)
& gener(c570,sp)
& refer(c570,det)
& varia(c570,con)
& card(c571,int1)
& etype(c571,int0)
& fact(c571,real)
& gener(c571,sp)
& refer(c571,indet)
& varia(c571,varia_c)
& card(c572,cons(x_constant,cons(int1,nil)))
& etype(c572,int1)
& fact(c572,real)
& gener(c572,gener_c)
& refer(c572,indet)
& varia(c572,varia_c)
& card(kei_1_1,int1)
& etype(kei_1_1,int0)
& fact(kei_1_1,real)
& gener(kei_1_1,ge)
& refer(kei_1_1,refer_c)
& varia(kei_1_1,varia_c)
& card(c573,int1)
& etype(c573,int0)
& fact(c573,real)
& gener(c573,gener_c)
& refer(c573,refer_c)
& varia(c573,varia_c)
& card(einstieg_1_1,int1)
& etype(einstieg_1_1,int0)
& fact(einstieg_1_1,real)
& gener(einstieg_1_1,ge)
& refer(einstieg_1_1,refer_c)
& varia(einstieg_1_1,varia_c)
& card(c582,int1)
& etype(c582,int0)
& fact(c582,real)
& gener(c582,sp)
& refer(c582,det)
& varia(c582,con)
& card(nobelfirma_1_1,int1)
& etype(nobelfirma_1_1,int0)
& fact(nobelfirma_1_1,real)
& gener(nobelfirma_1_1,ge)
& refer(nobelfirma_1_1,refer_c)
& varia(nobelfirma_1_1,varia_c)
& card(c590,int1)
& etype(c590,int0)
& fact(c590,real)
& gener(c590,sp)
& refer(c590,det)
& varia(c590,con)
& card(c591,int1)
& etype(c591,int0)
& fact(c591,real)
& gener(c591,sp)
& refer(c591,indet)
& varia(c591,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(c699,card_c)
& etype(c699,etype_c)
& fact(c699,real)
& gener(c699,gener_c)
& refer(c699,refer_c)
& varia(c699,varia_c) ),
inference(pure_predicate_removal,[],[f10327]) ).
fof(f10333,plain,
( attr(c557,c558)
& sub(c557,firma_1_1)
& sub(c558,name_1_1)
& val(c558,bmw_0)
& attr(c564,c565)
& sub(c564,mensch_1_1)
& sub(c565,familiename_1_1)
& val(c565,roll_0)
& attr(c570,c571)
& sub(c570,mensch_1_1)
& sub(c571,familiename_1_1)
& val(c571,royce_0)
& pred(c572,kei_1_1)
& subs(c573,einstieg_1_1)
& prop(c582,britisch__1_1)
& sub(c582,nobelfirma_1_1)
& attr(c590,c591)
& sub(c590,stadt__1_1)
& sub(c591,name_1_1)
& val(c591,london_0)
& assoc(nobelfirma_1_1,gro__337m__374tig_1_1)
& sub(nobelfirma_1_1,firma_1_1)
& etype(c557,int0)
& fact(c557,real)
& gener(c557,sp)
& refer(c557,det)
& varia(c557,con)
& etype(c558,int0)
& fact(c558,real)
& gener(c558,sp)
& refer(c558,indet)
& varia(c558,varia_c)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& refer(firma_1_1,refer_c)
& varia(firma_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(c564,int0)
& fact(c564,real)
& gener(c564,sp)
& refer(c564,det)
& varia(c564,con)
& etype(c565,int0)
& fact(c565,real)
& gener(c565,sp)
& refer(c565,indet)
& varia(c565,varia_c)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& refer(mensch_1_1,refer_c)
& varia(mensch_1_1,varia_c)
& etype(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(c570,int0)
& fact(c570,real)
& gener(c570,sp)
& refer(c570,det)
& varia(c570,con)
& etype(c571,int0)
& fact(c571,real)
& gener(c571,sp)
& refer(c571,indet)
& varia(c571,varia_c)
& etype(c572,int1)
& fact(c572,real)
& gener(c572,gener_c)
& refer(c572,indet)
& varia(c572,varia_c)
& etype(kei_1_1,int0)
& fact(kei_1_1,real)
& gener(kei_1_1,ge)
& refer(kei_1_1,refer_c)
& varia(kei_1_1,varia_c)
& etype(c573,int0)
& fact(c573,real)
& gener(c573,gener_c)
& refer(c573,refer_c)
& varia(c573,varia_c)
& etype(einstieg_1_1,int0)
& fact(einstieg_1_1,real)
& gener(einstieg_1_1,ge)
& refer(einstieg_1_1,refer_c)
& varia(einstieg_1_1,varia_c)
& etype(c582,int0)
& fact(c582,real)
& gener(c582,sp)
& refer(c582,det)
& varia(c582,con)
& etype(nobelfirma_1_1,int0)
& fact(nobelfirma_1_1,real)
& gener(nobelfirma_1_1,ge)
& refer(nobelfirma_1_1,refer_c)
& varia(nobelfirma_1_1,varia_c)
& etype(c590,int0)
& fact(c590,real)
& gener(c590,sp)
& refer(c590,det)
& varia(c590,con)
& etype(c591,int0)
& fact(c591,real)
& gener(c591,sp)
& refer(c591,indet)
& varia(c591,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(c699,etype_c)
& fact(c699,real)
& gener(c699,gener_c)
& refer(c699,refer_c)
& varia(c699,varia_c) ),
inference(pure_predicate_removal,[],[f10330]) ).
fof(f10336,plain,
( attr(c557,c558)
& sub(c557,firma_1_1)
& sub(c558,name_1_1)
& val(c558,bmw_0)
& attr(c564,c565)
& sub(c564,mensch_1_1)
& sub(c565,familiename_1_1)
& val(c565,roll_0)
& attr(c570,c571)
& sub(c570,mensch_1_1)
& sub(c571,familiename_1_1)
& val(c571,royce_0)
& pred(c572,kei_1_1)
& subs(c573,einstieg_1_1)
& prop(c582,britisch__1_1)
& sub(c582,nobelfirma_1_1)
& attr(c590,c591)
& sub(c590,stadt__1_1)
& sub(c591,name_1_1)
& val(c591,london_0)
& assoc(nobelfirma_1_1,gro__337m__374tig_1_1)
& sub(nobelfirma_1_1,firma_1_1)
& etype(c557,int0)
& fact(c557,real)
& gener(c557,sp)
& varia(c557,con)
& etype(c558,int0)
& fact(c558,real)
& gener(c558,sp)
& varia(c558,varia_c)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& varia(firma_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(c564,int0)
& fact(c564,real)
& gener(c564,sp)
& varia(c564,con)
& etype(c565,int0)
& fact(c565,real)
& gener(c565,sp)
& varia(c565,varia_c)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& varia(mensch_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(c570,int0)
& fact(c570,real)
& gener(c570,sp)
& varia(c570,con)
& etype(c571,int0)
& fact(c571,real)
& gener(c571,sp)
& varia(c571,varia_c)
& etype(c572,int1)
& fact(c572,real)
& gener(c572,gener_c)
& varia(c572,varia_c)
& etype(kei_1_1,int0)
& fact(kei_1_1,real)
& gener(kei_1_1,ge)
& varia(kei_1_1,varia_c)
& etype(c573,int0)
& fact(c573,real)
& gener(c573,gener_c)
& varia(c573,varia_c)
& etype(einstieg_1_1,int0)
& fact(einstieg_1_1,real)
& gener(einstieg_1_1,ge)
& varia(einstieg_1_1,varia_c)
& etype(c582,int0)
& fact(c582,real)
& gener(c582,sp)
& varia(c582,con)
& etype(nobelfirma_1_1,int0)
& fact(nobelfirma_1_1,real)
& gener(nobelfirma_1_1,ge)
& varia(nobelfirma_1_1,varia_c)
& etype(c590,int0)
& fact(c590,real)
& gener(c590,sp)
& varia(c590,con)
& etype(c591,int0)
& fact(c591,real)
& gener(c591,sp)
& varia(c591,varia_c)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& varia(stadt__1_1,varia_c)
& etype(c699,etype_c)
& fact(c699,real)
& gener(c699,gener_c)
& varia(c699,varia_c) ),
inference(pure_predicate_removal,[],[f10333]) ).
fof(f10341,plain,
( attr(c557,c558)
& sub(c557,firma_1_1)
& sub(c558,name_1_1)
& val(c558,bmw_0)
& attr(c564,c565)
& sub(c564,mensch_1_1)
& sub(c565,familiename_1_1)
& val(c565,roll_0)
& attr(c570,c571)
& sub(c570,mensch_1_1)
& sub(c571,familiename_1_1)
& val(c571,royce_0)
& pred(c572,kei_1_1)
& subs(c573,einstieg_1_1)
& prop(c582,britisch__1_1)
& sub(c582,nobelfirma_1_1)
& attr(c590,c591)
& sub(c590,stadt__1_1)
& sub(c591,name_1_1)
& val(c591,london_0)
& assoc(nobelfirma_1_1,gro__337m__374tig_1_1)
& sub(nobelfirma_1_1,firma_1_1)
& etype(c557,int0)
& fact(c557,real)
& gener(c557,sp)
& etype(c558,int0)
& fact(c558,real)
& gener(c558,sp)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& gener(firma_1_1,ge)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& gener(name_1_1,ge)
& etype(c564,int0)
& fact(c564,real)
& gener(c564,sp)
& etype(c565,int0)
& fact(c565,real)
& gener(c565,sp)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& gener(mensch_1_1,ge)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& gener(familiename_1_1,ge)
& etype(c570,int0)
& fact(c570,real)
& gener(c570,sp)
& etype(c571,int0)
& fact(c571,real)
& gener(c571,sp)
& etype(c572,int1)
& fact(c572,real)
& gener(c572,gener_c)
& etype(kei_1_1,int0)
& fact(kei_1_1,real)
& gener(kei_1_1,ge)
& etype(c573,int0)
& fact(c573,real)
& gener(c573,gener_c)
& etype(einstieg_1_1,int0)
& fact(einstieg_1_1,real)
& gener(einstieg_1_1,ge)
& etype(c582,int0)
& fact(c582,real)
& gener(c582,sp)
& etype(nobelfirma_1_1,int0)
& fact(nobelfirma_1_1,real)
& gener(nobelfirma_1_1,ge)
& etype(c590,int0)
& fact(c590,real)
& gener(c590,sp)
& etype(c591,int0)
& fact(c591,real)
& gener(c591,sp)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& gener(stadt__1_1,ge)
& etype(c699,etype_c)
& fact(c699,real)
& gener(c699,gener_c) ),
inference(pure_predicate_removal,[],[f10336]) ).
fof(f10346,plain,
( attr(c557,c558)
& sub(c557,firma_1_1)
& sub(c558,name_1_1)
& val(c558,bmw_0)
& attr(c564,c565)
& sub(c564,mensch_1_1)
& sub(c565,familiename_1_1)
& val(c565,roll_0)
& attr(c570,c571)
& sub(c570,mensch_1_1)
& sub(c571,familiename_1_1)
& val(c571,royce_0)
& pred(c572,kei_1_1)
& subs(c573,einstieg_1_1)
& prop(c582,britisch__1_1)
& sub(c582,nobelfirma_1_1)
& attr(c590,c591)
& sub(c590,stadt__1_1)
& sub(c591,name_1_1)
& val(c591,london_0)
& assoc(nobelfirma_1_1,gro__337m__374tig_1_1)
& sub(nobelfirma_1_1,firma_1_1)
& etype(c557,int0)
& fact(c557,real)
& etype(c558,int0)
& fact(c558,real)
& etype(firma_1_1,int0)
& fact(firma_1_1,real)
& etype(name_1_1,int0)
& fact(name_1_1,real)
& etype(c564,int0)
& fact(c564,real)
& etype(c565,int0)
& fact(c565,real)
& etype(mensch_1_1,int0)
& fact(mensch_1_1,real)
& etype(familiename_1_1,int0)
& fact(familiename_1_1,real)
& etype(c570,int0)
& fact(c570,real)
& etype(c571,int0)
& fact(c571,real)
& etype(c572,int1)
& fact(c572,real)
& etype(kei_1_1,int0)
& fact(kei_1_1,real)
& etype(c573,int0)
& fact(c573,real)
& etype(einstieg_1_1,int0)
& fact(einstieg_1_1,real)
& etype(c582,int0)
& fact(c582,real)
& etype(nobelfirma_1_1,int0)
& fact(nobelfirma_1_1,real)
& etype(c590,int0)
& fact(c590,real)
& etype(c591,int0)
& fact(c591,real)
& etype(stadt__1_1,int0)
& fact(stadt__1_1,real)
& etype(c699,etype_c)
& fact(c699,real) ),
inference(pure_predicate_removal,[],[f10341]) ).
fof(f10349,plain,
! [X0,X1,X2] :
( member(X0,cons(X1,X2))
| ~ member(X0,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f10514,plain,
! [X0,X1,X2] :
( ? [X3] :
( arg1(X3,X2)
& arg2(X3,X2)
& subs(X3,hei__337en_1_1) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(ennf_transformation,[],[f159]) ).
fof(f10515,plain,
! [X0,X1,X2] :
( ? [X3] :
( arg1(X3,X2)
& arg2(X3,X2)
& subs(X3,hei__337en_1_1) )
| ~ attr(X2,X0)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1) ),
inference(flattening,[],[f10514]) ).
fof(f10518,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( arg1(X4,X1)
& arg2(X4,X2)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(ennf_transformation,[],[f161]) ).
fof(f10519,plain,
! [X0,X1,X2] :
( ? [X3,X4] :
( arg1(X4,X1)
& arg2(X4,X2)
& hsit(X0,X3)
& mcont(X3,X4)
& obj(X3,X1)
& subr(X4,rprs_0)
& subs(X3,bezeichnen_1_1) )
| ~ arg1(X0,X1)
| ~ arg2(X0,X2)
| ~ subs(X0,hei__337en_1_1) ),
inference(flattening,[],[f10518]) ).
fof(f10551,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ attr(X0,X1)
| ~ attr(X3,X2)
| ~ attr(X5,X6)
| ~ obj(X4,X0)
| ~ sub(X1,name_1_1)
| ~ sub(X0,firma_1_1)
| ~ sub(X2,name_1_1)
| ~ val(X1,bmw_0)
| ~ val(X2,bmw_0) ),
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,cons(X1,X2))
| ~ member(X0,X2) ),
inference(cnf_transformation,[],[f10349]) ).
fof(f10812,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1)
| ~ attr(X2,X0)
| subs(sK50(X2),hei__337en_1_1) ),
inference(cnf_transformation,[],[f10515]) ).
fof(f10813,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X0,X1)
| ~ attr(X2,X0)
| arg2(sK50(X2),X2) ),
inference(cnf_transformation,[],[f10515]) ).
fof(f10814,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)
| arg1(sK50(X2),X2) ),
inference(cnf_transformation,[],[f10515]) ).
fof(f10821,plain,
! [X2,X0,X1] :
( ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| ~ arg1(X0,X1)
| obj(sK52(X0,X1,X2),X1) ),
inference(cnf_transformation,[],[f10519]) ).
fof(f20768,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ val(X2,bmw_0)
| ~ val(X1,bmw_0)
| ~ sub(X2,name_1_1)
| ~ sub(X0,firma_1_1)
| ~ sub(X1,name_1_1)
| ~ obj(X4,X0)
| ~ attr(X5,X6)
| ~ attr(X3,X2)
| ~ attr(X0,X1) ),
inference(cnf_transformation,[],[f10551]) ).
fof(f20826,plain,
attr(c564,c565),
inference(cnf_transformation,[],[f10346]) ).
fof(f20827,plain,
val(c558,bmw_0),
inference(cnf_transformation,[],[f10346]) ).
fof(f20828,plain,
sub(c558,name_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20829,plain,
sub(c557,firma_1_1),
inference(cnf_transformation,[],[f10346]) ).
fof(f20830,plain,
attr(c557,c558),
inference(cnf_transformation,[],[f10346]) ).
fof(f20984,plain,
! [X2,X0,X1] :
( ~ arg1(sK50(X2),X2)
| ~ member(X1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(X2,X0)
| ~ sub(X0,X1) ),
inference(consistent_polarity_flipping,[],[f10814]) ).
fof(f20990,plain,
! [X2,X0,X1] :
( ~ subs(X0,hei__337en_1_1)
| ~ arg2(X0,X2)
| arg1(X0,X1)
| obj(sK52(X0,X1,X2),X1) ),
inference(consistent_polarity_flipping,[],[f10821]) ).
fof(f21304,definition,
( spl63_1
<=> ! [X6,X5] : ~ attr(X5,X6) ),
introduced(definition,[new_symbols(definition,[spl63_1])],[avatar_definition]) ).
fof(f21305,plain,
( ! [X6,X5] : ~ attr(X5,X6)
| ~ spl63_1 ),
inference(avatar_component_clause,[],[f21304]) ).
fof(f21307,definition,
( spl63_2
<=> ! [X4,X0,X1] :
( ~ val(X1,bmw_0)
| ~ sub(X1,name_1_1)
| ~ sub(X0,firma_1_1)
| ~ attr(X0,X1)
| ~ obj(X4,X0) ) ),
introduced(definition,[new_symbols(definition,[spl63_2])],[avatar_definition]) ).
fof(f21308,plain,
( ! [X0,X1,X4] :
( ~ val(X1,bmw_0)
| ~ sub(X1,name_1_1)
| ~ sub(X0,firma_1_1)
| ~ attr(X0,X1)
| ~ obj(X4,X0) )
| ~ spl63_2 ),
inference(avatar_component_clause,[],[f21307]) ).
fof(f21310,definition,
( spl63_3
<=> ! [X2,X3] :
( ~ val(X2,bmw_0)
| ~ attr(X3,X2)
| ~ sub(X2,name_1_1) ) ),
introduced(definition,[new_symbols(definition,[spl63_3])],[avatar_definition]) ).
fof(f21311,plain,
( ! [X2,X3] :
( ~ val(X2,bmw_0)
| ~ attr(X3,X2)
| ~ sub(X2,name_1_1) )
| ~ spl63_3 ),
inference(avatar_component_clause,[],[f21310]) ).
fof(f21312,plain,
( spl63_1
| spl63_2
| spl63_3 ),
inference(avatar_split_clause,[],[f20768,f21310,f21307,f21304]) ).
fof(f21313,plain,
( ! [X0,X1] :
( ~ sub(c558,name_1_1)
| ~ sub(X0,firma_1_1)
| ~ attr(X0,c558)
| ~ obj(X1,X0) )
| ~ spl63_2 ),
inference(resolution,[],[f20827,f21308]) ).
fof(f21315,definition,
( spl63_4
<=> ! [X0,X1] :
( ~ sub(X0,firma_1_1)
| ~ obj(X1,X0)
| ~ attr(X0,c558) ) ),
introduced(definition,[new_symbols(definition,[spl63_4])],[avatar_definition]) ).
fof(f21316,plain,
( ! [X0,X1] :
( ~ attr(X0,c558)
| ~ obj(X1,X0)
| ~ sub(X0,firma_1_1) )
| ~ spl63_4 ),
inference(avatar_component_clause,[],[f21315]) ).
fof(f21318,definition,
( spl63_5
<=> sub(c558,name_1_1) ),
introduced(definition,[new_symbols(definition,[spl63_5])],[avatar_definition]) ).
fof(f21319,plain,
( sub(c558,name_1_1)
| ~ spl63_5 ),
inference(avatar_component_clause,[],[f21318]) ).
fof(f21324,plain,
spl63_5,
inference(avatar_split_clause,[],[f20828,f21318]) ).
fof(f21327,definition,
( spl63_6
<=> ! [X0] : ~ attr(X0,c558) ),
introduced(definition,[new_symbols(definition,[spl63_6])],[avatar_definition]) ).
fof(f21328,plain,
( ! [X0] : ~ attr(X0,c558)
| ~ spl63_6 ),
inference(avatar_component_clause,[],[f21327]) ).
fof(f21332,plain,
( $false
| ~ spl63_1 ),
inference(backward_subsumption_resolution,[],[f20826,f21305]) ).
fof(f21335,plain,
~ spl63_1,
inference(avatar_contradiction_clause,[],[f21332]) ).
fof(f21337,plain,
( ! [X0] :
( ~ attr(X0,c558)
| ~ sub(c558,name_1_1) )
| ~ spl63_3 ),
inference(resolution,[],[f21311,f20827]) ).
fof(f21338,plain,
( ~ spl63_5
| spl63_6
| ~ spl63_3 ),
inference(avatar_split_clause,[],[f21337,f21310,f21327,f21318]) ).
fof(f21339,plain,
( $false
| ~ spl63_6 ),
inference(forward_subsumption_resolution,[],[f20830,f21328]) ).
fof(f21340,plain,
~ spl63_6,
inference(avatar_contradiction_clause,[],[f21339]) ).
fof(f21341,plain,
( ! [X0,X1] :
( ~ sub(X0,firma_1_1)
| ~ attr(X0,c558)
| ~ obj(X1,X0) )
| ~ spl63_2
| ~ spl63_5 ),
inference(forward_subsumption_resolution,[],[f21313,f21319]) ).
fof(f21342,plain,
( spl63_4
| ~ spl63_2
| ~ spl63_5 ),
inference(avatar_split_clause,[],[f21341,f21318,f21307,f21315]) ).
fof(f21345,plain,
( ! [X0] :
( ~ obj(X0,c557)
| ~ sub(c557,firma_1_1) )
| ~ spl63_4 ),
inference(resolution,[],[f20830,f21316]) ).
fof(f21346,plain,
( ! [X0] : ~ obj(X0,c557)
| ~ spl63_4 ),
inference(forward_subsumption_resolution,[],[f21345,f20829]) ).
fof(f23055,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(familiename_1_1,cons(name_1_1,nil)))
| ~ attr(X2,X0)
| subs(sK50(X2),hei__337en_1_1)
| ~ sub(X0,X1) ),
inference(resolution,[],[f10812,f10553]) ).
fof(f23067,plain,
! [X2,X0,X1] :
( ~ member(X1,cons(familiename_1_1,cons(name_1_1,nil)))
| ~ attr(X2,X0)
| arg2(sK50(X2),X2)
| ~ sub(X0,X1) ),
inference(resolution,[],[f10813,f10553]) ).
fof(f23756,plain,
! [X2,X0,X1] :
( ~ member(X2,cons(name_1_1,nil))
| subs(sK50(X0),hei__337en_1_1)
| ~ sub(X1,X2)
| ~ attr(X0,X1) ),
inference(resolution,[],[f23055,f10553]) ).
fof(f23758,plain,
! [X2,X0,X1] :
( ~ member(X2,cons(name_1_1,nil))
| arg2(sK50(X0),X0)
| ~ sub(X1,X2)
| ~ attr(X0,X1) ),
inference(resolution,[],[f23067,f10553]) ).
fof(f27781,plain,
! [X0,X1] :
( ~ attr(X0,X1)
| ~ sub(X1,name_1_1)
| subs(sK50(X0),hei__337en_1_1) ),
inference(resolution,[],[f23756,f10552]) ).
fof(f27783,plain,
! [X0,X1] :
( ~ attr(X0,X1)
| ~ sub(X1,name_1_1)
| arg2(sK50(X0),X0) ),
inference(resolution,[],[f23758,f10552]) ).
fof(f27985,plain,
( ~ sub(c558,name_1_1)
| subs(sK50(c557),hei__337en_1_1) ),
inference(resolution,[],[f27781,f20830]) ).
fof(f28130,plain,
( subs(sK50(c557),hei__337en_1_1)
| ~ spl63_5 ),
inference(forward_subsumption_resolution,[],[f27985,f21319]) ).
fof(f28133,plain,
( ! [X0,X1] :
( ~ arg2(sK50(c557),X0)
| arg1(sK50(c557),X1)
| obj(sK52(sK50(c557),X1,X0),X1) )
| ~ spl63_5 ),
inference(resolution,[],[f28130,f20990]) ).
fof(f28356,plain,
( ~ sub(c558,name_1_1)
| arg2(sK50(c557),c557) ),
inference(resolution,[],[f27783,f20830]) ).
fof(f28519,plain,
( arg2(sK50(c557),c557)
| ~ spl63_5 ),
inference(forward_subsumption_resolution,[],[f28356,f21319]) ).
fof(f28521,plain,
( ! [X0] :
( obj(sK52(sK50(c557),X0,c557),X0)
| arg1(sK50(c557),X0) )
| ~ spl63_5 ),
inference(resolution,[],[f28519,f28133]) ).
fof(f28542,plain,
( arg1(sK50(c557),c557)
| ~ spl63_4
| ~ spl63_5 ),
inference(resolution,[],[f28521,f21346]) ).
fof(f28549,plain,
( ! [X0,X1] :
( ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c557,X1)
| ~ sub(X1,X0) )
| ~ spl63_4
| ~ spl63_5 ),
inference(resolution,[],[f28542,f20984]) ).
fof(f28579,definition,
( spl63_426
<=> ! [X0,X1] :
( ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ attr(c557,X1)
| ~ sub(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl63_426])],[avatar_definition]) ).
fof(f28580,plain,
( ! [X0,X1] :
( ~ attr(c557,X1)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ sub(X1,X0) )
| ~ spl63_426 ),
inference(avatar_component_clause,[],[f28579]) ).
fof(f28586,plain,
( spl63_426
| ~ spl63_4
| ~ spl63_5 ),
inference(avatar_split_clause,[],[f28549,f21318,f21315,f28579]) ).
fof(f28593,plain,
( ! [X0] :
( ~ sub(c558,X0)
| ~ member(X0,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil)))) )
| ~ spl63_426 ),
inference(resolution,[],[f28580,f20830]) ).
fof(f28598,plain,
( ~ member(name_1_1,cons(eigenname_1_1,cons(familiename_1_1,cons(name_1_1,nil))))
| ~ spl63_5
| ~ spl63_426 ),
inference(resolution,[],[f28593,f21319]) ).
fof(f28605,plain,
( ~ member(name_1_1,cons(familiename_1_1,cons(name_1_1,nil)))
| ~ spl63_5
| ~ spl63_426 ),
inference(resolution,[],[f28598,f10553]) ).
fof(f28612,plain,
( ~ member(name_1_1,cons(name_1_1,nil))
| ~ spl63_5
| ~ spl63_426 ),
inference(resolution,[],[f28605,f10553]) ).
fof(f28613,plain,
( $false
| ~ spl63_5
| ~ spl63_426 ),
inference(forward_subsumption_resolution,[],[f28612,f10552]) ).
fof(f28614,plain,
( ~ spl63_5
| ~ spl63_426 ),
inference(avatar_contradiction_clause,[],[f28613]) ).
cnf(s1,plain,
( spl63_1
| spl63_2
| spl63_3 ),
inference(sat_conversion,[],[f21312]) ).
cnf(s4,plain,
spl63_5,
inference(sat_conversion,[],[f21324]) ).
cnf(s8,plain,
~ spl63_1,
inference(sat_conversion,[],[f21335]) ).
cnf(s10,plain,
( ~ spl63_3
| ~ spl63_5
| spl63_6 ),
inference(sat_conversion,[],[f21338]) ).
cnf(s11,plain,
~ spl63_6,
inference(sat_conversion,[],[f21340]) ).
cnf(s12,plain,
( ~ spl63_2
| spl63_4
| ~ spl63_5 ),
inference(sat_conversion,[],[f21342]) ).
cnf(s276,plain,
( ~ spl63_4
| ~ spl63_5
| spl63_426 ),
inference(sat_conversion,[],[f28586]) ).
cnf(s277,plain,
( ~ spl63_5
| ~ spl63_426 ),
inference(sat_conversion,[],[f28614]) ).
cnf(s279,plain,
( ~ spl63_3
| ~ spl63_5 ),
inference(rat,[],[s10,s11]) ).
cnf(s282,plain,
~ spl63_426,
inference(rat,[],[s277,s4]) ).
cnf(s283,plain,
~ spl63_4,
inference(rat,[],[s276,s282,s4]) ).
cnf(s285,plain,
~ spl63_3,
inference(rat,[],[s279,s4]) ).
cnf(s286,plain,
~ spl63_2,
inference(rat,[],[s12,s4,s283]) ).
cnf(s287,plain,
$false,
inference(rat,[],[s1,s285,s286,s8]) ).
fof(f28615,plain,
$false,
inference(avatar_sat_refutation,[],[s287]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR115+44 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n018.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 23:19:22 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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
% 3.47/0.92 % (3888362)Will run a generic schedule for satisfiability detection.
% 3.47/0.92 % (3888368)% WARNING: option uhcvi not known.
% 3.47/0.92 % (3888368)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3764876484:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 3.47/0.92 % (3888367)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1820545982_2998 on theBenchmark for (2998ds/0Mi)
% 3.47/0.92 % (3888369)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1634002980:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 3.47/0.92 % (3888370)dis+10_1_sil=32000:sp=arity:random_seed=3214934931:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 3.47/0.92 % (3888372)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3731398411:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 3.47/0.92 % (3888371)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2112989507:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 3.47/0.92 % (3888373)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4291893256:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 3.47/0.92 % (3888370)Instruction limit reached!
% 3.47/0.92 % (3888370)------------------------------
% 3.47/0.92 % (3888370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.92 % (3888370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.92 % (3888370)CaDiCaL version: 2.1.3
% 3.47/0.92 % (3888370)Termination reason: Instruction limit
% 3.47/0.92 % (3888370)Termination phase: Saturation
% 3.47/0.92 % (3888370)Time elapsed: 0.060 s
% 3.47/0.92 % (3888370)Peak memory usage: 26 MB
% 3.47/0.92 % (3888370)Instructions burned: 106 (million)
% 3.47/0.92 % (3888372)Instruction limit reached!
% 3.47/0.92 % (3888372)------------------------------
% 3.47/0.92 % (3888372)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.92 % (3888372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.92 % (3888372)CaDiCaL version: 2.1.3
% 3.47/0.92 % (3888372)Termination reason: Instruction limit
% 3.47/0.92 % (3888372)Termination phase: Saturation
% 3.47/0.92 % (3888372)Time elapsed: 0.071 s
% 3.47/0.92 % (3888372)Peak memory usage: 27 MB
% 3.47/0.92 % (3888372)Instructions burned: 132 (million)
% 3.47/0.92 % (3888371)Instruction limit reached!
% 3.47/0.92 % (3888371)------------------------------
% 3.47/0.92 % (3888371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.92 % (3888371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.92 % (3888371)CaDiCaL version: 2.1.3
% 3.47/0.92 % (3888371)Termination reason: Instruction limit
% 3.47/0.92 % (3888371)Termination phase: Blocked clause elimination
% 3.47/0.92 % (3888371)Time elapsed: 0.073 s
% 3.47/0.92 % (3888371)Peak memory usage: 27 MB
% 3.47/0.92 % (3888371)Instructions burned: 117 (million)
% 3.47/0.92 % (3888381)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4261006182:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 3.47/0.92 % (3888382)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3484721298:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 3.47/0.92 % (3888383)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=361243840:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 3.47/0.92 % (3888373)Instruction limit reached!
% 3.47/0.92 % (3888373)------------------------------
% 3.47/0.92 % (3888373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.92 % (3888373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.92 % (3888373)CaDiCaL version: 2.1.3
% 3.47/0.92 % (3888373)Termination reason: Instruction limit
% 3.47/0.92 % (3888373)Termination phase: Saturation
% 3.47/0.92 % (3888373)Time elapsed: 0.096 s
% 3.47/0.92 % (3888373)Peak memory usage: 30 MB
% 3.47/0.92 % (3888373)Instructions burned: 161 (million)
% 3.47/0.92 % (3888387)ott-21_1_sil=16000:fs=off:random_seed=2742234245:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 3.47/0.92 % (3888382)Instruction limit reached!
% 3.47/0.92 % (3888382)------------------------------
% 3.47/0.92 % (3888382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.92 % (3888382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.92 % (3888382)CaDiCaL version: 2.1.3
% 3.47/0.92 % (3888382)Termination reason: Instruction limit
% 3.47/0.92 % (3888382)Termination phase: Blocked clause elimination
% 3.47/0.92 % (3888382)Time elapsed: 0.077 s
% 3.47/0.92 % (3888382)Peak memory usage: 28 MB
% 3.47/0.92 % (3888382)Instructions burned: 132 (million)
% 3.47/0.92 % (3888389)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2826754179:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 3.47/0.92 % (3888387)Instruction limit reached!
% 3.47/0.92 % (3888387)------------------------------
% 3.47/0.92 % (3888387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.92 % (3888387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.92 % (3888387)CaDiCaL version: 2.1.3
% 3.47/0.92 % (3888387)Termination reason: Instruction limit
% 3.47/0.92 % (3888387)Termination phase: Saturation
% 3.47/0.92 % (3888387)Time elapsed: 0.090 s
% 3.47/0.92 % (3888387)Peak memory usage: 27 MB
% 3.47/0.92 % (3888387)Instructions burned: 181 (million)
% 3.47/0.92 % (3888391)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3773899038:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 3.47/0.92 % TRYING [1]
% 3.47/0.92 % TRYING [1]
% 3.47/0.92 % TRYING [2]
% 3.47/0.92 % TRYING [2]
% 3.47/0.92 % (3888381)Instruction limit reached!
% 3.47/0.92 % (3888381)------------------------------
% 3.47/0.92 % (3888381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.92 % (3888381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.92 % (3888381)CaDiCaL version: 2.1.3
% 3.47/0.92 % (3888381)Termination reason: Instruction limit
% 3.47/0.92 % (3888381)Termination phase: Finite model building constraint generation
% 3.47/0.92 % (3888381)Time elapsed: 0.324 s
% 3.47/0.92 % (3888381)Peak memory usage: 54 MB
% 3.47/0.92 % (3888381)Instructions burned: 715 (million)
% 3.47/0.92 % TRYING [3]
% 3.47/0.92 % (3888393)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=601333576:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 3.47/0.92 % TRYING [1]
% 3.47/0.92 % (3888389)Instruction limit reached!
% 3.47/0.92 % (3888389)------------------------------
% 3.47/0.92 % (3888389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.92 % (3888389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.92 % (3888389)CaDiCaL version: 2.1.3
% 3.47/0.92 % (3888389)Termination reason: Instruction limit
% 3.47/0.92 % (3888389)Termination phase: Saturation
% 3.47/0.92 % (3888389)Time elapsed: 0.246 s
% 3.47/0.92 % (3888389)Peak memory usage: 36 MB
% 3.47/0.92 % (3888389)Instructions burned: 477 (million)
% 3.47/0.92 % (3888383)Instruction limit reached!
% 3.47/0.92 % (3888383)------------------------------
% 3.47/0.92 % (3888383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.92 % (3888383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.92 % (3888383)CaDiCaL version: 2.1.3
% 3.47/0.92 % (3888383)Termination reason: Instruction limit
% 3.47/0.92 % (3888383)Termination phase: Saturation
% 3.47/0.92 % (3888383)Time elapsed: 0.351 s
% 3.47/0.92 % (3888383)Peak memory usage: 33 MB
% 3.47/0.92 % (3888383)Instructions burned: 686 (million)
% 3.47/0.92 % (3888395)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=382468011:i=889:ins=1_2993 on theBenchmark for (2993ds/889Mi)
% 3.47/0.92 % (3888396)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=689469894: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)
% 3.47/0.92 % (3888368) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3888362-3888368"...
% 3.47/0.92 % (3888368)...printing done.
% 3.47/0.92 % (3888368)Refutation found. Thanks to Tanya!
% 3.47/0.92 % SZS status Theorem for theBenchmark
% 3.47/0.92 % SZS output start Proof for theBenchmark
% See solution above
% 3.47/0.93 % (3888368)------------------------------
% 3.47/0.93 % (3888368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.47/0.93 % (3888368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.47/0.93 % (3888368)CaDiCaL version: 2.1.3
% 3.47/0.93 % (3888368)Termination reason: Refutation
% 3.47/0.93 % (3888368)Time elapsed: 0.505 s
% 3.47/0.93 % (3888368)Peak memory usage: 39 MB
% 3.47/0.93 % (3888368)Instructions burned: 1849 (million)
% 3.47/0.93 % (3888362)Success in time 0.7 s
% 3.47/0.93 % Vampire exiting
%------------------------------------------------------------------------------