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

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-lp4l.opb
MD5SUM3c39e3c2b993ee2185e2a1a3e73b9723
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 2967
Optimality of the best value was proved YES
Number of terms in the objective function 1086
Biggest coefficient in the objective function 283
Number of bits for the biggest coefficient in the objective function 9
Sum of the numbers in the objective function 197191
Number of bits of the sum of numbers in the objective function 18
Biggest number in a constraint 283
Number of bits of the biggest number in a constraint 9
Biggest sum of numbers in a constraint 197191
Number of bits of the biggest sum of numbers18
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark312.791
Number of variables1086
Total number of constraints1171
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)1170
Number of constraints which are nor clauses,nor cardinality constraints1
Minimum length of a constraint1
Maximum length of a constraint1086

Trace number 6092

Launcher Data

LAUNCH ON wulflinc10 THE 2005-09-20 03:13:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3244 boxname=wulflinc10 idbench=900 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  3c39e3c2b993ee2185e2a1a3e73b9723  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-lp4l.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-lp4l.opb
IDLAUNCH: 3244
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        787076 kB
Buffers:         38436 kB
Cached:         181996 kB
SwapCached:        228 kB
Active:          83772 kB
Inactive:       139612 kB
HighTotal:      131008 kB
HighFree:         7168 kB
LowTotal:       903652 kB
LowFree:        779908 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            18704 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 03:33:34 (client local time) WITH STATUS 10 IN 1206.4 SECONDS
stats: 3244 7 1206.4 10

Solver Data

