%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM453+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 : n012.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 34.41s 11.54s % Output : CNFRefutation 34.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : NUM453+6 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.03/0.30 % Computer : n012.cluster.edu % 0.03/0.30 % Model : x86_64 x86_64 % 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.03/0.30 % Memory : 8046.5625MB % 0.03/0.30 % OS : Linux 6.8.0-71-generic % 0.03/0.30 % CPULimit : 300 % 0.03/0.30 % WCLimit : 300 % 0.03/0.30 % DateTime : Sat Sep 26 02:48:52 UTC 2026 % 0.03/0.30 % CPUTime : % 0.03/0.30 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 34.41/11.54 % SZS status Theorem for theBenchmark.p % 34.41/11.54 % SZS output start CNFRefutation for theBenchmark.p % 34.41/11.54 fof(mIntZero, axiom, aInteger0(sz00)). % 34.41/11.54 fof(mIntOne, axiom, aInteger0(sz10)). % 34.41/11.54 fof(mIntNeg, axiom, ! [X0] : ((aInteger0(X0) => aInteger0(smndt0(X0))))). % 34.41/11.54 fof(mAddAsso, axiom, ! [X0] : ! [X1] : ! [X2] : (((aInteger0(X0) & (aInteger0(X1) & aInteger0(X2))) => sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2)))). % 34.41/11.54 fof(mAddComm, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => sdtpldt0(X0,X1) = sdtpldt0(X1,X0)))). % 34.41/11.54 fof(mAddZero, axiom, ! [X0] : ((aInteger0(X0) => (sdtpldt0(X0,sz00) = X0 & X0 = sdtpldt0(sz00,X0))))). % 34.41/11.54 fof(mAddNeg, axiom, ! [X0] : ((aInteger0(X0) => (sdtpldt0(X0,smndt0(X0)) = sz00 & sz00 = sdtpldt0(smndt0(X0),X0))))). % 34.41/11.54 fof(mZeroDiv, axiom, ! [X0] : ! [X1] : (((aInteger0(X0) & aInteger0(X1)) => (sdtasdt0(X0,X1) = sz00 => (X0 = sz00 | X1 = sz00))))). % 34.41/11.54 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)))))))))))). % 34.41/11.54 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)))))))))). % 34.41/11.54 fof(m__, conjecture, (sdtpldt0(sz10,xp) != sz10 & sdtpldt0(sz10,smndt0(xp)) != sz10)). % 34.41/11.54 fof(negated_conjecture, negated_conjecture, ~((sdtpldt0(sz10,xp) != sz10 & sdtpldt0(sz10,smndt0(xp)) != sz10)), inference(negate_conjecture, [status(cth)], [m__])). % 34.41/11.54 cnf(c0, plain, aInteger0(sz00), inference(clausification, [status(esa)], [mIntZero])). % 34.41/11.54 cnf(c1, plain, aInteger0(sz10), inference(clausification, [status(esa)], [mIntOne])). % 34.41/11.54 cnf(c2, plain, ~aInteger0(X0) | aInteger0(smndt0(X0)), inference(clausification, [status(esa)], [mIntNeg])). % 34.41/11.54 cnf(c5, plain, ~aInteger0(X0) | ~aInteger0(X1) | ~aInteger0(X2) | sdtpldt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtpldt0(X0,X1),X2), inference(clausification, [status(esa)], [mAddAsso])). % 34.41/11.54 cnf(c6, plain, ~aInteger0(X0) | ~aInteger0(X1) | sdtpldt0(X0,X1) = sdtpldt0(X1,X0), inference(clausification, [status(esa)], [mAddComm])). % 34.41/11.54 cnf(c7, plain, ~aInteger0(X0) | sdtpldt0(X0,sz00) = X0, inference(clausification, [status(esa)], [mAddZero])). % 34.41/11.54 cnf(c8, plain, ~aInteger0(X0) | X0 = sdtpldt0(sz00,X0), inference(clausification, [status(esa)], [mAddZero])). % 34.41/11.54 cnf(c9, plain, ~aInteger0(X0) | sdtpldt0(X0,smndt0(X0)) = sz00, inference(clausification, [status(esa)], [mAddNeg])). % 34.41/11.54 cnf(c10, plain, ~aInteger0(X0) | sz00 = sdtpldt0(smndt0(X0),X0), inference(clausification, [status(esa)], [mAddNeg])). % 34.41/11.54 cnf(c21, plain, X0 = sz00 | sdtasdt0(X0,X1) != sz00 | ~aInteger0(X0) | ~aInteger0(X1) | X1 = sz00, inference(clausification, [status(esa)], [mZeroDiv])). % 34.41/11.54 cnf(c224, plain, aInteger0(xp), inference(clausification, [status(esa)], [m__2171])). % 34.41/11.54 cnf(c225, plain, xp != sz00, inference(clausification, [status(esa)], [m__2171])). % 34.41/11.54 cnf(c227, plain, ~aElementOf0(X0,szAzrzSzezqlpdtcmdtrp0(sz10,xp)) | X1(X0), inference(clausification, [status(esa)], [m__2171])). % 34.41/11.54 cnf(c241, plain, ~X0(X1) | aInteger0(X1), inference(clausification, [status(esa)], [m__2171])). % 34.41/11.54 cnf(c246, plain, aInteger0(sK160), inference(clausification, [status(esa)], [m__2232])). % 34.41/11.54 cnf(c247, plain, sdtasdt0(xp,sK160) = sdtpldt0(sdtpldt0(sz10,xp),smndt0(sz10)), inference(clausification, [status(esa)], [m__2232])). % 34.41/11.54 cnf(c250, plain, aElementOf0(sdtpldt0(sz10,xp),szAzrzSzezqlpdtcmdtrp0(sz10,xp)), inference(clausification, [status(esa)], [m__2232])). % 34.41/11.54 cnf(c251, plain, aInteger0(sK161), inference(clausification, [status(esa)], [m__2232])). % 34.41/11.54 cnf(c252, plain, sdtasdt0(xp,sK161) = sdtpldt0(sdtpldt0(sz10,smndt0(xp)),smndt0(sz10)), inference(clausification, [status(esa)], [m__2232])). % 34.41/11.54 cnf(c256, plain, sdtpldt0(sz10,xp) = sz10 | sdtpldt0(sz10,smndt0(xp)) = sz10, inference(clausification, [status(esa)], [negated_conjecture])). % 34.41/11.54 cnf(d0, plain, sz00 = sdtpldt0(X0,smndt0(X0)) | ~aInteger0(smndt0(X0)) | ~aInteger0(X0) | ~aInteger0(X0), inference(superposition, [status(thm)], [c10,c6])). % 34.41/11.54 cnf(d1, plain, sdtpldt0(sz10,sdtpldt0(smndt0(xp),X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)) | ~aInteger0(sz10) | sdtpldt0(sz10,xp) = sz10, inference(superposition, [status(thm)], [c256,c5])). % 34.41/11.54 cnf(d2, plain, sdtpldt0(sz10,sdtpldt0(smndt0(xp),X0)) = sdtpldt0(sz10,X0) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(X0) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c1,d1])). % 34.41/11.54 cnf(d3, plain, sdtpldt0(sz10,smndt0(xp)) = sdtpldt0(sz10,sz00) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(sz00) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [c7,d2])). % 34.41/11.54 cnf(d4, plain, sdtpldt0(sz10,smndt0(xp)) = sdtpldt0(sz10,sz00) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c0,d3])). % 34.41/11.54 cnf(d5, plain, sz10 = sdtpldt0(sz10,sz00) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(smndt0(xp)) | sdtpldt0(sz10,xp) = sz10, inference(superposition, [status(thm)], [c256,d4])). % 34.41/11.54 cnf(d6, plain, sdtpldt0(sz10,sdtpldt0(xp,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(xp) | ~aInteger0(sz10) | sz10 = sdtpldt0(sz10,sz00) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d5,c5])). % 34.41/11.54 cnf(d7, plain, sz10 = sdtpldt0(sz10,sz00) | sdtpldt0(sz10,sdtpldt0(xp,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)) | ~aInteger0(xp), inference(resolution, [status(thm)], [c1,d6])). % 34.41/11.54 cnf(d8, plain, sz10 = sdtpldt0(sz10,sz00) | sdtpldt0(sz10,sdtpldt0(xp,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d7])). % 34.41/11.54 cnf(d9, plain, sdtpldt0(sz10,xp) = sdtpldt0(sz10,sz00) | sz10 = sdtpldt0(sz10,sz00) | ~aInteger0(sz00) | ~aInteger0(smndt0(xp)) | ~aInteger0(xp), inference(superposition, [status(thm)], [c7,d8])). % 34.41/11.54 cnf(d10, plain, sz10 = sdtpldt0(sz10,sz00) | sdtpldt0(sz10,xp) = sdtpldt0(sz10,sz00) | ~aInteger0(smndt0(xp)) | ~aInteger0(xp), inference(resolution, [status(thm)], [c0,d9])). % 34.41/11.54 cnf(d11, plain, sz10 = sdtpldt0(sz10,sz00) | sdtpldt0(sz10,xp) = sdtpldt0(sz10,sz00) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d10])). % 34.41/11.54 cnf(d12, plain, sz10 = sdtpldt0(sz10,sz00) | sz10 = sdtpldt0(sz10,sz00) | ~aInteger0(smndt0(xp)) | sz10 = sdtpldt0(sz10,sz00) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d5,d11])). % 34.41/11.54 cnf(d13, plain, sdtpldt0(sz00,sz10) = sz10 | ~aInteger0(sz00) | ~aInteger0(sz10) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d12,c6])). % 34.41/11.54 cnf(d14, plain, sdtpldt0(sz00,sz10) = sz10 | ~aInteger0(sz10) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c0,d13])). % 34.41/11.54 cnf(d15, plain, sdtpldt0(sz00,sz10) = sz10 | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c1,d14])). % 34.41/11.54 cnf(d16, plain, sdtpldt0(sz00,sdtpldt0(sz10,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(sz10) | ~aInteger0(sz00) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d15,c5])). % 34.41/11.54 cnf(d17, plain, sdtpldt0(sz00,sdtpldt0(sz10,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(sz10) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c0,d16])). % 34.41/11.54 cnf(d18, plain, sdtpldt0(sz00,sdtpldt0(sz10,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c1,d17])). % 34.41/11.54 cnf(d19, plain, sdtpldt0(sz00,sdtpldt0(sz10,sz00)) = sdtpldt0(sz10,smndt0(xp)) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d4,d18])). % 34.41/11.54 cnf(d20, plain, sdtpldt0(sz10,sdtpldt0(X0,smndt0(xp))) = sdtpldt0(sz10,X0) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(X0) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)) | ~aInteger0(X0), inference(superposition, [status(thm)], [c6,d2])). % 34.41/11.54 cnf(d21, plain, sdtpldt0(sz10,sz00) = sdtpldt0(sz10,xp) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(xp) | ~aInteger0(smndt0(xp)) | ~aInteger0(xp), inference(superposition, [status(thm)], [c9,d20])). % 34.41/11.54 cnf(d22, plain, sdtpldt0(sz10,sz00) = sdtpldt0(sz10,xp) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d21])). % 34.41/11.54 cnf(d23, plain, sdtpldt0(sz00,sdtpldt0(sz10,sz00)) = sdtpldt0(sz10,xp) | ~aInteger0(xp) | ~aInteger0(smndt0(xp)) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d22,d18])). % 34.41/11.54 cnf(d24, plain, sdtpldt0(sz00,sdtpldt0(sz10,sz00)) = sdtpldt0(sz10,xp) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d23])). % 34.41/11.54 cnf(d25, plain, sdtpldt0(sz10,xp) = sdtpldt0(sz10,smndt0(xp)) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(smndt0(xp)) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d24,d19])). % 34.41/11.54 cnf(d26, plain, sdtpldt0(sz10,xp) = sz10 | sdtpldt0(sz10,xp) = sz10 | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d25,c256])). % 34.41/11.54 cnf(d27, plain, sdtasdt0(xp,sK160) = sdtpldt0(sz10,smndt0(sz10)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d26,c247])). % 34.41/11.54 cnf(d28, plain, sdtasdt0(xp,sK160) = sz00 | ~aInteger0(sz10) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d27,c9])). % 34.41/11.54 cnf(d29, plain, sdtasdt0(xp,sK160) = sz00 | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c1,d28])). % 34.41/11.54 cnf(d30, plain, sz00 != sz00 | sK160 = sz00 | xp = sz00 | ~aInteger0(sK160) | ~aInteger0(xp) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d29,c21])). % 34.41/11.54 cnf(d31, plain, sz00 != sz00 | xp = sz00 | sK160 = sz00 | ~aInteger0(smndt0(xp)) | ~aInteger0(sK160), inference(resolution, [status(thm)], [c224,d30])). % 34.41/11.54 cnf(d32, plain, sz00 != sz00 | xp = sz00 | sK160 = sz00 | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c246,d31])). % 34.41/11.54 cnf(d33, plain, sz00 != sz00 | sK160 = sz00 | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c225,d32])). % 34.41/11.54 cnf(d34, plain, sK160 = sz00 | ~aInteger0(smndt0(xp)), inference(equality_resolution, [status(thm)], [d33])). % 34.41/11.54 cnf(d35, plain, sK160 = sz00 | ~aInteger0(xp), inference(resolution, [status(thm)], [d34,c2])). % 34.41/11.54 cnf(d36, plain, sK160 = sz00, inference(resolution, [status(thm)], [c224,d35])). % 34.41/11.54 cnf(d37, plain, sdtpldt0(sz10,sdtpldt0(xp,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(xp) | ~aInteger0(sz10) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d26,c5])). % 34.41/11.54 cnf(d38, plain, sdtpldt0(sz10,sdtpldt0(xp,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)) | ~aInteger0(xp), inference(resolution, [status(thm)], [c1,d37])). % 34.41/11.54 cnf(d39, plain, sdtpldt0(sz10,sdtpldt0(xp,X0)) = sdtpldt0(sz10,X0) | ~aInteger0(X0) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d38])). % 34.41/11.54 cnf(d40, plain, sdtpldt0(sz10,sz00) = sdtpldt0(sz10,smndt0(xp)) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)) | ~aInteger0(xp), inference(superposition, [status(thm)], [c9,d39])). % 34.41/11.54 cnf(d41, plain, sdtpldt0(sz10,sz00) = sdtpldt0(sz10,smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d40])). % 34.41/11.54 cnf(d42, plain, sdtpldt0(sz00,sdtpldt0(sz10,sz00)) = sdtpldt0(sz10,smndt0(xp)) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d41,d18])). % 34.41/11.54 cnf(d43, plain, sdtpldt0(sz10,smndt0(xp)) = sdtpldt0(sz10,sz00) | ~aInteger0(sz00) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d42,d18])). % 34.41/11.54 cnf(d44, plain, sdtpldt0(sz10,smndt0(xp)) = sdtpldt0(sz10,sz00) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c0,d43])). % 34.41/11.54 cnf(d45, plain, sdtasdt0(xp,sK161) = sdtpldt0(sdtpldt0(sz10,sz00),smndt0(sz10)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d44,c252])). % 34.41/11.54 cnf(d46, plain, sdtpldt0(sz00,sz10) = sdtpldt0(sz10,sz00) | ~aInteger0(sz00) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d12,d18])). % 34.41/11.54 cnf(d47, plain, sdtpldt0(sz00,sz10) = sdtpldt0(sz10,sz00) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c0,d46])). % 34.41/11.54 cnf(d48, plain, sdtpldt0(sz00,sdtpldt0(sz00,sz10)) = sdtpldt0(sz10,sz00) | ~aInteger0(sz00) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d47,d18])). % 34.41/11.54 cnf(d49, plain, sdtpldt0(sz00,sdtpldt0(sz00,sz10)) = sdtpldt0(sz10,sz00) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c0,d48])). % 34.41/11.54 cnf(d50, plain, sdtpldt0(sz00,sz10) = sdtpldt0(sz10,xp) | ~aInteger0(xp) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d26,d18])). % 34.41/11.54 cnf(d51, plain, sdtpldt0(sz00,sz10) = sdtpldt0(sz10,xp) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d50])). % 34.41/11.54 cnf(d52, plain, sdtpldt0(sz00,sdtpldt0(sz00,sz10)) = sdtpldt0(sz10,xp) | ~aInteger0(xp) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d51,d18])). % 34.41/11.54 cnf(d53, plain, sdtpldt0(sz00,sdtpldt0(sz00,sz10)) = sdtpldt0(sz10,xp) | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c224,d52])). % 34.41/11.54 cnf(d54, plain, sdtpldt0(sz10,xp) = sdtpldt0(sz10,sz00) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d53,d49])). % 34.41/11.54 cnf(d55, plain, sdtpldt0(sz10,sz00) = sz10 | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d54,d26])). % 34.41/11.54 cnf(d56, plain, sdtasdt0(xp,sK161) = sdtpldt0(sz10,smndt0(sz10)) | ~aInteger0(smndt0(xp)) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d55,d45])). % 34.41/11.54 cnf(d57, plain, sdtasdt0(xp,sK161) = sz00 | ~aInteger0(sz10) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d56,c9])). % 34.41/11.54 cnf(d58, plain, sdtasdt0(xp,sK161) = sz00 | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c1,d57])). % 34.41/11.54 cnf(d59, plain, sz00 != sz00 | sK161 = sz00 | xp = sz00 | ~aInteger0(sK161) | ~aInteger0(xp) | ~aInteger0(smndt0(xp)), inference(superposition, [status(thm)], [d58,c21])). % 34.41/11.54 cnf(d60, plain, sz00 != sz00 | xp = sz00 | sK161 = sz00 | ~aInteger0(smndt0(xp)) | ~aInteger0(sK161), inference(resolution, [status(thm)], [c224,d59])). % 34.41/11.54 cnf(d61, plain, sz00 != sz00 | xp = sz00 | sK161 = sz00 | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c251,d60])). % 34.41/11.54 cnf(d62, plain, sz00 != sz00 | sK161 = sz00 | ~aInteger0(smndt0(xp)), inference(resolution, [status(thm)], [c225,d61])). % 34.41/11.54 cnf(d63, plain, sK161 = sz00 | ~aInteger0(smndt0(xp)), inference(equality_resolution, [status(thm)], [d62])). % 34.41/11.54 cnf(d64, plain, sK161 = sz00 | ~aInteger0(xp), inference(resolution, [status(thm)], [d63,c2])). % 34.41/11.54 cnf(d65, plain, sK161 = sz00, inference(resolution, [status(thm)], [c224,d64])). % 34.41/11.54 cnf(d66, plain, sdtasdt0(xp,sK161) = sdtpldt0(sz10,smndt0(sz10)) | sdtpldt0(sz10,xp) = sz10, inference(superposition, [status(thm)], [c256,c252])). % 34.41/11.54 cnf(d67, plain, sz00 = sdtasdt0(xp,sK161) | ~aInteger0(sz10) | ~aInteger0(smndt0(sz10)) | sdtpldt0(sz10,xp) = sz10, inference(superposition, [status(thm)], [d66,d0])). % 34.41/11.54 cnf(d68, plain, sz00 = sdtasdt0(xp,sK161) | sdtpldt0(sz10,xp) = sz10 | ~aInteger0(smndt0(sz10)), inference(resolution, [status(thm)], [c1,d67])). % 34.41/11.54 cnf(d69, plain, sdtasdt0(xp,sK160) = sdtpldt0(sz10,smndt0(sz10)) | sz00 = sdtasdt0(xp,sK161) | ~aInteger0(smndt0(sz10)), inference(superposition, [status(thm)], [d68,c247])). % 34.41/11.54 cnf(d70, plain, sz00 = sdtasdt0(xp,sz00) | sdtasdt0(xp,sK160) = sdtpldt0(sz10,smndt0(sz10)) | ~aInteger0(smndt0(sz10)), inference(demodulation, [status(thm)], [d69,d65])). % 34.41/11.54 cnf(d71, plain, sz00 = sdtasdt0(xp,sz00) | sdtasdt0(xp,sz00) = sdtpldt0(sz10,smndt0(sz10)) | ~aInteger0(smndt0(sz10)), inference(demodulation, [status(thm)], [d70,d36])). % 34.41/11.54 cnf(d72, plain, sz00 = sdtasdt0(xp,sz00) | ~aInteger0(sz10) | ~aInteger0(smndt0(sz10)) | sz00 = sdtasdt0(xp,sz00) | ~aInteger0(smndt0(sz10)), inference(superposition, [status(thm)], [d71,d0])). % 34.41/11.54 cnf(d73, plain, sz00 = sdtasdt0(xp,sz00) | ~aInteger0(smndt0(sz10)), inference(resolution, [status(thm)], [c1,d72])). % 34.41/11.54 cnf(d74, plain, sdtpldt0(smndt0(X0),sdtpldt0(X0,X1)) = sdtpldt0(sz00,X1) | ~aInteger0(X1) | ~aInteger0(X0) | ~aInteger0(smndt0(X0)) | ~aInteger0(X0), inference(superposition, [status(thm)], [c10,c5])). % 34.41/11.54 cnf(d75, plain, sdtasdt0(xp,sK160) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,xp)) | ~aInteger0(sdtpldt0(sz10,xp)) | ~aInteger0(smndt0(sz10)), inference(superposition, [status(thm)], [c247,c6])). % 34.41/11.54 cnf(d76, plain, sdtasdt0(xp,sz00) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,xp)) | ~aInteger0(smndt0(sz10)) | ~aInteger0(sdtpldt0(sz10,xp)), inference(demodulation, [status(thm)], [d75,d36])). % 34.41/11.54 cnf(d77, plain, 'Ts151'(sdtpldt0(sz10,xp)), inference(resolution, [status(thm)], [c250,c227])). % 34.41/11.54 cnf(d78, plain, aInteger0(sdtpldt0(sz10,xp)), inference(resolution, [status(thm)], [d77,c241])). % 34.41/11.54 cnf(d79, plain, sdtasdt0(xp,sz00) = sdtpldt0(smndt0(sz10),sdtpldt0(sz10,xp)) | ~aInteger0(smndt0(sz10)), inference(resolution, [status(thm)], [d78,d76])). % 34.41/11.54 cnf(d80, plain, sdtasdt0(xp,sz00) = sdtpldt0(sz00,xp) | ~aInteger0(xp) | ~aInteger0(sz10) | ~aInteger0(smndt0(sz10)) | ~aInteger0(smndt0(sz10)), inference(superposition, [status(thm)], [d79,d74])). % 34.41/11.54 cnf(d81, plain, sdtasdt0(xp,sz00) = sdtpldt0(sz00,xp) | ~aInteger0(smndt0(sz10)) | ~aInteger0(xp), inference(resolution, [status(thm)], [c1,d80])). % 34.41/11.54 cnf(d82, plain, sdtasdt0(xp,sz00) = sdtpldt0(sz00,xp) | ~aInteger0(smndt0(sz10)), inference(resolution, [status(thm)], [c224,d81])). % 34.41/11.54 cnf(d83, plain, sz00 = sdtpldt0(sz00,xp) | ~aInteger0(smndt0(sz10)) | ~aInteger0(smndt0(sz10)), inference(superposition, [status(thm)], [d82,d73])). % 34.41/11.54 cnf(d84, plain, xp = sz00 | ~aInteger0(xp) | ~aInteger0(smndt0(sz10)), inference(superposition, [status(thm)], [d83,c8])). % 34.41/11.54 cnf(d85, plain, xp = sz00 | ~aInteger0(smndt0(sz10)), inference(resolution, [status(thm)], [c224,d84])). % 34.41/11.54 cnf(d86, plain, ~aInteger0(smndt0(sz10)), inference(resolution, [status(thm)], [c225,d85])). % 34.41/11.54 cnf(d87, plain, ~aInteger0(sz10), inference(resolution, [status(thm)], [d86,c2])). % 34.41/11.54 cnf(d88, plain, $false, inference(resolution, [status(thm)], [c1,d87])). % 34.41/11.54 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------