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=  225551 States=   1e+006 Transitions= 1.44e+006 Memory=   953.674	t= 2.25e+003 R=  4e+002
Depth=  225551 States=   2e+006 Transitions= 3.05e+006 Memory=   953.674	t= 4.78e+003 R=  4e+002
Depth=  225551 States=   3e+006 Transitions= 4.91e+006 Memory=   953.674	t= 7.68e+003 R=  4e+002
Depth=  225551 States=   4e+006 Transitions= 7.25e+006 Memory=   953.674	t= 1.14e+004 R=  4e+002

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

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

State-vector 644496 byte, depth reached 225551, errors: 0
  4348618 states, stored
  4046101 states, matched
  8394719 transitions (= stored+matched)
        0 atomic steps

hash factor: 1.92903 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):
2672848.035	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.32e+004 seconds
pan: rate 329.90845 states/second