%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR113+13 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:31 AM UTC 2026
% Result : Theorem 127.89s 17.61s
% Output : CNFRefutation 127.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 6
% Syntax : Number of formulae : 27 ( 10 unt; 0 def)
% Number of atoms : 289 ( 0 equ)
% Maximal formula atoms : 221 ( 10 avg)
% Number of connectives : 292 ( 30 ~; 26 |; 233 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 221 ( 12 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 29 ( 28 usr; 1 prp; 0-3 aty)
% Number of functors : 65 ( 65 usr; 63 con; 0-2 aty)
% Number of variables : 48 ( 6 sgn 10 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_003_mira_wp_196_a19713,hypothesis,
( varia('parade$u$u1$u1','varia$uc')
& refer('parade$u$u1$u1','refer$uc')
& quant('parade$u$u1$u1',one)
& gener('parade$u$u1$u1',ge)
& fact('parade$u$u1$u1',real)
& etype('parade$u$u1$u1',int0)
& card('parade$u$u1$u1',int1)
& sort('parade$u$u1$u1',ad)
& varia('konfetti$u1$u1','varia$uc')
& refer('konfetti$u1$u1','refer$uc')
& quant('konfetti$u1$u1',one)
& gener('konfetti$u1$u1',ge)
& fact('konfetti$u1$u1',real)
& etype('konfetti$u1$u1',int0)
& card('konfetti$u1$u1',int1)
& sort('konfetti$u1$u1',o)
& 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)
& card(c65,int1894)
& sort(c65,nu)
& 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)
& 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(c70,'varia$uc')
& refer(c70,'refer$uc')
& quant(c70,'quant$uc')
& gener(c70,sp)
& fact(c70,real)
& etype(c70,'etype$uc')
& card(c70,'card$uc')
& sort(c70,ta)
& sort(c70,oa)
& sort(c70,me)
& varia('konfettiparade$u1$u1','varia$uc')
& refer('konfettiparade$u1$u1','refer$uc')
& quant('konfettiparade$u1$u1',one)
& gener('konfettiparade$u1$u1',ge)
& fact('konfettiparade$u1$u1',real)
& etype('konfettiparade$u1$u1',int0)
& card('konfettiparade$u1$u1',int1)
& sort('konfettiparade$u1$u1',ad)
& card('erst$u1$u1',int1)
& sort('erst$u1$u1',oq)
& varia(c69,con)
& refer(c69,det)
& quant(c69,one)
& gener(c69,sp)
& fact(c69,real)
& etype(c69,int0)
& card(c69,int1)
& sort(c69,t)
& varia(c66,'varia$uc')
& refer(c66,'refer$uc')
& quant(c66,one)
& gener(c66,ge)
& fact(c66,real)
& etype(c66,int0)
& card(c66,int1)
& sort(c66,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(c59,'varia$uc')
& refer(c59,indet)
& quant(c59,one)
& gener(c59,sp)
& fact(c59,real)
& etype(c59,int0)
& card(c59,int1)
& sort(c59,na)
& varia(c58,con)
& refer(c58,det)
& quant(c58,one)
& gener(c58,sp)
& fact(c58,real)
& etype(c58,int0)
& card(c58,int1)
& sort(c58,io)
& sort(c58,d)
& varia('einweihung$u1$u1','varia$uc')
& refer('einweihung$u1$u1','refer$uc')
& quant('einweihung$u1$u1',one)
& gener('einweihung$u1$u1',ge)
& fact('einweihung$u1$u1',real)
& etype('einweihung$u1$u1',int0)
& card('einweihung$u1$u1',int1)
& sort('einweihung$u1$u1',ad)
& varia(c7,con)
& refer(c7,det)
& quant(c7,one)
& gener(c7,sp)
& fact(c7,real)
& etype(c7,int0)
& card(c7,int1)
& sort(c7,d)
& varia(c3,'varia$uc')
& refer(c3,det)
& quant(c3,one)
& gener(c3,sp)
& fact(c3,real)
& etype(c3,int0)
& card(c3,int1)
& sort(c3,ad)
& gener('kommen$u1$u1',ge)
& fact('kommen$u1$u1',real)
& sort('kommen$u1$u1',da)
& varia(c63,con)
& refer(c63,det)
& quant(c63,one)
& gener(c63,sp)
& fact(c63,real)
& etype(c63,int0)
& card(c63,int1)
& sort(c63,ad)
& sort('spontan$u1$u1',nq)
& varia(c72,con)
& refer(c72,det)
& quant(c72,one)
& gener(c72,sp)
& fact(c72,real)
& etype(c72,int0)
& card(c72,int1)
& sort(c72,l)
& varia(c33,'varia$uc')
& refer(c33,det)
& quant(c33,one)
& gener(c33,sp)
& fact(c33,real)
& etype(c33,int0)
& card(c33,int1)
& sort(c33,o)
& gener(c16,sp)
& fact(c16,real)
& sort(c16,da)
& varia('vortag$u1$u1','varia$uc')
& refer('vortag$u1$u1','refer$uc')
& quant('vortag$u1$u1',one)
& gener('vortag$u1$u1',ge)
& fact('vortag$u1$u1',real)
& etype('vortag$u1$u1',int0)
& card('vortag$u1$u1',int1)
& sort('vortag$u1$u1',ta)
& varia(c11,con)
& refer(c11,det)
& quant(c11,one)
& gener(c11,sp)
& fact(c11,real)
& etype(c11,int0)
& card(c11,int1)
& sort(c11,ta)
& subs('konfettiparade$u1$u1','parade$u$u1$u1')
& assoc('konfettiparade$u1$u1','konfetti$u1$u1')
& sub('freiheitsstatue$u1$u1','statue$u1$u1')
& assoc('freiheitsstatue$u1$u1','freiheit$u1$u1')
& in(c72,c58)
& val(c70,c65)
& sub(c70,'jahr$u$u1$u1')
& sub(c7,'freiheitsstatue$u1$u1')
& attr(c69,c70)
& pmod(c66,'erst$u1$u1','konfettiparade$u1$u1')
& temp(c63,c69)
& subs(c63,c66)
& val(c59,'new$uyork$u0')
& sub(c59,'name$u1$u1')
& sub(c58,'stadt$u$u1$u1')
& attr(c58,c59)
& temp(c3,c11)
& subs(c3,'einweihung$u1$u1')
& obj(c3,c7)
& ante(c3,c16)
& subs(c16,'kommen$u1$u1')
& purp(c16,c63)
& mannr(c16,'spontan$u1$u1')
& dircl(c16,c72)
& agt(c16,c33)
& sub(c11,'vortag$u1$u1') ) ).
fof(member_first,axiom,
! [X0,X1] : member(X0,cons(X0,X1)) ).
fof(member_second,axiom,
! [X0,X1,X2] :
( member(X0,X2)
=> member(X0,cons(X1,X2)) ) ).
fof(attr_name__abk__374rzung_stehen_1_b_f__374r,axiom,
! [X0,X1,X2] :
( ( sub(X0,X1)
& member(X1,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil))))
& attr(X2,X0) )
=> ? [X3] :
( subs(X3,'stehen$u1$ub')
& scar(X3,X2)
& obj(X3,X2)
& mcont(X3,X2) ) ) ).
fof(local_function___flp,axiom,
! [X0,X1] :
( ( bei(X0,X1)
| an(X0,X1)
| in(X0,X1) )
=> flp(X0,X1) ) ).
fof(synth_qa07_003_mira_wp_196_a19713,conjecture,
? [X0,X1,X2,X3,X4] :
( val(X1,'new$uyork$u0')
& sub(X1,'name$u1$u1')
& scar(X3,X4)
& attr(X2,X1)
& flp(X0,X2) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4] :
( val(X1,'new$uyork$u0')
& sub(X1,'name$u1$u1')
& scar(X3,X4)
& attr(X2,X1)
& flp(X0,X2) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_003_mira_wp_196_a19713]) ).
cnf(c5,plain,
attr(c58,c59),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_mira_wp_196_a19713]) ).
cnf(c6,plain,
sub(c59,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_mira_wp_196_a19713]) ).
cnf(c210,plain,
in(c72,c58),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_mira_wp_196_a19713]) ).
cnf(c214,plain,
val(c59,'new$uyork$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_003_mira_wp_196_a19713]) ).
cnf(c221,plain,
member(X0,cons(X0,X1)),
inference(clausification,[status(esa)],[member_first]) ).
cnf(c222,plain,
( member(X0,cons(X2,X1))
| ~ member(X0,X1) ),
inference(clausification,[status(esa)],[member_second]) ).
cnf(c434,plain,
( scar(sK275(X2),X2)
| ~ attr(X2,X1)
| ~ sub(X1,X0)
| ~ member(X0,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) ),
inference(clausification,[status(esa)],[attr_name__abk__374rzung_stehen_1_b_f__374r]) ).
cnf(c485,plain,
( flp(X0,X1)
| ~ in(X0,X1) ),
inference(clausification,[status(esa)],[local_function___flp]) ).
cnf(c534,plain,
( ~ val(X4,'new$uyork$u0')
| ~ attr(X1,X4)
| ~ sub(X4,'name$u1$u1')
| ~ scar(X2,X3)
| ~ flp(X0,X1) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
flp(c72,c58),
inference(resolution,[status(thm)],[c485,c210]) ).
cnf(d1,plain,
( ~ member(X1,cons('familiename$u1$u1',cons('name$u1$u1',nil)))
| scar(sK275(X2),X2)
| ~ attr(X2,X0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[c434,c222]) ).
cnf(d2,plain,
( ~ member(X1,cons('name$u1$u1',nil))
| scar(sK275(X2),X2)
| ~ attr(X2,X0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[d1,c222]) ).
cnf(d3,plain,
( scar(sK275(X1),X1)
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d2,c221]) ).
cnf(d4,plain,
( scar(sK275(c58),c58)
| ~ sub(c59,'name$u1$u1') ),
inference(resolution,[status(thm)],[d3,c5]) ).
cnf(d5,plain,
scar(sK275(c58),c58),
inference(resolution,[status(thm)],[c6,d4]) ).
cnf(d6,plain,
( ~ flp(X2,X1)
| ~ val(X0,'new$uyork$u0')
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d5,c534]) ).
cnf(d7,plain,
( ~ val(X0,'new$uyork$u0')
| ~ attr(c58,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d6,d0]) ).
cnf(d8,plain,
( ~ attr(c58,c59)
| ~ sub(c59,'name$u1$u1') ),
inference(resolution,[status(thm)],[d7,c214]) ).
cnf(d9,plain,
~ sub(c59,'name$u1$u1'),
inference(resolution,[status(thm)],[c5,d8]) ).
cnf(d10,plain,
$false,
inference(resolution,[status(thm)],[c6,d9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR113+13 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n004.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 27 01:01:54 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 127.89/17.61 % SZS status Theorem for theBenchmark.p
% 127.89/17.61 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------