%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : RNG092+2 : 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 : n010.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:25:51 AM UTC 2026 % Result : Theorem 16.14s 3.63s % Output : CNFRefutation 16.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : RNG092+2 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.11/0.36 % Computer : n010.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Sat Sep 26 06:03:14 UTC 2026 % 0.11/0.37 % CPUTime : % 0.11/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 16.14/3.63 % SZS status Theorem for theBenchmark.p % 16.14/3.63 % SZS output start CNFRefutation for theBenchmark.p % 16.14/3.63 fof(mSortsC, axiom, aElement0(sz00)). % 16.14/3.63 fof(m__, conjecture, (! [X0] : ! [X1] : ! [X2] : ((((? [X3] : ? [X4] : ((aElementOf0(X3,xI) & (aElementOf0(X4,xJ) & sdtpldt0(X3,X4) = X0))) | aElementOf0(X0,sdtpldt1(xI,xJ))) & ((? [X3] : ? [X4] : ((aElementOf0(X3,xI) & (aElementOf0(X4,xJ) & sdtpldt0(X3,X4) = X1))) | aElementOf0(X1,sdtpldt1(xI,xJ))) & aElement0(X2))) => ? [X3] : ? [X4] : ((aElementOf0(X3,xI) & (aElementOf0(X4,xJ) & (X0 = sdtpldt0(X3,X4) & ? [X5] : ? [X6] : ((aElementOf0(X5,xI) & (aElementOf0(X6,xJ) & (X1 = sdtpldt0(X5,X6) & (aElementOf0(sdtpldt0(X3,X5),xI) & (aElementOf0(sdtpldt0(X4,X6),xJ) & (aElementOf0(sdtasdt0(X2,X3),xI) & (aElementOf0(sdtasdt0(X2,X4),xJ) & (sdtpldt0(X0,X1) = sdtpldt0(sdtpldt0(X3,X5),sdtpldt0(X4,X6)) & (? [X7] : ? [X8] : ((aElementOf0(X7,xI) & (aElementOf0(X8,xJ) & sdtpldt0(X7,X8) = sdtpldt0(X0,X1)))) & (aElementOf0(sdtpldt0(X0,X1),sdtpldt1(xI,xJ)) & (? [X7] : ? [X8] : ((aElementOf0(X7,xI) & (aElementOf0(X8,xJ) & sdtpldt0(X7,X8) = sdtasdt0(X2,X0)))) & aElementOf0(sdtasdt0(X2,X0),sdtpldt1(xI,xJ)))))))))))))))))))) => ((aSet0(sdtpldt1(xI,xJ)) & ! [X0] : ((aElementOf0(X0,sdtpldt1(xI,xJ)) <=> ? [X1] : ? [X2] : ((aElementOf0(X1,xI) & (aElementOf0(X2,xJ) & sdtpldt0(X1,X2) = X0)))))) => (! [X0] : ((aElementOf0(X0,sdtpldt1(xI,xJ)) => (! [X1] : ((aElementOf0(X1,sdtpldt1(xI,xJ)) => aElementOf0(sdtpldt0(X0,X1),sdtpldt1(xI,xJ)))) & ! [X1] : ((aElement0(X1) => aElementOf0(sdtasdt0(X1,X0),sdtpldt1(xI,xJ))))))) | aIdeal0(sdtpldt1(xI,xJ)))))). % 16.14/3.63 fof(negated_conjecture, negated_conjecture, ~((! [X0] : ! [X1] : ! [X2] : ((((? [X3] : ? [X4] : ((aElementOf0(X3,xI) & (aElementOf0(X4,xJ) & sdtpldt0(X3,X4) = X0))) | aElementOf0(X0,sdtpldt1(xI,xJ))) & ((? [X3] : ? [X4] : ((aElementOf0(X3,xI) & (aElementOf0(X4,xJ) & sdtpldt0(X3,X4) = X1))) | aElementOf0(X1,sdtpldt1(xI,xJ))) & aElement0(X2))) => ? [X3] : ? [X4] : ((aElementOf0(X3,xI) & (aElementOf0(X4,xJ) & (X0 = sdtpldt0(X3,X4) & ? [X5] : ? [X6] : ((aElementOf0(X5,xI) & (aElementOf0(X6,xJ) & (X1 = sdtpldt0(X5,X6) & (aElementOf0(sdtpldt0(X3,X5),xI) & (aElementOf0(sdtpldt0(X4,X6),xJ) & (aElementOf0(sdtasdt0(X2,X3),xI) & (aElementOf0(sdtasdt0(X2,X4),xJ) & (sdtpldt0(X0,X1) = sdtpldt0(sdtpldt0(X3,X5),sdtpldt0(X4,X6)) & (? [X7] : ? [X8] : ((aElementOf0(X7,xI) & (aElementOf0(X8,xJ) & sdtpldt0(X7,X8) = sdtpldt0(X0,X1)))) & (aElementOf0(sdtpldt0(X0,X1),sdtpldt1(xI,xJ)) & (? [X7] : ? [X8] : ((aElementOf0(X7,xI) & (aElementOf0(X8,xJ) & sdtpldt0(X7,X8) = sdtasdt0(X2,X0)))) & aElementOf0(sdtasdt0(X2,X0),sdtpldt1(xI,xJ)))))))))))))))))))) => ((aSet0(sdtpldt1(xI,xJ)) & ! [X0] : ((aElementOf0(X0,sdtpldt1(xI,xJ)) <=> ? [X1] : ? [X2] : ((aElementOf0(X1,xI) & (aElementOf0(X2,xJ) & sdtpldt0(X1,X2) = X0)))))) => (! [X0] : ((aElementOf0(X0,sdtpldt1(xI,xJ)) => (! [X1] : ((aElementOf0(X1,sdtpldt1(xI,xJ)) => aElementOf0(sdtpldt0(X0,X1),sdtpldt1(xI,xJ)))) & ! [X1] : ((aElement0(X1) => aElementOf0(sdtasdt0(X1,X0),sdtpldt1(xI,xJ))))))) | aIdeal0(sdtpldt1(xI,xJ)))))), inference(negate_conjecture, [status(cth)], [m__])). % 16.14/3.63 cnf(c0, plain, aElement0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 16.14/3.63 cnf(c76, plain, ~aElementOf0(X0,sdtpldt1(xI,xJ)) | ~aElementOf0(X1,sdtpldt1(xI,xJ)) | ~aElement0(X2) | X3(X0,X1,X2), inference(clausification, [status(esa)], [negated_conjecture])). % 16.14/3.63 cnf(c82, plain, aElementOf0(sK80,sdtpldt1(xI,xJ)), inference(clausification, [status(esa)], [negated_conjecture])). % 16.14/3.63 cnf(c83, plain, aElementOf0(sK81,sdtpldt1(xI,xJ)) | aElement0(sK82), inference(clausification, [status(esa)], [negated_conjecture])). % 16.14/3.63 cnf(c84, plain, aElementOf0(sK81,sdtpldt1(xI,xJ)) | ~aElementOf0(sdtasdt0(sK82,sK80),sdtpldt1(xI,xJ)), inference(clausification, [status(esa)], [negated_conjecture])). % 16.14/3.63 cnf(c85, plain, ~aElementOf0(sdtpldt0(sK80,sK81),sdtpldt1(xI,xJ)) | aElement0(sK82), inference(clausification, [status(esa)], [negated_conjecture])). % 16.14/3.63 cnf(c86, plain, ~aElementOf0(sdtpldt0(sK80,sK81),sdtpldt1(xI,xJ)) | ~aElementOf0(sdtasdt0(sK82,sK80),sdtpldt1(xI,xJ)), inference(clausification, [status(esa)], [negated_conjecture])). % 16.14/3.63 cnf(c102, plain, ~X0(X1,X2,X3) | aElementOf0(sdtpldt0(X1,X2),sdtpldt1(xI,xJ)), inference(clausification, [status(esa)], [negated_conjecture])). % 16.14/3.63 cnf(c106, plain, ~X0(X1,X2,X3) | aElementOf0(sdtasdt0(X3,X1),sdtpldt1(xI,xJ)), inference(clausification, [status(esa)], [negated_conjecture])). % 16.14/3.63 cnf(d0, plain, ~aElement0(X0) | ~aElementOf0(X1,sdtpldt1(xI,xJ)) | 'Ts67'(sK80,X1,X0), inference(resolution, [status(thm)], [c76,c82])). % 16.14/3.63 cnf(d1, plain, ~aElement0(X0) | 'Ts67'(sK80,sK80,X0), inference(resolution, [status(thm)], [d0,c82])). % 16.14/3.63 cnf(d2, plain, ~aElementOf0(sdtpldt0(sK80,sK81),sdtpldt1(xI,xJ)) | ~'Ts67'(sK80,X0,sK82), inference(resolution, [status(thm)], [c86,c106])). % 16.14/3.63 cnf(d3, plain, ~'Ts67'(sK80,X0,sK82) | ~'Ts67'(sK80,sK81,X1), inference(resolution, [status(thm)], [d2,c102])). % 16.14/3.63 cnf(d4, plain, aElementOf0(sK81,sdtpldt1(xI,xJ)) | ~'Ts67'(sK80,X0,sK82), inference(resolution, [status(thm)], [c84,c106])). % 16.14/3.63 cnf(d5, plain, ~aElement0(X0) | 'Ts67'(sK80,sK81,X0) | ~'Ts67'(sK80,X1,sK82), inference(resolution, [status(thm)], [d0,d4])). % 16.14/3.63 cnf(d6, plain, ~aElement0(X0) | 'Ts67'(sK80,sK81,X0) | ~aElement0(sK82), inference(resolution, [status(thm)], [d5,d1])). % 16.14/3.63 cnf(d7, plain, ~'Ts67'(sK80,sK81,X0) | aElement0(sK82), inference(resolution, [status(thm)], [c102,c85])). % 16.14/3.63 cnf(d8, plain, ~aElement0(X0) | 'Ts67'(sK80,sK81,X0) | aElement0(sK82), inference(resolution, [status(thm)], [d0,c83])). % 16.14/3.63 cnf(d9, plain, ~aElement0(X0) | aElement0(sK82) | aElement0(sK82), inference(resolution, [status(thm)], [d8,d7])). % 16.14/3.63 cnf(d10, plain, aElement0(sK82), inference(resolution, [status(thm)], [d9,c0])). % 16.14/3.63 cnf(d11, plain, ~aElement0(X0) | 'Ts67'(sK80,sK81,X0), inference(resolution, [status(thm)], [d10,d6])). % 16.14/3.63 cnf(d12, plain, ~aElement0(X0) | ~'Ts67'(sK80,X1,sK82), inference(resolution, [status(thm)], [d11,d3])). % 16.14/3.63 cnf(d13, plain, ~aElement0(X0) | ~aElement0(sK82), inference(resolution, [status(thm)], [d12,d1])). % 16.14/3.63 cnf(d14, plain, ~aElement0(X0), inference(resolution, [status(thm)], [d10,d13])). % 16.14/3.63 cnf(d15, plain, $false, inference(resolution, [status(thm)], [d14,c0])). % 16.14/3.63 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------