%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LCL686+1.001 : 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 : n011.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 8.86s 1.66s % Output : CNFRefutation 8.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL686+1.001 : 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.08/0.37 % Computer : n011.cluster.edu % 0.08/0.37 % Model : x86_64 x86_64 % 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.37 % Memory : 8046.5625MB % 0.08/0.37 % OS : Linux 6.8.0-71-generic % 0.08/0.37 % CPULimit : 300 % 0.08/0.37 % WCLimit : 300 % 0.08/0.37 % DateTime : Fri Sep 25 23:22:59 UTC 2026 % 0.08/0.37 % CPUTime : % 0.08/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.86/1.66 % SZS status Theorem for theBenchmark.p % 8.86/1.66 % SZS output start CNFRefutation for theBenchmark.p % 8.86/1.66 fof(reflexivity, axiom, ! [X0] : r1(X0,X0)). % 8.86/1.66 fof(main, conjecture, ~? [X0] : ~((! [X1] : ((~r1(X0,X1) | (~p3(X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0)))))) | ! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~((! [X1] : ((~r1(X0,X1) | $false)) | (~! [X1] : ((~r1(X0,X1) | ~(((p2(X1) & ~p1(X1)) | (~p2(X1) & p1(X1)))))) | (! [X1] : ((~r1(X0,X1) | p3(X1))) | ! [X1] : ((~r1(X0,X1) | ((~p1(X1) & ~p2(X1)) | (p2(X1) & p1(X1)))))))))))))))). % 8.86/1.66 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ~((! [X1] : ((~r1(X0,X1) | (~p3(X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0)))))) | ! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~((! [X1] : ((~r1(X0,X1) | $false)) | (~! [X1] : ((~r1(X0,X1) | ~(((p2(X1) & ~p1(X1)) | (~p2(X1) & p1(X1)))))) | (! [X1] : ((~r1(X0,X1) | p3(X1))) | ! [X1] : ((~r1(X0,X1) | ((~p1(X1) & ~p2(X1)) | (p2(X1) & p1(X1))))))))))))))), inference(negate_conjecture, [status(cth)], [main])). % 8.86/1.66 cnf(c0, plain, r1(X0,X0), inference(clausification, [status(esa)], [reflexivity])). % 8.86/1.66 cnf(c7, plain, ~r1(sK8,X0) | X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 8.86/1.66 cnf(c9, plain, ~X0(X1) | ~r1(X1,X2) | ~p2(X2) | p1(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 8.86/1.66 cnf(c10, plain, ~X0(X1) | ~r1(X1,X2) | p2(X2) | ~p1(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 8.86/1.66 cnf(c11, plain, ~X0(X1) | r1(X1,sK12(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 8.86/1.66 cnf(c13, plain, ~X0(X1) | r1(X1,sK13(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 8.86/1.66 cnf(c14, plain, ~X0(X1) | p1(sK13(X1)) | p2(sK13(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 8.86/1.66 cnf(c15, plain, ~X0(X1) | ~p2(sK13(X1)) | ~p1(sK13(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 8.86/1.66 cnf(d0, plain, ~'Ts4'(sK8) | 'Ts4'(sK12(sK8)), inference(resolution, [status(thm)], [c11,c7])). % 8.86/1.66 cnf(d1, plain, 'Ts4'(sK8), inference(resolution, [status(thm)], [c7,c0])). % 8.86/1.66 cnf(d2, plain, 'Ts4'(sK12(sK8)), inference(resolution, [status(thm)], [d1,d0])). % 8.86/1.66 cnf(d3, plain, ~'Ts4'(X0) | p1(sK13(X0)) | ~'Ts4'(X0) | ~p2(sK13(X0)), inference(resolution, [status(thm)], [c13,c9])). % 8.86/1.66 cnf(d4, plain, p1(sK13(X0)) | ~'Ts4'(X0) | p1(sK13(X0)) | ~'Ts4'(X0), inference(resolution, [status(thm)], [d3,c14])). % 8.86/1.66 cnf(d5, plain, ~'Ts4'(X0) | ~p1(sK13(X0)) | ~'Ts4'(X0) | p2(sK13(X0)), inference(resolution, [status(thm)], [c13,c10])). % 8.86/1.66 cnf(d6, plain, ~'Ts4'(X0) | ~'Ts4'(X0) | p2(sK13(X0)), inference(resolution, [status(thm)], [d4,d5])). % 8.86/1.66 cnf(d7, plain, ~'Ts4'(X0) | ~p1(sK13(X0)) | ~'Ts4'(X0), inference(resolution, [status(thm)], [d6,c15])). % 8.86/1.66 cnf(d8, plain, ~'Ts4'(X0) | ~'Ts4'(X0), inference(resolution, [status(thm)], [d7,d4])). % 8.86/1.66 cnf(d9, plain, $false, inference(resolution, [status(thm)], [d8,d2])). % 8.86/1.66 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------