%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM436+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 : n010.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:44 AM UTC 2026 % Result : Theorem 14.51s 3.90s % Output : CNFRefutation 14.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : NUM436+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.18/0.42 % Computer : n010.cluster.edu % 0.18/0.42 % Model : x86_64 x86_64 % 0.18/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.42 % Memory : 8046.5625MB % 0.18/0.42 % OS : Linux 6.8.0-71-generic % 0.18/0.42 % CPULimit : 300 % 0.18/0.42 % WCLimit : 300 % 0.18/0.42 % DateTime : Sat Sep 26 02:44:00 UTC 2026 % 0.18/0.42 % CPUTime : % 0.18/0.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 14.51/3.90 % SZS status Theorem for theBenchmark.p % 14.51/3.90 % SZS output start CNFRefutation for theBenchmark.p % 14.51/3.90 fof(mIntMult, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => aInteger0(sdtasdt0(X0,X1))))). % 14.51/3.90 fof(m__979, hypothesis, (aInteger0(xa) & (aInteger0(xb) & (aInteger0(xp) & (xp != sz00 & (aInteger0(xq) & xq != sz00)))))). % 14.51/3.90 fof(m__1032, hypothesis, (aInteger0(xm) & sdtasdt0(sdtasdt0(xp,xq),xm) = sdtpldt0(xa,smndt0(xb)))). % 14.51/3.90 fof(m__1071, hypothesis, (sdtasdt0(xp,sdtasdt0(xq,xm)) = sdtpldt0(xa,smndt0(xb)) & sdtpldt0(xa,smndt0(xb)) = sdtasdt0(xq,sdtasdt0(xp,xm)))). % 14.51/3.90 fof(m__, conjecture, ((? [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))))). % 14.51/3.90 fof(negated_conjecture, negated_conjecture, ~(((? [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__])). % 14.51/3.90 cnf(c4, plain, ~aInteger0(X0) | ~aInteger0(X1) | aInteger0(sdtasdt0(X0,X1)), inference(clausification, [status(esa)], [mIntMult])). % 14.51/3.90 cnf(c36, plain, aInteger0(xp), inference(clausification, [status(esa)], [m__979])). % 14.51/3.90 cnf(c38, plain, aInteger0(xq), inference(clausification, [status(esa)], [m__979])). % 14.51/3.90 cnf(c45, plain, aInteger0(xm), inference(clausification, [status(esa)], [m__1032])). % 14.51/3.90 cnf(c47, plain, sdtasdt0(xp,sdtasdt0(xq,xm)) = sdtpldt0(xa,smndt0(xb)), inference(clausification, [status(esa)], [m__1071])). % 14.51/3.90 cnf(c48, plain, sdtpldt0(xa,smndt0(xb)) = sdtasdt0(xq,sdtasdt0(xp,xm)), inference(clausification, [status(esa)], [m__1071])). % 14.51/3.90 cnf(c49, plain, ~X0 | ~aInteger0(X1) | sdtasdt0(xq,X1) != sdtpldt0(xa,smndt0(xb)), inference(clausification, [status(esa)], [negated_conjecture])). % 14.51/3.90 cnf(c52, plain, X0 | ~aInteger0(X1) | sdtasdt0(xp,X1) != sdtpldt0(xa,smndt0(xb)), inference(clausification, [status(esa)], [negated_conjecture])). % 14.51/3.90 cnf(d0, plain, sdtpldt0(xa,smndt0(xb)) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(sdtasdt0(xq,xm)) | 'Ts44', inference(superposition, [status(thm)], [c47,c52])). % 14.51/3.90 cnf(d1, plain, ~aInteger0(sdtasdt0(xq,xm)) | 'Ts44', inference(equality_resolution, [status(thm)], [d0])). % 14.51/3.90 cnf(d2, plain, 'Ts44' | ~aInteger0(xm) | ~aInteger0(xq), inference(resolution, [status(thm)], [d1,c4])). % 14.51/3.90 cnf(d3, plain, ~aInteger0(xm) | 'Ts44', inference(resolution, [status(thm)], [c38,d2])). % 14.51/3.90 cnf(d4, plain, 'Ts44', inference(resolution, [status(thm)], [c45,d3])). % 14.51/3.90 cnf(d5, plain, sdtasdt0(xq,X0) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(X0), inference(resolution, [status(thm)], [d4,c49])). % 14.51/3.90 cnf(d6, plain, sdtpldt0(xa,smndt0(xb)) != sdtpldt0(xa,smndt0(xb)) | ~aInteger0(sdtasdt0(xp,xm)), inference(superposition, [status(thm)], [c48,d5])). % 14.51/3.90 cnf(d7, plain, ~aInteger0(sdtasdt0(xp,xm)), inference(equality_resolution, [status(thm)], [d6])). % 14.51/3.90 cnf(d8, plain, ~aInteger0(xm) | ~aInteger0(xp), inference(resolution, [status(thm)], [d7,c4])). % 14.51/3.90 cnf(d9, plain, ~aInteger0(xm), inference(resolution, [status(thm)], [c36,d8])). % 14.51/3.90 cnf(d10, plain, $false, inference(resolution, [status(thm)], [c45,d9])). % 14.51/3.90 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------