Some explanations

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

General information on the benchmark

Namesubmitted/aloul/FPGA_SAT05/normalized-fpga40_39_sat_pb.cnf.cr.opb
MD5SUMb0b9c98556325dcf5a5811fc2d17a816
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 0
Optimality of the best value was proved NO
Number of terms in the objective function 0
Biggest coefficient in the objective function 0
Number of bits for the biggest coefficient in the objective function 0
Sum of the numbers in the objective function 0
Number of bits of the sum of numbers in the objective function 0
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 41
Number of bits of the biggest sum of numbers6
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark4.40033
Number of variables2340
Total number of constraints1678
Number of constraints which are clauses1599
Number of constraints which are cardinality constraints (but not clauses)79
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint20
Maximum length of a constraint40

Trace number 889

Launcher Data

LAUNCH ON wulflinc21 THE 2005-09-18 12:34:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2392 boxname=wulflinc21 idbench=48 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  b0b9c98556325dcf5a5811fc2d17a816  /oldhome/oroussel/tmp/wulflinc21/normalized-fpga40_39_sat_pb.cnf.cr.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc21/normalized-fpga40_39_sat_pb.cnf.cr.opb
IDLAUNCH: 2392
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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	: 3
cpu MHz		: 451.161
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:        925052 kB
Buffers:         33628 kB
Cached:          48628 kB
SwapCached:        908 kB
Active:          66068 kB
Inactive:        18912 kB
HighTotal:      131008 kB
HighFree:        85792 kB
LowTotal:       903652 kB
LowFree:        839260 kB
SwapTotal:     2097892 kB
SwapFree:      2096472 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5804 kB
Slab:            18976 kB
Committed_AS:    64332 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 12:52:20 (client local time) WITH STATUS 10 IN 1081.88 SECONDS
stats: 2392 7 1081.88 10

Solver Data

