struct Nil {}
struct Cons<X, XS> {}

trait First {
    type X;
}

impl First for Nil {
    type X = Nil;
}

impl<X, XS> First for Cons<X, XS> {
    type X = X;
}

trait ListConcat {
    type C;
}

impl<X> ListConcat for (Nil, X) {
    type C = X;
}

impl<A, As, Bs> ListConcat for (Cons<A, As>, Bs) where (As, Bs): ListConcat {
    type C = Cons<A, <(As, Bs) as ListConcat>::C>;
}

trait ListConcatAll {
    type L;
}

impl ListConcatAll for Nil {
    type L = Nil;
}

impl<Chunk, Rest> ListConcatAll for Cons<Chunk, Rest> where Rest: ListConcatAll, (Chunk, <Rest as ListConcatAll>::L): ListConcat {
    type L = <(Chunk, <Rest as ListConcatAll>::L) as ListConcat>::C;
}

struct True {}
struct False {}

trait Not {
    type B;
}

impl Not for True {
    type B = False;
}

impl Not for False {
    type B = True;
}

trait Or {
    type B;
}

impl Or for (True, True) {
    type B = True;
}

impl Or for (True, False) {
    type B = True;
}

impl Or for (False, True) {
    type B = True;
}

impl Or for (False, False) {
    type B = False;
}

trait AnyTrue {
    type T;
}

impl AnyTrue for Nil {
    type T = False;
}

impl<More> AnyTrue for Cons<True, More> {
    type T = True;
}

impl<List> AnyTrue for Cons<False, List> where List: AnyTrue {
    type T = <List as AnyTrue>::T;
}

struct Z {}
struct S<N> {}

trait PeanoEqual {
    type T;
}

impl PeanoEqual for (Z, Z) {
    type T = True;
}

impl<A> PeanoEqual for (S<A>, Z) {
    type T = False;
}

impl<B> PeanoEqual for (Z, S<B>) {
    type T = False;
}

impl<A, B> PeanoEqual for (S<A>, S<B>) where (A, B): PeanoEqual {
    type T = <(A, B) as PeanoEqual>::T;
}

trait PeanoLT {
    type T;
}

impl PeanoLT for (Z, Z) {
    type T = False;
}

impl<X> PeanoLT for (S<X>, Z) {
    type T = False;
}

impl<X> PeanoLT for (Z, S<X>) {
    type T = True;
}

impl<A, B> PeanoLT for (S<A>, S<B>) where (A, B): PeanoLT {
    type T = <(A, B) as PeanoLT>::T;
}

trait PeanoAbsDiff {
    type C;
}

impl PeanoAbsDiff for (Z, Z) {
    type C = Z;
}

impl<B> PeanoAbsDiff for (Z, S<B>) {
    type C = S<B>;
}

impl<A> PeanoAbsDiff for (S<A>, Z) {
    type C = S<A>;
}

impl<A, B> PeanoAbsDiff for (S<A>, S<B>) where (A, B): PeanoAbsDiff {
    type C = <(A, B) as PeanoAbsDiff>::C;
}

trait Range {
    type Xs;
}

impl Range for Z {
    type Xs = Nil;
}

impl<N> Range for S<N> where N: Range {
    type Xs = Cons<N, <N as Range>::Xs>;
}

trait Apply {
    type R;
}

struct Conj1<List> {}

impl<List, X> Apply for (Conj1<List>, X) {
    type R = Cons<X, List>;
}

trait Map {
    type Ys;
}

impl<F> Map for (F, Nil) {
    type Ys = Nil;
}

impl<F, X, Xs> Map for (F, Cons<X, Xs>) where (F, X): Apply, (F, Xs): Map {
    type Ys = Cons<<(F, X) as Apply>::R, <(F, Xs) as Map>::Ys>;
}

trait MapCat {
    type Zs;
}

impl<F> MapCat for (F, Nil) {
    type Zs = Nil;
}

impl<F, Xs> MapCat for (F, Xs) where (F, Xs): Map, <(F, Xs) as Map>::Ys: ListConcatAll {
    type Zs = <<(F, Xs) as Map>::Ys as ListConcatAll>::L;
}

trait AppendIf {
    type Zs;
}

impl<X, Ys> AppendIf for (True, X, Ys) {
    type Zs = Cons<X, Ys>;
}

impl<X, Ys> AppendIf for (False, X, Ys) {
    type Zs = Ys;
}

trait Filter {
    type Ys;
}

impl<F> Filter for (F, Nil) {
    type Ys = Nil;
}

impl<F, X, Xs> Filter for (F, Cons<X, Xs>) where (F, X): Apply, (F, Xs): Filter, (<(F, X) as Apply>::R, X, <(F, Xs) as Filter>::Ys): AppendIf {
    type Ys = <(<(F, X) as Apply>::R, X, <(F, Xs) as Filter>::Ys) as AppendIf>::Zs;
}

