Some explanations

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

General information on the benchmark

Nameweb/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-1.opb
MD5SUM16a8eb66aae2bcfd534a482dd0a3948e
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -30
Optimality of the best value was proved NO
Number of terms in the objective function 595
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 595
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 595
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.03
Number of variables595
Total number of constraints27856
Number of constraints which are clauses27856
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint2

Trace number 2284

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        928432 kB
Buffers:         34360 kB
Cached:          45500 kB
SwapCached:        856 kB
Active:          63816 kB
Inactive:        18712 kB
HighTotal:      131008 kB
HighFree:        84028 kB
LowTotal:       903652 kB
LowFree:        844404 kB
SwapTotal:     2097136 kB
SwapFree:      2095712 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            18036 kB
Committed_AS:    72360 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:58:12 (client local time) WITH STATUS 10 IN 1209.73 SECONDS
stats: 2690 7 1209.73 10

Solver Data

c Parsing PB file...
c Converting 27856 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27856    55712 |    9285       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -25
c ---[   0]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   56151   122167 |   18717       0        0     nan |  0.000 % |
c |       100 |   55641   121103 |   20588      80     1297    16.2 |  1.436 % |
c |       250 |   54951   119605 |   22647     189     2268    12.0 |  3.524 % |
c |       476 |   54022   117586 |   24912     364     4235    11.6 |  6.330 % |
c |       813 |   52202   113569 |   27403     615     7046    11.5 | 11.983 % |
c |      1319 |   50454   109647 |   30143    1040    11817    11.4 | 17.600 % |
c ==============================================================================
c Found solution: -26
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1402 |   50068   108787 |   16689    1107    12820    11.6 | 17.600 % |
c |      1502 |   49454   107371 |   18357    1174    13840    11.8 | 21.069 % |
c |      1652 |   48818   105945 |   20193    1300    15532    11.9 | 22.940 % |
c |      1877 |   48058   104211 |   22213    1452    17303    11.9 | 25.446 % |
c |      2214 |   47050   101919 |   24434    1732    20313    11.7 | 28.742 % |
c |      2720 |   45617    98616 |   26877    2151    25789    12.0 | 33.547 % |
c |      3479 |   43899    94657 |   29565    2788    35155    12.6 | 39.272 % |
c |      4618 |   40020    85547 |   32522    3583    49056    13.7 | 52.286 % |
c ==============================================================================
c Found solution: -27
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4643 |   40055    85703 |   13351    3591    49288    13.7 | 52.286 % |
c |      4745 |   39723    84935 |   14686    3575    49232    13.8 | 53.493 % |
c |      4895 |   39621    84699 |   16154    3698    51856    14.0 | 53.838 % |
c |      5120 |   39179    83659 |   17770    3874    56863    14.7 | 55.355 % |
c |      5457 |   37944    80743 |   19547    4038    60606    15.0 | 59.650 % |
c |      5963 |   37234    79072 |   21501    4463    73988    16.6 | 62.099 % |
c ==============================================================================
c Found solution: -28
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6315 |   37042    78587 |   12347    4760    82824    17.4 | 62.099 % |
c |      6415 |   36898    78246 |   13581    4847    84510    17.4 | 63.317 % |
c |      6566 |   36429    77135 |   14939    4926    88695    18.0 | 64.927 % |
c |      6791 |   36313    76855 |   16433    5126    95703    18.7 | 65.343 % |
c |      7128 |   35730    75480 |   18077    5353   100982    18.9 | 67.308 % |
c |      7634 |   35222    74253 |   19884    5765   125403    21.8 | 69.093 % |
c |      8393 |   34627    72820 |   21873    6399   144024    22.5 | 71.186 % |
c ==============================================================================
c Found solution: -29
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9306 |   34209    71811 |   11403    7189   178763    24.9 | 71.186 % |
c |      9407 |   34209    71811 |   12543    7290   180868    24.8 | 72.783 % |
c |      9557 |   34129    71619 |   13797    7379   182136    24.7 | 73.065 % |
c |      9783 |   34089    71525 |   15177    7572   191361    25.3 | 73.204 % |
c |     10120 |   34089    71525 |   16695    7909   209404    26.5 | 73.204 % |
c |     10626 |   34043    71415 |   18364    8361   232830    27.8 | 73.363 % |
c |     11385 |   33962    71214 |   20201    9085   269116    29.6 | 73.666 % |
c |     12525 |   33255    69528 |   22221    9902   298057    30.1 | 76.137 % |
c |     14233 |   32889    68642 |   24443   11283   385731    34.2 | 77.457 % |
c |     16795 |   32768    68345 |   26887   13632   659300    48.4 | 77.888 % |
c ==============================================================================
c Found solution: -30
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17157 |   32647    68009 |   10882   13954   681985    48.9 | 77.888 % |
c |     17258 |   32641    67993 |   11970   14049   684582    48.7 | 78.347 % |
c |     17408 |   32641    67993 |   13167   14199   690091    48.6 | 78.347 % |
c |     17634 |   32588    67867 |   14483   14349   701963    48.9 | 78.532 % |
c |     17971 |   32555    67786 |   15932   14650   714775    48.8 | 78.655 % |
c |     18477 |   32411    67425 |   17525   15034   729230    48.5 | 79.195 % |
c |     19237 |   32367    67321 |   19278   15759   758129    48.1 | 79.349 % |
c |     20376 |   32301    67168 |   21205   16840   848616    50.4 | 79.544 % |
c |     22085 |   32218    66973 |   23326   18501   944250    51.0 | 79.832 % |
c |     24647 |   32151    66816 |   25659   21011  1154613    55.0 | 80.063 % |
c ==============================================================================
c Found solution: -31
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27056 |   32115    66734 |   10705   23335  1321535    56.6 | 80.063 % |
c |     27157 |   32113    66730 |   11775   23435  1326791    56.6 | 80.316 % |
c |     27308 |   32113    66730 |   12953   23586  1331776    56.5 | 80.316 % |
c |     27533 |   32071    66627 |   14248   23711  1346197    56.8 | 80.470 % |
c |     27871 |   32034    66544 |   15673   23983  1360153    56.7 | 80.587 % |
c |     28377 |   31959    66360 |   17240   24473  1380446    56.4 | 80.868 % |
c |     29136 |   31866    66137 |   18964   25210  1423417    56.5 | 81.191 % |
c |     30275 |   31832    66053 |   20861   26274  1496718    57.0 | 81.313 % |
c |     31983 |   31832    66053 |   22947   27982  1622123    58.0 | 81.313 % |
c |     34545 |   31805    65984 |   25241   30493  1805024    59.2 | 81.416 % |
c |     38389 |   31766    65891 |   27766   34166  2010912    58.9 | 81.554 % |
c |     44157 |   31719    65774 |   30542   39804  2430835    61.1 | 81.733 % |
c |     52806 |   31615    65520 |   33596   18059   877920    48.6 | 82.106 % |
c ==============================================================================
c Found solution: -32
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62973 |   31532    65307 |   10510   28208  1448576    51.4 | 82.106 % |
c |     63076 |   31532    65307 |   11561   14207   578195    40.7 | 82.410 % |
c |     63226 |   31532    65307 |   12717   14357   585145    40.8 | 82.410 % |
c |     63451 |   31532    65307 |   13988   14582   598581    41.0 | 82.410 % |
c |     63788 |   31532    65307 |   15387   14919   620951    41.6 | 82.410 % |
c |     64294 |   31532    65307 |   16926   15425   653206    42.3 | 82.410 % |
c |     65053 |   31464    65147 |   18619   16165   701648    43.4 | 82.634 % |
c |     66192 |   31419    65036 |   20481   17286   776803    44.9 | 82.803 % |
c |     67901 |   31419    65036 |   22529   18995   879887    46.3 | 82.803 % |
c |     70463 |   31402    64997 |   24782   21553   994708    46.2 | 82.860 % |
c |     74308 |   31402    64997 |   27260   25398  1201104    47.3 | 82.859 % |
c |     80074 |   31402    64997 |   29986   31164  1386011    44.5 | 82.860 % |
c |     88723 |   31378    64935 |   32984   39808  1664419    41.8 | 82.957 % |
c |    101698 |   31329    64818 |   36283   20738   615428    29.7 | 83.131 % |
c |    121159 |   31329    64818 |   39911   40199  1368273    34.0 | 83.131 % |
c |    150352 |   31266    64657 |   43902   30887   952875    30.9 | 83.376 % |
c |    194141 |   31229    64565 |   48293   31138  1004370    32.3 | 83.514 % |
c ==============================================================================
c Found solution: -33
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    217392 |   31241    64598 |   10413   54386  1860959    34.2 | 83.514 % |
c |    217494 |   31241    64598 |   11454   17566   456371    26.0 | 83.495 % |
c |    217644 |   31241    64598 |   12599   17716   463136    26.1 | 83.495 % |
c |    217869 |   31241    64598 |   13859   17941   471453    26.3 | 83.495 % |
c |    218206 |   31241    64598 |   15245   18278   487008    26.6 | 83.495 % |
c |    218712 |   31241    64598 |   16770   18784   502493    26.8 | 83.495 % |
c |    219471 |   31241    64598 |   18447   19543   525927    26.9 | 83.495 % |
c |    220610 |   31241    64598 |   20291   20682   558029    27.0 | 83.495 % |
c |    222318 |   31241    64598 |   22321   22390   603953    27.0 | 83.495 % |
c |    224880 |   31241    64598 |   24553   24952   673524    27.0 | 83.495 % |
c |    228724 |   31227    64566 |   27008   28790   773486    26.9 | 83.541 % |
c |    234490 |   31207    64514 |   29709   34403   940104    27.3 | 83.623 % |
c |    243140 |   31207    64514 |   32680   43053  1183495    27.5 | 83.623 % |
c |    256114 |   31207    64514 |   35948   24367   575570    23.6 | 83.623 % |
c |    275576 |   31168    64425 |   39543   43805  1874953    42.8 | 83.750 % |
c |    304768 |   31161    64408 |   43497   33136  1335594    40.3 | 83.776 % |
c |    348558 |   31153    64388 |   47847   36328   955951    26.3 | 83.807 % |
c |    414243 |   31122    64317 |   52632   58263  1623043    27.9 | 83.904 % |
c |    512769 |   31083    64216 |   57895   59889  2165270    36.2 | 84.047 % |
c ==============================================================================
c Found solution: -34
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    614887 |   31011    64017 |   10337   52804  1656316    31.4 | 84.047 % |
c |    614988 |   31011    64017 |   11370   21171   575638    27.2 | 84.304 % |
c |    615139 |   31011    64017 |   12507   21322   578882    27.1 | 84.304 % |
c |    615365 |   31011    64017 |   13758   21548   583379    27.1 | 84.304 % |
c |    615703 |   31011    64017 |   15134   21886   590624    27.0 | 84.304 % |
c |    616209 |   31011    64017 |   16647   22392   603214    26.9 | 84.304 % |
c |    616969 |   31011    64017 |   18312   23152   624588    27.0 | 84.304 % |
c |    618110 |   31011    64017 |   20143   24293   653811    26.9 | 84.304 % |
c |    619819 |   31011    64017 |   22158   26002   714382    27.5 | 84.304 % |
c |    622381 |   30983    63957 |   24374   28562   777468    27.2 | 84.385 % |
c |    626226 |   30983    63957 |   26811   32407   890463    27.5 | 84.385 % |
c |    631992 |   30983    63957 |   29492   38173  1062628    27.8 | 84.385 % |

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/19958/stat): 19958 (minisat+_script) R 19957 19958 31915 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785234476 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/19958/statm): 174 3 169 147 0 27 0
[pid=19958] 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=19959
New process pid=19960
New process pid=19961
execve syscall for /bin/sed executable
One traced child (pid=19960) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=19961) exited with status: 0
One traced child (pid=19959) exited with status: 0
New process pid=19962
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc3/normalized-frb35-17-1.opb

