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-chnl15_16_pb.cnf.cr.opb
MD5SUM3f8902c4e8af50006f671e2bddb3e9aa
Bench Categoryno optimization function (SAT)
Has Objective FunctionNO
SatisfiableNO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
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 17
Number of bits of the biggest sum of numbers5
Best result obtained on this benchmarkUNSAT
Best CPU time to get the best result obtained on this benchmark0.017996
Number of variables480
Total number of constraints62
Number of constraints which are clauses32
Number of constraints which are cardinality constraints (but not clauses)30
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint15
Maximum length of a constraint16

Trace number 807

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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:        907324 kB
Buffers:         37160 kB
Cached:          60396 kB
SwapCached:        908 kB
Active:          83108 kB
Inactive:        17292 kB
HighTotal:      131008 kB
HighFree:        74480 kB
LowTotal:       903652 kB
LowFree:        832844 kB
SwapTotal:     2097136 kB
SwapFree:      2095620 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5992 kB
Slab:            21132 kB
Committed_AS:    93132 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-18 12:44:02 (client local time) WITH STATUS 0 IN 1209.99 SECONDS
stats: 2347 7 1209.99 0

Solver Data

c Parsing PB file...
c Converting 62 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ................................
c ---[  29]---> BDD-cost:   29
c ---[  28]---> BDD-cost:   29
c ---[  27]---> BDD-cost:   29
c ---[  26]---> BDD-cost:   29
c ---[  25]---> BDD-cost:   29
c ---[  24]---> BDD-cost:   29
c ---[  23]---> BDD-cost:   29
c ---[  22]---> BDD-cost:   29
c ---[  21]---> BDD-cost:   29
c ---[  20]---> BDD-cost:   29
c ---[  19]---> BDD-cost:   29
c ---[  18]---> BDD-cost:   29
c ---[  17]---> BDD-cost:   29
c ---[  16]---> BDD-cost:   29
c ---[  15]---> BDD-cost:   29
c ---[  14]---> BDD-cost:   29
c ---[  13]---> BDD-cost:   29
c ---[  12]---> BDD-cost:   29
c ---[  11]---> BDD-cost:   29
c ---[  10]---> BDD-cost:   29
c ---[   9]---> BDD-cost:   29
c ---[   8]---> BDD-cost:   29
c ---[   7]---> BDD-cost:   29
c ---[   6]---> BDD-cost:   29
c ---[   5]---> BDD-cost:   29
c ---[   4]---> BDD-cost:   29
c ---[   3]---> BDD-cost:   29
c ---[   2]---> BDD-cost:   29
c ---[   1]---> BDD-cost:   29
c ---[   0]---> BDD-cost:   29
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    2162     6030 |     720       0        0     nan |  0.000 % |
c |       102 |    2162     6030 |     792     102     5686    55.7 |  2.222 % |
c |       252 |    2162     6030 |     871     252    14004    55.6 |  2.222 % |
c |       478 |    2162     6030 |     958     478    28490    59.6 |  2.222 % |
c |       815 |    2162     6030 |    1054     815    57080    70.0 |  2.222 % |
c |      1322 |    2162     6030 |    1159    1322   104342    78.9 |  2.222 % |
c |      2084 |    2162     6030 |    1275    1423   130456    91.7 |  2.222 % |
c |      3226 |    2162     6030 |    1403    1038    95866    92.4 |  2.222 % |
c |      4934 |    2162     6030 |    1543    1033   102989    99.7 |  2.222 % |
c |      7499 |    2162     6030 |    1697    1732   186615   107.7 |  2.222 % |
c |     11345 |    2162     6030 |    1867    1717   162221    94.5 |  2.222 % |
c |     17111 |    2162     6030 |    2054    1970   199253   101.1 |  2.222 % |
c |     25760 |    2162     6030 |    2259    2320   271642   117.1 |  2.222 % |
c |     38735 |    2162     6030 |    2485    2566   270521   105.4 |  2.222 % |
c |     58199 |    2162     6030 |    2734    2477   258968   104.5 |  2.222 % |
c |     87394 |    2162     6030 |    3007    2810   295638   105.2 |  2.222 % |
c |    131184 |    2162     6030 |    3308    1846   187402   101.5 |  2.222 % |
c |    196869 |    2162     6030 |    3639    3043   323650   106.4 |  2.222 % |
c |    295396 |    2162     6030 |    4003    3086   314350   101.9 |  2.222 % |
c |    443187 |    2162     6030 |    4403    2851   287482   100.8 |  2.222 % |
c |    664871 |    2162     6030 |    4843    3470   330999    95.4 |  2.222 % |
c |    997401 |    2162     6030 |    5328    4395   477257   108.6 |  2.222 % |
c |   1496194 |    2162     6030 |    5860    4647   485933   104.6 |  2.222 % |

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/21538/stat): 21538 (minisat+_script) R 21537 21538 17733 0 -1 0 19 0 0 0 0 0 0 0 22 0 1 0 1726145431 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/21538/statm): 174 3 169 147 0 27 0
[pid=21538] 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=21539
New process pid=21540
New process pid=21541
execve syscall for /bin/sed executable
One traced child (pid=21540) 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=21541) exited with status: 0
One traced child (pid=21539) exited with status: 0
New process pid=21542
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc1/normalized-chnl15_16_pb.cnf.cr.opb

[startup+10.0047 s]
Raw data (loadavg): 0.72 0.91 0.93 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 636 0 2 0 983 2 0 0 25 0 1 0 1726145436 2891776 625 4294967295 134512640 135094434 3221224432 3221223104 134556242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 706 625 145 145 0 561 0
[pid=21542] vsize: 2824
Current children cumulated CPU time (s) 9.86
Current children cumulated vsize (Kb) 4948

