%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM537+2 : 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 : n001.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:04 AM UTC 2026 % Result : Theorem 15.56s 3.78s % Output : CNFRefutation 15.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM537+2 : 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.09/0.34 % Computer : n001.cluster.edu % 0.09/0.34 % Model : x86_64 x86_64 % 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.34 % Memory : 8046.5625MB % 0.09/0.34 % OS : Linux 6.8.0-71-generic % 0.09/0.34 % CPULimit : 300 % 0.09/0.34 % WCLimit : 300 % 0.09/0.34 % DateTime : Sat Sep 26 03:14:41 UTC 2026 % 0.09/0.34 % CPUTime : % 0.09/0.34 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 15.56/3.78 % SZS status Theorem for theBenchmark.p % 15.56/3.78 % SZS output start CNFRefutation for theBenchmark.p % 15.56/3.78 fof(mEOfElem, axiom, ! [X0] : ((aSet0(X0) => ! [X1] : ((aElementOf0(X1,X0) => aElement0(X1)))))). % 15.56/3.78 fof(m__679, hypothesis, (aElement0(xx) & aSet0(xS))). % 15.56/3.78 fof(m__679_02, hypothesis, ~aElementOf0(xx,xS)). % 15.56/3.78 fof(m__, conjecture, (((aSet0(sdtpldt0(xS,xx)) & ! [X0] : ((aElementOf0(X0,sdtpldt0(xS,xx)) <=> (aElement0(X0) & (aElementOf0(X0,xS) | X0 = xx))))) => ((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx)) & ! [X0] : ((aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx)) <=> (aElement0(X0) & (aElementOf0(X0,sdtpldt0(xS,xx)) & X0 != xx))))) => (! [X0] : ((aElementOf0(X0,xS) => aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx)))) | aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))))) & ((aSet0(sdtpldt0(xS,xx)) & ! [X0] : ((aElementOf0(X0,sdtpldt0(xS,xx)) <=> (aElement0(X0) & (aElementOf0(X0,xS) | X0 = xx))))) => ((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx)) & ! [X0] : ((aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx)) <=> (aElement0(X0) & (aElementOf0(X0,sdtpldt0(xS,xx)) & X0 != xx))))) => (! [X0] : ((aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx)) => aElementOf0(X0,xS))) | aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)))))). % 15.56/3.78 fof(negated_conjecture, negated_conjecture, ~((((aSet0(sdtpldt0(xS,xx)) & ! [X0] : ((aElementOf0(X0,sdtpldt0(xS,xx)) <=> (aElement0(X0) & (aElementOf0(X0,xS) | X0 = xx))))) => ((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx)) & ! [X0] : ((aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx)) <=> (aElement0(X0) & (aElementOf0(X0,sdtpldt0(xS,xx)) & X0 != xx))))) => (! [X0] : ((aElementOf0(X0,xS) => aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx)))) | aSubsetOf0(xS,sdtmndt0(sdtpldt0(xS,xx),xx))))) & ((aSet0(sdtpldt0(xS,xx)) & ! [X0] : ((aElementOf0(X0,sdtpldt0(xS,xx)) <=> (aElement0(X0) & (aElementOf0(X0,xS) | X0 = xx))))) => ((aSet0(sdtmndt0(sdtpldt0(xS,xx),xx)) & ! [X0] : ((aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx)) <=> (aElement0(X0) & (aElementOf0(X0,sdtpldt0(xS,xx)) & X0 != xx))))) => (! [X0] : ((aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx)) => aElementOf0(X0,xS))) | aSubsetOf0(sdtmndt0(sdtpldt0(xS,xx),xx),xS)))))), inference(negate_conjecture, [status(cth)], [m__])). % 15.56/3.78 cnf(c0, plain, ~aSet0(X0) | ~aElementOf0(X1,X0) | aElement0(X1), inference(clausification, [status(esa)], [mEOfElem])). % 15.56/3.78 cnf(c48, plain, aSet0(xS), inference(clausification, [status(esa)], [m__679])). % 15.56/3.78 cnf(c49, plain, ~aElementOf0(xx,xS), inference(clausification, [status(esa)], [m__679_02])). % 15.56/3.78 cnf(c50, plain, ~X0 | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 15.56/3.78 cnf(c54, plain, X0 | aElementOf0(X1,sdtpldt0(xS,xx)) | ~aElement0(X1) | ~aElementOf0(X1,xS), inference(clausification, [status(esa)], [negated_conjecture])). % 15.56/3.78 cnf(c60, plain, X0 = xx | X1 | ~aElementOf0(X0,sdtpldt0(xS,xx)) | ~aElement0(X0) | aElementOf0(X0,sdtmndt0(sdtpldt0(xS,xx),xx)), inference(clausification, [status(esa)], [negated_conjecture])). % 15.56/3.78 cnf(c61, plain, X0 | aElementOf0(sK41,xS), inference(clausification, [status(esa)], [negated_conjecture])). % 15.56/3.78 cnf(c62, plain, X0 | ~aElementOf0(sK41,sdtmndt0(sdtpldt0(xS,xx),xx)), inference(clausification, [status(esa)], [negated_conjecture])). % 15.56/3.78 cnf(c66, plain, X0 | ~aElementOf0(X1,sdtpldt0(xS,xx)) | aElementOf0(X1,xS) | X1 = xx, inference(clausification, [status(esa)], [negated_conjecture])). % 15.56/3.78 cnf(c71, plain, X0 | ~aElementOf0(X1,sdtmndt0(sdtpldt0(xS,xx),xx)) | aElementOf0(X1,sdtpldt0(xS,xx)), inference(clausification, [status(esa)], [negated_conjecture])). % 15.56/3.78 cnf(c72, plain, X0 | ~aElementOf0(X1,sdtmndt0(sdtpldt0(xS,xx),xx)) | X1 != xx, inference(clausification, [status(esa)], [negated_conjecture])). % 15.56/3.78 cnf(c74, plain, X0 | aElementOf0(sK44,sdtmndt0(sdtpldt0(xS,xx),xx)), inference(clausification, [status(esa)], [negated_conjecture])). % 15.56/3.78 cnf(c75, plain, X0 | ~aElementOf0(sK44,xS), inference(clausification, [status(esa)], [negated_conjecture])). % 15.56/3.78 cnf(d0, plain, ~aElementOf0(xx,sdtmndt0(sdtpldt0(xS,xx),xx)) | 'Ts38', inference(equality_resolution, [status(thm)], [c72])). % 15.56/3.78 cnf(d1, plain, 'Ts37' | ~aSet0(xS) | aElement0(sK41), inference(resolution, [status(thm)], [c61,c0])). % 15.56/3.78 cnf(d2, plain, aElement0(sK41) | 'Ts37', inference(resolution, [status(thm)], [c48,d1])). % 15.56/3.78 cnf(d3, plain, sK41 = xx | ~aElementOf0(sK41,sdtpldt0(xS,xx)) | ~aElement0(sK41) | 'Ts37' | 'Ts37', inference(resolution, [status(thm)], [c60,c62])). % 15.56/3.78 cnf(d4, plain, sK41 = xx | ~aElement0(sK41) | 'Ts37' | ~aElementOf0(sK41,xS) | ~aElement0(sK41) | 'Ts37', inference(resolution, [status(thm)], [d3,c54])). % 15.56/3.78 cnf(d5, plain, sK41 = xx | ~aElement0(sK41) | 'Ts37' | 'Ts37', inference(resolution, [status(thm)], [d4,c61])). % 15.56/3.78 cnf(d6, plain, sK41 = xx | 'Ts37' | 'Ts37', inference(resolution, [status(thm)], [d5,d2])). % 15.56/3.78 cnf(d7, plain, sK41 = xx | ~'Ts38', inference(resolution, [status(thm)], [d6,c50])). % 15.56/3.78 cnf(d8, plain, aElementOf0(sK44,sdtpldt0(xS,xx)) | 'Ts38' | 'Ts38', inference(resolution, [status(thm)], [c71,c74])). % 15.56/3.78 cnf(d9, plain, 'Ts38' | sK44 = xx | aElementOf0(sK44,xS) | 'Ts38', inference(resolution, [status(thm)], [d8,c66])). % 15.56/3.78 cnf(d10, plain, sK44 = xx | 'Ts38' | 'Ts38', inference(resolution, [status(thm)], [d9,c75])). % 15.56/3.78 cnf(d11, plain, sK41 = xx | sK44 = xx, inference(resolution, [status(thm)], [d7,d10])). % 15.56/3.78 cnf(d12, plain, aElementOf0(xx,sdtmndt0(sdtpldt0(xS,xx),xx)) | 'Ts38' | sK41 = xx, inference(superposition, [status(thm)], [d11,c74])). % 15.56/3.78 cnf(d13, plain, sK41 = xx | 'Ts38' | 'Ts38', inference(resolution, [status(thm)], [d12,d0])). % 15.56/3.78 cnf(d14, plain, sK41 = xx | sK41 = xx, inference(resolution, [status(thm)], [d13,d7])). % 15.56/3.78 cnf(d15, plain, aElementOf0(xx,xS) | 'Ts37', inference(demodulation, [status(thm)], [c61,d14])). % 15.56/3.78 cnf(d16, plain, 'Ts37', inference(resolution, [status(thm)], [c49,d15])). % 15.56/3.78 cnf(d17, plain, ~'Ts38', inference(resolution, [status(thm)], [d16,c50])). % 15.56/3.78 cnf(d18, plain, ~aElementOf0(xx,sdtmndt0(sdtpldt0(xS,xx),xx)), inference(resolution, [status(thm)], [d17,d0])). % 15.56/3.78 cnf(d19, plain, sK44 = xx, inference(resolution, [status(thm)], [d17,d10])). % 15.56/3.78 cnf(d20, plain, aElementOf0(sK44,sdtmndt0(sdtpldt0(xS,xx),xx)), inference(resolution, [status(thm)], [d17,c74])). % 15.56/3.78 cnf(d21, plain, aElementOf0(xx,sdtmndt0(sdtpldt0(xS,xx),xx)), inference(demodulation, [status(thm)], [d20,d19])). % 15.56/3.78 cnf(d22, plain, $false, inference(resolution, [status(thm)], [d21,d18])). % 15.56/3.78 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------