%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+91 : 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 : n015.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:50 AM UTC 2026
% Result : Theorem 66.37s 8.86s
% Output : CNFRefutation 66.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 4
% Syntax : Number of formulae : 25 ( 11 unt; 0 def)
% Number of atoms : 473 ( 0 equ)
% Maximal formula atoms : 391 ( 18 avg)
% Number of connectives : 498 ( 50 ~; 39 |; 408 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 391 ( 20 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 19 ( 18 usr; 1 prp; 0-20 aty)
% Number of functors : 86 ( 86 usr; 84 con; 0-2 aty)
% Number of variables : 64 ( 33 sgn 3 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_wp_529,hypothesis,
( varia('fahrzeug$u$u1$u1','varia$uc')
& refer('fahrzeug$u$u1$u1','refer$uc')
& quant('fahrzeug$u$u1$u1',one)
& gener('fahrzeug$u$u1$u1',ge)
& fact('fahrzeug$u$u1$u1',real)
& etype('fahrzeug$u$u1$u1',int0)
& card('fahrzeug$u$u1$u1',int1)
& sort('fahrzeug$u$u1$u1',d)
& varia('luxus$u$u1$u1','varia$uc')
& refer('luxus$u$u1$u1','refer$uc')
& quant('luxus$u$u1$u1',one)
& gener('luxus$u$u1$u1',ge)
& fact('luxus$u$u1$u1',real)
& etype('luxus$u$u1$u1',int0)
& card('luxus$u$u1$u1',int1)
& sort('luxus$u$u1$u1',io)
& varia(c50663,'varia$uc')
& refer(c50663,'refer$uc')
& quant(c50663,'quant$uc')
& gener(c50663,'gener$uc')
& fact(c50663,real)
& etype(c50663,'etype$uc')
& card(c50663,'card$uc')
& sort(c50663,ent)
& sort('v8$u0',fe)
& varia('erzeugnis$u1$u1','varia$uc')
& refer('erzeugnis$u1$u1','refer$uc')
& quant('erzeugnis$u1$u1','quant$uc')
& gener('erzeugnis$u1$u1',ge)
& fact('erzeugnis$u1$u1',real)
& etype('erzeugnis$u1$u1','etype$uc')
& card('erzeugnis$u1$u1','card$uc')
& sort('erzeugnis$u1$u1',co)
& varia(c47513,'varia$uc')
& refer(c47513,indet)
& quant(c47513,one)
& gener(c47513,sp)
& fact(c47513,real)
& etype(c47513,int0)
& card(c47513,int1)
& sort(c47513,na)
& varia(c47512,con)
& refer(c47512,det)
& quant(c47512,'quant$uc')
& gener(c47512,sp)
& fact(c47512,real)
& etype(c47512,'etype$uc')
& card(c47512,'card$uc')
& sort(c47512,co)
& sort('bmw$u0',fe)
& varia(c47503,'varia$uc')
& refer(c47503,indet)
& quant(c47503,one)
& gener(c47503,sp)
& fact(c47503,real)
& etype(c47503,int0)
& card(c47503,int1)
& sort(c47503,na)
& varia(c47502,con)
& refer(c47502,det)
& quant(c47502,one)
& gener(c47502,sp)
& fact(c47502,real)
& etype(c47502,int0)
& card(c47502,int1)
& sort(c47502,io)
& sort(c47502,d)
& varia('abzeichen$u1$u1','varia$uc')
& refer('abzeichen$u1$u1','refer$uc')
& quant('abzeichen$u1$u1',one)
& gener('abzeichen$u1$u1',ge)
& fact('abzeichen$u1$u1',real)
& etype('abzeichen$u1$u1',int0)
& card('abzeichen$u1$u1',int1)
& sort('abzeichen$u1$u1',d)
& varia(c47485,'varia$uc')
& refer(c47485,'refer$uc')
& quant(c47485,one)
& gener(c47485,'gener$uc')
& fact(c47485,real)
& etype(c47485,int0)
& card(c47485,int1)
& sort(c47485,d)
& varia('propeller$u1$u1','varia$uc')
& refer('propeller$u1$u1','refer$uc')
& quant('propeller$u1$u1',one)
& gener('propeller$u1$u1',ge)
& fact('propeller$u1$u1',real)
& etype('propeller$u1$u1',int0)
& card('propeller$u1$u1',int1)
& sort('propeller$u1$u1',d)
& varia(c47482,con)
& refer(c47482,det)
& quant(c47482,one)
& gener(c47482,sp)
& fact(c47482,real)
& etype(c47482,int0)
& card(c47482,int1)
& sort(c47482,d)
& varia('zeit$u1$u1','varia$uc')
& refer('zeit$u1$u1','refer$uc')
& quant('zeit$u1$u1',one)
& gener('zeit$u1$u1',ge)
& fact('zeit$u1$u1',real)
& etype('zeit$u1$u1',int0)
& card('zeit$u1$u1',int1)
& sort('zeit$u1$u1',ta)
& varia(c47476,'varia$uc')
& refer(c47476,'refer$uc')
& quant(c47476,one)
& gener(c47476,'gener$uc')
& fact(c47476,real)
& etype(c47476,int0)
& card(c47476,int1)
& sort(c47476,ta)
& varia(c47465,'varia$uc')
& refer(c47465,'refer$uc')
& quant(c47465,one)
& gener(c47465,'gener$uc')
& fact(c47465,real)
& etype(c47465,int0)
& card(c47465,int1)
& sort(c47465,ad)
& varia('ehe$u2$u1','varia$uc')
& refer('ehe$u2$u1','refer$uc')
& quant('ehe$u2$u1',one)
& gener('ehe$u2$u1',ge)
& fact('ehe$u2$u1',real)
& etype('ehe$u2$u1',int0)
& card('ehe$u2$u1',int1)
& sort('ehe$u2$u1',re)
& sort('ehe$u2$u1',as)
& varia(c47452,con)
& refer(c47452,det)
& quant(c47452,one)
& gener(c47452,sp)
& fact(c47452,real)
& etype(c47452,int0)
& card(c47452,int1)
& sort(c47452,re)
& sort(c47452,as)
& sort('luxuri$u$u366s$u1$u1',nq)
& varia('v8er$u1$u1','varia$uc')
& refer('v8er$u1$u1','refer$uc')
& quant('v8er$u1$u1',one)
& gener('v8er$u1$u1',ge)
& fact('v8er$u1$u1',real)
& etype('v8er$u1$u1',int0)
& card('v8er$u1$u1',int1)
& sort('v8er$u1$u1',o)
& varia(c47416,'varia$uc')
& refer(c47416,'refer$uc')
& quant(c47416,mult)
& gener(c47416,'gener$uc')
& fact(c47416,real)
& etype(c47416,int1)
& card(c47416,cons('x$uconstant',cons(int1,nil)))
& sort(c47416,o)
& sort('dingolfing$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(c47407,'varia$uc')
& refer(c47407,indet)
& quant(c47407,one)
& gener(c47407,sp)
& fact(c47407,real)
& etype(c47407,int0)
& card(c47407,int1)
& sort(c47407,na)
& varia(c47406,con)
& refer(c47406,det)
& quant(c47406,one)
& gener(c47406,sp)
& fact(c47406,real)
& etype(c47406,int0)
& card(c47406,int1)
& sort(c47406,io)
& sort(c47406,d)
& varia('glas$u1$u1','varia$uc')
& refer('glas$u1$u1','refer$uc')
& quant('glas$u1$u1',one)
& gener('glas$u1$u1',ge)
& fact('glas$u1$u1',real)
& etype('glas$u1$u1',int0)
& card('glas$u1$u1',int1)
& sort('glas$u1$u1',s)
& varia(c47399,'varia$uc')
& refer(c47399,'refer$uc')
& quant(c47399,one)
& gener(c47399,'gener$uc')
& fact(c47399,real)
& etype(c47399,int0)
& card(c47399,int1)
& sort(c47399,s)
& 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(c47395,con)
& refer(c47395,det)
& quant(c47395,one)
& gener(c47395,sp)
& fact(c47395,real)
& etype(c47395,int0)
& card(c47395,int1)
& sort(c47395,io)
& sort(c47395,d)
& varia('annahme$u1$u1','varia$uc')
& refer('annahme$u1$u1','refer$uc')
& quant('annahme$u1$u1',one)
& gener('annahme$u1$u1',ge)
& fact('annahme$u1$u1',real)
& etype('annahme$u1$u1',int0)
& card('annahme$u1$u1',int1)
& sort('annahme$u1$u1',ad)
& varia(c47391,con)
& refer(c47391,det)
& quant(c47391,one)
& gener(c47391,sp)
& fact(c47391,real)
& etype(c47391,int0)
& card(c47391,int1)
& sort(c47391,ad)
& sort('n1960er$u1$u1',gq)
& 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)
& varia(c47385,con)
& refer(c47385,det)
& quant(c47385,'quant$uc')
& gener(c47385,sp)
& fact(c47385,real)
& etype(c47385,'etype$uc')
& card(c47385,'card$uc')
& sort(c47385,ta)
& sort(c47385,oa)
& sort(c47385,me)
& varia(c47379,con)
& refer(c47379,det)
& quant(c47379,one)
& gener(c47379,sp)
& fact(c47379,real)
& etype(c47379,int0)
& card(c47379,int1)
& sort(c47379,io)
& sort(c47379,ad)
& varia('inter$umezzo$u1$u1','varia$uc')
& refer('inter$umezzo$u1$u1','refer$uc')
& quant('inter$umezzo$u1$u1',one)
& gener('inter$umezzo$u1$u1',ge)
& fact('inter$umezzo$u1$u1',real)
& etype('inter$umezzo$u1$u1',int0)
& card('inter$umezzo$u1$u1',int1)
& sort('inter$umezzo$u1$u1',o)
& sort('kurz$u1$u1',mq)
& varia(c47374,con)
& refer(c47374,det)
& quant(c47374,one)
& gener(c47374,sp)
& fact(c47374,real)
& etype(c47374,int0)
& card(c47374,int1)
& sort(c47374,o)
& 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)
& varia(c47366,'varia$uc')
& refer(c47366,'refer$uc')
& quant(c47366,one)
& gener(c47366,'gener$uc')
& fact(c47366,real)
& etype(c47366,int0)
& card(c47366,int1)
& sort(c47366,io)
& sort(c47366,ad)
& varia('bmw$u1$u1','varia$uc')
& refer('bmw$u1$u1','refer$uc')
& quant('bmw$u1$u1',one)
& gener('bmw$u1$u1',ge)
& fact('bmw$u1$u1',real)
& etype('bmw$u1$u1',int0)
& card('bmw$u1$u1',int1)
& sort('bmw$u1$u1',d)
& varia(c47360,'varia$uc')
& refer(c47360,'refer$uc')
& quant(c47360,one)
& gener(c47360,'gener$uc')
& fact(c47360,real)
& etype(c47360,int0)
& card(c47360,int1)
& sort(c47360,d)
& varia('luxusfahrzeug$u1$u1','varia$uc')
& refer('luxusfahrzeug$u1$u1','refer$uc')
& quant('luxusfahrzeug$u1$u1',one)
& gener('luxusfahrzeug$u1$u1',ge)
& fact('luxusfahrzeug$u1$u1',real)
& etype('luxusfahrzeug$u1$u1',int0)
& card('luxusfahrzeug$u1$u1',int1)
& sort('luxusfahrzeug$u1$u1',d)
& varia(c47356,con)
& refer(c47356,det)
& quant(c47356,mult)
& gener(c47356,sp)
& fact(c47356,real)
& etype(c47356,int1)
& card(c47356,cons('x$uconstant',cons(int1,nil)))
& sort(c47356,d)
& varia('aera$u1$u1','varia$uc')
& refer('aera$u1$u1','refer$uc')
& quant('aera$u1$u1',one)
& gener('aera$u1$u1',ge)
& fact('aera$u1$u1',real)
& etype('aera$u1$u1',int0)
& card('aera$u1$u1',int1)
& sort('aera$u1$u1',ta)
& varia(c47352,con)
& refer(c47352,det)
& quant(c47352,one)
& gener(c47352,sp)
& fact(c47352,real)
& etype(c47352,int0)
& card(c47352,int1)
& sort(c47352,ta)
& sub('luxusfahrzeug$u1$u1','fahrzeug$u$u1$u1')
& assoc('luxusfahrzeug$u1$u1','luxus$u$u1$u1')
& 'tupl$up20'(c50663,c47352,c47356,c47360,c47366,c47374,c47379,c47385,c47391,c47395,c47399,c47406,c47416,c47452,c47465,c47476,c47482,c47485,c47502,c47512)
& val(c47513,'v8$u0')
& sub(c47513,'name$u1$u1')
& sub(c47512,'erzeugnis$u1$u1')
& attr(c47512,c47513)
& val(c47503,'bmw$u0')
& sub(c47503,'name$u1$u1')
& sub(c47502,'firma$u1$u1')
& attr(c47502,c47503)
& sub(c47485,'abzeichen$u1$u1')
& sub(c47482,'propeller$u1$u1')
& sub(c47476,'zeit$u1$u1')
& prop(c47476,'kurz$u1$u1')
& subs(c47465,'annahme$u1$u1')
& subr(c47452,'ehe$u2$u1')
& prop(c47416,'luxuri$u$u366s$u1$u1')
& pred(c47416,'v8er$u1$u1')
& val(c47407,'dingolfing$u0')
& sub(c47407,'name$u1$u1')
& sub(c47406,'stadt$u$u1$u1')
& attr(c47406,c47407)
& sub(c47399,'glas$u1$u1')
& sub(c47395,'firma$u1$u1')
& subs(c47391,'annahme$u1$u1')
& prop(c47385,'n1960er$u1$u1')
& pred(c47385,'jahr$u$u1$u1')
& sub(c47379,'abschlu$u$u337$u1$u1')
& sub(c47374,'inter$umezzo$u1$u1')
& prop(c47374,'kurz$u1$u1')
& sub(c47366,'abschlu$u$u337$u1$u1')
& sub(c47360,'bmw$u1$u1')
& pred(c47356,'luxusfahrzeug$u1$u1')
& sub(c47352,'aera$u1$u1') ) ).
fof(chea_subs_abs__event,axiom,
! [X0,X1,X2] :
( ( subs(X0,X1)
& chea(X2,X1) )
=> ? [X3] :
( subs(X3,X2)
& chea(X3,X0) ) ) ).
fof(fact_8354,axiom,
chea('n374bernehmen$u1$u1','annahme$u1$u1') ).
fof(synth_qa07_007_mira_wp_529,conjecture,
? [X0,X1,X2,X3,X4,X5,X6] :
( val(X2,'bmw$u0')
& val(X1,'bmw$u0')
& subs(X4,'n374bernehmen$u1$u1')
& sub(X2,'name$u1$u1')
& sub(X0,'firma$u1$u1')
& sub(X1,'name$u1$u1')
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6] :
( val(X2,'bmw$u0')
& val(X1,'bmw$u0')
& subs(X4,'n374bernehmen$u1$u1')
& sub(X2,'name$u1$u1')
& sub(X0,'firma$u1$u1')
& sub(X1,'name$u1$u1')
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_007_mira_wp_529]) ).
cnf(c9,plain,
subs(c47391,'annahme$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_529]) ).
cnf(c12,plain,
attr(c47406,c47407),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_529]) ).
cnf(c24,plain,
attr(c47502,c47503),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_529]) ).
cnf(c25,plain,
sub(c47502,'firma$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_529]) ).
cnf(c26,plain,
sub(c47503,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_529]) ).
cnf(c27,plain,
val(c47503,'bmw$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_529]) ).
cnf(c477,plain,
( subs(sK99(X2,X0),X0)
| ~ subs(X2,X1)
| ~ chea(X0,X1) ),
inference(clausification,[status(esa)],[chea_subs_abs__event]) ).
cnf(c574,plain,
chea('n374bernehmen$u1$u1','annahme$u1$u1'),
inference(clausification,[status(esa)],[fact_8354]) ).
cnf(c588,plain,
( ~ sub(X2,'name$u1$u1')
| ~ sub(X4,'name$u1$u1')
| ~ attr(X0,X4)
| ~ attr(X5,X6)
| ~ val(X2,'bmw$u0')
| ~ val(X4,'bmw$u0')
| ~ subs(X3,'n374bernehmen$u1$u1')
| ~ attr(X1,X2)
| ~ sub(X0,'firma$u1$u1') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( subs(sK99(X0,'n374bernehmen$u1$u1'),'n374bernehmen$u1$u1')
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[c477,c574]) ).
cnf(d1,plain,
( ~ val(X1,'bmw$u0')
| ~ attr(X5,c47503)
| ~ attr(X0,X1)
| ~ attr(X3,X4)
| ~ subs(X2,'n374bernehmen$u1$u1')
| ~ sub(c47503,'name$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[c27,c588]) ).
cnf(d2,plain,
( ~ val(X0,'bmw$u0')
| ~ attr(X1,X0)
| ~ attr(X4,X5)
| ~ attr(X3,c47503)
| ~ subs(X2,'n374bernehmen$u1$u1')
| ~ sub(X1,'firma$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[c26,d1]) ).
cnf(d3,plain,
( ~ attr(X0,c47503)
| ~ attr(X4,c47503)
| ~ attr(X2,X3)
| ~ subs(X1,'n374bernehmen$u1$u1')
| ~ sub(c47503,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d2,c27]) ).
cnf(d4,plain,
( ~ attr(X0,c47503)
| ~ attr(X3,X4)
| ~ attr(X2,c47503)
| ~ subs(X1,'n374bernehmen$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[c26,d3]) ).
cnf(d5,plain,
( ~ attr(X3,c47503)
| ~ attr(X1,X2)
| ~ subs(X0,'n374bernehmen$u1$u1')
| ~ sub(c47502,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d4,c24]) ).
cnf(d6,plain,
( ~ attr(X2,X3)
| ~ attr(X1,c47503)
| ~ subs(X0,'n374bernehmen$u1$u1') ),
inference(resolution,[status(thm)],[c25,d5]) ).
cnf(d7,plain,
( ~ attr(X1,X2)
| ~ subs(X0,'n374bernehmen$u1$u1') ),
inference(resolution,[status(thm)],[d6,c24]) ).
cnf(d8,plain,
~ subs(X0,'n374bernehmen$u1$u1'),
inference(resolution,[status(thm)],[d7,c12]) ).
cnf(d9,plain,
~ subs(X0,'annahme$u1$u1'),
inference(resolution,[status(thm)],[d8,d0]) ).
cnf(d10,plain,
$false,
inference(resolution,[status(thm)],[d9,c9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+91 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n015.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 01:16:15 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 66.37/8.86 % SZS status Theorem for theBenchmark.p
% 66.37/8.86 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------