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

Nameweb/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-2.opb
MD5SUM409f1cf0658f035df65cb61f3e4f598e
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -30
Optimality of the best value was proved NO
Number of terms in the objective function 595
Biggest coefficient in the objective function 1
Number of bits for the biggest coefficient in the objective function 1
Sum of the numbers in the objective function 595
Number of bits of the sum of numbers in the objective function 10
Biggest number in a constraint 1
Number of bits of the biggest number in a constraint 1
Biggest sum of numbers in a constraint 595
Number of bits of the biggest sum of numbers10
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1195.03
Number of variables595
Total number of constraints27847
Number of constraints which are clauses27847
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints0
Minimum length of a constraint2
Maximum length of a constraint2

Trace number 2285

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        922200 kB
Buffers:         34512 kB
Cached:          50676 kB
SwapCached:        832 kB
Active:          60996 kB
Inactive:        26816 kB
HighTotal:      131008 kB
HighFree:        79548 kB
LowTotal:       903652 kB
LowFree:        842652 kB
SwapTotal:     2097892 kB
SwapFree:      2096460 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            18996 kB
Committed_AS:    64184 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-18 18:59:39 (client local time) WITH STATUS 10 IN 1209.38 SECONDS
stats: 2691 7 1209.38 10

Solver Data

