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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
    Note that some very long lines in this section may be truncated by your web browser !
  3. 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.
  4. 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

Nameweb/www.ps.uni-sb.de/~walser/benchmarks/radar/normalized-10:10:4.5:0.95:98.opb
MD5SUMac510382bae6003fe0373ad32fd0064f
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 7
Optimality of the best value was proved NO
Number of terms in the objective function 411
Biggest coefficient in the objective function 268
Number of bits for the biggest coefficient in the objective function 9
Sum of the numbers in the objective function 1129
Number of bits of the sum of numbers in the objective function 11
Biggest number in a constraint 268
Number of bits of the biggest number in a constraint 9
Biggest sum of numbers in a constraint 1129
Number of bits of the biggest sum of numbers11
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1205.78
Number of variables411
Total number of constraints887
Number of constraints which are clauses387
Number of constraints which are cardinality constraints (but not clauses)500
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint1
Maximum length of a constraint16

Trace number 2356

Launcher Data

LAUNCH ON wulflinc30 THE 2005-09-18 19:10:05 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2737 boxname=wulflinc30 idbench=393 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ac510382bae6003fe0373ad32fd0064f  /oldhome/oroussel/tmp/wulflinc30/normalized-10:10:4.5:0.95:98.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc30/normalized-10:10:4.5:0.95:98.opb
IDLAUNCH: 2737
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
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.072
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:        907692 kB
Buffers:         37528 kB
Cached:          59332 kB
SwapCached:        788 kB
Active:          65712 kB
Inactive:        33804 kB
HighTotal:      131008 kB
HighFree:        70896 kB
LowTotal:       903652 kB
LowFree:        836796 kB
SwapTotal:     2097892 kB
SwapFree:      2096636 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5732 kB
Slab:            21856 kB
Committed_AS:    64136 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 19:30:15 (client local time) WITH STATUS 10 IN 1208.2 SECONDS
stats: 2737 7 1208.2 10

Solver Data

