Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-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 benchmark1200.68
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 6109

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        911716 kB
Buffers:         14156 kB
Cached:          81072 kB
SwapCached:        516 kB
Active:          24760 kB
Inactive:        72860 kB
HighTotal:      131008 kB
HighFree:        50400 kB
LowTotal:       903652 kB
LowFree:        861316 kB
SwapTotal:     2097892 kB
SwapFree:      2096676 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5664 kB
Slab:            19768 kB
Committed_AS:    64316 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:46:20 (client local time) WITH STATUS 10 IN 1208.83 SECONDS
stats: 3268 7 1208.83 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/6633/stat): 6633 (minisat+_script) R 6632 6633 19316 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855309329 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/6633/statm): 174 3 169 147 0 27 0
[pid=6633] 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=6634
New process pid=6635
New process pid=6636
One traced child (pid=6635) exited with status: 0
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
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=6636) exited with status: 0
One traced child (pid=6634) exited with status: 0
New process pid=6637
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc17/normalized-mps-v2-13-7-sentoy.opb

[startup+10.0032 s]
Raw data (loadavg): 0.93 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 2439 0 0 0 974 10 0 0 25 0 1 0 1855309334 10932224 2338 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 2669 2338 145 145 0 2524 0
[pid=6637] vsize: 10676
Current children cumulated CPU time (s) 9.85
Current children cumulated vsize (Kb) 12800

[startup+20.0038 s]
Raw data (loadavg): 0.94 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 2554 0 0 0 1971 12 0 0 25 0 1 0 1855309334 11403264 2453 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 2784 2453 145 145 0 2639 0
[pid=6637] vsize: 11136
Current children cumulated CPU time (s) 19.84
Current children cumulated vsize (Kb) 13260

[startup+30.0054 s]
Raw data (loadavg): 0.95 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 2683 0 0 0 2969 13 0 0 25 0 1 0 1855309334 11935744 2582 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 2914 2582 145 145 0 2769 0
[pid=6637] vsize: 11656
Current children cumulated CPU time (s) 29.83
Current children cumulated vsize (Kb) 13780

[startup+40.006 s]
Raw data (loadavg): 0.96 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 2792 0 0 0 3967 14 0 0 25 0 1 0 1855309334 12394496 2691 4294967295 134512640 135094434 3221224432 3221223056 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 3026 2691 145 145 0 2881 0
[pid=6637] vsize: 12104
Current children cumulated CPU time (s) 39.82
Current children cumulated vsize (Kb) 14228

[startup+50.0076 s]
Raw data (loadavg): 0.96 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 2906 0 0 0 4964 16 0 0 25 0 1 0 1855309334 12853248 2805 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 3138 2805 145 145 0 2993 0
[pid=6637] vsize: 12552
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 14676

[startup+60.0082 s]
Raw data (loadavg): 0.97 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 3008 0 0 0 5962 17 0 0 25 0 1 0 1855309334 13262848 2907 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 3238 2907 145 145 0 3093 0
[pid=6637] vsize: 12952
Current children cumulated CPU time (s) 59.8
Current children cumulated vsize (Kb) 15076

[startup+70.0088 s]
Raw data (loadavg): 0.97 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 3133 0 0 0 6960 19 0 0 25 0 1 0 1855309334 13832192 3032 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 3377 3032 145 145 0 3232 0
[pid=6637] vsize: 13508
Current children cumulated CPU time (s) 69.8
Current children cumulated vsize (Kb) 15632

