%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+37 : 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 : n014.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:42 AM UTC 2026
% Result : Theorem 52.78s 8.40s
% Output : CNFRefutation 52.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 3
% Syntax : Number of formulae : 26 ( 12 unt; 0 def)
% Number of atoms : 271 ( 0 equ)
% Maximal formula atoms : 173 ( 10 avg)
% Number of connectives : 306 ( 61 ~; 50 |; 194 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 173 ( 12 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 1 prp; 0-3 aty)
% Number of functors : 56 ( 56 usr; 56 con; 0-0 aty)
% Number of variables : 58 ( 11 sgn 2 !; 16 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_news_1229,hypothesis,
( varia('entwicklungstendenz$u1$u1','varia$uc')
& refer('entwicklungstendenz$u1$u1','refer$uc')
& quant('entwicklungstendenz$u1$u1',one)
& gener('entwicklungstendenz$u1$u1',ge)
& fact('entwicklungstendenz$u1$u1',real)
& etype('entwicklungstendenz$u1$u1',int0)
& card('entwicklungstendenz$u1$u1',int1)
& sort('entwicklungstendenz$u1$u1',io)
& varia('markt$u1$u1','varia$uc')
& refer('markt$u1$u1','refer$uc')
& quant('markt$u1$u1',one)
& gener('markt$u1$u1',ge)
& fact('markt$u1$u1',real)
& etype('markt$u1$u1',int0)
& card('markt$u1$u1',int1)
& sort('markt$u1$u1',d)
& sort('halb$u$u1$u1',tq)
& varia('sich$u1$u1','varia$uc')
& refer('sich$u1$u1','refer$uc')
& quant('sich$u1$u1',one)
& gener('sich$u1$u1','gener$uc')
& fact('sich$u1$u1',real)
& etype('sich$u1$u1',int0)
& card('sich$u1$u1',int1)
& sort('sich$u1$u1',o)
& 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('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(c94,'varia$uc')
& refer(c94,indet)
& quant(c94,one)
& gener(c94,sp)
& fact(c94,real)
& etype(c94,int0)
& card(c94,int1)
& sort(c94,na)
& gener('abkoppeln$u1$u1',ge)
& fact('abkoppeln$u1$u1',real)
& sort('abkoppeln$u1$u1',da)
& varia(c95,'varia$uc')
& refer(c95,'refer$uc')
& quant(c95,'quant$uc')
& gener(c95,sp)
& fact(c95,real)
& etype(c95,'etype$uc')
& card(c95,'card$uc')
& sort(c95,co)
& gener('k$u$u366nnen$u0','gener$uc')
& fact('k$u$u366nnen$u0',real)
& sort('k$u$u366nnen$u0',md)
& varia(c93,con)
& refer(c93,det)
& quant(c93,one)
& gener(c93,sp)
& fact(c93,real)
& etype(c93,int0)
& card(c93,int1)
& sort(c93,io)
& sort(c93,d)
& gener(c111,sp)
& fact(c111,real)
& sort(c111,da)
& varia('markttrend$u1$u1','varia$uc')
& refer('markttrend$u1$u1','refer$uc')
& quant('markttrend$u1$u1',one)
& gener('markttrend$u1$u1',ge)
& fact('markttrend$u1$u1',real)
& etype('markttrend$u1$u1',int0)
& card('markttrend$u1$u1',int1)
& sort('markttrend$u1$u1',io)
& sort('r$u$u374ckg$u$u344ngig$u1$u1',nq)
& varia(c110,con)
& refer(c110,det)
& quant(c110,one)
& gener(c110,sp)
& fact(c110,real)
& etype(c110,int0)
& card(c110,int1)
& sort(c110,io)
& card(c102,int1994)
& sort(c102,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(c107,'varia$uc')
& refer(c107,'refer$uc')
& quant(c107,'quant$uc')
& gener(c107,sp)
& fact(c107,real)
& etype(c107,'etype$uc')
& card(c107,'card$uc')
& sort(c107,ta)
& sort(c107,oa)
& sort(c107,me)
& varia('halbjahr$u1$u1','varia$uc')
& refer('halbjahr$u1$u1','refer$uc')
& quant('halbjahr$u1$u1',one)
& gener('halbjahr$u1$u1',ge)
& fact('halbjahr$u1$u1',real)
& etype('halbjahr$u1$u1',int0)
& card('halbjahr$u1$u1',int1)
& sort('halbjahr$u1$u1',ta)
& card('erst$u1$u1',int1)
& sort('erst$u1$u1',oq)
& varia(c106,con)
& refer(c106,det)
& quant(c106,one)
& gener(c106,sp)
& fact(c106,real)
& etype(c106,int0)
& card(c106,int1)
& sort(c106,t)
& varia(c103,'varia$uc')
& refer(c103,'refer$uc')
& quant(c103,one)
& gener(c103,ge)
& fact(c103,real)
& etype(c103,int0)
& card(c103,int1)
& sort(c103,ta)
& varia(c100,con)
& refer(c100,det)
& quant(c100,one)
& gener(c100,sp)
& fact(c100,real)
& etype(c100,int0)
& card(c100,int1)
& sort(c100,ta)
& sub('markttrend$u1$u1','entwicklungstendenz$u1$u1')
& assoc('markttrend$u1$u1','markt$u1$u1')
& sub('halbjahr$u1$u1','jahr$u$u1$u1')
& assoc('halbjahr$u1$u1','halb$u$u1$u1')
& sub(c95,'sich$u1$u1')
& val(c94,'bmw$u0')
& sub(c94,'name$u1$u1')
& sub(c93,'firma$u1$u1')
& attr(c93,c94)
& temp(c111,c100)
& subs(c111,'abkoppeln$u1$u1')
& obj(c111,c95)
& modl(c111,'k$u$u366nnen$u0')
& benf(c111,c93)
& sub(c110,'markttrend$u1$u1')
& prop(c110,'r$u$u374ckg$u$u344ngig$u1$u1')
& attch(c110,c100)
& val(c107,c102)
& sub(c107,'jahr$u$u1$u1')
& attr(c106,c107)
& pmod(c103,'erst$u1$u1','halbjahr$u1$u1')
& temp(c100,c106)
& sub(c100,c103) ) ).
fof(has_card_eq,axiom,
! [X0,X1] :
( card(X0,X1)
=> 'has$ucard$uleq'(X0,X1) ) ).
fof(synth_qa07_007_mira_news_1229,conjecture,
? [X0,X1,X2,X3,X4,X5,X6,X7] :
( val(X6,X7)
& val(X2,'bmw$u0')
& val(X1,'bmw$u0')
& temp(X4,X5)
& 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) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5,X6,X7] :
( val(X6,X7)
& val(X2,'bmw$u0')
& val(X1,'bmw$u0')
& temp(X4,X5)
& 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) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_007_mira_news_1229]) ).
cnf(c1,plain,
temp(c100,c106),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1229]) ).
cnf(c3,plain,
attr(c106,c107),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1229]) ).
cnf(c4,plain,
sub(c107,'jahr$u$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1229]) ).
cnf(c5,plain,
val(c107,c102),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1229]) ).
cnf(c14,plain,
attr(c93,c94),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1229]) ).
cnf(c15,plain,
sub(c93,'firma$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1229]) ).
cnf(c16,plain,
sub(c94,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1229]) ).
cnf(c17,plain,
val(c94,'bmw$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1229]) ).
cnf(c78,plain,
card(c102,int1994),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1229]) ).
cnf(c187,plain,
( 'has$ucard$uleq'(X0,X1)
| ~ card(X0,X1) ),
inference(clausification,[status(esa)],[has_card_eq]) ).
cnf(c282,plain,
( ~ sub(X1,'name$u1$u1')
| ~ 'has$ucard$uleq'(X3,int1994)
| ~ attr(X7,X0)
| ~ temp(X6,X5)
| ~ attr(X4,X1)
| ~ attr(X5,X2)
| ~ sub(X4,'firma$u1$u1')
| ~ sub(X2,'jahr$u$u1$u1')
| ~ val(X2,X3)
| ~ val(X1,'bmw$u0')
| ~ sub(X0,'name$u1$u1')
| ~ val(X0,'bmw$u0') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ 'has$ucard$uleq'(X5,int1994)
| ~ val(X0,'bmw$u0')
| ~ val(X1,X5)
| ~ val(X0,'bmw$u0')
| ~ attr(X2,X0)
| ~ attr(X4,X1)
| ~ temp(X3,X4)
| ~ sub(X2,'firma$u1$u1')
| ~ sub(X0,'name$u1$u1')
| ~ sub(X1,'jahr$u$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(factoring,[status(thm)],[c282]) ).
cnf(d1,plain,
'has$ucard$uleq'(c102,int1994),
inference(resolution,[status(thm)],[c187,c78]) ).
cnf(d2,plain,
( ~ val(X2,'bmw$u0')
| ~ val(X1,c102)
| ~ attr(X0,X2)
| ~ attr(X4,X1)
| ~ temp(X3,X4)
| ~ sub(X2,'name$u1$u1')
| ~ sub(X1,'jahr$u$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d1,d0]) ).
cnf(d3,plain,
( ~ val(X0,'bmw$u0')
| ~ attr(X1,X0)
| ~ attr(X3,c107)
| ~ temp(X2,X3)
| ~ sub(X1,'firma$u1$u1')
| ~ sub(c107,'jahr$u$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d2,c5]) ).
cnf(d4,plain,
( ~ val(X1,'bmw$u0')
| ~ attr(X0,X1)
| ~ attr(X3,c107)
| ~ temp(X2,X3)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[c4,d3]) ).
cnf(d5,plain,
( ~ attr(X0,c94)
| ~ attr(X2,c107)
| ~ temp(X1,X2)
| ~ sub(X0,'firma$u1$u1')
| ~ sub(c94,'name$u1$u1') ),
inference(resolution,[status(thm)],[d4,c17]) ).
cnf(d6,plain,
( ~ attr(X0,c94)
| ~ attr(X2,c107)
| ~ temp(X1,X2)
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[c16,d5]) ).
cnf(d7,plain,
( ~ attr(X1,c107)
| ~ temp(X0,X1)
| ~ sub(c93,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d6,c14]) ).
cnf(d8,plain,
( ~ attr(X1,c107)
| ~ temp(X0,X1) ),
inference(resolution,[status(thm)],[c15,d7]) ).
cnf(d9,plain,
~ temp(X0,c106),
inference(resolution,[status(thm)],[d8,c3]) ).
cnf(d10,plain,
$false,
inference(resolution,[status(thm)],[d9,c1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+37 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n014.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:08:17 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 52.78/8.40 % SZS status Theorem for theBenchmark.p
% 52.78/8.40 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------