Name | mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-p0040.opb |
MD5SUM | 1c249519911563f3292efb34f4875b44 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 62027 |
Optimality of the best value was proved | YES |
Number of terms in the objective function | 40 |
Biggest coefficient in the objective function | 8161 |
Number of bits for the biggest coefficient in the objective function | 13 |
Sum of the numbers in the objective function | 265332 |
Number of bits of the sum of numbers in the objective function | 19 |
Biggest number in a constraint | 8161 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 265332 |
Number of bits of the biggest sum of numbers | 19 |
Best result obtained on this benchmark | OPTIMUM FOUND |
Best CPU time to get the best result obtained on this benchmark | 7.98079 |
Number of variables | 40 |
Total number of constraints | 63 |
Number of constraints which are clauses | 10 |
Number of constraints which are cardinality constraints (but not clauses) | 50 |
Number of constraints which are nor clauses,nor cardinality constraints | 3 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 10 |
LAUNCH ON wulflinc26 THE 2005-09-20 03:16:46 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3257 boxname=wulflinc26 idbench=913 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 1c249519911563f3292efb34f4875b44 /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-p0040.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-p0040.opb IDLAUNCH: 3257 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.061 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 888604 kB Buffers: 18652 kB Cached: 99072 kB SwapCached: 868 kB Active: 37516 kB Inactive: 82840 kB HighTotal: 131008 kB HighFree: 29596 kB LowTotal: 903652 kB LowFree: 859008 kB SwapTotal: 2097892 kB SwapFree: 2096540 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5704 kB Slab: 19892 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 03:17:54 (client local time) WITH STATUS 30 IN 67.6787 SECONDS stats: 3257 0 67.6787 30
c Parsing PB file... c Converting 23 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ########## c -- Clauses(.)/Splits(s): . c ---[ 21]---> BDD-cost: 5 c ---[ 19]---> BDD-cost: 5 c ---[ 17]---> BDD-cost: 5 c ---[ 15]---> BDD-cost: 5 c ---[ 13]---> BDD-cost: 5 c ---[ 11]---> BDD-cost: 5 c ---[ 9]---> BDD-cost: 5 c ---[ 7]---> BDD-cost: 5 c ---[ 5]---> BDD-cost: 5 c ---[ 3]---> BDD-cost: 5 c ---[ 2]---> BDD-cost: 17 c ---[ 1]---> BDD-cost: 16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 186 521 | 62 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 66539[0m c ---[ 0]---> Sorter-cost: 7884 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 19547 45827 | 6515 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 65737[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 19 | 19777 46482 | 6592 16 536 33.5 | 0.000 % | c | 119 | 19528 45919 | 7251 101 1221 12.1 | 1.637 % | c ============================================================================== c [1mFound solution: 65380[0m c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 170 | 19431 45784 | 6477 142 1778 12.5 | 1.637 % | c ============================================================================== c [1mFound solution: 65203[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 172 | 19449 45882 | 6483 144 1793 12.5 | 1.637 % | c ============================================================================== c [1mFound solution: 65108[0m c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 173 | 19460 45907 | 6486 145 1796 12.4 | 1.637 % | c ============================================================================== c [1mFound solution: 64519[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 191 | 19550 46137 | 6516 163 3580 22.0 | 1.637 % | c | 291 | 19520 46069 | 7167 260 8533 32.8 | 3.079 % | c | 444 | 19432 45878 | 7884 335 8986 26.8 | 3.489 % | c | 669 | 19432 45878 | 8672 560 19185 34.3 | 3.489 % | c | 1009 | 19432 45878 | 9540 900 29806 33.1 | 3.489 % | c | 1516 | 19432 45878 | 10494 1407 48112 34.2 | 3.489 % | c | 2276 | 19420 45851 | 11543 2166 72597 33.5 | 3.530 % | c ============================================================================== c [1mFound solution: 64214[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3130 | 19437 45912 | 6479 3020 106884 35.4 | 3.530 % | c ============================================================================== c [1mFound solution: 64158[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3224 | 19424 45890 | 6474 3112 110084 35.4 | 3.530 % | c | 3325 | 19424 45890 | 7121 3213 112436 35.0 | 3.860 % | c | 3475 | 19424 45890 | 7833 3363 115645 34.4 | 3.860 % | c | 3701 | 19424 45890 | 8616 3589 121232 33.8 | 3.860 % | c ============================================================================== c [1mFound solution: 64135[0m c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3966 | 19434 45912 | 6478 3854 131240 34.1 | 3.860 % | c | 4067 | 19352 45726 | 7125 3954 135460 34.3 | 4.198 % | c | 4217 | 19352 45726 | 7838 4104 141535 34.5 | 4.198 % | c ============================================================================== c [1mFound solution: 64003[0m c ---[ 0]---> Sorter-cost: 7 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4272 | 19433 45929 | 6477 4159 144001 34.6 | 4.198 % | c | 4373 | 19433 45929 | 7124 4260 147968 34.7 | 4.209 % | c | 4523 | 19433 45929 | 7837 4410 150540 34.1 | 4.209 % | c | 4751 | 19433 45929 | 8620 4638 154035 33.2 | 4.209 % | c | 5088 | 19209 45415 | 9482 4972 158178 31.8 | 5.032 % | c | 5594 | 19209 45415 | 10431 5478 171051 31.2 | 5.032 % | c ============================================================================== c [1mFound solution: 63972[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6285 | 19188 45380 | 6396 6168 195709 31.7 | 5.032 % | c | 6387 | 19188 45380 | 7035 6270 198254 31.6 | 5.174 % | c | 6538 | 19188 45380 | 7739 6421 204483 31.8 | 5.174 % | c ============================================================================== c [1mFound solution: 63747[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6676 | 19202 45413 | 6400 6559 210550 32.1 | 5.174 % | c | 6777 | 19202 45413 | 7040 6660 212224 31.9 | 5.181 % | c | 6927 | 19198 45405 | 7744 6807 215854 31.7 | 5.208 % | c | 7152 | 19198 45405 | 8518 7032 224568 31.9 | 5.208 % | c ============================================================================== c [1mFound solution: 63485[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7309 | 19200 45411 | 6400 7177 230480 32.1 | 5.208 % | c | 7410 | 19200 45411 | 7040 3690 92122 25.0 | 5.258 % | c | 7560 | 19200 45411 | 7744 3840 97081 25.3 | 5.259 % | c | 7785 | 19200 45411 | 8518 4065 104678 25.8 | 5.259 % | c | 8122 | 19200 45411 | 9370 4402 114208 25.9 | 5.259 % | c | 8629 | 19200 45411 | 10307 4909 129858 26.5 | 5.259 % | c ============================================================================== c [1mFound solution: 63469[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9339 | 19208 45429 | 6402 5619 150031 26.7 | 5.259 % | c | 9441 | 19208 45429 | 7042 5721 156236 27.3 | 5.269 % | c | 9591 | 19208 45429 | 7746 5871 160687 27.4 | 5.269 % | c | 9817 | 19208 45429 | 8521 6097 167454 27.5 | 5.269 % | c | 10154 | 19208 45429 | 9373 6434 176638 27.5 | 5.269 % | c | 10660 | 19208 45429 | 10310 6940 189839 27.4 | 5.269 % | c ============================================================================== c [1mFound solution: 63444[0m c ---[ 0]---> Sorter-cost: 11 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10890 | 19153 45305 | 6384 7166 198758 27.7 | 5.269 % | c | 10990 | 19153 45305 | 7022 3683 83383 22.6 | 5.545 % | c | 11140 | 19026 45010 | 7724 3828 85245 22.3 | 6.055 % | c ============================================================================== c [1mFound solution: 62690[0m c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11198 | 19087 45156 | 6362 3886 86134 22.2 | 6.055 % | c | 11299 | 19087 45156 | 6998 3987 87540 22.0 | 6.078 % | c ============================================================================== c [1mFound solution: 62215[0m c ---[ 0]---> Sorter-cost: 10 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 11310 | 19102 45200 | 6367 3998 87816 22.0 | 6.078 % | c | 11410 | 19102 45200 | 7003 4098 90516 22.1 | 6.084 % | c | 11561 | 19102 45200 | 7704 4249 93807 22.1 | 6.084 % | c | 11788 | 19102 45200 | 8474 4476 97844 21.9 | 6.084 % | c | 12126 | 19102 45200 | 9321 4814 105320 21.9 | 6.083 % | c | 12632 | 19093 45181 | 10254 5319 118427 22.3 | 6.150 % | c | 13394 | 19093 45181 | 11279 6081 133889 22.0 | 6.150 % | c | 14533 | 19093 45181 | 12407 7220 161123 22.3 | 6.152 % | c ============================================================================== c [1mFound solution: 62191[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 15008 | 19101 45199 | 6367 7689 171924 22.4 | 6.152 % | c | 15108 | 19101 45199 | 7003 3945 74220 18.8 | 6.198 % | c | 15258 | 19003 44977 | 7704 4091 78834 19.3 | 6.558 % | c | 15484 | 19003 44977 | 8474 4317 84306 19.5 | 6.558 % | c | 15822 | 19003 44977 | 9321 4655 92114 19.8 | 6.558 % | c ============================================================================== c [1mFound solution: 62180[0m c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16282 | 19011 44998 | 6337 5115 103759 20.3 | 6.558 % | c | 16382 | 19011 44998 | 6970 5215 105949 20.3 | 6.567 % | c | 16532 | 19011 44998 | 7667 5365 108330 20.2 | 6.568 % | c | 16759 | 19011 44998 | 8434 5592 112725 20.2 | 6.568 % | c | 17097 | 19011 44998 | 9278 5930 121051 20.4 | 6.567 % | c ============================================================================== c [1mFound solution: 62159[0m c ---[ 0]---> Sorter-cost: 8 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17223 | 18987 44943 | 6329 6054 123329 20.4 | 6.567 % | c ============================================================================== c [1mFound solution: 62156[0m c ---[ 0]---> Sorter-cost: 9 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17235 | 18998 44970 | 6332 6066 123601 20.4 | 6.567 % | c ============================================================================== c [1mFound solution: 62119[0m c ---[ 0]---> Sorter-cost: 7 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17243 | 19009 44996 | 6336 6074 123696 20.4 | 6.567 % | c | 17343 | 19009 44996 | 6969 6174 126980 20.6 | 6.735 % | c | 17494 | 19009 44996 | 7666 6325 132499 20.9 | 6.735 % | c ============================================================================== c [1mFound solution: 62104[0m c ---[ 0]---> Sorter-cost: 6 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17710 | 19017 45015 | 6339 6541 139664 21.4 | 6.735 % | c ============================================================================== c [1mFound solution: 62027[0m c ---[ 0]---> Sorter-cost: 4 Base: 3 3 3 3 3 3 7 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 17723 | 19023 45029 | 6341 6554 139846 21.3 | 6.735 % | c | 17825 | 19023 45029 | 6975 6656 141781 21.3 | 6.754 % | c | 17975 | 19023 45029 | 7672 6806 146493 21.5 | 6.754 % | c | 18201 | 19023 45029 | 8439 7032 152199 21.6 | 6.753 % | c ============================================================================== c [1mOptimal solution: 62027[0m s OPTIMUM FOUND v -C1001_bit0 C1002_bit0 -C1003_bit0 -C1004_bit0 -C1005_bit0 C1006_bit0 -C1007_bit0 -C1008_bit0 C1009_bit0 -C1010_bit0 -C1011_bit0 -C1012_bit0 -C1013_bit0 -C1014_bit0 C1015_bit0 -C1016_bit0 -C1017_bit0 C1018_bit0 -C1019_bit0 -C1020_bit0 -C1021_bit0 C1022_bit0 -C1023_bit0 -C1024_bit0 -C1025_bit0 C1026_bit0 -C1027_bit0 -C1028_bit0 C1029_bit0 -C1030_bit0 -C1031_bit0 -C1032_bit0 -C1033_bit0 C1034_bit0 -C1035_bit0 -C1036_bit0 -C1037_bit0 C1038_bit0 -C1039_bit0 -C1040_bit0 c _______________________________________________________________________________ c c restarts : 80 c conflicts : 18521 (276 /sec) c decisions : 40216 (598 /sec) c propagations : 0 (0 /sec) c inspects : 0 (0 /sec) c CPU time : 67.2168 s c _______________________________________________________________________________
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/16822/stat): 16822 (minisat+_script) R 16821 16822 16528 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1855238845 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/16822/statm): 174 3 169 147 0 27 0 [pid=16822] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=16823 New process pid=16824 New process pid=16825 execve syscall for /bin/sed executable One traced child (pid=16824) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=16825) exited with status: 0 One traced child (pid=16823) exited with status: 0 New process pid=16826 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-p0040.opb [startup+10.0032 s] Raw data (loadavg): 0.87 0.95 0.97 2/57 16826 Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16822/statm): 531 226 485 147 0 384 0 [pid=16822] vsize: 2124 Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 1838 0 0 0 984 6 0 0 25 0 1 0 1855238850 3948544 846 4294967295 134512640 135094434 3221224432 3221223056 134557650 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/16826/statm): 964 846 145 145 0 819 0 [pid=16826] vsize: 3856 Current children cumulated CPU time (s) 9.91 Current children cumulated vsize (Kb) 5980 [startup+20.0049 s] Raw data (loadavg): 0.89 0.96 0.97 2/57 16826 Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16822/statm): 531 226 485 147 0 384 0 [pid=16822] vsize: 2124 Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 3245 0 0 0 1977 10 0 0 25 0 1 0 1855238850 5042176 1114 4294967295 134512640 135094434 3221224432 3221221728 134677062 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16826/statm): 1231 1114 145 145 0 1086 0 [pid=16826] vsize: 4924 Current children cumulated CPU time (s) 19.88 Current children cumulated vsize (Kb) 7048 [startup+30.0056 s] Raw data (loadavg): 0.91 0.96 0.97 2/57 16826 Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16822/statm): 531 226 485 147 0 384 0 [pid=16822] vsize: 2124 Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 4555 0 0 0 2969 15 0 0 25 0 1 0 1855238850 5050368 1116 4294967295 134512640 135094434 3221224432 3221221628 134600154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16826/statm): 1233 1116 145 145 0 1088 0 [pid=16826] vsize: 4932 Current children cumulated CPU time (s) 29.85 Current children cumulated vsize (Kb) 7056 [startup+40.0052 s] Raw data (loadavg): 0.92 0.96 0.97 2/57 16826 Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16822/statm): 531 226 485 147 0 384 0 [pid=16822] vsize: 2124 Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 5508 0 0 0 3963 19 0 0 25 0 1 0 1855238850 5005312 1105 4294967295 134512640 135094434 3221224432 3221221552 134676301 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16826/statm): 1222 1105 145 145 0 1077 0 [pid=16826] vsize: 4888 Current children cumulated CPU time (s) 39.83 Current children cumulated vsize (Kb) 7012 [startup+50.0059 s] Raw data (loadavg): 0.93 0.96 0.97 2/57 16826 Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16822/statm): 531 226 485 147 0 384 0 [pid=16822] vsize: 2124 Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 7084 0 0 0 4953 24 0 0 25 0 1 0 1855238850 4984832 1100 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16826/statm): 1217 1100 145 145 0 1072 0 [pid=16826] vsize: 4868 Current children cumulated CPU time (s) 49.78 Current children cumulated vsize (Kb) 6992 [startup+60.0066 s] Raw data (loadavg): 0.94 0.96 0.97 2/57 16826 Raw data (/proc/16822/stat): 16822 (minisat+_script) S 16821 16822 16528 0 -1 0 289 239 0 0 0 1 0 0 22 0 1 0 1855238845 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/16822/statm): 531 226 485 147 0 384 0 [pid=16822] vsize: 2124 Raw data (/proc/16826/stat): 16826 (minisat+_64-bit) R 16822 16822 16528 0 -1 0 11106 0 0 0 5929 38 0 0 25 0 1 0 1855238850 6578176 1490 4294967295 134512640 135094434 3221224432 3221221984 134676539 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/16826/statm): 1606 1490 145 145 0 1461 0 [pid=16826] vsize: 6424 Current children cumulated CPU time (s) 59.68 Current children cumulated vsize (Kb) 8548 One traced child (pid=16826) exited with status: 30 One traced child (pid=16822) exited with status: 30 All traced children have exited ! Game is over. Child status: 30 Real time (s): 68.0104 CPU time (s): 67.6787 CPU user time (s): 67.2268 CPU system time (s): 0.451931 CPU usage (%): 99.5122 Max. virtual memory (cumulated for all children) (Kb): 8548
Verifier: OK 62027