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/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-bk4x3.opb
MD5SUMc2339539ffa69702e62053614fe34ce1
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 44800
Optimality of the best value was proved YES
Number of terms in the objective function 252
Biggest coefficient in the objective function 2621440
Number of bits for the biggest coefficient in the objective function 22
Sum of the numbers in the objective function 35682270
Number of bits of the sum of numbers in the objective function 26
Biggest number in a constraint 2621440
Number of bits of the biggest number in a constraint 22
Biggest sum of numbers in a constraint 35682270
Number of bits of the biggest sum of numbers26
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark15.3857
Number of variables252
Total number of constraints19
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints19
Minimum length of a constraint21
Maximum length of a constraint80

Trace number 6212

Launcher Data

LAUNCH ON wulflinc15 THE 2005-09-20 04:45:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3405 boxname=wulflinc15 idbench=1061 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  c2339539ffa69702e62053614fe34ce1  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bk4x3.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bk4x3.opb
IDLAUNCH: 3405
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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	: 2
cpu MHz		: 450.999
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:        899824 kB
Buffers:          8608 kB
Cached:          97068 kB
SwapCached:        744 kB
Active:          32392 kB
Inactive:        75936 kB
HighTotal:      131008 kB
HighFree:        32228 kB
LowTotal:       903652 kB
LowFree:        867596 kB
SwapTotal:     2097136 kB
SwapFree:      2095884 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5720 kB
Slab:            20904 kB
Committed_AS:    64140 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-20 04:45:41 (client local time) WITH STATUS 30 IN 28.4607 SECONDS
stats: 3405 0 28.4607 30

Solver Data

