%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR116+6 : 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:56 AM UTC 2026
% Result : Theorem 71.69s 11.11s
% Output : CNFRefutation 71.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR116+6 : 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.08/0.34 % Computer : n019.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 27 01:16:33 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 71.69/11.11 % SZS status Theorem for theBenchmark.p
% 71.69/11.11 % SZS output start CNFRefutation for theBenchmark.p
% 71.69/11.11 fof(ave07_era5_synth_qa07_010_mira_news_1607, hypothesis, (assoc('amtantritt$u1$u1','amt$u1$u2') & (assoc('apartheid$u1$u1','rasse$u1$u1') & (subs('apartheid$u1$u1','trennung$u1$u1') & (preds(c103,c105) & (prop(c103,'allgemein$u1$u1') & (pmod(c105,'erst$u1$u1','wahl$u1$u1') & (sub(c108,'abschlu$u$u337$u1$u1') & (assoc(c109,c108) & (sub(c109,'april$u$u1$u1') & (agt(c11,c17) & (mode(c11,c6) & (obj(c11,c21) & (sourc(c11,c28) & (subs(c11,'ziehen$u1$u1') & (subs(c115,'amtantritt$u1$u1') & (attch(c124,c163) & (attr(c124,c125) & (attr(c124,c126) & (prop(c124,'neo$u1$u1') & (sub(c124,'pr$u$u344sident$u1$u1') & (sub(c125,'eigenname$u1$u1') & (val(c125,'nelson$u0') & (sub(c126,'familiename$u1$u1') & (val(c126,'mandela$u0') & (poss(c14,c6) & (attch(c146,c163) & (attr(c146,c147) & (prop(c146,'afrikanisch$u$u1$u1') & (sub(c146,'nationalkongre$u$u337$u1$u1') & (sub(c146,'schwarzen$uorganisation$u1$u1') & (sub(c147,'name$u1$u1') & (val(c147,'anc$u0') & (cstr(c150,c103) & (obj(c150,c38) & (subs(c150,'besiegeln$u1$u1') & (itms(c163,c109,c115) & (attch(c163,c103) & (in(c165,c38) & (sub(c17,'sicherheitrat$u1$u1') & (sub(c21,'konsequenz$u1$u1') & (sub(c28,'abschlu$u$u337$u1$u1') & (attch(c32,c28) & (loc(c32,c165) & (subs(c32,'apartheid$u1$u1') & (attr(c38,c39) & (sub(c38,'land$u1$u1') & (sub(c39,'name$u1$u1') & (val(c39,'s$u$u374dafrika$u0') & (pred(c6,'beschlu$u$u337$u1$u1') & (assoc('nationalkongre$u$u337$u1$u1','national$u$u1$u1') & (sub('nationalkongre$u$u337$u1$u1','kongre$u$u337$u1$u1') & (assoc('schwarzen$uorganisation$u1$u1','schwarzen$u0') & (sub('schwarzen$uorganisation$u1$u1','organisation$u1$u1') & (assoc('sicherheitrat$u1$u1','sicherheit$u1$u1') & (sub('sicherheitrat$u1$u1','rat$u2$u1') & (sort('amtantritt$u1$u1',ad) & (card('amtantritt$u1$u1',int1) & (etype('amtantritt$u1$u1',int0) & (fact('amtantritt$u1$u1',real) & (gener('amtantritt$u1$u1',ge) & (quant('amtantritt$u1$u1',one) & (refer('amtantritt$u1$u1','refer$uc') & (varia('amtantritt$u1$u1','varia$uc') & (sort('amt$u1$u2',ad) & (sort('amt$u1$u2',io) & (card('amt$u1$u2',int1) & (etype('amt$u1$u2',int0) & (fact('amt$u1$u2',real) & (gener('amt$u1$u2',ge) & (quant('amt$u1$u2',one) & (refer('amt$u1$u2','refer$uc') & (varia('amt$u1$u2','varia$uc') & (sort('apartheid$u1$u1',ad) & (card('apartheid$u1$u1',int1) & (etype('apartheid$u1$u1',int0) & (fact('apartheid$u1$u1',real) & (gener('apartheid$u1$u1',ge) & (quant('apartheid$u1$u1',one) & (refer('apartheid$u1$u1','refer$uc') & (varia('apartheid$u1$u1','varia$uc') & (sort('rasse$u1$u1',io) & (card('rasse$u1$u1',int1) & (etype('rasse$u1$u1',int0) & (fact('rasse$u1$u1',real) & (gener('rasse$u1$u1',ge) & (quant('rasse$u1$u1',one) & (refer('rasse$u1$u1','refer$uc') & (varia('rasse$u1$u1','varia$uc') & (sort('trennung$u1$u1',ad) & (card('trennung$u1$u1',int1) & (etype('trennung$u1$u1',int0) & (fact('trennung$u1$u1',real) & (gener('trennung$u1$u1',ge) & (quant('trennung$u1$u1',one) & (refer('trennung$u1$u1','refer$uc') & (varia('trennung$u1$u1','varia$uc') & (sort(c103,ad) & (card(c103,cons('x$uconstant',cons(int1,nil))) & (etype(c103,int1) & (fact(c103,real) & (gener(c103,sp) & (quant(c103,mult) & (refer(c103,det) & (varia(c103,con) & (sort(c105,ad) & (card(c105,int1) & (etype(c105,int0) & (fact(c105,real) & (gener(c105,ge) & (quant(c105,one) & (refer(c105,'refer$uc') & (varia(c105,'varia$uc') & (sort('allgemein$u1$u1',nq) & (sort('erst$u1$u1',oq) & (card('erst$u1$u1',int1) & (sort('wahl$u1$u1',ad) & (card('wahl$u1$u1',int1) & (etype('wahl$u1$u1',int0) & (fact('wahl$u1$u1',real) & (gener('wahl$u1$u1',ge) & (quant('wahl$u1$u1',one) & (refer('wahl$u1$u1','refer$uc') & (varia('wahl$u1$u1','varia$uc') & (sort(c108,ad) & (sort(c108,io) & (card(c108,int1) & (etype(c108,int0) & (fact(c108,real) & (gener(c108,'gener$uc') & (quant(c108,one) & (refer(c108,'refer$uc') & (varia(c108,'varia$uc') & (sort('abschlu$u$u337$u1$u1',ad) & (sort('abschlu$u$u337$u1$u1',io) & (card('abschlu$u$u337$u1$u1',int1) & (etype('abschlu$u$u337$u1$u1',int0) & (fact('abschlu$u$u337$u1$u1',real) & (gener('abschlu$u$u337$u1$u1',ge) & (quant('abschlu$u$u337$u1$u1',one) & (refer('abschlu$u$u337$u1$u1','refer$uc') & (varia('abschlu$u$u337$u1$u1','varia$uc') & (sort(c109,ta) & (card(c109,int1) & (etype(c109,int0) & (fact(c109,real) & (gener(c109,'gener$uc') & (quant(c109,one) & (refer(c109,'refer$uc') & (varia(c109,'varia$uc') & (sort('april$u$u1$u1',ta) & (card('april$u$u1$u1',int1) & (etype('april$u$u1$u1',int0) & (fact('april$u$u1$u1',real) & (gener('april$u$u1$u1',ge) & (quant('april$u$u1$u1',one) & (refer('april$u$u1$u1','refer$uc') & (varia('april$u$u1$u1','varia$uc') & (sort(c11,da) & (fact(c11,real) & (gener(c11,sp) & (sort(c17,io) & (card(c17,int1) & (etype(c17,int1) & (fact(c17,real) & (gener(c17,sp) & (quant(c17,one) & (refer(c17,det) & (varia(c17,con) & (sort(c6,ad) & (sort(c6,d) & (sort(c6,io) & (card(c6,cons('x$uconstant',cons(int1,nil))) & (etype(c6,int1) & (fact(c6,real) & (gener(c6,sp) & (quant(c6,mult) & (refer(c6,det) & (varia(c6,'varia$uc') & (sort(c21,ad) & (sort(c21,io) & (card(c21,int1) & (etype(c21,int0) & (fact(c21,real) & (gener(c21,sp) & (quant(c21,one) & (refer(c21,det) & (varia(c21,con) & (sort(c28,ad) & (sort(c28,io) & (card(c28,int1) & (etype(c28,int0) & (fact(c28,real) & (gener(c28,sp) & (quant(c28,one) & (refer(c28,det) & (varia(c28,con) & (sort('ziehen$u1$u1',da) & (fact('ziehen$u1$u1',real) & (gener('ziehen$u1$u1',ge) & (sort(c115,ad) & (card(c115,int1) & (etype(c115,int0) & (fact(c115,real) & (gener(c115,sp) & (quant(c115,one) & (refer(c115,det) & (varia(c115,con) & (sort(c124,d) & (card(c124,int1) & (etype(c124,int0) & (fact(c124,real) & (gener(c124,sp) & (quant(c124,one) & (refer(c124,det) & (varia(c124,con) & (sort(c163,ab) & (card(c163,int2) & (etype(c163,int1) & (fact(c163,real) & (gener(c163,'gener$uc') & (quant(c163,nfquant) & (refer(c163,'refer$uc') & (varia(c163,'varia$uc') & (sort(c125,na) & (card(c125,int1) & (etype(c125,int0) & (fact(c125,real) & (gener(c125,sp) & (quant(c125,one) & (refer(c125,indet) & (varia(c125,'varia$uc') & (sort(c126,na) & (card(c126,int1) & (etype(c126,int0) & (fact(c126,real) & (gener(c126,sp) & (quant(c126,one) & (refer(c126,indet) & (varia(c126,'varia$uc') & (sort('neo$u1$u1',nq) & (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(c14,o) & (card(c14,int1) & (etype(c14,int0) & (fact(c14,real) & (gener(c14,sp) & (quant(c14,one) & (refer(c14,det) & (varia(c14,'varia$uc') & (sort(c146,d) & (sort(c146,io) & (card(c146,int1) & (etype(c146,int1) & (fact(c146,real) & (gener(c146,sp) & (quant(c146,one) & (refer(c146,det) & (varia(c146,con) & (sort(c147,na) & (card(c147,int1) & (etype(c147,int0) & (fact(c147,real) & (gener(c147,sp) & (quant(c147,one) & (refer(c147,indet) & (varia(c147,'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('schwarzen$uorganisation$u1$u1',d) & (sort('schwarzen$uorganisation$u1$u1',io) & (card('schwarzen$uorganisation$u1$u1','card$uc') & (etype('schwarzen$uorganisation$u1$u1',int1) & (fact('schwarzen$uorganisation$u1$u1',real) & (gener('schwarzen$uorganisation$u1$u1',ge) & (quant('schwarzen$uorganisation$u1$u1','quant$uc') & (refer('schwarzen$uorganisation$u1$u1','refer$uc') & (varia('schwarzen$uorganisation$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(c150,da) & (fact(c150,real) & (gener(c150,sp) & (sort(c38,d) & (sort(c38,io) & (card(c38,int1) & (etype(c38,int0) & (fact(c38,real) & (gener(c38,sp) & (quant(c38,one) & (refer(c38,det) & (varia(c38,con) & (sort('besiegeln$u1$u1',da) & (fact('besiegeln$u1$u1',real) & (gener('besiegeln$u1$u1',ge) & (sort(c165,l) & (card(c165,int1) & (etype(c165,int0) & (fact(c165,real) & (gener(c165,sp) & (quant(c165,one) & (refer(c165,det) & (varia(c165,con) & (sort('sicherheitrat$u1$u1',io) & (card('sicherheitrat$u1$u1','card$uc') & (etype('sicherheitrat$u1$u1',int1) & (fact('sicherheitrat$u1$u1',real) & (gener('sicherheitrat$u1$u1',ge) & (quant('sicherheitrat$u1$u1','quant$uc') & (refer('sicherheitrat$u1$u1','refer$uc') & (varia('sicherheitrat$u1$u1','varia$uc') & (sort('konsequenz$u1$u1',ad) & (sort('konsequenz$u1$u1',io) & (card('konsequenz$u1$u1',int1) & (etype('konsequenz$u1$u1',int0) & (fact('konsequenz$u1$u1',real) & (gener('konsequenz$u1$u1',ge) & (quant('konsequenz$u1$u1',one) & (refer('konsequenz$u1$u1','refer$uc') & (varia('konsequenz$u1$u1','varia$uc') & (sort(c32,ad) & (card(c32,int1) & (etype(c32,int0) & (fact(c32,real) & (gener(c32,sp) & (quant(c32,one) & (refer(c32,det) & (varia(c32,con) & (sort(c39,na) & (card(c39,int1) & (etype(c39,int0) & (fact(c39,real) & (gener(c39,sp) & (quant(c39,one) & (refer(c39,indet) & (varia(c39,'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('beschlu$u$u337$u1$u1',ad) & (sort('beschlu$u$u337$u1$u1',d) & (sort('beschlu$u$u337$u1$u1',io) & (card('beschlu$u$u337$u1$u1',int1) & (etype('beschlu$u$u337$u1$u1',int0) & (fact('beschlu$u$u337$u1$u1',real) & (gener('beschlu$u$u337$u1$u1',ge) & (quant('beschlu$u$u337$u1$u1',one) & (refer('beschlu$u$u337$u1$u1','refer$uc') & (varia('beschlu$u$u337$u1$u1','varia$uc') & (sort('national$u$u1$u1',nq) & (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('schwarzen$u0',fe) & (sort('organisation$u1$u1',d) & (sort('organisation$u1$u1',io) & (card('organisation$u1$u1','card$uc') & (etype('organisation$u1$u1',int1) & (fact('organisation$u1$u1',real) & (gener('organisation$u1$u1',ge) & (quant('organisation$u1$u1','quant$uc') & (refer('organisation$u1$u1','refer$uc') & (varia('organisation$u1$u1','varia$uc') & (sort('sicherheit$u1$u1',as) & (sort('sicherheit$u1$u1',io) & (card('sicherheit$u1$u1',int1) & (etype('sicherheit$u1$u1',int0) & (fact('sicherheit$u1$u1',real) & (gener('sicherheit$u1$u1',ge) & (quant('sicherheit$u1$u1',one) & (refer('sicherheit$u1$u1','refer$uc') & (varia('sicherheit$u1$u1','varia$uc') & (sort('rat$u2$u1',d) & (sort('rat$u2$u1',io) & (card('rat$u2$u1','card$uc') & (etype('rat$u2$u1',int1) & (fact('rat$u2$u1',real) & (gener('rat$u2$u1',ge) & (quant('rat$u2$u1','quant$uc') & (refer('rat$u2$u1','refer$uc') & varia('rat$u2$u1','varia$uc')))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 71.69/11.11 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')))))))))))).
% 71.69/11.11 fof(sub__sub_0_expansion, axiom, ! [X0] : ! [X1] : ((sub(X0,X1) => ? [X2] : ((arg1(X2,X0) & (arg2(X2,X1) & subr(X2,'sub$u0'))))))).
% 71.69/11.11 fof(synth_qa07_010_mira_news_1607, conjecture, ? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ? [X8] : ? [X9] : ((in(X5,X6) & (arg1(X3,X0) & (arg2(X3,X4) & (attr(X0,X1) & (attr(X0,X2) & (attr(X6,X7) & (obj(X8,X0) & (sub(X1,'familiename$u1$u1') & (sub(X2,'eigenname$u1$u1') & (sub(X4,X9) & (sub(X7,'name$u1$u1') & (subr(X3,'rprs$u0') & (val(X1,'mandela$u0') & (val(X2,'nelson$u0') & val(X7,'s$u$u374dafrika$u0'))))))))))))))))).
% 71.69/11.11 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ? [X7] : ? [X8] : ? [X9] : ((in(X5,X6) & (arg1(X3,X0) & (arg2(X3,X4) & (attr(X0,X1) & (attr(X0,X2) & (attr(X6,X7) & (obj(X8,X0) & (sub(X1,'familiename$u1$u1') & (sub(X2,'eigenname$u1$u1') & (sub(X4,X9) & (sub(X7,'name$u1$u1') & (subr(X3,'rprs$u0') & (val(X1,'mandela$u0') & (val(X2,'nelson$u0') & val(X7,'s$u$u374dafrika$u0')))))))))))))))), inference(negate_conjecture, [status(cth)], [synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c16, plain, attr(c124,c125), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c17, plain, attr(c124,c126), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c19, plain, sub(c124,'pr$u$u344sident$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c20, plain, sub(c125,'eigenname$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c21, plain, val(c125,'nelson$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c22, plain, sub(c126,'familiename$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c23, plain, val(c126,'mandela$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c37, plain, in(c165,c38), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c44, plain, attr(c38,c39), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c46, plain, sub(c39,'name$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c47, plain, val(c39,'s$u$u374dafrika$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1607])).
% 71.69/11.11 cnf(c589, plain, ~arg1(X0,X1) | ~arg2(X0,X2) | ~subr(X0,'sub$u0') | X3(X0,X1,X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 71.69/11.11 cnf(c590, plain, ~X0(X1,X2,X3) | arg1(sK219(X1,X2,X3),X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 71.69/11.11 cnf(c591, plain, ~X0(X1,X2,X3) | arg2(sK219(X1,X2,X3),sK220(X1,X2,X3)), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 71.69/11.11 cnf(c594, plain, ~X0(X1,X2,X3) | obj(sK218(X1,X2,X3),X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 71.69/11.11 cnf(c595, plain, ~X0(X1,X2,X3) | sub(sK220(X1,X2,X3),X3), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 71.69/11.11 cnf(c596, plain, ~X0(X1,X2,X3) | subr(sK219(X1,X2,X3),'rprs$u0'), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 71.69/11.11 cnf(c598, plain, ~sub(X0,X1) | arg1(sK223(X0,X1),X0), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 71.69/11.11 cnf(c599, plain, ~sub(X0,X1) | arg2(sK223(X0,X1),X1), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 71.69/11.11 cnf(c600, plain, ~sub(X0,X1) | subr(sK223(X0,X1),'sub$u0'), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 71.69/11.11 cnf(c666, plain, ~sub(X0,'eigenname$u1$u1') | ~arg1(X1,X2) | ~attr(X2,X0) | ~sub(X3,'name$u1$u1') | ~in(X4,X5) | ~sub(X6,'familiename$u1$u1') | ~val(X6,'mandela$u0') | ~attr(X2,X6) | ~arg2(X1,X7) | ~val(X0,'nelson$u0') | ~subr(X1,'rprs$u0') | ~attr(X5,X3) | ~val(X3,'s$u$u374dafrika$u0') | ~sub(X7,X8) | ~obj(X9,X2), inference(clausification, [status(esa)], [negated_conjecture])).
% 71.69/11.11 cnf(d0, plain, ~sub(X0,'eigenname$u1$u1') | ~sub(sK220(X1,X2,X3),X4) | ~sub(X5,'name$u1$u1') | ~sub(X6,'familiename$u1$u1') | ~obj(X7,X8) | ~attr(X9,X5) | ~attr(X8,X0) | ~attr(X8,X6) | ~val(X0,'nelson$u0') | ~val(X5,'s$u$u374dafrika$u0') | ~val(X6,'mandela$u0') | ~in(X10,X9) | ~arg1(sK219(X1,X2,X3),X8) | ~subr(sK219(X1,X2,X3),'rprs$u0') | ~'Ts214'(X1,X2,X3), inference(resolution, [status(thm)], [c666,c591])).
% 71.69/11.11 cnf(d1, plain, ~sub(X0,'familiename$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'eigenname$u1$u1') | ~sub(sK220(X3,X4,X5),X6) | ~obj(X7,X8) | ~attr(X9,X1) | ~attr(X8,X0) | ~attr(X8,X2) | ~val(X0,'mandela$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'nelson$u0') | ~in(X10,X9) | ~arg1(sK219(X3,X4,X5),X8) | ~'Ts214'(X3,X4,X5) | ~'Ts214'(X3,X4,X5), inference(resolution, [status(thm)], [d0,c596])).
% 71.69/11.11 cnf(d2, plain, ~sub(X0,'eigenname$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(sK220(X3,X4,X5),X6) | ~obj(X7,X4) | ~attr(X8,X1) | ~attr(X4,X0) | ~attr(X4,X2) | ~val(X0,'nelson$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'mandela$u0') | ~in(X9,X8) | ~'Ts214'(X3,X4,X5) | ~'Ts214'(X3,X4,X5), inference(resolution, [status(thm)], [d1,c590])).
% 71.69/11.11 cnf(d3, plain, ~sub(X0,'familiename$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'eigenname$u1$u1') | ~obj(X3,X4) | ~attr(X5,X1) | ~attr(X4,X0) | ~attr(X4,X2) | ~val(X0,'mandela$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'nelson$u0') | ~in(X6,X5) | ~'Ts214'(X7,X4,X8) | ~'Ts214'(X7,X4,X8), inference(resolution, [status(thm)], [d2,c595])).
% 71.69/11.11 cnf(d4, plain, ~sub(X0,'eigenname$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~obj(X3,X4) | ~attr(X5,X1) | ~attr(X4,X0) | ~attr(X4,X2) | ~val(X0,'nelson$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'mandela$u0') | ~in(X6,X5) | ~arg1(X7,X4) | ~subr(X7,'sub$u0') | ~arg2(X7,X8), inference(resolution, [status(thm)], [d3,c589])).
% 71.69/11.11 cnf(d5, plain, ~sub(X0,'familiename$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'eigenname$u1$u1') | ~obj(X3,X4) | ~attr(X5,X1) | ~attr(X4,X0) | ~attr(X4,X2) | ~val(X0,'mandela$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'nelson$u0') | ~in(X6,X5) | ~arg1(sK223(X7,X8),X4) | ~subr(sK223(X7,X8),'sub$u0') | ~sub(X7,X8), inference(resolution, [status(thm)], [d4,c599])).
% 71.69/11.11 cnf(d6, plain, ~sub(X0,X1) | ~sub(X2,'eigenname$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'familiename$u1$u1') | ~obj(X5,X6) | ~attr(X7,X3) | ~attr(X6,X2) | ~attr(X6,X4) | ~val(X2,'nelson$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'mandela$u0') | ~in(X8,X7) | ~arg1(sK223(X0,X1),X6) | ~sub(X0,X1), inference(resolution, [status(thm)], [d5,c600])).
% 71.69/11.11 cnf(d7, plain, ~sub(X0,'familiename$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'eigenname$u1$u1') | ~sub(X3,X4) | ~obj(X5,X3) | ~attr(X6,X1) | ~attr(X3,X0) | ~attr(X3,X2) | ~val(X0,'mandela$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X2,'nelson$u0') | ~in(X7,X6) | ~sub(X3,X4), inference(resolution, [status(thm)], [d6,c598])).
% 71.69/11.11 cnf(d8, plain, ~sub(X0,X1) | ~sub(X2,'eigenname$u1$u1') | ~sub(X3,'name$u1$u1') | ~sub(X4,'familiename$u1$u1') | ~obj(X5,X0) | ~attr(c38,X3) | ~attr(X0,X2) | ~attr(X0,X4) | ~val(X2,'nelson$u0') | ~val(X3,'s$u$u374dafrika$u0') | ~val(X4,'mandela$u0'), inference(resolution, [status(thm)], [d7,c37])).
% 71.69/11.11 cnf(d9, plain, ~sub(X0,'familiename$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(c125,'eigenname$u1$u1') | ~sub(X2,X3) | ~obj(X4,X2) | ~attr(X2,X0) | ~attr(X2,c125) | ~attr(c38,X1) | ~val(X0,'mandela$u0') | ~val(X1,'s$u$u374dafrika$u0'), inference(resolution, [status(thm)], [d8,c21])).
% 71.69/11.11 cnf(d10, plain, ~sub(X0,X1) | ~sub(X2,'name$u1$u1') | ~sub(X3,'familiename$u1$u1') | ~obj(X4,X0) | ~attr(X0,X3) | ~attr(X0,c125) | ~attr(c38,X2) | ~val(X2,'s$u$u374dafrika$u0') | ~val(X3,'mandela$u0'), inference(resolution, [status(thm)], [c20,d9])).
% 71.69/11.11 cnf(d11, plain, ~sub(X0,'familiename$u1$u1') | ~sub(c39,'name$u1$u1') | ~sub(X1,X2) | ~obj(X3,X1) | ~attr(X1,X0) | ~attr(X1,c125) | ~attr(c38,c39) | ~val(X0,'mandela$u0'), inference(resolution, [status(thm)], [d10,c47])).
% 71.69/11.11 cnf(d12, plain, ~sub(X0,X1) | ~sub(X2,'familiename$u1$u1') | ~sub(c39,'name$u1$u1') | ~obj(X3,X0) | ~attr(X0,X2) | ~attr(X0,c125) | ~val(X2,'mandela$u0'), inference(resolution, [status(thm)], [c44,d11])).
% 71.69/11.11 cnf(d13, plain, ~sub(X0,'familiename$u1$u1') | ~sub(X1,X2) | ~obj(X3,X1) | ~attr(X1,X0) | ~attr(X1,c125) | ~val(X0,'mandela$u0'), inference(resolution, [status(thm)], [c46,d12])).
% 71.69/11.11 cnf(d14, plain, ~sub(X0,X1) | ~sub(c126,'familiename$u1$u1') | ~obj(X2,X0) | ~attr(X0,c126) | ~attr(X0,c125), inference(resolution, [status(thm)], [d13,c23])).
% 71.69/11.11 cnf(d15, plain, ~sub(X0,X1) | ~obj(X2,X0) | ~attr(X0,c125) | ~attr(X0,c126), inference(resolution, [status(thm)], [c22,d14])).
% 71.69/11.11 cnf(d16, plain, ~sub(c124,X0) | ~obj(X1,c124) | ~attr(c124,c125), inference(resolution, [status(thm)], [d15,c17])).
% 71.69/11.11 cnf(d17, plain, ~sub(c124,X0) | ~obj(X1,c124), inference(resolution, [status(thm)], [c16,d16])).
% 71.69/11.11 cnf(d18, plain, ~sub(c124,X0) | ~'Ts214'(X1,c124,X2), inference(resolution, [status(thm)], [d17,c594])).
% 71.69/11.11 cnf(d19, plain, ~sub(c124,X0) | ~arg1(X1,c124) | ~subr(X1,'sub$u0') | ~arg2(X1,X2), inference(resolution, [status(thm)], [d18,c589])).
% 71.69/11.11 cnf(d20, plain, ~sub(c124,X0) | ~arg1(sK223(X1,X2),c124) | ~subr(sK223(X1,X2),'sub$u0') | ~sub(X1,X2), inference(resolution, [status(thm)], [d19,c599])).
% 71.69/11.11 cnf(d21, plain, ~sub(X0,X1) | ~sub(c124,X2) | ~arg1(sK223(X0,X1),c124) | ~sub(X0,X1), inference(resolution, [status(thm)], [d20,c600])).
% 71.69/11.11 cnf(d22, plain, ~sub(c124,X0) | ~sub(c124,X1) | ~sub(c124,X0), inference(resolution, [status(thm)], [d21,c598])).
% 71.69/11.11 cnf(d23, plain, ~sub(c124,X0), inference(resolution, [status(thm)], [d22,c19])).
% 71.69/11.11 cnf(d24, plain, $false, inference(resolution, [status(thm)], [d23,c19])).
% 71.69/11.11 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------