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/submitted/manquinho/routing/normalized-s4-4-3-9pb.opb
MD5SUM	7d64f372313e74de659e9e56ab2d9bab
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	68
Optimality of the best value was proved	NO
Number of terms in the objective function	840
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	840
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	3
Number of bits of the biggest number in a constraint	2
Biggest sum of numbers in a constraint	840
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.04684
Number of variables	840
Total number of constraints	2526
Number of constraints which are clauses	2502
Number of constraints which are cardinality constraints (but not clauses)	24
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	35
Trace number 5567

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc9 THE 2005-04-14 00:36:56 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4005 boxname=wulflinc9 idbench=245 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7d64f372313e74de659e9e56ab2d9bab  /oldhome/oroussel/tmp/wulflinc9/normalized-s4-4-3-9pb.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc9/normalized-s4-4-3-9pb.opb /oldhome/oroussel/tmp/wulflinc9/normalized-s4-4-3-9pb.opb
IDLAUNCH: 4005
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
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:        906144 kB
Buffers:         35276 kB
Cached:          73232 kB
SwapCached:        564 kB
Active:          52912 kB
Inactive:        59028 kB
HighTotal:      131008 kB
HighFree:        53872 kB
LowTotal:       903652 kB
LowFree:        852272 kB
SwapTotal:     2097136 kB
SwapFree:      2096572 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10956 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:47:38 (client local time) WITH STATUS 30 IN 642.774 SECONDS
stats: 4005 0 642.774 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 2526 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ############################################################################################################################################
c   -- Clauses(.)/Splits(s): ..............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[2520]---> BDD-cost:    1
c ---[2503]---> BDD-cost:    1
c ---[2465]---> BDD-cost:    1
c ---[2455]---> BDD-cost:    1
c ---[2449]---> BDD-cost:    1
c ---[2431]---> BDD-cost:    1
c ---[2393]---> BDD-cost:    1
c ---[2383]---> BDD-cost:    1
c ---[2377]---> BDD-cost:    1
c ---[2359]---> BDD-cost:    1
c ---[2321]---> BDD-cost:    1
c ---[2311]---> BDD-cost:    1
c ---[2309]---> BDD-cost:    1
c ---[2283]---> BDD-cost:    1
c ---[2265]---> BDD-cost:    1
c ---[2239]---> BDD-cost:    1
c ---[2206]---> BDD-cost:    1
c ---[2180]---> BDD-cost:    1
c ---[2178]---> BDD-cost:    1
c ---[2168]---> BDD-cost:    1
c ---[2151]---> BDD-cost:    1
c ---[2129]---> BDD-cost:    1
c ---[2103]---> BDD-cost:    1
c ---[2097]---> BDD-cost:    1
c ---[2079]---> BDD-cost:    1
c ---[2057]---> BDD-cost:    1
c ---[2031]---> BDD-cost:    1
c ---[2025]---> BDD-cost:    1
c ---[2007]---> BDD-cost:    1
c ---[1985]---> BDD-cost:    1
c ---[1959]---> BDD-cost:    1
c ---[1953]---> BDD-cost:    1
c ---[1935]---> BDD-cost:    1
c ---[1913]---> BDD-cost:    1
c ---[1887]---> BDD-cost:    1
c ---[1881]---> BDD-cost:    1
c ---[1871]---> BDD-cost:    1
c ---[1861]---> BDD-cost:    1
c ---[1812]---> BDD-cost:    1
c ---[1810]---> BDD-cost:    1
c ---[1758]---> BDD-cost:    1
c ---[1748]---> BDD-cost:    1
c ---[1742]---> BDD-cost:    1
c ---[1740]---> BDD-cost:    1
c ---[1692]---> BDD-cost:    1
c ---[1682]---> BDD-cost:    1
c ---[1672]---> BDD-cost:    1
c ---[1670]---> BDD-cost:    1
c ---[1664]---> BDD-cost:    1
c ---[1646]---> BDD-cost:    1
c ---[1609]---> BDD-cost:    1
c ---[1599]---> BDD-cost:    1
c ---[1593]---> BDD-cost:    1
c ---[1575]---> BDD-cost:    1
c ---[1537]---> BDD-cost:    1
c ---[1527]---> BDD-cost:    1
c ---[1513]---> BDD-cost:    1
c ---[1487]---> BDD-cost:    1
c ---[1465]---> BDD-cost:    1
c ---[1455]---> BDD-cost:    1
c ---[1422]---> BDD-cost:    1
c ---[1396]---> BDD-cost:    1
c ---[1394]---> BDD-cost:    1
c ---[1384]---> BDD-cost:    1
c ---[1378]---> BDD-cost:    1
c ---[1360]---> BDD-cost:    1
c ---[1322]---> BDD-cost:    1
c ---[1312]---> BDD-cost:    1
c ---[1298]---> BDD-cost:    1
c ---[1272]---> BDD-cost:    1
c ---[1250]---> BDD-cost:    1
c ---[1240]---> BDD-cost:    1
c ---[1234]---> BDD-cost:    1
c ---[1216]---> BDD-cost:    1
c ---[1178]---> BDD-cost:    1
c ---[1168]---> BDD-cost:    1
c ---[1135]---> BDD-cost:    1
c ---[1109]---> BDD-cost:    1
c ---[1107]---> BDD-cost:    1
c ---[1097]---> BDD-cost:    1
c ---[1079]---> BDD-cost:    1
c ---[1057]---> BDD-cost:    1
c ---[1031]---> BDD-cost:    1
c ---[1025]---> BDD-cost:    1
c ---[1007]---> BDD-cost:    1
c ---[ 985]---> BDD-cost:    1
c ---[ 959]---> BDD-cost:    1
c ---[ 953]---> BDD-cost:    1
c ---[ 935]---> BDD-cost:    1
c ---[ 913]---> BDD-cost:    1
c ---[ 887]---> BDD-cost:    1
c ---[ 881]---> BDD-cost:    1
c ---[ 875]---> BDD-cost:    1
c ---[ 858]---> BDD-cost:    1
c ---[ 820]---> BDD-cost:    1
c ---[ 810]---> BDD-cost:    1
c ---[ 808]---> BDD-cost:    1
c ---[ 782]---> BDD-cost:    1
c ---[ 764]---> BDD-cost:    1
c ---[ 738]---> BDD-cost:    1
c ---[ 724]---> BDD-cost:    1
c ---[ 698]---> BDD-cost:    1
c ---[ 676]---> BDD-cost:    1
c ---[ 666]---> BDD-cost:    1
c ---[ 652]---> BDD-cost:    1
c ---[ 627]---> BDD-cost:    1
c ---[ 605]---> BDD-cost:    1
c ---[ 595]---> BDD-cost:    1
c ---[ 593]---> BDD-cost:    1
c ---[ 567]---> BDD-cost:    1
c ---[ 549]---> BDD-cost:    1
c ---[ 523]---> BDD-cost:    1
c ---[ 521]---> BDD-cost:    1
c ---[ 495]---> BDD-cost:    1
c ---[ 477]---> BDD-cost:    1
c ---[ 451]---> BDD-cost:    1
c ---[ 438]---> BDD-cost:    1
c ---[ 412]---> BDD-cost:    1
c ---[ 390]---> BDD-cost:    1
c ---[ 380]---> BDD-cost:    1
c ---[ 378]---> BDD-cost:    1
c ---[ 352]---> BDD-cost:    1
c ---[ 334]---> BDD-cost:    1
c ---[ 308]---> BDD-cost:    1
c ---[ 306]---> BDD-cost:    1
c ---[ 280]---> BDD-cost:    1
c ---[ 262]---> BDD-cost:    1
c ---[ 236]---> BDD-cost:    1
c ---[ 188]---> BDD-cost:    1
c ---[ 178]---> BDD-cost:    1
c ---[ 168]---> BDD-cost:    1
c ---[ 166]---> BDD-cost:    1
c ---[ 156]---> BDD-cost:    1
c ---[ 146]---> BDD-cost:    1
c ---[  96]---> BDD-cost:    1
c ---[  94]---> BDD-cost:    1
c ---[  42]---> BDD-cost:    1
c ---[  32]---> BDD-cost:    1
c ---[  26]---> BDD-cost:    1
c ---[  24]---> BDD-cost:    1
c ---[  23]---> BDD-cost:  127
c ---[  22]---> BDD-cost:  127
c ---[  21]---> BDD-cost:  127
c ---[  20]---> BDD-cost:  127
c ---[  19]---> BDD-cost:  127
c ---[  18]---> BDD-cost:  127
c ---[  17]---> BDD-cost:  127
c ---[  16]---> BDD-cost:  127
c ---[  15]---> BDD-cost:  127
c ---[  14]---> BDD-cost:  127
c ---[  13]---> BDD-cost:  127
c ---[  12]---> BDD-cost:  127
c ---[  11]---> BDD-cost:  127
c ---[  10]---> BDD-cost:  127
c ---[   9]---> BDD-cost:  127
c ---[   8]---> BDD-cost:  127
c ---[   7]---> BDD-cost:  127
c ---[   6]---> BDD-cost:  127
c ---[   5]---> BDD-cost:  127
c ---[   4]---> BDD-cost:  127
c ---[   3]---> BDD-cost:  127
c ---[   2]---> BDD-cost:  127
c ---[   1]---> BDD-cost:  127
c ---[   0]---> BDD-cost:  127
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   10758    31070 |    3227       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3864          
c   -- var.elim.:  2000/3864          
c   -- var.elim.:  3000/3864          
c   -- var.elim.:  3864/3864          
c   -- var.elim.:  336/336          
c   -- subsuming                       
c   -- var.elim.:  216/216          
c   -- var.elim.:  264/264          
c   -- subsuming                       
c |         0 |   10614    30574 |      --       0       --      -- |     --   | -144/-144
c |         0 |   10614    30574 |    4245       0        0     nan |  0.000 % |
c |       101 |   10614    30574 |    4670     101     1809    17.9 |  4.222 % |
c |       251 |   10614    30574 |    5137     251     6151    24.5 |  4.222 % |
c |       477 |   10614    30574 |    5650     477    11983    25.1 |  4.222 % |
c |       814 |   10614    30574 |    6215     814    37996    46.7 |  4.222 % |
c |      1321 |   10614    30574 |    6837    1321    62344    47.2 |  4.222 % |
c |      2083 |   10614    30574 |    7521    2083   124513    59.8 |  4.222 % |
c |      3222 |   10614    30574 |    8273    3222   232075    72.0 |  4.222 % |
c |      4932 |   10614    30574 |    9100    4932   375737    76.2 |  4.222 % |
c |      7495 |   10614    30574 |   10010    7495   574057    76.6 |  4.222 % |
c |     11341 |   10614    30574 |   11011    7859   585167    74.5 |  4.222 % |
c |     17109 |   10614    30574 |   12113    9683   781027    80.7 |  4.222 % |
c |     25758 |   10614    30574 |   13324   10012  1008941   100.8 |  4.222 % |
c |     38733 |   10614    30574 |   14656    9154   690335    75.4 |  4.222 % |
c ==============================================================================
c (current CPU-time: 30.6673 s)
c ==============================================================================
c [1mFound solution: 70[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:38902     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     50817 |   55089   134223 |   16526   11147   736099    66.0 |  4.222 % |
c   -- subsuming                       
c   -- var.elim.:  1000/29946          
c   -- var.elim.:  2000/29946          
c   -- var.elim.:  3000/29946          
c   -- var.elim.:  4000/29946          
c   -- var.elim.:  5000/29946          
c   -- var.elim.:  6000/29946          
c   -- var.elim.:  7000/29946          
c   -- var.elim.:  8000/29946          
c   -- var.elim.:  9000/29946          
c   -- var.elim.:  10000/29946          
c   -- var.elim.:  11000/29946          
c   -- var.elim.:  12000/29946          
c   -- var.elim.:  13000/29946          
c   -- var.elim.:  14000/29946          
c   -- var.elim.:  15000/29946          
c   -- var.elim.:  16000/29946          
c   -- var.elim.:  17000/29946          
c   -- var.elim.:  18000/29946          
c   -- var.elim.:  19000/29946          
c   -- var.elim.:  20000/29946          
c   -- var.elim.:  21000/29946          
c   -- var.elim.:  22000/29946          
c   -- var.elim.:  23000/29946          
c   -- var.elim.:  24000/29946          
c   -- var.elim.:  25000/29946          
c   -- var.elim.:  26000/29946          
c   -- var.elim.:  27000/29946          
c   -- var.elim.:  28000/29946          
c   -- var.elim.:  29000/29946          
c   -- var.elim.:  29946/29946          
c   -- var.elim.:  1000/14813          
c   -- var.elim.:  2000/14813          
c   -- var.elim.:  3000/14813          
c   -- var.elim.:  4000/14813          
c   -- var.elim.:  5000/14813          
c   -- var.elim.:  6000/14813          
c   -- var.elim.:  7000/14813          
c   -- var.elim.:  8000/14813          
c   -- var.elim.:  9000/14813          
c   -- var.elim.:  10000/14813          
c   -- var.elim.:  11000/14813          
c   -- var.elim.:  12000/14813          
c   -- var.elim.:  13000/14813          
c   -- var.elim.:  14000/14813          
c   -- var.elim.:  14813/14813          
c   -- var.elim.:  1000/3911          
c   -- var.elim.:  2000/3911          
c   -- var.elim.:  3000/3911          
c   -- var.elim.:  3911/3911          
c   -- var.elim.:  1000/6293          
c   -- var.elim.:  2000/6293          
c   -- var.elim.:  3000/6293          
c   -- var.elim.:  4000/6293          
c   -- var.elim.:  5000/6293          
c   -- var.elim.:  6000/6293          
c   -- var.elim.:  6293/6293          
c   -- var.elim.:  1000/5347          
c   -- var.elim.:  2000/5347          
c   -- var.elim.:  3000/5347          
c   -- var.elim.:  4000/5347          
c   -- var.elim.:  5000/5347          
c   -- var.elim.:  5347/5347          
c   -- var.elim.:  1000/2348          
c   -- var.elim.:  2000/2348          
c   -- var.elim.:  2348/2348          
c   -- subsuming                       
c   -- var.elim.:  1000/12820          
c   -- var.elim.:  2000/12820          
c   -- var.elim.:  3000/12820          
c   -- var.elim.:  4000/12820          
c   -- var.elim.:  5000/12820          
c   -- var.elim.:  6000/12820          
c   -- var.elim.:  7000/12820          
c   -- var.elim.:  8000/12820          
c   -- var.elim.:  9000/12820          
c   -- var.elim.:  10000/12820          
c   -- var.elim.:  11000/12820          
c   -- var.elim.:  12000/12820          
c   -- var.elim.:  12820/12820          
c   -- var.elim.:  1000/5512          
c   -- var.elim.:  2000/5512          
c   -- var.elim.:  3000/5512          
c   -- var.elim.:  4000/5512          
c   -- var.elim.:  5000/5512          
c   -- var.elim.:  5512/5512          
c   -- var.elim.:  1000/6634          
c   -- var.elim.:  2000/6634          
c   -- var.elim.:  3000/6634          
c   -- var.elim.:  4000/6634          
c   -- var.elim.:  5000/6634          
c   -- var.elim.:  6000/6634          
c   -- var.elim.:  6634/6634          
c   -- var.elim.:  1000/7259          
c   -- var.elim.:  2000/7259          
c   -- var.elim.:  3000/7259          
c   -- var.elim.:  4000/7259          
c   -- var.elim.:  5000/7259          
c   -- var.elim.:  6000/7259          
c   -- var.elim.:  7000/7259          
c   -- var.elim.:  7259/7259          
c   -- var.elim.:  1000/1313          
c   -- var.elim.:  1313/1313          
c   -- subsuming                       
c   -- var.elim.:  1000/7369          
c   -- var.elim.:  2000/7369          
c   -- var.elim.:  3000/7369          
c   -- var.elim.:  4000/7369          
c   -- var.elim.:  5000/7369          
c   -- var.elim.:  6000/7369          
c   -- var.elim.:  7000/7369          
c   -- var.elim.:  7369/7369          
c   -- var.elim.:  1000/4656          
c   -- var.elim.:  2000/4656          
c   -- var.elim.:  3000/4656          
c   -- var.elim.:  4000/4656          
c   -- var.elim.:  4656/4656          
c   -- var.elim.:  1000/3553          
c   -- var.elim.:  2000/3553          
c   -- var.elim.:  3000/3553          
c   -- var.elim.:  3553/3553          
c   -- var.elim.:  1000/3503          
c   -- var.elim.:  2000/3503          
c   -- var.elim.:  3000/3503          
c   -- var.elim.:  3503/3503          
c   -- var.elim.:  1000/1062          
c   -- var.elim.:  1062/1062          
c   -- subsuming                       
c   -- var.elim.:  1000/4589          
c   -- var.elim.:  2000/4589          
c   -- var.elim.:  3000/4589          
c   -- var.elim.:  4000/4589          
c   -- var.elim.:  4589/4589          
c   -- var.elim.:  1000/2306          
c   -- var.elim.:  2000/2306          
c   -- var.elim.:  2306/2306          
c   -- var.elim.:  1000/1196          
c   -- var.elim.:  1196/1196          
c   -- var.elim.:  952/952          
c   -- subsuming                       
c   -- var.elim.:  1000/2261          
c   -- var.elim.:  2000/2261          
c   -- var.elim.:  2261/2261          
c   -- var.elim.:  1000/1942          
c   -- var.elim.:  1942/1942          
c |     50817 |   38611   217736 |      --   11147       --      -- |     --   | -16466/83549
c |     50817 |   38611   217736 |   15444   11147   736099    66.0 |  4.222 % |
c |     50917 |   38611   217736 |   16988   11247   742807    66.0 |  1.046 % |
c |     51069 |   38611   217736 |   18687   11399   748618    65.7 |  1.046 % |
c |     51296 |   38611   217736 |   20556   11626   759816    65.4 |  1.046 % |
c |     51633 |   38611   217736 |   22612   11963   777172    65.0 |  1.046 % |
c |     52139 |   38611   217736 |   24873   12469   818152    65.6 |  1.046 % |
c |     52899 |   38611   217736 |   27360   13229   885544    66.9 |  1.046 % |
c |     54042 |   38611   217736 |   30096   14372   967967    67.4 |  1.046 % |
c |     55757 |   38611   217736 |   33106   16087  1117650    69.5 |  1.046 % |
c |     58320 |   38611   217736 |   36417   18650  1382285    74.1 |  1.046 % |
c |     62168 |   38547   217395 |   39992   22488  1692053    75.2 |  1.070 % |
c |     67935 |   38511   217179 |   43950   28222  2234672    79.2 |  1.082 % |
c |     76584 |   38511   217179 |   48345   36871  3186678    86.4 |  1.082 % |
c |     89564 |   38511   217179 |   53180   14100  1612146   114.3 |  1.082 % |
c |    109028 |   38411   214344 |   58346   33508  3214322    95.9 |  1.135 % |
c |    138222 |   37845   206695 |   63235   17467   939911    53.8 |  1.436 % |
c |    182011 |   37607   205491 |   69121   34514  2014003    58.4 |  1.673 % |
c ==============================================================================
c (current CPU-time: 433.187 s)
c ==============================================================================
c [1mFound solution: 68[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:34844     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |    245472 |   77085   293856 |   23125   43804  2375526    54.2 |  1.673 % |
c   -- subsuming                       
c   -- var.elim.:  1000/34469          
c   -- var.elim.:  2000/34469          
c   -- var.elim.:  3000/34469          
c   -- var.elim.:  4000/34469          
c   -- var.elim.:  5000/34469          
c   -- var.elim.:  6000/34469          
c   -- var.elim.:  7000/34469          
c   -- var.elim.:  8000/34469          
c   -- var.elim.:  9000/34469          
c   -- var.elim.:  10000/34469          
c   -- var.elim.:  11000/34469          
c   -- var.elim.:  12000/34469          
c   -- var.elim.:  13000/34469          
c   -- var.elim.:  14000/34469          
c   -- var.elim.:  15000/34469          
c   -- var.elim.:  16000/34469          
c   -- var.elim.:  17000/34469          
c   -- var.elim.:  18000/34469          
c   -- var.elim.:  19000/34469          
c   -- var.elim.:  20000/34469          
c   -- var.elim.:  21000/34469          
c   -- var.elim.:  22000/34469          
c   -- var.elim.:  23000/34469          
c   -- var.elim.:  24000/34469          
c   -- var.elim.:  25000/34469          
c   -- var.elim.:  26000/34469          
c   -- var.elim.:  27000/34469          
c   -- var.elim.:  28000/34469          
c   -- var.elim.:  29000/34469          
c   -- var.elim.:  30000/34469          
c   -- var.elim.:  31000/34469          
c   -- var.elim.:  32000/34469          
c   -- var.elim.:  33000/34469          
c   -- var.elim.:  34000/34469          
c   -- var.elim.:  34469/34469          
c   -- var.elim.:  1000/18301          
c   -- var.elim.:  2000/18301          
c   -- var.elim.:  3000/18301          
c   -- var.elim.:  4000/18301          
c   -- var.elim.:  5000/18301          
c   -- var.elim.:  6000/18301          
c   -- var.elim.:  7000/18301          
c   -- var.elim.:  8000/18301          
c   -- var.elim.:  9000/18301          
c   -- var.elim.:  10000/18301          
c   -- var.elim.:  11000/18301          
c   -- var.elim.:  12000/18301          
c   -- var.elim.:  13000/18301          
c   -- var.elim.:  14000/18301          
c   -- var.elim.:  15000/18301          
c   -- var.elim.:  16000/18301          
c   -- var.elim.:  17000/18301          
c   -- var.elim.:  18000/18301          
c   -- var.elim.:  18301/18301          
c   -- var.elim.:  1000/8481          
c   -- var.elim.:  2000/8481          
c   -- var.elim.:  3000/8481          
c   -- var.elim.:  4000/8481          
c   -- var.elim.:  5000/8481          
c   -- var.elim.:  6000/8481          
c   -- var.elim.:  7000/8481          
c   -- var.elim.:  8000/8481          
c   -- var.elim.:  8481/8481          
c   -- var.elim.:  1000/12209          
c   -- var.elim.:  2000/12209          
c   -- var.elim.:  3000/12209          
c   -- var.elim.:  4000/12209          
c   -- var.elim.:  5000/12209          
c   -- var.elim.:  6000/12209          
c   -- var.elim.:  7000/12209          
c   -- var.elim.:  8000/12209          
c   -- var.elim.:  9000/12209          
c   -- var.elim.:  10000/12209          
c   -- var.elim.:  11000/12209          
c   -- var.elim.:  12000/12209          
c   -- var.elim.:  12209/12209          
c   -- var.elim.:  1000/8541          
c   -- var.elim.:  2000/8541          
c   -- var.elim.:  3000/8541          
c   -- var.elim.:  4000/8541          
c   -- var.elim.:  5000/8541          
c   -- var.elim.:  6000/8541          
c   -- var.elim.:  7000/8541          
c   -- var.elim.:  8000/8541          
c   -- var.elim.:  8541/8541          
c   -- var.elim.:  85/85          
c   -- subsuming                       
c   -- var.elim.:  1000/17776          
c   -- var.elim.:  2000/17776          
c   -- var.elim.:  3000/17776          
c   -- var.elim.:  4000/17776          
c   -- var.elim.:  5000/17776          
c   -- var.elim.:  6000/17776          
c   -- var.elim.:  7000/17776          
c   -- var.elim.:  8000/17776          
c   -- var.elim.:  9000/17776          
c   -- var.elim.:  10000/17776          
c   -- var.elim.:  11000/17776          
c   -- var.elim.:  12000/17776          
c   -- var.elim.:  13000/17776          
c   -- var.elim.:  14000/17776          
c   -- var.elim.:  15000/17776          
c   -- var.elim.:  16000/17776          
c   -- var.elim.:  17000/17776          
c   -- var.elim.:  17776/17776          
c   -- var.elim.:  1000/9524          
c   -- var.elim.:  2000/9524          
c   -- var.elim.:  3000/9524          
c   -- var.elim.:  4000/9524          
c   -- var.elim.:  5000/9524          
c   -- var.elim.:  6000/9524          
c   -- var.elim.:  7000/9524          
c   -- var.elim.:  8000/9524          
c   -- var.elim.:  9000/9524          
c   -- var.elim.:  9524/9524          
c   -- var.elim.:  1000/9979          
c   -- var.elim.:  2000/9979          
c   -- var.elim.:  3000/9979          
c   -- var.elim.:  4000/9979          
c   -- var.elim.:  5000/9979          
c   -- var.elim.:  6000/9979          
c   -- var.elim.:  7000/9979          
c   -- var.elim.:  8000/9979          
c   -- var.elim.:  9000/9979          
c   -- var.elim.:  9979/9979          
c   -- var.elim.:  1000/11078          
c   -- var.elim.:  2000/11078          
c   -- var.elim.:  3000/11078          
c   -- var.elim.:  4000/11078          
c   -- var.elim.:  5000/11078          
c   -- var.elim.:  6000/11078          
c   -- var.elim.:  7000/11078          
c   -- var.elim.:  8000/11078          
c   -- var.elim.:  9000/11078          
c   -- var.elim.:  10000/11078          
c   -- var.elim.:  11000/11078          
c   -- var.elim.:  11078/11078          
c   -- var.elim.:  1000/4350          
c   -- var.elim.:  2000/4350          
c   -- var.elim.:  3000/4350          
c   -- var.elim.:  4000/4350          
c   -- var.elim.:  4350/4350          
c   -- var.elim.:  1000/1083          
c   -- var.elim.:  1083/1083          
c   -- var.elim.:  537/537          
c   -- subsuming                       
c   -- var.elim.:  1000/11614          
c   -- var.elim.:  2000/11614          
c   -- var.elim.:  3000/11614          
c   -- var.elim.:  4000/11614          
c   -- var.elim.:  5000/11614          
c   -- var.elim.:  6000/11614          
c   -- var.elim.:  7000/11614          
c   -- var.elim.:  8000/11614          
c   -- var.elim.:  9000/11614          
c   -- var.elim.:  10000/11614          
c   -- var.elim.:  11000/11614          
c   -- var.elim.:  11614/11614          
c   -- var.elim.:  1000/7735          
c   -- var.elim.:  2000/7735          
c   -- var.elim.:  3000/7735          
c   -- var.elim.:  4000/7735          
c   -- var.elim.:  5000/7735          
c   -- var.elim.:  6000/7735          
c   -- var.elim.:  7000/7735          
c   -- var.elim.:  7735/7735          
c   -- var.elim.:  1000/4337          
c   -- var.elim.:  2000/4337          
c   -- var.elim.:  3000/4337          
c   -- var.elim.:  4000/4337          
c   -- var.elim.:  4337/4337          
c   -- var.elim.:  1000/2889          
c   -- var.elim.:  2000/2889          
c   -- var.elim.:  2889/2889          
c   -- var.elim.:  182/182          
c   -- subsuming                       
c   -- var.elim.:  1000/7396          
c   -- var.elim.:  2000/7396          
c   -- var.elim.:  3000/7396          
c   -- var.elim.:  4000/7396          
c   -- var.elim.:  5000/7396          
c   -- var.elim.:  6000/7396          
c   -- var.elim.:  7000/7396          
c   -- var.elim.:  7396/7396          
c   -- var.elim.:  229/229          
c |    245472 |   60332   364128 |      --   43804       --      -- |     --   | -16753/70273
c |    245472 |   60332   364128 |   24132   41161  2179768    53.0 |  1.673 % |
c |    245572 |   60332   364128 |   26546   15719   667077    42.4 |  1.166 % |
c |    245723 |   60332   364128 |   29200   15870   674117    42.5 |  1.166 % |
c |    245948 |   60332   364128 |   32120   16095   684896    42.6 |  1.166 % |
c |    246285 |   60332   364128 |   35332   16432   699321    42.6 |  1.166 % |
c |    246795 |   60332   364128 |   38866   16942   719744    42.5 |  1.166 % |
c |    247554 |   60332   364128 |   42752   17701   755711    42.7 |  1.166 % |
c |    248694 |   60332   364128 |   47028   18841   788195    41.8 |  1.166 % |
c |    250402 |   60298   363872 |   51701   20547   896062    43.6 |  1.217 % |
c |    252966 |   60298   363872 |   56871   23111  1011900    43.8 |  1.217 % |
c |    256810 |   60160   362624 |   62415   26951  1290292    47.9 |  1.412 % |
c |    262578 |   60059   361796 |   68542   32715  1652203    50.5 |  1.571 % |
c |    271228 |   58282   347463 |   73165   41268  2131250    51.6 |  4.201 % |
c ==============================================================================
c [1mOptimal solution: 68[0m
s OPTIMUM FOUND
v -v1 -v2 -v3 -v4 -v5 -v6 -v7 -v8 v9 -v10 -v11 -v12 -v13 -v14 -v15 -v16 -v17 -v18 -v19 -v20 -v21 -v22 -v23 -v24 -v25 -v26 v27 v28 v29 -v30 -v31 -v32 -v33 -v34 -v35 -v36 -v37 -v38 v39 -v40 v41 -v42 -v43 -v44 -v45 -v46 -v47 -v48 -v49 -v50 -v51 -v52 -v53 -v54 -v55 -v56 -v57 -v58 -v59 -v60 -v61 -v62 -v63 -v64 v65 -v66 -v67 -v68 -v69 -v70 -v71 -v72 v73 v74 v75 -v76 -v77 -v78 -v79 -v80 -v81 -v82 -v83 -v84 -v85 -v86 -v87 -v88 -v89 -v90 -v91 -v92 -v93 -v94 -v95 -v96 -v97 -v98 -v99 -v100 -v101 -v102 -v103 -v104 v105 -v106 -v107 -v108 -v109 -v110 -v111 -v112 -v113 -v114 -v115 v116 -v117 -v118 -v119 -v120 -v121 -v122 -v123 -v124 -v125 -v126 -v127 -v128 -v129 -v130 -v131 -v132 -v133 v134 -v135 -v136 -v137 -v138 -v139 -v140 -v141 -v142 -v143 -v144 -v145 -v146 -v147 -v148 -v149 -v150 -v151 -v152 -v153 -v154 v155 v156 -v157 -v158 -v159 -v160 -v161 -v162 -v163 -v164 -v165 -v166 -v167 v168 v169 -v170 -v171 -v172 -v173 -v174 -v175 -v176 -v177 -v178 -v179 -v180 -v181 v182 -v183 -v184 -v185 v186 -v187 -v188 -v189 v190 -v191 -v192 -v193 -v194 -v195 -v196 -v197 -v198 -v199 -v200 -v201 v202 -v203 -v204 v205 -v206 -v207 -v208 v209 -v210 -v211 -v212 v213 -v214 -v215 -v216 -v217 -v218 -v219 v220 -v221 -v222 -v223 -v224 -v225 -v226 -v227 -v228 -v229 -v230 -v231 -v232 -v233 v234 -v235 -v236 -v237 -v238 -v239 -v240 -v241 -v242 -v243 -v244 -v245 -v246 -v247 -v248 -v249 -v250 -v251 -v252 -v253 -v254 -v255 -v256 -v257 v258 -v259 -v260 -v261 -v262 -v263 -v264 -v265 -v266 -v267 -v268 -v269 -v270 -v271 -v272 -v273 -v274 -v275 -v276 -v277 -v278 -v279 -v280 -v281 -v282 v283 -v284 -v285 -v286 -v287 -v288 -v289 -v290 -v291 -v292 -v293 -v294 v295 v296 -v297 -v298 -v299 -v300 -v301 -v302 -v303 -v304 -v305 -v306 v307 -v308 -v309 -v310 -v311 -v312 -v313 -v314 -v315 -v316 -v317 -v318 -v319 -v320 -v321 -v322 -v323 v324 -v325 -v326 -v327 -v328 -v329 -v330 -v331 -v332 -v333 -v334 -v335 v336 -v337 -v338 v339 -v340 -v341 -v342 -v343 -v344 -v345 -v346 -v347 -v348 -v349 -v350 -v351 -v352 -v353 -v354 -v355 -v356 -v357 -v358 -v359 -v360 -v361 -v362 -v363 -v364 -v365 -v366 -v367 -v368 -v369 -v370 -v371 -v372 -v373 -v374 v375 -v376 -v377 -v378 v379 -v380 -v381 -v382 -v383 -v384 -v385 -v386 -v387 -v388 -v389 -v390 -v391 -v392 -v393 -v394 -v395 -v396 -v397 -v398 -v399 -v400 -v401 -v402 -v403 -v404 v405 -v406 -v407 -v408 -v409 v410 -v411 -v412 -v413 v414 -v415 -v416 -v417 -v418 -v419 v420 -v421 -v422 v423 -v424 -v425 -v426 -v427 v428 -v429 -v430 -v431 v432 -v433 -v434 -v435 -v436 -v437 -v438 -v439 -v440 -v441 -v442 -v443 -v444 -v445 -v446 -v447 -v448 -v449 -v450 -v451 -v452 v453 -v454 -v455 -v456 -v457 -v458 -v459 -v460 -v461 -v462 -v463 -v464 v465 -v466 -v467 -v468 -v469 -v470 -v471 -v472 -v473 -v474 -v475 v476 -v477 -v478 -v479 -v480 -v481 -v482 -v483 v484 -v485 -v486 -v487 -v488 -v489 -v490 -v491 -v492 -v493 v494 -v495 -v496 -v497 -v498 -v499 -v500 -v501 -v502 -v503 -v504 -v505 -v506 -v507 -v508 -v509 -v510 v511 -v512 -v513 -v514 -v515 -v516 -v517 -v518 -v519 -v520 -v521 -v522 -v523 -v524 -v525 v526 -v527 -v528 -v529 -v530 -v531 -v532 -v533 -v534 -v535 v536 -v537 -v538 -v539 -v540 -v541 -v542 -v543 -v544 -v545 -v546 -v547 -v548 -v549 v550 v551 -v552 -v553 -v554 -v555 -v556 -v557 -v558 v559 -v560 -v561 -v562 -v563 -v564 -v565 -v566 -v567 -v568 -v569 -v570 -v571 -v572 -v573 -v574 -v575 -v576 v577 v578 -v579 -v580 -v581 -v582 -v583 -v584 -v585 -v586 -v587 -v588 -v589 -v590 -v591 -v592 -v593 -v594 -v595 -v596 -v597 -v598 -v599 -v600 -v601 -v602 -v603 -v604 -v605 -v606 -v607 -v608 -v609 -v610 v611 -v612 -v613 -v614 -v615 -v616 -v617 -v618 -v619 -v620 -v621 -v622 -v623 -v624 -v625 -v626 -v627 -v628 -v629 -v630 -v631 v632 -v633 -v634 -v635 -v636 -v637 -v638 -v639 -v640 -v641 -v642 -v643 -v644 -v645 -v646 v647 -v648 -v649 -v650 -v651 -v652 -v653 -v654 -v655 -v656 -v657 -v658 -v659 -v660 -v661 -v662 -v663 v664 -v665 -v666 -v667 -v668 -v669 -v670 -v671 -v672 -v673 -v674 -v675 -v676 -v677 -v678 -v679 -v680 -v681 v682 v683 -v684 -v685 -v686 -v687 -v688 -v689 -v690 -v691 -v692 -v693 -v694 -v695 -v696 -v697 -v698 -v699 -v700 -v701 -v702 -v703 -v704 -v705 -v706 -v707 -v708 -v709 -v710 -v711 -v712 -v713 -v714 -v715 -v716 -v717 -v718 v719 -v720 -v721 -v722 -v723 -v724 -v725 -v726 -v727 -v728 -v729 v730 -v731 -v732 -v733 -v734 -v735 -v736 -v737 -v738 -v739 -v740 -v741 -v742 -v743 -v744 -v745 -v746 -v747 -v748 -v749 -v750 -v751 -v752 -v753 -v754 -v755 -v756 -v757 -v758 -v759 v760 -v761 -v762 -v763 -v764 -v765 -v766 -v767 -v768 -v769 -v770 -v771 -v772 v773 -v774 -v775 -v776 -v777 -v778 -v779 -v780 -v781 -v782 -v783 -v784 -v785 -v786 -v787 -v788 -v789 -v790 -v791 -v792 -v793 -v794 -v795 -v796 -v797 -v798 -v799 -v800 -v801 -v802 -v803 -v804 -v805 -v806 -v807 v808 -v809 -v810 -v811 -v812 -v813 -v814 -v815 -v816 -v817 -v818 -v819 -v820 v821 -v822 -v823 -v824 -v825 -v826 -v827 -v828 -v829 -v830 -v831 -v832 -v833 -v834 -v835 -v836 -v837 -v838 -v839 -v840
c _______________________________________________________________________________
c 
c restarts              : 44
c conflicts             : 275687         (429 /sec)
c decisions             : 465885         (726 /sec)
c propagations          : 61305810       (95506 /sec)
c inspects              : 751329916      (1170474 /sec)
c CPU time              : 641.902 s
c _______________________________________________________________________________
#### 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.95 0.90 2/54 1723
Raw data (stat): 1723 (runsolver) R 1722 30854 30853 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422101934 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0007 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 2087 0 0 0 992 6 0 0 25 0 1 0 422101934 10002432 2043 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2442 2043 603 41 0 2401 0
vsize: 9768
[startup+20.001 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 2563 0 0 0 1990 8 0 0 25 0 1 0 422101934 11960320 2519 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2920 2519 603 41 0 2879 0
vsize: 11680
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 2586 0 0 0 2990 8 0 0 25 0 1 0 422101934 12042240 2542 4294967295 134512640 134672761 3221224560 3221223600 134614343 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2940 2542 603 41 0 2899 0
vsize: 11760
[startup+40.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 5988 0 0 0 3975 23 0 0 25 0 1 0 422101934 28839936 5784 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7041 5784 603 41 0 7000 0
vsize: 28164
[startup+50.0032 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 6046 0 0 0 4973 25 0 0 25 0 1 0 422101934 28975104 5842 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7074 5842 603 41 0 7033 0
vsize: 28296
[startup+60.0034 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 6061 0 0 0 5972 25 0 0 25 0 1 0 422101934 29102080 5857 4294967295 134512640 134672761 3221224560 3221223000 134643589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7105 5857 603 41 0 7064 0
vsize: 28420
[startup+70.0043 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 6245 0 0 0 6972 26 0 0 25 0 1 0 422101934 29978624 6041 4294967295 134512640 134672761 3221224560 3221223056 134606977 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7319 6041 603 41 0 7278 0
vsize: 29276
[startup+80.0044 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 6245 0 0 0 7971 26 0 0 25 0 1 0 422101934 29978624 6041 4294967295 134512640 134672761 3221224560 3221223104 134621247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7319 6041 603 41 0 7278 0
vsize: 29276
[startup+90.0045 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 6245 0 0 0 8969 29 0 0 25 0 1 0 422101934 29130752 5885 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7112 5885 603 41 0 7071 0
vsize: 28448
[startup+100.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 6342 0 0 0 9968 30 0 0 25 0 1 0 422101934 29675520 5982 4294967295 134512640 134672761 3221224560 3221223056 134606372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7245 5982 603 41 0 7204 0
vsize: 28980
[startup+110.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 6342 0 0 0 10967 31 0 0 25 0 1 0 422101934 29130752 5885 4294967295 134512640 134672761 3221224560 3221223008 134643548 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7112 5885 603 41 0 7071 0
vsize: 28448
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 6513 0 0 0 11966 32 0 0 25 0 1 0 422101934 29786112 6025 4294967295 134512640 134672761 3221224560 3221223104 134621247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7272 6025 603 41 0 7231 0
vsize: 29088
[startup+130.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 6621 0 0 0 12966 33 0 0 25 0 1 0 422101934 29261824 5917 4294967295 134512640 134672761 3221224560 3221223008 134643987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7144 5917 603 41 0 7103 0
vsize: 28576
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 7481 0 0 0 13963 36 0 0 25 0 1 0 422101934 32878592 6777 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8027 6777 603 41 0 7986 0
vsize: 32108
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 8634 0 0 0 14959 40 0 0 25 0 1 0 422101934 37621760 7930 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9185 7930 603 41 0 9144 0
vsize: 36740
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 9673 0 0 0 15956 43 0 0 25 0 1 0 422101934 41984000 8969 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10250 8969 603 41 0 10209 0
vsize: 41000
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 10600 0 0 0 16953 46 0 0 25 0 1 0 422101934 45678592 9896 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11152 9896 603 41 0 11111 0
vsize: 44608
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11105 0 0 0 17952 48 0 0 25 0 1 0 422101934 47620096 10352 4294967295 134512640 134672761 3221224560 3221223760 134610637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11626 10352 603 41 0 11585 0
vsize: 46504
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11107 0 0 0 18952 48 0 0 25 0 1 0 422101934 47620096 10354 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11626 10354 603 41 0 11585 0
vsize: 46504
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11107 0 0 0 19952 48 0 0 25 0 1 0 422101934 47620096 10354 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11626 10354 603 41 0 11585 0
vsize: 46504
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11108 0 0 0 20952 48 0 0 25 0 1 0 422101934 47620096 10355 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11626 10355 603 41 0 11585 0
vsize: 46504
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11164 0 0 0 21952 48 0 0 25 0 1 0 422101934 47882240 10411 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11690 10411 603 41 0 11649 0
vsize: 46760
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11555 0 0 0 22951 49 0 0 25 0 1 0 422101934 49496064 10802 4294967295 134512640 134672761 3221224560 3221223616 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12084 10802 603 41 0 12043 0
vsize: 48336
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11556 0 0 0 23951 49 0 0 25 0 1 0 422101934 49364992 10776 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10776 603 41 0 12011 0
vsize: 48208
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11556 0 0 0 24951 49 0 0 25 0 1 0 422101934 49364992 10776 4294967295 134512640 134672761 3221224560 3221223600 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10776 603 41 0 12011 0
vsize: 48208
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11556 0 0 0 25952 49 0 0 25 0 1 0 422101934 49364992 10776 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10776 603 41 0 12011 0
vsize: 48208
[startup+270.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11556 0 0 0 26952 49 0 0 25 0 1 0 422101934 49364992 10776 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10776 603 41 0 12011 0
vsize: 48208
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11556 0 0 0 27952 49 0 0 25 0 1 0 422101934 49364992 10776 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10776 603 41 0 12011 0
vsize: 48208
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11559 0 0 0 28952 49 0 0 25 0 1 0 422101934 49364992 10779 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10779 603 41 0 12011 0
vsize: 48208
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11559 0 0 0 29952 49 0 0 25 0 1 0 422101934 49364992 10779 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10779 603 41 0 12011 0
vsize: 48208
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11559 0 0 0 30952 49 0 0 25 0 1 0 422101934 49364992 10779 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10779 603 41 0 12011 0
vsize: 48208
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11559 0 0 0 31953 49 0 0 25 0 1 0 422101934 49364992 10779 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10779 603 41 0 12011 0
vsize: 48208
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11560 0 0 0 32953 49 0 0 25 0 1 0 422101934 49364992 10780 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10780 603 41 0 12011 0
vsize: 48208
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11560 0 0 0 33953 49 0 0 25 0 1 0 422101934 49364992 10780 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10780 603 41 0 12011 0
vsize: 48208
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11561 0 0 0 34953 49 0 0 25 0 1 0 422101934 49364992 10781 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10781 603 41 0 12011 0
vsize: 48208
[startup+360.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11561 0 0 0 35953 49 0 0 25 0 1 0 422101934 49364992 10781 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10781 603 41 0 12011 0
vsize: 48208
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11564 0 0 0 36954 49 0 0 25 0 1 0 422101934 49364992 10784 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12052 10784 603 41 0 12011 0
vsize: 48208
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11569 0 0 0 37954 49 0 0 25 0 1 0 422101934 49627136 10789 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12116 10789 603 41 0 12075 0
vsize: 48464
[startup+390.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11640 0 0 0 38954 49 0 0 25 0 1 0 422101934 50151424 10860 4294967295 134512640 134672761 3221224560 3221223616 134644281 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12244 10860 603 41 0 12203 0
vsize: 48976
[startup+400.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11649 0 0 0 39954 49 0 0 25 0 1 0 422101934 49618944 10799 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 10799 603 41 0 12073 0
vsize: 48456
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11649 0 0 0 40954 49 0 0 25 0 1 0 422101934 49618944 10799 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 10799 603 41 0 12073 0
vsize: 48456
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11652 0 0 0 41954 49 0 0 25 0 1 0 422101934 49618944 10802 4294967295 134512640 134672761 3221224560 3221223704 134616373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 10802 603 41 0 12073 0
vsize: 48456
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 11653 0 0 0 42955 49 0 0 25 0 1 0 422101934 49618944 10803 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12114 10803 603 41 0 12073 0
vsize: 48456
[startup+440.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 13691 0 0 0 43942 62 0 0 25 0 1 0 422101934 53305344 11884 4294967295 134512640 134672761 3221224560 3221223008 134644040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13014 11884 603 41 0 12973 0
vsize: 52056
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 13691 0 0 0 44939 65 0 0 25 0 1 0 422101934 53305344 11884 4294967295 134512640 134672761 3221224560 3221223008 134644008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13014 11884 603 41 0 12973 0
vsize: 52056
[startup+460.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 13691 0 0 0 45936 67 0 0 25 0 1 0 422101934 53305344 11884 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13014 11884 603 41 0 12973 0
vsize: 52056
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 13691 0 0 0 46934 70 0 0 25 0 1 0 422101934 53305344 11884 4294967295 134512640 134672761 3221224560 3221223008 134643570 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13014 11884 603 41 0 12973 0
vsize: 52056
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 13691 0 0 0 47934 70 0 0 25 0 1 0 422101934 53305344 11884 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13014 11884 603 41 0 12973 0
vsize: 52056
[startup+490.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 13844 0 0 0 48934 70 0 0 25 0 1 0 422101934 53952512 12003 4294967295 134512640 134672761 3221224560 3221223024 134644246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 12003 603 41 0 13131 0
vsize: 52688
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 13844 0 0 0 49934 70 0 0 25 0 1 0 422101934 53952512 12003 4294967295 134512640 134672761 3221224560 3221223104 134621068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13172 12003 603 41 0 13131 0
vsize: 52688
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 13879 0 0 0 50931 73 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223008 134643524 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+520.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 13879 0 0 0 51930 74 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223008 134643556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 13879 0 0 0 52929 76 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221222900 1075351210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14031 0 0 0 53929 76 0 0 25 0 1 0 422101934 53788672 12003 4294967295 134512640 134672761 3221224560 3221223056 134606977 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13132 12003 603 41 0 13091 0
vsize: 52528
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14031 0 0 0 54928 77 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223008 134643542 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+560.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14031 0 0 0 55926 79 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223008 134643583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+570.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14183 0 0 0 56925 80 0 0 25 0 1 0 422101934 53829632 12003 4294967295 134512640 134672761 3221224560 3221223104 134621062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13142 12003 603 41 0 13101 0
vsize: 52568
[startup+580.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14224 0 0 0 57925 80 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14224 0 0 0 58925 80 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14224 0 0 0 59925 80 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14224 0 0 0 60925 80 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14224 0 0 0 61926 80 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223744 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14224 0 0 0 62926 80 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14224 0 0 0 63927 80 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 51800
[startup+642.722 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 1723
Raw data (stat): 1723 (minisat+) R 1722 30854 30853 0 -1 0 14224 0 0 0 63927 80 0 0 25 0 1 0 422101934 53043200 11851 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12950 11851 603 41 0 12909 0
vsize: 0

Child status: 30
Real time (s): 642.722
CPU time (s): 642.774
CPU user time (s): 641.927
CPU system time (s): 0.846871
CPU usage (%): 100.008
Max. virtual memory (Kb): 52688
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	68
#### END VERIFIER DATA ####