%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+49 : 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 : n015.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:44 AM UTC 2026
% Result : Theorem 84.14s 17.81s
% Output : CNFRefutation 84.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 4
% Syntax : Number of formulae : 22 ( 9 unt; 0 def)
% Number of atoms : 254 ( 0 equ)
% Maximal formula atoms : 180 ( 11 avg)
% Number of connectives : 275 ( 43 ~; 34 |; 197 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 180 ( 13 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 1 prp; 0-5 aty)
% Number of functors : 47 ( 47 usr; 46 con; 0-2 aty)
% Number of variables : 44 ( 8 sgn 3 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_news_1294,hypothesis,
( sort('m$u$u374nchen$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(c87,'varia$uc')
& refer(c87,indet)
& quant(c87,one)
& gener(c87,sp)
& fact(c87,real)
& etype(c87,int0)
& card(c87,int1)
& sort(c87,na)
& 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(c74,'varia$uc')
& refer(c74,indet)
& quant(c74,one)
& gener(c74,sp)
& fact(c74,real)
& etype(c74,int0)
& card(c74,int1)
& sort(c74,na)
& sort('rover$u0',fe)
& sort('britisch$u$u1$u1',nq)
& varia(c56,'varia$uc')
& refer(c56,indet)
& quant(c56,one)
& gener(c56,sp)
& fact(c56,real)
& etype(c56,int0)
& card(c56,int1)
& sort(c56,na)
& 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(c55,con)
& refer(c55,det)
& quant(c55,one)
& gener(c55,sp)
& fact(c55,real)
& etype(c55,int0)
& card(c55,int1)
& sort(c55,io)
& sort(c55,d)
& sort('eu$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('kommission$u1$u1','varia$uc')
& refer('kommission$u1$u1','refer$uc')
& quant('kommission$u1$u1','quant$uc')
& gener('kommission$u1$u1',ge)
& fact('kommission$u1$u1',real)
& etype('kommission$u1$u1',int1)
& card('kommission$u1$u1','card$uc')
& sort('kommission$u1$u1',io)
& sort('kommission$u1$u1',d)
& varia(c19,'varia$uc')
& refer(c19,det)
& quant(c19,one)
& gener(c19,sp)
& fact(c19,real)
& etype(c19,int0)
& card(c19,int1)
& sort(c19,na)
& varia(c86,con)
& refer(c86,det)
& quant(c86,one)
& gener(c86,sp)
& fact(c86,real)
& etype(c86,int0)
& card(c86,int1)
& sort(c86,io)
& sort(c86,d)
& varia(c73,con)
& refer(c73,det)
& quant(c73,one)
& gener(c73,sp)
& fact(c73,real)
& etype(c73,int0)
& card(c73,int1)
& sort(c73,io)
& sort(c73,d)
& varia(c25,con)
& refer(c25,det)
& quant(c25,one)
& gener(c25,sp)
& fact(c25,real)
& etype(c25,int0)
& card(c25,int1)
& sort(c25,ad)
& varia(c18,'varia$uc')
& refer(c18,det)
& quant(c18,one)
& gener(c18,sp)
& fact(c18,real)
& etype(c18,int1)
& card(c18,int1)
& sort(c18,io)
& sort(c18,d)
& varia(c171,'varia$uc')
& refer(c171,'refer$uc')
& quant(c171,'quant$uc')
& gener(c171,'gener$uc')
& fact(c171,real)
& etype(c171,'etype$uc')
& card(c171,'card$uc')
& sort(c171,ent)
& 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)
& val(c87,'m$u$u374nchen$u0')
& sub(c87,'name$u1$u1')
& sub(c86,'stadt$u$u1$u1')
& attr(c86,c87)
& val(c74,'bmw$u0')
& sub(c74,'name$u1$u1')
& sub(c73,'firma$u1$u1')
& attr(c73,c74)
& val(c56,'rover$u0')
& sub(c56,'name$u1$u1')
& sub(c55,'autobauer$u1$u1')
& prop(c55,'britisch$u$u1$u1')
& attr(c55,c56)
& subs(c25,'annahme$u1$u1')
& obj(c25,c55)
& val(c19,'eu$u0')
& sub(c19,'name$u1$u1')
& sub(c18,'kommission$u1$u1')
& attr(c18,c19)
& 'tupl$up5'(c171,c18,c25,c73,c86)
& 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(fact_8354,axiom,
chea('n374bernehmen$u1$u1','annahme$u1$u1') ).
fof(synth_qa07_007_mira_news_1294,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(X0,'firma$u1$u1')
& sub(X1,'name$u1$u1')
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1) ) ).
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(X0,'firma$u1$u1')
& sub(X1,'name$u1$u1')
& attr(X5,X6)
& attr(X3,X2)
& attr(X0,X1) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_007_mira_news_1294]) ).
cnf(c8,plain,
subs(c25,'annahme$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1294]) ).
cnf(c14,plain,
attr(c73,c74),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1294]) ).
cnf(c15,plain,
sub(c73,'firma$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1294]) ).
cnf(c16,plain,
sub(c74,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1294]) ).
cnf(c17,plain,
val(c74,'bmw$u0'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1294]) ).
cnf(c229,plain,
( subs(sK66(X2,X0),X0)
| ~ subs(X2,X1)
| ~ chea(X0,X1) ),
inference(clausification,[status(esa)],[chea_subs_abs__event]) ).
cnf(c260,plain,
chea('n374bernehmen$u1$u1','annahme$u1$u1'),
inference(clausification,[status(esa)],[fact_8354]) ).
cnf(c269,plain,
( ~ sub(X0,'name$u1$u1')
| ~ subs(X6,'n374bernehmen$u1$u1')
| ~ attr(X5,X4)
| ~ val(X4,'bmw$u0')
| ~ sub(X4,'name$u1$u1')
| ~ attr(X2,X3)
| ~ sub(X1,'firma$u1$u1')
| ~ attr(X1,X0)
| ~ val(X0,'bmw$u0') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ subs(X4,'n374bernehmen$u1$u1')
| ~ val(X1,'bmw$u0')
| ~ val(X0,'bmw$u0')
| ~ attr(X2,X1)
| ~ attr(X3,X0)
| ~ sub(X2,'firma$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'name$u1$u1') ),
inference(factoring,[status(thm)],[c269]) ).
cnf(d1,plain,
( ~ subs(X2,'n374bernehmen$u1$u1')
| ~ val(X1,'bmw$u0')
| ~ val(X1,'bmw$u0')
| ~ attr(X0,X1)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(factoring,[status(thm)],[d0]) ).
cnf(d2,plain,
( subs(sK66(X0,'n374bernehmen$u1$u1'),'n374bernehmen$u1$u1')
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[c229,c260]) ).
cnf(d3,plain,
( ~ val(X1,'bmw$u0')
| ~ attr(X2,X1)
| ~ sub(X2,'firma$u1$u1')
| ~ sub(X1,'name$u1$u1')
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[d2,d1]) ).
cnf(d4,plain,
( ~ val(X1,'bmw$u0')
| ~ attr(X0,X1)
| ~ sub(X1,'name$u1$u1')
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[d3,c8]) ).
cnf(d5,plain,
( ~ attr(X0,c74)
| ~ sub(X0,'firma$u1$u1')
| ~ sub(c74,'name$u1$u1') ),
inference(resolution,[status(thm)],[d4,c17]) ).
cnf(d6,plain,
( ~ attr(X0,c74)
| ~ sub(X0,'firma$u1$u1') ),
inference(resolution,[status(thm)],[c16,d5]) ).
cnf(d7,plain,
~ sub(c73,'firma$u1$u1'),
inference(resolution,[status(thm)],[d6,c14]) ).
cnf(d8,plain,
$false,
inference(resolution,[status(thm)],[c15,d7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+49 : 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.14/5.41 % Computer : n015.cluster.edu
% 0.14/5.41 % Model : x86_64 x86_64
% 0.14/5.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.41 % Memory : 8046.5625MB
% 0.14/5.41 % OS : Linux 6.8.0-71-generic
% 0.14/5.41 % CPULimit : 300
% 0.14/5.41 % WCLimit : 300
% 0.14/5.41 % DateTime : Sun Sep 27 01:13:04 UTC 2026
% 0.14/5.42 % CPUTime :
% 0.14/5.42 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 84.14/17.81 % SZS status Theorem for theBenchmark.p
% 84.14/17.81 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------