%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM601+3 : 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 : n020.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:17 AM UTC 2026 % Result : Theorem 50.17s 12.80s % Output : CNFRefutation 50.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM601+3 : 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.09/5.78 % Computer : n020.cluster.edu % 0.09/5.78 % Model : x86_64 x86_64 % 0.09/5.78 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/5.78 % Memory : 8046.5625MB % 0.09/5.78 % OS : Linux 6.8.0-71-generic % 0.09/5.78 % CPULimit : 300 % 0.09/5.78 % WCLimit : 300 % 0.09/5.78 % DateTime : Sat Sep 26 03:25:25 UTC 2026 % 0.09/5.78 % CPUTime : % 0.09/5.78 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 50.17/12.80 % SZS status Theorem for theBenchmark.p % 50.17/12.80 % SZS output start CNFRefutation for theBenchmark.p % 50.17/12.80 fof(mZeroNum, axiom, aElementOf0(sz00,szNzAzT0)). % 50.17/12.80 fof(mZeroLess, axiom, ! [X0] : ((aElementOf0(X0,szNzAzT0) => sdtlseqdt0(sz00,X0)))). % 50.17/12.80 fof(m__3623, hypothesis, (aFunction0(xN) & (szDzozmdt0(xN) = szNzAzT0 & (sdtlpdtrp0(xN,sz00) = xS & ! [X0] : ((aElementOf0(X0,szNzAzT0) => ((((aSet0(sdtlpdtrp0(xN,X0)) & ! [X1] : ((aElementOf0(X1,sdtlpdtrp0(xN,X0)) => aElementOf0(X1,szNzAzT0)))) | aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)) & isCountable0(sdtlpdtrp0(xN,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)))))) & (aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0))) & (! [X1] : ((aElementOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0))) => aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))) & (aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) & isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(X0))))))))))))))))). % 50.17/12.80 fof(m__3754, hypothesis, ! [X0] : ! [X1] : (((aElementOf0(X0,szNzAzT0) & aElementOf0(X1,szNzAzT0)) => (sdtlseqdt0(X1,X0) => (! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X0)) => aElementOf0(X2,sdtlpdtrp0(xN,X1)))) & aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1))))))). % 50.17/12.80 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))))))))). % 50.17/12.80 fof(m__4982, hypothesis, ! [X0] : (((? [X1] : ((aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd))) & sdtlpdtrp0(xe,X1) = X0)) | aElementOf0(X0,xO)) => ? [X1] : ((aElementOf0(X1,szNzAzT0) & (sdtlpdtrp0(xd,X1) = szDzizrdt0(xd) & (aElementOf0(X1,sdtlbdtrb0(xd,szDzizrdt0(xd))) & sdtlpdtrp0(xe,X1) = X0))))))). % 50.17/12.80 fof(m__, conjecture, (! [X0] : ((aElementOf0(X0,xO) => aElementOf0(X0,xS))) | aSubsetOf0(xO,xS))). % 50.17/12.80 fof(negated_conjecture, negated_conjecture, ~((! [X0] : ((aElementOf0(X0,xO) => aElementOf0(X0,xS))) | aSubsetOf0(xO,xS))), inference(negate_conjecture, [status(cth)], [m__])). % 50.17/12.80 cnf(c47, plain, aElementOf0(sz00,szNzAzT0), inference(clausification, [status(esa)], [mZeroNum])). % 50.17/12.80 cnf(c54, plain, ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(sz00,X0), inference(clausification, [status(esa)], [mZeroLess])). % 50.17/12.80 cnf(c212, plain, sdtlpdtrp0(xN,sz00) = xS, inference(clausification, [status(esa)], [m__3623])). % 50.17/12.80 cnf(c232, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | ~sdtlseqdt0(X0,X1) | ~aElementOf0(X2,sdtlpdtrp0(xN,X1)) | aElementOf0(X2,sdtlpdtrp0(xN,X0)), inference(clausification, [status(esa)], [m__3754])). % 50.17/12.80 cnf(c356, plain, ~aElementOf0(X0,szNzAzT0) | aElementOf0(sdtlpdtrp0(xe,X0),sdtlpdtrp0(xN,X0)), inference(clausification, [status(esa)], [m__4660])). % 50.17/12.80 cnf(c389, plain, ~aElementOf0(X0,xO) | X1(X0), inference(clausification, [status(esa)], [m__4982])). % 50.17/12.80 cnf(c390, plain, ~X0(X1) | aElementOf0(sK275(X1),szNzAzT0), inference(clausification, [status(esa)], [m__4982])). % 50.17/12.80 cnf(c392, plain, ~X0(X1) | sdtlpdtrp0(xe,sK275(X1)) = X1, inference(clausification, [status(esa)], [m__4982])). % 50.17/12.80 cnf(c394, plain, aElementOf0(sK276,xO), inference(clausification, [status(esa)], [negated_conjecture])). % 50.17/12.80 cnf(c395, plain, ~aElementOf0(sK276,xS), inference(clausification, [status(esa)], [negated_conjecture])). % 50.17/12.80 cnf(d0, plain, ~'Ts272'(X0) | sdtlseqdt0(sz00,sK275(X0)), inference(resolution, [status(thm)], [c390,c54])). % 50.17/12.80 cnf(d1, plain, 'Ts272'(sK276), inference(resolution, [status(thm)], [c389,c394])). % 50.17/12.80 cnf(d2, plain, sdtlpdtrp0(xe,sK275(sK276)) = sK276, inference(resolution, [status(thm)], [c392,d1])). % 50.17/12.80 cnf(d3, plain, aElementOf0(sK276,sdtlpdtrp0(xN,sK275(sK276))) | ~aElementOf0(sK275(sK276),szNzAzT0), inference(superposition, [status(thm)], [d2,c356])). % 50.17/12.80 cnf(d4, plain, ~aElementOf0(sK275(sK276),szNzAzT0) | ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(sK275(sK276),szNzAzT0) | aElementOf0(sK276,sdtlpdtrp0(xN,X0)) | ~sdtlseqdt0(X0,sK275(sK276)), inference(resolution, [status(thm)], [d3,c232])). % 50.17/12.80 cnf(d5, plain, aElementOf0(sK276,xS) | ~aElementOf0(sz00,szNzAzT0) | ~aElementOf0(sK275(sK276),szNzAzT0) | ~sdtlseqdt0(sz00,sK275(sK276)), inference(superposition, [status(thm)], [c212,d4])). % 50.17/12.80 cnf(d6, plain, ~aElementOf0(sz00,szNzAzT0) | ~aElementOf0(sK275(sK276),szNzAzT0) | ~sdtlseqdt0(sz00,sK275(sK276)), inference(resolution, [status(thm)], [c395,d5])). % 50.17/12.80 cnf(d7, plain, ~aElementOf0(sK275(sK276),szNzAzT0) | ~sdtlseqdt0(sz00,sK275(sK276)), inference(resolution, [status(thm)], [c47,d6])). % 50.17/12.80 cnf(d8, plain, ~aElementOf0(sK275(sK276),szNzAzT0) | ~'Ts272'(sK276), inference(resolution, [status(thm)], [d7,d0])). % 50.17/12.80 cnf(d9, plain, ~aElementOf0(sK275(sK276),szNzAzT0), inference(resolution, [status(thm)], [d1,d8])). % 50.17/12.80 cnf(d10, plain, ~'Ts272'(sK276), inference(resolution, [status(thm)], [d9,c390])). % 50.17/12.80 cnf(d11, plain, $false, inference(resolution, [status(thm)], [d1,d10])). % 50.17/12.80 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------