reset;

param l=3;

param s=2^l;

set subsets{n in 0..s-1} = {i in 0..l-1: n div 2^i mod 2} ordered by reversed {0..l-1};

param p=s^l;

param vec{v in 0..p-1, i in 0..l-1} = v div s^i mod s;
set Vec{v in 0..p-1, i in 0..l-1} = subsets[vec[v,i]];

set Inv = {v in 0..p-1: !
  exists{i1 in 0..l-1}
  (
   Vec[v,i1] within {}
   or
   exists{i2 in i1+1..l-1}
   (
    Vec[v,i1] symdiff Vec[v,i2] within {}
    or
    exists{i3 in i2+1..l-1}
    (
     Vec[v,i1] symdiff Vec[v,i2] symdiff Vec[v,i3] within {}
     or
     exists{i4 in i3+1..l-1}
     (
      Vec[v,i1] symdiff Vec[v,i2] symdiff Vec[v,i3] symdiff Vec[v,i4] within {}
      or
      exists{i5 in i4+1..l-1}
       Vec[v,i1] symdiff Vec[v,i2] symdiff Vec[v,i3] symdiff Vec[v,i4] symdiff Vec[v,i5] within {}
     )
    )
   )
  )
} ordered;

param start;
param stop;
let start := _ampl_time;

display card(Inv);

param inv{v in Inv} = 
  sum{i in 0..l-1}
  (
    s^i *
      min {n in 0..s-1:
        {ii in 0..l-1: card({iii in subsets[n]: ii in Vec[v,iii]}) mod 2} symdiff {i} within {}
      } n
  );

display card({v in Inv: inv[v]==v});

param invby{v1 in Inv, v2 in Inv} =
  sum{i in 0..l-1} s^i *
    sum{ii in 0..l-1: card({iii in Vec[inv[v1],i]: ii in Vec[v2,iii]}) mod 2} 2^ii;

display card({v1 in Inv, v2 in Inv: invby[v1,v2] in Inv});

param add{v1 in Inv, v2 in Inv} = sum{i in 0..l-1} s^i * sum{ii in Vec[v1,i] symdiff Vec[v2,i]} 2^ii;

display card({v1 in Inv, v2 in Inv: add[v1,v2] in Inv});

set G2 dimen 2 = {v1 in Inv, v2 in {v in Inv: v>v1}: add[v1,v2] in Inv};

display card(G2);

set G3 dimen 3 =
  {(v1,v2) in G2, (v2,v3) in G2:
    (v1,v3) in G2
  };

display card(G3);

set G4 dimen 4 =
  {(v1,v2,v3) in G3, (v2,v3,v4) in G3:
    (v1,v4) in G2
  };

display card(G4);

set G5 dimen 5 =
  {(v1,v2,v3,v4) in G4, (v2,v3,v4,v5) in G4:
    (v1,v5) in G2
  };

display card(G5);

set G6 dimen 6 =
  {(v1,v2,v3,v4,v5) in G5, (v2,v3,v4,v5,v6) in G5:
    (v1,v6) in G2
  };

display card(G6);

set G7 dimen 7 =
  {(v1,v2,v3,v4,v5,v6) in G6, (v2,v3,v4,v5,v6,v7) in G6:
    (v1,v7) in G2
  };

display card(G7);

set G8 dimen 8 =
  {(v1,v2,v3,v4,v5,v6,v7) in G7, (v2,v3,v4,v5,v6,v7,v8) in G7:
    (v1,v8) in G2
  };

display card(G8);

let stop := _ampl_time;
printf "computed within %f seconds\n",stop-start;