%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM629+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 : n003.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:23 AM UTC 2026 % Result : Theorem 63.07s 37.77s % Output : CNFRefutation 63.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.05 % Problem : NUM629+3 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.10/5.46 % Computer : n003.cluster.edu % 0.10/5.46 % Model : x86_64 x86_64 % 0.10/5.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/5.46 % Memory : 8046.5625MB % 0.10/5.46 % OS : Linux 6.8.0-71-generic % 0.10/5.46 % CPULimit : 300 % 0.10/5.46 % WCLimit : 300 % 0.10/5.46 % DateTime : Sat Sep 26 03:32:29 UTC 2026 % 0.10/5.46 % CPUTime : % 0.10/5.46 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 63.07/37.77 % SZS status Theorem for theBenchmark.p % 63.07/37.77 % SZS output start CNFRefutation for theBenchmark.p % 63.07/37.77 fof(mDefSub, definition, ! [X0] : ((aSet0(X0) => ! [X1] : ((aSubsetOf0(X1,X0) <=> (aSet0(X1) & ! [X2] : ((aElementOf0(X2,X1) => aElementOf0(X2,X0))))))))). % 63.07/37.77 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))))))))))))))))). % 63.07/37.77 fof(m__3671, hypothesis, ! [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)))))))). % 63.07/37.77 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))))))))). % 63.07/37.77 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)))))). % 63.07/37.77 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))))). % 63.07/37.77 fof(m__5334, hypothesis, (! [X0] : ((aElementOf0(X0,xP) => aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn))))) & aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))))). % 63.07/37.77 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))))))). % 63.07/37.77 fof(m__, conjecture, (! [X0] : ((aElementOf0(X0,xP) => aElementOf0(X0,xD))) | (aSubsetOf0(xP,xD) | aElementOf0(xP,slbdtsldtrb0(xD,xk))))). % 63.07/37.77 fof(negated_conjecture, negated_conjecture, ~((! [X0] : ((aElementOf0(X0,xP) => aElementOf0(X0,xD))) | (aSubsetOf0(xP,xD) | aElementOf0(xP,slbdtsldtrb0(xD,xk))))), inference(negate_conjecture, [status(cth)], [m__])). % 63.07/37.77 cnf(c9, plain, ~aSet0(X0) | aSubsetOf0(X1,X0) | aElementOf0(sK10(X0,X1),X1) | ~aSet0(X1), inference(clausification, [status(esa)], [mDefSub])). % 63.07/37.77 cnf(c10, plain, ~aSet0(X0) | aSubsetOf0(X1,X0) | ~aElementOf0(sK10(X0,X1),X0) | ~aSet0(X1), inference(clausification, [status(esa)], [mDefSub])). % 63.07/37.77 cnf(c215, plain, ~aElementOf0(X0,szNzAzT0) | X1(X0) | ~aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0) | ~isCountable0(sdtlpdtrp0(xN,X0)), inference(clausification, [status(esa)], [m__3623])). % 63.07/37.77 cnf(c222, plain, ~X0(X1) | ~aElementOf0(X2,sdtlpdtrp0(xN,szszuzczcdt0(X1))) | aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1)))), inference(clausification, [status(esa)], [m__3623])). % 63.07/37.77 cnf(c229, plain, ~aElementOf0(X0,szNzAzT0) | aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0), inference(clausification, [status(esa)], [m__3671])). % 63.07/37.77 cnf(c230, plain, ~aElementOf0(X0,szNzAzT0) | isCountable0(sdtlpdtrp0(xN,X0)), inference(clausification, [status(esa)], [m__3671])). % 63.07/37.77 cnf(c357, plain, ~aElementOf0(X0,szNzAzT0) | szmzizndt0(sdtlpdtrp0(xN,X0)) = sdtlpdtrp0(xe,X0), inference(clausification, [status(esa)], [m__4660])). % 63.07/37.77 cnf(c412, plain, aSet0(xP), inference(clausification, [status(esa)], [m__5164])). % 63.07/37.77 cnf(c430, plain, sdtlpdtrp0(xe,xn) = xp, inference(clausification, [status(esa)], [m__5309])). % 63.07/37.77 cnf(c431, plain, aElementOf0(xn,szNzAzT0), inference(clausification, [status(esa)], [m__5309])). % 63.07/37.77 cnf(c434, plain, ~aElementOf0(X0,xP) | aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn))), inference(clausification, [status(esa)], [m__5334])). % 63.07/37.77 cnf(c441, plain, sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))) = xD, inference(clausification, [status(esa)], [m__5585])). % 63.07/37.77 cnf(c442, plain, aSet0(xD), inference(clausification, [status(esa)], [m__5585])). % 63.07/37.77 cnf(c446, plain, ~aSubsetOf0(xP,xD), inference(clausification, [status(esa)], [negated_conjecture])). % 63.07/37.77 cnf(d0, plain, szmzizndt0(sdtlpdtrp0(xN,xn)) = sdtlpdtrp0(xe,xn), inference(resolution, [status(thm)], [c431,c357])). % 63.07/37.77 cnf(d1, plain, szmzizndt0(sdtlpdtrp0(xN,xn)) = xp, inference(demodulation, [status(thm)], [d0,c430])). % 63.07/37.77 cnf(d2, plain, sdtmndt0(sdtlpdtrp0(xN,xn),xp) = xD, inference(demodulation, [status(thm)], [c441,d1])). % 63.07/37.77 cnf(d3, plain, ~aElementOf0(sK10(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),X1),sdtlpdtrp0(xN,szszuzczcdt0(X0))) | ~'Ts185'(X0) | ~aSet0(X1) | ~aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) | aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))), inference(resolution, [status(thm)], [c222,c10])). % 63.07/37.77 cnf(d4, plain, ~aSet0(X0) | ~aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) | aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~'Ts185'(xn) | ~aElementOf0(sK10(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),X0),xP), inference(resolution, [status(thm)], [d3,c434])). % 63.07/37.77 cnf(d5, plain, ~aSet0(X0) | ~aSet0(sdtmndt0(sdtlpdtrp0(xN,xn),xp)) | ~aElementOf0(sK10(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),X0),xP) | aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~'Ts185'(xn), inference(demodulation, [status(thm)], [d4,d1])). % 63.07/37.77 cnf(d6, plain, ~aSet0(X0) | ~aSet0(xD) | ~aElementOf0(sK10(sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))),X0),xP) | aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~'Ts185'(xn), inference(demodulation, [status(thm)], [d5,d2])). % 63.07/37.77 cnf(d7, plain, ~aSet0(X0) | ~aSet0(xD) | ~aElementOf0(sK10(sdtmndt0(sdtlpdtrp0(xN,xn),xp),X0),xP) | aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~'Ts185'(xn), inference(demodulation, [status(thm)], [d6,d1])). % 63.07/37.77 cnf(d8, plain, ~aSet0(X0) | ~aSet0(xD) | ~aElementOf0(sK10(xD,X0),xP) | aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))) | ~'Ts185'(xn), inference(demodulation, [status(thm)], [d7,d2])). % 63.07/37.77 cnf(d9, plain, ~aSet0(X0) | ~aSet0(xD) | ~aElementOf0(sK10(xD,X0),xP) | aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xn),xp)) | ~'Ts185'(xn), inference(demodulation, [status(thm)], [d8,d1])). % 63.07/37.77 cnf(d10, plain, ~aSet0(X0) | ~aSet0(xD) | ~aElementOf0(sK10(xD,X0),xP) | aSubsetOf0(X0,xD) | ~'Ts185'(xn), inference(demodulation, [status(thm)], [d9,d2])). % 63.07/37.77 cnf(d11, plain, ~aSet0(X0) | ~aElementOf0(sK10(xD,X0),xP) | aSubsetOf0(X0,xD) | ~'Ts185'(xn), inference(resolution, [status(thm)], [c442,d10])). % 63.07/37.77 cnf(d12, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X0,szNzAzT0) | ~isCountable0(sdtlpdtrp0(xN,X0)) | 'Ts185'(X0), inference(resolution, [status(thm)], [c229,c215])). % 63.07/37.77 cnf(d13, plain, ~aElementOf0(X0,szNzAzT0) | 'Ts185'(X0) | ~aElementOf0(X0,szNzAzT0), inference(resolution, [status(thm)], [d12,c230])). % 63.07/37.77 cnf(d14, plain, 'Ts185'(xn), inference(resolution, [status(thm)], [d13,c431])). % 63.07/37.77 cnf(d15, plain, ~aSet0(X0) | ~aElementOf0(sK10(xD,X0),xP) | aSubsetOf0(X0,xD), inference(resolution, [status(thm)], [d14,d11])). % 63.07/37.77 cnf(d16, plain, ~aSet0(xP) | aSubsetOf0(xP,xD) | ~aSet0(xP) | ~aSet0(xD) | aSubsetOf0(xP,xD), inference(resolution, [status(thm)], [d15,c9])). % 63.07/37.77 cnf(d17, plain, ~aSet0(xD) | aSubsetOf0(xP,xD), inference(resolution, [status(thm)], [c412,d16])). % 63.07/37.77 cnf(d18, plain, aSubsetOf0(xP,xD), inference(resolution, [status(thm)], [c442,d17])). % 63.07/37.77 cnf(d19, plain, $false, inference(resolution, [status(thm)], [c446,d18])). % 63.07/37.77 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------