warning: for p.o. reduction to be valid the never claim must be stutter-closed
(never claims generated from LTL formulae are stutter-closed)
Depth=     782 States=   1e+06 Transitions= 1.7591e+06 Memory= 42.593
Depth=     866 States=   2e+06 Transitions= 3.53201e+06 Memory= 42.695
Depth=     866 States=   3e+06 Transitions= 5.30776e+06 Memory= 42.695
Depth=     866 States=   4e+06 Transitions= 7.03184e+06 Memory= 42.695
Depth=     866 States=   5e+06 Transitions= 8.79545e+06 Memory= 42.695
Depth=     866 States=   6e+06 Transitions= 1.05284e+07 Memory= 42.695
Depth=     866 States=   7e+06 Transitions= 1.21353e+07 Memory= 42.695
Depth=     866 States=   8e+06 Transitions= 1.39327e+07 Memory= 42.695
Depth=     866 States=   9e+06 Transitions= 1.57302e+07 Memory= 42.695
Depth=     866 States=   1e+07 Transitions= 1.75064e+07 Memory= 42.695
Depth=     866 States= 1.1e+07 Transitions= 1.93174e+07 Memory= 42.695
Depth=     866 States= 1.2e+07 Transitions= 2.11612e+07 Memory= 42.695
Depth=     866 States= 1.3e+07 Transitions= 2.30025e+07 Memory= 42.695
Depth=     866 States= 1.4e+07 Transitions= 2.48738e+07 Memory= 42.695
Depth=     866 States= 1.5e+07 Transitions= 2.66853e+07 Memory= 42.695
Depth=     898 States= 1.6e+07 Transitions= 2.86062e+07 Memory= 42.695
Depth=     898 States= 1.7e+07 Transitions= 3.04897e+07 Memory= 42.695
Depth=     898 States= 1.8e+07 Transitions= 3.24047e+07 Memory= 42.695
Depth=     898 States= 1.9e+07 Transitions= 3.43776e+07 Memory= 42.695
Depth=     898 States=   2e+07 Transitions= 3.64301e+07 Memory= 42.695
Depth=     898 States= 2.1e+07 Transitions= 3.84934e+07 Memory= 42.695
Depth=     898 States= 2.2e+07 Transitions= 4.05185e+07 Memory= 42.695
Depth=     898 States= 2.3e+07 Transitions= 4.25693e+07 Memory= 42.695
Depth=     898 States= 2.4e+07 Transitions= 4.47033e+07 Memory= 42.695
Depth=     898 States= 2.5e+07 Transitions= 4.69441e+07 Memory= 42.695
Depth=     898 States= 2.6e+07 Transitions= 4.9202e+07 Memory= 42.695
Depth=     898 States= 2.7e+07 Transitions= 5.14224e+07 Memory= 42.695
(Spin Version 3.2.2 -- 20 July 1998)
	+ Partial Order Reduction

Bit statespace search for:
	never-claim         	+
	assertion violations	+ (if within scope of claim)
	acceptance   cycles 	+ (fairness disabled)
	invalid endstates	- (disabled by never-claim)

State-vector 668 byte, depth reached 898, errors: 0
2.79588e+07 states, stored
2.57286e+07 states, matched
5.36874e+07 transitions (= stored+matched)
  463608 atomic steps
hash factor: 2.40028 (best coverage if >100)
(max size 2^26 states)

Stats on memory usage (in Megabytes):
19011.996	equivalent memory usage for states (stored*(State-vector + overhead))
8.389 	memory used for hash-array (-w26)
0.240 	memory used for DFS stack (-m10000)
42.695	total actual memory usage

real  2:04:18.3
user  1:56:12.8
sys         0.5