%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR114+19 : 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 : n013.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:36 AM UTC 2026
% Result : Theorem 16.49s 5.77s
% Output : CNFRefutation 16.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 3
% Syntax : Number of formulae : 25 ( 8 unt; 0 def)
% Number of atoms : 329 ( 0 equ)
% Maximal formula atoms : 243 ( 13 avg)
% Number of connectives : 358 ( 54 ~; 43 |; 260 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 243 ( 14 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-2 aty)
% Number of functors : 67 ( 67 usr; 65 con; 0-2 aty)
% Number of variables : 40 ( 0 sgn 2 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_004_qapn_66,hypothesis,
( gener('zelebrieren$u1$u1',ge)
& fact('zelebrieren$u1$u1',real)
& sort('zelebrieren$u1$u1',da)
& varia('weg$u1$u1','varia$uc')
& refer('weg$u1$u1','refer$uc')
& quant('weg$u1$u1',one)
& gener('weg$u1$u1',ge)
& fact('weg$u1$u1',real)
& etype('weg$u1$u1',int0)
& card('weg$u1$u1',int1)
& sort('weg$u1$u1',d)
& varia('kreuz$u1$u1','varia$uc')
& refer('kreuz$u1$u1','refer$uc')
& quant('kreuz$u1$u1',one)
& gener('kreuz$u1$u1',ge)
& fact('kreuz$u1$u1',real)
& etype('kreuz$u1$u1',int0)
& card('kreuz$u1$u1',int1)
& sort('kreuz$u1$u1',io)
& sort('kreuz$u1$u1',d)
& varia('gl$u$u344ubig$u2$u1','varia$uc')
& refer('gl$u$u344ubig$u2$u1','refer$uc')
& quant('gl$u$u344ubig$u2$u1',one)
& gener('gl$u$u344ubig$u2$u1',ge)
& fact('gl$u$u344ubig$u2$u1',real)
& etype('gl$u$u344ubig$u2$u1',int0)
& card('gl$u$u344ubig$u2$u1',int1)
& sort('gl$u$u344ubig$u2$u1',o)
& varia(c9,'varia$uc')
& refer(c9,indet)
& quant(c9,mult)
& gener(c9,'gener$uc')
& fact(c9,real)
& etype(c9,int1)
& card(c9,cons('x$uconstant',cons(int1,nil)))
& sort(c9,o)
& varia('kreuzung$u1$u1','varia$uc')
& refer('kreuzung$u1$u1','refer$uc')
& quant('kreuzung$u1$u1',one)
& gener('kreuzung$u1$u1',ge)
& fact('kreuzung$u1$u1',real)
& etype('kreuzung$u1$u1',int0)
& card('kreuzung$u1$u1',int1)
& sort('kreuzung$u1$u1',d)
& sort('althergebracht$u1$u1',nq)
& sort('rom$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(c148,'varia$uc')
& refer(c148,indet)
& quant(c148,one)
& gener(c148,sp)
& fact(c148,real)
& etype(c148,int0)
& card(c148,int1)
& sort(c148,na)
& varia(c147,con)
& refer(c147,det)
& quant(c147,one)
& gener(c147,sp)
& fact(c147,real)
& etype(c147,int0)
& card(c147,int1)
& sort(c147,io)
& sort(c147,d)
& varia('kolosseum$u1$u1',con)
& refer('kolosseum$u1$u1',det)
& quant('kolosseum$u1$u1',one)
& gener('kolosseum$u1$u1',sp)
& fact('kolosseum$u1$u1',real)
& etype('kolosseum$u1$u1',int0)
& card('kolosseum$u1$u1',int1)
& sort('kolosseum$u1$u1',d)
& varia(c169,con)
& refer(c169,det)
& quant(c169,one)
& gener(c169,sp)
& fact(c169,real)
& etype(c169,int0)
& card(c169,int1)
& sort(c169,l)
& varia(c140,con)
& refer(c140,det)
& quant(c140,one)
& gener(c140,sp)
& fact(c140,real)
& etype(c140,int0)
& card(c140,int1)
& sort(c140,d)
& varia('freiertag$u1$u1','varia$uc')
& refer('freiertag$u1$u1','refer$uc')
& quant('freiertag$u1$u1',one)
& gener('freiertag$u1$u1',ge)
& fact('freiertag$u1$u1',real)
& etype('freiertag$u1$u1',int0)
& card('freiertag$u1$u1',int1)
& sort('freiertag$u1$u1',ta)
& sort('paul$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('johannes$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('kirchenf$u$u374rst$u1$u1','varia$uc')
& refer('kirchenf$u$u374rst$u1$u1','refer$uc')
& quant('kirchenf$u$u374rst$u1$u1',one)
& gener('kirchenf$u$u374rst$u1$u1',ge)
& fact('kirchenf$u$u374rst$u1$u1',real)
& etype('kirchenf$u$u374rst$u1$u1',int0)
& card('kirchenf$u$u374rst$u1$u1',int1)
& sort('kirchenf$u$u374rst$u1$u1',d)
& varia(c129,'varia$uc')
& refer(c129,det)
& quant(c129,one)
& gener(c129,sp)
& fact(c129,real)
& etype(c129,int0)
& card(c129,int1)
& sort(c129,na)
& varia(c128,'varia$uc')
& refer(c128,indet)
& quant(c128,one)
& gener(c128,sp)
& fact(c128,real)
& etype(c128,int0)
& card(c128,int1)
& sort(c128,na)
& varia(c135,con)
& refer(c135,det)
& quant(c135,one)
& gener(c135,sp)
& fact(c135,real)
& etype(c135,int0)
& card(c135,int1)
& sort(c135,ta)
& varia('abend$u2$u1','varia$uc')
& refer('abend$u2$u1','refer$uc')
& quant('abend$u2$u1',one)
& gener('abend$u2$u1',sp)
& fact('abend$u2$u1',real)
& etype('abend$u2$u1',int0)
& card('abend$u2$u1',int1)
& sort('abend$u2$u1',t)
& gener('haben$u1$u1',ge)
& fact('haben$u1$u1',real)
& sort('haben$u1$u1',st)
& varia(c127,'varia$uc')
& refer(c127,det)
& quant(c127,one)
& gener(c127,sp)
& fact(c127,real)
& etype(c127,int0)
& card(c127,int1)
& sort(c127,d)
& varia(c150,con)
& refer(c150,det)
& quant(c150,one)
& gener(c150,sp)
& fact(c150,real)
& etype(c150,int0)
& card(c150,int1)
& sort(c150,d)
& varia(c170,con)
& refer(c170,det)
& quant(c170,one)
& gener(c170,sp)
& fact(c170,real)
& etype(c170,int0)
& card(c170,int1)
& sort(c170,l)
& varia(c171,'varia$uc')
& refer(c171,'refer$uc')
& quant(c171,'quant$uc')
& gener(c171,'gener$uc')
& fact(c171,real)
& etype(c171,int1)
& card(c171,'card$uc')
& sort(c171,o)
& card(c130,int2)
& sort(c130,oq)
& sort(c0,tq)
& gener(c10,sp)
& fact(c10,real)
& sort(c10,st)
& chsp2('zelebrieren$u1$u1',c0)
& sub('kreuzung$u1$u1','weg$u1$u1')
& assoc('kreuzung$u1$u1','kreuz$u1$u1')
& pred(c9,'gl$u$u344ubig$u2$u1')
& subm(c171,c9)
& an(c170,c140)
& in(c169,c147)
& sub(c150,'kreuzung$u1$u1')
& prop(c150,'althergebracht$u1$u1')
& val(c148,'rom$u0')
& sub(c148,'name$u1$u1')
& sub(c147,'stadt$u$u1$u1')
& attr(c147,c148)
& sub(c140,'kolosseum$u1$u1')
& loc(c140,c169)
& sub(c135,'freiertag$u1$u1')
& val(c129,'paul$u0')
& sub(c129,'familiename$u1$u1')
& val(c128,'johannes$u0')
& sub(c128,'eigenname$u1$u1')
& sub(c127,'kirchenf$u$u374rst$u1$u1')
& attr(c127,c129)
& attr(c127,c128)
& temp(c10,c135)
& temp(c10,'abend$u2$u1')
& subs(c10,'haben$u1$u1')
& scar(c10,c127)
& obj(c10,c150)
& loc(c10,c170)
& ctxt(c10,c171)
& assoc(c10,c130)
& assoc(c10,c0) ) ).
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_004_qapn_66,conjecture,
? [X0,X1,X2,X3,X4] :
( val(X1,'rom$u0')
& subs(X4,'stehen$u1$u1')
& sub(X3,'kolosseum$u1$u1')
& sub(X0,'stadt$u$u1$u1')
& sub(X1,'name$u1$u1')
& scar(X4,X3)
& loc(X4,X2)
& attr(X0,X1)
& in(X2,X0) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4] :
( val(X1,'rom$u0')
& subs(X4,'stehen$u1$u1')
& sub(X3,'kolosseum$u1$u1')
& sub(X0,'stadt$u$u1$u1')
& sub(X1,'name$u1$u1')
& scar(X4,X3)
& loc(X4,X2)
& attr(X0,X1)
& in(X2,X0) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_004_qapn_66]) ).
cnf(c17,plain,
loc(c140,c169),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapn_66]) ).
cnf(c18,plain,
sub(c140,'kolosseum$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapn_66]) ).
cnf(c19,plain,
attr(c147,c148),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapn_66]) ).
cnf(c20,plain,
sub(c147,'stadt$u$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapn_66]) ).
cnf(c21,plain,
sub(c148,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapn_66]) ).
cnf(c22,plain,
val(c148,'rom$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapn_66]) ).
cnf(c25,plain,
in(c169,c147),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapn_66]) ).
cnf(c604,plain,
( loc(sK480(X0,X1),X1)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c605,plain,
( scar(sK480(X0,X1),X0)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c606,plain,
( subs(sK480(X0,X1),'stehen$u1$u1')
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c10614,plain,
( ~ val(X1,'rom$u0')
| ~ in(X4,X0)
| ~ loc(X3,X4)
| ~ scar(X3,X2)
| ~ sub(X1,'name$u1$u1')
| ~ subs(X3,'stehen$u1$u1')
| ~ sub(X2,'kolosseum$u1$u1')
| ~ attr(X0,X1)
| ~ sub(X0,'stadt$u$u1$u1') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ val(X2,'rom$u0')
| ~ sub(X1,'kolosseum$u1$u1')
| ~ sub(c147,'stadt$u$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ attr(c147,X2)
| ~ subs(X0,'stehen$u1$u1')
| ~ scar(X0,X1)
| ~ loc(X0,c169) ),
inference(resolution,[status(thm)],[c25,c10614]) ).
cnf(d1,plain,
( ~ val(X2,'rom$u0')
| ~ sub(X1,'kolosseum$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ attr(c147,X2)
| ~ subs(X0,'stehen$u1$u1')
| ~ scar(X0,X1)
| ~ loc(X0,c169) ),
inference(resolution,[status(thm)],[c20,d0]) ).
cnf(d2,plain,
( ~ sub(X1,'kolosseum$u1$u1')
| ~ sub(c148,'name$u1$u1')
| ~ attr(c147,c148)
| ~ subs(X0,'stehen$u1$u1')
| ~ scar(X0,X1)
| ~ loc(X0,c169) ),
inference(resolution,[status(thm)],[d1,c22]) ).
cnf(d3,plain,
( ~ sub(c148,'name$u1$u1')
| ~ sub(X1,'kolosseum$u1$u1')
| ~ subs(X0,'stehen$u1$u1')
| ~ scar(X0,X1)
| ~ loc(X0,c169) ),
inference(resolution,[status(thm)],[c19,d2]) ).
cnf(d4,plain,
( ~ sub(X1,'kolosseum$u1$u1')
| ~ subs(X0,'stehen$u1$u1')
| ~ scar(X0,X1)
| ~ loc(X0,c169) ),
inference(resolution,[status(thm)],[c21,d3]) ).
cnf(d5,plain,
( ~ subs(X0,'stehen$u1$u1')
| ~ scar(X0,c140)
| ~ loc(X0,c169) ),
inference(resolution,[status(thm)],[d4,c18]) ).
cnf(d6,plain,
( ~ scar(sK480(X0,X1),c140)
| ~ loc(sK480(X0,X1),c169)
| ~ loc(X0,X1) ),
inference(resolution,[status(thm)],[c606,d5]) ).
cnf(d7,plain,
( ~ loc(c140,X0)
| ~ loc(sK480(c140,X0),c169)
| ~ loc(c140,X0) ),
inference(resolution,[status(thm)],[d6,c605]) ).
cnf(d8,plain,
( ~ loc(c140,c169)
| ~ loc(c140,c169) ),
inference(resolution,[status(thm)],[d7,c604]) ).
cnf(d9,plain,
$false,
inference(resolution,[status(thm)],[c17,d8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR114+19 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n013.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:04:51 UTC 2026
% 0.12/0.35 % CPUTime :
% 0.12/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.49/5.77 % SZS status Theorem for theBenchmark.p
% 16.49/5.77 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------