Name | normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-afiro.opb |
MD5SUM | b9a386a980af3ebe560fd16ca36e17ae |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -1486831 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 100 |
Biggest coefficient in the objective function | 131072000 |
Number of bits for the biggest coefficient in the objective function | 27 |
Sum of the numbers in the objective function | 309329625 |
Number of bits of the sum of numbers in the objective function | 29 |
Biggest number in a constraint | 1273495552 |
Number of bits of the biggest number in a constraint | 31 |
Biggest sum of numbers in a constraint | 20473426875 |
Number of bits of the biggest sum of numbers | 35 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 484.119 |
Number of variables | 640 |
Total number of constraints | 27 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 27 |
Minimum length of a constraint | 20 |
Maximum length of a constraint | 180 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc25 THE 2005-05-27 18:57:44 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=15452 boxname=wulflinc25 idbench=1189 idsolver=8 numberseed=0 MD5SUM SOLVER: 4b637b3b6117f2add1a6288e91336322 /oldhome/oroussel/solvers/vallstSAT2005PB.sh MD5SUM BENCH: b9a386a980af3ebe560fd16ca36e17ae /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-afiro.opb REAL COMMAND: vallstSAT2005PB.sh /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-afiro.opb 0 IDLAUNCH: 15452 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 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.220 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: 714632 kB Buffers: 31432 kB Cached: 267984 kB SwapCached: 1008 kB Active: 48504 kB Inactive: 253048 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 714380 kB SwapTotal: 2097892 kB SwapFree: 2095980 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5044 kB Slab: 12608 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 19:03:54 (client local time) WITH STATUS 10 IN 369.247 SECONDS stats: 15452 6 369.247 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### 1: seed: 0 Nr of vars set: 28 (#equs: 0) Nr of vars set: 108 (#equs: 0) #decisions: 942477; #end-nodes: 419770; #proof improvement attempts: 0; #restarts: 1536 Current batch, end-nodes: 0 / 463 (463) #axs: 35, #non-axs: 34 tight: meta-meta: start: 3, end: 4; meta: start: 8, end (keep): 15 loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50 result: the time limit has been exceeded (2) No model found at all. result: the time limit has been exceeded (2) seed: 0 Nr of vars set: 108 (#equs: 0) Time taken: 5 min, 19 sec 2: seed: 0 Nr of vars set: 108 (#equs: 0) Nr of vars set: 108 (#equs: 0) #decisions: 295216; #end-nodes: 117575; #proof improvement attempts: 0; #restarts: 598 Current batch, end-nodes: 251 / 269 (269) #axs: 34, #non-axs: 84 tight: meta-meta: start: 3, end: 3; meta: start: 5, end (keep): 9 loose: meta-meta: start: 9, end: 14; meta: start: 30, end (keep): 50 result: model found (1) seed: 0 Nr of vars set: 494 (#equs: 0) Time taken in seconds: 48 times: 0m0.019s 0m0.006s 5m59.515s 0m9.416s v X02_bit_7 -X02_bit_6 -X02_bit_5 X02_bit_4 -X02_bit_3 X02_bit_2 X02_bit_1 X02_bit0 X02_bit1 X02_bit2 -X02_bit3 -X02_bit4 -X02_bit5 -X02_bit6 -X02_bit7 -X02_bit8 -X02_bit9 -X02_bit10 -X02_bit11 -X02_bit12 X14_bit_7 -X14_bit_6 -X14_bit_5 X14_bit_4 -X14_bit_3 -X14_bit_2 -X14_bit_1 -X14_bit0 X14_bit1 -X14_bit2 -X14_bit3 -X14_bit4 -X14_bit5 -X14_bit6 -X14_bit7 -X14_bit8 -X14_bit9 -X14_bit10 -X14_bit11 -X14_bit12 X23_bit_7 X23_bit_6 X23_bit_5 X23_bit_4 -X23_bit_3 X23_bit_2 X23_bit_1 X23_bit0 X23_bit1 -X23_bit2 -X23_bit3 X23_bit4 X23_bit5 X23_bit6 -X23_bit7 X23_bit8 -X23_bit9 -X23_bit10 -X23_bit11 -X23_bit12 -X36_bit_7 -X36_bit_6 -X36_bit_5 -X36_bit_4 X36_bit_3 -X36_bit_2 -X36_bit_1 -X36_bit0 -X36_bit1 -X36_bit2 X36_bit3 -X36_bit4 -X36_bit5 -X36_bit6 -X36_bit7 X36_bit8 -X36_bit9 -X36_bit10 -X36_bit11 -X36_bit12 X39_bit_7 -X39_bit_6 -X39_bit_5 -X39_bit_4 -X39_bit_3 -X39_bit_2 -X39_bit_1 X39_bit0 -X39_bit1 -X39_bit2 -X39_bit3 -X39_bit4 -X39_bit5 -X39_bit6 -X39_bit7 -X39_bit8 -X39_bit9 -X39_bit10 -X39_bit11 -X39_bit12 -X01_bit_7 X01_bit_6 -X01_bit_5 X01_bit_4 -X01_bit_3 X01_bit_2 X01_bit_1 X01_bit0 -X01_bit1 -X01_bit2 X01_bit3 -X01_bit4 -X01_bit5 X01_bit6 -X01_bit7 -X01_bit8 -X01_bit9 -X01_bit10 -X01_bit11 -X01_bit12 X03_bit_7 -X03_bit_6 -X03_bit_5 -X03_bit_4 -X03_bit_3 -X03_bit_2 -X03_bit_1 -X03_bit0 X03_bit1 -X03_bit2 -X03_bit3 -X03_bit4 -X03_bit5 X03_bit6 -X03_bit7 -X03_bit8 -X03_bit9 -X03_bit10 -X03_bit11 -X03_bit12 X04_bit_7 -X04_bit_6 -X04_bit_5 -X04_bit_4 -X04_bit_3 X04_bit_2 -X04_bit_1 -X04_bit0 X04_bit1 X04_bit2 X04_bit3 -X04_bit4 -X04_bit5 X04_bit6 -X04_bit7 -X04_bit8 -X04_bit9 -X04_bit10 -X04_bit11 -X04_bit12 X06_bit_7 -X06_bit_6 -X06_bit_5 -X06_bit_4 -X06_bit_3 -X06_bit_2 -X06_bit_1 -X06_bit0 -X06_bit1 -X06_bit2 -X06_bit3 -X06_bit4 -X06_bit5 -X06_bit6 X06_bit7 -X06_bit8 -X06_bit9 -X06_bit10 -X06_bit11 -X06_bit12 -X07_bit_7 -X07_bit_6 -X07_bit_5 -X07_bit_4 -X07_bit_3 -X07_bit_2 -X07_bit_1 X07_bit0 -X07_bit1 -X07_bit2 -X07_bit3 -X07_bit4 -X07_bit5 -X07_bit6 -X07_bit7 -X07_bit8 -X07_bit9 -X07_bit10 -X07_bit11 -X07_bit12 -X08_bit_7 -X08_bit_6 X08_bit_5 -X08_bit_4 -X08_bit_3 -X08_bit_2 -X08_bit_1 -X08_bit0 -X08_bit1 -X08_bit2 -X08_bit3 -X08_bit4 -X08_bit5 -X08_bit6 -X08_bit7 -X08_bit8 -X08_bit9 -X08_bit10 -X08_bit11 -X08_bit12 X09_bit_7 -X09_bit_6 -X09_bit_5 -X09_bit_4 -X09_bit_3 X09_bit_2 -X09_bit_1 -X09_bit0 -X09_bit1 -X09_bit2 -X09_bit3 -X09_bit4 -X09_bit5 -X09_bit6 -X09_bit7 -X09_bit8 -X09_bit9 -X09_bit10 -X09_bit11 -X09_bit12 X15_bit_7 -X15_bit_6 X15_bit_5 X15_bit_4 X15_bit_3 -X15_bit_2 -X15_bit_1 X15_bit0 X15_bit1 X15_bit2 X15_bit3 X15_bit4 X15_bit5 X15_bit6 -X15_bit7 -X15_bit8 -X15_bit9 -X15_bit10 -X15_bit11 -X15_bit12 -X16_bit_7 -X16_bit_6 -X16_bit_5 -X16_bit_4 -X16_bit_3 -X16_bit_2 -X16_bit_1 X16_bit0 -X16_bit1 -X16_bit2 X16_bit3 -X16_bit4 -X16_bit5 -X16_bit6 X16_bit7 -X16_bit8 -X16_bit9 -X16_bit10 -X16_bit11 -X16_bit12 -X22_bit_7 -X22_bit_6 -X22_bit_5 -X22_bit_4 -X22_bit_3 -X22_bit_2 -X22_bit_1 -X22_bit0 -X22_bit1 X22_bit2 -X22_bit3 X22_bit4 X22_bit5 X22_bit6 X22_bit7 X22_bit8 -X22_bit9 -X22_bit10 -X22_bit11 -X22_bit12 X24_bit_7 -X24_bit_6 -X24_bit_5 -X24_bit_4 X24_bit_3 -X24_bit_2 -X24_bit_1 -X24_bit0 -X24_bit1 -X24_bit2 -X24_bit3 -X24_bit4 -X24_bit5 -X24_bit6 X24_bit7 -X24_bit8 -X24_bit9 -X24_bit10 -X24_bit11 -X24_bit12 -X25_bit_7 -X25_bit_6 -X25_bit_5 -X25_bit_4 -X25_bit_3 -X25_bit_2 -X25_bit_1 -X25_bit0 -X25_bit1 -X25_bit2 -X25_bit3 -X25_bit4 -X25_bit5 -X25_bit6 -X25_bit7 -X25_bit8 -X25_bit9 -X25_bit10 -X25_bit11 -X25_bit12 -X26_bit_7 -X26_bit_6 -X26_bit_5 -X26_bit_4 -X26_bit_3 -X26_bit_2 -X26_bit_1 X26_bit0 X26_bit1 X26_bit2 -X26_bit3 X26_bit4 -X26_bit5 X26_bit6 X26_bit7 -X26_bit8 -X26_bit9 -X26_bit10 -X26_bit11 -X26_bit12 -X28_bit_7 -X28_bit_6 -X28_bit_5 -X28_bit_4 -X28_bit_3 -X28_bit_2 -X28_bit_1 -X28_bit0 -X28_bit1 -X28_bit2 -X28_bit3 -X28_bit4 -X28_bit5 -X28_bit6 -X28_bit7 -X28_bit8 -X28_bit9 -X28_bit10 -X28_bit11 -X28_bit12 -X29_bit_7 -X29_bit_6 -X29_bit_5 -X29_bit_4 -X29_bit_3 -X29_bit_2 -X29_bit_1 -X29_bit0 -X29_bit1 X29_bit2 -X29_bit3 -X29_bit4 -X29_bit5 -X29_bit6 -X29_bit7 X29_bit8 -X29_bit9 -X29_bit10 -X29_bit11 -X29_bit12 -X30_bit_7 -X30_bit_6 -X30_bit_5 -X30_bit_4 -X30_bit_3 -X30_bit_2 -X30_bit_1 -X30_bit0 -X30_bit1 -X30_bit2 -X30_bit3 -X30_bit4 -X30_bit5 -X30_bit6 -X30_bit7 -X30_bit8 -X30_bit9 -X30_bit10 -X30_bit11 -X30_bit12 -X31_bit_7 -X31_bit_6 -X31_bit_5 -X31_bit_4 X31_bit_3 -X31_bit_2 X31_bit_1 -X31_bit0 -X31_bit1 -X31_bit2 -X31_bit3 -X31_bit4 -X31_bit5 -X31_bit6 -X31_bit7 -X31_bit8 -X31_bit9 -X31_bit10 -X31_bit11 -X31_bit12 -X38_bit_7 -X38_bit_6 X38_bit_5 -X38_bit_4 -X38_bit_3 -X38_bit_2 -X38_bit_1 -X38_bit0 -X38_bit1 -X38_bit2 -X38_bit3 X38_bit4 X38_bit5 X38_bit6 -X38_bit7 -X38_bit8 -X38_bit9 -X38_bit10 -X38_bit11 -X38_bit12 X37_bit_7 X37_bit_6 X37_bit_5 X37_bit_4 X37_bit_3 X37_bit_2 -X37_bit_1 -X37_bit0 X37_bit1 X37_bit2 X37_bit3 -X37_bit4 X37_bit5 -X37_bit6 -X37_bit7 -X37_bit8 -X37_bit9 -X37_bit10 -X37_bit11 -X37_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 X12_bit_7 X12_bit_6 X12_bit_5 X12_bit_4 X12_bit_3 X12_bit_2 X12_bit_1 X12_bit0 X12_bit1 X12_bit2 X12_bit3 X12_bit4 X12_bit5 X12_bit6 X12_bit7 X12_bit8 X12_bit9 X12_bit10 X12_bit11 X12_bit12 X13_bit_7 X13_bit_6 X13_bit_5 X13_bit_4 X13_bit_3 X13_bit_2 X13_bit_1 X13_bit0 X13_bit1 X13_bit2 X13_bit3 X13_bit4 X13_bit5 X13_bit6 X13_bit7 X13_bit8 X13_bit9 X13_bit10 X13_bit11 X13_bit12 X32_bit_7 X32_bit_6 X32_bit_5 X32_bit_4 X32_bit_3 X32_bit_2 X32_bit_1 X32_bit0 X32_bit1 X32_bit2 X32_bit3 X32_bit4 X32_bit5 X32_bit6 X32_bit7 X32_bit8 X32_bit9 X32_bit10 X32_bit11 X32_bit12 X33_bit_7 X33_bit_6 X33_bit_5 X33_bit_4 X33_bit_3 X33_bit_2 X33_bit_1 X33_bit0 X33_bit1 X33_bit2 X33_bit3 X33_bit4 X33_bit5 X33_bit6 X33_bit7 X33_bit8 X33_bit9 X33_bit10 X33_bit11 X33_bit12 X34_bit_7 X34_bit_6 X34_bit_5 X34_bit_4 X34_bit_3 X34_bit_2 X34_bit_1 X34_bit0 X34_bit1 X34_bit2 X34_bit3 X34_bit4 X34_bit5 X34_bit6 X34_bit7 X34_bit8 X34_bit9 X34_bit10 X34_bit11 -X34_bit12 X35_bit_7 X35_bit_6 X35_bit_5 X35_bit_4 X35_bit_3 X35_bit_2 X35_bit_1 X35_bit0 X35_bit1 X35_bit2 X35_bit3 X35_bit4 X35_bit5 X35_bit6 X35_bit7 X35_bit8 X35_bit9 X35_bit10 X35_bit11 -X35_bit12 s SATISFIABLE #### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Enforcing Stack size limit: 67108864 bytes Current StackSize limit: 67108864 bytes Raw data (loadavg): 0.70 0.91 0.94 2/54 3795 Raw data (stat): 3795 (runsolver) R 3794 1586 1585 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 858513724 884736 94 4294967295 134512640 135332820 3221224448 3221219612 135092226 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+10.0008 s] Raw data (loadavg): 0.74 0.91 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+20.0001 s] Raw data (loadavg): 0.78 0.91 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+30.001 s] Raw data (loadavg): 0.81 0.91 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+40.0005 s] Raw data (loadavg): 0.84 0.92 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+50.0008 s] Raw data (loadavg): 0.87 0.92 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+60.0007 s] Raw data (loadavg): 0.89 0.92 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+70.0003 s] Raw data (loadavg): 0.90 0.92 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+80.0006 s] Raw data (loadavg): 0.92 0.92 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+90.0005 s] Raw data (loadavg): 0.93 0.93 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+100.001 s] Raw data (loadavg): 0.94 0.93 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+110.001 s] Raw data (loadavg): 0.95 0.93 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+120.001 s] Raw data (loadavg): 0.96 0.93 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+130.002 s] Raw data (loadavg): 0.96 0.93 0.94 2/55 3798 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+140.001 s] Raw data (loadavg): 0.97 0.94 0.94 2/56 3799 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+150.002 s] Raw data (loadavg): 1.05 0.95 0.95 2/55 3851 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+160.002 s] Raw data (loadavg): 1.04 0.95 0.95 2/55 3851 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+170.001 s] Raw data (loadavg): 1.03 0.96 0.95 2/55 3851 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+180.004 s] Raw data (loadavg): 1.03 0.96 0.95 2/55 3851 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+190.004 s] Raw data (loadavg): 1.02 0.96 0.95 2/55 3851 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+200.005 s] Raw data (loadavg): 1.02 0.96 0.95 2/55 3851 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+210.006 s] Raw data (loadavg): 1.02 0.96 0.95 2/55 3851 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+220.005 s] Raw data (loadavg): 1.01 0.96 0.95 2/55 3853 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+230.006 s] Raw data (loadavg): 1.01 0.96 0.95 2/55 3853 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+240.006 s] Raw data (loadavg): 1.01 0.96 0.95 2/55 3853 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+250.006 s] Raw data (loadavg): 1.01 0.96 0.95 2/55 3853 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+260.005 s] Raw data (loadavg): 1.00 0.96 0.95 2/55 3853 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+270.005 s] Raw data (loadavg): 1.00 0.97 0.95 2/55 3853 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+280.006 s] Raw data (loadavg): 1.00 0.97 0.95 2/55 3853 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+290.006 s] Raw data (loadavg): 1.00 0.97 0.95 2/55 3853 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+300.007 s] Raw data (loadavg): 1.00 0.97 0.95 2/55 3853 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+310.007 s] Raw data (loadavg): 1.00 0.97 0.95 2/55 3853 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 321 231 0 0 1 0 0 0 20 0 1 0 858513724 2179072 242 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 242 485 147 0 385 0 vsize: 2128 [startup+320.007 s] Raw data (loadavg): 1.00 0.97 0.95 2/55 3855 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 369 739 0 0 1 0 31323 677 19 0 1 0 858513724 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 248 485 147 0 385 0 vsize: 2128 [startup+330.008 s] Raw data (loadavg): 1.00 0.97 0.95 2/55 3855 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 369 739 0 0 1 0 31323 677 19 0 1 0 858513724 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 248 485 147 0 385 0 vsize: 2128 [startup+340.007 s] Raw data (loadavg): 1.00 0.97 0.95 2/55 3855 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 369 739 0 0 1 0 31323 677 19 0 1 0 858513724 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 248 485 147 0 385 0 vsize: 2128 [startup+350.008 s] Raw data (loadavg): 1.00 0.97 0.95 2/55 3855 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 369 739 0 0 1 0 31323 677 19 0 1 0 858513724 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 248 485 147 0 385 0 vsize: 2128 [startup+360.008 s] Raw data (loadavg): 1.00 0.97 0.95 2/55 3855 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 369 739 0 0 1 0 31323 677 19 0 1 0 858513724 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 248 485 147 0 385 0 vsize: 2128 [startup+369.571 s] Raw data (loadavg): 1.00 0.97 0.95 1/53 3865 Raw data (stat): 3795 (vallstSAT2005PB) S 3794 1586 1585 0 -1 0 369 739 0 0 1 0 31323 677 19 0 1 0 858513724 2179072 248 4294967295 134512640 135087896 3221224512 3221223240 1074634510 0 65536 5 1132560122 3222414538 0 0 17 1 0 0 Raw data (statm): 532 248 485 147 0 385 0 vsize: 0 Child status: 10 Real time (s): 369.57 CPU time (s): 369.247 CPU user time (s): 359.735 CPU system time (s): 9.51155 CPU usage (%): 99.9125 Max. virtual memory (Kb): 2128 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### Verifier: FAILED ERROR: unsatisfied constraint on line 57 #### END VERIFIER DATA ####