%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : COM022+4 : 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 : n012.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 06:58:45 AM UTC 2026 % Result : Theorem 16.65s 8.15s % Output : CNFRefutation 16.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : COM022+4 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.05/5.93 % Computer : n012.cluster.edu % 0.05/5.93 % Model : x86_64 x86_64 % 0.05/5.93 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.05/5.93 % Memory : 8046.5625MB % 0.05/5.93 % OS : Linux 6.8.0-71-generic % 0.05/5.94 % CPULimit : 300 % 0.05/5.94 % WCLimit : 300 % 0.05/5.94 % DateTime : Sat Sep 26 23:23:05 UTC 2026 % 0.05/5.94 % CPUTime : % 0.05/5.94 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 16.65/8.15 % SZS status Theorem for theBenchmark.p % 16.65/8.15 % SZS output start CNFRefutation for theBenchmark.p % 16.65/8.15 fof(m__731, hypothesis, (aElement0(xa) & (aElement0(xb) & aElement0(xc)))). % 16.65/8.15 fof(m__, conjecture, ((((aReductOfIn0(xb,xa,xR) | (? [X0] : ((aElement0(X0) & (aReductOfIn0(X0,xa,xR) & sdtmndtplgtdt0(X0,xR,xb)))) | sdtmndtplgtdt0(xa,xR,xb))) & (aReductOfIn0(xc,xa,xR) | (? [X0] : ((aElement0(X0) & (aReductOfIn0(X0,xa,xR) & sdtmndtplgtdt0(X0,xR,xc)))) | sdtmndtplgtdt0(xa,xR,xc)))) => ? [X0] : ((aElement0(X0) & (aReductOfIn0(X0,xa,xR) & ((X0 = xb | ((aReductOfIn0(xb,X0,xR) | ? [X1] : ((aElement0(X1) & (aReductOfIn0(X1,X0,xR) & sdtmndtplgtdt0(X1,xR,xb))))) & sdtmndtplgtdt0(X0,xR,xb))) & (sdtmndtasgtdt0(X0,xR,xb) & ? [X1] : ((aElement0(X1) & (aReductOfIn0(X1,xa,xR) & ((X1 = xc | ((aReductOfIn0(xc,X1,xR) | ? [X2] : ((aElement0(X2) & (aReductOfIn0(X2,X1,xR) & sdtmndtplgtdt0(X2,xR,xc))))) & sdtmndtplgtdt0(X1,xR,xc))) & (sdtmndtasgtdt0(X1,xR,xc) & ? [X2] : ((aElement0(X2) & ((X0 = X2 | ((aReductOfIn0(X2,X0,xR) | ? [X3] : ((aElement0(X3) & (aReductOfIn0(X3,X0,xR) & sdtmndtplgtdt0(X3,xR,X2))))) & sdtmndtplgtdt0(X0,xR,X2))) & (sdtmndtasgtdt0(X0,xR,X2) & ((X1 = X2 | ((aReductOfIn0(X2,X1,xR) | ? [X3] : ((aElement0(X3) & (aReductOfIn0(X3,X1,xR) & sdtmndtplgtdt0(X3,xR,X2))))) & sdtmndtplgtdt0(X1,xR,X2))) & (sdtmndtasgtdt0(X1,xR,X2) & ? [X3] : ((aElement0(X3) & ((X2 = X3 | ((aReductOfIn0(X3,X2,xR) | ? [X4] : ((aElement0(X4) & (aReductOfIn0(X4,X2,xR) & sdtmndtplgtdt0(X4,xR,X3))))) & sdtmndtplgtdt0(X2,xR,X3))) & (sdtmndtasgtdt0(X2,xR,X3) & (~? [X4] : aReductOfIn0(X4,X3,xR) & (aNormalFormOfIn0(X3,X2,xR) & ((xb = X3 | ((aReductOfIn0(X3,xb,xR) | ? [X4] : ((aElement0(X4) & (aReductOfIn0(X4,xb,xR) & sdtmndtplgtdt0(X4,xR,X3))))) & sdtmndtplgtdt0(xb,xR,X3))) & (sdtmndtasgtdt0(xb,xR,X3) & ((xc = X3 | ((aReductOfIn0(X3,xc,xR) | ? [X4] : ((aElement0(X4) & (aReductOfIn0(X4,xc,xR) & sdtmndtplgtdt0(X4,xR,X3))))) & sdtmndtplgtdt0(xc,xR,X3))) & sdtmndtasgtdt0(xc,xR,X3))))))))))))))))))))))))))) => (((xa = xb | ((aReductOfIn0(xb,xa,xR) | ? [X0] : ((aElement0(X0) & (aReductOfIn0(X0,xa,xR) & sdtmndtplgtdt0(X0,xR,xb))))) & sdtmndtplgtdt0(xa,xR,xb))) & (sdtmndtasgtdt0(xa,xR,xb) & ((xa = xc | ((aReductOfIn0(xc,xa,xR) | ? [X0] : ((aElement0(X0) & (aReductOfIn0(X0,xa,xR) & sdtmndtplgtdt0(X0,xR,xc))))) & sdtmndtplgtdt0(xa,xR,xc))) & sdtmndtasgtdt0(xa,xR,xc)))) => ? [X0] : ((aElement0(X0) & ((xb = X0 | (aReductOfIn0(X0,xb,xR) | (? [X1] : ((aElement0(X1) & (aReductOfIn0(X1,xb,xR) & sdtmndtplgtdt0(X1,xR,X0)))) | (sdtmndtplgtdt0(xb,xR,X0) | sdtmndtasgtdt0(xb,xR,X0))))) & (xc = X0 | (aReductOfIn0(X0,xc,xR) | (? [X1] : ((aElement0(X1) & (aReductOfIn0(X1,xc,xR) & sdtmndtplgtdt0(X1,xR,X0)))) | (sdtmndtplgtdt0(xc,xR,X0) | sdtmndtasgtdt0(xc,xR,X0))))))))))). % 16.65/8.15 fof(negated_conjecture, negated_conjecture, ~(((((aReductOfIn0(xb,xa,xR) | (? [X0] : ((aElement0(X0) & (aReductOfIn0(X0,xa,xR) & sdtmndtplgtdt0(X0,xR,xb)))) | sdtmndtplgtdt0(xa,xR,xb))) & (aReductOfIn0(xc,xa,xR) | (? [X0] : ((aElement0(X0) & (aReductOfIn0(X0,xa,xR) & sdtmndtplgtdt0(X0,xR,xc)))) | sdtmndtplgtdt0(xa,xR,xc)))) => ? [X0] : ((aElement0(X0) & (aReductOfIn0(X0,xa,xR) & ((X0 = xb | ((aReductOfIn0(xb,X0,xR) | ? [X1] : ((aElement0(X1) & (aReductOfIn0(X1,X0,xR) & sdtmndtplgtdt0(X1,xR,xb))))) & sdtmndtplgtdt0(X0,xR,xb))) & (sdtmndtasgtdt0(X0,xR,xb) & ? [X1] : ((aElement0(X1) & (aReductOfIn0(X1,xa,xR) & ((X1 = xc | ((aReductOfIn0(xc,X1,xR) | ? [X2] : ((aElement0(X2) & (aReductOfIn0(X2,X1,xR) & sdtmndtplgtdt0(X2,xR,xc))))) & sdtmndtplgtdt0(X1,xR,xc))) & (sdtmndtasgtdt0(X1,xR,xc) & ? [X2] : ((aElement0(X2) & ((X0 = X2 | ((aReductOfIn0(X2,X0,xR) | ? [X3] : ((aElement0(X3) & (aReductOfIn0(X3,X0,xR) & sdtmndtplgtdt0(X3,xR,X2))))) & sdtmndtplgtdt0(X0,xR,X2))) & (sdtmndtasgtdt0(X0,xR,X2) & ((X1 = X2 | ((aReductOfIn0(X2,X1,xR) | ? [X3] : ((aElement0(X3) & (aReductOfIn0(X3,X1,xR) & sdtmndtplgtdt0(X3,xR,X2))))) & sdtmndtplgtdt0(X1,xR,X2))) & (sdtmndtasgtdt0(X1,xR,X2) & ? [X3] : ((aElement0(X3) & ((X2 = X3 | ((aReductOfIn0(X3,X2,xR) | ? [X4] : ((aElement0(X4) & (aReductOfIn0(X4,X2,xR) & sdtmndtplgtdt0(X4,xR,X3))))) & sdtmndtplgtdt0(X2,xR,X3))) & (sdtmndtasgtdt0(X2,xR,X3) & (~? [X4] : aReductOfIn0(X4,X3,xR) & (aNormalFormOfIn0(X3,X2,xR) & ((xb = X3 | ((aReductOfIn0(X3,xb,xR) | ? [X4] : ((aElement0(X4) & (aReductOfIn0(X4,xb,xR) & sdtmndtplgtdt0(X4,xR,X3))))) & sdtmndtplgtdt0(xb,xR,X3))) & (sdtmndtasgtdt0(xb,xR,X3) & ((xc = X3 | ((aReductOfIn0(X3,xc,xR) | ? [X4] : ((aElement0(X4) & (aReductOfIn0(X4,xc,xR) & sdtmndtplgtdt0(X4,xR,X3))))) & sdtmndtplgtdt0(xc,xR,X3))) & sdtmndtasgtdt0(xc,xR,X3))))))))))))))))))))))))))) => (((xa = xb | ((aReductOfIn0(xb,xa,xR) | ? [X0] : ((aElement0(X0) & (aReductOfIn0(X0,xa,xR) & sdtmndtplgtdt0(X0,xR,xb))))) & sdtmndtplgtdt0(xa,xR,xb))) & (sdtmndtasgtdt0(xa,xR,xb) & ((xa = xc | ((aReductOfIn0(xc,xa,xR) | ? [X0] : ((aElement0(X0) & (aReductOfIn0(X0,xa,xR) & sdtmndtplgtdt0(X0,xR,xc))))) & sdtmndtplgtdt0(xa,xR,xc))) & sdtmndtasgtdt0(xa,xR,xc)))) => ? [X0] : ((aElement0(X0) & ((xb = X0 | (aReductOfIn0(X0,xb,xR) | (? [X1] : ((aElement0(X1) & (aReductOfIn0(X1,xb,xR) & sdtmndtplgtdt0(X1,xR,X0)))) | (sdtmndtplgtdt0(xb,xR,X0) | sdtmndtasgtdt0(xb,xR,X0))))) & (xc = X0 | (aReductOfIn0(X0,xc,xR) | (? [X1] : ((aElement0(X1) & (aReductOfIn0(X1,xc,xR) & sdtmndtplgtdt0(X1,xR,X0)))) | (sdtmndtplgtdt0(xc,xR,X0) | sdtmndtasgtdt0(xc,xR,X0))))))))))), inference(negate_conjecture, [status(cth)], [m__])). % 16.65/8.15 cnf(c66, plain, aElement0(xb), inference(clausification, [status(esa)], [m__731])). % 16.65/8.15 cnf(c67, plain, aElement0(xc), inference(clausification, [status(esa)], [m__731])). % 16.65/8.15 cnf(c92, plain, ~X0 | ~sdtmndtplgtdt0(xa,xR,xc) | X1, inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c96, plain, xa = xb | sdtmndtplgtdt0(xa,xR,xb), inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c101, plain, xa = xc | sdtmndtplgtdt0(xa,xR,xc), inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c102, plain, sdtmndtasgtdt0(xa,xR,xc), inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c103, plain, ~aElement0(X0) | ~X1(X0) | ~X2(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c106, plain, X0 | ~sdtmndtplgtdt0(xa,xR,xb), inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c132, plain, ~X0 | aElement0(sK98), inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c144, plain, ~X0 | sdtmndtasgtdt0(xb,xR,sK98), inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c149, plain, ~X0 | sdtmndtasgtdt0(xc,xR,sK98), inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c150, plain, X0(X1) | xb != X1, inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c154, plain, X0(X1) | ~sdtmndtasgtdt0(xb,xR,X1), inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c155, plain, X0(X1) | xc != X1, inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c158, plain, X0(X1) | ~sdtmndtplgtdt0(xc,xR,X1), inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(c159, plain, X0(X1) | ~sdtmndtasgtdt0(xc,xR,X1), inference(clausification, [status(esa)], [negated_conjecture])). % 16.65/8.15 cnf(d0, plain, 'Ts84'(sK98) | ~'Ts83', inference(resolution, [status(thm)], [c154,c144])). % 16.65/8.15 cnf(d1, plain, 'Ts85'(sK98) | ~'Ts83', inference(resolution, [status(thm)], [c159,c149])). % 16.65/8.15 cnf(d2, plain, ~aElement0(sK98) | ~'Ts84'(sK98) | ~'Ts83', inference(resolution, [status(thm)], [c103,d1])). % 16.65/8.15 cnf(d3, plain, ~aElement0(sK98) | ~'Ts83' | ~'Ts83', inference(resolution, [status(thm)], [d2,d0])). % 16.65/8.15 cnf(d4, plain, ~'Ts83' | ~'Ts83', inference(resolution, [status(thm)], [d3,c132])). % 16.65/8.15 cnf(d5, plain, ~sdtmndtplgtdt0(xa,xR,xc) | ~'Ts82', inference(resolution, [status(thm)], [d4,c92])). % 16.65/8.15 cnf(d6, plain, xa = xc | ~'Ts82', inference(resolution, [status(thm)], [c101,d5])). % 16.65/8.15 cnf(d7, plain, xa = xb | 'Ts82', inference(resolution, [status(thm)], [c96,c106])). % 16.65/8.15 cnf(d8, plain, xa = xb | xa = xc, inference(resolution, [status(thm)], [d7,d6])). % 16.65/8.15 cnf(d9, plain, sdtmndtplgtdt0(xc,xR,xb) | xa = xb | xa = xb, inference(superposition, [status(thm)], [d8,c96])). % 16.65/8.15 cnf(d10, plain, xa = xb | 'Ts85'(xb), inference(resolution, [status(thm)], [d9,c158])). % 16.65/8.15 cnf(d11, plain, xa = xb | ~aElement0(xb) | ~'Ts84'(xb), inference(resolution, [status(thm)], [d10,c103])). % 16.65/8.15 cnf(d12, plain, 'Ts84'(xb), inference(equality_resolution, [status(thm)], [c150])). % 16.65/8.15 cnf(d13, plain, xa = xb | ~aElement0(xb), inference(resolution, [status(thm)], [d12,d11])). % 16.65/8.15 cnf(d14, plain, xa = xb, inference(resolution, [status(thm)], [c66,d13])). % 16.65/8.15 cnf(d15, plain, sdtmndtasgtdt0(xb,xR,xc), inference(demodulation, [status(thm)], [c102,d14])). % 16.65/8.15 cnf(d16, plain, 'Ts84'(xc), inference(resolution, [status(thm)], [d15,c154])). % 16.65/8.15 cnf(d17, plain, 'Ts85'(xc), inference(equality_resolution, [status(thm)], [c155])). % 16.65/8.15 cnf(d18, plain, ~aElement0(xc) | ~'Ts84'(xc), inference(resolution, [status(thm)], [c103,d17])). % 16.65/8.15 cnf(d19, plain, ~'Ts84'(xc), inference(resolution, [status(thm)], [c67,d18])). % 16.65/8.15 cnf(d20, plain, $false, inference(resolution, [status(thm)], [d19,d16])). % 16.65/8.15 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------