%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR116+20 : 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 : 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:52 AM UTC 2026
% Result : Theorem 58.89s 9.20s
% Output : CNFRefutation 58.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR116+20 : 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 : n018.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:38 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.89/9.20 % SZS status Theorem for theBenchmark.p
% 58.89/9.20 % SZS output start CNFRefutation for theBenchmark.p
% 58.89/9.20 fof(ave07_era5_synth_qa07_010_mira_news_1772, hypothesis, (obj(c1706,c1710) & (subs(c1706,'bildung$u1$u1') & (sub(c1710,'regierung$u1$u1') & (attch(c19,c26) & (attr(c19,c20) & (prop(c19,'afrikanisch$u$u1$u1') & (sub(c19,'nationalkongre$u$u337$u1$u1') & (sub(c20,'name$u1$u1') & (val(c20,'anc$u0') & (agt(c2016,c19) & (circ(c2016,c1706) & (modl(c2016,'wollen$u0') & (obj(c2016,c54) & (ornt(c2016,c2058) & (subs(c2016,'lassen$u1$u4') & (attch(c2054,c1710) & (attr(c2054,c2055) & (prop(c2054,'frei$u1$u1') & (prop(c2054,'national$u$u1$u1') & (sub(c2054,'einheit$u1$u2') & (sub(c2055,'familiename$u1$u1') & (val(c2055,'hand$u0') & (itms(c2058,c26,c40) & (sub(c26,'parteibo$u$u337$u1$u1') & (pred(c40,'pr$u$u344sident$u1$u1') & (prop(c40,c41) & (modp(c41,'voraussichtlich$u1$u1','kuenftig$u1$u1') & (attch(c46,c2058) & (attr(c46,c47) & (sub(c46,'land$u1$u1') & (sub(c47,'name$u1$u1') & (val(c47,'s$u$u374dafrika$u0') & (attr(c54,c55) & (attr(c54,c56) & (sub(c54,'mensch$u1$u1') & (sub(c55,'eigenname$u1$u1') & (val(c55,'nelson$u0') & (sub(c56,'familiename$u1$u1') & (val(c56,'mandela$u0') & (assoc('nationalkongre$u$u337$u1$u1','national$u$u1$u1') & (sub('nationalkongre$u$u337$u1$u1','kongre$u$u337$u1$u1') & (assoc('parteibo$u$u337$u1$u1','partei$u1$u1') & (sub('parteibo$u$u337$u1$u1','an$uf$u$u374hrer$u1$u1') & (sort(c1706,ad) & (card(c1706,int1) & (etype(c1706,int0) & (fact(c1706,real) & (gener(c1706,sp) & (quant(c1706,one) & (refer(c1706,det) & (varia(c1706,con) & (sort(c1710,d) & (sort(c1710,io) & (card(c1710,int1) & (etype(c1710,int1) & (fact(c1710,real) & (gener(c1710,sp) & (quant(c1710,one) & (refer(c1710,indet) & (varia(c1710,'varia$uc') & (sort('bildung$u1$u1',ad) & (card('bildung$u1$u1',int1) & (etype('bildung$u1$u1',int0) & (fact('bildung$u1$u1',real) & (gener('bildung$u1$u1',ge) & (quant('bildung$u1$u1',one) & (refer('bildung$u1$u1','refer$uc') & (varia('bildung$u1$u1','varia$uc') & (sort('regierung$u1$u1',d) & (sort('regierung$u1$u1',io) & (card('regierung$u1$u1','card$uc') & (etype('regierung$u1$u1',int1) & (fact('regierung$u1$u1',real) & (gener('regierung$u1$u1',ge) & (quant('regierung$u1$u1','quant$uc') & (refer('regierung$u1$u1','refer$uc') & (varia('regierung$u1$u1','varia$uc') & (sort(c19,d) & (sort(c19,io) & (card(c19,int1) & (etype(c19,int0) & (fact(c19,real) & (gener(c19,sp) & (quant(c19,one) & (refer(c19,det) & (varia(c19,con) & (sort(c26,d) & (card(c26,int1) & (etype(c26,int0) & (fact(c26,real) & (gener(c26,sp) & (quant(c26,one) & (refer(c26,det) & (varia(c26,'varia$uc') & (sort(c20,na) & (card(c20,int1) & (etype(c20,int0) & (fact(c20,real) & (gener(c20,sp) & (quant(c20,one) & (refer(c20,indet) & (varia(c20,'varia$uc') & (sort('afrikanisch$u$u1$u1',nq) & (sort('nationalkongre$u$u337$u1$u1',d) & (sort('nationalkongre$u$u337$u1$u1',io) & (card('nationalkongre$u$u337$u1$u1',int1) & (etype('nationalkongre$u$u337$u1$u1',int0) & (fact('nationalkongre$u$u337$u1$u1',real) & (gener('nationalkongre$u$u337$u1$u1',ge) & (quant('nationalkongre$u$u337$u1$u1',one) & (refer('nationalkongre$u$u337$u1$u1','refer$uc') & (varia('nationalkongre$u$u337$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('anc$u0',fe) & (sort(c2016,da) & (fact(c2016,real) & (gener(c2016,sp) & (sort('wollen$u0',md) & (fact('wollen$u0',real) & (gener('wollen$u0','gener$uc') & (sort(c54,d) & (card(c54,int1) & (etype(c54,int0) & (fact(c54,real) & (gener(c54,sp) & (quant(c54,one) & (refer(c54,det) & (varia(c54,con) & (sort(c2058,d) & (card(c2058,int2) & (etype(c2058,int1) & (fact(c2058,real) & (gener(c2058,sp) & (quant(c2058,nfquant) & (refer(c2058,det) & (varia(c2058,'varia$uc') & (sort('lassen$u1$u4',da) & (fact('lassen$u1$u4',real) & (gener('lassen$u1$u4',ge) & (sort(c2054,d) & (card(c2054,int1) & (etype(c2054,int1) & (fact(c2054,real) & (gener(c2054,sp) & (quant(c2054,one) & (refer(c2054,det) & (varia(c2054,con) & (sort(c2055,na) & (card(c2055,int1) & (etype(c2055,int0) & (fact(c2055,real) & (gener(c2055,sp) & (quant(c2055,one) & (refer(c2055,indet) & (varia(c2055,'varia$uc') & (sort('frei$u1$u1',nq) & (sort('national$u$u1$u1',nq) & (sort('einheit$u1$u2',d) & (card('einheit$u1$u2','card$uc') & (etype('einheit$u1$u2',int1) & (fact('einheit$u1$u2',real) & (gener('einheit$u1$u2',ge) & (quant('einheit$u1$u2','quant$uc') & (refer('einheit$u1$u2','refer$uc') & (varia('einheit$u1$u2','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('hand$u0',fe) & (sort(c40,d) & (card(c40,cons('x$uconstant',cons(int1,nil))) & (etype(c40,int1) & (fact(c40,real) & (gener(c40,sp) & (quant(c40,mult) & (refer(c40,det) & (varia(c40,'varia$uc') & (sort('parteibo$u$u337$u1$u1',d) & (card('parteibo$u$u337$u1$u1',int1) & (etype('parteibo$u$u337$u1$u1',int0) & (fact('parteibo$u$u337$u1$u1',real) & (gener('parteibo$u$u337$u1$u1',ge) & (quant('parteibo$u$u337$u1$u1',one) & (refer('parteibo$u$u337$u1$u1','refer$uc') & (varia('parteibo$u$u337$u1$u1','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(c41,tq) & (sort('voraussichtlich$u1$u1',tq) & (sort('kuenftig$u1$u1',tq) & (sort(c46,d) & (sort(c46,io) & (card(c46,int1) & (etype(c46,int0) & (fact(c46,real) & (gener(c46,sp) & (quant(c46,one) & (refer(c46,det) & (varia(c46,con) & (sort(c47,na) & (card(c47,int1) & (etype(c47,int0) & (fact(c47,real) & (gener(c47,sp) & (quant(c47,one) & (refer(c47,indet) & (varia(c47,'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('s$u$u374dafrika$u0',fe) & (sort(c55,na) & (card(c55,int1) & (etype(c55,int0) & (fact(c55,real) & (gener(c55,sp) & (quant(c55,one) & (refer(c55,indet) & (varia(c55,'varia$uc') & (sort(c56,na) & (card(c56,int1) & (etype(c56,int0) & (fact(c56,real) & (gener(c56,sp) & (quant(c56,one) & (refer(c56,indet) & (varia(c56,'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('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('mandela$u0',fe) & (sort('kongre$u$u337$u1$u1',d) & (sort('kongre$u$u337$u1$u1',io) & (card('kongre$u$u337$u1$u1',int1) & (etype('kongre$u$u337$u1$u1',int0) & (fact('kongre$u$u337$u1$u1',real) & (gener('kongre$u$u337$u1$u1',ge) & (quant('kongre$u$u337$u1$u1',one) & (refer('kongre$u$u337$u1$u1','refer$uc') & (varia('kongre$u$u337$u1$u1','varia$uc') & (sort('partei$u1$u1',d) & (sort('partei$u1$u1',io) & (card('partei$u1$u1','card$uc') & (etype('partei$u1$u1',int1) & (fact('partei$u1$u1',real) & (gener('partei$u1$u1',ge) & (quant('partei$u1$u1','quant$uc') & (refer('partei$u1$u1','refer$uc') & (varia('partei$u1$u1','varia$uc') & (sort('an$uf$u$u374hrer$u1$u1',d) & (card('an$uf$u$u374hrer$u1$u1',int1) & (etype('an$uf$u$u374hrer$u1$u1',int0) & (fact('an$uf$u$u374hrer$u1$u1',real) & (gener('an$uf$u$u374hrer$u1$u1',ge) & (quant('an$uf$u$u374hrer$u1$u1',one) & (refer('an$uf$u$u374hrer$u1$u1','refer$uc') & varia('an$uf$u$u374hrer$u1$u1','varia$uc')))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 58.89/9.20 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')))))))))))).
% 58.89/9.20 fof(sub__sub_0_expansion, axiom, ! [X0] : ! [X1] : ((sub(X0,X1) => ? [X2] : ((arg1(X2,X0) & (arg2(X2,X1) & subr(X2,'sub$u0'))))))).
% 58.89/9.20 fof(synth_qa07_010_mira_news_1772, 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')))))))))))))))).
% 58.89/9.20 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_1772])).
% 58.89/9.20 cnf(c12, plain, obj(c2016,c54), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1772])).
% 58.89/9.20 cnf(c28, plain, attr(c46,c47), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1772])).
% 58.89/9.20 cnf(c30, plain, sub(c47,'name$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1772])).
% 58.89/9.20 cnf(c31, plain, val(c47,'s$u$u374dafrika$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1772])).
% 58.89/9.20 cnf(c32, plain, attr(c54,c55), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1772])).
% 58.89/9.20 cnf(c33, plain, attr(c54,c56), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1772])).
% 58.89/9.20 cnf(c34, plain, sub(c54,'mensch$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1772])).
% 58.89/9.20 cnf(c35, plain, sub(c55,'eigenname$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1772])).
% 58.89/9.20 cnf(c36, plain, val(c55,'nelson$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1772])).
% 58.89/9.20 cnf(c37, plain, sub(c56,'familiename$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1772])).
% 58.89/9.20 cnf(c38, plain, val(c56,'mandela$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1772])).
% 58.89/9.20 cnf(c496, plain, ~arg1(X0,X1) | ~arg2(X0,X2) | ~subr(X0,'sub$u0') | X3(X0,X1,X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 58.89/9.20 cnf(c497, plain, ~X0(X1,X2,X3) | arg1(sK281(X1,X2,X3),X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 58.89/9.20 cnf(c498, plain, ~X0(X1,X2,X3) | arg2(sK281(X1,X2,X3),sK282(X1,X2,X3)), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 58.89/9.20 cnf(c502, plain, ~X0(X1,X2,X3) | sub(sK282(X1,X2,X3),X3), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 58.89/9.20 cnf(c503, plain, ~X0(X1,X2,X3) | subr(sK281(X1,X2,X3),'rprs$u0'), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 58.89/9.20 cnf(c505, plain, ~sub(X0,X1) | arg1(sK285(X0,X1),X0), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 58.89/9.20 cnf(c506, plain, ~sub(X0,X1) | arg2(sK285(X0,X1),X1), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 58.89/9.20 cnf(c507, plain, ~sub(X0,X1) | subr(sK285(X0,X1),'sub$u0'), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 58.89/9.20 cnf(c568, 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])).
% 58.89/9.20 cnf(d0, plain, ~obj(X0,X1) | ~sub(sK282(X2,X3,X4),X5) | ~sub(X6,'familiename$u1$u1') | ~sub(X7,'name$u1$u1') | ~sub(X8,'eigenname$u1$u1') | ~attr(X9,X7) | ~attr(X1,X6) | ~attr(X1,X8) | ~val(X6,'mandela$u0') | ~val(X7,'s$u$u374dafrika$u0') | ~val(X8,'nelson$u0') | ~arg1(sK281(X2,X3,X4),X1) | ~subr(sK281(X2,X3,X4),'rprs$u0') | ~'Ts276'(X2,X3,X4), inference(resolution, [status(thm)], [c568,c498])).
% 58.89/9.20 cnf(d1, plain, ~obj(X0,X1) | ~sub(X2,'eigenname$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'familiename$u1$u1') | ~sub(sK282(X5,X6,X7),X8) | ~attr(X9,X3) | ~attr(X1,X2) | ~attr(X1,X4) | ~val(X2,'nelson$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'mandela$u0') | ~arg1(sK281(X5,X6,X7),X1) | ~'Ts276'(X5,X6,X7) | ~'Ts276'(X5,X6,X7), inference(resolution, [status(thm)], [d0,c503])).
% 58.89/9.20 cnf(d2, plain, ~obj(X0,X1) | ~sub(X2,'familiename$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'eigenname$u1$u1') | ~sub(sK282(X5,X1,X6),X7) | ~attr(X8,X3) | ~attr(X1,X2) | ~attr(X1,X4) | ~val(X2,'mandela$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'nelson$u0') | ~'Ts276'(X5,X1,X6) | ~'Ts276'(X5,X1,X6), inference(resolution, [status(thm)], [d1,c497])).
% 58.89/9.20 cnf(d3, plain, ~obj(X0,X1) | ~sub(X2,'eigenname$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'familiename$u1$u1') | ~attr(X5,X3) | ~attr(X1,X2) | ~attr(X1,X4) | ~val(X2,'nelson$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'mandela$u0') | ~'Ts276'(X6,X1,X7) | ~'Ts276'(X6,X1,X7), inference(resolution, [status(thm)], [d2,c502])).
% 58.89/9.20 cnf(d4, plain, ~obj(X0,X1) | ~sub(X2,'familiename$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'eigenname$u1$u1') | ~attr(X5,X3) | ~attr(X1,X2) | ~attr(X1,X4) | ~val(X2,'mandela$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'nelson$u0') | ~arg1(X6,X1) | ~subr(X6,'sub$u0') | ~arg2(X6,X7), inference(resolution, [status(thm)], [d3,c496])).
% 58.89/9.20 cnf(d5, plain, ~obj(X0,X1) | ~sub(X2,'eigenname$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'familiename$u1$u1') | ~attr(X5,X3) | ~attr(X1,X2) | ~attr(X1,X4) | ~val(X2,'nelson$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'mandela$u0') | ~arg1(sK285(X6,X7),X1) | ~subr(sK285(X6,X7),'sub$u0') | ~sub(X6,X7), inference(resolution, [status(thm)], [d4,c506])).
% 58.89/9.20 cnf(d6, plain, ~obj(X0,X1) | ~sub(X2,X3) | ~sub(X4,'familiename$u1$u1') | ~sub(X5,'name$u1$u1') | ~sub(X6,'eigenname$u1$u1') | ~attr(X7,X5) | ~attr(X1,X4) | ~attr(X1,X6) | ~val(X4,'mandela$u0') | ~val(X5,'s$u$u374dafrika$u0') | ~val(X6,'nelson$u0') | ~arg1(sK285(X2,X3),X1) | ~sub(X2,X3), inference(resolution, [status(thm)], [d5,c507])).
% 58.89/9.20 cnf(d7, plain, ~obj(X0,X1) | ~sub(X2,'eigenname$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'familiename$u1$u1') | ~sub(X1,X5) | ~attr(X6,X3) | ~attr(X1,X2) | ~attr(X1,X4) | ~val(X2,'nelson$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'mandela$u0') | ~sub(X1,X5), inference(resolution, [status(thm)], [d6,c505])).
% 58.89/9.20 cnf(d8, plain, ~obj(X0,X1) | ~sub(X2,'familiename$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(c55,'eigenname$u1$u1') | ~sub(X1,X4) | ~attr(X5,X3) | ~attr(X1,X2) | ~attr(X1,c55) | ~val(X2,'mandela$u0') | ~val(X3,'s$u$u374dafrika$u0'), inference(resolution, [status(thm)], [d7,c36])).
% 58.89/9.20 cnf(d9, plain, ~obj(X0,X1) | ~sub(X2,'name$u1$u1') | ~sub(X3,'familiename$u1$u1') | ~sub(X1,X4) | ~attr(X5,X2) | ~attr(X1,X3) | ~attr(X1,c55) | ~val(X2,'s$u$u374dafrika$u0') | ~val(X3,'mandela$u0'), inference(resolution, [status(thm)], [c35,d8])).
% 58.89/9.20 cnf(d10, plain, ~obj(X0,X1) | ~sub(X2,'familiename$u1$u1') | ~sub(c47,'name$u1$u1') | ~sub(X1,X3) | ~attr(X4,c47) | ~attr(X1,X2) | ~attr(X1,c55) | ~val(X2,'mandela$u0'), inference(resolution, [status(thm)], [d9,c31])).
% 58.89/9.20 cnf(d11, plain, ~obj(X0,X1) | ~sub(X2,'familiename$u1$u1') | ~sub(X1,X3) | ~attr(X4,c47) | ~attr(X1,X2) | ~attr(X1,c55) | ~val(X2,'mandela$u0'), inference(resolution, [status(thm)], [c30,d10])).
% 58.89/9.20 cnf(d12, plain, ~obj(X0,X1) | ~sub(c56,'familiename$u1$u1') | ~sub(X1,X2) | ~attr(X3,c47) | ~attr(X1,c56) | ~attr(X1,c55), inference(resolution, [status(thm)], [d11,c38])).
% 58.89/9.20 cnf(d13, plain, ~obj(X0,X1) | ~sub(X1,X2) | ~attr(X3,c47) | ~attr(X1,c55) | ~attr(X1,c56), inference(resolution, [status(thm)], [c37,d12])).
% 58.89/9.20 cnf(d14, plain, ~obj(X0,c54) | ~sub(c54,X1) | ~attr(X2,c47) | ~attr(c54,c55), inference(resolution, [status(thm)], [d13,c33])).
% 58.89/9.20 cnf(d15, plain, ~obj(X0,c54) | ~sub(c54,X1) | ~attr(X2,c47), inference(resolution, [status(thm)], [c32,d14])).
% 58.89/9.20 cnf(d16, plain, ~obj(X0,c54) | ~sub(c54,X1), inference(resolution, [status(thm)], [d15,c28])).
% 58.89/9.20 cnf(d17, plain, ~obj(X0,c54), inference(resolution, [status(thm)], [d16,c34])).
% 58.89/9.20 cnf(d18, plain, $false, inference(resolution, [status(thm)], [d17,c12])).
% 58.89/9.20 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------