%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+38 : 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 : n007.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:42 AM UTC 2026
% Result : Theorem 75.07s 10.79s
% Output : CNFRefutation 75.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+38 : 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.12/0.37 % Computer : n007.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 01:07:09 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 75.07/10.79 % SZS status Theorem for theBenchmark.p
% 75.07/10.79 % SZS output start CNFRefutation for theBenchmark.p
% 75.07/10.79 fof(ave07_era5_synth_qa07_007_mira_news_1233, hypothesis, (attr(c11,c12) & (sub(c11,'stadt$u$u1$u1') & (sub(c12,'name$u1$u1') & (val(c12,'m$u$u374nchen$u0') & (attr(c17,c18) & (attr(c17,c19) & (sub(c18,'tag$u1$u1') & (val(c18,c15) & (sub(c19,'monat$u1$u1') & (val(c19,c16) & (prop(c2226,c2204) & (pred(c2230,'maschinenfabrikant$u1$u1') & (prop(c2230,'britisch$u$u1$u1') & (attr(c2836,c2837) & (sub(c2836,'firma$u1$u1') & (sub(c2837,'name$u1$u1') & (val(c2837,'bmw$u0') & (attr(c2840,c2841) & (sub(c2840,'mensch$u1$u1') & (sub(c2841,'familiename$u1$u1') & (val(c2841,'roll$u0') & (sub(c2842,'gmbh$u$u1$u1') & (attr(c2844,c2845) & (sub(c2844,'mensch$u1$u1') & (sub(c2845,'familiename$u1$u1') & (val(c2845,'royce$u0') & (comp(c2868,'fix$u1$u2',c2206) & (tupl(c31,c11,c17) & ('tupl$up8'(c3436,c2226,c2230,c2836,c2840,c2844,c2842,c2868) & (chsp2('gr$u$u374nden$u1$u2',c2204) & (assoc('maschinenfabrikant$u1$u1','aggregat$u1$u1') & (sub('maschinenfabrikant$u1$u1','fabrikant$u1$u1') & (chsp2('planen$u1$u1',c2206) & (sort(c11,d) & (sort(c11,io) & (card(c11,int1) & (etype(c11,int0) & (fact(c11,real) & (gener(c11,sp) & (quant(c11,one) & (refer(c11,det) & (varia(c11,con) & (sort(c12,na) & (card(c12,int1) & (etype(c12,int0) & (fact(c12,real) & (gener(c12,sp) & (quant(c12,one) & (refer(c12,indet) & (varia(c12,'varia$uc') & (sort('stadt$u$u1$u1',d) & (sort('stadt$u$u1$u1',io) & (card('stadt$u$u1$u1',int1) & (etype('stadt$u$u1$u1',int0) & (fact('stadt$u$u1$u1',real) & (gener('stadt$u$u1$u1',ge) & (quant('stadt$u$u1$u1',one) & (refer('stadt$u$u1$u1','refer$uc') & (varia('stadt$u$u1$u1','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('m$u$u374nchen$u0',fe) & (sort(c17,t) & (card(c17,int1) & (etype(c17,int0) & (fact(c17,real) & (gener(c17,sp) & (quant(c17,one) & (refer(c17,det) & (varia(c17,con) & (sort(c18,me) & (sort(c18,oa) & (sort(c18,ta) & (card(c18,'card$uc') & (etype(c18,'etype$uc') & (fact(c18,real) & (gener(c18,sp) & (quant(c18,'quant$uc') & (refer(c18,'refer$uc') & (varia(c18,'varia$uc') & (sort(c19,me) & (sort(c19,oa) & (sort(c19,ta) & (card(c19,'card$uc') & (etype(c19,'etype$uc') & (fact(c19,real) & (gener(c19,sp) & (quant(c19,'quant$uc') & (refer(c19,'refer$uc') & (varia(c19,'varia$uc') & (sort('tag$u1$u1',me) & (sort('tag$u1$u1',oa) & (sort('tag$u1$u1',ta) & (card('tag$u1$u1','card$uc') & (etype('tag$u1$u1','etype$uc') & (fact('tag$u1$u1',real) & (gener('tag$u1$u1',ge) & (quant('tag$u1$u1','quant$uc') & (refer('tag$u1$u1','refer$uc') & (varia('tag$u1$u1','varia$uc') & (sort(c15,nu) & (card(c15,int3) & (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(c16,nu) & (card(c16,int5) & (sort(c2226,ab) & (card(c2226,int1990) & (etype(c2226,int1) & (fact(c2226,real) & (gener(c2226,'gener$uc') & (quant(c2226,nfquant) & (refer(c2226,'refer$uc') & (varia(c2226,'varia$uc') & (sort(c2204,tq) & (sort(c2230,d) & (sort(c2230,io) & (card(c2230,cons('x$uconstant',cons(int1,nil))) & (etype(c2230,int1) & (fact(c2230,real) & (gener(c2230,'gener$uc') & (quant(c2230,mult) & (refer(c2230,'refer$uc') & (varia(c2230,'varia$uc') & (sort('maschinenfabrikant$u1$u1',d) & (sort('maschinenfabrikant$u1$u1',io) & (card('maschinenfabrikant$u1$u1',int1) & (etype('maschinenfabrikant$u1$u1',int0) & (fact('maschinenfabrikant$u1$u1',real) & (gener('maschinenfabrikant$u1$u1',ge) & (quant('maschinenfabrikant$u1$u1',one) & (refer('maschinenfabrikant$u1$u1','refer$uc') & (varia('maschinenfabrikant$u1$u1','varia$uc') & (sort('britisch$u$u1$u1',nq) & (sort(c2836,d) & (sort(c2836,io) & (card(c2836,int1) & (etype(c2836,int0) & (fact(c2836,real) & (gener(c2836,sp) & (quant(c2836,one) & (refer(c2836,det) & (varia(c2836,con) & (sort(c2837,na) & (card(c2837,int1) & (etype(c2837,int0) & (fact(c2837,real) & (gener(c2837,sp) & (quant(c2837,one) & (refer(c2837,indet) & (varia(c2837,'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('bmw$u0',fe) & (sort(c2840,d) & (card(c2840,int1) & (etype(c2840,int0) & (fact(c2840,real) & (gener(c2840,sp) & (quant(c2840,one) & (refer(c2840,det) & (varia(c2840,con) & (sort(c2841,na) & (card(c2841,int1) & (etype(c2841,int0) & (fact(c2841,real) & (gener(c2841,sp) & (quant(c2841,one) & (refer(c2841,indet) & (varia(c2841,'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('roll$u0',fe) & (sort(c2842,d) & (sort(c2842,io) & (card(c2842,int1) & (etype(c2842,int1) & (fact(c2842,real) & (gener(c2842,'gener$uc') & (quant(c2842,one) & (refer(c2842,'refer$uc') & (varia(c2842,'varia$uc') & (sort('gmbh$u$u1$u1',d) & (sort('gmbh$u$u1$u1',io) & (card('gmbh$u$u1$u1','card$uc') & (etype('gmbh$u$u1$u1',int1) & (fact('gmbh$u$u1$u1',real) & (gener('gmbh$u$u1$u1',ge) & (quant('gmbh$u$u1$u1','quant$uc') & (refer('gmbh$u$u1$u1','refer$uc') & (varia('gmbh$u$u1$u1','varia$uc') & (sort(c2844,d) & (card(c2844,int1) & (etype(c2844,int0) & (fact(c2844,real) & (gener(c2844,sp) & (quant(c2844,one) & (refer(c2844,det) & (varia(c2844,con) & (sort(c2845,na) & (card(c2845,int1) & (etype(c2845,int0) & (fact(c2845,real) & (gener(c2845,sp) & (quant(c2845,one) & (refer(c2845,indet) & (varia(c2845,'varia$uc') & (sort('royce$u0',fe) & (sort(c2868,tq) & (sort('fix$u1$u2',mq) & (sort(c2206,tq) & (sort(c31,ent) & (card(c31,'card$uc') & (etype(c31,'etype$uc') & (fact(c31,real) & (gener(c31,'gener$uc') & (quant(c31,'quant$uc') & (refer(c31,'refer$uc') & (varia(c31,'varia$uc') & (sort(c3436,ent) & (card(c3436,'card$uc') & (etype(c3436,'etype$uc') & (fact(c3436,real) & (gener(c3436,'gener$uc') & (quant(c3436,'quant$uc') & (refer(c3436,'refer$uc') & (varia(c3436,'varia$uc') & (sort('gr$u$u374nden$u1$u2',da) & (fact('gr$u$u374nden$u1$u2',real) & (gener('gr$u$u374nden$u1$u2',ge) & (sort('aggregat$u1$u1',d) & (sort('aggregat$u1$u1',io) & (card('aggregat$u1$u1',int1) & (etype('aggregat$u1$u1',int0) & (fact('aggregat$u1$u1',real) & (gener('aggregat$u1$u1',ge) & (quant('aggregat$u1$u1',one) & (refer('aggregat$u1$u1','refer$uc') & (varia('aggregat$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') & (sort('planen$u1$u1',da) & (fact('planen$u1$u1',real) & gener('planen$u1$u1',ge))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 75.07/10.79 fof(member_first, axiom, ! [X0] : ! [X1] : member(X0,cons(X0,X1))).
% 75.07/10.79 fof(member_second, axiom, ! [X0] : ! [X1] : ! [X2] : ((member(X0,X2) => member(X0,cons(X1,X2))))).
% 75.07/10.79 fof(attr_name_hei__337en_1_1, axiom, ! [X0] : ! [X1] : ! [X2] : (((attr(X2,X0) & (member(X1,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) & sub(X0,X1))) => ? [X3] : ((arg1(X3,X2) & (arg2(X3,X2) & subs(X3,'hei$u$u337en$u1$u1'))))))).
% 75.07/10.79 fof(hei__337en_1_1__bezeichnen_1_1_als, axiom, ! [X0] : ! [X1] : ! [X2] : (((arg1(X0,X1) & (arg2(X0,X2) & subs(X0,'hei$u$u337en$u1$u1'))) => ? [X3] : ? [X4] : ((arg1(X4,X1) & (arg2(X4,X2) & (hsit(X0,X3) & (mcont(X3,X4) & (obj(X3,X1) & (subr(X4,'rprs$u0') & subs(X3,'bezeichnen$u1$u1'))))))))))).
% 75.07/10.79 fof(synth_qa07_007_mira_news_1233, conjecture, ? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ((attr(X0,X1) & (attr(X3,X2) & (attr(X5,X6) & (obj(X4,X0) & (sub(X1,'name$u1$u1') & (sub(X0,'firma$u1$u1') & (sub(X2,'name$u1$u1') & (val(X1,'bmw$u0') & val(X2,'bmw$u0'))))))))))).
% 75.07/10.79 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ((attr(X0,X1) & (attr(X3,X2) & (attr(X5,X6) & (obj(X4,X0) & (sub(X1,'name$u1$u1') & (sub(X0,'firma$u1$u1') & (sub(X2,'name$u1$u1') & (val(X1,'bmw$u0') & val(X2,'bmw$u0')))))))))), inference(negate_conjecture, [status(cth)], [synth_qa07_007_mira_news_1233])).
% 75.07/10.79 cnf(c0, plain, attr(c11,c12), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1233])).
% 75.07/10.79 cnf(c13, plain, attr(c2836,c2837), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1233])).
% 75.07/10.79 cnf(c14, plain, sub(c2836,'firma$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1233])).
% 75.07/10.79 cnf(c15, plain, sub(c2837,'name$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1233])).
% 75.07/10.79 cnf(c16, plain, val(c2837,'bmw$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1233])).
% 75.07/10.79 cnf(c286, plain, member(X0,cons(X0,X1)), inference(clausification, [status(esa)], [member_first])).
% 75.07/10.79 cnf(c287, plain, ~member(X0,X1) | member(X0,cons(X2,X1)), inference(clausification, [status(esa)], [member_second])).
% 75.07/10.79 cnf(c480, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | arg1(sK254(X0),X0), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 75.07/10.79 cnf(c481, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | arg2(sK254(X0),X0), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 75.07/10.79 cnf(c482, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | subs(sK254(X0),'hei$u$u337en$u1$u1'), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 75.07/10.79 cnf(c487, plain, ~arg1(X0,X1) | ~arg2(X0,X2) | ~subs(X0,'hei$u$u337en$u1$u1') | X3(X0,X1,X2), inference(clausification, [status(esa)], [hei__337en_1_1__bezeichnen_1_1_als])).
% 75.07/10.79 cnf(c492, plain, ~X0(X1,X2,X3) | obj(sK263(X1,X2,X3),X2), inference(clausification, [status(esa)], [hei__337en_1_1__bezeichnen_1_1_als])).
% 75.07/10.79 cnf(c558, plain, ~obj(X0,X1) | ~attr(X2,X3) | ~attr(X1,X4) | ~sub(X4,'name$u1$u1') | ~attr(X5,X6) | ~sub(X1,'firma$u1$u1') | ~sub(X6,'name$u1$u1') | ~val(X6,'bmw$u0') | ~val(X4,'bmw$u0'), inference(clausification, [status(esa)], [negated_conjecture])).
% 75.07/10.79 cnf(d0, plain, ~attr(X0,X1) | ~sub(X1,X2) | arg1(sK254(X0),X0) | ~member(X2,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c480,c287])).
% 75.07/10.79 cnf(d1, plain, ~attr(X0,X1) | ~sub(X1,X2) | arg1(sK254(X0),X0) | ~member(X2,cons('name$u1$u1',nil)), inference(resolution, [status(thm)], [d0,c287])).
% 75.07/10.79 cnf(d2, plain, ~attr(X0,X1) | ~sub(X1,'name$u1$u1') | arg1(sK254(X0),X0), inference(resolution, [status(thm)], [d1,c286])).
% 75.07/10.79 cnf(d3, plain, ~attr(X0,c2837) | arg1(sK254(X0),X0), inference(resolution, [status(thm)], [d2,c15])).
% 75.07/10.79 cnf(d4, plain, ~'Ts259'(X0,X1,X2) | ~attr(X3,X4) | ~attr(X1,X5) | ~attr(X6,X7) | ~sub(X5,'name$u1$u1') | ~sub(X1,'firma$u1$u1') | ~sub(X4,'name$u1$u1') | ~val(X5,'bmw$u0') | ~val(X4,'bmw$u0'), inference(resolution, [status(thm)], [c492,c558])).
% 75.07/10.79 cnf(d5, plain, ~attr(X0,X1) | ~attr(X2,X3) | ~attr(X4,X5) | ~sub(X5,'name$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'firma$u1$u1') | ~val(X5,'bmw$u0') | ~val(X3,'bmw$u0') | ~subs(X6,'hei$u$u337en$u1$u1') | ~arg1(X6,X4) | ~arg2(X6,X7), inference(resolution, [status(thm)], [d4,c487])).
% 75.07/10.79 cnf(d6, plain, ~attr(X0,X1) | ~sub(X1,X2) | arg2(sK254(X0),X0) | ~member(X2,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c481,c287])).
% 75.07/10.79 cnf(d7, plain, ~attr(X0,X1) | ~sub(X1,X2) | arg2(sK254(X0),X0) | ~member(X2,cons('name$u1$u1',nil)), inference(resolution, [status(thm)], [d6,c287])).
% 75.07/10.79 cnf(d8, plain, ~attr(X0,X1) | ~sub(X1,'name$u1$u1') | arg2(sK254(X0),X0), inference(resolution, [status(thm)], [d7,c286])).
% 75.07/10.79 cnf(d9, plain, ~attr(X0,c2837) | arg2(sK254(X0),X0), inference(resolution, [status(thm)], [d8,c15])).
% 75.07/10.79 cnf(d10, plain, ~attr(X0,c2837) | ~attr(X1,X2) | ~attr(X3,X4) | ~attr(X5,X6) | ~sub(X2,'name$u1$u1') | ~sub(X1,'firma$u1$u1') | ~sub(X4,'name$u1$u1') | ~val(X2,'bmw$u0') | ~val(X4,'bmw$u0') | ~subs(sK254(X0),'hei$u$u337en$u1$u1') | ~arg1(sK254(X0),X1), inference(resolution, [status(thm)], [d9,d5])).
% 75.07/10.79 cnf(d11, plain, ~attr(X0,X1) | ~attr(X2,X3) | ~attr(X4,X5) | ~attr(X4,c2837) | ~sub(X3,'name$u1$u1') | ~sub(X5,'name$u1$u1') | ~sub(X4,'firma$u1$u1') | ~val(X3,'bmw$u0') | ~val(X5,'bmw$u0') | ~subs(sK254(X4),'hei$u$u337en$u1$u1') | ~attr(X4,c2837), inference(resolution, [status(thm)], [d10,d3])).
% 75.07/10.79 cnf(d12, plain, ~attr(X0,X1) | ~sub(X1,X2) | subs(sK254(X0),'hei$u$u337en$u1$u1') | ~member(X2,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c482,c287])).
% 75.07/10.79 cnf(d13, plain, ~attr(X0,X1) | ~sub(X1,X2) | subs(sK254(X0),'hei$u$u337en$u1$u1') | ~member(X2,cons('name$u1$u1',nil)), inference(resolution, [status(thm)], [d12,c287])).
% 75.07/10.79 cnf(d14, plain, ~attr(X0,X1) | ~sub(X1,'name$u1$u1') | subs(sK254(X0),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [d13,c286])).
% 75.07/10.79 cnf(d15, plain, ~attr(X0,c2837) | subs(sK254(X0),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [d14,c15])).
% 75.07/10.79 cnf(d16, plain, ~attr(X0,c2837) | ~attr(X0,X1) | ~attr(X0,c2837) | ~attr(X2,X3) | ~attr(X4,X5) | ~sub(X1,'name$u1$u1') | ~sub(X0,'firma$u1$u1') | ~sub(X3,'name$u1$u1') | ~val(X1,'bmw$u0') | ~val(X3,'bmw$u0'), inference(resolution, [status(thm)], [d15,d11])).
% 75.07/10.79 cnf(d17, plain, ~attr(X0,X1) | ~attr(X2,X3) | ~attr(X4,c2837) | ~attr(X4,c2837) | ~sub(X3,'name$u1$u1') | ~sub(c2837,'name$u1$u1') | ~sub(X4,'firma$u1$u1') | ~val(X3,'bmw$u0'), inference(resolution, [status(thm)], [d16,c16])).
% 75.07/10.79 cnf(d18, plain, ~attr(X0,c2837) | ~attr(X1,X2) | ~attr(X3,X4) | ~sub(X0,'firma$u1$u1') | ~sub(X2,'name$u1$u1') | ~val(X2,'bmw$u0'), inference(resolution, [status(thm)], [c15,d17])).
% 75.07/10.79 cnf(d19, plain, ~attr(X0,X1) | ~attr(X2,c2837) | ~attr(X3,c2837) | ~sub(c2837,'name$u1$u1') | ~sub(X3,'firma$u1$u1'), inference(resolution, [status(thm)], [d18,c16])).
% 75.07/10.79 cnf(d20, plain, ~attr(X0,c2837) | ~attr(X1,c2837) | ~attr(X2,X3) | ~sub(X0,'firma$u1$u1'), inference(resolution, [status(thm)], [c15,d19])).
% 75.07/10.79 cnf(d21, plain, ~attr(X0,X1) | ~attr(X2,c2837) | ~attr(c2836,c2837), inference(resolution, [status(thm)], [d20,c14])).
% 75.07/10.79 cnf(d22, plain, ~attr(X0,c2837) | ~attr(X1,X2), inference(resolution, [status(thm)], [c13,d21])).
% 75.07/10.79 cnf(d23, plain, ~attr(X0,X1), inference(resolution, [status(thm)], [d22,c13])).
% 75.07/10.79 cnf(d24, plain, $false, inference(resolution, [status(thm)], [d23,c0])).
% 75.07/10.79 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------