%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LCL686+1.005 : 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 : n012.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:14 AM UTC 2026 % Result : Theorem 20.73s 3.04s % Output : CNFRefutation 20.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : LCL686+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.02 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.02/0.29 % Computer : n012.cluster.edu % 0.02/0.29 % Model : x86_64 x86_64 % 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.02/0.29 % Memory : 8046.5625MB % 0.02/0.29 % OS : Linux 6.8.0-71-generic % 0.02/0.29 % CPULimit : 300 % 0.02/0.29 % WCLimit : 300 % 0.02/0.29 % DateTime : Fri Sep 25 23:22:50 UTC 2026 % 0.02/0.30 % CPUTime : % 0.02/0.30 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 20.73/3.04 % SZS status Theorem for theBenchmark.p % 20.73/3.04 % SZS output start CNFRefutation for theBenchmark.p % 20.73/3.04 fof(reflexivity, axiom, ! [X0] : r1(X0,X0)). % 20.73/3.04 fof(main, conjecture, ~? [X0] : ~((! [X1] : ((~r1(X0,X1) | (~p15(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) | $false)) | ~! [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) | p15(X1))) | ! [X1] : ((~r1(X0,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.73/3.04 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ~((! [X1] : ((~r1(X0,X1) | (~p15(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) | $false)) | ~! [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) | p15(X1))) | ! [X1] : ((~r1(X0,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.73/3.04 cnf(c0, plain, r1(X0,X0), inference(clausification, [status(esa)], [reflexivity])). % 20.73/3.04 cnf(c7, plain, ~r1(sK8,X0) | X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 20.73/3.04 cnf(c45, plain, ~X0(X1) | ~r1(X1,X2) | ~p2(X2) | p1(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 20.73/3.04 cnf(c46, plain, ~X0(X1) | ~r1(X1,X2) | p2(X2) | ~p1(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 20.73/3.04 cnf(c49, plain, ~X0(X1) | r1(X1,sK37(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 20.73/3.04 cnf(c74, plain, ~X0(X1) | p1(sK37(X1)) | p2(sK37(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 20.73/3.04 cnf(c75, plain, ~X0(X1) | ~p2(sK37(X1)) | ~p1(sK37(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 20.73/3.04 cnf(d0, plain, p1(X0) | ~'Ts4'(X0) | ~p2(X0), inference(resolution, [status(thm)], [c45,c0])). % 20.73/3.04 cnf(d1, plain, ~'Ts4'(sK8) | 'Ts4'(sK37(sK8)), inference(resolution, [status(thm)], [c49,c7])). % 20.73/3.04 cnf(d2, plain, 'Ts4'(sK8), inference(resolution, [status(thm)], [c7,c0])). % 20.73/3.04 cnf(d3, plain, 'Ts4'(sK37(sK8)), inference(resolution, [status(thm)], [d2,d1])). % 20.73/3.04 cnf(d4, plain, ~p1(X0) | ~'Ts4'(X0) | p2(X0), inference(resolution, [status(thm)], [c46,c0])). % 20.73/3.04 cnf(d5, plain, ~p1(sK37(sK8)) | p2(sK37(sK8)), inference(resolution, [status(thm)], [d4,d3])). % 20.73/3.04 cnf(d6, plain, ~'Ts4'(sK8) | p2(sK37(sK8)) | p2(sK37(sK8)), inference(resolution, [status(thm)], [c74,d5])). % 20.73/3.04 cnf(d7, plain, p2(sK37(sK8)), inference(resolution, [status(thm)], [d2,d6])). % 20.73/3.04 cnf(d8, plain, p1(sK37(sK8)) | ~'Ts4'(sK37(sK8)), inference(resolution, [status(thm)], [d7,d0])). % 20.73/3.04 cnf(d9, plain, p1(sK37(sK8)), inference(resolution, [status(thm)], [d3,d8])). % 20.73/3.04 cnf(d10, plain, ~p1(sK37(sK8)) | ~'Ts4'(sK8), inference(resolution, [status(thm)], [c75,d7])). % 20.73/3.04 cnf(d11, plain, ~p1(sK37(sK8)), inference(resolution, [status(thm)], [d2,d10])). % 20.73/3.04 cnf(d12, plain, $false, inference(resolution, [status(thm)], [d11,d9])). % 20.73/3.04 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------