%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+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 : n016.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:41 AM UTC 2026
% Result : Theorem 72.66s 9.90s
% Output : CNFRefutation 72.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 2
% Syntax : Number of formulae : 15 ( 7 unt; 0 def)
% Number of atoms : 233 ( 0 equ)
% Maximal formula atoms : 194 ( 15 avg)
% Number of connectives : 240 ( 22 ~; 15 |; 203 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 194 ( 17 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 19 ( 18 usr; 1 prp; 0-8 aty)
% Number of functors : 55 ( 55 usr; 54 con; 0-2 aty)
% Number of variables : 34 ( 16 sgn 0 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_news_1151_a19984,hypothesis,
( varia('einbau$u$u1$u1','varia$uc')
& refer('einbau$u$u1$u1','refer$uc')
& quant('einbau$u$u1$u1',one)
& gener('einbau$u$u1$u1',ge)
& fact('einbau$u$u1$u1',real)
& etype('einbau$u$u1$u1',int0)
& card('einbau$u$u1$u1',int1)
& sort('einbau$u$u1$u1',ad)
& varia('abschlu$u$u337$u1$u1','varia$uc')
& refer('abschlu$u$u337$u1$u1','refer$uc')
& quant('abschlu$u$u337$u1$u1',one)
& gener('abschlu$u$u337$u1$u1',ge)
& fact('abschlu$u$u337$u1$u1',real)
& etype('abschlu$u$u337$u1$u1',int0)
& card('abschlu$u$u337$u1$u1',int1)
& sort('abschlu$u$u337$u1$u1',io)
& sort('abschlu$u$u337$u1$u1',ad)
& sort('bmw$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(c865,'varia$uc')
& refer(c865,indet)
& quant(c865,one)
& gener(c865,sp)
& fact(c865,real)
& etype(c865,int0)
& card(c865,int1)
& sort(c865,na)
& varia('firma$u1$u1','varia$uc')
& refer('firma$u1$u1','refer$uc')
& quant('firma$u1$u1',one)
& gener('firma$u1$u1',ge)
& fact('firma$u1$u1',real)
& etype('firma$u1$u1',int0)
& card('firma$u1$u1',int1)
& sort('firma$u1$u1',io)
& sort('firma$u1$u1',d)
& varia('absatz$u1$u2','varia$uc')
& refer('absatz$u1$u2','refer$uc')
& quant('absatz$u1$u2',one)
& gener('absatz$u1$u2',ge)
& fact('absatz$u1$u2',real)
& etype('absatz$u1$u2',int0)
& card('absatz$u1$u2',int1)
& sort('absatz$u1$u2',ad)
& varia(c801,con)
& refer(c801,det)
& quant(c801,one)
& gener(c801,sp)
& fact(c801,real)
& etype(c801,int0)
& card(c801,int1)
& sort(c801,io)
& sort(c801,d)
& varia(c791,'varia$uc')
& refer(c791,det)
& quant(c791,one)
& gener(c791,sp)
& fact(c791,real)
& etype(c791,int0)
& card(c791,int1)
& sort(c791,o)
& varia('mitspieler$u1$u1','varia$uc')
& refer('mitspieler$u1$u1','refer$uc')
& quant('mitspieler$u1$u1',one)
& gener('mitspieler$u1$u1',ge)
& fact('mitspieler$u1$u1',real)
& etype('mitspieler$u1$u1',int0)
& card('mitspieler$u1$u1',int1)
& sort('mitspieler$u1$u1',d)
& varia('endmontage$u1$u1','varia$uc')
& refer('endmontage$u1$u1','refer$uc')
& quant('endmontage$u1$u1',one)
& gener('endmontage$u1$u1',ge)
& fact('endmontage$u1$u1',real)
& etype('endmontage$u1$u1',int0)
& card('endmontage$u1$u1',int1)
& sort('endmontage$u1$u1',ad)
& varia('rover$u1$u1','varia$uc')
& refer('rover$u1$u1','refer$uc')
& quant('rover$u1$u1',one)
& gener('rover$u1$u1',ge)
& fact('rover$u1$u1',real)
& etype('rover$u1$u1',int0)
& card('rover$u1$u1',int1)
& sort('rover$u1$u1',d)
& 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)
& card(c758,int15)
& sort(c758,nu)
& varia('kunstturner$u1$u1','varia$uc')
& refer('kunstturner$u1$u1','refer$uc')
& quant('kunstturner$u1$u1',one)
& gener('kunstturner$u1$u1',ge)
& fact('kunstturner$u1$u1',real)
& etype('kunstturner$u1$u1',int0)
& card('kunstturner$u1$u1',int1)
& sort('kunstturner$u1$u1',d)
& varia(c864,con)
& refer(c864,det)
& quant(c864,one)
& gener(c864,sp)
& fact(c864,real)
& etype(c864,int0)
& card(c864,int1)
& sort(c864,io)
& sort(c864,d)
& varia(c797,con)
& refer(c797,det)
& quant(c797,one)
& gener(c797,sp)
& fact(c797,real)
& etype(c797,int0)
& card(c797,int1)
& sort(c797,ad)
& varia(c787,'varia$uc')
& refer(c787,det)
& quant(c787,mult)
& gener(c787,sp)
& fact(c787,real)
& etype(c787,int1)
& card(c787,cons('x$uconstant',cons(int1,nil)))
& sort(c787,d)
& varia(c773,con)
& refer(c773,det)
& quant(c773,one)
& gener(c773,sp)
& fact(c773,real)
& etype(c773,int0)
& card(c773,int1)
& sort(c773,ad)
& varia(c767,'varia$uc')
& refer(c767,'refer$uc')
& quant(c767,one)
& gener(c767,'gener$uc')
& fact(c767,real)
& etype(c767,int0)
& card(c767,int1)
& sort(c767,d)
& varia(c762,'varia$uc')
& refer(c762,'refer$uc')
& quant(c762,'quant$uc')
& gener(c762,'gener$uc')
& fact(c762,real)
& etype(c762,'etype$uc')
& card(c762,'card$uc')
& sort(c762,ta)
& sort(c762,m)
& varia(c753,'varia$uc')
& refer(c753,indet)
& quant(c753,mult)
& gener(c753,'gener$uc')
& fact(c753,real)
& etype(c753,int1)
& card(c753,cons('x$uconstant',cons(int1,nil)))
& sort(c753,d)
& varia(c2495,'varia$uc')
& refer(c2495,'refer$uc')
& quant(c2495,'quant$uc')
& gener(c2495,'gener$uc')
& fact(c2495,real)
& etype(c2495,'etype$uc')
& card(c2495,'card$uc')
& sort(c2495,ent)
& subs('endmontage$u1$u1','einbau$u$u1$u1')
& assoc('endmontage$u1$u1','abschlu$u$u337$u1$u1')
& val(c865,'bmw$u0')
& sub(c865,'name$u1$u1')
& sub(c864,'firma$u1$u1')
& attr(c864,c865)
& sub(c801,'firma$u1$u1')
& subs(c797,'absatz$u1$u2')
& obj(c797,c801)
& attch(c791,c787)
& pred(c787,'mitspieler$u1$u1')
& subs(c773,'endmontage$u1$u1')
& sub(c767,'rover$u1$u1')
& 'quant$up3'(c762,c758,'jahr$u$u1$u1')
& pred(c753,'kunstturner$u1$u1')
& 'tupl$up8'(c2495,c753,c762,c767,c773,c787,c797,c864) ) ).
fof(synth_qa07_007_mira_news_1151_a19984,conjecture,
? [X0,X1,X2,X3,X4,X5] :
( val(X1,'bmw$u0')
& sub(X1,'name$u1$u1')
& sub(X0,'firma$u1$u1')
& obj(X3,X0)
& attr(X4,X5)
& attr(X2,X1) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5] :
( val(X1,'bmw$u0')
& sub(X1,'name$u1$u1')
& sub(X0,'firma$u1$u1')
& obj(X3,X0)
& attr(X4,X5)
& attr(X2,X1) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_007_mira_news_1151_a19984]) ).
cnf(c7,plain,
obj(c797,c801),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1151_a19984]) ).
cnf(c9,plain,
sub(c801,'firma$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1151_a19984]) ).
cnf(c10,plain,
attr(c864,c865),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1151_a19984]) ).
cnf(c12,plain,
sub(c865,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1151_a19984]) ).
cnf(c13,plain,
val(c865,'bmw$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1151_a19984]) ).
cnf(c10565,plain,
( ~ sub(X0,'name$u1$u1')
| ~ sub(X2,'firma$u1$u1')
| ~ attr(X5,X0)
| ~ attr(X3,X4)
| ~ obj(X1,X2)
| ~ val(X0,'bmw$u0') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ attr(X4,c865)
| ~ attr(X2,X3)
| ~ obj(X1,X0)
| ~ sub(c865,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[c13,c10565]) ).
cnf(d1,plain,
( ~ attr(X3,X4)
| ~ attr(X2,c865)
| ~ obj(X1,X0)
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[c12,d0]) ).
cnf(d2,plain,
( ~ attr(X2,X3)
| ~ obj(X1,X0)
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d1,c10]) ).
cnf(d3,plain,
( ~ obj(X1,X0)
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d2,c10]) ).
cnf(d4,plain,
~ sub(c801,'firma$u1$u1'),
inference(resolution,[status(thm)],[d3,c7]) ).
cnf(d5,plain,
$false,
inference(resolution,[status(thm)],[c9,d4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR115+24 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n016.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Sun Sep 27 01:12:45 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.46 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 72.66/9.90 % SZS status Theorem for theBenchmark.p
% 72.66/9.90 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------