%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM535+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 : n014.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:03 AM UTC 2026 % Result : Theorem 13.88s 2.06s % Output : CNFRefutation 13.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM535+2 : 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.09/0.35 % Computer : n014.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.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Sat Sep 26 03:08:02 UTC 2026 % 0.09/0.35 % CPUTime : % 0.09/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.88/2.06 % SZS status Theorem for theBenchmark.p % 13.88/2.06 % SZS output start CNFRefutation for theBenchmark.p % 13.88/2.06 fof(mEOfElem, axiom, ! [X0] : ((aSet0(X0) => ! [X1] : ((aElementOf0(X1,X0) => aElement0(X1)))))). % 13.88/2.06 fof(m__617, hypothesis, aSet0(xS)). % 13.88/2.06 fof(m__617_02, hypothesis, aElementOf0(xx,xS)). % 13.88/2.06 fof(m__, conjecture, (((aSet0(sdtmndt0(xS,xx)) & ! [X0] : ((aElementOf0(X0,sdtmndt0(xS,xx)) <=> (aElement0(X0) & (aElementOf0(X0,xS) & X0 != xx))))) => ((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx)) & ! [X0] : ((aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)) <=> (aElement0(X0) & (aElementOf0(X0,sdtmndt0(xS,xx)) | X0 = xx))))) => (! [X0] : ((aElementOf0(X0,xS) => aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)))) | aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))))) & ((aSet0(sdtmndt0(xS,xx)) & ! [X0] : ((aElementOf0(X0,sdtmndt0(xS,xx)) <=> (aElement0(X0) & (aElementOf0(X0,xS) & X0 != xx))))) => ((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx)) & ! [X0] : ((aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)) <=> (aElement0(X0) & (aElementOf0(X0,sdtmndt0(xS,xx)) | X0 = xx))))) => (! [X0] : ((aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)) => aElementOf0(X0,xS))) | aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)))))). % 13.88/2.06 fof(negated_conjecture, negated_conjecture, ~((((aSet0(sdtmndt0(xS,xx)) & ! [X0] : ((aElementOf0(X0,sdtmndt0(xS,xx)) <=> (aElement0(X0) & (aElementOf0(X0,xS) & X0 != xx))))) => ((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx)) & ! [X0] : ((aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)) <=> (aElement0(X0) & (aElementOf0(X0,sdtmndt0(xS,xx)) | X0 = xx))))) => (! [X0] : ((aElementOf0(X0,xS) => aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)))) | aSubsetOf0(xS,sdtpldt0(sdtmndt0(xS,xx),xx))))) & ((aSet0(sdtmndt0(xS,xx)) & ! [X0] : ((aElementOf0(X0,sdtmndt0(xS,xx)) <=> (aElement0(X0) & (aElementOf0(X0,xS) & X0 != xx))))) => ((aSet0(sdtpldt0(sdtmndt0(xS,xx),xx)) & ! [X0] : ((aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)) <=> (aElement0(X0) & (aElementOf0(X0,sdtmndt0(xS,xx)) | X0 = xx))))) => (! [X0] : ((aElementOf0(X0,sdtpldt0(sdtmndt0(xS,xx),xx)) => aElementOf0(X0,xS))) | aSubsetOf0(sdtpldt0(sdtmndt0(xS,xx),xx),xS)))))), inference(negate_conjecture, [status(cth)], [m__])). % 13.88/2.06 cnf(c0, plain, ~aSet0(X0) | ~aElementOf0(X1,X0) | aElement0(X1), inference(clausification, [status(esa)], [mEOfElem])). % 13.88/2.06 cnf(c46, plain, aSet0(xS), inference(clausification, [status(esa)], [m__617])). % 13.88/2.06 cnf(c47, plain, aElementOf0(xx,xS), inference(clausification, [status(esa)], [m__617_02])). % 13.88/2.06 cnf(c48, plain, ~X0 | ~X1, inference(clausification, [status(esa)], [negated_conjecture])). % 13.88/2.06 cnf(c53, plain, ~aElementOf0(X0,xS) | ~aElement0(X0) | aElementOf0(X0,sdtmndt0(xS,xx)) | X1 | X0 = xx, inference(clausification, [status(esa)], [negated_conjecture])). % 13.88/2.06 cnf(c57, plain, X0 | aElementOf0(X1,sdtpldt0(sdtmndt0(xS,xx),xx)) | ~aElement0(X1) | ~aElementOf0(X1,sdtmndt0(xS,xx)), inference(clausification, [status(esa)], [negated_conjecture])). % 13.88/2.06 cnf(c58, plain, X0 | aElementOf0(X1,sdtpldt0(sdtmndt0(xS,xx),xx)) | ~aElement0(X1) | X1 != xx, inference(clausification, [status(esa)], [negated_conjecture])). % 13.88/2.06 cnf(c59, plain, X0 | aElementOf0(sK39,xS), inference(clausification, [status(esa)], [negated_conjecture])). % 13.88/2.06 cnf(c60, plain, X0 | ~aElementOf0(sK39,sdtpldt0(sdtmndt0(xS,xx),xx)), inference(clausification, [status(esa)], [negated_conjecture])). % 13.88/2.06 cnf(c64, plain, X0 | ~aElementOf0(X1,sdtmndt0(xS,xx)) | aElementOf0(X1,xS), inference(clausification, [status(esa)], [negated_conjecture])). % 13.88/2.06 cnf(c69, plain, X0 | ~aElementOf0(X1,sdtpldt0(sdtmndt0(xS,xx),xx)) | aElementOf0(X1,sdtmndt0(xS,xx)) | X1 = xx, inference(clausification, [status(esa)], [negated_conjecture])). % 13.88/2.06 cnf(c72, plain, X0 | aElementOf0(sK42,sdtpldt0(sdtmndt0(xS,xx),xx)), inference(clausification, [status(esa)], [negated_conjecture])). % 13.88/2.06 cnf(c73, plain, X0 | ~aElementOf0(sK42,xS), inference(clausification, [status(esa)], [negated_conjecture])). % 13.88/2.06 cnf(d0, plain, sK42 = xx | aElementOf0(sK42,sdtmndt0(xS,xx)) | 'Ts36' | 'Ts36', inference(resolution, [status(thm)], [c69,c72])). % 13.88/2.06 cnf(d1, plain, sK42 = xx | 'Ts36' | aElementOf0(sK42,xS) | 'Ts36', inference(resolution, [status(thm)], [d0,c64])). % 13.88/2.06 cnf(d2, plain, sK42 = xx | 'Ts36' | 'Ts36', inference(resolution, [status(thm)], [d1,c73])). % 13.88/2.06 cnf(d3, plain, sK42 = xx | ~'Ts35', inference(resolution, [status(thm)], [d2,c48])). % 13.88/2.06 cnf(d4, plain, ~aElementOf0(sK39,sdtmndt0(xS,xx)) | ~aElement0(sK39) | 'Ts35' | 'Ts35', inference(resolution, [status(thm)], [c57,c60])). % 13.88/2.06 cnf(d5, plain, ~aElement0(sK39) | 'Ts35' | sK39 = xx | ~aElementOf0(sK39,xS) | ~aElement0(sK39) | 'Ts35', inference(resolution, [status(thm)], [d4,c53])). % 13.88/2.06 cnf(d6, plain, sK39 = xx | ~aElement0(sK39) | 'Ts35' | 'Ts35', inference(resolution, [status(thm)], [d5,c59])). % 13.88/2.06 cnf(d7, plain, 'Ts35' | ~aSet0(xS) | aElement0(sK39), inference(resolution, [status(thm)], [c59,c0])). % 13.88/2.06 cnf(d8, plain, aElement0(sK39) | 'Ts35', inference(resolution, [status(thm)], [c46,d7])). % 13.88/2.06 cnf(d9, plain, 'Ts35' | sK39 = xx | 'Ts35', inference(resolution, [status(thm)], [d8,d6])). % 13.88/2.06 cnf(d10, plain, sK42 = xx | sK39 = xx, inference(resolution, [status(thm)], [d3,d9])). % 13.88/2.06 cnf(d11, plain, ~aElementOf0(xx,xS) | 'Ts36' | sK39 = xx, inference(superposition, [status(thm)], [d10,c73])). % 13.88/2.06 cnf(d12, plain, sK39 = xx | 'Ts36', inference(resolution, [status(thm)], [c47,d11])). % 13.88/2.06 cnf(d13, plain, sK39 = xx | ~'Ts35', inference(resolution, [status(thm)], [d12,c48])). % 13.88/2.06 cnf(d14, plain, sK39 = xx | sK39 = xx, inference(resolution, [status(thm)], [d13,d9])). % 13.88/2.06 cnf(d15, plain, aElement0(xx) | 'Ts35', inference(demodulation, [status(thm)], [d8,d14])). % 13.88/2.06 cnf(d16, plain, aElementOf0(xx,sdtpldt0(sdtmndt0(xS,xx),xx)) | ~aElement0(xx) | 'Ts35', inference(equality_resolution, [status(thm)], [c58])). % 13.88/2.06 cnf(d17, plain, ~aElementOf0(xx,sdtpldt0(sdtmndt0(xS,xx),xx)) | 'Ts35', inference(demodulation, [status(thm)], [c60,d14])). % 13.88/2.06 cnf(d18, plain, 'Ts35' | ~aElement0(xx) | 'Ts35', inference(resolution, [status(thm)], [d17,d16])). % 13.88/2.06 cnf(d19, plain, 'Ts35' | 'Ts35', inference(resolution, [status(thm)], [d18,d15])). % 13.88/2.06 cnf(d20, plain, sK42 = xx, inference(resolution, [status(thm)], [d19,d3])). % 13.88/2.06 cnf(d21, plain, ~'Ts36', inference(resolution, [status(thm)], [d19,c48])). % 13.88/2.06 cnf(d22, plain, ~aElementOf0(sK42,xS), inference(resolution, [status(thm)], [d21,c73])). % 13.88/2.06 cnf(d23, plain, ~aElementOf0(xx,xS), inference(demodulation, [status(thm)], [d22,d20])). % 13.88/2.06 cnf(d24, plain, $false, inference(resolution, [status(thm)], [c47,d23])). % 13.88/2.06 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------