[startup+20.0065 s]
Raw data (loadavg): 0.76 0.91 0.93 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 706 0 2 0 1982 3 0 0 25 0 1 0 1726145436 3178496 695 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 776 695 145 145 0 631 0
[pid=21542] vsize: 3104
Current children cumulated CPU time (s) 19.86
Current children cumulated vsize (Kb) 5228

[startup+30.0073 s]
Raw data (loadavg): 0.80 0.91 0.93 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 770 0 2 0 2981 3 0 0 25 0 1 0 1726145436 3440640 759 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 840 759 145 145 0 695 0
[pid=21542] vsize: 3360
Current children cumulated CPU time (s) 29.85
Current children cumulated vsize (Kb) 5484

[startup+40.0071 s]
Raw data (loadavg): 0.83 0.91 0.93 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 813 0 2 0 3980 4 0 0 25 0 1 0 1726145436 3616768 802 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 883 802 145 145 0 738 0
[pid=21542] vsize: 3532
Current children cumulated CPU time (s) 39.85
Current children cumulated vsize (Kb) 5656

[startup+50.0089 s]
Raw data (loadavg): 1.01 0.95 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 841 0 2 0 4979 5 0 0 25 0 1 0 1726145436 3731456 830 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 911 830 145 145 0 766 0
[pid=21542] vsize: 3644
Current children cumulated CPU time (s) 49.85
Current children cumulated vsize (Kb) 5768

[startup+60.0097 s]
Raw data (loadavg): 1.01 0.95 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 860 0 2 0 5979 5 0 0 25 0 1 0 1726145436 3809280 849 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 930 849 145 145 0 785 0
[pid=21542] vsize: 3720
Current children cumulated CPU time (s) 59.85
Current children cumulated vsize (Kb) 5844

[startup+70.0114 s]
Raw data (loadavg): 1.00 0.95 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 860 0 2 0 6979 5 0 0 25 0 1 0 1726145436 3809280 849 4294967295 134512640 135094434 3221224432 3221222912 134780484 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 930 849 145 145 0 785 0
[pid=21542] vsize: 3720
Current children cumulated CPU time (s) 69.85
Current children cumulated vsize (Kb) 5844

[startup+80.0132 s]
Raw data (loadavg): 1.00 0.95 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 948 0 2 0 7977 6 0 0 25 0 1 0 1726145436 4173824 937 4294967295 134512640 135094434 3221224432 3221223088 134558011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1019 937 145 145 0 874 0
[pid=21542] vsize: 4076
Current children cumulated CPU time (s) 79.84
Current children cumulated vsize (Kb) 6200

[startup+90.013 s]
Raw data (loadavg): 1.00 0.95 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 968 0 2 0 8977 7 0 0 25 0 1 0 1726145436 4259840 957 4294967295 134512640 135094434 3221224432 3221223024 134557512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1040 957 145 145 0 895 0
[pid=21542] vsize: 4160
Current children cumulated CPU time (s) 89.85
Current children cumulated vsize (Kb) 6284

[startup+100.014 s]
Raw data (loadavg): 1.00 0.95 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 977 0 2 0 9976 7 0 0 25 0 1 0 1726145436 4300800 966 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1050 966 145 145 0 905 0
[pid=21542] vsize: 4200
Current children cumulated CPU time (s) 99.84
Current children cumulated vsize (Kb) 6324

[startup+110.015 s]
Raw data (loadavg): 1.00 0.96 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 977 0 2 0 10976 7 0 0 25 0 1 0 1726145436 4300800 966 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1050 966 145 145 0 905 0
[pid=21542] vsize: 4200
Current children cumulated CPU time (s) 109.84
Current children cumulated vsize (Kb) 6324

[startup+120.016 s]
Raw data (loadavg): 1.00 0.96 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1000 0 2 0 11976 7 0 0 25 0 1 0 1726145436 4395008 989 4294967295 134512640 135094434 3221224432 3221223088 134558135 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1073 989 145 145 0 928 0
[pid=21542] vsize: 4292
Current children cumulated CPU time (s) 119.84
Current children cumulated vsize (Kb) 6416

[startup+130.017 s]
Raw data (loadavg): 1.00 0.96 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1049 0 2 0 12975 8 0 0 25 0 1 0 1726145436 4603904 1038 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1124 1038 145 145 0 979 0
[pid=21542] vsize: 4496
Current children cumulated CPU time (s) 129.84
Current children cumulated vsize (Kb) 6620

[startup+140.018 s]
Raw data (loadavg): 1.00 0.96 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1056 0 2 0 13975 8 0 0 25 0 1 0 1726145436 4632576 1045 4294967295 134512640 135094434 3221224432 3221223104 134555453 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1131 1045 145 145 0 986 0
[pid=21542] vsize: 4524
Current children cumulated CPU time (s) 139.84
Current children cumulated vsize (Kb) 6648

[startup+150.02 s]
Raw data (loadavg): 1.00 0.96 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1094 0 2 0 14974 8 0 0 25 0 1 0 1726145436 4804608 1083 4294967295 134512640 135094434 3221224432 3221223024 134551463 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1173 1083 145 145 0 1028 0
[pid=21542] vsize: 4692
Current children cumulated CPU time (s) 149.83
Current children cumulated vsize (Kb) 6816

[startup+160.021 s]
Raw data (loadavg): 1.00 0.96 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1141 0 2 0 15975 8 0 0 25 0 1 0 1726145436 5009408 1130 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1223 1130 145 145 0 1078 0
[pid=21542] vsize: 4892
Current children cumulated CPU time (s) 159.84
Current children cumulated vsize (Kb) 7016

