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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-sentoy.opb
MD5SUM4df3e7eb358d27d446e34b975724a6c1
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -7772
Optimality of the best value was proved NO
Number of terms in the objective function 60
Biggest coefficient in the objective function 974
Number of bits for the biggest coefficient in the objective function 10
Sum of the numbers in the objective function 9460
Number of bits of the sum of numbers in the objective function 14
Biggest number in a constraint 6000
Number of bits of the biggest number in a constraint 13
Biggest sum of numbers in a constraint 26162
Number of bits of the biggest sum of numbers15
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1227.4
Number of variables60
Total number of constraints90
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)60
Number of constraints which are nor clauses,nor cardinality constraints30
Minimum length of a constraint1
Maximum length of a constraint60

Trace number 3885

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        911308 kB
Buffers:         35324 kB
Cached:          62012 kB
SwapCached:        856 kB
Active:          65320 kB
Inactive:        34656 kB
HighTotal:      131008 kB
HighFree:        67592 kB
LowTotal:       903652 kB
LowFree:        843716 kB
SwapTotal:     2097136 kB
SwapFree:      2095712 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            17892 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:45:55 (client local time) WITH STATUS 10 IN 1208.9 SECONDS
stats: 2884 7 1208.9 10

Solver Data

c Parsing PB file...
c Converting 30 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[  29]---> Adder-cost: 448   maxlim: 11620   bits: 15/14
c ---[  28]---> Adder-cost: 408   maxlim: 6087   bits: 14/13
c ---[  27]---> Adder-cost: 432   maxlim: 9310   bits: 14/14
c ---[  26]---> Adder-cost: 468   maxlim: 11096   bits: 15/14
c ---[  25]---> Adder-cost: 444   maxlim: 10275   bits: 14/14
c ---[  24]---> Adder-cost: 458   maxlim: 10302   bits: 14/14
c ---[  23]---> Adder-cost: 436   maxlim: 13436   bits: 15/14
c ---[  22]---> Adder-cost: 428   maxlim: 9755   bits: 14/14
c ---[  21]---> Adder-cost: 412   maxlim: 6448   bits: 14/13
c ---[  20]---> Adder-cost: 464   maxlim: 10002   bits: 14/14
c ---[  19]---> Adder-cost: 426   maxlim: 9583   bits: 14/14
c ---[  18]---> Adder-cost: 424   maxlim: 9848   bits: 14/14
c ---[  17]---> Adder-cost: 364   maxlim: 5722   bits: 14/13
c ---[  16]---> Adder-cost: 452   maxlim: 10594   bits: 15/14
c ---[  15]---> Adder-cost: 434   maxlim: 10081   bits: 14/14
c ---[  14]---> Adder-cost: 442   maxlim: 9196   bits: 14/14
c ---[  13]---> Adder-cost: 456   maxlim: 12391   bits: 15/14
c ---[  12]---> Adder-cost: 450   maxlim: 14161   bits: 15/14
c ---[  11]---> Adder-cost: 418   maxlim: 12220   bits: 15/14
c ---[  10]---> Adder-cost: 420   maxlim: 12782   bits: 15/14
c ---[   9]---> Adder-cost: 460   maxlim: 11486   bits: 15/14
c ---[   8]---> Adder-cost: 436   maxlim: 8903   bits: 14/14
c ---[   7]---> Adder-cost: 456   maxlim: 10103   bits: 14/14
c ---[   6]---> Adder-cost: 380   maxlim: 6238   bits: 14/13
c ---[   5]---> Adder-cost: 430   maxlim: 10469   bits: 15/14
c ---[   4]---> Adder-cost: 438   maxlim: 9149   bits: 14/14
c ---[   3]---> Adder-cost: 420   maxlim: 13773   bits: 15/14
c ---[   2]---> Adder-cost: 448   maxlim: 9436   bits: 14/14
c ---[   1]---> Adder-cost: 456   maxlim: 8907   bits: 14/14
c ---[   0]---> Adder-cost: 408   maxlim: 13608   bits: 15/14
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   89253   318894 |   29751       0        0     nan |  0.000 % |
c |       100 |   89253   318894 |   32726     100     1024    10.2 |  1.712 % |
c ==============================================================================
c Found solution: -1341
c ---[   0]---> Sorter-cost: 6599     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       191 |  106220   358591 |   35406     191     1682     8.8 |  1.712 % |
c |       291 |  106220   358591 |   38946     291     5111    17.6 |  1.192 % |
c |       443 |  106220   358591 |   42841     443     9280    20.9 |  1.192 % |
c |       669 |  106220   358591 |   47125     669    14719    22.0 |  1.192 % |
c |      1007 |  106214   358574 |   51837    1006    19436    19.3 |  1.197 % |
c ==============================================================================
c Found solution: -1485
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1190 |  106519   359320 |   35506    1189    21596    18.2 |  1.197 % |
c |      1293 |  106519   359320 |   39056    1292    22436    17.4 |  1.191 % |
c |      1445 |  106519   359320 |   42962    1444    24976    17.3 |  1.191 % |
c |      1670 |  106519   359320 |   47258    1669    29751    17.8 |  1.191 % |
c |      2007 |  106519   359320 |   51984    2006    35780    17.8 |  1.191 % |
c ==============================================================================
c Found solution: -1703
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2104 |  106596   359531 |   35532    2103    37022    17.6 |  1.191 % |
c |      2204 |  106596   359531 |   39085    2203    38425    17.4 |  1.194 % |
c |      2357 |  106596   359531 |   42993    2356    40994    17.4 |  1.194 % |
c |      2582 |  106596   359531 |   47293    2581    48161    18.7 |  1.194 % |
c |      2920 |  106596   359531 |   52022    2919    55040    18.9 |  1.194 % |
c ==============================================================================
c Found solution: -2044
c ---[   0]---> Sorter-cost:    8     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3041 |  106710   359836 |   35570    3040    59039    19.4 |  1.194 % |
c |      3141 |  106710   359836 |   39127    3140    59910    19.1 |  1.195 % |
c |      3291 |  106704   359819 |   43039    3289    62063    18.9 |  1.200 % |
c |      3516 |  106704   359819 |   47343    3514    64855    18.5 |  1.200 % |
c ==============================================================================
c Found solution: -2051
c ---[   0]---> Sorter-cost:    3     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3838 |  106709   359842 |   35569    3836    75916    19.8 |  1.200 % |
c |      3938 |  106709   359842 |   39125    3936    77693    19.7 |  1.205 % |
c |      4088 |  106709   359842 |   43038    4086    78884    19.3 |  1.205 % |
c ==============================================================================
c Found solution: -2441
c ---[   0]---> Sorter-cost:    4     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4105 |  106730   359904 |   35576    4103    79182    19.3 |  1.205 % |
c |      4205 |  106730   359904 |   39133    4203    85074    20.2 |  1.209 % |
c |      4356 |  106730   359904 |   43046    4354    87121    20.0 |  1.209 % |
c ==============================================================================
c Found solution: -2545
c ---[   0]---> Sorter-cost:    8     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4437 |  106743   359939 |   35581    4435    91419    20.6 |  1.209 % |
c |      4537 |  106743   359939 |   39139    4535    93846    20.7 |  1.214 % |
c |      4687 |  106743   359939 |   43053    4685    97645    20.8 |  1.214 % |
c |      4912 |  106743   359939 |   47358    4910   102902    21.0 |  1.214 % |
c |      5249 |  106743   359939 |   52094    5247   110257    21.0 |  1.213 % |
c |      5755 |  106743   359939 |   57303    5753   131413    22.8 |  1.214 % |
c |      6514 |  106743   359939 |   63033    6512   170601    26.2 |  1.214 % |
c |      7653 |  106743   359939 |   69337    7651   215921    28.2 |  1.214 % |
c ==============================================================================
c Found solution: -2651
c ---[   0]---> Sorter-cost:    5     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7953 |  106748   359952 |   35582    7951   223593    28.1 |  1.214 % |
c |      8055 |  106748   359952 |   39140    8053   225854    28.0 |  1.218 % |
c |      8205 |  106748   359952 |   43054    8203   228739    27.9 |  1.218 % |
c ==============================================================================
c Found solution: -2952
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      8246 |  106757   359976 |   35585    8244   230421    28.0 |  1.218 % |
c |      8346 |  106757   359976 |   39143    8344   232767    27.9 |  1.223 % |
c |      8496 |  106757   359976 |   43057    8494   236015    27.8 |  1.223 % |
c |      8721 |  106757   359976 |   47363    8719   243030    27.9 |  1.223 % |
c |      9058 |  106757   359976 |   52099    9056   255321    28.2 |  1.223 % |
c |      9566 |  106757   359976 |   57309    9564   270673    28.3 |  1.223 % |
c ==============================================================================
c Found solution: -3309
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9599 |  106798   360082 |   35599    9597   271200    28.3 |  1.223 % |
c |      9699 |  106798   360082 |   39158    9697   276476    28.5 |  1.227 % |
c |      9849 |  106798   360082 |   43074    9847   279294    28.4 |  1.227 % |
c |     10074 |  106798   360082 |   47382   10072   291867    29.0 |  1.227 % |
c |     10412 |  106798   360082 |   52120   10410   298988    28.7 |  1.227 % |
c |     10919 |  106798   360082 |   57332   10917   331053    30.3 |  1.227 % |
c |     11680 |  106792   360065 |   63065   11677   353489    30.3 |  1.232 % |
c |     12819 |  106792   360065 |   69372   12816   416224    32.5 |  1.232 % |
c |     14527 |  106792   360065 |   76309   14524   500281    34.4 |  1.232 % |
c |     17090 |  106786   360048 |   83940   17086   621843    36.4 |  1.237 % |
c |     20934 |  106786   360048 |   92334   20930   766604    36.6 |  1.237 % |
c |     26700 |  106786   360048 |  101568   26696   976667    36.6 |  1.237 % |
c |     35352 |  106786   360048 |  111724   35348  1373187    38.8 |  1.237 % |
c |     48326 |  106786   360048 |  122897   48322  2301426    47.6 |  1.237 % |
c ==============================================================================
c Found solution: -5491
c ---[   0]---> Sorter-cost:    6     Base: 3 2 3 3 5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     49564 |  106852   360209 |   35617   49560  2348470    47.4 |  1.237 % |
c |     49664 |  106852   360209 |   39178   13139   877063    66.8 |  1.239 % |
c |     49815 |  106852   360209 |   43096   13290   878830    66.1 |  1.239 % |
c |     50040 |  106852   360209 |   47406   13515   892196    66.0 |  1.239 % |
c |     50379 |  106852   360209 |   52146   13854   895991    64.7 |  1.239 % |
c |     50887 |  106852   360209 |   57361   14362   901416    62.8 |  1.239 % |
c |     51646 |  106852   360209 |   63097   15121   912500    60.3 |  1.239 % |
c |     52787 |  106852   360209 |   69407   16262   956151    58.8 |  1.239 % |
c |     54495 |  106852   360209 |   76348   17970  1040942    57.9 |  1.239 % |
c |     57057 |  106852   360209 |   83983   20532  1211813    59.0 |  1.239 % |
c |     60902 |  106852   360209 |   92381   24377  1475337    60.5 |  1.239 % |
c |     66669 |  106846   360192 |  101619   30143  1911942    63.4 |  1.245 % |
c |     75319 |  106846   360192 |  111781   38793  2562755    66.1 |  1.245 % |
c |     88295 |  106846   360192 |  122959   51769  3109322    60.1 |  1.245 % |
c |    107756 |  106846   360192 |  135255   71230  4469811    62.8 |  1.245 % |
c |    136950 |  106846   360192 |  148781  100424  6087573    60.6 |  1.245 % |
c |    180739 |  106840   360175 |  163659  144212  8423431    58.4 |  1.250 % |

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/24485/stat): 24485 (minisat+_script) R 24484 24485 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788401250 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/24485/statm): 174 3 169 147 0 27 0
[pid=24485] 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=24486
New process pid=24487
New process pid=24488
execve syscall for /bin/sed executable
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
One traced child (pid=24487) exited with status: 0
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=24488) exited with status: 0
One traced child (pid=24486) exited with status: 0
New process pid=24489
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-20-10-sentoy.opb

