%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR114+24 : 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 : n009.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 99.72s 23.18s
% Output : CNFRefutation 99.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 5
% Syntax : Number of formulae : 26 ( 11 unt; 0 def)
% Number of atoms : 339 ( 0 equ)
% Maximal formula atoms : 276 ( 13 avg)
% Number of connectives : 342 ( 29 ~; 23 |; 288 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 276 ( 14 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-13 aty)
% Number of functors : 67 ( 67 usr; 65 con; 0-2 aty)
% Number of variables : 41 ( 4 sgn 8 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_004_qapw_68_a281,hypothesis,
( varia('staette$u1$u1','varia$uc')
& refer('staette$u1$u1','refer$uc')
& quant('staette$u1$u1',one)
& gener('staette$u1$u1',ge)
& fact('staette$u1$u1',real)
& etype('staette$u1$u1',int0)
& card('staette$u1$u1',int1)
& sort('staette$u1$u1',d)
& varia('sport$u$u1$u1','varia$uc')
& refer('sport$u$u1$u1','refer$uc')
& quant('sport$u$u1$u1',one)
& gener('sport$u$u1$u1',ge)
& fact('sport$u$u1$u1',real)
& etype('sport$u$u1$u1',int0)
& card('sport$u$u1$u1',int1)
& sort('sport$u$u1$u1',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)
& varia(c49957,'varia$uc')
& refer(c49957,det)
& quant(c49957,one)
& gener(c49957,sp)
& fact(c49957,real)
& etype(c49957,int0)
& card(c49957,int1)
& sort(c49957,o)
& varia(c50158,'varia$uc')
& refer(c50158,'refer$uc')
& quant(c50158,'quant$uc')
& gener(c50158,'gener$uc')
& fact(c50158,real)
& etype(c50158,'etype$uc')
& card(c50158,'card$uc')
& sort(c50158,ent)
& varia('einander$u1$u1','varia$uc')
& refer('einander$u1$u1','refer$uc')
& quant('einander$u1$u1',mult)
& gener('einander$u1$u1','gener$uc')
& fact('einander$u1$u1',real)
& etype('einander$u1$u1',int1)
& card('einander$u1$u1',cons('x$uconstant',cons(int1,nil)))
& sort('einander$u1$u1',o)
& varia(c49977,'varia$uc')
& refer(c49977,'refer$uc')
& quant(c49977,mult)
& gener(c49977,'gener$uc')
& fact(c49977,real)
& etype(c49977,int1)
& card(c49977,cons('x$uconstant',cons(int1,nil)))
& sort(c49977,o)
& varia('gladiator$u1$u1','varia$uc')
& refer('gladiator$u1$u1','refer$uc')
& quant('gladiator$u1$u1',one)
& gener('gladiator$u1$u1',ge)
& fact('gladiator$u1$u1',real)
& etype('gladiator$u1$u1',int0)
& card('gladiator$u1$u1',int1)
& sort('gladiator$u1$u1',d)
& varia(c49974,'varia$uc')
& refer(c49974,indet)
& quant(c49974,mult)
& gener(c49974,'gener$uc')
& fact(c49974,real)
& etype(c49974,int1)
& card(c49974,cons('x$uconstant',cons(int1,nil)))
& sort(c49974,d)
& varia(c49955,'varia$uc')
& refer(c49955,indet)
& quant(c49955,one)
& gener(c49955,sp)
& fact(c49955,real)
& etype(c49955,int0)
& card(c49955,int1)
& sort(c49955,na)
& varia(c49954,con)
& refer(c49954,det)
& quant(c49954,one)
& gener(c49954,sp)
& fact(c49954,real)
& etype(c49954,int0)
& card(c49954,int1)
& sort(c49954,io)
& sort(c49954,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(c49948,con)
& refer(c49948,det)
& quant(c49948,one)
& gener(c49948,sp)
& fact(c49948,real)
& etype(c49948,int0)
& card(c49948,int1)
& sort(c49948,d)
& varia('gladiatorenkampf$u1$u1','varia$uc')
& refer('gladiatorenkampf$u1$u1','refer$uc')
& quant('gladiatorenkampf$u1$u1',one)
& gener('gladiatorenkampf$u1$u1',ge)
& fact('gladiatorenkampf$u1$u1',real)
& etype('gladiatorenkampf$u1$u1',int0)
& card('gladiatorenkampf$u1$u1',int1)
& sort('gladiatorenkampf$u1$u1',ad)
& varia(c49933,'varia$uc')
& refer(c49933,indet)
& quant(c49933,mult)
& gener(c49933,'gener$uc')
& fact(c49933,real)
& etype(c49933,int1)
& card(c49933,cons('x$uconstant',cons(int1,nil)))
& sort(c49933,ad)
& varia('wagenrennen$u1$u1','varia$uc')
& refer('wagenrennen$u1$u1','refer$uc')
& quant('wagenrennen$u1$u1',one)
& gener('wagenrennen$u1$u1',ge)
& fact('wagenrennen$u1$u1',real)
& etype('wagenrennen$u1$u1',int0)
& card('wagenrennen$u1$u1',int1)
& sort('wagenrennen$u1$u1',o)
& varia(c49930,'varia$uc')
& refer(c49930,indet)
& quant(c49930,mult)
& gener(c49930,'gener$uc')
& fact(c49930,real)
& etype(c49930,int1)
& card(c49930,cons('x$uconstant',cons(int1,nil)))
& sort(c49930,o)
& 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(c49926,'varia$uc')
& refer(c49926,indet)
& quant(c49926,one)
& gener(c49926,sp)
& fact(c49926,real)
& etype(c49926,int0)
& card(c49926,int1)
& sort(c49926,na)
& varia(c49925,con)
& refer(c49925,det)
& quant(c49925,one)
& gener(c49925,sp)
& fact(c49925,real)
& etype(c49925,int0)
& card(c49925,int1)
& sort(c49925,io)
& sort(c49925,d)
& varia('maximus$u1$u1','varia$uc')
& refer('maximus$u1$u1','refer$uc')
& quant('maximus$u1$u1',one)
& gener('maximus$u1$u1',ge)
& fact('maximus$u1$u1',real)
& etype('maximus$u1$u1',int0)
& card('maximus$u1$u1',int1)
& sort('maximus$u1$u1',o)
& varia(c49918,'varia$uc')
& refer(c49918,'refer$uc')
& quant(c49918,one)
& gener(c49918,'gener$uc')
& fact(c49918,real)
& etype(c49918,int0)
& card(c49918,int1)
& sort(c49918,o)
& varia('circus$u1$u1','varia$uc')
& refer('circus$u1$u1','refer$uc')
& quant('circus$u1$u1',one)
& gener('circus$u1$u1',ge)
& fact('circus$u1$u1',real)
& etype('circus$u1$u1',int0)
& card('circus$u1$u1',int1)
& sort('circus$u1$u1',o)
& varia(c49915,con)
& refer(c49915,det)
& quant(c49915,one)
& gener(c49915,sp)
& fact(c49915,real)
& etype(c49915,int0)
& card(c49915,int1)
& sort(c49915,o)
& varia('reich$u1$u1','varia$uc')
& refer('reich$u1$u1','refer$uc')
& quant('reich$u1$u1',one)
& gener('reich$u1$u1',ge)
& fact('reich$u1$u1',real)
& etype('reich$u1$u1',int0)
& card('reich$u1$u1',int1)
& sort('reich$u1$u1',io)
& sort('reich$u1$u1',d)
& sort('r$u$u366misch$u$u1$u1',tq)
& varia(c49905,con)
& refer(c49905,det)
& quant(c49905,one)
& gener(c49905,sp)
& fact(c49905,real)
& etype(c49905,int0)
& card(c49905,int1)
& sort(c49905,io)
& sort(c49905,d)
& varia(c49903,'varia$uc')
& refer(c49903,'refer$uc')
& quant(c49903,'quant$uc')
& gener(c49903,'gener$uc')
& fact(c49903,real)
& etype(c49903,int2)
& etype(c49903,int1)
& card(c49903,'card$uc')
& sort(c49903,o)
& sort('bekannt$u1$u1',nq)
& sort(c49902,tq)
& varia('sportort$u1$u1','varia$uc')
& refer('sportort$u1$u1','refer$uc')
& quant('sportort$u1$u1',one)
& gener('sportort$u1$u1',ge)
& fact('sportort$u1$u1',real)
& etype('sportort$u1$u1',int0)
& card('sportort$u1$u1',int1)
& sort('sportort$u1$u1',d)
& varia(c49899,con)
& refer(c49899,det)
& quant(c49899,mult)
& gener(c49899,sp)
& fact(c49899,real)
& etype(c49899,int1)
& card(c49899,cons('x$uconstant',cons(int1,nil)))
& sort(c49899,d)
& sub('sportort$u1$u1','staette$u1$u1')
& assoc('sportort$u1$u1','sport$u$u1$u1')
& subs('gladiatorenkampf$u1$u1','gefecht$u1$u1')
& assoc('gladiatorenkampf$u1$u1','gladiator$u1$u1')
& 'tupl$up13'(c50158,c49899,c49902,c49915,c49918,c49925,c49930,c49933,c49948,c49954,c49957,c49974,c49977)
& sub(c49977,'einander$u1$u1')
& pred(c49974,'gladiator$u1$u1')
& val(c49955,'rom$u0')
& sub(c49955,'name$u1$u1')
& sub(c49954,'stadt$u$u1$u1')
& attr(c49954,c49955)
& sub(c49948,'kolosseum$u1$u1')
& preds(c49933,'gladiatorenkampf$u1$u1')
& pred(c49930,'wagenrennen$u1$u1')
& val(c49926,'rom$u0')
& sub(c49926,'name$u1$u1')
& sub(c49925,'stadt$u$u1$u1')
& attr(c49925,c49926)
& sub(c49918,'maximus$u1$u1')
& sub(c49915,'circus$u1$u1')
& sub(c49905,'reich$u1$u1')
& prop(c49905,'r$u$u366misch$u$u1$u1')
& attch(c49905,c49899)
& supl(c49902,'bekannt$u1$u1',c49903)
& prop(c49899,c49902)
& pred(c49899,'sportort$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(synth_qa07_004_qapw_68_a281,conjecture,
? [X0,X1,X2,X3] :
( val(X1,'rom$u0')
& sub(X0,'stadt$u$u1$u1')
& sub(X1,'name$u1$u1')
& scar(X3,X2)
& attr(X0,X1) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3] :
( val(X1,'rom$u0')
& sub(X0,'stadt$u$u1$u1')
& sub(X1,'name$u1$u1')
& scar(X3,X2)
& attr(X0,X1) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_004_qapw_68_a281]) ).
cnf(c4,plain,
attr(c49925,c49926),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_68_a281]) ).
cnf(c5,plain,
sub(c49926,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_68_a281]) ).
cnf(c8,plain,
sub(c49954,'stadt$u$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_68_a281]) ).
cnf(c9,plain,
val(c49955,'rom$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_68_a281]) ).
cnf(c267,plain,
sub(c49955,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_68_a281]) ).
cnf(c268,plain,
attr(c49954,c49955),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_004_qapw_68_a281]) ).
cnf(c276,plain,
member(X0,cons(X0,X1)),
inference(clausification,[status(esa)],[member_first]) ).
cnf(c277,plain,
( member(X0,cons(X2,X1))
| ~ member(X0,X1) ),
inference(clausification,[status(esa)],[member_second]) ).
cnf(c486,plain,
( scar(sK276(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(c580,plain,
( ~ val(X1,'rom$u0')
| ~ scar(X2,X3)
| ~ attr(X0,X1)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'stadt$u$u1$u1') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ member(X1,cons('familiename$u1$u1',cons('name$u1$u1',nil)))
| scar(sK276(X2),X2)
| ~ attr(X2,X0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[c486,c277]) ).
cnf(d1,plain,
( ~ member(X1,cons('name$u1$u1',nil))
| scar(sK276(X2),X2)
| ~ attr(X2,X0)
| ~ sub(X0,X1) ),
inference(resolution,[status(thm)],[d0,c277]) ).
cnf(d2,plain,
( scar(sK276(X1),X1)
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d1,c276]) ).
cnf(d3,plain,
( scar(sK276(c49925),c49925)
| ~ sub(c49926,'name$u1$u1') ),
inference(resolution,[status(thm)],[d2,c4]) ).
cnf(d4,plain,
scar(sK276(c49925),c49925),
inference(resolution,[status(thm)],[c5,d3]) ).
cnf(d5,plain,
( ~ val(X1,'rom$u0')
| ~ attr(X0,X1)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'stadt$u$u1$u1') ),
inference(resolution,[status(thm)],[d4,c580]) ).
cnf(d6,plain,
( ~ attr(X0,c49955)
| ~ sub(X0,'stadt$u$u1$u1')
| ~ sub(c49955,'name$u1$u1') ),
inference(resolution,[status(thm)],[d5,c9]) ).
cnf(d7,plain,
( ~ attr(X0,c49955)
| ~ sub(X0,'stadt$u$u1$u1') ),
inference(resolution,[status(thm)],[c267,d6]) ).
cnf(d8,plain,
~ sub(c49954,'stadt$u$u1$u1'),
inference(resolution,[status(thm)],[d7,c268]) ).
cnf(d9,plain,
$false,
inference(resolution,[status(thm)],[c8,d8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR114+24 : 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.37 % Computer : n009.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Sun Sep 27 01:06:04 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 99.72/23.18 % SZS status Theorem for theBenchmark.p
% 99.72/23.18 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------