%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM528+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 : n016.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:13:02 AM UTC 2026 % Result : Theorem 119.50s 37.83s % Output : CNFRefutation 119.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : NUM528+3 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.17/5.44 % Computer : n016.cluster.edu % 0.17/5.44 % Model : x86_64 x86_64 % 0.17/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/5.44 % Memory : 8046.5625MB % 0.17/5.44 % OS : Linux 6.8.0-71-generic % 0.17/5.44 % CPULimit : 300 % 0.17/5.44 % WCLimit : 300 % 0.17/5.44 % DateTime : Sat Sep 26 03:12:06 UTC 2026 % 0.17/5.44 % CPUTime : % 0.17/5.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 119.50/37.83 % SZS status Theorem for theBenchmark.p % 119.50/37.83 % SZS output start CNFRefutation for theBenchmark.p % 119.50/37.83 fof(mSortsC, axiom, aNaturalNumber0(sz00)). % 119.50/37.83 fof(mSortsC_01, axiom, (aNaturalNumber0(sz10) & sz10 != sz00)). % 119.50/37.83 fof(mSortsB, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => aNaturalNumber0(sdtpldt0(X0,X1))))). % 119.50/37.83 fof(mSortsB_02, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => aNaturalNumber0(sdtasdt0(X0,X1))))). % 119.50/37.83 fof(mAddComm, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => sdtpldt0(X0,X1) = sdtpldt0(X1,X0)))). % 119.50/37.83 fof(mAddAsso, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))))). % 119.50/37.83 fof(m_AddZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtpldt0(X0,sz00) = X0 & X0 = sdtpldt0(sz00,X0))))). % 119.50/37.83 fof(mMulComm, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => sdtasdt0(X0,X1) = sdtasdt0(X1,X0)))). % 119.50/37.83 fof(mMulAsso, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2))))). % 119.50/37.83 fof(m_MulUnit, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz10) = X0 & X0 = sdtasdt0(sz10,X0))))). % 119.50/37.83 fof(m_MulZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 119.50/37.83 fof(mAMDistr, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => (sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) & sdtasdt0(sdtpldt0(X1,X2),X0) = sdtpldt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)))))). % 119.50/37.83 fof(mMulCanc, axiom, ! [X0] : ((aNaturalNumber0(X0) => (X0 != sz00 => ! [X1] : ! [X2] : (((aNaturalNumber0(X1) & aNaturalNumber0(X2)) => ((sdtasdt0(X0,X1) = sdtasdt0(X0,X2) | sdtasdt0(X1,X0) = sdtasdt0(X2,X0)) => X1 = X2))))))). % 119.50/37.83 fof(mZeroMul, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (sdtasdt0(X0,X1) = sz00 => (X0 = sz00 | X1 = sz00))))). % 119.50/37.83 fof(mLERefl, axiom, ! [X0] : ((aNaturalNumber0(X0) => sdtlseqdt0(X0,X0)))). % 119.50/37.83 fof(mLEAsym, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X0)) => X0 = X1)))). % 119.50/37.83 fof(mLETotal, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (sdtlseqdt0(X0,X1) | (X1 != X0 & sdtlseqdt0(X1,X0)))))). % 119.50/37.83 fof(mMonMul2, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (X0 != sz00 => sdtlseqdt0(X1,sdtasdt0(X1,X0)))))). % 119.50/37.83 fof(m__2987, hypothesis, (aNaturalNumber0(xn) & (aNaturalNumber0(xm) & (aNaturalNumber0(xp) & (xn != sz00 & (xm != sz00 & xp != sz00)))))). % 119.50/37.83 fof(m__3014, hypothesis, sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn)). % 119.50/37.83 fof(m__3025, hypothesis, (xp != sz10 & (! [X0] : (((aNaturalNumber0(X0) & (? [X1] : ((aNaturalNumber0(X1) & xp = sdtasdt0(X0,X1))) | doDivides0(X0,xp))) => (X0 = sz10 | X0 = xp))) & isPrime0(xp)))). % 119.50/37.83 fof(m__3046, hypothesis, (? [X0] : ((aNaturalNumber0(X0) & sdtasdt0(xn,xn) = sdtasdt0(xp,X0))) & (doDivides0(xp,sdtasdt0(xn,xn)) & (? [X0] : ((aNaturalNumber0(X0) & xn = sdtasdt0(xp,X0))) & doDivides0(xp,xn))))). % 119.50/37.83 fof(m__3059, hypothesis, (aNaturalNumber0(xq) & (xn = sdtasdt0(xp,xq) & xq = sdtsldt0(xn,xp)))). % 119.50/37.83 fof(m__3152, hypothesis, ((? [X0] : ((aNaturalNumber0(X0) & sdtpldt0(xn,X0) = xm)) | sdtlseqdt0(xn,xm)) => (? [X0] : ((aNaturalNumber0(X0) & sdtpldt0(sdtasdt0(xn,xn),X0) = sdtasdt0(xm,xm))) & sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))))). % 119.50/37.83 fof(m__, conjecture, (xm != xn & (? [X0] : ((aNaturalNumber0(X0) & sdtpldt0(xm,X0) = xn)) | sdtlseqdt0(xm,xn)))). % 119.50/37.83 fof(negated_conjecture, negated_conjecture, ~((xm != xn & (? [X0] : ((aNaturalNumber0(X0) & sdtpldt0(xm,X0) = xn)) | sdtlseqdt0(xm,xn)))), inference(negate_conjecture, [status(cth)], [m__])). % 119.50/37.83 cnf(c0, plain, aNaturalNumber0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 119.50/37.83 cnf(c1, plain, aNaturalNumber0(sz10), inference(clausification, [status(esa)], [mSortsC_01])). % 119.50/37.83 cnf(c3, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | aNaturalNumber0(sdtpldt0(X0,X1)), inference(clausification, [status(esa)], [mSortsB])). % 119.50/37.83 cnf(c4, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | aNaturalNumber0(sdtasdt0(X0,X1)), inference(clausification, [status(esa)], [mSortsB_02])). % 119.50/37.83 cnf(c5, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtpldt0(X0,X1) = sdtpldt0(X1,X0), inference(clausification, [status(esa)], [mAddComm])). % 119.50/37.83 cnf(c6, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2) | sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)), inference(clausification, [status(esa)], [mAddAsso])). % 119.50/37.83 cnf(c7, plain, ~aNaturalNumber0(X0) | sdtpldt0(X0,sz00) = X0, inference(clausification, [status(esa)], [m_AddZero])). % 119.50/37.83 cnf(c9, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtasdt0(X0,X1) = sdtasdt0(X1,X0), inference(clausification, [status(esa)], [mMulComm])). % 119.50/37.83 cnf(c10, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2) | sdtasdt0(sdtasdt0(X0,X1),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)), inference(clausification, [status(esa)], [mMulAsso])). % 119.50/37.83 cnf(c11, plain, ~aNaturalNumber0(X0) | sdtasdt0(X0,sz10) = X0, inference(clausification, [status(esa)], [m_MulUnit])). % 119.50/37.83 cnf(c13, plain, ~aNaturalNumber0(X0) | sdtasdt0(X0,sz00) = sz00, inference(clausification, [status(esa)], [m_MulZero])). % 119.50/37.83 cnf(c14, plain, ~aNaturalNumber0(X0) | sz00 = sdtasdt0(sz00,X0), inference(clausification, [status(esa)], [m_MulZero])). % 119.50/37.83 cnf(c15, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2) | sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)), inference(clausification, [status(esa)], [mAMDistr])). % 119.50/37.83 cnf(c16, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2) | sdtasdt0(sdtpldt0(X1,X2),X0) = sdtpldt0(sdtasdt0(X1,X0),sdtasdt0(X2,X0)), inference(clausification, [status(esa)], [mAMDistr])). % 119.50/37.83 cnf(c19, plain, X0 = sz00 | ~aNaturalNumber0(X0) | sdtasdt0(X0,X1) != sdtasdt0(X0,X2) | ~aNaturalNumber0(X2) | ~aNaturalNumber0(X1) | X1 = X2, inference(clausification, [status(esa)], [mMulCanc])). % 119.50/37.83 cnf(c20, plain, X0 = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2) | X2 = X1 | sdtasdt0(X2,X0) != sdtasdt0(X1,X0), inference(clausification, [status(esa)], [mMulCanc])). % 119.50/37.83 cnf(c23, plain, X0 = sz00 | X1 = sz00 | ~aNaturalNumber0(X1) | sdtasdt0(X0,X1) != sz00 | ~aNaturalNumber0(X0), inference(clausification, [status(esa)], [mZeroMul])). % 119.50/37.83 cnf(c30, plain, ~aNaturalNumber0(X0) | sdtlseqdt0(X0,X0), inference(clausification, [status(esa)], [mLERefl])). % 119.50/37.83 cnf(c31, plain, ~sdtlseqdt0(X0,X1) | ~sdtlseqdt0(X1,X0) | ~aNaturalNumber0(X0) | X0 = X1 | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mLEAsym])). % 119.50/37.83 cnf(c34, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtlseqdt0(X0,X1) | sdtlseqdt0(X1,X0), inference(clausification, [status(esa)], [mLETotal])). % 119.50/37.83 cnf(c45, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | X0 = sz00 | sdtlseqdt0(X1,sdtasdt0(X1,X0)), inference(clausification, [status(esa)], [mMonMul2])). % 119.50/37.83 cnf(c71, plain, aNaturalNumber0(xn), inference(clausification, [status(esa)], [m__2987])). % 119.50/37.83 cnf(c72, plain, aNaturalNumber0(xm), inference(clausification, [status(esa)], [m__2987])). % 119.50/37.83 cnf(c73, plain, aNaturalNumber0(xp), inference(clausification, [status(esa)], [m__2987])). % 119.50/37.83 cnf(c75, plain, xm != sz00, inference(clausification, [status(esa)], [m__2987])). % 119.50/37.83 cnf(c76, plain, xp != sz00, inference(clausification, [status(esa)], [m__2987])). % 119.50/37.83 cnf(c85, plain, sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn), inference(clausification, [status(esa)], [m__3014])). % 119.50/37.83 cnf(c86, plain, xp != sz10, inference(clausification, [status(esa)], [m__3025])). % 119.50/37.83 cnf(c90, plain, aNaturalNumber0(sK97), inference(clausification, [status(esa)], [m__3046])). % 119.50/37.83 cnf(c91, plain, sdtasdt0(xn,xn) = sdtasdt0(xp,sK97), inference(clausification, [status(esa)], [m__3046])). % 119.50/37.83 cnf(c96, plain, aNaturalNumber0(xq), inference(clausification, [status(esa)], [m__3059])). % 119.50/37.83 cnf(c97, plain, xn = sdtasdt0(xp,xq), inference(clausification, [status(esa)], [m__3059])). % 119.50/37.83 cnf(c101, plain, ~sdtlseqdt0(xn,xm) | X0, inference(clausification, [status(esa)], [m__3152])). % 119.50/37.83 cnf(c102, plain, ~X0 | aNaturalNumber0(sK101), inference(clausification, [status(esa)], [m__3152])). % 119.50/37.83 cnf(c103, plain, ~X0 | sdtpldt0(sdtasdt0(xn,xn),sK101) = sdtasdt0(xm,xm), inference(clausification, [status(esa)], [m__3152])). % 119.50/37.83 cnf(c104, plain, ~X0 | sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)), inference(clausification, [status(esa)], [m__3152])). % 119.50/37.83 cnf(c106, plain, xm = xn | ~sdtlseqdt0(xm,xn), inference(clausification, [status(esa)], [negated_conjecture])). % 119.50/37.83 cnf(d0, plain, sdtasdt0(xn,xn) != sdtasdt0(xp,X0) | sdtasdt0(xm,xm) = X0 | xp = sz00 | ~aNaturalNumber0(sdtasdt0(xm,xm)) | ~aNaturalNumber0(xp) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c85,c19])). % 119.50/37.83 cnf(d1, plain, sdtasdt0(xn,xn) != sdtasdt0(xp,X0) | sdtasdt0(xm,xm) = X0 | xp = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtasdt0(xm,xm)), inference(resolution, [status(thm)], [c73,d0])). % 119.50/37.83 cnf(d2, plain, sdtasdt0(xn,xn) != sdtasdt0(xp,X0) | sdtasdt0(xm,xm) = X0 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtasdt0(xm,xm)), inference(resolution, [status(thm)], [c76,d1])). % 119.50/37.83 cnf(d3, plain, ~aNaturalNumber0(xn) | ~aNaturalNumber0(xm) | sdtlseqdt0(xn,xm) | xm = xn, inference(resolution, [status(thm)], [c34,c106])). % 119.50/37.83 cnf(d4, plain, xm = xn | ~aNaturalNumber0(xm) | sdtlseqdt0(xn,xm), inference(resolution, [status(thm)], [c71,d3])). % 119.50/37.83 cnf(d5, plain, xm = xn | sdtlseqdt0(xn,xm), inference(resolution, [status(thm)], [c72,d4])). % 119.50/37.83 cnf(d6, plain, xm = xn | 'Ts99', inference(resolution, [status(thm)], [d5,c101])). % 119.50/37.83 cnf(d7, plain, ~sdtlseqdt0(xn,xn) | 'Ts99' | 'Ts99', inference(superposition, [status(thm)], [d6,c101])). % 119.50/37.83 cnf(d8, plain, 'Ts99' | ~aNaturalNumber0(xn), inference(resolution, [status(thm)], [d7,c30])). % 119.50/37.83 cnf(d9, plain, 'Ts99', inference(resolution, [status(thm)], [c71,d8])). % 119.50/37.83 cnf(d10, plain, sdtpldt0(sdtasdt0(xn,xn),sK101) = sdtasdt0(xm,xm), inference(resolution, [status(thm)], [d9,c103])). % 119.50/37.83 cnf(d11, plain, aNaturalNumber0(sdtasdt0(xm,xm)) | ~aNaturalNumber0(sK101) | ~aNaturalNumber0(sdtasdt0(xn,xn)), inference(superposition, [status(thm)], [d10,c3])). % 119.50/37.83 cnf(d12, plain, aNaturalNumber0(sdtasdt0(xn,xn)) | ~aNaturalNumber0(sK97) | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [c91,c4])). % 119.50/37.83 cnf(d13, plain, aNaturalNumber0(sdtasdt0(xn,xn)) | ~aNaturalNumber0(sK97), inference(resolution, [status(thm)], [c73,d12])). % 119.50/37.83 cnf(d14, plain, aNaturalNumber0(sdtasdt0(xn,xn)), inference(resolution, [status(thm)], [c90,d13])). % 119.50/37.83 cnf(d15, plain, aNaturalNumber0(sdtasdt0(xm,xm)) | ~aNaturalNumber0(sK101), inference(resolution, [status(thm)], [d14,d11])). % 119.50/37.83 cnf(d16, plain, aNaturalNumber0(sK101), inference(resolution, [status(thm)], [d9,c102])). % 119.50/37.83 cnf(d17, plain, aNaturalNumber0(sdtasdt0(xm,xm)), inference(resolution, [status(thm)], [d16,d15])). % 119.50/37.83 cnf(d18, plain, sdtasdt0(xn,xn) != sdtasdt0(xp,X0) | sdtasdt0(xm,xm) = X0 | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [d17,d2])). % 119.50/37.83 cnf(d19, plain, sdtasdt0(xn,xn) != sdtasdt0(xn,xn) | sdtasdt0(xm,xm) = sK97 | ~aNaturalNumber0(sK97), inference(superposition, [status(thm)], [c91,d18])). % 119.50/37.83 cnf(d20, plain, sdtasdt0(xn,xn) != sdtasdt0(xn,xn) | sdtasdt0(xm,xm) = sK97, inference(resolution, [status(thm)], [c90,d19])). % 119.50/37.83 cnf(d21, plain, sdtasdt0(xp,sdtpldt0(xq,X0)) = sdtpldt0(xn,sdtasdt0(xp,X0)) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(xq) | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [c97,c15])). % 119.50/37.83 cnf(d22, plain, sdtasdt0(xp,sdtpldt0(xq,X0)) = sdtpldt0(xn,sdtasdt0(xp,X0)) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(xq), inference(resolution, [status(thm)], [c73,d21])). % 119.50/37.83 cnf(d23, plain, sdtasdt0(xp,sdtpldt0(xq,X0)) = sdtpldt0(xn,sdtasdt0(xp,X0)) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c96,d22])). % 119.50/37.83 cnf(d24, plain, sdtasdt0(sdtasdt0(xn,xn),X0) = sdtasdt0(xp,sdtasdt0(sdtasdt0(xm,xm),X0)) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtasdt0(xm,xm)) | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [c85,c10])). % 119.50/37.83 cnf(d25, plain, sdtasdt0(sdtasdt0(xn,xn),X0) = sdtasdt0(xp,sdtasdt0(sdtasdt0(xm,xm),X0)) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtasdt0(xm,xm)), inference(resolution, [status(thm)], [c73,d24])). % 119.50/37.83 cnf(d26, plain, sdtasdt0(sdtasdt0(xn,xn),X0) = sdtasdt0(xp,sdtasdt0(sdtasdt0(xm,xm),X0)) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [d17,d25])). % 119.50/37.83 cnf(d27, plain, sdtasdt0(sdtasdt0(xn,xn),sz00) = sdtasdt0(xp,sz00) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(sdtasdt0(xm,xm)), inference(superposition, [status(thm)], [c13,d26])). % 119.50/37.83 cnf(d28, plain, sdtasdt0(sdtasdt0(xn,xn),sz00) = sdtasdt0(xp,sz00) | ~aNaturalNumber0(sdtasdt0(xm,xm)), inference(resolution, [status(thm)], [c0,d27])). % 119.50/37.83 cnf(d29, plain, sdtasdt0(sdtasdt0(xn,xn),sz00) = sdtasdt0(xp,sz00), inference(resolution, [status(thm)], [d17,d28])). % 119.50/37.83 cnf(d30, plain, sdtasdt0(xp,sz00) = sz00 | ~aNaturalNumber0(sdtasdt0(xn,xn)), inference(superposition, [status(thm)], [d29,c13])). % 119.50/37.83 cnf(d31, plain, sdtasdt0(xp,sz00) = sz00, inference(resolution, [status(thm)], [d14,d30])). % 119.50/37.83 cnf(d32, plain, sdtasdt0(xp,sdtpldt0(xq,sz00)) = sdtpldt0(xn,sz00) | ~aNaturalNumber0(sz00), inference(superposition, [status(thm)], [d31,d23])). % 119.50/37.83 cnf(d33, plain, sdtasdt0(xp,sdtpldt0(xq,sz00)) = sdtpldt0(xn,sz00), inference(resolution, [status(thm)], [c0,d32])). % 119.50/37.83 cnf(d34, plain, sdtasdt0(xp,xq) = sdtpldt0(xn,sz00) | ~aNaturalNumber0(xq), inference(superposition, [status(thm)], [c7,d33])). % 119.50/37.83 cnf(d35, plain, xn = sdtpldt0(xn,sz00) | ~aNaturalNumber0(xq), inference(demodulation, [status(thm)], [d34,c97])). % 119.50/37.83 cnf(d36, plain, xn = sdtpldt0(xn,sz00), inference(resolution, [status(thm)], [c96,d35])). % 119.50/37.83 cnf(d37, plain, sdtasdt0(X0,sdtpldt0(X1,sz00)) = sdtpldt0(sdtasdt0(X0,X1),sz00) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c13,c15])). % 119.50/37.83 cnf(d38, plain, sdtasdt0(X0,sdtpldt0(X1,sz00)) = sdtpldt0(sdtasdt0(X0,X1),sz00) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c0,d37])). % 119.50/37.83 cnf(d39, plain, sdtasdt0(xp,sdtpldt0(sK97,X0)) = sdtpldt0(sdtasdt0(xn,xn),sdtasdt0(xp,X0)) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK97) | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [c91,c15])). % 119.50/37.83 cnf(d40, plain, sdtasdt0(xp,sdtpldt0(sK97,X0)) = sdtpldt0(sdtasdt0(xn,xn),sdtasdt0(xp,X0)) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK97), inference(resolution, [status(thm)], [c73,d39])). % 119.50/37.83 cnf(d41, plain, sdtasdt0(xp,sdtpldt0(sK97,X0)) = sdtpldt0(sdtasdt0(xn,xn),sdtasdt0(xp,X0)) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c90,d40])). % 119.50/37.83 cnf(d42, plain, sdtasdt0(xp,sdtpldt0(sK97,sz00)) = sdtpldt0(sdtasdt0(xn,xn),sz00) | ~aNaturalNumber0(sz00), inference(superposition, [status(thm)], [d31,d41])). % 119.50/37.83 cnf(d43, plain, sdtasdt0(xp,sdtpldt0(sK97,sz00)) = sdtpldt0(sdtasdt0(xn,xn),sz00), inference(resolution, [status(thm)], [c0,d42])). % 119.50/37.83 cnf(d44, plain, sdtasdt0(xn,sdtpldt0(xn,sz00)) = sdtasdt0(xp,sdtpldt0(sK97,sz00)) | ~aNaturalNumber0(xn) | ~aNaturalNumber0(xn), inference(superposition, [status(thm)], [d43,d38])). % 119.50/37.83 cnf(d45, plain, sdtasdt0(xn,xn) = sdtasdt0(xp,sdtpldt0(sK97,sz00)) | ~aNaturalNumber0(xn), inference(demodulation, [status(thm)], [d44,d36])). % 119.50/37.83 cnf(d46, plain, sdtasdt0(xn,xn) = sdtasdt0(xp,sdtpldt0(sK97,sz00)), inference(resolution, [status(thm)], [c71,d45])). % 119.50/37.83 cnf(d47, plain, sdtasdt0(xn,xn) = sdtasdt0(xp,sK97) | ~aNaturalNumber0(sK97), inference(superposition, [status(thm)], [c7,d46])). % 119.50/37.83 cnf(d48, plain, sdtasdt0(xn,xn) = sdtasdt0(xn,xn) | ~aNaturalNumber0(sK97), inference(demodulation, [status(thm)], [d47,c91])). % 119.50/37.83 cnf(d49, plain, sdtasdt0(xn,xn) = sdtasdt0(xn,xn), inference(resolution, [status(thm)], [c90,d48])). % 119.50/37.83 cnf(d50, plain, sdtasdt0(xm,xm) = sK97, inference(resolution, [status(thm)], [d49,d20])). % 119.50/37.83 cnf(d51, plain, sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm)), inference(resolution, [status(thm)], [d9,c104])). % 119.50/37.83 cnf(d52, plain, sdtasdt0(xm,xm) = sdtasdt0(xn,xn) | ~aNaturalNumber0(sdtasdt0(xm,xm)) | ~aNaturalNumber0(sdtasdt0(xn,xn)) | ~sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn)), inference(resolution, [status(thm)], [d51,c31])). % 119.50/37.83 cnf(d53, plain, sdtasdt0(xm,xm) = sdtasdt0(xn,xn) | ~aNaturalNumber0(sdtasdt0(xm,xm)) | ~sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn)), inference(resolution, [status(thm)], [d14,d52])). % 119.50/37.83 cnf(d54, plain, sdtasdt0(xm,xm) = sdtasdt0(xn,xn) | ~sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn)), inference(resolution, [status(thm)], [d17,d53])). % 119.50/37.83 cnf(d55, plain, sK97 = sdtasdt0(xn,xn) | ~sdtlseqdt0(sdtasdt0(xm,xm),sdtasdt0(xn,xn)), inference(demodulation, [status(thm)], [d54,d50])). % 119.50/37.83 cnf(d56, plain, sK97 = sdtasdt0(xn,xn) | ~sdtlseqdt0(sK97,sdtasdt0(xn,xn)), inference(demodulation, [status(thm)], [d55,d50])). % 119.50/37.83 cnf(d57, plain, sdtlseqdt0(X0,sdtasdt0(X1,X0)) | X1 = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c9,c45])). % 119.50/37.83 cnf(d58, plain, sdtasdt0(xp,sK97) = sdtasdt0(xn,xn), inference(demodulation, [status(thm)], [c85,d50])). % 119.50/37.83 cnf(d59, plain, sdtlseqdt0(sK97,sdtasdt0(xn,xn)) | xp = sz00 | ~aNaturalNumber0(xp) | ~aNaturalNumber0(sK97), inference(superposition, [status(thm)], [d58,d57])). % 119.50/37.83 cnf(d60, plain, xp = sz00 | ~aNaturalNumber0(sK97) | sdtlseqdt0(sK97,sdtasdt0(xn,xn)), inference(resolution, [status(thm)], [c73,d59])). % 119.50/37.83 cnf(d61, plain, xp = sz00 | sdtlseqdt0(sK97,sdtasdt0(xn,xn)), inference(resolution, [status(thm)], [c90,d60])). % 119.50/37.83 cnf(d62, plain, sdtlseqdt0(sK97,sdtasdt0(xn,xn)), inference(resolution, [status(thm)], [c76,d61])). % 119.50/37.83 cnf(d63, plain, sK97 = sdtasdt0(xn,xn), inference(resolution, [status(thm)], [d62,d56])). % 119.50/37.83 cnf(d64, plain, sdtasdt0(xn,xn) != sdtasdt0(X0,sK97) | sK97 = sz00 | xp = X0 | ~aNaturalNumber0(sK97) | ~aNaturalNumber0(xp) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c91,c20])). % 119.50/37.83 cnf(d65, plain, sdtasdt0(xn,xn) != sdtasdt0(X0,sK97) | xp = X0 | sK97 = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sK97), inference(resolution, [status(thm)], [c73,d64])). % 119.50/37.83 cnf(d66, plain, sdtasdt0(xn,xn) != sdtasdt0(X0,sK97) | xp = X0 | sK97 = sz00 | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c90,d65])). % 119.50/37.83 cnf(d67, plain, sK97 != sz00 | xm = sz00 | xm = sz00 | ~aNaturalNumber0(xm) | ~aNaturalNumber0(xm), inference(superposition, [status(thm)], [d50,c23])). % 119.50/37.83 cnf(d68, plain, xm = sz00 | sK97 != sz00, inference(resolution, [status(thm)], [c72,d67])). % 119.50/37.83 cnf(d69, plain, sK97 != sz00, inference(resolution, [status(thm)], [c75,d68])). % 119.50/37.83 cnf(d70, plain, sdtasdt0(xn,xn) != sdtasdt0(X0,sK97) | xp = X0 | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [d69,d66])). % 119.50/37.83 cnf(d71, plain, sK97 != sdtasdt0(X0,sK97) | xp = X0 | ~aNaturalNumber0(X0), inference(demodulation, [status(thm)], [d70,d63])). % 119.50/37.83 cnf(d72, plain, sdtasdt0(sdtasdt0(X1,X0),X2) = sdtasdt0(X0,sdtasdt0(X1,X2)) | ~aNaturalNumber0(X2) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c9,c10])). % 119.50/37.83 cnf(d73, plain, sdtasdt0(xm,xm) = sdtpldt0(sK101,sdtasdt0(xn,xn)) | ~aNaturalNumber0(sK101) | ~aNaturalNumber0(sdtasdt0(xn,xn)), inference(superposition, [status(thm)], [d10,c5])). % 119.50/37.83 cnf(d74, plain, sdtasdt0(xm,xm) = sdtpldt0(sK101,sdtasdt0(xn,xn)) | ~aNaturalNumber0(sK101), inference(resolution, [status(thm)], [d14,d73])). % 119.50/37.83 cnf(d75, plain, sdtasdt0(xm,xm) = sdtpldt0(sK101,sdtasdt0(xn,xn)), inference(resolution, [status(thm)], [d16,d74])). % 119.50/37.83 cnf(d76, plain, sdtpldt0(sz00,X0) = X0 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c5,c7])). % 119.50/37.83 cnf(d77, plain, sdtpldt0(sz00,X0) = X0 | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c0,d76])). % 119.50/37.83 cnf(d78, plain, sdtpldt0(X0,X1) = sdtpldt0(sz00,sdtpldt0(X0,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [d77,c6])). % 119.50/37.83 cnf(d79, plain, sdtpldt0(X0,X1) = sdtpldt0(sz00,sdtpldt0(X0,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c0,d78])). % 119.50/37.83 cnf(d80, plain, sdtpldt0(sK101,sdtasdt0(xn,xn)) = sdtpldt0(sz00,sdtasdt0(xm,xm)) | ~aNaturalNumber0(sdtasdt0(xn,xn)) | ~aNaturalNumber0(sK101), inference(superposition, [status(thm)], [d75,d79])). % 119.50/37.83 cnf(d81, plain, sdtasdt0(xm,xm) = sdtpldt0(sz00,sdtasdt0(xm,xm)) | ~aNaturalNumber0(sdtasdt0(xn,xn)) | ~aNaturalNumber0(sK101), inference(demodulation, [status(thm)], [d80,d75])). % 119.50/37.83 cnf(d82, plain, sdtasdt0(xm,xm) = sdtpldt0(sz00,sdtasdt0(xm,xm)) | ~aNaturalNumber0(sK101), inference(resolution, [status(thm)], [d14,d81])). % 119.50/37.83 cnf(d83, plain, sdtasdt0(xm,xm) = sdtpldt0(sz00,sdtasdt0(xm,xm)), inference(resolution, [status(thm)], [d16,d82])). % 119.50/37.83 cnf(d84, plain, sdtasdt0(sdtpldt0(sz00,X1),X0) = sdtpldt0(sz00,sdtasdt0(X1,X0)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c14,c16])). % 119.50/37.83 cnf(d85, plain, sdtasdt0(sdtpldt0(sz00,X0),X1) = sdtpldt0(sz00,sdtasdt0(X0,X1)) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1), inference(resolution, [status(thm)], [c0,d84])). % 119.50/37.83 cnf(d86, plain, sdtasdt0(xm,xm) = sdtasdt0(sdtpldt0(sz00,xm),xm) | ~aNaturalNumber0(xm) | ~aNaturalNumber0(xm), inference(superposition, [status(thm)], [d85,d83])). % 119.50/37.83 cnf(d87, plain, sdtasdt0(xm,xm) = sdtasdt0(sdtpldt0(sz00,xm),xm), inference(resolution, [status(thm)], [c72,d86])). % 119.50/37.83 cnf(d88, plain, sdtasdt0(sdtpldt0(X0,X1),sz10) = sdtpldt0(X0,sdtasdt0(X1,sz10)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c11,c16])). % 119.50/37.83 cnf(d89, plain, sdtasdt0(sdtpldt0(X0,X1),sz10) = sdtpldt0(X0,sdtasdt0(X1,sz10)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c1,d88])). % 119.50/37.83 cnf(d90, plain, sdtasdt0(sz00,X0) = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz00), inference(superposition, [status(thm)], [c9,c13])). % 119.50/37.83 cnf(d91, plain, sdtasdt0(sz00,X0) = sz00 | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c0,d90])). % 119.50/37.83 cnf(d92, plain, sdtasdt0(sz00,X1) = sdtasdt0(sz00,sdtasdt0(X0,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c14,c10])). % 119.50/37.83 cnf(d93, plain, sdtasdt0(sz00,X0) = sdtasdt0(sz00,sdtasdt0(X1,X0)) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1), inference(resolution, [status(thm)], [c0,d92])). % 119.50/37.83 cnf(d94, plain, sdtasdt0(X0,sdtpldt0(sz10,X1)) = sdtpldt0(X0,sdtasdt0(X0,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c11,c15])). % 119.50/37.83 cnf(d95, plain, sdtasdt0(X0,sdtpldt0(sz10,X1)) = sdtpldt0(X0,sdtasdt0(X0,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c1,d94])). % 119.50/37.83 cnf(d96, plain, sdtasdt0(xp,sdtpldt0(sz10,sz00)) = sdtpldt0(xp,sz00) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [d31,d95])). % 119.50/37.83 cnf(d97, plain, sdtasdt0(xp,sdtpldt0(sz10,sz00)) = sdtpldt0(xp,sz00) | ~aNaturalNumber0(xp), inference(resolution, [status(thm)], [c0,d96])). % 119.50/37.83 cnf(d98, plain, sdtasdt0(xp,sdtpldt0(sz10,sz00)) = sdtpldt0(xp,sz00), inference(resolution, [status(thm)], [c73,d97])). % 119.50/37.83 cnf(d99, plain, sdtasdt0(xp,sz10) = sdtpldt0(xp,sz00) | ~aNaturalNumber0(sz10), inference(superposition, [status(thm)], [c7,d98])). % 119.50/37.83 cnf(d100, plain, sdtasdt0(xp,sz10) = sdtpldt0(xp,sz00), inference(resolution, [status(thm)], [c1,d99])). % 119.50/37.83 cnf(d101, plain, sdtasdt0(xp,sz10) = sdtpldt0(sz00,xp) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [d100,c5])). % 119.50/37.83 cnf(d102, plain, sdtasdt0(xp,sz10) = sdtpldt0(sz00,xp) | ~aNaturalNumber0(xp), inference(resolution, [status(thm)], [c0,d101])). % 119.50/37.83 cnf(d103, plain, sdtasdt0(xp,sz10) = sdtpldt0(sz00,xp), inference(resolution, [status(thm)], [c73,d102])). % 119.50/37.83 cnf(d104, plain, sdtasdt0(X0,sdtpldt0(sz00,X1)) = sdtpldt0(sz00,sdtasdt0(X0,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c13,c15])). % 119.50/37.83 cnf(d105, plain, sdtasdt0(X0,sdtpldt0(sz00,X1)) = sdtpldt0(sz00,sdtasdt0(X0,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c0,d104])). % 119.50/37.83 cnf(d106, plain, sdtpldt0(xp,sz00) = sdtpldt0(sz00,sdtasdt0(xp,sz10)) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [d100,d79])). % 119.50/37.83 cnf(d107, plain, sdtasdt0(xp,sz10) = sdtpldt0(sz00,sdtasdt0(xp,sz10)) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xp), inference(demodulation, [status(thm)], [d106,d100])). % 119.50/37.83 cnf(d108, plain, sdtasdt0(xp,sz10) = sdtpldt0(sz00,sdtasdt0(xp,sz10)) | ~aNaturalNumber0(xp), inference(resolution, [status(thm)], [c0,d107])). % 119.50/37.83 cnf(d109, plain, sdtasdt0(xp,sz10) = sdtpldt0(sz00,sdtasdt0(xp,sz10)), inference(resolution, [status(thm)], [c73,d108])). % 119.50/37.83 cnf(d110, plain, sdtasdt0(xp,sz10) = sdtpldt0(sz00,sdtasdt0(sz10,xp)) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [c9,d109])). % 119.50/37.83 cnf(d111, plain, sdtasdt0(xp,sz10) = sdtpldt0(sz00,sdtasdt0(sz10,xp)) | ~aNaturalNumber0(xp), inference(resolution, [status(thm)], [c1,d110])). % 119.50/37.83 cnf(d112, plain, sdtasdt0(xp,sz10) = sdtpldt0(sz00,sdtasdt0(sz10,xp)), inference(resolution, [status(thm)], [c73,d111])). % 119.50/37.83 cnf(d113, plain, sdtasdt0(sz10,sdtpldt0(sz00,xp)) = sdtasdt0(xp,sz10) | ~aNaturalNumber0(xp) | ~aNaturalNumber0(sz10), inference(superposition, [status(thm)], [d112,d105])). % 119.50/37.83 cnf(d114, plain, sdtasdt0(sz10,sdtasdt0(xp,sz10)) = sdtasdt0(xp,sz10) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(xp), inference(demodulation, [status(thm)], [d113,d103])). % 119.50/37.83 cnf(d115, plain, sdtasdt0(sz10,sdtasdt0(xp,sz10)) = sdtasdt0(xp,sz10) | ~aNaturalNumber0(xp), inference(resolution, [status(thm)], [c1,d114])). % 119.50/37.83 cnf(d116, plain, sdtasdt0(sz10,sdtasdt0(xp,sz10)) = sdtasdt0(xp,sz10), inference(resolution, [status(thm)], [c73,d115])). % 119.50/37.83 cnf(d117, plain, sdtasdt0(sz10,xp) = sdtasdt0(xp,sz10) | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [c11,d116])). % 119.50/37.83 cnf(d118, plain, sdtasdt0(sz10,xp) = sdtasdt0(xp,sz10), inference(resolution, [status(thm)], [c73,d117])). % 119.50/37.83 cnf(d119, plain, sdtasdt0(sz00,sz10) = sdtasdt0(sz00,sdtasdt0(sz10,xp)) | ~aNaturalNumber0(xp) | ~aNaturalNumber0(sz10), inference(superposition, [status(thm)], [d118,d93])). % 119.50/37.83 cnf(d120, plain, sdtasdt0(sz00,sz10) = sdtasdt0(sz00,sdtasdt0(sz10,xp)) | ~aNaturalNumber0(xp), inference(resolution, [status(thm)], [c1,d119])). % 119.50/37.83 cnf(d121, plain, sdtasdt0(sz00,sz10) = sdtasdt0(sz00,sdtasdt0(sz10,xp)), inference(resolution, [status(thm)], [c73,d120])). % 119.50/37.83 cnf(d122, plain, sdtasdt0(sz00,sz10) = sz00 | ~aNaturalNumber0(sdtasdt0(sz10,xp)), inference(superposition, [status(thm)], [d121,d91])). % 119.50/37.83 cnf(d123, plain, aNaturalNumber0(sdtasdt0(xp,sz10)) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [d100,c3])). % 119.50/37.83 cnf(d124, plain, aNaturalNumber0(sdtasdt0(xp,sz10)) | ~aNaturalNumber0(xp), inference(resolution, [status(thm)], [c0,d123])). % 119.50/37.83 cnf(d125, plain, aNaturalNumber0(sdtasdt0(xp,sz10)), inference(resolution, [status(thm)], [c73,d124])). % 119.50/37.83 cnf(d126, plain, aNaturalNumber0(sdtasdt0(sz10,xp)), inference(demodulation, [status(thm)], [d125,d118])). % 119.50/37.83 cnf(d127, plain, sdtasdt0(sz00,sz10) = sz00, inference(resolution, [status(thm)], [d126,d122])). % 119.50/37.83 cnf(d128, plain, sdtasdt0(sdtpldt0(X0,sz00),sz10) = sdtpldt0(X0,sz00) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [d127,d89])). % 119.50/37.83 cnf(d129, plain, sdtasdt0(sdtpldt0(X0,sz00),sz10) = sdtpldt0(X0,sz00) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c0,d128])). % 119.50/37.83 cnf(d130, plain, sdtasdt0(X0,sz10) = sdtpldt0(X0,sz00) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [c7,d129])). % 119.50/37.83 cnf(d131, plain, sdtasdt0(X0,sz10) = sdtpldt0(sz00,X0) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X0), inference(superposition, [status(thm)], [d130,c5])). % 119.50/37.83 cnf(d132, plain, sdtasdt0(X0,sz10) = sdtpldt0(sz00,X0) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c0,d131])). % 119.50/37.83 cnf(d133, plain, sdtasdt0(xm,xm) = sdtasdt0(sdtasdt0(xm,sz10),xm) | ~aNaturalNumber0(xm), inference(superposition, [status(thm)], [d132,d87])). % 119.50/37.83 cnf(d134, plain, sdtasdt0(xm,xm) = sdtasdt0(sdtasdt0(xm,sz10),xm), inference(resolution, [status(thm)], [c72,d133])). % 119.50/37.83 cnf(d135, plain, sdtasdt0(xm,xm) = sdtasdt0(sz10,sdtasdt0(xm,xm)) | ~aNaturalNumber0(xm) | ~aNaturalNumber0(xm) | ~aNaturalNumber0(sz10), inference(superposition, [status(thm)], [d134,d72])). % 119.50/37.83 cnf(d136, plain, sdtasdt0(xm,xm) = sdtasdt0(sz10,sdtasdt0(xm,xm)) | ~aNaturalNumber0(xm), inference(resolution, [status(thm)], [c1,d135])). % 119.50/37.83 cnf(d137, plain, sdtasdt0(xm,xm) = sdtasdt0(sz10,sdtasdt0(xm,xm)), inference(resolution, [status(thm)], [c72,d136])). % 119.50/37.83 cnf(d138, plain, sK97 = sdtasdt0(sz10,sdtasdt0(xm,xm)), inference(demodulation, [status(thm)], [d137,d50])). % 119.50/37.83 cnf(d139, plain, sK97 = sdtasdt0(sz10,sK97), inference(demodulation, [status(thm)], [d138,d50])). % 119.50/37.83 cnf(d140, plain, sK97 != sK97 | xp = sz10 | ~aNaturalNumber0(sz10), inference(superposition, [status(thm)], [d139,d71])). % 119.50/37.83 cnf(d141, plain, xp = sz10 | sK97 != sK97, inference(resolution, [status(thm)], [c1,d140])). % 119.50/37.83 cnf(d142, plain, sK97 != sK97, inference(resolution, [status(thm)], [c86,d141])). % 119.50/37.83 cnf(d143, plain, sK97 = sdtasdt0(xm,xm) | ~aNaturalNumber0(xm) | ~aNaturalNumber0(xm), inference(superposition, [status(thm)], [d50,c9])). % 119.50/37.83 cnf(d144, plain, sK97 = sK97 | ~aNaturalNumber0(xm), inference(demodulation, [status(thm)], [d143,d50])). % 119.50/37.83 cnf(d145, plain, sK97 = sK97, inference(resolution, [status(thm)], [c72,d144])). % 119.50/37.83 cnf(d146, plain, $false, inference(resolution, [status(thm)], [d145,d142])). % 119.50/37.83 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------