[startup+10.0042 s]
Raw data (loadavg): 1.11 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 2438 0 0 0 975 9 0 0 25 0 1 0 1788401255 10928128 2337 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24489/statm): 2668 2337 145 145 0 2523 0
[pid=24489] vsize: 10672
Current children cumulated CPU time (s) 9.86
Current children cumulated vsize (Kb) 12796

[startup+20.006 s]
Raw data (loadavg): 1.10 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 2554 0 0 0 1973 10 0 0 25 0 1 0 1788401255 11403264 2453 4294967295 134512640 135094434 3221224432 3221223056 134557681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 2784 2453 145 145 0 2639 0
[pid=24489] vsize: 11136
Current children cumulated CPU time (s) 19.85
Current children cumulated vsize (Kb) 13260

[startup+30.0069 s]
Raw data (loadavg): 1.08 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 2683 0 0 0 2969 11 0 0 25 0 1 0 1788401255 11935744 2582 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24489/statm): 2914 2582 145 145 0 2769 0
[pid=24489] vsize: 11656
Current children cumulated CPU time (s) 29.82
Current children cumulated vsize (Kb) 13780

[startup+40.0087 s]
Raw data (loadavg): 1.07 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 2793 0 0 0 3968 12 0 0 25 0 1 0 1788401255 12398592 2692 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 3027 2692 145 145 0 2882 0
[pid=24489] vsize: 12108
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 14232

