%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+17 : 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:40 AM UTC 2026
% Result : Theorem 80.01s 14.01s
% Output : CNFRefutation 80.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+17 : 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.11/0.36 % Computer : n020.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 01:08:19 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 80.01/14.01 % SZS status Theorem for theBenchmark.p
% 80.01/14.01 % SZS output start CNFRefutation for theBenchmark.p
% 80.01/14.01 fof(ave07_era5_synth_qa07_007_mira_news_1127, hypothesis, (sub(c142,'bmw$u1$u1') & (sub(c147,'kurs$u1$u1') & (subs(c159,'einstieg$u1$u1') & ('tupl$up6'(c1612,c142,c147,c159,c175,c185) & (attr(c175,c176) & (prop(c175,'britisch$u$u1$u1') & (sub(c175,'gruppe$u1$u1') & (sub(c176,'familiename$u1$u1') & (val(c176,'rover$u0') & (attr(c185,c186) & (attr(c185,c187) & (sub(c186,'monat$u1$u1') & (val(c186,c184) & (sub(c187,'jahr$u$u1$u1') & (val(c187,c183) & (prop(c4,'aktuell$u1$u1') & (sub(c4,'kurswert$u1$u1') & (assoc(c42,c7) & (exp(c42,c4) & (obj(c42,c47) & (subs(c42,'beiliegen$u1$u1') & ('quant$up3'(c47,c43,'mark$u1$u1') & (sub(c7,'aktie$u1$u1') & (assoc('kurswert$u1$u1','kurs$u1$u1') & (sub('kurswert$u1$u1','wert$u1$u1') & (sort(c142,d) & (card(c142,int1) & (etype(c142,int0) & (fact(c142,real) & (gener(c142,sp) & (quant(c142,one) & (refer(c142,det) & (varia(c142,con) & (sort('bmw$u1$u1',d) & (card('bmw$u1$u1',int1) & (etype('bmw$u1$u1',int0) & (fact('bmw$u1$u1',real) & (gener('bmw$u1$u1',ge) & (quant('bmw$u1$u1',one) & (refer('bmw$u1$u1','refer$uc') & (varia('bmw$u1$u1','varia$uc') & (sort(c147,ad) & (sort(c147,d) & (sort(c147,io) & (card(c147,int1) & (etype(c147,int0) & (fact(c147,real) & (gener(c147,'gener$uc') & (quant(c147,one) & (refer(c147,'refer$uc') & (varia(c147,'varia$uc') & (sort('kurs$u1$u1',ad) & (sort('kurs$u1$u1',d) & (sort('kurs$u1$u1',io) & (card('kurs$u1$u1',int1) & (etype('kurs$u1$u1',int0) & (fact('kurs$u1$u1',real) & (gener('kurs$u1$u1',ge) & (quant('kurs$u1$u1',one) & (refer('kurs$u1$u1','refer$uc') & (varia('kurs$u1$u1','varia$uc') & (sort(c159,ad) & (card(c159,int1) & (etype(c159,int0) & (fact(c159,real) & (gener(c159,sp) & (quant(c159,one) & (refer(c159,det) & (varia(c159,con) & (sort('einstieg$u1$u1',ad) & (card('einstieg$u1$u1',int1) & (etype('einstieg$u1$u1',int0) & (fact('einstieg$u1$u1',real) & (gener('einstieg$u1$u1',ge) & (quant('einstieg$u1$u1',one) & (refer('einstieg$u1$u1','refer$uc') & (varia('einstieg$u1$u1','varia$uc') & (sort(c1612,ent) & (card(c1612,'card$uc') & (etype(c1612,'etype$uc') & (fact(c1612,real) & (gener(c1612,'gener$uc') & (quant(c1612,'quant$uc') & (refer(c1612,'refer$uc') & (varia(c1612,'varia$uc') & (sort(c175,d) & (card(c175,int1) & (etype(c175,int1) & (fact(c175,real) & (gener(c175,sp) & (quant(c175,one) & (refer(c175,det) & (varia(c175,'varia$uc') & (sort(c185,t) & (card(c185,int1) & (etype(c185,int0) & (fact(c185,real) & (gener(c185,sp) & (quant(c185,one) & (refer(c185,det) & (varia(c185,con) & (sort(c176,na) & (card(c176,int1) & (etype(c176,int0) & (fact(c176,real) & (gener(c176,sp) & (quant(c176,one) & (refer(c176,det) & (varia(c176,'varia$uc') & (sort('britisch$u$u1$u1',nq) & (sort('gruppe$u1$u1',d) & (card('gruppe$u1$u1','card$uc') & (etype('gruppe$u1$u1',int1) & (fact('gruppe$u1$u1',real) & (gener('gruppe$u1$u1',ge) & (quant('gruppe$u1$u1','quant$uc') & (refer('gruppe$u1$u1','refer$uc') & (varia('gruppe$u1$u1','varia$uc') & (sort('familiename$u1$u1',na) & (card('familiename$u1$u1',int1) & (etype('familiename$u1$u1',int0) & (fact('familiename$u1$u1',real) & (gener('familiename$u1$u1',ge) & (quant('familiename$u1$u1',one) & (refer('familiename$u1$u1','refer$uc') & (varia('familiename$u1$u1','varia$uc') & (sort('rover$u0',fe) & (sort(c186,me) & (sort(c186,oa) & (sort(c186,ta) & (card(c186,'card$uc') & (etype(c186,'etype$uc') & (fact(c186,real) & (gener(c186,sp) & (quant(c186,'quant$uc') & (refer(c186,'refer$uc') & (varia(c186,'varia$uc') & (sort(c187,me) & (sort(c187,oa) & (sort(c187,ta) & (card(c187,'card$uc') & (etype(c187,'etype$uc') & (fact(c187,real) & (gener(c187,sp) & (quant(c187,'quant$uc') & (refer(c187,'refer$uc') & (varia(c187,'varia$uc') & (sort('monat$u1$u1',me) & (sort('monat$u1$u1',oa) & (sort('monat$u1$u1',ta) & (card('monat$u1$u1','card$uc') & (etype('monat$u1$u1','etype$uc') & (fact('monat$u1$u1',real) & (gener('monat$u1$u1',ge) & (quant('monat$u1$u1','quant$uc') & (refer('monat$u1$u1','refer$uc') & (varia('monat$u1$u1','varia$uc') & (sort(c184,nu) & (card(c184,int1) & (sort('jahr$u$u1$u1',me) & (sort('jahr$u$u1$u1',oa) & (sort('jahr$u$u1$u1',ta) & (card('jahr$u$u1$u1','card$uc') & (etype('jahr$u$u1$u1','etype$uc') & (fact('jahr$u$u1$u1',real) & (gener('jahr$u$u1$u1',ge) & (quant('jahr$u$u1$u1','quant$uc') & (refer('jahr$u$u1$u1','refer$uc') & (varia('jahr$u$u1$u1','varia$uc') & (sort(c183,nu) & (card(c183,int1994) & (sort(c4,io) & (sort(c4,oa) & (card(c4,int1) & (etype(c4,int0) & (fact(c4,real) & (gener(c4,sp) & (quant(c4,one) & (refer(c4,det) & (varia(c4,con) & (sort('aktuell$u1$u1',nq) & (sort('kurswert$u1$u1',io) & (sort('kurswert$u1$u1',oa) & (card('kurswert$u1$u1',int1) & (etype('kurswert$u1$u1',int0) & (fact('kurswert$u1$u1',real) & (gener('kurswert$u1$u1',ge) & (quant('kurswert$u1$u1',one) & (refer('kurswert$u1$u1','refer$uc') & (varia('kurswert$u1$u1','varia$uc') & (sort(c42,dn) & (fact(c42,real) & (gener(c42,sp) & (sort(c7,d) & (sort(c7,io) & (card(c7,int1) & (etype(c7,int0) & (fact(c7,real) & (gener(c7,'gener$uc') & (quant(c7,one) & (refer(c7,'refer$uc') & (varia(c7,'varia$uc') & (sort(c47,co) & (sort(c47,m) & (card(c47,'card$uc') & (etype(c47,'etype$uc') & (fact(c47,real) & (gener(c47,sp) & (quant(c47,'quant$uc') & (refer(c47,'refer$uc') & (varia(c47,con) & (sort('beiliegen$u1$u1',dn) & (fact('beiliegen$u1$u1',real) & (gener('beiliegen$u1$u1',ge) & (sort(c43,nu) & (card(c43,int768) & (sort('mark$u1$u1',me) & (gener('mark$u1$u1',ge) & (sort('aktie$u1$u1',d) & (sort('aktie$u1$u1',io) & (card('aktie$u1$u1',int1) & (etype('aktie$u1$u1',int0) & (fact('aktie$u1$u1',real) & (gener('aktie$u1$u1',ge) & (quant('aktie$u1$u1',one) & (refer('aktie$u1$u1','refer$uc') & (varia('aktie$u1$u1','varia$uc') & (sort('wert$u1$u1',io) & (sort('wert$u1$u1',oa) & (card('wert$u1$u1',int1) & (etype('wert$u1$u1',int0) & (fact('wert$u1$u1',real) & (gener('wert$u1$u1',ge) & (quant('wert$u1$u1',one) & (refer('wert$u1$u1','refer$uc') & varia('wert$u1$u1','varia$uc'))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 80.01/14.01 fof(state_adjective__in_state, axiom, ! [X0] : ! [X1] : ! [X2] : (((prop(X0,X1) & 'state$uadjective$ustate$ubinding'(X1,X2)) => ? [X3] : ? [X4] : ? [X5] : ((in(X5,X3) & (attr(X3,X4) & (loc(X0,X5) & (sub(X3,'land$u1$u1') & (sub(X4,'name$u1$u1') & val(X4,X2)))))))))).
% 80.01/14.01 fof(fact_8846, axiom, 'state$uadjective$ustate$ubinding'('britisch$u$u1$u1','grossbritannien$u0')).
% 80.01/14.01 fof(synth_qa07_007_mira_news_1127, conjecture, ? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ((attr(X0,X1) & (attr(X3,X2) & (attr(X4,X5) & (sub(X1,'name$u1$u1') & sub(X2,'name$u1$u1'))))))).
% 80.01/14.01 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ((attr(X0,X1) & (attr(X3,X2) & (attr(X4,X5) & (sub(X1,'name$u1$u1') & sub(X2,'name$u1$u1')))))), inference(negate_conjecture, [status(cth)], [synth_qa07_007_mira_news_1127])).
% 80.01/14.01 cnf(c2, plain, attr(c175,c176), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1127])).
% 80.01/14.01 cnf(c233, plain, prop(c175,'britisch$u$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1127])).
% 80.01/14.01 cnf(c444, plain, ~'state$uadjective$ustate$ubinding'(X0,X1) | ~prop(X2,X0) | X3(X2,X1), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 80.01/14.01 cnf(c447, plain, ~X0(X1,X2) | sub(sK264(X1,X2),'name$u1$u1'), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 80.01/14.01 cnf(c450, plain, ~X0(X1,X2) | attr(sK263(X1,X2),sK264(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 80.01/14.01 cnf(c555, plain, 'state$uadjective$ustate$ubinding'('britisch$u$u1$u1','grossbritannien$u0'), inference(clausification, [status(esa)], [fact_8846])).
% 80.01/14.01 cnf(c565, plain, ~attr(X0,X1) | ~attr(X2,X3) | ~sub(X1,'name$u1$u1') | ~sub(X4,'name$u1$u1') | ~attr(X5,X4), inference(clausification, [status(esa)], [negated_conjecture])).
% 80.01/14.01 cnf(d0, plain, ~prop(X0,'britisch$u$u1$u1') | 'Ts259'(X0,'grossbritannien$u0'), inference(resolution, [status(thm)], [c444,c555])).
% 80.01/14.01 cnf(d1, plain, 'Ts259'(c175,'grossbritannien$u0'), inference(resolution, [status(thm)], [d0,c233])).
% 80.01/14.01 cnf(d2, plain, ~sub(X0,'name$u1$u1') | ~sub(X1,'name$u1$u1') | ~attr(X2,X0) | ~attr(X3,X1), inference(resolution, [status(thm)], [c2,c565])).
% 80.01/14.01 cnf(d3, plain, ~'Ts259'(X0,X1) | ~sub(X2,'name$u1$u1') | ~sub(sK264(X0,X1),'name$u1$u1') | ~attr(X3,X2), inference(resolution, [status(thm)], [c450,d2])).
% 80.01/14.01 cnf(d4, plain, ~sub(X0,'name$u1$u1') | ~attr(X1,X0) | ~'Ts259'(X2,X3) | ~'Ts259'(X2,X3), inference(resolution, [status(thm)], [d3,c447])).
% 80.01/14.01 cnf(d5, plain, ~sub(X0,'name$u1$u1') | ~attr(X1,X0), inference(resolution, [status(thm)], [d1,d4])).
% 80.01/14.01 cnf(d6, plain, ~sub(sK264(X0,X1),'name$u1$u1') | ~'Ts259'(X0,X1), inference(resolution, [status(thm)], [d5,c450])).
% 80.01/14.01 cnf(d7, plain, ~'Ts259'(X0,X1) | ~'Ts259'(X0,X1), inference(resolution, [status(thm)], [d6,c447])).
% 80.01/14.01 cnf(d8, plain, $false, inference(resolution, [status(thm)], [d7,d1])).
% 80.01/14.01 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------