Inferred invariants
ENTRY:
   N = size(B)
   N in [7..13]¨
   B: All elements in [-100..100]
EXIT:
   N = I = orig(N) = size(B)
   B = orig(B)
   S = sum(B)¨
   N in [7..13]
   B: All elements in [-100..100]
Line Callout 2: ¨ Formal specification (goal)
¨ Formal specification (goal)
This is the result from experiment 1; make that clear.
This is actual, complete output from the system.  (Everything else you will see is also actual output.)

Precondition: n  0
Postcondition: s = (j: 0  j < n : b[j])
Extra properties reported beyond Gries’s invariants give information about the data set.  (If data set is sufficiently broad, the resulting invariants are info about the function in isolation, or about the program.)

Conclusion:  the system is accurate.
But it doesn’t matter how accurate the results are if they aren’t good for anything.  (Now I’ll address that issue.)