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-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-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.81066
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 14708

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-21 00:52:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=20277 boxname=wulflinc6 idbench=1560 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b6b40b25db69f63dc02649b5c9a3693a  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-sp98ic.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-sp98ic.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-sp98ic.opb
IDLAUNCH: 20277
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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.042
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:        785892 kB
Buffers:         30468 kB
Cached:         196036 kB
SwapCached:          4 kB
Active:         102176 kB
Inactive:       126856 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        785640 kB
SwapTotal:     2097136 kB
SwapFree:      2096768 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5924 kB
Slab:            14064 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 01:12:59 (client local time) WITH STATUS 0 IN 1200.61 SECONDS
stats: 20277 7 1200.61 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.85 0.97 0.92 2/54 27328
Raw data (stat): 27328 (runsolver) R 27327 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 482685550 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.0004 s]
Raw data (loadavg): 0.87 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 34016 0 0 0 915 84 0 0 25 0 1 0 482685550 151834624 32308 4294967295 134512640 134672761 3221224544 3221223844 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37069 32308 603 41 0 37028 0
vsize: 148276
[startup+20.0001 s]
Raw data (loadavg): 0.89 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 34552 0 0 0 1915 84 0 0 25 0 1 0 482685550 153931776 32844 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37581 32844 603 41 0 37540 0
vsize: 150324
[startup+30.0007 s]
Raw data (loadavg): 0.91 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 34794 0 0 0 2914 85 0 0 25 0 1 0 482685550 155013120 33086 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.0005 s]
Raw data (loadavg): 0.92 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 35123 0 0 0 3914 86 0 0 25 0 1 0 482685550 156364800 33415 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38175 33415 603 41 0 38134 0
vsize: 152700
[startup+50.0005 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 35321 0 0 0 4913 87 0 0 25 0 1 0 482685550 157175808 33613 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38373 33613 603 41 0 38332 0
vsize: 153492
[startup+60.0011 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 35530 0 0 0 5912 88 0 0 25 0 1 0 482685550 157986816 33822 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38571 33822 603 41 0 38530 0
vsize: 154284
[startup+70.0013 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 35675 0 0 0 6912 89 0 0 25 0 1 0 482685550 158527488 33967 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38703 33967 603 41 0 38662 0
vsize: 154812
[startup+80.001 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 35800 0 0 0 7911 90 0 0 25 0 1 0 482685550 159068160 34092 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38835 34092 603 41 0 38794 0
vsize: 155340
[startup+90.0016 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 35956 0 0 0 8911 90 0 0 25 0 1 0 482685550 159744000 34248 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39000 34248 603 41 0 38959 0
vsize: 156000
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36041 0 0 0 9910 91 0 0 25 0 1 0 482685550 160014336 34333 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39066 34333 603 41 0 39025 0
vsize: 156264
[startup+110.001 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36126 0 0 0 10910 91 0 0 25 0 1 0 482685550 160419840 34418 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39165 34418 603 41 0 39124 0
vsize: 156660
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36185 0 0 0 11910 91 0 0 25 0 1 0 482685550 160690176 34477 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39231 34477 603 41 0 39190 0
vsize: 156924
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36278 0 0 0 12910 92 0 0 25 0 1 0 482685550 161095680 34570 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39330 34570 603 41 0 39289 0
vsize: 157320
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36368 0 0 0 13909 93 0 0 25 0 1 0 482685550 161366016 34660 4294967295 134512640 134672761 3221224544 3221223760 134557677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39396 34660 603 41 0 39355 0
vsize: 157584
[startup+150.003 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36435 0 0 0 14909 94 0 0 25 0 1 0 482685550 161636352 34727 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39462 34727 603 41 0 39421 0
vsize: 157848
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36480 0 0 0 15909 94 0 0 25 0 1 0 482685550 161771520 34772 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36506 0 0 0 16909 95 0 0 25 0 1 0 482685550 161906688 34798 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39528 34798 603 41 0 39487 0
vsize: 158112
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36526 0 0 0 17908 95 0 0 25 0 1 0 482685550 162041856 34818 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39561 34818 603 41 0 39520 0
vsize: 158244
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36550 0 0 0 18908 96 0 0 25 0 1 0 482685550 162041856 34842 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39561 34842 603 41 0 39520 0
vsize: 158244
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36586 0 0 0 19908 96 0 0 25 0 1 0 482685550 162177024 34878 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39594 34878 603 41 0 39553 0
vsize: 158376
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36607 0 0 0 20908 96 0 0 25 0 1 0 482685550 162312192 34899 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39627 34899 603 41 0 39586 0
vsize: 158508
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36640 0 0 0 21908 97 0 0 25 0 1 0 482685550 162447360 34932 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39660 34932 603 41 0 39619 0
vsize: 158640
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36682 0 0 0 22908 97 0 0 25 0 1 0 482685550 162590720 34974 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39695 34974 603 41 0 39654 0
vsize: 158780
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36710 0 0 0 23908 97 0 0 25 0 1 0 482685550 162725888 35002 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39728 35002 603 41 0 39687 0
vsize: 158912
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36722 0 0 0 24908 98 0 0 25 0 1 0 482685550 162725888 35014 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39728 35014 603 41 0 39687 0
vsize: 158912
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36756 0 0 0 25908 98 0 0 25 0 1 0 482685550 162861056 35048 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39761 35048 603 41 0 39720 0
vsize: 159044
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36777 0 0 0 26908 98 0 0 25 0 1 0 482685550 162996224 35069 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39794 35069 603 41 0 39753 0
vsize: 159176
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36796 0 0 0 27908 98 0 0 25 0 1 0 482685550 162996224 35088 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39794 35088 603 41 0 39753 0
vsize: 159176
[startup+290.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36819 0 0 0 28908 99 0 0 25 0 1 0 482685550 163131392 35111 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39827 35111 603 41 0 39786 0
vsize: 159308
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36832 0 0 0 29908 99 0 0 25 0 1 0 482685550 163131392 35124 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39827 35124 603 41 0 39786 0
vsize: 159308
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36840 0 0 0 30908 100 0 0 25 0 1 0 482685550 163266560 35132 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39860 35132 603 41 0 39819 0
vsize: 159440
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36852 0 0 0 31907 100 0 0 25 0 1 0 482685550 163266560 35144 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39860 35144 603 41 0 39819 0
vsize: 159440
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36864 0 0 0 32907 100 0 0 25 0 1 0 482685550 163266560 35156 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39860 35156 603 41 0 39819 0
vsize: 159440
[startup+340.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36871 0 0 0 33907 101 0 0 25 0 1 0 482685550 163266560 35163 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39860 35163 603 41 0 39819 0
vsize: 159440
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36886 0 0 0 34907 101 0 0 25 0 1 0 482685550 163401728 35178 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39893 35178 603 41 0 39852 0
vsize: 159572
[startup+360.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36892 0 0 0 35908 101 0 0 25 0 1 0 482685550 163401728 35184 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39893 35184 603 41 0 39852 0
vsize: 159572
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36898 0 0 0 36908 102 0 0 25 0 1 0 482685550 163401728 35190 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39893 35190 603 41 0 39852 0
vsize: 159572
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36906 0 0 0 37907 102 0 0 25 0 1 0 482685550 163536896 35198 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39926 35198 603 41 0 39885 0
vsize: 159704
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36914 0 0 0 38907 102 0 0 25 0 1 0 482685550 163536896 35206 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39926 35206 603 41 0 39885 0
vsize: 159704
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36924 0 0 0 39907 103 0 0 25 0 1 0 482685550 163536896 35216 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39926 35216 603 41 0 39885 0
vsize: 159704
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36930 0 0 0 40907 103 0 0 25 0 1 0 482685550 163536896 35222 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39926 35222 603 41 0 39885 0
vsize: 159704
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27328
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36944 0 0 0 41907 104 0 0 25 0 1 0 482685550 163672064 35236 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39959 35236 603 41 0 39918 0
vsize: 159836
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/57 27363
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36950 0 0 0 42907 104 0 0 25 0 1 0 482685550 163672064 35242 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.017 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 27381
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36967 0 0 0 43907 104 0 0 25 0 1 0 482685550 163672064 35259 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.018 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 27381
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36974 0 0 0 44907 105 0 0 25 0 1 0 482685550 163672064 35266 4294967295 134512640 134672761 3221224544 3221223716 134556602 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.018 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 27381
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36990 0 0 0 45907 105 0 0 25 0 1 0 482685550 163807232 35282 4294967295 134512640 134672761 3221224544 3221223744 134557895 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.019 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 27381
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 36998 0 0 0 46907 105 0 0 25 0 1 0 482685550 163807232 35290 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.019 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 27381
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37005 0 0 0 47907 106 0 0 25 0 1 0 482685550 163807232 35297 4294967295 134512640 134672761 3221224544 3221223712 134561201 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.02 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 27381
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37032 0 0 0 48907 106 0 0 25 0 1 0 482685550 164057088 35324 4294967295 134512640 134672761 3221224544 3221223668 134566122 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.02 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37032 0 0 0 49907 107 0 0 25 0 1 0 482685550 164057088 35324 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.021 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37034 0 0 0 50907 107 0 0 25 0 1 0 482685550 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.021 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37039 0 0 0 51907 107 0 0 25 0 1 0 482685550 164057088 35331 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40053 35331 603 41 0 40012 0
vsize: 160212
[startup+530.02 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37044 0 0 0 52907 107 0 0 25 0 1 0 482685550 164057088 35336 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40053 35336 603 41 0 40012 0
vsize: 160212
[startup+540.021 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37050 0 0 0 53908 107 0 0 25 0 1 0 482685550 164057088 35342 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40053 35342 603 41 0 40012 0
vsize: 160212
[startup+550.021 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37054 0 0 0 54908 107 0 0 25 0 1 0 482685550 164057088 35346 4294967295 134512640 134672761 3221224544 3221223744 134557876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40053 35346 603 41 0 40012 0
vsize: 160212
[startup+560.021 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37071 0 0 0 55908 107 0 0 25 0 1 0 482685550 164057088 35363 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40053 35363 603 41 0 40012 0
vsize: 160212
[startup+570.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37076 0 0 0 56908 108 0 0 25 0 1 0 482685550 164192256 35368 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40086 35368 603 41 0 40045 0
vsize: 160344
[startup+580.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37085 0 0 0 57909 108 0 0 25 0 1 0 482685550 164192256 35377 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40086 35377 603 41 0 40045 0
vsize: 160344
[startup+590.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37090 0 0 0 58909 108 0 0 25 0 1 0 482685550 164192256 35382 4294967295 134512640 134672761 3221224544 3221223760 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40086 35382 603 41 0 40045 0
vsize: 160344
[startup+600.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37098 0 0 0 59909 108 0 0 25 0 1 0 482685550 164192256 35390 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40086 35390 603 41 0 40045 0
vsize: 160344
[startup+610.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37103 0 0 0 60910 108 0 0 25 0 1 0 482685550 164192256 35395 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40086 35395 603 41 0 40045 0
vsize: 160344
[startup+620.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37113 0 0 0 61910 108 0 0 25 0 1 0 482685550 164192256 35405 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40086 35405 603 41 0 40045 0
vsize: 160344
[startup+630.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37117 0 0 0 62910 108 0 0 25 0 1 0 482685550 164327424 35409 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40119 35409 603 41 0 40078 0
vsize: 160476
[startup+640.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37123 0 0 0 63911 108 0 0 25 0 1 0 482685550 164327424 35415 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40119 35415 603 41 0 40078 0
vsize: 160476
[startup+650.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37128 0 0 0 64911 108 0 0 25 0 1 0 482685550 164327424 35420 4294967295 134512640 134672761 3221224544 3221223716 134556685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40119 35420 603 41 0 40078 0
vsize: 160476
[startup+660.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37139 0 0 0 65911 108 0 0 25 0 1 0 482685550 164327424 35431 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40119 35431 603 41 0 40078 0
vsize: 160476
[startup+670.023 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37146 0 0 0 66912 108 0 0 25 0 1 0 482685550 164327424 35438 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40119 35438 603 41 0 40078 0
vsize: 160476
[startup+680.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37154 0 0 0 67912 108 0 0 25 0 1 0 482685550 164462592 35446 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40152 35446 603 41 0 40111 0
vsize: 160608
[startup+690.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37160 0 0 0 68912 108 0 0 25 0 1 0 482685550 164462592 35452 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40152 35452 603 41 0 40111 0
vsize: 160608
[startup+700.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37163 0 0 0 69913 108 0 0 25 0 1 0 482685550 164462592 35455 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40152 35455 603 41 0 40111 0
vsize: 160608
[startup+710.024 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37169 0 0 0 70913 108 0 0 25 0 1 0 482685550 164462592 35461 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40152 35461 603 41 0 40111 0
vsize: 160608
[startup+720.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37174 0 0 0 71913 108 0 0 25 0 1 0 482685550 164462592 35466 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40152 35466 603 41 0 40111 0
vsize: 160608
[startup+730.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37179 0 0 0 72914 108 0 0 25 0 1 0 482685550 164462592 35471 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40152 35471 603 41 0 40111 0
vsize: 160608
[startup+740.025 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27383
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37184 0 0 0 73914 108 0 0 25 0 1 0 482685550 164462592 35476 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40152 35476 603 41 0 40111 0
vsize: 160608
[startup+750.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37190 0 0 0 74914 108 0 0 25 0 1 0 482685550 164597760 35482 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40185 35482 603 41 0 40144 0
vsize: 160740
[startup+760.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37195 0 0 0 75915 108 0 0 25 0 1 0 482685550 164597760 35487 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40185 35487 603 41 0 40144 0
vsize: 160740
[startup+770.032 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37202 0 0 0 76915 108 0 0 25 0 1 0 482685550 164597760 35494 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40185 35494 603 41 0 40144 0
vsize: 160740
[startup+780.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37204 0 0 0 77915 108 0 0 25 0 1 0 482685550 164597760 35496 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40185 35496 603 41 0 40144 0
vsize: 160740
[startup+790.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37218 0 0 0 78916 108 0 0 25 0 1 0 482685550 164597760 35510 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40185 35510 603 41 0 40144 0
vsize: 160740
[startup+800.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37229 0 0 0 79915 109 0 0 25 0 1 0 482685550 164597760 35521 4294967295 134512640 134672761 3221224544 3221223712 134560811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40185 35521 603 41 0 40144 0
vsize: 160740
[startup+810.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37242 0 0 0 80916 109 0 0 25 0 1 0 482685550 164732928 35534 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40218 35534 603 41 0 40177 0
vsize: 160872
[startup+820.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37245 0 0 0 81916 109 0 0 25 0 1 0 482685550 164732928 35537 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40218 35537 603 41 0 40177 0
vsize: 160872
[startup+830.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37251 0 0 0 82916 109 0 0 25 0 1 0 482685550 164732928 35543 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40218 35543 603 41 0 40177 0
vsize: 160872
[startup+840.033 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37256 0 0 0 83917 109 0 0 25 0 1 0 482685550 164732928 35548 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40218 35548 603 41 0 40177 0
vsize: 160872
[startup+850.037 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37260 0 0 0 84917 109 0 0 25 0 1 0 482685550 164732928 35552 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40218 35552 603 41 0 40177 0
vsize: 160872
[startup+860.037 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37264 0 0 0 85918 109 0 0 25 0 1 0 482685550 164732928 35556 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40218 35556 603 41 0 40177 0
vsize: 160872
[startup+870.037 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37269 0 0 0 86918 109 0 0 25 0 1 0 482685550 164732928 35561 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40218 35561 603 41 0 40177 0
vsize: 160872
[startup+880.037 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37271 0 0 0 87918 109 0 0 25 0 1 0 482685550 164732928 35563 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40218 35563 603 41 0 40177 0
vsize: 160872
[startup+890.038 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37274 0 0 0 88919 109 0 0 25 0 1 0 482685550 164868096 35566 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40251 35566 603 41 0 40210 0
vsize: 161004
[startup+900.139 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37277 0 0 0 89929 109 0 0 25 0 1 0 482685550 164868096 35569 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40251 35569 603 41 0 40210 0
vsize: 161004
[startup+910.139 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37288 0 0 0 90929 109 0 0 25 0 1 0 482685550 164868096 35580 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40251 35580 603 41 0 40210 0
vsize: 161004
[startup+920.141 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37289 0 0 0 91930 109 0 0 25 0 1 0 482685550 164868096 35581 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40251 35581 603 41 0 40210 0
vsize: 161004
[startup+930.141 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37311 0 0 0 92930 109 0 0 25 0 1 0 482685550 165003264 35603 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40284 35603 603 41 0 40243 0
vsize: 161136
[startup+940.141 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37320 0 0 0 93930 109 0 0 25 0 1 0 482685550 165003264 35612 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40284 35612 603 41 0 40243 0
vsize: 161136
[startup+950.141 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37323 0 0 0 94931 109 0 0 25 0 1 0 482685550 165003264 35615 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40284 35615 603 41 0 40243 0
vsize: 161136
[startup+960.141 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37327 0 0 0 95931 109 0 0 25 0 1 0 482685550 165003264 35619 4294967295 134512640 134672761 3221224544 3221223792 134562236 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40284 35619 603 41 0 40243 0
vsize: 161136
[startup+970.141 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37331 0 0 0 96931 109 0 0 25 0 1 0 482685550 165003264 35623 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40284 35623 603 41 0 40243 0
vsize: 161136
[startup+980.141 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37335 0 0 0 97932 109 0 0 25 0 1 0 482685550 165003264 35627 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40284 35627 603 41 0 40243 0
vsize: 161136
[startup+990.142 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37337 0 0 0 98932 109 0 0 25 0 1 0 482685550 165003264 35629 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40284 35629 603 41 0 40243 0
vsize: 161136
[startup+1000.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37340 0 0 0 99932 109 0 0 25 0 1 0 482685550 165003264 35632 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40284 35632 603 41 0 40243 0
vsize: 161136
[startup+1010.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37343 0 0 0 100933 109 0 0 25 0 1 0 482685550 165003264 35635 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40284 35635 603 41 0 40243 0
vsize: 161136
[startup+1020.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37354 0 0 0 101933 109 0 0 25 0 1 0 482685550 165138432 35646 4294967295 134512640 134672761 3221224544 3221223712 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40317 35646 603 41 0 40276 0
vsize: 161268
[startup+1030.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37357 0 0 0 102933 109 0 0 25 0 1 0 482685550 165138432 35649 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40317 35649 603 41 0 40276 0
vsize: 161268
[startup+1040.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37360 0 0 0 103934 109 0 0 25 0 1 0 482685550 165138432 35652 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40317 35652 603 41 0 40276 0
vsize: 161268
[startup+1050.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37363 0 0 0 104934 109 0 0 25 0 1 0 482685550 165138432 35655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40317 35655 603 41 0 40276 0
vsize: 161268
[startup+1060.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37366 0 0 0 105934 109 0 0 25 0 1 0 482685550 165138432 35658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40317 35658 603 41 0 40276 0
vsize: 161268
[startup+1070.14 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37369 0 0 0 106935 109 0 0 25 0 1 0 482685550 165138432 35661 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40317 35661 603 41 0 40276 0
vsize: 161268
[startup+1080.15 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37370 0 0 0 107935 109 0 0 25 0 1 0 482685550 165138432 35662 4294967295 134512640 134672761 3221224544 3221223696 134561035 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40317 35662 603 41 0 40276 0
vsize: 161268
[startup+1090.15 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37421 0 0 0 108935 109 0 0 25 0 1 0 482685550 165535744 35713 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35713 603 41 0 40373 0
vsize: 161656
[startup+1100.15 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37421 0 0 0 109936 109 0 0 25 0 1 0 482685550 165535744 35713 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35713 603 41 0 40373 0
vsize: 161656
[startup+1110.15 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37422 0 0 0 110936 109 0 0 25 0 1 0 482685550 165535744 35714 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35714 603 41 0 40373 0
vsize: 161656
[startup+1120.15 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37427 0 0 0 111937 109 0 0 25 0 1 0 482685550 165535744 35719 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35719 603 41 0 40373 0
vsize: 161656
[startup+1130.15 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37428 0 0 0 112937 109 0 0 25 0 1 0 482685550 165535744 35720 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35720 603 41 0 40373 0
vsize: 161656
[startup+1140.15 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37428 0 0 0 113937 109 0 0 25 0 1 0 482685550 165535744 35720 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35720 603 41 0 40373 0
vsize: 161656
[startup+1150.15 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37428 0 0 0 114938 109 0 0 25 0 1 0 482685550 165535744 35720 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35720 603 41 0 40373 0
vsize: 161656
[startup+1160.15 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37429 0 0 0 115939 109 0 0 25 0 1 0 482685550 165535744 35721 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35721 603 41 0 40373 0
vsize: 161656
[startup+1170.16 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37431 0 0 0 116940 109 0 0 25 0 1 0 482685550 165535744 35723 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35723 603 41 0 40373 0
vsize: 161656
[startup+1180.17 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37434 0 0 0 117941 109 0 0 25 0 1 0 482685550 165535744 35726 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35726 603 41 0 40373 0
vsize: 161656
[startup+1190.18 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37438 0 0 0 118942 109 0 0 25 0 1 0 482685550 165535744 35730 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35730 603 41 0 40373 0
vsize: 161656
[startup+1200.19 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 27385
Raw data (stat): 27328 (minisat+) R 27327 29653 29652 0 -1 0 37444 0 0 0 119944 109 0 0 25 0 1 0 482685550 165535744 35736 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40414 35736 603 41 0 40373 0
vsize: 161656
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.27 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 27385
Raw data (stat): 27328 (minisat+) Z 27327 29653 29652 0 -1 12 37446 0 0 0 119944 116 0 0 25 0 1 0 482685550 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.27
CPU time (s): 1200.61
CPU user time (s): 1199.44
CPU system time (s): 1.16982
CPU usage (%): 100.029
Max. virtual memory (Kb): 161656
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####