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

Namesubmitted/manquinho/synthesis-ptl-cmos-circuits/normalized-mux.opb
MD5SUMfa7153262db792d01bec14f5a651af5b
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 872
Optimality of the best value was proved YES
Number of terms in the objective function 232
Biggest coefficient in the objective function 61
Number of bits for the biggest coefficient in the objective function 6
Sum of the numbers in the objective function 9597
Number of bits of the sum of numbers in the objective function 14
Biggest number in a constraint 61
Number of bits of the biggest number in a constraint 6
Biggest sum of numbers in a constraint 9597
Number of bits of the biggest sum of numbers14
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark18.0453
Number of variables232
Total number of constraints527
Number of constraints which are clauses527
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 constraint27

Trace number 2212

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        882840 kB
Buffers:         34096 kB
Cached:          91472 kB
SwapCached:        708 kB
Active:          65260 kB
Inactive:        62876 kB
HighTotal:      131008 kB
HighFree:        66556 kB
LowTotal:       903652 kB
LowFree:        816284 kB
SwapTotal:     2097136 kB
SwapFree:      2095936 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5740 kB
Slab:            18048 kB
Committed_AS:    64128 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 18:31:09 (client local time) WITH STATUS 10 IN 1209.28 SECONDS
stats: 2597 7 1209.28 10

Solver Data

c Parsing PB file...
c Converting 527 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 |     527     2331 |     175       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 1330
c ---[   0]---> Sorter-cost:29793     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   71948   169106 |   23982       0        0     nan |  0.000 % |
c |       100 |   71806   168786 |   26380      99     2955    29.8 |  0.129 % |
c |       251 |   71806   168786 |   29018     250     6809    27.2 |  0.129 % |
c |       477 |   71373   167811 |   31920     472    10592    22.4 |  0.579 % |
c ==============================================================================
c Found solution: 1234
c ---[   0]---> Sorter-cost:24283     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       513 |  131893   309118 |   43964     507    11929    23.5 |  0.579 % |
c |       614 |  131893   309118 |   48360     608    14630    24.1 |  0.337 % |
c |       765 |  131893   309118 |   53196     759    16948    22.3 |  0.337 % |
c |       990 |  131893   309118 |   58516     984    20452    20.8 |  0.337 % |
c |      1327 |  131793   308891 |   64367    1316    29130    22.1 |  0.398 % |
c |      1833 |  131793   308891 |   70804    1822    42478    23.3 |  0.398 % |
c |      2592 |  131771   308841 |   77884    2580    60031    23.3 |  0.409 % |
c |      3733 |  131637   308542 |   85673    3717    88874    23.9 |  0.482 % |
c ==============================================================================
c Found solution: 1233
c ---[   0]---> Sorter-cost:    6     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4682 |  131826   309294 |   43942    4666   147647    31.6 |  0.482 % |
c |      4783 |  131826   309294 |   48336    4767   149006    31.3 |  0.483 % |
c ==============================================================================
c Found solution: 1199
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4810 |  132099   309958 |   44033    4794   152722    31.9 |  0.483 % |
c |      4910 |  132099   309958 |   48436    4894   157309    32.1 |  0.484 % |
c |      5060 |  132099   309958 |   53279    5044   166454    33.0 |  0.484 % |
c |      5285 |  132099   309958 |   58607    5269   177805    33.7 |  0.484 % |
c |      5622 |  132099   309958 |   64468    5606   190601    34.0 |  0.484 % |
c |      6128 |  131993   309729 |   70915    6108   202232    33.1 |  0.557 % |
c |      6889 |  131993   309729 |   78007    6869   218880    31.9 |  0.557 % |
c |      8029 |  131989   309720 |   85807    8008   393024    49.1 |  0.559 % |
c |      9737 |  131989   309720 |   94388    9716   464106    47.8 |  0.559 % |
c |     12300 |  131949   309629 |  103827   12275   614249    50.0 |  0.586 % |
c ==============================================================================
c Found solution: 1196
c ---[   0]---> Sorter-cost:    5     Base: 2 5 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15838 |  132219   310293 |   44073   15813  1409395    89.1 |  0.586 % |
c |     15939 |  132219   310293 |   48480   15914  1410776    88.6 |  0.588 % |
c |     16089 |  132219   310293 |   53328   16064  1413959    88.0 |  0.588 % |
c |     16316 |  132219   310293 |   58661   16291  1420583    87.2 |  0.588 % |
c |     16653 |  132219   310293 |   64527   16628  1424998    85.7 |  0.588 % |
c |     17160 |  132219   310293 |   70980   17135  1431067    83.5 |  0.588 % |
c |     17920 |  132219   310293 |   78078   17895  1444512    80.7 |  0.588 % |
c |     19059 |  132219   310293 |   85885   19034  1508888    79.3 |  0.588 % |
c |     20768 |  132219   310293 |   94474   20743  1585879    76.5 |  0.588 % |
c |     23330 |  132219   310293 |  103921   23305  1683334    72.2 |  0.588 % |
c |     27176 |  132219   310293 |  114314   27151  1841999    67.8 |  0.588 % |
c |     32944 |  132219   310293 |  125745   32919  2133960    64.8 |  0.588 % |
c |     41593 |  132219   310293 |  138319   41568  2548271    61.3 |  0.588 % |
c |     54567 |  132219   310293 |  152151   54542  3221898    59.1 |  0.588 % |
c |     74029 |  132219   310293 |  167367   74004  4058574    54.8 |  0.588 % |
c |    103224 |  132219   310293 |  184103  103199  5283147    51.2 |  0.588 % |

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/5568/stat): 5568 (minisat+_script) R 5567 5568 1333 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1785103563 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/5568/statm): 174 3 169 147 0 27 0
[pid=5568] 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=5569
New process pid=5570
New process pid=5571
execve syscall for /bin/sed executable
One traced child (pid=5570) 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=5571) exited with status: 0
One traced child (pid=5569) exited with status: 0
New process pid=5572
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc13/normalized-mux.opb

