%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LCL652+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 : n003.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:01 AM UTC 2026 % Result : Theorem 59.99s 18.17s % Output : CNFRefutation 59.99s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL652+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/10.39 % Computer : n003.cluster.edu % 0.10/10.39 % Model : x86_64 x86_64 % 0.10/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/10.39 % Memory : 8046.5625MB % 0.10/10.39 % OS : Linux 6.8.0-71-generic % 0.10/10.39 % CPULimit : 300 % 0.10/10.39 % WCLimit : 300 % 0.10/10.39 % DateTime : Fri Sep 25 23:00:19 UTC 2026 % 0.10/10.39 % CPUTime : % 0.10/10.39 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 59.99/18.17 % SZS status Theorem for theBenchmark.p % 59.99/18.17 % SZS output start CNFRefutation for theBenchmark.p % 59.99/18.17 fof(main, conjecture, ~? [X0] : ~((~! [X1] : ((~r1(X0,X1) | ~p4(X1))) | (~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0))))))) & ! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | ~p1(X1))))))))) | (~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p3(X0))) | ~p2(X1)))))) | (~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((! [X0] : ((~r1(X1,X0) | p3(X0))) | ~p2(X1))))) & (p2(X0) & ~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | ~p2(X1)))))))))))) | ((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p3(X1))) | ~p2(X0)))))))) & ! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | ~p2(X1)))))) | (~! [X0] : ((~r1(X1,X0) | ~((! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~p2(X0))))) & ! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p3(X0))) | ~p2(X1)))))))))))) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p3(X1))) | ~p2(X0)))) & ! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | ~p2(X1))))))))))))) | (~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | p1(X0))))))) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) | ! [X0] : ((~r1(X1,X0) | p1(X0)))))) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p2(X1))))))) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~p1(X1))))) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0)))))))))))))). % 59.99/18.17 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ~((~! [X1] : ((~r1(X0,X1) | ~p4(X1))) | (~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0))))))) & ! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | ~p1(X1))))))))) | (~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p3(X0))) | ~p2(X1)))))) | (~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ~((! [X0] : ((~r1(X1,X0) | p3(X0))) | ~p2(X1))))) & (p2(X0) & ~! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | ~p2(X1)))))))))))) | ((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p3(X1))) | ~p2(X0)))))))) & ! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | ~p2(X1)))))) | (~! [X0] : ((~r1(X1,X0) | ~((! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~p2(X0))))) & ! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p3(X0))) | ~p2(X1)))))))))))) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p3(X1))) | ~p2(X0)))) & ! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | ~p2(X1))))))))))))) | (~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | p1(X0))))))) | (! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))) | ! [X0] : ((~r1(X1,X0) | p1(X0)))))) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | p2(X1))))))) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~p1(X1))))) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0))))))))))))), inference(negate_conjecture, [status(cth)], [main])). % 59.99/18.17 cnf(c1, plain, ~r1(sK5,X0) | X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c9, plain, r1(sK5,sK16), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c10, plain, ~r1(sK16,X0) | r1(X0,sK18(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c11, plain, ~r1(sK16,X0) | ~p2(sK18(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c18, plain, ~X0(X1) | ~r1(X1,X2) | ~r1(X2,X3) | r1(X3,sK31(X3)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c19, plain, ~X0(X1) | ~r1(X1,X2) | ~r1(X2,X3) | p2(sK31(X3)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c22, plain, ~X0(X1) | r1(X1,sK33(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c23, plain, ~X0(X1) | p2(sK33(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c26, plain, ~X0(X1) | r1(X1,sK35(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c27, plain, ~X0(X1) | ~r1(sK35(X1),X2) | r1(X2,sK37(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c28, plain, ~X0(X1) | ~r1(sK35(X1),X2) | p2(sK37(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c33, plain, ~X0(X1) | ~r1(X1,X2) | p2(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c34, plain, ~X0(X1) | ~r1(X1,X2) | r1(X2,sK42(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c35, plain, ~X0(X1) | ~r1(X1,X2) | p2(sK42(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c38, plain, ~X0(X1) | X2(X1) | r1(X1,sK44(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c39, plain, ~X0(X1) | X2(X1) | ~r1(sK44(X1),X3) | ~p2(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c40, plain, ~X0(X1) | X2(X1) | r1(X1,sK46(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c41, plain, ~X0(X1) | X2(X1) | ~r1(sK46(X1),X3) | ~p2(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c42, plain, ~X0(X1) | ~r1(X1,X2) | X3(X2) | r1(X2,sK49(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c43, plain, ~r1(sK49(X0),X1) | ~X2(X3) | ~p2(X1) | X4(X0) | ~r1(X3,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c44, plain, ~r1(X0,X1) | ~X2(X3) | X4(X0) | ~p2(X0) | ~r1(X3,X0) | r1(X1,sK53(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(c45, plain, ~r1(X0,X1) | ~X2(X3) | X4(X0) | ~p2(X0) | ~r1(sK53(X1),X5) | ~r1(X3,X0) | ~p2(X5), inference(clausification, [status(esa)], [negated_conjecture])). % 59.99/18.17 cnf(d0, plain, 'Ts4'(sK16), inference(resolution, [status(thm)], [c9,c1])). % 59.99/18.17 cnf(d1, plain, r1(sK16,sK46(sK16)) | 'Ts1'(sK16), inference(resolution, [status(thm)], [c40,d0])). % 59.99/18.17 cnf(d2, plain, 'Ts1'(sK16) | ~'Ts4'(sK16) | p2(sK42(sK46(sK16))), inference(resolution, [status(thm)], [d1,c35])). % 59.99/18.17 cnf(d3, plain, p2(sK42(sK46(sK16))) | 'Ts1'(sK16), inference(resolution, [status(thm)], [d0,d2])). % 59.99/18.17 cnf(d4, plain, 'Ts1'(sK16) | r1(sK46(sK16),sK42(sK46(sK16))) | ~'Ts4'(sK16), inference(resolution, [status(thm)], [d1,c34])). % 59.99/18.17 cnf(d5, plain, r1(sK46(sK16),sK42(sK46(sK16))) | 'Ts1'(sK16), inference(resolution, [status(thm)], [d0,d4])). % 59.99/18.17 cnf(d6, plain, 'Ts1'(sK16) | ~'Ts4'(sK16) | ~p2(sK42(sK46(sK16))) | 'Ts1'(sK16), inference(resolution, [status(thm)], [d5,c41])). % 59.99/18.17 cnf(d7, plain, ~p2(sK42(sK46(sK16))) | 'Ts1'(sK16), inference(resolution, [status(thm)], [d0,d6])). % 59.99/18.17 cnf(d8, plain, 'Ts1'(sK16) | 'Ts1'(sK16), inference(resolution, [status(thm)], [d7,d3])). % 59.99/18.17 cnf(d9, plain, r1(sK16,sK33(sK16)), inference(resolution, [status(thm)], [d8,c22])). % 59.99/18.17 cnf(d10, plain, ~r1(sK33(sK16),X0) | ~r1(sK53(X0),X1) | ~'Ts4'(sK16) | ~p2(X1) | ~p2(sK33(sK16)) | 'Ts3'(sK33(sK16)), inference(resolution, [status(thm)], [d9,c45])). % 59.99/18.17 cnf(d11, plain, ~r1(sK33(sK16),X0) | ~r1(sK53(X0),X1) | ~p2(X1) | ~p2(sK33(sK16)) | 'Ts3'(sK33(sK16)), inference(resolution, [status(thm)], [d0,d10])). % 59.99/18.17 cnf(d12, plain, p2(sK33(sK16)), inference(resolution, [status(thm)], [d8,c23])). % 59.99/18.17 cnf(d13, plain, ~r1(sK33(sK16),X0) | ~r1(sK53(X0),X1) | ~p2(X1) | 'Ts3'(sK33(sK16)), inference(resolution, [status(thm)], [d12,d11])). % 59.99/18.17 cnf(d14, plain, r1(sK33(sK16),sK18(sK33(sK16))), inference(resolution, [status(thm)], [d9,c10])). % 59.99/18.17 cnf(d15, plain, p2(sK18(sK33(sK16))) | ~'Ts3'(sK33(sK16)), inference(resolution, [status(thm)], [d14,c33])). % 59.99/18.17 cnf(d16, plain, ~p2(sK18(sK33(sK16))), inference(resolution, [status(thm)], [d9,c11])). % 59.99/18.17 cnf(d17, plain, ~'Ts3'(sK33(sK16)), inference(resolution, [status(thm)], [d16,d15])). % 59.99/18.17 cnf(d18, plain, ~r1(sK33(sK16),X0) | ~r1(sK53(X0),X1) | ~p2(X1), inference(resolution, [status(thm)], [d17,d13])). % 59.99/18.17 cnf(d19, plain, r1(sK33(sK16),sK49(sK33(sK16))) | ~'Ts4'(sK16) | 'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d9,c42])). % 59.99/18.17 cnf(d20, plain, r1(sK33(sK16),sK49(sK33(sK16))) | 'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d0,d19])). % 59.99/18.17 cnf(d21, plain, 'Ts2'(sK33(sK16)) | ~r1(X0,sK33(sK16)) | p2(sK31(sK49(sK33(sK16)))) | ~'Ts0'(X0), inference(resolution, [status(thm)], [d20,c19])). % 59.99/18.17 cnf(d22, plain, p2(sK31(sK49(sK33(sK16)))) | ~'Ts0'(sK16) | 'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d21,d9])). % 59.99/18.17 cnf(d23, plain, r1(sK16,sK44(sK16)) | 'Ts0'(sK16), inference(resolution, [status(thm)], [c38,d0])). % 59.99/18.17 cnf(d24, plain, 'Ts0'(sK16) | ~'Ts4'(sK16) | p2(sK42(sK44(sK16))), inference(resolution, [status(thm)], [d23,c35])). % 59.99/18.17 cnf(d25, plain, p2(sK42(sK44(sK16))) | 'Ts0'(sK16), inference(resolution, [status(thm)], [d0,d24])). % 59.99/18.17 cnf(d26, plain, 'Ts0'(sK16) | r1(sK44(sK16),sK42(sK44(sK16))) | ~'Ts4'(sK16), inference(resolution, [status(thm)], [d23,c34])). % 59.99/18.17 cnf(d27, plain, r1(sK44(sK16),sK42(sK44(sK16))) | 'Ts0'(sK16), inference(resolution, [status(thm)], [d0,d26])). % 59.99/18.17 cnf(d28, plain, 'Ts0'(sK16) | ~'Ts4'(sK16) | ~p2(sK42(sK44(sK16))) | 'Ts0'(sK16), inference(resolution, [status(thm)], [d27,c39])). % 59.99/18.17 cnf(d29, plain, ~p2(sK42(sK44(sK16))) | 'Ts0'(sK16), inference(resolution, [status(thm)], [d0,d28])). % 59.99/18.17 cnf(d30, plain, 'Ts0'(sK16) | 'Ts0'(sK16), inference(resolution, [status(thm)], [d29,d25])). % 59.99/18.17 cnf(d31, plain, p2(sK31(sK49(sK33(sK16)))) | 'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d30,d22])). % 59.99/18.17 cnf(d32, plain, ~r1(sK49(sK33(sK16)),X0) | ~'Ts4'(sK16) | ~p2(X0) | 'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d9,c43])). % 59.99/18.17 cnf(d33, plain, ~r1(sK49(sK33(sK16)),X0) | ~p2(X0) | 'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d0,d32])). % 59.99/18.17 cnf(d34, plain, 'Ts2'(sK33(sK16)) | r1(sK49(sK33(sK16)),sK31(sK49(sK33(sK16)))) | ~r1(X0,sK33(sK16)) | ~'Ts0'(X0), inference(resolution, [status(thm)], [d20,c18])). % 59.99/18.17 cnf(d35, plain, r1(sK49(sK33(sK16)),sK31(sK49(sK33(sK16)))) | ~'Ts0'(sK16) | 'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d34,d9])). % 59.99/18.17 cnf(d36, plain, r1(sK49(sK33(sK16)),sK31(sK49(sK33(sK16)))) | 'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d30,d35])). % 59.99/18.17 cnf(d37, plain, 'Ts2'(sK33(sK16)) | ~p2(sK31(sK49(sK33(sK16)))) | 'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d36,d33])). % 59.99/18.17 cnf(d38, plain, 'Ts2'(sK33(sK16)) | 'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d37,d31])). % 59.99/18.17 cnf(d39, plain, r1(sK33(sK16),sK35(sK33(sK16))), inference(resolution, [status(thm)], [d38,c26])). % 59.99/18.17 cnf(d40, plain, ~r1(sK53(sK35(sK33(sK16))),X0) | ~p2(X0), inference(resolution, [status(thm)], [d39,d18])). % 59.99/18.17 cnf(d41, plain, r1(sK35(sK33(sK16)),sK53(sK35(sK33(sK16)))) | ~r1(X0,sK33(sK16)) | ~'Ts4'(X0) | ~p2(sK33(sK16)) | 'Ts3'(sK33(sK16)), inference(resolution, [status(thm)], [d39,c44])). % 59.99/18.17 cnf(d42, plain, ~r1(X0,sK33(sK16)) | r1(sK35(sK33(sK16)),sK53(sK35(sK33(sK16)))) | ~'Ts4'(X0) | 'Ts3'(sK33(sK16)), inference(resolution, [status(thm)], [d12,d41])). % 59.99/18.17 cnf(d43, plain, ~r1(X0,sK33(sK16)) | r1(sK35(sK33(sK16)),sK53(sK35(sK33(sK16)))) | ~'Ts4'(X0), inference(resolution, [status(thm)], [d17,d42])). % 59.99/18.17 cnf(d44, plain, r1(sK35(sK33(sK16)),sK53(sK35(sK33(sK16)))) | ~'Ts4'(sK16), inference(resolution, [status(thm)], [d43,d9])). % 59.99/18.17 cnf(d45, plain, r1(sK35(sK33(sK16)),sK53(sK35(sK33(sK16)))), inference(resolution, [status(thm)], [d0,d44])). % 59.99/18.17 cnf(d46, plain, r1(sK53(sK35(sK33(sK16))),sK37(sK53(sK35(sK33(sK16))))) | ~'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d45,c27])). % 59.99/18.17 cnf(d47, plain, r1(sK53(sK35(sK33(sK16))),sK37(sK53(sK35(sK33(sK16))))), inference(resolution, [status(thm)], [d38,d46])). % 59.99/18.17 cnf(d48, plain, ~p2(sK37(sK53(sK35(sK33(sK16))))), inference(resolution, [status(thm)], [d47,d40])). % 59.99/18.17 cnf(d49, plain, p2(sK37(sK53(sK35(sK33(sK16))))) | ~'Ts2'(sK33(sK16)), inference(resolution, [status(thm)], [d45,c28])). % 59.99/18.17 cnf(d50, plain, p2(sK37(sK53(sK35(sK33(sK16))))), inference(resolution, [status(thm)], [d38,d49])). % 59.99/18.17 cnf(d51, plain, $false, inference(resolution, [status(thm)], [d50,d48])). % 59.99/18.17 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------