%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM483+3 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/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:12:53 AM UTC 2026 % Result : Theorem 122.15s 33.09s % Output : CNFRefutation 122.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM483+3 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.08/0.35 % Computer : n010.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sat Sep 26 02:56:30 UTC 2026 % 0.08/0.36 % CPUTime : % 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 122.15/33.09 % SZS status Theorem for theBenchmark.p % 122.15/33.09 % SZS output start CNFRefutation for theBenchmark.p % 122.15/33.09 fof(mSortsC_01, axiom, (aNaturalNumber0(sz10) & sz10 != sz00)). % 122.15/33.09 fof(mMulComm, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => sdtasdt0(X0,X1) = sdtasdt0(X1,X0)))). % 122.15/33.09 fof(m_MulUnit, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz10) = X0 & X0 = sdtasdt0(sz10,X0))))). % 122.15/33.09 fof(m_MulZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 122.15/33.09 fof(mDefLE, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (sdtlseqdt0(X0,X1) <=> ? [X2] : ((aNaturalNumber0(X2) & sdtpldt0(X0,X2) = X1)))))). % 122.15/33.09 fof(mLERefl, axiom, ! [X0] : ((aNaturalNumber0(X0) => sdtlseqdt0(X0,X0)))). % 122.15/33.09 fof(mLENTr, axiom, ! [X0] : ((aNaturalNumber0(X0) => (X0 = sz00 | (X0 = sz10 | (sz10 != X0 & sdtlseqdt0(sz10,X0))))))). % 122.15/33.09 fof(mMonMul2, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (X0 != sz00 => sdtlseqdt0(X1,sdtasdt0(X1,X0)))))). % 122.15/33.09 fof(mIH_03, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((X0 != X1 & sdtlseqdt0(X0,X1)) => iLess0(X0,X1))))). % 122.15/33.09 fof(mDefDiv, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (doDivides0(X0,X1) <=> ? [X2] : ((aNaturalNumber0(X2) & X1 = sdtasdt0(X0,X2))))))). % 122.15/33.09 fof(mDivTrans, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => ((doDivides0(X0,X1) & doDivides0(X1,X2)) => doDivides0(X0,X2))))). % 122.15/33.09 fof(mDivLE, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((doDivides0(X0,X1) & X1 != sz00) => sdtlseqdt0(X0,X1))))). % 122.15/33.09 fof(m__1716, hypothesis, aNaturalNumber0(xk)). % 122.15/33.09 fof(m__1700, hypothesis, ! [X0] : (((aNaturalNumber0(X0) & (X0 != sz00 & X0 != sz10)) => (iLess0(X0,xk) => ? [X1] : ((aNaturalNumber0(X1) & (? [X2] : ((aNaturalNumber0(X2) & X0 = sdtasdt0(X1,X2))) & (doDivides0(X1,X0) & (X1 != sz00 & (X1 != sz10 & (! [X2] : (((aNaturalNumber0(X2) & (? [X3] : ((aNaturalNumber0(X3) & X1 = sdtasdt0(X2,X3))) | doDivides0(X2,X1))) => (X2 = sz10 | X2 = X1))) & isPrime0(X1)))))))))))). % 122.15/33.09 fof(m__1716_04, hypothesis, (xk != sz00 & xk != sz10)). % 122.15/33.09 fof(m__, conjecture, ? [X0] : ((aNaturalNumber0(X0) & ((? [X1] : ((aNaturalNumber0(X1) & xk = sdtasdt0(X0,X1))) | doDivides0(X0,xk)) & ((X0 != sz00 & (X0 != sz10 & ! [X1] : (((aNaturalNumber0(X1) & (? [X2] : ((aNaturalNumber0(X2) & X0 = sdtasdt0(X1,X2))) & doDivides0(X1,X0))) => (X1 = sz10 | X1 = X0))))) | isPrime0(X0)))))). % 122.15/33.09 fof(negated_conjecture, negated_conjecture, ~? [X0] : ((aNaturalNumber0(X0) & ((? [X1] : ((aNaturalNumber0(X1) & xk = sdtasdt0(X0,X1))) | doDivides0(X0,xk)) & ((X0 != sz00 & (X0 != sz10 & ! [X1] : (((aNaturalNumber0(X1) & (? [X2] : ((aNaturalNumber0(X2) & X0 = sdtasdt0(X1,X2))) & doDivides0(X1,X0))) => (X1 = sz10 | X1 = X0))))) | isPrime0(X0))))), inference(negate_conjecture, [status(cth)], [m__])). % 122.15/33.09 cnf(c1, plain, aNaturalNumber0(sz10), inference(clausification, [status(esa)], [mSortsC_01])). % 122.15/33.09 cnf(c2, plain, sz10 != sz00, inference(clausification, [status(esa)], [mSortsC_01])). % 122.15/33.09 cnf(c9, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtasdt0(X0,X1) = sdtasdt0(X1,X0), inference(clausification, [status(esa)], [mMulComm])). % 122.15/33.09 cnf(c11, plain, ~aNaturalNumber0(X0) | sdtasdt0(X0,sz10) = X0, inference(clausification, [status(esa)], [m_MulUnit])). % 122.15/33.09 cnf(c12, plain, ~aNaturalNumber0(X0) | X0 = sdtasdt0(sz10,X0), inference(clausification, [status(esa)], [m_MulUnit])). % 122.15/33.09 cnf(c13, plain, ~aNaturalNumber0(X0) | sdtasdt0(X0,sz00) = sz00, inference(clausification, [status(esa)], [m_MulZero])). % 122.15/33.09 cnf(c25, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~sdtlseqdt0(X0,X1) | sdtpldt0(X0,sK33(X0,X1)) = X1, inference(clausification, [status(esa)], [mDefLE])). % 122.15/33.09 cnf(c30, plain, ~aNaturalNumber0(X0) | sdtlseqdt0(X0,X0), inference(clausification, [status(esa)], [mLERefl])). % 122.15/33.09 cnf(c44, plain, ~aNaturalNumber0(X0) | X0 = sz00 | X0 = sz10 | sdtlseqdt0(sz10,X0), inference(clausification, [status(esa)], [mLENTr])). % 122.15/33.09 cnf(c45, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | X0 = sz00 | sdtlseqdt0(X1,sdtasdt0(X1,X0)), inference(clausification, [status(esa)], [mMonMul2])). % 122.15/33.09 cnf(c46, plain, ~aNaturalNumber0(X0) | X1 = X0 | iLess0(X1,X0) | ~sdtlseqdt0(X1,X0) | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mIH_03])). % 122.15/33.09 cnf(c49, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | doDivides0(X0,X1) | ~aNaturalNumber0(X2) | X1 != sdtasdt0(X0,X2), inference(clausification, [status(esa)], [mDefDiv])). % 122.15/33.09 cnf(c53, plain, ~doDivides0(X0,X1) | ~aNaturalNumber0(X0) | doDivides0(X0,X2) | ~doDivides0(X1,X2) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2), inference(clausification, [status(esa)], [mDivTrans])). % 122.15/33.09 cnf(c56, plain, ~aNaturalNumber0(X0) | X1 = sz00 | sdtlseqdt0(X0,X1) | ~doDivides0(X0,X1) | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mDivLE])). % 122.15/33.09 cnf(c67, plain, aNaturalNumber0(xk), inference(clausification, [status(esa)], [m__1716])). % 122.15/33.09 cnf(c68, plain, ~aNaturalNumber0(X0) | X1(X0) | X0 = sz10 | ~iLess0(X0,xk) | X0 = sz00, inference(clausification, [status(esa)], [m__1700])). % 122.15/33.09 cnf(c69, plain, ~X0(X1) | aNaturalNumber0(sK86(X1)), inference(clausification, [status(esa)], [m__1700])). % 122.15/33.09 cnf(c72, plain, ~X0(X1) | doDivides0(sK86(X1),X1), inference(clausification, [status(esa)], [m__1700])). % 122.15/33.09 cnf(c77, plain, ~X0(X1) | isPrime0(sK86(X1)), inference(clausification, [status(esa)], [m__1700])). % 122.15/33.09 cnf(c78, plain, xk != sz00, inference(clausification, [status(esa)], [m__1716_04])). % 122.15/33.09 cnf(c79, plain, xk != sz10, inference(clausification, [status(esa)], [m__1716_04])). % 122.15/33.09 cnf(c87, plain, ~X0(X1) | ~aNaturalNumber0(X1) | xk != sdtasdt0(X1,X2) | X1 = sz00 | ~aNaturalNumber0(X2) | X1 = sz10, inference(clausification, [status(esa)], [negated_conjecture])). % 122.15/33.09 cnf(c90, plain, ~aNaturalNumber0(X0) | ~doDivides0(X0,xk) | ~isPrime0(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 122.15/33.09 cnf(c91, plain, X0(X1) | aNaturalNumber0(sK95(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 122.15/33.09 cnf(c92, plain, X0(X1) | aNaturalNumber0(sK96(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 122.15/33.09 cnf(c93, plain, X0(X1) | X1 = sdtasdt0(sK95(X1),sK96(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 122.15/33.09 cnf(c94, plain, X0(X1) | doDivides0(sK95(X1),X1), inference(clausification, [status(esa)], [negated_conjecture])). % 122.15/33.09 cnf(c95, plain, X0(X1) | sK95(X1) != sz10, inference(clausification, [status(esa)], [negated_conjecture])). % 122.15/33.09 cnf(c96, plain, X0(X1) | sK95(X1) != X1, inference(clausification, [status(esa)], [negated_conjecture])). % 122.15/33.09 cnf(d0, plain, sdtasdt0(sK96(X0),sz00) = sz00 | 'Ts92'(X0), inference(resolution, [status(thm)], [c13,c92])). % 122.15/33.09 cnf(d1, plain, sdtasdt0(xk,sz10) = xk, inference(resolution, [status(thm)], [c67,c11])). % 122.15/33.09 cnf(d2, plain, xk != xk | xk = sz00 | xk = sz10 | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(xk) | ~'Ts92'(xk), inference(superposition, [status(thm)], [d1,c87])). % 122.15/33.09 cnf(d3, plain, xk = sz00 | xk = sz10 | xk != xk | ~aNaturalNumber0(xk) | ~'Ts92'(xk), inference(resolution, [status(thm)], [c1,d2])). % 122.15/33.09 cnf(d4, plain, xk = sz00 | xk = sz10 | xk != xk | ~'Ts92'(xk), inference(resolution, [status(thm)], [c67,d3])). % 122.15/33.09 cnf(d5, plain, xk = sz10 | xk != xk | ~'Ts92'(xk), inference(resolution, [status(thm)], [c78,d4])). % 122.15/33.09 cnf(d6, plain, xk != xk | ~'Ts92'(xk), inference(resolution, [status(thm)], [c79,d5])). % 122.15/33.09 cnf(d7, plain, ~'Ts92'(xk), inference(equality_resolution, [status(thm)], [d6])). % 122.15/33.09 cnf(d8, plain, sdtasdt0(sK96(xk),sz00) = sz00, inference(resolution, [status(thm)], [d7,d0])). % 122.15/33.09 cnf(d9, plain, X0 = sz00 | ~aNaturalNumber0(sK95(X0)) | ~aNaturalNumber0(X0) | sdtlseqdt0(sK95(X0),X0) | 'Ts92'(X0), inference(resolution, [status(thm)], [c56,c94])). % 122.15/33.09 cnf(d10, plain, X0 = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK95(X0)) | 'Ts92'(X0) | sK95(X0) = X0 | ~aNaturalNumber0(sK95(X0)) | ~aNaturalNumber0(X0) | iLess0(sK95(X0),X0), inference(resolution, [status(thm)], [d9,c46])). % 122.15/33.09 cnf(d11, plain, sK95(xk) = sz00 | sK95(xk) = sz10 | ~aNaturalNumber0(sK95(xk)) | 'Ts84'(sK95(xk)) | xk = sz00 | sK95(xk) = xk | ~aNaturalNumber0(xk) | ~aNaturalNumber0(sK95(xk)) | 'Ts92'(xk), inference(resolution, [status(thm)], [c68,d10])). % 122.15/33.09 cnf(d12, plain, xk = sz00 | sK95(xk) = sz00 | sK95(xk) = sz10 | sK95(xk) = xk | ~aNaturalNumber0(sK95(xk)) | 'Ts84'(sK95(xk)) | 'Ts92'(xk), inference(resolution, [status(thm)], [c67,d11])). % 122.15/33.09 cnf(d13, plain, sK95(xk) = sz00 | sK95(xk) = sz10 | sK95(xk) = xk | ~aNaturalNumber0(sK95(xk)) | 'Ts84'(sK95(xk)) | 'Ts92'(xk), inference(resolution, [status(thm)], [c78,d12])). % 122.15/33.09 cnf(d14, plain, sK95(xk) = sz00 | sK95(xk) = sz10 | sK95(xk) = xk | 'Ts84'(sK95(xk)) | 'Ts92'(xk) | 'Ts92'(xk), inference(resolution, [status(thm)], [d13,c91])). % 122.15/33.09 cnf(d15, plain, sK95(xk) = sz00 | sK95(xk) = sz10 | sK95(xk) = xk | 'Ts84'(sK95(xk)), inference(resolution, [status(thm)], [d7,d14])). % 122.15/33.09 cnf(d16, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK95(X1)) | ~aNaturalNumber0(X1) | ~doDivides0(X0,sK95(X1)) | doDivides0(X0,X1) | 'Ts92'(X1), inference(resolution, [status(thm)], [c53,c94])). % 122.15/33.09 cnf(d17, plain, ~'Ts84'(sK95(X0)) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK86(sK95(X0))) | ~aNaturalNumber0(sK95(X0)) | doDivides0(sK86(sK95(X0)),X0) | 'Ts92'(X0), inference(resolution, [status(thm)], [c72,d16])). % 122.15/33.09 cnf(d18, plain, ~aNaturalNumber0(xk) | ~aNaturalNumber0(sK86(sK95(xk))) | ~aNaturalNumber0(sK95(xk)) | ~'Ts84'(sK95(xk)) | 'Ts92'(xk) | ~aNaturalNumber0(sK86(sK95(xk))) | ~isPrime0(sK86(sK95(xk))), inference(resolution, [status(thm)], [d17,c90])). % 122.15/33.09 cnf(d19, plain, ~aNaturalNumber0(sK86(sK95(xk))) | ~aNaturalNumber0(sK95(xk)) | ~isPrime0(sK86(sK95(xk))) | ~'Ts84'(sK95(xk)) | 'Ts92'(xk), inference(resolution, [status(thm)], [c67,d18])). % 122.15/33.09 cnf(d20, plain, ~aNaturalNumber0(sK86(sK95(xk))) | ~aNaturalNumber0(sK95(xk)) | ~isPrime0(sK86(sK95(xk))) | ~'Ts84'(sK95(xk)), inference(resolution, [status(thm)], [d7,d19])). % 122.15/33.09 cnf(d21, plain, ~aNaturalNumber0(sK86(sK95(xk))) | ~aNaturalNumber0(sK95(xk)) | ~'Ts84'(sK95(xk)) | ~'Ts84'(sK95(xk)), inference(resolution, [status(thm)], [d20,c77])). % 122.15/33.09 cnf(d22, plain, ~aNaturalNumber0(sK95(xk)) | ~'Ts84'(sK95(xk)) | ~'Ts84'(sK95(xk)), inference(resolution, [status(thm)], [d21,c69])). % 122.15/33.09 cnf(d23, plain, ~aNaturalNumber0(sK95(xk)) | sK95(xk) = sz00 | sK95(xk) = sz10 | sK95(xk) = xk, inference(resolution, [status(thm)], [d22,d15])). % 122.15/33.09 cnf(d24, plain, sK95(xk) = sz00 | sK95(xk) = sz10 | sK95(xk) = xk | 'Ts92'(xk), inference(resolution, [status(thm)], [d23,c91])). % 122.15/33.09 cnf(d25, plain, sK95(xk) = sz00 | sK95(xk) = sz10 | sK95(xk) = xk, inference(resolution, [status(thm)], [d7,d24])). % 122.15/33.09 cnf(d26, plain, xk != xk | 'Ts92'(xk) | sK95(xk) = sz00 | sK95(xk) = sz10, inference(superposition, [status(thm)], [d25,c96])). % 122.15/33.09 cnf(d27, plain, xk != xk | sK95(xk) = sz00 | sK95(xk) = sz10, inference(resolution, [status(thm)], [d7,d26])). % 122.15/33.09 cnf(d28, plain, X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X0) | sdtpldt0(sz10,sK33(sz10,X0)) = X0 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10), inference(resolution, [status(thm)], [c44,c25])). % 122.15/33.09 cnf(d29, plain, X0 = sz00 | X0 = sz10 | sdtpldt0(sz10,sK33(sz10,X0)) = X0 | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c1,d28])). % 122.15/33.09 cnf(d30, plain, xk = sz00 | xk = sz10 | sdtpldt0(sz10,sK33(sz10,xk)) = xk, inference(resolution, [status(thm)], [d29,c67])). % 122.15/33.09 cnf(d31, plain, sdtpldt0(sz10,sK33(sz10,xk)) = xk | xk = sz10, inference(resolution, [status(thm)], [c78,d30])). % 122.15/33.09 cnf(d32, plain, sdtpldt0(sz10,sK33(sz10,xk)) = xk, inference(resolution, [status(thm)], [c79,d31])). % 122.15/33.09 cnf(d33, plain, sK95(X0) = sdtasdt0(sz10,sK95(X0)) | 'Ts92'(X0), inference(resolution, [status(thm)], [c12,c91])). % 122.15/33.09 cnf(d34, plain, sK95(xk) = sdtasdt0(sz10,sK95(xk)), inference(resolution, [status(thm)], [d7,d33])). % 122.15/33.09 cnf(d35, plain, X0 != sK95(xk) | ~aNaturalNumber0(sK95(xk)) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | doDivides0(sz10,X0), inference(superposition, [status(thm)], [d34,c49])). % 122.15/33.09 cnf(d36, plain, X0 != sK95(xk) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK95(xk)) | doDivides0(sz10,X0), inference(resolution, [status(thm)], [c1,d35])). % 122.15/33.09 cnf(d37, plain, ~aNaturalNumber0(sK95(xk)) | ~aNaturalNumber0(sK95(xk)) | doDivides0(sz10,sK95(xk)), inference(equality_resolution, [status(thm)], [d36])). % 122.15/33.09 cnf(d38, plain, ~aNaturalNumber0(sK95(xk)) | ~aNaturalNumber0(xk) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(sK95(xk)) | doDivides0(sz10,xk) | 'Ts92'(xk), inference(resolution, [status(thm)], [d37,d16])). % 122.15/33.09 cnf(d39, plain, ~aNaturalNumber0(xk) | ~aNaturalNumber0(sK95(xk)) | doDivides0(sz10,xk) | 'Ts92'(xk), inference(resolution, [status(thm)], [c1,d38])). % 122.15/33.09 cnf(d40, plain, ~aNaturalNumber0(sK95(xk)) | doDivides0(sz10,xk) | 'Ts92'(xk), inference(resolution, [status(thm)], [c67,d39])). % 122.15/33.09 cnf(d41, plain, ~aNaturalNumber0(sK95(xk)) | doDivides0(sz10,xk), inference(resolution, [status(thm)], [d7,d40])). % 122.15/33.09 cnf(d42, plain, doDivides0(sz10,xk) | 'Ts92'(xk), inference(resolution, [status(thm)], [d41,c91])). % 122.15/33.09 cnf(d43, plain, doDivides0(sz10,xk), inference(resolution, [status(thm)], [d7,d42])). % 122.15/33.09 cnf(d44, plain, xk = sz00 | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(xk) | sdtlseqdt0(sz10,xk), inference(resolution, [status(thm)], [d43,c56])). % 122.15/33.09 cnf(d45, plain, xk = sz00 | ~aNaturalNumber0(xk) | sdtlseqdt0(sz10,xk), inference(resolution, [status(thm)], [c1,d44])). % 122.15/33.09 cnf(d46, plain, xk = sz00 | sdtlseqdt0(sz10,xk), inference(resolution, [status(thm)], [c67,d45])). % 122.15/33.09 cnf(d47, plain, sdtlseqdt0(sz10,xk), inference(resolution, [status(thm)], [c78,d46])). % 122.15/33.09 cnf(d48, plain, sdtpldt0(sz10,sK33(sz10,xk)) = xk | ~aNaturalNumber0(xk) | ~aNaturalNumber0(sz10), inference(resolution, [status(thm)], [d47,c25])). % 122.15/33.09 cnf(d49, plain, xk = xk | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(xk), inference(demodulation, [status(thm)], [d48,d32])). % 122.15/33.09 cnf(d50, plain, xk = xk | ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [c1,d49])). % 122.15/33.09 cnf(d51, plain, xk = xk, inference(resolution, [status(thm)], [c67,d50])). % 122.15/33.09 cnf(d52, plain, sK95(xk) = sz00 | sK95(xk) = sz10, inference(resolution, [status(thm)], [d51,d27])). % 122.15/33.09 cnf(d53, plain, sz10 != sz10 | 'Ts92'(xk) | sK95(xk) = sz00, inference(superposition, [status(thm)], [d52,c95])). % 122.15/33.09 cnf(d54, plain, sz10 != sz10 | sK95(xk) = sz00, inference(resolution, [status(thm)], [d7,d53])). % 122.15/33.09 cnf(d55, plain, sdtasdt0(sz10,sz10) = sz10, inference(resolution, [status(thm)], [c11,c1])). % 122.15/33.09 cnf(d56, plain, ~aNaturalNumber0(X0) | sdtpldt0(X0,sK33(X0,X0)) = X0 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c30,c25])). % 122.15/33.09 cnf(d57, plain, sdtpldt0(sz10,sK33(sz10,sz10)) = sz10, inference(resolution, [status(thm)], [d56,c1])). % 122.15/33.09 cnf(d58, plain, X0 = sz00 | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | sdtpldt0(X1,sK33(X1,sdtasdt0(X1,X0))) = sdtasdt0(X1,X0) | ~aNaturalNumber0(sdtasdt0(X1,X0)) | ~aNaturalNumber0(X1), inference(resolution, [status(thm)], [c45,c25])). % 122.15/33.09 cnf(d59, plain, sz10 = sdtasdt0(sz10,sz10), inference(resolution, [status(thm)], [c12,c1])). % 122.15/33.09 cnf(d60, plain, ~aNaturalNumber0(sz10) | sz10 = sz00 | sdtpldt0(sz10,sK33(sz10,sdtasdt0(sz10,sz10))) = sdtasdt0(sz10,sz10) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(sz10), inference(superposition, [status(thm)], [d59,d58])). % 122.15/33.09 cnf(d61, plain, sz10 = sz00 | sdtpldt0(sz10,sK33(sz10,sz10)) = sdtasdt0(sz10,sz10) | ~aNaturalNumber0(sz10), inference(demodulation, [status(thm)], [d60,d55])). % 122.15/33.09 cnf(d62, plain, sz10 = sz00 | sz10 = sdtasdt0(sz10,sz10) | ~aNaturalNumber0(sz10), inference(demodulation, [status(thm)], [d61,d57])). % 122.15/33.09 cnf(d63, plain, sz10 = sz00 | sz10 = sz10 | ~aNaturalNumber0(sz10), inference(demodulation, [status(thm)], [d62,d55])). % 122.15/33.09 cnf(d64, plain, sz10 = sz00 | sz10 = sz10, inference(resolution, [status(thm)], [c1,d63])). % 122.15/33.09 cnf(d65, plain, sz10 = sz10, inference(resolution, [status(thm)], [c2,d64])). % 122.15/33.09 cnf(d66, plain, sK95(xk) = sz00, inference(resolution, [status(thm)], [d65,d54])). % 122.15/33.09 cnf(d67, plain, xk = sdtasdt0(sK95(xk),sK96(xk)), inference(resolution, [status(thm)], [d7,c93])). % 122.15/33.09 cnf(d68, plain, sdtasdt0(X0,sK95(X1)) = sdtasdt0(sK95(X1),X0) | ~aNaturalNumber0(X0) | 'Ts92'(X1), inference(resolution, [status(thm)], [c9,c91])). % 122.15/33.09 cnf(d69, plain, sdtasdt0(sK96(X0),sK95(X1)) = sdtasdt0(sK95(X1),sK96(X0)) | 'Ts92'(X1) | 'Ts92'(X0), inference(resolution, [status(thm)], [d68,c92])). % 122.15/33.09 cnf(d70, plain, sdtasdt0(sK96(X0),sK95(X0)) = sdtasdt0(sK95(X0),sK96(X0)) | 'Ts92'(X0), inference(factoring, [status(thm)], [d69])). % 122.15/33.09 cnf(d71, plain, sdtasdt0(sK96(xk),sK95(xk)) = sdtasdt0(sK95(xk),sK96(xk)), inference(resolution, [status(thm)], [d7,d70])). % 122.15/33.09 cnf(d72, plain, sdtasdt0(sK96(xk),sK95(xk)) = xk, inference(demodulation, [status(thm)], [d71,d67])). % 122.15/33.09 cnf(d73, plain, sdtasdt0(sK96(xk),sz00) = xk, inference(demodulation, [status(thm)], [d72,d66])). % 122.15/33.09 cnf(d74, plain, sz00 = xk, inference(demodulation, [status(thm)], [d73,d8])). % 122.15/33.09 cnf(d75, plain, sz00 != xk | 'Ts92'(xk), inference(superposition, [status(thm)], [d66,c96])). % 122.15/33.09 cnf(d76, plain, sz00 != xk, inference(resolution, [status(thm)], [d7,d75])). % 122.15/33.09 cnf(d77, plain, $false, inference(resolution, [status(thm)], [d76,d74])). % 122.15/33.09 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------