[startup+170.021 s]
Raw data (loadavg): 1.00 0.96 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1157 0 2 0 16974 8 0 0 25 0 1 0 1726145436 5091328 1146 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1243 1146 145 145 0 1098 0
[pid=21542] vsize: 4972
Current children cumulated CPU time (s) 169.83
Current children cumulated vsize (Kb) 7096

[startup+180.022 s]
Raw data (loadavg): 1.00 0.96 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1247 0 2 0 17973 9 0 0 25 0 1 0 1726145436 5459968 1236 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1333 1236 145 145 0 1188 0
[pid=21542] vsize: 5332
Current children cumulated CPU time (s) 179.83
Current children cumulated vsize (Kb) 7456

[startup+190.023 s]
Raw data (loadavg): 1.00 0.96 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1247 0 2 0 18973 9 0 0 25 0 1 0 1726145436 5459968 1236 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1333 1236 145 145 0 1188 0
[pid=21542] vsize: 5332
Current children cumulated CPU time (s) 189.83
Current children cumulated vsize (Kb) 7456

[startup+200.024 s]
Raw data (loadavg): 1.00 0.96 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1258 0 2 0 19973 9 0 0 25 0 1 0 1726145436 5505024 1247 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1344 1247 145 145 0 1199 0
[pid=21542] vsize: 5376
Current children cumulated CPU time (s) 199.83
Current children cumulated vsize (Kb) 7500

