%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM541+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 : n002.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:05 AM UTC 2026 % Result : Theorem 13.76s 2.53s % Output : CNFRefutation 13.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : NUM541+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.08/0.36 % Computer : n002.cluster.edu % 0.08/0.36 % Model : x86_64 x86_64 % 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.36 % Memory : 8046.5625MB % 0.08/0.36 % OS : Linux 6.8.0-71-generic % 0.08/0.36 % CPULimit : 300 % 0.08/0.36 % WCLimit : 300 % 0.08/0.36 % DateTime : Sat Sep 26 03:12:20 UTC 2026 % 0.08/0.36 % CPUTime : % 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.76/2.53 % SZS status Theorem for theBenchmark.p % 13.76/2.53 % SZS output start CNFRefutation for theBenchmark.p % 13.76/2.53 fof(mSuccNum, axiom, ! [X0] : ((aElementOf0(X0,szNzAzT0) => (aElementOf0(szszuzczcdt0(X0),szNzAzT0) & szszuzczcdt0(X0) != sz00)))). % 13.76/2.53 fof(mSuccLess, axiom, ! [X0] : ! [X1] : (((aElementOf0(X0,szNzAzT0) & aElementOf0(X1,szNzAzT0)) => (sdtlseqdt0(X0,X1) <=> sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1)))))). % 13.76/2.53 fof(mLessSucc, axiom, ! [X0] : ((aElementOf0(X0,szNzAzT0) => sdtlseqdt0(X0,szszuzczcdt0(X0))))). % 13.76/2.53 fof(mLessRefl, axiom, ! [X0] : ((aElementOf0(X0,szNzAzT0) => sdtlseqdt0(X0,X0)))). % 13.76/2.53 fof(mLessASymm, axiom, ! [X0] : ! [X1] : (((aElementOf0(X0,szNzAzT0) & aElementOf0(X1,szNzAzT0)) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X0)) => X0 = X1)))). % 13.76/2.53 fof(mLessTrans, axiom, ! [X0] : ! [X1] : ! [X2] : (((aElementOf0(X0,szNzAzT0) & (aElementOf0(X1,szNzAzT0) & aElementOf0(X2,szNzAzT0))) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X2)) => sdtlseqdt0(X0,X2))))). % 13.76/2.53 fof(mLessTotal, axiom, ! [X0] : ! [X1] : (((aElementOf0(X0,szNzAzT0) & aElementOf0(X1,szNzAzT0)) => (sdtlseqdt0(X0,X1) | sdtlseqdt0(szszuzczcdt0(X1),X0))))). % 13.76/2.53 fof(m__1936, hypothesis, (aElementOf0(xm,szNzAzT0) & aElementOf0(xn,szNzAzT0))). % 13.76/2.53 fof(m__, conjecture, (((sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)) & aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))) => (sdtlseqdt0(szszuzczcdt0(xm),xn) | (aElementOf0(xm,slbdtrb0(xn)) | xm = xn))) & (((sdtlseqdt0(szszuzczcdt0(xm),xn) & aElementOf0(xm,slbdtrb0(xn))) | xm = xn) => (sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)) | aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))))). % 13.76/2.53 fof(negated_conjecture, negated_conjecture, ~((((sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)) & aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn)))) => (sdtlseqdt0(szszuzczcdt0(xm),xn) | (aElementOf0(xm,slbdtrb0(xn)) | xm = xn))) & (((sdtlseqdt0(szszuzczcdt0(xm),xn) & aElementOf0(xm,slbdtrb0(xn))) | xm = xn) => (sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)) | aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))))))), inference(negate_conjecture, [status(cth)], [m__])). % 13.76/2.53 cnf(c55, plain, ~aElementOf0(X0,szNzAzT0) | aElementOf0(szszuzczcdt0(X0),szNzAzT0), inference(clausification, [status(esa)], [mSuccNum])). % 13.76/2.53 cnf(c63, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | ~sdtlseqdt0(X0,X1) | sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1)), inference(clausification, [status(esa)], [mSuccLess])). % 13.76/2.53 cnf(c64, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | sdtlseqdt0(X0,X1) | ~sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1)), inference(clausification, [status(esa)], [mSuccLess])). % 13.76/2.53 cnf(c65, plain, ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(X0,szszuzczcdt0(X0)), inference(clausification, [status(esa)], [mLessSucc])). % 13.76/2.53 cnf(c66, plain, ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(X0,X0), inference(clausification, [status(esa)], [mLessRefl])). % 13.76/2.53 cnf(c67, plain, ~sdtlseqdt0(X0,X1) | ~aElementOf0(X1,szNzAzT0) | ~sdtlseqdt0(X1,X0) | X1 = X0 | ~aElementOf0(X0,szNzAzT0), inference(clausification, [status(esa)], [mLessASymm])). % 13.76/2.53 cnf(c68, plain, ~aElementOf0(X0,szNzAzT0) | ~sdtlseqdt0(X0,X1) | sdtlseqdt0(X2,X1) | ~aElementOf0(X2,szNzAzT0) | ~sdtlseqdt0(X2,X0) | ~aElementOf0(X1,szNzAzT0), inference(clausification, [status(esa)], [mLessTrans])). % 13.76/2.53 cnf(c69, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | sdtlseqdt0(X0,X1) | sdtlseqdt0(szszuzczcdt0(X1),X0), inference(clausification, [status(esa)], [mLessTotal])). % 13.76/2.53 cnf(c104, plain, aElementOf0(xm,szNzAzT0), inference(clausification, [status(esa)], [m__1936])). % 13.76/2.53 cnf(c105, plain, aElementOf0(xn,szNzAzT0), inference(clausification, [status(esa)], [m__1936])). % 13.76/2.53 cnf(c106, plain, ~X0 | sdtlseqdt0(szszuzczcdt0(xm),xn) | xm = xn, inference(clausification, [status(esa)], [negated_conjecture])). % 13.76/2.53 cnf(c108, plain, ~X0 | ~sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)), inference(clausification, [status(esa)], [negated_conjecture])). % 13.76/2.53 cnf(c110, plain, X0 | sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)), inference(clausification, [status(esa)], [negated_conjecture])). % 13.76/2.53 cnf(c112, plain, X0 | ~sdtlseqdt0(szszuzczcdt0(xm),xn), inference(clausification, [status(esa)], [negated_conjecture])). % 13.76/2.53 cnf(c114, plain, X0 | xm != xn, inference(clausification, [status(esa)], [negated_conjecture])). % 13.76/2.53 cnf(d0, plain, ~aElementOf0(xm,szNzAzT0) | ~aElementOf0(xn,szNzAzT0) | sdtlseqdt0(xm,xn) | 'Ts99', inference(resolution, [status(thm)], [c64,c110])). % 13.76/2.53 cnf(d1, plain, ~aElementOf0(xn,szNzAzT0) | sdtlseqdt0(xm,xn) | 'Ts99', inference(resolution, [status(thm)], [c104,d0])). % 13.76/2.53 cnf(d2, plain, sdtlseqdt0(xm,xn) | 'Ts99', inference(resolution, [status(thm)], [c105,d1])). % 13.76/2.53 cnf(d3, plain, ~aElementOf0(xn,szNzAzT0) | ~aElementOf0(xm,szNzAzT0) | sdtlseqdt0(xn,xm) | 'Ts99', inference(resolution, [status(thm)], [c69,c112])). % 13.76/2.53 cnf(d4, plain, ~aElementOf0(xn,szNzAzT0) | sdtlseqdt0(xn,xm) | 'Ts99', inference(resolution, [status(thm)], [c104,d3])). % 13.76/2.53 cnf(d5, plain, sdtlseqdt0(xn,xm) | 'Ts99', inference(resolution, [status(thm)], [c105,d4])). % 13.76/2.53 cnf(d6, plain, 'Ts99' | xm = xn | ~aElementOf0(xm,szNzAzT0) | ~aElementOf0(xn,szNzAzT0) | ~sdtlseqdt0(xm,xn), inference(resolution, [status(thm)], [d5,c67])). % 13.76/2.53 cnf(d7, plain, xm = xn | ~aElementOf0(xn,szNzAzT0) | ~sdtlseqdt0(xm,xn) | 'Ts99', inference(resolution, [status(thm)], [c104,d6])). % 13.76/2.53 cnf(d8, plain, xm = xn | ~sdtlseqdt0(xm,xn) | 'Ts99', inference(resolution, [status(thm)], [c105,d7])). % 13.76/2.53 cnf(d9, plain, xm = xn | 'Ts99' | 'Ts99', inference(resolution, [status(thm)], [d8,d2])). % 13.76/2.53 cnf(d10, plain, ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | ~aElementOf0(xm,szNzAzT0) | sdtlseqdt0(szszuzczcdt0(xn),xm) | ~'Ts99', inference(resolution, [status(thm)], [c69,c108])). % 13.76/2.53 cnf(d11, plain, ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | sdtlseqdt0(szszuzczcdt0(xn),xm) | ~'Ts99', inference(resolution, [status(thm)], [c104,d10])). % 13.76/2.53 cnf(d12, plain, sdtlseqdt0(szszuzczcdt0(xn),xm) | ~'Ts99' | ~aElementOf0(xn,szNzAzT0), inference(resolution, [status(thm)], [d11,c55])). % 13.76/2.53 cnf(d13, plain, sdtlseqdt0(szszuzczcdt0(xn),xm) | ~'Ts99', inference(resolution, [status(thm)], [c105,d12])). % 13.76/2.53 cnf(d14, plain, ~'Ts99' | ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(xm,szNzAzT0) | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | ~sdtlseqdt0(xm,X0) | sdtlseqdt0(szszuzczcdt0(xn),X0), inference(resolution, [status(thm)], [d13,c68])). % 13.76/2.53 cnf(d15, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | sdtlseqdt0(szszuzczcdt0(xn),X0) | ~sdtlseqdt0(xm,X0) | ~'Ts99', inference(resolution, [status(thm)], [c104,d14])). % 13.76/2.53 cnf(d16, plain, ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(szszuzczcdt0(xn),X0) | ~sdtlseqdt0(xm,X0) | ~'Ts99' | ~aElementOf0(xn,szNzAzT0), inference(resolution, [status(thm)], [d15,c55])). % 13.76/2.53 cnf(d17, plain, ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(szszuzczcdt0(xn),X0) | ~sdtlseqdt0(xm,X0) | ~'Ts99', inference(resolution, [status(thm)], [c105,d16])). % 13.76/2.53 cnf(d18, plain, ~aElementOf0(szszuzczcdt0(X0),szNzAzT0) | ~sdtlseqdt0(xm,szszuzczcdt0(X0)) | ~'Ts99' | ~aElementOf0(xn,szNzAzT0) | ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(xn,X0), inference(resolution, [status(thm)], [d17,c64])). % 13.76/2.53 cnf(d19, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(szszuzczcdt0(X0),szNzAzT0) | ~sdtlseqdt0(xm,szszuzczcdt0(X0)) | sdtlseqdt0(xn,X0) | ~'Ts99', inference(resolution, [status(thm)], [c105,d18])). % 13.76/2.53 cnf(d20, plain, ~aElementOf0(xm,szNzAzT0) | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | sdtlseqdt0(xn,xm) | ~'Ts99' | ~aElementOf0(xm,szNzAzT0), inference(resolution, [status(thm)], [d19,c65])). % 13.76/2.53 cnf(d21, plain, ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | sdtlseqdt0(xn,xm) | ~'Ts99', inference(resolution, [status(thm)], [c104,d20])). % 13.76/2.53 cnf(d22, plain, sdtlseqdt0(xn,xm) | ~'Ts99' | ~aElementOf0(xm,szNzAzT0), inference(resolution, [status(thm)], [d21,c55])). % 13.76/2.53 cnf(d23, plain, sdtlseqdt0(xn,xm) | ~'Ts99', inference(resolution, [status(thm)], [c104,d22])). % 13.76/2.53 cnf(d24, plain, ~'Ts99' | ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(xm,szNzAzT0) | ~aElementOf0(xn,szNzAzT0) | ~sdtlseqdt0(xm,X0) | sdtlseqdt0(xn,X0), inference(resolution, [status(thm)], [d23,c68])). % 13.76/2.53 cnf(d25, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(xn,szNzAzT0) | ~sdtlseqdt0(xm,X0) | sdtlseqdt0(xn,X0) | ~'Ts99', inference(resolution, [status(thm)], [c104,d24])). % 13.76/2.53 cnf(d26, plain, ~aElementOf0(X0,szNzAzT0) | ~sdtlseqdt0(xm,X0) | sdtlseqdt0(xn,X0) | ~'Ts99', inference(resolution, [status(thm)], [c105,d25])). % 13.76/2.53 cnf(d27, plain, ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | sdtlseqdt0(xn,szszuzczcdt0(xm)) | ~'Ts99' | ~aElementOf0(xm,szNzAzT0), inference(resolution, [status(thm)], [d26,c65])). % 13.76/2.53 cnf(d28, plain, ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | sdtlseqdt0(xn,szszuzczcdt0(xm)) | ~'Ts99', inference(resolution, [status(thm)], [c104,d27])). % 13.76/2.53 cnf(d29, plain, sdtlseqdt0(xn,szszuzczcdt0(xm)) | ~'Ts99' | ~aElementOf0(xm,szNzAzT0), inference(resolution, [status(thm)], [d28,c55])). % 13.76/2.53 cnf(d30, plain, sdtlseqdt0(xn,szszuzczcdt0(xm)) | ~'Ts99', inference(resolution, [status(thm)], [c104,d29])). % 13.76/2.53 cnf(d31, plain, ~'Ts99' | szszuzczcdt0(xm) = xn | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | ~aElementOf0(xn,szNzAzT0) | ~sdtlseqdt0(szszuzczcdt0(xm),xn), inference(resolution, [status(thm)], [d30,c67])). % 13.76/2.53 cnf(d32, plain, szszuzczcdt0(xm) = xn | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | ~sdtlseqdt0(szszuzczcdt0(xm),xn) | ~'Ts99', inference(resolution, [status(thm)], [c105,d31])). % 13.76/2.53 cnf(d33, plain, szszuzczcdt0(xm) = xn | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | ~'Ts99' | xm = xn | ~'Ts99', inference(resolution, [status(thm)], [d32,c106])). % 13.76/2.53 cnf(d34, plain, szszuzczcdt0(xm) = xn | xm = xn | ~'Ts99' | ~aElementOf0(xm,szNzAzT0), inference(resolution, [status(thm)], [d33,c55])). % 13.76/2.53 cnf(d35, plain, szszuzczcdt0(xm) = xn | xm = xn | ~'Ts99', inference(resolution, [status(thm)], [c104,d34])). % 13.76/2.53 cnf(d36, plain, szszuzczcdt0(xm) = xn | xm = xn | xm = xn, inference(resolution, [status(thm)], [d35,d9])). % 13.76/2.53 cnf(d37, plain, ~sdtlseqdt0(xn,szszuzczcdt0(xn)) | ~'Ts99' | xm = xn, inference(superposition, [status(thm)], [d36,c108])). % 13.76/2.53 cnf(d38, plain, xm = xn | ~'Ts99' | ~aElementOf0(xn,szNzAzT0), inference(resolution, [status(thm)], [d37,c65])). % 13.76/2.53 cnf(d39, plain, xm = xn | ~'Ts99', inference(resolution, [status(thm)], [c105,d38])). % 13.76/2.53 cnf(d40, plain, xm = xn | xm = xn, inference(resolution, [status(thm)], [d39,d9])). % 13.76/2.53 cnf(d41, plain, ~aElementOf0(xm,szNzAzT0) | ~aElementOf0(xn,szNzAzT0) | ~sdtlseqdt0(xm,xn) | ~'Ts99', inference(resolution, [status(thm)], [c63,c108])). % 13.76/2.53 cnf(d42, plain, ~aElementOf0(xn,szNzAzT0) | ~sdtlseqdt0(xm,xn) | ~'Ts99', inference(resolution, [status(thm)], [c104,d41])). % 13.76/2.53 cnf(d43, plain, ~sdtlseqdt0(xm,xn) | ~'Ts99', inference(resolution, [status(thm)], [c105,d42])). % 13.76/2.53 cnf(d44, plain, ~sdtlseqdt0(xm,xm) | ~'Ts99', inference(demodulation, [status(thm)], [d43,d40])). % 13.76/2.53 cnf(d45, plain, sdtlseqdt0(xm,xm), inference(resolution, [status(thm)], [c66,c104])). % 13.76/2.53 cnf(d46, plain, ~'Ts99', inference(resolution, [status(thm)], [d45,d44])). % 13.76/2.53 cnf(d47, plain, 'Ts99', inference(resolution, [status(thm)], [d40,c114])). % 13.76/2.53 cnf(d48, plain, $false, inference(resolution, [status(thm)], [d47,d46])). % 13.76/2.53 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------