%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LCL668+1.001 : 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 : n010.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:55:07 AM UTC 2026 % Result : Theorem 46.44s 6.39s % Output : CNFRefutation 46.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL668+1.001 : 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.10/0.37 % Computer : n010.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Fri Sep 25 23:09:59 UTC 2026 % 0.10/0.37 % CPUTime : % 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 46.44/6.39 % SZS status Theorem for theBenchmark.p % 46.44/6.39 % SZS output start CNFRefutation for theBenchmark.p % 46.44/6.39 fof(reflexivity, axiom, ! [X0] : r1(X0,X0)). % 46.44/6.39 fof(main, conjecture, ~? [X0] : ~((! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | (~p12(X0) & (~p10(X0) & (~p8(X0) & (~p6(X0) & (~p4(X0) & ~p2(X0)))))))))))))))))) | (! [X1] : ((~r1(X0,X1) | p7(X1))) | (~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~(((~p5(X0) & ~p1(X0)) | (p1(X0) & p5(X0)))))))))))))))))) | (! [X0] : ((~r1(X1,X0) | p6(X0))) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~(((~p4(X0) & ~p5(X0)) | (p5(X0) & p4(X0)))))))))))))))) | (! [X1] : ((~r1(X0,X1) | p5(X1))) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~(((~p3(X0) & ~p4(X0)) | (p4(X0) & p3(X0)))))))))))))) | (! [X0] : ((~r1(X1,X0) | p4(X0))) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~(((~p2(X0) & ~p3(X0)) | (p3(X0) & p2(X0)))))))))))) | (! [X1] : ((~r1(X0,X1) | p3(X1))) | ~! [X1] : ((~r1(X0,X1) | ~~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~(((~p1(X0) & ~p2(X0)) | (p2(X0) & p1(X0)))))))))))))))))))))))))))))))) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | (p6(X0) & (p5(X0) & (p4(X0) & (p3(X0) & (p2(X0) & p1(X0))))))))))))))))))))))). % 46.44/6.39 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ~((! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | (~p12(X0) & (~p10(X0) & (~p8(X0) & (~p6(X0) & (~p4(X0) & ~p2(X0)))))))))))))))))) | (! [X1] : ((~r1(X0,X1) | p7(X1))) | (~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~(((~p5(X0) & ~p1(X0)) | (p1(X0) & p5(X0)))))))))))))))))) | (! [X0] : ((~r1(X1,X0) | p6(X0))) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~(((~p4(X0) & ~p5(X0)) | (p5(X0) & p4(X0)))))))))))))))) | (! [X1] : ((~r1(X0,X1) | p5(X1))) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~(((~p3(X0) & ~p4(X0)) | (p4(X0) & p3(X0)))))))))))))) | (! [X0] : ((~r1(X1,X0) | p4(X0))) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~(((~p2(X0) & ~p3(X0)) | (p3(X0) & p2(X0)))))))))))) | (! [X1] : ((~r1(X0,X1) | p3(X1))) | ~! [X1] : ((~r1(X0,X1) | ~~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~(((~p1(X0) & ~p2(X0)) | (p2(X0) & p1(X0)))))))))))))))))))))))))))))))) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | (p6(X0) & (p5(X0) & (p4(X0) & (p3(X0) & (p2(X0) & p1(X0)))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [main])). % 46.44/6.39 cnf(c0, plain, r1(X0,X0), inference(clausification, [status(esa)], [reflexivity])). % 46.44/6.39 cnf(c10, plain, ~r1(sK5,X0) | X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(c18, plain, ~r1(X0,X1) | ~r1(X2,X3) | p3(X1) | ~X4(X2) | ~r1(X3,X5) | p2(X1) | ~r1(X5,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(c19, plain, ~r1(X0,X1) | ~X2(X0) | ~r1(X1,X3) | ~p2(X4) | ~r1(X3,X5) | ~r1(X5,X4) | ~p3(X4), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(c20, plain, ~X0(X1) | r1(X1,sK24(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(c21, plain, ~X0(X1) | ~p3(sK24(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(c23, plain, ~p2(X0) | ~r1(X1,X0) | ~X2(X3) | ~r1(X4,X5) | ~r1(X3,X4) | ~r1(X5,X1) | ~p1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(c24, plain, ~r1(X0,X1) | p4(X2) | ~r1(X3,X4) | ~r1(X1,X2) | ~r1(X5,X3) | p3(X2) | ~X6(X5) | ~r1(X4,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(c28, plain, ~X0(X1) | ~r1(X1,X2) | X3(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(c30, plain, ~r1(X0,X1) | ~p5(X2) | ~X3(X4) | ~p4(X2) | ~r1(X1,X5) | ~r1(X5,X6) | ~r1(X4,X7) | ~r1(X6,X2) | ~r1(X7,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(c33, plain, ~X0(X1) | ~r1(X1,X2) | X3(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(c34, plain, ~r1(X0,X1) | ~r1(X1,X2) | ~X3(X4) | p1(X5) | ~r1(X4,X0) | ~r1(X6,X5) | ~r1(X2,X7) | ~r1(X8,X6) | ~r1(X7,X8) | p5(X5), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(c38, plain, ~X0(X1) | ~r1(X1,X2) | X3(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 46.44/6.39 cnf(d0, plain, ~'Ts1'(sK5) | 'Ts4'(sK24(sK5)), inference(resolution, [status(thm)], [c20,c10])). % 46.44/6.39 cnf(d1, plain, 'Ts1'(X0) | ~'Ts2'(X0), inference(resolution, [status(thm)], [c28,c0])). % 46.44/6.39 cnf(d2, plain, 'Ts2'(X0) | ~'Ts3'(X0), inference(resolution, [status(thm)], [c33,c0])). % 46.44/6.39 cnf(d3, plain, 'Ts4'(sK5), inference(resolution, [status(thm)], [c10,c0])). % 46.44/6.39 cnf(d4, plain, ~'Ts4'(X0) | 'Ts3'(X0), inference(resolution, [status(thm)], [c38,c0])). % 46.44/6.39 cnf(d5, plain, 'Ts3'(sK5), inference(resolution, [status(thm)], [d4,d3])). % 46.44/6.39 cnf(d6, plain, 'Ts2'(sK5), inference(resolution, [status(thm)], [d5,d2])). % 46.44/6.39 cnf(d7, plain, 'Ts1'(sK5), inference(resolution, [status(thm)], [d6,d1])). % 46.44/6.39 cnf(d8, plain, 'Ts4'(sK24(sK5)), inference(resolution, [status(thm)], [d7,d0])). % 46.44/6.39 cnf(d9, plain, ~r1(X0,X1) | ~r1(X2,X0) | ~r1(X3,X4) | ~r1(X5,X6) | ~r1(X1,X5) | ~r1(X6,X3) | ~'Ts4'(X2) | p1(X4) | p5(X4), inference(resolution, [status(thm)], [c34,c0])). % 46.44/6.39 cnf(d10, plain, ~r1(X0,X1) | ~r1(X2,X0) | ~r1(X1,X3) | ~r1(X4,X5) | ~r1(X5,X2) | ~'Ts4'(X4) | p1(X3) | p5(X3), inference(resolution, [status(thm)], [d9,c0])). % 46.44/6.39 cnf(d11, plain, ~r1(X0,X1) | ~r1(X2,X0) | ~r1(X1,X3) | ~r1(X3,X4) | ~'Ts4'(X2) | p1(X4) | p5(X4), inference(resolution, [status(thm)], [d10,c0])). % 46.44/6.39 cnf(d12, plain, ~r1(X0,X1) | ~r1(X2,X3) | ~r1(X3,X0) | ~'Ts4'(X2) | p1(X1) | p5(X1), inference(resolution, [status(thm)], [d11,c0])). % 46.44/6.39 cnf(d13, plain, ~r1(X0,X1) | ~r1(X2,X0) | ~'Ts4'(X2) | p1(X1) | p5(X1), inference(resolution, [status(thm)], [d12,c0])). % 46.44/6.39 cnf(d14, plain, ~r1(X0,X1) | ~'Ts4'(X0) | p1(X1) | p5(X1), inference(resolution, [status(thm)], [d13,c0])). % 46.44/6.39 cnf(d15, plain, ~'Ts4'(X0) | p1(X0) | p5(X0), inference(resolution, [status(thm)], [d14,c0])). % 46.44/6.39 cnf(d16, plain, p1(sK24(sK5)) | p5(sK24(sK5)), inference(resolution, [status(thm)], [d15,d8])). % 46.44/6.39 cnf(d17, plain, 'Ts3'(sK24(sK5)), inference(resolution, [status(thm)], [d8,d4])). % 46.44/6.39 cnf(d18, plain, 'Ts2'(sK24(sK5)), inference(resolution, [status(thm)], [d17,d2])). % 46.44/6.39 cnf(d19, plain, 'Ts1'(sK24(sK5)), inference(resolution, [status(thm)], [d18,d1])). % 46.44/6.39 cnf(d20, plain, ~r1(X0,X1) | ~r1(X2,X3) | ~r1(X1,X2) | ~p2(X3) | ~p1(X3) | ~'Ts1'(X0), inference(resolution, [status(thm)], [c23,c0])). % 46.44/6.39 cnf(d21, plain, ~r1(X0,X1) | ~r1(X2,X0) | ~p2(X1) | ~p1(X1) | ~'Ts1'(X2), inference(resolution, [status(thm)], [d20,c0])). % 46.44/6.39 cnf(d22, plain, ~r1(X0,X1) | ~p2(X1) | ~p1(X1) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d21,c0])). % 46.44/6.39 cnf(d23, plain, ~p2(X0) | ~p1(X0) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d22,c0])). % 46.44/6.39 cnf(d24, plain, ~p2(sK24(sK5)) | ~p1(sK24(sK5)), inference(resolution, [status(thm)], [d23,d19])). % 46.44/6.39 cnf(d25, plain, ~r1(X0,X1) | ~r1(X2,X3) | ~r1(X3,X0) | p2(X1) | p3(X1) | ~'Ts1'(X2), inference(resolution, [status(thm)], [c18,c0])). % 46.44/6.39 cnf(d26, plain, ~r1(X0,X1) | ~r1(X2,X0) | p2(X1) | p3(X1) | ~'Ts1'(X2), inference(resolution, [status(thm)], [d25,c0])). % 46.44/6.39 cnf(d27, plain, ~r1(X0,X1) | p2(X1) | p3(X1) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d26,c0])). % 46.44/6.39 cnf(d28, plain, p2(X0) | p3(X0) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d27,c0])). % 46.44/6.39 cnf(d29, plain, p2(sK24(sK5)) | p3(sK24(sK5)), inference(resolution, [status(thm)], [d28,d19])). % 46.44/6.39 cnf(d30, plain, p2(sK24(sK5)) | ~'Ts1'(sK5), inference(resolution, [status(thm)], [d29,c21])). % 46.44/6.39 cnf(d31, plain, p2(sK24(sK5)), inference(resolution, [status(thm)], [d7,d30])). % 46.44/6.39 cnf(d32, plain, ~p1(sK24(sK5)), inference(resolution, [status(thm)], [d31,d24])). % 46.44/6.39 cnf(d33, plain, p5(sK24(sK5)), inference(resolution, [status(thm)], [d32,d16])). % 46.44/6.39 cnf(d34, plain, ~r1(X0,X1) | ~r1(X1,X2) | ~r1(X3,X4) | ~r1(X2,X3) | ~r1(X5,X0) | ~p4(X4) | ~p5(X4) | ~'Ts3'(X5), inference(resolution, [status(thm)], [c30,c0])). % 46.44/6.39 cnf(d35, plain, ~r1(X0,X1) | ~r1(X2,X3) | ~r1(X4,X2) | ~r1(X1,X4) | ~p4(X3) | ~p5(X3) | ~'Ts3'(X0), inference(resolution, [status(thm)], [d34,c0])). % 46.44/6.39 cnf(d36, plain, ~r1(X0,X1) | ~r1(X1,X2) | ~r1(X3,X0) | ~p4(X2) | ~p5(X2) | ~'Ts3'(X3), inference(resolution, [status(thm)], [d35,c0])). % 46.44/6.39 cnf(d37, plain, ~r1(X0,X1) | ~r1(X1,X2) | ~p4(X2) | ~p5(X2) | ~'Ts3'(X0), inference(resolution, [status(thm)], [d36,c0])). % 46.44/6.39 cnf(d38, plain, ~r1(X0,X1) | ~p4(X1) | ~p5(X1) | ~'Ts3'(X0), inference(resolution, [status(thm)], [d37,c0])). % 46.44/6.39 cnf(d39, plain, ~p4(X0) | ~p5(X0) | ~'Ts3'(X0), inference(resolution, [status(thm)], [d38,c0])). % 46.44/6.39 cnf(d40, plain, ~p4(sK24(sK5)) | ~p5(sK24(sK5)), inference(resolution, [status(thm)], [d39,d17])). % 46.44/6.39 cnf(d41, plain, ~r1(X0,X1) | ~r1(X1,X2) | ~r1(X3,X4) | ~r1(X2,X3) | p4(X4) | p3(X4) | ~'Ts2'(X0), inference(resolution, [status(thm)], [c24,c0])). % 46.44/6.39 cnf(d42, plain, ~r1(X0,X1) | ~r1(X2,X0) | ~r1(X3,X2) | p4(X1) | p3(X1) | ~'Ts2'(X3), inference(resolution, [status(thm)], [d41,c0])). % 46.44/6.39 cnf(d43, plain, ~r1(X0,X1) | ~r1(X1,X2) | p4(X2) | p3(X2) | ~'Ts2'(X0), inference(resolution, [status(thm)], [d42,c0])). % 46.44/6.39 cnf(d44, plain, ~r1(X0,X1) | p4(X1) | p3(X1) | ~'Ts2'(X0), inference(resolution, [status(thm)], [d43,c0])). % 46.44/6.39 cnf(d45, plain, p4(X0) | p3(X0) | ~'Ts2'(X0), inference(resolution, [status(thm)], [d44,c0])). % 46.44/6.39 cnf(d46, plain, p4(sK24(sK5)) | p3(sK24(sK5)), inference(resolution, [status(thm)], [d45,d18])). % 46.44/6.39 cnf(d47, plain, ~r1(X0,X1) | ~r1(X2,X3) | ~r1(X3,X0) | ~p2(X1) | ~p3(X1) | ~'Ts1'(X2), inference(resolution, [status(thm)], [c19,c0])). % 46.44/6.39 cnf(d48, plain, ~r1(X0,X1) | ~r1(X2,X0) | ~p2(X1) | ~p3(X1) | ~'Ts1'(X2), inference(resolution, [status(thm)], [d47,c0])). % 46.44/6.39 cnf(d49, plain, ~r1(X0,X1) | ~p2(X1) | ~p3(X1) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d48,c0])). % 46.44/6.39 cnf(d50, plain, ~p2(X0) | ~p3(X0) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d49,c0])). % 46.44/6.39 cnf(d51, plain, ~p2(sK24(sK5)) | ~p3(sK24(sK5)), inference(resolution, [status(thm)], [d50,d19])). % 46.44/6.39 cnf(d52, plain, ~p3(sK24(sK5)), inference(resolution, [status(thm)], [d31,d51])). % 46.44/6.39 cnf(d53, plain, p4(sK24(sK5)), inference(resolution, [status(thm)], [d52,d46])). % 46.44/6.39 cnf(d54, plain, ~p5(sK24(sK5)), inference(resolution, [status(thm)], [d53,d40])). % 46.44/6.39 cnf(d55, plain, $false, inference(resolution, [status(thm)], [d54,d33])). % 46.44/6.39 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------