[startup+50.0096 s]
Raw data (loadavg): 1.06 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 2907 0 0 0 4966 13 0 0 25 0 1 0 1788401255 12857344 2806 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 3139 2806 145 145 0 2994 0
[pid=24489] vsize: 12556
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 14680

[startup+60.0104 s]
Raw data (loadavg): 1.05 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3011 0 0 0 5963 15 0 0 25 0 1 0 1788401255 13275136 2910 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 3241 2910 145 145 0 3096 0
[pid=24489] vsize: 12964
Current children cumulated CPU time (s) 59.8
Current children cumulated vsize (Kb) 15088

[startup+70.0112 s]
Raw data (loadavg): 1.04 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3135 0 0 0 6962 15 0 0 25 0 1 0 1788401255 13840384 3034 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 3379 3034 145 145 0 3234 0
[pid=24489] vsize: 13516
Current children cumulated CPU time (s) 69.79
Current children cumulated vsize (Kb) 15640

[startup+80.0121 s]
Raw data (loadavg): 1.03 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3241 0 0 0 7960 16 0 0 25 0 1 0 1788401255 14266368 3140 4294967295 134512640 135094434 3221224432 3221223088 134557934 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 3483 3140 145 145 0 3338 0
[pid=24489] vsize: 13932
Current children cumulated CPU time (s) 79.78
Current children cumulated vsize (Kb) 16056

[startup+90.0129 s]
Raw data (loadavg): 1.03 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3361 0 0 0 8958 17 0 0 25 0 1 0 1788401255 14745600 3260 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 3600 3260 145 145 0 3455 0
[pid=24489] vsize: 14400
Current children cumulated CPU time (s) 89.77
Current children cumulated vsize (Kb) 16524

