PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-sentoy.opb
MD5SUM	4df3e7eb358d27d446e34b975724a6c1
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-7772
Optimality of the best value was proved	NO
Number of terms in the objective function	60
Biggest coefficient in the objective function	974
Number of bits for the biggest coefficient in the objective function	10
Sum of the numbers in the objective function	9460
Number of bits of the sum of numbers in the objective function	14
Biggest number in a constraint	6000
Number of bits of the biggest number in a constraint	13
Biggest sum of numbers in a constraint	26162
Number of bits of the biggest sum of numbers	15
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.01884
Number of variables	60
Total number of constraints	90
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	60
Number of constraints which are nor clauses,nor cardinality constraints	30
Minimum length of a constraint	1
Maximum length of a constraint	60
Trace number 18953

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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:        767360 kB
Buffers:         12100 kB
Cached:         233756 kB
SwapCached:        304 kB
Active:          19472 kB
Inactive:       228920 kB
HighTotal:      131008 kB
HighFree:        68684 kB
LowTotal:       903652 kB
LowFree:        698676 kB
SwapTotal:     2097136 kB
SwapFree:      2096520 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6448 kB
Slab:            13272 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 17:39:04 (client local time) WITH STATUS 10 IN 1200.17 SECONDS
stats: 17262 7 1200.17 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  29]---> Adder-cost: 448   maxlim: 11620   bits: 15/14
c ---[  28]---> Adder-cost: 408   maxlim: 6087   bits: 14/13
c ---[  27]---> Adder-cost: 432   maxlim: 9310   bits: 14/14
c ---[  26]---> Adder-cost: 468   maxlim: 11096   bits: 15/14
c ---[  25]---> Adder-cost: 444   maxlim: 10275   bits: 14/14
c ---[  24]---> Adder-cost: 458   maxlim: 10302   bits: 14/14
c ---[  23]---> Adder-cost: 436   maxlim: 13436   bits: 15/14
c ---[  22]---> Adder-cost: 428   maxlim: 9755   bits: 14/14
c ---[  21]---> Adder-cost: 412   maxlim: 6448   bits: 14/13
c ---[  20]---> Adder-cost: 464   maxlim: 10002   bits: 14/14
c ---[  19]---> Adder-cost: 426   maxlim: 9583   bits: 14/14
c ---[  18]---> Adder-cost: 424   maxlim: 9848   bits: 14/14
c ---[  17]---> Adder-cost: 364   maxlim: 5722   bits: 14/13
c ---[  16]---> Adder-cost: 452   maxlim: 10594   bits: 15/14
c ---[  15]---> Adder-cost: 434   maxlim: 10081   bits: 14/14
c ---[  14]---> Adder-cost: 442   maxlim: 9196   bits: 14/14
c ---[  13]---> Adder-cost: 456   maxlim: 12391   bits: 15/14
c ---[  12]---> Adder-cost: 450   maxlim: 14161   bits: 15/14
c ---[  11]---> Adder-cost: 418   maxlim: 12220   bits: 15/14
c ---[  10]---> Adder-cost: 420   maxlim: 12782   bits: 15/14
c ---[   9]---> Adder-cost: 460   maxlim: 11486   bits: 15/14
c ---[   8]---> Adder-cost: 436   maxlim: 8903   bits: 14/14
c ---[   7]---> Adder-cost: 456   maxlim: 10103   bits: 14/14
c ---[   6]---> Adder-cost: 380   maxlim: 6238   bits: 14/13
c ---[   5]---> Adder-cost: 430   maxlim: 10469   bits: 15/14
c ---[   4]---> Adder-cost: 438   maxlim: 9149   bits: 14/14
c ---[   3]---> Adder-cost: 420   maxlim: 13773   bits: 15/14
c ---[   2]---> Adder-cost: 448   maxlim: 9436   bits: 14/14
c ---[   1]---> Adder-cost: 456   maxlim: 8907   bits: 14/14
c ---[   0]---> Adder-cost: 408   maxlim: 13608   bits: 15/14
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   89295   319020 |   26788       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13035          
c   -- var.elim.:  2000/13035          
c   -- var.elim.:  3000/13035          
c   -- var.elim.:  4000/13035          
c   -- var.elim.:  5000/13035          
c   -- var.elim.:  6000/13035          
c   -- var.elim.:  7000/13035          
c   -- var.elim.:  8000/13035          
c   -- var.elim.:  9000/13035          
c   -- var.elim.:  10000/13035          
c   -- var.elim.:  11000/13035          
c   -- var.elim.:  12000/13035          
c   -- var.elim.:  13000/13035          
c   -- var.elim.:  13035/13035          
c   -- var.elim.:  929/929          
c   -- subsuming                       
c   -- var.elim.:  73/73          
c   -- var.elim.:  62/62          
c |         0 |   88309   316345 |      --       0       --      -- |     --   | -930/-2153
c |         0 |   88309   316345 |   35323       0        0     nan |  0.000 % |
c |       100 |   88309   316345 |   38855     100      369     3.7 |  1.804 % |
c |       251 |   88309   316345 |   42741     251     3460    13.8 |  1.804 % |
c |       476 |   88309   316345 |   47015     476    10621    22.3 |  1.804 % |
c |       814 |   88309   316345 |   51717     814    21788    26.8 |  1.804 % |
c |      1324 |   88309   316345 |   56889    1324    36808    27.8 |  1.804 % |
c ==============================================================================
c (current CPU-time: 9.13361 s)
c ==============================================================================
c [1mFound solution: -2006[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost: 6599     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      1773 |  105307   356119 |   31592    1773    67382    38.0 |  1.804 % |
c   -- subsuming                       
c   -- var.elim.:  1000/5986          
c   -- var.elim.:  2000/5986          
c   -- var.elim.:  3000/5986          
c   -- var.elim.:  4000/5986          
c   -- var.elim.:  5000/5986          
c   -- var.elim.:  5986/5986          
c   -- var.elim.:  1000/3264          
c   -- var.elim.:  2000/3264          
c   -- var.elim.:  3000/3264          
c   -- var.elim.:  3264/3264          
c   -- var.elim.:  38/38          
c   -- subsuming                       
c   -- var.elim.:  348/348          
c   -- var.elim.:  49/49          
c |      1773 |  103530   363482 |      --    1773       --      -- |     --   | -1777/7364
c |      1773 |  103530   363482 |   41412    1773    67382    38.0 |  1.804 % |
c |      1874 |  103530   363482 |   45553    1874    71653    38.2 |  1.452 % |
c |      2024 |  103530   363482 |   50108    2024    73568    36.3 |  1.452 % |
c |      2249 |  103530   363482 |   55119    2249    76069    33.8 |  1.452 % |
c |      2587 |  103530   363482 |   60631    2587    83500    32.3 |  1.452 % |
c |      3093 |  103530   363482 |   66694    3093   102146    33.0 |  1.452 % |
c |      3853 |  103530   363482 |   73363    3853   128519    33.4 |  1.452 % |
c |      4993 |  103530   363482 |   80700    4993   161353    32.3 |  1.452 % |
c |      6702 |  103530   363482 |   88770    6702   198818    29.7 |  1.452 % |
c ==============================================================================
c (current CPU-time: 24.3253 s)
c ==============================================================================
c [1mFound solution: -2158[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      6852 |  104283   365467 |   31284    6852   201770    29.4 |  1.452 % |
c   -- subsuming                       
c   -- var.elim.:  1000/1121          
c   -- var.elim.:  1121/1121          
c   -- var.elim.:  592/592          
c   -- subsuming                       
c   -- var.elim.:  250/250          
c   -- var.elim.:  10/10          
c |      6852 |  103801   365032 |      --    6852       --      -- |     --   | -482/-434
c |      6852 |  103801   365032 |   41520    6841   198475    29.0 |  1.452 % |
c |      6952 |  103801   365032 |   45672    6941   199786    28.8 |  1.452 % |
c |      7105 |  103801   365032 |   50239    7094   203436    28.7 |  1.452 % |
c |      7330 |  103801   365032 |   55263    7319   209963    28.7 |  1.452 % |
c |      7667 |  103801   365032 |   60790    7656   216113    28.2 |  1.452 % |
c ==============================================================================
c (current CPU-time: 27.3808 s)
c ==============================================================================
c [1mFound solution: -2583[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      7858 |  104137   366004 |   31241    7847   218517    27.8 |  1.452 % |
c   -- subsuming                       
c   -- var.elim.:  591/591          
c   -- var.elim.:  351/351          
c   -- subsuming                       
c   -- var.elim.:  114/114          
c |      7858 |  103926   366384 |      --    7847       --      -- |     --   | -211/381
c |      7858 |  103926   366384 |   41570    7847   218517    27.8 |  1.452 % |
c |      7958 |  103926   366384 |   45727    7947   219607    27.6 |  1.455 % |
c |      8108 |  103926   366384 |   50300    8097   220558    27.2 |  1.455 % |
c |      8335 |  103926   366384 |   55330    8324   224027    26.9 |  1.455 % |
c ==============================================================================
c (current CPU-time: 29.3185 s)
c ==============================================================================
c [1mFound solution: -3152[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      8487 |  104174   367172 |   31252    8476   231807    27.3 |  1.455 % |
c   -- subsuming                       
c   -- var.elim.:  502/502          
c   -- var.elim.:  303/303          
c |      8487 |  103989   367513 |      --    8476       --      -- |     --   | -185/342
c |      8487 |  103989   367513 |   41595    8476   231807    27.3 |  1.455 % |
c |      8588 |  103989   367513 |   45755    8577   232969    27.2 |  1.460 % |
c |      8738 |  103989   367513 |   50330    8727   234839    26.9 |  1.460 % |
c |      8964 |  103989   367513 |   55363    8953   238681    26.7 |  1.460 % |
c |      9304 |  103989   367513 |   60900    9293   298102    32.1 |  1.460 % |
c |      9811 |  103989   367513 |   66990    9800   315134    32.2 |  1.460 % |
c ==============================================================================
c (current CPU-time: 37.0054 s)
c ==============================================================================
c [1mFound solution: -3229[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     10486 |  104110   367959 |   31232   10475   345237    33.0 |  1.460 % |
c   -- subsuming                       
c   -- var.elim.:  408/408          
c   -- var.elim.:  220/220          
c |     10486 |  104017   368314 |      --   10475       --      -- |     --   | -93/356
c |     10486 |  104017   368314 |   41606   10475   345237    33.0 |  1.460 % |
c |     10587 |  104017   368314 |   45767   10576   347071    32.8 |  1.466 % |
c |     10737 |  104017   368314 |   50344   10726   352783    32.9 |  1.466 % |
c |     10964 |  104017   368314 |   55378   10953   356565    32.6 |  1.466 % |
c |     11302 |  104017   368314 |   60916   11291   367369    32.5 |  1.466 % |
c ==============================================================================
c (current CPU-time: 41.6907 s)
c ==============================================================================
c [1mFound solution: -4106[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     11647 |  104338   369233 |   31301   11636   375565    32.3 |  1.466 % |
c   -- subsuming                       
c   -- var.elim.:  634/634          
c   -- var.elim.:  317/317          
c |     11647 |  104136   369499 |      --   11636       --      -- |     --   | -202/267
c |     11647 |  104136   369499 |   41654   11636   375565    32.3 |  1.466 % |
c |     11748 |  104136   369499 |   45819   11737   377542    32.2 |  1.469 % |
c |     11898 |  104136   369499 |   50401   11887   380367    32.0 |  1.469 % |
c |     12123 |  104136   369499 |   55442   12112   392140    32.4 |  1.469 % |
c |     12460 |  104136   369499 |   60986   12449   400637    32.2 |  1.469 % |
c |     12966 |  104136   369499 |   67084   12955   417926    32.3 |  1.469 % |
c |     13727 |  104136   369499 |   73793   13716   456875    33.3 |  1.469 % |
c |     14866 |  104136   369499 |   81172   14855   511016    34.4 |  1.469 % |
c |     16575 |  104136   369499 |   89289   16564   694292    41.9 |  1.469 % |
c |     19139 |  104136   369499 |   98218   19128   830745    43.4 |  1.469 % |
c ==============================================================================
c (current CPU-time: 93.6608 s)
c ==============================================================================
c [1mFound solution: -4188[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    8     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     22231 |  104247   369922 |   31274   22220  1194376    53.8 |  1.469 % |
c   -- subsuming                       
c   -- var.elim.:  385/385          
c   -- var.elim.:  219/219          
c |     22231 |  104166   370266 |      --   22220       --      -- |     --   | -81/345
c |     22231 |  104166   370266 |   41666   22220  1194376    53.8 |  1.469 % |
c |     22331 |  104166   370266 |   45833   22320  1197791    53.7 |  1.475 % |
c |     22481 |  104166   370266 |   50416   22470  1203038    53.5 |  1.475 % |
c |     22708 |  104166   370266 |   55457   22697  1210443    53.3 |  1.475 % |
c |     23045 |  104166   370266 |   61003   23034  1220687    53.0 |  1.475 % |
c |     23553 |  104166   370266 |   67104   23542  1250286    53.1 |  1.475 % |
c ==============================================================================
c (current CPU-time: 101.58 s)
c ==============================================================================
c [1mFound solution: -4422[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     23993 |  104254   370601 |   31276   23982  1290222    53.8 |  1.475 % |
c   -- subsuming                       
c   -- var.elim.:  289/289          
c   -- var.elim.:  178/178          
c |     23993 |  104193   370882 |      --   23982       --      -- |     --   | -61/282
c |     23993 |  104193   370882 |   41677   23941  1273306    53.2 |  1.475 % |
c |     24094 |  104193   370882 |   45844   24042  1275192    53.0 |  1.481 % |
c |     24244 |  104193   370882 |   50429   24192  1277041    52.8 |  1.481 % |
c |     24469 |  104193   370882 |   55472   24417  1283698    52.6 |  1.481 % |
c |     24808 |  104193   370882 |   61019   24756  1304176    52.7 |  1.481 % |
c |     25314 |  104193   370882 |   67121   25262  1317879    52.2 |  1.481 % |
c |     26074 |  104193   370882 |   73833   26022  1399828    53.8 |  1.481 % |
c |     27214 |  104193   370882 |   81217   27162  1447698    53.3 |  1.481 % |
c ==============================================================================
c (current CPU-time: 124.658 s)
c ==============================================================================
c [1mFound solution: -4446[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    7     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     28661 |  104285   371251 |   31285   28609  1654001    57.8 |  1.481 % |
c   -- subsuming                       
c   -- var.elim.:  271/271          
c   -- var.elim.:  197/197          
c |     28661 |  104219   371749 |      --   28609       --      -- |     --   | -66/499
c |     28661 |  104219   371749 |   41687   28609  1654001    57.8 |  1.481 % |
c |     28762 |  104219   371749 |   45856   28710  1656911    57.7 |  1.487 % |
c |     28912 |  104219   371749 |   50441   28860  1659394    57.5 |  1.487 % |
c |     29139 |  104219   371749 |   55486   29087  1677989    57.7 |  1.487 % |
c |     29477 |  104219   371749 |   61034   29425  1692438    57.5 |  1.487 % |
c |     29984 |  104219   371749 |   67138   29932  1742034    58.2 |  1.487 % |
c |     30747 |  104219   371749 |   73852   30695  1805226    58.8 |  1.487 % |
c |     31887 |  104219   371749 |   81237   31835  1844363    57.9 |  1.487 % |
c |     33595 |  104219   371749 |   89361   33543  1918654    57.2 |  1.487 % |
c |     36158 |  104219   371749 |   98297   36106  2103147    58.2 |  1.487 % |
c |     40002 |  104219   371749 |  108126   39950  2596544    65.0 |  1.487 % |
c |     45768 |  104219   371749 |  118939   45716  2991024    65.4 |  1.487 % |
c ==============================================================================
c (current CPU-time: 252.726 s)
c ==============================================================================
c [1mFound solution: -5328[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     47845 |  104430   372422 |   31328   47793  3141612    65.7 |  1.487 % |
c   -- subsuming                       
c   -- var.elim.:  483/483          
c   -- var.elim.:  266/266          
c |     47845 |  104270   372587 |      --   47793       --      -- |     --   | -160/166
c |     47845 |  104270   372587 |   41708   47793  3141612    65.7 |  1.487 % |
c |     47945 |  104270   372587 |   45878   13966  1048197    75.1 |  1.492 % |
c |     48095 |  104270   372587 |   50466   14116  1053015    74.6 |  1.492 % |
c |     48320 |  104270   372587 |   55513   14341  1084860    75.6 |  1.492 % |
c |     48658 |  104270   372587 |   61064   14679  1093240    74.5 |  1.492 % |
c |     49164 |  104270   372587 |   67171   15185  1113745    73.3 |  1.492 % |
c |     49923 |  104270   372587 |   73888   15944  1138904    71.4 |  1.492 % |
c |     51062 |  104270   372587 |   81277   17083  1297848    76.0 |  1.492 % |
c |     52771 |  104270   372587 |   89404   18792  1394231    74.2 |  1.492 % |
c |     55333 |  104270   372587 |   98345   21354  1717863    80.4 |  1.492 % |
c |     59177 |  104259   372550 |  108168   25197  1891459    75.1 |  1.498 % |
c |     64945 |  104259   372550 |  118985   30965  2254232    72.8 |  1.498 % |
c |     73595 |  104259   372550 |  130883   39615  3328663    84.0 |  1.498 % |
c |     86569 |  104259   372550 |  143972   52589  4266909    81.1 |  1.498 % |
c ==============================================================================
c (current CPU-time: 437.482 s)
c ==============================================================================
c [1mFound solution: -6113[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     93979 |  104334   372811 |   31300   59999  5021871    83.7 |  1.498 % |
c   -- subsuming                       
c   -- var.elim.:  297/297          
c   -- var.elim.:  124/124          
c |     93979 |  104286   372987 |      --   59999       --      -- |     --   | -48/177
c |     93979 |  104286   372987 |   41714   59999  5021871    83.7 |  1.498 % |
c |     94079 |  104286   372987 |   45885   15603  1161399    74.4 |  1.503 % |
c |     94231 |  104286   372987 |   50474   15755  1168678    74.2 |  1.503 % |
c |     94456 |  104286   372987 |   55521   15980  1170733    73.3 |  1.503 % |
c |     94794 |  104286   372987 |   61074   16318  1199008    73.5 |  1.503 % |
c |     95301 |  104286   372987 |   67181   16825  1213582    72.1 |  1.503 % |
c |     96060 |  104286   372987 |   73899   17584  1269827    72.2 |  1.503 % |
c ==============================================================================
c (current CPU-time: 447.783 s)
c ==============================================================================
c [1mFound solution: -6408[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    2     Base: 3 2 3 3 5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     96526 |  104334   373126 |   31300   18050  1310090    72.6 |  1.503 % |
c   -- subsuming                       
c   -- var.elim.:  145/145          
c   -- var.elim.:  53/53          
c |     96526 |  104306   373117 |      --   18050       --      -- |     --   | -28/-8
c |     96526 |  104306   373117 |   41722   18050  1310090    72.6 |  1.503 % |
c |     96627 |  104306   373117 |   45894   18151  1313743    72.4 |  1.509 % |
c |     96778 |  104306   373117 |   50484   18302  1327316    72.5 |  1.509 % |
c |     97005 |  104306   373117 |   55532   18529  1331596    71.9 |  1.509 % |
c |     97343 |  104306   373117 |   61085   18867  1338522    70.9 |  1.509 % |
c |     97853 |  104306   373117 |   67194   19377  1379865    71.2 |  1.509 % |
c |     98615 |  104306   373117 |   73913   20139  1411311    70.1 |  1.509 % |
c |     99754 |  104306   373117 |   81305   21278  1553274    73.0 |  1.509 % |
c |    101462 |  104306   373117 |   89435   22986  1653911    72.0 |  1.509 % |
c |    104024 |  104306   373117 |   98379   25548  1885591    73.8 |  1.509 % |
c |    107868 |  104306   373117 |  108217   29392  2222881    75.6 |  1.509 % |
c |    113634 |  104306   373117 |  119038   35158  3170214    90.2 |  1.509 % |
c |    122283 |  104306   373117 |  130942   43807  4917619   112.3 |  1.509 % |
c |    135258 |  104306   373117 |  144037   56782  6944932   122.3 |  1.509 % |
c |    154719 |  104306   373117 |  158440   76243  8919404   117.0 |  1.509 % |
c |    183911 |  104306   373117 |  174284  105435 14215881   134.8 |  1.509 % |
c 
c *** TERMINATE#### 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.77 0.91 0.90 2/54 12170
Raw data (stat): 12170 (runsolver) R 12169 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488608503 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0002 s]
Raw data (loadavg): 0.81 0.92 0.90 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 4978 0 0 0 982 15 0 0 25 0 1 0 488608503 20520960 4147 4294967295 134512640 134672761 3221224544 3221222992 134606665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5010 4147 603 41 0 4969 0
vsize: 20040
[startup+19.9998 s]
Raw data (loadavg): 0.84 0.92 0.90 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 5242 0 0 0 1980 16 0 0 25 0 1 0 488608503 20758528 4202 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5068 4202 603 41 0 5027 0
vsize: 20272
[startup+30.0055 s]
Raw data (loadavg): 0.86 0.92 0.90 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 7556 0 0 0 2972 24 0 0 25 0 1 0 488608503 22962176 4765 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5606 4765 603 41 0 5565 0
vsize: 22424
[startup+40.0054 s]
Raw data (loadavg): 0.88 0.92 0.90 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 8151 0 0 0 3969 26 0 0 25 0 1 0 488608503 23891968 4939 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5833 4939 603 41 0 5792 0
vsize: 23332
[startup+50.0046 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 8810 0 0 0 4966 29 0 0 25 0 1 0 488608503 24162304 4992 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5899 4992 603 41 0 5858 0
vsize: 23596
[startup+60.0046 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 8810 0 0 0 5966 29 0 0 25 0 1 0 488608503 24162304 4992 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5899 4992 603 41 0 5858 0
vsize: 23596
[startup+70.0053 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 8845 0 0 0 6966 29 0 0 25 0 1 0 488608503 24162304 5027 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5899 5027 603 41 0 5858 0
vsize: 23596
[startup+80.0055 s]
Raw data (loadavg): 0.94 0.93 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 9018 0 0 0 7966 30 0 0 25 0 1 0 488608503 24821760 5200 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6060 5200 603 41 0 6019 0
vsize: 24240
[startup+90.0055 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 9251 0 0 0 8965 30 0 0 25 0 1 0 488608503 25751552 5433 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6287 5433 603 41 0 6246 0
vsize: 25148
[startup+100.005 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 10189 0 0 0 9960 34 0 0 25 0 1 0 488608503 27897856 5923 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6811 5923 603 41 0 6770 0
vsize: 27244
[startup+110.006 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 10793 0 0 0 10958 36 0 0 25 0 1 0 488608503 28569600 6100 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6975 6100 603 41 0 6934 0
vsize: 27900
[startup+120.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 10793 0 0 0 11957 36 0 0 25 0 1 0 488608503 28569600 6100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6975 6100 603 41 0 6934 0
vsize: 27900
[startup+130.006 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 11620 0 0 0 12954 39 0 0 25 0 1 0 488608503 30175232 6462 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7367 6462 603 41 0 7326 0
vsize: 29468
[startup+140.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 11620 0 0 0 13954 39 0 0 25 0 1 0 488608503 30175232 6462 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7367 6462 603 41 0 7326 0
vsize: 29468
[startup+150.006 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 11701 0 0 0 14954 39 0 0 25 0 1 0 488608503 30306304 6543 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7399 6543 603 41 0 7358 0
vsize: 29596
[startup+160.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 11903 0 0 0 15954 40 0 0 25 0 1 0 488608503 31100928 6745 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7593 6745 603 41 0 7552 0
vsize: 30372
[startup+170.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12068 0 0 0 16953 41 0 0 25 0 1 0 488608503 31760384 6910 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7754 6910 603 41 0 7713 0
vsize: 31016
[startup+180.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12213 0 0 0 17953 41 0 0 25 0 1 0 488608503 32411648 7055 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7913 7055 603 41 0 7872 0
vsize: 31652
[startup+190.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12361 0 0 0 18952 42 0 0 25 0 1 0 488608503 33071104 7203 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8074 7203 603 41 0 8033 0
vsize: 32296
[startup+200.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12486 0 0 0 19952 42 0 0 25 0 1 0 488608503 33472512 7328 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8172 7328 603 41 0 8131 0
vsize: 32688
[startup+210.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12582 0 0 0 20952 43 0 0 25 0 1 0 488608503 33873920 7424 4294967295 134512640 134672761 3221224544 3221223728 134615551 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8270 7424 603 41 0 8229 0
vsize: 33080
[startup+220.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12673 0 0 0 21952 43 0 0 25 0 1 0 488608503 34271232 7515 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8367 7515 603 41 0 8326 0
vsize: 33468
[startup+230.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12788 0 0 0 22952 43 0 0 25 0 1 0 488608503 34803712 7630 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8497 7630 603 41 0 8456 0
vsize: 33988
[startup+240.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12907 0 0 0 23952 43 0 0 25 0 1 0 488608503 35209216 7749 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8596 7749 603 41 0 8555 0
vsize: 34384
[startup+250.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 12996 0 0 0 24952 44 0 0 25 0 1 0 488608503 35602432 7838 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8692 7838 603 41 0 8651 0
vsize: 34768
[startup+260.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 25949 46 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223532 1075347104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+270.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 26949 46 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+280.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 27949 46 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223744 134610703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+290.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 28949 46 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+300.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 29949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+310.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 30949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+320.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 31949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223680 134614505 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+330.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 32949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+340.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 33949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+350.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 34949 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+360.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13825 0 0 0 35950 47 0 0 25 0 1 0 488608503 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+370.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 13890 0 0 0 36950 47 0 0 25 0 1 0 488608503 37416960 8282 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9135 8282 603 41 0 9094 0
vsize: 36540
[startup+380.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 14049 0 0 0 37949 47 0 0 25 0 1 0 488608503 38072320 8441 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9295 8441 603 41 0 9254 0
vsize: 37180
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 14405 0 0 0 38948 49 0 0 25 0 1 0 488608503 39542784 8797 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9654 8797 603 41 0 9613 0
vsize: 38616
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 14651 0 0 0 39947 50 0 0 25 0 1 0 488608503 40464384 9043 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9879 9043 603 41 0 9838 0
vsize: 39516
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 14830 0 0 0 40947 50 0 0 25 0 1 0 488608503 41254912 9222 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10072 9222 603 41 0 10031 0
vsize: 40288
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 15148 0 0 0 41946 51 0 0 25 0 1 0 488608503 42569728 9540 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10393 9540 603 41 0 10352 0
vsize: 41572
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 15478 0 0 0 42945 52 0 0 25 0 1 0 488608503 43896832 9870 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10717 9870 603 41 0 10676 0
vsize: 42868
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 16461 0 0 0 43942 55 0 0 25 0 1 0 488608503 46182400 10401 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11275 10401 603 41 0 11234 0
vsize: 45100
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 44940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 45940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 46940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 47940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+490.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 48940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 49940 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 50941 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+520.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 51941 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 52941 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 53941 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+550.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 54941 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 55942 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 56942 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+580.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 57942 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 58942 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 59942 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 60943 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223584 134612777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17135 0 0 0 61943 57 0 0 25 0 1 0 488608503 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17177 0 0 0 62943 58 0 0 25 0 1 0 488608503 45858816 10338 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11196 10338 603 41 0 11155 0
vsize: 44784
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17431 0 0 0 63942 58 0 0 25 0 1 0 488608503 46776320 10592 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11420 10592 603 41 0 11379 0
vsize: 45680
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17730 0 0 0 64941 59 0 0 25 0 1 0 488608503 48099328 10891 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11743 10891 603 41 0 11702 0
vsize: 46972
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 17916 0 0 0 65941 60 0 0 25 0 1 0 488608503 48885760 11077 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11935 11077 603 41 0 11894 0
vsize: 47740
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 18157 0 0 0 66941 60 0 0 25 0 1 0 488608503 49799168 11318 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12158 11318 603 41 0 12117 0
vsize: 48632
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 18401 0 0 0 67940 61 0 0 25 0 1 0 488608503 50843648 11562 4294967295 134512640 134672761 3221224544 3221223744 134610709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12413 11562 603 41 0 12372 0
vsize: 49652
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 18667 0 0 0 68940 62 0 0 25 0 1 0 488608503 51888128 11828 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12668 11828 603 41 0 12627 0
vsize: 50672
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 18940 0 0 0 69939 63 0 0 25 0 1 0 488608503 53075968 12101 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12958 12101 603 41 0 12917 0
vsize: 51832
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 19170 0 0 0 70939 63 0 0 25 0 1 0 488608503 54001664 12331 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13184 12331 603 41 0 13143 0
vsize: 52736
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 19356 0 0 0 71938 64 0 0 25 0 1 0 488608503 54665216 12517 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13346 12517 603 41 0 13305 0
vsize: 53384
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 19553 0 0 0 72938 65 0 0 25 0 1 0 488608503 55590912 12714 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13572 12714 603 41 0 13531 0
vsize: 54288
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 19812 0 0 0 73937 66 0 0 25 0 1 0 488608503 56901632 12973 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13892 12973 603 41 0 13851 0
vsize: 55568
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 20068 0 0 0 74936 67 0 0 25 0 1 0 488608503 57946112 13229 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14147 13229 603 41 0 14106 0
vsize: 56588
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 20247 0 0 0 75935 68 0 0 25 0 1 0 488608503 58609664 13408 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14309 13408 603 41 0 14268 0
vsize: 57236
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 20467 0 0 0 76934 69 0 0 25 0 1 0 488608503 59527168 13628 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14533 13628 603 41 0 14492 0
vsize: 58132
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 20701 0 0 0 77934 70 0 0 25 0 1 0 488608503 60444672 13862 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14757 13862 603 41 0 14716 0
vsize: 59028
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 20922 0 0 0 78933 70 0 0 25 0 1 0 488608503 61374464 14083 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14984 14083 603 41 0 14943 0
vsize: 59936
[startup+800.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 21115 0 0 0 79933 71 0 0 25 0 1 0 488608503 62173184 14276 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15179 14276 603 41 0 15138 0
vsize: 60716
[startup+810.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 21355 0 0 0 80932 72 0 0 25 0 1 0 488608503 63107072 14516 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15407 14516 603 41 0 15366 0
vsize: 61628
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 21541 0 0 0 81932 72 0 0 25 0 1 0 488608503 63897600 14702 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15600 14702 603 41 0 15559 0
vsize: 62400
[startup+830.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 21719 0 0 0 82932 72 0 0 25 0 1 0 488608503 64561152 14880 4294967295 134512640 134672761 3221224544 3221223728 134615581 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15762 14880 603 41 0 15721 0
vsize: 63048
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 21932 0 0 0 83932 73 0 0 25 0 1 0 488608503 65478656 15093 4294967295 134512640 134672761 3221224544 3221223584 134613025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15986 15093 603 41 0 15945 0
vsize: 63944
[startup+850.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 22215 0 0 0 84931 74 0 0 25 0 1 0 488608503 66658304 15376 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16274 15376 603 41 0 16233 0
vsize: 65096
[startup+860.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 22417 0 0 0 85930 74 0 0 25 0 1 0 488608503 67461120 15578 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16470 15578 603 41 0 16429 0
vsize: 65880
[startup+870.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 22669 0 0 0 86930 75 0 0 25 0 1 0 488608503 68509696 15830 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16726 15830 603 41 0 16685 0
vsize: 66904
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 22863 0 0 0 87929 76 0 0 25 0 1 0 488608503 69296128 16024 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16918 16024 603 41 0 16877 0
vsize: 67672
[startup+890.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 23065 0 0 0 88929 77 0 0 25 0 1 0 488608503 70086656 16226 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17111 16226 603 41 0 17070 0
vsize: 68444
[startup+900.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 23223 0 0 0 89928 77 0 0 25 0 1 0 488608503 70742016 16384 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17271 16384 603 41 0 17230 0
vsize: 69084
[startup+910.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 23523 0 0 0 90928 78 0 0 25 0 1 0 488608503 71925760 16684 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17560 16684 603 41 0 17519 0
vsize: 70240
[startup+920.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 23754 0 0 0 91927 79 0 0 25 0 1 0 488608503 72855552 16915 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17787 16915 603 41 0 17746 0
vsize: 71148
[startup+930.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 23953 0 0 0 92927 79 0 0 25 0 1 0 488608503 73781248 17114 4294967295 134512640 134672761 3221224544 3221223348 1075358820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18013 17114 603 41 0 17972 0
vsize: 72052
[startup+940.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 24113 0 0 0 93927 79 0 0 25 0 1 0 488608503 74305536 17274 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18141 17274 603 41 0 18100 0
vsize: 72564
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 24293 0 0 0 94927 80 0 0 25 0 1 0 488608503 75091968 17454 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18333 17454 603 41 0 18292 0
vsize: 73332
[startup+960.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 24522 0 0 0 95926 80 0 0 25 0 1 0 488608503 76013568 17683 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18558 17683 603 41 0 18517 0
vsize: 74232
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 24773 0 0 0 96926 81 0 0 25 0 1 0 488608503 77070336 17934 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18816 17934 603 41 0 18775 0
vsize: 75264
[startup+980.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 25024 0 0 0 97926 81 0 0 25 0 1 0 488608503 78123008 18185 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19073 18185 603 41 0 19032 0
vsize: 76292
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 25225 0 0 0 98926 82 0 0 25 0 1 0 488608503 78921728 18386 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19268 18386 603 41 0 19227 0
vsize: 77072
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 25420 0 0 0 99925 82 0 0 25 0 1 0 488608503 79712256 18581 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19461 18581 603 41 0 19420 0
vsize: 77844
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 25620 0 0 0 100924 83 0 0 25 0 1 0 488608503 80502784 18781 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19654 18781 603 41 0 19613 0
vsize: 78616
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 25826 0 0 0 101924 84 0 0 25 0 1 0 488608503 81420288 18987 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19878 18987 603 41 0 19837 0
vsize: 79512
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 26053 0 0 0 102923 85 0 0 25 0 1 0 488608503 82333696 19214 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20101 19214 603 41 0 20060 0
vsize: 80404
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 26368 0 0 0 103922 86 0 0 25 0 1 0 488608503 83542016 19529 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20396 19529 603 41 0 20355 0
vsize: 81584
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 26615 0 0 0 104922 86 0 0 25 0 1 0 488608503 84590592 19776 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20652 19776 603 41 0 20611 0
vsize: 82608
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 26782 0 0 0 105922 87 0 0 25 0 1 0 488608503 85254144 19943 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20814 19943 603 41 0 20773 0
vsize: 83256
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27017 0 0 0 106921 88 0 0 25 0 1 0 488608503 86179840 20178 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21040 20178 603 41 0 20999 0
vsize: 84160
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27212 0 0 0 107921 88 0 0 25 0 1 0 488608503 86978560 20373 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21235 20373 603 41 0 21194 0
vsize: 84940
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27370 0 0 0 108920 89 0 0 25 0 1 0 488608503 87646208 20531 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21398 20531 603 41 0 21357 0
vsize: 85592
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27513 0 0 0 109920 90 0 0 25 0 1 0 488608503 88301568 20674 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21558 20674 603 41 0 21517 0
vsize: 86232
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27715 0 0 0 110920 90 0 0 25 0 1 0 488608503 89096192 20876 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21752 20876 603 41 0 21711 0
vsize: 87008
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 27888 0 0 0 111919 91 0 0 25 0 1 0 488608503 89755648 21049 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21913 21049 603 41 0 21872 0
vsize: 87652
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28032 0 0 0 112919 91 0 0 25 0 1 0 488608503 90423296 21193 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22076 21193 603 41 0 22035 0
vsize: 88304
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28158 0 0 0 113918 92 0 0 25 0 1 0 488608503 90816512 21319 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22172 21319 603 41 0 22131 0
vsize: 88688
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28288 0 0 0 114918 93 0 0 25 0 1 0 488608503 91340800 21449 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22300 21449 603 41 0 22259 0
vsize: 89200
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28422 0 0 0 115918 93 0 0 25 0 1 0 488608503 92000256 21583 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22461 21583 603 41 0 22420 0
vsize: 89844
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28599 0 0 0 116918 93 0 0 25 0 1 0 488608503 92663808 21760 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22623 21760 603 41 0 22582 0
vsize: 90492
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 28823 0 0 0 117917 94 0 0 25 0 1 0 488608503 94109696 21984 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22976 21984 603 41 0 22935 0
vsize: 91904
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 29025 0 0 0 118916 95 0 0 25 0 1 0 488608503 94924800 22186 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23175 22186 603 41 0 23134 0
vsize: 92700
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12170
Raw data (stat): 12170 (minisat+) R 12169 22932 22931 0 -1 0 29191 0 0 0 119916 96 0 0 25 0 1 0 488608503 95584256 22352 4294967295 134512640 134672761 3221224544 3221223728 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23336 22352 603 41 0 23295 0
vsize: 93344
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 12170
Raw data (stat): 12170 (minisat+) Z 12169 22932 22931 0 -1 12 29192 0 0 0 119916 100 0 0 25 0 1 0 488608503 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.17
CPU user time (s): 1199.16
CPU system time (s): 1.00485
CPU usage (%): 100.009
Max. virtual memory (Kb): 93344
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####