Some explanations

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

General information on the benchmark

Namemps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-share2b.opb
MD5SUM4012b33f10ee9cb79561239f68fdcd6b
Bench Categoryoptimization, big integers (OPTBIGINT)
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 870
Biggest coefficient in the objective function 204010946560
Number of bits for the biggest coefficient in the objective function 38
Sum of the numbers in the objective function 4534411718529
Number of bits of the sum of numbers in the objective function 43
Biggest number in a constraint 552977039360
Number of bits of the biggest number in a constraint 40
Biggest sum of numbers in a constraint 10976862656529
Number of bits of the biggest sum of numbers44
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables2370
Total number of constraints96
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints96
Minimum length of a constraint30
Maximum length of a constraint360

Trace number 2673

Launcher Data

LAUNCH ON wulflinc10 THE 2005-09-18 20:35:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2814 boxname=wulflinc10 idbench=470 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4012b33f10ee9cb79561239f68fdcd6b  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-share2b.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-share2b.opb
IDLAUNCH: 2814
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        917788 kB
Buffers:         35204 kB
Cached:          54872 kB
SwapCached:        228 kB
Active:          66924 kB
Inactive:        26124 kB
HighTotal:      131008 kB
HighFree:        72352 kB
LowTotal:       903652 kB
LowFree:        845436 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            18172 kB
Committed_AS:    64128 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 20:55:47 (client local time) WITH STATUS 0 IN 1207.22 SECONDS
stats: 2814 7 1207.22 0

Solver Data

c Parsing PB file...
c Converting 109 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: #############
c   -- Clauses(.)/Splits(s): (none)
c ---[ 108]---> Adder-cost: 860   maxlim: 24691811   bits: 26/25
c ---[ 107]---> Adder-cost: 574   maxlim: 5838564   bits: 24/23
c ---[ 106]---> Adder-cost: 632   maxlim: 6553549   bits: 24/23
c ---[ 105]---> Adder-cost: 860   maxlim: 11796389   bits: 25/24
c ---[ 104]---> Adder-cost: 1538   maxlim: 131070999   bits: 28/27
c ---[ 103]---> Adder-cost: 1520   maxlim: 131070999   bits: 28/27
c ---[ 102]---> Adder-cost: 1292   maxlim: 117963899   bits: 28/27
c ---[ 101]---> Adder-cost: 1032   maxlim: 117963899   bits: 28/27
c ---[ 100]---> BDD-cost:  160
c ---[  98]---> Sorter-cost: 2247     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  97]---> Adder-cost: 684   maxlim: 7974098   bits: 24/23
c ---[  96]---> Adder-cost: 482   maxlim: 2944795   bits: 23/22
c ---[  95]---> Adder-cost: 451   maxlim: 1638349   bits: 22/21
c ---[  94]---> Adder-cost: 669   maxlim: 2949029   bits: 23/22
c ---[  93]---> Adder-cost: 1179   maxlim: 29162629   bits: 26/25
c ---[  92]---> Adder-cost: 1203   maxlim: 29162629   bits: 26/25
c ---[  91]---> Adder-cost: 857   maxlim: 26868939   bits: 26/25
c ---[  90]---> Adder-cost: 771   maxlim: 26868939   bits: 26/25
c ---[  89]---> BDD-cost:  140
c ---[  87]---> Sorter-cost: 1452     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  86]---> Adder-cost: 1186   maxlim: 16204591   bits: 25/24
c ---[  85]---> Adder-cost: 754   maxlim: 4970022   bits: 23/23
c ---[  84]---> Adder-cost: 769   maxlim: 3276749   bits: 23/22
c ---[  83]---> Adder-cost: 966   maxlim: 5898149   bits: 24/23
c ---[  82]---> Adder-cost: 1745   maxlim: 65534999   bits: 27/26
c ---[  81]---> Adder-cost: 1659   maxlim: 65534999   bits: 27/26
c ---[  80]---> Adder-cost: 1313   maxlim: 29490749   bits: 26/25
c ---[  79]---> Adder-cost: 1225   maxlim: 58981499   bits: 27/26
c ---[  78]---> BDD-cost:  150
c ---[  76]---> Adder-cost: 248   maxlim: 96246   bits: 18/17
c ---[  75]---> Adder-cost: 970   maxlim: 9886616   bits: 24/24
c ---[  74]---> Adder-cost: 620   maxlim: 3731054   bits: 23/22
c ---[  73]---> Adder-cost: 758   maxlim: 1638349   bits: 22/21
c ---[  72]---> Adder-cost: 721   maxlim: 2949029   bits: 23/22
c ---[  71]---> Adder-cost: 1500   maxlim: 29162629   bits: 26/25
c ---[  70]---> Adder-cost: 1390   maxlim: 29162629   bits: 26/25
c ---[  69]---> Adder-cost: 1121   maxlim: 26868939   bits: 26/25
c ---[  68]---> Adder-cost: 1077   maxlim: 26868939   bits: 26/25
c ---[  67]---> BDD-cost:  140
c ---[  65]---> Sorter-cost: 2235     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  64]---> Adder-cost: 858   maxlim: 10320981   bits: 24/24
c ---[  63]---> Adder-cost: 444   maxlim: 3505911   bits: 23/22
c ---[  62]---> Adder-cost: 670   maxlim: 1638349   bits: 22/21
c ---[  61]---> Adder-cost: 922   maxlim: 2949029   bits: 23/22
c ---[  60]---> Adder-cost: 1578   maxlim: 33094669   bits: 26/25
c ---[  59]---> Adder-cost: 1469   maxlim: 33094669   bits: 26/25
c ---[  58]---> Adder-cost: 1360   maxlim: 29817969   bits: 26/25
c ---[  57]---> Adder-cost: 1282   maxlim: 29817969   bits: 26/25
c ---[  56]---> BDD-cost:  140
c ---[  54]---> Sorter-cost: 2609     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Adder-cost: 886   maxlim: 14431144   bits: 25/24
c ---[  52]---> Adder-cost: 550   maxlim: 3866247   bits: 23/22
c ---[  51]---> Adder-cost: 575   maxlim: 3276749   bits: 23/22
c ---[  50]---> Adder-cost: 818   maxlim: 5898149   bits: 24/23
c ---[  49]---> Adder-cost: 1533   maxlim: 58326149   bits: 27/26
c ---[  48]---> Adder-cost: 1549   maxlim: 58326149   bits: 27/26
c ---[  47]---> Adder-cost: 1225   maxlim: 53738699   bits: 27/26
c ---[  46]---> Adder-cost: 1321   maxlim: 53738699   bits: 27/26
c ---[  45]---> BDD-cost:  150
c ---[  43]---> Sorter-cost: 2520     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  465     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> BDD-cost:   58
c ---[  40]---> Sorter-cost: 1966     Base: 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[  39]---> Sorter-cost:  543     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  38]---> BDD-cost:   53
c ---[  37]---> Sorter-cost:  249     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> BDD-cost:   53
c ---[  35]---> Sorter-cost: 3109     Base: 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:   10
c ---[  32]---> Sorter-cost:  295     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  295     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  295     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Adder-cost: 366   maxlim: 964540   bits: 21/20
c ---[  28]---> BDD-cost:   48
c ---[  27]---> BDD-cost:   48
c ---[  26]---> BDD-cost:   48
c ---[  25]---> BDD-cost:   10
c ---[  23]---> Sorter-cost:  352     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> BDD-cost:  143
c ---[  19]---> Sorter-cost:  333     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> Sorter-cost:  323     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> BDD-cost:  133
c ---[  13]---> BDD-cost:  128
c ---[  12]---> BDD-cost:   48
c ---[  11]---> Sorter-cost:  810     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[  10]---> Adder-cost: 856   maxlim: 42535866   bits: 27/26
c ---[   9]---> Adder-cost: 622   maxlim: 8828577   bits: 25/24
c ---[   8]---> Adder-cost: 690   maxlim: 13107149   bits: 25/24
c ---[   7]---> Adder-cost: 860   maxlim: 23592869   bits: 26/25
c ---[   6]---> Adder-cost: 1596   maxlim: 235928699   bits: 29/28
c ---[   5]---> Adder-cost: 1614   maxlim: 235928699   bits: 29/28
c ---[   4]---> Adder-cost: 1432   maxlim: 217578689   bits: 29/28
c ---[   3]---> Adder-cost: 1464   maxlim: 217578689   bits: 29/28
c ---[   2]---> BDD-cost:  170
c ---[   0]---> Sorter-cost: 2644     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  469982  1608750 |  156660       0        0     nan |  0.000 % |
c |       101 |  469817  1608381 |  172326      76      305     4.0 |  3.136 % |
c |       252 |  469817  1608381 |  189558     227     1774     7.8 |  3.136 % |
c |       477 |  469817  1608381 |  208514     452     3745     8.3 |  3.136 % |
c |       817 |  469817  1608381 |  229365     792     9533    12.0 |  3.136 % |
c |      1325 |  469817  1608381 |  252302    1300    25297    19.5 |  3.136 % |
c |      2084 |  469817  1608381 |  277532    2059    46649    22.7 |  3.136 % |
c |      3223 |  469556  1607801 |  305286    3168    55879    17.6 |  3.223 % |
c |      4931 |  469354  1607336 |  335814    4860   132236    27.2 |  3.298 % |
c |      7493 |  469095  1606436 |  369396    7419   195209    26.3 |  3.311 % |
c |     11337 |  469095  1606436 |  406335   11263   315276    28.0 |  3.311 % |
c |     17103 |  469095  1606436 |  446969   17029   619643    36.4 |  3.311 % |
c |     25752 |  469057  1606335 |  491666   25633   953628    37.2 |  3.322 % |
c |     38726 |  468885  1605727 |  540832   38601  1743603    45.2 |  3.329 % |
c |     58187 |  468646  1605194 |  594916   58029  2868936    49.4 |  3.407 % |
c |     87380 |  468590  1605069 |  654407   87214  4525565    51.9 |  3.425 % |
c |    131169 |  468122  1603675 |  719848  130978  6390243    48.8 |  3.502 % |
c |    196854 |  468016  1603438 |  791833  196651  9700417    49.3 |  3.535 % |
c |    295381 |  468016  1603438 |  871016  295178 15254998    51.7 |  3.535 % |

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/32026/stat): 32026 (minisat+_script) R 32025 32026 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785988435 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/32026/statm): 174 3 169 147 0 27 0
[pid=32026] 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=32027
New process pid=32028
New process pid=32029
execve syscall for /bin/sed executable
One traced child (pid=32028) 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=32029) exited with status: 0
One traced child (pid=32027) exited with status: 0
New process pid=32030
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-share2b.opb

