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/een/normalized-mod008.opb
MD5SUM	18b325bb9311c83b0604c703bacc9a29
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	87
Optimality of the best value was proved	NO
Number of terms in the objective function	319
Biggest coefficient in the objective function	87
Number of bits for the biggest coefficient in the objective function	7
Sum of the numbers in the objective function	23554
Number of bits of the sum of numbers in the objective function	15
Biggest number in a constraint	7499
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	758444
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	0.283956
Number of variables	319
Total number of constraints	6
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	6
Minimum length of a constraint	186
Maximum length of a constraint	231
Trace number 7039

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-14 21:14:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=5146 boxname=wulflinc5 idbench=396 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  18b325bb9311c83b0604c703bacc9a29  /oldhome/oroussel/tmp/wulflinc5/normalized-mod008.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc5/normalized-mod008.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mod008.opb
IDLAUNCH: 5146
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        882644 kB
Buffers:         35672 kB
Cached:          94520 kB
SwapCached:       2272 kB
Active:          60320 kB
Inactive:        74968 kB
HighTotal:      131008 kB
HighFree:        32648 kB
LowTotal:       903652 kB
LowFree:        849996 kB
SwapTotal:     2097136 kB
SwapFree:      2094864 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            11120 kB
Committed_AS:    63472 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 21:17:26 (client local time) WITH STATUS 30 IN 172.335 SECONDS
stats: 5146 0 172.335 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 6 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): sss.ss
c ---[   4]---> BDD-cost:  105
c ---[   3]---> BDD-cost:  168
c ---[   2]---> BDD-cost:  223
c ---[   1]---> Sorter-cost:  663     Base: 3
c ---[   0]---> Sorter-cost:  354     Base: 11
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    2343     7303 |     702       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1342          
c   -- var.elim.:  1342/1342          
c   -- var.elim.:  786/786          
c   -- var.elim.:  361/361          
c   -- var.elim.:  239/239          
c   -- subsuming                       
c   -- var.elim.:  507/507          
c   -- var.elim.:  332/332          
c   -- var.elim.:  4/4          
c   -- var.elim.:  228/228          
c |         0 |    1682    15611 |      --       0       --      -- |     --   | -661/8313
c |         0 |    1682    15611 |     672       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.484926 s)
c ==============================================================================
c [1mFound solution: 3002[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:61666     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  152897   368710 |   45869       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/56152          
c   -- var.elim.:  2000/56152          
c   -- var.elim.:  3000/56152          
c   -- var.elim.:  4000/56152          
c   -- var.elim.:  5000/56152          
c   -- var.elim.:  6000/56152          
c   -- var.elim.:  7000/56152          
c   -- var.elim.:  8000/56152          
c   -- var.elim.:  9000/56152          
c   -- var.elim.:  10000/56152          
c   -- var.elim.:  11000/56152          
c   -- var.elim.:  12000/56152          
c   -- var.elim.:  13000/56152          
c   -- var.elim.:  14000/56152          
c   -- var.elim.:  15000/56152          
c   -- var.elim.:  16000/56152          
c   -- var.elim.:  17000/56152          
c   -- var.elim.:  18000/56152          
c   -- var.elim.:  19000/56152          
c   -- var.elim.:  20000/56152          
c   -- var.elim.:  21000/56152          
c   -- var.elim.:  22000/56152          
c   -- var.elim.:  23000/56152          
c   -- var.elim.:  24000/56152          
c   -- var.elim.:  25000/56152          
c   -- var.elim.:  26000/56152          
c   -- var.elim.:  27000/56152          
c   -- var.elim.:  28000/56152          
c   -- var.elim.:  29000/56152          
c   -- var.elim.:  30000/56152          
c   -- var.elim.:  31000/56152          
c   -- var.elim.:  32000/56152          
c   -- var.elim.:  33000/56152          
c   -- var.elim.:  34000/56152          
c   -- var.elim.:  35000/56152          
c   -- var.elim.:  36000/56152          
c   -- var.elim.:  37000/56152          
c   -- var.elim.:  38000/56152          
c   -- var.elim.:  39000/56152          
c   -- var.elim.:  40000/56152          
c   -- var.elim.:  41000/56152          
c   -- var.elim.:  42000/56152          
c   -- var.elim.:  43000/56152          
c   -- var.elim.:  44000/56152          
c   -- var.elim.:  45000/56152          
c   -- var.elim.:  46000/56152          
c   -- var.elim.:  47000/56152          
c   -- var.elim.:  48000/56152          
c   -- var.elim.:  49000/56152          
c   -- var.elim.:  50000/56152          
c   -- var.elim.:  51000/56152          
c   -- var.elim.:  52000/56152          
c   -- var.elim.:  53000/56152          
c   -- var.elim.:  54000/56152          
c   -- var.elim.:  55000/56152          
c   -- var.elim.:  56000/56152          
c   -- var.elim.:  56152/56152          
c   -- var.elim.:  1000/30101          
c   -- var.elim.:  2000/30101          
c   -- var.elim.:  3000/30101          
c   -- var.elim.:  4000/30101          
c   -- var.elim.:  5000/30101          
c   -- var.elim.:  6000/30101          
c   -- var.elim.:  7000/30101          
c   -- var.elim.:  8000/30101          
c   -- var.elim.:  9000/30101          
c   -- var.elim.:  10000/30101          
c   -- var.elim.:  11000/30101          
c   -- var.elim.:  12000/30101          
c   -- var.elim.:  13000/30101          
c   -- var.elim.:  14000/30101          
c   -- var.elim.:  15000/30101          
c   -- var.elim.:  16000/30101          
c   -- var.elim.:  17000/30101          
c   -- var.elim.:  18000/30101          
c   -- var.elim.:  19000/30101          
c   -- var.elim.:  20000/30101          
c   -- var.elim.:  21000/30101          
c   -- var.elim.:  22000/30101          
c   -- var.elim.:  23000/30101          
c   -- var.elim.:  24000/30101          
c   -- var.elim.:  25000/30101          
c   -- var.elim.:  26000/30101          
c   -- var.elim.:  27000/30101          
c   -- var.elim.:  28000/30101          
c   -- var.elim.:  29000/30101          
c   -- var.elim.:  30000/30101          
c   -- var.elim.:  30101/30101          
c   -- var.elim.:  564/564          
c   -- subsuming                       
c   -- var.elim.:  1000/5286          
c   -- var.elim.:  2000/5286          
c   -- var.elim.:  3000/5286          
c   -- var.elim.:  4000/5286          
c   -- var.elim.:  5000/5286          
c   -- var.elim.:  5286/5286          
c   -- var.elim.:  204/204          
c   -- subsuming                       
c   -- var.elim.:  79/79          
c   -- var.elim.:  7/7          
c |         0 |  135835   458593 |      --       0       --      -- |     --   | -17062/89884
c |         0 |  135835   458593 |   54334       0        0     nan |  0.000 % |
c |       100 |  135835   458593 |   59767     100     1626    16.3 |  0.020 % |
c |       250 |  135835   458593 |   65744     250     2927    11.7 |  0.020 % |
c |       475 |  135835   458593 |   72318     475     4568     9.6 |  0.020 % |
c |       814 |  135835   458593 |   79550     814    10797    13.3 |  0.020 % |
c |      1322 |  135835   458593 |   87505    1322   131461    99.4 |  0.020 % |
c |      2082 |  135835   458593 |   96255    2082   209718   100.7 |  0.020 % |
c |      3223 |  135835   458593 |  105881    3223   276264    85.7 |  0.020 % |
c |      4932 |  135835   458593 |  116469    4932   331702    67.3 |  0.020 % |
c |      7494 |  135835   458593 |  128116    7494   374019    49.9 |  0.020 % |
c |     11339 |  135835   458593 |  140928   11339   476841    42.1 |  0.020 % |
c |     17105 |  135835   458593 |  155021   17105   707933    41.4 |  0.020 % |
c ==============================================================================
c (current CPU-time: 52.438 s)
c ==============================================================================
c [1mFound solution: 2698[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     17492 |  137791   463951 |   41337   17492   735744    42.1 |  0.020 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3103          
c   -- var.elim.:  2000/3103          
c   -- var.elim.:  3000/3103          
c   -- var.elim.:  3103/3103          
c   -- var.elim.:  1000/1742          
c   -- var.elim.:  1742/1742          
c   -- subsuming                       
c   -- var.elim.:  117/117          
c |     17492 |  136672   464529 |      --   17492       --      -- |     --   | -1119/579
c |     17492 |  136672   464529 |   54668   17492   735744    42.1 |  0.020 % |
c |     17592 |  136672   464529 |   60135   17592   736518    41.9 |  0.023 % |
c |     17742 |  136672   464529 |   66149   17742   738562    41.6 |  0.023 % |
c |     17967 |  136672   464529 |   72764   17967   741327    41.3 |  0.023 % |
c |     18304 |  136672   464529 |   80040   18304   743519    40.6 |  0.023 % |
c |     18810 |  136672   464529 |   88044   18810   790898    42.0 |  0.023 % |
c |     19569 |  136672   464529 |   96849   19569   801850    41.0 |  0.023 % |
c |     20708 |  136672   464529 |  106534   20708   814472    39.3 |  0.023 % |
c |     22417 |  136672   464529 |  117187   22417   913646    40.8 |  0.023 % |
c |     24980 |  136672   464529 |  128906   24980   967008    38.7 |  0.023 % |
c |     28824 |  136672   464529 |  141796   28824  1088444    37.8 |  0.023 % |
c ==============================================================================
c (current CPU-time: 76.7673 s)
c ==============================================================================
c [1mFound solution: 2651[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     31430 |  138071   468400 |   41421   31430  1139487    36.3 |  0.023 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2264          
c   -- var.elim.:  2000/2264          
c   -- var.elim.:  2264/2264          
c   -- var.elim.:  1000/1311          
c   -- var.elim.:  1311/1311          
c   -- subsuming                       
c   -- var.elim.:  95/95          
c |     31430 |  137276   468638 |      --   31430       --      -- |     --   | -795/239
c |     31430 |  137276   468638 |   54910   31430  1139487    36.3 |  0.023 % |
c |     31530 |  137276   468638 |   60401   31530  1140241    36.2 |  0.026 % |
c |     31680 |  137276   468638 |   66441   31680  1156169    36.5 |  0.026 % |
c |     31905 |  137276   468638 |   73085   31905  1168770    36.6 |  0.026 % |
c ==============================================================================
c (current CPU-time: 80.7647 s)
c ==============================================================================
c [1mFound solution: 2640[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     31969 |  137220   468817 |   41165   31963  1170179    36.6 |  0.026 % |
c   -- subsuming                       
c   -- var.elim.:  505/505          
c   -- var.elim.:  782/782          
c |     31969 |  137189   469404 |      --   31963       --      -- |     --   | -31/588
c |     31969 |  137189   469404 |   54875   31963  1170179    36.6 |  0.026 % |
c |     32069 |  137189   469404 |   60363   32063  1183569    36.9 |  0.071 % |
c |     32221 |  137189   469404 |   66399   32215  1184697    36.8 |  0.071 % |
c |     32447 |  137189   469404 |   73039   32441  1186609    36.6 |  0.071 % |
c |     32784 |  137189   469404 |   80343   32778  1192205    36.4 |  0.071 % |
c |     33290 |  137189   469404 |   88377   33284  1202462    36.1 |  0.071 % |
c |     34049 |  137189   469404 |   97215   34043  1222962    35.9 |  0.071 % |
c |     35190 |  137189   469404 |  106937   35184  1238927    35.2 |  0.071 % |
c |     36899 |  137189   469404 |  117630   36893  1261287    34.2 |  0.071 % |
c ==============================================================================
c (current CPU-time: 95.1195 s)
c ==============================================================================
c [1mFound solution: 2603[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     37476 |  137352   470263 |   41205   37470  1278740    34.1 |  0.071 % |
c   -- subsuming                       
c   -- var.elim.:  780/780          
c   -- var.elim.:  569/569          
c   -- var.elim.:  11/11          
c   -- var.elim.:  242/242          
c |     37476 |  137231   470894 |      --   37470       --      -- |     --   | -121/632
c |     37476 |  137231   470894 |   54892   36832  1149670    31.2 |  0.071 % |
c |     37577 |  137231   470894 |   60381   36933  1155361    31.3 |  0.074 % |
c |     37727 |  137231   470894 |   66419   37083  1156353    31.2 |  0.074 % |
c ==============================================================================
c (current CPU-time: 96.9663 s)
c ==============================================================================
c [1mFound solution: 1186[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     37816 |  137692   472517 |   41307   37172  1156853    31.1 |  0.074 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1085          
c   -- var.elim.:  1085/1085          
c   -- var.elim.:  741/741          
c   -- var.elim.:  112/112          
c   -- subsuming                       
c   -- var.elim.:  147/147          
c |     37816 |  137386   472895 |      --   37172       --      -- |     --   | -306/379
c |     37816 |  137386   472895 |   54954   37172  1156853    31.1 |  0.074 % |
c ==============================================================================
c (current CPU-time: 98.2901 s)
c ==============================================================================
c [1mFound solution: 1104[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     37837 |  138946   477179 |   41683   37193  1160482    31.2 |  0.074 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2607          
c   -- var.elim.:  2000/2607          
c   -- var.elim.:  2607/2607          
c   -- var.elim.:  1000/1515          
c   -- var.elim.:  1515/1515          
c   -- var.elim.:  10/10          
c   -- var.elim.:  16/16          
c   -- subsuming                       
c   -- var.elim.:  26/26          
c |     37837 |  138035   477282 |      --   37193       --      -- |     --   | -911/104
c |     37837 |  138035   477282 |   55214   37193  1160482    31.2 |  0.074 % |
c ==============================================================================
c (current CPU-time: 100.235 s)
c ==============================================================================
c [1mFound solution: 785[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    4     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     37913 |  138262   478139 |   41478   37269  1173373    31.5 |  0.074 % |
c   -- subsuming                       
c   -- var.elim.:  598/598          
c   -- var.elim.:  432/432          
c |     37913 |  138118   480051 |      --   37269       --      -- |     --   | -144/1913
c |     37913 |  138118   480051 |   55247   37269  1173373    31.5 |  0.074 % |
c |     38013 |  138080   477715 |   60755   37368  1185586    31.7 |  0.093 % |
c |     38164 |  137952   477188 |   66768   37475  1187423    31.7 |  0.144 % |
c ==============================================================================
c (current CPU-time: 104.617 s)
c ==============================================================================
c [1mFound solution: 744[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     38178 |  137976   477326 |   41392   37489  1191699    31.8 |  0.144 % |
c   -- subsuming                       
c   -- var.elim.:  526/526          
c   -- var.elim.:  1000/1066          
c   -- var.elim.:  1066/1066          
c   -- var.elim.:  671/671          
c   -- var.elim.:  451/451          
c   -- subsuming                       
c   -- var.elim.:  806/806          
c   -- var.elim.:  5/5          
c |     38178 |  137922   479083 |      --   37489       --      -- |     --   | -54/1758
c |     38178 |  137922   479083 |   55168   37074  1080637    29.1 |  0.144 % |
c |     38278 |  137922   479083 |   60685   37174  1083254    29.1 |  0.148 % |
c ==============================================================================
c (current CPU-time: 108.321 s)
c ==============================================================================
c [1mFound solution: 668[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     38342 |  138024   479830 |   41407   37238  1084026    29.1 |  0.148 % |
c   -- subsuming                       
c   -- var.elim.:  946/946          
c   -- var.elim.:  572/572          
c   -- var.elim.:  295/295          
c   -- var.elim.:  108/108          
c |     38342 |  137951   480677 |      --   37238       --      -- |     --   | -68/860
c |     38342 |  137951   480677 |   55180   37238  1084026    29.1 |  0.148 % |
c ==============================================================================
c (current CPU-time: 109.697 s)
c ==============================================================================
c [1mFound solution: 662[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     38354 |  137978   480823 |   41393   37250  1084144    29.1 |  0.148 % |
c   -- subsuming                       
c   -- var.elim.:  200/200          
c   -- var.elim.:  101/101          
c   -- var.elim.:  81/81          
c |     38354 |  137959   480797 |      --   37250       --      -- |     --   | -19/-25
c |     38354 |  137959   480797 |   55183   37250  1084144    29.1 |  0.148 % |
c ==============================================================================
c (current CPU-time: 110.712 s)
c ==============================================================================
c [1mFound solution: 660[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     38355 |  137986   480943 |   41395   37251  1084162    29.1 |  0.148 % |
c   -- subsuming                       
c   -- var.elim.:  116/116          
c   -- var.elim.:  101/101          
c   -- var.elim.:  81/81          
c |     38355 |  137967   480920 |      --   37251       --      -- |     --   | -19/-22
c |     38355 |  137967   480920 |   55186   37251  1084162    29.1 |  0.148 % |
c ==============================================================================
c (current CPU-time: 111.857 s)
c ==============================================================================
c [1mFound solution: 577[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     38368 |  138026   481486 |   41407   37264  1085415    29.1 |  0.148 % |
c   -- subsuming                       
c   -- var.elim.:  499/499          
c   -- var.elim.:  465/465          
c   -- var.elim.:  90/90          
c   -- var.elim.:  112/112          
c |     38368 |  137987   481967 |      --   37264       --      -- |     --   | -39/482
c |     38368 |  137987   481967 |   55194   37264  1085415    29.1 |  0.148 % |
c ==============================================================================
c (current CPU-time: 113.995 s)
c ==============================================================================
c [1mFound solution: 500[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     38418 |  138131   482665 |   41439   37314  1096771    29.4 |  0.148 % |
c   -- subsuming                       
c   -- var.elim.:  550/550          
c   -- var.elim.:  440/440          
c |     38418 |  138010   482789 |      --   37314       --      -- |     --   | -121/125
c |     38418 |  138010   482789 |   55204   37314  1096771    29.4 |  0.148 % |
c |     38520 |  137933   481853 |   60690   37413  1108522    29.6 |  0.205 % |
c |     38670 |  137636   480431 |   66615   37492  1118120    29.8 |  0.331 % |
c ==============================================================================
c (current CPU-time: 117.613 s)
c ==============================================================================
c [1mFound solution: 468[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     38677 |  137659   480672 |   41297   37499  1118575    29.8 |  0.331 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1560          
c   -- var.elim.:  1560/1560          
c   -- var.elim.:  805/805          
c   -- var.elim.:  79/79          
c   -- subsuming                       
c   -- var.elim.:  629/629          
c   -- var.elim.:  10/10          
c |     38677 |  137592   481285 |      --   37499       --      -- |     --   | -67/614
c |     38677 |  137592   481285 |   55036   37290  1073090    28.8 |  0.331 % |
c |     38777 |  137592   481285 |   60540   37390  1075888    28.8 |  0.334 % |
c |     38927 |  137592   481285 |   66594   37540  1077926    28.7 |  0.334 % |
c ==============================================================================
c (current CPU-time: 127.163 s)
c ==============================================================================
c [1mFound solution: 280[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     39121 |  137373   479807 |   41211   37141   944406    25.4 |  0.334 % |
c   -- subsuming                       
c   -- var.elim.:  525/525          
c   -- var.elim.:  406/406          
c   -- var.elim.:  79/79          
c |     39121 |  137348   479785 |      --   37141       --      -- |     --   | -25/-21
c |     39121 |  137348   479785 |   54939   37141   944406    25.4 |  0.334 % |
c ==============================================================================
c (current CPU-time: 129.274 s)
c ==============================================================================
c [1mFound solution: 277[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     39148 |  137419   480374 |   41225   37168   949616    25.5 |  0.334 % |
c   -- subsuming                       
c   -- var.elim.:  507/507          
c   -- var.elim.:  463/463          
c   -- var.elim.:  197/197          
c   -- var.elim.:  112/112          
c |     39148 |  137363   480572 |      --   37168       --      -- |     --   | -56/199
c |     39148 |  137363   480572 |   54945   36671   912999    24.9 |  0.334 % |
c |     39248 |  137363   480572 |   60439   36771   924080    25.1 |  0.434 % |
c |     39398 |  137363   480572 |   66483   36921   929239    25.2 |  0.434 % |
c ==============================================================================
c (current CPU-time: 132.689 s)
c ==============================================================================
c [1mFound solution: 208[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    3     Base: 5 2 2 3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     39412 |  137388   480816 |   41216   36935   933314    25.3 |  0.434 % |
c   -- subsuming                       
c   -- var.elim.:  217/217          
c   -- var.elim.:  203/203          
c |     39412 |  137378   481180 |      --   36935       --      -- |     --   | -10/365
c |     39412 |  137378   481180 |   54951   36935   933314    25.3 |  0.434 % |
c ==============================================================================
c (current CPU-time: 134.312 s)
c ==============================================================================
c [1mFound solution: 190[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost: 2407
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     39455 |  143994   499853 |   43198   36978   939333    25.4 |  0.434 % |
c   -- subsuming                       
c   -- var.elim.:  1000/2718          
c   -- var.elim.:  2000/2718          
c   -- var.elim.:  2718/2718          
c   -- var.elim.:  42/42          
c |     39455 |  143992   499866 |      --   36978       --      -- |     --   | -2/16
c |     39455 |  143992   499866 |   57596   36978   939333    25.4 |  0.434 % |
c |     39556 |  143992   499866 |   63356   37079   969262    26.1 |  0.409 % |
c |     39709 |  143992   499866 |   69692   37232  1099247    29.5 |  0.409 % |
c ==============================================================================
c (current CPU-time: 140.843 s)
c ==============================================================================
c [1mFound solution: 128[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:  527
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     39786 |  145189   503106 |   43556   37309  1118960    30.0 |  0.409 % |
c   -- subsuming                       
c   -- var.elim.:  862/862          
c   -- var.elim.:  56/56          
c |     39786 |  145182   503101 |      --   37309       --      -- |     --   | -7/-2
c |     39786 |  145182   503101 |   58072   37309  1118960    30.0 |  0.409 % |
c ==============================================================================
c (current CPU-time: 142.079 s)
c ==============================================================================
c [1mFound solution: 124[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:  265
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     39845 |  145958   505367 |   43787   37368  1134303    30.4 |  0.409 % |
c   -- subsuming                       
c   -- var.elim.:  768/768          
c   -- var.elim.:  16/16          
c |     39845 |  145947   505336 |      --   37368       --      -- |     --   | -11/-28
c |     39845 |  145947   505336 |   58378   37368  1134303    30.4 |  0.409 % |
c |     39945 |  145947   505336 |   64216   37468  1163151    31.0 |  0.407 % |
c |     40095 |  145947   505336 |   70638   37618  1165911    31.0 |  0.407 % |
c |     40320 |  145656   504321 |   77547   37745  1190324    31.5 |  0.516 % |
c |     40659 |  145656   504321 |   85301   38084  1265009    33.2 |  0.516 % |
c ==============================================================================
c (current CPU-time: 165.649 s)
c ==============================================================================
c [1mFound solution: 87[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> BDD-cost:    0
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     40998 |  145656   504321 |   43696   38423  1323811    34.5 |  0.516 % |
c   -- subsuming                       
c   -- var.elim.:  1000/3769          
c   -- var.elim.:  2000/3769          
c   -- var.elim.:  3000/3769          
c   -- var.elim.:  3769/3769          
c   -- var.elim.:  1000/2702          
c   -- var.elim.:  2000/2702          
c   -- var.elim.:  2702/2702          
c   -- var.elim.:  1000/1034          
c   -- var.elim.:  1034/1034          
c   -- var.elim.:  846/846          
c   -- var.elim.:  638/638          
c   -- var.elim.:  36/36          
c   -- subsuming                       
c   -- var.elim.:  576/576          
c   -- var.elim.:  18/18          
c |     40998 |  138259   475816 |      --   38423       --      -- |     --   | -743/-1419
c |     40998 |  138259   475816 |   55303   32245   681880    21.1 |  0.516 % |
c ==============================================================================
c [1mOptimal solution: 87[0m
s OPTIMUM FOUND
v -x0 -x1 -x2 -x3 -x4 -x5 -x6 -x7 -x8 -x9 -x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 -x43 -x44 -x45 -x46 -x47 -x48 -x49 -x50 -x51 -x52 -x53 -x54 -x55 -x56 -x57 -x58 -x59 -x60 -x61 -x62 -x63 -x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 -x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 -x103 -x104 -x105 -x106 -x107 -x108 -x109 -x110 -x111 -x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 -x135 -x136 -x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -x165 -x166 -x167 -x168 -x169 -x170 -x171 -x172 -x173 -x174 -x175 -x176 -x177 -x178 -x179 -x180 -x181 -x182 -x183 -x184 -x185 -x186 -x187 -x188 -x189 -x190 -x191 -x192 -x193 -x194 -x195 -x196 -x197 -x198 -x199 -x200 -x201 -x202 -x203 -x204 -x205 -x206 -x207 -x208 -x209 -x210 -x211 -x212 -x213 -x214 -x215 -x216 -x217 -x218 -x219 -x220 -x221 -x222 -x223 -x224 -x225 -x226 -x227 -x228 -x229 -x230 -x231 -x232 -x233 -x234 -x235 -x236 -x237 -x238 -x239 -x240 -x241 -x242 -x243 -x244 -x245 -x246 -x247 -x248 -x249 -x250 -x251 -x252 -x253 -x254 -x255 -x256 -x257 -x258 -x259 -x260 -x261 -x262 -x263 -x264 -x265 -x266 -x267 -x268 -x269 -x270 -x271 -x272 -x273 -x274 -x275 -x276 -x277 -x278 -x279 -x280 -x281 -x282 -x283 -x284 -x285 -x286 -x287 -x288 -x289 -x290 -x291 -x292 -x293 -x294 -x295 -x296 -x297 -x298 -x299 -x300 -x301 -x302 -x303 -x304 -x305 -x306 -x307 -x308 -x309 -x310 -x311 -x312 -x313 -x314 -x315 -x316 -x317 x318
c _______________________________________________________________________________
c 
c restarts              : 72
c conflicts             : 41004          (241 /sec)
c decisions             : 132187         (776 /sec)
c propagations          : 42923789       (251987 /sec)
c inspects              : 175612799      (1030948 /sec)
c CPU time              : 170.341 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): 1.04 0.99 0.89 2/54 1754
Raw data (stat): 1754 (runsolver) R 1753 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 429528948 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 1.03 0.99 0.90 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 8879 0 0 0 959 32 0 0 25 0 1 0 429528948 38989824 8374 4294967295 134512640 134672761 3221224576 3221222880 134621829 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9519 8374 603 41 0 9478 0
vsize: 38076
[startup+20.0015 s]
Raw data (loadavg): 1.03 0.99 0.90 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 9382 0 0 0 1957 33 0 0 25 0 1 0 429528948 39256064 8452 4294967295 134512640 134672761 3221224576 3221223760 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9584 8452 603 41 0 9543 0
vsize: 38336
[startup+30.0019 s]
Raw data (loadavg): 1.02 0.99 0.90 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 9573 0 0 0 2957 33 0 0 25 0 1 0 429528948 40046592 8643 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9777 8643 603 41 0 9736 0
vsize: 39108
[startup+40.0023 s]
Raw data (loadavg): 1.02 0.99 0.90 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 9670 0 0 0 3956 34 0 0 25 0 1 0 429528948 40341504 8740 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9849 8740 603 41 0 9808 0
vsize: 39396
[startup+50.0027 s]
Raw data (loadavg): 1.01 0.99 0.90 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 9903 0 0 0 4955 35 0 0 25 0 1 0 429528948 41402368 8973 4294967295 134512640 134672761 3221224576 3221223396 1075755419 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10108 8973 603 41 0 10067 0
vsize: 40432
[startup+60.0032 s]
Raw data (loadavg): 1.01 0.99 0.90 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 12371 0 0 0 5946 43 0 0 25 0 1 0 429528948 42967040 9223 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10490 9223 603 41 0 10449 0
vsize: 41960
[startup+70.0042 s]
Raw data (loadavg): 1.01 0.99 0.90 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 12512 0 0 0 6946 43 0 0 25 0 1 0 429528948 43626496 9364 4294967295 134512640 134672761 3221224576 3221223760 134615576 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10651 9364 603 41 0 10610 0
vsize: 42604
[startup+80.005 s]
Raw data (loadavg): 1.01 0.99 0.90 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 15411 0 0 0 7936 53 0 0 25 0 1 0 429528948 44793856 9701 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10936 9701 603 41 0 10895 0
vsize: 43744
[startup+90.0054 s]
Raw data (loadavg): 1.01 0.99 0.90 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 17779 0 0 0 8928 61 0 0 25 0 1 0 429528948 45281280 9778 4294967295 134512640 134672761 3221224576 3221223744 134615859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11055 9778 603 41 0 11014 0
vsize: 44220
[startup+100.006 s]
Raw data (loadavg): 1.00 0.99 0.90 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 24129 0 0 0 9907 82 0 0 25 0 1 0 429528948 45887488 9972 4294967295 134512640 134672761 3221224576 3221223296 134564856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11203 9972 603 41 0 11162 0
vsize: 44812
[startup+110.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 30931 0 0 0 10883 106 0 0 25 0 1 0 429528948 53121024 11582 4294967295 134512640 134672761 3221224576 3221222792 1075349620 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12969 11582 603 41 0 12928 0
vsize: 51876
[startup+120.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 41691 0 0 0 11847 141 0 0 25 0 1 0 429528948 47714304 10286 4294967295 134512640 134672761 3221224576 3221223120 134621122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11649 10286 603 41 0 11608 0
vsize: 46596
[startup+130.006 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 44001 0 0 0 12838 150 0 0 25 0 1 0 429528948 45895680 9989 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11205 9989 603 41 0 11164 0
vsize: 44820
[startup+140.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 50096 0 0 0 13817 170 0 0 25 0 1 0 429528948 45969408 10061 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11223 10061 603 41 0 11182 0
vsize: 44892
[startup+150.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 54850 0 0 0 14802 184 0 0 25 0 1 0 429528948 47083520 10289 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11495 10289 603 41 0 11454 0
vsize: 45980
[startup+160.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 54968 0 0 0 15802 184 0 0 25 0 1 0 429528948 47476736 10407 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11591 10407 603 41 0 11550 0
vsize: 46364
[startup+170.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 57621 0 0 0 16794 193 0 0 25 0 1 0 429528948 49856512 10821 4294967295 134512640 134672761 3221224576 3221223120 134621041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 10821 603 41 0 12131 0
vsize: 48688
[startup+172.466 s]
Raw data (loadavg): 1.00 0.99 0.91 1/53 1754
Raw data (stat): 1754 (minisat+) R 1753 24215 24214 0 -1 0 57621 0 0 0 16794 193 0 0 25 0 1 0 429528948 49856512 10821 4294967295 134512640 134672761 3221224576 3221223120 134621041 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 10821 603 41 0 12131 0
vsize: 0

Child status: 30
Real time (s): 172.466
CPU time (s): 172.335
CPU user time (s): 170.365
CPU system time (s): 1.9697
CPU usage (%): 99.9239
Max. virtual memory (Kb): 51876
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	87
#### END VERIFIER DATA ####