Name | normalized-opb/submitted/manquinho/primes-dimacs-cnf/normalized-ii8e1.opb |
MD5SUM | 979ebd144bbd2b562b23479b90a02c66 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 343 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 1040 |
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 | 1040 |
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 | 1040 |
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.03484 |
Number of variables | 1040 |
Total number of constraints | 3656 |
Number of constraints which are clauses | 3656 |
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 wulflinc5 THE 2005-04-14 04:05:41 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4687 boxname=wulflinc5 idbench=175 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 979ebd144bbd2b562b23479b90a02c66 /oldhome/oroussel/tmp/wulflinc5/normalized-ii8e1.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc5/normalized-ii8e1.opb /oldhome/oroussel/tmp/wulflinc5/normalized-ii8e1.opb IDLAUNCH: 4687 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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: 894324 kB Buffers: 35000 kB Cached: 83700 kB SwapCached: 2272 kB Active: 56084 kB Inactive: 67740 kB HighTotal: 131008 kB HighFree: 43400 kB LowTotal: 903652 kB LowFree: 850924 kB SwapTotal: 2097136 kB SwapFree: 2094864 kB Dirty: 32 kB Writeback: 0 kB Mapped: 6924 kB Slab: 10856 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 04:25:43 (client local time) WITH STATUS 10 IN 1200.2 SECONDS stats: 4687 7 1200.2 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 3656 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 | 3656 8440 | 1218 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 474[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:56938 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16 | 138118 322824 | 46039 16 122 7.6 | 0.000 % | c | 116 | 138079 322737 | 50642 115 1410 12.3 | 0.046 % | c | 266 | 133895 313079 | 55707 184 2165 11.8 | 2.794 % | c | 491 | 124439 291410 | 61277 291 3481 12.0 | 9.032 % | c | 828 | 116589 273300 | 67405 520 7496 14.4 | 14.418 % | c ============================================================================== c [1mFound solution: 469[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 | 829 | 116881 274044 | 38960 521 7517 14.4 | 14.418 % | c ============================================================================== c [1mFound solution: 468[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 | 830 | 116631 273466 | 38877 522 7593 14.5 | 14.418 % | c | 930 | 113533 266320 | 42764 563 7971 14.2 | 16.683 % | c | 1080 | 112171 263179 | 47041 690 8624 12.5 | 17.619 % | c | 1306 | 111210 260962 | 51745 812 10816 13.3 | 18.280 % | c | 1643 | 98559 231679 | 56919 962 12725 13.2 | 26.971 % | c | 2149 | 84758 199759 | 62611 1201 16028 13.3 | 36.606 % | c | 2908 | 84758 199759 | 68872 1960 27759 14.2 | 36.606 % | c | 4048 | 72228 170741 | 75760 2889 39087 13.5 | 45.372 % | c ============================================================================== c [1mFound solution: 467[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 | 4797 | 69738 164992 | 23246 3561 47291 13.3 | 45.372 % | c | 4899 | 69135 163597 | 25570 3647 47649 13.1 | 47.561 % | c | 5050 | 68657 162483 | 28127 3783 49859 13.2 | 47.912 % | c | 5275 | 67987 160926 | 30940 3970 51269 12.9 | 48.389 % | c | 5612 | 67482 159758 | 34034 4292 55628 13.0 | 48.738 % | c | 6118 | 64471 152731 | 37437 4701 58689 12.5 | 50.897 % | c | 6878 | 63363 150150 | 41181 5395 68480 12.7 | 51.705 % | c | 8017 | 62813 148888 | 45299 6507 85328 13.1 | 52.062 % | c ============================================================================== c [1mFound solution: 453[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 | 9278 | 61858 146762 | 20619 7736 105352 13.6 | 52.062 % | c | 9378 | 60994 144752 | 22680 7774 106217 13.7 | 53.463 % | c | 9528 | 60800 144303 | 24948 7904 106963 13.5 | 53.583 % | c | 9754 | 60675 144015 | 27443 8122 109569 13.5 | 53.669 % | c ============================================================================== c [1mFound solution: 452[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 | 9802 | 60558 143738 | 20186 8170 110415 13.5 | 53.669 % | c | 9902 | 60200 142915 | 22204 8247 110759 13.4 | 53.987 % | c | 10052 | 60168 142843 | 24425 8397 111981 13.3 | 53.987 % | c ============================================================================== c [1mFound solution: 451[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 | 10230 | 60237 143025 | 20079 8575 115313 13.4 | 53.987 % | c | 10330 | 60237 143025 | 22086 8675 116025 13.4 | 53.970 % | c | 10481 | 59978 142425 | 24295 8814 117754 13.4 | 54.151 % | c | 10706 | 59805 142026 | 26725 9026 120080 13.3 | 54.267 % | c ============================================================================== c [1mFound solution: 450[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 | 11004 | 59751 141884 | 19917 9324 123062 13.2 | 54.267 % | c | 11105 | 59751 141884 | 21908 9425 123915 13.1 | 54.291 % | c | 11255 | 59630 141607 | 24099 9571 124724 13.0 | 54.367 % | c | 11480 | 59630 141607 | 26509 9796 128398 13.1 | 54.367 % | c | 11817 | 59630 141607 | 29160 10133 137246 13.5 | 54.367 % | c | 12323 | 58957 140045 | 32076 10609 141082 13.3 | 54.854 % | c | 13083 | 58826 139743 | 35284 11356 226155 19.9 | 54.943 % | c ============================================================================== c [1mFound solution: 449[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 | 13714 | 58948 140061 | 19649 11987 256436 21.4 | 54.943 % | c | 13814 | 58948 140061 | 21613 12087 257375 21.3 | 54.909 % | c | 13965 | 58948 140061 | 23775 12238 259216 21.2 | 54.909 % | c | 14191 | 58948 140061 | 26152 12464 262361 21.0 | 54.909 % | c | 14530 | 58948 140061 | 28768 12803 285919 22.3 | 54.909 % | c | 15036 | 58705 139495 | 31644 13263 289248 21.8 | 55.090 % | c | 15795 | 58705 139495 | 34809 14022 300153 21.4 | 55.090 % | c | 16934 | 58563 139168 | 38290 15157 323613 21.4 | 55.188 % | c ============================================================================== c [1mFound solution: 448[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 | 17398 | 58346 138651 | 19448 15483 319200 20.6 | 55.188 % | c | 17500 | 58346 138651 | 21392 15585 322368 20.7 | 55.332 % | c | 17651 | 58346 138651 | 23532 15736 323285 20.5 | 55.332 % | c | 17877 | 58346 138651 | 25885 15962 329729 20.7 | 55.332 % | c | 18214 | 58346 138651 | 28473 16299 335385 20.6 | 55.332 % | c | 18720 | 58229 138372 | 31321 16800 349342 20.8 | 55.430 % | c ============================================================================== c [1mFound solution: 444[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 | 19471 | 58214 138364 | 19404 17491 354933 20.3 | 55.430 % | c | 19571 | 58214 138364 | 21344 17591 356046 20.2 | 55.498 % | c | 19722 | 58214 138364 | 23478 17742 356857 20.1 | 55.498 % | c | 19947 | 58214 138364 | 25826 17967 361987 20.1 | 55.498 % | c | 20284 | 58214 138364 | 28409 18304 374970 20.5 | 55.498 % | c | 20790 | 58157 138234 | 31250 18809 382891 20.4 | 55.535 % | c | 21549 | 58157 138234 | 34375 19568 418496 21.4 | 55.535 % | c ============================================================================== c [1mFound solution: 443[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 | 22119 | 58226 138416 | 19408 20138 435739 21.6 | 55.535 % | c ============================================================================== c [1mFound solution: 442[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 | 22130 | 58163 138236 | 19387 20094 430738 21.4 | 55.535 % | c | 22231 | 58163 138236 | 21325 20195 432554 21.4 | 55.548 % | c | 22382 | 58015 137891 | 23458 20333 435793 21.4 | 55.659 % | c | 22608 | 57932 137696 | 25804 20549 440837 21.5 | 55.725 % | c | 22945 | 57663 137074 | 28384 20833 450653 21.6 | 55.914 % | c | 23451 | 57663 137074 | 31222 21339 461750 21.6 | 55.914 % | c | 24210 | 57663 137074 | 34345 22098 473155 21.4 | 55.914 % | c ============================================================================== c [1mFound solution: 441[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 | 24695 | 57561 136872 | 19187 21110 454695 21.5 | 55.914 % | c | 24795 | 57561 136872 | 21105 21210 455633 21.5 | 56.036 % | c | 24946 | 57561 136872 | 23216 21361 458254 21.5 | 56.036 % | c | 25173 | 57387 136468 | 25537 21535 460518 21.4 | 56.158 % | c | 25512 | 57387 136468 | 28091 21874 469149 21.4 | 56.158 % | c | 26020 | 57075 135740 | 30900 22281 476391 21.4 | 56.393 % | c | 26780 | 56885 135307 | 33990 22145 474538 21.4 | 56.512 % | c | 27919 | 56885 135307 | 37390 23284 511027 21.9 | 56.512 % | c | 29628 | 56885 135307 | 41129 24993 546404 21.9 | 56.512 % | c | 32190 | 56794 135094 | 45241 27532 637994 23.2 | 56.582 % | c ============================================================================== c [1mFound solution: 437[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 | 35757 | 56582 134637 | 18860 30955 734418 23.7 | 56.582 % | c | 35859 | 56582 134637 | 20746 31057 735052 23.7 | 56.810 % | c | 36009 | 56417 134255 | 22820 31140 736703 23.7 | 56.927 % | c | 36234 | 56386 134181 | 25102 31364 738214 23.5 | 56.951 % | c | 36574 | 56297 133977 | 27612 31702 740509 23.4 | 57.010 % | c | 37080 | 55693 132572 | 30374 32102 755607 23.5 | 57.442 % | c | 37839 | 55673 132526 | 33411 32859 772154 23.5 | 57.456 % | c | 38982 | 55510 132149 | 36752 33964 792781 23.3 | 57.571 % | c ============================================================================== c [1mFound solution: 436[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 | 39746 | 55401 131871 | 18467 34620 794634 23.0 | 57.571 % | c | 39846 | 55401 131871 | 20313 34720 796554 22.9 | 57.636 % | c | 39996 | 55401 131871 | 22345 34870 799145 22.9 | 57.636 % | c | 40222 | 55401 131871 | 24579 35096 802383 22.9 | 57.636 % | c ============================================================================== c [1mFound solution: 435[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 | 40546 | 55468 132047 | 18489 35420 813987 23.0 | 57.636 % | c | 40646 | 55468 132047 | 20337 35520 815654 23.0 | 57.617 % | c | 40797 | 55468 132047 | 22371 35671 817399 22.9 | 57.617 % | c | 41023 | 55468 132047 | 24608 35897 827821 23.1 | 57.617 % | c | 41360 | 55468 132047 | 27069 36234 844155 23.3 | 57.617 % | c | 41866 | 55373 131831 | 29776 36629 848352 23.2 | 57.676 % | c ============================================================================== c [1mFound solution: 433[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 | 42257 | 55484 132119 | 18494 37020 861101 23.3 | 57.676 % | c | 42357 | 55484 132119 | 20343 37120 864013 23.3 | 57.644 % | c | 42508 | 55395 131911 | 22377 37266 865668 23.2 | 57.707 % | c | 42734 | 55395 131911 | 24615 37492 871276 23.2 | 57.707 % | c | 43071 | 55395 131911 | 27077 37829 875627 23.1 | 57.707 % | c | 43577 | 55324 131751 | 29784 38334 886442 23.1 | 57.748 % | c | 44338 | 55324 131751 | 32763 39095 897769 23.0 | 57.748 % | c | 45477 | 55324 131751 | 36039 40234 933270 23.2 | 57.748 % | c | 47185 | 55324 131751 | 39643 41942 1039252 24.8 | 57.748 % | c ============================================================================== c [1mFound solution: 432[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 | 49495 | 55124 131236 | 18374 43765 1075694 24.6 | 57.748 % | c | 49595 | 55124 131236 | 20211 43865 1076889 24.6 | 57.885 % | c | 49745 | 55124 131236 | 22232 44015 1081882 24.6 | 57.885 % | c | 49972 | 55124 131236 | 24455 44242 1090656 24.7 | 57.885 % | c | 50310 | 55026 131010 | 26901 44572 1093389 24.5 | 57.952 % | c | 50817 | 55026 131010 | 29591 45079 1108118 24.6 | 57.952 % | c | 51576 | 55026 131010 | 32550 45838 1144412 25.0 | 57.952 % | c | 52715 | 55026 131010 | 35805 46977 1238694 26.4 | 57.952 % | c ============================================================================== c [1mFound solution: 431[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 | 53232 | 55093 131186 | 18364 47494 1257976 26.5 | 57.952 % | c | 53332 | 55093 131186 | 20200 19750 481110 24.4 | 57.934 % | c | 53482 | 55093 131186 | 22220 19900 484183 24.3 | 57.934 % | c | 53708 | 55093 131186 | 24442 20126 490160 24.4 | 57.934 % | c | 54045 | 55093 131186 | 26886 20463 495312 24.2 | 57.934 % | c | 54551 | 55093 131186 | 29575 20969 501778 23.9 | 57.934 % | c | 55310 | 55093 131186 | 32532 21728 536621 24.7 | 57.934 % | c | 56451 | 55093 131186 | 35786 22869 584333 25.6 | 57.934 % | c ============================================================================== c [1mFound solution: 430[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 | 56597 | 55007 130951 | 18335 22988 586792 25.5 | 57.934 % | c | 56698 | 55007 130951 | 20168 23089 587931 25.5 | 57.970 % | c | 56848 | 55007 130951 | 22185 23239 589140 25.4 | 57.970 % | c | 57074 | 55007 130951 | 24403 23465 591208 25.2 | 57.970 % | c | 57411 | 55007 130951 | 26844 23802 598971 25.2 | 57.970 % | c ============================================================================== c [1mFound solution: 429[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 | 57840 | 55109 131215 | 18369 24231 608920 25.1 | 57.970 % | c | 57940 | 55109 131215 | 20205 24331 613540 25.2 | 57.941 % | c | 58092 | 55109 131215 | 22226 24483 614832 25.1 | 57.941 % | c | 58317 | 55109 131215 | 24449 24708 622096 25.2 | 57.941 % | c | 58656 | 55109 131215 | 26894 25047 628009 25.1 | 57.941 % | c ============================================================================== c [1mFound solution: 425[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 | 58928 | 55190 131436 | 18396 25313 631982 25.0 | 57.941 % | c | 59028 | 55190 131436 | 20235 25413 632912 24.9 | 57.952 % | c | 59178 | 55182 131418 | 22259 25557 636437 24.9 | 57.957 % | c | 59403 | 55182 131418 | 24485 25782 644964 25.0 | 57.957 % | c | 59742 | 55182 131418 | 26933 26121 651379 24.9 | 57.957 % | c | 60249 | 55182 131418 | 29626 26628 665014 25.0 | 57.957 % | c | 61009 | 55156 131357 | 32589 27384 676971 24.7 | 57.976 % | c ============================================================================== c [1mFound solution: 423[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 | 61228 | 55223 131533 | 18407 27603 681518 24.7 | 57.976 % | c | 61328 | 55223 131533 | 20247 27703 684155 24.7 | 57.958 % | c | 61479 | 55223 131533 | 22272 27854 685215 24.6 | 57.958 % | c | 61704 | 55223 131533 | 24499 28079 688362 24.5 | 57.958 % | c | 62041 | 55032 131087 | 26949 28395 696931 24.5 | 58.101 % | c | 62547 | 55032 131087 | 29644 28901 707763 24.5 | 58.101 % | c | 63307 | 55032 131087 | 32609 29661 746615 25.2 | 58.101 % | c | 64446 | 55032 131087 | 35870 30800 767660 24.9 | 58.101 % | c ============================================================================== c [1mFound solution: 421[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 | 65351 | 55134 131351 | 18378 31705 826052 26.1 | 58.101 % | c | 65451 | 55134 131351 | 20215 31805 826960 26.0 | 58.071 % | c | 65601 | 54842 130670 | 22237 31262 821418 26.3 | 58.279 % | c | 65826 | 54842 130670 | 24461 31487 824071 26.2 | 58.279 % | c | 66163 | 54842 130670 | 26907 31824 832975 26.2 | 58.279 % | c | 66669 | 54842 130670 | 29597 32330 872796 27.0 | 58.279 % | c | 67428 | 54842 130670 | 32557 33089 883820 26.7 | 58.279 % | c | 68571 | 54525 129922 | 35813 34210 906539 26.5 | 58.498 % | c ============================================================================== c [1mFound solution: 399[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 | 69825 | 55067 131229 | 18355 35464 940261 26.5 | 58.498 % | c | 69928 | 55067 131229 | 20190 35567 941047 26.5 | 58.322 % | c | 70079 | 54903 130850 | 22209 35716 946628 26.5 | 58.436 % | c | 70304 | 54903 130850 | 24430 35941 963451 26.8 | 58.436 % | c | 70641 | 54903 130850 | 26873 36278 979008 27.0 | 58.436 % | c | 71147 | 54903 130850 | 29560 36784 998651 27.1 | 58.436 % | c ============================================================================== c [1mFound solution: 398[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 | 71808 | 54824 130639 | 18274 37433 1024116 27.4 | 58.436 % | c | 71908 | 54824 130639 | 20101 37533 1031145 27.5 | 58.470 % | c | 72058 | 54740 130442 | 22111 37628 1033603 27.5 | 58.530 % | c ============================================================================== c [1mFound solution: 397[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 | 72206 | 54836 130691 | 18278 37776 1037253 27.5 | 58.530 % | c | 72307 | 54779 130560 | 20105 37875 1039084 27.4 | 58.543 % | c | 72459 | 54639 130238 | 22116 37977 1042398 27.4 | 58.638 % | c | 72684 | 54453 129812 | 24328 38183 1046963 27.4 | 58.760 % | c | 73021 | 54453 129812 | 26760 38520 1053713 27.4 | 58.760 % | c | 73527 | 54391 129669 | 29436 38964 1072243 27.5 | 58.801 % | c | 74286 | 54391 129669 | 32380 39723 1121703 28.2 | 58.801 % | c | 75425 | 54391 129669 | 35618 40862 1145142 28.0 | 58.801 % | c | 77133 | 54387 129660 | 39180 42569 1205969 28.3 | 58.803 % | c | 79695 | 54387 129660 | 43098 45131 1465464 32.5 | 58.803 % | c | 83540 | 54303 129465 | 47408 48974 1612496 32.9 | 58.859 % | c | 89306 | 54167 129150 | 52149 54655 1870566 34.2 | 58.954 % | c ============================================================================== c [1mFound solution: 395[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 | 89567 | 54235 129327 | 18078 54916 1879160 34.2 | 58.954 % | c | 89667 | 54235 129327 | 19885 22064 690212 31.3 | 58.933 % | c | 89817 | 54235 129327 | 21874 22214 694376 31.3 | 58.933 % | c | 90043 | 53962 128691 | 24061 22433 697283 31.1 | 59.129 % | c | 90380 | 53962 128691 | 26467 22770 703174 30.9 | 59.129 % | c | 90887 | 53962 128691 | 29114 23277 723824 31.1 | 59.129 % | c | 91646 | 53962 128691 | 32026 24036 746277 31.0 | 59.129 % | c | 92785 | 53962 128691 | 35228 25175 810229 32.2 | 59.129 % | c | 94494 | 53962 128691 | 38751 26884 893776 33.2 | 59.129 % | c | 97058 | 53502 127624 | 42626 29325 1028663 35.1 | 59.448 % | c | 100903 | 53502 127624 | 46889 33170 1443156 43.5 | 59.448 % | c ============================================================================== c [1mFound solution: 392[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 | 102207 | 53321 127160 | 17773 34224 1571198 45.9 | 59.448 % | c | 102307 | 53321 127160 | 19550 34324 1572900 45.8 | 59.571 % | c | 102457 | 53321 127160 | 21505 34474 1576618 45.7 | 59.571 % | c | 102682 | 53321 127160 | 23655 34699 1590651 45.8 | 59.571 % | c | 103019 | 53263 127025 | 26021 35029 1604255 45.8 | 59.683 % | c | 103525 | 52966 126331 | 28623 35510 1643039 46.3 | 59.823 % | c | 104284 | 52966 126331 | 31485 36269 1749276 48.2 | 59.823 % | c | 105424 | 52966 126331 | 34634 37409 1794657 48.0 | 59.823 % | c | 107133 | 52966 126331 | 38098 39118 1869384 47.8 | 59.823 % | c ============================================================================== c [1mFound solution: 391[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 | 107998 | 53024 126481 | 17674 39983 1909277 47.8 | 59.823 % | c | 108098 | 53024 126481 | 19441 40083 1912087 47.7 | 59.806 % | c | 108250 | 53024 126481 | 21385 40235 1914748 47.6 | 59.806 % | c | 108475 | 53024 126481 | 23524 40460 1928824 47.7 | 59.806 % | c | 108815 | 53024 126481 | 25876 40800 1937853 47.5 | 59.806 % | c | 109321 | 53024 126481 | 28464 41306 1972223 47.7 | 59.806 % | c | 110081 | 53024 126481 | 31310 42066 2008878 47.8 | 59.806 % | c | 111220 | 53024 126481 | 34441 43205 2054716 47.6 | 59.806 % | c | 112928 | 53024 126481 | 37885 44913 2150068 47.9 | 59.806 % | c | 115491 | 53024 126481 | 41674 47476 2336613 49.2 | 59.806 % | c | 119337 | 53024 126481 | 45841 51322 3172972 61.8 | 59.806 % | c ============================================================================== c [1mFound solution: 387[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 | 120233 | 53130 126749 | 17710 52218 3214371 61.6 | 59.806 % | c | 120333 | 53130 126749 | 19481 22955 1343612 58.5 | 59.785 % | c | 120484 | 53096 126671 | 21429 22979 1346137 58.6 | 59.806 % | c | 120710 | 53096 126671 | 23572 23205 1352940 58.3 | 59.806 % | c | 121047 | 53096 126671 | 25929 23542 1362460 57.9 | 59.806 % | c | 121553 | 53096 126671 | 28522 24048 1391843 57.9 | 59.806 % | c | 122312 | 53096 126671 | 31374 24807 1414227 57.0 | 59.806 % | c | 123451 | 53096 126671 | 34511 25946 1500160 57.8 | 59.806 % | c | 125160 | 53096 126671 | 37962 27655 1569798 56.8 | 59.806 % | c | 127722 | 53096 126671 | 41759 30217 1659676 54.9 | 59.806 % | c ============================================================================== c [1mFound solution: 386[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 | 129602 | 53012 126448 | 17670 32097 1735795 54.1 | 59.806 % | c | 129703 | 53012 126448 | 19437 32198 1737801 54.0 | 59.842 % | c | 129853 | 53012 126448 | 21380 32348 1739600 53.8 | 59.842 % | c | 130078 | 53012 126448 | 23518 32573 1758908 54.0 | 59.842 % | c | 130415 | 53012 126448 | 25870 32910 1767014 53.7 | 59.842 % | c | 130921 | 53012 126448 | 28457 33416 1778011 53.2 | 59.842 % | c | 131681 | 52927 126253 | 31303 34175 1825203 53.4 | 59.898 % | c | 132822 | 52911 126213 | 34433 35315 1901575 53.8 | 59.915 % | c | 134532 | 52911 126213 | 37877 37025 1997722 54.0 | 59.915 % | c | 137094 | 52911 126213 | 41664 39587 2172163 54.9 | 59.915 % | c | 140939 | 52911 126213 | 45831 43432 2407350 55.4 | 59.915 % | c ============================================================================== c [1mFound solution: 385[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 | 145735 | 52806 125987 | 17602 48221 2619092 54.3 | 59.915 % | c | 145835 | 52806 125987 | 19362 23203 702614 30.3 | 60.010 % | c | 145985 | 52806 125987 | 21298 23353 706014 30.2 | 60.010 % | c | 146212 | 52806 125987 | 23428 23580 713242 30.2 | 60.010 % | c | 146550 | 52806 125987 | 25771 23918 726339 30.4 | 60.010 % | c | 147056 | 52806 125987 | 28348 24424 742527 30.4 | 60.010 % | c | 147815 | 52806 125987 | 31183 25183 767688 30.5 | 60.010 % | c | 148954 | 52806 125987 | 34301 26322 787456 29.9 | 60.010 % | c | 150662 | 52806 125987 | 37731 28030 929651 33.2 | 60.010 % | c | 153224 | 52806 125987 | 41504 30592 1101605 36.0 | 60.010 % | c | 157068 | 52806 125987 | 45655 34436 1729482 50.2 | 60.010 % | c | 162835 | 52806 125987 | 50220 40203 2287408 56.9 | 60.010 % | c | 171486 | 52806 125987 | 55242 48854 4501838 92.1 | 60.010 % | c | 184460 | 52806 125987 | 60766 61828 5894807 95.3 | 60.010 % | c | 203921 | 52806 125987 | 66843 81289 7133338 87.8 | 60.010 % | c ============================================================================== c [1mFound solution: 384[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 | 228199 | 52365 124877 | 17455 21102 2950215 139.8 | 60.010 % | c | 228299 | 52365 124877 | 19200 21202 2952021 139.2 | 60.293 % | c | 228449 | 52365 124877 | 21120 21352 2958624 138.6 | 60.293 % | c | 228674 | 52365 124877 | 23232 21577 2971024 137.7 | 60.293 % | c | 229011 | 52365 124877 | 25555 21914 2975769 135.8 | 60.293 % | c | 229522 | 52365 124877 | 28111 22425 2982227 133.0 | 60.293 % | c | 230281 | 52365 124877 | 30922 23184 3024901 130.5 | 60.293 % | c | 231421 | 52365 124877 | 34014 24324 3047739 125.3 | 60.293 % | c ============================================================================== c [1mFound solution: 383[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 | 232583 | 52422 125024 | 17474 25486 3083857 121.0 | 60.293 % | c | 232683 | 52422 125024 | 19221 25586 3085557 120.6 | 60.276 % | c | 232834 | 52422 125024 | 21143 25737 3090075 120.1 | 60.276 % | c | 233059 | 52422 125024 | 23257 25962 3092906 119.1 | 60.276 % | c | 233396 | 52422 125024 | 25583 26299 3096814 117.8 | 60.276 % | c | 233902 | 52422 125024 | 28142 26805 3104042 115.8 | 60.276 % | c | 234661 | 52422 125024 | 30956 27564 3120811 113.2 | 60.276 % | c | 235800 | 52422 125024 | 34051 28703 3155609 109.9 | 60.276 % | c | 237508 | 52422 125024 | 37457 30411 3285079 108.0 | 60.276 % | c | 240070 | 52356 124868 | 41202 32957 3368763 102.2 | 60.328 % | c | 243914 | 52291 124720 | 45323 36796 3601189 97.9 | 60.371 % | c ============================================================================== c [1mFound solution: 382[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 | 249200 | 51887 123719 | 17295 41809 3896215 93.2 | 60.371 % | c | 249300 | 51887 123719 | 19024 41909 3898427 93.0 | 60.634 % | c | 249452 | 51853 123642 | 20926 42059 3900218 92.7 | 60.658 % | c | 249677 | 51823 123572 | 23019 42277 3902136 92.3 | 60.679 % | c | 250014 | 51823 123572 | 25321 42614 3910680 91.8 | 60.679 % | c | 250520 | 51823 123572 | 27853 43120 3928389 91.1 | 60.679 % | c | 251279 | 51823 123572 | 30639 43879 3958204 90.2 | 60.679 % | c | 252418 | 51823 123572 | 33703 45018 3994711 88.7 | 60.679 % | c | 254129 | 51763 123431 | 37073 46704 4054559 86.8 | 60.724 % | c | 256692 | 51763 123431 | 40780 49267 4190756 85.1 | 60.724 % | c | 260537 | 51506 122837 | 44858 52663 4516221 85.8 | 60.900 % | c | 266304 | 51506 122837 | 49344 58430 4894888 83.8 | 60.900 % | c | 274954 | 51506 122837 | 54279 67080 5568885 83.0 | 60.900 % | c | 287928 | 51506 122837 | 59707 80054 7200542 89.9 | 60.900 % | c | 307389 | 51506 122837 | 65677 24926 2404222 96.5 | 60.900 % | c ============================================================================== c [1mFound solution: 381[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 | 308363 | 51567 122994 | 17189 25900 2465006 95.2 | 60.900 % | c | 308464 | 51567 122994 | 18907 26001 2470191 95.0 | 60.892 % | c | 308614 | 51567 122994 | 20798 26151 2478996 94.8 | 60.892 % | c | 308839 | 51567 122994 | 22878 26376 2493704 94.5 | 60.892 % | c | 309176 | 51567 122994 | 25166 26713 2505579 93.8 | 60.892 % | c | 309682 | 51567 122994 | 27683 27219 2537948 93.2 | 60.892 % | c | 310441 | 51567 122994 | 30451 27978 2646998 94.6 | 60.892 % | c | 311584 | 51567 122994 | 33496 29121 2671848 91.7 | 60.892 % | c | 313293 | 51567 122994 | 36846 30830 2742395 89.0 | 60.892 % | c | 315856 | 51567 122994 | 40530 33393 2805529 84.0 | 60.892 % | c ============================================================================== c [1mFound solution: 380[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 | 317254 | 51422 122628 | 17140 34773 2846286 81.9 | 60.892 % | c | 317354 | 51422 122628 | 18854 34873 2848133 81.7 | 60.979 % | c | 317506 | 51422 122628 | 20739 35025 2851911 81.4 | 60.979 % | c | 317732 | 51422 122628 | 22813 35251 2859718 81.1 | 60.979 % | c | 318069 | 51422 122628 | 25094 35588 2869911 80.6 | 60.979 % | c | 318575 | 51422 122628 | 27604 36094 2877645 79.7 | 60.979 % | c | 319335 | 51422 122628 | 30364 36854 2920600 79.2 | 60.979 % | c | 320474 | 51422 122628 | 33401 37993 2961503 77.9 | 60.979 % | c | 322184 | 51422 122628 | 36741 39703 3066663 77.2 | 60.979 % | c | 324746 | 51422 122628 | 40415 42265 3370120 79.7 | 60.979 % | 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 x#### 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.96 0.91 2/54 29425 Raw data (stat): 29425 (runsolver) R 29424 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423354898 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 0 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0007 s] Raw data (loadavg): 0.93 0.96 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4288 0 0 0 987 11 0 0 25 0 1 0 423354898 20066304 4115 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4899 4115 603 41 0 4858 0 vsize: 19596 [startup+20.0013 s] Raw data (loadavg): 0.94 0.96 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4398 0 0 0 1985 12 0 0 25 0 1 0 423354898 20832256 4225 4294967295 134512640 134672761 3221224576 3221223748 134556602 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5086 4225 603 41 0 5045 0 vsize: 20344 [startup+30.0007 s] Raw data (loadavg): 0.95 0.96 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4398 0 0 0 2985 12 0 0 25 0 1 0 423354898 20832256 4225 4294967295 134512640 134672761 3221224576 3221223728 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5086 4225 603 41 0 5045 0 vsize: 20344 [startup+40.0011 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4413 0 0 0 3984 12 0 0 25 0 1 0 423354898 20832256 4240 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5086 4240 603 41 0 5045 0 vsize: 20344 [startup+50.0014 s] Raw data (loadavg): 0.96 0.96 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4475 0 0 0 4984 12 0 0 25 0 1 0 423354898 21114880 4302 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5155 4302 603 41 0 5114 0 vsize: 20620 [startup+60.0019 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4664 0 0 0 5983 14 0 0 25 0 1 0 423354898 21897216 4491 4294967295 134512640 134672761 3221224576 3221223776 134557913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5346 4491 603 41 0 5305 0 vsize: 21384 [startup+70.0029 s] Raw data (loadavg): 0.97 0.96 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4782 0 0 0 6983 14 0 0 25 0 1 0 423354898 22433792 4609 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5477 4609 603 41 0 5436 0 vsize: 21908 [startup+80.0026 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 4862 0 0 0 7982 14 0 0 25 0 1 0 423354898 22683648 4689 4294967295 134512640 134672761 3221224576 3221223680 134560318 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5538 4689 603 41 0 5497 0 vsize: 22152 [startup+90.0031 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5081 0 0 0 8982 15 0 0 25 0 1 0 423354898 23621632 4908 4294967295 134512640 134672761 3221224576 3221223700 134566034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5767 4908 603 41 0 5726 0 vsize: 23068 [startup+100.003 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5225 0 0 0 9982 16 0 0 25 0 1 0 423354898 24350720 5052 4294967295 134512640 134672761 3221224576 3221223776 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5945 5052 603 41 0 5904 0 vsize: 23780 [startup+110.005 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5345 0 0 0 10982 16 0 0 25 0 1 0 423354898 24752128 5172 4294967295 134512640 134672761 3221224576 3221223748 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6043 5172 603 41 0 6002 0 vsize: 24172 [startup+120.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5539 0 0 0 11981 16 0 0 25 0 1 0 423354898 25559040 5366 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6240 5366 603 41 0 6199 0 vsize: 24960 [startup+130.004 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5691 0 0 0 12981 17 0 0 25 0 1 0 423354898 26185728 5518 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6393 5518 603 41 0 6352 0 vsize: 25572 [startup+140.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5845 0 0 0 13980 18 0 0 25 0 1 0 423354898 26722304 5672 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6524 5672 603 41 0 6483 0 vsize: 26096 [startup+150.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5847 0 0 0 14980 18 0 0 25 0 1 0 423354898 26722304 5674 4294967295 134512640 134672761 3221224576 3221223712 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6524 5674 603 41 0 6483 0 vsize: 26096 [startup+160.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5847 0 0 0 15980 18 0 0 25 0 1 0 423354898 26722304 5674 4294967295 134512640 134672761 3221224576 3221223744 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6524 5674 603 41 0 6483 0 vsize: 26096 [startup+170.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5848 0 0 0 16980 18 0 0 25 0 1 0 423354898 26722304 5675 4294967295 134512640 134672761 3221224576 3221223876 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6524 5675 603 41 0 6483 0 vsize: 26096 [startup+180.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5849 0 0 0 17980 18 0 0 25 0 1 0 423354898 26722304 5676 4294967295 134512640 134672761 3221224576 3221223720 134560630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6524 5676 603 41 0 6483 0 vsize: 26096 [startup+190.005 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 5897 0 0 0 18980 18 0 0 25 0 1 0 423354898 26984448 5724 4294967295 134512640 134672761 3221224576 3221223592 1075353266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6588 5724 603 41 0 6547 0 vsize: 26352 [startup+200.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6182 0 0 0 19980 19 0 0 25 0 1 0 423354898 28184576 6009 4294967295 134512640 134672761 3221224576 3221223748 134556643 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6881 6009 603 41 0 6840 0 vsize: 27524 [startup+210.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6340 0 0 0 20980 20 0 0 25 0 1 0 423354898 28725248 6167 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7013 6167 603 41 0 6972 0 vsize: 28052 [startup+220.006 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6512 0 0 0 21979 20 0 0 25 0 1 0 423354898 29528064 6339 4294967295 134512640 134672761 3221224576 3221223760 134558360 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7209 6339 603 41 0 7168 0 vsize: 28836 [startup+230.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6634 0 0 0 22979 21 0 0 25 0 1 0 423354898 29921280 6461 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7305 6461 603 41 0 7264 0 vsize: 29220 [startup+240.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6634 0 0 0 23979 21 0 0 25 0 1 0 423354898 29921280 6461 4294967295 134512640 134672761 3221224576 3221223760 134559532 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7305 6461 603 41 0 7264 0 vsize: 29220 [startup+250.007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6634 0 0 0 24979 21 0 0 25 0 1 0 423354898 29921280 6461 4294967295 134512640 134672761 3221224576 3221223744 134561266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7305 6461 603 41 0 7264 0 vsize: 29220 [startup+260.008 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6634 0 0 0 25980 21 0 0 25 0 1 0 423354898 29921280 6461 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7305 6461 603 41 0 7264 0 vsize: 29220 [startup+270.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6634 0 0 0 26980 21 0 0 25 0 1 0 423354898 29921280 6461 4294967295 134512640 134672761 3221224576 3221223744 134561201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7305 6461 603 41 0 7264 0 vsize: 29220 [startup+280.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6685 0 0 0 27980 21 0 0 25 0 1 0 423354898 30187520 6512 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7370 6512 603 41 0 7329 0 vsize: 29480 [startup+290.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 6839 0 0 0 28980 21 0 0 25 0 1 0 423354898 30855168 6666 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7533 6666 603 41 0 7492 0 vsize: 30132 [startup+300.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 7049 0 0 0 29979 22 0 0 25 0 1 0 423354898 31657984 6876 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7729 6876 603 41 0 7688 0 vsize: 30916 [startup+310.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 7278 0 0 0 30978 23 0 0 25 0 1 0 423354898 32595968 7105 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7958 7105 603 41 0 7917 0 vsize: 31832 [startup+320.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 7662 0 0 0 31977 24 0 0 25 0 1 0 423354898 34193408 7489 4294967295 134512640 134672761 3221224576 3221223680 134560008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8348 7489 603 41 0 8307 0 vsize: 33392 [startup+330.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8036 0 0 0 32976 25 0 0 25 0 1 0 423354898 35667968 7863 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8708 7863 603 41 0 8667 0 vsize: 34832 [startup+340.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 33976 25 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223680 134560160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7899 603 41 0 8700 0 vsize: 34964 [startup+350.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 34976 25 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7899 603 41 0 8700 0 vsize: 34964 [startup+360.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 35977 25 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7899 603 41 0 8700 0 vsize: 34964 [startup+370.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 36977 25 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7899 603 41 0 8700 0 vsize: 34964 [startup+380.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 37977 26 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7899 603 41 0 8700 0 vsize: 34964 [startup+390.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 38977 26 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223744 134560994 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7899 603 41 0 8700 0 vsize: 34964 [startup+400.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8072 0 0 0 39977 26 0 0 25 0 1 0 423354898 35803136 7899 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7899 603 41 0 8700 0 vsize: 34964 [startup+410.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 40978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7901 603 41 0 8700 0 vsize: 34964 [startup+420.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 41978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7901 603 41 0 8700 0 vsize: 34964 [startup+430.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 42978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223744 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7901 603 41 0 8700 0 vsize: 34964 [startup+440.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 43978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223728 134561249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7901 603 41 0 8700 0 vsize: 34964 [startup+450.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 44978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223680 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7901 603 41 0 8700 0 vsize: 34964 [startup+460.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 45978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223744 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7901 603 41 0 8700 0 vsize: 34964 [startup+470.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 46978 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7901 603 41 0 8700 0 vsize: 34964 [startup+480.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8074 0 0 0 47979 26 0 0 25 0 1 0 423354898 35803136 7901 4294967295 134512640 134672761 3221224576 3221223680 134559835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8741 7901 603 41 0 8700 0 vsize: 34964 [startup+490.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8242 0 0 0 48978 26 0 0 25 0 1 0 423354898 36597760 8069 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8935 8069 603 41 0 8894 0 vsize: 35740 [startup+500.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8580 0 0 0 49977 27 0 0 25 0 1 0 423354898 37924864 8407 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9259 8407 603 41 0 9218 0 vsize: 37036 [startup+510.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 8982 0 0 0 50977 28 0 0 25 0 1 0 423354898 39522304 8809 4294967295 134512640 134672761 3221224576 3221223760 134559498 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9649 8809 603 41 0 9608 0 vsize: 38596 [startup+520.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 9418 0 0 0 51976 29 0 0 25 0 1 0 423354898 41377792 9245 4294967295 134512640 134672761 3221224576 3221223760 134559616 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10102 9245 603 41 0 10061 0 vsize: 40408 [startup+530.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 9675 0 0 0 52975 30 0 0 25 0 1 0 423354898 42450944 9502 4294967295 134512640 134672761 3221224576 3221223680 134560291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10364 9502 603 41 0 10323 0 vsize: 41456 [startup+540.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 9956 0 0 0 53975 31 0 0 25 0 1 0 423354898 43528192 9783 4294967295 134512640 134672761 3221224576 3221223712 134560613 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10627 9783 603 41 0 10586 0 vsize: 42508 [startup+550.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 10232 0 0 0 54974 32 0 0 25 0 1 0 423354898 44728320 10059 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10920 10059 603 41 0 10879 0 vsize: 43680 [startup+560.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 10464 0 0 0 55973 32 0 0 25 0 1 0 423354898 45662208 10291 4294967295 134512640 134672761 3221224576 3221223744 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11148 10291 603 41 0 11107 0 vsize: 44592 [startup+570.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 10728 0 0 0 56973 33 0 0 25 0 1 0 423354898 46731264 10555 4294967295 134512640 134672761 3221224576 3221223680 134560285 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11409 10555 603 41 0 11368 0 vsize: 45636 [startup+580.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 10961 0 0 0 57972 34 0 0 25 0 1 0 423354898 47661056 10788 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11636 10788 603 41 0 11595 0 vsize: 46544 [startup+590.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11100 0 0 0 58971 35 0 0 25 0 1 0 423354898 48197632 10927 4294967295 134512640 134672761 3221224576 3221223760 134558687 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11767 10927 603 41 0 11726 0 vsize: 47068 [startup+600.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11264 0 0 0 59971 35 0 0 25 0 1 0 423354898 49123328 11091 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11993 11091 603 41 0 11952 0 vsize: 47972 [startup+610.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11420 0 0 0 60971 36 0 0 25 0 1 0 423354898 49786880 11247 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12155 11247 603 41 0 12114 0 vsize: 48620 [startup+620.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11605 0 0 0 61971 36 0 0 25 0 1 0 423354898 50450432 11432 4294967295 134512640 134672761 3221224576 3221223744 134560917 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12317 11432 603 41 0 12276 0 vsize: 49268 [startup+630.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11779 0 0 0 62970 37 0 0 25 0 1 0 423354898 51245056 11606 4294967295 134512640 134672761 3221224576 3221223712 134560628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12511 11606 603 41 0 12470 0 vsize: 50044 [startup+640.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 11954 0 0 0 63970 37 0 0 25 0 1 0 423354898 51908608 11781 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12673 11781 603 41 0 12632 0 vsize: 50692 [startup+650.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12114 0 0 0 64970 37 0 0 25 0 1 0 423354898 52609024 11941 4294967295 134512640 134672761 3221224576 3221223712 134560608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12844 11941 603 41 0 12803 0 vsize: 51376 [startup+660.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12287 0 0 0 65970 38 0 0 25 0 1 0 423354898 53272576 12114 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13006 12114 603 41 0 12965 0 vsize: 52024 [startup+670.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12440 0 0 0 66969 38 0 0 25 0 1 0 423354898 53936128 12267 4294967295 134512640 134672761 3221224576 3221223744 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13168 12267 603 41 0 13127 0 vsize: 52672 [startup+680.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12500 0 0 0 67969 39 0 0 25 0 1 0 423354898 54202368 12327 4294967295 134512640 134672761 3221224576 3221223744 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13233 12327 603 41 0 13192 0 vsize: 52932 [startup+690.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12584 0 0 0 68969 39 0 0 25 0 1 0 423354898 54468608 12411 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13298 12411 603 41 0 13257 0 vsize: 53192 [startup+700.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 12976 0 0 0 69968 40 0 0 25 0 1 0 423354898 56074240 12803 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13690 12803 603 41 0 13649 0 vsize: 54760 [startup+710.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 13403 0 0 0 70968 41 0 0 25 0 1 0 423354898 57815040 13230 4294967295 134512640 134672761 3221224576 3221223712 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14115 13230 603 41 0 14074 0 vsize: 56460 [startup+720.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 13864 0 0 0 71966 43 0 0 25 0 1 0 423354898 59695104 13691 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14574 13691 603 41 0 14533 0 vsize: 58296 [startup+730.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 14282 0 0 0 72965 44 0 0 25 0 1 0 423354898 61435904 14109 4294967295 134512640 134672761 3221224576 3221223680 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14999 14109 603 41 0 14958 0 vsize: 59996 [startup+740.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 14718 0 0 0 73964 46 0 0 25 0 1 0 423354898 63180800 14545 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15425 14545 603 41 0 15384 0 vsize: 61700 [startup+750.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 15125 0 0 0 74962 47 0 0 25 0 1 0 423354898 64794624 14952 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15819 14952 603 41 0 15778 0 vsize: 63276 [startup+760.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 15543 0 0 0 75961 49 0 0 25 0 1 0 423354898 66531328 15370 4294967295 134512640 134672761 3221224576 3221223744 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16243 15370 603 41 0 16202 0 vsize: 64972 [startup+770.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 15932 0 0 0 76959 50 0 0 25 0 1 0 423354898 68128768 15759 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16633 15759 603 41 0 16592 0 vsize: 66532 [startup+780.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 77959 51 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223712 134560637 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+790.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 78958 51 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223740 134564518 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+800.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 79957 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223728 134565064 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+810.018 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 80957 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+820.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 81958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+830.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 82958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223720 134560555 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+840.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 83958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+850.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 84958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+860.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 85958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223712 134560718 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+870.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 86958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+880.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 87958 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134559875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+890.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 88959 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+900.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 89959 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+910.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 90959 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+920.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 91959 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223776 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+930.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 92959 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+940.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 93960 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560264 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+950.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 94960 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223760 134558360 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+960.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 95960 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+970.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 96960 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223712 134565056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+980.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 97960 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+990.023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 98961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1000.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 99961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1010.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 100961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1020.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 101961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1030.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 102961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561400 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1040.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 103961 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223712 134560729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1050.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 104962 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1060.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 105962 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134559981 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1070.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 106962 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1080.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 107962 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134559914 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1090.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 108962 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223748 134559060 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1100.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 109963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560260 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1110.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 110963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223680 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1120.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 111963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1130.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 112963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1140.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 113963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223632 134565048 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1150.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 114963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1160.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 115963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1170.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 116963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1180.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 117963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223736 134561238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1190.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 118963 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223744 134561021 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 [startup+1200.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 29425 Raw data (stat): 29425 (minisat+) R 29424 24215 24214 0 -1 0 16212 0 0 0 119964 52 0 0 25 0 1 0 423354898 69332992 16039 4294967295 134512640 134672761 3221224576 3221223776 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16927 16039 603 41 0 16886 0 vsize: 67708 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.07 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 29425 Raw data (stat): 29425 (minisat+) Z 29424 24215 24214 0 -1 12 16215 0 0 0 119964 55 0 0 25 0 1 0 423354898 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 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.06 CPU time (s): 1200.2 CPU user time (s): 1199.64 CPU system time (s): 0.556915 CPU usage (%): 100.011 Max. virtual memory (Kb): 67708 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####