PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii32b1.opb
MD5SUM	c4653389ddee2820797c664a0856c651
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	191
Optimality of the best value was proved	NO
Number of terms in the objective function	456
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	456
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	456
Number of bits of the biggest sum of numbers	9
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.02784
Number of variables	456
Total number of constraints	1602
Number of constraints which are clauses	1602
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	0
Minimum length of a constraint	2
Maximum length of a constraint	32
Trace number 5466

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        906592 kB
Buffers:         34732 kB
Cached:          73676 kB
SwapCached:        392 kB
Active:          53708 kB
Inactive:        57940 kB
HighTotal:      131008 kB
HighFree:        53452 kB
LowTotal:       903652 kB
LowFree:        853140 kB
SwapTotal:     2097136 kB
SwapFree:      2096744 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            10804 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 00:23:59 (client local time) WITH STATUS 30 IN 1017.35 SECONDS
stats: 3907 0 1017.35 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 1602 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |    1602     6636 |     480       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  456/456          
c |         0 |    1602     6636 |     640       0        0     nan |  0.000 % |
c ==============================================================================
c (current CPU-time: 0.082987 s)
c ==============================================================================
c [1mFound solution: 216[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:17164     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |        38 |   22077    54533 |    6623      38     1984    52.2 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13722          
c   -- var.elim.:  2000/13722          
c   -- var.elim.:  3000/13722          
c   -- var.elim.:  4000/13722          
c   -- var.elim.:  5000/13722          
c   -- var.elim.:  6000/13722          
c   -- var.elim.:  7000/13722          
c   -- var.elim.:  8000/13722          
c   -- var.elim.:  9000/13722          
c   -- var.elim.:  10000/13722          
c   -- var.elim.:  11000/13722          
c   -- var.elim.:  12000/13722          
c   -- var.elim.:  13000/13722          
c   -- var.elim.:  13722/13722          
c   -- var.elim.:  1000/6717          
c   -- var.elim.:  2000/6717          
c   -- var.elim.:  3000/6717          
c   -- var.elim.:  4000/6717          
c   -- var.elim.:  5000/6717          
c   -- var.elim.:  6000/6717          
c   -- var.elim.:  6717/6717          
c   -- var.elim.:  1000/3929          
c   -- var.elim.:  2000/3929          
c   -- var.elim.:  3000/3929          
c   -- var.elim.:  3929/3929          
c   -- var.elim.:  1000/2772          
c   -- var.elim.:  2000/2772          
c   -- var.elim.:  2772/2772          
c   -- var.elim.:  1000/2052          
c   -- var.elim.:  2000/2052          
c   -- var.elim.:  2052/2052          
c   -- var.elim.:  1000/1111          
c   -- var.elim.:  1111/1111          
c   -- var.elim.:  143/143          
c   -- var.elim.:  18/18          
c   -- subsuming                       
c   -- var.elim.:  1000/2096          
c   -- var.elim.:  2000/2096          
c   -- var.elim.:  2096/2096          
c   -- var.elim.:  40/40          
c |        38 |    7109    40482 |      --      38       --      -- |     --   | -14960/-14027
c |        38 |    7109    40482 |    2843      38     1984    52.2 |  0.000 % |
c ==============================================================================
c (current CPU-time: 7.34488 s)
c ==============================================================================
c [1mFound solution: 196[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       116 |   22238    77582 |    6671     116    17735   152.9 |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/13591          
c   -- var.elim.:  2000/13591          
c   -- var.elim.:  3000/13591          
c   -- var.elim.:  4000/13591          
c   -- var.elim.:  5000/13591          
c   -- var.elim.:  6000/13591          
c   -- var.elim.:  7000/13591          
c   -- var.elim.:  8000/13591          
c   -- var.elim.:  9000/13591          
c   -- var.elim.:  10000/13591          
c   -- var.elim.:  11000/13591          
c   -- var.elim.:  12000/13591          
c   -- var.elim.:  13000/13591          
c   -- var.elim.:  13591/13591          
c   -- var.elim.:  1000/6537          
c   -- var.elim.:  2000/6537          
c   -- var.elim.:  3000/6537          
c   -- var.elim.:  4000/6537          
c   -- var.elim.:  5000/6537          
c   -- var.elim.:  6000/6537          
c   -- var.elim.:  6537/6537          
c   -- var.elim.:  1000/3846          
c   -- var.elim.:  2000/3846          
c   -- var.elim.:  3000/3846          
c   -- var.elim.:  3846/3846          
c   -- var.elim.:  1000/2912          
c   -- var.elim.:  2000/2912          
c   -- var.elim.:  2912/2912          
c   -- var.elim.:  1000/2458          
c   -- var.elim.:  2000/2458          
c   -- var.elim.:  2458/2458          
c   -- var.elim.:  1000/2137          
c   -- var.elim.:  2000/2137          
c   -- var.elim.:  2137/2137          
c   -- var.elim.:  1000/1304          
c   -- var.elim.:  1304/1304          
c   -- var.elim.:  135/135          
c   -- subsuming                       
c   -- var.elim.:  1000/1309          
c   -- var.elim.:  1309/1309          
c   -- var.elim.:  7/7          
c |       116 |    7473    44157 |      --     116       --      -- |     --   | -14755/-32992
c |       116 |    7473    44157 |    2989     116    17735   152.9 |  0.000 % |
c |       216 |    7473    44157 |    3288     216    41911   194.0 |  0.505 % |
c |       366 |    7473    44157 |    3616     366    93241   254.8 |  0.505 % |
c |       592 |    7320    43156 |    3897     584   147820   253.1 |  2.334 % |
c ==============================================================================
c (current CPU-time: 15.7056 s)
c ==============================================================================
c [1mFound solution: 195[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       719 |   19828    73725 |    5948     710   183276   258.1 |  2.334 % |
c   -- subsuming                       
c   -- var.elim.:  1000/11800          
c   -- var.elim.:  2000/11800          
c   -- var.elim.:  3000/11800          
c   -- var.elim.:  4000/11800          
c   -- var.elim.:  5000/11800          
c   -- var.elim.:  6000/11800          
c   -- var.elim.:  7000/11800          
c   -- var.elim.:  8000/11800          
c   -- var.elim.:  9000/11800          
c   -- var.elim.:  10000/11800          
c   -- var.elim.:  11000/11800          
c   -- var.elim.:  11800/11800          
c   -- var.elim.:  1000/5636          
c   -- var.elim.:  2000/5636          
c   -- var.elim.:  3000/5636          
c   -- var.elim.:  4000/5636          
c   -- var.elim.:  5000/5636          
c   -- var.elim.:  5636/5636          
c   -- var.elim.:  1000/3411          
c   -- var.elim.:  2000/3411          
c   -- var.elim.:  3000/3411          
c   -- var.elim.:  3411/3411          
c   -- var.elim.:  1000/2261          
c   -- var.elim.:  2000/2261          
c   -- var.elim.:  2261/2261          
c   -- var.elim.:  1000/1735          
c   -- var.elim.:  1735/1735          
c   -- var.elim.:  834/834          
c   -- var.elim.:  196/196          
c   -- var.elim.:  10/10          
c   -- subsuming                       
c   -- var.elim.:  552/552          
c |       719 |    7327    43828 |      --     710       --      -- |     --   | -12494/-29882
c |       719 |    7327    43828 |    2930     458    54755   119.6 |  2.334 % |
c |       819 |    7307    43690 |    3215     557    85245   153.0 |  3.574 % |
c ==============================================================================
c (current CPU-time: 22.3136 s)
c ==============================================================================
c [1mFound solution: 193[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |       886 |   20937    76993 |    6281     623   101935   163.6 |  3.574 % |
c   -- subsuming                       
c   -- var.elim.:  1000/12530          
c   -- var.elim.:  2000/12530          
c   -- var.elim.:  3000/12530          
c   -- var.elim.:  4000/12530          
c   -- var.elim.:  5000/12530          
c   -- var.elim.:  6000/12530          
c   -- var.elim.:  7000/12530          
c   -- var.elim.:  8000/12530          
c   -- var.elim.:  9000/12530          
c   -- var.elim.:  10000/12530          
c   -- var.elim.:  11000/12530          
c   -- var.elim.:  12000/12530          
c   -- var.elim.:  12530/12530          
c   -- var.elim.:  1000/5893          
c   -- var.elim.:  2000/5893          
c   -- var.elim.:  3000/5893          
c   -- var.elim.:  4000/5893          
c   -- var.elim.:  5000/5893          
c   -- var.elim.:  5893/5893          
c   -- var.elim.:  1000/3645          
c   -- var.elim.:  2000/3645          
c   -- var.elim.:  3000/3645          
c   -- var.elim.:  3645/3645          
c   -- var.elim.:  1000/2584          
c   -- var.elim.:  2000/2584          
c   -- var.elim.:  2584/2584          
c   -- var.elim.:  1000/1979          
c   -- var.elim.:  1979/1979          
c   -- var.elim.:  1000/1662          
c   -- var.elim.:  1662/1662          
c   -- var.elim.:  567/567          
c   -- var.elim.:  10/10          
c   -- subsuming                       
c   -- var.elim.:  585/585          
c |       886 |    7321    44685 |      --     623       --      -- |     --   | -13612/-32299
c |       886 |    7321    44685 |    2928     623   101935   163.6 |  3.574 % |
c |       987 |    7258    44248 |    3193     722   134998   187.0 |  5.116 % |
c |      1139 |    7229    44002 |    3498     873   190295   218.0 |  5.455 % |
c |      1364 |    7229    44002 |    3848    1098   271836   247.6 |  5.455 % |
c |      1701 |    7050    42449 |    4128    1429   422927   296.0 |  7.766 % |
c |      2207 |    7020    42295 |    4522    1930   518841   268.8 |  8.136 % |
c |      2969 |    7018    42289 |    4973    2691   716266   266.2 |  8.166 % |
c ==============================================================================
c (current CPU-time: 35.5286 s)
c ==============================================================================
c [1mFound solution: 192[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |      3819 |   17236    67195 |    5170    3540  1094151   309.1 |  8.166 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10066          
c   -- var.elim.:  2000/10066          
c   -- var.elim.:  3000/10066          
c   -- var.elim.:  4000/10066          
c   -- var.elim.:  5000/10066          
c   -- var.elim.:  6000/10066          
c   -- var.elim.:  7000/10066          
c   -- var.elim.:  8000/10066          
c   -- var.elim.:  9000/10066          
c   -- var.elim.:  10000/10066          
c   -- var.elim.:  10066/10066          
c   -- var.elim.:  1000/4532          
c   -- var.elim.:  2000/4532          
c   -- var.elim.:  3000/4532          
c   -- var.elim.:  4000/4532          
c   -- var.elim.:  4532/4532          
c   -- var.elim.:  1000/2695          
c   -- var.elim.:  2000/2695          
c   -- var.elim.:  2695/2695          
c   -- var.elim.:  1000/1740          
c   -- var.elim.:  1740/1740          
c   -- var.elim.:  1000/1305          
c   -- var.elim.:  1305/1305          
c   -- var.elim.:  853/853          
c   -- var.elim.:  11/11          
c   -- subsuming                       
c   -- var.elim.:  716/716          
c   -- var.elim.:  5/5          
c |      3819 |    6964    41380 |      --    3540       --      -- |     --   | -10232/-24400
c |      3819 |    6964    41380 |    2785    1639   131219    80.1 |  8.166 % |
c |      3919 |    6964    41380 |    3064    1739   153800    88.4 | 10.333 % |
c |      4070 |    6928    41098 |    3353    1889   205750   108.9 | 10.814 % |
c |      4297 |    6851    40505 |    3647    2113   266632   126.2 | 11.835 % |
c |      4637 |    6825    40343 |    3996    2451   375837   153.3 | 12.136 % |
c |      5146 |    6825    40343 |    4396    2960   437957   148.0 | 12.136 % |
c |      5906 |    6825    40343 |    4836    3720   540219   145.2 | 12.136 % |
c |      7045 |    6502    38230 |    5068    4844   941340   194.3 | 16.461 % |
c |      8753 |    6212    36258 |    5326    4493  1195545   266.1 | 19.976 % |
c |     11315 |    5973    33673 |    5633    7042  1938017   275.2 | 22.890 % |
c |     15159 |    5867    32945 |    6086    6075  1773236   291.9 | 24.302 % |
c |     20927 |    5221    28368 |    5958    6946  1796209   258.6 | 32.863 % |
c ==============================================================================
c (current CPU-time: 99.0399 s)
c ==============================================================================
c [1mFound solution: 191[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |     26598 |   17181    56614 |    5154    7362  1816140   246.7 | 32.863 % |
c   -- subsuming                       
c   -- var.elim.:  1000/10502          
c   -- var.elim.:  2000/10502          
c   -- var.elim.:  3000/10502          
c   -- var.elim.:  4000/10502          
c   -- var.elim.:  5000/10502          
c   -- var.elim.:  6000/10502          
c   -- var.elim.:  7000/10502          
c   -- var.elim.:  8000/10502          
c   -- var.elim.:  9000/10502          
c   -- var.elim.:  10000/10502          
c   -- var.elim.:  10502/10502          
c   -- var.elim.:  1000/4735          
c   -- var.elim.:  2000/4735          
c   -- var.elim.:  3000/4735          
c   -- var.elim.:  4000/4735          
c   -- var.elim.:  4735/4735          
c   -- var.elim.:  1000/2654          
c   -- var.elim.:  2000/2654          
c   -- var.elim.:  2654/2654          
c   -- var.elim.:  1000/1571          
c   -- var.elim.:  1571/1571          
c   -- var.elim.:  1000/1175          
c   -- var.elim.:  1175/1175          
c   -- var.elim.:  732/732          
c   -- var.elim.:  267/267          
c   -- subsuming                       
c   -- var.elim.:  415/415          
c   -- var.elim.:  20/20          
c |     26598 |    5144    28504 |      --    7362       --      -- |     --   | -11937/-27909
c |     26598 |    5144    28504 |    2057    2779   127188    45.8 | 32.863 % |
c |     26698 |    5144    28504 |    2263    2879   151638    52.7 | 44.670 % |
c |     26849 |    5144    28504 |    2489    3030   187120    61.8 | 44.670 % |
c |     27074 |    5124    28350 |    2728    3253   261166    80.3 | 44.878 % |
c |     27412 |    5124    28350 |    3000    3591   398676   111.0 | 44.878 % |
c |     27922 |    5124    28350 |    3300    4101   592230   144.4 | 44.878 % |
c |     28681 |    5124    28350 |    3630    4860   869929   179.0 | 44.878 % |
c |     29821 |    5124    28350 |    3994    6000  1268221   211.4 | 44.878 % |
c |     31529 |    5044    27791 |    4324    5705  1674304   293.5 | 45.814 % |
c |     34092 |    5044    27791 |    4757    5892  1698124   288.2 | 45.814 % |
c |     37942 |    4968    27202 |    5154    5082  1384797   272.5 | 46.620 % |
c |     43708 |    4918    26851 |    5612    5856  1266711   216.3 | 47.166 % |
c |     52358 |    4890    26650 |    6138    6860  1457222   212.4 | 47.478 % |
c |     65334 |    4767    25790 |    6582    5866   939337   160.1 | 48.908 % |
c |     84797 |    4553    24307 |    6916    7223  1536216   212.7 | 51.378 % |
c |    113993 |    4475    23672 |    7477    8324  1687658   202.7 | 52.366 % |
c |    157782 |    4475    23672 |    8225    8998  1557622   173.1 | 52.366 % |
c |    223466 |    4475    23672 |    9047   10275  2454217   238.9 | 52.366 % |
c |    321995 |    4475    23672 |    9952    9913  1917520   193.4 | 52.366 % |
c ==============================================================================
c [1mOptimal solution: 191[0m
s OPTIMUM FOUND
v x1 -x2 -x3 -x4 -x5 -x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 -x15 x16 x17 -x18 -x19 -x20 x21 -x22 x23 -x24 -x25 -x26 x27 -x28 x29 -x30 x31 -x32 -x33 -x34 x35 -x36 -x37 -x38 x39 -x40 -x41 -x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 -x51 -x52 -x53 -x54 x55 -x56 x57 -x58 x59 -x60 -x61 -x62 x63 -x64 x65 -x66 -x67 -x68 -x69 -x70 x71 -x72 x73 -x74 x75 -x76 x77 -x78 -x79 -x80 x81 -x82 -x83 -x84 -x85 -x86 x87 -x88 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 -x103 -x104 x105 -x106 x107 -x108 -x109 -x110 x111 -x112 x113 -x114 x115 -x116 -x117 -x118 x119 -x120 -x121 x122 x123 -x124 -x125 -x126 x127 -x128 x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 x151 -x152 x153 -x154 x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 x183 -x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 x193 -x194 x195 -x196 x197 -x198 x199 -x200 -x201 x202 x203 -x204 x205 -x206 x207 -x208 x209 -x210 x211 -x212 x213 -x214 x215 -x216 x217 -x218 -x219 x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 -x229 x230 x231 -x232 x233 -x234 x235 -x236 x237 -x238 x239 -x240 x241 -x242 x243 -x244 x245 -x246 x247 -x248 x249 -x250 x251 -x252 x253 -x254 x255 -x256 -x257 -x258 x259 -x260 -x261 -x262 x263 -x264 x265 -x266 x267 -x268 x269 -x270 x271 -x272 x273 -x274 -x275 -x276 x277 -x278 x279 -x280 x281 -x282 -x283 -x284 x285 -x286 x287 -x288 x289 -x290 x291 -x292 x293 -x294 -x295 -x296 x297 -x298 x299 -x300 x301 -x302 -x303 x304 -x305 -x306 x307 -x308 x309 -x310 -x311 -x312 -x313 x314 x315 -x316 x317 -x318 -x319 -x320 -x321 -x322 x323 -x324 -x325 -x326 x327 -x328 x329 -x330 -x331 -x332 x333 -x334 x335 -x336 x337 -x338 -x339 -x340 x341 -x342 x343 -x344 x345 -x346 -x347 -x348 -x349 -x350 x351 -x352 x353 -x354 x355 -x356 -x357 -x358 x359 -x360 x361 -x362 x363 -x364 x365 -x366 -x367 -x368 x369 -x370 -x371 x372 x373 -x374 -x375 -x376 x377 -x378 x379 -x380 -x381 -x382 x383 -x384 x385 -x386 -x387 x388 -x389 x390 -x391 x392 x393 -x394 -x395 x396 -x397 x398 x399 -x400 -x401 x402 -x403 x404 x405 -x406 -x407 x408 -x409 x410 x411 -x412 -x413 x414 -x415 x416 -x417 x418 x419 -x420 -x421 x422 x423 -x424 -x425 x426 -x427 x428 x429 -x430 -x431 x432 -x433 x434 x435 -x436 -x437 x438 x439 -x440 -x441 x442 -x443 x444 -x445 x446 -x447 x448 x449 -x450 -x451 x452 x453 -x454 -x455 x456
c _______________________________________________________________________________
c 
c restarts              : 46
c conflicts             : 404498         (398 /sec)
c decisions             : 959388         (944 /sec)
c propagations          : 108189624      (106442 /sec)
c inspects              : 1010462128     (994138 /sec)
c CPU time              : 1016.42 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.90 2/54 4019
Raw data (stat): 4019 (runsolver) R 4018 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421926111 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 3067 0 0 0 985 12 0 0 25 0 1 0 421926111 14045184 2847 4294967295 134512640 134672761 3221224576 3221223024 134643963 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3429 2847 603 41 0 3388 0
vsize: 13716
[startup+20.0008 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 4835 0 0 0 1969 29 0 0 25 0 1 0 421926111 20463616 4142 4294967295 134512640 134672761 3221224576 3221223024 134643468 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4996 4142 603 41 0 4955 0
vsize: 19984
[startup+30.0005 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 7113 0 0 0 2954 43 0 0 25 0 1 0 421926111 19554304 4016 4294967295 134512640 134672761 3221224576 3221223232 134553654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4774 4016 603 41 0 4733 0
vsize: 19096
[startup+40.0007 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 11602 0 0 0 3933 64 0 0 25 0 1 0 421926111 24227840 5242 4294967295 134512640 134672761 3221224576 3221223024 134643624 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5915 5242 603 41 0 5874 0
vsize: 23660
[startup+50.0008 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 11643 0 0 0 4931 64 0 0 25 0 1 0 421926111 24268800 5260 4294967295 134512640 134672761 3221224576 3221223720 134616350 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5925 5260 603 41 0 5884 0
vsize: 23700
[startup+60.0005 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 12273 0 0 0 5930 66 0 0 25 0 1 0 421926111 26882048 5890 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6563 5890 603 41 0 6522 0
vsize: 26252
[startup+70.0015 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 12747 0 0 0 6929 67 0 0 25 0 1 0 421926111 28889088 6364 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7053 6364 603 41 0 7012 0
vsize: 28212
[startup+80.0018 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 12748 0 0 0 7929 67 0 0 25 0 1 0 421926111 28889088 6365 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7053 6365 603 41 0 7012 0
vsize: 28212
[startup+90.0015 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 12789 0 0 0 8929 68 0 0 25 0 1 0 421926111 29016064 6406 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7084 6406 603 41 0 7043 0
vsize: 28336
[startup+100.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 14086 0 0 0 9925 71 0 0 25 0 1 0 421926111 35295232 7639 4294967295 134512640 134672761 3221224576 3221223052 134516356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8617 7639 603 41 0 8576 0
vsize: 34468
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 16525 0 0 0 10912 84 0 0 25 0 1 0 421926111 29052928 6545 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7093 6545 603 41 0 7052 0
vsize: 28372
[startup+120 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 16820 0 0 0 11911 85 0 0 25 0 1 0 421926111 30363648 6840 4294967295 134512640 134672761 3221224576 3221223388 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7413 6840 603 41 0 7372 0
vsize: 29652
[startup+130 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 12911 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223616 134613740 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+140 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 13911 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+149.999 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 14911 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+159.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 15911 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223760 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+170 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 16912 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223568 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+179.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 17912 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+189.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 18912 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+200 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 19912 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223616 134614256 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+209.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 20912 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+219.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 21912 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223760 134615796 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+229.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 22912 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+239.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 23913 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223760 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+249.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17028 0 0 0 24913 86 0 0 25 0 1 0 421926111 31133696 7048 4294967295 134512640 134672761 3221224576 3221223760 134616001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7601 7048 603 41 0 7560 0
vsize: 30404
[startup+259.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17051 0 0 0 25913 86 0 0 25 0 1 0 421926111 31264768 7071 4294967295 134512640 134672761 3221224576 3221223760 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7633 7071 603 41 0 7592 0
vsize: 30532
[startup+269.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17242 0 0 0 26913 86 0 0 25 0 1 0 421926111 32055296 7262 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7826 7262 603 41 0 7785 0
vsize: 31304
[startup+279.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17385 0 0 0 27913 86 0 0 25 0 1 0 421926111 32661504 7405 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7974 7405 603 41 0 7933 0
vsize: 31896
[startup+289.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17503 0 0 0 28912 87 0 0 25 0 1 0 421926111 33148928 7523 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8093 7523 603 41 0 8052 0
vsize: 32372
[startup+299.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17503 0 0 0 29912 87 0 0 25 0 1 0 421926111 33144832 7523 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8092 7523 603 41 0 8051 0
vsize: 32368
[startup+309.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17503 0 0 0 30913 87 0 0 25 0 1 0 421926111 33120256 7523 4294967295 134512640 134672761 3221224576 3221223776 134610697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8086 7523 603 41 0 8045 0
vsize: 32344
[startup+319.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17503 0 0 0 31913 87 0 0 25 0 1 0 421926111 33116160 7523 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8085 7523 603 41 0 8044 0
vsize: 32340
[startup+329.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17522 0 0 0 32913 87 0 0 25 0 1 0 421926111 33222656 7542 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8111 7542 603 41 0 8070 0
vsize: 32444
[startup+339.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 33913 87 0 0 25 0 1 0 421926111 33579008 7629 4294967295 134512640 134672761 3221224576 3221223616 134614271 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8198 7629 603 41 0 8157 0
vsize: 32792
[startup+349.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 34913 87 0 0 25 0 1 0 421926111 33579008 7629 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8198 7629 603 41 0 8157 0
vsize: 32792
[startup+359.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 35913 87 0 0 25 0 1 0 421926111 33554432 7629 4294967295 134512640 134672761 3221224576 3221223616 134612827 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8192 7629 603 41 0 8151 0
vsize: 32768
[startup+369.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 36913 87 0 0 25 0 1 0 421926111 33497088 7627 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8178 7627 603 41 0 8137 0
vsize: 32712
[startup+379.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 37914 87 0 0 25 0 1 0 421926111 33497088 7627 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8178 7627 603 41 0 8137 0
vsize: 32712
[startup+389.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 38914 87 0 0 25 0 1 0 421926111 33497088 7627 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8178 7627 603 41 0 8137 0
vsize: 32712
[startup+399.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 39914 87 0 0 25 0 1 0 421926111 33497088 7627 4294967295 134512640 134672761 3221224576 3221223760 134615994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8178 7627 603 41 0 8137 0
vsize: 32712
[startup+409.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 40914 87 0 0 25 0 1 0 421926111 33497088 7627 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8178 7627 603 41 0 8137 0
vsize: 32712
[startup+419.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 41914 87 0 0 25 0 1 0 421926111 33497088 7627 4294967295 134512640 134672761 3221224576 3221223760 134615785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8178 7627 603 41 0 8137 0
vsize: 32712
[startup+429.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 42914 87 0 0 25 0 1 0 421926111 33497088 7627 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8178 7627 603 41 0 8137 0
vsize: 32712
[startup+439.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 43915 87 0 0 25 0 1 0 421926111 33271808 7574 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8123 7574 603 41 0 8082 0
vsize: 32492
[startup+449.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 44915 87 0 0 25 0 1 0 421926111 33271808 7574 4294967295 134512640 134672761 3221224576 3221223760 134615643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8123 7574 603 41 0 8082 0
vsize: 32492
[startup+459.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 45915 87 0 0 25 0 1 0 421926111 33271808 7574 4294967295 134512640 134672761 3221224576 3221223760 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8123 7574 603 41 0 8082 0
vsize: 32492
[startup+469.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 46915 87 0 0 25 0 1 0 421926111 33271808 7574 4294967295 134512640 134672761 3221224576 3221223840 134617932 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8123 7574 603 41 0 8082 0
vsize: 32492
[startup+479.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17609 0 0 0 47915 87 0 0 25 0 1 0 421926111 33271808 7574 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8123 7574 603 41 0 8082 0
vsize: 32492
[startup+489.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17658 0 0 0 48915 87 0 0 25 0 1 0 421926111 33533952 7623 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8187 7623 603 41 0 8146 0
vsize: 32748
[startup+499.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17658 0 0 0 49916 87 0 0 25 0 1 0 421926111 33533952 7623 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8187 7623 603 41 0 8146 0
vsize: 32748
[startup+509.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17659 0 0 0 50916 87 0 0 25 0 1 0 421926111 33533952 7624 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8187 7624 603 41 0 8146 0
vsize: 32748
[startup+519.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17659 0 0 0 51916 87 0 0 25 0 1 0 421926111 33533952 7624 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8187 7624 603 41 0 8146 0
vsize: 32748
[startup+529.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17693 0 0 0 52916 87 0 0 25 0 1 0 421926111 33665024 7658 4294967295 134512640 134672761 3221224576 3221223616 134612783 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8219 7658 603 41 0 8178 0
vsize: 32876
[startup+539.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17716 0 0 0 53916 87 0 0 25 0 1 0 421926111 33796096 7681 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8251 7681 603 41 0 8210 0
vsize: 33004
[startup+549.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17805 0 0 0 54916 88 0 0 25 0 1 0 421926111 34156544 7770 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8339 7770 603 41 0 8298 0
vsize: 33356
[startup+559.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17805 0 0 0 55916 88 0 0 25 0 1 0 421926111 34136064 7770 4294967295 134512640 134672761 3221224576 3221223760 134615538 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8334 7770 603 41 0 8293 0
vsize: 33336
[startup+569.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17805 0 0 0 56917 88 0 0 25 0 1 0 421926111 34136064 7770 4294967295 134512640 134672761 3221224576 3221223616 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8334 7770 603 41 0 8293 0
vsize: 33336
[startup+579.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 57916 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+589.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 58916 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+599.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 59916 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615698 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+609.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 60917 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+619.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 61917 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+629.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 62917 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+639.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 63917 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+649.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 64918 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+659.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 65918 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+669.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 66918 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+679.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 67918 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+689.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 68918 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+699.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 69918 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+709.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 70919 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+719.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 71919 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+729.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 72919 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+739.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 73919 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223232 134645493 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+749.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 74919 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615523 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+759.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 75920 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+769.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 76920 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223616 134614209 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+779.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 77920 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+789.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 78920 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+800 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 79920 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223672 134616299 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+809.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 80920 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+819.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 81921 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+829.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 82921 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+839.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 83921 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+849.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 84921 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+859.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 85921 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+869.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 86921 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615689 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+879.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 87922 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+889.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 88922 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223616 134612892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+899.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 17937 0 0 0 89922 88 0 0 25 0 1 0 421926111 34652160 7902 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8460 7902 603 41 0 8419 0
vsize: 33840
[startup+909.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18004 0 0 0 90922 88 0 0 25 0 1 0 421926111 34914304 7969 4294967295 134512640 134672761 3221224576 3221223568 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8524 7969 603 41 0 8483 0
vsize: 34096
[startup+919.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18004 0 0 0 91922 88 0 0 25 0 1 0 421926111 34914304 7969 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8524 7969 603 41 0 8483 0
vsize: 34096
[startup+929.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18004 0 0 0 92922 88 0 0 25 0 1 0 421926111 34914304 7969 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8524 7969 603 41 0 8483 0
vsize: 34096
[startup+939.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18048 0 0 0 93922 89 0 0 25 0 1 0 421926111 35147776 8013 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8581 8013 603 41 0 8540 0
vsize: 34324
[startup+949.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18276 0 0 0 94922 89 0 0 25 0 1 0 421926111 36065280 8241 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8805 8241 603 41 0 8764 0
vsize: 35220
[startup+959.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18276 0 0 0 95922 89 0 0 25 0 1 0 421926111 36065280 8241 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8805 8241 603 41 0 8764 0
vsize: 35220
[startup+969.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18276 0 0 0 96922 89 0 0 25 0 1 0 421926111 36065280 8241 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8805 8241 603 41 0 8764 0
vsize: 35220
[startup+979.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18285 0 0 0 97922 89 0 0 25 0 1 0 421926111 36065280 8250 4294967295 134512640 134672761 3221224576 3221223760 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8805 8250 603 41 0 8764 0
vsize: 35220
[startup+989.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18359 0 0 0 98923 89 0 0 25 0 1 0 421926111 36425728 8324 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8893 8324 603 41 0 8852 0
vsize: 35572
[startup+999.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18359 0 0 0 99923 89 0 0 25 0 1 0 421926111 36425728 8324 4294967295 134512640 134672761 3221224576 3221223616 134603512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8893 8324 603 41 0 8852 0
vsize: 35572
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18359 0 0 0 100923 89 0 0 25 0 1 0 421926111 36413440 8324 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8890 8324 603 41 0 8849 0
vsize: 35560
[startup+1017.22 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 4019
Raw data (stat): 4019 (minisat+) R 4018 30701 30700 0 -1 0 18359 0 0 0 100923 89 0 0 25 0 1 0 421926111 36413440 8324 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8890 8324 603 41 0 8849 0
vsize: 0

Child status: 30
Real time (s): 1017.22
CPU time (s): 1017.35
CPU user time (s): 1016.43
CPU system time (s): 0.925859
CPU usage (%): 100.013
Max. virtual memory (Kb): 35572
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
Verifier:	OK	191
#### END VERIFIER DATA ####