Some explanations

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

General information on the benchmark

Namemps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-lseu.opb
MD5SUM5fcfa2f72175b9723ffb2781fb76fcdc
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 1120
Optimality of the best value was proved YES
Number of terms in the objective function 85
Biggest coefficient in the objective function 517
Number of bits for the biggest coefficient in the objective function 10
Sum of the numbers in the objective function 15494
Number of bits of the sum of numbers in the objective function 14
Biggest number in a constraint 1656
Number of bits of the biggest number in a constraint 11
Biggest sum of numbers in a constraint 15494
Number of bits of the biggest sum of numbers14
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark661.783
Number of variables89
Total number of constraints117
Number of constraints which are clauses2
Number of constraints which are cardinality constraints (but not clauses)104
Number of constraints which are nor clauses,nor cardinality constraints11
Minimum length of a constraint1
Maximum length of a constraint47

Trace number 6104

Launcher Data

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        839320 kB
Buffers:         31128 kB
Cached:         134276 kB
SwapCached:        788 kB
Active:          53448 kB
Inactive:       114448 kB
HighTotal:      131008 kB
HighFree:        23464 kB
LowTotal:       903652 kB
LowFree:        815856 kB
SwapTotal:     2097892 kB
SwapFree:      2096456 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5700 kB
Slab:            21712 kB
Committed_AS:    64332 kB
PageTables:        340 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:40:24 (client local time) WITH STATUS 30 IN 661.783 SECONDS
stats: 3280 0 661.783 30

Solver Data

