Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-neos5.opb |
MD5SUM | e6bff154156b54af3a9a38f7579209b6 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 17324 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 163 |
Biggest coefficient in the objective function | 1024 |
Number of bits for the biggest coefficient in the objective function | 11 |
Sum of the numbers in the objective function | 74742 |
Number of bits of the sum of numbers in the objective function | 17 |
Biggest number in a constraint | 8192 |
Number of bits of the biggest number in a constraint | 14 |
Biggest sum of numbers in a constraint | 74742 |
Number of bits of the biggest sum of numbers | 17 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.06984 |
Number of variables | 163 |
Total number of constraints | 126 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 56 |
Number of constraints which are nor clauses,nor cardinality constraints | 70 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 102 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc23 THE 2005-04-20 21:03:20 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=14713 boxname=wulflinc23 idbench=1132 idsolver=10 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: e6bff154156b54af3a9a38f7579209b6 /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-neos5.opb REAL COMMAND: minisat+ -ca /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-neos5.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-20-10-neos5.opb IDLAUNCH: 14713 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 3 cpu MHz : 451.037 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: 729828 kB Buffers: 31404 kB Cached: 236640 kB SwapCached: 624 kB Active: 17844 kB Inactive: 252424 kB HighTotal: 131008 kB HighFree: 40068 kB LowTotal: 903652 kB LowFree: 689760 kB SwapTotal: 2097136 kB SwapFree: 2095788 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5220 kB Slab: 28828 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-20 21:23:22 (client local time) WITH STATUS 10 IN 1200.22 SECONDS stats: 14713 7 1200.22 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 73 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 72]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 71]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 70]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 69]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 68]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 67]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 66]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 65]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 64]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 63]---> Adder-cost: 20 maxlim: 1022 bits: 11/10 c ---[ 62]---> Adder-cost: 59 maxlim: 7 bits: 4/3 c ---[ 61]---> Adder-cost: 117 maxlim: 7167 bits: 14/13 c ---[ 60]---> Adder-cost: 45 maxlim: 7167 bits: 14/13 c ---[ 59]---> Adder-cost: 149 maxlim: 7167 bits: 14/13 c ---[ 58]---> Adder-cost: 137 maxlim: 7167 bits: 14/13 c ---[ 57]---> Adder-cost: 47 maxlim: 7167 bits: 14/13 c ---[ 56]---> Adder-cost: 143 maxlim: 7167 bits: 14/13 c ---[ 55]---> Adder-cost: 135 maxlim: 7167 bits: 14/13 c ---[ 54]---> Adder-cost: 139 maxlim: 7167 bits: 14/13 c ---[ 53]---> Adder-cost: 49 maxlim: 7167 bits: 14/13 c ---[ 52]---> Adder-cost: 149 maxlim: 7167 bits: 14/13 c ---[ 51]---> Adder-cost: 43 maxlim: 7 bits: 4/3 c ---[ 50]---> Adder-cost: 135 maxlim: 7167 bits: 14/13 c ---[ 49]---> Adder-cost: 159 maxlim: 7167 bits: 14/13 c ---[ 48]---> Adder-cost: 69 maxlim: 6143 bits: 14/13 c ---[ 47]---> Adder-cost: 39 maxlim: 6143 bits: 14/13 c ---[ 46]---> Adder-cost: 39 maxlim: 6143 bits: 14/13 c ---[ 45]---> Adder-cost: 41 maxlim: 6143 bits: 14/13 c ---[ 44]---> Adder-cost: 39 maxlim: 6143 bits: 14/13 c ---[ 43]---> Adder-cost: 35 maxlim: 6143 bits: 14/13 c ---[ 42]---> Adder-cost: 37 maxlim: 6143 bits: 14/13 c ---[ 41]---> Adder-cost: 39 maxlim: 6143 bits: 14/13 c ---[ 40]---> Adder-cost: 39 maxlim: 8191 bits: 14/13 c ---[ 39]---> Adder-cost: 39 maxlim: 6143 bits: 14/13 c ---[ 38]---> Adder-cost: 145 maxlim: 6143 bits: 14/13 c ---[ 37]---> Adder-cost: 39 maxlim: 6143 bits: 14/13 c ---[ 36]---> Adder-cost: 35 maxlim: 6143 bits: 14/13 c ---[ 35]---> Adder-cost: 37 maxlim: 6143 bits: 14/13 c ---[ 34]---> Adder-cost: 39 maxlim: 6143 bits: 14/13 c ---[ 33]---> Adder-cost: 39 maxlim: 6143 bits: 14/13 c ---[ 32]---> Adder-cost: 145 maxlim: 6143 bits: 14/13 c ---[ 31]---> Adder-cost: 47 maxlim: 6143 bits: 14/13 c ---[ 30]---> Adder-cost: 43 maxlim: 6143 bits: 14/13 c ---[ 29]---> Adder-cost: 33 maxlim: 8191 bits: 14/13 c ---[ 28]---> Adder-cost: 129 maxlim: 6143 bits: 14/13 c ---[ 27]---> Adder-cost: 155 maxlim: 6143 bits: 14/13 c ---[ 26]---> Adder-cost: 33 maxlim: 5119 bits: 14/13 c ---[ 25]---> Adder-cost: 33 maxlim: 5119 bits: 14/13 c ---[ 24]---> Adder-cost: 33 maxlim: 5119 bits: 14/13 c ---[ 23]---> Adder-cost: 35 maxlim: 5119 bits: 14/13 c ---[ 22]---> Adder-cost: 35 maxlim: 5119 bits: 14/13 c ---[ 21]---> Adder-cost: 33 maxlim: 5119 bits: 14/13 c ---[ 20]---> Adder-cost: 33 maxlim: 5119 bits: 14/13 c ---[ 19]---> Adder-cost: 35 maxlim: 5119 bits: 14/13 c ---[ 18]---> Adder-cost: 33 maxlim: 8191 bits: 14/13 c ---[ 17]---> Adder-cost: 35 maxlim: 5119 bits: 14/13 c ---[ 16]---> Adder-cost: 35 maxlim: 5119 bits: 14/13 c ---[ 15]---> Adder-cost: 33 maxlim: 5119 bits: 14/13 c ---[ 14]---> Adder-cost: 37 maxlim: 5119 bits: 14/13 c ---[ 13]---> Adder-cost: 41 maxlim: 5119 bits: 14/13 c ---[ 12]---> Adder-cost: 37 maxlim: 5119 bits: 14/13 c ---[ 11]---> Adder-cost: 123 maxlim: 5119 bits: 14/13 c ---[ 10]---> Adder-cost: 30 maxlim: 4095 bits: 13/12 c ---[ 9]---> Adder-cost: 30 maxlim: 4095 bits: 13/12 c ---[ 8]---> Adder-cost: 30 maxlim: 4095 bits: 13/12 c ---[ 7]---> Adder-cost: 33 maxlim: 8191 bits: 14/13 c ---[ 6]---> Adder-cost: 30 maxlim: 4095 bits: 13/12 c ---[ 5]---> Adder-cost: 30 maxlim: 4095 bits: 13/12 c ---[ 4]---> Adder-cost: 34 maxlim: 4095 bits: 13/12 c ---[ 3]---> Adder-cost: 30 maxlim: 3071 bits: 13/12 c ---[ 2]---> Adder-cost: 39 maxlim: 6 bits: 4/3 c ---[ 1]---> Adder-cost: 39 maxlim: 7167 bits: 14/13 c ---[ 0]---> Adder-cost: 33 maxlim: 7167 bits: 14/13 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 23390 83389 | 7796 0 0 nan | 0.000 % | c | 100 | 23390 83389 | 8575 100 541 5.4 | 5.682 % | c | 250 | 23390 83389 | 9433 250 1369 5.5 | 5.682 % | c ============================================================================== c [1mFound solution: 21746[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 210 maxlim: 52996 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 436 | 24791 88389 | 8263 436 4122 9.5 | 5.682 % | c ============================================================================== c [1mFound solution: 21739[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 53003 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 485 | 24795 88426 | 8265 485 4472 9.2 | 5.682 % | c | 586 | 24795 88426 | 9091 586 5232 8.9 | 5.624 % | c | 736 | 24795 88426 | 10000 736 5900 8.0 | 5.624 % | c | 961 | 24789 88409 | 11000 960 7458 7.8 | 5.647 % | c ============================================================================== c [1mFound solution: 19959[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 54783 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1102 | 24794 88438 | 8264 1101 8253 7.5 | 5.647 % | c | 1204 | 24794 88438 | 9090 1203 9076 7.5 | 5.714 % | c | 1354 | 24794 88438 | 9999 1353 9826 7.3 | 5.714 % | c | 1579 | 24794 88438 | 10999 1578 13957 8.8 | 5.714 % | c | 1916 | 24794 88438 | 12099 1915 20125 10.5 | 5.714 % | c | 2422 | 24794 88438 | 13309 2421 27933 11.5 | 5.714 % | c ============================================================================== c [1mFound solution: 19831[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 54911 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2796 | 24795 88449 | 8265 2795 32600 11.7 | 5.714 % | c | 2896 | 24795 88449 | 9091 2895 33786 11.7 | 5.736 % | c | 3046 | 24795 88449 | 10000 3045 35261 11.6 | 5.736 % | c | 3271 | 24795 88449 | 11000 3270 37236 11.4 | 5.736 % | c | 3608 | 24795 88449 | 12100 3607 41950 11.6 | 5.736 % | c | 4115 | 24795 88449 | 13310 4114 47443 11.5 | 5.736 % | c | 4874 | 24795 88449 | 14641 4873 54952 11.3 | 5.736 % | c ============================================================================== c [1mFound solution: 19799[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 54943 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5556 | 24800 88478 | 8266 5555 61222 11.0 | 5.736 % | c | 5656 | 24800 88478 | 9092 5655 62141 11.0 | 5.758 % | c | 5807 | 24800 88478 | 10001 5806 64089 11.0 | 5.758 % | c ============================================================================== c [1mFound solution: 19719[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 55023 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 5953 | 24811 88549 | 8270 5952 66546 11.2 | 5.758 % | c | 6054 | 24811 88549 | 9097 6053 67832 11.2 | 5.824 % | c | 6204 | 24811 88549 | 10006 6203 70149 11.3 | 5.824 % | c | 6430 | 24811 88549 | 11007 6429 75307 11.7 | 5.824 % | c | 6767 | 24811 88549 | 12108 6766 83493 12.3 | 5.824 % | c ============================================================================== c [1mFound solution: 19191[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 55551 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7103 | 24813 88566 | 8271 7102 88458 12.5 | 5.824 % | c | 7204 | 24813 88566 | 9098 7203 89570 12.4 | 5.869 % | c | 7358 | 24813 88566 | 10007 7357 92116 12.5 | 5.869 % | c | 7583 | 24813 88566 | 11008 7582 95742 12.6 | 5.869 % | c | 7921 | 24813 88566 | 12109 7920 100029 12.6 | 5.869 % | c | 8427 | 24813 88566 | 13320 8426 108551 12.9 | 5.869 % | c ============================================================================== c [1mFound solution: 18935[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 55807 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8562 | 24814 88575 | 8271 8561 109895 12.8 | 5.869 % | c | 8662 | 24814 88575 | 9098 4381 54573 12.5 | 5.891 % | c | 8812 | 24814 88575 | 10007 4531 56370 12.4 | 5.891 % | c | 9038 | 24814 88575 | 11008 4757 59165 12.4 | 5.891 % | c | 9375 | 24814 88575 | 12109 5094 65812 12.9 | 5.891 % | c | 9881 | 24814 88575 | 13320 5600 75405 13.5 | 5.891 % | c ============================================================================== c [1mFound solution: 18679[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 56063 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 10435 | 24815 88585 | 8271 6154 85968 14.0 | 5.891 % | c | 10536 | 24815 88585 | 9098 6255 86750 13.9 | 5.913 % | c | 10686 | 24815 88585 | 10007 6405 89445 14.0 | 5.913 % | c | 10912 | 24815 88585 | 11008 6631 93048 14.0 | 5.913 % | c | 11252 | 24815 88585 | 12109 6971 100052 14.4 | 5.913 % | c | 11759 | 24815 88585 | 13320 7478 109101 14.6 | 5.913 % | c | 12518 | 24815 88585 | 14652 8237 138042 16.8 | 5.913 % | c | 13658 | 24815 88585 | 16117 9377 165001 17.6 | 5.913 % | c | 15366 | 24815 88585 | 17729 11085 209234 18.9 | 5.913 % | c | 17929 | 24815 88585 | 19502 13648 261170 19.1 | 5.913 % | c ============================================================================== c [1mFound solution: 18455[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 56287 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18851 | 24819 88623 | 8273 14570 278313 19.1 | 5.913 % | c | 18951 | 24819 88623 | 9100 7385 126364 17.1 | 5.978 % | c | 19101 | 24819 88623 | 10010 7535 127903 17.0 | 5.978 % | c | 19326 | 24819 88623 | 11011 7760 131002 16.9 | 5.978 % | c | 19663 | 24819 88623 | 12112 8097 134894 16.7 | 5.978 % | c ============================================================================== c [1mFound solution: 18359[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 56383 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20019 | 24821 88643 | 8273 8453 144428 17.1 | 5.978 % | c | 20119 | 24821 88643 | 9100 8553 144897 16.9 | 6.022 % | c | 20269 | 24821 88643 | 10010 8703 146260 16.8 | 6.022 % | c | 20494 | 24821 88643 | 11011 8928 150502 16.9 | 6.022 % | c | 20831 | 24821 88643 | 12112 9265 158022 17.1 | 6.022 % | c | 21337 | 24821 88643 | 13323 9771 163614 16.7 | 6.022 % | c | 22096 | 24821 88643 | 14656 10530 183015 17.4 | 6.022 % | c | 23236 | 24821 88643 | 16121 11670 205289 17.6 | 6.022 % | c ============================================================================== c [1mFound solution: 18332[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 56410 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23856 | 24833 88739 | 8277 12290 213724 17.4 | 6.022 % | c | 23956 | 24833 88739 | 9104 6245 89904 14.4 | 6.110 % | c | 24106 | 24833 88739 | 10015 6395 93025 14.5 | 6.110 % | c | 24333 | 24833 88739 | 11016 6622 96947 14.6 | 6.110 % | c ============================================================================== c [1mFound solution: 18167[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 56575 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 24528 | 24834 88749 | 8278 6817 99043 14.5 | 6.110 % | c | 24630 | 24834 88749 | 9105 6919 99959 14.4 | 6.132 % | c | 24780 | 24834 88749 | 10016 7069 101945 14.4 | 6.132 % | c | 25005 | 24834 88749 | 11018 7294 106146 14.6 | 6.132 % | c | 25342 | 24834 88749 | 12119 7631 112995 14.8 | 6.132 % | c | 25848 | 24834 88749 | 13331 8137 121460 14.9 | 6.132 % | c | 26609 | 24834 88749 | 14664 8898 141808 15.9 | 6.132 % | c | 27748 | 24834 88749 | 16131 10037 161084 16.0 | 6.132 % | c ============================================================================== c [1mFound solution: 17917[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 56825 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 28330 | 24844 88838 | 8281 10619 172982 16.3 | 6.132 % | c | 28431 | 24844 88838 | 9109 5411 78780 14.6 | 6.257 % | c | 28581 | 24844 88838 | 10020 5561 82574 14.8 | 6.257 % | c | 28806 | 24844 88838 | 11022 5786 87063 15.0 | 6.257 % | c | 29143 | 24844 88838 | 12124 6123 92543 15.1 | 6.257 % | c | 29651 | 24844 88838 | 13336 6631 101806 15.4 | 6.257 % | c | 30410 | 24844 88838 | 14670 7390 112879 15.3 | 6.257 % | c | 31550 | 24844 88838 | 16137 8530 142387 16.7 | 6.257 % | c ============================================================================== c [1mFound solution: 17913[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 56829 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 32529 | 24846 88871 | 8282 9509 166119 17.5 | 6.257 % | c | 32630 | 24846 88871 | 9110 4856 80160 16.5 | 6.301 % | c | 32780 | 24846 88871 | 10021 5006 83351 16.7 | 6.301 % | c | 33005 | 24846 88871 | 11023 5231 88003 16.8 | 6.301 % | c | 33342 | 24846 88871 | 12125 5568 94847 17.0 | 6.301 % | c | 33848 | 24846 88871 | 13338 6074 104092 17.1 | 6.301 % | c | 34607 | 24846 88871 | 14672 6833 120842 17.7 | 6.301 % | c | 35747 | 24846 88871 | 16139 7973 145655 18.3 | 6.301 % | c | 37455 | 24846 88871 | 17753 9681 182327 18.8 | 6.301 % | c ============================================================================== c [1mFound solution: 17271[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57471 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 39650 | 24852 88903 | 8284 11876 218984 18.4 | 6.301 % | c | 39750 | 24852 88903 | 9112 6038 88330 14.6 | 6.345 % | c | 39900 | 24852 88903 | 10023 6188 90952 14.7 | 6.345 % | c | 40125 | 24852 88903 | 11026 6413 93325 14.6 | 6.345 % | c | 40463 | 24852 88903 | 12128 6751 98785 14.6 | 6.345 % | c | 40969 | 24852 88903 | 13341 7257 105464 14.5 | 6.345 % | c | 41728 | 24852 88903 | 14675 8016 118322 14.8 | 6.345 % | c | 42869 | 24852 88903 | 16143 9157 136593 14.9 | 6.345 % | c | 44577 | 24852 88903 | 17757 10865 175522 16.2 | 6.345 % | c | 47140 | 24852 88903 | 19533 13428 239571 17.8 | 6.345 % | c | 50985 | 24852 88903 | 21486 17273 348444 20.2 | 6.345 % | c | 56751 | 24852 88903 | 23635 11890 300326 25.3 | 6.345 % | c | 65400 | 24852 88903 | 25998 20539 518023 25.2 | 6.345 % | c ============================================================================== c [1mFound solution: 17204[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57538 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 76212 | 24857 88954 | 8285 18110 454394 25.1 | 6.345 % | c | 76313 | 24857 88954 | 9113 4629 96775 20.9 | 6.407 % | c | 76465 | 24857 88954 | 10024 4781 98816 20.7 | 6.407 % | c | 76690 | 24857 88954 | 11027 5006 103711 20.7 | 6.407 % | c | 77027 | 24857 88954 | 12130 5343 108714 20.3 | 6.407 % | c | 77539 | 24857 88954 | 13343 5855 120234 20.5 | 6.407 % | c | 78301 | 24857 88954 | 14677 6617 136948 20.7 | 6.407 % | c | 79442 | 24857 88954 | 16145 7758 167151 21.5 | 6.407 % | c | 81152 | 24857 88954 | 17759 9468 206645 21.8 | 6.407 % | c | 83715 | 24857 88954 | 19535 12031 256487 21.3 | 6.407 % | c | 87560 | 24857 88954 | 21489 15876 373751 23.5 | 6.407 % | c ============================================================================== c [1mFound solution: 17142[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57600 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 88700 | 24860 88984 | 8286 17016 394608 23.2 | 6.407 % | c | 88800 | 24860 88984 | 9114 8608 183688 21.3 | 6.449 % | c | 88950 | 24860 88984 | 10026 8758 184742 21.1 | 6.449 % | c | 89175 | 24860 88984 | 11028 8983 186823 20.8 | 6.449 % | c | 89512 | 24860 88984 | 12131 9320 193969 20.8 | 6.449 % | c | 90018 | 24860 88984 | 13344 9826 205331 20.9 | 6.449 % | c | 90777 | 24860 88984 | 14679 10585 222963 21.1 | 6.449 % | c | 91916 | 24860 88984 | 16147 11724 252423 21.5 | 6.449 % | c | 93625 | 24860 88984 | 17761 13433 303817 22.6 | 6.449 % | c | 96188 | 24860 88984 | 19537 15996 371357 23.2 | 6.449 % | c ============================================================================== c [1mFound solution: 17125[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57617 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 99384 | 24863 89017 | 8287 19192 450034 23.4 | 6.449 % | c | 99485 | 24863 89017 | 9115 4899 85028 17.4 | 6.491 % | c | 99636 | 24863 89017 | 10027 5050 86142 17.1 | 6.491 % | c | 99861 | 24863 89017 | 11029 5275 90127 17.1 | 6.491 % | c | 100198 | 24863 89017 | 12132 5612 99494 17.7 | 6.491 % | c | 100705 | 24863 89017 | 13346 6119 106147 17.3 | 6.491 % | c | 101466 | 24863 89017 | 14680 6880 126147 18.3 | 6.491 % | c | 102606 | 24863 89017 | 16149 8020 159179 19.8 | 6.491 % | c | 104318 | 24863 89017 | 17763 9732 187115 19.2 | 6.491 % | c | 106884 | 24863 89017 | 19540 12298 239134 19.4 | 6.491 % | c | 110730 | 24863 89017 | 21494 16144 424818 26.3 | 6.491 % | c | 116496 | 24863 89017 | 23643 21910 626389 28.6 | 6.491 % | c | 125147 | 24863 89017 | 26008 17524 527205 30.1 | 6.491 % | c | 138121 | 24863 89017 | 28608 17226 490359 28.5 | 6.491 % | c ============================================================================== c [1mFound solution: 17121[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57621 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 143789 | 24865 89050 | 8288 22894 595118 26.0 | 6.491 % | c | 143890 | 24865 89050 | 9116 5825 88907 15.3 | 6.535 % | c | 144041 | 24865 89050 | 10028 5976 90664 15.2 | 6.535 % | c | 144266 | 24865 89050 | 11031 6201 94148 15.2 | 6.535 % | c | 144603 | 24865 89050 | 12134 6538 97272 14.9 | 6.535 % | c | 145109 | 24865 89050 | 13347 7044 106514 15.1 | 6.535 % | c | 145869 | 24865 89050 | 14682 7804 124531 16.0 | 6.535 % | c | 147010 | 24865 89050 | 16150 8945 155072 17.3 | 6.535 % | c | 148718 | 24865 89050 | 17766 10653 203081 19.1 | 6.535 % | c | 151281 | 24865 89050 | 19542 13216 269253 20.4 | 6.535 % | c | 155126 | 24865 89050 | 21496 17061 390811 22.9 | 6.535 % | c | 160892 | 24865 89050 | 23646 22827 547400 24.0 | 6.535 % | c | 169542 | 24865 89050 | 26011 19286 490721 25.4 | 6.535 % | c | 182518 | 24865 89050 | 28612 18805 436312 23.2 | 6.535 % | c | 201981 | 24865 89050 | 31473 22511 560953 24.9 | 6.535 % | c | 231174 | 24865 89050 | 34621 17632 438267 24.9 | 6.535 % | c ============================================================================== c [1mFound solution: 17091[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57651 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 247437 | 24869 89095 | 8289 33895 987918 29.1 | 6.535 % | c | 247539 | 24869 89095 | 9117 6494 211138 32.5 | 6.599 % | c | 247690 | 24869 89095 | 10029 6645 212239 31.9 | 6.599 % | c | 247915 | 24869 89095 | 11032 6870 214141 31.2 | 6.599 % | c | 248253 | 24869 89095 | 12135 7208 218503 30.3 | 6.599 % | c | 248762 | 24869 89095 | 13349 7717 226484 29.3 | 6.599 % | c | 249523 | 24869 89095 | 14684 8478 244923 28.9 | 6.599 % | c | 250662 | 24869 89095 | 16152 9617 283846 29.5 | 6.599 % | c | 252370 | 24869 89095 | 17768 11325 321131 28.4 | 6.599 % | c | 254932 | 24869 89095 | 19545 13887 368975 26.6 | 6.599 % | c | 258779 | 24869 89095 | 21499 17734 445164 25.1 | 6.599 % | c | 264546 | 24869 89095 | 23649 12033 304397 25.3 | 6.599 % | c | 273197 | 24869 89095 | 26014 20684 595235 28.8 | 6.599 % | c | 286171 | 24869 89095 | 28615 20399 485440 23.8 | 6.599 % | c | 305632 | 24869 89095 | 31477 24474 633640 25.9 | 6.599 % | c ============================================================================== c [1mFound solution: 17090[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57652 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 333039 | 24871 89115 | 8290 14577 451638 31.0 | 6.599 % | c | 333139 | 24871 89115 | 9119 7389 200076 27.1 | 6.619 % | c | 333290 | 24871 89115 | 10030 7540 201028 26.7 | 6.619 % | c | 333515 | 24871 89115 | 11033 7765 202356 26.1 | 6.619 % | c | 333853 | 24871 89115 | 12137 8103 207824 25.6 | 6.619 % | c | 334359 | 24871 89115 | 13351 8609 217248 25.2 | 6.619 % | c | 335119 | 24871 89115 | 14686 9369 229031 24.4 | 6.619 % | c | 336259 | 24871 89115 | 16154 10509 256751 24.4 | 6.619 % | c | 337967 | 24871 89115 | 17770 12217 288113 23.6 | 6.619 % | c | 340532 | 24871 89115 | 19547 14782 337067 22.8 | 6.619 % | c | 344376 | 24871 89115 | 21502 18626 441427 23.7 | 6.619 % | c | 350142 | 24871 89115 | 23652 13453 274565 20.4 | 6.619 % | c | 358793 | 24871 89115 | 26017 22104 466462 21.1 | 6.619 % | c ============================================================================== c [1mFound solution: 17089[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57653 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 364636 | 24873 89134 | 8291 27947 648026 23.2 | 6.619 % | c | 364736 | 24873 89134 | 9120 6907 151271 21.9 | 6.639 % | c | 364888 | 24873 89134 | 10032 7059 153816 21.8 | 6.639 % | c | 365113 | 24873 89134 | 11035 7284 157238 21.6 | 6.639 % | c | 365450 | 24873 89134 | 12138 7621 163712 21.5 | 6.639 % | c | 365956 | 24873 89134 | 13352 8127 172459 21.2 | 6.639 % | c | 366717 | 24873 89134 | 14688 8888 187776 21.1 | 6.639 % | c | 367858 | 24873 89134 | 16156 10029 205659 20.5 | 6.639 % | c | 369567 | 24873 89134 | 17772 11738 247420 21.1 | 6.639 % | c | 372129 | 24873 89134 | 19549 14300 368253 25.8 | 6.639 % | c | 375973 | 24873 89134 | 21504 18144 451052 24.9 | 6.639 % | c | 381740 | 24873 89134 | 23655 12537 291383 23.2 | 6.639 % | c | 390389 | 24873 89134 | 26020 21186 488660 23.1 | 6.639 % | c | 403364 | 24873 89134 | 28622 20716 837594 40.4 | 6.639 % | c | 422827 | 24873 89134 | 31485 25278 674336 26.7 | 6.639 % | c ============================================================================== c [1mFound solution: 17085[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57657 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 424389 | 24877 89168 | 8292 26840 714766 26.6 | 6.639 % | c | 424489 | 24877 89168 | 9121 6810 146243 21.5 | 6.679 % | c | 424640 | 24877 89168 | 10033 6961 147500 21.2 | 6.679 % | c | 424867 | 24877 89168 | 11036 7188 151912 21.1 | 6.679 % | c | 425206 | 24877 89168 | 12140 7527 158666 21.1 | 6.679 % | c | 425712 | 24877 89168 | 13354 8033 167334 20.8 | 6.679 % | c | 426471 | 24877 89168 | 14689 8792 183574 20.9 | 6.679 % | c | 427610 | 24877 89168 | 16158 9931 214917 21.6 | 6.679 % | c | 429319 | 24877 89168 | 17774 11640 262264 22.5 | 6.679 % | c | 431883 | 24877 89168 | 19552 14204 326420 23.0 | 6.679 % | c | 435728 | 24877 89168 | 21507 18049 432228 23.9 | 6.679 % | c | 441497 | 24877 89168 | 23658 12868 259428 20.2 | 6.679 % | c | 450147 | 24877 89168 | 26023 21518 533956 24.8 | 6.679 % | c | 463121 | 24877 89168 | 28626 21293 602071 28.3 | 6.679 % | c | 482582 | 24877 89168 | 31488 26239 669561 25.5 | 6.679 % | c | 511775 | 24877 89168 | 34637 22508 597606 26.6 | 6.679 % | c ============================================================================== c [1mFound solution: 17083[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57659 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 522333 | 24879 89186 | 8293 33066 866966 26.2 | 6.679 % | c | 522433 | 24879 89186 | 9122 7910 149325 18.9 | 6.699 % | c | 522583 | 24879 89186 | 10034 8060 150933 18.7 | 6.699 % | c | 522808 | 24879 89186 | 11037 8285 153460 18.5 | 6.699 % | c | 523146 | 24879 89186 | 12141 8623 162516 18.8 | 6.699 % | c | 523653 | 24879 89186 | 13355 9130 172851 18.9 | 6.699 % | c | 524412 | 24879 89186 | 14691 9889 190456 19.3 | 6.699 % | c | 525552 | 24879 89186 | 16160 11029 217008 19.7 | 6.699 % | c | 527261 | 24879 89186 | 17776 12738 258862 20.3 | 6.699 % | c | 529824 | 24879 89186 | 19554 15301 296567 19.4 | 6.699 % | c | 533668 | 24879 89186 | 21509 19145 391456 20.4 | 6.699 % | c | 539434 | 24879 89186 | 23660 13970 266613 19.1 | 6.699 % | c ============================================================================== c [1mFound solution: 17015[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57727 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 546598 | 24881 89199 | 8293 21134 550111 26.0 | 6.699 % | c | 546698 | 24881 89199 | 9122 5384 203523 37.8 | 6.719 % | c | 546850 | 24881 89199 | 10034 5536 204916 37.0 | 6.719 % | c | 547075 | 24881 89199 | 11037 5761 208875 36.3 | 6.719 % | c | 547413 | 24881 89199 | 12141 6099 218976 35.9 | 6.719 % | c | 547920 | 24881 89199 | 13355 6606 228977 34.7 | 6.719 % | c | 548681 | 24881 89199 | 14691 7367 245229 33.3 | 6.719 % | c | 549822 | 24881 89199 | 16160 8508 280336 32.9 | 6.719 % | c | 551531 | 24881 89199 | 17776 10217 334888 32.8 | 6.719 % | c | 554093 | 24881 89199 | 19554 12779 409396 32.0 | 6.719 % | c | 557940 | 24881 89199 | 21509 16626 492085 29.6 | 6.719 % | c | 563706 | 24881 89199 | 23660 22392 662019 29.6 | 6.719 % | c | 572355 | 24881 89199 | 26026 19026 425808 22.4 | 6.719 % | c | 585329 | 24881 89199 | 28629 18767 432475 23.0 | 6.719 % | c ============================================================================== c [1mFound solution: 16887[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57855 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 593106 | 24882 89208 | 8294 26544 906372 34.1 | 6.719 % | c | 593206 | 24882 89208 | 9123 6736 319448 47.4 | 6.741 % | c | 593356 | 24882 89208 | 10035 6886 320695 46.6 | 6.741 % | c | 593581 | 24882 89208 | 11039 7111 324843 45.7 | 6.741 % | c | 593918 | 24882 89208 | 12143 7448 330098 44.3 | 6.741 % | c | 594428 | 24882 89208 | 13357 7958 346574 43.6 | 6.741 % | c | 595187 | 24882 89208 | 14693 8717 357245 41.0 | 6.741 % | c | 596326 | 24882 89208 | 16162 9856 378092 38.4 | 6.741 % | c | 598037 | 24882 89208 | 17778 11567 414322 35.8 | 6.741 % | c | 600599 | 24882 89208 | 19556 14129 483921 34.3 | 6.741 % | c | 604444 | 24882 89208 | 21512 17974 588636 32.7 | 6.741 % | c | 610212 | 24882 89208 | 23663 12616 322111 25.5 | 6.741 % | c | 618861 | 24882 89208 | 26030 21265 606031 28.5 | 6.741 % | c | 631835 | 24882 89208 | 28633 21033 482428 22.9 | 6.741 % | c | 651297 | 24882 89208 | 31496 22898 569116 24.9 | 6.741 % | c | 680489 | 24882 89208 | 34646 17454 346528 19.9 | 6.741 % | c ============================================================================== c [1mFound solution: 16759[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 57983 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 702130 | 24884 89221 | 8294 16834 438653 26.1 | 6.741 % | c | 702230 | 24884 89221 | 9123 8517 142723 16.8 | 6.761 % | c | 702380 | 24884 89221 | 10035 8667 144024 16.6 | 6.761 % | c | 702606 | 24884 89221 | 11039 8893 147168 16.5 | 6.761 % | c | 702943 | 24884 89221 | 12143 9230 153328 16.6 | 6.761 % | c | 703450 | 24884 89221 | 13357 9737 162853 16.7 | 6.761 % | c | 704210 | 24884 89221 | 14693 10497 184967 17.6 | 6.761 % | c | 705350 | 24884 89221 | 16162 11637 222467 19.1 | 6.761 % | c | 707060 | 24884 89221 | 17778 13347 259550 19.4 | 6.761 % | c | 709622 | 24884 89221 | 19556 15909 357162 22.5 | 6.761 % | c | 713466 | 24884 89221 | 21512 19753 445850 22.6 | 6.761 % | c | 719233 | 24884 89221 | 23663 14588 384106 26.3 | 6.761 % | c ============================================================================== c [1mFound solution: 16736[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 58006 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 726077 | 24891 89289 | 8297 21432 541801 25.3 | 6.761 % | c | 726177 | 24891 89289 | 9126 5458 108805 19.9 | 6.842 % | c | 726327 | 24891 89289 | 10039 5608 110105 19.6 | 6.842 % | c | 726552 | 24891 89289 | 11043 5833 113039 19.4 | 6.842 % | c | 726889 | 24891 89289 | 12147 6170 116781 18.9 | 6.842 % | c | 727395 | 24891 89289 | 13362 6676 132285 19.8 | 6.842 % | c | 728155 | 24891 89289 | 14698 7436 149089 20.0 | 6.842 % | c | 729294 | 24891 89289 | 16168 8575 175924 20.5 | 6.842 % | c | 731002 | 24891 89289 | 17785 10283 210036 20.4 | 6.842 % | c | 733565 | 24891 89289 | 19563 12846 289575 22.5 | 6.842 % | c | 737412 | 24891 89289 | 21520 16693 508158 30.4 | 6.842 % | c | 743178 | 24891 89289 | 23672 22459 707643 31.5 | 6.842 % | c | 751830 | 24891 89289 | 26039 18851 580472 30.8 | 6.842 % | c | 764806 | 24891 89289 | 28643 18212 526917 28.9 | 6.842 % | c | 784267 | 24891 89289 | 31507 20718 1165349 56.2 | 6.842 % | c | 813459 | 24891 89289 | 34658 31761 836488 26.3 | 6.842 % | c | 857248 | 24891 89289 | 38124 17589 1078762 61.3 | 6.842 % | c ============================================================================== c [1mFound solution: 16631[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 58111 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 878969 | 24893 89301 | 8297 39310 2029149 51.6 | 6.842 % | c | 879071 | 24893 89301 | 9126 6870 237838 34.6 | 6.862 % | c | 879223 | 24893 89301 | 10039 7022 239518 34.1 | 6.862 % | c | 879448 | 24893 89301 | 11043 7247 241410 33.3 | 6.862 % | c | 879786 | 24893 89301 | 12147 7585 246653 32.5 | 6.862 % | c | 880293 | 24893 89301 | 13362 8092 254264 31.4 | 6.862 % | c | 881052 | 24893 89301 | 14698 8851 265179 30.0 | 6.862 % | c | 882192 | 24893 89301 | 16168 9991 291830 29.2 | 6.862 % | c | 883901 | 24893 89301 | 17785 11700 320027 27.4 | 6.862 % | c | 886463 | 24893 89301 | 19563 14262 376268 26.4 | 6.862 % | c | 890309 | 24893 89301 | 21520 18108 509243 28.1 | 6.862 % | c | 896076 | 24893 89301 | 23672 12865 379175 29.5 | 6.862 % | c | 904725 | 24893 89301 | 26039 21514 658359 30.6 | 6.862 % | c | 917699 | 24893 89301 | 28643 21236 698307 32.9 | 6.862 % | c | 937160 | 24893 89301 | 31507 25456 893995 35.1 | 6.862 % | c | 966352 | 24893 89301 | 34658 20076 455588 22.7 | 6.862 % | c | 1010141 | 24893 89301 | 38124 16897 791574 46.8 | 6.862 % | c | 1075825 | 24893 89301 | 41936 33154 1092614 33.0 | 6.862 % | c ============================================================================== c [1mFound solution: 16175[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 58567 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1109416 | 24900 89352 | 8300 37831 1224876 32.4 | 6.862 % | c | 1109516 | 24900 89352 | 9130 7899 206012 26.1 | 6.943 % | c | 1109666 | 24900 89352 | 10043 8049 207337 25.8 | 6.943 % | c | 1109891 | 24900 89352 | 11047 8274 211066 25.5 | 6.943 % | c | 1110228 | 24900 89352 | 12152 8611 216696 25.2 | 6.943 % | c | 1110734 | 24900 89352 | 13367 9117 222824 24.4 | 6.943 % | c | 1111496 | 24900 89352 | 14703 9879 245993 24.9 | 6.943 % | c | 1112636 | 24900 89352 | 16174 11019 278704 25.3 | 6.943 % | c | 1114345 | 24900 89352 | 17791 12728 311780 24.5 | 6.943 % | c | 1116907 | 24900 89352 | 19570 15290 412264 27.0 | 6.943 % | c | 1120755 | 24900 89352 | 21528 19138 579260 30.3 | 6.943 % | c | 1126522 | 24900 89352 | 23680 13912 426021 30.6 | 6.943 % | c | 1135171 | 24900 89352 | 26048 22561 744561 33.0 | 6.943 % | c | 1148148 | 24900 89352 | 28653 22292 695909 31.2 | 6.943 % | c | 1167609 | 24900 89352 | 31519 27213 1004697 36.9 | 6.943 % | c ============================================================================== c [1mFound solution: 16055[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Adder-cost: 0 maxlim: 58687 bits: 17/16 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1186420 | 24903 89376 | 8301 29533 976313 33.1 | 6.943 % | c | 1186520 | 24903 89376 | 9131 7484 165511 22.1 | 6.985 % | c | 1186670 | 24903 89376 | 10044 7634 167113 21.9 | 6.985 % | c | 1186895 | 24903 89376 | 11048 7859 169168 21.5 | 6.985 % | c | 1187232 | 24903 89376 | 12153 8196 173498 21.2 | 6.985 % | c | 1187738 | 24903 89376 | 13368 8702 182220 20.9 | 6.985 % | c | 1188499 | 24894 89345 | 14705 9443 205523 21.8 | 7.008 % | c | 1189642 | 24894 89345 | 16176 10586 235870 22.3 | 7.008 % | c | 1191350 | 24894 89345 | 17793 12294 279459 22.7 | 7.008 % | c | 1193912 | 24894 89345 | 19573 14856 363941 24.5 | 7.008 % | c | 1197758 | 24894 89345 | 21530 18702 489913 26.2 | 7.008 % | c | 1203524 | 24894 89345 | 23683 13448 395831 29.4 | 7.008 % | c | 1212175 | 24894 89345 | 26052 22099 643524 29.1 | 7.008 % | c | 1225149 | 24894 89345 | 28657 21704 610569 28.1 | 7.008 % | c | 1244612 | 24894 89345 | 31523 26110 743493 28.5 | 7.008 % | c | 1273805 | 24894 89345 | 34675 21089 886544 42.0 | 7.008 % | c | 1317594 | 24894 89345 | 38142 25351 619696 24.4 | 7.008 % | c | 1383278 | 24894 89345 | 41957 19013 1152392 60.6 | 7.008 % | #### 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.74 0.91 0.87 2/54 22135 Raw data (stat): 22135 (runsolver) R 22134 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539529099 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0009 s] Raw data (loadavg): 0.78 0.91 0.87 2/54 22135 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1281 0 0 0 994 4 0 0 25 0 1 0 539529099 7086080 1259 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1730 1259 603 41 0 1689 0 vsize: 6920 [startup+20.0015 s] Raw data (loadavg): 0.81 0.91 0.87 2/54 22135 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1329 0 0 0 1993 5 0 0 25 0 1 0 539529099 7221248 1307 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 1763 1307 603 41 0 1722 0 vsize: 7052 [startup+30.0068 s] Raw data (loadavg): 0.84 0.92 0.87 2/54 22135 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1678 0 0 0 2992 6 0 0 25 0 1 0 539529099 8740864 1656 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2134 1656 603 41 0 2093 0 vsize: 8536 [startup+40.0064 s] Raw data (loadavg): 0.87 0.92 0.87 2/54 22135 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1917 0 0 0 3991 8 0 0 25 0 1 0 539529099 9678848 1895 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2363 1895 603 41 0 2322 0 vsize: 9452 [startup+50.0074 s] Raw data (loadavg): 0.89 0.92 0.88 2/54 22135 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1917 0 0 0 4991 8 0 0 25 0 1 0 539529099 9678848 1895 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2363 1895 603 41 0 2322 0 vsize: 9452 [startup+60.008 s] Raw data (loadavg): 0.90 0.92 0.88 2/54 22135 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 1997 0 0 0 5990 9 0 0 25 0 1 0 539529099 10084352 1975 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2462 1975 603 41 0 2421 0 vsize: 9848 [startup+70.0082 s] Raw data (loadavg): 0.92 0.92 0.88 2/54 22135 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2143 0 0 0 6989 9 0 0 25 0 1 0 539529099 10629120 2121 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2595 2121 603 41 0 2554 0 vsize: 10380 [startup+80.0093 s] Raw data (loadavg): 0.93 0.93 0.88 2/54 22135 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2189 0 0 0 7988 10 0 0 25 0 1 0 539529099 10907648 2167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2663 2167 603 41 0 2622 0 vsize: 10652 [startup+90.0143 s] Raw data (loadavg): 0.94 0.93 0.88 2/54 22135 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2189 0 0 0 8988 10 0 0 25 0 1 0 539529099 10907648 2167 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2663 2167 603 41 0 2622 0 vsize: 10652 [startup+100.015 s] Raw data (loadavg): 0.95 0.93 0.88 2/54 22135 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2190 0 0 0 9988 11 0 0 25 0 1 0 539529099 10907648 2168 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2663 2168 603 41 0 2622 0 vsize: 10652 [startup+110.016 s] Raw data (loadavg): 0.96 0.93 0.88 2/54 22135 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2196 0 0 0 10988 11 0 0 25 0 1 0 539529099 10907648 2174 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2663 2174 603 41 0 2622 0 vsize: 10652 [startup+120.017 s] Raw data (loadavg): 0.96 0.93 0.88 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2243 0 0 0 11988 12 0 0 25 0 1 0 539529099 11055104 2221 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2699 2221 603 41 0 2658 0 vsize: 10796 [startup+130.017 s] Raw data (loadavg): 0.97 0.94 0.88 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2381 0 0 0 12987 13 0 0 25 0 1 0 539529099 11608064 2359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2834 2359 603 41 0 2793 0 vsize: 11336 [startup+140.017 s] Raw data (loadavg): 0.97 0.94 0.88 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2402 0 0 0 13987 13 0 0 25 0 1 0 539529099 11743232 2380 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2867 2380 603 41 0 2826 0 vsize: 11468 [startup+150.019 s] Raw data (loadavg): 0.98 0.94 0.89 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2434 0 0 0 14986 14 0 0 25 0 1 0 539529099 11882496 2412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2901 2412 603 41 0 2860 0 vsize: 11604 [startup+160.019 s] Raw data (loadavg): 0.98 0.94 0.89 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2457 0 0 0 15986 14 0 0 25 0 1 0 539529099 12029952 2435 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2937 2435 603 41 0 2896 0 vsize: 11748 [startup+170.019 s] Raw data (loadavg): 0.98 0.94 0.89 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2648 0 0 0 16985 15 0 0 25 0 1 0 539529099 12967936 2626 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3166 2626 603 41 0 3125 0 vsize: 12664 [startup+180.02 s] Raw data (loadavg): 0.98 0.94 0.89 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2648 0 0 0 17985 16 0 0 25 0 1 0 539529099 12967936 2626 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3166 2626 603 41 0 3125 0 vsize: 12664 [startup+190.02 s] Raw data (loadavg): 0.99 0.94 0.89 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2650 0 0 0 18985 16 0 0 25 0 1 0 539529099 12967936 2628 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3166 2628 603 41 0 3125 0 vsize: 12664 [startup+200.021 s] Raw data (loadavg): 0.99 0.95 0.89 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2652 0 0 0 19984 16 0 0 25 0 1 0 539529099 12967936 2630 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3166 2630 603 41 0 3125 0 vsize: 12664 [startup+210.022 s] Raw data (loadavg): 0.99 0.95 0.89 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2653 0 0 0 20984 17 0 0 25 0 1 0 539529099 12967936 2631 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3166 2631 603 41 0 3125 0 vsize: 12664 [startup+220.022 s] Raw data (loadavg): 0.99 0.95 0.89 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2654 0 0 0 21984 17 0 0 25 0 1 0 539529099 12967936 2632 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3166 2632 603 41 0 3125 0 vsize: 12664 [startup+230.03 s] Raw data (loadavg): 0.99 0.95 0.89 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2929 0 0 0 22984 18 0 0 25 0 1 0 539529099 14045184 2907 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3429 2907 603 41 0 3388 0 vsize: 13716 [startup+240.031 s] Raw data (loadavg): 0.99 0.95 0.89 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 23984 19 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3429 2915 603 41 0 3388 0 vsize: 13716 [startup+250.035 s] Raw data (loadavg): 0.99 0.95 0.89 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 24983 20 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3429 2915 603 41 0 3388 0 vsize: 13716 [startup+260.038 s] Raw data (loadavg): 0.99 0.95 0.90 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 25983 20 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223728 134559405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3429 2915 603 41 0 3388 0 vsize: 13716 [startup+270.038 s] Raw data (loadavg): 0.99 0.95 0.90 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 26983 20 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3429 2915 603 41 0 3388 0 vsize: 13716 [startup+280.038 s] Raw data (loadavg): 0.99 0.95 0.90 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 27983 20 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3429 2915 603 41 0 3388 0 vsize: 13716 [startup+290.039 s] Raw data (loadavg): 0.99 0.95 0.90 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2937 0 0 0 28982 21 0 0 25 0 1 0 539529099 14045184 2915 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3429 2915 603 41 0 3388 0 vsize: 13716 [startup+300.04 s] Raw data (loadavg): 0.99 0.96 0.90 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2950 0 0 0 29982 22 0 0 25 0 1 0 539529099 14184448 2928 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3463 2928 603 41 0 3422 0 vsize: 13852 [startup+310.04 s] Raw data (loadavg): 0.99 0.96 0.90 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2950 0 0 0 30982 22 0 0 25 0 1 0 539529099 14184448 2928 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3463 2928 603 41 0 3422 0 vsize: 13852 [startup+320.04 s] Raw data (loadavg): 0.99 0.96 0.90 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2971 0 0 0 31981 22 0 0 25 0 1 0 539529099 14184448 2949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3463 2949 603 41 0 3422 0 vsize: 13852 [startup+330.041 s] Raw data (loadavg): 0.99 0.96 0.90 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2978 0 0 0 32981 22 0 0 25 0 1 0 539529099 14331904 2956 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3499 2956 603 41 0 3458 0 vsize: 13996 [startup+340.058 s] Raw data (loadavg): 0.99 0.96 0.90 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 2994 0 0 0 33983 23 0 0 25 0 1 0 539529099 14331904 2972 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3499 2972 603 41 0 3458 0 vsize: 13996 [startup+350.059 s] Raw data (loadavg): 0.99 0.96 0.90 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3001 0 0 0 34982 23 0 0 25 0 1 0 539529099 14331904 2979 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3499 2979 603 41 0 3458 0 vsize: 13996 [startup+360.059 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3020 0 0 0 35982 24 0 0 25 0 1 0 539529099 14495744 2998 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3539 2998 603 41 0 3498 0 vsize: 14156 [startup+370.059 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3020 0 0 0 36982 24 0 0 25 0 1 0 539529099 14495744 2998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3539 2998 603 41 0 3498 0 vsize: 14156 [startup+380.06 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 37981 25 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3579 3026 603 41 0 3538 0 vsize: 14316 [startup+390.06 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 38981 26 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3579 3026 603 41 0 3538 0 vsize: 14316 [startup+400.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 39981 26 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3579 3026 603 41 0 3538 0 vsize: 14316 [startup+410.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 40981 26 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3579 3026 603 41 0 3538 0 vsize: 14316 [startup+420.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 41981 26 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3579 3026 603 41 0 3538 0 vsize: 14316 [startup+430.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3048 0 0 0 42981 26 0 0 25 0 1 0 539529099 14659584 3026 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3579 3026 603 41 0 3538 0 vsize: 14316 [startup+440.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3054 0 0 0 43982 26 0 0 25 0 1 0 539529099 14659584 3032 4294967295 134512640 134672761 3221224544 3221223728 134558645 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3579 3032 603 41 0 3538 0 vsize: 14316 [startup+450.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3054 0 0 0 44982 26 0 0 25 0 1 0 539529099 14659584 3032 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3579 3032 603 41 0 3538 0 vsize: 14316 [startup+460.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3054 0 0 0 45982 26 0 0 25 0 1 0 539529099 14659584 3032 4294967295 134512640 134672761 3221224544 3221223648 134554677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3579 3032 603 41 0 3538 0 vsize: 14316 [startup+470.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3058 0 0 0 46982 26 0 0 25 0 1 0 539529099 14659584 3036 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3579 3036 603 41 0 3538 0 vsize: 14316 [startup+480.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3070 0 0 0 47982 26 0 0 25 0 1 0 539529099 14823424 3048 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3619 3048 603 41 0 3578 0 vsize: 14476 [startup+490.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3125 0 0 0 48983 26 0 0 25 0 1 0 539529099 14958592 3103 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3652 3103 603 41 0 3611 0 vsize: 14608 [startup+500.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3125 0 0 0 49983 26 0 0 25 0 1 0 539529099 14958592 3103 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3652 3103 603 41 0 3611 0 vsize: 14608 [startup+510.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3126 0 0 0 50984 26 0 0 25 0 1 0 539529099 14958592 3104 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3652 3104 603 41 0 3611 0 vsize: 14608 [startup+520.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3126 0 0 0 51985 26 0 0 25 0 1 0 539529099 14958592 3104 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3652 3104 603 41 0 3611 0 vsize: 14608 [startup+530.082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3126 0 0 0 52983 26 0 0 25 0 1 0 539529099 14958592 3104 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3652 3104 603 41 0 3611 0 vsize: 14608 [startup+540.09 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3328 0 0 0 53983 27 0 0 25 0 1 0 539529099 15769600 3306 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3850 3306 603 41 0 3809 0 vsize: 15400 [startup+550.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3670 0 0 0 54983 28 0 0 25 0 1 0 539529099 17248256 3648 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4211 3648 603 41 0 4170 0 vsize: 16844 [startup+560.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3711 0 0 0 55983 28 0 0 25 0 1 0 539529099 17383424 3689 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4244 3689 603 41 0 4203 0 vsize: 16976 [startup+570.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3711 0 0 0 56972 29 0 0 25 0 1 0 539529099 17383424 3689 4294967295 134512640 134672761 3221224544 3221223728 134559334 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4244 3689 603 41 0 4203 0 vsize: 16976 [startup+580.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3711 0 0 0 57972 29 0 0 25 0 1 0 539529099 17383424 3689 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4244 3689 603 41 0 4203 0 vsize: 16976 [startup+590.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3716 0 0 0 58973 29 0 0 25 0 1 0 539529099 17383424 3694 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4244 3694 603 41 0 4203 0 vsize: 16976 [startup+600.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 3717 0 0 0 59972 29 0 0 25 0 1 0 539529099 17383424 3695 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4244 3695 603 41 0 4203 0 vsize: 16976 [startup+610.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4248 0 0 0 60971 31 0 0 25 0 1 0 539529099 19652608 4226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4798 4226 603 41 0 4757 0 vsize: 19192 [startup+620.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4492 0 0 0 61970 32 0 0 25 0 1 0 539529099 20611072 4470 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4470 603 41 0 4991 0 vsize: 20128 [startup+630.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4492 0 0 0 62970 32 0 0 25 0 1 0 539529099 20611072 4470 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4470 603 41 0 4991 0 vsize: 20128 [startup+640.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4507 0 0 0 63970 32 0 0 25 0 1 0 539529099 20611072 4485 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4485 603 41 0 4991 0 vsize: 20128 [startup+650.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4507 0 0 0 64970 32 0 0 25 0 1 0 539529099 20611072 4485 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4485 603 41 0 4991 0 vsize: 20128 [startup+660.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4507 0 0 0 65970 32 0 0 25 0 1 0 539529099 20611072 4485 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4485 603 41 0 4991 0 vsize: 20128 [startup+670.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4507 0 0 0 66970 32 0 0 25 0 1 0 539529099 20611072 4485 4294967295 134512640 134672761 3221224544 3221223136 134565829 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4485 603 41 0 4991 0 vsize: 20128 [startup+680.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4507 0 0 0 67970 32 0 0 25 0 1 0 539529099 20611072 4485 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4485 603 41 0 4991 0 vsize: 20128 [startup+690.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4510 0 0 0 68971 32 0 0 25 0 1 0 539529099 20611072 4488 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4488 603 41 0 4991 0 vsize: 20128 [startup+700.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 69971 32 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4489 603 41 0 4991 0 vsize: 20128 [startup+710.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 70971 32 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4489 603 41 0 4991 0 vsize: 20128 [startup+720.093 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 71971 32 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5032 4489 603 41 0 4991 0 vsize: 20128 [startup+730.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 72971 33 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4489 603 41 0 4991 0 vsize: 20128 [startup+740.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 73971 33 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4489 603 41 0 4991 0 vsize: 20128 [startup+750.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 74961 33 0 0 24 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4489 603 41 0 4991 0 vsize: 20128 [startup+760.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4511 0 0 0 75961 33 0 0 25 0 1 0 539529099 20611072 4489 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4489 603 41 0 4991 0 vsize: 20128 [startup+770.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4512 0 0 0 76961 33 0 0 25 0 1 0 539529099 20611072 4490 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4490 603 41 0 4991 0 vsize: 20128 [startup+780.095 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4512 0 0 0 77961 33 0 0 25 0 1 0 539529099 20611072 4490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4490 603 41 0 4991 0 vsize: 20128 [startup+790.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4512 0 0 0 78961 33 0 0 25 0 1 0 539529099 20611072 4490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4490 603 41 0 4991 0 vsize: 20128 [startup+800.094 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4512 0 0 0 79961 33 0 0 25 0 1 0 539529099 20611072 4490 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4490 603 41 0 4991 0 vsize: 20128 [startup+810.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4514 0 0 0 80962 33 0 0 25 0 1 0 539529099 20611072 4492 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4492 603 41 0 4991 0 vsize: 20128 [startup+820.098 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4514 0 0 0 81962 33 0 0 25 0 1 0 539529099 20611072 4492 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4492 603 41 0 4991 0 vsize: 20128 [startup+830.099 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4514 0 0 0 82962 33 0 0 25 0 1 0 539529099 20611072 4492 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4492 603 41 0 4991 0 vsize: 20128 [startup+840.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 83964 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+850.108 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 84963 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+860.107 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 85963 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+870.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 86964 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+880.109 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 87964 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+890.111 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 88964 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+900.217 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 89973 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+910.217 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 90973 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+920.216 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 91973 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+930.217 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 92973 33 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+940.218 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 93973 34 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+950.217 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 94974 34 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+960.218 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 95974 34 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+970.225 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4517 0 0 0 96975 34 0 0 25 0 1 0 539529099 20611072 4495 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4495 603 41 0 4991 0 vsize: 20128 [startup+980.226 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 97975 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4496 603 41 0 4991 0 vsize: 20128 [startup+990.249 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 98977 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4496 603 41 0 4991 0 vsize: 20128 [startup+1000.25 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 99977 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223728 134559332 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4496 603 41 0 4991 0 vsize: 20128 [startup+1010.25 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 100977 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4496 603 41 0 4991 0 vsize: 20128 [startup+1020.26 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 101978 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4496 603 41 0 4991 0 vsize: 20128 [startup+1030.26 s] Raw data (loadavg): 1.12 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 102978 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4496 603 41 0 4991 0 vsize: 20128 [startup+1040.28 s] Raw data (loadavg): 1.10 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 103979 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4496 603 41 0 4991 0 vsize: 20128 [startup+1050.29 s] Raw data (loadavg): 1.08 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4518 0 0 0 104981 34 0 0 25 0 1 0 539529099 20611072 4496 4294967295 134512640 134672761 3221224544 3221223648 134554877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4496 603 41 0 4991 0 vsize: 20128 [startup+1060.29 s] Raw data (loadavg): 1.07 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4520 0 0 0 105981 34 0 0 25 0 1 0 539529099 20611072 4498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4498 603 41 0 4991 0 vsize: 20128 [startup+1070.29 s] Raw data (loadavg): 1.06 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4523 0 0 0 106982 34 0 0 25 0 1 0 539529099 20611072 4501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4501 603 41 0 4991 0 vsize: 20128 [startup+1080.29 s] Raw data (loadavg): 1.05 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4523 0 0 0 107981 34 0 0 25 0 1 0 539529099 20611072 4501 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4501 603 41 0 4991 0 vsize: 20128 [startup+1090.3 s] Raw data (loadavg): 1.04 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4523 0 0 0 108982 34 0 0 25 0 1 0 539529099 20611072 4501 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4501 603 41 0 4991 0 vsize: 20128 [startup+1100.3 s] Raw data (loadavg): 1.03 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4523 0 0 0 109982 34 0 0 25 0 1 0 539529099 20611072 4501 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5032 4501 603 41 0 4991 0 vsize: 20128 [startup+1110.32 s] Raw data (loadavg): 1.03 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4529 0 0 0 110984 34 0 0 25 0 1 0 539529099 20758528 4507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5068 4507 603 41 0 5027 0 vsize: 20272 [startup+1120.32 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4606 0 0 0 111984 34 0 0 25 0 1 0 539529099 21024768 4584 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5133 4584 603 41 0 5092 0 vsize: 20532 [startup+1130.32 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4975 0 0 0 112983 35 0 0 25 0 1 0 539529099 22511616 4953 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5496 4953 603 41 0 5455 0 vsize: 21984 [startup+1140.32 s] Raw data (loadavg): 1.02 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 4987 0 0 0 113983 35 0 0 25 0 1 0 539529099 22654976 4965 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5531 4965 603 41 0 5490 0 vsize: 22124 [startup+1150.32 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5010 0 0 0 114983 35 0 0 25 0 1 0 539529099 22654976 4988 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5531 4988 603 41 0 5490 0 vsize: 22124 [startup+1160.32 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5453 0 0 0 115983 36 0 0 25 0 1 0 539529099 24526848 5431 4294967295 134512640 134672761 3221224544 3221223728 134558648 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5988 5431 603 41 0 5947 0 vsize: 23952 [startup+1170.32 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5896 0 0 0 116982 37 0 0 25 0 1 0 539529099 26255360 5874 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6410 5874 603 41 0 6369 0 vsize: 25640 [startup+1180.32 s] Raw data (loadavg): 1.01 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5968 0 0 0 117981 38 0 0 25 0 1 0 539529099 26660864 5946 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6509 5946 603 41 0 6468 0 vsize: 26036 [startup+1190.32 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5968 0 0 0 118981 38 0 0 25 0 1 0 539529099 26660864 5946 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6509 5946 603 41 0 6468 0 vsize: 26036 [startup+1200.32 s] Raw data (loadavg): 1.00 1.00 0.92 2/54 22137 Raw data (stat): 22135 (minisat+) R 22134 3260 3259 0 -1 0 5968 0 0 0 119981 39 0 0 25 0 1 0 539529099 26660864 5946 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6509 5946 603 41 0 6468 0 vsize: 26036 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.34 s] Raw data (loadavg): 1.00 1.00 0.92 1/54 22137 Raw data (stat): 22135 (minisat+) Z 22134 3260 3259 0 -1 12 5971 0 0 0 119981 40 0 0 25 0 1 0 539529099 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.34 CPU time (s): 1200.22 CPU user time (s): 1199.82 CPU system time (s): 0.403938 CPU usage (%): 99.9901 Max. virtual memory (Kb): 26036 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####