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/primes-dimacs-cnf/normalized-par32-4-c.opb
MD5SUM3d2c3109962e8068c6ff1a393a02942b
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function 2666
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 2666
Number of bits of the sum of numbers in the objective function 12
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 2666
Number of bits of the biggest sum of numbers12
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2666
Total number of constraints6659
Number of constraints which are clauses6659
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 constraint3

Trace number 1539

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        923872 kB
Buffers:         34500 kB
Cached:          52600 kB
SwapCached:        960 kB
Active:          64436 kB
Inactive:        25316 kB
HighTotal:      131008 kB
HighFree:        76076 kB
LowTotal:       903652 kB
LowFree:        847796 kB
SwapTotal:     2097136 kB
SwapFree:      2095628 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5692 kB
Slab:            15540 kB
Committed_AS:    72324 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 15:51:21 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 2539 7 1200.16 0

Solver Data

c Parsing PB file...
c Converting 6659 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 |    6659    18272 |    2219       0        0     nan |  0.000 % |
c |       102 |    6659    18272 |    2440     102     4036    39.6 |  0.003 % |
c |       252 |    6659    18272 |    2684     252     9977    39.6 |  0.000 % |
c |       478 |    6659    18272 |    2953     478    18267    38.2 |  0.000 % |
c |       817 |    6659    18272 |    3248     817    33443    40.9 |  0.000 % |
c |      1324 |    6659    18272 |    3573    1324    50708    38.3 |  0.000 % |
c |      2085 |    6659    18272 |    3931    2085    75530    36.2 |  0.000 % |
c |      3224 |    6659    18272 |    4324    3224   113144    35.1 |  0.000 % |
c |      4934 |    6659    18272 |    4756    2697    80855    30.0 |  0.000 % |
c |      7496 |    6659    18272 |    5232    2741    76314    27.8 |  0.000 % |
c |     11342 |    6659    18272 |    5755    3932    98780    25.1 |  0.000 % |
c |     17108 |    6659    18272 |    6331    3848    85273    22.2 |  0.000 % |
c |     25757 |    6659    18272 |    6964    6011   141979    23.6 |  0.000 % |
c |     38731 |    6659    18272 |    7660    4835   104809    21.7 |  0.000 % |
c |     58192 |    6659    18272 |    8426    4891   115405    23.6 |  0.000 % |
c |     87384 |    6659    18272 |    9269    8363   183816    22.0 |  0.000 % |
c |    131173 |    6652    18256 |   10196    5291   107425    20.3 |  0.075 % |
c |    196857 |    6652    18256 |   11215    9133   189013    20.7 |  0.075 % |
c |    295384 |    6652    18256 |   12337    5895   132460    22.5 |  0.075 % |
c |    443174 |    6652    18256 |   13571   10715   243644    22.7 |  0.075 % |
c |    664857 |    6652    18256 |   14928    6866   130708    19.0 |  0.075 % |
c |    997383 |    6652    18256 |   16421    8655   160498    18.5 |  0.075 % |

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/14271/stat): 14271 (minisat+_script) R 14270 14271 6847 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1784112042 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/14271/statm): 174 3 169 147 0 27 0
[pid=14271] 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=14272
New process pid=14273
New process pid=14274
execve syscall for /bin/sed executable
One traced child (pid=14273) 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=14274) exited with status: 0
One traced child (pid=14272) exited with status: 0
New process pid=14275
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc4/normalized-par32-4-c.opb

[startup+10.0034 s]
Raw data (loadavg): 0.93 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 746 0 0 0 989 3 0 0 25 0 1 0 1784112047 3354624 733 4294967295 134512640 135094434 3221224448 3221223072 134562048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14275/statm): 819 733 145 145 0 674 0
[pid=14275] vsize: 3276
Current children cumulated CPU time (s) 9.93
Current children cumulated vsize (Kb) 5400

[startup+20.0052 s]
Raw data (loadavg): 0.94 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 746 0 0 0 1989 3 0 0 25 0 1 0 1784112047 3354624 733 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 819 733 145 145 0 674 0
[pid=14275] vsize: 3276
Current children cumulated CPU time (s) 19.93
Current children cumulated vsize (Kb) 5400

