Name | normalized-opb/submitted/manquinho/synthesis-ptl-cmos-circuits/normalized-C432.opb |
MD5SUM | 6292e63147fb202dc159fbf5a9ff5c77 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 4822 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 771 |
Biggest coefficient in the objective function | 61 |
Number of bits for the biggest coefficient in the objective function | 6 |
Sum of the numbers in the objective function | 33355 |
Number of bits of the sum of numbers in the objective function | 16 |
Biggest number in a constraint | 61 |
Number of bits of the biggest number in a constraint | 6 |
Biggest sum of numbers in a constraint | 33355 |
Number of bits of the biggest sum of numbers | 16 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.02584 |
Number of variables | 771 |
Total number of constraints | 1951 |
Number of constraints which are clauses | 1949 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 2 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 42 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc31 THE 2005-04-14 00:37:30 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4008 boxname=wulflinc31 idbench=248 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6292e63147fb202dc159fbf5a9ff5c77 /oldhome/oroussel/tmp/wulflinc31/normalized-C432.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc31/normalized-C432.opb /oldhome/oroussel/tmp/wulflinc31/normalized-C432.opb IDLAUNCH: 4008 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 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.153 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: 906480 kB Buffers: 35604 kB Cached: 54104 kB SwapCached: 392 kB Active: 51092 kB Inactive: 41704 kB HighTotal: 131008 kB HighFree: 73276 kB LowTotal: 903652 kB LowFree: 833204 kB SwapTotal: 2097892 kB SwapFree: 2097452 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6832 kB Slab: 29804 kB Committed_AS: 63476 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-14 00:57:42 (client local time) WITH STATUS 10 IN 1210.11 SECONDS stats: 4008 7 1210.11 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 1905 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................. c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 1891 9233 | 567 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 704/704 c | 0 | 1808 8928 | -- 0 -- -- | -- | -83/-305 c | 0 | 1808 8928 | 723 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 0.097985 s) c ============================================================================== c [1mFound solution: 7184[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:125007 Base: 2 5 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 296770 697520 | 89030 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/114054 c -- var.elim.: 2000/114054 c -- var.elim.: 3000/114054 c -- var.elim.: 4000/114054 c -- var.elim.: 5000/114054 c -- var.elim.: 6000/114054 c -- var.elim.: 7000/114054 c -- var.elim.: 8000/114054 c -- var.elim.: 9000/114054 c -- var.elim.: 10000/114054 c -- var.elim.: 11000/114054 c -- var.elim.: 12000/114054 c -- var.elim.: 13000/114054 c -- var.elim.: 14000/114054 c -- var.elim.: 15000/114054 c -- var.elim.: 16000/114054 c -- var.elim.: 17000/114054 c -- var.elim.: 18000/114054 c -- var.elim.: 19000/114054 c -- var.elim.: 20000/114054 c -- var.elim.: 21000/114054 c -- var.elim.: 22000/114054 c -- var.elim.: 23000/114054 c -- var.elim.: 24000/114054 c -- var.elim.: 25000/114054 c -- var.elim.: 26000/114054 c -- var.elim.: 27000/114054 c -- var.elim.: 28000/114054 c -- var.elim.: 29000/114054 c -- var.elim.: 30000/114054 c -- var.elim.: 31000/114054 c -- var.elim.: 32000/114054 c -- var.elim.: 33000/114054 c -- var.elim.: 34000/114054 c -- var.elim.: 35000/114054 c -- var.elim.: 36000/114054 c -- var.elim.: 37000/114054 c -- var.elim.: 38000/114054 c -- var.elim.: 39000/114054 c -- var.elim.: 40000/114054 c -- var.elim.: 41000/114054 c -- var.elim.: 42000/114054 c -- var.elim.: 43000/114054 c -- var.elim.: 44000/114054 c -- var.elim.: 45000/114054 c -- var.elim.: 46000/114054 c -- var.elim.: 47000/114054 c -- var.elim.: 48000/114054 c -- var.elim.: 49000/114054 c -- var.elim.: 50000/114054 c -- var.elim.: 51000/114054 c -- var.elim.: 52000/114054 c -- var.elim.: 53000/114054 c -- var.elim.: 54000/114054 c -- var.elim.: 55000/114054 c -- var.elim.: 56000/114054 c -- var.elim.: 57000/114054 c -- var.elim.: 58000/114054 c -- var.elim.: 59000/114054 c -- var.elim.: 60000/114054 c -- var.elim.: 61000/114054 c -- var.elim.: 62000/114054 c -- var.elim.: 63000/114054 c -- var.elim.: 64000/114054 c -- var.elim.: 65000/114054 c -- var.elim.: 66000/114054 c -- var.elim.: 67000/114054 c -- var.elim.: 68000/114054 c -- var.elim.: 69000/114054 c -- var.elim.: 70000/114054 c -- var.elim.: 71000/114054 c -- var.elim.: 72000/114054 c -- var.elim.: 73000/114054 c -- var.elim.: 74000/114054 c -- var.elim.: 75000/114054 c -- var.elim.: 76000/114054 c -- var.elim.: 77000/114054 c -- var.elim.: 78000/114054 c -- var.elim.: 79000/114054 c -- var.elim.: 80000/114054 c -- var.elim.: 81000/114054 c -- var.elim.: 82000/114054 c -- var.elim.: 83000/114054 c -- var.elim.: 84000/114054 c -- var.elim.: 85000/114054 c -- var.elim.: 86000/114054 c -- var.elim.: 87000/114054 c -- var.elim.: 88000/114054 c -- var.elim.: 89000/114054 c -- var.elim.: 90000/114054 c -- var.elim.: 91000/114054 c -- var.elim.: 92000/114054 c -- var.elim.: 93000/114054 c -- var.elim.: 94000/114054 c -- var.elim.: 95000/114054 c -- var.elim.: 96000/114054 c -- var.elim.: 97000/114054 c -- var.elim.: 98000/114054 c -- var.elim.: 99000/114054 c -- var.elim.: 100000/114054 c -- var.elim.: 101000/114054 c -- var.elim.: 102000/114054 c -- var.elim.: 103000/114054 c -- var.elim.: 104000/114054 c -- var.elim.: 105000/114054 c -- var.elim.: 106000/114054 c -- var.elim.: 107000/114054 c -- var.elim.: 108000/114054 c -- var.elim.: 109000/114054 c -- var.elim.: 110000/114054 c -- var.elim.: 111000/114054 c -- var.elim.: 112000/114054 c -- var.elim.: 113000/114054 c -- var.elim.: 114000/114054 c -- var.elim.: 114054/114054 c -- var.elim.: 1000/60779 c -- var.elim.: 2000/60779 c -- var.elim.: 3000/60779 c -- var.elim.: 4000/60779 c -- var.elim.: 5000/60779 c -- var.elim.: 6000/60779 c -- var.elim.: 7000/60779 c -- var.elim.: 8000/60779 c -- var.elim.: 9000/60779 c -- var.elim.: 10000/60779 c -- var.elim.: 11000/60779 c -- var.elim.: 12000/60779 c -- var.elim.: 13000/60779 c -- var.elim.: 14000/60779 c -- var.elim.: 15000/60779 c -- var.elim.: 16000/60779 c -- var.elim.: 17000/60779 c -- var.elim.: 18000/60779 c -- var.elim.: 19000/60779 c -- var.elim.: 20000/60779 c -- var.elim.: 21000/60779 c -- var.elim.: 22000/60779 c -- var.elim.: 23000/60779 c -- var.elim.: 24000/60779 c -- var.elim.: 25000/60779 c -- var.elim.: 26000/60779 c -- var.elim.: 27000/60779 c -- var.elim.: 28000/60779 c -- var.elim.: 29000/60779 c -- var.elim.: 30000/60779 c -- var.elim.: 31000/60779 c -- var.elim.: 32000/60779 c -- var.elim.: 33000/60779 c -- var.elim.: 34000/60779 c -- var.elim.: 35000/60779 c -- var.elim.: 36000/60779 c -- var.elim.: 37000/60779 c -- var.elim.: 38000/60779 c -- var.elim.: 39000/60779 c -- var.elim.: 40000/60779 c -- var.elim.: 41000/60779 c -- var.elim.: 42000/60779 c -- var.elim.: 43000/60779 c -- var.elim.: 44000/60779 c -- var.elim.: 45000/60779 c -- var.elim.: 46000/60779 c -- var.elim.: 47000/60779 c -- var.elim.: 48000/60779 c -- var.elim.: 49000/60779 c -- var.elim.: 50000/60779 c -- var.elim.: 51000/60779 c -- var.elim.: 52000/60779 c -- var.elim.: 53000/60779 c -- var.elim.: 54000/60779 c -- var.elim.: 55000/60779 c -- var.elim.: 56000/60779 c -- var.elim.: 57000/60779 c -- var.elim.: 58000/60779 c -- var.elim.: 59000/60779 c -- var.elim.: 60000/60779 c -- var.elim.: 60779/60779 c -- var.elim.: 4/4 c -- subsuming c -- var.elim.: 1000/15340 c -- var.elim.: 2000/15340 c -- var.elim.: 3000/15340 c -- var.elim.: 4000/15340 c -- var.elim.: 5000/15340 c -- var.elim.: 6000/15340 c -- var.elim.: 7000/15340 c -- var.elim.: 8000/15340 c -- var.elim.: 9000/15340 c -- var.elim.: 10000/15340 c -- var.elim.: 11000/15340 c -- var.elim.: 12000/15340 c -- var.elim.: 13000/15340 c -- var.elim.: 14000/15340 c -- var.elim.: 15000/15340 c -- var.elim.: 15340/15340 c -- var.elim.: 1000/2726 c -- var.elim.: 2000/2726 c -- var.elim.: 2726/2726 c -- var.elim.: 632/632 c -- var.elim.: 1000/1139 c -- var.elim.: 1139/1139 c -- subsuming c -- var.elim.: 1000/1618 c -- var.elim.: 1618/1618 c -- var.elim.: 6/6 c | 0 | 262116 933394 | -- 0 -- -- | -- | -34654/235875 c | 0 | 262116 933394 | 104846 0 0 nan | 0.000 % | c | 100 | 261202 929211 | 114928 97 438 4.5 | 0.259 % | c | 250 | 261202 929211 | 126421 247 1923 7.8 | 0.259 % | c | 475 | 261202 929211 | 139063 472 6021 12.8 | 0.259 % | c | 813 | 260676 927480 | 152662 808 8231 10.2 | 0.391 % | c | 1319 | 260676 927480 | 167928 1314 13524 10.3 | 0.391 % | c | 2078 | 260676 927480 | 184721 2073 24891 12.0 | 0.391 % | c | 3217 | 260419 926501 | 202993 3209 42773 13.3 | 0.458 % | c | 4925 | 260419 926501 | 223292 4917 283057 57.6 | 0.458 % | c | 7487 | 260141 925429 | 245359 7472 328667 44.0 | 0.544 % | c | 11331 | 259969 924696 | 269717 11314 499456 44.1 | 0.600 % | c | 17097 | 259567 922609 | 296229 17070 1762575 103.3 | 0.735 % | c | 25746 | 259543 922385 | 325822 25718 2527451 98.3 | 0.755 % | c | 38720 | 259506 921624 | 358354 38689 7463322 192.9 | 0.773 % | c | 58181 | 259506 921624 | 394189 58150 8653986 148.8 | 0.773 % | c | 87373 | 259354 920007 | 433354 87340 17186182 196.8 | 0.793 % | c | 131162 | 259305 919772 | 476599 131125 30044658 229.1 | 0.816 % | c ============================================================================== c (current CPU-time: 999.037 s) c ============================================================================== c [1mFound solution: 7115[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:113802 Base: 2 5 2 2 c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 190118 | 526040 1542892 | 157811 190081 45016200 236.8 | 0.816 % | c -- subsuming c -- var.elim.: 1000/113128 c -- var.elim.: 2000/113128 c -- var.elim.: 3000/113128 c -- var.elim.: 4000/113128 c -- var.elim.: 5000/113128 c -- var.elim.: 6000/113128 c -- var.elim.: 7000/113128 c -- var.elim.: 8000/113128 c -- var.elim.: 9000/113128 c -- var.elim.: 10000/113128 c -- var.elim.: 11000/113128 c -- var.elim.: 12000/113128 c -- var.elim.: 13000/113128 c -- var.elim.: 14000/113128 c -- var.elim.: 15000/113128 c -- var.elim.: 16000/113128 c -- var.elim.: 17000/113128 c -- var.elim.: 18000/113128 c -- var.elim.: 19000/113128 c -- var.elim.: 20000/113128 c -- var.elim.: 21000/113128 c -- var.elim.: 22000/113128 c -- var.elim.: 23000/113128 c -- var.elim.: 24000/113128 c -- var.elim.: 25000/113128 c -- var.elim.: 26000/113128 c -- var.elim.: 27000/113128 c -- var.elim.: 28000/113128 c -- var.elim.: 29000/113128 c -- var.elim.: 30000/113128 c -- var.elim.: 31000/113128 c -- var.elim.: 32000/113128 c -- var.elim.: 33000/113128 c -- var.elim.: 34000/113128 c -- var.elim.: 35000/113128 c -- var.elim.: 36000/113128 c -- var.elim.: 37000/113128 c -- var.elim.: 38000/113128 c -- var.elim.: 39000/113128 c -- var.elim.: 40000/113128 c -- var.elim.: 41000/113128 c -- var.elim.: 42000/113128 c -- var.elim.: 43000/113128 c -- var.elim.: 44000/113128 c -- var.elim.: 45000/113128 c -- var.elim.: 46000/113128 c -- var.elim.: 47000/113128 c -- var.elim.: 48000/113128 c -- var.elim.: 49000/113128 c -- var.elim.: 50000/113128 c -- var.elim.: 51000/113128 c -- var.elim.: 52000/113128 c -- var.elim.: 53000/113128 c -- var.elim.: 54000/113128 c -- var.elim.: 55000/113128 c -- var.elim.: 56000/113128 c -- var.elim.: 57000/113128 c -- var.elim.: 58000/113128 c -- var.elim.: 59000/113128 c -- var.elim.: 60000/113128 c -- var.elim.: 61000/113128 c -- var.elim.: 62000/113128 c -- var.elim.: 63000/113128 c -- var.elim.: 64000/113128 c -- var.elim.: 65000/113128 c -- var.elim.: 66000/113128 c -- var.elim.: 67000/113128 c -- var.elim.: 68000/113128 c -- var.elim.: 69000/113128 c -- var.elim.: 70000/113128 c -- var.elim.: 71000/113128 c -- var.elim.: 72000/113128 c -- var.elim.: 73000/113128 c -- var.elim.: 74000/113128 c -- var.elim.: 75000/113128 c -- var.elim.: 76000/113128 c -- var.elim.: 77000/113128 c -- var.elim.: 78000/113128 c -- var.elim.: 79000/113128 c -- var.elim.: 80000/113128 c -- var.elim.: 81000/113128 c -- var.elim.: 82000/113128 c -- var.elim.: 83000/113128 c -- var.elim.: 84000/113128 c -- var.elim.: 85000/113128 c -- var.elim.: 86000/113128 c -- var.elim.: 87000/113128 c -- var.elim.: 88000/113128 c -- var.elim.: 89000/113128 c -- var.elim.: 90000/113128 c -- var.elim.: 91000/113128 c -- var.elim.: 92000/113128 c -- var.elim.: 93000/113128 c -- var.elim.: 94000/113128 c -- var.elim.: 95000/113128 c -- var.elim.: 96000/113128 c -- var.elim.: 97000/113128 c -- var.elim.: 98000/113128 c -- var.elim.: 99000/113128 c -- var.elim.: 100000/113128 c -- var.elim.: 101000/113128 c -- var.elim.: 102000/113128 c -- var.elim.: 103000/113128 c -- var.elim.: 104000/113128 c -- var.elim.: 105000/113128 c -- var.elim.: 106000/113128 c -- var.elim.: 107000/113128 c -- var.elim.: 108000/113128 c -- var.elim.: 109000/113128 c -- var.elim.: 110000/113128 c -- var.elim.: 111000/113128 c -- var.elim.: 112000/113128 c -- var.elim.: 113000/113128 c -- var.elim.: 113128/113128 c -- var.elim.: 1000/59060 c -- var.elim.: 2000/59060 c -- var.elim.: 3000/59060 c -- var.elim.: 4000/59060 c -- var.elim.: 5000/59060 c -- var.elim.: 6000/59060 c -- var.elim.: 7000/59060 c -- var.elim.: 8000/59060 c -- var.elim.: 9000/59060 c -- var.elim.: 10000/59060 c -- var.elim.: 11000/59060 c -- var.elim.: 12000/59060 c -- var.elim.: 13000/59060 c -- var.elim.: 14000/59060 c -- var.elim.: 15000/59060 c -- var.elim.: 16000/59060 c -- var.elim.: 17000/59060 c -- var.elim.: 18000/59060 c -- var.elim.: 19000/59060 c -- var.elim.: 20000/59060 c -- var.elim.: 21000/59060 c -- var.elim.: 22000/59060 c -- var.elim.: 23000/59060 c -- var.elim.: 24000/59060 c -- var.elim.: 25000/59060 c -- var.elim.: 26000/59060 c -- var.elim.: 27000/59060 c -- var.elim.: 28000/59060 c -- var.elim.: 29000/59060 c -- var.elim.: 30000/59060 c -- var.elim.: 31000/59060 c -- var.elim.: 32000/59060 c -- var.elim.: 33000/59060 c -- var.elim.: 34000/59060 c -- var.elim.: 35000/59060 c -- var.elim.: 36000/59060 c -- var.elim.: 37000/59060 c -- var.elim.: 38000/59060 c -- var.elim.: 39000/59060 c -- var.elim.: 40000/59060 c -- var.elim.: 41000/59060 c -- var.elim.: 42000/59060 c -- var.elim.: 43000/59060 c -- var.elim.: 44000/59060 c -- var.elim.: 45000/59060 c -- var.elim.: 46000/59060 c -- var.elim.: 47000/59060 c -- var.elim.: 48000/59060 c -- var.elim.: 49000/59060 c -- var.elim.: 50000/59060 c -- var.elim.: 51000/59060 c -- var.elim.: 52000/59060 c -- var.elim.: 53000/59060 c -- var.elim.: 54000/59060 c -- var.elim.: 55000/59060 c -- var.elim.: 56000/59060 c -- var.elim.: 57000/59060 c -- var.elim.: 58000/59060 c -- var.elim.: 59000/59060 c -- var.elim.: 59060/59060 c -- var.elim.: 828/828 c -- var.elim.: 795/795 c -- subsuming c -- var.elim.: 1000/16245 c -- var.elim.: 2000/16245 c -- var.elim.: 3000/16245 c -- var.elim.: 4000/16245 c -- var.elim.: 5000/16245 c -- var.elim.: 6000/16245 c -- var.elim.: 7000/16245 c -- var.elim.: 8000/16245 c -- var.elim.: 9000/16245 c -- var.elim.: 10000/16245 c -- var.elim.: 11000/16245 c -- var.elim.: 12000/16245 c -- var.elim.: 13000/16245 c -- var.elim.: 14000/16245 c -- var.elim.: 15000/16245 c -- var.elim.: 16000/16245 c -- var.elim.: 16245/16245 c -- var.elim.: 1000/1470 c -- var.elim.: 1470/1470 c -- subsuming c -- var.elim.: 537/537 c -- var.elim.: 769/769 c | 190118 | 493231 1767722 | -- 190081 -- -- | -- | -32777/224908 c | 190118 | 493231 1767722 | 197292 155283 12784591 82.3 | 0.816 % | c | 190219 | 493231 1767722 | 217021 155384 12786644 82.3 | 0.446 % | c | 190369 | 493231 1767722 | 238723 155534 12787793 82.2 | 0.446 % | c | 190594 | 493042 1767082 | 262495 155758 12790751 82.1 | 0.467 % | c | 190931 | 493042 1767082 | 288745 156095 12794915 82.0 | 0.467 % | c | 191437 | 493042 1767082 | 317619 156601 12808051 81.8 | 0.467 % | c | 192197 | 493042 1767082 | 349381 157361 12825714 81.5 | 0.467 % | c | 193336 | 492763 1765847 | 384102 158498 12847118 81.1 | 0.507 % | c | 195045 | 492763 1765847 | 422512 160207 12875831 80.4 | 0.507 % | c | 197607 | 492763 1765847 | 464763 162769 12912996 79.3 | 0.507 % | c | 201453 | 492763 1765847 | 511240 166615 13101379 78.6 | 0.507 % | c | 207221 | 492761 1765826 | 562361 172380 14046083 81.5 | 0.508 % | c | 215870 | 492761 1765826 | 618598 181029 14431419 79.7 | 0.508 % | c c *** TERMINATED *** s SATISFIABLE v -x1 -x2 -x3 -x4 -x5 -x6 x7 x8 x9 x10 -x11 -x12 -x13 -x14 -x15 -x16 -x17 -x18 -x19 -x20 -x21 -x22 -x23 -x24 -x25 -x26 -x27 -x28 -x29 -x30 -x31 -x32 -x33 -x34 -x35 -x36 -x37 -x38 -x39 -x40 -x41 -x42 x43 x44 -x45 -x46 -x47 x48 -x49 x50 -x51 -x52 -x53 -x54 x55 x56 x57 x58 -x59 -x60 -x61 x62 -x63 x64 -x65 -x66 -x67 -x68 -x69 -x70 -x71 -x72 -x73 -x74 -x75 -x76 -x77 -x78 -x79 -x80 -x81 -x82 -x83 -x84 -x85 -x86 x87 -x88 -x89 -x90 -x91 -x92 -x93 -x94 -x95 -x96 -x97 -x98 -x99 -x100 -x101 -x102 x103 x104 x105 -x106 -x107 -x108 -x109 x110 x111 x112 -x113 -x114 -x115 -x116 -x117 -x118 -x119 -x120 -x121 -x122 -x123 -x124 -x125 -x126 -x127 -x128 -x129 -x130 -x131 -x132 -x133 -x134 x135 -x136 x137 -x138 -x139 -x140 -x141 -x142 -x143 -x144 -x145 -x146 -x147 -x148 -x149 -x150 -x151 -x152 -x153 -x154 -x155 -x156 -x157 -x158 -x159 -x160 -x161 -x162 -x163 -x164 -#### 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.84 0.94 0.90 2/54 28559 Raw data (stat): 28559 (runsolver) R 28558 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480313806 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0003 s] Raw data (loadavg): 0.87 0.94 0.90 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 17269 0 0 0 948 49 0 0 25 0 1 0 480313806 73367552 16319 4294967295 134512640 134672761 3221224576 3221223024 134643493 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17912 16319 603 41 0 17871 0 vsize: 71648 [startup+20.0015 s] Raw data (loadavg): 0.89 0.94 0.90 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 17455 0 0 0 1932 65 0 0 25 0 1 0 480313806 73830400 16393 4294967295 134512640 134672761 3221224576 3221222880 1074972061 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18025 16393 603 41 0 17984 0 vsize: 72100 [startup+30.0023 s] Raw data (loadavg): 0.90 0.94 0.90 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 17455 0 0 0 2932 65 0 0 25 0 1 0 480313806 73043968 16221 4294967295 134512640 134672761 3221224576 3221222976 134604097 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17833 16221 603 41 0 17792 0 vsize: 71332 [startup+40.0029 s] Raw data (loadavg): 0.92 0.94 0.90 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 17455 0 0 0 3932 65 0 0 25 0 1 0 480313806 73043968 16221 4294967295 134512640 134672761 3221224576 3221223120 134621194 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17833 16221 603 41 0 17792 0 vsize: 71332 [startup+50.0041 s] Raw data (loadavg): 0.93 0.94 0.90 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 17774 0 0 0 4931 66 0 0 25 0 1 0 480313806 73043968 16251 4294967295 134512640 134672761 3221224576 3221223024 134643612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17833 16251 603 41 0 17792 0 vsize: 71332 [startup+60.0043 s] Raw data (loadavg): 0.94 0.95 0.90 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 18457 0 0 0 5929 68 0 0 25 0 1 0 480313806 73306112 16295 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17897 16295 603 41 0 17856 0 vsize: 71588 [startup+70.0048 s] Raw data (loadavg): 0.95 0.95 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 18677 0 0 0 6928 69 0 0 25 0 1 0 480313806 74240000 16515 4294967295 134512640 134672761 3221224576 3221223760 134615948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18125 16515 603 41 0 18084 0 vsize: 72500 [startup+80.005 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 18807 0 0 0 7927 70 0 0 25 0 1 0 480313806 74813440 16645 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18265 16645 603 41 0 18224 0 vsize: 73060 [startup+90.0059 s] Raw data (loadavg): 0.96 0.95 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 18927 0 0 0 8927 70 0 0 25 0 1 0 480313806 75198464 16765 4294967295 134512640 134672761 3221224576 3221223616 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18359 16765 603 41 0 18318 0 vsize: 73436 [startup+100.005 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 19278 0 0 0 9926 72 0 0 25 0 1 0 480313806 76640256 17116 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18711 17116 603 41 0 18670 0 vsize: 74844 [startup+110.006 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20110 0 0 0 10924 74 0 0 25 0 1 0 480313806 80203776 17948 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19581 17948 603 41 0 19540 0 vsize: 78324 [startup+120.007 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20279 0 0 0 11923 74 0 0 25 0 1 0 480313806 80863232 18117 4294967295 134512640 134672761 3221224576 3221223760 134615794 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19742 18117 603 41 0 19701 0 vsize: 78968 [startup+130.006 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20504 0 0 0 12923 75 0 0 25 0 1 0 480313806 81780736 18342 4294967295 134512640 134672761 3221224576 3221223748 134615856 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19966 18342 603 41 0 19925 0 vsize: 79864 [startup+140.008 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20700 0 0 0 13923 75 0 0 25 0 1 0 480313806 82567168 18538 4294967295 134512640 134672761 3221224576 3221223760 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20158 18538 603 41 0 20117 0 vsize: 80632 [startup+150.008 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20761 0 0 0 14923 75 0 0 25 0 1 0 480313806 82833408 18599 4294967295 134512640 134672761 3221224576 3221223776 134610646 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20223 18599 603 41 0 20182 0 vsize: 80892 [startup+160.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20858 0 0 0 15923 76 0 0 25 0 1 0 480313806 83234816 18696 4294967295 134512640 134672761 3221224576 3221223616 134613012 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20321 18696 603 41 0 20280 0 vsize: 81284 [startup+170.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 20998 0 0 0 16922 76 0 0 25 0 1 0 480313806 83755008 18836 4294967295 134512640 134672761 3221224576 3221223752 134615853 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20448 18836 603 41 0 20407 0 vsize: 81792 [startup+180.008 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 21217 0 0 0 17922 77 0 0 25 0 1 0 480313806 84680704 19055 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20674 19055 603 41 0 20633 0 vsize: 82696 [startup+190.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 21673 0 0 0 18921 78 0 0 25 0 1 0 480313806 86663168 19511 4294967295 134512640 134672761 3221224576 3221223616 134614223 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21156 19511 603 41 0 21115 0 vsize: 84632 [startup+200.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 23003 0 0 0 19918 81 0 0 25 0 1 0 480313806 92098560 20841 4294967295 134512640 134672761 3221224576 3221223680 134603709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22485 20841 603 41 0 22444 0 vsize: 89940 [startup+210.009 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 24166 0 0 0 20917 83 0 0 25 0 1 0 480313806 96800768 22004 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 23633 22004 603 41 0 23592 0 vsize: 94532 [startup+220.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 25476 0 0 0 21915 85 0 0 25 0 1 0 480313806 102187008 23314 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24948 23314 603 41 0 24907 0 vsize: 99792 [startup+230.01 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 25922 0 0 0 22914 86 0 0 25 0 1 0 480313806 103940096 23760 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25376 23760 603 41 0 25335 0 vsize: 101504 [startup+240.011 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 26017 0 0 0 23914 86 0 0 25 0 1 0 480313806 104337408 23855 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25473 23855 603 41 0 25432 0 vsize: 101892 [startup+250.012 s] Raw data (loadavg): 0.99 0.96 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 26290 0 0 0 24913 87 0 0 25 0 1 0 480313806 105508864 24128 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25759 24128 603 41 0 25718 0 vsize: 103036 [startup+260.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 26644 0 0 0 25913 87 0 0 25 0 1 0 480313806 106946560 24482 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26110 24482 603 41 0 26069 0 vsize: 104440 [startup+270.013 s] Raw data (loadavg): 1.07 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 26841 0 0 0 26913 88 0 0 25 0 1 0 480313806 107737088 24679 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26303 24679 603 41 0 26262 0 vsize: 105212 [startup+280.013 s] Raw data (loadavg): 1.06 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 27130 0 0 0 27911 89 0 0 25 0 1 0 480313806 108802048 24968 4294967295 134512640 134672761 3221224576 3221223760 134615703 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26563 24968 603 41 0 26522 0 vsize: 106252 [startup+290.015 s] Raw data (loadavg): 1.05 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 27322 0 0 0 28911 90 0 0 25 0 1 0 480313806 109596672 25160 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26757 25160 603 41 0 26716 0 vsize: 107028 [startup+300.015 s] Raw data (loadavg): 1.04 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 27974 0 0 0 29910 92 0 0 25 0 1 0 480313806 112238592 25812 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 27402 25812 603 41 0 27361 0 vsize: 109608 [startup+310.015 s] Raw data (loadavg): 1.03 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 28562 0 0 0 30909 93 0 0 25 0 1 0 480313806 114749440 26400 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28015 26400 603 41 0 27974 0 vsize: 112060 [startup+320.015 s] Raw data (loadavg): 1.03 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 29064 0 0 0 31907 94 0 0 25 0 1 0 480313806 116695040 26902 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 28490 26902 603 41 0 28449 0 vsize: 113960 [startup+330.015 s] Raw data (loadavg): 1.02 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 29709 0 0 0 32905 97 0 0 25 0 1 0 480313806 119619584 27547 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29204 27547 603 41 0 29163 0 vsize: 116816 [startup+340.016 s] Raw data (loadavg): 1.02 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 30642 0 0 0 33903 99 0 0 25 0 1 0 480313806 123420672 28480 4294967295 134512640 134672761 3221224576 3221223616 134612604 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30132 28481 603 41 0 30091 0 vsize: 120528 [startup+350.016 s] Raw data (loadavg): 1.02 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 31445 0 0 0 34901 102 0 0 25 0 1 0 480313806 126701568 29283 4294967295 134512640 134672761 3221224576 3221223568 134565149 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30933 29283 603 41 0 30892 0 vsize: 123732 [startup+360.016 s] Raw data (loadavg): 1.01 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 32858 0 0 0 35899 104 0 0 25 0 1 0 480313806 132571136 30696 4294967295 134512640 134672761 3221224576 3221223712 134614690 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 32366 30696 603 41 0 32325 0 vsize: 129464 [startup+370.017 s] Raw data (loadavg): 1.01 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 34066 0 0 0 36896 106 0 0 25 0 1 0 480313806 137396224 31904 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 33544 31904 603 41 0 33503 0 vsize: 134176 [startup+380.017 s] Raw data (loadavg): 1.01 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 34660 0 0 0 37894 108 0 0 25 0 1 0 480313806 139882496 32498 4294967295 134512640 134672761 3221224576 3221223616 134614228 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34151 32498 603 41 0 34110 0 vsize: 136604 [startup+390.018 s] Raw data (loadavg): 1.01 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 35426 0 0 0 38893 110 0 0 25 0 1 0 480313806 143052800 33264 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 34925 33264 603 41 0 34884 0 vsize: 139700 [startup+400.019 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 35663 0 0 0 39893 111 0 0 25 0 1 0 480313806 143970304 33501 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35149 33501 603 41 0 35108 0 vsize: 140596 [startup+410.019 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 35786 0 0 0 40892 111 0 0 25 0 1 0 480313806 144498688 33624 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35278 33624 603 41 0 35237 0 vsize: 141112 [startup+420.02 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 36104 0 0 0 41892 112 0 0 25 0 1 0 480313806 145805312 33942 4294967295 134512640 134672761 3221224576 3221223616 134614266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35597 33942 603 41 0 35556 0 vsize: 142388 [startup+430.019 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 36235 0 0 0 42892 112 0 0 25 0 1 0 480313806 146337792 34073 4294967295 134512640 134672761 3221224576 3221223720 134616350 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35727 34073 603 41 0 35686 0 vsize: 142908 [startup+440.021 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 36391 0 0 0 43891 113 0 0 25 0 1 0 480313806 146866176 34229 4294967295 134512640 134672761 3221224576 3221223760 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35856 34229 603 41 0 35815 0 vsize: 143424 [startup+450.02 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 36605 0 0 0 44891 113 0 0 25 0 1 0 480313806 147787776 34443 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36081 34443 603 41 0 36040 0 vsize: 144324 [startup+460.02 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 36827 0 0 0 45891 113 0 0 25 0 1 0 480313806 148713472 34665 4294967295 134512640 134672761 3221224576 3221223776 134610686 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36307 34665 603 41 0 36266 0 vsize: 145228 [startup+470.028 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 37082 0 0 0 46891 114 0 0 25 0 1 0 480313806 149762048 34920 4294967295 134512640 134672761 3221224576 3221223712 134614656 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36563 34920 603 41 0 36522 0 vsize: 146252 [startup+480.028 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 37172 0 0 0 47891 114 0 0 25 0 1 0 480313806 150016000 35010 4294967295 134512640 134672761 3221224576 3221223760 134615791 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36625 35010 603 41 0 36584 0 vsize: 146500 [startup+490.029 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 37330 0 0 0 48891 115 0 0 25 0 1 0 480313806 150663168 35168 4294967295 134512640 134672761 3221224576 3221223760 134615671 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 36783 35168 603 41 0 36742 0 vsize: 147132 [startup+500.03 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 37540 0 0 0 49890 116 0 0 25 0 1 0 480313806 151576576 35378 4294967295 134512640 134672761 3221224576 3221223712 134614814 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37006 35378 603 41 0 36965 0 vsize: 148024 [startup+510.03 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 37765 0 0 0 50889 117 0 0 25 0 1 0 480313806 152481792 35603 4294967295 134512640 134672761 3221224576 3221223616 134612739 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37227 35603 603 41 0 37186 0 vsize: 148908 [startup+520.03 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 38107 0 0 0 51889 118 0 0 25 0 1 0 480313806 153927680 35945 4294967295 134512640 134672761 3221224576 3221223760 134615929 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37580 35945 603 41 0 37539 0 vsize: 150320 [startup+530.03 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 38351 0 0 0 52888 118 0 0 25 0 1 0 480313806 154943488 36189 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 37828 36189 603 41 0 37787 0 vsize: 151312 [startup+540.031 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 39055 0 0 0 53887 120 0 0 25 0 1 0 480313806 157700096 36893 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 38501 36893 603 41 0 38460 0 vsize: 154004 [startup+550.031 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 39974 0 0 0 54883 123 0 0 25 0 1 0 480313806 161452032 37812 4294967295 134512640 134672761 3221224576 3221223760 134615671 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 39417 37812 603 41 0 39376 0 vsize: 157668 [startup+560.031 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 41048 0 0 0 55881 126 0 0 25 0 1 0 480313806 165941248 38886 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 40513 38886 603 41 0 40472 0 vsize: 162052 [startup+570.031 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 42196 0 0 0 56878 129 0 0 25 0 1 0 480313806 170541056 40034 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 41636 40034 603 41 0 41595 0 vsize: 166544 [startup+580.033 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 43145 0 0 0 57877 131 0 0 25 0 1 0 480313806 174489600 40983 4294967295 134512640 134672761 3221224576 3221223616 134614243 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 42600 40983 603 41 0 42559 0 vsize: 170400 [startup+590.034 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 43504 0 0 0 58876 132 0 0 25 0 1 0 480313806 175939584 41342 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 42954 41342 603 41 0 42913 0 vsize: 171816 [startup+600.034 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 44243 0 0 0 59874 134 0 0 25 0 1 0 480313806 178954240 42081 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 43690 42081 603 41 0 43649 0 vsize: 174760 [startup+610.035 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 45245 0 0 0 60872 136 0 0 25 0 1 0 480313806 183115776 43083 4294967295 134512640 134672761 3221224576 3221223760 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 44706 43083 603 41 0 44665 0 vsize: 178824 [startup+620.035 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 45879 0 0 0 61871 137 0 0 25 0 1 0 480313806 185630720 43717 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 45320 43717 603 41 0 45279 0 vsize: 181280 [startup+630.035 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 46278 0 0 0 62870 138 0 0 25 0 1 0 480313806 187326464 44116 4294967295 134512640 134672761 3221224576 3221223760 134615732 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 45734 44116 603 41 0 45693 0 vsize: 182936 [startup+640.036 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 46628 0 0 0 63870 139 0 0 25 0 1 0 480313806 188751872 44466 4294967295 134512640 134672761 3221224576 3221223712 134614727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 46082 44466 603 41 0 46041 0 vsize: 184328 [startup+650.037 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 47422 0 0 0 64868 141 0 0 25 0 1 0 480313806 191950848 45260 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 46863 45260 603 41 0 46822 0 vsize: 187452 [startup+660.037 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 47974 0 0 0 65867 142 0 0 25 0 1 0 480313806 194191360 45812 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 47410 45812 603 41 0 47369 0 vsize: 189640 [startup+670.037 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 48337 0 0 0 66866 144 0 0 25 0 1 0 480313806 195788800 46175 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 47800 46175 603 41 0 47759 0 vsize: 191200 [startup+680.038 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 48648 0 0 0 67865 145 0 0 25 0 1 0 480313806 196988928 46486 4294967295 134512640 134672761 3221224576 3221223760 134615627 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 48093 46486 603 41 0 48052 0 vsize: 192372 [startup+690.039 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 49059 0 0 0 68864 146 0 0 25 0 1 0 480313806 199229440 46897 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 48640 46897 603 41 0 48599 0 vsize: 194560 [startup+700.039 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 49302 0 0 0 69864 146 0 0 25 0 1 0 480313806 200146944 47140 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 48864 47140 603 41 0 48823 0 vsize: 195456 [startup+710.039 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 49451 0 0 0 70864 146 0 0 25 0 1 0 480313806 200806400 47289 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 49025 47289 603 41 0 48984 0 vsize: 196100 [startup+720.039 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 49634 0 0 0 71863 147 0 0 25 0 1 0 480313806 201596928 47472 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 49218 47472 603 41 0 49177 0 vsize: 196872 [startup+730.04 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 49918 0 0 0 72863 148 0 0 25 0 1 0 480313806 202645504 47756 4294967295 134512640 134672761 3221224576 3221223728 134541816 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 49474 47756 603 41 0 49433 0 vsize: 197896 [startup+740.042 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 50329 0 0 0 73861 149 0 0 25 0 1 0 480313806 204333056 48167 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 49886 48167 603 41 0 49845 0 vsize: 199544 [startup+750.042 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 50454 0 0 0 74861 150 0 0 25 0 1 0 480313806 204853248 48292 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 50013 48292 603 41 0 49972 0 vsize: 200052 [startup+760.042 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 50774 0 0 0 75860 151 0 0 25 0 1 0 480313806 206176256 48612 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 50336 48612 603 41 0 50295 0 vsize: 201344 [startup+770.043 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 51065 0 0 0 76860 152 0 0 25 0 1 0 480313806 207351808 48903 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 50623 48903 603 41 0 50582 0 vsize: 202492 [startup+780.044 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 51455 0 0 0 77858 153 0 0 25 0 1 0 480313806 208924672 49293 4294967295 134512640 134672761 3221224576 3221223776 134610697 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 51007 49293 603 41 0 50966 0 vsize: 204028 [startup+790.045 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 51701 0 0 0 78858 154 0 0 25 0 1 0 480313806 209985536 49539 4294967295 134512640 134672761 3221224576 3221223760 134615608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 51266 49539 603 41 0 51225 0 vsize: 205064 [startup+800.046 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 51987 0 0 0 79858 154 0 0 25 0 1 0 480313806 211169280 49825 4294967295 134512640 134672761 3221224576 3221223760 134615665 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 51555 49825 603 41 0 51514 0 vsize: 206220 [startup+810.046 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 52355 0 0 0 80857 155 0 0 25 0 1 0 480313806 212672512 50193 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 51922 50193 603 41 0 51881 0 vsize: 207688 [startup+820.046 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 52590 0 0 0 81857 156 0 0 25 0 1 0 480313806 213528576 50428 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 52131 50428 603 41 0 52090 0 vsize: 208524 [startup+830.046 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 52783 0 0 0 82856 156 0 0 25 0 1 0 480313806 214310912 50621 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 52322 50621 603 41 0 52281 0 vsize: 209288 [startup+840.047 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 53160 0 0 0 83856 157 0 0 25 0 1 0 480313806 215859200 50998 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 52700 50998 603 41 0 52659 0 vsize: 210800 [startup+850.048 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 53397 0 0 0 84855 158 0 0 25 0 1 0 480313806 216899584 51235 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 52954 51235 603 41 0 52913 0 vsize: 211816 [startup+860.048 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 53508 0 0 0 85855 158 0 0 25 0 1 0 480313806 217305088 51346 4294967295 134512640 134672761 3221224576 3221223776 134610528 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 53053 51346 603 41 0 53012 0 vsize: 212212 [startup+870.049 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 53950 0 0 0 86854 159 0 0 25 0 1 0 480313806 219017216 51788 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 53471 51788 603 41 0 53430 0 vsize: 213884 [startup+880.049 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 54157 0 0 0 87854 160 0 0 25 0 1 0 480313806 219938816 51995 4294967295 134512640 134672761 3221224576 3221223568 134565137 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 53696 51995 603 41 0 53655 0 vsize: 214784 [startup+890.05 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 54606 0 0 0 88853 161 0 0 25 0 1 0 480313806 221798400 52444 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 54150 52444 603 41 0 54109 0 vsize: 216600 [startup+900.05 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 54997 0 0 0 89852 162 0 0 25 0 1 0 480313806 223375360 52835 4294967295 134512640 134672761 3221224576 3221223760 134615601 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 54535 52835 603 41 0 54494 0 vsize: 218140 [startup+910.05 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 55340 0 0 0 90851 163 0 0 25 0 1 0 480313806 224776192 53178 4294967295 134512640 134672761 3221224576 3221223760 134615940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 54877 53178 603 41 0 54836 0 vsize: 219508 [startup+920.051 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 55708 0 0 0 91850 165 0 0 25 0 1 0 480313806 226197504 53546 4294967295 134512640 134672761 3221224576 3221223760 134615541 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 55224 53546 603 41 0 55183 0 vsize: 220896 [startup+930.051 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 56574 0 0 0 92848 167 0 0 25 0 1 0 480313806 229834752 54412 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 56112 54412 603 41 0 56071 0 vsize: 224448 [startup+940.052 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 57525 0 0 0 93846 169 0 0 25 0 1 0 480313806 233680896 55363 4294967295 134512640 134672761 3221224576 3221223760 134616014 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 57051 55363 603 41 0 57010 0 vsize: 228204 [startup+950.053 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 59113 0 0 0 94843 172 0 0 25 0 1 0 480313806 240189440 56951 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 58640 56951 603 41 0 58599 0 vsize: 234560 [startup+960.053 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 60403 0 0 0 95840 175 0 0 25 0 1 0 480313806 245456896 58241 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 59926 58241 603 41 0 59885 0 vsize: 239704 [startup+970.054 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 61382 0 0 0 96839 177 0 0 25 0 1 0 480313806 249466880 59220 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 60905 59220 603 41 0 60864 0 vsize: 243620 [startup+980.055 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 62293 0 0 0 97837 178 0 0 25 0 1 0 480313806 253145088 60131 4294967295 134512640 134672761 3221224576 3221223712 134614800 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 61803 60131 603 41 0 61762 0 vsize: 247212 [startup+990.056 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 63422 0 0 0 98835 181 0 0 25 0 1 0 480313806 257855488 61260 4294967295 134512640 134672761 3221224576 3221223568 134565045 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 62953 61260 603 41 0 62912 0 vsize: 251812 [startup+1000.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 64337 0 0 0 99833 183 0 0 25 0 1 0 480313806 261591040 62175 4294967295 134512640 134672761 3221224576 3221223760 134615549 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 63865 62175 603 41 0 63824 0 vsize: 255460 [startup+1010.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 81495 0 0 0 100788 228 0 0 25 0 1 0 480313806 321347584 75282 4294967295 134512640 134672761 3221224576 3221223120 134621238 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78454 75282 603 41 0 78413 0 vsize: 313816 [startup+1020.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 82587 0 0 0 101781 235 0 0 25 0 1 0 480313806 323121152 75700 4294967295 134512640 134672761 3221224576 3221222784 1075730206 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78887 75700 603 41 0 78846 0 vsize: 315548 [startup+1030.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 82699 0 0 0 102736 253 0 0 25 0 1 0 480313806 323149824 75701 4294967295 134512640 134672761 3221224576 3221223024 134643542 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78894 75701 603 41 0 78853 0 vsize: 315576 [startup+1040.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 82699 0 0 0 103737 253 0 0 25 0 1 0 480313806 322887680 75643 4294967295 134512640 134672761 3221224576 3221223024 134643583 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78830 75643 603 41 0 78789 0 vsize: 315320 [startup+1050.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 84198 0 0 0 104734 256 0 0 25 0 1 0 480313806 330534912 76935 4294967295 134512640 134672761 3221224576 3221223100 1075346542 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 80697 76935 603 41 0 80656 0 vsize: 322788 [startup+1060.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 84215 0 0 0 105733 257 0 0 25 0 1 0 480313806 322502656 75548 4294967295 134512640 134672761 3221224576 3221223024 134643516 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78736 75548 603 41 0 78695 0 vsize: 314944 [startup+1070.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 106730 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223776 134610661 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1080.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 107730 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1090.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 108730 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615594 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1100.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 109731 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223568 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1110.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 110731 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223720 134616293 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1120.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 111731 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223616 134612987 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1130.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 112731 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1140.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 113732 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615663 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1150.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 114732 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1160.06 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 115732 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615683 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1170.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 116732 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615804 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1180.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 117732 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615619 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1190.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 118733 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223760 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1200.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 119733 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223568 134565073 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 [startup+1210.07 s] Raw data (loadavg): 1.00 0.98 0.91 2/54 28559 Raw data (stat): 28559 (minisat+) R 28558 23176 23175 0 -1 0 85354 0 0 0 120733 260 0 0 25 0 1 0 480313806 322363392 75538 4294967295 134512640 134672761 3221224576 3221223776 134610707 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 78702 75538 603 41 0 78661 0 vsize: 314808 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1210.24 s] Raw data (loadavg): 1.00 0.98 0.91 1/54 28559 Raw data (stat): 28559 (minisat+) Z 28558 23176 23175 0 -1 12 85355 0 0 0 120733 277 0 0 25 0 1 0 480313806 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1210.24 CPU time (s): 1210.11 CPU user time (s): 1207.34 CPU system time (s): 2.77458 CPU usage (%): 99.9894 Max. virtual memory (Kb): 322788 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####