c Parsing PB file...
c Converting 26 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #######
c   -- Clauses(.)/Splits(s): (none)
c ---[  24]---> Sorter-cost:  237     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  275     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  18]---> Sorter-cost:  261     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  16]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  445     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  455     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> BDD-cost:   14
c ---[  10]---> BDD-cost:   14
c ---[   9]---> BDD-cost:   15
c ---[   8]---> BDD-cost:   15
c ---[   7]---> BDD-cost:   14
c ---[   6]---> BDD-cost:   15
c ---[   5]---> BDD-cost:   16
c ---[   4]---> BDD-cost:   16
c ---[   3]---> BDD-cost:   15
c ---[   2]---> BDD-cost:   16
c ---[   1]---> BDD-cost:   16
c ---[   0]---> BDD-cost:   15
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |    5719    13584 |    1906       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: 69632
c ---[   0]---> Sorter-cost: 6116     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         2 |   19981    46877 |    6660       2       15     7.5 |  0.000 % |
c |       104 |   19981    46877 |    7326     104     1142    11.0 |  4.283 % |
c ==============================================================================
c Found solution: 63168
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       187 |   20028    47001 |    6676     187     2186    11.7 |  4.283 % |
c ==============================================================================
c Found solution: 63040
c ---[   0]---> Sorter-cost:    6     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       244 |   20040    47036 |    6680     244     3256    13.3 |  4.283 % |
c |       344 |   20040    47036 |    7348     344     4021    11.7 |  4.288 % |
c |       494 |   20040    47036 |    8082     494     5290    10.7 |  4.288 % |
c |       720 |   20040    47036 |    8891     720     9531    13.2 |  4.288 % |
c ==============================================================================
c Found solution: 62454
c ---[   0]---> Sorter-cost:   12     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       841 |   20055    47085 |    6685     841    13225    15.7 |  4.288 % |
c |       943 |   20055    47085 |    7353     943    16068    17.0 |  4.296 % |
c ==============================================================================
c Found solution: 59900
c ---[   0]---> Sorter-cost:   11     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1076 |   20046    47073 |    6682    1074    18047    16.8 |  4.296 % |
c |      1176 |   20046    47073 |    7350    1174    19285    16.4 |  4.396 % |
c |      1326 |   20046    47073 |    8085    1324    27692    20.9 |  4.396 % |
c ==============================================================================
c Found solution: 57622
c ---[   0]---> Sorter-cost:    8     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1418 |   20072    47141 |    6690    1416    29974    21.2 |  4.396 % |
c |      1518 |   20072    47141 |    7359    1516    31706    20.9 |  4.400 % |
c |      1668 |   20072    47141 |    8094    1666    37067    22.2 |  4.400 % |
c |      1893 |   20043    47079 |    8904    1889    42867    22.7 |  4.530 % |
c |      2230 |   20043    47079 |    9794    2226    53581    24.1 |  4.530 % |
c |      2736 |   20040    47072 |   10774    2657    77254    29.1 |  4.555 % |
c |      3497 |   20040    47072 |   11851    3418   106715    31.2 |  4.555 % |
c |      4637 |   20033    47057 |   13036    4557   137444    30.2 |  4.581 % |
c |      6345 |   20033    47057 |   14340    6265   235328    37.6 |  4.581 % |
c |      8911 |   20033    47057 |   15774    8831   324335    36.7 |  4.581 % |
c ==============================================================================
c Found solution: 57620
c ---[   0]---> Sorter-cost:   10     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12119 |   20040    47080 |    6680   12038   491447    40.8 |  4.581 % |
c |     12219 |   20040    47080 |    7348    6119   242617    39.6 |  4.615 % |
c |     12372 |   20040    47080 |    8082    6272   246261    39.3 |  4.615 % |
c ==============================================================================
c Found solution: 50172
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12394 |   20086    47198 |    6695    6294   246681    39.2 |  4.615 % |
c |     12494 |   20086    47198 |    7364    6394   249097    39.0 |  4.611 % |
c |     12644 |   20086    47198 |    8100    6544   254240    38.9 |  4.611 % |
c |     12869 |   20086    47198 |    8911    6769   260927    38.5 |  4.611 % |
c |     13206 |   20086    47198 |    9802    7106   271797    38.2 |  4.611 % |
c ==============================================================================
c Found solution: 49620
c ---[   0]---> Sorter-cost:    7     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13637 |   20096    47227 |    6698    7537   283569    37.6 |  4.611 % |
c |     13739 |   20096    47227 |    7367    3871   118107    30.5 |  4.621 % |
c |     13889 |   20096    47227 |    8104    4021   124612    31.0 |  4.621 % |
c |     14115 |   20096    47227 |    8915    4247   129988    30.6 |  4.621 % |
c |     14452 |   20096    47227 |    9806    4584   138421    30.2 |  4.621 % |
c ==============================================================================
c Found solution: 48640
c ---[   0]---> Sorter-cost:    4     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14526 |   20107    47256 |    6702    4658   139936    30.0 |  4.621 % |
c |     14627 |   20107    47256 |    7372    4759   142402    29.9 |  4.630 % |
c |     14777 |   20100    47240 |    8109    4908   146510    29.9 |  4.643 % |
c |     15003 |   20100    47240 |    8920    5134   150696    29.4 |  4.643 % |
c |     15340 |   20100    47240 |    9812    5471   156640    28.6 |  4.643 % |
c |     15846 |   20100    47240 |   10793    5977   169252    28.3 |  4.643 % |
c |     16608 |   20100    47240 |   11873    6739   187436    27.8 |  4.643 % |
c ==============================================================================
c Found solution: 46080
c ---[   0]---> Sorter-cost:    3     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     17676 |   20118    47292 |    6706    7806   229462    29.4 |  4.643 % |
c |     17779 |   20118    47292 |    7376    4006    91340    22.8 |  4.672 % |
c |     17929 |   20118    47292 |    8114    4156    94666    22.8 |  4.672 % |
c |     18154 |   20118    47292 |    8925    4381   101775    23.2 |  4.672 % |
c |     18493 |   20118    47292 |    9818    4720   109794    23.3 |  4.672 % |
c |     18999 |   20118    47292 |   10800    5226   127053    24.3 |  4.672 % |
c |     19759 |   20118    47292 |   11880    5986   145165    24.3 |  4.672 % |
c ==============================================================================
c Found solution: 44800
c ---[   0]---> Sorter-cost:    5     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19805 |   20129    47324 |    6709    6032   146213    24.2 |  4.672 % |
c |     19905 |   20129    47324 |    7379    6132   148197    24.2 |  4.681 % |
c |     20055 |   20129    47324 |    8117    6282   150779    24.0 |  4.681 % |
c |     20281 |   20129    47324 |    8929    6508   155379    23.9 |  4.681 % |
c |     20618 |   20129    47324 |    9822    6845   161306    23.6 |  4.681 % |
c |     21124 |   20129    47324 |   10804    7351   170025    23.1 |  4.681 % |
c |     21883 |   20129    47324 |   11885    8110   184974    22.8 |  4.681 % |
c |     23022 |   19495    45902 |   13073    3587    71348    19.9 |  7.707 % |
c ==============================================================================
c Optimal solution: 44800
s OPTIMUM FOUND
v -X0_bit_7 -X0_bit_6 -X0_bit_5 -X0_bit_4 -X0_bit_3 -X0_bit_2 -X0_bit_1 -X0_bit0 -X0_bit1 -X0_bit2 -X0_bit3 -X0_bit4 -X0_bit5 -X0_bit6 -X0_bit7 -X0_bit8 -X0_bit9 -X0_bit10 -X0_bit11 -X0_bit12 -X1_bit_7 -X1_bit_6 -X1_bit_5 -X1_bit_4 -X1_bit_3 -X1_bit_2 -X1_bit_1 -X1_bit0 -X1_bit1 -X1_bit2 -X1_bit3 -X1_bit4 -X1_bit5 -X1_bit6 -X1_bit7 -X1_bit8 -X1_bit9 -X1_bit10 -X1_bit11 -X1_bit12 -X2_bit_7 -X2_bit_6 -X2_bit_5 -X2_bit_4 -X2_bit_3 -X2_bit_2 -X2_bit_1 -X2_bit0 X2_bit1 -X2_bit2 X2_bit3 -X2_bit4 -X2_bit5 -X2_bit6 -X2_bit7 -X2_bit8 -X2_bit9 -X2_bit10 -X2_bit11 -X2_bit12 -X3_bit_7 -X3_bit_6 -X3_bit_5 -X3_bit_4 -X3_bit_3 -X3_bit_2 -X3_bit_1 -X3_bit0 -X3_bit1 -X3_bit2 -X3_bit3 -X3_bit4 -X3_bit5 -X3_bit6 -X3_bit7 -X3_bit8 -X3_bit9 -X3_bit10 -X3_bit11 -X3_bit12 -X4_bit_7 -X4_bit_6 -X4_bit_5 -X4_bit_4 -X4_bit_3 -X4_bit_2 -X4_bit_1 -X4_bit0 X4_bit1 X4_bit2 X4_bit3 X4_bit4 -X4_bit5 -X4_bit6 -X4_bit7 -X4_bit8 -X4_bit9 -X4_bit10 -X4_bit11 -X4_bit12 -X5_bit_7 -X5_bit_6 -X5_bit_5 -X5_bit_4 -X5_bit_3 -X5_bit_2 -X5_bit_1 -X5_bit0 -X5_bit1 -X5_bit2 -X5_bit3 -X5_bit4 -X5_bit5 -X5_bit6 -X5_bit7 -X5_bit8 -X5_bit9 -X5_bit10 -X5_bit11 -X5_bit12 -X6_bit_7 -X6_bit_6 -X6_bit_5 -X6_bit_4 -X6_bit_3 -X6_bit_2 -X6_bit_1 -X6_bit0 -X6_bit1 X6_bit2 -X6_bit3 X6_bit4 -X6_bit5 -X6_bit6 -X6_bit7 -X6_bit8 -X6_bit9 -X6_bit10 -X6_bit11 -X6_bit12 -X7_bit_7 -X7_bit_6 -X7_bit_5 -X7_bit_4 -X7_bit_3 -X7_bit_2 -X7_bit_1 -X7_bit0 -X7_bit1 X7_bit2 -X7_bit3 X7_bit4 -X7_bit5 -X7_bit6 -X7_bit7 -X7_bit8 -X7_bit9 -X7_bit10 -X7_bit11 -X7_bit12 -X8_bit_7 -X8_bit_6 -X8_bit_5 -X8_bit_4 -X8_bit_3 -X8_bit_2 -X8_bit_1 -X8_bit0 -X8_bit1 -X8_bit2 -X8_bit3 -X8_bit4 -X8_bit5 -X8_bit6 -X8_bit7 -X8_bit8 -X8_bit9 -X8_bit10 -X8_bit11 -X8_bit12 -X9_bit_7 -X9_bit_6 -X9_bit_5 -X9_bit_4 -X9_bit_3 -X9_bit_2 -X9_bit_1 -X9_bit0 -X9_bit1 -X9_bit2 -X9_bit3 -X9_bit4 -X9_bit5 -X9_bit6 -X9_bit7 -X9_bit8 -X9_bit9 -X9_bit10 -X9_bit11 -X9_bit12 -X10_bit_7 -X10_bit_6 -X10_bit_5 -X10_bit_4 -X10_bit_3 -X10_bit_2 -X10_bit_1 -X10_bit0 -X10_bit1 -X10_bit2 -X10_bit3 -X10_bit4 -X10_bit5 -X10_bit6 -X10_bit7 -X10_bit8 -X10_bit9 -X10_bit10 -X10_bit11 -X10_bit12 -X11_bit_7 -X11_bit_6 -X11_bit_5 -X11_bit_4 -X11_bit_3 -X11_bit_2 -X11_bit_1 -X11_bit0 -X11_bit1 X11_bit2 -X11_bit3 X11_bit4 -X11_bit5 -X11_bit6 -X11_bit7 -X11_bit8 -X11_bit9 -X11_bit10 -X11_bit11 -X11_bit12 -Y0_bit0 -Y1_bit0 Y2_bit0 -Y3_bit0 Y4_bit0 -Y5_bit0 Y6_bit0 Y7_bit0 -Y8_bit0 -Y9_bit0 -Y10_bit0 Y11_bit0
c _______________________________________________________________________________
c 
c restarts              : 58
c conflicts             : 23099          (814 /sec)
c decisions             : 41358          (1458 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 28.3627 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/31491/stat): 31491 (minisat+_script) R 31490 31491 31778 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1797521406 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/31491/statm): 174 3 169 147 0 27 0
[pid=31491] 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=31492
New process pid=31493
New process pid=31494
execve syscall for /bin/sed executable
One traced child (pid=31493) 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=31494) exited with status: 0
One traced child (pid=31492) exited with status: 0
New process pid=31495
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-bk4x3.opb

