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-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-noswot.opb
MD5SUMce1061a060a0716eafe03a61d610732a
Bench Categoryoptimization, big integers (OPTBIGINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function -41
Optimality of the best value was proved YES
Number of terms in the objective function 425
Biggest coefficient in the objective function 65536
Number of bits for the biggest coefficient in the objective function 17
Sum of the numbers in the objective function 3276775
Number of bits of the sum of numbers in the objective function 22
Biggest number in a constraint 41943040000000
Number of bits of the biggest number in a constraint 46
Biggest sum of numbers in a constraint 204183950227182
Number of bits of the biggest sum of numbers48
Best result obtained on this benchmarkOPTIMUM FOUND
Best CPU time to get the best result obtained on this benchmark149.087
Number of variables1340
Total number of constraints282
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)75
Number of constraints which are nor clauses,nor cardinality constraints207
Minimum length of a constraint1
Maximum length of a constraint425

Trace number 3900

Launcher Data

LAUNCH ON wulflinc10 THE 2005-09-19 03:47:43 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=2930 boxname=wulflinc10 idbench=586 idsolver=3 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ce1061a060a0716eafe03a61d610732a  /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-noswot.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-noswot.opb
IDLAUNCH: 2930
/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:        865220 kB
Buffers:         36984 kB
Cached:         105520 kB
SwapCached:        228 kB
Active:          68028 kB
Inactive:        77420 kB
HighTotal:      131008 kB
HighFree:        56448 kB
LowTotal:       903652 kB
LowFree:        808772 kB
SwapTotal:     2097136 kB
SwapFree:      2096756 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6272 kB
Slab:            18400 kB
Committed_AS:    64164 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-09-19 03:50:13 (client local time) WITH STATUS 30 IN 149.087 SECONDS
stats: 2930 0 149.087 30

Solver Data

