%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : RNG111+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 : n003.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 13.69s 2.60s % Output : CNFRefutation 13.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : RNG111+4 : 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.58 % Computer : n003.cluster.edu % 0.11/0.58 % Model : x86_64 x86_64 % 0.11/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.58 % Memory : 8046.5625MB % 0.11/0.58 % OS : Linux 6.8.0-71-generic % 0.11/0.58 % CPULimit : 300 % 0.11/0.58 % WCLimit : 300 % 0.11/0.58 % DateTime : Sat Sep 26 06:09:54 UTC 2026 % 0.11/0.59 % CPUTime : % 0.11/0.59 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 13.69/2.60 % SZS status Theorem for theBenchmark.p % 13.69/2.60 % SZS output start CNFRefutation for theBenchmark.p % 13.69/2.60 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)) => ? [X2] : ((? [X3] : ? [X4] : ((aElementOf0(X3,slsdtgt0(xa)) & (aElementOf0(X4,slsdtgt0(xb)) & sdtpldt0(X3,X4) = X2))) & (aElementOf0(X2,xI) & (X2 != sz00 & ! [X3] : ((((? [X4] : ? [X5] : ((aElementOf0(X4,slsdtgt0(xa)) & (aElementOf0(X5,slsdtgt0(xb)) & sdtpldt0(X4,X5) = X3))) | aElementOf0(X3,xI)) & X3 != sz00) => ~iLess0(sbrdtbr0(X3),sbrdtbr0(X2))))))))))) => ? [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))))))))))). % 13.69/2.60 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)) => ? [X2] : ((? [X3] : ? [X4] : ((aElementOf0(X3,slsdtgt0(xa)) & (aElementOf0(X4,slsdtgt0(xb)) & sdtpldt0(X3,X4) = X2))) & (aElementOf0(X2,xI) & (X2 != sz00 & ! [X3] : ((((? [X4] : ? [X5] : ((aElementOf0(X4,slsdtgt0(xa)) & (aElementOf0(X5,slsdtgt0(xb)) & sdtpldt0(X4,X5) = X3))) | aElementOf0(X3,xI)) & X3 != sz00) => ~iLess0(sbrdtbr0(X3),sbrdtbr0(X2))))))))))) => ? [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)))))))))), inference(negate_conjecture, [status(cth)], [m__])). % 13.69/2.60 cnf(c172, plain, aElementOf0(sK144,xI), inference(clausification, [status(esa)], [negated_conjecture])). % 13.69/2.60 cnf(c173, plain, sK144 != sz00, inference(clausification, [status(esa)], [negated_conjecture])). % 13.69/2.60 cnf(c175, plain, ~aElementOf0(X0,xI) | X0 = sz00 | ~iLess0(sbrdtbr0(X0),sbrdtbr0(sK144)) | X1, inference(clausification, [status(esa)], [negated_conjecture])). % 13.69/2.60 cnf(c177, plain, ~aElementOf0(X0,xI) | X0 = sz00 | ~X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 13.69/2.60 cnf(c181, plain, ~X0 | aElementOf0(sK153,xI), inference(clausification, [status(esa)], [negated_conjecture])). % 13.69/2.60 cnf(c182, plain, ~X0 | sK153 != sz00, inference(clausification, [status(esa)], [negated_conjecture])). % 13.69/2.60 cnf(c184, plain, ~X0 | ~aElementOf0(X1,xI) | X1 = sz00 | ~iLess0(sbrdtbr0(X1),sbrdtbr0(sK153)), inference(clausification, [status(esa)], [negated_conjecture])). % 13.69/2.60 cnf(c188, plain, X0(X1) | aElementOf0(sK159(X1),xI), inference(clausification, [status(esa)], [negated_conjecture])). % 13.69/2.60 cnf(c189, plain, X0(X1) | sK159(X1) != sz00, inference(clausification, [status(esa)], [negated_conjecture])). % 13.69/2.60 cnf(c190, plain, X0(X1) | iLess0(sbrdtbr0(sK159(X1)),sbrdtbr0(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 13.69/2.60 cnf(d0, plain, sK159(sK144) = sz00 | ~aElementOf0(sK159(sK144),xI) | 'Ts142' | 'Ts143'(sK144), inference(resolution, [status(thm)], [c175,c190])). % 13.69/2.60 cnf(d1, plain, sK144 = sz00 | ~'Ts143'(sK144), inference(resolution, [status(thm)], [c177,c172])). % 13.69/2.60 cnf(d2, plain, ~'Ts143'(sK144), inference(resolution, [status(thm)], [c173,d1])). % 13.69/2.60 cnf(d3, plain, sK159(sK144) = sz00 | ~aElementOf0(sK159(sK144),xI) | 'Ts142', inference(resolution, [status(thm)], [d2,d0])). % 13.69/2.60 cnf(d4, plain, sK159(sK144) = sz00 | 'Ts142' | 'Ts143'(sK144), inference(resolution, [status(thm)], [d3,c188])). % 13.69/2.60 cnf(d5, plain, sK159(sK144) = sz00 | 'Ts142', inference(resolution, [status(thm)], [d2,d4])). % 13.69/2.60 cnf(d6, plain, sK153 = sz00 | ~'Ts143'(sK153) | ~'Ts142', inference(resolution, [status(thm)], [c177,c181])). % 13.69/2.60 cnf(d7, plain, sK159(sK153) = sz00 | ~aElementOf0(sK159(sK153),xI) | ~'Ts142' | 'Ts143'(sK153), inference(resolution, [status(thm)], [c184,c190])). % 13.69/2.60 cnf(d8, plain, sK159(sK153) = sz00 | ~'Ts142' | 'Ts143'(sK153) | 'Ts143'(sK153), inference(resolution, [status(thm)], [d7,c188])). % 13.69/2.60 cnf(d9, plain, sK159(sK153) = sz00 | ~'Ts142' | sK153 = sz00 | ~'Ts142', inference(resolution, [status(thm)], [d8,d6])). % 13.69/2.60 cnf(d10, plain, sK153 = sz00 | sK159(sK153) = sz00 | sK159(sK144) = sz00, inference(resolution, [status(thm)], [d9,d5])). % 13.69/2.60 cnf(d11, plain, sz00 != sz00 | 'Ts143'(sK153) | sK153 = sz00 | sK159(sK144) = sz00, inference(superposition, [status(thm)], [d10,c189])). % 13.69/2.60 cnf(d12, plain, sK153 = sz00 | sK159(sK144) = sz00 | 'Ts143'(sK153), inference(equality_resolution, [status(thm)], [d11])). % 13.69/2.60 cnf(d13, plain, sK153 = sz00 | sK159(sK144) = sz00 | sK153 = sz00 | ~'Ts142', inference(resolution, [status(thm)], [d12,d6])). % 13.69/2.60 cnf(d14, plain, sK153 = sz00 | sK159(sK144) = sz00 | sK159(sK144) = sz00, inference(resolution, [status(thm)], [d13,d5])). % 13.69/2.60 cnf(d15, plain, sz00 != sz00 | 'Ts143'(sK144) | sK153 = sz00, inference(superposition, [status(thm)], [d14,c189])). % 13.69/2.60 cnf(d16, plain, sz00 != sz00 | sK153 = sz00, inference(resolution, [status(thm)], [d2,d15])). % 13.69/2.60 cnf(d17, plain, sK153 = sz00, inference(equality_resolution, [status(thm)], [d16])). % 13.69/2.60 cnf(d18, plain, ~'Ts142', inference(resolution, [status(thm)], [d17,c182])). % 13.69/2.60 cnf(d19, plain, sK159(sK144) = sz00, inference(resolution, [status(thm)], [d18,d5])). % 13.69/2.60 cnf(d20, plain, sz00 != sz00 | 'Ts143'(sK144), inference(superposition, [status(thm)], [d19,c189])). % 13.69/2.60 cnf(d21, plain, sz00 != sz00, inference(resolution, [status(thm)], [d2,d20])). % 13.69/2.60 cnf(d22, plain, $false, inference(equality_resolution, [status(thm)], [d21])). % 13.69/2.60 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------