[startup+10.0027 s]
Raw data (loadavg): 1.06 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 633 0 0 0 989 2 0 0 25 0 1 0 1785988440 2904064 588 4294967295 134512640 135094434 3221224432 3221221808 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 709 588 145 145 0 564 0
[pid=32030] vsize: 2836
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 4960

[startup+20.0033 s]
Raw data (loadavg): 1.05 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 811 0 0 0 1989 3 0 0 25 0 1 0 1785988440 3391488 685 4294967295 134512640 135094434 3221224432 3221221808 134677313 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 828 685 145 145 0 683 0
[pid=32030] vsize: 3312
Current children cumulated CPU time (s) 19.92
Current children cumulated vsize (Kb) 5436

[startup+30.0038 s]
Raw data (loadavg): 1.04 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 905 0 0 0 2988 3 0 0 25 0 1 0 1785988440 3575808 747 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 873 747 145 145 0 728 0
[pid=32030] vsize: 3492
Current children cumulated CPU time (s) 29.91
Current children cumulated vsize (Kb) 5616

[startup+40.0044 s]
Raw data (loadavg): 1.04 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 987 0 0 0 3988 3 0 0 25 0 1 0 1785988440 3563520 750 4294967295 134512640 135094434 3221224432 3221221632 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 870 750 145 145 0 725 0
[pid=32030] vsize: 3480
Current children cumulated CPU time (s) 39.91
Current children cumulated vsize (Kb) 5604

[startup+50.0049 s]
Raw data (loadavg): 1.03 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1093 0 0 0 4988 4 0 0 25 0 1 0 1785988440 4145152 817 4294967295 134512640 135094434 3221224432 3221221456 134600267 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1012 817 145 145 0 867 0
[pid=32030] vsize: 4048
Current children cumulated CPU time (s) 49.92
Current children cumulated vsize (Kb) 6172

[startup+60.0055 s]
Raw data (loadavg): 1.02 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1202 0 0 0 5987 4 0 0 25 0 1 0 1785988440 4132864 826 4294967295 134512640 135094434 3221224432 3221221808 134600314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1009 826 145 145 0 864 0
[pid=32030] vsize: 4036
Current children cumulated CPU time (s) 59.91
Current children cumulated vsize (Kb) 6160