c Parsing PB file...
c Converting 209 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ###
c   -- Clauses(.)/Splits(s): .........................
c ---[ 183]---> Adder-cost: 112   maxlim: 93   bits: 8/7
c ---[ 182]---> BDD-cost:    6
c ---[ 181]---> BDD-cost:  820
c ---[ 180]---> BDD-cost:  269
c ---[ 179]---> BDD-cost:  708
c ---[ 177]---> BDD-cost:   49
c ---[ 176]---> BDD-cost:   56
c ---[ 175]---> BDD-cost:   56
c ---[ 174]---> BDD-cost:   56
c ---[ 173]---> BDD-cost:   56
c ---[ 172]---> BDD-cost:   56
c ---[ 169]---> BDD-cost:    2
c ---[ 167]---> BDD-cost:    2
c ---[ 165]---> BDD-cost:    2
c ---[ 163]---> BDD-cost:    2
c ---[ 161]---> BDD-cost:    2
c ---[ 160]---> BDD-cost:    6
c ---[ 159]---> BDD-cost:  217
c ---[ 158]---> BDD-cost:  342
c ---[ 157]---> BDD-cost:  217
c ---[ 156]---> BDD-cost:  342
c ---[ 155]---> BDD-cost:  217
c ---[ 154]---> BDD-cost:  342
c ---[ 153]---> BDD-cost:  217
c ---[ 152]---> BDD-cost:  342
c ---[ 151]---> BDD-cost:  217
c ---[ 150]---> BDD-cost:  342
c ---[ 148]---> BDD-cost:  297
c ---[ 147]---> BDD-cost:  301
c ---[ 146]---> BDD-cost:  297
c ---[ 145]---> BDD-cost:  301
c ---[ 144]---> BDD-cost:  297
c ---[ 143]---> BDD-cost:  301
c ---[ 142]---> BDD-cost:  297
c ---[ 141]---> BDD-cost:  301
c ---[ 140]---> BDD-cost:  297
c ---[ 139]---> BDD-cost:  301
c ---[ 138]---> BDD-cost:    6
c ---[ 137]---> BDD-cost:   19
c ---[ 136]---> BDD-cost:   31
c ---[ 135]---> BDD-cost:   31
c ---[ 134]---> BDD-cost:   31
c ---[ 133]---> BDD-cost:   31
c ---[ 132]---> BDD-cost:   31
c ---[ 129]---> BDD-cost:   15
c ---[ 126]---> BDD-cost:   15
c ---[ 123]---> BDD-cost:   12
c ---[ 121]---> BDD-cost:    4
c ---[ 119]---> BDD-cost:   16
c ---[ 118]---> BDD-cost:  297
c ---[ 117]---> BDD-cost:  102
c ---[ 116]---> BDD-cost:  297
c ---[ 115]---> BDD-cost:  102
c ---[ 114]---> BDD-cost:    3
c ---[ 113]---> BDD-cost:  297
c ---[ 112]---> BDD-cost:  102
c ---[ 111]---> BDD-cost:  297
c ---[ 110]---> BDD-cost:  102
c ---[ 109]---> BDD-cost:  297
c ---[ 108]---> BDD-cost:  102
c ---[ 107]---> BDD-cost:    7
c ---[ 106]---> BDD-cost:   51
c ---[ 105]---> BDD-cost:   51
c ---[ 104]---> BDD-cost:   51
c ---[ 103]---> BDD-cost:  820
c ---[ 102]---> BDD-cost:   51
c ---[ 101]---> BDD-cost:   49
c ---[  99]---> BDD-cost:    2
c ---[  97]---> BDD-cost:    2
c ---[  95]---> BDD-cost:    2
c ---[  93]---> BDD-cost:    2
c ---[  92]---> BDD-cost:  561
c ---[  90]---> BDD-cost:    2
c ---[  89]---> BDD-cost:   19
c ---[  88]---> BDD-cost:  820
c ---[  87]---> BDD-cost:   89
c ---[  86]---> BDD-cost:  561
c ---[  85]---> BDD-cost:  820
c ---[  84]---> BDD-cost:  561
c ---[  83]---> BDD-cost:  820
c ---[  82]---> BDD-cost:  561
c ---[  81]---> BDD-cost:  820
c ---[  80]---> BDD-cost:  308
c ---[  79]---> BDD-cost:  415
c ---[  78]---> BDD-cost:  598
c ---[  77]---> BDD-cost:  415
c ---[  76]---> BDD-cost:   89
c ---[  75]---> BDD-cost:  598
c ---[  74]---> BDD-cost:  415
c ---[  73]---> BDD-cost:  598
c ---[  72]---> BDD-cost:  415
c ---[  71]---> BDD-cost:  598
c ---[  70]---> BDD-cost:  415
c ---[  69]---> BDD-cost:  329
c ---[  68]---> BDD-cost:  144
c ---[  67]---> BDD-cost:  621
c ---[  66]---> BDD-cost:  144
c ---[  65]---> BDD-cost:   89
c ---[  64]---> BDD-cost:  621
c ---[  63]---> BDD-cost:  144
c ---[  62]---> BDD-cost:  621
c ---[  61]---> BDD-cost:  144
c ---[  60]---> BDD-cost:  621
c ---[  59]---> BDD-cost:  144
c ---[  58]---> BDD-cost:  379
c ---[  57]---> BDD-cost:  297
c ---[  56]---> BDD-cost:  555
c ---[  55]---> BDD-cost:  297
c ---[  54]---> BDD-cost:   89
c ---[  53]---> BDD-cost:  555
c ---[  52]---> BDD-cost:  297
c ---[  51]---> BDD-cost:  555
c ---[  50]---> BDD-cost:  297
c ---[  49]---> BDD-cost:  555
c ---[  48]---> BDD-cost:  297
c ---[  47]---> BDD-cost:  313
c ---[  46]---> Sorter-cost:  147     Base: 2 2 2
c ---[  45]---> BDD-cost:   94
c ---[  44]---> BDD-cost:   94
c ---[  43]---> BDD-cost:   71
c ---[  42]---> BDD-cost:   94
c ---[  41]---> BDD-cost:   94
c ---[  40]---> BDD-cost:   78
c ---[  38]---> BDD-cost:    5
c ---[  36]---> BDD-cost:    5
c ---[  34]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    4
c ---[  28]---> BDD-cost:  320
c ---[  27]---> BDD-cost:  738
c ---[  26]---> BDD-cost:  320
c ---[  25]---> BDD-cost:  738
c ---[  24]---> BDD-cost:  320
c ---[  23]---> BDD-cost:  738
c ---[  22]---> BDD-cost:  320
c ---[  21]---> BDD-cost:    6
c ---[  20]---> BDD-cost:  738
c ---[  19]---> BDD-cost:  320
c ---[  18]---> BDD-cost:  738
c ---[  17]---> BDD-cost:  152
c ---[  16]---> BDD-cost:  773
c ---[  15]---> BDD-cost:  152
c ---[  14]---> BDD-cost:  773
c ---[  13]---> BDD-cost:  152
c ---[  12]---> BDD-cost:  773
c ---[  11]---> BDD-cost:  152
c ---[   9]---> BDD-cost:  773
c ---[   8]---> BDD-cost:  152
c ---[   7]---> BDD-cost:  773
c ---[   6]---> BDD-cost:  269
c ---[   5]---> BDD-cost:  708
c ---[   4]---> BDD-cost:  269
c ---[   3]---> BDD-cost:  708
c ---[   2]---> BDD-cost:  269
c ---[   1]---> BDD-cost:  708
c ---[   0]---> BDD-cost:  157
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   90344   252471 |   30114       0        0     nan |  0.000 % |
c ==============================================================================
c Found solution: -31
c ---[   0]---> Sorter-cost: 1127     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |        43 |   91603   255441 |   30534      42      256     6.1 |  0.000 % |
c |       143 |   91469   255159 |   33587     133      877     6.6 |  7.325 % |
c ==============================================================================
c Found solution: -34
c ---[   0]---> Sorter-cost:    3     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       173 |   92322   257131 |   30774     163     1083     6.6 |  7.325 % |
c |       273 |   92322   257131 |   33851     263     2956    11.2 |  7.336 % |
c ==============================================================================
c Found solution: -36
c ---[   0]---> Sorter-cost:    3     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       409 |   92194   256850 |   30731     396     4382    11.1 |  7.336 % |
c |       510 |   92194   256850 |   33804     497     5486    11.0 |  7.472 % |
c |       660 |   92194   256850 |   37184     647     7891    12.2 |  7.472 % |
c |       886 |   92169   256796 |   40902     869    10323    11.9 |  7.493 % |
c ==============================================================================
c Found solution: -37
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |       939 |   92173   256809 |   30724     922    10670    11.6 |  7.493 % |
c |      1039 |   92173   256809 |   33796    1022    12154    11.9 |  7.495 % |
c ==============================================================================
c Found solution: -38
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1171 |   92110   256662 |   30703    1146    14368    12.5 |  7.495 % |
c |      1271 |   92110   256662 |   33773    1246    16246    13.0 |  7.555 % |
c |      1422 |   92088   256612 |   37150    1337    17847    13.3 |  7.585 % |
c |      1647 |   92088   256612 |   40865    1562    22000    14.1 |  7.585 % |
c |      1985 |   92088   256612 |   44952    1900    26986    14.2 |  7.585 % |
c ==============================================================================
c Found solution: -40
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2224 |   92088   256614 |   30696    2131    29132    13.7 |  7.585 % |
c |      2324 |   92088   256614 |   33765    2231    31881    14.3 |  7.597 % |
c |      2474 |   92088   256614 |   37142    2381    35912    15.1 |  7.597 % |
c |      2699 |   92088   256614 |   40856    2606    40514    15.5 |  7.597 % |
c |      3038 |   92088   256614 |   44942    2945    48868    16.6 |  7.597 % |
c |      3545 |   92059   256549 |   49436    3442    59252    17.2 |  7.622 % |
c |      4306 |   92059   256549 |   54379    4203    75585    18.0 |  7.622 % |
c |      5445 |   92059   256549 |   59817    5342    97997    18.3 |  7.622 % |
c |      7155 |   92059   256549 |   65799    7052   138180    19.6 |  7.622 % |
c |      9721 |   92037   256499 |   72379    9615   186814    19.4 |  7.637 % |
c ==============================================================================
c Found solution: -41
c ---[   0]---> Sorter-cost:    2     Base: 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     10614 |   92040   256506 |   30680   10508   205251    19.5 |  7.637 % |
c |     10715 |   92040   256506 |   33748   10609   206710    19.5 |  7.640 % |
c |     10866 |   92040   256506 |   37122   10760   209045    19.4 |  7.639 % |
c |     11091 |   92040   256506 |   40835   10985   214376    19.5 |  7.639 % |
c |     11428 |   92040   256506 |   44918   11322   221302    19.5 |  7.640 % |
c |     11935 |   92040   256506 |   49410   11829   231814    19.6 |  7.639 % |
c |     12694 |   92040   256506 |   54351   12588   244329    19.4 |  7.639 % |
c |     13834 |   92040   256506 |   59786   13728   264379    19.3 |  7.639 % |
c |     15544 |   92040   256506 |   65765   15438   298402    19.3 |  7.639 % |
c |     18108 |   92040   256506 |   72341   18002   349937    19.4 |  7.639 % |
c |     21954 |   92025   256473 |   79576   21834   409442    18.8 |  7.652 % |
c |     27720 |   91859   256088 |   87533   23963   460743    19.2 |  7.801 % |
c |     36369 |   91800   255923 |   96286   23369   440632    18.9 |  7.829 % |
c |     49343 |   91536   255217 |  105915   21394   398691    18.6 |  8.005 % |
c ==============================================================================
c Optimal solution: -41
s OPTIMUM FOUND
v -x52_bit0 -x52_bit1 x52_bit2 -x52_bit3 -x52_bit4 -x52_bit5 -x52_bit6 -x52_bit7 -x52_bit8 -x52_bit9 -x52_bit10 -x52_bit11 -x52_bit12 -x52_bit13 -x52_bit14 -x52_bit15 -x52_bit16 x54_bit0 -x54_bit1 -x54_bit2 x54_bit3 -x54_bit4 -x54_bit5 -x54_bit6 -x54_bit7 -x54_bit8 -x54_bit9 -x54_bit10 -x54_bit11 -x54_bit12 -x54_bit13 -x54_bit14 -x54_bit15 -x54_bit16 -x56_bit0 -x56_bit1 -x56_bit2 x56_bit3 -x56_bit4 -x56_bit5 -x56_bit6 -x56_bit7 -x56_bit8 -x56_bit9 -x56_bit10 -x56_bit11 -x56_bit12 -x56_bit13 -x56_bit14 -x56_bit15 -x56_bit16 x58_bit0 -x58_bit1 -x58_bit2 x58_bit3 -x58_bit4 -x58_bit5 -x58_bit6 -x58_bit7 -x58_bit8 -x58_bit9 -x58_bit10 -x58_bit11 -x58_bit12 -x58_bit13 -x58_bit14 -x58_bit15 -x58_bit16 x60_bit0 x60_bit1 -x60_bit2 -x60_bit3 -x60_bit4 -x60_bit5 -x60_bit6 -x60_bit7 -x60_bit8 -x60_bit9 -x60_bit10 -x60_bit11 -x60_bit12 -x60_bit13 -x60_bit14 -x60_bit15 -x60_bit16 -x62_bit0 x62_bit1 -x62_bit2 -x62_bit3 -x62_bit4 -x62_bit5 -x62_bit6 -x62_bit7 -x62_bit8 -x62_bit9 -x62_bit10 -x62_bit11 -x62_bit12 -x62_bit13 -x62_bit14 -x62_bit15 -x62_bit16 -x64_bit0 -x64_bit1 -x64_bit2 -x64_bit3 -x64_bit4 -x64_bit5 -x64_bit6 -x64_bit7 -x64_bit8 -x64_bit9 -x64_bit10 -x64_bit11 -x64_bit12 -x64_bit13 -x64_bit14 -x64_bit15 -x64_bit16 -x66_bit0 -x66_bit1 -x66_bit2 -x66_bit3 -x66_bit4 -x66_bit5 -x66_bit6 -x66_bit7 -x66_bit8 -x66_bit9 -x66_bit10 -x66_bit11 -x66_bit12 -x66_bit13 -x66_bit14 -x66_bit15 -x66_bit16 -x68_bit0 -x68_bit1 -x68_bit2 -x68_bit3 -x68_bit4 -x68_bit5 -x68_bit6 -x68_bit7 -x68_bit8 -x68_bit9 -x68_bit10 -x68_bit11 -x68_bit12 -x68_bit13 -x68_bit14 -x68_bit15 -x68_bit16 x70_bit0 x70_bit1 -x70_bit2 -x70_bit3 -x70_bit4 -x70_bit5 -x70_bit6 -x70_bit7 -x70_bit8 -x70_bit9 -x70_bit10 -x70_bit11 -x70_bit12 -x70_bit13 -x70_bit14 -x70_bit15 -x70_bit16 -x72_bit0 -x72_bit1 -x72_bit2 -x72_bit3 -x72_bit4 -x72_bit5 -x72_bit6 -x72_bit7 -x72_bit8 -x72_bit9 -x72_bit10 -x72_bit11 -x72_bit12 -x72_bit13 -x72_bit14 -x72_bit15 -x72_bit16 -x74_bit0 -x74_bit1 -x74_bit2 -x74_bit3 -x74_bit4 -x74_bit5 -x74_bit6 -x74_bit7 -x74_bit8 -x74_bit9 -x74_bit10 -x74_bit11 -x74_bit12 -x74_bit13 -x74_bit14 -x74_bit15 -x74_bit16 -x76_bit0 -x76_bit1 -x76_bit2 -x76_bit3 -x76_bit4 -x76_bit5 -x76_bit6 -x76_bit7 -x76_bit8 -x76_bit9 -x76_bit10 -x76_bit11 -x76_bit12 -x76_bit13 -x76_bit14 -x76_bit15 -x76_bit16 -x78_bit0 -x78_bit1 -x78_bit2 -x78_bit3 -x78_bit4 -x78_bit5 -x78_bit6 -x78_bit7 -x78_bit8 -x78_bit9 -x78_bit10 -x78_bit11 -x78_bit12 -x78_bit13 -x78_bit14 -x78_bit15 -x78_bit16 -x80_bit0 -x80_bit1 -x80_bit2 -x80_bit3 -x80_bit4 -x80_bit5 -x80_bit6 -x80_bit7 -x80_bit8 -x80_bit9 -x80_bit10 -x80_bit11 -x80_bit12 -x80_bit13 -x80_bit14 -x80_bit15 -x80_bit16 -x82_bit0 -x82_bit1 -x82_bit2 -x82_bit3 -x82_bit4 -x82_bit5 -x82_bit6 -x82_bit7 -x82_bit8 -x82_bit9 -x82_bit10 -x82_bit11 -x82_bit12 -x82_bit13 -x82_bit14 -x82_bit15 -x82_bit16 -x84_bit0 -x84_bit1 -x84_bit2 -x84_bit3 -x84_bit4 -x84_bit5 -x84_bit6 -x84_bit7 -x84_bit8 -x84_bit9 -x84_bit10 -x84_bit11 -x84_bit12 -x84_bit13 -x84_bit14 -x84_bit15 -x84_bit16 x86_bit0 -x86_bit1 -x86_bit2 -x86_bit3 -x86_bit4 -x86_bit5 -x86_bit6 -x86_bit7 -x86_bit8 -x86_bit9 -x86_bit10 -x86_bit11 -x86_bit12 -x86_bit13 -x86_bit14 -x86_bit15 -x86_bit16 -x88_bit0 -x88_bit1 -x88_bit2 -x88_bit3 -x88_bit4 -x88_bit5 -x88_bit6 -x88_bit7 -x88_bit8 -x88_bit9 -x88_bit10 -x88_bit11 -x88_bit12 -x88_bit13 -x88_bit14 -x88_bit15 -x88_bit16 -x90_bit0 -x90_bit1 -x90_bit2 -x90_bit3 -x90_bit4 -x90_bit5 -x90_bit6 -x90_bit7 -x90_bit8 -x90_bit9 -x90_bit10 -x90_bit11 -x90_bit12 -x90_bit13 -x90_bit14 -x90_bit15 -x90_bit16 -x92_bit0 x92_bit1 -x92_bit2 -x92_bit3 -x92_bit4 -x92_bit5 -x92_bit6 -x92_bit7 -x92_bit8 -x92_bit9 -x92_bit10 -x92_bit11 -x92_bit12 -x92_bit13 -x92_bit14 -x92_bit15 -x92_bit16 -x94_bit0 -x94_bit1 -x94_bit2 -x94_bit3 -x94_bit4 -x94_bit5 -x94_bit6 -x94_bit7 -x94_bit8 -x94_bit9 -x94_bit10 -x94_bit11 -x94_bit12 -x94_bit13 -x94_bit14 -x94_bit15 -x94_bit16 -x96_bit0 -x96_bit1 -x96_bit2 -x96_bit3 -x96_bit4 -x96_bit5 -x96_bit6 -x96_bit7 -x96_bit8 -x96_bit9 -x96_bit10 -x96_bit11 -x96_bit12 -x96_bit13 -x96_bit14 -x96_bit15 -x96_bit16 -x98_bit0 -x98_bit1 -x98_bit2 -x98_bit3 -x98_bit4 -x98_bit5 -x98_bit6 -x98_bit7 -x98_bit8 -x98_bit9 -x98_bit10 -x98_bit11 -x98_bit12 -x98_bit13 -x98_bit14 -x98_bit15 -x98_bit16 -x100_bit0 -x100_bit1 -x100_bit2 -x100_bit3 -x100_bit4 -x100_bit5 -x100_bit6 -x100_bit7 -x100_bit8 -x100_bit9 -x100_bit10 -x100_bit11 -x100_bit12 -x100_bit13 -x100_bit14 -x100_bit15 -x100_bit16 -x1_bit0 -x2_bit0 -x3_bit0 -x4_bit0 -x5_bit0 -x6_bit0 -x7_bit0 -x8_bit0 -x9_bit0 -x10_bit0 -x11_bit0 -x12_bit0 x13_bit0 -x14_bit0 -x15_bit0 x16_bit0 -x17_bit0 -x18_bit0 -x19_bit0 -x20_bit0 -x21_bit0 -x22_bit0 x23_bit0 -x24_bit0 -x25_bit0 -x26_bit0 x27_bit0 x28_bit0 -x29_bit0 -x30_bit0 x31_bit0 x32_bit0 -x33_bit0 x34_bit0 -x35_bit0 x36_bit0 -x37_bit0 x38_bit0 x39_bit0 -x40_bit0 x41_bit0 -x42_bit0 x43_bit0 x44_bit0 -x45_bit0 x46_bit0 x47_bit0 -x48_bit0 -x49_bit0 x50_bit0 x51_bit0 x53_bit0 x55_bit0 x57_bit0 x59_bit0 x61_bit0 -x63_bit0 -x65_bit0 -x67_bit0 x69_bit0 -x71_bit0 -x73_bit0 -x75_bit0 -x77_bit0 -x79_bit0 -x81_bit0 -x83_bit0 x85_bit0 -x87_bit0 -x89_bit0 x91_bit0 -x93_bit0 -x95_bit0 -x97_bit0 -x99_bit0 -x109_bit_10 -x109_bit_9 -x109_bit_8 -x109_bit_7 -x109_bit_6 -x109_bit_5 -x109_bit_4 -x109_bit_3 -x109_bit_2 -x109_bit_1 -x109_bit0 -x109_bit1 -x109_bit2 -x109_bit3 -x109_bit4 -x109_bit5 -x109_bit6 -x109_bit7 -x109_bit8 -x109_bit9 -x109_bit10 -x109_bit11 -x109_bit12 -x109_bit13 -x109_bit14 -x109_bit15 -x109_bit16 -x109_bit17 -x109_bit18 -x109_bit19 -x124_bit_10 -x124_bit_9 -x124_bit_8 -x124_bit_7 -x124_bit_6 -x124_bit_5 -x124_bit_4 -x124_bit_3 -x124_bit_2 -x124_bit_1 -x124_bit0 -x124_bit1 -x124_bit2 -x124_bit3 -x124_bit4 -x124_bit5 -x124_bit6 -x124_bit7 -x124_bit8 -x124_bit9 -x124_bit10 -x124_bit11 -x124_bit12 -x124_bit13 -x124_bit14 -x124_bit15 -x124_bit16 -x124_bit17 -x124_bit18 -x124_bit19 -x110_bit_10 -x110_bit_9 -x110_bit_8 x110_bit_7 -x110_bit_6 x110_bit_5 x110_bit_4 -x110_bit_3 -x110_bit_2 -x110_bit_1 -x110_bit0 -x110_bit1 -x110_bit2 -x110_bit3 -x110_bit4 -x110_bit5 -x110_bit6 -x110_bit7 -x110_bit8 -x110_bit9 -x110_bit10 -x110_bit11 -x110_bit12 -x110_bit13 -x110_bit14 -x110_bit15 -x110_bit16 -x110_bit17 -x110_bit18 -x110_bit19 -x125_bit_10 -x125_bit_9 -x125_bit_8 -x125_bit_7 -x125_bit_6 -x125_bit_5 -x125_bit_4 -x125_bit_3 -x125_bit_2 -x125_bit_1 -x125_bit0 -x125_bit1 -x125_bit2 -x125_bit3 -x125_bit4 -x125_bit5 -x125_bit6 -x125_bit7 -x125_bit8 -x125_bit9 -x125_bit10 -x125_bit11 -x125_bit12 -x125_bit13 -x125_bit14 -x125_bit15 -x125_bit16 -x125_bit17 -x125_bit18 -x125_bit19 -x111_bit_10 -x111_bit_9 -x111_bit_8 -x111_bit_7 -x111_bit_6 -x111_bit_5 -x111_bit_4 -x111_bit_3 -x111_bit_2 -x111_bit_1 -x111_bit0 -x111_bit1 -x111_bit2 -x111_bit3 -x111_bit4 -x111_bit5 -x111_bit6 -x111_bit7 -x111_bit8 -x111_bit9 -x111_bit10 -x111_bit11 -x111_bit12 -x111_bit13 -x111_bit14 -x111_bit15 -x111_bit16 -x111_bit17 -x111_bit18 -x111_bit19 -x112_bit_10 -x112_bit_9 -x112_bit_8 -x112_bit_7 -x112_bit_6 -x112_bit_5 -x112_bit_4 -x112_bit_3 -x112_bit_2 -x112_bit_1 -x112_bit0 -x112_bit1 -x112_bit2 -x112_bit3 -x112_bit4 -x112_bit5 -x112_bit6 -x112_bit7 -x112_bit8 -x112_bit9 -x112_bit10 -x112_bit11 -x112_bit12 -x112_bit13 -x112_bit14 -x112_bit15 -x112_bit16 -x112_bit17 -x112_bit18 -x112_bit19 -x113_bit_10 -x113_bit_9 -x113_bit_8 -x113_bit_7 -x113_bit_6 -x113_bit_5 -x113_bit_4 -x113_bit_3 -x113_bit_2 -x113_bit_1 -x113_bit0 -x113_bit1 -x113_bit2 -x113_bit3 -x113_bit4 -x113_bit5 -x113_bit6 -x113_bit7 -x113_bit8 -x113_bit9 -x113_bit10 -x113_bit11 -x113_bit12 -x113_bit13 -x113_bit14 -x113_bit15 -x113_bit16 -x113_bit17 -x113_bit18 -x113_bit19 -x114_bit_10 -x114_bit_9 -x114_bit_8 -x114_bit_7 -x114_bit_6 -x114_bit_5 -x114_bit_4 -x114_bit_3 -x114_bit_2 -x114_bit_1 -x114_bit0 -x114_bit1 -x114_bit2 -x114_bit3 -x114_bit4 -x114_bit5 -x114_bit6 -x114_bit7 -x114_bit8 -x114_bit9 -x114_bit10 -x114_bit11 -x114_bit12 -x114_bit13 -x114_bit14 -x114_bit15 -x114_bit16 -x114_bit17 -x114_bit18 -x114_bit19 -x115_bit_10 -x115_bit_9 -x115_bit_8 -x115_bit_7 -x115_bit_6 -x115_bit_5 -x115_bit_4 -x115_bit_3 -x115_bit_2 -x115_bit_1 -x115_bit0 -x115_bit1 -x115_bit2 -x115_bit3 -x115_bit4 -x115_bit5 -x115_bit6 -x115_bit7 -x115_bit8 -x115_bit9 -x115_bit10 -x115_bit11 -x115_bit12 -x115_bit13 -x115_bit14 -x115_bit15 -x115_bit16 -x115_bit17 -x115_bit18 -x115_bit19 -x116_bit_10 -x116_bit_9 -x116_bit_8 -x116_bit_7 -x116_bit_6 -x116_bit_5 -x116_bit_4 -x116_bit_3 -x116_bit_2 -x116_bit_1 -x116_bit0 -x116_bit1 -x116_bit2 -x116_bit3 -x116_bit4 -x116_bit5 -x116_bit6 -x116_bit7 -x116_bit8 -x116_bit9 -x116_bit10 -x116_bit11 -x116_bit12 -x116_bit13 -x116_bit14 -x116_bit15 -x116_bit16 -x116_bit17 -x116_bit18 -x116_bit19 -x117_bit_10 -x117_bit_9 -x117_bit_8 -x117_bit_7 -x117_bit_6 -x117_bit_5 -x117_bit_4 -x117_bit_3 -x117_bit_2 -x117_bit_1 -x117_bit0 -x117_bit1 -x117_bit2 -x117_bit3 -x117_bit4 -x117_bit5 -x117_bit6 -x117_bit7 -x117_bit8 -x117_bit9 -x117_bit10 -x117_bit11 -x117_bit12 -x117_bit13 -x117_bit14 -x117_bit15 -x117_bit16 -x117_bit17 -x117_bit18 -x117_bit19 x118_bit_10 x118_bit_9 x118_bit_8 x118_bit_7 x118_bit_6 x118_bit_5 -x118_bit_4 -x118_bit_3 x118_bit_2 -x118_bit_1 x118_bit0 -x118_bit1 -x118_bit2 -x118_bit3 x118_bit4 -x118_bit5 -x118_bit6 -x118_bit7 -x118_bit8 -x118_bit9 -x118_bit10 -x118_bit11 -x118_bit12 -x118_bit13 -x118_bit14 -x118_bit15 -x118_bit16 -x118_bit17 -x118_bit18 -x118_bit19 -x119_bit_10 -x119_bit_9 -x119_bit_8 -x119_bit_7 -x119_bit_6 -x119_bit_5 -x119_bit_4 -x119_bit_3 -x119_bit_2 -x119_bit_1 -x119_bit0 -x119_bit1 -x119_bit2 -x119_bit3 -x119_bit4 -x119_bit5 -x119_bit6 -x119_bit7 -x119_bit8 -x119_bit9 -x119_bit10 -x119_bit11 -x119_bit12 -x119_bit13 -x119_bit14 -x119_bit15 -x119_bit16 -x119_bit17 -x119_bit18 -x119_bit19 -x120_bit_10 -x120_bit_9 -x120_bit_8 -x120_bit_7 -x120_bit_6 -x120_bit_5 -x120_bit_4 -x120_bit_3 -x120_bit_2 -x120_bit_1 -x120_bit0 -x120_bit1 -x120_bit2 -x120_bit3 -x120_bit4 -x120_bit5 -x120_bit6 -x120_bit7 -x120_bit8 -x120_bit9 -x120_bit10 -x120_bit11 -x120_bit12 -x120_bit13 -x120_bit14 -x120_bit15 -x120_bit16 -x120_bit17 -x120_bit18 -x120_bit19 x121_bit_10 -x121_bit_9 -x121_bit_8 -x121_bit_7 -x121_bit_6 x121_bit_5 x121_bit_4 x121_bit_3 x121_bit_2 -x121_bit_1 x121_bit0 x121_bit1 x121_bit2 x121_bit3 -x121_bit4 -x121_bit5 -x121_bit6 -x121_bit7 -x121_bit8 -x121_bit9 -x121_bit10 -x121_bit11 -x121_bit12 -x121_bit13 -x121_bit14 -x121_bit15 -x121_bit16 -x121_bit17 -x121_bit18 -x121_bit19 -x122_bit_10 -x122_bit_9 -x122_bit_8 -x122_bit_7 -x122_bit_6 -x122_bit_5 -x122_bit_4 -x122_bit_3 -x122_bit_2 -x122_bit_1 -x122_bit0 -x122_bit1 -x122_bit2 -x122_bit3 -x122_bit4 -x122_bit5 -x122_bit6 -x122_bit7 -x122_bit8 -x122_bit9 -x122_bit10 -x122_bit11 -x122_bit12 -x122_bit13 -x122_bit14 -x122_bit15 -x122_bit16 -x122_bit17 -x122_bit18 -x122_bit19 -x123_bit_10 -x123_bit_9 -x123_bit_8 -x123_bit_7 -x123_bit_6 -x123_bit_5 -x123_bit_4 -x123_bit_3 -x123_bit_2 -x123_bit_1 -x123_bit0 -x123_bit1 -x123_bit2 -x123_bit3 -x123_bit4 -x123_bit5 -x123_bit6 -x123_bit7 -x123_bit8 -x123_bit9 -x123_bit10 -x123_bit11 -x123_bit12 -x123_bit13 -x123_bit14 -x123_bit15 -x123_bit16 -x123_bit17 -x123_bit18 -x123_bit19 -x127_bit_10 -x127_bit_9 -x127_bit_8 -x127_bit_7 -x127_bit_6 -x127_bit_5 -x127_bit_4 -x127_bit_3 -x127_bit_2 -x127_bit_1 -x127_bit0 -x127_bit1 -x127_bit2 -x127_bit3 -x127_bit4 -x127_bit5 -x127_bit6 -x127_bit7 -x127_bit8 -x127_bit9 -x127_bit10 -x127_bit11 -x127_bit12 -x127_bit13 -x127_bit14 -x127_bit15 -x127_bit16 -x127_bit17 -x127_bit18 -x127_bit19 -x126_bit_10 -x126_bit_9 -x126_bit_8 -x126_bit_7 -x126_bit_6 -x126_bit_5 -x126_bit_4 -x126_bit_3 -x126_bit_2 -x126_bit_1 -x126_bit0 -x126_bit1 -x126_bit2 -x126_bit3 -x126_bit4 -x126_bit5 -x126_bit6 -x126_bit7 -x126_bit8 -x126_bit9 -x126_bit10 -x126_bit11 -x126_bit12 -x126_bit13 -x126_bit14 -x126_bit15 -x126_bit16 -x126_bit17 -x126_bit18 -x126_bit19 -x128_bit_10 -x128_bit_9 -x128_bit_8 -x128_bit_7 -x128_bit_6 -x128_bit_5 -x128_bit_4 -x128_bit_3 -x128_bit_2 -x128_bit_1 -x128_bit0 -x128_bit1 -x128_bit2 -x128_bit3 -x128_bit4 -x128_bit5 -x128_bit6 -x128_bit7 -x128_bit8 -x128_bit9 -x128_bit10 -x128_bit11 -x128_bit12 -x128_bit13 -x128_bit14 -x128_bit15 -x128_bit16 -x128_bit17 -x128_bit18 -x128_bit19 -x101_bit_10 x101_bit_9 -x101_bit_8 x101_bit_7 x101_bit_6 x101_bit_5 x101_bit_4 -x101_bit_3 x101_bit_2 x101_bit_1 -x101_bit0 x101_bit1 x101_bit2 -x101_bit3 -x101_bit4 -x101_bit5 -x101_bit6 -x101_bit7 -x101_bit8 -x101_bit9 -x101_bit10 -x101_bit11 -x101_bit12 -x101_bit13 -x101_bit14 -x101_bit15 -x101_bit16 -x101_bit17 -x101_bit18 -x101_bit19 -x106_bit_10 -x106_bit_9 -x106_bit_8 -x106_bit_7 -x106_bit_6 -x106_bit_5 -x106_bit_4 -x106_bit_3 x106_bit_2 -x106_bit_1 -x106_bit0 -x106_bit1 -x106_bit2 -x106_bit3 -x106_bit4 -x106_bit5 -x106_bit6 -x106_bit7 -x106_bit8 -x106_bit9 -x106_bit10 -x106_bit11 -x106_bit12 -x106_bit13 -x106_bit14 -x106_bit15 -x106_bit16 -x106_bit17 -x106_bit18 -x106_bit19 -x102_bit_10 -x102_bit_9 -x102_bit_8 -x102_bit_7 -x102_bit_6 -x102_bit_5 x102_bit_4 x102_bit_3 -x102_bit_2 -x102_bit_1 -x102_bit0 -x102_bit1 -x102_bit2 -x102_bit3 -x102_bit4 -x102_bit5 -x102_bit6 -x102_bit7 -x102_bit8 -x102_bit9 -x102_bit10 -x102_bit11 -x102_bit12 -x102_bit13 -x102_bit14 -x102_bit15 -x102_bit16 -x102_bit17 -x102_bit18 -x102_bit19 -x107_bit_10 -x107_bit_9 -x107_bit_8 -x107_bit_7 -x107_bit_6 -x107_bit_5 -x107_bit_4 -x107_bit_3 -x107_bit_2 -x107_bit_1 -x107_bit0 -x107_bit1 -x107_bit2 -x107_bit3 -x107_bit4 -x107_bit5 -x107_bit6 -x107_bit7 -x107_bit8 -x107_bit9 -x107_bit10 -x107_bit11 -x107_bit12 -x107_bit13 -x107_bit14 -x107_bit15 -x107_bit16 -x107_bit17 -x107_bit18 -x107_bit19 -x103_bit_10 -x103_bit_9 x103_bit_8 -x103_bit_7 x103_bit_6 -x103_bit_5 -x103_bit_4 x103_bit_3 x103_bit_2 -x103_bit_1 -x103_bit0 -x103_bit1 -x103_bit2 -x103_bit3 -x103_bit4 -x103_bit5 -x103_bit6 -x103_bit7 -x103_bit8 -x103_bit9 -x103_bit10 -x103_bit11 -x103_bit12 -x103_bit13 -x103_bit14 -x103_bit15 -x103_bit16 -x103_bit17 -x103_bit18 -x103_bit19 -x108_bit_10 -x108_bit_9 -x108_bit_8 -x108_bit_7 -x108_bit_6 -x108_bit_5 -x108_bit_4 -x108_bit_3 -x108_bit_2 -x108_bit_1 -x108_bit0 -x108_bit1 -x108_bit2 -x108_bit3 -x108_bit4 -x108_bit5 -x108_bit6 -x108_bit7 -x108_bit8 -x108_bit9 -x108_bit10 -x108_bit11 -x108_bit12 -x108_bit13 -x108_bit14 -x108_bit15 -x108_bit16 -x108_bit17 -x108_bit18 -x108_bit19 -x104_bit_10 -x104_bit_9 -x104_bit_8 x104_bit_7 x104_bit_6 x104_bit_5 x104_bit_4 x104_bit_3 -x104_bit_2 -x104_bit_1 -x104_bit0 -x104_bit1 -x104_bit2 -x104_bit3 -x104_bit4 -x104_bit5 -x104_bit6 -x104_bit7 -x104_bit8 -x104_bit9 -x104_bit10 -x104_bit11 -x104_bit12 -x104_bit13 -x104_bit14 -x104_bit15 -x104_bit16 -x104_bit17 -x104_bit18 -x104_bit19 -x105_bit_10 x105_bit_9 x105_bit_8 -x105_bit_7 x105_bit_6 x105_bit_5 x105_bit_4 x105_bit_3 -x105_bit_2 x105_bit_1 x105_bit0 -x105_bit1 -x105_bit2 x105_bit3 -x105_bit4 -x105_bit5 -x105_bit6 -x105_bit7 -x105_bit8 -x105_bit9 -x105_bit10 -x105_bit11 -x105_bit12 -x105_bit13 -x105_bit14 -x105_bit15 -x105_bit16 -x105_bit17 -x105_bit18 -x105_bit19
c _______________________________________________________________________________
c 
c restarts              : 40
c conflicts             : 49863          (335 /sec)
c decisions             : 176974         (1189 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 148.805 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/3147/stat): 3147 (minisat+_script) R 3146 3147 22582 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1788581470 712704 3 4294967295 134512640 135087896 3221224496 3221224496 1073744960 0 0 5 0 0 0 0 17 0 0 0
Raw data (/proc/3147/statm): 174 3 169 147 0 27 0
[pid=3147] 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=3148
New process pid=3149
New process pid=3150
execve syscall for /bin/sed executable
One traced child (pid=3149) 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=3150) exited with status: 0
One traced child (pid=3148) exited with status: 0
New process pid=3151
execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable
open syscall for file /dev/null
open syscall for file /oldhome/oroussel/tmp/wulflinc10/normalized-mps-v2-20-10-noswot.opb