c Parsing PB file...
c Converting 1678 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[  78]---> BDD-cost:   75
c ---[  77]---> BDD-cost:   75
c ---[  76]---> BDD-cost:   75
c ---[  75]---> BDD-cost:   75
c ---[  74]---> BDD-cost:   75
c ---[  73]---> BDD-cost:   75
c ---[  72]---> BDD-cost:   75
c ---[  71]---> BDD-cost:   75
c ---[  70]---> BDD-cost:   75
c ---[  69]---> BDD-cost:   75
c ---[  68]---> BDD-cost:   75
c ---[  67]---> BDD-cost:   75
c ---[  66]---> BDD-cost:   75
c ---[  65]---> BDD-cost:   75
c ---[  64]---> BDD-cost:   75
c ---[  63]---> BDD-cost:   75
c ---[  62]---> BDD-cost:   75
c ---[  61]---> BDD-cost:   75
c ---[  60]---> BDD-cost:   75
c ---[  59]---> BDD-cost:   75
c ---[  58]---> BDD-cost:   75
c ---[  57]---> BDD-cost:   75
c ---[  56]---> BDD-cost:   75
c ---[  55]---> BDD-cost:   75
c ---[  54]---> BDD-cost:   75
c ---[  53]---> BDD-cost:   75
c ---[  52]---> BDD-cost:   75
c ---[  51]---> BDD-cost:   75
c ---[  50]---> BDD-cost:   75
c ---[  49]---> BDD-cost:   75
c ---[  48]---> BDD-cost:   75
c ---[  47]---> BDD-cost:   75
c ---[  46]---> BDD-cost:   75
c ---[  45]---> BDD-cost:   75
c ---[  44]---> BDD-cost:   75
c ---[  43]---> BDD-cost:   75
c ---[  42]---> BDD-cost:   75
c ---[  41]---> BDD-cost:   75
c ---[  40]---> BDD-cost:   75
c ---[  39]---> BDD-cost:   75
c ---[  38]---> BDD-cost:   37
c ---[  37]---> BDD-cost:   37
c ---[  36]---> BDD-cost:   37
c ---[  35]---> BDD-cost:   37
c ---[  34]---> BDD-cost:   37
c ---[  33]---> BDD-cost:   37
c ---[  32]---> BDD-cost:   37
c ---[  31]---> BDD-cost:   37
c ---[  30]---> BDD-cost:   37
c ---[  29]---> BDD-cost:   37
c ---[  28]---> BDD-cost:   37
c ---[  27]---> BDD-cost:   37
c ---[  26]---> BDD-cost:   37
c ---[  25]---> BDD-cost:   37
c ---[  24]---> BDD-cost:   37
c ---[  23]---> BDD-cost:   37
c ---[  22]---> BDD-cost:   37
c ---[  21]---> BDD-cost:   37
c ---[  20]---> BDD-cost:   37
c ---[  19]---> BDD-cost:   37
c ---[  18]---> BDD-cost:   37
c ---[  17]---> BDD-cost:   37
c ---[  16]---> BDD-cost:   37
c ---[  15]---> BDD-cost:   37
c ---[  14]---> BDD-cost:   37
c ---[  13]---> BDD-cost:   37
c ---[  12]---> BDD-cost:   37
c ---[  11]---> BDD-cost:   37
c ---[  10]---> BDD-cost:   37
c ---[   9]---> BDD-cost:   37
c ---[   8]---> BDD-cost:   37
c ---[   7]---> BDD-cost:   37
c ---[   6]---> BDD-cost:   37
c ---[   5]---> BDD-cost:   37
c ---[   4]---> BDD-cost:   37
c ---[   3]---> BDD-cost:   37
c ---[   2]---> BDD-cost:   37
c ---[   1]---> BDD-cost:   37
c ---[   0]---> BDD-cost:   37
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   12588    62143 |    4196       0        0     nan |  0.000 % |
c |       111 |   12588    62143 |    4615     111    33739   304.0 |  1.165 % |
c |       263 |   12588    62143 |    5077     263    74695   284.0 |  1.165 % |
c |       488 |   12588    62143 |    5584     488   117851   241.5 |  1.165 % |
c |       825 |   12588    62143 |    6143     825   182982   221.8 |  1.165 % |
c |      1332 |   12588    62143 |    6757    1332   313395   235.3 |  1.165 % |
c |      2093 |   12588    62143 |    7433    2093   552175   263.8 |  1.165 % |
c |      3234 |   12588    62143 |    8176    3234   826036   255.4 |  1.165 % |
c |      4942 |   12588    62143 |    8994    4942  1185368   239.9 |  1.165 % |
c |      7505 |   12588    62143 |    9893    7505  1634136   217.7 |  1.165 % |
c |     11350 |   12588    62143 |   10883   11350  3068153   270.3 |  1.165 % |
c |     17118 |   12588    62143 |   11971   11443  3648096   318.8 |  1.165 % |
c |     25767 |   12588    62143 |   13168   12050  3959642   328.6 |  1.165 % |
c |     38744 |   12588    62143 |   14485   16496  5481733   332.3 |  1.165 % |
c |     58205 |   12588    62143 |   15934   17828  2135865   119.8 |  1.165 % |
c |     87397 |   12588    62143 |   17527   17964  6583862   366.5 |  1.165 % |
c |    131186 |   12588    62143 |   19280   20533  8190543   398.9 |  1.165 % |
c |    196874 |   12588    62143 |   21208   16916  7196074   425.4 |  1.165 % |
c |    295401 |   12588    62143 |   23329   21506  5077493   236.1 |  1.165 % |
c ==============================================================================
c SATISFIABLE: No goal function specified.
s SATISFIABLE
v
c _______________________________________________________________________________
c 
c restarts              : 19
c conflicts             : 314711         (291 /sec)
c decisions             : 438316         (405 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 1080.93 s
c _______________________________________________________________________________

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/22584/stat): 22584 (minisat+_script) R 22583 22584 20602 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1718560978 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/22584/statm): 174 3 169 147 0 27 0
[pid=22584] 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=22585
New process pid=22586
New process pid=22587
execve syscall for /bin/sed executable
One traced child (pid=22586) 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=22587) exited with status: 0
One traced child (pid=22585) exited with status: 0
New process pid=22588
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-fpga40_39_sat_pb.cnf.cr.opb

[startup+10.0041 s]
Raw data (loadavg): 0.93 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 2785 0 2 0 951 13 0 0 25 0 1 0 1718560983 11735040 2773 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22588/statm): 2865 2773 145 145 0 2720 0
[pid=22588] vsize: 11460
Current children cumulated CPU time (s) 9.64
Current children cumulated vsize (Kb) 13584

[startup+20.0058 s]
Raw data (loadavg): 0.94 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 3989 0 2 0 1935 21 0 0 25 0 1 0 1718560983 16654336 3977 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22588/statm): 4066 3977 145 145 0 3921 0
[pid=22588] vsize: 16264
Current children cumulated CPU time (s) 19.56
Current children cumulated vsize (Kb) 18388

[startup+30.0064 s]
Raw data (loadavg): 0.95 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 4655 0 2 0 2924 25 0 0 25 0 1 0 1718560983 19390464 4643 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22588/statm): 4734 4643 145 145 0 4589 0
[pid=22588] vsize: 18936
Current children cumulated CPU time (s) 29.49
Current children cumulated vsize (Kb) 21060

[startup+40.0071 s]
Raw data (loadavg): 0.96 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 5949 0 2 0 3905 33 0 0 25 0 1 0 1718560983 24678400 5937 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22588/statm): 6025 5937 145 145 0 5880 0
[pid=22588] vsize: 24100
Current children cumulated CPU time (s) 39.38
Current children cumulated vsize (Kb) 26224

