%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : SWC181+1 : TPTP v9.3.1. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n001.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:54:32 AM UTC 2026 % Result : Theorem 41.09s 10.16s % Output : CNFRefutation 41.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : SWC181+1 : TPTP v9.3.1. Released v2.4.0. % 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.09/0.35 % Computer : n001.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 12:32:12 UTC 2026 % 0.09/0.35 % CPUTime : % 0.09/0.35 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 41.09/10.16 % SZS status Theorem for theBenchmark.p % 41.09/10.16 % SZS output start CNFRefutation for theBenchmark.p % 41.09/10.16 fof(ax12, axiom, ! [X0] : ((ssList(X0) => (strictorderedP(X0) <=> ! [X1] : ((ssItem(X1) => ! [X2] : ((ssItem(X2) => ! [X3] : ((ssList(X3) => ! [X4] : ((ssList(X4) => ! [X5] : ((ssList(X5) => (app(app(X3,cons(X1,X4)),cons(X2,X5)) = X0 => lt(X1,X2)))))))))))))))). % 41.09/10.16 fof(ax13, axiom, ! [X0] : ((ssList(X0) => (duplicatefreeP(X0) <=> ! [X1] : ((ssItem(X1) => ! [X2] : ((ssItem(X2) => ! [X3] : ((ssList(X3) => ! [X4] : ((ssList(X4) => ! [X5] : ((ssList(X5) => (app(app(X3,cons(X1,X4)),cons(X2,X5)) = X0 => X1 != X2))))))))))))))). % 41.09/10.16 fof(ax90, axiom, ! [X0] : ((ssItem(X0) => ~lt(X0,X0)))). % 41.09/10.16 fof(co1, conjecture, ! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ! [X2] : ((ssList(X2) => ! [X3] : ((ssList(X3) => (X1 != X3 | (X0 != X2 | (! [X4] : ((ssList(X4) => ! [X5] : ((ssList(X5) => (app(app(X4,X2),X5) != X3 | (~strictorderedP(X2) | (? [X6] : ((ssItem(X6) & ? [X7] : ((ssList(X7) & (app(X7,cons(X6,nil)) = X4 & ? [X8] : ((ssItem(X8) & ? [X9] : ((ssList(X9) & (app(cons(X8,nil),X9) = X2 & lt(X6,X8))))))))))) | ? [X10] : ((ssItem(X10) & ? [X11] : ((ssList(X11) & (app(cons(X10,nil),X11) = X5 & ? [X12] : ((ssItem(X12) & ? [X13] : ((ssList(X13) & (app(X13,cons(X12,nil)) = X2 & lt(X12,X10)))))))))))))))))) | (duplicatefreeP(X0) | (nil != X3 & nil = X2)))))))))))))). % 41.09/10.16 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((ssList(X0) => ! [X1] : ((ssList(X1) => ! [X2] : ((ssList(X2) => ! [X3] : ((ssList(X3) => (X1 != X3 | (X0 != X2 | (! [X4] : ((ssList(X4) => ! [X5] : ((ssList(X5) => (app(app(X4,X2),X5) != X3 | (~strictorderedP(X2) | (? [X6] : ((ssItem(X6) & ? [X7] : ((ssList(X7) & (app(X7,cons(X6,nil)) = X4 & ? [X8] : ((ssItem(X8) & ? [X9] : ((ssList(X9) & (app(cons(X8,nil),X9) = X2 & lt(X6,X8))))))))))) | ? [X10] : ((ssItem(X10) & ? [X11] : ((ssList(X11) & (app(cons(X10,nil),X11) = X5 & ? [X12] : ((ssItem(X12) & ? [X13] : ((ssList(X13) & (app(X13,cons(X12,nil)) = X2 & lt(X12,X10)))))))))))))))))) | (duplicatefreeP(X0) | (nil != X3 & nil = X2))))))))))))), inference(negate_conjecture, [status(cth)], [co1])). % 41.09/10.16 cnf(c61, plain, ~ssList(X0) | ~strictorderedP(X1) | lt(X2,X3) | ~ssItem(X2) | app(app(X0,cons(X2,X4)),cons(X3,X5)) != X1 | ~ssList(X5) | ~ssList(X1) | ~ssList(X4) | ~ssItem(X3), inference(clausification, [status(esa)], [ax12])). % 41.09/10.16 cnf(c71, plain, ~ssList(X0) | duplicatefreeP(X0) | X1(X0), inference(clausification, [status(esa)], [ax13])). % 41.09/10.16 cnf(c72, plain, ~X0(X1) | ssItem(sK94(X1)), inference(clausification, [status(esa)], [ax13])). % 41.09/10.16 cnf(c74, plain, ~X0(X1) | ssList(sK96(X1)), inference(clausification, [status(esa)], [ax13])). % 41.09/10.16 cnf(c75, plain, ~X0(X1) | ssList(sK97(X1)), inference(clausification, [status(esa)], [ax13])). % 41.09/10.16 cnf(c76, plain, ~X0(X1) | ssList(sK98(X1)), inference(clausification, [status(esa)], [ax13])). % 41.09/10.16 cnf(c77, plain, ~X0(X1) | sK95(X1) = sK94(X1), inference(clausification, [status(esa)], [ax13])). % 41.09/10.16 cnf(c78, plain, ~X0(X1) | app(app(sK96(X1),cons(sK94(X1),sK97(X1))),cons(sK95(X1),sK98(X1))) = X1, inference(clausification, [status(esa)], [ax13])). % 41.09/10.16 cnf(c191, plain, ~ssItem(X0) | ~lt(X0,X0), inference(clausification, [status(esa)], [ax90])). % 41.09/10.16 cnf(c199, plain, ssList(sK253), inference(clausification, [status(esa)], [negated_conjecture])). % 41.09/10.16 cnf(c203, plain, sK255 = sK253, inference(clausification, [status(esa)], [negated_conjecture])). % 41.09/10.16 cnf(c204, plain, ~duplicatefreeP(sK253), inference(clausification, [status(esa)], [negated_conjecture])). % 41.09/10.16 cnf(c208, plain, strictorderedP(sK255), inference(clausification, [status(esa)], [negated_conjecture])). % 41.09/10.16 cnf(d0, plain, duplicatefreeP(sK253) | 'Ts87'(sK253), inference(resolution, [status(thm)], [c71,c199])). % 41.09/10.16 cnf(d1, plain, 'Ts87'(sK253), inference(resolution, [status(thm)], [c204,d0])). % 41.09/10.16 cnf(d2, plain, sK95(sK253) = sK94(sK253), inference(resolution, [status(thm)], [c77,d1])). % 41.09/10.16 cnf(d3, plain, app(app(sK96(sK253),cons(sK94(sK253),sK97(sK253))),cons(sK95(sK253),sK98(sK253))) = sK253, inference(resolution, [status(thm)], [c78,d1])). % 41.09/10.16 cnf(d4, plain, app(app(sK96(sK253),cons(sK94(sK253),sK97(sK253))),cons(sK94(sK253),sK98(sK253))) = sK253, inference(demodulation, [status(thm)], [d3,d2])). % 41.09/10.16 cnf(d5, plain, sK253 != X0 | ~ssItem(sK94(sK253)) | ~ssItem(sK94(sK253)) | ~ssList(sK97(sK253)) | ~ssList(sK98(sK253)) | ~ssList(sK96(sK253)) | ~ssList(X0) | lt(sK94(sK253),sK94(sK253)) | ~strictorderedP(X0), inference(superposition, [status(thm)], [d4,c61])). % 41.09/10.16 cnf(d6, plain, ~ssItem(sK94(sK253)) | ~ssList(sK253) | ~ssList(sK96(sK253)) | ~ssList(sK97(sK253)) | ~ssList(sK98(sK253)) | lt(sK94(sK253),sK94(sK253)) | ~strictorderedP(sK253), inference(equality_resolution, [status(thm)], [d5])). % 41.09/10.16 cnf(d7, plain, ~ssItem(sK94(sK253)) | ~ssList(sK96(sK253)) | ~ssList(sK97(sK253)) | ~ssList(sK98(sK253)) | lt(sK94(sK253),sK94(sK253)) | ~strictorderedP(sK253), inference(resolution, [status(thm)], [c199,d6])). % 41.09/10.16 cnf(d8, plain, strictorderedP(sK253), inference(demodulation, [status(thm)], [c208,c203])). % 41.09/10.16 cnf(d9, plain, ~ssItem(sK94(sK253)) | ~ssList(sK96(sK253)) | ~ssList(sK97(sK253)) | ~ssList(sK98(sK253)) | lt(sK94(sK253),sK94(sK253)), inference(resolution, [status(thm)], [d8,d7])). % 41.09/10.16 cnf(d10, plain, ~ssItem(sK94(sK253)) | ~ssList(sK96(sK253)) | ~ssList(sK97(sK253)) | ~ssList(sK98(sK253)) | ~ssItem(sK94(sK253)), inference(resolution, [status(thm)], [d9,c191])). % 41.09/10.16 cnf(d11, plain, ~ssItem(sK94(sK253)) | ~ssList(sK96(sK253)) | ~ssList(sK97(sK253)) | ~'Ts87'(sK253), inference(resolution, [status(thm)], [d10,c76])). % 41.09/10.16 cnf(d12, plain, ~ssItem(sK94(sK253)) | ~ssList(sK96(sK253)) | ~ssList(sK97(sK253)), inference(resolution, [status(thm)], [d1,d11])). % 41.09/10.16 cnf(d13, plain, ~ssItem(sK94(sK253)) | ~ssList(sK96(sK253)) | ~'Ts87'(sK253), inference(resolution, [status(thm)], [d12,c75])). % 41.09/10.16 cnf(d14, plain, ~ssItem(sK94(sK253)) | ~ssList(sK96(sK253)), inference(resolution, [status(thm)], [d1,d13])). % 41.09/10.16 cnf(d15, plain, ~ssItem(sK94(sK253)) | ~'Ts87'(sK253), inference(resolution, [status(thm)], [d14,c74])). % 41.09/10.16 cnf(d16, plain, ~ssItem(sK94(sK253)), inference(resolution, [status(thm)], [d1,d15])). % 41.09/10.16 cnf(d17, plain, ~'Ts87'(sK253), inference(resolution, [status(thm)], [d16,c72])). % 41.09/10.16 cnf(d18, plain, $false, inference(resolution, [status(thm)], [d1,d17])). % 41.09/10.16 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------