PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-t1717.opb
MD5SUM	bc46e72682d969c09e6f4028df473a45
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	201342
Optimality of the best value was proved	NO
Number of terms in the objective function	73885
Biggest coefficient in the objective function	4066
Number of bits for the biggest coefficient in the objective function	12
Sum of the numbers in the objective function	172074995
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	4066
Number of bits of the biggest number in a constraint	12
Biggest sum of numbers in a constraint	172074995
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.18
Number of variables	73885
Total number of constraints	74436
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	74436
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	1
Maximum length of a constraint	612
Trace number 21507

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        615704 kB
Buffers:         26748 kB
Cached:         370100 kB
SwapCached:          0 kB
Active:         176136 kB
Inactive:       223556 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        615452 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13600 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:27:40 (client local time) WITH STATUS 0 IN 1200.58 SECONDS
stats: 13075 7 1200.58 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1102 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[1100]---> Adder-cost: 1170   maxlim: 590   bits: 10/10
c ---[1098]---> Adder-cost: 1178   maxlim: 591   bits: 10/10
c ---[1096]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[1094]---> Adder-cost: 958   maxlim: 586   bits: 10/10
c ---[1092]---> Adder-cost: 1178   maxlim: 593   bits: 10/10
c ---[1090]---> Adder-cost: 1162   maxlim: 584   bits: 10/10
c ---[1088]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[1086]---> Adder-cost: 1178   maxlim: 591   bits: 10/10
c ---[1084]---> Adder-cost: 1170   maxlim: 589   bits: 10/10
c ---[1082]---> Adder-cost: 1168   maxlim: 588   bits: 10/10
c ---[1080]---> Adder-cost: 1178   maxlim: 592   bits: 10/10
c ---[1078]---> Adder-cost: 1170   maxlim: 590   bits: 10/10
c ---[1076]---> Adder-cost: 1170   maxlim: 589   bits: 10/10
c ---[1074]---> Adder-cost: 1164   maxlim: 586   bits: 10/10
c ---[1072]---> Adder-cost: 1162   maxlim: 584   bits: 10/10
c ---[1070]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[1068]---> Adder-cost: 1162   maxlim: 584   bits: 10/10
c ---[1066]---> Adder-cost: 1184   maxlim: 595   bits: 10/10
c ---[1064]---> Adder-cost: 1162   maxlim: 584   bits: 10/10
c ---[1062]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[1060]---> Adder-cost: 1170   maxlim: 590   bits: 10/10
c ---[1058]---> Adder-cost: 1168   maxlim: 587   bits: 10/10
c ---[1056]---> Adder-cost: 1210   maxlim: 608   bits: 10/10
c ---[1054]---> Adder-cost: 1160   maxlim: 584   bits: 10/10
c ---[1052]---> Adder-cost: 1166   maxlim: 590   bits: 10/10
c ---[1050]---> Adder-cost: 1168   maxlim: 587   bits: 10/10
c ---[1048]---> Adder-cost: 1178   maxlim: 591   bits: 10/10
c ---[1046]---> Adder-cost: 1184   maxlim: 596   bits: 10/10
c ---[1044]---> Adder-cost: 1168   maxlim: 588   bits: 10/10
c ---[1042]---> Adder-cost: 1168   maxlim: 587   bits: 10/10
c ---[1040]---> Adder-cost: 1164   maxlim: 586   bits: 10/10
c ---[1038]---> Adder-cost: 1170   maxlim: 589   bits: 10/10
c ---[1036]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[1034]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[1032]---> Adder-cost: 1180   maxlim: 594   bits: 10/10
c ---[1030]---> Adder-cost: 1176   maxlim: 594   bits: 10/10
c ---[1028]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[1026]---> Adder-cost: 1166   maxlim: 588   bits: 10/10
c ---[1024]---> Adder-cost: 1170   maxlim: 590   bits: 10/10
c ---[1022]---> Adder-cost: 1170   maxlim: 589   bits: 10/10
c ---[1020]---> Adder-cost: 1160   maxlim: 586   bits: 10/10
c ---[1018]---> Adder-cost: 1170   maxlim: 589   bits: 10/10
c ---[1016]---> Adder-cost: 1168   maxlim: 594   bits: 10/10
c ---[1014]---> Adder-cost: 1170   maxlim: 590   bits: 10/10
c ---[1012]---> Adder-cost: 1180   maxlim: 594   bits: 10/10
c ---[1010]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[1008]---> Adder-cost: 1178   maxlim: 592   bits: 10/10
c ---[1006]---> Adder-cost: 1180   maxlim: 593   bits: 10/10
c ---[1004]---> Adder-cost: 1168   maxlim: 588   bits: 10/10
c ---[1002]---> Adder-cost: 1168   maxlim: 590   bits: 10/10
c ---[1000]---> Adder-cost: 1178   maxlim: 591   bits: 10/10
c ---[ 998]---> Adder-cost: 1128   maxlim: 589   bits: 10/10
c ---[ 996]---> Adder-cost: 1194   maxlim: 602   bits: 10/10
c ---[ 994]---> Adder-cost: 1138   maxlim: 596   bits: 10/10
c ---[ 992]---> Adder-cost: 1174   maxlim: 596   bits: 10/10
c ---[ 990]---> Adder-cost: 1150   maxlim: 588   bits: 10/10
c ---[ 988]---> Adder-cost: 1162   maxlim: 589   bits: 10/10
c ---[ 986]---> Adder-cost: 1138   maxlim: 596   bits: 10/10
c ---[ 984]---> Adder-cost: 1126   maxlim: 586   bits: 10/10
c ---[ 982]---> Adder-cost: 1166   maxlim: 594   bits: 10/10
c ---[ 980]---> Adder-cost: 508   maxlim: 584   bits: 10/10
c ---[ 978]---> Adder-cost: 1156   maxlim: 588   bits: 10/10
c ---[ 976]---> Adder-cost: 1106   maxlim: 587   bits: 10/10
c ---[ 974]---> Adder-cost: 1134   maxlim: 593   bits: 10/10
c ---[ 972]---> Adder-cost: 1154   maxlim: 589   bits: 10/10
c ---[ 970]---> Adder-cost: 1150   maxlim: 594   bits: 10/10
c ---[ 968]---> Adder-cost: 1150   maxlim: 588   bits: 10/10
c ---[ 966]---> Adder-cost: 974   maxlim: 587   bits: 10/10
c ---[ 964]---> Adder-cost: 1144   maxlim: 587   bits: 10/10
c ---[ 962]---> Adder-cost: 1168   maxlim: 588   bits: 10/10
c ---[ 960]---> Adder-cost: 1172   maxlim: 598   bits: 10/10
c ---[ 958]---> Adder-cost: 1112   maxlim: 587   bits: 10/10
c ---[ 956]---> Adder-cost: 1190   maxlim: 600   bits: 10/10
c ---[ 954]---> Adder-cost: 1166   maxlim: 589   bits: 10/10
c ---[ 952]---> Adder-cost: 832   maxlim: 592   bits: 10/10
c ---[ 950]---> Adder-cost: 1170   maxlim: 597   bits: 10/10
c ---[ 948]---> Adder-cost: 1130   maxlim: 593   bits: 10/10
c ---[ 946]---> Adder-cost: 1168   maxlim: 587   bits: 10/10
c ---[ 944]---> Adder-cost: 1182   maxlim: 596   bits: 10/10
c ---[ 942]---> Adder-cost: 1162   maxlim: 591   bits: 10/10
c ---[ 940]---> Adder-cost: 1136   maxlim: 597   bits: 10/10
c ---[ 938]---> Adder-cost: 682   maxlim: 589   bits: 10/10
c ---[ 936]---> Adder-cost: 1156   maxlim: 587   bits: 10/10
c ---[ 934]---> Adder-cost: 1160   maxlim: 587   bits: 10/10
c ---[ 932]---> Adder-cost: 1204   maxlim: 608   bits: 10/10
c ---[ 930]---> Adder-cost: 1160   maxlim: 589   bits: 10/10
c ---[ 928]---> Adder-cost: 1134   maxlim: 591   bits: 10/10
c ---[ 926]---> Adder-cost: 1136   maxlim: 588   bits: 10/10
c ---[ 924]---> Adder-cost: 1176   maxlim: 591   bits: 10/10
c ---[ 922]---> Adder-cost: 1158   maxlim: 590   bits: 10/10
c ---[ 920]---> Adder-cost: 984   maxlim: 589   bits: 10/10
c ---[ 918]---> Adder-cost: 1074   maxlim: 589   bits: 10/10
c ---[ 916]---> Adder-cost: 1148   maxlim: 595   bits: 10/10
c ---[ 914]---> Adder-cost: 1098   maxlim: 594   bits: 10/10
c ---[ 912]---> Adder-cost: 1098   maxlim: 597   bits: 10/10
c ---[ 910]---> Adder-cost: 1086   maxlim: 600   bits: 10/10
c ---[ 908]---> Adder-cost: 784   maxlim: 587   bits: 10/10
c ---[ 906]---> Adder-cost: 1180   maxlim: 595   bits: 10/10
c ---[ 904]---> Adder-cost: 1142   maxlim: 590   bits: 10/10
c ---[ 902]---> Adder-cost: 1106   maxlim: 589   bits: 10/10
c ---[ 900]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[ 898]---> Adder-cost: 1068   maxlim: 587   bits: 10/10
c ---[ 896]---> Adder-cost: 1094   maxlim: 592   bits: 10/10
c ---[ 894]---> Adder-cost: 1164   maxlim: 591   bits: 10/10
c ---[ 892]---> Adder-cost: 1142   maxlim: 597   bits: 10/10
c ---[ 890]---> Adder-cost: 1172   maxlim: 592   bits: 10/10
c ---[ 888]---> Adder-cost: 1142   maxlim: 587   bits: 10/10
c ---[ 886]---> Adder-cost: 810   maxlim: 596   bits: 10/10
c ---[ 884]---> Adder-cost: 1168   maxlim: 589   bits: 10/10
c ---[ 882]---> Adder-cost: 1152   maxlim: 590   bits: 10/10
c ---[ 880]---> Adder-cost: 1134   maxlim: 592   bits: 10/10
c ---[ 878]---> Adder-cost: 1162   maxlim: 588   bits: 10/10
c ---[ 876]---> Adder-cost: 1160   maxlim: 585   bits: 10/10
c ---[ 874]---> Adder-cost: 494   maxlim: 587   bits: 10/10
c ---[ 872]---> Adder-cost: 1116   maxlim: 595   bits: 10/10
c ---[ 870]---> Adder-cost: 1142   maxlim: 599   bits: 10/10
c ---[ 868]---> Adder-cost: 1160   maxlim: 586   bits: 10/10
c ---[ 866]---> Adder-cost: 1148   maxlim: 587   bits: 10/10
c ---[ 864]---> Adder-cost: 1112   maxlim: 587   bits: 10/10
c ---[ 862]---> Adder-cost: 1046   maxlim: 587   bits: 10/10
c ---[ 860]---> Adder-cost: 1158   maxlim: 587   bits: 10/10
c ---[ 858]---> Adder-cost: 958   maxlim: 602   bits: 10/10
c ---[ 856]---> Adder-cost: 1168   maxlim: 588   bits: 10/10
c ---[ 854]---> Adder-cost: 1166   maxlim: 587   bits: 10/10
c ---[ 852]---> Adder-cost: 1138   maxlim: 589   bits: 10/10
c ---[ 850]---> Adder-cost: 942   maxlim: 590   bits: 10/10
c ---[ 848]---> Adder-cost: 1158   maxlim: 590   bits: 10/10
c ---[ 846]---> Adder-cost: 1168   maxlim: 588   bits: 10/10
c ---[ 844]---> Adder-cost: 1108   maxlim: 587   bits: 10/10
c ---[ 842]---> Adder-cost: 1116   maxlim: 588   bits: 10/10
c ---[ 840]---> Adder-cost: 1170   maxlim: 595   bits: 10/10
c ---[ 838]---> Adder-cost: 1160   maxlim: 586   bits: 10/10
c ---[ 836]---> Adder-cost: 1112   maxlim: 589   bits: 10/10
c ---[ 834]---> Adder-cost: 1112   maxlim: 590   bits: 10/10
c ---[ 832]---> Adder-cost: 1154   maxlim: 587   bits: 10/10
c ---[ 830]---> Adder-cost: 1154   maxlim: 588   bits: 10/10
c ---[ 828]---> Adder-cost: 1144   maxlim: 590   bits: 10/10
c ---[ 826]---> Adder-cost: 870   maxlim: 586   bits: 10/10
c ---[ 824]---> Adder-cost: 1064   maxlim: 587   bits: 10/10
c ---[ 822]---> Adder-cost: 1164   maxlim: 588   bits: 10/10
c ---[ 820]---> Adder-cost: 1150   maxlim: 586   bits: 10/10
c ---[ 818]---> Adder-cost: 1192   maxlim: 602   bits: 10/10
c ---[ 816]---> Adder-cost: 976   maxlim: 588   bits: 10/10
c ---[ 814]---> Adder-cost: 1084   maxlim: 592   bits: 10/10
c ---[ 812]---> Adder-cost: 1134   maxlim: 587   bits: 10/10
c ---[ 810]---> Adder-cost: 778   maxlim: 587   bits: 10/10
c ---[ 808]---> Adder-cost: 1150   maxlim: 595   bits: 10/10
c ---[ 806]---> Adder-cost: 1150   maxlim: 598   bits: 10/10
c ---[ 804]---> Adder-cost: 1146   maxlim: 588   bits: 10/10
c ---[ 802]---> Adder-cost: 1166   maxlim: 589   bits: 10/10
c ---[ 800]---> Adder-cost: 1148   maxlim: 587   bits: 10/10
c ---[ 798]---> Adder-cost: 1128   maxlim: 587   bits: 10/10
c ---[ 796]---> Adder-cost: 1150   maxlim: 586   bits: 10/10
c ---[ 794]---> Adder-cost: 1138   maxlim: 586   bits: 10/10
c ---[ 792]---> Adder-cost: 1146   maxlim: 584   bits: 10/10
c ---[ 790]---> Adder-cost: 1158   maxlim: 590   bits: 10/10
c ---[ 788]---> Adder-cost: 1136   maxlim: 590   bits: 10/10
c ---[ 786]---> Adder-cost: 1164   maxlim: 591   bits: 10/10
c ---[ 784]---> Adder-cost: 1128   maxlim: 593   bits: 10/10
c ---[ 782]---> Adder-cost: 1158   maxlim: 588   bits: 10/10
c ---[ 780]---> Adder-cost: 1156   maxlim: 589   bits: 10/10
c ---[ 778]---> Adder-cost: 1176   maxlim: 591   bits: 10/10
c ---[ 776]---> Adder-cost: 1150   maxlim: 588   bits: 10/10
c ---[ 774]---> Adder-cost: 1094   maxlim: 586   bits: 10/10
c ---[ 772]---> Adder-cost: 1082   maxlim: 590   bits: 10/10
c ---[ 770]---> Adder-cost: 1028   maxlim: 588   bits: 10/10
c ---[ 768]---> Adder-cost: 1184   maxlim: 595   bits: 10/10
c ---[ 766]---> Adder-cost: 1096   maxlim: 588   bits: 10/10
c ---[ 764]---> Adder-cost: 820   maxlim: 586   bits: 10/10
c ---[ 762]---> Adder-cost: 1150   maxlim: 586   bits: 10/10
c ---[ 760]---> Adder-cost: 1090   maxlim: 589   bits: 10/10
c ---[ 758]---> Adder-cost: 1078   maxlim: 585   bits: 10/10
c ---[ 756]---> Adder-cost: 672   maxlim: 595   bits: 10/10
c ---[ 754]---> Adder-cost: 994   maxlim: 595   bits: 10/10
c ---[ 752]---> Adder-cost: 1190   maxlim: 600   bits: 10/10
c ---[ 750]---> Adder-cost: 1144   maxlim: 596   bits: 10/10
c ---[ 748]---> Adder-cost: 1172   maxlim: 600   bits: 10/10
c ---[ 746]---> Adder-cost: 1136   maxlim: 593   bits: 10/10
c ---[ 744]---> Adder-cost: 1134   maxlim: 586   bits: 10/10
c ---[ 742]---> Adder-cost: 1176   maxlim: 596   bits: 10/10
c ---[ 740]---> Adder-cost: 1162   maxlim: 590   bits: 10/10
c ---[ 738]---> Adder-cost: 1158   maxlim: 585   bits: 10/10
c ---[ 736]---> Adder-cost: 1164   maxlim: 589   bits: 10/10
c ---[ 734]---> Adder-cost: 1112   maxlim: 592   bits: 10/10
c ---[ 732]---> Adder-cost: 1088   maxlim: 587   bits: 10/10
c ---[ 730]---> Adder-cost: 1152   maxlim: 587   bits: 10/10
c ---[ 728]---> Adder-cost: 1018   maxlim: 596   bits: 10/10
c ---[ 726]---> Adder-cost: 1166   maxlim: 597   bits: 10/10
c ---[ 724]---> Adder-cost: 1118   maxlim: 593   bits: 10/10
c ---[ 722]---> Adder-cost: 1092   maxlim: 593   bits: 10/10
c ---[ 720]---> Adder-cost: 1120   maxlim: 588   bits: 10/10
c ---[ 718]---> Adder-cost: 1058   maxlim: 590   bits: 10/10
c ---[ 716]---> Adder-cost: 1102   maxlim: 587   bits: 10/10
c ---[ 714]---> Adder-cost: 1178   maxlim: 593   bits: 10/10
c ---[ 712]---> Adder-cost: 1138   maxlim: 587   bits: 10/10
c ---[ 710]---> Adder-cost: 1114   maxlim: 591   bits: 10/10
c ---[ 708]---> Adder-cost: 1166   maxlim: 591   bits: 10/10
c ---[ 706]---> Adder-cost: 1082   maxlim: 593   bits: 10/10
c ---[ 704]---> Adder-cost: 1046   maxlim: 597   bits: 10/10
c ---[ 702]---> Adder-cost: 1138   maxlim: 589   bits: 10/10
c ---[ 700]---> Adder-cost: 1096   maxlim: 592   bits: 10/10
c ---[ 698]---> Adder-cost: 1146   maxlim: 587   bits: 10/10
c ---[ 696]---> Adder-cost: 1152   maxlim: 588   bits: 10/10
c ---[ 694]---> Adder-cost: 1162   maxlim: 596   bits: 10/10
c ---[ 692]---> Adder-cost: 1166   maxlim: 588   bits: 10/10
c ---[ 690]---> Adder-cost: 1170   maxlim: 589   bits: 10/10
c ---[ 688]---> Adder-cost: 1094   maxlim: 596   bits: 10/10
c ---[ 686]---> Adder-cost: 1160   maxlim: 588   bits: 10/10
c ---[ 684]---> Adder-cost: 1072   maxlim: 588   bits: 10/10
c ---[ 682]---> Adder-cost: 1132   maxlim: 599   bits: 10/10
c ---[ 680]---> Adder-cost: 1154   maxlim: 591   bits: 10/10
c ---[ 678]---> Adder-cost: 1054   maxlim: 589   bits: 10/10
c ---[ 676]---> Adder-cost: 1158   maxlim: 587   bits: 10/10
c ---[ 674]---> Adder-cost: 1060   maxlim: 594   bits: 10/10
c ---[ 672]---> Adder-cost: 1148   maxlim: 596   bits: 10/10
c ---[ 670]---> Adder-cost: 1138   maxlim: 592   bits: 10/10
c ---[ 668]---> Adder-cost: 1046   maxlim: 591   bits: 10/10
c ---[ 666]---> Adder-cost: 1158   maxlim: 589   bits: 10/10
c ---[ 664]---> Adder-cost: 1024   maxlim: 588   bits: 10/10
c ---[ 662]---> Adder-cost: 1158   maxlim: 588   bits: 10/10
c ---[ 660]---> Adder-cost: 1158   maxlim: 587   bits: 10/10
c ---[ 658]---> Adder-cost: 1156   maxlim: 587   bits: 10/10
c ---[ 656]---> Adder-cost: 896   maxlim: 585   bits: 10/10
c ---[ 654]---> Adder-cost: 1162   maxlim: 584   bits: 10/10
c ---[ 652]---> Adder-cost: 1158   maxlim: 587   bits: 10/10
c ---[ 650]---> Adder-cost: 1040   maxlim: 595   bits: 10/10
c ---[ 648]---> Adder-cost: 1082   maxlim: 590   bits: 10/10
c ---[ 646]---> Adder-cost: 1170   maxlim: 589   bits: 10/10
c ---[ 644]---> Adder-cost: 1160   maxlim: 593   bits: 10/10
c ---[ 642]---> Adder-cost: 1030   maxlim: 597   bits: 10/10
c ---[ 640]---> Adder-cost: 1162   maxlim: 589   bits: 10/10
c ---[ 638]---> Adder-cost: 770   maxlim: 590   bits: 10/10
c ---[ 636]---> Adder-cost: 944   maxlim: 588   bits: 10/10
c ---[ 634]---> Adder-cost: 1164   maxlim: 586   bits: 10/10
c ---[ 632]---> Adder-cost: 1126   maxlim: 588   bits: 10/10
c ---[ 630]---> Adder-cost: 662   maxlim: 586   bits: 10/10
c ---[ 628]---> Adder-cost: 1162   maxlim: 585   bits: 10/10
c ---[ 626]---> Adder-cost: 1112   maxlim: 591   bits: 10/10
c ---[ 624]---> Adder-cost: 1160   maxlim: 584   bits: 10/10
c ---[ 622]---> Adder-cost: 1156   maxlim: 594   bits: 10/10
c ---[ 620]---> Adder-cost: 1098   maxlim: 590   bits: 10/10
c ---[ 618]---> Adder-cost: 1148   maxlim: 589   bits: 10/10
c ---[ 616]---> Adder-cost: 736   maxlim: 585   bits: 10/10
c ---[ 614]---> Adder-cost: 1060   maxlim: 592   bits: 10/10
c ---[ 612]---> Adder-cost: 1118   maxlim: 585   bits: 10/10
c ---[ 610]---> Adder-cost: 1106   maxlim: 588   bits: 10/10
c ---[ 608]---> Adder-cost: 1012   maxlim: 588   bits: 10/10
c ---[ 606]---> Adder-cost: 1142   maxlim: 588   bits: 10/10
c ---[ 604]---> Adder-cost: 1156   maxlim: 587   bits: 10/10
c ---[ 602]---> Adder-cost: 1122   maxlim: 590   bits: 10/10
c ---[ 600]---> Adder-cost: 1022   maxlim: 597   bits: 10/10
c ---[ 598]---> Adder-cost: 818   maxlim: 595   bits: 10/10
c ---[ 596]---> Adder-cost: 390   maxlim: 590   bits: 10/10
c ---[ 594]---> Adder-cost: 920   maxlim: 589   bits: 10/10
c ---[ 592]---> Adder-cost: 1158   maxlim: 588   bits: 10/10
c ---[ 590]---> Adder-cost: 1168   maxlim: 588   bits: 10/10
c ---[ 588]---> Adder-cost: 1164   maxlim: 588   bits: 10/10
c ---[ 586]---> Adder-cost: 1144   maxlim: 596   bits: 10/10
c ---[ 584]---> Adder-cost: 1098   maxlim: 590   bits: 10/10
c ---[ 582]---> Adder-cost: 838   maxlim: 588   bits: 10/10
c ---[ 580]---> Adder-cost: 1116   maxlim: 589   bits: 10/10
c ---[ 578]---> Adder-cost: 1092   maxlim: 592   bits: 10/10
c ---[ 576]---> Adder-cost: 864   maxlim: 597   bits: 10/10
c ---[ 574]---> Adder-cost: 1074   maxlim: 588   bits: 10/10
c ---[ 572]---> Adder-cost: 924   maxlim: 590   bits: 10/10
c ---[ 570]---> Adder-cost: 1142   maxlim: 586   bits: 10/10
c ---[ 568]---> Adder-cost: 1026   maxlim: 592   bits: 10/10
c ---[ 566]---> Adder-cost: 1160   maxlim: 586   bits: 10/10
c ---[ 564]---> Adder-cost: 1160   maxlim: 594   bits: 10/10
c ---[ 562]---> Adder-cost: 1150   maxlim: 590   bits: 10/10
c ---[ 560]---> Adder-cost: 1142   maxlim: 590   bits: 10/10
c ---[ 558]---> Adder-cost: 966   maxlim: 587   bits: 10/10
c ---[ 556]---> Adder-cost: 1058   maxlim: 587   bits: 10/10
c ---[ 554]---> Adder-cost: 1172   maxlim: 597   bits: 10/10
c ---[ 552]---> Adder-cost: 1122   maxlim: 590   bits: 10/10
c ---[ 550]---> Adder-cost: 1160   maxlim: 589   bits: 10/10
c ---[ 548]---> Adder-cost: 944   maxlim: 599   bits: 10/10
c ---[ 546]---> Adder-cost: 910   maxlim: 597   bits: 10/10
c ---[ 544]---> Adder-cost: 1100   maxlim: 588   bits: 10/10
c ---[ 542]---> Adder-cost: 1156   maxlim: 586   bits: 10/10
c ---[ 540]---> Adder-cost: 1138   maxlim: 588   bits: 10/10
c ---[ 538]---> Adder-cost: 1176   maxlim: 591   bits: 10/10
c ---[ 536]---> Adder-cost: 1026   maxlim: 595   bits: 10/10
c ---[ 534]---> Adder-cost: 1162   maxlim: 587   bits: 10/10
c ---[ 532]---> Adder-cost: 1018   maxlim: 584   bits: 10/10
c ---[ 530]---> Adder-cost: 1164   maxlim: 586   bits: 10/10
c ---[ 528]---> Adder-cost: 1170   maxlim: 589   bits: 10/10
c ---[ 526]---> Adder-cost: 792   maxlim: 595   bits: 10/10
c ---[ 524]---> Adder-cost: 1176   maxlim: 593   bits: 10/10
c ---[ 522]---> Adder-cost: 1170   maxlim: 589   bits: 10/10
c ---[ 520]---> Adder-cost: 1176   maxlim: 598   bits: 10/10
c ---[ 518]---> Adder-cost: 1160   maxlim: 592   bits: 10/10
c ---[ 516]---> Adder-cost: 1116   maxlim: 586   bits: 10/10
c ---[ 514]---> Adder-cost: 1174   maxlim: 591   bits: 10/10
c ---[ 512]---> Adder-cost: 1128   maxlim: 586   bits: 10/10
c ---[ 510]---> Adder-cost: 1152   maxlim: 590   bits: 10/10
c ---[ 508]---> Adder-cost: 900   maxlim: 587   bits: 10/10
c ---[ 506]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[ 504]---> Adder-cost: 1162   maxlim: 590   bits: 10/10
c ---[ 502]---> Adder-cost: 1112   maxlim: 592   bits: 10/10
c ---[ 500]---> Adder-cost: 618   maxlim: 584   bits: 10/10
c ---[ 498]---> Adder-cost: 1156   maxlim: 588   bits: 10/10
c ---[ 496]---> Adder-cost: 1178   maxlim: 595   bits: 10/10
c ---[ 494]---> Adder-cost: 1174   maxlim: 591   bits: 10/10
c ---[ 492]---> Adder-cost: 1156   maxlim: 586   bits: 10/10
c ---[ 490]---> Adder-cost: 1162   maxlim: 586   bits: 10/10
c ---[ 488]---> Adder-cost: 948   maxlim: 587   bits: 10/10
c ---[ 486]---> Adder-cost: 1150   maxlim: 587   bits: 10/10
c ---[ 484]---> Adder-cost: 1164   maxlim: 586   bits: 10/10
c ---[ 482]---> Adder-cost: 1166   maxlim: 588   bits: 10/10
c ---[ 480]---> Adder-cost: 1164   maxlim: 586   bits: 10/10
c ---[ 478]---> Adder-cost: 752   maxlim: 588   bits: 10/10
c ---[ 476]---> Adder-cost: 1180   maxlim: 593   bits: 10/10
c ---[ 474]---> Adder-cost: 1162   maxlim: 584   bits: 10/10
c ---[ 472]---> Adder-cost: 1164   maxlim: 591   bits: 10/10
c ---[ 470]---> Adder-cost: 1034   maxlim: 591   bits: 10/10
c ---[ 468]---> Adder-cost: 1170   maxlim: 589   bits: 10/10
c ---[ 466]---> Adder-cost: 452   maxlim: 587   bits: 10/10
c ---[ 464]---> Adder-cost: 1174   maxlim: 596   bits: 10/10
c ---[ 462]---> Adder-cost: 1036   maxlim: 605   bits: 10/10
c ---[ 460]---> Adder-cost: 1066   maxlim: 590   bits: 10/10
c ---[ 458]---> Adder-cost: 1046   maxlim: 586   bits: 10/10
c ---[ 456]---> Adder-cost: 1174   maxlim: 595   bits: 10/10
c ---[ 454]---> Adder-cost: 536   maxlim: 590   bits: 10/10
c ---[ 452]---> Adder-cost: 790   maxlim: 588   bits: 10/10
c ---[ 450]---> Adder-cost: 964   maxlim: 586   bits: 10/10
c ---[ 448]---> Adder-cost: 544   maxlim: 589   bits: 10/10
c ---[ 446]---> Adder-cost: 894   maxlim: 589   bits: 10/10
c ---[ 444]---> Adder-cost: 1042   maxlim: 589   bits: 10/10
c ---[ 442]---> Adder-cost: 1142   maxlim: 590   bits: 10/10
c ---[ 440]---> Adder-cost: 1142   maxlim: 594   bits: 10/10
c ---[ 438]---> Adder-cost: 1142   maxlim: 594   bits: 10/10
c ---[ 436]---> Adder-cost: 1126   maxlim: 595   bits: 10/10
c ---[ 434]---> Adder-cost: 1172   maxlim: 593   bits: 10/10
c ---[ 432]---> Adder-cost: 904   maxlim: 588   bits: 10/10
c ---[ 430]---> Adder-cost: 1126   maxlim: 584   bits: 10/10
c ---[ 428]---> Adder-cost: 1138   maxlim: 592   bits: 10/10
c ---[ 426]---> Adder-cost: 1052   maxlim: 589   bits: 10/10
c ---[ 424]---> Adder-cost: 1170   maxlim: 597   bits: 10/10
c ---[ 422]---> Adder-cost: 992   maxlim: 592   bits: 10/10
c ---[ 420]---> Adder-cost: 1114   maxlim: 586   bits: 10/10
c ---[ 418]---> Adder-cost: 942   maxlim: 591   bits: 10/10
c ---[ 416]---> Adder-cost: 1058   maxlim: 590   bits: 10/10
c ---[ 414]---> Adder-cost: 1134   maxlim: 586   bits: 10/10
c ---[ 412]---> Adder-cost: 1168   maxlim: 588   bits: 10/10
c ---[ 410]---> Adder-cost: 1156   maxlim: 586   bits: 10/10
c ---[ 408]---> Adder-cost: 1186   maxlim: 598   bits: 10/10
c ---[ 406]---> Adder-cost: 1158   maxlim: 586   bits: 10/10
c ---[ 404]---> Adder-cost: 1164   maxlim: 587   bits: 10/10
c ---[ 402]---> Adder-cost: 1136   maxlim: 590   bits: 10/10
c ---[ 400]---> Adder-cost: 988   maxlim: 588   bits: 10/10
c ---[ 398]---> Adder-cost: 1168   maxlim: 589   bits: 10/10
c ---[ 396]---> Adder-cost: 1166   maxlim: 588   bits: 10/10
c ---[ 394]---> Adder-cost: 892   maxlim: 591   bits: 10/10
c ---[ 392]---> Adder-cost: 978   maxlim: 588   bits: 10/10
c ---[ 390]---> Adder-cost: 1042   maxlim: 589   bits: 10/10
c ---[ 388]---> Adder-cost: 1120   maxlim: 586   bits: 10/10
c ---[ 386]---> Adder-cost: 898   maxlim: 595   bits: 10/10
c ---[ 384]---> Adder-cost: 996   maxlim: 606   bits: 10/10
c ---[ 382]---> Adder-cost: 1126   maxlim: 587   bits: 10/10
c ---[ 380]---> Adder-cost: 980   maxlim: 592   bits: 10/10
c ---[ 378]---> Adder-cost: 1144   maxlim: 600   bits: 10/10
c ---[ 376]---> Adder-cost: 1114   maxlim: 593   bits: 10/10
c ---[ 374]---> Adder-cost: 1028   maxlim: 589   bits: 10/10
c ---[ 372]---> Adder-cost: 1062   maxlim: 584   bits: 10/10
c ---[ 370]---> Adder-cost: 958   maxlim: 589   bits: 10/10
c ---[ 368]---> Adder-cost: 1018   maxlim: 588   bits: 10/10
c ---[ 366]---> Adder-cost: 1162   maxlim: 590   bits: 10/10
c ---[ 364]---> Adder-cost: 1084   maxlim: 591   bits: 10/10
c ---[ 362]---> Adder-cost: 1122   maxlim: 588   bits: 10/10
c ---[ 360]---> Adder-cost: 1158   maxlim: 586   bits: 10/10
c ---[ 358]---> Adder-cost: 1146   maxlim: 588   bits: 10/10
c ---[ 356]---> Adder-cost: 928   maxlim: 587   bits: 10/10
c ---[ 354]---> Adder-cost: 1090   maxlim: 587   bits: 10/10
c ---[ 352]---> Adder-cost: 1076   maxlim: 591   bits: 10/10
c ---[ 350]---> Adder-cost: 1156   maxlim: 586   bits: 10/10
c ---[ 348]---> Adder-cost: 1066   maxlim: 593   bits: 10/10
c ---[ 346]---> Adder-cost: 1122   maxlim: 588   bits: 10/10
c ---[ 344]---> Adder-cost: 1098   maxlim: 586   bits: 10/10
c ---[ 342]---> Adder-cost: 1160   maxlim: 590   bits: 10/10
c ---[ 340]---> Adder-cost: 1006   maxlim: 587   bits: 10/10
c ---[ 338]---> Adder-cost: 1204   maxlim: 611   bits: 10/10
c ---[ 336]---> Adder-cost: 1168   maxlim: 589   bits: 10/10
c ---[ 334]---> Adder-cost: 1178   maxlim: 592   bits: 10/10
c ---[ 332]---> Adder-cost: 844   maxlim: 590   bits: 10/10
c ---[ 330]---> Adder-cost: 1094   maxlim: 588   bits: 10/10
c ---[ 328]---> Adder-cost: 1042   maxlim: 589   bits: 10/10
c ---[ 326]---> Adder-cost: 1160   maxlim: 587   bits: 10/10
c ---[ 324]---> Adder-cost: 1000   maxlim: 589   bits: 10/10
c ---[ 322]---> Adder-cost: 1066   maxlim: 584   bits: 10/10
c ---[ 320]---> Adder-cost: 1086   maxlim: 603   bits: 10/10
c ---[ 318]---> Adder-cost: 1164   maxlim: 586   bits: 10/10
c ---[ 316]---> Adder-cost: 1146   maxlim: 587   bits: 10/10
c ---[ 314]---> Adder-cost: 1094   maxlim: 590   bits: 10/10
c ---[ 312]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[ 310]---> Adder-cost: 1168   maxlim: 588   bits: 10/10
c ---[ 308]---> Adder-cost: 1132   maxlim: 588   bits: 10/10
c ---[ 306]---> Adder-cost: 1166   maxlim: 588   bits: 10/10
c ---[ 304]---> Adder-cost: 1176   maxlim: 593   bits: 10/10
c ---[ 302]---> Adder-cost: 952   maxlim: 589   bits: 10/10
c ---[ 300]---> Adder-cost: 1160   maxlim: 584   bits: 10/10
c ---[ 298]---> Adder-cost: 1100   maxlim: 590   bits: 10/10
c ---[ 296]---> Adder-cost: 1046   maxlim: 587   bits: 10/10
c ---[ 294]---> Adder-cost: 958   maxlim: 588   bits: 10/10
c ---[ 292]---> Adder-cost: 1090   maxlim: 588   bits: 10/10
c ---[ 290]---> Adder-cost: 1086   maxlim: 588   bits: 10/10
c ---[ 288]---> Adder-cost: 832   maxlim: 600   bits: 10/10
c ---[ 286]---> Adder-cost: 1174   maxlim: 591   bits: 10/10
c ---[ 284]---> Adder-cost: 1038   maxlim: 589   bits: 10/10
c ---[ 282]---> Adder-cost: 840   maxlim: 593   bits: 10/10
c ---[ 280]---> Adder-cost: 1138   maxlim: 591   bits: 10/10
c ---[ 278]---> Adder-cost: 1046   maxlim: 592   bits: 10/10
c ---[ 276]---> Adder-cost: 1020   maxlim: 589   bits: 10/10
c ---[ 274]---> Adder-cost: 998   maxlim: 592   bits: 10/10
c ---[ 272]---> Adder-cost: 1060   maxlim: 594   bits: 10/10
c ---[ 270]---> Adder-cost: 992   maxlim: 587   bits: 10/10
c ---[ 268]---> Adder-cost: 1142   maxlim: 589   bits: 10/10
c ---[ 266]---> Adder-cost: 832   maxlim: 585   bits: 10/10
c ---[ 264]---> Adder-cost: 490   maxlim: 587   bits: 10/10
c ---[ 262]---> Adder-cost: 1034   maxlim: 596   bits: 10/10
c ---[ 260]---> Adder-cost: 1164   maxlim: 587   bits: 10/10
c ---[ 258]---> Adder-cost: 1038   maxlim: 596   bits: 10/10
c ---[ 256]---> Adder-cost: 1148   maxlim: 599   bits: 10/10
c ---[ 254]---> Adder-cost: 998   maxlim: 589   bits: 10/10
c ---[ 252]---> Adder-cost: 878   maxlim: 592   bits: 10/10
c ---[ 250]---> Adder-cost: 1158   maxlim: 595   bits: 10/10
c ---[ 248]---> Adder-cost: 1100   maxlim: 603   bits: 10/10
c ---[ 246]---> Adder-cost: 1018   maxlim: 593   bits: 10/10
c ---[ 244]---> Adder-cost: 1080   maxlim: 587   bits: 10/10
c ---[ 242]---> Adder-cost: 842   maxlim: 589   bits: 10/10
c ---[ 240]---> Adder-cost: 1118   maxlim: 587   bits: 10/10
c ---[ 238]---> Adder-cost: 1168   maxlim: 590   bits: 10/10
c ---[ 236]---> Adder-cost: 1154   maxlim: 587   bits: 10/10
c ---[ 234]---> Adder-cost: 1066   maxlim: 590   bits: 10/10
c ---[ 232]---> Adder-cost: 966   maxlim: 588   bits: 10/10
c ---[ 230]---> Adder-cost: 836   maxlim: 591   bits: 10/10
c ---[ 228]---> Adder-cost: 876   maxlim: 593   bits: 10/10
c ---[ 226]---> Adder-cost: 1144   maxlim: 585   bits: 10/10
c ---[ 224]---> Adder-cost: 1152   maxlim: 595   bits: 10/10
c ---[ 222]---> Adder-cost: 1100   maxlim: 592   bits: 10/10
c ---[ 220]---> Adder-cost: 1038   maxlim: 585   bits: 10/10
c ---[ 218]---> Adder-cost: 1180   maxlim: 598   bits: 10/10
c ---[ 216]---> Adder-cost: 1120   maxlim: 590   bits: 10/10
c ---[ 214]---> Adder-cost: 1128   maxlim: 590   bits: 10/10
c ---[ 212]---> Adder-cost: 1124   maxlim: 591   bits: 10/10
c ---[ 210]---> Adder-cost: 1096   maxlim: 588   bits: 10/10
c ---[ 208]---> Adder-cost: 1164   maxlim: 604   bits: 10/10
c ---[ 206]---> Adder-cost: 1116   maxlim: 595   bits: 10/10
c ---[ 204]---> Adder-cost: 1158   maxlim: 592   bits: 10/10
c ---[ 202]---> Adder-cost: 1156   maxlim: 591   bits: 10/10
c ---[ 200]---> Adder-cost: 1150   maxlim: 592   bits: 10/10
c ---[ 198]---> Adder-cost: 1094   maxlim: 592   bits: 10/10
c ---[ 196]---> Adder-cost: 954   maxlim: 587   bits: 10/10
c ---[ 194]---> Adder-cost: 1016   maxlim: 587   bits: 10/10
c ---[ 192]---> Adder-cost: 1120   maxlim: 588   bits: 10/10
c ---[ 190]---> Adder-cost: 1178   maxlim: 594   bits: 10/10
c ---[ 188]---> Adder-cost: 1058   maxlim: 584   bits: 10/10
c ---[ 186]---> Adder-cost: 1044   maxlim: 588   bits: 10/10
c ---[ 184]---> Adder-cost: 1162   maxlim: 586   bits: 10/10
c ---[ 182]---> Adder-cost: 918   maxlim: 595   bits: 10/10
c ---[ 180]---> Adder-cost: 1126   maxlim: 596   bits: 10/10
c ---[ 178]---> Adder-cost: 968   maxlim: 589   bits: 10/10
c ---[ 176]---> Adder-cost: 1102   maxlim: 591   bits: 10/10
c ---[ 174]---> Adder-cost: 1092   maxlim: 587   bits: 10/10
c ---[ 172]---> Adder-cost: 1032   maxlim: 598   bits: 10/10
c ---[ 170]---> Adder-cost: 1024   maxlim: 590   bits: 10/10
c ---[ 168]---> Adder-cost: 1176   maxlim: 595   bits: 10/10
c ---[ 166]---> Adder-cost: 1162   maxlim: 598   bits: 10/10
c ---[ 164]---> Adder-cost: 1146   maxlim: 593   bits: 10/10
c ---[ 162]---> Adder-cost: 1046   maxlim: 589   bits: 10/10
c ---[ 160]---> Adder-cost: 1034   maxlim: 590   bits: 10/10
c ---[ 158]---> Adder-cost: 1158   maxlim: 593   bits: 10/10
c ---[ 156]---> Adder-cost: 910   maxlim: 589   bits: 10/10
c ---[ 154]---> Adder-cost: 1162   maxlim: 599   bits: 10/10
c ---[ 152]---> Adder-cost: 1136   maxlim: 589   bits: 10/10
c ---[ 150]---> Adder-cost: 1084   maxlim: 589   bits: 10/10
c ---[ 148]---> Adder-cost: 1174   maxlim: 595   bits: 10/10
c ---[ 146]---> Adder-cost: 1158   maxlim: 590   bits: 10/10
c ---[ 144]---> Adder-cost: 1150   maxlim: 585   bits: 10/10
c ---[ 142]---> Adder-cost: 1132   maxlim: 594   bits: 10/10
c ---[ 140]---> Adder-cost: 1156   maxlim: 588   bits: 10/10
c ---[ 138]---> Adder-cost: 1062   maxlim: 588   bits: 10/10
c ---[ 136]---> Adder-cost: 1120   maxlim: 586   bits: 10/10
c ---[ 134]---> Adder-cost: 830   maxlim: 593   bits: 10/10
c ---[ 132]---> Adder-cost: 1132   maxlim: 587   bits: 10/10
c ---[ 130]---> Adder-cost: 1056   maxlim: 587   bits: 10/10
c ---[ 128]---> Adder-cost: 1096   maxlim: 587   bits: 10/10
c ---[ 126]---> Adder-cost: 1168   maxlim: 591   bits: 10/10
c ---[ 124]---> Adder-cost: 1104   maxlim: 598   bits: 10/10
c ---[ 122]---> Adder-cost: 1166   maxlim: 589   bits: 10/10
c ---[ 120]---> Adder-cost: 928   maxlim: 590   bits: 10/10
c ---[ 118]---> Adder-cost: 946   maxlim: 596   bits: 10/10
c ---[ 116]---> Adder-cost: 1122   maxlim: 596   bits: 10/10
c ---[ 114]---> Adder-cost: 1158   maxlim: 599   bits: 10/10
c ---[ 112]---> Adder-cost: 922   maxlim: 587   bits: 10/10
c ---[ 110]---> Adder-cost: 1062   maxlim: 586   bits: 10/10
c ---[ 108]---> Adder-cost: 1044   maxlim: 593   bits: 10/10
c ---[ 106]---> Adder-cost: 1068   maxlim: 601   bits: 10/10
c ---[ 104]---> Adder-cost: 1138   maxlim: 600   bits: 10/10
c ---[ 102]---> Adder-cost: 1136   maxlim: 592   bits: 10/10
c ---[ 100]---> Adder-cost: 932   maxlim: 587   bits: 10/10
c ---[  98]---> Adder-cost: 980   maxlim: 599   bits: 10/10
c ---[  96]---> Adder-cost: 1060   maxlim: 590   bits: 10/10
c ---[  94]---> Adder-cost: 1150   maxlim: 585   bits: 10/10
c ---[  92]---> Adder-cost: 1162   maxlim: 589   bits: 10/10
c ---[  90]---> Adder-cost: 1056   maxlim: 585   bits: 10/10
c ---[  88]---> Adder-cost: 952   maxlim: 586   bits: 10/10
c ---[  86]---> Adder-cost: 684   maxlim: 586   bits: 10/10
c ---[  84]---> Adder-cost: 1104   maxlim: 588   bits: 10/10
c ---[  82]---> Adder-cost: 1078   maxlim: 587   bits: 10/10
c ---[  80]---> Adder-cost: 1164   maxlim: 589   bits: 10/10
c ---[  78]---> Adder-cost: 1092   maxlim: 589   bits: 10/10
c ---[  76]---> Adder-cost: 1136   maxlim: 586   bits: 10/10
c ---[  74]---> Adder-cost: 1108   maxlim: 590   bits: 10/10
c ---[  72]---> Adder-cost: 1054   maxlim: 588   bits: 10/10
c ---[  70]---> Adder-cost: 1096   maxlim: 588   bits: 10/10
c ---[  68]---> Adder-cost: 1124   maxlim: 587   bits: 10/10
c ---[  66]---> Adder-cost: 1162   maxlim: 587   bits: 10/10
c ---[  64]---> Adder-cost: 1108   maxlim: 587   bits: 10/10
c ---[  62]---> Adder-cost: 1158   maxlim: 588   bits: 10/10
c ---[  60]---> Adder-cost: 1156   maxlim: 588   bits: 10/10
c ---[  58]---> Adder-cost: 1156   maxlim: 584   bits: 10/10
c ---[  56]---> Adder-cost: 890   maxlim: 586   bits: 10/10
c ---[  54]---> Adder-cost: 1024   maxlim: 591   bits: 10/10
c ---[  52]---> Adder-cost: 1164   maxlim: 585   bits: 10/10
c ---[  50]---> Adder-cost: 954   maxlim: 590   bits: 10/10
c ---[  48]---> Adder-cost: 1112   maxlim: 586   bits: 10/10
c ---[  46]---> Adder-cost: 776   maxlim: 587   bits: 10/10
c ---[  44]---> Adder-cost: 1158   maxlim: 587   bits: 10/10
c ---[  42]---> Adder-cost: 1152   maxlim: 591   bits: 10/10
c ---[  40]---> Adder-cost: 1048   maxlim: 589   bits: 10/10
c ---[  38]---> Adder-cost: 746   maxlim: 587   bits: 10/10
c ---[  36]---> Adder-cost: 650   maxlim: 584   bits: 10/10
c ---[  34]---> Adder-cost: 1012   maxlim: 588   bits: 10/10
c ---[  32]---> Adder-cost: 1096   maxlim: 587   bits: 10/10
c ---[  30]---> Adder-cost: 1008   maxlim: 594   bits: 10/10
c ---[  28]---> Adder-cost: 958   maxlim: 587   bits: 10/10
c ---[  26]---> Adder-cost: 1074   maxlim: 588   bits: 10/10
c ---[  24]---> Adder-cost: 1142   maxlim: 590   bits: 10/10
c ---[  22]---> Adder-cost: 1120   maxlim: 586   bits: 10/10
c ---[  20]---> Adder-cost: 1154   maxlim: 586   bits: 10/10
c ---[  18]---> Adder-cost: 1102   maxlim: 591   bits: 10/10
c ---[  16]---> Adder-cost: 1152   maxlim: 588   bits: 10/10
c ---[  14]---> Adder-cost: 1060   maxlim: 598   bits: 10/10
c ---[  12]---> Adder-cost: 902   maxlim: 597   bits: 10/10
c ---[  10]---> Adder-cost: 1136   maxlim: 596   bits: 10/10
c ---[   8]---> Adder-cost: 782   maxlim: 586   bits: 10/10
c ---[   6]---> Adder-cost: 1064   maxlim: 584   bits: 10/10
c ---[   4]---> Adder-cost: 896   maxlim: 588   bits: 10/10
c ---[   2]---> Adder-cost: 1040   maxlim: 585   bits: 10/10
c ---[   0]---> Adder-cost: 530   maxlim: 587   bits: 10/10
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 | 4137367 14764807 | 1379122       0        0     nan |  0.000 % |
c |       100 | 4136784 14762756 | 1517034      23       73     3.2 |  1.888 % |
c |       250 | 4135917 14759701 | 1668737      59      184     3.1 |  1.910 % |
c |       475 | 4134742 14755562 | 1835611     132      409     3.1 |  1.938 % |
c |       812 | 4132561 14747925 | 2019172     188      575     3.1 |  1.993 % |
c |      1319 | 4129446 14736964 | 2221089     270      823     3.0 |  2.070 % |
c |      2078 | 4125147 14721911 | 2443198     466     1413     3.0 |  2.177 % |
#### 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.72 0.91 0.89 2/54 10443
Raw data (stat): 10443 (runsolver) R 10442 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 477490369 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.76 0.91 0.89 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 30125 0 0 0 919 79 0 0 25 0 1 0 477490369 129703936 28353 4294967295 134512640 134672761 3221224544 3221219656 1075349707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31666 28353 603 41 0 31625 0
vsize: 126664
[startup+20.0073 s]
Raw data (loadavg): 0.80 0.91 0.89 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72225 0 0 0 1821 178 0 0 25 0 1 0 477490369 321921024 70453 4294967295 134512640 134672761 3221224544 3221223844 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70453 603 41 0 78553 0
vsize: 314376
[startup+30.0077 s]
Raw data (loadavg): 0.83 0.92 0.89 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72238 0 0 0 2821 178 0 0 25 0 1 0 477490369 321921024 70466 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70466 603 41 0 78553 0
vsize: 314376
[startup+40.0084 s]
Raw data (loadavg): 0.85 0.92 0.89 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72239 0 0 0 3821 179 0 0 25 0 1 0 477490369 321921024 70467 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70467 603 41 0 78553 0
vsize: 314376
[startup+50.0086 s]
Raw data (loadavg): 0.88 0.92 0.90 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72247 0 0 0 4821 179 0 0 25 0 1 0 477490369 321921024 70475 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70475 603 41 0 78553 0
vsize: 314376
[startup+60.009 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72247 0 0 0 5820 179 0 0 25 0 1 0 477490369 321921024 70475 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70475 603 41 0 78553 0
vsize: 314376
[startup+70.0088 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72248 0 0 0 6820 179 0 0 25 0 1 0 477490369 321921024 70476 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70476 603 41 0 78553 0
vsize: 314376
[startup+80.01 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72248 0 0 0 7820 180 0 0 25 0 1 0 477490369 321921024 70476 4294967295 134512640 134672761 3221224544 3221223724 134556674 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70476 603 41 0 78553 0
vsize: 314376
[startup+90.0104 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72248 0 0 0 8820 180 0 0 25 0 1 0 477490369 321921024 70476 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70476 603 41 0 78553 0
vsize: 314376
[startup+100.01 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72248 0 0 0 9820 180 0 0 25 0 1 0 477490369 321921024 70476 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70476 603 41 0 78553 0
vsize: 314376
[startup+110.012 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72249 0 0 0 10820 180 0 0 25 0 1 0 477490369 321921024 70477 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70477 603 41 0 78553 0
vsize: 314376
[startup+120.012 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72249 0 0 0 11820 180 0 0 25 0 1 0 477490369 321921024 70477 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70477 603 41 0 78553 0
vsize: 314376
[startup+130.012 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72249 0 0 0 12820 181 0 0 25 0 1 0 477490369 321921024 70477 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70477 603 41 0 78553 0
vsize: 314376
[startup+140.013 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72250 0 0 0 13820 181 0 0 25 0 1 0 477490369 321921024 70478 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78594 70478 603 41 0 78553 0
vsize: 314376
[startup+150.013 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72250 0 0 0 14820 181 0 0 25 0 1 0 477490369 321921024 70478 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70478 603 41 0 78553 0
vsize: 314376
[startup+160.013 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72250 0 0 0 15820 181 0 0 25 0 1 0 477490369 321921024 70478 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70478 603 41 0 78553 0
vsize: 314376
[startup+170.012 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72250 0 0 0 16820 181 0 0 25 0 1 0 477490369 321921024 70478 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70478 603 41 0 78553 0
vsize: 314376
[startup+180.013 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72251 0 0 0 17820 181 0 0 25 0 1 0 477490369 321921024 70479 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70479 603 41 0 78553 0
vsize: 314376
[startup+190.013 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72251 0 0 0 18820 181 0 0 25 0 1 0 477490369 321921024 70479 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70479 603 41 0 78553 0
vsize: 314376
[startup+200.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72251 0 0 0 19820 181 0 0 25 0 1 0 477490369 321921024 70479 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70479 603 41 0 78553 0
vsize: 314376
[startup+210.021 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72256 0 0 0 20821 181 0 0 25 0 1 0 477490369 321921024 70484 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70484 603 41 0 78553 0
vsize: 314376
[startup+220.142 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72257 0 0 0 21834 181 0 0 25 0 1 0 477490369 321921024 70485 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70485 603 41 0 78553 0
vsize: 314376
[startup+230.142 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72266 0 0 0 22834 181 0 0 25 0 1 0 477490369 321921024 70494 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70494 603 41 0 78553 0
vsize: 314376
[startup+240.142 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72272 0 0 0 23834 181 0 0 25 0 1 0 477490369 322056192 70500 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78627 70500 603 41 0 78586 0
vsize: 314508
[startup+250.142 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72288 0 0 0 24834 181 0 0 25 0 1 0 477490369 322056192 70516 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78627 70516 603 41 0 78586 0
vsize: 314508
[startup+260.143 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72292 0 0 0 25834 181 0 0 25 0 1 0 477490369 322056192 70520 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78627 70520 603 41 0 78586 0
vsize: 314508
[startup+270.142 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72311 0 0 0 26834 181 0 0 25 0 1 0 477490369 322191360 70539 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78660 70539 603 41 0 78619 0
vsize: 314640
[startup+280.15 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72311 0 0 0 27835 181 0 0 25 0 1 0 477490369 322191360 70539 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78660 70539 603 41 0 78619 0
vsize: 314640
[startup+290.159 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72321 0 0 0 28836 181 0 0 25 0 1 0 477490369 322191360 70549 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78660 70549 603 41 0 78619 0
vsize: 314640
[startup+300.158 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72331 0 0 0 29836 181 0 0 25 0 1 0 477490369 322191360 70559 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78660 70559 603 41 0 78619 0
vsize: 314640
[startup+310.157 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72338 0 0 0 30837 181 0 0 25 0 1 0 477490369 322191360 70566 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78660 70566 603 41 0 78619 0
vsize: 314640
[startup+320.158 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72340 0 0 0 31837 181 0 0 25 0 1 0 477490369 322326528 70568 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78693 70568 603 41 0 78652 0
vsize: 314772
[startup+330.158 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72349 0 0 0 32837 181 0 0 25 0 1 0 477490369 322326528 70577 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78693 70577 603 41 0 78652 0
vsize: 314772
[startup+340.166 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72365 0 0 0 33838 181 0 0 25 0 1 0 477490369 322326528 70593 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78693 70593 603 41 0 78652 0
vsize: 314772
[startup+350.172 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72367 0 0 0 34839 181 0 0 25 0 1 0 477490369 322461696 70595 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78726 70595 603 41 0 78685 0
vsize: 314904
[startup+360.181 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72382 0 0 0 35840 181 0 0 25 0 1 0 477490369 322461696 70610 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78726 70610 603 41 0 78685 0
vsize: 314904
[startup+370.181 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72405 0 0 0 36840 181 0 0 25 0 1 0 477490369 322596864 70633 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78759 70633 603 41 0 78718 0
vsize: 315036
[startup+380.191 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72410 0 0 0 37841 181 0 0 25 0 1 0 477490369 322596864 70638 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78759 70638 603 41 0 78718 0
vsize: 315036
[startup+390.2 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72416 0 0 0 38842 181 0 0 25 0 1 0 477490369 322596864 70644 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78759 70644 603 41 0 78718 0
vsize: 315036
[startup+400.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72423 0 0 0 39842 181 0 0 25 0 1 0 477490369 322596864 70651 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78759 70651 603 41 0 78718 0
vsize: 315036
[startup+410.201 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72426 0 0 0 40842 181 0 0 25 0 1 0 477490369 322596864 70654 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78759 70654 603 41 0 78718 0
vsize: 315036
[startup+420.2 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72437 0 0 0 41843 181 0 0 25 0 1 0 477490369 322732032 70665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78792 70665 603 41 0 78751 0
vsize: 315168
[startup+430.201 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72445 0 0 0 42843 181 0 0 25 0 1 0 477490369 322732032 70673 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78792 70673 603 41 0 78751 0
vsize: 315168
[startup+440.201 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72455 0 0 0 43843 181 0 0 25 0 1 0 477490369 322732032 70683 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78792 70683 603 41 0 78751 0
vsize: 315168
[startup+450.201 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72476 0 0 0 44843 181 0 0 25 0 1 0 477490369 322867200 70704 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78825 70704 603 41 0 78784 0
vsize: 315300
[startup+460.202 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72476 0 0 0 45843 181 0 0 25 0 1 0 477490369 322867200 70704 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78825 70704 603 41 0 78784 0
vsize: 315300
[startup+470.206 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72493 0 0 0 46844 181 0 0 25 0 1 0 477490369 322867200 70721 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78825 70721 603 41 0 78784 0
vsize: 315300
[startup+480.207 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72502 0 0 0 47844 181 0 0 25 0 1 0 477490369 323002368 70730 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78858 70730 603 41 0 78817 0
vsize: 315432
[startup+490.208 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72521 0 0 0 48844 181 0 0 25 0 1 0 477490369 323002368 70749 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78858 70749 603 41 0 78817 0
vsize: 315432
[startup+500.207 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72537 0 0 0 49844 181 0 0 25 0 1 0 477490369 323137536 70765 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78891 70765 603 41 0 78850 0
vsize: 315564
[startup+510.207 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72539 0 0 0 50844 181 0 0 25 0 1 0 477490369 323137536 70767 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78891 70767 603 41 0 78850 0
vsize: 315564
[startup+520.214 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72554 0 0 0 51845 181 0 0 25 0 1 0 477490369 323137536 70782 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78891 70782 603 41 0 78850 0
vsize: 315564
[startup+530.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72566 0 0 0 52846 181 0 0 25 0 1 0 477490369 323137536 70794 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78891 70794 603 41 0 78850 0
vsize: 315564
[startup+540.22 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72580 0 0 0 53846 181 0 0 25 0 1 0 477490369 323272704 70808 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78924 70808 603 41 0 78883 0
vsize: 315696
[startup+550.219 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72580 0 0 0 54846 181 0 0 25 0 1 0 477490369 323272704 70808 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78924 70808 603 41 0 78883 0
vsize: 315696
[startup+560.224 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72580 0 0 0 55847 181 0 0 25 0 1 0 477490369 323272704 70808 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78924 70808 603 41 0 78883 0
vsize: 315696
[startup+570.224 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72599 0 0 0 56847 181 0 0 25 0 1 0 477490369 323272704 70827 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78924 70827 603 41 0 78883 0
vsize: 315696
[startup+580.225 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72620 0 0 0 57847 181 0 0 25 0 1 0 477490369 323407872 70848 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78957 70848 603 41 0 78916 0
vsize: 315828
[startup+590.234 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72638 0 0 0 58848 182 0 0 25 0 1 0 477490369 323543040 70866 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78990 70866 603 41 0 78949 0
vsize: 315960
[startup+600.234 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72656 0 0 0 59848 182 0 0 25 0 1 0 477490369 323543040 70884 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78990 70884 603 41 0 78949 0
vsize: 315960
[startup+610.234 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72661 0 0 0 60848 182 0 0 25 0 1 0 477490369 323543040 70889 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78990 70889 603 41 0 78949 0
vsize: 315960
[startup+620.235 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72667 0 0 0 61848 182 0 0 25 0 1 0 477490369 323543040 70895 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78990 70895 603 41 0 78949 0
vsize: 315960
[startup+630.235 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72669 0 0 0 62848 182 0 0 25 0 1 0 477490369 323678208 70897 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79023 70897 603 41 0 78982 0
vsize: 316092
[startup+640.236 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72673 0 0 0 63849 182 0 0 25 0 1 0 477490369 323678208 70901 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79023 70901 603 41 0 78982 0
vsize: 316092
[startup+650.235 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72698 0 0 0 64849 182 0 0 25 0 1 0 477490369 323678208 70926 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79023 70926 603 41 0 78982 0
vsize: 316092
[startup+660.236 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72702 0 0 0 65849 182 0 0 25 0 1 0 477490369 323813376 70930 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79056 70930 603 41 0 79015 0
vsize: 316224
[startup+670.236 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72724 0 0 0 66849 182 0 0 25 0 1 0 477490369 323813376 70952 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79056 70952 603 41 0 79015 0
vsize: 316224
[startup+680.237 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72748 0 0 0 67849 182 0 0 25 0 1 0 477490369 323948544 70976 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79089 70976 603 41 0 79048 0
vsize: 316356
[startup+690.237 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72756 0 0 0 68849 182 0 0 25 0 1 0 477490369 323948544 70984 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79089 70984 603 41 0 79048 0
vsize: 316356
[startup+700.237 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72767 0 0 0 69849 182 0 0 25 0 1 0 477490369 323948544 70995 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79089 70995 603 41 0 79048 0
vsize: 316356
[startup+710.238 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72782 0 0 0 70850 182 0 0 25 0 1 0 477490369 324083712 71010 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79122 71010 603 41 0 79081 0
vsize: 316488
[startup+720.237 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72794 0 0 0 71850 182 0 0 25 0 1 0 477490369 324083712 71022 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79122 71022 603 41 0 79081 0
vsize: 316488
[startup+730.239 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72810 0 0 0 72850 182 0 0 25 0 1 0 477490369 324218880 71038 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79155 71038 603 41 0 79114 0
vsize: 316620
[startup+740.238 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72835 0 0 0 73850 182 0 0 25 0 1 0 477490369 324415488 71063 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79203 71063 603 41 0 79162 0
vsize: 316812
[startup+750.238 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72839 0 0 0 74850 182 0 0 25 0 1 0 477490369 324415488 71067 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79203 71067 603 41 0 79162 0
vsize: 316812
[startup+760.239 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72854 0 0 0 75850 182 0 0 25 0 1 0 477490369 324415488 71082 4294967295 134512640 134672761 3221224544 3221223716 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79203 71082 603 41 0 79162 0
vsize: 316812
[startup+770.24 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72858 0 0 0 76851 182 0 0 25 0 1 0 477490369 324415488 71086 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79203 71086 603 41 0 79162 0
vsize: 316812
[startup+780.24 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72871 0 0 0 77851 182 0 0 25 0 1 0 477490369 324550656 71099 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79236 71099 603 41 0 79195 0
vsize: 316944
[startup+790.24 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72879 0 0 0 78851 182 0 0 25 0 1 0 477490369 324550656 71107 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79236 71107 603 41 0 79195 0
vsize: 316944
[startup+800.24 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72888 0 0 0 79851 182 0 0 25 0 1 0 477490369 324550656 71116 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79236 71116 603 41 0 79195 0
vsize: 316944
[startup+810.24 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72905 0 0 0 80851 183 0 0 25 0 1 0 477490369 324685824 71133 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79269 71133 603 41 0 79228 0
vsize: 317076
[startup+820.241 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72905 0 0 0 81851 183 0 0 25 0 1 0 477490369 324685824 71133 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79269 71133 603 41 0 79228 0
vsize: 317076
[startup+830.242 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72919 0 0 0 82852 183 0 0 25 0 1 0 477490369 324685824 71147 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79269 71147 603 41 0 79228 0
vsize: 317076
[startup+840.243 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72939 0 0 0 83852 183 0 0 25 0 1 0 477490369 324820992 71167 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79302 71167 603 41 0 79261 0
vsize: 317208
[startup+850.243 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72955 0 0 0 84852 183 0 0 25 0 1 0 477490369 324820992 71183 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79302 71183 603 41 0 79261 0
vsize: 317208
[startup+860.244 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72955 0 0 0 85852 183 0 0 25 0 1 0 477490369 324820992 71183 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79302 71183 603 41 0 79261 0
vsize: 317208
[startup+870.244 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 72980 0 0 0 86852 183 0 0 25 0 1 0 477490369 324956160 71208 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79335 71208 603 41 0 79294 0
vsize: 317340
[startup+880.245 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73000 0 0 0 87853 183 0 0 25 0 1 0 477490369 324956160 71228 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79335 71228 603 41 0 79294 0
vsize: 317340
[startup+890.246 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73008 0 0 0 88853 183 0 0 25 0 1 0 477490369 325091328 71236 4294967295 134512640 134672761 3221224544 3221223732 134556676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79368 71236 603 41 0 79327 0
vsize: 317472
[startup+900.246 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73014 0 0 0 89853 183 0 0 25 0 1 0 477490369 325091328 71242 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79368 71242 603 41 0 79327 0
vsize: 317472
[startup+910.246 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73033 0 0 0 90853 183 0 0 25 0 1 0 477490369 325091328 71261 4294967295 134512640 134672761 3221224544 3221223744 134561967 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79368 71261 603 41 0 79327 0
vsize: 317472
[startup+920.246 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73051 0 0 0 91853 183 0 0 25 0 1 0 477490369 325226496 71279 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 79401 71279 603 41 0 79360 0
vsize: 317604
[startup+930.247 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73051 0 0 0 92853 183 0 0 25 0 1 0 477490369 325226496 71279 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79401 71279 603 41 0 79360 0
vsize: 317604
[startup+940.248 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73056 0 0 0 93853 183 0 0 25 0 1 0 477490369 325226496 71284 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79401 71284 603 41 0 79360 0
vsize: 317604
[startup+950.248 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73083 0 0 0 94853 183 0 0 25 0 1 0 477490369 325361664 71311 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79434 71311 603 41 0 79393 0
vsize: 317736
[startup+960.248 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73100 0 0 0 95853 183 0 0 25 0 1 0 477490369 325361664 71328 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79434 71328 603 41 0 79393 0
vsize: 317736
[startup+970.249 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73105 0 0 0 96854 183 0 0 25 0 1 0 477490369 325496832 71333 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79467 71333 603 41 0 79426 0
vsize: 317868
[startup+980.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73116 0 0 0 97854 183 0 0 25 0 1 0 477490369 325496832 71344 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79467 71344 603 41 0 79426 0
vsize: 317868
[startup+990.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73121 0 0 0 98854 183 0 0 25 0 1 0 477490369 325496832 71349 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79467 71349 603 41 0 79426 0
vsize: 317868
[startup+1000.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73128 0 0 0 99854 183 0 0 25 0 1 0 477490369 325496832 71356 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79467 71356 603 41 0 79426 0
vsize: 317868
[startup+1010.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73146 0 0 0 100854 183 0 0 25 0 1 0 477490369 325632000 71374 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79500 71374 603 41 0 79459 0
vsize: 318000
[startup+1020.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73154 0 0 0 101855 183 0 0 25 0 1 0 477490369 325632000 71382 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79500 71382 603 41 0 79459 0
vsize: 318000
[startup+1030.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73158 0 0 0 102855 183 0 0 25 0 1 0 477490369 325632000 71386 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79500 71386 603 41 0 79459 0
vsize: 318000
[startup+1040.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73167 0 0 0 103855 183 0 0 25 0 1 0 477490369 325632000 71395 4294967295 134512640 134672761 3221224544 3221223716 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79500 71395 603 41 0 79459 0
vsize: 318000
[startup+1050.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73173 0 0 0 104855 183 0 0 25 0 1 0 477490369 325767168 71401 4294967295 134512640 134672761 3221224544 3221223716 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79533 71401 603 41 0 79492 0
vsize: 318132
[startup+1060.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73192 0 0 0 105855 183 0 0 25 0 1 0 477490369 325767168 71420 4294967295 134512640 134672761 3221224544 3221223760 134561948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79533 71420 603 41 0 79492 0
vsize: 318132
[startup+1070.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73210 0 0 0 106856 183 0 0 25 0 1 0 477490369 325902336 71438 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79566 71438 603 41 0 79525 0
vsize: 318264
[startup+1080.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73219 0 0 0 107856 183 0 0 25 0 1 0 477490369 325902336 71447 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79566 71447 603 41 0 79525 0
vsize: 318264
[startup+1090.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73229 0 0 0 108856 183 0 0 25 0 1 0 477490369 325902336 71457 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79566 71457 603 41 0 79525 0
vsize: 318264
[startup+1100.25 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73237 0 0 0 109856 183 0 0 25 0 1 0 477490369 325902336 71465 4294967295 134512640 134672761 3221224544 3221223724 134556590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79566 71465 603 41 0 79525 0
vsize: 318264
[startup+1110.26 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73242 0 0 0 110856 183 0 0 25 0 1 0 477490369 326037504 71470 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79599 71470 603 41 0 79558 0
vsize: 318396
[startup+1120.26 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73246 0 0 0 111856 183 0 0 25 0 1 0 477490369 326037504 71474 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79599 71474 603 41 0 79558 0
vsize: 318396
[startup+1130.26 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73253 0 0 0 112857 183 0 0 25 0 1 0 477490369 326037504 71481 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79599 71481 603 41 0 79558 0
vsize: 318396
[startup+1140.26 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73271 0 0 0 113857 183 0 0 25 0 1 0 477490369 326172672 71499 4294967295 134512640 134672761 3221224544 3221223760 134561993 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79632 71499 603 41 0 79591 0
vsize: 318528
[startup+1150.26 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73296 0 0 0 114857 183 0 0 25 0 1 0 477490369 326172672 71524 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79632 71524 603 41 0 79591 0
vsize: 318528
[startup+1160.26 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73314 0 0 0 115858 183 0 0 25 0 1 0 477490369 326307840 71542 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79665 71542 603 41 0 79624 0
vsize: 318660
[startup+1170.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73327 0 0 0 116859 183 0 0 25 0 1 0 477490369 326307840 71555 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79665 71555 603 41 0 79624 0
vsize: 318660
[startup+1180.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73334 0 0 0 117859 183 0 0 25 0 1 0 477490369 326307840 71562 4294967295 134512640 134672761 3221224544 3221223728 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79665 71562 603 41 0 79624 0
vsize: 318660
[startup+1190.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73342 0 0 0 118859 183 0 0 25 0 1 0 477490369 326443008 71570 4294967295 134512640 134672761 3221224544 3221223744 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79698 71570 603 41 0 79657 0
vsize: 318792
[startup+1200.27 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 10443
Raw data (stat): 10443 (minisat+) R 10442 26667 26666 0 -1 0 73350 0 0 0 119859 183 0 0 25 0 1 0 477490369 326443008 71578 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79698 71578 603 41 0 79657 0
vsize: 318792
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.42 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 10443
Raw data (stat): 10443 (minisat+) Z 10442 26667 26666 0 -1 12 73352 0 0 0 119859 198 0 0 25 0 1 0 477490369 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.42
CPU time (s): 1200.58
CPU user time (s): 1198.6
CPU system time (s): 1.9807
CPU usage (%): 100.013
Max. virtual memory (Kb): 318792
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####