c Parsing PB file...
c Converting 28 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #
c   -- Clauses(.)/Splits(s): ...s..
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:    7
c ---[  26]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    3
c ---[  23]---> BDD-cost:    5
c ---[  22]---> BDD-cost:   11
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    7
c ---[  19]---> BDD-cost:    3
c ---[  18]---> BDD-cost:    7
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    5
c ---[  14]---> BDD-cost:    3
c ---[  12]---> BDD-cost:    7
c ---[   9]---> Sorter-cost: 3170     Base: 5 2 2 3
c ---[   8]---> BDD-cost:   28
c ---[   7]---> BDD-cost:  202
c ---[   6]---> Sorter-cost: 1878     Base: 5 2 2 3
c ---[   4]---> Sorter-cost: 1741     Base: 5 2 2 2
c ---[   2]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   32
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   16046    38074 |    5348       0        0     nan |  0.000 % |
c |       101 |   15986    37942 |    5882      99     1341    13.5 |  0.826 % |
c ==============================================================================
c Found solution: 3697
c ---[   0]---> Sorter-cost:12454     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       202 |   44688   105076 |   14896     173     2195    12.7 |  0.826 % |
c ==============================================================================
c Found solution: 3371
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       256 |   44990   105888 |   14996     226     2982    13.2 |  0.826 % |
c |       356 |   43633   102789 |   16495     292     3359    11.5 |  3.986 % |
c |       507 |   43603   102719 |   18145     441     4465    10.1 |  4.039 % |
c |       733 |   42927   101162 |   19959     655     8311    12.7 |  5.281 % |
c |      1070 |   42674   100581 |   21955     987    12553    12.7 |  5.716 % |
c |      1581 |   41908    98827 |   24151    1477    21494    14.6 |  7.053 % |
c ==============================================================================
c Found solution: 3322
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1681 |   41980    99026 |   13993    1559    22101    14.2 |  7.053 % |
c ==============================================================================
c Found solution: 3266
c ---[   0]---> Sorter-cost:    6     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1699 |   42327    99876 |   14109    1577    22632    14.4 |  7.053 % |
c |      1799 |   42177    99527 |   15519    1666    25015    15.0 |  7.434 % |
c ==============================================================================
c Found solution: 3256
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1848 |   42261    99747 |   14087    1715    26486    15.4 |  7.434 % |
c |      1948 |   42261    99747 |   15495    1815    27050    14.9 |  7.424 % |
c |      2099 |   42224    99662 |   17045    1963    29077    14.8 |  7.494 % |
c ==============================================================================
c Found solution: 2378
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2173 |   42342    99948 |   14114    2037    30298    14.9 |  7.494 % |
c |      2273 |   40889    96607 |   15525    2082    31508    15.1 | 10.064 % |
c |      2423 |   40747    96295 |   17077    2230    38797    17.4 | 10.314 % |
c ==============================================================================
c Found solution: 2053
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2639 |   40757    96342 |   13585    2445    47397    19.4 | 10.314 % |
c |      2740 |   40697    96205 |   14943    2543    49595    19.5 | 10.462 % |
c |      2891 |   40697    96205 |   16437    2694    52472    19.5 | 10.462 % |
c |      3119 |   40389    95500 |   18081    2918    57025    19.5 | 11.032 % |
c |      3458 |   40186    95030 |   19889    3252    68502    21.1 | 11.363 % |
c ==============================================================================
c Found solution: 2037
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3836 |   40320    95376 |   13440    3628    85309    23.5 | 11.363 % |
c |      3936 |   40286    95298 |   14784    3716    86903    23.4 | 11.496 % |
c ==============================================================================
c Found solution: 1955
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3980 |   40237    95215 |   13412    3759    88809    23.6 | 11.496 % |
c |      4080 |   40237    95215 |   14753    3859    89989    23.3 | 11.595 % |
c |      4230 |   40237    95215 |   16228    4009    94858    23.7 | 11.595 % |
c |      4455 |   40237    95215 |   17851    4234   106663    25.2 | 11.595 % |
c |      4792 |   40237    95215 |   19636    4571   129714    28.4 | 11.595 % |
c |      5299 |   40168    95064 |   21600    5070   155326    30.6 | 11.728 % |
c |      6058 |   40067    94833 |   23760    5826   206079    35.4 | 11.936 % |
c |      7198 |   40035    94764 |   26136    6963   270614    38.9 | 12.011 % |
c |      8909 |   37164    88133 |   28749    8599   344207    40.0 | 17.102 % |
c ==============================================================================
c Found solution: 1950
c ---[   0]---> Sorter-cost:    7     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10282 |   36034    85530 |   12011    9929   416384    41.9 | 17.102 % |
c |     10387 |   36034    85530 |   13212   10034   417773    41.6 | 19.346 % |
c |     10537 |   36034    85530 |   14533   10184   421049    41.3 | 19.346 % |
c |     10765 |   36034    85530 |   15986   10412   430808    41.4 | 19.346 % |
c |     11102 |   36034    85530 |   17585   10749   448087    41.7 | 19.346 % |
c |     11608 |   36034    85530 |   19343   11255   462432    41.1 | 19.346 % |
c ==============================================================================
c Found solution: 1850
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11882 |   36052    85587 |   12017   11529   471731    40.9 | 19.346 % |
c |     11982 |   36052    85587 |   13218   11629   474845    40.8 | 19.338 % |
c ==============================================================================
c Found solution: 1841
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12017 |   36059    85619 |   12019   11664   476260    40.8 | 19.338 % |
c |     12117 |   36059    85619 |   13220   11764   482121    41.0 | 19.338 % |
c |     12267 |   36059    85619 |   14542   11914   488323    41.0 | 19.338 % |
c |     12493 |   36004    85490 |   15997   12135   500186    41.2 | 19.453 % |
c |     12831 |   36004    85490 |   17597   12473   513216    41.1 | 19.453 % |
c |     13339 |   35900    85252 |   19356   12973   535678    41.3 | 19.631 % |
c |     14098 |   35900    85252 |   21292   13732   565749    41.2 | 19.631 % |
c |     15238 |   35900    85252 |   23421   14872   632272    42.5 | 19.631 % |
c |     16946 |   35900    85252 |   25763   16580   718187    43.3 | 19.631 % |
c |     19508 |   35861    85162 |   28340   19141   820839    42.9 | 19.706 % |
c ==============================================================================
c Found solution: 1831
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20797 |   35868    85178 |   11956   20430   868635    42.5 | 19.706 % |
c ==============================================================================
c Found solution: 1800
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     20822 |   35875    85194 |   11958   10240   370925    36.2 | 19.706 % |
c |     20922 |   35875    85194 |   13153   10340   376338    36.4 | 19.709 % |
c |     21073 |   35820    85065 |   14469   10484   379199    36.2 | 19.812 % |
c |     21298 |   35820    85065 |   15916   10709   384451    35.9 | 19.812 % |
c |     21635 |   35820    85065 |   17507   11046   403641    36.5 | 19.812 % |
c |     22141 |   35797    85013 |   19258   11551   425009    36.8 | 19.852 % |
c ==============================================================================
c Found solution: 1729
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     22401 |   35807    85052 |   11935   11811   435927    36.9 | 19.852 % |
c |     22503 |   35807    85052 |   13128   11913   437731    36.7 | 19.850 % |
c |     22654 |   35807    85052 |   14441   12064   440540    36.5 | 19.850 % |
c |     22882 |   35807    85052 |   15885   12292   449714    36.6 | 19.850 % |
c |     23220 |   35605    84581 |   17474   12628   457488    36.2 | 20.188 % |
c ==============================================================================
c Found solution: 1727
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23653 |   35611    84596 |   11870   13061   479394    36.7 | 20.188 % |
c ==============================================================================
c Found solution: 1683
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23732 |   35616    84608 |   11872   13140   483575    36.8 | 20.188 % |
c |     23832 |   35616    84608 |   13059   13240   487557    36.8 | 20.192 % |
c |     23983 |   35616    84608 |   14365   13391   493894    36.9 | 20.192 % |
c ==============================================================================
c Found solution: 1675
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     24036 |   35621    84619 |   11873   13444   495347    36.8 | 20.192 % |
c |     24136 |   35621    84619 |   13060   13544   503809    37.2 | 20.194 % |
c |     24286 |   35621    84619 |   14366   13694   506670    37.0 | 20.194 % |
c |     24512 |   35621    84619 |   15802   13920   519039    37.3 | 20.194 % |
c |     24849 |   35621    84619 |   17383   14257   537179    37.7 | 20.194 % |
c |     25355 |   35621    84619 |   19121   14763   550379    37.3 | 20.194 % |
c |     26114 |   35023    83235 |   21033   15466   571637    37.0 | 21.324 % |
c |     27253 |   35023    83235 |   23137   16605   619296    37.3 | 21.324 % |
c |     28963 |   35023    83235 |   25450   18315   687059    37.5 | 21.324 % |
c ==============================================================================
c Found solution: 1614
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     29392 |   35028    83246 |   11676   18744   708385    37.8 | 21.324 % |
c |     29492 |   35028    83246 |   12843    9472   290847    30.7 | 21.327 % |
c |     29642 |   34964    83098 |   14127    9621   294252    30.6 | 21.447 % |
c |     29869 |   34964    83098 |   15540    9848   299169    30.4 | 21.447 % |
c |     30208 |   34964    83098 |   17094   10187   308569    30.3 | 21.447 % |
c |     30714 |   34964    83098 |   18804   10693   320449    30.0 | 21.447 % |
c ==============================================================================
c Found solution: 1587
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31206 |   34978    83134 |   11659   11185   339724    30.4 | 21.447 % |
c |     31306 |   34978    83134 |   12824   11285   341955    30.3 | 21.442 % |
c |     31457 |   34978    83134 |   14107   11436   349352    30.5 | 21.442 % |
c ==============================================================================
c Found solution: 1570
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     31521 |   34985    83154 |   11661   11500   352534    30.7 | 21.442 % |
c |     31623 |   34985    83154 |   12827   11602   354369    30.5 | 21.442 % |
c |     31774 |   34985    83154 |   14109   11753   356599    30.3 | 21.442 % |
c |     32001 |   34985    83154 |   15520   11980   363253    30.3 | 21.442 % |
c |     32340 |   34985    83154 |   17072   12319   378819    30.8 | 21.442 % |
c |     32847 |   34985    83154 |   18780   12826   388215    30.3 | 21.442 % |
c |     33608 |   34985    83154 |   20658   13587   426121    31.4 | 21.442 % |
c |     34748 |   34985    83154 |   22723   14727   487779    33.1 | 21.442 % |
c |     36457 |   34985    83154 |   24996   16436   583123    35.5 | 21.442 % |
c |     39020 |   34801    82731 |   27496   18992   681940    35.9 | 21.745 % |
c ==============================================================================
c Found solution: 1517
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     41774 |   34808    82747 |   11602   21746   853274    39.2 | 21.745 % |
c |     41875 |   34808    82747 |   12762   10974   412117    37.6 | 21.746 % |
c |     42025 |   34808    82747 |   14038   11124   417783    37.6 | 21.746 % |
c |     42251 |   34808    82747 |   15442   11350   422061    37.2 | 21.746 % |
c |     42591 |   34808    82747 |   16986   11690   428663    36.7 | 21.746 % |
c |     43099 |   34808    82747 |   18685   12198   438542    36.0 | 21.746 % |
c |     43858 |   34808    82747 |   20553   12957   454152    35.1 | 21.746 % |
c |     44997 |   34808    82747 |   22609   14096   515846    36.6 | 21.746 % |
c ==============================================================================
c Found solution: 1516
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     45960 |   34815    82763 |   11605   15059   573361    38.1 | 21.746 % |
c |     46063 |   34815    82763 |   12765   15162   578306    38.1 | 21.747 % |
c |     46214 |   34815    82763 |   14042   15313   582046    38.0 | 21.747 % |
c |     46439 |   34815    82763 |   15446   15538   589238    37.9 | 21.747 % |
c ==============================================================================
c Found solution: 1503
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     46460 |   34820    82775 |   11606   15559   589681    37.9 | 21.747 % |
c |     46561 |   34820    82775 |   12766    7881   213609    27.1 | 21.749 % |
c |     46712 |   34820    82775 |   14043    8032   219155    27.3 | 21.749 % |
c |     46941 |   34820    82775 |   15447    8261   225582    27.3 | 21.749 % |
c |     47278 |   34820    82775 |   16992    8598   236302    27.5 | 21.749 % |
c |     47785 |   34820    82775 |   18691    9105   253128    27.8 | 21.749 % |
c |     48545 |   34652    82385 |   20560    9857   279243    28.3 | 22.070 % |
c ==============================================================================
c Found solution: 1455
c ---[   0]---> Sorter-cost:    1     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48864 |   34640    82360 |   11546   10174   303361    29.8 | 22.070 % |
c |     48966 |   34640    82360 |   12700   10276   305980    29.8 | 22.094 % |
c |     49117 |   34640    82360 |   13970   10427   313871    30.1 | 22.094 % |
c |     49342 |   34640    82360 |   15367   10652   325753    30.6 | 22.094 % |
c |     49679 |   34640    82360 |   16904   10989   339980    30.9 | 22.094 % |
c |     50187 |   34640    82360 |   18594   11497   359131    31.2 | 22.094 % |
c |     50948 |   34640    82360 |   20454   12258   394268    32.2 | 22.094 % |
c ==============================================================================
c Found solution: 1417
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     51133 |   34643    82367 |   11547   12443   404938    32.5 | 22.094 % |
c |     51233 |   34643    82367 |   12701   12543   406841    32.4 | 22.098 % |
c |     51383 |   34643    82367 |   13971   12693   415156    32.7 | 22.098 % |
c |     51608 |   34602    82270 |   15369   12916   422055    32.7 | 22.178 % |
c |     51947 |   34602    82270 |   16905   13255   442806    33.4 | 22.178 % |
c |     52453 |   34602    82270 |   18596   13761   461213    33.5 | 22.178 % |
c ==============================================================================
c Found solution: 1404
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     52597 |   34606    82280 |   11535   13905   467095    33.6 | 22.178 % |
c |     52697 |   34606    82280 |   12688   14005   470183    33.6 | 22.180 % |
c |     52848 |   34606    82280 |   13957   14156   476842    33.7 | 22.180 % |
c |     53074 |   34606    82280 |   15353   14382   483083    33.6 | 22.180 % |
c |     53411 |   34606    82280 |   16888   14719   490781    33.3 | 22.180 % |
c |     53918 |   34606    82280 |   18577   15226   502335    33.0 | 22.180 % |
c |     54677 |   34292    81543 |   20434   15982   546741    34.2 | 22.723 % |
c |     55816 |   34292    81543 |   22478   17121   612088    35.8 | 22.723 % |
c ==============================================================================
c Found solution: 1375
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56923 |   34297    81555 |   11432   18228   678540    37.2 | 22.723 % |
c |     57023 |   34297    81555 |   12575    9214   293213    31.8 | 22.725 % |
c ==============================================================================
c Found solution: 1356
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57139 |   34304    81571 |   11434    9330   295845    31.7 | 22.725 % |
c |     57241 |   34304    81571 |   12577    9432   297556    31.5 | 22.726 % |
c |     57391 |   34304    81571 |   13835    9582   300893    31.4 | 22.726 % |
c |     57616 |   34304    81571 |   15218    9807   310558    31.7 | 22.726 % |
c ==============================================================================
c Found solution: 1337
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57898 |   34309    81583 |   11436   10089   322077    31.9 | 22.726 % |
c |     57998 |   34309    81583 |   12579   10189   323845    31.8 | 22.728 % |
c |     58149 |   34259    81469 |   13837   10339   326150    31.5 | 22.819 % |
c |     58374 |   34241    81428 |   15221   10562   336472    31.9 | 22.853 % |
c |     58711 |   34241    81428 |   16743   10899   361196    33.1 | 22.853 % |
c |     59217 |   34241    81428 |   18417   11405   371956    32.6 | 22.853 % |
c |     59976 |   34168    81259 |   20259   12161   416868    34.3 | 22.991 % |
c |     61115 |   34082    81059 |   22285   13297   472342    35.5 | 23.151 % |
c ==============================================================================
c Found solution: 1312
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61210 |   34089    81075 |   11363   13392   476347    35.6 | 23.151 % |
c |     61311 |   34089    81075 |   12499   13493   483194    35.8 | 23.151 % |
c |     61461 |   34089    81075 |   13749   13643   489705    35.9 | 23.151 % |
c |     61686 |   34089    81075 |   15124   13868   501226    36.1 | 23.151 % |
c ==============================================================================
c Found solution: 1311
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61812 |   34094    81087 |   11364   13994   506283    36.2 | 23.151 % |
c ==============================================================================
c Found solution: 1308
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     61823 |   34101    81103 |   11367   14005   506542    36.2 | 23.151 % |
c |     61923 |   34101    81103 |   12503   14105   513908    36.4 | 23.154 % |
c |     62075 |   34101    81103 |   13754   14257   521363    36.6 | 23.153 % |
c |     62300 |   34101    81103 |   15129   14482   535416    37.0 | 23.153 % |
c |     62639 |   34043    80967 |   16642   14820   543359    36.7 | 23.262 % |
c |     63145 |   33977    80813 |   18306   15325   570800    37.2 | 23.394 % |
c ==============================================================================
c Found solution: 1276
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     63370 |   33993    80853 |   11331   15550   584365    37.6 | 23.394 % |
c |     63474 |   33993    80853 |   12464    7879   229194    29.1 | 23.386 % |
c |     63624 |   33993    80853 |   13710    8029   235781    29.4 | 23.386 % |
c |     63852 |   33993    80853 |   15081    8257   241118    29.2 | 23.386 % |
c |     64190 |   33993    80853 |   16589    8595   255628    29.7 | 23.386 % |
c |     64696 |   33993    80853 |   18248    9101   265330    29.2 | 23.386 % |
c |     65457 |   33993    80853 |   20073    9862   281658    28.6 | 23.386 % |
c |     66597 |   33993    80853 |   22080   11002   307035    27.9 | 23.386 % |
c |     68305 |   33993    80853 |   24289   12710   368240    29.0 | 23.386 % |
c ==============================================================================
c Found solution: 1261
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     68916 |   33997    80865 |   11332   13321   404243    30.3 | 23.386 % |
c |     69017 |   33997    80865 |   12465   13422   410227    30.6 | 23.388 % |
c |     69167 |   33997    80865 |   13711   13572   415038    30.6 | 23.388 % |
c |     69392 |   33997    80865 |   15082   13797   425319    30.8 | 23.388 % |
c |     69730 |   33997    80865 |   16591   14135   433786    30.7 | 23.388 % |
c |     70236 |   33997    80865 |   18250   14641   444412    30.4 | 23.388 % |
c |     70995 |   33997    80865 |   20075   15400   501489    32.6 | 23.388 % |
c ==============================================================================
c Found solution: 1249
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     71760 |   34004    80893 |   11334   16165   543216    33.6 | 23.388 % |
c |     71861 |   34004    80893 |   12467    8184   240743    29.4 | 23.387 % |
c |     72011 |   34004    80893 |   13714    8334   248316    29.8 | 23.387 % |
c |     72237 |   34000    80884 |   15085    8559   258603    30.2 | 23.392 % |
c |     72578 |   34000    80884 |   16594    8900   269183    30.2 | 23.392 % |
c |     73084 |   34000    80884 |   18253    9406   290102    30.8 | 23.392 % |
c ==============================================================================
c Found solution: 1233
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     73571 |   34004    80894 |   11334    9893   312372    31.6 | 23.392 % |
c |     73671 |   34004    80894 |   12467    9993   316963    31.7 | 23.394 % |
c |     73821 |   34004    80894 |   13714   10143   323069    31.9 | 23.394 % |
c |     74047 |   34004    80894 |   15085   10369   327866    31.6 | 23.394 % |
c |     74385 |   34004    80894 |   16594   10707   342711    32.0 | 23.394 % |
c |     74894 |   34004    80894 |   18253   11216   372879    33.2 | 23.394 % |
c ==============================================================================
c Found solution: 1219
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     75485 |   34009    80905 |   11336   11807   403318    34.2 | 23.394 % |
c |     75585 |   34009    80905 |   12469   11907   407498    34.2 | 23.396 % |
c |     75735 |   34009    80905 |   13716   12057   413667    34.3 | 23.396 % |
c |     75961 |   34009    80905 |   15088   12283   419498    34.2 | 23.396 % |
c |     76300 |   34009    80905 |   16597   12622   434871    34.5 | 23.396 % |
c |     76810 |   34009    80905 |   18256   13132   456938    34.8 | 23.396 % |
c |     77569 |   34009    80905 |   20082   13891   495418    35.7 | 23.396 % |
c ==============================================================================
c Found solution: 1215
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78703 |   34014    80916 |   11338   15025   556512    37.0 | 23.396 % |
c |     78803 |   34014    80916 |   12471   15125   560304    37.0 | 23.398 % |
c |     78955 |   34014    80916 |   13718   15277   567187    37.1 | 23.397 % |
c |     79180 |   34014    80916 |   15090   15502   570412    36.8 | 23.397 % |
c |     79517 |   34014    80916 |   16599   15839   574576    36.3 | 23.397 % |
c |     80024 |   34014    80916 |   18259   16346   584008    35.7 | 23.397 % |
c |     80783 |   33957    80784 |   20085   17103   609563    35.6 | 23.506 % |
c |     81922 |   33957    80784 |   22094   18242   652586    35.8 | 23.506 % |
c |     83631 |   33957    80784 |   24304   19951   738171    37.0 | 23.506 % |
c |     86193 |   33957    80784 |   26734   22513   862647    38.3 | 23.506 % |
c ==============================================================================
c Found solution: 1194
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86651 |   33964    80800 |   11321   22971   879386    38.3 | 23.506 % |
c ==============================================================================
c Found solution: 1149
c ---[   0]---> Sorter-cost:    3     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86700 |   33968    80809 |   11322   11535   366925    31.8 | 23.506 % |
c ==============================================================================
c Found solution: 1145
c ---[   0]---> Sorter-cost:    4     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     86718 |   33973    80820 |   11324   11553   367741    31.8 | 23.506 % |
c |     86822 |   33973    80820 |   12456   11657   372147    31.9 | 23.512 % |
c |     86973 |   33973    80820 |   13702   11808   379427    32.1 | 23.512 % |
c |     87198 |   33973    80820 |   15072   12033   388418    32.3 | 23.512 % |
c ==============================================================================
c Found solution: 1136
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     87295 |   33982    80843 |   11327   12130   392054    32.3 | 23.512 % |
c |     87395 |   33982    80843 |   12459   12230   397615    32.5 | 23.510 % |
c |     87546 |   33982    80843 |   13705   12381   401852    32.5 | 23.510 % |
c |     87771 |   33982    80843 |   15076   12606   408267    32.4 | 23.510 % |
c |     88111 |   33982    80843 |   16583   12946   416712    32.2 | 23.510 % |
c |     88617 |   33982    80843 |   18242   13452   438552    32.6 | 23.510 % |
c |     89376 |   33982    80843 |   20066   14211   467515    32.9 | 23.510 % |
c |     90515 |   33982    80843 |   22073   15350   505978    33.0 | 23.510 % |
c |     92223 |   33982    80843 |   24280   17058   574942    33.7 | 23.510 % |
c |     94785 |   33946    80759 |   26708   19618   651326    33.2 | 23.573 % |
c ==============================================================================
c Found solution: 1128
c ---[   0]---> Sorter-cost:    5     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     98336 |   33952    80774 |   11317   23169   802322    34.6 | 23.573 % |
c |     98438 |   33952    80774 |   12448   11687   310808    26.6 | 23.573 % |
c |     98588 |   33952    80774 |   13693   11837   317230    26.8 | 23.573 % |
c |     98817 |   33952    80774 |   15062   12066   326295    27.0 | 23.573 % |
c |     99155 |   33952    80774 |   16569   12404   336095    27.1 | 23.573 % |
c |     99661 |   33952    80774 |   18226   12910   359193    27.8 | 23.573 % |
c |    100420 |   33952    80774 |   20048   13669   396157    29.0 | 23.573 % |
c |    101560 |   33952    80774 |   22053   14809   437250    29.5 | 23.573 % |
c |    103268 |   33952    80774 |   24258   16517   516374    31.3 | 23.573 % |
c |    105830 |   33952    80774 |   26684   19079   624783    32.7 | 23.573 % |
c |    109676 |   33952    80774 |   29353   22925   762667    33.3 | 23.573 % |
c |    115442 |   33952    80774 |   32288   28691   989080    34.5 | 23.573 % |
c |    124092 |   33952    80774 |   35517   37341  1393060    37.3 | 23.573 % |
c ==============================================================================
c Found solution: 1120
c ---[   0]---> Sorter-cost:    2     Base: 2 3 13 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    136193 |   33955    80781 |   11318   26816  1021714    38.1 | 23.573 % |
c |    136293 |   33955    80781 |   12449   13508   480514    35.6 | 23.576 % |
c |    136444 |   33939    80744 |   13694   13658   485170    35.5 | 23.605 % |
c |    136669 |   33939    80744 |   15064   13883   491212    35.4 | 23.605 % |
c |    137006 |   33939    80744 |   16570   14220   500993    35.2 | 23.605 % |
c |    137516 |   33939    80744 |   18227   14730   521903    35.4 | 23.605 % |
c |    138276 |   33939    80744 |   20050   15490   536341    34.6 | 23.605 % |
c |    139416 |   33939    80744 |   22055   16630   592086    35.6 | 23.605 % |
c |    141124 |   33939    80744 |   24261   18338   662753    36.1 | 23.605 % |
c |    143686 |   33939    80744 |   26687   20900   767136    36.7 | 23.605 % |
c |    147530 |   33939    80744 |   29355   24744   895353    36.2 | 23.605 % |
c |    153296 |   33793    80407 |   32291   30507  1148443    37.6 | 23.901 % |
c ==============================================================================
c Optimal solution: 1120
s OPTIMUM FOUND
v C101_bit0 C102_bit0 -C103_bit0 -C104_bit0 -C105_bit0 -C108_bit0 -C111_bit0 -C112_bit0 -C113_bit0 C114_bit0 -C115_bit0 -C116_bit0 -C117_bit0 -C118_bit0 -C119_bit0 -C120_bit0 -C121_bit0 -C122_bit0 -C123_bit0 -C124_bit0 -C125_bit0 -C126_bit0 C127_bit0 -C128_bit0 -C129_bit0 -C130_bit0 -C131_bit0 -C132_bit0 -C133_bit0 -C134_bit0 C135_bit0 -C136_bit0 -C137_bit0 -C138_bit0 C139_bit0 -C140_bit0 -C141_bit0 -C142_bit0 C143_bit0 -C144_bit0 -C145_bit0 -C146_bit0 -C147_bit0 -C148_bit0 -C149_bit0 -C150_bit0 C151_bit0 -C152_bit0 C153_bit0 -C154_bit0 -C155_bit0 -C156_bit0 -C157_bit0 -C158_bit0 -C159_bit0 -C160_bit0 -C161_bit0 -C162_bit0 -C163_bit0 C164_bit0 -C165_bit0 C166_bit0 -C167_bit0 -C168_bit0 -C169_bit0 -C170_bit0 -C171_bit0 -C172_bit0 -C173_bit0 -C174_bit0 -C175_bit0 -C176_bit0 -C177_bit0 -C178_bit0 -C179_bit0 -C180_bit0 -C181_bit0 -C182_bit0 -C183_bit0 -C184_bit0 -C185_bit0 C186_bit0 -C187_bit0 -C188_bit0 -C189_bit0 -C106_bit0 C107_bit0 -C109_bit0 -C110_bit0
c _______________________________________________________________________________
c 
c restarts              : 247
c conflicts             : 155748         (235 /sec)
c decisions             : 277901         (420 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 661.4 s
c _______________________________________________________________________________

Watcher Data

Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing Stack size limit: 67108864 bytes
Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb
Enforcing VSIZE limit: 994918400 bytes
Current StackSize limit: 67108864 bytes
Raw data (/proc/13101/stat): 13101 (minisat+_script) R 13100 13101 20602 0 -1 0 19 0 0 0 0 0 0 0 24 0 1 0 1732573485 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/13101/statm): 174 3 169 147 0 27 0
[pid=13101] 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=13102
New process pid=13103
New process pid=13104
execve syscall for /bin/sed executable
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
One traced child (pid=13103) exited with status: 0
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=13104) exited with status: 0
One traced child (pid=13102) exited with status: 0
New process pid=13105
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-lseu.opb

