%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR113+7 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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 : Sun Sep 27 07:04:34 AM UTC 2026
% Result : Theorem 72.97s 16.79s
% Output : CNFRefutation 72.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 4
% Syntax : Number of formulae : 26 ( 9 unt; 0 def)
% Number of atoms : 565 ( 0 equ)
% Maximal formula atoms : 479 ( 21 avg)
% Number of connectives : 590 ( 51 ~; 43 |; 494 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 479 ( 23 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 30 ( 29 usr; 1 prp; 0-7 aty)
% Number of functors : 98 ( 98 usr; 97 con; 0-2 aty)
% Number of variables : 45 ( 0 sgn 4 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_003_mira_news_518_a19713,hypothesis,
( varia('vater$u1$u1','varia$uc')
& refer('vater$u1$u1','refer$uc')
& quant('vater$u1$u1',one)
& gener('vater$u1$u1',ge)
& fact('vater$u1$u1',real)
& etype('vater$u1$u1',int0)
& card('vater$u1$u1',int1)
& sort('vater$u1$u1',d)
& varia('bankkonto$u1$u1','varia$uc')
& refer('bankkonto$u1$u1','refer$uc')
& quant('bankkonto$u1$u1',one)
& gener('bankkonto$u1$u1',ge)
& fact('bankkonto$u1$u1',real)
& etype('bankkonto$u1$u1',int0)
& card('bankkonto$u1$u1',int1)
& sort('bankkonto$u1$u1',io)
& sort('bankkonto$u1$u1',d)
& gener('spenden$u1$u1',ge)
& fact('spenden$u1$u1',real)
& sort('spenden$u1$u1',da)
& varia('ansinnen$u1$u1','varia$uc')
& refer('ansinnen$u1$u1','refer$uc')
& quant('ansinnen$u1$u1',one)
& gener('ansinnen$u1$u1',ge)
& fact('ansinnen$u1$u1',real)
& etype('ansinnen$u1$u1',int0)
& card('ansinnen$u1$u1',int1)
& sort('ansinnen$u1$u1',io)
& sort('ansinnen$u1$u1',ad)
& varia('hilfe$u1$u1','varia$uc')
& refer('hilfe$u1$u1','refer$uc')
& quant('hilfe$u1$u1',one)
& gener('hilfe$u1$u1',ge)
& fact('hilfe$u1$u1',real)
& etype('hilfe$u1$u1',int0)
& card('hilfe$u1$u1',int1)
& sort('hilfe$u1$u1',io)
& sort('hilfe$u1$u1',ad)
& varia('statue$u1$u1','varia$uc')
& refer('statue$u1$u1','refer$uc')
& quant('statue$u1$u1',one)
& gener('statue$u1$u1',ge)
& fact('statue$u1$u1',real)
& etype('statue$u1$u1',int0)
& card('statue$u1$u1',int1)
& sort('statue$u1$u1',d)
& varia('freiheit$u1$u1','varia$uc')
& refer('freiheit$u1$u1','refer$uc')
& quant('freiheit$u1$u1',one)
& gener('freiheit$u1$u1',ge)
& fact('freiheit$u1$u1',real)
& etype('freiheit$u1$u1',int0)
& card('freiheit$u1$u1',int1)
& sort('freiheit$u1$u1',io)
& sort('freiheit$u1$u1',as)
& varia('plan$u1$u1','varia$uc')
& refer('plan$u1$u1','refer$uc')
& quant('plan$u1$u1',one)
& gener('plan$u1$u1',ge)
& fact('plan$u1$u1',real)
& etype('plan$u1$u1',int0)
& card('plan$u1$u1',int1)
& sort('plan$u1$u1',io)
& sort('plan$u1$u1',d)
& sort('plan$u1$u1',ad)
& varia('finanzierung$u1$u1','varia$uc')
& refer('finanzierung$u1$u1','refer$uc')
& quant('finanzierung$u1$u1',one)
& gener('finanzierung$u1$u1',ge)
& fact('finanzierung$u1$u1',real)
& etype('finanzierung$u1$u1',int0)
& card('finanzierung$u1$u1',int1)
& sort('finanzierung$u1$u1',ad)
& gener('rufen$u1$u2',ge)
& fact('rufen$u1$u2',real)
& sort('rufen$u1$u2',da)
& gener(c7183,sp)
& fact(c7183,real)
& sort(c7183,da)
& varia('leben$u1$u1','varia$uc')
& refer('leben$u1$u1','refer$uc')
& quant('leben$u1$u1',one)
& gener('leben$u1$u1',ge)
& fact('leben$u1$u1',real)
& etype('leben$u1$u1',int0)
& card('leben$u1$u1',int1)
& sort('leben$u1$u1',ad)
& varia(c7175,con)
& refer(c7175,det)
& quant(c7175,one)
& gener(c7175,sp)
& fact(c7175,real)
& etype(c7175,int0)
& card(c7175,int1)
& sort(c7175,ad)
& sort('new$uyork$u0',fe)
& varia(c7173,'varia$uc')
& refer(c7173,indet)
& quant(c7173,one)
& gener(c7173,sp)
& fact(c7173,real)
& etype(c7173,int0)
& card(c7173,int1)
& sort(c7173,na)
& varia(c7172,con)
& refer(c7172,det)
& quant(c7172,one)
& gener(c7172,sp)
& fact(c7172,real)
& etype(c7172,int0)
& card(c7172,int1)
& sort(c7172,io)
& sort(c7172,d)
& varia('freiheitsstatue$u1$u1','varia$uc')
& refer('freiheitsstatue$u1$u1','refer$uc')
& quant('freiheitsstatue$u1$u1',one)
& gener('freiheitsstatue$u1$u1',ge)
& fact('freiheitsstatue$u1$u1',real)
& etype('freiheitsstatue$u1$u1',int0)
& card('freiheitsstatue$u1$u1',int1)
& sort('freiheitsstatue$u1$u1',d)
& varia(c7202,con)
& refer(c7202,det)
& quant(c7202,one)
& gener(c7202,sp)
& fact(c7202,real)
& etype(c7202,int0)
& card(c7202,int1)
& sort(c7202,l)
& varia('hilfeprojekt$u1$u1','varia$uc')
& refer('hilfeprojekt$u1$u1','refer$uc')
& quant('hilfeprojekt$u1$u1',one)
& gener('hilfeprojekt$u1$u1',ge)
& fact('hilfeprojekt$u1$u1',real)
& etype('hilfeprojekt$u1$u1',int0)
& card('hilfeprojekt$u1$u1',int1)
& sort('hilfeprojekt$u1$u1',io)
& sort('hilfeprojekt$u1$u1',ad)
& sort('para$u1$u1',rq)
& varia(c7166,con)
& refer(c7166,det)
& quant(c7166,one)
& gener(c7166,sp)
& fact(c7166,real)
& etype(c7166,int0)
& card(c7166,int1)
& sort(c7166,d)
& varia(c7160,'varia$uc')
& refer(c7160,indet)
& quant(c7160,one)
& gener(c7160,sp)
& fact(c7160,real)
& etype(c7160,int0)
& card(c7160,int1)
& sort(c7160,io)
& sort(c7160,ad)
& varia('idol$u1$u1','varia$uc')
& refer('idol$u1$u1','refer$uc')
& quant('idol$u1$u1',one)
& gener('idol$u1$u1',ge)
& fact('idol$u1$u1',real)
& etype('idol$u1$u1',int0)
& card('idol$u1$u1',int1)
& sort('idol$u1$u1',d)
& varia(c7155,con)
& refer(c7155,det)
& quant(c7155,one)
& gener(c7155,sp)
& fact(c7155,real)
& etype(c7155,int0)
& card(c7155,int1)
& sort(c7155,d)
& varia('aktion$u1$u1','varia$uc')
& refer('aktion$u1$u1','refer$uc')
& quant('aktion$u1$u1',one)
& gener('aktion$u1$u1',ge)
& fact('aktion$u1$u1',real)
& etype('aktion$u1$u1',int0)
& card('aktion$u1$u1',int1)
& sort('aktion$u1$u1',ad)
& varia(c7203,con)
& refer(c7203,det)
& quant(c7203,one)
& gener(c7203,sp)
& fact(c7203,real)
& etype(c7203,int0)
& card(c7203,int1)
& sort(c7203,l)
& varia(c7149,con)
& refer(c7149,det)
& quant(c7149,one)
& gener(c7149,sp)
& fact(c7149,hypo)
& etype(c7149,int0)
& card(c7149,int1)
& sort(c7149,ad)
& sort('zilk$u0',fe)
& sort('helmut$u0',fe)
& varia('eigenname$u1$u1','varia$uc')
& refer('eigenname$u1$u1','refer$uc')
& quant('eigenname$u1$u1',one)
& gener('eigenname$u1$u1',ge)
& fact('eigenname$u1$u1',real)
& etype('eigenname$u1$u1',int0)
& card('eigenname$u1$u1',int1)
& sort('eigenname$u1$u1',na)
& varia(c7145,'varia$uc')
& refer(c7145,indet)
& quant(c7145,one)
& gener(c7145,sp)
& fact(c7145,real)
& etype(c7145,int0)
& card(c7145,int1)
& sort(c7145,na)
& varia(c7144,'varia$uc')
& refer(c7144,indet)
& quant(c7144,one)
& gener(c7144,sp)
& fact(c7144,real)
& etype(c7144,int0)
& card(c7144,int1)
& sort(c7144,na)
& sort('vienna$u0',fe)
& varia('stadt$u$u1$u1','varia$uc')
& refer('stadt$u$u1$u1','refer$uc')
& quant('stadt$u$u1$u1',one)
& gener('stadt$u$u1$u1',ge)
& fact('stadt$u$u1$u1',real)
& etype('stadt$u$u1$u1',int0)
& card('stadt$u$u1$u1',int1)
& sort('stadt$u$u1$u1',io)
& sort('stadt$u$u1$u1',d)
& varia(c7137,'varia$uc')
& refer(c7137,indet)
& quant(c7137,one)
& gener(c7137,sp)
& fact(c7137,real)
& etype(c7137,int0)
& card(c7137,int1)
& sort(c7137,na)
& varia(c7143,'varia$uc')
& refer(c7143,det)
& quant(c7143,one)
& gener(c7143,sp)
& fact(c7143,real)
& etype(c7143,int0)
& card(c7143,int1)
& sort(c7143,d)
& varia(c7136,con)
& refer(c7136,det)
& quant(c7136,one)
& gener(c7136,sp)
& fact(c7136,real)
& etype(c7136,int0)
& card(c7136,int1)
& sort(c7136,io)
& sort(c7136,d)
& varia(c7127,'varia$uc')
& refer(c7127,'refer$uc')
& quant(c7127,'quant$uc')
& gener(c7127,'gener$uc')
& fact(c7127,real)
& etype(c7127,'etype$uc')
& card(c7127,'card$uc')
& sort(c7127,ent)
& sort('rettet$uden$ustephansdom$u0',fe)
& varia('name$u1$u1','varia$uc')
& refer('name$u1$u1','refer$uc')
& quant('name$u1$u1',one)
& gener('name$u1$u1',ge)
& fact('name$u1$u1',real)
& etype('name$u1$u1',int0)
& card('name$u1$u1',int1)
& sort('name$u1$u1',na)
& varia('spendenkonto$u1$u1','varia$uc')
& refer('spendenkonto$u1$u1','refer$uc')
& quant('spendenkonto$u1$u1',one)
& gener('spendenkonto$u1$u1',ge)
& fact('spendenkonto$u1$u1',real)
& etype('spendenkonto$u1$u1',int0)
& card('spendenkonto$u1$u1',int1)
& sort('spendenkonto$u1$u1',io)
& sort('spendenkonto$u1$u1',d)
& varia(c7075,'varia$uc')
& refer(c7075,indet)
& quant(c7075,one)
& gener(c7075,sp)
& fact(c7075,real)
& etype(c7075,int0)
& card(c7075,int1)
& sort(c7075,na)
& varia(c7066,con)
& refer(c7066,det)
& quant(c7066,one)
& gener(c7066,sp)
& fact(c7066,real)
& etype(c7066,int0)
& card(c7066,int1)
& sort(c7066,io)
& sort(c7066,d)
& varia('jahr$u$u1$u1','varia$uc')
& refer('jahr$u$u1$u1','refer$uc')
& quant('jahr$u$u1$u1','quant$uc')
& gener('jahr$u$u1$u1',ge)
& fact('jahr$u$u1$u1',real)
& etype('jahr$u$u1$u1','etype$uc')
& card('jahr$u$u1$u1','card$uc')
& sort('jahr$u$u1$u1',ta)
& sort('jahr$u$u1$u1',oa)
& sort('jahr$u$u1$u1',me)
& card(c7057,int8)
& sort(c7057,nu)
& varia(c7062,'varia$uc')
& refer(c7062,'refer$uc')
& quant(c7062,'quant$uc')
& gener(c7062,'gener$uc')
& fact(c7062,real)
& etype(c7062,'etype$uc')
& card(c7062,'card$uc')
& sort(c7062,ta)
& sort(c7062,m)
& varia('gruendung$u1$u1','varia$uc')
& refer('gruendung$u1$u1','refer$uc')
& quant('gruendung$u1$u1',one)
& gener('gruendung$u1$u1',ge)
& fact('gruendung$u1$u1',real)
& etype('gruendung$u1$u1',int0)
& card('gruendung$u1$u1',int1)
& sort('gruendung$u1$u1',ad)
& varia(c7053,con)
& refer(c7053,det)
& quant(c7053,one)
& gener(c7053,sp)
& fact(c7053,real)
& etype(c7053,int0)
& card(c7053,int1)
& sort(c7053,ad)
& varia('franke$u1$u1','varia$uc')
& refer('franke$u1$u1','refer$uc')
& quant('franke$u1$u1',one)
& gener('franke$u1$u1',ge)
& fact('franke$u1$u1',real)
& etype('franke$u1$u1',int0)
& card('franke$u1$u1',int1)
& sort('franke$u1$u1',d)
& varia(c7043,'varia$uc')
& refer(c7043,'refer$uc')
& quant(c7043,nfquant)
& gener(c7043,'gener$uc')
& fact(c7043,real)
& etype(c7043,int1)
& card(c7043,float8400000)
& sort(c7043,d)
& sort('rund$u0',fe)
& varia('familiename$u1$u1','varia$uc')
& refer('familiename$u1$u1','refer$uc')
& quant('familiename$u1$u1',one)
& gener('familiename$u1$u1',ge)
& fact('familiename$u1$u1',real)
& etype('familiename$u1$u1',int0)
& card('familiename$u1$u1',int1)
& sort('familiename$u1$u1',na)
& varia('mensch$u1$u1','varia$uc')
& refer('mensch$u1$u1','refer$uc')
& quant('mensch$u1$u1',one)
& gener('mensch$u1$u1',ge)
& fact('mensch$u1$u1',real)
& etype('mensch$u1$u1',int0)
& card('mensch$u1$u1',int1)
& sort('mensch$u1$u1',d)
& varia(c7038,'varia$uc')
& refer(c7038,indet)
& quant(c7038,one)
& gener(c7038,sp)
& fact(c7038,real)
& etype(c7038,int0)
& card(c7038,int1)
& sort(c7038,na)
& varia(c7037,con)
& refer(c7037,det)
& quant(c7037,one)
& gener(c7037,sp)
& fact(c7037,real)
& etype(c7037,int0)
& card(c7037,int1)
& sort(c7037,d)
& varia('finanzierungsmodell$u1$u3','varia$uc')
& refer('finanzierungsmodell$u1$u3','refer$uc')
& quant('finanzierungsmodell$u1$u3',one)
& gener('finanzierungsmodell$u1$u3',ge)
& fact('finanzierungsmodell$u1$u3',real)
& etype('finanzierungsmodell$u1$u3',int0)
& card('finanzierungsmodell$u1$u3',int1)
& sort('finanzierungsmodell$u1$u3',io)
& sort('finanzierungsmodell$u1$u3',d)
& sort('finanzierungsmodell$u1$u3',ad)
& varia(c7029,'varia$uc')
& refer(c7029,'refer$uc')
& quant(c7029,one)
& gener(c7029,'gener$uc')
& fact(c7029,real)
& etype(c7029,int0)
& card(c7029,int1)
& sort(c7029,io)
& sort(c7029,d)
& sort(c7029,ad)
& varia('stadtvater$u1$u1','varia$uc')
& refer('stadtvater$u1$u1','refer$uc')
& quant('stadtvater$u1$u1',one)
& gener('stadtvater$u1$u1',ge)
& fact('stadtvater$u1$u1',real)
& etype('stadtvater$u1$u1',int0)
& card('stadtvater$u1$u1',int1)
& sort('stadtvater$u1$u1',d)
& sort('ehemalig$u1$u1',tq)
& varia(c1,'varia$uc')
& refer(c1,'refer$uc')
& quant(c1,'quant$uc')
& gener(c1,'gener$uc')
& fact(c1,'fact$uc')
& etype(c1,'etype$uc')
& card(c1,'card$uc')
& sort(c1,ent)
& sub('stadtvater$u1$u1','vater$u1$u1')
& assoc('stadtvater$u1$u1','stadt$u$u1$u1')
& sub('spendenkonto$u1$u1','bankkonto$u1$u1')
& assoc('spendenkonto$u1$u1','spenden$u1$u1')
& sub('hilfeprojekt$u1$u1','ansinnen$u1$u1')
& assoc('hilfeprojekt$u1$u1','hilfe$u1$u1')
& sub('freiheitsstatue$u1$u1','statue$u1$u1')
& assoc('freiheitsstatue$u1$u1','freiheit$u1$u1')
& sub('finanzierungsmodell$u1$u3','plan$u1$u1')
& assoc('finanzierungsmodell$u1$u3','finanzierung$u1$u1')
& flp(c7203,c7155)
& in(c7202,c7172)
& subs(c7183,'rufen$u1$u2')
& mcont(c7183,c7149)
& assoc(c7183,c7175)
& agt(c7183,c7143)
& subs(c7175,'leben$u1$u1')
& val(c7173,'new$uyork$u0')
& sub(c7173,'name$u1$u1')
& sub(c7172,'stadt$u$u1$u1')
& attr(c7172,c7173)
& sub(c7166,'freiheitsstatue$u1$u1')
& loc(c7166,c7202)
& sub(c7160,'hilfeprojekt$u1$u1')
& propr(c7160,'para$u1$u1')
& benf(c7160,c7166)
& attch(c7160,c7155)
& sub(c7155,'idol$u1$u1')
& subs(c7149,'aktion$u1$u1')
& dircl(c7149,c7203)
& val(c7145,'zilk$u0')
& sub(c7145,'familiename$u1$u1')
& val(c7144,'helmut$u0')
& sub(c7144,'eigenname$u1$u1')
& sub(c7143,c1)
& attr(c7143,c7145)
& attr(c7143,c7144)
& val(c7137,'vienna$u0')
& sub(c7137,'name$u1$u1')
& sub(c7136,'stadt$u$u1$u1')
& attr(c7136,c7137)
& attch(c7136,c7143)
& 'tupl$up7'(c7127,c7029,c7037,c7043,c7053,c7062,c7066)
& val(c7075,'rettet$uden$ustephansdom$u0')
& sub(c7075,'name$u1$u1')
& sub(c7066,'spendenkonto$u1$u1')
& attr(c7066,c7075)
& 'quant$up3'(c7062,c7057,'jahr$u$u1$u1')
& subs(c7053,'gruendung$u1$u1')
& pred(c7043,'franke$u1$u1')
& val(c7038,'rund$u0')
& sub(c7038,'familiename$u1$u1')
& sub(c7037,'mensch$u1$u1')
& attr(c7037,c7038)
& sub(c7029,'finanzierungsmodell$u1$u3')
& pmod(c1,'ehemalig$u1$u1','stadtvater$u1$u1') ) ).
fof(local_function___flp,axiom,
! [X0,X1] :
( ( bei(X0,X1)
| an(X0,X1)
| in(X0,X1) )
=> flp(X0,X1) ) ).
fof(loc__stehen_1_1_loc,axiom,
! [X0,X1] :
( loc(X0,X1)
=> ? [X2] :
( subs(X2,'stehen$u1$u1')
& scar(X2,X0)
& loc(X2,X1) ) ) ).
fof(synth_qa07_003_mira_news_518_a19713,conjecture,
? [X0,X1,X2,X3,X4] :
( val(X1,'new$uyork$u0')
& subs(X3,'stehen$u1$u1')
& sub(X4,'freiheitsstatue$u1$u1')
& sub(X1,'name$u1$u1')
& scar(X3,X4)
& loc(X3,X0)
& attr(X2,X1)
& flp(X0,X2) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4] :
( val(X1,'new$uyork$u0')
& subs(X3,'stehen$u1$u1')
& sub(X4,'freiheitsstatue$u1$u1')
& sub(X1,'name$u1$u1')
& scar(X3,X4)
& loc(X3,X0)
& attr(X2,X1)
& flp(X0,X2) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_003_mira_news_518_a19713]) ).
cnf(c33,plain,
loc(c7166,c7202),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_mira_news_518_a19713]) ).
cnf(c34,plain,
sub(c7166,'freiheitsstatue$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_mira_news_518_a19713]) ).
cnf(c35,plain,
attr(c7172,c7173),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_mira_news_518_a19713]) ).
cnf(c37,plain,
sub(c7173,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_mira_news_518_a19713]) ).
cnf(c38,plain,
val(c7173,'new$uyork$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_mira_news_518_a19713]) ).
cnf(c44,plain,
in(c7202,c7172),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_mira_news_518_a19713]) ).
cnf(c688,plain,
( flp(X0,X1)
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[local_function___flp]) ).
cnf(c691,plain,
( loc(sK291(X0,X1),X1)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c692,plain,
( scar(sK291(X0,X1),X0)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c693,plain,
( subs(sK291(X0,X1),'stehen$u1$u1')
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c728,plain,
( ~ scar(X4,X2)
| ~ loc(X4,X0)
| ~ subs(X4,'stehen$u1$u1')
| ~ val(X3,'new$uyork$u0')
| ~ attr(X1,X3)
| ~ sub(X3,'name$u1$u1')
| ~ sub(X2,'freiheitsstatue$u1$u1')
| ~ flp(X0,X1) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ flp(X4,X3)
| ~ loc(sK291(X0,X1),X4)
| ~ subs(sK291(X0,X1),'stehen$u1$u1')
| ~ val(X2,'new$uyork$u0')
| ~ attr(X3,X2)
| ~ sub(X0,'freiheitsstatue$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ loc(X0,X1) ),
inference(resolution,[status(thm)],[c692,c728]) ).
cnf(d1,plain,
( ~ loc(X1,X3)
| ~ flp(X3,X2)
| ~ loc(X1,X3)
| ~ subs(sK291(X1,X3),'stehen$u1$u1')
| ~ val(X0,'new$uyork$u0')
| ~ attr(X2,X0)
| ~ sub(X1,'freiheitsstatue$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d0,c691]) ).
cnf(d2,plain,
( ~ loc(X0,X3)
| ~ flp(X3,X2)
| ~ loc(X0,X3)
| ~ val(X1,'new$uyork$u0')
| ~ attr(X2,X1)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'freiheitsstatue$u1$u1') ),
inference(resolution,[status(thm)],[d1,c693]) ).
cnf(d3,plain,
flp(c7202,c7172),
inference(resolution,[status(thm)],[c688,c44]) ).
cnf(d4,plain,
( ~ loc(X1,c7202)
| ~ val(X0,'new$uyork$u0')
| ~ attr(c7172,X0)
| ~ sub(X1,'freiheitsstatue$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d3,d2]) ).
cnf(d5,plain,
( ~ val(X0,'new$uyork$u0')
| ~ attr(c7172,X0)
| ~ sub(X0,'name$u1$u1')
| ~ sub(c7166,'freiheitsstatue$u1$u1') ),
inference(resolution,[status(thm)],[d4,c33]) ).
cnf(d6,plain,
( ~ val(X0,'new$uyork$u0')
| ~ attr(c7172,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[c34,d5]) ).
cnf(d7,plain,
( ~ attr(c7172,c7173)
| ~ sub(c7173,'name$u1$u1') ),
inference(resolution,[status(thm)],[d6,c38]) ).
cnf(d8,plain,
~ sub(c7173,'name$u1$u1'),
inference(resolution,[status(thm)],[c35,d7]) ).
cnf(d9,plain,
$false,
inference(resolution,[status(thm)],[c37,d8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR113+7 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n017.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sun Sep 27 01:00:04 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 72.97/16.79 % SZS status Theorem for theBenchmark.p
% 72.97/16.79 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------