%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM433+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 : n009.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:43 AM UTC 2026 % Result : Theorem 24.20s 3.52s % Output : CNFRefutation 24.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM433+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.09/0.36 % Computer : n009.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 26 02:43:14 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 24.20/3.52 % SZS status Theorem for theBenchmark.p % 24.20/3.52 % SZS output start CNFRefutation for theBenchmark.p % 24.20/3.52 fof(mIntMult, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => aInteger0(sdtasdt0(X0,X1))))). % 24.20/3.52 fof(mMulAsso, axiom, ! [X0] : ! [X1] : ! [X2] : (((aInteger0(X0) & (aInteger0(X1) & aInteger0(X2))) => sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2)))). % 24.20/3.52 fof(mMulComm, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => sdtasdt0(X0,X1) = sdtasdt0(X1,X0)))). % 24.20/3.52 fof(mDivisor, definition, ! [X0] : ((aInteger0(X0) => ! [X1] : ((aDivisorOf0(X1,X0) <=> (aInteger0(X1) & (X1 != sz00 & ? [X2] : ((aInteger0(X2) & sdtasdt0(X1,X2) = X0))))))))). % 24.20/3.52 fof(m__979, hypothesis, (aInteger0(xa) & (aInteger0(xb) & (aInteger0(xp) & (xp != sz00 & (aInteger0(xq) & xq != sz00)))))). % 24.20/3.52 fof(m__, conjecture, ((sdtasdt0(xp,xq) != sz00 & (? [X0] : ((aInteger0(X0) & sdtasdt0(sdtasdt0(xp,xq),X0) = sdtpldt0(xa,smndt0(xb)))) & (aDivisorOf0(sdtasdt0(xp,xq),sdtpldt0(xa,smndt0(xb))) & sdteqdtlpzmzozddtrp0(xa,xb,sdtasdt0(xp,xq))))) => ((? [X0] : ((aInteger0(X0) & sdtasdt0(xp,X0) = sdtpldt0(xa,smndt0(xb)))) | (aDivisorOf0(xp,sdtpldt0(xa,smndt0(xb))) | sdteqdtlpzmzozddtrp0(xa,xb,xp))) & (? [X0] : ((aInteger0(X0) & sdtasdt0(xq,X0) = sdtpldt0(xa,smndt0(xb)))) | (aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb))) | sdteqdtlpzmzozddtrp0(xa,xb,xq)))))). % 24.20/3.52 fof(negated_conjecture, negated_conjecture, ~(((sdtasdt0(xp,xq) != sz00 & (? [X0] : ((aInteger0(X0) & sdtasdt0(sdtasdt0(xp,xq),X0) = sdtpldt0(xa,smndt0(xb)))) & (aDivisorOf0(sdtasdt0(xp,xq),sdtpldt0(xa,smndt0(xb))) & sdteqdtlpzmzozddtrp0(xa,xb,sdtasdt0(xp,xq))))) => ((? [X0] : ((aInteger0(X0) & sdtasdt0(xp,X0) = sdtpldt0(xa,smndt0(xb)))) | (aDivisorOf0(xp,sdtpldt0(xa,smndt0(xb))) | sdteqdtlpzmzozddtrp0(xa,xb,xp))) & (? [X0] : ((aInteger0(X0) & sdtasdt0(xq,X0) = sdtpldt0(xa,smndt0(xb)))) | (aDivisorOf0(xq,sdtpldt0(xa,smndt0(xb))) | sdteqdtlpzmzozddtrp0(xa,xb,xq)))))), inference(negate_conjecture, [status(cth)], [m__])). % 24.20/3.52 cnf(c4, plain, ~aInteger0(X0) | ~aInteger0(X1) | aInteger0(sdtasdt0(X0,X1)), inference(clausification, [status(esa)], [mIntMult])). % 24.20/3.52 cnf(c11, plain, ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(X2) | sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2), inference(clausification, [status(esa)], [mMulAsso])). % 24.20/3.52 cnf(c12, plain, ~aInteger0(X0) | ~aInteger0(X1) | sdtasdt0(X0,X1) = sdtasdt0(X1,X0), inference(clausification, [status(esa)], [mMulComm])). % 24.20/3.52 cnf(c22, plain, ~aInteger0(X0) | ~aDivisorOf0(X1,X0) | X2(X0,X1), inference(clausification, [status(esa)], [mDivisor])). % 24.20/3.52 cnf(c24, plain, ~X0(X1,X2) | aInteger0(X2), inference(clausification, [status(esa)], [mDivisor])). % 24.20/3.52 cnf(c36, plain, aInteger0(xp), inference(clausification, [status(esa)], [m__979])). % 24.20/3.52 cnf(c38, plain, aInteger0(xq), inference(clausification, [status(esa)], [m__979])). % 24.20/3.52 cnf(c41, plain, aInteger0(sK44), inference(clausification, [status(esa)], [negated_conjecture])). % 24.20/3.52 cnf(c42, plain, sdtasdt0(sdtasdt0(xp,xq),sK44) = sdtpldt0(xa,smndt0(xb)), inference(clausification, [status(esa)], [negated_conjecture])). % 24.20/3.52 cnf(c43, plain, aDivisorOf0(sdtasdt0(xp,xq),sdtpldt0(xa,smndt0(xb))), inference(clausification, [status(esa)], [negated_conjecture])). % 24.20/3.52 cnf(c45, plain, ~X0 | ~aInteger0(X1) | sdtasdt0(xq,X1) != sdtpldt0(xa,smndt0(xb)), inference(clausification, [status(esa)], [negated_conjecture])). % 24.20/3.52 cnf(c48, plain, X0 | ~aInteger0(X1) | sdtasdt0(xp,X1) != sdtpldt0(xa,smndt0(xb)), inference(clausification, [status(esa)], [negated_conjecture])). % 24.20/3.52 cnf(d0, plain, sdtasdt0(xp,sdtasdt0(xq,sK44)) = sdtpldt0(xa,smndt0(xb)) | ~aInteger0(xp) | ~aInteger0(xq) | ~aInteger0(sK44), inference(superposition, [status(thm)], [c11,c42])). % 24.20/3.52 cnf(d1, plain, sdtasdt0(xp,sdtasdt0(xq,sK44)) = sdtpldt0(xa,smndt0(xb)) | ~aInteger0(xp) | ~aInteger0(xq), inference(resolution, [status(thm)], [c41,d0])). % 24.20/3.52 cnf(d2, plain, sdtasdt0(xp,sdtasdt0(xq,sK44)) = sdtpldt0(xa,smndt0(xb)) | ~aInteger0(xq), inference(resolution, [status(thm)], [c36,d1])). % 24.20/3.52 cnf(d3, plain, sdtasdt0(xp,sdtasdt0(xq,sK44)) = sdtpldt0(xa,smndt0(xb)), inference(resolution, [status(thm)], [c38,d2])). % 24.20/3.52 cnf(d4, plain, sdtpldt0(xa,smndt0(xb)) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(sdtasdt0(xq,sK44)) | 'Ts43', inference(superposition, [status(thm)], [d3,c48])). % 24.20/3.52 cnf(d5, plain, ~aInteger0(sdtasdt0(xq,sK44)) | 'Ts43', inference(equality_resolution, [status(thm)], [d4])). % 24.20/3.52 cnf(d6, plain, 'Ts43' | ~aInteger0(sK44) | ~aInteger0(xq), inference(resolution, [status(thm)], [d5,c4])). % 24.20/3.52 cnf(d7, plain, ~aInteger0(xq) | 'Ts43', inference(resolution, [status(thm)], [c41,d6])). % 24.20/3.52 cnf(d8, plain, 'Ts43', inference(resolution, [status(thm)], [c38,d7])). % 24.20/3.52 cnf(d9, plain, sdtasdt0(xq,X0) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(X0), inference(resolution, [status(thm)], [d8,c45])). % 24.20/3.52 cnf(d10, plain, sdtasdt0(X0,xq) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(X0) | ~aInteger0(X0) | ~aInteger0(xq), inference(superposition, [status(thm)], [c12,d9])). % 24.20/3.52 cnf(d11, plain, sdtasdt0(X0,xq) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(X0), inference(resolution, [status(thm)], [c38,d10])). % 24.20/3.52 cnf(d12, plain, sdtasdt0(X0,sdtasdt0(X1,xq)) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(sdtasdt0(X0,X1)) | ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(xq), inference(superposition, [status(thm)], [c11,d11])). % 24.20/3.52 cnf(d13, plain, sdtasdt0(X0,sdtasdt0(X1,xq)) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(X1) | ~aInteger0(X0) | ~aInteger0(sdtasdt0(X0,X1)), inference(resolution, [status(thm)], [c38,d12])). % 24.20/3.52 cnf(d14, plain, sdtasdt0(sK44,sdtasdt0(xp,xq)) = sdtpldt0(xa,smndt0(xb)) | ~aInteger0(sK44) | ~aInteger0(sdtasdt0(xp,xq)), inference(superposition, [status(thm)], [c12,c42])). % 24.20/3.52 cnf(d15, plain, sdtasdt0(sK44,sdtasdt0(xp,xq)) = sdtpldt0(xa,smndt0(xb)) | ~aInteger0(sdtasdt0(xp,xq)), inference(resolution, [status(thm)], [c41,d14])). % 24.20/3.52 cnf(d16, plain, ~aInteger0(sdtpldt0(xa,smndt0(xb))) | 'Ts26'(sdtpldt0(xa,smndt0(xb)),sdtasdt0(xp,xq)), inference(resolution, [status(thm)], [c22,c43])). % 24.20/3.52 cnf(d17, plain, ~aInteger0(sdtpldt0(xa,smndt0(xb))) | aInteger0(sdtasdt0(xp,xq)), inference(resolution, [status(thm)], [d16,c24])). % 24.20/3.52 cnf(d18, plain, aInteger0(sdtpldt0(xa,smndt0(xb))) | ~aInteger0(sdtasdt0(xq,sK44)) | ~aInteger0(xp), inference(superposition, [status(thm)], [d3,c4])). % 24.20/3.52 cnf(d19, plain, aInteger0(sdtpldt0(xa,smndt0(xb))) | ~aInteger0(sdtasdt0(xq,sK44)), inference(resolution, [status(thm)], [c36,d18])). % 24.20/3.52 cnf(d20, plain, ~aInteger0(sdtasdt0(xq,sK44)) | aInteger0(sdtasdt0(xp,xq)), inference(resolution, [status(thm)], [d19,d17])). % 24.20/3.52 cnf(d21, plain, aInteger0(sdtasdt0(xp,xq)) | ~aInteger0(sK44) | ~aInteger0(xq), inference(resolution, [status(thm)], [d20,c4])). % 24.20/3.52 cnf(d22, plain, aInteger0(sdtasdt0(xp,xq)) | ~aInteger0(xq), inference(resolution, [status(thm)], [c41,d21])). % 24.20/3.52 cnf(d23, plain, aInteger0(sdtasdt0(xp,xq)), inference(resolution, [status(thm)], [c38,d22])). % 24.20/3.52 cnf(d24, plain, sdtasdt0(sK44,sdtasdt0(xp,xq)) = sdtpldt0(xa,smndt0(xb)), inference(resolution, [status(thm)], [d23,d15])). % 24.20/3.52 cnf(d25, plain, sdtpldt0(xa,smndt0(xb)) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(xp) | ~aInteger0(sK44) | ~aInteger0(sdtasdt0(sK44,xp)), inference(superposition, [status(thm)], [d24,d13])). % 24.20/3.52 cnf(d26, plain, sdtpldt0(xa,smndt0(xb)) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(sdtasdt0(sK44,xp)) | ~aInteger0(xp), inference(resolution, [status(thm)], [c41,d25])). % 24.20/3.52 cnf(d27, plain, sdtpldt0(xa,smndt0(xb)) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(sdtasdt0(sK44,xp)), inference(resolution, [status(thm)], [c36,d26])). % 24.20/3.52 cnf(d28, plain, sdtasdt0(xp,sdtasdt0(xq,sK44)) = sdtpldt0(xa,smndt0(xb)) | ~aInteger0(xp) | ~aInteger0(xq) | ~aInteger0(sK44), inference(superposition, [status(thm)], [c42,c11])). % 24.20/3.52 cnf(d29, plain, sdtpldt0(xa,smndt0(xb)) = sdtpldt0(xa,smndt0(xb)) | ~aInteger0(xp) | ~aInteger0(xq) | ~aInteger0(sK44), inference(demodulation, [status(thm)], [d28,d3])). % 24.20/3.52 cnf(d30, plain, sdtpldt0(xa,smndt0(xb)) = sdtpldt0(xa,smndt0(xb)) | ~aInteger0(xp) | ~aInteger0(xq), inference(resolution, [status(thm)], [c41,d29])). % 24.20/3.52 cnf(d31, plain, sdtpldt0(xa,smndt0(xb)) = sdtpldt0(xa,smndt0(xb)) | ~aInteger0(xq), inference(resolution, [status(thm)], [c36,d30])). % 24.20/3.52 cnf(d32, plain, sdtpldt0(xa,smndt0(xb)) = sdtpldt0(xa,smndt0(xb)), inference(resolution, [status(thm)], [c38,d31])). % 24.20/3.52 cnf(d33, plain, ~aInteger0(sdtasdt0(sK44,xp)), inference(resolution, [status(thm)], [d32,d27])). % 24.20/3.52 cnf(d34, plain, ~aInteger0(xp) | ~aInteger0(sK44), inference(resolution, [status(thm)], [d33,c4])). % 24.20/3.52 cnf(d35, plain, ~aInteger0(xp), inference(resolution, [status(thm)], [c41,d34])). % 24.20/3.52 cnf(d36, plain, $false, inference(resolution, [status(thm)], [c36,d35])). % 24.20/3.52 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------