%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM440+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 : n019.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 21.01s 8.91s % Output : CNFRefutation 21.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM440+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.10/5.53 % Computer : n019.cluster.edu % 0.10/5.53 % Model : x86_64 x86_64 % 0.10/5.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/5.53 % Memory : 8046.5625MB % 0.10/5.53 % OS : Linux 6.8.0-71-generic % 0.10/5.53 % CPULimit : 300 % 0.10/5.53 % WCLimit : 300 % 0.10/5.53 % DateTime : Sat Sep 26 02:45:39 UTC 2026 % 0.10/5.53 % CPUTime : % 0.10/5.53 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 21.01/8.91 % SZS status Theorem for theBenchmark.p % 21.01/8.91 % SZS output start CNFRefutation for theBenchmark.p % 21.01/8.91 fof(mIntZero, axiom, aInteger0(sz00)). % 21.01/8.91 fof(mAddNeg, axiom, ! [X0] : ((aInteger0(X0) => (sdtpldt0(X0,smndt0(X0)) = sz00 & sz00 = sdtpldt0(smndt0(X0),X0))))). % 21.01/8.91 fof(mMulZero, axiom, ! [X0] : ((aInteger0(X0) => (sdtasdt0(X0,sz00) = sz00 & sz00 = sdtasdt0(sz00,X0))))). % 21.01/8.91 fof(m__1826, hypothesis, (aSet0(cS1395) & (! [X0] : ((aElementOf0(X0,cS1395) <=> aInteger0(X0))) & (aSet0(xA) & (! [X0] : ((aElementOf0(X0,xA) => aElementOf0(X0,cS1395))) & (aSubsetOf0(xA,cS1395) & (aSet0(cS1395) & (! [X0] : ((aElementOf0(X0,cS1395) <=> aInteger0(X0))) & (aSet0(xB) & (! [X0] : ((aElementOf0(X0,xB) => aElementOf0(X0,cS1395))) & (aSubsetOf0(xB,cS1395) & (aSet0(stldt0(xA)) & (! [X0] : ((aElementOf0(X0,stldt0(xA)) <=> (aInteger0(X0) & ~aElementOf0(X0,xA)))) & (! [X0] : ((aElementOf0(X0,stldt0(xA)) => ? [X1] : ((aInteger0(X1) & (X1 != sz00 & (aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1)) & (! [X2] : (((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) => (aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)))) & (aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0))) & sdteqdtlpzmzozddtrp0(X2,X0,X1))))) & ((aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)))) | (aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0))) | sdteqdtlpzmzozddtrp0(X2,X0,X1)))) => aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))))) & (! [X2] : ((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) => aElementOf0(X2,stldt0(xA)))) & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),stldt0(xA)))))))))) & (isOpen0(stldt0(xA)) & (isClosed0(xA) & (aSet0(stldt0(xB)) & (! [X0] : ((aElementOf0(X0,stldt0(xB)) <=> (aInteger0(X0) & ~aElementOf0(X0,xB)))) & (! [X0] : ((aElementOf0(X0,stldt0(xB)) => ? [X1] : ((aInteger0(X1) & (X1 != sz00 & (aSet0(szAzrzSzezqlpdtcmdtrp0(X0,X1)) & (! [X2] : (((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) => (aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)))) & (aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0))) & sdteqdtlpzmzozddtrp0(X2,X0,X1))))) & ((aInteger0(X2) & (? [X3] : ((aInteger0(X3) & sdtasdt0(X1,X3) = sdtpldt0(X2,smndt0(X0)))) | (aDivisorOf0(X1,sdtpldt0(X2,smndt0(X0))) | sdteqdtlpzmzozddtrp0(X2,X0,X1)))) => aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1))))) & (! [X2] : ((aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,X1)) => aElementOf0(X2,stldt0(xB)))) & aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(X0,X1),stldt0(xB)))))))))) & (isOpen0(stldt0(xB)) & isClosed0(xB))))))))))))))))))))). % 21.01/8.91 fof(m__, conjecture, (((aSet0(stldt0(xA)) & ! [X0] : ((aElementOf0(X0,stldt0(xA)) <=> (aInteger0(X0) & ~aElementOf0(X0,xA))))) => ((aSet0(cS1395) & ! [X0] : ((aElementOf0(X0,cS1395) <=> aInteger0(X0)))) => (! [X0] : ((aElementOf0(X0,stldt0(xA)) => aElementOf0(X0,cS1395))) | aSubsetOf0(stldt0(xA),cS1395)))) & (((aSet0(stldt0(xB)) & ! [X0] : ((aElementOf0(X0,stldt0(xB)) <=> (aInteger0(X0) & ~aElementOf0(X0,xB))))) => ((aSet0(cS1395) & ! [X0] : ((aElementOf0(X0,cS1395) <=> aInteger0(X0)))) => (! [X0] : ((aElementOf0(X0,stldt0(xB)) => aElementOf0(X0,cS1395))) | aSubsetOf0(stldt0(xB),cS1395)))) & ((aSet0(sdtbsmnsldt0(xA,xB)) & ! [X0] : ((aElementOf0(X0,sdtbsmnsldt0(xA,xB)) <=> (aInteger0(X0) & (aElementOf0(X0,xA) | aElementOf0(X0,xB)))))) => ((aSet0(stldt0(sdtbsmnsldt0(xA,xB))) & ! [X0] : ((aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB))) <=> (aInteger0(X0) & ~aElementOf0(X0,sdtbsmnsldt0(xA,xB)))))) => (! [X0] : ((aElementOf0(X0,stldt0(xA)) <=> (aInteger0(X0) & ~aElementOf0(X0,xA)))) => (! [X0] : ((aElementOf0(X0,stldt0(xB)) <=> (aInteger0(X0) & ~aElementOf0(X0,xB)))) => (! [X0] : ((aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB))) <=> (aInteger0(X0) & (aElementOf0(X0,stldt0(xA)) & aElementOf0(X0,stldt0(xB)))))) | stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)))))))))). % 21.01/8.91 fof(negated_conjecture, negated_conjecture, ~((((aSet0(stldt0(xA)) & ! [X0] : ((aElementOf0(X0,stldt0(xA)) <=> (aInteger0(X0) & ~aElementOf0(X0,xA))))) => ((aSet0(cS1395) & ! [X0] : ((aElementOf0(X0,cS1395) <=> aInteger0(X0)))) => (! [X0] : ((aElementOf0(X0,stldt0(xA)) => aElementOf0(X0,cS1395))) | aSubsetOf0(stldt0(xA),cS1395)))) & (((aSet0(stldt0(xB)) & ! [X0] : ((aElementOf0(X0,stldt0(xB)) <=> (aInteger0(X0) & ~aElementOf0(X0,xB))))) => ((aSet0(cS1395) & ! [X0] : ((aElementOf0(X0,cS1395) <=> aInteger0(X0)))) => (! [X0] : ((aElementOf0(X0,stldt0(xB)) => aElementOf0(X0,cS1395))) | aSubsetOf0(stldt0(xB),cS1395)))) & ((aSet0(sdtbsmnsldt0(xA,xB)) & ! [X0] : ((aElementOf0(X0,sdtbsmnsldt0(xA,xB)) <=> (aInteger0(X0) & (aElementOf0(X0,xA) | aElementOf0(X0,xB)))))) => ((aSet0(stldt0(sdtbsmnsldt0(xA,xB))) & ! [X0] : ((aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB))) <=> (aInteger0(X0) & ~aElementOf0(X0,sdtbsmnsldt0(xA,xB)))))) => (! [X0] : ((aElementOf0(X0,stldt0(xA)) <=> (aInteger0(X0) & ~aElementOf0(X0,xA)))) => (! [X0] : ((aElementOf0(X0,stldt0(xB)) <=> (aInteger0(X0) & ~aElementOf0(X0,xB)))) => (! [X0] : ((aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB))) <=> (aInteger0(X0) & (aElementOf0(X0,stldt0(xA)) & aElementOf0(X0,stldt0(xB)))))) | stldt0(sdtbsmnsldt0(xA,xB)) = sdtslmnbsdt0(stldt0(xA),stldt0(xB)))))))))), inference(negate_conjecture, [status(cth)], [m__])). % 21.01/8.91 cnf(c0, plain, aInteger0(sz00), inference(clausification, [status(esa)], [mIntZero])). % 21.01/8.91 cnf(c9, plain, ~aInteger0(X0) | sdtpldt0(X0,smndt0(X0)) = sz00, inference(clausification, [status(esa)], [mAddNeg])). % 21.01/8.91 cnf(c17, plain, ~aInteger0(X0) | sdtasdt0(X0,sz00) = sz00, inference(clausification, [status(esa)], [mMulZero])). % 21.01/8.91 cnf(c144, plain, ~aElementOf0(X0,stldt0(xA)) | X1(X0), inference(clausification, [status(esa)], [m__1826])). % 21.01/8.91 cnf(c159, plain, ~X0(X1) | aInteger0(sK116(X1)), inference(clausification, [status(esa)], [m__1826])). % 21.01/8.91 cnf(c163, plain, sdtasdt0(sK116(X0),X1) != sdtpldt0(X2,smndt0(X0)) | ~X3(X0) | aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X0,sK116(X0))) | ~aInteger0(X1) | ~aInteger0(X2), inference(clausification, [status(esa)], [m__1826])). % 21.01/8.91 cnf(c166, plain, ~X0(X1) | ~aElementOf0(X2,szAzrzSzezqlpdtcmdtrp0(X1,sK116(X1))) | aElementOf0(X2,stldt0(xA)), inference(clausification, [status(esa)], [m__1826])). % 21.01/8.91 cnf(c182, plain, ~X0 | ~X1 | ~X2, inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c185, plain, X0 | ~aElementOf0(X1,sdtbsmnsldt0(xA,xB)) | aElementOf0(X1,xA) | aElementOf0(X1,xB), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c186, plain, X0 | aElementOf0(X1,sdtbsmnsldt0(xA,xB)) | ~aInteger0(X1) | ~aElementOf0(X1,xA), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c187, plain, X0 | aElementOf0(X1,sdtbsmnsldt0(xA,xB)) | ~aInteger0(X1) | ~aElementOf0(X1,xB), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c189, plain, X0 | ~aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB))) | aInteger0(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c190, plain, X0 | ~aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB))) | ~aElementOf0(X1,sdtbsmnsldt0(xA,xB)), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c191, plain, X0 | aElementOf0(X1,stldt0(sdtbsmnsldt0(xA,xB))) | ~aInteger0(X1) | aElementOf0(X1,sdtbsmnsldt0(xA,xB)), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c193, plain, X0 | ~aElementOf0(X1,stldt0(xA)) | ~aElementOf0(X1,xA), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c194, plain, X0 | aElementOf0(X1,stldt0(xA)) | ~aInteger0(X1) | aElementOf0(X1,xA), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c196, plain, X0 | ~aElementOf0(X1,stldt0(xB)) | ~aElementOf0(X1,xB), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c197, plain, X0 | aElementOf0(X1,stldt0(xB)) | ~aInteger0(X1) | aElementOf0(X1,xB), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c199, plain, X0 | aElementOf0(sK132,stldt0(sdtbsmnsldt0(xA,xB))) | aInteger0(sK132), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c200, plain, X0 | aElementOf0(sK132,stldt0(sdtbsmnsldt0(xA,xB))) | aElementOf0(sK132,stldt0(xA)), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c201, plain, X0 | aElementOf0(sK132,stldt0(sdtbsmnsldt0(xA,xB))) | aElementOf0(sK132,stldt0(xB)), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c202, plain, ~aElementOf0(sK132,stldt0(xB)) | ~aElementOf0(sK132,stldt0(xA)) | ~aElementOf0(sK132,stldt0(sdtbsmnsldt0(xA,xB))) | ~aInteger0(sK132) | X0, inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c208, plain, X0 | ~aElementOf0(X1,stldt0(xB)) | aInteger0(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c213, plain, X0 | aElementOf0(X1,cS1395) | ~aInteger0(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c214, plain, X0 | aElementOf0(sK135,stldt0(xB)), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c215, plain, X0 | ~aElementOf0(sK135,cS1395), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c218, plain, X0 | ~aElementOf0(X1,stldt0(xA)) | aInteger0(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c223, plain, X0 | aElementOf0(X1,cS1395) | ~aInteger0(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c224, plain, X0 | aElementOf0(sK138,stldt0(xA)), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(c225, plain, X0 | ~aElementOf0(sK138,cS1395), inference(clausification, [status(esa)], [negated_conjecture])). % 21.01/8.91 cnf(d0, plain, ~aInteger0(sK135) | 'Ts126' | 'Ts126', inference(resolution, [status(thm)], [c213,c215])). % 21.01/8.91 cnf(d1, plain, aInteger0(sK135) | 'Ts126' | 'Ts126', inference(resolution, [status(thm)], [c208,c214])). % 21.01/8.91 cnf(d2, plain, 'Ts126' | 'Ts126', inference(resolution, [status(thm)], [d1,d0])). % 21.01/8.91 cnf(d3, plain, ~'Ts125' | ~'Ts127', inference(resolution, [status(thm)], [d2,c182])). % 21.01/8.91 cnf(d4, plain, ~aInteger0(sK138) | 'Ts127' | 'Ts127', inference(resolution, [status(thm)], [c223,c225])). % 21.01/8.91 cnf(d5, plain, aInteger0(sK138) | 'Ts127' | 'Ts127', inference(resolution, [status(thm)], [c218,c224])). % 21.01/8.91 cnf(d6, plain, 'Ts127' | 'Ts127', inference(resolution, [status(thm)], [d5,d4])). % 21.01/8.91 cnf(d7, plain, ~'Ts125', inference(resolution, [status(thm)], [d6,d3])). % 21.01/8.91 cnf(d8, plain, ~aInteger0(X0) | aElementOf0(X0,stldt0(xB)) | aElementOf0(X0,xB), inference(resolution, [status(thm)], [d7,c197])). % 21.01/8.91 cnf(d9, plain, ~aElementOf0(X0,sdtbsmnsldt0(xA,xB)) | aElementOf0(X0,xA) | aElementOf0(X0,xB), inference(resolution, [status(thm)], [d7,c185])). % 21.01/8.91 cnf(d10, plain, ~aInteger0(X0) | aElementOf0(X0,sdtbsmnsldt0(xA,xB)) | aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB))), inference(resolution, [status(thm)], [d7,c191])). % 21.01/8.91 cnf(d11, plain, ~aInteger0(sK132) | ~aElementOf0(sK132,stldt0(sdtbsmnsldt0(xA,xB))) | ~aElementOf0(sK132,stldt0(xA)) | ~aElementOf0(sK132,stldt0(xB)), inference(resolution, [status(thm)], [d7,c202])). % 21.01/8.91 cnf(d12, plain, aInteger0(X0) | ~aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB))), inference(resolution, [status(thm)], [d7,c189])). % 21.01/8.91 cnf(d13, plain, aInteger0(sK132) | aElementOf0(sK132,stldt0(sdtbsmnsldt0(xA,xB))), inference(resolution, [status(thm)], [d7,c199])). % 21.01/8.91 cnf(d14, plain, aInteger0(sK132) | aInteger0(sK132), inference(resolution, [status(thm)], [d13,d12])). % 21.01/8.91 cnf(d15, plain, ~aElementOf0(sK132,stldt0(sdtbsmnsldt0(xA,xB))) | ~aElementOf0(sK132,stldt0(xA)) | ~aElementOf0(sK132,stldt0(xB)), inference(resolution, [status(thm)], [d14,d11])). % 21.01/8.91 cnf(d16, plain, sdtpldt0(sK132,smndt0(sK132)) = sz00, inference(resolution, [status(thm)], [d14,c9])). % 21.01/8.91 cnf(d17, plain, sdtasdt0(sK116(sK132),X0) != sz00 | ~aInteger0(sK132) | ~aInteger0(X0) | aElementOf0(sK132,szAzrzSzezqlpdtcmdtrp0(sK132,sK116(sK132))) | ~'Ts104'(sK132), inference(superposition, [status(thm)], [d16,c163])). % 21.01/8.91 cnf(d18, plain, sdtasdt0(sK116(sK132),X0) != sz00 | ~aInteger0(X0) | aElementOf0(sK132,szAzrzSzezqlpdtcmdtrp0(sK132,sK116(sK132))) | ~'Ts104'(sK132), inference(resolution, [status(thm)], [d14,d17])). % 21.01/8.91 cnf(d19, plain, ~aInteger0(X0) | aElementOf0(X0,stldt0(xA)) | aElementOf0(X0,xA), inference(resolution, [status(thm)], [d7,c194])). % 21.01/8.91 cnf(d20, plain, 'Ts104'(X0) | ~aInteger0(X0) | aElementOf0(X0,xA), inference(resolution, [status(thm)], [c144,d19])). % 21.01/8.91 cnf(d21, plain, ~aElementOf0(X0,stldt0(xA)) | ~aElementOf0(X0,xA), inference(resolution, [status(thm)], [d7,c193])). % 21.01/8.91 cnf(d22, plain, ~aInteger0(X0) | aElementOf0(X0,sdtbsmnsldt0(xA,xB)) | ~aElementOf0(X0,xA), inference(resolution, [status(thm)], [d7,c186])). % 21.01/8.91 cnf(d23, plain, aElementOf0(sK132,stldt0(sdtbsmnsldt0(xA,xB))) | aElementOf0(sK132,stldt0(xA)), inference(resolution, [status(thm)], [d7,c200])). % 21.01/8.91 cnf(d24, plain, ~aElementOf0(X0,sdtbsmnsldt0(xA,xB)) | ~aElementOf0(X0,stldt0(sdtbsmnsldt0(xA,xB))), inference(resolution, [status(thm)], [d7,c190])). % 21.01/8.91 cnf(d25, plain, ~aElementOf0(sK132,sdtbsmnsldt0(xA,xB)) | aElementOf0(sK132,stldt0(xA)), inference(resolution, [status(thm)], [d24,d23])). % 21.01/8.91 cnf(d26, plain, aElementOf0(sK132,stldt0(xA)) | ~aInteger0(sK132) | ~aElementOf0(sK132,xA), inference(resolution, [status(thm)], [d25,d22])). % 21.01/8.91 cnf(d27, plain, aElementOf0(sK132,stldt0(xA)) | ~aElementOf0(sK132,xA), inference(resolution, [status(thm)], [d14,d26])). % 21.01/8.91 cnf(d28, plain, ~aElementOf0(sK132,xA) | ~aElementOf0(sK132,xA), inference(resolution, [status(thm)], [d27,d21])). % 21.01/8.91 cnf(d29, plain, ~aInteger0(sK132) | 'Ts104'(sK132), inference(resolution, [status(thm)], [d28,d20])). % 21.01/8.91 cnf(d30, plain, 'Ts104'(sK132), inference(resolution, [status(thm)], [d14,d29])). % 21.01/8.91 cnf(d31, plain, sdtasdt0(sK116(sK132),X0) != sz00 | ~aInteger0(X0) | aElementOf0(sK132,szAzrzSzezqlpdtcmdtrp0(sK132,sK116(sK132))), inference(resolution, [status(thm)], [d30,d18])). % 21.01/8.91 cnf(d32, plain, ~'Ts104'(X0) | sdtasdt0(sK116(X0),sz00) = sz00, inference(resolution, [status(thm)], [c159,c17])). % 21.01/8.91 cnf(d33, plain, sdtasdt0(sK116(sK132),sz00) = sz00, inference(resolution, [status(thm)], [d32,d30])). % 21.01/8.91 cnf(d34, plain, sz00 != sz00 | ~aInteger0(sz00) | aElementOf0(sK132,szAzrzSzezqlpdtcmdtrp0(sK132,sK116(sK132))), inference(superposition, [status(thm)], [d33,d31])). % 21.01/8.91 cnf(d35, plain, sz00 != sz00 | aElementOf0(sK132,szAzrzSzezqlpdtcmdtrp0(sK132,sK116(sK132))), inference(resolution, [status(thm)], [c0,d34])). % 21.01/8.91 cnf(d36, plain, aElementOf0(sK132,szAzrzSzezqlpdtcmdtrp0(sK132,sK116(sK132))), inference(equality_resolution, [status(thm)], [d35])). % 21.01/8.91 cnf(d37, plain, aElementOf0(sK132,stldt0(xA)) | ~'Ts104'(sK132), inference(resolution, [status(thm)], [d36,c166])). % 21.01/8.91 cnf(d38, plain, aElementOf0(sK132,stldt0(xA)), inference(resolution, [status(thm)], [d30,d37])). % 21.01/8.91 cnf(d39, plain, ~aElementOf0(sK132,stldt0(sdtbsmnsldt0(xA,xB))) | ~aElementOf0(sK132,stldt0(xB)), inference(resolution, [status(thm)], [d38,d15])). % 21.01/8.91 cnf(d40, plain, ~aElementOf0(sK132,stldt0(xB)) | ~aInteger0(sK132) | aElementOf0(sK132,sdtbsmnsldt0(xA,xB)), inference(resolution, [status(thm)], [d39,d10])). % 21.01/8.91 cnf(d41, plain, aElementOf0(sK132,sdtbsmnsldt0(xA,xB)) | ~aElementOf0(sK132,stldt0(xB)), inference(resolution, [status(thm)], [d14,d40])). % 21.01/8.91 cnf(d42, plain, ~aElementOf0(sK132,stldt0(xB)) | aElementOf0(sK132,xA) | aElementOf0(sK132,xB), inference(resolution, [status(thm)], [d41,d9])). % 21.01/8.91 cnf(d43, plain, ~aElementOf0(X0,stldt0(xB)) | ~aElementOf0(X0,xB), inference(resolution, [status(thm)], [d7,c196])). % 21.01/8.91 cnf(d44, plain, ~aInteger0(X0) | aElementOf0(X0,sdtbsmnsldt0(xA,xB)) | ~aElementOf0(X0,xB), inference(resolution, [status(thm)], [d7,c187])). % 21.01/8.91 cnf(d45, plain, aElementOf0(sK132,stldt0(sdtbsmnsldt0(xA,xB))) | aElementOf0(sK132,stldt0(xB)), inference(resolution, [status(thm)], [d7,c201])). % 21.01/8.91 cnf(d46, plain, ~aElementOf0(sK132,sdtbsmnsldt0(xA,xB)) | aElementOf0(sK132,stldt0(xB)), inference(resolution, [status(thm)], [d24,d45])). % 21.01/8.91 cnf(d47, plain, aElementOf0(sK132,stldt0(xB)) | ~aInteger0(sK132) | ~aElementOf0(sK132,xB), inference(resolution, [status(thm)], [d46,d44])). % 21.01/8.91 cnf(d48, plain, aElementOf0(sK132,stldt0(xB)) | ~aElementOf0(sK132,xB), inference(resolution, [status(thm)], [d14,d47])). % 21.01/8.91 cnf(d49, plain, ~aElementOf0(sK132,xB) | ~aElementOf0(sK132,xB), inference(resolution, [status(thm)], [d48,d43])). % 21.01/8.91 cnf(d50, plain, ~aElementOf0(sK132,stldt0(xB)) | aElementOf0(sK132,xA), inference(resolution, [status(thm)], [d49,d42])). % 21.01/8.91 cnf(d51, plain, ~aElementOf0(sK132,stldt0(xB)), inference(resolution, [status(thm)], [d28,d50])). % 21.01/8.91 cnf(d52, plain, ~aInteger0(sK132) | aElementOf0(sK132,xB), inference(resolution, [status(thm)], [d51,d8])). % 21.01/8.91 cnf(d53, plain, aElementOf0(sK132,xB), inference(resolution, [status(thm)], [d14,d52])). % 21.01/8.91 cnf(d54, plain, $false, inference(resolution, [status(thm)], [d49,d53])). % 21.01/8.91 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------