%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM585+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:14 AM UTC 2026 % Result : Theorem 37.12s 6.06s % Output : CNFRefutation 37.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM585+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.11/0.37 % Computer : n016.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Sat Sep 26 03:25:45 UTC 2026 % 0.11/0.37 % CPUTime : % 0.11/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 37.12/6.06 % SZS status Theorem for theBenchmark.p % 37.12/6.06 % SZS output start CNFRefutation for theBenchmark.p % 37.12/6.06 fof(mImgRng, axiom, ! [X0] : ((aFunction0(X0) => ! [X1] : ((aElementOf0(X1,szDzozmdt0(X0)) => aElementOf0(sdtlpdtrp0(X0,X1),sdtlcdtrc0(X0,szDzozmdt0(X0)))))))). % 37.12/6.06 fof(m__3453, hypothesis, (aFunction0(xc) & (! [X0] : (((aElementOf0(X0,szDzozmdt0(xc)) => (aSet0(X0) & (! [X1] : ((aElementOf0(X1,X0) => aElementOf0(X1,xS))) & (aSubsetOf0(X0,xS) & sbrdtbr0(X0) = xK)))) & ((((aSet0(X0) & ! [X1] : ((aElementOf0(X1,X0) => aElementOf0(X1,xS)))) | aSubsetOf0(X0,xS)) & sbrdtbr0(X0) = xK) => aElementOf0(X0,szDzozmdt0(xc))))) & (szDzozmdt0(xc) = slbdtsldtrb0(xS,xK) & (aSet0(sdtlcdtrc0(xc,szDzozmdt0(xc))) & (! [X0] : ((aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc))) <=> ? [X1] : ((aElementOf0(X1,szDzozmdt0(xc)) & sdtlpdtrp0(xc,X1) = X0)))) & (! [X0] : ((aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc))) => aElementOf0(X0,xT))) & aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT)))))))). % 37.12/6.06 fof(m__3965, hypothesis, ! [X0] : ((aElementOf0(X0,szNzAzT0) => ! [X1] : (((aSet0(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,X1) => aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))) | aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))) & sbrdtbr0(X1) = xk) | aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)))))) => (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) & (! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X0)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2))) & (aSet0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) & (! [X2] : ((aElementOf0(X2,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) <=> (aElement0(X2) & (aElementOf0(X2,X1) | X2 = szmzizndt0(sdtlpdtrp0(xN,X0)))))) & (! [X2] : ((aElementOf0(X2,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) => aElementOf0(X2,xS))) & (aSubsetOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),xS) & (sbrdtbr0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) = xK & aElementOf0(sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))),slbdtsldtrb0(xS,xK)))))))))))))). % 37.12/6.06 fof(m__4151, hypothesis, (aFunction0(xC) & (szDzozmdt0(xC) = szNzAzT0 & ! [X0] : ((aElementOf0(X0,szNzAzT0) => (aFunction0(sdtlpdtrp0(xC,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)))))) & (! [X1] : (((aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0))) => (aSet0(X1) & (! [X2] : ((aElementOf0(X2,X1) => aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))) & (aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))) & sbrdtbr0(X1) = xk)))) & ((((aSet0(X1) & ! [X2] : ((aElementOf0(X2,X1) => aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))))) | aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))) & sbrdtbr0(X1) = xk) => aElementOf0(X1,szDzozmdt0(sdtlpdtrp0(xC,X0)))))) & (szDzozmdt0(sdtlpdtrp0(xC,X0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk) & ! [X1] : (((aSet0(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,X1) => aElementOf0(X2,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))) | aSubsetOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))))) & sbrdtbr0(X1) = xk) | aElementOf0(X1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0))),xk)))))) => (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)) & (! [X2] : ((aElementOf0(X2,sdtlpdtrp0(xN,X0)) => sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X2))) & (! [X2] : ((aElementOf0(X2,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0)))) <=> (aElement0(X2) & (aElementOf0(X2,X1) | X2 = szmzizndt0(sdtlpdtrp0(xN,X0)))))) & sdtlpdtrp0(sdtlpdtrp0(xC,X0),X1) = sdtlpdtrp0(xc,sdtpldt0(X1,szmzizndt0(sdtlpdtrp0(xN,X0))))))))))))))))))))). % 37.12/6.06 fof(m__, conjecture, ! [X0] : ((aElementOf0(X0,szNzAzT0) => ((aSet0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) & ! [X1] : ((aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) <=> ? [X2] : ((aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X0))) & sdtlpdtrp0(sdtlpdtrp0(xC,X0),X2) = X1))))) => (! [X1] : ((aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) => aElementOf0(X1,xT))) | aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))),xT)))))). % 37.12/6.06 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((aElementOf0(X0,szNzAzT0) => ((aSet0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) & ! [X1] : ((aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) <=> ? [X2] : ((aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X0))) & sdtlpdtrp0(sdtlpdtrp0(xC,X0),X2) = X1))))) => (! [X1] : ((aElementOf0(X1,sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0)))) => aElementOf0(X1,xT))) | aSubsetOf0(sdtlcdtrc0(sdtlpdtrp0(xC,X0),szDzozmdt0(sdtlpdtrp0(xC,X0))),xT))))), inference(negate_conjecture, [status(cth)], [m__])). % 37.12/6.06 cnf(c158, plain, ~aFunction0(X0) | ~aElementOf0(X1,szDzozmdt0(X0)) | aElementOf0(sdtlpdtrp0(X0,X1),sdtlcdtrc0(X0,szDzozmdt0(X0))), inference(clausification, [status(esa)], [mImgRng])). % 37.12/6.06 cnf(c179, plain, aFunction0(xc), inference(clausification, [status(esa)], [m__3453])). % 37.12/6.06 cnf(c187, plain, szDzozmdt0(xc) = slbdtsldtrb0(xS,xK), inference(clausification, [status(esa)], [m__3453])). % 37.12/6.06 cnf(c192, plain, ~aElementOf0(X0,sdtlcdtrc0(xc,szDzozmdt0(xc))) | aElementOf0(X0,xT), inference(clausification, [status(esa)], [m__3453])). % 37.12/6.06 cnf(c256, plain, ~aElementOf0(X0,szNzAzT0) | ~aSet0(X1) | ~X2(X0,X1) | X3(X0,X1), inference(clausification, [status(esa)], [m__3965])). % 37.12/6.06 cnf(c267, plain, X0(X1,X2) | ~aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk)), inference(clausification, [status(esa)], [m__3965])). % 37.12/6.06 cnf(c278, plain, ~X0(X1,X2) | aElementOf0(sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1))),slbdtsldtrb0(xS,xK)), inference(clausification, [status(esa)], [m__3965])). % 37.12/6.06 cnf(c281, plain, ~aElementOf0(X0,szNzAzT0) | X1(X0), inference(clausification, [status(esa)], [m__4151])). % 37.12/6.06 cnf(c292, plain, X0(X1,X2) | ~aElementOf0(X2,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk)), inference(clausification, [status(esa)], [m__4151])). % 37.12/6.06 cnf(c299, plain, ~X0(X1,X2) | sdtlpdtrp0(sdtlpdtrp0(xC,X1),X2) = sdtlpdtrp0(xc,sdtpldt0(X2,szmzizndt0(sdtlpdtrp0(xN,X1)))), inference(clausification, [status(esa)], [m__4151])). % 37.12/6.06 cnf(c308, plain, ~X0(X1) | ~aElementOf0(X2,szDzozmdt0(sdtlpdtrp0(xC,X1))) | aSet0(X2), inference(clausification, [status(esa)], [m__4151])). % 37.12/6.06 cnf(c315, plain, ~X0(X1) | szDzozmdt0(sdtlpdtrp0(xC,X1)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,X1),szmzizndt0(sdtlpdtrp0(xN,X1))),xk), inference(clausification, [status(esa)], [m__4151])). % 37.12/6.06 cnf(c316, plain, ~X0(X1) | ~aSet0(X2) | ~X3(X1,X2) | X4(X1,X2), inference(clausification, [status(esa)], [m__4151])). % 37.12/6.06 cnf(c317, plain, aElementOf0(sK229,szNzAzT0), inference(clausification, [status(esa)], [negated_conjecture])). % 37.12/6.06 cnf(c319, plain, ~aElementOf0(X0,sdtlcdtrc0(sdtlpdtrp0(xC,sK229),szDzozmdt0(sdtlpdtrp0(xC,sK229)))) | aElementOf0(sK231(X0),szDzozmdt0(sdtlpdtrp0(xC,sK229))), inference(clausification, [status(esa)], [negated_conjecture])). % 37.12/6.06 cnf(c320, plain, ~aElementOf0(X0,sdtlcdtrc0(sdtlpdtrp0(xC,sK229),szDzozmdt0(sdtlpdtrp0(xC,sK229)))) | sdtlpdtrp0(sdtlpdtrp0(xC,sK229),sK231(X0)) = X0, inference(clausification, [status(esa)], [negated_conjecture])). % 37.12/6.06 cnf(c322, plain, aElementOf0(sK233,sdtlcdtrc0(sdtlpdtrp0(xC,sK229),szDzozmdt0(sdtlpdtrp0(xC,sK229)))), inference(clausification, [status(esa)], [negated_conjecture])). % 37.12/6.06 cnf(c323, plain, ~aElementOf0(sK233,xT), inference(clausification, [status(esa)], [negated_conjecture])). % 37.12/6.06 cnf(d0, plain, aElementOf0(sdtpldt0(X0,szmzizndt0(sdtlpdtrp0(xN,X1))),szDzozmdt0(xc)) | ~'Ts205'(X1,X0), inference(demodulation, [status(thm)], [c278,c187])). % 37.12/6.06 cnf(d1, plain, aElementOf0(sdtlpdtrp0(xc,X0),xT) | ~aElementOf0(X0,szDzozmdt0(xc)) | ~aFunction0(xc), inference(resolution, [status(thm)], [c192,c158])). % 37.12/6.06 cnf(d2, plain, ~aElementOf0(X0,szDzozmdt0(xc)) | aElementOf0(sdtlpdtrp0(xc,X0),xT), inference(resolution, [status(thm)], [c179,d1])). % 37.12/6.06 cnf(d3, plain, sdtlpdtrp0(sdtlpdtrp0(xC,sK229),sK231(sK233)) = sK233, inference(resolution, [status(thm)], [c320,c322])). % 37.12/6.06 cnf(d4, plain, aElementOf0(sK231(sK233),szDzozmdt0(sdtlpdtrp0(xC,sK229))), inference(resolution, [status(thm)], [c319,c322])). % 37.12/6.06 cnf(d5, plain, 'Ts216'(sK229), inference(resolution, [status(thm)], [c281,c317])). % 37.12/6.06 cnf(d6, plain, szDzozmdt0(sdtlpdtrp0(xC,sK229)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,sK229),szmzizndt0(sdtlpdtrp0(xN,sK229))),xk), inference(resolution, [status(thm)], [c315,d5])). % 37.12/6.06 cnf(d7, plain, ~aElementOf0(X0,szDzozmdt0(sdtlpdtrp0(xC,sK229))) | 'Ts214'(sK229,X0), inference(superposition, [status(thm)], [d6,c292])). % 37.12/6.06 cnf(d8, plain, 'Ts214'(sK229,sK231(sK233)), inference(resolution, [status(thm)], [d7,d4])). % 37.12/6.06 cnf(d9, plain, ~aSet0(sK231(sK233)) | ~'Ts216'(sK229) | 'Ts215'(sK229,sK231(sK233)), inference(resolution, [status(thm)], [d8,c316])). % 37.12/6.06 cnf(d10, plain, ~aSet0(sK231(sK233)) | 'Ts215'(sK229,sK231(sK233)), inference(resolution, [status(thm)], [d5,d9])). % 37.12/6.06 cnf(d11, plain, aSet0(sK231(sK233)) | ~'Ts216'(sK229), inference(resolution, [status(thm)], [c308,d4])). % 37.12/6.06 cnf(d12, plain, aSet0(sK231(sK233)), inference(resolution, [status(thm)], [d5,d11])). % 37.12/6.06 cnf(d13, plain, 'Ts215'(sK229,sK231(sK233)), inference(resolution, [status(thm)], [d12,d10])). % 37.12/6.06 cnf(d14, plain, sdtlpdtrp0(sdtlpdtrp0(xC,sK229),sK231(sK233)) = sdtlpdtrp0(xc,sdtpldt0(sK231(sK233),szmzizndt0(sdtlpdtrp0(xN,sK229)))), inference(resolution, [status(thm)], [d13,c299])). % 37.12/6.06 cnf(d15, plain, sK233 = sdtlpdtrp0(xc,sdtpldt0(sK231(sK233),szmzizndt0(sdtlpdtrp0(xN,sK229)))), inference(demodulation, [status(thm)], [d14,d3])). % 37.12/6.06 cnf(d16, plain, aElementOf0(sK233,xT) | ~aElementOf0(sdtpldt0(sK231(sK233),szmzizndt0(sdtlpdtrp0(xN,sK229))),szDzozmdt0(xc)), inference(superposition, [status(thm)], [d15,d2])). % 37.12/6.06 cnf(d17, plain, ~aElementOf0(sdtpldt0(sK231(sK233),szmzizndt0(sdtlpdtrp0(xN,sK229))),szDzozmdt0(xc)), inference(resolution, [status(thm)], [c323,d16])). % 37.12/6.06 cnf(d18, plain, ~'Ts205'(sK229,sK231(sK233)), inference(resolution, [status(thm)], [d17,d0])). % 37.12/6.06 cnf(d19, plain, ~aElementOf0(X0,szDzozmdt0(sdtlpdtrp0(xC,sK229))) | 'Ts204'(sK229,X0), inference(superposition, [status(thm)], [d6,c267])). % 37.12/6.06 cnf(d20, plain, 'Ts204'(sK229,sK231(sK233)), inference(resolution, [status(thm)], [d19,d4])). % 37.12/6.06 cnf(d21, plain, ~aSet0(sK231(sK233)) | ~aElementOf0(sK229,szNzAzT0) | 'Ts205'(sK229,sK231(sK233)), inference(resolution, [status(thm)], [d20,c256])). % 37.12/6.06 cnf(d22, plain, ~aSet0(sK231(sK233)) | 'Ts205'(sK229,sK231(sK233)), inference(resolution, [status(thm)], [c317,d21])). % 37.12/6.06 cnf(d23, plain, 'Ts205'(sK229,sK231(sK233)), inference(resolution, [status(thm)], [d12,d22])). % 37.12/6.06 cnf(d24, plain, $false, inference(resolution, [status(thm)], [d23,d18])). % 37.12/6.06 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------