[startup+10.0037 s]
Raw data (loadavg): 0.93 0.95 0.90 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 1636 0 0 0 983 5 0 0 25 0 1 0 1732573490 8073216 1612 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 1971 1612 145 145 0 1826 0
[pid=13105] vsize: 7884
Current children cumulated CPU time (s) 9.88
Current children cumulated vsize (Kb) 10008

[startup+20.0053 s]
Raw data (loadavg): 0.94 0.96 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 1844 0 0 0 1979 8 0 0 25 0 1 0 1732573490 8921088 1820 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2178 1820 145 145 0 2033 0
[pid=13105] vsize: 8712
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 10836

[startup+30.006 s]
Raw data (loadavg): 0.95 0.96 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2002 0 0 0 2975 9 0 0 25 0 1 0 1732573490 9592832 1978 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2342 1978 145 145 0 2197 0
[pid=13105] vsize: 9368
Current children cumulated CPU time (s) 29.84
Current children cumulated vsize (Kb) 11492

[startup+40.0067 s]
Raw data (loadavg): 0.95 0.96 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2144 0 0 0 3972 11 0 0 25 0 1 0 1732573490 10153984 2120 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2479 2120 145 145 0 2334 0
[pid=13105] vsize: 9916
Current children cumulated CPU time (s) 39.83
Current children cumulated vsize (Kb) 12040