c Parsing PB file...
c Converting 169 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 168]---> Adder-cost: 592   maxlim: 2471   bits: 12/12
c ---[ 166]---> BDD-cost:   41
c ---[ 164]---> BDD-cost:   67
c ---[ 162]---> BDD-cost:   99
c ---[ 160]---> BDD-cost:   79
c ---[ 158]---> BDD-cost:   45
c ---[ 156]---> BDD-cost:   69
c ---[ 154]---> BDD-cost:   55
c ---[ 152]---> BDD-cost:   37
c ---[ 150]---> BDD-cost:   27
c ---[ 148]---> BDD-cost:   77
c ---[ 146]---> BDD-cost:   79
c ---[ 144]---> BDD-cost:   23
c ---[ 142]---> BDD-cost:   75
c ---[ 140]---> BDD-cost:   77
c ---[ 138]---> BDD-cost:   41
c ---[ 136]---> BDD-cost:   75
c ---[ 134]---> BDD-cost:  107
c ---[ 132]---> BDD-cost:   91
c ---[ 130]---> BDD-cost:  127
c ---[ 128]---> BDD-cost:  123
c ---[ 126]---> BDD-cost:   89
c ---[ 124]---> BDD-cost:   57
c ---[ 122]---> BDD-cost:   89
c ---[ 120]---> BDD-cost:   71
c ---[ 118]---> BDD-cost:  103
c ---[ 116]---> BDD-cost:  117
c ---[ 114]---> BDD-cost:  125
c ---[ 112]---> BDD-cost:   91
c ---[ 110]---> BDD-cost:   59
c ---[ 108]---> BDD-cost:   89
c ---[ 106]---> BDD-cost:   71
c ---[ 104]---> BDD-cost:  129
c ---[ 102]---> BDD-cost:  113
c ---[ 100]---> BDD-cost:  123
c ---[  98]---> BDD-cost:   89
c ---[  96]---> BDD-cost:   61
c ---[  94]---> BDD-cost:   59
c ---[  92]---> BDD-cost:   33
c ---[  90]---> BDD-cost:  123
c ---[  88]---> BDD-cost:  121
c ---[  86]---> BDD-cost:   99
c ---[  84]---> BDD-cost:   45
c ---[  82]---> BDD-cost:   69
c ---[  80]---> BDD-cost:   59
c ---[  78]---> BDD-cost:   33
c ---[  76]---> BDD-cost:   73
c ---[  74]---> BDD-cost:   69
c ---[  72]---> BDD-cost:   47
c ---[  70]---> BDD-cost:   67
c ---[  68]---> BDD-cost:   95
c ---[  66]---> BDD-cost:   85
c ---[  64]---> BDD-cost:  107
c ---[  62]---> BDD-cost:   97
c ---[  60]---> BDD-cost:   33
c ---[  58]---> BDD-cost:   79
c ---[  56]---> BDD-cost:   87
c ---[  54]---> BDD-cost:   75
c ---[  52]---> BDD-cost:   67
c ---[  50]---> BDD-cost:   43
c ---[  48]---> BDD-cost:   75
c ---[  46]---> BDD-cost:  105
c ---[  44]---> BDD-cost:   87
c ---[  42]---> BDD-cost:   77
c ---[  40]---> BDD-cost:   63
c ---[  38]---> BDD-cost:   39
c ---[  36]---> BDD-cost:   77
c ---[  34]---> BDD-cost:   63
c ---[  32]---> BDD-cost:    5
c ---[  30]---> BDD-cost:  169
c ---[  28]---> BDD-cost:  155
c ---[  26]---> BDD-cost:  115
c ---[  24]---> BDD-cost:   77
c ---[  22]---> BDD-cost:   83
c ---[  20]---> BDD-cost:  111
c ---[  18]---> BDD-cost:  107
c ---[  16]---> BDD-cost:  161
c ---[  14]---> BDD-cost:  151
c ---[  12]---> BDD-cost:  117
c ---[  10]---> BDD-cost:   57
c ---[   8]---> BDD-cost:   85
c ---[   6]---> BDD-cost:   71
c ---[   4]---> BDD-cost:   25
c ---[   2]---> BDD-cost:   37
c ---[   0]---> Adder-cost: 2160   maxlim: 1059   bits: 11/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   35697   111365 |   11899       0        0     nan |  0.000 % |
c |       100 |   35673   111283 |   13088      98     3550    36.2 |  1.208 % |
c |       250 |   35673   111283 |   14397     248     6872    27.7 |  1.208 % |
c |       475 |   35673   111283 |   15837     473    22930    48.5 |  1.208 % |
c |       812 |   35582   110964 |   17421     797    32292    40.5 |  1.350 % |
c |      1318 |   35228   109731 |   19163    1236    39075    31.6 |  1.930 % |
c |      2077 |   35115   109352 |   21079    1978    55328    28.0 |  2.083 % |
c |      3216 |   35106   109323 |   23187    3116   134443    43.1 |  2.102 % |
c |      4924 |   35091   109270 |   25506    4817   501813   104.2 |  2.111 % |
c ==============================================================================
c Found solution: 4678
c ---[   0]---> Adder-cost: 8142   maxlim: 192513   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5808 |   91968   312356 |   30656    5701   636022   111.6 |  2.111 % |
c |      5908 |   91968   312356 |   33721    5801   638088   110.0 |  1.222 % |
c ==============================================================================
c Found solution: 4381
c ---[   0]---> Adder-cost: 0   maxlim: 192810   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6012 |   91987   312479 |   30662    5905   642881   108.9 |  1.222 % |
c |      6113 |   91987   312479 |   33728    6006   643901   107.2 |  1.248 % |
c |      6263 |   91987   312479 |   37101    6156   648018   105.3 |  1.248 % |
c |      6490 |   91987   312479 |   40811    6383   655375   102.7 |  1.248 % |
c |      6828 |   91987   312479 |   44892    6721   678577   101.0 |  1.248 % |
c |      7334 |   91987   312479 |   49381    7227   710491    98.3 |  1.248 % |
c |      8093 |   91987   312479 |   54319    7986   772776    96.8 |  1.248 % |
c ==============================================================================
c Found solution: 4329
c ---[   0]---> Adder-cost: 0   maxlim: 192862   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8535 |   92003   312609 |   30667    8428   796805    94.5 |  1.248 % |
c |      8635 |   91996   312585 |   33733    8527   798553    93.6 |  1.285 % |
c |      8786 |   91996   312585 |   37107    8678   799323    92.1 |  1.285 % |
c |      9015 |   91996   312585 |   40817    8907   810541    91.0 |  1.285 % |
c ==============================================================================
c Found solution: 4303
c ---[   0]---> Adder-cost: 0   maxlim: 192888   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9343 |   92000   312645 |   30666    9235   872957    94.5 |  1.285 % |
c |      9447 |   92000   312645 |   33732    9339   877086    93.9 |  1.306 % |
c |      9599 |   92000   312645 |   37105    9491   896729    94.5 |  1.306 % |
c |      9825 |   91979   312575 |   40816    9711   900061    92.7 |  1.322 % |
c |     10164 |   91979   312575 |   44898   10050   962481    95.8 |  1.322 % |
c |     10673 |   91967   312533 |   49387   10550  1020834    96.8 |  1.328 % |
c |     11432 |   91967   312533 |   54326   11309  1107842    98.0 |  1.328 % |
c |     12574 |   91967   312533 |   59759   12451  1288451   103.5 |  1.328 % |
c |     14282 |   91951   312481 |   65735   14156  1567998   110.8 |  1.344 % |
c |     16846 |   91944   312457 |   72308   16718  2021257   120.9 |  1.349 % |
c |     20697 |   91944   312457 |   79539   20569  2889530   140.5 |  1.349 % |
c ==============================================================================
c Found solution: 4269
c ---[   0]---> Adder-cost: 0   maxlim: 192922   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21234 |   91954   312544 |   30651   21106  2966775   140.6 |  1.349 % |
c |     21335 |   91898   312350 |   33716   21192  2969519   140.1 |  1.413 % |
c |     21485 |   91898   312350 |   37087   21342  3004545   140.8 |  1.413 % |
c |     21711 |   91785   311959 |   40796   21531  3013007   139.9 |  1.504 % |
c |     22051 |   91785   311959 |   44876   21871  3070258   140.4 |  1.504 % |
c |     22559 |   91785   311959 |   49363   22379  3176774   142.0 |  1.504 % |
c |     23320 |   91756   311856 |   54300   23120  3255681   140.8 |  1.520 % |
c |     24459 |   91756   311856 |   59730   24259  3473974   143.2 |  1.520 % |
c |     26169 |   91756   311856 |   65703   25969  3776044   145.4 |  1.520 % |
c |     28733 |   91756   311856 |   72273   28533  4179806   146.5 |  1.520 % |
c |     32579 |   91676   311577 |   79500   32345  4833206   149.4 |  1.589 % |
c |     38348 |   91676   311577 |   87450   38114  6308737   165.5 |  1.589 % |
c |     46997 |   91601   311320 |   96195   46740  8459122   181.0 |  1.643 % |
c ==============================================================================
c Found solution: 4262
c ---[   0]---> Adder-cost: 0   maxlim: 192929   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     59475 |   91556   311180 |   30518   59211 11444311   193.3 |  1.643 % |
c |     59575 |   91556   311180 |   33569   16951  2967034   175.0 |  1.685 % |
c |     59727 |   91556   311180 |   36926   17103  2987056   174.7 |  1.685 % |
c |     59955 |   91556   311180 |   40619   17331  3023499   174.5 |  1.685 % |
c |     60296 |   91556   311180 |   44681   17672  3059606   173.1 |  1.685 % |
c |     60802 |   91556   311180 |   49149   18178  3146794   173.1 |  1.685 % |
c |     61561 |   91556   311180 |   54064   18937  3286300   173.5 |  1.685 % |
c |     62700 |   91556   311180 |   59470   20076  3636099   181.1 |  1.685 % |
c |     64412 |   91556   311180 |   65418   21788  3877981   178.0 |  1.685 % |
c ==============================================================================
c Found solution: 4219
c ---[   0]---> Adder-cost: 0   maxlim: 192972   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     66546 |   91560   311241 |   30520   23922  4366619   182.5 |  1.685 % |
c |     66646 |   91560   311241 |   33572   24022  4371054   182.0 |  1.707 % |
c |     66797 |   91560   311241 |   36929   24173  4384424   181.4 |  1.707 % |
c |     67026 |   91560   311241 |   40622   24402  4398296   180.2 |  1.707 % |
c |     67363 |   91560   311241 |   44684   24739  4461698   180.4 |  1.707 % |
c |     67871 |   91560   311241 |   49152   25247  4557821   180.5 |  1.707 % |
c |     68634 |   91560   311241 |   54068   26010  4671976   179.6 |  1.707 % |
c |     69773 |   91560   311241 |   59474   27149  5037188   185.5 |  1.707 % |
c |     71481 |   91560   311241 |   65422   28857  5394646   186.9 |  1.707 % |
c |     74043 |   91535   311160 |   71964   31415  6062380   193.0 |  1.733 % |
c |     77887 |   91535   311160 |   79161   35259  6921757   196.3 |  1.733 % |
c |     83653 |   91535   311160 |   87077   41025  8057816   196.4 |  1.733 % |
c |     92304 |   91535   311160 |   95784   49676 10781790   217.0 |  1.733 % |
c ==============================================================================
c Found solution: 4172
c ---[   0]---> Adder-cost: 0   maxlim: 193019   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95559 |   91542   311224 |   30514   52931 11644687   220.0 |  1.733 % |
c |     95659 |   91542   311224 |   33565   18941  3654438   192.9 |  1.754 % |
c |     95809 |   91542   311224 |   36921   19091  3658733   191.6 |  1.754 % |
c ==============================================================================
c Found solution: 3944
c ---[   0]---> Adder-cost: 0   maxlim: 193247   bits: 18/18
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     95994 |   91551   311287 |   30517   19276  3681560   191.0 |  1.754 % |
c |     96096 |   91551   311287 |   33568   19378  3703843   191.1 |  1.775 % |
c |     96246 |   91551   311287 |   36925   19528  3722802   190.6 |  1.775 % |
c |     96471 |   91551   311287 |   40618   19753  3810541   192.9 |  1.775 % |
c |     96811 |   91551   311287 |   44679   20093  3856602   191.9 |  1.775 % |
c |     97319 |   91551   311287 |   49147   20601  3980720   193.2 |  1.775 % |
c |     98078 |   91551   311287 |   54062   21360  4197445   196.5 |  1.775 % |
c |     99219 |   91551   311287 |   59468   22501  4443126   197.5 |  1.775 % |
c |    100927 |   91551   311287 |   65415   24209  5125900   211.7 |  1.775 % |
c |    103490 |   91551   311287 |   71957   26772  5785251   216.1 |  1.775 % |
c |    107334 |   91551   311287 |   79153   30616  7230782   236.2 |  1.775 % |
c |    113103 |   91551   311287 |   87068   36385  8775221   241.2 |  1.775 % |
c |    121753 |   91551   311287 |   95775   45035 11913321   264.5 |  1.775 % |
c |    134728 |   91506   311130 |  105352   58002 16013485   276.1 |  1.796 % |
c |    154190 |   91497   311099 |  115888   77462 23776761   306.9 |  1.802 % |
c |    183385 |   91480   311042 |  127477  106650 33287203   312.1 |  1.812 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v CO100001_bit0 -CO100002_bit0 -CO100003_bit0 -CO100004_bit0 -CO100005_bit0 -CO100006_bit0 -CO100007_bit0 -CO100008_bit0 -CO100009_bit0 -CO100010_bit0 -CO100011_bit0 -CO100012_bit0 -CO100013_bit0 -CO100014_bit0 -CO100015_bit0 -CO100016_bit0 -CO100017_bit0 -CO100018_bit0 -CO100019_bit0 -CO100020_bit0 -CO100021_bit0 -CO100022_bit0 -CO100023_bit0 -CO100024_bit0 -CO100025_bit0 -CO100026_bit0 CO100027_bit0 -CO100028_bit0 -CO100029_bit0 -CO100030_bit0 -CO100031_bit0 -CO100032_bit0 -CO100033_bit0 -CO100034_bit0 -CO100035_bit0 -CO100036_bit0 -CO100037_bit0 -CO100038_bit0 -CO100039_bit0 -CO100040_bit0 -CO100041_bit0 -CO100042_bit0 -CO100043_bit0 -CO100044_bit0 -CO100045_bit0 -CO100046_bit0 -CO100047_bit0 -CO100048_bit0 -CO100049_bit0 -CO100050_bit0 -CO100051_bit0 -CO100052_bit0 -CO100053_bit0 -CO100054_bit0 -CO100055_bit0 -CO100056_bit0 -CO100057_bit0 -CO100058_bit0 -CO100059_bit0 -CO100060_bit0 -CO100061_bit0 -CO100062_bit0 -CO100063_bit0 -CO100064_bit0 -CO100065_bit0 CO100066_bit0 -CO100067_bit0 -CO100068_bit0 -CO100069_bit0 -CO100070_bit0 -CO100071_bit0 -CO100072_bit0 -CO100073_bit0 -CO100074_bit0 -CO100075_bit0 -CO100076_bit0 -CO100077_bit0 -CO100078_bit0 -CO100079_bit0 -CO100080_bit0 CO100081_bit0 -CO100082_bit0 CO100083_bit0 -CO100084_bit0 -CO100085_bit0 -CO100086_bit0 -CO100087_bit0 -CO100088_bit0 -CO100089_bit0 -CO100090_bit0 -CO100091_bit0 -CO100092_bit0 -CO100093_bit0 -CO100094_bit0 -CO100095_bit0 -CO100096_bit0 -CO100097_bit0 -CO100098_bit0 -CO100099_bit0 CO100100_bit0 -CO100101_bit0 -CO100102_bit0 -CO100103_bit0 -CO100104_bit0 -CO100105_bit0 -CO100106_bit0 -CO100107_bit0 -CO100108_bit0 -CO100109_bit0 CO100110_bit0 -CO100111_bit0 -CO100112_bit0 -CO100113_bit0 -CO100114_bit0 -CO100115_bit0 -CO100116_bit0 -CO100117_bit0 -CO100118_bit0 -CO100119_bit0 -CO100120_bit0 -CO100121_bit0 -CO100122_bit0 -CO100123_bit0 -CO100124_bit0 -CO100125_bit0 -CO100126_bit0 -CO100127_bit0 -CO100128_bit0 -CO100129_bit0 -CO100130_bit0 -CO100131_bit0 -CO100132_bit0 -CO100133_bit0 -CO100134_bit0 CO100135_bit0 -CO100136_bit0 -CO100137_bit0 CO100138_bit0 -CO100139_bit0 -CO100140_bit0 -CO100141_bit0 -CO100142_bit0 -CO100143_bit0 -CO100144_bit0 -CO100145_bit0 -CO100146_bit0 -CO100147_bit0 -CO100148_bit0 -CO100149_bit0 -CO100150_bit0 -CO100151_bit0 -CO100152_bit0 -CO100153_bit0 -CO100154_bit0 -CO100155_bit0 -CO100156_bit0 -CO100157_bit0 -CO100158_bit0 -CO100159_bit0 -CO100160_bit0 -CO100161_bit0 -CO100162_bit0 -CO100163_bit0 -CO100164_bit0 -CO100165_bit0 CO100166_bit0 -CO100167_bit0 -CO100168_bit0 -CO100169_bit0 -CO100170_bit0 -CO100171_bit0 -CO100172_bit0 -CO100173_bit0 -CO100174_bit0 -CO100175_bit0 -CO100176_bit0 -CO100177_bit0 -CO100178_bit0 -CO100179_bit0 -CO100180_bit0 -CO100181_bit0 -CO100182_bit0 -CO100183_bit0 -CO100184_bit0 -CO100185_bit0 -CO100186_bit0 -CO100187_bit0 -CO100188_bit0 -CO100189_bit0 -CO100190_bit0 -CO100191_bit0 -CO100192_bit0 -CO100193_bit0 -CO100194_bit0 -CO100195_bit0 -CO100196_bit0 -CO100197_bit0 -CO100198_bit0 CO100199_bit0 -CO100200_bit0 -CO100201_bit0 -CO100202_bit0 -CO100203_bit0 -CO100204_bit0 -CO100205_bit0 -CO100206_bit0 -CO100207_bit0 -CO100208_bit0 -CO100209_bit0 -CO100210_bit0 -CO100211_bit0 -CO100212_bit0 -CO100213_bit0 -CO100214_bit0 -CO100215_bit0 -CO100216_bit0 -CO100217_bit0 -CO100218_bit0 -CO100219_bit0 -CO100220_bit0 -CO100221_bit0 -CO100222_bit0 -CO100223_bit0 -CO100224_bit0 -CO100225_bit0 -CO100226_bit0 -CO100227_bit0 -CO100228_bit0 -CO100229_bit0 CO100230_bit0 -CO100231_bit0 -CO100232_bit0 -CO100233_bit0 -CO100234_bit0 -CO100235_bit0 -CO100236_bit0 -CO100237_bit0 -CO100238_bit0 -CO100239_bit0 -CO100240_bit0 -CO100241_bit0 -CO100242_bit0 -CO100243_bit0 -CO100244_bit0 -CO100245_bit0 -CO100246_bit0 -CO100247_bit0 -CO100248_bit0 -CO100249_bit0 -CO100250_bit0 -CO100251_bit0 -CO100252_bit0 -CO100253_bit0 -CO100254_bit0 -CO100255_bit0 -CO100256_bit0 -CO100257_bit0 -CO100258_bit0 -CO100259_bit0 -CO100260_bit0 -CO100261_bit0 -CO100262_bit0 -CO100263_bit0 -CO100264_bit0 -CO100265_bit0 -CO100266_bit0 -CO100267_bit0 -CO100268_bit0 -CO100269_bit0 -CO100270_bit0 -CO100271_bit0 -CO100272_bit0 -CO100273_bit0 -CO100274_bit0 -CO100275_bit0 -CO100276_bit0 -CO100277_bit0 -CO100278_bit0 -CO100279_bit0 -CO100280_bit0 -CO100281_bit0 -CO100282_bit0 -CO100283_bit0 -CO100284_bit0 -CO100285_bit0 -CO100286_bit0 -CO100287_bit0 -CO100288_bit0 -CO100289_bit0 -CO100290_bit0 -CO100291_bit0 -CO100292_bit0 -CO100293_bit0 CO100294_bit0 -CO100295_bit0 -CO100296_bit0 -CO100297_bit0 -CO100298_bit0 -CO100299_bit0 -CO100300_bit0 -CO100301_bit0 -CO100302_bit0 -CO100303_bit0 -CO100304_bit0 -CO100305_bit0 -CO100306_bit0 -CO100307_bit0 -CO100308_bit0 -CO100309_bit0 -CO100310_bit0 -CO100311_bit0 -CO100312_bit0 -CO100313_bit0 -CO100314_bit0 -CO100315_bit0 -CO100316_bit0 -CO100317_bit0 -CO100318_bit0 -CO100319_bit0 -CO100320_bit0 -CO100321_bit0 -CO100322_bit0 -CO100323_bit0 -CO100324_bit0 -CO100325_bit0 -CO100326_bit0 -CO100327_bit0 -CO100328_bit0 -CO100329_bit0 -CO100330_bit0 -CO100331_bit0 -CO100332_bit0 -CO100333_bit0 -CO100334_bit0 -CO100335_bit0 -CO100336_bit0 -CO100337_bit0 -CO100338_bit0 -CO100339_bit0 -CO100340_bit0 -CO100341_bit0 -CO100342_bit0 -CO100343_bit0 -CO100344_bit0 -CO100345_bit0 -CO100346_bit0 -CO100347_bit0 -CO100348_bit0 -CO100349_bit0 -CO100350_bit0 -CO100351_bit0 -CO100352_bit0 -CO100353_bit0 -CO100354_bit0 -CO100355_bit0 -CO100356_bit0 -CO100357_bit0 -CO100358_bit0 -CO100359_bit0 -CO100360_bit0 -CO100361_bit0 -CO100362_bit0 -CO100363_bit0 -CO100364_bit0 -CO100365_bit0 -CO100366_bit0 -CO100367_bit0 -CO100368_bit0 -CO100369_bit0 -CO100370_bit0 -CO100371_bit0 -CO100372_bit0 -CO100373_bit0 -CO100374_bit0 -CO100375_bit0 -CO100376_bit0 -CO100377_bit0 -CO100378_bit0 -CO100379_bit0 -CO100380_bit0 -CO100381_bit0 -CO100382_bit0 -CO100383_bit0 -CO100384_bit0 -CO100385_bit0 -CO100386_bit0 -CO100387_bit0 -CO100388_bit0 -CO100389_bit0 -CO100390_bit0 -CO100391_bit0 -CO100392_bit0 -CO100393_bit0 -CO100394_bit0 -CO100395_bit0 -CO100396_bit0 -CO100397_bit0 -CO100398_bit0 -CO100399_bit0 -CO100400_bit0 -CO100401_bit0 -CO100402_bit0 -CO100403_bit0 -CO100404_bit0 -CO100405_bit0 -CO100406_bit0 CO100407_bit0 -CO100408_bit0 -CO100409_bit0 -CO100410_bit0 -CO100411_bit0 -CO100412_bit0 -CO100413_bit0 -CO100414_bit0 -CO100415_bit0 -CO100416_bit0 -CO100417_bit0 -CO100418_bit0 -CO100419_bit0 -CO100420_bit0 -CO100421_bit0 -CO100422_bit0 -CO100423_bit0 -CO100424_bit0 -CO100425_bit0 -CO100426_bit0 -CO100427_bit0 -CO100428_bit0 -CO100429_bit0 -CO100430_bit0 -CO100431_bit0 -CO100432_bit0 -CO100433_bit0 -CO100434_bit0 -CO100435_bit0 -CO100436_bit0 -CO100437_bit0 -CO100438_bit0 -CO100439_bit0 -CO100440_bit0 -CO100441_bit0 -CO100442_bit0 -CO100443_bit0 -CO100444_bit0 -CO100445_bit0 CO100446_bit0 -CO100447_bit0 -CO100448_bit0 -CO100449_bit0 -CO100450_bit0 -CO100451_bit0 -CO100452_bit0 -CO100453_bit0 -CO100454_bit0 -CO100455_bit0 -CO100456_bit0 -CO100457_bit0 -CO100458_bit0 -CO100459_bit0 -CO100460_bit0 -CO100461_bit0 -CO100462_bit0 -CO100463_bit0 -CO100464_bit0 -CO100465_bit0 -CO100466_bit0 -CO100467_bit0 -CO100468_bit0 -CO100469_bit0 -CO100470_bit0 -CO100471_bit0 -CO100472_bit0 -CO100473_bit0 -CO100474_bit0 -CO100475_bit0 -CO100476_bit0 -CO100477_bit0 -CO100478_bit0 -CO100479_bit0 -CO100480_bit0 -CO100481_bit0 -CO100482_bit0 -CO100483_bit0 -CO100484_bit0 -CO100485_bit0 -CO100486_bit0 -CO100487_bit0 -CO100488_bit0 -CO100489_bit0 -CO100490_bit0 -CO100491_bit0 -CO100492_bit0 -CO100493_bit0 -CO100494_bit0 -CO100495_bit0 -CO100496_bit0 -CO100497_bit0 -CO100498_bit0 -CO100499_bit0 -CO100500_bit0 -CO100501_bit0 -CO100502_bit0 -CO100503_bit0 -CO100504_bit0 -CO100505_bit0 -CO100506_bit0 -CO100507_bit0 -CO100508_bit0 -CO100509_bit0 CO100510_bit0 -CO100511_bit0 -CO100512_bit0 -CO100513_bit0 -CO100514_bit0 -CO100515_bit0 -CO100516_bit0 -CO100517_bit0 -CO100518_bit0 -CO100519_bit0 -CO100520_bit0 -CO100521_bit0 -CO100522_bit0 -CO100523_bit0 -CO100524_bit0 -CO100525_bit0 -CO100526_bit0 -CO100527_bit0 -CO100528_bit0 -CO100529_bit0 -CO100530_bit0 -CO100531_bit0 -CO100532_bit0 -CO100533_bit0 -CO100534_bit0 -CO100535_bit0 -CO100536_bit0 -CO100537_bit0 -CO100538_bit0 -CO100539_bit0 -CO100540_bit0 -CO100541_bit0 -CO100542_bit0 -CO100543_bit0 -CO100544_bit0 -CO100545_bit0 -CO100546_bit0 -CO100547_bit0 -CO100548_bit0 -CO100549_bit0 -CO100550_bit0 -CO100551_bit0 CO100552_bit0 -CO100553_bit0 -CO100554_bit0 -CO100555_bit0 -CO100556_bit0 -CO100557_bit0 -CO100558_bit0 -CO100559_bit0 -CO100560_bit0 -CO100561_bit0 -CO100562_bit0 -CO100563_bit0 -CO100564_bit0 -CO100565_bit0 -CO100566_bit0 -CO100567_bit0 -CO100568_bit0 -CO100569_bit0 -CO100570_bit0 -CO100571_bit0 -CO100572_bit0 CO100573_bit0 -CO100574_bit0 -CO100575_bit0 -CO100576_bit0 -CO100577_bit0 -CO100578_bit0 -CO100579_bit0 -CO100580_bit0 -CO100581_bit0 -CO100582_bit0 -CO100583_bit0 -CO100584_bit0 -CO100585_bit0 -CO100586_bit0 -CO100587_bit0 -CO100588_bit0 -CO100589_bit0 -CO100590_bit0 -CO100591_bit0 -CO100592_bit0 -CO100593_bit0 -CO100594_bit0 -CO100595_bit0 -CO100596_bit0 -CO100597_bit0 -CO100598_bit0 -CO100599_bit0 -CO100600_bit0 -CO100601_bit0 -CO100602_bit0 -CO100603_bit0 -CO100604_bit0 -CO100605_bit0 -CO100606_bit0 -CO100607_bit0 -CO100608_bit0 -CO100609_bit0 -CO100610_bit0 -CO100611_bit0 -CO100612_bit0 -CO100613_bit0 -CO100614_bit0 -CO100615_bit0 -CO100616_bit0 -CO100617_bit0 -CO100618_bit0 -CO100619_bit0 -CO100620_bit0 -CO100621_bit0 -CO100622_bit0 -CO100623_bit0 -CO100624_bit0 -CO100625_bit0 -CO100626_bit0 -CO100627_bit0 -CO100628_bit0 -CO100629_bit0 -CO100630_bit0 -CO100631_bit0 -CO100632_bit0 -CO100633_bit0 -CO100634_bit0 -CO100635_bit0 -CO100636_bit0 -CO100637_bit0 -CO100638_bit0 -CO100639_bit0 -CO100640_bit0 -CO100641_bit0 -CO100642_bit0 -CO100643_bit0 -CO100644_bit0 -CO100645_bit0 -CO100646_bit0 -CO100647_bit0 -CO100648_bit0 -CO100649_bit0 -CO100650_bit0 -CO100651_bit0 -CO100652_bit0 -CO100653_bit0 -CO100654_bit0 -CO100655_bit0 -CO100656_bit0 -CO100657_bit0 -CO100658_bit0 -CO100659_bit0 -CO100660_bit0 -CO100661_bit0 -CO100662_bit0 -CO100663_bit0 -CO100664_bit0 -CO100665_bit0 -CO100666_bit0 -CO100667_bit0 -CO100668_bit0 -CO100669_bit0 -CO100670_bit0 -CO100671_bit0 -CO100672_bit0 -CO100673_bit0 -CO100674_bit0 -CO100675_bit0 -CO100676_bit0 -CO100677_bit0 -CO100678_bit0 -CO100679_bit0 -CO100680_bit0 -CO100681_bit0 -CO100682_bit0 -CO100683_bit0 -CO100684_bit0 -CO100685_bit0 -CO100686_bit0 -CO100687_bit0 -CO100688_bit0 -CO100689_bit0 -CO100690_bit0 -CO100691_bit0 -CO100692_bit0 -CO100693_bit0 -CO100694_bit0 -CO100695_bit0 -CO100696_bit0 -CO100697_bit0 -CO100698_bit0 -CO100699_bit0 -CO100700_bit0 -CO100701_bit0 -CO100702_bit0 -CO100703_bit0 CO100704_bit0 -CO100705_bit0 -CO100706_bit0 -CO100707_bit0 -CO100708_bit0 -CO100709_bit0 -CO100710_bit0 -CO100711_bit0 -CO100712_bit0 -CO100713_bit0 -CO100714_bit0 -CO100715_bit0 -CO100716_bit0 -CO100717_bit0 -CO100718_bit0 -CO100719_bit0 -CO100720_bit0 -CO100721_bit0 -CO100722_bit0 -CO100723_bit0 -CO100724_bit0 -CO100725_bit0 -CO100726_bit0 -CO100727_bit0 -CO100728_bit0 -CO100729_bit0 -CO100730_bit0 -CO100731_bit0 -CO100732_bit0 -CO100733_bit0 -CO100734_bit0 -CO100735_bit0 -CO100736_bit0 -CO100737_bit0 -CO100738_bit0 -CO100739_bit0 -CO100740_bit0 -CO100741_bit0 -CO100742_bit0 -CO100743_bit0 -CO100744_bit0 -CO100745_bit0 -CO100746_bit0 -CO100747_bit0 -CO100748_bit0 -CO100749_bit0 -CO100750_bit0 CO100751_bit0 -CO100752_bit0 -CO100753_bit0 -CO100754_bit0 -CO100755_bit0 -CO100756_bit0 -CO100757_bit0 -CO100758_bit0 CO100759_bit0 -CO100760_bit0 -CO100761_bit0 -CO100762_bit0 -CO100763_bit0 -CO100764_bit0 -CO100765_bit0 -CO100766_bit0 -CO100767_bit0 -CO100768_bit0 -CO100769_bit0 -CO100770_bit0 -CO100771_bit0 -CO100772_bit0 -CO100773_bit0 -CO100774_bit0 -CO100775_bit0 -CO100776_bit0 -CO100777_bit0 -CO100778_bit0 -CO100779_bit0 -CO100780_bit0 -CO100781_bit0 -CO100782_bit0 -CO100783_bit0 -CO100784_bit0 -CO100785_bit0 -CO100786_bit0 -CO100787_bit0 -CO100788_bit0 -CO100789_bit0 -CO100790_bit0 -CO100791_bit0 -CO100792_bit0 -CO100793_bit0 -CO100794_bit0 -CO100795_bit0 -CO100796_bit0 -CO100797_bit0 -CO100798_bit0 -CO100799_bit0 -CO100800_bit0 -CO100801_bit0 -CO100802_bit0 -CO100803_bit0 -CO100804_bit0 -CO100805_bit0 -CO100806_bit0 -CO100807_bit0 -CO100808_bit0 -CO100809_bit0 -CO100810_bit0 -CO100811_bit0 -CO100812_bit0 -CO100813_bit0 -CO100814_bit0 -CO100815_bit0 -CO100816_bit0 -CO100817_bit0 -CO100818_bit0

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/14023/stat): 14023 (minisat+_script) R 14022 14023 22582 0 -1 0 19 0 0 0 0 0 0 0 19 0 1 0 1797016803 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/14023/statm): 174 3 169 147 0 27 0
[pid=14023] 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=14024
New process pid=14025
New process pid=14026
execve syscall for /bin/sed executable
One traced child (pid=14025) 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=14026) exited with status: 0
One traced child (pid=14024) exited with status: 0
New process pid=14027
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-13-7-lp4l.opb

