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 wulflinc25 THE 2005-04-21 21:21:55 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=14714 boxname=wulflinc25 idbench=1132 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: e6bff154156b54af3a9a38f7579209b6 /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos5.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos5.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-20-10-neos5.opb IDLAUNCH: 14714 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.220 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 788960 kB Buffers: 3008 kB Cached: 222036 kB SwapCached: 716 kB Active: 39912 kB Inactive: 187076 kB HighTotal: 131008 kB HighFree: 7924 kB LowTotal: 903652 kB LowFree: 781036 kB SwapTotal: 2097892 kB SwapFree: 2096236 kB Dirty: 36 kB Writeback: 0 kB Mapped: 4992 kB Slab: 12952 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 21:41:57 (client local time) WITH STATUS 10 IN 1200.34 SECONDS stats: 14714 7 1200.34 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]---> BDD-cost: 10 c ---[ 71]---> BDD-cost: 10 c ---[ 70]---> BDD-cost: 10 c ---[ 69]---> BDD-cost: 10 c ---[ 68]---> BDD-cost: 10 c ---[ 67]---> BDD-cost: 10 c ---[ 66]---> BDD-cost: 10 c ---[ 65]---> BDD-cost: 10 c ---[ 64]---> BDD-cost: 10 c ---[ 63]---> BDD-cost: 10 c ---[ 62]---> Sorter-cost: 382 Base: c ---[ 61]---> Sorter-cost: 831 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 60]---> Sorter-cost: 417 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 59]---> Sorter-cost: 1471 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 58]---> Sorter-cost: 1060 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 57]---> Sorter-cost: 429 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 56]---> Sorter-cost: 1241 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 1058 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 54]---> Sorter-cost: 1090 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 445 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 52]---> Sorter-cost: 1269 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 51]---> Sorter-cost: 216 Base: c ---[ 50]---> Sorter-cost: 1042 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 49]---> Sorter-cost: 1289 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 48]---> Sorter-cost: 548 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 46]---> Sorter-cost: 373 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 45]---> Sorter-cost: 405 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 44]---> Sorter-cost: 343 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 379 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 351 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 39]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 38]---> Sorter-cost: 1195 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 37]---> Sorter-cost: 345 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 36]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 35]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 379 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 33]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 1215 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 31]---> Sorter-cost: 405 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 417 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 29]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 28]---> Sorter-cost: 1020 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 27]---> Sorter-cost: 1259 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 26]---> Sorter-cost: 337 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 25]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 24]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 23]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 22]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 21]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 20]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 19]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 18]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 17]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 16]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 15]---> Sorter-cost: 355 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 14]---> Sorter-cost: 387 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 13]---> Sorter-cost: 389 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 12]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 11]---> Sorter-cost: 996 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 10]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 9]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 8]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 7]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 6]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 5]---> Sorter-cost: 355 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 4]---> Sorter-cost: 387 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 3]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 2]---> Sorter-cost: 130 Base: c ---[ 1]---> Sorter-cost: 301 Base: 2 2 2 2 2 2 2 2 2 2 c ---[ 0]---> Sorter-cost: 301 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 28565 68464 | 8569 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/18763 c -- var.elim.: 2000/18763 c -- var.elim.: 3000/18763 c -- var.elim.: 4000/18763 c -- var.elim.: 5000/18763 c -- var.elim.: 6000/18763 c -- var.elim.: 7000/18763 c -- var.elim.: 8000/18763 c -- var.elim.: 9000/18763 c -- var.elim.: 10000/18763 c -- var.elim.: 11000/18763 c -- var.elim.: 12000/18763 c -- var.elim.: 13000/18763 c -- var.elim.: 14000/18763 c -- var.elim.: 15000/18763 c -- var.elim.: 16000/18763 c -- var.elim.: 17000/18763 c -- var.elim.: 18000/18763 c -- var.elim.: 18763/18763 c -- var.elim.: 1000/8798 c -- var.elim.: 2000/8798 c -- var.elim.: 3000/8798 c -- var.elim.: 4000/8798 c -- var.elim.: 5000/8798 c -- var.elim.: 6000/8798 c -- var.elim.: 7000/8798 c -- var.elim.: 8000/8798 c -- var.elim.: 8798/8798 c -- var.elim.: 1000/1443 c -- var.elim.: 1443/1443 c -- var.elim.: 672/672 c -- subsuming c -- var.elim.: 1000/7898 c -- var.elim.: 2000/7898 c -- var.elim.: 3000/7898 c -- var.elim.: 4000/7898 c -- var.elim.: 5000/7898 c -- var.elim.: 6000/7898 c -- var.elim.: 7000/7898 c -- var.elim.: 7898/7898 c -- var.elim.: 1000/4083 c -- var.elim.: 2000/4083 c -- var.elim.: 3000/4083 c -- var.elim.: 4000/4083 c -- var.elim.: 4083/4083 c -- subsuming c -- var.elim.: 1000/1830 c -- var.elim.: 1830/1830 c -- var.elim.: 546/546 c -- subsuming c -- var.elim.: 426/426 c | 0 | 18638 93433 | -- 0 -- -- | -- | -9924/25050 c | 0 | 18638 93433 | 7455 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 4.82427 s) c ============================================================================== c [1mFound solution: 63104[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2665 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2 | 25127 108674 | 7538 2 35 17.5 | 0.000 % | c -- subsuming c -- var.elim.: 1000/2893 c -- var.elim.: 2000/2893 c -- var.elim.: 2893/2893 c -- var.elim.: 1000/1612 c -- var.elim.: 1612/1612 c -- subsuming c -- var.elim.: 420/420 c -- var.elim.: 310/310 c -- subsuming c -- var.elim.: 138/138 c | 2 | 24185 111924 | -- 2 -- -- | -- | -942/3251 c | 2 | 24185 111924 | 9674 2 35 17.5 | 0.000 % | c ============================================================================== c (current CPU-time: 5.69713 s) c ============================================================================== c [1mFound solution: 35326[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 56 | 24846 113763 | 7453 56 235 4.2 | 0.000 % | c -- subsuming c -- var.elim.: 1000/1045 c -- var.elim.: 1045/1045 c -- var.elim.: 564/564 c -- subsuming c -- var.elim.: 322/322 c | 56 | 24389 113444 | -- 56 -- -- | -- | -457/-318 c | 56 | 24389 113444 | 9755 56 235 4.2 | 0.000 % | c ============================================================================== c (current CPU-time: 6.22705 s) c ============================================================================== c [1mFound solution: 31462[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 129 | 24833 114751 | 7449 129 1031 8.0 | 0.000 % | c -- subsuming c -- var.elim.: 818/818 c -- var.elim.: 450/450 c -- var.elim.: 23/23 c | 129 | 24474 114653 | -- 129 -- -- | -- | -359/-97 c | 129 | 24474 114653 | 9789 129 1031 8.0 | 0.000 % | c | 229 | 24474 114653 | 10768 229 2171 9.5 | 0.837 % | c ============================================================================== c (current CPU-time: 6.74198 s) c ============================================================================== c [1mFound solution: 20544[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 254 | 24882 115814 | 7464 254 2271 8.9 | 0.837 % | c -- subsuming c -- var.elim.: 770/770 c -- var.elim.: 387/387 c | 254 | 24567 115512 | -- 254 -- -- | -- | -315/-301 c | 254 | 24567 115512 | 9826 254 2271 8.9 | 0.837 % | c | 354 | 24567 115512 | 10809 354 3367 9.5 | 0.877 % | c ============================================================================== c (current CPU-time: 7.30289 s) c ============================================================================== c [1mFound solution: 20543[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 424 | 24631 115719 | 7389 424 4316 10.2 | 0.877 % | c -- subsuming c -- var.elim.: 350/350 c -- var.elim.: 101/101 c | 424 | 24600 115881 | -- 424 -- -- | -- | -31/163 c | 424 | 24600 115881 | 9840 424 4316 10.2 | 0.877 % | c | 524 | 24600 115881 | 10824 524 6165 11.8 | 0.887 % | c ============================================================================== c (current CPU-time: 7.82781 s) c ============================================================================== c [1mFound solution: 20523[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 666 | 24669 116107 | 7400 666 7125 10.7 | 0.887 % | c -- subsuming c -- var.elim.: 154/154 c -- var.elim.: 113/113 c | 666 | 24634 116278 | -- 666 -- -- | -- | -35/172 c | 666 | 24634 116278 | 9853 666 7125 10.7 | 0.887 % | c | 766 | 24634 116278 | 10838 766 7654 10.0 | 0.897 % | c ============================================================================== c (current CPU-time: 8.29474 s) c ============================================================================== c [1mFound solution: 17655[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 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 851 | 24885 116918 | 7465 849 12731 15.0 | 0.897 % | c -- subsuming c -- var.elim.: 488/488 c -- var.elim.: 233/233 c | 851 | 24686 116724 | -- 849 -- -- | -- | -199/-193 c | 851 | 24686 116724 | 9874 849 12731 15.0 | 0.897 % | c | 951 | 24686 116724 | 10861 949 16234 17.1 | 0.948 % | c | 1104 | 24678 116660 | 11944 1091 18997 17.4 | 0.979 % | c | 1329 | 24678 116660 | 13138 1316 22814 17.3 | 0.979 % | c ============================================================================== c (current CPU-time: 9.15261 s) c ============================================================================== c [1mFound solution: 17450[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1406 | 24755 116917 | 7426 1393 26630 19.1 | 0.979 % | c -- subsuming c -- var.elim.: 414/414 c -- var.elim.: 130/130 c | 1406 | 24715 117058 | -- 1393 -- -- | -- | -40/142 c | 1406 | 24715 117058 | 9886 1393 26630 19.1 | 0.979 % | c | 1506 | 24715 117058 | 10874 1493 28731 19.2 | 1.010 % | c ============================================================================== c (current CPU-time: 9.70952 s) c ============================================================================== c [1mFound solution: 17449[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1573 | 24790 117306 | 7436 1560 32204 20.6 | 1.010 % | c -- subsuming c -- var.elim.: 169/169 c -- var.elim.: 125/125 c | 1573 | 24752 117473 | -- 1560 -- -- | -- | -38/168 c | 1573 | 24752 117473 | 9900 1560 32204 20.6 | 1.010 % | c | 1673 | 24752 117473 | 10890 1660 34452 20.8 | 1.020 % | c ============================================================================== c (current CPU-time: 10.2614 s) c ============================================================================== c [1mFound solution: 17446[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1778 | 24806 117642 | 7441 1765 39237 22.2 | 1.020 % | c -- subsuming c -- var.elim.: 111/111 c -- var.elim.: 80/80 c | 1778 | 24781 117771 | -- 1765 -- -- | -- | -25/130 c | 1778 | 24781 117771 | 9912 1765 39237 22.2 | 1.020 % | c ============================================================================== c (current CPU-time: 10.6924 s) c ============================================================================== c [1mFound solution: 17444[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 1861 | 24859 118030 | 7457 1848 41331 22.4 | 1.020 % | c -- subsuming c -- var.elim.: 177/177 c -- var.elim.: 130/130 c | 1861 | 24820 118327 | -- 1848 -- -- | -- | -39/298 c | 1861 | 24820 118327 | 9928 1848 41331 22.4 | 1.020 % | c | 1961 | 24820 118327 | 10920 1948 44318 22.8 | 1.040 % | c ============================================================================== c (current CPU-time: 11.2443 s) c ============================================================================== c [1mFound solution: 17439[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2057 | 24882 118493 | 7464 2024 46765 23.1 | 1.040 % | c -- subsuming c -- var.elim.: 279/279 c -- var.elim.: 105/105 c | 2057 | 24847 118668 | -- 2024 -- -- | -- | -35/176 c | 2057 | 24847 118668 | 9938 2024 46765 23.1 | 1.040 % | c | 2157 | 24847 118668 | 10932 2124 54196 25.5 | 1.082 % | c ============================================================================== c (current CPU-time: 11.8192 s) c ============================================================================== c [1mFound solution: 17438[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2213 | 24925 118927 | 7477 2180 56033 25.7 | 1.082 % | c -- subsuming c -- var.elim.: 177/177 c -- var.elim.: 129/129 c | 2213 | 24883 119160 | -- 2180 -- -- | -- | -42/234 c | 2213 | 24883 119160 | 9953 2180 56033 25.7 | 1.082 % | c | 2314 | 24883 119160 | 10948 2281 58904 25.8 | 1.092 % | c | 2467 | 24883 119160 | 12043 2434 63883 26.2 | 1.092 % | c ============================================================================== c (current CPU-time: 12.7111 s) c ============================================================================== c [1mFound solution: 17430[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2583 | 24960 119418 | 7487 2550 67995 26.7 | 1.092 % | c -- subsuming c -- var.elim.: 177/177 c -- var.elim.: 129/129 c | 2583 | 24920 119597 | -- 2550 -- -- | -- | -40/180 c | 2583 | 24920 119597 | 9968 2550 67995 26.7 | 1.092 % | c ============================================================================== c (current CPU-time: 13.095 s) c ============================================================================== c [1mFound solution: 17428[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2617 | 24983 119811 | 7494 2584 69170 26.8 | 1.092 % | c -- subsuming c -- var.elim.: 147/147 c -- var.elim.: 110/110 c | 2617 | 24952 119984 | -- 2584 -- -- | -- | -31/174 c | 2617 | 24952 119984 | 9980 2584 69170 26.8 | 1.092 % | c ============================================================================== c (current CPU-time: 13.463 s) c ============================================================================== c [1mFound solution: 17427[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 2668 | 25014 120195 | 7504 2635 69532 26.4 | 1.092 % | c -- subsuming c -- var.elim.: 145/145 c -- var.elim.: 109/109 c | 2668 | 24984 120368 | -- 2635 -- -- | -- | -30/174 c | 2668 | 24984 120368 | 9993 2635 69532 26.4 | 1.092 % | c | 2770 | 24984 120368 | 10992 2737 73217 26.8 | 1.122 % | c | 2920 | 24980 120328 | 12090 2884 78824 27.3 | 1.143 % | c | 3146 | 24980 120328 | 13299 3110 88206 28.4 | 1.143 % | c ============================================================================== c (current CPU-time: 14.6398 s) c ============================================================================== c [1mFound solution: 17426[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 3303 | 25047 120560 | 7514 3267 93765 28.7 | 1.143 % | c -- subsuming c -- var.elim.: 201/201 c -- var.elim.: 122/122 c | 3303 | 25014 120710 | -- 3267 -- -- | -- | -33/151 c | 3303 | 25014 120710 | 10005 3267 93765 28.7 | 1.143 % | c ============================================================================== c (current CPU-time: 15.0477 s) c ============================================================================== c [1mFound solution: 17424[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 3362 | 25076 120912 | 7522 3326 95642 28.8 | 1.143 % | c -- subsuming c -- var.elim.: 136/136 c -- var.elim.: 100/100 c | 3362 | 25046 121068 | -- 3326 -- -- | -- | -30/157 c | 3362 | 25046 121068 | 10018 3326 95642 28.8 | 1.143 % | c ============================================================================== c (current CPU-time: 15.4017 s) c ============================================================================== c [1mFound solution: 17423[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 3392 | 25107 121267 | 7532 3356 97093 28.9 | 1.143 % | c -- subsuming c -- var.elim.: 134/134 c -- var.elim.: 99/99 c | 3392 | 25078 121423 | -- 3356 -- -- | -- | -29/157 c | 3392 | 25078 121423 | 10031 3356 97093 28.9 | 1.143 % | c | 3492 | 25078 121423 | 11034 3456 99242 28.7 | 1.173 % | c ============================================================================== c (current CPU-time: 15.8476 s) c ============================================================================== c [1mFound solution: 17422[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 3507 | 25146 121657 | 7543 3471 99735 28.7 | 1.173 % | c -- subsuming c -- var.elim.: 162/162 c -- var.elim.: 122/122 c | 3507 | 25112 121787 | -- 3471 -- -- | -- | -34/131 c | 3507 | 25112 121787 | 10044 3471 99735 28.7 | 1.173 % | c | 3608 | 25112 121787 | 11049 3572 102478 28.7 | 1.183 % | c | 3759 | 25112 121787 | 12154 3723 108518 29.1 | 1.183 % | c | 3984 | 25112 121787 | 13369 3948 123023 31.2 | 1.183 % | c | 4322 | 25112 121787 | 14706 4286 134184 31.3 | 1.183 % | c ============================================================================== c (current CPU-time: 17.2544 s) c ============================================================================== c [1mFound solution: 17421[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 4491 | 25178 122012 | 7553 4455 138566 31.1 | 1.183 % | c -- subsuming c -- var.elim.: 155/155 c -- var.elim.: 117/117 c | 4491 | 25146 122146 | -- 4455 -- -- | -- | -32/135 c | 4491 | 25146 122146 | 10058 4455 138566 31.1 | 1.183 % | c ============================================================================== c (current CPU-time: 17.6283 s) c ============================================================================== c [1mFound solution: 17420[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 4515 | 25211 122362 | 7563 4479 140487 31.4 | 1.183 % | c -- subsuming c -- var.elim.: 147/147 c -- var.elim.: 110/110 c | 4515 | 25180 122498 | -- 4479 -- -- | -- | -31/137 c | 4515 | 25180 122498 | 10072 4479 140487 31.4 | 1.183 % | c | 4616 | 25170 122360 | 11074 4574 143196 31.3 | 1.234 % | c | 4766 | 25170 122360 | 12182 4724 145572 30.8 | 1.234 % | c | 4992 | 25170 122360 | 13400 4950 154173 31.1 | 1.234 % | c ============================================================================== c (current CPU-time: 18.6032 s) c ============================================================================== c [1mFound solution: 17419[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 5093 | 25230 122548 | 7568 5051 162944 32.3 | 1.234 % | c -- subsuming c -- var.elim.: 230/230 c -- var.elim.: 90/90 c | 5093 | 25202 122689 | -- 5051 -- -- | -- | -28/142 c | 5093 | 25202 122689 | 10080 5051 162944 32.3 | 1.234 % | c | 5194 | 25202 122689 | 11088 5152 167600 32.5 | 1.244 % | c | 5344 | 25202 122689 | 12197 5302 169868 32.0 | 1.244 % | c | 5570 | 25202 122689 | 13417 5528 177625 32.1 | 1.244 % | c ============================================================================== c (current CPU-time: 19.844 s) c ============================================================================== c [1mFound solution: 17414[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 5726 | 25256 122855 | 7576 5684 183395 32.3 | 1.244 % | c -- subsuming c -- var.elim.: 108/108 c -- var.elim.: 77/77 c | 5726 | 25232 122984 | -- 5684 -- -- | -- | -24/130 c | 5726 | 25232 122984 | 10092 5684 183395 32.3 | 1.244 % | c ============================================================================== c (current CPU-time: 20.3439 s) c ============================================================================== c [1mFound solution: 17413[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 5809 | 25297 123206 | 7589 5767 187017 32.4 | 1.244 % | c -- subsuming c -- var.elim.: 153/153 c -- var.elim.: 115/115 c | 5809 | 25265 123337 | -- 5767 -- -- | -- | -32/132 c | 5809 | 25265 123337 | 10106 5767 187017 32.4 | 1.244 % | c ============================================================================== c (current CPU-time: 20.8188 s) c ============================================================================== c [1mFound solution: 17412[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 5887 | 25330 123552 | 7598 5845 189377 32.4 | 1.244 % | c -- subsuming c -- var.elim.: 146/146 c -- var.elim.: 108/108 c | 5887 | 25298 123683 | -- 5845 -- -- | -- | -32/132 c | 5887 | 25298 123683 | 10119 5845 189377 32.4 | 1.244 % | c ============================================================================== c (current CPU-time: 21.2418 s) c ============================================================================== c [1mFound solution: 17410[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 5962 | 25360 123883 | 7607 5920 195152 33.0 | 1.244 % | c -- subsuming c -- var.elim.: 134/134 c -- var.elim.: 99/99 c | 5962 | 25331 124020 | -- 5920 -- -- | -- | -29/138 c | 5962 | 25331 124020 | 10132 5920 195152 33.0 | 1.244 % | c ============================================================================== c (current CPU-time: 21.6487 s) c ============================================================================== c [1mFound solution: 17409[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 6044 | 25394 124221 | 7618 6001 200302 33.4 | 1.244 % | c -- subsuming c -- var.elim.: 277/277 c -- var.elim.: 115/115 c | 6044 | 25362 124361 | -- 6001 -- -- | -- | -32/141 c | 6044 | 25362 124361 | 10144 6001 200302 33.4 | 1.244 % | c | 6145 | 25362 124361 | 11159 6102 205638 33.7 | 1.305 % | c ============================================================================== c (current CPU-time: 22.1766 s) c ============================================================================== c [1mFound solution: 17408[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 6174 | 25412 124501 | 7623 6131 207318 33.8 | 1.305 % | c -- subsuming c -- var.elim.: 86/86 c -- var.elim.: 57/57 c | 6174 | 25390 124634 | -- 6131 -- -- | -- | -22/134 c | 6174 | 25390 124634 | 10156 6128 207293 33.8 | 1.305 % | c | 6278 | 25390 124634 | 11171 6232 209386 33.6 | 1.315 % | c | 6429 | 25390 124634 | 12288 6383 215005 33.7 | 1.315 % | c | 6655 | 25390 124634 | 13517 6609 224815 34.0 | 1.315 % | c | 6994 | 25390 124634 | 14869 6948 232710 33.5 | 1.315 % | c | 7502 | 25388 124619 | 16355 7453 262811 35.3 | 1.326 % | c | 8261 | 25388 124619 | 17990 8212 292506 35.6 | 1.326 % | c | 9400 | 25388 124619 | 19789 9351 339242 36.3 | 1.326 % | c | 11108 | 25386 124597 | 21766 11044 421714 38.2 | 1.336 % | c ============================================================================== c (current CPU-time: 28.9916 s) c ============================================================================== c [1mFound solution: 16426[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 12027 | 25443 124777 | 7632 11963 493838 41.3 | 1.336 % | c -- subsuming c -- var.elim.: 315/315 c -- var.elim.: 109/109 c -- var.elim.: 136/136 c -- var.elim.: 40/40 c -- var.elim.: 9/9 c | 12027 | 24664 116571 | -- 11963 -- -- | -- | -779/-8205 c | 12027 | 24664 116571 | 9865 10888 446317 41.0 | 1.336 % | c | 12127 | 24664 116571 | 10852 7359 300160 40.8 | 1.351 % | c | 12278 | 24664 116571 | 11937 7510 306196 40.8 | 1.351 % | c | 12503 | 24664 116571 | 13131 7735 313370 40.5 | 1.351 % | c ============================================================================== c (current CPU-time: 30.3014 s) c ============================================================================== c [1mFound solution: 16424[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 12714 | 24729 116779 | 7418 7946 321650 40.5 | 1.351 % | c -- subsuming c -- var.elim.: 139/139 c -- var.elim.: 100/100 c | 12714 | 24698 116944 | -- 7946 -- -- | -- | -31/166 c | 12714 | 24698 116944 | 9879 7946 321650 40.5 | 1.351 % | c | 12814 | 24698 116944 | 10867 8046 323646 40.2 | 1.360 % | c | 12965 | 24698 116944 | 11953 8197 328609 40.1 | 1.360 % | c ============================================================================== c (current CPU-time: 31.0643 s) c ============================================================================== c [1mFound solution: 16422[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 13154 | 24750 117104 | 7424 8386 354086 42.2 | 1.360 % | c -- subsuming c -- var.elim.: 105/105 c -- var.elim.: 74/74 c | 13154 | 24723 117215 | -- 8386 -- -- | -- | -27/112 c | 13154 | 24723 117215 | 9889 8386 354086 42.2 | 1.360 % | c | 13254 | 24723 117215 | 10878 8486 355894 41.9 | 1.371 % | c | 13404 | 24723 117215 | 11965 8636 364555 42.2 | 1.371 % | c | 13629 | 24723 117215 | 13162 8861 377712 42.6 | 1.371 % | c | 13966 | 24723 117215 | 14478 9198 421802 45.9 | 1.371 % | c ============================================================================== c (current CPU-time: 32.631 s) c ============================================================================== c [1mFound solution: 16418[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 14086 | 24799 117465 | 7439 9318 429614 46.1 | 1.371 % | c -- subsuming c -- var.elim.: 170/170 c -- var.elim.: 123/123 c | 14086 | 24762 117815 | -- 9318 -- -- | -- | -37/351 c | 14086 | 24762 117815 | 9904 9318 429614 46.1 | 1.371 % | c | 14187 | 24762 117815 | 10895 9419 434057 46.1 | 1.381 % | c | 14337 | 24762 117815 | 11984 9569 447898 46.8 | 1.381 % | c | 14562 | 24762 117815 | 13183 9794 458340 46.8 | 1.381 % | c ============================================================================== c (current CPU-time: 33.7259 s) c ============================================================================== c [1mFound solution: 16406[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 14603 | 24837 118064 | 7451 9835 461888 47.0 | 1.381 % | c -- subsuming c -- var.elim.: 171/171 c -- var.elim.: 123/123 c | 14603 | 24795 118225 | -- 9835 -- -- | -- | -42/162 c | 14603 | 24795 118225 | 9918 9835 461888 47.0 | 1.381 % | c | 14704 | 24795 118225 | 10909 9936 464569 46.8 | 1.391 % | c | 14854 | 24795 118225 | 12000 10086 471467 46.7 | 1.390 % | c | 15079 | 24795 118225 | 13200 10311 481408 46.7 | 1.390 % | c | 15416 | 24795 118225 | 14520 10648 499927 47.0 | 1.390 % | c ============================================================================== c (current CPU-time: 35.6056 s) c ============================================================================== c [1mFound solution: 16402[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 15681 | 24861 118451 | 7458 10913 526451 48.2 | 1.390 % | c -- subsuming c -- var.elim.: 156/156 c -- var.elim.: 117/117 c | 15681 | 24827 118593 | -- 10913 -- -- | -- | -34/143 c | 15681 | 24827 118593 | 9930 10913 526451 48.2 | 1.390 % | c ============================================================================== c (current CPU-time: 36.1925 s) c ============================================================================== c [1mFound solution: 16398[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 15774 | 24893 118819 | 7467 7369 371803 50.5 | 1.390 % | c -- subsuming c -- var.elim.: 156/156 c -- var.elim.: 117/117 c | 15774 | 24859 118943 | -- 7369 -- -- | -- | -34/125 c | 15774 | 24859 118943 | 9943 7369 371803 50.5 | 1.390 % | c | 15875 | 24859 118943 | 10937 7470 382171 51.2 | 1.410 % | c ============================================================================== c (current CPU-time: 36.7694 s) c ============================================================================== c [1mFound solution: 16394[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 15968 | 24916 119122 | 7474 7563 388449 51.4 | 1.410 % | c -- subsuming c -- var.elim.: 118/118 c -- var.elim.: 86/86 c | 15968 | 24891 119271 | -- 7563 -- -- | -- | -25/150 c | 15968 | 24891 119271 | 9956 7563 388449 51.4 | 1.410 % | c | 16068 | 24891 119271 | 10952 7663 393222 51.3 | 1.420 % | c | 16218 | 24891 119271 | 12047 7813 400391 51.2 | 1.420 % | c | 16444 | 24891 119271 | 13251 8039 406395 50.6 | 1.420 % | c | 16782 | 24891 119271 | 14577 8377 457504 54.6 | 1.420 % | c ============================================================================== c (current CPU-time: 38.7601 s) c ============================================================================== c [1mFound solution: 16392[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 17212 | 24948 119450 | 7484 8807 496083 56.3 | 1.420 % | c -- subsuming c -- var.elim.: 119/119 c -- var.elim.: 86/86 c | 17212 | 24921 119588 | -- 8807 -- -- | -- | -27/139 c | 17212 | 24921 119588 | 9968 8807 496083 56.3 | 1.420 % | c | 17314 | 24921 119588 | 10965 8909 501195 56.3 | 1.431 % | c ============================================================================== c (current CPU-time: 39.432 s) c ============================================================================== c [1mFound solution: 16390[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 17377 | 24973 119747 | 7491 8972 506032 56.4 | 1.431 % | c -- subsuming c -- var.elim.: 104/104 c -- var.elim.: 73/73 c | 17377 | 24947 119860 | -- 8972 -- -- | -- | -26/114 c | 17377 | 24947 119860 | 9978 8972 506032 56.4 | 1.431 % | c | 17478 | 24947 119860 | 10976 9073 508232 56.0 | 1.441 % | c | 17628 | 24947 119860 | 12074 9223 516598 56.0 | 1.441 % | c | 17854 | 24947 119860 | 13281 9449 532785 56.4 | 1.441 % | c | 18192 | 24947 119860 | 14609 9787 563770 57.6 | 1.441 % | c | 18698 | 24947 119860 | 16070 10293 595013 57.8 | 1.441 % | c ============================================================================== c (current CPU-time: 41.8726 s) c ============================================================================== c [1mFound solution: 16389[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 18806 | 25010 120075 | 7502 10401 604948 58.2 | 1.441 % | c -- subsuming c -- var.elim.: 148/148 c -- var.elim.: 111/111 c | 18806 | 24978 120201 | -- 10401 -- -- | -- | -32/127 c | 18806 | 24978 120201 | 9991 10401 604948 58.2 | 1.441 % | c | 18906 | 24978 120201 | 10990 7034 397038 56.4 | 1.451 % | c | 19056 | 24978 120201 | 12089 7184 403074 56.1 | 1.451 % | c | 19281 | 24978 120201 | 13298 7409 425471 57.4 | 1.451 % | c ============================================================================== c (current CPU-time: 43.1444 s) c ============================================================================== c [1mFound solution: 16386[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 19380 | 25039 120396 | 7511 7508 431010 57.4 | 1.451 % | c -- subsuming c -- var.elim.: 130/130 c -- var.elim.: 95/95 c | 19380 | 25009 120526 | -- 7508 -- -- | -- | -30/131 c | 19380 | 25009 120526 | 10003 7508 431010 57.4 | 1.451 % | c ============================================================================== c (current CPU-time: 43.6974 s) c ============================================================================== c [1mFound solution: 16385[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 19464 | 25073 120742 | 7521 7592 434682 57.3 | 1.451 % | c -- subsuming c -- var.elim.: 148/148 c -- var.elim.: 111/111 c | 19464 | 25041 120877 | -- 7592 -- -- | -- | -32/136 c | 19464 | 25041 120877 | 10016 7592 434682 57.3 | 1.451 % | c ============================================================================== c (current CPU-time: 44.1653 s) c ============================================================================== c [1mFound solution: 16384[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 19512 | 25089 121010 | 7526 7640 441435 57.8 | 1.451 % | c -- subsuming c -- var.elim.: 81/81 c -- var.elim.: 53/53 c | 19512 | 25067 121138 | -- 7640 -- -- | -- | -22/129 c | 19512 | 25067 121138 | 10026 7640 441435 57.8 | 1.451 % | c | 19613 | 25067 121138 | 11029 7741 443308 57.3 | 1.481 % | c | 19763 | 25067 121138 | 12132 7891 450629 57.1 | 1.481 % | c | 19991 | 25067 121138 | 13345 8119 453764 55.9 | 1.481 % | c | 20329 | 25067 121138 | 14680 8457 476614 56.4 | 1.481 % | c | 20837 | 25067 121138 | 16148 8965 520602 58.1 | 1.481 % | c | 21599 | 25061 121084 | 17758 9572 557165 58.2 | 1.512 % | c | 22739 | 25061 121084 | 19534 10712 659415 61.6 | 1.512 % | c | 24447 | 25061 121084 | 21488 12420 789835 63.6 | 1.512 % | c | 27010 | 25061 121084 | 23637 14983 1055549 70.4 | 1.512 % | c | 30854 | 25061 121084 | 26000 18827 1392987 74.0 | 1.512 % | c | 36620 | 25061 121084 | 28600 24593 1788058 72.7 | 1.512 % | c | 45269 | 25061 121084 | 31460 17420 1455778 83.6 | 1.512 % | c | 58243 | 25057 121065 | 34601 30392 2711083 89.2 | 1.533 % | c ============================================================================== c (current CPU-time: 102.887 s) c ============================================================================== c [1mFound solution: 16378[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 70520 | 25112 121233 | 7533 23301 1648893 70.8 | 1.533 % | c -- subsuming c -- var.elim.: 354/354 c -- var.elim.: 94/94 c | 70520 | 25088 121387 | -- 23301 -- -- | -- | -24/155 c | 70520 | 25088 121387 | 10035 23301 1648893 70.8 | 1.533 % | c | 70621 | 25088 121387 | 11038 10043 510497 50.8 | 1.553 % | c | 70773 | 25088 121387 | 12142 10195 515137 50.5 | 1.553 % | c | 70998 | 25079 121249 | 13352 10394 518441 49.9 | 1.574 % | c | 71335 | 25073 121195 | 14683 10730 540553 50.4 | 1.605 % | c | 71841 | 25073 121195 | 16152 11236 572189 50.9 | 1.605 % | c | 72600 | 25009 120386 | 17721 11607 588221 50.7 | 1.791 % | c | 73740 | 25009 120386 | 19494 12747 643008 50.4 | 1.791 % | c | 75450 | 25009 120386 | 21443 14457 743365 51.4 | 1.791 % | c | 78012 | 25009 120386 | 23587 17019 1133452 66.6 | 1.791 % | c | 81857 | 25009 120386 | 25946 20864 1458324 69.9 | 1.791 % | c ============================================================================== c (current CPU-time: 119.303 s) c ============================================================================== c [1mFound solution: 16375[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 82147 | 25031 120439 | 7509 21154 1480532 70.0 | 1.791 % | c -- subsuming c -- var.elim.: 702/702 c -- var.elim.: 303/303 c -- var.elim.: 197/197 c -- var.elim.: 211/211 c | 82147 | 24997 120904 | -- 21154 -- -- | -- | -34/466 c | 82147 | 24997 120904 | 9998 20030 1240079 61.9 | 1.791 % | c | 82247 | 24997 120904 | 10998 9003 654543 72.7 | 1.835 % | c | 82397 | 24997 120904 | 12098 9153 664517 72.6 | 1.835 % | c | 82622 | 24997 120904 | 13308 9378 685748 73.1 | 1.835 % | c | 82959 | 24997 120904 | 14639 9715 708526 72.9 | 1.835 % | c | 83465 | 24997 120904 | 16103 10221 745268 72.9 | 1.835 % | c | 84227 | 24997 120904 | 17713 10983 799352 72.8 | 1.835 % | c | 85366 | 24991 120856 | 19480 12039 920660 76.5 | 1.866 % | c | 87075 | 24991 120856 | 21428 13748 1062830 77.3 | 1.866 % | c | 89637 | 24991 120856 | 23570 16310 1235492 75.8 | 1.866 % | c | 93482 | 24991 120856 | 25928 20155 1582590 78.5 | 1.866 % | c | 99248 | 24991 120856 | 28520 25921 2157013 83.2 | 1.866 % | c ============================================================================== c (current CPU-time: 147.721 s) c ============================================================================== c [1mFound solution: 16374[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 102259 | 25053 121081 | 7515 28932 2428833 83.9 | 1.866 % | c -- subsuming c -- var.elim.: 516/516 c -- var.elim.: 127/127 c | 102259 | 25018 122190 | -- 28932 -- -- | -- | -35/1110 c | 102259 | 25018 122190 | 10007 28895 2421192 83.8 | 1.866 % | c | 102362 | 25018 122190 | 11007 6970 397839 57.1 | 1.876 % | c | 102512 | 25018 122190 | 12108 7120 406093 57.0 | 1.876 % | c | 102738 | 25018 122190 | 13319 7346 420089 57.2 | 1.876 % | c | 103076 | 25018 122190 | 14651 7684 448182 58.3 | 1.876 % | c | 103582 | 25018 122190 | 16116 8190 480835 58.7 | 1.876 % | c | 104341 | 25018 122190 | 17728 8949 548548 61.3 | 1.876 % | c | 105482 | 25018 122190 | 19501 10090 594654 58.9 | 1.876 % | c | 107190 | 25018 122190 | 21451 11798 738740 62.6 | 1.876 % | c | 109753 | 25018 122190 | 23596 14361 982765 68.4 | 1.876 % | c | 113599 | 25018 122190 | 25956 18207 1591865 87.4 | 1.876 % | c | 119366 | 25018 122190 | 28551 23974 2161096 90.1 | 1.876 % | c | 128015 | 25018 122190 | 31406 16221 1143919 70.5 | 1.876 % | c | 140989 | 25003 121365 | 34526 29194 2329439 79.8 | 1.886 % | c | 160450 | 25003 121365 | 37979 28135 3236599 115.0 | 1.886 % | c | 189643 | 25003 121365 | 41777 31988 5555883 173.7 | 1.886 % | c ============================================================================== c (current CPU-time: 273.974 s) c ============================================================================== c [1mFound solution: 16373[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 193667 | 25050 121555 | 7514 36012 6000037 166.6 | 1.886 % | c -- subsuming c -- var.elim.: 363/363 c -- var.elim.: 345/345 c | 193667 | 24999 121977 | -- 36012 -- -- | -- | -51/423 c | 193667 | 24999 121977 | 9999 36012 6000037 166.6 | 1.886 % | c | 193767 | 24999 121977 | 10999 10239 821445 80.2 | 1.897 % | c | 193918 | 24999 121977 | 12099 10390 826843 79.6 | 1.897 % | c | 194143 | 24999 121977 | 13309 10615 834225 78.6 | 1.897 % | c | 194480 | 24999 121977 | 14640 10952 855711 78.1 | 1.898 % | c | 194986 | 24999 121977 | 16104 11458 908361 79.3 | 1.897 % | c | 195745 | 24999 121977 | 17714 12217 986642 80.8 | 1.897 % | c | 196886 | 24870 120531 | 19385 13327 1163267 87.3 | 2.374 % | c | 198594 | 24854 120438 | 21310 15031 1341674 89.3 | 2.457 % | c | 201159 | 24854 120438 | 23441 17596 1620250 92.1 | 2.457 % | c | 205003 | 24838 120344 | 25769 21436 1978735 92.3 | 2.540 % | c | 210769 | 24838 120344 | 28346 27202 2434421 89.5 | 2.540 % | c | 219418 | 24832 120292 | 31173 17665 2462284 139.4 | 2.571 % | c | 232392 | 24832 120292 | 34290 30639 4069297 132.8 | 2.571 % | c | 251855 | 24832 120292 | 37719 29286 3035479 103.6 | 2.571 % | c ============================================================================== c (current CPU-time: 355.093 s) c ============================================================================== c [1mFound solution: 16368[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 254163 | 24877 120462 | 7463 31594 3200227 101.3 | 2.571 % | c -- subsuming c -- var.elim.: 1000/1629 c -- var.elim.: 1629/1629 c -- var.elim.: 326/326 c -- var.elim.: 230/230 c -- var.elim.: 128/128 c -- subsuming c -- var.elim.: 256/256 c -- var.elim.: 153/153 c | 254163 | 24801 121436 | -- 31594 -- -- | -- | -76/975 c | 254163 | 24801 121436 | 9920 29980 2470663 82.4 | 2.571 % | c | 254264 | 24801 121436 | 10912 9597 464298 48.4 | 2.590 % | c | 254416 | 24801 121436 | 12003 9749 468816 48.1 | 2.590 % | c | 254641 | 24801 121436 | 13204 9974 474408 47.6 | 2.590 % | c | 254978 | 24801 121436 | 14524 10311 485314 47.1 | 2.590 % | c | 255484 | 24801 121436 | 15976 10817 503831 46.6 | 2.590 % | c | 256243 | 24737 120415 | 17529 11298 520556 46.1 | 2.757 % | c | 257384 | 24737 120415 | 19282 12439 577306 46.4 | 2.757 % | c | 259092 | 24737 120415 | 21210 14147 646592 45.7 | 2.757 % | c | 261654 | 24737 120415 | 23331 16709 909547 54.4 | 2.757 % | c | 265498 | 24721 120321 | 25647 20551 1222374 59.5 | 2.840 % | c | 271264 | 24721 120321 | 28212 26317 1947068 74.0 | 2.840 % | c | 279913 | 24721 120321 | 31034 19671 1887334 95.9 | 2.840 % | c ============================================================================== c (current CPU-time: 393.595 s) c ============================================================================== c [1mFound solution: 16367[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 284022 | 24765 120488 | 7429 23780 2229501 93.8 | 2.840 % | c -- subsuming c -- var.elim.: 713/713 c -- var.elim.: 376/376 c -- var.elim.: 162/162 c -- var.elim.: 241/241 c | 284022 | 24684 119200 | -- 23780 -- -- | -- | -81/-1287 c | 284022 | 24684 119200 | 9873 23245 2175023 93.6 | 2.840 % | c | 284123 | 24684 119200 | 10860 9735 748673 76.9 | 2.856 % | c | 284274 | 24684 119200 | 11947 9886 753183 76.2 | 2.856 % | c | 284499 | 24684 119200 | 13141 10111 768696 76.0 | 2.856 % | c | 284838 | 24684 119200 | 14455 10450 787526 75.4 | 2.856 % | c | 285345 | 24684 119200 | 15901 10957 823035 75.1 | 2.856 % | c | 286105 | 24684 119200 | 17491 11717 875930 74.8 | 2.856 % | c | 287244 | 24684 119200 | 19240 12856 996169 77.5 | 2.856 % | c | 288953 | 24684 119200 | 21164 14565 1090984 74.9 | 2.856 % | c | 291517 | 24684 119200 | 23281 17129 1363343 79.6 | 2.856 % | c | 295361 | 24684 119200 | 25609 20973 1700162 81.1 | 2.856 % | c | 301131 | 24668 119106 | 28152 26742 2294555 85.8 | 2.940 % | c | 309780 | 24668 119106 | 30967 18302 1308196 71.5 | 2.939 % | c | 322757 | 24668 119106 | 34064 31279 3089788 98.8 | 2.940 % | c | 342221 | 24668 119106 | 37470 30845 4688950 152.0 | 2.940 % | c | 371415 | 24658 119073 | 41201 36633 6474726 176.7 | 2.960 % | c | 415205 | 24658 119073 | 45321 22972 7231878 314.8 | 2.960 % | c | 480889 | 24658 119073 | 49853 21471 6138707 285.9 | 2.960 % | c | 579421 | 24658 119073 | 54838 43565 11227295 257.7 | 2.960 % | c ============================================================================== c (current CPU-time: 920.509 s) c ============================================================================== c [1mFound solution: 16295[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 588699 | 24703 119232 | 7410 52843 12666398 239.7 | 2.960 % | c -- subsuming c -- var.elim.: 511/511 c -- var.elim.: 87/87 c | 588699 | 24676 119585 | -- 52843 -- -- | -- | -27/354 c | 588699 | 24676 119585 | 9870 52843 12666398 239.7 | 2.960 % | c | 588799 | 24676 119585 | 10857 10061 1373717 136.5 | 2.970 % | c | 588950 | 24676 119585 | 11943 10212 1378063 134.9 | 2.970 % | c | 589176 | 24676 119585 | 13137 10438 1396636 133.8 | 2.970 % | c | 589513 | 24676 119585 | 14451 10775 1410617 130.9 | 2.970 % | c | 590020 | 24676 119585 | 15896 11282 1443485 127.9 | 2.970 % | c | 590781 | 24676 119585 | 17486 12043 1509134 125.3 | 2.970 % | c | 591920 | 24676 119585 | 19234 13182 1627150 123.4 | 2.970 % | c | 593628 | 24676 119585 | 21158 14890 1786837 120.0 | 2.970 % | c ============================================================================== c (current CPU-time: 931.91 s) c ============================================================================== c [1mFound solution: 16278[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 595751 | 24729 119790 | 7418 17013 1878122 110.4 | 2.970 % | c -- subsuming c -- var.elim.: 150/150 c -- var.elim.: 113/113 c | 595751 | 24695 120201 | -- 17013 -- -- | -- | -34/412 c | 595751 | 24695 120201 | 9878 17013 1878122 110.4 | 2.970 % | c | 595851 | 24695 120201 | 10865 7663 437024 57.0 | 2.980 % | c | 596001 | 24695 120201 | 11952 7813 446642 57.2 | 2.980 % | c | 596227 | 24695 120201 | 13147 8039 463338 57.6 | 2.980 % | c | 596565 | 24695 120201 | 14462 8377 502072 59.9 | 2.980 % | c | 597072 | 24695 120201 | 15908 8884 548795 61.8 | 2.980 % | c | 597831 | 24695 120201 | 17499 9643 629666 65.3 | 2.980 % | c | 598970 | 24695 120201 | 19249 10782 750232 69.6 | 2.980 % | c | 600679 | 24695 120201 | 21174 12491 864476 69.2 | 2.980 % | c | 603241 | 24695 120201 | 23291 15053 1113925 74.0 | 2.980 % | c | 607086 | 24695 120201 | 25620 18898 1470213 77.8 | 2.980 % | c | 612854 | 24695 120201 | 28183 24666 2320192 94.1 | 2.980 % | c | 621503 | 24695 120201 | 31001 18592 2030610 109.2 | 2.980 % | c ============================================================================== c (current CPU-time: 977.189 s) c ============================================================================== c [1mFound solution: 16102[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 2 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 629173 | 24732 120296 | 7419 26262 2796123 106.5 | 2.980 % | c -- subsuming c -- var.elim.: 56/56 c -- var.elim.: 32/32 c | 629173 | 24711 120433 | -- 26262 -- -- | -- | -21/138 c | 629173 | 24711 120433 | 9884 26262 2796123 106.5 | 2.980 % | c | 629274 | 24711 120433 | 10872 7002 502126 71.7 | 2.990 % | c | 629425 | 24711 120433 | 11960 7153 507773 71.0 | 2.990 % | c | 629650 | 24711 120433 | 13156 7378 518494 70.3 | 2.990 % | c | 629987 | 24711 120433 | 14471 7715 536038 69.5 | 2.990 % | c | 630494 | 24711 120433 | 15918 8222 569489 69.3 | 2.990 % | c | 631253 | 24711 120433 | 17510 8981 656421 73.1 | 2.990 % | c | 632392 | 24711 120433 | 19261 10120 766386 75.7 | 2.990 % | c | 634101 | 24711 120433 | 21188 11829 1013351 85.7 | 2.990 % | c | 636663 | 24711 120433 | 23306 14391 1286216 89.4 | 2.990 % | c | 640507 | 24711 120433 | 25637 18235 1776256 97.4 | 2.990 % | c | 646277 | 24711 120433 | 28201 24005 2657452 110.7 | 2.990 % | c | 654926 | 24711 120433 | 31021 18091 2263081 125.1 | 2.990 % | c | 667903 | 24711 120433 | 34123 31068 6794448 218.7 | 2.990 % | c ============================================================================== c (current CPU-time: 1058.77 s) c ============================================================================== c [1mFound solution: 16098[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 =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 674828 | 24761 120611 | 7428 37993 7481639 196.9 | 2.990 % | c -- subsuming c -- var.elim.: 126/126 c -- var.elim.: 92/92 c | 674828 | 24730 120758 | -- 37993 -- -- | -- | -31/148 c | 674828 | 24730 120758 | 9892 37993 7481639 196.9 | 2.990 % | c | 674930 | 24730 120758 | 10881 7297 495069 67.8 | 3.000 % | c | 675080 | 24730 120758 | 11969 7447 512526 68.8 | 3.000 % | c | 675305 | 24730 120758 | 13166 7672 522117 68.1 | 3.000 % | c | 675645 | 24730 120758 | 14482 8012 557170 69.5 | 3.000 % | c | 676152 | 24730 120758 | 15931 8519 585124 68.7 | 3.000 % | c | 676913 | 24730 120758 | 17524 9280 632062 68.1 | 3.000 % | c | 678052 | 24730 120758 | 19276 10419 773694 74.3 | 3.000 % | c | 679760 | 24730 120758 | 21204 12127 1061488 87.5 | 3.000 % | c | 682322 | 24714 120478 | 23309 14686 1329737 90.5 | 3.021 % | c | 686168 | 24714 120478 | 25640 18532 1872215 101.0 | 3.021 % | c | 691935 | 24714 120478 | 28204 24299 2795470 115.0 | 3.021 % | c | 700584 | 24714 120478 | 31025 18539 2146066 115.8 | 3.021 % | c | 713558 | 24714 120478 | 34127 31513 3832745 121.6 | 3.021 % | c | 733019 | 24714 120478 | 37540 31834 4268406 134.1 | 3.021 % | c c *** TERMINATED *** s SATISFIABLE v -d1_bit0 -d2_bit0 -d3_bit0 -d4_bit0 -d5_bit0 -d6_bit0 -d7_bit0 -d8_bit0 -d9_bit0 -d10_bit0 d11_bit0 d12_bit0 d13_bit0 d14_bit0 -d15_bit0#### 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.70 0.90 0.89 2/54 15047 Raw data (stat): 15047 (runsolver) R 15046 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 548292885 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+9.99942 s] Raw data (loadavg): 0.75 0.90 0.89 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 7620 0 0 0 970 27 0 0 25 0 1 0 548292885 18595840 3719 4294967295 134512640 134672761 3221224544 3221223680 134614690 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4540 3719 603 41 0 4499 0 vsize: 18160 [startup+20.0001 s] Raw data (loadavg): 0.78 0.90 0.89 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 16823 0 0 0 1931 66 0 0 25 0 1 0 548292885 19566592 3973 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4777 3973 603 41 0 4736 0 vsize: 19108 [startup+30.0007 s] Raw data (loadavg): 0.82 0.91 0.89 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 20388 0 0 0 2914 82 0 0 25 0 1 0 548292885 22343680 4539 4294967295 134512640 134672761 3221224544 3221222880 134605508 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5455 4539 603 41 0 5414 0 vsize: 21820 [startup+40.0012 s] Raw data (loadavg): 0.84 0.91 0.89 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 24694 0 0 0 3896 100 0 0 25 0 1 0 548292885 22769664 4650 4294967295 134512640 134672761 3221224544 3221222808 1075730078 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5559 4650 603 41 0 5518 0 vsize: 22236 [startup+50.0019 s] Raw data (loadavg): 0.87 0.91 0.89 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 26836 0 0 0 4885 111 0 0 25 0 1 0 548292885 20873216 4378 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5096 4378 603 41 0 5055 0 vsize: 20384 [startup+60.0017 s] Raw data (loadavg): 0.89 0.91 0.90 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 27276 0 0 0 5884 112 0 0 25 0 1 0 548292885 22773760 4818 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5560 4818 603 41 0 5519 0 vsize: 22240 [startup+70.002 s] Raw data (loadavg): 0.90 0.92 0.90 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 28222 0 0 0 6881 115 0 0 25 0 1 0 548292885 26587136 5764 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6491 5764 603 41 0 6450 0 vsize: 25964 [startup+80.0016 s] Raw data (loadavg): 0.92 0.92 0.90 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 28297 0 0 0 7882 115 0 0 25 0 1 0 548292885 26869760 5839 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6560 5839 603 41 0 6519 0 vsize: 26240 [startup+90.0025 s] Raw data (loadavg): 0.93 0.92 0.90 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 28584 0 0 0 8881 116 0 0 25 0 1 0 548292885 28049408 6126 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6848 6126 603 41 0 6807 0 vsize: 27392 [startup+100.002 s] Raw data (loadavg): 0.94 0.92 0.90 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 29261 0 0 0 9879 118 0 0 25 0 1 0 548292885 31211520 6803 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7620 6803 603 41 0 7579 0 vsize: 30480 [startup+110.002 s] Raw data (loadavg): 0.95 0.92 0.90 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 29965 0 0 0 10875 121 0 0 25 0 1 0 548292885 32587776 7125 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7956 7125 603 41 0 7915 0 vsize: 31824 [startup+120.002 s] Raw data (loadavg): 0.96 0.93 0.90 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 29965 0 0 0 11875 121 0 0 25 0 1 0 548292885 32587776 7125 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7956 7125 603 41 0 7915 0 vsize: 31824 [startup+130.002 s] Raw data (loadavg): 0.96 0.93 0.90 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30350 0 0 0 12874 123 0 0 25 0 1 0 548292885 32489472 7175 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7932 7175 603 41 0 7891 0 vsize: 31728 [startup+140.002 s] Raw data (loadavg): 0.97 0.93 0.90 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30350 0 0 0 13874 123 0 0 25 0 1 0 548292885 32489472 7175 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7932 7175 603 41 0 7891 0 vsize: 31728 [startup+150.003 s] Raw data (loadavg): 0.97 0.93 0.90 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30710 0 0 0 14872 125 0 0 25 0 1 0 548292885 31211520 6871 4294967295 134512640 134672761 3221224544 3221223640 134616156 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7620 6871 603 41 0 7579 0 vsize: 30480 [startup+160.002 s] Raw data (loadavg): 0.98 0.93 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30712 0 0 0 15871 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7620 6873 603 41 0 7579 0 vsize: 30480 [startup+170.002 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30712 0 0 0 16872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7620 6873 603 41 0 7579 0 vsize: 30480 [startup+180.002 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30712 0 0 0 17872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223584 134612827 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7620 6873 603 41 0 7579 0 vsize: 30480 [startup+190.002 s] Raw data (loadavg): 0.98 0.94 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30712 0 0 0 18872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7620 6873 603 41 0 7579 0 vsize: 30480 [startup+200.002 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30712 0 0 0 19872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223536 134565056 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7620 6873 603 41 0 7579 0 vsize: 30480 [startup+210.002 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30747 0 0 0 20872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223584 134603506 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7620 6873 603 41 0 7579 0 vsize: 30480 [startup+220.002 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 30747 0 0 0 21872 125 0 0 25 0 1 0 548292885 31211520 6873 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7620 6873 603 41 0 7579 0 vsize: 30480 [startup+230.002 s] Raw data (loadavg): 0.99 0.94 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 31746 0 0 0 22869 128 0 0 25 0 1 0 548292885 35414016 7872 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8646 7872 603 41 0 8605 0 vsize: 34584 [startup+240.003 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 33596 0 0 0 23864 134 0 0 25 0 1 0 548292885 42987520 9722 4294967295 134512640 134672761 3221224544 3221223744 134610614 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10495 9722 603 41 0 10454 0 vsize: 41980 [startup+250.003 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35065 0 0 0 24861 137 0 0 25 0 1 0 548292885 48726016 11152 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11896 11152 603 41 0 11855 0 vsize: 47584 [startup+260.002 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35065 0 0 0 25861 137 0 0 25 0 1 0 548292885 48726016 11152 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11896 11152 603 41 0 11855 0 vsize: 47584 [startup+270.002 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35065 0 0 0 26861 137 0 0 25 0 1 0 548292885 48726016 11152 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11896 11152 603 41 0 11855 0 vsize: 47584 [startup+280.002 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 27857 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12244 11441 603 41 0 12203 0 vsize: 48976 [startup+290.008 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 28858 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12244 11441 603 41 0 12203 0 vsize: 48976 [startup+300.111 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 29868 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12244 11441 603 41 0 12203 0 vsize: 48976 [startup+310.113 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 30869 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615526 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12244 11441 603 41 0 12203 0 vsize: 48976 [startup+320.121 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 31870 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12244 11441 603 41 0 12203 0 vsize: 48976 [startup+330.122 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 32870 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12244 11441 603 41 0 12203 0 vsize: 48976 [startup+340.122 s] Raw data (loadavg): 0.99 0.95 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 33870 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12244 11441 603 41 0 12203 0 vsize: 48976 [startup+350.121 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35762 0 0 0 34870 140 0 0 25 0 1 0 548292885 50151424 11441 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12244 11441 603 41 0 12203 0 vsize: 48976 [startup+360.121 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35915 0 0 0 35869 141 0 0 25 0 1 0 548292885 48648192 11135 4294967295 134512640 134672761 3221224544 3221223728 134615985 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11877 11135 603 41 0 11836 0 vsize: 47508 [startup+370.121 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35915 0 0 0 36868 141 0 0 25 0 1 0 548292885 48648192 11135 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11135 603 41 0 11836 0 vsize: 47508 [startup+380.121 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35915 0 0 0 37869 141 0 0 25 0 1 0 548292885 48648192 11135 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11135 603 41 0 11836 0 vsize: 47508 [startup+390.122 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 35915 0 0 0 38869 141 0 0 25 0 1 0 548292885 48648192 11135 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11135 603 41 0 11836 0 vsize: 47508 [startup+400.121 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 39867 143 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+410.12 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 40867 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+420.122 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 41867 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+430.122 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 42867 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+440.122 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 43868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+450.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 44868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+460.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 45868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+470.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 46868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+480.122 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 47868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+490.124 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 48868 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+500.123 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 49869 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+510.133 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 50870 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+520.132 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36205 0 0 0 51870 144 0 0 25 0 1 0 548292885 48648192 11137 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11877 11137 603 41 0 11836 0 vsize: 47508 [startup+530.134 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36819 0 0 0 52868 146 0 0 25 0 1 0 548292885 50962432 11707 4294967295 134512640 134672761 3221224544 3221223584 134613815 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12442 11707 603 41 0 12401 0 vsize: 49768 [startup+540.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36819 0 0 0 53869 146 0 0 25 0 1 0 548292885 50962432 11707 4294967295 134512640 134672761 3221224544 3221223584 134612478 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12442 11707 603 41 0 12401 0 vsize: 49768 [startup+550.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36819 0 0 0 54869 146 0 0 25 0 1 0 548292885 50962432 11707 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12442 11707 603 41 0 12401 0 vsize: 49768 [startup+560.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 36819 0 0 0 55869 146 0 0 25 0 1 0 548292885 50962432 11707 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12442 11707 603 41 0 12401 0 vsize: 49768 [startup+570.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 37132 0 0 0 56868 147 0 0 25 0 1 0 548292885 52281344 12020 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12764 12020 603 41 0 12723 0 vsize: 51056 [startup+580.134 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 38454 0 0 0 57865 150 0 0 25 0 1 0 548292885 57761792 13342 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14102 13342 603 41 0 14061 0 vsize: 56408 [startup+590.133 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39749 0 0 0 58861 154 0 0 25 0 1 0 548292885 62787584 14592 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15329 14592 603 41 0 15288 0 vsize: 61316 [startup+600.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39749 0 0 0 59861 154 0 0 25 0 1 0 548292885 62787584 14592 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15329 14592 603 41 0 15288 0 vsize: 61316 [startup+610.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39749 0 0 0 60862 154 0 0 25 0 1 0 548292885 62787584 14592 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15329 14592 603 41 0 15288 0 vsize: 61316 [startup+620.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39749 0 0 0 61862 154 0 0 25 0 1 0 548292885 62787584 14592 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15329 14592 603 41 0 15288 0 vsize: 61316 [startup+630.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39749 0 0 0 62862 154 0 0 25 0 1 0 548292885 62787584 14592 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15329 14592 603 41 0 15288 0 vsize: 61316 [startup+640.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39799 0 0 0 63862 154 0 0 25 0 1 0 548292885 62697472 14573 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15307 14573 603 41 0 15266 0 vsize: 61228 [startup+650.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39799 0 0 0 64862 154 0 0 25 0 1 0 548292885 62697472 14573 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15307 14573 603 41 0 15266 0 vsize: 61228 [startup+660.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39799 0 0 0 65863 154 0 0 25 0 1 0 548292885 62697472 14573 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15307 14573 603 41 0 15266 0 vsize: 61228 [startup+670.136 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39799 0 0 0 66863 154 0 0 25 0 1 0 548292885 62697472 14573 4294967295 134512640 134672761 3221224544 3221223584 134614239 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15307 14573 603 41 0 15266 0 vsize: 61228 [startup+680.135 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39799 0 0 0 67863 154 0 0 25 0 1 0 548292885 62697472 14573 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15307 14573 603 41 0 15266 0 vsize: 61228 [startup+690.137 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39802 0 0 0 68863 154 0 0 25 0 1 0 548292885 62693376 14575 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15306 14575 603 41 0 15265 0 vsize: 61224 [startup+700.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39802 0 0 0 69864 154 0 0 25 0 1 0 548292885 62693376 14575 4294967295 134512640 134672761 3221224544 3221223680 134614685 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15306 14575 603 41 0 15265 0 vsize: 61224 [startup+710.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39802 0 0 0 70864 154 0 0 25 0 1 0 548292885 62693376 14575 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15306 14575 603 41 0 15265 0 vsize: 61224 [startup+720.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 39802 0 0 0 71864 154 0 0 25 0 1 0 548292885 62693376 14575 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15306 14575 603 41 0 15265 0 vsize: 61224 [startup+730.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 40595 0 0 0 72863 156 0 0 25 0 1 0 548292885 65970176 15368 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16106 15368 603 41 0 16065 0 vsize: 64424 [startup+740.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 42100 0 0 0 73859 160 0 0 25 0 1 0 548292885 72142848 16873 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17613 16873 603 41 0 17572 0 vsize: 70452 [startup+750.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 43629 0 0 0 74856 162 0 0 25 0 1 0 548292885 78422016 18402 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19146 18402 603 41 0 19105 0 vsize: 76584 [startup+760.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45366 0 0 0 75852 167 0 0 25 0 1 0 548292885 85594112 20139 4294967295 134512640 134672761 3221224544 3221223552 134522369 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20897 20139 603 41 0 20856 0 vsize: 83588 [startup+770.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 76851 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21071 20342 603 41 0 21030 0 vsize: 84284 [startup+780.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 77851 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21071 20342 603 41 0 21030 0 vsize: 84284 [startup+790.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 78852 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615711 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21071 20342 603 41 0 21030 0 vsize: 84284 [startup+800.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 79852 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21071 20342 603 41 0 21030 0 vsize: 84284 [startup+810.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 80852 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21071 20342 603 41 0 21030 0 vsize: 84284 [startup+820.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45592 0 0 0 81852 168 0 0 25 0 1 0 548292885 86306816 20342 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21071 20342 603 41 0 21030 0 vsize: 84284 [startup+830.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 45593 0 0 0 82852 168 0 0 25 0 1 0 548292885 86306816 20343 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21071 20343 603 41 0 21030 0 vsize: 84284 [startup+840.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 46298 0 0 0 83851 170 0 0 25 0 1 0 548292885 89194496 21048 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21776 21048 603 41 0 21735 0 vsize: 87104 [startup+850.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 47724 0 0 0 84847 174 0 0 25 0 1 0 548292885 95076352 22474 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23212 22474 603 41 0 23171 0 vsize: 92848 [startup+860.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49190 0 0 0 85842 179 0 0 25 0 1 0 548292885 101126144 23940 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24689 23940 603 41 0 24648 0 vsize: 98756 [startup+870.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 86842 179 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25004 24271 603 41 0 24963 0 vsize: 100016 [startup+880.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 87842 179 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25004 24271 603 41 0 24963 0 vsize: 100016 [startup+890.138 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 88842 179 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25004 24271 603 41 0 24963 0 vsize: 100016 [startup+900.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 89842 179 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25004 24271 603 41 0 24963 0 vsize: 100016 [startup+910.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 90842 180 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25004 24271 603 41 0 24963 0 vsize: 100016 [startup+920.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49574 0 0 0 91842 180 0 0 25 0 1 0 548292885 102416384 24271 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25004 24271 603 41 0 24963 0 vsize: 100016 [startup+930.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49866 0 0 0 92839 182 0 0 25 0 1 0 548292885 102334464 24255 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24984 24255 603 41 0 24943 0 vsize: 99936 [startup+940.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49866 0 0 0 93838 183 0 0 25 0 1 0 548292885 102313984 24250 4294967295 134512640 134672761 3221224544 3221223728 134615755 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24250 603 41 0 24938 0 vsize: 99916 [startup+950.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49866 0 0 0 94838 183 0 0 25 0 1 0 548292885 102313984 24250 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24250 603 41 0 24938 0 vsize: 99916 [startup+960.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49866 0 0 0 95838 183 0 0 25 0 1 0 548292885 102313984 24250 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24250 603 41 0 24938 0 vsize: 99916 [startup+970.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49866 0 0 0 96838 184 0 0 25 0 1 0 548292885 102313984 24250 4294967295 134512640 134672761 3221224544 3221223584 134614340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24250 603 41 0 24938 0 vsize: 99916 [startup+980.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 97837 184 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223640 134616108 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+990.139 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 98837 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1000.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 99837 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1010.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 100837 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1020.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 101837 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1030.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 102838 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1040.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 103838 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1050.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 104838 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1060.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 105838 185 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1070.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 106836 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1080.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 107836 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1090.14 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 108837 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223552 134542729 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1100.15 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 109837 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1110.15 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 110838 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1120.15 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 111838 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615529 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1130.16 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 112839 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223640 134616350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1140.16 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 113839 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1150.16 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 114840 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1160.16 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 115840 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1170.17 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 116841 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223584 134614286 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1180.17 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 117841 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1190.17 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 118841 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223584 134613815 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 [startup+1200.17 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 15047 Raw data (stat): 15047 (minisat+) R 15046 28099 28098 0 -1 0 49867 0 0 0 119841 186 0 0 25 0 1 0 548292885 102313984 24251 4294967295 134512640 134672761 3221224544 3221223584 134613748 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24979 24251 603 41 0 24938 0 vsize: 99916 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.22 s] Raw data (loadavg): 0.99 0.97 0.91 1/54 15047 Raw data (stat): 15047 (minisat+) Z 15046 28099 28098 0 -1 12 49868 0 0 0 119842 191 0 0 25 0 1 0 548292885 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.22 CPU time (s): 1200.34 CPU user time (s): 1198.42 CPU system time (s): 1.91671 CPU usage (%): 100.01 Max. virtual memory (Kb): 100016 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####