[startup+10.0035 s]
Raw data (loadavg): 0.92 0.94 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 2154 0 0 0 980 8 0 0 25 0 1 0 1785234481 9760768 2141 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19962/statm): 2383 2141 145 145 0 2238 0
[pid=19962] vsize: 9532
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 11656

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.94 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 2225 0 0 0 1979 9 0 0 25 0 1 0 1785234481 10059776 2212 4294967295 134512640 135094434 3221224448 3221223108 134553501 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19962/statm): 2456 2212 145 145 0 2311 0
[pid=19962] vsize: 9824
Current children cumulated CPU time (s) 19.88
Current children cumulated vsize (Kb) 11948

[startup+30.0062 s]
Raw data (loadavg): 0.94 0.94 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 2744 0 0 0 2970 13 0 0 25 0 1 0 1785234481 12177408 2731 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19962/statm): 2973 2731 145 145 0 2828 0
[pid=19962] vsize: 11892
Current children cumulated CPU time (s) 29.83
Current children cumulated vsize (Kb) 14016

[startup+40.008 s]
Raw data (loadavg): 0.95 0.94 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 3289 0 0 0 3961 16 0 0 25 0 1 0 1785234481 14450688 3276 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19962/statm): 3528 3276 145 145 0 3383 0
[pid=19962] vsize: 14112
Current children cumulated CPU time (s) 39.77
Current children cumulated vsize (Kb) 16236