c Parsing PB file...
c Converting 476 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  95]---> BDD-cost:    8
c ---[  94]---> BDD-cost:    8
c ---[  93]---> BDD-cost:   14
c ---[  92]---> BDD-cost:    8
c ---[  91]---> BDD-cost:   11
c ---[  90]---> BDD-cost:   17
c ---[  89]---> BDD-cost:   14
c ---[  88]---> BDD-cost:   11
c ---[  87]---> BDD-cost:   11
c ---[  86]---> BDD-cost:    5
c ---[  85]---> BDD-cost:   11
c ---[  84]---> BDD-cost:   14
c ---[  83]---> BDD-cost:   17
c ---[  82]---> BDD-cost:   17
c ---[  81]---> BDD-cost:   21
c ---[  80]---> BDD-cost:   23
c ---[  79]---> BDD-cost:   17
c ---[  78]---> BDD-cost:   11
c ---[  77]---> BDD-cost:    8
c ---[  76]---> BDD-cost:   14
c ---[  75]---> BDD-cost:   17
c ---[  74]---> BDD-cost:   23
c ---[  73]---> BDD-cost:   26
c ---[  72]---> BDD-cost:   26
c ---[  71]---> BDD-cost:   32
c ---[  70]---> BDD-cost:   23
c ---[  69]---> BDD-cost:   14
c ---[  68]---> BDD-cost:   20
c ---[  67]---> BDD-cost:   11
c ---[  66]---> BDD-cost:   17
c ---[  65]---> BDD-cost:   23
c ---[  64]---> BDD-cost:   26
c ---[  63]---> BDD-cost:   29
c ---[  62]---> BDD-cost:   29
c ---[  61]---> BDD-cost:   32
c ---[  60]---> BDD-cost:   35
c ---[  59]---> BDD-cost:   23
c ---[  58]---> BDD-cost:   23
c ---[  57]---> BDD-cost:   17
c ---[  56]---> BDD-cost:   14
c ---[  55]---> BDD-cost:   26
c ---[  54]---> BDD-cost:   26
c ---[  53]---> BDD-cost:   29
c ---[  52]---> BDD-cost:   32
c ---[  51]---> BDD-cost:   41
c ---[  50]---> BDD-cost:   38
c ---[  49]---> BDD-cost:   26
c ---[  48]---> BDD-cost:   24
c ---[  47]---> BDD-cost:   20
c ---[  46]---> BDD-cost:   14
c ---[  45]---> BDD-cost:   23
c ---[  44]---> BDD-cost:   15
c ---[  43]---> BDD-cost:   29
c ---[  42]---> BDD-cost:   32
c ---[  41]---> BDD-cost:   38
c ---[  40]---> BDD-cost:   32
c ---[  39]---> BDD-cost:   29
c ---[  38]---> BDD-cost:   29
c ---[  37]---> BDD-cost:   23
c ---[  36]---> BDD-cost:    7
c ---[  35]---> BDD-cost:   20
c ---[  34]---> BDD-cost:   15
c ---[  33]---> BDD-cost:   23
c ---[  32]---> BDD-cost:   23
c ---[  31]---> BDD-cost:   32
c ---[  30]---> BDD-cost:   29
c ---[  29]---> BDD-cost:   23
c ---[  28]---> BDD-cost:   23
c ---[  24]---> BDD-cost:   13
c ---[  23]---> BDD-cost:   23
c ---[  22]---> BDD-cost:   29
c ---[  21]---> BDD-cost:   23
c ---[  20]---> BDD-cost:   23
c ---[  19]---> BDD-cost:   17
c ---[  18]---> BDD-cost:   17
c ---[  15]---> BDD-cost:   11
c ---[  14]---> BDD-cost:   20
c ---[  13]---> BDD-cost:   23
c ---[  12]---> BDD-cost:   20
c ---[  11]---> BDD-cost:   20
c ---[  10]---> BDD-cost:   11
c ---[   9]---> BDD-cost:   11
c ---[   6]---> BDD-cost:    7
c ---[   5]---> BDD-cost:   11
c ---[   4]---> BDD-cost:   17
c ---[   3]---> BDD-cost:   11
c ---[   2]---> BDD-cost:   14
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:   11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    4472    12709 |    1490       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 398
c ---[   0]---> Sorter-cost:23127     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   32494    78480 |   10831       0        0     nan |  0.000 % |
c |       102 |   32227    77921 |   11914      93     1757    18.9 |  1.135 % |
c ==============================================================================
c Found solution: 43
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       161 |   44201   105933 |   14733     151     2760    18.3 |  1.135 % |
c |       261 |   44201   105933 |   16206     251     7069    28.2 |  1.191 % |
c |       411 |   44129   105785 |   17826     368     8799    23.9 |  1.364 % |
c |       636 |   43979   105462 |   19609     564    10452    18.5 |  1.761 % |
c ==============================================================================
c Found solution: 37
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       858 |   44008   105544 |   14669     786    14574    18.5 |  1.761 % |
c |       958 |   44008   105544 |   16135     886    15808    17.8 |  1.764 % |
c |      1108 |   44008   105544 |   17749    1036    18772    18.1 |  1.764 % |
c |      1335 |   44008   105544 |   19524    1263    42756    33.9 |  1.764 % |
c |      1673 |   43872   105242 |   21476    1589    47389    29.8 |  2.038 % |
c ==============================================================================
c Found solution: 32
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2115 |   43823   105162 |   14607    2030    58752    28.9 |  2.038 % |
c |      2215 |   43719   104928 |   16067    2128    61709    29.0 |  2.444 % |
c |      2367 |   43671   104819 |   17674    2277    64221    28.2 |  2.503 % |
c |      2592 |   43369   104134 |   19441    2494    73322    29.4 |  3.036 % |
c ==============================================================================
c Found solution: 29
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2850 |   43376   104156 |   14458    2752    80617    29.3 |  3.036 % |
c |      2950 |   43376   104156 |   15903    2852    81890    28.7 |  3.040 % |
c |      3100 |   43376   104156 |   17494    3002    83094    27.7 |  3.040 % |
c |      3326 |   43376   104156 |   19243    3228    90300    28.0 |  3.040 % |
c |      3663 |   43209   103775 |   21167    3563   100193    28.1 |  3.345 % |
c |      4172 |   43209   103775 |   23284    4072   113402    27.8 |  3.345 % |
c ==============================================================================
c Found solution: 20
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4914 |   43272   103952 |   14424    4811   136307    28.3 |  3.345 % |
c |      5014 |   43177   103737 |   15866    4900   137820    28.1 |  3.483 % |
c |      5165 |   43177   103737 |   17453    5051   138864    27.5 |  3.483 % |
c |      5390 |   43177   103737 |   19198    5276   140350    26.6 |  3.483 % |
c |      5729 |   43177   103737 |   21118    5615   145264    25.9 |  3.483 % |
c |      6236 |   43165   103710 |   23229    6121   154621    25.3 |  3.497 % |
c |      6995 |   43072   103495 |   25552    6876   178998    26.0 |  3.710 % |
c |      8134 |   42972   103274 |   28108    8011   265475    33.1 |  3.914 % |
c |      9842 |   42943   103209 |   30919    9717   307744    31.7 |  3.996 % |
c |     12405 |   42943   103209 |   34011   12280   461530    37.6 |  3.996 % |
c |     16249 |   42943   103209 |   37412   16124   703042    43.6 |  3.996 % |
c |     22015 |   42912   103140 |   41153   21884  1438161    65.7 |  4.082 % |
c |     30666 |   42912   103140 |   45268   30535  2435749    79.8 |  4.082 % |
c |     43640 |   42912   103140 |   49795   43509  4226758    97.1 |  4.082 % |
c |     63102 |   42912   103140 |   54775   17575  3032611   172.6 |  4.082 % |
c ==============================================================================
c Found solution: 19
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     90954 |   42912   103147 |   14304   45424  8232293   181.2 |  4.082 % |
c |     91054 |   42912   103147 |   15734   14509  2806830   193.5 |  4.091 % |
c |     91204 |   42912   103147 |   17307   14659  2808371   191.6 |  4.091 % |
c |     91429 |   42912   103147 |   19038   14884  2812415   189.0 |  4.091 % |
c |     91770 |   42912   103147 |   20942   15225  2829835   185.9 |  4.091 % |
c |     92281 |   42894   103105 |   23036   15733  2837111   180.3 |  4.118 % |
c |     93040 |   42894   103105 |   25340   16492  2881603   174.7 |  4.118 % |
c |     94182 |   42894   103105 |   27874   17634  2927916   166.0 |  4.118 % |
c |     95892 |   42894   103105 |   30661   19344  3204381   165.7 |  4.118 % |
c |     98455 |   42894   103105 |   33728   21907  3314140   151.3 |  4.118 % |
c |    102302 |   42878   103068 |   37100   25751  3516726   136.6 |  4.141 % |
c ==============================================================================
c Found solution: 18
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    105316 |   42860   103033 |   14286   28730  3799486   132.2 |  4.141 % |
c |    105419 |   42860   103033 |   15714   13143   878856    66.9 |  4.208 % |
c |    105569 |   42725   102721 |   17286   13287   879762    66.2 |  4.472 % |
c |    105794 |   42725   102721 |   19014   13512   882017    65.3 |  4.472 % |
c |    106131 |   42725   102721 |   20916   13849   890028    64.3 |  4.472 % |
c |    106637 |   42725   102721 |   23007   14355   901438    62.8 |  4.472 % |
c |    107397 |   42725   102721 |   25308   15115   934652    61.8 |  4.472 % |
c |    108537 |   42725   102721 |   27839   16255   992155    61.0 |  4.472 % |
c |    110245 |   42725   102721 |   30623   17963  1066105    59.4 |  4.472 % |
c |    112807 |   42725   102721 |   33685   20525  1332557    64.9 |  4.472 % |
c ==============================================================================
c Found solution: 14
c ---[   0]---> Sorter-cost:    1     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    114488 |   42751   102796 |   14250   22206  1371666    61.8 |  4.472 % |
c |    114588 |   42751   102796 |   15675   11203   491922    43.9 |  4.473 % |
c |    114738 |   42751   102796 |   17242   11353   494101    43.5 |  4.473 % |
c |    114963 |   42751   102796 |   18966   11578   503314    43.5 |  4.473 % |
c |    115302 |   42751   102796 |   20863   11917   516562    43.3 |  4.473 % |
c |    115808 |   42751   102796 |   22949   12423   563916    45.4 |  4.473 % |
c |    116567 |   42655   102580 |   25244   13181   579913    44.0 |  4.672 % |
c |    117706 |   42655   102580 |   27769   14320   642355    44.9 |  4.672 % |
c |    119414 |   42655   102580 |   30546   16028   754371    47.1 |  4.672 % |
c |    121977 |   42655   102580 |   33600   18591  1012810    54.5 |  4.672 % |
c ==============================================================================
c Found solution: 11
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    125422 |   42654   102599 |   14218   22024  1133680    51.5 |  4.672 % |
c |    125522 |   42654   102599 |   15639   11112   496118    44.6 |  4.750 % |
c |    125673 |   42654   102599 |   17203   11263   499510    44.3 |  4.750 % |
c |    125899 |   42654   102599 |   18924   11489   514157    44.8 |  4.750 % |
c |    126240 |   42650   102591 |   20816   11827   525001    44.4 |  4.754 % |
c |    126748 |   42650   102591 |   22898   12335   554839    45.0 |  4.754 % |
c |    127508 |   42650   102591 |   25188   13095   613587    46.9 |  4.754 % |
c |    128647 |   42650   102591 |   27706   14234   686549    48.2 |  4.754 % |
c |    130355 |   42650   102591 |   30477   15942   847139    53.1 |  4.754 % |
c |    132917 |   42650   102591 |   33525   18504   975950    52.7 |  4.754 % |
c |    136761 |   42650   102591 |   36877   22348  1557897    69.7 |  4.754 % |
c |    142528 |   42650   102591 |   40565   28115  2081293    74.0 |  4.754 % |
c |    151177 |   42650   102591 |   44622   36764  3716668   101.1 |  4.754 % |
c |    164151 |   42650   102591 |   49084   17638  1034620    58.7 |  4.754 % |
c |    183612 |   42650   102591 |   53992   37099  4369752   117.8 |  4.754 % |
c |    212804 |   42650   102591 |   59392   19896  2166225   108.9 |  4.754 % |
c |    256593 |   42650   102591 |   65331   63685 14315644   224.8 |  4.754 % |
c ==============================================================================
c Found solution: 9
c ---[   0]---> Sorter-cost:    2     Base: 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    315536 |   42653   102605 |   14217   64339  9301830   144.6 |  4.754 % |
c |    315637 |   42653   102605 |   15638    8667   872064   100.6 |  4.762 % |
c |    315787 |   42653   102605 |   17202    8817   879176    99.7 |  4.762 % |
c |    316013 |   42653   102605 |   18922    9043   885390    97.9 |  4.762 % |
c |    316351 |   42653   102605 |   20815    9381   902282    96.2 |  4.762 % |
c |    316857 |   42653   102605 |   22896    9887   943964    95.5 |  4.762 % |
c |    317616 |   42641   102579 |   25186   10641   966354    90.8 |  4.794 % |
c |    318755 |   42641   102579 |   27704   11780  1004746    85.3 |  4.794 % |
c |    320465 |   42641   102579 |   30475   13490  1235075    91.6 |  4.794 % |
c |    323030 |   42641   102579 |   33522   16055  1348999    84.0 |  4.794 % |
c |    326875 |   42641   102579 |   36875   19900  1552401    78.0 |  4.794 % |

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/13914/stat): 13914 (minisat+_script) R 13913 13914 5245 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843653761 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/13914/statm): 174 3 169 147 0 27 0
[pid=13914] vsize: 696
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libtermcap.so.2
open syscall for file tls/i686/libtermcap.so.2
open syscall for file tls/mmx/libtermcap.so.2
open syscall for file tls/libtermcap.so.2
open syscall for file i686/mmx/libtermcap.so.2
open syscall for file i686/libtermcap.so.2
open syscall for file mmx/libtermcap.so.2
open syscall for file libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2
open syscall for file /oldhome/oroussel/lib/libtermcap.so.2
open syscall for file /etc/ld.so.cache
open syscall for file /lib/libtermcap.so.2
open syscall for file tls/i686/mmx/libdl.so.2
open syscall for file tls/i686/libdl.so.2
open syscall for file tls/mmx/libdl.so.2
open syscall for file tls/libdl.so.2
open syscall for file i686/mmx/libdl.so.2
open syscall for file i686/libdl.so.2
open syscall for file mmx/libdl.so.2
open syscall for file libdl.so.2
open syscall for file /oldhome/oroussel/lib/libdl.so.2
open syscall for file /lib/libdl.so.2
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /lib/tls/libc.so.6
open syscall for file /dev/tty
open syscall for file /etc/mtab
open syscall for file /proc/meminfo
open syscall for file /oldhome/oroussel/solvers/minisat+_script
New process pid=13915
New process pid=13916
New process pid=13917
execve syscall for /bin/sed executable
One traced child (pid=13916) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=13917) exited with status: 0
One traced child (pid=13915) exited with status: 0
New process pid=13918
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc30/normalized-10:10:4.5:0.95:98.opb