[startup+10.0036 s]
Raw data (loadavg): 0.93 0.98 0.95 2/57 31495
Raw data (/proc/31491/stat): 31491 (minisat+_script) S 31490 31491 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797521406 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31491/statm): 531 226 485 147 0 384 0
[pid=31491] vsize: 2124
Raw data (/proc/31495/stat): 31495 (minisat+_64-bit) R 31491 31491 31778 0 -1 0 1182 0 0 0 983 5 0 0 25 0 1 0 1797521410 5308416 1168 4294967295 134512640 135094434 3221224432 3221223024 134557157 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31495/statm): 1296 1168 145 145 0 1151 0
[pid=31495] vsize: 5184
Current children cumulated CPU time (s) 9.89
Current children cumulated vsize (Kb) 7308

[startup+20.0044 s]
Raw data (loadavg): 0.94 0.98 0.95 2/57 31495
Raw data (/proc/31491/stat): 31491 (minisat+_script) S 31490 31491 31778 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1797521406 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (/proc/31491/statm): 531 226 485 147 0 384 0
[pid=31491] vsize: 2124
Raw data (/proc/31495/stat): 31495 (minisat+_64-bit) R 31491 31491 31778 0 -1 0 1359 0 0 0 1980 6 0 0 25 0 1 0 1797521410 6021120 1345 4294967295 134512640 135094434 3221224432 3221223024 134557269 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/31495/statm): 1470 1345 145 145 0 1325 0
[pid=31495] vsize: 5880
Current children cumulated CPU time (s) 19.87
Current children cumulated vsize (Kb) 8004
One traced child (pid=31495) exited with status: 30
One traced child (pid=31491) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 28.5897
CPU time (s): 28.4607
CPU user time (s): 28.3717
CPU system time (s): 0.088986
CPU usage (%): 99.5486
Max. virtual memory (cumulated for all children) (Kb): 8004

Verifier Data

Verifier:	OK	44800