%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR114+3 : 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 : n012.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:38 AM UTC 2026
% Result : Theorem 18.88s 6.79s
% Output : CNFRefutation 18.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 3
% Syntax : Number of formulae : 25 ( 9 unt; 0 def)
% Number of atoms : 365 ( 0 equ)
% Maximal formula atoms : 273 ( 14 avg)
% Number of connectives : 400 ( 60 ~; 49 |; 290 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 273 ( 16 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-2 aty)
% Number of functors : 69 ( 69 usr; 67 con; 0-2 aty)
% Number of variables : 44 ( 0 sgn 2 !; 11 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_004_insicht_2,hypothesis,
( varia('eltern$u1$u1','varia$uc')
& refer('eltern$u1$u1','refer$uc')
& quant('eltern$u1$u1',one)
& gener('eltern$u1$u1',ge)
& fact('eltern$u1$u1',real)
& etype('eltern$u1$u1',int0)
& card('eltern$u1$u1',int1)
& sort('eltern$u1$u1',d)
& card(c1,int1970)
& sort(c1,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)
& sort('rom$u0',fe)
& varia(c5,'varia$uc')
& refer(c5,'refer$uc')
& quant(c5,'quant$uc')
& gener(c5,sp)
& fact(c5,real)
& etype(c5,'etype$uc')
& card(c5,'card$uc')
& sort(c5,ta)
& sort(c5,oa)
& sort(c5,me)
& 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(c400,'varia$uc')
& refer(c400,indet)
& quant(c400,one)
& gener(c400,sp)
& fact(c400,real)
& etype(c400,int0)
& card(c400,int1)
& sort(c400,na)
& varia(c399,con)
& refer(c399,det)
& quant(c399,one)
& gener(c399,sp)
& fact(c399,real)
& etype(c399,int0)
& card(c399,int1)
& sort(c399,io)
& sort(c399,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(c402,con)
& refer(c402,det)
& quant(c402,one)
& gener(c402,sp)
& fact(c402,real)
& etype(c402,int0)
& card(c402,int1)
& sort(c402,l)
& varia(c393,con)
& refer(c393,det)
& quant(c393,one)
& gener(c393,sp)
& fact(c393,real)
& etype(c393,int0)
& card(c393,int1)
& sort(c393,d)
& varia('konzert$u$u1$u1','varia$uc')
& refer('konzert$u$u1$u1','refer$uc')
& quant('konzert$u$u1$u1',one)
& gener('konzert$u$u1$u1',ge)
& fact('konzert$u$u1$u1',real)
& etype('konzert$u$u1$u1',int0)
& card('konzert$u$u1$u1',int1)
& sort('konzert$u$u1$u1',io)
& sort('konzert$u$u1$u1',d)
& sort('konzert$u$u1$u1',ad)
& varia(c403,con)
& refer(c403,det)
& quant(c403,one)
& gener(c403,sp)
& fact(c403,real)
& etype(c403,int0)
& card(c403,int1)
& sort(c403,l)
& gener('aufnehmen$u1$u1',ge)
& fact('aufnehmen$u1$u1',real)
& sort('aufnehmen$u1$u1',dn)
& varia(c389,con)
& refer(c389,det)
& quant(c389,one)
& gener(c389,sp)
& fact(c389,real)
& etype(c389,int0)
& card(c389,int1)
& sort(c389,io)
& sort(c389,d)
& sort(c389,ad)
& gener(c384,sp)
& fact(c384,real)
& sort(c384,dn)
& sort('italien$u0',fe)
& varia(c35,'varia$uc')
& refer(c35,indet)
& quant(c35,one)
& gener(c35,sp)
& fact(c35,real)
& etype(c35,int0)
& card(c35,int1)
& sort(c35,na)
& varia(c34,con)
& refer(c34,det)
& quant(c34,one)
& gener(c34,sp)
& fact(c34,real)
& etype(c34,int0)
& card(c34,int1)
& sort(c34,io)
& sort(c34,d)
& varia(c4,con)
& refer(c4,det)
& quant(c4,one)
& gener(c4,sp)
& fact(c4,real)
& etype(c4,int0)
& card(c4,int1)
& sort(c4,t)
& gener('gehen$u1$u1',ge)
& fact('gehen$u1$u1',real)
& sort('gehen$u1$u1',da)
& varia(c38,con)
& refer(c38,det)
& quant(c38,one)
& gener(c38,sp)
& fact(c38,real)
& etype(c38,int0)
& card(c38,int1)
& sort(c38,l)
& varia('retro$u1$u1','varia$uc')
& refer('retro$u1$u1','refer$uc')
& quant('retro$u1$u1',one)
& gener('retro$u1$u1',sp)
& fact('retro$u1$u1',real)
& etype('retro$u1$u1',int0)
& card('retro$u1$u1',int1)
& sort('retro$u1$u1',l)
& varia(c37,con)
& refer(c37,det)
& quant(c37,one)
& gener(c37,sp)
& fact(c37,real)
& etype(c37,int0)
& card(c37,int1)
& sort(c37,l)
& gener(c3,sp)
& fact(c3,real)
& sort(c3,da)
& varia('sohn$u1$u1','varia$uc')
& refer('sohn$u1$u1','refer$uc')
& quant('sohn$u1$u1',one)
& gener('sohn$u1$u1',ge)
& fact('sohn$u1$u1',real)
& etype('sohn$u1$u1',int0)
& card('sohn$u1$u1',int1)
& sort('sohn$u1$u1',d)
& varia(c25,con)
& refer(c25,det)
& quant(c25,one)
& gener(c25,sp)
& fact(c25,real)
& etype(c25,int0)
& card(c25,int1)
& sort(c25,d)
& sort('schweiz$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('land$u1$u1','varia$uc')
& refer('land$u1$u1','refer$uc')
& quant('land$u1$u1',one)
& gener('land$u1$u1',ge)
& fact('land$u1$u1',real)
& etype('land$u1$u1',int0)
& card('land$u1$u1',int1)
& sort('land$u1$u1',io)
& sort('land$u1$u1',d)
& varia(c21,'varia$uc')
& refer(c21,indet)
& quant(c21,one)
& gener(c21,sp)
& fact(c21,real)
& etype(c21,int0)
& card(c21,int1)
& sort(c21,na)
& varia(c20,con)
& refer(c20,det)
& quant(c20,one)
& gener(c20,sp)
& fact(c20,real)
& etype(c20,int0)
& card(c20,int1)
& sort(c20,io)
& sort(c20,d)
& varia(c9,'varia$uc')
& refer(c9,det)
& quant(c9,mult)
& gener(c9,sp)
& fact(c9,real)
& etype(c9,int1)
& card(c9,cons('x$uconstant',cons(int1,nil)))
& sort(c9,d)
& varia(c13,'varia$uc')
& refer(c13,det)
& quant(c13,one)
& gener(c13,sp)
& fact(c13,real)
& etype(c13,int0)
& card(c13,int1)
& sort(c13,o)
& pred(c9,'eltern$u1$u1')
& val(c5,c1)
& sub(c5,'jahr$u$u1$u1')
& in(c403,c393)
& in(c402,c399)
& val(c400,'rom$u0')
& sub(c400,'name$u1$u1')
& attr(c4,c5)
& sub(c399,'stadt$u$u1$u1')
& attr(c399,c400)
& sub(c393,'kolosseum$u1$u1')
& loc(c393,c402)
& sub(c389,'konzert$u$u1$u1')
& loc(c389,c403)
& subs(c384,'aufnehmen$u1$u1')
& obj(c384,c389)
& flp(c38,c20)
& flp(c37,c34)
& val(c35,'italien$u0')
& sub(c35,'name$u1$u1')
& sub(c34,'land$u1$u1')
& attr(c34,c35)
& temp(c3,c4)
& subs(c3,'gehen$u1$u1')
& origl(c3,c38)
& loc(c3,'retro$u1$u1')
& dircl(c3,c37)
& assoc(c3,c25)
& agt(c3,c9)
& sub(c25,'sohn$u1$u1')
& val(c21,'schweiz$u0')
& sub(c21,'name$u1$u1')
& sub(c20,'land$u1$u1')
& attr(c20,c21)
& attch(c13,c9) ) ).
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_insicht_2,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_insicht_2]) ).
cnf(c23,plain,
loc(c393,c402),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_insicht_2]) ).
cnf(c24,plain,
sub(c393,'kolosseum$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_insicht_2]) ).
cnf(c25,plain,
attr(c399,c400),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_insicht_2]) ).
cnf(c26,plain,
sub(c399,'stadt$u$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_insicht_2]) ).
cnf(c28,plain,
sub(c400,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_insicht_2]) ).
cnf(c29,plain,
val(c400,'rom$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_insicht_2]) ).
cnf(c30,plain,
in(c402,c399),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_insicht_2]) ).
cnf(c437,plain,
( loc(sK240(X0,X1),X1)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c438,plain,
( scar(sK240(X0,X1),X0)
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c439,plain,
( subs(sK240(X0,X1),'stehen$u1$u1')
| ~ loc(X0,X1) ),
inference(clausification,[status(esa)],[loc__stehen_1_1_loc]) ).
cnf(c462,plain,
( ~ sub(X0,'stadt$u$u1$u1')
| ~ subs(X3,'stehen$u1$u1')
| ~ val(X1,'rom$u0')
| ~ loc(X3,X2)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X4,'kolosseum$u1$u1')
| ~ scar(X3,X4)
| ~ in(X2,X0)
| ~ attr(X0,X1) ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ in(X4,X2)
| ~ subs(sK240(X0,X1),'stehen$u1$u1')
| ~ loc(sK240(X0,X1),X4)
| ~ val(X3,'rom$u0')
| ~ sub(X0,'kolosseum$u1$u1')
| ~ sub(X2,'stadt$u$u1$u1')
| ~ sub(X3,'name$u1$u1')
| ~ attr(X2,X3)
| ~ loc(X0,X1) ),
inference(resolution,[status(thm)],[c438,c462]) ).
cnf(d1,plain,
( ~ loc(X2,X3)
| ~ in(X4,X0)
| ~ loc(sK240(X2,X3),X4)
| ~ loc(X2,X3)
| ~ val(X1,'rom$u0')
| ~ sub(X2,'kolosseum$u1$u1')
| ~ sub(X0,'stadt$u$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[d0,c439]) ).
cnf(d2,plain,
( ~ loc(X2,X3)
| ~ in(X3,X0)
| ~ loc(X2,X3)
| ~ val(X1,'rom$u0')
| ~ sub(X0,'stadt$u$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X2,'kolosseum$u1$u1')
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[d1,c437]) ).
cnf(d3,plain,
( ~ loc(X1,c402)
| ~ val(X0,'rom$u0')
| ~ sub(c399,'stadt$u$u1$u1')
| ~ sub(X0,'name$u1$u1')
| ~ sub(X1,'kolosseum$u1$u1')
| ~ attr(c399,X0) ),
inference(resolution,[status(thm)],[d2,c30]) ).
cnf(d4,plain,
( ~ loc(X1,c402)
| ~ val(X0,'rom$u0')
| ~ sub(X0,'name$u1$u1')
| ~ sub(X1,'kolosseum$u1$u1')
| ~ attr(c399,X0) ),
inference(resolution,[status(thm)],[c26,d3]) ).
cnf(d5,plain,
( ~ val(X0,'rom$u0')
| ~ sub(X0,'name$u1$u1')
| ~ sub(c393,'kolosseum$u1$u1')
| ~ attr(c399,X0) ),
inference(resolution,[status(thm)],[d4,c23]) ).
cnf(d6,plain,
( ~ val(X0,'rom$u0')
| ~ sub(X0,'name$u1$u1')
| ~ attr(c399,X0) ),
inference(resolution,[status(thm)],[c24,d5]) ).
cnf(d7,plain,
( ~ sub(c400,'name$u1$u1')
| ~ attr(c399,c400) ),
inference(resolution,[status(thm)],[d6,c29]) ).
cnf(d8,plain,
~ sub(c400,'name$u1$u1'),
inference(resolution,[status(thm)],[c25,d7]) ).
cnf(d9,plain,
$false,
inference(resolution,[status(thm)],[c28,d8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR114+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Sun Sep 27 01:05:49 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.88/6.79 % SZS status Theorem for theBenchmark.p
% 18.88/6.79 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------