[startup+100.014 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3486 0 0 0 9956 18 0 0 25 0 1 0 1788401255 15249408 3385 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 3723 3385 145 145 0 3578 0
[pid=24489] vsize: 14892
Current children cumulated CPU time (s) 99.76
Current children cumulated vsize (Kb) 17016

[startup+110.016 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3599 0 0 0 10954 19 0 0 25 0 1 0 1788401255 15699968 3498 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 3833 3498 145 145 0 3688 0
[pid=24489] vsize: 15332
Current children cumulated CPU time (s) 109.75
Current children cumulated vsize (Kb) 17456

[startup+120.017 s]
Raw data (loadavg): 1.02 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3755 0 0 0 11952 20 0 0 25 0 1 0 1788401255 16330752 3654 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 3987 3654 145 145 0 3842 0
[pid=24489] vsize: 15948
Current children cumulated CPU time (s) 119.74
Current children cumulated vsize (Kb) 18072

[startup+130.018 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 3931 0 0 0 12949 22 0 0 25 0 1 0 1788401255 17043456 3830 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 4161 3830 145 145 0 4016 0
[pid=24489] vsize: 16644
Current children cumulated CPU time (s) 129.73
Current children cumulated vsize (Kb) 18768

[startup+140.019 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4093 0 0 0 13946 23 0 0 25 0 1 0 1788401255 17825792 3992 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 4352 3992 145 145 0 4207 0
[pid=24489] vsize: 17408
Current children cumulated CPU time (s) 139.71
Current children cumulated vsize (Kb) 19532

[startup+150.02 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4214 0 0 0 14943 24 0 0 25 0 1 0 1788401255 18313216 4113 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24489/statm): 4471 4113 145 145 0 4326 0
[pid=24489] vsize: 17884
Current children cumulated CPU time (s) 149.69
Current children cumulated vsize (Kb) 20008

[startup+160.022 s]
Raw data (loadavg): 1.01 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4322 0 0 0 15940 26 0 0 25 0 1 0 1788401255 18751488 4221 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 4578 4221 145 145 0 4433 0
[pid=24489] vsize: 18312
Current children cumulated CPU time (s) 159.68
Current children cumulated vsize (Kb) 20436

[startup+170.023 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4485 0 0 0 16937 27 0 0 25 0 1 0 1788401255 19402752 4384 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 4737 4384 145 145 0 4592 0
[pid=24489] vsize: 18948
Current children cumulated CPU time (s) 169.66
Current children cumulated vsize (Kb) 21072

[startup+180.024 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4582 0 0 0 17936 28 0 0 25 0 1 0 1788401255 19795968 4481 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 4833 4481 145 145 0 4688 0
[pid=24489] vsize: 19332
Current children cumulated CPU time (s) 179.66
Current children cumulated vsize (Kb) 21456

[startup+190.025 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4709 0 0 0 18933 30 0 0 25 0 1 0 1788401255 20312064 4608 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 4959 4608 145 145 0 4814 0
[pid=24489] vsize: 19836
Current children cumulated CPU time (s) 189.65
Current children cumulated vsize (Kb) 21960

[startup+200.026 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4835 0 0 0 19931 30 0 0 25 0 1 0 1788401255 20824064 4734 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5084 4734 145 145 0 4939 0
[pid=24489] vsize: 20336
Current children cumulated CPU time (s) 199.63
Current children cumulated vsize (Kb) 22460

[startup+210.027 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 4967 0 0 0 20928 32 0 0 25 0 1 0 1788401255 21356544 4866 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5214 4866 145 145 0 5069 0
[pid=24489] vsize: 20856
Current children cumulated CPU time (s) 209.62
Current children cumulated vsize (Kb) 22980

[startup+220.028 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5097 0 0 0 21926 33 0 0 25 0 1 0 1788401255 21884928 4996 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5343 4996 145 145 0 5198 0
[pid=24489] vsize: 21372
Current children cumulated CPU time (s) 219.61
Current children cumulated vsize (Kb) 23496

[startup+230.029 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5234 0 0 0 22923 34 0 0 25 0 1 0 1788401255 22437888 5133 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5478 5133 145 145 0 5333 0
[pid=24489] vsize: 21912
Current children cumulated CPU time (s) 229.59
Current children cumulated vsize (Kb) 24036

[startup+240.029 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 23923 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0
[pid=24489] vsize: 21944
Current children cumulated CPU time (s) 239.59
Current children cumulated vsize (Kb) 24068

[startup+250.03 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 24924 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0
[pid=24489] vsize: 21944
Current children cumulated CPU time (s) 249.6
Current children cumulated vsize (Kb) 24068

[startup+260.031 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 25924 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0
[pid=24489] vsize: 21944
Current children cumulated CPU time (s) 259.6
Current children cumulated vsize (Kb) 24068

[startup+270.032 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 26924 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0
[pid=24489] vsize: 21944
Current children cumulated CPU time (s) 269.6
Current children cumulated vsize (Kb) 24068

[startup+280.033 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 27924 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223056 134562122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0
[pid=24489] vsize: 21944
Current children cumulated CPU time (s) 279.6
Current children cumulated vsize (Kb) 24068

[startup+290.034 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 28925 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0
[pid=24489] vsize: 21944
Current children cumulated CPU time (s) 289.61
Current children cumulated vsize (Kb) 24068

[startup+300.035 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 29925 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0
[pid=24489] vsize: 21944
Current children cumulated CPU time (s) 299.61
Current children cumulated vsize (Kb) 24068

[startup+310.035 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 30925 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0
[pid=24489] vsize: 21944
Current children cumulated CPU time (s) 309.61
Current children cumulated vsize (Kb) 24068

[startup+320.036 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5242 0 0 0 31925 34 0 0 25 0 1 0 1788401255 22470656 5141 4294967295 134512640 135094434 3221224432 3221223104 134555599 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5486 5141 145 145 0 5341 0
[pid=24489] vsize: 21944
Current children cumulated CPU time (s) 319.61
Current children cumulated vsize (Kb) 24068

[startup+330.037 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5394 0 0 0 32922 35 0 0 25 0 1 0 1788401255 23093248 5293 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5638 5293 145 145 0 5493 0
[pid=24489] vsize: 22552
Current children cumulated CPU time (s) 329.59
Current children cumulated vsize (Kb) 24676

[startup+340.038 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5553 0 0 0 33919 37 0 0 25 0 1 0 1788401255 23752704 5452 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5799 5452 145 145 0 5654 0
[pid=24489] vsize: 23196
Current children cumulated CPU time (s) 339.58
Current children cumulated vsize (Kb) 25320

[startup+350.039 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5679 0 0 0 34916 38 0 0 25 0 1 0 1788401255 24268800 5578 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 5925 5578 145 145 0 5780 0
[pid=24489] vsize: 23700
Current children cumulated CPU time (s) 349.56
Current children cumulated vsize (Kb) 25824

[startup+360.041 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5807 0 0 0 35915 39 0 0 25 0 1 0 1788401255 24801280 5706 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 6055 5706 145 145 0 5910 0
[pid=24489] vsize: 24220
Current children cumulated CPU time (s) 359.56
Current children cumulated vsize (Kb) 26344

[startup+370.041 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 5913 0 0 0 36913 40 0 0 25 0 1 0 1788401255 25235456 5812 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 6161 5812 145 145 0 6016 0
[pid=24489] vsize: 24644
Current children cumulated CPU time (s) 369.55
Current children cumulated vsize (Kb) 26768

[startup+380.042 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6032 0 0 0 37912 40 0 0 25 0 1 0 1788401255 25722880 5931 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 6280 5931 145 145 0 6135 0
[pid=24489] vsize: 25120
Current children cumulated CPU time (s) 379.54
Current children cumulated vsize (Kb) 27244

[startup+390.044 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6154 0 0 0 38909 41 0 0 25 0 1 0 1788401255 26214400 6053 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 6400 6053 145 145 0 6255 0
[pid=24489] vsize: 25600
Current children cumulated CPU time (s) 389.52
Current children cumulated vsize (Kb) 27724

[startup+400.044 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6250 0 0 0 39908 42 0 0 25 0 1 0 1788401255 26611712 6149 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 6497 6149 145 145 0 6352 0
[pid=24489] vsize: 25988
Current children cumulated CPU time (s) 399.52
Current children cumulated vsize (Kb) 28112

[startup+410.045 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6336 0 0 0 40906 42 0 0 25 0 1 0 1788401255 26955776 6235 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 6581 6235 145 145 0 6436 0
[pid=24489] vsize: 26324
Current children cumulated CPU time (s) 409.5
Current children cumulated vsize (Kb) 28448

[startup+420.046 s]
Raw data (loadavg): 1.00 1.00 0.97 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6421 0 0 0 41905 43 0 0 25 0 1 0 1788401255 27299840 6320 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 6665 6320 145 145 0 6520 0
[pid=24489] vsize: 26660
Current children cumulated CPU time (s) 419.5
Current children cumulated vsize (Kb) 28784

[startup+430.046 s]
Raw data (loadavg): 1.07 1.02 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6561 0 0 0 42903 44 0 0 25 0 1 0 1788401255 27865088 6460 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 6803 6460 145 145 0 6658 0
[pid=24489] vsize: 27212
Current children cumulated CPU time (s) 429.49
Current children cumulated vsize (Kb) 29336

[startup+440.047 s]
Raw data (loadavg): 1.06 1.02 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6693 0 0 0 43900 45 0 0 25 0 1 0 1788401255 28401664 6592 4294967295 134512640 135094434 3221224432 3221223088 134558176 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 6934 6592 145 145 0 6789 0
[pid=24489] vsize: 27736
Current children cumulated CPU time (s) 439.47
Current children cumulated vsize (Kb) 29860

[startup+450.048 s]
Raw data (loadavg): 1.05 1.01 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6816 0 0 0 44898 46 0 0 25 0 1 0 1788401255 28897280 6715 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 7055 6715 145 145 0 6910 0
[pid=24489] vsize: 28220
Current children cumulated CPU time (s) 449.46
Current children cumulated vsize (Kb) 30344

[startup+460.049 s]
Raw data (loadavg): 1.04 1.01 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 6927 0 0 0 45896 47 0 0 25 0 1 0 1788401255 29360128 6826 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 7168 6826 145 145 0 7023 0
[pid=24489] vsize: 28672
Current children cumulated CPU time (s) 459.45
Current children cumulated vsize (Kb) 30796

[startup+470.05 s]
Raw data (loadavg): 1.04 1.01 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7052 0 0 0 46893 49 0 0 25 0 1 0 1788401255 29863936 6951 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 7291 6951 145 145 0 7146 0
[pid=24489] vsize: 29164
Current children cumulated CPU time (s) 469.44
Current children cumulated vsize (Kb) 31288

[startup+480.051 s]
Raw data (loadavg): 1.03 1.01 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7166 0 0 0 47891 50 0 0 25 0 1 0 1788401255 30326784 7065 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 7404 7065 145 145 0 7259 0
[pid=24489] vsize: 29616
Current children cumulated CPU time (s) 479.43
Current children cumulated vsize (Kb) 31740

[startup+490.052 s]
Raw data (loadavg): 1.02 1.01 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7310 0 0 0 48889 51 0 0 25 0 1 0 1788401255 31174656 7209 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 7611 7209 145 145 0 7466 0
[pid=24489] vsize: 30444
Current children cumulated CPU time (s) 489.42
Current children cumulated vsize (Kb) 32568

[startup+500.053 s]
Raw data (loadavg): 1.02 1.01 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7436 0 0 0 49886 51 0 0 25 0 1 0 1788401255 31682560 7335 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 7735 7335 145 145 0 7590 0
[pid=24489] vsize: 30940
Current children cumulated CPU time (s) 499.39
Current children cumulated vsize (Kb) 33064

[startup+510.054 s]
Raw data (loadavg): 1.02 1.01 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7538 0 0 0 50884 52 0 0 25 0 1 0 1788401255 32096256 7437 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 7836 7437 145 145 0 7691 0
[pid=24489] vsize: 31344
Current children cumulated CPU time (s) 509.38
Current children cumulated vsize (Kb) 33468

[startup+520.055 s]
Raw data (loadavg): 1.01 1.01 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7613 0 0 0 51883 53 0 0 25 0 1 0 1788401255 32399360 7512 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 7910 7512 145 145 0 7765 0
[pid=24489] vsize: 31640
Current children cumulated CPU time (s) 519.38
Current children cumulated vsize (Kb) 33764

[startup+530.056 s]
Raw data (loadavg): 1.01 1.01 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7698 0 0 0 52881 53 0 0 25 0 1 0 1788401255 32743424 7597 4294967295 134512640 135094434 3221224432 3221223088 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 7994 7597 145 145 0 7849 0
[pid=24489] vsize: 31976
Current children cumulated CPU time (s) 529.36
Current children cumulated vsize (Kb) 34100

[startup+540.057 s]
Raw data (loadavg): 1.01 1.01 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 7840 0 0 0 53879 54 0 0 25 0 1 0 1788401255 33316864 7739 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 8134 7739 145 145 0 7989 0
[pid=24489] vsize: 32536
Current children cumulated CPU time (s) 539.35
Current children cumulated vsize (Kb) 34660

[startup+550.058 s]
Raw data (loadavg): 1.01 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8003 0 0 0 54875 56 0 0 25 0 1 0 1788401255 33984512 7902 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 8297 7902 145 145 0 8152 0
[pid=24489] vsize: 33188
Current children cumulated CPU time (s) 549.33
Current children cumulated vsize (Kb) 35312

[startup+560.058 s]
Raw data (loadavg): 1.01 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8124 0 0 0 55873 57 0 0 25 0 1 0 1788401255 34467840 8023 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 8415 8023 145 145 0 8270 0
[pid=24489] vsize: 33660
Current children cumulated CPU time (s) 559.32
Current children cumulated vsize (Kb) 35784

[startup+570.059 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8203 0 0 0 56872 58 0 0 25 0 1 0 1788401255 34783232 8102 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 8492 8102 145 145 0 8347 0
[pid=24489] vsize: 33968
Current children cumulated CPU time (s) 569.32
Current children cumulated vsize (Kb) 36092

[startup+580.06 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8282 0 0 0 57871 59 0 0 25 0 1 0 1788401255 35115008 8181 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 8573 8181 145 145 0 8428 0
[pid=24489] vsize: 34292
Current children cumulated CPU time (s) 579.32
Current children cumulated vsize (Kb) 36416

[startup+590.061 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8357 0 0 0 58870 59 0 0 25 0 1 0 1788401255 35409920 8256 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 8645 8256 145 145 0 8500 0
[pid=24489] vsize: 34580
Current children cumulated CPU time (s) 589.31
Current children cumulated vsize (Kb) 36704

[startup+600.062 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8433 0 0 0 59868 60 0 0 25 0 1 0 1788401255 35721216 8332 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 8721 8332 145 145 0 8576 0
[pid=24489] vsize: 34884
Current children cumulated CPU time (s) 599.3
Current children cumulated vsize (Kb) 37008

[startup+610.063 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8535 0 0 0 60866 61 0 0 25 0 1 0 1788401255 36134912 8434 4294967295 134512640 135094434 3221224432 3221223088 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 8822 8434 145 145 0 8677 0
[pid=24489] vsize: 35288
Current children cumulated CPU time (s) 609.29
Current children cumulated vsize (Kb) 37412

[startup+620.063 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8635 0 0 0 61865 62 0 0 25 0 1 0 1788401255 36540416 8534 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 8921 8534 145 145 0 8776 0
[pid=24489] vsize: 35684
Current children cumulated CPU time (s) 619.29
Current children cumulated vsize (Kb) 37808

[startup+630.064 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8720 0 0 0 62864 63 0 0 25 0 1 0 1788401255 36888576 8619 4294967295 134512640 135094434 3221224432 3221223088 134558392 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9006 8619 145 145 0 8861 0
[pid=24489] vsize: 36024
Current children cumulated CPU time (s) 629.29
Current children cumulated vsize (Kb) 38148

[startup+640.065 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8817 0 0 0 63862 64 0 0 25 0 1 0 1788401255 37281792 8716 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9102 8716 145 145 0 8957 0
[pid=24489] vsize: 36408
Current children cumulated CPU time (s) 639.28
Current children cumulated vsize (Kb) 38532

[startup+650.066 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8886 0 0 0 64861 64 0 0 25 0 1 0 1788401255 37560320 8785 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9170 8785 145 145 0 9025 0
[pid=24489] vsize: 36680
Current children cumulated CPU time (s) 649.27
Current children cumulated vsize (Kb) 38804

[startup+660.068 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 8953 0 0 0 65860 65 0 0 25 0 1 0 1788401255 37826560 8852 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9235 8852 145 145 0 9090 0
[pid=24489] vsize: 36940
Current children cumulated CPU time (s) 659.27
Current children cumulated vsize (Kb) 39064

[startup+670.069 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9023 0 0 0 66859 66 0 0 25 0 1 0 1788401255 38109184 8922 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9304 8922 145 145 0 9159 0
[pid=24489] vsize: 37216
Current children cumulated CPU time (s) 669.27
Current children cumulated vsize (Kb) 39340

[startup+680.068 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9088 0 0 0 67858 66 0 0 25 0 1 0 1788401255 38371328 8987 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9368 8987 145 145 0 9223 0
[pid=24489] vsize: 37472
Current children cumulated CPU time (s) 679.26
Current children cumulated vsize (Kb) 39596

[startup+690.069 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9162 0 0 0 68857 66 0 0 25 0 1 0 1788401255 38670336 9061 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9441 9061 145 145 0 9296 0
[pid=24489] vsize: 37764
Current children cumulated CPU time (s) 689.25
Current children cumulated vsize (Kb) 39888

[startup+700.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9233 0 0 0 69857 67 0 0 25 0 1 0 1788401255 38957056 9132 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9511 9132 145 145 0 9366 0
[pid=24489] vsize: 38044
Current children cumulated CPU time (s) 699.26
Current children cumulated vsize (Kb) 40168

[startup+710.072 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9309 0 0 0 70856 67 0 0 25 0 1 0 1788401255 39264256 9208 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9586 9208 145 145 0 9441 0
[pid=24489] vsize: 38344
Current children cumulated CPU time (s) 709.25
Current children cumulated vsize (Kb) 40468

[startup+720.073 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9388 0 0 0 71854 68 0 0 25 0 1 0 1788401255 39579648 9287 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9663 9287 145 145 0 9518 0
[pid=24489] vsize: 38652
Current children cumulated CPU time (s) 719.24
Current children cumulated vsize (Kb) 40776

[startup+730.073 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9462 0 0 0 72854 68 0 0 25 0 1 0 1788401255 39886848 9361 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9738 9361 145 145 0 9593 0
[pid=24489] vsize: 38952
Current children cumulated CPU time (s) 729.24
Current children cumulated vsize (Kb) 41076

[startup+740.074 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9529 0 0 0 73853 68 0 0 25 0 1 0 1788401255 40157184 9428 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9804 9428 145 145 0 9659 0
[pid=24489] vsize: 39216
Current children cumulated CPU time (s) 739.23
Current children cumulated vsize (Kb) 41340

[startup+750.075 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9633 0 0 0 74851 69 0 0 25 0 1 0 1788401255 40587264 9532 4294967295 134512640 135094434 3221224432 3221223104 134555274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9909 9532 145 145 0 9764 0
[pid=24489] vsize: 39636
Current children cumulated CPU time (s) 749.22
Current children cumulated vsize (Kb) 41760

[startup+760.076 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9710 0 0 0 75849 70 0 0 25 0 1 0 1788401255 40898560 9609 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 9985 9609 145 145 0 9840 0
[pid=24489] vsize: 39940
Current children cumulated CPU time (s) 759.21
Current children cumulated vsize (Kb) 42064

[startup+770.077 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9802 0 0 0 76847 70 0 0 25 0 1 0 1788401255 41271296 9701 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 10076 9701 145 145 0 9931 0
[pid=24489] vsize: 40304
Current children cumulated CPU time (s) 769.19
Current children cumulated vsize (Kb) 42428

[startup+780.078 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9890 0 0 0 77846 71 0 0 25 0 1 0 1788401255 41627648 9789 4294967295 134512640 135094434 3221224432 3221223024 134556964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 10163 9789 145 145 0 10018 0
[pid=24489] vsize: 40652
Current children cumulated CPU time (s) 779.19
Current children cumulated vsize (Kb) 42776

[startup+790.079 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 9995 0 0 0 78845 72 0 0 25 0 1 0 1788401255 42049536 9894 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 10266 9894 145 145 0 10121 0
[pid=24489] vsize: 41064
Current children cumulated CPU time (s) 789.19
Current children cumulated vsize (Kb) 43188

[startup+800.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10078 0 0 0 79844 72 0 0 25 0 1 0 1788401255 42389504 9977 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 10349 9977 145 145 0 10204 0
[pid=24489] vsize: 41396
Current children cumulated CPU time (s) 799.18
Current children cumulated vsize (Kb) 43520

[startup+810.081 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10219 0 0 0 80842 73 0 0 25 0 1 0 1788401255 42975232 10118 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 10492 10118 145 145 0 10347 0
[pid=24489] vsize: 41968
Current children cumulated CPU time (s) 809.17
Current children cumulated vsize (Kb) 44092

[startup+820.082 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10344 0 0 0 81841 74 0 0 25 0 1 0 1788401255 43479040 10243 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 10615 10243 145 145 0 10470 0
[pid=24489] vsize: 42460
Current children cumulated CPU time (s) 819.17
Current children cumulated vsize (Kb) 44584

[startup+830.083 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10470 0 0 0 82839 74 0 0 25 0 1 0 1788401255 43978752 10369 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 10737 10369 145 145 0 10592 0
[pid=24489] vsize: 42948
Current children cumulated CPU time (s) 829.15
Current children cumulated vsize (Kb) 45072

[startup+840.085 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10610 0 0 0 83837 75 0 0 25 0 1 0 1788401255 44576768 10509 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 10883 10509 145 145 0 10738 0
[pid=24489] vsize: 43532
Current children cumulated CPU time (s) 839.14
Current children cumulated vsize (Kb) 45656

[startup+850.086 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10718 0 0 0 84834 76 0 0 25 0 1 0 1788401255 45019136 10617 4294967295 134512640 135094434 3221224432 3221223088 134557804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 10991 10617 145 145 0 10846 0
[pid=24489] vsize: 43964
Current children cumulated CPU time (s) 849.12
Current children cumulated vsize (Kb) 46088

[startup+860.087 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10825 0 0 0 85833 77 0 0 25 0 1 0 1788401255 45465600 10724 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 11100 10724 145 145 0 10955 0
[pid=24489] vsize: 44400
Current children cumulated CPU time (s) 859.12
Current children cumulated vsize (Kb) 46524

[startup+870.087 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 10918 0 0 0 86831 78 0 0 25 0 1 0 1788401255 45838336 10817 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 11191 10817 145 145 0 11046 0
[pid=24489] vsize: 44764
Current children cumulated CPU time (s) 869.11
Current children cumulated vsize (Kb) 46888

[startup+880.087 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11032 0 0 0 87829 78 0 0 25 0 1 0 1788401255 46297088 10931 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 11303 10931 145 145 0 11158 0
[pid=24489] vsize: 45212
Current children cumulated CPU time (s) 879.09
Current children cumulated vsize (Kb) 47336

[startup+890.088 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11129 0 0 0 88827 79 0 0 25 0 1 0 1788401255 46686208 11028 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 11398 11028 145 145 0 11253 0
[pid=24489] vsize: 45592
Current children cumulated CPU time (s) 889.08
Current children cumulated vsize (Kb) 47716

[startup+900.089 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11230 0 0 0 89826 80 0 0 25 0 1 0 1788401255 47108096 11129 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 11501 11129 145 145 0 11356 0
[pid=24489] vsize: 46004
Current children cumulated CPU time (s) 899.08
Current children cumulated vsize (Kb) 48128

[startup+910.09 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11300 0 0 0 90825 80 0 0 25 0 1 0 1788401255 47403008 11199 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 11573 11199 145 145 0 11428 0
[pid=24489] vsize: 46292
Current children cumulated CPU time (s) 909.07
Current children cumulated vsize (Kb) 48416

[startup+920.091 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11368 0 0 0 91824 81 0 0 25 0 1 0 1788401255 47677440 11267 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 11640 11267 145 145 0 11495 0
[pid=24489] vsize: 46560
Current children cumulated CPU time (s) 919.07
Current children cumulated vsize (Kb) 48684

[startup+930.091 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11448 0 0 0 92822 82 0 0 25 0 1 0 1788401255 47996928 11347 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 11718 11347 145 145 0 11573 0
[pid=24489] vsize: 46872
Current children cumulated CPU time (s) 929.06
Current children cumulated vsize (Kb) 48996

[startup+940.092 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11533 0 0 0 93821 83 0 0 25 0 1 0 1788401255 48873472 11432 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 11932 11432 145 145 0 11787 0
[pid=24489] vsize: 47728
Current children cumulated CPU time (s) 939.06
Current children cumulated vsize (Kb) 49852

[startup+950.093 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11626 0 0 0 94820 83 0 0 25 0 1 0 1788401255 49250304 11525 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12024 11525 145 145 0 11879 0
[pid=24489] vsize: 48096
Current children cumulated CPU time (s) 949.05
Current children cumulated vsize (Kb) 50220

[startup+960.095 s]
Raw data (loadavg): 1.15 1.03 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11721 0 0 0 95818 84 0 0 25 0 1 0 1788401255 49635328 11620 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12118 11620 145 145 0 11973 0
[pid=24489] vsize: 48472
Current children cumulated CPU time (s) 959.04
Current children cumulated vsize (Kb) 50596

[startup+970.096 s]
Raw data (loadavg): 1.13 1.03 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11787 0 0 0 96817 84 0 0 25 0 1 0 1788401255 49897472 11686 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12182 11686 145 145 0 12037 0
[pid=24489] vsize: 48728
Current children cumulated CPU time (s) 969.03
Current children cumulated vsize (Kb) 50852

[startup+980.097 s]
Raw data (loadavg): 1.11 1.03 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11863 0 0 0 97816 85 0 0 25 0 1 0 1788401255 50216960 11762 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12260 11762 145 145 0 12115 0
[pid=24489] vsize: 49040
Current children cumulated CPU time (s) 979.03
Current children cumulated vsize (Kb) 51164

[startup+990.097 s]
Raw data (loadavg): 1.09 1.03 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 11931 0 0 0 98815 85 0 0 25 0 1 0 1788401255 50495488 11830 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12328 11830 145 145 0 12183 0
[pid=24489] vsize: 49312
Current children cumulated CPU time (s) 989.02
Current children cumulated vsize (Kb) 51436

[startup+1000.1 s]
Raw data (loadavg): 1.08 1.03 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12000 0 0 0 99814 86 0 0 25 0 1 0 1788401255 50782208 11899 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12398 11899 145 145 0 12253 0
[pid=24489] vsize: 49592
Current children cumulated CPU time (s) 999.02
Current children cumulated vsize (Kb) 51716

[startup+1010.1 s]
Raw data (loadavg): 1.06 1.03 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12071 0 0 0 100813 87 0 0 25 0 1 0 1788401255 51060736 11970 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12466 11970 145 145 0 12321 0
[pid=24489] vsize: 49864
Current children cumulated CPU time (s) 1009.02
Current children cumulated vsize (Kb) 51988

[startup+1020.1 s]
Raw data (loadavg): 1.05 1.02 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12142 0 0 0 101812 87 0 0 25 0 1 0 1788401255 51347456 12041 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12536 12041 145 145 0 12391 0
[pid=24489] vsize: 50144
Current children cumulated CPU time (s) 1019.01
Current children cumulated vsize (Kb) 52268

[startup+1030.1 s]
Raw data (loadavg): 1.05 1.02 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12206 0 0 0 102812 87 0 0 25 0 1 0 1788401255 51613696 12105 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12601 12105 145 145 0 12456 0
[pid=24489] vsize: 50404
Current children cumulated CPU time (s) 1029.01
Current children cumulated vsize (Kb) 52528

[startup+1040.1 s]
Raw data (loadavg): 1.04 1.02 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12276 0 0 0 103811 88 0 0 25 0 1 0 1788401255 51896320 12175 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12670 12175 145 145 0 12525 0
[pid=24489] vsize: 50680
Current children cumulated CPU time (s) 1039.01
Current children cumulated vsize (Kb) 52804

[startup+1050.1 s]
Raw data (loadavg): 1.03 1.02 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12357 0 0 0 104809 89 0 0 25 0 1 0 1788401255 52228096 12256 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/24489/statm): 12751 12256 145 145 0 12606 0
[pid=24489] vsize: 51004
Current children cumulated CPU time (s) 1049
Current children cumulated vsize (Kb) 53128

[startup+1060.11 s]
Raw data (loadavg): 1.03 1.02 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12436 0 0 0 105807 90 0 0 25 0 1 0 1788401255 52539392 12335 4294967295 134512640 135094434 3221224432 3221223088 134558232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12827 12335 145 145 0 12682 0
[pid=24489] vsize: 51308
Current children cumulated CPU time (s) 1058.99
Current children cumulated vsize (Kb) 53432

[startup+1070.11 s]
Raw data (loadavg): 1.02 1.02 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12533 0 0 0 106805 91 0 0 25 0 1 0 1788401255 52924416 12432 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 12921 12432 145 145 0 12776 0
[pid=24489] vsize: 51684
Current children cumulated CPU time (s) 1068.98
Current children cumulated vsize (Kb) 53808

[startup+1080.11 s]
Raw data (loadavg): 1.02 1.02 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12631 0 0 0 107802 92 0 0 25 0 1 0 1788401255 53342208 12530 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13023 12530 145 145 0 12878 0
[pid=24489] vsize: 52092
Current children cumulated CPU time (s) 1078.96
Current children cumulated vsize (Kb) 54216

[startup+1090.11 s]
Raw data (loadavg): 1.02 1.02 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12708 0 0 0 108801 93 0 0 25 0 1 0 1788401255 53645312 12607 4294967295 134512640 135094434 3221224432 3221223120 134554685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13097 12607 145 145 0 12952 0
[pid=24489] vsize: 52388
Current children cumulated CPU time (s) 1088.96
Current children cumulated vsize (Kb) 54512

[startup+1100.11 s]
Raw data (loadavg): 1.01 1.02 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12787 0 0 0 109800 93 0 0 25 0 1 0 1788401255 53960704 12686 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13174 12686 145 145 0 13029 0
[pid=24489] vsize: 52696
Current children cumulated CPU time (s) 1098.95
Current children cumulated vsize (Kb) 54820

[startup+1110.11 s]
Raw data (loadavg): 1.01 1.02 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12876 0 0 0 110799 94 0 0 25 0 1 0 1788401255 54321152 12775 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13262 12775 145 145 0 13117 0
[pid=24489] vsize: 53048
Current children cumulated CPU time (s) 1108.95
Current children cumulated vsize (Kb) 55172

[startup+1120.11 s]
Raw data (loadavg): 1.01 1.02 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 12968 0 0 0 111797 95 0 0 25 0 1 0 1788401255 54693888 12867 4294967295 134512640 135094434 3221224432 3221223088 134557835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13353 12867 145 145 0 13208 0
[pid=24489] vsize: 53412
Current children cumulated CPU time (s) 1118.94
Current children cumulated vsize (Kb) 55536

[startup+1130.11 s]
Raw data (loadavg): 1.01 1.01 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13056 0 0 0 112795 96 0 0 25 0 1 0 1788401255 55054336 12955 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13441 12955 145 145 0 13296 0
[pid=24489] vsize: 53764
Current children cumulated CPU time (s) 1128.93
Current children cumulated vsize (Kb) 55888

[startup+1140.11 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13131 0 0 0 113793 96 0 0 25 0 1 0 1788401255 55361536 13030 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13516 13030 145 145 0 13371 0
[pid=24489] vsize: 54064
Current children cumulated CPU time (s) 1138.91
Current children cumulated vsize (Kb) 56188

[startup+1150.11 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13227 0 0 0 114792 97 0 0 25 0 1 0 1788401255 55726080 13126 4294967295 134512640 135094434 3221224432 3221223120 134554748 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13605 13126 145 145 0 13460 0
[pid=24489] vsize: 54420
Current children cumulated CPU time (s) 1148.91
Current children cumulated vsize (Kb) 56544

[startup+1160.11 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13302 0 0 0 115791 98 0 0 25 0 1 0 1788401255 56029184 13201 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13679 13201 145 145 0 13534 0
[pid=24489] vsize: 54716
Current children cumulated CPU time (s) 1158.91
Current children cumulated vsize (Kb) 56840

[startup+1170.11 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13383 0 0 0 116790 98 0 0 25 0 1 0 1788401255 56356864 13282 4294967295 134512640 135094434 3221224432 3221223088 134557962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13759 13282 145 145 0 13614 0
[pid=24489] vsize: 55036
Current children cumulated CPU time (s) 1168.9
Current children cumulated vsize (Kb) 57160

[startup+1180.12 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13463 0 0 0 117789 99 0 0 25 0 1 0 1788401255 56684544 13362 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13839 13362 145 145 0 13694 0
[pid=24489] vsize: 55356
Current children cumulated CPU time (s) 1178.9
Current children cumulated vsize (Kb) 57480

[startup+1190.12 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13535 0 0 0 118788 99 0 0 25 0 1 0 1788401255 56975360 13434 4294967295 134512640 135094434 3221224432 3221223088 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13910 13434 145 145 0 13765 0
[pid=24489] vsize: 55640
Current children cumulated CPU time (s) 1188.89
Current children cumulated vsize (Kb) 57764

[startup+1200.12 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13595 0 0 0 119787 100 0 0 25 0 1 0 1788401255 57217024 13494 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 13969 13494 145 145 0 13824 0
[pid=24489] vsize: 55876
Current children cumulated CPU time (s) 1198.89
Current children cumulated vsize (Kb) 58000

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13665 0 0 0 120785 101 0 0 25 0 1 0 1788401255 57507840 13564 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 14040 13564 145 145 0 13895 0
[pid=24489] vsize: 56160
Current children cumulated CPU time (s) 1208.88
Current children cumulated vsize (Kb) 58284



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.12 s]
Raw data (loadavg): 1.00 1.01 0.99 2/57 24489
Raw data (/proc/24485/stat): 24485 (minisat+_script) S 24484 24485 31915 0 -1 0 289 239 0 0 0 1 0 1 22 0 1 0 1788401250 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/24485/statm): 531 226 485 147 0 384 0
[pid=24485] vsize: 2124
Raw data (/proc/24489/stat): 24489 (minisat+_64-bit) R 24485 24485 31915 0 -1 0 13665 0 0 0 120785 101 0 0 25 0 1 0 1788401255 57507840 13564 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/24489/statm): 14040 13564 145 145 0 13895 0
[pid=24489] vsize: 56160
Current children cumulated CPU time (s) 1208.88
Current children cumulated vsize (Kb) 58284

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

Child status: 10
Real time (s): 1210.15
CPU time (s): 1208.9
CPU user time (s): 1207.86
CPU system time (s): 1.04084
CPU usage (%): 99.8968
Max. virtual memory (cumulated for all children) (Kb): 58284

Verifier Data

ERROR: no interpretation found !