[startup+210.023 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1278 0 2 0 20973 9 0 0 25 0 1 0 1726145436 5591040 1267 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1365 1267 145 145 0 1220 0
[pid=21542] vsize: 5460
Current children cumulated CPU time (s) 209.83
Current children cumulated vsize (Kb) 7584

[startup+220.024 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1301 0 2 0 21973 9 0 0 25 0 1 0 1726145436 5705728 1290 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1393 1290 145 145 0 1248 0
[pid=21542] vsize: 5572
Current children cumulated CPU time (s) 219.83
Current children cumulated vsize (Kb) 7696

[startup+230.025 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1302 0 2 0 22973 9 0 0 25 0 1 0 1726145436 5705728 1291 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1393 1291 145 145 0 1248 0
[pid=21542] vsize: 5572
Current children cumulated CPU time (s) 229.83
Current children cumulated vsize (Kb) 7696

[startup+240.025 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1302 0 2 0 23974 9 0 0 25 0 1 0 1726145436 5705728 1291 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1393 1291 145 145 0 1248 0
[pid=21542] vsize: 5572
Current children cumulated CPU time (s) 239.84
Current children cumulated vsize (Kb) 7696

[startup+250.026 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1306 0 2 0 24974 9 0 0 25 0 1 0 1726145436 5722112 1295 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1397 1295 145 145 0 1252 0
[pid=21542] vsize: 5588
Current children cumulated CPU time (s) 249.84
Current children cumulated vsize (Kb) 7712

[startup+260.026 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1391 0 2 0 25972 10 0 0 25 0 1 0 1726145436 6070272 1380 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1482 1380 145 145 0 1337 0
[pid=21542] vsize: 5928
Current children cumulated CPU time (s) 259.83
Current children cumulated vsize (Kb) 8052

[startup+270.027 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1408 0 2 0 26972 10 0 0 25 0 1 0 1726145436 6144000 1397 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1500 1397 145 145 0 1355 0
[pid=21542] vsize: 6000
Current children cumulated CPU time (s) 269.83
Current children cumulated vsize (Kb) 8124

[startup+280.028 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1409 0 2 0 27973 10 0 0 25 0 1 0 1726145436 6144000 1398 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1500 1398 145 145 0 1355 0
[pid=21542] vsize: 6000
Current children cumulated CPU time (s) 279.84
Current children cumulated vsize (Kb) 8124

[startup+290.029 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1431 0 2 0 28973 11 0 0 25 0 1 0 1726145436 6242304 1420 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1524 1420 145 145 0 1379 0
[pid=21542] vsize: 6096
Current children cumulated CPU time (s) 289.85
Current children cumulated vsize (Kb) 8220

[startup+300.03 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1473 0 2 0 29973 11 0 0 25 0 1 0 1726145436 6418432 1462 4294967295 134512640 135094434 3221224432 3221223104 134555413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1567 1462 145 145 0 1422 0
[pid=21542] vsize: 6268
Current children cumulated CPU time (s) 299.85
Current children cumulated vsize (Kb) 8392

[startup+310.029 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1480 0 2 0 30973 11 0 0 25 0 1 0 1726145436 6451200 1469 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1575 1469 145 145 0 1430 0
[pid=21542] vsize: 6300
Current children cumulated CPU time (s) 309.85
Current children cumulated vsize (Kb) 8424

[startup+320.03 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1481 0 2 0 31973 11 0 0 25 0 1 0 1726145436 6451200 1470 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1575 1470 145 145 0 1430 0
[pid=21542] vsize: 6300
Current children cumulated CPU time (s) 319.85
Current children cumulated vsize (Kb) 8424

[startup+330.031 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1481 0 2 0 32973 11 0 0 25 0 1 0 1726145436 6451200 1470 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1575 1470 145 145 0 1430 0
[pid=21542] vsize: 6300
Current children cumulated CPU time (s) 329.85
Current children cumulated vsize (Kb) 8424

[startup+340.031 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1491 0 2 0 33973 11 0 0 25 0 1 0 1726145436 6500352 1480 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1587 1480 145 145 0 1442 0
[pid=21542] vsize: 6348
Current children cumulated CPU time (s) 339.85
Current children cumulated vsize (Kb) 8472

[startup+350.032 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1512 0 2 0 34973 11 0 0 25 0 1 0 1726145436 6598656 1501 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1611 1501 145 145 0 1466 0
[pid=21542] vsize: 6444
Current children cumulated CPU time (s) 349.85
Current children cumulated vsize (Kb) 8568

[startup+360.032 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1512 0 2 0 35974 11 0 0 25 0 1 0 1726145436 6598656 1501 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1611 1501 145 145 0 1466 0
[pid=21542] vsize: 6444
Current children cumulated CPU time (s) 359.86
Current children cumulated vsize (Kb) 8568

[startup+370.033 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1525 0 2 0 36973 11 0 0 25 0 1 0 1726145436 6664192 1514 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1627 1514 145 145 0 1482 0
[pid=21542] vsize: 6508
Current children cumulated CPU time (s) 369.85
Current children cumulated vsize (Kb) 8632

[startup+380.034 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1525 0 2 0 37973 11 0 0 25 0 1 0 1726145436 6664192 1514 4294967295 134512640 135094434 3221224432 3221223104 134555753 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1627 1514 145 145 0 1482 0
[pid=21542] vsize: 6508
Current children cumulated CPU time (s) 379.85
Current children cumulated vsize (Kb) 8632

[startup+390.035 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1593 0 2 0 38972 11 0 0 25 0 1 0 1726145436 6942720 1582 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1695 1582 145 145 0 1550 0
[pid=21542] vsize: 6780
Current children cumulated CPU time (s) 389.84
Current children cumulated vsize (Kb) 8904

[startup+400.036 s]
Raw data (loadavg): 1.00 0.97 0.94 1/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) T 21538 21538 17733 0 -1 0 1615 0 2 0 39972 12 0 0 25 0 1 0 1726145436 7032832 1604 4294967295 134512640 135094434 3221224432 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1717 1604 145 145 0 1572 0
[pid=21542] vsize: 6868
Current children cumulated CPU time (s) 399.85
Current children cumulated vsize (Kb) 8992

[startup+410.035 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1641 0 2 0 40972 12 0 0 25 0 1 0 1726145436 7139328 1630 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1743 1630 145 145 0 1598 0
[pid=21542] vsize: 6972
Current children cumulated CPU time (s) 409.85
Current children cumulated vsize (Kb) 9096

[startup+420.036 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1655 0 2 0 41972 12 0 0 25 0 1 0 1726145436 7192576 1644 4294967295 134512640 135094434 3221224432 3221223088 134557988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1756 1644 145 145 0 1611 0
[pid=21542] vsize: 7024
Current children cumulated CPU time (s) 419.85
Current children cumulated vsize (Kb) 9148

[startup+430.037 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1655 0 2 0 42972 12 0 0 25 0 1 0 1726145436 7192576 1644 4294967295 134512640 135094434 3221224432 3221223088 134558013 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1756 1644 145 145 0 1611 0
[pid=21542] vsize: 7024
Current children cumulated CPU time (s) 429.85
Current children cumulated vsize (Kb) 9148

[startup+440.038 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1656 0 2 0 43972 12 0 0 25 0 1 0 1726145436 7192576 1645 4294967295 134512640 135094434 3221224432 3221223088 134558024 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1756 1645 145 145 0 1611 0
[pid=21542] vsize: 7024
Current children cumulated CPU time (s) 439.85
Current children cumulated vsize (Kb) 9148

[startup+450.038 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1668 0 2 0 44973 12 0 0 25 0 1 0 1726145436 7245824 1657 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1769 1657 145 145 0 1624 0
[pid=21542] vsize: 7076
Current children cumulated CPU time (s) 449.86
Current children cumulated vsize (Kb) 9200

[startup+460.039 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1682 0 2 0 45972 12 0 0 25 0 1 0 1726145436 7307264 1671 4294967295 134512640 135094434 3221224432 3221223024 134556793 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1784 1671 145 145 0 1639 0
[pid=21542] vsize: 7136
Current children cumulated CPU time (s) 459.85
Current children cumulated vsize (Kb) 9260

[startup+470.04 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1696 0 2 0 46973 12 0 0 25 0 1 0 1726145436 7368704 1685 4294967295 134512640 135094434 3221224432 3221223104 134555666 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1799 1685 145 145 0 1654 0
[pid=21542] vsize: 7196
Current children cumulated CPU time (s) 469.86
Current children cumulated vsize (Kb) 9320

[startup+480.041 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1700 0 2 0 47973 12 0 0 25 0 1 0 1726145436 7385088 1689 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1803 1689 145 145 0 1658 0
[pid=21542] vsize: 7212
Current children cumulated CPU time (s) 479.86
Current children cumulated vsize (Kb) 9336

[startup+490.041 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1704 0 2 0 48973 12 0 0 25 0 1 0 1726145436 7401472 1693 4294967295 134512640 135094434 3221224432 3221223088 134557928 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1807 1693 145 145 0 1662 0
[pid=21542] vsize: 7228
Current children cumulated CPU time (s) 489.86
Current children cumulated vsize (Kb) 9352

[startup+500.041 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1707 0 2 0 49973 12 0 0 25 0 1 0 1726145436 7401472 1696 4294967295 134512640 135094434 3221224432 3221223024 134556862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1807 1696 145 145 0 1662 0
[pid=21542] vsize: 7228
Current children cumulated CPU time (s) 499.86
Current children cumulated vsize (Kb) 9352

[startup+510.041 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1716 0 2 0 50973 12 0 0 25 0 1 0 1726145436 7438336 1705 4294967295 134512640 135094434 3221224432 3221223104 134556465 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1816 1705 145 145 0 1671 0
[pid=21542] vsize: 7264
Current children cumulated CPU time (s) 509.86
Current children cumulated vsize (Kb) 9388

[startup+520.042 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1720 0 2 0 51973 12 0 0 25 0 1 0 1726145436 7454720 1709 4294967295 134512640 135094434 3221224432 3221223104 134555673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1820 1709 145 145 0 1675 0
[pid=21542] vsize: 7280
Current children cumulated CPU time (s) 519.86
Current children cumulated vsize (Kb) 9404

[startup+530.043 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1727 0 2 0 52973 12 0 0 25 0 1 0 1726145436 7483392 1716 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1827 1716 145 145 0 1682 0
[pid=21542] vsize: 7308
Current children cumulated CPU time (s) 529.86
Current children cumulated vsize (Kb) 9432

[startup+540.043 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1735 0 2 0 53973 12 0 0 25 0 1 0 1726145436 7516160 1724 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1835 1724 145 145 0 1690 0
[pid=21542] vsize: 7340
Current children cumulated CPU time (s) 539.86
Current children cumulated vsize (Kb) 9464

[startup+550.043 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1736 0 2 0 54974 12 0 0 25 0 1 0 1726145436 7516160 1725 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1835 1725 145 145 0 1690 0
[pid=21542] vsize: 7340
Current children cumulated CPU time (s) 549.87
Current children cumulated vsize (Kb) 9464

[startup+560.044 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1746 0 2 0 55974 12 0 0 25 0 1 0 1726145436 7557120 1735 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1845 1735 145 145 0 1700 0
[pid=21542] vsize: 7380
Current children cumulated CPU time (s) 559.87
Current children cumulated vsize (Kb) 9504

[startup+570.045 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1748 0 2 0 56974 13 0 0 25 0 1 0 1726145436 7565312 1737 4294967295 134512640 135094434 3221224432 3221223088 134558162 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1847 1737 145 145 0 1702 0
[pid=21542] vsize: 7388
Current children cumulated CPU time (s) 569.88
Current children cumulated vsize (Kb) 9512

[startup+580.046 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1763 0 2 0 57974 13 0 0 25 0 1 0 1726145436 7626752 1752 4294967295 134512640 135094434 3221224432 3221223024 134557413 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1862 1752 145 145 0 1717 0
[pid=21542] vsize: 7448
Current children cumulated CPU time (s) 579.88
Current children cumulated vsize (Kb) 9572

[startup+590.046 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1780 0 2 0 58973 13 0 0 25 0 1 0 1726145436 7692288 1769 4294967295 134512640 135094434 3221224432 3221223088 134558286 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 1878 1769 145 145 0 1733 0
[pid=21542] vsize: 7512
Current children cumulated CPU time (s) 589.87
Current children cumulated vsize (Kb) 9636

[startup+600.047 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1832 0 2 0 59972 14 0 0 25 0 1 0 1726145436 7905280 1821 4294967295 134512640 135094434 3221224432 3221222896 134780635 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1930 1821 145 145 0 1785 0
[pid=21542] vsize: 7720
Current children cumulated CPU time (s) 599.87
Current children cumulated vsize (Kb) 9844

[startup+610.047 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1839 0 2 0 60973 14 0 0 25 0 1 0 1726145436 7938048 1828 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1938 1828 145 145 0 1793 0
[pid=21542] vsize: 7752
Current children cumulated CPU time (s) 609.88
Current children cumulated vsize (Kb) 9876

[startup+620.048 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1852 0 2 0 61973 14 0 0 25 0 1 0 1726145436 7991296 1841 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1951 1841 145 145 0 1806 0
[pid=21542] vsize: 7804
Current children cumulated CPU time (s) 619.88
Current children cumulated vsize (Kb) 9928

[startup+630.049 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1859 0 2 0 62972 15 0 0 25 0 1 0 1726145436 8024064 1848 4294967295 134512640 135094434 3221224432 3221223088 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1959 1848 145 145 0 1814 0
[pid=21542] vsize: 7836
Current children cumulated CPU time (s) 629.88
Current children cumulated vsize (Kb) 9960

[startup+640.049 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1859 0 2 0 63972 15 0 0 25 0 1 0 1726145436 8024064 1848 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1959 1848 145 145 0 1814 0
[pid=21542] vsize: 7836
Current children cumulated CPU time (s) 639.88
Current children cumulated vsize (Kb) 9960

[startup+650.05 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1859 0 2 0 64972 15 0 0 25 0 1 0 1726145436 8024064 1848 4294967295 134512640 135094434 3221224432 3221221728 134562794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1959 1848 145 145 0 1814 0
[pid=21542] vsize: 7836
Current children cumulated CPU time (s) 649.88
Current children cumulated vsize (Kb) 9960

[startup+660.05 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1869 0 2 0 65972 15 0 0 25 0 1 0 1726145436 8073216 1858 4294967295 134512640 135094434 3221224432 3221223120 134554728 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1971 1858 145 145 0 1826 0
[pid=21542] vsize: 7884
Current children cumulated CPU time (s) 659.88
Current children cumulated vsize (Kb) 10008

[startup+670.051 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1870 0 2 0 66972 16 0 0 25 0 1 0 1726145436 8073216 1859 4294967295 134512640 135094434 3221224432 3221223088 134558123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1971 1859 145 145 0 1826 0
[pid=21542] vsize: 7884
Current children cumulated CPU time (s) 669.89
Current children cumulated vsize (Kb) 10008

[startup+680.052 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1881 0 2 0 67972 16 0 0 25 0 1 0 1726145436 8122368 1870 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1983 1870 145 145 0 1838 0
[pid=21542] vsize: 7932
Current children cumulated CPU time (s) 679.89
Current children cumulated vsize (Kb) 10056

[startup+690.051 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1884 0 2 0 68972 16 0 0 25 0 1 0 1726145436 8138752 1873 4294967295 134512640 135094434 3221224432 3221223088 134558411 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1987 1873 145 145 0 1842 0
[pid=21542] vsize: 7948
Current children cumulated CPU time (s) 689.89
Current children cumulated vsize (Kb) 10072

[startup+700.052 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1892 0 2 0 69972 16 0 0 25 0 1 0 1726145436 8171520 1881 4294967295 134512640 135094434 3221224432 3221223104 134556471 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1995 1881 145 145 0 1850 0
[pid=21542] vsize: 7980
Current children cumulated CPU time (s) 699.89
Current children cumulated vsize (Kb) 10104

[startup+710.053 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1893 0 2 0 70972 16 0 0 25 0 1 0 1726145436 8171520 1882 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1995 1882 145 145 0 1850 0
[pid=21542] vsize: 7980
Current children cumulated CPU time (s) 709.89
Current children cumulated vsize (Kb) 10104

[startup+720.054 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1897 0 2 0 71973 16 0 0 25 0 1 0 1726145436 8187904 1886 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1999 1886 145 145 0 1854 0
[pid=21542] vsize: 7996
Current children cumulated CPU time (s) 719.9
Current children cumulated vsize (Kb) 10120

[startup+730.055 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1899 0 2 0 72973 16 0 0 25 0 1 0 1726145436 8187904 1888 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1999 1888 145 145 0 1854 0
[pid=21542] vsize: 7996
Current children cumulated CPU time (s) 729.9
Current children cumulated vsize (Kb) 10120

[startup+740.055 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1899 0 2 0 73973 16 0 0 25 0 1 0 1726145436 8187904 1888 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1999 1888 145 145 0 1854 0
[pid=21542] vsize: 7996
Current children cumulated CPU time (s) 739.9
Current children cumulated vsize (Kb) 10120

[startup+750.056 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1900 0 2 0 74973 16 0 0 25 0 1 0 1726145436 8187904 1889 4294967295 134512640 135094434 3221224432 3221223096 134556595 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 1999 1889 145 145 0 1854 0
[pid=21542] vsize: 7996
Current children cumulated CPU time (s) 749.9
Current children cumulated vsize (Kb) 10120

[startup+760.056 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1947 0 2 0 75973 16 0 0 25 0 1 0 1726145436 8372224 1936 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2044 1936 145 145 0 1899 0
[pid=21542] vsize: 8176
Current children cumulated CPU time (s) 759.9
Current children cumulated vsize (Kb) 10300

[startup+770.057 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1947 0 2 0 76973 17 0 0 25 0 1 0 1726145436 8372224 1936 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2044 1936 145 145 0 1899 0
[pid=21542] vsize: 8176
Current children cumulated CPU time (s) 769.91
Current children cumulated vsize (Kb) 10300

[startup+780.058 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1949 0 2 0 77973 17 0 0 25 0 1 0 1726145436 8372224 1938 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2044 1938 145 145 0 1899 0
[pid=21542] vsize: 8176
Current children cumulated CPU time (s) 779.91
Current children cumulated vsize (Kb) 10300

[startup+790.057 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1949 0 2 0 78973 17 0 0 25 0 1 0 1726145436 8372224 1938 4294967295 134512640 135094434 3221224432 3221223024 134556802 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2044 1938 145 145 0 1899 0
[pid=21542] vsize: 8176
Current children cumulated CPU time (s) 789.91
Current children cumulated vsize (Kb) 10300

[startup+800.058 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1953 0 2 0 79974 17 0 0 25 0 1 0 1726145436 8384512 1942 4294967295 134512640 135094434 3221224432 3221223104 134556252 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2047 1942 145 145 0 1902 0
[pid=21542] vsize: 8188
Current children cumulated CPU time (s) 799.92
Current children cumulated vsize (Kb) 10312

[startup+810.059 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1953 0 2 0 80973 17 0 0 25 0 1 0 1726145436 8384512 1942 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2047 1942 145 145 0 1902 0
[pid=21542] vsize: 8188
Current children cumulated CPU time (s) 809.91
Current children cumulated vsize (Kb) 10312

[startup+820.06 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1954 0 2 0 81974 17 0 0 25 0 1 0 1726145436 8384512 1943 4294967295 134512640 135094434 3221224432 3221223088 134558009 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2047 1943 145 145 0 1902 0
[pid=21542] vsize: 8188
Current children cumulated CPU time (s) 819.92
Current children cumulated vsize (Kb) 10312

[startup+830.061 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1954 0 2 0 82974 17 0 0 25 0 1 0 1726145436 8384512 1943 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2047 1943 145 145 0 1902 0
[pid=21542] vsize: 8188
Current children cumulated CPU time (s) 829.92
Current children cumulated vsize (Kb) 10312

[startup+840.061 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1954 0 2 0 83974 17 0 0 25 0 1 0 1726145436 8384512 1943 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2047 1943 145 145 0 1902 0
[pid=21542] vsize: 8188
Current children cumulated CPU time (s) 839.92
Current children cumulated vsize (Kb) 10312

[startup+850.062 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1955 0 2 0 84975 17 0 0 25 0 1 0 1726145436 8384512 1944 4294967295 134512640 135094434 3221224432 3221223024 134557416 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2047 1944 145 145 0 1902 0
[pid=21542] vsize: 8188
Current children cumulated CPU time (s) 849.93
Current children cumulated vsize (Kb) 10312

[startup+860.063 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1955 0 2 0 85975 17 0 0 25 0 1 0 1726145436 8384512 1944 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2047 1944 145 145 0 1902 0
[pid=21542] vsize: 8188
Current children cumulated CPU time (s) 859.93
Current children cumulated vsize (Kb) 10312

[startup+870.064 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1964 0 2 0 86975 17 0 0 25 0 1 0 1726145436 8421376 1953 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2056 1953 145 145 0 1911 0
[pid=21542] vsize: 8224
Current children cumulated CPU time (s) 869.93
Current children cumulated vsize (Kb) 10348

[startup+880.064 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1964 0 2 0 87975 17 0 0 25 0 1 0 1726145436 8421376 1953 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2056 1953 145 145 0 1911 0
[pid=21542] vsize: 8224
Current children cumulated CPU time (s) 879.93
Current children cumulated vsize (Kb) 10348

[startup+890.064 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1964 0 2 0 88975 17 0 0 25 0 1 0 1726145436 8421376 1953 4294967295 134512640 135094434 3221224432 3221223024 134551469 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2056 1953 145 145 0 1911 0
[pid=21542] vsize: 8224
Current children cumulated CPU time (s) 889.93
Current children cumulated vsize (Kb) 10348

[startup+900.065 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1964 0 2 0 89976 17 0 0 25 0 1 0 1726145436 8421376 1953 4294967295 134512640 135094434 3221224432 3221223024 134557248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2056 1953 145 145 0 1911 0
[pid=21542] vsize: 8224
Current children cumulated CPU time (s) 899.94
Current children cumulated vsize (Kb) 10348

[startup+910.066 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 1991 0 2 0 90975 17 0 0 25 0 1 0 1726145436 8527872 1980 4294967295 134512640 135094434 3221224432 3221223088 134558022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2082 1980 145 145 0 1937 0
[pid=21542] vsize: 8328
Current children cumulated CPU time (s) 909.93
Current children cumulated vsize (Kb) 10452

[startup+920.067 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2072 0 2 0 91974 18 0 0 25 0 1 0 1726145436 8855552 2061 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 2162 2061 145 145 0 2017 0
[pid=21542] vsize: 8648
Current children cumulated CPU time (s) 919.93
Current children cumulated vsize (Kb) 10772

[startup+930.067 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2073 0 2 0 92973 19 0 0 25 0 1 0 1726145436 8859648 2062 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/21542/statm): 2163 2062 145 145 0 2018 0
[pid=21542] vsize: 8652
Current children cumulated CPU time (s) 929.93
Current children cumulated vsize (Kb) 10776

[startup+940.068 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2106 0 2 0 93972 19 0 0 25 0 1 0 1726145436 8994816 2095 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2196 2095 145 145 0 2051 0
[pid=21542] vsize: 8784
Current children cumulated CPU time (s) 939.92
Current children cumulated vsize (Kb) 10908

[startup+950.069 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2106 0 2 0 94972 19 0 0 25 0 1 0 1726145436 8994816 2095 4294967295 134512640 135094434 3221224432 3221223104 134556257 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2196 2095 145 145 0 2051 0
[pid=21542] vsize: 8784
Current children cumulated CPU time (s) 949.92
Current children cumulated vsize (Kb) 10908

[startup+960.069 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2106 0 2 0 95972 19 0 0 25 0 1 0 1726145436 8994816 2095 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2196 2095 145 145 0 2051 0
[pid=21542] vsize: 8784
Current children cumulated CPU time (s) 959.92
Current children cumulated vsize (Kb) 10908

[startup+970.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2106 0 2 0 96972 19 0 0 25 0 1 0 1726145436 8994816 2095 4294967295 134512640 135094434 3221224432 3221223024 134557221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2196 2095 145 145 0 2051 0
[pid=21542] vsize: 8784
Current children cumulated CPU time (s) 969.92
Current children cumulated vsize (Kb) 10908

[startup+980.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2108 0 2 0 97973 19 0 0 25 0 1 0 1726145436 8994816 2097 4294967295 134512640 135094434 3221224432 3221223088 134558208 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2196 2097 145 145 0 2051 0
[pid=21542] vsize: 8784
Current children cumulated CPU time (s) 979.93
Current children cumulated vsize (Kb) 10908

[startup+990.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2108 0 2 0 98973 19 0 0 25 0 1 0 1726145436 8994816 2097 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2196 2097 145 145 0 2051 0
[pid=21542] vsize: 8784
Current children cumulated CPU time (s) 989.93
Current children cumulated vsize (Kb) 10908

[startup+1000.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2109 0 2 0 99973 19 0 0 25 0 1 0 1726145436 8994816 2098 4294967295 134512640 135094434 3221224432 3221223088 134557771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2196 2098 145 145 0 2051 0
[pid=21542] vsize: 8784
Current children cumulated CPU time (s) 999.93
Current children cumulated vsize (Kb) 10908

[startup+1010.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 100973 19 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0
[pid=21542] vsize: 8816
Current children cumulated CPU time (s) 1009.93
Current children cumulated vsize (Kb) 10940

[startup+1020.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 101973 19 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0
[pid=21542] vsize: 8816
Current children cumulated CPU time (s) 1019.93
Current children cumulated vsize (Kb) 10940

[startup+1030.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 102974 19 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0
[pid=21542] vsize: 8816
Current children cumulated CPU time (s) 1029.94
Current children cumulated vsize (Kb) 10940

[startup+1040.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 103974 20 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0
[pid=21542] vsize: 8816
Current children cumulated CPU time (s) 1039.95
Current children cumulated vsize (Kb) 10940

[startup+1050.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 104974 20 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0
[pid=21542] vsize: 8816
Current children cumulated CPU time (s) 1049.95
Current children cumulated vsize (Kb) 10940

[startup+1060.07 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2114 0 2 0 105974 20 0 0 25 0 1 0 1726145436 9027584 2103 4294967295 134512640 135094434 3221224432 3221223120 134554751 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2204 2103 145 145 0 2059 0
[pid=21542] vsize: 8816
Current children cumulated CPU time (s) 1059.95
Current children cumulated vsize (Kb) 10940

[startup+1070.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2115 0 2 0 106974 20 0 0 25 0 1 0 1726145436 9027584 2104 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2204 2104 145 145 0 2059 0
[pid=21542] vsize: 8816
Current children cumulated CPU time (s) 1069.95
Current children cumulated vsize (Kb) 10940

[startup+1080.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2115 0 2 0 107975 20 0 0 25 0 1 0 1726145436 9027584 2104 4294967295 134512640 135094434 3221224432 3221223088 134557925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2204 2104 145 145 0 2059 0
[pid=21542] vsize: 8816
Current children cumulated CPU time (s) 1079.96
Current children cumulated vsize (Kb) 10940

[startup+1090.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2125 0 2 0 108975 20 0 0 25 0 1 0 1726145436 9093120 2114 4294967295 134512640 135094434 3221224432 3221222912 134781511 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2220 2114 145 145 0 2075 0
[pid=21542] vsize: 8880
Current children cumulated CPU time (s) 1089.96
Current children cumulated vsize (Kb) 11004

[startup+1100.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2130 0 2 0 109975 20 0 0 25 0 1 0 1726145436 9125888 2119 4294967295 134512640 135094434 3221224432 3221223024 134557389 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2228 2119 145 145 0 2083 0
[pid=21542] vsize: 8912
Current children cumulated CPU time (s) 1099.96
Current children cumulated vsize (Kb) 11036

[startup+1110.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2130 0 2 0 110975 20 0 0 25 0 1 0 1726145436 9125888 2119 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2228 2119 145 145 0 2083 0
[pid=21542] vsize: 8912
Current children cumulated CPU time (s) 1109.96
Current children cumulated vsize (Kb) 11036

[startup+1120.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2130 0 2 0 111975 20 0 0 25 0 1 0 1726145436 9125888 2119 4294967295 134512640 135094434 3221224432 3221223024 134557528 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2228 2119 145 145 0 2083 0
[pid=21542] vsize: 8912
Current children cumulated CPU time (s) 1119.96
Current children cumulated vsize (Kb) 11036

[startup+1130.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2130 0 2 0 112975 20 0 0 25 0 1 0 1726145436 9125888 2119 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2228 2119 145 145 0 2083 0
[pid=21542] vsize: 8912
Current children cumulated CPU time (s) 1129.96
Current children cumulated vsize (Kb) 11036

[startup+1140.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2130 0 2 0 113976 20 0 0 25 0 1 0 1726145436 9125888 2119 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2228 2119 145 145 0 2083 0
[pid=21542] vsize: 8912
Current children cumulated CPU time (s) 1139.97
Current children cumulated vsize (Kb) 11036

[startup+1150.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2135 0 2 0 114976 20 0 0 25 0 1 0 1726145436 9158656 2124 4294967295 134512640 135094434 3221224432 3221223024 134551897 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2236 2124 145 145 0 2091 0
[pid=21542] vsize: 8944
Current children cumulated CPU time (s) 1149.97
Current children cumulated vsize (Kb) 11068

[startup+1160.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2140 0 2 0 115976 20 0 0 25 0 1 0 1726145436 9191424 2129 4294967295 134512640 135094434 3221224432 3221223104 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2244 2129 145 145 0 2099 0
[pid=21542] vsize: 8976
Current children cumulated CPU time (s) 1159.97
Current children cumulated vsize (Kb) 11100

[startup+1170.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2140 0 2 0 116976 20 0 0 25 0 1 0 1726145436 9191424 2129 4294967295 134512640 135094434 3221224432 3221223072 134562224 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2244 2129 145 145 0 2099 0
[pid=21542] vsize: 8976
Current children cumulated CPU time (s) 1169.97
Current children cumulated vsize (Kb) 11100

[startup+1180.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2140 0 2 0 117977 20 0 0 25 0 1 0 1726145436 9191424 2129 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2244 2129 145 145 0 2099 0
[pid=21542] vsize: 8976
Current children cumulated CPU time (s) 1179.98
Current children cumulated vsize (Kb) 11100

[startup+1190.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2140 0 2 0 118977 20 0 0 25 0 1 0 1726145436 9191424 2129 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2244 2129 145 145 0 2099 0
[pid=21542] vsize: 8976
Current children cumulated CPU time (s) 1189.98
Current children cumulated vsize (Kb) 11100

[startup+1200.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2140 0 2 0 119977 20 0 0 25 0 1 0 1726145436 9191424 2129 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2244 2129 145 145 0 2099 0
[pid=21542] vsize: 8976
Current children cumulated CPU time (s) 1199.98
Current children cumulated vsize (Kb) 11100

[startup+1210.08 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2146 0 2 0 120977 20 0 0 25 0 1 0 1726145436 9224192 2135 4294967295 134512640 135094434 3221224432 3221223024 134556843 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2252 2135 145 145 0 2107 0
[pid=21542] vsize: 9008
Current children cumulated CPU time (s) 1209.98
Current children cumulated vsize (Kb) 11132



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.97 0.94 2/58 21542
Raw data (/proc/21538/stat): 21538 (minisat+_script) S 21537 21538 17733 0 -1 0 289 239 0 0 0 0 0 1 21 0 1 0 1726145431 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/21538/statm): 531 226 485 147 0 384 0
[pid=21538] vsize: 2124
Raw data (/proc/21542/stat): 21542 (minisat+_64-bit) R 21538 21538 17733 0 -1 0 2146 0 2 0 120977 20 0 0 25 0 1 0 1726145436 9224192 2135 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/21542/statm): 2252 2135 145 145 0 2107 0
[pid=21542] vsize: 9008
Current children cumulated CPU time (s) 1209.98
Current children cumulated vsize (Kb) 11132

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

Child status: 0
Real time (s): 1210.09
CPU time (s): 1209.99
CPU user time (s): 1209.78
CPU system time (s): 0.210967
CPU usage (%): 99.9912
Max. virtual memory (cumulated for all children) (Kb): 11132

Verifier Data

ERROR: no interpretation found !