%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR116+47 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 106.53s 16.73s
% Output : CNFRefutation 106.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR116+47 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n009.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 27 01:16:01 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 106.53/16.73 % SZS status Theorem for theBenchmark.p
% 106.53/16.73 % SZS output start CNFRefutation for theBenchmark.p
% 106.53/16.73 fof(ave07_era5_synth_qa07_010_qapn_176_a671, hypothesis, (attr(c14,c15) & (prop(c14,'afrikanisch$u$u1$u1') & (sub(c14,'nationalkongre$u$u337$u1$u1') & (sub(c15,'name$u1$u1') & (val(c15,'anc$u0') & (attch(c22,c14) & (attr(c22,c23) & (attr(c22,c24) & (sub(c22,'mensch$u1$u1') & (sub(c23,'eigenname$u1$u1') & (val(c23,'nelson$u0') & (sub(c24,'familiename$u1$u1') & (val(c24,'mandela$u0') & (circ(c273,c946) & (mcont(c273,c969) & (obj(c273,c14) & (subs(c273,'gelten$u1$u4') & (sub(c36,'allianz$u1$u1') & (pred(c41,'kommunist$u1$u1') & (preds(c47,'wahl$u1$u1') & (agt(c48,c22) & (assoc(c48,c41) & (ctxt(c48,c36) & (purp(c48,c47) & (subs(c48,'antreten$u2$u1') & (prop(c938,'wahrscheinlich$u2$u1') & (sub(c938,'wahlgewinner$u1$u1') & (ctxt(c946,c953) & (preds(c946,c950) & (prop(c946,'allgemein$u1$u1') & (pmod(c950,'erst$u1$u1','wahl$u1$u1') & (agt(c953,c959) & (subs(c953,'beteiligung$u1$u1') & (loc(c959,c968) & (pred(c959,'mohr$u1$u1') & (attr(c965,c966) & (sub(c965,'land$u1$u1') & (sub(c966,'name$u1$u1') & (val(c966,'s$u$u374dafrika$u0') & (in(c968,c965) & (arg1(c969,c14) & (arg2(c969,c938) & (subr(c969,'rprs$u0') & (exp(c970,c938) & (subs(c970,'gewinnen$u1$u1') & (assoc('nationalkongre$u$u337$u1$u1','national$u$u1$u1') & (sub('nationalkongre$u$u337$u1$u1','einrichtung$u1$u2') & (sub('nationalkongre$u$u337$u1$u1','kongre$u$u337$u1$u1') & (assoc('wahlgewinner$u1$u1','auswahl$u1$u1') & (sub('wahlgewinner$u1$u1','gewinner$u$u1$u1') & (sort(c14,d) & (sort(c14,io) & (card(c14,int1) & (etype(c14,int0) & (fact(c14,real) & (gener(c14,sp) & (quant(c14,one) & (refer(c14,det) & (varia(c14,con) & (sort(c15,na) & (card(c15,int1) & (etype(c15,int0) & (fact(c15,real) & (gener(c15,sp) & (quant(c15,one) & (refer(c15,indet) & (varia(c15,'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(c22,d) & (card(c22,int1) & (etype(c22,int0) & (fact(c22,real) & (gener(c22,sp) & (quant(c22,one) & (refer(c22,det) & (varia(c22,con) & (sort(c23,na) & (card(c23,int1) & (etype(c23,int0) & (fact(c23,real) & (gener(c23,sp) & (quant(c23,one) & (refer(c23,indet) & (varia(c23,'varia$uc') & (sort(c24,na) & (card(c24,int1) & (etype(c24,int0) & (fact(c24,real) & (gener(c24,sp) & (quant(c24,one) & (refer(c24,indet) & (varia(c24,'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('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(c273,st) & (fact(c273,real) & (gener(c273,sp) & (sort(c946,ad) & (card(c946,cons('x$uconstant',cons(int1,nil))) & (etype(c946,int1) & (fact(c946,real) & (gener(c946,sp) & (quant(c946,mult) & (refer(c946,det) & (varia(c946,con) & (sort(c969,st) & (fact(c969,hypo) & (gener(c969,sp) & (sort('gelten$u1$u4',st) & (fact('gelten$u1$u4',real) & (gener('gelten$u1$u4',ge) & (sort(c36,io) & (card(c36,int1) & (etype(c36,int0) & (fact(c36,real) & (gener(c36,'gener$uc') & (quant(c36,one) & (refer(c36,'refer$uc') & (varia(c36,'varia$uc') & (sort('allianz$u1$u1',io) & (card('allianz$u1$u1',int1) & (etype('allianz$u1$u1',int0) & (fact('allianz$u1$u1',real) & (gener('allianz$u1$u1',ge) & (quant('allianz$u1$u1',one) & (refer('allianz$u1$u1','refer$uc') & (varia('allianz$u1$u1','varia$uc') & (sort(c41,d) & (card(c41,cons('x$uconstant',cons(int1,nil))) & (etype(c41,int1) & (fact(c41,real) & (gener(c41,sp) & (quant(c41,mult) & (refer(c41,det) & (varia(c41,con) & (sort('kommunist$u1$u1',d) & (card('kommunist$u1$u1',int1) & (etype('kommunist$u1$u1',int0) & (fact('kommunist$u1$u1',real) & (gener('kommunist$u1$u1',ge) & (quant('kommunist$u1$u1',one) & (refer('kommunist$u1$u1','refer$uc') & (varia('kommunist$u1$u1','varia$uc') & (sort(c47,ad) & (card(c47,cons('x$uconstant',cons(int1,nil))) & (etype(c47,int1) & (fact(c47,real) & (gener(c47,sp) & (quant(c47,mult) & (refer(c47,det) & (varia(c47,con) & (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(c48,da) & (fact(c48,real) & (gener(c48,sp) & (sort('antreten$u2$u1',da) & (fact('antreten$u2$u1',real) & (gener('antreten$u2$u1',ge) & (sort(c938,d) & (sort(c938,io) & (card(c938,int1) & (etype(c938,int0) & (fact(c938,real) & (gener(c938,sp) & (quant(c938,one) & (refer(c938,det) & (varia(c938,con) & (sort('wahrscheinlich$u2$u1',nq) & (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(c953,ad) & (card(c953,int1) & (etype(c953,int0) & (fact(c953,real) & (gener(c953,sp) & (quant(c953,one) & (refer(c953,det) & (varia(c953,'varia$uc') & (sort(c950,ad) & (card(c950,int1) & (etype(c950,int0) & (fact(c950,real) & (gener(c950,ge) & (quant(c950,one) & (refer(c950,'refer$uc') & (varia(c950,'varia$uc') & (sort('allgemein$u1$u1',nq) & (sort('erst$u1$u1',oq) & (card('erst$u1$u1',int1) & (sort(c959,d) & (card(c959,cons('x$uconstant',cons(int1,nil))) & (etype(c959,int1) & (fact(c959,real) & (gener(c959,sp) & (quant(c959,mult) & (refer(c959,det) & (varia(c959,con) & (sort('beteiligung$u1$u1',ad) & (card('beteiligung$u1$u1',int1) & (etype('beteiligung$u1$u1',int0) & (fact('beteiligung$u1$u1',real) & (gener('beteiligung$u1$u1',ge) & (quant('beteiligung$u1$u1',one) & (refer('beteiligung$u1$u1','refer$uc') & (varia('beteiligung$u1$u1','varia$uc') & (sort(c968,l) & (card(c968,int1) & (etype(c968,int0) & (fact(c968,real) & (gener(c968,sp) & (quant(c968,one) & (refer(c968,det) & (varia(c968,con) & (sort('mohr$u1$u1',d) & (card('mohr$u1$u1',int1) & (etype('mohr$u1$u1',int0) & (fact('mohr$u1$u1',real) & (gener('mohr$u1$u1',ge) & (quant('mohr$u1$u1',one) & (refer('mohr$u1$u1','refer$uc') & (varia('mohr$u1$u1','varia$uc') & (sort(c965,d) & (sort(c965,io) & (card(c965,int1) & (etype(c965,int0) & (fact(c965,real) & (gener(c965,sp) & (quant(c965,one) & (refer(c965,det) & (varia(c965,con) & (sort(c966,na) & (card(c966,int1) & (etype(c966,int0) & (fact(c966,real) & (gener(c966,sp) & (quant(c966,one) & (refer(c966,indet) & (varia(c966,'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('rprs$u0',st) & (fact('rprs$u0',real) & (gener('rprs$u0','gener$uc') & (sort(c970,dn) & (fact(c970,real) & (gener(c970,sp) & (sort('gewinnen$u1$u1',dn) & (fact('gewinnen$u1$u1',real) & (gener('gewinnen$u1$u1',ge) & (sort('national$u$u1$u1',nq) & (sort('einrichtung$u1$u2',ent) & (card('einrichtung$u1$u2','card$uc') & (etype('einrichtung$u1$u2','etype$uc') & (fact('einrichtung$u1$u2',real) & (gener('einrichtung$u1$u2','gener$uc') & (quant('einrichtung$u1$u2','quant$uc') & (refer('einrichtung$u1$u2','refer$uc') & (varia('einrichtung$u1$u2','varia$uc') & (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('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('gewinner$u$u1$u1',d) & (sort('gewinner$u$u1$u1',io) & (card('gewinner$u$u1$u1',int1) & (etype('gewinner$u$u1$u1',int0) & (fact('gewinner$u$u1$u1',real) & (gener('gewinner$u$u1$u1',ge) & (quant('gewinner$u$u1$u1',one) & (refer('gewinner$u$u1$u1','refer$uc') & varia('gewinner$u$u1$u1','varia$uc'))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 106.53/16.73 fof(member_first, axiom, ! [X0] : ! [X1] : member(X0,cons(X0,X1))).
% 106.53/16.73 fof(member_second, axiom, ! [X0] : ! [X1] : ! [X2] : ((member(X0,X2) => member(X0,cons(X1,X2))))).
% 106.53/16.73 fof(in_state__state_adjective, axiom, ! [X0] : ! [X1] : ! [X2] : ! [X3] : ! [X4] : ! [X5] : (((in(X5,X2) & (attr(X2,X3) & (loc(X0,X5) & ('state$uadjective$ustate$ubinding'(X1,X4) & (sub(X2,'land$u1$u1') & (sub(X3,'name$u1$u1') & val(X3,X4))))))) => prop(X0,X1)))).
% 106.53/16.73 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)))))))))).
% 106.53/16.73 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'))))))).
% 106.53/16.73 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'))))))))))).
% 106.53/16.73 fof(fact_8980, axiom, 'state$uadjective$ustate$ubinding'('s$u$u374dafrikanisch$u1$u1','s$u$u374dafrika$u0')).
% 106.53/16.73 fof(synth_qa07_010_qapn_176_a671, 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'))))))))))))))))).
% 106.53/16.73 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_qapn_176_a671])).
% 106.53/16.73 cnf(c6, plain, attr(c22,c23), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c7, plain, attr(c22,c24), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c8, plain, sub(c22,'mensch$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c9, plain, sub(c23,'eigenname$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c10, plain, val(c23,'nelson$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c11, plain, sub(c24,'familiename$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c12, plain, val(c24,'mandela$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c33, plain, loc(c959,c968), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c35, plain, attr(c965,c966), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c36, plain, sub(c965,'land$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c37, plain, sub(c966,'name$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c38, plain, val(c966,'s$u$u374dafrika$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c39, plain, in(c968,c965), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_010_qapn_176_a671])).
% 106.53/16.73 cnf(c348, plain, member(X0,cons(X0,X1)), inference(clausification, [status(esa)], [member_first])).
% 106.53/16.73 cnf(c349, plain, ~member(X0,X1) | member(X0,cons(X2,X1)), inference(clausification, [status(esa)], [member_second])).
% 106.53/16.73 cnf(c465, plain, prop(X0,X1) | ~'state$uadjective$ustate$ubinding'(X1,X2) | ~in(X3,X4) | ~sub(X5,'name$u1$u1') | ~sub(X4,'land$u1$u1') | ~loc(X0,X3) | ~val(X5,X2) | ~attr(X4,X5), inference(clausification, [status(esa)], [in_state__state_adjective])).
% 106.53/16.73 cnf(c466, plain, ~prop(X0,X1) | ~'state$uadjective$ustate$ubinding'(X1,X2) | X3(X0,X2), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 106.53/16.73 cnf(c467, plain, ~X0(X1,X2) | in(sK175(X1,X2),sK173(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 106.53/16.73 cnf(c468, plain, ~X0(X1,X2) | attr(sK173(X1,X2),sK174(X1,X2)), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 106.53/16.73 cnf(c471, plain, ~X0(X1,X2) | sub(sK174(X1,X2),'name$u1$u1'), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 106.53/16.73 cnf(c472, plain, ~X0(X1,X2) | val(sK174(X1,X2),X2), inference(clausification, [status(esa)], [state_adjective__in_state])).
% 106.53/16.73 cnf(c473, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | arg1(sK179(X0),X0), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 106.53/16.73 cnf(c474, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | arg2(sK179(X0),X0), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 106.53/16.73 cnf(c475, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | subs(sK179(X0),'hei$u$u337en$u1$u1'), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 106.53/16.73 cnf(c476, 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])).
% 106.53/16.73 cnf(c477, plain, ~X0(X1,X2,X3) | arg1(sK185(X1,X2,X3),X2), inference(clausification, [status(esa)], [hei__337en_1_1__bezeichnen_1_1_als])).
% 106.53/16.73 cnf(c478, plain, ~X0(X1,X2,X3) | arg2(sK185(X1,X2,X3),X3), inference(clausification, [status(esa)], [hei__337en_1_1__bezeichnen_1_1_als])).
% 106.53/16.73 cnf(c481, plain, ~X0(X1,X2,X3) | obj(sK184(X1,X2,X3),X2), inference(clausification, [status(esa)], [hei__337en_1_1__bezeichnen_1_1_als])).
% 106.53/16.73 cnf(c482, plain, ~X0(X1,X2,X3) | subr(sK185(X1,X2,X3),'rprs$u0'), inference(clausification, [status(esa)], [hei__337en_1_1__bezeichnen_1_1_als])).
% 106.53/16.73 cnf(c509, plain, 'state$uadjective$ustate$ubinding'('s$u$u374dafrikanisch$u1$u1','s$u$u374dafrika$u0'), inference(clausification, [status(esa)], [fact_8980])).
% 106.53/16.73 cnf(c514, plain, ~arg2(X0,X1) | ~subr(X0,'rprs$u0') | ~obj(X2,X3) | ~val(X4,'nelson$u0') | ~sub(X1,X5) | ~attr(X3,X6) | ~val(X7,'s$u$u374dafrika$u0') | ~in(X8,X9) | ~arg1(X0,X3) | ~attr(X3,X4) | ~sub(X7,'name$u1$u1') | ~attr(X9,X7) | ~sub(X6,'familiename$u1$u1') | ~sub(X4,'eigenname$u1$u1') | ~val(X6,'mandela$u0'), inference(clausification, [status(esa)], [negated_conjecture])).
% 106.53/16.73 cnf(d0, plain, ~attr(X0,X1) | ~sub(X1,X2) | arg1(sK179(X0),X0) | ~member(X2,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c473,c349])).
% 106.53/16.73 cnf(d1, plain, ~attr(X0,X1) | ~sub(X1,'familiename$u1$u1') | arg1(sK179(X0),X0), inference(resolution, [status(thm)], [d0,c348])).
% 106.53/16.73 cnf(d2, plain, ~attr(X0,c24) | arg1(sK179(X0),X0), inference(resolution, [status(thm)], [d1,c11])).
% 106.53/16.73 cnf(d3, plain, ~attr(X0,X1) | ~sub(X1,X2) | arg2(sK179(X0),X0) | ~member(X2,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c474,c349])).
% 106.53/16.73 cnf(d4, plain, ~attr(X0,X1) | ~sub(X1,'familiename$u1$u1') | arg2(sK179(X0),X0), inference(resolution, [status(thm)], [d3,c348])).
% 106.53/16.73 cnf(d5, plain, ~attr(X0,c24) | arg2(sK179(X0),X0), inference(resolution, [status(thm)], [d4,c11])).
% 106.53/16.73 cnf(d6, plain, ~prop(X0,'s$u$u374dafrikanisch$u1$u1') | 'Ts169'(X0,'s$u$u374dafrika$u0'), inference(resolution, [status(thm)], [c466,c509])).
% 106.53/16.73 cnf(d7, plain, ~attr(X0,X1) | prop(X2,'s$u$u374dafrikanisch$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X0,'land$u1$u1') | ~val(X1,'s$u$u374dafrika$u0') | ~loc(X2,X3) | ~in(X3,X0), inference(resolution, [status(thm)], [c465,c509])).
% 106.53/16.73 cnf(d8, plain, ~attr(c965,X0) | prop(X1,'s$u$u374dafrikanisch$u1$u1') | ~sub(X0,'name$u1$u1') | ~sub(c965,'land$u1$u1') | ~val(X0,'s$u$u374dafrika$u0') | ~loc(X1,c968), inference(resolution, [status(thm)], [d7,c39])).
% 106.53/16.73 cnf(d9, plain, ~attr(c965,X0) | prop(X1,'s$u$u374dafrikanisch$u1$u1') | ~sub(X0,'name$u1$u1') | ~val(X0,'s$u$u374dafrika$u0') | ~loc(X1,c968), inference(resolution, [status(thm)], [c36,d8])).
% 106.53/16.73 cnf(d10, plain, ~attr(c965,X0) | prop(c959,'s$u$u374dafrikanisch$u1$u1') | ~sub(X0,'name$u1$u1') | ~val(X0,'s$u$u374dafrika$u0'), inference(resolution, [status(thm)], [d9,c33])).
% 106.53/16.73 cnf(d11, plain, ~attr(c965,c966) | prop(c959,'s$u$u374dafrikanisch$u1$u1') | ~sub(c966,'name$u1$u1'), inference(resolution, [status(thm)], [d10,c38])).
% 106.53/16.73 cnf(d12, plain, prop(c959,'s$u$u374dafrikanisch$u1$u1') | ~sub(c966,'name$u1$u1'), inference(resolution, [status(thm)], [c35,d11])).
% 106.53/16.73 cnf(d13, plain, prop(c959,'s$u$u374dafrikanisch$u1$u1'), inference(resolution, [status(thm)], [c37,d12])).
% 106.53/16.73 cnf(d14, plain, 'Ts169'(c959,'s$u$u374dafrika$u0'), inference(resolution, [status(thm)], [d13,d6])).
% 106.53/16.73 cnf(d15, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X3,X4) | ~sub(X1,'eigenname$u1$u1') | ~sub(X5,X6) | ~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(X7,X0) | ~in(X8,X3) | ~arg1(sK185(X9,X10,X11),X0) | ~arg2(sK185(X9,X10,X11),X5) | ~'Ts180'(X9,X10,X11), inference(resolution, [status(thm)], [c514,c482])).
% 106.53/16.73 cnf(d16, 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(sK185(X9,X10,X5),X2) | ~'Ts180'(X9,X10,X5) | ~'Ts180'(X9,X10,X5), inference(resolution, [status(thm)], [d15,c478])).
% 106.53/16.73 cnf(d17, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X3,X4) | ~sub(X5,X6) | ~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(X7,X0) | ~in(X8,X3) | ~'Ts180'(X9,X0,X5) | ~'Ts180'(X9,X0,X5), inference(resolution, [status(thm)], [d16,c477])).
% 106.53/16.73 cnf(d18, 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) | ~subs(X9,'hei$u$u337en$u1$u1') | ~arg1(X9,X2) | ~arg2(X9,X5), inference(resolution, [status(thm)], [d17,c476])).
% 106.53/16.73 cnf(d19, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X3,X4) | ~sub(X5,X6) | ~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(X7,X0) | ~subs(sK179(X5),'hei$u$u337en$u1$u1') | ~in(X8,X3) | ~arg1(sK179(X5),X0) | ~attr(X5,c24), inference(resolution, [status(thm)], [d18,d5])).
% 106.53/16.73 cnf(d20, plain, ~attr(X0,X1) | ~sub(X1,X2) | subs(sK179(X0),'hei$u$u337en$u1$u1') | ~member(X2,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c475,c349])).
% 106.53/16.73 cnf(d21, plain, ~attr(X0,X1) | ~sub(X1,'familiename$u1$u1') | subs(sK179(X0),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [d20,c348])).
% 106.53/16.73 cnf(d22, plain, ~attr(X0,c24) | subs(sK179(X0),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [d21,c11])).
% 106.53/16.73 cnf(d23, plain, ~attr(X0,c24) | ~attr(X0,c24) | ~attr(X1,X2) | ~attr(X3,X4) | ~attr(X3,X5) | ~sub(X0,X6) | ~sub(X2,'name$u1$u1') | ~sub(X4,'familiename$u1$u1') | ~sub(X5,'eigenname$u1$u1') | ~val(X2,'s$u$u374dafrika$u0') | ~val(X4,'mandela$u0') | ~val(X5,'nelson$u0') | ~obj(X7,X3) | ~in(X8,X1) | ~arg1(sK179(X0),X3), inference(resolution, [status(thm)], [d22,d19])).
% 106.53/16.73 cnf(d24, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X3,X4) | ~attr(X0,c24) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X4,'name$u1$u1') | ~sub(X0,X5) | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~val(X4,'s$u$u374dafrika$u0') | ~obj(X6,X0) | ~in(X7,X3) | ~attr(X0,c24), inference(resolution, [status(thm)], [d23,d2])).
% 106.53/16.73 cnf(d25, plain, ~attr(sK173(X0,X1),X2) | ~attr(X3,X4) | ~attr(X3,X5) | ~attr(X3,c24) | ~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) | ~'Ts169'(X0,X1), inference(resolution, [status(thm)], [d24,c467])).
% 106.53/16.73 cnf(d26, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X0,c24) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X0,X3) | ~sub(sK174(X4,X5),'name$u1$u1') | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~val(sK174(X4,X5),'s$u$u374dafrika$u0') | ~obj(X6,X0) | ~'Ts169'(X4,X5) | ~'Ts169'(X4,X5), inference(resolution, [status(thm)], [d25,c468])).
% 106.53/16.73 cnf(d27, plain, ~'Ts169'(X0,X1) | ~attr(X2,X3) | ~attr(X2,X4) | ~attr(X2,c24) | ~sub(X3,'familiename$u1$u1') | ~sub(X4,'eigenname$u1$u1') | ~sub(X2,X5) | ~val(X3,'mandela$u0') | ~val(X4,'nelson$u0') | ~val(sK174(X0,X1),'s$u$u374dafrika$u0') | ~obj(X6,X2) | ~'Ts169'(X0,X1), inference(resolution, [status(thm)], [c471,d26])).
% 106.53/16.73 cnf(d28, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X0,c24) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X0,X3) | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~obj(X4,X0) | ~'Ts169'(X5,'s$u$u374dafrika$u0') | ~'Ts169'(X5,'s$u$u374dafrika$u0'), inference(resolution, [status(thm)], [d27,c472])).
% 106.53/16.73 cnf(d29, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X0,c24) | ~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)], [d28,d14])).
% 106.53/16.73 cnf(d30, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X0,c24) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X0,X3) | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~'Ts180'(X4,X0,X5), inference(resolution, [status(thm)], [d29,c481])).
% 106.53/16.73 cnf(d31, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X0,c24) | ~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)], [d30,c476])).
% 106.53/16.73 cnf(d32, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X0,c24) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X0,X3) | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~subs(sK179(X4),'hei$u$u337en$u1$u1') | ~arg1(sK179(X4),X0) | ~attr(X4,c24), inference(resolution, [status(thm)], [d31,d5])).
% 106.53/16.73 cnf(d33, plain, ~attr(X0,c24) | ~attr(X0,c24) | ~attr(X1,X2) | ~attr(X1,X3) | ~attr(X1,c24) | ~sub(X2,'familiename$u1$u1') | ~sub(X3,'eigenname$u1$u1') | ~sub(X1,X4) | ~val(X2,'mandela$u0') | ~val(X3,'nelson$u0') | ~arg1(sK179(X0),X1), inference(resolution, [status(thm)], [d22,d32])).
% 106.53/16.73 cnf(d34, plain, ~attr(X0,X1) | ~attr(X0,X2) | ~attr(X0,c24) | ~attr(X0,c24) | ~sub(X1,'eigenname$u1$u1') | ~sub(X2,'familiename$u1$u1') | ~sub(X0,X3) | ~val(X1,'nelson$u0') | ~val(X2,'mandela$u0') | ~attr(X0,c24), inference(resolution, [status(thm)], [d33,d2])).
% 106.53/16.73 cnf(d35, plain, ~attr(X0,X1) | ~attr(X0,c23) | ~attr(X0,c24) | ~sub(X1,'familiename$u1$u1') | ~sub(c23,'eigenname$u1$u1') | ~sub(X0,X2) | ~val(X1,'mandela$u0'), inference(resolution, [status(thm)], [d34,c10])).
% 106.53/16.73 cnf(d36, plain, ~attr(X0,X1) | ~attr(X0,c23) | ~attr(X0,c24) | ~sub(X1,'familiename$u1$u1') | ~sub(X0,X2) | ~val(X1,'mandela$u0'), inference(resolution, [status(thm)], [c9,d35])).
% 106.53/16.73 cnf(d37, plain, ~attr(X0,c24) | ~attr(X0,c23) | ~attr(X0,c24) | ~sub(c24,'familiename$u1$u1') | ~sub(X0,X1), inference(resolution, [status(thm)], [d36,c12])).
% 106.53/16.73 cnf(d38, plain, ~attr(X0,c23) | ~attr(X0,c24) | ~sub(X0,X1), inference(resolution, [status(thm)], [c11,d37])).
% 106.53/16.73 cnf(d39, plain, ~attr(c22,c23) | ~attr(c22,c24), inference(resolution, [status(thm)], [d38,c8])).
% 106.53/16.73 cnf(d40, plain, ~attr(c22,c24), inference(resolution, [status(thm)], [c6,d39])).
% 106.53/16.73 cnf(d41, plain, $false, inference(resolution, [status(thm)], [c7,d40])).
% 106.53/16.73 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------