%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+83 : 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 : n004.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:49 AM UTC 2026
% Result : Theorem 66.45s 12.83s
% Output : CNFRefutation 66.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 6
% Syntax : Number of formulae : 42 ( 15 unt; 0 def)
% Number of atoms : 395 ( 0 equ)
% Maximal formula atoms : 211 ( 9 avg)
% Number of connectives : 482 ( 129 ~; 113 |; 237 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 211 ( 11 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 27 ( 26 usr; 1 prp; 0-3 aty)
% Number of functors : 67 ( 67 usr; 66 con; 0-2 aty)
% Number of variables : 102 ( 15 sgn 8 !; 17 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_wp_499,hypothesis,
( gener('prop$u0','gener$uc')
& fact('prop$u0',real)
& sort('prop$u0',st)
& gener('werden$u1$u1',ge)
& fact('werden$u1$u1',real)
& sort('werden$u1$u1',dn)
& sort('besonders$u1$u1',lg)
& sort('bmw$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)
& varia(c1798,'varia$uc')
& refer(c1798,indet)
& quant(c1798,one)
& gener(c1798,sp)
& fact(c1798,real)
& etype(c1798,int0)
& card(c1798,int1)
& sort(c1798,na)
& sort('rover$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('britisch$u$u1$u1',nq)
& varia(c1786,'varia$uc')
& refer(c1786,indet)
& quant(c1786,one)
& gener(c1786,sp)
& fact(c1786,real)
& etype(c1786,int0)
& card(c1786,int1)
& sort(c1786,na)
& gener('einf$u$u344deln$u1$u1',ge)
& fact('einf$u$u344deln$u1$u1',real)
& sort('einf$u$u344deln$u1$u1',da)
& gener(c1751,sp)
& fact(c1751,real)
& sort(c1751,da)
& 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)
& sort(c2,tq)
& varia(c1785,con)
& refer(c1785,det)
& quant(c1785,one)
& gener(c1785,sp)
& fact(c1785,real)
& etype(c1785,int0)
& card(c1785,int1)
& sort(c1785,io)
& sort(c1785,d)
& varia(c1797,con)
& refer(c1797,det)
& quant(c1797,one)
& gener(c1797,sp)
& fact(c1797,real)
& etype(c1797,int0)
& card(c1797,int1)
& sort(c1797,io)
& sort(c1797,d)
& card(c1744,int1994)
& sort(c1744,nu)
& 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(c1748,'varia$uc')
& refer(c1748,'refer$uc')
& quant(c1748,'quant$uc')
& gener(c1748,sp)
& fact(c1748,real)
& etype(c1748,'etype$uc')
& card(c1748,'card$uc')
& sort(c1748,ta)
& sort(c1748,oa)
& sort(c1748,me)
& varia(c1747,con)
& refer(c1747,det)
& quant(c1747,one)
& gener(c1747,sp)
& fact(c1747,real)
& etype(c1747,int0)
& card(c1747,int1)
& sort(c1747,t)
& sort('pischetsrieder$u0',fe)
& varia('familiename$u1$u1','varia$uc')
& refer('familiename$u1$u1','refer$uc')
& quant('familiename$u1$u1',one)
& gener('familiename$u1$u1',ge)
& fact('familiename$u1$u1',real)
& etype('familiename$u1$u1',int0)
& card('familiename$u1$u1',int1)
& sort('familiename$u1$u1',na)
& varia('mensch$u1$u1','varia$uc')
& refer('mensch$u1$u1','refer$uc')
& quant('mensch$u1$u1',one)
& gener('mensch$u1$u1',ge)
& fact('mensch$u1$u1',real)
& etype('mensch$u1$u1',int0)
& card('mensch$u1$u1',int1)
& sort('mensch$u1$u1',d)
& sort('bekannt$u1$u1',nq)
& varia(c1736,'varia$uc')
& refer(c1736,indet)
& quant(c1736,one)
& gener(c1736,sp)
& fact(c1736,real)
& etype(c1736,int0)
& card(c1736,int1)
& sort(c1736,na)
& varia(c1735,con)
& refer(c1735,det)
& quant(c1735,one)
& gener(c1735,sp)
& fact(c1735,real)
& etype(c1735,int0)
& card(c1735,int1)
& sort(c1735,d)
& gener(c1800,sp)
& fact(c1800,real)
& sort(c1800,dn)
& gener(c1801,sp)
& fact(c1801,real)
& sort(c1801,st)
& varia(c1750,con)
& refer(c1750,det)
& quant(c1750,one)
& gener(c1750,sp)
& fact(c1750,real)
& etype(c1750,int0)
& card(c1750,int1)
& sort(c1750,ad)
& gener(c1731,sp)
& fact(c1731,real)
& sort(c1731,dn)
& 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)
& sort('automobil$u1$u1',tq)
& 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)
& chsp2('einf$u$u344deln$u1$u1',c2)
& subr(c1801,'prop$u0')
& arg2(c1801,'bekannt$u1$u1')
& arg1(c1801,c1735)
& mods(c1800,'besonders$u1$u1','werden$u1$u1')
& val(c1798,'bmw$u0')
& sub(c1798,'name$u1$u1')
& sub(c1797,'firma$u1$u1')
& attr(c1797,c1798)
& val(c1786,'rover$u0')
& sub(c1786,'name$u1$u1')
& sub(c1785,'autobauer$u1$u1')
& prop(c1785,'britisch$u$u1$u1')
& attr(c1785,c1786)
& temp(c1751,c1747)
& subs(c1751,'einf$u$u344deln$u1$u1')
& obj(c1751,c1750)
& agt(c1751,c1735)
& subs(c1750,'annahme$u1$u1')
& prop(c1750,c2)
& obj(c1750,c1785)
& agt(c1750,c1797)
& val(c1748,c1744)
& sub(c1748,'jahr$u$u1$u1')
& attr(c1747,c1748)
& val(c1736,'pischetsrieder$u0')
& sub(c1736,'familiename$u1$u1')
& sub(c1735,'mensch$u1$u1')
& prop(c1735,'bekannt$u1$u1')
& attr(c1735,c1736)
& subs(c1731,c1800)
& rslt(c1731,c1801)
& cstr(c1731,c1750)
& sub('autobauer$u1$u1','fabrikant$u1$u1')
& assoc('autobauer$u1$u1','automobil$u1$u1') ) ).
fof(has_card_eq,axiom,
! [X0,X1] :
( card(X0,X1)
=> 'has$ucard$uleq'(X0,X1) ) ).
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_wp_499,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7] :
( val(X6,X7)
& val(X2,'bmw$u0')
& val(X1,'bmw$u0')
& subs(X4,'n374bernehmen$u1$u1')
& sub(X6,'jahr$u$u1$u1')
& sub(X2,'name$u1$u1')
& sub(X0,'firma$u1$u1')
& sub(X1,'name$u1$u1')
& 'has$ucard$uleq'(X7,int1994)
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1)
& agt(X4,X3) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7] :
( val(X6,X7)
& val(X2,'bmw$u0')
& val(X1,'bmw$u0')
& subs(X4,'n374bernehmen$u1$u1')
& sub(X6,'jahr$u$u1$u1')
& sub(X2,'name$u1$u1')
& sub(X0,'firma$u1$u1')
& sub(X1,'name$u1$u1')
& 'has$ucard$uleq'(X7,int1994)
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1)
& agt(X4,X3) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_007_mira_wp_499]) ).
cnf(c10,plain,
attr(c1747,c1748),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c11,plain,
sub(c1748,'jahr$u$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c12,plain,
val(c1748,c1744),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c13,plain,
agt(c1750,c1797),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c16,plain,
subs(c1750,'annahme$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c26,plain,
attr(c1797,c1798),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c27,plain,
sub(c1797,'firma$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c28,plain,
sub(c1798,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c29,plain,
val(c1798,'bmw$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c134,plain,
card(c1744,int1994),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_wp_499]) ).
cnf(c230,plain,
( 'has$ucard$uleq'(X0,X1)
| ~ card(X0,X1) ),
inference(clausification,[status(esa)],[has_card_eq]) ).
cnf(c299,plain,
( chea(sK99(X2,X0),X2)
| ~ subs(X2,X1)
| ~ chea(X0,X1) ),
inference(clausification,[status(esa)],[chea_subs_abs__event]) ).
cnf(c300,plain,
( subs(sK99(X2,X0),X0)
| ~ subs(X2,X1)
| ~ chea(X0,X1) ),
inference(clausification,[status(esa)],[chea_subs_abs__event]) ).
cnf(c302,plain,
( agt(X2,X1)
| ~ chea(X2,X0)
| ~ agt(X0,X1) ),
inference(clausification,[status(esa)],[chea_agt_abs__event]) ).
cnf(c437,plain,
chea('n374bernehmen$u1$u1','annahme$u1$u1'),
inference(clausification,[status(esa)],[fact_8354]) ).
cnf(c458,plain,
( ~ 'has$ucard$uleq'(X7,int1994)
| ~ val(X5,X7)
| ~ subs(X2,'n374bernehmen$u1$u1')
| ~ attr(X4,X1)
| ~ attr(X6,X5)
| ~ sub(X5,'jahr$u$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X4,'firma$u1$u1')
| ~ attr(X3,X0)
| ~ agt(X2,X3)
| ~ val(X1,'bmw$u0')
| ~ val(X0,'bmw$u0')
| ~ sub(X0,'name$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)],[c300,c437]) ).
cnf(d1,plain,
'has$ucard$uleq'(c1744,int1994),
inference(resolution,[status(thm)],[c230,c134]) ).
cnf(d2,plain,
( ~ agt(X4,X6)
| ~ val(X2,'bmw$u0')
| ~ val(X1,'bmw$u0')
| ~ val(X0,c1744)
| ~ attr(X6,X1)
| ~ attr(X3,X2)
| ~ attr(X5,X0)
| ~ subs(X4,'n374bernehmen$u1$u1')
| ~ sub(X3,'firma$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'jahr$u$u1$u1') ),
inference(resolution,[status(thm)],[c458,d1]) ).
cnf(d3,plain,
( chea(sK99(X0,'n374bernehmen$u1$u1'),X0)
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[c299,c437]) ).
cnf(d4,plain,
( agt(sK99(X0,'n374bernehmen$u1$u1'),X1)
| ~ agt(X0,X1)
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[d3,c302]) ).
cnf(d5,plain,
( ~ val(X5,c1744)
| ~ val(X4,'bmw$u0')
| ~ val(X3,'bmw$u0')
| ~ attr(X2,X3)
| ~ attr(X6,X5)
| ~ attr(X1,X4)
| ~ subs(sK99(X0,'n374bernehmen$u1$u1'),'n374bernehmen$u1$u1')
| ~ sub(X5,'jahr$u$u1$u1')
| ~ sub(X4,'name$u1$u1')
| ~ sub(X3,'name$u1$u1')
| ~ sub(X2,'firma$u1$u1')
| ~ agt(X0,X1)
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[d4,d2]) ).
cnf(d6,plain,
( ~ subs(X4,'annahme$u1$u1')
| ~ agt(X4,X6)
| ~ val(X2,'bmw$u0')
| ~ val(X1,'bmw$u0')
| ~ val(X0,c1744)
| ~ attr(X6,X1)
| ~ attr(X3,X2)
| ~ attr(X5,X0)
| ~ subs(X4,'annahme$u1$u1')
| ~ sub(X3,'firma$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'jahr$u$u1$u1') ),
inference(resolution,[status(thm)],[d5,d0]) ).
cnf(d7,plain,
( ~ val(X3,c1744)
| ~ val(X2,'bmw$u0')
| ~ val(X1,'bmw$u0')
| ~ attr(X0,X1)
| ~ attr(X4,X3)
| ~ attr(c1797,X2)
| ~ subs(c1750,'annahme$u1$u1')
| ~ sub(X3,'jahr$u$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d6,c13]) ).
cnf(d8,plain,
( ~ val(X2,'bmw$u0')
| ~ val(X1,'bmw$u0')
| ~ val(X0,c1744)
| ~ attr(c1797,X1)
| ~ attr(X3,X2)
| ~ attr(X4,X0)
| ~ sub(X3,'firma$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'jahr$u$u1$u1') ),
inference(resolution,[status(thm)],[c16,d7]) ).
cnf(d9,plain,
( ~ val(X2,'bmw$u0')
| ~ val(X1,'bmw$u0')
| ~ attr(c1797,X2)
| ~ attr(X0,X1)
| ~ attr(X3,c1748)
| ~ sub(c1748,'jahr$u$u1$u1')
| ~ sub(X2,'name$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d8,c12]) ).
cnf(d10,plain,
( ~ val(X1,'bmw$u0')
| ~ val(X0,'bmw$u0')
| ~ attr(c1797,X0)
| ~ attr(X2,X1)
| ~ attr(X3,c1748)
| ~ sub(X2,'firma$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[c11,d9]) ).
cnf(d11,plain,
( ~ val(X1,'bmw$u0')
| ~ attr(c1797,c1798)
| ~ attr(X0,X1)
| ~ attr(X2,c1748)
| ~ sub(c1798,'name$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d10,c29]) ).
cnf(d12,plain,
( ~ val(X0,'bmw$u0')
| ~ attr(X1,X0)
| ~ attr(X2,c1748)
| ~ sub(c1798,'name$u1$u1')
| ~ sub(X1,'firma$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[c26,d11]) ).
cnf(d13,plain,
( ~ val(X1,'bmw$u0')
| ~ attr(X0,X1)
| ~ attr(X2,c1748)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[c28,d12]) ).
cnf(d14,plain,
( ~ attr(X0,c1798)
| ~ attr(X1,c1748)
| ~ sub(X0,'firma$u1$u1')
| ~ sub(c1798,'name$u1$u1') ),
inference(resolution,[status(thm)],[d13,c29]) ).
cnf(d15,plain,
( ~ attr(X0,c1798)
| ~ attr(X1,c1748)
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[c28,d14]) ).
cnf(d16,plain,
( ~ attr(X0,c1748)
| ~ sub(c1797,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d15,c26]) ).
cnf(d17,plain,
~ attr(X0,c1748),
inference(resolution,[status(thm)],[c27,d16]) ).
cnf(d18,plain,
$false,
inference(resolution,[status(thm)],[d17,c10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR115+83 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.35 % Computer : n004.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8046.5625MB
% 0.12/0.35 % OS : Linux 6.8.0-71-generic
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Sun Sep 27 01:12:37 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 66.45/12.83 % SZS status Theorem for theBenchmark.p
% 66.45/12.83 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------