%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LAT387+4 : 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 : n009.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 07:48:35 AM UTC 2026 % Result : Theorem 58.47s 7.88s % Output : CNFRefutation 58.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LAT387+4 : 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.09/0.35 % Computer : n009.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 : Fri Sep 25 21:39:29 UTC 2026 % 0.09/0.35 % CPUTime : % 0.09/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 58.47/7.88 % SZS status Theorem for theBenchmark.p % 58.47/7.88 % SZS output start CNFRefutation for theBenchmark.p % 58.47/7.88 fof(mEOfElem, axiom, ! [X0] : ((aSet0(X0) => ! [X1] : ((aElementOf0(X1,X0) => aElement0(X1)))))). % 58.47/7.88 fof(mARefl, axiom, ! [X0] : ((aElement0(X0) => sdtlseqdt0(X0,X0)))). % 58.47/7.88 fof(mASymm, axiom, ! [X0] : ! [X1] : (((aElement0(X0) & aElement0(X1)) => ((sdtlseqdt0(X0,X1) & sdtlseqdt0(X1,X0)) => X0 = X1)))). % 58.47/7.88 fof(mImgSort, axiom, ! [X0] : ((aFunction0(X0) => ! [X1] : ((aElementOf0(X1,szDzozmdt0(X0)) => aElementOf0(sdtlpdtrp0(X0,X1),szRzazndt0(X0))))))). % 58.47/7.88 fof(m__1123, hypothesis, (aSet0(xU) & (! [X0] : ((((aSet0(X0) & ! [X1] : ((aElementOf0(X1,X0) => aElementOf0(X1,xU)))) | aSubsetOf0(X0,xU)) => ? [X1] : ((aElementOf0(X1,xU) & (aElementOf0(X1,xU) & (! [X2] : ((aElementOf0(X2,X0) => sdtlseqdt0(X1,X2))) & (aLowerBoundOfIn0(X1,X0,xU) & (! [X2] : ((((aElementOf0(X2,xU) & ! [X3] : ((aElementOf0(X3,X0) => sdtlseqdt0(X2,X3)))) | aLowerBoundOfIn0(X2,X0,xU)) => sdtlseqdt0(X2,X1))) & (aInfimumOfIn0(X1,X0,xU) & ? [X2] : ((aElementOf0(X2,xU) & (aElementOf0(X2,xU) & (! [X3] : ((aElementOf0(X3,X0) => sdtlseqdt0(X3,X2))) & (aUpperBoundOfIn0(X2,X0,xU) & (! [X3] : ((((aElementOf0(X3,xU) & ! [X4] : ((aElementOf0(X4,X0) => sdtlseqdt0(X4,X3)))) | aUpperBoundOfIn0(X3,X0,xU)) => sdtlseqdt0(X2,X3))) & aSupremumOfIn0(X2,X0,xU)))))))))))))))) & (aCompleteLattice0(xU) & (aFunction0(xf) & (! [X0] : ! [X1] : (((aElementOf0(X0,szDzozmdt0(xf)) & aElementOf0(X1,szDzozmdt0(xf))) => (sdtlseqdt0(X0,X1) => sdtlseqdt0(sdtlpdtrp0(xf,X0),sdtlpdtrp0(xf,X1))))) & (isMonotone0(xf) & (szDzozmdt0(xf) = szRzazndt0(xf) & (szRzazndt0(xf) = xU & isOn0(xf,xU)))))))))). % 58.47/7.88 fof(m__1144, hypothesis, (aSet0(xS) & (! [X0] : (((aElementOf0(X0,xS) => (aElementOf0(X0,szDzozmdt0(xf)) & (sdtlpdtrp0(xf,X0) = X0 & aFixedPointOf0(X0,xf)))) & (((aElementOf0(X0,szDzozmdt0(xf)) & sdtlpdtrp0(xf,X0) = X0) | aFixedPointOf0(X0,xf)) => aElementOf0(X0,xS)))) & xS = cS1142(xf)))). % 58.47/7.88 fof(m__1173, hypothesis, (aSet0(xT) & (! [X0] : ((aElementOf0(X0,xT) => aElementOf0(X0,xS))) & aSubsetOf0(xT,xS)))). % 58.47/7.88 fof(m__1244, hypothesis, (aSet0(xP) & (! [X0] : (((aElementOf0(X0,xP) => (aElementOf0(X0,xU) & (sdtlseqdt0(sdtlpdtrp0(xf,X0),X0) & (! [X1] : ((aElementOf0(X1,xT) => sdtlseqdt0(X1,X0))) & aUpperBoundOfIn0(X0,xT,xU))))) & ((aElementOf0(X0,xU) & (sdtlseqdt0(sdtlpdtrp0(xf,X0),X0) & (! [X1] : ((aElementOf0(X1,xT) => sdtlseqdt0(X1,X0))) | aUpperBoundOfIn0(X0,xT,xU)))) => aElementOf0(X0,xP)))) & xP = cS1241(xU,xf,xT)))). % 58.47/7.88 fof(m__1261, hypothesis, (aElementOf0(xp,xU) & (aElementOf0(xp,xU) & (! [X0] : ((aElementOf0(X0,xP) => sdtlseqdt0(xp,X0))) & (aLowerBoundOfIn0(xp,xP,xU) & (! [X0] : ((((aElementOf0(X0,xU) & ! [X1] : ((aElementOf0(X1,xP) => sdtlseqdt0(X0,X1)))) | aLowerBoundOfIn0(X0,xP,xU)) => sdtlseqdt0(X0,xp))) & aInfimumOfIn0(xp,xP,xU))))))). % 58.47/7.88 fof(m__1299, hypothesis, (! [X0] : ((aElementOf0(X0,xP) => sdtlseqdt0(sdtlpdtrp0(xf,xp),X0))) & (aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU) & (! [X0] : ((aElementOf0(X0,xT) => sdtlseqdt0(X0,sdtlpdtrp0(xf,xp)))) & aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU))))). % 58.47/7.88 fof(m__, conjecture, (((aElementOf0(xp,szDzozmdt0(xf)) & sdtlpdtrp0(xf,xp) = xp) | aFixedPointOf0(xp,xf)) & (((! [X0] : ((aElementOf0(X0,xT) => sdtlseqdt0(X0,xp))) | aUpperBoundOfIn0(xp,xT,xS)) & ! [X0] : (((aElementOf0(X0,xS) & (! [X1] : ((aElementOf0(X1,xT) => sdtlseqdt0(X1,X0))) & aUpperBoundOfIn0(X0,xT,xS))) => sdtlseqdt0(xp,X0)))) | aSupremumOfIn0(xp,xT,xS)))). % 58.47/7.88 fof(negated_conjecture, negated_conjecture, ~((((aElementOf0(xp,szDzozmdt0(xf)) & sdtlpdtrp0(xf,xp) = xp) | aFixedPointOf0(xp,xf)) & (((! [X0] : ((aElementOf0(X0,xT) => sdtlseqdt0(X0,xp))) | aUpperBoundOfIn0(xp,xT,xS)) & ! [X0] : (((aElementOf0(X0,xS) & (! [X1] : ((aElementOf0(X1,xT) => sdtlseqdt0(X1,X0))) & aUpperBoundOfIn0(X0,xT,xS))) => sdtlseqdt0(xp,X0)))) | aSupremumOfIn0(xp,xT,xS)))), inference(negate_conjecture, [status(cth)], [m__])). % 58.47/7.88 cnf(c0, plain, ~aSet0(X0) | ~aElementOf0(X1,X0) | aElement0(X1), inference(clausification, [status(esa)], [mEOfElem])). % 58.47/7.88 cnf(c7, plain, ~aElement0(X0) | sdtlseqdt0(X0,X0), inference(clausification, [status(esa)], [mARefl])). % 58.47/7.88 cnf(c8, plain, X0 = X1 | ~aElement0(X1) | ~aElement0(X0) | ~sdtlseqdt0(X0,X1) | ~sdtlseqdt0(X1,X0), inference(clausification, [status(esa)], [mASymm])). % 58.47/7.88 cnf(c42, plain, ~aFunction0(X0) | ~aElementOf0(X1,szDzozmdt0(X0)) | aElementOf0(sdtlpdtrp0(X0,X1),szRzazndt0(X0)), inference(clausification, [status(esa)], [mImgSort])). % 58.47/7.88 cnf(c52, plain, aSet0(xU), inference(clausification, [status(esa)], [m__1123])). % 58.47/7.88 cnf(c54, plain, ~aElementOf0(X0,szDzozmdt0(xf)) | ~aElementOf0(X1,szDzozmdt0(xf)) | sdtlseqdt0(sdtlpdtrp0(xf,X1),sdtlpdtrp0(xf,X0)) | ~sdtlseqdt0(X1,X0), inference(clausification, [status(esa)], [m__1123])). % 58.47/7.88 cnf(c55, plain, szRzazndt0(xf) = szDzozmdt0(xf), inference(clausification, [status(esa)], [m__1123])). % 58.47/7.88 cnf(c57, plain, szRzazndt0(xf) = xU, inference(clausification, [status(esa)], [m__1123])). % 58.47/7.88 cnf(c59, plain, aFunction0(xf), inference(clausification, [status(esa)], [m__1123])). % 58.47/7.88 cnf(c77, plain, aSet0(xS), inference(clausification, [status(esa)], [m__1144])). % 58.47/7.88 cnf(c79, plain, ~aElementOf0(X0,xS) | aElementOf0(X0,szDzozmdt0(xf)), inference(clausification, [status(esa)], [m__1144])). % 58.47/7.88 cnf(c81, plain, ~aElementOf0(X0,xS) | sdtlpdtrp0(xf,X0) = X0, inference(clausification, [status(esa)], [m__1144])). % 58.47/7.88 cnf(c86, plain, ~aElementOf0(X0,xT) | aElementOf0(X0,xS), inference(clausification, [status(esa)], [m__1173])). % 58.47/7.88 cnf(c90, plain, ~aElementOf0(X0,xP) | ~aElementOf0(X1,xT) | sdtlseqdt0(X1,X0), inference(clausification, [status(esa)], [m__1244])). % 58.47/7.88 cnf(c93, plain, ~sdtlseqdt0(sdtlpdtrp0(xf,X0),X0) | aElementOf0(sK83(X0),xT) | ~aElementOf0(X0,xU) | aElementOf0(X0,xP), inference(clausification, [status(esa)], [m__1244])). % 58.47/7.88 cnf(c94, plain, ~sdtlseqdt0(sdtlpdtrp0(xf,X0),X0) | ~sdtlseqdt0(sK83(X0),X0) | ~aElementOf0(X0,xU) | aElementOf0(X0,xP), inference(clausification, [status(esa)], [m__1244])). % 58.47/7.88 cnf(c95, plain, ~sdtlseqdt0(sdtlpdtrp0(xf,X0),X0) | ~aUpperBoundOfIn0(X0,xT,xU) | ~aElementOf0(X0,xU) | aElementOf0(X0,xP), inference(clausification, [status(esa)], [m__1244])). % 58.47/7.88 cnf(c96, plain, aElementOf0(xp,xU), inference(clausification, [status(esa)], [m__1261])). % 58.47/7.88 cnf(c97, plain, ~aElementOf0(X0,xP) | sdtlseqdt0(xp,X0), inference(clausification, [status(esa)], [m__1261])). % 58.47/7.88 cnf(c98, plain, ~aElementOf0(X0,xU) | aElementOf0(sK86(X0),xP) | sdtlseqdt0(X0,xp), inference(clausification, [status(esa)], [m__1261])). % 58.47/7.88 cnf(c99, plain, ~aElementOf0(X0,xU) | ~sdtlseqdt0(X0,sK86(X0)) | sdtlseqdt0(X0,xp), inference(clausification, [status(esa)], [m__1261])). % 58.47/7.88 cnf(c100, plain, ~aLowerBoundOfIn0(X0,xP,xU) | sdtlseqdt0(X0,xp), inference(clausification, [status(esa)], [m__1261])). % 58.47/7.88 cnf(c105, plain, aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU), inference(clausification, [status(esa)], [m__1299])). % 58.47/7.88 cnf(c106, plain, aLowerBoundOfIn0(sdtlpdtrp0(xf,xp),xP,xU), inference(clausification, [status(esa)], [m__1299])). % 58.47/7.88 cnf(c107, plain, ~aElementOf0(xp,szDzozmdt0(xf)) | sdtlpdtrp0(xf,xp) != xp | X0, inference(clausification, [status(esa)], [negated_conjecture])). % 58.47/7.88 cnf(c109, plain, ~X0 | ~aElementOf0(X1,xT) | sdtlseqdt0(X1,sK91), inference(clausification, [status(esa)], [negated_conjecture])). % 58.47/7.88 cnf(c111, plain, ~X0 | aElementOf0(sK91,xS), inference(clausification, [status(esa)], [negated_conjecture])). % 58.47/7.88 cnf(c112, plain, ~X0 | ~sdtlseqdt0(xp,sK91), inference(clausification, [status(esa)], [negated_conjecture])). % 58.47/7.88 cnf(c113, plain, ~X0 | aElementOf0(sK93,xT) | X1, inference(clausification, [status(esa)], [negated_conjecture])). % 58.47/7.88 cnf(c114, plain, ~X0 | ~sdtlseqdt0(sK93,xp) | X1, inference(clausification, [status(esa)], [negated_conjecture])). % 58.47/7.88 cnf(d0, plain, xU = szDzozmdt0(xf), inference(demodulation, [status(thm)], [c55,c57])). % 58.47/7.88 cnf(d1, plain, sdtlpdtrp0(xf,xp) != xp | ~aElementOf0(xp,xU) | 'Ts90', inference(demodulation, [status(thm)], [c107,d0])). % 58.47/7.88 cnf(d2, plain, sdtlpdtrp0(xf,xp) != xp | 'Ts90', inference(resolution, [status(thm)], [c96,d1])). % 58.47/7.88 cnf(d3, plain, ~aElementOf0(X0,xU) | aElement0(X0), inference(resolution, [status(thm)], [c52,c0])). % 58.47/7.88 cnf(d4, plain, aElement0(xp), inference(resolution, [status(thm)], [d3,c96])). % 58.47/7.88 cnf(d5, plain, X0 = xp | ~aElement0(X0) | ~sdtlseqdt0(xp,X0) | ~sdtlseqdt0(X0,xp), inference(resolution, [status(thm)], [d4,c8])). % 58.47/7.88 cnf(d6, plain, ~aElementOf0(X0,xU) | aElementOf0(sdtlpdtrp0(xf,X0),szRzazndt0(xf)) | ~aFunction0(xf), inference(superposition, [status(thm)], [d0,c42])). % 58.47/7.88 cnf(d7, plain, ~aElementOf0(X0,xU) | aElementOf0(sdtlpdtrp0(xf,X0),xU) | ~aFunction0(xf), inference(demodulation, [status(thm)], [d6,c57])). % 58.47/7.88 cnf(d8, plain, ~aElementOf0(X0,xU) | aElementOf0(sdtlpdtrp0(xf,X0),xU), inference(resolution, [status(thm)], [c59,d7])). % 58.47/7.88 cnf(d9, plain, aElementOf0(sdtlpdtrp0(xf,xp),xU), inference(resolution, [status(thm)], [d8,c96])). % 58.47/7.88 cnf(d10, plain, aElement0(sdtlpdtrp0(xf,xp)), inference(resolution, [status(thm)], [d9,d3])). % 58.47/7.88 cnf(d11, plain, sdtlpdtrp0(xf,xp) = xp | ~sdtlseqdt0(sdtlpdtrp0(xf,xp),xp) | ~sdtlseqdt0(xp,sdtlpdtrp0(xf,xp)), inference(resolution, [status(thm)], [d10,d5])). % 58.47/7.88 cnf(d12, plain, sdtlseqdt0(sdtlpdtrp0(xf,xp),xp), inference(resolution, [status(thm)], [c100,c106])). % 58.47/7.88 cnf(d13, plain, sdtlpdtrp0(xf,xp) = xp | ~sdtlseqdt0(xp,sdtlpdtrp0(xf,xp)), inference(resolution, [status(thm)], [d12,d11])). % 58.47/7.88 cnf(d14, plain, aElementOf0(sdtlpdtrp0(xf,xp),xP) | ~sdtlseqdt0(sdtlpdtrp0(xf,sdtlpdtrp0(xf,xp)),sdtlpdtrp0(xf,xp)) | ~aUpperBoundOfIn0(sdtlpdtrp0(xf,xp),xT,xU), inference(resolution, [status(thm)], [d9,c95])). % 58.47/7.88 cnf(d15, plain, aElementOf0(sdtlpdtrp0(xf,xp),xP) | ~sdtlseqdt0(sdtlpdtrp0(xf,sdtlpdtrp0(xf,xp)),sdtlpdtrp0(xf,xp)), inference(resolution, [status(thm)], [c105,d14])). % 58.47/7.88 cnf(d16, plain, ~aElementOf0(X0,xU) | ~aElementOf0(X1,szDzozmdt0(xf)) | ~sdtlseqdt0(X1,X0) | sdtlseqdt0(sdtlpdtrp0(xf,X1),sdtlpdtrp0(xf,X0)), inference(demodulation, [status(thm)], [c54,d0])). % 58.47/7.88 cnf(d17, plain, ~aElementOf0(X0,xU) | ~aElementOf0(X1,xU) | ~sdtlseqdt0(X1,X0) | sdtlseqdt0(sdtlpdtrp0(xf,X1),sdtlpdtrp0(xf,X0)), inference(demodulation, [status(thm)], [d16,d0])). % 58.47/7.88 cnf(d18, plain, ~aElementOf0(X0,xU) | ~sdtlseqdt0(X0,xp) | sdtlseqdt0(sdtlpdtrp0(xf,X0),sdtlpdtrp0(xf,xp)), inference(resolution, [status(thm)], [d17,c96])). % 58.47/7.88 cnf(d19, plain, ~sdtlseqdt0(sdtlpdtrp0(xf,xp),xp) | sdtlseqdt0(sdtlpdtrp0(xf,sdtlpdtrp0(xf,xp)),sdtlpdtrp0(xf,xp)), inference(resolution, [status(thm)], [d18,d9])). % 58.47/7.88 cnf(d20, plain, sdtlseqdt0(sdtlpdtrp0(xf,sdtlpdtrp0(xf,xp)),sdtlpdtrp0(xf,xp)), inference(resolution, [status(thm)], [d12,d19])). % 58.47/7.88 cnf(d21, plain, aElementOf0(sdtlpdtrp0(xf,xp),xP), inference(resolution, [status(thm)], [d20,d15])). % 58.47/7.88 cnf(d22, plain, sdtlseqdt0(xp,sdtlpdtrp0(xf,xp)), inference(resolution, [status(thm)], [d21,c97])). % 58.47/7.88 cnf(d23, plain, sdtlpdtrp0(xf,xp) = xp, inference(resolution, [status(thm)], [d22,d13])). % 58.47/7.88 cnf(d24, plain, 'Ts90', inference(resolution, [status(thm)], [d23,d2])). % 58.47/7.88 cnf(d25, plain, ~sdtlseqdt0(sK93,xp) | 'Ts89', inference(resolution, [status(thm)], [d24,c114])). % 58.47/7.88 cnf(d26, plain, aElementOf0(X0,xU) | ~aElementOf0(X0,xS), inference(demodulation, [status(thm)], [c79,d0])). % 58.47/7.88 cnf(d27, plain, aElementOf0(sK93,xT) | 'Ts89', inference(resolution, [status(thm)], [d24,c113])). % 58.47/7.88 cnf(d28, plain, 'Ts89' | aElementOf0(sK93,xS), inference(resolution, [status(thm)], [d27,c86])). % 58.47/7.88 cnf(d29, plain, 'Ts89' | aElementOf0(sK93,xU), inference(resolution, [status(thm)], [d28,d26])). % 58.47/7.88 cnf(d30, plain, 'Ts89' | sdtlseqdt0(sK93,xp) | ~sdtlseqdt0(sK93,sK86(sK93)), inference(resolution, [status(thm)], [d29,c99])). % 58.47/7.88 cnf(d31, plain, 'Ts89' | aElementOf0(sK86(sK93),xP) | sdtlseqdt0(sK93,xp), inference(resolution, [status(thm)], [d29,c98])). % 58.47/7.88 cnf(d32, plain, sdtlseqdt0(sK93,xp) | 'Ts89' | ~aElementOf0(X0,xT) | sdtlseqdt0(X0,sK86(sK93)), inference(resolution, [status(thm)], [d31,c90])). % 58.47/7.88 cnf(d33, plain, sdtlseqdt0(sK93,sK86(sK93)) | sdtlseqdt0(sK93,xp) | 'Ts89' | 'Ts89', inference(resolution, [status(thm)], [d32,d27])). % 58.47/7.88 cnf(d34, plain, sdtlseqdt0(sK93,sK86(sK93)) | 'Ts89' | 'Ts89', inference(resolution, [status(thm)], [d33,d25])). % 58.47/7.88 cnf(d35, plain, 'Ts89' | sdtlseqdt0(sK93,xp) | 'Ts89', inference(resolution, [status(thm)], [d34,d30])). % 58.47/7.88 cnf(d36, plain, 'Ts89' | 'Ts89', inference(resolution, [status(thm)], [d35,d25])). % 58.47/7.88 cnf(d37, plain, aElementOf0(sK91,xS), inference(resolution, [status(thm)], [d36,c111])). % 58.47/7.88 cnf(d38, plain, sdtlpdtrp0(xf,sK91) = sK91, inference(resolution, [status(thm)], [d37,c81])). % 58.47/7.88 cnf(d39, plain, aElementOf0(sK91,xU), inference(resolution, [status(thm)], [d37,d26])). % 58.47/7.88 cnf(d40, plain, aElementOf0(sK91,xP) | ~sdtlseqdt0(sdtlpdtrp0(xf,sK91),sK91) | ~sdtlseqdt0(sK83(sK91),sK91), inference(resolution, [status(thm)], [d39,c94])). % 58.47/7.88 cnf(d41, plain, aElementOf0(sK91,xP) | ~sdtlseqdt0(sK91,sK91) | ~sdtlseqdt0(sK83(sK91),sK91), inference(demodulation, [status(thm)], [d40,d38])). % 58.47/7.88 cnf(d42, plain, ~aElementOf0(X0,xS) | aElement0(X0), inference(resolution, [status(thm)], [c77,c0])). % 58.47/7.88 cnf(d43, plain, aElement0(sK91), inference(resolution, [status(thm)], [d37,d42])). % 58.47/7.88 cnf(d44, plain, sdtlseqdt0(sK91,sK91), inference(resolution, [status(thm)], [d43,c7])). % 58.47/7.88 cnf(d45, plain, aElementOf0(sK91,xP) | ~sdtlseqdt0(sK83(sK91),sK91), inference(resolution, [status(thm)], [d44,d41])). % 58.47/7.88 cnf(d46, plain, ~aElementOf0(X0,xT) | sdtlseqdt0(X0,sK91), inference(resolution, [status(thm)], [d36,c109])). % 58.47/7.88 cnf(d47, plain, aElementOf0(sK91,xP) | aElementOf0(sK83(sK91),xT) | ~sdtlseqdt0(sdtlpdtrp0(xf,sK91),sK91), inference(resolution, [status(thm)], [d39,c93])). % 58.47/7.88 cnf(d48, plain, aElementOf0(sK83(sK91),xT) | aElementOf0(sK91,xP) | ~sdtlseqdt0(sK91,sK91), inference(demodulation, [status(thm)], [d47,d38])). % 58.47/7.88 cnf(d49, plain, aElementOf0(sK83(sK91),xT) | aElementOf0(sK91,xP), inference(resolution, [status(thm)], [d44,d48])). % 58.47/7.88 cnf(d50, plain, aElementOf0(sK91,xP) | sdtlseqdt0(sK83(sK91),sK91), inference(resolution, [status(thm)], [d49,d46])). % 58.47/7.88 cnf(d51, plain, sdtlseqdt0(sK83(sK91),sK91) | sdtlseqdt0(xp,sK91), inference(resolution, [status(thm)], [d50,c97])). % 58.47/7.88 cnf(d52, plain, ~sdtlseqdt0(xp,sK91), inference(resolution, [status(thm)], [d36,c112])). % 58.47/7.88 cnf(d53, plain, sdtlseqdt0(sK83(sK91),sK91), inference(resolution, [status(thm)], [d52,d51])). % 58.47/7.88 cnf(d54, plain, aElementOf0(sK91,xP), inference(resolution, [status(thm)], [d53,d45])). % 58.47/7.88 cnf(d55, plain, sdtlseqdt0(xp,sK91), inference(resolution, [status(thm)], [d54,c97])). % 58.47/7.88 cnf(d56, plain, $false, inference(resolution, [status(thm)], [d52,d55])). % 58.47/7.88 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------