c Parsing PB file...
c Converting 27847 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .......................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   27847    55694 |    9282       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -24
c ---[   0]---> Sorter-cost:26814     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   56112   122082 |   18704       0        0     nan |  0.000 % |
c |       100 |   55441   120669 |   20574      62      485     7.8 |  1.950 % |
c |       252 |   54383   118381 |   22631     186     1801     9.7 |  5.130 % |
c |       477 |   53349   116119 |   24895     313     3077     9.8 |  8.306 % |
c |       814 |   51759   112535 |   27384     516     5065     9.8 | 13.461 % |
c |      1321 |   49950   108452 |   30122     920     9543    10.4 | 19.341 % |
c ==============================================================================
c Found solution: -26
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1658 |   48453   105089 |   16151    1166    13758    11.8 | 19.341 % |
c |      1758 |   48207   104544 |   17766    1257    15573    12.4 | 25.098 % |
c |      1908 |   47653   103297 |   19542    1386    16993    12.3 | 26.885 % |
c |      2133 |   47022   101840 |   21496    1582    20176    12.8 | 29.018 % |
c |      2471 |   45334    97977 |   23646    1783    22714    12.7 | 34.745 % |
c |      2977 |   43116    92786 |   26011    2128    28051    13.2 | 41.789 % |
c ==============================================================================
c Found solution: -27
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3108 |   42804    92166 |   14268    2242    29536    13.2 | 41.789 % |
c |      3208 |   42633    91773 |   15694    2311    32120    13.9 | 43.581 % |
c |      3358 |   42086    90483 |   17264    2410    34663    14.4 | 45.442 % |
c |      3583 |   41186    88373 |   18990    2527    36936    14.6 | 48.512 % |
c |      3920 |   39875    85257 |   20889    2675    39865    14.9 | 53.073 % |
c |      4427 |   38250    81393 |   22978    2937    45919    15.6 | 58.815 % |
c |      5186 |   37415    79400 |   25276    3573    58638    16.4 | 61.715 % |
c ==============================================================================
c Found solution: -28
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5777 |   36536    77244 |   12178    3923    69803    17.8 | 61.715 % |
c |      5877 |   36375    76873 |   13395    4009    70834    17.7 | 65.308 % |
c |      6027 |   36111    76265 |   14735    4119    72852    17.7 | 66.182 % |
c |      6252 |   35833    75598 |   16208    4304    78604    18.3 | 67.328 % |
c |      6590 |   35525    74869 |   17829    4581    87877    19.2 | 68.259 % |
c |      7096 |   35132    73939 |   19612    5015   102250    20.4 | 69.626 % |
c |      7855 |   35004    73641 |   21574    5721   119858    21.0 | 70.063 % |
c |      8994 |   34621    72729 |   23731    6710   156327    23.3 | 71.405 % |
c |     10702 |   34449    72319 |   26104    8303   266846    32.1 | 72.007 % |
c ==============================================================================
c Found solution: -29
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10930 |   34398    72230 |   11466    8491   276955    32.6 | 72.007 % |
c |     11030 |   34307    72002 |   12612    8543   279040    32.7 | 72.564 % |
c |     11180 |   34307    72002 |   13873    8693   286044    32.9 | 72.564 % |
c |     11405 |   34227    71812 |   15261    8862   292699    33.0 | 72.846 % |
c |     11743 |   33985    71231 |   16787    9032   296460    32.8 | 73.704 % |
c |     12250 |   33985    71231 |   18466    9539   330834    34.7 | 73.704 % |
c |     13010 |   33963    71183 |   20312   10270   353365    34.4 | 73.770 % |
c |     14149 |   33552    70232 |   22343   11249   423515    37.6 | 75.141 % |
c |     15857 |   33222    69433 |   24578   12762   568784    44.6 | 76.291 % |
c |     18419 |   33120    69188 |   27036   15273   761555    49.9 | 76.651 % |
c |     22263 |   32930    68727 |   29739   18985  1120606    59.0 | 77.344 % |
c ==============================================================================
c Found solution: -30
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     26467 |   32657    68028 |   10885   22867  1465252    64.1 | 77.344 % |
c |     26567 |   32647    68006 |   11973   22966  1468382    63.9 | 78.332 % |
c |     26717 |   32647    68006 |   13170   23116  1476425    63.9 | 78.332 % |
c |     26942 |   32647    68006 |   14487   23341  1495373    64.1 | 78.332 % |
c |     27279 |   32477    67592 |   15936   23347  1512616    64.8 | 78.938 % |
c |     27785 |   32364    67313 |   17530   23764  1543363    64.9 | 79.364 % |
c |     28544 |   32254    67045 |   19283   24353  1597203    65.6 | 79.764 % |
c |     29683 |   32254    67045 |   21211   25492  1710400    67.1 | 79.764 % |
c |     31391 |   32254    67045 |   23332   27200  1919412    70.6 | 79.764 % |
c |     33955 |   32254    67045 |   25666   29764  2101826    70.6 | 79.764 % |
c ==============================================================================
c Found solution: -31
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35137 |   31980    66414 |   10660   30812  2169138    70.4 | 79.764 % |
c |     35238 |   31946    66328 |   11726   15491   930133    60.0 | 80.939 % |
c |     35389 |   31915    66258 |   12898   15639   935925    59.8 | 81.041 % |
c |     35614 |   31915    66258 |   14188   15864   948886    59.8 | 81.041 % |
c |     35951 |   31915    66258 |   15607   16201   965361    59.6 | 81.041 % |
c |     36458 |   31915    66258 |   17168   16708   996138    59.6 | 81.041 % |
c |     37217 |   31915    66258 |   18884   17467  1044393    59.8 | 81.041 % |
c |     38357 |   31910    66247 |   20773   18600  1113004    59.8 | 81.056 % |
c |     40065 |   31845    66095 |   22850   20288  1216954    60.0 | 81.276 % |
c |     42627 |   31804    65994 |   25135   22834  1375865    60.3 | 81.429 % |
c |     46471 |   31804    65994 |   27649   26678  1735048    65.0 | 81.429 % |
c |     52237 |   31510    65286 |   30414   32374  2209723    68.3 | 82.477 % |
c |     60886 |   31481    65217 |   33455   40961  2771939    67.7 | 82.579 % |
c |     73860 |   31477    65205 |   36801   19710   946500    48.0 | 82.600 % |
c |     93322 |   31477    65205 |   40481   39172  2462580    62.9 | 82.600 % |
c ==============================================================================
c Found solution: -32
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98887 |   31443    65100 |   10481   44676  2833202    63.4 | 82.600 % |
c |     98987 |   31443    65100 |   11529   17731   914127    51.6 | 82.724 % |
c |     99137 |   31443    65100 |   12682   17881   921601    51.5 | 82.724 % |
c |     99362 |   31405    65004 |   13950   18104   938348    51.8 | 82.867 % |
c |     99699 |   31381    64946 |   15345   18412   962309    52.3 | 82.954 % |
c |    100205 |   31381    64946 |   16879   18918  1006461    53.2 | 82.954 % |
c |    100964 |   31370    64919 |   18567   19674  1054745    53.6 | 82.995 % |
c |    102103 |   31370    64919 |   20424   20813  1143158    54.9 | 82.995 % |
c |    103813 |   31365    64908 |   22466   22519  1262523    56.1 | 83.011 % |
c |    106376 |   31365    64908 |   24713   25082  1418165    56.5 | 83.011 % |
c |    110222 |   31365    64908 |   27185   28928  1703939    58.9 | 83.011 % |
c |    115988 |   31330    64825 |   29903   34689  2037716    58.7 | 83.133 % |
c |    124637 |   31284    64708 |   32893   43252  2666638    61.7 | 83.307 % |
c |    137612 |   31239    64605 |   36183   22486   988221    43.9 | 83.450 % |
c |    157073 |   31239    64605 |   39801   41947  2056155    49.0 | 83.450 % |
c |    186265 |   31236    64598 |   43781   31773  1941768    61.1 | 83.460 % |
c |    230054 |   31231    64587 |   48159   32261  2906002    90.1 | 83.476 % |
c ==============================================================================
c Found solution: -33
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    278557 |   31244    64621 |   10414   32296  2237077    69.3 | 83.476 % |
c |    278658 |   31244    64621 |   11455   16249   954352    58.7 | 83.452 % |
c |    278809 |   31244    64621 |   12600   16400   966097    58.9 | 83.452 % |
c |    279034 |   31244    64621 |   13861   16625   981948    59.1 | 83.452 % |
c |    279372 |   31244    64621 |   15247   16963  1000566    59.0 | 83.452 % |
c |    279878 |   31244    64621 |   16771   17469  1034794    59.2 | 83.452 % |
c |    280638 |   31244    64621 |   18449   18229  1067205    58.5 | 83.452 % |
c |    281777 |   31244    64621 |   20293   19368  1125638    58.1 | 83.452 % |
c |    283486 |   31244    64621 |   22323   21077  1208886    57.4 | 83.452 % |
c |    286048 |   31244    64621 |   24555   23639  1365631    57.8 | 83.452 % |
c |    289893 |   31244    64621 |   27011   27484  1608741    58.5 | 83.452 % |
c |    295659 |   31207    64527 |   29712   33206  1964370    59.2 | 83.595 % |
c |    304308 |   31207    64527 |   32683   41855  2460979    58.8 | 83.595 % |
c |    317282 |   31197    64503 |   35951   22333   712494    31.9 | 83.630 % |
c |    336743 |   31197    64503 |   39547   41794  1397205    33.4 | 83.630 % |
c |    365935 |   31193    64493 |   43501   34344   952519    27.7 | 83.646 % |
c |    409725 |   31143    64373 |   47852   34709  1222470    35.2 | 83.824 % |
c |    475409 |   31136    64358 |   52637   54302  1647686    30.3 | 83.845 % |
c |    573935 |   31106    64290 |   57900   50437  1608080    31.9 | 83.942 % |

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/12763/stat): 12763 (minisat+_script) R 12762 12763 5929 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1843466770 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/12763/statm): 174 3 169 147 0 27 0
[pid=12763] 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=12764
New process pid=12765
New process pid=12766
execve syscall for /bin/sed executable
One traced child (pid=12765) 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=12766) exited with status: 0
One traced child (pid=12764) exited with status: 0
New process pid=12767
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc19/normalized-frb35-17-2.opb