[startup+50.0078 s]
Raw data (loadavg): 0.96 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 6197 0 2 0 4901 34 0 0 25 0 1 0 1718560983 25698304 6185 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 6274 6185 145 145 0 6129 0
[pid=22588] vsize: 25096
Current children cumulated CPU time (s) 49.35
Current children cumulated vsize (Kb) 27220

[startup+60.0075 s]
Raw data (loadavg): 0.97 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 6349 0 2 0 5899 35 0 0 25 0 1 0 1718560983 26329088 6337 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 6428 6337 145 145 0 6283 0
[pid=22588] vsize: 25712
Current children cumulated CPU time (s) 59.34
Current children cumulated vsize (Kb) 27836

[startup+70.0082 s]
Raw data (loadavg): 0.97 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 6692 0 2 0 6894 37 0 0 25 0 1 0 1718560983 27791360 6680 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 6785 6680 145 145 0 6640 0
[pid=22588] vsize: 27140
Current children cumulated CPU time (s) 69.31
Current children cumulated vsize (Kb) 29264

[startup+80.0088 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 6692 0 2 0 7894 37 0 0 25 0 1 0 1718560983 27791360 6680 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 6785 6680 145 145 0 6640 0
[pid=22588] vsize: 27140
Current children cumulated CPU time (s) 79.31
Current children cumulated vsize (Kb) 29264

[startup+90.0105 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 6692 0 2 0 8895 37 0 0 25 0 1 0 1718560983 27791360 6680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 6785 6680 145 145 0 6640 0
[pid=22588] vsize: 27140
Current children cumulated CPU time (s) 89.32
Current children cumulated vsize (Kb) 29264

[startup+100.011 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 6834 0 2 0 9893 38 0 0 25 0 1 0 1718560983 28401664 6822 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22588/statm): 6934 6822 145 145 0 6789 0
[pid=22588] vsize: 27736
Current children cumulated CPU time (s) 99.31
Current children cumulated vsize (Kb) 29860

[startup+110.012 s]
Raw data (loadavg): 0.98 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 6837 0 2 0 10893 38 0 0 25 0 1 0 1718560983 28401664 6825 4294967295 134512640 135094434 3221224432 3221223024 134556880 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 6934 6825 145 145 0 6789 0
[pid=22588] vsize: 27736
Current children cumulated CPU time (s) 109.31
Current children cumulated vsize (Kb) 29860

[startup+120.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 6837 0 2 0 11893 38 0 0 25 0 1 0 1718560983 28401664 6825 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 6934 6825 145 145 0 6789 0
[pid=22588] vsize: 27736
Current children cumulated CPU time (s) 119.31
Current children cumulated vsize (Kb) 29860

[startup+130.013 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 6837 0 2 0 12893 38 0 0 25 0 1 0 1718560983 28401664 6825 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 6934 6825 145 145 0 6789 0
[pid=22588] vsize: 27736
Current children cumulated CPU time (s) 129.31
Current children cumulated vsize (Kb) 29860

[startup+140.014 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 6837 0 2 0 13893 38 0 0 25 0 1 0 1718560983 28401664 6825 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 6934 6825 145 145 0 6789 0
[pid=22588] vsize: 27736
Current children cumulated CPU time (s) 139.31
Current children cumulated vsize (Kb) 29860

[startup+150.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 7100 0 2 0 14890 40 0 0 25 0 1 0 1718560983 29487104 7088 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22588/statm): 7199 7088 145 145 0 7054 0
[pid=22588] vsize: 28796
Current children cumulated CPU time (s) 149.3
Current children cumulated vsize (Kb) 30920

[startup+160.015 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 7796 0 2 0 15879 45 0 0 25 0 1 0 1718560983 32362496 7784 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22588/statm): 7901 7784 145 145 0 7756 0
[pid=22588] vsize: 31604
Current children cumulated CPU time (s) 159.24
Current children cumulated vsize (Kb) 33728

[startup+170.016 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 7807 0 2 0 16878 45 0 0 25 0 1 0 1718560983 32428032 7795 4294967295 134512640 135094434 3221224432 3221223088 134558235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 7917 7795 145 145 0 7772 0
[pid=22588] vsize: 31668
Current children cumulated CPU time (s) 169.23
Current children cumulated vsize (Kb) 33792

[startup+180.017 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 8394 0 2 0 17870 48 0 0 25 0 1 0 1718560983 34926592 8382 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 8527 8382 145 145 0 8382 0
[pid=22588] vsize: 34108
Current children cumulated CPU time (s) 179.18
Current children cumulated vsize (Kb) 36232

[startup+190.018 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 9589 0 2 0 18850 56 0 0 25 0 1 0 1718560983 39837696 9577 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 9726 9577 145 145 0 9581 0
[pid=22588] vsize: 38904
Current children cumulated CPU time (s) 189.06
Current children cumulated vsize (Kb) 41028

[startup+200.019 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 9963 0 2 0 19844 59 0 0 25 0 1 0 1718560983 41369600 9951 4294967295 134512640 135094434 3221224432 3221223024 134557360 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10100 9951 145 145 0 9955 0
[pid=22588] vsize: 40400
Current children cumulated CPU time (s) 199.03
Current children cumulated vsize (Kb) 42524

[startup+210.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 9963 0 2 0 20844 59 0 0 25 0 1 0 1718560983 41369600 9951 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10100 9951 145 145 0 9955 0
[pid=22588] vsize: 40400
Current children cumulated CPU time (s) 209.03
Current children cumulated vsize (Kb) 42524

[startup+220.02 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 9963 0 2 0 21844 59 0 0 25 0 1 0 1718560983 41369600 9951 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10100 9951 145 145 0 9955 0
[pid=22588] vsize: 40400
Current children cumulated CPU time (s) 219.03
Current children cumulated vsize (Kb) 42524

[startup+230.021 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 9963 0 2 0 22845 59 0 0 25 0 1 0 1718560983 41369600 9951 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10100 9951 145 145 0 9955 0
[pid=22588] vsize: 40400
Current children cumulated CPU time (s) 229.04
Current children cumulated vsize (Kb) 42524

[startup+240.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 9963 0 2 0 23845 59 0 0 25 0 1 0 1718560983 41369600 9951 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10100 9951 145 145 0 9955 0
[pid=22588] vsize: 40400
Current children cumulated CPU time (s) 239.04
Current children cumulated vsize (Kb) 42524

[startup+250.022 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 9963 0 2 0 24845 59 0 0 25 0 1 0 1718560983 41369600 9951 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10100 9951 145 145 0 9955 0
[pid=22588] vsize: 40400
Current children cumulated CPU time (s) 249.04
Current children cumulated vsize (Kb) 42524

[startup+260.023 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10266 0 2 0 25841 61 0 0 25 0 1 0 1718560983 42622976 10254 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10406 10254 145 145 0 10261 0
[pid=22588] vsize: 41624
Current children cumulated CPU time (s) 259.02
Current children cumulated vsize (Kb) 43748

[startup+270.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10267 0 2 0 26841 61 0 0 25 0 1 0 1718560983 42622976 10255 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10406 10255 145 145 0 10261 0
[pid=22588] vsize: 41624
Current children cumulated CPU time (s) 269.02
Current children cumulated vsize (Kb) 43748

[startup+280.024 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10279 0 2 0 27842 61 0 0 25 0 1 0 1718560983 42688512 10267 4294967295 134512640 135094434 3221224432 3221223024 134557421 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10422 10267 145 145 0 10277 0
[pid=22588] vsize: 41688
Current children cumulated CPU time (s) 279.03
Current children cumulated vsize (Kb) 43812

[startup+290.026 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10279 0 2 0 28842 61 0 0 25 0 1 0 1718560983 42688512 10267 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10422 10267 145 145 0 10277 0
[pid=22588] vsize: 41688
Current children cumulated CPU time (s) 289.03
Current children cumulated vsize (Kb) 43812

[startup+300.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10289 0 2 0 29842 61 0 0 25 0 1 0 1718560983 42754048 10277 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10438 10277 145 145 0 10293 0
[pid=22588] vsize: 41752
Current children cumulated CPU time (s) 299.03
Current children cumulated vsize (Kb) 43876

[startup+310.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10291 0 2 0 30842 61 0 0 25 0 1 0 1718560983 42754048 10279 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10438 10279 145 145 0 10293 0
[pid=22588] vsize: 41752
Current children cumulated CPU time (s) 309.03
Current children cumulated vsize (Kb) 43876

[startup+320.027 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10712 0 2 0 31835 65 0 0 25 0 1 0 1718560983 44478464 10700 4294967295 134512640 135094434 3221224432 3221223024 134556937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22588/statm): 10859 10700 145 145 0 10714 0
[pid=22588] vsize: 43436
Current children cumulated CPU time (s) 319
Current children cumulated vsize (Kb) 45560

[startup+330.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10712 0 2 0 32834 65 0 0 25 0 1 0 1718560983 44478464 10700 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10859 10700 145 145 0 10714 0
[pid=22588] vsize: 43436
Current children cumulated CPU time (s) 328.99
Current children cumulated vsize (Kb) 45560

[startup+340.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10712 0 2 0 33834 65 0 0 25 0 1 0 1718560983 44478464 10700 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10859 10700 145 145 0 10714 0
[pid=22588] vsize: 43436
Current children cumulated CPU time (s) 338.99
Current children cumulated vsize (Kb) 45560

[startup+350.029 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10712 0 2 0 34834 65 0 0 25 0 1 0 1718560983 44478464 10700 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10859 10700 145 145 0 10714 0
[pid=22588] vsize: 43436
Current children cumulated CPU time (s) 348.99
Current children cumulated vsize (Kb) 45560

[startup+360.03 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10712 0 2 0 35834 65 0 0 25 0 1 0 1718560983 44478464 10700 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10859 10700 145 145 0 10714 0
[pid=22588] vsize: 43436
Current children cumulated CPU time (s) 358.99
Current children cumulated vsize (Kb) 45560

[startup+370.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10712 0 2 0 36835 65 0 0 25 0 1 0 1718560983 44478464 10700 4294967295 134512640 135094434 3221224432 3221223024 134557522 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 10859 10700 145 145 0 10714 0
[pid=22588] vsize: 43436
Current children cumulated CPU time (s) 369
Current children cumulated vsize (Kb) 45560

[startup+380.031 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10870 0 2 0 37832 66 0 0 25 0 1 0 1718560983 45125632 10858 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 11017 10858 145 145 0 10872 0
[pid=22588] vsize: 44068
Current children cumulated CPU time (s) 378.98
Current children cumulated vsize (Kb) 46192

[startup+390.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10889 0 2 0 38832 66 0 0 25 0 1 0 1718560983 45256704 10877 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 11049 10877 145 145 0 10904 0
[pid=22588] vsize: 44196
Current children cumulated CPU time (s) 388.98
Current children cumulated vsize (Kb) 46320

[startup+400.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10917 0 2 0 39833 66 0 0 25 0 1 0 1718560983 45387776 10905 4294967295 134512640 135094434 3221224432 3221223024 134557002 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 11081 10905 145 145 0 10936 0
[pid=22588] vsize: 44324
Current children cumulated CPU time (s) 398.99
Current children cumulated vsize (Kb) 46448

[startup+410.032 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10917 0 2 0 40833 66 0 0 25 0 1 0 1718560983 45387776 10905 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 11081 10905 145 145 0 10936 0
[pid=22588] vsize: 44324
Current children cumulated CPU time (s) 408.99
Current children cumulated vsize (Kb) 46448

[startup+420.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10917 0 2 0 41833 66 0 0 25 0 1 0 1718560983 45387776 10905 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 11081 10905 145 145 0 10936 0
[pid=22588] vsize: 44324
Current children cumulated CPU time (s) 418.99
Current children cumulated vsize (Kb) 46448

[startup+430.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10917 0 2 0 42833 66 0 0 25 0 1 0 1718560983 45387776 10905 4294967295 134512640 135094434 3221224432 3221223024 134557518 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22588/statm): 11081 10905 145 145 0 10936 0
[pid=22588] vsize: 44324
Current children cumulated CPU time (s) 428.99
Current children cumulated vsize (Kb) 46448

[startup+440.033 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10917 0 2 0 43832 66 0 0 25 0 1 0 1718560983 45387776 10905 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 11081 10905 145 145 0 10936 0
[pid=22588] vsize: 44324
Current children cumulated CPU time (s) 438.98
Current children cumulated vsize (Kb) 46448

[startup+450.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 10917 0 2 0 44832 66 0 0 25 0 1 0 1718560983 45387776 10905 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 11081 10905 145 145 0 10936 0
[pid=22588] vsize: 44324
Current children cumulated CPU time (s) 448.98
Current children cumulated vsize (Kb) 46448

[startup+460.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) T 22584 22584 20602 0 -1 0 11375 0 2 0 45825 69 0 0 25 0 1 0 1718560983 47263744 11363 4294967295 134512640 135094434 3221224432 3221222796 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0
Raw data (/proc/22588/statm): 11539 11363 145 145 0 11394 0
[pid=22588] vsize: 46156
Current children cumulated CPU time (s) 458.94
Current children cumulated vsize (Kb) 48280

[startup+470.034 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 12423 0 2 0 46807 76 0 0 25 0 1 0 1718560983 51580928 12411 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 12593 12411 145 145 0 12448 0
[pid=22588] vsize: 50372
Current children cumulated CPU time (s) 468.83
Current children cumulated vsize (Kb) 52496

[startup+480.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 12520 0 2 0 47806 76 0 0 25 0 1 0 1718560983 51970048 12508 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 12688 12508 145 145 0 12543 0
[pid=22588] vsize: 50752
Current children cumulated CPU time (s) 478.82
Current children cumulated vsize (Kb) 52876

[startup+490.035 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 12522 0 2 0 48806 76 0 0 25 0 1 0 1718560983 51970048 12510 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 12688 12510 145 145 0 12543 0
[pid=22588] vsize: 50752
Current children cumulated CPU time (s) 488.82
Current children cumulated vsize (Kb) 52876

[startup+500.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 12522 0 2 0 49807 76 0 0 25 0 1 0 1718560983 51970048 12510 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 12688 12510 145 145 0 12543 0
[pid=22588] vsize: 50752
Current children cumulated CPU time (s) 498.83
Current children cumulated vsize (Kb) 52876

[startup+510.036 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 12523 0 2 0 50807 76 0 0 25 0 1 0 1718560983 51970048 12511 4294967295 134512640 135094434 3221224432 3221223104 134555931 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 12688 12511 145 145 0 12543 0
[pid=22588] vsize: 50752
Current children cumulated CPU time (s) 508.83
Current children cumulated vsize (Kb) 52876

[startup+520.037 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 12523 0 2 0 51807 76 0 0 25 0 1 0 1718560983 51970048 12511 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 12688 12511 145 145 0 12543 0
[pid=22588] vsize: 50752
Current children cumulated CPU time (s) 518.83
Current children cumulated vsize (Kb) 52876

[startup+530.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 12835 0 2 0 52802 79 0 0 25 0 1 0 1718560983 53268480 12823 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13005 12823 145 145 0 12860 0
[pid=22588] vsize: 52020
Current children cumulated CPU time (s) 528.81
Current children cumulated vsize (Kb) 54144

[startup+540.038 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13432 0 2 0 53794 82 0 0 25 0 1 0 1718560983 55717888 13420 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13603 13420 145 145 0 13458 0
[pid=22588] vsize: 54412
Current children cumulated CPU time (s) 538.76
Current children cumulated vsize (Kb) 56536

[startup+550.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13432 0 2 0 54794 82 0 0 25 0 1 0 1718560983 55717888 13420 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13603 13420 145 145 0 13458 0
[pid=22588] vsize: 54412
Current children cumulated CPU time (s) 548.76
Current children cumulated vsize (Kb) 56536

[startup+560.039 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13432 0 2 0 55795 82 0 0 25 0 1 0 1718560983 55717888 13420 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13603 13420 145 145 0 13458 0
[pid=22588] vsize: 54412
Current children cumulated CPU time (s) 558.77
Current children cumulated vsize (Kb) 56536

[startup+570.04 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13432 0 2 0 56795 82 0 0 25 0 1 0 1718560983 55717888 13420 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13603 13420 145 145 0 13458 0
[pid=22588] vsize: 54412
Current children cumulated CPU time (s) 568.77
Current children cumulated vsize (Kb) 56536

[startup+580.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13432 0 2 0 57795 82 0 0 25 0 1 0 1718560983 55717888 13420 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13603 13420 145 145 0 13458 0
[pid=22588] vsize: 54412
Current children cumulated CPU time (s) 578.77
Current children cumulated vsize (Kb) 56536

[startup+590.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13433 0 2 0 58795 82 0 0 25 0 1 0 1718560983 55717888 13421 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13603 13421 145 145 0 13458 0
[pid=22588] vsize: 54412
Current children cumulated CPU time (s) 588.77
Current children cumulated vsize (Kb) 56536

[startup+600.041 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13436 0 2 0 59796 82 0 0 25 0 1 0 1718560983 55717888 13424 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13603 13424 145 145 0 13458 0
[pid=22588] vsize: 54412
Current children cumulated CPU time (s) 598.78
Current children cumulated vsize (Kb) 56536

[startup+610.042 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13681 0 2 0 60792 83 0 0 25 0 1 0 1718560983 56762368 13669 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13858 13669 145 145 0 13713 0
[pid=22588] vsize: 55432
Current children cumulated CPU time (s) 608.75
Current children cumulated vsize (Kb) 57556

[startup+620.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13681 0 2 0 61792 83 0 0 25 0 1 0 1718560983 56762368 13669 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13858 13669 145 145 0 13713 0
[pid=22588] vsize: 55432
Current children cumulated CPU time (s) 618.75
Current children cumulated vsize (Kb) 57556

[startup+630.043 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13681 0 2 0 62793 83 0 0 25 0 1 0 1718560983 56762368 13669 4294967295 134512640 135094434 3221224432 3221223024 134557141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13858 13669 145 145 0 13713 0
[pid=22588] vsize: 55432
Current children cumulated CPU time (s) 628.76
Current children cumulated vsize (Kb) 57556

[startup+640.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13690 0 2 0 63793 83 0 0 25 0 1 0 1718560983 56827904 13678 4294967295 134512640 135094434 3221224432 3221223024 134556853 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13874 13678 145 145 0 13729 0
[pid=22588] vsize: 55496
Current children cumulated CPU time (s) 638.76
Current children cumulated vsize (Kb) 57620

[startup+650.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13690 0 2 0 64793 83 0 0 25 0 1 0 1718560983 56827904 13678 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13874 13678 145 145 0 13729 0
[pid=22588] vsize: 55496
Current children cumulated CPU time (s) 648.76
Current children cumulated vsize (Kb) 57620

[startup+660.044 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13690 0 2 0 65793 83 0 0 25 0 1 0 1718560983 56827904 13678 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13874 13678 145 145 0 13729 0
[pid=22588] vsize: 55496
Current children cumulated CPU time (s) 658.76
Current children cumulated vsize (Kb) 57620

[startup+670.045 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13699 0 2 0 66793 83 0 0 25 0 1 0 1718560983 56893440 13687 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 13890 13687 145 145 0 13745 0
[pid=22588] vsize: 55560
Current children cumulated CPU time (s) 668.76
Current children cumulated vsize (Kb) 57684

[startup+680.046 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13936 0 2 0 67790 84 0 0 25 0 1 0 1718560983 57880576 13924 4294967295 134512640 135094434 3221224432 3221223024 134557131 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14131 13924 145 145 0 13986 0
[pid=22588] vsize: 56524
Current children cumulated CPU time (s) 678.74
Current children cumulated vsize (Kb) 58648

[startup+690.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13937 0 2 0 68790 84 0 0 25 0 1 0 1718560983 57880576 13925 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14131 13925 145 145 0 13986 0
[pid=22588] vsize: 56524
Current children cumulated CPU time (s) 688.74
Current children cumulated vsize (Kb) 58648

[startup+700.047 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13949 0 2 0 69791 85 0 0 25 0 1 0 1718560983 57946112 13937 4294967295 134512640 135094434 3221224432 3221223076 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13937 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 698.76
Current children cumulated vsize (Kb) 58712

[startup+710.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13950 0 2 0 70791 85 0 0 25 0 1 0 1718560983 57946112 13938 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13938 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 708.76
Current children cumulated vsize (Kb) 58712

[startup+720.048 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13950 0 2 0 71791 85 0 0 25 0 1 0 1718560983 57946112 13938 4294967295 134512640 135094434 3221224432 3221223024 134551434 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13938 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 718.76
Current children cumulated vsize (Kb) 58712

[startup+730.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13950 0 2 0 72791 85 0 0 25 0 1 0 1718560983 57946112 13938 4294967295 134512640 135094434 3221224432 3221223088 134557996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13938 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 728.76
Current children cumulated vsize (Kb) 58712

[startup+740.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13953 0 2 0 73791 85 0 0 25 0 1 0 1718560983 57946112 13941 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13941 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 738.76
Current children cumulated vsize (Kb) 58712

[startup+750.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13954 0 2 0 74791 85 0 0 25 0 1 0 1718560983 57946112 13942 4294967295 134512640 135094434 3221224432 3221223088 134558156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13942 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 748.76
Current children cumulated vsize (Kb) 58712

[startup+760.049 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 75791 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 758.76
Current children cumulated vsize (Kb) 58712

[startup+770.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 76792 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 768.77
Current children cumulated vsize (Kb) 58712

[startup+780.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 77792 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 778.77
Current children cumulated vsize (Kb) 58712

[startup+790.05 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 78792 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223024 134551465 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 788.77
Current children cumulated vsize (Kb) 58712

[startup+800.051 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 79792 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 798.77
Current children cumulated vsize (Kb) 58712

[startup+810.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 80793 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 808.78
Current children cumulated vsize (Kb) 58712

[startup+820.052 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 81793 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223088 134558141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 818.78
Current children cumulated vsize (Kb) 58712

[startup+830.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 82793 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 828.78
Current children cumulated vsize (Kb) 58712

[startup+840.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 83793 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223104 134555544 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 838.78
Current children cumulated vsize (Kb) 58712

[startup+850.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 84793 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 848.78
Current children cumulated vsize (Kb) 58712

[startup+860.053 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 85794 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223104 134556450 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 858.79
Current children cumulated vsize (Kb) 58712

[startup+870.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 86794 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 868.79
Current children cumulated vsize (Kb) 58712

[startup+880.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 87794 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223024 134556876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 878.79
Current children cumulated vsize (Kb) 58712

[startup+890.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 88794 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 888.79
Current children cumulated vsize (Kb) 58712

[startup+900.055 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 89794 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 898.79
Current children cumulated vsize (Kb) 58712

[startup+910.054 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 90795 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 908.8
Current children cumulated vsize (Kb) 58712

[startup+920.056 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 13956 0 2 0 91795 85 0 0 25 0 1 0 1718560983 57946112 13944 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14147 13944 145 145 0 14002 0
[pid=22588] vsize: 56588
Current children cumulated CPU time (s) 918.8
Current children cumulated vsize (Kb) 58712

[startup+930.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14042 0 2 0 92794 85 0 0 25 0 1 0 1718560983 58302464 14030 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14234 14030 145 145 0 14089 0
[pid=22588] vsize: 56936
Current children cumulated CPU time (s) 928.79
Current children cumulated vsize (Kb) 59060

[startup+940.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14197 0 2 0 93791 86 0 0 25 0 1 0 1718560983 58953728 14185 4294967295 134512640 135094434 3221224432 3221223088 134557972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14185 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 938.77
Current children cumulated vsize (Kb) 59696

[startup+950.057 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14197 0 2 0 94791 86 0 0 25 0 1 0 1718560983 58953728 14185 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14185 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 948.77
Current children cumulated vsize (Kb) 59696

[startup+960.058 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14197 0 2 0 95791 86 0 0 25 0 1 0 1718560983 58953728 14185 4294967295 134512640 135094434 3221224432 3221223024 134556902 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14185 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 958.77
Current children cumulated vsize (Kb) 59696

[startup+970.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14197 0 2 0 96792 86 0 0 25 0 1 0 1718560983 58953728 14185 4294967295 134512640 135094434 3221224432 3221223104 134556410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14185 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 968.78
Current children cumulated vsize (Kb) 59696

[startup+980.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14197 0 2 0 97792 86 0 0 25 0 1 0 1718560983 58953728 14185 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14185 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 978.78
Current children cumulated vsize (Kb) 59696

[startup+990.059 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14197 0 2 0 98792 86 0 0 25 0 1 0 1718560983 58953728 14185 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14185 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 988.78
Current children cumulated vsize (Kb) 59696

[startup+1000.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14197 0 2 0 99792 86 0 0 25 0 1 0 1718560983 58953728 14185 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14185 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 998.78
Current children cumulated vsize (Kb) 59696

[startup+1010.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14197 0 2 0 100792 86 0 0 25 0 1 0 1718560983 58953728 14185 4294967295 134512640 135094434 3221224432 3221223024 134556876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14185 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 1008.78
Current children cumulated vsize (Kb) 59696

[startup+1020.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14197 0 2 0 101793 86 0 0 25 0 1 0 1718560983 58953728 14185 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14185 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 1018.79
Current children cumulated vsize (Kb) 59696

[startup+1030.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14197 0 2 0 102792 87 0 0 25 0 1 0 1718560983 58953728 14185 4294967295 134512640 135094434 3221224432 3221223024 134557514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/22588/statm): 14393 14185 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 1028.79
Current children cumulated vsize (Kb) 59696

[startup+1040.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14198 0 2 0 103791 87 0 0 25 0 1 0 1718560983 58953728 14186 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14186 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 1038.78
Current children cumulated vsize (Kb) 59696

[startup+1050.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14198 0 2 0 104792 87 0 0 25 0 1 0 1718560983 58953728 14186 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14186 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 1048.79
Current children cumulated vsize (Kb) 59696

[startup+1060.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14198 0 2 0 105792 87 0 0 25 0 1 0 1718560983 58953728 14186 4294967295 134512640 135094434 3221224432 3221223024 134556806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14186 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 1058.79
Current children cumulated vsize (Kb) 59696

[startup+1070.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14198 0 2 0 106792 87 0 0 25 0 1 0 1718560983 58953728 14186 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14186 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 1068.79
Current children cumulated vsize (Kb) 59696

[startup+1080.06 s]
Raw data (loadavg): 0.99 0.98 0.99 2/58 22588
Raw data (/proc/22584/stat): 22584 (minisat+_script) S 22583 22584 20602 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1718560978 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/22584/statm): 531 226 485 147 0 384 0
[pid=22584] vsize: 2124
Raw data (/proc/22588/stat): 22588 (minisat+_64-bit) R 22584 22584 20602 0 -1 0 14198 0 2 0 107792 87 0 0 25 0 1 0 1718560983 58953728 14186 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/22588/statm): 14393 14186 145 145 0 14248 0
[pid=22588] vsize: 57572
Current children cumulated CPU time (s) 1078.79
Current children cumulated vsize (Kb) 59696
One traced child (pid=22588) exited with status: 10
One traced child (pid=22584) exited with status: 10
All traced children have exited ! Game is over.

Child status: 10
Real time (s): 1083.16
CPU time (s): 1081.88
CPU user time (s): 1080.94
CPU system time (s): 0.941856
CPU usage (%): 99.8819
Max. virtual memory (cumulated for all children) (Kb): 59696

Verifier Data

ERROR: no interpretation found !