%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM541+1 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % Computer : n019.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 39.75s 11.11s % Output : CNFRefutation 39.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM541+1 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.11/5.38 % Computer : n019.cluster.edu % 0.11/5.38 % Model : x86_64 x86_64 % 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/5.38 % Memory : 8046.5625MB % 0.11/5.38 % OS : Linux 6.8.0-71-generic % 0.11/5.38 % CPULimit : 300 % 0.11/5.38 % WCLimit : 300 % 0.11/5.38 % DateTime : Sat Sep 26 03:10:11 UTC 2026 % 0.11/5.38 % CPUTime : % 0.11/5.39 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 39.75/11.11 % SZS status Theorem for theBenchmark.p % 39.75/11.11 % SZS output start CNFRefutation for theBenchmark.p % 39.75/11.11 fof(mSuccNum, axiom, ! [X0] : ((aElementOf0(X0,szNzAzT0) => (aElementOf0(szszuzczcdt0(X0),szNzAzT0) & szszuzczcdt0(X0) != sz00)))). % 39.75/11.11 fof(mSuccLess, axiom, ! [X0] : ! [X1] : (((aElementOf0(X0,szNzAzT0) & aElementOf0(X1,szNzAzT0)) => (sdtlseqdt0(X0,X1) <=> sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1)))))). % 39.75/11.11 fof(mLessSucc, axiom, ! [X0] : ((aElementOf0(X0,szNzAzT0) => sdtlseqdt0(X0,szszuzczcdt0(X0))))). % 39.75/11.11 fof(mLessRefl, axiom, ! [X0] : ((aElementOf0(X0,szNzAzT0) => sdtlseqdt0(X0,X0)))). % 39.75/11.11 fof(mLessASymm, axiom, ! [X0] : ! [X1] : (((aElementOf0(X0,szNzAzT0) & aElementOf0(X1,szNzAzT0)) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X0)) => X0 = X1)))). % 39.75/11.11 fof(mLessTrans, axiom, ! [X0] : ! [X1] : ! [X2] : (((aElementOf0(X0,szNzAzT0) & (aElementOf0(X1,szNzAzT0) & aElementOf0(X2,szNzAzT0))) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X2)) => sdtlseqdt0(X0,X2))))). % 39.75/11.11 fof(mLessTotal, axiom, ! [X0] : ! [X1] : (((aElementOf0(X0,szNzAzT0) & aElementOf0(X1,szNzAzT0)) => (sdtlseqdt0(X0,X1) | sdtlseqdt0(szszuzczcdt0(X1),X0))))). % 39.75/11.11 fof(mDefSeg, definition, ! [X0] : ((aElementOf0(X0,szNzAzT0) => ! [X1] : ((X1 = slbdtrb0(X0) <=> (aSet0(X1) & ! [X2] : ((aElementOf0(X2,X1) <=> (aElementOf0(X2,szNzAzT0) & sdtlseqdt0(szszuzczcdt0(X2),X0)))))))))). % 39.75/11.11 fof(m__1936, hypothesis, (aElementOf0(xm,szNzAzT0) & aElementOf0(xn,szNzAzT0))). % 39.75/11.11 fof(m__, conjecture, (aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) <=> (aElementOf0(xm,slbdtrb0(xn)) | xm = xn))). % 39.75/11.11 fof(negated_conjecture, negated_conjecture, ~((aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) <=> (aElementOf0(xm,slbdtrb0(xn)) | xm = xn))), inference(negate_conjecture, [status(cth)], [m__])). % 39.75/11.11 cnf(c55, plain, ~aElementOf0(X0,szNzAzT0) | aElementOf0(szszuzczcdt0(X0),szNzAzT0), inference(clausification, [status(esa)], [mSuccNum])). % 39.75/11.11 cnf(c64, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | sdtlseqdt0(X0,X1) | ~sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X1)), inference(clausification, [status(esa)], [mSuccLess])). % 39.75/11.11 cnf(c65, plain, ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(X0,szszuzczcdt0(X0)), inference(clausification, [status(esa)], [mLessSucc])). % 39.75/11.11 cnf(c66, plain, ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(X0,X0), inference(clausification, [status(esa)], [mLessRefl])). % 39.75/11.11 cnf(c67, plain, ~sdtlseqdt0(X0,X1) | ~aElementOf0(X1,szNzAzT0) | ~sdtlseqdt0(X1,X0) | X1 = X0 | ~aElementOf0(X0,szNzAzT0), inference(clausification, [status(esa)], [mLessASymm])). % 39.75/11.11 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])). % 39.75/11.11 cnf(c69, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | sdtlseqdt0(X0,X1) | sdtlseqdt0(szszuzczcdt0(X1),X0), inference(clausification, [status(esa)], [mLessTotal])). % 39.75/11.11 cnf(c90, plain, ~aElementOf0(X0,szNzAzT0) | X1 != slbdtrb0(X0) | X2(X0,X1), inference(clausification, [status(esa)], [mDefSeg])). % 39.75/11.11 cnf(c94, plain, ~X0(X1,X2) | ~aElementOf0(X3,X2) | sdtlseqdt0(szszuzczcdt0(X3),X1), inference(clausification, [status(esa)], [mDefSeg])). % 39.75/11.11 cnf(c95, plain, ~X0(X1,X2) | aElementOf0(X3,X2) | ~aElementOf0(X3,szNzAzT0) | ~sdtlseqdt0(szszuzczcdt0(X3),X1), inference(clausification, [status(esa)], [mDefSeg])). % 39.75/11.11 cnf(c104, plain, aElementOf0(xm,szNzAzT0), inference(clausification, [status(esa)], [m__1936])). % 39.75/11.11 cnf(c105, plain, aElementOf0(xn,szNzAzT0), inference(clausification, [status(esa)], [m__1936])). % 39.75/11.11 cnf(c107, plain, aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) | aElementOf0(xm,slbdtrb0(xn)) | xm = xn, inference(clausification, [status(esa)], [negated_conjecture])). % 39.75/11.11 cnf(c108, plain, ~aElementOf0(xm,slbdtrb0(xn)) | ~aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))), inference(clausification, [status(esa)], [negated_conjecture])). % 39.75/11.11 cnf(c110, plain, xm != xn | ~aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))), inference(clausification, [status(esa)], [negated_conjecture])). % 39.75/11.11 cnf(d0, plain, ~aElementOf0(X0,szNzAzT0) | 'Ts93'(X0,slbdtrb0(X0)), inference(equality_resolution, [status(thm)], [c90])). % 39.75/11.11 cnf(d1, plain, ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(szszuzczcdt0(X0),szszuzczcdt0(X0)), inference(resolution, [status(thm)], [c55,c66])). % 39.75/11.11 cnf(d2, plain, aElementOf0(X0,X1) | ~aElementOf0(X0,szNzAzT0) | ~'Ts93'(szszuzczcdt0(X0),X1) | ~aElementOf0(X0,szNzAzT0), inference(resolution, [status(thm)], [c95,d1])). % 39.75/11.11 cnf(d3, plain, aElementOf0(X0,slbdtrb0(szszuzczcdt0(X0))) | ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(szszuzczcdt0(X0),szNzAzT0), inference(resolution, [status(thm)], [d2,d0])). % 39.75/11.11 cnf(d4, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(szszuzczcdt0(X1),szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | ~sdtlseqdt0(szszuzczcdt0(X1),X0) | sdtlseqdt0(X1,X0) | ~aElementOf0(X1,szNzAzT0), inference(resolution, [status(thm)], [c68,c65])). % 39.75/11.11 cnf(d5, plain, ~aElementOf0(X0,slbdtrb0(X1)) | sdtlseqdt0(szszuzczcdt0(X0),X1) | ~aElementOf0(X1,szNzAzT0), inference(resolution, [status(thm)], [c94,d0])). % 39.75/11.11 cnf(d6, plain, ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | sdtlseqdt0(szszuzczcdt0(xm),szszuzczcdt0(xn)) | xm = xn | aElementOf0(xm,slbdtrb0(xn)), inference(resolution, [status(thm)], [d5,c107])). % 39.75/11.11 cnf(d7, plain, xm = xn | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | aElementOf0(xm,slbdtrb0(xn)) | ~aElementOf0(xm,szNzAzT0) | ~aElementOf0(xn,szNzAzT0) | sdtlseqdt0(xm,xn), inference(resolution, [status(thm)], [d6,c64])). % 39.75/11.11 cnf(d8, plain, xm = xn | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | aElementOf0(xm,slbdtrb0(xn)) | ~aElementOf0(xn,szNzAzT0) | sdtlseqdt0(xm,xn), inference(resolution, [status(thm)], [c104,d7])). % 39.75/11.11 cnf(d9, plain, xm = xn | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | aElementOf0(xm,slbdtrb0(xn)) | sdtlseqdt0(xm,xn), inference(resolution, [status(thm)], [c105,d8])). % 39.75/11.11 cnf(d10, plain, xm = xn | aElementOf0(xm,slbdtrb0(xn)) | sdtlseqdt0(xm,xn) | ~aElementOf0(xn,szNzAzT0), inference(resolution, [status(thm)], [d9,c55])). % 39.75/11.11 cnf(d11, plain, xm = xn | aElementOf0(xm,slbdtrb0(xn)) | sdtlseqdt0(xm,xn), inference(resolution, [status(thm)], [c105,d10])). % 39.75/11.11 cnf(d12, plain, xm = xn | sdtlseqdt0(xm,xn) | ~aElementOf0(xn,szNzAzT0) | sdtlseqdt0(szszuzczcdt0(xm),xn), inference(resolution, [status(thm)], [d11,d5])). % 39.75/11.11 cnf(d13, plain, xm = xn | sdtlseqdt0(szszuzczcdt0(xm),xn) | sdtlseqdt0(xm,xn), inference(resolution, [status(thm)], [c105,d12])). % 39.75/11.11 cnf(d14, plain, xm = xn | sdtlseqdt0(xm,xn) | ~aElementOf0(xm,szNzAzT0) | ~aElementOf0(xn,szNzAzT0) | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | sdtlseqdt0(xm,xn), inference(resolution, [status(thm)], [d13,d4])). % 39.75/11.11 cnf(d15, plain, xm = xn | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | ~aElementOf0(xn,szNzAzT0) | sdtlseqdt0(xm,xn), inference(resolution, [status(thm)], [c104,d14])). % 39.75/11.11 cnf(d16, plain, xm = xn | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | sdtlseqdt0(xm,xn), inference(resolution, [status(thm)], [c105,d15])). % 39.75/11.11 cnf(d17, plain, xm = xn | sdtlseqdt0(xm,xn) | ~aElementOf0(xm,szNzAzT0), inference(resolution, [status(thm)], [d16,c55])). % 39.75/11.11 cnf(d18, plain, xm = xn | sdtlseqdt0(xm,xn), inference(resolution, [status(thm)], [c104,d17])). % 39.75/11.11 cnf(d19, plain, xm = xn | xn = xm | ~aElementOf0(xn,szNzAzT0) | ~aElementOf0(xm,szNzAzT0) | ~sdtlseqdt0(xn,xm), inference(resolution, [status(thm)], [d18,c67])). % 39.75/11.11 cnf(d20, plain, xm = xn | xn = xm | ~aElementOf0(xn,szNzAzT0) | ~sdtlseqdt0(xn,xm), inference(resolution, [status(thm)], [c104,d19])). % 39.75/11.11 cnf(d21, plain, xm = xn | xn = xm | ~sdtlseqdt0(xn,xm), inference(resolution, [status(thm)], [c105,d20])). % 39.75/11.11 cnf(d22, plain, xm = xn | ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(xn,szNzAzT0) | ~aElementOf0(xm,szNzAzT0) | ~sdtlseqdt0(xn,X0) | sdtlseqdt0(xm,X0), inference(resolution, [status(thm)], [d18,c68])). % 39.75/11.11 cnf(d23, plain, xm = xn | ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(xn,szNzAzT0) | sdtlseqdt0(xm,X0) | ~sdtlseqdt0(xn,X0), inference(resolution, [status(thm)], [c104,d22])). % 39.75/11.11 cnf(d24, plain, xm = xn | ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(xm,X0) | ~sdtlseqdt0(xn,X0), inference(resolution, [status(thm)], [c105,d23])). % 39.75/11.11 cnf(d25, plain, xm = xn | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | sdtlseqdt0(xm,szszuzczcdt0(xn)) | ~aElementOf0(xn,szNzAzT0), inference(resolution, [status(thm)], [d24,c65])). % 39.75/11.11 cnf(d26, plain, xm = xn | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | sdtlseqdt0(xm,szszuzczcdt0(xn)), inference(resolution, [status(thm)], [c105,d25])). % 39.75/11.11 cnf(d27, plain, xm = xn | sdtlseqdt0(xm,szszuzczcdt0(xn)) | ~aElementOf0(xn,szNzAzT0), inference(resolution, [status(thm)], [d26,c55])). % 39.75/11.11 cnf(d28, plain, xm = xn | sdtlseqdt0(xm,szszuzczcdt0(xn)), inference(resolution, [status(thm)], [c105,d27])). % 39.75/11.11 cnf(d29, plain, xm = xn | szszuzczcdt0(xn) = xm | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | ~aElementOf0(xm,szNzAzT0) | ~sdtlseqdt0(szszuzczcdt0(xn),xm), inference(resolution, [status(thm)], [d28,c67])). % 39.75/11.11 cnf(d30, plain, szszuzczcdt0(xn) = xm | xm = xn | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | ~sdtlseqdt0(szszuzczcdt0(xn),xm), inference(resolution, [status(thm)], [c104,d29])). % 39.75/11.11 cnf(d31, plain, ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(X1,szNzAzT0) | sdtlseqdt0(X0,X1) | X0 = szszuzczcdt0(X1) | ~aElementOf0(X0,szNzAzT0) | ~aElementOf0(szszuzczcdt0(X1),szNzAzT0) | ~sdtlseqdt0(X0,szszuzczcdt0(X1)), inference(resolution, [status(thm)], [c69,c67])). % 39.75/11.11 cnf(d32, plain, xm = xn | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | aElementOf0(xm,slbdtrb0(xn)) | szszuzczcdt0(xm) = szszuzczcdt0(xn) | ~aElementOf0(xn,szNzAzT0) | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | sdtlseqdt0(szszuzczcdt0(xm),xn), inference(resolution, [status(thm)], [d6,d31])). % 39.75/11.11 cnf(d33, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | aElementOf0(xm,slbdtrb0(xn)) | sdtlseqdt0(szszuzczcdt0(xm),xn), inference(resolution, [status(thm)], [c105,d32])). % 39.75/11.11 cnf(d34, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | aElementOf0(xm,slbdtrb0(xn)) | sdtlseqdt0(szszuzczcdt0(xm),xn) | ~aElementOf0(xn,szNzAzT0), inference(resolution, [status(thm)], [d33,c55])). % 39.75/11.11 cnf(d35, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0) | aElementOf0(xm,slbdtrb0(xn)) | sdtlseqdt0(szszuzczcdt0(xm),xn), inference(resolution, [status(thm)], [c105,d34])). % 39.75/11.11 cnf(d36, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | aElementOf0(xm,slbdtrb0(xn)) | sdtlseqdt0(szszuzczcdt0(xm),xn) | ~aElementOf0(xm,szNzAzT0), inference(resolution, [status(thm)], [d35,c55])). % 39.75/11.11 cnf(d37, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | aElementOf0(xm,slbdtrb0(xn)) | sdtlseqdt0(szszuzczcdt0(xm),xn), inference(resolution, [status(thm)], [c104,d36])). % 39.75/11.11 cnf(d38, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | aElementOf0(xm,slbdtrb0(xn)) | aElementOf0(xm,X0) | ~aElementOf0(xm,szNzAzT0) | ~'Ts93'(xn,X0), inference(resolution, [status(thm)], [d37,c95])). % 39.75/11.11 cnf(d39, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | aElementOf0(xm,X0) | aElementOf0(xm,slbdtrb0(xn)) | ~'Ts93'(xn,X0), inference(resolution, [status(thm)], [c104,d38])). % 39.75/11.11 cnf(d40, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | aElementOf0(xm,slbdtrb0(xn)) | aElementOf0(xm,slbdtrb0(xn)) | ~aElementOf0(xn,szNzAzT0), inference(resolution, [status(thm)], [d39,d0])). % 39.75/11.11 cnf(d41, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | aElementOf0(xm,slbdtrb0(xn)), inference(resolution, [status(thm)], [c105,d40])). % 39.75/11.11 cnf(d42, plain, aElementOf0(X0,X1) | ~aElementOf0(X0,szNzAzT0) | ~'Ts93'(X2,X1) | ~aElementOf0(X2,szNzAzT0) | ~aElementOf0(X0,szNzAzT0) | sdtlseqdt0(X2,X0), inference(resolution, [status(thm)], [c95,c69])). % 39.75/11.11 cnf(d43, plain, ~aElementOf0(X0,szNzAzT0) | aElementOf0(X1,slbdtrb0(X0)) | ~aElementOf0(X1,szNzAzT0) | sdtlseqdt0(X0,X1) | ~aElementOf0(X0,szNzAzT0), inference(resolution, [status(thm)], [d42,d0])). % 39.75/11.11 cnf(d44, plain, ~aElementOf0(xm,szNzAzT0) | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | sdtlseqdt0(szszuzczcdt0(xn),xm) | ~aElementOf0(xm,slbdtrb0(xn)), inference(resolution, [status(thm)], [d43,c108])). % 39.75/11.11 cnf(d45, plain, ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | ~aElementOf0(xm,slbdtrb0(xn)) | sdtlseqdt0(szszuzczcdt0(xn),xm), inference(resolution, [status(thm)], [c104,d44])). % 39.75/11.11 cnf(d46, plain, ~aElementOf0(szszuzczcdt0(xn),szNzAzT0) | sdtlseqdt0(szszuzczcdt0(xn),xm) | szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn, inference(resolution, [status(thm)], [d45,d41])). % 39.75/11.11 cnf(d47, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | sdtlseqdt0(szszuzczcdt0(xn),xm) | ~aElementOf0(xn,szNzAzT0), inference(resolution, [status(thm)], [d46,c55])). % 39.75/11.11 cnf(d48, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | sdtlseqdt0(szszuzczcdt0(xn),xm), inference(resolution, [status(thm)], [c105,d47])). % 39.75/11.11 cnf(d49, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | xm = xn | szszuzczcdt0(xn) = xm | xm = xn | ~aElementOf0(szszuzczcdt0(xn),szNzAzT0), inference(resolution, [status(thm)], [d48,d30])). % 39.75/11.11 cnf(d50, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | szszuzczcdt0(xn) = xm | xm = xn | ~aElementOf0(xn,szNzAzT0), inference(resolution, [status(thm)], [d49,c55])). % 39.75/11.11 cnf(d51, plain, szszuzczcdt0(xm) = szszuzczcdt0(xn) | szszuzczcdt0(xn) = xm | xm = xn, inference(resolution, [status(thm)], [c105,d50])). % 39.75/11.11 cnf(d52, plain, sdtlseqdt0(szszuzczcdt0(xn),szszuzczcdt0(xm)) | ~aElementOf0(xn,szNzAzT0) | szszuzczcdt0(xn) = xm | xm = xn, inference(superposition, [status(thm)], [d51,d1])). % 39.75/11.11 cnf(d53, plain, szszuzczcdt0(xn) = xm | xm = xn | sdtlseqdt0(szszuzczcdt0(xn),szszuzczcdt0(xm)), inference(resolution, [status(thm)], [c105,d52])). % 39.75/11.11 cnf(d54, plain, szszuzczcdt0(xn) = xm | xm = xn | ~aElementOf0(xn,szNzAzT0) | ~aElementOf0(xm,szNzAzT0) | sdtlseqdt0(xn,xm), inference(resolution, [status(thm)], [d53,c64])). % 39.75/11.11 cnf(d55, plain, szszuzczcdt0(xn) = xm | xm = xn | ~aElementOf0(xn,szNzAzT0) | sdtlseqdt0(xn,xm), inference(resolution, [status(thm)], [c104,d54])). % 39.75/11.11 cnf(d56, plain, szszuzczcdt0(xn) = xm | xm = xn | sdtlseqdt0(xn,xm), inference(resolution, [status(thm)], [c105,d55])). % 39.75/11.11 cnf(d57, plain, szszuzczcdt0(xn) = xm | xm = xn | xm = xn | xn = xm, inference(resolution, [status(thm)], [d56,d21])). % 39.75/11.11 cnf(d58, plain, sdtlseqdt0(xn,xm) | ~aElementOf0(xn,szNzAzT0) | xm = xn | xn = xm, inference(superposition, [status(thm)], [d57,c65])). % 39.75/11.11 cnf(d59, plain, xm = xn | xn = xm | sdtlseqdt0(xn,xm), inference(resolution, [status(thm)], [c105,d58])). % 39.75/11.11 cnf(d60, plain, xm = xn | xn = xm | xm = xn | xn = xm, inference(resolution, [status(thm)], [d59,d21])). % 39.75/11.11 cnf(d61, plain, xm != xm | xn = xm, inference(equality_factoring, [status(thm)], [d60])). % 39.75/11.11 cnf(d62, plain, xn = xm, inference(equality_resolution, [status(thm)], [d61])). % 39.75/11.11 cnf(d63, plain, xm != xm | ~aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))), inference(demodulation, [status(thm)], [c110,d62])). % 39.75/11.11 cnf(d64, plain, xm != xm | ~aElementOf0(xm,slbdtrb0(szszuzczcdt0(xm))), inference(demodulation, [status(thm)], [d63,d62])). % 39.75/11.11 cnf(d65, plain, ~aElementOf0(xm,slbdtrb0(szszuzczcdt0(xm))), inference(equality_resolution, [status(thm)], [d64])). % 39.75/11.11 cnf(d66, plain, ~aElementOf0(xm,szNzAzT0) | ~aElementOf0(szszuzczcdt0(xm),szNzAzT0), inference(resolution, [status(thm)], [d65,d3])). % 39.75/11.11 cnf(d67, plain, ~aElementOf0(szszuzczcdt0(xm),szNzAzT0), inference(resolution, [status(thm)], [c104,d66])). % 39.75/11.11 cnf(d68, plain, ~aElementOf0(xm,szNzAzT0), inference(resolution, [status(thm)], [d67,c55])). % 39.75/11.11 cnf(d69, plain, $false, inference(resolution, [status(thm)], [c104,d68])). % 39.75/11.11 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------