%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LCL640+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 : n020.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:54:56 AM UTC 2026 % Result : Theorem 62.32s 8.60s % Output : CNFRefutation 62.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL640+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.10/0.58 % Computer : n020.cluster.edu % 0.10/0.58 % Model : x86_64 x86_64 % 0.10/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.58 % Memory : 8046.5625MB % 0.10/0.58 % OS : Linux 6.8.0-71-generic % 0.10/0.58 % CPULimit : 300 % 0.10/0.58 % WCLimit : 300 % 0.10/0.58 % DateTime : Fri Sep 25 22:53:04 UTC 2026 % 0.10/0.58 % CPUTime : % 0.10/0.58 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 62.32/8.60 % SZS status Theorem for theBenchmark.p % 62.32/8.60 % SZS output start CNFRefutation for theBenchmark.p % 62.32/8.60 fof(main, conjecture, ~? [X0] : ~((~! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ((p1(X0) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | ~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) | ((! [X0] : ((~r1(X1,X0) | p1(X0))) | (~p1(X1) | (! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p1(X0))) | ~p1(X1)))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | (~p1(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | ~p1(X0)))) | ~((! [X0] : ((~r1(X1,X0) | p1(X0))) | ~p1(X1))))))))))))) & ((p1(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) | p1(X0))) | ~p1(X1))))))))) & (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | p1(X1)))))) & (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | ~p1(X0))))))))) | ~! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p1(X0))) | ~p1(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))))) | ~! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p1(X0))) | ~p1(X1))))))))))))))) & (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ((p1(X0) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | ~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) | ((p1(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) | p1(X0))) | ~p1(X1))))))))) & ! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | p1(X1)))))))))))))))). % 62.32/8.60 fof(negated_conjecture, negated_conjecture, ~~? [X0] : ~((~! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ((p1(X0) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | ~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) | ((! [X0] : ((~r1(X1,X0) | p1(X0))) | (~p1(X1) | (! [X0] : ((~r1(X1,X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p1(X0))) | ~p1(X1)))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | (~p1(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | ~p1(X0)))) | ~((! [X0] : ((~r1(X1,X0) | p1(X0))) | ~p1(X1))))))))))))) & ((p1(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) | p1(X0))) | ~p1(X1))))))))) & (! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | p1(X1)))))) & (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | ~p1(X0))))))))) | ~! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p1(X0))) | ~p1(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))))) | ~! [X0] : ((~r1(X1,X0) | (p1(X0) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | p1(X0))) | ~p1(X1))))))))))))))) & (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ((p1(X0) | (! [X1] : ((~r1(X0,X1) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | (p1(X1) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | p1(X1))) | ~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) | ((p1(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) | p1(X0))) | ~p1(X1))))))))) & ! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | p1(X1))))))))))))))), inference(negate_conjecture, [status(cth)], [main])). % 62.32/8.60 cnf(c4, plain, ~r1(sK7,X0) | ~r1(X0,X1) | ~r1(X1,X2) | X3(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c5, plain, r1(sK7,sK21), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c6, plain, r1(sK21,sK22), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c7, plain, r1(sK22,sK23), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c8, plain, r1(sK23,sK24), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c9, plain, ~p1(sK24), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c10, plain, r1(sK23,sK25), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c11, plain, ~r1(sK25,X0) | p1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c12, plain, ~r1(sK23,X0) | p1(X0) | r1(X0,sK28(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c13, plain, ~r1(sK23,X0) | p1(X0) | r1(sK28(X0),sK29(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c14, plain, ~r1(sK23,X0) | p1(X0) | ~p1(sK29(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c15, plain, ~r1(sK23,X0) | p1(X0) | p1(sK28(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c27, plain, ~X0(X1) | r1(X1,sK48(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c28, plain, ~X0(X1) | r1(sK48(X1),sK49(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c29, plain, ~X0(X1) | ~p1(sK49(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c33, plain, ~r1(X0,X1) | ~X2(X3) | ~r1(X1,X4) | ~r1(sK48(X3),X0) | p1(X0) | p1(X4) | ~p1(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c34, plain, ~X0(X1) | r1(X1,sK54(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c35, plain, ~X0(X1) | ~p1(sK54(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c36, plain, ~p1(X0) | p1(X1) | ~r1(X0,X1) | ~X2(X3) | ~r1(sK54(X3),X0), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c37, plain, ~r1(X0,X1) | p1(X1) | ~r1(X2,X0) | r1(X1,sK59(X1)) | ~X3(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c38, plain, ~r1(X0,X1) | ~X2(X3) | r1(sK59(X1),sK60(X1)) | p1(X1) | ~r1(X3,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c39, plain, ~r1(X0,X1) | ~X2(X3) | ~p1(sK60(X1)) | p1(X1) | ~r1(X3,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c40, plain, ~r1(X0,X1) | ~X2(X3) | p1(sK59(X1)) | p1(X1) | ~r1(X3,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c41, plain, ~X0(X1) | r1(X2,sK63(X2)) | ~p1(X1) | ~r1(X1,X3) | X4(X1) | ~r1(X1,X2) | p1(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c42, plain, ~X0(X1) | ~p1(X1) | r1(sK63(X2),sK64(X2)) | ~r1(X1,X3) | X4(X1) | ~r1(X1,X2) | p1(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c43, plain, ~p1(sK64(X0)) | ~X1(X2) | ~p1(X2) | ~r1(X2,X3) | X4(X2) | ~r1(X2,X0) | p1(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c45, plain, ~X0(X1) | p1(X1) | r1(X2,sK66(X2)) | ~r1(X1,X2) | X3(X1), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c46, plain, p1(X0) | ~r1(X0,X1) | X2(X0) | ~p1(sK66(X1)) | ~X3(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c47, plain, p1(X0) | ~X1(X2) | ~r1(X2,X3) | ~r1(X4,X0) | r1(X3,sK70(X3)) | ~r1(X3,X4), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c48, plain, p1(X0) | ~X1(X2) | ~r1(X2,X3) | ~r1(X4,X0) | ~p1(sK70(X3)) | ~r1(X3,X4), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c49, plain, ~X0(X1) | X2(X1) | r1(X1,sK71(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c50, plain, ~X0(X1) | X2(X1) | ~p1(sK71(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(c51, plain, ~X0(X1) | ~r1(sK71(X1),X2) | X3(X1) | ~p1(X2) | p1(X4) | ~r1(X2,X4), inference(clausification, [status(esa)], [negated_conjecture])). % 62.32/8.60 cnf(d0, plain, ~r1(sK23,X0) | r1(sK63(X0),sK64(X0)) | p1(sK24) | ~p1(sK23) | ~'Ts4'(sK23) | 'Ts1'(sK23), inference(resolution, [status(thm)], [c42,c8])). % 62.32/8.60 cnf(d1, plain, ~r1(sK23,X0) | r1(sK63(X0),sK64(X0)) | ~p1(sK23) | ~'Ts4'(sK23) | 'Ts1'(sK23), inference(resolution, [status(thm)], [c9,d0])). % 62.32/8.60 cnf(d2, plain, ~r1(X0,X1) | ~r1(sK21,X0) | 'Ts4'(X1), inference(resolution, [status(thm)], [c4,c5])). % 62.32/8.60 cnf(d3, plain, ~r1(sK22,X0) | 'Ts4'(X0), inference(resolution, [status(thm)], [d2,c6])). % 62.32/8.60 cnf(d4, plain, 'Ts4'(sK23), inference(resolution, [status(thm)], [d3,c7])). % 62.32/8.60 cnf(d5, plain, ~r1(sK23,X0) | r1(sK63(X0),sK64(X0)) | ~p1(sK23) | 'Ts1'(sK23), inference(resolution, [status(thm)], [d4,d1])). % 62.32/8.60 cnf(d6, plain, r1(sK25,sK66(sK25)) | p1(sK23) | ~'Ts4'(sK23) | 'Ts2'(sK23), inference(resolution, [status(thm)], [c45,c10])). % 62.32/8.60 cnf(d7, plain, r1(sK25,sK66(sK25)) | p1(sK23) | 'Ts2'(sK23), inference(resolution, [status(thm)], [d4,d6])). % 62.32/8.60 cnf(d8, plain, p1(sK23) | 'Ts2'(sK23) | p1(sK66(sK25)), inference(resolution, [status(thm)], [d7,c11])). % 62.32/8.60 cnf(d9, plain, p1(sK23) | 'Ts2'(sK23) | ~r1(X0,sK25) | p1(X0) | ~'Ts4'(X0) | 'Ts2'(X0), inference(resolution, [status(thm)], [d8,c46])). % 62.32/8.60 cnf(d10, plain, p1(sK23) | p1(sK23) | ~'Ts4'(sK23) | 'Ts2'(sK23) | 'Ts2'(sK23), inference(resolution, [status(thm)], [d9,c10])). % 62.32/8.60 cnf(d11, plain, p1(sK23) | 'Ts2'(sK23), inference(resolution, [status(thm)], [d4,d10])). % 62.32/8.60 cnf(d12, plain, ~'Ts2'(sK23) | p1(sK54(sK23)) | p1(sK28(sK54(sK23))), inference(resolution, [status(thm)], [c34,c15])). % 62.32/8.60 cnf(d13, plain, ~r1(sK28(sK54(X0)),X1) | p1(X1) | ~p1(sK28(sK54(X0))) | ~'Ts2'(X0) | ~r1(sK23,sK54(X0)) | p1(sK54(X0)), inference(resolution, [status(thm)], [c36,c12])). % 62.32/8.60 cnf(d14, plain, ~r1(sK23,sK54(X0)) | p1(sK29(sK54(X0))) | ~p1(sK28(sK54(X0))) | p1(sK54(X0)) | ~'Ts2'(X0) | ~r1(sK23,sK54(X0)) | p1(sK54(X0)), inference(resolution, [status(thm)], [d13,c13])). % 62.32/8.60 cnf(d15, plain, ~r1(sK23,sK54(sK23)) | p1(sK29(sK54(sK23))) | p1(sK54(sK23)) | ~'Ts2'(sK23) | p1(sK54(sK23)) | ~'Ts2'(sK23), inference(resolution, [status(thm)], [d14,d12])). % 62.32/8.60 cnf(d16, plain, p1(sK29(sK54(sK23))) | p1(sK54(sK23)) | ~'Ts2'(sK23) | ~'Ts2'(sK23), inference(resolution, [status(thm)], [d15,c34])). % 62.32/8.60 cnf(d17, plain, p1(sK54(sK23)) | ~'Ts2'(sK23) | ~r1(sK23,sK54(sK23)) | p1(sK54(sK23)), inference(resolution, [status(thm)], [d16,c14])). % 62.32/8.60 cnf(d18, plain, p1(sK54(sK23)) | ~'Ts2'(sK23) | ~'Ts2'(sK23), inference(resolution, [status(thm)], [d17,c34])). % 62.32/8.60 cnf(d19, plain, ~'Ts2'(sK23) | ~'Ts2'(sK23), inference(resolution, [status(thm)], [d18,c35])). % 62.32/8.60 cnf(d20, plain, p1(sK23), inference(resolution, [status(thm)], [d19,d11])). % 62.32/8.60 cnf(d21, plain, ~r1(sK23,X0) | r1(sK63(X0),sK64(X0)) | 'Ts1'(sK23), inference(resolution, [status(thm)], [d20,d5])). % 62.32/8.60 cnf(d22, plain, ~'Ts4'(sK23) | 'Ts3'(sK23) | p1(sK71(sK23)) | p1(sK28(sK71(sK23))), inference(resolution, [status(thm)], [c49,c15])). % 62.32/8.60 cnf(d23, plain, p1(sK28(sK71(sK23))) | p1(sK71(sK23)) | 'Ts3'(sK23), inference(resolution, [status(thm)], [d4,d22])). % 62.32/8.60 cnf(d24, plain, ~r1(sK28(sK71(X0)),X1) | p1(X1) | ~p1(sK28(sK71(X0))) | ~'Ts4'(X0) | 'Ts3'(X0) | ~r1(sK23,sK71(X0)) | p1(sK71(X0)), inference(resolution, [status(thm)], [c51,c12])). % 62.32/8.60 cnf(d25, plain, ~r1(sK23,sK71(X0)) | p1(sK29(sK71(X0))) | ~p1(sK28(sK71(X0))) | p1(sK71(X0)) | ~'Ts4'(X0) | 'Ts3'(X0) | ~r1(sK23,sK71(X0)) | p1(sK71(X0)), inference(resolution, [status(thm)], [d24,c13])). % 62.32/8.60 cnf(d26, plain, ~r1(sK23,sK71(sK23)) | p1(sK29(sK71(sK23))) | p1(sK71(sK23)) | ~'Ts4'(sK23) | 'Ts3'(sK23) | p1(sK71(sK23)) | 'Ts3'(sK23), inference(resolution, [status(thm)], [d25,d23])). % 62.32/8.60 cnf(d27, plain, ~r1(sK23,sK71(sK23)) | p1(sK29(sK71(sK23))) | p1(sK71(sK23)) | 'Ts3'(sK23), inference(resolution, [status(thm)], [d4,d26])). % 62.32/8.60 cnf(d28, plain, p1(sK29(sK71(sK23))) | p1(sK71(sK23)) | 'Ts3'(sK23) | ~'Ts4'(sK23) | 'Ts3'(sK23), inference(resolution, [status(thm)], [d27,c49])). % 62.32/8.60 cnf(d29, plain, p1(sK29(sK71(sK23))) | p1(sK71(sK23)) | 'Ts3'(sK23), inference(resolution, [status(thm)], [d4,d28])). % 62.32/8.60 cnf(d30, plain, p1(sK71(sK23)) | 'Ts3'(sK23) | ~r1(sK23,sK71(sK23)) | p1(sK71(sK23)), inference(resolution, [status(thm)], [d29,c14])). % 62.32/8.60 cnf(d31, plain, p1(sK71(sK23)) | 'Ts3'(sK23) | ~'Ts4'(sK23) | 'Ts3'(sK23), inference(resolution, [status(thm)], [d30,c49])). % 62.32/8.60 cnf(d32, plain, p1(sK71(sK23)) | 'Ts3'(sK23), inference(resolution, [status(thm)], [d4,d31])). % 62.32/8.60 cnf(d33, plain, 'Ts3'(sK23) | ~'Ts4'(sK23) | 'Ts3'(sK23), inference(resolution, [status(thm)], [d32,c50])). % 62.32/8.60 cnf(d34, plain, 'Ts3'(sK23), inference(resolution, [status(thm)], [d4,d33])). % 62.32/8.60 cnf(d35, plain, ~r1(X0,sK48(X1)) | p1(sK49(X1)) | p1(sK59(sK49(X1))) | ~'Ts3'(X0) | ~'Ts1'(X1), inference(resolution, [status(thm)], [c40,c28])). % 62.32/8.60 cnf(d36, plain, p1(sK49(X0)) | p1(sK59(sK49(X0))) | ~'Ts1'(X0) | ~'Ts3'(X0) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d35,c27])). % 62.32/8.60 cnf(d37, plain, ~r1(X0,sK48(X1)) | r1(sK59(sK49(X1)),sK60(sK49(X1))) | p1(sK49(X1)) | ~'Ts3'(X0) | ~'Ts1'(X1), inference(resolution, [status(thm)], [c38,c28])). % 62.32/8.60 cnf(d38, plain, r1(sK59(sK49(X0)),sK60(sK49(X0))) | p1(sK49(X0)) | ~'Ts1'(X0) | ~'Ts3'(X0) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d37,c27])). % 62.32/8.60 cnf(d39, plain, ~r1(X0,X1) | ~r1(sK49(X2),X0) | p1(X1) | ~p1(X0) | p1(sK49(X2)) | ~'Ts1'(X2) | ~'Ts1'(X2), inference(resolution, [status(thm)], [c33,c28])). % 62.32/8.60 cnf(d40, plain, ~r1(X0,sK48(X1)) | r1(sK49(X1),sK59(sK49(X1))) | p1(sK49(X1)) | ~'Ts3'(X0) | ~'Ts1'(X1), inference(resolution, [status(thm)], [c37,c28])). % 62.32/8.60 cnf(d41, plain, r1(sK49(X0),sK59(sK49(X0))) | p1(sK49(X0)) | ~'Ts1'(X0) | ~'Ts3'(X0) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d40,c27])). % 62.32/8.60 cnf(d42, plain, p1(sK49(X0)) | ~'Ts1'(X0) | ~'Ts3'(X0) | ~r1(sK59(sK49(X0)),X1) | p1(X1) | ~p1(sK59(sK49(X0))) | p1(sK49(X0)) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d41,d39])). % 62.32/8.60 cnf(d43, plain, p1(sK60(sK49(X0))) | p1(sK49(X0)) | ~p1(sK59(sK49(X0))) | ~'Ts1'(X0) | ~'Ts3'(X0) | p1(sK49(X0)) | ~'Ts1'(X0) | ~'Ts3'(X0), inference(resolution, [status(thm)], [d42,d38])). % 62.32/8.60 cnf(d44, plain, p1(sK49(X0)) | p1(sK60(sK49(X0))) | ~'Ts1'(X0) | ~'Ts3'(X0) | p1(sK49(X0)) | ~'Ts1'(X0) | ~'Ts3'(X0), inference(resolution, [status(thm)], [d43,d36])). % 62.32/8.60 cnf(d45, plain, p1(sK49(X0)) | ~'Ts1'(X0) | ~'Ts3'(X0) | ~r1(X1,X2) | ~r1(X2,sK49(X0)) | p1(sK49(X0)) | ~'Ts3'(X1), inference(resolution, [status(thm)], [d44,c39])). % 62.32/8.60 cnf(d46, plain, ~r1(X0,sK48(X1)) | p1(sK49(X1)) | ~'Ts1'(X1) | ~'Ts3'(X0) | ~'Ts3'(X1) | ~'Ts1'(X1), inference(resolution, [status(thm)], [d45,c28])). % 62.32/8.60 cnf(d47, plain, p1(sK49(X0)) | ~'Ts1'(X0) | ~'Ts3'(X0) | ~'Ts3'(X0) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d46,c27])). % 62.32/8.60 cnf(d48, plain, ~'Ts1'(X0) | ~'Ts3'(X0) | ~'Ts1'(X0), inference(resolution, [status(thm)], [d47,c29])). % 62.32/8.60 cnf(d49, plain, ~'Ts1'(sK23), inference(resolution, [status(thm)], [d48,d34])). % 62.32/8.60 cnf(d50, plain, ~r1(sK23,X0) | r1(sK63(X0),sK64(X0)), inference(resolution, [status(thm)], [d49,d21])). % 62.32/8.60 cnf(d51, plain, r1(X0,sK63(X0)) | ~r1(sK23,X0) | p1(sK24) | ~p1(sK23) | ~'Ts4'(sK23) | 'Ts1'(sK23), inference(resolution, [status(thm)], [c41,c8])). % 62.32/8.60 cnf(d52, plain, r1(X0,sK63(X0)) | ~r1(sK23,X0) | ~p1(sK23) | ~'Ts4'(sK23) | 'Ts1'(sK23), inference(resolution, [status(thm)], [c9,d51])). % 62.32/8.60 cnf(d53, plain, r1(X0,sK63(X0)) | ~r1(sK23,X0) | ~p1(sK23) | 'Ts1'(sK23), inference(resolution, [status(thm)], [d4,d52])). % 62.32/8.60 cnf(d54, plain, r1(X0,sK63(X0)) | ~r1(sK23,X0) | 'Ts1'(sK23), inference(resolution, [status(thm)], [d20,d53])). % 62.32/8.60 cnf(d55, plain, r1(X0,sK63(X0)) | ~r1(sK23,X0), inference(resolution, [status(thm)], [d49,d54])). % 62.32/8.60 cnf(d56, plain, ~r1(sK25,X0) | r1(sK25,sK70(sK25)) | ~r1(X0,X1) | p1(X1) | ~'Ts4'(sK23), inference(resolution, [status(thm)], [c47,c10])). % 62.32/8.60 cnf(d57, plain, ~r1(X0,X1) | ~r1(sK25,X0) | r1(sK25,sK70(sK25)) | p1(X1), inference(resolution, [status(thm)], [d4,d56])). % 62.32/8.60 cnf(d58, plain, ~r1(sK23,sK25) | 'Ts1'(sK23) | ~r1(sK63(sK25),X0) | r1(sK25,sK70(sK25)) | p1(X0), inference(resolution, [status(thm)], [d54,d57])). % 62.32/8.60 cnf(d59, plain, r1(sK25,sK70(sK25)) | ~r1(sK63(sK25),X0) | p1(X0) | 'Ts1'(sK23), inference(resolution, [status(thm)], [c10,d58])). % 62.32/8.60 cnf(d60, plain, r1(sK25,sK70(sK25)) | p1(sK64(sK25)) | 'Ts1'(sK23) | ~r1(sK23,sK25) | 'Ts1'(sK23), inference(resolution, [status(thm)], [d59,d21])). % 62.32/8.60 cnf(d61, plain, r1(sK25,sK70(sK25)) | p1(sK64(sK25)) | 'Ts1'(sK23), inference(resolution, [status(thm)], [c10,d60])). % 62.32/8.60 cnf(d62, plain, p1(sK64(sK25)) | 'Ts1'(sK23) | p1(sK70(sK25)), inference(resolution, [status(thm)], [d61,c11])). % 62.32/8.60 cnf(d63, plain, p1(sK64(sK25)) | p1(sK70(sK25)), inference(resolution, [status(thm)], [d49,d62])). % 62.32/8.60 cnf(d64, plain, p1(sK64(sK25)) | ~r1(X0,X1) | ~r1(X2,sK25) | ~r1(sK25,X0) | p1(X1) | ~'Ts4'(X2), inference(resolution, [status(thm)], [d63,c48])). % 62.32/8.60 cnf(d65, plain, ~r1(X0,sK25) | ~r1(sK63(sK25),X1) | p1(X1) | p1(sK64(sK25)) | ~'Ts4'(X0) | ~r1(sK23,sK25), inference(resolution, [status(thm)], [d64,d55])). % 62.32/8.60 cnf(d66, plain, ~r1(X0,sK25) | ~r1(sK63(sK25),X1) | p1(X1) | p1(sK64(sK25)) | ~'Ts4'(X0), inference(resolution, [status(thm)], [c10,d65])). % 62.32/8.60 cnf(d67, plain, ~r1(X0,sK25) | p1(sK64(sK25)) | p1(sK64(sK25)) | ~'Ts4'(X0) | ~r1(sK23,sK25), inference(resolution, [status(thm)], [d66,d50])). % 62.32/8.60 cnf(d68, plain, ~r1(X0,sK25) | p1(sK64(sK25)) | ~'Ts4'(X0), inference(resolution, [status(thm)], [c10,d67])). % 62.32/8.60 cnf(d69, plain, p1(sK64(sK25)) | ~'Ts4'(sK23), inference(resolution, [status(thm)], [d68,c10])). % 62.32/8.60 cnf(d70, plain, p1(sK64(sK25)), inference(resolution, [status(thm)], [d4,d69])). % 62.32/8.60 cnf(d71, plain, ~r1(X0,X1) | ~r1(X0,sK25) | p1(X1) | ~p1(X0) | ~'Ts4'(X0) | 'Ts1'(X0), inference(resolution, [status(thm)], [d70,c43])). % 62.32/8.60 cnf(d72, plain, ~r1(sK23,X0) | p1(X0) | ~p1(sK23) | ~'Ts4'(sK23) | 'Ts1'(sK23), inference(resolution, [status(thm)], [d71,c10])). % 62.32/8.60 cnf(d73, plain, ~r1(sK23,X0) | p1(X0) | ~p1(sK23) | 'Ts1'(sK23), inference(resolution, [status(thm)], [d4,d72])). % 62.32/8.60 cnf(d74, plain, ~r1(sK23,X0) | p1(X0) | 'Ts1'(sK23), inference(resolution, [status(thm)], [d20,d73])). % 62.32/8.60 cnf(d75, plain, ~r1(sK23,X0) | p1(X0), inference(resolution, [status(thm)], [d49,d74])). % 62.32/8.60 cnf(d76, plain, p1(sK24), inference(resolution, [status(thm)], [d75,c8])). % 62.32/8.60 cnf(d77, plain, $false, inference(resolution, [status(thm)], [c9,d76])). % 62.32/8.60 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------