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-p0040.opb
MD5SUM1c249519911563f3292efb34f4875b44
Bench Categoryoptimization, small integers (OPTSMALLINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 62027
Optimality of the best value was proved YES
Number of terms in the objective function 40
Biggest coefficient in the objective function 8161
Number of bits for the biggest coefficient in the objective function 13
Sum of the numbers in the objective function 265332
Number of bits of the sum of numbers in the objective function 19
Biggest number in a constraint 8161
Number of bits of the biggest number in a constraint 13
Biggest sum of numbers in a constraint 265332
Number of bits of the biggest sum of numbers19
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark7.98079
Number of variables40
Total number of constraints63
Number of constraints which are clauses10
Number of constraints which are cardinality constraints (but not clauses)50
Number of constraints which are nor clauses,nor cardinality constraints3
Minimum length of a constraint1
Maximum length of a constraint10

Trace number 6063

Launcher Data

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        888604 kB
Buffers:         18652 kB
Cached:          99072 kB
SwapCached:        868 kB
Active:          37516 kB
Inactive:        82840 kB
HighTotal:      131008 kB
HighFree:        29596 kB
LowTotal:       903652 kB
LowFree:        859008 kB
SwapTotal:     2097892 kB
SwapFree:      2096540 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           5704 kB
Slab:            19892 kB
Committed_AS:    64168 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-09-20 03:17:54 (client local time) WITH STATUS 30 IN 67.6787 SECONDS
stats: 3257 0 67.6787 30

Solver Data

c Parsing PB file...
c Converting 23 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##########
c   -- Clauses(.)/Splits(s): .
c ---[  21]---> BDD-cost:    5
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:    5
c ---[  15]---> BDD-cost:    5
c ---[  13]---> BDD-cost:    5
c ---[  11]---> BDD-cost:    5
c ---[   9]---> BDD-cost:    5
c ---[   7]---> BDD-cost:    5
c ---[   5]---> BDD-cost:    5
c ---[   3]---> BDD-cost:    5
c ---[   2]---> BDD-cost:   17
c ---[   1]---> BDD-cost:   16
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |     186      521 |      62       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 66539
c ---[   0]---> Sorter-cost: 7884     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   19547    45827 |    6515       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 65737
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        19 |   19777    46482 |    6592      16      536    33.5 |  0.000 % |
c |       119 |   19528    45919 |    7251     101     1221    12.1 |  1.637 % |
c ==============================================================================
c Found solution: 65380
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       170 |   19431    45784 |    6477     142     1778    12.5 |  1.637 % |
c ==============================================================================
c Found solution: 65203
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       172 |   19449    45882 |    6483     144     1793    12.5 |  1.637 % |
c ==============================================================================
c Found solution: 65108
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       173 |   19460    45907 |    6486     145     1796    12.4 |  1.637 % |
c ==============================================================================
c Found solution: 64519
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       191 |   19550    46137 |    6516     163     3580    22.0 |  1.637 % |
c |       291 |   19520    46069 |    7167     260     8533    32.8 |  3.079 % |
c |       444 |   19432    45878 |    7884     335     8986    26.8 |  3.489 % |
c |       669 |   19432    45878 |    8672     560    19185    34.3 |  3.489 % |
c |      1009 |   19432    45878 |    9540     900    29806    33.1 |  3.489 % |
c |      1516 |   19432    45878 |   10494    1407    48112    34.2 |  3.489 % |
c |      2276 |   19420    45851 |   11543    2166    72597    33.5 |  3.530 % |
c ==============================================================================
c Found solution: 64214
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3130 |   19437    45912 |    6479    3020   106884    35.4 |  3.530 % |
c ==============================================================================
c Found solution: 64158
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3224 |   19424    45890 |    6474    3112   110084    35.4 |  3.530 % |
c |      3325 |   19424    45890 |    7121    3213   112436    35.0 |  3.860 % |
c |      3475 |   19424    45890 |    7833    3363   115645    34.4 |  3.860 % |
c |      3701 |   19424    45890 |    8616    3589   121232    33.8 |  3.860 % |
c ==============================================================================
c Found solution: 64135
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      3966 |   19434    45912 |    6478    3854   131240    34.1 |  3.860 % |
c |      4067 |   19352    45726 |    7125    3954   135460    34.3 |  4.198 % |
c |      4217 |   19352    45726 |    7838    4104   141535    34.5 |  4.198 % |
c ==============================================================================
c Found solution: 64003
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4272 |   19433    45929 |    6477    4159   144001    34.6 |  4.198 % |
c |      4373 |   19433    45929 |    7124    4260   147968    34.7 |  4.209 % |
c |      4523 |   19433    45929 |    7837    4410   150540    34.1 |  4.209 % |
c |      4751 |   19433    45929 |    8620    4638   154035    33.2 |  4.209 % |
c |      5088 |   19209    45415 |    9482    4972   158178    31.8 |  5.032 % |
c |      5594 |   19209    45415 |   10431    5478   171051    31.2 |  5.032 % |
c ==============================================================================
c Found solution: 63972
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6285 |   19188    45380 |    6396    6168   195709    31.7 |  5.032 % |
c |      6387 |   19188    45380 |    7035    6270   198254    31.6 |  5.174 % |
c |      6538 |   19188    45380 |    7739    6421   204483    31.8 |  5.174 % |
c ==============================================================================
c Found solution: 63747
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      6676 |   19202    45413 |    6400    6559   210550    32.1 |  5.174 % |
c |      6777 |   19202    45413 |    7040    6660   212224    31.9 |  5.181 % |
c |      6927 |   19198    45405 |    7744    6807   215854    31.7 |  5.208 % |
c |      7152 |   19198    45405 |    8518    7032   224568    31.9 |  5.208 % |
c ==============================================================================
c Found solution: 63485
c ---[   0]---> Sorter-cost:    4     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      7309 |   19200    45411 |    6400    7177   230480    32.1 |  5.208 % |
c |      7410 |   19200    45411 |    7040    3690    92122    25.0 |  5.258 % |
c |      7560 |   19200    45411 |    7744    3840    97081    25.3 |  5.259 % |
c |      7785 |   19200    45411 |    8518    4065   104678    25.8 |  5.259 % |
c |      8122 |   19200    45411 |    9370    4402   114208    25.9 |  5.259 % |
c |      8629 |   19200    45411 |   10307    4909   129858    26.5 |  5.259 % |
c ==============================================================================
c Found solution: 63469
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9339 |   19208    45429 |    6402    5619   150031    26.7 |  5.259 % |
c |      9441 |   19208    45429 |    7042    5721   156236    27.3 |  5.269 % |
c |      9591 |   19208    45429 |    7746    5871   160687    27.4 |  5.269 % |
c |      9817 |   19208    45429 |    8521    6097   167454    27.5 |  5.269 % |
c |     10154 |   19208    45429 |    9373    6434   176638    27.5 |  5.269 % |
c |     10660 |   19208    45429 |   10310    6940   189839    27.4 |  5.269 % |
c ==============================================================================
c Found solution: 63444
c ---[   0]---> Sorter-cost:   11     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10890 |   19153    45305 |    6384    7166   198758    27.7 |  5.269 % |
c |     10990 |   19153    45305 |    7022    3683    83383    22.6 |  5.545 % |
c |     11140 |   19026    45010 |    7724    3828    85245    22.3 |  6.055 % |
c ==============================================================================
c Found solution: 62690
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11198 |   19087    45156 |    6362    3886    86134    22.2 |  6.055 % |
c |     11299 |   19087    45156 |    6998    3987    87540    22.0 |  6.078 % |
c ==============================================================================
c Found solution: 62215
c ---[   0]---> Sorter-cost:   10     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11310 |   19102    45200 |    6367    3998    87816    22.0 |  6.078 % |
c |     11410 |   19102    45200 |    7003    4098    90516    22.1 |  6.084 % |
c |     11561 |   19102    45200 |    7704    4249    93807    22.1 |  6.084 % |
c |     11788 |   19102    45200 |    8474    4476    97844    21.9 |  6.084 % |
c |     12126 |   19102    45200 |    9321    4814   105320    21.9 |  6.083 % |
c |     12632 |   19093    45181 |   10254    5319   118427    22.3 |  6.150 % |
c |     13394 |   19093    45181 |   11279    6081   133889    22.0 |  6.150 % |
c |     14533 |   19093    45181 |   12407    7220   161123    22.3 |  6.152 % |
c ==============================================================================
c Found solution: 62191
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15008 |   19101    45199 |    6367    7689   171924    22.4 |  6.152 % |
c |     15108 |   19101    45199 |    7003    3945    74220    18.8 |  6.198 % |
c |     15258 |   19003    44977 |    7704    4091    78834    19.3 |  6.558 % |
c |     15484 |   19003    44977 |    8474    4317    84306    19.5 |  6.558 % |
c |     15822 |   19003    44977 |    9321    4655    92114    19.8 |  6.558 % |
c ==============================================================================
c Found solution: 62180
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16282 |   19011    44998 |    6337    5115   103759    20.3 |  6.558 % |
c |     16382 |   19011    44998 |    6970    5215   105949    20.3 |  6.567 % |
c |     16532 |   19011    44998 |    7667    5365   108330    20.2 |  6.568 % |
c |     16759 |   19011    44998 |    8434    5592   112725    20.2 |  6.568 % |
c |     17097 |   19011    44998 |    9278    5930   121051    20.4 |  6.567 % |
c ==============================================================================
c Found solution: 62159
c ---[   0]---> Sorter-cost:    8     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17223 |   18987    44943 |    6329    6054   123329    20.4 |  6.567 % |
c ==============================================================================
c Found solution: 62156
c ---[   0]---> Sorter-cost:    9     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17235 |   18998    44970 |    6332    6066   123601    20.4 |  6.567 % |
c ==============================================================================
c Found solution: 62119
c ---[   0]---> Sorter-cost:    7     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17243 |   19009    44996 |    6336    6074   123696    20.4 |  6.567 % |
c |     17343 |   19009    44996 |    6969    6174   126980    20.6 |  6.735 % |
c |     17494 |   19009    44996 |    7666    6325   132499    20.9 |  6.735 % |
c ==============================================================================
c Found solution: 62104
c ---[   0]---> Sorter-cost:    6     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17710 |   19017    45015 |    6339    6541   139664    21.4 |  6.735 % |
c ==============================================================================
c Found solution: 62027
c ---[   0]---> Sorter-cost:    4     Base: 3 3 3 3 3 3 7
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17723 |   19023    45029 |    6341    6554   139846    21.3 |  6.735 % |
c |     17825 |   19023    45029 |    6975    6656   141781    21.3 |  6.754 % |
c |     17975 |   19023    45029 |    7672    6806   146493    21.5 |  6.754 % |
c |     18201 |   19023    45029 |    8439    7032   152199    21.6 |  6.753 % |
c ==============================================================================
c Optimal solution: 62027
s OPTIMUM FOUND
v -C1001_bit0 C1002_bit0 -C1003_bit0 -C1004_bit0 -C1005_bit0 C1006_bit0 -C1007_bit0 -C1008_bit0 C1009_bit0 -C1010_bit0 -C1011_bit0 -C1012_bit0 -C1013_bit0 -C1014_bit0 C1015_bit0 -C1016_bit0 -C1017_bit0 C1018_bit0 -C1019_bit0 -C1020_bit0 -C1021_bit0 C1022_bit0 -C1023_bit0 -C1024_bit0 -C1025_bit0 C1026_bit0 -C1027_bit0 -C1028_bit0 C1029_bit0 -C1030_bit0 -C1031_bit0 -C1032_bit0 -C1033_bit0 C1034_bit0 -C1035_bit0 -C1036_bit0 -C1037_bit0 C1038_bit0 -C1039_bit0 -C1040_bit0
c _______________________________________________________________________________
c 
c restarts              : 80
c conflicts             : 18521          (276 /sec)
c decisions             : 40216          (598 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 67.2168 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/16822/stat): 16822 (minisat+_script) R 16821 16822 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855238845 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0
Raw data (/proc/16822/statm): 174 3 169 147 0 27 0
[pid=16822] 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=16823
New process pid=16824
New process pid=16825
execve syscall for /bin/sed executable
One traced child (pid=16824) exited with status: 0
open syscall for file /etc/ld.so.preload
open syscall for file tls/i686/mmx/libc.so.6
open syscall for file tls/i686/libc.so.6
open syscall for file tls/mmx/libc.so.6
open syscall for file tls/libc.so.6
open syscall for file i686/mmx/libc.so.6
open syscall for file i686/libc.so.6
open syscall for file mmx/libc.so.6
open syscall for file libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/tls/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/i686/libc.so.6
open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6
open syscall for file /oldhome/oroussel/lib/libc.so.6
open syscall for file /etc/ld.so.cache
open syscall for file /lib/tls/libc.so.6
One traced child (pid=16825) exited with status: 0
One traced child (pid=16823) exited with status: 0
New process pid=16826
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-p0040.opb

[startup+10.0032 s]
Raw data (loadavg): 0.87 0.95 0.97 2/57 16826
Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16822/statm): 531 226 485 147 0 384 0
[pid=16822] vsize: 2124
Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 1838 0 0 0 984 6 0 0 25 0 1 0 1855238850 3948544 846 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/16826/statm): 964 846 145 145 0 819 0
[pid=16826] vsize: 3856
Current children cumulated CPU time (s) 9.91
Current children cumulated vsize (Kb) 5980