[startup+10.0042 s]
Raw data (loadavg): 0.87 0.94 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) T 13914 13914 5245 0 -1 0 2226 0 0 0 976 9 0 0 25 0 1 0 1843653766 9646080 2093 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/13918/statm): 2355 2093 145 145 0 2210 0
[pid=13918] vsize: 9420
Current children cumulated CPU time (s) 9.86
Current children cumulated vsize (Kb) 11544

[startup+20.005 s]
Raw data (loadavg): 0.89 0.94 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 2571 0 0 0 1969 12 0 0 25 0 1 0 1843653766 11075584 2438 4294967295 134512640 135094434 3221224432 3221223088 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 2704 2438 145 145 0 2559 0
[pid=13918] vsize: 10816
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 12940

[startup+30.0068 s]
Raw data (loadavg): 0.90 0.94 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 2932 0 0 0 2963 14 0 0 25 0 1 0 1843653766 12595200 2799 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 3075 2799 145 145 0 2930 0
[pid=13918] vsize: 12300
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 14424

[startup+40.0076 s]
Raw data (loadavg): 0.92 0.94 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 3438 0 0 0 3953 19 0 0 25 0 1 0 1843653766 14655488 3305 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 3578 3305 145 145 0 3433 0
[pid=13918] vsize: 14312
Current children cumulated CPU time (s) 39.73
Current children cumulated vsize (Kb) 16436

