warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
Depth=  147405 States=   1e+006 Transitions= 1.39e+006 Memory=   953.674	t= 2.38e+003 R=  4e+002
Depth=  147405 States=   2e+006 Transitions= 2.97e+006 Memory=   953.674	t= 5.1e+003 R=  4e+002
Depth=  147405 States=   3e+006 Transitions= 4.75e+006 Memory=   953.674	t= 8.15e+003 R=  4e+002
Depth=  147405 States=   4e+006 Transitions= 7.09e+006 Memory=   953.674	t= 1.22e+004 R=  3e+002

(Spin Version 6.1.0 -- 4 May 2011)
	+ Partial Order Reduction

Bit statespace search for:
	never claim         	+ (p7)
	assertion violations	+ (if within scope of claim)
	cycle checks       	- (disabled by -DSAFETY)
	invalid end states	- (disabled by never claim)

State-vector 642096 byte, depth reached 147405, errors: 0
  4265287 states, stored
  3671798 states, matched
  7937085 transitions (= stored+matched)
        0 atomic steps

hash factor: 1.96672 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):
2611866.744	equivalent memory usage for states (stored*(State-vector + overhead))
    1.000	memory used for hash array (-w23)
    1.000	memory used for bit stack
   19.074	memory used for DFS stack (-m500000)
  932.601	other (proc and chan stacks)
  953.674	total actual memory usage


pan: elapsed time 1.36e+004 seconds
pan: rate  312.6434 states/second