PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.01784
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 21984

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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:        297852 kB
Buffers:         27000 kB
Cached:         686512 kB
SwapCached:        556 kB
Active:          37412 kB
Inactive:       678056 kB
HighTotal:      131008 kB
HighFree:        13888 kB
LowTotal:       903652 kB
LowFree:        283964 kB
SwapTotal:     2097892 kB
SwapFree:      2096428 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5096 kB
Slab:            15692 kB
Committed_AS:    63604 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:03:07 (client local time) WITH STATUS 10 IN 1200.2 SECONDS
stats: 12270 7 1200.2 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.16361 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.2893 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.3518 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.2695 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: 36.8094 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.4457 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: 92.8319 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: 100.595 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: 123.334 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: 249.492 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: 431.916 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: 442.113 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 *** TERMINAT#### 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.92 2/54 11188
Raw data (stat): 11188 (runsolver) R 11187 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549846586 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0005 s]
Raw data (loadavg): 0.80 0.91 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 4978 0 0 0 985 13 0 0 25 0 1 0 549846586 20520960 4147 4294967295 134512640 134672761 3221224544 3221222720 134604158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5010 4147 603 41 0 4969 0
vsize: 20040
[startup+20.0002 s]
Raw data (loadavg): 0.83 0.91 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 5243 0 0 0 1983 14 0 0 25 0 1 0 549846586 20758528 4203 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5068 4203 603 41 0 5027 0
vsize: 20272
[startup+30.0011 s]
Raw data (loadavg): 0.86 0.92 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 7556 0 0 0 2976 21 0 0 25 0 1 0 549846586 22962176 4765 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5606 4765 603 41 0 5565 0
vsize: 22424
[startup+40.0011 s]
Raw data (loadavg): 0.88 0.92 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 8151 0 0 0 3973 23 0 0 25 0 1 0 549846586 23891968 4939 4294967295 134512640 134672761 3221224544 3221223728 134615683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5833 4939 603 41 0 5792 0
vsize: 23332
[startup+50.0016 s]
Raw data (loadavg): 0.90 0.92 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 8810 0 0 0 4971 25 0 0 25 0 1 0 549846586 24162304 4992 4294967295 134512640 134672761 3221224544 3221223680 134614710 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5899 4992 603 41 0 5858 0
vsize: 23596
[startup+60.0017 s]
Raw data (loadavg): 0.91 0.92 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 8810 0 0 0 5971 25 0 0 25 0 1 0 549846586 24162304 4992 4294967295 134512640 134672761 3221224544 3221223584 134612992 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5899 4992 603 41 0 5858 0
vsize: 23596
[startup+70.0015 s]
Raw data (loadavg): 0.92 0.92 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 8852 0 0 0 6971 25 0 0 25 0 1 0 549846586 24162304 5034 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5899 5034 603 41 0 5858 0
vsize: 23596
[startup+80.0019 s]
Raw data (loadavg): 0.94 0.93 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 9037 0 0 0 7971 26 0 0 25 0 1 0 549846586 24821760 5219 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6060 5219 603 41 0 6019 0
vsize: 24240
[startup+90.002 s]
Raw data (loadavg): 0.95 0.93 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 9274 0 0 0 8970 27 0 0 25 0 1 0 549846586 25882624 5456 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6319 5456 603 41 0 6278 0
vsize: 25276
[startup+100.003 s]
Raw data (loadavg): 0.95 0.93 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 10189 0 0 0 9966 30 0 0 25 0 1 0 549846586 27897856 5923 4294967295 134512640 134672761 3221224544 3221223728 134615791 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.004 s]
Raw data (loadavg): 0.96 0.93 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 10793 0 0 0 10964 32 0 0 25 0 1 0 549846586 28569600 6100 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6975 6100 603 41 0 6934 0
vsize: 27900
[startup+120.004 s]
Raw data (loadavg): 0.97 0.93 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 10793 0 0 0 11964 32 0 0 25 0 1 0 549846586 28569600 6100 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6975 6100 603 41 0 6934 0
vsize: 27900
[startup+130.005 s]
Raw data (loadavg): 0.97 0.94 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 11620 0 0 0 12962 34 0 0 25 0 1 0 549846586 30175232 6462 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7367 6462 603 41 0 7326 0
vsize: 29468
[startup+140.006 s]
Raw data (loadavg): 0.97 0.94 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 11620 0 0 0 13962 34 0 0 25 0 1 0 549846586 30175232 6462 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7367 6462 603 41 0 7326 0
vsize: 29468
[startup+150.007 s]
Raw data (loadavg): 0.98 0.94 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 11738 0 0 0 14962 34 0 0 25 0 1 0 549846586 30437376 6580 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7431 6580 603 41 0 7390 0
vsize: 29724
[startup+160.008 s]
Raw data (loadavg): 0.98 0.94 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 11934 0 0 0 15962 35 0 0 25 0 1 0 549846586 31232000 6776 4294967295 134512640 134672761 3221224544 3221223680 134614756 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7625 6776 603 41 0 7584 0
vsize: 30500
[startup+170.008 s]
Raw data (loadavg): 0.98 0.94 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 12105 0 0 0 16962 35 0 0 25 0 1 0 549846586 32018432 6947 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7817 6947 603 41 0 7776 0
vsize: 31268
[startup+180.008 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 12257 0 0 0 17961 36 0 0 25 0 1 0 549846586 32542720 7099 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7945 7099 603 41 0 7904 0
vsize: 31780
[startup+190.008 s]
Raw data (loadavg): 0.99 0.94 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 12387 0 0 0 18960 37 0 0 25 0 1 0 549846586 33071104 7229 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8074 7229 603 41 0 8033 0
vsize: 32296
[startup+200.008 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 12512 0 0 0 19960 37 0 0 25 0 1 0 549846586 33607680 7354 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8205 7354 603 41 0 8164 0
vsize: 32820
[startup+210.008 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 12611 0 0 0 20960 37 0 0 25 0 1 0 549846586 34009088 7453 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8303 7453 603 41 0 8262 0
vsize: 33212
[startup+220.008 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 12710 0 0 0 21960 38 0 0 25 0 1 0 549846586 34406400 7552 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8400 7552 603 41 0 8359 0
vsize: 33600
[startup+230.009 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 12841 0 0 0 22960 38 0 0 25 0 1 0 549846586 34938880 7683 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8530 7683 603 41 0 8489 0
vsize: 34120
[startup+240.009 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 12936 0 0 0 23960 38 0 0 25 0 1 0 549846586 35340288 7778 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8628 7778 603 41 0 8587 0
vsize: 34512
[startup+250.009 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13697 0 0 0 24958 40 0 0 25 0 1 0 549846586 39555072 8539 4294967295 134512640 134672761 3221224544 3221222988 1075278826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9657 8539 603 41 0 9616 0
vsize: 38628
[startup+260.011 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13825 0 0 0 25956 41 0 0 25 0 1 0 549846586 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.011 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13825 0 0 0 26956 41 0 0 25 0 1 0 549846586 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134616006 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+280.012 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13825 0 0 0 27957 41 0 0 25 0 1 0 549846586 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+290.012 s]
Raw data (loadavg): 0.99 0.95 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13825 0 0 0 28957 41 0 0 25 0 1 0 549846586 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+300.013 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13825 0 0 0 29956 41 0 0 25 0 1 0 549846586 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.013 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13825 0 0 0 30957 41 0 0 25 0 1 0 549846586 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+320.013 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13825 0 0 0 31957 41 0 0 25 0 1 0 549846586 37285888 8217 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+330.014 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13825 0 0 0 32957 41 0 0 25 0 1 0 549846586 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+340.014 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13825 0 0 0 33957 41 0 0 25 0 1 0 549846586 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+350.014 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13825 0 0 0 34957 41 0 0 25 0 1 0 549846586 37285888 8217 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8217 603 41 0 9062 0
vsize: 36412
[startup+360.015 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13836 0 0 0 35958 42 0 0 25 0 1 0 549846586 37285888 8228 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9103 8228 603 41 0 9062 0
vsize: 36412
[startup+370.015 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 13969 0 0 0 36957 42 0 0 25 0 1 0 549846586 37679104 8361 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9199 8361 603 41 0 9158 0
vsize: 36796
[startup+380.015 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 14208 0 0 0 37956 43 0 0 25 0 1 0 549846586 38735872 8600 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9457 8600 603 41 0 9416 0
vsize: 37828
[startup+390.022 s]
Raw data (loadavg): 0.99 0.96 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 14558 0 0 0 38957 44 0 0 25 0 1 0 549846586 40067072 8950 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9782 8950 603 41 0 9741 0
vsize: 39128
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 14748 0 0 0 39956 44 0 0 25 0 1 0 549846586 40861696 9140 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9976 9140 603 41 0 9935 0
vsize: 39904
[startup+410.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 15022 0 0 0 40956 45 0 0 25 0 1 0 549846586 42045440 9414 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10265 9414 603 41 0 10224 0
vsize: 41060
[startup+420.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 15340 0 0 0 41955 46 0 0 25 0 1 0 549846586 43368448 9732 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10588 9732 603 41 0 10547 0
vsize: 42352
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 15611 0 0 0 42955 46 0 0 25 0 1 0 549846586 44429312 10003 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10847 10003 603 41 0 10806 0
vsize: 43388
[startup+440.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 16461 0 0 0 43953 48 0 0 25 0 1 0 549846586 46182400 10401 4294967295 134512640 134672761 3221224544 3221223584 134612851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11275 10401 603 41 0 11234 0
vsize: 45100
[startup+450.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 44951 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 45951 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+470.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 46951 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+480.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 47951 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+490.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 48951 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 49952 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 50952 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+520.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 51952 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 52952 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+540.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 53952 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+550.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 54953 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 55953 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+570.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 56953 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 57953 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 58953 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 59954 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 60954 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+620.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17135 0 0 0 61954 50 0 0 25 0 1 0 549846586 45592576 10296 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11131 10296 603 41 0 11090 0
vsize: 44524
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17390 0 0 0 62953 52 0 0 25 0 1 0 549846586 46645248 10551 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11388 10551 603 41 0 11347 0
vsize: 45552
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17687 0 0 0 63952 52 0 0 25 0 1 0 549846586 47833088 10848 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11678 10848 603 41 0 11637 0
vsize: 46712
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 17889 0 0 0 64952 53 0 0 25 0 1 0 549846586 48754688 11050 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11903 11050 603 41 0 11862 0
vsize: 47612
[startup+660.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 18130 0 0 0 65951 54 0 0 25 0 1 0 549846586 49668096 11291 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12126 11291 603 41 0 12085 0
vsize: 48504
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 18370 0 0 0 66951 54 0 0 25 0 1 0 549846586 50712576 11531 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12381 11531 603 41 0 12340 0
vsize: 49524
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 18656 0 0 0 67951 55 0 0 25 0 1 0 549846586 51888128 11817 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12668 11817 603 41 0 12627 0
vsize: 50672
[startup+690.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 18920 0 0 0 68950 55 0 0 25 0 1 0 549846586 52940800 12081 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12925 12081 603 41 0 12884 0
vsize: 51700
[startup+700.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 19159 0 0 0 69950 56 0 0 25 0 1 0 549846586 53866496 12320 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13151 12320 603 41 0 13110 0
vsize: 52604
[startup+710.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 19344 0 0 0 70950 56 0 0 25 0 1 0 549846586 54665216 12505 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12505 603 41 0 13305 0
vsize: 53384
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 19542 0 0 0 71949 57 0 0 25 0 1 0 549846586 55455744 12703 4294967295 134512640 134672761 3221224544 3221223680 134614674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13539 12703 603 41 0 13498 0
vsize: 54156
[startup+730.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 19806 0 0 0 72948 58 0 0 25 0 1 0 549846586 56770560 12967 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13860 12967 603 41 0 13819 0
vsize: 55440
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 20065 0 0 0 73948 59 0 0 25 0 1 0 549846586 57815040 13226 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14115 13226 603 41 0 14074 0
vsize: 56460
[startup+750.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 20247 0 0 0 74947 60 0 0 25 0 1 0 549846586 58609664 13408 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14309 13408 603 41 0 14268 0
vsize: 57236
[startup+760.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 20468 0 0 0 75947 60 0 0 25 0 1 0 549846586 59527168 13629 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14533 13629 603 41 0 14492 0
vsize: 58132
[startup+770.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 20707 0 0 0 76946 61 0 0 25 0 1 0 549846586 60444672 13868 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14757 13868 603 41 0 14716 0
vsize: 59028
[startup+780.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 20927 0 0 0 77946 62 0 0 25 0 1 0 549846586 61374464 14088 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14984 14088 603 41 0 14943 0
vsize: 59936
[startup+790.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 21131 0 0 0 78945 63 0 0 25 0 1 0 549846586 62173184 14292 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15179 14292 603 41 0 15138 0
vsize: 60716
[startup+800.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 21365 0 0 0 79944 64 0 0 25 0 1 0 549846586 63107072 14526 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15407 14526 603 41 0 15366 0
vsize: 61628
[startup+810.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 21557 0 0 0 80944 64 0 0 25 0 1 0 549846586 63897600 14718 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15600 14718 603 41 0 15559 0
vsize: 62400
[startup+820.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 21732 0 0 0 81943 65 0 0 25 0 1 0 549846586 64692224 14893 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15794 14893 603 41 0 15753 0
vsize: 63176
[startup+830.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 21964 0 0 0 82943 65 0 0 25 0 1 0 549846586 65609728 15125 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16018 15125 603 41 0 15977 0
vsize: 64072
[startup+840.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 22266 0 0 0 83943 66 0 0 25 0 1 0 549846586 66789376 15427 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16306 15427 603 41 0 16265 0
vsize: 65224
[startup+850.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 22442 0 0 0 84942 67 0 0 25 0 1 0 549846586 67592192 15603 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16502 15603 603 41 0 16461 0
vsize: 66008
[startup+860.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 22695 0 0 0 85941 68 0 0 25 0 1 0 549846586 68640768 15856 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16758 15856 603 41 0 16717 0
vsize: 67032
[startup+870.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 22900 0 0 0 86941 68 0 0 25 0 1 0 549846586 69427200 16061 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16950 16061 603 41 0 16909 0
vsize: 67800
[startup+880.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 23098 0 0 0 87940 69 0 0 25 0 1 0 549846586 70217728 16259 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17143 16259 603 41 0 17102 0
vsize: 68572
[startup+890.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 23277 0 0 0 88940 69 0 0 25 0 1 0 549846586 71000064 16438 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17334 16438 603 41 0 17293 0
vsize: 69336
[startup+900.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 23593 0 0 0 89940 70 0 0 25 0 1 0 549846586 72187904 16754 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17624 16754 603 41 0 17583 0
vsize: 70496
[startup+910.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 23816 0 0 0 90939 71 0 0 25 0 1 0 549846586 73117696 16977 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17851 16977 603 41 0 17810 0
vsize: 71404
[startup+920.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 23998 0 0 0 91939 71 0 0 25 0 1 0 549846586 73912320 17159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18045 17159 603 41 0 18004 0
vsize: 72180
[startup+930.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 24171 0 0 0 92938 72 0 0 25 0 1 0 549846586 74567680 17332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18205 17332 603 41 0 18164 0
vsize: 72820
[startup+940.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 24376 0 0 0 93938 72 0 0 25 0 1 0 549846586 75485184 17537 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18429 17537 603 41 0 18388 0
vsize: 73716
[startup+950.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 24617 0 0 0 94937 74 0 0 25 0 1 0 549846586 76406784 17778 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18654 17778 603 41 0 18613 0
vsize: 74616
[startup+960.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 24870 0 0 0 95937 74 0 0 25 0 1 0 549846586 77467648 18031 4294967295 134512640 134672761 3221224544 3221223648 134604307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18913 18031 603 41 0 18872 0
vsize: 75652
[startup+970.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 25093 0 0 0 96936 75 0 0 25 0 1 0 549846586 78393344 18254 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19139 18254 603 41 0 19098 0
vsize: 76556
[startup+980.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 25293 0 0 0 97936 75 0 0 25 0 1 0 549846586 79183872 18454 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19332 18454 603 41 0 19291 0
vsize: 77328
[startup+990.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 25493 0 0 0 98935 76 0 0 25 0 1 0 549846586 79970304 18654 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19524 18654 603 41 0 19483 0
vsize: 78096
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 25692 0 0 0 99935 76 0 0 25 0 1 0 549846586 80764928 18853 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19718 18853 603 41 0 19677 0
vsize: 78872
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 11188
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 25925 0 0 0 100935 77 0 0 25 0 1 0 549846586 81809408 19086 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19973 19086 603 41 0 19932 0
vsize: 79892
[startup+1020.04 s]
Raw data (loadavg): 1.15 1.00 0.93 2/56 11227
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 26186 0 0 0 101935 77 0 0 25 0 1 0 549846586 82890752 19347 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20237 19347 603 41 0 20196 0
vsize: 80948
[startup+1030.04 s]
Raw data (loadavg): 1.13 1.00 0.93 2/54 11241
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 26493 0 0 0 102933 79 0 0 25 0 1 0 549846586 84074496 19654 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20526 19654 603 41 0 20485 0
vsize: 82104
[startup+1040.04 s]
Raw data (loadavg): 1.11 1.00 0.93 2/54 11241
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 26686 0 0 0 103932 80 0 0 25 0 1 0 549846586 84860928 19847 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20718 19847 603 41 0 20677 0
vsize: 82872
[startup+1050.04 s]
Raw data (loadavg): 1.09 1.00 0.93 2/54 11241
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 26882 0 0 0 104931 81 0 0 25 0 1 0 549846586 85647360 20043 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20910 20043 603 41 0 20869 0
vsize: 83640
[startup+1060.04 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 11241
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 27075 0 0 0 105930 82 0 0 25 0 1 0 549846586 86441984 20236 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21104 20236 603 41 0 21063 0
vsize: 84416
[startup+1070.04 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 11241
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 27296 0 0 0 106929 83 0 0 25 0 1 0 549846586 87379968 20457 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21333 20457 603 41 0 21292 0
vsize: 85332
[startup+1080.04 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 11241
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 27449 0 0 0 107929 84 0 0 25 0 1 0 549846586 88039424 20610 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21494 20610 603 41 0 21453 0
vsize: 85976
[startup+1090.04 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 11241
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 27619 0 0 0 108928 85 0 0 25 0 1 0 549846586 88698880 20780 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21655 20780 603 41 0 21614 0
vsize: 86620
[startup+1100.04 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 11243
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 27801 0 0 0 109927 87 0 0 25 0 1 0 549846586 89358336 20962 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21816 20962 603 41 0 21775 0
vsize: 87264
[startup+1110.04 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 11243
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 27963 0 0 0 110926 87 0 0 25 0 1 0 549846586 90017792 21124 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21977 21124 603 41 0 21936 0
vsize: 87908
[startup+1120.04 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 11243
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 28110 0 0 0 111925 89 0 0 25 0 1 0 549846586 90685440 21271 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22140 21271 603 41 0 22099 0
vsize: 88560
[startup+1130.04 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 11243
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 28230 0 0 0 112924 89 0 0 25 0 1 0 549846586 91209728 21391 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22268 21391 603 41 0 22227 0
vsize: 89072
[startup+1140.04 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 11243
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 28373 0 0 0 113924 90 0 0 25 0 1 0 549846586 91738112 21534 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22397 21534 603 41 0 22356 0
vsize: 89588
[startup+1150.04 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 11243
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 28543 0 0 0 114922 92 0 0 25 0 1 0 549846586 92401664 21704 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22559 21704 603 41 0 22518 0
vsize: 90236
[startup+1160.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 11243
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 28728 0 0 0 115921 93 0 0 25 0 1 0 549846586 93188096 21889 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22751 21889 603 41 0 22710 0
vsize: 91004
[startup+1170.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 11243
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 28930 0 0 0 116920 94 0 0 25 0 1 0 549846586 94531584 22091 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23079 22091 603 41 0 23038 0
vsize: 92316
[startup+1180.05 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 11243
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 29110 0 0 0 117920 95 0 0 25 0 1 0 549846586 95322112 22271 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23272 22271 603 41 0 23231 0
vsize: 93088
[startup+1190.05 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 11243
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 29282 0 0 0 118919 96 0 0 25 0 1 0 549846586 95981568 22443 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23433 22443 603 41 0 23392 0
vsize: 93732
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 11243
Raw data (stat): 11188 (minisat+) R 11187 27222 27221 0 -1 0 29444 0 0 0 119918 97 0 0 25 0 1 0 549846586 96665600 22605 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23600 22605 603 41 0 23559 0
vsize: 94400
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 11243
Raw data (stat): 11188 (minisat+) Z 11187 27222 27221 0 -1 12 29445 0 0 0 119918 101 0 0 25 0 1 0 549846586 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.09
CPU time (s): 1200.2
CPU user time (s): 1199.19
CPU system time (s): 1.01784
CPU usage (%): 100.009
Max. virtual memory (Kb): 94400
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####