%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+65 : 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 : n019.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:46 AM UTC 2026
% Result : Theorem 42.54s 5.66s
% Output : CNFRefutation 42.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR115+65 : 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.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 01:10:49 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 42.54/5.66 % SZS status Theorem for theBenchmark.p
% 42.54/5.66 % SZS output start CNFRefutation for theBenchmark.p
% 42.54/5.66 fof(ave07_era5_synth_qa07_007_mira_wp_474, hypothesis, (sub(c34818,'limousine$u1$u1') & (pred(c34823,'einla$u$u337$u1$u1') & (pred(c34837,'einla$u$u337$u1$u1') & (sub(c34846,'cabrio$u$u1$u1') & (sub(c34855,'roadster$u1$u1') & (sub(c34864,'kombi$u$u1$u1') & (sub(c34881,'cabriovariante$u1$u1') & (sub(c34888,'artefakt$u1$u1') & (sub(c34895,'bmw$u1$u1') & (pred(c34906,'e30$u1$u1') & (prop(c34914,'klein$u1$u1') & (sub(c34914,'st$u$u374ckzahl$u1$u1') & (sub(c34920,'firma$u1$u1') & (attr(c34925,c34926) & (sub(c34925,'mensch$u1$u1') & (sub(c34926,'familiename$u1$u1') & (val(c34926,'baur$u0') & (sub(c34937,'bmw$u1$u1') & (sub(c34941,'h$u$u344ndlernetz$u1$u1') & ('tupl$up17'(c34978,c34818,c34823,c34837,c34846,c34855,c34864,c34881,c34888,c34895,c34906,c34914,c34920,c34925,c34846,c34937,c34941) & (assoc('cabriovariante$u1$u1','cabrio$u$u1$u1') & (sub('cabriovariante$u1$u1','spielart$u1$u1') & (assoc('h$u$u344ndlernetz$u1$u1','anbieter$u1$u1') & (sub('h$u$u344ndlernetz$u1$u1','netz$u1$u1') & (assoc('st$u$u374ckzahl$u1$u1','st$u$u374ck$u2$u1') & (sub('st$u$u374ckzahl$u1$u1','zahl$u1$u1') & (sort(c34818,d) & (card(c34818,int1) & (etype(c34818,int0) & (fact(c34818,real) & (gener(c34818,'gener$uc') & (quant(c34818,one) & (refer(c34818,'refer$uc') & (varia(c34818,'varia$uc') & (sort('limousine$u1$u1',d) & (card('limousine$u1$u1',int1) & (etype('limousine$u1$u1',int0) & (fact('limousine$u1$u1',real) & (gener('limousine$u1$u1',ge) & (quant('limousine$u1$u1',one) & (refer('limousine$u1$u1','refer$uc') & (varia('limousine$u1$u1','varia$uc') & (sort(c34823,d) & (card(c34823,int2) & (etype(c34823,int1) & (fact(c34823,real) & (gener(c34823,'gener$uc') & (quant(c34823,nfquant) & (refer(c34823,'refer$uc') & (varia(c34823,'varia$uc') & (sort('einla$u$u337$u1$u1',d) & (card('einla$u$u337$u1$u1',int1) & (etype('einla$u$u337$u1$u1',int0) & (fact('einla$u$u337$u1$u1',real) & (gener('einla$u$u337$u1$u1',ge) & (quant('einla$u$u337$u1$u1',one) & (refer('einla$u$u337$u1$u1','refer$uc') & (varia('einla$u$u337$u1$u1','varia$uc') & (sort(c34837,d) & (card(c34837,int4) & (etype(c34837,int1) & (fact(c34837,real) & (gener(c34837,'gener$uc') & (quant(c34837,nfquant) & (refer(c34837,'refer$uc') & (varia(c34837,'varia$uc') & (sort(c34846,d) & (card(c34846,int1) & (etype(c34846,int0) & (fact(c34846,real) & (gener(c34846,'gener$uc') & (quant(c34846,one) & (refer(c34846,'refer$uc') & (varia(c34846,'varia$uc') & (sort('cabrio$u$u1$u1',d) & (card('cabrio$u$u1$u1',int1) & (etype('cabrio$u$u1$u1',int0) & (fact('cabrio$u$u1$u1',real) & (gener('cabrio$u$u1$u1',ge) & (quant('cabrio$u$u1$u1',one) & (refer('cabrio$u$u1$u1','refer$uc') & (varia('cabrio$u$u1$u1','varia$uc') & (sort(c34855,d) & (card(c34855,int1) & (etype(c34855,int0) & (fact(c34855,real) & (gener(c34855,'gener$uc') & (quant(c34855,one) & (refer(c34855,'refer$uc') & (varia(c34855,'varia$uc') & (sort('roadster$u1$u1',d) & (card('roadster$u1$u1',int1) & (etype('roadster$u1$u1',int0) & (fact('roadster$u1$u1',real) & (gener('roadster$u1$u1',ge) & (quant('roadster$u1$u1',one) & (refer('roadster$u1$u1','refer$uc') & (varia('roadster$u1$u1','varia$uc') & (sort(c34864,d) & (card(c34864,int1) & (etype(c34864,int0) & (fact(c34864,real) & (gener(c34864,'gener$uc') & (quant(c34864,one) & (refer(c34864,'refer$uc') & (varia(c34864,'varia$uc') & (sort('kombi$u$u1$u1',d) & (card('kombi$u$u1$u1',int1) & (etype('kombi$u$u1$u1',int0) & (fact('kombi$u$u1$u1',real) & (gener('kombi$u$u1$u1',ge) & (quant('kombi$u$u1$u1',one) & (refer('kombi$u$u1$u1','refer$uc') & (varia('kombi$u$u1$u1','varia$uc') & (sort(c34881,io) & (sort(c34881,re) & (card(c34881,int1) & (etype(c34881,int0) & (fact(c34881,real) & (gener(c34881,sp) & (quant(c34881,one) & (refer(c34881,det) & (varia(c34881,con) & (sort('cabriovariante$u1$u1',io) & (sort('cabriovariante$u1$u1',re) & (card('cabriovariante$u1$u1',int1) & (etype('cabriovariante$u1$u1',int0) & (fact('cabriovariante$u1$u1',real) & (gener('cabriovariante$u1$u1',ge) & (quant('cabriovariante$u1$u1',one) & (refer('cabriovariante$u1$u1','refer$uc') & (varia('cabriovariante$u1$u1','varia$uc') & (sort(c34888,d) & (sort(c34888,io) & (card(c34888,int1) & (etype(c34888,int0) & (fact(c34888,real) & (gener(c34888,'gener$uc') & (quant(c34888,one) & (refer(c34888,'refer$uc') & (varia(c34888,'varia$uc') & (sort('artefakt$u1$u1',d) & (sort('artefakt$u1$u1',io) & (card('artefakt$u1$u1',int1) & (etype('artefakt$u1$u1',int0) & (fact('artefakt$u1$u1',real) & (gener('artefakt$u1$u1',ge) & (quant('artefakt$u1$u1',one) & (refer('artefakt$u1$u1','refer$uc') & (varia('artefakt$u1$u1','varia$uc') & (sort(c34895,d) & (card(c34895,int1) & (etype(c34895,int0) & (fact(c34895,real) & (gener(c34895,sp) & (quant(c34895,one) & (refer(c34895,det) & (varia(c34895,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(c34906,o) & (card(c34906,cons('x$uconstant',cons(int1,nil))) & (etype(c34906,int1) & (fact(c34906,real) & (gener(c34906,'gener$uc') & (quant(c34906,mult) & (refer(c34906,indet) & (varia(c34906,'varia$uc') & (sort('e30$u1$u1',o) & (card('e30$u1$u1',int1) & (etype('e30$u1$u1',int0) & (fact('e30$u1$u1',real) & (gener('e30$u1$u1',ge) & (quant('e30$u1$u1',one) & (refer('e30$u1$u1','refer$uc') & (varia('e30$u1$u1','varia$uc') & (sort(c34914,io) & (sort(c34914,oa) & (card(c34914,int1) & (etype(c34914,int0) & (fact(c34914,real) & (gener(c34914,'gener$uc') & (quant(c34914,one) & (refer(c34914,'refer$uc') & (varia(c34914,'varia$uc') & (sort('klein$u1$u1',mq) & (sort('st$u$u374ckzahl$u1$u1',io) & (sort('st$u$u374ckzahl$u1$u1',oa) & (card('st$u$u374ckzahl$u1$u1',int1) & (etype('st$u$u374ckzahl$u1$u1',int0) & (fact('st$u$u374ckzahl$u1$u1',real) & (gener('st$u$u374ckzahl$u1$u1',ge) & (quant('st$u$u374ckzahl$u1$u1',one) & (refer('st$u$u374ckzahl$u1$u1','refer$uc') & (varia('st$u$u374ckzahl$u1$u1','varia$uc') & (sort(c34920,d) & (sort(c34920,io) & (card(c34920,int1) & (etype(c34920,int0) & (fact(c34920,real) & (gener(c34920,sp) & (quant(c34920,one) & (refer(c34920,det) & (varia(c34920,con) & (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(c34925,d) & (card(c34925,int1) & (etype(c34925,int0) & (fact(c34925,real) & (gener(c34925,sp) & (quant(c34925,one) & (refer(c34925,det) & (varia(c34925,con) & (sort(c34926,na) & (card(c34926,int1) & (etype(c34926,int0) & (fact(c34926,real) & (gener(c34926,sp) & (quant(c34926,one) & (refer(c34926,indet) & (varia(c34926,'varia$uc') & (sort('mensch$u1$u1',d) & (card('mensch$u1$u1',int1) & (etype('mensch$u1$u1',int0) & (fact('mensch$u1$u1',real) & (gener('mensch$u1$u1',ge) & (quant('mensch$u1$u1',one) & (refer('mensch$u1$u1','refer$uc') & (varia('mensch$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('baur$u0',fe) & (sort(c34937,d) & (card(c34937,int1) & (etype(c34937,int0) & (fact(c34937,real) & (gener(c34937,sp) & (quant(c34937,one) & (refer(c34937,det) & (varia(c34937,con) & (sort(c34941,d) & (card(c34941,int1) & (etype(c34941,int0) & (fact(c34941,real) & (gener(c34941,'gener$uc') & (quant(c34941,one) & (refer(c34941,'refer$uc') & (varia(c34941,'varia$uc') & (sort('h$u$u344ndlernetz$u1$u1',d) & (card('h$u$u344ndlernetz$u1$u1',int1) & (etype('h$u$u344ndlernetz$u1$u1',int0) & (fact('h$u$u344ndlernetz$u1$u1',real) & (gener('h$u$u344ndlernetz$u1$u1',ge) & (quant('h$u$u344ndlernetz$u1$u1',one) & (refer('h$u$u344ndlernetz$u1$u1','refer$uc') & (varia('h$u$u344ndlernetz$u1$u1','varia$uc') & (sort(c34978,ent) & (card(c34978,'card$uc') & (etype(c34978,'etype$uc') & (fact(c34978,real) & (gener(c34978,'gener$uc') & (quant(c34978,'quant$uc') & (refer(c34978,'refer$uc') & (varia(c34978,'varia$uc') & (sort('spielart$u1$u1',io) & (sort('spielart$u1$u1',re) & (card('spielart$u1$u1',int1) & (etype('spielart$u1$u1',int0) & (fact('spielart$u1$u1',real) & (gener('spielart$u1$u1',ge) & (quant('spielart$u1$u1',one) & (refer('spielart$u1$u1','refer$uc') & (varia('spielart$u1$u1','varia$uc') & (sort('anbieter$u1$u1',d) & (sort('anbieter$u1$u1',io) & (card('anbieter$u1$u1',int1) & (etype('anbieter$u1$u1',int0) & (fact('anbieter$u1$u1',real) & (gener('anbieter$u1$u1',ge) & (quant('anbieter$u1$u1',one) & (refer('anbieter$u1$u1','refer$uc') & (varia('anbieter$u1$u1','varia$uc') & (sort('netz$u1$u1',d) & (card('netz$u1$u1',int1) & (etype('netz$u1$u1',int0) & (fact('netz$u1$u1',real) & (gener('netz$u1$u1',ge) & (quant('netz$u1$u1',one) & (refer('netz$u1$u1','refer$uc') & (varia('netz$u1$u1','varia$uc') & (sort('st$u$u374ck$u2$u1',d) & (sort('st$u$u374ck$u2$u1',io) & (card('st$u$u374ck$u2$u1',int1) & (etype('st$u$u374ck$u2$u1',int0) & (fact('st$u$u374ck$u2$u1',real) & (gener('st$u$u374ck$u2$u1',ge) & (quant('st$u$u374ck$u2$u1',one) & (refer('st$u$u374ck$u2$u1','refer$uc') & (varia('st$u$u374ck$u2$u1','varia$uc') & (sort('zahl$u1$u1',io) & (sort('zahl$u1$u1',oa) & (card('zahl$u1$u1',int1) & (etype('zahl$u1$u1',int0) & (fact('zahl$u1$u1',real) & (gener('zahl$u1$u1',ge) & (quant('zahl$u1$u1',one) & (refer('zahl$u1$u1','refer$uc') & varia('zahl$u1$u1','varia$uc'))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 42.54/5.66 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')))))))))))).
% 42.54/5.66 fof(sub__sub_0_expansion, axiom, ! [X0] : ! [X1] : ((sub(X0,X1) => ? [X2] : ((arg1(X2,X0) & (arg2(X2,X1) & subr(X2,'sub$u0'))))))).
% 42.54/5.66 fof(synth_qa07_007_mira_wp_474, conjecture, ? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ((attr(X0,X1) & (attr(X3,X2) & (attr(X5,X6) & obj(X4,X0)))))).
% 42.54/5.66 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ((attr(X0,X1) & (attr(X3,X2) & (attr(X5,X6) & obj(X4,X0))))), inference(negate_conjecture, [status(cth)], [synth_qa07_007_mira_wp_474])).
% 42.54/5.66 cnf(c13, plain, attr(c34925,c34926), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_474])).
% 42.54/5.66 cnf(c14, plain, sub(c34925,'mensch$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_474])).
% 42.54/5.66 cnf(c638, plain, ~arg1(X0,X1) | ~arg2(X0,X2) | ~subr(X0,'sub$u0') | X3(X0,X1,X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 42.54/5.66 cnf(c643, plain, ~X0(X1,X2,X3) | obj(sK406(X1,X2,X3),X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 42.54/5.66 cnf(c647, plain, ~sub(X0,X1) | arg1(sK411(X0,X1),X0), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 42.54/5.66 cnf(c648, plain, ~sub(X0,X1) | arg2(sK411(X0,X1),X1), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 42.54/5.66 cnf(c649, plain, ~sub(X0,X1) | subr(sK411(X0,X1),'sub$u0'), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 42.54/5.66 cnf(c10699, plain, ~attr(X0,X1) | ~attr(X2,X3) | ~attr(X4,X5) | ~obj(X6,X0), inference(clausification, [status(esa)], [negated_conjecture])).
% 42.54/5.66 cnf(d0, plain, ~'Ts402'(X0,X1,X2) | ~attr(X3,X4) | ~attr(X5,X6) | ~attr(X1,X7), inference(resolution, [status(thm)], [c643,c10699])).
% 42.54/5.66 cnf(d1, plain, ~attr(X0,X1) | ~attr(X2,X3) | ~attr(X4,X5) | ~arg1(X6,X4) | ~arg2(X6,X7) | ~subr(X6,'sub$u0'), inference(resolution, [status(thm)], [d0,c638])).
% 42.54/5.66 cnf(d2, plain, ~sub(X0,X1) | ~attr(X2,X3) | ~attr(X4,X5) | ~attr(X6,X7) | ~arg1(sK411(X0,X1),X2) | ~arg2(sK411(X0,X1),X8), inference(resolution, [status(thm)], [c649,d1])).
% 42.54/5.67 cnf(d3, plain, ~sub(X0,X1) | ~attr(X2,X3) | ~attr(X4,X5) | ~attr(X6,X7) | ~arg1(sK411(X0,X1),X6) | ~sub(X0,X1), inference(resolution, [status(thm)], [d2,c648])).
% 42.54/5.67 cnf(d4, plain, ~sub(X0,X1) | ~attr(X0,X2) | ~attr(X3,X4) | ~attr(X5,X6) | ~sub(X0,X1), inference(resolution, [status(thm)], [d3,c647])).
% 42.54/5.67 cnf(d5, plain, ~sub(c34925,X0) | ~attr(X1,X2) | ~attr(X3,X4), inference(resolution, [status(thm)], [d4,c13])).
% 42.54/5.67 cnf(d6, plain, ~sub(c34925,X0) | ~attr(X1,X2), inference(resolution, [status(thm)], [d5,c13])).
% 42.54/5.67 cnf(d7, plain, ~sub(c34925,X0), inference(resolution, [status(thm)], [d6,c13])).
% 42.54/5.67 cnf(d8, plain, $false, inference(resolution, [status(thm)], [d7,c14])).
% 42.54/5.67 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------