[startup+20.0049 s]
Raw data (loadavg): 0.89 0.96 0.97 2/57 16826
Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16822/statm): 531 226 485 147 0 384 0
[pid=16822] vsize: 2124
Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 3245 0 0 0 1977 10 0 0 25 0 1 0 1855238850 5042176 1114 4294967295 134512640 135094434 3221224432 3221221728 134677062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16826/statm): 1231 1114 145 145 0 1086 0
[pid=16826] vsize: 4924
Current children cumulated CPU time (s) 19.88
Current children cumulated vsize (Kb) 7048

[startup+30.0056 s]
Raw data (loadavg): 0.91 0.96 0.97 2/57 16826
Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16822/statm): 531 226 485 147 0 384 0
[pid=16822] vsize: 2124
Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 4555 0 0 0 2969 15 0 0 25 0 1 0 1855238850 5050368 1116 4294967295 134512640 135094434 3221224432 3221221628 134600154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16826/statm): 1233 1116 145 145 0 1088 0
[pid=16826] vsize: 4932
Current children cumulated CPU time (s) 29.85
Current children cumulated vsize (Kb) 7056

[startup+40.0052 s]
Raw data (loadavg): 0.92 0.96 0.97 2/57 16826
Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16822/statm): 531 226 485 147 0 384 0
[pid=16822] vsize: 2124
Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 5508 0 0 0 3963 19 0 0 25 0 1 0 1855238850 5005312 1105 4294967295 134512640 135094434 3221224432 3221221552 134676301 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16826/statm): 1222 1105 145 145 0 1077 0
[pid=16826] vsize: 4888
Current children cumulated CPU time (s) 39.83
Current children cumulated vsize (Kb) 7012

