Name | web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb45-21-opb/normalized-frb45-21-2.opb |
MD5SUM | a931f7e9a55cb6836807387327525e8b |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -36 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 945 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 945 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 945 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1195.04 |
Number of variables | 945 |
Total number of constraints | 58624 |
Number of constraints which are clauses | 58624 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 2 |
LAUNCH ON wulflinc7 THE 2005-09-18 18:45:24 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=2701 boxname=wulflinc7 idbench=357 idsolver=3 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a931f7e9a55cb6836807387327525e8b /oldhome/oroussel/tmp/wulflinc7/normalized-frb45-21-2.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc7/normalized-frb45-21-2.opb IDLAUNCH: 2701 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 913840 kB Buffers: 35624 kB Cached: 60536 kB SwapCached: 740 kB Active: 70156 kB Inactive: 28616 kB HighTotal: 131008 kB HighFree: 68320 kB LowTotal: 903652 kB LowFree: 845520 kB SwapTotal: 2097136 kB SwapFree: 2095892 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5716 kB Slab: 16324 kB Committed_AS: 64168 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-09-18 19:05:35 (client local time) WITH STATUS 10 IN 1208.32 SECONDS stats: 2701 7 1208.32 10
c Parsing PB file... c Converting 58624 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................ c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 58624 117248 | 19541 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: -31[0m c ---[ 0]---> Sorter-cost:44290 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 104213 224311 | 34737 0 0 nan | 0.000 % | c | 100 | 103753 223355 | 38210 63 352 5.6 | 0.799 % | c | 250 | 103075 221899 | 42031 184 1699 9.2 | 2.046 % | c | 475 | 101685 218869 | 46234 359 3428 9.5 | 4.676 % | c | 813 | 99941 215027 | 50858 624 5935 9.5 | 8.041 % | c ============================================================================== c [1mFound solution: -34[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1145 | 98367 211607 | 32789 875 9453 10.8 | 8.041 % | c | 1246 | 97670 210062 | 36067 936 10041 10.7 | 12.509 % | c | 1396 | 97202 209006 | 39674 1031 10925 10.6 | 13.452 % | c | 1621 | 95987 206277 | 43642 1161 12048 10.4 | 15.877 % | c | 1958 | 94801 203593 | 48006 1411 15086 10.7 | 18.255 % | c | 2464 | 92142 197582 | 52807 1692 17509 10.3 | 23.612 % | c | 3223 | 89622 191786 | 58087 2260 23288 10.3 | 28.835 % | c | 4362 | 85515 182365 | 63896 3094 31899 10.3 | 37.082 % | c | 6070 | 81641 173405 | 70286 4400 47324 10.8 | 45.054 % | c | 8632 | 76140 160465 | 77314 6222 77175 12.4 | 56.811 % | c | 12476 | 71881 150330 | 85046 9255 155440 16.8 | 66.013 % | c ============================================================================== c [1mFound solution: -35[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 14307 | 70810 147891 | 23603 10753 201061 18.7 | 66.013 % | c | 14407 | 70765 147784 | 25963 10841 202522 18.7 | 68.509 % | c | 14557 | 70765 147784 | 28559 10991 207402 18.9 | 68.509 % | c | 14783 | 70691 147602 | 31415 11185 216078 19.3 | 68.675 % | c | 15120 | 70586 147358 | 34557 11507 227319 19.8 | 68.886 % | c | 15626 | 70348 146787 | 38012 11951 241938 20.2 | 69.400 % | c | 16385 | 70089 146154 | 41814 12648 271863 21.5 | 69.975 % | c ============================================================================== c [1mFound solution: -36[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 16815 | 69891 145672 | 23297 13020 282802 21.7 | 69.975 % | c | 16915 | 69891 145672 | 25626 13120 284893 21.7 | 70.395 % | c | 17065 | 69891 145672 | 28189 13270 286399 21.6 | 70.395 % | c | 17290 | 69827 145517 | 31008 13475 295467 21.9 | 70.532 % | c | 17627 | 69734 145292 | 34109 13799 310942 22.5 | 70.743 % | c | 18133 | 69371 144409 | 37520 14192 322561 22.7 | 71.538 % | c ============================================================================== c [1mFound solution: -37[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 18277 | 69362 144430 | 23120 14335 325818 22.7 | 71.538 % | c | 18377 | 69362 144430 | 25432 14435 332585 23.0 | 71.584 % | c | 18527 | 69277 144233 | 27975 14556 347362 23.9 | 71.763 % | c | 18752 | 69277 144233 | 30772 14781 367844 24.9 | 71.763 % | c | 19089 | 69030 143626 | 33849 14950 374080 25.0 | 72.327 % | c | 19596 | 68741 142905 | 37234 15398 392392 25.5 | 73.016 % | c | 20355 | 68660 142718 | 40958 16081 432831 26.9 | 73.185 % | c | 21494 | 68513 142365 | 45054 17165 509426 29.7 | 73.511 % | c | 23202 | 68154 141510 | 49559 18653 641562 34.4 | 74.298 % | c ============================================================================== c [1mFound solution: -38[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 23824 | 67852 140729 | 22617 19046 663777 34.9 | 74.298 % | c | 23924 | 67766 140515 | 24878 19123 665280 34.8 | 75.183 % | c | 24074 | 67714 140393 | 27366 19252 669804 34.8 | 75.292 % | c | 24299 | 67714 140393 | 30103 19477 677322 34.8 | 75.292 % | c | 24636 | 67714 140393 | 33113 19814 696585 35.2 | 75.292 % | c | 25142 | 67678 140303 | 36424 20309 716491 35.3 | 75.375 % | c | 25902 | 67425 139703 | 40067 20929 797034 38.1 | 75.917 % | c | 27042 | 67212 139192 | 44074 21947 872312 39.7 | 76.383 % | c | 28750 | 67142 139014 | 48481 23609 1034815 43.8 | 76.548 % | c | 31312 | 67092 138893 | 53329 26102 1245314 47.7 | 76.657 % | c | 35156 | 66477 137377 | 58662 29648 1507713 50.9 | 78.057 % | c | 40922 | 66357 137092 | 64528 35234 2003265 56.9 | 78.315 % | c | 49572 | 66165 136632 | 70981 43618 2849495 65.3 | 78.733 % | c ============================================================================== c [1mFound solution: -39[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 53102 | 66131 136585 | 22043 46964 3239093 69.0 | 78.733 % | c | 53203 | 66092 136494 | 24247 19870 1267667 63.8 | 78.977 % | c | 53353 | 66092 136494 | 26672 20020 1277625 63.8 | 78.977 % | c | 53578 | 66092 136494 | 29339 20245 1297647 64.1 | 78.977 % | c | 53917 | 66083 136473 | 32273 20580 1329003 64.6 | 78.996 % | c | 54424 | 66083 136473 | 35500 21087 1371465 65.0 | 78.996 % | c | 55183 | 66081 136469 | 39050 21844 1449488 66.4 | 78.999 % | c | 56322 | 66081 136469 | 42955 22983 1576964 68.6 | 78.999 % | c | 58030 | 66081 136469 | 47251 24691 1727745 70.0 | 78.999 % | c | 60592 | 65903 136032 | 51976 27218 1994366 73.3 | 79.390 % | c | 64436 | 65748 135667 | 57173 31008 2368011 76.4 | 79.714 % | c | 70202 | 65748 135667 | 62891 36774 3054028 83.0 | 79.714 % | c | 78851 | 65630 135370 | 69180 45415 4281369 94.3 | 79.987 % | c | 91825 | 65630 135370 | 76098 58389 6085540 104.2 | 79.987 % | c ============================================================================== c [1mFound solution: -40[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 97446 | 65617 135317 | 21872 63942 6734885 105.3 | 79.987 % | c | 97546 | 65521 135083 | 24059 19913 1776166 89.2 | 80.240 % | c | 97696 | 65511 135059 | 26465 20062 1785837 89.0 | 80.262 % | c | 97921 | 65485 134999 | 29111 20286 1798820 88.7 | 80.316 % | c | 98258 | 65485 134999 | 32022 20623 1818617 88.2 | 80.316 % | c | 98765 | 65485 134999 | 35225 21130 1863451 88.2 | 80.316 % | c | 99525 | 65485 134999 | 38747 21890 1943719 88.8 | 80.316 % | c | 100667 | 65432 134870 | 42622 23023 2052223 89.1 | 80.433 % | c | 102376 | 65237 134387 | 46884 24634 2215179 89.9 | 80.881 % | c | 104938 | 65233 134377 | 51573 27193 2439838 89.7 | 80.891 % | c | 108784 | 65114 134084 | 56730 31017 2904470 93.6 | 81.164 % | c | 114550 | 64872 133502 | 62403 36617 3619951 98.9 | 81.689 % | c | 123199 | 64872 133502 | 68643 45266 4649642 102.7 | 81.689 % | c | 136175 | 64810 133346 | 75508 58227 6774965 116.4 | 81.838 % | c ============================================================================== c [1mFound solution: -41[0m c ---[ 0]---> Sorter-cost: 0 Base: c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 150026 | 64829 133402 | 21609 72073 8627626 119.7 | 81.838 % | c | 150126 | 64829 133402 | 23769 20486 1739332 84.9 | 81.817 % | c | 150276 | 64829 133402 | 26146 20636 1744519 84.5 | 81.817 % | c | 150501 | 64829 133402 | 28761 20861 1763472 84.5 | 81.817 % | c | 150839 | 64720 133135 | 31637 21184 1776192 83.8 | 82.068 % | c | 151345 | 64720 133135 | 34801 21690 1809498 83.4 | 82.068 % | c | 152104 | 64667 133003 | 38281 22431 1868161 83.3 | 82.192 % | c | 153244 | 64576 132788 | 42109 23332 1921393 82.4 | 82.385 % | c | 154952 | 64519 132644 | 46320 25032 2128460 85.0 | 82.515 % | c | 157514 | 64514 132633 | 50952 27592 2413144 87.5 | 82.525 % | c | 161359 | 64514 132633 | 56048 31437 2830357 90.0 | 82.525 % | c | 167125 | 64508 132619 | 61652 37198 3592888 96.6 | 82.538 % | c | 175774 | 64484 132559 | 67818 45837 4744404 103.5 | 82.595 % | c | 188750 | 64443 132458 | 74600 58799 6135883 104.4 | 82.690 % | c | 208211 | 64435 132438 | 82060 78258 8346917 106.7 | 82.709 % | c | 237404 | 64428 132421 | 90266 107448 11304159 105.2 | 82.725 % | c | 281193 | 64313 132144 | 99292 56003 5085663 90.8 | 82.979 % | c | 346877 | 64154 131750 | 109222 121446 12746175 105.0 | 83.347 % | c c *** TERMINATED *** s SATISFIABLE v -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 -C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 C883 -C882 -C881 -C880 C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 -C847 -C846 -C845 -C844 C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 -C708 -C707 -C706 C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 -C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 C380 -C379 C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 C321 -C320 -C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 -C266 -C26
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/26083/stat): 26083 (minisat+_script) R 26082 26083 15400 0 -1 0 19 0 0 0 0 0 0 0 23 0 1 0 1785314588 712704 3 4294967295 134512640 135087896 3221224512 3221224512 1073744960 0 0 5 0 0 0 0 17 0 0 0 Raw data (/proc/26083/statm): 174 3 169 147 0 27 0 [pid=26083] 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=26084 New process pid=26085 New process pid=26086 execve syscall for /bin/sed executable open syscall for file /etc/ld.so.preload One traced child (pid=26085) exited with status: 0 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=26086) exited with status: 0 One traced child (pid=26084) exited with status: 0 New process pid=26087 execve syscall for /oldhome/oroussel/solvers/minisat+_64-bit_static executable open syscall for file /dev/null open syscall for file /oldhome/oroussel/tmp/wulflinc7/normalized-frb45-21-2.opb [startup+10.0027 s] Raw data (loadavg): 1.08 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 3732 0 0 0 964 19 0 0 25 0 1 0 1785314593 15663104 3719 4294967295 134512640 135094434 3221224448 3221223108 134553515 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 3824 3719 145 145 0 3679 0 [pid=26087] vsize: 15296 Current children cumulated CPU time (s) 9.83 Current children cumulated vsize (Kb) 17420 [startup+20.0034 s] Raw data (loadavg): 1.07 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 3732 0 0 0 1964 19 0 0 25 0 1 0 1785314593 15663104 3719 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 3824 3719 145 145 0 3679 0 [pid=26087] vsize: 15296 Current children cumulated CPU time (s) 19.83 Current children cumulated vsize (Kb) 17420 [startup+30.004 s] Raw data (loadavg): 1.06 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 3732 0 0 0 2963 19 0 0 25 0 1 0 1785314593 15663104 3719 4294967295 134512640 135094434 3221224448 3221223108 134553446 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26087/statm): 3824 3719 145 145 0 3679 0 [pid=26087] vsize: 15296 Current children cumulated CPU time (s) 29.82 Current children cumulated vsize (Kb) 17420 [startup+40.0056 s] Raw data (loadavg): 1.05 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 3732 0 0 0 3963 19 0 0 25 0 1 0 1785314593 15663104 3719 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 3824 3719 145 145 0 3679 0 [pid=26087] vsize: 15296 Current children cumulated CPU time (s) 39.82 Current children cumulated vsize (Kb) 17420 [startup+50.0063 s] Raw data (loadavg): 1.04 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) T 26083 26083 15400 0 -1 0 3763 0 0 0 4963 19 0 0 25 0 1 0 1785314593 15810560 3750 4294967295 134512640 135094434 3221224448 3221222812 134870330 0 0 5 16386 3222434794 0 0 17 1 0 0 Raw data (/proc/26087/statm): 3860 3750 145 145 0 3715 0 [pid=26087] vsize: 15440 Current children cumulated CPU time (s) 49.82 Current children cumulated vsize (Kb) 17564 [startup+60.0069 s] Raw data (loadavg): 1.03 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 4114 0 0 0 5957 22 0 0 25 0 1 0 1785314593 16732160 3980 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26087/statm): 4085 3980 145 145 0 3940 0 [pid=26087] vsize: 16340 Current children cumulated CPU time (s) 59.79 Current children cumulated vsize (Kb) 18464 [startup+70.0086 s] Raw data (loadavg): 1.03 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 4570 0 0 0 6950 25 0 0 25 0 1 0 1785314593 18481152 4396 4294967295 134512640 135094434 3221224448 3221223072 134557565 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26087/statm): 4512 4396 145 145 0 4367 0 [pid=26087] vsize: 18048 Current children cumulated CPU time (s) 69.75 Current children cumulated vsize (Kb) 20172 [startup+80.0092 s] Raw data (loadavg): 1.09 1.03 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 5144 0 0 0 7939 30 0 0 25 0 1 0 1785314593 20811776 4970 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 5081 4970 145 145 0 4936 0 [pid=26087] vsize: 20324 Current children cumulated CPU time (s) 79.69 Current children cumulated vsize (Kb) 22448 [startup+90.0098 s] Raw data (loadavg): 1.07 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 5564 0 0 0 8932 32 0 0 25 0 1 0 1785314593 22511616 5390 4294967295 134512640 135094434 3221224448 3221223108 134553482 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 5496 5390 145 145 0 5351 0 [pid=26087] vsize: 21984 Current children cumulated CPU time (s) 89.64 Current children cumulated vsize (Kb) 24108 [startup+100.01 s] Raw data (loadavg): 1.06 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 6067 0 0 0 9925 35 0 0 25 0 1 0 1785314593 24686592 5893 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 6027 5893 145 145 0 5882 0 [pid=26087] vsize: 24108 Current children cumulated CPU time (s) 99.6 Current children cumulated vsize (Kb) 26232 [startup+110.011 s] Raw data (loadavg): 1.05 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 6552 0 0 0 10917 39 0 0 25 0 1 0 1785314593 26652672 6378 4294967295 134512640 135094434 3221224448 3221223060 134563049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 6507 6378 145 145 0 6362 0 [pid=26087] vsize: 26028 Current children cumulated CPU time (s) 109.56 Current children cumulated vsize (Kb) 28152 [startup+120.013 s] Raw data (loadavg): 1.04 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7076 0 0 0 11907 42 0 0 25 0 1 0 1785314593 28782592 6902 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 7027 6902 145 145 0 6882 0 [pid=26087] vsize: 28108 Current children cumulated CPU time (s) 119.49 Current children cumulated vsize (Kb) 30232 [startup+130.013 s] Raw data (loadavg): 1.04 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7414 0 0 0 12901 45 0 0 25 0 1 0 1785314593 29990912 7199 4294967295 134512640 135094434 3221224448 3221223104 134558016 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 7322 7199 145 145 0 7177 0 [pid=26087] vsize: 29288 Current children cumulated CPU time (s) 129.46 Current children cumulated vsize (Kb) 31412 [startup+140.014 s] Raw data (loadavg): 1.03 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7414 0 0 0 13902 45 0 0 25 0 1 0 1785314593 29990912 7199 4294967295 134512640 135094434 3221224448 3221223108 134553497 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 7322 7199 145 145 0 7177 0 [pid=26087] vsize: 29288 Current children cumulated CPU time (s) 139.47 Current children cumulated vsize (Kb) 31412 [startup+150.016 s] Raw data (loadavg): 1.03 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7414 0 0 0 14902 45 0 0 25 0 1 0 1785314593 29990912 7199 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 7322 7199 145 145 0 7177 0 [pid=26087] vsize: 29288 Current children cumulated CPU time (s) 149.47 Current children cumulated vsize (Kb) 31412 [startup+160.016 s] Raw data (loadavg): 1.02 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7415 0 0 0 15902 45 0 0 25 0 1 0 1785314593 29990912 7200 4294967295 134512640 135094434 3221224448 3221223120 134556434 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 7322 7200 145 145 0 7177 0 [pid=26087] vsize: 29288 Current children cumulated CPU time (s) 159.47 Current children cumulated vsize (Kb) 31412 [startup+170.017 s] Raw data (loadavg): 1.02 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 7751 0 0 0 16897 47 0 0 25 0 1 0 1785314593 31367168 7536 4294967295 134512640 135094434 3221224448 3221223120 134555574 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 7658 7536 145 145 0 7513 0 [pid=26087] vsize: 30632 Current children cumulated CPU time (s) 169.44 Current children cumulated vsize (Kb) 32756 [startup+180.018 s] Raw data (loadavg): 1.01 1.02 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 8325 0 0 0 17888 50 0 0 25 0 1 0 1785314593 33718272 8110 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 8232 8110 145 145 0 8087 0 [pid=26087] vsize: 32928 Current children cumulated CPU time (s) 179.38 Current children cumulated vsize (Kb) 35052 [startup+190.018 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 8847 0 0 0 18878 54 0 0 25 0 1 0 1785314593 35852288 8632 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 8753 8632 145 145 0 8608 0 [pid=26087] vsize: 35012 Current children cumulated CPU time (s) 189.32 Current children cumulated vsize (Kb) 37136 [startup+200.019 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 9331 0 0 0 19870 57 0 0 25 0 1 0 1785314593 37822464 9116 4294967295 134512640 135094434 3221224448 3221223040 134557413 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 9234 9116 145 145 0 9089 0 [pid=26087] vsize: 36936 Current children cumulated CPU time (s) 199.27 Current children cumulated vsize (Kb) 39060 [startup+210.019 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 9881 0 0 0 20860 61 0 0 25 0 1 0 1785314593 40062976 9666 4294967295 134512640 135094434 3221224448 3221223104 134558013 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 9781 9666 145 145 0 9636 0 [pid=26087] vsize: 39124 Current children cumulated CPU time (s) 209.21 Current children cumulated vsize (Kb) 41248 [startup+220.021 s] Raw data (loadavg): 1.01 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 10312 0 0 0 21852 65 0 0 25 0 1 0 1785314593 41816064 10097 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 10209 10097 145 145 0 10064 0 [pid=26087] vsize: 40836 Current children cumulated CPU time (s) 219.17 Current children cumulated vsize (Kb) 42960 [startup+230.022 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 10700 0 0 0 22845 67 0 0 25 0 1 0 1785314593 43397120 10485 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 10595 10485 145 145 0 10450 0 [pid=26087] vsize: 42380 Current children cumulated CPU time (s) 229.12 Current children cumulated vsize (Kb) 44504 [startup+240.022 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11086 0 0 0 23838 70 0 0 25 0 1 0 1785314593 44965888 10871 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 10978 10871 145 145 0 10833 0 [pid=26087] vsize: 43912 Current children cumulated CPU time (s) 239.08 Current children cumulated vsize (Kb) 46036 [startup+250.023 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 24835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223040 134551704 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0 [pid=26087] vsize: 44244 Current children cumulated CPU time (s) 249.07 Current children cumulated vsize (Kb) 46368 [startup+260.024 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 25835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0 [pid=26087] vsize: 44244 Current children cumulated CPU time (s) 259.07 Current children cumulated vsize (Kb) 46368 [startup+270.024 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 26835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0 [pid=26087] vsize: 44244 Current children cumulated CPU time (s) 269.07 Current children cumulated vsize (Kb) 46368 [startup+280.025 s] Raw data (loadavg): 1.00 1.01 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 27835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557879 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0 [pid=26087] vsize: 44244 Current children cumulated CPU time (s) 279.07 Current children cumulated vsize (Kb) 46368 [startup+290.025 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 28835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0 [pid=26087] vsize: 44244 Current children cumulated CPU time (s) 289.07 Current children cumulated vsize (Kb) 46368 [startup+300.026 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 29835 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0 [pid=26087] vsize: 44244 Current children cumulated CPU time (s) 299.07 Current children cumulated vsize (Kb) 46368 [startup+310.027 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 30836 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223040 134557336 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0 [pid=26087] vsize: 44244 Current children cumulated CPU time (s) 309.08 Current children cumulated vsize (Kb) 46368 [startup+320.027 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 31836 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0 [pid=26087] vsize: 44244 Current children cumulated CPU time (s) 319.08 Current children cumulated vsize (Kb) 46368 [startup+330.029 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 32836 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0 [pid=26087] vsize: 44244 Current children cumulated CPU time (s) 329.08 Current children cumulated vsize (Kb) 46368 [startup+340.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11211 0 0 0 33836 72 0 0 25 0 1 0 1785314593 45305856 10955 4294967295 134512640 135094434 3221224448 3221223104 134557903 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 11061 10955 145 145 0 10916 0 [pid=26087] vsize: 44244 Current children cumulated CPU time (s) 339.08 Current children cumulated vsize (Kb) 46368 [startup+350.03 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11505 0 0 0 34832 74 0 0 25 0 1 0 1785314593 46514176 11249 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 11356 11249 145 145 0 11211 0 [pid=26087] vsize: 45424 Current children cumulated CPU time (s) 349.06 Current children cumulated vsize (Kb) 47548 [startup+360.031 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 11994 0 0 0 35824 77 0 0 25 0 1 0 1785314593 48517120 11738 4294967295 134512640 135094434 3221224448 3221223104 134557934 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 11845 11738 145 145 0 11700 0 [pid=26087] vsize: 47380 Current children cumulated CPU time (s) 359.01 Current children cumulated vsize (Kb) 49504 [startup+370.032 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 12404 0 0 0 36816 81 0 0 25 0 1 0 1785314593 50450432 12148 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 12317 12148 145 145 0 12172 0 [pid=26087] vsize: 49268 Current children cumulated CPU time (s) 368.97 Current children cumulated vsize (Kb) 51392 [startup+380.032 s] Raw data (loadavg): 1.00 1.00 0.93 3/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 12800 0 0 0 37809 84 0 0 25 0 1 0 1785314593 52064256 12544 4294967295 134512640 135094434 3221224448 3221223040 134557429 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 12711 12544 145 145 0 12566 0 [pid=26087] vsize: 50844 Current children cumulated CPU time (s) 378.93 Current children cumulated vsize (Kb) 52968 [startup+390.034 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13142 0 0 0 38803 87 0 0 25 0 1 0 1785314593 53448704 12886 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13049 12886 145 145 0 12904 0 [pid=26087] vsize: 52196 Current children cumulated CPU time (s) 388.9 Current children cumulated vsize (Kb) 54320 [startup+400.034 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 39801 88 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 398.89 Current children cumulated vsize (Kb) 54780 [startup+410.034 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 40801 88 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 408.89 Current children cumulated vsize (Kb) 54780 [startup+420.035 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 41801 88 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 418.89 Current children cumulated vsize (Kb) 54780 [startup+430.035 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 42801 88 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 428.89 Current children cumulated vsize (Kb) 54780 [startup+440.036 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 43801 88 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223040 134557416 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 438.89 Current children cumulated vsize (Kb) 54780 [startup+450.037 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 44801 89 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 448.9 Current children cumulated vsize (Kb) 54780 [startup+460.039 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 45801 89 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 458.9 Current children cumulated vsize (Kb) 54780 [startup+470.04 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 46801 89 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 468.9 Current children cumulated vsize (Kb) 54780 [startup+480.041 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 47801 90 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223040 134556802 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 478.91 Current children cumulated vsize (Kb) 54780 [startup+490.042 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 48801 90 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 488.91 Current children cumulated vsize (Kb) 54780 [startup+500.043 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 49801 90 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 498.91 Current children cumulated vsize (Kb) 54780 [startup+510.043 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13299 0 0 0 50801 90 0 0 25 0 1 0 1785314593 53919744 13002 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13002 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 508.91 Current children cumulated vsize (Kb) 54780 [startup+520.044 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13300 0 0 0 51802 90 0 0 25 0 1 0 1785314593 53919744 13003 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13003 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 518.92 Current children cumulated vsize (Kb) 54780 [startup+530.045 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13300 0 0 0 52802 90 0 0 25 0 1 0 1785314593 53919744 13003 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13003 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 528.92 Current children cumulated vsize (Kb) 54780 [startup+540.046 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13300 0 0 0 53802 90 0 0 25 0 1 0 1785314593 53919744 13003 4294967295 134512640 135094434 3221224448 3221223104 134557818 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13003 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 538.92 Current children cumulated vsize (Kb) 54780 [startup+550.047 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13302 0 0 0 54802 90 0 0 25 0 1 0 1785314593 53919744 13005 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13005 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 548.92 Current children cumulated vsize (Kb) 54780 [startup+560.048 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13305 0 0 0 55802 90 0 0 25 0 1 0 1785314593 53919744 13008 4294967295 134512640 135094434 3221224448 3221223104 134558019 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13164 13008 145 145 0 13019 0 [pid=26087] vsize: 52656 Current children cumulated CPU time (s) 558.92 Current children cumulated vsize (Kb) 54780 [startup+570.048 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13395 0 0 0 56800 91 0 0 25 0 1 0 1785314593 54280192 13098 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13252 13098 145 145 0 13107 0 [pid=26087] vsize: 53008 Current children cumulated CPU time (s) 568.91 Current children cumulated vsize (Kb) 55132 [startup+580.049 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13686 0 0 0 57795 93 0 0 25 0 1 0 1785314593 55463936 13389 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13541 13389 145 145 0 13396 0 [pid=26087] vsize: 54164 Current children cumulated CPU time (s) 578.88 Current children cumulated vsize (Kb) 56288 [startup+590.049 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 13973 0 0 0 58790 95 0 0 25 0 1 0 1785314593 56627200 13676 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 13825 13676 145 145 0 13680 0 [pid=26087] vsize: 55300 Current children cumulated CPU time (s) 588.85 Current children cumulated vsize (Kb) 57424 [startup+600.05 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 14226 0 0 0 59784 98 0 0 25 0 1 0 1785314593 57667584 13929 4294967295 134512640 135094434 3221224448 3221223104 134557840 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 14079 13929 145 145 0 13934 0 [pid=26087] vsize: 56316 Current children cumulated CPU time (s) 598.82 Current children cumulated vsize (Kb) 58440 [startup+610.051 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 14510 0 0 0 60779 100 0 0 25 0 1 0 1785314593 58826752 14213 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 14362 14213 145 145 0 14217 0 [pid=26087] vsize: 57448 Current children cumulated CPU time (s) 608.79 Current children cumulated vsize (Kb) 59572 [startup+620.051 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 14780 0 0 0 61775 103 0 0 25 0 1 0 1785314593 59920384 14483 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 14629 14483 145 145 0 14484 0 [pid=26087] vsize: 58516 Current children cumulated CPU time (s) 618.78 Current children cumulated vsize (Kb) 60640 [startup+630.052 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 15029 0 0 0 62770 105 0 0 25 0 1 0 1785314593 60932096 14732 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 14876 14732 145 145 0 14731 0 [pid=26087] vsize: 59504 Current children cumulated CPU time (s) 628.75 Current children cumulated vsize (Kb) 61628 [startup+640.053 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 15223 0 0 0 63765 107 0 0 25 0 1 0 1785314593 61718528 14926 4294967295 134512640 135094434 3221224448 3221223104 134558249 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 15068 14926 145 145 0 14923 0 [pid=26087] vsize: 60272 Current children cumulated CPU time (s) 638.72 Current children cumulated vsize (Kb) 62396 [startup+650.053 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 15446 0 0 0 64761 109 0 0 25 0 1 0 1785314593 62627840 15149 4294967295 134512640 135094434 3221224448 3221223104 134557860 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 15290 15149 145 145 0 15145 0 [pid=26087] vsize: 61160 Current children cumulated CPU time (s) 648.7 Current children cumulated vsize (Kb) 63284 [startup+660.054 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 15651 0 0 0 65758 110 0 0 25 0 1 0 1785314593 63471616 15354 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 15496 15354 145 145 0 15351 0 [pid=26087] vsize: 61984 Current children cumulated CPU time (s) 658.68 Current children cumulated vsize (Kb) 64108 [startup+670.056 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 15854 0 0 0 66755 112 0 0 25 0 1 0 1785314593 64294912 15557 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 15697 15557 145 145 0 15552 0 [pid=26087] vsize: 62788 Current children cumulated CPU time (s) 668.67 Current children cumulated vsize (Kb) 64912 [startup+680.056 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 16048 0 0 0 67751 113 0 0 25 0 1 0 1785314593 65085440 15751 4294967295 134512640 135094434 3221224448 3221223104 134558178 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 15890 15751 145 145 0 15745 0 [pid=26087] vsize: 63560 Current children cumulated CPU time (s) 678.64 Current children cumulated vsize (Kb) 65684 [startup+690.058 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 16244 0 0 0 68747 115 0 0 25 0 1 0 1785314593 65880064 15947 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 16084 15947 145 145 0 15939 0 [pid=26087] vsize: 64336 Current children cumulated CPU time (s) 688.62 Current children cumulated vsize (Kb) 66460 [startup+700.058 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 16423 0 0 0 69743 116 0 0 25 0 1 0 1785314593 66596864 16126 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26087/statm): 16259 16126 145 145 0 16114 0 [pid=26087] vsize: 65036 Current children cumulated CPU time (s) 698.59 Current children cumulated vsize (Kb) 67160 [startup+710.059 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 16630 0 0 0 70740 117 0 0 25 0 1 0 1785314593 67436544 16333 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 16464 16333 145 145 0 16319 0 [pid=26087] vsize: 65856 Current children cumulated CPU time (s) 708.57 Current children cumulated vsize (Kb) 67980 [startup+720.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 16860 0 0 0 71734 120 0 0 25 0 1 0 1785314593 68382720 16563 4294967295 134512640 135094434 3221224448 3221223104 134557956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 16695 16563 145 145 0 16550 0 [pid=26087] vsize: 66780 Current children cumulated CPU time (s) 718.54 Current children cumulated vsize (Kb) 68904 [startup+730.06 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17085 0 0 0 72730 122 0 0 25 0 1 0 1785314593 69292032 16788 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 16917 16788 145 145 0 16772 0 [pid=26087] vsize: 67668 Current children cumulated CPU time (s) 728.52 Current children cumulated vsize (Kb) 69792 [startup+740.062 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17310 0 0 0 73726 123 0 0 25 0 1 0 1785314593 70217728 17013 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17143 17013 145 145 0 16998 0 [pid=26087] vsize: 68572 Current children cumulated CPU time (s) 738.49 Current children cumulated vsize (Kb) 70696 [startup+750.063 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17527 0 0 0 74723 124 0 0 25 0 1 0 1785314593 71098368 17230 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17358 17230 145 145 0 17213 0 [pid=26087] vsize: 69432 Current children cumulated CPU time (s) 748.47 Current children cumulated vsize (Kb) 71556 [startup+760.063 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 75722 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134558159 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 758.47 Current children cumulated vsize (Kb) 71696 [startup+770.064 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 76722 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 768.47 Current children cumulated vsize (Kb) 71696 [startup+780.064 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 77722 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134558395 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 778.47 Current children cumulated vsize (Kb) 71696 [startup+790.065 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 78722 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 788.47 Current children cumulated vsize (Kb) 71696 [startup+800.066 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 79723 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223136 134554723 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 798.48 Current children cumulated vsize (Kb) 71696 [startup+810.066 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 80723 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 808.48 Current children cumulated vsize (Kb) 71696 [startup+820.067 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 81723 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 818.48 Current children cumulated vsize (Kb) 71696 [startup+830.068 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 82724 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134558004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 828.49 Current children cumulated vsize (Kb) 71696 [startup+840.069 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 83723 125 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 838.48 Current children cumulated vsize (Kb) 71696 [startup+850.07 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 84723 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557948 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 848.49 Current children cumulated vsize (Kb) 71696 [startup+860.07 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 85723 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223072 134562149 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 858.49 Current children cumulated vsize (Kb) 71696 [startup+870.07 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 86723 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 868.49 Current children cumulated vsize (Kb) 71696 [startup+880.071 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 87723 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223088 134558264 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 878.49 Current children cumulated vsize (Kb) 71696 [startup+890.071 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 88723 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134558213 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 888.49 Current children cumulated vsize (Kb) 71696 [startup+900.072 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 89724 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 898.5 Current children cumulated vsize (Kb) 71696 [startup+910.073 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 90724 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223040 134557421 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 908.5 Current children cumulated vsize (Kb) 71696 [startup+920.073 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 91724 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 918.5 Current children cumulated vsize (Kb) 71696 [startup+930.074 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17563 0 0 0 92724 126 0 0 25 0 1 0 1785314593 71241728 17266 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17266 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 928.5 Current children cumulated vsize (Kb) 71696 [startup+940.075 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 93724 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223108 134553530 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 938.5 Current children cumulated vsize (Kb) 71696 [startup+950.075 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 94725 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223040 134557248 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 948.51 Current children cumulated vsize (Kb) 71696 [startup+960.076 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 95725 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 958.51 Current children cumulated vsize (Kb) 71696 [startup+970.077 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 96725 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 968.51 Current children cumulated vsize (Kb) 71696 [startup+980.077 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 97725 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134558126 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 978.51 Current children cumulated vsize (Kb) 71696 [startup+990.079 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 98726 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 988.52 Current children cumulated vsize (Kb) 71696 [startup+1000.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 99726 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557877 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 998.52 Current children cumulated vsize (Kb) 71696 [startup+1010.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 100726 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 1008.52 Current children cumulated vsize (Kb) 71696 [startup+1020.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 101726 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 1018.52 Current children cumulated vsize (Kb) 71696 [startup+1030.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 102726 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557937 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 1028.52 Current children cumulated vsize (Kb) 71696 [startup+1040.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 103727 126 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 1038.53 Current children cumulated vsize (Kb) 71696 [startup+1050.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 104726 127 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 1048.53 Current children cumulated vsize (Kb) 71696 [startup+1060.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 105726 127 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 1058.53 Current children cumulated vsize (Kb) 71696 [startup+1070.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 106726 127 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223104 134558187 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 1068.53 Current children cumulated vsize (Kb) 71696 [startup+1080.08 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17564 0 0 0 107726 128 0 0 25 0 1 0 1785314593 71241728 17267 4294967295 134512640 135094434 3221224448 3221223040 134557180 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17393 17267 145 145 0 17248 0 [pid=26087] vsize: 69572 Current children cumulated CPU time (s) 1078.54 Current children cumulated vsize (Kb) 71696 [startup+1090.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 17784 0 0 0 108722 130 0 0 25 0 1 0 1785314593 72142848 17487 4294967295 134512640 135094434 3221224448 3221223104 134558007 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26087/statm): 17613 17487 145 145 0 17468 0 [pid=26087] vsize: 70452 Current children cumulated CPU time (s) 1088.52 Current children cumulated vsize (Kb) 72576 [startup+1100.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 18010 0 0 0 109718 131 0 0 25 0 1 0 1785314593 73064448 17713 4294967295 134512640 135094434 3221224448 3221223040 134557219 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 17838 17713 145 145 0 17693 0 [pid=26087] vsize: 71352 Current children cumulated CPU time (s) 1098.49 Current children cumulated vsize (Kb) 73476 [startup+1110.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 18182 0 0 0 110715 133 0 0 25 0 1 0 1785314593 73777152 17885 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 0 0 0 Raw data (/proc/26087/statm): 18012 17885 145 145 0 17867 0 [pid=26087] vsize: 72048 Current children cumulated CPU time (s) 1108.48 Current children cumulated vsize (Kb) 74172 [startup+1120.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 18434 0 0 0 111708 135 0 0 25 0 1 0 1785314593 74813440 18137 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 18265 18137 145 145 0 18120 0 [pid=26087] vsize: 73060 Current children cumulated CPU time (s) 1118.43 Current children cumulated vsize (Kb) 75184 [startup+1130.09 s] Raw data (loadavg): 1.00 1.00 0.93 3/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 18686 0 0 0 112704 137 0 0 25 0 1 0 1785314593 75845632 18389 4294967295 134512640 135094434 3221224448 3221223104 134558210 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 18517 18389 145 145 0 18372 0 [pid=26087] vsize: 74068 Current children cumulated CPU time (s) 1128.41 Current children cumulated vsize (Kb) 76192 [startup+1140.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 18892 0 0 0 113700 139 0 0 25 0 1 0 1785314593 76689408 18595 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 18723 18595 145 145 0 18578 0 [pid=26087] vsize: 74892 Current children cumulated CPU time (s) 1138.39 Current children cumulated vsize (Kb) 77016 [startup+1150.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 19118 0 0 0 114696 140 0 0 25 0 1 0 1785314593 77606912 18821 4294967295 134512640 135094434 3221224448 3221223088 134562104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 18947 18821 145 145 0 18802 0 [pid=26087] vsize: 75788 Current children cumulated CPU time (s) 1148.36 Current children cumulated vsize (Kb) 77912 [startup+1160.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 19326 0 0 0 115692 142 0 0 25 0 1 0 1785314593 78454784 19029 4294967295 134512640 135094434 3221224448 3221223120 134556266 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 19154 19029 145 145 0 19009 0 [pid=26087] vsize: 76616 Current children cumulated CPU time (s) 1158.34 Current children cumulated vsize (Kb) 78740 [startup+1170.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 19529 0 0 0 116688 144 0 0 25 0 1 0 1785314593 79802368 19232 4294967295 134512640 135094434 3221224448 3221223104 134557928 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 19483 19232 145 145 0 19338 0 [pid=26087] vsize: 77932 Current children cumulated CPU time (s) 1168.32 Current children cumulated vsize (Kb) 80056 [startup+1180.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 19757 0 0 0 117684 146 0 0 25 0 1 0 1785314593 80732160 19460 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 19710 19460 145 145 0 19565 0 [pid=26087] vsize: 78840 Current children cumulated CPU time (s) 1178.3 Current children cumulated vsize (Kb) 80964 [startup+1190.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 20022 0 0 0 118681 148 0 0 25 0 1 0 1785314593 81809408 19725 4294967295 134512640 135094434 3221224448 3221223104 134557991 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 19973 19725 145 145 0 19828 0 [pid=26087] vsize: 79892 Current children cumulated CPU time (s) 1188.29 Current children cumulated vsize (Kb) 82016 [startup+1200.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 20252 0 0 0 119677 149 0 0 25 0 1 0 1785314593 82743296 19955 4294967295 134512640 135094434 3221224448 3221223104 134557906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 20201 19955 145 145 0 20056 0 [pid=26087] vsize: 80804 Current children cumulated CPU time (s) 1198.26 Current children cumulated vsize (Kb) 82928 [startup+1210.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 20267 0 0 0 120677 149 0 0 25 0 1 0 1785314593 82804736 19970 4294967295 134512640 135094434 3221224448 3221223072 134557685 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 20216 19970 145 145 0 20071 0 [pid=26087] vsize: 80864 Current children cumulated CPU time (s) 1208.26 Current children cumulated vsize (Kb) 82988 Maximum CPU time exceeded: sending SIGTERM then SIGKILL [startup+1210.09 s] Raw data (loadavg): 1.00 1.00 0.93 2/57 26087 Raw data (/proc/26083/stat): 26083 (minisat+_script) S 26082 26083 15400 0 -1 0 289 239 0 0 0 0 0 0 22 0 1 0 1785314588 2174976 226 4294967295 134512640 135087896 3221224512 3221223784 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (/proc/26083/statm): 531 226 485 147 0 384 0 [pid=26083] vsize: 2124 Raw data (/proc/26087/stat): 26087 (minisat+_64-bit) R 26083 26083 15400 0 -1 0 20267 0 0 0 120678 149 0 0 25 0 1 0 1785314593 82804736 19970 4294967295 134512640 135094434 3221224448 3221223104 134557837 0 0 5 16386 0 0 0 17 1 0 0 Raw data (/proc/26087/statm): 20216 19970 145 145 0 20071 0 [pid=26087] vsize: 80864 Current children cumulated CPU time (s) 1208.27 Current children cumulated vsize (Kb) 82988 Sending SIGTERM to -26083 Sleeping 2 seconds One traced child (pid=26083) ended because it received signal 15 (SIGTERM) One traced child (pid=26087) exited with status: 10 All traced children have exited ! Game is over. Child status: 10 Real time (s): 1210.14 CPU time (s): 1208.32 CPU user time (s): 1206.78 CPU system time (s): 1.53877 CPU usage (%): 99.8498 Max. virtual memory (cumulated for all children) (Kb): 82988
ERROR: no interpretation found !