[startup+80.0104 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 3239 0 0 0 7958 20 0 0 25 0 1 0 1855309334 14258176 3138 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 3481 3138 145 145 0 3336 0
[pid=6637] vsize: 13924
Current children cumulated CPU time (s) 79.79
Current children cumulated vsize (Kb) 16048

[startup+90.011 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 3357 0 0 0 8955 21 0 0 25 0 1 0 1855309334 14729216 3256 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 3596 3256 145 145 0 3451 0
[pid=6637] vsize: 14384
Current children cumulated CPU time (s) 89.77
Current children cumulated vsize (Kb) 16508

[startup+100.012 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 3482 0 0 0 9952 23 0 0 25 0 1 0 1855309334 15233024 3381 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 3719 3381 145 145 0 3574 0
[pid=6637] vsize: 14876
Current children cumulated CPU time (s) 99.76
Current children cumulated vsize (Kb) 17000

[startup+110.012 s]
Raw data (loadavg): 0.98 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 3594 0 0 0 10951 23 0 0 25 0 1 0 1855309334 15679488 3493 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 3828 3493 145 145 0 3683 0
[pid=6637] vsize: 15312
Current children cumulated CPU time (s) 109.75
Current children cumulated vsize (Kb) 17436

[startup+120.013 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 3752 0 0 0 11946 25 0 0 25 0 1 0 1855309334 16318464 3651 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 3984 3651 145 145 0 3839 0
[pid=6637] vsize: 15936
Current children cumulated CPU time (s) 119.72
Current children cumulated vsize (Kb) 18060

[startup+130.013 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 3927 0 0 0 12942 27 0 0 25 0 1 0 1855309334 17027072 3826 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 4157 3826 145 145 0 4012 0
[pid=6637] vsize: 16628
Current children cumulated CPU time (s) 129.7
Current children cumulated vsize (Kb) 18752

[startup+140.014 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 4091 0 0 0 13939 29 0 0 25 0 1 0 1855309334 17817600 3990 4294967295 134512640 135094434 3221224432 3221223088 134558398 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 4350 3990 145 145 0 4205 0
[pid=6637] vsize: 17400
Current children cumulated CPU time (s) 139.69
Current children cumulated vsize (Kb) 19524

[startup+150.016 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 4214 0 0 0 14937 30 0 0 25 0 1 0 1855309334 18313216 4113 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 4471 4113 145 145 0 4326 0
[pid=6637] vsize: 17884
Current children cumulated CPU time (s) 149.68
Current children cumulated vsize (Kb) 20008

[startup+160.016 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 4324 0 0 0 15936 31 0 0 25 0 1 0 1855309334 18759680 4223 4294967295 134512640 135094434 3221224432 3221223088 134557978 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 4580 4223 145 145 0 4435 0
[pid=6637] vsize: 18320
Current children cumulated CPU time (s) 159.68
Current children cumulated vsize (Kb) 20444

[startup+170.017 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 4487 0 0 0 16933 32 0 0 25 0 1 0 1855309334 19410944 4386 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 4739 4386 145 145 0 4594 0
[pid=6637] vsize: 18956
Current children cumulated CPU time (s) 169.66
Current children cumulated vsize (Kb) 21080

[startup+180.017 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 4584 0 0 0 17931 33 0 0 25 0 1 0 1855309334 19804160 4483 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 4835 4483 145 145 0 4690 0
[pid=6637] vsize: 19340
Current children cumulated CPU time (s) 179.65
Current children cumulated vsize (Kb) 21464

[startup+190.018 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 4713 0 0 0 18930 34 0 0 25 0 1 0 1855309334 20328448 4612 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 4963 4612 145 145 0 4818 0
[pid=6637] vsize: 19852
Current children cumulated CPU time (s) 189.65
Current children cumulated vsize (Kb) 21976

[startup+200.019 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 4841 0 0 0 19927 35 0 0 25 0 1 0 1855309334 20844544 4740 4294967295 134512640 135094434 3221224432 3221223056 134557585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5089 4740 145 145 0 4944 0
[pid=6637] vsize: 20356
Current children cumulated CPU time (s) 199.63
Current children cumulated vsize (Kb) 22480

[startup+210.019 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 4972 0 0 0 20924 36 0 0 25 0 1 0 1855309334 21377024 4871 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5219 4871 145 145 0 5074 0
[pid=6637] vsize: 20876
Current children cumulated CPU time (s) 209.61
Current children cumulated vsize (Kb) 23000

[startup+220.02 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5101 0 0 0 21922 37 0 0 25 0 1 0 1855309334 21901312 5000 4294967295 134512640 135094434 3221224432 3221223056 134557675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5347 5000 145 145 0 5202 0
[pid=6637] vsize: 21388
Current children cumulated CPU time (s) 219.6
Current children cumulated vsize (Kb) 23512

[startup+230.02 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5242 0 0 0 22919 39 0 0 25 0 1 0 1855309334 22470656 5141 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5486 5141 145 145 0 5341 0
[pid=6637] vsize: 21944
Current children cumulated CPU time (s) 229.59
Current children cumulated vsize (Kb) 24068

[startup+240.021 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5242 0 0 0 23919 39 0 0 25 0 1 0 1855309334 22470656 5141 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5486 5141 145 145 0 5341 0
[pid=6637] vsize: 21944
Current children cumulated CPU time (s) 239.59
Current children cumulated vsize (Kb) 24068

[startup+250.022 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5242 0 0 0 24920 39 0 0 25 0 1 0 1855309334 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5486 5141 145 145 0 5341 0
[pid=6637] vsize: 21944
Current children cumulated CPU time (s) 249.6
Current children cumulated vsize (Kb) 24068

[startup+260.022 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5242 0 0 0 25920 39 0 0 25 0 1 0 1855309334 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5486 5141 145 145 0 5341 0
[pid=6637] vsize: 21944
Current children cumulated CPU time (s) 259.6
Current children cumulated vsize (Kb) 24068

[startup+270.023 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5242 0 0 0 26920 39 0 0 25 0 1 0 1855309334 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5486 5141 145 145 0 5341 0
[pid=6637] vsize: 21944
Current children cumulated CPU time (s) 269.6
Current children cumulated vsize (Kb) 24068

[startup+280.023 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5242 0 0 0 27920 39 0 0 25 0 1 0 1855309334 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5486 5141 145 145 0 5341 0
[pid=6637] vsize: 21944
Current children cumulated CPU time (s) 279.6
Current children cumulated vsize (Kb) 24068

[startup+290.024 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5242 0 0 0 28920 39 0 0 25 0 1 0 1855309334 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5486 5141 145 145 0 5341 0
[pid=6637] vsize: 21944
Current children cumulated CPU time (s) 289.6
Current children cumulated vsize (Kb) 24068

[startup+300.025 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5242 0 0 0 29920 39 0 0 25 0 1 0 1855309334 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5486 5141 145 145 0 5341 0
[pid=6637] vsize: 21944
Current children cumulated CPU time (s) 299.6
Current children cumulated vsize (Kb) 24068

[startup+310.025 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5242 0 0 0 30921 39 0 0 25 0 1 0 1855309334 22470656 5141 4294967295 134512640 135094434 3221224432 3221223072 134558048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5486 5141 145 145 0 5341 0
[pid=6637] vsize: 21944
Current children cumulated CPU time (s) 309.61
Current children cumulated vsize (Kb) 24068

[startup+320.026 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5242 0 0 0 31921 39 0 0 25 0 1 0 1855309334 22470656 5141 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5486 5141 145 145 0 5341 0
[pid=6637] vsize: 21944
Current children cumulated CPU time (s) 319.61
Current children cumulated vsize (Kb) 24068

[startup+330.027 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5411 0 0 0 32917 41 0 0 25 0 1 0 1855309334 23166976 5310 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5656 5310 145 145 0 5511 0
[pid=6637] vsize: 22624
Current children cumulated CPU time (s) 329.59
Current children cumulated vsize (Kb) 24748

[startup+340.028 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5561 0 0 0 33916 42 0 0 25 0 1 0 1855309334 23785472 5460 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5807 5460 145 145 0 5662 0
[pid=6637] vsize: 23228
Current children cumulated CPU time (s) 339.59
Current children cumulated vsize (Kb) 25352

[startup+350.029 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5694 0 0 0 34913 44 0 0 25 0 1 0 1855309334 24330240 5593 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 5940 5593 145 145 0 5795 0
[pid=6637] vsize: 23760
Current children cumulated CPU time (s) 349.58
Current children cumulated vsize (Kb) 25884

[startup+360.029 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5821 0 0 0 35910 45 0 0 25 0 1 0 1855309334 24858624 5720 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 6069 5720 145 145 0 5924 0
[pid=6637] vsize: 24276
Current children cumulated CPU time (s) 359.56
Current children cumulated vsize (Kb) 26400

[startup+370.029 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 5928 0 0 0 36908 45 0 0 25 0 1 0 1855309334 25296896 5827 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 6176 5827 145 145 0 6031 0
[pid=6637] vsize: 24704
Current children cumulated CPU time (s) 369.54
Current children cumulated vsize (Kb) 26828

[startup+380.029 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 6044 0 0 0 37906 46 0 0 25 0 1 0 1855309334 25772032 5943 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 6292 5943 145 145 0 6147 0
[pid=6637] vsize: 25168
Current children cumulated CPU time (s) 379.53
Current children cumulated vsize (Kb) 27292

[startup+390.03 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 6168 0 0 0 38904 48 0 0 25 0 1 0 1855309334 26271744 6067 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 6414 6067 145 145 0 6269 0
[pid=6637] vsize: 25656
Current children cumulated CPU time (s) 389.53
Current children cumulated vsize (Kb) 27780

[startup+400.031 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 6264 0 0 0 39902 48 0 0 25 0 1 0 1855309334 26669056 6163 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 6511 6163 145 145 0 6366 0
[pid=6637] vsize: 26044
Current children cumulated CPU time (s) 399.51
Current children cumulated vsize (Kb) 28168

[startup+410.031 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 6347 0 0 0 40901 49 0 0 25 0 1 0 1855309334 27000832 6246 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 6592 6246 145 145 0 6447 0
[pid=6637] vsize: 26368
Current children cumulated CPU time (s) 409.51
Current children cumulated vsize (Kb) 28492

[startup+420.032 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 6437 0 0 0 41899 50 0 0 25 0 1 0 1855309334 27365376 6336 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 6681 6336 145 145 0 6536 0
[pid=6637] vsize: 26724
Current children cumulated CPU time (s) 419.5
Current children cumulated vsize (Kb) 28848

[startup+430.032 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 6578 0 0 0 42897 51 0 0 25 0 1 0 1855309334 27934720 6477 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 6820 6477 145 145 0 6675 0
[pid=6637] vsize: 27280
Current children cumulated CPU time (s) 429.49
Current children cumulated vsize (Kb) 29404

[startup+440.033 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 6716 0 0 0 43895 51 0 0 25 0 1 0 1855309334 28491776 6615 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 6956 6615 145 145 0 6811 0
[pid=6637] vsize: 27824
Current children cumulated CPU time (s) 439.47
Current children cumulated vsize (Kb) 29948

[startup+450.035 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 6837 0 0 0 44893 52 0 0 25 0 1 0 1855309334 28983296 6736 4294967295 134512640 135094434 3221224432 3221223084 134558036 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 7076 6736 145 145 0 6931 0
[pid=6637] vsize: 28304
Current children cumulated CPU time (s) 449.46
Current children cumulated vsize (Kb) 30428

[startup+460.035 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 6950 0 0 0 45890 53 0 0 25 0 1 0 1855309334 29450240 6849 4294967295 134512640 135094434 3221224432 3221223044 134563055 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 7190 6849 145 145 0 7045 0
[pid=6637] vsize: 28760
Current children cumulated CPU time (s) 459.44
Current children cumulated vsize (Kb) 30884

[startup+470.036 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 7074 0 0 0 46886 54 0 0 25 0 1 0 1855309334 29954048 6973 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 7313 6973 145 145 0 7168 0
[pid=6637] vsize: 29252
Current children cumulated CPU time (s) 469.41
Current children cumulated vsize (Kb) 31376

[startup+480.037 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 7191 0 0 0 47884 55 0 0 25 0 1 0 1855309334 30429184 7090 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 7429 7090 145 145 0 7284 0
[pid=6637] vsize: 29716
Current children cumulated CPU time (s) 479.4
Current children cumulated vsize (Kb) 31840

[startup+490.038 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 7332 0 0 0 48882 56 0 0 25 0 1 0 1855309334 31264768 7231 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 7633 7231 145 145 0 7488 0
[pid=6637] vsize: 30532
Current children cumulated CPU time (s) 489.39
Current children cumulated vsize (Kb) 32656

[startup+500.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 7471 0 0 0 49880 57 0 0 25 0 1 0 1855309334 31825920 7370 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 7770 7370 145 145 0 7625 0
[pid=6637] vsize: 31080
Current children cumulated CPU time (s) 499.38
Current children cumulated vsize (Kb) 33204

[startup+510.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 7553 0 0 0 50879 57 0 0 25 0 1 0 1855309334 32157696 7452 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 7851 7452 145 145 0 7706 0
[pid=6637] vsize: 31404
Current children cumulated CPU time (s) 509.37
Current children cumulated vsize (Kb) 33528

[startup+520.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 7628 0 0 0 51878 58 0 0 25 0 1 0 1855309334 32460800 7527 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 7925 7527 145 145 0 7780 0
[pid=6637] vsize: 31700
Current children cumulated CPU time (s) 519.37
Current children cumulated vsize (Kb) 33824

[startup+530.04 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 7716 0 0 0 52877 59 0 0 25 0 1 0 1855309334 32817152 7615 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 8012 7615 145 145 0 7867 0
[pid=6637] vsize: 32048
Current children cumulated CPU time (s) 529.37
Current children cumulated vsize (Kb) 34172

[startup+540.041 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 7868 0 0 0 53873 60 0 0 25 0 1 0 1855309334 33431552 7767 4294967295 134512640 135094434 3221224432 3221223056 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 8162 7767 145 145 0 8017 0
[pid=6637] vsize: 32648
Current children cumulated CPU time (s) 539.34
Current children cumulated vsize (Kb) 34772

[startup+550.042 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8034 0 0 0 54870 61 0 0 25 0 1 0 1855309334 34103296 7933 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 8326 7933 145 145 0 8181 0
[pid=6637] vsize: 33304
Current children cumulated CPU time (s) 549.32
Current children cumulated vsize (Kb) 35428

[startup+560.042 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8143 0 0 0 55868 62 0 0 25 0 1 0 1855309334 34541568 8042 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 8433 8042 145 145 0 8288 0
[pid=6637] vsize: 33732
Current children cumulated CPU time (s) 559.31
Current children cumulated vsize (Kb) 35856

[startup+570.043 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8219 0 0 0 56867 63 0 0 25 0 1 0 1855309334 34848768 8118 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 8508 8118 145 145 0 8363 0
[pid=6637] vsize: 34032
Current children cumulated CPU time (s) 569.31
Current children cumulated vsize (Kb) 36156

[startup+580.043 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8299 0 0 0 57865 65 0 0 25 0 1 0 1855309334 35176448 8198 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 8588 8198 145 145 0 8443 0
[pid=6637] vsize: 34352
Current children cumulated CPU time (s) 579.31
Current children cumulated vsize (Kb) 36476

[startup+590.044 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8376 0 0 0 58863 66 0 0 25 0 1 0 1855309334 35491840 8275 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 8665 8275 145 145 0 8520 0
[pid=6637] vsize: 34660
Current children cumulated CPU time (s) 589.3
Current children cumulated vsize (Kb) 36784

[startup+600.045 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8461 0 0 0 59862 66 0 0 25 0 1 0 1855309334 35840000 8360 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 8750 8360 145 145 0 8605 0
[pid=6637] vsize: 35000
Current children cumulated CPU time (s) 599.29
Current children cumulated vsize (Kb) 37124

[startup+610.045 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8556 0 0 0 60860 68 0 0 25 0 1 0 1855309334 36220928 8455 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 8843 8455 145 145 0 8698 0
[pid=6637] vsize: 35372
Current children cumulated CPU time (s) 609.29
Current children cumulated vsize (Kb) 37496

[startup+620.046 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8656 0 0 0 61858 69 0 0 25 0 1 0 1855309334 36626432 8555 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 8942 8555 145 145 0 8797 0
[pid=6637] vsize: 35768
Current children cumulated CPU time (s) 619.28
Current children cumulated vsize (Kb) 37892

[startup+630.047 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8749 0 0 0 62857 69 0 0 25 0 1 0 1855309334 37007360 8648 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9035 8648 145 145 0 8890 0
[pid=6637] vsize: 36140
Current children cumulated CPU time (s) 629.27
Current children cumulated vsize (Kb) 38264

[startup+640.048 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8836 0 0 0 63855 70 0 0 25 0 1 0 1855309334 37355520 8735 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9120 8735 145 145 0 8975 0
[pid=6637] vsize: 36480
Current children cumulated CPU time (s) 639.26
Current children cumulated vsize (Kb) 38604

[startup+650.05 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8906 0 0 0 64854 71 0 0 25 0 1 0 1855309334 37638144 8805 4294967295 134512640 135094434 3221224432 3221223104 134556552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9189 8805 145 145 0 9044 0
[pid=6637] vsize: 36756
Current children cumulated CPU time (s) 649.26
Current children cumulated vsize (Kb) 38880

[startup+660.05 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 8972 0 0 0 65852 72 0 0 25 0 1 0 1855309334 37904384 8871 4294967295 134512640 135094434 3221224432 3221223024 134556990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9254 8871 145 145 0 9109 0
[pid=6637] vsize: 37016
Current children cumulated CPU time (s) 659.25
Current children cumulated vsize (Kb) 39140

[startup+670.05 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9040 0 0 0 66851 73 0 0 25 0 1 0 1855309334 38178816 8939 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9321 8939 145 145 0 9176 0
[pid=6637] vsize: 37284
Current children cumulated CPU time (s) 669.25
Current children cumulated vsize (Kb) 39408

[startup+680.051 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9109 0 0 0 67849 73 0 0 25 0 1 0 1855309334 38457344 9008 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9389 9008 145 145 0 9244 0
[pid=6637] vsize: 37556
Current children cumulated CPU time (s) 679.23
Current children cumulated vsize (Kb) 39680

[startup+690.052 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9183 0 0 0 68847 75 0 0 25 0 1 0 1855309334 38756352 9082 4294967295 134512640 135094434 3221224432 3221223056 134562057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9462 9082 145 145 0 9317 0
[pid=6637] vsize: 37848
Current children cumulated CPU time (s) 689.23
Current children cumulated vsize (Kb) 39972

[startup+700.053 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9254 0 0 0 69845 76 0 0 25 0 1 0 1855309334 39038976 9153 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9531 9153 145 145 0 9386 0
[pid=6637] vsize: 38124
Current children cumulated CPU time (s) 699.22
Current children cumulated vsize (Kb) 40248

[startup+710.053 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9328 0 0 0 70844 76 0 0 25 0 1 0 1855309334 39337984 9227 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9604 9227 145 145 0 9459 0
[pid=6637] vsize: 38416
Current children cumulated CPU time (s) 709.21
Current children cumulated vsize (Kb) 40540

[startup+720.054 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9407 0 0 0 71843 76 0 0 25 0 1 0 1855309334 39653376 9306 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9681 9306 145 145 0 9536 0
[pid=6637] vsize: 38724
Current children cumulated CPU time (s) 719.2
Current children cumulated vsize (Kb) 40848

[startup+730.054 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9484 0 0 0 72843 76 0 0 25 0 1 0 1855309334 39972864 9383 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9759 9383 145 145 0 9614 0
[pid=6637] vsize: 39036
Current children cumulated CPU time (s) 729.2
Current children cumulated vsize (Kb) 41160

[startup+740.055 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9570 0 0 0 73841 77 0 0 25 0 1 0 1855309334 40325120 9469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 9845 9469 145 145 0 9700 0
[pid=6637] vsize: 39380
Current children cumulated CPU time (s) 739.19
Current children cumulated vsize (Kb) 41504

[startup+750.057 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9658 0 0 0 74840 77 0 0 25 0 1 0 1855309334 40689664 9557 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 9934 9557 145 145 0 9789 0
[pid=6637] vsize: 39736
Current children cumulated CPU time (s) 749.18
Current children cumulated vsize (Kb) 41860

[startup+760.057 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9737 0 0 0 75838 78 0 0 25 0 1 0 1855309334 41009152 9636 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 10012 9636 145 145 0 9867 0
[pid=6637] vsize: 40048
Current children cumulated CPU time (s) 759.17
Current children cumulated vsize (Kb) 42172

[startup+770.058 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9827 0 0 0 76837 79 0 0 25 0 1 0 1855309334 41369600 9726 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 10100 9726 145 145 0 9955 0
[pid=6637] vsize: 40400
Current children cumulated CPU time (s) 769.17
Current children cumulated vsize (Kb) 42524

[startup+780.059 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 9926 0 0 0 77835 80 0 0 25 0 1 0 1855309334 41771008 9825 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 10198 9825 145 145 0 10053 0
[pid=6637] vsize: 40792
Current children cumulated CPU time (s) 779.16
Current children cumulated vsize (Kb) 42916

[startup+790.06 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 10019 0 0 0 78834 81 0 0 25 0 1 0 1855309334 42147840 9918 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 10290 9918 145 145 0 10145 0
[pid=6637] vsize: 41160
Current children cumulated CPU time (s) 789.16
Current children cumulated vsize (Kb) 43284

[startup+800.061 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 10121 0 0 0 79832 82 0 0 25 0 1 0 1855309334 42573824 10020 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 10394 10020 145 145 0 10249 0
[pid=6637] vsize: 41576
Current children cumulated CPU time (s) 799.15
Current children cumulated vsize (Kb) 43700

[startup+810.062 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 10263 0 0 0 80830 83 0 0 25 0 1 0 1855309334 43147264 10162 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 10534 10162 145 145 0 10389 0
[pid=6637] vsize: 42136
Current children cumulated CPU time (s) 809.14
Current children cumulated vsize (Kb) 44260

[startup+820.062 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 10393 0 0 0 81827 84 0 0 25 0 1 0 1855309334 43675648 10292 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 10663 10292 145 145 0 10518 0
[pid=6637] vsize: 42652
Current children cumulated CPU time (s) 819.12
Current children cumulated vsize (Kb) 44776

[startup+830.062 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 10521 0 0 0 82826 84 0 0 25 0 1 0 1855309334 44183552 10420 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 10787 10420 145 145 0 10642 0
[pid=6637] vsize: 43148
Current children cumulated CPU time (s) 829.11
Current children cumulated vsize (Kb) 45272

[startup+840.063 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 10650 0 0 0 83824 85 0 0 25 0 1 0 1855309334 44744704 10549 4294967295 134512640 135094434 3221224432 3221223024 134556812 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 10924 10549 145 145 0 10779 0
[pid=6637] vsize: 43696
Current children cumulated CPU time (s) 839.1
Current children cumulated vsize (Kb) 45820

[startup+850.064 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 10758 0 0 0 84822 86 0 0 25 0 1 0 1855309334 45191168 10657 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 11033 10657 145 145 0 10888 0
[pid=6637] vsize: 44132
Current children cumulated CPU time (s) 849.09
Current children cumulated vsize (Kb) 46256

[startup+860.064 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 10854 0 0 0 85820 87 0 0 25 0 1 0 1855309334 45580288 10753 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 11128 10753 145 145 0 10983 0
[pid=6637] vsize: 44512
Current children cumulated CPU time (s) 859.08
Current children cumulated vsize (Kb) 46636

[startup+870.065 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 10964 0 0 0 86819 88 0 0 25 0 1 0 1855309334 46026752 10863 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 11237 10863 145 145 0 11092 0
[pid=6637] vsize: 44948
Current children cumulated CPU time (s) 869.08
Current children cumulated vsize (Kb) 47072

[startup+880.065 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11067 0 0 0 87817 88 0 0 25 0 1 0 1855309334 46440448 10966 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 11338 10966 145 145 0 11193 0
[pid=6637] vsize: 45352
Current children cumulated CPU time (s) 879.06
Current children cumulated vsize (Kb) 47476

[startup+890.066 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11166 0 0 0 88816 89 0 0 25 0 1 0 1855309334 46833664 11065 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 11434 11065 145 145 0 11289 0
[pid=6637] vsize: 45736
Current children cumulated CPU time (s) 889.06
Current children cumulated vsize (Kb) 47860

[startup+900.067 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11265 0 0 0 89813 90 0 0 25 0 1 0 1855309334 47263744 11164 4294967295 134512640 135094434 3221224432 3221223024 134557213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 11539 11164 145 145 0 11394 0
[pid=6637] vsize: 46156
Current children cumulated CPU time (s) 899.04
Current children cumulated vsize (Kb) 48280

[startup+910.067 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11326 0 0 0 90812 90 0 0 25 0 1 0 1855309334 47509504 11225 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 11599 11225 145 145 0 11454 0
[pid=6637] vsize: 46396
Current children cumulated CPU time (s) 909.03
Current children cumulated vsize (Kb) 48520

[startup+920.068 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11395 0 0 0 91811 91 0 0 25 0 1 0 1855309334 47788032 11294 4294967295 134512640 135094434 3221224432 3221223024 134557429 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 11667 11294 145 145 0 11522 0
[pid=6637] vsize: 46668
Current children cumulated CPU time (s) 919.03
Current children cumulated vsize (Kb) 48792

[startup+930.068 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11482 0 0 0 92809 92 0 0 25 0 1 0 1855309334 48132096 11381 4294967295 134512640 135094434 3221224432 3221223088 134557920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 11751 11381 145 145 0 11606 0
[pid=6637] vsize: 47004
Current children cumulated CPU time (s) 929.02
Current children cumulated vsize (Kb) 49128

[startup+940.069 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11569 0 0 0 93808 92 0 0 25 0 1 0 1855309334 49020928 11468 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 11968 11468 145 145 0 11823 0
[pid=6637] vsize: 47872
Current children cumulated CPU time (s) 939.01
Current children cumulated vsize (Kb) 49996

[startup+950.071 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11663 0 0 0 94806 93 0 0 25 0 1 0 1855309334 49397760 11562 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12060 11562 145 145 0 11915 0
[pid=6637] vsize: 48240
Current children cumulated CPU time (s) 949
Current children cumulated vsize (Kb) 50364

[startup+960.071 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11748 0 0 0 95805 93 0 0 25 0 1 0 1855309334 49741824 11647 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12144 11647 145 145 0 11999 0
[pid=6637] vsize: 48576
Current children cumulated CPU time (s) 958.99
Current children cumulated vsize (Kb) 50700

[startup+970.071 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11817 0 0 0 96804 93 0 0 25 0 1 0 1855309334 50036736 11716 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12216 11716 145 145 0 12071 0
[pid=6637] vsize: 48864
Current children cumulated CPU time (s) 968.98
Current children cumulated vsize (Kb) 50988

[startup+980.071 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11893 0 0 0 97803 94 0 0 25 0 1 0 1855309334 50339840 11792 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12290 11792 145 145 0 12145 0
[pid=6637] vsize: 49160
Current children cumulated CPU time (s) 978.98
Current children cumulated vsize (Kb) 51284

[startup+990.072 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 11958 0 0 0 98801 95 0 0 25 0 1 0 1855309334 50601984 11857 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12354 11857 145 145 0 12209 0
[pid=6637] vsize: 49416
Current children cumulated CPU time (s) 988.97
Current children cumulated vsize (Kb) 51540

[startup+1000.07 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12033 0 0 0 99801 96 0 0 25 0 1 0 1855309334 50909184 11932 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12429 11932 145 145 0 12284 0
[pid=6637] vsize: 49716
Current children cumulated CPU time (s) 998.98
Current children cumulated vsize (Kb) 51840

[startup+1010.07 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12106 0 0 0 100800 96 0 0 25 0 1 0 1855309334 51204096 12005 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12501 12005 145 145 0 12356 0
[pid=6637] vsize: 50004
Current children cumulated CPU time (s) 1008.97
Current children cumulated vsize (Kb) 52128

[startup+1020.07 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12171 0 0 0 101799 97 0 0 25 0 1 0 1855309334 51470336 12070 4294967295 134512640 135094434 3221224432 3221223088 134558238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12566 12070 145 145 0 12421 0
[pid=6637] vsize: 50264
Current children cumulated CPU time (s) 1018.97
Current children cumulated vsize (Kb) 52388

[startup+1030.07 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12235 0 0 0 102797 97 0 0 25 0 1 0 1855309334 51732480 12134 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12630 12134 145 145 0 12485 0
[pid=6637] vsize: 50520
Current children cumulated CPU time (s) 1028.95
Current children cumulated vsize (Kb) 52644

[startup+1040.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12302 0 0 0 103797 97 0 0 25 0 1 0 1855309334 51998720 12201 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12695 12201 145 145 0 12550 0
[pid=6637] vsize: 50780
Current children cumulated CPU time (s) 1038.95
Current children cumulated vsize (Kb) 52904

[startup+1050.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12396 0 0 0 104795 98 0 0 25 0 1 0 1855309334 52379648 12295 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12788 12295 145 145 0 12643 0
[pid=6637] vsize: 51152
Current children cumulated CPU time (s) 1048.94
Current children cumulated vsize (Kb) 53276

[startup+1060.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12479 0 0 0 105793 99 0 0 25 0 1 0 1855309334 52711424 12378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12869 12378 145 145 0 12724 0
[pid=6637] vsize: 51476
Current children cumulated CPU time (s) 1058.93
Current children cumulated vsize (Kb) 53600

[startup+1070.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12574 0 0 0 106792 100 0 0 25 0 1 0 1855309334 53104640 12473 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 12965 12473 145 145 0 12820 0
[pid=6637] vsize: 51860
Current children cumulated CPU time (s) 1068.93
Current children cumulated vsize (Kb) 53984

[startup+1080.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12663 0 0 0 107791 100 0 0 25 0 1 0 1855309334 53469184 12562 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 13054 12562 145 145 0 12909 0
[pid=6637] vsize: 52216
Current children cumulated CPU time (s) 1078.92
Current children cumulated vsize (Kb) 54340

[startup+1090.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12747 0 0 0 108789 101 0 0 25 0 1 0 1855309334 53800960 12646 4294967295 134512640 135094434 3221224432 3221223056 134557705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 13135 12646 145 145 0 12990 0
[pid=6637] vsize: 52540
Current children cumulated CPU time (s) 1088.91
Current children cumulated vsize (Kb) 54664

[startup+1100.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12836 0 0 0 109788 101 0 0 25 0 1 0 1855309334 54161408 12735 4294967295 134512640 135094434 3221224432 3221223088 134558029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 13223 12735 145 145 0 13078 0
[pid=6637] vsize: 52892
Current children cumulated CPU time (s) 1098.9
Current children cumulated vsize (Kb) 55016

[startup+1110.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 12919 0 0 0 110786 102 0 0 25 0 1 0 1855309334 54497280 12818 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 13305 12818 145 145 0 13160 0
[pid=6637] vsize: 53220
Current children cumulated CPU time (s) 1108.89
Current children cumulated vsize (Kb) 55344

[startup+1120.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 13013 0 0 0 111784 103 0 0 25 0 1 0 1855309334 54874112 12912 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 13397 12912 145 145 0 13252 0
[pid=6637] vsize: 53588
Current children cumulated CPU time (s) 1118.88
Current children cumulated vsize (Kb) 55712

[startup+1130.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 13091 0 0 0 112783 104 0 0 25 0 1 0 1855309334 55197696 12990 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 13476 12990 145 145 0 13331 0
[pid=6637] vsize: 53904
Current children cumulated CPU time (s) 1128.88
Current children cumulated vsize (Kb) 56028

[startup+1140.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 13179 0 0 0 113780 105 0 0 25 0 1 0 1855309334 55533568 13078 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 13558 13078 145 145 0 13413 0
[pid=6637] vsize: 54232
Current children cumulated CPU time (s) 1138.86
Current children cumulated vsize (Kb) 56356

[startup+1150.08 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 13259 0 0 0 114778 106 0 0 25 0 1 0 1855309334 55857152 13158 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 13637 13158 145 145 0 13492 0
[pid=6637] vsize: 54548
Current children cumulated CPU time (s) 1148.85
Current children cumulated vsize (Kb) 56672

[startup+1160.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 13340 0 0 0 115776 107 0 0 25 0 1 0 1855309334 56184832 13239 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 13717 13239 145 145 0 13572 0
[pid=6637] vsize: 54868
Current children cumulated CPU time (s) 1158.84
Current children cumulated vsize (Kb) 56992

[startup+1170.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 13419 0 0 0 116774 108 0 0 25 0 1 0 1855309334 56504320 13318 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/6637/statm): 13795 13318 145 145 0 13650 0
[pid=6637] vsize: 55180
Current children cumulated CPU time (s) 1168.83
Current children cumulated vsize (Kb) 57304

[startup+1180.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 13493 0 0 0 117773 109 0 0 25 0 1 0 1855309334 56811520 13392 4294967295 134512640 135094434 3221224432 3221223088 134558246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 13870 13392 145 145 0 13725 0
[pid=6637] vsize: 55480
Current children cumulated CPU time (s) 1178.83
Current children cumulated vsize (Kb) 57604

[startup+1190.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 13564 0 0 0 118771 110 0 0 25 0 1 0 1855309334 57094144 13463 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 13939 13463 145 145 0 13794 0
[pid=6637] vsize: 55756
Current children cumulated CPU time (s) 1188.82
Current children cumulated vsize (Kb) 57880

[startup+1200.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 13628 0 0 0 119769 111 0 0 25 0 1 0 1855309334 57360384 13527 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 14004 13527 145 145 0 13859 0
[pid=6637] vsize: 56016
Current children cumulated CPU time (s) 1198.81
Current children cumulated vsize (Kb) 58140

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 13694 0 0 0 120768 111 0 0 25 0 1 0 1855309334 57626624 13593 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 14069 13593 145 145 0 13924 0
[pid=6637] vsize: 56276
Current children cumulated CPU time (s) 1208.8
Current children cumulated vsize (Kb) 58400



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 0.99 0.98 0.97 2/57 6637
Raw data (/proc/6633/stat): 6633 (minisat+_script) S 6632 6633 19316 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855309329 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/6633/statm): 531 226 485 147 0 384 0
[pid=6633] vsize: 2124
Raw data (/proc/6637/stat): 6637 (minisat+_64-bit) R 6633 6633 19316 0 -1 0 13694 0 0 0 120768 111 0 0 25 0 1 0 1855309334 57626624 13593 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/6637/statm): 14069 13593 145 145 0 13924 0
[pid=6637] vsize: 56276
Current children cumulated CPU time (s) 1208.8
Current children cumulated vsize (Kb) 58400

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

Child status: 10
Real time (s): 1210.12
CPU time (s): 1208.83
CPU user time (s): 1207.69
CPU system time (s): 1.14283
CPU usage (%): 99.8934
Max. virtual memory (cumulated for all children) (Kb): 58400

Verifier Data

ERROR: no interpretation found !