%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR114+26 : 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 : 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:37 AM UTC 2026
% Result : Theorem 42.02s 11.02s
% Output : CNFRefutation 42.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 3
% Syntax : Number of formulae : 25 ( 9 unt; 0 def)
% Number of atoms : 318 ( 0 equ)
% Maximal formula atoms : 231 ( 12 avg)
% Number of connectives : 348 ( 55 ~; 44 |; 248 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 231 ( 14 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-3 aty)
% Number of functors : 73 ( 73 usr; 71 con; 0-2 aty)
% Number of variables : 45 ( 0 sgn 2 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_004_qapw_82,hypothesis,
( varia('spiel$u1$u2','varia$uc')
& refer('spiel$u1$u2','refer$uc')
& quant('spiel$u1$u2',one)
& gener('spiel$u1$u2',ge)
& fact('spiel$u1$u2',real)
& etype('spiel$u1$u2',int0)
& card('spiel$u1$u2',int1)
& sort('spiel$u1$u2',ad)
& varia('gefecht$u1$u1','varia$uc')
& refer('gefecht$u1$u1','refer$uc')
& quant('gefecht$u1$u1',one)
& gener('gefecht$u1$u1',ge)
& fact('gefecht$u1$u1',real)
& etype('gefecht$u1$u1',int0)
& card('gefecht$u1$u1',int1)
& sort('gefecht$u1$u1',ad)
& 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(c89,'varia$uc')
& refer(c89,indet)
& quant(c89,one)
& gener(c89,sp)
& fact(c89,real)
& etype(c89,int0)
& card(c89,int1)
& sort(c89,na)
& varia(c88,con)
& refer(c88,det)
& quant(c88,one)
& gener(c88,sp)
& fact(c88,real)
& etype(c88,int0)
& card(c88,int1)
& sort(c88,io)
& sort(c88,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(c91,con)
& refer(c91,det)
& quant(c91,one)
& gener(c91,sp)
& fact(c91,real)
& etype(c91,int0)
& card(c91,int1)
& sort(c91,l)
& varia(c81,'varia$uc')
& refer(c81,'refer$uc')
& quant(c81,'quant$uc')
& gener(c81,'gener$uc')
& fact(c81,real)
& etype(c81,int2)
& etype(c81,int1)
& card(c81,'card$uc')
& sort(c81,o)
& sort('bekannt$u1$u1',nq)
& varia('beispiel$u1$u1','varia$uc')
& refer('beispiel$u1$u1','refer$uc')
& quant('beispiel$u1$u1',one)
& gener('beispiel$u1$u1',ge)
& fact('beispiel$u1$u1',real)
& etype('beispiel$u1$u1',int0)
& card('beispiel$u1$u1',int1)
& sort('beispiel$u1$u1',io)
& sort(c80,tq)
& gener('eintreffen$u1$u2',ge)
& fact('eintreffen$u1$u2',real)
& sort('eintreffen$u1$u2',dn)
& varia(c73,con)
& refer(c73,det)
& quant(c73,mult)
& gener(c73,sp)
& fact(c73,real)
& etype(c73,int1)
& card(c73,cons('x$uconstant',cons(int1,nil)))
& sort(c73,l)
& varia(c74,'varia$uc')
& refer(c74,indet)
& quant(c74,nfquant)
& gener(c74,sp)
& fact(c74,real)
& etype(c74,int2)
& card(c74,int2)
& sort(c74,o)
& gener(c67,sp)
& fact(c67,real)
& sort(c67,dn)
& varia('tierhatz$u1$u1','varia$uc')
& refer('tierhatz$u1$u1','refer$uc')
& quant('tierhatz$u1$u1',one)
& gener('tierhatz$u1$u1',ge)
& fact('tierhatz$u1$u1',real)
& etype('tierhatz$u1$u1',int0)
& card('tierhatz$u1$u1',int1)
& sort('tierhatz$u1$u1',o)
& varia(c66,'varia$uc')
& refer(c66,indet)
& quant(c66,mult)
& gener(c66,sp)
& fact(c66,real)
& etype(c66,int1)
& card(c66,cons('x$uconstant',cons(int1,nil)))
& sort(c66,o)
& gener('haben$u1$u1',ge)
& fact('haben$u1$u1',real)
& sort('haben$u1$u1',st)
& gener('weitaus$u1$u1','gener$uc')
& fact('weitaus$u1$u1',real)
& sort('weitaus$u1$u1',md)
& varia(c76,'varia$uc')
& refer(c76,'refer$uc')
& quant(c76,one)
& gener(c76,'gener$uc')
& fact(c76,real)
& etype(c76,int0)
& card(c76,int1)
& sort(c76,io)
& varia(c82,con)
& refer(c82,det)
& quant(c82,one)
& gener(c82,sp)
& fact(c82,real)
& etype(c82,int0)
& card(c82,int1)
& sort(c82,d)
& gener(c5,sp)
& fact(c5,real)
& sort(c5,st)
& varia('bedeutung$u1$u1','varia$uc')
& refer('bedeutung$u1$u1','refer$uc')
& quant('bedeutung$u1$u1',one)
& gener('bedeutung$u1$u1',ge)
& fact('bedeutung$u1$u1',real)
& etype('bedeutung$u1$u1',int0)
& card('bedeutung$u1$u1',int1)
& sort('bedeutung$u1$u1',io)
& sort('gro$u$u337$u1$u1',mq)
& varia(c4,'varia$uc')
& refer(c4,'refer$uc')
& quant(c4,one)
& gener(c4,sp)
& fact(c4,real)
& etype(c4,int0)
& card(c4,int1)
& sort(c4,io)
& varia('kampfspiel$u1$u2','varia$uc')
& refer('kampfspiel$u1$u2','refer$uc')
& quant('kampfspiel$u1$u2',one)
& gener('kampfspiel$u1$u2',ge)
& fact('kampfspiel$u1$u2',real)
& etype('kampfspiel$u1$u2',int0)
& card('kampfspiel$u1$u2',int1)
& sort('kampfspiel$u1$u2',ad)
& varia(c32,'varia$uc')
& refer(c32,indet)
& quant(c32,mult)
& gener(c32,sp)
& fact(c32,real)
& etype(c32,int1)
& card(c32,cons('x$uconstant',cons(int1,nil)))
& sort(c32,ab)
& varia('amphi$utheater$u1$u1','varia$uc')
& refer('amphi$utheater$u1$u1','refer$uc')
& quant('amphi$utheater$u1$u1',one)
& gener('amphi$utheater$u1$u1',ge)
& fact('amphi$utheater$u1$u1',real)
& etype('amphi$utheater$u1$u1',int0)
& card('amphi$utheater$u1$u1',int1)
& sort('amphi$utheater$u1$u1',o)
& varia(c10,con)
& refer(c10,det)
& quant(c10,'quant$uc')
& gener(c10,sp)
& fact(c10,real)
& etype(c10,'etype$uc')
& card(c10,'card$uc')
& sort(c10,re)
& sort(c10,ta)
& sort(c10,mo)
& sort(c10,io)
& sort(c10,co)
& sort(c10,abs)
& subs('kampfspiel$u1$u2','spiel$u1$u2')
& assoc('kampfspiel$u1$u2','gefecht$u1$u1')
& in(c91,c88)
& val(c89,'rom$u0')
& sub(c89,'name$u1$u1')
& sub(c88,'stadt$u$u1$u1')
& attr(c88,c89)
& sub(c82,'kolosseum$u1$u1')
& loc(c82,c91)
& supl(c80,'bekannt$u1$u1',c81)
& sub(c76,'beispiel$u1$u1')
& prop(c76,c80)
& itms(c74,c32,c66)
& in(c73,c10)
& subs(c67,'eintreffen$u1$u2')
& loc(c67,c73)
& exp(c67,c74)
& pred(c66,'tierhatz$u1$u1')
& subs(c5,'haben$u1$u1')
& scar(c5,c10)
& obj(c5,c4)
& modl(c5,'weitaus$u1$u1')
& ctxt(c5,c76)
& assoc(c5,c82)
& sub(c4,'bedeutung$u1$u1')
& prop(c4,'gro$u$u337$u1$u1')
& pred(c32,'kampfspiel$u1$u2')
& pred(c10,'amphi$utheater$u1$u1') ) ).
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_82,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_82]) ).
cnf(c19,plain,
loc(c82,c91),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_82]) ).
cnf(c20,plain,
sub(c82,'kolosseum$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_82]) ).
cnf(c21,plain,
attr(c88,c89),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_82]) ).
cnf(c22,plain,
sub(c88,'stadt$u$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_82]) ).
cnf(c23,plain,
sub(c89,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_82]) ).
cnf(c24,plain,
val(c89,'rom$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_82]) ).
cnf(c25,plain,
in(c91,c88),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_82]) ).
cnf(c592,plain,
( loc(sK480(X0,X1),X1)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c593,plain,
( scar(sK480(X0,X1),X0)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c594,plain,
( subs(sK480(X0,X1),'stehen$u1$u1')
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c10602,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,
( ~ attr(X0,c89)
| ~ in(X3,X0)
| ~ loc(X2,X3)
| ~ subs(X2,'stehen$u1$u1')
| ~ scar(X2,X1)
| ~ sub(X1,'kolosseum$u1$u1')
| ~ sub(X0,'stadt$u$u1$u1')
| ~ sub(c89,'name$u1$u1') ),
inference(resolution,[status(thm)],[c24,c10602]) ).
cnf(d1,plain,
( ~ attr(X1,c89)
| ~ in(X3,X1)
| ~ loc(X2,X3)
| ~ subs(X2,'stehen$u1$u1')
| ~ scar(X2,X0)
| ~ sub(X1,'stadt$u$u1$u1')
| ~ sub(X0,'kolosseum$u1$u1') ),
inference(resolution,[status(thm)],[c23,d0]) ).
cnf(d2,plain,
( ~ in(X2,c88)
| ~ loc(X1,X2)
| ~ subs(X1,'stehen$u1$u1')
| ~ scar(X1,X0)
| ~ sub(X0,'kolosseum$u1$u1')
| ~ sub(c88,'stadt$u$u1$u1') ),
inference(resolution,[status(thm)],[d1,c21]) ).
cnf(d3,plain,
( ~ in(X2,c88)
| ~ loc(X1,X2)
| ~ subs(X1,'stehen$u1$u1')
| ~ scar(X1,X0)
| ~ sub(X0,'kolosseum$u1$u1') ),
inference(resolution,[status(thm)],[c22,d2]) ).
cnf(d4,plain,
( ~ loc(X1,c91)
| ~ subs(X1,'stehen$u1$u1')
| ~ scar(X1,X0)
| ~ sub(X0,'kolosseum$u1$u1') ),
inference(resolution,[status(thm)],[d3,c25]) ).
cnf(d5,plain,
( ~ subs(sK480(X0,c91),'stehen$u1$u1')
| ~ scar(sK480(X0,c91),X1)
| ~ sub(X1,'kolosseum$u1$u1')
| ~ loc(X0,c91) ),
inference(resolution,[status(thm)],[c592,d4]) ).
cnf(d6,plain,
( ~ loc(X0,c91)
| ~ scar(sK480(X0,c91),X1)
| ~ sub(X1,'kolosseum$u1$u1')
| ~ loc(X0,c91) ),
inference(resolution,[status(thm)],[c594,d5]) ).
cnf(d7,plain,
( ~ loc(X0,c91)
| ~ loc(X0,c91)
| ~ sub(X0,'kolosseum$u1$u1') ),
inference(resolution,[status(thm)],[d6,c593]) ).
cnf(d8,plain,
~ sub(c82,'kolosseum$u1$u1'),
inference(resolution,[status(thm)],[d7,c19]) ).
cnf(d9,plain,
$false,
inference(resolution,[status(thm)],[c20,d8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR114+26 : 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/5.57 % Computer : n008.cluster.edu
% 0.08/5.57 % Model : x86_64 x86_64
% 0.08/5.57 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.57 % Memory : 8046.5625MB
% 0.08/5.57 % OS : Linux 6.8.0-71-generic
% 0.08/5.57 % CPULimit : 300
% 0.08/5.57 % WCLimit : 300
% 0.08/5.57 % DateTime : Sun Sep 27 01:06:47 UTC 2026
% 0.08/5.57 % CPUTime :
% 0.08/5.57 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 42.02/11.02 % SZS status Theorem for theBenchmark.p
% 42.02/11.02 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------