[startup+50.0059 s]
Raw data (loadavg): 0.93 0.96 0.97 2/57 16826
Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16822/statm): 531 226 485 147 0 384 0
[pid=16822] vsize: 2124
Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 7084 0 0 0 4953 24 0 0 25 0 1 0 1855238850 4984832 1100 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16826/statm): 1217 1100 145 145 0 1072 0
[pid=16826] vsize: 4868
Current children cumulated CPU time (s) 49.78
Current children cumulated vsize (Kb) 6992

[startup+60.0066 s]
Raw data (loadavg): 0.94 0.96 0.97 2/57 16826
Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/16822/statm): 531 226 485 147 0 384 0
[pid=16822] vsize: 2124
Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 11106 0 0 0 5929 38 0 0 25 0 1 0 1855238850 6578176 1490 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/16826/statm): 1606 1490 145 145 0 1461 0
[pid=16826] vsize: 6424
Current children cumulated CPU time (s) 59.68
Current children cumulated vsize (Kb) 8548
One traced child (pid=16826) exited with status: 30
One traced child (pid=16822) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 68.0104
CPU time (s): 67.6787
CPU user time (s): 67.2268
CPU system time (s): 0.451931
CPU usage (%): 99.5122
Max. virtual memory (cumulated for all children) (Kb): 8548

Verifier Data

Verifier:	OK	62027