warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
Changing debug level from 0 to -1
Using 1015 state memory
Using 12 stats memory
cpu1: Depth=      27 States=   1e+06 Transitions= 1.70514e+06 Memory= 0.000    
warning: for p.o. reduction to be valid the never claim must be stutter-invariant
(never claims generated from LTL formulae are stutter-invariant)
Changing debug level from 0 to -1
Using 1015 state memory
Using 12 stats memory
cpu0: Depth=      21 States=   1e+06 Transitions= 1.03011e+06 Memory= 256.654  
cpu1: Depth=      27 States=   2e+06 Transitions= 3.39874e+06 Memory= 0.000    
cpu1: Depth=      27 States=   3e+06 Transitions= 5.05535e+06 Memory= 0.000    
cpu0: Depth=      21 States=   2e+06 Transitions= 2.07294e+06 Memory= 256.654  
cpu1: Depth=      27 States=   4e+06 Transitions= 6.67855e+06 Memory= 0.000    
cpu0: Depth=      21 States=   3e+06 Transitions= 3.10346e+06 Memory= 256.654  
cpu1: Depth=      27 States=   5e+06 Transitions= 8.26267e+06 Memory= 0.000    
cpu0: Depth=      21 States=   4e+06 Transitions= 4.14583e+06 Memory= 256.654  
cpu1: Depth=      27 States=   6e+06 Transitions= 9.83032e+06 Memory= 0.000    
cpu0: Depth=      21 States=   5e+06 Transitions= 5.17492e+06 Memory= 256.654  
cpu1: Depth=      27 States=   7e+06 Transitions= 1.13372e+07 Memory= 0.000    
cpu0: Depth=      21 States=   6e+06 Transitions= 6.23054e+06 Memory= 256.654  
cpu0: Depth=      21 States=   7e+06 Transitions= 7.27272e+06 Memory= 256.654  
cpu1: Depth=      27 States=   8e+06 Transitions= 1.28738e+07 Memory= 0.000    
cpu0: Depth=      21 States=   8e+06 Transitions= 8.30119e+06 Memory= 256.654  
cpu1: Depth=      27 States=   9e+06 Transitions= 1.43346e+07 Memory= 0.000    
cpu0: Depth=      27 States=   9e+06 Transitions= 9.36176e+06 Memory= 256.654  
cpu1: Depth=      27 States=   1e+07 Transitions= 1.58156e+07 Memory= 0.000    
cpu0: Depth=      27 States=   1e+07 Transitions= 1.04084e+07 Memory= 256.654  
cpu0: Depth=      27 States= 1.1e+07 Transitions= 1.14493e+07 Memory= 256.654  
cpu1: Depth=      27 States= 1.1e+07 Transitions= 1.72496e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.2e+07 Transitions= 1.2479e+07 Memory= 256.654  
cpu1: Depth=      27 States= 1.2e+07 Transitions= 1.86803e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.3e+07 Transitions= 1.35452e+07 Memory= 256.654  
cpu0: Depth=      27 States= 1.4e+07 Transitions= 1.4591e+07 Memory= 256.654  
cpu1: Depth=      27 States= 1.3e+07 Transitions= 2.01492e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.5e+07 Transitions= 1.56274e+07 Memory= 256.654  
cpu1: Depth=      27 States= 1.4e+07 Transitions= 2.15657e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.6e+07 Transitions= 1.66656e+07 Memory= 256.654  
cpu0: Depth=      27 States= 1.7e+07 Transitions= 1.76928e+07 Memory= 256.654  
cpu1: Depth=      27 States= 1.5e+07 Transitions= 2.2897e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.8e+07 Transitions= 1.87374e+07 Memory= 256.654  
cpu1: Depth=      27 States= 1.6e+07 Transitions= 2.43578e+07 Memory= 0.000    
cpu0: Depth=      27 States= 1.9e+07 Transitions= 1.97867e+07 Memory= 256.654  
cpu0: Depth=      27 States=   2e+07 Transitions= 2.0829e+07 Memory= 256.654  
cpu1: Depth=      27 States= 1.7e+07 Transitions= 2.5767e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.1e+07 Transitions= 2.18629e+07 Memory= 256.654  
cpu1: Depth=      27 States= 1.8e+07 Transitions= 2.71324e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.2e+07 Transitions= 2.2896e+07 Memory= 256.654  
cpu0: Depth=      27 States= 2.3e+07 Transitions= 2.39224e+07 Memory= 256.654  
cpu1: Depth=      27 States= 1.9e+07 Transitions= 2.84601e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.4e+07 Transitions= 2.49576e+07 Memory= 256.654  
cpu1: Depth=      27 States=   2e+07 Transitions= 2.9888e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.5e+07 Transitions= 2.60129e+07 Memory= 256.654  
cpu0: Depth=      27 States= 2.6e+07 Transitions= 2.70573e+07 Memory= 256.654  
cpu1: Depth=      27 States= 2.1e+07 Transitions= 3.12431e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.7e+07 Transitions= 2.80933e+07 Memory= 256.654  
cpu0: Depth=      27 States= 2.8e+07 Transitions= 2.91282e+07 Memory= 256.654  
cpu1: Depth=      27 States= 2.2e+07 Transitions= 3.25868e+07 Memory= 0.000    
cpu0: Depth=      27 States= 2.9e+07 Transitions= 3.01591e+07 Memory= 256.654  
cpu1: Depth=      27 States= 2.3e+07 Transitions= 3.38566e+07 Memory= 0.000    
cpu0: Depth=      27 States=   3e+07 Transitions= 3.11827e+07 Memory= 256.654  
cpu0: Depth=      27 States= 3.1e+07 Transitions= 3.22143e+07 Memory= 256.654  
cpu1: Depth=      27 States= 2.4e+07 Transitions= 3.52726e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.2e+07 Transitions= 3.32826e+07 Memory= 256.654  
cpu0: Depth=      27 States= 3.3e+07 Transitions= 3.43294e+07 Memory= 256.654  
cpu1: Depth=      27 States= 2.5e+07 Transitions= 3.65965e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.4e+07 Transitions= 3.53657e+07 Memory= 256.654  
cpu1: Depth=      27 States= 2.6e+07 Transitions= 3.79098e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.5e+07 Transitions= 3.63964e+07 Memory= 256.654  
cpu0: Depth=      27 States= 3.6e+07 Transitions= 3.74325e+07 Memory= 256.654  
cpu1: Depth=      27 States= 2.7e+07 Transitions= 3.91898e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.7e+07 Transitions= 3.84647e+07 Memory= 256.654  
cpu0: Depth=      27 States= 3.8e+07 Transitions= 3.94908e+07 Memory= 256.654  
cpu1: Depth=      27 States= 2.8e+07 Transitions= 4.0509e+07 Memory= 0.000    
cpu0: Depth=      27 States= 3.9e+07 Transitions= 4.05451e+07 Memory= 256.654  
cpu1: Depth=      27 States= 2.9e+07 Transitions= 4.18738e+07 Memory= 0.000    
cpu0: Depth=      27 States=   4e+07 Transitions= 4.15987e+07 Memory= 256.654  
cpu0: Depth=      27 States= 4.1e+07 Transitions= 4.26483e+07 Memory= 256.654  
cpu1: Depth=      27 States=   3e+07 Transitions= 4.31656e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.2e+07 Transitions= 4.3689e+07 Memory= 256.654  
cpu0: Depth=      27 States= 4.3e+07 Transitions= 4.47232e+07 Memory= 256.654  
cpu1: Depth=      27 States= 3.1e+07 Transitions= 4.44688e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.4e+07 Transitions= 4.57612e+07 Memory= 256.654  
cpu1: Depth=      27 States= 3.2e+07 Transitions= 4.57215e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.5e+07 Transitions= 4.67918e+07 Memory= 256.654  
cpu0: Depth=      27 States= 4.6e+07 Transitions= 4.78261e+07 Memory= 256.654  
cpu1: Depth=      27 States= 3.3e+07 Transitions= 4.70957e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.7e+07 Transitions= 4.88862e+07 Memory= 256.654  
cpu0: Depth=      27 States= 4.8e+07 Transitions= 4.99402e+07 Memory= 256.654  
cpu1: Depth=      27 States= 3.4e+07 Transitions= 4.8401e+07 Memory= 0.000    
cpu0: Depth=      27 States= 4.9e+07 Transitions= 5.09807e+07 Memory= 256.654  
cpu1: Depth=      27 States= 3.5e+07 Transitions= 4.96879e+07 Memory= 0.000    
cpu0: Depth=      27 States=   5e+07 Transitions= 5.2024e+07 Memory= 256.654  
cpu0: Depth=      27 States= 5.1e+07 Transitions= 5.30702e+07 Memory= 256.654  
cpu1: Depth=      27 States= 3.6e+07 Transitions= 5.09717e+07 Memory= 0.000    
cpu0: Depth=      27 States= 5.2e+07 Transitions= 5.41097e+07 Memory= 256.654  
cpu1: Depth=      27 States= 3.7e+07 Transitions= 5.22383e+07 Memory= 0.000    
cpu0: Depth=      27 States= 5.3e+07 Transitions= 5.51452e+07 Memory= 256.654  
cpu0: Depth=      27 States= 5.4e+07 Transitions= 5.61906e+07 Memory= 256.654  
cpu1: Depth=      27 States= 3.8e+07 Transitions= 5.36005e+07 Memory= 0.000    
cpu0: Depth=      27 States= 5.5e+07 Transitions= 5.72668e+07 Memory= 256.654  
cpu1: Depth=      27 States= 3.9e+07 Transitions= 5.49006e+07 Memory= 0.000    
cpu0: Depth=      27 States= 5.6e+07 Transitions= 5.83252e+07 Memory= 256.654  
cpu0: Depth=      27 States= 5.7e+07 Transitions= 5.9376e+07 Memory= 256.654  
cpu1: Depth=      27 States=   4e+07 Transitions= 5.62068e+07 Memory= 0.000    
cpu0: Depth=      27 States= 5.8e+07 Transitions= 6.04313e+07 Memory= 256.654  
cpu1: Depth=      27 States= 4.1e+07 Transitions= 5.74812e+07 Memory= 0.000    
cpu0: Depth=      27 States= 5.9e+07 Transitions= 6.14769e+07 Memory= 256.654  
cpu0: Depth=      27 States=   6e+07 Transitions= 6.25224e+07 Memory= 256.654  
cpu1: Depth=      27 States= 4.2e+07 Transitions= 5.87989e+07 Memory= 0.000    
cpu0: Depth=      27 States= 6.1e+07 Transitions= 6.35954e+07 Memory= 256.654  
cpu1: Depth=      27 States= 4.3e+07 Transitions= 6.01729e+07 Memory= 0.000    
cpu0: Depth=      27 States= 6.2e+07 Transitions= 6.46652e+07 Memory= 256.654  
cpu1: Depth=      27 States= 4.4e+07 Transitions= 6.14893e+07 Memory= 0.000    
cpu0: Depth=      27 States= 6.3e+07 Transitions= 6.5736e+07 Memory= 256.654  
cpu1: Depth=      27 States= 4.5e+07 Transitions= 6.28187e+07 Memory= 0.000    
cpu0: Depth=      27 States= 6.4e+07 Transitions= 6.6792e+07 Memory= 256.654  
cpu0: Depth=      27 States= 6.5e+07 Transitions= 6.7841e+07 Memory= 256.654  
cpu1: Depth=      27 States= 4.6e+07 Transitions= 6.41281e+07 Memory= 0.000    
cpu0: Depth=      27 States= 6.6e+07 Transitions= 6.89326e+07 Memory= 256.654  
cpu1: Depth=      27 States= 4.7e+07 Transitions= 6.55306e+07 Memory= 0.000    
cpu0: Depth=      27 States= 6.7e+07 Transitions= 7.00131e+07 Memory= 256.654  
cpu1: Depth=      27 States= 4.8e+07 Transitions= 6.68827e+07 Memory= 0.000    
cpu0: Depth=      27 States= 6.8e+07 Transitions= 7.10883e+07 Memory= 256.654  
cpu1: Depth=      27 States= 4.9e+07 Transitions= 6.82172e+07 Memory= 0.000    
cpu0: Depth=      27 States= 6.9e+07 Transitions= 7.21618e+07 Memory= 256.654  
cpu1: Depth=      27 States=   5e+07 Transitions= 6.96218e+07 Memory= 0.000    
cpu1: Depth=      27 States= 5.1e+07 Transitions= 7.10313e+07 Memory= 0.000    
cpu0: Depth=      27 States=   7e+07 Transitions= 7.3266e+07 Memory= 256.654  
cpu1: Depth=      27 States= 5.2e+07 Transitions= 7.24241e+07 Memory= 0.000    
cpu0: Depth=      27 States= 7.1e+07 Transitions= 7.43534e+07 Memory= 256.654  
cpu1: Depth=      27 States= 5.3e+07 Transitions= 7.38912e+07 Memory= 0.000    
cpu1: Depth=      27 States= 5.4e+07 Transitions= 7.53329e+07 Memory= 0.000    
cpu0: Depth=      27 States= 7.2e+07 Transitions= 7.54871e+07 Memory= 256.654  
cpu1: Depth=      27 States= 5.5e+07 Transitions= 7.68466e+07 Memory= 0.000    
cpu0: Depth=      27 States= 7.3e+07 Transitions= 7.66567e+07 Memory= 256.654  
cpu1: Depth=      27 States= 5.6e+07 Transitions= 7.83996e+07 Memory= 0.000    
cpu1: Depth=      27 States= 5.7e+07 Transitions= 8.00097e+07 Memory= 0.000    
cpu1: done -- local memcnt 0 Mb
cpu1: states stored  57518900	matched  23374277
cpu0: cpu1: locks: global         0	other      184498
cpu1: waits: states   4879799	slots           0

