%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR113+1 : 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 : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:04:32 AM UTC 2026
% Result : Theorem 61.09s 13.28s
% Output : CNFRefutation 61.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 4
% Syntax : Number of formulae : 26 ( 8 unt; 0 def)
% Number of atoms : 245 ( 0 equ)
% Maximal formula atoms : 164 ( 9 avg)
% Number of connectives : 265 ( 46 ~; 38 |; 179 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 164 ( 11 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 26 ( 25 usr; 1 prp; 0-2 aty)
% Number of functors : 51 ( 51 usr; 49 con; 0-2 aty)
% Number of variables : 41 ( 0 sgn 4 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_003_insicht_3,hypothesis,
( 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)
& gener('propr$u0','gener$uc')
& fact('propr$u0',real)
& sort('propr$u0',st)
& gener(c54,sp)
& fact(c54,real)
& sort(c54,st)
& sort('new$uyork$u0',fe)
& varia(c49,'varia$uc')
& refer(c49,indet)
& quant(c49,one)
& gener(c49,sp)
& fact(c49,real)
& etype(c49,int0)
& card(c49,int1)
& sort(c49,na)
& varia(c48,con)
& refer(c48,det)
& quant(c48,one)
& gener(c48,sp)
& fact(c48,real)
& etype(c48,int0)
& card(c48,int1)
& sort(c48,io)
& sort(c48,d)
& varia(c57,con)
& refer(c57,det)
& quant(c57,one)
& gener(c57,sp)
& fact(c57,real)
& etype(c57,int0)
& card(c57,int1)
& sort(c57,l)
& varia(c41,con)
& refer(c41,det)
& quant(c41,one)
& gener(c41,sp)
& fact(c41,real)
& etype(c41,int0)
& card(c41,int1)
& sort(c41,d)
& varia('gr$u$u366$u$u337e$u1$u1','varia$uc')
& refer('gr$u$u366$u$u337e$u1$u1','refer$uc')
& quant('gr$u$u366$u$u337e$u1$u1',one)
& gener('gr$u$u366$u$u337e$u1$u1',ge)
& fact('gr$u$u366$u$u337e$u1$u1',real)
& etype('gr$u$u366$u$u337e$u1$u1',int0)
& card('gr$u$u366$u$u337e$u1$u1',int1)
& sort('gr$u$u366$u$u337e$u1$u1',oa)
& varia(c36,con)
& refer(c36,det)
& quant(c36,mult)
& gener(c36,sp)
& fact(c36,real)
& etype(c36,int1)
& card(c36,cons('x$uconstant',cons(int1,nil)))
& sort(c36,oa)
& sort('gleich$u1$u1',rq)
& 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)
& sort('paris$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(c14,'varia$uc')
& refer(c14,indet)
& quant(c14,one)
& gener(c14,sp)
& fact(c14,real)
& etype(c14,int0)
& card(c14,int1)
& sort(c14,na)
& varia(c13,con)
& refer(c13,det)
& quant(c13,one)
& gener(c13,sp)
& fact(c13,real)
& etype(c13,int0)
& card(c13,int1)
& sort(c13,io)
& sort(c13,d)
& gener('befinden$u1$u2',ge)
& fact('befinden$u1$u2',real)
& sort('befinden$u1$u2',st)
& varia(c18,'varia$uc')
& refer(c18,indet)
& quant(c18,nfquant)
& gener(c18,sp)
& fact(c18,real)
& etype(c18,int1)
& card(c18,int4)
& sort(c18,d)
& varia(c59,con)
& refer(c59,det)
& quant(c59,one)
& gener(c59,sp)
& fact(c59,real)
& etype(c59,int0)
& card(c59,int1)
& sort(c59,l)
& gener(c11,sp)
& fact(c11,real)
& sort(c11,st)
& sub('freiheitsstatue$u1$u1','statue$u1$u1')
& assoc('freiheitsstatue$u1$u1','freiheit$u1$u1')
& in(c59,c13)
& in(c57,c48)
& subr(c54,'propr$u0')
& instr(c54,c41)
& assoc(c54,c36)
& arg2(c54,'gleich$u1$u1')
& arg1(c54,c18)
& val(c49,'new$uyork$u0')
& sub(c49,'name$u1$u1')
& sub(c48,'stadt$u$u1$u1')
& attr(c48,c49)
& sub(c41,'freiheitsstatue$u1$u1')
& loc(c41,c57)
& pred(c36,'gr$u$u366$u$u337e$u1$u1')
& propr(c18,'gleich$u1$u1')
& pred(c18,'freiheitsstatue$u1$u1')
& val(c14,'paris$u0')
& sub(c14,'name$u1$u1')
& sub(c13,'stadt$u$u1$u1')
& attr(c13,c14)
& subs(c11,'befinden$u1$u2')
& scar(c11,c18)
& loc(c11,c59) ) ).
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_3,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_3]) ).
cnf(c10,plain,
loc(c41,c57),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_3]) ).
cnf(c11,plain,
sub(c41,'freiheitsstatue$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_3]) ).
cnf(c12,plain,
attr(c48,c49),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_3]) ).
cnf(c14,plain,
sub(c49,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_3]) ).
cnf(c15,plain,
val(c49,'new$uyork$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_3]) ).
cnf(c21,plain,
in(c57,c48),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_insicht_3]) ).
cnf(c331,plain,
( flp(X0,X1)
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[local_function___flp]) ).
cnf(c334,plain,
( loc(sK252(X0,X1),X1)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c335,plain,
( scar(sK252(X0,X1),X0)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c336,plain,
( subs(sK252(X0,X1),'stehen$u1$u1')
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c356,plain,
( ~ flp(X2,X4)
| ~ attr(X4,X3)
| ~ sub(X1,'freiheitsstatue$u1$u1')
| ~ sub(X3,'name$u1$u1')
| ~ val(X3,'new$uyork$u0')
| ~ loc(X0,X2)
| ~ scar(X0,X1)
| ~ subs(X0,'stehen$u1$u1') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
flp(c57,c48),
inference(resolution,[status(thm)],[c331,c21]) ).
cnf(d1,plain,
( ~ val(X2,'new$uyork$u0')
| ~ sub(X1,'freiheitsstatue$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ attr(c48,X2)
| ~ subs(X0,'stehen$u1$u1')
| ~ scar(X0,X1)
| ~ loc(X0,c57) ),
inference(resolution,[status(thm)],[d0,c356]) ).
cnf(d2,plain,
( ~ sub(X1,'freiheitsstatue$u1$u1')
| ~ sub(c49,'name$u1$u1')
| ~ attr(c48,c49)
| ~ subs(X0,'stehen$u1$u1')
| ~ scar(X0,X1)
| ~ loc(X0,c57) ),
inference(resolution,[status(thm)],[d1,c15]) ).
cnf(d3,plain,
( ~ sub(c49,'name$u1$u1')
| ~ sub(X1,'freiheitsstatue$u1$u1')
| ~ subs(X0,'stehen$u1$u1')
| ~ scar(X0,X1)
| ~ loc(X0,c57) ),
inference(resolution,[status(thm)],[c12,d2]) ).
cnf(d4,plain,
( ~ sub(X1,'freiheitsstatue$u1$u1')
| ~ subs(X0,'stehen$u1$u1')
| ~ scar(X0,X1)
| ~ loc(X0,c57) ),
inference(resolution,[status(thm)],[c14,d3]) ).
cnf(d5,plain,
( ~ subs(X0,'stehen$u1$u1')
| ~ scar(X0,c41)
| ~ loc(X0,c57) ),
inference(resolution,[status(thm)],[d4,c11]) ).
cnf(d6,plain,
( ~ loc(X0,X1)
| ~ scar(sK252(X0,X1),c41)
| ~ loc(sK252(X0,X1),c57) ),
inference(resolution,[status(thm)],[d5,c336]) ).
cnf(d7,plain,
( ~ loc(c41,X0)
| ~ loc(sK252(c41,X0),c57)
| ~ loc(c41,X0) ),
inference(resolution,[status(thm)],[d6,c335]) ).
cnf(d8,plain,
( ~ loc(c41,c57)
| ~ loc(c41,c57) ),
inference(resolution,[status(thm)],[d7,c334]) ).
cnf(d9,plain,
$false,
inference(resolution,[status(thm)],[c10,d8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR113+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.37 % Computer : n008.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Sun Sep 27 01:03:17 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 61.09/13.28 % SZS status Theorem for theBenchmark.p
% 61.09/13.28 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------