[startup+10.0042 s]
Raw data (loadavg): 1.00 0.95 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 2152 0 0 0 979 8 0 0 25 0 1 0 1843466775 9752576 2139 4294967295 134512640 135094434 3221224448 3221223072 134557714 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 2381 2139 145 145 0 2236 0
[pid=12767] vsize: 9524
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 11648

[startup+20.006 s]
Raw data (loadavg): 1.00 0.95 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 2235 0 0 0 1978 9 0 0 25 0 1 0 1843466775 10092544 2222 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 2464 2222 145 145 0 2319 0
[pid=12767] vsize: 9856
Current children cumulated CPU time (s) 19.88
Current children cumulated vsize (Kb) 11980

[startup+30.0068 s]
Raw data (loadavg): 1.00 0.95 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 2852 0 0 0 2968 14 0 0 25 0 1 0 1843466775 12619776 2839 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 3081 2839 145 145 0 2936 0
[pid=12767] vsize: 12324
Current children cumulated CPU time (s) 29.83
Current children cumulated vsize (Kb) 14448

[startup+40.0076 s]
Raw data (loadavg): 1.00 0.95 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 3528 0 0 0 3954 21 0 0 25 0 1 0 1843466775 15429632 3515 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 3767 3515 145 145 0 3622 0
[pid=12767] vsize: 15068
Current children cumulated CPU time (s) 39.76
Current children cumulated vsize (Kb) 17192

