Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8d2.opb |
MD5SUM | 44910688b6ba81ef96bbced304e8624c |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 540 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1860 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 1860 |
Number of bits of the sum of numbers in the objective function | 11 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 1860 |
Number of bits of the biggest sum of numbers | 11 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.07284 |
Number of variables | 1860 |
Total number of constraints | 7477 |
Number of constraints which are clauses | 7477 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 10 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-04-14 04:04:53 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4686 boxname=wulflinc4 idbench=174 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 44910688b6ba81ef96bbced304e8624c /oldhome/oroussel/tmp/wulflinc4/normalized-ii8d2.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc4/normalized-ii8d2.opb /oldhome/oroussel/tmp/wulflinc4/normalized-ii8d2.opb IDLAUNCH: 4686 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 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: 890608 kB Buffers: 36368 kB Cached: 87732 kB SwapCached: 0 kB Active: 55640 kB Inactive: 71320 kB HighTotal: 131008 kB HighFree: 39480 kB LowTotal: 903652 kB LowFree: 851128 kB SwapTotal: 2097136 kB SwapFree: 2097136 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6920 kB Slab: 11540 kB Committed_AS: 71676 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 04:24:56 (client local time) WITH STATUS 10 IN 1200.53 SECONDS stats: 4686 7 1200.53 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 7477 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................... c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 7477 16950 | 2492 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 709[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:105556 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4 | 267832 625557 | 89277 4 21 5.2 | 0.000 % | c | 105 | 267797 625479 | 98204 104 990 9.5 | 0.011 % | c | 255 | 262517 613353 | 108025 117 1133 9.7 | 1.843 % | c | 481 | 260784 609388 | 118827 316 7132 22.6 | 2.431 % | c | 818 | 257414 601681 | 130710 605 16107 26.6 | 3.559 % | c | 1324 | 244945 572977 | 143781 927 20906 22.6 | 7.906 % | c | 2083 | 238281 557610 | 158159 1592 31797 20.0 | 10.256 % | c | 3222 | 222827 521986 | 173975 2527 46136 18.3 | 15.749 % | c | 4930 | 198457 465753 | 191373 3784 78083 20.6 | 24.415 % | c | 7492 | 162507 382705 | 210510 5538 123547 22.3 | 37.351 % | c | 11336 | 133989 316602 | 231561 8771 206350 23.5 | 47.726 % | c | 17102 | 123182 291599 | 254717 14099 318956 22.6 | 51.622 % | c ============================================================================== c [1mFound solution: 708[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 22424 | 122700 290476 | 40900 19358 456621 23.6 | 51.622 % | c | 22524 | 122700 290476 | 44990 19458 458088 23.5 | 51.791 % | c | 22677 | 122700 290476 | 49489 19611 461010 23.5 | 51.791 % | c | 22902 | 122700 290476 | 54437 19836 465366 23.5 | 51.791 % | c | 23239 | 122700 290476 | 59881 20173 471155 23.4 | 51.791 % | c | 23747 | 122700 290476 | 65869 20681 479891 23.2 | 51.791 % | c | 24509 | 122696 290467 | 72456 21442 495102 23.1 | 51.792 % | c | 25648 | 121905 288648 | 79702 22534 518550 23.0 | 52.068 % | c | 27356 | 119317 282654 | 87672 24184 565992 23.4 | 53.015 % | c | 29919 | 118622 281055 | 96440 26700 608826 22.8 | 53.257 % | c | 33763 | 117997 279608 | 106084 30262 707751 23.4 | 53.484 % | c | 39530 | 117194 277745 | 116692 36000 851469 23.7 | 53.781 % | c | 48181 | 116631 276448 | 128361 44627 1085310 24.3 | 53.980 % | c | 61155 | 116494 276132 | 141197 57572 1477344 25.7 | 54.029 % | c ============================================================================== c [1mFound solution: 707[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 72975 | 116426 275997 | 38808 69389 3164475 45.6 | 54.029 % | c | 73075 | 116426 275997 | 42688 69489 3166148 45.6 | 54.070 % | c | 73225 | 116422 275988 | 46957 69637 3167997 45.5 | 54.071 % | c | 73451 | 116422 275988 | 51653 69863 3170475 45.4 | 54.071 % | c | 73789 | 116319 275750 | 56818 70186 3179392 45.3 | 54.108 % | c | 74295 | 116319 275750 | 62500 70692 3187327 45.1 | 54.108 % | c | 75054 | 116303 275713 | 68750 71450 3200065 44.8 | 54.114 % | c | 76194 | 116303 275713 | 75625 72590 3234605 44.6 | 54.114 % | c | 77903 | 116303 275713 | 83188 74299 3288648 44.3 | 54.114 % | c | 80465 | 116303 275713 | 91507 76861 3343512 43.5 | 54.114 % | c | 84309 | 116032 275082 | 100657 80670 3679334 45.6 | 54.218 % | c ============================================================================== c [1mFound solution: 706[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 90002 | 115981 274961 | 38660 86332 3815308 44.2 | 54.218 % | c | 90103 | 115879 274722 | 42526 86432 3816015 44.2 | 54.272 % | c | 90253 | 115783 274494 | 46778 86578 3821863 44.1 | 54.314 % | c | 90478 | 115783 274494 | 51456 86803 3829943 44.1 | 54.314 % | c | 90815 | 115775 274476 | 56602 87135 3848326 44.2 | 54.316 % | c | 91321 | 115775 274476 | 62262 87641 3869986 44.2 | 54.316 % | c ============================================================================== c [1mFound solution: 705[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 91729 | 115858 274691 | 38619 88049 3881835 44.1 | 54.316 % | c | 91830 | 115858 274691 | 42480 24770 637506 25.7 | 54.303 % | c | 91982 | 115858 274691 | 46728 24922 638382 25.6 | 54.303 % | c | 92207 | 115858 274691 | 51401 25147 641538 25.5 | 54.303 % | c | 92548 | 115858 274691 | 56542 25488 646512 25.4 | 54.303 % | c | 93054 | 115858 274691 | 62196 25994 653362 25.1 | 54.303 % | c | 93813 | 115858 274691 | 68415 26753 673733 25.2 | 54.303 % | c | 94952 | 115858 274691 | 75257 27892 696049 25.0 | 54.303 % | c | 96660 | 115727 274389 | 82783 29599 736662 24.9 | 54.350 % | c | 99223 | 115727 274389 | 91061 32162 810161 25.2 | 54.350 % | c | 103067 | 115727 274389 | 100167 36006 980976 27.2 | 54.350 % | c | 108833 | 115500 273863 | 110184 41765 1123454 26.9 | 54.434 % | c ============================================================================== c [1mFound solution: 704[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 115702 | 115258 273290 | 38419 48438 1410589 29.1 | 54.434 % | c | 115802 | 115258 273290 | 42260 48538 1413868 29.1 | 54.519 % | c | 115952 | 115258 273290 | 46486 48688 1417876 29.1 | 54.519 % | c | 116177 | 115258 273290 | 51135 48913 1422657 29.1 | 54.519 % | c | 116514 | 115258 273290 | 56249 49250 1428205 29.0 | 54.519 % | c | 117020 | 115258 273290 | 61874 49756 1439101 28.9 | 54.519 % | c | 117779 | 115258 273290 | 68061 50515 1453674 28.8 | 54.519 % | c | 118919 | 115258 273290 | 74867 51655 1496454 29.0 | 54.519 % | c | 120627 | 114711 272035 | 82354 53286 1555708 29.2 | 54.707 % | c ============================================================================== c [1mFound solution: 678[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 120958 | 114937 272625 | 38312 53399 1499579 28.1 | 54.707 % | c | 121058 | 114937 272625 | 42143 53499 1504069 28.1 | 54.727 % | c | 121208 | 114937 272625 | 46357 53649 1508805 28.1 | 54.727 % | c | 121433 | 114937 272625 | 50993 53874 1515156 28.1 | 54.727 % | c | 121770 | 114937 272625 | 56092 54211 1521029 28.1 | 54.727 % | c | 122277 | 114937 272625 | 61701 54718 1541042 28.2 | 54.727 % | c | 123037 | 114830 272375 | 67872 55474 1576038 28.4 | 54.768 % | c | 124177 | 114826 272366 | 74659 56611 1617760 28.6 | 54.770 % | c | 125887 | 114822 272357 | 82125 58316 1700128 29.2 | 54.771 % | c | 128449 | 114822 272357 | 90337 60878 1956489 32.1 | 54.771 % | c ============================================================================== c [1mFound solution: 677[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 131015 | 114713 272125 | 38237 63438 2045057 32.2 | 54.771 % | c | 131116 | 114605 271875 | 42060 63531 2046308 32.2 | 54.871 % | c | 131266 | 114526 271692 | 46266 63677 2047340 32.2 | 54.901 % | c | 131491 | 114526 271692 | 50893 63902 2057815 32.2 | 54.901 % | c | 131829 | 114526 271692 | 55982 64240 2082094 32.4 | 54.901 % | c | 132335 | 114526 271692 | 61581 64746 2107011 32.5 | 54.901 % | c | 133094 | 114526 271692 | 67739 65505 2179772 33.3 | 54.901 % | c | 134234 | 114464 271548 | 74513 66644 2263461 34.0 | 54.925 % | c | 135942 | 114464 271548 | 81964 68352 2322628 34.0 | 54.925 % | c | 138504 | 114464 271548 | 90160 70914 2431284 34.3 | 54.925 % | c | 142348 | 113872 270165 | 99176 74733 2586796 34.6 | 55.156 % | c | 148116 | 113868 270156 | 109094 80497 3434466 42.7 | 55.157 % | c | 156765 | 113673 269706 | 120004 89131 3957652 44.4 | 55.227 % | c ============================================================================== c [1mFound solution: 676[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 163726 | 113522 269340 | 37840 94999 4081195 43.0 | 55.227 % | c | 163826 | 113522 269340 | 41624 31445 833075 26.5 | 55.279 % | c | 163977 | 113522 269340 | 45786 31596 845448 26.8 | 55.279 % | c | 164205 | 113522 269340 | 50365 31824 850469 26.7 | 55.279 % | c | 164542 | 113522 269340 | 55401 32161 857935 26.7 | 55.279 % | c | 165048 | 113522 269340 | 60941 32667 877392 26.9 | 55.279 % | c | 165810 | 113522 269340 | 67035 33429 895225 26.8 | 55.279 % | c | 166951 | 113274 268761 | 73739 34558 922430 26.7 | 55.375 % | c | 168660 | 112885 267863 | 81113 36143 997415 27.6 | 55.517 % | c | 171222 | 112885 267863 | 89224 38705 1238495 32.0 | 55.517 % | c ============================================================================== c [1mFound solution: 673[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 173491 | 113027 268225 | 37675 40974 1617815 39.5 | 55.517 % | c | 173592 | 113027 268225 | 41442 41075 1619426 39.4 | 55.494 % | c | 173742 | 112796 267691 | 45586 41205 1623355 39.4 | 55.578 % | c | 173968 | 112796 267691 | 50145 41431 1641944 39.6 | 55.578 % | c | 174307 | 112796 267691 | 55159 41770 1647935 39.5 | 55.578 % | c | 174813 | 112649 267349 | 60675 42270 1662108 39.3 | 55.635 % | c | 175572 | 112649 267349 | 66743 43029 1678740 39.0 | 55.635 % | c | 176711 | 112649 267349 | 73417 44168 1701419 38.5 | 55.635 % | c | 178419 | 112427 266839 | 80759 45862 1757472 38.3 | 55.712 % | c | 180981 | 112427 266839 | 88835 48424 1819682 37.6 | 55.712 % | c | 184826 | 112427 266839 | 97719 52269 2176370 41.6 | 55.712 % | c | 190593 | 112423 266830 | 107491 58033 2790673 48.1 | 55.713 % | c ============================================================================== c [1mFound solution: 672[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 193011 | 112371 266702 | 37457 60244 3197887 53.1 | 55.713 % | c | 193111 | 112371 266702 | 41202 60344 3199753 53.0 | 55.726 % | c | 193261 | 112371 266702 | 45322 60494 3202983 52.9 | 55.726 % | c | 193486 | 112371 266702 | 49855 60719 3224710 53.1 | 55.726 % | c | 193824 | 112371 266702 | 54840 61057 3230342 52.9 | 55.726 % | c | 194330 | 112371 266702 | 60324 61563 3258077 52.9 | 55.726 % | c | 195089 | 112371 266702 | 66357 62322 3270744 52.5 | 55.726 % | c | 196229 | 111986 265817 | 72993 61838 3264728 52.8 | 55.860 % | c | 197937 | 111982 265808 | 80292 63543 3288059 51.7 | 55.861 % | c | 200499 | 111919 265662 | 88321 66104 3408862 51.6 | 55.885 % | c | 204343 | 111919 265662 | 97153 69948 3555319 50.8 | 55.885 % | c ============================================================================== c [1mFound solution: 671[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 206897 | 111993 265856 | 37331 72502 3836579 52.9 | 55.885 % | c | 206998 | 111896 265630 | 41064 72599 3838041 52.9 | 55.911 % | c | 207148 | 111896 265630 | 45170 72749 3839710 52.8 | 55.911 % | c | 207374 | 111797 265402 | 49687 72970 3842276 52.7 | 55.946 % | c | 207711 | 111797 265402 | 54656 73307 3860555 52.7 | 55.946 % | c | 208218 | 111797 265402 | 60121 73814 3875398 52.5 | 55.946 % | c | 208977 | 111751 265293 | 66134 74524 3896674 52.3 | 55.959 % | c | 210118 | 111751 265293 | 72747 75665 3930226 51.9 | 55.959 % | c | 211826 | 111751 265293 | 80022 77373 4033738 52.1 | 55.959 % | c | 214388 | 111751 265293 | 88024 79935 4127424 51.6 | 55.959 % | c | 218233 | 111555 264837 | 96826 83701 4891913 58.4 | 56.033 % | c | 224000 | 111555 264837 | 106509 89468 5798477 64.8 | 56.033 % | c | 232649 | 111555 264837 | 117160 98117 7560794 77.1 | 56.033 % | c | 245625 | 111409 264496 | 128876 110975 9999404 90.1 | 56.090 % | c c *** TERMINATED *** s SATISFIABLE v x1 -x2 x3 -x4 x5 -x6 x7 -x8 x9 -x10 x11 -x12 x13 -x14 x15 -x16 x17 -x18 x19 -x20 x21 -x22 -x23 x24 x25 -x26 x27 -x28 x29 -x30 x31 -x32 x33 -x34 x35 -x36 x37 -x38 x39 -x40 x41 -x42 x43 -x44 x45 -x46 x47 -x48 x49 -x50 x51 -x52 x53 -x54 -x55 x56 x57 -x58 x59 -x60 x61 -x62 x63 -x64 x65 -x66 x67 -x68 x69 -x70 -x71 x72 x73 -x74 x75 -x76 x77 -x78 x79 -x80 x81 -x82 x83 -x84 x85 -x86 x87 -x88 x89 -x90 x91 -x92 x93 -x94 x95 -x96 x97 -x98 x99 -x100 x101 -x102 x103 -x104 x105 -x106 x107 -x108 x109 -x110 -x111 x112 x113 -x114 -x115 x116 x117 -x118 x119 -x120 x121 -x122 x123 -x124 x125 -x126 -x127 x128 x129 -x130 x131 -x132 x133 -x134 x135 -x136 x137 -x138 x139 -x140 x141 -x142 x143 -x144 x145 -x146 x147 -x148 x149 -x150 -x151 x152 x153 -x154 x155 -x156 x157 -x158 x159 -x160 x161 -x162 x163 -x164 x165 -x166 x167 -x168 x169 -x170 x171 -x172 x173 -x174 x175 -x176 x177 -x178 x179 -x180 x181 -x182 -x183 x184 x185 -x186 x187 -x188 x189 -x190 x191 -x192 x193 -x194 x195 -x196 x197 -x198 x199 -x200 x201 -x202 -x203 x204 x205 -x206 x207 -x208 x209 -x210 x211 -x212 x213 -x214 x215 -x216 x217 -x218 -x219 x220 x221 -x222 x223 -x224 x225 -x226 x227 -x228 x229 -x230 x231 -x232 x233 -x234 x235 -x236 x237 -x238 x239 -x240 x241 -x242 x243 -x244 x245 -x246 -x247 x248 x249 -x250 x251 -x252 x253 -x254 x255 -x256 x257 -x258 x259 -x260 x261 -x262 x263 -x264 x265 -x266 x267 -x268 x269 -x270 x271 -x272 x273 -x274 x275 -x276 x277 -x278 -x279 x280 x281 -x282 x283 -x284 x285 -x286 x287 -x288 x289 -x290 x291 -x292 x293 -x294 x295 -x296 x297 -x298 x299 -x300 x301 -x302 -x303 x304 x305 -x306 -x307 x308 x309 -x310 x311 -x312 x313 -x314 x315 -x316 x317 -x318 -x319 x320 -x321 x322 -x323 x324 -x325 x326 x327 -x328 -x329 x330 -x331 x332 -x333 -x334 -x335 x336 -x337 x338 -x339 -x340 -x341 -x342 -x343 -x344 -x345 x346 -x347 x348 -x349 -x350 x351 -x352 -x353 x354 -x355 -x356 -x357 -x358 -x359 x360 x361 -x362 -x363 -x364 -x365 x366 -x367 x368 -x369 -x370 -x371 -x372 -x373 x374 -x375 -x376 -x377 -x378 -x379 x380 -x381 x382 -x383 x384 -x385 x386 -x387 x388 -x389 x390 -x391 x392 x393 -x394 -x395 x396 -x397 x398 -x399 x400 -x401 -x402 -x403 -x404 -x405 x406 -x407 x408 -x409 -x410 -x411 -x412 -x413 x414 -x415 -x416 x417 -x418 -x419 x420 x421 -x422 -x423 -x424 -x425 x426 -x427 x428 -x429 -x430 -x431 -x432 -x433 x434 -x435 -x436 -x437 -x438 -x439 x440 -x441 x442 -x443 x444 -x445 -x446 -x447 -x448 -x449 x450 -x451 x452 -x453 x454 -x455 x456 -x457 x458 x459 -x460 -x461 -x462 -x463 -x464 x465 -x466 -x467 x468 -x469 -x470 -x471 -x472 -x473 x474 -x475 -x476 -x477 -x478 -x479 x480 -x481 x482 -x483 x484 x485 -x486 -x487 x488 -x489 x490 -x491 x492 -x493 x494 -x495 x496 -x497 x498 -x499 x500 -x501 x502 -x503 x504 x505 -x506 -x507 -x508 -x509 x510 -x511 x512 -x513 x514 -x515 x516 -x517 x518 -x519 -x520 -x521 x522 -x523 x524 x525 -x526 -x527 x528 -x529 x530 -x531 x532 -x533 x534 -x535 x536 -x537 x538 -x539 x540 -x541 -x542 -x543 -x544 -x545 x546 -x547 x548 -x549 -x550 -x551 -x552 -x553 x554 x555 -x556 -x557 x558 -x559 x560 -x561 -x562 -x563 -x564 -x565 x566 -x567 -x568 x569 -x570 -x571 -x572 -x573 x574 -x575 -x576 -x577 -x578 -x579 -x580 -x581 -x582 -x583 -x584 -x585 x586 -x587 x588 -x589 -x590 -x591 -x592 -x593 x594 x595 -x596 -x597 -x598 -x599 x600 -x601 -x602 -x603 -x604 -x605 -x606 -x607 x608 -x609 x610 -x611 -x612 -x613 x614 -x615 -x616 x617 -x618 -x619 x620 -x621 -x622 -x623 -x624 -x625 -x626 -x627 -x628 -x629 -x630 -x631 -x632 -x633 -x634 -x635 -x636 x637 -x638 -x639 -x640 -x641 -x642 -x643 -x644 -x645 -x646 -x647 x648 -x649 -x650 -x651 -x652 -x653 -x654 -x655 -x656 x657 -x658 -x659 x660 -x661 x662 -x663 x664 -x665 -x666 -x667 x668 -x669 x670 -x671 x672 x673 -x674 -x675 x676 -x677 x678 -x679 x680 -x681 x682 -x683 x684 -x685 x686 -x687 x688 -x689 x690 -x691 x692 x693 -x694 -x695 x696 -x697 x698 -x699 x700 -x701 x702 -x703 x704 -x705 -x706 x707 -x708 -x709 x710 -x711 x712 -x713 x714 -x715 x716 -x717 x718 -x719 -x720 -x721 x722 -x723 x724 x725 -x726 -x727 x728 -x729 x730 -x731 x732 -x733 x734 -x735 x736 -x737 x738 -x739 x740 -x741 -x742 -x743 -x744 -x745 -x746 -x747 x748 -x749 -x750 -x751 -x752 -x753 x754 -x755 -x756 x757 -x758 -x759 x760 -x761 x762 -x763 x764 -x765 x766 -x767 x768 -x769 x770 -x771 x772 x773 -x774 -x775 x776 -x777 x778 -x779 x780 -x781 -x782 -x783 -x784 x785 -x786 -x787 -x788 -x789 -x790 -x791 -x792 -x793 x794 -x795 -x796 -x797 -x798 -x799 -x800 -x801 -x802 -x803 -x804 -x805 -x806 -x807 x808 -x809 -x810 -x811 -x812 -x813 x814 x815 -x816 -x817 -x818 -x819 x820 -x821 x822 -x823 x824 x825 -x826 -x827 x828 -x829 x830 -x831 x832 -x833 x834 -x835 x836 -x837 x838 -x839 x840 -x841 -x842 -x843 -x844 x845 -x846 -x847 x848 -x849 -x850 -x851 -x852 -x853 -x854 -x855 -x856 -x857 -x858 -x859 x860 -x861 x862 -x863 x864 x865 -x866 -x867 x868 -x869 x870 -x871 x872 -x873 x874 -x875 x876 -x877 x878 -x879 x880 -x881 x882 -x883 x884 x885 -x886 -x887 x888 -x889 x890 -x891 x892 -x893 x894 -x895 x896 -x897 x898 -x899 x900 -x901 -x902 -x903 -x904 -x905 x906 -x907 -x908 x909 -x910 -x911 -x912 -x913 x914 -x915 -x916 -x917 -x918 -x919 -x920 -x921 -x922 -x923 -x924 -x925 -x926 -x927 x928 -x929 -x930 -x931 -x932 -x933 x934 x935 -x936 -x937 -x938 -x939 x940 -x941 -x942 x943 -x944 -x945 x946 -x947 x948 -x949 -x950 -x951 -x952 -x953 x954 -x955 -x956 -x957 -x958 -x959 x960 -x961 x962 -x963 x964 -x965 -x966 x967 -x968 -x969 x970 -x971 x972 -x973 x974 -x975 x976 -x977 x978 -x979 -x980 x981 -x982 -x983 -x984 -x985 -x986 -x987 x988 -x989 -x990 -x991 -x992 -x993 -x994 -x995 -x996 -x997 -x998 -x999 x1000 -x1001 -x1002 -x1003 -x1004 -x1005 -x1006 -x1007 x1008 -x1009 -x1010 x1011 -x1012 -x1013 x1014 -x1015 -x1016 -x1017 -x1018 -x1019 x1020 x1021 -x1022 -x1023 -x1024 -x1025 -x1026 -x1027 x1028 -x1029 -x1030 -x1031 -x1032 -x1033 -x1034 -x1035 -x1036 -x1037 -x1038 -x1039 x1040 -x1041 -x1042 -x1043 -x1044 -x1045 -x1046 -x1047 x1048 -x1049 -x1050 -x1051 -x1052 -x1053 x1054 -x1055 -x1056 x1057 -x1058 -x1059 x1060 -x1061 -x1062 -x1063 -x1064 -x1065 -x1066 -x1067 x1068 x1069 -x1070 -x1071 -x1072 -x1073 x1074 -x1075 -x1076 -x1077 -x1078 -x1079 x1080 -x1081 -x1082 -x1083 -x1084 -x1085 x1086 -x1087 x1088 -x1089 x1090 x1091 -x1092 -x1093 x1094 -x1095 -x1096 -x1097 -x1098 -x1099 x1100 -x1101 -x1102 -x1103 -x1104 -x1105 x1106 -x1107 x1108 -x1109 x1110 -x1111 x1112 x1113 -x1114 -x1115 -x1116 -x1117 -x1118 -x1119 x1120 -x1121 -x1122 -x1123 -x1124 -x1125 x1126 -x1127 x1128 x1129 -x1130 -x1131 -x1132 -x1133 x1134 -x1135 -x1136 -x1137 -x1138 -x1139 x1140 -x1141 x1142 -x1143 x1144 x1145 -x1146 -x1147 x1148 -x1149 x1150 -x1151 x1152 -x1153 x1154 -x1155 x1156 -x1157 x1158 -x1159 x1160 x1161 -x1162 -x1163 -x1164 -x1165 x1166 -x1167 x1168 -x1169 -x1170 -x1171 -x1172 -x1173 -x1174 -x1175 -x1176 -x1177 -x1178 -x1179 x1180 -x1181 x1182 -x1183 x1184 -x1185 x1186 -x1187 x1188 -x1189 x1190 -x1191 x1192 x1193 -x1194 -x1195 x1196 -x1197 x1198 -x1199 x1200 -x1201 -x1202 -x1203 -x1204 x1205 -x1206 -x1207 x1208 -x1209 -x1210 -x1211 -x1212 -x1213 x1214 -x1215 -x1216 -x1217 -x1218 -x1219 x1220 x1221 -x1222 -x1223 -x1224 -x1225 x1226 -x1227 x1228 -x1229 -x1230 -x1231 -x1232 -x1233 x1234 -x1235 -x1236 -x1237 -x1238 -x1239 x1240 -x1241 -x1242 -x1243 -x1244 x1245 -x1246 -x1247 x1248 -x1249 -x1250 -x1251 -x1252 -x1253 x1254 -x1255 -x1256 -x1257 -x1258 -x1259 x1260 -x1261 x1262 -x1263 x1264 x1265 -x1266 -x1267 x1268 -x1269 x1270 -x1271 x1272 -x1273 x1274 -x1275 x1276 -x1277 x1278 -x1279 x1280 -x1281 -x1282 x1283 -x1284 -x1285 x1286 -x1287 x1288 -x1289 -x1290 -x1291 x1292 -x1293 -x1294 -x1295 -x1296 -x1297 -x1298 -x1299 x1300 -x1301 x1302 -x1303 x1304 x1305 -x1306 -x1307 -x1308 -x1309 x1310 -x1311 x1312 -x1313 -x1314 -x1315 x1316 -x1317 x1318 -x1319 -x1320 -x1321 -x1322 -x1323 -x1324 -x1325 x1326 -x1327 -x1328 -x1329 -x1330 -x1331 -x1332 -x1333 x1334 -x1335 -x1336 x1337 -x1338 -x1339 -x1340 -x1341 -x1342 -x1343 -x1344 -x1345 x1346 -x1347 x1348 -x1349 -x1350 -x1351 -x1352 -x1353 x1354 x1355 -x1356 -x1357 -x1358 -x1359 x1360 -x1361 -x1362 -x1363 -x1364 -x1365 x1366 -x1367 x1368 -x1369 -x1370 -x1371 -x1372 -x1373 -x1374 -x1375 -x1376 x1377 -x1378 -x1379 x1380 -x1381 -x1382 -x1383 -x1384 -x1385 x1386 -x1387 x1388 -x1389 -x1390 -x1391 -#### 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.92 0.98 0.92 2/54 13251 Raw data (stat): 13251 (runsolver) R 13250 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423345975 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0004 s] Raw data (loadavg): 0.93 0.98 0.92 2/54 13251 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 7883 0 0 0 976 22 0 0 25 0 1 0 423345975 36704256 7628 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8961 7628 603 41 0 8920 0 vsize: 35844 [startup+20.0014 s] Raw data (loadavg): 0.94 0.98 0.92 2/54 13251 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 7897 0 0 0 1975 22 0 0 25 0 1 0 423345975 36704256 7642 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8961 7642 603 41 0 8920 0 vsize: 35844 [startup+30.0015 s] Raw data (loadavg): 0.95 0.98 0.92 2/54 13251 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 7899 0 0 0 2975 22 0 0 25 0 1 0 423345975 36704256 7644 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8961 7644 603 41 0 8920 0 vsize: 35844 [startup+40.0018 s] Raw data (loadavg): 0.96 0.98 0.92 2/54 13251 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 7910 0 0 0 3975 22 0 0 25 0 1 0 423345975 36835328 7655 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8993 7655 603 41 0 8952 0 vsize: 35972 [startup+50.0026 s] Raw data (loadavg): 0.96 0.98 0.92 2/54 13251 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 7914 0 0 0 4975 22 0 0 25 0 1 0 423345975 36835328 7659 4294967295 134512640 134672761 3221224576 3221223700 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8993 7659 603 41 0 8952 0 vsize: 35972 [startup+60.0031 s] Raw data (loadavg): 0.97 0.98 0.92 2/54 13251 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 7941 0 0 0 5975 22 0 0 25 0 1 0 423345975 36970496 7686 4294967295 134512640 134672761 3221224576 3221223748 134556649 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9026 7686 603 41 0 8985 0 vsize: 36104 [startup+70.0038 s] Raw data (loadavg): 0.97 0.98 0.92 2/54 13251 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 7941 0 0 0 6974 23 0 0 25 0 1 0 423345975 36970496 7686 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9026 7686 603 41 0 8985 0 vsize: 36104 [startup+80.0052 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 13251 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 7950 0 0 0 7974 23 0 0 25 0 1 0 423345975 36970496 7695 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9026 7695 603 41 0 8985 0 vsize: 36104 [startup+90.0046 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 7952 0 0 0 8974 23 0 0 25 0 1 0 423345975 36970496 7697 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9026 7697 603 41 0 8985 0 vsize: 36104 [startup+100.005 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 7963 0 0 0 9974 23 0 0 25 0 1 0 423345975 36970496 7708 4294967295 134512640 134672761 3221224576 3221223748 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9026 7708 603 41 0 8985 0 vsize: 36104 [startup+110.006 s] Raw data (loadavg): 0.98 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8004 0 0 0 10974 23 0 0 25 0 1 0 423345975 37269504 7749 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9099 7749 603 41 0 9058 0 vsize: 36396 [startup+120.005 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8018 0 0 0 11974 23 0 0 25 0 1 0 423345975 37269504 7763 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9099 7763 603 41 0 9058 0 vsize: 36396 [startup+130.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8047 0 0 0 12974 23 0 0 25 0 1 0 423345975 37466112 7792 4294967295 134512640 134672761 3221224576 3221223776 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9147 7792 603 41 0 9106 0 vsize: 36588 [startup+140.006 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8065 0 0 0 13974 23 0 0 25 0 1 0 423345975 37466112 7810 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9147 7810 603 41 0 9106 0 vsize: 36588 [startup+150.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8104 0 0 0 14975 23 0 0 25 0 1 0 423345975 37601280 7849 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9180 7849 603 41 0 9139 0 vsize: 36720 [startup+160.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8181 0 0 0 15974 24 0 0 25 0 1 0 423345975 38014976 7926 4294967295 134512640 134672761 3221224576 3221223712 134560619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9281 7927 603 41 0 9240 0 vsize: 37124 [startup+170.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8454 0 0 0 16974 25 0 0 25 0 1 0 423345975 39534592 8199 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9652 8199 603 41 0 9611 0 vsize: 38608 [startup+180.007 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8522 0 0 0 17973 25 0 0 25 0 1 0 423345975 39804928 8267 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9718 8267 603 41 0 9677 0 vsize: 38872 [startup+190.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8579 0 0 0 18974 25 0 0 25 0 1 0 423345975 40075264 8324 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9784 8324 603 41 0 9743 0 vsize: 39136 [startup+200.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8674 0 0 0 19973 25 0 0 25 0 1 0 423345975 40476672 8419 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9882 8419 603 41 0 9841 0 vsize: 39528 [startup+210.008 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8760 0 0 0 20973 26 0 0 25 0 1 0 423345975 40873984 8505 4294967295 134512640 134672761 3221224576 3221223744 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9979 8505 603 41 0 9938 0 vsize: 39916 [startup+220.066 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8860 0 0 0 21978 26 0 0 25 0 1 0 423345975 41275392 8605 4294967295 134512640 134672761 3221224576 3221223700 134566100 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10077 8605 603 41 0 10036 0 vsize: 40308 [startup+230.066 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 8967 0 0 0 22978 27 0 0 25 0 1 0 423345975 41680896 8712 4294967295 134512640 134672761 3221224576 3221223712 134560590 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10176 8712 603 41 0 10135 0 vsize: 40704 [startup+240.065 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 9093 0 0 0 23978 27 0 0 25 0 1 0 423345975 42217472 8838 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10307 8838 603 41 0 10266 0 vsize: 41228 [startup+250.065 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 9190 0 0 0 24978 27 0 0 25 0 1 0 423345975 42622976 8935 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10406 8935 603 41 0 10365 0 vsize: 41624 [startup+260.065 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 9287 0 0 0 25978 28 0 0 25 0 1 0 423345975 43028480 9032 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10505 9032 603 41 0 10464 0 vsize: 42020 [startup+270.065 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 9395 0 0 0 26978 28 0 0 25 0 1 0 423345975 43429888 9140 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10603 9140 603 41 0 10562 0 vsize: 42412 [startup+280.065 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 9514 0 0 0 27978 28 0 0 25 0 1 0 423345975 43839488 9259 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10703 9259 603 41 0 10662 0 vsize: 42812 [startup+290.065 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 9770 0 0 0 28978 28 0 0 25 0 1 0 423345975 44896256 9515 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10961 9515 603 41 0 10920 0 vsize: 43844 [startup+300.066 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 9986 0 0 0 29977 29 0 0 25 0 1 0 423345975 45842432 9731 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11192 9731 603 41 0 11151 0 vsize: 44768 [startup+310.066 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 10403 0 0 0 30977 30 0 0 25 0 1 0 423345975 47460352 10148 4294967295 134512640 134672761 3221224576 3221223680 134554910 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11587 10148 603 41 0 11546 0 vsize: 46348 [startup+320.066 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 10912 0 0 0 31975 31 0 0 25 0 1 0 423345975 49635328 10657 4294967295 134512640 134672761 3221224576 3221223724 134560552 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12118 10657 603 41 0 12077 0 vsize: 48472 [startup+330.066 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 11171 0 0 0 32975 31 0 0 25 0 1 0 423345975 50843648 10916 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12413 10916 603 41 0 12372 0 vsize: 49652 [startup+340.066 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 11300 0 0 0 33975 32 0 0 25 0 1 0 423345975 51384320 11045 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12545 11045 603 41 0 12504 0 vsize: 50180 [startup+350.066 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 11445 0 0 0 34974 32 0 0 25 0 1 0 423345975 51908608 11155 4294967295 134512640 134672761 3221224576 3221223728 134561035 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12673 11155 603 41 0 12632 0 vsize: 50692 [startup+360.067 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 11561 0 0 0 35974 33 0 0 25 0 1 0 423345975 52314112 11271 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12772 11271 603 41 0 12731 0 vsize: 51088 [startup+370.067 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 11693 0 0 0 36973 34 0 0 25 0 1 0 423345975 52854784 11403 4294967295 134512640 134672761 3221224576 3221223744 134561269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12904 11403 603 41 0 12863 0 vsize: 51616 [startup+380.068 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 11969 0 0 0 37973 34 0 0 25 0 1 0 423345975 53940224 11679 4294967295 134512640 134672761 3221224576 3221223744 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13169 11679 603 41 0 13128 0 vsize: 52676 [startup+390.068 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12079 0 0 0 38973 35 0 0 25 0 1 0 423345975 54341632 11789 4294967295 134512640 134672761 3221224576 3221223744 134561161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13267 11789 603 41 0 13226 0 vsize: 53068 [startup+400.068 s] Raw data (loadavg): 0.99 0.98 0.92 3/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12245 0 0 0 39973 35 0 0 25 0 1 0 423345975 54870016 11919 4294967295 134512640 134672761 3221224576 3221223680 134560148 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13396 11919 603 41 0 13355 0 vsize: 53584 [startup+410.068 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12342 0 0 0 40973 35 0 0 25 0 1 0 423345975 55107584 11983 4294967295 134512640 134672761 3221224576 3221223744 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11983 603 41 0 13413 0 vsize: 53816 [startup+420.068 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12342 0 0 0 41973 35 0 0 25 0 1 0 423345975 55107584 11983 4294967295 134512640 134672761 3221224576 3221223744 134561264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11983 603 41 0 13413 0 vsize: 53816 [startup+430.069 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12342 0 0 0 42973 35 0 0 25 0 1 0 423345975 55107584 11983 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11983 603 41 0 13413 0 vsize: 53816 [startup+440.069 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12342 0 0 0 43973 35 0 0 25 0 1 0 423345975 55107584 11983 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11983 603 41 0 13413 0 vsize: 53816 [startup+450.07 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12342 0 0 0 44973 35 0 0 25 0 1 0 423345975 55107584 11983 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11983 603 41 0 13413 0 vsize: 53816 [startup+460.069 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12342 0 0 0 45974 35 0 0 25 0 1 0 423345975 55107584 11983 4294967295 134512640 134672761 3221224576 3221223840 134562662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11983 603 41 0 13413 0 vsize: 53816 [startup+470.145 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12342 0 0 0 46981 35 0 0 25 0 1 0 423345975 55107584 11983 4294967295 134512640 134672761 3221224576 3221223744 134561378 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11983 603 41 0 13413 0 vsize: 53816 [startup+480.146 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12342 0 0 0 47982 35 0 0 25 0 1 0 423345975 55107584 11983 4294967295 134512640 134672761 3221224576 3221223712 134560598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11983 603 41 0 13413 0 vsize: 53816 [startup+490.146 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12342 0 0 0 48982 35 0 0 25 0 1 0 423345975 55107584 11983 4294967295 134512640 134672761 3221224576 3221223744 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11983 603 41 0 13413 0 vsize: 53816 [startup+500.147 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 49982 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223712 134560716 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+510.147 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 50982 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+520.146 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 51982 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+530.147 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 52982 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+540.147 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 53982 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+550.148 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 54983 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+560.148 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 55983 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+570.148 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 56983 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+580.148 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 57983 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+590.149 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 58983 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223680 134559927 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+600.149 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 59984 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+610.15 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 60984 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223680 134560399 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+620.15 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 61984 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223700 134566071 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+630.151 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12343 0 0 0 62984 35 0 0 25 0 1 0 423345975 55107584 11984 4294967295 134512640 134672761 3221224576 3221223744 134560867 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13454 11984 603 41 0 13413 0 vsize: 53816 [startup+640.152 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12417 0 0 0 63984 35 0 0 25 0 1 0 423345975 55500800 12058 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13550 12058 603 41 0 13509 0 vsize: 54200 [startup+650.152 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12606 0 0 0 64984 36 0 0 25 0 1 0 423345975 56299520 12247 4294967295 134512640 134672761 3221224576 3221223712 134560604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13745 12247 603 41 0 13704 0 vsize: 54980 [startup+660.152 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12750 0 0 0 65984 36 0 0 25 0 1 0 423345975 56836096 12391 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13876 12391 603 41 0 13835 0 vsize: 55504 [startup+670.151 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 12867 0 0 0 66984 37 0 0 25 0 1 0 423345975 57241600 12508 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13975 12508 603 41 0 13934 0 vsize: 55900 [startup+680.152 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13099 0 0 0 67984 37 0 0 25 0 1 0 423345975 58163200 12738 4294967295 134512640 134672761 3221224576 3221223744 134560828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12738 603 41 0 14159 0 vsize: 56800 [startup+690.152 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13099 0 0 0 68984 37 0 0 25 0 1 0 423345975 58163200 12738 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12738 603 41 0 14159 0 vsize: 56800 [startup+700.153 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13099 0 0 0 69984 37 0 0 25 0 1 0 423345975 58163200 12738 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12738 603 41 0 14159 0 vsize: 56800 [startup+710.153 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13101 0 0 0 70984 37 0 0 25 0 1 0 423345975 58163200 12740 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12740 603 41 0 14159 0 vsize: 56800 [startup+720.153 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13101 0 0 0 71984 37 0 0 25 0 1 0 423345975 58163200 12740 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12740 603 41 0 14159 0 vsize: 56800 [startup+730.154 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13101 0 0 0 72985 37 0 0 25 0 1 0 423345975 58163200 12740 4294967295 134512640 134672761 3221224576 3221223680 134559866 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12740 603 41 0 14159 0 vsize: 56800 [startup+740.153 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13101 0 0 0 73985 37 0 0 25 0 1 0 423345975 58163200 12740 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12740 603 41 0 14159 0 vsize: 56800 [startup+750.154 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13101 0 0 0 74985 37 0 0 25 0 1 0 423345975 58163200 12740 4294967295 134512640 134672761 3221224576 3221223712 134560557 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12740 603 41 0 14159 0 vsize: 56800 [startup+760.154 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13101 0 0 0 75985 37 0 0 25 0 1 0 423345975 58163200 12740 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12740 603 41 0 14159 0 vsize: 56800 [startup+770.154 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 76985 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223680 134559835 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+780.154 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 77986 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+790.155 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 78986 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223680 134559883 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+800.155 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 79986 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223712 134565089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+810.156 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 80986 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+820.156 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 81986 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+830.156 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 82986 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223724 134559754 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+840.156 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 83987 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+850.157 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 84987 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+860.157 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 85987 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223744 134560797 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+870.156 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 86987 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+880.157 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 87987 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+890.157 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 88987 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+900.158 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 89988 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223724 134560631 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+910.158 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 90988 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223776 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+920.157 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13102 0 0 0 91988 37 0 0 25 0 1 0 423345975 58163200 12741 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14200 12741 603 41 0 14159 0 vsize: 56800 [startup+930.157 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13173 0 0 0 92988 37 0 0 25 0 1 0 423345975 58572800 12812 4294967295 134512640 134672761 3221224576 3221223712 134560709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14300 12812 603 41 0 14259 0 vsize: 57200 [startup+940.157 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13510 0 0 0 93987 38 0 0 25 0 1 0 423345975 59916288 13149 4294967295 134512640 134672761 3221224576 3221223680 134560326 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14628 13149 603 41 0 14587 0 vsize: 58512 [startup+950.158 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13690 0 0 0 94987 38 0 0 25 0 1 0 423345975 60583936 13329 4294967295 134512640 134672761 3221224576 3221223776 134557852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14791 13329 603 41 0 14750 0 vsize: 59164 [startup+960.158 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 13854 0 0 0 95987 39 0 0 25 0 1 0 423345975 61345792 13493 4294967295 134512640 134672761 3221224576 3221223680 134560191 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14977 13493 603 41 0 14936 0 vsize: 59908 [startup+970.158 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 14067 0 0 0 96986 40 0 0 25 0 1 0 423345975 62128128 13706 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15168 13706 603 41 0 15127 0 vsize: 60672 [startup+980.159 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 14321 0 0 0 97986 40 0 0 25 0 1 0 423345975 63295488 13960 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15453 13960 603 41 0 15412 0 vsize: 61812 [startup+990.159 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 14515 0 0 0 98985 41 0 0 25 0 1 0 423345975 64081920 14154 4294967295 134512640 134672761 3221224576 3221223680 134560379 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15645 14154 603 41 0 15604 0 vsize: 62580 [startup+1000.16 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 14685 0 0 0 99985 41 0 0 25 0 1 0 423345975 64733184 14324 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15804 14324 603 41 0 15763 0 vsize: 63216 [startup+1010.16 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 14815 0 0 0 100985 42 0 0 25 0 1 0 423345975 65261568 14454 4294967295 134512640 134672761 3221224576 3221223776 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15933 14454 603 41 0 15892 0 vsize: 63732 [startup+1020.16 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 15009 0 0 0 101985 42 0 0 25 0 1 0 423345975 66027520 14648 4294967295 134512640 134672761 3221224576 3221223680 134560025 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16120 14648 603 41 0 16079 0 vsize: 64480 [startup+1030.16 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 15282 0 0 0 102984 43 0 0 25 0 1 0 423345975 67231744 14921 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16414 14921 603 41 0 16373 0 vsize: 65656 [startup+1040.16 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 15581 0 0 0 103983 44 0 0 25 0 1 0 423345975 68440064 15220 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16709 15220 603 41 0 16668 0 vsize: 66836 [startup+1050.16 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 15808 0 0 0 104983 44 0 0 25 0 1 0 423345975 69369856 15447 4294967295 134512640 134672761 3221224576 3221223680 134560229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16936 15447 603 41 0 16895 0 vsize: 67744 [startup+1060.16 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 16014 0 0 0 105982 45 0 0 25 0 1 0 423345975 70148096 15653 4294967295 134512640 134672761 3221224576 3221223744 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17126 15653 603 41 0 17085 0 vsize: 68504 [startup+1070.17 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 16278 0 0 0 106983 46 0 0 25 0 1 0 423345975 71303168 15917 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17408 15917 603 41 0 17367 0 vsize: 69632 [startup+1080.17 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 16495 0 0 0 107982 46 0 0 25 0 1 0 423345975 72110080 16134 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17605 16134 603 41 0 17564 0 vsize: 70420 [startup+1090.17 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 16856 0 0 0 108982 47 0 0 25 0 1 0 423345975 73576448 16495 4294967295 134512640 134672761 3221224576 3221223576 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17963 16495 603 41 0 17922 0 vsize: 71852 [startup+1100.17 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 17004 0 0 0 109981 47 0 0 25 0 1 0 423345975 74248192 16643 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18127 16643 603 41 0 18086 0 vsize: 72508 [startup+1110.17 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 17107 0 0 0 110981 48 0 0 25 0 1 0 423345975 74653696 16746 4294967295 134512640 134672761 3221224576 3221223740 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18226 16746 603 41 0 18185 0 vsize: 72904 [startup+1120.17 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 17250 0 0 0 111981 48 0 0 25 0 1 0 423345975 75190272 16889 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18357 16889 603 41 0 18316 0 vsize: 73428 [startup+1130.17 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 17402 0 0 0 112981 48 0 0 25 0 1 0 423345975 75853824 17041 4294967295 134512640 134672761 3221224576 3221223680 134560054 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18519 17041 603 41 0 18478 0 vsize: 74076 [startup+1140.17 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 17766 0 0 0 113980 49 0 0 25 0 1 0 423345975 77320192 17405 4294967295 134512640 134672761 3221224576 3221223744 134561278 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18877 17405 603 41 0 18836 0 vsize: 75508 [startup+1150.21 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 18147 0 0 0 114984 50 0 0 25 0 1 0 423345975 78917632 17786 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19267 17786 603 41 0 19226 0 vsize: 77068 [startup+1160.34 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 18560 0 0 0 115996 51 0 0 25 0 1 0 423345975 80527360 18199 4294967295 134512640 134672761 3221224576 3221223680 134560248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19660 18199 603 41 0 19619 0 vsize: 78640 [startup+1170.34 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 18851 0 0 0 116996 51 0 0 25 0 1 0 423345975 81735680 18490 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19955 18490 603 41 0 19914 0 vsize: 79820 [startup+1180.34 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 18954 0 0 0 117996 52 0 0 25 0 1 0 423345975 82137088 18593 4294967295 134512640 134672761 3221224576 3221223712 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20053 18593 603 41 0 20012 0 vsize: 80212 [startup+1190.34 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 19126 0 0 0 118995 52 0 0 25 0 1 0 423345975 82948096 18765 4294967295 134512640 134672761 3221224576 3221223744 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20251 18765 603 41 0 20210 0 vsize: 81004 [startup+1200.34 s] Raw data (loadavg): 0.99 0.98 0.92 2/54 13253 Raw data (stat): 13251 (minisat+) R 13250 5897 5896 0 -1 0 19433 0 0 0 119995 53 0 0 25 0 1 0 423345975 84135936 19072 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20541 19072 603 41 0 20500 0 vsize: 82164 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.38 s] Raw data (loadavg): 0.99 0.98 0.92 1/54 13253 Raw data (stat): 13251 (minisat+) Z 13250 5897 5896 0 -1 12 19436 0 0 0 119995 56 0 0 25 0 1 0 423345975 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.38 CPU time (s): 1200.53 CPU user time (s): 1199.96 CPU system time (s): 0.569913 CPU usage (%): 100.012 Max. virtual memory (Kb): 82164 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####