done -- local memcnt 256.654 Mb
cpu0: states stored  73708039	matched   3890581
cpu0: locks: global       150	other      158602
cpu0: waits: states 5.3700761e+09	slots           0

(Spin Version 5.0.0 -- 8 May 2007)
	+ Multi-Core (NCORE=2 -z20)
	+ Partial Order Reduction

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

State-vector 180 byte, depth reached 27, errors: 0
1.3122694e+08 states, stored
 27264858 states, matched
1.584918e+08 transitions (= stored+matched)
 52542138 atomic steps

hash factor: 8.18233 (best if > 100.)

bits set per state: 3 (-k3)

Stats on memory usage (in Megabytes):
26030.734	equivalent memory usage for states (stored*(State-vector + overhead))
128.000  	memory used for hash array (-w30)
0.076    	memory used for bit stack
0.458    	memory used for DFS stack (-m10000)
128.000  	memory used for shared work-queues
128.071  	other (proc and chan stacks)
0.049    	memory lost to fragmentation
256.654  	total actual memory usage

Successor counts:
  0	    859151	(0.5824 % of total)
  1	 141974894	(96.25 % of total)
  2	   3398524	(2.304 % of total)
  4	    940886	(0.6379 % of total)
 14	     83755	(0.05678 % of total)
 16	    251281	(0.1704 % of total)
mean 1.069 (without 0: 1.076)

cpu0: elapsed time 216 seconds (1.31227e+08 states)
cpu0: rate 608885 states/second