[startup+50.0094 s]
Raw data (loadavg): 1.00 0.95 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 3944 0 0 0 4946 25 0 0 25 0 1 0 1843466775 17117184 3931 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 4179 3931 145 145 0 4034 0
[pid=12767] vsize: 16716
Current children cumulated CPU time (s) 49.72
Current children cumulated vsize (Kb) 18840

[startup+60.0092 s]
Raw data (loadavg): 1.00 0.95 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 4465 0 0 0 5935 29 0 0 25 0 1 0 1843466775 19230720 4452 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 4695 4452 145 145 0 4550 0
[pid=12767] vsize: 18780
Current children cumulated CPU time (s) 59.65
Current children cumulated vsize (Kb) 20904

[startup+70.01 s]
Raw data (loadavg): 1.00 0.95 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 4549 0 0 0 6933 30 0 0 25 0 1 0 1843466775 19570688 4536 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 4778 4536 145 145 0 4633 0
[pid=12767] vsize: 19112
Current children cumulated CPU time (s) 69.64
Current children cumulated vsize (Kb) 21236

[startup+80.0108 s]
Raw data (loadavg): 1.00 0.95 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 4549 0 0 0 7933 30 0 0 25 0 1 0 1843466775 19570688 4536 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 4778 4536 145 145 0 4633 0
[pid=12767] vsize: 19112
Current children cumulated CPU time (s) 79.64
Current children cumulated vsize (Kb) 21236

[startup+90.0116 s]
Raw data (loadavg): 1.00 0.96 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 4587 0 0 0 8932 30 0 0 25 0 1 0 1843466775 19722240 4574 4294967295 134512640 135094434 3221224448 3221223072 134557681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 4815 4574 145 145 0 4670 0
[pid=12767] vsize: 19260
Current children cumulated CPU time (s) 89.63
Current children cumulated vsize (Kb) 21384

[startup+100.012 s]
Raw data (loadavg): 1.00 0.96 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 4987 0 0 0 9925 34 0 0 25 0 1 0 1843466775 21471232 4974 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 5242 4974 145 145 0 5097 0
[pid=12767] vsize: 20968
Current children cumulated CPU time (s) 99.6
Current children cumulated vsize (Kb) 23092

[startup+110.013 s]
Raw data (loadavg): 1.00 0.96 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 5352 0 0 0 10918 37 0 0 25 0 1 0 1843466775 22949888 5339 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 5603 5339 145 145 0 5458 0
[pid=12767] vsize: 22412
Current children cumulated CPU time (s) 109.56
Current children cumulated vsize (Kb) 24536

[startup+120.014 s]
Raw data (loadavg): 1.00 0.96 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 5673 0 0 0 11911 41 0 0 25 0 1 0 1843466775 24244224 5660 4294967295 134512640 135094434 3221224448 3221223040 134557531 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 5919 5660 145 145 0 5774 0
[pid=12767] vsize: 23676
Current children cumulated CPU time (s) 119.53
Current children cumulated vsize (Kb) 25800

[startup+130.015 s]
Raw data (loadavg): 1.00 0.96 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 5963 0 0 0 12906 43 0 0 25 0 1 0 1843466775 25415680 5950 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6205 5950 145 145 0 6060 0
[pid=12767] vsize: 24820
Current children cumulated CPU time (s) 129.5
Current children cumulated vsize (Kb) 26944

[startup+140.016 s]
Raw data (loadavg): 1.00 0.96 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6040 0 0 0 13905 44 0 0 25 0 1 0 1843466775 25726976 6027 4294967295 134512640 135094434 3221224448 3221223104 134557875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6281 6027 145 145 0 6136 0
[pid=12767] vsize: 25124
Current children cumulated CPU time (s) 139.5
Current children cumulated vsize (Kb) 27248

[startup+150.016 s]
Raw data (loadavg): 1.00 0.96 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6040 0 0 0 14905 44 0 0 25 0 1 0 1843466775 25726976 6027 4294967295 134512640 135094434 3221224448 3221223040 134556826 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6281 6027 145 145 0 6136 0
[pid=12767] vsize: 25124
Current children cumulated CPU time (s) 149.5
Current children cumulated vsize (Kb) 27248

