%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM571+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 : n016.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:11 AM UTC 2026 % Result : Theorem 19.02s 13.03s % Output : CNFRefutation 19.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM571+3 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.08/10.58 % Computer : n016.cluster.edu % 0.08/10.58 % Model : x86_64 x86_64 % 0.08/10.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/10.58 % Memory : 8046.5625MB % 0.08/10.58 % OS : Linux 6.8.0-71-generic % 0.08/10.58 % CPULimit : 300 % 0.08/10.58 % WCLimit : 300 % 0.08/10.58 % DateTime : Sat Sep 26 03:21:26 UTC 2026 % 0.08/10.58 % CPUTime : % 0.08/10.58 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.02/13.03 % SZS status Theorem for theBenchmark.p % 19.02/13.03 % SZS output start CNFRefutation for theBenchmark.p % 19.02/13.03 fof(m__3435, hypothesis, (aSet0(xS) & (! [X0] : ((aElementOf0(X0,xS) => aElementOf0(X0,szNzAzT0))) & (aSubsetOf0(xS,szNzAzT0) & isCountable0(xS))))). % 19.02/13.03 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))))))))))))))))). % 19.02/13.03 fof(m__3702_02, hypothesis, (xi != sz00 => (? [X0] : ((aElementOf0(X0,szNzAzT0) & szszuzczcdt0(X0) = xi)) & (aSet0(sdtlpdtrp0(xN,xi)) & (! [X0] : ((aElementOf0(X0,sdtlpdtrp0(xN,xi)) => aElementOf0(X0,szNzAzT0))) & (aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) & isCountable0(sdtlpdtrp0(xN,xi)))))))). % 19.02/13.03 fof(m__, conjecture, (((aSet0(sdtlpdtrp0(xN,xi)) & ! [X0] : ((aElementOf0(X0,sdtlpdtrp0(xN,xi)) => aElementOf0(X0,szNzAzT0)))) | aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)) & isCountable0(sdtlpdtrp0(xN,xi)))). % 19.02/13.03 fof(negated_conjecture, negated_conjecture, ~((((aSet0(sdtlpdtrp0(xN,xi)) & ! [X0] : ((aElementOf0(X0,sdtlpdtrp0(xN,xi)) => aElementOf0(X0,szNzAzT0)))) | aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)) & isCountable0(sdtlpdtrp0(xN,xi)))), inference(negate_conjecture, [status(cth)], [m__])). % 19.02/13.03 cnf(c177, plain, aSubsetOf0(xS,szNzAzT0), inference(clausification, [status(esa)], [m__3435])). % 19.02/13.03 cnf(c178, plain, isCountable0(xS), inference(clausification, [status(esa)], [m__3435])). % 19.02/13.03 cnf(c229, plain, sdtlpdtrp0(xN,sz00) = xS, inference(clausification, [status(esa)], [m__3623])). % 19.02/13.03 cnf(c249, plain, xi = sz00 | X0, inference(clausification, [status(esa)], [m__3702_02])). % 19.02/13.03 cnf(c254, plain, ~X0 | aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0), inference(clausification, [status(esa)], [m__3702_02])). % 19.02/13.03 cnf(c255, plain, ~X0 | isCountable0(sdtlpdtrp0(xN,xi)), inference(clausification, [status(esa)], [m__3702_02])). % 19.02/13.03 cnf(c258, plain, ~aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0) | ~isCountable0(sdtlpdtrp0(xN,xi)), inference(clausification, [status(esa)], [negated_conjecture])). % 19.02/13.03 cnf(d0, plain, ~'Ts196' | ~isCountable0(sdtlpdtrp0(xN,xi)), inference(resolution, [status(thm)], [c254,c258])). % 19.02/13.03 cnf(d1, plain, ~'Ts196' | ~'Ts196', inference(resolution, [status(thm)], [d0,c255])). % 19.02/13.03 cnf(d2, plain, xi = sz00, inference(resolution, [status(thm)], [d1,c249])). % 19.02/13.03 cnf(d3, plain, sdtlpdtrp0(xN,xi) = xS, inference(demodulation, [status(thm)], [c229,d2])). % 19.02/13.03 cnf(d4, plain, ~isCountable0(xS) | ~aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0), inference(demodulation, [status(thm)], [c258,d3])). % 19.02/13.03 cnf(d5, plain, ~isCountable0(xS) | ~aSubsetOf0(xS,szNzAzT0), inference(demodulation, [status(thm)], [d4,d3])). % 19.02/13.03 cnf(d6, plain, ~aSubsetOf0(xS,szNzAzT0), inference(resolution, [status(thm)], [c178,d5])). % 19.02/13.03 cnf(d7, plain, $false, inference(resolution, [status(thm)], [c177,d6])). % 19.02/13.03 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------