%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LCL686+1.010 : 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 : 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 07:55:15 AM UTC 2026 % Result : Theorem 20.46s 3.86s % Output : CNFRefutation 20.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL686+1.010 : 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.12/0.37 % Computer : n019.cluster.edu % 0.12/0.37 % Model : x86_64 x86_64 % 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.37 % Memory : 8046.5625MB % 0.12/0.37 % OS : Linux 6.8.0-71-generic % 0.12/0.37 % CPULimit : 300 % 0.12/0.37 % WCLimit : 300 % 0.12/0.37 % DateTime : Fri Sep 25 23:23:33 UTC 2026 % 0.12/0.37 % CPUTime : % 0.12/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 20.46/3.86 % SZS status Theorem for theBenchmark.p % 20.46/3.86 % SZS output start CNFRefutation for theBenchmark.p % 20.46/3.86 fof(reflexivity, axiom, ! [X0] : r1(X0,X0)). % 20.46/3.86 fof(main, conjecture, ~? [X0] : ~((! [X1] : ((~r1(X0,X1) | (~p30(X1) | ! [X0] : ((~r1(X1,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) | (! [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) | (! [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) | (! [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) | $false)) | ~! [X0] : ((~r1(X1,X0) | ~(((p29(X0) & ~p28(X0)) | (~p29(X0) & p28(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p28(X1) & ~p27(X1)) | (~p28(X1) & p27(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p27(X0) & ~p26(X0)) | (~p27(X0) & p26(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p26(X1) & ~p25(X1)) | (~p26(X1) & p25(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p25(X0) & ~p24(X0)) | (~p25(X0) & p24(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p24(X1) & ~p23(X1)) | (~p24(X1) & p23(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p23(X0) & ~p22(X0)) | (~p23(X0) & p22(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p22(X1) & ~p21(X1)) | (~p22(X1) & p21(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p21(X0) & ~p20(X0)) | (~p21(X0) & p20(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p20(X1) & ~p19(X1)) | (~p20(X1) & p19(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p19(X0) & ~p18(X0)) | (~p19(X0) & p18(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p18(X1) & ~p17(X1)) | (~p18(X1) & p17(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p17(X0) & ~p16(X0)) | (~p17(X0) & p16(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p16(X1) & ~p15(X1)) | (~p16(X1) & p15(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p15(X0) & ~p14(X0)) | (~p15(X0) & p14(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p14(X1) & ~p13(X1)) | (~p14(X1) & p13(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p13(X0) & ~p12(X0)) | (~p13(X0) & p12(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p12(X1) & ~p11(X1)) | (~p12(X1) & p11(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p11(X0) & ~p10(X0)) | (~p11(X0) & p10(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p10(X1) & ~p9(X1)) | (~p10(X1) & p9(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p9(X0) & ~p8(X0)) | (~p9(X0) & p8(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p8(X1) & ~p7(X1)) | (~p8(X1) & p7(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p7(X0) & ~p6(X0)) | (~p7(X0) & p6(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p6(X1) & ~p5(X1)) | (~p6(X1) & p5(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p5(X0) & ~p4(X0)) | (~p5(X0) & p4(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p4(X1) & ~p3(X1)) | (~p4(X1) & p3(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p3(X0) & ~p2(X0)) | (~p3(X0) & p2(X0))))))))) | (~! [X1] : ((~r1(X0,X1) | ~(((p2(X1) & ~p1(X1)) | (~p2(X1) & p1(X1)))))) | (! [X1] : ((~r1(X0,X1) | p30(X1))) | ! [X1] : ((~r1(X0,X1) | ((~p28(X1) & ~p29(X1)) | ((p29(X1) & p28(X1)) | ((~p27(X1) & ~p28(X1)) | ((p28(X1) & p27(X1)) | ((~p26(X1) & ~p27(X1)) | ((p27(X1) & p26(X1)) | ((~p25(X1) & ~p26(X1)) | ((p26(X1) & p25(X1)) | ((~p24(X1) & ~p25(X1)) | ((p25(X1) & p24(X1)) | ((~p23(X1) & ~p24(X1)) | ((p24(X1) & p23(X1)) | ((~p22(X1) & ~p23(X1)) | ((p23(X1) & p22(X1)) | ((~p21(X1) & ~p22(X1)) | ((p22(X1) & p21(X1)) | ((~p20(X1) & ~p21(X1)) | ((p21(X1) & p20(X1)) | ((~p19(X1) & ~p20(X1)) | ((p20(X1) & p19(X1)) | ((~p18(X1) & ~p19(X1)) | ((p19(X1) & p18(X1)) | ((~p17(X1) & ~p18(X1)) | ((p18(X1) & p17(X1)) | ((~p16(X1) & ~p17(X1)) | ((p17(X1) & p16(X1)) | ((~p15(X1) & ~p16(X1)) | ((p16(X1) & p15(X1)) | ((~p14(X1) & ~p15(X1)) | ((p15(X1) & p14(X1)) | ((~p13(X1) & ~p14(X1)) | ((p14(X1) & p13(X1)) | ((~p12(X1) & ~p13(X1)) | ((p13(X1) & p12(X1)) | ((~p11(X1) & ~p12(X1)) | ((p12(X1) & p11(X1)) | ((~p10(X1) & ~p11(X1)) | ((p11(X1) & p10(X1)) | ((~p9(X1) & ~p10(X1)) | ((p10(X1) & p9(X1)) | ((~p8(X1) & ~p9(X1)) | ((p9(X1) & p8(X1)) | ((~p7(X1) & ~p8(X1)) | ((p8(X1) & p7(X1)) | ((~p6(X1) & ~p7(X1)) | ((p7(X1) & p6(X1)) | ((~p5(X1) & ~p6(X1)) | ((p6(X1) & p5(X1)) | ((~p4(X1) & ~p5(X1)) | ((p5(X1) & p4(X1)) | ((~p3(X1) & ~p4(X1)) | ((p4(X1) & p3(X1)) | ((~p2(X1) & ~p3(X1)) | ((p3(X1) & p2(X1)) | ((~p1(X1) & ~p2(X1)) | (p2(X1) & p1(X1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))). % 20.46/3.86 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ~((! [X1] : ((~r1(X0,X1) | (~p30(X1) | ! [X0] : ((~r1(X1,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) | (! [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) | (! [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) | (! [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) | $false)) | ~! [X0] : ((~r1(X1,X0) | ~(((p29(X0) & ~p28(X0)) | (~p29(X0) & p28(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p28(X1) & ~p27(X1)) | (~p28(X1) & p27(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p27(X0) & ~p26(X0)) | (~p27(X0) & p26(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p26(X1) & ~p25(X1)) | (~p26(X1) & p25(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p25(X0) & ~p24(X0)) | (~p25(X0) & p24(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p24(X1) & ~p23(X1)) | (~p24(X1) & p23(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p23(X0) & ~p22(X0)) | (~p23(X0) & p22(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p22(X1) & ~p21(X1)) | (~p22(X1) & p21(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p21(X0) & ~p20(X0)) | (~p21(X0) & p20(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p20(X1) & ~p19(X1)) | (~p20(X1) & p19(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p19(X0) & ~p18(X0)) | (~p19(X0) & p18(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p18(X1) & ~p17(X1)) | (~p18(X1) & p17(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p17(X0) & ~p16(X0)) | (~p17(X0) & p16(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p16(X1) & ~p15(X1)) | (~p16(X1) & p15(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p15(X0) & ~p14(X0)) | (~p15(X0) & p14(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p14(X1) & ~p13(X1)) | (~p14(X1) & p13(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p13(X0) & ~p12(X0)) | (~p13(X0) & p12(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p12(X1) & ~p11(X1)) | (~p12(X1) & p11(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p11(X0) & ~p10(X0)) | (~p11(X0) & p10(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p10(X1) & ~p9(X1)) | (~p10(X1) & p9(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p9(X0) & ~p8(X0)) | (~p9(X0) & p8(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p8(X1) & ~p7(X1)) | (~p8(X1) & p7(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p7(X0) & ~p6(X0)) | (~p7(X0) & p6(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p6(X1) & ~p5(X1)) | (~p6(X1) & p5(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p5(X0) & ~p4(X0)) | (~p5(X0) & p4(X0))))))))) | ~! [X1] : ((~r1(X0,X1) | ~(((p4(X1) & ~p3(X1)) | (~p4(X1) & p3(X1))))))))) | ~! [X0] : ((~r1(X1,X0) | ~(((p3(X0) & ~p2(X0)) | (~p3(X0) & p2(X0))))))))) | (~! [X1] : ((~r1(X0,X1) | ~(((p2(X1) & ~p1(X1)) | (~p2(X1) & p1(X1)))))) | (! [X1] : ((~r1(X0,X1) | p30(X1))) | ! [X1] : ((~r1(X0,X1) | ((~p28(X1) & ~p29(X1)) | ((p29(X1) & p28(X1)) | ((~p27(X1) & ~p28(X1)) | ((p28(X1) & p27(X1)) | ((~p26(X1) & ~p27(X1)) | ((p27(X1) & p26(X1)) | ((~p25(X1) & ~p26(X1)) | ((p26(X1) & p25(X1)) | ((~p24(X1) & ~p25(X1)) | ((p25(X1) & p24(X1)) | ((~p23(X1) & ~p24(X1)) | ((p24(X1) & p23(X1)) | ((~p22(X1) & ~p23(X1)) | ((p23(X1) & p22(X1)) | ((~p21(X1) & ~p22(X1)) | ((p22(X1) & p21(X1)) | ((~p20(X1) & ~p21(X1)) | ((p21(X1) & p20(X1)) | ((~p19(X1) & ~p20(X1)) | ((p20(X1) & p19(X1)) | ((~p18(X1) & ~p19(X1)) | ((p19(X1) & p18(X1)) | ((~p17(X1) & ~p18(X1)) | ((p18(X1) & p17(X1)) | ((~p16(X1) & ~p17(X1)) | ((p17(X1) & p16(X1)) | ((~p15(X1) & ~p16(X1)) | ((p16(X1) & p15(X1)) | ((~p14(X1) & ~p15(X1)) | ((p15(X1) & p14(X1)) | ((~p13(X1) & ~p14(X1)) | ((p14(X1) & p13(X1)) | ((~p12(X1) & ~p13(X1)) | ((p13(X1) & p12(X1)) | ((~p11(X1) & ~p12(X1)) | ((p12(X1) & p11(X1)) | ((~p10(X1) & ~p11(X1)) | ((p11(X1) & p10(X1)) | ((~p9(X1) & ~p10(X1)) | ((p10(X1) & p9(X1)) | ((~p8(X1) & ~p9(X1)) | ((p9(X1) & p8(X1)) | ((~p7(X1) & ~p8(X1)) | ((p8(X1) & p7(X1)) | ((~p6(X1) & ~p7(X1)) | ((p7(X1) & p6(X1)) | ((~p5(X1) & ~p6(X1)) | ((p6(X1) & p5(X1)) | ((~p4(X1) & ~p5(X1)) | ((p5(X1) & p4(X1)) | ((~p3(X1) & ~p4(X1)) | ((p4(X1) & p3(X1)) | ((~p2(X1) & ~p3(X1)) | ((p3(X1) & p2(X1)) | ((~p1(X1) & ~p2(X1)) | (p2(X1) & p1(X1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(negate_conjecture, [status(cth)], [main])). % 20.46/3.86 cnf(c0, plain, r1(X0,X0), inference(clausification, [status(esa)], [reflexivity])). % 20.46/3.86 cnf(c7, plain, ~r1(sK8,X0) | X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 20.46/3.86 cnf(c90, plain, ~X0(X1) | ~r1(X1,X2) | ~p2(X2) | p1(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 20.46/3.86 cnf(c91, plain, ~X0(X1) | ~r1(X1,X2) | p2(X2) | ~p1(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 20.46/3.86 cnf(c94, plain, ~X0(X1) | r1(X1,sK67(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 20.46/3.86 cnf(c149, plain, ~X0(X1) | p1(sK67(X1)) | p2(sK67(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 20.46/3.86 cnf(c150, plain, ~X0(X1) | ~p2(sK67(X1)) | ~p1(sK67(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 20.46/3.86 cnf(d0, plain, p1(X0) | ~'Ts4'(X0) | ~p2(X0), inference(resolution, [status(thm)], [c90,c0])). % 20.46/3.86 cnf(d1, plain, ~'Ts4'(sK8) | 'Ts4'(sK67(sK8)), inference(resolution, [status(thm)], [c94,c7])). % 20.46/3.86 cnf(d2, plain, 'Ts4'(sK8), inference(resolution, [status(thm)], [c7,c0])). % 20.46/3.86 cnf(d3, plain, 'Ts4'(sK67(sK8)), inference(resolution, [status(thm)], [d2,d1])). % 20.46/3.86 cnf(d4, plain, ~p1(X0) | ~'Ts4'(X0) | p2(X0), inference(resolution, [status(thm)], [c91,c0])). % 20.46/3.86 cnf(d5, plain, ~p1(sK67(sK8)) | p2(sK67(sK8)), inference(resolution, [status(thm)], [d4,d3])). % 20.46/3.86 cnf(d6, plain, ~'Ts4'(sK8) | p2(sK67(sK8)) | p2(sK67(sK8)), inference(resolution, [status(thm)], [c149,d5])). % 20.46/3.86 cnf(d7, plain, p2(sK67(sK8)), inference(resolution, [status(thm)], [d2,d6])). % 20.46/3.86 cnf(d8, plain, p1(sK67(sK8)) | ~'Ts4'(sK67(sK8)), inference(resolution, [status(thm)], [d7,d0])). % 20.46/3.86 cnf(d9, plain, p1(sK67(sK8)), inference(resolution, [status(thm)], [d3,d8])). % 20.46/3.86 cnf(d10, plain, ~p1(sK67(sK8)) | ~'Ts4'(sK8), inference(resolution, [status(thm)], [d7,c150])). % 20.46/3.86 cnf(d11, plain, ~p1(sK67(sK8)), inference(resolution, [status(thm)], [d2,d10])). % 20.46/3.86 cnf(d12, plain, $false, inference(resolution, [status(thm)], [d11,d9])). % 20.46/3.86 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------