[startup+70.0061 s]
Raw data (loadavg): 1.02 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1556 0 0 0 6986 5 0 0 25 0 1 0 1785988440 4780032 1019 4294967295 134512640 135094434 3221224432 3221221432 134676241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1167 1019 145 145 0 1022 0
[pid=32030] vsize: 4668
Current children cumulated CPU time (s) 69.91
Current children cumulated vsize (Kb) 6792

[startup+80.0066 s]
Raw data (loadavg): 1.02 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1653 0 0 0 7985 6 0 0 25 0 1 0 1785988440 4722688 1005 4294967295 134512640 135094434 3221224432 3221220576 134677346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1153 1005 145 145 0 1008 0
[pid=32030] vsize: 4612
Current children cumulated CPU time (s) 79.91
Current children cumulated vsize (Kb) 6736

[startup+90.0072 s]
Raw data (loadavg): 1.01 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1743 0 0 0 8985 6 0 0 25 0 1 0 1785988440 4874240 1056 4294967295 134512640 135094434 3221224432 3221221632 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1190 1056 145 145 0 1045 0
[pid=32030] vsize: 4760
Current children cumulated CPU time (s) 89.91
Current children cumulated vsize (Kb) 6884

[startup+100.008 s]
Raw data (loadavg): 1.01 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1898 0 0 0 9985 6 0 0 25 0 1 0 1785988440 5025792 1106 4294967295 134512640 135094434 3221224432 3221220752 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1227 1106 145 145 0 1082 0
[pid=32030] vsize: 4908
Current children cumulated CPU time (s) 99.91
Current children cumulated vsize (Kb) 7032

[startup+110.008 s]
Raw data (loadavg): 1.01 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 1998 0 0 0 10984 7 0 0 25 0 1 0 1785988440 5951488 1167 4294967295 134512640 135094434 3221224432 3221220928 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1453 1167 145 145 0 1308 0
[pid=32030] vsize: 5812
Current children cumulated CPU time (s) 109.91
Current children cumulated vsize (Kb) 7936

[startup+120.009 s]
Raw data (loadavg): 1.01 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2111 0 0 0 11984 7 0 0 25 0 1 0 1785988440 6049792 1215 4294967295 134512640 135094434 3221224432 3221220928 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1477 1215 145 145 0 1332 0
[pid=32030] vsize: 5908
Current children cumulated CPU time (s) 119.91
Current children cumulated vsize (Kb) 8032

[startup+130.008 s]
Raw data (loadavg): 1.01 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2225 0 0 0 12983 8 0 0 25 0 1 0 1785988440 6057984 1217 4294967295 134512640 135094434 3221224432 3221221168 134677091 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1479 1217 145 145 0 1334 0
[pid=32030] vsize: 5916
Current children cumulated CPU time (s) 129.91
Current children cumulated vsize (Kb) 8040