[startup+30.0061 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 746 0 0 0 2988 3 0 0 25 0 1 0 1784112047 3354624 733 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 819 733 145 145 0 674 0
[pid=14275] vsize: 3276
Current children cumulated CPU time (s) 29.92
Current children cumulated vsize (Kb) 5400

[startup+40.0069 s]
Raw data (loadavg): 0.95 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 746 0 0 0 3989 3 0 0 25 0 1 0 1784112047 3354624 733 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 819 733 145 145 0 674 0
[pid=14275] vsize: 3276
Current children cumulated CPU time (s) 39.93
Current children cumulated vsize (Kb) 5400

[startup+50.0078 s]
Raw data (loadavg): 0.96 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 746 0 0 0 4989 3 0 0 25 0 1 0 1784112047 3354624 733 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 819 733 145 145 0 674 0
[pid=14275] vsize: 3276
Current children cumulated CPU time (s) 49.93
Current children cumulated vsize (Kb) 5400

[startup+60.0087 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 772 0 0 0 5989 4 0 0 25 0 1 0 1784112047 3485696 759 4294967295 134512640 135094434 3221224448 3221223104 134558156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 851 759 145 145 0 706 0
[pid=14275] vsize: 3404
Current children cumulated CPU time (s) 59.94
Current children cumulated vsize (Kb) 5528

[startup+70.0105 s]
Raw data (loadavg): 0.97 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 776 0 0 0 6989 4 0 0 25 0 1 0 1784112047 3502080 763 4294967295 134512640 135094434 3221224448 3221223040 134557372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 855 763 145 145 0 710 0
[pid=14275] vsize: 3420
Current children cumulated CPU time (s) 69.94
Current children cumulated vsize (Kb) 5544

[startup+80.0114 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 782 0 0 0 7989 4 0 0 25 0 1 0 1784112047 3551232 769 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 867 769 145 145 0 722 0
[pid=14275] vsize: 3468
Current children cumulated CPU time (s) 79.94
Current children cumulated vsize (Kb) 5592

[startup+90.0112 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 799 0 0 0 8989 4 0 0 25 0 1 0 1784112047 3608576 786 4294967295 134512640 135094434 3221224448 3221223120 134556257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 881 786 145 145 0 736 0
[pid=14275] vsize: 3524
Current children cumulated CPU time (s) 89.94
Current children cumulated vsize (Kb) 5648

[startup+100.012 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 817 0 0 0 9989 4 0 0 25 0 1 0 1784112047 3686400 804 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 900 804 145 145 0 755 0
[pid=14275] vsize: 3600
Current children cumulated CPU time (s) 99.94
Current children cumulated vsize (Kb) 5724

[startup+110.013 s]
Raw data (loadavg): 0.98 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 821 0 0 0 10990 4 0 0 25 0 1 0 1784112047 3702784 808 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 904 808 145 145 0 759 0
[pid=14275] vsize: 3616
Current children cumulated CPU time (s) 109.95
Current children cumulated vsize (Kb) 5740

[startup+120.015 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 825 0 0 0 11990 4 0 0 25 0 1 0 1784112047 3719168 812 4294967295 134512640 135094434 3221224448 3221223072 134562085 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 908 812 145 145 0 763 0
[pid=14275] vsize: 3632
Current children cumulated CPU time (s) 119.95
Current children cumulated vsize (Kb) 5756

[startup+130.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 825 0 0 0 12990 4 0 0 25 0 1 0 1784112047 3719168 812 4294967295 134512640 135094434 3221224448 3221223104 134558405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 908 812 145 145 0 763 0
[pid=14275] vsize: 3632
Current children cumulated CPU time (s) 129.95
Current children cumulated vsize (Kb) 5756

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 851 0 0 0 13989 4 0 0 25 0 1 0 1784112047 3829760 838 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 935 838 145 145 0 790 0
[pid=14275] vsize: 3740
Current children cumulated CPU time (s) 139.94
Current children cumulated vsize (Kb) 5864

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 855 0 0 0 14989 4 0 0 25 0 1 0 1784112047 3846144 842 4294967295 134512640 135094434 3221224448 3221223120 134555583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 939 842 145 145 0 794 0
[pid=14275] vsize: 3756
Current children cumulated CPU time (s) 149.94
Current children cumulated vsize (Kb) 5880

[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 858 0 0 0 15990 4 0 0 25 0 1 0 1784112047 3878912 845 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 947 845 145 145 0 802 0
[pid=14275] vsize: 3788
Current children cumulated CPU time (s) 159.95
Current children cumulated vsize (Kb) 5912

[startup+170.017 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 867 0 0 0 16990 4 0 0 25 0 1 0 1784112047 3911680 854 4294967295 134512640 135094434 3221224448 3221223076 134557564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 955 854 145 145 0 810 0
[pid=14275] vsize: 3820
Current children cumulated CPU time (s) 169.95
Current children cumulated vsize (Kb) 5944

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 874 0 0 0 17990 4 0 0 25 0 1 0 1784112047 3944448 861 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 963 861 145 145 0 818 0
[pid=14275] vsize: 3852
Current children cumulated CPU time (s) 179.95
Current children cumulated vsize (Kb) 5976

[startup+190.019 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 884 0 0 0 18990 4 0 0 25 0 1 0 1784112047 3993600 871 4294967295 134512640 135094434 3221224448 3221223012 134562166 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 975 871 145 145 0 830 0
[pid=14275] vsize: 3900
Current children cumulated CPU time (s) 189.95
Current children cumulated vsize (Kb) 6024

[startup+200.02 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 884 0 0 0 19990 4 0 0 25 0 1 0 1784112047 3993600 871 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 975 871 145 145 0 830 0
[pid=14275] vsize: 3900
Current children cumulated CPU time (s) 199.95
Current children cumulated vsize (Kb) 6024

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 891 0 0 0 20991 4 0 0 25 0 1 0 1784112047 4018176 878 4294967295 134512640 135094434 3221224448 3221222976 134783130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 981 878 145 145 0 836 0
[pid=14275] vsize: 3924
Current children cumulated CPU time (s) 209.96
Current children cumulated vsize (Kb) 6048

[startup+220.021 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 937 0 0 0 21990 5 0 0 25 0 1 0 1784112047 4198400 924 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1025 924 145 145 0 880 0
[pid=14275] vsize: 4100
Current children cumulated CPU time (s) 219.96
Current children cumulated vsize (Kb) 6224

[startup+230.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 942 0 0 0 22990 5 0 0 25 0 1 0 1784112047 4231168 929 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1033 929 145 145 0 888 0
[pid=14275] vsize: 4132
Current children cumulated CPU time (s) 229.96
Current children cumulated vsize (Kb) 6256

[startup+240.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 942 0 0 0 23990 5 0 0 25 0 1 0 1784112047 4231168 929 4294967295 134512640 135094434 3221224448 3221223120 134556415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1033 929 145 145 0 888 0
[pid=14275] vsize: 4132
Current children cumulated CPU time (s) 239.96
Current children cumulated vsize (Kb) 6256

[startup+250.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 942 0 0 0 24990 5 0 0 25 0 1 0 1784112047 4231168 929 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1033 929 145 145 0 888 0
[pid=14275] vsize: 4132
Current children cumulated CPU time (s) 249.96
Current children cumulated vsize (Kb) 6256

[startup+260.025 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 942 0 0 0 25991 5 0 0 25 0 1 0 1784112047 4231168 929 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1033 929 145 145 0 888 0
[pid=14275] vsize: 4132
Current children cumulated CPU time (s) 259.97
Current children cumulated vsize (Kb) 6256

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 942 0 0 0 26990 5 0 0 25 0 1 0 1784112047 4231168 929 4294967295 134512640 135094434 3221224448 3221223104 134557792 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1033 929 145 145 0 888 0
[pid=14275] vsize: 4132
Current children cumulated CPU time (s) 269.96
Current children cumulated vsize (Kb) 6256

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 943 0 0 0 27990 5 0 0 25 0 1 0 1784112047 4235264 930 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1034 930 145 145 0 889 0
[pid=14275] vsize: 4136
Current children cumulated CPU time (s) 279.96
Current children cumulated vsize (Kb) 6260

[startup+290.027 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 951 0 0 0 28991 5 0 0 25 0 1 0 1784112047 4280320 938 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1045 938 145 145 0 900 0
[pid=14275] vsize: 4180
Current children cumulated CPU time (s) 289.97
Current children cumulated vsize (Kb) 6304

[startup+300.028 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 951 0 0 0 29991 5 0 0 25 0 1 0 1784112047 4280320 938 4294967295 134512640 135094434 3221224448 3221223040 134551434 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1045 938 145 145 0 900 0
[pid=14275] vsize: 4180
Current children cumulated CPU time (s) 299.97
Current children cumulated vsize (Kb) 6304

[startup+310.029 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 954 0 0 0 30991 5 0 0 25 0 1 0 1784112047 4296704 941 4294967295 134512640 135094434 3221224448 3221223112 134562037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1049 941 145 145 0 904 0
[pid=14275] vsize: 4196
Current children cumulated CPU time (s) 309.97
Current children cumulated vsize (Kb) 6320

[startup+320.03 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 955 0 0 0 31991 5 0 0 25 0 1 0 1784112047 4296704 942 4294967295 134512640 135094434 3221224448 3221223104 134558240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1049 942 145 145 0 904 0
[pid=14275] vsize: 4196
Current children cumulated CPU time (s) 319.97
Current children cumulated vsize (Kb) 6320

[startup+330.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 993 0 0 0 32990 6 0 0 25 0 1 0 1784112047 4452352 980 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1087 980 145 145 0 942 0
[pid=14275] vsize: 4348
Current children cumulated CPU time (s) 329.97
Current children cumulated vsize (Kb) 6472

[startup+340.031 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1006 0 0 0 33990 6 0 0 25 0 1 0 1784112047 4501504 993 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1099 993 145 145 0 954 0
[pid=14275] vsize: 4396
Current children cumulated CPU time (s) 339.97
Current children cumulated vsize (Kb) 6520

[startup+350.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1029 0 0 0 34990 6 0 0 25 0 1 0 1784112047 4608000 1016 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1125 1016 145 145 0 980 0
[pid=14275] vsize: 4500
Current children cumulated CPU time (s) 349.97
Current children cumulated vsize (Kb) 6624

[startup+360.032 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1036 0 0 0 35990 6 0 0 25 0 1 0 1784112047 4648960 1023 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1135 1023 145 145 0 990 0
[pid=14275] vsize: 4540
Current children cumulated CPU time (s) 359.97
Current children cumulated vsize (Kb) 6664

[startup+370.033 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1037 0 0 0 36991 6 0 0 25 0 1 0 1784112047 4648960 1024 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1135 1024 145 145 0 990 0
[pid=14275] vsize: 4540
Current children cumulated CPU time (s) 369.98
Current children cumulated vsize (Kb) 6664

[startup+380.034 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1043 0 0 0 37991 6 0 0 25 0 1 0 1784112047 4681728 1030 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1143 1030 145 145 0 998 0
[pid=14275] vsize: 4572
Current children cumulated CPU time (s) 379.98
Current children cumulated vsize (Kb) 6696

[startup+390.035 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1044 0 0 0 38991 6 0 0 25 0 1 0 1784112047 4681728 1031 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1143 1031 145 145 0 998 0
[pid=14275] vsize: 4572
Current children cumulated CPU time (s) 389.98
Current children cumulated vsize (Kb) 6696

[startup+400.036 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1044 0 0 0 39991 6 0 0 25 0 1 0 1784112047 4681728 1031 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1143 1031 145 145 0 998 0
[pid=14275] vsize: 4572
Current children cumulated CPU time (s) 399.98
Current children cumulated vsize (Kb) 6696

[startup+410.037 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1045 0 0 0 40992 6 0 0 25 0 1 0 1784112047 4681728 1032 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1143 1032 145 145 0 998 0
[pid=14275] vsize: 4572
Current children cumulated CPU time (s) 409.99
Current children cumulated vsize (Kb) 6696

[startup+420.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1051 0 0 0 41992 6 0 0 25 0 1 0 1784112047 4714496 1038 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1151 1038 145 145 0 1006 0
[pid=14275] vsize: 4604
Current children cumulated CPU time (s) 419.99
Current children cumulated vsize (Kb) 6728

[startup+430.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1051 0 0 0 42992 6 0 0 25 0 1 0 1784112047 4714496 1038 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1151 1038 145 145 0 1006 0
[pid=14275] vsize: 4604
Current children cumulated CPU time (s) 429.99
Current children cumulated vsize (Kb) 6728

[startup+440.038 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1051 0 0 0 43992 6 0 0 25 0 1 0 1784112047 4714496 1038 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1151 1038 145 145 0 1006 0
[pid=14275] vsize: 4604
Current children cumulated CPU time (s) 439.99
Current children cumulated vsize (Kb) 6728

[startup+450.039 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1051 0 0 0 44992 6 0 0 25 0 1 0 1784112047 4714496 1038 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1151 1038 145 145 0 1006 0
[pid=14275] vsize: 4604
Current children cumulated CPU time (s) 449.99
Current children cumulated vsize (Kb) 6728

[startup+460.04 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1057 0 0 0 45992 6 0 0 25 0 1 0 1784112047 4747264 1044 4294967295 134512640 135094434 3221224448 3221223120 134555568 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1159 1044 145 145 0 1014 0
[pid=14275] vsize: 4636
Current children cumulated CPU time (s) 459.99
Current children cumulated vsize (Kb) 6760

[startup+470.041 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1064 0 0 0 46992 6 0 0 25 0 1 0 1784112047 4780032 1051 4294967295 134512640 135094434 3221224448 3221223120 134556033 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1167 1051 145 145 0 1022 0
[pid=14275] vsize: 4668
Current children cumulated CPU time (s) 469.99
Current children cumulated vsize (Kb) 6792

[startup+480.042 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1064 0 0 0 47992 6 0 0 25 0 1 0 1784112047 4780032 1051 4294967295 134512640 135094434 3221224448 3221222976 134780546 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1167 1051 145 145 0 1022 0
[pid=14275] vsize: 4668
Current children cumulated CPU time (s) 479.99
Current children cumulated vsize (Kb) 6792

[startup+490.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1065 0 0 0 48992 6 0 0 25 0 1 0 1784112047 4780032 1052 4294967295 134512640 135094434 3221224448 3221223120 134555274 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1167 1052 145 145 0 1022 0
[pid=14275] vsize: 4668
Current children cumulated CPU time (s) 489.99
Current children cumulated vsize (Kb) 6792

[startup+500.043 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1065 0 0 0 49992 6 0 0 25 0 1 0 1784112047 4780032 1052 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1167 1052 145 145 0 1022 0
[pid=14275] vsize: 4668
Current children cumulated CPU time (s) 499.99
Current children cumulated vsize (Kb) 6792

[startup+510.044 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1065 0 0 0 50993 6 0 0 25 0 1 0 1784112047 4780032 1052 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1167 1052 145 145 0 1022 0
[pid=14275] vsize: 4668
Current children cumulated CPU time (s) 510
Current children cumulated vsize (Kb) 6792

[startup+520.045 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1066 0 0 0 51993 6 0 0 25 0 1 0 1784112047 4780032 1053 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1167 1053 145 145 0 1022 0
[pid=14275] vsize: 4668
Current children cumulated CPU time (s) 520
Current children cumulated vsize (Kb) 6792

[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1067 0 0 0 52993 6 0 0 25 0 1 0 1784112047 4780032 1054 4294967295 134512640 135094434 3221224448 3221223120 134556275 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1167 1054 145 145 0 1022 0
[pid=14275] vsize: 4668
Current children cumulated CPU time (s) 530
Current children cumulated vsize (Kb) 6792

[startup+540.046 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1067 0 0 0 53993 6 0 0 25 0 1 0 1784112047 4780032 1054 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1167 1054 145 145 0 1022 0
[pid=14275] vsize: 4668
Current children cumulated CPU time (s) 540
Current children cumulated vsize (Kb) 6792

[startup+550.047 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1073 0 0 0 54994 6 0 0 25 0 1 0 1784112047 4812800 1060 4294967295 134512640 135094434 3221224448 3221223104 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1175 1060 145 145 0 1030 0
[pid=14275] vsize: 4700
Current children cumulated CPU time (s) 550.01
Current children cumulated vsize (Kb) 6824

[startup+560.048 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1073 0 0 0 55994 6 0 0 25 0 1 0 1784112047 4812800 1060 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1175 1060 145 145 0 1030 0
[pid=14275] vsize: 4700
Current children cumulated CPU time (s) 560.01
Current children cumulated vsize (Kb) 6824

[startup+570.049 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1079 0 0 0 56994 6 0 0 25 0 1 0 1784112047 4845568 1066 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1183 1066 145 145 0 1038 0
[pid=14275] vsize: 4732
Current children cumulated CPU time (s) 570.01
Current children cumulated vsize (Kb) 6856

[startup+580.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1079 0 0 0 57994 6 0 0 25 0 1 0 1784112047 4845568 1066 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1183 1066 145 145 0 1038 0
[pid=14275] vsize: 4732
Current children cumulated CPU time (s) 580.01
Current children cumulated vsize (Kb) 6856

[startup+590.05 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1086 0 0 0 58994 6 0 0 25 0 1 0 1784112047 4878336 1073 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1191 1073 145 145 0 1046 0
[pid=14275] vsize: 4764
Current children cumulated CPU time (s) 590.01
Current children cumulated vsize (Kb) 6888

[startup+600.051 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1086 0 0 0 59995 6 0 0 25 0 1 0 1784112047 4878336 1073 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1191 1073 145 145 0 1046 0
[pid=14275] vsize: 4764
Current children cumulated CPU time (s) 600.02
Current children cumulated vsize (Kb) 6888

[startup+610.052 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1092 0 0 0 60995 6 0 0 25 0 1 0 1784112047 4911104 1079 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1199 1079 145 145 0 1054 0
[pid=14275] vsize: 4796
Current children cumulated CPU time (s) 610.02
Current children cumulated vsize (Kb) 6920

[startup+620.053 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1093 0 0 0 61995 6 0 0 25 0 1 0 1784112047 4911104 1080 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1199 1080 145 145 0 1054 0
[pid=14275] vsize: 4796
Current children cumulated CPU time (s) 620.02
Current children cumulated vsize (Kb) 6920

[startup+630.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1093 0 0 0 62995 6 0 0 25 0 1 0 1784112047 4911104 1080 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1199 1080 145 145 0 1054 0
[pid=14275] vsize: 4796
Current children cumulated CPU time (s) 630.02
Current children cumulated vsize (Kb) 6920

[startup+640.054 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1093 0 0 0 63995 7 0 0 25 0 1 0 1784112047 4911104 1080 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1199 1080 145 145 0 1054 0
[pid=14275] vsize: 4796
Current children cumulated CPU time (s) 640.03
Current children cumulated vsize (Kb) 6920

[startup+650.055 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1093 0 0 0 64996 7 0 0 25 0 1 0 1784112047 4911104 1080 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1199 1080 145 145 0 1054 0
[pid=14275] vsize: 4796
Current children cumulated CPU time (s) 650.04
Current children cumulated vsize (Kb) 6920

[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1100 0 0 0 65996 7 0 0 25 0 1 0 1784112047 4943872 1087 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1207 1087 145 145 0 1062 0
[pid=14275] vsize: 4828
Current children cumulated CPU time (s) 660.04
Current children cumulated vsize (Kb) 6952

[startup+670.058 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1100 0 0 0 66996 7 0 0 25 0 1 0 1784112047 4943872 1087 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1207 1087 145 145 0 1062 0
[pid=14275] vsize: 4828
Current children cumulated CPU time (s) 670.04
Current children cumulated vsize (Kb) 6952

[startup+680.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 67997 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0
[pid=14275] vsize: 4860
Current children cumulated CPU time (s) 680.05
Current children cumulated vsize (Kb) 6984

[startup+690.059 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 68997 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0
[pid=14275] vsize: 4860
Current children cumulated CPU time (s) 690.05
Current children cumulated vsize (Kb) 6984

[startup+700.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 69997 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0
[pid=14275] vsize: 4860
Current children cumulated CPU time (s) 700.05
Current children cumulated vsize (Kb) 6984

[startup+710.06 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 70997 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0
[pid=14275] vsize: 4860
Current children cumulated CPU time (s) 710.05
Current children cumulated vsize (Kb) 6984

[startup+720.061 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 71997 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0
[pid=14275] vsize: 4860
Current children cumulated CPU time (s) 720.05
Current children cumulated vsize (Kb) 6984

[startup+730.062 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 72998 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0
[pid=14275] vsize: 4860
Current children cumulated CPU time (s) 730.06
Current children cumulated vsize (Kb) 6984

[startup+740.063 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1108 0 0 0 73998 7 0 0 25 0 1 0 1784112047 4976640 1095 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1215 1095 145 145 0 1070 0
[pid=14275] vsize: 4860
Current children cumulated CPU time (s) 740.06
Current children cumulated vsize (Kb) 6984

[startup+750.064 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1109 0 0 0 74998 7 0 0 25 0 1 0 1784112047 4976640 1096 4294967295 134512640 135094434 3221224448 3221223040 134557500 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1215 1096 145 145 0 1070 0
[pid=14275] vsize: 4860
Current children cumulated CPU time (s) 750.06
Current children cumulated vsize (Kb) 6984

[startup+760.065 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1136 0 0 0 75997 7 0 0 25 0 1 0 1784112047 5091328 1123 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1243 1123 145 145 0 1098 0
[pid=14275] vsize: 4972
Current children cumulated CPU time (s) 760.05
Current children cumulated vsize (Kb) 7096

[startup+770.066 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1136 0 0 0 76998 7 0 0 25 0 1 0 1784112047 5091328 1123 4294967295 134512640 135094434 3221224448 3221223104 134558156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1243 1123 145 145 0 1098 0
[pid=14275] vsize: 4972
Current children cumulated CPU time (s) 770.06
Current children cumulated vsize (Kb) 7096

[startup+780.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1136 0 0 0 77998 7 0 0 25 0 1 0 1784112047 5091328 1123 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1243 1123 145 145 0 1098 0
[pid=14275] vsize: 4972
Current children cumulated CPU time (s) 780.06
Current children cumulated vsize (Kb) 7096

[startup+790.067 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1136 0 0 0 78998 7 0 0 25 0 1 0 1784112047 5091328 1123 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1243 1123 145 145 0 1098 0
[pid=14275] vsize: 4972
Current children cumulated CPU time (s) 790.06
Current children cumulated vsize (Kb) 7096

[startup+800.068 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1142 0 0 0 79998 7 0 0 25 0 1 0 1784112047 5124096 1129 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1251 1129 145 145 0 1106 0
[pid=14275] vsize: 5004
Current children cumulated CPU time (s) 800.06
Current children cumulated vsize (Kb) 7128

[startup+810.069 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1147 0 0 0 80999 7 0 0 25 0 1 0 1784112047 5156864 1134 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1259 1134 145 145 0 1114 0
[pid=14275] vsize: 5036
Current children cumulated CPU time (s) 810.07
Current children cumulated vsize (Kb) 7160

[startup+820.07 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1147 0 0 0 81999 7 0 0 25 0 1 0 1784112047 5156864 1134 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1259 1134 145 145 0 1114 0
[pid=14275] vsize: 5036
Current children cumulated CPU time (s) 820.07
Current children cumulated vsize (Kb) 7160

[startup+830.071 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1147 0 0 0 82999 7 0 0 25 0 1 0 1784112047 5156864 1134 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1259 1134 145 145 0 1114 0
[pid=14275] vsize: 5036
Current children cumulated CPU time (s) 830.07
Current children cumulated vsize (Kb) 7160

[startup+840.072 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1147 0 0 0 83999 7 0 0 25 0 1 0 1784112047 5156864 1134 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1259 1134 145 145 0 1114 0
[pid=14275] vsize: 5036
Current children cumulated CPU time (s) 840.07
Current children cumulated vsize (Kb) 7160

[startup+850.073 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1148 0 0 0 85000 7 0 0 25 0 1 0 1784112047 5156864 1135 4294967295 134512640 135094434 3221224448 3221223080 134557561 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1259 1135 145 145 0 1114 0
[pid=14275] vsize: 5036
Current children cumulated CPU time (s) 850.08
Current children cumulated vsize (Kb) 7160

[startup+860.074 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1149 0 0 0 86000 7 0 0 25 0 1 0 1784112047 5156864 1136 4294967295 134512640 135094434 3221224448 3221223104 134557950 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1259 1136 145 145 0 1114 0
[pid=14275] vsize: 5036
Current children cumulated CPU time (s) 860.08
Current children cumulated vsize (Kb) 7160

[startup+870.075 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1155 0 0 0 87000 7 0 0 25 0 1 0 1784112047 5189632 1142 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1267 1142 145 145 0 1122 0
[pid=14275] vsize: 5068
Current children cumulated CPU time (s) 870.08
Current children cumulated vsize (Kb) 7192

[startup+880.076 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1160 0 0 0 88000 7 0 0 25 0 1 0 1784112047 5222400 1147 4294967295 134512640 135094434 3221224448 3221223060 134563130 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1275 1147 145 145 0 1130 0
[pid=14275] vsize: 5100
Current children cumulated CPU time (s) 880.08
Current children cumulated vsize (Kb) 7224

[startup+890.077 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1162 0 0 0 89000 7 0 0 25 0 1 0 1784112047 5222400 1149 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1275 1149 145 145 0 1130 0
[pid=14275] vsize: 5100
Current children cumulated CPU time (s) 890.08
Current children cumulated vsize (Kb) 7224

[startup+900.078 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1163 0 0 0 90001 7 0 0 25 0 1 0 1784112047 5222400 1150 4294967295 134512640 135094434 3221224448 3221223104 134557972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1275 1150 145 145 0 1130 0
[pid=14275] vsize: 5100
Current children cumulated CPU time (s) 900.09
Current children cumulated vsize (Kb) 7224

[startup+910.079 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1163 0 0 0 91001 7 0 0 25 0 1 0 1784112047 5222400 1150 4294967295 134512640 135094434 3221224448 3221223120 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1275 1150 145 145 0 1130 0
[pid=14275] vsize: 5100
Current children cumulated CPU time (s) 910.09
Current children cumulated vsize (Kb) 7224

[startup+920.081 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1163 0 0 0 92001 7 0 0 25 0 1 0 1784112047 5222400 1150 4294967295 134512640 135094434 3221224448 3221223104 134558426 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1275 1150 145 145 0 1130 0
[pid=14275] vsize: 5100
Current children cumulated CPU time (s) 920.09
Current children cumulated vsize (Kb) 7224

[startup+930.081 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1163 0 0 0 93002 7 0 0 25 0 1 0 1784112047 5222400 1150 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1275 1150 145 145 0 1130 0
[pid=14275] vsize: 5100
Current children cumulated CPU time (s) 930.1
Current children cumulated vsize (Kb) 7224

[startup+940.082 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1168 0 0 0 94002 7 0 0 25 0 1 0 1784112047 5255168 1155 4294967295 134512640 135094434 3221224448 3221223040 134551469 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1283 1155 145 145 0 1138 0
[pid=14275] vsize: 5132
Current children cumulated CPU time (s) 940.1
Current children cumulated vsize (Kb) 7256

[startup+950.083 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1168 0 0 0 95002 7 0 0 25 0 1 0 1784112047 5255168 1155 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1283 1155 145 145 0 1138 0
[pid=14275] vsize: 5132
Current children cumulated CPU time (s) 950.1
Current children cumulated vsize (Kb) 7256

[startup+960.084 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1168 0 0 0 96002 7 0 0 25 0 1 0 1784112047 5255168 1155 4294967295 134512640 135094434 3221224448 3221223104 134557917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1283 1155 145 145 0 1138 0
[pid=14275] vsize: 5132
Current children cumulated CPU time (s) 960.1
Current children cumulated vsize (Kb) 7256

[startup+970.086 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1169 0 0 0 97003 7 0 0 25 0 1 0 1784112047 5255168 1156 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1283 1156 145 145 0 1138 0
[pid=14275] vsize: 5132
Current children cumulated CPU time (s) 970.11
Current children cumulated vsize (Kb) 7256

[startup+980.087 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1170 0 0 0 98003 7 0 0 25 0 1 0 1784112047 5255168 1157 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1283 1157 145 145 0 1138 0
[pid=14275] vsize: 5132
Current children cumulated CPU time (s) 980.11
Current children cumulated vsize (Kb) 7256

[startup+990.087 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1170 0 0 0 99003 7 0 0 25 0 1 0 1784112047 5255168 1157 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1283 1157 145 145 0 1138 0
[pid=14275] vsize: 5132
Current children cumulated CPU time (s) 990.11
Current children cumulated vsize (Kb) 7256

[startup+1000.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1175 0 0 0 100003 7 0 0 25 0 1 0 1784112047 5287936 1162 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1291 1162 145 145 0 1146 0
[pid=14275] vsize: 5164
Current children cumulated CPU time (s) 1000.11
Current children cumulated vsize (Kb) 7288

[startup+1010.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1177 0 0 0 101003 7 0 0 25 0 1 0 1784112047 5287936 1164 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1291 1164 145 145 0 1146 0
[pid=14275] vsize: 5164
Current children cumulated CPU time (s) 1010.11
Current children cumulated vsize (Kb) 7288

[startup+1020.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1182 0 0 0 102004 7 0 0 25 0 1 0 1784112047 5320704 1169 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1299 1169 145 145 0 1154 0
[pid=14275] vsize: 5196
Current children cumulated CPU time (s) 1020.12
Current children cumulated vsize (Kb) 7320

[startup+1030.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1183 0 0 0 103004 7 0 0 25 0 1 0 1784112047 5320704 1170 4294967295 134512640 135094434 3221224448 3221223120 134554867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1299 1170 145 145 0 1154 0
[pid=14275] vsize: 5196
Current children cumulated CPU time (s) 1030.12
Current children cumulated vsize (Kb) 7320

[startup+1040.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1184 0 0 0 104004 7 0 0 25 0 1 0 1784112047 5320704 1171 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1299 1171 145 145 0 1154 0
[pid=14275] vsize: 5196
Current children cumulated CPU time (s) 1040.12
Current children cumulated vsize (Kb) 7320

[startup+1050.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1184 0 0 0 105005 7 0 0 25 0 1 0 1784112047 5320704 1171 4294967295 134512640 135094434 3221224448 3221222992 134562048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1299 1171 145 145 0 1154 0
[pid=14275] vsize: 5196
Current children cumulated CPU time (s) 1050.13
Current children cumulated vsize (Kb) 7320

[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1197 0 0 0 106005 7 0 0 25 0 1 0 1784112047 5386240 1184 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1315 1184 145 145 0 1170 0
[pid=14275] vsize: 5260
Current children cumulated CPU time (s) 1060.13
Current children cumulated vsize (Kb) 7384

[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1205 0 0 0 107005 7 0 0 25 0 1 0 1784112047 5414912 1192 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1322 1192 145 145 0 1177 0
[pid=14275] vsize: 5288
Current children cumulated CPU time (s) 1070.13
Current children cumulated vsize (Kb) 7412

[startup+1080.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1205 0 0 0 108005 7 0 0 25 0 1 0 1784112047 5414912 1192 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1322 1192 145 145 0 1177 0
[pid=14275] vsize: 5288
Current children cumulated CPU time (s) 1080.13
Current children cumulated vsize (Kb) 7412

[startup+1090.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1205 0 0 0 109005 7 0 0 25 0 1 0 1784112047 5414912 1192 4294967295 134512640 135094434 3221224448 3221223120 134555560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1322 1192 145 145 0 1177 0
[pid=14275] vsize: 5288
Current children cumulated CPU time (s) 1090.13
Current children cumulated vsize (Kb) 7412

[startup+1100.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1205 0 0 0 110005 7 0 0 25 0 1 0 1784112047 5414912 1192 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1322 1192 145 145 0 1177 0
[pid=14275] vsize: 5288
Current children cumulated CPU time (s) 1100.13
Current children cumulated vsize (Kb) 7412

[startup+1110.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1206 0 0 0 111006 7 0 0 25 0 1 0 1784112047 5414912 1193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1322 1193 145 145 0 1177 0
[pid=14275] vsize: 5288
Current children cumulated CPU time (s) 1110.14
Current children cumulated vsize (Kb) 7412

[startup+1120.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1206 0 0 0 112006 7 0 0 25 0 1 0 1784112047 5414912 1193 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1322 1193 145 145 0 1177 0
[pid=14275] vsize: 5288
Current children cumulated CPU time (s) 1120.14
Current children cumulated vsize (Kb) 7412

[startup+1130.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1206 0 0 0 113006 7 0 0 25 0 1 0 1784112047 5414912 1193 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1322 1193 145 145 0 1177 0
[pid=14275] vsize: 5288
Current children cumulated CPU time (s) 1130.14
Current children cumulated vsize (Kb) 7412

[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1206 0 0 0 114006 7 0 0 25 0 1 0 1784112047 5414912 1193 4294967295 134512640 135094434 3221224448 3221223072 134562092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1322 1193 145 145 0 1177 0
[pid=14275] vsize: 5288
Current children cumulated CPU time (s) 1140.14
Current children cumulated vsize (Kb) 7412

[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1213 0 0 0 115007 7 0 0 25 0 1 0 1784112047 5447680 1200 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1330 1200 145 145 0 1185 0
[pid=14275] vsize: 5320
Current children cumulated CPU time (s) 1150.15
Current children cumulated vsize (Kb) 7444

[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1213 0 0 0 116006 8 0 0 25 0 1 0 1784112047 5447680 1200 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/14275/statm): 1330 1200 145 145 0 1185 0
[pid=14275] vsize: 5320
Current children cumulated CPU time (s) 1160.15
Current children cumulated vsize (Kb) 7444

[startup+1170.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1231 0 0 0 117006 8 0 0 25 0 1 0 1784112047 5578752 1218 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1362 1218 145 145 0 1217 0
[pid=14275] vsize: 5448
Current children cumulated CPU time (s) 1170.15
Current children cumulated vsize (Kb) 7572

[startup+1180.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1235 0 0 0 118006 8 0 0 25 0 1 0 1784112047 5595136 1222 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1366 1222 145 145 0 1221 0
[pid=14275] vsize: 5464
Current children cumulated CPU time (s) 1180.15
Current children cumulated vsize (Kb) 7588

[startup+1190.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1235 0 0 0 119006 8 0 0 25 0 1 0 1784112047 5595136 1222 4294967295 134512640 135094434 3221224448 3221223104 134557882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1366 1222 145 145 0 1221 0
[pid=14275] vsize: 5464
Current children cumulated CPU time (s) 1190.15
Current children cumulated vsize (Kb) 7588

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1240 0 0 0 120006 8 0 0 25 0 1 0 1784112047 5623808 1227 4294967295 134512640 135094434 3221224448 3221223072 134557694 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1373 1227 145 145 0 1228 0
[pid=14275] vsize: 5492
Current children cumulated CPU time (s) 1200.15
Current children cumulated vsize (Kb) 7616



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1200.11 s]
Raw data (loadavg): 0.99 0.97 0.99 2/57 14275
Raw data (/proc/14271/stat): 14271 (minisat+_script) S 14270 14271 6847 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1784112042 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/14271/statm): 531 226 485 147 0 384 0
[pid=14271] vsize: 2124
Raw data (/proc/14275/stat): 14275 (minisat+_64-bit) R 14271 14271 6847 0 -1 0 1240 0 0 0 120006 8 0 0 25 0 1 0 1784112047 5623808 1227 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/14275/statm): 1373 1227 145 145 0 1228 0
[pid=14275] vsize: 5492
Current children cumulated CPU time (s) 1200.15
Current children cumulated vsize (Kb) 7616

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

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.16
CPU user time (s): 1200.07
CPU system time (s): 0.088986
CPU usage (%): 100.003
Max. virtual memory (cumulated for all children) (Kb): 7616

Verifier Data

ERROR: no interpretation found !