%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM452+6 : 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 : n020.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:46 AM UTC 2026 % Result : Theorem 45.74s 7.11s % Output : CNFRefutation 45.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM452+6 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.08/0.35 % Computer : n020.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sat Sep 26 02:49:03 UTC 2026 % 0.08/0.36 % CPUTime : % 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 45.74/7.11 % SZS status Theorem for theBenchmark.p % 45.74/7.11 % SZS output start CNFRefutation for theBenchmark.p % 45.74/7.11 fof(mIntZero, axiom, aInteger0(sz00)). % 45.74/7.11 fof(mIntOne, axiom, aInteger0(sz10)). % 45.74/7.11 fof(mIntNeg, axiom, ! [X0] : ((aInteger0(X0) => aInteger0(smndt0(X0))))). % 45.74/7.11 fof(mAddAsso, axiom, ! [X0] : ! [X1] : ! [X2] : (((aInteger0(X0) & (aInteger0(X1) & aInteger0(X2))) => sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)))). % 45.74/7.11 fof(mAddComm, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => sdtpldt0(X0,X1) = sdtpldt0(X1,X0)))). % 45.74/7.11 fof(mAddZero, axiom, ! [X0] : ((aInteger0(X0) => (sdtpldt0(X0,sz00) = X0 & X0 = sdtpldt0(sz00,X0))))). % 45.74/7.11 fof(mAddNeg, axiom, ! [X0] : ((aInteger0(X0) => (sdtpldt0(X0,smndt0(X0)) = sz00 & sz00 = sdtpldt0(smndt0(X0),X0))))). % 45.74/7.11 fof(mMulComm, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => sdtasdt0(X0,X1) = sdtasdt0(X1,X0)))). % 45.74/7.11 fof(mMulOne, axiom, ! [X0] : ((aInteger0(X0) => (sdtasdt0(X0,sz10) = X0 & X0 = sdtasdt0(sz10,X0))))). % 45.74/7.11 fof(mMulMinOne, axiom, ! [X0] : ((aInteger0(X0) => (sdtasdt0(smndt0(sz10),X0) = smndt0(X0) & smndt0(X0) = sdtasdt0(X0,smndt0(sz10)))))). % 45.74/7.11 fof(m__2079, hypothesis, (aSet0(sbsmnsldt0(xS)) & (! [X0] : ((aElementOf0(X0,sbsmnsldt0(xS)) <=> (aInteger0(X0) & ? [X1] : ((aElementOf0(X1,xS) & aElementOf0(X0,X1)))))) & (aSet0(stldt0(sbsmnsldt0(xS))) & (! [X0] : ((aElementOf0(X0,stldt0(sbsmnsldt0(xS))) <=> (aInteger0(X0) & ~aElementOf0(X0,sbsmnsldt0(xS))))) & (! [X0] : ((aElementOf0(X0,stldt0(sbsmnsldt0(xS))) <=> (X0 = sz10 | X0 = smndt0(sz10)))) & stldt0(sbsmnsldt0(xS)) = cS2076)))))). % 45.74/7.11 fof(m__2171, hypothesis, (aInteger0(xp) & (xp != sz00 & (aSet0(szAzrzSzezqlpdtcmdtrp0(sz10,xp)) & (! [X0] : (((aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) => (aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)))) & (aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10))) & sdteqdtlpzmzozddtrp0(X0,sz10,xp))))) & ((aInteger0(X0) & (? [X1] : ((aInteger0(X1) & sdtasdt0(xp,X1) = sdtpldt0(X0,smndt0(sz10)))) | (aDivisorOf0(xp,sdtpldt0(X0,smndt0(sz10))) | sdteqdtlpzmzozddtrp0(X0,sz10,xp)))) => aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp))))) & (aSet0(sbsmnsldt0(xS)) & (! [X0] : ((aElementOf0(X0,sbsmnsldt0(xS)) <=> (aInteger0(X0) & ? [X1] : ((aElementOf0(X1,xS) & aElementOf0(X0,X1)))))) & (! [X0] : ((aElementOf0(X0,stldt0(sbsmnsldt0(xS))) <=> (aInteger0(X0) & ~aElementOf0(X0,sbsmnsldt0(xS))))) & (! [X0] : ((aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) => aElementOf0(X0,stldt0(sbsmnsldt0(xS))))) & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS)))))))))))). % 45.74/7.11 fof(m__, conjecture, ((? [X0] : ((aInteger0(X0) & sdtasdt0(xp,X0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))) | (aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))) | (sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp) | aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))))) & (? [X0] : ((aInteger0(X0) & sdtasdt0(xp,X0) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))) | (aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))) | (sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp) | aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))))))). % 45.74/7.11 fof(negated_conjecture, negated_conjecture, ~(((? [X0] : ((aInteger0(X0) & sdtasdt0(xp,X0) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)))) | (aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10))) | (sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,xp),sz10,xp) | aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp))))) & (? [X0] : ((aInteger0(X0) & sdtasdt0(xp,X0) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)))) | (aDivisorOf0(xp,sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10))) | (sdteqdtlpzmzozddtrp0(sdtpldt0(sz10,smndt0(xp)),sz10,xp) | aElementOf0(sdtpldt0(sz10,smndt0(xp)),szAzrzSzezqlpdtcmdtrp0(sz10,xp))))))), inference(negate_conjecture, [status(cth)], [m__])). % 45.74/7.11 cnf(c0, plain, aInteger0(sz00), inference(clausification, [status(esa)], [mIntZero])). % 45.74/7.11 cnf(c1, plain, aInteger0(sz10), inference(clausification, [status(esa)], [mIntOne])). % 45.74/7.11 cnf(c2, plain, ~aInteger0(X0) | aInteger0(smndt0(X0)), inference(clausification, [status(esa)], [mIntNeg])). % 45.74/7.11 cnf(c5, plain, ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(X2) | sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2), inference(clausification, [status(esa)], [mAddAsso])). % 45.74/7.11 cnf(c6, plain, ~aInteger0(X0) | ~aInteger0(X1) | sdtpldt0(X0,X1) = sdtpldt0(X1,X0), inference(clausification, [status(esa)], [mAddComm])). % 45.74/7.11 cnf(c7, plain, ~aInteger0(X0) | sdtpldt0(X0,sz00) = X0, inference(clausification, [status(esa)], [mAddZero])). % 45.74/7.11 cnf(c8, plain, ~aInteger0(X0) | X0 = sdtpldt0(sz00,X0), inference(clausification, [status(esa)], [mAddZero])). % 45.74/7.11 cnf(c9, plain, ~aInteger0(X0) | sdtpldt0(X0,smndt0(X0)) = sz00, inference(clausification, [status(esa)], [mAddNeg])). % 45.74/7.11 cnf(c12, plain, ~aInteger0(X0) | ~aInteger0(X1) | sdtasdt0(X0,X1) = sdtasdt0(X1,X0), inference(clausification, [status(esa)], [mMulComm])). % 45.74/7.11 cnf(c14, plain, ~aInteger0(X0) | X0 = sdtasdt0(sz10,X0), inference(clausification, [status(esa)], [mMulOne])). % 45.74/7.11 cnf(c20, plain, ~aInteger0(X0) | smndt0(X0) = sdtasdt0(X0,smndt0(sz10)), inference(clausification, [status(esa)], [mMulMinOne])). % 45.74/7.11 cnf(c168, plain, ~aElementOf0(X0,stldt0(sbsmnsldt0(xS))) | aInteger0(X0), inference(clausification, [status(esa)], [m__2079])). % 45.74/7.11 cnf(c173, plain, aElementOf0(X0,stldt0(sbsmnsldt0(xS))) | X0 != smndt0(sz10), inference(clausification, [status(esa)], [m__2079])). % 45.74/7.11 cnf(c174, plain, stldt0(sbsmnsldt0(xS)) = cS2076, inference(clausification, [status(esa)], [m__2079])). % 45.74/7.11 cnf(c224, plain, aInteger0(xp), inference(clausification, [status(esa)], [m__2171])). % 45.74/7.11 cnf(c246, plain, ~X0 | ~aInteger0(X1) | sdtasdt0(xp,X1) != sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)), inference(clausification, [status(esa)], [negated_conjecture])). % 45.74/7.11 cnf(c250, plain, X0 | ~aInteger0(X1) | sdtasdt0(xp,X1) != sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)), inference(clausification, [status(esa)], [negated_conjecture])). % 45.74/7.11 cnf(d0, plain, sdtasdt0(xp,X0) != sdtpldt0(sz10,sdtpldt0(smndt0(xp),smndt0(sz10))) | ~aInteger0(X0) | ~'Ts160' | ~aInteger0(smndt0(sz10)) | ~aInteger0(smndt0(xp)) | ~aInteger0(sz10), inference(superposition, [status(thm)], [c5,c246])). % 45.74/7.11 cnf(d1, plain, sdtasdt0(xp,X0) != sdtpldt0(sz10,sdtpldt0(smndt0(xp),smndt0(sz10))) | ~aInteger0(X0) | ~aInteger0(smndt0(sz10)) | ~aInteger0(smndt0(xp)) | ~'Ts160', inference(resolution, [status(thm)], [c1,d0])). % 45.74/7.11 cnf(d2, plain, sdtasdt0(xp,X0) != sdtpldt0(sz10,sdtpldt0(smndt0(sz10),smndt0(xp))) | ~aInteger0(X0) | ~aInteger0(smndt0(sz10)) | ~aInteger0(smndt0(xp)) | ~'Ts160' | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(sz10)), inference(superposition, [status(thm)], [c6,d1])). % 45.74/7.11 cnf(d3, plain, aInteger0(X0) | ~aElementOf0(X0,cS2076), inference(demodulation, [status(thm)], [c168,c174])). % 45.74/7.11 cnf(d4, plain, X0 != smndt0(sz10) | aElementOf0(X0,cS2076), inference(demodulation, [status(thm)], [c173,c174])). % 45.74/7.11 cnf(d5, plain, aElementOf0(smndt0(sz10),cS2076), inference(equality_resolution, [status(thm)], [d4])). % 45.74/7.11 cnf(d6, plain, aInteger0(smndt0(sz10)), inference(resolution, [status(thm)], [d5,d3])). % 45.74/7.11 cnf(d7, plain, sdtasdt0(xp,X0) != sdtpldt0(sz10,sdtpldt0(smndt0(sz10),smndt0(xp))) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)) | ~'Ts160', inference(resolution, [status(thm)], [d6,d2])). % 45.74/7.11 cnf(d8, plain, sdtasdt0(X0,xp) != sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)) | ~aInteger0(X0) | 'Ts160' | ~aInteger0(X0) | ~aInteger0(xp), inference(superposition, [status(thm)], [c12,c250])). % 45.74/7.11 cnf(d9, plain, sdtasdt0(X0,xp) != sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)) | ~aInteger0(X0) | 'Ts160', inference(resolution, [status(thm)], [c224,d8])). % 45.74/7.11 cnf(d10, plain, sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X1,X0),X2) | ~aInteger0(X2) | ~aInteger0(X1) | ~aInteger0(X0) | ~aInteger0(X0) | ~aInteger0(X1), inference(superposition, [status(thm)], [c6,c5])). % 45.74/7.11 cnf(d11, plain, sdtasdt0(X0,xp) != sdtpldt0(xp,sdtpldt0(sz10,smndt0(sz10))) | ~aInteger0(X0) | 'Ts160' | ~aInteger0(smndt0(sz10)) | ~aInteger0(sz10) | ~aInteger0(xp), inference(superposition, [status(thm)], [d10,d9])). % 45.74/7.11 cnf(d12, plain, sdtasdt0(X0,xp) != sdtpldt0(xp,sdtpldt0(sz10,smndt0(sz10))) | ~aInteger0(X0) | ~aInteger0(smndt0(sz10)) | ~aInteger0(xp) | 'Ts160', inference(resolution, [status(thm)], [c1,d11])). % 45.74/7.11 cnf(d13, plain, sdtasdt0(X0,xp) != sdtpldt0(xp,sdtpldt0(sz10,smndt0(sz10))) | ~aInteger0(X0) | ~aInteger0(smndt0(sz10)) | 'Ts160', inference(resolution, [status(thm)], [c224,d12])). % 45.74/7.11 cnf(d14, plain, sdtasdt0(X0,xp) != sdtpldt0(xp,sdtpldt0(sz10,smndt0(sz10))) | ~aInteger0(X0) | 'Ts160', inference(resolution, [status(thm)], [d6,d13])). % 45.74/7.11 cnf(d15, plain, sdtasdt0(X0,xp) != sdtpldt0(xp,sz00) | ~aInteger0(X0) | 'Ts160' | ~aInteger0(sz10), inference(superposition, [status(thm)], [c9,d14])). % 45.74/7.11 cnf(d16, plain, sdtasdt0(X0,xp) != sdtpldt0(xp,sz00) | ~aInteger0(X0) | 'Ts160', inference(resolution, [status(thm)], [c1,d15])). % 45.74/7.11 cnf(d17, plain, xp != sdtpldt0(xp,sz00) | ~aInteger0(sz10) | 'Ts160' | ~aInteger0(xp), inference(superposition, [status(thm)], [c14,d16])). % 45.74/7.11 cnf(d18, plain, xp != sdtpldt0(xp,sz00) | ~aInteger0(xp) | 'Ts160', inference(resolution, [status(thm)], [c1,d17])). % 45.74/7.11 cnf(d19, plain, xp != sdtpldt0(xp,sz00) | 'Ts160', inference(resolution, [status(thm)], [c224,d18])). % 45.74/7.11 cnf(d20, plain, X0 = sdtpldt0(X0,sz00) | ~aInteger0(X0) | ~aInteger0(sz00) | ~aInteger0(X0), inference(superposition, [status(thm)], [c6,c8])). % 45.74/7.11 cnf(d21, plain, X0 = sdtpldt0(X0,sz00) | ~aInteger0(X0), inference(resolution, [status(thm)], [c0,d20])). % 45.74/7.11 cnf(d22, plain, xp != xp | 'Ts160' | ~aInteger0(xp), inference(superposition, [status(thm)], [d21,d19])). % 45.74/7.11 cnf(d23, plain, xp != xp | 'Ts160', inference(resolution, [status(thm)], [c224,d22])). % 45.74/7.11 cnf(d24, plain, 'Ts160', inference(equality_resolution, [status(thm)], [d23])). % 45.74/7.11 cnf(d25, plain, sdtasdt0(xp,X0) != sdtpldt0(sz10,sdtpldt0(smndt0(sz10),smndt0(xp))) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [d24,d7])). % 45.74/7.11 cnf(d26, plain, sdtpldt0(X0,sdtpldt0(smndt0(X0),X1)) = sdtpldt0(sz00,X1) | ~aInteger0(X1) | ~aInteger0(smndt0(X0)) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [c9,c5])). % 45.74/7.11 cnf(d27, plain, sdtasdt0(xp,X0) != sdtpldt0(sz00,smndt0(xp)) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)) | ~aInteger0(sz10) | ~aInteger0(smndt0(sz10)), inference(superposition, [status(thm)], [d26,d25])). % 45.74/7.11 cnf(d28, plain, sdtasdt0(xp,X0) != sdtpldt0(sz00,smndt0(xp)) | ~aInteger0(X0) | ~aInteger0(smndt0(sz10)) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c1,d27])). % 45.74/7.11 cnf(d29, plain, sdtasdt0(xp,X0) != sdtpldt0(sz00,smndt0(xp)) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [d6,d28])). % 45.74/7.11 cnf(d30, plain, sdtpldt0(sz00,X0) = X0 | ~aInteger0(X0) | ~aInteger0(X0) | ~aInteger0(sz00), inference(superposition, [status(thm)], [c6,c7])). % 45.74/7.11 cnf(d31, plain, sdtpldt0(sz00,X0) = X0 | ~aInteger0(X0), inference(resolution, [status(thm)], [c0,d30])). % 45.74/7.11 cnf(d32, plain, sdtasdt0(xp,X0) != smndt0(xp) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d31,d29])). % 45.74/7.11 cnf(d33, plain, smndt0(xp) != smndt0(xp) | ~aInteger0(smndt0(sz10)) | ~aInteger0(smndt0(xp)) | ~aInteger0(xp), inference(superposition, [status(thm)], [c20,d32])). % 45.74/7.11 cnf(d34, plain, smndt0(xp) != smndt0(xp) | ~aInteger0(smndt0(sz10)) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d33])). % 45.74/7.11 cnf(d35, plain, smndt0(xp) != smndt0(xp) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [d6,d34])). % 45.74/7.11 cnf(d36, plain, ~aInteger0(smndt0(xp)), inference(equality_resolution, [status(thm)], [d35])). % 45.74/7.11 cnf(d37, plain, ~aInteger0(xp), inference(resolution, [status(thm)], [d36,c2])). % 45.74/7.11 cnf(d38, plain, $false, inference(resolution, [status(thm)], [c224,d37])). % 45.74/7.11 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------