[startup+140.009 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2654 0 0 0 13982 9 0 0 25 0 1 0 1785988440 6901760 1439 4294967295 134512640 135094434 3221224432 3221221104 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1685 1439 145 145 0 1540 0
[pid=32030] vsize: 6740
Current children cumulated CPU time (s) 139.91
Current children cumulated vsize (Kb) 8864

[startup+150.01 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2654 0 0 0 14983 9 0 0 25 0 1 0 1785988440 6901760 1439 4294967295 134512640 135094434 3221224432 3221221456 134677307 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1685 1439 145 145 0 1540 0
[pid=32030] vsize: 6740
Current children cumulated CPU time (s) 149.92
Current children cumulated vsize (Kb) 8864

[startup+160.009 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2774 0 0 0 15982 9 0 0 25 0 1 0 1785988440 6946816 1456 4294967295 134512640 135094434 3221224432 3221221456 134677290 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1696 1456 145 145 0 1551 0
[pid=32030] vsize: 6784
Current children cumulated CPU time (s) 159.91
Current children cumulated vsize (Kb) 8908

[startup+170.01 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 2998 0 0 0 16981 10 0 0 25 0 1 0 1785988440 7135232 1537 4294967295 134512640 135094434 3221224432 3221220752 134600151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 1742 1537 145 145 0 1597 0
[pid=32030] vsize: 6968
Current children cumulated CPU time (s) 169.91
Current children cumulated vsize (Kb) 9092

[startup+180.01 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3147 0 0 0 17980 11 0 0 25 0 1 0 1785988440 7348224 1622 4294967295 134512640 135094434 3221224432 3221220224 134676539 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1794 1622 145 145 0 1649 0
[pid=32030] vsize: 7176
Current children cumulated CPU time (s) 179.91
Current children cumulated vsize (Kb) 9300

[startup+190.011 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3147 0 0 0 18980 11 0 0 25 0 1 0 1785988440 7348224 1622 4294967295 134512640 135094434 3221224432 3221220752 134600175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1794 1622 145 145 0 1649 0
[pid=32030] vsize: 7176
Current children cumulated CPU time (s) 189.91
Current children cumulated vsize (Kb) 9300

[startup+200.011 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3147 0 0 0 19980 11 0 0 25 0 1 0 1785988440 7348224 1622 4294967295 134512640 135094434 3221224432 3221221188 134677077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1794 1622 145 145 0 1649 0
[pid=32030] vsize: 7176
Current children cumulated CPU time (s) 199.91
Current children cumulated vsize (Kb) 9300

[startup+210.012 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3147 0 0 0 20980 11 0 0 25 0 1 0 1785988440 7348224 1622 4294967295 134512640 135094434 3221224432 3221221880 134677084 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1794 1622 145 145 0 1649 0
[pid=32030] vsize: 7176
Current children cumulated CPU time (s) 209.91
Current children cumulated vsize (Kb) 9300

[startup+220.012 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3318 0 0 0 21979 12 0 0 25 0 1 0 1785988440 7507968 1682 4294967295 134512640 135094434 3221224432 3221222256 134677138 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1833 1682 145 145 0 1688 0
[pid=32030] vsize: 7332
Current children cumulated CPU time (s) 219.91
Current children cumulated vsize (Kb) 9456

[startup+230.013 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 3373 0 0 0 22979 12 0 0 25 0 1 0 1785988440 7565312 1696 4294967295 134512640 135094434 3221224432 3221221280 134676586 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 1847 1696 145 145 0 1702 0
[pid=32030] vsize: 7388
Current children cumulated CPU time (s) 229.91
Current children cumulated vsize (Kb) 9512

[startup+240.014 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 10828 0 0 0 23909 45 0 0 25 0 1 0 1785988440 41287680 9135 4294967295 134512640 135094434 3221224432 3221223092 134553491 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 10080 9135 145 145 0 9935 0
[pid=32030] vsize: 40320
Current children cumulated CPU time (s) 239.54
Current children cumulated vsize (Kb) 42444

[startup+250.014 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 11162 0 0 0 24902 49 0 0 25 0 1 0 1785988440 42672128 9469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 10418 9469 145 145 0 10273 0
[pid=32030] vsize: 41672
Current children cumulated CPU time (s) 249.51
Current children cumulated vsize (Kb) 43796

[startup+260.014 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 11647 0 0 0 25893 52 0 0 25 0 1 0 1785988440 44699648 9954 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 10913 9954 145 145 0 10768 0
[pid=32030] vsize: 43652
Current children cumulated CPU time (s) 259.45
Current children cumulated vsize (Kb) 45776

[startup+270.015 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 11996 0 0 0 26886 55 0 0 25 0 1 0 1785988440 46100480 10303 4294967295 134512640 135094434 3221224432 3221223056 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 11255 10303 145 145 0 11110 0
[pid=32030] vsize: 45020
Current children cumulated CPU time (s) 269.41
Current children cumulated vsize (Kb) 47144

[startup+280.016 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 12325 0 0 0 27879 58 0 0 25 0 1 0 1785988440 47427584 10632 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 11579 10632 145 145 0 11434 0
[pid=32030] vsize: 46316
Current children cumulated CPU time (s) 279.37
Current children cumulated vsize (Kb) 48440

[startup+290.017 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 12772 0 0 0 28872 62 0 0 25 0 1 0 1785988440 49364992 11079 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 12052 11079 145 145 0 11907 0
[pid=32030] vsize: 48208
Current children cumulated CPU time (s) 289.34
Current children cumulated vsize (Kb) 50332

[startup+300.018 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 13169 0 0 0 29865 65 0 0 25 0 1 0 1785988440 50970624 11476 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 12444 11476 145 145 0 12299 0
[pid=32030] vsize: 49776
Current children cumulated CPU time (s) 299.3
Current children cumulated vsize (Kb) 51900

[startup+310.018 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 13505 0 0 0 30859 68 0 0 25 0 1 0 1785988440 52330496 11812 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 12776 11812 145 145 0 12631 0
[pid=32030] vsize: 51104
Current children cumulated CPU time (s) 309.27
Current children cumulated vsize (Kb) 53228

[startup+320.018 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 13853 0 0 0 31853 70 0 0 25 0 1 0 1785988440 53739520 12160 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 13120 12160 145 145 0 12975 0
[pid=32030] vsize: 52480
Current children cumulated CPU time (s) 319.23
Current children cumulated vsize (Kb) 54604

[startup+330.019 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 14141 0 0 0 32848 72 0 0 25 0 1 0 1785988440 54902784 12448 4294967295 134512640 135094434 3221224432 3221223092 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 13404 12448 145 145 0 13259 0
[pid=32030] vsize: 53616
Current children cumulated CPU time (s) 329.2
Current children cumulated vsize (Kb) 55740

[startup+340.019 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 14367 0 0 0 33844 74 0 0 25 0 1 0 1785988440 55762944 12674 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 13614 12674 145 145 0 13469 0
[pid=32030] vsize: 54456
Current children cumulated CPU time (s) 339.18
Current children cumulated vsize (Kb) 56580

[startup+350.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 14683 0 0 0 34838 77 0 0 25 0 1 0 1785988440 57032704 12990 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 13924 12990 145 145 0 13779 0
[pid=32030] vsize: 55696
Current children cumulated CPU time (s) 349.15
Current children cumulated vsize (Kb) 57820

[startup+360.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 14990 0 0 0 35831 80 0 0 25 0 1 0 1785988440 58535936 13297 4294967295 134512640 135094434 3221224432 3221223056 134557685 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 14291 13297 145 145 0 14146 0
[pid=32030] vsize: 57164
Current children cumulated CPU time (s) 359.11
Current children cumulated vsize (Kb) 59288

[startup+370.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 15272 0 0 0 36825 83 0 0 25 0 1 0 1785988440 59670528 13579 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 14568 13579 145 145 0 14423 0
[pid=32030] vsize: 58272
Current children cumulated CPU time (s) 369.08
Current children cumulated vsize (Kb) 60396

[startup+380.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 15579 0 0 0 37819 86 0 0 25 0 1 0 1785988440 60911616 13886 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 14871 13886 145 145 0 14726 0
[pid=32030] vsize: 59484
Current children cumulated CPU time (s) 379.05
Current children cumulated vsize (Kb) 61608

[startup+390.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 15850 0 0 0 38815 88 0 0 25 0 1 0 1785988440 62013440 14157 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 15140 14157 145 145 0 14995 0
[pid=32030] vsize: 60560
Current children cumulated CPU time (s) 389.03
Current children cumulated vsize (Kb) 62684

[startup+400.024 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 16127 0 0 0 39810 90 0 0 25 0 1 0 1785988440 63139840 14434 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 15415 14434 145 145 0 15270 0
[pid=32030] vsize: 61660
Current children cumulated CPU time (s) 399
Current children cumulated vsize (Kb) 63784

[startup+410.024 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 16339 0 0 0 40806 91 0 0 25 0 1 0 1785988440 64004096 14646 4294967295 134512640 135094434 3221224432 3221223056 134557717 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 15626 14646 145 145 0 15481 0
[pid=32030] vsize: 62504
Current children cumulated CPU time (s) 408.97
Current children cumulated vsize (Kb) 64628

[startup+420.026 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 16554 0 0 0 41803 93 0 0 25 0 1 0 1785988440 64872448 14861 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 15838 14861 145 145 0 15693 0
[pid=32030] vsize: 63352
Current children cumulated CPU time (s) 418.96
Current children cumulated vsize (Kb) 65476

[startup+430.026 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 16883 0 0 0 42796 95 0 0 25 0 1 0 1785988440 66195456 15190 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 16161 15190 145 145 0 16016 0
[pid=32030] vsize: 64644
Current children cumulated CPU time (s) 428.91
Current children cumulated vsize (Kb) 66768

[startup+440.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 17194 0 0 0 43791 98 0 0 25 0 1 0 1785988440 67457024 15501 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 16469 15501 145 145 0 16324 0
[pid=32030] vsize: 65876
Current children cumulated CPU time (s) 438.89
Current children cumulated vsize (Kb) 68000

[startup+450.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 17443 0 0 0 44787 99 0 0 25 0 1 0 1785988440 68456448 15750 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 16713 15750 145 145 0 16568 0
[pid=32030] vsize: 66852
Current children cumulated CPU time (s) 448.86
Current children cumulated vsize (Kb) 68976

[startup+460.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) T 32026 32026 22582 0 -1 0 17782 0 0 0 45781 102 0 0 25 0 1 0 1785988440 69816320 16089 4294967295 134512640 135094434 3221224432 3221222780 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32030/statm): 17045 16089 145 145 0 16900 0
[pid=32030] vsize: 68180
Current children cumulated CPU time (s) 458.83
Current children cumulated vsize (Kb) 70304

[startup+470.027 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 18072 0 0 0 46775 104 0 0 25 0 1 0 1785988440 70979584 16379 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 17329 16379 145 145 0 17184 0
[pid=32030] vsize: 69316
Current children cumulated CPU time (s) 468.79
Current children cumulated vsize (Kb) 71440

[startup+480.028 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 18550 0 0 0 47767 108 0 0 25 0 1 0 1785988440 72908800 16857 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 17800 16857 145 145 0 17655 0
[pid=32030] vsize: 71200
Current children cumulated CPU time (s) 478.75
Current children cumulated vsize (Kb) 73324

[startup+490.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 18868 0 0 0 48761 110 0 0 25 0 1 0 1785988440 74715136 17175 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 18241 17175 145 145 0 18096 0
[pid=32030] vsize: 72964
Current children cumulated CPU time (s) 488.71
Current children cumulated vsize (Kb) 75088

[startup+500.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) T 32026 32026 22582 0 -1 0 19265 0 0 0 49753 113 0 0 25 0 1 0 1785988440 76312576 17572 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32030/statm): 18631 17572 145 145 0 18486 0
[pid=32030] vsize: 74524
Current children cumulated CPU time (s) 498.66
Current children cumulated vsize (Kb) 76648

[startup+510.031 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 19617 0 0 0 50747 116 0 0 25 0 1 0 1785988440 77729792 17924 4294967295 134512640 135094434 3221224432 3221223104 134555560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 18977 17924 145 145 0 18832 0
[pid=32030] vsize: 75908
Current children cumulated CPU time (s) 508.63
Current children cumulated vsize (Kb) 78032

[startup+520.031 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 19923 0 0 0 51740 119 0 0 25 0 1 0 1785988440 78962688 18230 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 19278 18230 145 145 0 19133 0
[pid=32030] vsize: 77112
Current children cumulated CPU time (s) 518.59
Current children cumulated vsize (Kb) 79236

[startup+530.032 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 20200 0 0 0 52735 122 0 0 25 0 1 0 1785988440 80080896 18507 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 19551 18507 145 145 0 19406 0
[pid=32030] vsize: 78204
Current children cumulated CPU time (s) 528.57
Current children cumulated vsize (Kb) 80328

[startup+540.032 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 20449 0 0 0 53731 124 0 0 25 0 1 0 1785988440 81104896 18756 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 19801 18756 145 145 0 19656 0
[pid=32030] vsize: 79204
Current children cumulated CPU time (s) 538.55
Current children cumulated vsize (Kb) 81328

[startup+550.033 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 20704 0 0 0 54725 125 0 0 25 0 1 0 1785988440 82137088 19011 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 20053 19011 145 145 0 19908 0
[pid=32030] vsize: 80212
Current children cumulated CPU time (s) 548.5
Current children cumulated vsize (Kb) 82336

[startup+560.033 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 20932 0 0 0 55721 127 0 0 25 0 1 0 1785988440 83054592 19239 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 20277 19239 145 145 0 20132 0
[pid=32030] vsize: 81108
Current children cumulated CPU time (s) 558.48
Current children cumulated vsize (Kb) 83232

[startup+570.033 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 21196 0 0 0 56716 129 0 0 25 0 1 0 1785988440 84131840 19503 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 20540 19503 145 145 0 20395 0
[pid=32030] vsize: 82160
Current children cumulated CPU time (s) 568.45
Current children cumulated vsize (Kb) 84284

[startup+580.034 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 21426 0 0 0 57712 131 0 0 25 0 1 0 1785988440 85073920 19733 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 20770 19733 145 145 0 20625 0
[pid=32030] vsize: 83080
Current children cumulated CPU time (s) 578.43
Current children cumulated vsize (Kb) 85204

[startup+590.034 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 21825 0 0 0 58704 134 0 0 25 0 1 0 1785988440 86683648 20132 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 21163 20132 145 145 0 21018 0
[pid=32030] vsize: 84652
Current children cumulated CPU time (s) 588.38
Current children cumulated vsize (Kb) 86776

[startup+600.035 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 22147 0 0 0 59699 136 0 0 25 0 1 0 1785988440 87982080 20454 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 21480 20454 145 145 0 21335 0
[pid=32030] vsize: 85920
Current children cumulated CPU time (s) 598.35
Current children cumulated vsize (Kb) 88044

[startup+610.035 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 22453 0 0 0 60693 138 0 0 25 0 1 0 1785988440 89235456 20760 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 21786 20760 145 145 0 21641 0
[pid=32030] vsize: 87144
Current children cumulated CPU time (s) 608.31
Current children cumulated vsize (Kb) 89268

[startup+620.036 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 22729 0 0 0 61690 139 0 0 25 0 1 0 1785988440 90370048 21036 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 22063 21036 145 145 0 21918 0
[pid=32030] vsize: 88252
Current children cumulated CPU time (s) 618.29
Current children cumulated vsize (Kb) 90376

[startup+630.037 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 23059 0 0 0 62682 143 0 0 25 0 1 0 1785988440 91688960 21366 4294967295 134512640 135094434 3221224432 3221223072 134558269 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 22385 21366 145 145 0 22240 0
[pid=32030] vsize: 89540
Current children cumulated CPU time (s) 628.25
Current children cumulated vsize (Kb) 91664

[startup+640.038 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 23399 0 0 0 63675 146 0 0 25 0 1 0 1785988440 93065216 21706 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 22721 21706 145 145 0 22576 0
[pid=32030] vsize: 90884
Current children cumulated CPU time (s) 638.21
Current children cumulated vsize (Kb) 93008

[startup+650.039 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 23689 0 0 0 64669 148 0 0 25 0 1 0 1785988440 94240768 21996 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 23008 21996 145 145 0 22863 0
[pid=32030] vsize: 92032
Current children cumulated CPU time (s) 648.17
Current children cumulated vsize (Kb) 94156

[startup+660.039 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 23980 0 0 0 65665 150 0 0 25 0 1 0 1785988440 95416320 22287 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 23295 22287 145 145 0 23150 0
[pid=32030] vsize: 93180
Current children cumulated CPU time (s) 658.15
Current children cumulated vsize (Kb) 95304

[startup+670.041 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 24222 0 0 0 66660 152 0 0 25 0 1 0 1785988440 96407552 22529 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 23537 22529 145 145 0 23392 0
[pid=32030] vsize: 94148
Current children cumulated CPU time (s) 668.12
Current children cumulated vsize (Kb) 96272

[startup+680.041 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 24446 0 0 0 67657 154 0 0 25 0 1 0 1785988440 97341440 22753 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 23765 22753 145 145 0 23620 0
[pid=32030] vsize: 95060
Current children cumulated CPU time (s) 678.11
Current children cumulated vsize (Kb) 97184

[startup+690.043 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 24658 0 0 0 68652 156 0 0 25 0 1 0 1785988440 98193408 22965 4294967295 134512640 135094434 3221224432 3221223104 134555232 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 23973 22965 145 145 0 23828 0
[pid=32030] vsize: 95892
Current children cumulated CPU time (s) 688.08
Current children cumulated vsize (Kb) 98016

[startup+700.043 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 24863 0 0 0 69647 158 0 0 25 0 1 0 1785988440 99020800 23170 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 24175 23170 145 145 0 24030 0
[pid=32030] vsize: 96700
Current children cumulated CPU time (s) 698.05
Current children cumulated vsize (Kb) 98824

[startup+710.044 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 25063 0 0 0 70643 160 0 0 25 0 1 0 1785988440 99823616 23370 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 24371 23370 145 145 0 24226 0
[pid=32030] vsize: 97484
Current children cumulated CPU time (s) 708.03
Current children cumulated vsize (Kb) 99608

[startup+720.046 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 25249 0 0 0 71640 162 0 0 25 0 1 0 1785988440 100585472 23556 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 24557 23556 145 145 0 24412 0
[pid=32030] vsize: 98228
Current children cumulated CPU time (s) 718.02
Current children cumulated vsize (Kb) 100352

[startup+730.046 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 25453 0 0 0 72636 163 0 0 25 0 1 0 1785988440 101433344 23760 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 24764 23760 145 145 0 24619 0
[pid=32030] vsize: 99056
Current children cumulated CPU time (s) 727.99
Current children cumulated vsize (Kb) 101180

[startup+740.048 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 25657 0 0 0 73632 165 0 0 25 0 1 0 1785988440 102248448 23964 4294967295 134512640 135094434 3221224432 3221223104 134556288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 24963 23964 145 145 0 24818 0
[pid=32030] vsize: 99852
Current children cumulated CPU time (s) 737.97
Current children cumulated vsize (Kb) 101976

[startup+750.048 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 25843 0 0 0 74628 167 0 0 25 0 1 0 1785988440 102998016 24150 4294967295 134512640 135094434 3221224432 3221223088 134557872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 25146 24150 145 145 0 25001 0
[pid=32030] vsize: 100584
Current children cumulated CPU time (s) 747.95
Current children cumulated vsize (Kb) 102708

[startup+760.049 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26020 0 0 0 75625 168 0 0 25 0 1 0 1785988440 103727104 24327 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 25324 24327 145 145 0 25179 0
[pid=32030] vsize: 101296
Current children cumulated CPU time (s) 757.93
Current children cumulated vsize (Kb) 103420

[startup+770.05 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26201 0 0 0 76621 171 0 0 25 0 1 0 1785988440 104464384 24508 4294967295 134512640 135094434 3221224432 3221223096 134562037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 25504 24508 145 145 0 25359 0
[pid=32030] vsize: 102016
Current children cumulated CPU time (s) 767.92
Current children cumulated vsize (Kb) 104140

[startup+780.051 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26373 0 0 0 77618 173 0 0 25 0 1 0 1785988440 105189376 24680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 25681 24680 145 145 0 25536 0
[pid=32030] vsize: 102724
Current children cumulated CPU time (s) 777.91
Current children cumulated vsize (Kb) 104848

[startup+790.052 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26541 0 0 0 78614 175 0 0 25 0 1 0 1785988440 105877504 24848 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 25849 24848 145 145 0 25704 0
[pid=32030] vsize: 103396
Current children cumulated CPU time (s) 787.89
Current children cumulated vsize (Kb) 105520

[startup+800.052 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26729 0 0 0 79611 176 0 0 25 0 1 0 1785988440 106622976 25036 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 26031 25036 145 145 0 25886 0
[pid=32030] vsize: 104124
Current children cumulated CPU time (s) 797.87
Current children cumulated vsize (Kb) 106248

[startup+810.053 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 26911 0 0 0 80609 177 0 0 25 0 1 0 1785988440 107425792 25218 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 26227 25218 145 145 0 26082 0
[pid=32030] vsize: 104908
Current children cumulated CPU time (s) 807.86
Current children cumulated vsize (Kb) 107032

[startup+820.053 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27068 0 0 0 81606 179 0 0 25 0 1 0 1785988440 109166592 25375 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 26652 25375 145 145 0 26507 0
[pid=32030] vsize: 106608
Current children cumulated CPU time (s) 817.85
Current children cumulated vsize (Kb) 108732

[startup+830.054 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27215 0 0 0 82603 180 0 0 25 0 1 0 1785988440 109731840 25522 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 26790 25522 145 145 0 26645 0
[pid=32030] vsize: 107160
Current children cumulated CPU time (s) 827.83
Current children cumulated vsize (Kb) 109284

[startup+840.055 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27337 0 0 0 83600 181 0 0 25 0 1 0 1785988440 110211072 25644 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 26907 25644 145 145 0 26762 0
[pid=32030] vsize: 107628
Current children cumulated CPU time (s) 837.81
Current children cumulated vsize (Kb) 109752

[startup+850.056 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27462 0 0 0 84598 182 0 0 25 0 1 0 1785988440 110702592 25769 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 27027 25769 145 145 0 26882 0
[pid=32030] vsize: 108108
Current children cumulated CPU time (s) 847.8
Current children cumulated vsize (Kb) 110232

[startup+860.056 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27627 0 0 0 85596 183 0 0 25 0 1 0 1785988440 111407104 25934 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 27199 25934 145 145 0 27054 0
[pid=32030] vsize: 108796
Current children cumulated CPU time (s) 857.79
Current children cumulated vsize (Kb) 110920

[startup+870.058 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27752 0 0 0 86594 184 0 0 25 0 1 0 1785988440 111964160 26059 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 27335 26059 145 145 0 27190 0
[pid=32030] vsize: 109340
Current children cumulated CPU time (s) 867.78
Current children cumulated vsize (Kb) 111464

[startup+880.059 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 27879 0 0 0 87592 185 0 0 25 0 1 0 1785988440 112480256 26186 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 27461 26186 145 145 0 27316 0
[pid=32030] vsize: 109844
Current children cumulated CPU time (s) 877.77
Current children cumulated vsize (Kb) 111968

[startup+890.06 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28031 0 0 0 88589 186 0 0 25 0 1 0 1785988440 113086464 26338 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 27609 26338 145 145 0 27464 0
[pid=32030] vsize: 110436
Current children cumulated CPU time (s) 887.75
Current children cumulated vsize (Kb) 112560

[startup+900.061 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28185 0 0 0 89587 187 0 0 25 0 1 0 1785988440 113700864 26492 4294967295 134512640 135094434 3221224432 3221223088 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 27759 26492 145 145 0 27614 0
[pid=32030] vsize: 111036
Current children cumulated CPU time (s) 897.74
Current children cumulated vsize (Kb) 113160

[startup+910.06 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28335 0 0 0 90582 190 0 0 25 0 1 0 1785988440 114327552 26642 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 27912 26642 145 145 0 27767 0
[pid=32030] vsize: 111648
Current children cumulated CPU time (s) 907.72
Current children cumulated vsize (Kb) 113772

[startup+920.062 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28459 0 0 0 91580 192 0 0 25 0 1 0 1785988440 114831360 26766 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 28035 26766 145 145 0 27890 0
[pid=32030] vsize: 112140
Current children cumulated CPU time (s) 917.72
Current children cumulated vsize (Kb) 114264

[startup+930.062 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28623 0 0 0 92577 193 0 0 25 0 1 0 1785988440 115490816 26930 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 28196 26930 145 145 0 28051 0
[pid=32030] vsize: 112784
Current children cumulated CPU time (s) 927.7
Current children cumulated vsize (Kb) 114908

[startup+940.063 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28763 0 0 0 93575 194 0 0 25 0 1 0 1785988440 116056064 27070 4294967295 134512640 135094434 3221224432 3221223088 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 28334 27070 145 145 0 28189 0
[pid=32030] vsize: 113336
Current children cumulated CPU time (s) 937.69
Current children cumulated vsize (Kb) 115460

[startup+950.063 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 28906 0 0 0 94572 196 0 0 25 0 1 0 1785988440 116629504 27213 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 28474 27213 145 145 0 28329 0
[pid=32030] vsize: 113896
Current children cumulated CPU time (s) 947.68
Current children cumulated vsize (Kb) 116020

[startup+960.064 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 29065 0 0 0 95569 197 0 0 25 0 1 0 1785988440 117280768 27372 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 28633 27372 145 145 0 28488 0
[pid=32030] vsize: 114532
Current children cumulated CPU time (s) 957.66
Current children cumulated vsize (Kb) 116656

[startup+970.065 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 29237 0 0 0 96566 199 0 0 25 0 1 0 1785988440 117981184 27544 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 28804 27544 145 145 0 28659 0
[pid=32030] vsize: 115216
Current children cumulated CPU time (s) 967.65
Current children cumulated vsize (Kb) 117340

[startup+980.065 s]
Raw data (loadavg): 1.00 1.00 0.98 1/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) T 32026 32026 22582 0 -1 0 29381 0 0 0 97563 200 0 0 25 0 1 0 1785988440 118599680 27688 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/32030/statm): 28955 27688 145 145 0 28810 0
[pid=32030] vsize: 115820
Current children cumulated CPU time (s) 977.63
Current children cumulated vsize (Kb) 117944

[startup+990.067 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 29651 0 0 0 98559 201 0 0 25 0 1 0 1785988440 119697408 27958 4294967295 134512640 135094434 3221224432 3221222896 134780607 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 29223 27958 145 145 0 29078 0
[pid=32030] vsize: 116892
Current children cumulated CPU time (s) 987.6
Current children cumulated vsize (Kb) 119016

[startup+1000.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 29845 0 0 0 99556 203 0 0 25 0 1 0 1785988440 120475648 28152 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 29413 28152 145 145 0 29268 0
[pid=32030] vsize: 117652
Current children cumulated CPU time (s) 997.59
Current children cumulated vsize (Kb) 119776

[startup+1010.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 30048 0 0 0 100553 204 0 0 25 0 1 0 1785988440 121294848 28355 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 29613 28355 145 145 0 29468 0
[pid=32030] vsize: 118452
Current children cumulated CPU time (s) 1007.57
Current children cumulated vsize (Kb) 120576

[startup+1020.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 30269 0 0 0 101549 205 0 0 25 0 1 0 1785988440 122200064 28576 4294967295 134512640 135094434 3221224432 3221223092 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 29834 28576 145 145 0 29689 0
[pid=32030] vsize: 119336
Current children cumulated CPU time (s) 1017.54
Current children cumulated vsize (Kb) 121460

[startup+1030.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) T 32026 32026 22582 0 -1 0 30391 0 0 0 102548 206 0 0 25 0 1 0 1785988440 122695680 28698 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32030/statm): 29955 28698 145 145 0 29810 0
[pid=32030] vsize: 119820
Current children cumulated CPU time (s) 1027.54
Current children cumulated vsize (Kb) 121944

[startup+1040.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 30566 0 0 0 103545 207 0 0 25 0 1 0 1785988440 123396096 28873 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 30126 28873 145 145 0 29981 0
[pid=32030] vsize: 120504
Current children cumulated CPU time (s) 1037.52
Current children cumulated vsize (Kb) 122628

[startup+1050.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 30763 0 0 0 104542 209 0 0 25 0 1 0 1785988440 124190720 29070 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 30320 29070 145 145 0 30175 0
[pid=32030] vsize: 121280
Current children cumulated CPU time (s) 1047.51
Current children cumulated vsize (Kb) 123404

[startup+1060.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) T 32026 32026 22582 0 -1 0 30958 0 0 0 105539 210 0 0 25 0 1 0 1785988440 125005824 29265 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/32030/statm): 30519 29265 145 145 0 30374 0
[pid=32030] vsize: 122076
Current children cumulated CPU time (s) 1057.49
Current children cumulated vsize (Kb) 124200

[startup+1070.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 31149 0 0 0 106536 211 0 0 25 0 1 0 1785988440 125779968 29456 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 30708 29456 145 145 0 30563 0
[pid=32030] vsize: 122832
Current children cumulated CPU time (s) 1067.47
Current children cumulated vsize (Kb) 124956

[startup+1080.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 31549 0 0 0 107529 215 0 0 25 0 1 0 1785988440 127381504 29856 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 31099 29856 145 145 0 30954 0
[pid=32030] vsize: 124396
Current children cumulated CPU time (s) 1077.44
Current children cumulated vsize (Kb) 126520

[startup+1090.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 31740 0 0 0 108525 216 0 0 25 0 1 0 1785988440 128151552 30047 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 31287 30047 145 145 0 31142 0
[pid=32030] vsize: 125148
Current children cumulated CPU time (s) 1087.41
Current children cumulated vsize (Kb) 127272

[startup+1100.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 31868 0 0 0 109522 218 0 0 25 0 1 0 1785988440 128688128 30175 4294967295 134512640 135094434 3221224432 3221223056 134557648 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 31418 30175 145 145 0 31273 0
[pid=32030] vsize: 125672
Current children cumulated CPU time (s) 1097.4
Current children cumulated vsize (Kb) 127796

[startup+1110.07 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 32010 0 0 0 110520 219 0 0 25 0 1 0 1785988440 129290240 30317 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 31565 30317 145 145 0 31420 0
[pid=32030] vsize: 126260
Current children cumulated CPU time (s) 1107.39
Current children cumulated vsize (Kb) 128384

[startup+1120.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 32280 0 0 0 111516 221 0 0 25 0 1 0 1785988440 130371584 30587 4294967295 134512640 135094434 3221224432 3221223088 134557866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 31829 30587 145 145 0 31684 0
[pid=32030] vsize: 127316
Current children cumulated CPU time (s) 1117.37
Current children cumulated vsize (Kb) 129440

[startup+1130.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 32396 0 0 0 112514 222 0 0 25 0 1 0 1785988440 130850816 30703 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 31946 30703 145 145 0 31801 0
[pid=32030] vsize: 127784
Current children cumulated CPU time (s) 1127.36
Current children cumulated vsize (Kb) 129908

[startup+1140.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 32527 0 0 0 113511 223 0 0 25 0 1 0 1785988440 131371008 30834 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 32073 30834 145 145 0 31928 0
[pid=32030] vsize: 128292
Current children cumulated CPU time (s) 1137.34
Current children cumulated vsize (Kb) 130416

[startup+1150.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 32812 0 0 0 114506 225 0 0 25 0 1 0 1785988440 132501504 31119 4294967295 134512640 135094434 3221224432 3221223092 134553499 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 32349 31119 145 145 0 32204 0
[pid=32030] vsize: 129396
Current children cumulated CPU time (s) 1147.31
Current children cumulated vsize (Kb) 131520

[startup+1160.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 33094 0 0 0 115501 227 0 0 25 0 1 0 1785988440 133636096 31401 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 32626 31401 145 145 0 32481 0
[pid=32030] vsize: 130504
Current children cumulated CPU time (s) 1157.28
Current children cumulated vsize (Kb) 132628

[startup+1170.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 33434 0 0 0 116494 231 0 0 25 0 1 0 1785988440 135008256 31741 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 32961 31741 145 145 0 32816 0
[pid=32030] vsize: 131844
Current children cumulated CPU time (s) 1167.25
Current children cumulated vsize (Kb) 133968

[startup+1180.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 33694 0 0 0 117489 233 0 0 25 0 1 0 1785988440 136056832 32001 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/32030/statm): 33217 32001 145 145 0 33072 0
[pid=32030] vsize: 132868
Current children cumulated CPU time (s) 1177.22
Current children cumulated vsize (Kb) 134992

[startup+1190.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 33937 0 0 0 118484 235 0 0 25 0 1 0 1785988440 137039872 32244 4294967295 134512640 135094434 3221224432 3221223088 134558225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 33457 32244 145 145 0 33312 0
[pid=32030] vsize: 133828
Current children cumulated CPU time (s) 1187.19
Current children cumulated vsize (Kb) 135952

[startup+1200.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 34162 0 0 0 119481 236 0 0 25 0 1 0 1785988440 137953280 32469 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 33680 32469 145 145 0 33535 0
[pid=32030] vsize: 134720
Current children cumulated CPU time (s) 1197.17
Current children cumulated vsize (Kb) 136844

[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 34397 0 0 0 120477 238 0 0 25 0 1 0 1785988440 138891264 32704 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 33909 32704 145 145 0 33764 0
[pid=32030] vsize: 135636
Current children cumulated CPU time (s) 1207.15
Current children cumulated vsize (Kb) 137760



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.08 s]
Raw data (loadavg): 1.00 1.00 0.98 2/57 32030
Raw data (/proc/32026/stat): 32026 (minisat+_script) S 32025 32026 22582 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785988435 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/32026/statm): 531 226 485 147 0 384 0
[pid=32026] vsize: 2124
Raw data (/proc/32030/stat): 32030 (minisat+_64-bit) R 32026 32026 22582 0 -1 0 34397 0 0 0 120477 238 0 0 25 0 1 0 1785988440 138891264 32704 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/32030/statm): 33909 32704 145 145 0 33764 0
[pid=32030] vsize: 135636
Current children cumulated CPU time (s) 1207.15
Current children cumulated vsize (Kb) 137760

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

Child status: 0
Real time (s): 1210.15
CPU time (s): 1207.22
CPU user time (s): 1204.77
CPU system time (s): 2.44963
CPU usage (%): 99.7587
Max. virtual memory (cumulated for all children) (Kb): 137760

Verifier Data

ERROR: no interpretation found !