max expr size  =    7
  |- on ineqs  =    4
  |- on conds  =    4
max  #-tests   = 1080
max  #-vars    =    2  (for inequational and conditional laws)

_ :: Bool  (holes: Bool)
_ :: Int  (holes: Int)
_ :: Nat3  (holes: Nat3)
_ :: Graph Nat3  (holes: Graph Nat3)
0 :: Nat3
0 :: Int
True :: Bool
empty :: Graph Nat3
vertex :: Nat3 -> Graph Nat3
(+) :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
(*) :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
overlay :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
connect :: Graph Nat3 -> Graph Nat3 -> Graph Nat3
edge :: Nat3 -> Nat3 -> Graph Nat3
length :: Graph Nat3 -> Int
size :: Graph Nat3 -> Int

    length (vertex i) == length (vertex j)
      size (vertex i) == length (vertex 0)
       length (x * y) == length (x + y)
         size (x * y) == size (x + y)
length (x + vertex i) == length (x + vertex j)
  size (x + vertex i) == size (x + vertex j)
   length (x * y + z) == length (x + (y + z))
     size (x * y + z) == size (x + (y + z))
                x + x == x
            x + empty == x
            x * empty == x
            empty * x == x
                x + y == y + x
          overlay x y == x + y
          connect x y == x * y
            x + x * y == x * y
            x + y * x == y * x
             edge i j == vertex i * vertex j
          (x + y) + z == x + (y + z)
          (x * y) * z == x * (y * z)
      x + y * (x * z) == y * (x * z)
      x + y * (z * x) == y * (z * x)
          x * (y + z) == x * y + x * z
          (x + y) * z == x * z + y * z
          x * (x * y) == x * x + x * y
          x * (y * y) == x * y + y * y
    x * (y * (x * z)) == x * (y * x) + x * (y * z)

         0 <= length x
         0 <= size x
  length x <= size x
size empty <= size x
         x <= size (y + z)
  length x <= length (edge i i)
  length x <= length (x + y)
     empty <= x
         x <= x + y
         x <= x * y
         x <= y * x
     x + y <= x * y