%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM630+3 : 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 : 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:13:24 AM UTC 2026 % Result : Theorem 178.91s 23.22s % Output : CNFRefutation 178.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : NUM630+3 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.17/0.43 % Computer : n026.cluster.edu % 0.17/0.43 % Model : x86_64 x86_64 % 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.43 % Memory : 8046.5625MB % 0.17/0.43 % OS : Linux 6.8.0-71-generic % 0.17/0.43 % CPULimit : 300 % 0.17/0.43 % WCLimit : 300 % 0.17/0.43 % DateTime : Sat Sep 26 03:33:25 UTC 2026 % 0.17/0.43 % CPUTime : % 0.17/0.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 178.91/23.22 % SZS status Theorem for theBenchmark.p % 178.91/23.22 % SZS output start CNFRefutation for theBenchmark.p % 178.91/23.22 fof(mEOfElem, axiom, ! [X0] : ((aSet0(X0) => ! [X1] : ((aElementOf0(X1,X0) => aElement0(X1)))))). % 178.91/23.22 fof(mDefSub, definition, ! [X0] : ((aSet0(X0) => ! [X1] : ((aSubsetOf0(X1,X0) <=> (aSet0(X1) & ! [X2] : ((aElementOf0(X2,X1) => aElementOf0(X2,X0))))))))). % 178.91/23.22 fof(mSubASymm, axiom, ! [X0] : ! [X1] : (((aSet0(X0) & aSet0(X1)) => ((aSubsetOf0(X0,X1) & aSubsetOf0(X1,X0)) => X0 = X1)))). % 178.91/23.22 fof(mSubTrans, axiom, ! [X0] : ! [X1] : ! [X2] : (((aSet0(X0) & (aSet0(X1) & aSet0(X2))) => ((aSubsetOf0(X0,X1) & aSubsetOf0(X1,X2)) => aSubsetOf0(X0,X2))))). % 178.91/23.22 fof(mConsDiff, axiom, ! [X0] : ((aSet0(X0) => ! [X1] : ((aElementOf0(X1,X0) => sdtpldt0(sdtmndt0(X0,X1),X1) = X0))))). % 178.91/23.22 fof(m__3435, hypothesis, (aSet0(xS) & (! [X0] : ((aElementOf0(X0,xS) => aElementOf0(X0,szNzAzT0))) & (aSubsetOf0(xS,szNzAzT0) & isCountable0(xS))))). % 178.91/23.22 fof(m__4151, hypothesis, (aFunction0(xC) & (szDzozmdt0(xC) = szNzAzT0 & ! [X0] : ((aElementOf0(X0,szNzAzT0) => (aFunction0(sdtlpdtrp0(xC,X0)) & (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) & (! [X1] : ((aElementOf0(X1,sdtlpdtrp0(xN,X0)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1))) & (aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) & (! [X1] : ((aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) <=> (aElement0(X1) & (aElementOf0(X1,sdtlpdtrp0(xN,X0)) & X1 != szmzizndt0(sdtlpdtrp0(xN,X0)))))) & (! [X1] : (((aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0))) => (aSet0(X1) & (! [X2] : ((aElementOf0(X2,X1) => aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))) & (aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) & sbrdtbr0(X1) = xk)))) & ((((aSet0(X1) & ! [X2] : ((aElementOf0(X2,X1) => aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))))) | aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))) & sbrdtbr0(X1) = xk) => aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0)))))) & (szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk) & ! [X1] : (((aSet0(X1) & ((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) & ! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X0)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2)))) => ((aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) & ! [X2] : ((aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) <=> (aElement0(X2) & (aElementOf0(X2,sdtlpdtrp0(xN,X0)) & X2 != szmzizndt0(sdtlpdtrp0(xN,X0))))))) => (((! [X2] : ((aElementOf0(X2,X1) => aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))) | aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))) & sbrdtbr0(X1) = xk) | aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)))))) => (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) & (! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X0)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2))) & (! [X2] : ((aElementOf0(X2,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) <=> (aElement0(X2) & (aElementOf0(X2,X1) | X2 = szmzizndt0(sdtlpdtrp0(xN,X0)))))) & sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))))))))))))))))))). % 178.91/23.22 fof(m__4660, hypothesis, (aFunction0(xe) & (szDzozmdt0(xe) = szNzAzT0 & ! [X0] : ((aElementOf0(X0,szNzAzT0) => (aElementOf0(sdtlpdtrp0(xe,X0),sdtlpdtrp0(xN,X0)) & (! [X1] : ((aElementOf0(X1,sdtlpdtrp0(xN,X0)) => sdtlseqdt0(sdtlpdtrp0(xe,X0),X1))) & sdtlpdtrp0(xe,X0) = szmzizndt0(sdtlpdtrp0(xN,X0))))))))). % 178.91/23.22 fof(m__4891, hypothesis, (aSet0(xO) & (aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))) & (! [X0] : ((aElementOf0(X0,sdtlbdtrb0(xd,szDzizrdt0(xd))) <=> (aElementOf0(X0,szDzozmdt0(xd)) & sdtlpdtrp0(xd,X0) = szDzizrdt0(xd)))) & (! [X0] : ((aElementOf0(X0,xO) <=> ? [X1] : ((aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd))) & sdtlpdtrp0(xe,X1) = X0)))) & xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd)))))))). % 178.91/23.22 fof(m__4998, hypothesis, (! [X0] : ((aElementOf0(X0,xO) => aElementOf0(X0,xS))) & aSubsetOf0(xO,xS))). % 178.91/23.22 fof(m__5078, hypothesis, (aSet0(xQ) & (! [X0] : ((aElementOf0(X0,xQ) => aElementOf0(X0,xO))) & (aSubsetOf0(xQ,xO) & (sbrdtbr0(xQ) = xK & aElementOf0(xQ,slbdtsldtrb0(xO,xK))))))). % 178.91/23.22 fof(m__5147, hypothesis, (aElementOf0(xp,xQ) & (! [X0] : ((aElementOf0(X0,xQ) => sdtlseqdt0(xp,X0))) & xp = szmzizndt0(xQ)))). % 178.91/23.22 fof(m__5164, hypothesis, (aSet0(xP) & (! [X0] : ((aElementOf0(X0,xQ) => sdtlseqdt0(szmzizndt0(xQ),X0))) & (! [X0] : ((aElementOf0(X0,xP) <=> (aElement0(X0) & (aElementOf0(X0,xQ) & X0 != szmzizndt0(xQ))))) & xP = sdtmndt0(xQ,szmzizndt0(xQ)))))). % 178.91/23.22 fof(m__5208, hypothesis, (! [X0] : ((aElementOf0(X0,xP) => aElementOf0(X0,xO))) & aSubsetOf0(xP,xO))). % 178.91/23.22 fof(m__5309, hypothesis, (aElementOf0(xn,szDzozmdt0(xd)) & (sdtlpdtrp0(xd,xn) = szDzizrdt0(xd) & (aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd))) & (aElementOf0(xn,szNzAzT0) & sdtlpdtrp0(xe,xn) = xp))))). % 178.91/23.22 fof(m__5585, hypothesis, (! [X0] : ((aElementOf0(X0,sdtlpdtrp0(xN,xn)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0))) & (aSet0(xD) & (! [X0] : ((aElementOf0(X0,xD) <=> (aElement0(X0) & (aElementOf0(X0,sdtlpdtrp0(xN,xn)) & X0 != szmzizndt0(sdtlpdtrp0(xN,xn)))))) & xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))))). % 178.91/23.22 fof(m__5599, hypothesis, (! [X0] : ((aElementOf0(X0,xP) => aElementOf0(X0,xD))) & (aSubsetOf0(xP,xD) & aElementOf0(xP,slbdtsldtrb0(xD,xk))))). % 178.91/23.22 fof(m__, conjecture, (! [X0] : ((aElementOf0(X0,sdtlpdtrp0(xN,xn)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0))) => ((aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) & ! [X0] : ((aElementOf0(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) <=> (aElement0(X0) & (aElementOf0(X0,xP) | X0 = szmzizndt0(sdtlpdtrp0(xN,xn))))))) => sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)))). % 178.91/23.22 fof(negated_conjecture, negated_conjecture, ~((! [X0] : ((aElementOf0(X0,sdtlpdtrp0(xN,xn)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0))) => ((aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) & ! [X0] : ((aElementOf0(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) <=> (aElement0(X0) & (aElementOf0(X0,xP) | X0 = szmzizndt0(sdtlpdtrp0(xN,xn))))))) => sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP)))), inference(negate_conjecture, [status(cth)], [m__])). % 178.91/23.22 cnf(c0, plain, ~aSet0(X0) | ~aElementOf0(X1,X0) | aElement0(X1), inference(clausification, [status(esa)], [mEOfElem])). % 178.91/23.22 cnf(c8, plain, ~aSet0(X0) | ~aSubsetOf0(X1,X0) | ~aElementOf0(X2,X1) | aElementOf0(X2,X0), inference(clausification, [status(esa)], [mDefSub])). % 178.91/23.22 cnf(c9, plain, ~aSet0(X0) | aSubsetOf0(X1,X0) | ~aSet0(X1) | aElementOf0(sK14(X0,X1),X1), inference(clausification, [status(esa)], [mDefSub])). % 178.91/23.22 cnf(c10, plain, ~aSet0(X0) | aSubsetOf0(X1,X0) | ~aSet0(X1) | ~aElementOf0(sK14(X0,X1),X0), inference(clausification, [status(esa)], [mDefSub])). % 178.91/23.22 cnf(c13, plain, ~aSubsetOf0(X0,X1) | ~aSet0(X1) | X1 = X0 | ~aSet0(X0) | ~aSubsetOf0(X1,X0), inference(clausification, [status(esa)], [mSubASymm])). % 178.91/23.22 cnf(c14, plain, ~aSubsetOf0(X0,X1) | ~aSet0(X1) | ~aSet0(X0) | ~aSet0(X2) | ~aSubsetOf0(X2,X0) | aSubsetOf0(X2,X1), inference(clausification, [status(esa)], [mSubTrans])). % 178.91/23.22 cnf(c46, plain, ~aSet0(X0) | ~aElementOf0(X1,X0) | sdtpldt0(sdtmndt0(X0,X1),X1) = X0, inference(clausification, [status(esa)], [mConsDiff])). % 178.91/23.22 cnf(c175, plain, aSet0(xS), inference(clausification, [status(esa)], [m__3435])). % 178.91/23.22 cnf(c281, plain, ~aElementOf0(X0,szNzAzT0) | X1(X0), inference(clausification, [status(esa)], [m__4151])). % 178.91/23.22 cnf(c292, plain, X0(X1,X2) | ~aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk)), inference(clausification, [status(esa)], [m__4151])). % 178.91/23.22 cnf(c299, plain, ~X0(X1,X2) | sdtlpdtrp0(sdtlpdtrp0(xC,X1),X2) = sdtlpdtrp0(xc,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1)))), inference(clausification, [status(esa)], [m__4151])). % 178.91/23.22 cnf(c316, plain, ~X0(X1) | ~aSet0(X2) | ~X3(X1,X2) | X4(X1,X2), inference(clausification, [status(esa)], [m__4151])). % 178.91/23.22 cnf(c375, plain, ~aElementOf0(X0,szNzAzT0) | sdtlpdtrp0(xe,X0) = szmzizndt0(sdtlpdtrp0(xN,X0)), inference(clausification, [status(esa)], [m__4660])). % 178.91/23.22 cnf(c393, plain, aSet0(xO), inference(clausification, [status(esa)], [m__4891])). % 178.91/23.22 cnf(c411, plain, aSubsetOf0(xO,xS), inference(clausification, [status(esa)], [m__4998])). % 178.91/23.22 cnf(c412, plain, aSet0(xQ), inference(clausification, [status(esa)], [m__5078])). % 178.91/23.22 cnf(c427, plain, aElementOf0(xp,xQ), inference(clausification, [status(esa)], [m__5147])). % 178.91/23.22 cnf(c429, plain, xp = szmzizndt0(xQ), inference(clausification, [status(esa)], [m__5147])). % 178.91/23.22 cnf(c430, plain, aSet0(xP), inference(clausification, [status(esa)], [m__5164])). % 178.91/23.22 cnf(c434, plain, ~aElementOf0(X0,xP) | X0 != szmzizndt0(xQ), inference(clausification, [status(esa)], [m__5164])). % 178.91/23.22 cnf(c436, plain, xP = sdtmndt0(xQ,szmzizndt0(xQ)), inference(clausification, [status(esa)], [m__5164])). % 178.91/23.22 cnf(c443, plain, aSubsetOf0(xP,xO), inference(clausification, [status(esa)], [m__5208])). % 178.91/23.22 cnf(c449, plain, aElementOf0(xn,szNzAzT0), inference(clausification, [status(esa)], [m__5309])). % 178.91/23.22 cnf(c450, plain, sdtlpdtrp0(xe,xn) = xp, inference(clausification, [status(esa)], [m__5309])). % 178.91/23.22 cnf(c460, plain, xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))), inference(clausification, [status(esa)], [m__5585])). % 178.91/23.22 cnf(c463, plain, aElementOf0(xP,slbdtsldtrb0(xD,xk)), inference(clausification, [status(esa)], [m__5599])). % 178.91/23.22 cnf(c465, plain, aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))), inference(clausification, [status(esa)], [negated_conjecture])). % 178.91/23.22 cnf(c467, plain, ~aElementOf0(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | aElementOf0(X0,xP) | X0 = szmzizndt0(sdtlpdtrp0(xN,xn)), inference(clausification, [status(esa)], [negated_conjecture])). % 178.91/23.22 cnf(c468, plain, aElementOf0(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~aElement0(X0) | ~aElementOf0(X0,xP), inference(clausification, [status(esa)], [negated_conjecture])). % 178.91/23.22 cnf(c469, plain, aElementOf0(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~aElement0(X0) | X0 != szmzizndt0(sdtlpdtrp0(xN,xn)), inference(clausification, [status(esa)], [negated_conjecture])). % 178.91/23.22 cnf(c470, plain, sdtlpdtrp0(xc,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) != sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP), inference(clausification, [status(esa)], [negated_conjecture])). % 178.91/23.22 cnf(d0, plain, ~aSet0(X0) | ~aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | aSubsetOf0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),X0) | sK14(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = szmzizndt0(sdtlpdtrp0(xN,xn)) | aElementOf0(sK14(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))),xP), inference(resolution, [status(thm)], [c9,c467])). % 178.91/23.22 cnf(d1, plain, sK14(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) = szmzizndt0(sdtlpdtrp0(xN,xn)) | ~aSet0(X0) | aElementOf0(sK14(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))),xP) | aSubsetOf0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),X0), inference(resolution, [status(thm)], [c465,d0])). % 178.91/23.22 cnf(d2, plain, ~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0) | ~aSet0(X0) | ~aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | aSubsetOf0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),X0) | ~aSet0(X0) | aElementOf0(sK14(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))),xP) | aSubsetOf0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),X0), inference(superposition, [status(thm)], [d1,c10])). % 178.91/23.22 cnf(d3, plain, ~aSet0(X0) | aElementOf0(sK14(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))),xP) | ~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),X0) | aSubsetOf0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),X0), inference(resolution, [status(thm)], [c465,d2])). % 178.91/23.22 cnf(d4, plain, ~aSet0(xP) | ~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),xP) | aSubsetOf0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),xP) | ~aSet0(xP) | ~aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | aSubsetOf0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),xP), inference(resolution, [status(thm)], [d3,c10])). % 178.91/23.22 cnf(d5, plain, ~aSet0(xP) | ~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),xP) | aSubsetOf0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),xP), inference(resolution, [status(thm)], [c465,d4])). % 178.91/23.22 cnf(d6, plain, ~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),xP) | aSubsetOf0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),xP), inference(resolution, [status(thm)], [c430,d5])). % 178.91/23.22 cnf(d7, plain, aSubsetOf0(sdtpldt0(xP,sdtlpdtrp0(xe,xn)),xP) | ~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),xP) | ~aElementOf0(xn,szNzAzT0), inference(superposition, [status(thm)], [c375,d6])). % 178.91/23.22 cnf(d8, plain, ~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),xP) | ~aElementOf0(xn,szNzAzT0) | aSubsetOf0(sdtpldt0(xP,xp),xP), inference(demodulation, [status(thm)], [d7,c450])). % 178.91/23.22 cnf(d9, plain, ~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xn)),xP) | aSubsetOf0(sdtpldt0(xP,xp),xP), inference(resolution, [status(thm)], [c449,d8])). % 178.91/23.22 cnf(d10, plain, ~aElementOf0(sdtlpdtrp0(xe,xn),xP) | aSubsetOf0(sdtpldt0(xP,xp),xP) | ~aElementOf0(xn,szNzAzT0), inference(superposition, [status(thm)], [c375,d9])). % 178.91/23.22 cnf(d11, plain, ~aElementOf0(xp,xP) | ~aElementOf0(xn,szNzAzT0) | aSubsetOf0(sdtpldt0(xP,xp),xP), inference(demodulation, [status(thm)], [d10,c450])). % 178.91/23.22 cnf(d12, plain, ~aElementOf0(xp,xP) | aSubsetOf0(sdtpldt0(xP,xp),xP), inference(resolution, [status(thm)], [c449,d11])). % 178.91/23.22 cnf(d13, plain, X0 != sdtlpdtrp0(xe,xn) | aElementOf0(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~aElement0(X0) | ~aElementOf0(xn,szNzAzT0), inference(superposition, [status(thm)], [c375,c469])). % 178.91/23.22 cnf(d14, plain, X0 != xp | aElementOf0(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~aElementOf0(xn,szNzAzT0) | ~aElement0(X0), inference(demodulation, [status(thm)], [d13,c450])). % 178.91/23.22 cnf(d15, plain, X0 != xp | aElementOf0(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~aElement0(X0), inference(resolution, [status(thm)], [c449,d14])). % 178.91/23.22 cnf(d16, plain, aElementOf0(xp,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~aElement0(xp), inference(equality_resolution, [status(thm)], [d15])). % 178.91/23.22 cnf(d17, plain, ~aSet0(xQ) | aElement0(xp), inference(resolution, [status(thm)], [c427,c0])). % 178.91/23.22 cnf(d18, plain, aElement0(xp), inference(resolution, [status(thm)], [c412,d17])). % 178.91/23.22 cnf(d19, plain, aElementOf0(xp,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))), inference(resolution, [status(thm)], [d18,d16])). % 178.91/23.22 cnf(d20, plain, xp = szmzizndt0(sdtlpdtrp0(xN,xn)) | aElementOf0(xp,xP), inference(resolution, [status(thm)], [d19,c467])). % 178.91/23.22 cnf(d21, plain, ~aElementOf0(X0,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xn),xp),xk)) | 'Ts214'(xn,X0) | aElementOf0(xp,xP), inference(superposition, [status(thm)], [d20,c292])). % 178.91/23.22 cnf(d22, plain, xD = sdtmndt0(sdtlpdtrp0(xN,xn),xp) | aElementOf0(xp,xP), inference(superposition, [status(thm)], [d20,c460])). % 178.91/23.22 cnf(d23, plain, ~aElementOf0(X0,slbdtsldtrb0(xD,xk)) | aElementOf0(xp,xP) | 'Ts214'(xn,X0) | aElementOf0(xp,xP), inference(superposition, [status(thm)], [d22,d21])). % 178.91/23.22 cnf(d24, plain, aElementOf0(xp,xP) | 'Ts214'(xn,xP), inference(resolution, [status(thm)], [d23,c463])). % 178.91/23.22 cnf(d25, plain, aElementOf0(xp,xP) | ~aSet0(xP) | ~'Ts216'(xn) | 'Ts215'(xn,xP), inference(resolution, [status(thm)], [d24,c316])). % 178.91/23.22 cnf(d26, plain, aElementOf0(xp,xP) | ~'Ts216'(xn) | 'Ts215'(xn,xP), inference(resolution, [status(thm)], [c430,d25])). % 178.91/23.22 cnf(d27, plain, 'Ts216'(xn), inference(resolution, [status(thm)], [c281,c449])). % 178.91/23.22 cnf(d28, plain, aElementOf0(xp,xP) | 'Ts215'(xn,xP), inference(resolution, [status(thm)], [d27,d26])). % 178.91/23.22 cnf(d29, plain, sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) != sdtlpdtrp0(sdtlpdtrp0(xC,xn),xP) | ~'Ts215'(xn,xP), inference(superposition, [status(thm)], [c299,c470])). % 178.91/23.22 cnf(d30, plain, ~'Ts215'(xn,xP), inference(equality_resolution, [status(thm)], [d29])). % 178.91/23.22 cnf(d31, plain, aElementOf0(xp,xP), inference(resolution, [status(thm)], [d30,d28])). % 178.91/23.22 cnf(d32, plain, aSubsetOf0(sdtpldt0(xP,xp),xP), inference(resolution, [status(thm)], [d31,d12])). % 178.91/23.22 cnf(d33, plain, xP = sdtpldt0(xP,xp) | ~aSet0(xP) | ~aSet0(sdtpldt0(xP,xp)) | ~aSubsetOf0(xP,sdtpldt0(xP,xp)), inference(resolution, [status(thm)], [d32,c13])). % 178.91/23.22 cnf(d34, plain, xP = sdtpldt0(xP,xp) | ~aSet0(sdtpldt0(xP,xp)) | ~aSubsetOf0(xP,sdtpldt0(xP,xp)), inference(resolution, [status(thm)], [c430,d33])). % 178.91/23.22 cnf(d35, plain, aSet0(sdtpldt0(xP,sdtlpdtrp0(xe,xn))) | ~aElementOf0(xn,szNzAzT0), inference(superposition, [status(thm)], [c375,c465])). % 178.91/23.22 cnf(d36, plain, aSet0(sdtpldt0(xP,xp)) | ~aElementOf0(xn,szNzAzT0), inference(demodulation, [status(thm)], [d35,c450])). % 178.91/23.22 cnf(d37, plain, aSet0(sdtpldt0(xP,xp)), inference(resolution, [status(thm)], [c449,d36])). % 178.91/23.22 cnf(d38, plain, xP = sdtpldt0(xP,xp) | ~aSubsetOf0(xP,sdtpldt0(xP,xp)), inference(resolution, [status(thm)], [d37,d34])). % 178.91/23.22 cnf(d39, plain, ~aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~aSet0(X0) | aSubsetOf0(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~aElementOf0(sK14(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),X0),xP) | ~aElement0(sK14(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),X0)), inference(resolution, [status(thm)], [c10,c468])). % 178.91/23.22 cnf(d40, plain, ~aSet0(X0) | ~aElementOf0(sK14(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),X0),xP) | ~aElement0(sK14(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),X0)) | aSubsetOf0(X0,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))), inference(resolution, [status(thm)], [c465,d39])). % 178.91/23.22 cnf(d41, plain, ~aSet0(xP) | ~aElement0(sK14(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),xP)) | aSubsetOf0(xP,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~aSet0(xP) | aSubsetOf0(xP,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))), inference(resolution, [status(thm)], [d40,c9])). % 178.91/23.22 cnf(d42, plain, ~aSet0(xP) | ~aElement0(sK14(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),xP)) | aSubsetOf0(xP,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))), inference(resolution, [status(thm)], [c465,d41])). % 178.91/23.22 cnf(d43, plain, ~aElement0(sK14(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn))),xP)) | aSubsetOf0(xP,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))), inference(resolution, [status(thm)], [c430,d42])). % 178.91/23.22 cnf(d44, plain, ~aSet0(X0) | ~aSet0(X1) | aSubsetOf0(X1,X0) | ~aSet0(X1) | aElement0(sK14(X0,X1)), inference(resolution, [status(thm)], [c9,c0])). % 178.91/23.22 cnf(d45, plain, aElementOf0(X0,sdtpldt0(xP,sdtlpdtrp0(xe,xn))) | ~aElementOf0(X0,xP) | ~aElement0(X0) | ~aElementOf0(xn,szNzAzT0), inference(superposition, [status(thm)], [c375,c468])). % 178.91/23.22 cnf(d46, plain, aElementOf0(X0,sdtpldt0(xP,xp)) | ~aElementOf0(X0,xP) | ~aElementOf0(xn,szNzAzT0) | ~aElement0(X0), inference(demodulation, [status(thm)], [d45,c450])). % 178.91/23.22 cnf(d47, plain, aElementOf0(X0,sdtpldt0(xP,xp)) | ~aElementOf0(X0,xP) | ~aElement0(X0), inference(resolution, [status(thm)], [c449,d46])). % 178.91/23.22 cnf(d48, plain, ~aSet0(X0) | ~aSet0(xS) | ~aSet0(xO) | aSubsetOf0(X0,xS) | ~aSubsetOf0(X0,xO), inference(resolution, [status(thm)], [c14,c411])). % 178.91/23.22 cnf(d49, plain, ~aSet0(X0) | ~aSet0(xO) | aSubsetOf0(X0,xS) | ~aSubsetOf0(X0,xO), inference(resolution, [status(thm)], [c175,d48])). % 178.91/23.22 cnf(d50, plain, ~aSet0(X0) | aSubsetOf0(X0,xS) | ~aSubsetOf0(X0,xO), inference(resolution, [status(thm)], [c393,d49])). % 178.91/23.22 cnf(d51, plain, ~aSet0(X0) | ~aSet0(xO) | ~aSet0(xP) | aSubsetOf0(X0,xO) | ~aSubsetOf0(X0,xP), inference(resolution, [status(thm)], [c14,c443])). % 178.91/23.22 cnf(d52, plain, ~aSet0(X0) | ~aSet0(xP) | aSubsetOf0(X0,xO) | ~aSubsetOf0(X0,xP), inference(resolution, [status(thm)], [c393,d51])). % 178.91/23.22 cnf(d53, plain, ~aSet0(X0) | aSubsetOf0(X0,xO) | ~aSubsetOf0(X0,xP), inference(resolution, [status(thm)], [c430,d52])). % 178.91/23.22 cnf(d54, plain, ~aSet0(sdtpldt0(xP,xp)) | aSubsetOf0(sdtpldt0(xP,xp),xO), inference(resolution, [status(thm)], [d53,d32])). % 178.91/23.22 cnf(d55, plain, aSubsetOf0(sdtpldt0(xP,xp),xO), inference(resolution, [status(thm)], [d37,d54])). % 178.91/23.22 cnf(d56, plain, ~aSet0(sdtpldt0(xP,xp)) | aSubsetOf0(sdtpldt0(xP,xp),xS), inference(resolution, [status(thm)], [d55,d50])). % 178.91/23.22 cnf(d57, plain, aSubsetOf0(sdtpldt0(xP,xp),xS), inference(resolution, [status(thm)], [d37,d56])). % 178.91/23.22 cnf(d58, plain, ~aSet0(xS) | aElementOf0(X0,xS) | ~aElementOf0(X0,sdtpldt0(xP,xp)), inference(resolution, [status(thm)], [d57,c8])). % 178.91/23.22 cnf(d59, plain, ~aElementOf0(X0,sdtpldt0(xP,xp)) | aElementOf0(X0,xS), inference(resolution, [status(thm)], [c175,d58])). % 178.91/23.22 cnf(d60, plain, aElementOf0(X0,xS) | ~aElementOf0(X0,xP) | ~aElement0(X0), inference(resolution, [status(thm)], [d59,d47])). % 178.91/23.22 cnf(d61, plain, aElementOf0(sK14(X0,xP),xS) | ~aElement0(sK14(X0,xP)) | ~aSet0(X0) | ~aSet0(xP) | aSubsetOf0(xP,X0), inference(resolution, [status(thm)], [d60,c9])). % 178.91/23.22 cnf(d62, plain, ~aSet0(X0) | aElementOf0(sK14(X0,xP),xS) | ~aElement0(sK14(X0,xP)) | aSubsetOf0(xP,X0), inference(resolution, [status(thm)], [c430,d61])). % 178.91/23.22 cnf(d63, plain, ~aSet0(xS) | ~aElement0(sK14(xS,xP)) | aSubsetOf0(xP,xS) | ~aSet0(xS) | ~aSet0(xP) | aSubsetOf0(xP,xS), inference(resolution, [status(thm)], [d62,c10])). % 178.91/23.22 cnf(d64, plain, ~aSet0(xP) | ~aElement0(sK14(xS,xP)) | aSubsetOf0(xP,xS), inference(resolution, [status(thm)], [c175,d63])). % 178.91/23.22 cnf(d65, plain, ~aElement0(sK14(xS,xP)) | aSubsetOf0(xP,xS), inference(resolution, [status(thm)], [c430,d64])). % 178.91/23.22 cnf(d66, plain, aSubsetOf0(xP,xS) | ~aSet0(xP) | ~aSet0(xS) | aSubsetOf0(xP,xS), inference(resolution, [status(thm)], [d65,d44])). % 178.91/23.22 cnf(d67, plain, ~aSet0(xP) | aSubsetOf0(xP,xS), inference(resolution, [status(thm)], [c175,d66])). % 178.91/23.22 cnf(d68, plain, aSubsetOf0(xP,xS), inference(resolution, [status(thm)], [c430,d67])). % 178.91/23.22 cnf(d69, plain, ~aSet0(xS) | aElementOf0(X0,xS) | ~aElementOf0(X0,xP), inference(resolution, [status(thm)], [d68,c8])). % 178.91/23.22 cnf(d70, plain, aElementOf0(X0,xS) | ~aElementOf0(X0,xP), inference(resolution, [status(thm)], [c175,d69])). % 178.91/23.22 cnf(d71, plain, aElementOf0(sK14(X0,xP),xS) | ~aSet0(X0) | ~aSet0(xP) | aSubsetOf0(xP,X0), inference(resolution, [status(thm)], [d70,c9])). % 178.91/23.22 cnf(d72, plain, ~aSet0(X0) | aElementOf0(sK14(X0,xP),xS) | aSubsetOf0(xP,X0), inference(resolution, [status(thm)], [c430,d71])). % 178.91/23.22 cnf(d73, plain, ~aSet0(X0) | aSubsetOf0(xP,X0) | ~aSet0(xS) | aElement0(sK14(X0,xP)), inference(resolution, [status(thm)], [d72,c0])). % 178.91/23.22 cnf(d74, plain, ~aSet0(X0) | aElement0(sK14(X0,xP)) | aSubsetOf0(xP,X0), inference(resolution, [status(thm)], [c175,d73])). % 178.91/23.22 cnf(d75, plain, ~aSet0(sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | aSubsetOf0(xP,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))) | aSubsetOf0(xP,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))), inference(resolution, [status(thm)], [d74,d43])). % 178.91/23.22 cnf(d76, plain, aSubsetOf0(xP,sdtpldt0(xP,szmzizndt0(sdtlpdtrp0(xN,xn)))), inference(resolution, [status(thm)], [c465,d75])). % 178.91/23.22 cnf(d77, plain, aSubsetOf0(xP,sdtpldt0(xP,sdtlpdtrp0(xe,xn))) | ~aElementOf0(xn,szNzAzT0), inference(superposition, [status(thm)], [c375,d76])). % 178.91/23.22 cnf(d78, plain, ~aElementOf0(xn,szNzAzT0) | aSubsetOf0(xP,sdtpldt0(xP,xp)), inference(demodulation, [status(thm)], [d77,c450])). % 178.91/23.22 cnf(d79, plain, aSubsetOf0(xP,sdtpldt0(xP,xp)), inference(resolution, [status(thm)], [c449,d78])). % 178.91/23.22 cnf(d80, plain, xP = sdtpldt0(xP,xp), inference(resolution, [status(thm)], [d79,d38])). % 178.91/23.22 cnf(d81, plain, xP = sdtmndt0(xQ,xp), inference(demodulation, [status(thm)], [c436,c429])). % 178.91/23.22 cnf(d82, plain, sdtpldt0(xP,xp) = xQ | ~aSet0(xQ) | ~aElementOf0(xp,xQ), inference(superposition, [status(thm)], [d81,c46])). % 178.91/23.22 cnf(d83, plain, xP = xQ | ~aSet0(xQ) | ~aElementOf0(xp,xQ), inference(demodulation, [status(thm)], [d82,d80])). % 178.91/23.22 cnf(d84, plain, xP = xQ | ~aElementOf0(xp,xQ), inference(resolution, [status(thm)], [c412,d83])). % 178.91/23.22 cnf(d85, plain, xP = xQ, inference(resolution, [status(thm)], [c427,d84])). % 178.91/23.22 cnf(d86, plain, X0 != xp | ~aElementOf0(X0,xP), inference(demodulation, [status(thm)], [c434,c429])). % 178.91/23.22 cnf(d87, plain, X0 != xp | ~aElementOf0(X0,xQ), inference(demodulation, [status(thm)], [d86,d85])). % 178.91/23.22 cnf(d88, plain, ~aElementOf0(xp,xQ), inference(equality_resolution, [status(thm)], [d87])). % 178.91/23.22 cnf(d89, plain, $false, inference(resolution, [status(thm)], [c427,d88])). % 178.91/23.22 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------