%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM483+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 : n007.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:53 AM UTC 2026 % Result : Theorem 186.58s 27.39s % Output : CNFRefutation 186.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM483+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.09/0.36 % Computer : n007.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 26 02:53:53 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 186.58/27.39 % SZS status Theorem for theBenchmark.p % 186.58/27.39 % SZS output start CNFRefutation for theBenchmark.p % 186.58/27.39 fof(mSortsC, axiom, aNaturalNumber0(sz00)). % 186.58/27.39 fof(mSortsC_01, axiom, (aNaturalNumber0(sz10) & sz10 != sz00)). % 186.58/27.39 fof(mSortsB, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => aNaturalNumber0(sdtpldt0(X0,X1))))). % 186.58/27.39 fof(mAddComm, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => sdtpldt0(X0,X1) = sdtpldt0(X1,X0)))). % 186.58/27.39 fof(m_AddZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtpldt0(X0,sz00) = X0 & X0 = sdtpldt0(sz00,X0))))). % 186.58/27.39 fof(m_MulUnit, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz10) = X0 & X0 = sdtasdt0(sz10,X0))))). % 186.58/27.39 fof(m_MulZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 186.58/27.39 fof(mDefLE, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (sdtlseqdt0(X0,X1) <=> ? [X2] : ((aNaturalNumber0(X2) & sdtpldt0(X0,X2) = X1)))))). % 186.58/27.39 fof(mDefDiff, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (sdtlseqdt0(X0,X1) => ! [X2] : ((X2 = sdtmndt0(X1,X0) <=> (aNaturalNumber0(X2) & sdtpldt0(X0,X2) = X1))))))). % 186.58/27.39 fof(mLEAsym, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X0)) => X0 = X1)))). % 186.58/27.39 fof(mLETotal, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (sdtlseqdt0(X0,X1) | (X1 != X0 & sdtlseqdt0(X1,X0)))))). % 186.58/27.39 fof(mIH_03, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((X0 != X1 & sdtlseqdt0(X0,X1)) => iLess0(X0,X1))))). % 186.58/27.39 fof(mDefDiv, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (doDivides0(X0,X1) <=> ? [X2] : ((aNaturalNumber0(X2) & X1 = sdtasdt0(X0,X2))))))). % 186.58/27.39 fof(mDivTrans, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => ((doDivides0(X0,X1) & doDivides0(X1,X2)) => doDivides0(X0,X2))))). % 186.58/27.39 fof(mDivMin, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => ((doDivides0(X0,X1) & doDivides0(X0,sdtpldt0(X1,X2))) => doDivides0(X0,X2))))). % 186.58/27.39 fof(mDivLE, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((doDivides0(X0,X1) & X1 != sz00) => sdtlseqdt0(X0,X1))))). % 186.58/27.39 fof(mDefPrime, definition, ! [X0] : ((aNaturalNumber0(X0) => (isPrime0(X0) <=> (X0 != sz00 & (X0 != sz10 & ! [X1] : (((aNaturalNumber0(X1) & doDivides0(X1,X0)) => (X1 = sz10 | X1 = X0))))))))). % 186.58/27.39 fof(m__1716, hypothesis, aNaturalNumber0(xk)). % 186.58/27.39 fof(m__1700, hypothesis, ! [X0] : (((aNaturalNumber0(X0) & (X0 != sz00 & X0 != sz10)) => (iLess0(X0,xk) => ? [X1] : ((aNaturalNumber0(X1) & (doDivides0(X1,X0) & isPrime0(X1)))))))). % 186.58/27.39 fof(m__1716_04, hypothesis, (xk != sz00 & xk != sz10)). % 186.58/27.39 fof(m__1725, hypothesis, ~isPrime0(xk)). % 186.58/27.39 fof(m__, conjecture, ? [X0] : ((aNaturalNumber0(X0) & (doDivides0(X0,xk) & isPrime0(X0))))). % 186.58/27.39 fof(negated_conjecture, negated_conjecture, ~? [X0] : ((aNaturalNumber0(X0) & (doDivides0(X0,xk) & isPrime0(X0)))), inference(negate_conjecture, [status(cth)], [m__])). % 186.58/27.39 cnf(c0, plain, aNaturalNumber0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 186.58/27.39 cnf(c1, plain, aNaturalNumber0(sz10), inference(clausification, [status(esa)], [mSortsC_01])). % 186.58/27.39 cnf(c3, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | aNaturalNumber0(sdtpldt0(X1,X0)), inference(clausification, [status(esa)], [mSortsB])). % 186.58/27.39 cnf(c5, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtpldt0(X0,X1) = sdtpldt0(X1,X0), inference(clausification, [status(esa)], [mAddComm])). % 186.58/27.39 cnf(c7, plain, ~aNaturalNumber0(X0) | sdtpldt0(X0,sz00) = X0, inference(clausification, [status(esa)], [m_AddZero])). % 186.58/27.39 cnf(c8, plain, ~aNaturalNumber0(X0) | sdtpldt0(sz00,X0) = X0, inference(clausification, [status(esa)], [m_AddZero])). % 186.58/27.39 cnf(c11, plain, ~aNaturalNumber0(X0) | sdtasdt0(X0,sz10) = X0, inference(clausification, [status(esa)], [m_MulUnit])). % 186.58/27.39 cnf(c12, plain, ~aNaturalNumber0(X0) | sdtasdt0(sz10,X0) = X0, inference(clausification, [status(esa)], [m_MulUnit])). % 186.58/27.39 cnf(c14, plain, ~aNaturalNumber0(X0) | sdtasdt0(sz00,X0) = sz00, inference(clausification, [status(esa)], [m_MulZero])). % 186.58/27.39 cnf(c26, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtpldt0(X1,X2) != X0 | ~aNaturalNumber0(X2) | sdtlseqdt0(X1,X0), inference(clausification, [status(esa)], [mDefLE])). % 186.58/27.39 cnf(c28, plain, sdtpldt0(X0,X1) = X2 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X2) | sdtmndt0(X2,X0) != X1 | ~sdtlseqdt0(X0,X2), inference(clausification, [status(esa)], [mDefDiff])). % 186.58/27.39 cnf(c29, plain, sdtpldt0(X0,X1) != X2 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~sdtlseqdt0(X0,X2) | sdtmndt0(X2,X0) = X1 | ~aNaturalNumber0(X2), inference(clausification, [status(esa)], [mDefDiff])). % 186.58/27.39 cnf(c31, plain, ~sdtlseqdt0(X0,X1) | ~aNaturalNumber0(X1) | ~sdtlseqdt0(X1,X0) | X0 = X1 | ~aNaturalNumber0(X0), inference(clausification, [status(esa)], [mLEAsym])). % 186.58/27.39 cnf(c33, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | X1 != X0 | sdtlseqdt0(X1,X0), inference(clausification, [status(esa)], [mLETotal])). % 186.58/27.39 cnf(c34, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtlseqdt0(X0,X1) | sdtlseqdt0(X1,X0), inference(clausification, [status(esa)], [mLETotal])). % 186.58/27.39 cnf(c46, plain, ~aNaturalNumber0(X0) | iLess0(X1,X0) | ~sdtlseqdt0(X1,X0) | X0 = X1 | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mIH_03])). % 186.58/27.39 cnf(c47, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~doDivides0(X1,X0) | aNaturalNumber0(sK58(X1,X0)), inference(clausification, [status(esa)], [mDefDiv])). % 186.58/27.39 cnf(c48, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~doDivides0(X1,X0) | sdtasdt0(X1,sK58(X1,X0)) = X0, inference(clausification, [status(esa)], [mDefDiv])). % 186.58/27.39 cnf(c49, plain, sdtasdt0(X0,X1) != X2 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2) | doDivides0(X0,X2), inference(clausification, [status(esa)], [mDefDiv])). % 186.58/27.39 cnf(c53, plain, doDivides0(X0,X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X2) | ~aNaturalNumber0(X1) | ~doDivides0(X2,X1) | ~doDivides0(X0,X2), inference(clausification, [status(esa)], [mDivTrans])). % 186.58/27.39 cnf(c55, plain, ~doDivides0(X0,sdtpldt0(X1,X2)) | ~aNaturalNumber0(X0) | doDivides0(X0,X2) | ~aNaturalNumber0(X2) | ~doDivides0(X0,X1) | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mDivMin])). % 186.58/27.39 cnf(c56, plain, X0 = sz00 | ~doDivides0(X1,X0) | ~aNaturalNumber0(X0) | sdtlseqdt0(X1,X0) | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mDivLE])). % 186.58/27.39 cnf(c58, plain, ~aNaturalNumber0(X0) | X1(X0), inference(clausification, [status(esa)], [mDefPrime])). % 186.58/27.39 cnf(c62, plain, ~X0(X1) | X1 = sz10 | isPrime0(X1) | doDivides0(sK80(X1),X1) | X1 = sz00, inference(clausification, [status(esa)], [mDefPrime])). % 186.58/27.39 cnf(c63, plain, aNaturalNumber0(sK80(X0)) | ~X1(X0) | X0 = sz00 | X0 = sz10 | isPrime0(X0), inference(clausification, [status(esa)], [mDefPrime])). % 186.58/27.39 cnf(c64, plain, ~X0(X1) | X1 = sz00 | X1 = sz10 | X1 != sK80(X1) | isPrime0(X1), inference(clausification, [status(esa)], [mDefPrime])). % 186.58/27.39 cnf(c65, plain, ~X0(X1) | X1 = sz00 | sK80(X1) != sz10 | X1 = sz10 | isPrime0(X1), inference(clausification, [status(esa)], [mDefPrime])). % 186.58/27.39 cnf(c66, plain, aNaturalNumber0(xk), inference(clausification, [status(esa)], [m__1716])). % 186.58/27.39 cnf(c67, plain, aNaturalNumber0(sK82(X0)) | ~iLess0(X0,xk) | ~aNaturalNumber0(X0) | X0 = sz10 | X0 = sz00, inference(clausification, [status(esa)], [m__1700])). % 186.58/27.39 cnf(c68, plain, ~iLess0(X0,xk) | ~aNaturalNumber0(X0) | X0 = sz10 | X0 = sz00 | isPrime0(sK82(X0)), inference(clausification, [status(esa)], [m__1700])). % 186.58/27.39 cnf(c69, plain, doDivides0(sK82(X0),X0) | ~iLess0(X0,xk) | ~aNaturalNumber0(X0) | X0 = sz10 | X0 = sz00, inference(clausification, [status(esa)], [m__1700])). % 186.58/27.39 cnf(c70, plain, xk != sz00, inference(clausification, [status(esa)], [m__1716_04])). % 186.58/27.39 cnf(c71, plain, xk != sz10, inference(clausification, [status(esa)], [m__1716_04])). % 186.58/27.39 cnf(c72, plain, ~isPrime0(xk), inference(clausification, [status(esa)], [m__1725])). % 186.58/27.39 cnf(c73, plain, ~aNaturalNumber0(X0) | ~isPrime0(X0) | ~doDivides0(X0,xk), inference(clausification, [status(esa)], [negated_conjecture])). % 186.58/27.39 cnf(d0, plain, 'Ts77'(xk), inference(resolution, [status(thm)], [c58,c66])). % 186.58/27.39 cnf(d1, plain, X0 = sz00 | X0 = sz10 | ~'Ts77'(X0) | isPrime0(X0) | sdtasdt0(sz10,sK80(X0)) = sK80(X0), inference(resolution, [status(thm)], [c63,c12])). % 186.58/27.39 cnf(d2, plain, xk = sz00 | xk = sz10 | sdtasdt0(sz10,sK80(xk)) = sK80(xk) | isPrime0(xk), inference(resolution, [status(thm)], [d1,d0])). % 186.58/27.39 cnf(d3, plain, sdtasdt0(sz10,sK80(xk)) = sK80(xk) | xk = sz00 | xk = sz10, inference(resolution, [status(thm)], [c72,d2])). % 186.58/27.39 cnf(d4, plain, sdtasdt0(sz10,sK80(xk)) = sK80(xk) | xk = sz10, inference(resolution, [status(thm)], [c70,d3])). % 186.58/27.39 cnf(d5, plain, sdtasdt0(sz10,sK80(xk)) = sK80(xk), inference(resolution, [status(thm)], [c71,d4])). % 186.58/27.39 cnf(d6, plain, sdtpldt0(xk,sz00) = xk, inference(resolution, [status(thm)], [c7,c66])). % 186.58/27.39 cnf(d7, plain, sdtmndt0(sdtpldt0(X0,X1),X0) = X1 | ~aNaturalNumber0(sdtpldt0(X0,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~sdtlseqdt0(X0,sdtpldt0(X0,X1)), inference(equality_resolution, [status(thm)], [c29])). % 186.58/27.39 cnf(d8, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtmndt0(sdtpldt0(X1,X0),X1) = X0 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~sdtlseqdt0(X1,sdtpldt0(X1,X0)), inference(resolution, [status(thm)], [c3,d7])). % 186.58/27.39 cnf(d9, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(sdtpldt0(X1,X0)) | sdtlseqdt0(X1,sdtpldt0(X1,X0)), inference(equality_resolution, [status(thm)], [c26])). % 186.58/27.39 cnf(d10, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | sdtlseqdt0(X1,sdtpldt0(X1,X0)), inference(resolution, [status(thm)], [c3,d9])). % 186.58/27.39 cnf(d11, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtmndt0(sdtpldt0(X0,X1),X0) = X1 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1), inference(resolution, [status(thm)], [d10,d8])). % 186.58/27.39 cnf(d12, plain, sdtmndt0(sdtpldt0(xk,X0),xk) = X0 | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [d11,c66])). % 186.58/27.39 cnf(d13, plain, sdtmndt0(sdtpldt0(xk,sz00),xk) = sz00, inference(resolution, [status(thm)], [d12,c0])). % 186.58/27.39 cnf(d14, plain, sdtmndt0(xk,xk) = sz00, inference(demodulation, [status(thm)], [d13,d6])). % 186.58/27.39 cnf(d15, plain, 'Ts77'(sdtpldt0(X0,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c58,c3])). % 186.58/27.39 cnf(d16, plain, sdtpldt0(X0,sdtmndt0(X1,X0)) = X1 | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~sdtlseqdt0(X0,X1), inference(equality_resolution, [status(thm)], [c28])). % 186.58/27.39 cnf(d17, plain, X0 = X1 | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | iLess0(X1,X0) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtlseqdt0(X0,X1), inference(resolution, [status(thm)], [c46,c34])). % 186.58/27.39 cnf(d18, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtlseqdt0(X1,X0) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtlseqdt0(X1,X0) | iLess0(X0,X1), inference(resolution, [status(thm)], [c33,d17])). % 186.58/27.39 cnf(d19, plain, X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X0) | ~iLess0(X0,xk) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK82(X0)) | ~doDivides0(X0,X1) | doDivides0(sK82(X0),X1), inference(resolution, [status(thm)], [c69,c53])). % 186.58/27.39 cnf(d20, plain, X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X0) | ~iLess0(X0,xk) | X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~iLess0(X0,xk) | ~doDivides0(X0,X1) | doDivides0(sK82(X0),X1), inference(resolution, [status(thm)], [c67,d19])). % 186.58/27.39 cnf(d21, plain, X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(xk) | ~aNaturalNumber0(X0) | ~iLess0(X0,xk) | ~doDivides0(X0,xk) | ~aNaturalNumber0(sK82(X0)) | ~isPrime0(sK82(X0)), inference(resolution, [status(thm)], [d20,c73])). % 186.58/27.39 cnf(d22, plain, X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK82(X0)) | ~iLess0(X0,xk) | ~doDivides0(X0,xk) | ~isPrime0(sK82(X0)), inference(resolution, [status(thm)], [c66,d21])). % 186.58/27.39 cnf(d23, plain, X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X0) | ~iLess0(X0,xk) | X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X0) | ~iLess0(X0,xk) | ~doDivides0(X0,xk) | ~isPrime0(sK82(X0)), inference(resolution, [status(thm)], [c67,d22])). % 186.58/27.39 cnf(d24, plain, X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X0) | ~iLess0(X0,xk) | X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X0) | ~iLess0(X0,xk) | ~doDivides0(X0,xk), inference(resolution, [status(thm)], [c68,d23])). % 186.58/27.39 cnf(d25, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | ~aNaturalNumber0(sK80(xk)) | ~iLess0(sK80(xk),xk) | xk = sz00 | xk = sz10 | ~'Ts77'(xk) | isPrime0(xk), inference(resolution, [status(thm)], [d24,c62])). % 186.58/27.39 cnf(d26, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sz00 | xk = sz10 | ~aNaturalNumber0(sK80(xk)) | ~iLess0(sK80(xk),xk) | ~'Ts77'(xk), inference(resolution, [status(thm)], [c72,d25])). % 186.58/27.39 cnf(d27, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sz10 | ~aNaturalNumber0(sK80(xk)) | ~iLess0(sK80(xk),xk) | ~'Ts77'(xk), inference(resolution, [status(thm)], [c70,d26])). % 186.58/27.39 cnf(d28, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | ~aNaturalNumber0(sK80(xk)) | ~iLess0(sK80(xk),xk) | ~'Ts77'(xk), inference(resolution, [status(thm)], [c71,d27])). % 186.58/27.39 cnf(d29, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | ~aNaturalNumber0(sK80(xk)) | ~iLess0(sK80(xk),xk), inference(resolution, [status(thm)], [d0,d28])). % 186.58/27.39 cnf(d30, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | ~aNaturalNumber0(sK80(xk)) | ~aNaturalNumber0(xk) | ~aNaturalNumber0(sK80(xk)) | sdtlseqdt0(xk,sK80(xk)), inference(resolution, [status(thm)], [d29,d18])). % 186.58/27.39 cnf(d31, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | ~aNaturalNumber0(sK80(xk)) | sdtlseqdt0(xk,sK80(xk)), inference(resolution, [status(thm)], [c66,d30])). % 186.58/27.39 cnf(d32, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | ~aNaturalNumber0(sK80(xk)) | sdtpldt0(xk,sdtmndt0(sK80(xk),xk)) = sK80(xk) | ~aNaturalNumber0(sK80(xk)) | ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [d31,d16])). % 186.58/27.39 cnf(d33, plain, sdtpldt0(xk,sdtmndt0(sK80(xk),xk)) = sK80(xk) | sK80(xk) = sz00 | sK80(xk) = sz10 | ~aNaturalNumber0(sK80(xk)), inference(resolution, [status(thm)], [c66,d32])). % 186.58/27.39 cnf(d34, plain, X0 = sz00 | X0 = sz10 | ~'Ts77'(X0) | isPrime0(X0) | X0 = sz00 | ~aNaturalNumber0(sK80(X0)) | ~aNaturalNumber0(X0) | sdtlseqdt0(sK80(X0),X0), inference(resolution, [status(thm)], [c62,c56])). % 186.58/27.39 cnf(d35, plain, ~aNaturalNumber0(X0) | X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK80(X0)) | sdtlseqdt0(sK80(X0),X0) | isPrime0(X0), inference(resolution, [status(thm)], [c58,d34])). % 186.58/27.39 cnf(d36, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | ~aNaturalNumber0(sK80(xk)) | xk = sK80(xk) | ~aNaturalNumber0(sK80(xk)) | ~aNaturalNumber0(xk) | ~sdtlseqdt0(sK80(xk),xk), inference(resolution, [status(thm)], [d31,c31])). % 186.58/27.39 cnf(d37, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sK80(xk) | ~aNaturalNumber0(sK80(xk)) | ~sdtlseqdt0(sK80(xk),xk), inference(resolution, [status(thm)], [c66,d36])). % 186.58/27.39 cnf(d38, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sK80(xk) | ~aNaturalNumber0(sK80(xk)) | xk = sz00 | xk = sz10 | ~aNaturalNumber0(xk) | ~aNaturalNumber0(sK80(xk)) | isPrime0(xk), inference(resolution, [status(thm)], [d37,d35])). % 186.58/27.39 cnf(d39, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sz00 | xk = sz10 | xk = sK80(xk) | ~aNaturalNumber0(sK80(xk)) | isPrime0(xk), inference(resolution, [status(thm)], [c66,d38])). % 186.58/27.39 cnf(d40, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sz00 | xk = sz10 | xk = sK80(xk) | ~aNaturalNumber0(sK80(xk)), inference(resolution, [status(thm)], [c72,d39])). % 186.58/27.39 cnf(d41, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sz10 | xk = sK80(xk) | ~aNaturalNumber0(sK80(xk)), inference(resolution, [status(thm)], [c70,d40])). % 186.58/27.39 cnf(d42, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sK80(xk) | ~aNaturalNumber0(sK80(xk)), inference(resolution, [status(thm)], [c71,d41])). % 186.58/27.39 cnf(d43, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sK80(xk) | xk = sz00 | xk = sz10 | ~'Ts77'(xk) | isPrime0(xk), inference(resolution, [status(thm)], [d42,c63])). % 186.58/27.39 cnf(d44, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sz00 | xk = sz10 | xk = sK80(xk) | ~'Ts77'(xk), inference(resolution, [status(thm)], [c72,d43])). % 186.58/27.39 cnf(d45, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sz10 | xk = sK80(xk) | ~'Ts77'(xk), inference(resolution, [status(thm)], [c70,d44])). % 186.58/27.39 cnf(d46, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sK80(xk) | ~'Ts77'(xk), inference(resolution, [status(thm)], [c71,d45])). % 186.58/27.39 cnf(d47, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | xk = sK80(xk), inference(resolution, [status(thm)], [d0,d46])). % 186.58/27.39 cnf(d48, plain, ~aNaturalNumber0(xk) | sdtpldt0(xk,sdtmndt0(sK80(xk),xk)) = sK80(xk) | sK80(xk) = sz00 | sK80(xk) = sz10 | sK80(xk) = sz00 | sK80(xk) = sz10, inference(superposition, [status(thm)], [d47,d33])). % 186.58/27.39 cnf(d49, plain, sdtpldt0(xk,sdtmndt0(sK80(xk),xk)) = sK80(xk) | sK80(xk) = sz00 | sK80(xk) = sz10, inference(resolution, [status(thm)], [c66,d48])). % 186.58/27.39 cnf(d50, plain, 'Ts77'(sK80(xk)) | ~aNaturalNumber0(sdtmndt0(sK80(xk),xk)) | ~aNaturalNumber0(xk) | sK80(xk) = sz00 | sK80(xk) = sz10, inference(superposition, [status(thm)], [d49,d15])). % 186.58/27.39 cnf(d51, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | ~aNaturalNumber0(sdtmndt0(sK80(xk),xk)) | 'Ts77'(sK80(xk)), inference(resolution, [status(thm)], [c66,d50])). % 186.58/27.39 cnf(d52, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | ~aNaturalNumber0(sK80(xk)) | sK80(xk) = xk | ~aNaturalNumber0(xk) | ~aNaturalNumber0(sK80(xk)) | iLess0(xk,sK80(xk)), inference(resolution, [status(thm)], [d31,c46])). % 186.58/27.39 cnf(d53, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | sK80(xk) = xk | ~aNaturalNumber0(sK80(xk)) | iLess0(xk,sK80(xk)), inference(resolution, [status(thm)], [c66,d52])). % 186.58/27.39 cnf(d54, plain, iLess0(xk,xk) | sK80(xk) = sz00 | sK80(xk) = sz10 | sK80(xk) = xk | ~aNaturalNumber0(sK80(xk)) | sK80(xk) = sz00 | sK80(xk) = sz10, inference(superposition, [status(thm)], [d47,d53])). % 186.58/27.39 cnf(d55, plain, sdtasdt0(xk,sz10) = xk, inference(resolution, [status(thm)], [c11,c66])). % 186.58/27.39 cnf(d56, plain, xk != X0 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(xk) | doDivides0(xk,X0), inference(superposition, [status(thm)], [d55,c49])). % 186.58/27.39 cnf(d57, plain, xk != X0 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(xk) | doDivides0(xk,X0), inference(resolution, [status(thm)], [c1,d56])). % 186.58/27.39 cnf(d58, plain, xk != X0 | ~aNaturalNumber0(X0) | doDivides0(xk,X0), inference(resolution, [status(thm)], [c66,d57])). % 186.58/27.39 cnf(d59, plain, ~aNaturalNumber0(xk) | doDivides0(xk,xk), inference(equality_resolution, [status(thm)], [d58])). % 186.58/27.39 cnf(d60, plain, doDivides0(xk,xk), inference(resolution, [status(thm)], [c66,d59])). % 186.58/27.39 cnf(d61, plain, xk = sz00 | xk = sz10 | ~aNaturalNumber0(xk) | ~iLess0(xk,xk), inference(resolution, [status(thm)], [d24,d60])). % 186.58/27.39 cnf(d62, plain, xk = sz00 | xk = sz10 | ~iLess0(xk,xk), inference(resolution, [status(thm)], [c66,d61])). % 186.58/27.39 cnf(d63, plain, xk = sz10 | ~iLess0(xk,xk), inference(resolution, [status(thm)], [c70,d62])). % 186.58/27.39 cnf(d64, plain, ~iLess0(xk,xk), inference(resolution, [status(thm)], [c71,d63])). % 186.58/27.39 cnf(d65, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | sK80(xk) = xk | ~aNaturalNumber0(sK80(xk)), inference(resolution, [status(thm)], [d64,d54])). % 186.58/27.39 cnf(d66, plain, ~aNaturalNumber0(xk) | sK80(xk) = sz00 | sK80(xk) = sz10 | sK80(xk) = xk | sK80(xk) = sz00 | sK80(xk) = sz10, inference(superposition, [status(thm)], [d47,d65])). % 186.58/27.39 cnf(d67, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | sK80(xk) = xk, inference(resolution, [status(thm)], [c66,d66])). % 186.58/27.39 cnf(d68, plain, ~aNaturalNumber0(sdtmndt0(xk,xk)) | sK80(xk) = sz00 | sK80(xk) = sz10 | 'Ts77'(sK80(xk)) | sK80(xk) = sz00 | sK80(xk) = sz10, inference(superposition, [status(thm)], [d67,d51])). % 186.58/27.39 cnf(d69, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | ~aNaturalNumber0(sz00) | 'Ts77'(sK80(xk)), inference(demodulation, [status(thm)], [d68,d14])). % 186.58/27.39 cnf(d70, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | 'Ts77'(sK80(xk)), inference(resolution, [status(thm)], [c0,d69])). % 186.58/27.39 cnf(d71, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | sK80(xk) = sz00 | sK80(xk) = sz10 | sdtasdt0(sz10,sK80(sK80(xk))) = sK80(sK80(xk)) | isPrime0(sK80(xk)), inference(resolution, [status(thm)], [d70,d1])). % 186.58/27.39 cnf(d72, plain, isPrime0(xk) | sdtasdt0(sz10,sK80(sK80(xk))) = sK80(sK80(xk)) | sK80(xk) = sz00 | sK80(xk) = sz10 | sK80(xk) = sz00 | sK80(xk) = sz10, inference(superposition, [status(thm)], [d67,d71])). % 186.58/27.39 cnf(d73, plain, sdtasdt0(sz10,sK80(sK80(xk))) = sK80(sK80(xk)) | sK80(xk) = sz00 | sK80(xk) = sz10, inference(resolution, [status(thm)], [c72,d72])). % 186.58/27.39 cnf(d74, plain, sdtasdt0(sz10,sK80(xk)) = sK80(sK80(xk)) | sK80(xk) = sz00 | sK80(xk) = sz10 | sK80(xk) = sz00 | sK80(xk) = sz10, inference(superposition, [status(thm)], [d67,d73])). % 186.58/27.39 cnf(d75, plain, sK80(xk) = sK80(sK80(xk)) | sK80(xk) = sz00 | sK80(xk) = sz10, inference(demodulation, [status(thm)], [d74,d5])). % 186.58/27.39 cnf(d76, plain, sK80(xk) != sK80(xk) | sK80(xk) = sz00 | sK80(xk) = sz10 | ~'Ts77'(sK80(xk)) | isPrime0(sK80(xk)) | sK80(xk) = sz00 | sK80(xk) = sz10, inference(superposition, [status(thm)], [d75,c64])). % 186.58/27.39 cnf(d77, plain, X0 = sz00 | X0 = sz10 | ~'Ts77'(X0) | isPrime0(X0) | sdtpldt0(sK80(X0),sz00) = sK80(X0), inference(resolution, [status(thm)], [c63,c7])). % 186.58/27.39 cnf(d78, plain, xk = sz00 | xk = sz10 | sdtpldt0(sK80(xk),sz00) = sK80(xk) | isPrime0(xk), inference(resolution, [status(thm)], [d77,d0])). % 186.58/27.39 cnf(d79, plain, sdtpldt0(sK80(xk),sz00) = sK80(xk) | xk = sz00 | xk = sz10, inference(resolution, [status(thm)], [c72,d78])). % 186.58/27.39 cnf(d80, plain, sdtpldt0(sK80(xk),sz00) = sK80(xk) | xk = sz10, inference(resolution, [status(thm)], [c70,d79])). % 186.58/27.39 cnf(d81, plain, sdtpldt0(sK80(xk),sz00) = sK80(xk), inference(resolution, [status(thm)], [c71,d80])). % 186.58/27.39 cnf(d82, plain, sdtpldt0(sz00,X0) = sdtpldt0(X0,sz00) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c5,c0])). % 186.58/27.39 cnf(d83, plain, X0 = sz00 | X0 = sz10 | ~'Ts77'(X0) | isPrime0(X0) | sdtpldt0(sz00,sK80(X0)) = sdtpldt0(sK80(X0),sz00), inference(resolution, [status(thm)], [c63,d82])). % 186.58/27.39 cnf(d84, plain, xk = sz00 | xk = sz10 | sdtpldt0(sz00,sK80(xk)) = sdtpldt0(sK80(xk),sz00) | isPrime0(xk), inference(resolution, [status(thm)], [d83,d0])). % 186.58/27.39 cnf(d85, plain, sdtpldt0(sz00,sK80(xk)) = sK80(xk) | xk = sz00 | xk = sz10 | isPrime0(xk), inference(demodulation, [status(thm)], [d84,d81])). % 186.58/27.39 cnf(d86, plain, sdtpldt0(sz00,sK80(xk)) = sK80(xk) | xk = sz00 | xk = sz10, inference(resolution, [status(thm)], [c72,d85])). % 186.58/27.39 cnf(d87, plain, sdtpldt0(sz00,sK80(xk)) = sK80(xk) | xk = sz10, inference(resolution, [status(thm)], [c70,d86])). % 186.58/27.39 cnf(d88, plain, sdtpldt0(sz00,sK80(xk)) = sK80(xk), inference(resolution, [status(thm)], [c71,d87])). % 186.58/27.39 cnf(d89, plain, X0 = sz00 | X0 = sz10 | ~'Ts77'(X0) | isPrime0(X0) | sdtpldt0(sz00,sK80(X0)) = sK80(X0), inference(resolution, [status(thm)], [c63,c8])). % 186.58/27.39 cnf(d90, plain, xk = sz00 | xk = sz10 | sdtpldt0(sz00,sK80(xk)) = sK80(xk) | isPrime0(xk), inference(resolution, [status(thm)], [d89,d0])). % 186.58/27.39 cnf(d91, plain, sK80(xk) = sK80(xk) | xk = sz00 | xk = sz10 | isPrime0(xk), inference(demodulation, [status(thm)], [d90,d88])). % 186.58/27.39 cnf(d92, plain, sK80(xk) = sK80(xk) | xk = sz00 | xk = sz10, inference(resolution, [status(thm)], [c72,d91])). % 186.58/27.39 cnf(d93, plain, sK80(xk) = sK80(xk) | xk = sz10, inference(resolution, [status(thm)], [c70,d92])). % 186.58/27.39 cnf(d94, plain, sK80(xk) = sK80(xk), inference(resolution, [status(thm)], [c71,d93])). % 186.58/27.39 cnf(d95, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | ~'Ts77'(sK80(xk)) | isPrime0(sK80(xk)), inference(resolution, [status(thm)], [d94,d76])). % 186.58/27.39 cnf(d96, plain, sK80(xk) = sz00 | sK80(xk) = sz10 | sK80(xk) = sz00 | sK80(xk) = sz10 | isPrime0(sK80(xk)), inference(resolution, [status(thm)], [d70,d95])). % 186.58/27.39 cnf(d97, plain, isPrime0(xk) | sK80(xk) = sz00 | sK80(xk) = sz10 | sK80(xk) = sz00 | sK80(xk) = sz10, inference(superposition, [status(thm)], [d67,d96])). % 186.58/27.39 cnf(d98, plain, sK80(xk) = sz00 | sK80(xk) = sz10, inference(resolution, [status(thm)], [c72,d97])). % 186.58/27.39 cnf(d99, plain, sz10 != sz10 | xk = sz00 | xk = sz10 | ~'Ts77'(xk) | isPrime0(xk) | sK80(xk) = sz00, inference(superposition, [status(thm)], [d98,c65])). % 186.58/27.39 cnf(d100, plain, sz10 != sz10 | sK80(xk) = sz00 | xk = sz00 | xk = sz10 | ~'Ts77'(xk), inference(resolution, [status(thm)], [c72,d99])). % 186.58/27.39 cnf(d101, plain, sz10 != sz10 | sK80(xk) = sz00 | xk = sz10 | ~'Ts77'(xk), inference(resolution, [status(thm)], [c70,d100])). % 186.58/27.39 cnf(d102, plain, sz10 != sz10 | sK80(xk) = sz00 | ~'Ts77'(xk), inference(resolution, [status(thm)], [c71,d101])). % 186.58/27.39 cnf(d103, plain, sz10 != sz10 | sK80(xk) = sz00, inference(resolution, [status(thm)], [d0,d102])). % 186.58/27.39 cnf(d104, plain, sdtpldt0(sz00,sz10) = sz10, inference(resolution, [status(thm)], [c8,c1])). % 186.58/27.39 cnf(d105, plain, sz10 != X0 | sdtmndt0(X0,sz00) = sz10 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(sz00) | ~sdtlseqdt0(sz00,X0), inference(superposition, [status(thm)], [d104,c29])). % 186.58/27.39 cnf(d106, plain, sz10 != X0 | sdtmndt0(X0,sz00) = sz10 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | ~sdtlseqdt0(sz00,X0), inference(resolution, [status(thm)], [c0,d105])). % 186.58/27.39 cnf(d107, plain, sz10 != X0 | sdtmndt0(X0,sz00) = sz10 | ~aNaturalNumber0(X0) | ~sdtlseqdt0(sz00,X0), inference(resolution, [status(thm)], [c1,d106])). % 186.58/27.39 cnf(d108, plain, sz10 != X0 | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(X0) | sdtlseqdt0(sz00,X0), inference(superposition, [status(thm)], [d104,c26])). % 186.58/27.39 cnf(d109, plain, sz10 != X0 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | sdtlseqdt0(sz00,X0), inference(resolution, [status(thm)], [c0,d108])). % 186.58/27.39 cnf(d110, plain, sz10 != X0 | ~aNaturalNumber0(X0) | sdtlseqdt0(sz00,X0), inference(resolution, [status(thm)], [c1,d109])). % 186.58/27.39 cnf(d111, plain, sz10 != X0 | ~aNaturalNumber0(X0) | sz10 != X0 | sdtmndt0(X0,sz00) = sz10 | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [d110,d107])). % 186.58/27.39 cnf(d112, plain, sdtmndt0(sz10,sz00) = sz10 | ~aNaturalNumber0(sz10), inference(equality_resolution, [status(thm)], [d111])). % 186.58/27.39 cnf(d113, plain, sdtmndt0(sz10,sz00) = sz10, inference(resolution, [status(thm)], [c1,d112])). % 186.58/27.39 cnf(d114, plain, ~aNaturalNumber0(sz10) | sdtlseqdt0(sz00,sz10), inference(equality_resolution, [status(thm)], [d110])). % 186.58/27.39 cnf(d115, plain, sdtlseqdt0(sz00,sz10), inference(resolution, [status(thm)], [c1,d114])). % 186.58/27.39 cnf(d116, plain, sdtpldt0(sz00,sdtmndt0(sz10,sz00)) = sz10 | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(sz00), inference(resolution, [status(thm)], [d16,d115])). % 186.58/27.39 cnf(d117, plain, sdtpldt0(sz00,sz10) = sz10 | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(sz10), inference(demodulation, [status(thm)], [d116,d113])). % 186.58/27.39 cnf(d118, plain, sz10 = sz10 | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(sz10), inference(demodulation, [status(thm)], [d117,d104])). % 186.58/27.39 cnf(d119, plain, sz10 = sz10 | ~aNaturalNumber0(sz10), inference(resolution, [status(thm)], [c0,d118])). % 186.58/27.39 cnf(d120, plain, sz10 = sz10, inference(resolution, [status(thm)], [c1,d119])). % 186.58/27.39 cnf(d121, plain, sK80(xk) = sz00, inference(resolution, [status(thm)], [d120,d103])). % 186.58/27.39 cnf(d122, plain, sdtpldt0(sz00,xk) = xk, inference(resolution, [status(thm)], [c8,c66])). % 186.58/27.39 cnf(d123, plain, sdtpldt0(X0,X1) = sz00 | sdtpldt0(X0,X1) = sz10 | ~'Ts77'(sdtpldt0(X0,X1)) | isPrime0(sdtpldt0(X0,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK80(sdtpldt0(X0,X1))) | doDivides0(sK80(sdtpldt0(X0,X1)),X1) | ~doDivides0(sK80(sdtpldt0(X0,X1)),X0), inference(resolution, [status(thm)], [c62,c55])). % 186.58/27.39 cnf(d124, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtpldt0(X1,X0) = sz00 | sdtpldt0(X1,X0) = sz10 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(sK80(sdtpldt0(X1,X0))) | doDivides0(sK80(sdtpldt0(X1,X0)),X0) | ~doDivides0(sK80(sdtpldt0(X1,X0)),X1) | isPrime0(sdtpldt0(X1,X0)), inference(resolution, [status(thm)], [d15,d123])). % 186.58/27.39 cnf(d125, plain, ~doDivides0(sK80(xk),sz00) | sdtpldt0(sz00,xk) = sz00 | sdtpldt0(sz00,xk) = sz10 | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xk) | ~aNaturalNumber0(sK80(sdtpldt0(sz00,xk))) | doDivides0(sK80(sdtpldt0(sz00,xk)),xk) | isPrime0(sdtpldt0(sz00,xk)), inference(superposition, [status(thm)], [d122,d124])). % 186.58/27.39 cnf(d126, plain, xk = sz00 | sdtpldt0(sz00,xk) = sz10 | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(sK80(sdtpldt0(sz00,xk))) | ~aNaturalNumber0(xk) | doDivides0(sK80(sdtpldt0(sz00,xk)),xk) | ~doDivides0(sK80(xk),sz00) | isPrime0(sdtpldt0(sz00,xk)), inference(demodulation, [status(thm)], [d125,d122])). % 186.58/27.39 cnf(d127, plain, xk = sz00 | xk = sz10 | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(sK80(sdtpldt0(sz00,xk))) | ~aNaturalNumber0(xk) | doDivides0(sK80(sdtpldt0(sz00,xk)),xk) | ~doDivides0(sK80(xk),sz00) | isPrime0(sdtpldt0(sz00,xk)), inference(demodulation, [status(thm)], [d126,d122])). % 186.58/27.39 cnf(d128, plain, xk = sz00 | xk = sz10 | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(sK80(xk)) | ~aNaturalNumber0(xk) | doDivides0(sK80(sdtpldt0(sz00,xk)),xk) | ~doDivides0(sK80(xk),sz00) | isPrime0(sdtpldt0(sz00,xk)), inference(demodulation, [status(thm)], [d127,d122])). % 186.58/27.39 cnf(d129, plain, xk = sz00 | xk = sz10 | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(sK80(xk)) | ~aNaturalNumber0(xk) | doDivides0(sK80(xk),xk) | ~doDivides0(sK80(xk),sz00) | isPrime0(sdtpldt0(sz00,xk)), inference(demodulation, [status(thm)], [d128,d122])). % 186.58/27.39 cnf(d130, plain, xk = sz00 | xk = sz10 | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(sK80(xk)) | ~aNaturalNumber0(xk) | doDivides0(sK80(xk),xk) | ~doDivides0(sK80(xk),sz00) | isPrime0(xk), inference(demodulation, [status(thm)], [d129,d122])). % 186.58/27.39 cnf(d131, plain, xk = sz00 | xk = sz10 | ~aNaturalNumber0(sK80(xk)) | ~aNaturalNumber0(xk) | doDivides0(sK80(xk),xk) | ~doDivides0(sK80(xk),sz00) | isPrime0(xk), inference(resolution, [status(thm)], [c0,d130])). % 186.58/27.39 cnf(d132, plain, xk = sz00 | xk = sz10 | ~aNaturalNumber0(sK80(xk)) | ~doDivides0(sK80(xk),sz00) | doDivides0(sK80(xk),xk) | isPrime0(xk), inference(resolution, [status(thm)], [c66,d131])). % 186.58/27.39 cnf(d133, plain, xk = sz00 | xk = sz10 | ~aNaturalNumber0(sK80(xk)) | ~doDivides0(sK80(xk),sz00) | doDivides0(sK80(xk),xk), inference(resolution, [status(thm)], [c72,d132])). % 186.58/27.39 cnf(d134, plain, xk = sz10 | ~aNaturalNumber0(sK80(xk)) | ~doDivides0(sK80(xk),sz00) | doDivides0(sK80(xk),xk), inference(resolution, [status(thm)], [c70,d133])). % 186.58/27.39 cnf(d135, plain, ~aNaturalNumber0(sK80(xk)) | ~doDivides0(sK80(xk),sz00) | doDivides0(sK80(xk),xk), inference(resolution, [status(thm)], [c71,d134])). % 186.58/27.39 cnf(d136, plain, ~doDivides0(X0,xk) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xk) | ~aNaturalNumber0(X0) | doDivides0(X0,sz00) | ~doDivides0(X0,xk), inference(superposition, [status(thm)], [d6,c55])). % 186.58/27.39 cnf(d137, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(xk) | doDivides0(X0,sz00) | ~doDivides0(X0,xk), inference(resolution, [status(thm)], [c0,d136])). % 186.58/27.39 cnf(d138, plain, ~aNaturalNumber0(X0) | doDivides0(X0,sz00) | ~doDivides0(X0,xk), inference(resolution, [status(thm)], [c66,d137])). % 186.58/27.39 cnf(d139, plain, ~aNaturalNumber0(sK80(xk)) | doDivides0(sK80(xk),sz00) | xk = sz00 | xk = sz10 | ~'Ts77'(xk) | isPrime0(xk), inference(resolution, [status(thm)], [d138,c62])). % 186.58/27.39 cnf(d140, plain, xk = sz00 | xk = sz10 | ~aNaturalNumber0(sK80(xk)) | doDivides0(sK80(xk),sz00) | ~'Ts77'(xk), inference(resolution, [status(thm)], [c72,d139])). % 186.58/27.39 cnf(d141, plain, xk = sz10 | ~aNaturalNumber0(sK80(xk)) | doDivides0(sK80(xk),sz00) | ~'Ts77'(xk), inference(resolution, [status(thm)], [c70,d140])). % 186.58/27.39 cnf(d142, plain, ~aNaturalNumber0(sK80(xk)) | doDivides0(sK80(xk),sz00) | ~'Ts77'(xk), inference(resolution, [status(thm)], [c71,d141])). % 186.58/27.39 cnf(d143, plain, ~aNaturalNumber0(sK80(xk)) | doDivides0(sK80(xk),sz00), inference(resolution, [status(thm)], [d0,d142])). % 186.58/27.39 cnf(d144, plain, ~aNaturalNumber0(sK80(xk)) | ~aNaturalNumber0(sK80(xk)) | doDivides0(sK80(xk),xk), inference(resolution, [status(thm)], [d143,d135])). % 186.58/27.39 cnf(d145, plain, ~aNaturalNumber0(sz00) | doDivides0(sK80(xk),xk), inference(demodulation, [status(thm)], [d144,d121])). % 186.58/27.39 cnf(d146, plain, ~aNaturalNumber0(sz00) | doDivides0(sz00,xk), inference(demodulation, [status(thm)], [d145,d121])). % 186.58/27.39 cnf(d147, plain, doDivides0(sz00,xk), inference(resolution, [status(thm)], [c0,d146])). % 186.58/27.39 cnf(d148, plain, sdtasdt0(sz00,sK58(sz00,xk)) = xk | ~aNaturalNumber0(xk) | ~aNaturalNumber0(sz00), inference(resolution, [status(thm)], [d147,c48])). % 186.58/27.39 cnf(d149, plain, sdtasdt0(sz00,sK58(sz00,xk)) = xk | ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [c0,d148])). % 186.58/27.39 cnf(d150, plain, sdtasdt0(sz00,sK58(sz00,xk)) = xk, inference(resolution, [status(thm)], [c66,d149])). % 186.58/27.39 cnf(d151, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~doDivides0(X1,X0) | sdtasdt0(sz00,sK58(X1,X0)) = sz00, inference(resolution, [status(thm)], [c47,c14])). % 186.58/27.39 cnf(d152, plain, sdtasdt0(sz00,sK58(sz00,xk)) = sz00 | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [d147,d151])). % 186.58/27.39 cnf(d153, plain, xk = sz00 | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xk), inference(demodulation, [status(thm)], [d152,d150])). % 186.58/27.39 cnf(d154, plain, xk = sz00 | ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [c0,d153])). % 186.58/27.39 cnf(d155, plain, xk = sz00, inference(resolution, [status(thm)], [c66,d154])). % 186.58/27.39 cnf(d156, plain, $false, inference(resolution, [status(thm)], [c70,d155])). % 186.58/27.39 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------