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=  168981 States=   1e+006 Transitions= 1.4e+006 Memory=   953.674	t= 2.19e+003 R=  5e+002
Depth=  168981 States=   2e+006 Transitions= 2.99e+006 Memory=   953.674	t= 4.68e+003 R=  4e+002
Depth=  168981 States=   3e+006 Transitions= 4.76e+006 Memory=   953.674	t= 7.45e+003 R=  4e+002

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

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

State-vector 640640 byte, depth reached 168981, errors: 0
  3719686 states, stored
  2595333 states, matched
  6315019 transitions (= stored+matched)
        0 atomic steps

hash factor: 2.25519 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):
2272600.668	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 9.89e+003 seconds
pan: rate 375.98042 states/second