Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-markshare2.opb |
MD5SUM | 3b5121187baf09367bd50bdc4d869d21 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 8448 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 140 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 7340025 |
Number of bits of the sum of numbers in the objective function | 23 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 7340025 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.43 |
Number of variables | 200 |
Total number of constraints | 67 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 7 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 80 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-04-21 16:04:35 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17646 boxname=wulflinc4 idbench=1358 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: 3b5121187baf09367bd50bdc4d869d21 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-markshare2.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-markshare2.opb IDLAUNCH: 17646 /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: 816932 kB Buffers: 23548 kB Cached: 172880 kB SwapCached: 364 kB Active: 28288 kB Inactive: 170604 kB HighTotal: 131008 kB HighFree: 94080 kB LowTotal: 903652 kB LowFree: 722852 kB SwapTotal: 2097136 kB SwapFree: 2096356 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6400 kB Slab: 13096 kB Committed_AS: 71640 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-21 16:24:37 (client local time) WITH STATUS 10 IN 1200.18 SECONDS stats: 17646 7 1200.18 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 14 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####### c -- Clauses(.)/Splits(s): (none) c ---[ 12]---> Adder-cost: 354 maxlim: 431615 bits: 20/19 c ---[ 10]---> Adder-cost: 380 maxlim: 461183 bits: 20/19 c ---[ 8]---> Adder-cost: 350 maxlim: 445183 bits: 20/19 c ---[ 6]---> Adder-cost: 340 maxlim: 477951 bits: 20/19 c ---[ 4]---> Adder-cost: 390 maxlim: 451839 bits: 20/19 c ---[ 2]---> Adder-cost: 358 maxlim: 468735 bits: 20/19 c ---[ 0]---> Adder-cost: 374 maxlim: 444543 bits: 20/19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 17222 61228 | 5740 0 0 nan | 0.000 % | c | 100 | 17222 61228 | 6314 100 905 9.1 | 9.969 % | c | 253 | 17214 61202 | 6945 252 2033 8.1 | 10.003 % | c | 478 | 17206 61176 | 7639 476 4722 9.9 | 10.038 % | c ============================================================================== c [1mFound solution: 866304[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1068 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 536 | 19853 67360 | 6617 534 5740 10.7 | 10.038 % | c ============================================================================== c [1mFound solution: 828672[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 632 | 19863 67400 | 6621 629 13956 22.2 | 10.038 % | c | 733 | 19863 67400 | 7283 730 20234 27.7 | 7.644 % | c | 884 | 19855 67374 | 8011 879 45616 51.9 | 7.696 % | c | 1110 | 19847 67348 | 8812 1105 70591 63.9 | 7.696 % | c | 1447 | 19839 67322 | 9693 1441 95879 66.5 | 7.723 % | c ============================================================================== c [1mFound solution: 702720[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1945 | 19842 67325 | 6614 1938 159401 82.3 | 7.723 % | c | 2046 | 19842 67325 | 7275 2039 167910 82.3 | 7.761 % | c | 2197 | 19842 67325 | 8002 2190 179220 81.8 | 7.761 % | c | 2423 | 19842 67325 | 8803 2416 196028 81.1 | 7.761 % | c | 2761 | 19842 67325 | 9683 2754 236792 86.0 | 7.761 % | c | 3268 | 19842 67325 | 10651 3261 287766 88.2 | 7.761 % | c ============================================================================== c [1mFound solution: 676352[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3715 | 19858 67370 | 6619 3708 318920 86.0 | 7.761 % | c | 3815 | 19858 67370 | 7280 3808 328892 86.4 | 7.766 % | c | 3965 | 19858 67370 | 8008 3958 346566 87.6 | 7.766 % | c | 4190 | 19858 67370 | 8809 4183 366380 87.6 | 7.766 % | c | 4528 | 19852 67357 | 9690 4520 400494 88.6 | 7.819 % | c | 5034 | 19844 67331 | 10659 5025 444892 88.5 | 7.845 % | c | 5794 | 19836 67305 | 11725 5784 509124 88.0 | 7.871 % | c | 6934 | 19828 67279 | 12898 6923 580155 83.8 | 7.897 % | c ============================================================================== c [1mFound solution: 674304[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7359 | 19838 67302 | 6612 7348 621804 84.6 | 7.897 % | c | 7463 | 19838 67302 | 7273 3778 243653 64.5 | 7.913 % | c | 7614 | 19838 67302 | 8000 3929 255506 65.0 | 7.913 % | c ============================================================================== c [1mFound solution: 654336[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7790 | 19849 67335 | 6616 4105 268736 65.5 | 7.913 % | c ============================================================================== c [1mFound solution: 645120[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7856 | 19857 67359 | 6619 4171 271081 65.0 | 7.913 % | c | 7958 | 19857 67359 | 7280 4273 278513 65.2 | 7.938 % | c ============================================================================== c [1mFound solution: 465408[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8075 | 19869 67387 | 6623 4390 284865 64.9 | 7.938 % | c | 8175 | 19869 67387 | 7285 4490 290752 64.8 | 7.949 % | c | 8326 | 19869 67387 | 8013 4641 302249 65.1 | 7.949 % | c | 8551 | 19869 67387 | 8815 4866 312895 64.3 | 7.949 % | c | 8888 | 19869 67387 | 9696 5203 337269 64.8 | 7.949 % | c | 9394 | 19869 67387 | 10666 5709 372234 65.2 | 7.949 % | c | 10153 | 19869 67387 | 11733 6468 427615 66.1 | 7.949 % | c | 11294 | 19869 67387 | 12906 7609 506572 66.6 | 7.949 % | c | 13003 | 19863 67369 | 14196 9317 680687 73.1 | 7.975 % | c | 15565 | 19838 67290 | 15616 11876 979173 82.4 | 8.079 % | c | 19410 | 19838 67290 | 17178 15721 1427200 90.8 | 8.079 % | c ============================================================================== c [1mFound solution: 426240[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24555 | 19802 67164 | 6600 11781 991951 84.2 | 8.079 % | c | 24656 | 19802 67164 | 7260 5992 340445 56.8 | 8.251 % | c | 24806 | 19802 67164 | 7986 6142 346020 56.3 | 8.251 % | c | 25031 | 19802 67164 | 8784 6367 351779 55.3 | 8.251 % | c | 25370 | 19802 67164 | 9663 6706 376621 56.2 | 8.251 % | c | 25878 | 19802 67164 | 10629 7214 412120 57.1 | 8.251 % | c | 26639 | 19802 67164 | 11692 7975 454198 57.0 | 8.251 % | c | 27779 | 19802 67164 | 12861 9115 506655 55.6 | 8.251 % | c | 29487 | 19802 67164 | 14147 10823 597522 55.2 | 8.251 % | c | 32049 | 19802 67164 | 15562 13385 746703 55.8 | 8.251 % | c | 35893 | 19802 67164 | 17118 9134 445739 48.8 | 8.251 % | c | 41660 | 19802 67164 | 18830 14901 900002 60.4 | 8.251 % | c | 50309 | 19802 67164 | 20713 13630 900207 66.0 | 8.251 % | c | 63285 | 19802 67164 | 22784 15643 876282 56.0 | 8.251 % | c | 82746 | 19802 67164 | 25063 23100 1569191 67.9 | 8.251 % | c ============================================================================== c [1mFound solution: 420352[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 110809 | 19810 67183 | 6603 24998 2030699 81.2 | 8.251 % | c | 110909 | 19810 67183 | 7263 6350 368699 58.1 | 8.269 % | c | 111061 | 19810 67183 | 7989 6502 374493 57.6 | 8.269 % | c | 111288 | 19810 67183 | 8788 6729 385690 57.3 | 8.269 % | c | 111626 | 19810 67183 | 9667 7067 413477 58.5 | 8.269 % | c | 112132 | 19810 67183 | 10634 7573 438726 57.9 | 8.269 % | c | 112891 | 19810 67183 | 11697 8332 475591 57.1 | 8.269 % | c | 114031 | 19810 67183 | 12867 9472 602990 63.7 | 8.269 % | c | 115740 | 19810 67183 | 14154 11181 705503 63.1 | 8.269 % | c ============================================================================== c [1mFound solution: 411392[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 118101 | 19822 67210 | 6607 13542 911670 67.3 | 8.269 % | c | 118201 | 19822 67210 | 7267 6871 405686 59.0 | 8.282 % | c | 118351 | 19822 67210 | 7994 7021 414241 59.0 | 8.282 % | c | 118576 | 19822 67210 | 8793 7246 434055 59.9 | 8.282 % | c | 118913 | 19822 67210 | 9673 7583 456334 60.2 | 8.282 % | c | 119419 | 19822 67210 | 10640 8089 483898 59.8 | 8.282 % | c | 120178 | 19822 67210 | 11704 8848 528469 59.7 | 8.282 % | c | 121317 | 19822 67210 | 12875 9987 592730 59.4 | 8.282 % | c | 123025 | 19822 67210 | 14162 11695 721731 61.7 | 8.282 % | c | 125587 | 19822 67210 | 15578 14257 897308 62.9 | 8.282 % | c | 129431 | 19822 67210 | 17136 9873 539594 54.7 | 8.282 % | c | 135198 | 19814 67184 | 18850 15639 1121030 71.7 | 8.308 % | c | 143849 | 19814 67184 | 20735 14328 969560 67.7 | 8.308 % | c ============================================================================== c [1mFound solution: 404480[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 151309 | 19816 67186 | 6605 11073 646615 58.4 | 8.308 % | c | 151411 | 19816 67186 | 7265 5639 309058 54.8 | 8.374 % | c | 151561 | 19816 67186 | 7992 5789 311658 53.8 | 8.374 % | c | 151786 | 19816 67186 | 8791 6014 337987 56.2 | 8.374 % | c | 152124 | 19816 67186 | 9670 6352 350939 55.2 | 8.374 % | c ============================================================================== c [1mFound solution: 363264[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 152583 | 19829 67218 | 6609 6811 361631 53.1 | 8.374 % | c | 152685 | 19829 67218 | 7269 6913 366844 53.1 | 8.385 % | c | 152836 | 19829 67218 | 7996 7064 390436 55.3 | 8.385 % | c | 153061 | 19829 67218 | 8796 7289 402314 55.2 | 8.385 % | c | 153398 | 19829 67218 | 9676 7626 416355 54.6 | 8.385 % | c | 153907 | 19829 67218 | 10643 8135 436418 53.6 | 8.385 % | c | 154667 | 19829 67218 | 11708 8895 517597 58.2 | 8.385 % | c | 155807 | 19829 67218 | 12879 10035 580468 57.8 | 8.385 % | c | 157517 | 19829 67218 | 14166 11745 642591 54.7 | 8.385 % | c | 160079 | 19829 67218 | 15583 14307 764160 53.4 | 8.385 % | c ============================================================================== c [1mFound solution: 343936[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 162554 | 19860 67292 | 6620 8590 324198 37.7 | 8.385 % | c | 162655 | 19860 67292 | 7282 4396 151608 34.5 | 8.372 % | c | 162807 | 19860 67292 | 8010 4548 161742 35.6 | 8.372 % | c | 163033 | 19860 67292 | 8811 4774 168934 35.4 | 8.372 % | c | 163371 | 19860 67292 | 9692 5112 176581 34.5 | 8.372 % | c | 163877 | 19860 67292 | 10661 5618 253166 45.1 | 8.372 % | c | 164636 | 19860 67292 | 11727 6377 301500 47.3 | 8.372 % | c | 165778 | 19860 67292 | 12900 7519 356921 47.5 | 8.372 % | c | 167486 | 19860 67292 | 14190 9227 445248 48.3 | 8.372 % | c | 170048 | 19860 67292 | 15609 11789 602596 51.1 | 8.372 % | c | 173892 | 19860 67292 | 17170 15633 831926 53.2 | 8.372 % | c | 179659 | 19860 67292 | 18887 12423 597867 48.1 | 8.372 % | c | 188308 | 19848 67265 | 20776 11130 791462 71.1 | 8.449 % | c ============================================================================== c [1mFound solution: 260352[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 188746 | 19854 67281 | 6618 11568 801463 69.3 | 8.449 % | c | 188847 | 19854 67281 | 7279 5885 256847 43.6 | 8.465 % | c | 188997 | 19854 67281 | 8007 6035 266435 44.1 | 8.465 % | c | 189223 | 19854 67281 | 8808 6261 281425 44.9 | 8.465 % | c | 189561 | 19854 67281 | 9689 6599 298712 45.3 | 8.465 % | c | 190067 | 19854 67281 | 10658 7105 319291 44.9 | 8.465 % | c | 190827 | 19854 67281 | 11724 7865 359467 45.7 | 8.465 % | c | 191968 | 19854 67281 | 12896 9006 410789 45.6 | 8.465 % | c | 193677 | 19854 67281 | 14186 10715 531399 49.6 | 8.465 % | c | 196241 | 19854 67281 | 15604 13279 685851 51.6 | 8.465 % | c | 200085 | 19854 67281 | 17165 8898 488070 54.9 | 8.465 % | c | 205852 | 19854 67281 | 18881 14665 711080 48.5 | 8.465 % | c ============================================================================== c [1mFound solution: 80128[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 206193 | 19806 67113 | 6602 14727 700340 47.6 | 8.465 % | c | 206293 | 19806 67113 | 7262 3782 103785 27.4 | 8.666 % | c | 206444 | 19806 67113 | 7988 3933 104553 26.6 | 8.666 % | c | 206669 | 19806 67113 | 8787 4158 107432 25.8 | 8.666 % | c | 207006 | 19806 67113 | 9665 4495 116514 25.9 | 8.666 % | c | 207513 | 19806 67113 | 10632 5002 128589 25.7 | 8.666 % | c ============================================================================== c [1mFound solution: 64896[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 207893 | 19615 66613 | 6538 5362 135046 25.2 | 8.666 % | c | 207995 | 19615 66613 | 7191 5464 137131 25.1 | 10.089 % | c | 208146 | 19615 66613 | 7910 5615 139840 24.9 | 10.089 % | c | 208371 | 19615 66613 | 8702 5840 147321 25.2 | 10.089 % | c | 208708 | 19615 66613 | 9572 6177 155749 25.2 | 10.089 % | c | 209215 | 19615 66613 | 10529 6684 179508 26.9 | 10.089 % | c | 209976 | 19615 66613 | 11582 7445 201615 27.1 | 10.089 % | c | 211115 | 19615 66613 | 12740 8584 243072 28.3 | 10.089 % | c | 212823 | 19615 66613 | 14014 10292 303964 29.5 | 10.089 % | c | 215385 | 19615 66613 | 15416 12854 404034 31.4 | 10.089 % | c | 219229 | 19615 66613 | 16957 8598 318726 37.1 | 10.089 % | c ============================================================================== c [1mFound solution: 63616[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 222041 | 19622 66634 | 6540 11410 477534 41.9 | 10.089 % | c | 222143 | 19622 66634 | 7194 5807 236093 40.7 | 10.102 % | c | 222293 | 19622 66634 | 7913 5957 236962 39.8 | 10.102 % | c | 222518 | 19622 66634 | 8704 6182 240201 38.9 | 10.102 % | c | 222855 | 19622 66634 | 9575 6519 253550 38.9 | 10.102 % | c | 223361 | 19622 66634 | 10532 7025 263589 37.5 | 10.102 % | c | 224121 | 19622 66634 | 11586 7785 284201 36.5 | 10.102 % | c | 225260 | 19622 66634 | 12744 8924 354542 39.7 | 10.102 % | c | 226971 | 19622 66634 | 14019 10635 414350 39.0 | 10.102 % | c | 229533 | 19622 66634 | 15420 13197 533639 40.4 | 10.102 % | c | 233377 | 19607 66589 | 16963 8676 346338 39.9 | 10.179 % | c | 239144 | 19607 66589 | 18659 14443 554456 38.4 | 10.179 % | c | 247793 | 19530 66415 | 20525 13278 517714 39.0 | 10.816 % | c | 260769 | 19429 66185 | 22577 15427 982742 63.7 | 11.633 % | c | 280230 | 19319 65931 | 24835 23197 1024138 44.1 | 12.628 % | c | 309423 | 19319 65931 | 27319 25948 1521579 58.6 | 12.628 % | c ============================================================================== c [1mFound solution: 59008[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 327090 | 19320 65935 | 6440 27848 1354853 48.7 | 12.628 % | c | 327191 | 19320 65935 | 7084 6666 249277 37.4 | 12.732 % | c | 327341 | 19320 65935 | 7792 6816 250694 36.8 | 12.732 % | c | 327566 | 19320 65935 | 8571 7041 259558 36.9 | 12.732 % | c | 327904 | 19320 65935 | 9428 7379 266686 36.1 | 12.732 % | c | 328410 | 19320 65935 | 10371 7885 277400 35.2 | 12.732 % | c | 329171 | 19320 65935 | 11408 8646 299566 34.6 | 12.732 % | c | 330310 | 19320 65935 | 12549 9785 331642 33.9 | 12.732 % | c | 332018 | 19320 65935 | 13804 11493 456254 39.7 | 12.732 % | c | 334582 | 19320 65935 | 15185 14057 533507 38.0 | 12.732 % | c | 338428 | 19320 65935 | 16703 9687 452672 46.7 | 12.732 % | c | 344195 | 19320 65935 | 18374 15454 704774 45.6 | 12.732 % | c | 352844 | 19306 65902 | 20211 14334 779072 54.4 | 12.911 % | c | 365818 | 19288 65862 | 22232 16842 680144 40.4 | 13.038 % | c | 385280 | 19288 65862 | 24455 13318 512736 38.5 | 13.038 % | c | 414473 | 19288 65862 | 26901 17159 819651 47.8 | 13.038 % | c | 458262 | 19259 65797 | 29591 16835 605068 35.9 | 13.242 % | c | 523948 | 19241 65756 | 32550 15348 637855 41.6 | 13.369 % | c | 622474 | 19241 65756 | 35805 17341 946468 54.6 | 13.369 % | #### 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.85 0.96 0.98 2/54 10350 Raw data (stat): 10350 (runsolver) R 10349 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488152266 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0007 s] Raw data (loadavg): 0.87 0.97 0.98 2/54 10350 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 1341 0 0 0 995 3 0 0 25 0 1 0 488152266 7036928 1319 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 1718 1319 603 41 0 1677 0 vsize: 6872 [startup+20.0017 s] Raw data (loadavg): 0.89 0.97 0.98 2/54 10350 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 1476 0 0 0 1994 4 0 0 25 0 1 0 488152266 7696384 1454 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1879 1454 603 41 0 1838 0 vsize: 7516 [startup+30.0024 s] Raw data (loadavg): 0.91 0.97 0.98 2/54 10350 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 1816 0 0 0 2993 5 0 0 25 0 1 0 488152266 9023488 1794 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 2203 1794 603 41 0 2162 0 vsize: 8812 [startup+40.0021 s] Raw data (loadavg): 0.92 0.97 0.98 2/54 10350 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2167 0 0 0 3991 7 0 0 25 0 1 0 488152266 10485760 2145 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2560 2145 603 41 0 2519 0 vsize: 10240 [startup+50.0026 s] Raw data (loadavg): 0.93 0.97 0.98 2/54 10350 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2495 0 0 0 4990 8 0 0 25 0 1 0 488152266 11915264 2473 4294967295 134512640 134672761 3221224624 3221223772 134565030 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2909 2473 603 41 0 2868 0 vsize: 11636 [startup+60.0029 s] Raw data (loadavg): 0.94 0.97 0.98 2/54 10350 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2666 0 0 0 5989 9 0 0 25 0 1 0 488152266 12574720 2644 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3070 2644 603 41 0 3029 0 vsize: 12280 [startup+70.0038 s] Raw data (loadavg): 0.95 0.97 0.98 2/54 10350 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2666 0 0 0 6989 9 0 0 25 0 1 0 488152266 12574720 2644 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3070 2644 603 41 0 3029 0 vsize: 12280 [startup+80.0048 s] Raw data (loadavg): 0.96 0.97 0.98 2/54 10350 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2666 0 0 0 7989 9 0 0 25 0 1 0 488152266 12574720 2644 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3070 2644 603 41 0 3029 0 vsize: 12280 [startup+90.0054 s] Raw data (loadavg): 0.96 0.97 0.98 2/54 10350 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2666 0 0 0 8989 9 0 0 25 0 1 0 488152266 12574720 2644 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3070 2644 603 41 0 3029 0 vsize: 12280 [startup+100.005 s] Raw data (loadavg): 0.97 0.97 0.98 2/54 10350 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2667 0 0 0 9989 9 0 0 25 0 1 0 488152266 12574720 2645 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3070 2645 603 41 0 3029 0 vsize: 12280 [startup+110.007 s] Raw data (loadavg): 0.97 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2667 0 0 0 10989 9 0 0 25 0 1 0 488152266 12574720 2645 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3070 2645 603 41 0 3029 0 vsize: 12280 [startup+120.007 s] Raw data (loadavg): 0.98 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2669 0 0 0 11989 9 0 0 25 0 1 0 488152266 12574720 2647 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3070 2647 603 41 0 3029 0 vsize: 12280 [startup+130.008 s] Raw data (loadavg): 0.98 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2669 0 0 0 12990 9 0 0 25 0 1 0 488152266 12574720 2647 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3070 2647 603 41 0 3029 0 vsize: 12280 [startup+140.008 s] Raw data (loadavg): 0.98 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2669 0 0 0 13990 9 0 0 25 0 1 0 488152266 12574720 2647 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3070 2647 603 41 0 3029 0 vsize: 12280 [startup+150.007 s] Raw data (loadavg): 0.98 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2735 0 0 0 14990 9 0 0 25 0 1 0 488152266 12840960 2713 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3135 2713 603 41 0 3094 0 vsize: 12540 [startup+160.007 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2735 0 0 0 15990 9 0 0 25 0 1 0 488152266 12840960 2713 4294967295 134512640 134672761 3221224624 3221223792 134561156 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3135 2713 603 41 0 3094 0 vsize: 12540 [startup+170.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 2770 0 0 0 16990 9 0 0 25 0 1 0 488152266 12976128 2748 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3168 2748 603 41 0 3127 0 vsize: 12672 [startup+180.008 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3090 0 0 0 17989 10 0 0 25 0 1 0 488152266 14307328 3068 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3493 3068 603 41 0 3452 0 vsize: 13972 [startup+190.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3090 0 0 0 18990 10 0 0 25 0 1 0 488152266 14307328 3068 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3493 3068 603 41 0 3452 0 vsize: 13972 [startup+200.009 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3090 0 0 0 19990 10 0 0 25 0 1 0 488152266 14307328 3068 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3493 3068 603 41 0 3452 0 vsize: 13972 [startup+210.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3169 0 0 0 20990 10 0 0 25 0 1 0 488152266 14573568 3147 4294967295 134512640 134672761 3221224624 3221223808 134558656 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3558 3147 603 41 0 3517 0 vsize: 14232 [startup+220.01 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3307 0 0 0 21989 11 0 0 25 0 1 0 488152266 15106048 3285 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3688 3285 603 41 0 3647 0 vsize: 14752 [startup+230.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3307 0 0 0 22990 11 0 0 25 0 1 0 488152266 15106048 3285 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3688 3285 603 41 0 3647 0 vsize: 14752 [startup+240.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3307 0 0 0 23990 11 0 0 25 0 1 0 488152266 15106048 3285 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3688 3285 603 41 0 3647 0 vsize: 14752 [startup+250.011 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 24990 11 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+260.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 25990 11 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+270.012 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 26990 11 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+280.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 27990 11 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+290.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 28990 11 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223808 134558658 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+300.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 29991 11 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+310.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 30991 11 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+320.013 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 31991 11 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+330.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 32991 11 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223580 1075349796 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+340.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 33991 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+350.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 34991 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+360.015 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 35991 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+370.014 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 36991 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223768 134560553 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+380.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 37991 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+390.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 38992 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+400.016 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 39992 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+410.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 40992 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223824 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+420.018 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 41992 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+430.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 42992 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+440.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 43993 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+450.019 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 44993 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+460.02 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 45993 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+470.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 46993 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+480.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 47993 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+490.021 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 48994 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+500.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 49994 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+510.022 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3360 0 0 0 50994 12 0 0 25 0 1 0 488152266 15368192 3338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3338 603 41 0 3711 0 vsize: 15008 [startup+520.023 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3361 0 0 0 51994 12 0 0 25 0 1 0 488152266 15368192 3339 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3339 603 41 0 3711 0 vsize: 15008 [startup+530.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3361 0 0 0 52994 12 0 0 25 0 1 0 488152266 15368192 3339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3339 603 41 0 3711 0 vsize: 15008 [startup+540.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3361 0 0 0 53995 12 0 0 25 0 1 0 488152266 15368192 3339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3339 603 41 0 3711 0 vsize: 15008 [startup+550.024 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 54995 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+560.025 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 55995 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223924 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+570.026 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 56995 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+580.027 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 57995 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223728 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+590.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 58995 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223728 134559838 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+600.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 59995 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223728 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+610.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 60995 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+620.028 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 61995 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+630.029 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 62995 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+640.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 63995 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+650.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 64996 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+660.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 65996 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+670.03 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 66996 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223760 134560661 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+680.031 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 67996 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+690.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 68997 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+700.032 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 69997 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+710.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3362 0 0 0 70997 12 0 0 25 0 1 0 488152266 15368192 3340 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3340 603 41 0 3711 0 vsize: 15008 [startup+720.033 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3363 0 0 0 71997 12 0 0 25 0 1 0 488152266 15368192 3341 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3341 603 41 0 3711 0 vsize: 15008 [startup+730.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3363 0 0 0 72997 12 0 0 25 0 1 0 488152266 15368192 3341 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3341 603 41 0 3711 0 vsize: 15008 [startup+740.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3363 0 0 0 73998 12 0 0 25 0 1 0 488152266 15368192 3341 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3341 603 41 0 3711 0 vsize: 15008 [startup+750.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3363 0 0 0 74998 12 0 0 25 0 1 0 488152266 15368192 3341 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3341 603 41 0 3711 0 vsize: 15008 [startup+760.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3365 0 0 0 75998 12 0 0 25 0 1 0 488152266 15368192 3343 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3343 603 41 0 3711 0 vsize: 15008 [startup+770.035 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3365 0 0 0 76998 12 0 0 25 0 1 0 488152266 15368192 3343 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3343 603 41 0 3711 0 vsize: 15008 [startup+780.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3365 0 0 0 77998 12 0 0 25 0 1 0 488152266 15368192 3343 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3752 3343 603 41 0 3711 0 vsize: 15008 [startup+790.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3642 0 0 0 78997 13 0 0 25 0 1 0 488152266 16572416 3620 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4046 3620 603 41 0 4005 0 vsize: 16184 [startup+800.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3672 0 0 0 79997 13 0 0 25 0 1 0 488152266 16707584 3650 4294967295 134512640 134672761 3221224624 3221223808 134559334 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4079 3650 603 41 0 4038 0 vsize: 16316 [startup+810.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3679 0 0 0 80997 13 0 0 25 0 1 0 488152266 16707584 3657 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4079 3657 603 41 0 4038 0 vsize: 16316 [startup+820.036 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3689 0 0 0 81998 13 0 0 25 0 1 0 488152266 16707584 3667 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4079 3667 603 41 0 4038 0 vsize: 16316 [startup+830.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3692 0 0 0 82998 13 0 0 25 0 1 0 488152266 16707584 3670 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4079 3670 603 41 0 4038 0 vsize: 16316 [startup+840.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3692 0 0 0 83998 13 0 0 25 0 1 0 488152266 16707584 3670 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4079 3670 603 41 0 4038 0 vsize: 16316 [startup+850.037 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3692 0 0 0 84998 13 0 0 25 0 1 0 488152266 16707584 3670 4294967295 134512640 134672761 3221224624 3221223792 134561136 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4079 3670 603 41 0 4038 0 vsize: 16316 [startup+860.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3692 0 0 0 85997 14 0 0 25 0 1 0 488152266 16707584 3670 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4079 3670 603 41 0 4038 0 vsize: 16316 [startup+870.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3692 0 0 0 86997 14 0 0 25 0 1 0 488152266 16707584 3670 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4079 3670 603 41 0 4038 0 vsize: 16316 [startup+880.038 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3740 0 0 0 87997 14 0 0 25 0 1 0 488152266 17108992 3718 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4177 3718 603 41 0 4136 0 vsize: 16708 [startup+890.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3744 0 0 0 88998 14 0 0 25 0 1 0 488152266 17108992 3722 4294967295 134512640 134672761 3221224624 3221223792 134560888 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4177 3722 603 41 0 4136 0 vsize: 16708 [startup+900.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3755 0 0 0 89998 14 0 0 25 0 1 0 488152266 17108992 3733 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4177 3733 603 41 0 4136 0 vsize: 16708 [startup+910.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 3982 0 0 0 90997 15 0 0 25 0 1 0 488152266 18038784 3960 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4404 3960 603 41 0 4363 0 vsize: 17616 [startup+920.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4076 0 0 0 91997 15 0 0 25 0 1 0 488152266 18440192 4054 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4502 4054 603 41 0 4461 0 vsize: 18008 [startup+930.039 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4093 0 0 0 92997 15 0 0 25 0 1 0 488152266 18575360 4071 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4535 4071 603 41 0 4494 0 vsize: 18140 [startup+940.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4100 0 0 0 93997 15 0 0 25 0 1 0 488152266 18575360 4078 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4535 4078 603 41 0 4494 0 vsize: 18140 [startup+950.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4107 0 0 0 94997 15 0 0 25 0 1 0 488152266 18575360 4085 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4535 4085 603 41 0 4494 0 vsize: 18140 [startup+960.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4194 0 0 0 95997 16 0 0 25 0 1 0 488152266 18972672 4172 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4632 4172 603 41 0 4591 0 vsize: 18528 [startup+970.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4200 0 0 0 96997 16 0 0 25 0 1 0 488152266 18972672 4178 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4632 4178 603 41 0 4591 0 vsize: 18528 [startup+980.041 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4213 0 0 0 97998 16 0 0 25 0 1 0 488152266 19128320 4191 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4670 4191 603 41 0 4629 0 vsize: 18680 [startup+990.042 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4220 0 0 0 98998 16 0 0 25 0 1 0 488152266 19128320 4198 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4670 4198 603 41 0 4629 0 vsize: 18680 [startup+1000.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4245 0 0 0 99998 16 0 0 25 0 1 0 488152266 19128320 4223 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4670 4223 603 41 0 4629 0 vsize: 18680 [startup+1010.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4245 0 0 0 100998 16 0 0 25 0 1 0 488152266 19128320 4223 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4670 4223 603 41 0 4629 0 vsize: 18680 [startup+1020.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4255 0 0 0 101998 16 0 0 25 0 1 0 488152266 19271680 4233 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4705 4233 603 41 0 4664 0 vsize: 18820 [startup+1030.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4257 0 0 0 102999 16 0 0 25 0 1 0 488152266 19271680 4235 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4705 4235 603 41 0 4664 0 vsize: 18820 [startup+1040.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4335 0 0 0 103999 16 0 0 25 0 1 0 488152266 19533824 4313 4294967295 134512640 134672761 3221224624 3221223776 134565153 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4769 4313 603 41 0 4728 0 vsize: 19076 [startup+1050.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4335 0 0 0 104998 16 0 0 25 0 1 0 488152266 19533824 4313 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4769 4313 603 41 0 4728 0 vsize: 19076 [startup+1060.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4338 0 0 0 105998 16 0 0 25 0 1 0 488152266 19533824 4316 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4769 4316 603 41 0 4728 0 vsize: 19076 [startup+1070.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4340 0 0 0 106998 16 0 0 25 0 1 0 488152266 19533824 4318 4294967295 134512640 134672761 3221224624 3221223824 134557811 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4769 4318 603 41 0 4728 0 vsize: 19076 [startup+1080.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4479 0 0 0 107998 16 0 0 25 0 1 0 488152266 20201472 4457 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4932 4457 603 41 0 4891 0 vsize: 19728 [startup+1090.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4479 0 0 0 108998 16 0 0 25 0 1 0 488152266 20201472 4457 4294967295 134512640 134672761 3221224624 3221223840 134558181 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4932 4457 603 41 0 4891 0 vsize: 19728 [startup+1100.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4481 0 0 0 109998 16 0 0 25 0 1 0 488152266 20201472 4459 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4932 4459 603 41 0 4891 0 vsize: 19728 [startup+1110.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4482 0 0 0 110999 16 0 0 25 0 1 0 488152266 20201472 4460 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4932 4460 603 41 0 4891 0 vsize: 19728 [startup+1120.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4485 0 0 0 111999 16 0 0 25 0 1 0 488152266 20201472 4463 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4932 4463 603 41 0 4891 0 vsize: 19728 [startup+1130.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4485 0 0 0 112999 16 0 0 25 0 1 0 488152266 20201472 4463 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4932 4463 603 41 0 4891 0 vsize: 19728 [startup+1140.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4485 0 0 0 113999 16 0 0 25 0 1 0 488152266 20201472 4463 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4932 4463 603 41 0 4891 0 vsize: 19728 [startup+1150.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4485 0 0 0 114999 16 0 0 25 0 1 0 488152266 20201472 4463 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4932 4463 603 41 0 4891 0 vsize: 19728 [startup+1160.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4496 0 0 0 115999 16 0 0 25 0 1 0 488152266 20201472 4474 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4932 4474 603 41 0 4891 0 vsize: 19728 [startup+1170.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4497 0 0 0 116999 16 0 0 25 0 1 0 488152266 20201472 4475 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4932 4475 603 41 0 4891 0 vsize: 19728 [startup+1180.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4497 0 0 0 118000 16 0 0 25 0 1 0 488152266 20201472 4475 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4932 4475 603 41 0 4891 0 vsize: 19728 [startup+1190.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4518 0 0 0 119000 16 0 0 25 0 1 0 488152266 20340736 4496 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4966 4496 603 41 0 4925 0 vsize: 19864 [startup+1200.04 s] Raw data (loadavg): 0.99 0.97 0.98 2/54 10352 Raw data (stat): 10350 (minisat+) R 10349 5897 5896 0 -1 0 4519 0 0 0 120000 16 0 0 25 0 1 0 488152266 20340736 4497 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4966 4497 603 41 0 4925 0 vsize: 19864 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.06 s] Raw data (loadavg): 0.99 0.97 0.98 1/54 10352 Raw data (stat): 10350 (minisat+) Z 10349 5897 5896 0 -1 12 4522 0 0 0 120000 17 0 0 25 0 1 0 488152266 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.05 CPU time (s): 1200.18 CPU user time (s): 1200.01 CPU system time (s): 0.176973 CPU usage (%): 100.011 Max. virtual memory (Kb): 19864 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####