%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+20 : 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 : n013.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 72.80s 11.52s
% Output : CNFRefutation 72.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR115+20 : 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/0.36 % Computer : n013.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:07:06 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 72.80/11.52 % SZS status Theorem for theBenchmark.p
% 72.80/11.52 % SZS output start CNFRefutation for theBenchmark.p
% 72.80/11.52 fof(ave07_era5_synth_qa07_007_mira_news_1142, hypothesis, (assoc('aggregat$u1$u1','ableger$u1$u1') & (sub('aggregat$u1$u1','werk$u1$u2') & (attr(c1158,c1159) & (sub(c1158,'firma$u1$u1') & (sub(c1159,'name$u1$u1') & (val(c1159,'bmw$u0') & (attr(c1162,c1163) & (sub(c1162,'mensch$u1$u1') & (sub(c1163,'familiename$u1$u1') & (val(c1163,'roll$u0') & (attr(c1167,c1168) & (sub(c1167,'mensch$u1$u1') & (sub(c1168,'familiename$u1$u1') & (val(c1168,'royce$u0') & (attr(c1170,c1171) & (sub(c1171,'jahr$u$u1$u1') & (val(c1171,c1165) & (attr(c1174,c1175) & (sub(c1175,'jahr$u$u1$u1') & (val(c1175,c1172) & (pred(c1177,'kontrakt$u1$u1') & (attr(c1186,c1187) & (sub(c1186,'land$u1$u1') & (sub(c1187,'name$u1$u1') & (val(c1187,'usa$u0') & (attr(c1188,c1213) & (prop(c1188,'kandadischen$u1$u1') & (sub(c1188,'fabrikant$u1$u1') & (sub(c1188,'firma$u1$u1') & (pred(c1189,'gulfstream$u1$u1') & (sub(c1213,'name$u1$u1') & (val(c1213,'bombardier$u0') & ('tupl$up14'(c1251,c162,c170,c180,c1158,c1162,c1167,c1170,c1174,c1177,c1186,c1188,c1189,c1188) & (prop(c162,'klein$u1$u1') & (sub(c162,'aggregat$u1$u1') & (attch(c167,c170) & (attr(c167,c168) & (sub(c167,'einrichtung$u1$u2') & (sub(c168,'name$u1$u1') & (val(c168,'br$u0') & (attr(c170,c171) & (sub(c171,'jahr$u$u1$u1') & (val(c171,c165) & (pred(c180,'fr$u$u374htyp$u1$u1') & (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('ableger$u1$u1',d) & (card('ableger$u1$u1',int1) & (etype('ableger$u1$u1',int0) & (fact('ableger$u1$u1',real) & (gener('ableger$u1$u1',ge) & (quant('ableger$u1$u1',one) & (refer('ableger$u1$u1','refer$uc') & (varia('ableger$u1$u1','varia$uc') & (sort('werk$u1$u2',d) & (sort('werk$u1$u2',io) & (card('werk$u1$u2',int1) & (etype('werk$u1$u2',int0) & (fact('werk$u1$u2',real) & (gener('werk$u1$u2',ge) & (quant('werk$u1$u2',one) & (refer('werk$u1$u2','refer$uc') & (varia('werk$u1$u2','varia$uc') & (sort(c1158,d) & (sort(c1158,io) & (card(c1158,int1) & (etype(c1158,int0) & (fact(c1158,real) & (gener(c1158,sp) & (quant(c1158,one) & (refer(c1158,det) & (varia(c1158,con) & (sort(c1159,na) & (card(c1159,int1) & (etype(c1159,int0) & (fact(c1159,real) & (gener(c1159,sp) & (quant(c1159,one) & (refer(c1159,indet) & (varia(c1159,'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('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(c1162,d) & (card(c1162,int1) & (etype(c1162,int0) & (fact(c1162,real) & (gener(c1162,sp) & (quant(c1162,one) & (refer(c1162,det) & (varia(c1162,con) & (sort(c1163,na) & (card(c1163,int1) & (etype(c1163,int0) & (fact(c1163,real) & (gener(c1163,sp) & (quant(c1163,one) & (refer(c1163,indet) & (varia(c1163,'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(c1167,d) & (card(c1167,int1) & (etype(c1167,int0) & (fact(c1167,real) & (gener(c1167,sp) & (quant(c1167,one) & (refer(c1167,det) & (varia(c1167,con) & (sort(c1168,na) & (card(c1168,int1) & (etype(c1168,int0) & (fact(c1168,real) & (gener(c1168,sp) & (quant(c1168,one) & (refer(c1168,indet) & (varia(c1168,'varia$uc') & (sort('royce$u0',fe) & (sort(c1170,t) & (card(c1170,int1) & (etype(c1170,int0) & (fact(c1170,real) & (gener(c1170,sp) & (quant(c1170,one) & (refer(c1170,det) & (varia(c1170,con) & (sort(c1171,me) & (sort(c1171,oa) & (sort(c1171,ta) & (card(c1171,'card$uc') & (etype(c1171,'etype$uc') & (fact(c1171,real) & (gener(c1171,sp) & (quant(c1171,'quant$uc') & (refer(c1171,'refer$uc') & (varia(c1171,'varia$uc') & (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(c1165,nu) & (card(c1165,int1992) & (sort(c1174,t) & (card(c1174,int1) & (etype(c1174,int0) & (fact(c1174,real) & (gener(c1174,sp) & (quant(c1174,one) & (refer(c1174,det) & (varia(c1174,con) & (sort(c1175,me) & (sort(c1175,oa) & (sort(c1175,ta) & (card(c1175,'card$uc') & (etype(c1175,'etype$uc') & (fact(c1175,real) & (gener(c1175,sp) & (quant(c1175,'quant$uc') & (refer(c1175,'refer$uc') & (varia(c1175,'varia$uc') & (sort(c1172,nu) & (card(c1172,int1993) & (sort(c1177,d) & (sort(c1177,io) & (card(c1177,cons('x$uconstant',cons(int1,nil))) & (etype(c1177,int1) & (fact(c1177,real) & (gener(c1177,'gener$uc') & (quant(c1177,mult) & (refer(c1177,indet) & (varia(c1177,'varia$uc') & (sort('kontrakt$u1$u1',d) & (sort('kontrakt$u1$u1',io) & (card('kontrakt$u1$u1',int1) & (etype('kontrakt$u1$u1',int0) & (fact('kontrakt$u1$u1',real) & (gener('kontrakt$u1$u1',ge) & (quant('kontrakt$u1$u1',one) & (refer('kontrakt$u1$u1','refer$uc') & (varia('kontrakt$u1$u1','varia$uc') & (sort(c1186,d) & (sort(c1186,io) & (card(c1186,int1) & (etype(c1186,int0) & (fact(c1186,real) & (gener(c1186,sp) & (quant(c1186,one) & (refer(c1186,det) & (varia(c1186,con) & (sort(c1187,na) & (card(c1187,int1) & (etype(c1187,int0) & (fact(c1187,real) & (gener(c1187,sp) & (quant(c1187,one) & (refer(c1187,indet) & (varia(c1187,'varia$uc') & (sort('land$u1$u1',d) & (sort('land$u1$u1',io) & (card('land$u1$u1',int1) & (etype('land$u1$u1',int0) & (fact('land$u1$u1',real) & (gener('land$u1$u1',ge) & (quant('land$u1$u1',one) & (refer('land$u1$u1','refer$uc') & (varia('land$u1$u1','varia$uc') & (sort('usa$u0',fe) & (sort(c1188,d) & (sort(c1188,io) & (card(c1188,int1) & (etype(c1188,int0) & (fact(c1188,real) & (gener(c1188,'gener$uc') & (quant(c1188,one) & (refer(c1188,'refer$uc') & (varia(c1188,'varia$uc') & (sort(c1213,na) & (card(c1213,int1) & (etype(c1213,int0) & (fact(c1213,real) & (gener(c1213,sp) & (quant(c1213,one) & (refer(c1213,indet) & (varia(c1213,'varia$uc') & (sort('kandadischen$u1$u1',gq) & (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(c1189,o) & (card(c1189,cons('x$uconstant',cons(int1,nil))) & (etype(c1189,int1) & (fact(c1189,real) & (gener(c1189,'gener$uc') & (quant(c1189,mult) & (refer(c1189,indet) & (varia(c1189,'varia$uc') & (sort('gulfstream$u1$u1',o) & (card('gulfstream$u1$u1',int1) & (etype('gulfstream$u1$u1',int0) & (fact('gulfstream$u1$u1',real) & (gener('gulfstream$u1$u1',ge) & (quant('gulfstream$u1$u1',one) & (refer('gulfstream$u1$u1','refer$uc') & (varia('gulfstream$u1$u1','varia$uc') & (sort('bombardier$u0',fe) & (sort(c1251,ent) & (card(c1251,'card$uc') & (etype(c1251,'etype$uc') & (fact(c1251,real) & (gener(c1251,'gener$uc') & (quant(c1251,'quant$uc') & (refer(c1251,'refer$uc') & (varia(c1251,'varia$uc') & (sort(c162,d) & (sort(c162,io) & (card(c162,int1) & (etype(c162,int0) & (fact(c162,real) & (gener(c162,sp) & (quant(c162,one) & (refer(c162,det) & (varia(c162,con) & (sort(c170,t) & (card(c170,int1) & (etype(c170,int0) & (fact(c170,real) & (gener(c170,sp) & (quant(c170,one) & (refer(c170,det) & (varia(c170,con) & (sort(c180,d) & (card(c180,cons('x$uconstant',cons(int1,nil))) & (etype(c180,int1) & (fact(c180,real) & (gener(c180,'gener$uc') & (quant(c180,mult) & (refer(c180,indet) & (varia(c180,'varia$uc') & (sort('klein$u1$u1',mq) & (sort(c167,d) & (sort(c167,io) & (card(c167,int1) & (etype(c167,int1) & (fact(c167,real) & (gener(c167,sp) & (quant(c167,one) & (refer(c167,det) & (varia(c167,con) & (sort(c168,na) & (card(c168,int1) & (etype(c168,int0) & (fact(c168,real) & (gener(c168,sp) & (quant(c168,one) & (refer(c168,indet) & (varia(c168,'varia$uc') & (sort('einrichtung$u1$u2',d) & (sort('einrichtung$u1$u2',io) & (card('einrichtung$u1$u2','card$uc') & (etype('einrichtung$u1$u2',int1) & (fact('einrichtung$u1$u2',real) & (gener('einrichtung$u1$u2',ge) & (quant('einrichtung$u1$u2','quant$uc') & (refer('einrichtung$u1$u2','refer$uc') & (varia('einrichtung$u1$u2','varia$uc') & (sort('br$u0',fe) & (sort(c171,me) & (sort(c171,oa) & (sort(c171,ta) & (card(c171,'card$uc') & (etype(c171,'etype$uc') & (fact(c171,real) & (gener(c171,sp) & (quant(c171,'quant$uc') & (refer(c171,'refer$uc') & (varia(c171,'varia$uc') & (sort(c165,nu) & (card(c165,int710) & (sort('fr$u$u374htyp$u1$u1',d) & (card('fr$u$u374htyp$u1$u1',int1) & (etype('fr$u$u374htyp$u1$u1',int0) & (fact('fr$u$u374htyp$u1$u1',real) & (gener('fr$u$u374htyp$u1$u1',ge) & (quant('fr$u$u374htyp$u1$u1',one) & (refer('fr$u$u374htyp$u1$u1','refer$uc') & varia('fr$u$u374htyp$u1$u1','varia$uc')))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 72.80/11.52 fof(member_first, axiom, ! [X0] : ! [X1] : member(X0,cons(X0,X1))).
% 72.80/11.52 fof(member_second, axiom, ! [X0] : ! [X1] : ! [X2] : ((member(X0,X2) => member(X0,cons(X1,X2))))).
% 72.80/11.52 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'))))))).
% 72.80/11.52 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'))))))))))).
% 72.80/11.52 fof(synth_qa07_007_mira_news_1142, 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') & (sub(X6,'jahr$u$u1$u1') & (val(X1,'bmw$u0') & val(X2,'bmw$u0')))))))))))).
% 72.80/11.52 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') & (sub(X6,'jahr$u$u1$u1') & (val(X1,'bmw$u0') & val(X2,'bmw$u0'))))))))))), inference(negate_conjecture, [status(cth)], [synth_qa07_007_mira_news_1142])).
% 72.80/11.52 cnf(c2, plain, attr(c1158,c1159), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1142])).
% 72.80/11.52 cnf(c3, plain, sub(c1158,'firma$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1142])).
% 72.80/11.52 cnf(c4, plain, sub(c1159,'name$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1142])).
% 72.80/11.52 cnf(c5, plain, val(c1159,'bmw$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1142])).
% 72.80/11.52 cnf(c17, plain, attr(c1174,c1175), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1142])).
% 72.80/11.52 cnf(c18, plain, sub(c1175,'jahr$u$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_news_1142])).
% 72.80/11.52 cnf(c375, plain, member(X0,cons(X0,X1)), inference(clausification, [status(esa)], [member_first])).
% 72.80/11.52 cnf(c376, plain, ~member(X0,X1) | member(X0,cons(X2,X1)), inference(clausification, [status(esa)], [member_second])).
% 72.80/11.52 cnf(c471, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | arg1(sK151(X0),X0), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 72.80/11.52 cnf(c472, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | arg2(sK151(X0),X0), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 72.80/11.52 cnf(c473, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | subs(sK151(X0),'hei$u$u337en$u1$u1'), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 72.80/11.52 cnf(c474, 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])).
% 72.80/11.52 cnf(c479, plain, ~X0(X1,X2,X3) | obj(sK156(X1,X2,X3),X2), inference(clausification, [status(esa)], [hei__337en_1_1__bezeichnen_1_1_als])).
% 72.80/11.52 cnf(c497, plain, ~val(X0,'bmw$u0') | ~attr(X1,X0) | ~sub(X2,'firma$u1$u1') | ~val(X3,'bmw$u0') | ~sub(X0,'name$u1$u1') | ~obj(X4,X2) | ~attr(X5,X6) | ~sub(X6,'jahr$u$u1$u1') | ~attr(X2,X3) | ~sub(X3,'name$u1$u1'), inference(clausification, [status(esa)], [negated_conjecture])).
% 72.80/11.52 cnf(d0, plain, ~sub(X0,X1) | ~attr(X2,X0) | arg1(sK151(X2),X2) | ~member(X1,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c471,c376])).
% 72.80/11.52 cnf(d1, plain, ~sub(X0,X1) | ~attr(X2,X0) | arg1(sK151(X2),X2) | ~member(X1,cons('name$u1$u1',nil)), inference(resolution, [status(thm)], [d0,c376])).
% 72.80/11.52 cnf(d2, plain, ~sub(X0,'name$u1$u1') | ~attr(X1,X0) | arg1(sK151(X1),X1), inference(resolution, [status(thm)], [d1,c375])).
% 72.80/11.52 cnf(d3, plain, ~sub(c1159,'name$u1$u1') | arg1(sK151(c1158),c1158), inference(resolution, [status(thm)], [d2,c2])).
% 72.80/11.52 cnf(d4, plain, arg1(sK151(c1158),c1158), inference(resolution, [status(thm)], [c4,d3])).
% 72.80/11.52 cnf(d5, plain, ~sub(X0,'jahr$u$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'firma$u1$u1') | ~attr(X3,X0) | ~attr(X2,X1) | ~val(X1,'bmw$u0') | ~val(X1,'bmw$u0') | ~obj(X4,X2), inference(factoring, [status(thm)], [c497])).
% 72.80/11.52 cnf(d6, plain, ~sub(X0,'firma$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'jahr$u$u1$u1') | ~attr(X3,X2) | ~attr(X0,X1) | ~val(X1,'bmw$u0') | ~'Ts152'(X4,X0,X5), inference(resolution, [status(thm)], [d5,c479])).
% 72.80/11.52 cnf(d7, plain, ~sub(X0,'jahr$u$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'firma$u1$u1') | ~attr(X3,X0) | ~attr(X2,X1) | ~val(X1,'bmw$u0') | ~subs(X4,'hei$u$u337en$u1$u1') | ~arg1(X4,X2) | ~arg2(X4,X5), inference(resolution, [status(thm)], [d6,c474])).
% 72.80/11.52 cnf(d8, plain, ~sub(X0,X1) | ~attr(X2,X0) | arg2(sK151(X2),X2) | ~member(X1,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c472,c376])).
% 72.80/11.52 cnf(d9, plain, ~sub(X0,X1) | ~attr(X2,X0) | arg2(sK151(X2),X2) | ~member(X1,cons('name$u1$u1',nil)), inference(resolution, [status(thm)], [d8,c376])).
% 72.80/11.52 cnf(d10, plain, ~sub(X0,'name$u1$u1') | ~attr(X1,X0) | arg2(sK151(X1),X1), inference(resolution, [status(thm)], [d9,c375])).
% 72.80/11.52 cnf(d11, plain, ~sub(c1159,'name$u1$u1') | arg2(sK151(c1158),c1158), inference(resolution, [status(thm)], [d10,c2])).
% 72.80/11.52 cnf(d12, plain, arg2(sK151(c1158),c1158), inference(resolution, [status(thm)], [c4,d11])).
% 72.80/11.52 cnf(d13, plain, ~sub(X0,'firma$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'jahr$u$u1$u1') | ~attr(X3,X2) | ~attr(X0,X1) | ~val(X1,'bmw$u0') | ~subs(sK151(c1158),'hei$u$u337en$u1$u1') | ~arg1(sK151(c1158),X0), inference(resolution, [status(thm)], [d12,d7])).
% 72.80/11.52 cnf(d14, plain, ~sub(X0,X1) | ~attr(X2,X0) | subs(sK151(X2),'hei$u$u337en$u1$u1') | ~member(X1,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c473,c376])).
% 72.80/11.52 cnf(d15, plain, ~sub(X0,X1) | ~attr(X2,X0) | subs(sK151(X2),'hei$u$u337en$u1$u1') | ~member(X1,cons('name$u1$u1',nil)), inference(resolution, [status(thm)], [d14,c376])).
% 72.80/11.52 cnf(d16, plain, ~sub(X0,'name$u1$u1') | ~attr(X1,X0) | subs(sK151(X1),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [d15,c375])).
% 72.80/11.52 cnf(d17, plain, ~sub(c1159,'name$u1$u1') | subs(sK151(c1158),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [d16,c2])).
% 72.80/11.52 cnf(d18, plain, subs(sK151(c1158),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [c4,d17])).
% 72.80/11.52 cnf(d19, plain, ~sub(X0,'jahr$u$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'firma$u1$u1') | ~attr(X3,X0) | ~attr(X2,X1) | ~val(X1,'bmw$u0') | ~arg1(sK151(c1158),X2), inference(resolution, [status(thm)], [d18,d13])).
% 72.80/11.52 cnf(d20, plain, ~sub(c1158,'firma$u1$u1') | ~sub(X0,'name$u1$u1') | ~sub(X1,'jahr$u$u1$u1') | ~attr(X2,X1) | ~attr(c1158,X0) | ~val(X0,'bmw$u0'), inference(resolution, [status(thm)], [d19,d4])).
% 72.80/11.52 cnf(d21, plain, ~sub(X0,'jahr$u$u1$u1') | ~sub(X1,'name$u1$u1') | ~attr(X2,X0) | ~attr(c1158,X1) | ~val(X1,'bmw$u0'), inference(resolution, [status(thm)], [c3,d20])).
% 72.80/11.52 cnf(d22, plain, ~sub(c1159,'name$u1$u1') | ~sub(X0,'jahr$u$u1$u1') | ~attr(X1,X0) | ~attr(c1158,c1159), inference(resolution, [status(thm)], [d21,c5])).
% 72.80/11.52 cnf(d23, plain, ~sub(X0,'jahr$u$u1$u1') | ~sub(c1159,'name$u1$u1') | ~attr(X1,X0), inference(resolution, [status(thm)], [c2,d22])).
% 72.80/11.52 cnf(d24, plain, ~sub(X0,'jahr$u$u1$u1') | ~attr(X1,X0), inference(resolution, [status(thm)], [c4,d23])).
% 72.80/11.52 cnf(d25, plain, ~sub(c1175,'jahr$u$u1$u1'), inference(resolution, [status(thm)], [d24,c17])).
% 72.80/11.52 cnf(d26, plain, $false, inference(resolution, [status(thm)], [c18,d25])).
% 72.80/11.52 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------