%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR114+25 : 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 : n007.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:37 AM UTC 2026
% Result : Theorem 90.99s 18.84s
% Output : CNFRefutation 90.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 3
% Syntax : Number of formulae : 25 ( 9 unt; 0 def)
% Number of atoms : 307 ( 0 equ)
% Maximal formula atoms : 215 ( 12 avg)
% Number of connectives : 342 ( 60 ~; 49 |; 232 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 215 ( 13 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 29 ( 28 usr; 1 prp; 0-2 aty)
% Number of functors : 65 ( 65 usr; 63 con; 0-2 aty)
% Number of variables : 46 ( 0 sgn 2 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_004_qapw_81,hypothesis,
( varia('art$u1$u1','varia$uc')
& refer('art$u1$u1','refer$uc')
& quant('art$u1$u1','quant$uc')
& gener('art$u1$u1',ge)
& fact('art$u1$u1',real)
& etype('art$u1$u1',int1)
& card('art$u1$u1','card$uc')
& sort('art$u1$u1',ad)
& varia(c9853,'varia$uc')
& refer(c9853,det)
& quant(c9853,one)
& gener(c9853,sp)
& fact(c9853,real)
& etype(c9853,int1)
& card(c9853,int1)
& sort(c9853,ad)
& sort('spaet$u1$u1',mq)
& varia('anlage$u1$u1','varia$uc')
& refer('anlage$u1$u1','refer$uc')
& quant('anlage$u1$u1',one)
& gener('anlage$u1$u1',ge)
& fact('anlage$u1$u1',real)
& etype('anlage$u1$u1',int0)
& card('anlage$u1$u1',int1)
& sort('anlage$u1$u1',as)
& varia('technik$u$u1$u1','varia$uc')
& refer('technik$u$u1$u1','refer$uc')
& quant('technik$u$u1$u1',one)
& gener('technik$u$u1$u1',ge)
& fact('technik$u$u1$u1',real)
& etype('technik$u$u1$u1',int0)
& card('technik$u$u1$u1',int1)
& sort('technik$u$u1$u1',io)
& varia('man$u1$u1','varia$uc')
& refer('man$u1$u1','refer$uc')
& quant('man$u1$u1',one)
& gener('man$u1$u1',ge)
& fact('man$u1$u1',real)
& etype('man$u1$u1',int0)
& card('man$u1$u1',int1)
& sort('man$u1$u1',d)
& gener('geben$u1$u4',ge)
& fact('geben$u1$u4',real)
& sort('geben$u1$u4',da)
& varia(c9837,con)
& refer(c9837,det)
& quant(c9837,one)
& gener(c9837,sp)
& fact(c9837,real)
& etype(c9837,int0)
& card(c9837,int1)
& sort(c9837,io)
& gener('nicht$u1$u1','gener$uc')
& fact('nicht$u1$u1',real)
& sort('nicht$u1$u1',md)
& sort('wie$u1$u1',mq)
& varia(c9847,'varia$uc')
& refer(c9847,det)
& quant(c9847,mult)
& gener(c9847,sp)
& fact(c9847,real)
& etype(c9847,int1)
& card(c9847,cons('x$uconstant',cons(int1,nil)))
& sort(c9847,as)
& varia(c9825,'varia$uc')
& refer(c9825,det)
& quant(c9825,one)
& gener(c9825,sp)
& fact(c9825,real)
& etype(c9825,int0)
& card(c9825,int1)
& sort(c9825,o)
& gener('haben$u1$u1',ge)
& fact('haben$u1$u1',real)
& sort('haben$u1$u1',st)
& varia(c4,'varia$uc')
& refer(c4,'refer$uc')
& quant(c4,one)
& gener(c4,ge)
& fact(c4,real)
& etype(c4,int0)
& card(c4,int1)
& sort(c4,d)
& gener(c24,sp)
& fact(c24,real)
& sort(c24,da)
& gener(c21,sp)
& fact(c21,real)
& sort(c21,st)
& varia('bau$u1$u1','varia$uc')
& refer('bau$u1$u1','refer$uc')
& quant('bau$u1$u1',one)
& gener('bau$u1$u1',ge)
& fact('bau$u1$u1',real)
& etype('bau$u1$u1',int0)
& card('bau$u1$u1',int1)
& sort('bau$u1$u1',d)
& varia(c20,'varia$uc')
& refer(c20,det)
& quant(c20,mult)
& gener(c20,sp)
& fact(c20,real)
& etype(c20,int1)
& card(c20,cons('x$uconstant',cons(int1,nil)))
& sort(c20,d)
& 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(c13132,'varia$uc')
& refer(c13132,indet)
& quant(c13132,one)
& gener(c13132,sp)
& fact(c13132,real)
& etype(c13132,int0)
& card(c13132,int1)
& sort(c13132,na)
& varia(c13131,con)
& refer(c13131,det)
& quant(c13131,one)
& gener(c13131,sp)
& fact(c13131,real)
& etype(c13131,int0)
& card(c13131,int1)
& sort(c13131,io)
& sort(c13131,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(c13134,con)
& refer(c13134,det)
& quant(c13134,one)
& gener(c13134,sp)
& fact(c13134,real)
& etype(c13134,int0)
& card(c13134,int1)
& sort(c13134,l)
& varia(c13125,con)
& refer(c13125,det)
& quant(c13125,one)
& gener(c13125,sp)
& fact(c13125,real)
& etype(c13125,int0)
& card(c13125,int1)
& sort(c13125,d)
& varia('er$ufahrung$u1$u1','varia$uc')
& refer('er$ufahrung$u1$u1','refer$uc')
& quant('er$ufahrung$u1$u1',one)
& gener('er$ufahrung$u1$u1',ge)
& fact('er$ufahrung$u1$u1',real)
& etype('er$ufahrung$u1$u1',int0)
& card('er$ufahrung$u1$u1',int1)
& sort('er$ufahrung$u1$u1',io)
& sort('er$ufahrung$u1$u1',as)
& varia(c11,'varia$uc')
& refer(c11,indet)
& quant(c11,mult)
& gener(c11,sp)
& fact(c11,nonreal)
& etype(c11,int1)
& card(c11,cons('x$uconstant',cons(int1,nil)))
& sort(c11,io)
& sort(c11,as)
& sort(c0,tq)
& gener('auskl$u$u374geln$u1$u1',ge)
& fact('auskl$u$u374geln$u1$u1',real)
& sort('auskl$u$u374geln$u1$u1',dn)
& subs(c9853,'art$u1$u1')
& attch(c9853,c9847)
& prop(c9847,'spaet$u1$u1')
& preds(c9847,'anlage$u1$u1')
& sub(c9837,'technik$u$u1$u1')
& prop(c9837,c0)
& sub(c4,'man$u1$u1')
& subs(c24,'geben$u1$u4')
& obj(c24,c9837)
& modl(c24,'nicht$u1$u1')
& mannr(c24,'wie$u1$u1')
& circ(c24,c9847)
& benf(c24,c13125)
& agt(c24,c9825)
& subs(c21,'haben$u1$u1')
& scar(c21,c4)
& reas(c21,c24)
& obj(c21,c11)
& assoc(c21,c20)
& pred(c20,'bau$u1$u1')
& in(c13134,c13131)
& val(c13132,'rom$u0')
& sub(c13132,'name$u1$u1')
& sub(c13131,'stadt$u$u1$u1')
& attr(c13131,c13132)
& sub(c13125,'kolosseum$u1$u1')
& loc(c13125,c13134)
& pred(c11,'er$ufahrung$u1$u1')
& chsp2('auskl$u$u374geln$u1$u1',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_qapw_81,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_qapw_81]) ).
cnf(c2,plain,
loc(c13125,c13134),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_81]) ).
cnf(c3,plain,
sub(c13125,'kolosseum$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_81]) ).
cnf(c4,plain,
attr(c13131,c13132),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_81]) ).
cnf(c5,plain,
sub(c13131,'stadt$u$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_81]) ).
cnf(c6,plain,
sub(c13132,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_81]) ).
cnf(c7,plain,
val(c13132,'rom$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_81]) ).
cnf(c8,plain,
in(c13134,c13131),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_81]) ).
cnf(c407,plain,
( loc(sK271(X0,X1),X1)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c408,plain,
( scar(sK271(X0,X1),X0)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c409,plain,
( subs(sK271(X0,X1),'stehen$u1$u1')
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c435,plain,
( ~ sub(X2,'name$u1$u1')
| ~ sub(X4,'kolosseum$u1$u1')
| ~ scar(X1,X4)
| ~ loc(X1,X3)
| ~ in(X3,X0)
| ~ val(X2,'rom$u0')
| ~ attr(X0,X2)
| ~ subs(X1,'stehen$u1$u1')
| ~ sub(X0,'stadt$u$u1$u1') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ scar(sK271(X0,X1),X3)
| ~ in(X2,X5)
| ~ val(X4,'rom$u0')
| ~ attr(X5,X4)
| ~ sub(X5,'stadt$u$u1$u1')
| ~ sub(X4,'name$u1$u1')
| ~ sub(X3,'kolosseum$u1$u1')
| ~ loc(sK271(X0,X1),X2)
| ~ loc(X0,X1) ),
inference(resolution,[status(thm)],[c409,c435]) ).
cnf(d1,plain,
( ~ loc(X0,X1)
| ~ in(X2,X3)
| ~ val(X4,'rom$u0')
| ~ attr(X3,X4)
| ~ sub(X0,'kolosseum$u1$u1')
| ~ sub(X4,'name$u1$u1')
| ~ sub(X3,'stadt$u$u1$u1')
| ~ loc(sK271(X0,X1),X2)
| ~ loc(X0,X1) ),
inference(resolution,[status(thm)],[d0,c408]) ).
cnf(d2,plain,
( ~ loc(X0,X1)
| ~ in(X1,X3)
| ~ val(X2,'rom$u0')
| ~ attr(X3,X2)
| ~ sub(X0,'kolosseum$u1$u1')
| ~ sub(X3,'stadt$u$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ loc(X0,X1) ),
inference(resolution,[status(thm)],[d1,c407]) ).
cnf(d3,plain,
( ~ val(X1,'rom$u0')
| ~ attr(c13131,X1)
| ~ sub(X0,'kolosseum$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(c13131,'stadt$u$u1$u1')
| ~ loc(X0,c13134) ),
inference(resolution,[status(thm)],[d2,c8]) ).
cnf(d4,plain,
( ~ val(X1,'rom$u0')
| ~ attr(c13131,X1)
| ~ sub(X0,'kolosseum$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ loc(X0,c13134) ),
inference(resolution,[status(thm)],[c5,d3]) ).
cnf(d5,plain,
( ~ attr(c13131,c13132)
| ~ sub(X0,'kolosseum$u1$u1')
| ~ sub(c13132,'name$u1$u1')
| ~ loc(X0,c13134) ),
inference(resolution,[status(thm)],[d4,c7]) ).
cnf(d6,plain,
( ~ sub(c13132,'name$u1$u1')
| ~ sub(X0,'kolosseum$u1$u1')
| ~ loc(X0,c13134) ),
inference(resolution,[status(thm)],[c4,d5]) ).
cnf(d7,plain,
( ~ sub(X0,'kolosseum$u1$u1')
| ~ loc(X0,c13134) ),
inference(resolution,[status(thm)],[c6,d6]) ).
cnf(d8,plain,
~ loc(c13125,c13134),
inference(resolution,[status(thm)],[d7,c3]) ).
cnf(d9,plain,
$false,
inference(resolution,[status(thm)],[c2,d8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR114+25 : 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.09/5.38 % Computer : n007.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Sun Sep 27 01:04:00 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 90.99/18.84 % SZS status Theorem for theBenchmark.p
% 90.99/18.84 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------