[startup+50.0074 s]
Raw data (loadavg): 0.96 0.96 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2315 0 0 0 4968 13 0 0 25 0 1 0 1732573490 10846208 2291 4294967295 134512640 135094434 3221224432 3221223024 134557168 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2648 2291 145 145 0 2503 0
[pid=13105] vsize: 10592
Current children cumulated CPU time (s) 49.81
Current children cumulated vsize (Kb) 12716

[startup+60.0081 s]
Raw data (loadavg): 0.97 0.96 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2451 0 0 0 5966 14 0 0 25 0 1 0 1732573490 11456512 2427 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2797 2427 145 145 0 2652 0
[pid=13105] vsize: 11188
Current children cumulated CPU time (s) 59.8
Current children cumulated vsize (Kb) 13312

[startup+70.0088 s]
Raw data (loadavg): 0.97 0.96 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2576 0 0 0 6964 15 0 0 25 0 1 0 1732573490 11968512 2552 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2922 2552 145 145 0 2777 0
[pid=13105] vsize: 11688
Current children cumulated CPU time (s) 69.79
Current children cumulated vsize (Kb) 13812

[startup+80.0094 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2613 0 0 0 7963 15 0 0 25 0 1 0 1732573490 12120064 2589 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2959 2589 145 145 0 2814 0
[pid=13105] vsize: 11836
Current children cumulated CPU time (s) 79.78
Current children cumulated vsize (Kb) 13960

[startup+90.0101 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2614 0 0 0 8963 16 0 0 25 0 1 0 1732573490 12120064 2590 4294967295 134512640 135094434 3221224432 3221223056 134562068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2959 2590 145 145 0 2814 0
[pid=13105] vsize: 11836
Current children cumulated CPU time (s) 89.79
Current children cumulated vsize (Kb) 13960

[startup+100.011 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2614 0 0 0 9963 16 0 0 25 0 1 0 1732573490 12120064 2590 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2959 2590 145 145 0 2814 0
[pid=13105] vsize: 11836
Current children cumulated CPU time (s) 99.79
Current children cumulated vsize (Kb) 13960

[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2614 0 0 0 10963 16 0 0 25 0 1 0 1732573490 12120064 2590 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2959 2590 145 145 0 2814 0
[pid=13105] vsize: 11836
Current children cumulated CPU time (s) 109.79
Current children cumulated vsize (Kb) 13960

[startup+120.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2614 0 0 0 11962 16 0 0 25 0 1 0 1732573490 12120064 2590 4294967295 134512640 135094434 3221224432 3221223056 134562060 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2959 2590 145 145 0 2814 0
[pid=13105] vsize: 11836
Current children cumulated CPU time (s) 119.78
Current children cumulated vsize (Kb) 13960

[startup+130.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2614 0 0 0 12962 16 0 0 25 0 1 0 1732573490 12120064 2590 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2959 2590 145 145 0 2814 0
[pid=13105] vsize: 11836
Current children cumulated CPU time (s) 129.78
Current children cumulated vsize (Kb) 13960

[startup+140.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2614 0 0 0 13962 17 0 0 25 0 1 0 1732573490 12120064 2590 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2959 2590 145 145 0 2814 0
[pid=13105] vsize: 11836
Current children cumulated CPU time (s) 139.79
Current children cumulated vsize (Kb) 13960

[startup+150.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2619 0 0 0 14962 17 0 0 25 0 1 0 1732573490 12136448 2595 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 2963 2595 145 145 0 2818 0
[pid=13105] vsize: 11852
Current children cumulated CPU time (s) 149.79
Current children cumulated vsize (Kb) 13976

[startup+160.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2688 0 0 0 15960 18 0 0 25 0 1 0 1732573490 12414976 2664 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3031 2664 145 145 0 2886 0
[pid=13105] vsize: 12124
Current children cumulated CPU time (s) 159.78
Current children cumulated vsize (Kb) 14248

[startup+170.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2688 0 0 0 16960 18 0 0 25 0 1 0 1732573490 12414976 2664 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3031 2664 145 145 0 2886 0
[pid=13105] vsize: 12124
Current children cumulated CPU time (s) 169.78
Current children cumulated vsize (Kb) 14248

[startup+180.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2688 0 0 0 17960 18 0 0 25 0 1 0 1732573490 12414976 2664 4294967295 134512640 135094434 3221224432 3221223104 134556329 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3031 2664 145 145 0 2886 0
[pid=13105] vsize: 12124
Current children cumulated CPU time (s) 179.78
Current children cumulated vsize (Kb) 14248

[startup+190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2688 0 0 0 18960 18 0 0 25 0 1 0 1732573490 12414976 2664 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3031 2664 145 145 0 2886 0
[pid=13105] vsize: 12124
Current children cumulated CPU time (s) 189.78
Current children cumulated vsize (Kb) 14248

[startup+200.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2688 0 0 0 19960 19 0 0 25 0 1 0 1732573490 12414976 2664 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3031 2664 145 145 0 2886 0
[pid=13105] vsize: 12124
Current children cumulated CPU time (s) 199.79
Current children cumulated vsize (Kb) 14248

[startup+210.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2688 0 0 0 20960 19 0 0 25 0 1 0 1732573490 12414976 2664 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3031 2664 145 145 0 2886 0
[pid=13105] vsize: 12124
Current children cumulated CPU time (s) 209.79
Current children cumulated vsize (Kb) 14248

[startup+220.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2688 0 0 0 21959 19 0 0 25 0 1 0 1732573490 12414976 2664 4294967295 134512640 135094434 3221224432 3221223024 134557423 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3031 2664 145 145 0 2886 0
[pid=13105] vsize: 12124
Current children cumulated CPU time (s) 219.78
Current children cumulated vsize (Kb) 14248

[startup+230.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2688 0 0 0 22959 19 0 0 25 0 1 0 1732573490 12414976 2664 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3031 2664 145 145 0 2886 0
[pid=13105] vsize: 12124
Current children cumulated CPU time (s) 229.78
Current children cumulated vsize (Kb) 14248

[startup+240.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2688 0 0 0 23959 20 0 0 25 0 1 0 1732573490 12414976 2664 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3031 2664 145 145 0 2886 0
[pid=13105] vsize: 12124
Current children cumulated CPU time (s) 239.79
Current children cumulated vsize (Kb) 14248

[startup+250.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2688 0 0 0 24959 20 0 0 25 0 1 0 1732573490 12414976 2664 4294967295 134512640 135094434 3221224432 3221223104 134556073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3031 2664 145 145 0 2886 0
[pid=13105] vsize: 12124
Current children cumulated CPU time (s) 249.79
Current children cumulated vsize (Kb) 14248

[startup+260.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2688 0 0 0 25958 20 0 0 25 0 1 0 1732573490 12414976 2664 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3031 2664 145 145 0 2886 0
[pid=13105] vsize: 12124
Current children cumulated CPU time (s) 259.78
Current children cumulated vsize (Kb) 14248

[startup+270.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2697 0 0 0 26958 20 0 0 25 0 1 0 1732573490 12455936 2673 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3041 2673 145 145 0 2896 0
[pid=13105] vsize: 12164
Current children cumulated CPU time (s) 269.78
Current children cumulated vsize (Kb) 14288

[startup+280.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2697 0 0 0 27958 21 0 0 25 0 1 0 1732573490 12455936 2673 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3041 2673 145 145 0 2896 0
[pid=13105] vsize: 12164
Current children cumulated CPU time (s) 279.79
Current children cumulated vsize (Kb) 14288

[startup+290.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2699 0 0 0 28958 21 0 0 25 0 1 0 1732573490 12468224 2675 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3044 2675 145 145 0 2899 0
[pid=13105] vsize: 12176
Current children cumulated CPU time (s) 289.79
Current children cumulated vsize (Kb) 14300

[startup+300.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2704 0 0 0 29958 21 0 0 25 0 1 0 1732573490 12488704 2680 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3049 2680 145 145 0 2904 0
[pid=13105] vsize: 12196
Current children cumulated CPU time (s) 299.79
Current children cumulated vsize (Kb) 14320

[startup+310.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2704 0 0 0 30958 21 0 0 25 0 1 0 1732573490 12488704 2680 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3049 2680 145 145 0 2904 0
[pid=13105] vsize: 12196
Current children cumulated CPU time (s) 309.79
Current children cumulated vsize (Kb) 14320

[startup+320.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2704 0 0 0 31958 21 0 0 25 0 1 0 1732573490 12488704 2680 4294967295 134512640 135094434 3221224432 3221223120 134554788 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3049 2680 145 145 0 2904 0
[pid=13105] vsize: 12196
Current children cumulated CPU time (s) 319.79
Current children cumulated vsize (Kb) 14320

[startup+330.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2817 0 0 0 32956 22 0 0 25 0 1 0 1732573490 12947456 2793 4294967295 134512640 135094434 3221224432 3221223024 134557404 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3161 2793 145 145 0 3016 0
[pid=13105] vsize: 12644
Current children cumulated CPU time (s) 329.78
Current children cumulated vsize (Kb) 14768

[startup+340.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2817 0 0 0 33956 22 0 0 25 0 1 0 1732573490 12947456 2793 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3161 2793 145 145 0 3016 0
[pid=13105] vsize: 12644
Current children cumulated CPU time (s) 339.78
Current children cumulated vsize (Kb) 14768

[startup+350.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2817 0 0 0 34956 22 0 0 25 0 1 0 1732573490 12947456 2793 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3161 2793 145 145 0 3016 0
[pid=13105] vsize: 12644
Current children cumulated CPU time (s) 349.78
Current children cumulated vsize (Kb) 14768

[startup+360.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2824 0 0 0 35956 22 0 0 25 0 1 0 1732573490 12976128 2800 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3168 2800 145 145 0 3023 0
[pid=13105] vsize: 12672
Current children cumulated CPU time (s) 359.78
Current children cumulated vsize (Kb) 14796

[startup+370.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2824 0 0 0 36956 23 0 0 25 0 1 0 1732573490 12976128 2800 4294967295 134512640 135094434 3221224432 3221223056 134557660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3168 2800 145 145 0 3023 0
[pid=13105] vsize: 12672
Current children cumulated CPU time (s) 369.79
Current children cumulated vsize (Kb) 14796

[startup+380.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2831 0 0 0 37956 23 0 0 25 0 1 0 1732573490 13008896 2807 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3176 2807 145 145 0 3031 0
[pid=13105] vsize: 12704
Current children cumulated CPU time (s) 379.79
Current children cumulated vsize (Kb) 14828

[startup+390.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2838 0 0 0 38955 24 0 0 25 0 1 0 1732573490 13037568 2814 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3183 2814 145 145 0 3038 0
[pid=13105] vsize: 12732
Current children cumulated CPU time (s) 389.79
Current children cumulated vsize (Kb) 14856

[startup+400.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2838 0 0 0 39955 24 0 0 25 0 1 0 1732573490 13037568 2814 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3183 2814 145 145 0 3038 0
[pid=13105] vsize: 12732
Current children cumulated CPU time (s) 399.79
Current children cumulated vsize (Kb) 14856

[startup+410.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2838 0 0 0 40955 24 0 0 25 0 1 0 1732573490 13037568 2814 4294967295 134512640 135094434 3221224432 3221223104 134556291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/13105/statm): 3183 2814 145 145 0 3038 0
[pid=13105] vsize: 12732
Current children cumulated CPU time (s) 409.79
Current children cumulated vsize (Kb) 14856

[startup+420.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2847 0 0 0 41955 24 0 0 25 0 1 0 1732573490 13082624 2823 4294967295 134512640 135094434 3221224432 3221223104 134555957 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 3194 2823 145 145 0 3049 0
[pid=13105] vsize: 12776
Current children cumulated CPU time (s) 419.79
Current children cumulated vsize (Kb) 14900

[startup+430.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2847 0 0 0 42955 24 0 0 25 0 1 0 1732573490 13082624 2823 4294967295 134512640 135094434 3221224432 3221223024 134557031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 3194 2823 145 145 0 3049 0
[pid=13105] vsize: 12776
Current children cumulated CPU time (s) 429.79
Current children cumulated vsize (Kb) 14900

[startup+440.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2852 0 0 0 43955 24 0 0 25 0 1 0 1732573490 13099008 2828 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 3198 2828 145 145 0 3053 0
[pid=13105] vsize: 12792
Current children cumulated CPU time (s) 439.79
Current children cumulated vsize (Kb) 14916

[startup+450.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 2916 0 0 0 44953 25 0 0 25 0 1 0 1732573490 13365248 2892 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 3263 2892 145 145 0 3118 0
[pid=13105] vsize: 13052
Current children cumulated CPU time (s) 449.78
Current children cumulated vsize (Kb) 15176

[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3026 0 0 0 45952 26 0 0 25 0 1 0 1732573490 13828096 3002 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 3376 3002 145 145 0 3231 0
[pid=13105] vsize: 13504
Current children cumulated CPU time (s) 459.78
Current children cumulated vsize (Kb) 15628

[startup+470.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3141 0 0 0 46950 26 0 0 25 0 1 0 1732573490 14299136 3117 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 3491 3117 145 145 0 3346 0
[pid=13105] vsize: 13964
Current children cumulated CPU time (s) 469.76
Current children cumulated vsize (Kb) 16088

[startup+480.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3267 0 0 0 47949 27 0 0 25 0 1 0 1732573490 14942208 3243 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 3648 3243 145 145 0 3503 0
[pid=13105] vsize: 14592
Current children cumulated CPU time (s) 479.76
Current children cumulated vsize (Kb) 16716

[startup+490.047 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3344 0 0 0 48948 28 0 0 25 0 1 0 1732573490 15257600 3320 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 3725 3320 145 145 0 3580 0
[pid=13105] vsize: 14900
Current children cumulated CPU time (s) 489.76
Current children cumulated vsize (Kb) 17024

[startup+500.048 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3448 0 0 0 49946 28 0 0 25 0 1 0 1732573490 15679488 3424 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 3828 3424 145 145 0 3683 0
[pid=13105] vsize: 15312
Current children cumulated CPU time (s) 499.74
Current children cumulated vsize (Kb) 17436

[startup+510.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3547 0 0 0 50944 29 0 0 25 0 1 0 1732573490 16113664 3523 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 3934 3523 145 145 0 3789 0
[pid=13105] vsize: 15736
Current children cumulated CPU time (s) 509.73
Current children cumulated vsize (Kb) 17860

[startup+520.049 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3637 0 0 0 51943 29 0 0 25 0 1 0 1732573490 16486400 3613 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4025 3613 145 145 0 3880 0
[pid=13105] vsize: 16100
Current children cumulated CPU time (s) 519.72
Current children cumulated vsize (Kb) 18224

[startup+530.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3724 0 0 0 52942 30 0 0 25 0 1 0 1732573490 16834560 3700 4294967295 134512640 135094434 3221224432 3221223024 134551428 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4110 3700 145 145 0 3965 0
[pid=13105] vsize: 16440
Current children cumulated CPU time (s) 529.72
Current children cumulated vsize (Kb) 18564

[startup+540.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3724 0 0 0 53941 31 0 0 25 0 1 0 1732573490 16834560 3700 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4110 3700 145 145 0 3965 0
[pid=13105] vsize: 16440
Current children cumulated CPU time (s) 539.72
Current children cumulated vsize (Kb) 18564

[startup+550.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3726 0 0 0 54940 32 0 0 25 0 1 0 1732573490 16842752 3702 4294967295 134512640 135094434 3221224432 3221223024 134552003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4112 3702 145 145 0 3967 0
[pid=13105] vsize: 16448
Current children cumulated CPU time (s) 549.72
Current children cumulated vsize (Kb) 18572

[startup+560.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3729 0 0 0 55940 32 0 0 25 0 1 0 1732573490 16859136 3705 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4116 3705 145 145 0 3971 0
[pid=13105] vsize: 16464
Current children cumulated CPU time (s) 559.72
Current children cumulated vsize (Kb) 18588

[startup+570.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3737 0 0 0 56940 32 0 0 25 0 1 0 1732573490 16891904 3713 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4124 3713 145 145 0 3979 0
[pid=13105] vsize: 16496
Current children cumulated CPU time (s) 569.72
Current children cumulated vsize (Kb) 18620

[startup+580.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3737 0 0 0 57940 33 0 0 25 0 1 0 1732573490 16891904 3713 4294967295 134512640 135094434 3221224432 3221223088 134557879 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4124 3713 145 145 0 3979 0
[pid=13105] vsize: 16496
Current children cumulated CPU time (s) 579.73
Current children cumulated vsize (Kb) 18620

[startup+590.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3737 0 0 0 58940 33 0 0 25 0 1 0 1732573490 16891904 3713 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4124 3713 145 145 0 3979 0
[pid=13105] vsize: 16496
Current children cumulated CPU time (s) 589.73
Current children cumulated vsize (Kb) 18620

[startup+600.054 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3738 0 0 0 59940 33 0 0 25 0 1 0 1732573490 16891904 3714 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4124 3714 145 145 0 3979 0
[pid=13105] vsize: 16496
Current children cumulated CPU time (s) 599.73
Current children cumulated vsize (Kb) 18620

[startup+610.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3740 0 0 0 60940 33 0 0 25 0 1 0 1732573490 16891904 3716 4294967295 134512640 135094434 3221224432 3221223088 134558169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4124 3716 145 145 0 3979 0
[pid=13105] vsize: 16496
Current children cumulated CPU time (s) 609.73
Current children cumulated vsize (Kb) 18620

[startup+620.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3740 0 0 0 61940 33 0 0 25 0 1 0 1732573490 16891904 3716 4294967295 134512640 135094434 3221224432 3221223056 134562139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4124 3716 145 145 0 3979 0
[pid=13105] vsize: 16496
Current children cumulated CPU time (s) 619.73
Current children cumulated vsize (Kb) 18620

[startup+630.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3740 0 0 0 62941 33 0 0 25 0 1 0 1732573490 16891904 3716 4294967295 134512640 135094434 3221224432 3221223088 134557846 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4124 3716 145 145 0 3979 0
[pid=13105] vsize: 16496
Current children cumulated CPU time (s) 629.74
Current children cumulated vsize (Kb) 18620

[startup+640.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3752 0 0 0 63941 33 0 0 25 0 1 0 1732573490 16957440 3728 4294967295 134512640 135094434 3221224432 3221223024 134557273 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4140 3728 145 145 0 3995 0
[pid=13105] vsize: 16560
Current children cumulated CPU time (s) 639.74
Current children cumulated vsize (Kb) 18684

[startup+650.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3752 0 0 0 64941 34 0 0 25 0 1 0 1732573490 16957440 3728 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4140 3728 145 145 0 3995 0
[pid=13105] vsize: 16560
Current children cumulated CPU time (s) 649.75
Current children cumulated vsize (Kb) 18684

[startup+660.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/58 13105
Raw data (/proc/13101/stat): 13101 (minisat+_script) S 13100 13101 20602 0 -1 0 289 239 0 0 0 0 0 0 23 0 1 0 1732573485 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/13101/statm): 531 226 485 147 0 384 0
[pid=13101] vsize: 2124
Raw data (/proc/13105/stat): 13105 (minisat+_64-bit) R 13101 13101 20602 0 -1 0 3763 0 0 0 65941 34 0 0 25 0 1 0 1732573490 17022976 3739 4294967295 134512640 135094434 3221224432 3221223088 134557856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/13105/statm): 4156 3739 145 145 0 4011 0
[pid=13105] vsize: 16624
Current children cumulated CPU time (s) 659.75
Current children cumulated vsize (Kb) 18748
One traced child (pid=13105) exited with status: 30
One traced child (pid=13101) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 662.068
CPU time (s): 661.783
CPU user time (s): 661.413
CPU system time (s): 0.369943
CPU usage (%): 99.957
Max. virtual memory (cumulated for all children) (Kb): 18748

Verifier Data

Verifier:	OK	1120