%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+8 : 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 : n003.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.27s 9.10s
% Output : CNFRefutation 66.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 6
% Syntax : Number of formulae : 37 ( 12 unt; 0 def)
% Number of atoms : 391 ( 0 equ)
% Maximal formula atoms : 259 ( 10 avg)
% Number of connectives : 440 ( 86 ~; 73 |; 278 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 259 ( 12 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 : 72 ( 2 sgn 9 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_news_1099_a19984,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(chea_obj_abs__event,axiom,
! [X0,X1,X2] :
( ( obj(X0,X2)
& chea(X1,X0) )
=> obj(X1,X2) ) ).
fof(fact_8354,axiom,
chea('n374bernehmen$u1$u1','annahme$u1$u1') ).
fof(synth_qa07_007_mira_news_1099_a19984,conjecture,
? [X0,X1,X2,X3,X4,X5] :
( val(X1,'bmw$u0')
& subs(X3,'n374bernehmen$u1$u1')
& sub(X1,'name$u1$u1')
& sub(X0,'firma$u1$u1')
& prop(X0,'britisch$u$u1$u1')
& obj(X3,X0)
& attr(X4,X5)
& attr(X2,X1)
& agt(X3,X2) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5] :
( val(X1,'bmw$u0')
& subs(X3,'n374bernehmen$u1$u1')
& sub(X1,'name$u1$u1')
& sub(X0,'firma$u1$u1')
& prop(X0,'britisch$u$u1$u1')
& obj(X3,X0)
& attr(X4,X5)
& attr(X2,X1)
& agt(X3,X2) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_007_mira_news_1099_a19984]) ).
cnf(c10,plain,
agt(c1730,c2006),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1099_a19984]) ).
cnf(c12,plain,
obj(c1730,c1912),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1099_a19984]) ).
cnf(c13,plain,
subs(c1730,'annahme$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1099_a19984]) ).
cnf(c19,plain,
prop(c1912,'britisch$u$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1099_a19984]) ).
cnf(c20,plain,
sub(c1912,'firma$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1099_a19984]) ).
cnf(c23,plain,
attr(c2006,c2007),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1099_a19984]) ).
cnf(c26,plain,
sub(c2007,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1099_a19984]) ).
cnf(c27,plain,
val(c2007,'bmw$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1099_a19984]) ).
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(c324,plain,
( obj(X0,X2)
| ~ obj(X1,X2)
| ~ chea(X0,X1) ),
inference(clausification,[status(esa)],[chea_obj_abs__event]) ).
cnf(c359,plain,
chea('n374bernehmen$u1$u1','annahme$u1$u1'),
inference(clausification,[status(esa)],[fact_8354]) ).
cnf(c364,plain,
( ~ attr(X4,X5)
| ~ attr(X3,X0)
| ~ subs(X2,'n374bernehmen$u1$u1')
| ~ obj(X2,X1)
| ~ val(X0,'bmw$u0')
| ~ prop(X1,'britisch$u$u1$u1')
| ~ agt(X2,X3)
| ~ sub(X1,'firma$u1$u1')
| ~ 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,
( obj(sK78(X0,'n374bernehmen$u1$u1'),X1)
| ~ obj(X0,X1)
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[d0,c324]) ).
cnf(d3,plain,
( ~ subs(X3,'n374bernehmen$u1$u1')
| ~ obj(X3,X0)
| ~ agt(X3,X2)
| ~ val(X1,'bmw$u0')
| ~ prop(X0,'britisch$u$u1$u1')
| ~ attr(X2,X1)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(factoring,[status(thm)],[c364]) ).
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,
( ~ obj(sK78(X0,'n374bernehmen$u1$u1'),X2)
| ~ agt(sK78(X0,'n374bernehmen$u1$u1'),X3)
| ~ val(X1,'bmw$u0')
| ~ prop(X2,'britisch$u$u1$u1')
| ~ attr(X3,X1)
| ~ sub(X2,'firma$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[d4,d3]) ).
cnf(d6,plain,
( ~ subs(X3,'annahme$u1$u1')
| ~ obj(X3,X0)
| ~ subs(X3,'annahme$u1$u1')
| ~ agt(sK78(X3,'n374bernehmen$u1$u1'),X2)
| ~ val(X1,'bmw$u0')
| ~ prop(X0,'britisch$u$u1$u1')
| ~ attr(X2,X1)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d5,d2]) ).
cnf(d7,plain,
( ~ subs(X3,'annahme$u1$u1')
| ~ agt(X3,X2)
| ~ subs(X3,'annahme$u1$u1')
| ~ obj(X3,X1)
| ~ val(X0,'bmw$u0')
| ~ prop(X1,'britisch$u$u1$u1')
| ~ attr(X2,X0)
| ~ sub(X1,'firma$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d6,d1]) ).
cnf(d8,plain,
( ~ obj(c1730,X0)
| ~ agt(c1730,X2)
| ~ val(X1,'bmw$u0')
| ~ prop(X0,'britisch$u$u1$u1')
| ~ attr(X2,X1)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d7,c13]) ).
cnf(d9,plain,
( ~ agt(c1730,X1)
| ~ val(X0,'bmw$u0')
| ~ prop(c1912,'britisch$u$u1$u1')
| ~ attr(X1,X0)
| ~ sub(c1912,'firma$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d8,c12]) ).
cnf(d10,plain,
( ~ agt(c1730,X1)
| ~ val(X0,'bmw$u0')
| ~ attr(X1,X0)
| ~ sub(c1912,'firma$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[c19,d9]) ).
cnf(d11,plain,
( ~ agt(c1730,X1)
| ~ val(X0,'bmw$u0')
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[c20,d10]) ).
cnf(d12,plain,
( ~ val(X0,'bmw$u0')
| ~ attr(c2006,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d11,c10]) ).
cnf(d13,plain,
( ~ attr(c2006,c2007)
| ~ sub(c2007,'name$u1$u1') ),
inference(resolution,[status(thm)],[d12,c27]) ).
cnf(d14,plain,
~ sub(c2007,'name$u1$u1'),
inference(resolution,[status(thm)],[c23,d13]) ).
cnf(d15,plain,
$false,
inference(resolution,[status(thm)],[c26,d14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+8 : 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.11/0.37 % Computer : n003.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 01:14:55 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 66.27/9.10 % SZS status Theorem for theBenchmark.p
% 66.27/9.10 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------