%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+7 : 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:48 AM UTC 2026
% Result : Theorem 20.04s 14.11s
% Output : CNFRefutation 20.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 5
% Syntax : Number of formulae : 28 ( 9 unt; 0 def)
% Number of atoms : 353 ( 0 equ)
% Maximal formula atoms : 259 ( 12 avg)
% Number of connectives : 381 ( 56 ~; 46 |; 277 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 259 ( 14 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-3 aty)
% Number of functors : 68 ( 68 usr; 67 con; 0-2 aty)
% Number of variables : 58 ( 4 sgn 6 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_news_1097,hypothesis,
( varia(c34,'varia$uc')
& refer(c34,'refer$uc')
& quant(c34,'quant$uc')
& gener(c34,'gener$uc')
& fact(c34,real)
& etype(c34,'etype$uc')
& card(c34,'card$uc')
& sort(c34,ent)
& varia('feb$u1$u1','varia$uc')
& refer('feb$u1$u1','refer$uc')
& quant('feb$u1$u1',one)
& gener('feb$u1$u1',ge)
& fact('feb$u1$u1',real)
& etype('feb$u1$u1',int0)
& card('feb$u1$u1',int1)
& sort('feb$u1$u1',o)
& varia(c21,'varia$uc')
& refer(c21,'refer$uc')
& quant(c21,one)
& gener(c21,'gener$uc')
& fact(c21,real)
& etype(c21,int0)
& card(c21,int1)
& sort(c21,o)
& gener('hundertstel$u$u1$u1',ge)
& sort('hundertstel$u$u1$u1',me)
& card(c2013,int20)
& sort(c2013,nu)
& gener('abziehen$u1$u2',ge)
& fact('abziehen$u1$u2',real)
& sort('abziehen$u1$u2',da)
& gener('wollen$u0','gener$uc')
& fact('wollen$u0',real)
& sort('wollen$u0',md)
& varia('anteil$u1$u1','varia$uc')
& refer('anteil$u1$u1','refer$uc')
& quant('anteil$u1$u1','quant$uc')
& gener('anteil$u1$u1',ge)
& fact('anteil$u1$u1',real)
& etype('anteil$u1$u1','etype$uc')
& card('anteil$u1$u1','card$uc')
& sort('anteil$u1$u1',co)
& varia(c2036,con)
& refer(c2036,'refer$uc')
& quant(c2036,'quant$uc')
& gener(c2036,'gener$uc')
& fact(c2036,real)
& etype(c2036,'etype$uc')
& card(c2036,'card$uc')
& sort(c2036,co)
& sort('bmw$u0',fe)
& sort('bundesdeutsch$u1$u1',tq)
& varia(c2007,'varia$uc')
& refer(c2007,indet)
& quant(c2007,one)
& gener(c2007,sp)
& fact(c2007,real)
& etype(c2007,int0)
& card(c2007,int1)
& sort(c2007,na)
& sort('rover$u0',fe)
& 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)
& sort('britisch$u$u1$u1',nq)
& varia(c1913,'varia$uc')
& refer(c1913,indet)
& quant(c1913,one)
& gener(c1913,sp)
& fact(c1913,real)
& etype(c1913,int0)
& card(c1913,int1)
& sort(c1913,na)
& sort('tokio$u0',fe)
& 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(c19,'varia$uc')
& refer(c19,indet)
& quant(c19,one)
& gener(c19,sp)
& fact(c19,real)
& etype(c19,int0)
& card(c19,int1)
& sort(c19,na)
& varia(c18,con)
& refer(c18,det)
& quant(c18,one)
& gener(c18,sp)
& fact(c18,real)
& etype(c18,int0)
& card(c18,int1)
& sort(c18,io)
& sort(c18,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(c1912,con)
& refer(c1912,det)
& quant(c1912,one)
& gener(c1912,sp)
& fact(c1912,real)
& etype(c1912,int0)
& card(c1912,int1)
& sort(c1912,io)
& sort(c1912,d)
& gener(c2016,sp)
& fact(c2016,real)
& sort(c2016,da)
& varia(c2006,con)
& refer(c2006,det)
& quant(c2006,one)
& gener(c2006,sp)
& fact(c2006,real)
& etype(c2006,int0)
& card(c2006,int1)
& sort(c2006,io)
& sort(c2006,d)
& varia(c1730,con)
& refer(c1730,det)
& quant(c1730,one)
& gener(c1730,sp)
& fact(c1730,real)
& etype(c1730,int0)
& card(c1730,int1)
& sort(c1730,ad)
& sort('honda$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)
& sort('japanisch$u$u1$u1',nq)
& varia(c2008,'varia$uc')
& refer(c2008,det)
& quant(c2008,'quant$uc')
& gener(c2008,sp)
& fact(c2008,real)
& etype(c2008,'etype$uc')
& card(c2008,'card$uc')
& sort(c2008,co)
& varia(c1725,'varia$uc')
& refer(c1725,indet)
& quant(c1725,one)
& gener(c1725,sp)
& fact(c1725,real)
& etype(c1725,int0)
& card(c1725,int1)
& sort(c1725,na)
& varia(c1724,con)
& refer(c1724,det)
& quant(c1724,one)
& gener(c1724,sp)
& fact(c1724,real)
& etype(c1724,int0)
& card(c1724,int1)
& sort(c1724,io)
& sort(c1724,d)
& varia('firmengruppe$u1$u1','varia$uc')
& refer('firmengruppe$u1$u1','refer$uc')
& quant('firmengruppe$u1$u1',one)
& gener('firmengruppe$u1$u1',ge)
& fact('firmengruppe$u1$u1',real)
& etype('firmengruppe$u1$u1',int0)
& card('firmengruppe$u1$u1',int1)
& sort('firmengruppe$u1$u1',io)
& sort('firmengruppe$u1$u1',d)
& varia('autokonzern$u1$u1','varia$uc')
& refer('autokonzern$u1$u1','refer$uc')
& quant('autokonzern$u1$u1',one)
& gener('autokonzern$u1$u1',ge)
& fact('autokonzern$u1$u1',real)
& etype('autokonzern$u1$u1',int0)
& card('autokonzern$u1$u1',int1)
& sort('autokonzern$u1$u1',io)
& sort('autokonzern$u1$u1',d)
& varia('fabrikant$u1$u1','varia$uc')
& refer('fabrikant$u1$u1','refer$uc')
& quant('fabrikant$u1$u1',one)
& gener('fabrikant$u1$u1',ge)
& fact('fabrikant$u1$u1',real)
& etype('fabrikant$u1$u1',int0)
& card('fabrikant$u1$u1',int1)
& sort('fabrikant$u1$u1',io)
& sort('fabrikant$u1$u1',d)
& varia('auto$u$u1$u1','varia$uc')
& refer('auto$u$u1$u1','refer$uc')
& quant('auto$u$u1$u1',one)
& gener('auto$u$u1$u1',ge)
& fact('auto$u$u1$u1',real)
& etype('auto$u$u1$u1',int0)
& card('auto$u$u1$u1',int1)
& sort('auto$u$u1$u1',d)
& varia('autobauer$u1$u1','varia$uc')
& refer('autobauer$u1$u1','refer$uc')
& quant('autobauer$u1$u1',one)
& gener('autobauer$u1$u1',ge)
& fact('autobauer$u1$u1',real)
& etype('autobauer$u1$u1',int0)
& card('autobauer$u1$u1',int1)
& sort('autobauer$u1$u1',io)
& sort('autobauer$u1$u1',d)
& tupl(c34,c18,c21)
& sub(c21,'feb$u1$u1')
& 'quant$up3'(c2036,c2013,'hundertstel$u$u1$u1')
& subs(c2016,'abziehen$u1$u2')
& obj(c2016,c2008)
& modl(c2016,'wollen$u0')
& agt(c2016,c1724)
& sub(c2008,'anteil$u1$u1')
& attch(c2008,c2036)
& val(c2007,'bmw$u0')
& sub(c2007,'name$u1$u1')
& sub(c2006,'autobauer$u1$u1')
& prop(c2006,'bundesdeutsch$u1$u1')
& attr(c2006,c2007)
& val(c1913,'rover$u0')
& sub(c1913,'name$u1$u1')
& sub(c1912,'firma$u1$u1')
& prop(c1912,'britisch$u$u1$u1')
& attr(c1912,c1913)
& val(c19,'tokio$u0')
& sub(c19,'name$u1$u1')
& sub(c18,'stadt$u$u1$u1')
& attr(c18,c19)
& subs(c1730,'annahme$u1$u1')
& obj(c1730,c1912)
& ante(c1730,c2016)
& agt(c1730,c2006)
& val(c1725,'honda$u0')
& sub(c1725,'name$u1$u1')
& sub(c1724,'autokonzern$u1$u1')
& prop(c1724,'japanisch$u$u1$u1')
& poss(c1724,c2008)
& attr(c1724,c1725)
& sub('autokonzern$u1$u1','firmengruppe$u1$u1')
& assoc('autokonzern$u1$u1','auto$u$u1$u1')
& sub('autobauer$u1$u1','fabrikant$u1$u1')
& assoc('autobauer$u1$u1','auto$u$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(chea_agt_abs__event,axiom,
! [X0,X1,X2] :
( ( chea(X1,X0)
& agt(X0,X2) )
=> agt(X1,X2) ) ).
fof(fact_8354,axiom,
chea('n374bernehmen$u1$u1','annahme$u1$u1') ).
fof(synth_qa07_007_mira_news_1097,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(X1,'name$u1$u1')
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1)
& agt(X4,X3) ) ).
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(X1,'name$u1$u1')
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1)
& agt(X4,X3) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_007_mira_news_1097]) ).
cnf(c10,plain,
agt(c1730,c2006),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1097]) ).
cnf(c13,plain,
subs(c1730,'annahme$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1097]) ).
cnf(c23,plain,
attr(c2006,c2007),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1097]) ).
cnf(c26,plain,
sub(c2007,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1097]) ).
cnf(c27,plain,
val(c2007,'bmw$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1097]) ).
cnf(c319,plain,
( chea(sK78(X2,X0),X2)
| ~ subs(X2,X1)
| ~ chea(X0,X1) ),
inference(clausification,[status(esa)],[chea_subs_abs__event]) ).
cnf(c320,plain,
( subs(sK78(X2,X0),X0)
| ~ subs(X2,X1)
| ~ chea(X0,X1) ),
inference(clausification,[status(esa)],[chea_subs_abs__event]) ).
cnf(c322,plain,
( agt(X2,X1)
| ~ chea(X2,X0)
| ~ agt(X0,X1) ),
inference(clausification,[status(esa)],[chea_agt_abs__event]) ).
cnf(c359,plain,
chea('n374bernehmen$u1$u1','annahme$u1$u1'),
inference(clausification,[status(esa)],[fact_8354]) ).
cnf(c364,plain,
( ~ subs(X1,'n374bernehmen$u1$u1')
| ~ attr(X2,X6)
| ~ sub(X6,'name$u1$u1')
| ~ val(X6,'bmw$u0')
| ~ attr(X4,X5)
| ~ val(X0,'bmw$u0')
| ~ attr(X3,X0)
| ~ agt(X1,X2)
| ~ sub(X0,'name$u1$u1') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( chea(sK78(X0,'n374bernehmen$u1$u1'),X0)
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[c319,c359]) ).
cnf(d1,plain,
( ~ agt(X0,X1)
| agt(sK78(X0,'n374bernehmen$u1$u1'),X1)
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[d0,c322]) ).
cnf(d2,plain,
( ~ subs(X4,'n374bernehmen$u1$u1')
| ~ agt(X4,X2)
| ~ val(X1,'bmw$u0')
| ~ val(X0,'bmw$u0')
| ~ attr(X3,X0)
| ~ attr(X2,X1)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(factoring,[status(thm)],[c364]) ).
cnf(d3,plain,
( ~ subs(X2,'n374bernehmen$u1$u1')
| ~ agt(X2,X1)
| ~ val(X0,'bmw$u0')
| ~ val(X0,'bmw$u0')
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(factoring,[status(thm)],[d2]) ).
cnf(d4,plain,
( subs(sK78(X0,'n374bernehmen$u1$u1'),'n374bernehmen$u1$u1')
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[c320,c359]) ).
cnf(d5,plain,
( ~ agt(sK78(X0,'n374bernehmen$u1$u1'),X2)
| ~ val(X1,'bmw$u0')
| ~ attr(X2,X1)
| ~ sub(X1,'name$u1$u1')
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[d4,d3]) ).
cnf(d6,plain,
( ~ subs(X2,'annahme$u1$u1')
| ~ agt(X2,X1)
| ~ subs(X2,'annahme$u1$u1')
| ~ val(X0,'bmw$u0')
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d5,d1]) ).
cnf(d7,plain,
( ~ agt(c1730,X1)
| ~ val(X0,'bmw$u0')
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d6,c13]) ).
cnf(d8,plain,
( ~ val(X0,'bmw$u0')
| ~ attr(c2006,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d7,c10]) ).
cnf(d9,plain,
( ~ attr(c2006,c2007)
| ~ sub(c2007,'name$u1$u1') ),
inference(resolution,[status(thm)],[d8,c27]) ).
cnf(d10,plain,
~ sub(c2007,'name$u1$u1'),
inference(resolution,[status(thm)],[c23,d9]) ).
cnf(d11,plain,
$false,
inference(resolution,[status(thm)],[c26,d10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : CSR115+7 : 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.03/5.32 % Computer : n012.cluster.edu
% 0.03/5.32 % Model : x86_64 x86_64
% 0.03/5.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/5.32 % Memory : 8046.5625MB
% 0.03/5.32 % OS : Linux 6.8.0-71-generic
% 0.03/5.32 % CPULimit : 300
% 0.03/5.32 % WCLimit : 300
% 0.03/5.32 % DateTime : Sun Sep 27 01:11:56 UTC 2026
% 0.03/5.32 % CPUTime :
% 0.03/5.32 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.04/14.11 % SZS status Theorem for theBenchmark.p
% 20.04/14.11 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------