Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-pipex.opb |
MD5SUM | b9c1029cc1d97a8d60e984f96f5d3267 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 788263 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 48 |
Biggest coefficient in the objective function | 107865 |
Number of bits for the biggest coefficient in the objective function | 17 |
Sum of the numbers in the objective function | 2514082 |
Number of bits of the sum of numbers in the objective function | 22 |
Biggest number in a constraint | 107865 |
Number of bits of the biggest number in a constraint | 17 |
Biggest sum of numbers in a constraint | 2514082 |
Number of bits of the biggest sum of numbers | 22 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02184 |
Number of variables | 48 |
Total number of constraints | 73 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 64 |
Number of constraints which are nor clauses,nor cardinality constraints | 9 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 16 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc12 THE 2005-04-22 01:52:59 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12205 boxname=wulflinc12 idbench=939 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b9c1029cc1d97a8d60e984f96f5d3267 /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-pipex.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-pipex.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-20-10-pipex.opb IDLAUNCH: 12205 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.091 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 : 2 cpu MHz : 451.091 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: 711100 kB Buffers: 27484 kB Cached: 274504 kB SwapCached: 476 kB Active: 8652 kB Inactive: 295448 kB HighTotal: 131008 kB HighFree: 108080 kB LowTotal: 903652 kB LowFree: 603020 kB SwapTotal: 2097136 kB SwapFree: 2095888 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5276 kB Slab: 13796 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-22 01:59:51 (client local time) WITH STATUS 0 IN 411.555 SECONDS stats: 12205 7 411.555 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 41 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################ c -- Clauses(.)/Splits(s): (none) c ---[ 40]---> Sorter-cost: 709 Base: 2 5 2 c ---[ 39]---> Sorter-cost: 709 Base: 2 5 2 c ---[ 38]---> Sorter-cost: 709 Base: 2 5 2 c ---[ 37]---> Sorter-cost: 485 Base: 2 5 2 c ---[ 36]---> Sorter-cost: 485 Base: 2 5 2 c ---[ 35]---> Sorter-cost: 485 Base: 2 5 2 c ---[ 34]---> BDD-cost: 145 c ---[ 33]---> Sorter-cost: 847 Base: 2 5 3 3 c ---[ 32]---> Sorter-cost: 846 Base: 2 5 3 3 c ---[ 30]---> BDD-cost: 3 c ---[ 28]---> BDD-cost: 3 c ---[ 26]---> BDD-cost: 3 c ---[ 24]---> BDD-cost: 3 c ---[ 22]---> BDD-cost: 3 c ---[ 20]---> BDD-cost: 3 c ---[ 18]---> BDD-cost: 3 c ---[ 16]---> BDD-cost: 3 c ---[ 14]---> BDD-cost: 3 c ---[ 12]---> BDD-cost: 3 c ---[ 10]---> BDD-cost: 3 c ---[ 8]---> BDD-cost: 3 c ---[ 6]---> BDD-cost: 3 c ---[ 4]---> BDD-cost: 3 c ---[ 2]---> BDD-cost: 3 c ---[ 0]---> BDD-cost: 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 10626 25220 | 3187 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/4140 c -- var.elim.: 2000/4140 c -- var.elim.: 3000/4140 c -- var.elim.: 4000/4140 c -- var.elim.: 4140/4140 c -- var.elim.: 1000/2023 c -- var.elim.: 2000/2023 c -- var.elim.: 2023/2023 c -- var.elim.: 33/33 c -- subsuming c -- var.elim.: 1000/1093 c -- var.elim.: 1093/1093 c -- var.elim.: 399/399 c -- var.elim.: 5/5 c -- subsuming c -- var.elim.: 171/171 c | 0 | 8527 27325 | -- 0 -- -- | -- | -2099/2164 c | 0 | 8527 27325 | 3410 0 0 nan | 0.000 % | c | 100 | 8527 27325 | 3751 100 1606 16.1 | 1.202 % | c | 253 | 8527 27325 | 4127 253 8124 32.1 | 1.202 % | c | 479 | 8527 27325 | 4539 479 18652 38.9 | 1.203 % | c | 817 | 8527 27325 | 4993 817 31708 38.8 | 1.202 % | c ============================================================================== c (current CPU-time: 1.52277 s) c ============================================================================== c [1mFound solution: 849258[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9869 Base: 2 5 3 3 2 2 3 3 3 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1090 | 32385 83129 | 9715 1090 45898 42.1 | 1.202 % | c -- subsuming c -- var.elim.: 1000/8764 c -- var.elim.: 2000/8764 c -- var.elim.: 3000/8764 c -- var.elim.: 4000/8764 c -- var.elim.: 5000/8764 c -- var.elim.: 6000/8764 c -- var.elim.: 7000/8764 c -- var.elim.: 8000/8764 c -- var.elim.: 8764/8764 c -- var.elim.: 1000/4656 c -- var.elim.: 2000/4656 c -- var.elim.: 3000/4656 c -- var.elim.: 4000/4656 c -- var.elim.: 4656/4656 c -- var.elim.: 689/689 c -- var.elim.: 616/616 c -- var.elim.: 74/74 c -- subsuming c -- var.elim.: 1000/1076 c -- var.elim.: 1076/1076 c -- var.elim.: 363/363 c -- var.elim.: 260/260 c -- var.elim.: 286/286 c -- subsuming c -- var.elim.: 341/341 c -- var.elim.: 69/69 c | 1090 | 28420 90753 | -- 1090 -- -- | -- | -3965/7625 c | 1090 | 28420 90753 | 11368 1090 45898 42.1 | 1.202 % | c | 1191 | 28420 90753 | 12504 1191 49320 41.4 | 1.851 % | c | 1342 | 28420 90753 | 13755 1342 53801 40.1 | 1.851 % | c | 1568 | 28420 90753 | 15130 1568 61460 39.2 | 1.851 % | c | 1907 | 28420 90753 | 16643 1907 76328 40.0 | 1.851 % | c ============================================================================== c (current CPU-time: 7.33488 s) c ============================================================================== c [1mFound solution: 833719[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 14 Base: 2 5 3 3 2 2 3 3 3 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2217 | 29748 94113 | 8924 2217 93447 42.2 | 1.851 % | c -- subsuming c -- var.elim.: 1000/1795 c -- var.elim.: 1795/1795 c -- var.elim.: 896/896 c -- var.elim.: 170/170 c -- var.elim.: 126/126 c -- subsuming c -- var.elim.: 35/35 c | 2217 | 29007 93602 | -- 2217 -- -- | -- | -733/-494 c | 2217 | 29007 93602 | 11602 2217 93447 42.2 | 1.851 % | c | 2319 | 29007 93602 | 12763 2319 97129 41.9 | 2.105 % | c | 2470 | 29007 93602 | 14039 2470 101853 41.2 | 2.105 % | c | 2698 | 29007 93602 | 15443 2698 109622 40.6 | 2.105 % | c | 3035 | 29007 93602 | 16987 3035 120872 39.8 | 2.105 % | c | 3541 | 29007 93602 | 18686 3541 141847 40.1 | 2.105 % | c | 4301 | 29007 93602 | 20555 4301 171217 39.8 | 2.105 % | c | 5442 | 29007 93602 | 22610 5442 217424 40.0 | 2.105 % | c ============================================================================== c (current CPU-time: 20.4149 s) c ============================================================================== c [1mFound solution: 820766[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 5 3 3 2 2 3 3 3 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 6489 | 29013 93021 | 8703 6488 280107 43.2 | 2.105 % | c -- subsuming c -- var.elim.: 788/788 c -- var.elim.: 537/537 c -- var.elim.: 91/91 c -- var.elim.: 117/117 c -- subsuming c -- var.elim.: 54/54 c -- var.elim.: 15/15 c | 6489 | 28784 93192 | -- 6488 -- -- | -- | -224/182 c | 6489 | 28784 93192 | 11513 6488 280107 43.2 | 2.105 % | c | 6591 | 28784 93192 | 12664 6590 291648 44.3 | 2.710 % | c | 6742 | 28784 93192 | 13931 6741 299297 44.4 | 2.710 % | c | 6970 | 28784 93192 | 15324 6969 310407 44.5 | 2.710 % | c | 7310 | 28784 93192 | 16857 7309 331421 45.3 | 2.710 % | c | 7817 | 28784 93192 | 18542 7816 355383 45.5 | 2.710 % | c ============================================================================== c (current CPU-time: 27.3408 s) c ============================================================================== c [1mFound solution: 811394[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 5 3 3 2 2 3 3 3 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 8275 | 28942 93786 | 8682 8274 381481 46.1 | 2.710 % | c -- subsuming c -- var.elim.: 422/422 c -- var.elim.: 323/323 c -- var.elim.: 183/183 c -- var.elim.: 146/146 c | 8275 | 28825 94602 | -- 8274 -- -- | -- | -116/819 c | 8275 | 28825 94602 | 11530 8274 381481 46.1 | 2.710 % | c | 8375 | 28825 94602 | 12683 8374 387624 46.3 | 2.751 % | c | 8529 | 28825 94602 | 13951 8528 394569 46.3 | 2.751 % | c | 8754 | 28825 94602 | 15346 8753 404031 46.2 | 2.751 % | c | 9092 | 28825 94602 | 16881 9091 421104 46.3 | 2.751 % | c | 9599 | 28825 94602 | 18569 9598 441269 46.0 | 2.751 % | c | 10359 | 28825 94602 | 20426 10358 474245 45.8 | 2.751 % | c ============================================================================== c (current CPU-time: 38.0762 s) c ============================================================================== c [1mFound solution: 806822[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 15 Base: 2 5 3 3 2 2 3 3 3 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 11439 | 29026 95293 | 8707 11438 562545 49.2 | 2.751 % | c -- subsuming c -- var.elim.: 494/494 c -- var.elim.: 342/342 c -- var.elim.: 154/154 c -- var.elim.: 161/161 c | 11439 | 28893 95786 | -- 11438 -- -- | -- | -133/494 c | 11439 | 28893 95786 | 11557 11438 562545 49.2 | 2.751 % | c | 11539 | 28878 95708 | 12706 11537 570270 49.4 | 2.790 % | c | 11690 | 28878 95708 | 13976 11688 577500 49.4 | 2.790 % | c | 11917 | 28878 95708 | 15374 11915 605289 50.8 | 2.790 % | c | 12255 | 28878 95708 | 16912 12253 625792 51.1 | 2.790 % | c | 12762 | 28878 95708 | 18603 12760 647138 50.7 | 2.790 % | c | 13525 | 28878 95708 | 20463 13523 681122 50.4 | 2.792 % | c | 14664 | 28745 94941 | 22406 14618 767789 52.5 | 2.968 % | c | 16376 | 28731 94872 | 24634 16211 886112 54.7 | 2.998 % | c | 18939 | 28315 92594 | 26706 18773 1175266 62.6 | 3.710 % | c | 22783 | 28258 92362 | 29317 22614 1918940 84.9 | 3.903 % | c | 28550 | 28170 91356 | 32148 28378 2759933 97.3 | 4.037 % | c ============================================================================== c (current CPU-time: 119.871 s) c ============================================================================== c [1mFound solution: 802184[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 5 3 3 2 2 3 3 3 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 32554 | 28171 91396 | 8451 32379 3552485 109.7 | 4.037 % | c -- subsuming c -- var.elim.: 1000/1348 c -- var.elim.: 1348/1348 c -- var.elim.: 993/993 c -- var.elim.: 184/184 c -- var.elim.: 189/189 c -- subsuming c -- var.elim.: 406/406 c -- var.elim.: 58/58 c | 32554 | 27924 92860 | -- 32379 -- -- | -- | -244/1471 c | 32554 | 27924 92860 | 11169 32379 3552485 109.7 | 4.037 % | c | 32655 | 27849 92289 | 12253 4461 117952 26.4 | 4.494 % | c | 32805 | 27665 90762 | 13389 4608 124851 27.1 | 4.796 % | c | 33030 | 27665 90762 | 14728 4833 144555 29.9 | 4.796 % | c | 33367 | 27665 90762 | 16201 5170 174629 33.8 | 4.796 % | c | 33875 | 27665 90762 | 17821 5678 270450 47.6 | 4.796 % | c | 34634 | 27665 90762 | 19604 6437 396073 61.5 | 4.796 % | c | 35773 | 27578 90388 | 21496 7575 554035 73.1 | 5.022 % | c | 37481 | 27578 90388 | 23646 9283 808616 87.1 | 5.022 % | c | 40044 | 27578 90388 | 26010 11846 1281459 108.2 | 5.022 % | c | 43888 | 27578 90388 | 28612 15690 1794683 114.4 | 5.022 % | c | 49654 | 27492 90065 | 31375 21455 2809171 130.9 | 5.203 % | c | 58303 | 27385 89665 | 34378 30099 4300962 142.9 | 5.414 % | c | 71279 | 27332 89416 | 37742 23363 2967685 127.0 | 5.490 % | c ============================================================================== c (current CPU-time: 276.797 s) c ============================================================================== c [1mFound solution: 800174[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 5 3 3 2 2 3 3 3 3 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 74083 | 27464 89888 | 8239 26167 3372779 128.9 | 5.490 % | c -- subsuming c -- var.elim.: 1000/1091 c -- var.elim.: 1091/1091 c -- var.elim.: 645/645 c -- var.elim.: 410/410 c -- var.elim.: 305/305 c -- var.elim.: 34/34 c -- subsuming c -- var.elim.: 263/263 c -- var.elim.: 119/119 c | 74083 | 27121 89995 | -- 26167 -- -- | -- | -335/124 c | 74083 | 27121 89995 | 10848 20847 1228667 58.9 | 5.490 % | c | 74184 | 27121 89995 | 11933 9239 430676 46.6 | 5.634 % | c | 74335 | 27121 89995 | 13126 9390 453323 48.3 | 5.633 % | c | 74561 | 27121 89995 | 14439 9616 481932 50.1 | 5.633 % | c | 74898 | 27121 89995 | 15883 9953 523352 52.6 | 5.634 % | c | 75408 | 27121 89995 | 17471 10463 615191 58.8 | 5.634 % | c | 76168 | 27121 89995 | 19218 11223 744548 66.3 | 5.634 % #### 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 Raw data (loadavg): 0.77 0.85 0.88 2/54 11022 Raw data (stat): 11022 (runsolver) R 11021 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 491683965 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0012 s] Raw data (loadavg): 0.81 0.86 0.88 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 3282 0 0 0 988 10 0 0 25 0 1 0 491683965 11558912 2324 4294967295 134512640 134672761 3221224544 3221223680 134614814 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2822 2324 603 41 0 2781 0 vsize: 11288 [startup+20.0019 s] Raw data (loadavg): 0.84 0.86 0.88 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 3333 0 0 0 1987 10 0 0 25 0 1 0 491683965 11821056 2375 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2886 2375 603 41 0 2845 0 vsize: 11544 [startup+30.0027 s] Raw data (loadavg): 0.86 0.86 0.88 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 4167 0 0 0 2983 14 0 0 25 0 1 0 491683965 13979648 2883 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3413 2883 603 41 0 3372 0 vsize: 13652 [startup+40.0026 s] Raw data (loadavg): 0.88 0.87 0.88 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 4565 0 0 0 3981 16 0 0 25 0 1 0 491683965 14905344 3115 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3639 3115 603 41 0 3598 0 vsize: 14556 [startup+50.0024 s] Raw data (loadavg): 0.90 0.87 0.88 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 4565 0 0 0 4981 16 0 0 25 0 1 0 491683965 14905344 3115 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3639 3115 603 41 0 3598 0 vsize: 14556 [startup+60.0022 s] Raw data (loadavg): 0.92 0.88 0.88 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 4773 0 0 0 5981 16 0 0 25 0 1 0 491683965 15777792 3323 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3852 3323 603 41 0 3811 0 vsize: 15408 [startup+70.0021 s] Raw data (loadavg): 0.93 0.88 0.88 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 5220 0 0 0 6979 18 0 0 25 0 1 0 491683965 17612800 3770 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4300 3770 603 41 0 4259 0 vsize: 17200 [startup+80.0033 s] Raw data (loadavg): 0.94 0.88 0.88 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 5751 0 0 0 7977 20 0 0 25 0 1 0 491683965 19722240 4301 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4815 4301 603 41 0 4774 0 vsize: 19260 [startup+90.0037 s] Raw data (loadavg): 0.95 0.89 0.88 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 6162 0 0 0 8976 22 0 0 25 0 1 0 491683965 21438464 4712 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5234 4712 603 41 0 5193 0 vsize: 20936 [startup+100.004 s] Raw data (loadavg): 0.95 0.89 0.89 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 6561 0 0 0 9974 24 0 0 25 0 1 0 491683965 23031808 5111 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5623 5111 603 41 0 5582 0 vsize: 22492 [startup+110.004 s] Raw data (loadavg): 0.96 0.89 0.89 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 6972 0 0 0 10972 26 0 0 25 0 1 0 491683965 24735744 5522 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6039 5522 603 41 0 5998 0 vsize: 24156 [startup+120.004 s] Raw data (loadavg): 0.97 0.90 0.89 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 7444 0 0 0 11971 27 0 0 25 0 1 0 491683965 26710016 5994 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6521 5994 603 41 0 6480 0 vsize: 26084 [startup+130.005 s] Raw data (loadavg): 0.97 0.90 0.89 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 8129 0 0 0 12969 29 0 0 25 0 1 0 491683965 28147712 6348 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6872 6348 603 41 0 6831 0 vsize: 27488 [startup+140.005 s] Raw data (loadavg): 0.98 0.90 0.89 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 8129 0 0 0 13969 29 0 0 25 0 1 0 491683965 28147712 6348 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6872 6348 603 41 0 6831 0 vsize: 27488 [startup+150.006 s] Raw data (loadavg): 0.98 0.90 0.89 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 8129 0 0 0 14969 29 0 0 25 0 1 0 491683965 28147712 6348 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6872 6348 603 41 0 6831 0 vsize: 27488 [startup+160.006 s] Raw data (loadavg): 0.98 0.91 0.89 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 8129 0 0 0 15969 29 0 0 25 0 1 0 491683965 28147712 6348 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6872 6348 603 41 0 6831 0 vsize: 27488 [startup+170.006 s] Raw data (loadavg): 0.98 0.91 0.89 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 8129 0 0 0 16970 29 0 0 25 0 1 0 491683965 28147712 6348 4294967295 134512640 134672761 3221224544 3221223584 134612878 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6872 6348 603 41 0 6831 0 vsize: 27488 [startup+180.006 s] Raw data (loadavg): 0.99 0.91 0.89 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 8129 0 0 0 17970 29 0 0 25 0 1 0 491683965 28147712 6348 4294967295 134512640 134672761 3221224544 3221223744 134619640 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6872 6348 603 41 0 6831 0 vsize: 27488 [startup+190.006 s] Raw data (loadavg): 0.99 0.91 0.89 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 8129 0 0 0 18970 29 0 0 25 0 1 0 491683965 28147712 6348 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6872 6348 603 41 0 6831 0 vsize: 27488 [startup+200.006 s] Raw data (loadavg): 0.99 0.92 0.90 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 8129 0 0 0 19970 29 0 0 25 0 1 0 491683965 28147712 6348 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6872 6348 603 41 0 6831 0 vsize: 27488 [startup+210.007 s] Raw data (loadavg): 0.99 0.92 0.90 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 8428 0 0 0 20970 30 0 0 25 0 1 0 491683965 29319168 6647 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7158 6647 603 41 0 7117 0 vsize: 28632 [startup+220.007 s] Raw data (loadavg): 0.99 0.92 0.90 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 8843 0 0 0 21968 31 0 0 25 0 1 0 491683965 31027200 7062 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7575 7062 603 41 0 7534 0 vsize: 30300 [startup+230.007 s] Raw data (loadavg): 0.99 0.92 0.90 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 9298 0 0 0 22967 33 0 0 25 0 1 0 491683965 33132544 7517 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8089 7517 603 41 0 8048 0 vsize: 32356 [startup+240.006 s] Raw data (loadavg): 0.99 0.92 0.90 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 9630 0 0 0 23966 33 0 0 25 0 1 0 491683965 34447360 7849 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8410 7849 603 41 0 8369 0 vsize: 33640 [startup+250.006 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 9744 0 0 0 24966 33 0 0 25 0 1 0 491683965 34672640 7927 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8465 7927 603 41 0 8424 0 vsize: 33860 [startup+260.006 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 9744 0 0 0 25966 33 0 0 25 0 1 0 491683965 34672640 7927 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8465 7927 603 41 0 8424 0 vsize: 33860 [startup+270.006 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 9747 0 0 0 26967 33 0 0 25 0 1 0 491683965 34672640 7930 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8465 7930 603 41 0 8424 0 vsize: 33860 [startup+280.006 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10400 0 0 0 27964 36 0 0 25 0 1 0 491683965 34971648 8005 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8538 8005 603 41 0 8497 0 vsize: 34152 [startup+290.007 s] Raw data (loadavg): 0.99 0.93 0.90 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10400 0 0 0 28964 36 0 0 25 0 1 0 491683965 34971648 8005 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8538 8005 603 41 0 8497 0 vsize: 34152 [startup+300.006 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10400 0 0 0 29963 36 0 0 25 0 1 0 491683965 34971648 8005 4294967295 134512640 134672761 3221224544 3221223728 134615840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8538 8005 603 41 0 8497 0 vsize: 34152 [startup+310.006 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10400 0 0 0 30962 36 0 0 25 0 1 0 491683965 34971648 8005 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8538 8005 603 41 0 8497 0 vsize: 34152 [startup+320.007 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10400 0 0 0 31962 36 0 0 25 0 1 0 491683965 34971648 8005 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8538 8005 603 41 0 8497 0 vsize: 34152 [startup+330.006 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10401 0 0 0 32961 36 0 0 25 0 1 0 491683965 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8538 8006 603 41 0 8497 0 vsize: 34152 [startup+340.006 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10401 0 0 0 33961 36 0 0 25 0 1 0 491683965 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8538 8006 603 41 0 8497 0 vsize: 34152 [startup+350.006 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10401 0 0 0 34961 36 0 0 25 0 1 0 491683965 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8538 8006 603 41 0 8497 0 vsize: 34152 [startup+360.006 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10401 0 0 0 35961 37 0 0 25 0 1 0 491683965 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8538 8006 603 41 0 8497 0 vsize: 34152 [startup+370.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10401 0 0 0 36961 37 0 0 25 0 1 0 491683965 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8538 8006 603 41 0 8497 0 vsize: 34152 [startup+380.006 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10401 0 0 0 37961 37 0 0 25 0 1 0 491683965 34971648 8006 4294967295 134512640 134672761 3221224544 3221223688 134616350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8538 8006 603 41 0 8497 0 vsize: 34152 [startup+390.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10401 0 0 0 38961 37 0 0 25 0 1 0 491683965 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8538 8006 603 41 0 8497 0 vsize: 34152 [startup+400.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10401 0 0 0 39961 37 0 0 25 0 1 0 491683965 34971648 8006 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8538 8006 603 41 0 8497 0 vsize: 34152 [startup+410.007 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10401 0 0 0 40961 37 0 0 25 0 1 0 491683965 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8538 8006 603 41 0 8497 0 vsize: 34152 [startup+411.577 s] Raw data (loadavg): 0.99 0.95 0.91 1/53 11022 Raw data (stat): 11022 (minisat+) R 11021 25285 25284 0 -1 0 10401 0 0 0 40961 37 0 0 25 0 1 0 491683965 34971648 8006 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8538 8006 603 41 0 8497 0 vsize: 0 Child ended because it received signal 11 (SIGSEGV) Real time (s): 411.576 CPU time (s): 411.555 CPU user time (s): 411.142 CPU system time (s): 0.413937 CPU usage (%): 99.995 Max. virtual memory (Kb): 34152 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####