[startup+10.0033 s]
Raw data (loadavg): 0.92 0.95 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4197 0 0 0 964 18 0 0 25 0 1 0 1785103568 18714624 3999 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 4569 3999 145 145 0 4424 0
[pid=5572] vsize: 18276
Current children cumulated CPU time (s) 9.83
Current children cumulated vsize (Kb) 20400

[startup+20.0049 s]
Raw data (loadavg): 0.93 0.96 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4289 0 0 0 1962 19 0 0 25 0 1 0 1785103568 19083264 4091 4294967295 134512640 135094434 3221224448 3221223104 134558295 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 4659 4091 145 145 0 4514 0
[pid=5572] vsize: 18636
Current children cumulated CPU time (s) 19.82
Current children cumulated vsize (Kb) 20760

[startup+30.0056 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4492 0 0 0 2960 20 0 0 25 0 1 0 1785103568 19902464 4290 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 4859 4290 145 145 0 4714 0
[pid=5572] vsize: 19436
Current children cumulated CPU time (s) 29.81
Current children cumulated vsize (Kb) 21560

[startup+40.0062 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4503 0 0 0 3960 20 0 0 25 0 1 0 1785103568 19943424 4301 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 4869 4301 145 145 0 4724 0
[pid=5572] vsize: 19476
Current children cumulated CPU time (s) 39.81
Current children cumulated vsize (Kb) 21600

[startup+50.0079 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4694 0 0 0 4957 22 0 0 25 0 1 0 1785103568 20721664 4492 4294967295 134512640 135094434 3221224448 3221223072 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 5059 4492 145 145 0 4914 0
[pid=5572] vsize: 20236
Current children cumulated CPU time (s) 49.8
Current children cumulated vsize (Kb) 22360

[startup+60.0085 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4768 0 0 0 5955 23 0 0 25 0 1 0 1785103568 21045248 4566 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 5138 4566 145 145 0 4993 0
[pid=5572] vsize: 20552
Current children cumulated CPU time (s) 59.79
Current children cumulated vsize (Kb) 22676

[startup+70.0102 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 4890 0 0 0 6953 24 0 0 25 0 1 0 1785103568 21553152 4688 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 5262 4688 145 145 0 5117 0
[pid=5572] vsize: 21048
Current children cumulated CPU time (s) 69.78
Current children cumulated vsize (Kb) 23172

[startup+80.0118 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5000 0 0 0 7951 25 0 0 25 0 1 0 1785103568 21995520 4798 4294967295 134512640 135094434 3221224448 3221223040 134556975 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 5370 4798 145 145 0 5225 0
[pid=5572] vsize: 21480
Current children cumulated CPU time (s) 79.77
Current children cumulated vsize (Kb) 23604

[startup+90.0125 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5278 0 0 0 8945 27 0 0 25 0 1 0 1785103568 23130112 5076 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 5647 5076 145 145 0 5502 0
[pid=5572] vsize: 22588
Current children cumulated CPU time (s) 89.73
Current children cumulated vsize (Kb) 24712

[startup+100.013 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5557 0 0 0 9940 29 0 0 25 0 1 0 1785103568 24268800 5355 4294967295 134512640 135094434 3221224448 3221223104 134557896 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 5925 5355 145 145 0 5780 0
[pid=5572] vsize: 23700
Current children cumulated CPU time (s) 99.7
Current children cumulated vsize (Kb) 25824

[startup+110.014 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5829 0 0 0 10937 31 0 0 25 0 1 0 1785103568 25382912 5627 4294967295 134512640 135094434 3221224448 3221223072 134557669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6197 5627 145 145 0 6052 0
[pid=5572] vsize: 24788
Current children cumulated CPU time (s) 109.69
Current children cumulated vsize (Kb) 26912

[startup+120.015 s]
Raw data (loadavg): 0.98 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5874 0 0 0 11936 31 0 0 25 0 1 0 1785103568 25567232 5672 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6242 5672 145 145 0 6097 0
[pid=5572] vsize: 24968
Current children cumulated CPU time (s) 119.68
Current children cumulated vsize (Kb) 27092

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 5939 0 0 0 12935 32 0 0 25 0 1 0 1785103568 25833472 5737 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6307 5737 145 145 0 6162 0
[pid=5572] vsize: 25228
Current children cumulated CPU time (s) 129.68
Current children cumulated vsize (Kb) 27352

[startup+140.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6021 0 0 0 13933 33 0 0 25 0 1 0 1785103568 26169344 5819 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6389 5819 145 145 0 6244 0
[pid=5572] vsize: 25556
Current children cumulated CPU time (s) 139.67
Current children cumulated vsize (Kb) 27680

[startup+150.017 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6084 0 0 0 14931 34 0 0 25 0 1 0 1785103568 26427392 5882 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6452 5882 145 145 0 6307 0
[pid=5572] vsize: 25808
Current children cumulated CPU time (s) 149.66
Current children cumulated vsize (Kb) 27932

[startup+160.018 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6152 0 0 0 15929 36 0 0 25 0 1 0 1785103568 26705920 5950 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6520 5950 145 145 0 6375 0
[pid=5572] vsize: 26080
Current children cumulated CPU time (s) 159.66
Current children cumulated vsize (Kb) 28204

[startup+170.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6226 0 0 0 16927 37 0 0 25 0 1 0 1785103568 27009024 6024 4294967295 134512640 135094434 3221224448 3221223088 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6594 6024 145 145 0 6449 0
[pid=5572] vsize: 26376
Current children cumulated CPU time (s) 169.65
Current children cumulated vsize (Kb) 28500

[startup+180.02 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6308 0 0 0 17925 38 0 0 25 0 1 0 1785103568 27344896 6106 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6676 6106 145 145 0 6531 0
[pid=5572] vsize: 26704
Current children cumulated CPU time (s) 179.64
Current children cumulated vsize (Kb) 28828

[startup+190.021 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6374 0 0 0 18924 39 0 0 25 0 1 0 1785103568 27615232 6172 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6742 6172 145 145 0 6597 0
[pid=5572] vsize: 26968
Current children cumulated CPU time (s) 189.64
Current children cumulated vsize (Kb) 29092

[startup+200.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6439 0 0 0 19923 40 0 0 25 0 1 0 1785103568 27881472 6237 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6807 6237 145 145 0 6662 0
[pid=5572] vsize: 27228
Current children cumulated CPU time (s) 199.64
Current children cumulated vsize (Kb) 29352

[startup+210.022 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6501 0 0 0 20922 40 0 0 25 0 1 0 1785103568 28135424 6299 4294967295 134512640 135094434 3221224448 3221223092 134558040 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6869 6299 145 145 0 6724 0
[pid=5572] vsize: 27476
Current children cumulated CPU time (s) 209.63
Current children cumulated vsize (Kb) 29600

[startup+220.024 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6571 0 0 0 21920 41 0 0 25 0 1 0 1785103568 28422144 6369 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 6939 6369 145 145 0 6794 0
[pid=5572] vsize: 27756
Current children cumulated CPU time (s) 219.62
Current children cumulated vsize (Kb) 29880

[startup+230.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6647 0 0 0 22919 42 0 0 25 0 1 0 1785103568 28733440 6445 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7015 6445 145 145 0 6870 0
[pid=5572] vsize: 28060
Current children cumulated CPU time (s) 229.62
Current children cumulated vsize (Kb) 30184

[startup+240.025 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6696 0 0 0 23918 43 0 0 25 0 1 0 1785103568 29061120 6494 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7095 6494 145 145 0 6950 0
[pid=5572] vsize: 28380
Current children cumulated CPU time (s) 239.62
Current children cumulated vsize (Kb) 30504

[startup+250.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6762 0 0 0 24917 43 0 0 25 0 1 0 1785103568 29323264 6560 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7159 6560 145 145 0 7014 0
[pid=5572] vsize: 28636
Current children cumulated CPU time (s) 249.61
Current children cumulated vsize (Kb) 30760

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6829 0 0 0 25916 44 0 0 25 0 1 0 1785103568 29593600 6627 4294967295 134512640 135094434 3221224448 3221223040 134557042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7225 6627 145 145 0 7080 0
[pid=5572] vsize: 28900
Current children cumulated CPU time (s) 259.61
Current children cumulated vsize (Kb) 31024

[startup+270.028 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6897 0 0 0 26915 45 0 0 25 0 1 0 1785103568 29872128 6695 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7293 6695 145 145 0 7148 0
[pid=5572] vsize: 29172
Current children cumulated CPU time (s) 269.61
Current children cumulated vsize (Kb) 31296

[startup+280.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 6961 0 0 0 27914 45 0 0 25 0 1 0 1785103568 30126080 6759 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7355 6759 145 145 0 7210 0
[pid=5572] vsize: 29420
Current children cumulated CPU time (s) 279.6
Current children cumulated vsize (Kb) 31544

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7024 0 0 0 28912 46 0 0 25 0 1 0 1785103568 30371840 6822 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7415 6822 145 145 0 7270 0
[pid=5572] vsize: 29660
Current children cumulated CPU time (s) 289.59
Current children cumulated vsize (Kb) 31784

[startup+300.03 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7081 0 0 0 29911 47 0 0 25 0 1 0 1785103568 30601216 6879 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7471 6879 145 145 0 7326 0
[pid=5572] vsize: 29884
Current children cumulated CPU time (s) 299.59
Current children cumulated vsize (Kb) 32008

[startup+310.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7137 0 0 0 30910 47 0 0 25 0 1 0 1785103568 30826496 6935 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7526 6935 145 145 0 7381 0
[pid=5572] vsize: 30104
Current children cumulated CPU time (s) 309.58
Current children cumulated vsize (Kb) 32228

[startup+320.031 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7206 0 0 0 31909 48 0 0 25 0 1 0 1785103568 31117312 7004 4294967295 134512640 135094434 3221224448 3221223072 134557606 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7597 7004 145 145 0 7452 0
[pid=5572] vsize: 30388
Current children cumulated CPU time (s) 319.58
Current children cumulated vsize (Kb) 32512

[startup+330.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7285 0 0 0 32908 48 0 0 25 0 1 0 1785103568 31424512 7083 4294967295 134512640 135094434 3221224448 3221223040 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7672 7083 145 145 0 7527 0
[pid=5572] vsize: 30688
Current children cumulated CPU time (s) 329.57
Current children cumulated vsize (Kb) 32812

[startup+340.032 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7347 0 0 0 33906 49 0 0 25 0 1 0 1785103568 31674368 7145 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7733 7145 145 145 0 7588 0
[pid=5572] vsize: 30932
Current children cumulated CPU time (s) 339.56
Current children cumulated vsize (Kb) 33056

[startup+350.033 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7421 0 0 0 34905 50 0 0 25 0 1 0 1785103568 31973376 7219 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7806 7219 145 145 0 7661 0
[pid=5572] vsize: 31224
Current children cumulated CPU time (s) 349.56
Current children cumulated vsize (Kb) 33348

[startup+360.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7494 0 0 0 35904 51 0 0 25 0 1 0 1785103568 32260096 7292 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7876 7292 145 145 0 7731 0
[pid=5572] vsize: 31504
Current children cumulated CPU time (s) 359.56
Current children cumulated vsize (Kb) 33628

[startup+370.034 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7578 0 0 0 36903 51 0 0 25 0 1 0 1785103568 32600064 7376 4294967295 134512640 135094434 3221224448 3221223040 134557042 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 7959 7376 145 145 0 7814 0
[pid=5572] vsize: 31836
Current children cumulated CPU time (s) 369.55
Current children cumulated vsize (Kb) 33960

[startup+380.035 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7652 0 0 0 37902 52 0 0 25 0 1 0 1785103568 32899072 7450 4294967295 134512640 135094434 3221224448 3221223040 134557182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8032 7450 145 145 0 7887 0
[pid=5572] vsize: 32128
Current children cumulated CPU time (s) 379.55
Current children cumulated vsize (Kb) 34252

[startup+390.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7726 0 0 0 38899 53 0 0 25 0 1 0 1785103568 33198080 7524 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8105 7524 145 145 0 7960 0
[pid=5572] vsize: 32420
Current children cumulated CPU time (s) 389.53
Current children cumulated vsize (Kb) 34544

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7789 0 0 0 39898 53 0 0 25 0 1 0 1785103568 33452032 7587 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8167 7587 145 145 0 8022 0
[pid=5572] vsize: 32668
Current children cumulated CPU time (s) 399.52
Current children cumulated vsize (Kb) 34792

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7861 0 0 0 40897 54 0 0 25 0 1 0 1785103568 33742848 7659 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8238 7659 145 145 0 8093 0
[pid=5572] vsize: 32952
Current children cumulated CPU time (s) 409.52
Current children cumulated vsize (Kb) 35076

[startup+420.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7917 0 0 0 41897 54 0 0 25 0 1 0 1785103568 33980416 7715 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8296 7715 145 145 0 8151 0
[pid=5572] vsize: 33184
Current children cumulated CPU time (s) 419.52
Current children cumulated vsize (Kb) 35308

[startup+430.039 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 7988 0 0 0 42895 55 0 0 25 0 1 0 1785103568 34267136 7786 4294967295 134512640 135094434 3221224448 3221223040 134557363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8366 7786 145 145 0 8221 0
[pid=5572] vsize: 33464
Current children cumulated CPU time (s) 429.51
Current children cumulated vsize (Kb) 35588

[startup+440.04 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8046 0 0 0 43893 56 0 0 25 0 1 0 1785103568 34525184 7844 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 8429 7844 145 145 0 8284 0
[pid=5572] vsize: 33716
Current children cumulated CPU time (s) 439.5
Current children cumulated vsize (Kb) 35840

[startup+450.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8117 0 0 0 44892 57 0 0 25 0 1 0 1785103568 34816000 7915 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8500 7915 145 145 0 8355 0
[pid=5572] vsize: 34000
Current children cumulated CPU time (s) 449.5
Current children cumulated vsize (Kb) 36124

[startup+460.042 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8171 0 0 0 45891 57 0 0 25 0 1 0 1785103568 35061760 7969 4294967295 134512640 135094434 3221224448 3221223072 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8560 7969 145 145 0 8415 0
[pid=5572] vsize: 34240
Current children cumulated CPU time (s) 459.49
Current children cumulated vsize (Kb) 36364

[startup+470.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8218 0 0 0 46891 58 0 0 25 0 1 0 1785103568 35250176 8016 4294967295 134512640 135094434 3221224448 3221223112 134556595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8606 8016 145 145 0 8461 0
[pid=5572] vsize: 34424
Current children cumulated CPU time (s) 469.5
Current children cumulated vsize (Kb) 36548

[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8263 0 0 0 47889 58 0 0 25 0 1 0 1785103568 35430400 8061 4294967295 134512640 135094434 3221224448 3221223072 134557660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8650 8061 145 145 0 8505 0
[pid=5572] vsize: 34600
Current children cumulated CPU time (s) 479.48
Current children cumulated vsize (Kb) 36724

[startup+490.044 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8311 0 0 0 48888 59 0 0 25 0 1 0 1785103568 35627008 8109 4294967295 134512640 135094434 3221224448 3221223104 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8698 8109 145 145 0 8553 0
[pid=5572] vsize: 34792
Current children cumulated CPU time (s) 489.48
Current children cumulated vsize (Kb) 36916

[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8353 0 0 0 49887 59 0 0 25 0 1 0 1785103568 35799040 8151 4294967295 134512640 135094434 3221224448 3221223072 134557616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 8740 8151 145 145 0 8595 0
[pid=5572] vsize: 34960
Current children cumulated CPU time (s) 499.47
Current children cumulated vsize (Kb) 37084

[startup+510.046 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8404 0 0 0 50886 59 0 0 24 0 1 0 1785103568 35999744 8202 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 8789 8202 145 145 0 8644 0
[pid=5572] vsize: 35156
Current children cumulated CPU time (s) 509.46
Current children cumulated vsize (Kb) 37280

[startup+520.047 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8460 0 0 0 51885 60 0 0 25 0 1 0 1785103568 36229120 8258 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 8845 8258 145 145 0 8700 0
[pid=5572] vsize: 35380
Current children cumulated CPU time (s) 519.46
Current children cumulated vsize (Kb) 37504

[startup+530.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8519 0 0 0 52884 62 0 0 25 0 1 0 1785103568 36462592 8317 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 8902 8317 145 145 0 8757 0
[pid=5572] vsize: 35608
Current children cumulated CPU time (s) 529.47
Current children cumulated vsize (Kb) 37732

[startup+540.049 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8566 0 0 0 53882 62 0 0 25 0 1 0 1785103568 36651008 8364 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 8948 8364 145 145 0 8803 0
[pid=5572] vsize: 35792
Current children cumulated CPU time (s) 539.45
Current children cumulated vsize (Kb) 37916

[startup+550.05 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8624 0 0 0 54881 63 0 0 25 0 1 0 1785103568 36888576 8422 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9006 8422 145 145 0 8861 0
[pid=5572] vsize: 36024
Current children cumulated CPU time (s) 549.45
Current children cumulated vsize (Kb) 38148

[startup+560.051 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8674 0 0 0 55880 64 0 0 25 0 1 0 1785103568 37355520 8472 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9120 8472 145 145 0 8975 0
[pid=5572] vsize: 36480
Current children cumulated CPU time (s) 559.45
Current children cumulated vsize (Kb) 38604

[startup+570.052 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8719 0 0 0 56879 64 0 0 25 0 1 0 1785103568 37539840 8517 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9165 8517 145 145 0 9020 0
[pid=5572] vsize: 36660
Current children cumulated CPU time (s) 569.44
Current children cumulated vsize (Kb) 38784

[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8771 0 0 0 57878 65 0 0 25 0 1 0 1785103568 37744640 8569 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9215 8569 145 145 0 9070 0
[pid=5572] vsize: 36860
Current children cumulated CPU time (s) 579.44
Current children cumulated vsize (Kb) 38984

[startup+590.054 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8814 0 0 0 58876 67 0 0 25 0 1 0 1785103568 37924864 8612 4294967295 134512640 135094434 3221224448 3221223040 134557040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9259 8612 145 145 0 9114 0
[pid=5572] vsize: 37036
Current children cumulated CPU time (s) 589.44
Current children cumulated vsize (Kb) 39160

[startup+600.055 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8863 0 0 0 59875 67 0 0 25 0 1 0 1785103568 38137856 8661 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9311 8661 145 145 0 9166 0
[pid=5572] vsize: 37244
Current children cumulated CPU time (s) 599.43
Current children cumulated vsize (Kb) 39368

[startup+610.056 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8903 0 0 0 60874 68 0 0 25 0 1 0 1785103568 38289408 8701 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9348 8701 145 145 0 9203 0
[pid=5572] vsize: 37392
Current children cumulated CPU time (s) 609.43
Current children cumulated vsize (Kb) 39516

[startup+620.057 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 8950 0 0 0 61873 69 0 0 25 0 1 0 1785103568 38502400 8748 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9400 8748 145 145 0 9255 0
[pid=5572] vsize: 37600
Current children cumulated CPU time (s) 619.43
Current children cumulated vsize (Kb) 39724

[startup+630.058 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9009 0 0 0 62872 69 0 0 25 0 1 0 1785103568 38727680 8807 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9455 8807 145 145 0 9310 0
[pid=5572] vsize: 37820
Current children cumulated CPU time (s) 629.42
Current children cumulated vsize (Kb) 39944

[startup+640.059 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9056 0 0 0 63870 70 0 0 25 0 1 0 1785103568 38916096 8854 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9501 8854 145 145 0 9356 0
[pid=5572] vsize: 38004
Current children cumulated CPU time (s) 639.41
Current children cumulated vsize (Kb) 40128

[startup+650.06 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9099 0 0 0 64870 71 0 0 25 0 1 0 1785103568 39088128 8897 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9543 8897 145 145 0 9398 0
[pid=5572] vsize: 38172
Current children cumulated CPU time (s) 649.42
Current children cumulated vsize (Kb) 40296

[startup+660.061 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9159 0 0 0 65869 72 0 0 25 0 1 0 1785103568 39346176 8957 4294967295 134512640 135094434 3221224448 3221223072 134557596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9606 8957 145 145 0 9461 0
[pid=5572] vsize: 38424
Current children cumulated CPU time (s) 659.42
Current children cumulated vsize (Kb) 40548

[startup+670.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9211 0 0 0 66867 72 0 0 25 0 1 0 1785103568 39542784 9009 4294967295 134512640 135094434 3221224448 3221223076 134557637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9654 9009 145 145 0 9509 0
[pid=5572] vsize: 38616
Current children cumulated CPU time (s) 669.4
Current children cumulated vsize (Kb) 40740

[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9265 0 0 0 67866 73 0 0 25 0 1 0 1785103568 39759872 9063 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9707 9063 145 145 0 9562 0
[pid=5572] vsize: 38828
Current children cumulated CPU time (s) 679.4
Current children cumulated vsize (Kb) 40952

[startup+690.063 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9312 0 0 0 68865 73 0 0 25 0 1 0 1785103568 40009728 9110 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9768 9110 145 145 0 9623 0
[pid=5572] vsize: 39072
Current children cumulated CPU time (s) 689.39
Current children cumulated vsize (Kb) 41196

[startup+700.065 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9365 0 0 0 69864 74 0 0 25 0 1 0 1785103568 40222720 9163 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9820 9163 145 145 0 9675 0
[pid=5572] vsize: 39280
Current children cumulated CPU time (s) 699.39
Current children cumulated vsize (Kb) 41404

[startup+710.066 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9423 0 0 0 70863 75 0 0 25 0 1 0 1785103568 40456192 9221 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9877 9221 145 145 0 9732 0
[pid=5572] vsize: 39508
Current children cumulated CPU time (s) 709.39
Current children cumulated vsize (Kb) 41632

[startup+720.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9475 0 0 0 71861 76 0 0 25 0 1 0 1785103568 40673280 9273 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9930 9273 145 145 0 9785 0
[pid=5572] vsize: 39720
Current children cumulated CPU time (s) 719.38
Current children cumulated vsize (Kb) 41844

[startup+730.067 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9517 0 0 0 72860 76 0 0 25 0 1 0 1785103568 40837120 9315 4294967295 134512640 135094434 3221224448 3221223088 134558269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 9970 9315 145 145 0 9825 0
[pid=5572] vsize: 39880
Current children cumulated CPU time (s) 729.37
Current children cumulated vsize (Kb) 42004

[startup+740.068 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9573 0 0 0 73858 77 0 0 25 0 1 0 1785103568 41058304 9371 4294967295 134512640 135094434 3221224448 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10024 9371 145 145 0 9879 0
[pid=5572] vsize: 40096
Current children cumulated CPU time (s) 739.36
Current children cumulated vsize (Kb) 42220

[startup+750.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9612 0 0 0 74857 79 0 0 25 0 1 0 1785103568 41222144 9410 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10064 9410 145 145 0 9919 0
[pid=5572] vsize: 40256
Current children cumulated CPU time (s) 749.37
Current children cumulated vsize (Kb) 42380

[startup+760.07 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9665 0 0 0 75855 80 0 0 25 0 1 0 1785103568 41431040 9463 4294967295 134512640 135094434 3221224448 3221223100 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10115 9463 145 145 0 9970 0
[pid=5572] vsize: 40460
Current children cumulated CPU time (s) 759.36
Current children cumulated vsize (Kb) 42584

[startup+770.071 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9724 0 0 0 76853 81 0 0 25 0 1 0 1785103568 41668608 9522 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10173 9522 145 145 0 10028 0
[pid=5572] vsize: 40692
Current children cumulated CPU time (s) 769.35
Current children cumulated vsize (Kb) 42816

[startup+780.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9773 0 0 0 77852 81 0 0 25 0 1 0 1785103568 41861120 9571 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10220 9571 145 145 0 10075 0
[pid=5572] vsize: 40880
Current children cumulated CPU time (s) 779.34
Current children cumulated vsize (Kb) 43004

[startup+790.073 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9823 0 0 0 78851 82 0 0 25 0 1 0 1785103568 42086400 9621 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10275 9621 145 145 0 10130 0
[pid=5572] vsize: 41100
Current children cumulated CPU time (s) 789.34
Current children cumulated vsize (Kb) 43224

[startup+800.075 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9871 0 0 0 79850 83 0 0 25 0 1 0 1785103568 42274816 9669 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10321 9669 145 145 0 10176 0
[pid=5572] vsize: 41284
Current children cumulated CPU time (s) 799.34
Current children cumulated vsize (Kb) 43408

[startup+810.077 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 9937 0 0 0 80849 83 0 0 25 0 1 0 1785103568 42573824 9735 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10394 9735 145 145 0 10249 0
[pid=5572] vsize: 41576
Current children cumulated CPU time (s) 809.33
Current children cumulated vsize (Kb) 43700

[startup+820.077 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10001 0 0 0 81848 84 0 0 25 0 1 0 1785103568 42901504 9799 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10474 9799 145 145 0 10329 0
[pid=5572] vsize: 41896
Current children cumulated CPU time (s) 819.33
Current children cumulated vsize (Kb) 44020

[startup+830.079 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10057 0 0 0 82847 85 0 0 25 0 1 0 1785103568 43171840 9855 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10540 9855 145 145 0 10395 0
[pid=5572] vsize: 42160
Current children cumulated CPU time (s) 829.33
Current children cumulated vsize (Kb) 44284

[startup+840.08 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10088 0 0 0 83847 85 0 0 25 0 1 0 1785103568 43302912 9886 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10572 9886 145 145 0 10427 0
[pid=5572] vsize: 42288
Current children cumulated CPU time (s) 839.33
Current children cumulated vsize (Kb) 44412

[startup+850.081 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10119 0 0 0 84846 86 0 0 25 0 1 0 1785103568 43421696 9917 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/5572/statm): 10601 9917 145 145 0 10456 0
[pid=5572] vsize: 42404
Current children cumulated CPU time (s) 849.33
Current children cumulated vsize (Kb) 44528

[startup+860.082 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10154 0 0 0 85845 86 0 0 25 0 1 0 1785103568 43560960 9952 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 10635 9952 145 145 0 10490 0
[pid=5572] vsize: 42540
Current children cumulated CPU time (s) 859.32
Current children cumulated vsize (Kb) 44664

[startup+870.083 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10199 0 0 0 86844 87 0 0 25 0 1 0 1785103568 43741184 9997 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 10679 9997 145 145 0 10534 0
[pid=5572] vsize: 42716
Current children cumulated CPU time (s) 869.32
Current children cumulated vsize (Kb) 44840

[startup+880.083 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10244 0 0 0 87843 87 0 0 25 0 1 0 1785103568 43917312 10042 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 10722 10042 145 145 0 10577 0
[pid=5572] vsize: 42888
Current children cumulated CPU time (s) 879.31
Current children cumulated vsize (Kb) 45012

[startup+890.084 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10283 0 0 0 88842 88 0 0 25 0 1 0 1785103568 44077056 10081 4294967295 134512640 135094434 3221224448 3221223136 134554733 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 10761 10081 145 145 0 10616 0
[pid=5572] vsize: 43044
Current children cumulated CPU time (s) 889.31
Current children cumulated vsize (Kb) 45168

[startup+900.085 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10325 0 0 0 89842 88 0 0 25 0 1 0 1785103568 44244992 10123 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 10802 10123 145 145 0 10657 0
[pid=5572] vsize: 43208
Current children cumulated CPU time (s) 899.31
Current children cumulated vsize (Kb) 45332

[startup+910.085 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10374 0 0 0 90841 89 0 0 25 0 1 0 1785103568 44421120 10172 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 10845 10172 145 145 0 10700 0
[pid=5572] vsize: 43380
Current children cumulated CPU time (s) 909.31
Current children cumulated vsize (Kb) 45504

[startup+920.086 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10413 0 0 0 91840 89 0 0 25 0 1 0 1785103568 44576768 10211 4294967295 134512640 135094434 3221224448 3221223040 134557522 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 10883 10211 145 145 0 10738 0
[pid=5572] vsize: 43532
Current children cumulated CPU time (s) 919.3
Current children cumulated vsize (Kb) 45656

[startup+930.087 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10449 0 0 0 92840 89 0 0 25 0 1 0 1785103568 44728320 10247 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 10920 10247 145 145 0 10775 0
[pid=5572] vsize: 43680
Current children cumulated CPU time (s) 929.3
Current children cumulated vsize (Kb) 45804

[startup+940.087 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10482 0 0 0 93839 90 0 0 25 0 1 0 1785103568 44859392 10280 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 10952 10280 145 145 0 10807 0
[pid=5572] vsize: 43808
Current children cumulated CPU time (s) 939.3
Current children cumulated vsize (Kb) 45932

[startup+950.089 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10519 0 0 0 94839 91 0 0 25 0 1 0 1785103568 45006848 10317 4294967295 134512640 135094434 3221224448 3221223072 134557587 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 10988 10317 145 145 0 10843 0
[pid=5572] vsize: 43952
Current children cumulated CPU time (s) 949.31
Current children cumulated vsize (Kb) 46076

[startup+960.089 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10557 0 0 0 95838 91 0 0 25 0 1 0 1785103568 45158400 10355 4294967295 134512640 135094434 3221224448 3221223040 134556773 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11025 10355 145 145 0 10880 0
[pid=5572] vsize: 44100
Current children cumulated CPU time (s) 959.3
Current children cumulated vsize (Kb) 46224

[startup+970.089 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10599 0 0 0 96838 91 0 0 25 0 1 0 1785103568 45322240 10397 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11065 10397 145 145 0 10920 0
[pid=5572] vsize: 44260
Current children cumulated CPU time (s) 969.3
Current children cumulated vsize (Kb) 46384

[startup+980.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10632 0 0 0 97837 91 0 0 25 0 1 0 1785103568 45457408 10430 4294967295 134512640 135094434 3221224448 3221223072 134557737 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11098 10430 145 145 0 10953 0
[pid=5572] vsize: 44392
Current children cumulated CPU time (s) 979.29
Current children cumulated vsize (Kb) 46516

[startup+990.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10701 0 0 0 98836 92 0 0 25 0 1 0 1785103568 45785088 10499 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11178 10499 145 145 0 11033 0
[pid=5572] vsize: 44712
Current children cumulated CPU time (s) 989.29
Current children cumulated vsize (Kb) 46836

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10767 0 0 0 99836 93 0 0 25 0 1 0 1785103568 46067712 10565 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11247 10565 145 145 0 11102 0
[pid=5572] vsize: 44988
Current children cumulated CPU time (s) 999.3
Current children cumulated vsize (Kb) 47112

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10811 0 0 0 100835 93 0 0 25 0 1 0 1785103568 46239744 10609 4294967295 134512640 135094434 3221224448 3221223136 134554788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11289 10609 145 145 0 11144 0
[pid=5572] vsize: 45156
Current children cumulated CPU time (s) 1009.29
Current children cumulated vsize (Kb) 47280

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10851 0 0 0 101835 93 0 0 25 0 1 0 1785103568 46403584 10649 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11329 10649 145 145 0 11184 0
[pid=5572] vsize: 45316
Current children cumulated CPU time (s) 1019.29
Current children cumulated vsize (Kb) 47440

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10890 0 0 0 102834 94 0 0 25 0 1 0 1785103568 46559232 10688 4294967295 134512640 135094434 3221224448 3221223136 134554705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11367 10688 145 145 0 11222 0
[pid=5572] vsize: 45468
Current children cumulated CPU time (s) 1029.29
Current children cumulated vsize (Kb) 47592

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10932 0 0 0 103833 95 0 0 25 0 1 0 1785103568 46731264 10730 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11409 10730 145 145 0 11264 0
[pid=5572] vsize: 45636
Current children cumulated CPU time (s) 1039.29
Current children cumulated vsize (Kb) 47760

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 10976 0 0 0 104832 95 0 0 25 0 1 0 1785103568 46915584 10774 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11454 10774 145 145 0 11309 0
[pid=5572] vsize: 45816
Current children cumulated CPU time (s) 1049.28
Current children cumulated vsize (Kb) 47940

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11028 0 0 0 105832 95 0 0 25 0 1 0 1785103568 47165440 10826 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11515 10826 145 145 0 11370 0
[pid=5572] vsize: 46060
Current children cumulated CPU time (s) 1059.28
Current children cumulated vsize (Kb) 48184

[startup+1070.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11061 0 0 0 106831 95 0 0 25 0 1 0 1785103568 47259648 10859 4294967295 134512640 135094434 3221224448 3221223040 134556864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11538 10859 145 145 0 11393 0
[pid=5572] vsize: 46152
Current children cumulated CPU time (s) 1069.27
Current children cumulated vsize (Kb) 48276

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11094 0 0 0 107831 96 0 0 25 0 1 0 1785103568 47448064 10892 4294967295 134512640 135094434 3221224448 3221223120 134555953 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11584 10892 145 145 0 11439 0
[pid=5572] vsize: 46336
Current children cumulated CPU time (s) 1079.28
Current children cumulated vsize (Kb) 48460

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11134 0 0 0 108831 96 0 0 25 0 1 0 1785103568 47611904 10932 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11624 10932 145 145 0 11479 0
[pid=5572] vsize: 46496
Current children cumulated CPU time (s) 1089.28
Current children cumulated vsize (Kb) 48620

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11172 0 0 0 109830 96 0 0 25 0 1 0 1785103568 47755264 10970 4294967295 134512640 135094434 3221224448 3221223104 134558295 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11659 10970 145 145 0 11514 0
[pid=5572] vsize: 46636
Current children cumulated CPU time (s) 1099.27
Current children cumulated vsize (Kb) 48760

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11207 0 0 0 110830 96 0 0 25 0 1 0 1785103568 47898624 11005 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11694 11005 145 145 0 11549 0
[pid=5572] vsize: 46776
Current children cumulated CPU time (s) 1109.27
Current children cumulated vsize (Kb) 48900

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11245 0 0 0 111829 97 0 0 25 0 1 0 1785103568 48050176 11043 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11731 11043 145 145 0 11586 0
[pid=5572] vsize: 46924
Current children cumulated CPU time (s) 1119.27
Current children cumulated vsize (Kb) 49048

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11302 0 0 0 112829 97 0 0 25 0 1 0 1785103568 48398336 11100 4294967295 134512640 135094434 3221224448 3221223040 134556914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11816 11100 145 145 0 11671 0
[pid=5572] vsize: 47264
Current children cumulated CPU time (s) 1129.27
Current children cumulated vsize (Kb) 49388

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11332 0 0 0 113829 97 0 0 25 0 1 0 1785103568 48590848 11130 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11863 11130 145 145 0 11718 0
[pid=5572] vsize: 47452
Current children cumulated CPU time (s) 1139.27
Current children cumulated vsize (Kb) 49576

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11367 0 0 0 114829 97 0 0 25 0 1 0 1785103568 48754688 11165 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11903 11165 145 145 0 11758 0
[pid=5572] vsize: 47612
Current children cumulated CPU time (s) 1149.27
Current children cumulated vsize (Kb) 49736

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11403 0 0 0 115829 97 0 0 25 0 1 0 1785103568 48889856 11201 4294967295 134512640 135094434 3221224448 3221223040 134556894 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11936 11201 145 145 0 11791 0
[pid=5572] vsize: 47744
Current children cumulated CPU time (s) 1159.27
Current children cumulated vsize (Kb) 49868

[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11439 0 0 0 116828 98 0 0 25 0 1 0 1785103568 49025024 11237 4294967295 134512640 135094434 3221224448 3221223136 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 11969 11237 145 145 0 11824 0
[pid=5572] vsize: 47876
Current children cumulated CPU time (s) 1169.27
Current children cumulated vsize (Kb) 50000

[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11477 0 0 0 117828 98 0 0 25 0 1 0 1785103568 49168384 11275 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 12004 11275 145 145 0 11859 0
[pid=5572] vsize: 48016
Current children cumulated CPU time (s) 1179.27
Current children cumulated vsize (Kb) 50140

[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11519 0 0 0 118827 98 0 0 25 0 1 0 1785103568 49369088 11317 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 12053 11317 145 145 0 11908 0
[pid=5572] vsize: 48212
Current children cumulated CPU time (s) 1189.26
Current children cumulated vsize (Kb) 50336

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11557 0 0 0 119827 99 0 0 25 0 1 0 1785103568 49528832 11355 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 12092 11355 145 145 0 11947 0
[pid=5572] vsize: 48368
Current children cumulated CPU time (s) 1199.27
Current children cumulated vsize (Kb) 50492

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11593 0 0 0 120826 99 0 0 25 0 1 0 1785103568 49668096 11391 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 12126 11391 145 145 0 11981 0
[pid=5572] vsize: 48504
Current children cumulated CPU time (s) 1209.26
Current children cumulated vsize (Kb) 50628



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.11 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 5572
Raw data (/proc/5568/stat): 5568 (minisat+_script) S 5567 5568 1333 0 -1 0 288 239 0 0 0 1 0 0 21 0 1 0 1785103563 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/5568/statm): 531 226 485 147 0 384 0
[pid=5568] vsize: 2124
Raw data (/proc/5572/stat): 5572 (minisat+_64-bit) R 5568 5568 1333 0 -1 0 11593 0 0 0 120826 99 0 0 25 0 1 0 1785103568 49668096 11391 4294967295 134512640 135094434 3221224448 3221223096 134558258 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/5572/statm): 12126 11391 145 145 0 11981 0
[pid=5572] vsize: 48504
Current children cumulated CPU time (s) 1209.26
Current children cumulated vsize (Kb) 50628

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

Child status: 10
Real time (s): 1210.13
CPU time (s): 1209.28
CPU user time (s): 1208.26
CPU system time (s): 1.01984
CPU usage (%): 99.9298
Max. virtual memory (cumulated for all children) (Kb): 50628

Verifier Data

ERROR: no interpretation found !