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=  169029 States=   1e+006 Transitions= 1.4e+006 Memory=   953.674	t= 2.41e+003 R=  4e+002
Depth=  169029 States=   2e+006 Transitions= 2.99e+006 Memory=   953.674	t= 5.16e+003 R=  4e+002
Depth=  169029 States=   3e+006 Transitions= 4.76e+006 Memory=   953.674	t= 8.22e+003 R=  4e+002

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

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

State-vector 640800 byte, depth reached 169029, errors: 0
  3725541 states, stored
  2604260 states, matched
  6329801 transitions (= stored+matched)
        0 atomic steps

hash factor: 2.25165 (best if > 100.)

bits set per state: 3 (-k3)

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


pan: elapsed time 1.09e+004 seconds
pan: rate 340.47343 states/second