Name | normalized-opb/mps-v2-13-7/plato.asu.edu/pub/milp/normalized-mps-v2-13-7-neos5.opb |
MD5SUM | 4f5f6e30a602f3968daa9ca41c7da043 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 2058 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 133 |
Biggest coefficient in the objective function | 128 |
Number of bits for the biggest coefficient in the objective function | 8 |
Sum of the numbers in the objective function | 9334 |
Number of bits of the sum of numbers in the objective function | 14 |
Biggest number in a constraint | 1024 |
Number of bits of the biggest number in a constraint | 11 |
Biggest sum of numbers in a constraint | 9334 |
Number of bits of the biggest sum of numbers | 14 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1.05284 |
Number of variables | 133 |
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 | 81 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc4 THE 2005-05-25 23:59:58 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22701 boxname=wulflinc4 idbench=1517 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 4f5f6e30a602f3968daa9ca41c7da043 /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-neos5.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-neos5.opb IDLAUNCH: 22701 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 828912 kB Buffers: 31504 kB Cached: 154316 kB SwapCached: 500 kB Active: 38400 kB Inactive: 149752 kB HighTotal: 131008 kB HighFree: 1904 kB LowTotal: 903652 kB LowFree: 827008 kB SwapTotal: 2097136 kB SwapFree: 2096004 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5788 kB Slab: 11948 kB Committed_AS: 71796 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-26 00:20:28 (client local time) WITH STATUS 152 IN 1229.85 SECONDS stats: 22701 7 1229.85 152 #### 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: 7 c ---[ 71]---> BDD-cost: 7 c ---[ 70]---> BDD-cost: 7 c ---[ 69]---> BDD-cost: 7 c ---[ 68]---> BDD-cost: 7 c ---[ 67]---> BDD-cost: 7 c ---[ 66]---> BDD-cost: 7 c ---[ 65]---> BDD-cost: 7 c ---[ 64]---> BDD-cost: 7 c ---[ 63]---> BDD-cost: 7 c ---[ 62]---> Sorter-cost: 382 Base: c ---[ 61]---> Sorter-cost: 717 Base: 2 2 2 2 2 2 2 c ---[ 60]---> Sorter-cost: 417 Base: 2 2 2 2 2 2 2 c ---[ 59]---> Sorter-cost: 1147 Base: 2 2 2 2 2 2 2 c ---[ 58]---> Sorter-cost: 868 Base: 2 2 2 2 2 2 2 c ---[ 57]---> Sorter-cost: 429 Base: 2 2 2 2 2 2 2 c ---[ 56]---> Sorter-cost: 989 Base: 2 2 2 2 2 2 2 c ---[ 55]---> Sorter-cost: 866 Base: 2 2 2 2 2 2 2 c ---[ 54]---> Sorter-cost: 898 Base: 2 2 2 2 2 2 2 c ---[ 53]---> Sorter-cost: 445 Base: 2 2 2 2 2 2 2 c ---[ 52]---> Sorter-cost: 1011 Base: 2 2 2 2 2 2 2 c ---[ 51]---> Sorter-cost: 216 Base: c ---[ 50]---> Sorter-cost: 856 Base: 2 2 2 2 2 2 2 c ---[ 49]---> Sorter-cost: 1043 Base: 2 2 2 2 2 2 2 c ---[ 48]---> Sorter-cost: 488 Base: 2 2 2 2 2 2 2 c ---[ 47]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 c ---[ 46]---> Sorter-cost: 373 Base: 2 2 2 2 2 2 2 c ---[ 45]---> Sorter-cost: 405 Base: 2 2 2 2 2 2 2 c ---[ 44]---> Sorter-cost: 343 Base: 2 2 2 2 2 2 2 c ---[ 43]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 c ---[ 42]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 c ---[ 41]---> Sorter-cost: 379 Base: 2 2 2 2 2 2 2 c ---[ 40]---> Sorter-cost: 351 Base: 2 2 2 2 2 2 2 c ---[ 39]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 c ---[ 38]---> Sorter-cost: 955 Base: 2 2 2 2 2 2 2 c ---[ 37]---> Sorter-cost: 345 Base: 2 2 2 2 2 2 2 c ---[ 36]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 c ---[ 35]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 c ---[ 34]---> Sorter-cost: 379 Base: 2 2 2 2 2 2 2 c ---[ 33]---> Sorter-cost: 399 Base: 2 2 2 2 2 2 2 c ---[ 32]---> Sorter-cost: 969 Base: 2 2 2 2 2 2 2 c ---[ 31]---> Sorter-cost: 405 Base: 2 2 2 2 2 2 2 c ---[ 30]---> Sorter-cost: 417 Base: 2 2 2 2 2 2 2 c ---[ 29]---> Sorter-cost: 311 Base: 2 2 2 2 2 2 2 c ---[ 28]---> Sorter-cost: 828 Base: 2 2 2 2 2 2 2 c ---[ 27]---> Sorter-cost: 1013 Base: 2 2 2 2 2 2 2 c ---[ 26]---> Sorter-cost: 337 Base: 2 2 2 2 2 2 2 c ---[ 25]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 c ---[ 24]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 c ---[ 23]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 c ---[ 22]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 c ---[ 21]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 c ---[ 20]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 c ---[ 19]---> Sorter-cost: 365 Base: 2 2 2 2 2 2 2 c ---[ 18]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 c ---[ 17]---> Sorter-cost: 397 Base: 2 2 2 2 2 2 2 c ---[ 16]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 c ---[ 15]---> Sorter-cost: 355 Base: 2 2 2 2 2 2 2 c ---[ 14]---> Sorter-cost: 387 Base: 2 2 2 2 2 2 2 c ---[ 13]---> Sorter-cost: 389 Base: 2 2 2 2 2 2 2 c ---[ 12]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 c ---[ 11]---> Sorter-cost: 810 Base: 2 2 2 2 2 2 2 c ---[ 10]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 c ---[ 9]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 c ---[ 8]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 c ---[ 7]---> Sorter-cost: 319 Base: 2 2 2 2 2 2 2 c ---[ 6]---> Sorter-cost: 329 Base: 2 2 2 2 2 2 2 c ---[ 5]---> Sorter-cost: 355 Base: 2 2 2 2 2 2 2 c ---[ 4]---> Sorter-cost: 387 Base: 2 2 2 2 2 2 2 c ---[ 3]---> Sorter-cost: 319 Base: 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 c ---[ 0]---> Sorter-cost: 301 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 25058 60127 | 8352 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 7865[0m c ---[ 0]---> Sorter-cost: 2067 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2 | 29745 71113 | 9915 2 22 11.0 | 0.000 % | c ============================================================================== c [1mFound solution: 4982[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 57 | 29959 71656 | 9986 57 225 3.9 | 0.000 % | c ============================================================================== c [1mFound solution: 4278[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 104 | 30029 71844 | 10009 104 412 4.0 | 0.000 % | c ============================================================================== c [1mFound solution: 3709[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 122 | 30077 71967 | 10025 122 476 3.9 | 0.000 % | c ============================================================================== c [1mFound solution: 3587[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 129 | 30088 71998 | 10029 129 559 4.3 | 0.000 % | c ============================================================================== c [1mFound solution: 2685[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 213 | 30158 72168 | 10052 213 1235 5.8 | 0.000 % | c ============================================================================== c [1mFound solution: 2654[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 235 | 30170 72207 | 10056 235 1355 5.8 | 0.000 % | c ============================================================================== c [1mFound solution: 2646[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 244 | 30177 72225 | 10059 244 1386 5.7 | 0.000 % | c ============================================================================== c [1mFound solution: 2645[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 244 | 30184 72243 | 10061 244 1386 5.7 | 0.000 % | c ============================================================================== c [1mFound solution: 2642[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 244 | 30194 72272 | 10064 244 1386 5.7 | 0.000 % | c ============================================================================== c [1mFound solution: 2641[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 244 | 30203 72294 | 10067 244 1386 5.7 | 0.000 % | c ============================================================================== c [1mFound solution: 2581[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 244 | 30207 72303 | 10069 244 1386 5.7 | 0.000 % | c ============================================================================== c [1mFound solution: 2578[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 244 | 30211 72312 | 10070 244 1386 5.7 | 0.000 % | c ============================================================================== c [1mFound solution: 2577[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 244 | 30215 72321 | 10071 244 1386 5.7 | 0.000 % | c ============================================================================== c [1mFound solution: 2575[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 257 | 30221 72335 | 10073 257 1482 5.8 | 0.000 % | c ============================================================================== c [1mFound solution: 2562[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 283 | 30228 72351 | 10076 283 1645 5.8 | 0.000 % | c | 383 | 30228 72351 | 11083 383 2370 6.2 | 0.519 % | c | 533 | 30222 72339 | 12191 532 3734 7.0 | 0.535 % | c ============================================================================== c [1mFound solution: 2433[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 539 | 30243 72391 | 10081 538 3828 7.1 | 0.535 % | c ============================================================================== c [1mFound solution: 2432[0m c ---[ 0]---> Sorter-cost: 8 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 568 | 30255 72425 | 10085 567 4202 7.4 | 0.535 % | c ============================================================================== c [1mFound solution: 2304[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 599 | 30265 72449 | 10088 598 4520 7.6 | 0.535 % | c | 701 | 30265 72449 | 11096 700 5583 8.0 | 0.551 % | c | 853 | 30265 72449 | 12206 852 8308 9.8 | 0.551 % | c | 1079 | 30265 72449 | 13427 1078 11040 10.2 | 0.551 % | c | 1416 | 30265 72449 | 14769 1415 16310 11.5 | 0.551 % | c ============================================================================== c [1mFound solution: 2303[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1905 | 30271 72462 | 10090 1904 21674 11.4 | 0.551 % | c | 2009 | 30269 72458 | 11099 2005 22744 11.3 | 0.562 % | c | 2160 | 30269 72458 | 12208 2156 25543 11.8 | 0.562 % | c | 2385 | 30259 72437 | 13429 2358 28130 11.9 | 0.594 % | c | 2724 | 30258 72434 | 14772 2672 35247 13.2 | 0.599 % | c ============================================================================== c [1mFound solution: 2302[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 2936 | 30263 72445 | 10087 2884 40313 14.0 | 0.599 % | c | 3038 | 30263 72445 | 11095 2986 41318 13.8 | 0.605 % | c | 3188 | 30263 72445 | 12205 3136 43360 13.8 | 0.605 % | c | 3414 | 30263 72445 | 13425 3362 47053 14.0 | 0.605 % | c ============================================================================== c [1mFound solution: 2280[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3647 | 30287 72507 | 10095 3595 50008 13.9 | 0.605 % | c | 3747 | 30287 72507 | 11104 3695 52982 14.3 | 0.615 % | c | 3897 | 30287 72507 | 12214 3845 55042 14.3 | 0.615 % | c ============================================================================== c [1mFound solution: 2278[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4089 | 30295 72532 | 10098 4037 60000 14.9 | 0.615 % | c | 4189 | 30293 72528 | 11107 4136 61270 14.8 | 0.626 % | c | 4340 | 30293 72528 | 12218 4287 62565 14.6 | 0.626 % | c | 4565 | 30293 72528 | 13440 4512 68337 15.1 | 0.626 % | c | 4905 | 30293 72528 | 14784 4852 84491 17.4 | 0.626 % | c | 5411 | 30293 72528 | 16262 5358 96213 18.0 | 0.626 % | c | 6170 | 30287 72514 | 17889 6098 112050 18.4 | 0.647 % | c ============================================================================== c [1mFound solution: 2228[0m c ---[ 0]---> Sorter-cost: 7 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 6491 | 30294 72533 | 10098 6419 118900 18.5 | 0.647 % | c | 6591 | 30294 72533 | 11107 6519 121991 18.7 | 0.652 % | c | 6742 | 30294 72533 | 12218 6670 123908 18.6 | 0.652 % | c | 6967 | 30294 72533 | 13440 6895 128894 18.7 | 0.652 % | c | 7304 | 30294 72533 | 14784 7232 135222 18.7 | 0.652 % | c | 7810 | 30294 72533 | 16262 7738 154229 19.9 | 0.652 % | c ============================================================================== c [1mFound solution: 2163[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 7969 | 30301 72554 | 10100 7897 156108 19.8 | 0.652 % | c | 8069 | 30301 72554 | 11110 7997 158680 19.8 | 0.658 % | c | 8219 | 30301 72554 | 12221 8147 164256 20.2 | 0.658 % | c | 8444 | 30301 72554 | 13443 8372 168166 20.1 | 0.658 % | c ============================================================================== c [1mFound solution: 2049[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 8508 | 30308 72569 | 10102 8436 171099 20.3 | 0.658 % | c | 8608 | 30308 72569 | 11112 8536 173093 20.3 | 0.663 % | c | 8760 | 30308 72569 | 12223 8688 176166 20.3 | 0.663 % | c | 8985 | 30308 72569 | 13445 8913 183116 20.5 | 0.663 % | c | 9322 | 30308 72569 | 14790 9250 209552 22.7 | 0.663 % | c ============================================================================== c [1mFound solution: 2048[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 9770 | 30304 72561 | 10101 9696 232110 23.9 | 0.663 % | c | 9871 | 30304 72561 | 11111 9797 233194 23.8 | 0.690 % | c | 10021 | 30304 72561 | 12222 9947 238904 24.0 | 0.690 % | c | 10246 | 30304 72561 | 13444 10172 243667 24.0 | 0.690 % | c | 10584 | 30304 72561 | 14788 10510 257383 24.5 | 0.690 % | c | 11090 | 30304 72561 | 16267 11016 272958 24.8 | 0.690 % | c | 11849 | 30304 72561 | 17894 11775 305277 25.9 | 0.690 % | c | 12988 | 30304 72561 | 19683 12914 325888 25.2 | 0.690 % | c | 14697 | 30304 72561 | 21652 14623 466104 31.9 | 0.690 % | c | 17260 | 30289 72526 | 23817 17110 529488 30.9 | 0.717 % | c ============================================================================== c [1mFound solution: 2042[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 20917 | 30278 72502 | 10092 20754 676782 32.6 | 0.717 % | c | 21017 | 30278 72502 | 11101 5289 123412 23.3 | 0.781 % | c | 21167 | 30278 72502 | 12211 5439 126170 23.2 | 0.781 % | c | 21393 | 30278 72502 | 13432 5665 129534 22.9 | 0.781 % | c | 21730 | 30278 72502 | 14775 6002 155817 26.0 | 0.781 % | c | 22236 | 30278 72502 | 16253 6508 178176 27.4 | 0.781 % | c | 22995 | 30278 72502 | 17878 7267 199606 27.5 | 0.781 % | c | 24137 | 30276 72498 | 19666 8408 238458 28.4 | 0.787 % | c | 25845 | 30276 72498 | 21633 10116 276591 27.3 | 0.787 % | c | 28408 | 30276 72498 | 23796 12679 426829 33.7 | 0.787 % | c | 32252 | 30276 72498 | 26176 16523 540088 32.7 | 0.787 % | c ============================================================================== c [1mFound solution: 2040[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 37912 | 30282 72511 | 10094 22183 733704 33.1 | 0.787 % | c | 38015 | 30282 72511 | 11103 5650 122697 21.7 | 0.792 % | c | 38165 | 30282 72511 | 12213 5800 128333 22.1 | 0.792 % | c | 38390 | 30282 72511 | 13435 6025 138366 23.0 | 0.792 % | c | 38727 | 30282 72511 | 14778 6362 150039 23.6 | 0.792 % | c | 39234 | 30282 72511 | 16256 6869 168341 24.5 | 0.792 % | c | 39995 | 30282 72511 | 17882 7630 190345 24.9 | 0.792 % | c | 41137 | 30282 72511 | 19670 8772 221960 25.3 | 0.792 % | c | 42846 | 30282 72511 | 21637 10481 293277 28.0 | 0.792 % | c | 45409 | 30282 72511 | 23801 13044 470017 36.0 | 0.792 % | c | 49257 | 30282 72511 | 26181 16892 662441 39.2 | 0.792 % | c ============================================================================== c [1mFound solution: 2038[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 50921 | 30293 72537 | 10097 18556 729401 39.3 | 0.792 % | c | 51021 | 30293 72537 | 11106 9378 293455 31.3 | 0.813 % | c | 51171 | 30293 72537 | 12217 9528 298447 31.3 | 0.813 % | c | 51396 | 30293 72537 | 13439 9753 303506 31.1 | 0.813 % | c | 51733 | 30293 72537 | 14783 10090 316145 31.3 | 0.813 % | c | 52240 | 30293 72537 | 16261 10597 338448 31.9 | 0.813 % | c | 52999 | 30293 72537 | 17887 11356 372821 32.8 | 0.813 % | c | 54138 | 30293 72537 | 19676 12495 422072 33.8 | 0.813 % | c | 55846 | 30293 72537 | 21643 14203 509563 35.9 | 0.813 % | c | 58408 | 30293 72537 | 23808 16765 655374 39.1 | 0.813 % | c | 62254 | 30293 72537 | 26189 20611 938462 45.5 | 0.813 % | c | 68021 | 30293 72537 | 28807 26378 1255036 47.6 | 0.813 % | c | 76670 | 30293 72537 | 31688 35027 2091568 59.7 | 0.813 % | c | 89644 | 30293 72537 | 34857 29230 2035256 69.6 | 0.813 % | c | 109106 | 30293 72537 | 38343 24662 1710977 69.4 | 0.813 % | c | 138298 | 30289 72528 | 42177 31620 2254632 71.3 | 0.819 % | c | 182089 | 30289 72528 | 46395 42844 4397296 102.6 | 0.819 % | c ============================================================================== c [1mFound solution: 2037[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 208814 | 30294 72543 | 10098 40026 3122766 78.0 | 0.819 % | c | 208914 | 30294 72543 | 11107 9107 453328 49.8 | 0.824 % | c | 209066 | 30294 72543 | 12218 9259 460063 49.7 | 0.824 % | c | 209291 | 30294 72543 | 13440 9484 473442 49.9 | 0.824 % | c | 209628 | 30294 72543 | 14784 9821 497096 50.6 | 0.824 % | c | 210134 | 30294 72543 | 16262 10327 513875 49.8 | 0.824 % | c | 210893 | 30294 72543 | 17889 11086 558188 50.4 | 0.824 % | c | 212033 | 30294 72543 | 19678 12226 646452 52.9 | 0.824 % | c | 213742 | 30294 72543 | 21645 13935 758196 54.4 | 0.824 % | c | 216305 | 30294 72543 | 23810 16498 885107 53.6 | 0.824 % | c ============================================================================== c [1mFound solution: 2036[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 217979 | 30298 72553 | 10099 18172 958657 52.8 | 0.824 % | c | 218079 | 30298 72553 | 11108 9186 260984 28.4 | 0.829 % | c | 218231 | 30298 72553 | 12219 9338 264238 28.3 | 0.829 % | c | 218460 | 30298 72553 | 13441 9567 270453 28.3 | 0.829 % | c | 218797 | 30298 72553 | 14785 9904 281067 28.4 | 0.829 % | c | 219305 | 30298 72553 | 16264 10412 301155 28.9 | 0.829 % | c | 220065 | 30298 72553 | 17890 11172 328923 29.4 | 0.829 % | c | 221206 | 30298 72553 | 19680 12313 374119 30.4 | 0.829 % | c | 222915 | 30298 72553 | 21648 14022 413782 29.5 | 0.829 % | c ============================================================================== c [1mFound solution: 2035[0m c ---[ 0]---> Sorter-cost: 2 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 225286 | 30301 72560 | 10100 16393 497229 30.3 | 0.829 % | c | 225386 | 30301 72560 | 11110 8297 146061 17.6 | 0.834 % | c | 225538 | 30301 72560 | 12221 8449 150054 17.8 | 0.834 % | c | 225763 | 30301 72560 | 13443 8674 154553 17.8 | 0.834 % | c | 226100 | 30301 72560 | 14787 9011 161769 18.0 | 0.834 % | c | 226606 | 30301 72560 | 16266 9517 181575 19.1 | 0.834 % | c | 227366 | 30301 72560 | 17892 10277 216146 21.0 | 0.834 % | c | 228506 | 30301 72560 | 19682 11417 261748 22.9 | 0.834 % | c | 230214 | 30301 72560 | 21650 13125 312840 23.8 | 0.834 % | c ============================================================================== c [1mFound solution: 2034[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 232171 | 30305 72571 | 10101 15082 399414 26.5 | 0.834 % | c | 232271 | 30305 72571 | 11111 7641 150076 19.6 | 0.840 % | c | 232421 | 30298 72556 | 12222 7754 152557 19.7 | 0.861 % | c | 232646 | 30298 72556 | 13444 7979 171379 21.5 | 0.861 % | c | 232985 | 30298 72556 | 14788 8318 184740 22.2 | 0.861 % | c | 233492 | 30298 72556 | 16267 8825 211213 23.9 | 0.861 % | c | 234251 | 30298 72556 | 17894 9584 244037 25.5 | 0.861 % | c | 235390 | 30298 72556 | 19683 10723 305332 28.5 | 0.861 % | c | 237099 | 30298 72556 | 21652 12432 363109 29.2 | 0.861 % | c | 239661 | 30298 72556 | 23817 14994 486752 32.5 | 0.861 % | c | 243505 | 30298 72556 | 26199 18838 856949 45.5 | 0.861 % | c ============================================================================== c [1mFound solution: 2018[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 246171 | 30304 72571 | 10101 21504 948392 44.1 | 0.861 % | c | 246272 | 30304 72571 | 11111 5477 65194 11.9 | 0.866 % | c | 246423 | 30304 72571 | 12222 5628 67034 11.9 | 0.866 % | c | 246648 | 30304 72571 | 13444 5853 76394 13.1 | 0.866 % | c | 246985 | 30304 72571 | 14788 6190 92176 14.9 | 0.866 % | c | 247491 | 30304 72571 | 16267 6696 128503 19.2 | 0.866 % | c | 248250 | 30304 72571 | 17894 7455 161534 21.7 | 0.866 % | c | 249389 | 30304 72571 | 19683 8594 239195 27.8 | 0.866 % | c | 251097 | 30304 72571 | 21652 10302 363537 35.3 | 0.866 % | c | 253660 | 30304 72571 | 23817 12865 469870 36.5 | 0.866 % | c | 257506 | 30304 72571 | 26199 16711 628632 37.6 | 0.866 % | c | 263273 | 30304 72571 | 28819 22478 1114326 49.6 | 0.866 % | c | 271922 | 30304 72571 | 31701 31127 1854890 59.6 | 0.866 % | c ============================================================================== c [1mFound solution: 2017[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 272492 | 30310 72586 | 10103 31697 1879788 59.3 | 0.866 % | c | 272593 | 30310 72586 | 11113 8026 239606 29.9 | 0.871 % | c | 272743 | 30310 72586 | 12224 8176 244624 29.9 | 0.872 % | c | 272968 | 30310 72586 | 13447 8401 248454 29.6 | 0.871 % | c | 273305 | 30310 72586 | 14791 8738 257058 29.4 | 0.871 % | c | 273811 | 30114 72175 | 16270 9201 282448 30.7 | 1.366 % | c | 274571 | 30114 72175 | 17898 9961 344514 34.6 | 1.366 % | c | 275710 | 30114 72175 | 19687 11100 419701 37.8 | 1.366 % | c | 277419 | 30114 72175 | 21656 12809 518184 40.5 | 1.366 % | c | 279987 | 30114 72175 | 23822 15377 725371 47.2 | 1.366 % | c | 283832 | 30114 72175 | 26204 19222 1130563 58.8 | 1.366 % | c | 289601 | 30114 72175 | 28825 24991 1796894 71.9 | 1.366 % | c | 298250 | 30114 72175 | 31707 33640 2795713 83.1 | 1.366 % | c ============================================================================== c [1mFound solution: 2016[0m c ---[ 0]---> Sorter-cost: 4 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 306549 | 30112 72174 | 10037 25118 1840003 73.3 | 1.366 % | c | 306650 | 30112 72174 | 11040 6381 90787 14.2 | 1.393 % | c | 306800 | 30112 72174 | 12144 6531 94048 14.4 | 1.393 % | c | 307026 | 30112 72174 | 13359 6757 102663 15.2 | 1.393 % | c | 307363 | 30112 72174 | 14695 7094 120332 17.0 | 1.393 % | c | 307869 | 30112 72174 | 16164 7600 143661 18.9 | 1.393 % | c | 308630 | 30112 72174 | 17781 8361 165407 19.8 | 1.393 % | c | 309769 | 30091 72125 | 19559 9486 225158 23.7 | 1.431 % | c | 311478 | 30091 72125 | 21515 11195 273080 24.4 | 1.431 % | c | 314040 | 30091 72125 | 23666 13757 442865 32.2 | 1.431 % | c | 317884 | 30091 72125 | 26033 17601 650760 37.0 | 1.431 % | c | 323650 | 30080 72102 | 28636 23363 995344 42.6 | 1.452 % | c | 332299 | 30058 72055 | 31500 15252 514538 33.7 | 1.500 % | c | 345274 | 30058 72055 | 34650 28227 1015690 36.0 | 1.501 % | c ============================================================================== c [1mFound solution: 1987[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 348188 | 30065 72071 | 10021 31141 1135656 36.5 | 1.501 % | c | 348288 | 30065 72071 | 11023 7886 130211 16.5 | 1.506 % | c | 348440 | 30065 72071 | 12125 8038 133603 16.6 | 1.506 % | c | 348665 | 30065 72071 | 13337 8263 138357 16.7 | 1.506 % | c | 349002 | 30065 72071 | 14671 8600 165696 19.3 | 1.506 % | c | 349508 | 30060 72060 | 16138 9091 192789 21.2 | 1.522 % | c | 350267 | 30060 72060 | 17752 9850 229398 23.3 | 1.522 % | c | 351406 | 30060 72060 | 19528 10989 320079 29.1 | 1.522 % | c | 353114 | 30060 72060 | 21480 12697 397146 31.3 | 1.522 % | c ============================================================================== c [1mFound solution: 1986[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 354243 | 30066 72074 | 10022 13826 467725 33.8 | 1.522 % | c | 354343 | 30066 72074 | 11024 7013 154795 22.1 | 1.527 % | c | 354493 | 30066 72074 | 12126 7163 158225 22.1 | 1.527 % | c | 354720 | 30066 72074 | 13339 7390 167735 22.7 | 1.527 % | c | 355057 | 30066 72074 | 14673 7727 174615 22.6 | 1.527 % | c | 355563 | 30066 72074 | 16140 8233 189784 23.1 | 1.527 % | c | 356322 | 30066 72074 | 17754 8992 221782 24.7 | 1.527 % | c | 357461 | 30066 72074 | 19530 10131 287813 28.4 | 1.527 % | c | 359169 | 30063 72067 | 21483 11804 379485 32.1 | 1.537 % | c | 361731 | 30063 72067 | 23631 14366 515415 35.9 | 1.538 % | c | 365576 | 30063 72067 | 25994 18211 857635 47.1 | 1.538 % | c | 371342 | 30063 72067 | 28593 23977 1254320 52.3 | 1.538 % | c ============================================================================== c [1mFound solution: 1985[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 379796 | 30069 72081 | 10023 32431 1921379 59.2 | 1.538 % | c | 379896 | 30069 72081 | 11025 8208 230839 28.1 | 1.543 % | c | 380046 | 30052 72046 | 12127 8349 238475 28.6 | 1.591 % | c | 380271 | 30052 72046 | 13340 8574 242818 28.3 | 1.591 % | c | 380608 | 30052 72046 | 14674 8911 253941 28.5 | 1.591 % | c | 381114 | 30052 72046 | 16142 9417 272863 29.0 | 1.591 % | c | 381873 | 30052 72046 | 17756 10176 294633 29.0 | 1.591 % | c | 383013 | 30052 72046 | 19531 11316 425644 37.6 | 1.591 % | c | 384721 | 30052 72046 | 21485 13024 514701 39.5 | 1.591 % | c | 387284 | 30039 72019 | 23633 15576 811143 52.1 | 1.629 % | c | 391130 | 30039 72019 | 25997 19422 993229 51.1 | 1.629 % | c | 396897 | 30039 72019 | 28596 25189 1197276 47.5 | 1.629 % | c | 405546 | 30039 72019 | 31456 33838 2349966 69.4 | 1.629 % | c ============================================================================== c [1mFound solution: 1984[0m c ---[ 0]---> Sorter-cost: 3 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 412452 | 30045 72033 | 10015 23825 1563799 65.6 | 1.629 % | c | 412553 | 30045 72033 | 11016 6058 63936 10.6 | 1.634 % | c | 412706 | 30045 72033 | 12118 6211 66641 10.7 | 1.634 % | c | 412931 | 30045 72033 | 13329 6436 73707 11.5 | 1.634 % | c | 413268 | 30045 72033 | 14662 6772 82297 12.2 | 1.650 % | c | 413774 | 30040 72022 | 16129 7277 90265 12.4 | 1.650 % | c | 414535 | 30040 72022 | 17742 8038 122557 15.2 | 1.650 % | c | 415674 | 30040 72022 | 19516 9177 145477 15.9 | 1.650 % | c | 417383 | 30040 72022 | 21468 10886 341590 31.4 | 1.650 % | c | 419946 | 30040 72022 | 23614 13449 485434 36.1 | 1.650 % | c | 423792 | 30040 72022 | 25976 17295 651050 37.6 | 1.650 % | c | 429558 | 30040 72022 | 28573 23061 852779 37.0 | 1.650 % | c | 438208 | 30016 71967 | 31431 31704 1553912 49.0 | 1.687 % | c | 451183 | 30002 71936 | 34574 28660 2011024 70.2 | 1.730 % | c ============================================================================== c [1mFound solution: 1963[0m c ---[ 0]---> Sorter-cost: 6 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 465057 | 30009 71953 | 10003 24428 1513836 62.0 | 1.730 % | c | 465157 | 30006 71946 | 11003 6206 165676 26.7 | 1.746 % | c | 465307 | 30006 71946 | 12103 6356 171394 27.0 | 1.746 % | c | 465536 | 29882 71673 | 13313 6550 174477 26.6 | 2.095 % | c | 465874 | 29877 71661 | 14645 6674 179880 27.0 | 2.111 % | c | 466380 | 29877 71661 | 16109 7180 197269 27.5 | 2.111 % | c | 467142 | 29877 71661 | 17720 7942 239540 30.2 | 2.111 % | c | 468282 | 29877 71661 | 19493 9082 291813 32.1 | 2.111 % | c | 469990 | 29877 71661 | 21442 10790 344114 31.9 | 2.111 % | c | 472553 | 29877 71661 | 23586 13353 432431 32.4 | 2.111 % | c | 476397 | 29877 71661 | 25945 17197 576325 33.5 | 2.111 % | c | 482163 | 29877 71661 | 28539 22963 1062955 46.3 | 2.111 % | c | 490812 | 29873 71653 | 31393 31610 1482964 46.9 | 2.122 % | c | 503787 | 29873 71653 | 34533 22465 1213509 54.0 | 2.122 % | c | 523249 | 29873 71653 | 37986 21048 1041990 49.5 | 2.122 % | c | 552441 | 29865 71635 | 41785 23381 2648690 113.3 | 2.149 % | c | 596230 | 29865 71635 | 45963 36314 3603614 99.2 | 2.149 % | c ============================================================================== c [1mFound solution: 1962[0m c ---[ 0]---> Sorter-cost: 5 Base: 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 660239 | 29872 71652 | 9957 34216 1695417 49.6 | 2.149 % | c | 660339 | 29872 71652 | 10952 8654 132559 15.3 | 2.154 % | c | 660489 | 29872 71652 | 12047 8804 136022 15.5 | 2.154 % | c | 660714 | 29872 71652 | 13252 9029 151945 16.8 | 2.154 % | c | 661051 | 29872 71652 | 14578 9366 160732 17.2 | 2.154 % | c | 661557 | 29869 71646 | 16035 9871 193841 19.6 | 2.159 % | c | 662317 | 29869 71646 | 17639 10631 222334 20.9 | 2.159 % | c | 663456 | 29860 71627 | 19403 11768 255780 21.7 | 2.186 % | c | 665164 | 29860 71627 | 21343 13476 372429 27.6 | 2.186 % | c | 667728 | 29860 71627 | 23478 16040 668467 41.7 | 2.186 % | c | 671575 | 29860 71627 | 25825 19887 878314 44.2 | 2.186 % | c | 677341 | 29860 71627 | 28408 25653 1222800 47.7 | 2.186 % | c | 685990 | 29860 71627 | 31249 17721 507357 28.6 | 2.186 % | c | 698964 | 29860 71627 | 34374 30695 1255223 40.9 | 2.186 % | /oldhome/oroussel/solvers/minisat+_script: line 9: 6977 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@" #### 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.91 0.97 0.93 2/54 6973 Raw data (stat): 6973 (runsolver) R 6972 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 784800488 1052672 99 4294967295 134512640 135381576 3221224496 3221219704 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0011 s] Raw data (loadavg): 1.01 0.98 0.94 2/55 7030 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+20.0023 s] Raw data (loadavg): 1.01 0.98 0.94 2/55 7030 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+30.0035 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7030 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+40.0044 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7030 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+50.005 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7030 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+60.0066 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7030 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+70.0078 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7030 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+80.0086 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+90.0096 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+100.009 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.01 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.01 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+130.011 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+140.012 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+150.012 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.013 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+170.014 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+180.015 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+190.015 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+200.015 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+210.016 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+220.016 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+230.017 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+240.018 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+250.018 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+260.019 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+270.019 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+280.019 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+290.02 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+300.021 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+310.021 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+320.021 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7032 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+330.022 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+340.023 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+350.024 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+360.025 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+370.026 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+380.026 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+390.026 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+400.026 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+410.027 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+420.029 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+430.03 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+440.031 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+450.031 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+460.031 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+470.031 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+480.032 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+490.032 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+500.032 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+510.033 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+520.034 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+530.034 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+540.035 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+550.035 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+560.035 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+570.035 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+580.035 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+590.036 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+600.048 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+610.048 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+620.048 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+630.048 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+640.049 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+650.049 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+660.05 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+670.05 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+680.05 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+690.05 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+700.05 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+710.051 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+720.051 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+730.052 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+740.053 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+750.053 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+760.053 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+770.054 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+780.054 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+790.055 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+800.056 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+810.057 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+820.057 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+830.057 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+840.058 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+850.058 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+860.058 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+870.059 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+880.059 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+890.06 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+900.06 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+910.061 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+920.061 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+930.061 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+940.062 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+950.062 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+960.063 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+970.063 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+980.063 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+990.064 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1000.06 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1010.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1020.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1030.06 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1040.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1050.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1060.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1070.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1080.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1090.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1100.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1110.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1120.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1130.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1140.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1150.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1160.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1170.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1180.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1190.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1200.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1210.07 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1220.08 s] Raw data (loadavg): 1.00 0.98 0.94 2/55 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+1229.74 s] Raw data (loadavg): 1.00 0.98 0.94 1/53 7034 Raw data (stat): 6973 (minisat+_script) S 6972 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 784800488 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 0 Child status: 152 Real time (s): 1229.74 CPU time (s): 1229.85 CPU user time (s): 1229.54 CPU system time (s): 0.309952 CPU usage (%): 100.009 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####