%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM481+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 : n014.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 164.63s 35.82s % Output : CNFRefutation 164.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM481+3 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/5.38 % Computer : n014.cluster.edu % 0.12/5.38 % Model : x86_64 x86_64 % 0.12/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/5.38 % Memory : 8046.5625MB % 0.12/5.38 % OS : Linux 6.8.0-71-generic % 0.12/5.38 % CPULimit : 300 % 0.12/5.38 % WCLimit : 300 % 0.12/5.38 % DateTime : Sat Sep 26 02:55:38 UTC 2026 % 0.12/5.38 % CPUTime : % 0.12/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 164.63/35.82 % SZS status Theorem for theBenchmark.p % 164.63/35.82 % SZS output start CNFRefutation for theBenchmark.p % 164.63/35.82 fof(mSortsC, axiom, aNaturalNumber0(sz00)). % 164.63/35.82 fof(mSortsC_01, axiom, (aNaturalNumber0(sz10) & sz10 != sz00)). % 164.63/35.82 fof(mSortsB_02, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => aNaturalNumber0(sdtasdt0(X0,X1))))). % 164.63/35.82 fof(mMulComm, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => sdtasdt0(X0,X1) = sdtasdt0(X1,X0)))). % 164.63/35.82 fof(mMulAsso, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))))). % 164.63/35.82 fof(m_MulUnit, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz10) = X0 & X0 = sdtasdt0(sz10,X0))))). % 164.63/35.82 fof(m_MulZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 164.63/35.82 fof(mLEAsym, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X0)) => X0 = X1)))). % 164.63/35.82 fof(mLENTr, axiom, ! [X0] : ((aNaturalNumber0(X0) => (X0 = sz00 | (X0 = sz10 | (sz10 != X0 & sdtlseqdt0(sz10,X0))))))). % 164.63/35.82 fof(mIH_03, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((X0 != X1 & sdtlseqdt0(X0,X1)) => iLess0(X0,X1))))). % 164.63/35.82 fof(mDefDiv, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (doDivides0(X0,X1) <=> ? [X2] : ((aNaturalNumber0(X2) & X1 = sdtasdt0(X0,X2))))))). % 164.63/35.82 fof(mDivTrans, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => ((doDivides0(X0,X1) & doDivides0(X1,X2)) => doDivides0(X0,X2))))). % 164.63/35.82 fof(mDivLE, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((doDivides0(X0,X1) & X1 != sz00) => sdtlseqdt0(X0,X1))))). % 164.63/35.82 fof(m__, conjecture, ! [X0] : (((aNaturalNumber0(X0) & (X0 != sz00 & X0 != sz10)) => (! [X1] : (((aNaturalNumber0(X1) & (X1 != sz00 & X1 != sz10)) => (iLess0(X1,X0) => ? [X2] : ((aNaturalNumber0(X2) & (? [X3] : ((aNaturalNumber0(X3) & X1 = sdtasdt0(X2,X3))) & (doDivides0(X2,X1) & (X2 != sz00 & (X2 != sz10 & (! [X3] : (((aNaturalNumber0(X3) & (? [X4] : ((aNaturalNumber0(X4) & X2 = sdtasdt0(X3,X4))) | doDivides0(X3,X2))) => (X3 = sz10 | X3 = X2))) & isPrime0(X2))))))))))) => ? [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))))))))). % 164.63/35.82 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((aNaturalNumber0(X0) & (X0 != sz00 & X0 != sz10)) => (! [X1] : (((aNaturalNumber0(X1) & (X1 != sz00 & X1 != sz10)) => (iLess0(X1,X0) => ? [X2] : ((aNaturalNumber0(X2) & (? [X3] : ((aNaturalNumber0(X3) & X1 = sdtasdt0(X2,X3))) & (doDivides0(X2,X1) & (X2 != sz00 & (X2 != sz10 & (! [X3] : (((aNaturalNumber0(X3) & (? [X4] : ((aNaturalNumber0(X4) & X2 = sdtasdt0(X3,X4))) | doDivides0(X3,X2))) => (X3 = sz10 | X3 = X2))) & isPrime0(X2))))))))))) => ? [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)))))))), inference(negate_conjecture, [status(cth)], [m__])). % 164.63/35.82 cnf(c0, plain, aNaturalNumber0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 164.63/35.82 cnf(c1, plain, aNaturalNumber0(sz10), inference(clausification, [status(esa)], [mSortsC_01])). % 164.63/35.82 cnf(c2, plain, sz10 != sz00, inference(clausification, [status(esa)], [mSortsC_01])). % 164.63/35.82 cnf(c4, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | aNaturalNumber0(sdtasdt0(X0,X1)), inference(clausification, [status(esa)], [mSortsB_02])). % 164.63/35.82 cnf(c9, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtasdt0(X0,X1) = sdtasdt0(X1,X0), inference(clausification, [status(esa)], [mMulComm])). % 164.63/35.82 cnf(c10, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2) | sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)), inference(clausification, [status(esa)], [mMulAsso])). % 164.63/35.82 cnf(c11, plain, ~aNaturalNumber0(X0) | sdtasdt0(X0,sz10) = X0, inference(clausification, [status(esa)], [m_MulUnit])). % 164.63/35.82 cnf(c13, plain, ~aNaturalNumber0(X0) | sdtasdt0(X0,sz00) = sz00, inference(clausification, [status(esa)], [m_MulZero])). % 164.63/35.82 cnf(c14, plain, ~aNaturalNumber0(X0) | sz00 = sdtasdt0(sz00,X0), inference(clausification, [status(esa)], [m_MulZero])). % 164.63/35.82 cnf(c31, plain, ~sdtlseqdt0(X0,X1) | ~sdtlseqdt0(X1,X0) | ~aNaturalNumber0(X0) | X0 = X1 | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mLEAsym])). % 164.63/35.82 cnf(c44, plain, ~aNaturalNumber0(X0) | X0 = sz00 | X0 = sz10 | sdtlseqdt0(sz10,X0), inference(clausification, [status(esa)], [mLENTr])). % 164.63/35.82 cnf(c46, plain, ~aNaturalNumber0(X0) | X1 = X0 | iLess0(X1,X0) | ~sdtlseqdt0(X1,X0) | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mIH_03])). % 164.63/35.82 cnf(c47, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~doDivides0(X0,X1) | aNaturalNumber0(sK61(X0,X1)), inference(clausification, [status(esa)], [mDefDiv])). % 164.63/35.82 cnf(c48, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~doDivides0(X0,X1) | X1 = sdtasdt0(X0,sK61(X0,X1)), inference(clausification, [status(esa)], [mDefDiv])). % 164.63/35.82 cnf(c53, plain, ~doDivides0(X0,X1) | ~aNaturalNumber0(X0) | doDivides0(X0,X2) | ~doDivides0(X1,X2) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2), inference(clausification, [status(esa)], [mDivTrans])). % 164.63/35.82 cnf(c56, plain, ~aNaturalNumber0(X0) | X1 = sz00 | sdtlseqdt0(X0,X1) | ~doDivides0(X0,X1) | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mDivLE])). % 164.63/35.82 cnf(c67, plain, aNaturalNumber0(sK86), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c68, plain, sK86 != sz00, inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c69, plain, sK86 != sz10, inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c70, plain, ~aNaturalNumber0(X0) | X0 = sz10 | X1(X0) | X0 = sz00 | ~iLess0(X0,sK86), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c71, plain, ~aNaturalNumber0(X0) | X0 = sz00 | ~aNaturalNumber0(X1) | sK86 != sdtasdt0(X0,X1) | X0 = sz10 | ~X2(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c72, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sK86 != sdtasdt0(X0,X1) | ~isPrime0(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c73, plain, ~aNaturalNumber0(X0) | ~doDivides0(X0,sK86) | X0 = sz00 | X0 = sz10 | ~X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c74, plain, ~aNaturalNumber0(X0) | ~doDivides0(X0,sK86) | ~isPrime0(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c75, plain, ~X0(X1) | aNaturalNumber0(sK90(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c78, plain, ~X0(X1) | doDivides0(sK90(X1),X1), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c83, plain, ~X0(X1) | isPrime0(sK90(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c84, plain, X0(X1) | aNaturalNumber0(sK94(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c85, plain, X0(X1) | aNaturalNumber0(sK95(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c86, plain, X0(X1) | X1 = sdtasdt0(sK94(X1),sK95(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c87, plain, X0(X1) | doDivides0(sK94(X1),X1), inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c88, plain, X0(X1) | sK94(X1) != sz10, inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(c89, plain, X0(X1) | sK94(X1) != X1, inference(clausification, [status(esa)], [negated_conjecture])). % 164.63/35.82 cnf(d0, plain, X0 = sz00 | ~aNaturalNumber0(sK94(X0)) | ~aNaturalNumber0(X0) | sdtlseqdt0(sK94(X0),X0) | 'Ts85'(X0), inference(resolution, [status(thm)], [c56,c87])). % 164.63/35.82 cnf(d1, plain, X0 = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK94(X0)) | 'Ts85'(X0) | sK94(X0) = X0 | ~aNaturalNumber0(sK94(X0)) | ~aNaturalNumber0(X0) | iLess0(sK94(X0),X0), inference(resolution, [status(thm)], [d0,c46])). % 164.63/35.82 cnf(d2, plain, sK86 = sz00 | sK94(sK86) = sK86 | ~aNaturalNumber0(sK86) | ~aNaturalNumber0(sK94(sK86)) | 'Ts85'(sK86) | sK94(sK86) = sz00 | sK94(sK86) = sz10 | ~aNaturalNumber0(sK94(sK86)) | 'Ts84'(sK94(sK86)), inference(resolution, [status(thm)], [d1,c70])). % 164.63/35.82 cnf(d3, plain, sK86 = sz00 | sK94(sK86) = sz00 | sK94(sK86) = sz10 | sK94(sK86) = sK86 | ~aNaturalNumber0(sK94(sK86)) | 'Ts84'(sK94(sK86)) | 'Ts85'(sK86), inference(resolution, [status(thm)], [c67,d2])). % 164.63/35.82 cnf(d4, plain, sK94(sK86) = sz00 | sK94(sK86) = sz10 | sK94(sK86) = sK86 | ~aNaturalNumber0(sK94(sK86)) | 'Ts84'(sK94(sK86)) | 'Ts85'(sK86), inference(resolution, [status(thm)], [c68,d3])). % 164.63/35.82 cnf(d5, plain, sK86 != X0 | X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(X0) | ~'Ts85'(X0) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c11,c71])). % 164.63/35.82 cnf(d6, plain, X0 = sz00 | X0 = sz10 | sK86 != X0 | ~aNaturalNumber0(X0) | ~'Ts85'(X0), inference(resolution, [status(thm)], [c1,d5])). % 164.63/35.82 cnf(d7, plain, sK86 = sz00 | sK86 = sz10 | ~aNaturalNumber0(sK86) | ~'Ts85'(sK86), inference(equality_resolution, [status(thm)], [d6])). % 164.63/35.82 cnf(d8, plain, sK86 = sz00 | sK86 = sz10 | ~'Ts85'(sK86), inference(resolution, [status(thm)], [c67,d7])). % 164.63/35.82 cnf(d9, plain, sK86 = sz10 | ~'Ts85'(sK86), inference(resolution, [status(thm)], [c68,d8])). % 164.63/35.82 cnf(d10, plain, ~'Ts85'(sK86), inference(resolution, [status(thm)], [c69,d9])). % 164.63/35.82 cnf(d11, plain, sK94(sK86) = sz00 | sK94(sK86) = sz10 | sK94(sK86) = sK86 | ~aNaturalNumber0(sK94(sK86)) | 'Ts84'(sK94(sK86)), inference(resolution, [status(thm)], [d10,d4])). % 164.63/35.82 cnf(d12, plain, sK86 != sK86 | 'Ts85'(sK86) | sK94(sK86) = sz00 | sK94(sK86) = sz10 | ~aNaturalNumber0(sK94(sK86)) | 'Ts84'(sK94(sK86)), inference(superposition, [status(thm)], [d11,c89])). % 164.63/35.82 cnf(d13, plain, sK86 != sK86 | sK94(sK86) = sz00 | sK94(sK86) = sz10 | ~aNaturalNumber0(sK94(sK86)) | 'Ts84'(sK94(sK86)), inference(resolution, [status(thm)], [d10,d12])). % 164.63/35.82 cnf(d14, plain, sK94(sK86) = sz00 | sK94(sK86) = sz10 | ~aNaturalNumber0(sK94(sK86)) | 'Ts84'(sK94(sK86)), inference(equality_resolution, [status(thm)], [d13])). % 164.63/35.82 cnf(d15, plain, sK86 != sdtasdt0(X1,X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~isPrime0(X0) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1), inference(superposition, [status(thm)], [c9,c72])). % 164.63/35.82 cnf(d16, plain, sK86 != sdtasdt0(X0,sdtasdt0(X1,X2)) | ~aNaturalNumber0(sdtasdt0(X0,X1)) | ~aNaturalNumber0(X2) | ~isPrime0(X2) | ~aNaturalNumber0(X2) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c10,d15])). % 164.63/35.82 cnf(d17, plain, sK86 != sdtasdt0(X2,sdtasdt0(X1,X0)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X2) | ~aNaturalNumber0(sdtasdt0(X2,X0)) | ~isPrime0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1), inference(superposition, [status(thm)], [c9,d16])). % 164.63/35.82 cnf(d18, plain, sK86 != sdtasdt0(X1,sz00) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(sdtasdt0(X1,sz00)) | ~isPrime0(X0) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c13,d17])). % 164.63/35.82 cnf(d19, plain, sK86 != sdtasdt0(X0,sz00) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(sdtasdt0(X0,sz00)) | ~isPrime0(X1), inference(resolution, [status(thm)], [c0,d18])). % 164.63/35.82 cnf(d20, plain, sK86 != sdtasdt0(sz00,X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtasdt0(X0,sz00)) | ~isPrime0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz00), inference(superposition, [status(thm)], [c9,d19])). % 164.63/35.82 cnf(d21, plain, sK86 != sdtasdt0(sz00,X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtasdt0(X0,sz00)) | ~isPrime0(X1), inference(resolution, [status(thm)], [c0,d20])). % 164.63/35.82 cnf(d22, plain, sK86 != X0 | ~aNaturalNumber0(X1) | ~aNaturalNumber0(sK61(sz00,X0)) | ~aNaturalNumber0(sdtasdt0(sK61(sz00,X0),sz00)) | ~isPrime0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz00) | ~doDivides0(sz00,X0), inference(superposition, [status(thm)], [c48,d21])). % 164.63/35.82 cnf(d23, plain, sK86 != X0 | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtasdt0(sK61(sz00,X0),sz00)) | ~aNaturalNumber0(sK61(sz00,X0)) | ~doDivides0(sz00,X0) | ~isPrime0(X1), inference(resolution, [status(thm)], [c0,d22])). % 164.63/35.82 cnf(d24, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK86) | ~aNaturalNumber0(sdtasdt0(sK61(sz00,sK86),sz00)) | ~aNaturalNumber0(sK61(sz00,sK86)) | ~doDivides0(sz00,sK86) | ~isPrime0(X0), inference(equality_resolution, [status(thm)], [d23])). % 164.63/35.82 cnf(d25, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtasdt0(sK61(sz00,sK86),sz00)) | ~aNaturalNumber0(sK61(sz00,sK86)) | ~doDivides0(sz00,sK86) | ~isPrime0(X0), inference(resolution, [status(thm)], [c67,d24])). % 164.63/35.82 cnf(d26, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK61(sz00,sK86)) | ~doDivides0(sz00,sK86) | ~isPrime0(X0) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(sK61(sz00,sK86)), inference(resolution, [status(thm)], [d25,c4])). % 164.63/35.82 cnf(d27, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK61(sz00,sK86)) | ~doDivides0(sz00,sK86) | ~isPrime0(X0), inference(resolution, [status(thm)], [c0,d26])). % 164.63/35.82 cnf(d28, plain, ~aNaturalNumber0(X0) | ~doDivides0(sz00,sK86) | ~isPrime0(X0) | ~aNaturalNumber0(sK86) | ~aNaturalNumber0(sz00) | ~doDivides0(sz00,sK86), inference(resolution, [status(thm)], [d27,c47])). % 164.63/35.82 cnf(d29, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz00) | ~doDivides0(sz00,sK86) | ~isPrime0(X0), inference(resolution, [status(thm)], [c67,d28])). % 164.63/35.82 cnf(d30, plain, ~aNaturalNumber0(X0) | ~doDivides0(sz00,sK86) | ~isPrime0(X0), inference(resolution, [status(thm)], [c0,d29])). % 164.63/35.82 cnf(d31, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK94(X1)) | ~aNaturalNumber0(X1) | ~doDivides0(X0,sK94(X1)) | doDivides0(X0,X1) | 'Ts85'(X1), inference(resolution, [status(thm)], [c53,c87])). % 164.63/35.82 cnf(d32, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK90(sK94(X0))) | ~aNaturalNumber0(sK94(X0)) | doDivides0(sK90(sK94(X0)),X0) | 'Ts85'(X0) | ~'Ts84'(sK94(X0)), inference(resolution, [status(thm)], [d31,c78])). % 164.63/35.82 cnf(d33, plain, ~aNaturalNumber0(sK86) | ~aNaturalNumber0(sK90(sK94(sK86))) | ~aNaturalNumber0(sK94(sK86)) | ~'Ts84'(sK94(sK86)) | 'Ts85'(sK86) | ~aNaturalNumber0(sK90(sK94(sK86))) | ~isPrime0(sK90(sK94(sK86))), inference(resolution, [status(thm)], [d32,c74])). % 164.63/35.82 cnf(d34, plain, ~aNaturalNumber0(sK90(sK94(sK86))) | ~aNaturalNumber0(sK94(sK86)) | ~isPrime0(sK90(sK94(sK86))) | ~'Ts84'(sK94(sK86)) | 'Ts85'(sK86), inference(resolution, [status(thm)], [c67,d33])). % 164.63/35.82 cnf(d35, plain, ~aNaturalNumber0(sK90(sK94(sK86))) | ~aNaturalNumber0(sK94(sK86)) | ~isPrime0(sK90(sK94(sK86))) | ~'Ts84'(sK94(sK86)), inference(resolution, [status(thm)], [d10,d34])). % 164.63/35.82 cnf(d36, plain, ~aNaturalNumber0(sK90(sK94(sK86))) | ~aNaturalNumber0(sK94(sK86)) | ~'Ts84'(sK94(sK86)) | ~'Ts84'(sK94(sK86)), inference(resolution, [status(thm)], [d35,c83])). % 164.63/35.82 cnf(d37, plain, ~aNaturalNumber0(sK94(sK86)) | ~'Ts84'(sK94(sK86)) | ~'Ts84'(sK94(sK86)), inference(resolution, [status(thm)], [d36,c75])). % 164.63/35.82 cnf(d38, plain, sK94(sK86) = sz00 | sK94(sK86) = sz10 | ~aNaturalNumber0(sK94(sK86)) | ~'Ts85'(sK94(sK86)) | 'Ts85'(sK86), inference(resolution, [status(thm)], [c73,c87])). % 164.63/35.82 cnf(d39, plain, sz10 != sz10 | 'Ts85'(sK86) | sK94(sK86) = sz00 | ~aNaturalNumber0(sK94(sK86)) | 'Ts85'(sK86) | ~'Ts85'(sK94(sK86)), inference(superposition, [status(thm)], [d38,c88])). % 164.63/35.82 cnf(d40, plain, sK94(sK86) = sz00 | ~aNaturalNumber0(sK94(sK86)) | 'Ts85'(sK86) | ~'Ts85'(sK94(sK86)), inference(equality_resolution, [status(thm)], [d39])). % 164.63/35.82 cnf(d41, plain, doDivides0(sz00,sK86) | 'Ts85'(sK86) | ~aNaturalNumber0(sK94(sK86)) | 'Ts85'(sK86) | ~'Ts85'(sK94(sK86)), inference(superposition, [status(thm)], [d40,c87])). % 164.63/35.82 cnf(d42, plain, ~aNaturalNumber0(sK94(sK86)) | doDivides0(sz00,sK86) | ~'Ts85'(sK94(sK86)), inference(resolution, [status(thm)], [d10,d41])). % 164.63/35.82 cnf(d43, plain, ~'Ts85'(sz10) | ~aNaturalNumber0(sK94(sK86)) | doDivides0(sz00,sK86) | sK94(sK86) = sz00 | ~aNaturalNumber0(sK94(sK86)) | 'Ts84'(sK94(sK86)), inference(superposition, [status(thm)], [d14,d42])). % 164.63/35.82 cnf(d44, plain, X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X0) | X0 = sz10 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | ~sdtlseqdt0(X0,sz10), inference(resolution, [status(thm)], [c44,c31])). % 164.63/35.82 cnf(d45, plain, X0 = sz00 | X0 = sz10 | ~aNaturalNumber0(X0) | ~sdtlseqdt0(X0,sz10), inference(resolution, [status(thm)], [c1,d44])). % 164.63/35.82 cnf(d46, plain, sK94(sz10) = sz00 | sK94(sz10) = sz10 | ~aNaturalNumber0(sK94(sz10)) | sz10 = sz00 | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(sK94(sz10)) | 'Ts85'(sz10), inference(resolution, [status(thm)], [d45,d0])). % 164.63/35.82 cnf(d47, plain, sz10 = sz00 | sK94(sz10) = sz00 | sK94(sz10) = sz10 | ~aNaturalNumber0(sK94(sz10)) | 'Ts85'(sz10), inference(resolution, [status(thm)], [c1,d46])). % 164.63/35.82 cnf(d48, plain, sK94(sz10) = sz00 | sK94(sz10) = sz10 | ~aNaturalNumber0(sK94(sz10)) | 'Ts85'(sz10), inference(resolution, [status(thm)], [c2,d47])). % 164.63/35.82 cnf(d49, plain, sz10 != sz10 | 'Ts85'(sz10) | sK94(sz10) = sz00 | ~aNaturalNumber0(sK94(sz10)) | 'Ts85'(sz10), inference(superposition, [status(thm)], [d48,c88])). % 164.63/35.82 cnf(d50, plain, sK94(sz10) = sz00 | ~aNaturalNumber0(sK94(sz10)) | 'Ts85'(sz10), inference(equality_resolution, [status(thm)], [d49])). % 164.63/35.82 cnf(d51, plain, sz10 = sdtasdt0(sz00,sK95(sz10)) | 'Ts85'(sz10) | ~aNaturalNumber0(sK94(sz10)) | 'Ts85'(sz10), inference(superposition, [status(thm)], [d50,c86])). % 164.63/35.82 cnf(d52, plain, sz00 = sz10 | ~aNaturalNumber0(sK95(sz10)) | ~aNaturalNumber0(sK94(sz10)) | 'Ts85'(sz10), inference(superposition, [status(thm)], [d51,c14])). % 164.63/35.82 cnf(d53, plain, sz00 = sz10 | ~aNaturalNumber0(sK94(sz10)) | 'Ts85'(sz10) | 'Ts85'(sz10), inference(resolution, [status(thm)], [d52,c85])). % 164.63/35.82 cnf(d54, plain, sz00 = sz10 | 'Ts85'(sz10) | 'Ts85'(sz10), inference(resolution, [status(thm)], [d53,c84])). % 164.63/35.82 cnf(d55, plain, sz00 != sz00 | 'Ts85'(sz10), inference(superposition, [status(thm)], [d54,c2])). % 164.63/35.82 cnf(d56, plain, 'Ts85'(sz10), inference(equality_resolution, [status(thm)], [d55])). % 164.63/35.82 cnf(d57, plain, sK94(sK86) = sz00 | ~aNaturalNumber0(sK94(sK86)) | doDivides0(sz00,sK86) | 'Ts84'(sK94(sK86)), inference(resolution, [status(thm)], [d56,d43])). % 164.63/35.82 cnf(d58, plain, doDivides0(sz00,sK86) | 'Ts85'(sK86) | ~aNaturalNumber0(sK94(sK86)) | doDivides0(sz00,sK86) | 'Ts84'(sK94(sK86)), inference(superposition, [status(thm)], [d57,c87])). % 164.63/35.82 cnf(d59, plain, ~aNaturalNumber0(sK94(sK86)) | doDivides0(sz00,sK86) | 'Ts84'(sK94(sK86)), inference(resolution, [status(thm)], [d10,d58])). % 164.63/35.82 cnf(d60, plain, doDivides0(sz00,sK86) | 'Ts84'(sK94(sK86)) | 'Ts85'(sK86), inference(resolution, [status(thm)], [d59,c84])). % 164.63/35.82 cnf(d61, plain, doDivides0(sz00,sK86) | 'Ts84'(sK94(sK86)), inference(resolution, [status(thm)], [d10,d60])). % 164.63/35.82 cnf(d62, plain, doDivides0(sz00,sK86) | ~aNaturalNumber0(sK94(sK86)), inference(resolution, [status(thm)], [d61,d37])). % 164.63/35.82 cnf(d63, plain, doDivides0(sz00,sK86) | 'Ts85'(sK86), inference(resolution, [status(thm)], [d62,c84])). % 164.63/35.82 cnf(d64, plain, doDivides0(sz00,sK86), inference(resolution, [status(thm)], [d10,d63])). % 164.63/35.82 cnf(d65, plain, ~aNaturalNumber0(X0) | ~isPrime0(X0), inference(resolution, [status(thm)], [d64,d30])). % 164.63/35.82 cnf(d66, plain, ~aNaturalNumber0(sK90(X0)) | ~'Ts84'(X0), inference(resolution, [status(thm)], [d65,c83])). % 164.63/35.82 cnf(d67, plain, ~'Ts84'(X0) | ~'Ts84'(X0), inference(resolution, [status(thm)], [d66,c75])). % 164.63/35.82 cnf(d68, plain, sK94(sK86) = sz00 | sK94(sK86) = sz10 | ~aNaturalNumber0(sK94(sK86)), inference(resolution, [status(thm)], [d67,d14])). % 164.63/35.82 cnf(d69, plain, sz10 != sz10 | 'Ts85'(sK86) | sK94(sK86) = sz00 | ~aNaturalNumber0(sK94(sK86)), inference(superposition, [status(thm)], [d68,c88])). % 164.63/35.82 cnf(d70, plain, sz10 != sz10 | sK94(sK86) = sz00 | ~aNaturalNumber0(sK94(sK86)), inference(resolution, [status(thm)], [d10,d69])). % 164.63/35.82 cnf(d71, plain, sK94(sK86) = sz00 | ~aNaturalNumber0(sK94(sK86)), inference(equality_resolution, [status(thm)], [d70])). % 164.63/35.82 cnf(d72, plain, sK86 = sdtasdt0(sz00,sK95(sK86)) | 'Ts85'(sK86) | ~aNaturalNumber0(sK94(sK86)), inference(superposition, [status(thm)], [d71,c86])). % 164.63/35.82 cnf(d73, plain, sK86 = sdtasdt0(sz00,sK95(sK86)) | ~aNaturalNumber0(sK94(sK86)), inference(resolution, [status(thm)], [d10,d72])). % 164.63/35.82 cnf(d74, plain, sz00 = sK86 | ~aNaturalNumber0(sK95(sK86)) | ~aNaturalNumber0(sK94(sK86)), inference(superposition, [status(thm)], [d73,c14])). % 164.63/35.82 cnf(d75, plain, sz00 = sK86 | ~aNaturalNumber0(sK94(sK86)) | 'Ts85'(sK86), inference(resolution, [status(thm)], [d74,c85])). % 164.63/35.82 cnf(d76, plain, sz00 = sK86 | ~aNaturalNumber0(sK94(sK86)), inference(resolution, [status(thm)], [d10,d75])). % 164.63/35.82 cnf(d77, plain, sz00 = sK86 | 'Ts85'(sK86), inference(resolution, [status(thm)], [d76,c84])). % 164.63/35.82 cnf(d78, plain, sz00 = sK86, inference(resolution, [status(thm)], [d10,d77])). % 164.63/35.82 cnf(d79, plain, sz00 != sK86 | 'Ts85'(sK86) | ~aNaturalNumber0(sK94(sK86)), inference(superposition, [status(thm)], [d71,c89])). % 164.63/35.82 cnf(d80, plain, sz00 != sK86 | ~aNaturalNumber0(sK94(sK86)), inference(resolution, [status(thm)], [d10,d79])). % 164.63/35.82 cnf(d81, plain, ~aNaturalNumber0(sK94(sK86)), inference(resolution, [status(thm)], [d78,d80])). % 164.63/35.82 cnf(d82, plain, ~aNaturalNumber0(sK94(sz00)), inference(demodulation, [status(thm)], [d81,d78])). % 164.63/35.82 cnf(d83, plain, 'Ts85'(sz00), inference(resolution, [status(thm)], [d82,c84])). % 164.63/35.82 cnf(d84, plain, sK86 = sdtasdt0(sz00,sK95(sK86)) | 'Ts85'(sK86) | ~aNaturalNumber0(sK94(sK86)) | 'Ts85'(sK86) | ~'Ts85'(sK94(sK86)), inference(superposition, [status(thm)], [d40,c86])). % 164.63/35.82 cnf(d85, plain, sK86 = sdtasdt0(sz00,sK95(sK86)) | ~aNaturalNumber0(sK94(sK86)) | ~'Ts85'(sK94(sK86)), inference(resolution, [status(thm)], [d10,d84])). % 164.63/35.82 cnf(d86, plain, sK86 = sz00 | ~aNaturalNumber0(sK94(sK86)) | ~'Ts85'(sK94(sK86)) | ~aNaturalNumber0(sK95(sK86)), inference(superposition, [status(thm)], [c14,d85])). % 164.63/35.82 cnf(d87, plain, ~aNaturalNumber0(sK94(sK86)) | ~aNaturalNumber0(sK95(sK86)) | ~'Ts85'(sK94(sK86)), inference(resolution, [status(thm)], [c68,d86])). % 164.63/35.82 cnf(d88, plain, ~'Ts85'(sz10) | ~aNaturalNumber0(sK94(sK86)) | ~aNaturalNumber0(sK95(sK86)) | sK94(sK86) = sz00 | ~aNaturalNumber0(sK94(sK86)), inference(superposition, [status(thm)], [d68,d87])). % 164.63/35.82 cnf(d89, plain, sK94(sK86) = sz00 | ~aNaturalNumber0(sK94(sK86)) | ~aNaturalNumber0(sK95(sK86)), inference(resolution, [status(thm)], [d56,d88])). % 164.63/35.82 cnf(d90, plain, ~'Ts85'(sz00) | ~aNaturalNumber0(sK94(sK86)) | ~aNaturalNumber0(sK95(sK86)) | ~aNaturalNumber0(sK94(sK86)) | ~aNaturalNumber0(sK95(sK86)), inference(superposition, [status(thm)], [d89,d87])). % 164.63/35.82 cnf(d91, plain, ~aNaturalNumber0(sK94(sK86)) | ~'Ts85'(sz00) | 'Ts85'(sK86), inference(resolution, [status(thm)], [d90,c85])). % 164.63/35.82 cnf(d92, plain, ~aNaturalNumber0(sK94(sK86)) | ~'Ts85'(sz00), inference(resolution, [status(thm)], [d10,d91])). % 164.63/35.82 cnf(d93, plain, ~'Ts85'(sz00) | 'Ts85'(sK86), inference(resolution, [status(thm)], [d92,c84])). % 164.63/35.82 cnf(d94, plain, ~'Ts85'(sz00), inference(resolution, [status(thm)], [d10,d93])). % 164.63/35.82 cnf(d95, plain, $false, inference(resolution, [status(thm)], [d94,d83])). % 164.63/35.82 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------