%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : SWC002+1 : TPTP v9.3.1. Released v2.4.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 08:53:53 AM UTC 2026 % Result : Theorem 39.38s 9.84s % Output : CNFRefutation 39.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWC002+1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.11/0.37 % Computer : n005.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Sat Sep 26 12:02:18 UTC 2026 % 0.04/0.37 % CPUTime : % 0.04/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 39.38/9.84 % SZS status Theorem for theBenchmark.p % 39.38/9.84 % SZS output start CNFRefutation for theBenchmark.p % 39.38/9.84 fof(ax3, axiom, ! [X0] : ((ssList(X0) => ! [X1] : ((ssItem(X1) => (memberP(X0,X1) <=> ? [X2] : ((ssList(X2) & ? [X3] : ((ssList(X3) & app(X2,cons(X1,X3)) = X0)))))))))). % 39.38/9.84 fof(co1, conjecture, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ! [X2] : ((ssList(X2) => ! [X3] : ((ssList(X3) => (X1 != X3 | (X0 != X2 | ((~neq(X1,nil) | (? [X4] : ((ssItem(X4) & ? [X5] : ((ssList(X5) & ? [X6] : ((ssList(X6) & (app(app(X5,cons(X4,nil)),X6) = X1 & (app(X5,X6) = X0 & ! [X7] : ((ssItem(X7) => (~memberP(X1,X7) | (~geq(X7,X4) | X4 = X7)))))))))))) | ! [X8] : ((ssItem(X8) => ! [X9] : ((ssList(X9) => ! [X10] : ((ssList(X10) => (app(app(X9,cons(X8,nil)),X10) != X3 | (app(X9,X10) != X2 | ? [X11] : ((ssItem(X11) & (X8 != X11 & (memberP(X3,X11) & geq(X11,X8))))))))))))))) & (~neq(X1,nil) | neq(X3,nil)))))))))))))). % 39.38/9.84 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ! [X2] : ((ssList(X2) => ! [X3] : ((ssList(X3) => (X1 != X3 | (X0 != X2 | ((~neq(X1,nil) | (? [X4] : ((ssItem(X4) & ? [X5] : ((ssList(X5) & ? [X6] : ((ssList(X6) & (app(app(X5,cons(X4,nil)),X6) = X1 & (app(X5,X6) = X0 & ! [X7] : ((ssItem(X7) => (~memberP(X1,X7) | (~geq(X7,X4) | X4 = X7)))))))))))) | ! [X8] : ((ssItem(X8) => ! [X9] : ((ssList(X9) => ! [X10] : ((ssList(X10) => (app(app(X9,cons(X8,nil)),X10) != X3 | (app(X9,X10) != X2 | ? [X11] : ((ssItem(X11) & (X8 != X11 & (memberP(X3,X11) & geq(X11,X8))))))))))))))) & (~neq(X1,nil) | neq(X3,nil))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 39.38/9.84 cnf(c7, plain, ~ssList(X0) | ~ssItem(X1) | ~memberP(X0,X1) | app(sK6(X0,X1),cons(X1,sK7(X0,X1))) = X0, inference(clausification, [status(esa)], [ax3])). % 39.38/9.84 cnf(c200, plain, ssList(sK255), inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c203, plain, sK256 = sK254, inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c204, plain, X0(sK254,sK255,sK256,sK257) | neq(sK255,nil), inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c205, plain, X0(sK254,sK255,sK256,sK257) | ~neq(sK257,nil), inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c206, plain, sK257 = sK255, inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c207, plain, ~X0(X1,X2,X3,X4) | neq(X2,nil), inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c208, plain, ~X0(X1,X2,X3,X4) | ssItem(sK258(X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c209, plain, ~X0(X1,X2,X3,X4) | ssList(sK259(X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c210, plain, ~X0(X1,X2,X3,X4) | ssList(sK260(X3,X4)), inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c211, plain, ~X0(X1,X2,X3,X4) | app(sK259(X3,X4),sK260(X3,X4)) = X3, inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c212, plain, ~geq(X0,sK258(X1,X2)) | ~X3(X4,X5,X1,X2) | ~memberP(X2,X0) | ~ssItem(X0) | X0 = sK258(X1,X2), inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c213, plain, ~X0(X1,X2,X3,X4) | app(app(sK259(X3,X4),cons(sK258(X3,X4),nil)),sK260(X3,X4)) = X4, inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c214, plain, ssItem(sK265(X0,X1)) | ~ssItem(X1) | ~ssList(X2) | ~ssList(X3) | ~X4(X5,X0,X6,X7) | app(X2,X3) != X5 | app(app(X2,cons(X1,nil)),X3) != X0, inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c215, plain, ~ssItem(X0) | ~ssList(X1) | ~ssList(X2) | ~X3(X4,X5,X6,X7) | app(X1,X2) != X4 | app(app(X1,cons(X0,nil)),X2) != X5 | geq(sK265(X5,X0),X0), inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c216, plain, sK265(X0,X1) != X1 | ~ssItem(X1) | ~ssList(X2) | ~ssList(X3) | ~X4(X5,X0,X6,X7) | app(X2,X3) != X5 | app(app(X2,cons(X1,nil)),X3) != X0, inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(c217, plain, ~ssItem(X0) | ~ssList(X1) | ~ssList(X2) | ~X3(X4,X5,X6,X7) | app(app(X1,cons(X0,nil)),X2) != X5 | app(X1,X2) != X4 | memberP(X5,sK265(X5,X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 39.38/9.84 cnf(d0, plain, ~neq(sK255,nil) | 'Ts253'(sK254,sK255,sK256,sK257), inference(demodulation, [status(thm)], [c205,c206])). % 39.38/9.84 cnf(d1, plain, ~neq(sK255,nil) | 'Ts253'(sK254,sK255,sK254,sK257), inference(demodulation, [status(thm)], [d0,c203])). % 39.38/9.84 cnf(d2, plain, ~neq(sK255,nil) | 'Ts253'(sK254,sK255,sK254,sK255), inference(demodulation, [status(thm)], [d1,c206])). % 39.38/9.84 cnf(d3, plain, neq(sK255,nil) | 'Ts253'(sK254,sK255,sK254,sK257), inference(demodulation, [status(thm)], [c204,c203])). % 39.38/9.84 cnf(d4, plain, neq(sK255,nil) | 'Ts253'(sK254,sK255,sK254,sK255), inference(demodulation, [status(thm)], [d3,c206])). % 39.38/9.84 cnf(d5, plain, neq(sK255,nil) | neq(sK255,nil), inference(resolution, [status(thm)], [c207,d4])). % 39.38/9.84 cnf(d6, plain, 'Ts253'(sK254,sK255,sK254,sK255), inference(resolution, [status(thm)], [d5,d2])). % 39.38/9.84 cnf(d7, plain, app(sK259(sK254,sK255),sK260(sK254,sK255)) = sK254, inference(resolution, [status(thm)], [c211,d6])). % 39.38/9.84 cnf(d8, plain, app(app(sK259(sK254,sK255),cons(sK258(sK254,sK255),nil)),sK260(sK254,sK255)) = sK255, inference(resolution, [status(thm)], [c213,d6])). % 39.38/9.84 cnf(d9, plain, sK255 != X0 | app(sK259(sK254,sK255),sK260(sK254,sK255)) != X1 | sK265(X0,sK258(sK254,sK255)) != sK258(sK254,sK255) | ~ssItem(sK258(sK254,sK255)) | ~ssList(sK260(sK254,sK255)) | ~ssList(sK259(sK254,sK255)) | ~'Ts253'(X1,X0,X2,X3), inference(superposition, [status(thm)], [d8,c216])). % 39.38/9.84 cnf(d10, plain, sK254 != X0 | sK255 != X1 | sK265(X1,sK258(sK254,sK255)) != sK258(sK254,sK255) | ~ssItem(sK258(sK254,sK255)) | ~ssList(sK259(sK254,sK255)) | ~ssList(sK260(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(demodulation, [status(thm)], [d9,d7])). % 39.38/9.84 cnf(d11, plain, ssItem(sK258(sK254,sK255)), inference(resolution, [status(thm)], [c208,d6])). % 39.38/9.84 cnf(d12, plain, sK254 != X0 | sK255 != X1 | sK265(X1,sK258(sK254,sK255)) != sK258(sK254,sK255) | ~ssList(sK259(sK254,sK255)) | ~ssList(sK260(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d11,d10])). % 39.38/9.84 cnf(d13, plain, ssList(sK259(sK254,sK255)), inference(resolution, [status(thm)], [c209,d6])). % 39.38/9.84 cnf(d14, plain, sK254 != X0 | sK255 != X1 | sK265(X1,sK258(sK254,sK255)) != sK258(sK254,sK255) | ~ssList(sK260(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d13,d12])). % 39.38/9.84 cnf(d15, plain, ssList(sK260(sK254,sK255)), inference(resolution, [status(thm)], [c210,d6])). % 39.38/9.84 cnf(d16, plain, sK254 != X0 | sK255 != X1 | sK265(X1,sK258(sK254,sK255)) != sK258(sK254,sK255) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d15,d14])). % 39.38/9.84 cnf(d17, plain, X0 = sK258(sK254,sK255) | ~ssItem(X0) | ~memberP(sK255,X0) | ~geq(X0,sK258(sK254,sK255)), inference(resolution, [status(thm)], [c212,d6])). % 39.38/9.84 cnf(d18, plain, sK255 != X0 | app(sK259(sK254,sK255),sK260(sK254,sK255)) != X1 | ~ssItem(sK258(sK254,sK255)) | ~ssList(sK260(sK254,sK255)) | ~ssList(sK259(sK254,sK255)) | geq(sK265(X0,sK258(sK254,sK255)),sK258(sK254,sK255)) | ~'Ts253'(X1,X0,X2,X3), inference(superposition, [status(thm)], [d8,c215])). % 39.38/9.84 cnf(d19, plain, sK254 != X0 | sK255 != X1 | ~ssItem(sK258(sK254,sK255)) | ~ssList(sK259(sK254,sK255)) | ~ssList(sK260(sK254,sK255)) | geq(sK265(X1,sK258(sK254,sK255)),sK258(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(demodulation, [status(thm)], [d18,d7])). % 39.38/9.84 cnf(d20, plain, sK254 != X0 | sK255 != X1 | ~ssList(sK259(sK254,sK255)) | ~ssList(sK260(sK254,sK255)) | geq(sK265(X1,sK258(sK254,sK255)),sK258(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d11,d19])). % 39.38/9.84 cnf(d21, plain, sK254 != X0 | sK255 != X1 | ~ssList(sK260(sK254,sK255)) | geq(sK265(X1,sK258(sK254,sK255)),sK258(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d13,d20])). % 39.38/9.84 cnf(d22, plain, sK254 != X0 | sK255 != X1 | geq(sK265(X1,sK258(sK254,sK255)),sK258(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d15,d21])). % 39.38/9.84 cnf(d23, plain, sK254 != X0 | geq(sK265(sK255,sK258(sK254,sK255)),sK258(sK254,sK255)) | ~'Ts253'(X0,sK255,X1,X2), inference(equality_resolution, [status(thm)], [d22])). % 39.38/9.84 cnf(d24, plain, geq(sK265(sK255,sK258(sK254,sK255)),sK258(sK254,sK255)) | ~'Ts253'(sK254,sK255,X0,X1), inference(equality_resolution, [status(thm)], [d23])). % 39.38/9.84 cnf(d25, plain, geq(sK265(sK255,sK258(sK254,sK255)),sK258(sK254,sK255)), inference(resolution, [status(thm)], [d24,d6])). % 39.38/9.84 cnf(d26, plain, sK265(sK255,sK258(sK254,sK255)) = sK258(sK254,sK255) | ~ssItem(sK265(sK255,sK258(sK254,sK255))) | ~memberP(sK255,sK265(sK255,sK258(sK254,sK255))), inference(resolution, [status(thm)], [d25,d17])). % 39.38/9.84 cnf(d27, plain, sK255 != X0 | app(sK259(sK254,sK255),sK260(sK254,sK255)) != X1 | ~ssItem(sK258(sK254,sK255)) | ssItem(sK265(X0,sK258(sK254,sK255))) | ~ssList(sK260(sK254,sK255)) | ~ssList(sK259(sK254,sK255)) | ~'Ts253'(X1,X0,X2,X3), inference(superposition, [status(thm)], [d8,c214])). % 39.38/9.84 cnf(d28, plain, sK254 != X0 | sK255 != X1 | ~ssItem(sK258(sK254,sK255)) | ssItem(sK265(X1,sK258(sK254,sK255))) | ~ssList(sK259(sK254,sK255)) | ~ssList(sK260(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(demodulation, [status(thm)], [d27,d7])). % 39.38/9.84 cnf(d29, plain, sK254 != X0 | sK255 != X1 | ssItem(sK265(X1,sK258(sK254,sK255))) | ~ssList(sK259(sK254,sK255)) | ~ssList(sK260(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d11,d28])). % 39.38/9.84 cnf(d30, plain, sK254 != X0 | sK255 != X1 | ssItem(sK265(X1,sK258(sK254,sK255))) | ~ssList(sK260(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d13,d29])). % 39.38/9.84 cnf(d31, plain, sK254 != X0 | sK255 != X1 | ssItem(sK265(X1,sK258(sK254,sK255))) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d15,d30])). % 39.38/9.84 cnf(d32, plain, sK254 != X0 | ssItem(sK265(sK255,sK258(sK254,sK255))) | ~'Ts253'(X0,sK255,X1,X2), inference(equality_resolution, [status(thm)], [d31])). % 39.38/9.84 cnf(d33, plain, ssItem(sK265(sK255,sK258(sK254,sK255))) | ~'Ts253'(sK254,sK255,X0,X1), inference(equality_resolution, [status(thm)], [d32])). % 39.38/9.84 cnf(d34, plain, ssItem(sK265(sK255,sK258(sK254,sK255))), inference(resolution, [status(thm)], [d33,d6])). % 39.38/9.84 cnf(d35, plain, sK265(sK255,sK258(sK254,sK255)) = sK258(sK254,sK255) | ~memberP(sK255,sK265(sK255,sK258(sK254,sK255))), inference(resolution, [status(thm)], [d34,d26])). % 39.38/9.84 cnf(d36, plain, sK255 != X0 | app(sK259(sK254,sK255),sK260(sK254,sK255)) != X1 | ~ssItem(sK258(sK254,sK255)) | memberP(X0,sK265(X0,sK258(sK254,sK255))) | ~ssList(sK260(sK254,sK255)) | ~ssList(sK259(sK254,sK255)) | ~'Ts253'(X1,X0,X2,X3), inference(superposition, [status(thm)], [d8,c217])). % 39.38/9.84 cnf(d37, plain, sK254 != X0 | sK255 != X1 | ~ssItem(sK258(sK254,sK255)) | memberP(X1,sK265(X1,sK258(sK254,sK255))) | ~ssList(sK259(sK254,sK255)) | ~ssList(sK260(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(demodulation, [status(thm)], [d36,d7])). % 39.38/9.84 cnf(d38, plain, sK254 != X0 | sK255 != X1 | memberP(X1,sK265(X1,sK258(sK254,sK255))) | ~ssList(sK259(sK254,sK255)) | ~ssList(sK260(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d11,d37])). % 39.38/9.84 cnf(d39, plain, sK254 != X0 | sK255 != X1 | memberP(X1,sK265(X1,sK258(sK254,sK255))) | ~ssList(sK260(sK254,sK255)) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d13,d38])). % 39.38/9.84 cnf(d40, plain, sK254 != X0 | sK255 != X1 | memberP(X1,sK265(X1,sK258(sK254,sK255))) | ~'Ts253'(X0,X1,X2,X3), inference(resolution, [status(thm)], [d15,d39])). % 39.38/9.84 cnf(d41, plain, sK254 != X0 | memberP(sK255,sK265(sK255,sK258(sK254,sK255))) | ~'Ts253'(X0,sK255,X1,X2), inference(equality_resolution, [status(thm)], [d40])). % 39.38/9.84 cnf(d42, plain, memberP(sK255,sK265(sK255,sK258(sK254,sK255))) | ~'Ts253'(sK254,sK255,X0,X1), inference(equality_resolution, [status(thm)], [d41])). % 39.38/9.84 cnf(d43, plain, memberP(sK255,sK265(sK255,sK258(sK254,sK255))), inference(resolution, [status(thm)], [d42,d6])). % 39.38/9.84 cnf(d44, plain, sK265(sK255,sK258(sK254,sK255)) = sK258(sK254,sK255), inference(resolution, [status(thm)], [d43,d35])). % 39.38/9.84 cnf(d45, plain, sK258(sK254,sK255) != sK258(sK254,sK255) | sK254 != X0 | sK255 != sK255 | ~'Ts253'(X0,sK255,X1,X2), inference(superposition, [status(thm)], [d44,d16])). % 39.38/9.84 cnf(d46, plain, app(sK6(sK255,sK265(sK255,sK258(sK254,sK255))),cons(sK265(sK255,sK258(sK254,sK255)),sK7(sK255,sK265(sK255,sK258(sK254,sK255))))) = sK255 | ~ssItem(sK265(sK255,sK258(sK254,sK255))) | ~ssList(sK255), inference(resolution, [status(thm)], [d43,c7])). % 39.38/9.84 cnf(d47, plain, app(sK6(sK255,sK265(sK255,sK258(sK254,sK255))),cons(sK265(sK255,sK258(sK254,sK255)),sK7(sK255,sK265(sK255,sK258(sK254,sK255))))) = sK255 | ~ssItem(sK265(sK255,sK258(sK254,sK255))), inference(resolution, [status(thm)], [c200,d46])). % 39.38/9.84 cnf(d48, plain, app(sK6(sK255,sK265(sK255,sK258(sK254,sK255))),cons(sK265(sK255,sK258(sK254,sK255)),sK7(sK255,sK265(sK255,sK258(sK254,sK255))))) = sK255, inference(resolution, [status(thm)], [d34,d47])). % 39.38/9.84 cnf(d49, plain, app(sK6(sK255,sK258(sK254,sK255)),cons(sK265(sK255,sK258(sK254,sK255)),sK7(sK255,sK265(sK255,sK258(sK254,sK255))))) = sK255, inference(demodulation, [status(thm)], [d48,d44])). % 39.38/9.84 cnf(d50, plain, app(sK6(sK255,sK258(sK254,sK255)),cons(sK258(sK254,sK255),sK7(sK255,sK265(sK255,sK258(sK254,sK255))))) = sK255, inference(demodulation, [status(thm)], [d49,d44])). % 39.38/9.84 cnf(d51, plain, app(sK6(sK255,sK258(sK254,sK255)),cons(sK258(sK254,sK255),sK7(sK255,sK258(sK254,sK255)))) = sK255, inference(demodulation, [status(thm)], [d50,d44])). % 39.38/9.84 cnf(d52, plain, memberP(sK255,sK258(sK254,sK255)), inference(demodulation, [status(thm)], [d43,d44])). % 39.38/9.84 cnf(d53, plain, app(sK6(sK255,sK258(sK254,sK255)),cons(sK258(sK254,sK255),sK7(sK255,sK258(sK254,sK255)))) = sK255 | ~ssItem(sK258(sK254,sK255)) | ~ssList(sK255), inference(resolution, [status(thm)], [d52,c7])). % 39.38/9.84 cnf(d54, plain, sK255 = sK255 | ~ssItem(sK258(sK254,sK255)) | ~ssList(sK255), inference(demodulation, [status(thm)], [d53,d51])). % 39.38/9.84 cnf(d55, plain, sK255 = sK255 | ~ssItem(sK258(sK254,sK255)), inference(resolution, [status(thm)], [c200,d54])). % 39.38/9.84 cnf(d56, plain, sK255 = sK255, inference(resolution, [status(thm)], [d11,d55])). % 39.38/9.84 cnf(d57, plain, sK254 != X0 | sK258(sK254,sK255) != sK258(sK254,sK255) | ~'Ts253'(X0,sK255,X1,X2), inference(resolution, [status(thm)], [d56,d45])). % 39.38/9.84 cnf(d58, plain, sK254 != X0 | ~'Ts253'(X0,sK255,X1,X2), inference(equality_resolution, [status(thm)], [d57])). % 39.38/9.84 cnf(d59, plain, ~'Ts253'(sK254,sK255,X0,X1), inference(equality_resolution, [status(thm)], [d58])). % 39.38/9.84 cnf(d60, plain, $false, inference(resolution, [status(thm)], [d59,d6])). % 39.38/9.84 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------