%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR113+2 : 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 : n015.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 68.53s 15.68s
% Output : CNFRefutation 68.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 4
% Syntax : Number of formulae : 26 ( 9 unt; 0 def)
% Number of atoms : 385 ( 0 equ)
% Maximal formula atoms : 299 ( 14 avg)
% Number of connectives : 410 ( 51 ~; 43 |; 314 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 299 ( 16 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 27 ( 26 usr; 1 prp; 0-3 aty)
% Number of functors : 68 ( 68 usr; 67 con; 0-2 aty)
% Number of variables : 45 ( 0 sgn 4 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_003_insicht_4,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('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)
& sort('vienna$u0',fe)
& varia(c9,'varia$uc')
& refer(c9,indet)
& quant(c9,one)
& gener(c9,sp)
& fact(c9,real)
& etype(c9,int0)
& card(c9,int1)
& sort(c9,na)
& varia(c8,con)
& refer(c8,det)
& quant(c8,one)
& gener(c8,sp)
& fact(c8,real)
& etype(c8,int0)
& card(c8,int1)
& sort(c8,io)
& sort(c8,d)
& gener('rufen$u1$u2',ge)
& fact('rufen$u1$u2',real)
& sort('rufen$u1$u2',da)
& gener(c55,sp)
& fact(c55,real)
& sort(c55,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(c47,con)
& refer(c47,det)
& quant(c47,one)
& gener(c47,sp)
& fact(c47,real)
& etype(c47,int0)
& card(c47,int1)
& sort(c47,ad)
& sort('new$uyork$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('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(c45,'varia$uc')
& refer(c45,indet)
& quant(c45,one)
& gener(c45,sp)
& fact(c45,real)
& etype(c45,int0)
& card(c45,int1)
& sort(c45,na)
& varia(c44,con)
& refer(c44,det)
& quant(c44,one)
& gener(c44,sp)
& fact(c44,real)
& etype(c44,int0)
& card(c44,int1)
& sort(c44,io)
& sort(c44,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(c74,con)
& refer(c74,det)
& quant(c74,one)
& gener(c74,sp)
& fact(c74,real)
& etype(c74,int0)
& card(c74,int1)
& sort(c74,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(c38,con)
& refer(c38,det)
& quant(c38,one)
& gener(c38,sp)
& fact(c38,real)
& etype(c38,int0)
& card(c38,int1)
& sort(c38,d)
& varia(c32,'varia$uc')
& refer(c32,indet)
& quant(c32,one)
& gener(c32,sp)
& fact(c32,real)
& etype(c32,int0)
& card(c32,int1)
& sort(c32,io)
& sort(c32,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(c27,con)
& refer(c27,det)
& quant(c27,one)
& gener(c27,sp)
& fact(c27,real)
& etype(c27,int0)
& card(c27,int1)
& sort(c27,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(c75,con)
& refer(c75,det)
& quant(c75,one)
& gener(c75,sp)
& fact(c75,real)
& etype(c75,int0)
& card(c75,int1)
& sort(c75,l)
& varia(c21,con)
& refer(c21,det)
& quant(c21,one)
& gener(c21,sp)
& fact(c21,hypo)
& etype(c21,int0)
& card(c21,int1)
& sort(c21,ad)
& sort('zilk$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)
& 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(c17,'varia$uc')
& refer(c17,indet)
& quant(c17,one)
& gener(c17,sp)
& fact(c17,real)
& etype(c17,int0)
& card(c17,int1)
& sort(c17,na)
& varia(c16,'varia$uc')
& refer(c16,indet)
& quant(c16,one)
& gener(c16,sp)
& fact(c16,real)
& etype(c16,int0)
& card(c16,int1)
& sort(c16,na)
& varia(c15,'varia$uc')
& refer(c15,det)
& quant(c15,one)
& gener(c15,sp)
& fact(c15,real)
& etype(c15,int0)
& card(c15,int1)
& sort(c15,d)
& 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('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')
& val(c9,'vienna$u0')
& sub(c9,'name$u1$u1')
& sub(c8,'stadt$u$u1$u1')
& attr(c8,c9)
& attch(c8,c15)
& flp(c75,c27)
& in(c74,c44)
& subs(c55,'rufen$u1$u2')
& mcont(c55,c21)
& assoc(c55,c47)
& agt(c55,c15)
& subs(c47,'leben$u1$u1')
& val(c45,'new$uyork$u0')
& sub(c45,'name$u1$u1')
& sub(c44,'stadt$u$u1$u1')
& attr(c44,c45)
& sub(c38,'freiheitsstatue$u1$u1')
& loc(c38,c74)
& sub(c32,'hilfeprojekt$u1$u1')
& propr(c32,'para$u1$u1')
& benf(c32,c38)
& attch(c32,c27)
& sub(c27,'idol$u1$u1')
& subs(c21,'aktion$u1$u1')
& dircl(c21,c75)
& val(c17,'zilk$u0')
& sub(c17,'familiename$u1$u1')
& val(c16,'helmut$u0')
& sub(c16,'eigenname$u1$u1')
& sub(c15,c1)
& attr(c15,c17)
& attr(c15,c16)
& 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_insicht_4,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_insicht_4]) ).
cnf(c15,plain,
loc(c38,c74),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c16,plain,
sub(c38,'freiheitsstatue$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c17,plain,
attr(c44,c45),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c19,plain,
sub(c45,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c20,plain,
val(c45,'new$uyork$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c26,plain,
in(c74,c44),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_4]) ).
cnf(c498,plain,
( flp(X0,X1)
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[local_function___flp]) ).
cnf(c501,plain,
( loc(sK280(X0,X1),X1)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c502,plain,
( scar(sK280(X0,X1),X0)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c503,plain,
( subs(sK280(X0,X1),'stehen$u1$u1')
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c531,plain,
( ~ scar(X1,X0)
| ~ attr(X3,X4)
| ~ loc(X1,X2)
| ~ val(X4,'new$uyork$u0')
| ~ sub(X4,'name$u1$u1')
| ~ flp(X2,X3)
| ~ subs(X1,'stehen$u1$u1')
| ~ sub(X0,'freiheitsstatue$u1$u1') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ flp(X4,X2)
| ~ loc(sK280(X0,X1),X4)
| ~ subs(sK280(X0,X1),'stehen$u1$u1')
| ~ val(X3,'new$uyork$u0')
| ~ sub(X0,'freiheitsstatue$u1$u1')
| ~ sub(X3,'name$u1$u1')
| ~ attr(X2,X3)
| ~ loc(X0,X1) ),
inference(resolution,[status(thm)],[c502,c531]) ).
cnf(d1,plain,
( ~ loc(X2,X3)
| ~ flp(X3,X0)
| ~ loc(X2,X3)
| ~ subs(sK280(X2,X3),'stehen$u1$u1')
| ~ val(X1,'new$uyork$u0')
| ~ sub(X2,'freiheitsstatue$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[d0,c501]) ).
cnf(d2,plain,
( ~ loc(X2,X3)
| ~ flp(X3,X0)
| ~ loc(X2,X3)
| ~ val(X1,'new$uyork$u0')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X2,'freiheitsstatue$u1$u1')
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[d1,c503]) ).
cnf(d3,plain,
flp(c74,c44),
inference(resolution,[status(thm)],[c498,c26]) ).
cnf(d4,plain,
( ~ loc(X1,c74)
| ~ val(X0,'new$uyork$u0')
| ~ sub(X0,'name$u1$u1')
| ~ sub(X1,'freiheitsstatue$u1$u1')
| ~ attr(c44,X0) ),
inference(resolution,[status(thm)],[d3,d2]) ).
cnf(d5,plain,
( ~ val(X0,'new$uyork$u0')
| ~ sub(X0,'name$u1$u1')
| ~ sub(c38,'freiheitsstatue$u1$u1')
| ~ attr(c44,X0) ),
inference(resolution,[status(thm)],[d4,c15]) ).
cnf(d6,plain,
( ~ val(X0,'new$uyork$u0')
| ~ sub(X0,'name$u1$u1')
| ~ attr(c44,X0) ),
inference(resolution,[status(thm)],[c16,d5]) ).
cnf(d7,plain,
( ~ sub(c45,'name$u1$u1')
| ~ attr(c44,c45) ),
inference(resolution,[status(thm)],[d6,c20]) ).
cnf(d8,plain,
~ sub(c45,'name$u1$u1'),
inference(resolution,[status(thm)],[c17,d7]) ).
cnf(d9,plain,
$false,
inference(resolution,[status(thm)],[c19,d8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR113+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n015.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Sun Sep 27 01:07:01 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.45 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 68.53/15.68 % SZS status Theorem for theBenchmark.p
% 68.53/15.68 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------