struct Queen<X, Y> {}
struct Queen1<X> {}

impl<X, Y> Apply for (Queen1<X>, Y) {
    type R = Queen<X, Y>;
}

trait QueensInRow {
    type Queens;
}

impl<N, X> QueensInRow for (N, X) where N: Range, (Queen1<X>, <N as Range>::Xs): Map {
    type Queens = <(Queen1<X>, <N as Range>::Xs) as Map>::Ys;
}

trait Threatens {
    type T;
}

impl<Ax, Ay, Bx, By> Threatens for (Queen<Ax, Ay>, Queen<Bx, By>)
    where (Ax, Bx): PeanoEqual, (Ax, Bx): PeanoAbsDiff, (Ay, By): PeanoEqual, (Ay, By): PeanoAbsDiff,
          (<(Ax, Bx) as PeanoEqual>::T, <(Ay, By) as PeanoEqual>::T): Or,
          (<(Ax, Bx) as PeanoAbsDiff>::C, <(Ay, By) as PeanoAbsDiff>::C): PeanoEqual,
          (<(<(Ax, Bx) as PeanoEqual>::T, <(Ay, By) as PeanoEqual>::T) as Or>::B,
           <(<(Ax, Bx) as PeanoAbsDiff>::C, <(Ay, By) as PeanoAbsDiff>::C) as PeanoEqual>::T,
          ): Or {
    type T = <(
        <(<(Ax, Bx) as PeanoEqual>::T, <(Ay, By) as PeanoEqual>::T) as Or>::B,
        <(<(Ax, Bx) as PeanoAbsDiff>::C, <(Ay, By) as PeanoAbsDiff>::C) as PeanoEqual>::T,
    ) as Or>::B;
}

struct Threatens1<A> {}

impl<A, B> Apply for (Threatens1<A>, B) where (A, B): Threatens {
    type R = <(A, B) as Threatens>::T;
}

trait Safe {
    type T;
}

impl<Config, Queen> Safe for (Config, Queen)
    where (Threatens1<Queen>, Config): Map,
          <(Threatens1<Queen>, Config) as Map>::Ys: AnyTrue,
          <<(Threatens1<Queen>, Config) as Map>::Ys as AnyTrue>::T: Not {
    type T = <<<(Threatens1<Queen>, Config) as Map>::Ys as AnyTrue>::T as Not>::B;
}

struct Safe1<Config> {}

impl<Config, Queen> Apply for (Safe1<Config>, Queen) where (Config, Queen): Safe {
    type R = <(Config, Queen) as Safe>::T;
}

trait AddQueen {
    type Cs;
}

impl<N, X, C> AddQueen for (N, X, C)
    where (N, X): QueensInRow,
          (Safe1<C>, <(N, X) as QueensInRow>::Queens): Filter,
          <(Conj1<C>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter>::Ys: Map {
    type Cs = <<(Conj1<C>, (Safe1<C>, <(N, X) as QueensInRow>::Queens)) as Filter>::Ys as Map>::Ys;
}

struct AddQueen2<N, X> {}

impl<N, X, C> Apply for (AddQueen2<N, X>, C) where (N, X, C): AddQueen {
    type R = <(N, X, C) as AddQueen>::Cs;
}

trait AddQueenToAll {
    type CsPrime;
}

impl<N, X, Cs> AddQueenToAll for (N, X, Cs) where (AddQueen2<N, X>, Cs): MapCat {
    type CsPrime = <(AddQueen2<N, X>, Cs) as MapCat>::Zs;
}

trait AddQueensIf {
    type CsPrime;
}

impl<N, X, Cs> AddQueensIf for (False, N, X, Cs) {
    type CsPrime = Cs;
}

impl<N, X, Cs> AddQueensIf for (True, N, X, Cs)
    where (N, X, Cs): AddQueenToAll,
          (N, S<X>, <(N, X, Cs) as AddQueenToAll>::CsPrime): AddQueens {
    type CsPrime = <(N, S<X>, <(N, X, Cs) as AddQueenToAll>::CsPrime) as AddQueens>::CsPrime;
}

trait AddQueens {
    type CsPrime;
}

impl<N, X, Cs> AddQueens for (N, X, Cs)
    where (X, N): PeanoLT,
          (<(X, N) as PeanoLT>::T, N, X, Cs): AddQueensIf {
    type CsPrime = <(<(X, N) as PeanoLT>::T, N, X, Cs) as AddQueensIf>::CsPrime;
}

trait Solution {
    type C;
}

impl<N> Solution for N where (N, Z, Cons<Nil, Nil>): AddQueens, <(N, Z, Cons<Nil, Nil>) as AddQueens>::CsPrime: First {
    type C = <<(N, Z, Cons<Nil, Nil>) as AddQueens>::CsPrime as First>::X;
}

// <N6 as Solution>::C