%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM510+3 : 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 : n005.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:58 AM UTC 2026 % Result : Theorem 48.47s 6.58s % Output : CNFRefutation 48.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM510+3 : 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.10/0.36 % Computer : n005.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Sat Sep 26 03:02:47 UTC 2026 % 0.10/0.36 % CPUTime : % 0.10/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 48.47/6.58 % SZS status Theorem for theBenchmark.p % 48.47/6.58 % SZS output start CNFRefutation for theBenchmark.p % 48.47/6.58 fof(mSortsC, axiom, aNaturalNumber0(sz00)). % 48.47/6.58 fof(mSortsC_01, axiom, (aNaturalNumber0(sz10) & sz10 != sz00)). % 48.47/6.58 fof(m_AddZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtpldt0(X0,sz00) = X0 & X0 = sdtpldt0(sz00,X0))))). % 48.47/6.58 fof(mMulComm, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => sdtasdt0(X0,X1) = sdtasdt0(X1,X0)))). % 48.47/6.58 fof(m_MulUnit, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz10) = X0 & X0 = sdtasdt0(sz10,X0))))). % 48.47/6.58 fof(m_MulZero, axiom, ! [X0] : ((aNaturalNumber0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 48.47/6.58 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))))))). % 48.47/6.58 fof(mMonMul2, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => (X0 != sz00 => sdtlseqdt0(X1,sdtasdt0(X1,X0)))))). % 48.47/6.58 fof(m__1837, hypothesis, (aNaturalNumber0(xn) & (aNaturalNumber0(xm) & aNaturalNumber0(xp)))). % 48.47/6.58 fof(m__1860, hypothesis, (xp != sz00 & (xp != sz10 & (! [X0] : (((aNaturalNumber0(X0) & (? [X1] : ((aNaturalNumber0(X1) & xp = sdtasdt0(X0,X1))) | doDivides0(X0,xp))) => (X0 = sz10 | X0 = xp))) & (isPrime0(xp) & (? [X0] : ((aNaturalNumber0(X0) & sdtasdt0(xn,xm) = sdtasdt0(xp,X0))) & doDivides0(xp,sdtasdt0(xn,xm)))))))). % 48.47/6.58 fof(m__2306, hypothesis, (aNaturalNumber0(xk) & (sdtasdt0(xn,xm) = sdtasdt0(xp,xk) & xk = sdtsldt0(sdtasdt0(xn,xm),xp)))). % 48.47/6.58 fof(m__2315, hypothesis, ~((xk = sz00 | xk = sz10))). % 48.47/6.58 fof(m__2342, hypothesis, (aNaturalNumber0(xr) & (? [X0] : ((aNaturalNumber0(X0) & xk = sdtasdt0(xr,X0))) & (doDivides0(xr,xk) & (xr != sz00 & (xr != sz10 & (! [X0] : (((aNaturalNumber0(X0) & (? [X1] : ((aNaturalNumber0(X1) & xr = sdtasdt0(X0,X1))) | doDivides0(X0,xr))) => (X0 = sz10 | X0 = xr))) & isPrime0(xr)))))))). % 48.47/6.58 fof(m__, conjecture, (~((aNaturalNumber0(sdtsldt0(xn,xr)) & (xn = sdtasdt0(xr,sdtsldt0(xn,xr)) & sdtsldt0(xn,xr) = xn))) & ((aNaturalNumber0(sdtsldt0(xn,xr)) & xn = sdtasdt0(xr,sdtsldt0(xn,xr))) => (? [X0] : ((aNaturalNumber0(X0) & sdtpldt0(sdtsldt0(xn,xr),X0) = xn)) | sdtlseqdt0(sdtsldt0(xn,xr),xn))))). % 48.47/6.58 fof(negated_conjecture, negated_conjecture, ~((~((aNaturalNumber0(sdtsldt0(xn,xr)) & (xn = sdtasdt0(xr,sdtsldt0(xn,xr)) & sdtsldt0(xn,xr) = xn))) & ((aNaturalNumber0(sdtsldt0(xn,xr)) & xn = sdtasdt0(xr,sdtsldt0(xn,xr))) => (? [X0] : ((aNaturalNumber0(X0) & sdtpldt0(sdtsldt0(xn,xr),X0) = xn)) | sdtlseqdt0(sdtsldt0(xn,xr),xn))))), inference(negate_conjecture, [status(cth)], [m__])). % 48.47/6.58 cnf(c0, plain, aNaturalNumber0(sz00), inference(clausification, [status(esa)], [mSortsC])). % 48.47/6.58 cnf(c1, plain, aNaturalNumber0(sz10), inference(clausification, [status(esa)], [mSortsC_01])). % 48.47/6.58 cnf(c7, plain, ~aNaturalNumber0(X0) | sdtpldt0(X0,sz00) = X0, inference(clausification, [status(esa)], [m_AddZero])). % 48.47/6.58 cnf(c9, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtasdt0(X0,X1) = sdtasdt0(X1,X0), inference(clausification, [status(esa)], [mMulComm])). % 48.47/6.58 cnf(c11, plain, ~aNaturalNumber0(X0) | sdtasdt0(X0,sz10) = X0, inference(clausification, [status(esa)], [m_MulUnit])). % 48.47/6.58 cnf(c12, plain, ~aNaturalNumber0(X0) | sdtasdt0(sz10,X0) = X0, inference(clausification, [status(esa)], [m_MulUnit])). % 48.47/6.58 cnf(c13, plain, ~aNaturalNumber0(X0) | sdtasdt0(X0,sz00) = sz00, inference(clausification, [status(esa)], [m_MulZero])). % 48.47/6.58 cnf(c14, plain, ~aNaturalNumber0(X0) | sdtasdt0(sz00,X0) = sz00, inference(clausification, [status(esa)], [m_MulZero])). % 48.47/6.58 cnf(c19, plain, ~aNaturalNumber0(X0) | X1 = sz00 | ~aNaturalNumber0(X2) | ~aNaturalNumber0(X1) | X2 = X0 | sdtasdt0(X1,X2) != sdtasdt0(X1,X0), inference(clausification, [status(esa)], [mMulCanc])). % 48.47/6.58 cnf(c20, plain, sdtasdt0(X0,X1) != sdtasdt0(X2,X1) | ~aNaturalNumber0(X2) | X1 = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | X0 = X2, inference(clausification, [status(esa)], [mMulCanc])). % 48.47/6.58 cnf(c45, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtlseqdt0(X0,sdtasdt0(X0,X1)) | X1 = sz00, inference(clausification, [status(esa)], [mMonMul2])). % 48.47/6.58 cnf(c69, plain, aNaturalNumber0(xn), inference(clausification, [status(esa)], [m__1837])). % 48.47/6.58 cnf(c70, plain, aNaturalNumber0(xp), inference(clausification, [status(esa)], [m__1837])). % 48.47/6.58 cnf(c71, plain, aNaturalNumber0(xm), inference(clausification, [status(esa)], [m__1837])). % 48.47/6.58 cnf(c89, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | X1 = xp | X1 = sz10 | sdtasdt0(X1,X0) != xp, inference(clausification, [status(esa)], [m__1860])). % 48.47/6.58 cnf(c108, plain, aNaturalNumber0(xk), inference(clausification, [status(esa)], [m__2306])). % 48.47/6.58 cnf(c110, plain, sdtasdt0(xp,xk) = sdtasdt0(xn,xm), inference(clausification, [status(esa)], [m__2306])). % 48.47/6.58 cnf(c111, plain, xk != sz00, inference(clausification, [status(esa)], [m__2315])). % 48.47/6.58 cnf(c115, plain, aNaturalNumber0(xr), inference(clausification, [status(esa)], [m__2342])). % 48.47/6.58 cnf(c117, plain, xr != sz10, inference(clausification, [status(esa)], [m__2342])). % 48.47/6.58 cnf(c121, plain, xr != sz00, inference(clausification, [status(esa)], [m__2342])). % 48.47/6.58 cnf(c142, plain, aNaturalNumber0(sdtsldt0(xn,xr)) | X0, inference(clausification, [status(esa)], [negated_conjecture])). % 48.47/6.58 cnf(c143, plain, sdtsldt0(xn,xr) = xn | X0, inference(clausification, [status(esa)], [negated_conjecture])). % 48.47/6.58 cnf(c144, plain, sdtasdt0(xr,sdtsldt0(xn,xr)) = xn | X0, inference(clausification, [status(esa)], [negated_conjecture])). % 48.47/6.58 cnf(c145, plain, ~X0 | sdtasdt0(xr,sdtsldt0(xn,xr)) = xn, inference(clausification, [status(esa)], [negated_conjecture])). % 48.47/6.58 cnf(c146, plain, ~X0 | aNaturalNumber0(sdtsldt0(xn,xr)), inference(clausification, [status(esa)], [negated_conjecture])). % 48.47/6.58 cnf(c147, plain, ~X0 | ~sdtlseqdt0(sdtsldt0(xn,xr),xn), inference(clausification, [status(esa)], [negated_conjecture])). % 48.47/6.58 cnf(d0, plain, sdtasdt0(xr,sdtsldt0(xn,xr)) = xn | sdtasdt0(xr,sdtsldt0(xn,xr)) = xn, inference(resolution, [status(thm)], [c145,c144])). % 48.47/6.58 cnf(d1, plain, sdtasdt0(X0,sdtsldt0(xn,xr)) = sdtasdt0(sdtsldt0(xn,xr),X0) | ~aNaturalNumber0(X0) | ~'Ts111', inference(resolution, [status(thm)], [c9,c146])). % 48.47/6.58 cnf(d2, plain, sdtasdt0(xr,sdtsldt0(xn,xr)) = sdtasdt0(sdtsldt0(xn,xr),xr) | ~'Ts111', inference(resolution, [status(thm)], [d1,c115])). % 48.47/6.58 cnf(d3, plain, xn = sdtasdt0(sdtsldt0(xn,xr),xr) | ~'Ts111', inference(demodulation, [status(thm)], [d2,d0])). % 48.47/6.58 cnf(d4, plain, sdtasdt0(X0,sdtsldt0(xn,xr)) = sdtasdt0(sdtsldt0(xn,xr),X0) | ~aNaturalNumber0(X0) | 'Ts111', inference(resolution, [status(thm)], [c9,c142])). % 48.47/6.58 cnf(d5, plain, sdtasdt0(xr,sdtsldt0(xn,xr)) = sdtasdt0(sdtsldt0(xn,xr),xr) | 'Ts111', inference(resolution, [status(thm)], [d4,c115])). % 48.47/6.58 cnf(d6, plain, xn = sdtasdt0(sdtsldt0(xn,xr),xr) | 'Ts111', inference(demodulation, [status(thm)], [d5,d0])). % 48.47/6.58 cnf(d7, plain, xn = sdtasdt0(sdtsldt0(xn,xr),xr) | xn = sdtasdt0(sdtsldt0(xn,xr),xr), inference(resolution, [status(thm)], [d6,d3])). % 48.47/6.58 cnf(d8, plain, sdtlseqdt0(sdtsldt0(xn,xr),xn) | xr = sz00 | ~aNaturalNumber0(xr) | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(superposition, [status(thm)], [d7,c45])). % 48.47/6.58 cnf(d9, plain, xr = sz00 | ~aNaturalNumber0(sdtsldt0(xn,xr)) | sdtlseqdt0(sdtsldt0(xn,xr),xn), inference(resolution, [status(thm)], [c115,d8])). % 48.47/6.58 cnf(d10, plain, xr = sz00 | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~'Ts111', inference(resolution, [status(thm)], [d9,c147])). % 48.47/6.58 cnf(d11, plain, xr = sz00 | ~'Ts111' | ~'Ts111', inference(resolution, [status(thm)], [d10,c146])). % 48.47/6.58 cnf(d12, plain, xr = sz00 | sdtsldt0(xn,xr) = xn, inference(resolution, [status(thm)], [d11,c143])). % 48.47/6.58 cnf(d13, plain, sdtsldt0(xn,xr) = xn, inference(resolution, [status(thm)], [c121,d12])). % 48.47/6.58 cnf(d14, plain, sdtasdt0(sdtsldt0(xn,xr),sz10) = sdtsldt0(xn,xr) | ~'Ts111', inference(resolution, [status(thm)], [c11,c146])). % 48.47/6.58 cnf(d15, plain, sdtasdt0(sdtsldt0(xn,xr),sz10) = sdtsldt0(xn,xr) | 'Ts111', inference(resolution, [status(thm)], [c11,c142])). % 48.47/6.58 cnf(d16, plain, sdtasdt0(sdtsldt0(xn,xr),sz10) = sdtsldt0(xn,xr) | sdtasdt0(sdtsldt0(xn,xr),sz10) = sdtsldt0(xn,xr), inference(resolution, [status(thm)], [d15,d14])). % 48.47/6.58 cnf(d17, plain, sdtsldt0(xn,xr) != sdtasdt0(sdtsldt0(xn,xr),X0) | sz10 = X0 | sdtsldt0(xn,xr) = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(superposition, [status(thm)], [d16,c19])). % 48.47/6.58 cnf(d18, plain, sz10 = X0 | xn = sz00 | sdtsldt0(xn,xr) != sdtasdt0(sdtsldt0(xn,xr),X0) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(demodulation, [status(thm)], [d17,d13])). % 48.47/6.58 cnf(d19, plain, sz10 = X0 | xn = sz00 | xn != sdtasdt0(sdtsldt0(xn,xr),X0) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(demodulation, [status(thm)], [d18,d13])). % 48.47/6.58 cnf(d20, plain, sz10 = X0 | xn = sz00 | xn != sdtasdt0(xn,X0) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(demodulation, [status(thm)], [d19,d13])). % 48.47/6.58 cnf(d21, plain, sz10 = X0 | xn = sz00 | xn != sdtasdt0(xn,X0) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz10) | ~aNaturalNumber0(xn), inference(demodulation, [status(thm)], [d20,d13])). % 48.47/6.58 cnf(d22, plain, sz10 = X0 | xn = sz00 | xn != sdtasdt0(xn,X0) | ~aNaturalNumber0(X0) | ~aNaturalNumber0(xn), inference(resolution, [status(thm)], [c1,d21])). % 48.47/6.58 cnf(d23, plain, sz10 = X0 | xn = sz00 | xn != sdtasdt0(xn,X0) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c69,d22])). % 48.47/6.58 cnf(d24, plain, xn = sdtasdt0(xn,xr) | xr = sz00, inference(superposition, [status(thm)], [d12,d7])). % 48.47/6.58 cnf(d25, plain, xn = sdtasdt0(xn,xr), inference(resolution, [status(thm)], [c121,d24])). % 48.47/6.58 cnf(d26, plain, xn != xn | sz10 = xr | xn = sz00 | ~aNaturalNumber0(xr), inference(superposition, [status(thm)], [d25,d23])). % 48.47/6.58 cnf(d27, plain, sz10 = xr | xn = sz00 | xn != xn, inference(resolution, [status(thm)], [c115,d26])). % 48.47/6.58 cnf(d28, plain, sdtasdt0(xr,xn) = xn | xr = sz00, inference(superposition, [status(thm)], [d12,d0])). % 48.47/6.58 cnf(d29, plain, sdtasdt0(xr,xn) = xn, inference(resolution, [status(thm)], [c121,d28])). % 48.47/6.58 cnf(d30, plain, sdtasdt0(xn,sz10) = sdtsldt0(xn,xr) | xr = sz00, inference(superposition, [status(thm)], [d12,d16])). % 48.47/6.58 cnf(d31, plain, sdtasdt0(sz10,sdtsldt0(xn,xr)) = sdtsldt0(xn,xr) | ~'Ts111', inference(resolution, [status(thm)], [c12,c146])). % 48.47/6.58 cnf(d32, plain, sdtasdt0(sz10,sdtsldt0(xn,xr)) = sdtsldt0(xn,xr) | 'Ts111', inference(resolution, [status(thm)], [c12,c142])). % 48.47/6.58 cnf(d33, plain, sdtasdt0(sz10,sdtsldt0(xn,xr)) = sdtsldt0(xn,xr) | sdtasdt0(sz10,sdtsldt0(xn,xr)) = sdtsldt0(xn,xr), inference(resolution, [status(thm)], [d32,d31])). % 48.47/6.58 cnf(d34, plain, sdtasdt0(sz10,xn) = sdtsldt0(xn,xr) | xr = sz00, inference(superposition, [status(thm)], [d12,d33])). % 48.47/6.58 cnf(d35, plain, sdtasdt0(xn,sz10) = sdtasdt0(sz10,xn) | xr = sz00 | xr = sz00, inference(superposition, [status(thm)], [d34,d30])). % 48.47/6.58 cnf(d36, plain, sdtasdt0(xn,sz10) = xn | xr = sz00 | xr = sz00, inference(superposition, [status(thm)], [d30,d12])). % 48.47/6.58 cnf(d37, plain, xn = sdtasdt0(sz10,xn) | xr = sz00 | xr = sz00, inference(superposition, [status(thm)], [d36,d35])). % 48.47/6.58 cnf(d38, plain, sdtpldt0(sdtsldt0(xn,xr),sz00) = sdtsldt0(xn,xr) | ~'Ts111', inference(resolution, [status(thm)], [c7,c146])). % 48.47/6.58 cnf(d39, plain, sdtpldt0(sdtsldt0(xn,xr),sz00) = sdtsldt0(xn,xr) | 'Ts111', inference(resolution, [status(thm)], [c7,c142])). % 48.47/6.58 cnf(d40, plain, sdtpldt0(sdtsldt0(xn,xr),sz00) = sdtsldt0(xn,xr) | sdtpldt0(sdtsldt0(xn,xr),sz00) = sdtsldt0(xn,xr), inference(resolution, [status(thm)], [d39,d38])). % 48.47/6.58 cnf(d41, plain, sdtpldt0(xn,sz00) = sdtsldt0(xn,xr) | xr = sz00, inference(superposition, [status(thm)], [d12,d40])). % 48.47/6.58 cnf(d42, plain, sdtasdt0(sz10,xn) = sdtpldt0(xn,sz00) | xr = sz00 | xr = sz00, inference(superposition, [status(thm)], [d41,d34])). % 48.47/6.58 cnf(d43, plain, xn = sdtpldt0(xn,sz00) | xr = sz00 | xr = sz00, inference(superposition, [status(thm)], [d42,d37])). % 48.47/6.58 cnf(d44, plain, xn = sdtpldt0(xn,sz00), inference(resolution, [status(thm)], [c121,d43])). % 48.47/6.58 cnf(d45, plain, sdtasdt0(xr,sdtasdt0(sz10,xn)) = xn | xr = sz00, inference(superposition, [status(thm)], [d34,d0])). % 48.47/6.58 cnf(d46, plain, sdtasdt0(xr,sdtpldt0(xn,sz00)) = xn | xr = sz00 | xr = sz00, inference(superposition, [status(thm)], [d42,d45])). % 48.47/6.58 cnf(d47, plain, sdtasdt0(xr,xn) = xn | xr = sz00, inference(demodulation, [status(thm)], [d46,d44])). % 48.47/6.58 cnf(d48, plain, xn = xn | xr = sz00, inference(demodulation, [status(thm)], [d47,d29])). % 48.47/6.58 cnf(d49, plain, xn = xn, inference(resolution, [status(thm)], [c121,d48])). % 48.47/6.58 cnf(d50, plain, sz10 = xr | xn = sz00, inference(resolution, [status(thm)], [d49,d27])). % 48.47/6.58 cnf(d51, plain, sz10 != sz10 | xn = sz00, inference(superposition, [status(thm)], [d50,c117])). % 48.47/6.58 cnf(d52, plain, xn = sz00, inference(equality_resolution, [status(thm)], [d51])). % 48.47/6.58 cnf(d53, plain, sdtasdt0(sz10,xn) = xn | xr = sz00 | xr = sz00, inference(superposition, [status(thm)], [d34,d12])). % 48.47/6.58 cnf(d54, plain, sdtasdt0(sz10,xn) = xn, inference(resolution, [status(thm)], [c121,d53])). % 48.47/6.58 cnf(d55, plain, sdtasdt0(sz10,xn) = sdtsldt0(xn,xr), inference(resolution, [status(thm)], [c121,d34])). % 48.47/6.58 cnf(d56, plain, xn = sdtsldt0(xn,xr), inference(demodulation, [status(thm)], [d55,d54])). % 48.47/6.58 cnf(d57, plain, sz00 = sdtsldt0(xn,xr), inference(demodulation, [status(thm)], [d56,d52])). % 48.47/6.58 cnf(d58, plain, sz00 = sdtsldt0(sz00,xr), inference(demodulation, [status(thm)], [d57,d52])). % 48.47/6.58 cnf(d59, plain, sdtasdt0(xk,sz00) = sz00, inference(resolution, [status(thm)], [c13,c108])). % 48.47/6.58 cnf(d60, plain, sdtasdt0(xk,sdtsldt0(xn,xr)) = sdtasdt0(sdtsldt0(xn,xr),xk) | ~'Ts111', inference(resolution, [status(thm)], [d1,c108])). % 48.47/6.58 cnf(d61, plain, sdtasdt0(xk,sdtsldt0(xn,xr)) = sdtasdt0(sdtsldt0(xn,xr),xk) | 'Ts111', inference(resolution, [status(thm)], [d4,c108])). % 48.47/6.58 cnf(d62, plain, sdtasdt0(xk,sdtsldt0(xn,xr)) = sdtasdt0(sdtsldt0(xn,xr),xk) | sdtasdt0(xk,sdtsldt0(xn,xr)) = sdtasdt0(sdtsldt0(xn,xr),xk), inference(resolution, [status(thm)], [d61,d60])). % 48.47/6.58 cnf(d63, plain, sdtasdt0(xk,sdtsldt0(xn,xr)) != sdtasdt0(X0,xk) | sdtsldt0(xn,xr) = X0 | xk = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xk), inference(superposition, [status(thm)], [d62,c20])). % 48.47/6.58 cnf(d64, plain, sdtasdt0(xk,sdtsldt0(sz00,xr)) != sdtasdt0(X0,xk) | sdtsldt0(xn,xr) = X0 | xk = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xk), inference(demodulation, [status(thm)], [d63,d52])). % 48.47/6.58 cnf(d65, plain, sdtasdt0(xk,sz00) != sdtasdt0(X0,xk) | sdtsldt0(xn,xr) = X0 | xk = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xk), inference(demodulation, [status(thm)], [d64,d58])). % 48.47/6.58 cnf(d66, plain, sz00 != sdtasdt0(X0,xk) | sdtsldt0(xn,xr) = X0 | xk = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xk), inference(demodulation, [status(thm)], [d65,d59])). % 48.47/6.58 cnf(d67, plain, sz00 != sdtasdt0(X0,xk) | sdtsldt0(sz00,xr) = X0 | xk = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xk), inference(demodulation, [status(thm)], [d66,d52])). % 48.47/6.58 cnf(d68, plain, sz00 != sdtasdt0(X0,xk) | sz00 = X0 | xk = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xk), inference(demodulation, [status(thm)], [d67,d58])). % 48.47/6.58 cnf(d69, plain, sz00 != sdtasdt0(X0,xk) | sz00 = X0 | xk = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sdtsldt0(sz00,xr)) | ~aNaturalNumber0(xk), inference(demodulation, [status(thm)], [d68,d52])). % 48.47/6.58 cnf(d70, plain, sz00 != sdtasdt0(X0,xk) | sz00 = X0 | xk = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(sz00) | ~aNaturalNumber0(xk), inference(demodulation, [status(thm)], [d69,d58])). % 48.47/6.58 cnf(d71, plain, sz00 != sdtasdt0(X0,xk) | sz00 = X0 | xk = sz00 | ~aNaturalNumber0(X0) | ~aNaturalNumber0(xk), inference(resolution, [status(thm)], [c0,d70])). % 48.47/6.58 cnf(d72, plain, sz00 = X0 | sz00 != sdtasdt0(X0,xk) | xk = sz00 | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c108,d71])). % 48.47/6.58 cnf(d73, plain, sz00 = X0 | sz00 != sdtasdt0(X0,xk) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c111,d72])). % 48.47/6.58 cnf(d74, plain, sdtasdt0(sz00,xm) = sz00, inference(resolution, [status(thm)], [c14,c71])). % 48.47/6.58 cnf(d75, plain, sdtasdt0(xp,xk) = sdtasdt0(sz00,xm), inference(demodulation, [status(thm)], [c110,d52])). % 48.47/6.58 cnf(d76, plain, sdtasdt0(xp,xk) = sz00, inference(demodulation, [status(thm)], [d75,d74])). % 48.47/6.58 cnf(d77, plain, sz00 != sz00 | sz00 = xp | ~aNaturalNumber0(xp), inference(superposition, [status(thm)], [d76,d73])). % 48.47/6.58 cnf(d78, plain, sz00 != sz00 | sz00 = xp, inference(resolution, [status(thm)], [c70,d77])). % 48.47/6.58 cnf(d79, plain, sdtasdt0(sdtsldt0(xn,xr),sz00) = sz00 | ~'Ts111', inference(resolution, [status(thm)], [c13,c146])). % 48.47/6.58 cnf(d80, plain, sdtasdt0(sdtsldt0(xn,xr),sz00) = sz00 | 'Ts111', inference(resolution, [status(thm)], [c13,c142])). % 48.47/6.58 cnf(d81, plain, sdtasdt0(sdtsldt0(xn,xr),sz00) = sz00 | sdtasdt0(sdtsldt0(xn,xr),sz00) = sz00, inference(resolution, [status(thm)], [d80,d79])). % 48.47/6.58 cnf(d82, plain, sdtasdt0(xn,sz00) = sz00 | xr = sz00, inference(superposition, [status(thm)], [d12,d81])). % 48.47/6.58 cnf(d83, plain, sdtasdt0(xn,sz00) = sz00, inference(resolution, [status(thm)], [c121,d82])). % 48.47/6.58 cnf(d84, plain, sdtasdt0(sdtasdt0(sz10,xn),sz00) = sz00 | xr = sz00, inference(superposition, [status(thm)], [d34,d81])). % 48.47/6.58 cnf(d85, plain, sdtasdt0(sdtpldt0(xn,sz00),sz00) = sz00 | xr = sz00 | xr = sz00, inference(superposition, [status(thm)], [d42,d84])). % 48.47/6.58 cnf(d86, plain, sdtasdt0(xn,sz00) = sz00 | xr = sz00, inference(demodulation, [status(thm)], [d85,d44])). % 48.47/6.58 cnf(d87, plain, sz00 = sz00 | xr = sz00, inference(demodulation, [status(thm)], [d86,d83])). % 48.47/6.58 cnf(d88, plain, sz00 = sz00, inference(resolution, [status(thm)], [c121,d87])). % 48.47/6.58 cnf(d89, plain, sz00 = xp, inference(resolution, [status(thm)], [d88,d78])). % 48.47/6.58 cnf(d90, plain, xn != xp | xr = sz10 | xr = xp | ~aNaturalNumber0(xn) | ~aNaturalNumber0(xr), inference(superposition, [status(thm)], [d29,c89])). % 48.47/6.58 cnf(d91, plain, xn != xp | xr = sz10 | xr = xp | ~aNaturalNumber0(xr), inference(resolution, [status(thm)], [c69,d90])). % 48.47/6.58 cnf(d92, plain, xn != xp | xr = sz10 | xr = xp, inference(resolution, [status(thm)], [c115,d91])). % 48.47/6.58 cnf(d93, plain, xn != xp | xr = xp, inference(resolution, [status(thm)], [c117,d92])). % 48.47/6.58 cnf(d94, plain, sz00 != xp | xr = xp, inference(demodulation, [status(thm)], [d93,d52])). % 48.47/6.58 cnf(d95, plain, xr = xp, inference(resolution, [status(thm)], [d89,d94])). % 48.47/6.58 cnf(d96, plain, xr = sz00, inference(demodulation, [status(thm)], [d95,d89])). % 48.47/6.58 cnf(d97, plain, $false, inference(resolution, [status(thm)], [c121,d96])). % 48.47/6.58 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------