[startup+10.0043 s]
Raw data (loadavg): 0.93 0.95 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 3754 0 0 0 964 16 0 0 25 0 1 0 1788581475 17006592 3558 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3151/statm): 4152 3558 145 145 0 4007 0
[pid=3151] vsize: 16608
Current children cumulated CPU time (s) 9.81
Current children cumulated vsize (Kb) 18732

[startup+20.0058 s]
Raw data (loadavg): 0.94 0.96 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 3869 0 0 0 1961 17 0 0 25 0 1 0 1788581475 17477632 3673 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4267 3673 145 145 0 4122 0
[pid=3151] vsize: 17068
Current children cumulated CPU time (s) 19.79
Current children cumulated vsize (Kb) 19192

[startup+30.0064 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 3976 0 0 0 2959 18 0 0 25 0 1 0 1788581475 17932288 3780 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (/proc/3151/statm): 4378 3780 145 145 0 4233 0
[pid=3151] vsize: 17512
Current children cumulated CPU time (s) 29.78
Current children cumulated vsize (Kb) 19636

[startup+40.0069 s]
Raw data (loadavg): 0.95 0.96 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 4067 0 0 0 3957 19 0 0 25 0 1 0 1788581475 18292736 3871 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4466 3871 145 145 0 4321 0
[pid=3151] vsize: 17864
Current children cumulated CPU time (s) 39.77
Current children cumulated vsize (Kb) 19988

[startup+50.0075 s]
Raw data (loadavg): 0.96 0.96 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 4160 0 0 0 4956 20 0 0 25 0 1 0 1788581475 18726912 3964 4294967295 134512640 135094434 3221224432 3221223088 134558218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4572 3964 145 145 0 4427 0
[pid=3151] vsize: 18288
Current children cumulated CPU time (s) 49.77
Current children cumulated vsize (Kb) 20412

[startup+60.008 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 4252 0 0 0 5954 21 0 0 25 0 1 0 1788581475 19103744 4056 4294967295 134512640 135094434 3221224432 3221223120 134554796 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4664 4056 145 145 0 4519 0
[pid=3151] vsize: 18656
Current children cumulated CPU time (s) 59.76
Current children cumulated vsize (Kb) 20780

[startup+70.0086 s]
Raw data (loadavg): 0.97 0.96 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 4289 0 0 0 6953 21 0 0 25 0 1 0 1788581475 19243008 4093 4294967295 134512640 135094434 3221224432 3221223088 134558426 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4698 4093 145 145 0 4553 0
[pid=3151] vsize: 18792
Current children cumulated CPU time (s) 69.75
Current children cumulated vsize (Kb) 20916

[startup+80.0092 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 4357 0 0 0 7952 21 0 0 25 0 1 0 1788581475 19521536 4161 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4766 4161 145 145 0 4621 0
[pid=3151] vsize: 19064
Current children cumulated CPU time (s) 79.74
Current children cumulated vsize (Kb) 21188

[startup+90.0097 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 4390 0 0 0 8952 21 0 0 25 0 1 0 1788581475 19656704 4194 4294967295 134512640 135094434 3221224432 3221223088 134558213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4799 4194 145 145 0 4654 0
[pid=3151] vsize: 19196
Current children cumulated CPU time (s) 89.74
Current children cumulated vsize (Kb) 21320

[startup+100.01 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 4391 0 0 0 9952 21 0 0 25 0 1 0 1788581475 19660800 4195 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4800 4195 145 145 0 4655 0
[pid=3151] vsize: 19200
Current children cumulated CPU time (s) 99.74
Current children cumulated vsize (Kb) 21324

[startup+110.012 s]
Raw data (loadavg): 0.98 0.96 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 4411 0 0 0 10952 21 0 0 25 0 1 0 1788581475 19759104 4215 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4824 4215 145 145 0 4679 0
[pid=3151] vsize: 19296
Current children cumulated CPU time (s) 109.74
Current children cumulated vsize (Kb) 21420

[startup+120.012 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 4420 0 0 0 11952 21 0 0 25 0 1 0 1788581475 19800064 4224 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4834 4224 145 145 0 4689 0
[pid=3151] vsize: 19336
Current children cumulated CPU time (s) 119.74
Current children cumulated vsize (Kb) 21460

[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 4480 0 0 0 12952 22 0 0 25 0 1 0 1788581475 20037632 4284 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4892 4284 145 145 0 4747 0
[pid=3151] vsize: 19568
Current children cumulated CPU time (s) 129.75
Current children cumulated vsize (Kb) 21692

[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.98 2/57 3151
Raw data (/proc/3147/stat): 3147 (minisat+_script) S 3146 3147 22582 0 -1 0 289 239 0 0 0 0 0 1 22 0 1 0 1788581470 2174976 226 4294967295 134512640 135087896 3221224496 3221223768 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (/proc/3147/statm): 531 226 485 147 0 384 0
[pid=3147] vsize: 2124
Raw data (/proc/3151/stat): 3151 (minisat+_64-bit) R 3147 3147 22582 0 -1 0 4480 0 0 0 13952 22 0 0 25 0 1 0 1788581475 20037632 4284 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0
Raw data (/proc/3151/statm): 4892 4284 145 145 0 4747 0
[pid=3151] vsize: 19568
Current children cumulated CPU time (s) 139.75
Current children cumulated vsize (Kb) 21692
One traced child (pid=3151) exited with status: 30
One traced child (pid=3147) exited with status: 30
All traced children have exited ! Game is over.

Child status: 30
Real time (s): 149.332
CPU time (s): 149.087
CPU user time (s): 148.83
CPU system time (s): 0.25696
CPU usage (%): 99.8364
Max. virtual memory (cumulated for all children) (Kb): 21692

Verifier Data

Verifier:	OK	-41