%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM487+1 : 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 : n018.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:12:54 AM UTC 2026 % Result : Theorem 222.77s 42.41s % Output : CNFRefutation 222.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM487+1 : 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/5.37 % Computer : n018.cluster.edu % 0.11/5.37 % Model : x86_64 x86_64 % 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/5.37 % Memory : 8046.5625MB % 0.11/5.37 % OS : Linux 6.8.0-71-generic % 0.11/5.37 % CPULimit : 300 % 0.11/5.37 % WCLimit : 300 % 0.11/5.37 % DateTime : Sat Sep 26 02:59:12 UTC 2026 % 0.11/5.37 % CPUTime : % 0.11/5.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 222.77/42.41 % SZS status Theorem for theBenchmark.p % 222.77/42.41 % SZS output start CNFRefutation for theBenchmark.p % 222.77/42.41 fof(mSortsC, axiom, aNaturalNumber0(sz00)). % 222.77/42.41 fof(mSortsB, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => aNaturalNumber0(sdtpldt0(X0,X1))))). % 222.77/42.41 fof(mAddComm, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => sdtpldt0(X0,X1) = sdtpldt0(X1,X0)))). % 222.77/42.41 fof(m_AddZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtpldt0(X0,sz00) = X0 & X0 = sdtpldt0(sz00,X0))))). % 222.77/42.41 fof(mAddCanc, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => ((sdtpldt0(X0,X1) = sdtpldt0(X0,X2) | sdtpldt0(X1,X0) = sdtpldt0(X2,X0)) => X1 = X2)))). % 222.77/42.41 fof(mDefLE, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (sdtlseqdt0(X0,X1) <=> ? [X2] : ((aNaturalNumber0(X2) & sdtpldt0(X0,X2) = X1)))))). % 222.77/42.41 fof(mDefDiff, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (sdtlseqdt0(X0,X1) => ! [X2] : ((X2 = sdtmndt0(X1,X0) <=> (aNaturalNumber0(X2) & sdtpldt0(X0,X2) = X1))))))). % 222.77/42.41 fof(mLETran, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X2)) => sdtlseqdt0(X0,X2))))). % 222.77/42.41 fof(mLETotal, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (sdtlseqdt0(X0,X1) | (X1 != X0 & sdtlseqdt0(X1,X0)))))). % 222.77/42.41 fof(mDefPrime, definition, ! [X0] : ((aNaturalNumber0(X0) => (isPrime0(X0) <=> (X0 != sz00 & (X0 != sz10 & ! [X1] : (((aNaturalNumber0(X1) & doDivides0(X1,X0)) => (X1 = sz10 | X1 = X0))))))))). % 222.77/42.41 fof(m__1837, hypothesis, (aNaturalNumber0(xn) & (aNaturalNumber0(xm) & aNaturalNumber0(xp)))). % 222.77/42.41 fof(m__1860, hypothesis, (isPrime0(xp) & doDivides0(xp,sdtasdt0(xn,xm)))). % 222.77/42.41 fof(m__1870, hypothesis, sdtlseqdt0(xp,xn)). % 222.77/42.41 fof(m__1883, hypothesis, xr = sdtmndt0(xn,xp)). % 222.77/42.41 fof(m__, conjecture, (xr != xn & sdtlseqdt0(xr,xn))). % 222.77/42.41 fof(negated_conjecture, negated_conjecture, ~((xr != xn & sdtlseqdt0(xr,xn))), inference(negate_conjecture, [status(cth)], [m__])). % 222.77/42.41 cnf(c0, plain, aNaturalNumber0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 222.77/42.41 cnf(c3, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | aNaturalNumber0(sdtpldt0(X1,X0)), inference(clausification, [status(esa)], [mSortsB])). % 222.77/42.41 cnf(c5, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtpldt0(X0,X1) = sdtpldt0(X1,X0), inference(clausification, [status(esa)], [mAddComm])). % 222.77/42.41 cnf(c8, plain, ~aNaturalNumber0(X0) | sdtpldt0(sz00,X0) = X0, inference(clausification, [status(esa)], [m_AddZero])). % 222.77/42.41 cnf(c18, plain, ~aNaturalNumber0(X0) | X1 = X2 | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2) | sdtpldt0(X1,X0) != sdtpldt0(X2,X0), inference(clausification, [status(esa)], [mAddCanc])). % 222.77/42.41 cnf(c24, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~sdtlseqdt0(X1,X0) | aNaturalNumber0(sK32(X1,X0)), inference(clausification, [status(esa)], [mDefLE])). % 222.77/42.41 cnf(c25, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~sdtlseqdt0(X1,X0) | sdtpldt0(X1,sK32(X1,X0)) = X0, inference(clausification, [status(esa)], [mDefLE])). % 222.77/42.41 cnf(c26, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtpldt0(X1,X2) != X0 | ~aNaturalNumber0(X2) | sdtlseqdt0(X1,X0), inference(clausification, [status(esa)], [mDefLE])). % 222.77/42.41 cnf(c27, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | aNaturalNumber0(X2) | sdtmndt0(X1,X0) != X2 | ~sdtlseqdt0(X0,X1), inference(clausification, [status(esa)], [mDefDiff])). % 222.77/42.41 cnf(c28, plain, sdtpldt0(X0,X1) = X2 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X2) | sdtmndt0(X2,X0) != X1 | ~sdtlseqdt0(X0,X2), inference(clausification, [status(esa)], [mDefDiff])). % 222.77/42.41 cnf(c32, plain, sdtlseqdt0(X0,X1) | ~sdtlseqdt0(X2,X1) | ~sdtlseqdt0(X0,X2) | ~aNaturalNumber0(X2) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(clausification, [status(esa)], [mLETran])). % 222.77/42.41 cnf(c34, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtlseqdt0(X0,X1) | sdtlseqdt0(X1,X0), inference(clausification, [status(esa)], [mLETotal])). % 222.77/42.41 cnf(c58, plain, ~aNaturalNumber0(X0) | X1(X0), inference(clausification, [status(esa)], [mDefPrime])). % 222.77/42.41 cnf(c59, plain, ~X0(X1) | ~isPrime0(X1) | X1 != sz00, inference(clausification, [status(esa)], [mDefPrime])). % 222.77/42.41 cnf(c69, plain, aNaturalNumber0(xn), inference(clausification, [status(esa)], [m__1837])). % 222.77/42.41 cnf(c70, plain, aNaturalNumber0(xp), inference(clausification, [status(esa)], [m__1837])). % 222.77/42.41 cnf(c73, plain, isPrime0(xp), inference(clausification, [status(esa)], [m__1860])). % 222.77/42.41 cnf(c75, plain, sdtlseqdt0(xp,xn), inference(clausification, [status(esa)], [m__1870])). % 222.77/42.41 cnf(c76, plain, sdtmndt0(xn,xp) = xr, inference(clausification, [status(esa)], [m__1883])). % 222.77/42.41 cnf(c77, plain, xr = xn | ~sdtlseqdt0(xr,xn), inference(clausification, [status(esa)], [negated_conjecture])). % 222.77/42.41 cnf(d0, plain, sdtpldt0(sz00,xn) = xn, inference(resolution, [status(thm)], [c8,c69])). % 222.77/42.41 cnf(d1, plain, xn != sdtpldt0(X0,xn) | sz00 = X0 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(xn) | ~aNaturalNumber0(sz00), inference(superposition, [status(thm)], [d0,c18])). % 222.77/42.41 cnf(d2, plain, sz00 = X0 | xn != sdtpldt0(X0,xn) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(xn), inference(resolution, [status(thm)], [c0,d1])). % 222.77/42.41 cnf(d3, plain, sz00 = X0 | xn != sdtpldt0(X0,xn) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c69,d2])). % 222.77/42.41 cnf(d4, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~sdtlseqdt0(X0,X1) | sdtpldt0(sz00,sK32(X0,X1)) = sK32(X0,X1), inference(resolution, [status(thm)], [c24,c8])). % 222.77/42.41 cnf(d5, plain, ~aNaturalNumber0(xr) | ~aNaturalNumber0(xn) | sdtlseqdt0(xn,xr) | xr = xn, inference(resolution, [status(thm)], [c34,c77])). % 222.77/42.41 cnf(d6, plain, xr = xn | ~aNaturalNumber0(xr) | sdtlseqdt0(xn,xr), inference(resolution, [status(thm)], [c69,d5])). % 222.77/42.41 cnf(d7, plain, xr = xn | ~aNaturalNumber0(xr) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(xr) | ~aNaturalNumber0(xn) | sdtlseqdt0(X0,xr) | ~sdtlseqdt0(X0,xn), inference(resolution, [status(thm)], [d6,c32])). % 222.77/42.41 cnf(d8, plain, xr = xn | ~aNaturalNumber0(X0) | ~aNaturalNumber0(xr) | ~sdtlseqdt0(X0,xn) | sdtlseqdt0(X0,xr), inference(resolution, [status(thm)], [c69,d7])). % 222.77/42.41 cnf(d9, plain, xr != X0 | aNaturalNumber0(X0) | ~aNaturalNumber0(xn) | ~aNaturalNumber0(xp) | ~sdtlseqdt0(xp,xn), inference(superposition, [status(thm)], [c76,c27])). % 222.77/42.41 cnf(d10, plain, xr != X0 | aNaturalNumber0(X0) | ~aNaturalNumber0(xp) | ~sdtlseqdt0(xp,xn), inference(resolution, [status(thm)], [c69,d9])). % 222.77/42.41 cnf(d11, plain, xr != X0 | aNaturalNumber0(X0) | ~sdtlseqdt0(xp,xn), inference(resolution, [status(thm)], [c70,d10])). % 222.77/42.41 cnf(d12, plain, xr != X0 | aNaturalNumber0(X0), inference(resolution, [status(thm)], [c75,d11])). % 222.77/42.41 cnf(d13, plain, aNaturalNumber0(xr), inference(equality_resolution, [status(thm)], [d12])). % 222.77/42.41 cnf(d14, plain, xr = xn | ~aNaturalNumber0(X0) | ~sdtlseqdt0(X0,xn) | sdtlseqdt0(X0,xr), inference(resolution, [status(thm)], [d13,d8])). % 222.77/42.41 cnf(d15, plain, xn != X0 | ~aNaturalNumber0(xn) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(X0) | sdtlseqdt0(sz00,X0), inference(superposition, [status(thm)], [d0,c26])). % 222.77/42.41 cnf(d16, plain, xn != X0 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(xn) | sdtlseqdt0(sz00,X0), inference(resolution, [status(thm)], [c0,d15])). % 222.77/42.41 cnf(d17, plain, xn != X0 | ~aNaturalNumber0(X0) | sdtlseqdt0(sz00,X0), inference(resolution, [status(thm)], [c69,d16])). % 222.77/42.41 cnf(d18, plain, ~aNaturalNumber0(xn) | sdtlseqdt0(sz00,xn), inference(equality_resolution, [status(thm)], [d17])). % 222.77/42.41 cnf(d19, plain, sdtlseqdt0(sz00,xn), inference(resolution, [status(thm)], [c69,d18])). % 222.77/42.41 cnf(d20, plain, xr = xn | ~aNaturalNumber0(sz00) | sdtlseqdt0(sz00,xr), inference(resolution, [status(thm)], [d19,d14])). % 222.77/42.41 cnf(d21, plain, xr = xn | sdtlseqdt0(sz00,xr), inference(resolution, [status(thm)], [c0,d20])). % 222.77/42.41 cnf(d22, plain, xr = xn | sdtpldt0(sz00,sK32(sz00,xr)) = sK32(sz00,xr) | ~aNaturalNumber0(xr) | ~aNaturalNumber0(sz00), inference(resolution, [status(thm)], [d21,d4])). % 222.77/42.41 cnf(d23, plain, sdtpldt0(sz00,sK32(sz00,xr)) = sK32(sz00,xr) | xr = xn | ~aNaturalNumber0(xr), inference(resolution, [status(thm)], [c0,d22])). % 222.77/42.41 cnf(d24, plain, sdtpldt0(sz00,sK32(sz00,xr)) = sK32(sz00,xr) | xr = xn, inference(resolution, [status(thm)], [d13,d23])). % 222.77/42.41 cnf(d25, plain, xr = xn | sdtpldt0(sz00,sK32(sz00,xr)) = xr | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xr), inference(resolution, [status(thm)], [d21,c25])). % 222.77/42.41 cnf(d26, plain, sdtpldt0(sz00,sK32(sz00,xr)) = xr | xr = xn | ~aNaturalNumber0(xr), inference(resolution, [status(thm)], [c0,d25])). % 222.77/42.41 cnf(d27, plain, sdtpldt0(sz00,sK32(sz00,xr)) = xr | xr = xn, inference(resolution, [status(thm)], [d13,d26])). % 222.77/42.41 cnf(d28, plain, sK32(sz00,xr) = xr | xr = xn | xr = xn, inference(superposition, [status(thm)], [d24,d27])). % 222.77/42.41 cnf(d29, plain, sdtpldt0(sz00,xr) = sK32(sz00,xr) | xr = xn | xr = xn, inference(superposition, [status(thm)], [d28,d24])). % 222.77/42.41 cnf(d30, plain, sdtpldt0(sz00,sdtpldt0(sz00,xr)) = sK32(sz00,xr) | xr = xn | xr = xn, inference(superposition, [status(thm)], [d29,d24])). % 222.77/42.41 cnf(d31, plain, aNaturalNumber0(sK32(sz00,xr)) | ~aNaturalNumber0(sdtpldt0(sz00,xr)) | ~aNaturalNumber0(sz00) | xr = xn, inference(superposition, [status(thm)], [d30,c3])). % 222.77/42.41 cnf(d32, plain, xr = xn | ~aNaturalNumber0(sdtpldt0(sz00,xr)) | aNaturalNumber0(sK32(sz00,xr)), inference(resolution, [status(thm)], [c0,d31])). % 222.77/42.41 cnf(d33, plain, xr = sK32(sz00,xr) | xr = xn | xr = xn, inference(superposition, [status(thm)], [d27,d24])). % 222.77/42.41 cnf(d34, plain, xr = sdtpldt0(sz00,xr) | xr = xn | xr = xn, inference(superposition, [status(thm)], [d29,d33])). % 222.77/42.41 cnf(d35, plain, ~aNaturalNumber0(xr) | xr = xn | aNaturalNumber0(sK32(sz00,xr)) | xr = xn, inference(superposition, [status(thm)], [d34,d32])). % 222.77/42.41 cnf(d36, plain, xr = xn | aNaturalNumber0(sK32(sz00,xr)), inference(resolution, [status(thm)], [d13,d35])). % 222.77/42.41 cnf(d37, plain, sdtpldt0(xp,X0) = sdtpldt0(X0,xp) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c5,c70])). % 222.77/42.41 cnf(d38, plain, xr = xn | sdtpldt0(xp,sK32(sz00,xr)) = sdtpldt0(sK32(sz00,xr),xp), inference(resolution, [status(thm)], [d36,d37])). % 222.77/42.41 cnf(d39, plain, sdtpldt0(xp,sK32(sz00,xr)) = sdtpldt0(xr,xp) | xr = xn | xr = xn, inference(superposition, [status(thm)], [d33,d38])). % 222.77/42.41 cnf(d40, plain, aNaturalNumber0(sdtpldt0(xr,xp)) | ~aNaturalNumber0(sK32(sz00,xr)) | ~aNaturalNumber0(xp) | xr = xn, inference(superposition, [status(thm)], [d39,c3])). % 222.77/42.41 cnf(d41, plain, xr = xn | aNaturalNumber0(sdtpldt0(xr,xp)) | ~aNaturalNumber0(sK32(sz00,xr)), inference(resolution, [status(thm)], [c70,d40])). % 222.77/42.41 cnf(d42, plain, xr = xn | aNaturalNumber0(sdtpldt0(xr,xp)) | xr = xn, inference(resolution, [status(thm)], [d41,d36])). % 222.77/42.41 cnf(d43, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(sdtpldt0(X1,X0)) | sdtlseqdt0(X1,sdtpldt0(X1,X0)), inference(equality_resolution, [status(thm)], [c26])). % 222.77/42.41 cnf(d44, plain, xr != X0 | sdtpldt0(xp,X0) = xn | ~aNaturalNumber0(xn) | ~aNaturalNumber0(xp) | ~sdtlseqdt0(xp,xn), inference(superposition, [status(thm)], [c76,c28])). % 222.77/42.41 cnf(d45, plain, sdtpldt0(xp,X0) = xn | xr != X0 | ~aNaturalNumber0(xp) | ~sdtlseqdt0(xp,xn), inference(resolution, [status(thm)], [c69,d44])). % 222.77/42.41 cnf(d46, plain, sdtpldt0(xp,X0) = xn | xr != X0 | ~sdtlseqdt0(xp,xn), inference(resolution, [status(thm)], [c70,d45])). % 222.77/42.41 cnf(d47, plain, sdtpldt0(xp,X0) = xn | xr != X0, inference(resolution, [status(thm)], [c75,d46])). % 222.77/42.41 cnf(d48, plain, sdtpldt0(xp,xr) = xn, inference(equality_resolution, [status(thm)], [d47])). % 222.77/42.41 cnf(d49, plain, sdtpldt0(xp,xr) = sdtpldt0(xr,xp) | xr = xn | xr = xn, inference(superposition, [status(thm)], [d33,d39])). % 222.77/42.41 cnf(d50, plain, xn = sdtpldt0(xr,xp) | xr = xn, inference(demodulation, [status(thm)], [d49,d48])). % 222.77/42.41 cnf(d51, plain, sdtlseqdt0(xr,xn) | ~aNaturalNumber0(xr) | ~aNaturalNumber0(xp) | ~aNaturalNumber0(sdtpldt0(xr,xp)) | xr = xn, inference(superposition, [status(thm)], [d50,d43])). % 222.77/42.41 cnf(d52, plain, xr = xn | ~aNaturalNumber0(sdtpldt0(xr,xp)) | ~aNaturalNumber0(xr) | sdtlseqdt0(xr,xn), inference(resolution, [status(thm)], [c70,d51])). % 222.77/42.41 cnf(d53, plain, xr = xn | ~aNaturalNumber0(sdtpldt0(xr,xp)) | sdtlseqdt0(xr,xn), inference(resolution, [status(thm)], [d13,d52])). % 222.77/42.41 cnf(d54, plain, xr = xn | sdtlseqdt0(xr,xn) | xr = xn, inference(resolution, [status(thm)], [d53,d42])). % 222.77/42.41 cnf(d55, plain, xr = xn | xr = xn, inference(resolution, [status(thm)], [d54,c77])). % 222.77/42.41 cnf(d56, plain, sdtpldt0(xp,xn) = xn, inference(demodulation, [status(thm)], [d48,d55])). % 222.77/42.41 cnf(d57, plain, xn != xn | sz00 = xp | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [d56,d3])). % 222.77/42.41 cnf(d58, plain, sz00 = xp | xn != xn, inference(resolution, [status(thm)], [c70,d57])). % 222.77/42.41 cnf(d59, plain, sdtpldt0(X0,sdtmndt0(X1,X0)) = X1 | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~sdtlseqdt0(X0,X1), inference(equality_resolution, [status(thm)], [c28])). % 222.77/42.41 cnf(d60, plain, sdtpldt0(xp,sdtmndt0(xn,xp)) = xn | ~aNaturalNumber0(xn) | ~aNaturalNumber0(xp), inference(resolution, [status(thm)], [d59,c75])). % 222.77/42.41 cnf(d61, plain, sdtpldt0(xp,xr) = xn | ~aNaturalNumber0(xn) | ~aNaturalNumber0(xp), inference(demodulation, [status(thm)], [d60,c76])). % 222.77/42.41 cnf(d62, plain, xn = xn | ~aNaturalNumber0(xn) | ~aNaturalNumber0(xp), inference(demodulation, [status(thm)], [d61,d48])). % 222.77/42.41 cnf(d63, plain, xn = xn | ~aNaturalNumber0(xp), inference(resolution, [status(thm)], [c69,d62])). % 222.77/42.41 cnf(d64, plain, xn = xn, inference(resolution, [status(thm)], [c70,d63])). % 222.77/42.41 cnf(d65, plain, sz00 = xp, inference(resolution, [status(thm)], [d64,d58])). % 222.77/42.41 cnf(d66, plain, isPrime0(sz00), inference(demodulation, [status(thm)], [c73,d65])). % 222.77/42.41 cnf(d67, plain, ~'Ts77'(sz00) | ~isPrime0(sz00), inference(equality_resolution, [status(thm)], [c59])). % 222.77/42.41 cnf(d68, plain, 'Ts77'(sz00), inference(resolution, [status(thm)], [c58,c0])). % 222.77/42.41 cnf(d69, plain, ~isPrime0(sz00), inference(resolution, [status(thm)], [d68,d67])). % 222.77/42.41 cnf(d70, plain, $false, inference(resolution, [status(thm)], [d69,d66])). % 222.77/42.41 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------