# The 2nd killer of Sergey Markelov (February 11, 1998)

hyp := [2*S-k*n*sin(2*a)-l*m*sin(2*c), 2*S-k*l*sin(2*b)-m*n*sin(2*d),
        x1^2+y1^2-1, x2^2+y2^2-1, x3^2+y3^2-1, x4^2+y4^2-1, sin(a+b+c+d),
        k^2+n^2-2*k*n*cos(2*a)-l^2-m^2+2*l*m*cos(2*c),
        k^2+l^2-2*k*l*cos(2*b)-m^2-n^2+2*m*n*cos(2*d)]:
ss := sin(a)=x1, sin(b)=x2, sin(c)=x3, sin(d)=x4,
      cos(a)=y1, cos(b)=y2, cos(c)=y3, cos(d)=y4, n=1:

con:=4*S-(k+l+m+n)^2/(cos(a)/sin(a)+cos(b)/sin(b)+cos(c)/sin(c)+cos(d)/sin(d))
        +(k-l+m-n)^2/(sin(a)/cos(a)+sin(b)/cos(b)+sin(c)/cos(c)+sin(d)/cos(d)):

Killer2 := Theorem(subs(ss,expand(hyp)), numer(subs(ss,con)),
                   [y2, x2, y3, x3, y4, x4, y1, x1, l, k, m, S]); 
Remark(
`   See`,
`X. Hou, H. Li, D. Wang, L. Yang: "Russian Killer" No. 2: A Challenging    `,
`Geometric Theorem with Human and Machine Proofs. The Mathematical         `,
`Intelligencer 23(1) (2001) 9-15.`
):
