%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR116+25 : 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 : n005.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:53 AM UTC 2026
% Result : Theorem 91.02s 21.20s
% Output : CNFRefutation 91.02s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR116+25 : 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.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 27 01:14:31 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 91.02/21.20 % SZS status Theorem for theBenchmark.p
% 91.02/21.20 % SZS output start CNFRefutation for theBenchmark.p
% 91.02/21.20 fof(ave07_era5_synth_qa07_010_mira_news_1794, hypothesis, ('tupl$up5'(c156,c69,c75,c85,c91) & (prop(c661,'afrikanisch$u$u1$u1') & (subs(c661,'nationalkongre$u$u337$u2$u1') & (attr(c667,c668) & (sub(c667,'einrichtung$u1$u2') & (sub(c668,'name$u1$u1') & (val(c668,'anc$u0') & (attr(c676,c677) & (attr(c676,c678) & (prop(c676,'s$u$u374dafrikanisch$u1$u1') & (sub(c676,'pr$u$u344sident$u1$u1') & (sub(c677,'eigenname$u1$u1') & (val(c677,'nelson$u0') & (sub(c678,'familiename$u1$u1') & (val(c678,'mandela$u0') & (pred(c69,'wahlgewinner$u1$u1') & (attr(c691,c692) & (attr(c691,c693) & (sub(c692,'tag$u1$u1') & (val(c692,c689) & (sub(c693,'monat$u1$u1') & (val(c693,c690) & (subm(c696,c701) & (preds(c701,'stimme$u1$u1') & (attch(c71,c69) & (attr(c71,c72) & (sub(c71,'einrichtung$u1$u2') & (sub(c72,'name$u1$u1') & (val(c72,'anc$u0') & ('tupl$up7'(c732,c661,c667,c676,c75,c691,c696) & (preds(c75,'kommunalswahl$u1$u1') & (attch(c81,c85) & (attr(c81,c82) & (sub(c81,'land$u1$u1') & (sub(c82,'name$u1$u1') & (val(c82,'s$u$u374dafrika$u0') & (attr(c85,c86) & (sub(c85,'stadt$u$u1$u1') & (sub(c86,'name$u1$u1') & (val(c86,'johannesburg$u0') & (attr(c91,c92) & (attr(c91,c93) & (sub(c92,'tag$u1$u1') & (val(c92,c89) & (sub(c93,'monat$u1$u1') & (val(c93,c90) & (assoc('kommunalswahl$u1$u1','gemeindlich$u1$u1') & (subs('kommunalswahl$u1$u1','wahl$u1$u1') & (assoc('nationalkongre$u$u337$u2$u1','national$u$u1$u1') & (subs('nationalkongre$u$u337$u2$u1','kongre$u$u337$u2$u1') & (assoc('wahlgewinner$u1$u1','auswahl$u1$u1') & (sub('wahlgewinner$u1$u1','sieger$u$u1$u1') & (sort(c156,ent) & (card(c156,'card$uc') & (etype(c156,'etype$uc') & (fact(c156,real) & (gener(c156,'gener$uc') & (quant(c156,'quant$uc') & (refer(c156,'refer$uc') & (varia(c156,'varia$uc') & (sort(c69,d) & (sort(c69,io) & (card(c69,cons('x$uconstant',cons(int1,nil))) & (etype(c69,int1) & (fact(c69,real) & (gener(c69,sp) & (quant(c69,mult) & (refer(c69,indet) & (varia(c69,'varia$uc') & (sort(c75,ad) & (card(c75,cons('x$uconstant',cons(int1,nil))) & (etype(c75,int1) & (fact(c75,real) & (gener(c75,'gener$uc') & (quant(c75,mult) & (refer(c75,indet) & (varia(c75,'varia$uc') & (sort(c85,d) & (sort(c85,io) & (card(c85,int1) & (etype(c85,int0) & (fact(c85,real) & (gener(c85,sp) & (quant(c85,one) & (refer(c85,det) & (varia(c85,con) & (sort(c91,t) & (card(c91,int1) & (etype(c91,int0) & (fact(c91,real) & (gener(c91,sp) & (quant(c91,one) & (refer(c91,det) & (varia(c91,con) & (sort(c661,ad) & (card(c661,int1) & (etype(c661,int0) & (fact(c661,real) & (gener(c661,sp) & (quant(c661,one) & (refer(c661,det) & (varia(c661,con) & (sort('afrikanisch$u$u1$u1',nq) & (sort('nationalkongre$u$u337$u2$u1',ad) & (card('nationalkongre$u$u337$u2$u1',int1) & (etype('nationalkongre$u$u337$u2$u1',int0) & (fact('nationalkongre$u$u337$u2$u1',real) & (gener('nationalkongre$u$u337$u2$u1',ge) & (quant('nationalkongre$u$u337$u2$u1',one) & (refer('nationalkongre$u$u337$u2$u1','refer$uc') & (varia('nationalkongre$u$u337$u2$u1','varia$uc') & (sort(c667,d) & (sort(c667,io) & (card(c667,int1) & (etype(c667,int1) & (fact(c667,real) & (gener(c667,sp) & (quant(c667,one) & (refer(c667,det) & (varia(c667,con) & (sort(c668,na) & (card(c668,int1) & (etype(c668,int0) & (fact(c668,real) & (gener(c668,sp) & (quant(c668,one) & (refer(c668,indet) & (varia(c668,'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('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(c676,d) & (card(c676,int1) & (etype(c676,int0) & (fact(c676,real) & (gener(c676,sp) & (quant(c676,one) & (refer(c676,det) & (varia(c676,con) & (sort(c677,na) & (card(c677,int1) & (etype(c677,int0) & (fact(c677,real) & (gener(c677,sp) & (quant(c677,one) & (refer(c677,indet) & (varia(c677,'varia$uc') & (sort(c678,na) & (card(c678,int1) & (etype(c678,int0) & (fact(c678,real) & (gener(c678,sp) & (quant(c678,one) & (refer(c678,indet) & (varia(c678,'varia$uc') & (sort('s$u$u374dafrikanisch$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('wahlgewinner$u1$u1',d) & (sort('wahlgewinner$u1$u1',io) & (card('wahlgewinner$u1$u1',int1) & (etype('wahlgewinner$u1$u1',int0) & (fact('wahlgewinner$u1$u1',real) & (gener('wahlgewinner$u1$u1',ge) & (quant('wahlgewinner$u1$u1',one) & (refer('wahlgewinner$u1$u1','refer$uc') & (varia('wahlgewinner$u1$u1','varia$uc') & (sort(c691,t) & (card(c691,int1) & (etype(c691,int0) & (fact(c691,real) & (gener(c691,sp) & (quant(c691,one) & (refer(c691,det) & (varia(c691,con) & (sort(c692,me) & (sort(c692,oa) & (sort(c692,ta) & (card(c692,'card$uc') & (etype(c692,'etype$uc') & (fact(c692,real) & (gener(c692,sp) & (quant(c692,'quant$uc') & (refer(c692,'refer$uc') & (varia(c692,'varia$uc') & (sort(c693,me) & (sort(c693,oa) & (sort(c693,ta) & (card(c693,'card$uc') & (etype(c693,'etype$uc') & (fact(c693,real) & (gener(c693,sp) & (quant(c693,'quant$uc') & (refer(c693,'refer$uc') & (varia(c693,'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(c689,nu) & (card(c689,int1) & (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(c690,nu) & (card(c690,int11) & (sort(c696,ad) & (card(c696,'float0$u6666666666') & (etype(c696,int1) & (fact(c696,real) & (gener(c696,sp) & (quant(c696,nfquant) & (refer(c696,det) & (varia(c696,'varia$uc') & (sort(c701,ad) & (card(c701,cons('x$uconstant',cons(int1,nil))) & (etype(c701,int1) & (fact(c701,real) & (gener(c701,sp) & (quant(c701,mult) & (refer(c701,det) & (varia(c701,con) & (sort('stimme$u1$u1',ad) & (card('stimme$u1$u1',int1) & (etype('stimme$u1$u1',int0) & (fact('stimme$u1$u1',real) & (gener('stimme$u1$u1',ge) & (quant('stimme$u1$u1',one) & (refer('stimme$u1$u1','refer$uc') & (varia('stimme$u1$u1','varia$uc') & (sort(c71,d) & (sort(c71,io) & (card(c71,int1) & (etype(c71,int1) & (fact(c71,real) & (gener(c71,sp) & (quant(c71,one) & (refer(c71,det) & (varia(c71,con) & (sort(c72,na) & (card(c72,int1) & (etype(c72,int0) & (fact(c72,real) & (gener(c72,sp) & (quant(c72,one) & (refer(c72,indet) & (varia(c72,'varia$uc') & (sort(c732,ent) & (card(c732,'card$uc') & (etype(c732,'etype$uc') & (fact(c732,real) & (gener(c732,'gener$uc') & (quant(c732,'quant$uc') & (refer(c732,'refer$uc') & (varia(c732,'varia$uc') & (sort('kommunalswahl$u1$u1',ad) & (card('kommunalswahl$u1$u1',int1) & (etype('kommunalswahl$u1$u1',int0) & (fact('kommunalswahl$u1$u1',real) & (gener('kommunalswahl$u1$u1',ge) & (quant('kommunalswahl$u1$u1',one) & (refer('kommunalswahl$u1$u1','refer$uc') & (varia('kommunalswahl$u1$u1','varia$uc') & (sort(c81,d) & (sort(c81,io) & (card(c81,int1) & (etype(c81,int0) & (fact(c81,real) & (gener(c81,sp) & (quant(c81,one) & (refer(c81,det) & (varia(c81,con) & (sort(c82,na) & (card(c82,int1) & (etype(c82,int0) & (fact(c82,real) & (gener(c82,sp) & (quant(c82,one) & (refer(c82,indet) & (varia(c82,'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(c86,na) & (card(c86,int1) & (etype(c86,int0) & (fact(c86,real) & (gener(c86,sp) & (quant(c86,one) & (refer(c86,indet) & (varia(c86,'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('johannesburg$u0',fe) & (sort(c92,me) & (sort(c92,oa) & (sort(c92,ta) & (card(c92,'card$uc') & (etype(c92,'etype$uc') & (fact(c92,real) & (gener(c92,sp) & (quant(c92,'quant$uc') & (refer(c92,'refer$uc') & (varia(c92,'varia$uc') & (sort(c93,me) & (sort(c93,oa) & (sort(c93,ta) & (card(c93,'card$uc') & (etype(c93,'etype$uc') & (fact(c93,real) & (gener(c93,sp) & (quant(c93,'quant$uc') & (refer(c93,'refer$uc') & (varia(c93,'varia$uc') & (sort(c89,nu) & (card(c89,int5) & (sort(c90,nu) & (card(c90,int11) & (sort('gemeindlich$u1$u1',tq) & (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('national$u$u1$u1',nq) & (sort('kongre$u$u337$u2$u1',ad) & (card('kongre$u$u337$u2$u1',int1) & (etype('kongre$u$u337$u2$u1',int0) & (fact('kongre$u$u337$u2$u1',real) & (gener('kongre$u$u337$u2$u1',ge) & (quant('kongre$u$u337$u2$u1',one) & (refer('kongre$u$u337$u2$u1','refer$uc') & (varia('kongre$u$u337$u2$u1','varia$uc') & (sort('auswahl$u1$u1',as) & (card('auswahl$u1$u1',int1) & (etype('auswahl$u1$u1',int0) & (fact('auswahl$u1$u1',real) & (gener('auswahl$u1$u1',ge) & (quant('auswahl$u1$u1',one) & (refer('auswahl$u1$u1','refer$uc') & (varia('auswahl$u1$u1','varia$uc') & (sort('sieger$u$u1$u1',d) & (sort('sieger$u$u1$u1',io) & (card('sieger$u$u1$u1',int1) & (etype('sieger$u$u1$u1',int0) & (fact('sieger$u$u1$u1',real) & (gener('sieger$u$u1$u1',ge) & (quant('sieger$u$u1$u1',one) & (refer('sieger$u$u1$u1','refer$uc') & varia('sieger$u$u1$u1','varia$uc')))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 91.02/21.20 fof(member_first, axiom, ! [X0] : ! [X1] : member(X0,cons(X0,X1))).
% 91.02/21.20 fof(state_adjective__in_state, axiom, ! [X0] : ! [X1] : ! [X2] : (((prop(X0,X1) & 'state$uadjective$ustate$ubinding'(X1,X2)) => ? [X3] : ? [X4] : ? [X5] : ((in(X5,X3) & (attr(X3,X4) & (loc(X0,X5) & (sub(X3,'land$u1$u1') & (sub(X4,'name$u1$u1') & val(X4,X2)))))))))).
% 91.02/21.20 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'))))))).
% 91.02/21.20 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'))))))))))).
% 91.02/21.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')))))))))))).
% 91.02/21.20 fof(sub__sub_0_expansion, axiom, ! [X0] : ! [X1] : ((sub(X0,X1) => ? [X2] : ((arg1(X2,X0) & (arg2(X2,X1) & subr(X2,'sub$u0'))))))).
% 91.02/21.20 fof(fact_8980, axiom, 'state$uadjective$ustate$ubinding'('s$u$u374dafrikanisch$u1$u1','s$u$u374dafrika$u0')).
% 91.02/21.20 fof(synth_qa07_010_mira_news_1794, 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'))))))))))))))))).
% 91.02/21.20 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_1794])).
% 91.02/21.20 cnf(c7, plain, attr(c676,c677), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1794])).
% 91.02/21.20 cnf(c8, plain, attr(c676,c678), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1794])).
% 91.02/21.20 cnf(c9, plain, prop(c676,'s$u$u374dafrikanisch$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1794])).
% 91.02/21.20 cnf(c10, plain, sub(c676,'pr$u$u344sident$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1794])).
% 91.02/21.20 cnf(c11, plain, sub(c677,'eigenname$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1794])).
% 91.02/21.20 cnf(c12, plain, val(c677,'nelson$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1794])).
% 91.02/21.20 cnf(c13, plain, sub(c678,'familiename$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1794])).
% 91.02/21.20 cnf(c14, plain, val(c678,'mandela$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_mira_news_1794])).
% 91.02/21.20 cnf(c419, plain, member(X0,cons(X0,X1)), inference(clausification, [status(esa)], [member_first])).
% 91.02/21.20 cnf(c580, plain, ~prop(X0,X1) | ~'state$uadjective$ustate$ubinding'(X1,X2) | X3(X0,X2), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 91.02/21.20 cnf(c581, plain, ~X0(X1,X2) | in(sK218(X1,X2),sK216(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 91.02/21.20 cnf(c582, plain, ~X0(X1,X2) | attr(sK216(X1,X2),sK217(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 91.02/21.20 cnf(c585, plain, ~X0(X1,X2) | sub(sK217(X1,X2),'name$u1$u1'), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 91.02/21.20 cnf(c586, plain, ~X0(X1,X2) | val(sK217(X1,X2),X2), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 91.02/21.20 cnf(c589, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | arg1(sK232(X0),X0), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 91.02/21.20 cnf(c590, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | arg2(sK232(X0),X0), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 91.02/21.20 cnf(c591, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | subs(sK232(X0),'hei$u$u337en$u1$u1'), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 91.02/21.20 cnf(c592, 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])).
% 91.02/21.20 cnf(c597, plain, ~X0(X1,X2,X3) | obj(sK237(X1,X2,X3),X2), inference(clausification, [status(esa)], [hei__337en_1_1__bezeichnen_1_1_als])).
% 91.02/21.20 cnf(c600, plain, ~arg1(X0,X1) | ~arg2(X0,X2) | ~subr(X0,'sub$u0') | X3(X0,X1,X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 91.02/21.20 cnf(c601, plain, ~X0(X1,X2,X3) | arg1(sK244(X1,X2,X3),X2), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 91.02/21.20 cnf(c602, plain, ~X0(X1,X2,X3) | arg2(sK244(X1,X2,X3),sK245(X1,X2,X3)), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 91.02/21.20 cnf(c606, plain, ~X0(X1,X2,X3) | sub(sK245(X1,X2,X3),X3), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 91.02/21.20 cnf(c607, plain, ~X0(X1,X2,X3) | subr(sK244(X1,X2,X3),'rprs$u0'), inference(clausification, [status(esa)], [sub__bezeichnen_1_1_als])).
% 91.02/21.20 cnf(c609, plain, ~sub(X0,X1) | arg1(sK248(X0,X1),X0), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 91.02/21.20 cnf(c610, plain, ~sub(X0,X1) | arg2(sK248(X0,X1),X1), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 91.02/21.20 cnf(c611, plain, ~sub(X0,X1) | subr(sK248(X0,X1),'sub$u0'), inference(clausification, [status(esa)], [sub__sub_0_expansion])).
% 91.02/21.20 cnf(c660, plain, 'state$uadjective$ustate$ubinding'('s$u$u374dafrikanisch$u1$u1','s$u$u374dafrika$u0'), inference(clausification, [status(esa)], [fact_8980])).
% 91.02/21.20 cnf(c673, plain, ~obj(X0,X1) | ~sub(X2,'eigenname$u1$u1') | ~arg1(X3,X1) | ~attr(X1,X2) | ~val(X2,'nelson$u0') | ~sub(X4,'familiename$u1$u1') | ~sub(X5,X6) | ~attr(X7,X8) | ~sub(X8,'name$u1$u1') | ~attr(X1,X4) | ~val(X4,'mandela$u0') | ~arg2(X3,X5) | ~in(X9,X7) | ~val(X8,'s$u$u374dafrika$u0') | ~subr(X3,'rprs$u0'), inference(clausification, [status(esa)], [negated_conjecture])).
% 91.02/21.20 cnf(d0, plain, subs(sK232(X0),'hei$u$u337en$u1$u1') | ~attr(X0,X1) | ~sub(X1,'eigenname$u1$u1'), inference(resolution, [status(thm)], [c591,c419])).
% 91.02/21.20 cnf(d1, plain, subs(sK232(X0),'hei$u$u337en$u1$u1') | ~attr(X0,c677), inference(resolution, [status(thm)], [d0,c11])).
% 91.02/21.20 cnf(d2, plain, ~attr(X0,X1) | ~sub(X1,'eigenname$u1$u1') | arg1(sK232(X0),X0), inference(resolution, [status(thm)], [c589,c419])).
% 91.02/21.20 cnf(d3, plain, ~attr(X0,c677) | arg1(sK232(X0),X0), inference(resolution, [status(thm)], [d2,c11])).
% 91.02/21.20 cnf(d4, plain, ~prop(X0,'s$u$u374dafrikanisch$u1$u1') | 'Ts212'(X0,'s$u$u374dafrika$u0'), inference(resolution, [status(thm)], [c580,c660])).
% 91.02/21.20 cnf(d5, plain, 'Ts212'(c676,'s$u$u374dafrika$u0'), inference(resolution, [status(thm)], [d4,c9])).
% 91.02/21.20 cnf(d6, plain, ~attr(X0,X1) | ~attr(X2,X3) | ~attr(X2,X4) | ~sub(sK245(X5,X6,X7),X8) | ~sub(X3,'familiename$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X4,'eigenname$u1$u1') | ~val(X3,'mandela$u0') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X4,'nelson$u0') | ~obj(X9,X2) | ~in(X10,X0) | ~arg1(sK244(X5,X6,X7),X2) | ~subr(sK244(X5,X6,X7),'rprs$u0') | ~'Ts239'(X5,X6,X7), inference(resolution, [status(thm)], [c673,c602])).
% 91.02/21.20 cnf(d7, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X3,X4) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X4,'name$u1$u1') | ~sub(sK245(X5,X6,X7),X8) | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~val(X4,'s$u$u374dafrika$u0') | ~obj(X9,X0) | ~in(X10,X3) | ~arg1(sK244(X5,X6,X7),X0) | ~'Ts239'(X5,X6,X7) | ~'Ts239'(X5,X6,X7), inference(resolution, [status(thm)], [d6,c607])).
% 91.02/21.20 cnf(d8, plain, ~attr(X0,X1) | ~attr(X2,X3) | ~attr(X2,X4) | ~sub(X1,'name$u1$u1') | ~sub(X3,'familiename$u1$u1') | ~sub(X4,'eigenname$u1$u1') | ~sub(sK245(X5,X2,X6),X7) | ~val(X1,'s$u$u374dafrika$u0') | ~val(X3,'mandela$u0') | ~val(X4,'nelson$u0') | ~obj(X8,X2) | ~in(X9,X0) | ~'Ts239'(X5,X2,X6) | ~'Ts239'(X5,X2,X6), inference(resolution, [status(thm)], [d7,c601])).
% 91.02/21.20 cnf(d9, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X3,X4) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X4,'name$u1$u1') | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~val(X4,'s$u$u374dafrika$u0') | ~obj(X5,X0) | ~in(X6,X3) | ~'Ts239'(X7,X0,X8) | ~'Ts239'(X7,X0,X8), inference(resolution, [status(thm)], [d8,c606])).
% 91.02/21.20 cnf(d10, plain, ~attr(X0,X1) | ~attr(X2,X3) | ~attr(X2,X4) | ~sub(X1,'name$u1$u1') | ~sub(X3,'familiename$u1$u1') | ~sub(X4,'eigenname$u1$u1') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X3,'mandela$u0') | ~val(X4,'nelson$u0') | ~obj(X5,X2) | ~in(X6,X0) | ~arg1(X7,X2) | ~subr(X7,'sub$u0') | ~arg2(X7,X8), inference(resolution, [status(thm)], [d9,c600])).
% 91.02/21.20 cnf(d11, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X3,X4) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X4,'name$u1$u1') | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~val(X4,'s$u$u374dafrika$u0') | ~obj(X5,X0) | ~in(X6,X3) | ~arg1(sK248(X7,X8),X0) | ~subr(sK248(X7,X8),'sub$u0') | ~sub(X7,X8), inference(resolution, [status(thm)], [d10,c610])).
% 91.02/21.20 cnf(d12, plain, ~attr(X0,X1) | ~attr(X2,X3) | ~attr(X2,X4) | ~sub(X5,X6) | ~sub(X1,'name$u1$u1') | ~sub(X3,'familiename$u1$u1') | ~sub(X4,'eigenname$u1$u1') | ~val(X1,'s$u$u374dafrika$u0') | ~val(X3,'mandela$u0') | ~val(X4,'nelson$u0') | ~obj(X7,X2) | ~in(X8,X0) | ~arg1(sK248(X5,X6),X2) | ~sub(X5,X6), inference(resolution, [status(thm)], [d11,c611])).
% 91.02/21.20 cnf(d13, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X3,X4) | ~sub(X0,X5) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X4,'name$u1$u1') | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~val(X4,'s$u$u374dafrika$u0') | ~obj(X6,X0) | ~in(X7,X3) | ~sub(X0,X5), inference(resolution, [status(thm)], [d12,c609])).
% 91.02/21.20 cnf(d14, plain, ~attr(sK216(X0,X1),X2) | ~attr(X3,X4) | ~attr(X3,X5) | ~sub(X2,'name$u1$u1') | ~sub(X4,'familiename$u1$u1') | ~sub(X5,'eigenname$u1$u1') | ~sub(X3,X6) | ~val(X2,'s$u$u374dafrika$u0') | ~val(X4,'mandela$u0') | ~val(X5,'nelson$u0') | ~obj(X7,X3) | ~'Ts212'(X0,X1), inference(resolution, [status(thm)], [d13,c581])).
% 91.02/21.20 cnf(d15, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X0,X3) | ~sub(sK217(X4,X5),'name$u1$u1') | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~val(sK217(X4,X5),'s$u$u374dafrika$u0') | ~obj(X6,X0) | ~'Ts212'(X4,X5) | ~'Ts212'(X4,X5), inference(resolution, [status(thm)], [d14,c582])).
% 91.02/21.20 cnf(d16, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~sub(X1,'familiename$u1$u1') | ~sub(X2,'eigenname$u1$u1') | ~sub(X0,X3) | ~sub(sK217(X4,'s$u$u374dafrika$u0'),'name$u1$u1') | ~val(X1,'mandela$u0') | ~val(X2,'nelson$u0') | ~obj(X5,X0) | ~'Ts212'(X4,'s$u$u374dafrika$u0') | ~'Ts212'(X4,'s$u$u374dafrika$u0'), inference(resolution, [status(thm)], [d15,c586])).
% 91.02/21.20 cnf(d17, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X0,X3) | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~obj(X4,X0) | ~'Ts212'(X5,'s$u$u374dafrika$u0') | ~'Ts212'(X5,'s$u$u374dafrika$u0'), inference(resolution, [status(thm)], [d16,c585])).
% 91.02/21.20 cnf(d18, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~sub(X1,'familiename$u1$u1') | ~sub(X2,'eigenname$u1$u1') | ~sub(X0,X3) | ~val(X1,'mandela$u0') | ~val(X2,'nelson$u0') | ~obj(X4,X0), inference(resolution, [status(thm)], [d17,d5])).
% 91.02/21.20 cnf(d19, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X0,X3) | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~'Ts233'(X4,X0,X5), inference(resolution, [status(thm)], [d18,c597])).
% 91.02/21.20 cnf(d20, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~sub(X1,'familiename$u1$u1') | ~sub(X2,'eigenname$u1$u1') | ~sub(X0,X3) | ~val(X1,'mandela$u0') | ~val(X2,'nelson$u0') | ~subs(X4,'hei$u$u337en$u1$u1') | ~arg1(X4,X0) | ~arg2(X4,X5), inference(resolution, [status(thm)], [d19,c592])).
% 91.02/21.20 cnf(d21, plain, ~attr(X0,X1) | ~sub(X1,'eigenname$u1$u1') | arg2(sK232(X0),X0), inference(resolution, [status(thm)], [c590,c419])).
% 91.02/21.20 cnf(d22, plain, ~attr(X0,c677) | arg2(sK232(X0),X0), inference(resolution, [status(thm)], [d21,c11])).
% 91.02/21.20 cnf(d23, plain, ~attr(X0,c677) | ~subs(sK232(X0),'hei$u$u337en$u1$u1') | ~attr(X1,X2) | ~attr(X1,X3) | ~sub(X2,'eigenname$u1$u1') | ~sub(X3,'familiename$u1$u1') | ~sub(X1,X4) | ~val(X2,'nelson$u0') | ~val(X3,'mandela$u0') | ~arg1(sK232(X0),X1), inference(resolution, [status(thm)], [d22,d20])).
% 91.02/21.20 cnf(d24, plain, ~subs(sK232(X0),'hei$u$u337en$u1$u1') | ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X0,c677) | ~sub(X1,'familiename$u1$u1') | ~sub(X2,'eigenname$u1$u1') | ~sub(X0,X3) | ~val(X1,'mandela$u0') | ~val(X2,'nelson$u0') | ~attr(X0,c677), inference(resolution, [status(thm)], [d23,d3])).
% 91.02/21.20 cnf(d25, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X0,c677) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X0,X3) | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~attr(X0,c677), inference(resolution, [status(thm)], [d24,d1])).
% 91.02/21.20 cnf(d26, plain, ~attr(X0,X1) | ~attr(X0,c677) | ~attr(X0,c677) | ~sub(X1,'familiename$u1$u1') | ~sub(c677,'eigenname$u1$u1') | ~sub(X0,X2) | ~val(X1,'mandela$u0'), inference(resolution, [status(thm)], [d25,c12])).
% 91.02/21.20 cnf(d27, plain, ~attr(X0,X1) | ~attr(X0,c677) | ~sub(X1,'familiename$u1$u1') | ~sub(X0,X2) | ~val(X1,'mandela$u0'), inference(resolution, [status(thm)], [c11,d26])).
% 91.02/21.20 cnf(d28, plain, ~attr(X0,c678) | ~attr(X0,c677) | ~sub(c678,'familiename$u1$u1') | ~sub(X0,X1), inference(resolution, [status(thm)], [d27,c14])).
% 91.02/21.20 cnf(d29, plain, ~attr(X0,c677) | ~attr(X0,c678) | ~sub(X0,X1), inference(resolution, [status(thm)], [c13,d28])).
% 91.02/21.20 cnf(d30, plain, ~attr(c676,c677) | ~attr(c676,c678), inference(resolution, [status(thm)], [d29,c10])).
% 91.02/21.20 cnf(d31, plain, ~attr(c676,c678), inference(resolution, [status(thm)], [c7,d30])).
% 91.02/21.20 cnf(d32, plain, $false, inference(resolution, [status(thm)], [c8,d31])).
% 91.02/21.20 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------