*** SUM  0.49s -->
Input: \f -> f [] == 0 && (f [1] == 1) && (f [2] == 2) && (f [1,2] == 3) && (f [1,0] == 1) && (f [1,2,3] == 6)