[startup+10.0032 s]
Raw data (loadavg): 0.93 0.95 0.90 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 2451 0 0 0 974 10 0 0 25 0 1 0 1797016808 10907648 2310 4294967295 134512640 135094434 3221224432 3221223024 134557232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 2663 2310 145 145 0 2518 0
[pid=14027] vsize: 10652
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 12776

[startup+20.0038 s]
Raw data (loadavg): 0.94 0.96 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 7027 0 0 0 1940 29 0 0 25 0 1 0 1797016808 28471296 6098 4294967295 134512640 135094434 3221224432 3221221984 134677330 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 6951 6098 145 145 0 6806 0
[pid=14027] vsize: 27804
Current children cumulated CPU time (s) 19.7
Current children cumulated vsize (Kb) 29928

[startup+30.0044 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 7478 0 0 0 2933 32 0 0 25 0 1 0 1797016808 29356032 6316 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 7167 6316 145 145 0 7022 0
[pid=14027] vsize: 28668
Current children cumulated CPU time (s) 29.66
Current children cumulated vsize (Kb) 30792

[startup+40.0039 s]
Raw data (loadavg): 0.95 0.96 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 7906 0 0 0 3924 35 0 0 25 0 1 0 1797016808 31100928 6744 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 7593 6744 145 145 0 7448 0
[pid=14027] vsize: 30372
Current children cumulated CPU time (s) 39.6
Current children cumulated vsize (Kb) 32496

[startup+50.0045 s]
Raw data (loadavg): 0.96 0.96 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 8401 0 0 0 4914 40 0 0 25 0 1 0 1797016808 33112064 7239 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 8084 7239 145 145 0 7939 0
[pid=14027] vsize: 32336
Current children cumulated CPU time (s) 49.55
Current children cumulated vsize (Kb) 34460

[startup+60.0041 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 8949 0 0 0 5905 44 0 0 25 0 1 0 1797016808 35405824 7787 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 8644 7787 145 145 0 8499 0
[pid=14027] vsize: 34576
Current children cumulated CPU time (s) 59.5
Current children cumulated vsize (Kb) 36700

[startup+70.0046 s]
Raw data (loadavg): 0.97 0.96 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 9502 0 0 0 6895 47 0 0 25 0 1 0 1797016808 37666816 8340 4294967295 134512640 135094434 3221224432 3221222864 134591762 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 9196 8340 145 145 0 9051 0
[pid=14027] vsize: 36784
Current children cumulated CPU time (s) 69.43
Current children cumulated vsize (Kb) 38908

[startup+80.0052 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 10010 0 0 0 7889 50 0 0 25 0 1 0 1797016808 38871040 8637 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 9490 8637 145 145 0 9345 0
[pid=14027] vsize: 37960
Current children cumulated CPU time (s) 79.4
Current children cumulated vsize (Kb) 40084

[startup+90.0048 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 10486 0 0 0 8879 55 0 0 25 0 1 0 1797016808 40812544 9113 4294967295 134512640 135094434 3221224432 3221223024 134556847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 9964 9113 145 145 0 9819 0
[pid=14027] vsize: 39856
Current children cumulated CPU time (s) 89.35
Current children cumulated vsize (Kb) 41980

[startup+100.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 10988 0 0 0 9871 59 0 0 25 0 1 0 1797016808 42856448 9615 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 10463 9615 145 145 0 10318 0
[pid=14027] vsize: 41852
Current children cumulated CPU time (s) 99.31
Current children cumulated vsize (Kb) 43976

[startup+110.006 s]
Raw data (loadavg): 0.98 0.96 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 11492 0 0 0 10862 63 0 0 25 0 1 0 1797016808 44912640 10119 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 10965 10119 145 145 0 10820 0
[pid=14027] vsize: 43860
Current children cumulated CPU time (s) 109.26
Current children cumulated vsize (Kb) 45984

[startup+120.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 11759 0 0 0 11857 65 0 0 25 0 1 0 1797016808 46129152 10386 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 11262 10386 145 145 0 11117 0
[pid=14027] vsize: 45048
Current children cumulated CPU time (s) 119.23
Current children cumulated vsize (Kb) 47172

[startup+130.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 12177 0 0 0 12850 68 0 0 25 0 1 0 1797016808 47833088 10804 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 11678 10804 145 145 0 11533 0
[pid=14027] vsize: 46712
Current children cumulated CPU time (s) 129.19
Current children cumulated vsize (Kb) 48836

[startup+140.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 12708 0 0 0 13841 72 0 0 25 0 1 0 1797016808 49999872 11335 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 12207 11335 145 145 0 12062 0
[pid=14027] vsize: 48828
Current children cumulated CPU time (s) 139.14
Current children cumulated vsize (Kb) 50952

[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 13208 0 0 0 14832 75 0 0 25 0 1 0 1797016808 52043776 11835 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 12706 11835 145 145 0 12561 0
[pid=14027] vsize: 50824
Current children cumulated CPU time (s) 149.08
Current children cumulated vsize (Kb) 52948

[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 13621 0 0 0 15826 78 0 0 25 0 1 0 1797016808 53727232 12248 4294967295 134512640 135094434 3221224432 3221223024 134551997 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 13117 12248 145 145 0 12972 0
[pid=14027] vsize: 52468
Current children cumulated CPU time (s) 159.05
Current children cumulated vsize (Kb) 54592

[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 14085 0 0 0 16817 82 0 0 25 0 1 0 1797016808 55623680 12712 4294967295 134512640 135094434 3221224432 3221223088 134558254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 13580 12712 145 145 0 13435 0
[pid=14027] vsize: 54320
Current children cumulated CPU time (s) 169
Current children cumulated vsize (Kb) 56444

[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 14575 0 0 0 17811 85 0 0 17 0 1 0 1797016808 57622528 13202 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 14068 13202 145 145 0 13923 0
[pid=14027] vsize: 56272
Current children cumulated CPU time (s) 178.97
Current children cumulated vsize (Kb) 58396

[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 15036 0 0 0 18803 89 0 0 25 0 1 0 1797016808 59502592 13663 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 14527 13663 145 145 0 14382 0
[pid=14027] vsize: 58108
Current children cumulated CPU time (s) 188.93
Current children cumulated vsize (Kb) 60232

[startup+200.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 15423 0 0 0 19795 91 0 0 25 0 1 0 1797016808 61083648 14050 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 14913 14050 145 145 0 14768 0
[pid=14027] vsize: 59652
Current children cumulated CPU time (s) 198.87
Current children cumulated vsize (Kb) 61776

[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 15847 0 0 0 20787 95 0 0 25 0 1 0 1797016808 62812160 14474 4294967295 134512640 135094434 3221224432 3221223088 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 15335 14474 145 145 0 15190 0
[pid=14027] vsize: 61340
Current children cumulated CPU time (s) 208.83
Current children cumulated vsize (Kb) 63464

[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 16340 0 0 0 21778 99 0 0 25 0 1 0 1797016808 64823296 14967 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 15826 14967 145 145 0 15681 0
[pid=14027] vsize: 63304
Current children cumulated CPU time (s) 218.78
Current children cumulated vsize (Kb) 65428

[startup+230.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) T 14023 14023 22582 0 -1 0 16796 0 0 0 22771 102 0 0 25 0 1 0 1797016808 66682880 15423 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14027/statm): 16280 15423 145 145 0 16135 0
[pid=14027] vsize: 65120
Current children cumulated CPU time (s) 228.74
Current children cumulated vsize (Kb) 67244

[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 17255 0 0 0 23764 105 0 0 25 0 1 0 1797016808 68562944 15882 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 16739 15882 145 145 0 16594 0
[pid=14027] vsize: 66956
Current children cumulated CPU time (s) 238.7
Current children cumulated vsize (Kb) 69080

[startup+250.014 s]
Raw data (loadavg): 1.06 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 17692 0 0 0 24759 107 0 0 25 0 1 0 1797016808 70344704 16319 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 17174 16319 145 145 0 17029 0
[pid=14027] vsize: 68696
Current children cumulated CPU time (s) 248.67
Current children cumulated vsize (Kb) 70820

[startup+260.014 s]
Raw data (loadavg): 1.05 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18193 0 0 0 25750 111 0 0 25 0 1 0 1797016808 72388608 16820 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 17673 16820 145 145 0 17528 0
[pid=14027] vsize: 70692
Current children cumulated CPU time (s) 258.62
Current children cumulated vsize (Kb) 72816

[startup+270.015 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 26743 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 268.58
Current children cumulated vsize (Kb) 74224

[startup+280.015 s]
Raw data (loadavg): 1.04 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 27743 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223076 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 278.58
Current children cumulated vsize (Kb) 74224

[startup+290.016 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 28743 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 288.58
Current children cumulated vsize (Kb) 74224

[startup+300.017 s]
Raw data (loadavg): 1.03 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 29744 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221222800 134519172 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 298.59
Current children cumulated vsize (Kb) 74224

[startup+310.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 30743 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223056 134557636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 308.58
Current children cumulated vsize (Kb) 74224

[startup+320.018 s]
Raw data (loadavg): 1.02 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 31743 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 318.58
Current children cumulated vsize (Kb) 74224

[startup+330.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 32744 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 328.59
Current children cumulated vsize (Kb) 74224

[startup+340.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 33744 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 338.59
Current children cumulated vsize (Kb) 74224

[startup+350.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 34744 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 348.59
Current children cumulated vsize (Kb) 74224

[startup+360.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 35744 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 358.59
Current children cumulated vsize (Kb) 74224

[startup+370.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 36744 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223024 134556904 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 368.59
Current children cumulated vsize (Kb) 74224

[startup+380.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 37745 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 378.6
Current children cumulated vsize (Kb) 74224

[startup+390.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 38745 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 388.6
Current children cumulated vsize (Kb) 74224

[startup+400.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18694 0 0 0 39745 114 0 0 25 0 1 0 1797016808 73830400 17174 4294967295 134512640 135094434 3221224432 3221223024 134556933 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17174 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 398.6
Current children cumulated vsize (Kb) 74224

[startup+410.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18695 0 0 0 40745 114 0 0 25 0 1 0 1797016808 73830400 17175 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17175 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 408.6
Current children cumulated vsize (Kb) 74224

[startup+420.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18695 0 0 0 41746 114 0 0 25 0 1 0 1797016808 73830400 17175 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17175 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 418.61
Current children cumulated vsize (Kb) 74224

[startup+430.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18695 0 0 0 42746 114 0 0 25 0 1 0 1797016808 73830400 17175 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17175 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 428.61
Current children cumulated vsize (Kb) 74224

[startup+440.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 18695 0 0 0 43746 114 0 0 25 0 1 0 1797016808 73830400 17175 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18025 17175 145 145 0 17880 0
[pid=14027] vsize: 72100
Current children cumulated CPU time (s) 438.61
Current children cumulated vsize (Kb) 74224

[startup+450.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19301 0 0 0 44741 116 0 0 25 0 1 0 1797016808 75071488 17478 4294967295 134512640 135094434 3221224432 3221223088 134558238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17478 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 448.58
Current children cumulated vsize (Kb) 75436

[startup+460.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 45740 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 458.58
Current children cumulated vsize (Kb) 75436

[startup+470.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 46740 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 468.58
Current children cumulated vsize (Kb) 75436

[startup+480.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 47741 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223104 134556263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 478.59
Current children cumulated vsize (Kb) 75436

[startup+490.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 48741 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 488.59
Current children cumulated vsize (Kb) 75436

[startup+500.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 49741 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 498.59
Current children cumulated vsize (Kb) 75436

[startup+510.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 50741 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 508.59
Current children cumulated vsize (Kb) 75436

[startup+520.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 51742 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 518.6
Current children cumulated vsize (Kb) 75436

[startup+530.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 52742 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 528.6
Current children cumulated vsize (Kb) 75436

[startup+540.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 53742 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 538.6
Current children cumulated vsize (Kb) 75436

[startup+550.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 54742 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 548.6
Current children cumulated vsize (Kb) 75436

[startup+560.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 55742 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 558.6
Current children cumulated vsize (Kb) 75436

[startup+570.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 56743 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223044 134563061 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 568.61
Current children cumulated vsize (Kb) 75436

[startup+580.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 57743 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223024 134556834 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 578.61
Current children cumulated vsize (Kb) 75436

[startup+590.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19427 0 0 0 58743 117 0 0 25 0 1 0 1797016808 75071488 17479 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18328 17479 145 145 0 18183 0
[pid=14027] vsize: 73312
Current children cumulated CPU time (s) 588.61
Current children cumulated vsize (Kb) 75436

[startup+600.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 19902 0 0 0 59734 121 0 0 25 0 1 0 1797016808 77017088 17954 4294967295 134512640 135094434 3221224432 3221223024 134557022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 18803 17954 145 145 0 18658 0
[pid=14027] vsize: 75212
Current children cumulated CPU time (s) 598.56
Current children cumulated vsize (Kb) 77336

[startup+610.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 20475 0 0 0 60723 125 0 0 25 0 1 0 1797016808 79364096 18527 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 19376 18527 145 145 0 19231 0
[pid=14027] vsize: 77504
Current children cumulated CPU time (s) 608.49
Current children cumulated vsize (Kb) 79628

[startup+620.03 s]
Raw data (loadavg): 1.00 0.99 0.91 1/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) T 14023 14023 22582 0 -1 0 21016 0 0 0 61715 128 0 0 25 0 1 0 1797016808 81580032 19068 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14027/statm): 19917 19068 145 145 0 19772 0
[pid=14027] vsize: 79668
Current children cumulated CPU time (s) 618.44
Current children cumulated vsize (Kb) 81792

[startup+630.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 21555 0 0 0 62707 132 0 0 25 0 1 0 1797016808 83787776 19607 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 20456 19607 145 145 0 20311 0
[pid=14027] vsize: 81824
Current children cumulated CPU time (s) 628.4
Current children cumulated vsize (Kb) 83948

[startup+640.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 22281 0 0 0 63700 135 0 0 25 0 1 0 1797016808 86761472 20333 4294967295 134512640 135094434 3221224432 3221223104 134555743 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 21182 20333 145 145 0 21037 0
[pid=14027] vsize: 84728
Current children cumulated CPU time (s) 638.36
Current children cumulated vsize (Kb) 86852

[startup+650.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 22673 0 0 0 64695 137 0 0 25 0 1 0 1797016808 88367104 20725 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 21574 20725 145 145 0 21429 0
[pid=14027] vsize: 86296
Current children cumulated CPU time (s) 648.33
Current children cumulated vsize (Kb) 88420

[startup+660.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 23162 0 0 0 65687 141 0 0 25 0 1 0 1797016808 90370048 21214 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 22063 21214 145 145 0 21918 0
[pid=14027] vsize: 88252
Current children cumulated CPU time (s) 658.29
Current children cumulated vsize (Kb) 90376

[startup+670.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 23562 0 0 0 66680 144 0 0 25 0 1 0 1797016808 92008448 21614 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 22463 21614 145 145 0 22318 0
[pid=14027] vsize: 89852
Current children cumulated CPU time (s) 668.25
Current children cumulated vsize (Kb) 91976

[startup+680.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 24007 0 0 0 67672 147 0 0 25 0 1 0 1797016808 93831168 22059 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 22908 22059 145 145 0 22763 0
[pid=14027] vsize: 91632
Current children cumulated CPU time (s) 678.2
Current children cumulated vsize (Kb) 93756

[startup+690.034 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 24619 0 0 0 68661 152 0 0 25 0 1 0 1797016808 96337920 22671 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 23520 22671 145 145 0 23375 0
[pid=14027] vsize: 94080
Current children cumulated CPU time (s) 688.14
Current children cumulated vsize (Kb) 96204

[startup+700.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 25249 0 0 0 69653 156 0 0 25 0 1 0 1797016808 98910208 23301 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 24148 23301 145 145 0 24003 0
[pid=14027] vsize: 96592
Current children cumulated CPU time (s) 698.1
Current children cumulated vsize (Kb) 98716

[startup+710.035 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 25795 0 0 0 70645 160 0 0 25 0 1 0 1797016808 101142528 23847 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 24693 23847 145 145 0 24548 0
[pid=14027] vsize: 98772
Current children cumulated CPU time (s) 708.06
Current children cumulated vsize (Kb) 100896

[startup+720.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 26268 0 0 0 71636 163 0 0 25 0 1 0 1797016808 103071744 24320 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 25164 24320 145 145 0 25019 0
[pid=14027] vsize: 100656
Current children cumulated CPU time (s) 718
Current children cumulated vsize (Kb) 102780

[startup+730.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 26689 0 0 0 72629 166 0 0 25 0 1 0 1797016808 104792064 24741 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 25584 24741 145 145 0 25439 0
[pid=14027] vsize: 102336
Current children cumulated CPU time (s) 727.96
Current children cumulated vsize (Kb) 104460

[startup+740.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 27160 0 0 0 73622 170 0 0 25 0 1 0 1797016808 106979328 25212 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 26118 25212 145 145 0 25973 0
[pid=14027] vsize: 104472
Current children cumulated CPU time (s) 737.93
Current children cumulated vsize (Kb) 106596

[startup+750.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 27655 0 0 0 74614 173 0 0 25 0 1 0 1797016808 109002752 25707 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 26612 25707 145 145 0 26467 0
[pid=14027] vsize: 106448
Current children cumulated CPU time (s) 747.88
Current children cumulated vsize (Kb) 108572

[startup+760.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 28125 0 0 0 75608 176 0 0 25 0 1 0 1797016808 110919680 26177 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 27080 26177 145 145 0 26935 0
[pid=14027] vsize: 108320
Current children cumulated CPU time (s) 757.85
Current children cumulated vsize (Kb) 110444

[startup+770.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 28581 0 0 0 76600 180 0 0 25 0 1 0 1797016808 112783360 26633 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 27535 26633 145 145 0 27390 0
[pid=14027] vsize: 110140
Current children cumulated CPU time (s) 767.81
Current children cumulated vsize (Kb) 112264

[startup+780.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) T 14023 14023 22582 0 -1 0 29368 0 0 0 77591 184 0 0 25 0 1 0 1797016808 116002816 27420 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/14027/statm): 28321 27420 145 145 0 28176 0
[pid=14027] vsize: 113284
Current children cumulated CPU time (s) 777.76
Current children cumulated vsize (Kb) 115408

[startup+790.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 30168 0 0 0 78581 188 0 0 25 0 1 0 1797016808 119271424 28220 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 29119 28220 145 145 0 28974 0
[pid=14027] vsize: 116476
Current children cumulated CPU time (s) 787.7
Current children cumulated vsize (Kb) 118600

[startup+800.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 30597 0 0 0 79575 191 0 0 25 0 1 0 1797016808 121024512 28649 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 29547 28649 145 145 0 29402 0
[pid=14027] vsize: 118188
Current children cumulated CPU time (s) 797.67
Current children cumulated vsize (Kb) 120312

[startup+810.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 31113 0 0 0 80569 193 0 0 25 0 1 0 1797016808 123133952 29165 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 30062 29165 145 145 0 29917 0
[pid=14027] vsize: 120248
Current children cumulated CPU time (s) 807.63
Current children cumulated vsize (Kb) 122372

[startup+820.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 31539 0 0 0 81562 196 0 0 25 0 1 0 1797016808 124870656 29591 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 30486 29591 145 145 0 30341 0
[pid=14027] vsize: 121944
Current children cumulated CPU time (s) 817.59
Current children cumulated vsize (Kb) 124068

[startup+830.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 31915 0 0 0 82555 199 0 0 25 0 1 0 1797016808 126406656 29967 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 30861 29967 145 145 0 30716 0
[pid=14027] vsize: 123444
Current children cumulated CPU time (s) 827.55
Current children cumulated vsize (Kb) 125568

[startup+840.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 32310 0 0 0 83547 202 0 0 25 0 1 0 1797016808 128020480 30362 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 31255 30362 145 145 0 31110 0
[pid=14027] vsize: 125020
Current children cumulated CPU time (s) 837.5
Current children cumulated vsize (Kb) 127144

[startup+850.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 32685 0 0 0 84541 205 0 0 25 0 1 0 1797016808 129552384 30737 4294967295 134512640 135094434 3221224432 3221223088 134558129 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 31629 30737 145 145 0 31484 0
[pid=14027] vsize: 126516
Current children cumulated CPU time (s) 847.47
Current children cumulated vsize (Kb) 128640

[startup+860.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 33151 0 0 0 85534 208 0 0 25 0 1 0 1797016808 131457024 31203 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 32094 31203 145 145 0 31949 0
[pid=14027] vsize: 128376
Current children cumulated CPU time (s) 857.43
Current children cumulated vsize (Kb) 130500

[startup+870.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 33543 0 0 0 86529 210 0 0 25 0 1 0 1797016808 133058560 31595 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 32485 31595 145 145 0 32340 0
[pid=14027] vsize: 129940
Current children cumulated CPU time (s) 867.4
Current children cumulated vsize (Kb) 132064

[startup+880.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 33910 0 0 0 87523 213 0 0 25 0 1 0 1797016808 134557696 31962 4294967295 134512640 135094434 3221224432 3221223104 134556239 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 32851 31962 145 145 0 32706 0
[pid=14027] vsize: 131404
Current children cumulated CPU time (s) 877.37
Current children cumulated vsize (Kb) 133528

[startup+890.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 34293 0 0 0 88517 216 0 0 25 0 1 0 1797016808 136122368 32345 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 33233 32345 145 145 0 33088 0
[pid=14027] vsize: 132932
Current children cumulated CPU time (s) 887.34
Current children cumulated vsize (Kb) 135056

[startup+900.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 34704 0 0 0 89512 218 0 0 25 0 1 0 1797016808 137801728 32756 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 33643 32756 145 145 0 33498 0
[pid=14027] vsize: 134572
Current children cumulated CPU time (s) 897.31
Current children cumulated vsize (Kb) 136696

[startup+910.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 35078 0 0 0 90506 221 0 0 25 0 1 0 1797016808 139325440 33130 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 34015 33130 145 145 0 33870 0
[pid=14027] vsize: 136060
Current children cumulated CPU time (s) 907.28
Current children cumulated vsize (Kb) 138184

[startup+920.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 35495 0 0 0 91499 224 0 0 25 0 1 0 1797016808 141029376 33547 4294967295 134512640 135094434 3221224432 3221223024 134557500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 34431 33547 145 145 0 34286 0
[pid=14027] vsize: 137724
Current children cumulated CPU time (s) 917.24
Current children cumulated vsize (Kb) 139848

[startup+930.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 35921 0 0 0 92493 226 0 0 25 0 1 0 1797016808 142770176 33973 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 34856 33973 145 145 0 34711 0
[pid=14027] vsize: 139424
Current children cumulated CPU time (s) 927.2
Current children cumulated vsize (Kb) 141548

[startup+940.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 36257 0 0 0 93488 228 0 0 25 0 1 0 1797016808 144142336 34309 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 35191 34309 145 145 0 35046 0
[pid=14027] vsize: 140764
Current children cumulated CPU time (s) 937.17
Current children cumulated vsize (Kb) 142888

[startup+950.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 36550 0 0 0 94483 231 0 0 25 0 1 0 1797016808 145338368 34602 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 35483 34602 145 145 0 35338 0
[pid=14027] vsize: 141932
Current children cumulated CPU time (s) 947.15
Current children cumulated vsize (Kb) 144056

[startup+960.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 36944 0 0 0 95477 233 0 0 25 0 1 0 1797016808 146944000 34996 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 35875 34996 145 145 0 35730 0
[pid=14027] vsize: 143500
Current children cumulated CPU time (s) 957.11
Current children cumulated vsize (Kb) 145624

[startup+970.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 37408 0 0 0 96470 236 0 0 25 0 1 0 1797016808 148840448 35460 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 36338 35460 145 145 0 36193 0
[pid=14027] vsize: 145352
Current children cumulated CPU time (s) 967.07
Current children cumulated vsize (Kb) 147476

[startup+980.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 37774 0 0 0 97465 238 0 0 25 0 1 0 1797016808 150335488 35826 4294967295 134512640 135094434 3221224432 3221223092 134553487 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 36703 35826 145 145 0 36558 0
[pid=14027] vsize: 146812
Current children cumulated CPU time (s) 977.04
Current children cumulated vsize (Kb) 148936

[startup+990.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 38102 0 0 0 98459 241 0 0 25 0 1 0 1797016808 151674880 36154 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 37030 36154 145 145 0 36885 0
[pid=14027] vsize: 148120
Current children cumulated CPU time (s) 987.01
Current children cumulated vsize (Kb) 150244

[startup+1000.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 38487 0 0 0 99452 244 0 0 25 0 1 0 1797016808 153247744 36539 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 37414 36539 145 145 0 37269 0
[pid=14027] vsize: 149656
Current children cumulated CPU time (s) 996.97
Current children cumulated vsize (Kb) 151780

[startup+1010.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 38794 0 0 0 100447 247 0 0 25 0 1 0 1797016808 154501120 36846 4294967295 134512640 135094434 3221224432 3221223088 134558402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 37720 36846 145 145 0 37575 0
[pid=14027] vsize: 150880
Current children cumulated CPU time (s) 1006.95
Current children cumulated vsize (Kb) 153004

[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 39261 0 0 0 101442 249 0 0 25 0 1 0 1797016808 156409856 37313 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 38186 37313 145 145 0 38041 0
[pid=14027] vsize: 152744
Current children cumulated CPU time (s) 1016.92
Current children cumulated vsize (Kb) 154868

[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 39757 0 0 0 102436 252 0 0 25 0 1 0 1797016808 158437376 37809 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 38681 37809 145 145 0 38536 0
[pid=14027] vsize: 154724
Current children cumulated CPU time (s) 1026.89
Current children cumulated vsize (Kb) 156848

[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 40100 0 0 0 103430 254 0 0 25 0 1 0 1797016808 159838208 38152 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 39023 38152 145 145 0 38878 0
[pid=14027] vsize: 156092
Current children cumulated CPU time (s) 1036.85
Current children cumulated vsize (Kb) 158216

[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 40481 0 0 0 104425 257 0 0 25 0 1 0 1797016808 161394688 38533 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 39403 38533 145 145 0 39258 0
[pid=14027] vsize: 157612
Current children cumulated CPU time (s) 1046.83
Current children cumulated vsize (Kb) 159736

[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 40975 0 0 0 105419 260 0 0 25 0 1 0 1797016808 163414016 39027 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 39896 39027 145 145 0 39751 0
[pid=14027] vsize: 159584
Current children cumulated CPU time (s) 1056.8
Current children cumulated vsize (Kb) 161708

[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 41292 0 0 0 106414 262 0 0 25 0 1 0 1797016808 164716544 39344 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 40214 39344 145 145 0 40069 0
[pid=14027] vsize: 160856
Current children cumulated CPU time (s) 1066.77
Current children cumulated vsize (Kb) 162980

[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 41548 0 0 0 107408 265 0 0 25 0 1 0 1797016808 165765120 39600 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14027/statm): 40470 39600 145 145 0 40325 0
[pid=14027] vsize: 161880
Current children cumulated CPU time (s) 1076.74
Current children cumulated vsize (Kb) 164004

[startup+1090.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 41957 0 0 0 108401 268 0 0 25 0 1 0 1797016808 167428096 40009 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 40876 40009 145 145 0 40731 0
[pid=14027] vsize: 163504
Current children cumulated CPU time (s) 1086.7
Current children cumulated vsize (Kb) 165628

[startup+1100.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 42397 0 0 0 109396 270 0 0 25 0 1 0 1797016808 169226240 40449 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 41315 40449 145 145 0 41170 0
[pid=14027] vsize: 165260
Current children cumulated CPU time (s) 1096.67
Current children cumulated vsize (Kb) 167384

[startup+1110.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 42880 0 0 0 110389 273 0 0 25 0 1 0 1797016808 171204608 40932 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 41798 40932 145 145 0 41653 0
[pid=14027] vsize: 167192
Current children cumulated CPU time (s) 1106.63
Current children cumulated vsize (Kb) 169316

[startup+1120.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 43337 0 0 0 111383 276 0 0 25 0 1 0 1797016808 173072384 41389 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 42254 41389 145 145 0 42109 0
[pid=14027] vsize: 169016
Current children cumulated CPU time (s) 1116.6
Current children cumulated vsize (Kb) 171140

[startup+1130.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 43790 0 0 0 112376 278 0 0 25 0 1 0 1797016808 174923776 41842 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 42706 41842 145 145 0 42561 0
[pid=14027] vsize: 170824
Current children cumulated CPU time (s) 1126.55
Current children cumulated vsize (Kb) 172948

[startup+1140.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 44243 0 0 0 113368 282 0 0 25 0 1 0 1797016808 176775168 42295 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 43158 42295 145 145 0 43013 0
[pid=14027] vsize: 172632
Current children cumulated CPU time (s) 1136.51
Current children cumulated vsize (Kb) 174756

[startup+1150.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 44638 0 0 0 114363 285 0 0 25 0 1 0 1797016808 178388992 42690 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 43552 42690 145 145 0 43407 0
[pid=14027] vsize: 174208
Current children cumulated CPU time (s) 1146.49
Current children cumulated vsize (Kb) 176332

[startup+1160.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 45024 0 0 0 115358 287 0 0 25 0 1 0 1797016808 179965952 43076 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 43937 43076 145 145 0 43792 0
[pid=14027] vsize: 175748
Current children cumulated CPU time (s) 1156.46
Current children cumulated vsize (Kb) 177872

[startup+1170.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 45395 0 0 0 116352 290 0 0 25 0 1 0 1797016808 181481472 43447 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 44307 43447 145 145 0 44162 0
[pid=14027] vsize: 177228
Current children cumulated CPU time (s) 1166.43
Current children cumulated vsize (Kb) 179352

[startup+1180.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 45819 0 0 0 117348 293 0 0 25 0 1 0 1797016808 183214080 43871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 44730 43871 145 145 0 44585 0
[pid=14027] vsize: 178920
Current children cumulated CPU time (s) 1176.42
Current children cumulated vsize (Kb) 181044

[startup+1190.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 46197 0 0 0 118341 296 0 0 25 0 1 0 1797016808 184758272 44249 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 45107 44249 145 145 0 44962 0
[pid=14027] vsize: 180428
Current children cumulated CPU time (s) 1186.38
Current children cumulated vsize (Kb) 182552

[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 46555 0 0 0 119336 297 0 0 25 0 1 0 1797016808 186220544 44607 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 45464 44607 145 145 0 45319 0
[pid=14027] vsize: 181856
Current children cumulated CPU time (s) 1196.34
Current children cumulated vsize (Kb) 183980

[startup+1210.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 46932 0 0 0 120331 300 0 0 25 0 1 0 1797016808 187760640 44984 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 45840 44984 145 145 0 45695 0
[pid=14027] vsize: 183360
Current children cumulated CPU time (s) 1206.32
Current children cumulated vsize (Kb) 185484



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/57 14027
Raw data (/proc/14023/stat): 14023 (minisat+_script) S 14022 14023 22582 0 -1 0 289 239 0 0 0 0 0 1 19 0 1 0 1797016803 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14023/statm): 531 226 485 147 0 384 0
[pid=14023] vsize: 2124
Raw data (/proc/14027/stat): 14027 (minisat+_64-bit) R 14023 14023 22582 0 -1 0 46932 0 0 0 120331 300 0 0 25 0 1 0 1797016808 187760640 44984 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14027/statm): 45840 44984 145 145 0 45695 0
[pid=14027] vsize: 183360
Current children cumulated CPU time (s) 1206.32
Current children cumulated vsize (Kb) 185484

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

Child status: 10
Real time (s): 1210.16
CPU time (s): 1206.4
CPU user time (s): 1203.31
CPU system time (s): 3.08753
CPU usage (%): 99.6897
Max. virtual memory (cumulated for all children) (Kb): 185484

Verifier Data

ERROR: no interpretation found !