%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : RNG112+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 : n026.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:55 AM UTC 2026 % Result : Theorem 40.78s 5.59s % Output : CNFRefutation 40.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : RNG112+4 : 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.06/0.34 % Computer : n026.cluster.edu % 0.06/0.34 % Model : x86_64 x86_64 % 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.34 % Memory : 8046.5625MB % 0.06/0.34 % OS : Linux 6.8.0-71-generic % 0.06/0.34 % CPULimit : 300 % 0.06/0.34 % WCLimit : 300 % 0.06/0.34 % DateTime : Sat Sep 26 06:11:09 UTC 2026 % 0.06/0.34 % CPUTime : % 0.06/0.34 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 40.78/5.59 % SZS status Theorem for theBenchmark.p % 40.78/5.59 % SZS output start CNFRefutation for theBenchmark.p % 40.78/5.59 fof(m__2174, hypothesis, (aSet0(xI) & (! [X0] : ((aElementOf0(X0,xI) => (! [X1] : ((aElementOf0(X1,xI) => aElementOf0(sdtpldt0(X0,X1),xI))) & ! [X1] : ((aElement0(X1) => aElementOf0(sdtasdt0(X1,X0),xI)))))) & (aIdeal0(xI) & (! [X0] : ((aElementOf0(X0,slsdtgt0(xa)) <=> ? [X1] : ((aElement0(X1) & sdtasdt0(xa,X1) = X0)))) & (! [X0] : ((aElementOf0(X0,slsdtgt0(xb)) <=> ? [X1] : ((aElement0(X1) & sdtasdt0(xb,X1) = X0)))) & (! [X0] : ((aElementOf0(X0,xI) <=> ? [X1] : ? [X2] : ((aElementOf0(X1,slsdtgt0(xa)) & (aElementOf0(X2,slsdtgt0(xb)) & sdtpldt0(X1,X2) = X0))))) & xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))))))))). % 40.78/5.59 fof(m__2228, hypothesis, ? [X0] : ((! [X1] : ((aElementOf0(X1,slsdtgt0(xa)) <=> ? [X2] : ((aElement0(X2) & sdtasdt0(xa,X2) = X1)))) & (! [X1] : ((aElementOf0(X1,slsdtgt0(xb)) <=> ? [X2] : ((aElement0(X2) & sdtasdt0(xb,X2) = X1)))) & (? [X1] : ? [X2] : ((aElementOf0(X1,slsdtgt0(xa)) & (aElementOf0(X2,slsdtgt0(xb)) & sdtpldt0(X1,X2) = X0))) & (aElementOf0(X0,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))) & X0 != sz00)))))). % 40.78/5.59 fof(m__2351, hypothesis, ! [X0] : ((((? [X1] : ? [X2] : ((aElementOf0(X1,slsdtgt0(xa)) & (aElementOf0(X2,slsdtgt0(xb)) & sdtpldt0(X1,X2) = X0))) | aElementOf0(X0,xI)) & X0 != sz00) => ? [X1] : ((? [X2] : ? [X3] : ((aElementOf0(X2,slsdtgt0(xa)) & (aElementOf0(X3,slsdtgt0(xb)) & sdtpldt0(X2,X3) = X1))) & (aElementOf0(X1,xI) & (X1 != sz00 & ! [X2] : ((((? [X3] : ? [X4] : ((aElementOf0(X3,slsdtgt0(xa)) & (aElementOf0(X4,slsdtgt0(xb)) & sdtpldt0(X3,X4) = X2))) | aElementOf0(X2,xI)) & X2 != sz00) => ~iLess0(sbrdtbr0(X2),sbrdtbr0(X1))))))))))). % 40.78/5.59 fof(m__, conjecture, ? [X0] : (((? [X1] : ? [X2] : ((aElementOf0(X1,slsdtgt0(xa)) & (aElementOf0(X2,slsdtgt0(xb)) & sdtpldt0(X1,X2) = X0))) | aElementOf0(X0,xI)) & (X0 != sz00 & ! [X1] : (((? [X2] : ? [X3] : ((aElementOf0(X2,slsdtgt0(xa)) & (aElementOf0(X3,slsdtgt0(xb)) & sdtpldt0(X2,X3) = X1))) & (aElementOf0(X1,xI) & X1 != sz00)) => ~iLess0(sbrdtbr0(X1),sbrdtbr0(X0)))))))). % 40.78/5.59 fof(negated_conjecture, negated_conjecture, ~? [X0] : (((? [X1] : ? [X2] : ((aElementOf0(X1,slsdtgt0(xa)) & (aElementOf0(X2,slsdtgt0(xb)) & sdtpldt0(X1,X2) = X0))) | aElementOf0(X0,xI)) & (X0 != sz00 & ! [X1] : (((? [X2] : ? [X3] : ((aElementOf0(X2,slsdtgt0(xa)) & (aElementOf0(X3,slsdtgt0(xb)) & sdtpldt0(X2,X3) = X1))) & (aElementOf0(X1,xI) & X1 != sz00)) => ~iLess0(sbrdtbr0(X1),sbrdtbr0(X0))))))), inference(negate_conjecture, [status(cth)], [m__])). % 40.78/5.59 cnf(c145, plain, xI = sdtpldt1(slsdtgt0(xa),slsdtgt0(xb)), inference(clausification, [status(esa)], [m__2174])). % 40.78/5.59 cnf(c167, plain, aElementOf0(sK133,sdtpldt1(slsdtgt0(xa),slsdtgt0(xb))), inference(clausification, [status(esa)], [m__2228])). % 40.78/5.59 cnf(c168, plain, sK133 != sz00, inference(clausification, [status(esa)], [m__2228])). % 40.78/5.59 cnf(c170, plain, ~aElementOf0(X0,xI) | X0 = sz00 | X1, inference(clausification, [status(esa)], [m__2351])). % 40.78/5.59 cnf(c174, plain, ~X0 | aElementOf0(sK146,xI), inference(clausification, [status(esa)], [m__2351])). % 40.78/5.59 cnf(c175, plain, ~X0 | sK146 != sz00, inference(clausification, [status(esa)], [m__2351])). % 40.78/5.59 cnf(c177, plain, ~X0 | ~aElementOf0(X1,xI) | X1 = sz00 | ~iLess0(sbrdtbr0(X1),sbrdtbr0(sK146)), inference(clausification, [status(esa)], [m__2351])). % 40.78/5.59 cnf(c179, plain, ~aElementOf0(X0,xI) | X0 = sz00 | ~X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 40.78/5.59 cnf(c183, plain, X0(X1) | aElementOf0(sK156(X1),xI), inference(clausification, [status(esa)], [negated_conjecture])). % 40.78/5.59 cnf(c184, plain, X0(X1) | sK156(X1) != sz00, inference(clausification, [status(esa)], [negated_conjecture])). % 40.78/5.59 cnf(c185, plain, X0(X1) | iLess0(sbrdtbr0(sK156(X1)),sbrdtbr0(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 40.78/5.59 cnf(d0, plain, aElementOf0(sK133,xI), inference(demodulation, [status(thm)], [c167,c145])). % 40.78/5.59 cnf(d1, plain, sK133 = sz00 | ~'Ts152'(sK133), inference(resolution, [status(thm)], [d0,c179])). % 40.78/5.59 cnf(d2, plain, ~'Ts152'(sK133), inference(resolution, [status(thm)], [c168,d1])). % 40.78/5.59 cnf(d3, plain, sK156(X0) = sz00 | 'Ts142' | 'Ts152'(X0), inference(resolution, [status(thm)], [c170,c183])). % 40.78/5.59 cnf(d4, plain, sz00 != sz00 | 'Ts152'(X0) | 'Ts142' | 'Ts152'(X0), inference(superposition, [status(thm)], [d3,c184])). % 40.78/5.59 cnf(d5, plain, 'Ts142' | 'Ts152'(X0), inference(equality_resolution, [status(thm)], [d4])). % 40.78/5.59 cnf(d6, plain, 'Ts142', inference(resolution, [status(thm)], [d5,d2])). % 40.78/5.59 cnf(d7, plain, X0 = sz00 | ~aElementOf0(X0,xI) | ~iLess0(sbrdtbr0(X0),sbrdtbr0(sK146)), inference(resolution, [status(thm)], [d6,c177])). % 40.78/5.59 cnf(d8, plain, sK156(sK146) = sz00 | ~aElementOf0(sK156(sK146),xI) | 'Ts152'(sK146), inference(resolution, [status(thm)], [d7,c185])). % 40.78/5.59 cnf(d9, plain, ~'Ts142' | sK146 = sz00 | ~'Ts152'(sK146), inference(resolution, [status(thm)], [c174,c179])). % 40.78/5.59 cnf(d10, plain, sz00 != sz00 | ~'Ts142' | ~'Ts142' | ~'Ts152'(sK146), inference(superposition, [status(thm)], [d9,c175])). % 40.78/5.59 cnf(d11, plain, ~'Ts142' | ~'Ts152'(sK146), inference(equality_resolution, [status(thm)], [d10])). % 40.78/5.59 cnf(d12, plain, ~'Ts152'(sK146), inference(resolution, [status(thm)], [d6,d11])). % 40.78/5.59 cnf(d13, plain, sK156(sK146) = sz00 | ~aElementOf0(sK156(sK146),xI), inference(resolution, [status(thm)], [d12,d8])). % 40.78/5.59 cnf(d14, plain, sK156(sK146) = sz00 | 'Ts152'(sK146), inference(resolution, [status(thm)], [d13,c183])). % 40.78/5.59 cnf(d15, plain, sK156(sK146) = sz00, inference(resolution, [status(thm)], [d12,d14])). % 40.78/5.59 cnf(d16, plain, sz00 != sz00 | 'Ts152'(sK146), inference(superposition, [status(thm)], [d15,c184])). % 40.78/5.59 cnf(d17, plain, sz00 != sz00, inference(resolution, [status(thm)], [d12,d16])). % 40.78/5.59 cnf(d18, plain, $false, inference(equality_resolution, [status(thm)], [d17])). % 40.78/5.59 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------