%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : NUM540+1 : 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 : n007.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 14.17s 2.60s % Output : CNFRefutation 14.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM540+1 : 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.36 % Computer : n007.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 26 03:07:23 UTC 2026 % 0.13/0.36 % CPUTime : % 0.13/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 14.17/2.60 % SZS status Theorem for theBenchmark.p % 14.17/2.60 % SZS output start CNFRefutation for theBenchmark.p % 14.17/2.60 fof(mDefEmp, definition, ! [X0] : ((X0 = slcrc0 <=> (aSet0(X0) & ~? [X1] : aElementOf0(X1,X0))))). % 14.17/2.60 fof(mZeroNum, axiom, aElementOf0(sz00,szNzAzT0)). % 14.17/2.60 fof(mNoScLessZr, axiom, ! [X0] : ((aElementOf0(X0,szNzAzT0) => ~sdtlseqdt0(szszuzczcdt0(X0),sz00)))). % 14.17/2.60 fof(mDefSeg, definition, ! [X0] : ((aElementOf0(X0,szNzAzT0) => ! [X1] : ((X1 = slbdtrb0(X0) <=> (aSet0(X1) & ! [X2] : ((aElementOf0(X2,X1) <=> (aElementOf0(X2,szNzAzT0) & sdtlseqdt0(szszuzczcdt0(X2),X0)))))))))). % 14.17/2.60 fof(m__, conjecture, slbdtrb0(sz00) = slcrc0). % 14.17/2.60 fof(negated_conjecture, negated_conjecture, slbdtrb0(sz00) != slcrc0, inference(negate_conjecture, [status(cth)], [m__])). % 14.17/2.60 cnf(c1, plain, X0 != slcrc0 | aSet0(X0), inference(clausification, [status(esa)], [mDefEmp])). % 14.17/2.60 cnf(c2, plain, X0 != slcrc0 | ~aElementOf0(X1,X0), inference(clausification, [status(esa)], [mDefEmp])). % 14.17/2.60 cnf(c54, plain, aElementOf0(sz00,szNzAzT0), inference(clausification, [status(esa)], [mZeroNum])). % 14.17/2.60 cnf(c62, plain, ~aElementOf0(X0,szNzAzT0) | ~sdtlseqdt0(szszuzczcdt0(X0),sz00), inference(clausification, [status(esa)], [mNoScLessZr])). % 14.17/2.60 cnf(c91, plain, ~aElementOf0(X0,szNzAzT0) | X1 = slbdtrb0(X0) | ~X2(X0,X1), inference(clausification, [status(esa)], [mDefSeg])). % 14.17/2.60 cnf(c97, plain, X0(X1,X2) | ~aSet0(X2) | aElementOf0(sK97(X1,X2),X2) | aElementOf0(sK97(X1,X2),szNzAzT0), inference(clausification, [status(esa)], [mDefSeg])). % 14.17/2.60 cnf(c98, plain, X0(X1,X2) | ~aSet0(X2) | aElementOf0(sK97(X1,X2),X2) | sdtlseqdt0(szszuzczcdt0(sK97(X1,X2)),X1), inference(clausification, [status(esa)], [mDefSeg])). % 14.17/2.60 cnf(c103, plain, slbdtrb0(sz00) != slcrc0, inference(clausification, [status(esa)], [negated_conjecture])). % 14.17/2.60 cnf(d0, plain, ~aElementOf0(X0,slcrc0), inference(equality_resolution, [status(thm)], [c2])). % 14.17/2.60 cnf(d1, plain, ~aSet0(slcrc0) | aElementOf0(sK97(X0,slcrc0),szNzAzT0) | 'Ts93'(X0,slcrc0), inference(resolution, [status(thm)], [c97,d0])). % 14.17/2.60 cnf(d2, plain, aSet0(slcrc0), inference(equality_resolution, [status(thm)], [c1])). % 14.17/2.60 cnf(d3, plain, aElementOf0(sK97(X0,slcrc0),szNzAzT0) | 'Ts93'(X0,slcrc0), inference(resolution, [status(thm)], [d2,d1])). % 14.17/2.60 cnf(d4, plain, ~aSet0(slcrc0) | sdtlseqdt0(szszuzczcdt0(sK97(X0,slcrc0)),X0) | 'Ts93'(X0,slcrc0), inference(resolution, [status(thm)], [c98,d0])). % 14.17/2.60 cnf(d5, plain, sdtlseqdt0(szszuzczcdt0(sK97(X0,slcrc0)),X0) | 'Ts93'(X0,slcrc0), inference(resolution, [status(thm)], [d2,d4])). % 14.17/2.60 cnf(d6, plain, 'Ts93'(sz00,slcrc0) | ~aElementOf0(sK97(sz00,slcrc0),szNzAzT0), inference(resolution, [status(thm)], [d5,c62])). % 14.17/2.60 cnf(d7, plain, 'Ts93'(sz00,slcrc0) | 'Ts93'(sz00,slcrc0), inference(resolution, [status(thm)], [d6,d3])). % 14.17/2.60 cnf(d8, plain, slcrc0 = slbdtrb0(sz00) | ~aElementOf0(sz00,szNzAzT0), inference(resolution, [status(thm)], [d7,c91])). % 14.17/2.60 cnf(d9, plain, slcrc0 = slbdtrb0(sz00), inference(resolution, [status(thm)], [c54,d8])). % 14.17/2.60 cnf(d10, plain, slcrc0 != slcrc0, inference(demodulation, [status(thm)], [c103,d9])). % 14.17/2.60 cnf(d11, plain, $false, inference(equality_resolution, [status(thm)], [d10])). % 14.17/2.60 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------