%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+21 : 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 : n016.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:40 AM UTC 2026
% Result : Theorem 45.30s 7.94s
% Output : CNFRefutation 45.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 2
% Syntax : Number of formulae : 17 ( 7 unt; 0 def)
% Number of atoms : 193 ( 0 equ)
% Maximal formula atoms : 135 ( 11 avg)
% Number of connectives : 213 ( 37 ~; 28 |; 148 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 135 ( 13 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-2 aty)
% Number of functors : 43 ( 43 usr; 43 con; 0-0 aty)
% Number of variables : 45 ( 24 sgn 0 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_news_1144,hypothesis,
( gener('val$u0','gener$uc')
& fact('val$u0',real)
& sort('val$u0',st)
& gener('zulegen$u1$u1',ge)
& fact('zulegen$u1$u1',real)
& sort('zulegen$u1$u1',da)
& gener('just$u1$u1','gener$uc')
& fact('just$u1$u1',real)
& sort('just$u1$u1',md)
& gener(c816,sp)
& fact(c816,real)
& sort(c816,da)
& 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(c814,'varia$uc')
& refer(c814,det)
& quant(c814,one)
& gener(c814,sp)
& fact(c814,real)
& etype(c814,int0)
& card(c814,int1)
& sort(c814,io)
& sort(c814,d)
& varia('wert$u1$u1','varia$uc')
& refer('wert$u1$u1','refer$uc')
& quant('wert$u1$u1',one)
& gener('wert$u1$u1',ge)
& fact('wert$u1$u1',real)
& etype('wert$u1$u1',int0)
& card('wert$u1$u1',int1)
& sort('wert$u1$u1',oa)
& sort('wert$u1$u1',io)
& 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('k$u$u344ufer$u1$u1','varia$uc')
& refer('k$u$u344ufer$u1$u1','refer$uc')
& quant('k$u$u344ufer$u1$u1',one)
& gener('k$u$u344ufer$u1$u1',ge)
& fact('k$u$u344ufer$u1$u1',real)
& etype('k$u$u344ufer$u1$u1',int0)
& card('k$u$u344ufer$u1$u1',int1)
& sort('k$u$u344ufer$u1$u1',io)
& sort('k$u$u344ufer$u1$u1',d)
& varia(c718,'varia$uc')
& refer(c718,indet)
& quant(c718,one)
& gener(c718,sp)
& fact(c718,real)
& etype(c718,int0)
& card(c718,int1)
& sort(c718,na)
& varia(c717,con)
& refer(c717,det)
& quant(c717,one)
& gener(c717,sp)
& fact(c717,real)
& etype(c717,int0)
& card(c717,int1)
& sort(c717,io)
& sort(c717,d)
& gener('gewinnen$u1$u2',ge)
& fact('gewinnen$u1$u2',real)
& sort('gewinnen$u1$u2',dn)
& gener(c821,sp)
& fact(c821,real)
& sort(c821,st)
& sort('enorm$u1$u1',nq)
& gener(c822,sp)
& fact(c822,real)
& sort(c822,st)
& gener(c537,sp)
& fact(c537,real)
& sort(c537,dn)
& varia('papier$u1$u1','varia$uc')
& refer('papier$u1$u1','refer$uc')
& quant('papier$u1$u1',one)
& gener('papier$u1$u1',ge)
& fact('papier$u1$u1',real)
& etype('papier$u1$u1',int0)
& card('papier$u1$u1',int1)
& sort('papier$u1$u1',s)
& varia(c802,'varia$uc')
& refer(c802,'refer$uc')
& quant(c802,one)
& gener(c802,'gener$uc')
& fact(c802,real)
& etype(c802,int0)
& card(c802,int1)
& sort(c802,oa)
& sort(c802,io)
& varia(c5,con)
& refer(c5,det)
& quant(c5,one)
& gener(c5,sp)
& fact(c5,real)
& etype(c5,int0)
& card(c5,int1)
& sort(c5,s)
& subr(c822,'val$u0')
& arg1(c822,c802)
& subr(c821,'val$u0')
& arg1(c821,c802)
& subs(c816,'zulegen$u1$u1')
& reas(c816,c537)
& obj(c816,c814)
& modl(c816,'just$u1$u1')
& agt(c816,c717)
& sub(c814,'firma$u1$u1')
& sub(c802,'wert$u1$u1')
& val(c718,'bmw$u0')
& sub(c718,'name$u1$u1')
& sub(c717,'k$u$u344ufer$u1$u1')
& attr(c717,c718)
& attch(c717,c5)
& subs(c537,'gewinnen$u1$u2')
& rslt(c537,c821)
& mannr(c537,'enorm$u1$u1')
& init(c537,c822)
& aff(c537,c5)
& sub(c5,'papier$u1$u1')
& attr(c5,c802) ) ).
fof(synth_qa07_007_mira_news_1144,conjecture,
? [X0,X1,X2,X3,X4,X5,X6] :
( val(X2,'bmw$u0')
& val(X1,'bmw$u0')
& 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')
& 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_1144]) ).
cnf(c0,plain,
attr(c5,c802),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1144]) ).
cnf(c8,plain,
attr(c717,c718),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1144]) ).
cnf(c10,plain,
sub(c718,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1144]) ).
cnf(c11,plain,
val(c718,'bmw$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1144]) ).
cnf(c14,plain,
agt(c816,c717),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1144]) ).
cnf(c10506,plain,
( ~ attr(X5,X6)
| ~ attr(X4,X0)
| ~ sub(X2,'name$u1$u1')
| ~ agt(X3,X4)
| ~ val(X2,'bmw$u0')
| ~ attr(X1,X2)
| ~ val(X0,'bmw$u0')
| ~ sub(X0,'name$u1$u1') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ val(X4,'bmw$u0')
| ~ val(X3,'bmw$u0')
| ~ sub(X4,'name$u1$u1')
| ~ sub(X3,'name$u1$u1')
| ~ attr(c717,X4)
| ~ attr(X2,X3)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[c14,c10506]) ).
cnf(d1,plain,
( ~ val(X3,'bmw$u0')
| ~ sub(c718,'name$u1$u1')
| ~ sub(X3,'name$u1$u1')
| ~ attr(c717,X3)
| ~ attr(X1,X2)
| ~ attr(X0,c718) ),
inference(resolution,[status(thm)],[d0,c11]) ).
cnf(d2,plain,
( ~ val(X3,'bmw$u0')
| ~ sub(X3,'name$u1$u1')
| ~ attr(c717,X3)
| ~ attr(X2,c718)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[c10,d1]) ).
cnf(d3,plain,
( ~ sub(c718,'name$u1$u1')
| ~ attr(c717,c718)
| ~ attr(X1,X2)
| ~ attr(X0,c718) ),
inference(resolution,[status(thm)],[d2,c11]) ).
cnf(d4,plain,
( ~ sub(c718,'name$u1$u1')
| ~ attr(X2,c718)
| ~ attr(X0,X1) ),
inference(resolution,[status(thm)],[c8,d3]) ).
cnf(d5,plain,
( ~ attr(X1,X2)
| ~ attr(X0,c718) ),
inference(resolution,[status(thm)],[c10,d4]) ).
cnf(d6,plain,
~ attr(X0,X1),
inference(resolution,[status(thm)],[d5,c8]) ).
cnf(d7,plain,
$false,
inference(resolution,[status(thm)],[d6,c0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+21 : 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.12/0.38 % Computer : n016.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 01:12:15 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.30/7.94 % SZS status Theorem for theBenchmark.p
% 45.30/7.94 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------