%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM578+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 : n018.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:13 AM UTC 2026 % Result : Theorem 19.68s 8.61s % Output : CNFRefutation 19.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM578+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.08/5.38 % Computer : n018.cluster.edu % 0.08/5.38 % Model : x86_64 x86_64 % 0.08/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/5.38 % Memory : 8046.5625MB % 0.08/5.38 % OS : Linux 6.8.0-71-generic % 0.08/5.38 % CPULimit : 300 % 0.08/5.38 % WCLimit : 300 % 0.08/5.38 % DateTime : Sat Sep 26 03:20:26 UTC 2026 % 0.08/5.38 % CPUTime : % 0.08/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 19.68/8.61 % SZS status Theorem for theBenchmark.p % 19.68/8.61 % SZS output start CNFRefutation for theBenchmark.p % 19.68/8.61 fof(mLessASymm, axiom, ! [X0] : ! [X1] : (((aElementOf0(X0,szNzAzT0) & aElementOf0(X1,szNzAzT0)) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X0)) => X0 = X1)))). % 19.68/8.61 fof(mLessTotal, axiom, ! [X0] : ! [X1] : (((aElementOf0(X0,szNzAzT0) & aElementOf0(X1,szNzAzT0)) => (sdtlseqdt0(X0,X1) | sdtlseqdt0(szszuzczcdt0(X1),X0))))). % 19.68/8.61 fof(m__3856, hypothesis, (aElementOf0(xi,szNzAzT0) & aElementOf0(xj,szNzAzT0))). % 19.68/8.61 fof(m__, conjecture, (! [X0] : ! [X1] : (((aElementOf0(X0,szNzAzT0) & aElementOf0(X1,szNzAzT0)) => (sdtlseqdt0(szszuzczcdt0(X0),X1) => (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) & (! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X0)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2))) & (aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) & (! [X2] : ((aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) <=> (aElement0(X2) & (aElementOf0(X2,sdtlpdtrp0(xN,X0)) & X2 != szmzizndt0(sdtlpdtrp0(xN,X0)))))) & (! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X1)) => aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))) & (aSubsetOf0(sdtlpdtrp0(xN,X1),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) & ~(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1)) & ! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X1)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X2)))) => ((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X0)) & ! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X0)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X2)))) | szmzizndt0(sdtlpdtrp0(xN,X1)) = szmzizndt0(sdtlpdtrp0(xN,X0)))))))))))))) => (xi != xj => ~((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) & (! [X0] : ((aElementOf0(X0,sdtlpdtrp0(xN,xi)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0))) & (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj)) & (! [X0] : ((aElementOf0(X0,sdtlpdtrp0(xN,xj)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0))) & szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj)))))))))). % 19.68/8.61 fof(negated_conjecture, negated_conjecture, ~((! [X0] : ! [X1] : (((aElementOf0(X0,szNzAzT0) & aElementOf0(X1,szNzAzT0)) => (sdtlseqdt0(szszuzczcdt0(X0),X1) => (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) & (! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X0)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2))) & (aSet0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) & (! [X2] : ((aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) <=> (aElement0(X2) & (aElementOf0(X2,sdtlpdtrp0(xN,X0)) & X2 != szmzizndt0(sdtlpdtrp0(xN,X0)))))) & (! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X1)) => aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))) & (aSubsetOf0(sdtlpdtrp0(xN,X1),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) & ~(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X1)) & ! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X1)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X2)))) => ((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X1)),sdtlpdtrp0(xN,X0)) & ! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X0)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X1)),X2)))) | szmzizndt0(sdtlpdtrp0(xN,X1)) = szmzizndt0(sdtlpdtrp0(xN,X0)))))))))))))) => (xi != xj => ~((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi)) & (! [X0] : ((aElementOf0(X0,sdtlpdtrp0(xN,xi)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0))) & (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xj)) & (! [X0] : ((aElementOf0(X0,sdtlpdtrp0(xN,xj)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),X0))) & szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj)))))))))), inference(negate_conjecture, [status(cth)], [m__])). % 19.68/8.61 cnf(c67, plain, ~sdtlseqdt0(X0,X1) | ~aElementOf0(X1,szNzAzT0) | ~sdtlseqdt0(X1,X0) | X1 = X0 | ~aElementOf0(X0,szNzAzT0), inference(clausification, [status(esa)], [mLessASymm])). % 19.68/8.61 cnf(c69, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | sdtlseqdt0(X0,X1) | sdtlseqdt0(szszuzczcdt0(X1),X0), inference(clausification, [status(esa)], [mLessTotal])). % 19.68/8.61 cnf(c250, plain, aElementOf0(xi,szNzAzT0), inference(clausification, [status(esa)], [m__3856])). % 19.68/8.61 cnf(c251, plain, aElementOf0(xj,szNzAzT0), inference(clausification, [status(esa)], [m__3856])). % 19.68/8.61 cnf(c253, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | ~sdtlseqdt0(szszuzczcdt0(X0),X1) | X2(X0,X1), inference(clausification, [status(esa)], [negated_conjecture])). % 19.68/8.61 cnf(c254, plain, xi != xj, inference(clausification, [status(esa)], [negated_conjecture])). % 19.68/8.61 cnf(c259, plain, szmzizndt0(sdtlpdtrp0(xN,xi)) = szmzizndt0(sdtlpdtrp0(xN,xj)), inference(clausification, [status(esa)], [negated_conjecture])). % 19.68/8.61 cnf(c273, plain, ~X0(X1,X2) | szmzizndt0(sdtlpdtrp0(xN,X2)) != szmzizndt0(sdtlpdtrp0(xN,X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 19.68/8.61 cnf(d0, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | sdtlseqdt0(X0,X1) | ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | 'Ts199'(X1,X0), inference(resolution, [status(thm)], [c69,c253])). % 19.68/8.61 cnf(d1, plain, ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(xi,X0) | 'Ts199'(X0,xi), inference(resolution, [status(thm)], [c250,d0])). % 19.68/8.61 cnf(d2, plain, sdtlseqdt0(xi,xj) | 'Ts199'(xj,xi), inference(resolution, [status(thm)], [d1,c251])). % 19.68/8.61 cnf(d3, plain, szmzizndt0(sdtlpdtrp0(xN,X0)) != szmzizndt0(sdtlpdtrp0(xN,xi)) | ~'Ts199'(xj,X0), inference(superposition, [status(thm)], [c259,c273])). % 19.68/8.61 cnf(d4, plain, ~'Ts199'(xj,xi), inference(equality_resolution, [status(thm)], [d3])). % 19.68/8.61 cnf(d5, plain, sdtlseqdt0(xi,xj), inference(resolution, [status(thm)], [d4,d2])). % 19.68/8.61 cnf(d6, plain, xj = xi | ~aElementOf0(xj,szNzAzT0) | ~aElementOf0(xi,szNzAzT0) | ~sdtlseqdt0(xj,xi), inference(resolution, [status(thm)], [d5,c67])). % 19.68/8.61 cnf(d7, plain, xj = xi | ~aElementOf0(xj,szNzAzT0) | ~sdtlseqdt0(xj,xi), inference(resolution, [status(thm)], [c250,d6])). % 19.68/8.61 cnf(d8, plain, xj = xi | ~sdtlseqdt0(xj,xi), inference(resolution, [status(thm)], [c251,d7])). % 19.68/8.61 cnf(d9, plain, ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(xj,X0) | 'Ts199'(X0,xj), inference(resolution, [status(thm)], [c251,d0])). % 19.68/8.61 cnf(d10, plain, sdtlseqdt0(xj,xi) | 'Ts199'(xi,xj), inference(resolution, [status(thm)], [d9,c250])). % 19.68/8.61 cnf(d11, plain, szmzizndt0(sdtlpdtrp0(xN,xi)) != szmzizndt0(sdtlpdtrp0(xN,X0)) | ~'Ts199'(X0,xj), inference(superposition, [status(thm)], [c259,c273])). % 19.68/8.61 cnf(d12, plain, ~'Ts199'(xi,xj), inference(equality_resolution, [status(thm)], [d11])). % 19.68/8.61 cnf(d13, plain, sdtlseqdt0(xj,xi), inference(resolution, [status(thm)], [d12,d10])). % 19.68/8.61 cnf(d14, plain, xj = xi, inference(resolution, [status(thm)], [d13,d8])). % 19.68/8.61 cnf(d15, plain, xi != xi, inference(demodulation, [status(thm)], [c254,d14])). % 19.68/8.61 cnf(d16, plain, $false, inference(equality_resolution, [status(thm)], [d15])). % 19.68/8.61 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------