Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-markshare2.opb |
MD5SUM | 3b5121187baf09367bd50bdc4d869d21 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 8448 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 140 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 7340025 |
Number of bits of the sum of numbers in the objective function | 23 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 7340025 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.43 |
Number of variables | 200 |
Total number of constraints | 67 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 7 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 80 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc18 THE 2005-05-25 22:26:51 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22542 boxname=wulflinc18 idbench=1358 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 3b5121187baf09367bd50bdc4d869d21 /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-markshare2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-markshare2.opb IDLAUNCH: 22542 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.177 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.177 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: 666480 kB Buffers: 38752 kB Cached: 301476 kB SwapCached: 588 kB Active: 71500 kB Inactive: 274100 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 666228 kB SwapTotal: 2097892 kB SwapFree: 2096632 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5668 kB Slab: 16896 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-25 22:47:21 (client local time) WITH STATUS 152 IN 1229.84 SECONDS stats: 22542 7 1229.84 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 14 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####### c -- Clauses(.)/Splits(s): (none) c ---[ 12]---> Adder-cost: 354 maxlim: 431615 bits: 20/19 c ---[ 10]---> Adder-cost: 380 maxlim: 461183 bits: 20/19 c ---[ 8]---> Adder-cost: 350 maxlim: 445183 bits: 20/19 c ---[ 6]---> Adder-cost: 340 maxlim: 477951 bits: 20/19 c ---[ 4]---> Adder-cost: 390 maxlim: 451839 bits: 20/19 c ---[ 2]---> Adder-cost: 358 maxlim: 468735 bits: 20/19 c ---[ 0]---> Adder-cost: 374 maxlim: 444543 bits: 20/19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 17222 61228 | 5740 0 0 nan | 0.000 % | c | 100 | 17222 61228 | 6314 100 905 9.1 | 9.969 % | c | 253 | 17214 61202 | 6945 252 2033 8.1 | 10.003 % | c | 478 | 17206 61176 | 7639 476 4722 9.9 | 10.038 % | c ============================================================================== c [1mFound solution: 866304[0m c ---[ 0]---> Sorter-cost: 1068 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 536 | 19853 67360 | 6617 534 5740 10.7 | 10.038 % | c ============================================================================== c [1mFound solution: 828672[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 632 | 19863 67400 | 6621 629 13956 22.2 | 10.038 % | c | 733 | 19863 67400 | 7283 730 20234 27.7 | 7.644 % | c | 884 | 19855 67374 | 8011 879 45616 51.9 | 7.696 % | c | 1110 | 19847 67348 | 8812 1105 70591 63.9 | 7.696 % | c | 1447 | 19839 67322 | 9693 1441 95879 66.5 | 7.723 % | c ============================================================================== c [1mFound solution: 702720[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1945 | 19842 67325 | 6614 1938 159401 82.3 | 7.723 % | c | 2046 | 19842 67325 | 7275 2039 167910 82.3 | 7.761 % | c | 2197 | 19842 67325 | 8002 2190 179220 81.8 | 7.761 % | c | 2423 | 19842 67325 | 8803 2416 196028 81.1 | 7.761 % | c | 2761 | 19842 67325 | 9683 2754 236792 86.0 | 7.761 % | c | 3268 | 19842 67325 | 10651 3261 287766 88.2 | 7.761 % | c ============================================================================== c [1mFound solution: 676352[0m c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3715 | 19858 67370 | 6619 3708 318920 86.0 | 7.761 % | c | 3815 | 19858 67370 | 7280 3808 328892 86.4 | 7.766 % | c | 3965 | 19858 67370 | 8008 3958 346566 87.6 | 7.766 % | c | 4190 | 19858 67370 | 8809 4183 366380 87.6 | 7.766 % | c | 4528 | 19852 67357 | 9690 4520 400494 88.6 | 7.819 % | c | 5034 | 19844 67331 | 10659 5025 444892 88.5 | 7.845 % | c | 5794 | 19836 67305 | 11725 5784 509124 88.0 | 7.871 % | c | 6934 | 19828 67279 | 12898 6923 580155 83.8 | 7.897 % | c ============================================================================== c [1mFound solution: 674304[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7359 | 19838 67302 | 6612 7348 621804 84.6 | 7.897 % | c | 7463 | 19838 67302 | 7273 3778 243653 64.5 | 7.913 % | c | 7614 | 19838 67302 | 8000 3929 255506 65.0 | 7.913 % | c ============================================================================== c [1mFound solution: 654336[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7790 | 19849 67335 | 6616 4105 268736 65.5 | 7.913 % | c ============================================================================== c [1mFound solution: 645120[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7856 | 19857 67359 | 6619 4171 271081 65.0 | 7.913 % | c | 7958 | 19857 67359 | 7280 4273 278513 65.2 | 7.938 % | c ============================================================================== c [1mFound solution: 465408[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8075 | 19869 67387 | 6623 4390 284865 64.9 | 7.938 % | c | 8175 | 19869 67387 | 7285 4490 290752 64.8 | 7.949 % | c | 8326 | 19869 67387 | 8013 4641 302249 65.1 | 7.949 % | c | 8551 | 19869 67387 | 8815 4866 312895 64.3 | 7.949 % | c | 8888 | 19869 67387 | 9696 5203 337269 64.8 | 7.949 % | c | 9394 | 19869 67387 | 10666 5709 372234 65.2 | 7.949 % | c | 10153 | 19869 67387 | 11733 6468 427615 66.1 | 7.949 % | c | 11294 | 19869 67387 | 12906 7609 506572 66.6 | 7.949 % | c | 13003 | 19863 67369 | 14196 9317 680687 73.1 | 7.975 % | c | 15565 | 19838 67290 | 15616 11876 979173 82.4 | 8.079 % | c | 19410 | 19838 67290 | 17178 15721 1427200 90.8 | 8.079 % | c ============================================================================== c [1mFound solution: 426240[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24555 | 19802 67164 | 6600 11781 991951 84.2 | 8.079 % | c | 24656 | 19802 67164 | 7260 5992 340445 56.8 | 8.251 % | c | 24806 | 19802 67164 | 7986 6142 346020 56.3 | 8.251 % | c | 25031 | 19802 67164 | 8784 6367 351779 55.3 | 8.251 % | c | 25370 | 19802 67164 | 9663 6706 376621 56.2 | 8.251 % | c | 25878 | 19802 67164 | 10629 7214 412120 57.1 | 8.251 % | c | 26639 | 19802 67164 | 11692 7975 454198 57.0 | 8.251 % | c | 27779 | 19802 67164 | 12861 9115 506655 55.6 | 8.251 % | c | 29487 | 19802 67164 | 14147 10823 597522 55.2 | 8.251 % | c | 32049 | 19802 67164 | 15562 13385 746703 55.8 | 8.251 % | c | 35893 | 19802 67164 | 17118 9134 445739 48.8 | 8.251 % | c | 41660 | 19802 67164 | 18830 14901 900002 60.4 | 8.251 % | c | 50309 | 19802 67164 | 20713 13630 900207 66.0 | 8.251 % | c | 63285 | 19802 67164 | 22784 15643 876282 56.0 | 8.251 % | c | 82746 | 19802 67164 | 25063 23100 1569191 67.9 | 8.251 % | c ============================================================================== c [1mFound solution: 420352[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 110809 | 19810 67183 | 6603 24998 2030699 81.2 | 8.251 % | c | 110909 | 19810 67183 | 7263 6350 368699 58.1 | 8.269 % | c | 111061 | 19810 67183 | 7989 6502 374493 57.6 | 8.269 % | c | 111288 | 19810 67183 | 8788 6729 385690 57.3 | 8.269 % | c | 111626 | 19810 67183 | 9667 7067 413477 58.5 | 8.269 % | c | 112132 | 19810 67183 | 10634 7573 438726 57.9 | 8.269 % | c | 112891 | 19810 67183 | 11697 8332 475591 57.1 | 8.269 % | c | 114031 | 19810 67183 | 12867 9472 602990 63.7 | 8.269 % | c | 115740 | 19810 67183 | 14154 11181 705503 63.1 | 8.269 % | c ============================================================================== c [1mFound solution: 411392[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 118101 | 19822 67210 | 6607 13542 911670 67.3 | 8.269 % | c | 118201 | 19822 67210 | 7267 6871 405686 59.0 | 8.282 % | c | 118351 | 19822 67210 | 7994 7021 414241 59.0 | 8.282 % | c | 118576 | 19822 67210 | 8793 7246 434055 59.9 | 8.282 % | c | 118913 | 19822 67210 | 9673 7583 456334 60.2 | 8.282 % | c | 119419 | 19822 67210 | 10640 8089 483898 59.8 | 8.282 % | c | 120178 | 19822 67210 | 11704 8848 528469 59.7 | 8.282 % | c | 121317 | 19822 67210 | 12875 9987 592730 59.4 | 8.282 % | c | 123025 | 19822 67210 | 14162 11695 721731 61.7 | 8.282 % | c | 125587 | 19822 67210 | 15578 14257 897308 62.9 | 8.282 % | c | 129431 | 19822 67210 | 17136 9873 539594 54.7 | 8.282 % | c | 135198 | 19814 67184 | 18850 15639 1121030 71.7 | 8.308 % | c | 143849 | 19814 67184 | 20735 14328 969560 67.7 | 8.308 % | c ============================================================================== c [1mFound solution: 404480[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 151309 | 19816 67186 | 6605 11073 646615 58.4 | 8.308 % | c | 151411 | 19816 67186 | 7265 5639 309058 54.8 | 8.374 % | c | 151561 | 19816 67186 | 7992 5789 311658 53.8 | 8.374 % | c | 151786 | 19816 67186 | 8791 6014 337987 56.2 | 8.374 % | c | 152124 | 19816 67186 | 9670 6352 350939 55.2 | 8.374 % | c ============================================================================== c [1mFound solution: 363264[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 152583 | 19829 67218 | 6609 6811 361631 53.1 | 8.374 % | c | 152685 | 19829 67218 | 7269 6913 366844 53.1 | 8.385 % | c | 152836 | 19829 67218 | 7996 7064 390436 55.3 | 8.385 % | c | 153061 | 19829 67218 | 8796 7289 402314 55.2 | 8.385 % | c | 153398 | 19829 67218 | 9676 7626 416355 54.6 | 8.385 % | c | 153907 | 19829 67218 | 10643 8135 436418 53.6 | 8.385 % | c | 154667 | 19829 67218 | 11708 8895 517597 58.2 | 8.385 % | c | 155807 | 19829 67218 | 12879 10035 580468 57.8 | 8.385 % | c | 157517 | 19829 67218 | 14166 11745 642591 54.7 | 8.385 % | c | 160079 | 19829 67218 | 15583 14307 764160 53.4 | 8.385 % | c ============================================================================== c [1mFound solution: 343936[0m c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 162554 | 19860 67292 | 6620 8590 324198 37.7 | 8.385 % | c | 162655 | 19860 67292 | 7282 4396 151608 34.5 | 8.372 % | c | 162807 | 19860 67292 | 8010 4548 161742 35.6 | 8.372 % | c | 163033 | 19860 67292 | 8811 4774 168934 35.4 | 8.372 % | c | 163371 | 19860 67292 | 9692 5112 176581 34.5 | 8.372 % | c | 163877 | 19860 67292 | 10661 5618 253166 45.1 | 8.372 % | c | 164636 | 19860 67292 | 11727 6377 301500 47.3 | 8.372 % | c | 165778 | 19860 67292 | 12900 7519 356921 47.5 | 8.372 % | c | 167486 | 19860 67292 | 14190 9227 445248 48.3 | 8.372 % | c | 170048 | 19860 67292 | 15609 11789 602596 51.1 | 8.372 % | c | 173892 | 19860 67292 | 17170 15633 831926 53.2 | 8.372 % | c | 179659 | 19860 67292 | 18887 12423 597867 48.1 | 8.372 % | c | 188308 | 19848 67265 | 20776 11130 791462 71.1 | 8.449 % | c ============================================================================== c [1mFound solution: 260352[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 188746 | 19854 67281 | 6618 11568 801463 69.3 | 8.449 % | c | 188847 | 19854 67281 | 7279 5885 256847 43.6 | 8.465 % | c | 188997 | 19854 67281 | 8007 6035 266435 44.1 | 8.465 % | c | 189223 | 19854 67281 | 8808 6261 281425 44.9 | 8.465 % | c | 189561 | 19854 67281 | 9689 6599 298712 45.3 | 8.465 % | c | 190067 | 19854 67281 | 10658 7105 319291 44.9 | 8.465 % | c | 190827 | 19854 67281 | 11724 7865 359467 45.7 | 8.465 % | c | 191968 | 19854 67281 | 12896 9006 410789 45.6 | 8.465 % | c | 193677 | 19854 67281 | 14186 10715 531399 49.6 | 8.465 % | c | 196241 | 19854 67281 | 15604 13279 685851 51.6 | 8.465 % | c | 200085 | 19854 67281 | 17165 8898 488070 54.9 | 8.465 % | c | 205852 | 19854 67281 | 18881 14665 711080 48.5 | 8.465 % | c ============================================================================== c [1mFound solution: 80128[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 206193 | 19806 67113 | 6602 14727 700340 47.6 | 8.465 % | c | 206293 | 19806 67113 | 7262 3782 103785 27.4 | 8.666 % | c | 206444 | 19806 67113 | 7988 3933 104553 26.6 | 8.666 % | c | 206669 | 19806 67113 | 8787 4158 107432 25.8 | 8.666 % | c | 207006 | 19806 67113 | 9665 4495 116514 25.9 | 8.666 % | c | 207513 | 19806 67113 | 10632 5002 128589 25.7 | 8.666 % | c ============================================================================== c [1mFound solution: 64896[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 207893 | 19615 66613 | 6538 5362 135046 25.2 | 8.666 % | c | 207995 | 19615 66613 | 7191 5464 137131 25.1 | 10.089 % | c | 208146 | 19615 66613 | 7910 5615 139840 24.9 | 10.089 % | c | 208371 | 19615 66613 | 8702 5840 147321 25.2 | 10.089 % | c | 208708 | 19615 66613 | 9572 6177 155749 25.2 | 10.089 % | c | 209215 | 19615 66613 | 10529 6684 179508 26.9 | 10.089 % | c | 209976 | 19615 66613 | 11582 7445 201615 27.1 | 10.089 % | c | 211115 | 19615 66613 | 12740 8584 243072 28.3 | 10.089 % | c | 212823 | 19615 66613 | 14014 10292 303964 29.5 | 10.089 % | c | 215385 | 19615 66613 | 15416 12854 404034 31.4 | 10.089 % | c | 219229 | 19615 66613 | 16957 8598 318726 37.1 | 10.089 % | c ============================================================================== c [1mFound solution: 63616[0m c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 222041 | 19622 66634 | 6540 11410 477534 41.9 | 10.089 % | c | 222143 | 19622 66634 | 7194 5807 236093 40.7 | 10.102 % | c | 222293 | 19622 66634 | 7913 5957 236962 39.8 | 10.102 % | c | 222518 | 19622 66634 | 8704 6182 240201 38.9 | 10.102 % | c | 222855 | 19622 66634 | 9575 6519 253550 38.9 | 10.102 % | c | 223361 | 19622 66634 | 10532 7025 263589 37.5 | 10.102 % | c | 224121 | 19622 66634 | 11586 7785 284201 36.5 | 10.102 % | c | 225260 | 19622 66634 | 12744 8924 354542 39.7 | 10.102 % | c | 226971 | 19622 66634 | 14019 10635 414350 39.0 | 10.102 % | c | 229533 | 19622 66634 | 15420 13197 533639 40.4 | 10.102 % | c | 233377 | 19607 66589 | 16963 8676 346338 39.9 | 10.179 % | c | 239144 | 19607 66589 | 18659 14443 554456 38.4 | 10.179 % | c | 247793 | 19530 66415 | 20525 13278 517714 39.0 | 10.816 % | c | 260769 | 19429 66185 | 22577 15427 982742 63.7 | 11.633 % | c | 280230 | 19319 65931 | 24835 23197 1024138 44.1 | 12.628 % | c | 309423 | 19319 65931 | 27319 25948 1521579 58.6 | 12.628 % | c ============================================================================== c [1mFound solution: 59008[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 327090 | 19320 65935 | 6440 27848 1354853 48.7 | 12.628 % | c | 327191 | 19320 65935 | 7084 6666 249277 37.4 | 12.732 % | c | 327341 | 19320 65935 | 7792 6816 250694 36.8 | 12.732 % | c | 327566 | 19320 65935 | 8571 7041 259558 36.9 | 12.732 % | c | 327904 | 19320 65935 | 9428 7379 266686 36.1 | 12.732 % | c | 328410 | 19320 65935 | 10371 7885 277400 35.2 | 12.732 % | c | 329171 | 19320 65935 | 11408 8646 299566 34.6 | 12.732 % | c | 330310 | 19320 65935 | 12549 9785 331642 33.9 | 12.732 % | c | 332018 | 19320 65935 | 13804 11493 456254 39.7 | 12.732 % | c | 334582 | 19320 65935 | 15185 14057 533507 38.0 | 12.732 % | c | 338428 | 19320 65935 | 16703 9687 452672 46.7 | 12.732 % | c | 344195 | 19320 65935 | 18374 15454 704774 45.6 | 12.732 % | c | 352844 | 19306 65902 | 20211 14334 779072 54.4 | 12.911 % | c | 365818 | 19288 65862 | 22232 16842 680144 40.4 | 13.038 % | c | 385280 | 19288 65862 | 24455 13318 512736 38.5 | 13.038 % | c | 414473 | 19288 65862 | 26901 17159 819651 47.8 | 13.038 % | c | 458262 | 19259 65797 | 29591 16835 605068 35.9 | 13.242 % | c | 523948 | 19241 65756 | 32550 15348 637855 41.6 | 13.369 % | c | 622474 | 19241 65756 | 35805 17341 946468 54.6 | 13.369 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 6346 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### 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.91 0.95 0.92 2/54 6342 Raw data (stat): 6342 (runsolver) R 6341 24172 24171 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842457259 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0009 s] Raw data (loadavg): 0.93 0.95 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0015 s] Raw data (loadavg): 0.94 0.96 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0014 s] Raw data (loadavg): 0.95 0.96 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0023 s] Raw data (loadavg): 0.95 0.96 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.0019 s] Raw data (loadavg): 0.96 0.96 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0021 s] Raw data (loadavg): 0.97 0.96 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.003 s] Raw data (loadavg): 0.97 0.96 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0027 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0029 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.003 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.003 s] Raw data (loadavg): 0.98 0.96 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.004 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.008 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.007 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.047 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.156 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.156 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.156 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.156 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.156 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.157 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.157 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.158 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.157 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.157 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.158 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.159 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.16 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.16 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.16 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.16 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.16 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.161 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.162 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.161 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.161 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.161 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.162 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.162 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.162 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.163 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.163 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.163 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.164 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.164 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.165 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.164 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.165 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.165 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.165 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.167 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.166 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.166 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.167 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.167 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.167 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.168 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.168 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.169 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.168 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.169 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.169 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.171 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.171 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.172 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.172 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.174 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.174 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.178 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.183 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.184 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.184 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.19 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.191 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.19 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.192 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.192 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.192 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.192 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.192 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.193 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.19 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.19 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.19 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.2 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.21 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.21 s] Raw data (loadavg): 0.99 0.97 0.92 2/55 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.7 s] Raw data (loadavg): 0.99 0.97 0.92 1/53 6346 Raw data (stat): 6342 (minisat+_script) S 6341 24172 24171 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 842457259 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.7 CPU time (s): 1229.84 CPU user time (s): 1229.59 CPU system time (s): 0.244962 CPU usage (%): 100.011 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####