PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/plato.asu.edu/pub/unibo/normalized-mps-v2-13-7-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	11.8052
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 13863

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        291104 kB
Buffers:         17648 kB
Cached:         701928 kB
SwapCached:          0 kB
Active:         118764 kB
Inactive:       603676 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        290852 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            15320 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-20 22:25:58 (client local time) WITH STATUS 0 IN 1200.49 SECONDS
stats: 20251 7 1200.49 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.86 0.97 0.93 2/55 29886
Raw data (stat): 29886 (runsolver) R 29885 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 417168913 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0002 s]
Raw data (loadavg): 0.88 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 36252 0 0 0 916 82 0 0 25 0 1 0 417168913 160452608 34507 4294967295 134512640 134672761 3221224544 3221222184 134543021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39173 34507 603 41 0 39132 0
vsize: 156692
[startup+20.0017 s]
Raw data (loadavg): 0.90 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 36628 0 0 0 1916 83 0 0 25 0 1 0 417168913 161837056 34883 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.0014 s]
Raw data (loadavg): 0.92 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 36696 0 0 0 2916 83 0 0 25 0 1 0 417168913 162107392 34951 4294967295 134512640 134672761 3221224544 3221223716 134556632 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.0071 s]
Raw data (loadavg): 0.93 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 36742 0 0 0 3916 83 0 0 25 0 1 0 417168913 162451456 34997 4294967295 134512640 134672761 3221224544 3221223728 134556675 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.0088 s]
Raw data (loadavg): 0.94 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 36799 0 0 0 4916 84 0 0 25 0 1 0 417168913 162586624 35054 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39694 35054 603 41 0 39653 0
vsize: 158776
[startup+60.0089 s]
Raw data (loadavg): 0.95 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 36889 0 0 0 5916 84 0 0 25 0 1 0 417168913 162992128 35144 4294967295 134512640 134672761 3221224544 3221223716 134556685 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.0082 s]
Raw data (loadavg): 0.96 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 36949 0 0 0 6916 84 0 0 25 0 1 0 417168913 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.0244 s]
Raw data (loadavg): 0.96 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37008 0 0 0 7917 85 0 0 25 0 1 0 417168913 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.0246 s]
Raw data (loadavg): 0.97 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37100 0 0 0 8917 85 0 0 25 0 1 0 417168913 163803136 35355 4294967295 134512640 134672761 3221224544 3221223712 134560869 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.025 s]
Raw data (loadavg): 0.97 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37206 0 0 0 9917 85 0 0 25 0 1 0 417168913 164208640 35461 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40090 35461 603 41 0 40049 0
vsize: 160360
[startup+110.025 s]
Raw data (loadavg): 0.98 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37271 0 0 0 10917 85 0 0 25 0 1 0 417168913 164478976 35526 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40156 35526 603 41 0 40115 0
vsize: 160624
[startup+120.041 s]
Raw data (loadavg): 0.98 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37384 0 0 0 11919 85 0 0 25 0 1 0 417168913 165019648 35639 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40288 35639 603 41 0 40247 0
vsize: 161152
[startup+130.04 s]
Raw data (loadavg): 0.98 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37426 0 0 0 12919 85 0 0 25 0 1 0 417168913 165154816 35681 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40321 35681 603 41 0 40280 0
vsize: 161284
[startup+140.04 s]
Raw data (loadavg): 0.98 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37536 0 0 0 13918 86 0 0 25 0 1 0 417168913 165560320 35791 4294967295 134512640 134672761 3221224544 3221223716 134556646 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.041 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37619 0 0 0 14918 86 0 0 25 0 1 0 417168913 165965824 35874 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40519 35874 603 41 0 40478 0
vsize: 162076
[startup+160.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37686 0 0 0 15918 87 0 0 25 0 1 0 417168913 166236160 35941 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40585 35941 603 41 0 40544 0
vsize: 162340
[startup+170.04 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37769 0 0 0 16918 87 0 0 25 0 1 0 417168913 166641664 36024 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40684 36024 603 41 0 40643 0
vsize: 162736
[startup+180.112 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37816 0 0 0 17925 87 0 0 25 0 1 0 417168913 166776832 36071 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40717 36071 603 41 0 40676 0
vsize: 162868
[startup+190.217 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37917 0 0 0 18936 87 0 0 25 0 1 0 417168913 167182336 36172 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40816 36172 603 41 0 40775 0
vsize: 163264
[startup+200.218 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 37982 0 0 0 19936 87 0 0 25 0 1 0 417168913 167452672 36237 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40882 36237 603 41 0 40841 0
vsize: 163528
[startup+210.219 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38036 0 0 0 20935 88 0 0 25 0 1 0 417168913 167723008 36291 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40948 36291 603 41 0 40907 0
vsize: 163792
[startup+220.228 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38107 0 0 0 21936 88 0 0 25 0 1 0 417168913 167993344 36362 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41014 36362 603 41 0 40973 0
vsize: 164056
[startup+230.228 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38182 0 0 0 22936 88 0 0 25 0 1 0 417168913 168263680 36437 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41080 36437 603 41 0 41039 0
vsize: 164320
[startup+240.229 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38243 0 0 0 23935 89 0 0 25 0 1 0 417168913 168534016 36498 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.229 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38303 0 0 0 24935 89 0 0 25 0 1 0 417168913 168804352 36558 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41212 36558 603 41 0 41171 0
vsize: 164848
[startup+260.229 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38321 0 0 0 25935 89 0 0 25 0 1 0 417168913 168804352 36576 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41212 36576 603 41 0 41171 0
vsize: 164848
[startup+270.229 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38371 0 0 0 26935 89 0 0 25 0 1 0 417168913 169074688 36626 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.228 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38403 0 0 0 27935 89 0 0 25 0 1 0 417168913 169209856 36658 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.229 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38433 0 0 0 28935 89 0 0 25 0 1 0 417168913 169345024 36688 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41344 36688 603 41 0 41303 0
vsize: 165376
[startup+300.23 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38487 0 0 0 29935 90 0 0 25 0 1 0 417168913 169480192 36742 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41377 36742 603 41 0 41336 0
vsize: 165508
[startup+310.23 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38526 0 0 0 30935 90 0 0 25 0 1 0 417168913 169615360 36781 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41410 36781 603 41 0 41369 0
vsize: 165640
[startup+320.236 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38571 0 0 0 31935 91 0 0 25 0 1 0 417168913 169885696 36826 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41476 36826 603 41 0 41435 0
vsize: 165904
[startup+330.237 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38610 0 0 0 32935 91 0 0 25 0 1 0 417168913 170020864 36865 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41509 36865 603 41 0 41468 0
vsize: 166036
[startup+340.236 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38633 0 0 0 33935 92 0 0 25 0 1 0 417168913 170020864 36888 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41509 36888 603 41 0 41468 0
vsize: 166036
[startup+350.237 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38681 0 0 0 34934 92 0 0 25 0 1 0 417168913 170291200 36936 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41575 36936 603 41 0 41534 0
vsize: 166300
[startup+360.241 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38700 0 0 0 35934 92 0 0 25 0 1 0 417168913 170291200 36955 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41575 36955 603 41 0 41534 0
vsize: 166300
[startup+370.24 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38727 0 0 0 36934 93 0 0 25 0 1 0 417168913 170426368 36982 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41608 36982 603 41 0 41567 0
vsize: 166432
[startup+380.241 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38775 0 0 0 37934 93 0 0 25 0 1 0 417168913 170561536 37030 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41641 37030 603 41 0 41600 0
vsize: 166564
[startup+390.241 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38802 0 0 0 38934 93 0 0 25 0 1 0 417168913 170696704 37057 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41674 37057 603 41 0 41633 0
vsize: 166696
[startup+400.241 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38832 0 0 0 39934 93 0 0 25 0 1 0 417168913 170835968 37087 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41708 37087 603 41 0 41667 0
vsize: 166832
[startup+410.241 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38860 0 0 0 40934 93 0 0 25 0 1 0 417168913 170971136 37115 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41741 37115 603 41 0 41700 0
vsize: 166964
[startup+420.241 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38876 0 0 0 41934 94 0 0 25 0 1 0 417168913 170971136 37131 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41741 37131 603 41 0 41700 0
vsize: 166964
[startup+430.242 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38901 0 0 0 42934 94 0 0 25 0 1 0 417168913 171106304 37156 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41774 37156 603 41 0 41733 0
vsize: 167096
[startup+440.242 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38916 0 0 0 43934 94 0 0 25 0 1 0 417168913 171106304 37171 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41774 37171 603 41 0 41733 0
vsize: 167096
[startup+450.242 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38932 0 0 0 44933 95 0 0 25 0 1 0 417168913 171241472 37187 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41807 37187 603 41 0 41766 0
vsize: 167228
[startup+460.243 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38946 0 0 0 45933 95 0 0 25 0 1 0 417168913 171241472 37201 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41807 37201 603 41 0 41766 0
vsize: 167228
[startup+470.242 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38955 0 0 0 46933 95 0 0 25 0 1 0 417168913 171376640 37210 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41840 37210 603 41 0 41799 0
vsize: 167360
[startup+480.242 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38961 0 0 0 47934 95 0 0 25 0 1 0 417168913 171376640 37216 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41840 37216 603 41 0 41799 0
vsize: 167360
[startup+490.242 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38977 0 0 0 48933 95 0 0 25 0 1 0 417168913 171376640 37232 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41840 37232 603 41 0 41799 0
vsize: 167360
[startup+500.243 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38988 0 0 0 49933 95 0 0 25 0 1 0 417168913 171376640 37243 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41840 37243 603 41 0 41799 0
vsize: 167360
[startup+510.242 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 38999 0 0 0 50934 95 0 0 25 0 1 0 417168913 171511808 37254 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41873 37254 603 41 0 41832 0
vsize: 167492
[startup+520.241 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39008 0 0 0 51934 95 0 0 25 0 1 0 417168913 171511808 37263 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41873 37263 603 41 0 41832 0
vsize: 167492
[startup+530.242 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39019 0 0 0 52934 95 0 0 25 0 1 0 417168913 171511808 37274 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41873 37274 603 41 0 41832 0
vsize: 167492
[startup+540.242 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39025 0 0 0 53934 95 0 0 25 0 1 0 417168913 171646976 37280 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41906 37280 603 41 0 41865 0
vsize: 167624
[startup+550.242 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39034 0 0 0 54934 95 0 0 25 0 1 0 417168913 171646976 37289 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41906 37289 603 41 0 41865 0
vsize: 167624
[startup+560.248 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39043 0 0 0 55935 95 0 0 25 0 1 0 417168913 171646976 37298 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41906 37298 603 41 0 41865 0
vsize: 167624
[startup+570.248 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39057 0 0 0 56935 95 0 0 25 0 1 0 417168913 171646976 37312 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41906 37312 603 41 0 41865 0
vsize: 167624
[startup+580.248 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39063 0 0 0 57935 95 0 0 25 0 1 0 417168913 171646976 37318 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41906 37318 603 41 0 41865 0
vsize: 167624
[startup+590.247 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39072 0 0 0 58935 95 0 0 25 0 1 0 417168913 171782144 37327 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41939 37327 603 41 0 41898 0
vsize: 167756
[startup+600.249 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39084 0 0 0 59935 95 0 0 25 0 1 0 417168913 171782144 37339 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41939 37339 603 41 0 41898 0
vsize: 167756
[startup+610.249 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39099 0 0 0 60935 96 0 0 25 0 1 0 417168913 171782144 37354 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41939 37354 603 41 0 41898 0
vsize: 167756
[startup+620.249 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39113 0 0 0 61935 96 0 0 25 0 1 0 417168913 171917312 37368 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41972 37368 603 41 0 41931 0
vsize: 167888
[startup+630.249 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39115 0 0 0 62936 96 0 0 25 0 1 0 417168913 171917312 37370 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41972 37370 603 41 0 41931 0
vsize: 167888
[startup+640.249 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39130 0 0 0 63935 96 0 0 25 0 1 0 417168913 171917312 37385 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41972 37385 603 41 0 41931 0
vsize: 167888
[startup+650.249 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39144 0 0 0 64936 96 0 0 25 0 1 0 417168913 172072960 37399 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37399 603 41 0 41969 0
vsize: 168040
[startup+660.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39145 0 0 0 65936 96 0 0 25 0 1 0 417168913 172072960 37400 4294967295 134512640 134672761 3221224544 3221223744 134557911 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.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39147 0 0 0 66936 96 0 0 25 0 1 0 417168913 172072960 37402 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37402 603 41 0 41969 0
vsize: 168040
[startup+680.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39152 0 0 0 67936 96 0 0 25 0 1 0 417168913 172072960 37407 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37407 603 41 0 41969 0
vsize: 168040
[startup+690.249 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39165 0 0 0 68935 97 0 0 25 0 1 0 417168913 172072960 37420 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37420 603 41 0 41969 0
vsize: 168040
[startup+700.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39168 0 0 0 69935 97 0 0 25 0 1 0 417168913 172072960 37423 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37423 603 41 0 41969 0
vsize: 168040
[startup+710.249 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39173 0 0 0 70935 97 0 0 25 0 1 0 417168913 172072960 37428 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37428 603 41 0 41969 0
vsize: 168040
[startup+720.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39185 0 0 0 71935 97 0 0 25 0 1 0 417168913 172072960 37440 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42010 37440 603 41 0 41969 0
vsize: 168040
[startup+730.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39191 0 0 0 72935 97 0 0 25 0 1 0 417168913 172208128 37446 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37446 603 41 0 42002 0
vsize: 168172
[startup+740.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39195 0 0 0 73935 97 0 0 25 0 1 0 417168913 172208128 37450 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37450 603 41 0 42002 0
vsize: 168172
[startup+750.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39198 0 0 0 74936 97 0 0 25 0 1 0 417168913 172208128 37453 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39202 0 0 0 75935 97 0 0 25 0 1 0 417168913 172208128 37457 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37457 603 41 0 42002 0
vsize: 168172
[startup+770.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39208 0 0 0 76936 97 0 0 25 0 1 0 417168913 172208128 37463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37463 603 41 0 42002 0
vsize: 168172
[startup+780.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39213 0 0 0 77935 98 0 0 25 0 1 0 417168913 172208128 37468 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37468 603 41 0 42002 0
vsize: 168172
[startup+790.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39217 0 0 0 78935 98 0 0 25 0 1 0 417168913 172208128 37472 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.251 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39219 0 0 0 79935 98 0 0 25 0 1 0 417168913 172208128 37474 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42043 37474 603 41 0 42002 0
vsize: 168172
[startup+810.251 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39233 0 0 0 80935 98 0 0 25 0 1 0 417168913 172343296 37488 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37488 603 41 0 42035 0
vsize: 168304
[startup+820.251 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39238 0 0 0 81935 99 0 0 25 0 1 0 417168913 172343296 37493 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37493 603 41 0 42035 0
vsize: 168304
[startup+830.251 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39241 0 0 0 82935 99 0 0 25 0 1 0 417168913 172343296 37496 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37496 603 41 0 42035 0
vsize: 168304
[startup+840.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39243 0 0 0 83935 99 0 0 25 0 1 0 417168913 172343296 37498 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42076 37498 603 41 0 42035 0
vsize: 168304
[startup+850.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39252 0 0 0 84935 99 0 0 25 0 1 0 417168913 172343296 37507 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42076 37507 603 41 0 42035 0
vsize: 168304
[startup+860.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39256 0 0 0 85935 99 0 0 25 0 1 0 417168913 172343296 37511 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42076 37511 603 41 0 42035 0
vsize: 168304
[startup+870.251 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39260 0 0 0 86936 99 0 0 25 0 1 0 417168913 172343296 37515 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42076 37515 603 41 0 42035 0
vsize: 168304
[startup+880.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39263 0 0 0 87936 99 0 0 25 0 1 0 417168913 172343296 37518 4294967295 134512640 134672761 3221224544 3221223680 134560579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42076 37518 603 41 0 42035 0
vsize: 168304
[startup+890.251 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39270 0 0 0 88936 99 0 0 25 0 1 0 417168913 172478464 37525 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42109 37525 603 41 0 42068 0
vsize: 168436
[startup+900.251 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39275 0 0 0 89936 99 0 0 25 0 1 0 417168913 172478464 37530 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42109 37530 603 41 0 42068 0
vsize: 168436
[startup+910.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39282 0 0 0 90936 99 0 0 25 0 1 0 417168913 172478464 37537 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42109 37537 603 41 0 42068 0
vsize: 168436
[startup+920.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39303 0 0 0 91936 99 0 0 25 0 1 0 417168913 172478464 37558 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42109 37558 603 41 0 42068 0
vsize: 168436
[startup+930.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39308 0 0 0 92937 99 0 0 25 0 1 0 417168913 172478464 37563 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42109 37563 603 41 0 42068 0
vsize: 168436
[startup+940.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39310 0 0 0 93937 99 0 0 25 0 1 0 417168913 172478464 37565 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42109 37565 603 41 0 42068 0
vsize: 168436
[startup+950.253 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39312 0 0 0 94937 99 0 0 25 0 1 0 417168913 172613632 37567 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37567 603 41 0 42101 0
vsize: 168568
[startup+960.253 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39317 0 0 0 95937 99 0 0 25 0 1 0 417168913 172613632 37572 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37572 603 41 0 42101 0
vsize: 168568
[startup+970.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39319 0 0 0 96937 99 0 0 25 0 1 0 417168913 172613632 37574 4294967295 134512640 134672761 3221224544 3221223712 134560898 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.253 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39320 0 0 0 97938 99 0 0 25 0 1 0 417168913 172613632 37575 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37575 603 41 0 42101 0
vsize: 168568
[startup+990.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39322 0 0 0 98938 99 0 0 25 0 1 0 417168913 172613632 37577 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37577 603 41 0 42101 0
vsize: 168568
[startup+1000.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39325 0 0 0 99938 99 0 0 25 0 1 0 417168913 172613632 37580 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37580 603 41 0 42101 0
vsize: 168568
[startup+1010.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39328 0 0 0 100938 99 0 0 25 0 1 0 417168913 172613632 37583 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37583 603 41 0 42101 0
vsize: 168568
[startup+1020.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39333 0 0 0 101938 99 0 0 25 0 1 0 417168913 172613632 37588 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37588 603 41 0 42101 0
vsize: 168568
[startup+1030.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39338 0 0 0 102938 99 0 0 25 0 1 0 417168913 172613632 37593 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37593 603 41 0 42101 0
vsize: 168568
[startup+1040.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39341 0 0 0 103939 99 0 0 25 0 1 0 417168913 172613632 37596 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37596 603 41 0 42101 0
vsize: 168568
[startup+1050.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39347 0 0 0 104939 99 0 0 25 0 1 0 417168913 172613632 37602 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42142 37602 603 41 0 42101 0
vsize: 168568
[startup+1060.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39349 0 0 0 105939 99 0 0 25 0 1 0 417168913 172748800 37604 4294967295 134512640 134672761 3221224544 3221223740 134556678 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37604 603 41 0 42134 0
vsize: 168700
[startup+1070.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39351 0 0 0 106939 99 0 0 25 0 1 0 417168913 172748800 37606 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37606 603 41 0 42134 0
vsize: 168700
[startup+1080.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39354 0 0 0 107939 99 0 0 25 0 1 0 417168913 172748800 37609 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37609 603 41 0 42134 0
vsize: 168700
[startup+1090.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39367 0 0 0 108939 99 0 0 25 0 1 0 417168913 172748800 37622 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37622 603 41 0 42134 0
vsize: 168700
[startup+1100.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39372 0 0 0 109940 99 0 0 25 0 1 0 417168913 172748800 37627 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42175 37627 603 41 0 42134 0
vsize: 168700
[startup+1110.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39373 0 0 0 110940 99 0 0 25 0 1 0 417168913 172748800 37628 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42175 37628 603 41 0 42134 0
vsize: 168700
[startup+1120.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39375 0 0 0 111940 99 0 0 25 0 1 0 417168913 172748800 37630 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42175 37630 603 41 0 42134 0
vsize: 168700
[startup+1130.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39377 0 0 0 112940 100 0 0 25 0 1 0 417168913 172748800 37632 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42175 37632 603 41 0 42134 0
vsize: 168700
[startup+1140.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39384 0 0 0 113940 100 0 0 25 0 1 0 417168913 172748800 37639 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42175 37639 603 41 0 42134 0
vsize: 168700
[startup+1150.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39405 0 0 0 114940 100 0 0 25 0 1 0 417168913 173002752 37660 4294967295 134512640 134672761 3221224544 3221223716 134556627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42237 37660 603 41 0 42196 0
vsize: 168948
[startup+1160.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39405 0 0 0 115940 100 0 0 25 0 1 0 417168913 173002752 37660 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42237 37660 603 41 0 42196 0
vsize: 168948
[startup+1170.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39407 0 0 0 116940 100 0 0 25 0 1 0 417168913 173002752 37662 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42237 37662 603 41 0 42196 0
vsize: 168948
[startup+1180.25 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39408 0 0 0 117939 101 0 0 25 0 1 0 417168913 173002752 37663 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42237 37663 603 41 0 42196 0
vsize: 168948
[startup+1190.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39408 0 0 0 118940 101 0 0 25 0 1 0 417168913 173002752 37663 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42237 37663 603 41 0 42196 0
vsize: 168948
[startup+1200.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/55 29886
Raw data (stat): 29886 (minisat+) R 29885 30927 30926 0 -1 0 39408 0 0 0 119940 101 0 0 25 0 1 0 417168913 173002752 37663 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42237 37663 603 41 0 42196 0
vsize: 168948
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.33 s]
Raw data (loadavg): 0.99 0.97 0.93 1/55 29886
Raw data (stat): 29886 (minisat+) Z 29885 30927 30926 0 -1 12 39410 0 0 0 119940 108 0 0 25 0 1 0 417168913 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.33
CPU time (s): 1200.49
CPU user time (s): 1199.4
CPU system time (s): 1.08383
CPU usage (%): 100.013
Max. virtual memory (Kb): 168948
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####