PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-sp98ic.opb
MD5SUM	b6b40b25db69f63dc02649b5c9a3693a
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	2147483647
Optimality of the best value was proved	NO
Number of terms in the objective function	10894
Biggest coefficient in the objective function	1079902210
Number of bits for the biggest coefficient in the objective function	31
Sum of the numbers in the objective function	3040671454286
Number of bits of the sum of numbers in the objective function	42
Biggest number in a constraint	1079902210
Number of bits of the biggest number in a constraint	31
Biggest sum of numbers in a constraint	3040671454286
Number of bits of the biggest sum of numbers	42
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	8.81166
Number of variables	10894
Total number of constraints	11719
Number of constraints which are clauses	20
Number of constraints which are cardinality constraints (but not clauses)	11518
Number of constraints which are nor clauses,nor cardinality constraints	181
Minimum length of a constraint	1
Maximum length of a constraint	5038
Trace number 13241

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-20 20:20:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15272 boxname=wulflinc8 idbench=1175 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b6b40b25db69f63dc02649b5c9a3693a  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-sp98ic.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-sp98ic.opb /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-sp98ic.opb
IDLAUNCH: 15272
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        813952 kB
Buffers:         33188 kB
Cached:         164556 kB
SwapCached:          0 kB
Active:          69380 kB
Inactive:       131284 kB
HighTotal:      131008 kB
HighFree:        39172 kB
LowTotal:       903652 kB
LowFree:        774780 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:               0 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14320 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-20 20:40:54 (client local time) WITH STATUS 0 IN 1200.41 SECONDS
stats: 15272 7 1200.41 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 825 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ssssss.ssssssss.ss.s..sssss..sssssssssssssssssssssssssssssssssss.sssss.s..sssssssssssssssssssssssssssss.ssssssss.sssss..s.s.s.sssssssssssssssssss.ssss.sssssssssssssssssssss
c ---[ 976]---> Adder-cost: 1845   maxlim: 3   bits: 3/2
c ---[ 970]---> Adder-cost: 2336   maxlim: 26   bits: 6/5
c ---[ 953]---> Adder-cost: 2441   maxlim: 3   bits: 3/2
c ---[ 942]---> Adder-cost: 5853   maxlim: 28   bits: 6/5
c ---[ 931]---> Adder-cost: 836   maxlim: 2   bits: 3/2
c ---[ 912]---> Adder-cost: 763   maxlim: 4   bits: 4/3
c ---[ 910]---> Adder-cost: 1271   maxlim: 21   bits: 6/5
c ---[ 872]---> Adder-cost: 5376   maxlim: 13   bits: 5/4
c ---[ 866]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 865]---> Adder-cost: 884   maxlim: 3   bits: 3/2
c ---[ 863]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 862]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 861]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 860]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 859]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 858]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 857]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 856]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 855]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 854]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 852]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 851]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 850]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 849]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 848]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 847]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 846]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 845]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 844]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 843]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 841]---> Adder-cost: 28   maxlim: 22   bits: 5/5
c ---[ 840]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 839]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 838]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 837]---> Adder-cost: 30   maxlim: 19   bits: 5/5
c ---[ 836]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 835]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 834]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 833]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 832]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 831]---> Adder-cost: 6956   maxlim: 4   bits: 4/3
c ---[ 830]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 829]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 828]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 827]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 826]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 825]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 824]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 823]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 822]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 821]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 819]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 818]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 817]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 816]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 815]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 814]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 813]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 812]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 811]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 810]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 808]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 807]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 806]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 805]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 804]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 803]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 802]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 801]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 800]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 799]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 797]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 796]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 795]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 794]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 793]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 792]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 791]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 790]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 789]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 788]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 786]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 785]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 784]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 783]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 782]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 781]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 780]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 779]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 778]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 777]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 776]---> Adder-cost: 0   maxlim: 3   bits: 3/2
c ---[ 775]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 774]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 773]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 772]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 771]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 770]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 769]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 768]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 767]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 766]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 765]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ---[ 764]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 763]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 762]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 761]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 760]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 759]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 758]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 757]---> Adder-cost: 28   maxlim: 22   bits: 5/5
c ---[ 756]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 755]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 753]---> Adder-cost: 1423   maxlim: 3   bits: 3/2
c ---[ 752]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 751]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 750]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 749]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 748]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 747]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 746]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 745]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 744]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 743]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 742]---> Adder-cost: 680   maxlim: 2   bits: 3/2
c ---[ 741]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 740]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 739]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 738]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 737]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 736]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 735]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 734]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 733]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 732]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 730]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 729]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 728]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 727]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 726]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 725]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 724]---> Adder-cost: 32   maxlim: 21   bits: 5/5
c ---[ 723]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 722]---> Adder-cost: 28   maxlim: 21   bits: 5/5
c ---[ 721]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 719]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 718]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 717]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 716]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 715]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 714]---> Adder-cost: 32   maxlim: 21   bits: 5/5
c ---[ 713]---> Adder-cost: 14   maxlim: 7   bits: 4/3
c ---[ 712]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 711]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 710]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 708]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 707]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 706]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 705]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 704]---> Adder-cost: 26   maxlim: 22   bits: 5/5
c ---[ 703]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 702]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 701]---> Adder-cost: 36   maxlim: 21   bits: 5/5
c ---[ 700]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 699]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 697]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 696]---> Adder-cost: 32   maxlim: 21   bits: 5/5
c ---[ 695]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 694]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 693]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 692]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 691]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 690]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 689]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 688]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 686]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 685]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 684]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 683]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 682]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 681]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 680]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 679]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 678]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 677]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 675]---> Adder-cost: 30   maxlim: 19   bits: 5/5
c ---[ 674]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 673]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 672]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 671]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 670]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 669]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 668]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 667]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 666]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 665]---> Adder-cost: 491   maxlim: 2   bits: 3/2
c ---[ 664]---> Adder-cost: 30   maxlim: 19   bits: 5/5
c ---[ 663]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 662]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 661]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 660]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 659]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 658]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 657]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 656]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 655]---> Adder-cost: 30   maxlim: 19   bits: 5/5
c ---[ 654]---> Adder-cost: 1065   maxlim: 26   bits: 6/5
c ---[ 653]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 652]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 651]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 650]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 649]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 648]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 647]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 646]---> Adder-cost: 30   maxlim: 19   bits: 5/5
c ---[ 645]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 644]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 642]---> Adder-cost: 4345   maxlim: 4   bits: 4/3
c ---[ 641]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 640]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 639]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 638]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 637]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 636]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 635]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 634]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 633]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 632]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 630]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 629]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 628]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 627]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 625]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 624]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 623]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 622]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 621]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 619]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 618]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 617]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 616]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 615]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 614]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 613]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 612]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 611]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 610]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 608]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 607]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 606]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 605]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 604]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 603]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 602]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 601]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 600]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 599]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 597]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 596]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 595]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 594]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 593]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 592]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 591]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 590]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 589]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 588]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 586]---> Adder-cost: 30   maxlim: 19   bits: 5/5
c ---[ 585]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 584]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 583]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 582]---> Adder-cost: 20   maxlim: 13   bits: 4/4
c ---[ 581]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 580]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 579]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 578]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 577]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 575]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 574]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 573]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 572]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 571]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 570]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 569]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 568]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 567]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 566]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 564]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 563]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 562]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 561]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 560]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 559]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 558]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 557]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 556]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 555]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 553]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 552]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 551]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 550]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 549]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 548]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 547]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 546]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 545]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 544]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 542]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 541]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 540]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 539]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 538]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 537]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 536]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 535]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 534]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 533]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 532]---> Adder-cost: 6106   maxlim: 2   bits: 3/2
c ---[ 531]---> Adder-cost: 3397   maxlim: 18   bits: 6/5
c ---[ 530]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 529]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 528]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 527]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 526]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 525]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[ 524]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 523]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 522]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 521]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 520]---> Adder-cost: 1055   maxlim: 13   bits: 5/4
c ---[ 519]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 518]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 517]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 516]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 515]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 514]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 513]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 512]---> Adder-cost: 28   maxlim: 22   bits: 5/5
c ---[ 511]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 510]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 508]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 507]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 506]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 505]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 504]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 503]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 502]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 501]---> Adder-cost: 20   maxlim: 19   bits: 5/5
c ---[ 500]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 499]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 497]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 496]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 495]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 494]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 493]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 492]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 491]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 490]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 489]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 488]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 486]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 485]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 484]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 483]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 482]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 481]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 480]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 479]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 478]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 477]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 475]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 474]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 473]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 472]---> Adder-cost: 30   maxlim: 19   bits: 5/5
c ---[ 471]---> Adder-cost: 20   maxlim: 14   bits: 5/4
c ---[ 470]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 469]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 468]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 467]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 466]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 465]---> Adder-cost: 9797   maxlim: 12   bits: 5/4
c ---[ 464]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 463]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 462]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 461]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 460]---> Adder-cost: 20   maxlim: 19   bits: 5/5
c ---[ 459]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 458]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 457]---> Adder-cost: 20   maxlim: 14   bits: 5/4
c ---[ 456]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 455]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 453]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 452]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 451]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 450]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 449]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 448]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 447]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 446]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 445]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 444]---> Adder-cost: 26   maxlim: 17   bits: 5/5
c ---[ 442]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 441]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 440]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 439]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 438]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 437]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 436]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 435]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 434]---> Adder-cost: 12   maxlim: 13   bits: 4/4
c ---[ 433]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 431]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 430]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 429]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 428]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 427]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 426]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 425]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 424]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 423]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 422]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 419]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 418]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 417]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 416]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 415]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 414]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 413]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[ 412]---> Adder-cost: 20   maxlim: 14   bits: 5/4
c ---[ 411]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 410]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 408]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 407]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 406]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 405]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 404]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 403]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 402]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 401]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 400]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 399]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 397]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 396]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 395]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 394]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 393]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 392]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 391]---> Adder-cost: 18   maxlim: 13   bits: 4/4
c ---[ 390]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 389]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 388]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 386]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 385]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 384]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 383]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 382]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 381]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 380]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 379]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 378]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 377]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 375]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 374]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 373]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 372]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 371]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 370]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 369]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 368]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 367]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 366]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 365]---> Adder-cost: 6165   maxlim: 14   bits: 5/4
c ---[ 364]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 363]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 362]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 361]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 360]---> Adder-cost: 20   maxlim: 14   bits: 5/4
c ---[ 359]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 358]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 357]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 356]---> Adder-cost: 20   maxlim: 14   bits: 5/4
c ---[ 355]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 353]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 352]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 351]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 350]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 349]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 348]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 347]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 346]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 345]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 344]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 342]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 341]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 340]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 339]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 338]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 337]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 336]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 335]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 334]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 333]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 331]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 330]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 329]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 328]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 327]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 326]---> Adder-cost: 20   maxlim: 10   bits: 4/4
c ---[ 325]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 324]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 323]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 322]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 320]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 319]---> Adder-cost: 20   maxlim: 14   bits: 5/4
c ---[ 318]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 317]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 316]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 315]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 314]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 313]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 312]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 311]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 310]---> Adder-cost: 3157   maxlim: 2   bits: 3/2
c ---[ 308]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 307]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 305]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 304]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 303]---> Adder-cost: 24   maxlim: 14   bits: 5/4
c ---[ 302]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 301]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 300]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 299]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 297]---> Adder-cost: 30   maxlim: 14   bits: 5/4
c ---[ 296]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 295]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 294]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 293]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 292]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 291]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 290]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 289]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 288]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 287]---> Adder-cost: 1987   maxlim: 16   bits: 6/5
c ---[ 286]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 285]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 284]---> Adder-cost: 16   maxlim: 13   bits: 4/4
c ---[ 283]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 282]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 281]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 280]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 279]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 278]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 277]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 275]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 274]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 273]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 272]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 271]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 270]---> Adder-cost: 16   maxlim: 21   bits: 5/5
c ---[ 269]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 268]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 267]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 266]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 264]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 263]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 262]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 261]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 260]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 259]---> Adder-cost: 14   maxlim: 8   bits: 4/4
c ---[ 258]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 257]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 256]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 255]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 253]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 252]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 251]---> Adder-cost: 20   maxlim: 19   bits: 5/5
c ---[ 250]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 248]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 247]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 246]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 245]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 244]---> Adder-cost: 34   maxlim: 22   bits: 5/5
c ---[ 242]---> Adder-cost: 36   maxlim: 22   bits: 5/5
c ---[ 241]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 240]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 239]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 238]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 237]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 236]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 235]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 234]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 233]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 231]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 230]---> Adder-cost: 30   maxlim: 22   bits: 5/5
c ---[ 229]---> Adder-cost: 26   maxlim: 22   bits: 5/5
c ---[ 228]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 227]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 226]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 225]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 224]---> Adder-cost: 20   maxlim: 19   bits: 5/5
c ---[ 223]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 222]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 220]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 219]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 218]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 217]---> Adder-cost: 20   maxlim: 14   bits: 5/4
c ---[ 216]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 215]---> Adder-cost: 22   maxlim: 21   bits: 5/5
c ---[ 214]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 213]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 212]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 211]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 209]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 208]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 207]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 206]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 205]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 204]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 203]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 202]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 201]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 200]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 199]---> Adder-cost: 2481   maxlim: 3   bits: 3/2
c ---[ 197]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 196]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 195]---> Adder-cost: 20   maxlim: 19   bits: 5/5
c ---[ 194]---> Adder-cost: 44   maxlim: 22   bits: 5/5
c ---[ 193]---> Adder-cost: 38   maxlim: 22   bits: 5/5
c ---[ 192]---> Adder-cost: 16   maxlim: 8   bits: 4/4
c ---[ 191]---> Adder-cost: 32   maxlim: 22   bits: 5/5
c ---[ 190]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 189]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 188]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 186]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 185]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 184]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 183]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 182]---> Adder-cost: 22   maxlim: 13   bits: 4/4
c ---[ 181]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 180]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 179]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 178]---> Adder-cost: 28   maxlim: 14   bits: 5/4
c ---[ 177]---> Adder-cost: 26   maxlim: 17   bits: 5/5
c ---[ 176]---> Adder-cost: 14777   maxlim: 25   bits: 6/5
c ---[ 175]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 174]---> Adder-cost: 22   maxlim: 14   bits: 5/4
c ---[ 173]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 172]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 171]---> Adder-cost: 20   maxlim: 19   bits: 5/5
c ---[ 170]---> Adder-cost: 26   maxlim: 14   bits: 5/4
c ---[ 169]---> Adder-cost: 3648   maxlim: 22   bits: 6/5
c ---[ 162]---> Adder-cost: 3184   maxlim: 3   bits: 3/2
c ---[ 155]---> Adder-cost: 5940   maxlim: 28   bits: 6/5
c ---[ 151]---> Adder-cost: 342   maxlim: 1   bits: 2/1
c ---[ 150]---> Adder-cost: 1310   maxlim: 6   bits: 4/3
c ---[ 149]---> Adder-cost: 3214   maxlim: 22   bits: 6/5
c ---[ 148]---> Adder-cost: 1874   maxlim: 8   bits: 5/4
c ---[ 147]---> Adder-cost: 7277   maxlim: 13   bits: 5/4
c ---[ 146]---> Adder-cost: 2401   maxlim: 1   bits: 2/1
c ---[ 145]---> Adder-cost: 3906   maxlim: 1   bits: 2/1
c ---[ 144]---> Adder-cost: 1629   maxlim: 1   bits: 2/1
c ---[ 143]---> Adder-cost: 165   maxlim: 1   bits: 2/1
c ---[ 142]---> Adder-cost: 288   maxlim: 6   bits: 4/3
c ---[ 141]---> Adder-cost: 129   maxlim: 1   bits: 2/1
c ---[ 140]---> Adder-cost: 120   maxlim: 1   bits: 2/1
c ---[ 139]---> Adder-cost: 566   maxlim: 1   bits: 2/1
c ---[ 138]---> Adder-cost: 1366   maxlim: 1   bits: 2/1
c ---[ 137]---> Adder-cost: 938   maxlim: 1   bits: 2/1
c ---[ 136]---> Adder-cost: 2983   maxlim: 1   bits: 2/1
c ---[ 135]---> Adder-cost: 31   maxlim: 1   bits: 2/1
c ---[ 134]---> Adder-cost: 192   maxlim: 1   bits: 2/1
c ---[ 133]---> Adder-cost: 144   maxlim: 1   bits: 2/1
c ---[ 132]---> Adder-cost: 720   maxlim: 1   bits: 2/1
c ---[ 131]---> Adder-cost: 419   maxlim: 1   bits: 2/1
c ---[ 130]---> Adder-cost: 654   maxlim: 1   bits: 2/1
c ---[ 129]---> Adder-cost: 1140   maxlim: 1   bits: 2/1
c ---[ 128]---> Adder-cost: 656   maxlim: 1   bits: 2/1
c ---[ 127]---> Adder-cost: 2054   maxlim: 1   bits: 2/1
c ---[ 126]---> Adder-cost: 29   maxlim: 1   bits: 2/1
c ---[ 125]---> Adder-cost: 63   maxlim: 1   bits: 2/1
c ---[ 124]---> Adder-cost: 162   maxlim: 1   bits: 2/1
c ---[ 123]---> Adder-cost: 1560   maxlim: 3   bits: 3/2
c ---[ 122]---> Adder-cost: 2675   maxlim: 2   bits: 3/2
c ---[ 121]---> Adder-cost: 426   maxlim: 2   bits: 3/2
c ---[ 120]---> Adder-cost: 4262   maxlim: 3   bits: 3/2
c ---[ 119]---> Adder-cost: 657   maxlim: 2   bits: 3/2
c ---[ 118]---> Adder-cost: 531   maxlim: 2   bits: 3/2
c ---[ 117]---> Adder-cost: 1027   maxlim: 5   bits: 4/3
c ---[ 116]---> Adder-cost: 2889   maxlim: 2   bits: 3/2
c ---[ 115]---> Adder-cost: 2879   maxlim: 3   bits: 3/2
c ---[ 114]---> Adder-cost: 3557   maxlim: 2   bits: 3/2
c ---[ 113]---> Adder-cost: 420   maxlim: 2   bits: 3/2
c ---[ 112]---> Adder-cost: 2086   maxlim: 2   bits: 3/2
c ---[ 111]---> Adder-cost: 368   maxlim: 3   bits: 3/2
c ---[ 110]---> Adder-cost: 1419   maxlim: 3   bits: 3/2
c ---[ 109]---> Adder-cost: 916   maxlim: 3   bits: 3/2
c ---[ 108]---> Adder-cost: 2988   maxlim: 5   bits: 4/3
c ---[ 107]---> Adder-cost: 1240   maxlim: 1   bits: 2/1
c ---[ 106]---> Adder-cost: 848   maxlim: 4   bits: 4/3
c ---[ 105]---> Adder-cost: 1792   maxlim: 3   bits: 3/2
c ---[ 104]---> Adder-cost: 1339   maxlim: 4   bits: 4/3
c ---[ 103]---> Adder-cost: 4046   maxlim: 5   bits: 4/3
c ---[ 102]---> Adder-cost: 624   maxlim: 2   bits: 3/2
c ---[ 101]---> Adder-cost: 2181   maxlim: 2   bits: 3/2
c ---[ 100]---> Adder-cost: 231   maxlim: 2   bits: 3/2
c ---[  99]---> Adder-cost: 132   maxlim: 1   bits: 2/1
c ---[  98]---> Adder-cost: 4954   maxlim: 13   bits: 5/4
c ---[  97]---> Adder-cost: 11702   maxlim: 17   bits: 6/5
c ---[  96]---> Adder-cost: 2095   maxlim: 9   bits: 5/4
c ---[  95]---> Adder-cost: 1938   maxlim: 21   bits: 6/5
c ---[  94]---> Adder-cost: 100   maxlim: 1   bits: 2/1
c ---[  93]---> Adder-cost: 160   maxlim: 1   bits: 2/1
c ---[  92]---> Adder-cost: 1847   maxlim: 1   bits: 2/1
c ---[  91]---> Adder-cost: 364   maxlim: 1   bits: 2/1
c ---[  90]---> Adder-cost: 1128   maxlim: 1   bits: 2/1
c ---[  89]---> Adder-cost: 261   maxlim: 9   bits: 5/4
c ---[  88]---> Adder-cost: 1457   maxlim: 1   bits: 2/1
c ---[  87]---> Adder-cost: 209   maxlim: 1   bits: 2/1
c ---[  86]---> Adder-cost: 1261   maxlim: 1   bits: 2/1
c ---[  85]---> Adder-cost: 4034   maxlim: 5   bits: 4/3
c ---[  84]---> Adder-cost: 460   maxlim: 2   bits: 3/2
c ---[  83]---> Adder-cost: 5490   maxlim: 3   bits: 3/2
c ---[  82]---> Adder-cost: 608   maxlim: 4   bits: 4/3
c ---[  81]---> Adder-cost: 2888   maxlim: 3   bits: 3/2
c ---[  80]---> Adder-cost: 619   maxlim: 7   bits: 4/3
c ---[  79]---> Adder-cost: 213   maxlim: 4   bits: 4/3
c ---[  78]---> Adder-cost: 1459   maxlim: 5   bits: 4/3
c ---[  77]---> Adder-cost: 942   maxlim: 5   bits: 4/3
c ---[  76]---> Adder-cost: 695   maxlim: 2   bits: 3/2
c ---[  75]---> Adder-cost: 1041   maxlim: 5   bits: 4/3
c ---[  74]---> Adder-cost: 2848   maxlim: 3   bits: 3/2
c ---[  73]---> Adder-cost: 261   maxlim: 1   bits: 2/1
c ---[  72]---> Adder-cost: 114   maxlim: 1   bits: 2/1
c ---[  71]---> Adder-cost: 1811   maxlim: 1   bits: 2/1
c ---[  70]---> Adder-cost: 435   maxlim: 1   bits: 2/1
c ---[  69]---> Adder-cost: 692   maxlim: 6   bits: 4/3
c ---[  68]---> Adder-cost: 1073   maxlim: 3   bits: 3/2
c ---[  67]---> Adder-cost: 3095   maxlim: 5   bits: 4/3
c ---[  66]---> Adder-cost: 3357   maxlim: 5   bits: 4/3
c ---[  65]---> Adder-cost: 1318   maxlim: 1   bits: 2/1
c ---[  64]---> Adder-cost: 1421   maxlim: 1   bits: 2/1
c ---[  63]---> Adder-cost: 718   maxlim: 3   bits: 3/2
c ---[  62]---> Adder-cost: 589   maxlim: 3   bits: 3/2
c ---[  61]---> Adder-cost: 603   maxlim: 5   bits: 4/3
c ---[  60]---> Adder-cost: 979   maxlim: 1   bits: 2/1
c ---[  59]---> Adder-cost: 1277   maxlim: 6   bits: 4/3
c ---[  58]---> Adder-cost: 579   maxlim: 1   bits: 2/1
c ---[  57]---> Adder-cost: 301   maxlim: 5   bits: 4/3
c ---[  56]---> Adder-cost: 368   maxlim: 1   bits: 2/1
c ---[  55]---> Adder-cost: 146   maxlim: 4   bits: 4/3
c ---[  54]---> Adder-cost: 114   maxlim: 1   bits: 2/1
c ---[  53]---> Adder-cost: 1284   maxlim: 1   bits: 2/1
c ---[  52]---> Adder-cost: 4588   maxlim: 13   bits: 5/4
c ---[  51]---> Adder-cost: 99   maxlim: 4   bits: 4/3
c ---[  50]---> Adder-cost: 1335   maxlim: 1   bits: 2/1
c ---[  49]---> Adder-cost: 8828   maxlim: 20   bits: 6/5
c ---[  48]---> Adder-cost: 19   maxlim: 3   bits: 3/2
c ---[  47]---> Adder-cost: 7967   maxlim: 20   bits: 6/5
c ---[  46]---> Adder-cost: 98   maxlim: 3   bits: 3/2
c ---[  45]---> Adder-cost: 267   maxlim: 5   bits: 4/3
c ---[  44]---> Adder-cost: 103   maxlim: 3   bits: 3/2
c ---[  43]---> Adder-cost: 147   maxlim: 3   bits: 3/2
c ---[  42]---> Adder-cost: 1978   maxlim: 1   bits: 2/1
c ---[  41]---> Adder-cost: 5506   maxlim: 13   bits: 5/4
c ---[  40]---> Adder-cost: 512   maxlim: 1   bits: 2/1
c ---[  39]---> Adder-cost: 970   maxlim: 7   bits: 4/3
c ---[  38]---> Adder-cost: 1144   maxlim: 1   bits: 2/1
c ---[  37]---> Adder-cost: 1449   maxlim: 6   bits: 4/3
c ---[  36]---> Adder-cost: 845   maxlim: 1   bits: 2/1
c ---[  35]---> Adder-cost: 11037   maxlim: 17   bits: 6/5
c ---[  34]---> Adder-cost: 1107   maxlim: 6   bits: 4/3
c ---[  33]---> Adder-cost: 502   maxlim: 1   bits: 2/1
c ---[  32]---> Adder-cost: 935   maxlim: 10   bits: 5/4
c ---[  31]---> Adder-cost: 581   maxlim: 1   bits: 2/1
c ---[  30]---> Adder-cost: 2124   maxlim: 9   bits: 5/4
c ---[  29]---> Adder-cost: 1614   maxlim: 1   bits: 2/1
c ---[  28]---> Adder-cost: 2886   maxlim: 10   bits: 5/4
c ---[  27]---> Adder-cost: 2459   maxlim: 1   bits: 2/1
c ---[  26]---> Adder-cost: 8073   maxlim: 14   bits: 5/4
c ---[  25]---> Adder-cost: 331   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 931   maxlim: 12   bits: 5/4
c ---[  23]---> Adder-cost: 451   maxlim: 1   bits: 2/1
c ---[  22]---> Adder-cost: 626   maxlim: 1   bits: 2/1
c ---[  21]---> Adder-cost: 864   maxlim: 1   bits: 2/1
c ---[  20]---> Adder-cost: 1621   maxlim: 10   bits: 5/4
c ---[  19]---> Adder-cost: 631   maxlim: 1   bits: 2/1
c ---[  18]---> Adder-cost: 1115   maxlim: 10   bits: 5/4
c ---[  17]---> Adder-cost: 3227   maxlim: 11   bits: 5/4
c ---[  16]---> Adder-cost: 478   maxlim: 6   bits: 4/3
c ---[  15]---> Adder-cost: 1359   maxlim: 1   bits: 2/1
c ---[  14]---> Adder-cost: 803   maxlim: 1   bits: 2/1
c ---[  13]---> Adder-cost: 2215   maxlim: 8   bits: 5/4
c ---[  12]---> Adder-cost: 1906   maxlim: 1   bits: 2/1
c ---[  11]---> Adder-cost: 3911   maxlim: 11   bits: 5/4
c ---[  10]---> Adder-cost: 341   maxlim: 1   bits: 2/1
c ---[   9]---> Adder-cost: 571   maxlim: 6   bits: 4/3
c ---[   8]---> Adder-cost: 2757   maxlim: 18   bits: 6/5
c ---[   7]---> Adder-cost: 5364   maxlim: 13   bits: 5/4
c ---[   6]---> Adder-cost: 5675   maxlim: 12   bits: 5/4
c ---[   5]---> Adder-cost: 757   maxlim: 10   bits: 5/4
c ---[   4]---> Adder-cost: 1957   maxlim: 10   bits: 5/4
c ---[   3]---> Adder-cost: 5046   maxlim: 14   bits: 5/4
c ---[   2]---> Adder-cost: 2883   maxlim: 13   bits: 5/4
c ---[   1]---> Adder-cost: 2892   maxlim: 10   bits: 5/4
c ---[   0]---> Adder-cost: 2563   maxlim: 11   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1850483  6878053 |  616827       0        0     nan |  0.000 % |
c |       100 | 1850483  6878053 |  678509     100      330     3.3 |  1.232 % |
c |       251 | 1850476  6878030 |  746360     250      904     3.6 |  1.233 % |
c |       476 | 1850440  6877907 |  820996     472     1747     3.7 |  1.235 % |
c |       814 | 1850440  6877907 |  903096     810     3883     4.8 |  1.235 % |
c |      1320 | 1850213  6877104 |  993406    1299     5805     4.5 |  1.248 % |
c |      2080 | 1849839  6875792 | 1092746    2023     8600     4.3 |  1.271 % |
c |      3219 | 1849510  6874645 | 1202021    3132    14816     4.7 |  1.291 % |
c |      4927 | 1848904  6872538 | 1322223    4772    22644     4.7 |  1.326 % |
c |      7489 | 1848313  6870480 | 1454445    7266    41345     5.7 |  1.358 % |
c |     11334 | 1847517  6867740 | 1599890   10994    71032     6.5 |  1.400 % |
c |     17101 | 1845374  6860166 | 1759879   16458   112687     6.8 |  1.489 % |
c |     25751 | 1840912  6844623 | 1935867   24548   174368     7.1 |  1.689 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.18 0.04 0.01 2/54 14059
Raw data (stat): 14059 (runsolver) R 14058 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 467488478 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0013 s]
Raw data (loadavg): 0.38 0.09 0.03 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 34016 0 0 0 915 83 0 0 25 0 1 0 467488478 151834624 32308 4294967295 134512640 134672761 3221224544 3221223844 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37069 32308 603 41 0 37028 0
vsize: 148276
[startup+20.0018 s]
Raw data (loadavg): 0.47 0.12 0.04 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 34552 0 0 0 1911 85 0 0 25 0 1 0 467488478 153931776 32844 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37581 32844 603 41 0 37540 0
vsize: 150324
[startup+30.0112 s]
Raw data (loadavg): 0.55 0.15 0.04 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 34794 0 0 0 2909 85 0 0 25 0 1 0 467488478 155013120 33086 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37845 33086 603 41 0 37804 0
vsize: 151380
[startup+40.0197 s]
Raw data (loadavg): 0.62 0.18 0.05 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 35125 0 0 0 3908 86 0 0 25 0 1 0 467488478 156364800 33417 4294967295 134512640 134672761 3221224544 3221223752 134561960 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38175 33417 603 41 0 38134 0
vsize: 152700
[startup+50.0456 s]
Raw data (loadavg): 0.68 0.20 0.06 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 35323 0 0 0 4910 87 0 0 25 0 1 0 467488478 157175808 33615 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38373 33615 603 41 0 38332 0
vsize: 153492
[startup+60.0491 s]
Raw data (loadavg): 0.73 0.23 0.07 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 35530 0 0 0 5909 88 0 0 25 0 1 0 467488478 157986816 33822 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38571 33822 603 41 0 38530 0
vsize: 154284
[startup+70.0493 s]
Raw data (loadavg): 0.77 0.25 0.08 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 35675 0 0 0 6908 88 0 0 25 0 1 0 467488478 158527488 33967 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38703 33967 603 41 0 38662 0
vsize: 154812
[startup+80.0539 s]
Raw data (loadavg): 0.80 0.28 0.09 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 35800 0 0 0 7908 88 0 0 25 0 1 0 467488478 159068160 34092 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38835 34092 603 41 0 38794 0
vsize: 155340
[startup+90.0538 s]
Raw data (loadavg): 0.91 0.32 0.11 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 35956 0 0 0 8907 89 0 0 25 0 1 0 467488478 159744000 34248 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39000 34248 603 41 0 38959 0
vsize: 156000
[startup+100.053 s]
Raw data (loadavg): 0.92 0.34 0.12 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36041 0 0 0 9907 89 0 0 25 0 1 0 467488478 160014336 34333 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39066 34333 603 41 0 39025 0
vsize: 156264
[startup+110.064 s]
Raw data (loadavg): 0.93 0.36 0.13 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36126 0 0 0 10908 89 0 0 25 0 1 0 467488478 160419840 34418 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39165 34418 603 41 0 39124 0
vsize: 156660
[startup+120.093 s]
Raw data (loadavg): 0.94 0.38 0.13 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36185 0 0 0 11911 90 0 0 25 0 1 0 467488478 160690176 34477 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39231 34477 603 41 0 39190 0
vsize: 156924
[startup+130.098 s]
Raw data (loadavg): 0.95 0.40 0.14 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36278 0 0 0 12912 90 0 0 25 0 1 0 467488478 161095680 34570 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39330 34570 603 41 0 39289 0
vsize: 157320
[startup+140.098 s]
Raw data (loadavg): 0.96 0.42 0.15 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36371 0 0 0 13910 90 0 0 25 0 1 0 467488478 161366016 34663 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39396 34663 603 41 0 39355 0
vsize: 157584
[startup+150.103 s]
Raw data (loadavg): 0.96 0.44 0.16 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36436 0 0 0 14909 91 0 0 25 0 1 0 467488478 161636352 34728 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39462 34728 603 41 0 39421 0
vsize: 157848
[startup+160.106 s]
Raw data (loadavg): 0.97 0.46 0.17 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36480 0 0 0 15908 91 0 0 25 0 1 0 467488478 161771520 34772 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39495 34772 603 41 0 39454 0
vsize: 157980
[startup+170.106 s]
Raw data (loadavg): 0.97 0.47 0.18 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36506 0 0 0 16907 91 0 0 25 0 1 0 467488478 161906688 34798 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39528 34798 603 41 0 39487 0
vsize: 158112
[startup+180.107 s]
Raw data (loadavg): 0.98 0.49 0.19 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36526 0 0 0 17907 91 0 0 25 0 1 0 467488478 162041856 34818 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39561 34818 603 41 0 39520 0
vsize: 158244
[startup+190.111 s]
Raw data (loadavg): 0.98 0.51 0.19 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36550 0 0 0 18908 92 0 0 25 0 1 0 467488478 162041856 34842 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39561 34842 603 41 0 39520 0
vsize: 158244
[startup+200.165 s]
Raw data (loadavg): 0.98 0.52 0.20 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36588 0 0 0 19913 92 0 0 25 0 1 0 467488478 162177024 34880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39594 34880 603 41 0 39553 0
vsize: 158376
[startup+210.165 s]
Raw data (loadavg): 0.98 0.54 0.21 3/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36608 0 0 0 20914 92 0 0 25 0 1 0 467488478 162312192 34900 4294967295 134512640 134672761 3221224544 3221223760 134557528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39627 34900 603 41 0 39586 0
vsize: 158508
[startup+220.165 s]
Raw data (loadavg): 0.99 0.55 0.22 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36641 0 0 0 21913 92 0 0 25 0 1 0 467488478 162447360 34933 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39660 34933 603 41 0 39619 0
vsize: 158640
[startup+230.166 s]
Raw data (loadavg): 0.99 0.57 0.23 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36683 0 0 0 22914 92 0 0 25 0 1 0 467488478 162590720 34975 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39695 34975 603 41 0 39654 0
vsize: 158780
[startup+240.166 s]
Raw data (loadavg): 0.99 0.58 0.23 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36710 0 0 0 23914 92 0 0 25 0 1 0 467488478 162725888 35002 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39728 35002 603 41 0 39687 0
vsize: 158912
[startup+250.166 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36723 0 0 0 24914 92 0 0 25 0 1 0 467488478 162725888 35015 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39728 35015 603 41 0 39687 0
vsize: 158912
[startup+260.169 s]
Raw data (loadavg): 0.99 0.61 0.25 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36756 0 0 0 25914 92 0 0 25 0 1 0 467488478 162861056 35048 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39761 35048 603 41 0 39720 0
vsize: 159044
[startup+270.169 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36778 0 0 0 26914 92 0 0 25 0 1 0 467488478 162996224 35070 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39794 35070 603 41 0 39753 0
vsize: 159176
[startup+280.169 s]
Raw data (loadavg): 0.99 0.63 0.26 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36796 0 0 0 27914 92 0 0 25 0 1 0 467488478 162996224 35088 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39794 35088 603 41 0 39753 0
vsize: 159176
[startup+290.2 s]
Raw data (loadavg): 0.99 0.64 0.27 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36820 0 0 0 28918 92 0 0 25 0 1 0 467488478 163131392 35112 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39827 35112 603 41 0 39786 0
vsize: 159308
[startup+300.2 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36833 0 0 0 29918 92 0 0 25 0 1 0 467488478 163131392 35125 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39827 35125 603 41 0 39786 0
vsize: 159308
[startup+310.2 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36840 0 0 0 30918 93 0 0 25 0 1 0 467488478 163266560 35132 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39860 35132 603 41 0 39819 0
vsize: 159440
[startup+320.2 s]
Raw data (loadavg): 0.99 0.68 0.29 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36852 0 0 0 31918 93 0 0 25 0 1 0 467488478 163266560 35144 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39860 35144 603 41 0 39819 0
vsize: 159440
[startup+330.209 s]
Raw data (loadavg): 0.99 0.69 0.30 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36866 0 0 0 32919 93 0 0 25 0 1 0 467488478 163266560 35158 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39860 35158 603 41 0 39819 0
vsize: 159440
[startup+340.209 s]
Raw data (loadavg): 0.99 0.70 0.31 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36871 0 0 0 33919 93 0 0 25 0 1 0 467488478 163266560 35163 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39860 35163 603 41 0 39819 0
vsize: 159440
[startup+350.211 s]
Raw data (loadavg): 0.99 0.71 0.31 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36886 0 0 0 34919 93 0 0 25 0 1 0 467488478 163401728 35178 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39893 35178 603 41 0 39852 0
vsize: 159572
[startup+360.214 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36892 0 0 0 35920 93 0 0 25 0 1 0 467488478 163401728 35184 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39893 35184 603 41 0 39852 0
vsize: 159572
[startup+370.214 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36898 0 0 0 36920 93 0 0 25 0 1 0 467488478 163401728 35190 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39893 35190 603 41 0 39852 0
vsize: 159572
[startup+380.214 s]
Raw data (loadavg): 0.99 0.73 0.33 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36906 0 0 0 37920 93 0 0 25 0 1 0 467488478 163536896 35198 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39926 35198 603 41 0 39885 0
vsize: 159704
[startup+390.214 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36914 0 0 0 38920 93 0 0 25 0 1 0 467488478 163536896 35206 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39926 35206 603 41 0 39885 0
vsize: 159704
[startup+400.214 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36924 0 0 0 39920 93 0 0 25 0 1 0 467488478 163536896 35216 4294967295 134512640 134672761 3221224544 3221223760 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39926 35216 603 41 0 39885 0
vsize: 159704
[startup+410.214 s]
Raw data (loadavg): 0.99 0.76 0.35 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36930 0 0 0 40920 93 0 0 25 0 1 0 467488478 163536896 35222 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39926 35222 603 41 0 39885 0
vsize: 159704
[startup+420.214 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36944 0 0 0 41921 93 0 0 25 0 1 0 467488478 163672064 35236 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39959 35236 603 41 0 39918 0
vsize: 159836
[startup+430.214 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36950 0 0 0 42921 93 0 0 25 0 1 0 467488478 163672064 35242 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39959 35242 603 41 0 39918 0
vsize: 159836
[startup+440.214 s]
Raw data (loadavg): 0.99 0.78 0.37 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36967 0 0 0 43921 93 0 0 25 0 1 0 467488478 163672064 35259 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39959 35259 603 41 0 39918 0
vsize: 159836
[startup+450.214 s]
Raw data (loadavg): 0.99 0.79 0.38 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36974 0 0 0 44921 93 0 0 25 0 1 0 467488478 163672064 35266 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39959 35266 603 41 0 39918 0
vsize: 159836
[startup+460.214 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36990 0 0 0 45921 93 0 0 25 0 1 0 467488478 163807232 35282 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39992 35282 603 41 0 39951 0
vsize: 159968
[startup+470.214 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 36998 0 0 0 46921 93 0 0 25 0 1 0 467488478 163807232 35290 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39992 35290 603 41 0 39951 0
vsize: 159968
[startup+480.214 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37005 0 0 0 47922 93 0 0 25 0 1 0 467488478 163807232 35297 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39992 35297 603 41 0 39951 0
vsize: 159968
[startup+490.214 s]
Raw data (loadavg): 0.99 0.81 0.40 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37032 0 0 0 48921 93 0 0 25 0 1 0 467488478 164057088 35324 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40053 35324 603 41 0 40012 0
vsize: 160212
[startup+500.214 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37032 0 0 0 49922 93 0 0 25 0 1 0 467488478 164057088 35324 4294967295 134512640 134672761 3221224544 3221223712 134564668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40053 35324 603 41 0 40012 0
vsize: 160212
[startup+510.214 s]
Raw data (loadavg): 0.99 0.82 0.41 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37034 0 0 0 50922 93 0 0 25 0 1 0 467488478 164057088 35326 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40053 35326 603 41 0 40012 0
vsize: 160212
[startup+520.214 s]
Raw data (loadavg): 0.99 0.83 0.42 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37039 0 0 0 51922 93 0 0 25 0 1 0 467488478 164057088 35331 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40053 35331 603 41 0 40012 0
vsize: 160212
[startup+530.215 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37044 0 0 0 52922 93 0 0 25 0 1 0 467488478 164057088 35336 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40053 35336 603 41 0 40012 0
vsize: 160212
[startup+540.215 s]
Raw data (loadavg): 0.99 0.84 0.43 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37050 0 0 0 53922 93 0 0 25 0 1 0 467488478 164057088 35342 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40053 35342 603 41 0 40012 0
vsize: 160212
[startup+550.215 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37054 0 0 0 54922 93 0 0 25 0 1 0 467488478 164057088 35346 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40053 35346 603 41 0 40012 0
vsize: 160212
[startup+560.215 s]
Raw data (loadavg): 0.99 0.85 0.44 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37071 0 0 0 55923 93 0 0 25 0 1 0 467488478 164057088 35363 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40053 35363 603 41 0 40012 0
vsize: 160212
[startup+570.215 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37075 0 0 0 56923 93 0 0 25 0 1 0 467488478 164192256 35367 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40086 35367 603 41 0 40045 0
vsize: 160344
[startup+580.215 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37080 0 0 0 57923 93 0 0 25 0 1 0 467488478 164192256 35372 4294967295 134512640 134672761 3221224544 3221223708 134561028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40086 35372 603 41 0 40045 0
vsize: 160344
[startup+590.215 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37090 0 0 0 58923 93 0 0 25 0 1 0 467488478 164192256 35382 4294967295 134512640 134672761 3221224544 3221223760 134561950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40086 35382 603 41 0 40045 0
vsize: 160344
[startup+600.215 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37098 0 0 0 59923 93 0 0 25 0 1 0 467488478 164192256 35390 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40086 35390 603 41 0 40045 0
vsize: 160344
[startup+610.216 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37102 0 0 0 60923 93 0 0 25 0 1 0 467488478 164192256 35394 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40086 35394 603 41 0 40045 0
vsize: 160344
[startup+620.216 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37112 0 0 0 61923 94 0 0 25 0 1 0 467488478 164192256 35404 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40086 35404 603 41 0 40045 0
vsize: 160344
[startup+630.216 s]
Raw data (loadavg): 0.99 0.88 0.48 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37117 0 0 0 62924 94 0 0 25 0 1 0 467488478 164327424 35409 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40119 35409 603 41 0 40078 0
vsize: 160476
[startup+640.217 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37122 0 0 0 63924 94 0 0 25 0 1 0 467488478 164327424 35414 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40119 35414 603 41 0 40078 0
vsize: 160476
[startup+650.217 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37128 0 0 0 64924 94 0 0 25 0 1 0 467488478 164327424 35420 4294967295 134512640 134672761 3221224544 3221223712 134560819 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40119 35420 603 41 0 40078 0
vsize: 160476
[startup+660.218 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37139 0 0 0 65924 94 0 0 25 0 1 0 467488478 164327424 35431 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40119 35431 603 41 0 40078 0
vsize: 160476
[startup+670.217 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37146 0 0 0 66924 94 0 0 25 0 1 0 467488478 164327424 35438 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40119 35438 603 41 0 40078 0
vsize: 160476
[startup+680.218 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37153 0 0 0 67924 94 0 0 25 0 1 0 467488478 164327424 35445 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40119 35445 603 41 0 40078 0
vsize: 160476
[startup+690.218 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37160 0 0 0 68925 94 0 0 25 0 1 0 467488478 164462592 35452 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40152 35452 603 41 0 40111 0
vsize: 160608
[startup+700.218 s]
Raw data (loadavg): 0.99 0.90 0.51 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37163 0 0 0 69925 94 0 0 25 0 1 0 467488478 164462592 35455 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40152 35455 603 41 0 40111 0
vsize: 160608
[startup+710.219 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37168 0 0 0 70925 94 0 0 25 0 1 0 467488478 164462592 35460 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40152 35460 603 41 0 40111 0
vsize: 160608
[startup+720.218 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37174 0 0 0 71925 94 0 0 25 0 1 0 467488478 164462592 35466 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40152 35466 603 41 0 40111 0
vsize: 160608
[startup+730.219 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37178 0 0 0 72925 94 0 0 25 0 1 0 467488478 164462592 35470 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40152 35470 603 41 0 40111 0
vsize: 160608
[startup+740.22 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37184 0 0 0 73925 94 0 0 25 0 1 0 467488478 164462592 35476 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40152 35476 603 41 0 40111 0
vsize: 160608
[startup+750.22 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37189 0 0 0 74926 94 0 0 25 0 1 0 467488478 164597760 35481 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40185 35481 603 41 0 40144 0
vsize: 160740
[startup+760.225 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37195 0 0 0 75926 94 0 0 25 0 1 0 467488478 164597760 35487 4294967295 134512640 134672761 3221224544 3221223780 134557604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40185 35487 603 41 0 40144 0
vsize: 160740
[startup+770.234 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37202 0 0 0 76927 94 0 0 25 0 1 0 467488478 164597760 35494 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40185 35494 603 41 0 40144 0
vsize: 160740
[startup+780.244 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37204 0 0 0 77929 94 0 0 25 0 1 0 467488478 164597760 35496 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40185 35496 603 41 0 40144 0
vsize: 160740
[startup+790.244 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37218 0 0 0 78929 94 0 0 25 0 1 0 467488478 164597760 35510 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40185 35510 603 41 0 40144 0
vsize: 160740
[startup+800.244 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37229 0 0 0 79928 94 0 0 25 0 1 0 467488478 164597760 35521 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40185 35521 603 41 0 40144 0
vsize: 160740
[startup+810.244 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37242 0 0 0 80929 94 0 0 25 0 1 0 467488478 164732928 35534 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40218 35534 603 41 0 40177 0
vsize: 160872
[startup+820.244 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37245 0 0 0 81929 94 0 0 25 0 1 0 467488478 164732928 35537 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40218 35537 603 41 0 40177 0
vsize: 160872
[startup+830.261 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37251 0 0 0 82931 94 0 0 25 0 1 0 467488478 164732928 35543 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40218 35543 603 41 0 40177 0
vsize: 160872
[startup+840.261 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37256 0 0 0 83931 94 0 0 25 0 1 0 467488478 164732928 35548 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40218 35548 603 41 0 40177 0
vsize: 160872
[startup+850.261 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37259 0 0 0 84931 94 0 0 25 0 1 0 467488478 164732928 35551 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40218 35551 603 41 0 40177 0
vsize: 160872
[startup+860.261 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37264 0 0 0 85931 94 0 0 25 0 1 0 467488478 164732928 35556 4294967295 134512640 134672761 3221224544 3221223680 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40218 35556 603 41 0 40177 0
vsize: 160872
[startup+870.261 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37269 0 0 0 86931 94 0 0 25 0 1 0 467488478 164732928 35561 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40218 35561 603 41 0 40177 0
vsize: 160872
[startup+880.262 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37271 0 0 0 87932 94 0 0 25 0 1 0 467488478 164732928 35563 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40218 35563 603 41 0 40177 0
vsize: 160872
[startup+890.264 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37274 0 0 0 88932 94 0 0 25 0 1 0 467488478 164868096 35566 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40251 35566 603 41 0 40210 0
vsize: 161004
[startup+900.264 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37277 0 0 0 89932 94 0 0 25 0 1 0 467488478 164868096 35569 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40251 35569 603 41 0 40210 0
vsize: 161004
[startup+910.263 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37287 0 0 0 90932 94 0 0 25 0 1 0 467488478 164868096 35579 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40251 35579 603 41 0 40210 0
vsize: 161004
[startup+920.264 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37289 0 0 0 91932 94 0 0 25 0 1 0 467488478 164868096 35581 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40251 35581 603 41 0 40210 0
vsize: 161004
[startup+930.263 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37311 0 0 0 92932 94 0 0 25 0 1 0 467488478 165003264 35603 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40284 35603 603 41 0 40243 0
vsize: 161136
[startup+940.263 s]
Raw data (loadavg): 0.99 0.95 0.61 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37320 0 0 0 93932 94 0 0 25 0 1 0 467488478 165003264 35612 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40284 35612 603 41 0 40243 0
vsize: 161136
[startup+950.27 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37323 0 0 0 94933 94 0 0 25 0 1 0 467488478 165003264 35615 4294967295 134512640 134672761 3221224544 3221223728 134558275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40284 35615 603 41 0 40243 0
vsize: 161136
[startup+960.27 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37325 0 0 0 95933 94 0 0 25 0 1 0 467488478 165003264 35617 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40284 35617 603 41 0 40243 0
vsize: 161136
[startup+970.27 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37331 0 0 0 96934 94 0 0 25 0 1 0 467488478 165003264 35623 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40284 35623 603 41 0 40243 0
vsize: 161136
[startup+980.27 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37334 0 0 0 97934 94 0 0 25 0 1 0 467488478 165003264 35626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40284 35626 603 41 0 40243 0
vsize: 161136
[startup+990.271 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37336 0 0 0 98934 94 0 0 25 0 1 0 467488478 165003264 35628 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40284 35628 603 41 0 40243 0
vsize: 161136
[startup+1000.27 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37340 0 0 0 99934 94 0 0 25 0 1 0 467488478 165003264 35632 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40284 35632 603 41 0 40243 0
vsize: 161136
[startup+1010.27 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37342 0 0 0 100934 95 0 0 25 0 1 0 467488478 165003264 35634 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40284 35634 603 41 0 40243 0
vsize: 161136
[startup+1020.27 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37353 0 0 0 101934 95 0 0 25 0 1 0 467488478 165138432 35645 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40317 35645 603 41 0 40276 0
vsize: 161268
[startup+1030.27 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37357 0 0 0 102934 95 0 0 25 0 1 0 467488478 165138432 35649 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40317 35649 603 41 0 40276 0
vsize: 161268
[startup+1040.27 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37359 0 0 0 103935 95 0 0 25 0 1 0 467488478 165138432 35651 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40317 35651 603 41 0 40276 0
vsize: 161268
[startup+1050.27 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37363 0 0 0 104935 95 0 0 25 0 1 0 467488478 165138432 35655 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40317 35655 603 41 0 40276 0
vsize: 161268
[startup+1060.27 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37365 0 0 0 105935 95 0 0 25 0 1 0 467488478 165138432 35657 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40317 35657 603 41 0 40276 0
vsize: 161268
[startup+1070.27 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37368 0 0 0 106935 95 0 0 25 0 1 0 467488478 165138432 35660 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40317 35660 603 41 0 40276 0
vsize: 161268
[startup+1080.27 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37370 0 0 0 107935 95 0 0 25 0 1 0 467488478 165138432 35662 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40317 35662 603 41 0 40276 0
vsize: 161268
[startup+1090.27 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37421 0 0 0 108936 95 0 0 25 0 1 0 467488478 165535744 35713 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35713 603 41 0 40373 0
vsize: 161656
[startup+1100.27 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37421 0 0 0 109936 95 0 0 25 0 1 0 467488478 165535744 35713 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35713 603 41 0 40373 0
vsize: 161656
[startup+1110.27 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37422 0 0 0 110936 95 0 0 25 0 1 0 467488478 165535744 35714 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35714 603 41 0 40373 0
vsize: 161656
[startup+1120.27 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37427 0 0 0 111936 95 0 0 25 0 1 0 467488478 165535744 35719 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35719 603 41 0 40373 0
vsize: 161656
[startup+1130.27 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37428 0 0 0 112936 95 0 0 25 0 1 0 467488478 165535744 35720 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35720 603 41 0 40373 0
vsize: 161656
[startup+1140.27 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37428 0 0 0 113936 95 0 0 25 0 1 0 467488478 165535744 35720 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35720 603 41 0 40373 0
vsize: 161656
[startup+1150.27 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37428 0 0 0 114937 95 0 0 25 0 1 0 467488478 165535744 35720 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35720 603 41 0 40373 0
vsize: 161656
[startup+1160.28 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37429 0 0 0 115937 95 0 0 25 0 1 0 467488478 165535744 35721 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35721 603 41 0 40373 0
vsize: 161656
[startup+1170.28 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37431 0 0 0 116937 95 0 0 25 0 1 0 467488478 165535744 35723 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35723 603 41 0 40373 0
vsize: 161656
[startup+1180.28 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37433 0 0 0 117937 95 0 0 25 0 1 0 467488478 165535744 35725 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35725 603 41 0 40373 0
vsize: 161656
[startup+1190.28 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37437 0 0 0 118938 95 0 0 25 0 1 0 467488478 165535744 35729 4294967295 134512640 134672761 3221224544 3221223760 134561985 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35729 603 41 0 40373 0
vsize: 161656
[startup+1200.28 s]
Raw data (loadavg): 0.99 0.97 0.70 2/54 14059
Raw data (stat): 14059 (minisat+) R 14058 26667 26666 0 -1 0 37444 0 0 0 119938 95 0 0 25 0 1 0 467488478 165535744 35736 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40414 35736 603 41 0 40373 0
vsize: 161656
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.39 s]
Raw data (loadavg): 0.99 0.97 0.70 1/54 14059
Raw data (stat): 14059 (minisat+) Z 14058 26667 26666 0 -1 12 37446 0 0 0 119938 102 0 0 22 0 1 0 467488478 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.39
CPU time (s): 1200.41
CPU user time (s): 1199.39
CPU system time (s): 1.02284
CPU usage (%): 100.002
Max. virtual memory (Kb): 161656
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####