%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM592+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 : n005.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:15 AM UTC 2026 % Result : Theorem 41.40s 5.71s % Output : CNFRefutation 41.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM592+3 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.09/0.35 % Computer : n005.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 26 03:22:04 UTC 2026 % 0.09/0.36 % CPUTime : % 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 41.40/5.71 % SZS status Theorem for theBenchmark.p % 41.40/5.71 % SZS output start CNFRefutation for theBenchmark.p % 41.40/5.71 fof(m__4448_02, hypothesis, (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) & (! [X0] : ((aElementOf0(X0,sdtlpdtrp0(xN,xi)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0))) & (aSet0(xY) & (! [X0] : ((aElementOf0(X0,xY) <=> (aElement0(X0) & (aElementOf0(X0,sdtlpdtrp0(xN,xi)) & X0 != szmzizndt0(sdtlpdtrp0(xN,xi)))))) & (xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))) & xd = sdtlpdtrp0(xC,xi))))))). % 41.40/5.71 fof(m__4545, hypothesis, (aElementOf0(xu,xT) & (aSet0(xX) & (! [X0] : ((aElementOf0(X0,xX) => aElementOf0(X0,xY))) & (aSubsetOf0(xX,xY) & (isCountable0(xX) & ! [X0] : (((aSet0(X0) & (((! [X1] : ((aElementOf0(X1,X0) => aElementOf0(X1,xX))) | aSubsetOf0(X0,xX)) & sbrdtbr0(X0) = xk) | aElementOf0(X0,slbdtsldtrb0(xX,xk)))) => sdtlpdtrp0(xd,X0) = xu)))))))). % 41.40/5.71 fof(m__, conjecture, ? [X0] : ((aElementOf0(X0,xT) & ? [X1] : ((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) & ! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,xi)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2)))) => ((aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) & ! [X2] : ((aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) <=> (aElement0(X2) & (aElementOf0(X2,sdtlpdtrp0(xN,xi)) & X2 != szmzizndt0(sdtlpdtrp0(xN,xi))))))) => ((aSet0(X1) & ! [X2] : ((aElementOf0(X2,X1) => aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))) | aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))) & (isCountable0(X1) & ! [X2] : (((aSet0(X2) & (! [X3] : ((aElementOf0(X3,X2) => aElementOf0(X3,X1))) & (aSubsetOf0(X2,X1) & (sbrdtbr0(X2) = xk & aElementOf0(X2,slbdtsldtrb0(X1,xk)))))) => sdtlpdtrp0(sdtlpdtrp0(xC,xi),X2) = X0)))))))). % 41.40/5.71 fof(negated_conjecture, negated_conjecture, ~? [X0] : ((aElementOf0(X0,xT) & ? [X1] : ((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) & ! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,xi)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X2)))) => ((aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) & ! [X2] : ((aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) <=> (aElement0(X2) & (aElementOf0(X2,sdtlpdtrp0(xN,xi)) & X2 != szmzizndt0(sdtlpdtrp0(xN,xi))))))) => ((aSet0(X1) & ! [X2] : ((aElementOf0(X2,X1) => aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))) | aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))) & (isCountable0(X1) & ! [X2] : (((aSet0(X2) & (! [X3] : ((aElementOf0(X3,X2) => aElementOf0(X3,X1))) & (aSubsetOf0(X2,X1) & (sbrdtbr0(X2) = xk & aElementOf0(X2,slbdtsldtrb0(X1,xk)))))) => sdtlpdtrp0(sdtlpdtrp0(xC,xi),X2) = X0))))))), inference(negate_conjecture, [status(cth)], [m__])). % 41.40/5.71 cnf(c357, plain, xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))), inference(clausification, [status(esa)], [m__4448_02])). % 41.40/5.71 cnf(c358, plain, xd = sdtlpdtrp0(xC,xi), inference(clausification, [status(esa)], [m__4448_02])). % 41.40/5.71 cnf(c374, plain, aElementOf0(xu,xT), inference(clausification, [status(esa)], [m__4545])). % 41.40/5.71 cnf(c377, plain, aSubsetOf0(xX,xY), inference(clausification, [status(esa)], [m__4545])). % 41.40/5.71 cnf(c378, plain, isCountable0(xX), inference(clausification, [status(esa)], [m__4545])). % 41.40/5.71 cnf(c382, plain, ~aSet0(X0) | ~aElementOf0(X0,slbdtsldtrb0(xX,xk)) | sdtlpdtrp0(xd,X0) = xu, inference(clausification, [status(esa)], [m__4545])). % 41.40/5.71 cnf(c383, plain, ~aElementOf0(X0,xT) | ~X1(X2) | ~isCountable0(X2) | ~X3(X0,X2), inference(clausification, [status(esa)], [negated_conjecture])). % 41.40/5.71 cnf(c384, plain, X0(X1,X2) | aSet0(sK264(X1,X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 41.40/5.71 cnf(c388, plain, X0(X1,X2) | aElementOf0(sK264(X1,X2),slbdtsldtrb0(X2,xk)), inference(clausification, [status(esa)], [negated_conjecture])). % 41.40/5.71 cnf(c389, plain, X0(X1,X2) | sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK264(X1,X2)) != X1, inference(clausification, [status(esa)], [negated_conjecture])). % 41.40/5.71 cnf(c399, plain, X0(X1) | ~aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))), inference(clausification, [status(esa)], [negated_conjecture])). % 41.40/5.71 cnf(d0, plain, sdtlpdtrp0(xd,sK264(X0,X1)) != X0 | 'Ts260'(X0,X1), inference(demodulation, [status(thm)], [c389,c358])). % 41.40/5.71 cnf(d1, plain, sdtlpdtrp0(xd,sK264(X0,xX)) = xu | ~aSet0(sK264(X0,xX)) | 'Ts260'(X0,xX), inference(resolution, [status(thm)], [c382,c388])). % 41.40/5.71 cnf(d2, plain, sdtlpdtrp0(xd,sK264(X0,xX)) = xu | 'Ts260'(X0,xX) | 'Ts260'(X0,xX), inference(resolution, [status(thm)], [d1,c384])). % 41.40/5.71 cnf(d3, plain, sdtlpdtrp0(xd,sK264(X0,xX)) = xu | ~aElementOf0(X0,xT) | ~isCountable0(xX) | ~'Ts261'(xX), inference(resolution, [status(thm)], [d2,c383])). % 41.40/5.71 cnf(d4, plain, sdtlpdtrp0(xd,sK264(X0,xX)) = xu | ~aElementOf0(X0,xT) | ~'Ts261'(xX), inference(resolution, [status(thm)], [c378,d3])). % 41.40/5.71 cnf(d5, plain, ~aSubsetOf0(X0,xY) | 'Ts261'(X0), inference(demodulation, [status(thm)], [c399,c357])). % 41.40/5.71 cnf(d6, plain, 'Ts261'(xX), inference(resolution, [status(thm)], [c377,d5])). % 41.40/5.71 cnf(d7, plain, sdtlpdtrp0(xd,sK264(X0,xX)) = xu | ~aElementOf0(X0,xT), inference(resolution, [status(thm)], [d6,d4])). % 41.40/5.71 cnf(d8, plain, sdtlpdtrp0(xd,sK264(xu,xX)) = xu, inference(resolution, [status(thm)], [d7,c374])). % 41.40/5.71 cnf(d9, plain, xu != xu | 'Ts260'(xu,xX), inference(superposition, [status(thm)], [d8,d0])). % 41.40/5.71 cnf(d10, plain, 'Ts260'(xu,xX), inference(equality_resolution, [status(thm)], [d9])). % 41.40/5.71 cnf(d11, plain, ~aElementOf0(xu,xT) | ~isCountable0(xX) | ~'Ts261'(xX), inference(resolution, [status(thm)], [d10,c383])). % 41.40/5.71 cnf(d12, plain, ~aElementOf0(xu,xT) | ~'Ts261'(xX), inference(resolution, [status(thm)], [c378,d11])). % 41.40/5.71 cnf(d13, plain, ~'Ts261'(xX), inference(resolution, [status(thm)], [c374,d12])). % 41.40/5.71 cnf(d14, plain, $false, inference(resolution, [status(thm)], [d6,d13])). % 41.40/5.71 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------