バカがいますよ

終端に到達する前に枝刈りすればいいなら，これでどうか．
1000回実行で，総当り61.891sec，早期枝刈りあり2.359sec (ちなみに条件チェックを省略した総当りバージョンは23.782sec)だった．

def pseud_amb(*ar, &block)
  result = []
  amb_impl = lambda {|a, work|
    if a[0]==nil # 終端に到達
      result.push( work.dup)
    else
      a[0].each {|d|
        tmp = work.dup.push(d)
        amb_impl[a[1..-1], tmp] if !block_given? || block[tmp]
      }
    end
  }
  amb_impl[ar, []]
  result
end


  Baker = 0
  Cooper = 1
  Fletcher = 2
  Miller = 3
  Smith = 4

old = Process.times.utime
p pseud_amb(1..5, 1..5, 1..5, 1..5, 1..5) {|a|
    ret = false
    if (a.uniq.size == a.size)
      case a.size
      when 1; ret = (a[Baker] != 5)
      when 2; ret = (a[Cooper] != 1)
      when 3; ret = (a[Fletcher] != 1 and a[Fletcher] != 5 and
              (a[Fletcher] - a[Cooper]).abs != 1)
      when 4; ret = (a[Miller] > a[Cooper])
      when 5; ret = ((a[Smith] - a[Fletcher]).abs != 1)
      end
    end
    ret
  }
p Process.times.utime - old

しかし，これでは枝刈りする順番が固定ではないか．scheme恐ろしい子．
条件はもっと綺麗に書ける気がする．