Name | 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 | 1984 |
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 | 1195.14 |
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 |
LAUNCH ON wulflinc25 THE 2005-09-20 05:20:56 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=3460 boxname=wulflinc25 idbench=1116 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 4f5f6e30a602f3968daa9ca41c7da043 /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-neos5.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-neos5.opb IDLAUNCH: 3460 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.220 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 903792 kB Buffers: 17956 kB Cached: 85264 kB SwapCached: 888 kB Active: 22036 kB Inactive: 83812 kB HighTotal: 131008 kB HighFree: 42308 kB LowTotal: 903652 kB LowFree: 861484 kB SwapTotal: 2097892 kB SwapFree: 2096524 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5728 kB Slab: 19220 kB Committed_AS: 64132 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-09-20 05:41:06 (client local time) WITH STATUS 10 IN 1209.3 SECONDS stats: 3460 7 1209.3 10
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 % |
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing Stack size limit: 67108864 bytes Enforcing memory limit (will send SIGTERM then SIGKILL): 921600 Kb Enforcing VSIZE limit: 994918400 bytes Current StackSize limit: 67108864 bytes Raw data (/proc/28295/stat): 28295 (minisat+_script) R 28294 28295 4419 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1856000325 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 1 0 0 Raw data (/proc/28295/statm): 174 3 169 147 0 27 0 [pid=28295] vsize: 696 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libtermcap.so.2 open syscall for file tls/i686/libtermcap.so.2 open syscall for file tls/mmx/libtermcap.so.2 open syscall for file tls/libtermcap.so.2 open syscall for file i686/mmx/libtermcap.so.2 open syscall for file i686/libtermcap.so.2 open syscall for file mmx/libtermcap.so.2 open syscall for file libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/tls/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/i686/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/mmx/libtermcap.so.2 open syscall for file /oldhome/oroussel/lib/libtermcap.so.2 open syscall for file /etc/ld.so.cache open syscall for file /lib/libtermcap.so.2 open syscall for file tls/i686/mmx/libdl.so.2 open syscall for file tls/i686/libdl.so.2 open syscall for file tls/mmx/libdl.so.2 open syscall for file tls/libdl.so.2 open syscall for file i686/mmx/libdl.so.2 open syscall for file i686/libdl.so.2 open syscall for file mmx/libdl.so.2 open syscall for file libdl.so.2 open syscall for file /oldhome/oroussel/lib/libdl.so.2 open syscall for file /lib/libdl.so.2 open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /lib/tls/libc.so.6 open syscall for file /dev/tty open syscall for file /etc/mtab open syscall for file /proc/meminfo open syscall for file /oldhome/oroussel/solvers/minisat+_script New process pid=28296 New process pid=28297 New process pid=28298 execve syscall for /bin/sed executable One traced child (pid=28297) exited with status: 0 open syscall for file /etc/ld.so.preload open syscall for file tls/i686/mmx/libc.so.6 open syscall for file tls/i686/libc.so.6 open syscall for file tls/mmx/libc.so.6 open syscall for file tls/libc.so.6 open syscall for file i686/mmx/libc.so.6 open syscall for file i686/libc.so.6 open syscall for file mmx/libc.so.6 open syscall for file libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/tls/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/i686/libc.so.6 open syscall for file /oldhome/oroussel/lib/mmx/libc.so.6 open syscall for file /oldhome/oroussel/lib/libc.so.6 open syscall for file /etc/ld.so.cache open syscall for file /lib/tls/libc.so.6 One traced child (pid=28298) exited with status: 0 One traced child (pid=28296) exited with status: 0 New process pid=28299 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-neos5.opb [startup+10.0037 s] Raw data (loadavg): 0.89 0.95 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 1993 0 0 0 978 10 0 0 25 0 1 0 1856000330 9154560 1892 4294967295 134512640 135094434 3221224432 3221223120 134554731 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 2235 1892 145 145 0 2090 0 [pid=28299] vsize: 8940 Current children cumulated CPU time (s) 9.88 Current children cumulated vsize (Kb) 11064 [startup+20.0053 s] Raw data (loadavg): 0.90 0.96 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2394 0 0 0 1971 14 0 0 25 0 1 0 1856000330 10801152 2293 4294967295 134512640 135094434 3221224432 3221223088 134557893 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 2637 2293 145 145 0 2492 0 [pid=28299] vsize: 10548 Current children cumulated CPU time (s) 19.85 Current children cumulated vsize (Kb) 12672 [startup+30.0069 s] Raw data (loadavg): 0.92 0.96 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2671 0 0 0 2965 18 0 0 25 0 1 0 1856000330 11972608 2570 4294967295 134512640 135094434 3221224432 3221223088 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 2923 2570 145 145 0 2778 0 [pid=28299] vsize: 11692 Current children cumulated CPU time (s) 29.83 Current children cumulated vsize (Kb) 13816 [startup+40.0075 s] Raw data (loadavg): 0.93 0.96 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2671 0 0 0 3964 18 0 0 25 0 1 0 1856000330 11972608 2570 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 2923 2570 145 145 0 2778 0 [pid=28299] vsize: 11692 Current children cumulated CPU time (s) 39.82 Current children cumulated vsize (Kb) 13816 [startup+50.0081 s] Raw data (loadavg): 0.94 0.96 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2788 0 0 0 4962 19 0 0 25 0 1 0 1856000330 12447744 2687 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 3039 2687 145 145 0 2894 0 [pid=28299] vsize: 12156 Current children cumulated CPU time (s) 49.81 Current children cumulated vsize (Kb) 14280 [startup+60.0097 s] Raw data (loadavg): 0.95 0.96 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2788 0 0 0 5962 19 0 0 25 0 1 0 1856000330 12447744 2687 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 3039 2687 145 145 0 2894 0 [pid=28299] vsize: 12156 Current children cumulated CPU time (s) 59.81 Current children cumulated vsize (Kb) 14280 [startup+70.0103 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 2805 0 0 0 6961 20 0 0 25 0 1 0 1856000330 12517376 2704 4294967295 134512640 135094434 3221224432 3221223104 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 3056 2704 145 145 0 2911 0 [pid=28299] vsize: 12224 Current children cumulated CPU time (s) 69.81 Current children cumulated vsize (Kb) 14348 [startup+80.0119 s] Raw data (loadavg): 0.96 0.96 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 3102 0 0 0 7956 22 0 0 25 0 1 0 1856000330 13742080 3001 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 3355 3001 145 145 0 3210 0 [pid=28299] vsize: 13420 Current children cumulated CPU time (s) 79.78 Current children cumulated vsize (Kb) 15544 [startup+90.0125 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 3585 0 0 0 8946 27 0 0 25 0 1 0 1856000330 15695872 3484 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 3832 3484 145 145 0 3687 0 [pid=28299] vsize: 15328 Current children cumulated CPU time (s) 89.73 Current children cumulated vsize (Kb) 17452 [startup+100.013 s] Raw data (loadavg): 0.97 0.96 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 4234 0 0 0 9935 32 0 0 25 0 1 0 1856000330 18464768 4133 4294967295 134512640 135094434 3221224432 3221223072 134562085 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 4508 4133 145 145 0 4363 0 [pid=28299] vsize: 18032 Current children cumulated CPU time (s) 99.67 Current children cumulated vsize (Kb) 20156 [startup+110.015 s] Raw data (loadavg): 0.98 0.96 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 4304 0 0 0 10933 34 0 0 25 0 1 0 1856000330 18747392 4203 4294967295 134512640 135094434 3221224432 3221223104 134555614 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 4577 4203 145 145 0 4432 0 [pid=28299] vsize: 18308 Current children cumulated CPU time (s) 109.67 Current children cumulated vsize (Kb) 20432 [startup+120.015 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 4304 0 0 0 11933 34 0 0 25 0 1 0 1856000330 18747392 4203 4294967295 134512640 135094434 3221224432 3221223088 134558184 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 4577 4203 145 145 0 4432 0 [pid=28299] vsize: 18308 Current children cumulated CPU time (s) 119.67 Current children cumulated vsize (Kb) 20432 [startup+130.016 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 4548 0 0 0 12926 37 0 0 25 0 1 0 1856000330 19750912 4447 4294967295 134512640 135094434 3221224432 3221223104 134556317 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 4822 4447 145 145 0 4677 0 [pid=28299] vsize: 19288 Current children cumulated CPU time (s) 129.63 Current children cumulated vsize (Kb) 21412 [startup+140.017 s] Raw data (loadavg): 0.98 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5128 0 0 0 13914 43 0 0 25 0 1 0 1856000330 22110208 5027 4294967295 134512640 135094434 3221224432 3221223056 134557696 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 5398 5027 145 145 0 5253 0 [pid=28299] vsize: 21592 Current children cumulated CPU time (s) 139.57 Current children cumulated vsize (Kb) 23716 [startup+150.017 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5478 0 0 0 14907 47 0 0 25 0 1 0 1856000330 23539712 5377 4294967295 134512640 135094434 3221224432 3221223072 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 5747 5377 145 145 0 5602 0 [pid=28299] vsize: 22988 Current children cumulated CPU time (s) 149.54 Current children cumulated vsize (Kb) 25112 [startup+160.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5479 0 0 0 15907 47 0 0 25 0 1 0 1856000330 23539712 5378 4294967295 134512640 135094434 3221224432 3221223024 134557230 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 5747 5378 145 145 0 5602 0 [pid=28299] vsize: 22988 Current children cumulated CPU time (s) 159.54 Current children cumulated vsize (Kb) 25112 [startup+170.019 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5479 0 0 0 16906 48 0 0 25 0 1 0 1856000330 23539712 5378 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 5747 5378 145 145 0 5602 0 [pid=28299] vsize: 22988 Current children cumulated CPU time (s) 169.54 Current children cumulated vsize (Kb) 25112 [startup+180.02 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5479 0 0 0 17906 48 0 0 25 0 1 0 1856000330 23539712 5378 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 5747 5378 145 145 0 5602 0 [pid=28299] vsize: 22988 Current children cumulated CPU time (s) 179.54 Current children cumulated vsize (Kb) 25112 [startup+190.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5479 0 0 0 18906 48 0 0 25 0 1 0 1856000330 23539712 5378 4294967295 134512640 135094434 3221224432 3221223024 134556785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 5747 5378 145 145 0 5602 0 [pid=28299] vsize: 22988 Current children cumulated CPU time (s) 189.54 Current children cumulated vsize (Kb) 25112 [startup+200.021 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5554 0 0 0 19904 50 0 0 25 0 1 0 1856000330 23846912 5453 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 5822 5453 145 145 0 5677 0 [pid=28299] vsize: 23288 Current children cumulated CPU time (s) 199.54 Current children cumulated vsize (Kb) 25412 [startup+210.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5554 0 0 0 20903 50 0 0 25 0 1 0 1856000330 23846912 5453 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 5822 5453 145 145 0 5677 0 [pid=28299] vsize: 23288 Current children cumulated CPU time (s) 209.53 Current children cumulated vsize (Kb) 25412 [startup+220.022 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5554 0 0 0 21903 51 0 0 25 0 1 0 1856000330 23846912 5453 4294967295 134512640 135094434 3221224432 3221223056 134557612 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 5822 5453 145 145 0 5677 0 [pid=28299] vsize: 23288 Current children cumulated CPU time (s) 219.54 Current children cumulated vsize (Kb) 25412 [startup+230.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5554 0 0 0 22902 51 0 0 25 0 1 0 1856000330 23846912 5453 4294967295 134512640 135094434 3221224432 3221223088 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 5822 5453 145 145 0 5677 0 [pid=28299] vsize: 23288 Current children cumulated CPU time (s) 229.53 Current children cumulated vsize (Kb) 25412 [startup+240.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 5780 0 0 0 23897 53 0 0 25 0 1 0 1856000330 24780800 5679 4294967295 134512640 135094434 3221224432 3221223084 134558255 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 6050 5679 145 145 0 5905 0 [pid=28299] vsize: 24200 Current children cumulated CPU time (s) 239.5 Current children cumulated vsize (Kb) 26324 [startup+250.024 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6176 0 0 0 24890 56 0 0 25 0 1 0 1856000330 26386432 6075 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 6442 6075 145 145 0 6297 0 [pid=28299] vsize: 25768 Current children cumulated CPU time (s) 249.46 Current children cumulated vsize (Kb) 27892 [startup+260.026 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6572 0 0 0 25884 59 0 0 25 0 1 0 1856000330 28000256 6471 4294967295 134512640 135094434 3221224432 3221223056 134562076 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 6836 6471 145 145 0 6691 0 [pid=28299] vsize: 27344 Current children cumulated CPU time (s) 259.43 Current children cumulated vsize (Kb) 29468 [startup+270.025 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6884 0 0 0 26878 62 0 0 25 0 1 0 1856000330 29274112 6783 4294967295 134512640 135094434 3221224432 3221223024 134551876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7147 6783 145 145 0 7002 0 [pid=28299] vsize: 28588 Current children cumulated CPU time (s) 269.4 Current children cumulated vsize (Kb) 30712 [startup+280.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6884 0 0 0 27878 62 0 0 25 0 1 0 1856000330 29274112 6783 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7147 6783 145 145 0 7002 0 [pid=28299] vsize: 28588 Current children cumulated CPU time (s) 279.4 Current children cumulated vsize (Kb) 30712 [startup+290.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6884 0 0 0 28878 62 0 0 25 0 1 0 1856000330 29274112 6783 4294967295 134512640 135094434 3221224432 3221223088 134558016 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7147 6783 145 145 0 7002 0 [pid=28299] vsize: 28588 Current children cumulated CPU time (s) 289.4 Current children cumulated vsize (Kb) 30712 [startup+300.027 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6889 0 0 0 29879 62 0 0 25 0 1 0 1856000330 29306880 6788 4294967295 134512640 135094434 3221224432 3221223088 134558126 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7155 6788 145 145 0 7010 0 [pid=28299] vsize: 28620 Current children cumulated CPU time (s) 299.41 Current children cumulated vsize (Kb) 30744 [startup+310.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6890 0 0 0 30879 62 0 0 25 0 1 0 1856000330 29306880 6789 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7155 6789 145 145 0 7010 0 [pid=28299] vsize: 28620 Current children cumulated CPU time (s) 309.41 Current children cumulated vsize (Kb) 30744 [startup+320.028 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6890 0 0 0 31879 62 0 0 25 0 1 0 1856000330 29306880 6789 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7155 6789 145 145 0 7010 0 [pid=28299] vsize: 28620 Current children cumulated CPU time (s) 319.41 Current children cumulated vsize (Kb) 30744 [startup+330.029 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6890 0 0 0 32879 62 0 0 25 0 1 0 1856000330 29306880 6789 4294967295 134512640 135094434 3221224432 3221223024 134556789 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7155 6789 145 145 0 7010 0 [pid=28299] vsize: 28620 Current children cumulated CPU time (s) 329.41 Current children cumulated vsize (Kb) 30744 [startup+340.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 6890 0 0 0 33879 62 0 0 25 0 1 0 1856000330 29306880 6789 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7155 6789 145 145 0 7010 0 [pid=28299] vsize: 28620 Current children cumulated CPU time (s) 339.41 Current children cumulated vsize (Kb) 30744 [startup+350.03 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7206 0 0 0 34874 64 0 0 25 0 1 0 1856000330 30625792 7105 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7477 7105 145 145 0 7332 0 [pid=28299] vsize: 29908 Current children cumulated CPU time (s) 349.38 Current children cumulated vsize (Kb) 32032 [startup+360.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7562 0 0 0 35868 66 0 0 25 0 1 0 1856000330 32092160 7461 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7835 7461 145 145 0 7690 0 [pid=28299] vsize: 31340 Current children cumulated CPU time (s) 359.34 Current children cumulated vsize (Kb) 33464 [startup+370.031 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 36867 67 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223044 134563046 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0 [pid=28299] vsize: 31416 Current children cumulated CPU time (s) 369.34 Current children cumulated vsize (Kb) 33540 [startup+380.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 37865 67 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0 [pid=28299] vsize: 31416 Current children cumulated CPU time (s) 379.32 Current children cumulated vsize (Kb) 33540 [startup+390.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 38865 68 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223072 134562095 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0 [pid=28299] vsize: 31416 Current children cumulated CPU time (s) 389.33 Current children cumulated vsize (Kb) 33540 [startup+400.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 39865 68 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223088 134558187 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0 [pid=28299] vsize: 31416 Current children cumulated CPU time (s) 399.33 Current children cumulated vsize (Kb) 33540 [startup+410.034 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 40865 68 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0 [pid=28299] vsize: 31416 Current children cumulated CPU time (s) 409.33 Current children cumulated vsize (Kb) 33540 [startup+420.033 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7581 0 0 0 41865 68 0 0 25 0 1 0 1856000330 32169984 7480 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7854 7480 145 145 0 7709 0 [pid=28299] vsize: 31416 Current children cumulated CPU time (s) 419.33 Current children cumulated vsize (Kb) 33540 [startup+430.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 42865 68 0 0 25 0 1 0 1856000330 32432128 7512 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7918 7512 145 145 0 7773 0 [pid=28299] vsize: 31672 Current children cumulated CPU time (s) 429.33 Current children cumulated vsize (Kb) 33796 [startup+440.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 43865 68 0 0 25 0 1 0 1856000330 32432128 7512 4294967295 134512640 135094434 3221224432 3221223088 134557863 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7918 7512 145 145 0 7773 0 [pid=28299] vsize: 31672 Current children cumulated CPU time (s) 439.33 Current children cumulated vsize (Kb) 33796 [startup+450.035 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 44866 68 0 0 25 0 1 0 1856000330 32432128 7512 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7918 7512 145 145 0 7773 0 [pid=28299] vsize: 31672 Current children cumulated CPU time (s) 449.34 Current children cumulated vsize (Kb) 33796 [startup+460.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 45866 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 459.34 Current children cumulated vsize (Kb) 34052 [startup+470.036 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 46866 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223088 134557964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 469.34 Current children cumulated vsize (Kb) 34052 [startup+480.037 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 47866 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223120 134554742 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 479.34 Current children cumulated vsize (Kb) 34052 [startup+490.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 48866 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 489.34 Current children cumulated vsize (Kb) 34052 [startup+500.038 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 49867 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 499.35 Current children cumulated vsize (Kb) 34052 [startup+510.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 50867 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223068 134557560 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 509.35 Current children cumulated vsize (Kb) 34052 [startup+520.039 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 51867 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 519.35 Current children cumulated vsize (Kb) 34052 [startup+530.04 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 52867 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 529.35 Current children cumulated vsize (Kb) 34052 [startup+540.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7613 0 0 0 53868 68 0 0 25 0 1 0 1856000330 32694272 7512 4294967295 134512640 135094434 3221224432 3221223104 134555574 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7512 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 539.36 Current children cumulated vsize (Kb) 34052 [startup+550.041 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 54868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 549.37 Current children cumulated vsize (Kb) 34052 [startup+560.042 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 55868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223024 134557537 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 559.37 Current children cumulated vsize (Kb) 34052 [startup+570.043 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 56868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134558281 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 569.37 Current children cumulated vsize (Kb) 34052 [startup+580.044 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 57868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223024 134551704 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 579.37 Current children cumulated vsize (Kb) 34052 [startup+590.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 58868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 589.37 Current children cumulated vsize (Kb) 34052 [startup+600.045 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 59868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 599.37 Current children cumulated vsize (Kb) 34052 [startup+610.046 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 60868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 609.37 Current children cumulated vsize (Kb) 34052 [startup+620.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 61868 69 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 619.37 Current children cumulated vsize (Kb) 34052 [startup+630.047 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 62869 70 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 629.39 Current children cumulated vsize (Kb) 34052 [startup+640.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 63869 70 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 639.39 Current children cumulated vsize (Kb) 34052 [startup+650.049 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7615 0 0 0 64869 70 0 0 25 0 1 0 1856000330 32694272 7514 4294967295 134512640 135094434 3221224432 3221223088 134557948 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7514 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 649.39 Current children cumulated vsize (Kb) 34052 [startup+660.05 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 65869 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557860 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 659.39 Current children cumulated vsize (Kb) 34052 [startup+670.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 66869 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 669.39 Current children cumulated vsize (Kb) 34052 [startup+680.051 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 67870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 679.4 Current children cumulated vsize (Kb) 34052 [startup+690.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 68870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 689.4 Current children cumulated vsize (Kb) 34052 [startup+700.052 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 69870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557884 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 699.4 Current children cumulated vsize (Kb) 34052 [startup+710.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 70870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 709.4 Current children cumulated vsize (Kb) 34052 [startup+720.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 71870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223064 134557561 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 719.4 Current children cumulated vsize (Kb) 34052 [startup+730.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 72870 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557180 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 729.4 Current children cumulated vsize (Kb) 34052 [startup+740.054 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 73871 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 739.41 Current children cumulated vsize (Kb) 34052 [startup+750.053 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 74871 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557832 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 749.41 Current children cumulated vsize (Kb) 34052 [startup+760.055 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 75871 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 759.41 Current children cumulated vsize (Kb) 34052 [startup+770.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 76871 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134556815 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 769.41 Current children cumulated vsize (Kb) 34052 [startup+780.056 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 77871 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 779.41 Current children cumulated vsize (Kb) 34052 [startup+790.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 78872 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557398 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 789.42 Current children cumulated vsize (Kb) 34052 [startup+800.057 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 79872 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223044 134563074 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 799.42 Current children cumulated vsize (Kb) 34052 [startup+810.058 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 80872 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 809.42 Current children cumulated vsize (Kb) 34052 [startup+820.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 81872 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 819.42 Current children cumulated vsize (Kb) 34052 [startup+830.059 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 82873 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223056 134557598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 829.43 Current children cumulated vsize (Kb) 34052 [startup+840.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 83873 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 839.43 Current children cumulated vsize (Kb) 34052 [startup+850.06 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 84873 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 849.43 Current children cumulated vsize (Kb) 34052 [startup+860.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 85873 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 859.43 Current children cumulated vsize (Kb) 34052 [startup+870.061 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 86873 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 869.43 Current children cumulated vsize (Kb) 34052 [startup+880.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 87874 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 879.44 Current children cumulated vsize (Kb) 34052 [startup+890.063 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 88874 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 889.44 Current children cumulated vsize (Kb) 34052 [startup+900.062 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 89874 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223120 134554733 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 899.44 Current children cumulated vsize (Kb) 34052 [startup+910.064 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 90874 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134558019 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 909.44 Current children cumulated vsize (Kb) 34052 [startup+920.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 91874 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134558178 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 919.44 Current children cumulated vsize (Kb) 34052 [startup+930.065 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 92875 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 929.45 Current children cumulated vsize (Kb) 34052 [startup+940.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 93875 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223088 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 939.45 Current children cumulated vsize (Kb) 34052 [startup+950.067 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7617 0 0 0 94875 70 0 0 25 0 1 0 1856000330 32694272 7516 4294967295 134512640 135094434 3221224432 3221223024 134557028 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 7982 7516 145 145 0 7837 0 [pid=28299] vsize: 31928 Current children cumulated CPU time (s) 949.45 Current children cumulated vsize (Kb) 34052 [startup+960.068 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 7825 0 0 0 95873 72 0 0 25 0 1 0 1856000330 33546240 7724 4294967295 134512640 135094434 3221224432 3221223056 134557596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 8190 7724 145 145 0 8045 0 [pid=28299] vsize: 32760 Current children cumulated CPU time (s) 959.45 Current children cumulated vsize (Kb) 34884 [startup+970.069 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 8241 0 0 0 96865 76 0 0 25 0 1 0 1856000330 35250176 8140 4294967295 134512640 135094434 3221224432 3221223088 134557877 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 8606 8140 145 145 0 8461 0 [pid=28299] vsize: 34424 Current children cumulated CPU time (s) 969.41 Current children cumulated vsize (Kb) 36548 [startup+980.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 8707 0 0 0 97857 79 0 0 25 0 1 0 1856000330 37183488 8606 4294967295 134512640 135094434 3221224432 3221223088 134557950 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 9078 8606 145 145 0 8933 0 [pid=28299] vsize: 36312 Current children cumulated CPU time (s) 979.36 Current children cumulated vsize (Kb) 38436 [startup+990.071 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9159 0 0 0 98850 82 0 0 25 0 1 0 1856000330 39043072 9058 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 9532 9058 145 145 0 9387 0 [pid=28299] vsize: 38128 Current children cumulated CPU time (s) 989.32 Current children cumulated vsize (Kb) 40252 [startup+1000.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9578 0 0 0 99843 85 0 0 25 0 1 0 1856000330 40775680 9477 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 9955 9477 145 145 0 9810 0 [pid=28299] vsize: 39820 Current children cumulated CPU time (s) 999.28 Current children cumulated vsize (Kb) 41944 [startup+1010.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9955 0 0 0 100836 88 0 0 25 0 1 0 1856000330 42319872 9854 4294967295 134512640 135094434 3221224432 3221223088 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10332 9854 145 145 0 10187 0 [pid=28299] vsize: 41328 Current children cumulated CPU time (s) 1009.24 Current children cumulated vsize (Kb) 43452 [startup+1020.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 101835 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223120 134554709 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1019.23 Current children cumulated vsize (Kb) 43600 [startup+1030.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 102836 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223024 134557297 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1029.24 Current children cumulated vsize (Kb) 43600 [startup+1040.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 103836 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1039.24 Current children cumulated vsize (Kb) 43600 [startup+1050.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 104836 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223088 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1049.24 Current children cumulated vsize (Kb) 43600 [startup+1060.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 105836 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223104 134555568 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1059.24 Current children cumulated vsize (Kb) 43600 [startup+1070.07 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 106836 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223024 134557202 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1069.24 Current children cumulated vsize (Kb) 43600 [startup+1080.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9992 0 0 0 107837 88 0 0 25 0 1 0 1856000330 42471424 9891 4294967295 134512640 135094434 3221224432 3221223056 134557714 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9891 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1079.25 Current children cumulated vsize (Kb) 43600 [startup+1090.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 108837 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221222048 134562841 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1089.25 Current children cumulated vsize (Kb) 43600 [startup+1100.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 109837 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223104 134556454 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1099.25 Current children cumulated vsize (Kb) 43600 [startup+1110.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 110837 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134557976 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1109.25 Current children cumulated vsize (Kb) 43600 [startup+1120.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 111838 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223024 134557372 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1119.26 Current children cumulated vsize (Kb) 43600 [startup+1130.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 112838 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134558153 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1129.26 Current children cumulated vsize (Kb) 43600 [startup+1140.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 113838 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134558159 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1139.26 Current children cumulated vsize (Kb) 43600 [startup+1150.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 114838 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134558004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1149.26 Current children cumulated vsize (Kb) 43600 [startup+1160.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 115838 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1159.26 Current children cumulated vsize (Kb) 43600 [startup+1170.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 116839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223072 134538541 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1169.27 Current children cumulated vsize (Kb) 43600 [startup+1180.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 117839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134558249 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1179.27 Current children cumulated vsize (Kb) 43600 [startup+1190.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 118839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1189.27 Current children cumulated vsize (Kb) 43600 [startup+1200.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 119839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223120 134554746 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1199.27 Current children cumulated vsize (Kb) 43600 [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 120839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223088 134557837 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1209.27 Current children cumulated vsize (Kb) 43600 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.08 s] Raw data (loadavg): 0.99 0.97 0.91 2/57 28299 Raw data (/proc/28295/stat): 28295 (minisat+_script) S 28294 28295 4419 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1856000325 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (/proc/28295/statm): 531 226 485 147 0 384 0 [pid=28295] vsize: 2124 Raw data (/proc/28299/stat): 28299 (minisat+_64-bit) R 28295 28295 4419 0 -1 0 9997 0 0 0 120839 88 0 0 25 0 1 0 1856000330 42471424 9896 4294967295 134512640 135094434 3221224432 3221223024 134557238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/28299/statm): 10369 9896 145 145 0 10224 0 [pid=28299] vsize: 41476 Current children cumulated CPU time (s) 1209.27 Current children cumulated vsize (Kb) 43600 Sending SIGTERM to -28295 Sleeping 2 seconds One traced child (pid=28295) ended because it received signal 15 (SIGTERM) One traced child (pid=28299) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.11 CPU time (s): 1209.3 CPU user time (s): 1208.39 CPU system time (s): 0.909861 CPU usage (%): 99.9336 Max. virtual memory (cumulated for all children) (Kb): 43600
ERROR: no interpretation found !