PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-sp97ic.opb
MD5SUM	e8862b41c9b4f49ec8d11d1df0495e74
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	12497
Biggest coefficient in the objective function	1010107916
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	3093137085579
Number of bits of the sum of numbers in the objective function	42
Biggest number in a constraint	1010107916
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	3093137085579
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	12.972
Number of variables	12497
Total number of constraints	13530
Number of constraints which are clauses	41
Number of constraints which are cardinality constraints (but not clauses)	13312
Number of constraints which are nor clauses,nor cardinality constraints	177
Minimum length of a constraint	1
Maximum length of a constraint	6739
Trace number 13280

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-20 20:23:40 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=15246 boxname=wulflinc26 idbench=1173 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  e8862b41c9b4f49ec8d11d1df0495e74  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-sp97ic.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-sp97ic.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-20-10-sp97ic.opb
IDLAUNCH: 15246
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        578512 kB
Buffers:         37552 kB
Cached:         377452 kB
SwapCached:          0 kB
Active:         216484 kB
Inactive:       201428 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        578260 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6964 kB
Slab:            32460 kB
Committed_AS:    63712 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 20:43:43 (client local time) WITH STATUS 0 IN 1200.54 SECONDS
stats: 15246 7 1200.54 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1033 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .sssss.sssssssssssssssss..s.sss.s.sssss.ss.sssssssssssssssssssssssssssssss..ss.ss.sssssssss.s.ssss...sssss.s...s.ss.s.s.s.s....ss.ssss.s.ss..sssssssssssssssss...s..ssssss
c ---[1158]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1157]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1156]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1155]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1154]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[1153]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1152]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1151]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1150]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[1149]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[1147]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1146]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1145]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1144]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[1143]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1142]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1141]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1140]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1139]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1138]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1136]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1135]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[1134]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1133]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1132]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[1131]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1130]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1129]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1128]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1127]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1125]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1124]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1123]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1117]---> Adder-cost: 23092   maxlim: 39   bits: 7/6
c ---[1114]---> Adder-cost: 13882   maxlim: 29   bits: 6/5
c ---[1098]---> Adder-cost: 122   maxlim: 1   bits: 2/1
c ---[1093]---> Adder-cost: 1188   maxlim: 3   bits: 3/2
c ---[1082]---> Adder-cost: 839   maxlim: 2   bits: 3/2
c ---[1071]---> Adder-cost: 131   maxlim: 2   bits: 3/2
c ---[1067]---> Adder-cost: 162   maxlim: 4   bits: 4/3
c ---[1060]---> Adder-cost: 223   maxlim: 10   bits: 5/4
c ---[1051]---> Adder-cost: 3011   maxlim: 10   bits: 5/4
c ---[1050]---> Adder-cost: 705   maxlim: 12   bits: 5/4
c ---[1033]---> Adder-cost: 179   maxlim: 5   bits: 4/3
c ---[1011]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1010]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[1009]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1008]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[1007]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[1006]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1005]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[1004]---> Adder-cost: 5224   maxlim: 3   bits: 3/2
c ---[1003]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[1002]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[1001]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 999]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 998]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 997]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 996]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 995]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 994]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 992]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 991]---> Adder-cost: 24   maxlim: 23   bits: 5/5
c ---[ 990]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 989]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 988]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 987]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 985]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 984]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 983]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 981]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 980]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 978]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 977]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 976]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 975]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 974]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 973]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 972]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 970]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 969]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 968]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 967]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 966]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 965]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 964]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 963]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 962]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 961]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 960]---> Adder-cost: 0   maxlim: 3   bits: 3/2
c ---[ 959]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 958]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 957]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 956]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 955]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 953]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 952]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 951]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 950]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 949]---> Adder-cost: 2720   maxlim: 3   bits: 3/2
c ---[ 948]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 947]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 946]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 945]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 944]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 943]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 942]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 941]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 940]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 939]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 938]---> Adder-cost: 4648   maxlim: 2   bits: 3/2
c ---[ 937]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 936]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 935]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 934]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 933]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 932]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 931]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 930]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 929]---> Adder-cost: 24   maxlim: 23   bits: 5/5
c ---[ 928]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 926]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 925]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 924]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 923]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 922]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 921]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 920]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 919]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 918]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 917]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 915]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 914]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 913]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 912]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 911]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 910]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 909]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 908]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 907]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 906]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 905]---> Adder-cost: 1489   maxlim: 2   bits: 3/2
c ---[ 903]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 902]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 901]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 900]---> Adder-cost: 4   maxlim: 3   bits: 3/2
c ---[ 899]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 898]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 897]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 896]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 895]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 894]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 892]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 891]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 890]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 889]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 888]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 887]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 886]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 885]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 884]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 883]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 882]---> Adder-cost: 3599   maxlim: 2   bits: 3/2
c ---[ 881]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 880]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 879]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 878]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 877]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 876]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 875]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 874]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 873]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 872]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 870]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 869]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 868]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 867]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 866]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 865]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 864]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 863]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 862]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 861]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 859]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 858]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 857]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 856]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 855]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 854]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 853]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 852]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 851]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 850]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 849]---> Adder-cost: 2041   maxlim: 2   bits: 3/2
c ---[ 848]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 847]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 846]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 845]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 844]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 843]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 842]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 841]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 840]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 839]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 838]---> Adder-cost: 3598   maxlim: 2   bits: 3/2
c ---[ 837]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 836]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 835]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 834]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 833]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 832]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 831]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 830]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 829]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 828]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 827]---> Adder-cost: 6220   maxlim: 5   bits: 4/3
c ---[ 826]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 825]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 824]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 823]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 822]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 821]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 820]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 819]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 818]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 817]---> Adder-cost: 16   maxlim: 11   bits: 4/4
c ---[ 816]---> Adder-cost: 16310   maxlim: 39   bits: 7/6
c ---[ 815]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 814]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 813]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 812]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 811]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 810]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 809]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 808]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 807]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 806]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 805]---> Adder-cost: 1591   maxlim: 2   bits: 3/2
c ---[ 804]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 803]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 802]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 801]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 800]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 799]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 798]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 797]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 796]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 795]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 794]---> Adder-cost: 2307   maxlim: 2   bits: 3/2
c ---[ 793]---> Adder-cost: 849   maxlim: 2   bits: 3/2
c ---[ 792]---> Adder-cost: 38   maxlim: 21   bits: 5/5
c ---[ 791]---> Adder-cost: 16   maxlim: 21   bits: 5/5
c ---[ 790]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 789]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 788]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 787]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 786]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 785]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 784]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 783]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 782]---> Adder-cost: 2187   maxlim: 3   bits: 3/2
c ---[ 781]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 780]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 779]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 778]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 777]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 776]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 775]---> Adder-cost: 22   maxlim: 23   bits: 5/5
c ---[ 774]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 773]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 772]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 771]---> Adder-cost: 6630   maxlim: 29   bits: 6/5
c ---[ 770]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 769]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 768]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 767]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 766]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 765]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 764]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 763]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 762]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 761]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 760]---> Adder-cost: 508   maxlim: 2   bits: 3/2
c ---[ 759]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 758]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 757]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 756]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 755]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 754]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 753]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 752]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 751]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 750]---> Adder-cost: 28   maxlim: 21   bits: 5/5
c ---[ 749]---> Adder-cost: 492   maxlim: 2   bits: 3/2
c ---[ 748]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 747]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 746]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 745]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 744]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 743]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 742]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 741]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 740]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 739]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 737]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 736]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 735]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 734]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 733]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 732]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 731]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 730]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 729]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 728]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 726]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 725]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 724]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 723]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 722]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 721]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 720]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 719]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 718]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 717]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 715]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 714]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 713]---> Adder-cost: 22   maxlim: 21   bits: 5/5
c ---[ 712]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 711]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 710]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 709]---> Adder-cost: 22   maxlim: 21   bits: 5/5
c ---[ 708]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 707]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 706]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 704]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 703]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 702]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 701]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 700]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 699]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 698]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 697]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 696]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 695]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 693]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 692]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 691]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 690]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 687]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 686]---> Adder-cost: 16   maxlim: 21   bits: 5/5
c ---[ 685]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 684]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 683]---> Adder-cost: 2729   maxlim: 2   bits: 3/2
c ---[ 681]---> Adder-cost: 24   maxlim: 23   bits: 5/5
c ---[ 680]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 679]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 678]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 677]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 676]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 675]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 674]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 673]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 672]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 670]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 669]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 668]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 667]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 666]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 665]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 664]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 663]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 662]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 661]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 659]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 658]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 657]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 655]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 654]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 653]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 652]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 651]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 650]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 648]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 647]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 646]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 645]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 644]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 643]---> Adder-cost: 14   maxlim: 11   bits: 4/4
c ---[ 642]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 641]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 640]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 639]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 637]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 636]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 635]---> Adder-cost: 20   maxlim: 23   bits: 5/5
c ---[ 634]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 633]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 632]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 631]---> Adder-cost: 14   maxlim: 11   bits: 4/4
c ---[ 630]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 629]---> Adder-cost: 16   maxlim: 11   bits: 4/4
c ---[ 628]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 627]---> Adder-cost: 3392   maxlim: 2   bits: 3/2
c ---[ 626]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 625]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 624]---> Adder-cost: 14   maxlim: 11   bits: 4/4
c ---[ 623]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 622]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 621]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 620]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 619]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 618]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 617]---> Adder-cost: 14   maxlim: 11   bits: 4/4
c ---[ 616]---> Adder-cost: 406   maxlim: 2   bits: 3/2
c ---[ 615]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 614]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 613]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 612]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 611]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 610]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 609]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 608]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 607]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 606]---> Adder-cost: 30   maxlim: 21   bits: 5/5
c ---[ 604]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 603]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 602]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 601]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 600]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 599]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 598]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 597]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 596]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 595]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 593]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 592]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 591]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 590]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 589]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 587]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 586]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 585]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 584]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 582]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 581]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 580]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 579]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 578]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 577]---> Adder-cost: 32   maxlim: 17   bits: 5/5
c ---[ 576]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 575]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 574]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[ 569]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 568]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 567]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 566]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 565]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 564]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 563]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 562]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 561]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 560]---> Adder-cost: 5540   maxlim: 16   bits: 6/5
c ---[ 559]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 558]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 557]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 556]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 555]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 554]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 553]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 552]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 551]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 550]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 549]---> Adder-cost: 4893   maxlim: 14   bits: 5/4
c ---[ 548]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 546]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 545]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 544]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 543]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 542]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 541]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 540]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 539]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 538]---> Adder-cost: 5764   maxlim: 11   bits: 5/4
c ---[ 537]---> Adder-cost: 4   maxlim: 5   bits: 3/3
c ---[ 536]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 535]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 534]---> Adder-cost: 18   maxlim: 12   bits: 4/4
c ---[ 533]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 532]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 531]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 530]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 529]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 528]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 526]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 525]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 524]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 523]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 522]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 521]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 520]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 519]---> Adder-cost: 14   maxlim: 11   bits: 4/4
c ---[ 518]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 517]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 515]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 514]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 513]---> Adder-cost: 44   maxlim: 23   bits: 5/5
c ---[ 512]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 511]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 510]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 509]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 508]---> Adder-cost: 24   maxlim: 23   bits: 5/5
c ---[ 507]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 506]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 505]---> Adder-cost: 14773   maxlim: 16   bits: 6/5
c ---[ 504]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 503]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 502]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 501]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 500]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 499]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 498]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 497]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 496]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 495]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 493]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 492]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 491]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 490]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 489]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 488]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 487]---> Adder-cost: 18   maxlim: 12   bits: 4/4
c ---[ 486]---> Adder-cost: 8   maxlim: 5   bits: 3/3
c ---[ 485]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 484]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 482]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 481]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 480]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 479]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 478]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 477]---> Adder-cost: 4   maxlim: 3   bits: 3/2
c ---[ 476]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 475]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 474]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 473]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 471]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 470]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 469]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 468]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 467]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 466]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 465]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 464]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 463]---> Adder-cost: 14   maxlim: 11   bits: 4/4
c ---[ 462]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 459]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 458]---> Adder-cost: 24   maxlim: 23   bits: 5/5
c ---[ 457]---> Adder-cost: 28   maxlim: 21   bits: 5/5
c ---[ 456]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 455]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 454]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 453]---> Adder-cost: 22   maxlim: 23   bits: 5/5
c ---[ 452]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 451]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 450]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 449]---> Adder-cost: 2679   maxlim: 22   bits: 6/5
c ---[ 448]---> Adder-cost: 30   maxlim: 21   bits: 5/5
c ---[ 447]---> Adder-cost: 24   maxlim: 23   bits: 5/5
c ---[ 446]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 445]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 444]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 443]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 442]---> Adder-cost: 22   maxlim: 23   bits: 5/5
c ---[ 441]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 440]---> Adder-cost: 36   maxlim: 23   bits: 5/5
c ---[ 439]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[ 438]---> Adder-cost: 2067   maxlim: 16   bits: 6/5
c ---[ 437]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 436]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 435]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 434]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 433]---> Adder-cost: 22   maxlim: 23   bits: 5/5
c ---[ 432]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 431]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 430]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 429]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 428]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 426]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 425]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 424]---> Adder-cost: 24   maxlim: 23   bits: 5/5
c ---[ 423]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 422]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 421]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 420]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 419]---> Adder-cost: 28   maxlim: 21   bits: 5/5
c ---[ 418]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 417]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 415]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 414]---> Adder-cost: 16   maxlim: 11   bits: 4/4
c ---[ 413]---> Adder-cost: 8   maxlim: 9   bits: 4/4
c ---[ 412]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 411]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 410]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 409]---> Adder-cost: 22   maxlim: 21   bits: 5/5
c ---[ 408]---> Adder-cost: 24   maxlim: 23   bits: 5/5
c ---[ 407]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 406]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 404]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 403]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 402]---> Adder-cost: 34   maxlim: 23   bits: 5/5
c ---[ 401]---> Adder-cost: 24   maxlim: 23   bits: 5/5
c ---[ 400]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 399]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 398]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 397]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 396]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 395]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 393]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 392]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 391]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 390]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 389]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 388]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 387]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 386]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 385]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 384]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 382]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 381]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 380]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 379]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 378]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 377]---> Adder-cost: 6   maxlim: 5   bits: 3/3
c ---[ 376]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 375]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 374]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 373]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 371]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 370]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 369]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 368]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 367]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 366]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 365]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 364]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 363]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 362]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 360]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 359]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 358]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 357]---> Adder-cost: 24   maxlim: 17   bits: 5/5
c ---[ 356]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 355]---> Adder-cost: 18   maxlim: 12   bits: 4/4
c ---[ 354]---> Adder-cost: 22   maxlim: 17   bits: 5/5
c ---[ 353]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 352]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 351]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 350]---> Adder-cost: 4927   maxlim: 2   bits: 3/2
c ---[ 348]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 347]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 346]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 345]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 344]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 343]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 342]---> Adder-cost: 30   maxlim: 17   bits: 5/5
c ---[ 341]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 340]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 339]---> Adder-cost: 18   maxlim: 17   bits: 5/5
c ---[ 337]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 336]---> Adder-cost: 26   maxlim: 17   bits: 5/5
c ---[ 335]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 334]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 333]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 332]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 331]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 330]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 329]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 328]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 326]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 325]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 324]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 323]---> Adder-cost: 18   maxlim: 12   bits: 4/4
c ---[ 322]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 321]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 319]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 318]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 317]---> Adder-cost: 28   maxlim: 21   bits: 5/5
c ---[ 316]---> Adder-cost: 1934   maxlim: 19   bits: 6/5
c ---[ 314]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 313]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 312]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 311]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 310]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 309]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 308]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 307]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 306]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 305]---> Adder-cost: 5621   maxlim: 18   bits: 6/5
c ---[ 304]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 303]---> Adder-cost: 14   maxlim: 11   bits: 4/4
c ---[ 302]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 301]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 300]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 299]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 298]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 297]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 296]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 295]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 294]---> Adder-cost: 8871   maxlim: 12   bits: 5/4
c ---[ 293]---> Adder-cost: 38   maxlim: 23   bits: 5/5
c ---[ 292]---> Adder-cost: 22   maxlim: 12   bits: 4/4
c ---[ 291]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 290]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 289]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 287]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 286]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 285]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 284]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 283]---> Adder-cost: 6578   maxlim: 9   bits: 5/4
c ---[ 282]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 281]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 280]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 279]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 278]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 277]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 276]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 275]---> Adder-cost: 16   maxlim: 11   bits: 4/4
c ---[ 274]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 273]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 272]---> Adder-cost: 3008   maxlim: 11   bits: 5/4
c ---[ 271]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 270]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 269]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 268]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 267]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 266]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 265]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 264]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 263]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 262]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 261]---> Adder-cost: 4471   maxlim: 10   bits: 5/4
c ---[ 260]---> Adder-cost: 26   maxlim: 21   bits: 5/5
c ---[ 259]---> Adder-cost: 20   maxlim: 17   bits: 5/5
c ---[ 258]---> Adder-cost: 22   maxlim: 21   bits: 5/5
c ---[ 257]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 256]---> Adder-cost: 34   maxlim: 21   bits: 5/5
c ---[ 255]---> Adder-cost: 10   maxlim: 6   bits: 4/3
c ---[ 254]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 253]---> Adder-cost: 18   maxlim: 12   bits: 4/4
c ---[ 252]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 251]---> Adder-cost: 18   maxlim: 12   bits: 4/4
c ---[ 250]---> Adder-cost: 1535   maxlim: 14   bits: 5/4
c ---[ 249]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 248]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 247]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 246]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 245]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 244]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 243]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 242]---> Adder-cost: 4   maxlim: 3   bits: 3/2
c ---[ 241]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 240]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 238]---> Adder-cost: 1360   maxlim: 15   bits: 5/4
c ---[ 237]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 236]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 235]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 234]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 233]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 232]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 229]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 228]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 227]---> Adder-cost: 1001   maxlim: 9   bits: 5/4
c ---[ 226]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 225]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 224]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 223]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 222]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 221]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 220]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 219]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 218]---> Adder-cost: 24   maxlim: 19   bits: 5/5
c ---[ 217]---> Adder-cost: 28   maxlim: 17   bits: 5/5
c ---[ 216]---> Adder-cost: 7437   maxlim: 15   bits: 5/4
c ---[ 215]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[ 214]---> Adder-cost: 14   maxlim: 11   bits: 4/4
c ---[ 213]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 212]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 211]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 210]---> Adder-cost: 12   maxlim: 12   bits: 4/4
c ---[ 209]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 208]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 207]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 206]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 205]---> Adder-cost: 1071   maxlim: 12   bits: 5/4
c ---[ 204]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 203]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 202]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 201]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 200]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 199]---> Adder-cost: 6   maxlim: 3   bits: 3/2
c ---[ 198]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 197]---> Adder-cost: 28   maxlim: 19   bits: 5/5
c ---[ 196]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 195]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 193]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 192]---> Adder-cost: 14   maxlim: 11   bits: 4/4
c ---[ 191]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 190]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 189]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 188]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 187]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 186]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 185]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 184]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 182]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 181]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 180]---> Adder-cost: 32   maxlim: 23   bits: 5/5
c ---[ 179]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 178]---> Adder-cost: 18   maxlim: 12   bits: 4/4
c ---[ 177]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 176]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 175]---> Adder-cost: 16   maxlim: 12   bits: 4/4
c ---[ 174]---> Adder-cost: 8   maxlim: 4   bits: 3/3
c ---[ 173]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 171]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 170]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 169]---> Adder-cost: 20   maxlim: 19   bits: 5/5
c ---[ 168]---> Adder-cost: 14   maxlim: 11   bits: 4/4
c ---[ 167]---> Adder-cost: 18   maxlim: 11   bits: 4/4
c ---[ 166]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 165]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 164]---> Adder-cost: 12   maxlim: 9   bits: 4/4
c ---[ 163]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 162]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 160]---> Adder-cost: 28   maxlim: 21   bits: 5/5
c ---[ 159]---> Adder-cost: 22   maxlim: 21   bits: 5/5
c ---[ 158]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 157]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 156]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 155]---> Adder-cost: 16   maxlim: 11   bits: 4/4
c ---[ 154]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 153]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 152]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 151]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 149]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 148]---> Adder-cost: 14   maxlim: 6   bits: 4/3
c ---[ 147]---> Adder-cost: 30   maxlim: 23   bits: 5/5
c ---[ 146]---> Adder-cost: 14   maxlim: 12   bits: 4/4
c ---[ 145]---> Adder-cost: 16   maxlim: 9   bits: 4/4
c ---[ 144]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 143]---> Adder-cost: 36   maxlim: 19   bits: 5/5
c ---[ 142]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 141]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 140]---> Adder-cost: 20   maxlim: 11   bits: 4/4
c ---[ 138]---> Adder-cost: 6   maxlim: 2   bits: 3/2
c ---[ 137]---> Adder-cost: 12   maxlim: 6   bits: 4/3
c ---[ 136]---> Adder-cost: 26   maxlim: 23   bits: 5/5
c ---[ 135]---> Adder-cost: 20   maxlim: 12   bits: 4/4
c ---[ 134]---> Adder-cost: 24   maxlim: 21   bits: 5/5
c ---[ 133]---> Adder-cost: 16   maxlim: 21   bits: 5/5
c ---[ 132]---> Adder-cost: 22   maxlim: 19   bits: 5/5
c ---[ 131]---> Adder-cost: 26   maxlim: 19   bits: 5/5
c ---[ 130]---> Adder-cost: 28   maxlim: 23   bits: 5/5
c ---[ 129]---> Adder-cost: 32   maxlim: 19   bits: 5/5
c ---[ 128]---> Adder-cost: 581   maxlim: 4   bits: 4/3
c ---[ 127]---> Adder-cost: 5703   maxlim: 8   bits: 5/4
c ---[ 126]---> Adder-cost: 1297   maxlim: 4   bits: 4/3
c ---[ 125]---> Adder-cost: 2204   maxlim: 5   bits: 4/3
c ---[ 124]---> Adder-cost: 2847   maxlim: 7   bits: 4/3
c ---[ 123]---> Adder-cost: 2536   maxlim: 7   bits: 4/3
c ---[ 122]---> Adder-cost: 2310   maxlim: 6   bits: 4/3
c ---[ 121]---> Adder-cost: 6579   maxlim: 19   bits: 6/5
c ---[ 120]---> Adder-cost: 3943   maxlim: 18   bits: 6/5
c ---[ 119]---> Adder-cost: 1261   maxlim: 14   bits: 5/4
c ---[ 118]---> Adder-cost: 966   maxlim: 1   bits: 2/1
c ---[ 117]---> Adder-cost: 10237   maxlim: 15   bits: 5/4
c ---[ 116]---> Adder-cost: 773   maxlim: 12   bits: 5/4
c ---[ 115]---> Adder-cost: 1210   maxlim: 4   bits: 4/3
c ---[ 114]---> Adder-cost: 3724   maxlim: 9   bits: 5/4
c ---[ 113]---> Adder-cost: 1225   maxlim: 1   bits: 2/1
c ---[ 112]---> Adder-cost: 862   maxlim: 1   bits: 2/1
c ---[ 111]---> Adder-cost: 33   maxlim: 1   bits: 2/1
c ---[ 110]---> Adder-cost: 3227   maxlim: 1   bits: 2/1
c ---[ 109]---> Adder-cost: 378   maxlim: 1   bits: 2/1
c ---[ 108]---> Adder-cost: 662   maxlim: 5   bits: 4/3
c ---[ 107]---> Adder-cost: 478   maxlim: 1   bits: 2/1
c ---[ 106]---> Adder-cost: 370   maxlim: 1   bits: 2/1
c ---[ 105]---> Adder-cost: 69   maxlim: 1   bits: 2/1
c ---[ 104]---> Adder-cost: 109   maxlim: 1   bits: 2/1
c ---[ 103]---> Adder-cost: 527   maxlim: 1   bits: 2/1
c ---[ 102]---> Adder-cost: 797   maxlim: 1   bits: 2/1
c ---[ 101]---> Adder-cost: 575   maxlim: 1   bits: 2/1
c ---[ 100]---> Adder-cost: 1155   maxlim: 1   bits: 2/1
c ---[  99]---> Adder-cost: 686   maxlim: 1   bits: 2/1
c ---[  98]---> Adder-cost: 176   maxlim: 1   bits: 2/1
c ---[  97]---> Adder-cost: 141   maxlim: 1   bits: 2/1
c ---[  96]---> Adder-cost: 1682   maxlim: 1   bits: 2/1
c ---[  95]---> Adder-cost: 276   maxlim: 1   bits: 2/1
c ---[  94]---> Adder-cost: 1132   maxlim: 1   bits: 2/1
c ---[  93]---> Adder-cost: 848   maxlim: 1   bits: 2/1
c ---[  92]---> Adder-cost: 2465   maxlim: 4   bits: 4/3
c ---[  91]---> Adder-cost: 2150   maxlim: 2   bits: 3/2
c ---[  90]---> Adder-cost: 3504   maxlim: 5   bits: 4/3
c ---[  89]---> Adder-cost: 143   maxlim: 2   bits: 3/2
c ---[  88]---> Adder-cost: 7569   maxlim: 4   bits: 4/3
c ---[  87]---> Adder-cost: 949   maxlim: 2   bits: 3/2
c ---[  86]---> Adder-cost: 1505   maxlim: 2   bits: 3/2
c ---[  85]---> Adder-cost: 1458   maxlim: 5   bits: 4/3
c ---[  84]---> Adder-cost: 940   maxlim: 4   bits: 4/3
c ---[  83]---> Adder-cost: 169   maxlim: 2   bits: 3/2
c ---[  82]---> Adder-cost: 319   maxlim: 2   bits: 3/2
c ---[  81]---> Adder-cost: 482   maxlim: 2   bits: 3/2
c ---[  80]---> Adder-cost: 547   maxlim: 2   bits: 3/2
c ---[  79]---> Adder-cost: 779   maxlim: 2   bits: 3/2
c ---[  78]---> Adder-cost: 4383   maxlim: 3   bits: 3/2
c ---[  77]---> Adder-cost: 72   maxlim: 2   bits: 3/2
c ---[  76]---> Adder-cost: 2503   maxlim: 3   bits: 3/2
c ---[  75]---> Adder-cost: 2125   maxlim: 2   bits: 3/2
c ---[  74]---> Adder-cost: 2878   maxlim: 3   bits: 3/2
c ---[  73]---> Adder-cost: 737   maxlim: 5   bits: 4/3
c ---[  72]---> Adder-cost: 360   maxlim: 3   bits: 3/2
c ---[  71]---> Adder-cost: 3904   maxlim: 3   bits: 3/2
c ---[  70]---> Adder-cost: 464   maxlim: 4   bits: 4/3
c ---[  69]---> Adder-cost: 2021   maxlim: 3   bits: 3/2
c ---[  68]---> Adder-cost: 394   maxlim: 1   bits: 2/1
c ---[  67]---> Adder-cost: 1481   maxlim: 1   bits: 2/1
c ---[  66]---> Adder-cost: 686   maxlim: 1   bits: 2/1
c ---[  65]---> Adder-cost: 306   maxlim: 1   bits: 2/1
c ---[  64]---> Adder-cost: 63   maxlim: 1   bits: 2/1
c ---[  63]---> Adder-cost: 351   maxlim: 1   bits: 2/1
c ---[  62]---> Adder-cost: 290   maxlim: 1   bits: 2/1
c ---[  61]---> Adder-cost: 142   maxlim: 1   bits: 2/1
c ---[  60]---> Adder-cost: 218   maxlim: 5   bits: 4/3
c ---[  59]---> Adder-cost: 490   maxlim: 1   bits: 2/1
c ---[  58]---> Adder-cost: 4210   maxlim: 3   bits: 3/2
c ---[  57]---> Adder-cost: 765   maxlim: 3   bits: 3/2
c ---[  56]---> Adder-cost: 3587   maxlim: 3   bits: 3/2
c ---[  55]---> Adder-cost: 440   maxlim: 3   bits: 3/2
c ---[  54]---> Adder-cost: 339   maxlim: 2   bits: 3/2
c ---[  53]---> Adder-cost: 481   maxlim: 1   bits: 2/1
c ---[  52]---> Adder-cost: 43   maxlim: 1   bits: 2/1
c ---[  51]---> Adder-cost: 451   maxlim: 1   bits: 2/1
c ---[  50]---> Adder-cost: 251   maxlim: 1   bits: 2/1
c ---[  49]---> Adder-cost: 993   maxlim: 4   bits: 4/3
c ---[  48]---> Adder-cost: 251   maxlim: 5   bits: 4/3
c ---[  47]---> Adder-cost: 576   maxlim: 3   bits: 3/2
c ---[  46]---> Adder-cost: 3700   maxlim: 3   bits: 3/2
c ---[  45]---> Adder-cost: 208   maxlim: 3   bits: 3/2
c ---[  44]---> Adder-cost: 194   maxlim: 5   bits: 4/3
c ---[  43]---> Adder-cost: 191   maxlim: 1   bits: 2/1
c ---[  42]---> Adder-cost: 68   maxlim: 2   bits: 3/2
c ---[  41]---> Adder-cost: 815   maxlim: 3   bits: 3/2
c ---[  40]---> Adder-cost: 7092   maxlim: 24   bits: 6/5
c ---[  39]---> Adder-cost: 117   maxlim: 3   bits: 3/2
c ---[  38]---> Adder-cost: 715   maxlim: 1   bits: 2/1
c ---[  37]---> Adder-cost: 677   maxlim: 5   bits: 4/3
c ---[  36]---> Adder-cost: 227   maxlim: 3   bits: 3/2
c ---[  35]---> Adder-cost: 97   maxlim: 3   bits: 3/2
c ---[  34]---> Adder-cost: 116   maxlim: 3   bits: 3/2
c ---[  33]---> Adder-cost: 177   maxlim: 3   bits: 3/2
c ---[  32]---> Adder-cost: 899   maxlim: 1   bits: 2/1
c ---[  31]---> Adder-cost: 523   maxlim: 4   bits: 4/3
c ---[  30]---> Adder-cost: 870   maxlim: 1   bits: 2/1
c ---[  29]---> Adder-cost: 496   maxlim: 4   bits: 4/3
c ---[  28]---> Adder-cost: 370   maxlim: 1   bits: 2/1
c ---[  27]---> Adder-cost: 212   maxlim: 4   bits: 4/3
c ---[  26]---> Adder-cost: 1681   maxlim: 8   bits: 5/4
c ---[  25]---> Adder-cost: 25   maxlim: 1   bits: 2/1
c ---[  24]---> Adder-cost: 1157   maxlim: 1   bits: 2/1
c ---[  23]---> Adder-cost: 175   maxlim: 1   bits: 2/1
c ---[  22]---> Adder-cost: 230   maxlim: 6   bits: 4/3
c ---[  21]---> Adder-cost: 1277   maxlim: 1   bits: 2/1
c ---[  20]---> Adder-cost: 2624   maxlim: 7   bits: 4/3
c ---[  19]---> Adder-cost: 1600   maxlim: 1   bits: 2/1
c ---[  18]---> Adder-cost: 90   maxlim: 7   bits: 4/3
c ---[  17]---> Adder-cost: 4177   maxlim: 8   bits: 5/4
c ---[  16]---> Adder-cost: 201   maxlim: 1   bits: 2/1
c ---[  15]---> Adder-cost: 520   maxlim: 8   bits: 5/4
c ---[  14]---> Adder-cost: 446   maxlim: 1   bits: 2/1
c ---[  13]---> Adder-cost: 554   maxlim: 6   bits: 4/3
c ---[  12]---> Adder-cost: 664   maxlim: 1   bits: 2/1
c ---[  11]---> Adder-cost: 806   maxlim: 6   bits: 4/3
c ---[  10]---> Adder-cost: 805   maxlim: 1   bits: 2/1
c ---[   9]---> Adder-cost: 1770   maxlim: 7   bits: 4/3
c ---[   8]---> Adder-cost: 1094   maxlim: 1   bits: 2/1
c ---[   7]---> Adder-cost: 1509   maxlim: 6   bits: 4/3
c ---[   6]---> Adder-cost: 1005   maxlim: 1   bits: 2/1
c ---[   5]---> Adder-cost: 1214   maxlim: 1   bits: 2/1
c ---[   4]---> Adder-cost: 4846   maxlim: 9   bits: 5/4
c ---[   3]---> Adder-cost: 3391   maxlim: 11   bits: 5/4
c ---[   2]---> Adder-cost: 2755   maxlim: 7   bits: 4/3
c ---[   1]---> Adder-cost: 2195   maxlim: 7   bits: 4/3
c ---[   0]---> Adder-cost: 2561   maxlim: 8   bits: 5/4
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 1997853  7398594 |  665951       0        0     nan |  0.000 % |
c |       100 | 1997853  7398594 |  732546     100      379     3.8 |  1.166 % |
c |       252 | 1997798  7398407 |  805800     247      963     3.9 |  1.169 % |
c |       477 | 1997583  7397668 |  886380     455     1735     3.8 |  1.183 % |
c |       814 | 1996800  7394977 |  975018     727     2985     4.1 |  1.234 % |
c |      1320 | 1995711  7391228 | 1072520    1146     5077     4.4 |  1.300 % |
c |      2080 | 1994807  7388100 | 1179772    1834     9035     4.9 |  1.354 % |
c |      3219 | 1993185  7382476 | 1297750    2836    13776     4.9 |  1.453 % |
c |      4928 | 1991782  7377593 | 1427525    4427    23460     5.3 |  1.530 % |
c |      7492 | 1990136  7371809 | 1570277    6833    38028     5.6 |  1.606 % |
c |     11336 | 1987880  7363844 | 1727305   10444    61654     5.9 |  1.706 % |
c |     17102 | 1983606  7348797 | 1900035   15806    96936     6.1 |  1.891 % |
#### 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.08 0.02 0.01 2/54 17638
Raw data (stat): 17638 (runsolver) R 17637 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539296707 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.22 0.05 0.02 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 36293 0 0 0 909 89 0 0 25 0 1 0 539296707 160620544 34548 4294967295 134512640 134672761 3221224544 3221223844 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39214 34548 603 41 0 39173 0
vsize: 156856
[startup+20.0082 s]
Raw data (loadavg): 0.34 0.08 0.02 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 36628 0 0 0 1909 90 0 0 25 0 1 0 539296707 161837056 34883 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39511 34883 603 41 0 39470 0
vsize: 158044
[startup+30.0089 s]
Raw data (loadavg): 0.44 0.11 0.03 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 36696 0 0 0 2909 91 0 0 25 0 1 0 539296707 162107392 34951 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39577 34951 603 41 0 39536 0
vsize: 158308
[startup+40.0093 s]
Raw data (loadavg): 0.53 0.14 0.04 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 36742 0 0 0 3908 91 0 0 25 0 1 0 539296707 162451456 34997 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39661 34997 603 41 0 39620 0
vsize: 158644
[startup+50.022 s]
Raw data (loadavg): 0.60 0.17 0.05 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 36800 0 0 0 4909 92 0 0 25 0 1 0 539296707 162586624 35055 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39694 35055 603 41 0 39653 0
vsize: 158776
[startup+60.0222 s]
Raw data (loadavg): 0.66 0.19 0.06 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 36889 0 0 0 5908 93 0 0 25 0 1 0 539296707 162992128 35144 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39793 35144 603 41 0 39752 0
vsize: 159172
[startup+70.0226 s]
Raw data (loadavg): 0.71 0.22 0.07 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 36949 0 0 0 6908 93 0 0 25 0 1 0 539296707 163262464 35204 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39859 35204 603 41 0 39818 0
vsize: 159436
[startup+80.0252 s]
Raw data (loadavg): 0.76 0.24 0.08 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37008 0 0 0 7908 94 0 0 25 0 1 0 539296707 163532800 35263 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39925 35263 603 41 0 39884 0
vsize: 159700
[startup+90.0278 s]
Raw data (loadavg): 0.79 0.27 0.09 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37100 0 0 0 8908 94 0 0 25 0 1 0 539296707 163803136 35355 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39991 35355 603 41 0 39950 0
vsize: 159964
[startup+100.028 s]
Raw data (loadavg): 0.82 0.29 0.10 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37206 0 0 0 9907 95 0 0 25 0 1 0 539296707 164208640 35461 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40090 35461 603 41 0 40049 0
vsize: 160360
[startup+110.048 s]
Raw data (loadavg): 0.85 0.31 0.11 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37276 0 0 0 10909 95 0 0 25 0 1 0 539296707 164614144 35531 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40189 35531 603 41 0 40148 0
vsize: 160756
[startup+120.08 s]
Raw data (loadavg): 0.87 0.34 0.12 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37386 0 0 0 11912 96 0 0 25 0 1 0 539296707 165019648 35641 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40288 35641 603 41 0 40247 0
vsize: 161152
[startup+130.08 s]
Raw data (loadavg): 0.89 0.36 0.13 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37434 0 0 0 12912 96 0 0 25 0 1 0 539296707 165154816 35689 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40321 35689 603 41 0 40280 0
vsize: 161284
[startup+140.079 s]
Raw data (loadavg): 0.91 0.38 0.14 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37536 0 0 0 13911 97 0 0 25 0 1 0 539296707 165560320 35791 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40420 35791 603 41 0 40379 0
vsize: 161680
[startup+150.088 s]
Raw data (loadavg): 0.92 0.40 0.15 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37620 0 0 0 14911 97 0 0 25 0 1 0 539296707 165965824 35875 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40519 35875 603 41 0 40478 0
vsize: 162076
[startup+160.088 s]
Raw data (loadavg): 0.93 0.42 0.15 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37688 0 0 0 15911 98 0 0 25 0 1 0 539296707 166236160 35943 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40585 35943 603 41 0 40544 0
vsize: 162340
[startup+170.096 s]
Raw data (loadavg): 0.94 0.44 0.16 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37770 0 0 0 16911 99 0 0 25 0 1 0 539296707 166641664 36025 4294967295 134512640 134672761 3221224544 3221223724 134556674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40684 36025 603 41 0 40643 0
vsize: 162736
[startup+180.097 s]
Raw data (loadavg): 0.95 0.45 0.17 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37819 0 0 0 17911 99 0 0 25 0 1 0 539296707 166776832 36074 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40717 36074 603 41 0 40676 0
vsize: 162868
[startup+190.102 s]
Raw data (loadavg): 0.96 0.47 0.18 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37924 0 0 0 18911 99 0 0 25 0 1 0 539296707 167182336 36179 4294967295 134512640 134672761 3221224544 3221223696 134565058 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40816 36179 603 41 0 40775 0
vsize: 163264
[startup+200.107 s]
Raw data (loadavg): 0.96 0.49 0.19 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 37991 0 0 0 19911 100 0 0 25 0 1 0 539296707 167452672 36246 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40882 36246 603 41 0 40841 0
vsize: 163528
[startup+210.107 s]
Raw data (loadavg): 0.97 0.51 0.20 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38047 0 0 0 20911 100 0 0 25 0 1 0 539296707 167723008 36302 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40948 36302 603 41 0 40907 0
vsize: 163792
[startup+220.107 s]
Raw data (loadavg): 0.97 0.52 0.20 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38118 0 0 0 21910 101 0 0 25 0 1 0 539296707 167993344 36373 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41014 36373 603 41 0 40973 0
vsize: 164056
[startup+230.107 s]
Raw data (loadavg): 0.98 0.54 0.21 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38189 0 0 0 22910 102 0 0 25 0 1 0 539296707 168263680 36444 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41080 36444 603 41 0 41039 0
vsize: 164320
[startup+240.107 s]
Raw data (loadavg): 0.98 0.55 0.22 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38243 0 0 0 23909 103 0 0 25 0 1 0 539296707 168534016 36498 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41146 36498 603 41 0 41105 0
vsize: 164584
[startup+250.107 s]
Raw data (loadavg): 0.98 0.57 0.23 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38305 0 0 0 24909 103 0 0 25 0 1 0 539296707 168804352 36560 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41212 36560 603 41 0 41171 0
vsize: 164848
[startup+260.107 s]
Raw data (loadavg): 0.98 0.58 0.24 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38323 0 0 0 25909 103 0 0 25 0 1 0 539296707 168804352 36578 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41212 36578 603 41 0 41171 0
vsize: 164848
[startup+270.108 s]
Raw data (loadavg): 0.99 0.59 0.24 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38371 0 0 0 26908 104 0 0 25 0 1 0 539296707 169074688 36626 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41278 36626 603 41 0 41237 0
vsize: 165112
[startup+280.108 s]
Raw data (loadavg): 0.99 0.61 0.25 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38403 0 0 0 27908 104 0 0 25 0 1 0 539296707 169209856 36658 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41311 36658 603 41 0 41270 0
vsize: 165244
[startup+290.108 s]
Raw data (loadavg): 0.99 0.62 0.26 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38447 0 0 0 28907 105 0 0 25 0 1 0 539296707 169345024 36702 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41344 36702 603 41 0 41303 0
vsize: 165376
[startup+300.109 s]
Raw data (loadavg): 0.99 0.63 0.27 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38489 0 0 0 29907 106 0 0 25 0 1 0 539296707 169480192 36744 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41377 36744 603 41 0 41336 0
vsize: 165508
[startup+310.109 s]
Raw data (loadavg): 0.99 0.64 0.28 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38532 0 0 0 30906 106 0 0 25 0 1 0 539296707 169750528 36787 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41443 36787 603 41 0 41402 0
vsize: 165772
[startup+320.11 s]
Raw data (loadavg): 0.99 0.65 0.28 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38572 0 0 0 31906 106 0 0 25 0 1 0 539296707 169885696 36827 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41476 36827 603 41 0 41435 0
vsize: 165904
[startup+330.111 s]
Raw data (loadavg): 0.99 0.66 0.29 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38614 0 0 0 32906 107 0 0 25 0 1 0 539296707 170020864 36869 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41509 36869 603 41 0 41468 0
vsize: 166036
[startup+340.11 s]
Raw data (loadavg): 0.99 0.67 0.30 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38644 0 0 0 33905 107 0 0 25 0 1 0 539296707 170156032 36899 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41542 36899 603 41 0 41501 0
vsize: 166168
[startup+350.111 s]
Raw data (loadavg): 0.99 0.68 0.30 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38682 0 0 0 34904 108 0 0 25 0 1 0 539296707 170291200 36937 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41575 36937 603 41 0 41534 0
vsize: 166300
[startup+360.111 s]
Raw data (loadavg): 0.99 0.69 0.31 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38704 0 0 0 35904 109 0 0 25 0 1 0 539296707 170291200 36959 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41575 36959 603 41 0 41534 0
vsize: 166300
[startup+370.111 s]
Raw data (loadavg): 0.99 0.70 0.32 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38732 0 0 0 36903 110 0 0 25 0 1 0 539296707 170426368 36987 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41608 36987 603 41 0 41567 0
vsize: 166432
[startup+380.111 s]
Raw data (loadavg): 0.99 0.71 0.32 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38781 0 0 0 37903 110 0 0 25 0 1 0 539296707 170696704 37036 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41674 37036 603 41 0 41633 0
vsize: 166696
[startup+390.111 s]
Raw data (loadavg): 0.99 0.72 0.33 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38816 0 0 0 38903 111 0 0 25 0 1 0 539296707 170835968 37071 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41708 37071 603 41 0 41667 0
vsize: 166832
[startup+400.112 s]
Raw data (loadavg): 0.99 0.73 0.34 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38838 0 0 0 39902 111 0 0 25 0 1 0 539296707 170835968 37093 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41708 37093 603 41 0 41667 0
vsize: 166832
[startup+410.112 s]
Raw data (loadavg): 0.99 0.74 0.34 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38872 0 0 0 40902 111 0 0 25 0 1 0 539296707 170971136 37127 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41741 37127 603 41 0 41700 0
vsize: 166964
[startup+420.113 s]
Raw data (loadavg): 0.99 0.75 0.35 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38878 0 0 0 41902 112 0 0 25 0 1 0 539296707 170971136 37133 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41741 37133 603 41 0 41700 0
vsize: 166964
[startup+430.114 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38902 0 0 0 42902 113 0 0 25 0 1 0 539296707 171106304 37157 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41774 37157 603 41 0 41733 0
vsize: 167096
[startup+440.113 s]
Raw data (loadavg): 0.99 0.76 0.36 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38917 0 0 0 43901 113 0 0 25 0 1 0 539296707 171106304 37172 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41774 37172 603 41 0 41733 0
vsize: 167096
[startup+450.113 s]
Raw data (loadavg): 0.99 0.77 0.37 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38933 0 0 0 44901 114 0 0 25 0 1 0 539296707 171241472 37188 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41807 37188 603 41 0 41766 0
vsize: 167228
[startup+460.113 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38950 0 0 0 45900 114 0 0 25 0 1 0 539296707 171241472 37205 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41807 37205 603 41 0 41766 0
vsize: 167228
[startup+470.114 s]
Raw data (loadavg): 0.99 0.78 0.38 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38956 0 0 0 46900 115 0 0 25 0 1 0 539296707 171376640 37211 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41840 37211 603 41 0 41799 0
vsize: 167360
[startup+480.114 s]
Raw data (loadavg): 0.99 0.79 0.39 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38962 0 0 0 47900 115 0 0 25 0 1 0 539296707 171376640 37217 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41840 37217 603 41 0 41799 0
vsize: 167360
[startup+490.115 s]
Raw data (loadavg): 0.99 0.80 0.39 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38979 0 0 0 48900 115 0 0 25 0 1 0 539296707 171376640 37234 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41840 37234 603 41 0 41799 0
vsize: 167360
[startup+500.116 s]
Raw data (loadavg): 0.99 0.80 0.40 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 38991 0 0 0 49900 115 0 0 25 0 1 0 539296707 171376640 37246 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41840 37246 603 41 0 41799 0
vsize: 167360
[startup+510.115 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39000 0 0 0 50899 116 0 0 25 0 1 0 539296707 171511808 37255 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41873 37255 603 41 0 41832 0
vsize: 167492
[startup+520.116 s]
Raw data (loadavg): 0.99 0.81 0.41 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39010 0 0 0 51899 116 0 0 25 0 1 0 539296707 171511808 37265 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41873 37265 603 41 0 41832 0
vsize: 167492
[startup+530.117 s]
Raw data (loadavg): 0.99 0.82 0.42 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39021 0 0 0 52898 117 0 0 25 0 1 0 539296707 171511808 37276 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41873 37276 603 41 0 41832 0
vsize: 167492
[startup+540.118 s]
Raw data (loadavg): 0.99 0.83 0.42 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39028 0 0 0 53898 117 0 0 25 0 1 0 539296707 171646976 37283 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41906 37283 603 41 0 41865 0
vsize: 167624
[startup+550.118 s]
Raw data (loadavg): 0.99 0.83 0.43 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39038 0 0 0 54898 117 0 0 25 0 1 0 539296707 171646976 37293 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41906 37293 603 41 0 41865 0
vsize: 167624
[startup+560.12 s]
Raw data (loadavg): 0.99 0.84 0.43 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39044 0 0 0 55898 118 0 0 25 0 1 0 539296707 171646976 37299 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41906 37299 603 41 0 41865 0
vsize: 167624
[startup+570.121 s]
Raw data (loadavg): 0.99 0.84 0.44 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39060 0 0 0 56898 118 0 0 25 0 1 0 539296707 171646976 37315 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41906 37315 603 41 0 41865 0
vsize: 167624
[startup+580.123 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39067 0 0 0 57898 118 0 0 25 0 1 0 539296707 171782144 37322 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41939 37322 603 41 0 41898 0
vsize: 167756
[startup+590.124 s]
Raw data (loadavg): 0.99 0.85 0.45 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39079 0 0 0 58898 119 0 0 25 0 1 0 539296707 171782144 37334 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41939 37334 603 41 0 41898 0
vsize: 167756
[startup+600.153 s]
Raw data (loadavg): 0.99 0.85 0.46 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39089 0 0 0 59900 120 0 0 25 0 1 0 539296707 171782144 37344 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41939 37344 603 41 0 41898 0
vsize: 167756
[startup+610.163 s]
Raw data (loadavg): 0.99 0.86 0.46 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39103 0 0 0 60900 120 0 0 25 0 1 0 539296707 171782144 37358 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41939 37358 603 41 0 41898 0
vsize: 167756
[startup+620.165 s]
Raw data (loadavg): 0.99 0.86 0.47 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39114 0 0 0 61900 121 0 0 25 0 1 0 539296707 171917312 37369 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41972 37369 603 41 0 41931 0
vsize: 167888
[startup+630.165 s]
Raw data (loadavg): 0.99 0.87 0.47 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39116 0 0 0 62900 121 0 0 25 0 1 0 539296707 171917312 37371 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41972 37371 603 41 0 41931 0
vsize: 167888
[startup+640.166 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39133 0 0 0 63899 122 0 0 25 0 1 0 539296707 171917312 37388 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41972 37388 603 41 0 41931 0
vsize: 167888
[startup+650.167 s]
Raw data (loadavg): 0.99 0.87 0.48 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39145 0 0 0 64899 122 0 0 25 0 1 0 539296707 172072960 37400 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37400 603 41 0 41969 0
vsize: 168040
[startup+660.182 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39145 0 0 0 65901 122 0 0 25 0 1 0 539296707 172072960 37400 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37400 603 41 0 41969 0
vsize: 168040
[startup+670.183 s]
Raw data (loadavg): 0.99 0.88 0.49 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39150 0 0 0 66900 123 0 0 25 0 1 0 539296707 172072960 37405 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37405 603 41 0 41969 0
vsize: 168040
[startup+680.184 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39160 0 0 0 67900 123 0 0 25 0 1 0 539296707 172072960 37415 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37415 603 41 0 41969 0
vsize: 168040
[startup+690.183 s]
Raw data (loadavg): 0.99 0.89 0.50 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39166 0 0 0 68900 123 0 0 25 0 1 0 539296707 172072960 37421 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37421 603 41 0 41969 0
vsize: 168040
[startup+700.184 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39169 0 0 0 69899 124 0 0 25 0 1 0 539296707 172072960 37424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37424 603 41 0 41969 0
vsize: 168040
[startup+710.185 s]
Raw data (loadavg): 0.99 0.89 0.51 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39176 0 0 0 70899 124 0 0 25 0 1 0 539296707 172072960 37431 4294967295 134512640 134672761 3221224544 3221223728 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37431 603 41 0 41969 0
vsize: 168040
[startup+720.197 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39188 0 0 0 71900 125 0 0 25 0 1 0 539296707 172208128 37443 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37443 603 41 0 42002 0
vsize: 168172
[startup+730.202 s]
Raw data (loadavg): 0.99 0.90 0.52 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39192 0 0 0 72900 125 0 0 25 0 1 0 539296707 172208128 37447 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37447 603 41 0 42002 0
vsize: 168172
[startup+740.202 s]
Raw data (loadavg): 0.99 0.90 0.53 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39196 0 0 0 73900 125 0 0 25 0 1 0 539296707 172208128 37451 4294967295 134512640 134672761 3221224544 3221223712 134564698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37451 603 41 0 42002 0
vsize: 168172
[startup+750.204 s]
Raw data (loadavg): 0.99 0.91 0.53 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39198 0 0 0 74900 126 0 0 25 0 1 0 539296707 172208128 37453 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37453 603 41 0 42002 0
vsize: 168172
[startup+760.204 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39205 0 0 0 75900 126 0 0 25 0 1 0 539296707 172208128 37460 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37460 603 41 0 42002 0
vsize: 168172
[startup+770.205 s]
Raw data (loadavg): 0.99 0.91 0.54 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39210 0 0 0 76899 127 0 0 25 0 1 0 539296707 172208128 37465 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37465 603 41 0 42002 0
vsize: 168172
[startup+780.206 s]
Raw data (loadavg): 0.99 0.91 0.55 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39215 0 0 0 77898 127 0 0 25 0 1 0 539296707 172208128 37470 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37470 603 41 0 42002 0
vsize: 168172
[startup+790.209 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39217 0 0 0 78898 128 0 0 25 0 1 0 539296707 172208128 37472 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37472 603 41 0 42002 0
vsize: 168172
[startup+800.216 s]
Raw data (loadavg): 0.99 0.92 0.55 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39229 0 0 0 79898 129 0 0 25 0 1 0 539296707 172343296 37484 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37484 603 41 0 42035 0
vsize: 168304
[startup+810.216 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39235 0 0 0 80898 129 0 0 25 0 1 0 539296707 172343296 37490 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37490 603 41 0 42035 0
vsize: 168304
[startup+820.221 s]
Raw data (loadavg): 0.99 0.92 0.56 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39239 0 0 0 81898 129 0 0 25 0 1 0 539296707 172343296 37494 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37494 603 41 0 42035 0
vsize: 168304
[startup+830.221 s]
Raw data (loadavg): 0.99 0.92 0.57 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39242 0 0 0 82898 130 0 0 25 0 1 0 539296707 172343296 37497 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37497 603 41 0 42035 0
vsize: 168304
[startup+840.23 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39245 0 0 0 83899 130 0 0 25 0 1 0 539296707 172343296 37500 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37500 603 41 0 42035 0
vsize: 168304
[startup+850.232 s]
Raw data (loadavg): 0.99 0.93 0.57 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39254 0 0 0 84898 130 0 0 25 0 1 0 539296707 172343296 37509 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37509 603 41 0 42035 0
vsize: 168304
[startup+860.239 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39258 0 0 0 85899 131 0 0 25 0 1 0 539296707 172343296 37513 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37513 603 41 0 42035 0
vsize: 168304
[startup+870.243 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39261 0 0 0 86899 131 0 0 25 0 1 0 539296707 172343296 37516 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37516 603 41 0 42035 0
vsize: 168304
[startup+880.246 s]
Raw data (loadavg): 0.99 0.93 0.58 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39268 0 0 0 87899 131 0 0 25 0 1 0 539296707 172478464 37523 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42109 37523 603 41 0 42068 0
vsize: 168436
[startup+890.249 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39271 0 0 0 88899 132 0 0 25 0 1 0 539296707 172478464 37526 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42109 37526 603 41 0 42068 0
vsize: 168436
[startup+900.25 s]
Raw data (loadavg): 0.99 0.94 0.59 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39280 0 0 0 89899 132 0 0 25 0 1 0 539296707 172478464 37535 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42109 37535 603 41 0 42068 0
vsize: 168436
[startup+910.25 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39298 0 0 0 90898 133 0 0 25 0 1 0 539296707 172478464 37553 4294967295 134512640 134672761 3221224544 3221223716 134556658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42109 37553 603 41 0 42068 0
vsize: 168436
[startup+920.257 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39306 0 0 0 91899 133 0 0 25 0 1 0 539296707 172478464 37561 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42109 37561 603 41 0 42068 0
vsize: 168436
[startup+930.264 s]
Raw data (loadavg): 0.99 0.94 0.60 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39308 0 0 0 92899 133 0 0 25 0 1 0 539296707 172478464 37563 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42109 37563 603 41 0 42068 0
vsize: 168436
[startup+940.265 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39312 0 0 0 93899 133 0 0 25 0 1 0 539296707 172613632 37567 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42142 37567 603 41 0 42101 0
vsize: 168568
[startup+950.266 s]
Raw data (loadavg): 0.99 0.94 0.61 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39315 0 0 0 94899 134 0 0 25 0 1 0 539296707 172613632 37570 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37570 603 41 0 42101 0
vsize: 168568
[startup+960.27 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39318 0 0 0 95900 134 0 0 25 0 1 0 539296707 172613632 37573 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37573 603 41 0 42101 0
vsize: 168568
[startup+970.284 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39319 0 0 0 96901 134 0 0 25 0 1 0 539296707 172613632 37574 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37574 603 41 0 42101 0
vsize: 168568
[startup+980.284 s]
Raw data (loadavg): 0.99 0.95 0.62 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39321 0 0 0 97901 134 0 0 25 0 1 0 539296707 172613632 37576 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37576 603 41 0 42101 0
vsize: 168568
[startup+990.284 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39324 0 0 0 98902 134 0 0 25 0 1 0 539296707 172613632 37579 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37579 603 41 0 42101 0
vsize: 168568
[startup+1000.28 s]
Raw data (loadavg): 0.99 0.95 0.63 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39327 0 0 0 99902 134 0 0 25 0 1 0 539296707 172613632 37582 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37582 603 41 0 42101 0
vsize: 168568
[startup+1010.28 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39332 0 0 0 100902 134 0 0 25 0 1 0 539296707 172613632 37587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37587 603 41 0 42101 0
vsize: 168568
[startup+1020.28 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39336 0 0 0 101902 134 0 0 25 0 1 0 539296707 172613632 37591 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37591 603 41 0 42101 0
vsize: 168568
[startup+1030.28 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39340 0 0 0 102902 134 0 0 25 0 1 0 539296707 172613632 37595 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37595 603 41 0 42101 0
vsize: 168568
[startup+1040.28 s]
Raw data (loadavg): 0.99 0.95 0.64 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39346 0 0 0 103902 134 0 0 25 0 1 0 539296707 172613632 37601 4294967295 134512640 134672761 3221224544 3221223760 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37601 603 41 0 42101 0
vsize: 168568
[startup+1050.28 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39349 0 0 0 104903 134 0 0 25 0 1 0 539296707 172748800 37604 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37604 603 41 0 42134 0
vsize: 168700
[startup+1060.29 s]
Raw data (loadavg): 0.99 0.95 0.65 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39350 0 0 0 105904 134 0 0 25 0 1 0 539296707 172748800 37605 4294967295 134512640 134672761 3221224544 3221223716 134556669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37605 603 41 0 42134 0
vsize: 168700
[startup+1070.3 s]
Raw data (loadavg): 0.99 0.96 0.65 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39352 0 0 0 106904 134 0 0 25 0 1 0 539296707 172748800 37607 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37607 603 41 0 42134 0
vsize: 168700
[startup+1080.3 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39363 0 0 0 107904 134 0 0 25 0 1 0 539296707 172748800 37618 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37618 603 41 0 42134 0
vsize: 168700
[startup+1090.3 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39368 0 0 0 108904 134 0 0 25 0 1 0 539296707 172748800 37623 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37623 603 41 0 42134 0
vsize: 168700
[startup+1100.3 s]
Raw data (loadavg): 0.99 0.96 0.66 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39373 0 0 0 109905 134 0 0 25 0 1 0 539296707 172748800 37628 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37628 603 41 0 42134 0
vsize: 168700
[startup+1110.3 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39375 0 0 0 110904 134 0 0 25 0 1 0 539296707 172748800 37630 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37630 603 41 0 42134 0
vsize: 168700
[startup+1120.3 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39377 0 0 0 111904 134 0 0 25 0 1 0 539296707 172748800 37632 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37632 603 41 0 42134 0
vsize: 168700
[startup+1130.31 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39380 0 0 0 112905 135 0 0 25 0 1 0 539296707 172748800 37635 4294967295 134512640 134672761 3221224544 3221223736 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37635 603 41 0 42134 0
vsize: 168700
[startup+1140.32 s]
Raw data (loadavg): 0.99 0.96 0.67 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39387 0 0 0 113906 135 0 0 25 0 1 0 539296707 172748800 37642 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37642 603 41 0 42134 0
vsize: 168700
[startup+1150.32 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39405 0 0 0 114906 135 0 0 25 0 1 0 539296707 173002752 37660 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42237 37660 603 41 0 42196 0
vsize: 168948
[startup+1160.32 s]
Raw data (loadavg): 0.99 0.96 0.68 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39406 0 0 0 115906 135 0 0 25 0 1 0 539296707 173002752 37661 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42237 37661 603 41 0 42196 0
vsize: 168948
[startup+1170.32 s]
Raw data (loadavg): 0.99 0.97 0.68 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39408 0 0 0 116906 135 0 0 25 0 1 0 539296707 173002752 37663 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42237 37663 603 41 0 42196 0
vsize: 168948
[startup+1180.32 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39408 0 0 0 117906 135 0 0 25 0 1 0 539296707 173002752 37663 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42237 37663 603 41 0 42196 0
vsize: 168948
[startup+1190.32 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39408 0 0 0 118907 135 0 0 25 0 1 0 539296707 173002752 37663 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42237 37663 603 41 0 42196 0
vsize: 168948
[startup+1200.35 s]
Raw data (loadavg): 0.99 0.97 0.69 2/54 17638
Raw data (stat): 17638 (minisat+) R 17637 22612 22611 0 -1 0 39408 0 0 0 119910 135 0 0 25 0 1 0 539296707 173002752 37663 4294967295 134512640 134672761 3221224544 3221223732 134556588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42237 37663 603 41 0 42196 0
vsize: 168948
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.43 s]
Raw data (loadavg): 0.99 0.97 0.69 1/54 17638
Raw data (stat): 17638 (minisat+) Z 17637 22612 22611 0 -1 12 39410 0 0 0 119910 143 0 0 25 0 1 0 539296707 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.42
CPU time (s): 1200.54
CPU user time (s): 1199.1
CPU system time (s): 1.43178
CPU usage (%): 100.009
Max. virtual memory (Kb): 168948
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####