%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR116+15 : 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 : n026.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:52 AM UTC 2026
% Result : Theorem 66.27s 11.45s
% Output : CNFRefutation 66.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+15 : 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.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 01:16:56 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 66.27/11.45 % SZS status Theorem for theBenchmark.p
% 66.27/11.45 % SZS output start CNFRefutation for theBenchmark.p
% 66.27/11.45 fof(ave07_era5_synth_qa07_010_mira_news_1724, hypothesis, (sub(c37989,'attribut$u$u1$u1') & (attch(c38000,c38006) & (attr(c38000,c38001) & (sub(c38000,'land$u1$u1') & (sub(c38001,'name$u1$u1') & (val(c38001,'s$u$u374dafrika$u0') & (attr(c38006,c38007) & (attr(c38006,c38008) & (sub(c38006,'pr$u$u344sident$u1$u1') & (sub(c38007,'eigenname$u1$u1') & (val(c38007,'nelson$u0') & (sub(c38008,'familiename$u1$u1') & (val(c38008,'mandela$u0') & (sub(c38015,'schuldenproblem$u1$u1') & (attch(c38022,c38015) & (attr(c38022,c38023) & (sub(c38022,'gebietsinstitution$u1$u1') & (sub(c38023,'name$u1$u1') & (val(c38023,'afrika$u0') & (prop(c38029,c37984) & (rslt(c38029,c38035) & (subs(c38029,'schaffung$u1$u1') & (prop(c38035,'gemeinsam$u1$u1') & (sub(c38035,'markt$u1$u1') & (predr(c38044,'gesch$u$u344ftbeziehung$u1$u1') & (attch(c38049,c38044) & (pred(c38049,'land$u1$u1') & (prop(c38049,'afrikanisch$u$u1$u1') & (attr(c38064,c38065) & (sub(c38064,'einrichtung$u1$u2') & (sub(c38065,'name$u1$u1') & (val(c38065,'eu$u0') & ('tupl$up8'(c38071,c37989,c37993,c38006,c38015,c38029,c38044,c38064) & (assoc('gesch$u$u344ftbeziehung$u1$u1','gesch$u$u344ft$u1$u2') & (subr('gesch$u$u344ftbeziehung$u1$u1','be$uziehung$u1$u1') & (chsp2('planen$u1$u1',c37984) & (assoc('schuldenproblem$u1$u1','schulden$u2$u1') & (sub('schuldenproblem$u1$u1','problem$u1$u1') & (sort(c37989,io) & (sort(c37989,na) & (card(c37989,int1) & (etype(c37989,int0) & (fact(c37989,real) & (gener(c37989,sp) & (quant(c37989,one) & (refer(c37989,det) & (varia(c37989,'varia$uc') & (sort('attribut$u$u1$u1',io) & (sort('attribut$u$u1$u1',na) & (card('attribut$u$u1$u1',int1) & (etype('attribut$u$u1$u1',int0) & (fact('attribut$u$u1$u1',real) & (gener('attribut$u$u1$u1',ge) & (quant('attribut$u$u1$u1',one) & (refer('attribut$u$u1$u1','refer$uc') & (varia('attribut$u$u1$u1','varia$uc') & (sort(c38000,d) & (sort(c38000,io) & (card(c38000,int1) & (etype(c38000,int0) & (fact(c38000,real) & (gener(c38000,sp) & (quant(c38000,one) & (refer(c38000,det) & (varia(c38000,con) & (sort(c38006,d) & (card(c38006,int1) & (etype(c38006,int0) & (fact(c38006,real) & (gener(c38006,sp) & (quant(c38006,one) & (refer(c38006,det) & (varia(c38006,'varia$uc') & (sort(c38001,na) & (card(c38001,int1) & (etype(c38001,int0) & (fact(c38001,real) & (gener(c38001,sp) & (quant(c38001,one) & (refer(c38001,indet) & (varia(c38001,'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('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('s$u$u374dafrika$u0',fe) & (sort(c38007,na) & (card(c38007,int1) & (etype(c38007,int0) & (fact(c38007,real) & (gener(c38007,sp) & (quant(c38007,one) & (refer(c38007,indet) & (varia(c38007,'varia$uc') & (sort(c38008,na) & (card(c38008,int1) & (etype(c38008,int0) & (fact(c38008,real) & (gener(c38008,sp) & (quant(c38008,one) & (refer(c38008,indet) & (varia(c38008,'varia$uc') & (sort('pr$u$u344sident$u1$u1',d) & (card('pr$u$u344sident$u1$u1',int1) & (etype('pr$u$u344sident$u1$u1',int0) & (fact('pr$u$u344sident$u1$u1',real) & (gener('pr$u$u344sident$u1$u1',ge) & (quant('pr$u$u344sident$u1$u1',one) & (refer('pr$u$u344sident$u1$u1','refer$uc') & (varia('pr$u$u344sident$u1$u1','varia$uc') & (sort('eigenname$u1$u1',na) & (card('eigenname$u1$u1',int1) & (etype('eigenname$u1$u1',int0) & (fact('eigenname$u1$u1',real) & (gener('eigenname$u1$u1',ge) & (quant('eigenname$u1$u1',one) & (refer('eigenname$u1$u1','refer$uc') & (varia('eigenname$u1$u1','varia$uc') & (sort('nelson$u0',fe) & (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('mandela$u0',fe) & (sort(c38015,as) & (sort(c38015,io) & (card(c38015,int1) & (etype(c38015,int0) & (fact(c38015,real) & (gener(c38015,sp) & (quant(c38015,one) & (refer(c38015,det) & (varia(c38015,con) & (sort('schuldenproblem$u1$u1',as) & (sort('schuldenproblem$u1$u1',io) & (card('schuldenproblem$u1$u1',int1) & (etype('schuldenproblem$u1$u1',int0) & (fact('schuldenproblem$u1$u1',real) & (gener('schuldenproblem$u1$u1',ge) & (quant('schuldenproblem$u1$u1',one) & (refer('schuldenproblem$u1$u1','refer$uc') & (varia('schuldenproblem$u1$u1','varia$uc') & (sort(c38022,d) & (sort(c38022,io) & (card(c38022,int1) & (etype(c38022,int0) & (fact(c38022,real) & (gener(c38022,sp) & (quant(c38022,one) & (refer(c38022,det) & (varia(c38022,con) & (sort(c38023,na) & (card(c38023,int1) & (etype(c38023,int0) & (fact(c38023,real) & (gener(c38023,sp) & (quant(c38023,one) & (refer(c38023,indet) & (varia(c38023,'varia$uc') & (sort('gebietsinstitution$u1$u1',d) & (sort('gebietsinstitution$u1$u1',io) & (card('gebietsinstitution$u1$u1',int1) & (etype('gebietsinstitution$u1$u1',int0) & (fact('gebietsinstitution$u1$u1',real) & (gener('gebietsinstitution$u1$u1',ge) & (quant('gebietsinstitution$u1$u1',one) & (refer('gebietsinstitution$u1$u1','refer$uc') & (varia('gebietsinstitution$u1$u1','varia$uc') & (sort('afrika$u0',fe) & (sort(c38029,ad) & (card(c38029,int1) & (etype(c38029,int0) & (fact(c38029,real) & (gener(c38029,sp) & (quant(c38029,one) & (refer(c38029,det) & (varia(c38029,con) & (sort(c37984,tq) & (sort(c38035,d) & (card(c38035,int1) & (etype(c38035,int0) & (fact(c38035,real) & (gener(c38035,sp) & (quant(c38035,one) & (refer(c38035,indet) & (varia(c38035,'varia$uc') & (sort('schaffung$u1$u1',ad) & (card('schaffung$u1$u1',int1) & (etype('schaffung$u1$u1',int0) & (fact('schaffung$u1$u1',real) & (gener('schaffung$u1$u1',ge) & (quant('schaffung$u1$u1',one) & (refer('schaffung$u1$u1','refer$uc') & (varia('schaffung$u1$u1','varia$uc') & (sort('gemeinsam$u1$u1',tq) & (sort('markt$u1$u1',d) & (card('markt$u1$u1',int1) & (etype('markt$u1$u1',int0) & (fact('markt$u1$u1',real) & (gener('markt$u1$u1',ge) & (quant('markt$u1$u1',one) & (refer('markt$u1$u1','refer$uc') & (varia('markt$u1$u1','varia$uc') & (sort(c38044,as) & (sort(c38044,re) & (card(c38044,cons('x$uconstant',cons(int1,nil))) & (etype(c38044,int1) & (fact(c38044,real) & (gener(c38044,sp) & (quant(c38044,mult) & (refer(c38044,det) & (varia(c38044,con) & (sort('gesch$u$u344ftbeziehung$u1$u1',as) & (sort('gesch$u$u344ftbeziehung$u1$u1',re) & (card('gesch$u$u344ftbeziehung$u1$u1',int1) & (etype('gesch$u$u344ftbeziehung$u1$u1',int0) & (fact('gesch$u$u344ftbeziehung$u1$u1',real) & (gener('gesch$u$u344ftbeziehung$u1$u1',ge) & (quant('gesch$u$u344ftbeziehung$u1$u1',one) & (refer('gesch$u$u344ftbeziehung$u1$u1','refer$uc') & (varia('gesch$u$u344ftbeziehung$u1$u1','varia$uc') & (sort(c38049,d) & (sort(c38049,io) & (card(c38049,cons('x$uconstant',cons(int1,nil))) & (etype(c38049,int1) & (fact(c38049,real) & (gener(c38049,sp) & (quant(c38049,mult) & (refer(c38049,det) & (varia(c38049,con) & (sort('afrikanisch$u$u1$u1',nq) & (sort(c38064,d) & (sort(c38064,io) & (card(c38064,int1) & (etype(c38064,int1) & (fact(c38064,real) & (gener(c38064,sp) & (quant(c38064,one) & (refer(c38064,det) & (varia(c38064,con) & (sort(c38065,na) & (card(c38065,int1) & (etype(c38065,int0) & (fact(c38065,real) & (gener(c38065,sp) & (quant(c38065,one) & (refer(c38065,indet) & (varia(c38065,'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('eu$u0',fe) & (sort(c38071,ent) & (card(c38071,'card$uc') & (etype(c38071,'etype$uc') & (fact(c38071,real) & (gener(c38071,'gener$uc') & (quant(c38071,'quant$uc') & (refer(c38071,'refer$uc') & (varia(c38071,'varia$uc') & (sort(c37993,o) & (card(c37993,int1) & (etype(c37993,int0) & (fact(c37993,real) & (gener(c37993,sp) & (quant(c37993,one) & (refer(c37993,det) & (varia(c37993,'varia$uc') & (sort('gesch$u$u344ft$u1$u2',ad) & (card('gesch$u$u344ft$u1$u2',int1) & (etype('gesch$u$u344ft$u1$u2',int0) & (fact('gesch$u$u344ft$u1$u2',real) & (gener('gesch$u$u344ft$u1$u2',ge) & (quant('gesch$u$u344ft$u1$u2',one) & (refer('gesch$u$u344ft$u1$u2','refer$uc') & (varia('gesch$u$u344ft$u1$u2','varia$uc') & (sort('be$uziehung$u1$u1',as) & (sort('be$uziehung$u1$u1',re) & (card('be$uziehung$u1$u1',int1) & (etype('be$uziehung$u1$u1',int0) & (fact('be$uziehung$u1$u1',real) & (gener('be$uziehung$u1$u1',ge) & (quant('be$uziehung$u1$u1',one) & (refer('be$uziehung$u1$u1','refer$uc') & (varia('be$uziehung$u1$u1','varia$uc') & (sort('planen$u1$u1',da) & (fact('planen$u1$u1',real) & (gener('planen$u1$u1',ge) & (sort('schulden$u2$u1',st) & (fact('schulden$u2$u1',real) & (gener('schulden$u2$u1',ge) & (sort('problem$u1$u1',as) & (sort('problem$u1$u1',io) & (card('problem$u1$u1',int1) & (etype('problem$u1$u1',int0) & (fact('problem$u1$u1',real) & (gener('problem$u1$u1',ge) & (quant('problem$u1$u1',one) & (refer('problem$u1$u1','refer$uc') & varia('problem$u1$u1','varia$uc')))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 66.27/11.45 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')))))))))))).
% 66.27/11.45 fof(sub__sub_0_expansion, axiom, ! [X0] : ! [X1] : ((sub(X0,X1) => ? [X2] : ((arg1(X2,X0) & (arg2(X2,X1) & subr(X2,'sub$u0'))))))).
% 66.27/11.45 fof(synth_qa07_010_mira_news_1724, conjecture, ? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ? [X8] : ((arg1(X3,X0) & (arg2(X3,X4) & (attr(X0,X1) & (attr(X0,X2) & (attr(X5,X6) & (obj(X7,X0) & (sub(X1,'familiename$u1$u1') & (sub(X2,'eigenname$u1$u1') & (sub(X4,X8) & (sub(X6,'name$u1$u1') & (subr(X3,'rprs$u0') & (val(X1,'mandela$u0') & (val(X2,'nelson$u0') & val(X6,'s$u$u374dafrika$u0')))))))))))))))).
% 66.27/11.45 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ? [X8] : ((arg1(X3,X0) & (arg2(X3,X4) & (attr(X0,X1) & (attr(X0,X2) & (attr(X5,X6) & (obj(X7,X0) & (sub(X1,'familiename$u1$u1') & (sub(X2,'eigenname$u1$u1') & (sub(X4,X8) & (sub(X6,'name$u1$u1') & (subr(X3,'rprs$u0') & (val(X1,'mandela$u0') & (val(X2,'nelson$u0') & val(X6,'s$u$u374dafrika$u0'))))))))))))))), inference(negate_conjecture, [status(cth)], [synth_qa07_010_mira_news_1724])).
% 66.27/11.45 cnf(c2, plain, attr(c38000,c38001), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1724])).
% 66.27/11.45 cnf(c4, plain, sub(c38001,'name$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1724])).
% 66.27/11.45 cnf(c5, plain, val(c38001,'s$u$u374dafrika$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1724])).
% 66.27/11.45 cnf(c6, plain, attr(c38006,c38007), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1724])).
% 66.27/11.45 cnf(c7, plain, attr(c38006,c38008), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1724])).
% 66.27/11.45 cnf(c8, plain, sub(c38006,'pr$u$u344sident$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1724])).
% 66.27/11.45 cnf(c9, plain, sub(c38007,'eigenname$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1724])).
% 66.27/11.45 cnf(c10, plain, val(c38007,'nelson$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1724])).
% 66.27/11.45 cnf(c11, plain, sub(c38008,'familiename$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1724])).
% 66.27/11.45 cnf(c12, plain, val(c38008,'mandela$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1724])).
% 66.27/11.45 cnf(c540, plain, ~arg1(X0,X1) | ~arg2(X0,X2) | ~subr(X0,'sub$u0') | X3(X0,X1,X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 66.27/11.45 cnf(c541, plain, ~X0(X1,X2,X3) | arg1(sK281(X1,X2,X3),X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 66.27/11.45 cnf(c542, plain, ~X0(X1,X2,X3) | arg2(sK281(X1,X2,X3),sK282(X1,X2,X3)), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 66.27/11.45 cnf(c545, plain, ~X0(X1,X2,X3) | obj(sK280(X1,X2,X3),X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 66.27/11.45 cnf(c546, plain, ~X0(X1,X2,X3) | sub(sK282(X1,X2,X3),X3), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 66.27/11.45 cnf(c547, plain, ~X0(X1,X2,X3) | subr(sK281(X1,X2,X3),'rprs$u0'), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 66.27/11.45 cnf(c549, plain, ~sub(X0,X1) | arg1(sK285(X0,X1),X0), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 66.27/11.45 cnf(c550, plain, ~sub(X0,X1) | arg2(sK285(X0,X1),X1), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 66.27/11.45 cnf(c551, plain, ~sub(X0,X1) | subr(sK285(X0,X1),'sub$u0'), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 66.27/11.45 cnf(c620, plain, ~arg1(X0,X1) | ~sub(X2,'eigenname$u1$u1') | ~val(X3,'mandela$u0') | ~attr(X4,X5) | ~sub(X6,X7) | ~attr(X1,X2) | ~arg2(X0,X6) | ~val(X2,'nelson$u0') | ~subr(X0,'rprs$u0') | ~sub(X5,'name$u1$u1') | ~attr(X1,X3) | ~obj(X8,X1) | ~val(X5,'s$u$u374dafrika$u0') | ~sub(X3,'familiename$u1$u1'), inference(clausification, [status(esa)], [negated_conjecture])).
% 66.27/11.45 cnf(d0, plain, ~sub(sK282(X0,X1,X2),X3) | ~sub(X4,'familiename$u1$u1') | ~sub(X5,'name$u1$u1') | ~sub(X6,'eigenname$u1$u1') | ~attr(X7,X5) | ~attr(X8,X4) | ~attr(X8,X6) | ~val(X4,'mandela$u0') | ~val(X5,'s$u$u374dafrika$u0') | ~val(X6,'nelson$u0') | ~subr(sK281(X0,X1,X2),'rprs$u0') | ~obj(X9,X8) | ~arg1(sK281(X0,X1,X2),X8) | ~'Ts276'(X0,X1,X2), inference(resolution, [status(thm)], [c620,c542])).
% 66.27/11.45 cnf(d1, plain, ~sub(X0,'eigenname$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(sK282(X3,X4,X5),X6) | ~attr(X4,X0) | ~attr(X4,X2) | ~attr(X7,X1) | ~val(X0,'nelson$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'mandela$u0') | ~subr(sK281(X3,X4,X5),'rprs$u0') | ~obj(X8,X4) | ~'Ts276'(X3,X4,X5) | ~'Ts276'(X3,X4,X5), inference(resolution, [status(thm)], [d0,c541])).
% 66.27/11.45 cnf(d2, plain, ~sub(X0,'familiename$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'eigenname$u1$u1') | ~sub(sK282(X3,X4,X5),X6) | ~attr(X7,X1) | ~attr(X4,X0) | ~attr(X4,X2) | ~val(X0,'mandela$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'nelson$u0') | ~obj(X8,X4) | ~'Ts276'(X3,X4,X5) | ~'Ts276'(X3,X4,X5), inference(resolution, [status(thm)], [d1,c547])).
% 66.27/11.45 cnf(d3, plain, ~sub(X0,'eigenname$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~attr(X3,X1) | ~attr(X4,X0) | ~attr(X4,X2) | ~val(X0,'nelson$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'mandela$u0') | ~obj(X5,X4) | ~'Ts276'(X6,X4,X7) | ~'Ts276'(X6,X4,X7), inference(resolution, [status(thm)], [d2,c546])).
% 66.27/11.45 cnf(d4, plain, ~sub(X0,'familiename$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'eigenname$u1$u1') | ~attr(X3,X0) | ~attr(X3,X2) | ~attr(X4,X1) | ~val(X0,'mandela$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'nelson$u0') | ~obj(X5,X3) | ~subr(X6,'sub$u0') | ~arg1(X6,X3) | ~arg2(X6,X7), inference(resolution, [status(thm)], [d3,c540])).
% 66.27/11.45 cnf(d5, plain, ~sub(X0,'eigenname$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~attr(X3,X1) | ~attr(X4,X0) | ~attr(X4,X2) | ~val(X0,'nelson$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'mandela$u0') | ~subr(sK285(X5,X6),'sub$u0') | ~obj(X7,X4) | ~arg1(sK285(X5,X6),X4) | ~sub(X5,X6), inference(resolution, [status(thm)], [d4,c550])).
% 66.27/11.45 cnf(d6, plain, ~sub(X0,X1) | ~sub(X2,'familiename$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'eigenname$u1$u1') | ~attr(X0,X2) | ~attr(X0,X4) | ~attr(X5,X3) | ~val(X2,'mandela$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'nelson$u0') | ~subr(sK285(X0,X1),'sub$u0') | ~obj(X6,X0) | ~sub(X0,X1), inference(resolution, [status(thm)], [d5,c549])).
% 66.27/11.45 cnf(d7, plain, ~sub(X0,'eigenname$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X3,X4) | ~attr(X5,X1) | ~attr(X3,X0) | ~attr(X3,X2) | ~val(X0,'nelson$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'mandela$u0') | ~obj(X6,X3) | ~sub(X3,X4), inference(resolution, [status(thm)], [d6,c551])).
% 66.27/11.45 cnf(d8, plain, ~sub(X0,X1) | ~sub(X2,'familiename$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'eigenname$u1$u1') | ~attr(X5,X3) | ~attr(X0,X2) | ~attr(X0,X4) | ~val(X2,'mandela$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'nelson$u0') | ~'Ts276'(X6,X0,X7), inference(resolution, [status(thm)], [d7,c545])).
% 66.27/11.45 cnf(d9, plain, ~sub(X0,'eigenname$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X3,X4) | ~attr(X5,X1) | ~attr(X3,X0) | ~attr(X3,X2) | ~val(X0,'nelson$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'mandela$u0') | ~subr(X6,'sub$u0') | ~arg1(X6,X3) | ~arg2(X6,X7), inference(resolution, [status(thm)], [d8,c540])).
% 66.27/11.45 cnf(d10, plain, ~sub(X0,X1) | ~sub(X2,'familiename$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'eigenname$u1$u1') | ~attr(X5,X3) | ~attr(X0,X2) | ~attr(X0,X4) | ~val(X2,'mandela$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'nelson$u0') | ~subr(sK285(X6,X7),'sub$u0') | ~arg1(sK285(X6,X7),X0) | ~sub(X6,X7), inference(resolution, [status(thm)], [d9,c550])).
% 66.27/11.45 cnf(d11, plain, ~sub(X0,X1) | ~sub(X2,'eigenname$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'familiename$u1$u1') | ~sub(X0,X5) | ~attr(X6,X3) | ~attr(X0,X2) | ~attr(X0,X4) | ~val(X2,'nelson$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'mandela$u0') | ~subr(sK285(X0,X1),'sub$u0') | ~sub(X0,X1), inference(resolution, [status(thm)], [d10,c549])).
% 66.27/11.45 cnf(d12, plain, ~sub(X0,'familiename$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'eigenname$u1$u1') | ~sub(X3,X4) | ~sub(X3,X5) | ~attr(X6,X1) | ~attr(X3,X0) | ~attr(X3,X2) | ~val(X0,'mandela$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'nelson$u0') | ~sub(X3,X5), inference(resolution, [status(thm)], [d11,c551])).
% 66.27/11.45 cnf(d13, plain, ~sub(X0,X1) | ~sub(X0,X2) | ~sub(X3,'eigenname$u1$u1') | ~sub(X4,'name$u1$u1') | ~sub(c38008,'familiename$u1$u1') | ~attr(X5,X4) | ~attr(X0,X3) | ~attr(X0,c38008) | ~val(X3,'nelson$u0') | ~val(X4,'s$u$u374dafrika$u0'), inference(resolution, [status(thm)], [d12,c12])).
% 66.27/11.45 cnf(d14, plain, ~sub(X0,'name$u1$u1') | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,X3) | ~sub(X2,X4) | ~attr(X5,X0) | ~attr(X2,X1) | ~attr(X2,c38008) | ~val(X0,'s$u$u374dafrika$u0') | ~val(X1,'nelson$u0'), inference(resolution, [status(thm)], [c11,d13])).
% 66.27/11.45 cnf(d15, plain, ~sub(X0,X1) | ~sub(X0,X2) | ~sub(X3,'eigenname$u1$u1') | ~sub(c38001,'name$u1$u1') | ~attr(X4,c38001) | ~attr(X0,X3) | ~attr(X0,c38008) | ~val(X3,'nelson$u0'), inference(resolution, [status(thm)], [d14,c5])).
% 66.27/11.45 cnf(d16, plain, ~sub(X0,'eigenname$u1$u1') | ~sub(X1,X2) | ~sub(X1,X3) | ~attr(X4,c38001) | ~attr(X1,X0) | ~attr(X1,c38008) | ~val(X0,'nelson$u0'), inference(resolution, [status(thm)], [c4,d15])).
% 66.27/11.45 cnf(d17, plain, ~sub(X0,X1) | ~sub(X0,X2) | ~sub(c38007,'eigenname$u1$u1') | ~attr(X3,c38001) | ~attr(X0,c38007) | ~attr(X0,c38008), inference(resolution, [status(thm)], [d16,c10])).
% 66.27/11.45 cnf(d18, plain, ~sub(X0,X1) | ~sub(X0,X2) | ~attr(X3,c38001) | ~attr(X0,c38007) | ~attr(X0,c38008), inference(resolution, [status(thm)], [c9,d17])).
% 66.27/11.45 cnf(d19, plain, ~sub(c38006,X0) | ~sub(c38006,X1) | ~attr(X2,c38001) | ~attr(c38006,c38007), inference(resolution, [status(thm)], [d18,c7])).
% 66.27/11.45 cnf(d20, plain, ~sub(c38006,X0) | ~sub(c38006,X1) | ~attr(X2,c38001), inference(resolution, [status(thm)], [c6,d19])).
% 66.27/11.45 cnf(d21, plain, ~sub(c38006,X0) | ~sub(c38006,X1), inference(resolution, [status(thm)], [d20,c2])).
% 66.27/11.45 cnf(d22, plain, ~sub(c38006,X0), inference(resolution, [status(thm)], [d21,c8])).
% 66.27/11.45 cnf(d23, plain, $false, inference(resolution, [status(thm)], [d22,c8])).
% 66.27/11.45 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------