[startup+50.0089 s]
Raw data (loadavg): 0.96 0.94 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 3784 0 0 0 4950 23 0 0 25 0 1 0 1785234481 16453632 3771 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19962/statm): 4017 3771 145 145 0 3872 0
[pid=19962] vsize: 16068
Current children cumulated CPU time (s) 49.73
Current children cumulated vsize (Kb) 18192

[startup+60.0097 s]
Raw data (loadavg): 0.97 0.94 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 4228 0 0 0 5941 26 0 0 25 0 1 0 1785234481 18247680 4215 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 4455 4215 145 145 0 4310 0
[pid=19962] vsize: 17820
Current children cumulated CPU time (s) 59.67
Current children cumulated vsize (Kb) 19944

[startup+70.0125 s]
Raw data (loadavg): 0.97 0.95 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 4604 0 0 0 6934 29 0 0 25 0 1 0 1785234481 19902464 4591 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19962/statm): 4859 4591 145 145 0 4714 0
[pid=19962] vsize: 19436
Current children cumulated CPU time (s) 69.63
Current children cumulated vsize (Kb) 21560

[startup+80.0133 s]
Raw data (loadavg): 0.97 0.95 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5011 0 0 0 7926 34 0 0 25 0 1 0 1785234481 21549056 4998 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5261 4998 145 145 0 5116 0
[pid=19962] vsize: 21044
Current children cumulated CPU time (s) 79.6
Current children cumulated vsize (Kb) 23168

