%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+59 : 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 : n020.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:45 AM UTC 2026
% Result : Theorem 62.80s 9.65s
% Output : CNFRefutation 62.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 5
% Syntax : Number of formulae : 27 ( 9 unt; 0 def)
% Number of atoms : 293 ( 0 equ)
% Maximal formula atoms : 218 ( 10 avg)
% Number of connectives : 309 ( 43 ~; 34 |; 230 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 218 ( 12 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 1 prp; 0-7 aty)
% Number of functors : 52 ( 52 usr; 51 con; 0-2 aty)
% Number of variables : 65 ( 22 sgn 6 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ave07_era5_synth_qa07_007_mira_news_1319_a19984,hypothesis,
( varia(c2161,'varia$uc')
& refer(c2161,'refer$uc')
& quant(c2161,'quant$uc')
& gener(c2161,'gener$uc')
& fact(c2161,real)
& etype(c2161,'etype$uc')
& card(c2161,'card$uc')
& sort(c2161,ent)
& varia('get$u$u366se$u1$u1','varia$uc')
& refer('get$u$u366se$u1$u1','refer$uc')
& quant('get$u$u366se$u1$u1',one)
& gener('get$u$u366se$u1$u1',ge)
& fact('get$u$u366se$u1$u1',real)
& etype('get$u$u366se$u1$u1',int0)
& card('get$u$u366se$u1$u1',int1)
& sort('get$u$u366se$u1$u1',d)
& sort('kr$u$u344ftig$u1$u1',nq)
& varia(c157,'varia$uc')
& refer(c157,'refer$uc')
& quant(c157,one)
& gener(c157,'gener$uc')
& fact(c157,real)
& etype(c157,int0)
& card(c157,int1)
& sort(c157,d)
& sort('frankfurter$u1$u1',gq)
& varia(c145,con)
& refer(c145,det)
& quant(c145,one)
& gener(c145,sp)
& fact(c145,real)
& etype(c145,int0)
& card(c145,int1)
& sort(c145,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(c134,'varia$uc')
& refer(c134,'refer$uc')
& quant(c134,one)
& gener(c134,'gener$uc')
& fact(c134,real)
& etype(c134,int0)
& card(c134,int1)
& sort(c134,io)
& sort(c134,d)
& varia('bmw$u1$u1','varia$uc')
& refer('bmw$u1$u1','refer$uc')
& quant('bmw$u1$u1',one)
& gener('bmw$u1$u1',ge)
& fact('bmw$u1$u1',real)
& etype('bmw$u1$u1',int0)
& card('bmw$u1$u1',int1)
& sort('bmw$u1$u1',d)
& sort('bairisch$u1$u1',nq)
& varia(c130,con)
& refer(c130,det)
& quant(c130,one)
& gener(c130,sp)
& fact(c130,real)
& etype(c130,int0)
& card(c130,int1)
& sort(c130,d)
& varia('rover$u1$u1','varia$uc')
& refer('rover$u1$u1','refer$uc')
& quant('rover$u1$u1',one)
& gener('rover$u1$u1',ge)
& fact('rover$u1$u1',real)
& etype('rover$u1$u1',int0)
& card('rover$u1$u1',int1)
& sort('rover$u1$u1',d)
& varia(c122,'varia$uc')
& refer(c122,'refer$uc')
& quant(c122,one)
& gener(c122,'gener$uc')
& fact(c122,real)
& etype(c122,int0)
& card(c122,int1)
& sort(c122,d)
& sort('britisch$u$u1$u1',nq)
& 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(c117,con)
& refer(c117,det)
& quant(c117,one)
& gener(c117,sp)
& fact(c117,real)
& etype(c117,int0)
& card(c117,int1)
& sort(c117,d)
& varia(c113,con)
& refer(c113,det)
& quant(c113,one)
& gener(c113,sp)
& fact(c113,real)
& etype(c113,int0)
& card(c113,int1)
& sort(c113,ad)
& sort('frankfurt$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('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(c104,'varia$uc')
& refer(c104,det)
& quant(c104,one)
& gener(c104,sp)
& fact(c104,real)
& etype(c104,int0)
& card(c104,int1)
& sort(c104,na)
& varia(c103,'varia$uc')
& refer(c103,det)
& quant(c103,one)
& gener(c103,sp)
& fact(c103,real)
& etype(c103,int0)
& card(c103,int1)
& sort(c103,io)
& sort(c103,d)
& varia('parkett$u1$u1','varia$uc')
& refer('parkett$u1$u1','refer$uc')
& quant('parkett$u1$u1',one)
& gener('parkett$u1$u1',ge)
& fact('parkett$u1$u1',real)
& etype('parkett$u1$u1',int0)
& card('parkett$u1$u1',int1)
& sort('parkett$u1$u1',d)
& varia('b$u$u366rse$u1$u1','varia$uc')
& refer('b$u$u366rse$u1$u1','refer$uc')
& quant('b$u$u366rse$u1$u1',one)
& gener('b$u$u366rse$u1$u1',ge)
& fact('b$u$u366rse$u1$u1',real)
& etype('b$u$u366rse$u1$u1',int0)
& card('b$u$u366rse$u1$u1',int1)
& sort('b$u$u366rse$u1$u1',io)
& sort('b$u$u366rse$u1$u1',d)
& varia('b$u$u366rsenparkett$u1$u1','varia$uc')
& refer('b$u$u366rsenparkett$u1$u1','refer$uc')
& quant('b$u$u366rsenparkett$u1$u1',one)
& gener('b$u$u366rsenparkett$u1$u1',ge)
& fact('b$u$u366rsenparkett$u1$u1',real)
& etype('b$u$u366rsenparkett$u1$u1',int0)
& card('b$u$u366rsenparkett$u1$u1',int1)
& sort('b$u$u366rsenparkett$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)
& assoc('frankfurter$u1$u1',c103)
& 'tupl$up7'(c2161,c113,c122,c130,c134,c145,c157)
& sub(c157,'get$u$u366se$u1$u1')
& prop(c157,'kr$u$u344ftig$u1$u1')
& sub(c145,'b$u$u366rsenparkett$u1$u1')
& prop(c145,'frankfurter$u1$u1')
& sub(c134,'firmengruppe$u1$u1')
& sub(c130,'bmw$u1$u1')
& prop(c130,'bairisch$u1$u1')
& sub(c122,'rover$u1$u1')
& sub(c117,'autobauer$u1$u1')
& prop(c117,'britisch$u$u1$u1')
& subs(c113,'annahme$u1$u1')
& obj(c113,c117)
& val(c104,'frankfurt$u0')
& sub(c104,'name$u1$u1')
& sub(c103,'stadt$u$u1$u1')
& attr(c103,c104)
& sub('b$u$u366rsenparkett$u1$u1','parkett$u1$u1')
& assoc('b$u$u366rsenparkett$u1$u1','b$u$u366rse$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_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_1319_a19984,conjecture,
? [X0,X1,X2,X3,X4,X5] :
( subs(X3,'n374bernehmen$u1$u1')
& sub(X1,'name$u1$u1')
& prop(X0,'britisch$u$u1$u1')
& obj(X3,X0)
& attr(X4,X5)
& attr(X2,X1) ) ).
fof(negated_conjecture,negated_conjecture,
~ ? [X0,X1,X2,X3,X4,X5] :
( subs(X3,'n374bernehmen$u1$u1')
& sub(X1,'name$u1$u1')
& prop(X0,'britisch$u$u1$u1')
& obj(X3,X0)
& attr(X4,X5)
& attr(X2,X1) ),
inference(negate_conjecture,[status(cth)],[synth_qa07_007_mira_news_1319_a19984]) ).
cnf(c4,plain,
attr(c103,c104),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1319_a19984]) ).
cnf(c6,plain,
sub(c104,'name$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1319_a19984]) ).
cnf(c8,plain,
obj(c113,c117),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1319_a19984]) ).
cnf(c9,plain,
subs(c113,'annahme$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1319_a19984]) ).
cnf(c10,plain,
prop(c117,'britisch$u$u1$u1'),
inference(clausification,[status(esa)],[ave07_era5_synth_qa07_007_mira_news_1319_a19984]) ).
cnf(c277,plain,
( chea(sK87(X2,X0),X2)
| ~ subs(X2,X1)
| ~ chea(X0,X1) ),
inference(clausification,[status(esa)],[chea_subs_abs__event]) ).
cnf(c278,plain,
( subs(sK87(X2,X0),X0)
| ~ subs(X2,X1)
| ~ chea(X0,X1) ),
inference(clausification,[status(esa)],[chea_subs_abs__event]) ).
cnf(c282,plain,
( obj(X0,X2)
| ~ obj(X1,X2)
| ~ chea(X0,X1) ),
inference(clausification,[status(esa)],[chea_obj_abs__event]) ).
cnf(c326,plain,
chea('n374bernehmen$u1$u1','annahme$u1$u1'),
inference(clausification,[status(esa)],[fact_8354]) ).
cnf(c340,plain,
( ~ attr(X4,X5)
| ~ attr(X3,X1)
| ~ subs(X2,'n374bernehmen$u1$u1')
| ~ obj(X2,X0)
| ~ sub(X1,'name$u1$u1')
| ~ prop(X0,'britisch$u$u1$u1') ),
inference(clausification,[status(esa)],[negated_conjecture]) ).
cnf(d0,plain,
( ~ subs(X4,'n374bernehmen$u1$u1')
| ~ obj(X4,c117)
| ~ attr(X2,X3)
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[c10,c340]) ).
cnf(d1,plain,
( subs(sK87(X0,'n374bernehmen$u1$u1'),'n374bernehmen$u1$u1')
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[c278,c326]) ).
cnf(d2,plain,
( ~ obj(sK87(X0,'n374bernehmen$u1$u1'),c117)
| ~ attr(X4,X1)
| ~ attr(X2,X3)
| ~ sub(X1,'name$u1$u1')
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[d1,d0]) ).
cnf(d3,plain,
( chea(sK87(X0,'n374bernehmen$u1$u1'),X0)
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[c277,c326]) ).
cnf(d4,plain,
( ~ obj(X0,X1)
| obj(sK87(X0,'n374bernehmen$u1$u1'),X1)
| ~ subs(X0,'annahme$u1$u1') ),
inference(resolution,[status(thm)],[d3,c282]) ).
cnf(d5,plain,
( ~ subs(X0,'annahme$u1$u1')
| ~ attr(X3,X4)
| ~ attr(X2,X1)
| ~ sub(X1,'name$u1$u1')
| ~ subs(X0,'annahme$u1$u1')
| ~ obj(X0,c117) ),
inference(resolution,[status(thm)],[d4,d2]) ).
cnf(d6,plain,
( ~ obj(c113,c117)
| ~ attr(X3,X0)
| ~ attr(X1,X2)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[d5,c9]) ).
cnf(d7,plain,
( ~ attr(X2,X3)
| ~ attr(X1,X0)
| ~ sub(X0,'name$u1$u1') ),
inference(resolution,[status(thm)],[c8,d6]) ).
cnf(d8,plain,
( ~ attr(X0,X1)
| ~ sub(c104,'name$u1$u1') ),
inference(resolution,[status(thm)],[d7,c4]) ).
cnf(d9,plain,
~ attr(X0,X1),
inference(resolution,[status(thm)],[c6,d8]) ).
cnf(d10,plain,
$false,
inference(resolution,[status(thm)],[d9,c4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR115+59 : 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.07/0.34 % Computer : n020.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 27 01:11:04 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 62.80/9.65 % SZS status Theorem for theBenchmark.p
% 62.80/9.65 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------