[startup+50.0084 s]
Raw data (loadavg): 0.93 0.94 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 3876 0 0 0 4945 23 0 0 25 0 1 0 1843653766 16429056 3743 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 4011 3743 145 145 0 3866 0
[pid=13918] vsize: 16044
Current children cumulated CPU time (s) 49.69
Current children cumulated vsize (Kb) 18168

[startup+60.0092 s]
Raw data (loadavg): 0.94 0.95 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 4294 0 0 0 5938 25 0 0 25 0 1 0 1843653766 18128896 4161 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 4426 4161 145 145 0 4281 0
[pid=13918] vsize: 17704
Current children cumulated CPU time (s) 59.64
Current children cumulated vsize (Kb) 19828

[startup+70.01 s]
Raw data (loadavg): 0.95 0.95 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 4694 0 0 0 6932 28 0 0 25 0 1 0 1843653766 19759104 4561 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 4824 4561 145 145 0 4679 0
[pid=13918] vsize: 19296
Current children cumulated CPU time (s) 69.61
Current children cumulated vsize (Kb) 21420

[startup+80.0118 s]
Raw data (loadavg): 0.96 0.95 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 5068 0 0 0 7924 32 0 0 25 0 1 0 1843653766 21409792 4935 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 5227 4935 145 145 0 5082 0
[pid=13918] vsize: 20908
Current children cumulated CPU time (s) 79.57
Current children cumulated vsize (Kb) 23032

[startup+90.0126 s]
Raw data (loadavg): 0.96 0.95 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 5466 0 0 0 8914 36 0 0 25 0 1 0 1843653766 23044096 5333 4294967295 134512640 135094434 3221224432 3221223056 134562110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 5626 5333 145 145 0 5481 0
[pid=13918] vsize: 22504
Current children cumulated CPU time (s) 89.51
Current children cumulated vsize (Kb) 24628

[startup+100.012 s]
Raw data (loadavg): 0.97 0.95 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 5806 0 0 0 9907 39 0 0 25 0 1 0 1843653766 24424448 5673 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13918/statm): 5963 5673 145 145 0 5818 0
[pid=13918] vsize: 23852
Current children cumulated CPU time (s) 99.47
Current children cumulated vsize (Kb) 25976

[startup+110.014 s]
Raw data (loadavg): 0.97 0.95 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) T 13914 13914 5245 0 -1 0 6180 0 0 0 10900 42 0 0 25 0 1 0 1843653766 25948160 6047 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/13918/statm): 6335 6047 145 145 0 6190 0
[pid=13918] vsize: 25340
Current children cumulated CPU time (s) 109.43
Current children cumulated vsize (Kb) 27464

