// null = no satisfaction
// otherwise return var map
static Iterable<SS> gSatAnd(L<S> statements) {
  assertTrue(l(statements) >= 1);
  
  if (l(statements) == 1)
    ret gSat(first(statements));
  
  new L<SS> l;
  for (SS map : gSat(first(statements)))
    for (SS map2 : gSatAnd(dropFirst(statements)))
      addIfNotEmpty(l, mergeMappings(map, map2));
  ret l;
}

static Iterable<SS> gSatAnd(S... statements) {
  ret gSatAnd(asList(statements));
}