%------------------------------------------------------------------------------ % File : LisaST---0.9 % Problem : LCL670+1.005 : 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 : n015.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:08 AM UTC 2026 % Result : Theorem 187.86s 34.36s % Output : CNFRefutation 187.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL670+1.005 : 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/5.38 % Computer : n015.cluster.edu % 0.08/5.38 % Model : x86_64 x86_64 % 0.08/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/5.38 % Memory : 8046.5625MB % 0.08/5.38 % OS : Linux 6.8.0-71-generic % 0.08/5.38 % CPULimit : 300 % 0.08/5.38 % WCLimit : 300 % 0.08/5.38 % DateTime : Fri Sep 25 23:14:33 UTC 2026 % 0.08/5.38 % CPUTime : % 0.08/5.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 187.86/34.36 % SZS status Theorem for theBenchmark.p % 187.86/34.36 % SZS output start CNFRefutation for theBenchmark.p % 187.86/34.36 fof(reflexivity, axiom, ! [X0] : r1(X0,X0)). % 187.86/34.36 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) | ~((~! [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))))))))))) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | p1(X0))))))))))) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | p1(X1))))))))))) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | p1(X0))))))))))) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | p1(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) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) | ! [X1] : ((~r1(X0,X1) | p1(X1)))))) | (! [X0] : ((~r1(X1,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))))) | ! [X1] : ((~r1(X0,X1) | p1(X1)))))) | (! [X0] : ((~r1(X1,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)))))))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | ~p1(X1)))))))))) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~p1(X1))))) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0)))))))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | ~p1(X1)))))))))) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~p1(X1))))) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0))))))))))))). % 187.86/34.36 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) | ~((~! [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))))))))))) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | p1(X0))))))))))) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | p1(X1))))))))))) | ~! [X1] : ((~r1(X0,X1) | ~((~! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | p1(X1))))) & ! [X0] : ((~r1(X1,X0) | p1(X0))))))))))) | ~! [X0] : ((~r1(X1,X0) | ~((~! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | p1(X0))))) & ! [X1] : ((~r1(X0,X1) | p1(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) | ~! [X0] : ((~r1(X1,X0) | p1(X0))))) | ! [X1] : ((~r1(X0,X1) | p1(X1)))))) | (! [X0] : ((~r1(X1,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))))) | ! [X1] : ((~r1(X0,X1) | p1(X1)))))) | (! [X0] : ((~r1(X1,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)))))))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | ~p1(X1)))))))))) | ~! [X1] : ((~r1(X0,X1) | (! [X0] : ((~r1(X1,X0) | ! [X1] : ((~r1(X0,X1) | ~p1(X1))))) | ~! [X0] : ((~r1(X1,X0) | ~p1(X0)))))))))) | ~! [X0] : ((~r1(X1,X0) | (! [X1] : ((~r1(X0,X1) | ! [X0] : ((~r1(X1,X0) | ~p1(X0))))) | ~! [X1] : ((~r1(X0,X1) | ~p1(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])). % 187.86/34.36 cnf(c0, plain, r1(X0,X0), inference(clausification, [status(esa)], [reflexivity])). % 187.86/34.36 cnf(c4, plain, r1(sK6,sK12), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c5, plain, r1(sK12,sK13), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c6, plain, r1(sK13,sK14), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c7, plain, r1(sK14,sK15), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c8, plain, r1(sK15,sK16), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c9, plain, ~r1(sK16,X0) | r1(X0,sK18(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c10, plain, ~r1(sK16,X0) | ~p2(sK18(X0)), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c46, plain, ~r1(sK6,X0) | X1(X0), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c47, plain, ~X0(X1) | ~r1(X1,X2) | ~r1(X2,X3) | r1(X3,sK62(X3)), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c48, plain, ~X0(X1) | ~r1(X1,X2) | ~r1(X2,X3) | p2(sK62(X3)), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c53, plain, ~X0(X1) | ~r1(X1,X2) | p2(X2), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c54, plain, ~X0(X1) | ~r1(X1,X2) | r1(X2,sK67(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c55, plain, ~X0(X1) | ~r1(X1,X2) | p2(sK67(X2)), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c58, plain, ~X0(X1) | X2(X1) | r1(X1,sK69(X1)), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c59, plain, ~X0(X1) | X2(X1) | ~r1(sK69(X1),X3) | ~p2(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c60, plain, ~r1(X0,X1) | ~X2(X3) | ~p2(X0) | r1(X1,sK73(X1)) | X4(X0) | ~r1(X3,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c61, plain, ~r1(X0,X1) | ~r1(sK73(X1),X2) | ~X3(X4) | ~p2(X2) | ~p2(X0) | X5(X0) | ~r1(X4,X0), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c62, plain, ~X0(X1) | ~r1(X1,X2) | ~r1(X2,X3) | X4(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(c67, plain, ~X0(X1) | ~r1(X1,X2) | ~r1(X2,X3) | X4(X3), inference(clausification, [status(esa)], [negated_conjecture])). % 187.86/34.36 cnf(d0, plain, r1(sK16,sK67(sK16)) | ~'Ts3'(sK15), inference(resolution, [status(thm)], [c54,c8])). % 187.86/34.36 cnf(d1, plain, ~r1(X0,sK14) | 'Ts3'(sK15) | ~'Ts4'(X0), inference(resolution, [status(thm)], [c62,c7])). % 187.86/34.36 cnf(d2, plain, 'Ts3'(sK15) | ~'Ts4'(sK13), inference(resolution, [status(thm)], [d1,c6])). % 187.86/34.36 cnf(d3, plain, ~r1(X0,X1) | ~'Ts5'(X0) | 'Ts4'(X1), inference(resolution, [status(thm)], [c67,c0])). % 187.86/34.36 cnf(d4, plain, ~'Ts5'(sK12) | 'Ts4'(sK13), inference(resolution, [status(thm)], [d3,c5])). % 187.86/34.36 cnf(d5, plain, 'Ts5'(sK12), inference(resolution, [status(thm)], [c46,c4])). % 187.86/34.36 cnf(d6, plain, 'Ts4'(sK13), inference(resolution, [status(thm)], [d5,d4])). % 187.86/34.36 cnf(d7, plain, 'Ts3'(sK15), inference(resolution, [status(thm)], [d6,d2])). % 187.86/34.36 cnf(d8, plain, r1(sK16,sK67(sK16)), inference(resolution, [status(thm)], [d7,d0])). % 187.86/34.36 cnf(d9, plain, ~r1(sK67(sK16),X0) | ~r1(sK73(X0),X1) | ~p2(X1) | ~p2(sK67(sK16)) | 'Ts2'(sK67(sK16)) | ~'Ts3'(sK16), inference(resolution, [status(thm)], [d8,c61])). % 187.86/34.36 cnf(d10, plain, p2(sK67(sK16)) | ~'Ts3'(sK15), inference(resolution, [status(thm)], [c55,c8])). % 187.86/34.36 cnf(d11, plain, p2(sK67(sK16)), inference(resolution, [status(thm)], [d7,d10])). % 187.86/34.36 cnf(d12, plain, ~r1(sK67(sK16),X0) | ~r1(sK73(X0),X1) | ~p2(X1) | 'Ts2'(sK67(sK16)) | ~'Ts3'(sK16), inference(resolution, [status(thm)], [d11,d9])). % 187.86/34.36 cnf(d13, plain, ~r1(X0,sK15) | 'Ts3'(sK16) | ~'Ts4'(X0), inference(resolution, [status(thm)], [c62,c8])). % 187.86/34.36 cnf(d14, plain, 'Ts3'(sK16) | ~'Ts4'(sK14), inference(resolution, [status(thm)], [d13,c7])). % 187.86/34.36 cnf(d15, plain, ~r1(X0,sK13) | ~'Ts5'(X0) | 'Ts4'(sK14), inference(resolution, [status(thm)], [c67,c6])). % 187.86/34.36 cnf(d16, plain, ~'Ts5'(sK12) | 'Ts4'(sK14), inference(resolution, [status(thm)], [d15,c5])). % 187.86/34.36 cnf(d17, plain, 'Ts4'(sK14), inference(resolution, [status(thm)], [d5,d16])). % 187.86/34.36 cnf(d18, plain, 'Ts3'(sK16), inference(resolution, [status(thm)], [d17,d14])). % 187.86/34.36 cnf(d19, plain, ~r1(sK67(sK16),X0) | ~r1(sK73(X0),X1) | ~p2(X1) | 'Ts2'(sK67(sK16)), inference(resolution, [status(thm)], [d18,d12])). % 187.86/34.36 cnf(d20, plain, r1(sK67(sK16),sK18(sK67(sK16))), inference(resolution, [status(thm)], [d8,c9])). % 187.86/34.36 cnf(d21, plain, p2(sK18(sK67(sK16))) | ~'Ts2'(sK67(sK16)), inference(resolution, [status(thm)], [d20,c53])). % 187.86/34.36 cnf(d22, plain, ~p2(sK18(sK67(sK16))), inference(resolution, [status(thm)], [d8,c10])). % 187.86/34.36 cnf(d23, plain, ~'Ts2'(sK67(sK16)), inference(resolution, [status(thm)], [d22,d21])). % 187.86/34.36 cnf(d24, plain, ~r1(sK67(sK16),X0) | ~r1(sK73(X0),X1) | ~p2(X1), inference(resolution, [status(thm)], [d23,d19])). % 187.86/34.36 cnf(d25, plain, ~r1(sK73(sK67(sK16)),X0) | ~p2(X0), inference(resolution, [status(thm)], [d24,c0])). % 187.86/34.36 cnf(d26, plain, r1(X0,sK73(X0)) | ~r1(X1,X0) | ~p2(X0) | 'Ts2'(X0) | ~'Ts3'(X1), inference(resolution, [status(thm)], [c60,c0])). % 187.86/34.36 cnf(d27, plain, r1(sK67(sK16),sK73(sK67(sK16))) | ~p2(sK67(sK16)) | 'Ts2'(sK67(sK16)) | ~'Ts3'(sK16), inference(resolution, [status(thm)], [d8,d26])). % 187.86/34.36 cnf(d28, plain, r1(sK67(sK16),sK73(sK67(sK16))) | 'Ts2'(sK67(sK16)) | ~'Ts3'(sK16), inference(resolution, [status(thm)], [d11,d27])). % 187.86/34.36 cnf(d29, plain, r1(sK67(sK16),sK73(sK67(sK16))) | 'Ts2'(sK67(sK16)), inference(resolution, [status(thm)], [d18,d28])). % 187.86/34.36 cnf(d30, plain, r1(sK67(sK16),sK73(sK67(sK16))), inference(resolution, [status(thm)], [d23,d29])). % 187.86/34.36 cnf(d31, plain, r1(X0,sK62(X0)) | ~r1(sK67(sK16),X0) | ~'Ts1'(sK16), inference(resolution, [status(thm)], [d8,c47])). % 187.86/34.36 cnf(d32, plain, ~r1(sK16,X0) | p2(sK62(X0)) | ~'Ts1'(sK15), inference(resolution, [status(thm)], [c48,c8])). % 187.86/34.36 cnf(d33, plain, r1(sK16,sK69(sK16)) | 'Ts1'(sK16), inference(resolution, [status(thm)], [d18,c58])). % 187.86/34.36 cnf(d34, plain, 'Ts1'(sK16) | p2(sK62(sK69(sK16))) | ~'Ts1'(sK15), inference(resolution, [status(thm)], [d33,d32])). % 187.86/34.36 cnf(d35, plain, ~r1(sK15,X0) | p2(sK62(X0)) | ~'Ts1'(sK14), inference(resolution, [status(thm)], [c48,c7])). % 187.86/34.36 cnf(d36, plain, r1(sK15,sK69(sK15)) | 'Ts1'(sK15), inference(resolution, [status(thm)], [d7,c58])). % 187.86/34.36 cnf(d37, plain, 'Ts1'(sK15) | p2(sK62(sK69(sK15))) | ~'Ts1'(sK14), inference(resolution, [status(thm)], [d36,d35])). % 187.86/34.36 cnf(d38, plain, ~r1(X0,sK13) | 'Ts3'(sK14) | ~'Ts4'(X0), inference(resolution, [status(thm)], [c62,c6])). % 187.86/34.36 cnf(d39, plain, 'Ts3'(sK14) | ~'Ts4'(sK12), inference(resolution, [status(thm)], [d38,c5])). % 187.86/34.36 cnf(d40, plain, ~'Ts5'(X0) | 'Ts4'(X0), inference(resolution, [status(thm)], [d3,c0])). % 187.86/34.36 cnf(d41, plain, 'Ts4'(sK12), inference(resolution, [status(thm)], [d40,d5])). % 187.86/34.36 cnf(d42, plain, 'Ts3'(sK14), inference(resolution, [status(thm)], [d41,d39])). % 187.86/34.36 cnf(d43, plain, r1(sK14,sK69(sK14)) | 'Ts1'(sK14), inference(resolution, [status(thm)], [d42,c58])). % 187.86/34.36 cnf(d44, plain, 'Ts1'(sK14) | p2(sK67(sK69(sK14))) | ~'Ts3'(sK14), inference(resolution, [status(thm)], [d43,c55])). % 187.86/34.36 cnf(d45, plain, p2(sK67(sK69(sK14))) | 'Ts1'(sK14), inference(resolution, [status(thm)], [d42,d44])). % 187.86/34.36 cnf(d46, plain, 'Ts1'(sK14) | r1(sK69(sK14),sK67(sK69(sK14))) | ~'Ts3'(sK14), inference(resolution, [status(thm)], [d43,c54])). % 187.86/34.36 cnf(d47, plain, r1(sK69(sK14),sK67(sK69(sK14))) | 'Ts1'(sK14), inference(resolution, [status(thm)], [d42,d46])). % 187.86/34.36 cnf(d48, plain, 'Ts1'(sK14) | ~p2(sK67(sK69(sK14))) | 'Ts1'(sK14) | ~'Ts3'(sK14), inference(resolution, [status(thm)], [d47,c59])). % 187.86/34.36 cnf(d49, plain, ~p2(sK67(sK69(sK14))) | 'Ts1'(sK14), inference(resolution, [status(thm)], [d42,d48])). % 187.86/34.36 cnf(d50, plain, 'Ts1'(sK14) | 'Ts1'(sK14), inference(resolution, [status(thm)], [d49,d45])). % 187.86/34.36 cnf(d51, plain, p2(sK62(sK69(sK15))) | 'Ts1'(sK15), inference(resolution, [status(thm)], [d50,d37])). % 187.86/34.36 cnf(d52, plain, r1(X0,sK62(X0)) | ~r1(sK15,X0) | ~'Ts1'(sK14), inference(resolution, [status(thm)], [c47,c7])). % 187.86/34.36 cnf(d53, plain, 'Ts1'(sK15) | r1(sK69(sK15),sK62(sK69(sK15))) | ~'Ts1'(sK14), inference(resolution, [status(thm)], [d36,d52])). % 187.86/34.36 cnf(d54, plain, r1(sK69(sK15),sK62(sK69(sK15))) | 'Ts1'(sK15), inference(resolution, [status(thm)], [d50,d53])). % 187.86/34.36 cnf(d55, plain, 'Ts1'(sK15) | ~p2(sK62(sK69(sK15))) | 'Ts1'(sK15) | ~'Ts3'(sK15), inference(resolution, [status(thm)], [d54,c59])). % 187.86/34.36 cnf(d56, plain, ~p2(sK62(sK69(sK15))) | 'Ts1'(sK15), inference(resolution, [status(thm)], [d7,d55])). % 187.86/34.36 cnf(d57, plain, 'Ts1'(sK15) | 'Ts1'(sK15), inference(resolution, [status(thm)], [d56,d51])). % 187.86/34.36 cnf(d58, plain, p2(sK62(sK69(sK16))) | 'Ts1'(sK16), inference(resolution, [status(thm)], [d57,d34])). % 187.86/34.36 cnf(d59, plain, r1(X0,sK62(X0)) | ~r1(sK16,X0) | ~'Ts1'(sK15), inference(resolution, [status(thm)], [c47,c8])). % 187.86/34.36 cnf(d60, plain, r1(X0,sK62(X0)) | ~r1(sK16,X0), inference(resolution, [status(thm)], [d57,d59])). % 187.86/34.36 cnf(d61, plain, r1(sK69(sK16),sK62(sK69(sK16))) | 'Ts1'(sK16), inference(resolution, [status(thm)], [d60,d33])). % 187.86/34.36 cnf(d62, plain, 'Ts1'(sK16) | ~p2(sK62(sK69(sK16))) | 'Ts1'(sK16) | ~'Ts3'(sK16), inference(resolution, [status(thm)], [d61,c59])). % 187.86/34.36 cnf(d63, plain, ~p2(sK62(sK69(sK16))) | 'Ts1'(sK16), inference(resolution, [status(thm)], [d18,d62])). % 187.86/34.36 cnf(d64, plain, 'Ts1'(sK16) | 'Ts1'(sK16), inference(resolution, [status(thm)], [d63,d58])). % 187.86/34.36 cnf(d65, plain, r1(X0,sK62(X0)) | ~r1(sK67(sK16),X0), inference(resolution, [status(thm)], [d64,d31])). % 187.86/34.36 cnf(d66, plain, r1(sK73(sK67(sK16)),sK62(sK73(sK67(sK16)))), inference(resolution, [status(thm)], [d65,d30])). % 187.86/34.36 cnf(d67, plain, ~p2(sK62(sK73(sK67(sK16)))), inference(resolution, [status(thm)], [d66,d25])). % 187.86/34.36 cnf(d68, plain, ~r1(sK67(sK16),X0) | p2(sK62(X0)) | ~'Ts1'(sK16), inference(resolution, [status(thm)], [d8,c48])). % 187.86/34.36 cnf(d69, plain, p2(sK62(sK73(sK67(sK16)))) | ~'Ts1'(sK16), inference(resolution, [status(thm)], [d68,d30])). % 187.86/34.36 cnf(d70, plain, p2(sK62(sK73(sK67(sK16)))), inference(resolution, [status(thm)], [d64,d69])). % 187.86/34.36 cnf(d71, plain, $false, inference(resolution, [status(thm)], [d70,d67])). % 187.86/34.36 % SZS output end CNFRefutation for theBenchmark.p %------------------------------------------------------------------------------