%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+45 : 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 : n018.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:43 AM UTC 2026
% Result : Theorem 41.62s 10.72s
% Output : CNFRefutation 41.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+45 : 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.09/5.36 % Computer : n018.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Sun Sep 27 01:11:43 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.09/5.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 41.62/10.72 % SZS status Theorem for theBenchmark.p
% 41.62/10.72 % SZS output start CNFRefutation for theBenchmark.p
% 41.62/10.72 fof(ave07_era5_synth_qa07_007_mira_news_1256_a19984, hypothesis, (assoc('autofirma$u1$u1','auto$u$u1$u1') & (sub('autofirma$u1$u1','firma$u1$u1') & (agt(c484,c893) & (benf(c484,c858) & (obj(c484,c902) & (subs(c484,'nehmen$u1$u7') & (temp(c484,c865) & (attr(c858,c859) & (sub(c858,'firma$u1$u1') & (sub(c859,'name$u1$u1') & (val(c859,'bmw$u0') & (prop(c865,'pass$u$u351$u1$u1') & (sub(c865,'sommer$u$u1$u1') & (attr(c893,c894) & (sub(c893,'autofirma$u1$u1') & (sub(c894,'name$u1$u1') & (val(c894,'rover$u0') & (prop(c902,'britisch$u$u1$u1') & (prop(c902,'unabh$u$u344ngig$u1$u1') & (sub(c902,c904) & (pmod(c904,'letzt$u1$u1','massenhersteller$u1$u1') & (agt(c907,c902) & (subs(c907,'herstellen$u1$u1') & (assoc('massenhersteller$u1$u1','masse$u1$u1') & (sub('massenhersteller$u1$u1','fabrikant$u1$u1') & (sort('autofirma$u1$u1',d) & (sort('autofirma$u1$u1',io) & (card('autofirma$u1$u1',int1) & (etype('autofirma$u1$u1',int0) & (fact('autofirma$u1$u1',real) & (gener('autofirma$u1$u1',ge) & (quant('autofirma$u1$u1',one) & (refer('autofirma$u1$u1','refer$uc') & (varia('autofirma$u1$u1','varia$uc') & (sort('auto$u$u1$u1',d) & (card('auto$u$u1$u1',int1) & (etype('auto$u$u1$u1',int0) & (fact('auto$u$u1$u1',real) & (gener('auto$u$u1$u1',ge) & (quant('auto$u$u1$u1',one) & (refer('auto$u$u1$u1','refer$uc') & (varia('auto$u$u1$u1','varia$uc') & (sort('firma$u1$u1',d) & (sort('firma$u1$u1',io) & (card('firma$u1$u1',int1) & (etype('firma$u1$u1',int0) & (fact('firma$u1$u1',real) & (gener('firma$u1$u1',ge) & (quant('firma$u1$u1',one) & (refer('firma$u1$u1','refer$uc') & (varia('firma$u1$u1','varia$uc') & (sort(c484,da) & (fact(c484,real) & (gener(c484,sp) & (sort(c893,d) & (sort(c893,io) & (card(c893,int1) & (etype(c893,int0) & (fact(c893,real) & (gener(c893,sp) & (quant(c893,one) & (refer(c893,det) & (varia(c893,con) & (sort(c858,d) & (sort(c858,io) & (card(c858,int1) & (etype(c858,int0) & (fact(c858,real) & (gener(c858,sp) & (quant(c858,one) & (refer(c858,det) & (varia(c858,con) & (sort(c902,io) & (card(c902,int1) & (etype(c902,int0) & (fact(c902,real) & (gener(c902,sp) & (quant(c902,one) & (refer(c902,det) & (varia(c902,con) & (sort('nehmen$u1$u7',da) & (fact('nehmen$u1$u7',real) & (gener('nehmen$u1$u7',ge) & (sort(c865,ta) & (card(c865,int1) & (etype(c865,int0) & (fact(c865,real) & (gener(c865,sp) & (quant(c865,one) & (refer(c865,det) & (varia(c865,con) & (sort(c859,na) & (card(c859,int1) & (etype(c859,int0) & (fact(c859,real) & (gener(c859,sp) & (quant(c859,one) & (refer(c859,indet) & (varia(c859,'varia$uc') & (sort('name$u1$u1',na) & (card('name$u1$u1',int1) & (etype('name$u1$u1',int0) & (fact('name$u1$u1',real) & (gener('name$u1$u1',ge) & (quant('name$u1$u1',one) & (refer('name$u1$u1','refer$uc') & (varia('name$u1$u1','varia$uc') & (sort('bmw$u0',fe) & (sort('pass$u$u351$u1$u1',tq) & (sort('sommer$u$u1$u1',ta) & (card('sommer$u$u1$u1',int1) & (etype('sommer$u$u1$u1',int0) & (fact('sommer$u$u1$u1',real) & (gener('sommer$u$u1$u1',ge) & (quant('sommer$u$u1$u1',one) & (refer('sommer$u$u1$u1','refer$uc') & (varia('sommer$u$u1$u1','varia$uc') & (sort(c894,na) & (card(c894,int1) & (etype(c894,int0) & (fact(c894,real) & (gener(c894,sp) & (quant(c894,one) & (refer(c894,indet) & (varia(c894,'varia$uc') & (sort('rover$u0',fe) & (sort('britisch$u$u1$u1',nq) & (sort('unabh$u$u344ngig$u1$u1',nq) & (sort(c904,d) & (sort(c904,io) & (card(c904,int1) & (etype(c904,int0) & (fact(c904,real) & (gener(c904,ge) & (quant(c904,one) & (refer(c904,'refer$uc') & (varia(c904,'varia$uc') & (sort('letzt$u1$u1',oq) & (card('letzt$u1$u1','card$uc') & (sort('massenhersteller$u1$u1',d) & (sort('massenhersteller$u1$u1',io) & (card('massenhersteller$u1$u1',int1) & (etype('massenhersteller$u1$u1',int0) & (fact('massenhersteller$u1$u1',real) & (gener('massenhersteller$u1$u1',ge) & (quant('massenhersteller$u1$u1',one) & (refer('massenhersteller$u1$u1','refer$uc') & (varia('massenhersteller$u1$u1','varia$uc') & (sort(c907,da) & (fact(c907,real) & (gener(c907,sp) & (sort('herstellen$u1$u1',da) & (fact('herstellen$u1$u1',real) & (gener('herstellen$u1$u1',ge) & (sort('masse$u1$u1',io) & (card('masse$u1$u1','card$uc') & (etype('masse$u1$u1',int1) & (fact('masse$u1$u1',real) & (gener('masse$u1$u1',ge) & (quant('masse$u1$u1','quant$uc') & (refer('masse$u1$u1','refer$uc') & (varia('masse$u1$u1','varia$uc') & (sort('fabrikant$u1$u1',d) & (sort('fabrikant$u1$u1',io) & (card('fabrikant$u1$u1',int1) & (etype('fabrikant$u1$u1',int0) & (fact('fabrikant$u1$u1',real) & (gener('fabrikant$u1$u1',ge) & (quant('fabrikant$u1$u1',one) & (refer('fabrikant$u1$u1','refer$uc') & varia('fabrikant$u1$u1','varia$uc')))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 41.62/10.72 fof(sub__bezeichnen_1_1_als, axiom, ! [X0] : ! [X1] : ! [X2] : (((arg1(X0,X1) & (arg2(X0,X2) & subr(X0,'sub$u0'))) => ? [X3] : ? [X4] : ? [X5] : ((arg1(X4,X1) & (arg2(X4,X5) & (hsit(X0,X3) & (mcont(X3,X4) & (obj(X3,X1) & (sub(X5,X2) & (subr(X4,'rprs$u0') & subs(X3,'bezeichnen$u1$u1')))))))))))).
% 41.62/10.72 fof(sub__sub_0_expansion, axiom, ! [X0] : ! [X1] : ((sub(X0,X1) => ? [X2] : ((arg1(X2,X0) & (arg2(X2,X1) & subr(X2,'sub$u0'))))))).
% 41.62/10.72 fof(synth_qa07_007_mira_news_1256_a19984, conjecture, ? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ((attr(X2,X1) & (attr(X4,X5) & (obj(X3,X0) & (sub(X0,'firma$u1$u1') & (sub(X1,'name$u1$u1') & val(X1,'bmw$u0')))))))).
% 41.62/10.72 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ((attr(X2,X1) & (attr(X4,X5) & (obj(X3,X0) & (sub(X0,'firma$u1$u1') & (sub(X1,'name$u1$u1') & val(X1,'bmw$u0'))))))), inference(negate_conjecture, [status(cth)], [synth_qa07_007_mira_news_1256_a19984])).
% 41.62/10.72 cnf(c1, plain, sub('autofirma$u1$u1','firma$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1256_a19984])).
% 41.62/10.72 cnf(c7, plain, attr(c858,c859), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1256_a19984])).
% 41.62/10.72 cnf(c9, plain, sub(c859,'name$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1256_a19984])).
% 41.62/10.72 cnf(c10, plain, val(c859,'bmw$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1256_a19984])).
% 41.62/10.72 cnf(c481, plain, ~arg1(X0,X1) | ~arg2(X0,X2) | ~subr(X0,'sub$u0') | X3(X0,X1,X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 41.62/10.72 cnf(c486, plain, ~X0(X1,X2,X3) | obj(sK406(X1,X2,X3),X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 41.62/10.72 cnf(c490, plain, ~sub(X0,X1) | arg1(sK411(X0,X1),X0), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 41.62/10.72 cnf(c491, plain, ~sub(X0,X1) | arg2(sK411(X0,X1),X1), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 41.62/10.72 cnf(c492, plain, ~sub(X0,X1) | subr(sK411(X0,X1),'sub$u0'), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 41.62/10.72 cnf(c10542, plain, ~val(X0,'bmw$u0') | ~obj(X1,X2) | ~attr(X3,X4) | ~attr(X5,X0) | ~sub(X2,'firma$u1$u1') | ~sub(X0,'name$u1$u1'), inference(clausification, [status(esa)], [negated_conjecture])).
% 41.62/10.72 cnf(d0, plain, ~sub(X0,'firma$u1$u1') | ~sub(c859,'name$u1$u1') | ~obj(X1,X0) | ~attr(X2,X3) | ~attr(X4,c859), inference(resolution, [status(thm)], [c10,c10542])).
% 41.62/10.72 cnf(d1, plain, ~sub(X0,'firma$u1$u1') | ~obj(X1,X0) | ~attr(X2,c859) | ~attr(X3,X4), inference(resolution, [status(thm)], [c9,d0])).
% 41.62/10.72 cnf(d2, plain, ~sub(X0,'firma$u1$u1') | ~obj(X1,X0) | ~attr(X2,X3), inference(resolution, [status(thm)], [d1,c7])).
% 41.62/10.72 cnf(d3, plain, ~sub(X0,'firma$u1$u1') | ~obj(X1,X0), inference(resolution, [status(thm)], [d2,c7])).
% 41.62/10.72 cnf(d4, plain, ~'Ts402'(X0,X1,X2) | ~sub(X1,'firma$u1$u1'), inference(resolution, [status(thm)], [c486,d3])).
% 41.62/10.72 cnf(d5, plain, ~sub(X0,'firma$u1$u1') | ~arg1(X1,X0) | ~arg2(X1,X2) | ~subr(X1,'sub$u0'), inference(resolution, [status(thm)], [d4,c481])).
% 41.62/10.72 cnf(d6, plain, ~sub(X0,X1) | ~sub(X2,'firma$u1$u1') | ~arg1(sK411(X0,X1),X2) | ~arg2(sK411(X0,X1),X3), inference(resolution, [status(thm)], [c492,d5])).
% 41.62/10.72 cnf(d7, plain, ~sub(X0,'firma$u1$u1') | ~sub(X1,X2) | ~arg1(sK411(X1,X2),X0) | ~sub(X1,X2), inference(resolution, [status(thm)], [d6,c491])).
% 41.62/10.72 cnf(d8, plain, ~sub(X0,X1) | ~sub(X0,'firma$u1$u1') | ~sub(X0,X1), inference(resolution, [status(thm)], [d7,c490])).
% 41.62/10.72 cnf(d9, plain, ~sub('autofirma$u1$u1',X0), inference(resolution, [status(thm)], [d8,c1])).
% 41.62/10.72 cnf(d10, plain, $false, inference(resolution, [status(thm)], [d9,c1])).
% 41.62/10.72 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------