%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM454+6 : 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 : n026.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:47 AM UTC 2026 % Result : Theorem 137.93s 28.45s % Output : CNFRefutation 137.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM454+6 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.11/5.37 % Computer : n026.cluster.edu % 0.11/5.37 % Model : x86_64 x86_64 % 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/5.37 % Memory : 8046.5625MB % 0.11/5.37 % OS : Linux 6.8.0-71-generic % 0.11/5.37 % CPULimit : 300 % 0.11/5.37 % WCLimit : 300 % 0.11/5.37 % DateTime : Sat Sep 26 02:51:33 UTC 2026 % 0.11/5.38 % CPUTime : % 0.11/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 137.93/28.45 % SZS status Theorem for theBenchmark.p % 137.93/28.45 % SZS output start CNFRefutation for theBenchmark.p % 137.93/28.45 fof(mIntZero, axiom, aInteger0(sz00)). % 137.93/28.45 fof(mIntOne, axiom, aInteger0(sz10)). % 137.93/28.45 fof(mIntPlus, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => aInteger0(sdtpldt0(X0,X1))))). % 137.93/28.45 fof(mIntMult, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => aInteger0(sdtasdt0(X0,X1))))). % 137.93/28.45 fof(mAddAsso, axiom, ! [X0] : ! [X1] : ! [X2] : (((aInteger0(X0) & (aInteger0(X1) & aInteger0(X2))) => sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)))). % 137.93/28.45 fof(mAddComm, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => sdtpldt0(X0,X1) = sdtpldt0(X1,X0)))). % 137.93/28.45 fof(mAddZero, axiom, ! [X0] : ((aInteger0(X0) => (sdtpldt0(X0,sz00) = X0 & X0 = sdtpldt0(sz00,X0))))). % 137.93/28.45 fof(mAddNeg, axiom, ! [X0] : ((aInteger0(X0) => (sdtpldt0(X0,smndt0(X0)) = sz00 & sz00 = sdtpldt0(smndt0(X0),X0))))). % 137.93/28.45 fof(mMulAsso, axiom, ! [X0] : ! [X1] : ! [X2] : (((aInteger0(X0) & (aInteger0(X1) & aInteger0(X2))) => sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2)))). % 137.93/28.45 fof(mMulComm, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => sdtasdt0(X0,X1) = sdtasdt0(X1,X0)))). % 137.93/28.45 fof(mMulOne, axiom, ! [X0] : ((aInteger0(X0) => (sdtasdt0(X0,sz10) = X0 & X0 = sdtasdt0(sz10,X0))))). % 137.93/28.45 fof(mDistrib, axiom, ! [X0] : ! [X1] : ! [X2] : (((aInteger0(X0) & (aInteger0(X1) & aInteger0(X2))) => (sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) & sdtasdt0(sdtpldt0(X0,X1),X2) = sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)))))). % 137.93/28.45 fof(mMulZero, axiom, ! [X0] : ((aInteger0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 137.93/28.45 fof(mMulMinOne, axiom, ! [X0] : ((aInteger0(X0) => (sdtasdt0(smndt0(sz10),X0) = smndt0(X0) & smndt0(X0) = sdtasdt0(X0,smndt0(sz10)))))). % 137.93/28.45 fof(mZeroDiv, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => (sdtasdt0(X0,X1) = sz00 => (X0 = sz00 | X1 = sz00))))). % 137.93/28.45 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)))))))))))). % 137.93/28.45 fof(m__2232, hypothesis, (? [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)))))))))). % 137.93/28.45 fof(m__, conjecture, (sdtpldt0(sz10,xp) != smndt0(sz10) | sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10))). % 137.93/28.45 fof(negated_conjecture, negated_conjecture, ~((sdtpldt0(sz10,xp) != smndt0(sz10) | sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10))), inference(negate_conjecture, [status(cth)], [m__])). % 137.93/28.45 cnf(c0, plain, aInteger0(sz00), inference(clausification, [status(esa)], [mIntZero])). % 137.93/28.45 cnf(c1, plain, aInteger0(sz10), inference(clausification, [status(esa)], [mIntOne])). % 137.93/28.45 cnf(c3, plain, ~aInteger0(X0) | ~aInteger0(X1) | aInteger0(sdtpldt0(X0,X1)), inference(clausification, [status(esa)], [mIntPlus])). % 137.93/28.45 cnf(c4, plain, ~aInteger0(X0) | ~aInteger0(X1) | aInteger0(sdtasdt0(X0,X1)), inference(clausification, [status(esa)], [mIntMult])). % 137.93/28.45 cnf(c5, plain, ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(X2) | sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2), inference(clausification, [status(esa)], [mAddAsso])). % 137.93/28.45 cnf(c6, plain, ~aInteger0(X0) | ~aInteger0(X1) | sdtpldt0(X0,X1) = sdtpldt0(X1,X0), inference(clausification, [status(esa)], [mAddComm])). % 137.93/28.45 cnf(c7, plain, ~aInteger0(X0) | sdtpldt0(X0,sz00) = X0, inference(clausification, [status(esa)], [mAddZero])). % 137.93/28.45 cnf(c8, plain, ~aInteger0(X0) | X0 = sdtpldt0(sz00,X0), inference(clausification, [status(esa)], [mAddZero])). % 137.93/28.45 cnf(c9, plain, ~aInteger0(X0) | sdtpldt0(X0,smndt0(X0)) = sz00, inference(clausification, [status(esa)], [mAddNeg])). % 137.93/28.45 cnf(c10, plain, ~aInteger0(X0) | sz00 = sdtpldt0(smndt0(X0),X0), inference(clausification, [status(esa)], [mAddNeg])). % 137.93/28.45 cnf(c11, plain, ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(X2) | sdtasdt0(X0,sdtasdt0(X1,X2)) = sdtasdt0(sdtasdt0(X0,X1),X2), inference(clausification, [status(esa)], [mMulAsso])). % 137.93/28.45 cnf(c12, plain, ~aInteger0(X0) | ~aInteger0(X1) | sdtasdt0(X0,X1) = sdtasdt0(X1,X0), inference(clausification, [status(esa)], [mMulComm])). % 137.93/28.45 cnf(c13, plain, ~aInteger0(X0) | sdtasdt0(X0,sz10) = X0, inference(clausification, [status(esa)], [mMulOne])). % 137.93/28.45 cnf(c14, plain, ~aInteger0(X0) | X0 = sdtasdt0(sz10,X0), inference(clausification, [status(esa)], [mMulOne])). % 137.93/28.45 cnf(c15, plain, ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(X2) | sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)), inference(clausification, [status(esa)], [mDistrib])). % 137.93/28.45 cnf(c16, plain, ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(X2) | sdtasdt0(sdtpldt0(X0,X1),X2) = sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)), inference(clausification, [status(esa)], [mDistrib])). % 137.93/28.45 cnf(c17, plain, ~aInteger0(X0) | sdtasdt0(X0,sz00) = sz00, inference(clausification, [status(esa)], [mMulZero])). % 137.93/28.45 cnf(c18, plain, ~aInteger0(X0) | sz00 = sdtasdt0(sz00,X0), inference(clausification, [status(esa)], [mMulZero])). % 137.93/28.45 cnf(c19, plain, ~aInteger0(X0) | sdtasdt0(smndt0(sz10),X0) = smndt0(X0), inference(clausification, [status(esa)], [mMulMinOne])). % 137.93/28.45 cnf(c20, plain, ~aInteger0(X0) | smndt0(X0) = sdtasdt0(X0,smndt0(sz10)), inference(clausification, [status(esa)], [mMulMinOne])). % 137.93/28.45 cnf(c21, plain, X0 = sz00 | sdtasdt0(X0,X1) != sz00 | ~aInteger0(X0) | ~aInteger0(X1) | X1 = sz00, inference(clausification, [status(esa)], [mZeroDiv])). % 137.93/28.45 cnf(c224, plain, aInteger0(xp), inference(clausification, [status(esa)], [m__2171])). % 137.93/28.45 cnf(c225, plain, xp != sz00, inference(clausification, [status(esa)], [m__2171])). % 137.93/28.45 cnf(c227, plain, ~aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) | X1(X0), inference(clausification, [status(esa)], [m__2171])). % 137.93/28.45 cnf(c241, plain, ~X0(X1) | aInteger0(X1), inference(clausification, [status(esa)], [m__2171])). % 137.93/28.45 cnf(c250, plain, aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp)), inference(clausification, [status(esa)], [m__2232])). % 137.93/28.45 cnf(c251, plain, aInteger0(sK161), inference(clausification, [status(esa)], [m__2232])). % 137.93/28.45 cnf(c252, plain, sdtasdt0(xp,sK161) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)), inference(clausification, [status(esa)], [m__2232])). % 137.93/28.45 cnf(c258, plain, sdtpldt0(sz10,xp) = smndt0(sz10), inference(clausification, [status(esa)], [negated_conjecture])). % 137.93/28.45 cnf(c259, plain, sdtpldt0(sz10,smndt0(xp)) = smndt0(sz10), inference(clausification, [status(esa)], [negated_conjecture])). % 137.93/28.45 cnf(d0, plain, sdtasdt0(sz10,sdtpldt0(X0,X1)) = sdtpldt0(X0,sdtasdt0(sz10,X1)) | ~aInteger0(X1) | ~aInteger0(sz10) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [c14,c15])). % 137.93/28.45 cnf(d1, plain, sdtasdt0(sz10,sdtpldt0(X0,X1)) = sdtpldt0(X0,sdtasdt0(sz10,X1)) | ~aInteger0(X1) | ~aInteger0(X0), inference(resolution, [status(thm)], [c1,d0])). % 137.93/28.45 cnf(d2, plain, sdtpldt0(sz10,sdtpldt0(xp,X0)) = sdtpldt0(smndt0(sz10),X0) | ~aInteger0(X0) | ~aInteger0(xp) | ~aInteger0(sz10), inference(superposition, [status(thm)], [c258,c5])). % 137.93/28.45 cnf(d3, plain, sdtpldt0(sz10,sdtpldt0(xp,X0)) = sdtpldt0(smndt0(sz10),X0) | ~aInteger0(X0) | ~aInteger0(xp), inference(resolution, [status(thm)], [c1,d2])). % 137.93/28.45 cnf(d4, plain, sdtpldt0(sz10,sdtpldt0(xp,X0)) = sdtpldt0(smndt0(sz10),X0) | ~aInteger0(X0), inference(resolution, [status(thm)], [c224,d3])). % 137.93/28.45 cnf(d5, plain, sdtpldt0(sz10,sdtpldt0(X0,xp)) = sdtpldt0(smndt0(sz10),X0) | ~aInteger0(X0) | ~aInteger0(xp) | ~aInteger0(X0), inference(superposition, [status(thm)], [c6,d4])). % 137.93/28.45 cnf(d6, plain, sdtpldt0(sz10,sdtpldt0(X0,xp)) = sdtpldt0(smndt0(sz10),X0) | ~aInteger0(X0), inference(resolution, [status(thm)], [c224,d5])). % 137.93/28.45 cnf(d7, plain, sdtpldt0(sz10,smndt0(sz10)) = sdtpldt0(smndt0(sz10),sz10) | ~aInteger0(sz10), inference(superposition, [status(thm)], [c258,d6])). % 137.93/28.45 cnf(d8, plain, sdtpldt0(sz10,smndt0(sz10)) = sdtpldt0(smndt0(sz10),sz10), inference(resolution, [status(thm)], [c1,d7])). % 137.93/28.45 cnf(d9, plain, sz00 = sdtpldt0(sz10,smndt0(sz10)) | ~aInteger0(sz10), inference(superposition, [status(thm)], [d8,c10])). % 137.93/28.45 cnf(d10, plain, sz00 = sdtpldt0(sz10,smndt0(sz10)), inference(resolution, [status(thm)], [c1,d9])). % 137.93/28.45 cnf(d11, plain, sdtpldt0(sz10,sdtpldt0(smndt0(sz10),X0)) = sdtpldt0(sz00,X0) | ~aInteger0(X0) | ~aInteger0(smndt0(sz10)) | ~aInteger0(sz10), inference(superposition, [status(thm)], [d10,c5])). % 137.93/28.45 cnf(d12, plain, sdtpldt0(sz10,sdtpldt0(smndt0(sz10),X0)) = sdtpldt0(sz00,X0) | ~aInteger0(X0) | ~aInteger0(smndt0(sz10)), inference(resolution, [status(thm)], [c1,d11])). % 137.93/28.45 cnf(d13, plain, aElementOf0(smndt0(sz10),szAzrzSzezqlpdtcmdtrp0(sz10,xp)), inference(demodulation, [status(thm)], [c250,c258])). % 137.93/28.45 cnf(d14, plain, 'Ts151'(smndt0(sz10)), inference(resolution, [status(thm)], [d13,c227])). % 137.93/28.45 cnf(d15, plain, aInteger0(smndt0(sz10)), inference(resolution, [status(thm)], [d14,c241])). % 137.93/28.45 cnf(d16, plain, sdtpldt0(sz10,sdtpldt0(smndt0(sz10),X0)) = sdtpldt0(sz00,X0) | ~aInteger0(X0), inference(resolution, [status(thm)], [d15,d12])). % 137.93/28.45 cnf(d17, plain, sdtpldt0(sz10,sz00) = sdtpldt0(sz00,sz10) | ~aInteger0(sz10) | ~aInteger0(sz10), inference(superposition, [status(thm)], [c10,d16])). % 137.93/28.45 cnf(d18, plain, sdtpldt0(sz10,sz00) = sdtpldt0(sz00,sz10), inference(resolution, [status(thm)], [c1,d17])). % 137.93/28.45 cnf(d19, plain, sdtpldt0(sz00,sz10) = sz10 | ~aInteger0(sz10), inference(superposition, [status(thm)], [d18,c7])). % 137.93/28.45 cnf(d20, plain, sdtpldt0(sz00,sz10) = sz10, inference(resolution, [status(thm)], [c1,d19])). % 137.93/28.45 cnf(d21, plain, sdtpldt0(sz00,sdtpldt0(sz10,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(sz10) | ~aInteger0(sz00), inference(superposition, [status(thm)], [d20,c5])). % 137.93/28.45 cnf(d22, plain, sdtpldt0(sz00,sdtpldt0(sz10,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(sz10), inference(resolution, [status(thm)], [c0,d21])). % 137.93/28.45 cnf(d23, plain, sdtpldt0(sz00,sdtpldt0(sz10,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0), inference(resolution, [status(thm)], [c1,d22])). % 137.93/28.45 cnf(d24, plain, sdtpldt0(sz00,sz00) = sdtpldt0(sz10,smndt0(sz10)) | ~aInteger0(smndt0(sz10)), inference(superposition, [status(thm)], [d10,d23])). % 137.93/28.45 cnf(d25, plain, sdtpldt0(sz00,sz00) = sz00 | ~aInteger0(smndt0(sz10)), inference(demodulation, [status(thm)], [d24,d10])). % 137.93/28.45 cnf(d26, plain, sdtpldt0(sz00,sz00) = sz00, inference(resolution, [status(thm)], [d15,d25])). % 137.93/28.45 cnf(d27, plain, sdtasdt0(sz10,sz00) = sdtpldt0(sz00,sdtasdt0(sz10,sz00)) | ~aInteger0(sz00) | ~aInteger0(sz00), inference(superposition, [status(thm)], [d26,d1])). % 137.93/28.45 cnf(d28, plain, sdtasdt0(sz10,sz00) = sdtpldt0(sz00,sdtasdt0(sz10,sz00)), inference(resolution, [status(thm)], [c0,d27])). % 137.93/28.45 cnf(d29, plain, sdtasdt0(sz10,sdtasdt0(X0,X1)) = sdtasdt0(X0,X1) | ~aInteger0(sz10) | ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(X0), inference(superposition, [status(thm)], [c14,c11])). % 137.93/28.45 cnf(d30, plain, sdtasdt0(sz10,sdtasdt0(X0,X1)) = sdtasdt0(X0,X1) | ~aInteger0(X1) | ~aInteger0(X0), inference(resolution, [status(thm)], [c1,d29])). % 137.93/28.45 cnf(d31, plain, sdtasdt0(X0,sdtpldt0(sz10,X1)) = sdtpldt0(X0,sdtasdt0(X0,X1)) | ~aInteger0(X1) | ~aInteger0(X0) | ~aInteger0(sz10) | ~aInteger0(X0), inference(superposition, [status(thm)], [c13,c15])). % 137.93/28.45 cnf(d32, plain, sdtasdt0(X0,sdtpldt0(sz10,X1)) = sdtpldt0(X0,sdtasdt0(X0,X1)) | ~aInteger0(X1) | ~aInteger0(X0), inference(resolution, [status(thm)], [c1,d31])). % 137.93/28.45 cnf(d33, plain, sdtpldt0(sz10,sz00) = sz10, inference(demodulation, [status(thm)], [d18,d20])). % 137.93/28.45 cnf(d34, plain, sdtasdt0(X0,sz10) = sdtpldt0(X0,sdtasdt0(X0,sz00)) | ~aInteger0(sz00) | ~aInteger0(X0), inference(superposition, [status(thm)], [d33,d32])). % 137.93/28.45 cnf(d35, plain, sdtasdt0(X0,sz10) = sdtpldt0(X0,sdtasdt0(X0,sz00)) | ~aInteger0(X0), inference(resolution, [status(thm)], [c0,d34])). % 137.93/28.45 cnf(d36, plain, sdtasdt0(X0,sz10) = sdtpldt0(X0,sz00) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [c17,d35])). % 137.93/28.45 cnf(d37, plain, sdtasdt0(sz10,sdtpldt0(X0,sz00)) = sdtasdt0(X0,sz10) | ~aInteger0(sz10) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [d36,d30])). % 137.93/28.45 cnf(d38, plain, sdtasdt0(sz10,sdtpldt0(X0,sz00)) = sdtasdt0(X0,sz10) | ~aInteger0(X0), inference(resolution, [status(thm)], [c1,d37])). % 137.93/28.45 cnf(d39, plain, X0 = sdtpldt0(X0,sz00) | ~aInteger0(sz00) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [c8,c6])). % 137.93/28.45 cnf(d40, plain, X0 = sdtpldt0(X0,sz00) | ~aInteger0(X0), inference(resolution, [status(thm)], [c0,d39])). % 137.93/28.45 cnf(d41, plain, sdtasdt0(sz10,X0) = sdtasdt0(X0,sz10) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [d40,d38])). % 137.93/28.45 cnf(d42, plain, sdtasdt0(sz10,sz00) = sdtpldt0(sz00,sdtasdt0(sz00,sz10)) | ~aInteger0(sz00), inference(superposition, [status(thm)], [d41,d28])). % 137.93/28.45 cnf(d43, plain, sdtasdt0(sz10,sz00) = sdtpldt0(sz00,sdtasdt0(sz00,sz10)), inference(resolution, [status(thm)], [c0,d42])). % 137.93/28.45 cnf(d44, plain, sdtasdt0(X0,sdtpldt0(sz10,sz00)) = sdtasdt0(X0,sz10) | ~aInteger0(sz00) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [d35,d32])). % 137.93/28.45 cnf(d45, plain, sdtasdt0(X0,sz10) = sdtasdt0(X0,sz10) | ~aInteger0(X0) | ~aInteger0(sz00), inference(demodulation, [status(thm)], [d44,d33])). % 137.93/28.45 cnf(d46, plain, sdtasdt0(X0,sz10) = sdtasdt0(X0,sz10) | ~aInteger0(X0), inference(resolution, [status(thm)], [c0,d45])). % 137.93/28.45 cnf(d47, plain, sdtasdt0(X0,sz10) = sdtasdt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [d41,d46])). % 137.93/28.45 cnf(d48, plain, sdtasdt0(sz10,sz00) = sdtpldt0(sz00,sdtasdt0(sz00,sz10)) | ~aInteger0(sz00), inference(superposition, [status(thm)], [d47,d28])). % 137.93/28.45 cnf(d49, plain, sdtasdt0(sz10,sz00) = sdtasdt0(sz10,sz00) | ~aInteger0(sz00), inference(demodulation, [status(thm)], [d48,d43])). % 137.93/28.45 cnf(d50, plain, sdtasdt0(sz10,sz00) = sdtasdt0(sz10,sz00), inference(resolution, [status(thm)], [c0,d49])). % 137.93/28.45 cnf(d51, plain, sz00 = sdtasdt0(sz10,sz00) | ~aInteger0(sz10), inference(superposition, [status(thm)], [c17,d50])). % 137.93/28.45 cnf(d52, plain, sz00 = sdtasdt0(sz10,sz00), inference(resolution, [status(thm)], [c1,d51])). % 137.93/28.45 cnf(d53, plain, sz00 = sdtpldt0(sz00,sdtasdt0(sz00,sz10)), inference(demodulation, [status(thm)], [d43,d52])). % 137.93/28.45 cnf(d54, plain, sdtasdt0(sz00,sz10) = sz00 | ~aInteger0(sdtasdt0(sz00,sz10)), inference(superposition, [status(thm)], [d53,c8])). % 137.93/28.45 cnf(d55, plain, aInteger0(sdtasdt0(X0,sz10)) | ~aInteger0(X0) | ~aInteger0(sdtasdt0(X0,sz00)) | ~aInteger0(X0), inference(superposition, [status(thm)], [d35,c3])). % 137.93/28.45 cnf(d56, plain, ~aInteger0(sz00) | ~aInteger0(sz00) | aInteger0(sdtasdt0(sz00,sz10)) | ~aInteger0(sz00), inference(superposition, [status(thm)], [c18,d55])). % 137.93/28.45 cnf(d57, plain, aInteger0(sdtasdt0(sz00,sz10)), inference(resolution, [status(thm)], [c0,d56])). % 137.93/28.45 cnf(d58, plain, sdtasdt0(sz00,sz10) = sz00, inference(resolution, [status(thm)], [d57,d54])). % 137.93/28.45 cnf(d59, plain, sdtasdt0(X0,sdtpldt0(X1,X1)) = sdtasdt0(sdtpldt0(X0,X0),X1) | ~aInteger0(X1) | ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(X1) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [c16,c15])). % 137.93/28.45 cnf(d60, plain, sdtpldt0(sz10,sz00) = sdtpldt0(smndt0(sz10),smndt0(xp)) | ~aInteger0(smndt0(xp)) | ~aInteger0(xp), inference(superposition, [status(thm)], [c9,d4])). % 137.93/28.45 cnf(d61, plain, sdtpldt0(sz10,sz00) = sdtpldt0(smndt0(sz10),smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d60])). % 137.93/28.45 cnf(d62, plain, sdtpldt0(sz00,sz10) = sdtpldt0(smndt0(sz10),smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(demodulation, [status(thm)], [d61,d18])). % 137.93/28.45 cnf(d63, plain, sz10 = sdtpldt0(smndt0(sz10),smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(demodulation, [status(thm)], [d62,d20])). % 137.93/28.45 cnf(d64, plain, sdtpldt0(sz10,sz10) = sdtpldt0(sz00,smndt0(xp)) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d63,d16])). % 137.93/28.45 cnf(d65, plain, sdtpldt0(sz10,sz10) = smndt0(xp) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [c8,d64])). % 137.93/28.45 cnf(d66, plain, sdtpldt0(sz10,sdtpldt0(smndt0(xp),X0)) = sdtpldt0(smndt0(sz10),X0) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)) | ~aInteger0(sz10), inference(superposition, [status(thm)], [c259,c5])). % 137.93/28.45 cnf(d67, plain, sdtpldt0(sz10,sdtpldt0(smndt0(xp),X0)) = sdtpldt0(smndt0(sz10),X0) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c1,d66])). % 137.93/28.45 cnf(d68, plain, sdtpldt0(sz10,sdtpldt0(X0,smndt0(xp))) = sdtpldt0(smndt0(sz10),X0) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)) | ~aInteger0(X0), inference(superposition, [status(thm)], [c6,d67])). % 137.93/28.45 cnf(d69, plain, sdtpldt0(sz10,sz00) = sdtpldt0(smndt0(sz10),xp) | ~aInteger0(xp) | ~aInteger0(smndt0(xp)) | ~aInteger0(xp), inference(superposition, [status(thm)], [c9,d68])). % 137.93/28.45 cnf(d70, plain, sdtpldt0(sz10,sz00) = sdtpldt0(smndt0(sz10),xp) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d69])). % 137.93/28.45 cnf(d71, plain, sdtpldt0(sz00,sz10) = sdtpldt0(smndt0(sz10),xp) | ~aInteger0(smndt0(xp)), inference(demodulation, [status(thm)], [d70,d18])). % 137.93/28.45 cnf(d72, plain, sz10 = sdtpldt0(smndt0(sz10),xp) | ~aInteger0(smndt0(xp)), inference(demodulation, [status(thm)], [d71,d20])). % 137.93/28.45 cnf(d73, plain, sdtpldt0(sz10,sz10) = sdtpldt0(sz00,xp) | ~aInteger0(xp) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d72,d16])). % 137.93/28.45 cnf(d74, plain, sdtpldt0(sz10,sz10) = sdtpldt0(sz00,xp) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d73])). % 137.93/28.45 cnf(d75, plain, sdtpldt0(sz00,xp) = smndt0(xp) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d74,d65])). % 137.93/28.45 cnf(d76, plain, xp = smndt0(xp) | ~aInteger0(xp) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d75,c8])). % 137.93/28.45 cnf(d77, plain, xp = smndt0(xp) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d76])). % 137.93/28.45 cnf(d78, plain, sz00 = sdtpldt0(xp,xp) | ~aInteger0(xp) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d77,c10])). % 137.93/28.45 cnf(d79, plain, sz00 = sdtpldt0(xp,xp) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d78])). % 137.93/28.45 cnf(d80, plain, sdtasdt0(smndt0(sz10),sdtasdt0(X0,X1)) = sdtasdt0(smndt0(X0),X1) | ~aInteger0(smndt0(sz10)) | ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(X0), inference(superposition, [status(thm)], [c19,c11])). % 137.93/28.45 cnf(d81, plain, sdtasdt0(smndt0(sz10),sdtasdt0(X0,X1)) = sdtasdt0(smndt0(X0),X1) | ~aInteger0(X1) | ~aInteger0(X0), inference(resolution, [status(thm)], [d15,d80])). % 137.93/28.45 cnf(d82, plain, sdtpldt0(sz00,xp) = sdtpldt0(smndt0(sz10),smndt0(sz10)) | ~aInteger0(smndt0(sz10)) | ~aInteger0(xp), inference(superposition, [status(thm)], [d16,d6])). % 137.93/28.45 cnf(d83, plain, sdtpldt0(sz00,xp) = sdtpldt0(smndt0(sz10),smndt0(sz10)) | ~aInteger0(smndt0(sz10)), inference(resolution, [status(thm)], [c224,d82])). % 137.93/28.45 cnf(d84, plain, sdtpldt0(sz00,xp) = sdtpldt0(smndt0(sz10),smndt0(sz10)), inference(resolution, [status(thm)], [d15,d83])). % 137.93/28.45 cnf(d85, plain, sdtpldt0(smndt0(sz10),smndt0(sz10)) = sdtpldt0(sz00,xp) | ~aInteger0(smndt0(sz10)) | ~aInteger0(smndt0(sz10)), inference(superposition, [status(thm)], [d84,c6])). % 137.93/28.45 cnf(d86, plain, sdtpldt0(sz00,xp) = sdtpldt0(sz00,xp) | ~aInteger0(smndt0(sz10)), inference(demodulation, [status(thm)], [d85,d84])). % 137.93/28.45 cnf(d87, plain, sdtpldt0(sz00,xp) = sdtpldt0(sz00,xp), inference(resolution, [status(thm)], [d15,d86])). % 137.93/28.45 cnf(d88, plain, sdtpldt0(sz00,xp) = xp | ~aInteger0(xp), inference(superposition, [status(thm)], [c8,d87])). % 137.93/28.45 cnf(d89, plain, sdtpldt0(sz00,xp) = xp, inference(resolution, [status(thm)], [c224,d88])). % 137.93/28.45 cnf(d90, plain, xp = sdtpldt0(smndt0(sz10),smndt0(sz10)), inference(demodulation, [status(thm)], [d84,d89])). % 137.93/28.45 cnf(d91, plain, sdtasdt0(xp,sK161) = sdtpldt0(smndt0(sz10),smndt0(sz10)), inference(demodulation, [status(thm)], [c252,c259])). % 137.93/28.45 cnf(d92, plain, sdtasdt0(xp,sK161) = xp, inference(demodulation, [status(thm)], [d91,d90])). % 137.93/28.45 cnf(d93, plain, sdtasdt0(smndt0(sz10),xp) = sdtasdt0(smndt0(xp),sK161) | ~aInteger0(sK161) | ~aInteger0(xp), inference(superposition, [status(thm)], [d92,d81])). % 137.93/28.45 cnf(d94, plain, sdtasdt0(smndt0(sz10),xp) = sdtasdt0(smndt0(xp),sK161) | ~aInteger0(sK161), inference(resolution, [status(thm)], [c224,d93])). % 137.93/28.45 cnf(d95, plain, sdtasdt0(smndt0(sz10),xp) = sdtasdt0(smndt0(xp),sK161), inference(resolution, [status(thm)], [c251,d94])). % 137.93/28.45 cnf(d96, plain, sdtasdt0(X0,sdtasdt0(smndt0(sz10),X1)) = sdtasdt0(smndt0(X0),X1) | ~aInteger0(X0) | ~aInteger0(smndt0(sz10)) | ~aInteger0(X1) | ~aInteger0(X0), inference(superposition, [status(thm)], [c20,c11])). % 137.93/28.45 cnf(d97, plain, sdtasdt0(X0,sdtasdt0(smndt0(sz10),X1)) = sdtasdt0(smndt0(X0),X1) | ~aInteger0(X1) | ~aInteger0(X0), inference(resolution, [status(thm)], [d15,d96])). % 137.93/28.45 cnf(d98, plain, smndt0(X0) = sdtasdt0(smndt0(sz10),X0) | ~aInteger0(smndt0(sz10)) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [c20,c12])). % 137.93/28.45 cnf(d99, plain, smndt0(X0) = sdtasdt0(smndt0(sz10),X0) | ~aInteger0(X0), inference(resolution, [status(thm)], [d15,d98])). % 137.93/28.45 cnf(d100, plain, sdtasdt0(X1,smndt0(X0)) = sdtasdt0(smndt0(X1),X0) | ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(X0), inference(superposition, [status(thm)], [d99,d97])). % 137.93/28.45 cnf(d101, plain, sdtasdt0(smndt0(sz10),xp) = sdtasdt0(xp,smndt0(sK161)) | ~aInteger0(xp) | ~aInteger0(sK161), inference(superposition, [status(thm)], [d100,d95])). % 137.93/28.45 cnf(d102, plain, sdtasdt0(smndt0(sz10),xp) = sdtasdt0(xp,smndt0(sK161)) | ~aInteger0(sK161), inference(resolution, [status(thm)], [c224,d101])). % 137.93/28.45 cnf(d103, plain, sdtasdt0(smndt0(sz10),xp) = sdtasdt0(xp,smndt0(sK161)), inference(resolution, [status(thm)], [c251,d102])). % 137.93/28.45 cnf(d104, plain, sdtasdt0(xp,smndt0(sK161)) = smndt0(xp) | ~aInteger0(xp), inference(superposition, [status(thm)], [d103,c19])). % 137.93/28.45 cnf(d105, plain, sdtasdt0(xp,smndt0(sK161)) = smndt0(xp), inference(resolution, [status(thm)], [c224,d104])). % 137.93/28.45 cnf(d106, plain, X0 = sdtasdt0(X0,sz10) | ~aInteger0(X0) | ~aInteger0(sz10) | ~aInteger0(X0), inference(superposition, [status(thm)], [c14,c12])). % 137.93/28.45 cnf(d107, plain, X0 = sdtasdt0(X0,sz10) | ~aInteger0(X0), inference(resolution, [status(thm)], [c1,d106])). % 137.93/28.45 cnf(d108, plain, sdtasdt0(smndt0(sz10),X0) = sdtasdt0(smndt0(X0),sz10) | ~aInteger0(sz10) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [d107,d81])). % 137.93/28.45 cnf(d109, plain, sdtasdt0(smndt0(sz10),X0) = sdtasdt0(smndt0(X0),sz10) | ~aInteger0(X0), inference(resolution, [status(thm)], [c1,d108])). % 137.93/28.45 cnf(d110, plain, aInteger0(sdtasdt0(smndt0(X0),sz10)) | ~aInteger0(X0) | ~aInteger0(smndt0(sz10)) | ~aInteger0(X0), inference(superposition, [status(thm)], [d109,c4])). % 137.93/28.45 cnf(d111, plain, ~aInteger0(X0) | aInteger0(sdtasdt0(smndt0(X0),sz10)), inference(resolution, [status(thm)], [d15,d110])). % 137.93/28.45 cnf(d112, plain, aInteger0(sdtasdt0(smndt0(sz10),X0)) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [d109,d111])). % 137.93/28.45 cnf(d113, plain, aInteger0(sdtasdt0(xp,smndt0(sK161))) | ~aInteger0(xp), inference(superposition, [status(thm)], [d103,d112])). % 137.93/28.45 cnf(d114, plain, aInteger0(sdtasdt0(xp,smndt0(sK161))), inference(resolution, [status(thm)], [c224,d113])). % 137.93/28.45 cnf(d115, plain, aInteger0(smndt0(xp)), inference(demodulation, [status(thm)], [d114,d105])). % 137.93/28.45 cnf(d116, plain, sz00 = sdtpldt0(xp,xp), inference(resolution, [status(thm)], [d115,d79])). % 137.93/28.45 cnf(d117, plain, sdtasdt0(xp,sdtpldt0(X0,X0)) = sdtasdt0(sz00,X0) | ~aInteger0(X0) | ~aInteger0(xp), inference(superposition, [status(thm)], [d116,d59])). % 137.93/28.45 cnf(d118, plain, sdtasdt0(xp,sdtpldt0(X0,X0)) = sdtasdt0(sz00,X0) | ~aInteger0(X0), inference(resolution, [status(thm)], [c224,d117])). % 137.93/28.45 cnf(d119, plain, sdtpldt0(sz00,xp) = sdtpldt0(sz10,sz10) | ~aInteger0(sz10) | ~aInteger0(sz10) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d74,c6])). % 137.93/28.45 cnf(d120, plain, sdtpldt0(sz00,xp) = sdtpldt0(sz10,sz10) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c1,d119])). % 137.93/28.45 cnf(d121, plain, xp = sdtpldt0(sz10,sz10) | ~aInteger0(smndt0(xp)), inference(demodulation, [status(thm)], [d120,d89])). % 137.93/28.45 cnf(d122, plain, xp = sdtpldt0(sz10,sz10), inference(resolution, [status(thm)], [d115,d121])). % 137.93/28.45 cnf(d123, plain, sdtasdt0(xp,xp) = sdtasdt0(sz00,sz10) | ~aInteger0(sz10), inference(superposition, [status(thm)], [d122,d118])). % 137.93/28.45 cnf(d124, plain, sdtasdt0(xp,xp) = sz00 | ~aInteger0(sz10), inference(demodulation, [status(thm)], [d123,d58])). % 137.93/28.45 cnf(d125, plain, sdtasdt0(xp,xp) = sz00, inference(resolution, [status(thm)], [c1,d124])). % 137.93/28.45 cnf(d126, plain, sz00 != sz00 | xp = sz00 | xp = sz00 | ~aInteger0(xp) | ~aInteger0(xp), inference(superposition, [status(thm)], [d125,c21])). % 137.93/28.45 cnf(d127, plain, sz00 != sz00 | xp = sz00, inference(resolution, [status(thm)], [c224,d126])). % 137.93/28.45 cnf(d128, plain, sz00 != sz00, inference(resolution, [status(thm)], [c225,d127])). % 137.93/28.45 cnf(d129, plain, sz00 = sdtpldt0(smndt0(sz10),sz10), inference(demodulation, [status(thm)], [d8,d10])). % 137.93/28.45 cnf(d130, plain, sdtpldt0(sz10,smndt0(sz10)) = sz00 | ~aInteger0(sz10) | ~aInteger0(smndt0(sz10)), inference(superposition, [status(thm)], [d129,c6])). % 137.93/28.45 cnf(d131, plain, sz00 = sz00 | ~aInteger0(sz10) | ~aInteger0(smndt0(sz10)), inference(demodulation, [status(thm)], [d130,d10])). % 137.93/28.45 cnf(d132, plain, sz00 = sz00 | ~aInteger0(smndt0(sz10)), inference(resolution, [status(thm)], [c1,d131])). % 137.93/28.45 cnf(d133, plain, sz00 = sz00, inference(resolution, [status(thm)], [d15,d132])). % 137.93/28.45 cnf(d134, plain, $false, inference(resolution, [status(thm)], [d133,d128])). % 137.93/28.45 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------