[startup+120.015 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 6569 0 0 0 11893 45 0 0 25 0 1 0 1843653766 27529216 6436 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 6721 6436 145 145 0 6576 0
[pid=13918] vsize: 26884
Current children cumulated CPU time (s) 119.39
Current children cumulated vsize (Kb) 29008

[startup+130.016 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 7039 0 0 0 12885 49 0 0 25 0 1 0 1843653766 29442048 6906 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 7188 6906 145 145 0 7043 0
[pid=13918] vsize: 28752
Current children cumulated CPU time (s) 129.35
Current children cumulated vsize (Kb) 30876

[startup+140.017 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 7574 0 0 0 13875 53 0 0 25 0 1 0 1843653766 31625216 7441 4294967295 134512640 135094434 3221224432 3221223120 134554705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 7721 7441 145 145 0 7576 0
[pid=13918] vsize: 30884
Current children cumulated CPU time (s) 139.29
Current children cumulated vsize (Kb) 33008

[startup+150.017 s]
Raw data (loadavg): 0.98 0.95 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 8033 0 0 0 14865 58 0 0 25 0 1 0 1843653766 33497088 7900 4294967295 134512640 135094434 3221224432 3221223024 134551997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 8178 7900 145 145 0 8033 0
[pid=13918] vsize: 32712
Current children cumulated CPU time (s) 149.24
Current children cumulated vsize (Kb) 34836

[startup+160.018 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 8487 0 0 0 15856 62 0 0 25 0 1 0 1843653766 35348480 8354 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 8630 8354 145 145 0 8485 0
[pid=13918] vsize: 34520
Current children cumulated CPU time (s) 159.19
Current children cumulated vsize (Kb) 36644

[startup+170.019 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 8937 0 0 0 16847 66 0 0 25 0 1 0 1843653766 37183488 8804 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 9078 8804 145 145 0 8933 0
[pid=13918] vsize: 36312
Current children cumulated CPU time (s) 169.14
Current children cumulated vsize (Kb) 38436

[startup+180.02 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9360 0 0 0 17838 69 0 0 25 0 1 0 1843653766 38907904 9227 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 9499 9227 145 145 0 9354 0
[pid=13918] vsize: 37996
Current children cumulated CPU time (s) 179.08
Current children cumulated vsize (Kb) 40120

[startup+190.021 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9836 0 0 0 18832 71 0 0 25 0 1 0 1843653766 40845312 9703 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 9972 9703 145 145 0 9827 0
[pid=13918] vsize: 39888
Current children cumulated CPU time (s) 189.04
Current children cumulated vsize (Kb) 42012

[startup+200.021 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9917 0 0 0 19830 72 0 0 25 0 1 0 1843653766 41177088 9784 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 10053 9784 145 145 0 9908 0
[pid=13918] vsize: 40212
Current children cumulated CPU time (s) 199.03
Current children cumulated vsize (Kb) 42336

[startup+210.022 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9917 0 0 0 20830 72 0 0 25 0 1 0 1843653766 41177088 9784 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 10053 9784 145 145 0 9908 0
[pid=13918] vsize: 40212
Current children cumulated CPU time (s) 209.03
Current children cumulated vsize (Kb) 42336

[startup+220.023 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9917 0 0 0 21831 72 0 0 25 0 1 0 1843653766 41177088 9784 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 10053 9784 145 145 0 9908 0
[pid=13918] vsize: 40212
Current children cumulated CPU time (s) 219.04
Current children cumulated vsize (Kb) 42336

[startup+230.032 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9917 0 0 0 22831 72 0 0 25 0 1 0 1843653766 41177088 9784 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 10053 9784 145 145 0 9908 0
[pid=13918] vsize: 40212
Current children cumulated CPU time (s) 229.04
Current children cumulated vsize (Kb) 42336

[startup+240.033 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9917 0 0 0 23831 72 0 0 25 0 1 0 1843653766 41177088 9784 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 10053 9784 145 145 0 9908 0
[pid=13918] vsize: 40212
Current children cumulated CPU time (s) 239.04
Current children cumulated vsize (Kb) 42336

[startup+250.032 s]
Raw data (loadavg): 0.99 0.96 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9917 0 0 0 24831 72 0 0 25 0 1 0 1843653766 41177088 9784 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13918/statm): 10053 9784 145 145 0 9908 0
[pid=13918] vsize: 40212
Current children cumulated CPU time (s) 249.04
Current children cumulated vsize (Kb) 42336

[startup+260.034 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9917 0 0 0 25830 73 0 0 25 0 1 0 1843653766 41177088 9784 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13918/statm): 10053 9784 145 145 0 9908 0
[pid=13918] vsize: 40212
Current children cumulated CPU time (s) 259.04
Current children cumulated vsize (Kb) 42336

[startup+270.035 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9917 0 0 0 26829 73 0 0 25 0 1 0 1843653766 41177088 9784 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 10053 9784 145 145 0 9908 0
[pid=13918] vsize: 40212
Current children cumulated CPU time (s) 269.03
Current children cumulated vsize (Kb) 42336

[startup+280.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9917 0 0 0 27829 73 0 0 25 0 1 0 1843653766 41177088 9784 4294967295 134512640 135094434 3221224432 3221223104 134556336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 10053 9784 145 145 0 9908 0
[pid=13918] vsize: 40212
Current children cumulated CPU time (s) 279.03
Current children cumulated vsize (Kb) 42336

[startup+290.036 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9917 0 0 0 28830 73 0 0 25 0 1 0 1843653766 41177088 9784 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 10053 9784 145 145 0 9908 0
[pid=13918] vsize: 40212
Current children cumulated CPU time (s) 289.04
Current children cumulated vsize (Kb) 42336

[startup+300.037 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 9953 0 0 0 29829 74 0 0 25 0 1 0 1843653766 41324544 9820 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 10089 9820 145 145 0 9944 0
[pid=13918] vsize: 40356
Current children cumulated CPU time (s) 299.04
Current children cumulated vsize (Kb) 42480

[startup+310.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10396 0 0 0 30819 78 0 0 25 0 1 0 1843653766 43143168 10263 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 10533 10263 145 145 0 10388 0
[pid=13918] vsize: 42132
Current children cumulated CPU time (s) 308.98
Current children cumulated vsize (Kb) 44256

[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10860 0 0 0 31812 81 0 0 25 0 1 0 1843653766 45043712 10727 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 10997 10727 145 145 0 10852 0
[pid=13918] vsize: 43988
Current children cumulated CPU time (s) 318.94
Current children cumulated vsize (Kb) 46112

[startup+330.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 32811 81 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223024 134551906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 328.93
Current children cumulated vsize (Kb) 46176

[startup+340.04 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 33811 81 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 338.93
Current children cumulated vsize (Kb) 46176

[startup+350.041 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 34812 81 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 348.94
Current children cumulated vsize (Kb) 46176

[startup+360.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 35812 81 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 358.94
Current children cumulated vsize (Kb) 46176

[startup+370.043 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 36812 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134557856 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 368.95
Current children cumulated vsize (Kb) 46176

[startup+380.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 37811 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 378.94
Current children cumulated vsize (Kb) 46176

[startup+390.044 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 38812 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 388.95
Current children cumulated vsize (Kb) 46176

[startup+400.045 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 39812 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 398.95
Current children cumulated vsize (Kb) 46176

[startup+410.046 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 40812 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 408.95
Current children cumulated vsize (Kb) 46176

[startup+420.047 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 41812 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 418.95
Current children cumulated vsize (Kb) 46176

[startup+430.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 42812 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 428.95
Current children cumulated vsize (Kb) 46176

[startup+440.048 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 43812 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223120 134554723 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 438.95
Current children cumulated vsize (Kb) 46176

[startup+450.049 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 44813 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 448.96
Current children cumulated vsize (Kb) 46176

[startup+460.05 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 45813 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 458.96
Current children cumulated vsize (Kb) 46176

[startup+470.051 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 46813 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 468.96
Current children cumulated vsize (Kb) 46176

[startup+480.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 47813 82 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 478.96
Current children cumulated vsize (Kb) 46176

[startup+490.052 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 48813 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 488.97
Current children cumulated vsize (Kb) 46176

[startup+500.053 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 49814 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 498.98
Current children cumulated vsize (Kb) 46176

[startup+510.054 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 50814 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 508.98
Current children cumulated vsize (Kb) 46176

[startup+520.055 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 51814 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223104 134556543 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 518.98
Current children cumulated vsize (Kb) 46176

[startup+530.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 52814 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 528.98
Current children cumulated vsize (Kb) 46176

[startup+540.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 53815 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 538.99
Current children cumulated vsize (Kb) 46176

[startup+550.056 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 54815 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 548.99
Current children cumulated vsize (Kb) 46176

[startup+560.057 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 55815 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223024 134556999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 558.99
Current children cumulated vsize (Kb) 46176

[startup+570.058 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 56815 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 568.99
Current children cumulated vsize (Kb) 46176

[startup+580.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 57815 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223056 134557619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 578.99
Current children cumulated vsize (Kb) 46176

[startup+590.059 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 58815 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 588.99
Current children cumulated vsize (Kb) 46176

[startup+600.06 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 59816 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223068 134557639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 599
Current children cumulated vsize (Kb) 46176

[startup+610.061 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 60816 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223024 134557219 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 609
Current children cumulated vsize (Kb) 46176

[startup+620.062 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 61816 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 619
Current children cumulated vsize (Kb) 46176

[startup+630.063 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10876 0 0 0 62817 83 0 0 25 0 1 0 1843653766 45109248 10743 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10743 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 629.01
Current children cumulated vsize (Kb) 46176

[startup+640.064 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 63816 83 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 639
Current children cumulated vsize (Kb) 46176

[startup+650.065 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 64817 83 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223056 134557665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 649.01
Current children cumulated vsize (Kb) 46176

[startup+660.066 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 65817 83 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 659.01
Current children cumulated vsize (Kb) 46176

[startup+670.067 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 66817 83 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 669.01
Current children cumulated vsize (Kb) 46176

[startup+680.068 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 67818 83 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 679.02
Current children cumulated vsize (Kb) 46176

[startup+690.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 68818 83 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223024 134557199 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 689.02
Current children cumulated vsize (Kb) 46176

[startup+700.069 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 69818 83 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223024 134556773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 699.02
Current children cumulated vsize (Kb) 46176

[startup+710.07 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 70818 83 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 709.02
Current children cumulated vsize (Kb) 46176

[startup+720.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 71818 83 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 719.02
Current children cumulated vsize (Kb) 46176

[startup+730.071 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 72818 83 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223104 134555811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 729.02
Current children cumulated vsize (Kb) 46176

[startup+740.072 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 73819 83 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223024 134557016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 739.03
Current children cumulated vsize (Kb) 46176

[startup+750.073 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 74818 85 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 749.04
Current children cumulated vsize (Kb) 46176

[startup+760.074 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 10878 0 0 0 75817 85 0 0 25 0 1 0 1843653766 45109248 10745 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11013 10745 145 145 0 10868 0
[pid=13918] vsize: 44052
Current children cumulated CPU time (s) 759.03
Current children cumulated vsize (Kb) 46176

[startup+770.075 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 11292 0 0 0 76811 89 0 0 25 0 1 0 1843653766 46804992 11159 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11427 11159 145 145 0 11282 0
[pid=13918] vsize: 45708
Current children cumulated CPU time (s) 769.01
Current children cumulated vsize (Kb) 47832

[startup+780.076 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 11768 0 0 0 77801 93 0 0 25 0 1 0 1843653766 48754688 11635 4294967295 134512640 135094434 3221224432 3221223088 134555980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 11903 11635 145 145 0 11758 0
[pid=13918] vsize: 47612
Current children cumulated CPU time (s) 778.95
Current children cumulated vsize (Kb) 49736

[startup+790.077 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 12176 0 0 0 78795 96 0 0 25 0 1 0 1843653766 50438144 12043 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 12314 12043 145 145 0 12169 0
[pid=13918] vsize: 49256
Current children cumulated CPU time (s) 788.92
Current children cumulated vsize (Kb) 51380

[startup+800.078 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 12578 0 0 0 79788 98 0 0 25 0 1 0 1843653766 52076544 12445 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 12714 12445 145 145 0 12569 0
[pid=13918] vsize: 50856
Current children cumulated CPU time (s) 798.87
Current children cumulated vsize (Kb) 52980

[startup+810.079 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 12949 0 0 0 80781 101 0 0 25 0 1 0 1843653766 53600256 12816 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 13086 12816 145 145 0 12941 0
[pid=13918] vsize: 52344
Current children cumulated CPU time (s) 808.83
Current children cumulated vsize (Kb) 54468

[startup+820.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 13319 0 0 0 81775 103 0 0 25 0 1 0 1843653766 55128064 13186 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 13459 13186 145 145 0 13314 0
[pid=13918] vsize: 53836
Current children cumulated CPU time (s) 818.79
Current children cumulated vsize (Kb) 55960

[startup+830.08 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 13772 0 0 0 82768 107 0 0 25 0 1 0 1843653766 56975360 13639 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 13910 13639 145 145 0 13765 0
[pid=13918] vsize: 55640
Current children cumulated CPU time (s) 828.76
Current children cumulated vsize (Kb) 57764

[startup+840.081 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 14163 0 0 0 83761 110 0 0 25 0 1 0 1843653766 58576896 14030 4294967295 134512640 135094434 3221224432 3221223024 134556817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 14301 14030 145 145 0 14156 0
[pid=13918] vsize: 57204
Current children cumulated CPU time (s) 838.72
Current children cumulated vsize (Kb) 59328

[startup+850.082 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 14563 0 0 0 84753 113 0 0 25 0 1 0 1843653766 60215296 14430 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 14701 14430 145 145 0 14556 0
[pid=13918] vsize: 58804
Current children cumulated CPU time (s) 848.67
Current children cumulated vsize (Kb) 60928

[startup+860.083 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 14998 0 0 0 85746 116 0 0 25 0 1 0 1843653766 61997056 14865 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 15136 14865 145 145 0 14991 0
[pid=13918] vsize: 60544
Current children cumulated CPU time (s) 858.63
Current children cumulated vsize (Kb) 62668

[startup+870.084 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 15390 0 0 0 86739 119 0 0 25 0 1 0 1843653766 63602688 15257 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 15528 15257 145 145 0 15383 0
[pid=13918] vsize: 62112
Current children cumulated CPU time (s) 868.59
Current children cumulated vsize (Kb) 64236

[startup+880.084 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 15807 0 0 0 87732 122 0 0 25 0 1 0 1843653766 65314816 15674 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 15946 15674 145 145 0 15801 0
[pid=13918] vsize: 63784
Current children cumulated CPU time (s) 878.55
Current children cumulated vsize (Kb) 65908

[startup+890.085 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 16204 0 0 0 88726 125 0 0 25 0 1 0 1843653766 66961408 16071 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 16348 16071 145 145 0 16203 0
[pid=13918] vsize: 65392
Current children cumulated CPU time (s) 888.52
Current children cumulated vsize (Kb) 67516

[startup+900.086 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 16548 0 0 0 89719 128 0 0 25 0 1 0 1843653766 68386816 16415 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 16696 16415 145 145 0 16551 0
[pid=13918] vsize: 66784
Current children cumulated CPU time (s) 898.48
Current children cumulated vsize (Kb) 68908

[startup+910.087 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 16908 0 0 0 90714 131 0 0 25 0 1 0 1843653766 69873664 16775 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 17059 16775 145 145 0 16914 0
[pid=13918] vsize: 68236
Current children cumulated CPU time (s) 908.46
Current children cumulated vsize (Kb) 70360

[startup+920.088 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 17258 0 0 0 91706 133 0 0 25 0 1 0 1843653766 71315456 17125 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 17411 17125 145 145 0 17266 0
[pid=13918] vsize: 69644
Current children cumulated CPU time (s) 918.4
Current children cumulated vsize (Kb) 71768

[startup+930.089 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 17620 0 0 0 92701 135 0 0 25 0 1 0 1843653766 72790016 17487 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 17771 17487 145 145 0 17626 0
[pid=13918] vsize: 71084
Current children cumulated CPU time (s) 928.37
Current children cumulated vsize (Kb) 73208

[startup+940.09 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 18006 0 0 0 93694 138 0 0 25 0 1 0 1843653766 74629120 17873 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 18220 17873 145 145 0 18075 0
[pid=13918] vsize: 72880
Current children cumulated CPU time (s) 938.33
Current children cumulated vsize (Kb) 75004

[startup+950.091 s]
Raw data (loadavg): 0.99 0.97 0.96 1/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) T 13914 13914 5245 0 -1 0 18438 0 0 0 94687 141 0 0 25 0 1 0 1843653766 76390400 18305 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/13918/statm): 18650 18305 145 145 0 18505 0
[pid=13918] vsize: 74600
Current children cumulated CPU time (s) 948.29
Current children cumulated vsize (Kb) 76724

[startup+960.093 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 18885 0 0 0 95679 145 0 0 25 0 1 0 1843653766 78217216 18752 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 19096 18752 145 145 0 18951 0
[pid=13918] vsize: 76384
Current children cumulated CPU time (s) 958.25
Current children cumulated vsize (Kb) 78508

[startup+970.094 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 19340 0 0 0 96672 148 0 0 25 0 1 0 1843653766 80072704 19207 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 19549 19207 145 145 0 19404 0
[pid=13918] vsize: 78196
Current children cumulated CPU time (s) 968.21
Current children cumulated vsize (Kb) 80320

[startup+980.094 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 19765 0 0 0 97663 151 0 0 25 0 1 0 1843653766 81809408 19632 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 19973 19632 145 145 0 19828 0
[pid=13918] vsize: 79892
Current children cumulated CPU time (s) 978.15
Current children cumulated vsize (Kb) 82016

[startup+990.096 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20176 0 0 0 98656 155 0 0 25 0 1 0 1843653766 83484672 20043 4294967295 134512640 135094434 3221224432 3221223024 134557401 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20382 20043 145 145 0 20237 0
[pid=13918] vsize: 81528
Current children cumulated CPU time (s) 988.12
Current children cumulated vsize (Kb) 83652

[startup+1000.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 99655 155 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 998.11
Current children cumulated vsize (Kb) 83780

[startup+1010.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 100655 155 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1008.11
Current children cumulated vsize (Kb) 83780

[startup+1020.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 101655 155 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1018.11
Current children cumulated vsize (Kb) 83780

[startup+1030.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 102655 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1028.12
Current children cumulated vsize (Kb) 83780

[startup+1040.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 103656 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223056 134557669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1038.13
Current children cumulated vsize (Kb) 83780

[startup+1050.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 104656 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1048.13
Current children cumulated vsize (Kb) 83780

[startup+1060.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 105656 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1058.13
Current children cumulated vsize (Kb) 83780

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 106656 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223024 134557210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1068.13
Current children cumulated vsize (Kb) 83780

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 107657 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1078.14
Current children cumulated vsize (Kb) 83780

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 108657 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1088.14
Current children cumulated vsize (Kb) 83780

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 109657 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1098.14
Current children cumulated vsize (Kb) 83780

[startup+1110.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 110657 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1108.14
Current children cumulated vsize (Kb) 83780

[startup+1120.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 111658 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1118.15
Current children cumulated vsize (Kb) 83780

[startup+1130.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 112658 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223024 134557389 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1128.15
Current children cumulated vsize (Kb) 83780

[startup+1140.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 113658 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1138.15
Current children cumulated vsize (Kb) 83780

[startup+1150.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 114658 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1148.15
Current children cumulated vsize (Kb) 83780

[startup+1160.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 115658 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1158.15
Current children cumulated vsize (Kb) 83780

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 116658 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1168.15
Current children cumulated vsize (Kb) 83780

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 117658 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223056 134557574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1178.15
Current children cumulated vsize (Kb) 83780

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 118658 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1188.15
Current children cumulated vsize (Kb) 83780

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 119659 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1198.16
Current children cumulated vsize (Kb) 83780

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 120659 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223024 134557133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1208.16
Current children cumulated vsize (Kb) 83780



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 0.99 0.97 0.96 2/57 13918
Raw data (/proc/13914/stat): 13914 (minisat+_script) S 13913 13914 5245 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1843653761 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/13914/statm): 531 226 485 147 0 384 0
[pid=13914] vsize: 2124
Raw data (/proc/13918/stat): 13918 (minisat+_64-bit) R 13914 13914 5245 0 -1 0 20208 0 0 0 120659 156 0 0 25 0 1 0 1843653766 83615744 20075 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13918/statm): 20414 20075 145 145 0 20269 0
[pid=13918] vsize: 81656
Current children cumulated CPU time (s) 1208.16
Current children cumulated vsize (Kb) 83780

Sending SIGTERM to -13914
Sleeping 2 seconds
One traced child (pid=13914) ended because it received signal 15 (SIGTERM)
One traced child (pid=13918) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1210.16
CPU time (s): 1208.2
CPU user time (s): 1206.6
CPU system time (s): 1.60676
CPU usage (%): 99.8384
Max. virtual memory (cumulated for all children) (Kb): 83780

Verifier Data

ERROR: no interpretation found !