[startup+90.0142 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5341 0 0 0 8920 36 0 0 25 0 1 0 1785234481 22884352 5328 4294967295 134512640 135094434 3221224448 3221223072 134562152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5587 5328 145 145 0 5442 0
[pid=19962] vsize: 22348
Current children cumulated CPU time (s) 89.56
Current children cumulated vsize (Kb) 24472

[startup+100.015 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5498 0 0 0 9917 37 0 0 25 0 1 0 1785234481 23515136 5485 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5741 5485 145 145 0 5596 0
[pid=19962] vsize: 22964
Current children cumulated CPU time (s) 99.54
Current children cumulated vsize (Kb) 25088

[startup+110.016 s]
Raw data (loadavg): 0.98 0.95 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5498 0 0 0 10917 37 0 0 25 0 1 0 1785234481 23515136 5485 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5741 5485 145 145 0 5596 0
[pid=19962] vsize: 22964
Current children cumulated CPU time (s) 109.54
Current children cumulated vsize (Kb) 25088

[startup+120.018 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5518 0 0 0 11917 37 0 0 25 0 1 0 1785234481 23674880 5505 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5505 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 119.54
Current children cumulated vsize (Kb) 25244

[startup+130.019 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5518 0 0 0 12918 37 0 0 25 0 1 0 1785234481 23674880 5505 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5505 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 129.55
Current children cumulated vsize (Kb) 25244

[startup+140.019 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5518 0 0 0 13918 37 0 0 25 0 1 0 1785234481 23674880 5505 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5505 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 139.55
Current children cumulated vsize (Kb) 25244

[startup+150.02 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5518 0 0 0 14918 37 0 0 25 0 1 0 1785234481 23674880 5505 4294967295 134512640 135094434 3221224448 3221223072 134557636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5505 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 149.55
Current children cumulated vsize (Kb) 25244

[startup+160.021 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5518 0 0 0 15918 37 0 0 25 0 1 0 1785234481 23674880 5505 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5505 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 159.55
Current children cumulated vsize (Kb) 25244

[startup+170.022 s]
Raw data (loadavg): 0.99 0.95 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5518 0 0 0 16919 37 0 0 25 0 1 0 1785234481 23674880 5505 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5505 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 169.56
Current children cumulated vsize (Kb) 25244

[startup+180.023 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5519 0 0 0 17919 37 0 0 25 0 1 0 1785234481 23674880 5506 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5506 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 179.56
Current children cumulated vsize (Kb) 25244

[startup+190.025 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5519 0 0 0 18919 37 0 0 25 0 1 0 1785234481 23674880 5506 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5506 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 189.56
Current children cumulated vsize (Kb) 25244

[startup+200.025 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5519 0 0 0 19919 37 0 0 25 0 1 0 1785234481 23674880 5506 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5506 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 199.56
Current children cumulated vsize (Kb) 25244

[startup+210.026 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5519 0 0 0 20920 37 0 0 25 0 1 0 1785234481 23674880 5506 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5506 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 209.57
Current children cumulated vsize (Kb) 25244

[startup+220.028 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5519 0 0 0 21920 37 0 0 25 0 1 0 1785234481 23674880 5506 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5506 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 219.57
Current children cumulated vsize (Kb) 25244

[startup+230.029 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5519 0 0 0 22920 37 0 0 25 0 1 0 1785234481 23674880 5506 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5506 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 229.57
Current children cumulated vsize (Kb) 25244

[startup+240.031 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5520 0 0 0 23920 37 0 0 25 0 1 0 1785234481 23674880 5507 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5507 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 239.57
Current children cumulated vsize (Kb) 25244

[startup+250.032 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5525 0 0 0 24921 37 0 0 25 0 1 0 1785234481 23674880 5512 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5512 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 249.58
Current children cumulated vsize (Kb) 25244

[startup+260.032 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5526 0 0 0 25921 37 0 0 25 0 1 0 1785234481 23674880 5513 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5513 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 259.58
Current children cumulated vsize (Kb) 25244

[startup+270.033 s]
Raw data (loadavg): 0.99 0.96 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5526 0 0 0 26921 37 0 0 25 0 1 0 1785234481 23674880 5513 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5513 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 269.58
Current children cumulated vsize (Kb) 25244

[startup+280.034 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5526 0 0 0 27921 37 0 0 25 0 1 0 1785234481 23674880 5513 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5513 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 279.58
Current children cumulated vsize (Kb) 25244

[startup+290.036 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5526 0 0 0 28922 37 0 0 25 0 1 0 1785234481 23674880 5513 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5513 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 289.59
Current children cumulated vsize (Kb) 25244

[startup+300.037 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5526 0 0 0 29922 37 0 0 25 0 1 0 1785234481 23674880 5513 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5513 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 299.59
Current children cumulated vsize (Kb) 25244

[startup+310.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5526 0 0 0 30922 37 0 0 25 0 1 0 1785234481 23674880 5513 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5780 5513 145 145 0 5635 0
[pid=19962] vsize: 23120
Current children cumulated CPU time (s) 309.59
Current children cumulated vsize (Kb) 25244

[startup+320.038 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5550 0 0 0 31922 38 0 0 25 0 1 0 1785234481 23801856 5537 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5811 5537 145 145 0 5666 0
[pid=19962] vsize: 23244
Current children cumulated CPU time (s) 319.6
Current children cumulated vsize (Kb) 25368

[startup+330.039 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5553 0 0 0 32922 38 0 0 25 0 1 0 1785234481 23932928 5540 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5540 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 329.6
Current children cumulated vsize (Kb) 25496

[startup+340.041 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 33923 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 339.61
Current children cumulated vsize (Kb) 25496

[startup+350.042 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 34923 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 349.61
Current children cumulated vsize (Kb) 25496

[startup+360.043 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 35923 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223040 134557202 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 359.61
Current children cumulated vsize (Kb) 25496

[startup+370.044 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 36923 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 369.61
Current children cumulated vsize (Kb) 25496

[startup+380.044 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 37924 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 379.62
Current children cumulated vsize (Kb) 25496

[startup+390.045 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 38924 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 389.62
Current children cumulated vsize (Kb) 25496

[startup+400.047 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 39924 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223104 134558141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 399.62
Current children cumulated vsize (Kb) 25496

[startup+410.048 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 40924 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223120 134556533 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 409.62
Current children cumulated vsize (Kb) 25496

[startup+420.049 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 41925 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 419.63
Current children cumulated vsize (Kb) 25496

[startup+430.05 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 42925 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 429.63
Current children cumulated vsize (Kb) 25496

[startup+440.05 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 43925 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 439.63
Current children cumulated vsize (Kb) 25496

[startup+450.051 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 44925 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 449.63
Current children cumulated vsize (Kb) 25496

[startup+460.052 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 45925 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 459.63
Current children cumulated vsize (Kb) 25496

[startup+470.054 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 46926 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 469.64
Current children cumulated vsize (Kb) 25496

[startup+480.055 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5566 0 0 0 47926 38 0 0 25 0 1 0 1785234481 23932928 5553 4294967295 134512640 135094434 3221224448 3221223072 134557705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5843 5553 145 145 0 5698 0
[pid=19962] vsize: 23372
Current children cumulated CPU time (s) 479.64
Current children cumulated vsize (Kb) 25496

[startup+490.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5575 0 0 0 48926 38 0 0 25 0 1 0 1785234481 23998464 5562 4294967295 134512640 135094434 3221224448 3221223040 134556851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5859 5562 145 145 0 5714 0
[pid=19962] vsize: 23436
Current children cumulated CPU time (s) 489.64
Current children cumulated vsize (Kb) 25560

[startup+500.056 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5576 0 0 0 49926 38 0 0 25 0 1 0 1785234481 23998464 5563 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5859 5563 145 145 0 5714 0
[pid=19962] vsize: 23436
Current children cumulated CPU time (s) 499.64
Current children cumulated vsize (Kb) 25560

[startup+510.057 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5577 0 0 0 50927 38 0 0 25 0 1 0 1785234481 23998464 5564 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5859 5564 145 145 0 5714 0
[pid=19962] vsize: 23436
Current children cumulated CPU time (s) 509.65
Current children cumulated vsize (Kb) 25560

[startup+520.058 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5628 0 0 0 51926 38 0 0 25 0 1 0 1785234481 24207360 5615 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5910 5615 145 145 0 5765 0
[pid=19962] vsize: 23640
Current children cumulated CPU time (s) 519.64
Current children cumulated vsize (Kb) 25764

[startup+530.059 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5660 0 0 0 52926 38 0 0 25 0 1 0 1785234481 24338432 5647 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5942 5647 145 145 0 5797 0
[pid=19962] vsize: 23768
Current children cumulated CPU time (s) 529.64
Current children cumulated vsize (Kb) 25892

[startup+540.061 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5660 0 0 0 53926 38 0 0 25 0 1 0 1785234481 24338432 5647 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5942 5647 145 145 0 5797 0
[pid=19962] vsize: 23768
Current children cumulated CPU time (s) 539.64
Current children cumulated vsize (Kb) 25892

[startup+550.062 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5660 0 0 0 54926 38 0 0 25 0 1 0 1785234481 24338432 5647 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5942 5647 145 145 0 5797 0
[pid=19962] vsize: 23768
Current children cumulated CPU time (s) 549.64
Current children cumulated vsize (Kb) 25892

[startup+560.062 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5667 0 0 0 55926 38 0 0 25 0 1 0 1785234481 24371200 5654 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5950 5654 145 145 0 5805 0
[pid=19962] vsize: 23800
Current children cumulated CPU time (s) 559.64
Current children cumulated vsize (Kb) 25924

[startup+570.063 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5675 0 0 0 56927 38 0 0 25 0 1 0 1785234481 24403968 5662 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5958 5662 145 145 0 5813 0
[pid=19962] vsize: 23832
Current children cumulated CPU time (s) 569.65
Current children cumulated vsize (Kb) 25956

[startup+580.064 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5675 0 0 0 57927 38 0 0 25 0 1 0 1785234481 24403968 5662 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5958 5662 145 145 0 5813 0
[pid=19962] vsize: 23832
Current children cumulated CPU time (s) 579.65
Current children cumulated vsize (Kb) 25956

[startup+590.065 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5691 0 0 0 58927 38 0 0 25 0 1 0 1785234481 24485888 5678 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5978 5678 145 145 0 5833 0
[pid=19962] vsize: 23912
Current children cumulated CPU time (s) 589.65
Current children cumulated vsize (Kb) 26036

[startup+600.066 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5702 0 0 0 59927 38 0 0 25 0 1 0 1785234481 24535040 5689 4294967295 134512640 135094434 3221224448 3221223008 134550329 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 5990 5689 145 145 0 5845 0
[pid=19962] vsize: 23960
Current children cumulated CPU time (s) 599.65
Current children cumulated vsize (Kb) 26084

[startup+610.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5713 0 0 0 60927 38 0 0 25 0 1 0 1785234481 24600576 5700 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6006 5700 145 145 0 5861 0
[pid=19962] vsize: 24024
Current children cumulated CPU time (s) 609.65
Current children cumulated vsize (Kb) 26148

[startup+620.067 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5718 0 0 0 61928 38 0 0 25 0 1 0 1785234481 24633344 5705 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6014 5705 145 145 0 5869 0
[pid=19962] vsize: 24056
Current children cumulated CPU time (s) 619.66
Current children cumulated vsize (Kb) 26180

[startup+630.068 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5719 0 0 0 62928 38 0 0 25 0 1 0 1785234481 24633344 5706 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6014 5706 145 145 0 5869 0
[pid=19962] vsize: 24056
Current children cumulated CPU time (s) 629.66
Current children cumulated vsize (Kb) 26180

[startup+640.07 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5719 0 0 0 63928 38 0 0 25 0 1 0 1785234481 24633344 5706 4294967295 134512640 135094434 3221224448 3221223136 134554687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6014 5706 145 145 0 5869 0
[pid=19962] vsize: 24056
Current children cumulated CPU time (s) 639.66
Current children cumulated vsize (Kb) 26180

[startup+650.071 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5719 0 0 0 64929 38 0 0 25 0 1 0 1785234481 24633344 5706 4294967295 134512640 135094434 3221224448 3221223040 134557310 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6014 5706 145 145 0 5869 0
[pid=19962] vsize: 24056
Current children cumulated CPU time (s) 649.67
Current children cumulated vsize (Kb) 26180

[startup+660.072 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5720 0 0 0 65929 38 0 0 25 0 1 0 1785234481 24633344 5707 4294967295 134512640 135094434 3221224448 3221223104 134558420 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6014 5707 145 145 0 5869 0
[pid=19962] vsize: 24056
Current children cumulated CPU time (s) 659.67
Current children cumulated vsize (Kb) 26180

[startup+670.073 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5730 0 0 0 66929 38 0 0 25 0 1 0 1785234481 24682496 5717 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6026 5717 145 145 0 5881 0
[pid=19962] vsize: 24104
Current children cumulated CPU time (s) 669.67
Current children cumulated vsize (Kb) 26228

[startup+680.073 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5733 0 0 0 67929 38 0 0 25 0 1 0 1785234481 24698880 5720 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6030 5720 145 145 0 5885 0
[pid=19962] vsize: 24120
Current children cumulated CPU time (s) 679.67
Current children cumulated vsize (Kb) 26244

[startup+690.075 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5761 0 0 0 68929 38 0 0 25 0 1 0 1785234481 24813568 5748 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6058 5748 145 145 0 5913 0
[pid=19962] vsize: 24232
Current children cumulated CPU time (s) 689.67
Current children cumulated vsize (Kb) 26356

[startup+700.076 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5768 0 0 0 69930 38 0 0 25 0 1 0 1785234481 24829952 5755 4294967295 134512640 135094434 3221224448 3221223120 134556277 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6062 5755 145 145 0 5917 0
[pid=19962] vsize: 24248
Current children cumulated CPU time (s) 699.68
Current children cumulated vsize (Kb) 26372

[startup+710.077 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5768 0 0 0 70930 38 0 0 25 0 1 0 1785234481 24829952 5755 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6062 5755 145 145 0 5917 0
[pid=19962] vsize: 24248
Current children cumulated CPU time (s) 709.68
Current children cumulated vsize (Kb) 26372

[startup+720.078 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5774 0 0 0 71930 38 0 0 25 0 1 0 1785234481 24862720 5761 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6070 5761 145 145 0 5925 0
[pid=19962] vsize: 24280
Current children cumulated CPU time (s) 719.68
Current children cumulated vsize (Kb) 26404

[startup+730.079 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5775 0 0 0 72930 38 0 0 25 0 1 0 1785234481 24862720 5762 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6070 5762 145 145 0 5925 0
[pid=19962] vsize: 24280
Current children cumulated CPU time (s) 729.68
Current children cumulated vsize (Kb) 26404

[startup+740.08 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5793 0 0 0 73931 38 0 0 25 0 1 0 1785234481 24993792 5780 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6102 5780 145 145 0 5957 0
[pid=19962] vsize: 24408
Current children cumulated CPU time (s) 739.69
Current children cumulated vsize (Kb) 26532

[startup+750.081 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5797 0 0 0 74931 38 0 0 25 0 1 0 1785234481 24993792 5784 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6102 5784 145 145 0 5957 0
[pid=19962] vsize: 24408
Current children cumulated CPU time (s) 749.69
Current children cumulated vsize (Kb) 26532

[startup+760.082 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5797 0 0 0 75931 38 0 0 25 0 1 0 1785234481 24993792 5784 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6102 5784 145 145 0 5957 0
[pid=19962] vsize: 24408
Current children cumulated CPU time (s) 759.69
Current children cumulated vsize (Kb) 26532

[startup+770.084 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5805 0 0 0 76931 39 0 0 25 0 1 0 1785234481 24993792 5792 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19962/statm): 6102 5792 145 145 0 5957 0
[pid=19962] vsize: 24408
Current children cumulated CPU time (s) 769.7
Current children cumulated vsize (Kb) 26532

[startup+780.085 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5823 0 0 0 77930 39 0 0 25 0 1 0 1785234481 25124864 5810 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6134 5810 145 145 0 5989 0
[pid=19962] vsize: 24536
Current children cumulated CPU time (s) 779.69
Current children cumulated vsize (Kb) 26660

[startup+790.086 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5832 0 0 0 78931 39 0 0 25 0 1 0 1785234481 25387008 5819 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6198 5819 145 145 0 6053 0
[pid=19962] vsize: 24792
Current children cumulated CPU time (s) 789.7
Current children cumulated vsize (Kb) 26916

[startup+800.086 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5833 0 0 0 79931 39 0 0 25 0 1 0 1785234481 25387008 5820 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6198 5820 145 145 0 6053 0
[pid=19962] vsize: 24792
Current children cumulated CPU time (s) 799.7
Current children cumulated vsize (Kb) 26916

[startup+810.086 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5833 0 0 0 80931 39 0 0 25 0 1 0 1785234481 25387008 5820 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6198 5820 145 145 0 6053 0
[pid=19962] vsize: 24792
Current children cumulated CPU time (s) 809.7
Current children cumulated vsize (Kb) 26916

[startup+820.087 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5833 0 0 0 81931 39 0 0 25 0 1 0 1785234481 25387008 5820 4294967295 134512640 135094434 3221224448 3221223120 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6198 5820 145 145 0 6053 0
[pid=19962] vsize: 24792
Current children cumulated CPU time (s) 819.7
Current children cumulated vsize (Kb) 26916

[startup+830.088 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5833 0 0 0 82931 39 0 0 25 0 1 0 1785234481 25387008 5820 4294967295 134512640 135094434 3221224448 3221223040 134556853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6198 5820 145 145 0 6053 0
[pid=19962] vsize: 24792
Current children cumulated CPU time (s) 829.7
Current children cumulated vsize (Kb) 26916

[startup+840.089 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5833 0 0 0 83932 39 0 0 25 0 1 0 1785234481 25387008 5820 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6198 5820 145 145 0 6053 0
[pid=19962] vsize: 24792
Current children cumulated CPU time (s) 839.71
Current children cumulated vsize (Kb) 26916

[startup+850.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5842 0 0 0 84932 39 0 0 25 0 1 0 1785234481 25452544 5829 4294967295 134512640 135094434 3221224448 3221223104 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5829 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 849.71
Current children cumulated vsize (Kb) 26980

[startup+860.09 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 85932 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 859.71
Current children cumulated vsize (Kb) 26980

[startup+870.091 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 86932 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 869.71
Current children cumulated vsize (Kb) 26980

[startup+880.092 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 87933 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 879.72
Current children cumulated vsize (Kb) 26980

[startup+890.094 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 88933 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 889.72
Current children cumulated vsize (Kb) 26980

[startup+900.095 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 89933 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 899.72
Current children cumulated vsize (Kb) 26980

[startup+910.096 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 90933 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 909.72
Current children cumulated vsize (Kb) 26980

[startup+920.097 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 91934 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 919.73
Current children cumulated vsize (Kb) 26980

[startup+930.098 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 92934 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223104 134558225 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 929.73
Current children cumulated vsize (Kb) 26980

[startup+940.1 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 93934 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 939.73
Current children cumulated vsize (Kb) 26980

[startup+950.101 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 94935 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 949.74
Current children cumulated vsize (Kb) 26980

[startup+960.102 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 95935 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 959.74
Current children cumulated vsize (Kb) 26980

[startup+970.104 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5843 0 0 0 96935 39 0 0 25 0 1 0 1785234481 25452544 5830 4294967295 134512640 135094434 3221224448 3221223104 134557976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6214 5830 145 145 0 6069 0
[pid=19962] vsize: 24856
Current children cumulated CPU time (s) 969.74
Current children cumulated vsize (Kb) 26980

[startup+980.105 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 5959 0 0 0 97933 40 0 0 25 0 1 0 1785234481 25927680 5946 4294967295 134512640 135094434 3221224448 3221223072 134562106 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6330 5946 145 145 0 6185 0
[pid=19962] vsize: 25320
Current children cumulated CPU time (s) 979.73
Current children cumulated vsize (Kb) 27444

[startup+990.105 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6122 0 0 0 98930 40 0 0 25 0 1 0 1785234481 26587136 6109 4294967295 134512640 135094434 3221224448 3221223072 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6491 6109 145 145 0 6346 0
[pid=19962] vsize: 25964
Current children cumulated CPU time (s) 989.7
Current children cumulated vsize (Kb) 28088

[startup+1000.11 s]
Raw data (loadavg): 0.99 0.97 0.95 1/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) T 19958 19958 31915 0 -1 0 6253 0 0 0 99927 42 0 0 25 0 1 0 1785234481 27111424 6240 4294967295 134512640 135094434 3221224448 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6619 6240 145 145 0 6474 0
[pid=19962] vsize: 26476
Current children cumulated CPU time (s) 999.69
Current children cumulated vsize (Kb) 28600

[startup+1010.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6256 0 0 0 100927 42 0 0 25 0 1 0 1785234481 27123712 6243 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6622 6243 145 145 0 6477 0
[pid=19962] vsize: 26488
Current children cumulated CPU time (s) 1009.69
Current children cumulated vsize (Kb) 28612

[startup+1020.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6256 0 0 0 101928 42 0 0 25 0 1 0 1785234481 27123712 6243 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6622 6243 145 145 0 6477 0
[pid=19962] vsize: 26488
Current children cumulated CPU time (s) 1019.7
Current children cumulated vsize (Kb) 28612

[startup+1030.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6256 0 0 0 102928 42 0 0 25 0 1 0 1785234481 27123712 6243 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6622 6243 145 145 0 6477 0
[pid=19962] vsize: 26488
Current children cumulated CPU time (s) 1029.7
Current children cumulated vsize (Kb) 28612

[startup+1040.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6256 0 0 0 103928 42 0 0 25 0 1 0 1785234481 27123712 6243 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6622 6243 145 145 0 6477 0
[pid=19962] vsize: 26488
Current children cumulated CPU time (s) 1039.7
Current children cumulated vsize (Kb) 28612

[startup+1050.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6256 0 0 0 104928 42 0 0 25 0 1 0 1785234481 27123712 6243 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6622 6243 145 145 0 6477 0
[pid=19962] vsize: 26488
Current children cumulated CPU time (s) 1049.7
Current children cumulated vsize (Kb) 28612

[startup+1060.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6263 0 0 0 105928 42 0 0 25 0 1 0 1785234481 27152384 6250 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6629 6250 145 145 0 6484 0
[pid=19962] vsize: 26516
Current children cumulated CPU time (s) 1059.7
Current children cumulated vsize (Kb) 28640

[startup+1070.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6263 0 0 0 106929 42 0 0 25 0 1 0 1785234481 27152384 6250 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6629 6250 145 145 0 6484 0
[pid=19962] vsize: 26516
Current children cumulated CPU time (s) 1069.71
Current children cumulated vsize (Kb) 28640

[startup+1080.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6266 0 0 0 107929 42 0 0 25 0 1 0 1785234481 27217920 6253 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6645 6253 145 145 0 6500 0
[pid=19962] vsize: 26580
Current children cumulated CPU time (s) 1079.71
Current children cumulated vsize (Kb) 28704

[startup+1090.11 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6266 0 0 0 108929 42 0 0 25 0 1 0 1785234481 27217920 6253 4294967295 134512640 135094434 3221224448 3221223120 134556297 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6645 6253 145 145 0 6500 0
[pid=19962] vsize: 26580
Current children cumulated CPU time (s) 1089.71
Current children cumulated vsize (Kb) 28704

[startup+1100.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6279 0 0 0 109929 42 0 0 25 0 1 0 1785234481 27250688 6266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6653 6266 145 145 0 6508 0
[pid=19962] vsize: 26612
Current children cumulated CPU time (s) 1099.71
Current children cumulated vsize (Kb) 28736

[startup+1110.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6407 0 0 0 110927 43 0 0 25 0 1 0 1785234481 27774976 6394 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6781 6394 145 145 0 6636 0
[pid=19962] vsize: 27124
Current children cumulated CPU time (s) 1109.7
Current children cumulated vsize (Kb) 29248

[startup+1120.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6525 0 0 0 111925 43 0 0 25 0 1 0 1785234481 28262400 6512 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6900 6512 145 145 0 6755 0
[pid=19962] vsize: 27600
Current children cumulated CPU time (s) 1119.68
Current children cumulated vsize (Kb) 29724

[startup+1130.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6525 0 0 0 112926 43 0 0 25 0 1 0 1785234481 28262400 6512 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6900 6512 145 145 0 6755 0
[pid=19962] vsize: 27600
Current children cumulated CPU time (s) 1129.69
Current children cumulated vsize (Kb) 29724

[startup+1140.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6530 0 0 0 113926 43 0 0 25 0 1 0 1785234481 28295168 6517 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6908 6517 145 145 0 6763 0
[pid=19962] vsize: 27632
Current children cumulated CPU time (s) 1139.69
Current children cumulated vsize (Kb) 29756

[startup+1150.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6535 0 0 0 114926 43 0 0 25 0 1 0 1785234481 28327936 6522 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6916 6522 145 145 0 6771 0
[pid=19962] vsize: 27664
Current children cumulated CPU time (s) 1149.69
Current children cumulated vsize (Kb) 29788

[startup+1160.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6536 0 0 0 115926 43 0 0 25 0 1 0 1785234481 28327936 6523 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6916 6523 145 145 0 6771 0
[pid=19962] vsize: 27664
Current children cumulated CPU time (s) 1159.69
Current children cumulated vsize (Kb) 29788

[startup+1170.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6536 0 0 0 116927 43 0 0 25 0 1 0 1785234481 28327936 6523 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6916 6523 145 145 0 6771 0
[pid=19962] vsize: 27664
Current children cumulated CPU time (s) 1169.7
Current children cumulated vsize (Kb) 29788

[startup+1180.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6542 0 0 0 117927 43 0 0 25 0 1 0 1785234481 28348416 6529 4294967295 134512640 135094434 3221224448 3221222380 134780472 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6921 6529 145 145 0 6776 0
[pid=19962] vsize: 27684
Current children cumulated CPU time (s) 1179.7
Current children cumulated vsize (Kb) 29808

[startup+1190.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6542 0 0 0 118926 44 0 0 25 0 1 0 1785234481 28348416 6529 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6921 6529 145 145 0 6776 0
[pid=19962] vsize: 27684
Current children cumulated CPU time (s) 1189.7
Current children cumulated vsize (Kb) 29808

[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6542 0 0 0 119927 44 0 0 25 0 1 0 1785234481 28348416 6529 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6921 6529 145 145 0 6776 0
[pid=19962] vsize: 27684
Current children cumulated CPU time (s) 1199.71
Current children cumulated vsize (Kb) 29808

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6542 0 0 0 120927 44 0 0 25 0 1 0 1785234481 28348416 6529 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6921 6529 145 145 0 6776 0
[pid=19962] vsize: 27684
Current children cumulated CPU time (s) 1209.71
Current children cumulated vsize (Kb) 29808



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.13 s]
Raw data (loadavg): 0.99 0.97 0.95 2/57 19962
Raw data (/proc/19958/stat): 19958 (minisat+_script) S 19957 19958 31915 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785234476 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/19958/statm): 531 226 485 147 0 384 0
[pid=19958] vsize: 2124
Raw data (/proc/19962/stat): 19962 (minisat+_64-bit) R 19958 19958 31915 0 -1 0 6542 0 0 0 120927 44 0 0 25 0 1 0 1785234481 28348416 6529 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/19962/statm): 6921 6529 145 145 0 6776 0
[pid=19962] vsize: 27684
Current children cumulated CPU time (s) 1209.71
Current children cumulated vsize (Kb) 29808

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

Child status: 10
Real time (s): 1210.14
CPU time (s): 1209.73
CPU user time (s): 1209.28
CPU system time (s): 0.45693
CPU usage (%): 99.9661
Max. virtual memory (cumulated for all children) (Kb): 29808

Verifier Data

ERROR: no interpretation found !