%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM596+1 : 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 : n015.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:16 AM UTC 2026 % Result : Theorem 56.16s 21.67s % Output : CNFRefutation 56.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : NUM596+1 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.20/0.45 % Computer : n015.cluster.edu % 0.20/0.45 % Model : x86_64 x86_64 % 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.20/0.45 % Memory : 8046.5625MB % 0.20/0.45 % OS : Linux 6.8.0-71-generic % 0.20/0.45 % CPULimit : 300 % 0.20/0.45 % WCLimit : 300 % 0.20/0.45 % DateTime : Sat Sep 26 03:26:28 UTC 2026 % 0.20/0.46 % CPUTime : % 0.20/0.46 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 56.16/21.67 % SZS status Theorem for theBenchmark.p % 56.16/21.67 % SZS output start CNFRefutation for theBenchmark.p % 56.16/21.67 fof(mDefEmp, definition, ! [X0] : ((X0 = slcrc0 <=> (aSet0(X0) & ~? [X1] : aElementOf0(X1,X0))))). % 56.16/21.67 fof(mCountNFin_01, axiom, ! [X0] : (((aSet0(X0) & isCountable0(X0)) => X0 != slcrc0))). % 56.16/21.67 fof(mDefSub, definition, ! [X0] : ((aSet0(X0) => ! [X1] : ((aSubsetOf0(X1,X0) <=> (aSet0(X1) & ! [X2] : ((aElementOf0(X2,X1) => aElementOf0(X2,X0))))))))). % 56.16/21.67 fof(mSubFSet, axiom, ! [X0] : (((aSet0(X0) & isFinite0(X0)) => ! [X1] : ((aSubsetOf0(X1,X0) => isFinite0(X1)))))). % 56.16/21.67 fof(mNATSet, axiom, (aSet0(szNzAzT0) & isCountable0(szNzAzT0))). % 56.16/21.67 fof(mDefPtt, definition, ! [X0] : ! [X1] : (((aFunction0(X0) & aElement0(X1)) => ! [X2] : ((X2 = sdtlbdtrb0(X0,X1) <=> (aSet0(X2) & ! [X3] : ((aElementOf0(X3,X2) <=> (aElementOf0(X3,szDzozmdt0(X0)) & sdtlpdtrp0(X0,X3) = X1))))))))). % 56.16/21.67 fof(mImgRng, axiom, ! [X0] : ((aFunction0(X0) => ! [X1] : ((aElementOf0(X1,szDzozmdt0(X0)) => aElementOf0(sdtlpdtrp0(X0,X1),sdtlcdtrc0(X0,szDzozmdt0(X0)))))))). % 56.16/21.67 fof(mDirichlet, axiom, ! [X0] : ((aFunction0(X0) => ((isCountable0(szDzozmdt0(X0)) & isFinite0(sdtlcdtrc0(X0,szDzozmdt0(X0)))) => (aElement0(szDzizrdt0(X0)) & isCountable0(sdtlbdtrb0(X0,szDzizrdt0(X0)))))))). % 56.16/21.67 fof(m__3291, hypothesis, (aSet0(xT) & isFinite0(xT))). % 56.16/21.67 fof(m__4730, hypothesis, (aFunction0(xd) & (szDzozmdt0(xd) = szNzAzT0 & ! [X0] : ((aElementOf0(X0,szNzAzT0) => ! [X1] : (((aSet0(X1) & aElementOf0(X1,slbdtsldtrb0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),xk))) => sdtlpdtrp0(xd,X0) = sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1)))))))). % 56.16/21.67 fof(m__4758, hypothesis, aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT)). % 56.16/21.67 fof(m__, conjecture, aElementOf0(szDzizrdt0(xd),xT)). % 56.16/21.67 fof(negated_conjecture, negated_conjecture, ~aElementOf0(szDzizrdt0(xd),xT), inference(negate_conjecture, [status(cth)], [m__])). % 56.16/21.67 cnf(c1, plain, X0 != slcrc0 | aSet0(X0), inference(clausification, [status(esa)], [mDefEmp])). % 56.16/21.67 cnf(c2, plain, X0 != slcrc0 | ~aElementOf0(X1,X0), inference(clausification, [status(esa)], [mDefEmp])). % 56.16/21.67 cnf(c6, plain, ~aSet0(X0) | ~isCountable0(X0) | X0 != slcrc0, inference(clausification, [status(esa)], [mCountNFin_01])). % 56.16/21.67 cnf(c8, plain, ~aSet0(X0) | ~aSubsetOf0(X1,X0) | ~aElementOf0(X2,X1) | aElementOf0(X2,X0), inference(clausification, [status(esa)], [mDefSub])). % 56.16/21.67 cnf(c11, plain, ~aSet0(X0) | ~isFinite0(X0) | ~aSubsetOf0(X1,X0) | isFinite0(X1), inference(clausification, [status(esa)], [mSubFSet])). % 56.16/21.67 cnf(c53, plain, isCountable0(szNzAzT0), inference(clausification, [status(esa)], [mNATSet])). % 56.16/21.67 cnf(c134, plain, ~aFunction0(X0) | ~aElement0(X1) | X2 = sdtlbdtrb0(X0,X1) | ~X3(X0,X1,X2), inference(clausification, [status(esa)], [mDefPtt])). % 56.16/21.67 cnf(c140, plain, X0(X1,X2,X3) | ~aSet0(X3) | aElementOf0(sK134(X1,X2,X3),X3) | aElementOf0(sK134(X1,X2,X3),szDzozmdt0(X1)), inference(clausification, [status(esa)], [mDefPtt])). % 56.16/21.67 cnf(c141, plain, X0(X1,X2,X3) | ~aSet0(X3) | aElementOf0(sK134(X1,X2,X3),X3) | sdtlpdtrp0(X1,sK134(X1,X2,X3)) = X2, inference(clausification, [status(esa)], [mDefPtt])). % 56.16/21.67 cnf(c158, plain, ~aFunction0(X0) | ~aElementOf0(X1,szDzozmdt0(X0)) | aElementOf0(sdtlpdtrp0(X0,X1),sdtlcdtrc0(X0,szDzozmdt0(X0))), inference(clausification, [status(esa)], [mImgRng])). % 56.16/21.67 cnf(c170, plain, ~aFunction0(X0) | ~isCountable0(szDzozmdt0(X0)) | ~isFinite0(sdtlcdtrc0(X0,szDzozmdt0(X0))) | aElement0(szDzizrdt0(X0)), inference(clausification, [status(esa)], [mDirichlet])). % 56.16/21.67 cnf(c171, plain, ~aFunction0(X0) | ~isCountable0(szDzozmdt0(X0)) | ~isFinite0(sdtlcdtrc0(X0,szDzozmdt0(X0))) | isCountable0(sdtlbdtrb0(X0,szDzizrdt0(X0))), inference(clausification, [status(esa)], [mDirichlet])). % 56.16/21.67 cnf(c172, plain, aSet0(xT), inference(clausification, [status(esa)], [m__3291])). % 56.16/21.67 cnf(c173, plain, isFinite0(xT), inference(clausification, [status(esa)], [m__3291])). % 56.16/21.67 cnf(c214, plain, aFunction0(xd), inference(clausification, [status(esa)], [m__4730])). % 56.16/21.67 cnf(c215, plain, szDzozmdt0(xd) = szNzAzT0, inference(clausification, [status(esa)], [m__4730])). % 56.16/21.67 cnf(c217, plain, aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT), inference(clausification, [status(esa)], [m__4758])). % 56.16/21.67 cnf(c218, plain, ~aElementOf0(szDzizrdt0(xd),xT), inference(clausification, [status(esa)], [negated_conjecture])). % 56.16/21.67 cnf(d0, plain, ~isFinite0(sdtlcdtrc0(xd,szNzAzT0)) | ~isCountable0(szDzozmdt0(xd)) | isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) | ~aFunction0(xd), inference(superposition, [status(thm)], [c215,c171])). % 56.16/21.67 cnf(d1, plain, ~isFinite0(sdtlcdtrc0(xd,szNzAzT0)) | ~isCountable0(szNzAzT0) | isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) | ~aFunction0(xd), inference(demodulation, [status(thm)], [d0,c215])). % 56.16/21.67 cnf(d2, plain, ~isFinite0(sdtlcdtrc0(xd,szNzAzT0)) | isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) | ~aFunction0(xd), inference(resolution, [status(thm)], [c53,d1])). % 56.16/21.67 cnf(d3, plain, ~isFinite0(sdtlcdtrc0(xd,szNzAzT0)) | isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))), inference(resolution, [status(thm)], [c214,d2])). % 56.16/21.67 cnf(d4, plain, aSubsetOf0(sdtlcdtrc0(xd,szNzAzT0),xT), inference(demodulation, [status(thm)], [c217,c215])). % 56.16/21.67 cnf(d5, plain, ~aSet0(xT) | isFinite0(sdtlcdtrc0(xd,szNzAzT0)) | ~isFinite0(xT), inference(resolution, [status(thm)], [c11,d4])). % 56.16/21.67 cnf(d6, plain, isFinite0(sdtlcdtrc0(xd,szNzAzT0)) | ~isFinite0(xT), inference(resolution, [status(thm)], [c172,d5])). % 56.16/21.67 cnf(d7, plain, isFinite0(sdtlcdtrc0(xd,szNzAzT0)), inference(resolution, [status(thm)], [c173,d6])). % 56.16/21.67 cnf(d8, plain, isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))), inference(resolution, [status(thm)], [d7,d3])). % 56.16/21.67 cnf(d9, plain, isCountable0(X0) | ~aElement0(szDzizrdt0(xd)) | ~aFunction0(xd) | ~'Ts129'(xd,szDzizrdt0(xd),X0), inference(superposition, [status(thm)], [c134,d8])). % 56.16/21.67 cnf(d10, plain, ~aElement0(szDzizrdt0(xd)) | isCountable0(X0) | ~'Ts129'(xd,szDzizrdt0(xd),X0), inference(resolution, [status(thm)], [c214,d9])). % 56.16/21.67 cnf(d11, plain, ~isFinite0(sdtlcdtrc0(xd,szNzAzT0)) | aElement0(szDzizrdt0(xd)) | ~isCountable0(szDzozmdt0(xd)) | ~aFunction0(xd), inference(superposition, [status(thm)], [c215,c170])). % 56.16/21.67 cnf(d12, plain, aElement0(szDzizrdt0(xd)) | ~isFinite0(sdtlcdtrc0(xd,szNzAzT0)) | ~isCountable0(szNzAzT0) | ~aFunction0(xd), inference(demodulation, [status(thm)], [d11,c215])). % 56.16/21.67 cnf(d13, plain, aElement0(szDzizrdt0(xd)) | ~isFinite0(sdtlcdtrc0(xd,szNzAzT0)) | ~aFunction0(xd), inference(resolution, [status(thm)], [c53,d12])). % 56.16/21.67 cnf(d14, plain, aElement0(szDzizrdt0(xd)) | ~isFinite0(sdtlcdtrc0(xd,szNzAzT0)), inference(resolution, [status(thm)], [c214,d13])). % 56.16/21.67 cnf(d15, plain, aElement0(szDzizrdt0(xd)), inference(resolution, [status(thm)], [d7,d14])). % 56.16/21.67 cnf(d16, plain, isCountable0(X0) | ~'Ts129'(xd,szDzizrdt0(xd),X0), inference(resolution, [status(thm)], [d15,d10])). % 56.16/21.67 cnf(d17, plain, ~aElementOf0(X0,slcrc0), inference(equality_resolution, [status(thm)], [c2])). % 56.16/21.67 cnf(d18, plain, aElementOf0(sK134(xd,X0,X1),szNzAzT0) | ~aSet0(X1) | aElementOf0(sK134(xd,X0,X1),X1) | 'Ts129'(xd,X0,X1), inference(superposition, [status(thm)], [c215,c140])). % 56.16/21.67 cnf(d19, plain, ~aSet0(xT) | aElementOf0(X0,xT) | ~aElementOf0(X0,sdtlcdtrc0(xd,szNzAzT0)), inference(resolution, [status(thm)], [c8,d4])). % 56.16/21.67 cnf(d20, plain, ~aElementOf0(X0,sdtlcdtrc0(xd,szNzAzT0)) | aElementOf0(X0,xT), inference(resolution, [status(thm)], [c172,d19])). % 56.16/21.67 cnf(d21, plain, aElementOf0(sdtlpdtrp0(xd,X0),sdtlcdtrc0(xd,szNzAzT0)) | ~aElementOf0(X0,szDzozmdt0(xd)) | ~aFunction0(xd), inference(superposition, [status(thm)], [c215,c158])). % 56.16/21.67 cnf(d22, plain, ~aElementOf0(X0,szNzAzT0) | aElementOf0(sdtlpdtrp0(xd,X0),sdtlcdtrc0(xd,szNzAzT0)) | ~aFunction0(xd), inference(demodulation, [status(thm)], [d21,c215])). % 56.16/21.67 cnf(d23, plain, ~aElementOf0(X0,szNzAzT0) | aElementOf0(sdtlpdtrp0(xd,X0),sdtlcdtrc0(xd,szNzAzT0)), inference(resolution, [status(thm)], [c214,d22])). % 56.16/21.67 cnf(d24, plain, ~aElementOf0(X0,szNzAzT0) | aElementOf0(sdtlpdtrp0(xd,X0),xT), inference(resolution, [status(thm)], [d23,d20])). % 56.16/21.67 cnf(d25, plain, aElementOf0(X0,xT) | ~aElementOf0(sK134(xd,X0,X1),szNzAzT0) | ~aSet0(X1) | aElementOf0(sK134(xd,X0,X1),X1) | 'Ts129'(xd,X0,X1), inference(superposition, [status(thm)], [c141,d24])). % 56.16/21.67 cnf(d26, plain, ~aSet0(X0) | aElementOf0(X1,xT) | aElementOf0(sK134(xd,X1,X0),X0) | 'Ts129'(xd,X1,X0) | ~aSet0(X0) | aElementOf0(sK134(xd,X1,X0),X0) | 'Ts129'(xd,X1,X0), inference(resolution, [status(thm)], [d25,d18])). % 56.16/21.67 cnf(d27, plain, ~aSet0(slcrc0) | aElementOf0(X0,xT) | 'Ts129'(xd,X0,slcrc0), inference(resolution, [status(thm)], [d26,d17])). % 56.16/21.67 cnf(d28, plain, aSet0(slcrc0), inference(equality_resolution, [status(thm)], [c1])). % 56.16/21.67 cnf(d29, plain, aElementOf0(X0,xT) | 'Ts129'(xd,X0,slcrc0), inference(resolution, [status(thm)], [d28,d27])). % 56.16/21.67 cnf(d30, plain, aElementOf0(szDzizrdt0(xd),xT) | isCountable0(slcrc0), inference(resolution, [status(thm)], [d29,d16])). % 56.16/21.67 cnf(d31, plain, isCountable0(slcrc0), inference(resolution, [status(thm)], [c218,d30])). % 56.16/21.67 cnf(d32, plain, ~aSet0(slcrc0) | ~isCountable0(slcrc0), inference(equality_resolution, [status(thm)], [c6])). % 56.16/21.67 cnf(d33, plain, ~isCountable0(slcrc0), inference(resolution, [status(thm)], [d28,d32])). % 56.16/21.67 cnf(d34, plain, $false, inference(resolution, [status(thm)], [d33,d31])). % 56.16/21.67 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------