Add ?IMPLIES(length(Ops) > 1, ...) to avoid legit model ambiguity

... in cases where the op list is too short to make a reasonable &
correct guess of behavior.

Use eqc:testing_time/2 for test length & EUnit timeout at 2x
testing time.