%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM517+1 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n019.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:59 AM UTC 2026 % Result : Theorem 24.05s 23.08s % Output : CNFRefutation 24.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : NUM517+1 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.14/0.39 % Computer : n019.cluster.edu % 0.14/0.39 % Model : x86_64 x86_64 % 0.14/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.39 % Memory : 8046.5625MB % 0.14/0.39 % OS : Linux 6.8.0-71-generic % 0.14/0.39 % CPULimit : 300 % 0.14/0.39 % WCLimit : 300 % 0.14/0.39 % DateTime : Sat Sep 26 03:04:48 UTC 2026 % 0.14/0.40 % CPUTime : % 0.14/0.40 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 24.05/23.08 % SZS status Theorem for theBenchmark.p % 24.05/23.08 % SZS output start CNFRefutation for theBenchmark.p % 24.05/23.08 fof(mSortsB, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => aNaturalNumber0(sdtpldt0(X0,X1))))). % 24.05/23.08 fof(mAddComm, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => sdtpldt0(X0,X1) = sdtpldt0(X1,X0)))). % 24.05/23.08 fof(mAddAsso, axiom, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2))))). % 24.05/23.08 fof(mIH_03, axiom, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((X0 != X1 & sdtlseqdt0(X0,X1)) => iLess0(X0,X1))))). % 24.05/23.08 fof(mDefQuot, definition, ! [X0] : ! [X1] : (((aNaturalNumber0(X0) & aNaturalNumber0(X1)) => ((X0 != sz00 & doDivides0(X0,X1)) => ! [X2] : ((X2 = sdtsldt0(X1,X0) <=> (aNaturalNumber0(X2) & X1 = sdtasdt0(X0,X2)))))))). % 24.05/23.08 fof(mDefPrime, definition, ! [X0] : ((aNaturalNumber0(X0) => (isPrime0(X0) <=> (X0 != sz00 & (X0 != sz10 & ! [X1] : (((aNaturalNumber0(X1) & doDivides0(X1,X0)) => (X1 = sz10 | X1 = X0))))))))). % 24.05/23.08 fof(m__1837, hypothesis, (aNaturalNumber0(xn) & (aNaturalNumber0(xm) & aNaturalNumber0(xp)))). % 24.05/23.08 fof(m__1799, hypothesis, ! [X0] : ! [X1] : ! [X2] : (((aNaturalNumber0(X0) & (aNaturalNumber0(X1) & aNaturalNumber0(X2))) => ((isPrime0(X2) & doDivides0(X2,sdtasdt0(X0,X1))) => (iLess0(sdtpldt0(sdtpldt0(X0,X1),X2),sdtpldt0(sdtpldt0(xn,xm),xp)) => (doDivides0(X2,X0) | doDivides0(X2,X1))))))). % 24.05/23.08 fof(m__1860, hypothesis, (isPrime0(xp) & doDivides0(xp,sdtasdt0(xn,xm)))). % 24.05/23.08 fof(m__2342, hypothesis, (aNaturalNumber0(xr) & (doDivides0(xr,xk) & isPrime0(xr)))). % 24.05/23.08 fof(m__2487, hypothesis, doDivides0(xr,xn)). % 24.05/23.08 fof(m__2529, hypothesis, doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm))). % 24.05/23.08 fof(m__2686, hypothesis, (sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp) != sdtpldt0(sdtpldt0(xn,xm),xp) & sdtlseqdt0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp)))). % 24.05/23.08 fof(m__, conjecture, (doDivides0(xp,sdtsldt0(xn,xr)) | doDivides0(xp,xm))). % 24.05/23.08 fof(negated_conjecture, negated_conjecture, ~((doDivides0(xp,sdtsldt0(xn,xr)) | doDivides0(xp,xm))), inference(negate_conjecture, [status(cth)], [m__])). % 24.05/23.08 cnf(c3, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | aNaturalNumber0(sdtpldt0(X0,X1)), inference(clausification, [status(esa)], [mSortsB])). % 24.05/23.08 cnf(c5, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | sdtpldt0(X0,X1) = sdtpldt0(X1,X0), inference(clausification, [status(esa)], [mAddComm])). % 24.05/23.08 cnf(c6, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2) | sdtpldt0(sdtpldt0(X0,X1),X2) = sdtpldt0(X0,sdtpldt0(X1,X2)), inference(clausification, [status(esa)], [mAddAsso])). % 24.05/23.08 cnf(c46, plain, ~aNaturalNumber0(X0) | X1 = X0 | iLess0(X1,X0) | ~sdtlseqdt0(X1,X0) | ~aNaturalNumber0(X1), inference(clausification, [status(esa)], [mIH_03])). % 24.05/23.08 cnf(c50, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | X2 != sdtsldt0(X1,X0) | aNaturalNumber0(X2) | ~doDivides0(X0,X1) | X0 = sz00, inference(clausification, [status(esa)], [mDefQuot])). % 24.05/23.08 cnf(c58, plain, ~aNaturalNumber0(X0) | ~isPrime0(X0) | X1(X0), inference(clausification, [status(esa)], [mDefPrime])). % 24.05/23.08 cnf(c60, plain, ~X0(X1) | X1 != sz00, inference(clausification, [status(esa)], [mDefPrime])). % 24.05/23.08 cnf(c70, plain, aNaturalNumber0(xn), inference(clausification, [status(esa)], [m__1837])). % 24.05/23.08 cnf(c71, plain, aNaturalNumber0(xm), inference(clausification, [status(esa)], [m__1837])). % 24.05/23.08 cnf(c72, plain, aNaturalNumber0(xp), inference(clausification, [status(esa)], [m__1837])). % 24.05/23.08 cnf(c73, plain, ~aNaturalNumber0(X0) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X2) | ~isPrime0(X1) | doDivides0(X1,X0) | ~doDivides0(X1,sdtasdt0(X2,X0)) | ~iLess0(sdtpldt0(sdtpldt0(X2,X0),X1),sdtpldt0(sdtpldt0(xn,xm),xp)) | doDivides0(X1,X2), inference(clausification, [status(esa)], [m__1799])). % 24.05/23.08 cnf(c74, plain, isPrime0(xp), inference(clausification, [status(esa)], [m__1860])). % 24.05/23.08 cnf(c87, plain, aNaturalNumber0(xr), inference(clausification, [status(esa)], [m__2342])). % 24.05/23.08 cnf(c89, plain, isPrime0(xr), inference(clausification, [status(esa)], [m__2342])). % 24.05/23.08 cnf(c95, plain, doDivides0(xr,xn), inference(clausification, [status(esa)], [m__2487])). % 24.05/23.08 cnf(c98, plain, doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)), inference(clausification, [status(esa)], [m__2529])). % 24.05/23.08 cnf(c99, plain, sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp) != sdtpldt0(sdtpldt0(xn,xm),xp), inference(clausification, [status(esa)], [m__2686])). % 24.05/23.08 cnf(c100, plain, sdtlseqdt0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp)), inference(clausification, [status(esa)], [m__2686])). % 24.05/23.08 cnf(c101, plain, ~doDivides0(xp,sdtsldt0(xn,xr)), inference(clausification, [status(esa)], [negated_conjecture])). % 24.05/23.08 cnf(c102, plain, ~doDivides0(xp,xm), inference(clausification, [status(esa)], [negated_conjecture])). % 24.05/23.08 cnf(d0, plain, X0 = sz00 | ~aNaturalNumber0(X0) | aNaturalNumber0(sdtsldt0(X1,X0)) | ~aNaturalNumber0(X1) | ~doDivides0(X0,X1), inference(equality_resolution, [status(thm)], [c50])). % 24.05/23.08 cnf(d1, plain, sdtpldt0(xp,X0) = sdtpldt0(X0,xp) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c5,c72])). % 24.05/23.08 cnf(d2, plain, sdtpldt0(xp,xm) = sdtpldt0(xm,xp), inference(resolution, [status(thm)], [d1,c71])). % 24.05/23.08 cnf(d3, plain, sdtpldt0(sdtpldt0(X0,xm),X1) = sdtpldt0(X0,sdtpldt0(xm,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c6,c71])). % 24.05/23.08 cnf(d4, plain, sdtpldt0(sdtpldt0(xn,xm),X0) = sdtpldt0(xn,sdtpldt0(xm,X0)) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [d3,c70])). % 24.05/23.08 cnf(d5, plain, sdtpldt0(sdtpldt0(xn,xm),xp) = sdtpldt0(xn,sdtpldt0(xm,xp)), inference(resolution, [status(thm)], [d4,c72])). % 24.05/23.08 cnf(d6, plain, sdtpldt0(sdtpldt0(xn,xm),xp) = sdtpldt0(xn,sdtpldt0(xp,xm)), inference(demodulation, [status(thm)], [d5,d2])). % 24.05/23.08 cnf(d7, plain, sdtpldt0(xn,X0) = sdtpldt0(X0,xn) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c5,c70])). % 24.05/23.08 cnf(d8, plain, sdtpldt0(xn,xm) = sdtpldt0(xm,xn), inference(resolution, [status(thm)], [d7,c71])). % 24.05/23.08 cnf(d9, plain, sdtpldt0(sdtpldt0(X0,xn),X1) = sdtpldt0(X0,sdtpldt0(xn,X1)) | ~aNaturalNumber0(X1) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [c6,c70])). % 24.05/23.08 cnf(d10, plain, sdtpldt0(sdtpldt0(xm,xn),X0) = sdtpldt0(xm,sdtpldt0(xn,X0)) | ~aNaturalNumber0(X0), inference(resolution, [status(thm)], [d9,c71])). % 24.05/23.08 cnf(d11, plain, sdtpldt0(sdtpldt0(xn,xm),X0) = sdtpldt0(xm,sdtpldt0(xn,X0)) | ~aNaturalNumber0(X0), inference(demodulation, [status(thm)], [d10,d8])). % 24.05/23.08 cnf(d12, plain, sdtpldt0(sdtpldt0(xn,xm),xp) = sdtpldt0(xm,sdtpldt0(xn,xp)), inference(resolution, [status(thm)], [d11,c72])). % 24.05/23.08 cnf(d13, plain, sdtpldt0(xn,sdtpldt0(xp,xm)) = sdtpldt0(xm,sdtpldt0(xn,xp)), inference(demodulation, [status(thm)], [d12,d6])). % 24.05/23.08 cnf(d14, plain, aNaturalNumber0(sdtpldt0(xm,sdtpldt0(xn,xp))) | ~aNaturalNumber0(xp) | ~aNaturalNumber0(sdtpldt0(xn,xm)), inference(superposition, [status(thm)], [d12,c3])). % 24.05/23.08 cnf(d15, plain, ~aNaturalNumber0(sdtpldt0(xn,xm)) | aNaturalNumber0(sdtpldt0(xn,sdtpldt0(xp,xm))) | ~aNaturalNumber0(xp), inference(demodulation, [status(thm)], [d14,d13])). % 24.05/23.08 cnf(d16, plain, ~aNaturalNumber0(sdtpldt0(xn,xm)) | aNaturalNumber0(sdtpldt0(xn,sdtpldt0(xp,xm))), inference(resolution, [status(thm)], [c72,d15])). % 24.05/23.08 cnf(d17, plain, sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp) = sdtpldt0(sdtpldt0(xn,xm),xp) | ~aNaturalNumber0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp)) | ~aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp)) | iLess0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp)), inference(resolution, [status(thm)], [c100,c46])). % 24.05/23.08 cnf(d18, plain, ~aNaturalNumber0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp)) | ~aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp)) | iLess0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp),sdtpldt0(sdtpldt0(xn,xm),xp)), inference(resolution, [status(thm)], [c99,d17])). % 24.05/23.08 cnf(d19, plain, ~aNaturalNumber0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp)) | ~aNaturalNumber0(sdtpldt0(sdtpldt0(xn,xm),xp)) | ~aNaturalNumber0(xp) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xm) | doDivides0(xp,sdtsldt0(xn,xr)) | doDivides0(xp,xm) | ~doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)) | ~isPrime0(xp), inference(resolution, [status(thm)], [d18,c73])). % 24.05/23.08 cnf(d20, plain, ~aNaturalNumber0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp)) | ~aNaturalNumber0(sdtpldt0(xn,sdtpldt0(xp,xm))) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xm) | ~aNaturalNumber0(xp) | ~doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)) | doDivides0(xp,sdtsldt0(xn,xr)) | doDivides0(xp,xm) | ~isPrime0(xp), inference(demodulation, [status(thm)], [d19,d6])). % 24.05/23.08 cnf(d21, plain, ~aNaturalNumber0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp)) | ~aNaturalNumber0(sdtpldt0(xn,sdtpldt0(xp,xm))) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xm) | ~aNaturalNumber0(xp) | ~doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)) | doDivides0(xp,sdtsldt0(xn,xr)) | ~isPrime0(xp), inference(resolution, [status(thm)], [c102,d20])). % 24.05/23.08 cnf(d22, plain, ~aNaturalNumber0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp)) | ~aNaturalNumber0(sdtpldt0(xn,sdtpldt0(xp,xm))) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xm) | ~aNaturalNumber0(xp) | ~doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)) | ~isPrime0(xp), inference(resolution, [status(thm)], [c101,d21])). % 24.05/23.08 cnf(d23, plain, ~aNaturalNumber0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp)) | ~aNaturalNumber0(sdtpldt0(xn,sdtpldt0(xp,xm))) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xp) | ~doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)) | ~isPrime0(xp), inference(resolution, [status(thm)], [c71,d22])). % 24.05/23.08 cnf(d24, plain, ~aNaturalNumber0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp)) | ~aNaturalNumber0(sdtpldt0(xn,sdtpldt0(xp,xm))) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)) | ~isPrime0(xp), inference(resolution, [status(thm)], [c72,d23])). % 24.05/23.08 cnf(d25, plain, ~aNaturalNumber0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp)) | ~aNaturalNumber0(sdtpldt0(xn,sdtpldt0(xp,xm))) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~doDivides0(xp,sdtasdt0(sdtsldt0(xn,xr),xm)), inference(resolution, [status(thm)], [c74,d24])). % 24.05/23.08 cnf(d26, plain, ~aNaturalNumber0(sdtpldt0(sdtpldt0(sdtsldt0(xn,xr),xm),xp)) | ~aNaturalNumber0(sdtpldt0(xn,sdtpldt0(xp,xm))) | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [c98,d25])). % 24.05/23.08 cnf(d27, plain, ~aNaturalNumber0(sdtpldt0(xn,sdtpldt0(xp,xm))) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xp) | ~aNaturalNumber0(sdtpldt0(sdtsldt0(xn,xr),xm)), inference(resolution, [status(thm)], [d26,c3])). % 24.05/23.08 cnf(d28, plain, ~aNaturalNumber0(sdtpldt0(sdtsldt0(xn,xr),xm)) | ~aNaturalNumber0(sdtpldt0(xn,sdtpldt0(xp,xm))) | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [c72,d27])). % 24.05/23.08 cnf(d29, plain, ~aNaturalNumber0(sdtpldt0(sdtsldt0(xn,xr),xm)) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(sdtpldt0(xn,xm)), inference(resolution, [status(thm)], [d28,d16])). % 24.05/23.08 cnf(d30, plain, ~aNaturalNumber0(sdtpldt0(xn,xm)) | ~aNaturalNumber0(sdtsldt0(xn,xr)) | ~aNaturalNumber0(xm) | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [d29,c3])). % 24.05/23.08 cnf(d31, plain, ~aNaturalNumber0(sdtpldt0(xn,xm)) | ~aNaturalNumber0(sdtsldt0(xn,xr)), inference(resolution, [status(thm)], [c71,d30])). % 24.05/23.08 cnf(d32, plain, ~aNaturalNumber0(sdtpldt0(xn,xm)) | xr = sz00 | ~aNaturalNumber0(xn) | ~aNaturalNumber0(xr) | ~doDivides0(xr,xn), inference(resolution, [status(thm)], [d31,d0])). % 24.05/23.08 cnf(d33, plain, xr = sz00 | ~aNaturalNumber0(sdtpldt0(xn,xm)) | ~aNaturalNumber0(xr) | ~doDivides0(xr,xn), inference(resolution, [status(thm)], [c70,d32])). % 24.05/23.08 cnf(d34, plain, xr = sz00 | ~aNaturalNumber0(sdtpldt0(xn,xm)) | ~doDivides0(xr,xn), inference(resolution, [status(thm)], [c87,d33])). % 24.05/23.08 cnf(d35, plain, xr = sz00 | ~aNaturalNumber0(sdtpldt0(xn,xm)), inference(resolution, [status(thm)], [c95,d34])). % 24.05/23.08 cnf(d36, plain, xr = sz00 | ~aNaturalNumber0(xm) | ~aNaturalNumber0(xn), inference(resolution, [status(thm)], [d35,c3])). % 24.05/23.08 cnf(d37, plain, xr = sz00 | ~aNaturalNumber0(xm), inference(resolution, [status(thm)], [c70,d36])). % 24.05/23.08 cnf(d38, plain, xr = sz00, inference(resolution, [status(thm)], [c71,d37])). % 24.05/23.08 cnf(d39, plain, ~aNaturalNumber0(xr) | 'Ts80'(xr), inference(resolution, [status(thm)], [c58,c89])). % 24.05/23.08 cnf(d40, plain, 'Ts80'(xr), inference(resolution, [status(thm)], [c87,d39])). % 24.05/23.08 cnf(d41, plain, 'Ts80'(sz00), inference(demodulation, [status(thm)], [d40,d38])). % 24.05/23.08 cnf(d42, plain, ~'Ts80'(sz00), inference(equality_resolution, [status(thm)], [c60])). % 24.05/23.08 cnf(d43, plain, $false, inference(resolution, [status(thm)], [d42,d41])). % 24.05/23.08 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------