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/MIPLIB/miplib2003/normalized-mps-v2-13-7-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.34
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 18863

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        839644 kB
Buffers:          5464 kB
Cached:         162060 kB
SwapCached:         28 kB
Active:          58424 kB
Inactive:       111924 kB
HighTotal:      131008 kB
HighFree:         5292 kB
LowTotal:       903652 kB
LowFree:        834352 kB
SwapTotal:     2097892 kB
SwapFree:      2097796 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6800 kB
Slab:            18920 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:08:52 (client local time) WITH STATUS 0 IN 1200.33 SECONDS
stats: 18067 7 1200.33 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.92 0.97 0.92 2/54 22620
Raw data (stat): 22620 (runsolver) R 22619 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546640703 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.93 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 30585 0 0 0 922 77 0 0 25 0 1 0 546640703 131055616 28813 4294967295 134512640 134672761 3221224544 3221220040 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31996 28814 603 41 0 31955 0
vsize: 127984
[startup+20.0015 s]
Raw data (loadavg): 0.94 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72225 0 0 0 1829 170 0 0 25 0 1 0 546640703 321921024 70453 4294967295 134512640 134672761 3221224544 3221223844 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70453 603 41 0 78553 0
vsize: 314376
[startup+30.0026 s]
Raw data (loadavg): 0.95 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72238 0 0 0 2828 170 0 0 25 0 1 0 546640703 321921024 70466 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70466 603 41 0 78553 0
vsize: 314376
[startup+40.0034 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72239 0 0 0 3829 170 0 0 25 0 1 0 546640703 321921024 70467 4294967295 134512640 134672761 3221224544 3221223716 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70467 603 41 0 78553 0
vsize: 314376
[startup+50.0039 s]
Raw data (loadavg): 0.96 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72247 0 0 0 4829 170 0 0 25 0 1 0 546640703 321921024 70475 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70475 603 41 0 78553 0
vsize: 314376
[startup+60.0039 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72247 0 0 0 5829 170 0 0 25 0 1 0 546640703 321921024 70475 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70475 603 41 0 78553 0
vsize: 314376
[startup+70.0037 s]
Raw data (loadavg): 0.97 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72248 0 0 0 6829 170 0 0 25 0 1 0 546640703 321921024 70476 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70476 603 41 0 78553 0
vsize: 314376
[startup+80.0042 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72248 0 0 0 7829 170 0 0 25 0 1 0 546640703 321921024 70476 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70476 603 41 0 78553 0
vsize: 314376
[startup+90.0043 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72248 0 0 0 8829 170 0 0 25 0 1 0 546640703 321921024 70476 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70476 603 41 0 78553 0
vsize: 314376
[startup+100.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72248 0 0 0 9830 170 0 0 25 0 1 0 546640703 321921024 70476 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70476 603 41 0 78553 0
vsize: 314376
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72249 0 0 0 10830 170 0 0 25 0 1 0 546640703 321921024 70477 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70477 603 41 0 78553 0
vsize: 314376
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72249 0 0 0 11830 170 0 0 25 0 1 0 546640703 321921024 70477 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72249 0 0 0 12830 170 0 0 25 0 1 0 546640703 321921024 70477 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70477 603 41 0 78553 0
vsize: 314376
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72250 0 0 0 13830 170 0 0 25 0 1 0 546640703 321921024 70478 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70478 603 41 0 78553 0
vsize: 314376
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72250 0 0 0 14830 170 0 0 25 0 1 0 546640703 321921024 70478 4294967295 134512640 134672761 3221224544 3221223716 134556682 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72250 0 0 0 15830 170 0 0 25 0 1 0 546640703 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.007 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72250 0 0 0 16830 170 0 0 25 0 1 0 546640703 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+180.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72251 0 0 0 17831 170 0 0 25 0 1 0 546640703 321921024 70479 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72251 0 0 0 18831 170 0 0 25 0 1 0 546640703 321921024 70479 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72251 0 0 0 19831 170 0 0 25 0 1 0 546640703 321921024 70479 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.008 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72256 0 0 0 20831 170 0 0 25 0 1 0 546640703 321921024 70484 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.009 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72258 0 0 0 21831 170 0 0 25 0 1 0 546640703 321921024 70486 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78594 70486 603 41 0 78553 0
vsize: 314376
[startup+230.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72266 0 0 0 22831 170 0 0 25 0 1 0 546640703 321921024 70494 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72280 0 0 0 23831 171 0 0 25 0 1 0 546640703 322056192 70508 4294967295 134512640 134672761 3221224544 3221223716 134556606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78627 70508 603 41 0 78586 0
vsize: 314508
[startup+250.01 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72288 0 0 0 24831 171 0 0 25 0 1 0 546640703 322056192 70516 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72298 0 0 0 25831 171 0 0 25 0 1 0 546640703 322056192 70526 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78627 70526 603 41 0 78586 0
vsize: 314508
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72311 0 0 0 26831 171 0 0 25 0 1 0 546640703 322191360 70539 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72313 0 0 0 27831 171 0 0 25 0 1 0 546640703 322191360 70541 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78660 70541 603 41 0 78619 0
vsize: 314640
[startup+290.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72323 0 0 0 28832 171 0 0 25 0 1 0 546640703 322191360 70551 4294967295 134512640 134672761 3221224544 3221223716 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78660 70551 603 41 0 78619 0
vsize: 314640
[startup+300.012 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72331 0 0 0 29832 172 0 0 25 0 1 0 546640703 322191360 70559 4294967295 134512640 134672761 3221224544 3221223716 134556632 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.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72338 0 0 0 30832 172 0 0 25 0 1 0 546640703 322191360 70566 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72340 0 0 0 31832 172 0 0 25 0 1 0 546640703 322326528 70568 4294967295 134512640 134672761 3221224544 3221223728 134556589 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72352 0 0 0 32832 172 0 0 25 0 1 0 546640703 322326528 70580 4294967295 134512640 134672761 3221224544 3221223760 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78693 70580 603 41 0 78652 0
vsize: 314772
[startup+340.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72365 0 0 0 33832 172 0 0 25 0 1 0 546640703 322326528 70593 4294967295 134512640 134672761 3221224544 3221223716 134556639 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72367 0 0 0 34832 172 0 0 25 0 1 0 546640703 322461696 70595 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72384 0 0 0 35832 172 0 0 25 0 1 0 546640703 322461696 70612 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 78726 70612 603 41 0 78685 0
vsize: 314904
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72405 0 0 0 36832 172 0 0 25 0 1 0 546640703 322596864 70633 4294967295 134512640 134672761 3221224544 3221223728 134556675 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.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72410 0 0 0 37832 172 0 0 25 0 1 0 546640703 322596864 70638 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72416 0 0 0 38832 172 0 0 25 0 1 0 546640703 322596864 70644 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72423 0 0 0 39832 172 0 0 25 0 1 0 546640703 322596864 70651 4294967295 134512640 134672761 3221224544 3221223716 134556596 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72426 0 0 0 40832 172 0 0 25 0 1 0 546640703 322596864 70654 4294967295 134512640 134672761 3221224544 3221223752 134561960 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72437 0 0 0 41832 172 0 0 25 0 1 0 546640703 322732032 70665 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72449 0 0 0 42832 173 0 0 25 0 1 0 546640703 322732032 70677 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78792 70677 603 41 0 78751 0
vsize: 315168
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72462 0 0 0 43833 173 0 0 25 0 1 0 546640703 322732032 70690 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78792 70690 603 41 0 78751 0
vsize: 315168
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72476 0 0 0 44833 173 0 0 25 0 1 0 546640703 322867200 70704 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72476 0 0 0 45833 173 0 0 25 0 1 0 546640703 322867200 70704 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72493 0 0 0 46833 173 0 0 25 0 1 0 546640703 322867200 70721 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72502 0 0 0 47833 173 0 0 25 0 1 0 546640703 323002368 70730 4294967295 134512640 134672761 3221224544 3221223716 134556651 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72524 0 0 0 48833 173 0 0 25 0 1 0 546640703 323002368 70752 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78858 70752 603 41 0 78817 0
vsize: 315432
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72538 0 0 0 49833 173 0 0 25 0 1 0 546640703 323137536 70766 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78891 70766 603 41 0 78850 0
vsize: 315564
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72539 0 0 0 50833 173 0 0 25 0 1 0 546640703 323137536 70767 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72554 0 0 0 51834 173 0 0 25 0 1 0 546640703 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72566 0 0 0 52834 173 0 0 25 0 1 0 546640703 323137536 70794 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72580 0 0 0 53834 173 0 0 25 0 1 0 546640703 323272704 70808 4294967295 134512640 134672761 3221224544 3221223760 134561987 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.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72580 0 0 0 54834 173 0 0 25 0 1 0 546640703 323272704 70808 4294967295 134512640 134672761 3221224544 3221223716 134556632 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72582 0 0 0 55833 173 0 0 25 0 1 0 546640703 323272704 70810 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78924 70810 603 41 0 78883 0
vsize: 315696
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72605 0 0 0 56834 173 0 0 25 0 1 0 546640703 323407872 70833 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 78957 70833 603 41 0 78916 0
vsize: 315828
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72620 0 0 0 57834 174 0 0 25 0 1 0 546640703 323407872 70848 4294967295 134512640 134672761 3221224544 3221223716 134556643 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72638 0 0 0 58834 174 0 0 25 0 1 0 546640703 323543040 70866 4294967295 134512640 134672761 3221224544 3221223744 134561967 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72656 0 0 0 59834 174 0 0 25 0 1 0 546640703 323543040 70884 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72661 0 0 0 60834 174 0 0 25 0 1 0 546640703 323543040 70889 4294967295 134512640 134672761 3221224544 3221223732 134556676 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72667 0 0 0 61834 174 0 0 25 0 1 0 546640703 323543040 70895 4294967295 134512640 134672761 3221224544 3221223728 134556675 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.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72669 0 0 0 62834 174 0 0 25 0 1 0 546640703 323678208 70897 4294967295 134512640 134672761 3221224544 3221223724 134556590 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.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72677 0 0 0 63834 174 0 0 25 0 1 0 546640703 323678208 70905 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79023 70905 603 41 0 78982 0
vsize: 316092
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72698 0 0 0 64835 174 0 0 25 0 1 0 546640703 323678208 70926 4294967295 134512640 134672761 3221224544 3221223728 134556589 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.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72702 0 0 0 65835 174 0 0 25 0 1 0 546640703 323813376 70930 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 22620
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72727 0 0 0 66835 174 0 0 25 0 1 0 546640703 323813376 70955 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79056 70955 603 41 0 79015 0
vsize: 316224
[startup+680.018 s]
Raw data (loadavg): 1.07 0.99 0.93 2/54 22673
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72753 0 0 0 67835 174 0 0 25 0 1 0 546640703 323948544 70981 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79089 70981 603 41 0 79048 0
vsize: 316356
[startup+690.018 s]
Raw data (loadavg): 1.06 0.99 0.93 2/54 22673
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72767 0 0 0 68835 175 0 0 25 0 1 0 546640703 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+700.018 s]
Raw data (loadavg): 1.05 0.99 0.93 2/54 22673
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72767 0 0 0 69835 175 0 0 25 0 1 0 546640703 323948544 70995 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.019 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 22673
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72782 0 0 0 70835 175 0 0 25 0 1 0 546640703 324083712 71010 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.019 s]
Raw data (loadavg): 1.04 0.99 0.93 2/54 22673
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72794 0 0 0 71835 175 0 0 25 0 1 0 546640703 324083712 71022 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.019 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 22673
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72812 0 0 0 72835 175 0 0 25 0 1 0 546640703 324218880 71040 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79155 71040 603 41 0 79114 0
vsize: 316620
[startup+740.019 s]
Raw data (loadavg): 1.03 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72835 0 0 0 73835 175 0 0 25 0 1 0 546640703 324415488 71063 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.019 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72844 0 0 0 74836 175 0 0 25 0 1 0 546640703 324415488 71072 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79203 71072 603 41 0 79162 0
vsize: 316812
[startup+760.02 s]
Raw data (loadavg): 1.02 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72854 0 0 0 75836 175 0 0 25 0 1 0 546640703 324415488 71082 4294967295 134512640 134672761 3221224544 3221223716 134556651 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.02 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72858 0 0 0 76836 175 0 0 25 0 1 0 546640703 324415488 71086 4294967295 134512640 134672761 3221224544 3221223760 134561997 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.019 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72871 0 0 0 77836 175 0 0 25 0 1 0 546640703 324550656 71099 4294967295 134512640 134672761 3221224544 3221223736 134556585 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.019 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72881 0 0 0 78836 175 0 0 25 0 1 0 546640703 324550656 71109 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79236 71109 603 41 0 79195 0
vsize: 316944
[startup+800.019 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72888 0 0 0 79836 175 0 0 25 0 1 0 546640703 324550656 71116 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.02 s]
Raw data (loadavg): 1.01 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72905 0 0 0 80837 175 0 0 25 0 1 0 546640703 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+820.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72905 0 0 0 81837 175 0 0 25 0 1 0 546640703 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+830.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72919 0 0 0 82837 175 0 0 25 0 1 0 546640703 324685824 71147 4294967295 134512640 134672761 3221224544 3221223716 134556639 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.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72939 0 0 0 83837 175 0 0 25 0 1 0 546640703 324820992 71167 4294967295 134512640 134672761 3221224544 3221223716 134556602 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.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72955 0 0 0 84836 176 0 0 25 0 1 0 546640703 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72955 0 0 0 85836 176 0 0 25 0 1 0 546640703 324820992 71183 4294967295 134512640 134672761 3221224544 3221223716 134556682 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 72980 0 0 0 86836 176 0 0 25 0 1 0 546640703 324956160 71208 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.019 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73000 0 0 0 87836 176 0 0 25 0 1 0 546640703 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73008 0 0 0 88837 176 0 0 25 0 1 0 546640703 325091328 71236 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73014 0 0 0 89837 176 0 0 25 0 1 0 546640703 325091328 71242 4294967295 134512640 134672761 3221224544 3221223716 134556653 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.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73033 0 0 0 90837 176 0 0 25 0 1 0 546640703 325091328 71261 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73051 0 0 0 91836 177 0 0 25 0 1 0 546640703 325226496 71279 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79401 71279 603 41 0 79360 0
vsize: 317604
[startup+930.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73051 0 0 0 92836 177 0 0 25 0 1 0 546640703 325226496 71279 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73056 0 0 0 93836 177 0 0 25 0 1 0 546640703 325226496 71284 4294967295 134512640 134672761 3221224544 3221223748 134561964 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.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73083 0 0 0 94836 177 0 0 25 0 1 0 546640703 325361664 71311 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73100 0 0 0 95836 177 0 0 25 0 1 0 546640703 325361664 71328 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73105 0 0 0 96836 178 0 0 25 0 1 0 546640703 325496832 71333 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.021 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73116 0 0 0 97837 178 0 0 25 0 1 0 546640703 325496832 71344 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.022 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73121 0 0 0 98837 178 0 0 25 0 1 0 546640703 325496832 71349 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73128 0 0 0 99837 178 0 0 25 0 1 0 546640703 325496832 71356 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22675
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73146 0 0 0 100837 178 0 0 25 0 1 0 546640703 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73154 0 0 0 101837 178 0 0 25 0 1 0 546640703 325632000 71382 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73158 0 0 0 102837 178 0 0 25 0 1 0 546640703 325632000 71386 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73167 0 0 0 103837 178 0 0 25 0 1 0 546640703 325632000 71395 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73173 0 0 0 104838 178 0 0 25 0 1 0 546640703 325767168 71401 4294967295 134512640 134672761 3221224544 3221223716 134556682 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73192 0 0 0 105838 178 0 0 25 0 1 0 546640703 325767168 71420 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73210 0 0 0 106838 178 0 0 25 0 1 0 546640703 325902336 71438 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73219 0 0 0 107838 178 0 0 25 0 1 0 546640703 325902336 71447 4294967295 134512640 134672761 3221224544 3221223760 134561948 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.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73229 0 0 0 108838 178 0 0 25 0 1 0 546640703 325902336 71457 4294967295 134512640 134672761 3221224544 3221223716 134556649 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73237 0 0 0 109838 178 0 0 25 0 1 0 546640703 325902336 71465 4294967295 134512640 134672761 3221224544 3221223716 134556667 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73242 0 0 0 110838 178 0 0 25 0 1 0 546640703 326037504 71470 4294967295 134512640 134672761 3221224544 3221223760 134561993 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73246 0 0 0 111839 178 0 0 25 0 1 0 546640703 326037504 71474 4294967295 134512640 134672761 3221224544 3221223716 134556598 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73253 0 0 0 112839 178 0 0 25 0 1 0 546640703 326037504 71481 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73271 0 0 0 113839 178 0 0 25 0 1 0 546640703 326172672 71499 4294967295 134512640 134672761 3221224544 3221223716 134556634 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.02 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73296 0 0 0 114839 178 0 0 25 0 1 0 546640703 326172672 71524 4294967295 134512640 134672761 3221224544 3221223744 134561972 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.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73314 0 0 0 115839 179 0 0 25 0 1 0 546640703 326307840 71542 4294967295 134512640 134672761 3221224544 3221223716 134556688 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.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73327 0 0 0 116839 179 0 0 25 0 1 0 546640703 326307840 71555 4294967295 134512640 134672761 3221224544 3221223716 134556639 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.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73334 0 0 0 117839 179 0 0 25 0 1 0 546640703 326307840 71562 4294967295 134512640 134672761 3221224544 3221223760 134561948 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.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73350 0 0 0 118839 179 0 0 25 0 1 0 546640703 326443008 71578 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 79698 71578 603 41 0 79657 0
vsize: 318792
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.93 2/54 22677
Raw data (stat): 22620 (minisat+) R 22619 11931 11930 0 -1 0 73350 0 0 0 119839 179 0 0 25 0 1 0 546640703 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.17 s]
Raw data (loadavg): 1.00 0.99 0.93 1/54 22677
Raw data (stat): 22620 (minisat+) Z 22619 11931 11930 0 -1 12 73352 0 0 0 119840 193 0 0 25 0 1 0 546640703 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.17
CPU time (s): 1200.33
CPU user time (s): 1198.4
CPU system time (s): 1.93271
CPU usage (%): 100.014
Max. virtual memory (Kb): 318792
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####