[startup+160.016 s]
Raw data (loadavg): 1.00 0.96 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6040 0 0 0 15904 44 0 0 25 0 1 0 1843466775 25726976 6027 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6281 6027 145 145 0 6136 0
[pid=12767] vsize: 25124
Current children cumulated CPU time (s) 159.49
Current children cumulated vsize (Kb) 27248

[startup+170.017 s]
Raw data (loadavg): 1.00 0.96 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6040 0 0 0 16904 44 0 0 25 0 1 0 1843466775 25726976 6027 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6281 6027 145 145 0 6136 0
[pid=12767] vsize: 25124
Current children cumulated CPU time (s) 169.49
Current children cumulated vsize (Kb) 27248

[startup+180.018 s]
Raw data (loadavg): 1.00 0.96 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6040 0 0 0 17903 45 0 0 25 0 1 0 1843466775 25726976 6027 4294967295 134512640 135094434 3221224448 3221223104 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6281 6027 145 145 0 6136 0
[pid=12767] vsize: 25124
Current children cumulated CPU time (s) 179.49
Current children cumulated vsize (Kb) 27248

[startup+190.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 18903 45 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 189.49
Current children cumulated vsize (Kb) 27404

[startup+200.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 19903 46 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 199.5
Current children cumulated vsize (Kb) 27404

[startup+210.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 20902 46 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 209.49
Current children cumulated vsize (Kb) 27404

[startup+220.022 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 21902 47 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 219.5
Current children cumulated vsize (Kb) 27404

[startup+230.023 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 22901 47 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557890 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 229.49
Current children cumulated vsize (Kb) 27404

[startup+240.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 23899 49 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 239.49
Current children cumulated vsize (Kb) 27404

[startup+250.025 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 24898 51 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557813 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 249.5
Current children cumulated vsize (Kb) 27404

[startup+260.025 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 25897 51 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557945 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 259.49
Current children cumulated vsize (Kb) 27404

[startup+270.026 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 26896 52 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223088 134562165 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 269.49
Current children cumulated vsize (Kb) 27404

[startup+280.027 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 27895 53 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223136 134554793 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 279.49
Current children cumulated vsize (Kb) 27404

[startup+290.029 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 28895 53 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 289.49
Current children cumulated vsize (Kb) 27404

[startup+300.03 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 29894 54 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 299.49
Current children cumulated vsize (Kb) 27404

[startup+310.029 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6060 0 0 0 30894 55 0 0 25 0 1 0 1843466775 25886720 6047 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6047 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 309.5
Current children cumulated vsize (Kb) 27404

[startup+320.03 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6062 0 0 0 31893 55 0 0 25 0 1 0 1843466775 25886720 6049 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6320 6049 145 145 0 6175 0
[pid=12767] vsize: 25280
Current children cumulated CPU time (s) 319.49
Current children cumulated vsize (Kb) 27404

[startup+330.031 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6088 0 0 0 32892 56 0 0 25 0 1 0 1843466775 25980928 6075 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6343 6075 145 145 0 6198 0
[pid=12767] vsize: 25372
Current children cumulated CPU time (s) 329.49
Current children cumulated vsize (Kb) 27496

[startup+340.032 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6088 0 0 0 33892 56 0 0 25 0 1 0 1843466775 25980928 6075 4294967295 134512640 135094434 3221224448 3221223040 134556847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6343 6075 145 145 0 6198 0
[pid=12767] vsize: 25372
Current children cumulated CPU time (s) 339.49
Current children cumulated vsize (Kb) 27496

[startup+350.033 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6088 0 0 0 34892 57 0 0 25 0 1 0 1843466775 25980928 6075 4294967295 134512640 135094434 3221224448 3221223104 134558232 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6343 6075 145 145 0 6198 0
[pid=12767] vsize: 25372
Current children cumulated CPU time (s) 349.5
Current children cumulated vsize (Kb) 27496

[startup+360.033 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6088 0 0 0 35892 57 0 0 25 0 1 0 1843466775 25980928 6075 4294967295 134512640 135094434 3221224448 3221223120 134555991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6343 6075 145 145 0 6198 0
[pid=12767] vsize: 25372
Current children cumulated CPU time (s) 359.5
Current children cumulated vsize (Kb) 27496

[startup+370.034 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6093 0 0 0 36891 57 0 0 25 0 1 0 1843466775 26009600 6080 4294967295 134512640 135094434 3221224448 3221223072 134557675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6350 6080 145 145 0 6205 0
[pid=12767] vsize: 25400
Current children cumulated CPU time (s) 369.49
Current children cumulated vsize (Kb) 27524

[startup+380.035 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6093 0 0 0 37890 58 0 0 25 0 1 0 1843466775 26009600 6080 4294967295 134512640 135094434 3221224448 3221223092 134558261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6350 6080 145 145 0 6205 0
[pid=12767] vsize: 25400
Current children cumulated CPU time (s) 379.49
Current children cumulated vsize (Kb) 27524

[startup+390.036 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6496 0 0 0 38882 62 0 0 25 0 1 0 1843466775 27660288 6483 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 6753 6483 145 145 0 6608 0
[pid=12767] vsize: 27012
Current children cumulated CPU time (s) 389.45
Current children cumulated vsize (Kb) 29136

[startup+400.038 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 6873 0 0 0 39875 65 0 0 25 0 1 0 1843466775 29208576 6860 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 7131 6860 145 145 0 6986 0
[pid=12767] vsize: 28524
Current children cumulated CPU time (s) 399.41
Current children cumulated vsize (Kb) 30648

[startup+410.038 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7325 0 0 0 40865 69 0 0 25 0 1 0 1843466775 31059968 7312 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 7583 7312 145 145 0 7438 0
[pid=12767] vsize: 30332
Current children cumulated CPU time (s) 409.35
Current children cumulated vsize (Kb) 32456

[startup+420.039 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 41857 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223120 134556450 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0
[pid=12767] vsize: 31884
Current children cumulated CPU time (s) 419.3
Current children cumulated vsize (Kb) 34008

[startup+430.04 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 42857 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0
[pid=12767] vsize: 31884
Current children cumulated CPU time (s) 429.3
Current children cumulated vsize (Kb) 34008

[startup+440.041 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 43857 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134558141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0
[pid=12767] vsize: 31884
Current children cumulated CPU time (s) 439.3
Current children cumulated vsize (Kb) 34008

[startup+450.042 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 44858 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0
[pid=12767] vsize: 31884
Current children cumulated CPU time (s) 449.31
Current children cumulated vsize (Kb) 34008

[startup+460.041 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 45858 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0
[pid=12767] vsize: 31884
Current children cumulated CPU time (s) 459.31
Current children cumulated vsize (Kb) 34008

[startup+470.042 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 46858 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223084 134557560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0
[pid=12767] vsize: 31884
Current children cumulated CPU time (s) 469.31
Current children cumulated vsize (Kb) 34008

[startup+480.042 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 47858 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0
[pid=12767] vsize: 31884
Current children cumulated CPU time (s) 479.31
Current children cumulated vsize (Kb) 34008

[startup+490.043 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 48858 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0
[pid=12767] vsize: 31884
Current children cumulated CPU time (s) 489.31
Current children cumulated vsize (Kb) 34008

[startup+500.044 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7716 0 0 0 49859 72 0 0 25 0 1 0 1843466775 32649216 7703 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 7971 7703 145 145 0 7826 0
[pid=12767] vsize: 31884
Current children cumulated CPU time (s) 499.32
Current children cumulated vsize (Kb) 34008

[startup+510.043 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 7988 0 0 0 50854 74 0 0 25 0 1 0 1843466775 33763328 7975 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8243 7975 145 145 0 8098 0
[pid=12767] vsize: 32972
Current children cumulated CPU time (s) 509.29
Current children cumulated vsize (Kb) 35096

[startup+520.044 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8273 0 0 0 51849 77 0 0 25 0 1 0 1843466775 34926592 8260 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8527 8260 145 145 0 8382 0
[pid=12767] vsize: 34108
Current children cumulated CPU time (s) 519.27
Current children cumulated vsize (Kb) 36232

[startup+530.045 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8543 0 0 0 52844 79 0 0 25 0 1 0 1843466775 36032512 8530 4294967295 134512640 135094434 3221224448 3221223104 134557900 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8797 8530 145 145 0 8652 0
[pid=12767] vsize: 35188
Current children cumulated CPU time (s) 529.24
Current children cumulated vsize (Kb) 37312

[startup+540.046 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 53844 79 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557859 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 539.24
Current children cumulated vsize (Kb) 37792

[startup+550.047 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 54844 79 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 549.24
Current children cumulated vsize (Kb) 37792

[startup+560.048 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 55844 80 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223236 134553508 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 559.25
Current children cumulated vsize (Kb) 37792

[startup+570.048 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 56843 80 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 569.24
Current children cumulated vsize (Kb) 37792

[startup+580.049 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 57842 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 579.24
Current children cumulated vsize (Kb) 37792

[startup+590.05 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 58842 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 589.24
Current children cumulated vsize (Kb) 37792

[startup+600.051 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 59842 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 599.24
Current children cumulated vsize (Kb) 37792

[startup+610.051 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 60842 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 609.24
Current children cumulated vsize (Kb) 37792

[startup+620.051 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 61843 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223136 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 619.25
Current children cumulated vsize (Kb) 37792

[startup+630.052 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 62843 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 629.25
Current children cumulated vsize (Kb) 37792

[startup+640.053 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 63843 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223072 134557583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 639.25
Current children cumulated vsize (Kb) 37792

[startup+650.054 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 64843 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 649.25
Current children cumulated vsize (Kb) 37792

[startup+660.055 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 65843 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 659.25
Current children cumulated vsize (Kb) 37792

[startup+670.055 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 66844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 669.26
Current children cumulated vsize (Kb) 37792

[startup+680.055 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 67844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 679.26
Current children cumulated vsize (Kb) 37792

[startup+690.056 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 68844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 689.26
Current children cumulated vsize (Kb) 37792

[startup+700.057 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 69844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 699.26
Current children cumulated vsize (Kb) 37792

[startup+710.057 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 70844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134558218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 709.26
Current children cumulated vsize (Kb) 37792

[startup+720.057 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 71844 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 719.26
Current children cumulated vsize (Kb) 37792

[startup+730.057 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 72845 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223120 134556288 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 729.27
Current children cumulated vsize (Kb) 37792

[startup+740.058 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8600 0 0 0 73845 81 0 0 25 0 1 0 1843466775 36524032 8587 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8587 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 739.27
Current children cumulated vsize (Kb) 37792

[startup+750.059 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 74845 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134558172 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 749.27
Current children cumulated vsize (Kb) 37792

[startup+760.059 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 75845 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 759.27
Current children cumulated vsize (Kb) 37792

[startup+770.059 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 76846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 769.28
Current children cumulated vsize (Kb) 37792

[startup+780.06 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 77846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223040 134551454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 779.28
Current children cumulated vsize (Kb) 37792

[startup+790.061 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 78846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 789.28
Current children cumulated vsize (Kb) 37792

[startup+800.062 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 79846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 799.28
Current children cumulated vsize (Kb) 37792

[startup+810.063 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 80846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223120 134556244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 809.28
Current children cumulated vsize (Kb) 37792

[startup+820.063 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 81846 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 819.28
Current children cumulated vsize (Kb) 37792

[startup+830.064 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 82847 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 829.29
Current children cumulated vsize (Kb) 37792

[startup+840.065 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 83847 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 839.29
Current children cumulated vsize (Kb) 37792

[startup+850.066 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 84847 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223120 134556410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 849.29
Current children cumulated vsize (Kb) 37792

[startup+860.067 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 85847 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223040 134556817 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 859.29
Current children cumulated vsize (Kb) 37792

[startup+870.067 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 86847 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 869.29
Current children cumulated vsize (Kb) 37792

[startup+880.068 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 87848 81 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 879.3
Current children cumulated vsize (Kb) 37792

[startup+890.07 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 88848 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223120 134555889 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 889.31
Current children cumulated vsize (Kb) 37792

[startup+900.071 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 89848 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 899.31
Current children cumulated vsize (Kb) 37792

[startup+910.072 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 90848 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 909.31
Current children cumulated vsize (Kb) 37792

[startup+920.073 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 91849 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 919.32
Current children cumulated vsize (Kb) 37792

[startup+930.073 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 92849 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 929.32
Current children cumulated vsize (Kb) 37792

[startup+940.074 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 93849 82 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 939.32
Current children cumulated vsize (Kb) 37792

[startup+950.076 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8601 0 0 0 94848 83 0 0 25 0 1 0 1843466775 36524032 8588 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 8917 8588 145 145 0 8772 0
[pid=12767] vsize: 35668
Current children cumulated CPU time (s) 949.32
Current children cumulated vsize (Kb) 37792

[startup+960.076 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8615 0 0 0 95847 83 0 0 25 0 1 0 1843466775 36638720 8602 4294967295 134512640 135094434 3221224448 3221223104 134557914 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8602 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 959.31
Current children cumulated vsize (Kb) 37904

[startup+970.077 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8616 0 0 0 96848 83 0 0 25 0 1 0 1843466775 36638720 8603 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8603 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 969.32
Current children cumulated vsize (Kb) 37904

[startup+980.077 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 97848 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 979.32
Current children cumulated vsize (Kb) 37904

[startup+990.078 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 98848 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 989.32
Current children cumulated vsize (Kb) 37904

[startup+1000.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 99848 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134558227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 999.32
Current children cumulated vsize (Kb) 37904

[startup+1010.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 100848 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1009.32
Current children cumulated vsize (Kb) 37904

[startup+1020.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 101849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223040 134557137 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1019.33
Current children cumulated vsize (Kb) 37904

[startup+1030.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 102849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223120 134556242 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1029.33
Current children cumulated vsize (Kb) 37904

[startup+1040.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 103849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1039.33
Current children cumulated vsize (Kb) 37904

[startup+1050.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 104849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1049.33
Current children cumulated vsize (Kb) 37904

[startup+1060.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 105849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1059.33
Current children cumulated vsize (Kb) 37904

[startup+1070.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8621 0 0 0 106849 83 0 0 25 0 1 0 1843466775 36638720 8608 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8608 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1069.33
Current children cumulated vsize (Kb) 37904

[startup+1080.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 107850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1079.34
Current children cumulated vsize (Kb) 37904

[startup+1090.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 108850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223040 134557331 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1089.34
Current children cumulated vsize (Kb) 37904

[startup+1100.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 109850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223072 134557585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1099.34
Current children cumulated vsize (Kb) 37904

[startup+1110.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 110850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134558235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1109.34
Current children cumulated vsize (Kb) 37904

[startup+1120.08 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 111850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1119.34
Current children cumulated vsize (Kb) 37904

[startup+1130.09 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 112851 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1129.35
Current children cumulated vsize (Kb) 37904

[startup+1140.09 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 113851 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1139.35
Current children cumulated vsize (Kb) 37904

[startup+1150.09 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 114850 83 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1149.34
Current children cumulated vsize (Kb) 37904

[startup+1160.09 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 115850 84 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223120 134555943 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1159.35
Current children cumulated vsize (Kb) 37904

[startup+1170.09 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 116851 84 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1169.36
Current children cumulated vsize (Kb) 37904

[startup+1180.09 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8622 0 0 0 117851 84 0 0 25 0 1 0 1843466775 36638720 8609 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8609 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1179.36
Current children cumulated vsize (Kb) 37904

[startup+1190.09 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8626 0 0 0 118851 84 0 0 25 0 1 0 1843466775 36638720 8613 4294967295 134512640 135094434 3221224448 3221223072 134562057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8613 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1189.36
Current children cumulated vsize (Kb) 37904

[startup+1200.09 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8627 0 0 0 119851 84 0 0 25 0 1 0 1843466775 36638720 8614 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8614 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1199.36
Current children cumulated vsize (Kb) 37904

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8627 0 0 0 120851 84 0 0 25 0 1 0 1843466775 36638720 8614 4294967295 134512640 135094434 3221224448 3221223072 134562152 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8614 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1209.36
Current children cumulated vsize (Kb) 37904



Maximum CPU time exceeded: sending SIGTERM then SIGKILL

[startup+1210.09 s]
Raw data (loadavg): 1.00 0.97 0.95 2/57 12767
Raw data (/proc/12763/stat): 12763 (minisat+_script) S 12762 12763 5929 0 -1 0 288 239 0 0 0 1 0 0 22 0 1 0 1843466770 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/12763/statm): 531 226 485 147 0 384 0
[pid=12763] vsize: 2124
Raw data (/proc/12767/stat): 12767 (minisat+_64-bit) R 12763 12763 5929 0 -1 0 8627 0 0 0 120851 84 0 0 25 0 1 0 1843466775 36638720 8614 4294967295 134512640 135094434 3221224448 3221223104 134558221 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/12767/statm): 8945 8614 145 145 0 8800 0
[pid=12767] vsize: 35780
Current children cumulated CPU time (s) 1209.36
Current children cumulated vsize (Kb) 37904

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

Child status: 10
Real time (s): 1210.11
CPU time (s): 1209.38
CPU user time (s): 1208.52
CPU system time (s): 0.861868
CPU usage (%): 99.9396
Max. virtual memory (cumulated for all children) (Kb): 37904

Verifier Data

ERROR: no interpretation found !