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=  230189 States=   1e+006 Transitions= 1.43e+006 Memory=   953.674	t= 2.46e+003 R=  4e+002
Depth=  230189 States=   2e+006 Transitions= 3.05e+006 Memory=   953.674	t= 5.23e+003 R=  4e+002
Depth=  230189 States=   3e+006 Transitions= 4.86e+006 Memory=   953.674	t= 8.34e+003 R=  4e+002
Depth=  230189 States=   4e+006 Transitions= 7.23e+006 Memory=   953.674	t= 1.24e+004 R=  3e+002

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

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

State-vector 641768 byte, depth reached 230189, errors: 0
  4131588 states, stored
  3494269 states, matched
  7625857 transitions (= stored+matched)
        0 atomic steps

hash factor: 2.03036 (best if > 100.)

bits set per state: 3 (-k3)

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