%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : CSR115+85 : 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 : n002.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:49 AM UTC 2026
% Result : Theorem 67.68s 11.65s
% Output : CNFRefutation 67.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR115+85 : 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.12/0.38 % Computer : n002.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 01:15:22 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 67.68/11.65 % SZS status Theorem for theBenchmark.p
% 67.68/11.65 % SZS output start CNFRefutation for theBenchmark.p
% 67.68/11.65 fof(ave07_era5_synth_qa07_007_mira_wp_504, hypothesis, (sub(c2174,'lizenz$u$u1$u1') & (attr(c2181,c2182) & (sub(c2181,'mensch$u1$u1') & (sub(c2182,'familiename$u1$u1') & (val(c2182,'frazer$u0') & (attr(c2186,c2187) & (sub(c2186,'mensch$u1$u1') & (sub(c2187,'familiename$u1$u1') & (val(c2187,'nash$u0') & (sub(c2196,'firma$u1$u1') & (attr(c2204,c2205) & (sub(c2205,'jahr$u$u1$u1') & (val(c2205,c2201) & (attr(c2212,c2213) & (sub(c2212,'firma$u1$u1') & (sub(c2213,'name$u1$u1') & (val(c2213,'bmw$u0') & (pred(c2214,'motor$u$u1$u1') & ('tupl$up12'(c2326,c948,c954,c2169,c954,c2174,c2181,c2186,c2196,c2204,c2212,c2214) & (sub(c948,'brite$u1$u1') & (sub(c954,'wagen$u1$u1') & (sort(c2174,d) & (sort(c2174,io) & (card(c2174,int1) & (etype(c2174,int0) & (fact(c2174,real) & (gener(c2174,'gener$uc') & (quant(c2174,one) & (refer(c2174,'refer$uc') & (varia(c2174,'varia$uc') & (sort('lizenz$u$u1$u1',d) & (sort('lizenz$u$u1$u1',io) & (card('lizenz$u$u1$u1',int1) & (etype('lizenz$u$u1$u1',int0) & (fact('lizenz$u$u1$u1',real) & (gener('lizenz$u$u1$u1',ge) & (quant('lizenz$u$u1$u1',one) & (refer('lizenz$u$u1$u1','refer$uc') & (varia('lizenz$u$u1$u1','varia$uc') & (sort(c2181,d) & (card(c2181,int1) & (etype(c2181,int0) & (fact(c2181,real) & (gener(c2181,sp) & (quant(c2181,one) & (refer(c2181,det) & (varia(c2181,con) & (sort(c2182,na) & (card(c2182,int1) & (etype(c2182,int0) & (fact(c2182,real) & (gener(c2182,sp) & (quant(c2182,one) & (refer(c2182,indet) & (varia(c2182,'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('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('frazer$u0',fe) & (sort(c2186,d) & (card(c2186,int1) & (etype(c2186,int0) & (fact(c2186,real) & (gener(c2186,sp) & (quant(c2186,one) & (refer(c2186,det) & (varia(c2186,con) & (sort(c2187,na) & (card(c2187,int1) & (etype(c2187,int0) & (fact(c2187,real) & (gener(c2187,sp) & (quant(c2187,one) & (refer(c2187,indet) & (varia(c2187,'varia$uc') & (sort('nash$u0',fe) & (sort(c2196,d) & (sort(c2196,io) & (card(c2196,int1) & (etype(c2196,int0) & (fact(c2196,real) & (gener(c2196,sp) & (quant(c2196,one) & (refer(c2196,det) & (varia(c2196,'varia$uc') & (sort('firma$u1$u1',d) & (sort('firma$u1$u1',io) & (card('firma$u1$u1',int1) & (etype('firma$u1$u1',int0) & (fact('firma$u1$u1',real) & (gener('firma$u1$u1',ge) & (quant('firma$u1$u1',one) & (refer('firma$u1$u1','refer$uc') & (varia('firma$u1$u1','varia$uc') & (sort(c2204,t) & (card(c2204,int1) & (etype(c2204,int0) & (fact(c2204,real) & (gener(c2204,sp) & (quant(c2204,one) & (refer(c2204,det) & (varia(c2204,con) & (sort(c2205,me) & (sort(c2205,oa) & (sort(c2205,ta) & (card(c2205,'card$uc') & (etype(c2205,'etype$uc') & (fact(c2205,real) & (gener(c2205,sp) & (quant(c2205,'quant$uc') & (refer(c2205,'refer$uc') & (varia(c2205,'varia$uc') & (sort('jahr$u$u1$u1',me) & (sort('jahr$u$u1$u1',oa) & (sort('jahr$u$u1$u1',ta) & (card('jahr$u$u1$u1','card$uc') & (etype('jahr$u$u1$u1','etype$uc') & (fact('jahr$u$u1$u1',real) & (gener('jahr$u$u1$u1',ge) & (quant('jahr$u$u1$u1','quant$uc') & (refer('jahr$u$u1$u1','refer$uc') & (varia('jahr$u$u1$u1','varia$uc') & (sort(c2201,nu) & (card(c2201,int1934) & (sort(c2212,d) & (sort(c2212,io) & (card(c2212,int1) & (etype(c2212,int0) & (fact(c2212,real) & (gener(c2212,sp) & (quant(c2212,one) & (refer(c2212,det) & (varia(c2212,con) & (sort(c2213,na) & (card(c2213,int1) & (etype(c2213,int0) & (fact(c2213,real) & (gener(c2213,sp) & (quant(c2213,one) & (refer(c2213,indet) & (varia(c2213,'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('bmw$u0',fe) & (sort(c2214,d) & (card(c2214,cons('x$uconstant',cons(int1,nil))) & (etype(c2214,int1) & (fact(c2214,real) & (gener(c2214,'gener$uc') & (quant(c2214,mult) & (refer(c2214,indet) & (varia(c2214,'varia$uc') & (sort('motor$u$u1$u1',d) & (card('motor$u$u1$u1',int1) & (etype('motor$u$u1$u1',int0) & (fact('motor$u$u1$u1',real) & (gener('motor$u$u1$u1',ge) & (quant('motor$u$u1$u1',one) & (refer('motor$u$u1$u1','refer$uc') & (varia('motor$u$u1$u1','varia$uc') & (sort(c2326,ent) & (card(c2326,'card$uc') & (etype(c2326,'etype$uc') & (fact(c2326,real) & (gener(c2326,'gener$uc') & (quant(c2326,'quant$uc') & (refer(c2326,'refer$uc') & (varia(c2326,'varia$uc') & (sort(c948,d) & (card(c948,int1) & (etype(c948,int0) & (fact(c948,real) & (gener(c948,sp) & (quant(c948,one) & (refer(c948,det) & (varia(c948,con) & (sort(c954,o) & (card(c954,int1) & (etype(c954,int0) & (fact(c954,real) & (gener(c954,sp) & (quant(c954,one) & (refer(c954,det) & (varia(c954,'varia$uc') & (sort(c2169,o) & (card(c2169,int1) & (etype(c2169,int0) & (fact(c2169,real) & (gener(c2169,sp) & (quant(c2169,one) & (refer(c2169,det) & (varia(c2169,'varia$uc') & (sort('brite$u1$u1',d) & (card('brite$u1$u1',int1) & (etype('brite$u1$u1',int0) & (fact('brite$u1$u1',real) & (gener('brite$u1$u1',ge) & (quant('brite$u1$u1',one) & (refer('brite$u1$u1','refer$uc') & (varia('brite$u1$u1','varia$uc') & (sort('wagen$u1$u1',d) & (card('wagen$u1$u1',int1) & (etype('wagen$u1$u1',int0) & (fact('wagen$u1$u1',real) & (gener('wagen$u1$u1',ge) & (quant('wagen$u1$u1',one) & (refer('wagen$u1$u1','refer$uc') & varia('wagen$u1$u1','varia$uc')))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
% 67.68/11.65 fof(member_first, axiom, ! [X0] : ! [X1] : member(X0,cons(X0,X1))).
% 67.68/11.65 fof(member_second, axiom, ! [X0] : ! [X1] : ! [X2] : ((member(X0,X2) => member(X0,cons(X1,X2))))).
% 67.68/11.65 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'))))))).
% 67.68/11.65 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'))))))))))).
% 67.68/11.65 fof(synth_qa07_007_mira_wp_504, conjecture, ? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ((attr(X0,X1) & (attr(X3,X2) & (attr(X5,X6) & (obj(X4,X0) & (sub(X1,'name$u1$u1') & (sub(X0,'firma$u1$u1') & (sub(X2,'name$u1$u1') & (sub(X6,'jahr$u$u1$u1') & (val(X1,'bmw$u0') & val(X2,'bmw$u0')))))))))))).
% 67.68/11.65 fof(negated_conjecture, negated_conjecture, ~? [X0] : ? [X1] : ? [X2] : ? [X3] : ? [X4] : ? [X5] : ? [X6] : ((attr(X0,X1) & (attr(X3,X2) & (attr(X5,X6) & (obj(X4,X0) & (sub(X1,'name$u1$u1') & (sub(X0,'firma$u1$u1') & (sub(X2,'name$u1$u1') & (sub(X6,'jahr$u$u1$u1') & (val(X1,'bmw$u0') & val(X2,'bmw$u0'))))))))))), inference(negate_conjecture, [status(cth)], [synth_qa07_007_mira_wp_504])).
% 67.68/11.65 cnf(c10, plain, attr(c2204,c2205), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_504])).
% 67.68/11.65 cnf(c11, plain, sub(c2205,'jahr$u$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_504])).
% 67.68/11.65 cnf(c13, plain, attr(c2212,c2213), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_504])).
% 67.68/11.65 cnf(c14, plain, sub(c2212,'firma$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_504])).
% 67.68/11.65 cnf(c15, plain, sub(c2213,'name$u1$u1'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_504])).
% 67.68/11.65 cnf(c16, plain, val(c2213,'bmw$u0'), inference(clausification, [status(esa)], [ave07_era5_synth_qa07_007_mira_wp_504])).
% 67.68/11.65 cnf(c227, plain, member(X0,cons(X0,X1)), inference(clausification, [status(esa)], [member_first])).
% 67.68/11.65 cnf(c228, plain, ~member(X0,X1) | member(X0,cons(X2,X1)), inference(clausification, [status(esa)], [member_second])).
% 67.68/11.65 cnf(c380, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | arg1(sK227(X0),X0), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 67.68/11.65 cnf(c381, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | arg2(sK227(X0),X0), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 67.68/11.65 cnf(c382, plain, ~attr(X0,X1) | ~member(X2,cons('eigenname$u1$u1',cons('familiename$u1$u1',cons('name$u1$u1',nil)))) | ~sub(X1,X2) | subs(sK227(X0),'hei$u$u337en$u1$u1'), inference(clausification, [status(esa)], [attr_name_hei__337en_1_1])).
% 67.68/11.65 cnf(c387, 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])).
% 67.68/11.65 cnf(c392, plain, ~X0(X1,X2,X3) | obj(sK236(X1,X2,X3),X2), inference(clausification, [status(esa)], [hei__337en_1_1__bezeichnen_1_1_als])).
% 67.68/11.65 cnf(c448, plain, ~sub(X0,'name$u1$u1') | ~val(X1,'bmw$u0') | ~attr(X2,X0) | ~sub(X1,'name$u1$u1') | ~sub(X3,'jahr$u$u1$u1') | ~attr(X4,X1) | ~attr(X5,X3) | ~obj(X6,X4) | ~sub(X4,'firma$u1$u1') | ~val(X0,'bmw$u0'), inference(clausification, [status(esa)], [negated_conjecture])).
% 67.68/11.65 cnf(d0, plain, ~sub(X0,X1) | ~attr(X2,X0) | arg1(sK227(X2),X2) | ~member(X1,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c380,c228])).
% 67.68/11.65 cnf(d1, plain, ~sub(X0,X1) | ~attr(X2,X0) | arg1(sK227(X2),X2) | ~member(X1,cons('name$u1$u1',nil)), inference(resolution, [status(thm)], [d0,c228])).
% 67.68/11.65 cnf(d2, plain, ~sub(X0,'name$u1$u1') | ~attr(X1,X0) | arg1(sK227(X1),X1), inference(resolution, [status(thm)], [d1,c227])).
% 67.68/11.65 cnf(d3, plain, ~sub(c2213,'name$u1$u1') | arg1(sK227(c2212),c2212), inference(resolution, [status(thm)], [d2,c13])).
% 67.68/11.65 cnf(d4, plain, arg1(sK227(c2212),c2212), inference(resolution, [status(thm)], [c15,d3])).
% 67.68/11.65 cnf(d5, plain, ~'Ts232'(X0,X1,X2) | ~sub(X3,'name$u1$u1') | ~sub(X4,'jahr$u$u1$u1') | ~sub(X5,'name$u1$u1') | ~sub(X1,'firma$u1$u1') | ~attr(X6,X4) | ~attr(X7,X3) | ~attr(X1,X5) | ~val(X3,'bmw$u0') | ~val(X5,'bmw$u0'), inference(resolution, [status(thm)], [c392,c448])).
% 67.68/11.65 cnf(d6, plain, ~sub(X0,'name$u1$u1') | ~sub(X1,'jahr$u$u1$u1') | ~sub(X2,'name$u1$u1') | ~sub(X3,'firma$u1$u1') | ~attr(X4,X2) | ~attr(X5,X1) | ~attr(X3,X0) | ~val(X0,'bmw$u0') | ~val(X2,'bmw$u0') | ~subs(X6,'hei$u$u337en$u1$u1') | ~arg1(X6,X3) | ~arg2(X6,X7), inference(resolution, [status(thm)], [d5,c387])).
% 67.68/11.65 cnf(d7, plain, ~sub(X0,X1) | ~attr(X2,X0) | arg2(sK227(X2),X2) | ~member(X1,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c381,c228])).
% 67.68/11.65 cnf(d8, plain, ~sub(X0,X1) | ~attr(X2,X0) | arg2(sK227(X2),X2) | ~member(X1,cons('name$u1$u1',nil)), inference(resolution, [status(thm)], [d7,c228])).
% 67.68/11.65 cnf(d9, plain, ~sub(X0,'name$u1$u1') | ~attr(X1,X0) | arg2(sK227(X1),X1), inference(resolution, [status(thm)], [d8,c227])).
% 67.68/11.65 cnf(d10, plain, ~sub(c2213,'name$u1$u1') | arg2(sK227(c2212),c2212), inference(resolution, [status(thm)], [d9,c13])).
% 67.68/11.65 cnf(d11, plain, arg2(sK227(c2212),c2212), inference(resolution, [status(thm)], [c15,d10])).
% 67.68/11.65 cnf(d12, plain, ~sub(X0,'firma$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(X2,'jahr$u$u1$u1') | ~sub(X3,'name$u1$u1') | ~attr(X4,X2) | ~attr(X5,X1) | ~attr(X0,X3) | ~val(X1,'bmw$u0') | ~val(X3,'bmw$u0') | ~subs(sK227(c2212),'hei$u$u337en$u1$u1') | ~arg1(sK227(c2212),X0), inference(resolution, [status(thm)], [d11,d6])).
% 67.68/11.65 cnf(d13, plain, ~sub(X0,'name$u1$u1') | ~sub(X1,'jahr$u$u1$u1') | ~sub(X2,'name$u1$u1') | ~sub(c2212,'firma$u1$u1') | ~attr(X3,X2) | ~attr(X4,X1) | ~attr(c2212,X0) | ~val(X0,'bmw$u0') | ~val(X2,'bmw$u0') | ~subs(sK227(c2212),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [d12,d4])).
% 67.68/11.65 cnf(d14, plain, ~sub(X0,'name$u1$u1') | ~sub(X1,'jahr$u$u1$u1') | ~sub(X2,'name$u1$u1') | ~attr(X3,X1) | ~attr(X4,X0) | ~attr(c2212,X2) | ~val(X0,'bmw$u0') | ~val(X2,'bmw$u0') | ~subs(sK227(c2212),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [c14,d13])).
% 67.68/11.65 cnf(d15, plain, ~sub(X0,X1) | ~attr(X2,X0) | subs(sK227(X2),'hei$u$u337en$u1$u1') | ~member(X1,cons('familiename$u1$u1',cons('name$u1$u1',nil))), inference(resolution, [status(thm)], [c382,c228])).
% 67.68/11.65 cnf(d16, plain, ~sub(X0,X1) | ~attr(X2,X0) | subs(sK227(X2),'hei$u$u337en$u1$u1') | ~member(X1,cons('name$u1$u1',nil)), inference(resolution, [status(thm)], [d15,c228])).
% 67.68/11.65 cnf(d17, plain, ~sub(X0,'name$u1$u1') | ~attr(X1,X0) | subs(sK227(X1),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [d16,c227])).
% 67.68/11.65 cnf(d18, plain, ~sub(c2213,'name$u1$u1') | subs(sK227(c2212),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [d17,c13])).
% 67.68/11.65 cnf(d19, plain, subs(sK227(c2212),'hei$u$u337en$u1$u1'), inference(resolution, [status(thm)], [c15,d18])).
% 67.68/11.65 cnf(d20, plain, ~sub(X0,'name$u1$u1') | ~sub(X1,'jahr$u$u1$u1') | ~sub(X2,'name$u1$u1') | ~attr(X3,X2) | ~attr(X4,X1) | ~attr(c2212,X0) | ~val(X0,'bmw$u0') | ~val(X2,'bmw$u0'), inference(resolution, [status(thm)], [d19,d14])).
% 67.68/11.65 cnf(d21, plain, ~sub(X0,'name$u1$u1') | ~sub(X1,'jahr$u$u1$u1') | ~sub(c2213,'name$u1$u1') | ~attr(X2,X1) | ~attr(X3,X0) | ~attr(c2212,c2213) | ~val(X0,'bmw$u0'), inference(resolution, [status(thm)], [d20,c16])).
% 67.68/11.65 cnf(d22, plain, ~sub(X0,'jahr$u$u1$u1') | ~sub(X1,'name$u1$u1') | ~sub(c2213,'name$u1$u1') | ~attr(X2,X1) | ~attr(X3,X0) | ~val(X1,'bmw$u0'), inference(resolution, [status(thm)], [c13,d21])).
% 67.68/11.65 cnf(d23, plain, ~sub(X0,'name$u1$u1') | ~sub(X1,'jahr$u$u1$u1') | ~attr(X2,X1) | ~attr(X3,X0) | ~val(X0,'bmw$u0'), inference(resolution, [status(thm)], [c15,d22])).
% 67.68/11.65 cnf(d24, plain, ~sub(X0,'jahr$u$u1$u1') | ~sub(c2213,'name$u1$u1') | ~attr(X1,c2213) | ~attr(X2,X0), inference(resolution, [status(thm)], [d23,c16])).
% 67.68/11.65 cnf(d25, plain, ~sub(X0,'jahr$u$u1$u1') | ~attr(X1,X0) | ~attr(X2,c2213), inference(resolution, [status(thm)], [c15,d24])).
% 67.68/11.65 cnf(d26, plain, ~sub(c2205,'jahr$u$u1$u1') | ~attr(X0,c2213), inference(resolution, [status(thm)], [d25,c10])).
% 67.68/11.65 cnf(d27, plain, ~attr(X0,c2213), inference(resolution, [status(thm)], [c11,d26])).
% 67.68/11.65 cnf(d28, plain, $false, inference(resolution, [status(thm)], [d27,c13])).
% 67.68/11.65 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------